1 Nov 2005 21:44:00 -0500

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] |

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 |

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.