🚀 go-pugleaf

In article <1992Jul16.072806.8333@ecrc.de>, joachim@ecrc.de (Joachim Schimpf) writes:

> However, if one insists on comparing variables (is there actually a
> convincing application for it?),

What's a good way to represent sets of (possibly non-ground) terms in a setting
where terms are regarded as identical if they are variants of one another?  (Two
terms are variants of one another if each is an instance of the other, i.e. if
one is obtained from the other by "systematically" renaming variable.)  For
ground terms, a convenient and efficient way to represent sets is as sorted
lists without duplicates.  Doing something like this for non-ground terms may
involve comparing variables.

If variable-name correspondence between terms in the set is not important, a
solution is to independently numbervars each term, thereby reducing each to a
canonical ground form.  This would be the case, for example, for a set of
clauses.

But if variable-name correspondence between terms in the set _is_ important, as
for example if it's a set of atoms within a clause, this device will not work.
For example, the equivalence of the sets
		{p(X, a), p(Y, b)} and
		{p(U, b), p(V, a)}
does not seem to be easily detectable.

-- 
        Relations among people to be by mutual consent, or not at all.
         ---John E. Kreznar, jkreznar@ininx.com, uunet!ininx!jkreznar