A Divide-and-Conquer Logic Algorithm Schema

Note that a canonical representation is not unique, because of the possible permutations of parameters. The permutations of parameters as in the schema can t be imposed at the instance level, because there is no possible control over how problems, and hence predicates, are defined. We can t thus introduce a concept such as the normalized representation of a logic algorithm. 

Almost all logic algorithms of this book are canonical representations wrt some schema in this chapter. 

In essence, the divide-and-conquer design strategy solves a problem by the following sequence of three steps  

Hence the name of the strategy. In the sequel, we focus on applying this strategy to data-structures, rather than to states of partial computations. 

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

---

Third, we only aim at the synthesis of single-loop logic algorithms. In other words, we assume that the only loop is the one that is achieved in the schema by the recursion on the induction parameter, and that none of the instances of the predicate-variables is defined recursively (possibly as a divide-and-conquer logic algorithm). 

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. 

Second, as we already have hinted when stopping the incremental inference of different versions of a divide-and-conquer schema, version 4 of that schema is far from covering all possible divide-and-conquer logic algorithms. 

Logic algorithms designed by this basic divide-and-conquer strategy are covered by Schema 8-1, where R(TX,T ) stands for ai j R TXj,TYj), and j is a notation-variable. 

Is the mechanism able to design the whole family of possible logic algorithms for a given problem This ability is in theory achieved for the family of algorithms that are covered by version 3 of the divide-and-conquer schema. In practice, everything depends on the completeness of the databases used by Steps 2 and 3. How many structural forms are there Due to our restriction to version 3 of the divide-and-conquer schema. Task C of Step 2 only considers the distinction between two structural forms, namely one minimal form and one non-minimal form. A generalization of this task is considered future research. 

A possible solution is to automatically infer a property set of the intended relation and then to use an entire synthesis mechanism (such as the one described in the two previous chapters) in order to infer a logic algorithm that is complete wrt the given examples and inferred properties. We here describe such a method, called the Synthesis Method, which is specific to the synthesis of the Processj and Composej predicate-variables of the divide-and-conquer schema. 

---