Transcript Document

Unification
- An overview
• Need for Unification
• Ranked alfabeths and terms.
• Substitutions
• Unifiers and mgus
• Martelli Montanari Algorithm
10 October 2006
Foundations of Logic and Constraint Programming
1
Why unification ?
- In propositional logic two clauses may resolve if they have two complementary
literals.
A  P
P  B
A  B
- In the propositional case, two literals are the same if they have the same
proposition (negated in exactly one of them).
- In first order logic, the situation is more complex, due to the existence of
variables. We may assume that variables are universally quantified.
- In this case, to apply resolution, the proposition do not have to be the same in
the complementary literals belonging to two clauses.
- Intuitively, since the variables are universally quantified and may be replaced by
any “objects”, the predicate must refer to the same objects. For example
q(X)  p(X,b)
P(a,Y)  r(Y)
q(a) r(b)
10 October 2006
Foundations of Logic and Constraint Programming
2
Term Universe
- Informally, the purpose of unification is to find what the common objects are.
Such goal may be acomplished by purely syntactic means, through processing
of the terms appearing in the common predicates.
- A term is composed of one or more symbols from
• Variable symbols (convention: starting with upper case)
• Alphabet is a finite set Σ of symbols (convention: starting with lower case)
• To every symbol a natural number  0 is assigned (its arity or rank).
• Σ(n) denotes the subset of Σ with arity n
• A symbol with arity 0 (belonging to Σ(0)) is a constant.
- Given a set of variables V and a ranked alphabet of function symbols F, the
term universe TUF,V (over F and V) is the smallest set T of terms such that
a) V  T
b) f  T, if f  F(0)
c) f(t1,t2, ... ,tn)  T if f  F(n) and t1,t2, ... , tn  T
10 October 2006
Foundations of Logic and Constraint Programming
3
Ground terms and Herbrand Universe
- The set of variables appearing in a term t is denoted by Var(t)
 Var(t) : set of variables in term t
- A term is ground if it contains no variables
 t is ground : Var(t) = 
- If F is a ranked alphabet of function symbols, then HUF, the Herbrand Universe
over F, is the set of terms that can be formed without variables
 HUF : TUF, 
 Example: Given F = {a, f/1, g/2} it is HUF =
= { a,
f(a), g(a,a),
g(a,f(a)), g(f(a),a), g(g(a,a),a), g(a, g(a,a)),
f(f(a)), f(g(a,a)), g(f(a),f(a)), g(f(a),g(a,a)),
g(g(a,a),f(a)), g(g(a,a),g(a,a)),... }
- A subterm s of t, is a term that is included in t
 s = sub_term(t) : s is a term that is a sub-string of t
10 October 2006
Foundations of Logic and Constraint Programming
4
Substitutions
-
Informally a variable (universally quantified) may be substituted by a term
(with some constraints). More formally, given
• V, a set of Variables
• X  V, a subset of variables to be substituted
• F, a ranked alphabet
a subtitution θ :  X → TUF,V with x  θ(x) for any x  X.
-
The following notation is commonly used for a substitution θ
θ = {x1/t1, x2/t2, ... xn/tn }, where
1. X = {x1, x2, ... xn },
2. θ(xi) = ti for every xi  X
-
It is also convenient to define
 Empty substitution ε :  n = 0
 θ is a ground substitution :  t1, t2, ... , tn are ground terms.
 θ is a pure variable substitution:  t1, t2, ... , tn are variables.
 θ is a renaming :  {t1, t2, ... , tn }  {x1, x2, ... xn }.
10 October 2006
Foundations of Logic and Constraint Programming
5
Substitutions
-
For a subtitution θ it is also convenient to consider

The domain of the substitution is the set of variables to be substituted
Dom(θ ) :  {x1, x2, ... xn }.

The Range of the substitution is the set of terms for which the variable are
substituted
Range(θ ) :  {t1, t2, ... , tn }

The Ran of the substitution is the set of variables appearing in these terms
Ran(θ ) :  Var(Range(θ ) )

The variables of the substitution are those in its domain or in its ran.
Var(θ ) :  Dom(θ)  Ran(θ )

