fails(<program>,
<query>)
iff <program> and <query>
are names of program P and, respectively, query Q such that there is no substitution
for which
-
P
Q
Davide Martinenghi
Roskilde University Center,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.
Contents
In this document we describe the features of the new Demo system (here referred to as DemoII), which has been developed 1997-1998 by Henning Christiansen and Davide Martinenghi with first public release on WWW, December 1998. The previous version of the system (DemoI), still available on the WWW, was written in SICStus Prolog version 2 around 1994 and was adapted for version 3 in 1996.
A user manual is also available. The typographical conventions used in the DemoII manuals are defined here.
There were several good reasons to rewrite the system from scratch, namely:
freeze and frozen,
which is not very elegant and also implies a few bugs).We expect the reader of this document to have read the relevant research paper about the Demo approach:
This document is organized in three main chapters (plus the introduction, which is this chapter).
In the second chapter we describe the extended syntax, which looks very much the same way as in DemoI, at least from a user's point of view.
We keep the three quotation operators:
\ for programs and clauses;\\ for formulas (including atoms and dif and =
constraints);\\\ for terms.?.
In the new system, the user can simply extend the syntax by adding new operators, types
and subtypes. For object programs, the notion of program modules and the &
operator are kept. However, in DemoII there is no preprocessing of clauses in an object
program module; so, if a module, say m, is defined, the syntax reader
replaces its occurrences by the source code associated to m.
The third chapter illustrates the constraint solver, which was written with the CHR library, introduced in SICStus Prolog version 3.7. The behavior of the rules is based on the type and operator definitions of the extended syntax (that can be modified by the user). Adding new constraint solving rules is also possible, although not recommended.
The fourth chapter deals with negation. In order to treat conditions about non-provability at the object level, we implemented a predicate specified as follows:
fails(<program>,
<query>)
iff <program> and <query>
are names of program P and, respectively, query Q such that 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).The extended syntax is in use when the system reads and writes terms. The syntax is defined by means of declarations of types (each with a quotation operator), subtypes and operators. In this document, we describe the form and meaning of these declarations. Declarations are intended to be used in the code that defines DemoII (hence specified by its developers) as well as in applications written by other users. The syntax is inspired by the one used in DemoI, but differs in a few ways, most notably in that object variables now have to be written using single quotes.
Internally, DemoII works with a detailed ground representation of phrases of the (current) object language. This is necessary in order to implement the sort of constraints that are needed in DemoII. On the other hand, this notation would be very tiresome for programmers as well as for "normal users", and therefore a "syntactic sugar" is provided.
This so-called extended syntax is used:
The extended syntax used in DemoI has been carried over into DemoII with some minor adjustments:
2.2 A "generic representation" of object language phrases
In DemoI, a large number of different functors are used for representing different operators of the object language. In order to make the coding of DemoII easier, a generic representation is chosen instead. Another significant change is that the arity of predicate and function symbols does not appear explicitly in DemoII, as it was the case in the previous system.
A phrase of the object language is represented by the general meta-level (Prolog) term:
where gr
stands for ground representation. For instance, the object
language term f(a, X) is represented by
the meta-level term
gr(structure, f, [gr(constant,a,[]), gr(variable,'X', [])])
which can be written more conveniently, using the extended syntax, as
\\\ f(a,'X').
Notice that the <type> in the example is structure and not term,
as we assume that the most specific type is always used in the ground representation (and structure is a subtype of term). See section
2.3.3 below for more details.
This notation takes up to roughly three times as much space as a DemoI-like representation, but it makes it much easier to write a generic handler for the extended syntax and a constraint solver.
Object substitutions, that are used only "internally" in the system, are
represented by a list of variable/substitution pairs, separated by a -> symbol. Example:
[ ('X'-> gr(constant,a,[])), (('Y'->
gr(structure,f,[...])) | _ ]
When talking about a pseudo-substitution we refer to
a term of this form, but where the subterms to the right of ->
are not necessarily a correct name of an object language term.
Terms of the form gr(T,S,L) will normally
have T and S instantiated, but there are cases where this does
not hold, for instance if we want to parameterize over <symbol>,
e.g., if we want to express properties that hold for all predicates (see paragraph
2.5).
2.2.1 Manipulating the extended syntax
The extended syntax can be activated and disactivated by manipulating some "switches" available in the system:
ahead (default: on)
controls the (forth-)translation from anything into the ground representation;back (default: on)
controls the (back-)translation from ground representation into the readable extended syntax;garbage (default: off)
if activated, possibly masks some of the output coming from a fails
predicate (see chapter 4), which is identified to be the result of a garbage collection
(a technique not described in this manual).A switch is (dis)activated as follows:
switch(<switch name>=<flag>)
where <switch name> is one of the switches mentioned above and
<flag> is either on (activated)
or off (disactivated).
Example:
switch(back=off).
X= \\p(a).
X = gr(atom,p,[gr(constant,a,[])])
2.3.1 General notions concerned with types
A type defined by the user is identified by a Prolog constant. Types
are ordered in a hierarchy so that one type can be a subtype of another. For example, constant is a subtype of term.
In addition we have types in the system which are used for argument lists and similar things. The set of all types is defined by the following grammar:
type or subtype declaration
(see below)*(<simple-type>)+(<simple-type>)[<simple-type>1
, ...,
<simple-type>n], n>=0Each type stands for a set of terms in the meta-language, and for each simple type there
is a constraint, satisfied for any such term. So, for example, we have a constraint
atom_/1
satisfied for those terms that name an object language atom. The name of all such
constraints is the name of the type followed by an underscore and it is derived from the
type declaration.
The star, plus and list types stand for sets of Prolog list structures of terms of the indicated types. Examples:
[variable, atom] indicates a list with two
elements, the first being of type variable, the
second of type atom;*(term) indicates a list of 0 or more
elements, each of type term;+(term) indicates a list of 1 or more
elements, each of type term.2.3.2 Limitations due to the constraint solver
We made some assumptions on the types in order to simplify the design of the constraint solver.
In particular, there are three categories of types:
variable, which is a subtype of
term;term;The reason for distinguishing these groups is that the implementation of instance constraints needs to have a different rule for each of them. The user can therefore add a new type belonging to the second or the third category, and the instance constraints will automatically work.
Furthermore, the implementation of membership
constraints assumes that the types clause
and program are defined. If new user-defined
types are added, the user is responsible for extending the relevant constraints by means
of new constraint solving rules, if those new types are to be considered as programs or
clauses.
We define the subtype relation precisely as follows.
+(S) is a subtype of *(T)+(S) is a subtype of +(T)*(S) is a subtype of *(T)[S1, ...,Sn], with n>=0, is a subtype of
*(T)[S1,
...,Sn], with n>=1, is a subtype of
+(T)[S1,
...,Sn] is a subtype of [T1,
...,Tn] if Si is
a subtype of Ti, for i = 1..n.We say that S is a proper subtype of T if S is a subtype of T with S different from T.
Property. For any term t of type S, if S is subtype of some type T, then t is of type T.
Definition. The least common type of two simple types T1 and T2, denoted lct(T1, T2), is:
A predicate lct/3 has been implemented whose
third argument evaluates to the lct of the first two arguments, if it is defined;
otherwise the predicate fails.
Types are used for classifying meta-level terms according the sort of object language phrase they name. The given set of defined simple types and operators induce a type relation for meta-level terms defined in the following way (the precise syntax for type, subtypes, and operators is defined below):
*
...* <simple-type>n
--> <simple-type>0gr(<simple-type>0,
<op>, [T1,
..., Tn])[T1,
..., Tn]
has type *(<simple-type>).[T1,
..., Tn]
has type +(<simple-type>).[T1,
..., Tn]
has type [<simple-type>1,
..., <simple-type>n]2.4 Declarations of types and operators
A user/developer can declare:
The declarations will affect the extended syntax (i.e., the Prolog reader) as well as type and instance constraints.
All the definitions of the "basic" types used in DemoII are found in file type_definitions.pl; the user can add new definitions
in a new file.
The precedence among declarations (in case of ambiguity) complies with the following rules:
stands for
option (see below) are ignored.In this way a new operator or type (but not subtype) declaration added by the user may
serve as an exception to the previous declarations for that type when the system reads
input. If, for example, the user wants to add a new operator that applies to atoms inside
clauses, e.g. not, he can do so in his source
file, and the object phrase not p(a) will be
recognized as an occurrence of this operator and not as an atom with predicate not with p(a) understood as a term!
Notice that this order of precedence is the opposite of the precedence among the clauses of a Prolog program.
All declarations are "global" in the sense that they do not respect SICStus Prolog's scope rules (given by modules). The precedence described above depends on the order in which files are consulted and reconsulted, so it may be necessary to start up DemoII from scratch when files are edited.
In this paragraph we show how type definitions can be made and what
mechanisms are involved in such an
operation. The reader is referred to the source file type_definitions.pl for
precise information on the basic types defined in the current version of
DemoII.
A type definition is an expression of the following form:
type <type> quoted by <quotator>.<type> is a
Prolog atom and <quotator>
is the quotation operator used to write object expressions of type
<type>. After the type
definition, <quotator>
will be automatically defined as a Prolog operator with precedence 3 and type fx with a directive:
op(3, fx, <quotator>)Subtypes can be defined with a declaration like the following one:
subtype <subtype> < <type>.<subtype> is a Prolog atom and <type> is intended as its supertype. <type> must have already been declared as a type or a subtype. The quotation operator of a subtype is inherited from the supertype.
For each type (and subtype) a constraint is defined whose name is the name of the type (subtype) followed by an underscore.
Example:
type term quoted by (\\\).
A constraint term_/1 is created and the
quotation operator for the type term which can
be used in the extended syntax is \\\. Notice
that in this case we needed to enclose the operator between parenthesis because the \ character is normally used to write escape
sequences.
As mentioned above, the order of subtype declarations has no impact on the extended syntax, so that, after the definition of the following subtypes
subtype constant < term.
subtype variable < term.
subtype structure < term.
the system can decide whether an expression quoted by
\\\ is a term, a constant, a variable
or a structure depending solely on the order of the operator declarations.
It is, of course, also possible to define subtypes of subtypes:
subtype funny_constant < constant.
According to the definition of subtype, funny_constant
is a subtype of constant as well as of term.
The same quotation operator can be used for different types:
type clause quoted by (\).
type program quoted by (\).
According to our precedence principles, the expression \a will be understood as a program or as a clause only
depending on the order of the operator declarations. When no operators are defined, it is
not possible to denote a phrase belonging to a declared type.
Type and subtype declarations are required to be hierarchical in the following sense:
Definition. For any defined type (or subtype) T, there is assumed an infinite set of constants c(T, 1), c(T, 2), ... of type T. There is no way to denote these constants in the meta-language.
This implies a semantics for type constraints as well as dif
constraints (the latter in object- as well as meta-language) which is sensible to implement.
The mentioned constant symbols are completely fictitious and do not appear in the
implementation.
The definition implies the following properties:
dif calls, with the arguments being
non-identical or non-distinguishable (as defined in the theoretical
paper Christiansen, H., Automated reasoning with a constraint-based metainterpreter,
Journal of Logic Programming, 1998. Vol 37(1-3) Oct-Dec 98, pp. 213-253)
is satisfiable.2.4.3 Definitions of operators
Operator definitions are of the following form:
operator <op>: <in_types>
--> <out_type>
[, { <code>
}] [stands
for <output>].Notice that the arrow in the type signature is --> and not ->, since the latter is already declared in Prolog
with a precedence that does not fit with this usage.
<op> can indicate either an ordinary operator or a special operator. In the first case, <op> is a Prolog atom representing the operator. In the second case, <op> is an expression of the following form:
any-<special_category>
[^<primary_symbol>
[^<argument_list>]
]<in_types> indicates the types of the arguments of the operator. <out_type> is the type of the operator. <out_type> can only be a simple type, whereas <in_types> can be:
Product-types are shorthands for writing list-types. A product-type can be:
[T];(T1 * ...* Tn), which corresponds to the list-type [T1,
...,Tn];[].The operator definition is valid if and only if the types mentioned in <in_types> and <out_type> are existing types.
<code> is optional Prolog code (to be enclosed between curly brackets) executed when the rule applies. Notice that a comma is used when this field is present.
<output> is an optional expression preceded
by stands for used to override the normal
translation with a user-defined one.
Comments on the use of <code> and <output>:
Suppose types formula and constraint
are defined:
type formula quoted by (\\).subtype constraint < formula.operator = : term * term --> constraint.
If the user does not explicitly define with a Prolog op
directive the associativity of the operator, the Prolog default will be assumed. In this
particular case, = is therefore an infix
operator.
Together with the two type definitions above, this definition makes it possible to recognize the following syntax (where the question mark is the general unquote operator)
\\ (?E1 = ?E2)
as a syntactically sugared form of the following meta-level (i.e., Prolog) term:
gr(constraint, =, [E1, E2])
A call to the type constraint
constraint_( \\ (?E1 = ?E2) )
can therefore reduce to
term_(E1), term_(E2)
Empty programs are an example of operators with no arguments:
operator []: --> program.
Prolog's list constructor, normally written [...|...]
can also be defined as an operator by referring to its internal representation in Prolog, which
is a binary functor '.'.
The following operator provides a smooth interaction with Prolog's parser, so that object programs can be written
as lists of clauses:
operator '.' : clause * program --> program.
As recalled above, the <op> field of a special operator definition is of the following form:
any-<special_category>
[^<primary_symbol>
[^<argument_list>]
]<special_category> is one of the symbols sketched in the table of special categories.
<primary_symbol> and <argument_list> can be any Prolog term (usually they are variables). When the given rule is applied, <primary_symbol> is unified with the value of the primary symbol of the matched term, and <argument_list> with its argument list. For constant symbols, the argument list is an empty list.
The following declaration
operator any-head: *(term) --> atom.
indicates that we recognize as an object atom anything that is a head (see below) whose 0 or more arguments are of type term.
Notice that the following more specific definitions (meant as exceptions) need to be placed after the one above in order to be in effect:
operator ',' : formula * formula --> formula.
operator ';' : formula * formula --> formula.
operator true : --> formula.
operator = : term * term --> constraint.
operator dif : term * term --> constraint.
atom and constraint
are subtypes of formula, and the precedence
principles ensures that \\ (?A; ?B) will be read
as a formula with operator ';' and never as an
atom with predicate symbol ';'. We have also
that \\ (?A = ?B) will be read as a constraint
and never as an atom. It should be noticed that, actually, in order to resemble Prolog, the special category
any-head is already implemented in a way that does not allow any of the
5 symbols above. However, if the user wants to write an atom with a binary predicate
corresponding to the equality sign, he can still do so using the ground representation, e.g.
gr(atom, =, [\\\a, \\\'X']).
Suppose following operator definition is available for writing object clauses:
operator :- : atom * formula --> clause.
For all the definitions placed after this one, the syntactic sugar introduced by the :- operator will be applied. So it is possible to
declare a rule for facts in the following way:
operator any-head^P^AL : *(term) --> clause
{ es:translate(\ (?P ^ ?AL :- true), O) }
stands for O.
where the term following stands for is
translated to ground representation according to all the declarations made up to this
point. P will match the primary symbol and AL the argument list of the predicate in question, thus
\ [a, b, c(d)]
will be read as a program with three facts, which could have also been written in the following way:
\ [(a:- true), (b:- true), (c(d):- true)]
The explicit call
to es:translate (a predicate internal to the extended syntax that performs the
translation) is necessary because in some cases
further translation is needed (which is prevented by the unquoting operator ?),
for instance when P is parameterized (see paragraph 2.5).
Notice that if we had written the rule in this way:
operator any-head^P : *(term) --> clause
{ es:translate(\ (?P :- true), O) }
stands for O.
a program like \ [p(a)] would be translated
as if it was \ [(p :- true)], and therefore the
information about the argument list would be lost.
Program modules are defined in the following way:
operator any-identifier^M : --> program,
{object_module_source(M, S)}
stands for S.
any-identifier (see
below) matches any Prolog atom whose name begins with a lowercase letter. The code
informs the system that any identifier matched by M
for which the call to object_module_source
succeeds is acceptable as a program. The translation of an expression matching this rule
is the value returned for S from the call
to object_module_source(M, S).
The user may also decide to customize the error handling. For example, the above definition could be rewritten as follows:
operator any-identifier^M : --> program,
{object_module_source(M, S) -> true ;
write('wrong module '), write(M), nl, S = \ [] }
stands for S.
2.4.3.3 Further remarks about precedence
Let us now assume that the user declares the following operator:
operator crazy : --> program,
{ write('are you nuts?'), nl, fail }.
This is an exception to the rule for modules. Even if a module is defined with the name
crazy, the presence of crazy
where a program is expected will refer to the (most recent) rule above.
It is also possible (but not recommended!!) for the user to redefine central notations such as the empty list symbol, e.g. as follows:
operator [] : --> program
stands for my_very_strange_definition_of_empty_program.
Terms of type variable are matched by the
following rule:
operator any-variable_id : --> variable.
The expression any-variable_id matches
anything that looks like a Prolog variable inside a quotation operator (unless covered by
a question mark) and the name of the operator is the "quoted" Prolog atom
corresponding to the variable name. So, for example, the expression \\\'X'
is read as
gr(variable,'X',[])
Notice the difference from the previous Demo system where object variables could be written without quotes.
A syntax for the anonymous variable is also included. For this purpose, we introduced another special symbol that matches only the anonymous variable.
operator any-anonymous_variable_id : --> variable,
{generate_variable_id(V)}
stands for gr(variable, V, []).
The predicate generate_variable_id generates
a new, yet unused variable identifier, e.g. of the form '_345',
'_346', etc.
Because this operator definition appears after the one for general variables above, the anonymous variable will never be taken for an ordinary one.
notation |
is any term... |
examples |
any-prolog_atom |
matching atom
and not beginning with _ or a capital letter |
a, b, ===,
but not 7 |
any-prolog_atomic |
matching atomic
and not beginning with _ or a capital letter |
a, b, ===, 7, -3,
3.14, -2.7 |
any-integer |
matching integer |
7, -3 |
any-float |
matching float |
3.14, 2.0, but not 7,
-3 |
any-number |
matching number |
3.14, 2.0, 7, -3 |
any-identifier |
matching atom and beginning with a small letter |
a, b, but not === or 7 |
any-head |
that is acceptable as the head of a clause | a, a('X'), 2+2, but not 7 or (a,b) |
any-compound |
matching compound |
a('X'), 2+2, but not 7 |
any-term |
which is a correct Prolog term | |
any-anonymous_variable_id |
shaped as a quoted Prolog anonymous variable | '_' (and nothing else) |
any-variable_id |
shaped as a quoted Prolog non-anonymous variable | 'A', 'X11', but not '_' |
For the three special categories any-term, any-head, and any-compound,
the extended syntax will also recognize an auxiliary notation, that is an expression of the form:
^
<argument_list>This notation enhances the expressibility of the extended notation, as it allows meta-variables in <primary_symbol> and <argument_list> (without the auxiliary notation one can only use a meta-variable for a single argument). Some examples are shown in the following table, where we suppose that there exists a type t whose quotation operator is qo.
| DemoII expression | Ground representation |
qo(?F ^ ?Args)
|
gr(t, F, Args) |
qo(?f ^ ?Args) |
gr(t, f, Args) |
qo(?F ^ [?A1,
?A2]) |
gr(t, F, [A1, A2]) |
qo(?F ^ [?A |
?Args]) |
gr(t, F, [A | Args]) |
qo(?F ^ [a |
?Args]) |
gr(t, F, [gr(ta,a,[])|Args]) |
In the last example we indicated with ta the type of the object a that will be matched in this specific context.
The auxiliary notation is also used to parameterize <primary_symbol> with an object variable. See paragraph 2.5.
When DemoII prints out answers and the normal notation does not apply, the auxiliary notation is used.
In cases where not even the auxiliary notation applies, the
system will fall back to the use of gr, possibly
prefixed by a question mark.
Object program modules are used for making it easier to write calls to the demo predicate; without modules one would have to
write the entire object programs as arguments each time a query was posed.
Modules are declared in the following way:
object_module(<module_name>, <object_program>).where <module_name> is the name associated to the program
<object_program>.
<module_name>
must be a Prolog atom and <object_program>
must be completely ground at the meta-level – in other words, no
meta-variables are allowed. Of course, it only makes sense when
<object_program> expresses a term in
ground representation of type program, but no
check is attempted.
Example:
object_module_source( my_object_prog, \ [my_fact]).
This declares a module named my_object_prog
by asserting the following Prolog fact:
object_module_source( my_object_prog,
gr(program,'.',
[gr(clause,':-',[gr(atom,my_fact,[]),gr(formula,true,[])]),
gr(program,[],[])]).
DemoII provides an easy way to write predicates consisting of a pattern which applies unchanged to each clause in an object program. Such predicates can be declared by the user with the following macro:
easy_mk_bias_predicate(<predicate_name>, <clause_pattern>, <condition>)The system expands the macro according to the following scheme:
:- block <predicate_name>(-), <predicate_name>_aux(-).(\[]).(\ (?A & ?B)) :- <predicate_name>(A), <predicate_name>(B).(\ [?C | ?More]) :-
<predicate_name>_aux(C),
<predicate_name>(More)._aux(<clause_pattern>) :-
<condition>.This pattern can be used as a general scheme for predicates like the following one (where one usually
forgets to include a rule for '&'). A natural language example:
easy_mk_bias_predicate( verb_clauses, \verb(?Word, ?ObjCat, ?SubCat), (constant_(Word),
category(ObjCat), category(SubCat))which expands to
- :- block verb_clauses(-), verb_clauses_aux(-).
- verb_clauses( \[]).
- verb_clauses( \ (?A & ?B)):-
- verb_clauses(A), verb_clauses(B).
- verb_clauses( \ [? C | ?More]):-
- verb_clauses_aux(C),
- verb_clauses(More).
- verb_clauses_aux( \verb(?Word, ?ObjCat, ?SubCat) ):-
- constant_(Word),
category(ObjCat), category(SubCat).
Notice that this macro cannot be used to write predicates that need to carry along information about the whole program. For instance, a predicate for expressing that a program does not contain duplicate clauses cannot be written in this way, because being disjoint from the rest of the program is a property that depends on the program and not on the single clause.
2.5 Parameterizing over predicate and function symbols
There are cases where it is interesting to write conditions that parameterize over function or predicate symbols. Here is an example of an integrity constraint:
fails(Prog, \\ ('P' ^ ['X',yes], 'P' ^ ['X',no]))
The meaning of it is that there does not exist any predicate name (to be substituted
for 'P') and values (to be substituted for 'X') such that the indicated conjunction holds. For a
better understanding of this example, see also chapter
4.
Whenever an object variable occurs in front of the ^
operator in the auxiliary notation, it is represented internally using the special marker par
(which stands for parameter). Notice that the parameterization can only be expressed with the auxiliary notation,
otherwise the system will raise an error. Examples:
| DemoII expression | Ground representation |
\\ ('P' ^ [a]) |
gr(atom, par('P'),
[gr(constant,a,[])]) |
\\ ('P'(a)) |
wrong expression |
\\ ('P' ^ []) |
gr(atom, par('P'),
[]) |
\\ ('P') |
wrong expression |
The unquoting operator cannot be used to express parameterization, so
\\ ( ?par(PAR) ^ [a] )is not a valid expression. If one wants to refer explicitly to the parameter name, this has to be done in two steps. Example:
X = \\ ( ?ParRef ^ [a] ), ParRef = par(PAR).2.6 Implementation of the extended syntax in SICStus Prolog version 3
Translation from the extended syntax to the ground representation of terms is
performed with the hook predicate term_expansion/2,
available in SICStus Prolog version 3.
When answers are being printed out a similar back-translation is performed for those
terms that match one of the syntactic definitions. There is a similar hook predicate which
modifies Prolog's standard output mechanism, called portray/1.
So, for example, a query of the form
?- X = \\\f(a,'X').
(which assigns the variable X a value gr(...) ),
is answered by
X = \\\f(a,'X') ?
and not
X = gr(...) ?In case of ambiguity, gr structures are
printed directly: in a query like
?- X = gr(atom,'=', [A,B]), Y = gr(constraint,'=', [A,B]).
the answer is printed as
X = \\ gr(atom,=,[A,B]),
Y = \\ (?A = ?B) ?
and not as
X = \\ (?A = ?B),
Y = \\ (?A = ?B) ?
Rules defined using stands for are ignored in
the output phase.
3 Constraints in the DemoII system
In this chapter we describe the most important constraints that are used
in the DemoII system. We consider instance and type constraints and a few others that are
needed for the demo predicate. We describe here the declarative
semantics and a few points concerning their implementation.
Those constraints that are relevant for most users of DemoII are:
type constraints and the related ground_ constraint;fails and associated preds_
and no_preds_ described in chapter 4Notice that, due to some limitations of CHR, all files containing CHR rules must be merged in one file.
So, if a user wants to add a new file with CHR rules to the system, the following line in file
demo.pl needs to be modified:
:- merge(['Source/tc.pl', 'Source/ic.pl', 'Source/oc.pl', 'Source/sc.pl',
'Source/ac.pl', 'Source/df.pl'], demo_temporary)
The files mentioned in the first argument of merge are discussed in this
chapter, except for the last two, which are described in chapter 4.
merge is a special predicate defined in DemoII that, among other things,
allows detecting singleton variables in CHR rules (which are not reported by CHR).
Extra files should then be listed after
'Source/df.pl'. demo_temporary is the file
containing the result of the merging, which is consulted and thereafter deleted.
As anticipated in chapter 2, each type (and subtype) defined by the user gives rise to a type constraint which is mapped into a generic type constraint in the following way:
_(X) :- type(<simple-type>, X).These constraints are automatically generated and should not be applied directly by a user. Their declarative semantics is as follows:
type(<type>,
T)
holds iff T is of type
<type> (def. section 2.3.4)
Thus, for any simple type <simple-type> we have
_(T)
iff T is of type <simple-type>.
The rules defining the behavior of type constraints are found in file tc.pl.
Normally, the evaluation of a type constraint does not instantiate its arguments. In a call of the form
_(X)the variable X is not instantiated and the constraint delays. For a
call of the form
<type>1_( gr(<type>2,
<symbol>,
<arglist>) )
with <type>2 and <symbol> ground, the constraint solver selects a matching operator definition, if any, and calls recursively a type constraint for the argument list, which will delay if <arglist> (or a tail of it) is a variable. If more than one operator is possible, they are all tried on backtracking.
However, things are different if <type>2 and/or <symbol> are nonground. In such a case, all possible instantiations for <type>2 and <symbol> are tried on backtracking. The user should be aware that this behavior never occurs, unless the user is forcing it with some programming virtuosism (which we do not encourage).
3.2 Low-level syntactic constraints
In order to cope with
terms in ground representation with nonground <type>
and/or <symbol> components, we need a few accessory
constraints. The purpose of these constraints is to classify the <symbol>
field of gr structures and to interact with type constraints.
The categories of Prolog symbols corresponding to these constraints are organized in such a way that either two of them are disjoint or one is a subset of the other. Next follows a short description.
| Syntactical category | matches any term |
prolog_atomic_ |
satisfying Prolog's atomic and not beginning
with _ or a capital letter |
number_ |
satisfying Prolog's number |
integer_ |
satisfying Prolog's integer |
float_ |
satisfying Prolog's float |
anonymous_variable_id_ |
shaped as a Prolog anonymous variable |
variable_id_ |
shaped as a Prolog non-anonymous variable |
function_id_ |
acceptable as a function identifier beginning with a small letter |
parameter_ |
of the form par(<P>),
where <P>
satisfies variable_id_ (for internal use only) |
function_id_or_parameter_ |
satisfying either function_id_ or parameter_ |
We can indicate the subset ordering by indentation as follows:
- prolog_atomic_
- number_
- integer_
- float_
- anonymous_variable_id
- variable_id_
- function_id_or_parameter_
- function_id_
- parameter_
The following behavior is then guaranteed: if a variable is constrained at the same time to
In all the other cases these constraints evaluate to failure or success if an only if their argument is ground.
Example. The following type constraint
constant_( gr(constant, X, L) )reduces to the couple of constraints
prolog_atomic_(X), type([],L)because of the existence of the operator definition:
operator any-prolog_atomic : --> constant.No further evaluation is made until X
(or L) gets instantiated.
The syntactic constraints are defined in file sc.pl
As recalled in section 2.3.2, there are three categories of types:
variable, which is a subtype of term;term;The constraint
instance_(t1,
t2)is satisfied if and only if t1 and t2 name object phrases T1 and,
respectively, T2 with T2 being an instance of T1.
Implementation-wise, instance_/2 constraints are mapped
into instance_/3 constraints, where the additional argument
represents an object-level substitution:
instance_(X,Y) :- instance_(X,Y,_).The declarative semantics of instance_/3 can be defined as follows:
instance_(t1,
t2, s)
is satisfied when
t1, t2 and s name object-level terms
T1, T2 and, respectively, substitution with
T1 = T2.However, for practical reasons, we use a slightly more general definition, based on pseudo-substitutions, which, as mentioned in paragraph 2.2, is a list of pairs of the form
(<id>
-> <term>)
where <id> is an acceptable identifier for an object variable and <term> is an arbitrary meta-level term (not necessarily being the name of anything). All the object variable identifiers in a given pseudo-substitution must be distinct.
The application of a pseudo-substitution S to any meta-level term T (which can be made both for usual object variables and for the predicate/function symbol paremeters described in section 2.5) is defined as follows.
gr(variable,
<id>, [])
in T, for which S = [
... (<id>
->
<term>)
...],
is replaced by <term>;gr(<type>,
par(<id>),
<argument_list>1)
in T, for which S = [
... (<id>
->
<term>)
...],
is replaced by
gr(<type>,
<term>),
<argument_list>2),
where, recursively, S applied to <argument_list>1 yields
<argument_list>2.
The revised declarative semantics used by DemoII is then the following:
instance_(t1,
t2, s)
is satisfied for any meta-level terms
t1 and t2 and pseudo-substitution s whenever
s applied to t1 yields t2.
We can formally relate to the previous definition by the following property:
_(t1),
<type>_(t2),
instance(t1,
t2,
s)Notice that instance constraints do not carry information about the type, as we assume that the involved terms are already covered by type constraints.
The rules defining the behavior of instance constraints are found in file ic.pl.
3.3.1 Remarks about activation and delay
The behavior of instance constraints changes depending on the type of its arguments. Normally the propagation of the arguments takes place from left to right. Examples:
- instance_(X,Y,S), X = \\true.
- X = \\true,
- Y = \\true
- instance_(X,Y,S), Y = \\\f(?A,?B).
- Y = \\\f(?A,?B),
- instance_(X,\\\f(?A,?B),S)
In the first example the constraint is activated and the second argument (Y)
gets instantiated. In the second example the constraint is delayed because the first argument is unknown.
However, if the second argument's type is different from term the propagation can also take place from right to left. Example:
- instance_(X,Y,S), Y = \\f(?A,?B).
- X = \\f(?_A,?_B),
- Y = \\f(?A,?B),
- instance_(_A,A,S),
- instance_(_B,B,S)
If the first argument is an object variable, the propagation may also reach the third argument or issue a failure. Examples:
instance_(\\\'X', \\\a, S).
- S = [('X'-> \\\a)|_A]
instance_(\\\'X', \\\a, [(\\\'X'-> \\\b)|_]).
- no
Notice that an instance constraint does not perform any consistency check on the types of its arguments, as these are supposed to be already covered by type constraints. So, in principle, it would be possible to use instance constraints with wrong object terms. Example:
instance_(X,Y1,S), X = nonsense.
- X = nonsense,
- instance_(nonsense,Y1,S)
instance_(X,Y1,S), formula_(X), X = nonsense.
- no
3.3.2 Adding "occurs-check" to the constraint solver
In order to handle cases where occurs-check may be relevant, we provide an alternate version of the file
containing instance constraints (see also the section on how to start the system in the
user manual). In this file, ic_o.pl, unification
proper is replaced by unification with occurs-check, implemented in SICStus Prolog as
unify_with_occurs_check. We give no formal proof of the validity of
this approach.
DemoII includes a few other accessory constraints, defined in file oc.pl:
ground_(<term>),
which fails if <term> is covered by a
variable_ constraint. Furthermore, it causes the arguments of an instance
constraint to be unified, if one of them is covered by ground_.
This constraint is currently not used anywhere in the system.member_(<clause>,
<program>), which states membership
of clause <clause> in program <program>.
This constraint is implemented in plain Prolog, therefore it does not delay. Two cases are only possible:
demo predicate.
no_duplicates_(<program>),
which states that the same clause cannot appear more than once in <program>.
This constraint is implemented as a Prolog blocked predicate and is used
in the definition of the demo predicate.disjoint_(<program>1,
<program>2),
which states that <program>1 and
<program>2 have no clause in common. It is used
by no_duplicates_ and implemented as a blocked
predicate.not_member_(<clause>,
<program>), which states that
<clause> cannot be a member of <program>.
It is used by no_duplicates_ and disjoint_
and implemented as a blocked predicate.In this chapter we shall describe briefly the principle of lazy negation as failure
used for the implementation of fails.
This feature is new and it will be described in a forthcoming publication, expected 1999.
Ordinary negation as failure in Prolog consists of examining all possible branches of a given goal to make sure that it cannot be proved. In our object language, a program can have "holes", that is unknown parts referenced to by a meta-variable. Example:
\ [(p('X'):- q('X')), q(a),
..., ?MetaVar]
The "hole" represented by the meta-variable MetaVar
stands, in this case, for an unknown clause of the program.
Lazy negation as failure behaves then as follows:
This means that, initially, the known part of the program is checked to obey the specified conditions, and each time a new program part arrives, it is checked, in an incremental way, if this part violates the conditions.
Examples of application can be found for instance in database view update with integrity constraints. Consider the following module, defining a knowledge basekb:
object_module( kb, \ [
- (sibling('X','Y'):- parent('Z','X'), parent('Z','Y')),
- (parent('X','Y'):- father('X','Y')),
- (parent('X','Y'):- mother('X','Y')),
- (father(john, mary):- true),
- (mother(jane,mary):- true)
- ]).
ic:
object_module( ic, \ [
- (bottom:- father('A','C'), father('B','C'), dif('A','B')),
- (bottom:- mother('A','C'), mother('B','C'), dif('A','B')),
- (bottom:- father('X','_'), mother('X','_'))
- ]).
New) of father
or mother type only (which is specified by the predicate
father_mother_facts_only), provided that the integrity constraints
are not violated:
?- father_mother_facts_only(New),
- fails( \ (kb & ic & ?New), \\bottom ),
- demo( \ (kb & ?New), \\sibling(mary,bob) ).
4.1 Implementation of lazy negation as failure
fails has been programmed with the Constraint Handling Rules
library (CHR) available in SICStus Prolog. Its source code is contained
in file df.pl.
The main idea is to replace Prolog's backtracking by an explicit iteration process such that different subcomputations can be delayed for the part of the object program that is "missing". This means that a selected atom needs to be unified with the head of several clauses. In order to obtain a correct behavior, we need to produce fresh copies of the current query as well as of the delayed constraints pending on it.
However, the basic principles of this process can be reasonably explained in terms of a nondeterministic implementation that does not include this copy machinery. It works as follows:
fails
are activated instead of just a single one
(i.e., at least one call for each branch in the SLDNF tree).demo predicate,
fails
takes an instance of the object query and calls
another predicate (fails1) that does the job.
fails(P, Q):-
- instance_(Q, Q1),
- fails1(P, Q1).
fails1(P,Q1) is roughly,
that Q1 names a ground object query that fails in the given
program.
fails1 is defined as the negation of the object goal for trivial cases
by the following CHR rules:
- fails1(_, \\ true) <=> fail.
- fails1(_, \\ dif(?A,?B)) <=> A=B.
- fails1(_, \\ (?A = ?B)) <=> dif(A,B).
In general, fails1 proceeds only if it is
possible to select a "simple" goal. If it is, it then separates such goal from the rest of the query, tests the goal
and continues with the rest, after having nondeterministically selected a clause of the program.
fails1(P, Q) <=> can_select_simple(Q, Simple, Rest) |
- (
- Simple = \\dif(?A,?B) ->
... fails1(P,Rest) ;fails1(P,Rest) ;) ->C in P), fails1_with_clause(C, Simple, P, Rest)A simple goal is either a dif or =
constraint whose arguments satisfy Prolog's ?=/2 or a
gr structure whose type is atom.
In other words, if no part of the query is sufficiently instantiated, fails1
delays.
The continuation is immediately stopped if the head of the selected clause evidently cannot unify with the selected goal, like for instance when the predicate names or the arities are different.
fails1_with_clause(\ (?Head :- ?_), SelectedAtom, _, Cont) <=>
- (
a surface test shows that Head can never unify SelectedAtom) |Otherwise, if the possible success of the unification can be trusted independently of instantiations of external variables interfering with the two atoms (which is checked by determinable_instance), the unification is executed (via instance_ constraints) thus leading either to continuation on the remaining goals or to success.
fails1_with_clause(\ (?Head :- ?Body), SelectedAtom, Prog, Cont) <=>
- determinable_instance(Head,SelectedAtom) |
- ( instance_(Head, SelectedAtom, S)
- -> ( instance_(Body, Body1, S),
- conjunc(Body1, Cont, NewQuery),
- fails1(Prog, NewQuery)) ;
- true).
Some examples can show the behavior of fails.
Definitive answers:
- | ?- fails(\[(a)], \\a).
- no
- | ?- fails(\[(b)], \\a).
- yes
- | ?- fails(\[(?H :- true)], \\f(?A)).
- instance_(A,_A,_B),
- fails1_with_clause(\ (?H:-true),
- \\f(?_A),
- \[(?H:-true)], \\true) ?
- | ?- fails(\[(?H :- true)], \\f(?A)), H= \\b.
- H = \\b ?
- | ?- fails(\[(?H :- true)], \\f(c,?A,a)).
- instance_(A,_A,_B),
- fails1_with_clause(\ (?H:-true),
- \\f(c,?_A,a),\[(?H:-true)],\\true) ?
- | ?- fails(\[(?H :- true)],\\f(c,?A,a)), H= \\f(d,?B,b).
- H = \\f(d,?B,b) ?
fails can effectively discard useless branches
in the case that the predicate symbols of selected atom and clause
are instantiated and different. In order to be able to discard branches also for clauses
and subprograms, still given as uninstantiated metavariables,
the user can inform the system about those predicates that
can (or cannot) appear, using the following constraints:
preds_(<term>,
<specification>)no_preds_(<term>,
<specification>)<specification> is a list of predicate names without arity. A predicate is
either a Prolog atomic or the term par(ameter).
<term> is either a gr structure
of type program, clause, or atom, or a prolog atomic or a structure of the form par(<object-variable>).
preds_ is satisfied if and only if the predicate symbol of each clause
head in <term> (or <term> itself)
matches an element given in <specification>.
The term par(ameter)
is meant to match par(<object-variable>)
and nothing else; any other symbol matches only itself.
no_preds is the negated version (meaning that no predicate
name in <term> matches an element in <specification>).
Example:
preds_(P, [p,q,par(ameter)])
These constraints are defined in file ac.pl
This document was last modified on Monday, December 21, 1998