Re: Layout syntax

<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

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