🚀 go-pugleaf

Our Prolog system ECLiPSe, which is the successor of SEPIA, has an option
to enable the occurs check. ECLiPSe is available for academic sites for
a nominal fee. Please send email if you are interested.

---------------------------------------------------------------------------
 Joachim Schimpf                                 Email   joachim@ecrc.de 
 European Computer-Industry Research Centre      Phone   +49 89 92699 111
 Arabellastrasse 17, D-8000 Munich 81, Germany   Fax     +49 89 92699 170

In article <1992Dec13.173016.8849@nntp.hut.fi> jur@robin.cs.hut.fi (Jussi Rintanen) writes:

>   Question 1: What implementations of Prolog implement the occurs check?
>   (Our university has both Sicstus and NU-Prolog.)
>


Try SEPIA-Prolog  from  ECRC  in munich/Germany.  It   has   some nice
features, including the  possibility  for sound unification.  It  also
includes "iterative deepening", so you need not program it explicitly.
Sepia is cheap and pretty fast. Contact sepia_request@ecrc.de (i'm not
quite sure about this adress)

As an alternative you could "linearize" the heads of your rules, i.e.
eliminate multiple occurences of variables in the head. For example, 
your rule

	axiom(impl(A,impl(B,A)),k).

then becomes

	axiom(impl(A,impl(B,A1)),k) :- unify(A,A1).

where unify/2 is a sound unification procedure, as can be found e.g. 
in the quintus library. This works sufficiently well for many
programs. However, the first alternative, a Prolog with built-in sound
unification, is superior (wrt. efficiency).

	Peter
--
____________________________________________________________________
Peter Baumgartner                      | peter@infko.uni-koblenz.de
Universitaet Koblenz,                  |
Institut fuer Informatik               | Voice: +49 261 9119-426
Rheinau 3-4, D-5400 Koblenz, Germany   | Fax:   +49 261 37524

joachim@ecrc.de (Joachim Schimpf) writes:

>Our Prolog system ECLiPSe, which is the successor of SEPIA, has an option
How is ECLiPSe different from SEPIA?

jim

In article <1992Dec13.173016.8849@nntp.hut.fi>, jur@robin.cs.hut.fi (Jussi Rintanen) writes:
> 
> Question 1: What implementations of Prolog implement the occurs check?
> (Our university has both Sicstus and NU-Prolog.)
> 

The Wild_LIFE system implements unification of psi-terms, which
renders the occur check superfluous.  Wild_LIFE is an
implementation of LIFE, a language that elegantly generalizes
Prolog.  A psi-term is an open-ended dynamic record that may be
cyclic  (i.e., it is a general rooted graph).

Peter 

----------------------------------------------------------------
Peter Van Roy
Digital Equipment Corporation          Net: vanroy@prl.dec.com
Paris Research Laboratory              Tel: (33) (1) 47 14 28 65
85, avenue Victor Hugo                 Fax: (33) (1) 47 14 28 99
92500 Rueil-Malmaison Cedex           Home: (33) (1) 30 61 41 29
France
----------------------------------------------------------------

In article <1992Dec13.173016.8849@nntp.hut.fi> Jussi.Rintanen@hut.fi writes:
>Question 1: What implementations of Prolog implement the occurs check?

I have written programs which rely on the occur-check not
happening, since they intentionally build circular structures.
What should be so wrong with this - after all it's a standard
programing feature in lazy functional languages.

Matthew Huntbach

In article <1992Dec17.111142.24450@dcs.qmw.ac.uk> mmh@dcs.qmw.ac.uk 
(Matthew Huntbach) writes:

   >I have written programs which rely on the occur-check not
   >happening, since they intentionally build circular structures.
   >What should be so wrong with this - after all it's a standard
   >programing feature in lazy functional languages.

  There's nothing wrong with it. It's just that it's a good idea, both from
a theoretical and a practical point of view, to know what constraint system
one is working in. A Prolog without occur check which nevertheless only
partially supports circular term-like structures promotes the use of obscure
programming tricks and widens the gap between theory and practice.

