2 Jan 2004 03:43:26 -0500

Related articles |
---|

[3 earlier articles] |

Re: Layout syntax cdc@maxnet.co.nz (Carl Cerecke) (2003-12-13) |

Re: Layout syntax joachim.durchholz@web.de (Joachim Durchholz) (2003-12-14) |

Re: Layout syntax haberg@matematik.su.se (2003-12-20) |

Re: Layout syntax joachim.durchholz@web.de (Joachim Durchholz) (2003-12-21) |

Re: Layout syntax haberg@matematik.su.se (2003-12-23) |

Re: Layout syntax joachim.durchholz@web.de (Joachim Durchholz) (2003-12-27) |

Re: Layout syntax haberg@matematik.su.se (2004-01-02) |

Re: Layout syntax joachim.durchholz@web.de (Joachim Durchholz) (2004-01-07) |

Re: Layout syntax haberg@matematik.su.se (2004-01-09) |

Re: Layout syntax joachim.durchholz@web.de (Joachim Durchholz) (2004-01-12) |

Re: Layout syntax haberg@matematik.su.se (2004-01-16) |

Re: Layout syntax joachim.durchholz@web.de (Joachim Durchholz) (2004-01-18) |

Re: Layout syntax bayard@newsguy.com (Ian Zimmerman) (2004-01-18) |

[4 later articles] |

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

Newsgroups: | comp.compilers |

Date: | 2 Jan 2004 03:43:26 -0500 |

Organization: | Mathematics |

References: | 03-12-016 03-12-060 03-12-081 03-12-104 03-12-112 03-12-124 03-12-131 03-12-136 |

Keywords: | syntax |

Posted-Date: | 02 Jan 2004 03:43:26 EST |

<joachim.durchholz@web.de> wrote:

*>> The question is what happens when math is written proof verification*

*>> system, as the computer can easily check any nesting: then manual*

*>> unnesting will no longer needed. So one will probably see more of*

*>> such nesting then.*

*>I don't think that this would be a Good Thing.*

*>After all, proofs aren't just read by computers, they are also read by*

*>humans (e.g. to check whether a proof states what was intended, or to*

*>modify a proof to prove something slightly different but more*

*>interesting), and humans don't parse nested constructs very well.*

This is a type of discussion about the influence of computers that I

have already lived through several times: When calculators first

arrived in the seventies, many felt one should not departure from

knowledge about how it was calculated. But eventually, the calculators

became more accurate, and then nobody, expect experts, cares exactly

how those calculations are done.

The same thing will most surely happen with computer languages: At a

point in time when the implementations of algorithms and proofs can be

mathematically rigorously and reliably checked by the computer, there

will be no need for humans to do that checking, except when

implementing the proof checking programs themselves. Those that write

proofs will do that interactively with a computer, just as one is

doing in programming. So it will not be needed to wrote proofs so that

humans can directly check them, even though humans still must be able

to write proofs.

But getting there is a long way to go.

*>I think we're largely in agreement, and just differ in how far one*

*>should go when trying to import mathematical conventions into a*

*>computerized language.*

Let's generalize typical computer type systems, and see where we might

land: Hindley-Milner type systems rely on unification to resolve

polymorphic types. The next generalization might be a type system that

make use of a Prolog engine, of which unification is a part then. And

generalizing that, one might instead make use of a proof checking

engine, based on metamathematics. Then the type system might be

something like axiomatic set theory. If one gets that far, one has

unified computer type systems with pure math. :-)

*>I.e. I agree that arithmetic operators should be in any language, I'm*

*>not so sure about difficult-to-parse constructs like lambdas without a*

*>lambda keyword (but it might be worth the effort if the language is*

*>specifically tailored towards expressing traditional math),*

Church's (lambda x.f) is in working math often written as x |-> f. The way

I handle these syntactic differences when implementing my proof checking

program is by designing it around "semantic trees": A semantic tree is a

(finite) labelled ordered tree. A parse tree is a semantic tree, and one

can get new semantic trees by specializing via suitable grammar rule

actions. With this terminology in hand, the semantic trees of (lambda x.f)

and x |-> f will be

lambda |->

/ \ / \

x f x f

That is, they will be the same except for a trivial relabelling of the

nodes: lambda <-> |->. This is in fact a common situation in math: Even

though notation may vary, one often seems to agree fairly well on what

these semantic trees should be.

So it is by that easy to find a common semantic representation in the

computer. And so it will not make any difference which syntax is used in a

formula, in the sense that one can allow local parsing contexts.

Hans Aberg

Post a followup to this message

Return to the
comp.compilers page.

Search the
comp.compilers archives again.