Review of PROV-CONSTRAINTS issues (ISSUE-582, ISSUE-579, ISSUE-585, ISSUE-583)

I have made additional changes addressing ISSUE-582, ISSUE-579, ISSUE-585, ISSUE-583.  These are the most minor ones requiring few changes.  As in the previous batch, there are no changes affecting the behavior of implementations in this batch, though some of the text is in normative sections.

The summaries and responses are below; the current versions of responses (draft and pending review) are here.  These issues have been marked "pending review".  Please respond (to this message or to the appropriate issue thread) with any objections or suggested improvements by next Wednesday (Oct. 31)  if you disagree with the proposed response.

--James


ISSUE-584 (merging)

	• Original email: http://lists.w3.org/Archives/Public/public-prov-comments/2012Oct/0004.html
	• Tracker: http://www.w3.org/2011/prov/track/issues/584
	• Summary: The nonstandard/procedurally defined term 'merging'
	• Group response:
		• For terms, "merging" is exactly unification in the usual first-order logic / logic programming sense, as we state in a remark. For predicates that carry attribute lists, things are more complicated since key constraints require the attribute lists be combined, not unified in the usual sense.
	• References:
	• Changes to the document:
		• Use "unification" for "merging" at the level of terms
		• Declaratively describe unification as producing "either failure or a substitution that makes both sides equal", as well as giving the (standard) algorithm
		• Retain "merging" for the nonstandard operation on predicates that unifies the term arguments and concatenates the lists of attributes.
	• Original author's acknowledgement:

[edit] ISSUE-579 (declarative-fol-specification)

	• Original email: http://lists.w3.org/Archives/Public/public-prov-comments/2012Oct/0004.html
	• Tracker: http://www.w3.org/2011/prov/track/issues/579
	• Summary: Suggestion to replace procedural specification with (equivalent, but shorter and less prescriptive) declarative theory in First-Order Logic
	• Group response:
		• PROV-CONSTRAINTS intentionally reuses as much of standard techniques from logic and particularly database theory as possible. However, our audience (as reflected by the composition of the WG) is not expected to be familiar already with first-order logic, so we felt it was important to elaborate upon these concepts sufficiently that someone without background in these areas can implement it.
		• Moreover, writing an arbitrary FOL axiomatization has its own problems: since there is currently no standard way to do this we would have to restate a lot of the standard definitions in order to make the specification self-contained (as we have already done). In addition, an arbitrary FOL theory is not guaranteed to be decidable, even over finite models. We resolved that the constraints document had to demonstrate decidability/computability, as a basic prerequisite for implementability. Simply giving a set of FOL axioms on its own would not be enough to do this, and would leave (the vast majority of) implementors not familiar with FOL theorem proving/databases/constraint solving at sea with respect to implementation.
		• Thus, this issue is deferred to the planned PROV-SEM note.
	• References:
	• Changes to the document:
		• PROV-CONSTRAINTS updated to clarify that a declarative alternative is deferred to PROV-SEM
		• Add non-normative material PROV-SEM giving a FOL axiomatization, proof of soundness/completeness with respect to the algorithm in the spec and soundness with respect to the draft model-theory in the current draft of PROV-SEM.
	• Original author's acknowledgement:


[edit] ISSUE-585 (applying-satisfying-constraints)

	• Original email: http://lists.w3.org/Archives/Public/public-prov-comments/2012Oct/0004.html
	• Tracker: http://www.w3.org/2011/prov/track/issues/585
	• Summary: Suggestion to avoid discussing how to 'apply' definitions, inferences and constraints; the term 'satisfies' is not adequately defined in the context of PROV-CONSTRAINTS
	• Group response:
		• As noted in the response to ISSUE-585, we disagree that rewriting everything in terms of pure first-order logic would lead to a satisfactory specification (as opposed to a satisfactory research paper, say). The goal of the non-normative section here is essentially to link the (implicit) declarative semantics of the first-order theory, which we described informally earlier, with the procedural way in which normalization handles this behavior. This is exactly analogous with an operational, or proof-theoretic approach the semantics of logic programming, which is equally valid compared with a declarative, denotational semantics; we simply chose to present the approach that lends itself more immediately to efficient implementation.
		• We inadvertently used "satisfies" as as shorthand for "passes all constraint checks without generating INVALID". This will be clarified.
	• References:
	• Changes to the document:
		• Clarify that "applying" is one of many ways of "checking" constraints
		• Clarify meaning of "satisfies" in definition of validity
	• Original author's acknowledgement:


[edit] ISSUE-583 (equivalent-instances-in-bundles)

	• Original email: http://lists.w3.org/Archives/Public/public-prov-comments/2012Oct/0004.html
	• Tracker: http://www.w3.org/2011/prov/track/issues/583
	• Summary: Questions concerning what it means for applications to treat equivalent instances 'in the same way', particularly in bundles.
	• Group response:
		• Since validity and equivalence are optional, this is not a formal requirement, but a guideline; what it means for an application to treat equivalent instances/documents "in the same way" is application specific, and there are natural settings where it makes sense for an application (evenone that cares about validity) to have different behavior for equivalent documents. We give one example of formatting/pretty printing. You give some additional examples; digital signing is a third. Because we have no way of circumscribing what applications might do or what it means for an application to treat documents "in the same way", we just leave this as a guideline.
	• References:
	• Changes to the document:
		• Clarify that the suggestion that applications SHOULD treat equivalent instances 'in the same way' is a guideline, and depends on what 'in the same way' means for a given application.
	• Original author's acknowledgement:
-- 
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.

Received on Friday, 26 October 2012 17:33:00 UTC