In article <1992Dec17.111142.24450@dcs.qmw.ac.uk> mmh@dcs.qmw.ac.uk (Matthew Huntbach) writes:

MH   I have written programs which rely on the occur-check not
MH   happening, since they intentionally build circular structures.
MH   What should be so wrong with this - after all it's a standard
MH   programing feature in lazy functional languages.

If you allow cycles, you change the term universe.
A solution to a goal t=u where t and u are first order terms should be
a substitution (a mapping from variables to first-order terms) sigma,
such that sigma(t)=sigma(u).  Because sigma is a first-order
substitution, the resulting terms are first-order too.

If you are using unification without occur-check, then the
substitution might not be first-order, the substituted terms can
contain cycles. One can express this semantically by adding a fixpoint
operator to the term universe.
You are right that it is often useful to have cyclic terms;
but they live in this different term universe
and Prolog's = is an incomplete unification there, e.g. the goal
	A=f(A), B=f(B), A=B
usually fails to terminate, although it should either fail (in the
Herbrand universe) or succeed (in the extended universe).
It is possible to extend unification with a cycle check to make it
terminate even for cyclic terms (some Prologs have such a thing; I
even know a programming language which uses unification with cycle
check for type inference), but this is again less efficient than
ordinary = , probably similar in efficiency to unification with occur
check.

--
Stefan Kahrs	                   JANET:    smk@uk.ac.ed.dcs
LFCS, Dept. of Computer Science    Internet: smk@dcs.ed.ac.uk
University of Edinburgh            UUCP:     ..!mcsun!uknet!dcs!smk
Edinburgh
EH9 3JZ                            Tel:      (44)-31-650-5139
SCOTLAND                           Fax:      (44)-31-667-7209

In article <1992Dec17.111142.24450@dcs.qmw.ac.uk> mmh@dcs.qmw.ac.uk (Matthew Huntbach) writes:
>I have written programs which rely on the occur-check not
>happening, since they intentionally build circular structures.
>What should be so wrong with this - after all it's a standard
>programing feature in lazy functional languages.
If you think of Prolog programs as *logic* programs where the logic is
(a fragment of) first-order logic, what is wrong it that the answers
derived without the occurs-check are in general unsound. For example,
consider the first-order question

	forall x. exists y. r(x,y) ?= exists x. r(x, x)

(where ?= means ``is the rhs a logical consequence of the lhs?''). The
answer is negative, eg. take r to be the successor relation on the natural
numbers. Now convert the question to Prolog by Skolemization. The same
question maps to the Prolog question

	r(X, f(X)) ?- r(U, U)

Without the occurs check, this succeeds! Lest you think this is an artificial
example of no practical import, let me say that I have been badly bitten
by the lack of an occurs check in several natural-language parsers and
generators. Nonetheless, the efficiency reasons that led to Prolog's
unification not having the check are pretty compelling, so I do not advocate
adding it to Prolog in all cases. A clever compiler might be able to
recognize many cases of practical importance in which the check is
not needed and only call the more expensive unification with occurs check
in the remaining cases. Alternatively, careful programmers can do some of
that analysis by hand, and put explicit calls to a sound unification
when necessary.

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 (the reverse can also happen for acyclic terms
with a lot of reentrancy, though) and that cost is incurred at every
unification in a program.

Fernando Pereira
2D-447, AT&T Bell Laboratories
600 Mountain Ave, PO Box 636
Murray Hill, NJ 07974-0636
pereira@research.att.com

In article <1992Dec15.131151.21406@prl.dec.com> vanroy@prl.dec.com (Peter Van Roy) writes:
>The Wild_LIFE system implements unification of psi-terms, which
>renders the occur check superfluous.  Wild_LIFE is an
>implementation of LIFE, a language that elegantly generalizes
>Prolog.  A psi-term is an open-ended dynamic record that may be
>cyclic  (i.e., it is a general rooted graph).

Could you please provide references for Wild_LIFE? Thanks.

-- Milan Richter, Seattle 

Fernando Pereira writes:
> Nonetheless, the efficiency reasons that led to Prolog's
> unification not having the check are pretty compelling, so I do not advocate
> adding it to Prolog in all cases. 

