🚀 go-pugleaf

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