The projection of a substitution to a subset of its domain Y  Dom(θ )
θ | Y :  {y/t | y/t  θ and y  Y)
10 October 2006
Foundations of Logic and Constraint Programming
6
Application of Substitutions
- A few notational conventions and definitions are commonly used when a
substitution θ is applied
 If x is a variable and x  Dom(θ), then xθ :  θ(x)
 If x is a variable and x  Dom(θ), then xθ :  x
 f(t1, t2, ... , tn )θ :  f(t1θ, t2θ, ... , tn θ )
 t is an instance of s :  there is a substitution θ with sθ = t
 s is more general than t :  t is an instance of s
 t is a variant of s :  there is a renaming θ with sθ = t
- Lemma 2.5
 t is a variant of s iff t is an instance of s and s is an instance of t.
10 October 2006
Foundations of Logic and Constraint Programming
7
Composition of Substitutions
-
During a resolution proof, several substitutions are performed in sequence, in
which variables are successively replaced by terms with other variables. The
notion of composition captures the intuition of end result of these
substitutions.
Definition (2.6)
The composition of substitutions θ and σ is defined as
(θ σ) x :  x (θ)σ for every variable x
-
Lemma (2.3)
Let θ = {x1/t1, x2/t2, ... xn/tn }, σ = {y1/s1, y2/s2, ... ym/sm }. Then θ σ can be
constructed from the sequence
x1/t1 σ, x2/t2 σ, ... xn/tn σ, , y1/s1, y2/s2, ... ym/sm
1. By removing all bindings xi/ti σ where xi = ti σ
2. By removing all bindings yj/sj where yj  {x1, x2, ... xn}
3. By forming a substitution from the resulting sequence.
10 October 2006
Foundations of Logic and Constraint Programming
8
An Ordering of Substitutions
- A substitution restricts the values a variable may take, and the more so, when
more substitutions are applied in sequence. This augmented restriction is
captured by the ordering of substitutions.
Definition (2.6)
- Let θ and σ be substitutions. Then
θ is more general than σ :  σ = θ for some substitution .
(equivalently, σ is a specialisation of θ , or θ can be specialised to σ).
- Examples:
- θ = {x/y} is more general than σ = {x/a, y/a} since for  = {y/a} it is σ = θ.
Since, y = a, then θ = {x/yσ , y/a} = {x/a, y/a} = σ.
- θ = {x/y} is not more general than σ = {x/a}, since every  such that θ = σ
should contain a pair y/a, and that pair should appear in θ .
x/a  {x/y}   y/a    y  Dom(σ ) = Dom (θ)
Intuitively, σ = {x/a} can be specialised to {x/a, y/b} but θ = {x/y} cannot, so
θ cannot be more general than σ.
10 October 2006
Foundations of Logic and Constraint Programming
9
Unifiers
- The resolution of two clauses does not require the occorrence of
complementary literals that are equal (apart from the negation) but rather that
the complementary literals are applicable to the same objects. Hence, the terms
in the literals must be unifiable, i.e. equal after performing some substitution.
Definition (2.9)
- Given substitution θ and terms s and t
 θ is a unifier of s and t :  sθ = tθ.
 s and t are unifiable :  sθ = tθ for some θ.
Many unifiers may exist between two terms, but it is specially interesting (e.g. in
resolution) to consider the most general unifier (mgu).
 θ is a mgu of s and t :  sθ = tθ  s σ = t σ  σ = θ for some .
- The definition of unifiers for pairs of terms, may be extended for sets of pairs of
terms.
10 October 2006
Foundations of Logic and Constraint Programming
10
Most General Unifiers
• The literals to be unified may have more than one argument. The following
definitions are relevant in this case.
- Let s1, s2, ... , sn, t1, t2, ... , tn, be terms; si ≈ ti denote the (ordered ) pair (si, ti);
and E = {s1 ≈ t1, s2 ≈ t2, ... Sn ≈ tn }. Then
 θ is a unifier of E :  siθ = tiθ for all i 1..n.
 θ is an mgu of E :  σ is a unifier of E  σ = θ for some .
- Sets E and E’ are equivalent
:  θ is a unifier of E  θ is a unifier of E’
- E = {x1 ≈ t1, x2 ≈ t2, ... xn ≈ tn } is solved : 
 xi, xj are pairwise distinct variables (1  i  j,  n)
 no xi, occurs in tj (1  i, j,  n)
