Monday, January 19, 2009

Ch2, Ex13

From the algorithm given in the book its clear that unification is a symmetric operation, so whatever order we follow; following is the resulting set of bindings:
X = Y = [a b]
W = a
Z = b

it can also be confirmed from mozart system by executing following

local X Y W Z in
% try different order of unifications
X = [a Z]
Y = [W b]
X = Y
% No matter what the above sequence is, following sequence
% always prints
% true
% [a b]
% a
% b
{Browse X==Y}
{Browse X}
{Browse W}
{Browse Z}

No comments:

Post a Comment