Abbott@AEROSPACE@sri-unix.UUCP (07/20/83)
From: Abbott at AEROSPACE (Russ Abbott)
/*
Bill Kornfeld (see his paper referenced in an earlier Prolog Digest for
more details) has defined a nifty variant to Prolog that permits one to
state equality theorems to be used by the unifier when attempting to
apply predicates. In his implementation he modified his LISP-based
Prolog interpreter. Following is a version of the same capability that
runs in standard Prolog.
One problem we have found is that it is possible to build circular
structures, in which case the interpreter will loop forever. Other than
that, this approach seems to work successfully. No guarantee, however; we
have not tested it thoroughly. We offer it for your further development.
First an example program that shows how it may be used. Then the actual
Prolog clauses.
*/
example :-
le(X, Y), % Establish that X < Y, although
write('X = '), write(X), nl, % both are variables.
write('Y = '), write(Y), nl,
member(X, [3, 4, 5]), % Bind X and then Y. (Binding X first
member(Y, [3, 4, 5]), % is "harder" because as le is
write('X = '), write(X), nl, % written X is defined in terms of Y
write('Y = '), write(Y), nl, % rather than Y in terms of X.)
instantiate(X, X1), % Instantiate X, i.e., force it to
write('X1 = '), write(X1), nl, % take on an actual value, such
instantiate(Y, Y1), % as 3, 4, or 5, if possible.
write('Y1 = '), write(Y1), nl, % Instantiate Y.
write('At fail'), nl, % Backup and get other values for
fail. % first Y and then X.
/***********************************************************************
Here are le and member redefined so that they can make use of equality.
*/
le(X, Y) :- % If both arguments can be
instantiate(X, X1), % instantiated to integers, evaluate
instantiate(Y, Y1), % le with those values.
integer(X1),
integer(Y1),
!,
X1 =< Y1.
le(X, Y) :- % If one argument can be instantiated
instantiate(Y, Y1), % use it. Define the other in terms
integer(Y1), % of it. Read "omega(X, P)" as
!, % "a value X such that P holds."
equals(X, omega(Z, le(Z, Y1))). % (Presumably X appears in P.) So
% this sets X to "a value Z that
% is less than or equal to Y1."
le(X, Y) :-
instantiate(X, X1), % The same thing, but in terms of the
integer(X1), % other argument. (Actually this
!, % is not needed since the next is the
equals(Y, omega(Z, le(X1, Z))). % same.
le(X, Y) :- % Otherwise build a new omega
equals(X, omega(Z, le(Z, Y))). % structure that defines Y in terms
% of X.
/*
The traditional definition of member
member(First_Element, [First_Element, Rest_of_List]).
member(Element, [First_Element | Rest_of_List]) :-
member(Element, Rest_of_List).
is replaced by: */
member(X, Y) :-
structure(Y, [First_Element | Rest_of_List]),
equals(X, First_Element).
member(X, Y) :-
structure(Y, [First_Element | Rest_of_List]),
member(X, Rest_of_List).
/*
The translation may be performed automatically. All arguments are replaced
by new variables. Then, if an argument was initially a variable, such as
First_Element, set the new variable, I.e., X, equals to it, whence
equals(X, First_Element), in the first clause of member. If the original
argument was a structure, such as the list structures, use structure to
require that the new argument be a structure of the same form. */
/********************************************************************
Now here are the definitions of equals and the supporting predicates. */
equals(A, Y) :-
structure(A, omega(X, P)), % If A is an omega structure in X,
instantiate(Y, Z), % and if Y can be instantiated to the
!, % value Z, then Z is a valid value for
equals(X, Z), % A if P holds on Z.
P.
equals(Y, A) :-
structure(A, omega(X, P)), % Same thing, but with
instantiate(Y, Z), % the arguments reversed.
!,
equals(X, Z),
P.
equals(A, B) :-
structure(A, omega(X, P_1)), % If A and B are both omega structures,
structure(B, omega(Y, P_2)), % compose them, i.e., require that both
!, % P_1 and P_2 hold.
Y = A.
equals(A, B) :- % Two structures are equal if their
nonvar(A), % components are equal.
nonvar(B),
functor(A, F, N), % They must have the same functor and
functor(B, F, N), % the same number of arguments.
A =.. [F, A_1 | A_Rest], % Structures with no arguments are
B =.. [F, B_1 | B_Rest], % atoms.
!,
equals(A_1, B_1),
equals(A_Rest, B_Rest).
equals(X, X) :- % If all else fails, use standard
!. % unification.
instantiate(Thing, Thing) :- % If Thing is instantiated,
instantiated(Thing). % return it unchanged.
instantiate(Thing, Value) :- % If Thing is an omega
structure(Thing, omega(Value, P)), % structure, with Value as
P, % its local variable, evaluate
instantiated(Value). % its predicate P. If that
% succeeds, return (the
% resulting) Value as Thing's
% instantiation.
instantiated(X) :- % If Thing is not a variable
nonvar(X), % and not and omega structure,
not functor(X, omega, 2). % it is already instantiated.
structure(X, Y) :- % Succeeds if X is a structure of
nonvar(X), % the form Y.
X = Y.