--- a/model/prov-constraints.html Mon Jul 16 16:26:20 2012 -0400
+++ b/model/prov-constraints.html Tue Jul 17 13:12:57 2012 +0100
@@ -1228,46 +1228,137 @@
</li>
</ul>
- Uniqueness constraints are checked through <a>merging</a> pairs of
- statements.
+ <section
+ id="uniqueness-constraints">
-<div class="note">
- TODO: More about what it means for constraints to be satisfied;
- constraint template(s)
+
+ <h3>Uniqueness Constraints</h3>
+
+
+
+ <p> Uniqueness constraints are checked through <a>merging</a> pairs of
+ statements subject to equalities. For example, suppose we have
+ two activity statements <span class="name">activity(a,t1,-,[a=1])</span>
+ and <span class="name">activity(a,-,t2,[b=2])</span>. The
+ <a>merge</a> of these two statements (describing the same activity
+ <span class="name">a</span>) is <span
+ class="name">activity(a,t1,t2,[a=1,b=2])</span>.
+ </p>
+
+ <p> Merging can be applied
+ to a pair of terms, a pair of attributes, or a pair of statements.
+ The result of merging is either a substitution (mapping
+ existentially quantified variables to terms) or a special symbol
+ <span class="name">undefined</span> indicating that the merge
+ cannot be performed. Merging of pairs of terms, attribute lists,
+ or statements is defined as follows.</p>
+
+ <ul>
+ <li> If <span class="name">t</span> and <span
+ class="name">t'</span> are concrete identifiers or values, then
+ their <a>merge</a> exists only if they are equal, otherwise merging
+ is undefined. </li>
+ <li> If one <span class="name">t</span> and
+ <span class="name">t'</span> is an existential variable, then their
+ <a>merge</a> is </li>
+ <li> The <a>merge</a> of two attribute lists <span
+ class="name">attrs1</span> and <span class="name">attrs2</span>
+ is their union, considered as unordered lists:, written <span
+ class="name">attrs1 ∪ attrs2</span> </li>
+ <li> If <span class="name">r(id;t_1,...,t_n,attrs1)</span> and
+ <span class="name">r(id;u_1,...,u_n,attrs2)</span> are two
+ statements with the same name, same identifier, and same number
+ of arguments, then
+ </li>
+ </ul>
+
+
+A typical uniqueness constraint is as follows:
+ <div class="constraint-example" id="uniqueness-example">
+<p> IF hyp_1 AND ... AND hyp_n THEN t_1 = u_1 AND ... AND t_n = u_n.</p>
</div>
+ where
+
+ In the common case that a particular field of a relation uniquely
+ determines the other fields, we call the uniqueness constraint a
+ <a>key constraint</a>. Key constraints are written as follows:
+
+ <div
+ class="constraint-example" id="key-example">
+ <p>The <span
+ class="name">a_k</span> field is a KEY for relation <span
+ class="name">r(a_0;a_1,...a_n)</span>. </p></div>
+
+ A key constraint is interpreted as a uniqueness constraint of the
+ following form:
+ <div
+ class="constraint-example" id="key-example-expanded">
+ <p>IF <span
+ class="name">r(a_0;a_1,...a_n)</span> AND <span
+ class="name">r(b_0;b_1,...b_n)</span> (where a_k = b_k) THEN <span
+ class="name">a_0 = b_0 </span> AND ... AND <span
+ class="name">a_n = b_n</span>. </p></div>
+
+<p>If a PROV instance contains an apparent violation of a uniqueness
+ constraint or key constraint, merging can be used to determine
+ whether the constraint can be satisfied by unifying an existential
+ variable with another term. For key constraints, this is the same
+ as merging pairs of statements whose keys are equal, because after
+ merging, the two statements become equal and one can be omitted.
+ Finally, the substitution obtained by merging is applied to all
+ other statements in the instance, to reflect additional knowledge
+ about existential variables gained through merging.</p>
- <section id="uniqueness-constraints">
-<h3>Uniqueness Constraints</h3>
- <div class="note"> More explanation about constraints. Non-examples
- such as attributes not necessarily being unique. Define merging semantics.</div>
+
+
+
+
<p>
<hr>
- <p id='unique-entity_text'> We assume that the various identified objects of PROV-DM have
- unique statements describing them within a PROV instance.
+ <p id='key_text'> We assume that the various identified objects of PROV-DM have
+ unique statements describing them within a PROV instance, through
+ the following key constraints:
</p>
- <div class='constraint' id='unique-entity'>
-<p>Given an entity identifier <span class="name">e</span>, there is at
- most one expression
-<span class="name">entity(e,attrs)</span>, where <span
- class="name">attrs</span> is some set of attribute-values.</p>
- </div>
- <div class='constraint' id='unique-activity'>
-<p>Given an activity identifier <span class="name">a</span>, there is
- at most one expression
-<span class="name">activity(a,t1,t2,attrs)</span>, where <span
- class="name">attrs</span> is some set of attribute-values.</p>
- </div>
- <div class="note">TODO: Same goes for all other objects:
- agent, note, generation, usage, invalidation, start, end,
- communication, start by, attribution, association, delegation,
- derivation, revision, quotation. We should find a
- way of saying this once concisely.
+ <div class='constraint' id='key-object'>
+<p><ol>
+ <li>The identifier field <span class="name">e</span> is a KEY for
+ the <span class="name">entity(e,attrs)</span> statement.
+ </li>
+ <li>The identifier field <span class="name">a</span> is a KEY for
+ the <span class="name">activity(a,t1,t2,attrs)</span> statement.
+ </li>
+<li>The identifier field <span class="name">ag</span> is a KEY for
+ the <span class="name">agent(ag,attrs)</span> statement.
+ </li>
+ </ol>
+ </p>
+ </div>
+
+ <hr />
+ <p id='key_relation_text'> Likewise, we assume that the identifiers
+ of relationships in PROV-DM uniquely identify the corresponding statements a PROV instance, through
+ the following key constraints:
+ </p>
+ <div class='constraint' id='key-relation'>
+<p><ol>
+ <li>The identifier field <span class="name">use</span> is a KEY for
+ the <span class="name">used(use;a,e,t,attrs)</span> statement.
+ </li>
+ <li>The identifier field <span class="name">gen</span> is a KEY for
+ the <span class="name">wasGeneratedBy(gen;e,a,t,attrs)</span> statement.
+ </li>
+ <li>...</li>
+ </ol>
+</p> </div>
+ <div class="note">@@TODO: Same goes for other relations:
+generation, usage, invalidation, start, end,
+ communication, attribution, association, delegation,
+ derivation, revision, quotation.
</div>
-<p>
<hr>
@@ -1473,6 +1564,26 @@
instance.</p>
+<p> A typical ordering constraint is as follows.</p>
+
+ <div
+ class="constraint-example" id="ordering-example">
+ <p>IF <span
+ class="name">hyp_1</span> AND ... AND <span
+ class="name">hyp_n</span> THEN <span
+ class="name">a_0</span> <a>precedes</a>/<a>strictly precedes</a> <span
+ class="name">b_0</span>. </p></div>
+ <p>
+ The conclusion of an ordering constraint is either <a>precedes</a>
+ or <a>strictly precedes</a>. To check ordering constraints, we
+ generate all possible <a>precedes</a> and <a>strictly precedes</a>
+ relationships (including transitive), and check that the resulting
+ relation has no strict cycles (that is, the <a>strictly precedes</a>
+ relation induced by the edges is irreflexive). This is equivalent to
+ constructing a directed graph, with edges marked <a>precedes</a> or
+ <a>strictly precedes</a>, and checking that there is no cycle
+ containing a <a>strictly-precedes</a> edge.
+ </p>