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



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.

Regards,
GB





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