Introduction to Algorithm Schemata

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

The following logic algorithm for the sort/2 problem is also known as Naive-Sort  

This algorithm is an instance of the generate-and-test schema, namely via the second-order substitution R/sort, Generate permutation, Test ordered, XIL, F/S.  

Reality is more complex, however. Function-variables and predicate-variables may have any arity, and this calls for schema-variables to denote these arities. Conjunctions, disjunctions, or quantifications of any length may appear, and this calls for schema-variables to denote the ranges of such ellipses. Permutations of parameters, conjuncts, disjuncts, or quantifications may have to be performed in order to see why a logic algorithm is an instance of some schema. Unfold transformations may have to be performed in order to see why a logic algorithm is an instance of some schema. 

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. 

---