Logic algorithm design

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. 

Example 5-12 The following logic algorithm for split L,F,S) has been designed by a totally different method, namely introduction of an additional parameter, plus logic algorithm design by structural induction for the new problem. 

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. 

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. 

Stage B Design of a logic algorithm (and possibly its transformation) ... 

This chapter is organized as follows. In Section 4.1, we discuss the elaboration of specifications. Section 4.2 is about the design of logic algorithms, whereas Section 4.3 is about their transformation. Section 4.4 describes the derivation of logic programs, whereas Section 4,5 describes their transformation. 

Let s explain these four steps one by one. Note that this method is proven to yield correct logic algorithms. A tool, called Logist, is being developed for the Folon environment to assist a designer in following these steps [Deville and Bumay 89]. 

Here follow, in alphabetical order on the predicates, some logic algorithms for some problems posed in Section 1.5. We do not explain their design processes, but give... 

Example 5-1 The following logic algorithm for delOddElems L,R) has been designed with L as induction parameter. A design with R as induction parameter would yield a quite similar logic algorithm. 

The following other logic algorithm for JirstN N,LJi) has been designed with N as induction parameter. Note the interesting variable sharing between HE and HR their value is invented , but common. Also note the relevant presence of a true atom. 

The following other logic algorithm for insert(E,LJt) has been designed with R as induction parameter. Note that the non-minimal form gives rise to two cases, one of them without a recursive atom. 

This last dimension is actually also applicable for classifying relations, as no design choice affects into which category the resulting logic algorithms fall. 

How to discover which parameters are aiailiary parameters Problems such as efface 3, insert 3, member , partition , and plateau 3 have auxiliary parameters unless this is stated somewhere, considerable design effort may go into detecting this. The logic algorithms listed above for these problems actually are versions for which the detection was not done. 

When a logic algorithm is designed by structural induction on some parameter (as in Chapter 4), then predicate r n can be interpreted in any Herbrand model of LA(r). 

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). 

Since we only consider logic algorithms that are designed by structural induction, correctness reduces, by Corollary 7-1, to = UC r), Moreover, partial correctness is achieved iff UCir) (that is, iff the atoms computed by LA r) are correct), and completeness is achieved iff LA r) (that is, iff all the correct atoms are computed by LA r)). These criteria are in the sequel called the intuitive criteria. 

It is interesting to decompose a synthesis process into a series of steps, each designing an intermediate logic algorithm. Indeed ... 

---