author | jcheney@inf.ed.ac.uk |

Fri, 12 Apr 2013 12:05:00 +0100 | |

changeset 6134 | 2171dd7a9fb5 |

parent 6133 | 92af37385002 |

child 6138 | 3024f3a1577e |

* typos

model/prov-constraints.html | ||

semantics/prov-sem.html |

--- a/model/prov-constraints.html Thu Apr 11 13:27:31 2013 -0400 +++ b/model/prov-constraints.html Fri Apr 12 12:05:00 2013 +0100 @@ -1382,7 +1382,7 @@ </section> <section id="overview" class="informative"> -<h4>Validation Process Overview</h4> +<h2>Validation Process Overview</h2> <p> @@ -1407,13 +1407,13 @@ implementers, while the procedural approach adopted here immediately demonstrates implementability and provides an adequate (polynomial-time) default implementation. In this section we relate the declarative meaning of formulas to their -procedural meaning. [[PROV-SEM]] will provide an alternative, -declarative characterization of validity and equivalence which could +procedural meaning. [[PROV-SEM]] provides an alternative, +declarative characterization of validity which could be used as a starting point for other implementation strategies. </p> - <h4>Constants, Variables and Placeholders</h4> + <h3>Constants, Variables and Placeholders</h3> <p> PROV statements involve identifiers, literals, placeholders, and attribute lists. Identifiers are, according to PROV-N, expressed as <a href="http://www.w3.org/TR/2013/REC-prov-n-20130430/#prod-QUALIFIED_NAME">qualified names</a> which can be mapped to URIs [[!RFC3987]]. @@ -1450,7 +1450,7 @@ </p> - <h4>Substitution</h4> + <h3>Substitution</h3> <p>A <em>substitution</em> is a function that maps variables to terms. Concretely, since we only need to consider substitutions of finite sets of variables, we can write substitutions as <span class="math">[x<sub>1</sub> = t<sub>1</sub>,...,x<sub>n</sub>=t<sub>n</sub>]</span>. A substitution @@ -1482,7 +1482,7 @@ - <h4>Formulas</h4> + <h3>Formulas</h3> <p> For the purpose of constraint checking, we view PROV statements (possibly involving existential variables) as @@ -1497,7 +1497,7 @@ <li>Uniqueness constraints employ atomic equational formulas <span class="math">t = t'</span>.</li> <li>Ordering constraints employ atomic precedence relations that can - be thought of as binary formulas <span class="math">precedes(t,t')</span> or <span class="math">strictly_precedes(t,t')</span> + be thought of as binary formulas <span class="math">precedes(t,t')</span> or <span class="math">strictlyPrecedes(t,t')</span> </li> <li>Typing constraints <span class="name">'type' ∈ typeOf(id)</span> can be represented as a atomic formulas <span class="name">typeOf(id,'type')</span>. @@ -1512,24 +1512,24 @@ background on logical formulas, see a logic textbook such as [[Logic]].</p> <ul> <li> - A definition of the form <span class="name">A</span> <span class="conditional">IF AND ONLY IF</span> there - exists <span class="name">y<sub>1</sub></span>...<span class="name">y<sub>m</sub></span> such that <span class="name">B<sub>1</sub></span> and ... and <span class="name">B<sub>k</sub></span> + A definition of the form "<span class="name">A</span> <span class="conditional">IF AND ONLY IF</span> there + exists <span class="name">y<sub>1</sub></span>...<span class="name">y<sub>m</sub></span> such that <span class="name">B<sub>1</sub></span> and ... and <span class="name">B<sub>k</sub></span>" can be thought of as a formula <span class="math">∀ x<sub>1</sub>,....,x<sub>n</sub>. A ⇔ ∃ y<sub>1</sub>...y<sub>m</sub> . B<sub>1</sub> ∧ ... ∧ B<sub>k</sub></span>, where <span class="math">x<sub>1</sub></span>...<span class="math">x<sub>n</sub></span> are the free variables of the definition. </li> -<li>An inference of the form <span class="conditional">IF</span> <span class="name">A<sub>1</sub></span> and ... and <span class="name">A<sub>p</sub></span> <span class="conditional">THEN</span> there - exists <span class="name">y<sub>1</sub></span>...<span class="name">y<sub>m</sub></span> such that <span class="name">B<sub>1</sub></span> and ... and <span class="name">B<sub>k</sub></span> can +<li>An inference of the form "<span class="conditional">IF</span> <span class="name">A<sub>1</sub></span> and ... and <span class="name">A<sub>p</sub></span> <span class="conditional">THEN</span> there + exists <span class="name">y<sub>1</sub></span>...<span class="name">y<sub>m</sub></span> such that <span class="name">B<sub>1</sub></span> and ... and <span class="name">B<sub>k</sub></span>" can be thought of as a formula <span class="math">∀ x<sub>1</sub>,....,x<sub>n</sub>. A<sub>1</sub> ∧ ... ∧ A<sub>p</sub> ⇒ ∃ y<sub>1</sub>...y<sub>m</sub> . B<sub>1</sub> ∧ ... ∧ B<sub>k</sub></span>, where <span class="math">x<sub>1</sub></span>...<span class="math">x<sub>n</sub></span> are the free variables of the inference. </li> -<li>A uniqueness, ordering, or typing constraint of the form <span class="conditional">IF</span> <span class="name">A<sub>1</sub> ∧ ... ∧ A<sub>p</sub></span> <span class="conditional">THEN</span> <span class="name">C</span> can be viewed as a formula +<li>A uniqueness, ordering, or typing constraint of the form "<span class="conditional">IF</span> <span class="name">A<sub>1</sub> ∧ ... ∧ A<sub>p</sub></span> <span class="conditional">THEN</span> <span class="name">C</span>" can be viewed as a formula <span class="math">∀ x<sub>1</sub>...x<sub>n</sub>. A<sub>1</sub> ∧ ... ∧ A<sub>p</sub> ⇒ C</span>. </li> -<li>A constraint of the form <span class="conditional">IF</span> <span class="name">A<sub>1</sub> ∧ ... ∧ A<sub>p</sub></span> <span class="conditional">THEN INVALID</span> can be viewed as a formula +<li>A constraint of the form "<span class="conditional">IF</span> <span class="name">A<sub>1</sub> ∧ ... ∧ A<sub>p</sub></span> <span class="conditional">THEN INVALID</span>" can be viewed as a formula <span class="math">∀ x<sub>1</sub>...x<sub>n</sub>. A<sub>1</sub> ∧ ... ∧ A<sub>p</sub> ⇒ False</span>. </li> </ul> - <h4>Satisfying definitions, inferences, and constraints</h4> + <h3>Satisfying definitions, inferences, and constraints</h3> <p> In logic, a formula's meaning is defined by saying when it is <em>satisfied</em>. We can view @@ -1548,7 +1548,7 @@ B<sub>k</sub></span> are either both true or both false. </li> <li>A logical implication as used in an inference is - satisfied with the formula <span class="math">∀ + satisfied when the formula <span class="math">∀ x<sub>1</sub>,....,x<sub>n</sub>. A<sub>1</sub> ∧ ... ∧ A<sub>p</sub> ⇒ ∃ y<sub>1</sub>...y<sub>m</sub> . B<sub>1</sub> ∧ ... ∧ B<sub>k</sub></span> holds, that is, for any substitution of @@ -1569,7 +1569,7 @@ substitution for <span class="math">x<sub>1</sub>...x<sub>n</sub></span> making <span class="math">A<sub>1</sub> ∧ ... ∧ A<sub>p</sub></span> true. </ol> -<h4>Unification and Merging</h4> +<h3>Unification and Merging</h3> <p><em>Unification</em> is an operation that takes two terms and compares them to determine whether they can be made equal by substituting an @@ -1592,7 +1592,7 @@ - <h4>Applying definitions, inferences, and constraints</h4> + <h3>Applying definitions, inferences, and constraints</h3> <p>Formulas can also be interpreted as having computational content. That is, if an instance does not satisfy a formula, we can often <em>apply</em> the formula to the instance to produce another @@ -1621,7 +1621,7 @@ A<sub>p</sub> ⇒ ∃ y<sub>1</sub>...y<sub>m</sub> . B<sub>1</sub> ∧ ... ∧ B<sub>k</sub></span> can be applied by searching for any occurrences of <span class="math"> A<sub>1</sub> ∧ ... ∧ - A<sub>p</sub></span> in the instance and, for each such match, + A<sub>p</sub></span> in the instance and, for each such match for which the entire conclusion does not already hold (for some <span class="math">y<sub>1</sub>,...,y<sub>m</sub></span>), adding <span class="math">B<sub>1</sub> ∧ ... ∧ B<sub>k</sub></span> to the instance, generating fresh existential @@ -1668,7 +1668,7 @@ </p> - <h4>Termination</h4> + <h3>Termination</h3> <p> In general, applying sets of logical formulas of the above definition, inference, and constraint forms is not guaranteed to @@ -1735,7 +1735,7 @@ </div> - <h4>Checking ordering, typing, and impossibility constraints</h4> + <h3>Checking ordering, typing, and impossibility constraints</h3> <p> The ordering, typing, and impossibility constraints are checked rather than applied. This means that they do not generate new @@ -1801,7 +1801,7 @@ - <h4>Equivalence and Isomorphism</h4> + <h3>Equivalence and Isomorphism</h3> <p> Given two normal forms, a natural question is whether they contain the same information, that is, whether they are equivalent (if so, then the original instances are also equivalent.) By analogy with @@ -1858,7 +1858,7 @@ <li>every pair of invalid instances are equivalent</li> </ol> -<h4>From Instances to Bundles and Documents</h4> +<h3>From Instances to Bundles and Documents</h3> <p>PROV documents can contain multiple instances: a <a>toplevel instance</a>, and @@ -1888,7 +1888,7 @@ </section> <section class="informative"> -<h4>Summary of inferences and constraints</h4> +<h2>Summary of inferences and constraints</h2> <p><a href="">Table 2</a> summarizes the inferences, and constraints specified in this document, broken down by component and @@ -2542,7 +2542,7 @@ <div class="remark"> - <p>Definitions <a class="rule-ref" href="#optional-identifiers"><span>TBD</span></a> and <a class="rule-ref" href="#optional-attributes"><span>TBD</span></a>. + <p>Definitions <a class="rule-ref" href="#optional-identifiers"><span>TBD</span></a> and <a class="rule-ref" href="#optional-attributes"><span>TBD</span></a> do not apply to <span class="name">alternateOf</span> and <span class="name">specializationOf</span>, which do not have identifiers and attributes. </p> </div> @@ -2722,7 +2722,7 @@ Essentially, the definitions state that parameters <span class="name">g,u</span> are expandable only if the activity is specified, i.e., if parameter <span class="name">a</span> is provided. -The rationale for this is that when a is provided, then there have to be two events, namely <span class="name">u</span> and <span class="name">g</span>, which account for the usage of <span class="name">e1</span> and the generation of <span class="name">e2</span>, respectively, by <span class="name">a</span>. Conversely, if <span class="name">a</span> is not provided, then one cannot tell whether one or more activities are involved in the derivation, and the explicit introduction of such events, which correspond to a single activity, would therefore not be justified. </p> +The rationale for this is that when <span class="name">a</span> is provided, then there have to be two events, namely <span class="name">u</span> and <span class="name">g</span>, which account for the usage of <span class="name">e1</span> and the generation of <span class="name">e2</span>, respectively, by <span class="name">a</span>. Conversely, if <span class="name">a</span> is not provided, then one cannot tell whether one or more activities are involved in the derivation, and the explicit introduction of such events, which correspond to a single activity, would therefore not be justified. </p> <p> A later constraint, <a class="rule-ref" @@ -4562,7 +4562,7 @@ That is, <span class="name">typeOf(e)</span> returns the set of types associated with identifier <span class="name">e</span>. The function <span class="name">typeOf</span> is not a PROV statement, but a -construct used only during validation PROV, similar to <a>precedes</a>. +construct used only during validation, similar to <a>precedes</a>. </p> @@ -4982,11 +4982,8 @@ <a title="equivalence">equivalence</a> of PROV documents and instances. We first define these concepts for PROV instances and then extend them to PROV documents.</p> -<section id="instances"> - <h2>Instances</h2> - <div class="remark"> - Before normalization or validation, implementations should expand + Implementations should expand namespace prefixes and perform any appropriate reasoning about co-reference of identifiers, and rewrite the instance (by replacing co-referent identifiers with a single common identifier) to @@ -4998,6 +4995,10 @@ reasoning). </div> + <section id="instances"> + <h2>Instances</h2> + + <p> We define the <dfn>normal form</dfn> of a PROV instance as the set of provenance statements resulting from applying all definitions, inferences, and uniqueness constraints, obtained as follows:</p> @@ -5259,8 +5260,7 @@ attributes would also arise from one with no attributes. </p> - <p><b>Termination for instances without attributes.</b> For - these instances, uniqueness and key constraints can be + <p><b>Termination for instances without attributes.</b> As shown in [[DBCONSTRAINTS]], termination of normalization can be shown by checking that the inference rules are <em>weakly acyclic</em>. In addition, weak acyclicity can be checked @@ -5389,13 +5389,20 @@ <ul> <li> Changed the status of this document section. <li> Changed all URLs to PROV documents. + <li> Fixed some minor typos in section 2.4. + <li> Fixed typo in remark after definition 2. + <li> Fixed typo in paragraph after table 2. + <li> Fixed typo in sec. 6.3. + <li> Fixed wording in remark in sec. 7.1, and moved it before + section heading. + <li> Fixed typo in appendix A. </ul> </section> <section class="appendix"> - <h2>Changes from Candidate Recommendation to this version</h2> + <h2>Changes from Candidate Recommendation to Proposed Recommendation</h2> <p> Please see the <a href="http://www.w3.org/2011/prov/wiki/ResponsesToPublicCommentsCR"> Responses to Public Comments on the Candidate Recommendation</a>

