Re: syntax extension, was Why context-free?

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

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