Re: [isabelle] Context Free Language



On Fri, 23 Nov 2012, Jens Doll wrote:

Hello all.

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.


	Makarius


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