--- a/semantics/prov-sem.html Thu Apr 11 13:27:31 2013 -0400 +++ b/semantics/prov-sem.html Fri Apr 12 12:05:00 2013 +0100 @@ -1026,7 +1026,7 @@ <li> <a href="http://www.w3.org/TR/2013/NOTE-prov-xml-20130430/">PROV-XML</a> (Note), an XML schema for the PROV data model [[PROV-XML]];</li> <li> <a href="http://www.w3.org/TR/2013/NOTE-prov-aq-20130430/">PROV-AQ</a> (Note), the mechanisms for accessing and querying provenance [[PROV-AQ]]; </li> <li> <a href="http://www.w3.org/TR/2013/NOTE-prov-dictionary-20130430/">PROV-DICTIONARY</a> (Note) introduces a specific type of collection, consisting of key-entity pairs [[PROV-DICTIONARY]];</li> -<li> <a href="http://www.w3.org/TR/2013/NOTE-prov-dc-20130430/">PROV-DC</a> (Note) provides a mapping between PROV and Dublic Core Terms [[PROV-DC]];</li> +<li> <a href="http://www.w3.org/TR/2013/NOTE-prov-dc-20130430/">PROV-DC</a> (Note) provides a mapping between PROV and Dublin Core Terms [[PROV-DC]];</li> <li> <a href="http://www.w3.org/TR/2013/NOTE-prov-sem-20130430/">PROV-SEM</a> (Note), a declarative specification in terms of @@ -4404,9 +4404,14 @@ contents reflect extensive discussion within the Working Group as a whole. Thanks specifically to Khalid Belhajjame, Tom De Nies, Paolo - Missier, Simon Miles, Luc Moreau, Satya Sahoo, Joachim Van - Herwegen for detailed feedback. + Missier, Simon Miles, Luc Moreau, Satya Sahoo, Jan van den + Bussche, and Joachim Van + Herwegen for detailed feedback. Significant progress was made on this document at + <a href="http://www.dagstuhl.de/12091">Dagstuhl Seminar 12901 (Principles of Provenance)</a>, and so we + would also like to acknowledge participants in that event and + the staff of <a href="http://www.dagstuhl.de">Schloss Dagstuhl - Leibniz Center for Informatics</a>. </p> + <p>Thanks also to Robin Berjon for the ReSPec.js specification writing tool and to MathJax for their LaTeX-to-HTML conversion tools, both of which aided in the preparation of this document.</p>