2 Nov 2005 22:11:59 -0500

From: | haberg@math.su.se (Hans Aberg) |

Newsgroups: | comp.compilers |

Date: | 2 Nov 2005 22:11:59 -0500 |

Organization: | Mathematics |

References: | 05-10-053 05-10-061 05-10-062 05-11-004 05-11-014 |

Keywords: | design |

Posted-Date: | 02 Nov 2005 22:11:59 EST |

Karsten Nyblad <148f3wg02@sneakemail.com> wrote:

*> > I am somewhat interested in this question, writing on a theorem prover,*

*> > because in pure math, there is not universal accepted notation...*

*> 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.*

It turns out that TeX is wholly unsuitable, as it is a graphically

oriented format. The formulas should be entered in a semantically

correct manner, and one should develop a suitable syntax for

that. Therefore, I am developing my own, better suited, format. Once

the formulas have been properly entered and parsed, it becomes easy to

add suitable pretty-printing format.

The current pretty-printer tries to write closely to the input

theorems and proofs, with additional diagnostics, i.e., whether a

statement was proved or not. One can also write out the proofs in a

human readable format. This is needed for proper debugging.

*> 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.) *

This is, as you say one very important aspect. If the formulas are not

readable to me, then I cannot debug properly. Right know, the most

difficult part is to make sure the proofs are completely accurate

(according to standard metamath).

In fact I have come quite far. Instead of a Prolog first depth search, I

make a breadth first search, and I have a format to write out the proofs

by which I can easily check their accuracy. (I have been able to attain

some automated induction proofs, i.e., the theorem prover finds the

induction predicate, and the user only needs to guess which formulas to

use in order to cut down the proof search paths.)

In addition, I have recently started to use Unicode UTF-8, using correct

mathematical symbols instead of ASCII words. This turns out to help up the

code a great deal.

*> I think such a front end and pretty printer is much more important than*

*> a facility for changing the grammar of the input.*

As always in math, notions and notation are closely intertwined. In

the computer language design version, semantics and syntax should be

closely worked together. Since I am the only user, it suffices right

now to use a static grammar, handled by Flex and Bison. But the

question is what dynamic extensibility will lingers on the horizon.

*> 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.*

Right now, I want to avoid doing anything more than the core

math. Thus, I have only a very small math set which contains only some

math core components to play around with.

But it runs out that one can do quite much with a text only syntax,

both using only ASCII, but also using UTF-8. A graphical pretty

printer would be beneficial for handling sup-/super-scripts and other

more complex math notation. But right now, I do not have so much need

for that.

--

Hans Aberg

Post a followup to this message

Return to the
comp.compilers page.

Search the
comp.compilers archives again.