Automatic Inductive Synthesis of Functional Programs.pdfVIP

Automatic Inductive Synthesis of Functional Programs Nachum Dershowitz and Ely Pinchover School of Computer Science Tel Aviv University Ramat Aviv, Tel Aviv 69978, Israel {nachumd,elypinch}@tau.ac.il Abstract. An automated system for the synthesis of functional pro- grams, expressed as a convergent set of rewrite rules, is presented. De- ductive and inductive rewriting techniques are combined to synthesize a program from a formal specification. Deductive consequences of an equational specification, and of equations expressing domain knowledge, are produced by a completion-based inference engine. The novel compo- nent of the system is its incorporation of inductive techniques to guess program clauses, which are then subjected to verification. This paper describes the heuristics that are employed for generalizing from a set of deductive consequences to form new equations. The proof-by-consistency method is then used to establish validity in the initial algebra of newly suggested program rules. In the same fashion, induction is used to guess lemmata needed in the proof and deduction is used to verify them. An ex- perimental ML implementation, geared to programs dealing with natural numbers and recursive data structures, has been written and is described. The judicious combination of completion, heuristic generalization, and inductive theorem proving allows it to derive provably correct programs fully automatically. 1 Introduction Rewriting [10, 23] is a very powerful method for dealing computationally with equations. Oriented e