Deductive and Inductive Synthesis of Equational Programs

An equational approach to the synthesis of functional and logic program is taken. Typically, the synthesis task involves finding equations which make the given specification an inductive theorem. To synthesize such programs, induction is necessary. We formulate efficient procedures for inductive proof as well as program synthesis using the framework of ordered rewriting. We also propose heuristics for generalizing from a sequence of equational consequences. These heuristics handle cases where the deductive process alone is not adequate to come with a program. 1 Introduction In a seminal piece of work, Burstall and Darlington [BD77] showed how functional programs, expressed as equations, can be transformed to more efficient ones using equational reasoning. Given a specification of a new function to be synthesized, they use the original program equations forwards ("unfolding") and backwards ("folding") in a controlled fashion and obtain a recursive program for the new function. The meth..