c60c-2ca@WEB.berkeley.edu (Andrew Choi) (05/07/90)
Hi Gurus. I have a simple question about unification... Assume I have the following predicate defined: equal(X, X). Does the following unify? ?- equal(foo(Y), Y). On my Prolog interpreter, it unifies but gives very strange instantiation for Y. What should the "correct" answer be? Thanks a lot. Andrew Choi Internet Address: c60c-2ca@web.berkeley.edu Standard Disclaimer
weyand@csli.Stanford.EDU (Chris Weyand) (05/08/90)
c60c-2ca@WEB.berkeley.edu (Andrew Choi) writes: >Hi Gurus. I have a simple question about unification... >Assume I have the following predicate defined: >equal(X, X). >Does the following unify? >?- equal(foo(Y), Y). >On my Prolog interpreter, it unifies but gives very strange >instantiation for Y. What should the "correct" answer be? This is like querying with: ?- Y = foo(Y). In which case what will be returned is a very long predicate with the following form: Y = foo(foo(foo(foo(foo(foo(... It's just a recursive definiition of Y that happens to be somewhat nasty. Sort of like setting the cdr of a list to the list itself. Chris Weyand weyand@csli.Stanford.edu
pgl@cup.portal.com (Peter G Ludemann) (05/08/90)
Andrew Choi asks: > equal(X, X). > Does the following unify? > ?- equal(foo(Y), Y). The answer is "sort of". Most Prologs lack the 'occurs check', so this will unify but will set Y to an 'infinite structure' foo(foo(foo(foo(....)))). Some Prologs (e.g., IBM-Prolog and Prolog-III) can handle such infinite structures and output them in the form foo(@(1)) -- the "@" notation refers to how many levels up in the tree the pointer goes. Is this useful? Not terribly. The one use I have seen for it is to represent a recursive program in data. Is this reasonable? That depends on your point of view. Robinson's original resolution forbad unifying foo(Y) and Y because it was against the rules of his logic -- Colmerauer has defined a different logic which allows such structures (he calls them 'rational trees'). Some Prologs have a special 'occurs-check unifier' which you can use explicitly to avoid such structures. Unifying without the occurs check is much faster than unifying with the occurs check. - Peter Ludemann --- standard disclaimer ---
bradley@cs.utexas.edu (Bradley L. Richards) (05/09/90)
In article <1990May7.132305.15989@agate.berkeley.edu> c60c-2ca@WEB.berkeley.edu (Andrew Choi) writes: >Assume I have the following predicate defined: >equal(X, X). >Does the following unify? >?- equal(foo(Y), Y). > >On my Prolog interpreter, it unifies but gives very strange >instantiation for Y. What should the "correct" answer be? According to the proper definition for unification, these terms should not unify. However, for "efficiency" reasons, most Prolog implementations omit the "occurs" check (i.e. here Y appears in foo(Y)), and blindly unify these terms. This is, in fact, an error--and one worth fussing at the manufacturer of your Prolog about. Implementing the occurs check isn't really that costly.... Bradley
stolcke@icsi.Berkeley.EDU (Andreas Stolcke) (05/09/90)
In article <189@qt.cs.utexas.edu>, bradley@cs.utexas.edu (Bradley L. Richards) writes: |> According to the proper definition for unification, these terms should |> not unify. However, for "efficiency" reasons, most Prolog implementations |> omit the "occurs" check (i.e. here Y appears in foo(Y)), and blindly |> unify these terms. This is, in fact, an error--and one worth fussing |> at the manufacturer of your Prolog about. Implementing the occurs |> check isn't really that costly.... Quoting from the C-Prolog User's manual, edited by Fernando Pereira, 1984: The absence of the occur check is not a bug or design oversight, but a conscious design decision. The reason for this decision is that unification with the occur check is at best linear on the sum of the sizes of the terms being unified, whereas unification without the occur check is linear on the size of the smallest of the terms being unified. In any practical programming language, basic operations are supposed to take constant time. Unification against a variable should be thought of as the basic operation of Prolog, but this can take constant time only if the occur check is omitted. Thus the absence of a occur check is essential to make Prolog into a practi- cal programming language. The inconvenience caused by this Unless there is some technique I'm not aware of to make the occurs check sub-linear, I'd say that the above argument against the occur check sound pretty reasonable. ---- Andreas Stolcke International Computer Science Institute stolcke@icsi.Berkeley.EDU 1957 Center St., Suite 600, Berkeley, CA 94704 (415) 642-4274 ext. 126
bradley@cs.utexas.edu (Bradley L. Richards) (05/10/90)
In article <24861@pasteur.Berkeley.EDU> stolcke@icsi.Berkeley.EDU (Andreas Stolcke) writes: >In article <189@qt.cs.utexas.edu>, bradley@cs.utexas.edu (Bradley L. >Richards) writes: >|> for "efficiency" reasons, most Prolog implementations >|> omit the "occurs" check (i.e. here Y appears in foo(Y)), and blindly >|> unify these terms. This is, in fact, an error-- > >Quoting from the C-Prolog User's manual, edited by Fernando Pereira, 1984: > > The absence of the occur check is not a bug or > design oversight, but a conscious design decision. > In any practical programming > language, basic operations are supposed to take constant > time. Unification against a variable should be thought of > as the basic operation of Prolog, but this can take constant > time only if the occur check is omitted. > >I'd say that the above argument against the occur check sound >pretty reasonable. I think "conscious design decision" is the key phrase here. IMHO, a decision to improve efficiency at the expense of correctness is a poor decision. It's much like the thread on this group about integer overflow--omitting checks for integer overflow for the sake of efficiency is foolish (as an *option* it's ok, but as a *default* it's nuts). The same thing with the occurs check. What definition of "practical" are we using here? Is a language that produces erroneous results "practical"? Again, for optimization after code has been thoroughly tested and debugged, we might want to turn off some of the safety checks. But as a standard way of doing business, omitting the occurs check is simply wrong. --------------------------------------------------------------------------- Bradley L. Richards uucp: cs.utexas.edu!bradley bradley@cs.utexas.edu CompuServe: 75216,1744 ---------------------------------------------------------------------------
pereira@alice.UUCP (Fernando Pereira) (05/18/90)
In article <40089@brunix.UUCP> mj@cs.brown.edu (Mark Johnson) writes: >It is computationally cheaper to implement safe unification and eq-tests >than to implement the occurs check. It is not clear that this is the case asymptotically , see for instance ``An Almost Linear Robinson Unification Algorithm'' by Peter Ruzicka (missing some diacritics) and Igor Privara, Acta Informatica 27, pp.61-71, 1989. Unfortunately, the real problem is constant factors; every rational term unification algorithm I know requires far more (and more complex) trailing of side-effects to terms than the usual Prolog unification. No free lunch... Fernando Pereira 2D-447, AT&T Bell Laboratories 600 Mountain Ave, Murray Hill, NJ 07974 pereira@research.att.com
mj@cs.brown.edu (Mark Johnson) (05/28/90)
pereira@alice.UUCP (Fernando Pereira) writes: > mj@cs.brown.edu (Mark Johnson) writes: > >It is computationally cheaper to implement safe unification > >than to implement the occurs check. > > Unfortunately, the real problem is constant factors; every rational term > unification algorithm I know requires far more (and more complex) trailing > of side-effects to terms than the usual Prolog unification. No free lunch... True enough. But not having a safe unification can lead to some nasty bugs. In e.g. C-Prolog, see what happens with the following query: X = f(X,X), Y = f(Y,Y), X = Y, fail. Most debuggers I know of can't identify this sort of bug; they just drop dead on you. I also wonder how much more trailing rational term unification requires. After all, half of the nodes of a binary tree are leaf nodes. Also, as I understand it, rational term unification makes unified structures eq, so it should help reduce heap size. Finally, to obtain a safe unification algorithm it's only necessary to redirect (and hence trail) one term node in every cycle, so term nodes that the compiler can identify as part of an acyclic term don't need to be trailed at all. Mark Johnson.