Home > Archive > Prolog > March 2008 > Unification
You are viewing an archived Text-only version of the thread.
To view this thread in it's original format and/or if you want to reply to
this thread please [click here]
|
|
|
| Hello, I have a question about algorithm of unification.
When we unify two predicates p(x_1,...,x_n) , p(y_1,..,y_n)
there is a step:
//.....
if x_i is a variable, y_i is a complex term and x_i is not a subterm
of y_i
then add x_i=y_i to substitutions.
//.....
else
p(x_1,...,x_n) and p(y_1,...,y_n) are not unifable.
But what if x_i IS a subterm of y_i
why can't we unify two expressions?
For example, let's consider an example.
q(u,v):-p(v,u,f(v,u)).
p(x,y,x).
let's unify p(x,y,x) and p(v,u,f(v,u))
We'll get
1. substitutions={x/t1, v/t1}, p(t1,y,t1), p(t1,u,f(t1,u))
2. substitutions={x/t1, v/t1, y/t2, u/t2} p(t1,t2,t1),
p(t1,t2,f(t1,t2))
3. Why can't we say, that on condition f(t1,t2)=t1 these two
predicates are unifable?
Can we expand the first rule of the program to
q(t1,t2):-p(t1,t2,f(t1,t2)),f(t1,t2)=t1 ???
| |
| Bart Demoen 2008-03-14, 8:13 am |
| alp wrote:
> Hello, I have a question about algorithm of unification.
>
> When we unify two predicates p(x_1,...,x_n) , p(y_1,..,y_n)
> there is a step:
Just a small thing about terminology: we don't unify predicates.
We unify terms, or the head of a predicate clause with a goal.
> 3. Why can't we say, that on condition f(t1,t2)=t1 these two
> terms are unifable?
Logic is usually about finite terms, and unification is about finding
and applying a variable substitution that makes two terms
syntactically equal.
In that framework, the unification of X with f(X) cannot work, ie.
you can't find a finite term to replace X with so that X and f(X)
(after the replacement) are syntactically equal terms.
The "occurs check" in the unification is there to detect that failure
of the attempt to unify.
The occurs check is expensive, at least, in general. So many Prolog
systems don't do it. Several things can happen if you enter
X = f(X).
as the toplevel goal of a Prolog system:
- loops endlessly without any output
- prints f(f(f(f(f(f(f(ff(f(f(f(f(f(f(f(f(f( [lots of them] followed
by Segmentation fault
- prints X = f(f(f(f(f(f(f(f(f(f(...))))))))))
- ...
So what is happening: one can find an infinite term to substitute X
for, so that X and f(X) become equal - some systems have trouble
"constructing" the infinite term; some can represent it, but cannot
print it; some deal with it in a very nice way, almost all the time
(even in assert, findall, sort ...)
ISO allows Prolog systems to deal with infinite terms, but also
imposes Prolog systems to have a built-in unify_with_occurs_check/2,
so that
?- unify_with_occurs_check(X,f(X)).
fails.
Why does classical logic deal only with finite terms ?
As an example, if you define some reasonable axioms about Peano
arithmetic, and then allow infinite terms, you will be able to
conclude that 1 == 0, or something equally bad :-)
(I only vaguely remember that example from a paper by Mark Stickel,
mid 80ties - if someone feels like reconstructing it, please do).
Cheers
Bart Demoen
|
|
|
|
|