Divide-and-Conquer Logic Algorithm Analysis

Let s first restrict ourselves to binary predicates, and present a most basic strategy that already yields solutions to many problems. 

A divide-and-conquer algorithm for a binary predicate r over parameters X and Y works as follows. Let X be the induction parameter. IfX is minimal, then Y is (usually) easily found by directly solving the problem. Otherwise, that is if X is non-minimal, decompose X into a vector HX of heads of X and a vector TX of tails of X, the tails being of the same type as X, as well as smaller than X according to some well-founded relation. The tails TX recursively yield tails TY of Y. The heads HX are processed into a vector HY of heads of Y. Finally, Y is composed from its heads HY and tails TY. 

For further discussion, we quantify the vectors as follows. There are h heads of X, and h heads of Y, and t tails of X, hence t tails of Y. Thus  

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. 

Note that we prefer the verb decompose to divide , and that the combine operation is actually split into a process operation and a compose operation. 

---