While I believe this statement, it would be interesting to actually see some
numbers (preferably for programs other than nrev) showing how much more
expensive unification becomes with the occurs check.  Do the implementors
of Sepia, NU-Prolog, and other systems that provide both kinds of
unification have any numbers they'd care to post?
-- 
Saumya Debray
CIS Dept, University of Oregon, Eugene, OR
debray@cs.uoregon.edu

In article <24435@alice.att.com> pereira@alice.att.com (Fernando Pereira)
 writes:

   >If you think of Prolog programs as *logic* programs where the logic is
   >(a fragment of) first-order logic, what is wrong it that the answers
   >derived without the occurs-check are in general unsound.

  This is putting it too strongly, since such answers are perfectly
sound relative to the interpretation of a (pure) program as the union
of the clauses and the identities true in a suitable universe of
rational trees. The logic involved is still first order logic, it's
just that we have a somewhat stronger interpretation of programs.
Generally speaking, these distinctions are much simpler if we think in
terms of wedding different constraint theories to Horn clauses, as
originally suggested by Colmerauer.

In article <24435@alice.att.com> pereira@alice.UUCP () writes:
>If you think of Prolog programs as *logic* programs where the logic is
>(a fragment of) first-order logic, what is wrong it that the answers
>derived without the occurs-check are in general unsound. For example,
>consider the first-order question
>
Well, yes, I'm aware of this, but Prolog is such a compromised
form of logic that I wonder if it matters. In any case, I
generally program in Strand where since there isn't full
unification, the problems of unifying cyclic terms don't occur.

Matthew Huntbach

In article <1992Dec17.185017.17766@cs.uoregon.edu> debray@majestix.cs.uoregon.edu (Saumya K. Debray) writes:
>Fernando Pereira writes:
>> Nonetheless, the efficiency reasons that led to Prolog's
>> unification not having the check are pretty compelling, so I do not advocate
>> adding it to Prolog in all cases. 
>While I believe this statement, it would be interesting to actually see some
>numbers (preferably for programs other than nrev) showing how much more
>expensive unification becomes with the occurs check.
Let me refine and qualify my assertion. In typical programs that I have
written or read, fairly large terms are passed around. With a naive
implementation of the occurs check, each such term has to be fully examined
whenever it is passed as an actual parameter to a predicate. For instance,
append becomes O(n^2) rather than O(n). However, in many of the cases
the complex term is being unified with a variable occuring only once in
the head, with a term the variables in which occur only once in the
head, or the same situations arise involving variable instances that can be
shown by global flow analysis to be ``new'' (that is not occuring
anywhere else in the current resolvent). In any of those cases, the occurs
check is not needed. This is just scratching the surface, much more
sophisticated analyses have been published.

Fernando Pereira
2D-447, AT&T Bell Laboratories
600 Mountain Ave, PO Box 636
Murray Hill, NJ 07974-0636
pereira@research.att.com

In article <TORKEL.92Dec17201903@bast.sics.se> torkel@sics.se (Torkel Franzen) writes:
>In article <24435@alice.att.com> pereira@alice.att.com (Fernando Pereira)
> writes:
>   >If you think of Prolog programs as *logic* programs where the logic is
>   >(a fragment of) first-order logic, what is wrong it that the answers
>   >derived without the occurs-check are in general unsound.
>  This is putting it too strongly, since such answers are perfectly
>sound relative to the interpretation of a (pure) program as the union
>of the clauses and the identities true in a suitable universe of
>rational trees. The logic involved is still first order logic, it's
>just that we have a somewhat stronger interpretation of programs.
No, it is not too strong. I think you are confusing deduction in
an interpreted system (eg. Horn clauses over the domain of finite trees,
or of rational trees) with deduction that yields consequences true
in any model, that is, valid consequences. If I use resolution to
show that P |- exists x. Q (by deriving the empty clause from
P /\ forall x. not Q) I have shown P |= exists x. Q, that is, for *any*
model M such that M |= P there is an assignment a for x such that
P, a |= Q. In particular (going back to my example) if I conclude
by resolution that P |- exists x. r(x,x) then in every model of P
there is an element that stands in the r relation with itself. With
P = forall u. r(u, f(u)), from which exists x. r(x,x) follows by resolution
without the occurs check, the model in which r is the successor relation
on |N and f the successor function refutes exists x. r(x, x). Thus
resolution without the occurs check is unsound as a method for deriving
valid consequences in (uninterpreted) first-order logic. It could
still be sound as a method for deriving true conseuqnces over some class of
models, eg. rational trees. But that is a *very* different thing. When
using logic for knowledge representation, we often do not know what
models to consider, but rather we are interested in characterizing
logically the class on models of interest. Thus we need to work with
valid consequence, not just true consequence in particular models.
On the other hand, if we are interested in using logic to define
relations over particular structures, eg. rational trees, resolution
modulo a particular equational theory can be the right way to go.
Still, it is important not to confuse those two alternatives.

