Gabriel@ANL-MCS.ARPA (01/24/84)
From: Gabriel@ANL-MCS.ARPA (John Gabriel)
The outcome of a friendly challenge from our resolution based theorem
proving community is appended. I am not completely satisfied with it,
for reasons that may be only that I would have liked to find a proof
more in the style of resolution without writing a mini-resolution
system in Prolog. It was originally posed in connection with the
occurs check (which looks out for attempts at
eq(X,X). /* unification */
eq(f(X),X). /* this succeeds and it is not clear to me whether this
prevents a successful resolution system in Prolog */ )
An occurs check causes the above to fail, and makes Prolog
unification more like the one the logicians prefer.
A couple of thoughts. eq(f(X),X) essentially defines f(X) recursively
but it is not recursively evaluable. Thus if f(X) is evaluated by
Prolog the evaluation will not terminate. Is this strong enough for
the "real" unification (I.e. that preferred by logicians), or do we
need more. The practical objection to the occurs check is that it
slows Prolog down a fair amount, and if Prolog is viewed not so
much as a logic system, but as an evaluator of recursive functions
with a flavour of logic thrown in, it seems unnecessary.
However, I don't pretend to know the truth about all this, and would
not be surprised by a storm of brickbats from all sides. But I'm
always willing to learn. Here is the "proof".
/* ************************************************************ */
/* A group of order 2 is commutative */
/* ************************************************************ */
/* the product X * Y * Z * ... is [X,Y,Z,.....] */
eq(X,X):- !. /* equality */
p([X,e],[X]):- !. /* the next two are identity */
p([e,X],[X]):- !.
p([X,X],[e]):- !. /* order 2 */
p([a,b],[c]). /* There exist a & b, and they have a product c */
/* the next four clauses express assocaitivity for any product,
the first two terminate the recursion of the second two */
p([X,Y,Z],[R]):- p([X,Y],[T1]),p([T1,Z],[R]).
p([X,Y,Z],[R]):- p([Y,Z],[T1]),p([X,T1],[R]).
p([X,Y|List],[R]):- p(List,[T1]),p([X,Y,T1],[R]).
p([X|List],[R]):- p(List,[T1]),p([X,T1],[R]).
equal(M1,M2):- /* An expression for identity of products */
p(M1,R),p(M2,R).
test1(R):- p([a,b,a,b],R). /* should set R=[e] */
test2(R):- p([a,b,b,a],R). /* also sets R=[e] */
/* Thus [a,b,b,a] = [a,b,a,b] */
/* but how do we define equal to discover [a,b] = [b,a] */
/* search for equality, [X|T] is list of possible multipliers */
/* this generates the tests that would be done automatically
by the set of support strategy */
search([], M1, M2):- equal(M1,M2).
search([X|T], M1, M2):-
equal(M1,M2);
search(T,[X|M1], [X|M2]).
test:- search([a,b], [a,b], [b,a]).
test:- search([b,a], [a,b], [b,a]). /* must try both orders of
multipliers */
-- John Gabriel