Re: [isabelle] Syntax issue: lost between HOL and Isar
Le Sat, 04 Aug 2012 22:03:59 +0200, Gottfried Barrow
<gottfried.barrow at gmx.com> 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.” 
“Structured Programming supports the law of the excluded muddle.” 
: Epigrams on Programming — Alan J. — P. Yale University
This archive was generated by a fusion of
Pipermail (Mailman edition) and