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,
- instance(S', T', sigma')
--- S' and T' are names of terms S and T, sigma' name
of a substitution \sigma with
Ssigma=T.
- member(C', P')
--- C' and P' are names of
clause and program C and P with C a member of P.
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:
- Uninstantiated variables in the first argument
to an instance constraint can easily lead the programs
of (Hill, Gallagher, 1994; Bowers, Gurr, 1995) into floundering
states, so no answer is provided.
This arise in the maintenance of substitution arguments.
- A subgoal instance(X,Y,Z), for variables
X, Y, Z, will initiate by backtracking
a generation process of all possible names of terms
in the object language until one that meets the
subsequent subgoals is reached.
- The representation of programs as lists
results in infinitely many equivalent
solutions produced for essentially
the same object program by permutation and
duplication of clauses and
by insertion of arbitrary numbers of new
variables. (To see this, consider the solutions
to the Prolog call member(a,L), member(b,L)).
Backtracking on failure is thus condemned to loop.
- Satisfiability for
sets of calls to 'instance' (allowing arbitrary
use of uninstantiated variables) is closely
related to
the undecidable semiunification problem, so
establishing termination result is problematic.
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.