Subject: Re: representing terms canonically

From: Paul Singleton <[email-masked]>
Date: Fri, 18 Aug 2000 22:44:40 +0100

[I want to export terms from Prolog with:]

>          * no loss of information
>             + an equivalent term should be reconstructable from the foreign repn.
>               (I can do this :-)
>             + preserve internal order of any variables (I can see how to do this)
> 
>          * compactly
>             + cyclic terms have finite representations
>             + recombinant terms are not "exploded"
>             + common atoms, variables (of course) and subterms are factored out
> 
>          * canonically
>             + all (inc. cyclic) terms denoting the "same" term (apart from renaming
>               of variables) have a single common representation

RAO'K has proposed a computable canonical repn of cyclic terms (thanks),
and I'm working my way towards it, although I'm not confident of my
competence to implement it...

Meanwhile I've hit a problem with achieving some other requirements (above).

While traversing a term, I maintain a list of "ancestor" terms (those on the
path from the "top" of the term to the subterm under consideration), and I also
accumulate a list of all compound terms (including atoms) met so far.

I aim to detect cycles by checking whether the subterm-under-consideration
occurs on the path-from-the-root (and, less importantly but desirably, to
factor out common subterms by checking whether it occurs among the
compound-terms-seen-so-far).

I note (empirically) that ==/2 succeeds when comparing a cyclic term with
itself, which is half of what I need, but (understandably) it doesn't
terminate when comparing some cyclic terms which don't "match up", e.g.

  T1 = f(f(T1)),
  T2 = f(T1),
  T1 == T2.

T1 and T2, although identical, can never be found to be identical by ==/2,
as their f/2 nodes are forever out-of-step.

So when checking for cycles in T1, where T1 = f(f(T1)), my code nonterminates
(and runs out of stack) when it tries to compare the "second-level" f/2 with
the first (I want it to fail, and succeed at the third level).

What I think I need, is a (distinctly non-logical :-) term comparison which
immediately (without any recursive searching) reports whether two terms are
the same actual compound "cell" (or whatever Prolog implementors call it).

If there's a way to terminatingly detect cycles within terms with the usual
builtins, I'm afraid I can't see it.

I'm happy to implement this as a foreign function, but I don't know how to
look beyond the term_refs to get at e.g. the addresses of the storage
allocated for a compound...

Once I've got my "model" (Prolog) implementation working, I'll consider what
data structures are most efficient (for whatever I assume about the likely
profile of terms to be exported).

But I want safety first (this is a general-purpose conversion for writing
arbitrary terms to a database, or sending them to another Prolog system,
etc., and it must always terminate, 'cos I can't guarantee that the apps
which use it won't produce cyclic terms inadvertently or deliberately).

Paul Singleton