9 Jan 2004 23:34:54 -0500

Related articles |
---|

[5 earlier articles] |

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

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

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

[2 later articles] |

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

Newsgroups: | comp.compilers |

Date: | 9 Jan 2004 23:34:54 -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 04-01-014 04-01-021 |

Keywords: | syntax |

Posted-Date: | 09 Jan 2004 23:34:54 EST |

Joachim Durchholz <joachim.durchholz@web.de> wrote:

*>> <joachim.durchholz@web.de> wrote:*

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

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

*>I didn't mean checking the validity of the proof - programs for doing*

*>that have been written decades ago.*

One must keep the distinction between a formal proof in the sense of

metamathematics written out in full, and a proof in the sense that humans

write it. A formal proof of a theorem S |-_T A, where S is a set of

formulas and T a formal theory, consists of a sequence of formulas A_1,

..., A_k = A, where each A_i is either a member of S or T, or a

consequence by a rule of inference in T from formulas before it in the

sequence. In principle, it ought to be easy to write a proof checker for

formal proofs, but in reality there are several complications: For

example, it is tricky to implement the metamathematics that is actually in

use in pure mathematics, and humans rarely write a full formal proof, but

a simplified version.

For the first problem, I know only of one system that implements binders

(like quantifiers, lambda that binds free object variables) in any way

that one might make correct metamathematics, namely, Qu-Prolog:

http://www.itee.uq.edu.au/~pjr/HomePages/QuPrologHome.html

But I recently discovered some mathematical problems with it, and it does

not seem to make use of the type theory one uses in metamathematics.

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! -- But if somebody can give me a reference to

a 100% correct proof checking system according to standard

metamathematics, please let me know.

Then, if one by a proof means what humans usually write, then there is no

clear distinction between a proof checker and a theorem prover, as the

human written simplified proof merely invokes a proof search engine that

is doing more work. The most extremely simplified proof is the empty one,

which leads to the classical idea of a theorem prover. Also, the search

engine will in any case be a modified Prolog type proof engine, so from

the point of implementation, there is no clear distinction either.

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

is no algorithm to tell which theorems have a proof. So an automated

theorem prover can never expect to prove all theorems. In fact, most

theorem provers pretty quickly cannot handle typical pure math. In

addition, automated proof techniques makes one to loose the ability to

know whether a statement is unprovable by a set of axioms: The reason is

that it is easy to implement empirical search techniques that can tell

whether it found a proof.

*>I meant checking that the theorem being proven is actually what we want*

*>proven.*

The way you have worded this sentence, there is no way for a computer to

tell if a theorem makes sense; only humans can do that. So you probably

mean something else.

*>For example, every tax calculation program is an existence proof*

*>for a best way of filling out the tax forms given a set of input*

*>parameters under the constraints of obeying the tax laws. This can also*

*>be done in reverse: when I have a proof that such a solution exists,*

*>without using the law of the excluded middle, then a program that*

*>calculates the value can be automatically derived from the proof.*

What you describe here is just a standard way to form a mathematical

theory: One has as a basis certain axioms and rules of inference

(essentially Prolog clause plus metamathematical typing), and proves from

them some theorems. Then from axioms and theorems, one may want to prove

new theorems.

When one calculates a value, invokes a proved algorithm, or proves that

two an implementation of an algorithm actually produces the results of the

algorithm, those are just examples of theorems with proof. So, from the

formal point of view, one does not get anything new here, even though it

may be difficult to find good ways to implement practical systems.

*>When I mistype or misinterpret the laws, the program is still a proof*

*>(resp. there's still a specification and an automatically deduced*

*>program), but not for the theorem that I wanted proven.*

This means that you want to invoke a formerly proved theorem in a illegal

manner. In a formal sense, what you will not be a formal proof with

respect to the given theory. Thus what you write will not pass as a formal

proof, and will be rejected by the proof checking system.

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

*>Actually that's a road that I'd like to explore. (I think it's already*

*>being done in academia, though I haven't heard of practial results yet.)*

The funny thing is that I do not know of any such investigations that

build on a formally correct metamathematics. The system that comes the

most close is the above mentioned Qu-Prolog.

For my experimentation, I started with the Mini-Prolog that comes with

Hugs <http://haskell.org/hugs/>, and translated it into C++. Then I

replaced its slow parser with a Flex/Bison generated lexer/parser. This

resulted in a very good object-oriented Prolog engine, suitable for

experimentation with CLP and other techniques.

Eventually, I embarked onto the idea of attempting to implement a formally

correct metamathematics. I use books on metamathematics by Elliott

Mendelson, Stephen Cole Kleene, and Joseph R. Shoenfield. On that road I

am right now.

Hans Aberg

Post a followup to this message

Return to the
comp.compilers page.

Search the
comp.compilers archives again.