--- a/model/prov-constraints.html Wed Aug 29 08:19:06 2012 -0400
+++ b/model/prov-constraints.html Wed Aug 29 18:30:30 2012 +0100
@@ -791,7 +791,7 @@
named event such as usage, generation, or a relationship such as
attribution.)
This specification includes <a href="#type-constraints">disjointness and typing constraints</a> that
-check these requirements. Here, we merely
+check these requirements. Here, we
summarize the type constraints in <a href="#typing-table">Table 1</a>.
</p>
@@ -874,8 +874,8 @@
</tr>
<tr align="center">
<td rowspan="2" class="name">wasInvalidatedBy(id; e,a,t,attrs)</td>
- <td class="name">a</td>
- <td class="name">'activity'</td>
+ <td class="name">e</td>
+ <td class="name">'entity'</td>
</tr>
<tr align="center">
<td class="name">a</td>
@@ -981,14 +981,6 @@
<section>
<h4>Validation Process Overview</h4>
-<div style="text-align: center;">
-<figure>
-<img src="images/constraints/prov-c.graffle.svg/overview.svg" alt="validation process overview" />
-<br>
-<figcaption id="validation-process-overview">Overview of the Validation Process</figcaption>
-</figure> <!-- <b>new Figure 1:</b> -->
-</div>
-
<div class="note">
In progress, outline to be filled in
</div>
@@ -1020,11 +1012,11 @@
<p>Several definitions and inferences conclude by saying that some
objects exist such that some other formulas hold. Such an inference
- introduces fresh <em>existential variables</em> into the instance.
- Such a variable denotes a fixed object that exists, but its exact
- identity is unknown, so we often refer to such variables as
- <em>existential variables</em>. We do not allow existential
- variables that stand for unknown attribute lists. </p>
+ introduces fresh <a>existential variable</a>s into the instance. An
+ existential variable denotes a fixed object that exists, but its
+ exact identity is unknown. Existential variables can stand for
+ unknown identifiers or literal values only; we do not allow
+ existential variables that stand for unknown attribute lists. </p>
<p>In particular, many
occurrences of the placeholder symbol <span class="name">-</span> stand for unknown
@@ -1035,24 +1027,33 @@
places.
</p>
<p>An expression is called a <em>term</em> if it is either a
- constant identifier, literal, placeholder, or variable, and write
+ constant identifier, literal, placeholder, or variable. We write
<span class="math">t</span> to denote an arbitrary term.
</p>
<h4>Substitution</h4>
-<p>A substitution is a function that maps variables to terms. Concretely, since we only
+<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_1 = t_1,...,x_n=t_n]</span>. A substitution
- <span class="math">S = [x_1 = t_1,...,x_n=t_n]</span>
+ 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
+ <span class="math">S = [x<sub>1</sub> = t<sub>1</sub>,...,x<sub>n</sub>=t<sub>n</sub>]</span>
can be <em>applied</em> to a term as follows.
+</p>
<ol><li>
- If the term is a variable <span class="math">x_i</span>, one of the variables in the
- domain of <span class="math">S</span>, then <span class="math">S(x) = t_i</span>.
+ If the term is a variable <span class="math">x<sub>i</sub></span>, one of the variables in the
+ domain of <span class="math">S</span>, then <span class="math">S(x<sub>i</sub>) = t<sub>i</sub></span>.
</li>
- <li>
+ <li>If the term is a constant identifier or literal <span
+ class="math">c</span>, then <span class="math">S(c) = c</span>.
</li>
</ol>
+<p>
+ In addition, a substitution can be applied to an atomic formula
+ (PROV statement) <span class="math">p(t<sub>1</sub>,...,t<sub>n</sub>)</span> by applying it to each term,
+ that is, <span class="math">S(p(t<sub>1</sub>,...,t<sub>n</sub>)) = p(S(t<sub>1</sub>),...,t<sub>n</sub>)</span>. Likewise, a
+ substitution <span class="math">S</span> can be applied to an instance <span class="math">I</span> by applying
+ it to each atomic formula (PROV statement) in <span class="math">I</span>, that is, <span class="math">S(I)
+ = {S(A) | A ∈ I}</span>.
</p>
@@ -1071,30 +1072,36 @@
<p>The atomic constraints considered in this specification can be
viewed as atomic formulas:</p>
<ul>
- <li>Uniqueness constraints...</li>
- <li>Ordering constraints...
+ <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>
</li>
- <li>Typing constraints...
+ <li>Typing constraints employ the set-valued <span class="name">typeOf</span> function, but
+ the property <span class="name">type ∈ typeOf(id)</span> can be represented as a binary
+ relation <span class="name">typeOf(id,type)</span>.
</li>
- <li>Impossibility constraints</li>
+ <li>Impossibility constraints employ the conclusion <span class="name">INVALID</span>,
+ which is equivalent to the logical constant <span class="math">False</span>. </li>
</ul>
<p> Similarly, the definitions, inferences, and constraint rules in this
specification can also be viewed as logical formulas.</p>
<ul>
<li>
- A definition of the form "A IF AND ONLY IF there
- exists y1...ym such that B1 and ... and Bk"
- can be thought of as a formula "\forall x1,....,xn. A <==> \exists y1...ym such that B1 and ... and Bn", where x1...xn are the
+ 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 formula.
</li>
-<li>An inference of the form "IF A THEN there
- exists y1...ym such that B1 and ... and Bk" can be thought of as a formula "\forall x1,....,xn. A ==> \exists y1...ym such that B1 and ... and Bn", where x1...xn are the
+<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>l</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>l</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 formula.
</li>
-<li>A uniqueness, ordering, or typing constraint of the form "IF A THEN C" can be viewed as a formula
- "forall x1...xn. A ==> C". </li>
-<li>A constraint of the form "IF A THEN INVALID" can be viewed as a formula
- "forall x1...xn. A ==> false". </li>
+<li>A uniqueness, ordering, or typing constraint of the form "<span class="conditional">IF</span> <span class="name">A</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 ⇒ C</span>". </li>
+<li>A constraint of the form "<span class="conditional">IF</span> <span class="name">A</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 ⇒ False</span>". </li>
</ul>
@@ -1188,6 +1195,16 @@
indirectly referenced in other relations.
</p>
+
+<div style="text-align: center;">
+<figure>
+<img src="images/constraints/prov-c.graffle.svg/overview.svg" alt="validation process overview" />
+<br>
+<figcaption id="validation-process-overview">Overview of the Validation Process</figcaption>
+</figure> <!-- <b>new Figure 1:</b> -->
+</div>
+
+
<h4>Checking ordering, typing, and impossibility constraints</h4>
<p>
The ordering, typing, and impossibility constraints are checked
@@ -1231,7 +1248,7 @@
logic, if we consider normalized PROV instances with existential
variables to represent sets of possible situations, then two normal
forms may describe the same situation but differ in inessential
- details such as the order of statements or of elemennts of
+ details such as the order of statements or of elements of
attribute-value lists. To remedy this, we can easily consider
instances to be equvalent up to reordering of attributes. However,
instances can also be equvalent if they differ only in choice of