home *** CD-ROM | disk | FTP | other *** search
/ NetNews Usenet Archive 1992 #31 / NN_1992_31.iso / spool / comp / lang / prolog / 2279 < prev    next >
Encoding:
Internet Message Format  |  1992-12-21  |  2.1 KB
  1. Path: sparky!uunet!spool.mu.edu!yale.edu!ira.uka.de!sbusol.rz.uni-sb.de!gs-serv3.dfki.uni-sb.de!dfki.uni-sb.de!smolka
  2. From: smolka@dfki.uni-sb.de (Gert Smolka)
  3. Newsgroups: comp.lang.prolog
  4. Subject: Re: Occurs check
  5. Date: 21 Dec 1992 14:17:49 +0100
  6. Organization: DFKI - German Research Center for AI
  7. Lines: 32
  8. Sender: gs-soft@gs-serv3.dfki.uni-sb.de
  9. Distribution: world
  10. Message-ID: <1h4g5tINN5l6@eagle.dfki.uni-sb.de>
  11. References: <1992Dec13.173016.8849@nntp.hut.fi> <1992Dec17.111142.24450@dcs.qmw.ac.uk> <24435@alice.att.com>
  12. NNTP-Posting-Host: gs-serv1.dfki.uni-sb.de
  13.  
  14. In article <24435@alice.att.com>,
  15. pereira@alice.att.com (Fernando Pereira) writes:
  16. |> If you want to program with cyclic terms, you have gone outside
  17. |> bare first-order logic to a system in which terms are interpreted
  18. |> in a different way. The theoretical framework and practical value
  19. |> of that alternative were established with the Prolog II work at Marseille,
  20. |> and there's certainly a sound way of thinking about Prolog with cyclic
  21. |> terms. However, as far as I know there is no free lunch. Sound and
  22. |> terminating unification of cyclic terms can be more costly than
  23. |> unsound Prolog unification.
  24.  
  25. I seriously doubt that rational tree unification pays any significant
  26. efficiency penalties in practise over Edinburgh-style unification
  27. without occurs check.  As has been mentioned by Torkel before,
  28. UNIFICATION IN SICSTUS IS RATIONAL TREE UNIFICATION, and Sicstus seems
  29. to be rather efficient.
  30.  
  31. Isn't it strange that the forthcoming Prolog standard will explicitly
  32. accept implementations of unification that may not terminate on certain
  33. terms.  I certainly understand that finite tree unifications is needed
  34. for some interesting applications.  However, given the efficiency and
  35. the clean *logical* status of rational tree unification, I would expect
  36. that rational tree unification is taken as default and finite tree
  37. unification is accommodated as a built-in predicate.
  38.  
  39. By the way, was it Edinburgh or Marseille which first dropped
  40. the occurs check?
  41.  
  42. -- 
  43. Gert Smolka, DFKI, Stuhlsatzenhausweg 3, D-W-6600 Saarbr"ucken, Germany
  44. Tel: +49 681 302-5311;  Fax: +49 681 302-5341; Net: smolka@dfki.uni-sb.de
  45.  
  46.