Re: Layout syntax

<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

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