Schema-guided synthesis

Since deductive inference is generally a familiar notion, we do not survey it here. We rather directly propose a taxonomy of the different ways of applying deductive inference to program synthesis from axiomatic specifications. Thus, Sections 2.2.1 to 2.2.3 respectively contain general introductions to transformational synthesis, proofs-as-programs synthesis, and schema-guided synthesis. 

Schema-guided synthesis was argued for in Section 8.1 because schemas are an interesting way of incorporating algorithm design knowledge into a synthesis process. Schema-guided synthesis is naturally a stepwise synthesis, as the predicate-variables are not all instantiated at the same time. A most interesting approach was then advocated in Section 8.3, namely to deploy an entire tool-box of predicate-variable instantiating methods, rather than a unique method. In Chapter 9 (Proofs-as-Programs Method) and Chapter 10 (MSG Method), we described two of the more sophisticated methods we have developed so far. Note that these methods are entirely dissociated from specific schemas or predicate-variables.

P. Flener and Y. Deville. Towards stepwise, schema-guided synthesis of logic programs. In [Clement and Lau 92], pp. 46-64. 

In Chapter 2, we survey the use of deductive inference in automatic programming. Axiomatic specifications are expected to be complete and non-ambiguous, but are usually also quite lengthy and artificial. Deductive synthesis from axiomatic specifications can be classified into transformational synthesis, proofs-as-programs synthesis (or constructive synthesis), and schema-guided synthesis. We survey the achievements of deductive synthesis of LISP functions and Prolog predicates. 

Stepwise, Schema-Guided Logic Algorithm Synthesis... 

A few researchers have tackled this lack of discipline in the synthesis of recursive logic programs from examples for instance, [Tinkham 90] and [Sterling and Kirschenbaum 93] investigate the use of schemas to guide synthesis. Curiously, the now virtually defunct research on trace-based synthesis of functional programs from examples [Summers 77] [Biermann 78] did not suffer from such a marked lack of discipline , even though this research preceded ILP research. 

In the sub-area of synthesis from incomplete specifications, schemas are often implicitly or explicitly present to guide the synthesis. Early systems based on divide-and-conquer schemas are described by [Shaw et al. 75], [Hardy 75], [Summers 77], and [Biermann and Smith 79]. 

The divide-and-conquer strategy was presented as an attractive strategy in Section 8.2, because of its diverse applicability, efficient results, and simplicity of application. The chosen approach for developing a synthesis mechanism is thus stepwise synthesis guided by a divide-and-conquer schema. 

The presented synthesis mechanism is guided by version 3 of the divide-and-conquer logic algorithm schema. This preliminary restriction (made in Section 11.2) has considerably simplified the notations needed for the theoretical presentation. The support of version 4 (relations of any non-zero arity) is actually a pretty straightforward extension, because only some additional vectorization is needed. Version 4 is actually supported by the implementation of the synthesis mechanism. 

In other words, a Step 0 would be to select an appropriate schema, and the subsequent steps would be either a hardwired sequence (specific to the selected schema) of applications of methods, or a user-guided selection of variables and methods. Our grand view of algorithm synthesis systems thus is one of a large workbench with a disparate tool-box of highly specialized methods for a set of schemas that covers (as much as possible of) the space of all possible algorithms. 

In Part III, we develop an actual logic algorithm synthesis mechanism from specifications by examples and properties, as seen in Chapter 6. It fits the particular non-incremental synthesis strategy presented in Chapter 7, is guided by the divide-and-conquer algorithm schema seen in Chapter 8, and uses the tool-box of methods developed in Chapters 9 and 10. 

---