Well-founded relation

The second step is the selection of a well-founded relation (wfr) over the type of the induction parameter. Two heuristics have been identified ... 

Example 4-6 For the compressll problem, the intrinsic heuristic leads towards selecting is the tail of as well-founded relation over the type of L. Weaker relations such as has less elements than or is a suffix of are also suitable, but it is best to start with strong relations, and relax them as needed. 

Select a well-founded relation that reflects the definition of the type of some other parameter, or that reflects the structure of the specified relation. 

Example 4-7 For the compressll problem, the extrinsic heuristic leads towards selecting has one plateau less than as well-founded relation over the type of L, because it reflects the structure of the C parameter. But we retain the well-founded relation suggested by the Intrinsic Heuristic for the remainder of this section, and come back to this decision in Section 5.2.1. 

An interesting exercise is to compare logic algorithms designed by induction on different parameters, or using different well-founded relations. Considering the heuristics above, it is no surprise that, for a binary predicate r having X and Y as parameters, LA r-int-X) and LA r-ext-Y) are structurally similar, or that LA r-int-Y) and LA r-ext-X) are structurally similar. 

Let s first reconsider Step 2 (Selection of a Well-Founded Relation), and follow the Extrinsic Heuristic when selecting a well-founded relation over the type of the induction parameter L. This means that we want to decompose L into something smaller in a way reflecting the structure of parameter C. Every element of C represents a summary of a plateau of L, so the idea is to decompose L by extracting its first maximal plateau as head of L, and the corresponding suffix as tail of L. This decomposition is non-trivial, but considerably facilitates the rest of the construction. Step 3 is unaffected by this decision, and after Step 4, the result is ... 

An intrinsic decomposition reflects a well-founded relation selected via the Intrinsic Heuristic, and an extrinsic or logarithmic decomposition reflects a well-founded relation selected via the Extrinsic Heuristic (see Chapter 4). Sample classifications are given below. 

In the following, we thus only consider recursive logic algorithms where some well-founded relation can be defined between the recursive literals and the head. We thus have to enforce that a synthesis mechanism doesn t design non-terminating recursion (for ground queries). 

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. 

The instance of X, that is the induction parameter, must be of an inductive type. Indeed, otherwise, its decomposition into tails TX that are each smaller thanX according to some well-founded relation would be impossible. 

The decomposition of X must yield tails 7X, that are each smaller than X according to some well-founded relation < . This means that the formula ... 

Failure is not always detectable, except in specific settings. For instance, no infinite derivation can occur if all primitive predicates have finite proofs for all directionalities, and if there is a well-founded relation between the recursive atoms of a property and the head of that property. 

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. 

An intrinsic decomposition reflects a well-founded relation selected via the Intrinsic Heuristic (Heuristic 4-3), and an extrinsic or logarithmic decomposition reflects a well-founded relation selected via the Extrinsic Heuristic (Heuristic 4-4). The selection of a strategy is a high-level decision that may significantly affect the complexity of the resulting algorithm (but probably not its existence). A reasonable implementation of this synthesis mechanism would accept a preference hint from the specifier. 

The databases used by the method of Task F guarantee that each instance reflects decomposition according to some well-founded relation. ... 

How to discover compound induction parameters Due to our restriction to version 3 of the divide-and-conquer schema. Task A only considers simple induction parameters. Meeting this challenge is thus considered future research. According to what well-founded relation to decompose the induction parameter Step 3 (Synthesis of Decompose) does this non-deterministically by considering all predefined decomposition operators (which each reflect some well-founded relation) of a typed database, and possibly by listening to the specifier s hints. 

---