home *** CD-ROM | disk | FTP | other *** search
/ NetNews Usenet Archive 1992 #30 / NN_1992_30.iso / spool / comp / lang / prolog / 2259 < prev    next >
Encoding:
Text File  |  1992-12-21  |  2.6 KB  |  62 lines

  1. Newsgroups: comp.lang.prolog
  2. Path: sparky!uunet!gumby!destroyer!cs.ubc.ca!fornax!jamie
  3. From: jamie@cs.sfu.ca (Jamie Andrews)
  4. Subject: Re: Occurs check
  5. Message-ID: <1992Dec18.175714.3917@cs.sfu.ca>
  6. Organization: CSS, Simon Fraser University, Burnaby, B.C., Canada
  7. References: <1992Dec17.111142.24450@dcs.qmw.ac.uk> <24435@alice.att.com> <TORKEL.92Dec17201903@bast.sics.se>
  8. Date: Fri, 18 Dec 1992 17:57:14 GMT
  9. Lines: 51
  10.  
  11. In article <TORKEL.92Dec17201903@bast.sics.se> torkel@sics.se (Torkel Franzen) writes:
  12. >  This is putting it too strongly, since such answers are perfectly
  13. >sound relative to the interpretation of a (pure) program as the union
  14. >of the clauses and the identities true in a suitable universe of
  15. >rational trees.
  16.  
  17.      I was going to object to this, when I realized what Torkel
  18. meant:  any answers that you *do* get out of systems without
  19. occurs check are sound relative to the corresponding theory of
  20. rational trees.
  21.  
  22.      However, there are still completeness problems, with cases
  23. like
  24.           x=f(x), y=f(y), x=y
  25. where such systems typically loop instead of succeeding, and
  26. even cases like
  27.           x=f(x,g(x)), y=f(y,h(y)), x=y
  28. where such systems may loop where they should fail.  My guess
  29. would be that applications which rely on the absence of occurs
  30. check to construct cyclic structures would be likely to run into
  31. these problems when comparing terms.  On the other hand I've
  32. never written such an application so I could be wrong.
  33.  
  34.      Another point that comes out of this is that there isn't
  35. just one "unification without occurs check"; we have to be more
  36. precise about exactly what algorithm is being used before we can
  37. tell how it's going to behave.  (I'm not even convinced that
  38. *all* such straightforward unification algorithms would be sound
  39. w.r.t. rational trees.)  I seem to dimly remember someone having
  40. characterized the precise theory solved by some unification
  41. without occurs check.  Does anyone remember the reference?
  42.  
  43.      Also, I sometimes tell people that Martelli and Montanari's
  44. and Paterson and Wegman's linear unification algorithms are not
  45. used because either (a) the constant factor is too high or (b)
  46. the space requirements are too high.  Can anyone point to
  47. something comparing time *and space* requirements for
  48.  
  49. - a typical occurs-check unification
  50. - a typical occurs-check-free unification
  51. - Martelli and Montanari's linear unification
  52. - Paterson and Wegman's linear unification
  53. - Colmerauer's (or other) rational tree unification?
  54.  
  55. As I recall, M&M and P&W just proved that their algorithms were
  56. linear.
  57.  
  58. thanks
  59. --Jamie.
  60.   jamie@cs.sfu.ca
  61. "The Tao's net encompasses the whole universe."  - tao te ching
  62.