Fernando Pereira
2D-447, AT&T Bell Laboratories
600 Mountain Ave, PO Box 636
Murray Hill, NJ 07974-0636
pereira@research.att.com

In article <1992Dec17.185017.17766@cs.uoregon.edu>, debray@majestix.cs.uoregon.edu (Saumya K. Debray) writes:
> Fernando Pereira writes:
> > Nonetheless, the efficiency reasons that led to Prolog's
> > unification not having the check are pretty compelling, so I do not advocate
> > adding it to Prolog in all cases. 
> 
> While I believe this statement, it would be interesting to actually see some
> numbers (preferably for programs other than nrev) ...

An extreme example is "append" for difference lists (no flames on the
terminology, please!).  Without the occurs check, the cost is O(1);
with the occurs check, the cost is O(n) on the size of the terms (in 
other words, it gets the same cost as regular append).  Normally, the
programmer knows that the occurs check isn't needed, so this is a big win.

Without the occurs check, "infinite" or "rational" terms can be produced.
I've seen one practical use for them, for representing the fixpoint
of a recursive program as a term.  No doubt, there are other uses.

-----

Peter Ludemann

>In article <1992Dec17.185017.17766@cs.uoregon.edu> debray@majestix.cs.uoregon.edu (Saumya K. Debray) writes:
>
>Fernando Pereira writes:
>> Nonetheless, the efficiency reasons that led to Prolog's
>> unification not having the check are pretty compelling, so I do not advocate
>> adding it to Prolog in all cases. 
>
>While I believe this statement, it would be interesting to actually see some
>numbers (preferably for programs other than nrev) showing how much more
>expensive unification becomes with the occurs check. ...
>
That's a topic we are interested in, too. Often, people
working on the sound omission of the occur check write that carrying
out sound unification always is prohibited for efficiency reasons.
But has anybody investigated this systematically? 

In order to support the efficiency argument for omitting the occur
check, we carried out some small experiments with SEPIA-Prolog.
We ran the reverse-program on a list of about 1000 terms.  
The result was astonishing (at least to us): 
performance degrades only about 10-20 percent when using sound
unification. Here, it was necessary to work on (moderately) large terms in
order to note a difference at all. 

Maybe our observation is not true in general, and the result is due to
the clever implementation of SEPIA. Does someone know about 
the SEPIA-Implementation? 
Are there any better examples supporting the effciency argument?

	P. Baumgartner
--
____________________________________________________________________
Peter Baumgartner                      | peter@infko.uni-koblenz.de
Universitaet Koblenz,                  |
Institut fuer Informatik               | Voice: +49 261 9119-426
Rheinau 3-4, D-5400 Koblenz, Germany   | Fax:   +49 261 37524

In article <1992Dec18.093045.21069@dcs.qmw.ac.uk> mmh@dcs.qmw.ac.uk (Matthew Huntbach) writes:
>In article <24435@alice.att.com> pereira@alice.UUCP () writes:
>>If you think of Prolog programs as *logic* programs where the logic is
>>(a fragment of) first-order logic, what is wrong it that the answers
>>derived without the occurs-check are in general unsound. 
>Well, yes, I'm aware of this, but Prolog is such a compromised
>form of logic that I wonder if it matters.
Right. Since we've had a hurricane, why not go for an earthquake as well?
More seriously, except for the lack of an occurs check, the original
*pure* Prolog is sound, and *many* interesting deductive tasks can
be coded in pure Prolog. Furthermore, extralogical features like assert
can be used in constrained *logical* ways, eg. for lemma storage,
and the resulting programs would be sound with respect to well-defined
logical systems, *if they were executed with the occurs check.* The
problem with the lack of an occurs check is that it can hit you
in unforeseen and mysterious ways, while the nonlogical parts
of Prolog hit you *only* if you use them unwisely.

