Re: substantive semantics change?

In brief: pending confirmation from Brian, I'm inclined to
agree with Pat that this is an editorial change. It
seems to be consistent with the proceedings of the WG
and responsive to a comment.

Details...

On Wed, 2003-11-12 at 11:04, pat hayes wrote:
> >pat:
> >>  > 8. (related). The definitions of rdf and rdfs entailment have been
> >>  > simplified so that they do not make explicit reference to a
> >>  > vocabulary. This is actually more conventional; and Herman pointed
> >>  > out that the more complicated definitions meant that entailment might
> >>  > not be transitive (aargh). The motive for introducing this
> >>  > complication in the definition in the first place has been removed by
> >>  > subsequent changes. This doesn't change any test cases.
> >>  >
> >jeremy:
> >>  My understanding is that test cases do change - in particular the
> >>  test cases
> >>
> >>
> >>  >   rdfms-seq-representation/Manifest.rdf#test002
> >>  >   rdfms-seq-representation/Manifest.rdf#test004
> >>
> >>  which were incorrect according to the LC2 semantics doc, now
> >>  become correct.

Euler and Surnia seem to agree that they're correct.
3store disagrees with test004, but I'm inclined to
chalk that up as a bug.
http://www.w3.org/2003/11/results/rdf-core-tests#ByTestType_table_2_Approved


> >>  So this is a substantive rather than an editorial change. (I am awaiting
> >>  feedback from HP implementors concerning this)
> >>
> >
> >Further, as far as I understand, the Last Call 2 doc had the empty document
> >entailing only a finite number of ground triples
> 
> No, it has always entailed an infinite number of them of the form
> 
> rdf:_n rdf:type rdf:Property .

That has never been entirely clear to me, so I take this
opportunity to catch up on the details... The test above
are named after issue
http://www.w3.org/2000/03/rdf-tracking/#rdfms-seq-representation

The only WG decision I can find under that issue is about
the first/rest style collections, so as far as I can tell,
the WG has never explicitly instructed the editor, but
implicitly accepted the design in the LC1 and LC2 semantics
documents (by deciding to go to last call, i.e. deciding
that all issues are closed ot the WG's satisfaction).
The manifest for the tests cites the 10 Jan minutes as approval
http://lists.w3.org/Archives/Public/w3c-rdfcore-wg/2003Jan/0025.html
I don't see a decision there, but item 6 notes a number
of completed actions. I'm having trouble finding the relevant
one; perhaps it was a consequence of a relevant WG decision.
I can't tell.

Anyway...


It seems important to distinguish between simple entialment,
RDF entailment, and RDFS entialment in these cases.
The empty graph does not simply-entiail rdf:_1 type Property;

"Empty Graph Lemma. The empty set of triples is entailed by any graph,
and does not entail any graph except itself."
 -- http://www.w3.org/TR/2003/WD-rdf-mt-20031010/

Ah... I concur with Pat; the LC2 doc is pretty clear
that the empty graph rdf-entials rdf:_1 type Property
and infinitely many triples like it;
the "RDF axiomatic triples" box is quite explicit on that.
http://www.w3.org/TR/2003/WD-rdf-mt-20031010/#InterpVocab



> They weren't in the 'closure', as we once defined it in the
> closure lemmas - and that was the point of going through all this 
> contortion involving crdfV - but they were entailed, in the sense that
> 
> { } entails {rdf:_n rdf:type rdf:Property .}
> 
> was a true statement (in LC2 and now.)  Since the lemmas are no 
> longer stated in terms of closures, and that was the only reason for 
> the crdfV restriction, this change seemed to me to be purely internal 
> to the semantics.
> 
> >, whereas the current
> >editors draft has the empty document entailing an infinite number of ground
> >triples.
> >HP is unlikely to implement such a change, and would oppose it, if it were
> >formally proposed.
> 
> Well, Im not sure what that word 'implement' means. The MT doesn't 
> constrain a reasoner to be strongly complete wrt entailment, and 
> certainly not a forward rule-based reasoner. But this is an issue 
> with forward reasoners in just about any language. Such a reasoner 
> for propositional calculus would have the same issue: the set of 
> tautologies is infinite.
> 
> >Moreover, since this substantive change (assuming my understanding is
> >correct) had not been highlighted before the PR vote, we may need to ask the
> >chairs to rewind history a little.
> >
> >I don't follow the transitivity argument ...
> >
> >G entails H if every interpretation of G is an interpretation of H.
> >
> >this is clearly transitive
> 
> Yes, phrased this directly it is, which is why I like this direct 
> phrasing.  LC2 doesnt state it this directly, which is where the 
> problems arose.
> 
> Pat
> 
> >, and a "counter-example" like
> >
> >*empty*
> >   entails
> >rdf:_1 rdf:type rdfs:Resource
> >   entails
> >rdf:_1 rdf:type rdfs:ContainerMembershipProperty
> >
> >is flawed because the first entailment is false according to the LC2
> >semantics.
> >
> >Is it possible to undo some of the changes to semantics without it falling
> >apart, leaving hermann and/or peter dissatisfied?
> >
> >Jeremy
-- 
Dan Connolly, W3C http://www.w3.org/People/Connolly/

Received on Wednesday, 12 November 2003 12:52:50 UTC