Re: [isabelle] Syntax issue: lost between HOL and Isar



On 8/2/2012 11:17 AM, Lawrence Paulson wrote:
ML is a programming language. You write programs in ML.

Pure is not a programming language. It is a logical formalism, specifically, the logical framework that is the basis of Isabelle.

HOL is also a programming language, namely higher-order logic.

Isar is a formal language for proof developments. These are not programs and it is not a programming language.

Larry, thanks. I'm making some progress here. I've acquired some resolution for the word "language". A language that's used on a computer is not necessarily a "programming language". Sounds reasonable. I guess. It's hard for me not to think of a sequence of instructions as a program.

Now all I have to do is figure out exactly what the "Isar proof language" is, and what between "theory" and "end" isn't Isar.

It gets a little difficult to sort it all out. ML is a programming language which is used to implement Isar, which is a formal language, but not a programming language, and Isar is used to implement HOL, which is a programming language, and the syntax for Isar and "HOL syntax" is all intertwined, where you occasionally drop down into the ML programming language to use an "Isar command", like "Outer_syntax.command", to define syntax for the HOL programming language.

I'll check out on this thread, and store away any other comments that come in for future reference.

Regards,
GB


Larry Paulson


On 2 Aug 2012, at 16:46, Gottfried Barrow wrote:

One last comment, hopefully.

Outer_syntax is defined in src/Pure/Isar/outer_syntax.ML:

    (*  Title:      Pure/Isar/outer_syntax.ML
        Author:     Markus Wenzel, TU Muenchen

    The global Isabelle/Isar outer syntax.

I was wanting to start using the phrase "the Pure programming language", but "Outer_syntax.command" is an Isar command, so the HOL outer syntax "datatype" is defined as HOL syntax using an Isar command.

My use of "the Pure programming language" will have to wait until I understand whether there's any HOL syntax which can be defined using ML, but which cannot be defined using Isar.

I like to have the vocabulary locked down. I go with these ideas until someone tells me different.

Regards,
GB











This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.