Automatic Extraction of a Solution

The logic we are using is designed to facilitate the automatic derivation of programs from specifications, where the specification is taken to be a statement of solubility, and the proof serves as a guide for realizing that solution concretely. See Automatic Extraction for an explanation of the method. Our theorem

Thm*  n:, p,q:Peg.
Thm*  p  q
Thm*  
Thm*  (a:. 
Thm*  (z:{a...}, s:({a...z}{1...n}Peg).
Thm*  (s is a Hanoi(n disk) seq on a..z & s(a) = (i.p) & s(z) = (i.q))

is such a specification claiming the existence of a sequence of the right sort given the appropriate preconditions. When we gave Standard Solution Explicitly, it was based on reading the proof of the above theorem. We shall see that the program extracted automatically from that proof bears a striking resemblance to the one we constructed explicitly, the difference being that the automatically extracted program has a number of trivial elements that neither contribute nor detract significantly from the computation, although they are somewhat distracting to the reader trying to understand the extracted program directly.

About: IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html