home *** CD-ROM | disk | FTP | other *** search
- Path: sparky!uunet!cs.utexas.edu!zaphod.mps.ohio-state.edu!pacific.mps.ohio-state.edu!linac!att!att!allegra!alice!pereira
- From: pereira@alice.att.com (Fernando Pereira)
- Newsgroups: comp.lang.prolog
- Subject: Re: Occurs check
- Message-ID: <24435@alice.att.com>
- Date: 17 Dec 92 17:10:03 GMT
- Article-I.D.: alice.24435
- References: <1992Dec13.173016.8849@nntp.hut.fi> <1992Dec17.111142.24450@dcs.qmw.ac.uk>
- Reply-To: pereira@alice.UUCP ()
- Organization: AT&T, Bell Labs
- Lines: 47
-
- 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
-