- From: Peter F. Patel-Schneider <pfps@research.bell-labs.com>
- Date: Fri, 11 Jan 2002 11:28:54 -0500
- To: sandro@w3.org
- Cc: phayes@ai.uwf.edu, hendler@cs.umd.edu, timbl@w3.org, las@olin.edu, connolly@w3.org, w3c-semweb-ad@w3.org, www-archive@w3.org
From: Sandro Hawke <sandro@w3.org> Subject: Re: Grist for layering discussion Date: Fri, 11 Jan 2002 10:42:06 -0500 [...] > > The third price is that we have introduced a form of reification and a > > construct that can assert the truth of reification constructs. This > > (probably) doesn't cause any problems here because the extension is so > > expressively limited. However, for more powerful extensions reification > > produces paradoxes, and thus cannot be used. > > Two answers here. > > 1. I've heard some people say, "Who Cares?" Operationally, what's > the problem with a paradox? My guess is it will show up as infinite > loops and/or bottomless recursion, which is unpleasant but can be > managed as a resource-management problem. That is, in theory there's > a huge difference between a paradox and a problem that will simply > take 4 hours to terminate, but operationally they're both just systems > that go off into the weeds. The user presses "stop" and everything's > fine again. Who cares? Just the people that matter, that's all. By the ``people that matter'', I don't mean just Pat and myself, I mean anyone who wants to implement or work with the formalism. A formalism with a paradox is fundamentally broken. The breakage can appear in several ways. For standard logics the breakage will often show up as a breakdown in the retrieval specification. For example, consider initial versions of set theory that allowed the creation of { x : x not in x }. In a formalism that includes this paradox it is generally possible to reason as follows: Assume that John is in { x : x not in x } Then John is not in { x : x not in x }. Contradiction, so John is in { x : x not in x } implies that it is snowing. Assume that John is not in { x : x not in x } Then John is in { x : x not in x }. Contradiction, so John is not in { x : x not in x } implies that it is snowing. Thus it is snowing. So the operational result of this paradox is not an infinite regress, but instead the production of any consequence whatsoever (and very quickly). A reasoner based on model theory could be even faster. There are no models for KBwhatever. Therefore it is snowing is true in all models for KBwhatever. Reply that it is snowing. Again, no long computation, just strange results. Some operational characterisations of paradoxes do result in infinite regresses. However, infinite regresses are *very* different from expensive but terminating computations. It is possible, and has been done many times in the past, to take a problem that appears to be computationally very exensive (think heat death of the universe timing) and come up with a clever optimisation that results in a system that solves the problem almost instantaneously. Look at recent description logic provers for examples of this kind of improvement. The difference here is not between two apparently-computationally-unobtainable results. Instead the difference is between an apparently-computationally-unobtainable result and a result that is not defined. This is a qualitative different, not a quantitative one, and, moreove, a difference that has visible and far-reaching results. > 2. I don't really like systems going off into the weeds. And I don't > see why they have to, if we're careful about the feedback loop. That > is: reasoners should not look for their inputs in their own outputs. You can, of course, terminate a computation if you think that it is going into a loop. However, what result are you going to return? > Can that loop be avoided if there are two reasoners...? Hm. I think > so, but it might be expensive. How? > If you still say that wont work, is there some system I can construct > (in code or just detailed specification) to demonstrate it will? Like > finishing up my FOL-encoded-in-RDF system? If I can have RDFS and FOL > reasoners properly attached to the same database, would that be > convincing? (That's kind of a silly case since RDFS can be done with > FOL axioms, but I wouldn't implement it that way here. Maybe some > floating-point math thing.) Sure. You will have to provide a specification as to how this is going to work that is an extension of RDF and that provides all of FOL. You will also have to abide by both the letter and the spirit of my definition of extension. (I put the ``spirit'' condition in here because my definition is informal and thus does not cover all eventualities.) > -- sandro peter
Received on Friday, 11 January 2002 11:29:18 UTC