Re: worries about useMentionOp and how queries relate to rules and proofs

>Pat,
>
>I can't quite put my finger on it, but I'm afraid there are
>some serious architectural use/mention issues with operators like
>BOUND, URI-equal, isURI, and isBlank
>   http://www.w3.org/2001/sw/DataAccess/issues#useMentionOp
>
>As I see the architecture, a query plays the role of
>a conjecture to be proved. A query solution is a sketch
>of a proof.

That is one way to think about it, which I find congenial myself. 
Another way is that the target graph is like a dark pool of triples, 
and the query is like fishing or casting a net into the pool to see 
what you can catch. I think some of the WG think more like the second 
than the first. Yet another way is the DB idea of thinking of a query 
as a kind of algebraic filter applied to a table, which only lets the 
answers through; this gives you a much more algebraic view of query 
languages, where they consist of 'operators'. I think SQL is partly 
based on that idea.

>If I write
>
>  SELECT ?who
>  WHERE ?who foaf:name "Dan Connolly"
>
>it's akin to asking a theorem prover to prove:
>
>   exists (x) such that foaf:name(x, "Dan Connolly")
>
>The solution "?who binds to <danshomePage#topic>"
>is a sketch of a proof (I think the literature
>uses the term "witness" for this sort of thing).

Right. Though in this case I think that 'sketch of a proof' might be 
a bit of an overstatement. I think of it as more like the bindings 
produced by a proof.  For RDF these are almost the same thing because 
proofs are so simple, but when we move to OWL or (still more so) a 
rules reasoner which answers queries against a closure graph (like 
cwm?) the disparity between the proof and the final variable bindings 
becomes more extreme. Still, this is probably just niggling , I see 
your basic point.

>
>Now I can't imagine how to turn
>
>  SELECT ?who
>  WHERE ?who foaf:homePage ?x
>    AND isURI(?x)
>
>into a conjecture to be proved by a theorem prover.
>isURI() is not a function of objects in the
>domain of discourse, but an operator that distinguishes
>one sort of term from another.

Right. Its a kind of meta-constraint on the TP rather than an 
assertion in the logical language. Still, its meaningful, and you 
could even axiomatize it if your language doesnt have equality 
(though that would be a hack, and would break when you extended the 
language).

>We might have
>
>	<dansHomePage#topic> owl:sameAs _:somebody .
>and by definition
>	isURI(<dansHomePage#topic>)
>but not
>	isURI(_:somebody)
>
>This sets off flags in my mind, but I can't state,
>in black-and-white, testable ways that matter to
>applications and coders, why it matters.

Well, one thing to say is that constraints on the form of results, 
like this, are not themselves expressible in RDF, so cannot be sent 
downstream from the query itself. Also there might be some nasty 
interactions between these and the UNSAID  construction, but I only 
just thought of that one and will need to think more.

>Does it worry you?

Yes and no.  Or maybe, I've learned to stop worrying. That is, I wish 
the world were logically neat, but I gave up years ago thinking it 
was going to actually be logically neat. And one CAN give a neat 
story about things like this, by talking about metalevel constraints, 
or constraints on the syntactic form, and so forth. And they clearly 
seem to be useful in practice: and who are we to limit what kinds of 
software might want to fiddle around with RDF query results?

Also, you know, RDF has always flirted with this use/mention issue: 
reification was kind of ambivalent about it, and the idea of 
rdfs:Literal kept sliding back and forth between meaning literal 
values and actual  literal forms, and as far as I can see the new XML 
Schema part 2 doesnt even talk about values in the RDF sense at all. 
If you are thinking in terms of code and structured programming 
models and so forth, its all 'form', and the model-theoretic stuff is 
just a kind of Platonic fantasy: so what's wrong with looking at the 
URIs and checking that they really are URIs (say)? I can see the 
force of this POV.

>p.s. formally this is a WG issue
>   http://www.w3.org/2001/sw/DataAccess/issues#useMentionOp
>In Helsinki, we has some relevant discussion and made
>a nearby decision, but it wasn't explicitly a decision
>to close this issue.
>
>   RESOLVED: BOUND keyword and no UNSAID to address common
>   UNSAID issues. KendallC abstaining
>   http://www.w3.org/2001/sw/DataAccess/ftf4.html#item04

Sigh, I havnt been keeping up with BOUND and these discussions, my 
bad. I'll try to get up to speed soon (after MOnday: we have some 
awful deadlines looming)

>
>I'm trying to figure out whether to open substantive discussion
>of this useMentionOp issue or just say "oh... yeah, we meant to close
>that one too, didn't we?"

My guess is that it will be a lead balloon. After all, if you have 
some neat app in mind, to be told that you shouldn't do a simple 
thing because a logician thinks that it violates his dream of the way 
the world should be, isn't likely to resonate very strongly, if you 
take my meaning. And after all, these form-restrictions are perfectly 
meaningful: its just that they are syntactic rather than semantic. 
But why shouln't a query language allow syntactic constraints on 
answers? Even reasoning engines do things like that to recognize 
call-out cases and apply optimizations, after all.

Pat

PS all in haste, more later.

>
>
>--
>Dan Connolly, W3C http://www.w3.org/People/Connolly/
>D3C2 887B 0F92 6005 C541  0875 0F91 96DE 6E52 C29E


-- 
---------------------------------------------------------------------
IHMC		(850)434 8903 or (650)494 3973   home
40 South Alcaniz St.	(850)202 4416   office
Pensacola			(850)202 4440   fax
FL 32502			(850)291 0667    cell
phayes@ihmc.us       http://www.ihmc.us/users/phayes