Circular Multi-Orgls & Logic Programming

[Mark S. Miller <mark>]

Awhile ago, in a conversation with Ravi, the subject of circular
multi-orgls came up.  I gave him the standard answer: "since orgls are
side-effect free, they can only contain orgls which are already there,
and therefore we don't have to worry about circular (or infinite)
multi-orgl containment.".  Since then, it's occurred to me that the
introduction of partial orgls into the semantics invalidates this
statement.

In fact, with the introduction of partial orgls, the situation is less
like that in a functional programming language, and more like that in
a logic programming language.  (In retrospect, this is not surprising,
in that partial orgls were inspired by the power of stream programming
in FCP.)  In a functional programming language, all values are like
our orgls were before the introduction of partiallity, and like most
of the X++ data types (such as Sets & Tuples) are right now: they are
fully formed when they are born, and never change after that (except
to have their storage reclaimed, which is considered to be at a lower
level of semantics).  In most functional programming languages,
therefore, it is impossible to form circular data structures (an
exception would be a language in which you could give bith to a
circular structure "all at once").

In logic programming languages, we are still "side effect free" in the
sense that we cannot change the value of a given data structure.
However, we don't have to fully determine the value at the time we
create the data structure.  Instead, we can use "logic variables"--
place holders for components of the value that are yet to be
determined.  At a later time, we can fill these place holders in, in
which case the original value is more fully determined.  As
computation proceeds forward (I will ignore backtracking, which
doesn't exist in FCP or most related languages), more of the contents
of partial structures are determined or "discovered".  It is a valid
and interesting point of view to consider the final value of the
structure as having been the true value all along.  Early in the
computation we were ignorant of most of it, but it was uncovered as we
proceeded.  If we push this point of view too far, we can get into the
kind of "determinism vs free will" pseudo-paradoxes that philosophers
who don't program are generally very confused about, but we don't have
to worry about that, as we will not push it that far ;->

Now when logic programming took this step, it had to face the same
circularity problem we now do.  The reason is that one could now
create a partial structure, and then fill in a piece by designating
the whole.  I know of only three alternatives for dealing with this
issue, each of which has been applied by some logic programming
language: 

1) The "occur check".  This solution simply outlaws circularities.
The name refers to the action of checking whether the value with which
we are filling in a logic variable place holder contains that very
placeholder.  If it does, then the filling in operation is rejected.
For some obscure reason that I don't understand in first order logic,
it is allowed to simply reject the operation as if to say "no valid
solution lies down that path".  Could any logicians in the audience
explain why we're allowed to do this, I never did understand it.

The theorem provers which are the historic roots of Prolog generally
all did the occur check.  However, when the creators of Prolog wanted
to turn this theorem proving machinery into efficient programming
language machinery, they found the occur check was causing a
*tremendous* cost in execution time (I think it turned unification
(the filling in operation) from being O(N) to O(N^2) in the size of
the structures being unified), while never having an effect on
"normal" Prolog programs.

2) "It is an error".  By removing the occur check, they were able to
figure out how to implement Prologs at speeds exceeding that of Lisp
(even on Symbolics hardware which had been extensively tuned for
Lisp).  Instead, they provided ... (drum roll) ... nothing!  They
simply defined it as an error for a Prolog program to ever do a
unification that would have failed the occur check.  The occur check
moved from the implementation into the definition of a "valid
program".  The consequences of violating this contraint in a program
could lead to infinite loops, and (I think) to seemingly valid
termination with invalid outputs.

This is a situation that most programming languages impose on their
users at every turn--for example the consequences in C or Pascal of
storing through an uninitialized pointer are even more unpredictable.
Nevertheless, because of the cultural roots of Logic Programming, this
non-solution grated on the nerves of many, and many attempts at a way
out were tried.  The one which worked is that built into Prolog II
(solution #3).

Note that this kind of non-solution (#2) is totally unsuitable for
Xanadu, in that the back-end must be shared server which continues to
provide valid service in response to valid requests, even if it gets
invalid requests.  If an invalid request would mess up the back-end,
then the back-end MAY NOT depend on its users to not send such a
request.  It must instead detect such a request itself and properly
reject it & survive.  If we decide that informing a partial orgl in
such a way that it becomes circular is invalid, then we must detect
and reject it.  This would correspond directly to the occur check
solution (#1).  I don't yet have a feel for whether this would have
performance consequences like it had for Prolog.  Or we could do what
Prolog II did.

3) Generalize.  Prolog II allows circular structures just fine.  The
unification algorithm had to be significantly changed so that it
worked correctly on circular structures, and a generalization of first
order logic had to be invented so that "correctly" could be defined.
Since Prolog II structures (like our orgls) had no EQ-ness identity,
the semantics were not that such a structure is circular, but that it
is infinite.  However, the class of infinite structure which can be
represented by a circular structure has much the same relationship to
general infinite structures that rational numbers have to real
numbers.  Hence they called these infinite structures "rational
trees".  It turned out that the algorithm for unification of rational
trees when run on non-circular structures only cost about 10% more
than Prolog's unification, whereas to check for and reject potential
circularities was much more expensive.

The really pleasant surprise was that the introduction of rational
trees into the language also made it a more pwerful and elegant
language.  A beautiful example is a recursive descent parser written
in Prolog II.  It derives its beauty from the representation of an
entire BNF grammer as a rational tree, which is then passed as a
single argument to the parsing program.

What does all this mean for us?  I suggest we start with solution #1.
This means that our inform operations have to check for and reject
circularities, but on first blush I think we can do so efficiently.

Given that we are hiding the orgls&berts layer for now, we could
theoretically adopt solution #2, and specify that the docs&links layer
must not ever create a circular structure or the back-end will be
invalid.  I would really hate it if we did this, as the correctness of
the system up through the orgls&berts layer really shouldn't depend on
any property of the docs&links layer.  

Eventually I would like us to use solution #3, which means defining
and implementing backfollow, version compare, copy, transform, etc...
all on rationally infinite multi-orgls.  I think this will take some
thought.  Note that if we start with solution #1, but we document the
rejection of circularity as the rejection of the attempt to invoke a
not yet implemented feature, then we can upgrade to solution #3 when
we understand what it means.

Comments?  Was this at all clear?