author | Luc Moreau <l.moreau@ecs.soton.ac.uk> |

Mon, 03 Sep 2012 21:41:07 +0100 | |

changeset 4397 | 866dc32ffa40 |

parent 4396 | beb137e18688 |

child 4398 | 5feff7139186 |

minor changes to constraints

model/prov-constraints.html |

--- a/model/prov-constraints.html Mon Sep 03 18:29:49 2012 +0100 +++ b/model/prov-constraints.html Mon Sep 03 21:41:07 2012 +0100 @@ -1000,15 +1000,17 @@ <h4>Constants, Variables and Placeholders</h4> <p> - PROV statements involve identifiers (URIs), literals, - placeholders, and attribute lists. However, in order to specify + PROV statements involve identifiers, literals, + placeholders, and attribute lists. Identifiers are, according to PROV-N, expressed as <a href="http://www.w3.org/TR/prov-n/#prod-QUALIFIED_NAME">qualified names</a> which can be mapped to URIs [[!IRI]]. + However, in order to specify constraints over PROV instances, we also need <em>variables</em> that represent unknown identifiers, literals, or placeholders. These variables are similar to those in first-order logic [[Logic]]. A variable is a symbol that can be replaced by other symbols, including either other variables or constant identifiers, literals, or placeholders. In a few special cases, we - also use variables for unknown attribute lists. + also use variables for unknown attribute lists. + To help distinguish identifiers and variables, we also term the former 'constant identifiers' to highlight their non-variable nature. </p> <p>Several definitions and inferences conclude by saying that some @@ -1189,18 +1191,19 @@ </li> <li>An inference of the form <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> ∧ + 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>l</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 variables <span class="math">y<sub>1</sub>,...,y<sub>m</sub></span>. </li> <li>A uniqueness constraint of the form <span class="math">∀ -x<sub>1</sub>...x<sub>n</sub>. A<sub>1</sub> ∧ ... ∧ A<sub>l</sub> ⇒ t +x<sub>1</sub>...x<sub>n</sub>. A<sub>1</sub> ∧ ... ∧ A<sub>p</sub> ⇒ t = t'</span> can be - applied by searching for an occurrence of <span class="math">A</span> in the instance, and + applied by searching for an occurrence <span class="math">A<sub>1</sub> ∧ ... ∧ A<sub>p</sub></span> in the instance, and if one is found, merging the terms <span class="math">t</span> and <span class="math">t'</span>. If successful, the resulting substitution is applied to the instance; otherwise, the application @@ -1314,9 +1317,9 @@ of as a directed graph whose nodes are terms, and whose edges are precedes or strictly-precedes relationships. An ordering constraint of the form <span class="math">∀ -x<sub>1</sub>...x<sub>n</sub>. A<sub>1</sub> ∧ ... ∧ A<sub>l</sub> ⇒ +x<sub>1</sub>...x<sub>n</sub>. A<sub>1</sub> ∧ ... ∧ A<sub>p</sub> ⇒ precedes(t,t')</span> can be applied by searching for occurrences of -<span class="math"> A<sub>1</sub> ∧ ... ∧ A<sub>l</sub></span> and for each such match +<span class="math"> A<sub>1</sub> ∧ ... ∧ A<sub>p</sub></span> and for each such match adding the atomic formula <span class="math">precedes(t,t')</span> to the instance, and similarly for strictly-precedes constraints. After all such constraints have been checked, and the resulting edges added to the graph, the ordering constraints are @@ -1329,7 +1332,7 @@ start with a function mapping each identifier to the empty set, reflecting no constraints on the identifiers' types. A typing constraint of the form <span class="math">∀ -x<sub>1</sub>...x<sub>n</sub>. A<sub>1</sub> ∧ ... ∧ A<sub>l</sub> ⇒ 'type' ∈ typeOf(id) +x<sub>1</sub>...x<sub>n</sub>. A<sub>1</sub> ∧ ... ∧ A<sub>p</sub> ⇒ 'type' ∈ typeOf(id) </span> is checked by adjusting the function by adding <span class="name">'type'</span> to <span class="math">typeOf(id)</span> for each conclusion <span class="name">'type' ∈ typeOf(id)</span> of the rule. Typing constraints with @@ -1343,9 +1346,9 @@ forbidden pattern that the impossibility constraint describes. Any match of this pattern leads to failure of the constraint checking process. An impossibility constraint of the form <span class="math">∀ -x<sub>1</sub>...x<sub>n</sub>. A<sub>1</sub> ∧ ... ∧ A<sub>l</sub> ⇒ +x<sub>1</sub>...x<sub>n</sub>. A<sub>1</sub> ∧ ... ∧ A<sub>p</sub> ⇒ False</span> can be applied by searching for occurrences of -<span class="math"> A<sub>1</sub> ∧ ... ∧ A<sub>l</sub></span> in the instance, and if any +<span class="math">A<sub>1</sub> ∧ ... ∧ A<sub>p</sub></span> in the instance, and if any such occurrence is found, signaling failure.</p> </li> </ol> @@ -1737,8 +1740,7 @@ priority. </p> - <div class="note"> To reviewers: We specifically invite review for - consistency between the informal and formal text.</div> + </section> @@ -2107,10 +2109,10 @@ <div class="definition" id="optional-placeholders"> <ol><li> <span class="name">activity(id,-,t2,attrs)</span> <span class="conditional">IF AND ONLY - IF</span> there exists <span class="name">t1</span> such that <span class="name">activity(id,t1,t2,attrs)</span>. + IF</span> there exists <span class="name">t1</span> such that <span class="name">activity(id,t1,t2,attrs)</span>. Here, <span class="name">t2</span> MAY be a placeholder. </li> <li> <span class="name">activity(id,t1,-,attrs)</span> <span class="conditional">IF AND ONLY - IF</span> there exists <span class="name">t2</span> such that <span class="name">activity(id,t1,t2,attrs)</span>. + IF</span> there exists <span class="name">t2</span> such that <span class="name">activity(id,t1,t2,attrs)</span>. Here, <span class="name">t1</span> MUST NOT be a placeholder. </li> <!-- <li>For each <span class="name">r</span> in {<span @@ -2199,13 +2201,9 @@ such that <span class="name">wasGeneratedBy(_gen; e,a1,_t1,[])</span> and <span class="name">used(_use; a2,e,_t2,[])</span> hold.</p> </div> + <p id="generation-use-communication-inference_text"> -<div class="note"> -A final check is required on <a class="rule-text" href="#generation-use-communication-inference"><span>TBD</span></a> to ensure that it does not lead to non-termination, when combined with -<a class="rule-text" href="#communication-generation-use-inference"><span>TBD</span></a>. - </div> - <div class='inference' id='generation-use-communication-inference'> <p> <span class="conditional">IF</span> <span class="name">wasGeneratedBy(_gen; e,a1,_t1,_attrs1)</span> @@ -2821,7 +2819,7 @@ <ul> <li> If <span class="name">t</span> and <span - class="name">t'</span> are concrete identifiers or values + class="name">t'</span> are constant identifiers or values (including the placeholder <span class="name">-</span>), then their <a>merge</a> exists only if they are equal, otherwise merging fails. </li> @@ -3007,7 +3005,7 @@ <p> Entities may have multiple generation or invalidation events (either or both may, however, be left implicit). An entity can be generated by more than one activity, with one generation event per - interaction. These events must be simultaneous, as required by <a + each entity-activity pair. These events must be simultaneous, as required by <a class="rule-ref" href="#generation-generation-ordering"><span>generation-generation-ordering</span></a> and <a