10 October 2006
Foundations of Logic and Constraint Programming
11
Most General Unifiers
Lemma (2.15)
If E = {x1 ≈ t1, x2 ≈ t2, ... xn ≈ tn } is solved, then θ = {x1/t1, x2/t2, ... xn/tn }, is an
mgu of E.
Proof:
1)xi θ = ti= ti θ
2)For every unifier σ of E, it is xiσ = ti σ. But ti= ti θ and so xiσ = xi θ σ; for
every i 1..n. Additionally, x σ = x θ σ = x for every x {x1, x2, ... , xn}.
Hence, σ = θ σ and θ is thus more general than σ.
• Once the unification of predicates and terms with more than one argument is
defined, it is important to obtain an algorithm to perform the unification of two
terms.
• In fact, it is easier to define an algorithm that unifies a set of pairs of terms –
the Martelli – Montanari algorithm.
10 October 2006
Foundations of Logic and Constraint Programming
12
Martelli – Montanari algorithm
Martelli-Montaneri algorithm (MM)
Let E be a set of pairs of terms. As long as it is possible, choose
nondeterministically a pair in E and perform the appropriate action:
a) f(s1,s2, .. , sn) ≈ f(t1,t2, .. , tn)
→ replace, in E, by s1 ≈ t1, s1 ≈ t1 , ... , sn ≈ tn
b) f(s1,s2, .. , sn) ≈ g(t1,t2, .. , tn) where f  g
→ halt with failure (clash)
c) x ≈ x
→ delete the pair
d) t ≈ x where t is not a variable
→ replace by x ≈ t
e) x ≈ t where x  Var(t) and x occurs in some other pair
→ perform substitution { x / t } in those pairs
f) x ≈ t where x  Var(t) and x  t
→ halt with failure (occurs check)
The algorithm terminates when no action can be performed.
10 October 2006
Foundations of Logic and Constraint Programming
13
Martelli – Montanari algorithm
Theorem 2.16
If the original set has a unifier, the algorithm MM successfully terminates and
produces a solved set E´ that is equivalent to E; otherwise the algorithm
terminates with failure.
Proof Steps:
1. Prove that the algorithm terminates.
2. Prove that each action replaces the set of pairs by an equivalent one.
3. Prove that the algorithm terminates with failure, then the set of pairs at the
moment of failure has no unifiers*.
• Given 2, the set E’ is equivalent to E, so E also has no unifiers
4. Prove that if the algorithm terminates successfully, the final set of pairs is
solved**.
• By lemma 2.15, if the final set of pairs is solved, then it is an mgu.
10 October 2006
Foundations of Logic and Constraint Programming
14
Substitution Ordering
- Before going through each of the steps, the notion of well-founded orderings
must be defined for relations on sets.
- Intuitively, even if the set is infinite, an well founded relation guarantees that the
sets can be ordered so that they have an “initial” element.
- First some definitions on relations
Definitions
 R relation on set A :  R  A  A
 R reflexive
:  (a,a)  R for all a  A
 R irreflexive
:  (a,a)  R for all a  A
 R antisymmetric
:  (a,b)  R and (b,a)  R implies that a = b.
 R transitive
:  (a,b)  R and (b,c)  R implies that (a,c)  R .
10 October 2006
Foundations of Logic and Constraint Programming
15
Lexicographic Ordering
- The lexicographic ordering <n (n>1) is defined inductively on the set Nn of ntuples of natural numbers.
 Base Clause
(a1) <1 (b1) :  a1 < b1
 Inductive Clause
(a1, a2, ... , an+1) <n+1 (b1, b2, ... , bn+1) : 
(a1, a2, ... , an) <n+1 (b1, b2, ... , bn) ; or
(a1, a2, ... , an) = (b1, b2, ... , bn) and an+1 <n bn+1
- Examples: (5,3,9) <3 (5,3,11),
(1,4,8) <3 (2,3,5).
- The lexicographic ordering (Nn, <n) is well-founded
 Irreflexive partial ordering (irreflexible and transitive) with
 Lowest element : (0,0, ..., 0)
10 October 2006
Foundations of Logic and Constraint Programming
16
Well founded orderings
- Once defined the basic properties of relations some properties may be defined
on the orderings they induce in particular sets..
Definitions
 (A, R) is a (reflexive) partial ordering
:  R is a reflexive, antisymmetric, and transitive relation on A
 (A, R) is a irreflexive partial ordering
:  R is a irreflexive and transitive relation on A
 (A, R) is well-founded ordering
:  R is a irreflexive partial ordering; and
there is no infinite descending chain ... a2 R a1 R a0.
Examples
Partial Orderings :
Irreflexive partial Orderings:
Well Founded:
Not Well Founded:
10 October 2006
(N, ),
(N, <),
(N, <),
(Z, <),
(Z, ), (({1,2,3,4}), )
(Z, <), (({1,2,3,4}), )
(({1,2,3,4}), )
Foundations of Logic and Constraint Programming
17
Algorithm MM terminates
1. MM terminates (1)
- Let the following denotations apply
 Variable x solved in E : 