Fernando Pereira
2D-447, AT&T Bell Laboratories
600 Mountain Ave, PO Box 636
Murray Hill, NJ 07974-0636
pereira@research.att.com

In article <24439@alice.att.com> pereira@alice.att.com (Fernando Pereira)
 writes:

   >No, it is not too strong. I think you are confusing deduction in
   >an interpreted system (eg. Horn clauses over the domain of finite trees,
   >or of rational trees) with deduction that yields consequences true
   >in any model, that is, valid consequences.

  There is no confusion involved. It is merely a matter of "valid
consequences of what". The answers yielded by a Prolog system using
unification without occurs check are consequences in first order logic
of the clauses of the program together with the first order identity
theory of rational trees.

In article <TORKEL.92Dec18231028@lludd.sics.se> torkel@sics.se (Torkel Franzen) writes:
>In article <24439@alice.att.com> pereira@alice.att.com (Fernando Pereira)
> writes:
>   >No, it is not too strong. I think you are confusing deduction in
>   >an interpreted system (eg. Horn clauses over the domain of finite trees,
>   >or of rational trees) with deduction that yields consequences true
>   >in any model, that is, valid consequences.
>  There is no confusion involved. It is merely a matter of "valid
>consequences of what". The answers yielded by a Prolog system using
>unification without occurs check are consequences in first order logic
>of the clauses of the program together with the first order identity
>theory of rational trees.
I agree. Adding the first-order theory of rational trees to the left of the
|- is precisely restricting the class of models under consideration
from arbitrary first-order models to rational tree models. For some
applications this is fine, but as I pointed out earlier for many others
it is not. In any case, one needs to be *very* clear about what one
is assuming to the left of the |-. 

Fernando Pereira
pereira@research.att.com

In article <24454@alice.att.com> pereira@alice.att.com (Fernando Pereira)
 writes:

   >I agree. Adding the first-order theory of rational trees to the left of the
   >|- is precisely restricting the class of models under consideration
   >from arbitrary first-order models to rational tree models.

   This is not so, since the class of rational tree models cannot be
characterized by any set of first order axioms, any more than the finite
tree models.

   >In any case, one needs to be *very* clear about what one
   >is assuming to the left of the |-. 

  In a more perspicuous description of Prolog-style Horn clause programming,
I think it's a good idea to separate the constraint system from the
resolution mechanism. Thus Prolog (in the simplified version here considered),
whatever the constraint system used, delivers answers to a question A(x)
of the form C(x,y), where C(x,y) is a conjunction of constraints, and
it always holds that

    (1)                     C(x,y) -> A(x)

is a logical consequence of the program, read as a set of Horn clauses. Of
course (1) does not imply that there is an x such that A(x); for this to
follow, the constraint theory must be used.

In article <TORKEL.92Dec20104928@bast.sics.se> torkel@sics.se (Torkel Franzen) writes:
>In article <24454@alice.att.com> pereira@alice.att.com (Fernando Pereira)
>   >I agree. Adding the first-order theory of rational trees to the left of the
>   >|- is precisely restricting the class of models under consideration
>   >from arbitrary first-order models to rational tree models.
>
>   This is not so, since the class of rational tree models cannot be
>characterized by any set of first order axioms, any more than the finite
>tree models.
It cannot be characterized by any *finite* set of first-order formulas.
Notice that I used *theory*, not program in my note. The term "theory"
in logic means any deductively closed set of formulas. In fact, for a finite
signature you can characterize the finite tree models by a finite set
of equality and inequality formulas -- that's precisely what the Clark
completion uses. I don't have handy the relevant papers on rational tree
models, but I believe the same is true for them (papers by Joxan Jaffar and
Michael Maher?).

