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
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@common-lisp.net http://common-lisp.net/mailman/listinfo/cl-unification-devel
-- Marco Antoniotti
cl-unification-devel@common-lisp.net
-
Marco Antoniotti -
Matthew D. Swank