Unification and Freshness

$\alpha$Prolog provides two special built-in predicates, $=$ (unification) and $\mathrel\char93$ (freshness). For example, unification for ground terms is just syntactic equality:

?- 1 = 1.
Yes.
?- 1 = 0.
No.

Free variables can be instantiated to terms to solve the equations:

?- 1 = X, X = Y, Y = Z.
Yes.
X = 1
Y = 1
Z = 1
?- X = 1, Y = plus X 0, Y = X.
No.

In the last query, the "Y = X" subgoal fails because "plus 1 0" is syntactically different from "1".

Freshness tests are a propositions of the form a # T, where "a" is a name and "T" is a term. They test that the name "a" does not occur free in "T" (that is, all occurrences are enclosed by an abstraction of "a".) Any two syntactically different names are assumed to be distinct (in contrast to logic variables, which might eventually be identified through unification.) For example,

?- a # a.
No.
?- a # b.
Yes.
?- a # b\a.
No.
?= a # b\b.
Yes.
?- a # a\a.
Yes.
?- a # (a~b) a.
Yes.

As the last example illustrates, freshness checking occurs after any transpositions have been applied.

Testing whether terms involving abstractions are equal is more complex than ordinary first-order unification such as Prolog uses. For example:

?- x\y\(X1,y) = y\x\(x,X1).
No.

?- x\y\(X2,y) = y\x\(x,X3).
Yes.
X2 = x
X3 = y

The results of unification can contain delayed permutations as well as additional freshness constraints.

?- x\X = y\Y.
Yes.
X = (x~y)Y

?- x\X = y\X.
Yes.
x # X.
y # X.

?- x\y\(y,X6) = x\x\(x,X7).
Yes. 
X6 = (x~y)X7
y # X7

In the last example, if "X7" were instantiated to "y", then we would have x\y\(x,x) = x\x\(x,x), but the "x"'s in the first term are bound to the outer "x" whereas in the second term they are bound to the inner "x".

Similarly, freshness tests of non-ground terms might generate new constraints.

?- x # x\Y.
Yes.
?- x # y\Y.
Yes.
x # Y
?- x # y\Y, x = Y.
No.