home *** CD-ROM | disk | FTP | other *** search
/ NetNews Usenet Archive 1992 #30 / NN_1992_30.iso / spool / comp / lang / prolog / 2274 < prev    next >
Encoding:
Internet Message Format  |  1992-12-21  |  2.3 KB
  1. Path: sparky!uunet!europa.asd.contel.com!howland.reston.ans.net!usc!zaphod.mps.ohio-state.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: <24458@alice.att.com>
  6. Date: 20 Dec 92 22:53:14 GMT
  7. Article-I.D.: alice.24458
  8. References: <1992Dec13.173016.8849@nntp.hut.fi> <1992Dec17.111142.24450@dcs.qmw.ac.uk> <24435@alice.att.com> <TORKEL.92Dec17201903@bast.sics.se> <24439@alice.att.com> <TORKEL.92Dec18231028@lludd.sics.se> <24454@alice.att.com> <TORKEL.92Dec20104928@bast.sics.se>
  9. Reply-To: pereira@alice.UUCP ()
  10. Organization: AT&T, Bell Labs
  11. Lines: 31
  12.  
  13. In article <TORKEL.92Dec20104928@bast.sics.se> torkel@sics.se (Torkel Franzen) writes:
  14. >In article <24454@alice.att.com> pereira@alice.att.com (Fernando Pereira)
  15. >   >I agree. Adding the first-order theory of rational trees to the left of the
  16. >   >|- is precisely restricting the class of models under consideration
  17. >   >from arbitrary first-order models to rational tree models.
  18. >
  19. >   This is not so, since the class of rational tree models cannot be
  20. >characterized by any set of first order axioms, any more than the finite
  21. >tree models.
  22. It cannot be characterized by any *finite* set of first-order formulas.
  23. Notice that I used *theory*, not program in my note. The term "theory"
  24. in logic means any deductively closed set of formulas. In fact, for a finite
  25. signature you can characterize the finite tree models by a finite set
  26. of equality and inequality formulas -- that's precisely what the Clark
  27. completion uses. I don't have handy the relevant papers on rational tree
  28. models, but I believe the same is true for them (papers by Joxan Jaffar and
  29. Michael Maher?).
  30.  
  31. Anyway, this is just fine print, the main points have already been made clear:
  32. (i) the occurs check is needed for sound deduction in pure first-order
  33. logic; (ii) unification without the occurs check is sound for
  34. deduction over rational tree models; (iii) Prolog unification (by this
  35. I mean what was in Prolog originally) can construct rational terms,
  36. but may not termfinate when unifying them; (iv) there are various
  37. unification algorithms for rational trees, the asymptotically most efficient
  38. of which I believe are all based on UNION-FIND (DFA equivalence). 
  39.  
  40. Fernando Pereira
  41. pereira@research.att.com
  42.  
  43.  
  44.