Re: LISPPA

From: Alexander Baranovsky (ab_at_cable.netlux.org)
Date: 05/10/04 

Date: 10 May 2004 03:03:21 -0700

Thomas Schilling <tjs_ng@yahoo.de> wrote in message news:<opr7qix7ddtrs3c0@news.CIS.DFN.DE>...
> Alexander Baranovsky wrote:
> > http://www.cs.bham.ac.uk/research/poplog/paradigms_lectures/lecture20.html#unification
> >
> > which describes the unification algorithm in Scheme. I guess that
> > Peter Norvig's book presents the same idea of unification.
>
> > 1. I do not use the binding list. The bindings are expressed by means
> > of aliases in my approach. Ok, I use extra structure which contains
> > parameters of term, but this approach provides the linear algorithm of
> > renaming variables.
> > 2. I do not use search in the binding list.
> > 3. I use one function Unify instead of two functions: unify and
> > unify-variable.
> > 4. I do not use the mutual recursion (of unify and unify-variable) in
> > my algorithm, so it is much more easy to get a non-recursive version
> > of the algorithm.
> > 5. My algorithm is more concise and easy for understanding.
>
> Here's the version from Norvig's compiler:
>
> (defstruct var name (binding unbound))
> ;; in pascal this is like:
> ;; type
> ;; Var = record
> ;; name: ?;
> ;; binding: ^var; (* default value = unbound *)
> ;; end;
>
> (defun bound-p (var) (not (eq (var-binding var) unbound)))
> ;; (var-binding var) would be var.binding
>
> (defmacro deref (exp)
> "Follow pointers for bound variables."
> `(progn (loop while (and (var-p ,exp) (bound-p ,exp))
> do (setf ,exp (var-binding ,exp)))
> ,exp))
> ;; this is a macro, although in this case you can
> ;; remove all the "`" and "," and consider it as a function
> ;; being inlined in the actual code
>
> (defun unify! (x y)
> "Destructively unify two expressions"
> (cond ((eql (deref x) (deref y)) t)
> ((var-p x) (set-binding! x y))
> ((var-p y) (set-binding! y x))
> ((and (consp x) (consp y))
> (and (unify! (first x) (first y))
> (unify! (rest x) (rest y))))
> (t nil)))
>
> (defun set-binding! (var value)
> "Set var's binding to value. Always succeeds (returns t)."
> (setf (var-binding var) value)
> t)
> ;; (setf (var-binding var) value) means var.binding := value;
>
> So, now concerning your remarks:
> 1) thesame (see the macro)
> 2) thesame
> 3) thesame
> 4) thesame. also: recursion must not be bad
> 5) well, that's a matter of taste (and getting used to).

Please let me explain why I'm not quite agree with you. The key of the
problem is the different representation of bindings. In the Lisp
program, the bindings are represented as an associative list which
contains pairs (variable, value). In my approach the binding expressed
by means of alias, so the variable is just an alias of value. It
contains address of the value in the implementation. So, my approach
is a bit less expensive regarding the memory amount and it promises
more fast work because the search of variable in the binding list is
not necessary.

Let's assume, we have two terms:

t1 = L(x, x)
t2 = L(f(y), f(a))

I represent these terms as

t1 = [L, PX, PX]
t2 = [L, [F, PY], [F, A]]

where PX and PY are parameters of terms t1 and t2 accordingly. PX and
PY are aliases of X and Y, so the terms "looks" as

t1 = [L, X, X]
t2 = [L, [F, Y], [F, A]]

in any expressions.

The line

 else if IsVar(T1[I]) and (not Inside(T1[I], T2[I])) then T1[I]^ := @
T2[I]^

of Unify function will assign X (parameter of t1, not actual item of
T1 !) as alias of Y, so now terms "look" like

t1 = [L, [F, Y], [F, Y]]
t2 = [L, [F, Y], [F, A]]

Please note, we have not made actual substitutions, we just executed
simple operation of creation of alias.

The Unify algorithm continues his work, now it consideres the third
item of t1 as a compound term [F, Y], not variable X. Once again, the
line

 else if IsVar(T1[I]) and (not Inside(T1[I], T2[I])) then T1[I]^ := @
T2[I]^

will assign Y variable as alias of A.

As you can see, the Unify function acts quite straightforward. At the
end of work we obtain that the terms "look" like

t1 = [L, [F, A], [F, A]]
t2 = [L, [F, A], [F, A]]

and the Unify function returns true. Note, the actual values of items
of t1 and t2 have not been changed, we did not actual substitutions.
But only parameters of t1 and t2 have been changed.

I'll answer the rest of your message later this day.

A..