home *** CD-ROM | disk | FTP | other *** search
/ NetNews Usenet Archive 1992 #30 / NN_1992_30.iso / spool / comp / lang / prolog / 2250 < prev    next >
Encoding:
Internet Message Format  |  1992-12-17  |  2.8 KB

  1. Path: sparky!uunet!cs.utexas.edu!zaphod.mps.ohio-state.edu!pacific.mps.ohio-state.edu!linac!att!att!allegra!alice!pereira
  2. From: pereira@alice.att.com (Fernando Pereira)
  3. Newsgroups: comp.lang.prolog
  4. Subject: Re: Occurs check
  5. Message-ID: <24435@alice.att.com>
  6. Date: 17 Dec 92 17:10:03 GMT
  7. Article-I.D.: alice.24435
  8. References: <1992Dec13.173016.8849@nntp.hut.fi> <1992Dec17.111142.24450@dcs.qmw.ac.uk>
  9. Reply-To: pereira@alice.UUCP ()
  10. Organization: AT&T, Bell Labs
  11. Lines: 47
  12.  
  13. In article <1992Dec17.111142.24450@dcs.qmw.ac.uk> mmh@dcs.qmw.ac.uk (Matthew Huntbach) writes:
  14. >I have written programs which rely on the occur-check not
  15. >happening, since they intentionally build circular structures.
  16. >What should be so wrong with this - after all it's a standard
  17. >programing feature in lazy functional languages.
  18. If you think of Prolog programs as *logic* programs where the logic is
  19. (a fragment of) first-order logic, what is wrong it that the answers
  20. derived without the occurs-check are in general unsound. For example,
  21. consider the first-order question
  22.  
  23.     forall x. exists y. r(x,y) ?= exists x. r(x, x)
  24.  
  25. (where ?= means ``is the rhs a logical consequence of the lhs?''). The
  26. answer is negative, eg. take r to be the successor relation on the natural
  27. numbers. Now convert the question to Prolog by Skolemization. The same
  28. question maps to the Prolog question
  29.  
  30.     r(X, f(X)) ?- r(U, U)
  31.  
  32. Without the occurs check, this succeeds! Lest you think this is an artificial
  33. example of no practical import, let me say that I have been badly bitten
  34. by the lack of an occurs check in several natural-language parsers and
  35. generators. Nonetheless, the efficiency reasons that led to Prolog's
  36. unification not having the check are pretty compelling, so I do not advocate
  37. adding it to Prolog in all cases. A clever compiler might be able to
  38. recognize many cases of practical importance in which the check is
  39. not needed and only call the more expensive unification with occurs check
  40. in the remaining cases. Alternatively, careful programmers can do some of
  41. that analysis by hand, and put explicit calls to a sound unification
  42. when necessary.
  43.  
  44. If you want to program with cyclic terms, you have gone outside
  45. bare first-order logic to a system in which terms are interpreted
  46. in a different way. The theoretical framework and practical value
  47. of that alternative were established with the Prolog II work at Marseille,
  48. and there's certainly a sound way of thinking about Prolog with cyclic
  49. terms. However, as far as I know there is no free lunch. Sound and
  50. terminating unification of cyclic terms can be more costly than
  51. unsound Prolog unification (the reverse can also happen for acyclic terms
  52. with a lot of reentrancy, though) and that cost is incurred at every
  53. unification in a program.
  54.  
  55. Fernando Pereira
  56. 2D-447, AT&T Bell Laboratories
  57. 600 Mountain Ave, PO Box 636
  58. Murray Hill, NJ 07974-0636
  59. pereira@research.att.com
  60.