🚀 go-pugleaf

In article <8227@agate.BERKELEY.EDU> weemba@garnet.berkeley.edu (Obnoxious Math Grad Student) writes:
>The axioms they use, in an intuitive form due
>to Aczel, lead to unique sets with any given pattern of abstract cir-
>cular reference, eg, there is only one x such that x={x}, only one y
>such that y={0,y}, etc.
I'm reminded of Alain Colmerauer's handling of self-referential
trees [see, for example, Proceedings of the Int'l Conf. on 5th Gen.
Computer Systems, 1984] in which the task is to tell whether two
data structures (let's say, trees) with unbound variables at some of
the nodes can be unified by a suitable assignment of variables, and
if so what this assignment is in a least Herbrand model (the "least"
allows for unique solutions -- it's not actually true that there is
only one x such that x={x}, but there's a unique minimal solution.
Somebody correct me if I'm taking the name of Herbrand in vain.)  And
in fact most of his examples look like "find y such that y = (0 y)".

Colmerauer gives algorithms for solving systems of simultaneous
equations (and "inequations", i.e. "x CANNOT be unified with y" as
opposed to "x is not NECESSARILY unified with y", which is the usual
understanding of "not" in a Prolog system) of this sort, and I did
an undergrad independent study implementing (in Prolog) a Prolog
interpreter using said algorithms as a unifier.

The rest of the book review is fascinating, too, and I'll try to
find the book.
				Another Obnoxious Math Grad Student
					Steve Bloch