Re: syntax extension, was Why context-free?

Karsten Nyblad <148f3wg02@sneakemail.com>
1 Nov 2005 21:44:00 -0500

          From comp.compilers

Related articles
Why context-free? nmm1@cus.cam.ac.uk (2005-10-06)
Re: Why context-free? bobduff@shell01.TheWorld.com (Robert A Duff) (2005-10-07)
Re: Why context-free? nmm1@cus.cam.ac.uk (2005-10-08)
Re: syntax extenstion, was Why context-free? haberg@math.su.se (2005-11-01)
Re: syntax extension, was Why context-free? toby@telegraphics.com.au (toby) (2005-11-01)
Re: syntax extension, was Why context-free? nmm1@cus.cam.ac.uk (2005-11-01)
Re: syntax extension, was Why context-free? 148f3wg02@sneakemail.com (Karsten Nyblad) (2005-11-01)
Re: syntax extension, was Why context-free? gah@ugcs.caltech.edu (glen herrmannsfeldt) (2005-11-02)
Re: syntax extension, was Why context-free? haberg@math.su.se (2005-11-02)
Re: syntax extension, was Why context-free? toby@telegraphics.com.au (toby) (2005-11-04)
Re: syntax extension, was Why context-free? henry@spsystems.net (2005-11-26)
Re: syntax extension, was Why context-free? haberg@math.su.se (2005-11-27)
Re: syntax extension, was Why context-free? mpah@thegreen.co.uk (2005-12-08)
[3 later articles]
| List of all articles for this month |

From: Karsten Nyblad <148f3wg02@sneakemail.com>
Newsgroups: comp.compilers
Date: 1 Nov 2005 21:44:00 -0500
Organization: Compilers Central
References: 05-10-053 05-10-061 05-10-062 05-11-004
Keywords: syntax
Posted-Date: 01 Nov 2005 21:43:59 EST

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


Post a followup to this message

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