
Re: Formal Proof Language Example  HumanReadable?
Posted:
Jun 21, 2009 5:04 PM


Jan Burse schrieb: > Except maybe the "," in Prolog, which has the meaning of a kind of > a conjunction. But in Prolog the "," is mostly treated as any other > operator. With a level and a associativity etc.. So maybe we can > advance the discussion as follows. You want the following operator: > > ";" : Conjunction > "forall" : Universal quantifier > "implies": Implication > "thereexists" : Existential quantifier > > Ok, now tell me, how will the story continue for proof figures?
(c) Jan Burse
Ok, here is a hint. Proofs are usually a mesh. So it is quite crucial that axioms, lemmas, etc.. can be labled. At least this is one approach, and it can practically not be avoided.
In normal programming languages we have a many objects that are nameable. For example variables and functions. This is alreay quite nice, since they are on different levels. And a similar thing will also happen to proofs.
So there will be proofs where the mathematician himself will give names, in the form of lemmas, subtheorems, etc.. We could use function object syntax for that:
lemma helper1 { }
lemma helper2 { }
And there will be proof steps, the mathematician is refering in his phrasing of the proofs. We could use variable object syntax for that:
step line21 = lamma helper2 { step line22 =
}
We can only introduce local variables, when the step is really not used outside. So we will have local and global steps. And the step itselfs will be not tactics, but inference rule applications, or axiom schema instantiations. Something like:
step line21 = eqReflex("y"); lemma helper2 { step line22 = modusPonens(line21,helper1); return line22; }
The verification could also be done by constant evaluation, a compiler could do this at compile time. We could combine proofs and other code. Maybe use proofs in assertions. Wow!
Does this make sense to you?
Bye

