🚀 go-pugleaf

In article <24435@alice.att.com>,
pereira@alice.att.com (Fernando Pereira) writes:
|> If you want to program with cyclic terms, you have gone outside
|> bare first-order logic to a system in which terms are interpreted
|> in a different way. The theoretical framework and practical value
|> of that alternative were established with the Prolog II work at Marseille,
|> and there's certainly a sound way of thinking about Prolog with cyclic
|> terms. However, as far as I know there is no free lunch. Sound and
|> terminating unification of cyclic terms can be more costly than
|> unsound Prolog unification.

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.

Isn't it strange that the forthcoming Prolog standard will explicitly
accept implementations of unification that may not terminate on certain
terms.  I certainly understand that finite tree unifications is needed
for some interesting applications.  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.

By the way, was it Edinburgh or Marseille which first dropped
the occurs check?

-- 
Gert Smolka, DFKI, Stuhlsatzenhausweg 3, D-W-6600 Saarbr"ucken, Germany
Tel: +49 681 302-5311;  Fax: +49 681 302-5341; Net: smolka@dfki.uni-sb.de