Recursive non-minimal case

Several aspects of logic algorithm design can be discussed now. We first propose a useful terminology for logic algorithm classification, and then show in what sense minimal cases and non-recursive non-minimal cases, though syntactically similar, are totally different concepts. 

As the logic algorithms of this book exhibit, not all non-minimal cases are recursive. Indeed, prefix-traversal logic algorithms have non-recursive non-minimal cases. But some structural cases of logic algorithms in Chapter 4, or [Deville 90], seem hard to classify. There are several potential reasons to this. 

A first reason is that non-recursive non-minimal cases of prefix-scan logic algorithms can often be merged with their minimal cases. The resulting algorithm looks like it has no minimal case. It exhibits cases whose structural forms are not mutually exclusive, and is thus easy to detect as being a rewriting of the canonical version. 

The form L = L J is not minimal, as it overlaps with the other form. It rather results from a merger of the minimal case and the non-recursive non-minimal case. ... 

Another reason for non-recursive non-minimal cases is recursion elimination by partial evaluation. The result is a non-minimal case that looks like a minimal case. This is hard to detect, since the cases still exhibit mutually exclusive structural forms. There is no limit to creating non-recursive non-minimal cases by partial evaluation. 

It is important to understand that such logic algorithms with non-recursive, non-minimal cases are the result of re-writing canonical logic algorithms, rather than unpleasant aberrations. 

Such is however not the case with the SolveNonMin, where Decompose and Discriminate are explicitly present this is for reasons of homogeneity with the recursive non-minimal case. This even implies that instances of the SolveNonMini may use the variables HX and TX introduced by Decompose, rather than start from scratch with a non-decomposed X. 

This amounts to the support of binary predicates, single induction parameters, a single minimal form, a single non-minimal form, and non-recursive non-minimal cases. 

An instantiation of the Solve (respectively SolveNonMinj ) predicate-variable computes, in the minimal case (respectively the non-recursive non-minimal case), the value of the other parameter Y from the induction parameter X. Step 5 yields LA r) by using similar methods to those of Steps 6 and 7. 

For instance, in case L is the empty list, its compression C is the empty list as well. This is performed by the atomic formula C = []. There is no non-recursive non-minimal case, and hence no need to instantiate some SolveNonMinj. LA (compress) is thus as follows ... 

This amounts to splitting the non-minimal case into two non-mandatory cases, called the non-recursive non-minimal case and the recursive non-minimal case, respectively. For convenience, we drop the qualifier non-minimal from these two names. Recursion may be useless in the sense that the recursively computed TY are not needed for the computation of Y. Useless recursion wouldn t affect the correctness of a logic algorithm, though. Its elimination is thus rather a matter of algorithm optimization. The following objectives of the strategy ... 

An instantiation of the Decompose predicate-variable deterministically decomposes, in the non-minimal case, the induction parameter, say X, into a vector HX of heads and a vector TX of tails, the tails TXj being smaller than X according to some well-founded relation. These tails are meant for the recursive computation of the tails TYj of the other parameter, say Y. Step 3 yields LA ir) by instantiating the Decompose predicate-variable by means of the Database Method, which here relies on a database of type-specific decomposition formulas. 

Example 5-4 The following logic algorithm for insert(EEfi) has been designed with L as induction parameter. Parameter E is an auxiliary parameter. Note that the non-minimal form gives rise to two cases, one of them without a recursive atom. 

How to detect that recursion is useless in some non-minimal sub-cases Step 4 (Syntactic introduction of the recursive atoms) creates a non-recursive case if at least one example Ej leads to a non-admissible procComp(,,yp atom. Howto invent or re-use appropriate predicates How to implement invented predicates The predicate invention problem is tackled at four points during the synthesis. At Steps 2 and 3, the Database Method re-uses predefined predicates this amounts to using domain knowledge. At Step 6, the Synthesis Method (see Section 14.2.4 below) invents new composition operators. As of now, there is no method yet of re-using common composition operators. At Step 7, the PaP Method synthesizes discriminants that are in terms of predicates other than rfn. How to discover which parameters are auxiliary parameters Due to our restriction to version 3 of the divide-and-conquer schema, auxiliary parameters are not taken into account. See Section 14.2.2 below on how to achieve this. 

A first idea is to use the MSG Method (see Chapter 10). Note that, in both the minimal and the non-recursive case, Y may be totally independent of X. Indeed, Y could be constructed in terms of ... 

---