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

Le Sat, 04 Aug 2012 22:03:59 +0200, Gottfried Barrow <gottfried.barrow at> a écrit:

On 8/2/2012 10:42 AM, Lars Noschinski wrote:

"HOL syntax" is not a very useful term here. In Isabelle/Isar, we distinguish between outer and inner syntax. The inner syntax is the syntax used to input terms (and types). Apart from trivial cases, inner syntax needs to be quoted.

The outer syntax is everything else. Most of it is already part of Pure (i.e. independent of any logic), mainly everything which makes up proof and document structure; but logics often add additional commands for logic-specific operations (e.g. "fun" and "inductive" for HOL).

I think I have it.

HOL imports pure, therefore it inherits the Isar language and a default set of Isar outer syntax commands, where new outer syntax can be defined with "Outer_syntax.command". Everything in a .thy file is Isar syntax and everything is HOL syntax, so there's no need to talk about HOL syntax, since, again, everything is HOL syntax. We could, however, compare Isabelle/HOL syntax with Isabelle/FOL syntax, where they would both share the default Isar outer syntax commands.

The word "term" doesn't have a lot of significance to me. I assume you mean "lambda calculus term", but I see very little lambda calculus in expressions between double quotes, so it doesn't completely help me to know what to put in double quotes.

However, it is useful to know that if I see something in double quotes, I know it must be either a type or a lambda calculus term, even if the lambda calculus doesn't look like lambda calculus.


Except for the technical details about which I didn't investigate, I feel to understand about the same as I read documents explaining Isabelle (actually, Markus Wenzel's thesis you pointed to, a captivating document): the distinction between inner and outer syntax, does not map the distinction between Isabelle‑Pure and the rest. If all is defined by extension in terms derived and derived‑derived from the Isabelle‑Pure core, and if extension can apply to both the outer and inner syntax, then the distinction is not that meaningful. Finally, may inner syntax is for some kind of expressions, and expressions which are not lexically atomic. Perhaps that's a layout choice inspired by simplifying parsing. Can we say what is a value (ex. contains variables of all kinds) and is not lexically atomic (or is lexically atomic, but whose name is not a simple name), have to be written in quotes? Just that?

“Syntactic sugar causes cancer of the semi-colons.” [1]
“Structured Programming supports the law of the excluded muddle.” [1]
[1]: Epigrams on Programming — Alan J. — P. Yale University

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