Automatic synthesis of recursive programs as proof procedures

Publication date 23 January 1993

inductive action specifications program synthesis

Research exposition (monographs, survey articles) pertaining to computer science (68-02)

The book is a reprint of the author's PhD thesis. It is devoted to a particular problem in the area of proving mathematical theorems by means of a computer. There are, however, also applications in other areas, for example the automated synthesis of algorithms and computer programs, or the automated generated of recursive plans from inductive action specifications. The particular problem the book is concerned with the following: Given is the recursive definition of some mathematical objects (data structures), for example natural numbers, lists or trees, together with definitions of functions and predicates operating on these data structures and some properties of these functions and predicates. All this is formulated in first order predicate logic (actually a many sorted version of predicate logic.) Now we want to prove a theorem of the kind \(\forall x_ 1,\dots,x_ n \exists y \Phi(x_ 1,\dots,x_ n,y)\) from these specifications. In a program synthesis application, the \(x_ i\) would be the input variables and \(y\) would be the output variable. The ``mathematical way to prove this theorem would be to guess a function \(f(x_ 1,\dots,x_ n)\) and prove the theorem \(\forall x_ 1,\dots,x_ n \Phi(x_ 1,\dots,x_ n,f(x_ 1,\dots,x_ n))\) with mathematical induction. Semi automated procedures as for example Boyer and Moores' inductive theorem prover support only the verification part, i.e. the user has to come up with a definition for \(f\). More elaborate methods like Manna and Waldinger's program synthesis method give concrete recipes for finding candidates for \(f\). They are, however, not yet in a state where the recipe can be applied fully automatically. The author describes a method for solving this problem fully automatically. The procedure systematically manipulates the definition of the data structures and the theorem \(\Phi\) by means of heuristically controlled applications of transformation rules until a definition of \(f\) is obtained. This is then, also automatically, verified by an inductive theorem prover. Since the problem is known to be incomplete, i.e. there can be no algorithm that is guaranteed to come up with a solution when there is one, the proposed method must be partial. Nevertheless, it has been implemented and it performs well on nontrivial examples. Listed examples are the completeness proof for a propositional theorem prover, the synthesis of the reverse function for lists, the synthesis of a sorting function and the synthesis of a function for computing integer quotient and remainder.

Recommendations

Cited in

(30)

This page was built for publication: Automatic synthesis of recursive programs as proof procedures

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4023948)