demo(<program>,
<query>)
with
P 
Q Henning Christiansen - henning@ruc.dk
Davide Martinenghi - dm@ruc.dk
Copyright © Davide Martinenghi, Henning Christiansen 1998
All rights reserved.
Permission is granted for copying and printing this document in single copies; further distribution is not allowed.
This document is part of the DemoII system, available at http://www.dat.ruc.dk/software/demo.html.
DemoII is a meta-logic programming system that covers a wide range of automated
reasoning tasks including abduction and induction. These task are specified in terms of declarative
meta-level statements using the proof predicate demo,
which can be specified as follows.
demo(<program>,
<query>) |
iff | <program>
and <query> are names of object
program P and query Q
and there exists a substitution with
P Q |
P and Q refer to an object language, which we call O, of definite clause programs; by a name of an O-phrase (O-program, O-formula, etc.) we understand a unique ground term which identifies it.
DemoII provides an implementation of demo
which is reversible in the sense that it works equally well for executing known
programs as well as for generating new programs that make given goals provable.
Specifications in DemoII may include also syntactic bias and integrity constraints. The system appears as a highly generic environment for experiments with different reasoning methods. Distinct for the DemoII system is the ease with which different methods can be combined, e.g., integrating abduction and induction with default rules.
These properties are obtained using constraint logic techniques implemented with the Constraint Handling Rules library included in SICStus Prolog 3.7, under which the system runs. Among the features are:
fails(<program>,
<query>),
with the meaning that the query named by <query> must fail in the
program named by <program>. It can be used for expressing
counterexamples to predicates and integrity constraints, which are evaluated in a
"lazy" and incremental way.In order to generate useful programs in this way, one often needs to
define a meta-program which determines such class of useful programs. The
DemoII package provides tools for writing such meta-programs, so you can
specify your own predicate, say, useful, and use it in conjunction
with demo, e.g.:
useful(<program>),
demo(<program>,
<facts>)The use of co-routines makes it possible to achieve a reasonable execution speed by interleaving the actions of the two predicates.
The applications which you will find in the Examples directory of this
package demonstrate the approach for tasks such as
The DemoII system provides an extended notation (see chapter 3) with explicit naming operators, which makes programming about the ground representation much more attractive. If you write, say,
\\ p(a, 'X')
this stands for the ground term that represents the
O-atom p(a, X).
As a programmer, you do not need to be aware of
the fact that \\ p(a, 'X') is internally represented as the following structure:
gr(atom,p,[gr(constant,a,[]),gr(variable,'X',[])])
We recommend you to experiment with the example files before you build your own applications (e.g. the annotated example in chapter 4 below).
However, the authors' own experience is, despite the extended syntax and the system's declarative style, that this is a new style of meta-programming that one has to learn.
This user manual shows only the general ideas of the system in order to get acquainted with it; more technical details can be found in the reference manual and the examples files provided with the package.
The documentation included in the system consists of
For problems, questions, complaints, suggestions or perhaps applications of the DemoII
system which would fit into the Examples directory,
do not hesitate to write to henning@ruc.dk (Henning Christiansen).
The ideas behind the DemoII system and references to related work are described in a number of papers:
fails.
For a general introduction to meta-programming in logic we recommend two survey papers:
Currently also available from University of Leeds, School of Computer Studies, as
Research Report number 94.22.
Also available from Uppsala University, Computing Science Department, as
UPMAIL Technical Report No. 80.
and the book
As the DemoII system runs under SICStus Prolog you may occasionally need:
The demoII system can only be used in an enviromnent with SICStus Prolog (version 3.7 or later) installed and the reader is assumed to be familiar with its use.
To install the system, you need to:
A directory called DemoII will then be created inside the directory
from which you unpacked the archive. For instance, if
in a Windows-based environment you used the root directory of drive C, you will have a
directory C:\DemoII containing the following things:
README.txt with general information about the system.Source containing all the system source files.Examples containing some example files.demo.pl - compiled version.demo_i.pl - interpreted version.demo_o.pl - compiled version with occur-check.demo_oi.pl - interpreted version with occur-check.Once the system is installed, it can be
started by running SICStus from the DemoII directory, presumably by typing commands like the following ones:
demo_i,
demo_o, demo_oi).
The system will confirm it has been loaded correctly and the following messages will appear on the screen:
To leave the system and Prolog, write as usual
- | ?- halt.
It is implemented by pre- and post-processors which
The actual syntax is defined by a set of declarations provided by a part of the system that most users of DemoII do not have to care about - and which is not described in the present User Manual. It is possible for a user to extend and modify the syntax. A complete description of the extended syntax is found in the reference manual.
In the following, we describe the basic syntax coming with the DemoII package and which is sufficient for all examples provided with the package.
\\ p(a, 'X') is a way of writing
the ground representation which serves as the name of the object
language atom p(a, X).
Let us analyze what happens with the following query:
-
| ?- Z = \\ p(a, 'X').
Z = \\p(a,'X') ?
yes
It might seem that everything is as usual, but if we insert a call to writeq
in the query, we can see where the difference is.
-
| ?- Z = \\ p(a, 'X'), nl, writeq(Z), nl.
gr(atom,p,[gr(constant,a,[]),gr(variable,'X',[])])
Z = \\p(a,'X') ?
yes
Thus \\ p(a, 'X') is actually read as the ground term
gr(...)
printed out by writeq. The \\
operator is used here as a kind of quotation mechanism.
? operator is used
for putting a meta-variable (i.e. a Prolog variable) inside a term name.
So the expression \\ p(a, ?X) stands for
the name of an object language atom whose predicate is p/2, whose
first argument is the object language constant a and whose second
component is unspecified, indicated by the meta-variable X.
-
| ?- Z = \\ p(a,?X), nl, writeq(Z), nl.
gr(atom,p,[gr(constant,a,[]),_112])
Z = \\p(a,?X) ?
yes
\ for object programs and clauses;\\ for object formulas;\\\ for object terms.Here are a few examples of names of object language phrases written using the extended notation. Notice that programs are written as list of clauses.
\ [ (p('X'):- q('X')), p(a), q(b) ] (a program with a rule and two facts);\ ( p('X'):- q('X') ) (a clause);\\ p(a,'X') (an atom);\\\ f(a,'X') (a structure).There are also forms which make it possible to write object language atoms and structures with unspecified predicate/function symbol and/or argument list; see paragraph 3.4 and the Reference Manual.
Below we will also show how to compose programs with the &
operator and how to make user-defined object program modules.
When using the naming operators, it is sometimes needed to separate different operators with a space. In particular, none of the naming operators can:
= symbol;? operator;(...) expression if it
contains an infix Prolog operator with priority greater than or equal 1000, like, e.g., the comma (,).In all these cases an extra space is needed. Examples:
X= \\f.X= \\\ ?V.X= \\ (a,b).Notice that, in the last case, if one omits the space, the Prolog interpreter will
understand \\ as a functor whose arguments are
a and b, and
not as the naming operator \\.
DemoII generates then a warning message.
[<clause>,
..., <clause>]
& <program>[]Notice: An object program is a set of
clauses and the clauses mentioned in the name of a program are expected to
be different, even in programs composed by & and modules.
The demo predicate and the module mechanism (below) will
check that there are no duplicates and provide an error message when
needed. In general, however, the system does not prevent the user from
writing, say, \[p, p], thus creating a meta-level term which is
not the name of a program.
:- <formula>(<term>,
...,<term>)'_' or a capital lettertrue, <formula>; <formula>= <term>dif(<term>,
<term>)(<term>,
..., <term>)
atomic
and not beginning with '_' or a capital letter'_'Inside a program, a clause of the form
:- trueMeta-variables preceded by ? can replace any sub-phrase,
and its type will be deduced from the context.
If you wish to refer explicitly to the predicate (function) symbol and to the argument list, it is possible to use the following syntax for <atom>s or <structure>s:
^ <argument-list>[<term>,
..., <term>]
[]This is especially useful when used together with meta-variables, e.g.
?F ^ ?AL?P ^ [a,?X]With this notation it is also possible to parameterize predicate and function symbols with an object variable. This is achieved by using an object variable as <name>. Example:
fails(Prog, \\ ('P' ^ ['X',yes], 'P' ^ ['X',no]))
Notice that the extended syntax provides another "expansion facility", a macro mechanism, that provides a simple way to define metalevel predicates defining classes of object programs. This is described in more details in the reference manual and applications of it are found in the example files.
The remaining details of the extended syntax can be found in the reference manual.
In the following we describe a very simple example developed in DemoII which is intended to serve as an introduction for using the system.
The example concerns abduction in a simple propopositional context without integrity constraints and, thus, covers only a small fraction of DemoII's capabilities. To get a better impression of what the system can do, the reader is referred to the other example files.
Examples/wet_grass.pl, which contains a very simple
standard example of abduction, in the usual way:
| ?- ['Examples/wet_grass.pl'].
The file defines, among other things, an object program module in the following way:
-
object_module( garden,
- \[ (grass_is_wet:- rained_last_night),
- (grass_is_wet:- sprinkler_was_on)
- ]).
Details about the
object_module directive are found in chapter 5.
The effect of the module declaration above is that you can use the constant
garden anywhere an object
program is expected, instead of writing
all the clauses each time. I.e., the expression
\gardenis now a program name.
demo to ask queries to the garden program defined
above. The program argument to demo is composed by & from
the garden program and another program which consists of one
unspecified clause, indicated by the meta-variable WHY (notice
the use of the ? operator). See also the comments on
& in paragraph 8.2.
| ?- demo( \(garden & [?WHY]), \\grass_is_wet ).
WHY = \ (rained_last_night:-true) ?
The answer is a value for WHY which is the name of a clause
which makes the conclusion in the demo query provable. The actual answer
we got seems to be a perfect abducible explanation.
Now, let's type ; for alternative answers: alas the
interpreter runs into a loop! There is a good reason for this which we will discuss in chapter 8.
However, the main intuitive reason to these troubles is that our query
to demo was not stated carefully enough.
The query asked for any kind of clause which makes grass_is_wet
hold. So we were actually very lucky that the internal control inside demo
actually produced a sensible first answer!
Usually abduction is understood as the task of finding facts of a certain "primitive" kind.
To this end, our example file Examples/wet_grass.pl defines
a meta-predicate abducible(_) as follows:
:- block abducible(-).
abducible( \ (rained_last_night:- true) ).
abducible( \ (sprinkler_was_on:- true) ).
abducible( \ (full_moon:- true) ).
abducible( \ (sun_shines:- true) ).
abducible( \ (dog_on_lawn:- true) ).
The block declaration causes any call abducible(X)
to delay until some other event (e.g., an internal action of demo) assigns a value
to X. (Block declarations are described in the
SICStus Prolog User's Manual).
Consider, now, the following query:
| ?- abducible(WHY), demo( \(garden & [?WHY]), \\grass_is_wet ).
WHY = \ (rained_last_night:-true) ? ;
WHY = \ (sprinkler_was_on:-true) ? ;
no
This looks more like abduction. The call abducible(WHY) delays
a condition on WHY, which wakes up when demo
actually begins to involve the "clause" WHY in a proof. In this
tiny example, the block declaration does not actually make much difference
but when things become more complicated it can be essential to have such
additional conditions delay as long as possible.
In paragraph 6.2 and in chapter 8
we discuss more aspects of the use of the blocking mechanism.
This ends the first little annotated example intended as an introduction
to the basic functionality of the DemoII system. Other less trivial examples are found in the
Examples directory.
An object program module is defined by a directive as follows:
object_module(<identifier>,
<program-name>)
<identifier> is, as already stated, a Prolog atom beginning
with a small letter; <program-name>
is any term which can be accepted as the name of an object program that does not contain meta-variables.
Here the extended syntax provided by the \ naming operator is useful.
Example:
object_module( pq_program,
\[ (p('X'):- q('X')),
p(a),
p(b)
]).
The execution of this directive makes pq_program available
as a program module which can be used as (part of) a program name, e.g.:
| ?- demo(\pq_program, ...).
In the translation from extended syntax to Prolog structures, a name
like \pq_program is replaced by a copy of the original
source text (unlike the previous version of the system, there is no preprocessing of clauses).
The ground representation of a module is stored as an asserted fact
object_module_source/2.
You can also use the & syntax in the definition
of a module, e.g.:
object_module( extended_pq_program,
\ ( pq_program & [(q('X'):- r('X')), r(c)] )).
In this way you can build a hierarchy of object language programs which are extensions of each others.
Restrictions:\ (p(a):-true).&.demo predicate is defined by means of constraints. These constraints
are, among other things, a convenient tool for dealing with user-defined meta-predicates to be used together
with demo. For some applications it may be necessary to write another
demo predicate which uses, say, another search strategy; the sample file
Examples/linear_drinks.pl shows an alternative demo predicate which
can produce programs under linear-logic-like conditions.
In this chapter we explain which constraints are available and what one may need to know about their execution behavior.
The kinds of constraints DemoII is working with are thoroughly described in the reference manual; in the following paragraphs we introduce type and instance constraints, constraints for negation and some auxiliaries. The other constraints are not described here, as they ought to be used only by DemoII internal control.
As a general introduction to constraint techniques in logic programming, we advocate the following:
There is one type constraint for every type defined in the object language:
program_clause_formula_atom_constraint_term_constant_structure_variable_Each constraint is satisfied whenever its argument is the name of an object phrase of the indicated type. Thus, for example, the following constraints are all satisfied:
program_( \[] )atom_( \\ p(a) )constraint_( \\ ('X' = b) )variable_( \\\'X' )formula_( \\ (q1;q2) )Notice that each constraint name ends with an underscore in order to have a consistent way to distinguish them from a few Prolog built-ins.
Instance constraints are of the form
instance_(<Object>1,
<Object>2)
An instance constraint is satisfied whenever <Object>1 and <Object>2 are names of object language phrases O1 and O2 with O2 being an instance of O1.
Instance constraints are essential for defining a meta-interpreter
such as demo, but users who stick to the delivered demo predicate will
probably never need to use instance constraints.
In order to treat conditions about non-provability at the object level, we implemented a constraint specified as follows:
fails(<program>,
<query>)
iff <program> and <query>
are names of object program P and query Q and there is no substitution
for which
P Q
In the actual implementation, a goal like
fails(P, \\p(a))
will delay until P gets instantiated. This resembles an incrementally
executing integrity constraint that delays subcomputations on
remaining meta-variables and
wakes up when these in turn are instantiated:
\\p(a) above).fails works internally with some other constraints, described in
the reference manual. Such constraints can appear in the answer if the computation
is delayed.
DemoII includes a few other constraints of which
ground_ is probably the only one
that is relevant when developing new applications
in DemoII. We mention them here because they
can appear as part of answers produced by the system.
ground_(<term>),
which states the argument must be the name of a ground
object language phrase.member_(<clause>,
<program>), which states membership
of clause <clause> in program <program>.
This constraint is implemented in plain Prolog, therefore it does not delay.
It distributes correctly over object program modules and the concatenation operator
&.no_duplicates_(<program>),
which states that the same clause cannot appear more than once in <program>.disjoint_(<program>1,
<program>2),
which states that <program>1 and
<program>2 have no clause in common.not_member_(<clause>,
<program>), which states that
<clause> cannot be a member of
<program>.program_(P)
P or another constraint call) which might possibly
violate program_(P). The implementation of this is
mainly based on the Constraint Handling
Rules library (CHR) included in the SICStus Prolog package (in a few cases we used SICStus
block declarations instead).
Ideally, the user should not need to be aware of when or how constraints
actually execute. However, user-defined meta-predicates may need to delay,
thus functioning as a sort of constraints that interact
with those set up by the demo predicate.
Whenever a constraint "decides" to assign a value to a
variable X, the event also triggers user-defined predicates.
Or, the other way around; a simple unification made by user code may
trigger a large collection of accumulated system constraints.
A precise and formal model for execution of constraints is given in the paper "Automated reasoning with a constraint-based metainterpreter" referenced in the introduction. Here we present the basic rules in an informal way, which we believe is sufficient for those who want to develop their own meta-predicates:
program_(P)) delay as long as
possible.Rule (a) indicates that even a constraint such as atom_(A) does
not assign a value to A. We found that this
principle works better together with delayed user predicates.
According to rule (b), it happens for example that:
term_(X), constant_(X) reduces
to constant_(X).formula_(X), variable_(X) fails.An example of application of rule (c) is the following:
| ?- clause_(\ (?A:- ?B)).
atom_(A),
formula_(B) ?
As an advice, we can give a rule of thumb saying that user-defined
meta-predicates to be used in conjunction with demo should be as
"lazy" as possible, i.e., have as many (sensible) block
declarations as possible. The demo predicate will accumulate roughly one
type constraint for each uninstantiated meta-variable. When or if such
a variable is assigned a value, the constraint evaluates as a test. Type
constraints do not assign values to variables; hence, they do not trigger
delayed user predicates. Actually, this is true except for a few cases discussed in the
reference manual. As a programmer or DemoII user, you seldom have to
worry about type constraints.
Warnings:
In the normal execution mode, there is no occur check involved in solving instance constraints; see chapter 2 for how to enable occur check. In the examples provided with the the DemoII package this does not make a difference, but in another (yet undocumented) experiment trying to generate polymorphic type declarations from program text, the occur check appears to be essential.
There is no facility in the DemoII system which prevents the user from writing additional code which delays calls of his or her own predicates which are unsatisfiable in conjunction with the accumulated system constraints.
X appearing in an argument to
demo. When the demo call has succeded, the answer printed out by the system
often consists of a collection of more or less comprehensible constraints
about X. Alternatively, X
may be assigned a structure with a number
of new meta-variables on which quite many constraints can be expected.
To provide more compact answers we have implemented a predicate
close_constraints(<AnyPhrase>)
which localizes the uninstantiated meta-variables in the argument
<AnyPhrase> and tries to assign values to them which will satisfy
the accumulated constraints. The sample file Examples/still_life.pl
shows how it works.
The close_constraints predicate is a purely heuristic
construction which succeeds only once giving a suggestion for a
prototypical, concrete answer contained in the constraints.
It applies an adapted (an not yet documented)
least-general-generalization method, and
includes
strategies for reusing existing symbols and inventing new ones when
necessary.
Sometimes the set of accumulated constraints and delayed user
predicates is unsatisfiable. In this case the predicate issues a warning
and fails, hoping for demo and the user predicates to come up with a
better set of constraints.
The following example shows a problem that can arise with close_constraints.
Consider the query:
demo( \ (... ?X
...), ...),close_constraints(X),condition(X).It may be the case that this query fails because close_constraints
instantiates the solution provided by demo in a way different from what
you expected. This query may fail even if demo has produced a set of
constraints that contain a grounded solution satisfied
by condition(X). The correct action is likely to reprogram
condition(X)
as a co-routine that interleaves with the actions of demo.
The close_constraints predicate is especially useful
in the early experimental phases in the development of a new application
of demo. The first version of a new meta-predicate to support demo
is typically
not precise enough: it can be quite a challenge to formalize what it means
for an object program to be a good object program in a given context.
So in your first experimental execution of
good(P), demo(P, ...),P is probably very
little and the amount of delayed calls quite difficult to understand. Try instead
good(P), demo(P, ...), close_constraints(P)good predicate needs revision.
The more you revise the good predicate, the less
meta-variables are left for close_constraints and, in the final
version, close_constraints can be dropped or used only for trivial
tasks such as closing open program tails.
We have found that the warning issued by close_constraints
on failure is an effective means for recognition of programming errors
in user predicates (but, alas, not for localizing the erroneous point!).
We cannot present a methodological textbook on meta-programming using the DemoII system; here we discuss a few points which may be of importance for those who want to develop new applications.
demo predicate works top-down,
trying (and inventing, if necessary) clauses in the order they appear in
the program and executing goals from left to right (in other words, in
the same manner as a traditional Prolog system). As in Prolog, this may
result in loops and other unwanted behavior unless the programmer has
taken proper precautions. And when demo is applied for generating
programs, there are of course even more pitfalls. Without any additional
meta-programs supplied for the particular application, demo will easily
get into trouble.
The following basic version of the demo predicate illustrates
this control pattern.
demo(P, Q) :-
program_(P),
no_duplicates_(P),
instance_(Q, Q1),
demo1(P, Q1).
demo1(_, \\true).
demo1(P, A):-
member_( C, P),
instance_( C, \ (?A :- ?B1)),
demo1(P, B1).
demo1(_, \\ (?T1 = ?T2)) :- T1 = T2.
demo1(_, \\ dif(?T1, ?T2)) :- dif(T1, T2).
demo1(P, \\ (? A, ?B)) :- demo1(P, A), demo1(P, B).
demo1(P, \\ (? A; ?B)) :- demo1(P, A); demo1(P, B).
We will illustrate the potential problems with the following
query to demo for object programs in which the object query
p is true.
| ?- demo(X, \\p).
The first answer is as follows (note that the extended syntax is used when the answer is printed out):
X = \[(p:-true)|?_A],
user:not_member_(\ (p:-true),_A),
user:no_duplicates_(_A),
program_(_A) ?
This says that X is a program having a fact saying
"p holds" and some internal
constraints expressing that the tail of X must be a program.
When asking for a second solution, we run into a loop which is very easy to
explain. Asked for an alternative answer, demo will try to redo its last
choice, which was to expand the tail of the novel clause to
true. Alternatively, it tries to expand it to an atom, and
this atom must unify with the head of a clause in the program; as expected
it tries the first clause (whose head is p), so the object
clause p:- p is created.
However, the observed behavior only reflects the quality of the query.
It is difficult to imagine an application where one is interested in just
a program which makes p provable: there will be
many weird ones, also which include the clause p:- p. In
most cases there will be some inherent criteria, formalized, say, as a
meta-predicate good(_), which will exclude this. This was the case
of the abduction example in file Examples/wet_grass.pl
which we discussed in chapter 4 above.
This means that no duplicates are allowed at the representation level.
In practice, this makes the demo predicate less prone to loops. Whenever
demo needs to expand (using member_)
a variable in the
position of a program tail into a structure with one new clause and yet a
new tail, it will not try to expand this new tail again on backtracking.
Consider an example query,
conditions(P), demo( P, \\p)
and assume that demo
expands P to \ [?C1 | ?P1]
and for some reason (e.g., due to conditions(P)) this fails,
i.e. there is no such clause which can make p provable. Without
the mentioned mechanism, demo might now try to expand
P1 into
\ [?C2 | ?P2], which is likely also to fail; and so on.
With demo as we have implemented it, the
whole demo call fails after
the first failed expansion.
This principle, expand-tail-only-once-on-failure, extends to
programs composed by the & operator. We illustrate this
by the following query:
- red(Pr), green(Pg), blue(Pb),
- demo( \ (?Pr & ?Pg & ?Pb), \\p).
The predicates red,
green and blue
define different kinds of clauses which are relevant with respect to the
given problem domain. Now, if the call to demo (or perhaps
some deeply nested, recursive call) fails on expanding the tail (of a tail of ...) of
Pr (i.e., the
red meta-condition fails), then expansion of
Pg is tried, and if this also fails (i.e.,
green fails), expansion of Pb
is tried (and then tested with blue).
As the example indicates this makes it easier to structure meta-predicates in a more orthogonal way.
This document was last modified on Monday, December 21, 1998