--- a/model/working-copy/wd5-prov-dm-constraints-revised.html Tue Apr 17 18:03:27 2012 +0100
+++ b/model/working-copy/wd5-prov-dm-constraints-revised.html Tue Apr 17 18:52:57 2012 +0100
@@ -38,12 +38,7 @@
"<a href=\"http://www.ditext.com/johnson/intro-3.html\"><cite>Logic: Part III</cite></a>."+
"1924. "+
"URL: <a href=\"http://www.ditext.com/johnson/intro-3.html\">http://www.ditext.com/johnson/intro-3.html</a>",
- "Lattices":
- "TODO"+
- "<a href=\"http://TODO\"><cite>TODO</cite></a>."+
- "YYYY. "+
- "URL: <a href=\"http://TODO\">http://TODO</a>",
- "PROV-SEM":
+ "PROV-SEM":
"James Cheney "+
"<a href=\"http://www.w3.org/2011/prov/wiki/FormalSemanticsStrawman\"><cite>Formal Semantics Strawman</cite></a>. "+
"2011, Work in progress. "+
@@ -90,7 +85,7 @@
// if your specification has a subtitle that goes below the main
// formal title, define it here
- subtitle : "Initial document for discussion, WD5",
+ subtitle : "WD5, being updated following internal review",
// if you wish the publication date to be other than today, set this
//publishDate: "2012-02-01",
@@ -445,6 +440,28 @@
such that <span class="name">wasGeneratedBy(-,e,a1,-,attrs1)</span> and <span class="name">used(-,a2,e,-,attrs2)</span> hold.
</div>
+<p>The relationship <span class="name">wasInformedBy</span> is not
+transitive. Indeed, consider the following descriptions.</p>
+<pre class="codeexample">
+wasInformedBy(a2,a1)
+wasInformedBy(a3,a2)
+</pre>
+<p> We cannot infer <span class="name">wasInformedBy(a3,a1)</span> from these expressions. 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>
+and used by <span class="name">a2</span>. Likewise, from <span class="name">wasInformedBy(a3,a2)</span>, we know that there exists <span class="name">e2</span> such that <span
+class="name">e2</span> was generated by <span class="name">a2</span> and used by <span class="name">a3</span>. The following illustration shows a case for which transitivity cannot hold. The
+horizontal axis represents the event line. We see that <span class="name">e1</span> was generated after <span class="name">e2</span> was used. Furthermore, the illustration also shows that
+<span class="name">a3</span> completes before <span class="name">a1</span>. So it is impossible for <span class="name">a3</span> to have used an entity generated by <span
+class="name">a1</span>.</p>
+
+<div style="text-align: center;">
+<figure>
+<img src="images/informedByNonTransitive.png" alt="non transitivity of wasInformedBy" />
+<figcaption>Counter-example for transitivity of wasInformedBy</figcaption>
+</figure>
+</div>
+
<p>Start of <span class="name">a2</span> by activity <span
class="name">a1</span> is <a title="definition">defined</a> as follows.</p>
@@ -483,16 +500,27 @@
</pre>
</div>
+<p> Responsibility relates agents where one agent acts on behalf of
+another, in the context of some activity. The supervising agent
+delegates some responsibility for part of the activity to the
+subordinate agent, while retaining some responsibility for the overall
+activity. </p>
+
+
<div class="note">
- There should probably be some inferences about responsibility/actedOnBehalfOf.
- </div>
+ @@TODO: Could this be an inference? Does it imply that
+ a1 is associated with all activities a2 is associated with?
+ </div></p>
+
+
</section>
<section>
<h3>Component 3: Derivations</h3>
-<section>
-<h4>Derivation</h4>
- <p>A further inference is permitted from derivations with an explicit activity and no usage: </p>
+
+
+ <p>Derivations with an explicit activity and no usage admit the
+ following inference: </p>
<div class='inference' id='derivation-use'>
<p>Given an activity <span class="name">a</span>, entities denoted by <span class="name">e1</span> and <span class="name">e2</span>,
<span class='conditional'>IF</span> <span class="name">wasDerivedFrom(-,e2,e1, a, -)</span> and <span class="name">wasGeneratedBy(-,e2,a,-,-)</span> hold, <span
@@ -502,15 +530,38 @@
(see <a href="#generation-uniqueness">generation-uniqueness</a>). Hence, this activity is also the one referred to by the usage of <span class="name">e1</span>.
</p>
+<div class="note">
+ There is some redundancy in the following discussion.
+ </div>
<p>The converse inference does not hold.
From <span class="name">wasDerivedFrom(e2,e1)</span> and <span class="name">used(a,e1,-)</span>, one cannot
derive <span class="name">wasGeneratedBy(e2,a,-)</span> because identifier <span class="name">e1</span> may occur in usages performed by many activities, which may have not generated the entity denoted by <span class="name">e2</span>.</p>
-
-</section>
-<section>
-<h4>Revision</h4>
+ <p>
+Note that derivation cannot in general be inferred from the existence
+of related usage and generation events. Indeed, when a generation <span class="name">wasGeneratedBy(g, e2, a, -, attrs2)</span>
+<a>precedes</a> <span class="name">used(u, a, e1, -, attrs1)</span>, for
+some <span class="name">e1</span>, <span class="name">e2</span>, <span class="name">attrs1</span>, <span class="name">attrs2</span>, and <span class="name">a</span>, one
+cannot infer derivation <span class="name">wasDerivedFrom(e2, e1, a, g, u)</span>
+or <span class="name">wasDerivedFrom(e2,e1)</span> since
+ <span class="name">e2</span> cannot possibly be derived from
+ <span class="name">e1</span>, given the creation of <span class="name">e2</span> <a>precedes</a> the use
+of <span class="name">e1</span>. That is, if <span class="name">e1</span> is generated
+by an activity before <span class="name">e2</span> is used, then
+obviously <span class="name">e2</span> cannot have been derived from
+<span class="name">e1</span>. However, even if <span
+class="name">e2</span> happens used before <span class="name">e1</span>
+is generated, it is not safe to assume that <span
+class="name">e2</span> was derived from <span class="name">e1</span>.
+</p>
+
+<p> Derivation is not defined to be transitive. Domain-specific specializations of derivation may be defined in such a way that the transitivity property
+holds.</p>
+
+
+
+
<p>A revision needs to satisfy the following constraint, linking the two entities by a derivation, and stating them to be a specialization of a third entity.</p>
@@ -534,11 +585,8 @@
may satisfy <span class="name">wasDerivedFrom(e2,e1)</span> without being a variant of
each other.
</p>
-</section>
-
-<section>
-<h4>Quotation</h4>
-<div class="note">
+
+ <div class="note">
Motivation for quotation inference
</div>
<div class='inference' id='quotation-implication'>
@@ -555,13 +603,7 @@
<p>
-<div id="optional-attributes6">In a quotation of the form <span class="name">wasQuotedFrom(e2,e1,-,-,attrs)</span>, the absence of an agent means: either no agent exists, or an agent exists but it is not identified.</div>
-
-</section>
-
-
-<section id="term-traceability">
-<h3>Traceability</h3>
+
<p>Traceability allows an entity to be transitively linked to another entity it is derived from, to an agent it is attributed to, or another agent having some responsibility, or a trigger of an activity that generated it.</p>
@@ -603,7 +645,6 @@
allow us to infer anything about the attributes of the related
entities, agents or events.
</p>
-</section>
</section>
@@ -612,11 +653,14 @@
<section>
<h3>Component 4: Alternate Entities</h3>
<div class="note">TODO: There is currently no consensus what inferences on
- alternate or specialization should be assumed.
- </div>
-
- The relation <span class='name'>alternateOf</span> is an equivalence relation: reflexive,
- transitive and symmetric.
+ alternate or specialization should be assumed. The following
+ section lists possible inferences that may or may not be adopted. Section is under review, pending ISSUE-29.
+</div>
+
+
+ <p>The relation <span class='name'>alternateOf</span> is an equivalence relation: <a>reflexive</a>,
+ <a>transitive</a> and <a>symmetric</a>.</p>
+
<div class='inference' id="alternate-reflexive">
For any entity <span class='name'>e</span>, we have <span class='name'>alternateOf(e,e)</span>.
</div>
@@ -631,14 +675,24 @@
For any entity <span class='name'>e1</span>, <span class='name'>e2</span>, <span class='conditional'>IF</span> <span class='name'>alternateOf(e1,e2)</span> <span class='conditional'>THEN</span> <span class='name'>alternateOf(e2,e1)</span>.
</div>
-Similarly, specialization is a partial order: it is reflexive and
- transitive.
+<p>Similarly, specialization is a partial order: it is <a>reflexive</a>,
+ <a>anti-symmetric</a> and
+ <a>transitive</a>.</p>
<div class='inference' id="specialization-reflexive">
For any entity <span class='name'>e</span>, we
have <span class='name'>specializationOf(e,e)</span>.
</div>
-
+<div class='inference' id="specialization-transitive">
+ For any
+ entities <span class='name'>e1</span>, <span
+ class='name'>e2</span>,
+ <span class='conditional'>IF</span>
+ <span class='name'>specializationOf(e1,e2)</span>
+ and
+ <span class='name'>specializationOf(e2,e1)</span> <span
+ class='conditional'>THEN</span> <span class='name'>e1 = e2</span>.
+ </div>
<div class='inference' id="specialization-transitive">
For any
entities <span class='name'>e1</span>, <span class='name'>e2</span>, <span class='name'>e3</span>, <span class='conditional'>IF</span> <span class='name'>specializationOf(e1,e2)</span>
@@ -648,7 +702,9 @@
- If one entity specializes another, then they are also alternates:
+ <p>Finally, if one entity specializes another, then they are also
+ alternates:</p>
+
<div class='inference' id="specialization-alternate">
For any entities <span class='name'>e1</span>, <span class='name'>e2</span>, <span class='conditional'>IF</span> <span class='name'>specializationOf(e1,e2)</span> <span class='conditional'>THEN</span> <span class='name'>alternateOf(e1,e2)</span>.
</div>
@@ -657,7 +713,105 @@
<div class="note">TODO: Possible inferences about attributes,
generation, invalidation?
</div>
+
+
+ <div class="note">
+ The following sections are retained from an older version, and are
+ not consistent with the above constraints. This will be revised
+ once the consensus on ISSUE-29 is clearer.
+ </div>
+ <section id="term-Specialization">
+<h3>Specialization</h3>
+
+
+<p>Specialization is <em>neither symmetric nor anti-symmetric</em>.
+</p>
+
+<div class="anexample" id="anexample-not-symmetric">
+"Alice's toyota car on fifth Avenue" is a specialization of "Alice's toyota car", but the converse does not hold.
+</div>
+
+<div class="anexample" id="anexample-specialization-not-anti-symmetric">
+anti-symmetric counter-example???
+</div>
+
+
+<p>Specialization is <em>transitive</em>. Indeed if <span
+class="name">specializationOf(e1,e2)</span> holds, then there is some
+common thing, say <span class="name">T1-2</span> they both refer to,
+and <span class="name">e1</span> is a more specific aspect of this
+thing than <span class="name">e2</span>. Likewise, if <span
+class="name">specializationOf(e2,e3)</span> holds, then there is some
+common thing, say <span class="name">T2-3</span> they both refer to, and <span class="name">e2</span> is a more specific aspect of this
+thing than <span class="name">e3</span>. The things <span
+class="name">T1-2</span> and <span class="name">T2-3</span> are the
+same since <span class="name">e2</span> is an aspect of both of them,
+so <span
+class="name">specializationOf(e1,e3)</span> follows since <span class="name">e1<span class="name"> and <span class="name">e3<span class="name">
+are aspects fo the same thing and <span class="name">e1<span class="name"> is more specific than <span class="name">e3<span class="name">. </p>
+
+
+<div class="anexample" id="anexample-specialization-is-transitive">
+A specialization of "this email message" would be, for example, the "printed version on my desk", which is a specialization of "my thoughts on this email thread". So, the "printed version on my desk" is also a specialization "my thoughts on this email thread".
+</div>
+
+
+</section>
+
+<section id="term-Alternate">
+<h3>Alternate</h3>
+</section>
+
+
+<p>Alternate not is <em>reflexive</em>. Indeed, <span class="name">alternate(e,e)</span> does not hold for any arbitrary entity <span class="name">e</span> since <span class="name">e</span> may not be a specialization of another entity.</p>
+
+
+<p>Alternate is <em>symmetric</em>. Indeed, if <span class="name">alternate(e1,e2)</span> holds,
+then there exists an unspecified entity <span class="name">e</span>, such that
+both <span class="name">e1</span> and <span class="name">e2</span> are specialization of <span class="name">e</span>.
+Therefore, <span class="name">alternate(e2,e1)</span> also holds.
+</p>
+
+
+
+<p>Alternate is <em>not transitive</em>. Indeed, if <span class="name">alternate(e1,e2)</span> holds,
+then there exists an unspecified entity <span class="name">e1-2</span>, such that
+both <span class="name">e1</span> and <span class="name">e2</span> are specialization of <span class="name">e1-2</span>.
+Likewise, if <span class="name">alternate(e2,e3)</span> holds,
+then there exists an unspecified entity <span class="name">e2-3</span>, such that
+both <span class="name">e2</span> and <span class="name">e3</span> are specialization of <span class="name">e2-3</span>.
+It does not imply that there is a common entity <span class="name">e1-3</span>
+that both <span class="name">e1</span> and <span class="name">e3</span> specialize.
+</p>
+
+
+<div class="anexample" id="anexample-alternate-not-transitive1">
+<p>At 6pm, the customer in a chair is a woman in a red dress, who happens to be Alice. After she leaves, another customer arrives at 7pm, a man with glasses, who happens to be Bob. Transitivity does not hold since the <span class="name">womanInRedDress\</span> is not alternate of <span class="name">customerInChairAt7pm</span>.
+<pre>
+alternate(womanInRedDress,customerInChairAt6pm)
+specialization(customerInChairAt6pm,Alice)
+specialization(womanInRedDress,Alice)
+
+alternate(manWithGlasses,customerInChairAt7pm)
+specialization(customerInChairAt7pm,Bob)
+specialization(manWithGlasses,Bob)
+
+alternate(customerInChairAt6pm, customerInChairAt7pm)
+specialization(customerInChairAt6pm, customerInChair)
+specialization(customerInChairAt7pm, customerInChair)
+</pre>
+</div>
+
+<p>The above example shows that <span class="name">customerInChairAt6pm</span> and <span class="name">customerInChairAt7pm</span> are two alternate entities that have no overlap, while <span class="name">womanInRedDress</span> and <span class="name">customerInChairAt6pm</span> do overlap.
+The following example illustrates another case of non-overlapping alternate entities.
+</p>
+
+<div class="anexample">Two copies of the same book, where copy A was destroyed before copy B was made.</div>
+
+
+</section>
+
</section>
</section>
@@ -666,12 +820,19 @@
<section id="equivalence">
<h2>Equivalence</h2>
-For the purpose of checking inferences and constraints, we define a
+
+ For the purpose of checking inferences and constraints, we define a
notion of <a>equivalence</a> of PROV-DM instances. Equivalence is
-defined as follows:
+has the following characteristics:
<ul>
+ <li>Missing attributes that are interpreted as omitted values are
+ handled by generating a fresh
+ identifier for the omitted value.
+ </li>
+ <li> Redundant expressions are merged according to uniqueness
+ constraints. </li>
<li>
The order of provenance expressions is irrelevant to the meaning of a PROV-DM instance. That is, a
PROV-DM instance is equivalent to any other instance obtained by
@@ -685,15 +846,69 @@
<li>Equivalence is reflexive, symmetric, and transitive.</li>
</ul>
+ <section id="optional-attributes">
+ <h3>Optional Attributes</h4>
+
+<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">PROV-DM allows for some attributes to
+ be optionally expressed. Unless otherwise specified, when an
+ optional attribute is not present in a description, some value
+ SHOULD be assumed to exist for this attribute, though it is not
+ known which.
+
+ The only exceptions are:
+ <ul>
+ <li><span id="optional-attributes2">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></li>
+ <li><span id="optional-attributes3">Activities also allow for an optional end time attribute. If both are specified, they MUST be the same, as expressed by the following constraint.</span></li>
+ <li>
+ <div id="optional-attributes6">In a quotation of the form <span class="name">wasQuotedFrom(e2,e1,-,-,attrs)</span>, the absence of an agent means: either no agent exists, or an agent exists but it is not identified.</div>
+</li>
+<div id="optional-attributes4">
+<li><p>In an association of the form <span class="name">wasAssociatedWith(a, ag, -, attr)</span>, the absence of a plan means: either no plan exists, or a plan exists but it is not identified.</p>
+
+
+<p>In an association of the form <span class="name">wasAssociatedWith(a, -, pl, attr)</span>, an agent exists but it is not identified.</p>
+</div>
+</li>
+<li><div id="optional-activity">
+<p>In a a delegation of the form <span class="name">actedOnBehalfOf(a,
+ ag2, ag1, -, attr)</span>, the absence of an activity means that
+ <span class="name">a2</span> acts on behalf of <span
+ class="name">a1</span> for all activities with which <span
+ class="name">a2</span> is
+ associated.
+</div></li>
+ </ul>
+</div>
+
+</section>
+
+<section id="normalization">
+<h3>Normalization</h3>
+
+
<p>
We define the <dfn>normal form</dfn> of a PROV-DM instance as the set
-of provenance expressions resulting from combining all of the
+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-DM instances are
-<dfn>equivalent</dfn> if, after applying all applicable inference
-rules, they yield the same set of provenance expressions.
+<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
@@ -737,6 +952,28 @@
</li>
</ul>
+<p>The PROV-DM data model is implicitly based on a notion of <dfn
+ id="dfn-event">instantaneous event</dfn>s (or just <a
+ title="instantaneous event">event</a>s), that mark
+transitions in the world. Events include generation, usage, or
+invalidation of entities, as well as starting or ending of activities. This
+notion of event is not first-class in the data model, but it is useful
+for explaining its other concepts and its semantics [[PROV-SEM]].
+Thus, events help justify <i>inferences</i> on provenance as well as
+<i>validity</i> constraints indicating when provenance is self-consistent. In <a href="#section-event-time" class="sectionRef"></a> we
+discuss the motivation for <a title="instantaneous event">instantaneous events</a>
+and their relationship to time in greater detail.</p>
+
+<p> PROV-DM
+identifies five kinds of <a title="instantaneous event">instantaneous events</a>, namely <a>entity generation
+event</a>, <a>entity usage event</a>, <a>entity invalidation event</a>, <a>activity start event</a>
+and <a>activity end event</a>. PROV-DM adopts Lamport's clock
+assumptions [[CLOCK]] in the form of a reflexive, transitive partial order <a>follows</a>
+(and its inverse <a>precedes</a>) between <a title="instantaneous event">instantaneous events</a>. Furthermore,
+PROV-DM assumes the existence of a mapping from <a title="instantaneous event">instantaneous events</a> to time clocks,
+though the actual mapping is not in scope of this specification.</p>
+
+
<div class="note">
TODO: More about what it means for constraints to be satisfied;
constraint template(s)
@@ -744,10 +981,7 @@
<section id="structural-constraints">
<h3>Uniqueness Constraints</h3>
-<div class="note">
- TODO Merge material from <a href="#structural-constraints"
- class="sectionRef"></a> and <a href="#definitional-constraints" class="sectionRef"></a>.
- </div>
+
<div class="note">
Attribute uniqueness constraints?
</div>
@@ -821,7 +1055,10 @@
</p>
<div class='constraint' id='unique-endTime'>
-<span class='conditional'>IF</span> <span class="name">activity(a,t1,t2,-)</span> and <span class="name">wasEndedBy(id,a,e,t,-)</span>, <span class='conditional'>THEN</span> <span class="name">t</span>=<span class="name">t1</span>.
+<span class='conditional'>IF</span> <span
+ class="name">activity(a,t1,t2,-)</span> and <span
+ class="name">wasEndedBy(id,a,e,t,-)</span>, <span
+ class='conditional'>THEN</span> <span class="name">t</span> = <span class="name">t2</span>.
</div>
@@ -851,16 +1088,6 @@
<section id="event-ordering-constraints">
<h3>Event Ordering Constraints</h3>
-<p>Section <a href="#section-time-event">section-time-event</a>
-introduces a notion of <a title="instantaneous event">instantaneous event</a>
-marking changes in the world, in its activities and entities. PROV-DM
-identifies five kinds of <a title="instantaneous event">instantaneous events</a>, namely <a>entity generation
-event</a>, <a>entity usage event</a>, <a>entity invalidation event</a>, <a>activity start event</a>
-and <a>activity end event</a>. PROV-DM adopts Lamport's clock
-assumptions [[CLOCK]] in the form of a reflexive, transitive partial order <a>follows</a>
-(and its inverse <a>precedes</a>) between <a title="instantaneous event">instantaneous events</a>. Furthermore,
-PROV-DM assumes the existence of a mapping from <a title="instantaneous event">instantaneous events</a> to time clocks,
-though the actual mapping is not in scope of this specification.</p>
<p>Given that provenance consists of a description of past entities
and activities, <a>valid</a> provenance descriptions MUST
@@ -875,6 +1102,34 @@
set of instantaneous event ordering constraints. </p>
+<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>.
+</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 either the two events are equal or <span
+class="name">e1</span> happened 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 either the two events are equal or <span
+class="name">e1</span> happened after <span
+class="name">e2</span>. Both relations are partial orders, meaning
+that they are reflexive, transitive, and antisymmetric.</p>
+
+<div class="note"> Define reflexivity, transitivity
+and antisymmetry in glossary. Also, do we want to allow an event to
+ "precede" itself?
+</div>
+
+<div class="note">
+ The following discussion is unclear: what is being said here, and why?
+ </div>
+
<p>PROV-DM also allows for time observations to be inserted in
specific provenance descriptions, for each of the five kinds
of <a title="instantaneous event">instantaneous events</a> introduced in this specification. The
@@ -934,6 +1189,8 @@
start and endpoints of its lifetime.
</p>
+<hr />
+
<p>The existence of an activity implies that the <a>activity start event</a> always <a>precedes</a> the corresponding <a>activity end
event</a>. This is
illustrated by Subfigure <a href="#constraint-summary">constraint-summary</a> (a) and expressed by constraint <a href="#start-precedes-end">start-precedes-end</a>.</p>
@@ -951,7 +1208,10 @@
<span class="name">start</span>
<a>precedes</a>
<span class="name">end</span>.
-</div>
+</div>
+
+<hr />
+
<p>A usage implies ordering of <a title="instantaneous event">events</a>, since the <a title="entity usage event">usage event</a> had to occur during the associated activity. This is
illustrated by Subfigure <a href="#constraint-summary">constraint-summary</a> (c) and expressed by constraint <a href="#usage-within-activity">usage-within-activity</a>.</p>
@@ -988,6 +1248,7 @@
</ol>
</div>
+<hr />
<p>A generation implies ordering of <a title="instantaneous event">events</a>, since the <a title="entity generation event">generation event</a> had to occur during the associated activity. This is
@@ -1027,6 +1288,8 @@
</ol>
</div>
+<hr />
+
<p>Communication between two activities <span class="name">a1</span> and <span class="name">a2</span> also implies ordering of <a
title="instantaneous event">events</a>, since some entity must have been generated by the former and used by the latter, which implies that the start event of <span class="name">a1</span>
cannot follow the end event of <span class="name">a2</span>. This is
@@ -1053,6 +1316,8 @@
</div>
+<hr />
+
<p>Start of <span class="name">a2</span> by activity <span class="name">a1</span> also implies ordering of <a
title="instantaneous event">events</a>, since <span class="name">a1</span> must have been active before <span class="name">a2</span> started. This is
illustrated by Subfigure <a href="#constraint-summary">constraint-summary</a> (h) and expressed by constraint <a href="#wasStartedBy-ordering">wasStartedBy-ordering</a>.</p>
@@ -1089,7 +1354,8 @@
can be used, revised, or other entities can be derived from them, and
finally are invalidated.
</p>
-</p>
+<hr />
+
<p>Generation of an entity precedes its invalidation. (This
follows from other constraints if the entity is used, but we state it
explicitly to cover the case of an entity that is generated and
@@ -1110,6 +1376,7 @@
<a>precedes</a>
<span class="name">inv</span>.
</div>
+<hr />
<p> A usage and a generation for a given entity implies ordering of <a title="instantaneous event">events</a>, since the <a title="entity generation
event">generation event</a> had to precede the <a title="entity usage event">usage event</a>. This is
@@ -1129,6 +1396,7 @@
<span class="name">use</span>.
</div>
+<hr />
<p>All usages of an entity precede its invalidation, which is captured by constraint <a href="#usage-precedes-invalidation">usage-precedes-invalidation</a> (without any explicit graphical representation).</p>
@@ -1149,6 +1417,7 @@
+<hr />
@@ -1182,6 +1451,7 @@
<span class="name">u1</span>.
</div>
+<hr />
<p>When the usage is unknown, a similar constraint exists, except that the constraint refers to its
generation event, as
@@ -1235,6 +1505,7 @@
</figure>
</div>
+<hr />
<p>The agent that started an activity must exist before the activity starts.
This is
@@ -1276,6 +1547,7 @@
</li>
</ol>
</div>
+<hr />
<p> Similarly, if an agent is associated with an activity then the
agent must exist before the activity starts and persist until the
@@ -1317,6 +1589,7 @@
</ol>
</div>
+<hr />
<p>An activity that was associated with an agent must have some overlap with the agent. The agent may be generated, or may only become associated with the activity, after the activity start: so, the agent is required to exist before the activity end. Likewise, the agent may be destructed, or may terminate its association with the activity, before the activity end: hence, the agent invalidation is required to happen after the activity start.
This is
@@ -1359,6 +1632,7 @@
</ol>
</div>
+<hr />
<p>An entity that was attributed to an agent must have some overlap
with the agent. The agent is required to exist before the entity
@@ -1405,6 +1679,8 @@
</ol>
</div>
+<hr />
+
<p>For responsibility, two agents need to have some overlap in their lifetime.</p>
@@ -1440,7 +1716,11 @@
<section id="collection-constraints">
<h2>Collection Constraints</h2>
-
+<div class="note">
+ Work on collections and on these constraints is deferred until after
+ the next working draft, so this section may not be stable.
+ </div>
+
<p>Membership is a convenience notation, since it can be expressed in terms of an insertion into some collection. The membership definition is formalized by constraint <a href="#membership-as-insertion">membership-as-insertion</a>.</p>
<div class='definition' id='membership-as-insertion'>
@@ -1621,10 +1901,6 @@
</div>
-->
-<p>
- <div class="structural-forward">
- See Section <a href="#structural-constraints">structural-constraints</a> for a structural constraint on accounts
- </div>
<p>In some cases, there may be a requirement for two different
@@ -1639,14 +1915,6 @@
</pre>
</div>
-<div class="note">
- Following text transplanted from structural constraints section.
- </div>
-
- <p>
-An account is said to be structurally well-formed if
-it satisfies the constraint <a href="#generation-uniqueness">generation-uniqueness</a>. If an account is structurally well-formed, it supports the inference <a
-href="#derivation-use">derivation-use</a>.</p>
<div class='note'>
Since we are not specifying ways to take the union of two accounts,
@@ -1666,7 +1934,7 @@
<div class="note">
- Material transplanted from structural well-formedness constraints section.
+ Material transplanted from old structural well-formedness constraints section.
This example isn't very clear, since the sub-workflow-ness isn't
represented in the data. According to what was written above, we
@@ -1748,7 +2016,7 @@
constraints of <a href="#constraints" class="sectionRef"></a> are
satisfied on the <a>normal form</a> of the instance.</li>
<li> When producing provenance meant for other applications to
- use, the application SHOULD produce valid provenance. </li>
+ use, the application SHOULD produce <a>valid</a> provenance. </li>
</ul>
<div class="note">
Should we specify a way for PROV-DM instances to say whether they
@@ -1761,7 +2029,15 @@
<section id='rationale' class="informative">
<h2>Rationale for inferences and constraints</h2>
-
+<div class="note"> This section collects all of the explanatory
+ material that I was not certain how to interpret as an unambiguous
+ inference or constraint. Some of these observations may need to be folded
+ into the explanatory text in respective sections (for example for
+ events,
+ accounts or collections).
+
+ Editing is also needed to decrease redundancy.
+ </div>
<section id='section-attributes'>
<h4>Entities and Attributes</h4>
@@ -1819,12 +2095,6 @@
specialization and alternate can be used to link such entities.</p>
-<div class="note">
- The following statement should be put somewhere normative, ideally
- in PROV-DM itself, to clarify the rules about optional attributes.
- </div>
-
-<div id="optional-attributes1">PROV-DM allows for some attributes to be optionally expressed. Unless otherwise specified, when an optional attribute is not present in a description, some value SHOULD be assumed to exist for this attribute, though it is not known which. </div>
@@ -1862,15 +2132,89 @@
<p>
However, the attributes of entities have special meaning because they
are considered to be fixed aspects
-of underlying, changing things. This means, for example, that
-if two entities have overlapping lifetimes and they have some
-attributes in common, those attributes SHOULD match. </p>
+of underlying, changing things. This motivates constraints on
+<span class="name">alternateOf</span> and <span class="name">specializationOf</span> relating the attribute values of
+different entities.
+</p>
<div class="note">
- @@TODO:
-Constraints for this?
+ TODO:
+Constraints on alternateOf/specializationOf for this?
</div>
+
+ <div class="note">
+TODO: Further discussion of entities moved from the old "Definitional
+ constraints" section. Should merge with the surrounding
+ discussion to avoid repetition.
+ </div>
+<p>
+An <dfn>entity</dfn> is a thing one wants to provide provenance for
+and whose situation in the world is described by some attribute-value
+pairs. An entity's attribute-value pairs are established as part of
+the entity description and their values remain unchanged for the
+lifetime of the entity. An entity's attribute-value pairs are expected
+to describe the entity's situation and (partial) state during an
+entity's <a title="characterization interval">characterization interval</a>.</p>
+
+<p>If an entity's situation or state changes, this may result in its description being invalid, because one or more attribute-value pairs no longer hold. In that case, from the PROV viewpoint, there exists a new entity, which needs to be given a distinct identifier, and associated with the attribute-value pairs that reflect its new situation or state.</p>
+
+
+
+Further considerations:
+<ul>
+<li>In order to describe the provenance of something during an interval over which
+ relevant attributes of the thing are not fixed, it is required to
+ create multiple entities, each with its own identifier, <a
+ title="characterization interval">characterization interval</a>, and
+ fixed attributes, and express
+ dependencies between the various entities using events.
+ For example, if we want to describe the provenance of several
+ versions of a document, involving attributes such as authorship that
+ change over time, we need different entities for the versions linked
+ by appropriate generation, usage, revision, and invalidation events.
+</li>
+
+<li>There is no assumption that the set of attributes is complete, nor
+that the attributes are independent or orthogonal of each other.</li>
+<li>There is no assumption that the attributes of an entity uniquely
+identify it. Two different entities that are aspects of different
+things can have the same attributes.</li>
+<li>A <a title="characterization interval">characterization interval</a> may collapse into a single instant.</li>
+</ul>
+
</section>
+<section>
+<h3>Activities</h3>
+
+<div class="note>
+ TODO: Further discussion of activities moved from old "Definitional
+ constraints and inferences" section. Edit to avoid repeating information.
+
+
+
+<p>An activity is delimited by its <a title="activity start event">start</a> and its <a title="activity end event">end</a> events; hence, it occurs over
+an interval delimited by two <a title="instantaneous event">instantaneous
+events</a>. However, an activity record need not mention start or end time information, because they may not be known.
+An activity's attribute-value pairs are expected to describe the activity's situation during its interval, i.e. an interval between two instantaneous events, namely its <a title="activity start event">start</a> event and its <a title="activity end event">end</a> event.
+</p>
+
+
+<p>Further considerations:</p>
+<ul>
+<li>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 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 distinction is similar to the distinction between
+'continuant' and 'occurrent' in logic [[Logic]].</li>
+</ul>
+
+
+
+</section>
<section id="representation-term-assertion-inference">
@@ -1888,7 +2232,8 @@
<p>The data model is designed to capture activities that happened in the past, as opposed to activities
that may or will happen.
However, this distinction is not formally enforced.
-Therefore, all PROV-DM descriptions SHOULD be interpreted as what has happened, as opposed to what may or will happen.</p>
+Therefore, PROV-DM descriptions are intended to be interpreted as what
+has happened, as opposed to what may or will happen.</p>
@@ -1917,15 +2262,6 @@
<h4>Events and Time</h4>
-<p>The PROV-DM data model is implicitly based on a notion of <dfn
- id="dfn-event">instantaneous event</dfn>s (or just <a
- title="instantaneous event">event</a>s), that mark
-transitions in the world. Events include generation, usage, or
-invalidation of entities, as well as starting or ending of activities. This
-notion of event is not first-class in the data model, but it is useful
-for explaining its other concepts and its semantics [[PROV-SEM]].
-Thus, events help justify <i>inferences</i> on provenance as well as
-<i>validity</i> constraints indicating when provenance is self-consistent. </p>
<p>Time is critical in the context of provenance, since it can help corroborate provenance claims. For instance, if an entity is claimed to be obtained by transforming another, then the
@@ -1962,30 +2298,7 @@
<section id="event-ordering">
<h4>Event Ordering</h4>
-<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>.
-</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 either the two events are equal or <span
-class="name">e1</span> happened 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 either the two events are equal or <span
-class="name">e1</span> happened after <span
-class="name">e2</span>. Both relations are partial orders, meaning
-that they are reflexive, transitive, and antisymmetric
-[[Lattices]].</p>
-
-<div class="note"> Define reflexivity, transitivity
-and antisymmetry in glossary. Also, do we want to allow an event to
- "precede" itself?
-</div>
+
<div class="note">
The following paragraphs are unclear and need to be revised, to
@@ -1995,7 +2308,7 @@
then how can implementations check that event ordering constraints
are satisfied?
</div>
-<p> How such a partial order is implemented in practice is beyond the scope
+<p> How the <a>precedes</a> partial order is implemented in practice is beyond the scope
of this specification. This specification only assumes that
each <a title="instantaneous event">instantaneous event</a> can be mapped to an instant in some form of
timeline. The actual mapping is not in scope of this
@@ -2028,7 +2341,6 @@
<section id="types-of-events">
<h4>Types of Events</h4>
-
<p>Five kinds of <a title="instantaneous event">instantaneous events</a> are used
for the PROV-DM data model. The <strong>activity start</strong> and
<strong>activity end</strong> events delimit the beginning and the end
@@ -2046,12 +2358,17 @@
<p>An <dfn id="dfn-usage-event">entity usage event</dfn> is the <a
title="instantaneous event">instantaneous event</a> that marks the first instant of
-an entity's consumption timespan by an activity.</p>
+an entity's consumption timespan by an activity. Before this instant
+the entity had not begun to be used by the activity.</p>
<p>An <dfn id="dfn-generation-event">entity generation event</dfn> is the <a title="instantaneous event">instantaneous event</a> that marks the final instant of an entity's creation timespan, after which
-it is available for use.</p>
-
-<p>An <dfn id="dfn-invalidation-event">entity invalidation event</dfn> is the <a title="instantaneous event">instantaneous event</a> that marks the initial instant of the destruction, invalidation, or cessation of an entity, after which the entity is no longer available for use.</p>
+it is available for use. The entity did not exist before this event.</p>
+
+<p>An <dfn id="dfn-invalidation-event">entity invalidation event</dfn>
+is the <a title="instantaneous event">instantaneous event</a> that
+marks the initial instant of the destruction, invalidation, or
+cessation of an entity, after which the entity is no longer available
+for use. The entity no longer exists after this event.</p>
</section>
@@ -2062,6 +2379,12 @@
<section id="account-section">
<h3>Account</h3>
+<div class="note">
+ Some of this discussion may belong in the account constraint section
+ as motivation, or as formal constraints/inferences. In particular,
+ the MUST, MAY, SHOULD statements should be clarified and put into
+ the normative section.
+ </div>
<p>It is common for multiple provenance records to co-exist. For
instance, when emailing a file, there could be a provenance record
@@ -2100,7 +2423,10 @@
</div>
<p>
-There is no construct in PROV-DM to create such bundles of descriptions. Instead, it is assumed that some mechanism, outside PROV-DM can create them. However, from a provenance viewpoint, such accounts are things we may want to describe the provenance of. In order to be able to do so, we need to see accounts as entities, whose origin can be described using PROV-DM vocabulary. Thus, PROV-DM introduces the reserved type <span class="name">Account</span>.
+There is no construct in PROV-DM to create such bundles of
+descriptions. Instead, it is assumed that some mechanism, outside
+PROV-DM can create them. However, from a provenance viewpoint, such
+accounts are things whose provenance we may want to describe. In order to be able to do so, we need to see accounts as entities, whose origin can be described using PROV-DM vocabulary. Thus, PROV-DM introduces the reserved type <span class="name">Account</span>.
</p>
</section>
@@ -2108,657 +2434,6 @@
-<section id="definitional-constraints">
-<h2>[OLD] Definitional constraints and inferences</h2>
-
-<div class="Note">
- This material is out of date. All constraints from it have been
- moved to the main body.</div>
-
-
- <section id="component1">
-<h3>Component 1: Entities and Activities</h3>
-
- <section id="term-Entity">
-
-<h4>Entity</h4>
-
-
-<p>
-An <dfn>entity</dfn> is a thing one wants to provide provenance for
-and whose situation in the world is described by some attribute-value
-pairs. An entity's attribute-value pairs are established as part of
-the entity description and their values remain unchanged for the
-lifetime of the entity. An entity's attribute-value pairs are expected
-to describe the entity's situation and (partial) state during an
-entity's <a title="characterization interval">characterization interval</a>.</p>
-
-<p>If an entity's situation or state changes, this may result in its description being invalid, because one or more attribute-value pairs no longer hold. In that case, from the PROV viewpoint, there exists a new entity, which needs to be given a distinct identifier, and associated with the attribute-value pairs that reflect its new situation or state.</p>
-
-
-
-Further considerations:
-<ul>
-<li>In order to describe the provenance of something during an interval over which
- relevant attributes of the thing are not fixed, it is required to
- create multiple entities, each with its own identifier, <a
- title="characterization interval">characterization interval</a>, and
- fixed attributes, and express
- dependencies between the various entities using events.
- For example, if we want to describe the provenance of several
- versions of a document, involving attributes such as authorship that
- change over time, we need different entities for the versions linked
- by appropriate generation, usage, revision, and invalidation events.
-</li>
-
-<li>There is no assumption that the set of attributes is complete, nor
-that the attributes are independent or orthogonal of each other.</li>
-<li>There is no assumption that the attributes of an entity uniquely
-identify it. Two different entities that are aspects of different
-things can have the same attributes.</li>
-<li>A <a title="characterization interval">characterization interval</a> may collapse into a single instant.</li>
-</ul>
-
-
-<div class="interpretation-forward">
-For the interpretation of an entity, see <a href="#usage-precedes-invalidation">usage-precedes-invalidation</a>.
-</div>
-
-
-
-</section>
-
- <section id="term-Activity">
-
-<h3>Activity</h3>
-
-
-
-<p>An activity is delimited by its <a title="activity start event">start</a> and its <a title="activity end event">end</a> events; hence, it occurs over
-an interval delimited by two <a title="instantaneous event">instantaneous
-events</a>. However, an activity record need not mention start or end time information, because they may not be known.
-An activity's attribute-value pairs are expected to describe the activity's situation during its interval, i.e. an interval between two instantaneous events, namely its <a title="activity start event">start</a> event and its <a title="activity end event">end</a> event.
-</p>
-
-<div class="interpretation-forward">
-For the interpretation of an activity, see <a href="#start-precedes-end">start-precedes-end</a>.
-</div>
-
-<p>Further considerations:</p>
-<ul>
-<li>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 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 distinction is similar to the distinction between
-'continuant' and 'occurrent' in logic [[Logic]].</li>
-</ul>
-
-
-
-</section>
-
-<section id="term-Generation">
-<h4>Generation</h4>
-<div class="note">
- ISSUE-346 (BLOCKING): Distinction between constraints,
- interpretations, inferences not clear and hard to follow in text
- here.
-
- Navigation links among constraints, inferences, and definitions are
- broken or confusing. Section to be reorganized.
- </div>
-
-<p>A <dfn id="dfn-Generation">generation</dfn> is an <a title="instantaneous event">instantaneous event</a>, the completed creation of a new
-entity by an activity. This entity becomes available for usage after this <a title="instantaneous event">instantaneous
-event</a>. This entity did not exist before creation.
-Generation events can have attributes that describe how the entity was
-generated by the activity..</p>
-
-
-
-
-<p>
-A generation's identifier is OPTIONAL. It MUST be used when annotating generations or when defining
-derivations (see <a href="#Derivation-Relation">Derivation</a>).
-</p>
-
-
-<div class="interpretation-forward">
-For the interpretation of a generation, see <a href="#generation-within-activity">generation-within-activity</a>.
-</div>
-
-
-<p>A generation can be used to indicate a generation time without having to specify the involved activity. A generation time is unique, as specified by the following constraint.<p>
-
-<div class='constraint' id='unique-generation-time'>
-Given an entity denoted by <span class="name">e</span> and
-two time instants <span class="name">t1</span> and <span
-class="name">t2</span>,
-<span class='conditional'>IF</span> <span class="name">wasGeneratedBy(e, -, t1)</span> and <span class="name">wasGeneratedBy(e, -, t2)</span> hold, then <span class="name">t1</span>=<span class="name">t2</span>.
-</div>
-
-<p></p>
-<div class="structural-forward">
-See <a href="#generation-uniqueness">generation-uniqueness</a> for further structural constraints on generations.
-</div>
-
-
-
-</section>
-
-
-<section id="term-Usage">
-<h3>Usage</h3>
-
-
-
-<p>A <dfn id="dfn-Use">usage</dfn> is an <a title="instantaneous event">instantaneous event</a>: an activity beginning to consume an entity.
-Before this event, the activity had not begun to consume or use to this entity.
- The description includes the modalities of usage of this entity by this activity.</p>
-
-
-
-
-
-
-<p>
-A usage identifier is OPTIONAL. It MUST be present when annotating usages or when defining derivations (see
-<a href="#Derivation-Relation">Derivation</a>).</p>
-
-<p>
-A reference to a given entity MAY appear in multiple usages for a given activity identifier.
-</p>
-
-
-<div class="interpretation-forward">
-For the interpretation of a usage, see <a href="#generation-precedes-usage">generation-precedes-usage</a> and <a href="#usage-within-activity">usage-within-activity</a>.
-</div>
-
-
-
-</section>
-
-<section id="term-Start">
-<h3>Start</h3>
-
-
-<p>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-attributes2">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'>
-Given an activity <span class="name">activity(a,t1,t2,attrs1)</span> and its start <span class="name">wasStartedBy(id,a,e,t,attrs2)</span>, then <span class="name">t</span>=<span class="name">t1</span>.
-</div>
-</section>
-
-<section id="term-End">
-<h3>End</h3>
-
-
-<p>An <a>activity end event</a> is the <a title="instantaneous event">instantaneous event</a> that marks the instant an activity ends. It allows for an optional time attribute. <span id="optional-attributes3">Activities also allow for an optional end time attribute. If both are specified, they MUST be the same, as expressed by the following constraint.</span>
-</p>
-
-<div class='constraint' id='unique-endTime'>
-Given an activity <span class="name">activity(a,t1,t2,attrs1)</span> and its end <span class="name">wasEndedBy(id,a,e,t,attrs2)</span>, then <span class="name">t</span>=<span class="name">t2</span>.
-</div>
-
-
-</section>
-
-
-<section id="term-Communication">
-<h3>Communication</h3>
-
-
-
-<p>Communication is formally defined as follows.</p>
-
-<div class='definition' id='wasInformedBy-Definition'>Given two activities identified by <span class="name">a1</span> and <span class="name">a2</span>,
- <span class="name">wasInformedBy(a2,a1)</span>
-holds, <span class='conditional'>IF AND ONLY IF</span>
- there is an entity with some identifier <span class="name">e</span> and some sets of attribute-value pairs <span class="name">attrs1</span> and <span class="name">attrs2</span>,
-such that <span class="name">wasGeneratedBy(-,e,a1,-,attrs1)</span> and <span class="name">used(-,a2,e,-,attrs2)</span> hold.
-</div>
-
-
-<p>
-<div class="interpretation-forward">
-For the constraints on ordering of communication events, see <a href="#wasInformedBy-ordering">wasInformedBy-ordering</a>.
-</div>
-
-
-<p>The relationship <span class="name">wasInformedBy</span> is not transitive. Indeed, consider the following descriptions.</p>
-<pre class="codeexample">
-wasInformedBy(a2,a1)
-wasInformedBy(a3,a2)
-</pre>
-<p> We cannot infer <span class="name">wasInformedBy(a3,a1)</span> from these expressions. 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>
-and used by <span class="name">a2</span>. Likewise, from <span class="name">wasInformedBy(a3,a2)</span>, we know that there exists <span class="name">e2</span> such that <span
-class="name">e2</span> was generated by <span class="name">a2</span> and used by <span class="name">a3</span>. The following illustration shows a case for which transitivity cannot hold. The
-horizontal axis represents the event line. We see that <span class="name">e1</span> was generated after <span class="name">e2</span> was used. Furthermore, the illustration also shows that
-<span class="name">a3</span> completes before <span class="name">a1</span>. So it is impossible for <span class="name">a3</span> to have used an entity generated by <span
-class="name">a1</span>.</p>
-
-<div style="text-align: center;">
-<figure>
-<img src="images/informedByNonTransitive.png" alt="non transitivity of wasInformedBy" />
-<figcaption>Counter-example for transitivity of wasInformedBy</figcaption>
-</figure>
-</div>
-
-</section>
-
-
-
-
-<section id="term-StartByActivity">
-<h3>Start by Activity</h3>
-</section>
-
-
-<p>Start of <span class="name">a2</span> by activity <span class="name">a1</span> is specified as follows.</p>
-
-<div class='definition' id='wasStartedBy'>Given two activities with identifiers <span class="name">a1</span> and <span class="name">a2</span>,
- <span class="name">wasStartedBy(a2,a1)</span>
-holds <span class='conditional'>IF AND ONLY IF</span>
- there exist an entity with some identifier <span class="name">e</span>
-and some attributes <span class="name">gAttr</span> and <span class="name">sAttr</span>,
-such that
- <span class="name">wasGeneratedBy(-,e,a1,-,gAttr)</span>
- and <span class="name">wasStartedBy(-,a2,e,-,sAttr)</span> hold.
-</div>
-
-
-<p>
-
-<div class="interpretation-forward">
-For constraints on ordering of start events, see <a href="#wasStartedBy-ordering">wasStartedBy-ordering</a>.
-</div>
-
-
-
- </section>
-
-
-
- <section id="component2">
-<h3>Component 2: Agents and Responsibility</h3>
-
-
-<section id="term-attribution">
-<h3>Attribution</h3>
-
-Attribution identifies an agent as responsible for an entity. An
-agent can only be responsible for an entity if it was associated with
-an activity that generated the entity. If the activity, generation
-and association events are not explicit in the description, they can
-be inferred.
-
-<div class='inference' id='attribution-implication'>
-<span class='conditional'>IF</span>
-<span class="name">wasAttributedTo(e,ag)</span> holds for some identifiers
-<span class="name">e</span> and <span class="name">ag</span>,
-<span class='conditional'>THEN</span> there exists an activity with some identifier <span class="name">a</span> such that the following statements hold:
-<pre>
-activity(a, t1, t2, attr1)
-wasGeneratedBy(-,e, a, -)
-wasAssociatedWith(-,a, ag, -, attr2)
-</pre>
-for some sets of attribute-value pairs <span class="name">attr1</span>
- and <span class="name">attr2</span>, and times <span class="name">t1</span> and <span class="name">t2</span>.
-</div>
-
-</section>
-
-
-
-
-<section id="term-Association">
-<h4>Association</h4>
-
-<p>
-An association relates an agent to an activity for which the agent had
-some responsibility. Associations can mention a <em>plan</em> that
-describes how the agent expected to participate. The plan may or may
-not have been followed; PROV-DM does not constrain the plan in any
-way. Additional attributes can be used to describe how the agent
-participated, for example to name a role or indicate when the agent
-was associated with a long-running activity.
-</p>
-<div id="optional-attributes4">
-<p>In an association of the form <span class="name">wasAssociatedWith(a, ag, -, attr)</span>, the absence of a plan means: either no plan exists, or a plan exists but it is not identified.</p>
-
-
-<p>In an association of the form <span class="name">wasAssociatedWith(a, -, pl, attr)</span>, an agent exists but it is not identified.</p>
-</div>
-
-
-<div class="interpretation-forward">
-For the interpretation of an association, see <a href="#wasAssociatedWith-ordering">wasAssociatedWith-ordering</a>.
-</div>
-
-
-
-</section>
-
-<section id="term-Responsibility">
-<h3>Responsibility</h3>
-</section>
-
-<p> Responsibility relates agents where one agent acts on behalf of
-another, in the context of some activity. The supervising agent
-delegates some responsibility for part of the activity to the
-subordinate agent, while retaining some responsibility for the overall
-activity. </p>
-
-<div id="optional-activity">
-<p>In a a delegation of the form <span class="name">actedOnBehalfOf(a,
- ag2, ag1, -, attr)</span>, the absence of an activity means that
- <span class="name">a2</span> acts on behalf of <span
- class="name">a1</span> for all activities with which <span
- class="name">a2</span> is
- associated.
-</div>
-<div class="note">
- @@TODO: Could this be an inference? Does it imply that
- a1 is associated with all activities a2 is associated with?
- </div></p>
-
-<div class="interpretation-forward">
-For the interpretation of responsibility, see <a href="#actedOnBehalfOf-ordering">actedOnBehalfOf-ordering</a>.
-</div>
-
-
-</section>
-
-
-
-
-
- <section id="component3">
-<h3>Component 3: Derivations</h3>
-
-
-
-
-<section id="Derivation-Relation">
-<h4>Derivation</h4>
-
-<div class="interpretation-forward">
-For the interpretation of a derivation, see <a href="#derivation-usage-generation-ordering">derivation-usage-generation-ordering</a> and <a
-href="#derivation-generation-generation-ordering">derivation-generation-generation-ordering</a>
-</div>
-
-
-<p>
-Note that derivation cannot in general be inferred from the existence
-of related usage and generation events. Indeed, when a generation <span class="name">wasGeneratedBy(g, e2, a, -, attrs2)</span>
-<a>precedes</a> <span class="name">used(u, a, e1, -, attrs1)</span>, for
-some <span class="name">e1</span>, <span class="name">e2</span>, <span class="name">attrs1</span>, <span class="name">attrs2</span>, and <span class="name">a</span>, one
-cannot infer derivation <span class="name">wasDerivedFrom(e2, e1, a, g, u)</span>
-or <span class="name">wasDerivedFrom(e2,e1)</span> since
- <span class="name">e2</span> cannot possibly be derived from
- <span class="name">e1</span>, given the creation of <span class="name">e2</span> <a>precedes</a> the use
-of <span class="name">e1</span>. That is, if <span class="name">e1</span> is generated
-by an activity before <span class="name">e2</span> is used, then
-obviously <span class="name">e2</span> cannot have been derived from
-<span class="name">e1</span>. However, even if <span
-class="name">e2</span> happens used before <span class="name">e1</span>
-is generated, it is not safe to assume that <span
-class="name">e2</span> was derived from <span class="name">e1</span>.
-</p>
-
-<p> Derivation is not defined to be transitive. Domain-specific specializations of derivation may be defined in such a way that the transitivity property
-holds.</p>
-
-
-
-<p></p>
-<div class="structural-forward">
-See <a href="#derivation-use">derivation-use</a> for a structural constraint on derivations.
-</div>
-
-
-
-
-
-
-
-</section>
-
-<section id="term-Revision">
-<h3>Revision</h3>
-
-
-
-<p>A revision needs to satisfy the following constraint, linking the two entities by a derivation, and stating them to be a specialization of a third entity.</p>
-
-<div class='inference' id='wasRevision'>
-Given two identifiers <span class="name">e1</span> and <span class="name">e2</span> identifying two entities, and an identifier <span class="name">ag</span> identifying an agent,
-<span class='conditional'>IF</span> <span class="name">wasRevisionOf(e2,e1,ag)</span> holds, <span class='conditional'>THEN</span>
-there exists an entity with some identifier <span class="name">e</span> and some attribute-values <span class="name">eAttrs</span>, <span class="name">dAttrs</span>, such that the following
-hold:
-<pre>
-wasDerivedFrom(e2,e1,dAttrs)
-entity(e,eAttrs)
-specializationOf(e2,e)
-specializationOf(e1,e)
-wasAttributedTo(e2,ag)
-</pre>
-</div>
-
-<p>
-<div id="optional-attributes5">In a revision of the form <span class="name">wasRevisionOf(e2,e1,-,attr)</span>, the absence of an agent means: either no agent exists, or an agent exists but it is not identified.</div>
-
-
-<p><span class="name">wasRevisionOf</span> is a strict sub-relation
- of <span class="name">wasDerivedFrom</span> since two entities <span class="name">e2</span> and <span class="name">e1</span>
- may satisfy <span class="name">wasDerivedFrom(e2,e1)</span> without being a variant of
- each other.
-</p>
-
-
-</section>
-
-<section id="term-quotation">
-<h3>Quotation</h3>
-
-
-<div class='inference' id='quotation-implication'>
-<span class='conditional'>IF</span>
-<span class="name">wasQuotedFrom(e2,e1,ag2,ag1,attrs)</span> holds for some identifiers
-<span class="name">e2</span>, <span class="name">e1</span>, <span class="name">ag2</span>, <span class="name">ag1</span>,
-<span class='conditional'>THEN</span> the following hold:
-<pre>
-wasDerivedFrom(e2,e1)
-wasAttributedTo(e2,ag2)
-wasAttributedTo(e1,ag1)
-</pre>
-</div>
-
-<p>
-
-<div id="optional-attributes6">In a quotation of the form <span class="name">wasQuotedFrom(e2,e1,-,-,attrs)</span>, the absence of an agent means: either no agent exists, or an agent exists but it is not identified.</div>
-
-
-</section>
-
-
-
-
-<section id="term-traceability">
-<h3>Traceability</h3>
-
-<p>Traceability allows an entity to be transitively linked to another entity it is derived from, to an agent it is attributed to, or another agent having some responsibility, or a trigger of an activity that generated it.</p>
-
-<p>Traceability can be inferred from existing descriptions, or can be asserted stating that a dependency path exists without its individual steps being expressed. This is captured
-by the following inference and constraint, respectively.
-
-<div class='inference' id='traceability-inference'>
-Given two identifiers <span class="name">e2</span> and <span class="name">e1</span> for entities,
-the following statements hold:
-
-<ol>
-<li><span class='conditional'>IF</span> <span class="name">wasDerivedFrom(e2,e1,a,g2,u1)</span> holds, for some <span class="name">a</span>, <span class="name">g2</span>, <span
-class="name">u1</span>, <span class='conditional'>THEN</span> <span class="name">tracedTo(e2,e1)</span> also holds.</li>
-<li><span class='conditional'>IF</span> <span class="name">wasDerivedFrom(e2,e1)</span> holds, <span class='conditional'>THEN</span> <span class="name">tracedTo(e2,e1)</span> also
-holds.</li>
-<li><span class='conditional'>IF</span> <span class="name">wasAttributedTo(e2,ag1,aAttr)</span> holds, <span class='conditional'>THEN</span> <span class="name">tracedTo(e2,ag1)</span> also holds.</li>
-<li><span class='conditional'>IF</span> <span class="name">wasAttributedTo(e2,ag2,aAttr)</span>, <span class="name">wasGeneratedBy(e2,a,gAttr)</span>, and <span
-class="name">actedOnBehalfOf(ag2,ag1,a,rAttr)</span> hold, for some <span class="name">a</span>, <span class="name">ag2</span>, <span class="name">ag1</span>, <span class="name">aAttr</span>, <span class="name">gAttr</span>, and <span class="name">rAttr</span>, <span
-class='conditional'>THEN</span> <span class="name">tracedTo(e2,ag1)</span> also holds.</li>
-
-<li><span class='conditional'>IF</span> <span
-class="name">wasGeneratedBy(e2,a,gAttr)</span> and <span
-class="name">wasStartedBy(a,e1,sAttr)</span> hold, for some <span
-class="name">a</span>, <span class="name">gAttr</span> , <span
-class="name">sAttr</span> then <span
-class="name">tracedTo(e2,e1)</span> holds.</li>
-<li><span class='conditional'>IF</span> <span class="name">tracedTo(e2,e)</span> and <span class="name">tracedTo(e,e1)</span> hold for some <span class="name">e</span>, <span
-class='conditional'>THEN</span> <span class="name">tracedTo(e2,e1)</span> also holds.</li>
-</ol>
-</div>
-
-<p>We note that the inference rule <a
-href="#traceability-inference">traceability-inference</a> does not
-allow us to infer anything about the attributes of the related
-entities or events. </p>
-
-<div class='constraint' id='traceability-assertion'>
-<span class='conditional'>IF</span> <span
- class="name">tracedTo(r2,r1,attrs)</span> holds for two entity identifiers <span class="name">r2</span> and <span class="name">r1</span>, and attribute-value pairs <span class="name">attrs</span>,
- <span class='conditional'>THEN</span> there exist
-<span class="name">e<sub>0</sub></span>, <span class="name">e<sub>1</sub></span>, ..., <span class="name">e<sub>n</sub></span> for <span class="name">n≥1</span>, with <span
-class="name">e<sub>0</sub></span>=<span class="name">r2</span> and <span class="name">e<sub>n</sub></span>=<span class="name">r1</span>, and
-for any i such that <span class="name">0≤i≤n-1</span>, at least
- one of the following statements holds:
-<ul>
-<li> <span class="name">wasDerivedFrom(e<sub>i</sub>,e<sub>i+1</sub>,a,g2,u1)</span> holds, for some <span class="name">a</span>, <span class="name">g2</span>, <span class="name">u1</span>,
-or</li>
-<li> <span class="name">wasDerivedFrom(e<sub>i</sub>,e<sub>i+1</sub>)</span> holds, or</li>
-<li> <span class="name">wasAttributedTo(e<sub>i</sub>,e<sub>i+1</sub>)</span> holds, or</li>
-<li> <span class="name">wasAttributedTo(e<sub>i</sub>,e)</span>, <span class="name">wasGeneratedBy(e<sub>i</sub>,a,gAttr)</span>, and <span class="name">actedOnBehalfOf(e,e<sub>i+1</sub>,a,rAttr)</span> hold,
-for some <span class="name">a</span>, <span class="name">e</span> and <span class="name">gAttr</span>, <span class="name">rAttr</span>, or</li>
-<li> <span class="name">wasGeneratedBy(e<sub>i</sub>,a,gAttr) and wasStartedBy(a,e<sub>i+1</sub>,sAttr)</span> hold, for some <span class="name">a</span>, <span class="name">e</span>, and
-<span class="name">gAttr</span>, and <span
-class="name">sAttr</span>.</li>
-</ul>
-</div>
-
-<p>We note that the previous constraint is not really an inference <em>rule</em>, since there is nothing that we can actually infer. Instead, this constraint should simply be seen as part
-of the definition of the traceability relation. </p>
-
-
-</section>
-
-</section>
-
-<section id="component4">
-<h3>Component 4: Alternate Entities</h3>
-<div class='note'>TODO:
-This section is under review, pending ISSUE-29.
-</div>
-
-<section id="term-Specialization">
-<h3>Specialization</h3>
-
-
-<p>Specialization is <em>neither symmetric nor anti-symmetric</em>.
-</p>
-
-<div class="anexample" id="anexample-not-symmetric">
-"Alice's toyota car on fifth Avenue" is a specialization of "Alice's toyota car", but the converse does not hold.
-</div>
-
-<div class="anexample" id="anexample-specialization-not-anti-symmetric">
-anti-symmetric counter-example???
-</div>
-
-
-<p>Specialization is <em>transitive</em>. Indeed if <span
-class="name">specializationOf(e1,e2)</span> holds, then there is some
-common thing, say <span class="name">T1-2</span> they both refer to,
-and <span class="name">e1</span> is a more specific aspect of this
-thing than <span class="name">e2</span>. Likewise, if <span
-class="name">specializationOf(e2,e3)</span> holds, then there is some
-common thing, say <span class="name">T2-3</span> they both refer to, and <span class="name">e2</span> is a more specific aspect of this
-thing than <span class="name">e3</span>. The things <span
-class="name">T1-2</span> and <span class="name">T2-3</span> are the
-same since <span class="name">e2</span> is an aspect of both of them,
-so <span
-class="name">specializationOf(e1,e3)</span> follows since <span class="name">e1<span class="name"> and <span class="name">e3<span class="name">
-are aspects fo the same thing and <span class="name">e1<span class="name"> is more specific than <span class="name">e3<span class="name">. </p>
-
-
-<div class="anexample" id="anexample-specialization-is-transitive">
-A specialization of "this email message" would be, for example, the "printed version on my desk", which is a specialization of "my thoughts on this email thread". So, the "printed version on my desk" is also a specialization "my thoughts on this email thread".
-</div>
-
-
-</section>
-
-<section id="term-Alternate">
-<h3>Alternate</h3>
-</section>
-
-
-<p>Alternate not is <em>reflexive</em>. Indeed, <span class="name">alternate(e,e)</span> does not hold for any arbitrary entity <span class="name">e</span> since <span class="name">e</span> may not be a specialization of another entity.</p>
-
-
-<p>Alternate is <em>symmetric</em>. Indeed, if <span class="name">alternate(e1,e2)</span> holds,
-then there exists an unspecified entity <span class="name">e</span>, such that
-both <span class="name">e1</span> and <span class="name">e2</span> are specialization of <span class="name">e</span>.
-Therefore, <span class="name">alternate(e2,e1)</span> also holds.
-</p>
-
-
-
-<p>Alternate is <em>not transitive</em>. Indeed, if <span class="name">alternate(e1,e2)</span> holds,
-then there exists an unspecified entity <span class="name">e1-2</span>, such that
-both <span class="name">e1</span> and <span class="name">e2</span> are specialization of <span class="name">e1-2</span>.
-Likewise, if <span class="name">alternate(e2,e3)</span> holds,
-then there exists an unspecified entity <span class="name">e2-3</span>, such that
-both <span class="name">e2</span> and <span class="name">e3</span> are specialization of <span class="name">e2-3</span>.
-It does not imply that there is a common entity <span class="name">e1-3</span>
-that both <span class="name">e1</span> and <span class="name">e3</span> specialize.
-</p>
-
-
-<div class="anexample" id="anexample-alternate-not-transitive1">
-<p>At 6pm, the customer in a chair is a woman in a red dress, who happens to be Alice. After she leaves, another customer arrives at 7pm, a man with glasses, who happens to be Bob. Transitivity does not hold since the <span class="name">womanInRedDress\</span> is not alternate of <span class="name">customerInChairAt7pm</span>.
-<pre>
-alternate(womanInRedDress,customerInChairAt6pm)
-specialization(customerInChairAt6pm,Alice)
-specialization(womanInRedDress,Alice)
-
-alternate(manWithGlasses,customerInChairAt7pm)
-specialization(customerInChairAt7pm,Bob)
-specialization(manWithGlasses,Bob)
-
-alternate(customerInChairAt6pm, customerInChairAt7pm)
-specialization(customerInChairAt6pm, customerInChair)
-specialization(customerInChairAt7pm, customerInChair)
-</pre>
-</div>
-
-<p>The above example shows that <span class="name">customerInChairAt6pm</span> and <span class="name">customerInChairAt7pm</span> are two alternate entities that have no overlap, while <span class="name">womanInRedDress</span> and <span class="name">customerInChairAt6pm</span> do overlap.
-The following example illustrates another case of non-overlapping alternate entities.
-</p>
-
-<div class="anexample">Two copies of the same book, where copy A was destroyed before copy B was made.</div>
-
-
-</section>
-
-
-
-</section>
-
@@ -2768,7 +2443,24 @@
WG membership to be listed here.
</p>
</section>
-
+
+<section class="glossary">
+ <h2>Glossary</h2>
+ <ul>
+ <li> <dfn>anti-symmetric</dfn>: A relation R over X is <a>anti-symmetric</a> if
+ for any elements x, y of X, if x R y and y R x then x = y.</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>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
+ for any elements x, y, z of X, if x R y and y R z then x R z.</li>
+
+
+ </ul>
+ </section>
+
+
</body></html>
<!-- LocalWords: px DM RL RDF AQ SEM SOTD Definitional wasInformedBy attrs ag