🚀 go-pugleaf

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