x ≈ t  E, and this is the only occurrence of x in E
 Uns(E) : 
number of variables in E that are unsolved
 lfun(E) : 
number of occurrences of function symbols in the first components of
pairs in E
 card(E) : 
number of pairs in E
- Let us consider tuple (Uns(E) , lfun(E), card(E)). To prove termination of MM, it
is sufficient to prove that each action in MM reduces this tuple. From the wellfoundness of 3 tuples, the recursion must terminate (in the worst case, it cannot
go below the lowest element).
10 October 2006
Foundations of Logic and Constraint Programming
18
Algorithm MM terminates
1. MM terminates (2)
- Let us consider tuple (u,l,c) = (Uns(E) , lfun(E), card(E)) to show that the MM
operations except b) and f), leading to failure, always lead to a lower tuple.
a) f(s1,s2, .. , sn) ≈ f(t1,t2, .. , tn)
→ replace, in E, by s1 ≈ t1, s2 ≈ t2 , ... , sn ≈ tn
(u,l,c) → (u-k, l-1, c+n-1) for some k  1..n
c) x ≈ x
→ delete the pair
(u,l,c) → (u-k, l, c-1) for some k  0..1
d) t ≈ x where t is not a variable
→ replace by x ≈ t
(u,l,c) → (u-k1, l-k2, c) for some k1  0..1 and k2  1
e) x ≈ t where x  Var(t) and x occurs in some other pair
→ perform substitution { x / t } in those pairs
(u,l,c) → (u-1, l+k, c) for some k  1
10 October 2006
Foundations of Logic and Constraint Programming
19
Algorithm MM is correct
2. MM replaces the set of pairs by an equivalents set
a) f(s1,s2, .. , sn) ≈ f(t1,t2, .. , tn) → replace, in E, by s1 ≈ t1, s1 ≈ t1 , ... , sn ≈ tn
c) x ≈ x → delete the pair
d) t ≈ x where t is not a variable → replace by x ≈ t
•
This is clearly true for actions a), c) and d) above. For action e)
e) when x ≈ t where x  Var(t) and x occurs in some other pair
→ perform substitution {x/t } in those pairs
consider E  {x ≈ t } and E{ x/t }  {x ≈ t } then
iff
iff
iff
θ is a unifier of E  {x ≈ t }
(θ is a unifier of E) and xθ = tθ
(θ is a unifier of E {x/t} ) and xθ = tθ
θ is a unifier of E {x/t}  {x ≈ t }
10 October 2006
Foundations of Logic and Constraint Programming
20
Algorithm MM Result
3. If MM terminates with failure, then the set of pairs at the moment of
failure has no unifiers
•
In MM terminates with failure, the last action taken in E’ was either b) or d).
b) f(s1,s2, .. , sn) ≈ g(t1,t2, .. , tn) where f  g
→ halt with failure (clash)
f) x ≈ t where x  Var(t) and x  t
→ halt with failure (occurs check)
•
Given the definition of unification, there must be no unifier of E’.
Any substitution θ applied to f(s1,s2, .. , sn) θ would result in a term with
functor f, not g, so no unifier θ exists.
No substitution θ may contain a pair x/t where x  Var(t) and x  t, as would
be needed to unify x and t.
10 October 2006
Foundations of Logic and Constraint Programming
21
Algorithm MM Result
4. If the algorithm terminates successfully, the final set of pairs is solved
•
When algorithm MM terminates, with success, no left components of the pairs
in E’ are functions (otherwise, actions a) or b) or d) would apply).
a) f(s1,s2, .. , sn) ≈ f(t1,t2, .. , tn) → replace, in E, by s1 ≈ t1, s1 ≈ t1 , ... , sn ≈ tn
d) t ≈ x where t is not a variable → replace by x ≈ t
•
All pairs in E’ are in the form x ≈ t, where x is a variable. Furthermore t  x
(otherwise action c) would apply)
c) x ≈ x → delete the pair
•
No pair other than x ≈ t contains variable x, otherwise action e) would apply
e) x ≈ t where x  Var(t) and x occurs in some other pair
→ perform substitution { x / t } in those pairs
•
Hence, E’ has the form E’ = {x1 ≈ t1, x2 ≈ t2, ... xn ≈ tn }, where xi Var(tj), for
1 i  j n, and is thus in solved form.
10 October 2006
Foundations of Logic and Constraint Programming
22
Examples
- Some non-trivial examples (from SICStus Prolog, where variables are written in
upper case)
| ?- f(X,b) = f(a,Y).
X = a,Y = b ? ; no
|?- f(X,f(b)) = f(g(a,Y),Y).
X = g(a,f(b)), Y = f(b) ? ; no
| ?- f(X,f(b,Z)) = f(g(a,Y),Y).
X = g(a,f(b,Z)), Y = f(b,Z) ? ; no
| ?- X = f(Y), Y = f(a).
X = f(f(a)), Y = f(a) ? ; no
| ?- X = f(Y,Z), g(a,Y) = g(Z,b).
X = f(b,a),Y = b,Z = a ? ; no
10 October 2006
Foundations of Logic and Constraint Programming
23
Unifiers Size Can Be Exponential
- Example:
| ?- f(X1) = f(g(X0,X0)).
X1 = g(X0,X0) ? ; no
| ?- f(X1,X2) = f(g(X0,X0),g(X1,X1)).
X1 = g(X0,X0),
X2 = g(g(X0,X0),g(X0,X0)) ? ; no
| ?- f(X1,X2,X3) = f(g(X0,X0),g(X1,X1),g(X2,X2)).
X1 = g(X0,X0),
X2 = g(g(X0,X0),g(X0,X0)),
X3 = g(g(g(X0,X0),g(X0,X0)),g(g(X0,X0),g(X0,X0))) ?
; no.
...
- In this case, the “size” of variable Xi, in terms of occurrences of X0, is:
size(X1) = 2
size(X2) = 22 = 4
size(X3) = 23 = 8
...
size(Xn) = 2n
10 October 2006
Foundations of Logic and Constraint Programming
24
Strong MGUs
Definition
 Substitution θ is Idempotent
