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