Re: [isabelle] Context Free Language
On Fri, 23 Nov 2012, Jens Doll wrote:
let me again ask a question about Isabelle proofs in common. Being a
formal language professional I wonder why these artefacts in your proof
libraries need the abstract language level at all. In my opinion most of
the proofs could be specified in context free syntax with the semantics
attached to it or having semantics in mind or specified elsewhere. If
we had the proofs in a CH(2) pattern we could build transformers to
transfer them to and from other formalisms, which in turn would foster
exchange with other groups building proof libraries worldwide. Am I
wrong or is there a reason for maintaining such a hurdle?
Ancient LCF tradition already started this "syntax-less" attitude: it is
all just "semantics" (in ML) with some notation to produce it, and it is
extensible in all directions.
The Isar framework emphasizes this further, allowing the user (or rather
tool implementor) to invent new languages and embed them into the system.
Even the core proof language does not have fixed syntax, although there is
a reconstruction of some of it in appendix A of the isar-ref manual. This
integration of many languages is actually more close to common practice in
the world out there: consider "HTML5" and its many sub-languages that are
not HTML at all.
This archive was generated by a fusion of
Pipermail (Mailman edition) and