Re: Layout syntax

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

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