--- a/model/prov-constraints.html Thu Jul 19 16:28:01 2012 +0100
+++ b/model/prov-constraints.html Thu Jul 19 16:28:14 2012 +0100
@@ -405,7 +405,7 @@
that applications MAY employ, including <em>definitions</em> of some
provenance statements in terms of others, and also defines a class of
<em>valid</em> PROV instances by specifying <em>constraints</em> that
-xsvalid PROV instances must satisfy. Applications SHOULD produce valid
+valid PROV instances must satisfy. Applications SHOULD produce valid
provenance and MAY reject provenance that is not valid. Applications
SHOULD also use definitions, inferences and constraints to normalize
PROV instances in order to determine whether two such instances convey
@@ -441,12 +441,14 @@
new facts representing implicit knowledge about the structure of
provenance. </p>
-<p><a href="#constraints">Section 5</a> presents two kinds of constraints,
+<p><a href="#constraints">Section 5</a> presents three kinds of constraints,
<em>uniqueness</em> constraints that prescribe that certain statments
-must be unique within PROV <a>instances</a>, and
+must be unique within PROV <a>instances</a>,
<em>event ordering</em> constraints that require that the records in a
PROV <a>instance</a> are consistent with a sensible ordering of events
-relating the activities, entities and agents involved.
+relating the activities, entities and agents involved, and
+<em>impossibility</em> constraints that forbid certain patterns of
+statements in valid PROV instances.
</p>
<p><a href="#equivalence">Section 6</a> defines the notions
@@ -557,7 +559,7 @@
<p>An activity is not an entity. Indeed, an entity exists in full at
any point in its lifetime, persists during this interval, and
-preserves the characteristics that makes it identifiable. In
+preserves the characteristics that make it identifiable. In
contrast, an activity is something that occurs, happens, unfolds, or
develops through time, but is typically not identifiable by the
characteristics it exhibits at any point during its duration. This
@@ -628,7 +630,8 @@
constraints of this document.
</p>
-<div class="note">Table: work in progress; do after constraints are done.</div>
+<div class="note">Table: work in progress; do when rest is
+ stable. Also, standardize constraint names.</div>
<div id="prov-constraints-fig" style="text-align: left;">
<table class="thinborder" style="margin-left: auto; margin-right: auto;">
@@ -731,11 +734,10 @@
<section id="inferences">
<h2>Inferences and Definitions</h2>
-<div class='note'> Add definitions/rules for expanding optionals</div>
<p>
In this section, we describe <a title="inference">inferences</a> and <a title="definition">definitions</a> that MAY be used on
provenance data, and preserve <a>equivalence</a> on <a>valid</a>
-PROV instances (as detailed in <a href="#equivalence" class="sectionRef"></a>).
+PROV instances (as detailed in <a href="#normalization-validity-equivalence" class="sectionRef"></a>).
An <dfn id="inference">inference</dfn> is a rule that can be applied
to PROV instances to add new PROV statements. A <dfn
id="definition">definition</dfn> is a rule that states that a
@@ -747,20 +749,20 @@
<p> Inferences have the following general form:</p>
<div class='inference-example' id='inference-example'>
<p>
- <span class='conditional'>IF</span> <span class="name">hyp_1</span> and ... and
-<span class="name">hyp_k</span> <span class='conditional'>THEN</span>
- there exists <span class="name">a_1</span> and ... and <span
- class="name">a_m</span> such that <span
- class="name">conclusion_1</span> and ... and <span class="name">conclusion_n</span>.</p>
+ <span class='conditional'>IF</span> <span class="name">hyp<sub>1</sub></span> and ... and
+<span class="name">hyp<sub>k</sub></span> <span class='conditional'>THEN</span>
+ there exists <span class="name">a<sub>1</sub></span> and ... and <span
+ class="name">a<sub>m</sub></span> such that <span
+ class="name">conclusion<sub>1</sub></span> and ... and <span class="name">conclusion<sub>n</sub></span>.</p>
</div>
<p> This means that if all of the provenance statements matching
- <span class="name">hyp_1</span>... <span class="name">hyp_k</span>
+ <span class="name">hyp<sub>1</sub></span>... <span class="name">hyp<sub>k</sub></span>
can be found in a PROV instance, we can add all of the statements
- <span class="name">concl_1</span> ... <span
- class="name">concl_n</span> to the instance, possibly after
- generating fresh identifiers <span class="name">a_1</span>,...,<span
- class="name">a_m</span> for unknown objects. These fresh
+ <span class="name">concl<sub>1</sub></span> ... <span
+ class="name">concl<sub>n</sub></span> to the instance, possibly after
+ generating fresh identifiers <span class="name">a<sub>1</sub></span>,...,<span
+ 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
@@ -773,10 +775,11 @@
<div class='definition-example' id='definition-example'>
<p>
- <span class="name">defined_exp</span> holds <span class='conditional'>IF AND ONLY IF </span>
- there exists <span class="name">a_1</span>,..., <span
- class="name">a_m</span> such that <span
- class="name">defining_exp_1</span> and ... and <span class="name">defining_exp_n</span>.</p>
+ <span class="name">defined_exp</span> holds <span
+ class='conditional'>IF AND ONLY IF</span>
+ there exists <span class="name">a<sub>1</sub></span>,..., <span
+ class="name">a<sub>m</sub></span> such that <span
+ class="name">defining_exp<sub>1</sub></span> and ... and <span class="name">defining_exp<sub>n</sub></span>.</p>
</div>
<p>
@@ -784,9 +787,9 @@
terms of other statements. This can be viewed as a two-way
inference: If <span class="name">defined_exp</span>
can be found in a PROV instance, we can add all of the statements
-<span class="name">defining_exp_1</span> ... <span class="name">defining_exp_n</span> to the instance, possibly after generating fresh
- identifiers <span class="name">a_1</span>,...,<span
- class="name">a_m</span> for unknown objects. It is safe to replace
+<span class="name">defining_exp<sub>1</sub></span> ... <span class="name">defining_exp<sub>n</sub></span> to the instance, possibly after generating fresh
+ identifiers <span class="name">a<sub>1</sub></span>,...,<span
+ class="name">a<sub>m</sub></span> for unknown objects. It is safe to replace
a defined statement with
its definition.
</p>
@@ -794,7 +797,7 @@
<p> Definitions and inferences can be viewed as logical formulas;
similar formalisms are often used in rule-based reasoning [[CHR]]
and in databases [[DBCONSTRAINTS]]. In particular, the identifiers
- <span class="name">a_1</span> ... <span class="name">a_n</span>
+ <span class="name">a<sub>1</sub></span> ... <span class="name">a<sub>n</sub></span>
should be viewed as existentially quantified variables, meaning that
through subsequent reasoning steps they may turn out to be equal to
other identifiers that are already known, or to other existentially
@@ -817,9 +820,24 @@
</p>
<div class="definition" id="optional-identifiers">
- <p>
- <span class="name">r(a_1,...,a_n) </span> holds <span class="conditional">IF AND ONLY IF</span>
- there exists <span class="name">id</span> such that <span class="name">r(id;a_1,...,a_n)</span> holds.</p>
+<p> Suppose <span class="name">r</span> is in {
+<span class="name">used</span>,
+<span class="name">wasGeneratedBy</span>,
+<span class="name">wasInfluencedBy</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>
+ <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
+ class="name">r(id;a<sub>1</sub>,...,a<sub>n</sub>)</span> holds.</li>
+ <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
+ class="name">r(id;a<sub>1</sub>,...,a<sub>n</sub>)</span> holds.</li>
+ </ol>
</div>
<p>Likewise, many PROV statements allow for an optional attribute
@@ -828,13 +846,23 @@
<div class="definition" id="optional-attributes">
<ol>
<li>
- <span class="name">r(a_1,...,a_n)</span> holds and does not contain an explicit attribute
+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
- class="name">r(a_1,...,a_n,[])</span> holds.</li>
+ class="name">r(a<sub>1</sub>,...,a<sub>n</sub>,[])</span> holds.</li>
<li>
- Similarly, <span class="name">r(id;a_1,...,a_n)</span> holds and does not contain an explicit attribute
+ Similarly, suppose <span class="name">r</span> is in {
+<span class="name">used</span>,
+<span class="name">wasGeneratedBy</span>,
+<span class="name">wasInfluencedBy</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>}.
+ 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
- class="name">r(id;a_1,...,a_n,[])</span> holds.</li></ol>
+ class="name">r(id;a<sub>1</sub>,...,a<sub>n</sub>,[])</span> holds.</li></ol>
</div>
<p> Finally, many PROV
@@ -872,7 +900,7 @@
<div class="remark">
<p>
- Note that there is no expansion rule for wasDerivedFrom. In a derivation of the form
+ Note that there is no expansion rule for <span class="name">wasDerivedFrom</span>. In a derivation of the form
<span class="name">wasDerivedFrom(id;e1,e2,attr)</span>, the
absence of the optional activity, generation and use identifiers
means that the derivation relationship may encompass multiple activities,
@@ -899,7 +927,8 @@
by fresh existential variables, distinct from any others occurring in
the instance.
The only exceptions, where <span class="name">-</span> MUST be left
- in place, is the plan parameter in <span class="name">wasAssociatedWith</span>.
+ in place, are the <span class="name">activity</span> parameter in <span class="name">wasDerivedFrom</span> and
+ the <span class="name">plan</span> parameter in <span class="name">wasAssociatedWith</span>.
</p>
<div class="note">
@@ -909,14 +938,28 @@
rules, since the expansion is completely uniform except for the
plan parameter.</div>
- <div class="definition" id="optional-variables">
-
- <p> <span class="name">r(a_0;...,a_{i-1}, -, a_i, ...,a_n) </span> <span class="conditional">IF AND ONLY IF</span> there exists <span class="name">a'</span>
- such that <span class="name">r(a_0;...,a_{i-1},a',a_i,...,a_n)</span>. This definiton
+ <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>.
+ </li>
+ <li> Similarly, suppose <span class="name">r</span> is in {
+<span class="name">used</span>,
+<span class="name">wasGeneratedBy</span>,
+<span class="name">wasInfluencedBy</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>}. 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>.
- </p>
+ 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>.
+ </li></ol>
</div>
<div class="remark">In an association of the form
@@ -924,7 +967,12 @@
absence of a plan means: either no plan exists, or a plan exists but
it is not identified. Thus, it is not equivalent to <span
class="name">wasAssociatedWith(id;a,ag,p,attr)</span> where a
- plan <span class="name">p</span> is given.
+ plan <span class="name">p</span> is given. Similarly, a <span
+ class="name">wasDerivedFrom(id;e2,e1,a,gen,use,attrs)</span> that
+ specifies an activity explicitly is not
+ equivalent to <span
+ class="name">wasDerivedFrom(id;e2,e1,-,gen,use,attrs)</span> with a
+ missing activity.
</div>
</section>
@@ -938,31 +986,40 @@
title="definition">defined</a> as the existence of an underlying
entity generated by one activity and used by the other.</p>
- <div class="note">Where do the attributes of the wasInformedBy
- relation go? The definition is essentially saying they don't
- matter. If this is what we mean, then the id and attributes are
- irrelevant to the meaning/validity.</div>
-
-<div class='definition' id='wasInformedBy-definition'>
+<div class='inference' id='inference-communication-generation-use'>
<p>
-Given two activities identified by <span class="name">a1</span> and <span class="name">a2</span>,
+IF
<span class="name">wasInformedBy(_id;a2,a1,_attrs)</span>
-holds <span class='conditional'>IF AND ONLY IF</span>
- there exists <span class="name">e</span>, <span class="name">_id1</span>, <span class="name">_t1</span>, <span class="name">_attrs1</span>, <span class="name">_id2</span>, <span class="name">_t2</span>, <span class="name">_attrs2</span>,
-such that <span class="name">wasGeneratedBy(_id1;e,a1,_t1,_attrs1)</span> and <span class="name">used(_id2;a2,e,_t2,_attrs2)</span> hold.</p>
+holds <span class='conditional'>THEN</span>
+ there exist <span class="name">e</span>, <span
+ class="name">_id1</span>, <span class="name">_t1</span>, <span
+ class="name">_id2</span>, and <span class="name">_t2</span>,
+such that <span class="name">wasGeneratedBy(_id1;e,a1,_t1,[])</span> and <span class="name">used(_id2;a2,e,_t2,[])</span> hold.</p>
</div>
-<div class="note"> We don't give counterexamples to most other
- non-inferences. Suggest dropping this counterexample, as it is purely
- illustrative, not normative.</div>
-
+<div class="note">
+The following inference is "at risk" 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>
+ and <span class="name">used(_id2;a2,e,_t2,_attrs2)</span> hold
+ <span class='conditional'>THEN</span>
+ there exists <span
+ class="name">_id</span>
+such that <span class="name">wasInformedBy(_id;a2,a1,[])</span>
+</p></div>
+
+
+ <div class="remark">
<p>The relationship <span class="name">wasInformedBy</span> is not
<a>transitive</a>. Indeed, consider the following statements.</p>
<pre class="codeexample">
wasInformedBy(a2,a1)
wasInformedBy(a3,a2)
</pre>
- <div class="remark">
<p> We cannot infer <span class="name">wasInformedBy(a3,a1)</span> from these statements. Indeed,
from
<span class="name">wasInformedBy(a2,a1)</span>, we know that there exists <span class="name">e1</span> such that <span class="name">e1</span> was generated by <span class="name">a1</span>
@@ -986,6 +1043,21 @@
<div class="note">Luc: The narrative is not right for both
<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
+ 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.
+ Similarly, we can use inverence-activity-start-end,
+start-type-inference, inference-entity-generation-invalidation,
+ and generation-type-inference forever to infer an infinite chain of
+ entities generated by activities that were started by entities that
+ were generated by activities ...
+
+ 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.
+ </div>
<hr />
<p id="entity-generation-invalidation-inference_text">
From an entity, we can infer that the existence of
@@ -996,10 +1068,10 @@
<span class='conditional'>IF</span> <span
class="name">entity(e,_attrs)</span> <span
class="conditional">THEN</span> there exist
-<span class="name">_id1</span>, <span class="name">_a1</span>, <span class="name">_t1</span>, <span class="name">_attrs1</span>,
-<span class="name">_id2</span>, <span class="name">_a2</span>, <span class="name">_t2</span>, and <span class="name">_attrs2</span> such that
+<span class="name">_id1</span>, <span class="name">_a1</span>, <span class="name">_t1</span>,
+<span class="name">_id2</span>, <span class="name">_a2</span>, and <span class="name">_t2</span> such that
<span
- class="name">wasGeneratedBy(_id1;e,_a1,_t1,_attrs1)</span> and <span class="name">wasInvalidatedBy(_id2;e,_a2,_t2,_attrs2)</span>.
+ class="name">wasGeneratedBy(_id1;e,_a1,_t1,[])</span> and <span class="name">wasInvalidatedBy(_id2;e,_a2,_t2,[])</span>.
</div>
@@ -1013,10 +1085,10 @@
<p>
<span class='conditional'>IF</span> <span
class="name">activity(a,t1,t2,_attrs)</span> <span
- class="conditional">THEN</span> there exist <span class="name">_id1</span>, <span class="name">_e1</span>,
- <span class="name">_attrs1</span>, <span class="name">_id2</span>, <span class="name">_e2</span>, and <span class="name">_attrs2</span> such that
+ class="conditional">THEN</span> there exist <span class="name">_id1</span>, <span class="name">_e1</span>, <span class="name">_id2</span>,
+ and <span class="name">_e2</span> such that
<span
- class="name">wasStartedBy(_id1;a,_e1,t1,_attrs1)</span> and <span class="name">wasEndedBy(_id2;a,_e2,t2,_attrs2)</span>.
+ class="name">wasStartedBy(_id1;a,_e1,_a1,t1,[])</span> and <span class="name">wasEndedBy(_id2;a,_e2,_a2,t2,[])</span>.
</div>
@@ -1031,9 +1103,10 @@
<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='conditional'>THEN</span> there exist <span class="name">_gen</span>, <span class="name">_t1</span>,
- and <span class="name">_attrs1</span> such that
- <span class="name">wasGeneratedBy(_gen;e1,a1,_t1,_attrs1)</span>.</p>
+<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>
</div>
<p>
@@ -1049,9 +1122,9 @@
<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='conditional'>THEN</span> there exist <span class="name">_gen</span>, <span class="name">_t1</span>,
- and <span class="name">_attrs1</span> such that
- <span class="name">wasGeneratedBy(_gen;e1,a1,_t1,_attrs1)</span>.</p>
+<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>
</div>
@@ -1064,36 +1137,41 @@
<hr>
-<p id='derivation-generation-use_text'>Derivations with explicit activity, generation, and usage admit the following inference: </p>
+<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>
<li><span class='conditional'>IF</span> <span
class="name">wasDerivedFrom(_id;e2,e1,a,id2,_id1,_attrs)</span>,
- <span class='conditional'>THEN</span> there exist <span
- class="name">_t2</span> and <span class="name">_attrs2</span>
- such that <span class="name">wasGeneratedBy(id2;e2,a,_t2,_attrs2)</span>.
+ <span class='conditional'>THEN</span> there exists <span
+ class="name">_t2</span>
+ such that <span class="name">wasGeneratedBy(id2;e2,a,_t2,[])</span>.
<li><span class='conditional'>IF</span> <span
class="name">wasDerivedFrom(_id;e2,e1,a,_id2,id1,_attrs)</span>,
- <span class='conditional'>THEN</span> there exist <span
- class="name">_t1</span> and <span class="name">_attrs1</span>
- such that <span class="name">used(id1;a,e1,_t1,_attrs1)</span>.
+ <span class='conditional'>THEN</span> there exists <span
+ class="name">_t1</span>
+ such that <span class="name">used(id1;a,e1,_t1,[])</span>.
</ol>
</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>
<div class='inference' id='derivation-use'>
<p>
<span class='conditional'>IF</span> <span class="name">wasDerivedFrom(id;e2,e1,a,-,-,attrs)</span> and <span class="name">wasGeneratedBy(gen;e2,a,_t2,_attrs2)</span> hold, <span
-class='conditional'>THEN</span>:
-<ul>
-<li>
- there exist <span
- class="name">_t1</span> and <span class="name">_attrs1</span> such
- that <span class="name">used(use;a,e1,_t1,_attrs1)</span>;
-<li> furthermore, <span class="name">wasDerivedFrom(id;e2,e1,a,gen,use,attrs)</span>.
+class='conditional'>THEN</span> there exist <span
+ class="name">_t1</span> and <span class="name">use</span> such
+ that <span class="name">used(use;a,e1,_t1,[])</span> and <span
+ class="name">wasDerivedFrom(id;e2,e1,a,gen,use,attrs)</span> hold.
</div>
<p>This inference is justified by the fact that the entity denoted by <span class="name">e2</span> is generated by at most one activity
(see <a class="rule-text" href="#unique-generation"><span>TBD</span></a>). Hence, this activity is also the one referred to by the usage of <span class="name">e1</span>.
@@ -1117,20 +1195,41 @@
</div>
<hr />
-<p>A revision admits the following inference, stating that the two entities
+<p id="inference-specific-derivation_text">A derivation
+ specifying activity, generation and use events is a special case of
+ a derivation that leaves these unspecified. (The converse is not
+ the case).</p>
+
+<div class='inference' id='inference-specific-derivation'>
+<p><span class='conditional'>IF</span> <span
+ class="name">wasDerivedFrom(id;e2,e1,_act,_gen,_use,attrs)</span>
+ holds, <span class='conditional'>THEN</span> <span
+ class="name">wasDerivedFrom(id;e2,e1,attrs)</span> holds.
+</p>
+</div>
+
+
+<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'>
-<ol><li><span class='conditional'>IF</span> <span
+<p>
+ <span class='conditional'>IF</span> <span
class="name">wasDerivedFrom(_id;e2,e1,[prov:type='prov:Revision'])</span>
holds, <span class='conditional'>THEN</span> <span
class="name">alternateOf(e2,e1)</span> holds.
-</li>
+</p>
+<!--
<li><span class='conditional'>IF</span> <span
class="name">wasDerivedFrom(_id;e2,e1,_act,_gen,_use,[prov:type='prov:Revision'])</span>
holds, <span class='conditional'>THEN</span> <span
class="name">alternateOf(e2,e1)</span> holds.
-</li></ol>
+</li>
+-->
+</ol>
</div>
@@ -1184,18 +1283,12 @@
<span class='conditional'>THEN</span> there exist
<span class="name">a</span>,
<span class="name">_t</span>,
- <span class="name">_t1</span>,
- <span class="name">_t2</span>,
- <span class="name">_gen</span>,
+<span class="name">_gen</span>,
<span class="name">_assoc</span>,
<span class="name">_pl</span>,
- <span class="name">_attrs1</span>,
- <span class="name">_attrs2</span>,
- <span class="name">_attrs3</span>,
- such that
-<span class="name">activity(a,_t1,_t2,_attrs1)</span> and
-<span class="name">wasGeneratedBy(_gen;e,a,_t,_attrs2)</span> and
-<span class="name">wasAssociatedWith(_assoc;a,ag,_pl,_attrs3)</span> hold.
+such that
+<span class="name">wasGeneratedBy(_gen;e,a,_t,[])</span> and
+<span class="name">wasAssociatedWith(_assoc;a,ag,_pl,[])</span> hold.
</p>
</div>
<hr />
@@ -1212,11 +1305,9 @@
<span class="name">actedOnBehalfOf(_id;ag1, ag2, a, _attrs)</span>
<span class='conditional'>THEN</span> there exist <span
class="name">_id1</span>, <span class="name">_pl1</span>, <span
- class="name">_attrs1</span>, <span
- class="name">_id2</span>, <span class="name">_pl2</span>, and <span
- class="name">_attrs2</span> such that <span
- class="name">wasAssociatedWith(_id1;a, ag1, _pl1, _attrs1)</span>
- and <span class="name">wasAssociatedWith(_id2;a, ag2, _pl2, _attrs2)</span>.
+ class="name">_id2</span>, and <span class="name">_pl2</span> such that <span
+ class="name">wasAssociatedWith(_id1;a, ag1, _pl1, [])</span>
+ and <span class="name">wasAssociatedWith(_id2;a, ag2, _pl2, [])</span>.
</p>
</div>
@@ -1262,13 +1353,10 @@
<span class="conditional">IF</span> <span class="name">wasInvalidatedBy(id;e,a,t,attrs)</span> <span class="conditional">THEN</span> <span class="name">wasInfluencedBy(id; e, a, attrs)</span>.
</li>
<li>
- <span class="conditional">IF</span> <span class="name">wasDerivedFrom(id; e2, e1, a, g2, u1, attrs)</span> <span class="conditional">THEN</span> <span class="name">wasInfluencedBy(id; e2, e1, attrs)</span>.
+ <span class="conditional">IF</span> <span class="name">wasDerivedFrom(id; e2, e1, attrs)</span> <span class="conditional">THEN</span> <span class="name">wasInfluencedBy(id; e2, e1, attrs)</span>.
</li>
- <li>
- <span class="conditional">IF</span> <span class="name">wasDerivedFrom(id; e2, e1, -, -, -, attrs)</span> <span class="conditional">THEN</span> <span class="name">wasInfluencedBy(id; e2, e1, attrs)</span>.
- </li>
- <li>
+ <li>
<span class="conditional">IF</span> <span class="name">wasAttributedTo(id;e,ag,attr)</span> <span class="conditional">THEN</span> <span class="name">wasInfluencedBy(id; e, ag, attrs)</span>.
</li>
<li>
@@ -1319,40 +1407,14 @@
<p>
-<hr>
-
- <div class="note">Perhaps this should be a constraint.</div>
-<p id="specialization-irreflexive_text">Similarly, specialization is a
- <a>strict partial order</a>: it is <a>irreflexive</a> and
- <a>transitive</a>.</p>
-
- <div class='inference' id="specialization-irreflexive">
-<p>
- For any entity <span class='name'>e</span>, it is not the case that
-<span class='name'>specializationOf(e,e)</span> holds.</p>
- </div>
-
<hr>
-<div class="note"> This is also a constraint, but follows from
- irreflexivity and transitivity so we may omit it.</div>
-
- <p id="specialization-asymmetric_text"/>
-
-<div class='inference' id="specialization-asymmetric">
-<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>
-
-<p>
-<hr>
<p id="specialization-transitive_text"/>
-
+Similarly, specialization is a
+ <a>strict partial order</a>: it is <a>irreflexive</a> and
+ <a>transitive</a>. Irreflexivity is handled later as a
+ constraint.
+ </p>
<div class='inference' id="specialization-transitive">
<p>
<!-- For any entities <span class='name'>e1</span>, <span class='name'>e2</span>, <span class='name'>e3</span>, -->
@@ -1365,7 +1427,7 @@
<hr>
- <p id="specialization-alternate_text">Finally, if one entity specializes another, then they are also
+ <p id="specialization-alternate_text">If one entity specializes another, then they are also
alternates:</p>
<div class='inference' id="specialization-alternate">
@@ -1375,21 +1437,20 @@
</div>
<hr />
- <div class="note"> Explanation needed. Also, the following
- inference is too specific - it only handles the case of a single
- attribute, whereas in general we want the sub-entity to inherit all
- attributes of the super-entity.
- </div>
-
+<p id="specialization-attributes_text">
+ If one entity specializes another then all attributes of the more
+ general entity are also attributes of the more specific one.
+ </p>
<div class="inference" id="specialization-attributes">
<p>
<!-- For any entities <span class='name'>e1</span>, <span class='name'>e2</span>,-->
-<span class='conditional'>IF</span> <span class='name'>entity(e1, [a=x])</span> holds for some
- attribute <span class='name'>a</span> with value <span class='name'>x </span> and <span class='name'>specializationOf(e2,e1)</span> holds, <span class='conditional'>THEN </span>
- <span class='name'>entity(e2, [a=x])</span> also holds.</p>
+<span class='conditional'>IF</span> <span class='name'>entity(e1, attrs)</span> holds for some
+ attributes <span class='name'>attrs</span> and <span class='name'>specializationOf(e2,e1)</span> holds, <span class='conditional'>THEN </span>
+ <span class='name'>entity(e2, attrs)</span> also holds.</p>
</div>
+
<hr />
<div class="note">
@@ -1608,20 +1669,22 @@
<p>
This section defines a collection of constraints on PROV instances.
-There are two kinds of constraints:
+There are three kinds of constraints:
<ul><li><em>uniqueness constraints</em> that say that a <a>PROV
instance</a> can contain at most one statement of each kind with a
given identifier. For
example, if we describe the same generation event twice, then the
two statements should have the same times;
</li>
- <li> and <em>event ordering constraints</em> that say that it
+ <li> <em>event ordering constraints</em> that say that it
should be possible to arrange the
events (generation, usage, invalidation, start, end) described in a
PROV instance into a preorder that corresponds to a sensible
"history" (for example, an entity should not be generated after it
- is used).
+ is used); and
</li>
+ <li><em>impossibility constraints</em>, which forbid certain
+ patterns of statements in <a>valid</a> PROV instances.
</ul>
<section
@@ -1661,7 +1724,7 @@
(including the placeholder <span class="name">-</span>), then
their <a>merge</a> exists only if they are equal, otherwise merging
is undefined. </li>
- <li> If one <span class="name">x</span> is an existential variable
+ <li> If <span class="name">x</span> is an existential variable
and
<span class="name">t'</span> is any term (identifier, constant,
placeholder <span class="name">-</span>, or
@@ -1669,7 +1732,7 @@
<a>merge</a> is <span class="name">t'</span>, and the resulting substitution is
<span class="name">[x=t']</span>. In the special case where <span class="name">t'=x</span>, the merge is
<span class="name">x</span> and the resulting substitution is empty.</li>
- <li> If one <span class="name">t</span> is any term (identifier, constant,
+ <li> If <span class="name">t</span> is any term (identifier, constant,
placeholder <span class="name">-</span>, or
existential variable) and
<span class="name">x'</span> is an existential variable, then their
@@ -1690,21 +1753,21 @@
A typical uniqueness constraint is as follows:
</p>
<div class="constraint-example" id="uniqueness-example">
-<p> IF <span class="name">hyp_1</span> AND ... AND <span class="name">hyp_n</span> THEN <span class="name">t_1</span> = <span class="name">u_1</span> AND ... AND <span class="name">t_n</span> = <span class="name">u_n</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> 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>
</div>
<p> Such a constraint is enforced as follows:</p>
- <ol> <li>Suppose PROV instance I contains all of the hypotheses
- <span class="name">hyp_1</span> AND ... AND <span class="name">hyp_n</span>.
+ <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>.
</li>
<li>Attempt to merge all of the equated terms in the conclusion
- <span class="name">t_1</span> = <span class="name">u_1</span> AND ... AND <span class="name">t_n</span> = <span class="name">u_n</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 I
+ is unsatisfiable, so application of the constraint to <span class="math">I</span>
fails.</li>
- <li>If merging succeeds with a substitution S, then
- S is applied to the instance I, yielding result I(S).</li>
+ <li>If merging succeeds with a substitution <span class="math">S</span>, then
+ <span class="math">S</span> is applied to the instance <span class="math">I</span>, yielding result <span class="math">I(S)</span>.</li>
</ol>
<p> In the common case that a particular field of a relation uniquely
@@ -1715,30 +1778,30 @@
<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>
+ class="name">a<sub>k</sub></span> field is a KEY 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
reduce directly to uniqueness constraints. Instead, we enforce key
constraints as follows. </p>
<ol>
<li> Suppose <span
- class="name">r(a_0;a_1,...a_n,attrs1)</span> AND <span
- class="name">r(b_0;b_1,...b_n,attrs2)</span> hold in PROV instance I, where the key fields <span
- class="name">a_k = b_k</span> are equal.</li>
+ 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_0 = b_0 </span> AND ... AND <span
- class="name">a_n = b_n</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 I fails.
+ application of the key constraint to <span class="math">I</span> fails.
</li>
- <li>If merging succeeds with substitution S, then we remove <span
- class="name">r(a_0;a_1,...a_n,attrs1)</span> AND <span
- class="name">r(b_0;b_1,...b_n,attrs2)</span> from I, obtaining
- instance I', and return instance <span
- class="name">{r(S(a_0);S(a_1),...S(a_n),attrs1 ∪
- attrs2)}</span> ∪ S(I').
+ <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(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 ∪
+ attrs2)}</span> ∪ <span class="math">S(I')</span>.
</ol>
@@ -1827,35 +1890,6 @@
</ol>
</p> </div>
- <hr />
- <p id='key_relation2_text'> Furthermore, identifiers
- of relationships in PROV uniquely identify a relation (except for wasInfluencedBy), through
- the following key constraint:
- </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_1,...,a_n)</span>
-where r is in {
-<span class="name">used</span>,
-<span class="name">wasGeneratedBy</span>,
-<span class="name">wasInfluencedBy</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>
-
- <hr />
- <p id='entity-activity-disjoint_text'> Furthermore, the set of entities and activities are disjoint, expressed by
- the following constraint:
- </p>
- <div class='constraint' id='entity-activity-disjoint'>
- <p>It is not the case that <span class="name">entity(id,attrs1)</span> and
-<span class="name">activity(id,_t1,_t2,attrs2)</span>.
-</p> </div>
<hr>
@@ -2025,7 +2059,7 @@
(e.g. different time zones) leading to apparent inconsistencies. For
the purpose of checking ordering constraints, the times associated
with events are irrelevant; thus, there is no inference that time ordering
-implies event ordering. However, an application MAY flag time values
+implies event ordering, or vice versa. However, an application MAY flag time values
that appear inconsistent with the event ordering as possible
inconsistencies. When generating provenance, an application SHOULD
use a consistent timeline for related PROV statements within an
@@ -2037,8 +2071,8 @@
<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">hyp<sub>1</sub></span> AND ... AND <span
+ class="name">hyp<sub>n</sub></span> THEN <span
class="name">evt1</span> <a>precedes</a>/<a title="precedes">strictly precedes</a> <span
class="name">evt2</span>. </p></div>
<p>
@@ -2093,9 +2127,7 @@
(originally from Tim Lebo):
<ul>
<li>
- I think it would help if the "corresponding edges between entities and activities" where the same visual style as the vertical line marking the time the Usage, generation and derivation occurred. A matching visual style provides a Gestalt that matches the concept. I am looking at subfigures b and c in 5.2.0</li>
-<li>
-Is Invalidation missing in "The following figure summarizes the ordering constraints" paragraph?</li> </ul>
+ I think it would help if the "corresponding edges between entities and activities" where the same visual style as the vertical line marking the time the Usage, generation and derivation occurred. A matching visual style provides a Gestalt that matches the concept. I am looking at subfigures b and c in 5.2. </ul>
</div>
<div style="text-align: center;">
@@ -2144,7 +2176,7 @@
<span class="name">wasStartedBy(start;a,_e1,_a1,_t1,_attrs1)</span>
<span class="conditional">THEN</span>
<span class="name">start</span>
-<a title="precedes">strictly precedes</a>
+<a title="precedes">precedes</a>
<span class="name">use</span>.
</li>
<li>
@@ -2154,7 +2186,7 @@
<span class="name">wasEndedBy(end;a,_e1,_a1,_t1,_attrs1)</span>
<span class="conditional">THEN</span>
<span class="name">use</span>
-<a title="precedes">strictly precedes</a>
+<a title="precedes">precedes</a>
<span class="name">end</span>.
</li>
</ol>
@@ -2177,7 +2209,7 @@
<span class="name">wasStartedBy(start;a,_e1,_a1,_t1,_attrs1)</span>
<span class="conditional">THEN</span>
<span class="name">start</span>
-<a title="precedes">strictly precedes</a>
+<a title="precedes">precedes</a>
<span class="name">gen</span>.
</li>
<li>
@@ -2187,7 +2219,7 @@
<span class="name">wasEndedBy(end;a,_e1,_a1,_t1,_attrs1)</span>
<span class="conditional">THEN</span>
<span class="name">gen</span>
-<a title="precedes">strictly precedes</a>
+<a title="precedes">precedes</a>
<span class="name">end</span>.
</li>
</ol>
@@ -2316,7 +2348,7 @@
<span class="name">used(use;_a2,e,_t2,_attrs2)</span>
<span class="conditional">THEN</span>
<span class="name">gen</span>
-<a title="precedes">strictly precedes</a>
+<a title="precedes">precedes</a>
<span class="name">use</span>.
</p>
</div>
@@ -2334,7 +2366,7 @@
<span class="name">wasInvalidatedBy(inv;e,_a2,_t2,_attrs2)</span>
<span class="conditional">THEN</span>
<span class="name">use</span>
-<a title="precedes">strictly precedes</a>
+<a title="precedes">precedes</a>
<span class="name">inv</span>.</p>
</div>
@@ -2412,7 +2444,7 @@
<span class="name">wasGeneratedBy(gen;e,_a2,_t2,_attrs2)</span>
<span class="conditional">THEN</span>
<span class="name">gen</span>
-<a title="precedes">strictly precedes</a>
+<a title="precedes">precedes</a>
<span class="name">start</span>.
</li><li>
<span class="conditional">IF</span>
@@ -2421,7 +2453,7 @@
<span class="name">wasInvalidatedBy(inv;e,_a2,_t2,_attrs2)</span>
<span class="conditional">THEN</span>
<span class="name">start</span>
-<a title="precedes">strictly precedes</a>
+<a title="precedes">precedes</a>
<span class="name">inv</span>.
</li>
</ol>
@@ -2444,7 +2476,7 @@
<span class="name">wasGeneratedBy(gen;e,_a2,_t2,_attrs2)</span>
<span class="conditional">THEN</span>
<span class="name">gen</span>
-<a title="precedes">strictly precedes</a>
+<a title="precedes">precedes</a>
<span class="name">end</span>.
</li><li>
<span class="conditional">IF</span>
@@ -2453,7 +2485,7 @@
<span class="name">wasInvalidatedBy(inv;e,_a2,_t2,_attrs2)</span>
<span class="conditional">THEN</span>
<span class="name">end</span>
-<a title="precedes">strictly precedes</a>
+<a title="precedes">precedes</a>
<span class="name">inv</span>.
</li>
</ol>
@@ -2526,7 +2558,7 @@
<span class="name">wasInvalidatedBy(inv;ag,_a2,_t2,_attrs2)</span>
<span class="conditional">THEN</span>
<span class="name">start</span>
-<a title="precedes">strictly precedes</a>
+<a title="precedes">precedes</a>
<span class="name">inv</span>.
</li><li>
<span class="conditional">IF</span>
@@ -2537,7 +2569,7 @@
<span class="name">wasEndedBy(end;a,_e2,_a2,_t2,_attrs2)</span>
<span class="conditional">THEN</span>
<span class="name">gen</span>
-<a title="precedes">strictly precedes</a>
+<a title="precedes">precedes</a>
<span class="name">end</span>.
</li>
</ol>
@@ -2567,7 +2599,7 @@
<span class="name">wasInvalidatedBy(inv;ag,_a2,_t2,_attrs2)</span>
<span class="conditional">THEN</span>
<span class="name">gen</span>
-<a title="precedes">strictly precedes</a>
+<a title="precedes">precedes</a>
<span class="name">inv</span>.
</li><li>
<span class="conditional">IF</span>
@@ -2578,7 +2610,7 @@
<span class="name">wasInvalidatedBy(inv;e,_a2,_t2,_attrs2)</span>
<span class="conditional">THEN</span>
<span class="name">gen</span>
-<a title="precedes">strictly precedes</a>
+<a title="precedes">precedes</a>
<span class="name">inv</span>.
</li>
</ol>
@@ -2599,7 +2631,7 @@
<span class="name">wasInvalidatedBy(inv;ag2,_a2,_t2,_attrs2)</span>
<span class="conditional">THEN</span>
<span class="name">gen</span>
-<a title="precedes">strictly precedes</a>
+<a title="precedes">precedes</a>
<span class="name">inv</span>.
</p>
</div>
@@ -2608,6 +2640,108 @@
</section> <!--event-ordering-constraints-->
+<section>
+<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> To check an impossibility constraint on instance <span class="math">I</span>, we check 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">Perhaps this should be a constraint.</div>
+<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 we may omit it.</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 />
+
+<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>
+ <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 {
+<span class="name">used</span>,
+<span class="name">wasGeneratedBy</span>,
+<span class="name">wasInfluencedBy</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>
+
+
+ <hr />
+ <p id='entity-activity-disjoint_text'> Furthermore, the set of entities and activities are disjoint, expressed by
+ the following constraint:
+ </p>
+ <div class='constraint' id='entity-activity-disjoint'>
+<!-- <p>It is not the case that <span class="name">entity(id,_attrs1)</span> and
+<span class="name">activity(id,_t1,_t2,_attrs2)</span>.
+</p>-->
+
+<p> <span class="conditional">IF</span> <span class="name">entity(id,_attrs1)</span> and <span
+ class="name">activity(id,_t1,_t2,_attrs2)</span> <span class="conditional">THEN</span> <span class="conditional">INVALID</span>.</p>
+ </div>
+
+
+
+</section> <!--impossibility-constraints -->
+
</section> <!-- constraints -->
<section id="normalization-validity-equivalence">
@@ -2616,7 +2750,7 @@
<p>We define the notions of <a title="normal form">normalization</a>, <a
title="valid">validity</a> and
-<a title="equivalent">equivalence</a> of PROV instances. We first define these concepts
+<a title="equivalence">equivalence</a> of PROV instances. We first define these concepts
for PROV instances that consist of a single, unnamed <a>bundle</a> of
statements, called the <dfn>toplevel bundle</dfn>.</p>
@@ -2647,14 +2781,14 @@
an instance <span class="math">I<sub>3</sub></span>. If some uniqueness constraint cannot be
applied, then normalization fails.
</li>
- <li>If no inferences can be applied to instance <span class="math">I<sub>3</sub></span>, then <span class="math">I<sub>3</sub></span> is the
+ <li>If no definitions, inferences, or uniqueness constraints can be applied to instance <span class="math">I<sub>3</sub></span>, then <span class="math">I<sub>3</sub></span> is the
normal form of <span class="math">I</span>.</li>
<li>Otherwise, the normal form of <span class="math">I</span> is the same as the normal form
of <span class="math">I<sub>3</sub></span> (that is, proceed by recursively normalizing <span class="math">I<sub>3</sub></span>).
</ol>
-<p>Because of the potential interaction among inferences, definitons and
- constraints, there is a loop in the above algorithm. Nevertheless,
+<p>Because of the potential interaction among inferences, definitions and
+ constraints, the above algorithm is recursive. Nevertheless,
all of our constraints fall into a class of <a>tuple-generating
dependencies</a> and <a>equality-generating dependencies</a> that
satisfy a termination condition called <a>weak acyclicity</a> that
@@ -2682,17 +2816,22 @@
are labeled by "precedes"
and "strictly precedes" relationships among events induced by the constraints.</li>
<li> Determine whether there is a cycle in <span class="math">G</span> that contains a
- "strictly precedes" edge. If so, then <span class="math">I</span> is not <a>valid</a>. If no
- such cycle exists, then I is <a>valid</a>.
+ "strictly precedes" edge. If so, then <span class="math">I</span> is not <a>valid</a>.
+ </li>
+ <li>
+ If no
+ such cycle exists, and none of the impossibility constraints are
+ violated, then <span class="math">I</span> is <a>valid</a>.
</li>
</ol>
<p>Two PROV instances are <dfn>equivalent</dfn> if they have the
-same normal form (that is, after applying all possible inference
+isomorphic normal forms (that is, after applying all possible inference
rules, the two instances produce the same set of PROV statements,
-up to reordering of statements and attributes within attribute lists).
+up to reordering of statements and attributes within attribute lists,
+ and renaming of existential variables).
Equivalence has the following characteristics: </p>
<ul>
@@ -2707,6 +2846,10 @@
statement carrying attributes is equivalent to any other statement
obtained by permuting attribute-value pairs.
</li>
+ <li>The particular choices of names of existential variables are irrelevant to the meaning
+ of an instance; that is, the names can be permuted without changing
+ the meaning. (Replacing two different names with equal names does
+ change the meaning.)</li>
<li>
Applying inference rules, definitions, and uniqueness constraints preserves equivalence. That is, a <a>PROV
instance</a> is equivalent to the instance obtained by applying any
@@ -2718,7 +2861,7 @@
<p> An application that processes PROV data SHOULD handle
equivalent instances in the same way. (Common exceptions to this rule
-include, for example, pretty printers that seek to preserve the
+include, for example, pretty-printers that seek to preserve the
original order of statements in a file and avoid expanding
inferences.) </p>
@@ -2765,7 +2908,7 @@
..., <span class="name">B<sub>n</sub></span> are valid and none of the bundle identifiers <span class="name">b<sub>i</sub></span> are repeated.</p>
<p>Two (valid) general PROV instances <span class="name">(B<sub>0</sub>,[b<sub>1</sub>=B<sub>1</sub>,...,b<sub>n</sub>=B<sub>n</sub>])</span> and
-<span class="name">(B'<sub>0</sub>,[b<sub>1</sub>'=B'<sub>1</sub>,...,b'_m=B'_m])</span> are <a>equivalent</a> if <span class="name">B<sub>0</sub></span> is
+<span class="name">(B'<sub>0</sub>,[b<sub>1</sub>'=B'<sub>1</sub>,...,b'<sub>m</sub>=B'<sub>m</sub>])</span> are <a>equivalent</a> if <span class="name">B<sub>0</sub></span> is
equivalent to <span class="name">B'<sub>0</sub></span> and <span class="name">n = m</span> and
there exists a permutation <span class="name">P : {1..n} -> {1..n}</span> such that for each <span class="name">i</span>, <span class="name">b<sub>i</sub> =
b'<sub>P(i)</sub></span> and <span class="name">B<sub>i</sub></span> is equivalent to <span class="name">B'<sub>P(i)</sub></span>.