--- a/model/prov-constraints.html Thu Jul 19 18:44:06 2012 +0200
+++ b/model/prov-constraints.html Thu Jul 19 19:53:04 2012 +0100
@@ -325,9 +325,23 @@
<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 two <a href="http://www.w3.org/2005/10/Process-20051014/tr#cfi">features at risk</a>, related to Mention [[PROV-DM]]:
+<p>This specification identifies several <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]]:
<a class="rule-text" href="#mention-specialization"><span>TBD</span></a> and
-<a class="rule-text" href="#mention-unique"><span>TBD</span></a> might be removed from PROV if implementation experience reveals problems with supporting this construct.</p>
+<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="#inference-generation-use-communication"><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="#inference-entity-generation-invalidation"><span>TBD</span></a> and activities <a class="rule-text" href="#inference-activity-start-end"><span>TBD</span></a> that may, together with certain
+other inference rules, lead to nontermination.</ul>
+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
@@ -766,7 +780,7 @@
class="name">a<sub>m</sub></span> for unknown objects. These fresh
identifiers might later be found to be equal to known identifiers;
they play a similar role in PROV constraints to existential
- variables in logic or to blank nodes in [[RDF]]. With a few
+ variables in logic, "labeled nulls" in database theory [[DBCONSTRAINTS]], or to blank nodes in [[RDF]]. With a few
exceptions (discussed below), omitted optional parameters to
[[PROV-N]] statements, or explicit <span class="name">-</span>
markers, are placeholders for existentially quantified variables;
@@ -812,25 +826,29 @@
<section>
<h4>Optional Identifiers and Attributes</h4>
- <p>Many PROV relation statements have an identifier,
- identifying a link between two or more related objects. Identifiers
- can sometimes be omitted in [[PROV-N]] notation.
- For the purpose of inference and validity checking, we generate
- special identifiers called <dfn>existential variables</dfn> denoting
- the unknown values.
- </p>
+ <p>Many PROV relation statements have an identifier, identifying a
+ link between two or more related objects. Identifiers can sometimes
+ be omitted in [[PROV-N]] notation. For the purpose of inference and
+ validity checking, we generate special identifiers called
+ <dfn>existential variables</dfn> denoting the unknown values.
+ Existential variables can be <em>substituted</em> with constant
+ identifiers, literals, the placeholder <span class="name">-</span>,
+ or other <a>existential variables</a>. </p>
<div class="definition" id="optional-identifiers">
-<p> Suppose <span class="name">r</span> is in {
+<p>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>}</p>
+<span class="name">actedOnBehalfOf</span>}, the following
+ definitional rules hold:</p>
<ol> <li>
<span class="name">r(a<sub>1</sub>,...,a<sub>n</sub>) </span> holds <span class="conditional">IF AND ONLY IF</span>
there exists <span class="name">id</span> such that <span
@@ -847,22 +865,30 @@
<div class="definition" id="optional-attributes">
<ol>
<li>
-Suppose <span class="name">r</span> is in {<span class="name">entity</span>, <span class="name">activity</span> or <span class="name">agent</span>}. Then <span class="name">r(a<sub>1</sub>,...,a<sub>n</sub>)</span> holds and does not contain an explicit attribute
- list <span class="conditional">IF AND ONLY IF</span> <span
+For each <span class="name">r</span> in {<span
+ class="name">entity</span>, <span class="name">activity</span>,
+ <span class="name">agent</span>}, if <span class="name">a_n</span> is not an attribute
+ list parameter then the following definitional rule holds:</p>
+ <p><span class="name">r(a<sub>1</sub>,...,a<sub>n</sub>)</span>
+ holds <span class="conditional">IF AND ONLY IF</span> <span
class="name">r(a<sub>1</sub>,...,a<sub>n</sub>,[])</span> holds.</li>
<li>
- Similarly, suppose <span class="name">r</span> is in {
+ For each <span class="name">r</span> in {
<span class="name">used</span>,
<span class="name">wasGeneratedBy</span>,
+<span class="name">wasInvalidated</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>}.
- Then <span class="name">r(id;a<sub>1</sub>,...,a<sub>n</sub>)</span> holds and does not contain an explicit attribute
- list <span class="conditional">IF AND ONLY IF</span> <span
+<span class="name">actedOnBehalfOf</span>}, if <span class="name">a_n</span> is not an
+ attribute list parameter then the following definition holds:</p>
+
+ <p> <span class="name">r(id;a<sub>1</sub>,...,a<sub>n</sub>)</span> holds
+ <span class="conditional">IF AND ONLY IF</span> <span
class="name">r(id;a<sub>1</sub>,...,a<sub>n</sub>,[])</span> holds.</li></ol>
</div>
@@ -871,10 +897,6 @@
used if none of the optional arguments is present. These are
handled by specific rules listed below. </p>
- <div class="note"> The following list assumes that we have already
- expanded id and attribute parameters, so that we do not need
- extra cases. Moreover it assumes that "-" will be normalized
- away in the next step.</div>
<div class="definition" id="definition-short-forms">
<p>
@@ -932,34 +954,106 @@
the <span class="name">plan</span> parameter in <span class="name">wasAssociatedWith</span>.
</p>
- <div class="note">
- The following is a template for a large number of more precise
- rules specifying how to fill in optional parameters. It would be
- nice to find a uniform way of saying this without lots of tedious
- rules, since the expansion is completely uniform except for the
- plan parameter.</div>
+ <p>The following table characterizes the <dfn>expandable
+ parameter</dfn>s of the properties of PROV, needed in the
+ following definition. For emphasis, the two optional parameters
+ that are not <a title="expandable parameter">expandable</a> are
+ also listed.</p>
+ <table border=1>
+ <tr>
+ <th>Relation</th>
+ <th>Expandable</th>
+ <th>Non-expandable</th>
+ </tr>
+ <tr>
+ <td class="name">wasGeneratedBy(id;e,a,t,attrs)</td>
+ <td class="name">id,a,t</td>
+ <td></td>
+ </tr>
+ <tr>
+ <td class="name">used(id;a,e,t,attrs)</td>
+ <td class="name">id,e,t</td>
+ <td></td>
+ </tr>
+ <tr>
+ <td class="name">wasInformedBy(id;a2,a1,attrs)</td>
+ <td class="name">id</td>
+ <td></td>
+ </tr>
+ <tr>
+ <td class="name">wasStartedBy(id;a2,e,a1,t,attrs)</td>
+ <td class="name">id,e,a1,t</td>
+ <td></td>
+ </tr>
+ <tr>
+ <td class="name">wasEndedBy(id;a2,e,a1,t,attrs)</td>
+ <td class="name">id,e,a1,t</td>
+ <td></td>
+ </tr>
+ <tr>
+ <td class="name">wasInvalidatedBy(id;e,a,t,attrs)</td>
+ <td class="name">id,a,t</td>
+ <td></td>
+ </tr>
+ <tr>
+ <td class="name">wasDerivedFrom(id;e2,e1,a,g2,u1,attrs)</td>
+ <td class="name">id,g2,u1</td>
+ <td class="name">a</td>
+ </tr>
+ <tr>
+ <td class="name">wasDerivedFrom(id;e2,e1,attrs)</td>
+ <td class="name">id</td>
+ <td></td>
+ </tr>
+ <tr>
+ <td class="name">wasAttributedTo(id;e,ag,attr)</td>
+ <td class="name">id</td>
+ <td></td>
+ </tr>
+ <tr>
+ <td class="name">wasAssociatedWith(id;a,ag,pl,attrs)</td>
+ <td class="name">id,ag</td>
+ <td class="name">pl</td>
+ </tr>
+ <tr>
+ <td class="name">actedOnBehalfOf(id;ag2,ag1,a,attrs)</td>
+ <td class="name">id,a</td>
+ <td></td>
+ </tr>
+ <tr>
+ <td class="name">wasInfluencedBy(id;e2,e1,attrs)</td>
+ <td class="name">id</td>
+ <td></td>
+ </tr>
+</table>
<div class="definition" id="optional-placeholders">
<ol><li>
-Suppose <span class="name">r</span> is in {<span class="name">entity</span>, <span class="name">activity</span> or <span class="name">agent</span>}. Then <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>.
+For each <span class="name">r</span> in {<span
+ class="name">entity</span>, <span class="name">activity</span>,
+ <span class="name">agent</span>}, the following definition
+ holds:
+ </p>
+ <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>
- <li> Similarly, suppose <span class="name">r</span> is in {
+ <li>For each <span class="name">r</span> in {
<span class="name">used</span>,
<span class="name">wasGeneratedBy</span>,
<span class="name">wasInfluencedBy</span>,
+<span class="name">wasInvalidatedBy</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>}. Then <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>. This definition
- applies to any relation containing a placeholder <span
- class="name">-</span>, <b>except</b> for a placeholder in the <span class="name">plan</span>
- position (i.e., the fourth argument) of <span
- class="name">wasAssociatedWith</span> or the <span class="name">activity</span>
- position (i.e., the fourth argument) of <span class="name">wasDerivedFrom</span>.
+<span class="name">actedOnBehalfOf</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> then the following definition holds:</p>
+ <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>
</div>
@@ -989,7 +1083,7 @@
<div class='inference' id='inference-communication-generation-use'>
<p>
-IF
+<span class="conditional">IF</span>
<span class="name">wasInformedBy(_id;a2,a1,_attrs)</span>
holds <span class='conditional'>THEN</span>
there exist <span class="name">e</span>, <span
@@ -999,13 +1093,15 @@
</div>
<div class="note">
-The following inference is "at risk" and may be dropped if it leads to
+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 class='inference' id='inference-generation-use-communication'>
<p>
-IF <span class="name">wasGeneratedBy(_id1;e,a1,_t1,_attrs1)</span>
+<span class="conditional">IF</span> <span class="name">wasGeneratedBy(_id1;e,a1,_t1,_attrs1)</span>
and <span class="name">used(_id2;a2,e,_t2,_attrs2)</span> hold
<span class='conditional'>THEN</span>
there exists <span
@@ -1045,7 +1141,7 @@
<a class="rule-text" href="#inference-entity-generation-invalidation"><span>TBD</span></a> and <a class="rule-text" href="#inference-activity-start-end"><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 interact with type inference to produce
+ The following two inferences could interact with type inference to produce
nontermination. For example, once we have an activity we can yse
inference-activity-start-end and start-type-inference forever to
infer an infinite chain of activities, each starting the next.
@@ -1055,11 +1151,19 @@
entities generated by activities that were started by entities that
were generated by activities ...
- We MUST break this recursion somewhere in order to ensure
+ We must break this recursion somewhere in order to ensure
implementability. I propose to drop both of the following
- inferences, since they are more questionable than the type inferences.
+ 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
generation and invalidation events.
@@ -1077,6 +1181,12 @@
<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="activity-start-end-inference_text">
From an activity statement we can infer that there must have existed
start and end events having times matching the start and end times of
@@ -1140,12 +1250,12 @@
<hr>
<p id='derivation-generation-use_text'>Derivations with explicit
activity, generation, and usage admit the following inference: </p>
-<div class="note">James: This can be concisely stated as one rule that
- concludes both generation and use in one step.
- </div>
+
<div class='inference' id='derivation-generation-use'>
<p>
-<ol>
+<!--
+
+ <ol>
<li><span class='conditional'>IF</span> <span
class="name">wasDerivedFrom(_id;e2,e1,a,id2,_id1,_attrs)</span>,
<span class='conditional'>THEN</span> there exists <span
@@ -1157,14 +1267,26 @@
class="name">_t1</span>
such that <span class="name">used(id1;a,e1,_t1,[])</span>.
</ol>
+-->
+<p>
+<span class='conditional'>IF</span> <span
+ class="name">wasDerivedFrom(_id;e2,e1,a,id2,id1,_attrs)</span>,
+ <span class='conditional'>THEN</span> there exists <span
+ class="name">_t1</span> and <span
+ class="name">_t2</span> such that <span
+class="name">used(id1;a,e1,_t1,[])</span> and <span
+class="name">wasGeneratedBy(id2;e2,a,_t2,[])</span> hold.
+</p>
</div>
<p>
<hr>
<p id='derivation-use_text'>Derivations with an explicit activity and
no specified generation and usage admit the following inference: </p>
-<div class="note">James: This inference seems to be redundant,
- I propose to delete it.
+<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
+ appears redundant (it can be derived using other rules).
</div>
<div class='inference' id='derivation-use'>
<p>
@@ -1213,9 +1335,7 @@
<hr />
<p id="revision-is-alternate_text">A revision admits the following inference, stating that the two entities
linked by a revision are also alternates.</p>
-<div class="note">Note that part 2 is redundant if we believe
- inference-specific-derivation</div>
-
+
<div class='inference' id='revision-is-alternate'>
<p>
<span class='conditional'>IF</span> <span
@@ -1312,17 +1432,15 @@
</p>
</div>
-<div class="note">Make it clear somewhere that the existential
- variables _pl1 and _pl2 can be replaced with either a concrete plan
- identifier or <span class="name">-</span> placeholder, thus, there is no need for a
- disjunction in the head of the rule to cover both cases.
- </div>
+
<div class="remark">
Note that the two associations between the agents and the activity
may have different identifiers, different plans, and different
attributes. In particular, the plans of the two agents need not be
the same, and one, both, or neither can be the placeholder <span class="name">-</span>
- indicating that there is no plan.
+ indicating that there is no plan, because the existential variables
+ <span class="name">_pl1</span> and <span class="name">_pl2</span> can be replaced with constant identifiers or
+ placeholders <span class="name">-</span> independently.
</div>
<hr />
@@ -1754,15 +1872,15 @@
A typical uniqueness constraint is as follows:
</p>
<div class="constraint-example" id="uniqueness-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> THEN <span class="name">t<sub>1</sub></span> = <span class="name">u<sub>1</sub></span> AND ... AND <span class="name">t<sub>n</sub></span> = <span class="name">u<sub>n</sub></span>.</p>
+<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="name">t<sub>1</sub></span> = <span class="name">u<sub>1</sub></span> and ... and <span class="name">t<sub>n</sub></span> = <span class="name">u<sub>n</sub></span>.</p>
</div>
<p> Such a constraint is enforced as follows:</p>
<ol> <li>Suppose PROV instance <span class="math">I</span> contains all of the hypotheses
- <span class="name">hyp<sub>1</sub></span> AND ... AND <span class="name">hyp<sub>n</sub></span>.
+ <span class="name">hyp<sub>1</sub></span> and ... and <span class="name">hyp<sub>n</sub></span>.
</li>
<li>Attempt to merge all of the equated terms in the conclusion
- <span class="name">t<sub>1</sub></span> = <span class="name">u<sub>1</sub></span> AND ... AND <span class="name">t<sub>n</sub></span> = <span class="name">u<sub>n</sub></span>.
+ <span class="name">t<sub>1</sub></span> = <span class="name">u<sub>1</sub></span> and ... and <span class="name">t<sub>n</sub></span> = <span class="name">u<sub>n</sub></span>.
</li>
<li>If merging fails, then the constraint
is unsatisfiable, so application of the constraint to <span class="math">I</span>
@@ -1779,7 +1897,7 @@
<div
class="constraint-example" id="key-example">
<p>The <span
- class="name">a<sub>k</sub></span> field is a KEY for relation <span
+ class="name">a<sub>k</sub></span> field is a <span class="conditional">KEY</span> for relation <span
class="name">r(a<sub>0</sub>;a<sub>1</sub>,...,a<sub>n</sub>)</span>. </p></div>
<p> Because of the presence of attributes, key constraints do not
@@ -1787,18 +1905,18 @@
constraints as follows. </p>
<ol>
<li> Suppose <span
- class="name">r(a<sub>0</sub>;a<sub>1</sub>,...a<sub>n</sub>,attrs1)</span> AND <span
+ class="name">r(a<sub>0</sub>;a<sub>1</sub>,...a<sub>n</sub>,attrs1)</span> and <span
class="name">r(b<sub>0</sub>;b<sub>1</sub>,...b<sub>n</sub>,attrs2)</span> hold in PROV instance <span class="math">I</span>, where the key fields <span
class="name">a<sub>k</sub> = b<sub>k</sub></span> are equal.</li>
<li> Attempt to merge all of the corresponding parameters <span
- class="name">a<sub>0</sub> = b<sub>0</sub> </span> AND ... AND <span
+ class="name">a<sub>0</sub> = b<sub>0</sub> </span> and ... and <span
class="name">a<sub>n</sub> = b<sub>n</sub></span>.
</li>
<li>If merging fails, then the constraint is unsatisfiable, so
application of the key constraint to <span class="math">I</span> fails.
</li>
<li>If merging succeeds with substitution <span class="math">S</span>, then we remove <span
- class="name">r(a<sub>0</sub>;a<sub>1</sub>,...a<sub>n</sub>,attrs1)</span> AND <span
+ class="name">r(a<sub>0</sub>;a<sub>1</sub>,...a<sub>n</sub>,attrs1)</span> and <span
class="name">r(b<sub>0</sub>;b<sub>1</sub>,...b<sub>n</sub>,attrs2)</span> from <span class="math">I</span>, obtaining
instance <span class="math">I'</span>, and return instance <span
class="name">{r(S(a<sub>0</sub>);S(a<sub>1</sub>),...S(a<sub>n</sub>),attrs1 ∪
@@ -1829,13 +1947,13 @@
</p>
<div class='constraint' id='key-object'>
<p><ol>
- <li>The identifier field <span class="name">e</span> is a KEY for
+ <li>The identifier field <span class="name">e</span> is a <span class="conditional">KEY</span> for
the <span class="name">entity(e,attrs)</span> statement.
</li>
- <li>The identifier field <span class="name">a</span> is a KEY for
+ <li>The identifier field <span class="name">a</span> is a <span class="conditional">KEY</span> 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
+<li>The identifier field <span class="name">ag</span> is a <span class="conditional">KEY</span> for
the <span class="name">agent(ag,attrs)</span> statement.
</li>
</ol>
@@ -1843,49 +1961,49 @@
</div>
<hr />
- <p id='key_relation_text'> Likewise, we assume that the identifiers
+ <p id='key-properties_text'> Likewise, we assume that the identifiers
of relationships in PROV uniquely identify the corresponding statements a PROV instance, through
the following key constraints:
</p>
- <div class='constraint' id='key-relation'>
+ <div class='constraint' id='key-properties'>
<p><ol>
- <li>The identifier field <span class="name">id</span> is a KEY for
+ <li>The identifier field <span class="name">id</span> is a <span class="conditional">KEY</span> for
the <span class="name">wasGeneratedBy(id;e,a,t,attrs)</span> statement.
</li>
- <li>The identifier field <span class="name">id</span> is a KEY for
+ <li>The identifier field <span class="name">id</span> is a <span class="conditional">KEY</span> for
the <span class="name">used(id;a,e,t,attrs)</span> statement.
</li>
- <li>The identifier field <span class="name">id</span> is a KEY for
+ <li>The identifier field <span class="name">id</span> is a <span class="conditional">KEY</span> for
the <span class="name">wasInformedBy(id;a2,a1,attrs)</span> statement.
</li>
- <li>The identifier field <span class="name">id</span> is a KEY for
+ <li>The identifier field <span class="name">id</span> is a <span class="conditional">KEY</span> for
the <span class="name">wasStartedBy(id;a2,e,a1,t,attrs)</span> statement.
</li>
- <li>The identifier field <span class="name">id</span> is a KEY for
+ <li>The identifier field <span class="name">id</span> is a <span class="conditional">KEY</span> for
the <span class="name">wasEndedBy(id;a2,e,a1,t,attrs)</span> statement.
</li>
- <li>The identifier field <span class="name">id</span> is a KEY for
+ <li>The identifier field <span class="name">id</span> is a <span class="conditional">KEY</span> for
the <span class="name">wasInvalidatedBy(id;e,a,t,attrs)</span> statement.
</li>
- <li>The identifier field <span class="name">id</span> is a KEY for
+ <li>The identifier field <span class="name">id</span> is a <span class="conditional">KEY</span> for
the <span class="name">wasDerivedFrom(id; e2, e1, attrs)</span> statement.
</li>
- <li>The identifier field <span class="name">id</span> is a KEY for
+ <li>The identifier field <span class="name">id</span> is a <span class="conditional">KEY</span> for
the <span class="name">wasDerivedFrom(id; e2, e1, a, g2, u1, attrs)</span> statement.
</li>
- <li>The identifier field <span class="name">id</span> is a KEY for
+ <li>The identifier field <span class="name">id</span> is a <span class="conditional">KEY</span> for
the <span class="name">wasAttributedTo(id;e,ag,attr)</span> statement.
</li>
- <li>The identifier field <span class="name">id</span> is a KEY for
+ <li>The identifier field <span class="name">id</span> is a <span class="conditional">KEY</span> for
the <span class="name">wasAssociatedWith(id;a,ag,pl,attrs)</span> statement.
</li>
- <li>The identifier field <span class="name">id</span> is a KEY for
+ <li>The identifier field <span class="name">id</span> is a <span class="conditional">KEY</span> for
the <span class="name">wasAssociatedWith(id;a,ag,-,attrs)</span> statement.
</li>
- <li>The identifier field <span class="name">id</span> is a KEY for
+ <li>The identifier field <span class="name">id</span> is a <span class="conditional">KEY</span> for
the <span class="name">actedOnBehalfOf(id;ag2,ag1,a,attrs)</span> statement.
</li>
- <li>The identifier field <span class="name">id</span> is a KEY for
+ <li>The identifier field <span class="name">id</span> is a <span class="conditional">KEY</span> for
the <span class="name">wasInfluencedBy(id;o2,o1,attrs)</span> statement.
</li>
</ol>
@@ -2071,9 +2189,9 @@
<div
class="constraint-example" id="ordering-example">
- <p>IF <span
- class="name">hyp<sub>1</sub></span> AND ... AND <span
- class="name">hyp<sub>n</sub></span> THEN <span
+ <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="name">evt1</span> <a>precedes</a>/<a title="precedes">strictly precedes</a> <span
class="name">evt2</span>. </p></div>
<p>
@@ -2206,7 +2324,7 @@
<li>
<span class="conditional">IF</span>
<span class="name">wasGeneratedBy(gen;_e,a,_t,_attrs)</span>
-AND
+and
<span class="name">wasStartedBy(start;a,_e1,_a1,_t1,_attrs1)</span>
<span class="conditional">THEN</span>
<span class="name">start</span>
@@ -2216,7 +2334,7 @@
<li>
<span class="conditional">IF</span>
<span class="name">wasGeneratedBy(gen;_e,a,_t,_attrs)</span>
-AND
+and
<span class="name">wasEndedBy(end;a,_e1,_a1,_t1,_attrs1)</span>
<span class="conditional">THEN</span>
<span class="name">gen</span>
@@ -2229,9 +2347,6 @@
<p>
<hr />
-<div class="note">These constraints appear superfluous because we
- define wasInformedBY in terms of other statements, which together
- imply this ordering. TODO: Can we drop this constraint?</div>
<p id='wasInformedBy-ordering_text'>
Communication between two activities <span class="name">a1</span>
and <span class="name">a2</span> also implies ordering
@@ -2506,16 +2621,24 @@
</p>
<div class="constraint" id="specialization-generation">
<p>
-<span class="conditional">IF</span> <span class="name">specializationOf(e2,e1)</span> and <span class="name">wasGeneratedBy(gen1;e1,_a1,_t1,_attrs1)</span> and <span class="name">wasGeneratedBy(gen2;e2,_a2,_t2,_attrs2)</span> THEN <span class="name">gen1</span> <a>precedes</a> <span class="name">gen2</span>.
+<span class="conditional">IF</span> <span
+ class="name">specializationOf(e2,e1)</span> and <span
+ class="name">wasGeneratedBy(gen1;e1,_a1,_t1,_attrs1)</span> and
+ <span class="name">wasGeneratedBy(gen2;e2,_a2,_t2,_attrs2)</span>
+ <span class="conditional">THEN</span> <span class="name">gen1</span> <a>precedes</a> <span class="name">gen2</span>.
<p/p>
</div>
<hr />
-<p id="specialization-generation_text">
+<p id="specialization-invalidation_text">
Similarly, if an entity specalizes another, then its invalidation must follow the
specialized entity's invalidation.
</p><div class="constraint" id="specialization-invalidation">
<p>
-IF <span class="name">specializationOf(e2,e1)</span> and <span class="name">wasInvalidatedBy(inv1;e1,_a1,_t1,_attrs1)</span> and <span class="name">wasInvalidatedBy(inv2;e2,_a2,_t2,_attrs2)</span> THEN <span class="name">inv2</span> <a>precedes</a> <span class="name">inv1</span>.
+<span class="conditional">IF</span> <span
+ class="name">specializationOf(e2,e1)</span> and <span
+ class="name">wasInvalidatedBy(inv1;e1,_a1,_t1,_attrs1)</span> and
+ <span class="name">wasInvalidatedBy(inv2;e2,_a2,_t2,_attrs2)</span>
+ <span class="conditional">THEN</span> <span class="name">inv2</span> <a>precedes</a> <span class="name">inv1</span>.
</p>
</div>
@@ -2657,17 +2780,31 @@
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">Perhaps this should be a constraint.</div>
+
+
+ <hr />
+
+<p id="impossible-influence-reflexive_text">Influence is required to
+ be <a>irreflexive</a>, that is, it is impossible for something to
+ influence itself.</p>
+
+ <div class='constraint' id="impossible-influence-reflexive">
+ <p> <span class="conditional">IF</span> <span class="name">wasInfluencedBy(e,e)</span> <span class="conditional">THEN</span> <span class="conditional">INVALID</span>.</p>
+ </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>
+<!--<p>
For any entity <span class='name'>e</span>, it is not the case that
-<span class='name'>specializationOf(e,e)</span> holds.</p>
+<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>
@@ -2693,39 +2830,63 @@
<hr />
-<div class="note">
-James: I don't understand what this is trying to say, it seems to say the
- same as key-relation except for the absence of wasInfluencedBy
- (which is stated above.)
-
- If the intent is that "each id is mentioned in at most one relation
- in the following list, plus possibly wasInfluencedBY" then
- this should be formulated as explicit disjointness constraint(s);
- this does not fit the pattern of the key constraints above.
-
- TODO: Reformulate these as disjointness constraints.
- </div>
- <p id='key_relation2_text'> Furthermore, identifiers
- of relationships in PROV uniquely identify a relation (except for wasInfluencedBy), through
- the following key constraint:
+
+ <p id='impossible-property-overlap_text'> Furthermore, identifiers
+ of basic relationships are disjoint.
</p>
- <div class='constraint' id='key-relation2'>
- <p>The <span
- class="name">id</span> field is a KEY for statements of the form <span
- class="name">r(id;a<sub>1</sub>,...,a<sub>n</sub>)</span>
-where <span class="name">r</span> is in {
+ <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">wasInfluencedBy</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>}
-</p> </div>
-
-
+<span class="name">actedOnBehalfOf</span>} such that <span class="name">r</span> and <span class="name">s</span>
+ are different relations, 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">
+ 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.
+ </div>
+
+ <p id='impossible-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">r</span> in <span class="name">entity</span>, <span class="name">activity</span>
+ or <span class="name">agent</span> and for each <span class="name">s</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">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>
+
+
<hr />
<p id='entity-activity-disjoint_text'> Furthermore, the set of entities and activities are disjoint, expressed by
the following constraint: