🚀 go-pugleaf

Bart Demoen writes:
> Supporting rational tree unification (and conservation of sharing during
> some built-in predicates - which is a consequence of fully supporting cyclic
                                        ^^^^^^^^^^^
> terms) can actually speed up some programs quite a lot.

WEll, Well, well.  I like to be shightly more precise and show that
rational term unification and conservation of sharing are rather
independent.

The minimum that rational tree unification must do is to remember
every pair of equivalent terms in the current branch of the current
unification problem.  It will not buy you much conservation of
sharing.  The maximum it can do is to remember every pair of
equivalent terms in the current branch of the search-tree.  This will
buy you the maximum conservation of sharing.

In this context, "equivalent" means "made equivalent by unification".
Those terms that are equivalent without the help of unification may
well never be recognised as equivalent.

One might want to stick to the minimum for avoiding special trailing
and backtracking operations for handling the storing and unstoring of
equivalent pairs, and to benefit from the recursive control of
unification.  However, modern Prolog implementations already have
these special operations (for handling contraints, term rewriting or
whatever ...).  It would be rather mean of these implementations not
to give the maximum.

Note also, that remembering pairs of equivalent terms in the current
branch of the search-tree is also feasible and usefull for finite term
unification.  It improves memory representation and unification (if it
is smart enough to detect physically equal terms).

Moral: rational term unification and conservation of sharing are
rather independent issues.  Even if they use similar techniques.

Hoping it helps,

Olivier Ridoux