Re: PROV-ISSUE-576: logical definition and comments on prov-constratins [prov-dm-constraints]

Just to say I've put on the agenda this week a discussion so James can get confirmation.

Thanks
Paul

On Oct 23, 2012, at 20:14, James Cheney <jcheney@inf.ed.ac.uk> wrote:

> 
> On Oct 23, 2012, at 7:08 PM, Ivan Herman wrote:
> 
>> James,
>> 
>> I am fairly o.k. with your answer although, I must admit, I did not dive into all the details of what a declarative approach would look like.
> 
> Well, it's essentially what the commenter proposes (a first-order theory, plus a little more glue in sec. 2 or non-normative appendix explaining how it relates to the existing procedural spec).  I have a pretty good idea what this should be, but it hasn't been written down yet.  Just want to get a sense of whether the group is happy with this approach before putting more effort in.
> 
>> But I do not see a pressing reasons to change the current document.
>> 
>> One comment below:
>> 
>> On Oct 23, 2012, at 13:56 , James Cheney wrote:
>> 
>>> Hi,
>>> 
>>> These comments came in after the deadline for comments on PROV-CONSTRAINTS, but given the absence of other detailed comments I believe we had better respond to them.
>>> 
>>> The editors/contributors (Luc, Paolo, Tom, Paul, me) have discussed the comments a bit already, and I will try to synthesize a response based on this discussion by this Thursday, in order to allow time for broader discussion, and adoption of any non-editorial changes, before the planned November 1 vote.  
>>> 
>>> Brief summary:
>>> 
>>> * The commenter's main concern seems to be that we could have a much shorter and simpler spec if we gave a declarative specification in terms of first-order logical formulas, instead of giving a procedural definition of validity and equivalence in terms of normal forms.  Doing this may also have the nice benefit of allowing us to reuse standard terminology from logic instead of using standard-sounding terms in nonstandard ways.  This is true in some sense, and I'd certainly be happy with such a document, but (based on experience with the group so far, and extrapolating to the larger audience) I think doing this would make the document much less accessible to people without expertise on the formal/logic side.  
>>> 
>>> * It would be helpful to get a reading from the group as to whether the commenter's concerns are serious enough to merit a major change, from our procedural style to a declarative style.  If we did that, I think we would still need to have the procedural explanation as a non-normative explanation of how to implement the declarative spec.  So my view is that we should address this by explicitly acknowledging the issue, giving the declarative spec as an appendix (which builds on the connection to logic in section 2),
>> 
>> Just to emphasize (although it is said in your previous sentence): a non-normative appendix.
> 
> Correct - to avoid specifying the same thing twice (though they should be provably equivalent).
> 
> --James
> 
>> Ivan
>> 
>> 
>>> and stating/proving that the declarative and procedural specs give the same behavior.  Thus, while it's safe for an implementor to ignore all of the non-normative, logic stuff, it is also OK to implement the declarative spec in any other way without explicitly normalizing etc.
>>> 
>>> * I think the only non-editorial change will be to relax the definition of PROV-equivalence so that we specify that it is reflexive/symmetric/transitive on all instances/documents, but that no valid instance is equivalent to an invalid instance and its behavior on invalid documents is not further specified.  This is to avoid conflict with the usual notion of logical equivalence while not over-specifying that all invalid instances are equivalent.  I don't believe we are planning to test equivalence checking anyway, so perhaps this is moot.
>>> 
>>> * Aside from that, I plan to keep things more or less as is, and explain the rationale for our procedural presentation, but give additional detail about the declarative (first-order logic theory) specification that PROV-CONSTRAINTS implements.  
>>> 
>>> Perhaps we should add a brief straw poll as an agenda item to get an idea of whether there is consensus support for this approach.
>>> 
>>> For the moment, a draft response to individual points is in the repository at:
>>> 
>>> http://dvcs.w3.org/hg/prov/raw-file/default/model/comments/issue-576-antoine-zimmermann.txt
>>> 
>>> --James
>>> 
>>> 
>>> On Oct 23, 2012, at 2:14 PM, Provenance Working Group Issue Tracker wrote:
>>> 
>>>> PROV-ISSUE-576: logical definition and comments on prov-constratins [prov-dm-constraints]
>>>> 
>>>> http://www.w3.org/2011/prov/track/issues/576
>>>> 
>>>> Raised by: Paul Groth
>>>> On product: prov-dm-constraints
>>>> 
>>>> Please see the following public comment:
>>>> http://lists.w3.org/Archives/Public/public-prov-comments/2012Oct/0004.html
>>> 
>>> 
>>> -- 
>>> The University of Edinburgh is a charitable body, registered in
>>> Scotland, with registration number SC005336.
>> 
>> 
>> ----
>> Ivan Herman, W3C Semantic Web Activity Lead
>> Home: http://www.w3.org/People/Ivan/
>> mobile: +31-641044153
>> FOAF: http://www.ivan-herman.net/foaf.rdf
> 
> 
> -- 
> The University of Edinburgh is a charitable body, registered in
> Scotland, with registration number SC005336.
> 
> 

Received on Tuesday, 23 October 2012 18:19:15 UTC