Finite logic algorithm

The Proofs-as-Programs Method is deterministic because the results of all successful derivations are collected before computing 21 therefrom. The method is thus independent of any ordering of disjuncts within LA r), or of properties within P(r). The method may fail, as conveyed by Definition 9-5. However, nothing can be said about the synthesized logic algorithms in terms of determinism or finiteness, because nothing is known about the properties. 

Let s close in now on the MSG Method. Intuitively, its objective is to infer a logic algorithm of a predicate r n, given a finite set of examples of rhi The method should be applicable if the intended relation (from which the examples are extracted) can be expressed by a logic algorithm that is defined solely in terms of the =/2 primitive (hence is non-recursive, among others). This is feasible iff, in the intended relation, some parameters are somehow syntactically constructed from some other parameters. 

This algorithm is non-deterministic, finite, and never fails. Moreover, the synthesized logic algorithm is non-deterministic in general, and finite, but may fail. For instance, considering Example 10-2, the atom pcCompress eXe,2]X) is covered by both disjuncts of the synthesized logic algorithm, namely via the answer substitutions X/[e,3] and X/[c,l,, 2]. ... 

Within a restricted setting, the MSG Method infers, from a finite set of general examples, a non-recursive logic algorithm that is defined in terms of the =/2 primitive only, and that is correct wrt a natural extension of the given examples. The underlying algorithm is non-deterministic. 

So why not immediately use the Synthesis Method The reason is that both methods tackle different classes of problems. The MSG Method and the Synthesis Method are a joint answer to the same overall problem how to infer, from a finite set of general examples of an unknown relation that is however known to feature a given dataflow pattern between its parameters, a logic algorithm that is correct wrt a natural extension of the given examples. The MSG Method is the base case of the answer, because it doesn t look for recursion, and the Synthesis Method is the structure case of the answer, because it does look for recursion. 

Finally, the methods of tasks A, C, D are non-deterministic, but finite. This means that choice-points are created there, and that the made selections may be reconsidered later, either because synthesis fails, or because synthesis succeeds and the specifier wants more algorithms. Only Task A could possibly fail, namely if there is no parameter of an inductive type. Do not mix up non-deterministic synthesis and a non-deterministic synthesized algorithm. The latter would feature either mutually nonexclusive cases or predicates that are non-deterministic. The logic algorithm synthesized at Step 2 is deterministic, because the two cases are mutually exclusive by construction, and because the introduced predicates are deterministic. 

Second, note that the methods of both tasks are non-deterministic, finite, and can never fail. However, the introduced predicates are deterministic in the decomposition mode. This implies that the witnesses hxj and txj are unique. The logic algorithm synthesized at Step 3 is thus deterministic. 

The methods of Tasks M and Q are non-deterministic, finite, and never fail, because of the usage of the ground case of the MSG Method. Moreover, the synthesized instances are non-deterministic and finite, for the same reason. The logic algorithm... 

---