SHardy%SRI-KL@sri-unix.UUCP (07/18/83)
An earlier message asked how to define a predicate EQUAL on two terms
that didn't mind if variables were renamed but otherwise wanted the
terms to be identical, thus:
equal(A + B, C + D), equal(A + A, C + C)
are true, but not:
equal(A + A, B + C)
The proposed ``quick and dirty'' solution was something like:
equal(X, Y) :- assert(temp(1, X)), assert(temp(2, Y)),
retract(temp(1, A)), retract(temp(2, B)),
numbervars(A, 1, N), numbervars(B, 1, N),
A = B.
A ``better'' (I.e. faster) solution is:
equal(X, Y) :- \+notequal(X, Y).
notequal(X, Y) :- \+notnotequal(X, Y).
notnotequal(X, Y) :- numbervars(X, 1, N),
numbervars(Y, 1, N), X = Y.
This is ``better'' because it doesn't use ASSERT. It's best to avoid
Assert because:
* It is slow - it has to copy the structure being asserted.
* On the DEC-20, it consumes memory until the procedure doing
the ASSERT is backtracked over - not just until the item is
RETRACTed. This might be for the ENTIRE computation.
A useful heuristic is that predicates that side-effect their arguments
in undesirable ways (eg by using NUMBERVARS) can sometimes be rendered
safe by enclosing them in a double negation.
-- Steve Hardy,
Teknowledgeok@edai.UUCP (07/30/83)
Steve Hardy's solution to the term isomorphism problem is only
correct when you can guarantee in advance that the two terms don't
contain variables. With pointless predicates removed, his solution was
isomorphic(T1, T2) :-
\+ \+ (
numbervars(T1, 1, N),
numbervars(T2, 1, N),
T1 = T2
).
But consider T1 = f(X,Y), T2 = f(Y,X). According to all the
definitions in theorem-proving texts and aritcles I have ever seen,
these two terms are equal up to renaming of variables. However,
numbervars(T1,1,N) binds N to 2 and instantiates T1 to f($VAR(1),
$VAR(2)). Then numbervars(T2, 1, N) fails, because T2 no longer
contains any variables.
A while back I posted a file METUTL.PL of "meta-logical" utilities
to net.sources, it contained a predicate variant/2 which I believe to be
a correct solution to thise problem. If anyone finds a bug in it, do
let me know.
Here is another solution, which attacks the problem directly. (Why
can't people tackle problems like this from first principles? This is
an EASY one!)
There are four cases to consider.
T1 T2
var var we have to match the two variables somehow.
var nonvar non-isomorphic
nonvar var non-isomorphic
nonvar nonvar isomorphic iff they have the same principal functor
and corresponding arguments are isomorphic.
As for matching the variables, it is a bit like unification, except that
we don't want to bind anything. So we have to keep a mapping for each
term which says what each variable in that term is matched with. Note
that X (occurring in T1) may be matched with Y (occurring in T2), while
X (occurring in T2) may be matched with Z (occurring in T1). Each
variable will be matched with precisely one variable in the other term.
So let's start by defining a data structure and predicate for doing this
matching. The simplest possible structure is a list of pairs of
variables, so let's pick that until forced to do otherwise, and the
simplest way of extending it is to leave the tail unbound, and to
further instantiate it. So
match(V1, V2, [Match|_]) :-
var(Match), % we're at the end of the list
!, % neither X nor Y bound before
Match = V1-V2. % so extend map
match(V1, V2, [X1-X2|_]) :-
X1 == V1, % we've found the match for V1
!, % and there can only be one
X2 == V2. % check that it is V2
match(V1, V2, [X1-X2|_]) :-
X2 == V2, % we've found the match for V2
!, % because of the previous clause
X1 == V1. % this test must fail
match(V1, V2, [_|Matches]) :-
match(V1, V2, Matches).
And now we're pretty nearly finished:
isomorphic(T1, T2) :-
isomorphic(T1, T2, Matches).
isomorphic(T1, T2, Matches) :-
var(T1),
!,
var(T2),
match(T1, T2, Matches).
isomorphic(T1, T2, Matches) :-
nonvar(T1),
nonvar(T2),
functor(T1, Functor, Arity),
functor(T2, Functor, Arity),
isomorphic(Arity, T1, T2, Matches).
isomorphic(0, _, _, _) :- !.
isomorphic(N, T1, T2, Matches) :-
arg(N, T1, Arg1),
arg(N, T2, Arg2),
isomorphic(Arg1, Arg2, Matches),
M is N-1,
isomorphic(M, T1, T2, Matches).
And there you are. Steve Hardy's solution is cheaper when the
terms don't share variables, as it doesn't have to do a linear search on
every variable. But then it doesn't work in the general case, and if
you want the substitution which makes the two terms identical you pretty
well have to do something like this. The really nice thing about this
definition is that producing it requires essentially NO thought, you
just go STRAIGHT from the definition, and don't have to know about
tricks with the data base or numbervars. (You DO have to know about
var, nonvar, functor, arg, and the distinction between = and ==, but
then you have to be pretty thoroughly at home with them before you can
risk writing metalogical code anyway.) To show you just how easy it was
to write this, I just typed it straight down while composing this
message. I did call Prolog from the editor to check that my solution
works, which it appears to do.
Richard O'Keefe
ok!edai!ukc!...
OKeefe.R.A.@Edxa@Ucl-Cs@Isi-D