An automatic programming system, THESYS, for constructing recursive LISP programs from examples of what they do is described. The construction methodology is illustrated as a series of transformations from the set of examples to a program satisfying the examples. The transformations consist of (1) deriving the specific computation associated with a specific example, (2) deriving control flow predicates, and (3) deriving an equivalent program specification in the form of recurrence relations. Equivalence between certain recurrence relations and various program schemata is proved. A detailed description of the construction of four programs is presented to illustrate the application of the methodology.

This paper reports on a system, THESYS, that synthesizes LISP recursive programs from examples of what they do. There has been recent interest in this form of program specification[1,4,8]. The theory of such inductive systems has been investigated by Blum and Blum[2], Kugel[5] and Summers[10]. In this paper we describe the practical results of an investigation into the problem of program synthesis from examples. The methodology to be presented is based on a firm theoretical foundation which may provide a basis for generalizing the results to other kinds of program synthesis systems. The various theoretical models for computation and data that comprise the theory are not described in detail in this paper but may be found in [10].