W3C home > Mailing lists > Public > public-prov-wg@w3.org > October 2012

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

From: James Cheney <jcheney@inf.ed.ac.uk>
Date: Tue, 23 Oct 2012 18:56:50 +0100
Message-Id: <76D71786-9C2B-4696-BC6C-CE046A82FF24@inf.ed.ac.uk>
To: Provenance Working Group <public-prov-wg@w3.org>

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:



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.
Received on Tuesday, 23 October 2012 17:57:16 UTC

This archive was generated by hypermail 2.3.1 : Tuesday, 6 January 2015 21:58:20 UTC