home *** CD-ROM | disk | FTP | other *** search
/ NetNews Usenet Archive 1992 #30 / NN_1992_30.iso / spool / comp / lang / prolog / 2267 < prev    next >
Encoding:
Internet Message Format  |  1992-12-21  |  2.6 KB
  1. Path: sparky!uunet!spool.mu.edu!uwm.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: <24448@alice.att.com>
  6. Date: 19 Dec 92 00:30:12 GMT
  7. Article-I.D.: alice.24448
  8. References: <1992Dec17.111142.24450@dcs.qmw.ac.uk> <24435@alice.att.com> <TORKEL.92Dec17201903@bast.sics.se> <1992Dec18.175714.3917@cs.sfu.ca>
  9. Reply-To: pereira@alice.UUCP ()
  10. Organization: AT&T, Bell Labs
  11. Lines: 43
  12.  
  13. In article <1992Dec18.175714.3917@cs.sfu.ca> jamie@cs.sfu.ca (Jamie Andrews) writes:
  14. >I seem to dimly remember someone having
  15. >characterized the precise theory solved by some unification
  16. >without occurs check.  Does anyone remember the reference?
  17. @ARTICLE{jaffar-stuckey,
  18.     AUTHOR = {Joxan Jaffar and Peter J. Stuckey},
  19.     TITLE = {Semantics of Infinite Tree Logic Programming},
  20.     JOURNAL = {Theoretical Computer Science},
  21.     YEAR = {1986},
  22.     VOLUME = {46},
  23.     PAGES = {141-158}
  24. }
  25. >     Also, I sometimes tell people that Martelli and Montanari's
  26. >and Paterson and Wegman's linear unification algorithms are not
  27. >used because either (a) the constant factor is too high or (b)
  28. >the space requirements are too high.
  29. (a) is a problem, but the main problem is that those algorithms are linear
  30. on the *sum* of the sizes of the two terms being unified, while
  31. (in most practical cases) the Robinson unification algorithm without
  32. the occurs check is linear on the size of the *smaller* term. Notice
  33. that most such unifications in Prolog involve some arbitrarily large
  34. constructed term and a clause head, which is tyoically small, and
  35. of bounded size. I say above "in most practical cases" because
  36. the Robinson algorithm without occurs check is linear on the size of
  37. the *tree unfolding* of the smaller term, but the tree unfolding of
  38. a term may be exponential on the size of the (graph representation of)
  39. the term and thus on the number of variable substitution steps needed
  40. to construct the term. In contrast, the linear unification algorithms,
  41. as well as the most efficient algorithms for rational term unification
  42. (all in one way or another based on some version of UNION-FIND) keep
  43. track of which subterms they have visited and they don't revisit them.
  44. Another source of overhead for the rational term unification algorithms
  45. is that in general they side-effect not just the leaves (variable cells)
  46. but also internal (complex term) nodes (at least all that I have seen
  47. do). These side effects must be kept track of to be undone on backtracking.
  48.  
  49. Fernando Pereira
  50. 2D-447, AT&T Bell Laboratories
  51. 600 Mountain Ave, PO Box 636
  52. Murray Hill, NJ 07974-0636
  53. pereira@research.att.com
  54.  
  55.  
  56.