schuetze@csli.Stanford.EDU (Hinrich Schuetze) (01/16/90)
Does anyone know a good description of the unification algorithm used in prolog II? I'm interested in how circular structures are dealt with. Thanks a lot! Hinrich
Duchier-Denys@cs.yale.edu (Denys Duchier) (01/17/90)
In article <11740@csli.Stanford.EDU>, schuetze@csli (Hinrich Schuetze) writes: > Does anyone know a good description of the unification > algorithm used in prolog II? I'm interested in how > circular structures are dealt with. > > Thanks a lot! > > Hinrich If memory serves, they keep a stack of equations during unification. Think of them as assumptions. Whenever, they are about to unify 2 trees they first check the stack of assumptions; if the two trees have been postulated equal, the recursive call succeeds immediately; otherwise, they enter a new equation in the stack postulating that the 2 trees are equal, then proceed with regular unification (think of the subsequent computation as either showing the set of assumptions to be inconsistent, in which case it fails, or returning a unifier if it succeeds). It's a bit sketchy, but you get the general idea... --Denys
ridoux@calypso.irisa.fr (Olivier Ridoux) (01/17/90)
PrologII's terms are rational infinite terms. Rational means that though
infinite they have only a finite number of *different* sub-terms.
Consequently, they can be represented by finite circular structures. A term
may have many different representation (depends on how folded/unfolded it is).
The trick for unifying them is to make the number of different sub-structures
diminish along unification process.
--- An algorithm for unifying rational infinite terms.
Notations:
s:t is the term t represented by the structure s
a <- b is the assignment of the value of b to a
[a/b]c is the replacement of a by b in c
<a,b> is the elementary substitution of a to b
Id is identity function
o is function composition
(a,b) is a disagreement pair (to be unified)
D is the disagreement set memory
U is union
+ is disjoint union
S is the solution substitution memory
s1:t1 and s2:t2 are the two rational infinite terms to be unified
=t= is equality on terms (true only for equal atoms)
V is the set of logical variable
INIT D <- {(s1:t1,s2:t2)}, S <- Id
LOOP if D={} then goto SUCC
else let D = {(sx:tx,sy:ty)} + D'
(1) if sx = sy then D <- D' ; goto LOOP
(2) elif tx =t= ty then D <- D' ; goto LOOP
elif tx in V
(3) then S <- S o <sy:ty,sx:tx>, D <- [sx:tx/sy:ty] D' ;
goto LOOP
elif ty in V
(4) then S <- S o <sx:tx,sy:ty>, D <- [sy:ty/sx:tx] D' ;
goto LOOP
else let tx = fx (tx1, ... , txn)
ty = fy (ty1, ... , tym)
if fx = fy
then let f = f1 /* = f2 */
p = n /* = m */
(5) D <- [sx:tx/sy:ty] (D' U {(sxi:txi,syi:tyi)|i in [1,p]})
goto LOOP
else goto FAIL
fi
fi
SUCC success, the minimal unifier is in S
FAIL failure
Comments:
Either D diminishes (1,2,3 and 4) or the number of different
sub-structures (5).
The replacement in (5) can be represented as a substitution; then unifying two
terms make them physically equal.
The replacement in (5) can remain local to the unification procedure. It may
even be local to the unification of the (sxi:txi,xyi:tyi)'s.
The replacement in (5) has the nice property that if its life-length is the
whole computation it makes unification almost linear.
The algorithm is closely related to FSA comparison. It gives the main
lines for efficient first-order unification. It also gives the
main lines for unifying Ait-Kaci's psi-terms (TCS (45) '86, JLP (3) '86).
Olivier Ridoux
ridoux@irisa.fr
IRISA, Campus Universitaire de Beaulieu, 35042 RENNES CEDEX, FRANCE