Algorithm schema

Due to their diversity and their internal algorithms, schema matchers may have very specific parameters and/or user preferences. Here, we propose to detail some of them. 

Example 8-1 Here is a logic algorithm schema for the generate-and-test strategy ... 

A wff schema language is thus needed to write realistic logic algorithm schemas. The formal definition of such a language and of its semantics is beyond the scope of this book, so we do not develop it. But we know from experience that the intuitive understanding of our schemata is sufficient. 

Definition 8-1 A logic algorithm schema is a closed wff schema of the form ... 

Hereafter, we drop the universal quantifications in front of the heads, as well as any existential quantifications at the beginning of the bodies of logic algorithm schemas. 

It is evident that a logic algorithm schema without function-variables, predicate-variables, and schema-variables is a logic algorithm. 

Definition 8-2 An instance of a logic algorithm schema is a logic algorithm obtained by the following sequence of operations ... 

Logic Algorithm Schema 8-1 Divide-and-conquer (version 1)... 

First, in view of having a theoty of logic algorithm schemas and a formalization of the accompanying notions of instantiation and classification, a language for wff schemas needs to be developed, as well as its semantics defined. 

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. 

However, version 3 of the divide-and-conquer schema is hardwired into our synthesis mechanism. This results from a hardwired sequence of instantiations of predicate-variables of that schema, as well as from a hardwired mapping between these predicate-variables and the methods of the developed tool-box. Parameterizing the synthesis mechanism on algorithm schemas and tool-boxes would thus be a first step towards supporting schemas reflecting design strategies other than divide-and-conquer. 

Connectives for logic algorithms, schemas, properties, and implicative goals ... 

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. 

---