* constraints
authorjcheney@inf.ed.ac.uk
Fri, 08 Feb 2013 18:44:44 +0000
changeset 5519 e3113a4afbb9
parent 5518 a87ae9fe320f
child 5520 9cff043c2e77
* constraints
model/prov-constraints.html
--- a/model/prov-constraints.html	Fri Feb 08 17:04:07 2013 +0000
+++ b/model/prov-constraints.html	Fri Feb 08 18:44:44 2013 +0000
@@ -1516,7 +1516,7 @@
     </div>
 
 </section>
-<section class="informative">
+<section id="overview" class="informative">
 <h4>Validation Process Overview</h4>
 
 
@@ -2011,7 +2011,9 @@
 <!--Analogously to blank nodes in
 [[RDF]],-->
 The scope of an existential variable in PROV is delimited at the instance
-level, so existential variables with the same name occurring in
+level.  This means that occurrences of existential variables with the
+  same name appearing in different statements within the same
+  instance stand for a common, unknown term.  However, existential variables with the same name occurring in
 different instances do not necessarily denote the same term.  This
 is a consequence of the fact that the instances of two equivalent
 documents only need to be  pairwise isomorphic; this is a weaker
@@ -2373,6 +2375,8 @@
   appear inside an instance are often called <dfn>existential
   variables</dfn>, because they are implicitly existentially quantified.
 </p>
+
+
   
   <p> A <dfn id="term">PROV term</dfn> is a constant identifier
   <span class="math">c</span>, a placeholder <span
@@ -2465,6 +2469,13 @@
   <span class="math">S(I) = I'</span>.</p>
 
 
+<div class="remark">The scope of an existential variable is at the
+    instance level.  When we obtain information about an existential
+    variable, for example through unification or merging during
+    uniqueness constraint application, we substitute all other
+    occurrences of that variable occurring in the same instance.
+    Occurrences in other instances are not affected.  </div>
+  
 </section>
 <section id="inferences">
 <h2>Definitions and Inferences</h2>
@@ -2617,13 +2628,33 @@
    <div class="definition" id="optional-attributes">
 <ol>
   <li>