:θθ=θ
 :Mgu θ of terms s and t is strong
:  σ is mgu of s and t  σ = θ σ
Theorem 2.16
An mgu is strong iff it is idempotent.
Proof :
 Let θ be a strong mgu. Since θ is a strong mgu, for any unifier σ it is σ = θ σ.
In particular, for unifier θ, we have θ = θ θ. Hence θ is idempotent.
 Let θ be an idempotent mgu. Then, for any unifier σ there is some λ such
that σ = θ λ. But since θ is idempotent it is σ = θ λ = (θ θ) λ = θ ( θ λ) = θ σ.
Hence, θ is strong.
10 October 2006
Foundations of Logic and Constraint Programming
25
Strong MGUs
Examples
 The mgu θ = {x/y, y/x} of two identical terms is not strong. Indeed,
θ θ = {x/y, y/x } ° {x/y, y/x} = {x/x, y/y, x/y, y/x} = ε
 Substitution θ1 = {x/u, z/f(u,v), y/v} is Idempotent
{ x/u, z/f(u,v), y/v } ° { x/u, z/f(u,v), y/v } =
{ x/u, z/f(u,v), y/v, x/u, z/f(u,v), y/v } = { x/u, z/f(u,v), y/v } = θ1
Substitution θ2 = {x/u, z/f(u,v), v/y} is not Idempotent
{ x/u, z/f(u,v), v/y } ° { x/u, z/f(u,v), v/y } =
{ x/u, z/f(u,y), v/y, x/u, z/f(u,v), y/v } = { x/u, z/f(u,y), y/v }  θ2.
- The following lemma justifies a simple test to check whether a substitution mgu
is idempotent.
Lemma: A substitution θ is idempotent iff Dom(θ)  Ran (θ) 1 = 
10 October 2006
Foundations of Logic and Constraint Programming
26
Relevant MGUs
Definition
 Mgu θ of terms s and t is relevant
