Automated synthesis of recursive programs from a ∀∃ logical specification

The specification of a function is often given by a logical formula, called a For All There Exists-formula, of the following form: For All x There Exists y Phi(x, y). More precisely, a specification is given in the context of a certain theory E and is stated by the judgment E proves For All x There Exists y Phi(x, y). In this paper, we consider the case in which E is an equational theory. It is divided into two parts. In the first part, we develop a theory for the automated proof of such judgments in the initial model of E. The validity in the initial model means that we consider not only equational theorems but also inductive ones. From our theory we deduce an automated method for the proof of a class of such judgments. In the second part, we present an automated method for program synthesis. We show how the previous proof method can be used to generate a recursive program for a function f that satisfies a judgment E proves For All x Phi(x, f(x)). We illustrate our method with the automated synthesis of some recursive programs on domains such as integers and lists. Finally, we describe our system LEMMA, which is an implementation in Common Lisp of these new methods.