author | James Cheney <jcheney@inf.ed.ac.uk> |

Wed, 29 Aug 2012 18:30:30 +0100 | |

changeset 4373 | 5279a2172dc6 |

parent 4372 | fbe20385e1f3 |

child 4374 | 9d2967fd1345 |

* work on overview section

model/prov-constraints.html |

--- 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