Circular Multi-Orgls & Logic Programming

[Mark S. Miller <mark>]

Date: Sun, 22 Oct 89 15:14:28 PDT
   From: michael (Michael McClary)

   > From mark Sun Oct 22 00:30:35 1989
   > 
   > 1) The "occur check".  This solution simply outlaws circularities.
   > []
   > 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.

   That's easy:

     - A solution exists down that path IFF it exists on one of the
       paths you're already considering that DON'T loop.  Therefore:

     - Ignoring all paths that loop won't lose the solution, but:

     - If you consider the path that loops before you consider the
       one that leads to a solution, you will do it again as you
       follow the loop, and never find the solution.

I don't think that circularity in the structures themselves
corresponds to a circularity in the proof process.  However, there may
be some tricky equivalence here by which your answer does apply.  This
being logic, there are even more tricky, non-intuitive equivalences
than in normal programming.  I don't know.

   I think we need to answer two questions quickly.  First, is it
   possible to actually need/generate a looping tree in the usage
   of the backend, as currently contemplated?  (This includes "mistakes"
   from time-delays between multiple requests/threads/backends.)
   If not, solution 2 works.

Once again, this probably works, but I would be nervous if the
integrity of the orgls&berts layer depended on the docs&links layer.

   If so, we should look at what's actually involved in solution 3,
   and how often we do inform.  Solution 1 seems to square the
   complexity measure of inform, so it could produce a BAD
   performance hit.

   Does solution 1 actually square the complexity measure?  Or is it
   just the way it was implemented?  I suspect they walked the tree
   for each crum added, to see if it was already there.  Keeping a
   hash of something unique about each crum would reduce the order
   of that approach.  On the other hand, if it's the entire ent you
   must check against, N is ALWAYS very large, but the hash list
   could be kept around.  (Perhaps it is already...)

Hopefully we'll have some info on this soon.  

   I suspect solution 3 involves a "here there be dragons swallowing
   their tails" bit, and mods to follow operations s.t. they remember
   which marked crums they've visited, and don't pass them twice.
   Is this correct?

   I also suspect loops, if allowed, will play HELL with tree-balancing.

As we verbally discussed, if we do internally have a way of telling
which pointers are "upwards", such as your "dragons" bit, then we can
balance the *tree*s that result from ignoring exactly these pointers. 

   What about loops that are closed only through two backends?  They're
   guaranteed to cause trouble when you suck the bight into your local
   machine.  How can you reject them then?  How can you prevent them
   without making informs wait on a poll of (potentially all) backends
   (including archives and down machines)?

I strongly suspect that proper consideration of Bebe, especially in a
mutually mistrustful distributed system, will force us into solution
#3.  We should still be able to get away with #1 in first product
unless archiving throws a rationally infinite wrench into the works.
Dean? 

   (How much of this letter reveals a profound lack of understanding
    of Xanadu internals?  B-) )

Only the parenthetical question at the end.