Re: Editorial changes in Section 2.5

On 28 Jan 2006, at 07:09, Pat Hayes wrote:
>> I take it that G is
>>
>> :a :p _:bbb .
>> :a :q :e .
>
> OK, though G does not play any role here.
>
>> and that G' is
>>
>> :a :p _:b .
>> :a :q :e .
>
> Yes
>
>>
>> and that BGP is
>>
>> {?x :q _:b}
>
> Yes. Notice that they share a blank node.
>
>>
>> and that BGP' is
>>
>> {?x :q _:bb}
>
> Yes
>
>>
>> and that the instance S(BPG') is
>>
>> :a :q _:bb.
>
> Yes
>
>>
>> and anyhow find that G simply entails (G' union S(BGP'))
>> i.e.
>>
>> :a :p _:bbb.
>> :a :q :e.
>>
>> simply entails
>>
>> :a :p _:b.
>> :a :q :e.
>> :a :q _:bb.
>>
>> no?
>
> Yes, exactly. But it should not, because in this case G does NOT  
> simply entail (G' union S(BGP)).

And why it should? Where is it written? Remember that in the old  
chracterisation G' is required not to share any node with BGP, but in  
this example this is not true since they share _:b. What is important  
is that {?x/:a} *is* a solution in both the old and the latest  
characterisation - this is what we are characterising in the  
definition of BGP E-matching. See my example below.

> So in this case, that basic graph pattern should NOT match with  
> that solution. This answer is correct for BGP' , but it is not  
> correct for BGP. Which is what matters, since the definition is  
> supposed to be defining a match for BGP.

This is nonsense. Take the same G:

:a :p _:bbb .
:a :q :e .

and the same BGP:

{?x :q _:b}

According to the old definition, we need an arbitrary G' *not*  
sharing bnodes with BGP, for example:

:a :p _:bbbb .
:a :q :e .

Now, the solution {?x/:a} *is* a solution according to the old  
semantics, since the instance S(BPG) is:

:a :q _:b .

and (G' union S(BGP)) is:

:a :p _:bbbb .
:a :q :e .
:a :q _:b .

which is obviously entailed by G,
i.e.,

:a :p _:bbb .
:a :q :e .

simply entails

:a :p _:bbbb .
:a :q :e .
:a :q _:b .

So, the substitution {?x/:a} is actually a solution in both the old  
and the latest characterisation.
This is not a counter-example.

> The point is that we introduced G' in order, partly, to be able to  
> ensure that there were no 'accidental' bnode clashes between the G  
> and the BGP (and in part to ensure that all the answer bindings  
> used bnodes consistently with one another and with their pattern of  
> useage in G.)

Unluckily enough, in explaining your example you didn't take care of  
this important aspect.

> The original phrasing, in which we simply said that (G entails (G  
> union S(BGP))), was wrong, as Enrico noted, because G and BGP might  
> accidentally share bnodes, so there is a need to standardize them  
> apart.
> FUB suggested the directed merge trick to fix this; and then we  
> introduced the scoping graph G', and noticed that since G' could be  
> stipulated by definition to be standardized apart from all the  
> BGPs, there was no need to use a directed merge, because now a  
> simple union would do.

Exactly. And also with our latest characterisation, we make sure that  
there are no clashes by renaming the clashing existential variables  
(bnodes) in BGP - and we call BGP' this renamed BGP. We can legally  
do so since bnodes in BGP are scoped only locally to BGP, and since  
BGP' differ from BGP only beacuse there may be different bnode names.  
BGP and BGP' are SPARQL-equivalent since they give rise always to the  
same answers (in the old characterisation as well). So, once I take  
an appropriate BGP', and I make sure that BGP' does not share any  
bnode name with G', I satisfy the same conditions as in the old  
characterisation. By the way, this is an informal proof of the  
correctness of the latest characterisation.

> But by requiring the bnode-separation condition to hold not between  
> G' and BGP (as it should), but between G' and some variant BGP' of  
> BGP, we have rendered this condition vacuous, since BGP itself can  
> now share bnodes with G', which is exactly the situation we set up  
> all this machinery to avoid in the first place.
>
> I did not misread the definition: I suggest that y'all read through  
> the above carefully, and think about it.

We did it carefully. It is easy to see that the latest  
characterisation is correct, see above.
Convinced?

cheers
--e.