home *** CD-ROM | disk | FTP | other *** search
/ NetNews Usenet Archive 1992 #30 / NN_1992_30.iso / spool / comp / lang / prolog / 2258 < prev    next >
Encoding:
Internet Message Format  |  1992-12-21  |  3.9 KB
  1. Path: sparky!uunet!olivea!spool.mu.edu!caen!batcomputer!cornell!rochester!miller
  2. From: miller@cs.rochester.edu
  3. Newsgroups: comp.lang.prolog
  4. Subject: Re: Occurs check
  5. Message-ID: <9212181802.AA02717@alabaster.cs.rochester.edu>
  6. Date: 18 Dec 92 18:02:56 GMT
  7. Sender: miller@cs.rochester.edu (Brad Miller)
  8. Organization: Computer Science Department University of Rochester
  9. Lines: 60
  10. In-Reply-To: peter@infko.uni-koblenz.de's message of 18 Dec 92 20:15:31 GMT
  11.  
  12.  
  13. Well, I won't claim any generality, but the Rhet language (a prolog
  14. deviant) does allow you to turn the occurs check on and off, and also
  15. shows only about a 15% degradation in general when on. However, this is
  16. using an interpreted system, with a very general unification operator.
  17. Current work on a compiled replacement leads me to beleive that compiled
  18. specialized unification would indeed degrade by many-fold if it (always)
  19. needed to do an occurs check, but it is less than clear that this is in
  20. fact the case (i.e. the compiler may be able to detect when an occurs
  21. check provably isn't needed for a substantial subset of the cases that
  22. occur in day-to-day prolog type code). I do not yet have any numbers to
  23. back up this opinion, however, looking at the problem more abstractly...
  24. (and keeping in mind that I'm a AI/lisp hacker, not a theoretician :-)...
  25.  
  26. Graph Unification that does not detect infinite unifiablity can run in
  27. linear time O(E+V) where E and V are the number of edges and vertecies
  28. in the graph. (Prolog terms can be represented as graphs, obviously).
  29. Reference: M.S. Paterson and M.N. Wegman, "Linear unification," J.
  30. Comput. Syst. Sci., vol. 16, pp. 158-167, Apr. 1978
  31.  
  32. Graph Unification that DOES detect infinite unifiability can run in just
  33. over linear time (specifically O(alphaE + V) where alpha is the inverse
  34. ackerman's function. This result is mentioned in the above paper, but an
  35. example is given in Vitter J.S. and Simons R.A., "New Classes for
  36. Parallel Complexity: A Study of Unification and Other Complete Problems
  37. for *P*" IEEE Trans. on COmp. Vol. c35, no. 5 May 1986 pp 403-417. Note
  38. that this function does not come up with the substitution, it just
  39. detects unifiable, infinitely unifiable, or neither.
  40.  
  41. Essentially what this tells us is that detecting infinite unifiability
  42. and coming up with a substitution (stronger than just an occurs check,
  43. is only "slightly worse" than not doing so. For practical problems, the
  44. inverse ackerman's function is a constant, after all. HOWEVER, this does
  45. not discuss the all-important "constant factor" by which we really live
  46. our daily lives (e.g. even if I gave you a polynomial function for
  47. reducing NP complete problems to P problems, it would be of tremendous
  48. theoretical importance, but little practical importance if it looked
  49. like (((10**10)**10)**10)n**312875. So it is really in this constant
  50. factor that the occurs check becomes important, and that is where we are
  51. hard pressed to look to theory for any concrete answers (it's easy to
  52. show that checking that a substitution is valid is linear, but it's hard
  53. to show any sort of constant factors for anything since that becomes
  54. architecture-dependant). We can only come up with experiments, and say
  55. things like "so far, it looks pretty bad to me".
  56.  
  57. If you want to argue against the efficiency position, it really isn't an
  58. argument to say that in this particular program, it makes little
  59. difference, you have to come up with an algorithm for doing compiled
  60. unification & infinite unification that is at least as efficient as the
  61. best known work for doing unification, on a particular architecture.
  62. Such work are not really solid theoretical results, since someone else
  63. can come along with a better way of doing straight unification, but such
  64. is science...
  65.  
  66. Personally, I feel compelled by the early prolog results too, so I've
  67. never pushed hard to even try to do infinite unification efficiently.
  68. I'd love it if someone pushed through an interesting result!
  69.  
  70. Regards,
  71. Brad Miller
  72.