[Date Prev][Date Next][Thread Prev][Thread Next][Author Index][Date Index][Thread Index]

*To*: <michael>*Subject*: Circular Multi-Orgls & Logic Programming*From*: Mark S. Miller <mark>*Date*: Mon, 23 Oct 89 16:11:38 PDT*Cc*: <xanatech>*In-reply-to*: <Michael>,28 PDT <8910222214.AA21905@xanadu>

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.

**Follow-Ups**:**Circular Multi-Orgls & Logic Programming***From:*Eric Dean Tribble

**References**:**Re: Circular Multi-Orgls & Logic Programming***From:*Michael McClary

- Prev by Date:
**iterations** - Next by Date:
**UnaryFns & Tables** - Previous by thread:
**Circular Multi-Orgls & Logic Programming** - Next by thread:
**Circular Multi-Orgls & Logic Programming** - Index(es):