🚀 go-pugleaf

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