This algorithm presentation is indeed pedagogically unclear.
I will not repeat here the previous contributions. However, I believe
some points need clarification. Sorry if some of it is a bit subtle:
this program is far from being pedagogically written. I am thinking in particular of the presentation of the function UNIFY-VAR
which is analyzed below.
First one should note that we have two languages here, both with variables and constants, which may lead to much confusion if one is not very careful in the terminology. Hence my somewhat verbose presentation:
the object language defining the expressions being unified
the programming language which is a meta-language for the
object language, and in which the unification algorithm is expressed.
Regarding the object language
Apparently the OP could not find in his book the definition of the
object language, and hence did not know what a compound expression
may be. I do not have the book to check and can only guess. But it is
quite abnormal to give a unification algorithm without a reference to
a precise definition and terminology of the object language in which
unification is defined. There are many such object languages, and
unification may depend on them and their properties.
In this case my guess is that compound expression stands for an expression
composed of an operator and its operands. So if the metavariable x
has a compound expression as value, then x.OP
is the operator while
x.ARGS
is the list of its arguments.
But then we do not see anywhere what unifies operators. The
explanation is probably, as indicated by Yval Filmus in a comment,
that operators are treated as constant. Actually, as far as I know,
the habit is more to say that constants are operators without
arguments. But indeed, both can be treated in the same way. But again,
being explicit about it would not hurt the pedagogy, since few
students are used to treat the +
symbols as a constant, for example.
To conclude, the object language is just a language composed of
expressions, where an expression is either an atomic expression,
i.e. a constant or a variable, or a compound expression that applies
an operator (given by its name) to a list of arguments which are
expressions.
The name compound expression is in this context opposed to atomic
expression. The former has to be decomposed for unification, while
the latter cannot be decomposed.
About the function function UNIFY-VAR(var, x, theta) returns a substitution
First note that the value of the argument var
is always an object
variable, while the value of x
is always an object expression (which
could be reduced to a variable).
The use of if {var/val} E theta
here is a strange thing to do when
describing a unification algorithm for the object language, since it is implicitly using
unification at the programming language level, and in a strange way.
In the pair {var/val}
var
stands for the value of the meta-variable (i.e. programming
language variable) var
, i.e. for the object variable passed as
argument. This object variable is a constant from the meta point of view
of the programming language.
val
stands for itself, as a meta-variable: it was not assigned any
value, and thus can hardly be expected to stand for its value.
the pair {var/val}
is just a meta compound expression, a construction,
involving the pair operator, a constant (the value of var
), and the
variable val
, at the meta level of the programming language.
The use of if {var/val} E theta then do X
is actually intended to say, but at
the meta level:
if the meta expression {[var]/val}
unifies with an element of theta
, then do X.
where I insist again with the notation [var]
that the variable var
is replaced by its value,
while val
is not (and acts somewhat as what Prolog calls a logical variable).
Furthermore it does have a side effect: when the unification succeeds,
then the variable val
takes the value of the second component of the
substitution pair with whch it actually unified. And this value is to
be used in whatever is to be done, in this case return UNIFY(val, x, theta)
.
So this is not at all trivial. Furthermore, it is pedagogically unwise (to understate it),
when teaching beginners, since it is using unification at the
programming level to define unification at the object level.
Note that is no unification succeeds in the above test, the variable
val
remains undefined. Then the next test if {x/val} E theta then ...
is again a unification, slightly more complex, since the meta
variable x
is not necessarily a variable, though it will unify only
if it is one.
In the last line the construction {var/x}
is used again, but in this
case, both variables stand for their values.
So again, reading this piece of programming is a bit subtle, at least
for a beginner. It do not mean it is nad programming, only that it
mixes too many concepts and levels from a pedagogical point of view.
Occur-check
Finally, I do hope you understand what the call to OCCUR-CHECK?
is
supposed to do, because it is an essential part of the algorithm.
Essentially it is suppose to verify that when you try to unify a
variable with an expression that the variable does not appear in the
expression (allowing it would correspond to looping structures that
are not usually allowed in the language).
Note that in the call to [OCCUR-CHECK][1]?(var, x)
in your program, the
meta-variable var
is supposed to have as value an object variable, and the meta-variable
x
is supposed to have as value an object expression, and the
function will check that the object variable does not occur in the
object expression.