Computational uses of the manipulation of formal proofs
Chris Goad · Medical Entomology and Zoology · 1980
Mechanical procedures the manipulation of formal proofs have played a central role in proof theory more than fifty years. However, such procedures have not been widely applied to computational problems. One reason this is that work in computer science concerning formal proof systems has emphasized the use of formal proofs as evidence--as tools automatically establishing the truth of propositions. As a consequence of this emphasis, the problem of mechanizing the construction of proofs has received much attention, whereas the manipulation of proofs--that is, the conversion of one form of evidence into another--has not. However, formal proofs can serve purposes other than the presentation of evidence. In particular, a formal proof of a proposition having the form, for each x there is a such that the relation R holds between x and y provides, under the right conditions, a method computing values of from values of x. That is, such a proof describes an algorithm A where A satisfies the specification R in the sense that each x, R(x,A(x)) holds. Thus formal proof systems can serve as programming languages--languages the formal description of algorithms. A proof which describes an algorithm may be by use of any of a variety of procedures developed in proof theory. A proof differs from more conventional descriptions of the same algorithm in that it formalizes additional information about the algorithm beyond that formalized in the conventional description. This additional information expands the class of transformations on the algorithm which are amenable to automation. For example, there is a class of transformations which improve the computational efficiency of a natural deduction proof regarded as a program by removing unneeded case analyses. These transformations make essential use of dependency information which finds formal expression in a proof, but not in a conventional program. Pruning is particularly useful removing redundancies which arise when a general purpose algorithm is adapted to a special situation by symbolic execution. This thesis concerns (1) computational uses of the additional information contained in proofs, and (2) efficient methods the representation and transformation of proofs. An extended lambda-calculus is presented which allows compact expression of the computationally significant part of the information contained in proofs. Terms of the calculus preserve dependency data, but can be efficiently executed by an interpreter of the kind used lambda-calculus based languages such as LISP. The calculus has been implemented on the Stanford Artificial Intelligence Laboratory PDP-10 computer. Results of experiments on the use of pruning transformations in the specialization of a bin-packing algorithm are reported.