--- a/model/prov-constraints.html Tue Jul 17 10:56:10 2012 -0400
+++ b/model/prov-constraints.html Tue Jul 17 10:56:24 2012 -0400
@@ -196,13 +196,13 @@
"PROV-DM":
- "Luc Moreau and Paolo Missier (eds.) Khalid Belhajjame, Reza B'Far, Stephen Cresswell, Yolanda Gil, Paul Groth, Graham Klyne, Jim McCusker, Simon Miles, James Myers, Satya Sahoo, and Curt Tilmes"+
+ "Luc Moreau and Paolo Missier (eds.) Khalid Belhajjame, Reza B'Far, Stephen Cresswell, Yolanda Gil, Paul Groth, Graham Klyne, Jim McCusker, Simon Miles, James Myers, Satya Sahoo, and Curt Tilmes "+
"<a href=\"http://www.w3.org/TR/prov-dm/\"><cite>PROV-DM: The PROV Data Model</cite></a>. "+
"2012, Working Draft. "+
"URL: <a href=\"http://www.w3.org/TR/prov-dm/\">http://www.w3.org/TR/prov-dm/</a>",
"PROV-N":
- "Luc Moreau and Paolo Missier (eds.)"+
+ "Luc Moreau and Paolo Missier (eds.) "+
"<a href=\"http://www.w3.org/TR/prov-n/\"><cite>PROV-N: The Provenance Notation</cite></a>. "+
"2011, Working Draft. "+
"URL: <a href=\"http://www.w3.org/TR/prov-n/\">http://www.w3.org/TR/prov-n/</a>",
@@ -270,10 +270,10 @@
// This is optional, uncomment if you have authors as well as editors.
// only "name" is required. Same format as editors.
- //authors: ,
-// authors: [
-// { name: "TBD" },
-// ],
+//authors: ,
+ authors: [
+ { name: "Tom de Nies", company: "IBBT - Ghent University" },
+ ],
// name of the WG
wg: "Provenance Working Group",
@@ -394,7 +394,7 @@
<p> PROV-DM is a conceptual data model for provenance, which is
realizable using different serializations such as PROV-N, PROV-O, or
-PROV-XML. The PROV-DM specification [[PROV-DM]] imposes few
+PROV-XML. The PROV-DM specification [[!PROV-DM]] imposes few
requirements upon sets of PROV statements (or <a>instances</a>). By
default, PROV instances need not be valid, that is, they may not
correspond to a consistent history of objects and interactions to
@@ -421,7 +421,7 @@
of the semantics of PROV statements, which justifies the inferences
and constraints, can be found in the formal semantics [[PROV-SEM]].
</p>
-
+</section>
<section>
<h4>Structure of this document</h4>
@@ -435,7 +435,7 @@
detail in the rest of the document. </p>
<p> <a href="#inferences">Section 4</a> presents inferences and
-definitions. Definitions allow replacing shorthand notation in PROV-N
+definitions. Definitions allow replacing shorthand notation in [[!PROV-N]]
with more explicit and complete statements; inferences allow adding
new facts representing implicit knowledge about the structure of
provenance. </p>
@@ -452,11 +452,7 @@
of <a>validity</a>, <a>equivalence</a> and <a>normalization</a>.
</p>
-<p><a href="#bundle-constraints">Section 7</a> discusses how the
-preceding concepts are applied in a PROV instance with multiple
-bundles. </p>
-
-</section>
+
</section>
<section id="audience">
@@ -476,7 +472,7 @@
</p>
</section>
-</section>
+</section>
<section id='rationale' class="informative">
<h3>Rationale</h3>
@@ -683,7 +679,7 @@
<tr class="component2-color"><td class="provType"><a>Revision</a></td><td></td></tr>
<tr class="component2-color"><td class="provType"><a>Quotation</a></td><td></td></tr>
<tr class="component2-color"><td class="provType"><a>Original Source</a></td><td></td></tr>
-<tr class="component2-color"><td><a>Trace</a></td><td><a class="rule-text" href="#inference-trace"><span>TBD</span></a></td></tr>
+<tr class="component2-color"><td><a>Influence</a></td><td><a class="rule-text" href="#inference-influence"><span>TBD</span></a></td></tr>
<tr><td style="border-width: 0px; "></td><td style="border-width: 0px; "></td><td style="border-width: 0px; "></td></tr>
<tr class="component3-color" style="border-collapse: collapse; "><td class="essential"><a>Agent</a></td><td> </td><td rowspan="8"><a href="#component3">Component 3: Agents/Responsibility</a></td></tr>
@@ -816,14 +812,12 @@
list <span class="conditional">IF AND ONLY IF</span> <span class="name">r(id;a_1,...,a_n,[])</span> holds.</p>
</div>
- <p>We assume from now on that all optional identifiers have been
- filled in and all explicit attributes have been removed, generating
- <span class='name'>attribute</span> statements. Finally, many PROV
+ <p> Finally, many PROV
expressions have other optional arguments or short forms that can be
used if none of the optional arguments is present. These are
handled by specific rules listed below. </p> </section>
-
+<div class="note">Add expansion rules for optionals</div>
<section>
<h3>Component 1: Entities and Activities</h3>
@@ -849,8 +843,9 @@
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>
</div>
-<div class="note"> We don't give counterexamples to other
- non-inferences. Suggest dropping this one.</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>
<p>The relationship <span class="name">wasInformedBy</span> is not
<a>transitive</a>. Indeed, consider the following statements.</p>
@@ -1089,23 +1084,56 @@
<span class='conditional'>THEN</span> there exist <span
class="name">_id2</span>, <span class="name">_pl2</span>, and <span class="name">_attrs2</span> such that <span class="name">wasAssociatedWith(_id2;a, ag2, _pl2, _attrs2)</span>.
</p>
+</div>
+
+<hr />
+<p id="inference-influence_text">
+The <span class="name">wasInfluencedBy</span> relation is implied by other relations, including
+usage, start, end, generation, invalidation, communication,
+derivation, attribution, association, and delegation. To capture this
+explicitly, we allow the following inferences:
+</p>
+<div class="inference" id="inference-influence">
<p>
-<span class='conditional'>IF</span>
-<span class="name">wasAssociatedWith(_id2;a, ag1, _pl2, _attrs2)</span>
- and <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>, and <span class="name">_attrs1</span> such that <span class="name">wasAssociatedWith(_id1;a, ag1, _pl1, _attrs1)</span>.
+ <ol>
+ <li>
+ <span class="conditional">IF</span> <span class="name">wasGeneratedBy(id;e,a,t,attrs)</span> <span class="conditional">THEN</span> <span class="name">wasInfluencedBy(id; o2, o1, attrs)</span>.
+ </li>
+ <li>
+ <span class="conditional">IF</span> <span class="name">used(id;a,e,t,attrs)</span> <span class="conditional">THEN</span> <span class="name">wasInfluencedBy(id; a, e, attrs)</span>.
+ </li>
+ <li>
+ <span class="conditional">IF</span> <span class="name">wasInformedBy(id;a2,a1,attrs)</span> <span class="conditional">THEN</span> <span class="name">wasInfluencedBy(id; a2, a1, attrs)</span>.
+ </li>
+ <li>
+ <span class="conditional">IF</span> <span class="name">wasStartedBy(id;a2,e,a1,t,attrs)</span> <span class="conditional">THEN</span> <span class="name">wasInfluencedBy(id; a2, e, attrs)</span>.
+ </li>
+ <li>
+ <span class="conditional">IF</span> <span class="name">wasEndedBy(id;a2,e,a1,t,attrs)</span> <span class="conditional">THEN</span> <span class="name">wasInfluencedBy(id; a2, e, attrs)</span>.
+ </li>
+ <li>
+ <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>.
+ </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>
+ <span class="conditional">IF</span> <span class="name">wasAssociatedWith(id;a,ag,pl,attrs)</span> <span class="conditional">THEN</span> <span class="name">wasInfluencedBy(id; a, ag, attrs)</span>.
+ </li>
+ <li>
+ <span class="conditional">IF</span> <span class="name">actedOnBehalfOf(id;ag2,ag1,a,attrs)</span> <span class="conditional">THEN</span> <span class="name">wasInfluencedBy(id; ag2, ag1, attrs)</span>.
+ </li>
+</ol>
</p>
-</div>
-
-
-
</section>
<section>
-<h3>Component 4: Alternate and Specialized Entities</h3>
+<h3>Component 5: Alternate and Specialized Entities</h3>
@@ -1195,7 +1223,21 @@
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>
</div>
-
+
+
+ <div class="note">
+<p>Note: The following inference is associated with a feature "<a href="http://www.w3.org/2005/10/Process-20051014/tr#cfi">at risk</a>" and may be removed from this specification based on feedback. Please send feedback to public-prov-comments@w3.org.</p>
+</div>
+
+ <hr>
+
+ <p id="mention-specialization_text">If one entity is a mention of another in a bundle, then the former is also a specialization of the latter:</p>
+
+ <div class='inference' id="mention-specialization">
+<p>
+<span class='conditional'>IF</span> <span class='name'>mentionOf(e2,e1,b)</span> <span class='conditional'>THEN</span> <span class='name'>specializationOf(e2,e1)</span>.</p>
+ </div>
+
</section>
@@ -1222,7 +1264,7 @@
<li> and <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 partial order that corresponds to a sensible
+ PROV instance into a preorder that corresponds to a sensible
"history" (for example, an entity should not be generated after it
is used).
</li>
@@ -1264,25 +1306,20 @@
<a>merge</a> is </li>
<li> The <a>merge</a> of two attribute lists <span
class="name">attrs1</span> and <span class="name">attrs2</span>
- is their union, considered as unordered lists:, written <span
+ is their union, considered as unordered lists, written <span
class="name">attrs1 ∪ attrs2</span> </li>
- <li> If <span class="name">r(id;t_1,...,t_n,attrs1)</span> and
- <span class="name">r(id;u_1,...,u_n,attrs2)</span> are two
- statements with the same name, same identifier, and same number
- of arguments, then
- </li>
- </ul>
+</ul>
A typical uniqueness constraint is as follows:
<div class="constraint-example" id="uniqueness-example">
<p> IF hyp_1 AND ... AND hyp_n THEN t_1 = u_1 AND ... AND t_n = u_n.</p>
</div>
- where
-
- In the common case that a particular field of a relation uniquely
+
+<p> In the common case that a particular field of a relation uniquely
determines the other fields, we call the uniqueness constraint a
<a>key constraint</a>. Key constraints are written as follows:
+ </p>
<div
class="constraint-example" id="key-example">
@@ -1290,13 +1327,15 @@
class="name">a_k</span> field is a KEY for relation <span
class="name">r(a_0;a_1,...a_n)</span>. </p></div>
- A key constraint is interpreted as a uniqueness constraint of the
- following form:
+ <p> A key constraint is interpreted as a uniqueness constraint of the
+ following form:</p>
+
<div
class="constraint-example" id="key-example-expanded">
<p>IF <span
class="name">r(a_0;a_1,...a_n)</span> AND <span
- class="name">r(b_0;b_1,...b_n)</span> (where a_k = b_k) THEN <span
+ class="name">r(b_0;b_1,...b_n)</span> (where <span
+ class="name">a_k = b_k</span>) THEN <span
class="name">a_0 = b_0 </span> AND ... AND <span
class="name">a_n = b_n</span>. </p></div>
@@ -1344,28 +1383,54 @@
</p>
<div class='constraint' id='key-relation'>
<p><ol>
- <li>The identifier field <span class="name">use</span> is a KEY for
- the <span class="name">used(use;a,e,t,attrs)</span> statement.
- </li>
- <li>The identifier field <span class="name">gen</span> is a KEY for
- the <span class="name">wasGeneratedBy(gen;e,a,t,attrs)</span> statement.
+ <li>The identifier field <span class="name">id</span> is a KEY for
+ the <span class="name">used(id;a,e,t,attrs)</span> statement.
</li>
- <li>...</li>
- </ol>
+ <li>The identifier field <span class="name">id</span> is a KEY 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
+ 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
+ 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
+ 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
+ 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
+ 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
+ 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
+ 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
+ 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
+ the <span class="name">actedOnBehalfOf(id;ag2,ag1,a,attrs)</span> statement.
+ </li>
+</ol>
</p> </div>
- <div class="note">@@TODO: Same goes for other relations:
-generation, usage, invalidation, start, end,
- communication, attribution, association, delegation,
- derivation, revision, quotation.
- </div>
<hr>
-
+
+<div class="note"> The next four constraints can be stated more simply
+as key constraints</div>
<div id='unique-generation_text'>
<p>We assume that an entity has exactly one generation and
invalidation event (either or both may, however, be left implicit).
+ Note that together with the key constraints above, this implies that
+ <span class="name">e</span> is also a key for generation and
+ invalidation statements.
</p>
</div>
@@ -1373,17 +1438,15 @@
<div class='constraint' id='unique-generation'>
<p>
<span class='conditional'>IF</span> <span class="name">wasGeneratedBy(id1;e,a1,t1,attrs1)</span> and <span class="name">wasGeneratedBy(id2;e,a2,t2,attrs2)</span>,
-<span class='conditional'>THEN</span> <span class="name">id1</span>=<span class="name">id2</span>, <span class="name">a1</span>=<span class="name">a2</span>, <span class="name">t1</span>=<span class="name">t2</span> and <span class="name">attrs1</span>=<span class="name">attrs2</span>.</p>
+<span class='conditional'>THEN</span> <span class="name">id1</span>=<span class="name">id2</span>.</p>
</div>
<div class='constraint' id='unique-invalidation'>
<p>
<span class='conditional'>IF</span> <span class="name">wasInvalidatedBy(id1;e,a1,t1,attrs1)</span> and <span class="name">wasInvalidatedBy(id2;e,a2,t2,attrs2)</span>,
-<span class='conditional'>THEN</span> <span class="name">id1</span>=<span class="name">id2</span>, <span class="name">a1</span>=<span class="name">a2</span>, <span class="name">t1</span>=<span class="name">t2</span> and <span class="name">attrs1</span>=<span class="name">attrs2</span>.</p>
+<span class='conditional'>THEN</span> <span class="name">id1</span>=<span class="name">id2</span>.</p>
</div>
-<div class="note">
-Should the id of a generation/invalidation be uniquely determined by entity?
-</div>
+
<p> It follows from the above constraints that the generation and
invalidation times of
@@ -1395,7 +1458,10 @@
<hr />
<p id='unique-wasStartedBy_text'>
<p>We assume that an activity has exactly one start and
-end event (either or both may, however, be left implicit).
+end event (either or both may, however, be left implicit). Again,
+together with above key constraints these constraints imply that the
+activity is a key for activity start and end statements.,
+these
</p>
<div class='constraint' id='unique-wasStartedBy'>
@@ -1404,30 +1470,17 @@
class="name">wasStartedBy(id;a,e1,a1,t,attrs)</span> and <span
class="name">wasStartedBy(id';a,e1',a1',t',attrs')</span>, <span
class='conditional'>THEN</span> <span class="name">id</span>=<span
- class="name">id'</span> and <span class="name">e1</span>=<span
- class="name">e1'</span> and <span class="name">a1</span>=<span
- class="name">a1'</span> and <span class="name">t</span>=<span class="name">t'</span>
- and <span class="name">attrs</span>=<span class="name">attrs'</span>.</p>
+ class="name">id'</span>.</p>
</div>
-<p>
-<hr />
-<p id='unique-wasEndedBy_text'>
-<p>We assume that an activity has exactly one start and
-end event (either or both may, however, be left implicit).
-</p>
-
<div class='constraint' id='unique-wasEndedBy'>
<p>
<span class='conditional'>IF</span> <span
class="name">wasEndedBy(id;a,e1,a1,t,attrs)</span> and <span
class="name">wasEndedBy(id';a,e1',a1',t',attrs')</span>, <span
class='conditional'>THEN</span> <span class="name">id</span>=<span
- class="name">id'</span> and <span class="name">e1</span>=<span
- class="name">e1'</span> and <span class="name">a1</span>=<span
- class="name">a1'</span> and <span class="name">t</span>=<span class="name">t'</span>
- and <span class="name">attrs</span>=<span class="name">attrs'</span>.</p>
+ class="name">id'</span>.</p>
</div>
@@ -1437,11 +1490,7 @@
-<div class="note">James: The unique-startTime and unique-endTime constraints
- are now redundant, by activity-start-end-inference and unique-wasStartedBy/unique-wasEndedBy.<br>
-Luc: Agreed. However, I feel it's easier to check these constraints than to infer new expressions, and then check constraints.</div>
-
- <p id='unique-startTime_text'>An <a>activity start event</a> is the <a title="instantaneous event">instantaneous event</a> that marks the instant an activity starts. It allows for an optional time attribute. <span id="optional-start-time">Activities also allow for an optional start time attribute. If both are specified, they MUST be the same, as expressed by the following constraint.</span>
+ <p id='unique-startTime_text'>An <a>activity start event</a> is the <a title="instantaneous event">instantaneous event</a> that marks the instant an activity starts. It allows for an optional time attribute. <span id="optional-start-time">Activities also allow for an optional start time attribute. If both are specified, they MUST be the same, as expressed by the following constraint.</span>
</p>
<div class='constraint' id='unique-startTime'>
@@ -1465,17 +1514,11 @@
<p>
-<hr>
-
-
-<div class="note">This constraint belongs here (with other uniqueness
- constraints), or in the section on bundles.</div>
+<hr />
+
<div class="note">
-<p>Note: The following two constraints are a feature "<a href="http://www.w3.org/2005/10/Process-20051014/tr#cfi">at risk</a>" and may be removed from this specification based on feedback. Please send feedback to public-prov-comments@w3.org.</p>
-
-
-<p>The expression Mention might be removed from PROV if implementation experience reveals problems with supporting this construct.</p>
+<p>Note: The following constraint is associated with a feature "<a href="http://www.w3.org/2005/10/Process-20051014/tr#cfi">at risk</a>" and may be removed from this specification based on feedback. Please send feedback to public-prov-comments@w3.org.</p>
</div>
@@ -1490,18 +1533,8 @@
<span class='conditional'>THEN</span> <span class="name">e1</span>=<span class="name">e2</span> and <span class="name">b1</span>=<span class="name">b2</span>.</p>
</div>
-<p>
-
-<hr>
-
- <p id="mention-specialization_text">If one entity is a mention of another in a bundle, then the former is also a specialization of the latter:</p>
-
- <div class='inference' id="mention-specialization">
-<p>
-<span class='conditional'>IF</span> <span class='name'>mentionOf(e2,e1,b)</span> <span class='conditional'>THEN</span> <span class='name'>specializationOf(e2,e1)</span>.</p>
- </div>
-
-<p>
+
+
@@ -1526,27 +1559,26 @@
<p>To allow for minimalistic clock assumptions, like Lamport
[[CLOCK]], PROV-DM relies on a notion of relative ordering of <a title="instantaneous event">instantaneous events</a>,
-without using physical clocks. This specification assumes that a partial order exists between <a title="instantaneous event">instantaneous events</a>.
+without using physical clocks. This specification assumes that a preorder exists between <a title="instantaneous event">instantaneous events</a>.
</p>
-<p>Specifically, <dfn id="dfn-precedes">precedes</dfn> is a partial
-order between <a title="instantaneous event">instantaneous events</a>. When we say
-<span class="name">e1</span> precedes <span class="name">e2</span>,
-this means that <span
-class="name">e1</span> happened at the same time as or before <span class="name">e2</span>.
+<p>Specifically, <dfn id="dfn-precedes">precedes</dfn> is a <a>preorder</a>
+between <a title="instantaneous event">instantaneous events</a>. When
+we say <span class="name">e1</span> precedes <span
+class="name">e2</span>, this means that <span class="name">e1</span>
+happened at the same time as or before <span class="name">e2</span>.
For symmetry, <dfn id="dfn-follows">follows</dfn> is defined as the
inverse of <a title="precedes">precedes</a>; that is, when we say
<span class="name">e1</span> follows <span class="name">e2</span>,
-this means that <span
-class="name">e1</span> happened at the same time as or after <span
-class="name">e2</span>. Both relations are <a>preorder</a>s, meaning
-that they are <a>reflexive</a> and <a>transitive</a>. Moreover, we
-consider strict forms of these orders: we say <span
-class="name">e1</span> strictly precedes <span class="name">e2</span>
-to indicate that <span
-class="name">e1</span> happened before <span class="name">e2</span>.
-This is a <a>transitive</a> relation. </p>
+this means that <span class="name">e1</span> happened at the same time
+as or after <span class="name">e2</span>. Both relations are
+<a>preorder</a>s, meaning that they are <a>reflexive</a> and
+<a>transitive</a>. Moreover, we consider strict forms of these
+orders: we say <span class="name">e1</span> strictly precedes <span
+class="name">e2</span> to indicate that <span class="name">e1</span>
+happened before <span class="name">e2</span>. This is a
+<a>transitive</a> relation. </p>
<p>PROV-DM also allows for time observations to be inserted in
@@ -1556,7 +1588,7 @@
different sources might be with respect to different timelines
(e.g. different time zones) leading to apparent inconsistencies. For
the purpose of checking ordering constraints, the times associated
-with events is irrelevant; thus, there is no inference time ordering
+with events are irrelevant; thus, there is no inference that time ordering
implies event ordering. However, an application MAY flag time values
that appear inconsistent with the event ordering as possible
inconsistencies. When generating provenance, an application SHOULD
@@ -1571,17 +1603,17 @@
<p>IF <span
class="name">hyp_1</span> AND ... AND <span
class="name">hyp_n</span> THEN <span
- class="name">a_0</span> <a>precedes</a>/<a>strictly precedes</a> <span
+ class="name">a_0</span> <a>precedes</a>/<a title="precedes">strictly precedes</a> <span
class="name">b_0</span>. </p></div>
<p>
The conclusion of an ordering constraint is either <a>precedes</a>
- or <a>strictly precedes</a>. To check ordering constraints, we
- generate all possible <a>precedes</a> and <a>strictly precedes</a>
+ or <a title="precedes">strictly precedes</a>. To check ordering constraints, we
+ generate all possible <a>precedes</a> and <a title="precedes">strictly precedes</a>
relationships (including transitive), and check that the resulting
- relation has no strict cycles (that is, the <a>strictly precedes</a>
+ relation has no strict cycles (that is, the <a title="precedes">strictly precedes</a>
relation induced by the edges is irreflexive). This is equivalent to
constructing a directed graph, with edges marked <a>precedes</a> or
- <a>strictly precedes</a>, and checking that there is no cycle
+ <a title="precedes">strictly precedes</a>, and checking that there is no cycle
containing a <a>strictly-precedes</a> edge.
</p>
@@ -1616,23 +1648,16 @@
constraints on activities in a
graphical manner. For this and subsequent figures, an event time line points to the
right. Activities are represented by rectangles, whereas entities are
-represented by circles. Usage, generation and derivation are
+represented by circles. Usage, generation and invalidation are
represented by the corresponding edges between entities and
activities. The five kinds of <a title="instantaneous event">instantaneous events</a> are represented by vertical
dotted lines (adjacent to the vertical sides of an activity's
rectangle, or intersecting usage and generation edges). The ordering
constraints are represented by triangles: an occurrence of a triangle between two <a title="instantaneous event">instantaneous event</a> vertical dotted lines represents that the event denoted by the left
line precedes the event denoted by the right line.</p>
- <div class="note"> Miscellanous suggestions about figures:
+ <div class="note"> Miscellanous suggestions about figures
+ (originally from Tim Lebo):
<li>
- The use of triangles in the ordering constraints leaves me uncertain
- about which vertical line they are constraining. I worry that it
- is not the "very next one". I would be more confident if a yellow
- horizontal "edge" actually touched the two vertical edges that it
- was constraining (and the yellow triangle could be on top of that
- edge).
-
-</li><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>
@@ -1665,7 +1690,7 @@
<span class="name">wasEndedBy(end;a,_e2,_a2,_t2,_attrs2)</span>
<span class="conditional">THEN</span>
<span class="name">start</span>
-<a>precedes</a>
+<a title="precedes">strictly precedes</a>
<span class="name">end</span>.
</p>
</div>
@@ -1684,7 +1709,7 @@
<span class="name">wasStartedBy(start;a,_e1,_a1,_t1,_attrs1)</span>
<span class="conditional">THEN</span>
<span class="name">start</span>
-<a>precedes</a>
+<a title="precedes">strictly precedes</a>
<span class="name">use</span>.
</li>
<li>
@@ -1694,7 +1719,7 @@
<span class="name">wasEndedBy(end;a,_e1,_a1,_t1,_attrs1)</span>
<span class="conditional">THEN</span>
<span class="name">use</span>
-<a>precedes</a>
+<a title="precedes">strictly precedes</a>
<span class="name">end</span>.
</li>
</ol>
@@ -1712,22 +1737,22 @@
<ol>
<li>
<span class="conditional">IF</span>
-<span class="name">wasGeneratedBy(gen;e,a,_t,_attrs)</span>
-and
+<span class="name">wasGeneratedBy(gen;_e,a,_t,_attrs)</span>
+AND
<span class="name">wasStartedBy(start;a,_e1,_a1,_t1,_attrs1)</span>
<span class="conditional">THEN</span>
<span class="name">start</span>
-<a>precedes</a>
+<a title="precedes">strictly precedes</a>
<span class="name">gen</span>.
</li>
<li>
<span class="conditional">IF</span>
-<span class="name">wasGeneratedBy(gen;e,a,_t,_attrs)</span>
-and
+<span class="name">wasGeneratedBy(gen;_e,a,_t,_attrs)</span>
+AND
<span class="name">wasEndedBy(end;a,_e1,_a1,_t1,_attrs1)</span>
<span class="conditional">THEN</span>
<span class="name">gen</span>
-<a>precedes</a>
+<a title="precedes">strictly precedes</a>
<span class="name">end</span>.
</li>
</ol>
@@ -1736,7 +1761,9 @@
<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
@@ -1749,11 +1776,9 @@
(d) and expressed by <a class="rule-ref"
href="#wasInformedBy-ordering"><span>TBD</span></a>.</p>
-<div class="note">The following template illustrates the convention:
- any variable that appears only once in a constraint should start
- with _. TODO: Adopt this for other constraints.</div>
<div class='constraint' id='wasInformedBy-ordering'>
- <span class="conditional">IF</span>
+<p>
+ <span class="conditional">IF</span>
<span class="name">wasInformedBy(_id;a2,a1,_attrs)</span>
and
<span class="name">wasStartedBy(start;a1,_e1,_a1',_t1,_attrs1)</span>
@@ -1761,9 +1786,9 @@
<span class="name">wasEndedBy(end;a2,_e2,_a2',_t2,_attrs2)</span>
<span class="conditional">THEN</span>
<span class="name">start</span>
-<a>precedes</a>
+<a title="precedes">strictly precedes</a>
<span class="name">end</span>.
-
+</p>
</div>
<p>
@@ -1788,7 +1813,7 @@
<span class="name">wasStartedBy(start1;a1,-,-,-)</span>
<span class="conditional">THEN</span>
<span class="name">start1</span>
-<a>precedes</a>
+<a title="precedes">strictly precedes</a>
<span class="name">start2</span>.
</div>
-->
@@ -1835,7 +1860,7 @@
<span class="name">wasInvalidatedBy(inv;e,_a2,_t2,_attrs2)</span>
<span class="conditional">THEN</span>
<span class="name">gen</span>
-<a>precedes</a>
+<a title="precedes">strictly precedes</a>
<span class="name">inv</span>.
</p>
</div>
@@ -1856,7 +1881,7 @@
<span class="name">used(use;_a2,e,_t2,_attrs2)</span>
<span class="conditional">THEN</span>
<span class="name">gen</span>
-<a>precedes</a>
+<a title="precedes">strictly precedes</a>
<span class="name">use</span>.
</p>
</div>
@@ -1874,7 +1899,7 @@
<span class="name">wasInvalidatedBy(inv;e,_a2,_t2,_attrs2)</span>
<span class="conditional">THEN</span>
<span class="name">use</span>
-<a>precedes</a>
+<a title="precedes">strictly precedes</a>
<span class="name">inv</span>.</p>
</div>
@@ -1885,11 +1910,6 @@
-<div class="note">
- Can ordering constraints be factored into "influence implies
- precedes" and "everything implies influence"?
- </div>
-
<p id='derivation-usage-generation-ordering_text'>If there is a derivation between <span class="name">e2</span> and <span class="name">e1</span>, then
this means that the entity <span class="name">e1</span> had some influence on the entity <span class="name">e2</span>; for this to be possible, some event ordering must be satisfied.
First, we consider derivations, where the activity and usage are known. In that case, the <a title="entity usage event">usage</a> of <span class="name">e1</span> has to precede the <a title="entity generation
@@ -1905,7 +1925,7 @@
<span class="name">wasDerivedFrom(_d;_e2,_e1,_a,gen2,use1,_attrs)</span>
<span class="conditional">THEN</span>
<span class="name">use1</span>
-<a>precedes</a>
+<a title="precedes">strictly precedes</a>
<span class="name">gen2</span>.
</p>
</div>
@@ -1913,7 +1933,7 @@
<hr />
<p id='derivation-generation-generation-ordering_text'>
-When the usage is unknown, a similar constraint exists, except that the constraint refers to its
+When the activity, generation or usage is unknown, a similar constraint exists, except that the constraint refers to its
generation event, as
illustrated by <a href="#ordering-entity-fig">Figure 3</a> (c) and expressed by <a
class="rule-ref" href="#derivation-generation-generation-ordering"><span>TBD</span></a>.</p>
@@ -1929,7 +1949,7 @@
<span class="name">wasGeneratedBy(gen2;e2,_a2,_t2,_attrs2)</span>
<span class="conditional">THEN</span>
<span class="name">gen1</span>
-<a>precedes</a>
+<a title="precedes">strictly precedes</a>
<span class="name">gen2</span>.
</p>
</div>
@@ -1951,21 +1971,21 @@
<ol>
<li>
<span class="conditional">IF</span>
-<span class="name">wasStartedBy(start;a,e,_a1,_t1,_attrs1)</span>
+<span class="name">wasStartedBy(start;_a,e,_a1,_t1,_attrs1)</span>
and
<span class="name">wasGeneratedBy(gen;e,_a2,_t2,_attrs2)</span>
<span class="conditional">THEN</span>
<span class="name">gen</span>
-<a>precedes</a>
+<a title="precedes">strictly precedes</a>
<span class="name">start</span>.
</li><li>
<span class="conditional">IF</span>
-<span class="name">wasStartedBy(start;a,e,_a1,_t1,_attrs1)</span>
+<span class="name">wasStartedBy(start;_a,e,_a1,_t1,_attrs1)</span>
and
<span class="name">wasInvalidatedBy(inv;e,_a2,_t2,_attrs2)</span>
<span class="conditional">THEN</span>
<span class="name">start</span>
-<a>precedes</a>
+<a title="precedes">strictly precedes</a>
<span class="name">inv</span>.
</li>
</ol>
@@ -1983,21 +2003,21 @@
<ol>
<li>
<span class="conditional">IF</span>
-<span class="name">wasEndedBy(end;a,e,_a1,_t1,_attrs1)</span>
+<span class="name">wasEndedBy(end;_a,e,_a1,_t1,_attrs1)</span>
and
<span class="name">wasGeneratedBy(gen;e,_a2,_t2,_attrs2)</span>
<span class="conditional">THEN</span>
<span class="name">gen</span>
-<a>precedes</a>
+<a title="precedes">strictly precedes</a>
<span class="name">end</span>.
</li><li>
<span class="conditional">IF</span>
-<span class="name">wasEndedBy(end;a,e,_a1,_t1,_attrs1)</span>
+<span class="name">wasEndedBy(end;_a,e,_a1,_t1,_attrs1)</span>
and
<span class="name">wasInvalidatedBy(inv;e,_a2,_t2,_attrs2)</span>
<span class="conditional">THEN</span>
<span class="name">end</span>
-<a>precedes</a>
+<a title="precedes">strictly precedes</a>
<span class="name">inv</span>.
</li>
</ol>
@@ -2017,7 +2037,7 @@
</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> precedes-or-equals <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> THEN <span class="name">gen1</span> <a>precedes</a> <span class="name">gen2</span>.
<p/p>
</div>
<hr />
@@ -2026,7 +2046,7 @@
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-or-equals</a> <span class="name">inv1</span>.
+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>.
</p>
</div>
@@ -2070,7 +2090,7 @@
<span class="name">wasInvalidatedBy(inv;ag,_a2,_t2,_attrs2)</span>
<span class="conditional">THEN</span>
<span class="name">start</span>
-<a>precedes</a>
+<a title="precedes">strictly precedes</a>
<span class="name">inv</span>.
</li><li>
<span class="conditional">IF</span>
@@ -2081,7 +2101,7 @@
<span class="name">wasEndedBy(end;a,_e2,_a2,_t2,_attrs2)</span>
<span class="conditional">THEN</span>
<span class="name">gen</span>
-<a>precedes</a>
+<a title="precedes">strictly precedes</a>
<span class="name">end</span>.
</li>
</ol>
@@ -2111,7 +2131,7 @@
<span class="name">wasInvalidatedBy(inv;ag,_a2,_t2,_attrs2)</span>
<span class="conditional">THEN</span>
<span class="name">gen</span>
-<a>precedes</a>
+<a title="precedes">strictly precedes</a>
<span class="name">inv</span>.
</li><li>
<span class="conditional">IF</span>
@@ -2122,7 +2142,7 @@
<span class="name">wasInvalidatedBy(inv;e,_a2,_t2,_attrs2)</span>
<span class="conditional">THEN</span>
<span class="name">gen</span>
-<a>precedes</a>
+<a title="precedes">strictly precedes</a>
<span class="name">inv</span>.
</li>
</ol>
@@ -2143,7 +2163,7 @@
<span class="name">wasInvalidatedBy(inv;ag2,_a2,_t2,_attrs2)</span>
<span class="conditional">THEN</span>
<span class="name">gen</span>
-<a>precedes</a>
+<a title="precedes">strictly precedes</a>
<span class="name">inv</span>.
</p>
</div>
@@ -2154,15 +2174,112 @@
</section> <!-- constraints -->
- <section id="equivalence">
-<h2>Equivalence</h2>
-<div class="note">TODO: revise to discuss role of definitions and
- constraints in normalization, equivalence and
- validity checking</div>
-
- We define a
-notion of <a>normalization</a>, <a>validity</a> and <a>equivalence</a> of PROV instances. Equivalence has the following characteristics:
-
+ <section id="normalization-validity-equivalence">
+<h2>Normalization, Equivalence and Validity</h2>
+
+
+ <p>We define notions of <a>normalization</a>, <a>validity</a> and
+<a>equivalence</a> of PROV instances. We first define these concepts
+for PROV instances that consist of a single, unnamed bundle of
+statements, called the <a>toplevel bundle</a>.</p>
+
+ <section id="optional-attributes">
+ <h3>Optional Attributes</h3>
+
+
+<div id="optional-attributes1">
+<p>PROV-N allows some statement parameters and attributes to
+ be optional. Unless otherwise specified, when an
+ optional attribute is not present in a statement, it has a default
+ value. Thus, most optional parameters (written <span
+ class="name">-</span>) should be replaced by existential variables.
+ The only exceptions are:
+ </p>
+ <ul>
+<li><div id="optional-attributes4">In an association of the form
+ <span class="name">wasAssociatedWith(id;a, ag,-,attr)</span>, the
+ 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.</div></li>
+ <li><div id="optional-attributes4">In an association 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,
+generations, and uses. Thus, it is not equivalent to <span
+ class="name">wasDerivedFrom(id;e1,e2,a,g,u,attr)</span> where some
+ activity, generation and use are given explicitly.</div></li>
+</div></li>
+ </ul>
+</div>
+
+</section>
+
+<section id="normalization">
+<h3>Normalization and Validity</h3>
+
+<p> We define the <dfn>normal form</dfn> of a PROV instance as the set
+of provenance expressions resulting from merging to resolve all
+uniqueness constraints in the instance and applying all possible
+inference rules to this set. Formally, we say that two PROV instances
+are <dfn>equivalent</dfn> if they have the same normal form (that is,
+after applying all possible inference rules, the two instances produce
+the same set of PROV-DM expressions.) </p>
+
+<p> An application that processes PROV-DM data SHOULD handle
+equivalent instances in the same way. (Common exceptions to this rule
+include, for example, pretty printers that seek to preserve the
+original order of statements in a file and avoid expanding
+inferences.) </p>
+
+ A PROV instance is <dfn id="dfn-valid">valid</dfn>
+if its normal form exists and satisfies all of
+ the validity constraints; this implies that the instance satisfies
+ all of the inferences, definitions and constraints.
+ The following algorithm can be used to compute normal forms and test
+ validity:
+
+ <ol>
+ <li>
+ Apply all definitions by replacing each defined statement by its
+ definition (possibly introducing fresh identifiers in the process).
+ </li>
+ <li>
+ Apply all inferences by adding the conclusion of each inference
+ whose hypotheses are satisfied and whose conclusion does not
+ already hold.
+ </li>
+ <li>
+ Apply all uniqueness constraints by merging pairs of statements
+ and unifying existential variables and constants (or failing if this would require merging two
+ distinct constants). Merging may lead to substitutions of
+ existential variables that enable new inferences; thus, steps 2
+ and 3 may
+ need to be repeated.
+ </li>
+ <li>Apply event ordering constraints to determine whether there is
+ a consistent ordering on the events in the normal form.
+ </li>
+ </ol>
+
+<p>Because of the potential interaction among inferences, definitons and
+ constraints, there is a loop in the above algorithm. 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
+ has been studied in the context of relational databases
+ [[DBCONSTRAINTS]]. Therefore, the above algorithm terminates, independently
+ of the order in which inferences and constraints are applied.
+<div class="note">
+ Must check this for final constraints/inferences!
+ </div>
+</p>
+</section>
+ <section id="equivalence">
+<h3>Equivalence</h3>
+ <p>
+Equivalence has the following characteristics:
+</p>
<ul>
<li>
@@ -2185,121 +2302,61 @@
<li>Equivalence is reflexive, symmetric, and transitive.</li>
</ul>
- <section id="optional-attributes">
- <h3>Optional Attributes</h3>
-
-<div class="note">
- TODO: Clarify how optional attributes are handled; clarify merging. The following is
- not very explicit about the difference between "not present" and
- "omitted but inferred".
- </div>
-<div id="optional-attributes1">
-<p>PROV-N allows some statement parameters and attributes to
- be optional. Unless otherwise specified, when an
- optional attribute is not present in a statement, it has a default
- value.</p>
-
- The only exceptions are:
- <ul>
-<li><div id="optional-attributes4">In an association of the form
- <span class="name">wasAssociatedWith(id;a, ag,-,attr)</span>, the
- 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.</div></li>
- <li><div id="optional-attributes4">In an association of the form
- <span class="name">wasDerivedFrom(id;e1, a,e2,attr)</span>, the
- absence of the optional activity, generation and use identifiers
- means that the derivation relationship may encompass multiple activities,
-generations, and uses. Thus, it is not equivalent to <span
- class="name">wasDerivedFrom(id;e1,e2,a,g,u,attr)</span> where some
- activity, generation and use are given explicitly.</div></li>
-</div></li>
- </ul>
-</div>
+
</section>
-
-<section id="normalization">
-<h3>Normalization and Equivalence</h3>
-<div class="note"> Is instance = bundle here?</div>
-
-<p>
-We define the <dfn>normal form</dfn> of a PROV instance as the set
-of provenance expressions resulting from merging all of the overlapping
-expressions in the instance and applying all possible inference rules
-to this set. Formally, we say that two PROV instances are
-<dfn>equivalent</dfn> if they have the same normal form (that is,
-after applying all possible inference rules, the two instances produce
-the same set of PROV-DM expressions.)
-</p>
-
-<div class="note">
- We should check that normal forms exist, i.e. that applying rules
- and definitions eventually terminates. More clarity is needed about
- enforcing uniqueness via merging vs. constraint checking.
- </div>
-
-<p> An application that processes PROV-DM data SHOULD handle
-equivalent instances in the same way. (Common exceptions to this rule
-include, for example, pretty printers that seek to preserve the
-original order of statements in a file and avoid expanding
-inferences.) </p>
-
-</section>
- <section id="validity">
-<h3>Validity</h3>
-
- <div class="note">Move material on validity here. Signpost it in
- sec. 1 and 2. </div>
- A PROV instance is <dfn id="dfn-valid">valid</dfn>
-if its normal form exists and satisfies all of
- the validity constraints; this implies that the instance satisfies
- all of the inferences, definitions and constraints.
- The following algorithm can be used to compute normal forms and determine validity:
-
- <ol>
- <li>
- Apply all definitions by replacing each defined statement by its
- definition (possibly introducing fresh identifiers in the process).
- </li>
- <li>
- Apply all inferences by adding the conclusion of each inference
- whose hypotheses are satisfied and whose conclusion does not
- already hold.
- </li>
- <li>
- Apply all uniqueness constraints by merging pairs of statements
- and unifying identifiers and constants (or failing if this would require merging two
- distinct constants). If successful, this yields a normal form.
- </li>
- <li>Apply event ordering constraints to determine whether there is
- a consistent ordering on the events in the normal form.
- </li>
- </ul>
-
- <div class="note">Justify termination, confluence.</div>
-</section>
-
-</section> <!-- equivalence -->
-
-
-
<section id="bundle-constraints">
<h2>Bundles and Constraints</h2>
<div class="note">
-TODO: Summarize how bundles interact with constraints.
- Briefly, idea is: check each bundle independently, using the same
- rules as for top-level statements. A whole PROV instance containing
- several bundles is valid if each bundle is valid (including the "top
- level").
+TODO: Fix notation.
</div>
+<p>The definitions, inferences, and constraints introduced so far, and
+the resulting notions of normalization, validity and equivalence,
+assume a PROV instance with exactly one <a>bundle</a>, the <a>toplevel
+bundle</a>, consisting of all PROV statements in the toplevel of the
+instance. In this section, we describe how to deal with PROV
+instances consisting of multiple bundles. Briefly, each bundle is
+handled independently; there is no interaction between bundles from
+the perspective of applying definitions, inferences, or constraints,
+computing normal forms, or checking validity or equivalence.</p>
+
+<p> We model a general PROV instance, containing <span class="name">n</span> named bundles
+<span class="name">b<sub>1</sub>...b<sub>n</sub></span>, as a tuple <span class="name">(B<sub>0</sub>,[b<sub>1</sub>=B<sub>1</sub>,\ldots,b<sub>n</sub>=B<sub>n</sub>])</span> where TB is the set of
+statements of the toplevel bundle, and for each <span class="name">i, <span class="name">B<sub>i</sub></span> is the set of
+statements of bundle <span class="name">b<sub>i</sub></span>. This notation is shorthand for the
+following PROV-N syntax:</p>
+<pre>
+B<sub>0</sub>
+bundle b<sub>1</sub>
+ B<sub>1</sub>
+endBundle
+...
+bundle b<sub>n</sub>
+ B<sub>n</sub>
+endBundle
+</pre>
+
+<p> The <a>normal form</a> of a general PROV instance
+(B<sub>0</sub>,[b<sub>1</sub>=B<sub>1</sub>,...,[b<sub>n</sub>=B<sub>n</sub>]) is (B'<sub>0</sub>,[b<sub>1</sub>=B'<sub>1</sub>,...,b<sub>n</sub>=B'<sub>n</sub>])
+where B'<sub>i</sub> is the normal
+form of B<sub>i</sub> for each i between 0 and n. </p>
+
+<p>A general PROV instance is <a>valid</a> if each of the bundles B<sub>0</sub>,
+..., B<sub>n</sub> are valid and none of the bundle identifiers b<sub>i</sub> are repeated.</p>
+
+<p>Two (valid) general PROV instances (B<sub>0</sub>,[b<sub>1</sub>=B<sub>1</sub>,...,b<sub>n</sub>=B<sub>n</sub>]) and
+(B'<sub>0</sub>,[b<sub>1</sub>'=B'<sub>1</sub>,...,b'_m=B'_m]) are <a>equivalent</a> if B<sub>0</sub> is
+equivalent to B'<sub>0</sub> and n = m and
+there exists a permutation P : n -> n such that for each i, b<sub>i</sub> =
+b'<sub>P(i)</sub> and B<sub>i</sub> is equivalent to B'<sub>P(i)</sub>.
+</p>
</section> <!-- bundle-constraints-->
+</section> <!-- normalization, validity, and equivalence -->
@@ -2322,10 +2379,22 @@
<ul>
<li> <dfn>antisymmetric</dfn>: A relation R over X is <a>antisymmetric</a> if
for any elements x, y of X, if x R y and y R x then x = y.</li>
+ <li> <dfn>asymmetric</dfn>: A relation R over X is <a>asymmetric</a> if
+ x R y and y R x do not hold for any elements x, y of X.</li>
+ <li> <dfn>irreflexive</dfn>: A relation R over X is <a>irreflexive</a> if
+ for x R x does not hold for any element x of X.</li>
<li> <dfn>reflexive</dfn>: A relation R over X is <a>reflexive</a> if
for any element x of X, we have x R x.</li>
- <li><dfn>strict</dfn>: The strict form of a partial order or
- preorder is the relation formed by excluding reflexive steps.
+ <li><dfn>partial order</dfn>: A partial order is a relation
+ that is <a>reflexive</a>, <a>antisymmetric</a>, and <a>transitive</a>.</li>
+ <li><dfn>preorder</dfn>: A preorder is a relation R that is
+ <a>reflexive</a> and <a>transitive</a>. (It is not necessarily antisymmetric,
+ meaning there can be cycles of distinct elements x1 R x2 R ... R
+ xn R x1.)</li>
+ <li><dfn>strict partial order</dfn>: A strict partial order is a
+ relation that is <a>irreflexive</a>, <a>asymmetric</a> and <a>transitive</a>.</li>
+ <li><dfn>strict preorder</dfn>: A strict preorder is a relation
+ that is <a>irreflexive</a> and <a>transitive</a>.</li>
<li> <dfn>symmetric</dfn>: A relation R over X is <a>symmetric</a> if
for any elements x, y of X, if x R y then y R x.</li>
<li> <dfn>transitive</dfn>: A relation R over X is <a>transitive</a> if