Re: Grist for layering discussion

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