On solving member and instance constraints

Henning Christiansen
Department of Computer Science
Roskilde University, P.O.Box 260, DK-4000 Roskilde, Denmark

In this paper, we consider the particular problems that arise for the primitive operations in the demo predicate when used "backwards" as a tool for generating programs. The binary proof predicate demo is specified as follows.
   demo(P',Q')  iff  P' and Q' are names of program and query, P and Q,
                        such that there exists substitution sigma with

                               P |-  Q sigma
A metavariable, say X, in P' will thus stand for a piece of program text and a logically satisfactory implementation (such as our constraint-based version) will produce program fragments which make Q provable. By means of additional side-conditions, demo can be instructed to produce useful programs, as illustrated by the following pattern.

useful(X), demo(... X ..., ...)

The 'useful' predicate may specify syntactic requirements to the program fragments sought, perhaps extended with additional calls to demo to express integrity constraints. As demonstrated elsewhere (Christiansen, 1994a, 1994b, 1995, 1996), this principle can be used for defining quite concisely a wide range of reasoning tasks such as abduction, induction, diagnosis, default reasoning, etc. The present paper concerns the methods that are necessary in order to achieve an implementation of demo providing this functionality. We use the structure of the so-called "instance-demo" predicate which has been studied by several other authors recently (Hill, Gallagher, 1994; Bowers, Gurr, 1995). It replicates SLD-resolution using the following primitive operations,

The instance conditions can express object level unification in an efficient way which operationally is very similar to the use of a nonground representation in the Vanilla interpreter. In the referenced studies, programs are represented as list structures with 'member' being the usual list operation; 'instance' is implemented in a similar straightforward way in Prolog with substitutions represented as lists of variable-value pairs. While sufficient when the program argument to demo is fully given (i.e., ground), such a naive implementation implies severe problems in the general case we have in mind: It is obvious to suggest constraint techniques applied for the first two problems: When not enough information is present in the arguments to `instance', the call delays and some additional machinery should be invoked in order to check satisfiability. To solve the third problem, we consider programs as sets of clauses rather than list structures, and viewing also 'member' as a constraint makes it possible to provide a precise control over which solutions that are produced. With respect to the last problem, we have identified an invariant property called safeness for constraint sets produced by the demo predicate and under which our constraint solver is guaranteed to terminate. Roughly, safeness means that no variable can occur in a first as well as in a second argument to 'instance' constraints. The constraint solver has been mapped into an executable program in Sicstus Prolog (SICS, 1995) based on a notion of attributed variables, originally suggested by (Holzbaur, 1990, 1992). In this way, the constraints appear as predicates in Prolog with very little addition overhead. When demo is used for specific tasks as outlined above, the defining side-conditions depicted as a `useful' predicate above, should be instructed to behave in a ``lazy'' way by means of delay mechanisms in order to have preserve the optimal execution behaviour.

Metaprogramming and Metareasoning in Logic (META96), Tech. Repr. 127, Uppsala University, Compoure Science Dept., 1996, pp. 13-25.
See dvi, postscript.