Anyway, this is just fine print, the main points have already been made clear:
(i) the occurs check is needed for sound deduction in pure first-order
logic; (ii) unification without the occurs check is sound for
deduction over rational tree models; (iii) Prolog unification (by this
I mean what was in Prolog originally) can construct rational terms,
but may not termfinate when unifying them; (iv) there are various
unification algorithms for rational trees, the asymptotically most efficient
of which I believe are all based on UNION-FIND (DFA equivalence). 

Fernando Pereira
pereira@research.att.com

In article <24458@alice.att.com> pereira@alice.att.com (Fernando Pereira)
 writes:

   >It cannot be characterized by any *finite* set of first-order formulas.

  Finiteness is not relevant here. It is a matter of what can be
expressed in first order logic. By compactness, any set of first order
formulas which has a model with the Herbrand universe
{0,s(0),s(s(0)),..} as its domain will have countable models
containing elements different from (the interpretations of) the terms
0,s(0), ec. Therefore it is not correct to say that adding the
(complete) first order identity theory of finite trees to the left of
|- is precisely restricting the class of models under consideration
from arbitrary first order models to finite tree models.  Similarly
for rational trees. Such a restriction cannot be achieved in first
order logic.

 Saumya Debray writes:
 > 
 > Fernando Pereira writes:
 > > Nonetheless, the efficiency reasons that led to Prolog's
 > > unification not having the check are pretty compelling, so I do not advocate
 > > adding it to Prolog in all cases. 
 > 
 > While I believe this statement, it would be interesting to actually see some
 > numbers (preferably for programs other than nrev) showing how much more
 > expensive unification becomes with the occurs check.  Do the implementors
 > of Sepia, NU-Prolog, and other systems that provide both kinds of
 > unification have any numbers they'd care to post?

 Some benchmarks were published in a paper presenting an architecture design of
 a RISC processor for Prolog, in which the occur-check is always performed if
 necessary. They use the WAM, and take advantage of the fact that only
 get_value instructions really need to call the occur-check routine. According
 to their results, 5 % of the time is spent performing the occur-check... It's
 not that much !! Their benchmark programs include quite large programs, up to
 5600 lines. 

 With some analysis (even a simple groundness analysis can be useful, but there
 are also some more sophisticated analysis schemes), I'm sure that on most
 programs, the overhead of the occur-check on a compiled Prolog can be negligible.


 Reference:

 @inproceedings{ DRSW-89,
       author = "Peter Dreussen and Wolfgang Rosentiel and Klaus Erik Schauser and
                 J{\"{o}}rg Wedeck",
       Title  = "{Architecture Design of a RISC Processor for Prolog}", 
       Booktitle = "Euromicro 89",
       Year      =  1989 }

 
 B. Dumant

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

In article <1h4g5tINN5l6@eagle.dfki.uni-sb.de> smolka@dfki.uni-sb.de (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.
I don't know what "rather efficient" means without actual numbers to
back it up. But *all* the rational unification algorithms I know
of need to make and trail more assignments, and chase more pointers,
than the original Prolog unification without the occurs check.
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. 
>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
.he reason is that the efficiency issues mentioned above have not
been addressed to everyone's satisfaction.
>By the way, was it Edinburgh or Marseille which first dropped
>the occurs check?
Marseille. A very detailed and interesting account of the design history
of the first Prolog, written by Alain Colmerauer and Philipe Roussel,
will appear in the forthcoming proceedings of the History of Programming
Languages Conference (April 1993). Their choice was based on the
considerations that I have mentioned before. However, Alain eventually
changed his mind, as shown by the exclusive use of rational unification
in Prolog II. Nevertheless, the efficiency tradeoffs might still be
different for fast compiled Prologs than for interpreted systems
like the original Prolog and Prolog II: when the cost of clause
chasing goes down, the relative cost of term chasing goes up.

Fernando Pereira
2D-447, AT&T Bell Laboratories
600 Mountain Ave, PO Box 636
Murray Hill, NJ 07974-0636
pereira@research.att.com