type constraints instead of type inference
authorLuc Moreau <l.moreau@ecs.soton.ac.uk>
Mon, 23 Jul 2012 13:09:25 +0100
changeset 4221 38f8310d8f28
parent 4220 34993bea2bef
child 4222 664adf1ff424
type constraints instead of type inference
model/prov-constraints.html
--- a/model/prov-constraints.html	Mon Jul 23 12:55:14 2012 +0100
+++ b/model/prov-constraints.html	Mon Jul 23 13:09:25 2012 +0100
@@ -325,23 +325,12 @@
 <p>This is the second public release of the PROV-CONSTRAINTS document. 
 This is a Last Call Working Draft. The design is not expected to change significantly, going forward, and now is the key time for external review.</p>
 
-<p>This specification identifies several  <a
+<p>This specification identifies  <a
 href="http://www.w3.org/2005/10/Process-20051014/tr#cfi">features at
-risk</a>:
-<ul><li>two related to the at-risk Mention feature of [[PROV-DM]]:
+risk</a> related to the at-risk Mention feature of [[PROV-DM]]:
 <a class="rule-text" href="#mention-specialization"><span>TBD</span></a> and
-<a class="rule-text" href="#mention-unique"><span>TBD</span></a></li>
-<li>one consisting of an inference about Communication <a
-class="rule-text"
-href="#generation-use-communication-inference"><span>TBD</span></a>
-that  may complicate implementations.
-</li>
-<li>one consisting of an inference about Derivation <a class="rule-text" href="#derivation-use"><span>TBD</span></a> that appears
-redundant.
-</li>
-<li>two consisting of inferences about entities <a class="rule-text" href="#entity-generation-invalidation-inference"><span>TBD</span></a> and activities <a class="rule-text" href="#activity-start-end-inference"><span>TBD</span></a> that may, together with certain
-other inference rules, lead to nontermination.</ul>
-<p>These might be removed from PROV-CONSTRAINTS.</p>
+<a class="rule-text" href="#mention-unique"><span>TBD</span></a>.
+These might be removed from PROV-CONSTRAINTS.</p>
 
 <h4>PROV Family of Specifications</h4>
 This document is part of the PROV family of specifications, a set of specifications defining various aspects that are necessary to achieve the vision of inter-operable
@@ -1281,7 +1270,7 @@
 
   
 
-<p>Communication between activities is <a
+<p id="communication-generation-use-inference_text">Communication between activities is <a
  title="definition">defined</a> as the existence of an underlying
 entity generated by one activity and used by the other.</p>
 
@@ -1297,10 +1286,8 @@
 </div>
 
 <div class="note">
-The following inference is a  "<a
-href="http://www.w3.org/2005/10/Process-20051014/tr#cfi">feature at
-risk</a>" and may be dropped if it leads to
-  implementation difficulties.
+A final check is required on this inference 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'>
@@ -1341,9 +1328,7 @@
 </div>
 </div>
 
-<div class="note">Luc: The narrative is not right for both
-<a class="rule-text" href="#entity-generation-invalidation-inference"><span>TBD</span></a> and <a class="rule-text" href="#activity-start-end-inference"><span>TBD</span></a>, since "there must have existed" does not work for entities and activities that are still extant. However, from a constraint checking, it is ok, to add such invalidation/end events, with a future time.</div>
-
+<!--
 <div class="note">
   The following two inferences could interact with type inference to produce
   nontermination.  For example, once we have an activity we can yse
@@ -1359,17 +1344,21 @@
   implementability.  I propose to drop both of the following
   inferences, since they seem less necessary than the type inferences.
   </div>
-
+-->
  
 <hr />
+
+<!--
   <div class="note">
     The following inference is a  "<a
 href="http://www.w3.org/2005/10/Process-20051014/tr#cfi">feature at
 risk</a>" and may be dropped if it leads to
   implementation difficulties.
     </div>
+-->
+
 <p id="entity-generation-invalidation-inference_text">
-From an entity, we can infer that the existence of
+From an entity, we can infer that existence of
 generation and invalidation events.
 </p>
 <div class='inference' id='entity-generation-invalidation-inference'>
@@ -1385,14 +1374,16 @@
 
 
 <hr />
+<!--
   <div class="note">
     The following inference is a  "<a
 href="http://www.w3.org/2005/10/Process-20051014/tr#cfi">feature at
 risk</a>" and may be dropped if it leads to
   implementation difficulties.
-    </div>
+    </div>-->
+
 <p id="activity-start-end-inference_text">
-From an activity statement we can infer that there must have existed
+From an activity statemen,t we can infer that 
 start and end events having times matching the start and end times of
 the activity.
 </p>
@@ -1487,9 +1478,7 @@
 
 <p id='derivation-use_text'>Derivations with an explicit activity and
 no specified generation and usage admit the  following inference: </p>
-<div class="note">The following inference is a "<a
-href="http://www.w3.org/2005/10/Process-20051014/tr#cfi">feature at
-risk</a>" because it
+<div class="note">Final check required. The following inference
   appears redundant (it can be derived using other rules).
   </div>
 <div class='inference' id='derivation-use'>
@@ -3197,7 +3186,7 @@
   </li>
   <li>
   If no
-  such cycle exists, and none of the impossibility constraints are
+  such cycle exists, and none of the impossibility constraints and typing constraints are
   violated, then <span class="math">I</span> is <a>valid</a>.
   </li>
   </ol>