Path: utzoo!utgpu!news-server.csri.toronto.edu!rutgers!apple!portal!cup.portal.com!pgl
From: pgl@cup.portal.com (Peter G Ludemann)
Newsgroups: comp.lang.prolog
Subject: Re: Does It Unify?
Message-ID: <29713@cup.portal.com>
Date: 8 May 90 05:14:41 GMT
References: <1990May7.132305.15989@agate.berkeley.edu>
Distribution: usa
Organization: The Portal System (TM)
Lines: 27

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 ---