--- a/model/prov-constraints.html Fri Aug 10 16:40:46 2012 +0100
+++ b/model/prov-constraints.html Fri Aug 10 17:21:36 2012 +0100
@@ -1114,7 +1114,7 @@
<tr class="component1-color">
<td class="essential"><a>Generation</a></td>
<td><a class="rule-text" href="#generation-use-communication-inference"><span>TBD</span></a><br>
- <a class="rule-text" href="#derivation-use-inference"><span>TBD</span></a><br>
+<!-- <a class="rule-text" href="#derivation-use-inference"><span>TBD</span></a><br>-->
<a class="rule-text" href="#influence-inference"><span>TBD</span></a><br>
<a class="rule-text" href="#key-properties"><span>TBD</span></a><br>
<a class="rule-text" href="#unique-generation"><span>TBD</span></a><br>
@@ -1217,8 +1217,8 @@
<tr class="component2-color">
<td class="essential"><a>Derivation</a></td>
<td><a class="rule-text" href="#derivation-generation-use-inference"><span>TBD</span></a><br>
- <a class="rule-text" href="#derivation-use-inference"><span>TBD</span></a><br>
- <a class="rule-text" href="#specific-derivation-inference"><span>TBD</span></a><br>
+<!-- <a class="rule-text" href="#derivation-use-inference"><span>TBD</span></a><br>-->
+<!-- <a class="rule-text" href="#specific-derivation-inference"><span>TBD</span></a><br>-->
<a class="rule-text" href="#influence-inference"><span>TBD</span></a><br>
<a class="rule-text" href="#key-properties"><span>TBD</span></a><br>
<a class="rule-text" href="#derivation-usage-generation-ordering"><span>TBD</span></a><br>
@@ -1648,7 +1648,8 @@
that are not <a title="expandable parameter">expandable</a> are
also listed. Parameters that cannot have value <span
class="name">-</span>, and identifiers that are
- expanded by <a class="rule-ref" href="#optional-identifiers"><span>TBD</span></a>, are not listed.</p>
+ expanded by <a class="rule-ref"
+ href="#optional-identifiers"><span>TBD</span></a>, are not listed.</p>
<div id="expandable-parameters-fig">
<table id="expandable-parameters" border="1" class="thinborder" style="margin-left: auto; margin-right: auto; border-color: black;">
<caption id="expandable-parameters">Table 2: Expandable and
@@ -1669,11 +1670,12 @@
<td class="name">a,t</td>
<td></td>
</tr>
- <tr>
+<!-- <tr>
<td class="name">wasInformedBy(id; a2,a1,attrs)</td>
<td class="name"></td>
<td></td>
</tr>
+ -->
<tr>
<td class="name">wasStartedBy(id; a2,e,a1,t,attrs)</td>
<td class="name">e,a1,t</td>
@@ -1690,10 +1692,16 @@
<td></td>
</tr>
<tr>
- <td class="name">wasDerivedFrom(id; e2,e1,a,g2,u1,attrs)</td>
- <td class="name">e1,e2</td>
- <td class="name">a,g2,u1</td>
+ <td class="name">wasDerivedFrom(id; e2,e1,-,g,u,attrs)</td>
+ <td class="name"></td>
+ <td class="name">g,u</td>
+ </tr> <tr>
+ <td class="name">wasDerivedFrom(id; e2,e1,a,g,u,attrs)</td>
+ <td class="name">g,u</td>
+ <td class="name">a</td>
+ <td> (where <span class="name">a</span> is not placeholder <span class="name">-</span>.)</td>
</tr>
+
<!--
<tr>
<td class="name">wasDerivedFrom(id; e2,e1,attrs)</td>
@@ -1701,11 +1709,12 @@
<td></td>
</tr>
-->
- <tr>
+<!-- <tr>
<td class="name">wasAttributedTo(id; e,ag,attr)</td>
<td class="name"></td>
<td></td>
</tr>
+ -->
<tr>
<td class="name">wasAssociatedWith(id; a,ag,pl,attrs)</td>
<td class="name">ag</td>
@@ -1716,16 +1725,26 @@
<td class="name">a</td>
<td></td>
</tr>
- <tr>
+<!-- <tr>
<td class="name">wasInfluencedBy(id; o2,o1,attrs)</td>
<td class="name"></td>
<td></td>
- </tr></table>
+ </tr>
+ -->
+ </table>
</div>
<p> <a class="rule-ref"
href="#optional-placeholders"><span>TBD</span></a> states how parameters are to be expanded,
- using the expandable parameters defined in the <a href="#expandable-parameters-fig">Table 2</a>.</p>
+ using the expandable parameters defined in <a
+ href="#expandable-parameters-fig">Table 2</a>. The last two parts
+ indicate how to handle expansion of parameters for
+ <span class="name">wasDerivedFrom</span> expansion, which is only allowed for the
+ generation and use parameters when the activity is specified. A
+ later constraint <a class="rule-ref"
+ href="impossible-unspecified-derivation-generation-use"><span>impossible-unspecified-derivation-generation-use</span></a>
+ forbids specifying generation and use parameters when the activity
+ is unspecified.</p>
<div class="definition" id="optional-placeholders">
<ol><li>
@@ -1748,22 +1767,31 @@
<li>For each <span class="name">r</span> in {
<span class="name">used</span>,
<span class="name">wasGeneratedBy</span>,
-<span class="name">wasInformedBy</span>,
+<!--<span class="name">wasInformedBy</span>,-->
<span class="name">wasStartedBy</span>,
<span class="name">wasEndedBy</span>,
<span class="name">wasInvalidatedBy</span>,
-<span class="name">wasDerivedFrom</span>,
-<span class="name">wasAttributedTo</span>,
+<!--<span class="name">wasDerivedFrom</span>,-->
+<!--<span class="name">wasAttributedTo</span>,-->
<span class="name">wasAssociatedWith</span>,
<span class="name">actedOnBehalfOf</span>,
- <span class="name">wasInfluencedBy</span>}, if the <span class="name">i</span>th parameter
+ <!--<span class="name">wasInfluencedBy</span>
+ -->
+ }, if the <span class="name">i</span>th parameter
of <span class="name">r</span> is an <a>expandable parameter</a>
of <span class="name">r</span>
as specified in <a href="#expandable-parameters-fig">Table 2</a>
then the following definition holds:
<p> <span class="name">r(a<sub>0</sub>;...,a<sub>i-1</sub>, -, a<sub>i+1</sub>, ...,a<sub>n</sub>) </span> <span class="conditional">IF AND ONLY IF</span> there exists <span class="name">a'</span>
such that <span class="name">r(a<sub>0</sub>;...,a<sub>i-1</sub>,a',a<sub>i+1</sub>,...,a<sub>n</sub>)</span>.
- </li></ol>
+ </li>
+ <li>If <span class="name">a</span> is not the placeholder <span class="name">-</span>, and <span class="name">u</span> is any term, then the following definition holds:
+ <p> <span class="name">wasDerivedFrom(id;e2,e1,a,-,u,attrs)</span> <span class="conditional">IF AND ONLY IF</span> there exists <span class="name">g</span>
+ such that <span class="name">wasDerivedFrom(id; e2,e1,a,g,u,attrs)</span>.</li>
+ <li>If <span class="name">a</span> is not the placeholder <span class="name">-</span>, and <span class="name">g</span> is any term,
+ then the following definition holds:
+ <p> <span class="name">wasDerivedFrom(id;e2,e1,a,g,-,attrs)</span> <span class="conditional">IF AND ONLY IF</span> there exists <span class="name">u</span>
+ such that <span class="name">wasDerivedFrom(id; e2,e1,a,g,u,attrs)</span>.</li></ol>
</div>
<div class="remark">
@@ -1997,6 +2025,7 @@
</p>
</div>
<p>
+<!--
<hr>
<p id='derivation-use-inference_text'>According to <a class="rule-text"
@@ -2048,8 +2077,10 @@
the generation of <span
expanclass="name">e2</span>).</p>
</div>
-
-<hr />
+-->
+
+<!--
+ <hr />
<div class="note">
Likely to delete specific-derivation-inference
</div>
@@ -2070,7 +2101,7 @@
class="name">wasDerivedFrom(id; e2,e1,-,-,-,attrs)</span>.
</p>
</div>
-
+-->
<hr />
<p id="revision-is-alternate-inference_text">A revision admits the following inference, stating that the two entities
@@ -3550,143 +3581,7 @@
</section> <!--event-ordering-constraints-->
-<section id="impossibility-constraints">
-<h3>Impossibility constraints</h3>
-
-<p> Impossibility constraints require that certain patterns of
-statements never appear in <a>valid</a> PROV instances. Impossibility
-constraints have the following general form:
-</p>
-
-<div class="constraint-example" id="impossible-example">
- <p><span class="conditional">IF</span> <span class="name">hyp<sub>1</sub></span> and ... and <span class="name">hyp<sub>n</sub></span> <span class="conditional">THEN</span> <span class="conditional">INVALID</span>.</p>
- </div>
-
-<p> Checking an impossibility constraint on instance <span
- class="math">I</span> means checking whether there is
-any way of matching the pattern <span class="name">hyp<sub>1</sub></span>, ..., <span class="name">hyp<sub>n</sub></span>. If there
-is, then checking the constraint on <span class="math">I</span> fails (which implies that
-<span class="math">I</span> is invalid).
-
-
-<hr />
-
- <div class="note">
- @TODO: Add constraint to the effect that in a normal form,
- wasDerivedFrom(e1,e2,-,g,u) is only legal if g and u are also "-".
- </div>
-
-<hr />
-
-<p id="impossible-specialization-reflexive_text">As noted previously, specialization is a
- <a>strict partial order</a>: it is <a>irreflexive</a> and
- <a>transitive</a>.</p>
-
- <div class='constraint' id="impossible-specialization-reflexive">
-<!--<p>
- For any entity <span class='name'>e</span>, it is not the case that
-<span class='name'>specializationOf(e,e)</span> holds.</p>-->
- <p> <span class="conditional">IF</span> <span class="name">specializationOf(e,e)</span> <span class="conditional">THEN</span> <span class="conditional">INVALID</span>.</p>
- </div>
-
-
- <!--
-<hr>
-<div class="note"> This is also a constraint, but follows from
- irreflexivity and transitivity so it may be omitted.</div>
-
- <p id="specialization-asymmetric_text"/>
-
-<div class='constraint' id="impossible-specialization-symmetric">
-<p> For any
- entities <span class='name'>e1</span>, <span
- class='name'>e2</span>,
-it is not the case that
- <span class='name'>specializationOf(e1,e2)</span>
- and
- <span class='name'>specializationOf(e2,e1)</span>.</p>
-</div>
--->
-
-
- <hr />
-
-
- <p id='impossible-property-overlap_text'> Furthermore, identifiers
- of basic relationships are disjoint.
- </p>
- <div class='constraint' id='impossible-property-overlap'>
- <p>
-For each <span class="name">r</span> and <span class="name">s</span>
- in {
-<span class="name">used</span>,
-<span class="name">wasGeneratedBy</span>,
-<span class="name">wasInvalidatedBy</span>,
-<span class="name">wasStartedBy</span>,
-<span class="name">wasEndedBy</span>,
-<span class="name">wasInformedBy</span>,
-<span class="name">wasAttributedTo</span>,
-<span class="name">wasAssociatedWith</span>,
-<span class="name">actedOnBehalfOf</span>} such that <span class="name">r</span> and <span class="name">s</span>
- are different relation names, the
- following constraint holds:
-</p>
- <p>
- <span class="conditional">IF</span> <span class="name">r(id; a<sub>1</sub>,...,a<sub>n</sub>)</span> and <span class="name">s(id; b<sub>1</sub>,...,b<sub>n</sub>)</span> <span class="conditional">THEN INVALID</span>.
- </p>
- </div>
-
- <div class="remark">
- <p>Since <span class="name">wasInfluencedBy</span> is a superproperty of many other
- properties, it is excluded from the set of properties whose
- identifiers are required to be pairwise disjoint. The following
- example illustrates this observation:
- <pre>
-wasInfluencedBy(id;e2,e1)
-wasDerivedFrom(id;e2,e1)
-</pre>
- This satisfies the disjointness constraint.
- </p>
- <p>There is, however, no
- constraint requiring that every influence relationship is
- accompanied by a more specific relationship having the same
- identifier. The following valid example illustrates this observation:
- <pre>
-wasInfluencedBy(id; e2,e1)
-</pre>
- This is valid; there is no inferrable information about what kind
- of influence relates <span class="name">e2</span> and <span class="name">e1</span>, other than its identity.
- </p>
- </div>
-
- <p id='impossible-object-property-overlap_text'> Identifiers of entities,
- agents and activities cannot also be identifiers of properties.
- </p>
- <div class='constraint' id='impossible-object-property-overlap'>
- <p>
-For each <span class="name">p</span> in {<span class="name">entity</span>, <span class="name">activity</span>
- or <span class="name">agent</span>} and for each <span class="name">r</span> in {
-<span class="name">used</span>,
-<span class="name">wasGeneratedBy</span>,
-<span class="name">wasInvalidatedBy</span>,
-<span class="name">wasInfluencedBy</span>,
-<span class="name">wasStartedBy</span>,
-<span class="name">wasEndedBy</span>,
-<span class="name">wasInformedBy</span>,
-<span class="name">wasDerivedFrom</span>,
-<span class="name">wasAttributedTo</span>,
-<span class="name">wasAssociatedWith</span>,
-<span class="name">actedOnBehalfOf</span>}, the following
- impossibility constraint holds:</p>
-
-<p> <span class="conditional">IF</span> <span class="name">p(id,a<sub>1</sub>,...,a<sub>n</sub>)</span> and
- <span class="name">r(id; b<sub>1</sub>,...,b<sub>n</sub>)</span> <span class="conditional">THEN INVALID</span>.
- </p>
- </div>
-
-
-
-</section> <!--impossibility-constraints -->
+
<section id="type-constraints">
<h2>Type Constraints</h2>
@@ -3901,6 +3796,165 @@
</ol>
</div>
+</section> <!--type-constraints-->
+
+<section id="impossibility-constraints">
+<h3>Impossibility constraints</h3>
+
+<p> Impossibility constraints require that certain patterns of
+statements never appear in <a>valid</a> PROV instances. Impossibility
+constraints have the following general form:
+</p>
+
+<div class="constraint-example" id="impossible-example">
+ <p><span class="conditional">IF</span> <span class="name">hyp<sub>1</sub></span> and ... and <span class="name">hyp<sub>n</sub></span> <span class="conditional">THEN</span> <span class="conditional">INVALID</span>.</p>
+ </div>
+
+<p> Checking an impossibility constraint on instance <span
+ class="math">I</span> means checking whether there is
+any way of matching the pattern <span class="name">hyp<sub>1</sub></span>, ..., <span class="name">hyp<sub>n</sub></span>. If there
+is, then checking the constraint on <span class="math">I</span> fails (which implies that
+<span class="math">I</span> is invalid).
+
+
+<hr />
+
+ <div class="note">
+ @TODO: Add constraint to the effect that in a normal form,
+ wasDerivedFrom(e1,e2,-,g,u) is only legal if g and u are also "-".
+ </div>
+ <p id="impossible-unspecified-derivation-generation-use_text">
+A derivation with unspecified activity <span class="name">wasDerivedFrom(id;e1,e2,-,g,u,attrs)</span> represents a derivation that
+ takes one or more steps, whose activity, generation and use events
+ are unspecified. It is forbidden to specify a generation or use
+ event without specifying the activity.</p>
+
+ <div class='constraint' id="impossible-specialization-reflexive">
+<p> In the following rules, <span class="name">g</span> and <span class="name">u</span> MUST NOT be <span class="name">-</span>.</p>
+ <ol>
+ <li> <span class="conditional">IF</span>
+ <span class="name">wasDerivedFrom(_id;_e2,_e1,-,g,-,attrs)</span>
+ <span class="conditional">THEN</span> <span
+ class="conditional">INVALID</span>.</li> <li> <span class="conditional">IF</span>
+ <span class="name">wasDerivedFrom(_id;_e2,_e1,-,-,u,attrs)</span>
+ <span class="conditional">THEN</span> <span
+ class="conditional">INVALID</span>.</li>
+ <li> <span class="conditional">IF</span>
+ <span class="name">wasDerivedFrom(_id;_e2,_e1,-,g,u,attrs)</span>
+ <span class="conditional">THEN</span> <span
+ class="conditional">INVALID</span>.</li>
+ </ol>
+ </div>
+<hr />
+
+<p id="impossible-specialization-reflexive_text">As noted previously, specialization is a
+ <a>strict partial order</a>: it is <a>irreflexive</a> and
+ <a>transitive</a>.</p>
+
+ <div class='constraint' id="impossible-specialization-reflexive">
+<!--<p>
+ For any entity <span class='name'>e</span>, it is not the case that
+<span class='name'>specializationOf(e,e)</span> holds.</p>-->
+ <p> <span class="conditional">IF</span> <span class="name">specializationOf(e,e)</span> <span class="conditional">THEN</span> <span class="conditional">INVALID</span>.</p>
+ </div>
+
+
+ <!--
+<hr>
+<div class="note"> This is also a constraint, but follows from
+ irreflexivity and transitivity so it may be omitted.</div>
+
+ <p id="specialization-asymmetric_text"/>
+
+<div class='constraint' id="impossible-specialization-symmetric">
+<p> For any
+ entities <span class='name'>e1</span>, <span
+ class='name'>e2</span>,
+it is not the case that
+ <span class='name'>specializationOf(e1,e2)</span>
+ and
+ <span class='name'>specializationOf(e2,e1)</span>.</p>
+</div>
+-->
+
+
+ <hr />
+
+
+ <p id='impossible-property-overlap_text'> Furthermore, identifiers
+ of basic relationships are disjoint.
+ </p>
+ <div class='constraint' id='impossible-property-overlap'>
+ <p>
+For each <span class="name">r</span> and <span class="name">s</span>
+ in {
+<span class="name">used</span>,
+<span class="name">wasGeneratedBy</span>,
+<span class="name">wasInvalidatedBy</span>,
+<span class="name">wasStartedBy</span>,
+<span class="name">wasEndedBy</span>,
+<span class="name">wasInformedBy</span>,
+<span class="name">wasAttributedTo</span>,
+<span class="name">wasAssociatedWith</span>,
+<span class="name">actedOnBehalfOf</span>} such that <span class="name">r</span> and <span class="name">s</span>
+ are different relation names, the
+ following constraint holds:
+</p>
+ <p>
+ <span class="conditional">IF</span> <span class="name">r(id; a<sub>1</sub>,...,a<sub>n</sub>)</span> and <span class="name">s(id; b<sub>1</sub>,...,b<sub>n</sub>)</span> <span class="conditional">THEN INVALID</span>.
+ </p>
+ </div>
+
+ <div class="remark">
+ <p>Since <span class="name">wasInfluencedBy</span> is a superproperty of many other
+ properties, it is excluded from the set of properties whose
+ identifiers are required to be pairwise disjoint. The following
+ example illustrates this observation:
+ <pre>
+wasInfluencedBy(id;e2,e1)
+wasDerivedFrom(id;e2,e1)
+</pre>
+ This satisfies the disjointness constraint.
+ </p>
+ <p>There is, however, no
+ constraint requiring that every influence relationship is
+ accompanied by a more specific relationship having the same
+ identifier. The following valid example illustrates this observation:
+ <pre>
+wasInfluencedBy(id; e2,e1)
+</pre>
+ This is valid; there is no inferrable information about what kind
+ of influence relates <span class="name">e2</span> and <span class="name">e1</span>, other than its identity.
+ </p>
+ </div>
+
+ <p id='impossible-object-property-overlap_text'> Identifiers of entities,
+ agents and activities cannot also be identifiers of properties.
+ </p>
+ <div class='constraint' id='impossible-object-property-overlap'>
+ <p>
+For each <span class="name">p</span> in {<span class="name">entity</span>, <span class="name">activity</span>
+ or <span class="name">agent</span>} and for each <span class="name">r</span> in {
+<span class="name">used</span>,
+<span class="name">wasGeneratedBy</span>,
+<span class="name">wasInvalidatedBy</span>,
+<span class="name">wasInfluencedBy</span>,
+<span class="name">wasStartedBy</span>,
+<span class="name">wasEndedBy</span>,
+<span class="name">wasInformedBy</span>,
+<span class="name">wasDerivedFrom</span>,
+<span class="name">wasAttributedTo</span>,
+<span class="name">wasAssociatedWith</span>,
+<span class="name">actedOnBehalfOf</span>}, the following
+ impossibility constraint holds:</p>
+
+<p> <span class="conditional">IF</span> <span class="name">p(id,a<sub>1</sub>,...,a<sub>n</sub>)</span> and
+ <span class="name">r(id; b<sub>1</sub>,...,b<sub>n</sub>)</span> <span class="conditional">THEN INVALID</span>.
+ </p>
+ </div>
+
+
+
<hr />
<p id='entity-activity-disjoint_text'> The set of entities and activities are disjoint, expressed by
@@ -3945,7 +3999,8 @@
</div>
-</section>
+
+</section> <!--impossibility-constraints -->
</section> <!-- constraints -->