RIF Core Lists as Skolem Functions / Constructors

On Tue, 2010-07-27 at 23:36 +0100, Dave Reynolds wrote:
> > However, I'm pretty sure we did add new-node-construction into RIF
> > Core, although we may not have realized it at the time.  Specifically,
> > the list constructor (or at least the list builtins) act like a Skolem
> > function. 
...
> >    Of course, the slightly sneaky way this is done may mean
> > it wont be correctly implemented.  Someone should provide some test
> > cases on this...
> > 
> > Let's see:
> > 
> >    if x uncle y then exists z: x father z and y brother z
> > 
> > in BLD, with a Skolem function sk1 replacing the existential:
> > 
> >    forall ?X ?Y (
> >       And( ?X[parent->sk1(?X ?Y)] 
> >            sk1(?X ?Y)[brother->?Y] ) :- ?X[uncle->?Y]
> > 
> > and in Core, using a list constructor, and a per-application skolem
> > constant my:sk1 (which should be unique per rule):
> > 
> >    forall ?X ?Y (
> >       And( ?X[parent->func:make-list(my:sk1 ?X ?Y)] 
> >            func:make-list(my:sk1 ?X ?Y)][brother->?Y] ) :- ?X[uncle->?Y]
> > 
> > and fact:
> >    my:sandro[uncle->my:martin]
> >    
> > entails:
> >    exists ?P And(my:sandro[parent->?P and ?P[brother->my:martin])
> > 
> > 
> > Any comments on that now, or should I put it on the wiki?   (cleaning
> > up the syntax/qname a bit.)
> 
> Hmmm. 
> 
> I guess that's correct but you are right it won't be correctly
> implemented. Most RDF systems essentially use skolem constants for
> bNodes, including list elements, so identifying two lists because they
> have the same elements would lead to problems, especially with SPARQL. 
> 
> A SPARQL query of the form:
> 
>     SELECT ?P {my:sandro my:parent ?P. ?P my:brother my:martin. }
> 
> over a plain graph:
> 
>    my:sandro my:parent (my:sk1 my:sandro my:martin) .
>    (my:sk1 my:sandro my:martin)  my:brother my:martin .
> 
> returns no results.
> 
> This may be an issue for the SPARQL RIF entailment regime. Does this
> mean that the entailment regime should specify that the RDF graph
> closure entailed by RIF should be "leaned" (as in "made lean") before
> applying the SPARQL graph pattern? 
> 
> That way the behaviour of the SPARQL query would match the corresponding
> "exists ?P .." RIF formula.
> 
> At the cost of introducing an NP complete operation in the middle of
> what would otherwise be a polynomial problem. Ugh.

Although making the graph lean would address this particular instance
data, I think RIF entailment would also give this result if, for
instance, the list nodes had URI labels (instead of being blank nodes).
And making the graph lean wouldn't help with that.

I think this result follows, instead, from the bidirectional mapping
between RDF collections and RIF lists.  I'm not sure, but that strikes
me as a polynomial problem [which, with typical data, I bet will be
slower than graph leaning would be :-)  ].   

    -- Sandro

Received on Wednesday, 28 July 2010 15:50:39 UTC