[cl-unification-devel] newbie; questions on comutivity.

[Marco Antoniotti]

Hi

It is correct because what you see in Prolog systems you actually see  
one extra step in the process.

This is LW Prolog (SWIPl, arguably the most stable, free Prolog out  
there does the same).

======================

==> ?-

?- 42 = X.

X = 42;
NO.

?- t(42, A) = t(A, B).

A = 42
B = 42;
NO.

?- t(A, B) = t(42, A).

A = 42
B = 42;
NO.

?-
======================

When the variables are printed (or even during unification, but this  
makes things slower) the 'terms' (read: the 'variables') are  
"grounded".  I.e. all the substitutions are done and, in the second  
case the substitution for A is printed for B.

So, the choice is where to do the "grounding" of the terms.  I choose  
to leave it downstream.

The algorithm is nevertheless correct.   Check the following:

============================================================

UNIFY 10 > (unify '(?a ?b ?b) '(42 ?a 123))

Error: Cannot unify two different numbers: 42 123.
   1 (abort) Return to level 0.
   2 Return to top loop level 0.

Type :b for backtrace, :c <option number> to proceed,  or :? for other  
options

============================================================

If you inspect the environment in this debug level, you will see that  
the bindings are what you expect, and that (?B . ?A) appears among them.


To achieve what you expect you just need to add the proper call to  
APPLY-SUBSTITUTION to the binding of ?B.

Having said that, the current definition of APPLY-SUBSTITUTION is  
incomplete/buggy.  But I just fixed it to work in your example. I will  
put it in CVS ASAP.

Cheers
--
Marco






On Apr 16, 2009, at 06:22 , Matthew D. Swank wrote:

> As someone exposed to unification through languages like prolog and
> kanren, I'm a little puzzled as to why the following doesn't seem to
> commute:
> CL-USER> (let ((e (unify '(42 ?a) '(?a ?b))))
>           (values (v? '?b e) (v? '?a e)))
> 42
> 42
> CL-USER> (let ((e (unify '(?a ?b) '(42 ?a))))
>           (values (v? '?b e) (v? '?a e)))
> ?A
> 42
> CL-USER>
>
> If this is correct behavior, could someone explain it to me?
>
> Thank you,
>
> Matt
>
> -- 
> "You do not really understand something unless you can explain it to
> your grandmother." -- Albert Einstein.
>
> _______________________________________________
> cl-unification-devel site list
> cl-unification-devel at common-lisp.net
> http://common-lisp.net/mailman/listinfo/cl-unification-devel

--
Marco Antoniotti