🚀 go-pugleaf

In article <1992Dec17.111142.24450@dcs.qmw.ac.uk> mmh@dcs.qmw.ac.uk (Matthew Huntbach) writes:

MH   I have written programs which rely on the occur-check not
MH   happening, since they intentionally build circular structures.
MH   What should be so wrong with this - after all it's a standard
MH   programing feature in lazy functional languages.

If you allow cycles, you change the term universe.
A solution to a goal t=u where t and u are first order terms should be
a substitution (a mapping from variables to first-order terms) sigma,
such that sigma(t)=sigma(u).  Because sigma is a first-order
substitution, the resulting terms are first-order too.

If you are using unification without occur-check, then the
substitution might not be first-order, the substituted terms can
contain cycles. One can express this semantically by adding a fixpoint
operator to the term universe.
You are right that it is often useful to have cyclic terms;
but they live in this different term universe
and Prolog's = is an incomplete unification there, e.g. the goal
	A=f(A), B=f(B), A=B
usually fails to terminate, although it should either fail (in the
Herbrand universe) or succeed (in the extended universe).
It is possible to extend unification with a cycle check to make it
terminate even for cyclic terms (some Prologs have such a thing; I
even know a programming language which uses unification with cycle
check for type inference), but this is again less efficient than
ordinary = , probably similar in efficiency to unification with occur
check.

--
Stefan Kahrs	                   JANET:    smk@uk.ac.ed.dcs
LFCS, Dept. of Computer Science    Internet: smk@dcs.ed.ac.uk
University of Edinburgh            UUCP:     ..!mcsun!uknet!dcs!smk
Edinburgh
EH9 3JZ                            Tel:      (44)-31-650-5139
SCOTLAND                           Fax:      (44)-31-667-7209