* Added some further discussion of constraints
authorJames Cheney <jcheney@inf.ed.ac.uk>
Tue, 17 Jul 2012 13:12:57 +0100
changeset 4081 dfeec9a5c0a6
parent 4080 814fd0d24ee1
child 4083 1f56fd7ed2c2
* Added some further discussion of constraints
model/prov-constraints.html
--- 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 &#8746; 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>