16 Jan 2004 22:29:17 -0500

Related articles |
---|

[7 earlier articles] |

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

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

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

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

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

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

Newsgroups: | comp.compilers |

Date: | 16 Jan 2004 22:29:17 -0500 |

Organization: | Mathematics |

References: | 03-12-016 03-12-136 04-01-014 04-01-021 04-01-034 04-01-056 |

Keywords: | design, syntax |

Posted-Date: | 16 Jan 2004 22:29:17 EST |

<joachim.durchholz@web.de> wrote:

*>> So when merely attempting to implement a proof checker for formal*

*>> proofs written out in full that makes a correct use of*

*>> metamathematics, there are a number of mathematical subtleties,*

*>> which I do not think any system today handles. Surprise, surprise!*

*>*

*>Interesting - I had been thinking that this kind of thing was long solved.*

There are two problems, to ensure one gets the generality one expects

in math, and to surely map down that one gets ones favorite

mathematical theory. Most systems introduce severe mathematical

limitations, and it is hard to know that one for sure gets exactly

what metamathematics describes.

For example, in a formulation like "this program builds on ZFC", one

does not for sure know that one gets the ZFC (Zermelo-Fraenkel

axiomatic set theory + Continuum hypothesis) of pure math, and

mathematicians have not agreed that one should use ZFC.

On another level, in which language should the metatheorems be proved?

There appears to emerge a more fundamental framework here. Qu-Prolog seems

to contain some of this framework. This is also a question that interests

me.

*>> -- But if somebody can give me a reference to a 100% correct proof*

*>> checking system according to standard metamathematics, please let me*

*>> know.*

*>*

*>Coq? At least that's what's usually quoted at this point of the*

*>discussion (but I don't know much about it myself).*

Thank you for the suggestion. I had a brief look at it. It said

something to the effect that it is lambda-calculus based. In a

metamathematical approach, one ends up adding binders (which binds

free variables), of which the lambda is a special case. So it suggests

that Coq is, as apparently other programs, more limited in scope, not

usable for general pure math.

*>At a minimum, the hand-written proof must include the sub-theorems of*

*>all proofs by induction that are needed (and such a proof is required*

*>for every loop and every recursion present, and the induction*

*>information translates to loop invariants resp. assertions on the*

*>recursive functions).*

*>And, of course, the final theorems that one wants proven should be*

*>written down :-)*

*>These are the minimum requirements to make the task of giving a proof*

*>decidable.*

Actually, it is worse, because the Deduction Theorem (if A |- B then

|- A => B) in quantified theory of typical Hilbert metamathematics

requires one to have knowledge about the proofs as well. Computer

scientists can get around this, it seems, by making use of Gentzen

sequents. But these cannot capture the full generality of the Hilbert

metamathematics. I have now implemented unification branching, which

seems to be able to handle the Hilbert metamathematics. But I do not

know yet how to implement the full Deduction Theorem.

*> Besides, explicitly writing down loop invariants will improve code*

*>readability, so it's no loss if programmers have to write this down.*

*>After that, constructing the proof is "just" worst-case exponential*

*>in time and space... but there are a few theorems in Formal Logic*

*>that can drastically cut down the search space.*

I am not sure I can parse it.

But the path I explore is how to preserve the structure that

mathematicians use when describing math. I think that is very

essential for success to handling full pure math. So I do not deal

with optimizations, as it is already too complicated. And clever

rewritings usually destroy the structures that is essential when

describing the math.

*>> Also, not every theorem has a proof (by Goedel incompleteness), and*

*>> there is no algorithm to tell which theorems have a proof.*

*>*

*>It's my firm belief that all practically relevant theorems have*

*>automatically detectable proofs.*

This is essentially an AI (Artificial Intelligence) problem: If one

can make computers to think creatively about math the way humans can,

then they can prove any theorem a human can do. But otherwise not.

It is in fact difficult to handle very simple things like the

nontermination that MP (Modus Ponens: A, A => B |- B) produces. Simple

search cutoff techniques destroys the ability to tell whether the

statement is unprovable from a set of axioms.

*>BTW when looking at the source code of a typical program, the required*

*>"proofs" aren't much more than modus ponens, with the occasional*

*>transformation of boolean expressions. That's no wonder: other*

*>programming styles tend to be unmaintainable.*

The rules of inference (essentially Prolog clauses with non-empty

body) are very few in standard metamathematics. However, there are a

few more in quantification theory, and they are linked to the use of

the binding of variables, which becomes very complex. This is, in

fact, what makes the description of infinities possible, from which

the incompleteness theorems (Goedel, etc.) also becomes possible.

*>My idea of theorem proving in connection with practical programming goes*

*>like this:*

*>*

*>1. The programmer writes a program.*

*>2. The programmer wants to make sure that his program satisfies some*

*>property. The exact nature of that property can vary: it might be a*

*>statement on the program's results (or just a part of its results), or*

*>on resource usage, or that it doesn't access certain resources, or*

*>doesn't leak information - whatever the situation, it's the programmer*

*>who decides which properties are interesting in the first place.*

*>3. The programmer formalizes the properties, getting a theorem.*

*>4. The theorem prover proves (or disproves) the theorem.*

The formal metamathematical framework is very clear: Theorems are

developed in a clear succession, verified by proofs.

In an interactive computer system, one can let the user experiment against

a fully proved body. This is fact a very interesting aspect.

But it will not affect the structure of the metamathematical body.

*>Of course, details may vary wildly. The theorems could be set up before*

*>the first line of code is written. The programmer might have to state*

*>lemmas to help the theorem prover along. The theorem prover would have*

*>to be quite smart about reporting errors, since just a "the property*

*>doesn't hold" response isn't going to be very helpful. Etc. etc.*

Actually, I have a very simple system: One writes the math, axioms,

theorems, proofs, etc., in a file. Then one runs the program, and if all

is syntactically correct, it writes an output file with the same math, but

indicating the statements whose proofs failed. One can get further

diagnostics in a log file, the deductions of selected math portions, etc.

This way, it is usually easy to capture errors.

One can of course think of an interactive system, but I have no need for

that right now. One might also view the output math as "compiled code"

which can be read instead of the source file, as theorem proving is time

consuming. But I have no need for that either right now.

*>But I think that it could be done, with current technology. Even if*

*>there's no working theorem prover that correctly handles all current*

*>metamathematics - we don't need to prove mathematical statements, we*

*>want to prove statements about programs, at the level of formalization*

*>that the relevant programming language has.*

Actually, I ended up implementing the so called first order

metamathematical theory (not to be confused with first order Prolog

systems, which are more special) as described in mainly Mendelson's

book. The only reason is that this description is very clear and easy

to use for implementation. The underlying proving machinery does not

as such have any requirements of a first order metamathematical

theory, but the limitations are imposed by the parser alone.

Hans Aberg

Post a followup to this message

Return to the
comp.compilers page.

Search the
comp.compilers archives again.