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

Hi again,

Following some additional offline discussion, I've put together a draft response.  

http://www.w3.org/2011/prov/wiki/ResponsesToPublicComments#PROV-CONSTRAINTS

The main difference from the approach I originally suggested is that I now suggest that we will put the declarative specification into PROV-SEM, rather than adding it as a non-normative appendix.  The reason for this is that as it's non-normative anyway, better to place it off the critical path and have this material all in one place, where we can relate the model theory (in PROV-SEM already), first-order axioms, and checking procedures.

If people are generally happy with the overall approach, I plan to:
1.  break this issue into the ~12 sub-issues raised by the reviewer
2.  split the response up issue-by-issue, and address over the next week or so

I believe this is on the agenda to discuss today.

--James

On Oct 23, 2012, at 6:56 PM, 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), 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.
> 
> 
> 


-- 
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.

Received on Thursday, 25 October 2012 11:09:09 UTC