🚀 go-pugleaf

Gert Smolka writes:
> I seriously doubt that rational tree unification pays any significant
> efficiency penalties in practise over Edinburgh-style unification
> without occurs check.  As has been mentioned by Torkel before,
> UNIFICATION IN SICSTUS IS RATIONAL TREE UNIFICATION, and Sicstus seems
> to be rather efficient.
to which Fernando Pereira replies:
> I don't know what "rather efficient" means without actual numbers to
> back it up. 

Fernando Pereira is too cautious: SICStus and ProLog by BIM have chosen to
support unification of cyclic terms and they are more efficient than most
other systems that have no support for unification of cyclic terms, neither
- systematic - occurs check. If any Prolog system is worth being named "rather
efficient", it is them.
A Prolog system by Siemens has chosen for occurs check. Perhaps Christian
Pichler can comment on that: last time I talked to him, he said that the
overhead was quite small. Also the Siemens system is faster than the average
Prolog system.

again Gert:
> However, given the efficiency and
> the clean *logical* status of rational tree unification, I would expect
> that rational tree unification is taken as default and finite tree
> unification is accommodated as a built-in predicate
to which Fernando Pereira replies:
> .he reason is that the efficiency issues mentioned above have not
> been addressed to everyone's satisfaction.

I think rather the following: the reason why the forthcoming standard does not
require either occurs check or rational tree unification, is partly that some
implementors fear the implementation cost (they are right: the cost will not be
paid back by costumers) and partly that choosing between rational trees and
occurs check is next to impossible for the ISO committee (remember how long it
took for deciding about the database update view).
The nice thing about what the current draft of the standard now requires, is
that in order to keep the property that 2 unifications commute, implementors
should commit to rational trees or occurs check and never have undefined behaviour.

Supporting rational tree unification is easy. The tedious (and also fun) work
comes when one tries to make the built-in predicates behave sensibly when they
are called with cyclic terms. As far as I know, IBM Prolog did a good job at
this. In ProLog by BIM, the bag returned by bagof/3 can contain cyclic terms
(e.g. ?- bagof(X,X = f(X),L)) and the record predicates can store and retrieve
cyclic terms; numbervars/3, ground/1, copy_term/2 etc deal sensibly with
cyclic terms. And the others will follow (for some of them - like assert - it
will depend on options set by the user what happens exactly). But we don't
plan (at the moment) to have an external syntax for them like in IBM Prolog.
Cyclic bindings are shown at the toplevel as follows:

	?- X = f(X) .
	  X = f(X)

which is just the generalisation of showing the sharing even in the non cyclic
case, as in

	?- Y = [1,2,3] , X = f(Y,g(Y)) .
	  X = f(Y,g(Y))
	  Y = [1,2,3]

which is a bit more useful than

	?- Y = [1,2,3] , X = f(Y,g(Y)) .
	  Y = [1,2,3]
	  X = f([1,2,3],g([1,2,3]))

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.

Fernando again:
> I would be happy it it were shown *over a well-chosen mix of programs*
> that the overhead in question is negligible. But I've not seen such
> a demonstration. 
Depending on what exactly one wants to accept as a well-chosen mix of programs,
Peter Van Roy's thesis (or paper) on the Aquarius system, contains some useful
figures:  he compares the Aquarius system with BIM (with rational trees) and
Quintus (no rational trees, neither occurs check).

Bart Demoen