--- a/model/prov-constraints.html Fri Apr 12 12:07:26 2013 +0100
+++ b/model/prov-constraints.html Fri Apr 12 12:09:53 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>