Re: Circular Multi-Orgls & Logic Programming

[Michael McClary <michael>]

> 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.

That's fine for theorem-provers.  It doesn't work for knowledge-
representing structures intended for human browsing.  (Which may
have little bearing on ent internals.)  Structures representing
the visual appearance of the Pet Milk can label are broken either
way, since in the first case it doesn't represent the label, and
in the second case the rendering engine infinite loops.

> 2) "It is an error".  []
> The consequences of violating this contraint in a program
> could lead to infinite loops, and (I think) to seemingly valid
> termination with invalid outputs.

I suspect just infinite loops.

> 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.

Right.

> 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.
> 
> []
> Eventually I would like us to use solution #3, [].  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.

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.

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...)

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.

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)?

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

	michael