-  For each  <span class="name">p</span> in {<span
+<!--  For each  <span class="name">p</span> in {<span
    class="name">entity</span>, <span class="name">activity</span>,
    <span class="name">agent</span>}, if <span class="name">a<sub>n</sub></span> is not an attribute
    list parameter then the following definitional rule holds:
   <p><span class="name">p(a<sub>1</sub>,...,a<sub>n</sub>)</span> 
    <span  class="conditional">IF AND ONLY IF</span>   <span
    class="name">p(a<sub>1</sub>,...,a<sub>n</sub>,[])</span>.
+  -->
+<p>  The following definitional rules hold:</p>
+    <ul><li><span class="name">entity(id)</span> 
+   <span  class="conditional">IF AND ONLY IF</span>   <span
+   class="name">entity(id,[])</span>.
+    </li>
+    <li><span class="name">activity(id)</span> 
+   <span  class="conditional">IF AND ONLY IF</span>   <span
+   class="name">activity(id,[])</span>.
+    </li>
+   <li><span class="name">activity(id,t1,t2)</span> 
+   <span  class="conditional">IF AND ONLY IF</span>   <span
+   class="name">activity(id,t1,t2,[])</span>.
+    </li>
+    <li><span class="name">agent(id)</span> 
+   <span  class="conditional">IF AND ONLY IF</span>   <span
+   class="name">agent(id,[])</span>.
+    </li>
+    </ul>
+    <br />
   </li>
   <li>
      For each <span class="name">r</span> in { 
@@ -2905,7 +2936,7 @@
   missing activity, generation, and usage. In the latter form, it is not specified
   if one or more activities are involved in the derivation. </p>
 
- <p>Let us consider a system, in which a derivation is underpinned by multiple activities. Conceptually, one could also model such a system with a new activity that encompasses the two original activities and underpins the derivation.   The inferences defined in this specification do not allow the latter modelling to be inferred from the former. Hence, the two  modellings of the same system are regarded as different in the context of this specification.</p>
+ <p>Let us consider a system, in which a derivation is underpinned by multiple activities. Conceptually, one could also model such a system with a new activity that encompasses the two original activities and underpins the derivation.   The inferences defined in this specification do not allow the latter modeling to be inferred from the former. Hence, the two  modeling of the same system are regarded as different in the context of this specification.</p>
     </div>
 </section>
     
@@ -3059,7 +3090,7 @@
 
 <div class='inference' id='wasStartedBy-inference'>
 <p><span class='conditional'>IF</span>
- <span class="name">wasStartedBy(_id; a,e1,a1,_t,_attrs)</span>,
+ <span class="name">wasStartedBy(_id; _a,e1,a1,_t,_attrs)</span>,
 <span class='conditional'>THEN</span> there exist <span
   class="name">_gen</span> and  <span class="name">_t1</span>
 such that 
@@ -3077,7 +3108,7 @@
 
 <div class='inference' id='wasEndedBy-inference'>
 <p><span class='conditional'>IF</span>
- <span class="name">wasEndedBy(_id; a,e1,a1,_t,_attrs)</span>,
+ <span class="name">wasEndedBy(_id; _a,e1,a1,_t,_attrs)</span>,
 <span class='conditional'>THEN</span> there exist <span
   class="name">_gen</span> and <span class="name">_t1</span> such that 
  <span class="name">wasGeneratedBy(_gen; e1,a1,_t1,[])</span>.</p>
@@ -3335,7 +3366,7 @@
     <span class="conditional">IF</span> <span class="name">wasInformedBy(id; a2,a1,attrs)</span> <span class="conditional">THEN</span> <span class="name">wasInfluencedBy(id;  a2, a1, attrs)</span>.
   </li>
  <li>
-    <span class="conditional">IF</span> <span class="name">wasStartedBy(id; a2,e,a1,_t,attrs)</span> <span class="conditional">THEN</span> <span class="name">wasInfluencedBy(id;  a2, e, attrs)</span>.
+    <span class="conditional">IF</span> <span class="name">wasStartedBy(id; a2,e,_a1,_t,attrs)</span> <span class="conditional">THEN</span> <span class="name">wasInfluencedBy(id;  a2, e, attrs)</span>.
   </li>
   <li>
     <span class="conditional">IF</span> <span class="name">wasEndedBy(id; a2,e,_a1,_t,attrs)</span> <span class="conditional">THEN</span> <span class="name">wasInfluencedBy(id;  a2, e, attrs)</span>.
@@ -3345,10 +3376,10 @@
   </li>
  <li>
     <span class="conditional">IF</span> <span
-  class="name">wasDerivedFrom(id;  e2, e1, a, g, u, attrs)</span> <span
+  class="name">wasDerivedFrom(id;  e2, e1, _a, _g, _u, attrs)</span> <span
   class="conditional">THEN</span> <span
   class="name">wasInfluencedBy(id;  e2, e1, attrs)</span>.  Here,
-  <span class="name">a</span>, <span class="name">g</span>, <span class="name">u</span> MAY be placeholders <span class="name">-</span>.
+  <span class="name">_a</span>, <span class="name">_g</span>, <span class="name">_u</span> MAY be placeholders <span class="name">-</span>.
   </li>
 <li>
     <span class="conditional">IF</span> <span class="name">wasAttributedTo(id; e,ag,attrs)</span> <span class="conditional">THEN</span> <span class="name">wasInfluencedBy(id; e, ag, attrs)</span>.
@@ -4576,7 +4607,7 @@
   class="name">ag</span> is the subject of a
 <span
   class="name">wasEndedBy</span> statement, it is an activity according to the <a
-  href="#typing">typing constraints</a>.  Case 4 handes the symmetric
+  href="#typing">typing constraints</a>.  Case 4 handles the symmetric
   case, ensuring that the start of an agent-activity precedes the
   start of an associated activity. </p> </div>
 
@@ -5066,7 +5097,7 @@
   </p>
   <div class='constraint' id='membership-empty-collection'>
 <p> <span class="conditional">IF</span> 
- <span class="name">hasMember(c,e)</span> and
+ <span class="name">hadMember(c,e)</span> and
 <span class="name">'prov:EmptyCollection' &isin; typeOf(c)</span>
 <span class="conditional">THEN</span> <span class="conditional">INVALID</span>.</p>
   </div>
@@ -5553,7 +5584,22 @@
       Responses to Public Comments on the Candidate Recommendation</a>
       for more details about the justification of these changes.</p>
 <ul>
-  <li>Added clarification concerning constraint wasAssociatedWith-ordering.</li>
+  <li>Added clarification concerning constraint
+      <a href="#wasAssociatedWith-ordering">wasAssociatedWith-ordering</a> (issue-615).</li>
+      <li>Added underscores to some variables in inferences <a href="#wasStartedBy-inference">9</a>, <a href="#wasEndedBy-inference">10</a>,
+      <a href="#influence-inference">15</a> (issue-611).</li>
+      <li>Corrected a typo in the name <span
+      class="name">hadMember</span> in <a href="">constraint 56</a>
+      (issue-611).
+      </li>
+      <li>Clarified that existential variables are scoped at the
+      instance level, not statement level, thus it is correct to apply
+      uniqueness constraints by substituting variables through an
+      instance (issue-611).  (Remark at the end of <a href="#concepts">section
+      4. Basic concepts</a>, and clarified discussion in <a
+      href="#overview">Validation Process Overview</a>)</li>
+      <li>Gave equivalent form of <a
+      href="#optional-attributes">Definition 2</a> (issue-611).</li>
 </ul>
   
 </section>
@@ -5577,8 +5623,10 @@
 Jacek Kopecky,
 James Leigh,
 Jacco van Ossenbruggen,
+Héctor Pérez-Urbina,
 Alan Ruttenberg,
-Reza Samavi, and
+Reza Samavi,
+Evren Sirin, 
 Antoine Zimmermann.
 </p>
 
@@ -5685,7 +5733,7 @@
  -->
 <!--  LocalWords:  disjointness inferrable subtyping subtype subtypes hadMember
  -->
-<!--  LocalWords:  hasMember toplevel sameAs tuple acyclicity isomorphism IRI
+<!--  LocalWords: toplevel sameAs tuple acyclicity isomorphism IRI fff dfn xmpl
  -->
 <!--  LocalWords:  endBundle typeof equational acyclic invertible procedurally
  -->
@@ -5703,11 +5751,17 @@
  -->
 <!--  LocalWords:  Hodgson TopQuadrant Trung Huynh Klyne Revelytix Rensselaer
  -->
-<!--  LocalWords:  McCusker McGuinness Paolo Missier Luc Moreau Vinh Edoardo
+<!--  LocalWords:  McCusker McGuinness Paolo Missier Luc Moreau Vinh Edoardo pl
  -->
-<!--  LocalWords:  Pignotti Paulo Pinheiro Geospatial Retter Runnegar Satya
+<!--  LocalWords:  Pignotti Paulo Pinheiro Geospatial Retter Runnegar Satya gen
  -->
 <!--  LocalWords:  Sahoo Schaengold Schutzer FSTC Yogesh Simmhan Theodoridou
  -->
-<!--  LocalWords:  Thibodeau OpenLink Tilmes Zednik Zhao Yuting
+<!--  LocalWords:  Thibodeau OpenLink Tilmes Zednik Zhao Yuting anexample rgba
  -->
+<!--  LocalWords:  unamedconstraint deprecatedconstraint conceptexample prov
+ -->
+<!--  LocalWords:  pnExpression table.thinborder assoc Freimuth Satrajit Jacek
+ -->
+<!--  LocalWords:  Iannella Kopecky Jacco Ossenbruggen Ruttenberg Samavi
+ -->