
592
Lassez,
Mäher,
and
Marriott
the set of variables appearing in
t
v
...,t
n
.
An element v
f
— t
i
of a substitution
is called a binding.
Substitution θ is a grounding substitution if its right hand side (rhs) consists
of ground terms. It is a grounding substitution for W if its domain is W. For
example,
{JC
— a,y — f(a)} is a grounding substitution for
{x,y}.
A solution, Θ, of equation set Ε = {s
Y
=
t
x
,...,s
n
= t
n
} is a grounding sub-
stitution for V such that = ^θ,.,.,^θ = r
n
6. For example,
{JC
g(a), y—
g(a),
ζ — g(g(a))} is a solution of {f(x, z) = f(y, g(y))}. The (possibly
empty) set of solutions of equation set Ε is denoted by soln(E). It