home *** CD-ROM | disk | FTP | other *** search
/ NetNews Usenet Archive 1992 #30 / NN_1992_30.iso / spool / comp / lang / prolog / 2248 < prev    next >
Encoding:
Internet Message Format  |  1992-12-17  |  2.3 KB
  1. Path: sparky!uunet!pipex!doc.ic.ac.uk!uknet!edcastle!dcs.ed.ac.uk!smk
  2. From: smk@dcs.ed.ac.uk (Stefan Kahrs)
  3. Newsgroups: comp.lang.prolog
  4. Subject: Re: Occurs check
  5. Message-ID: <SMK.92Dec17140038@scarp.dcs.ed.ac.uk>
  6. Date: 17 Dec 92 14:00:38 GMT
  7. References: <1992Dec13.173016.8849@nntp.hut.fi> <1992Dec17.111142.24450@dcs.qmw.ac.uk>
  8. Sender: cnews@dcs.ed.ac.uk (UseNet News Admin)
  9. Distribution: comp
  10. Organization: University of Edinburgh, LFCS
  11. Lines: 37
  12. In-Reply-To: mmh@dcs.qmw.ac.uk's message of 17 Dec 92 11:11:42 GMT
  13.  
  14. In article <1992Dec17.111142.24450@dcs.qmw.ac.uk> mmh@dcs.qmw.ac.uk (Matthew Huntbach) writes:
  15.  
  16. MH   I have written programs which rely on the occur-check not
  17. MH   happening, since they intentionally build circular structures.
  18. MH   What should be so wrong with this - after all it's a standard
  19. MH   programing feature in lazy functional languages.
  20.  
  21. If you allow cycles, you change the term universe.
  22. A solution to a goal t=u where t and u are first order terms should be
  23. a substitution (a mapping from variables to first-order terms) sigma,
  24. such that sigma(t)=sigma(u).  Because sigma is a first-order
  25. substitution, the resulting terms are first-order too.
  26.  
  27. If you are using unification without occur-check, then the
  28. substitution might not be first-order, the substituted terms can
  29. contain cycles. One can express this semantically by adding a fixpoint
  30. operator to the term universe.
  31. You are right that it is often useful to have cyclic terms;
  32. but they live in this different term universe
  33. and Prolog's = is an incomplete unification there, e.g. the goal
  34.     A=f(A), B=f(B), A=B
  35. usually fails to terminate, although it should either fail (in the
  36. Herbrand universe) or succeed (in the extended universe).
  37. It is possible to extend unification with a cycle check to make it
  38. terminate even for cyclic terms (some Prologs have such a thing; I
  39. even know a programming language which uses unification with cycle
  40. check for type inference), but this is again less efficient than
  41. ordinary = , probably similar in efficiency to unification with occur
  42. check.
  43.  
  44. --
  45. Stefan Kahrs                       JANET:    smk@uk.ac.ed.dcs
  46. LFCS, Dept. of Computer Science    Internet: smk@dcs.ed.ac.uk
  47. University of Edinburgh            UUCP:     ..!mcsun!uknet!dcs!smk
  48. Edinburgh
  49. EH9 3JZ                            Tel:      (44)-31-650-5139
  50. SCOTLAND                           Fax:      (44)-31-667-7209
  51.