🚀 go-pugleaf

In article <TORKEL.92Dec20104928@bast.sics.se> torkel@sics.se (Torkel Franzen) writes:
>In article <24454@alice.att.com> pereira@alice.att.com (Fernando Pereira)
>   >I agree. Adding the first-order theory of rational trees to the left of the
>   >|- is precisely restricting the class of models under consideration
>   >from arbitrary first-order models to rational tree models.
>
>   This is not so, since the class of rational tree models cannot be
>characterized by any set of first order axioms, any more than the finite
>tree models.
It cannot be characterized by any *finite* set of first-order formulas.
Notice that I used *theory*, not program in my note. The term "theory"
in logic means any deductively closed set of formulas. In fact, for a finite
signature you can characterize the finite tree models by a finite set
of equality and inequality formulas -- that's precisely what the Clark
completion uses. I don't have handy the relevant papers on rational tree
models, but I believe the same is true for them (papers by Joxan Jaffar and
Michael Maher?).

Anyway, this is just fine print, the main points have already been made clear:
(i) the occurs check is needed for sound deduction in pure first-order
logic; (ii) unification without the occurs check is sound for
deduction over rational tree models; (iii) Prolog unification (by this
I mean what was in Prolog originally) can construct rational terms,
but may not termfinate when unifying them; (iv) there are various
unification algorithms for rational trees, the asymptotically most efficient
of which I believe are all based on UNION-FIND (DFA equivalence). 

Fernando Pereira
pereira@research.att.com