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