🚀 go-pugleaf

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