22 Jan 2004 23:10:58 -0500

Related articles |
---|

[11 earlier articles] |

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: | 22 Jan 2004 23:10:58 -0500 |

Organization: | Mathematics |

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

Keywords: | syntax, design |

Posted-Date: | 22 Jan 2004 23:10:58 EST |

<joachim.durchholz@web.de> wrote:

*>I think we've been talking a bit at cross-purpose here:*

*>* You are interested in doing pure mathematics.*

*>* I am interested in proving the properties of programs, with as much*

*>automation as possible and reasonable.*

The point is that, on a suitable generality level, these two should be the

same. :-)

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

*>>> automatically detectable proofs.*

*>*

*>The main issue here is that, for my objectives, all practically*

*>relevant theorems are those based on a given program. That's a*

*>tremendous amount of information that a theorem prover can use, since*

*>the program structure already reflects the proof structure. Also, all*

*>properties of a program can be proven using constructive*

*>mathematics. This also eases the task of the prover tremendously.*

This sounds like you want some kind of generalization of a Hindley-Milner

type system to include constructive math: The Hindley-Milner type system

uses unification to find the most general type that a program can fulfill.

I have not been thinking along those lines.

*>Any theorem prover that's intended for checking (or even finding)*

*>valid theorems in general mathematics has a far harder job: it cannot*

*>restrict itself to constructive mathematics, and it doesn't have a*

*>program. My goals are far more modest than yours :-)*

The way I think the application in computer programming to be, is that a

theorist proves an algorithm of some kind. Then somebody makes an

implementation of that algorithm, and one wants to ensure that it indeed

produces the result of the proven algorithm.

I think this should be an implementation of a statement that is a

specialization of the proven algorithm, and one should from the

implementation be able to extract a proof that it is. I have not spent

time on the algorithm verification issue, though.

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

*>*

*>This would probably be a good approach for error reporting in a program*

*>property prover as well.*

*>*

*>I'm not sure that this is enough though.*

To me, the main point is that I get a very simple system that is easy for

one person to develop. :-)

*> If the*

*>programmer/mathematician expects the prover to get along from one*

*>theorem to the next without the programmer's help, and the prover*

*>doesn't, this may mean one of two things: Either the prover is too*

*>dumb, or the programmer/mathematician made a mistake. I'm not sure*

*>what strategies would help the programmer/mathematician to find out*

*>which situation holds, and how to remedy the situation in the fastest*

*>possible way.*

The stuff that does not get proved is marked down with [*unproved*] in the

output file. If not direct inspection reveals exactly what the problem is,

one can, in my system, turn on local debugging that writes out the details

of the proof in the parts that one so wants. One will then be able to see

what is wrong.

*>For programmers, the error may even be in the theorems he wants to*

*>prove (i.e. he stated a theorem that's more general than is needed,*

*>and that actually doesn't hold). I'm not sure how common such a*

*>situation might be for a mathematician (I could imagine that similar*

*>situations could occur when the mathematician sets up a lemma, but I'm*

*>not sure how far this is relevant - the work of a mathematician is far*

*>more open-ended than that of a programmer).*

Actually, this is a very amusing situation that happens when I work up the

system, because the computer will immediately recognize such errors. Then,

of course, any proof will fail. A theorem without a valid proof will also

be marked down with [*unproved*] in the output file.

Any statement that is unproved, for a subsequent proof to succeed, can

only be used as a theorem assumption. This is in fact what one is doing

with conjectures: Using a conjecture directly as a statement will cause

all theorems using it to fail. But one can use it as an assumption in

other provable theorems, showing that it implies some other assumption.

This way, one gets a logically consistent core.

Hans Aberg

Post a followup to this message

Return to the
comp.compilers page.

Search the
comp.compilers archives again.