:  Var(θ )  Var(s)  Var(t)
Informaly, a relevant mgu does not introduce new variables. All mgus produced
by the Martelli-Montanari algorithm are relevant. Moreover
Theorem 2.22 (Relevance)
Every idempotent mgu is relevant.
Proof : in [Apt, 1997]
Note that the converse is not true, i.e. Not all relevant mgus are idempotent. For
example θ = {x/y, y/x}, which is a relevant mgu of terms s = f(x,y) and t = f(x,y),
is not idempotent.
As observed before, θ θ = ε, and ε is the mgu btained from the MM algorithm
when presented with E = { f(x,y) ≈ f(x,y) }.
10 October 2006
Foundations of Logic and Constraint Programming
27
Properties of MGUs
The following theorems can also be proved and are useful later (see [Apt97])
Lemma 2.23 (Equivalence):
Let θ1 be an mgu of a set of equations E. Then for every substitution θ2 , θ2 is
an mgu of E iff θ2 = θ1 ρ, where ρ is a renaming such that
Var(ρ) Var(θ1) Var(θ2).
Lemma 2.24 (Iteration) :
Let E1 and E2 be two sets of equations. Suppose that θ1 is an mgu of E1, and θ2
is an mgu of E2 θ1. Then θ1 θ2 is an mgu of E1  E2. Moreover, if E1  E2 is
unifiable, then an mgu θ1 of E1 exists and for any mgu θ1 of E1 there also exists
an mgu θ2 of E2 θ1.
Corollary 2.25 (Switching) :
Let E1 and E2 be two sets of equations. Suppose that θ1 is an mgu of E1, and θ2
is an mgu of E2 θ1. Then E2 is unifiable, and for every mgu θ1’ of E2 there exists
an mgu θ2’ of E2 θ1’ such that θ1’ θ2 ’ = θ1 θ2 . Moreover, θ2’ can be so chosen
such that Var(θ2’)  Var(E1)  Var(θ1’) Var(θ1 θ2).
10 October 2006
Foundations of Logic and Constraint Programming
28
Occurs Check in Prolog
- The occurs check is usually not implemented (by default) in Prolog, since
 It makes unification significantly harder
 It happens quite rarely
- Of course, unification behaves strangely when the occurs check is needed. For
example, in SICStus, we may observe
| ?- X = f(X).
X = f(f(f(f(f(f(f(f(f(f(...)))))))))) ? ; no
- Even worse
| ?- X = f(X).
X = f(f(f(f(f(f(f(f(f(f(f(... % LOOP <CTRL-C>
- To avoid this incorrect beheviour, most Prolog systems provide the possibility of
using correct, if innefficient unification.
10 October 2006
Foundations of Logic and Constraint Programming
29
Occurs Check in Prolog
- In SICStus, the explicit unification between two terms S and T can be expressed
either as
 S = T, the default mode, incorrect implementation of unification; or
 unify_with_occurs_check(S,T), correct implementation, inneficient.
- Now, it is
| ?- unify_with_occurs_check(X,f(X)).
no
| ?- unify_with_occurs_check(X,f(Y)).
X = f(Y) ? ; no
- It is up to the user to select the appropriate form. For example, the test or an
empty difference list L could be simply expressed as T-T. But if the list is not
empty, and containts n elements, then it takes the form
[a1, a2, ... , an | T] - T
in which case the default unification (without occurs check) would not work
properly, since it would try to unify T with [a1, a2, ... , an | T] .
10 October 2006
Foundations of Logic and Constraint Programming
30
Occurs Check in Prolog
- This behaviour can be observed with the rev_diff/2 predicate to reverse a
difference list
rev_diff(L-L,L-L). % incorrect version
rev_diff([H|T]-Z,X-W):- % according to diff_cat
Z \== [H|T],
% C=X, D=W if Y = [H|D]
rev_diff(T-Z,X-[H|W]).
leading to the following interaction
| ?- rev_diff0([1,2|T]-T,L).
L = [1,2,1,2,1,2,1,2,1|...]-[1,2,1,2,1,2,1,2,1|...],
T = [1,2,1,2,1,2,1,2,1,2|...] ? ;
L = [2,1|_A]-_A,
T = [2,1|_A] ? ;no
- If the first clause is written instead as
rev_diff(L-T,L-L):- unify_with_occurs_check(L,T).
then the correct behaviour is observed
| ?- rev_diff([1,2|T]-T,L).
L = [2,1|_A]-_A,
T = [2,1|_A] ? ;no
10 October 2006
Foundations of Logic and Constraint Programming
31
Exercises for the Week
- Solve exercises below from [Apt97], chapter 2
 2.1 (pag. 21);
 2.2 (pag. 21);
 2.3 (pag. 22);
 2.4 (pag. 24);
 2.5 (pag. 26);
 2.6 (pag. 33);
 2.8 (pag. 36);
- Optionally
 2.9 (pag. 37);
 2.10 (pag. 39);
10 October 2006
Foundations of Logic and Constraint Programming
32