Re: syntax extension, was Why context-free?

Hans Aberg wrote:
> I am somewhat interested in this question, writing on a theorem prover,
> because in pure math, there is not universal accepted notation: each paper
> can in principle have its own syntax, even though heavily dictated by the
> notions at hand, as well by traditions. So this calls for some
> extensibility. But too much extensibility will probably be quite unusable
> from the practical point of view. So there is a question what might be
> suitable to tuck this syntax problem conveniently away, from the
> implementation point of view.


Normally a theorem prover has some sort of interactive interface where
you can develop a script that proves your theorems. The formulas
entered are unreadable. If you want to prove some mathematical theorem,
then you have to enter a formula as readable as a formula written in
TeX. If you want to prove some some aspect of a program, then you have
to deal with formulas so long, that they are difficult to understand
because of that. The formulas are not only those entered by the human,
they are also formulas generated by the theorem prover during the
interactive process of proving theorems.


In both cases you need the theorem prover to present the formulas in a
way such that they are understandable to human readers. (You need the
theorem prover to present your input in a human readable way so that you
can proofread your input.) You need some sort of pretty printer, that
can present math formulas in the way used in books on math, and computer
programs and states in the way used in computer science books. This
should be integrated into some sort of IDE like tool, that acts as a
front end to the theorem prover just like an IDE acts as a front end to
the compiler and debugger.


I think such a front end and pretty printer is much more important than
a facility for changing the grammar of the input.


Karsten Nyblad
148f3wg02 at sneakemail dot com

Return to the comp.compilers page.
Search the comp.compilers archives again.