--- a/model/prov-constraints.html Fri Aug 17 08:48:25 2012 -0400
+++ b/model/prov-constraints.html Fri Aug 17 08:48:43 2012 -0400
@@ -777,6 +777,207 @@
</section>
+<section id="typing">
+<h2>Types</h2>
+
+<p> As set out in other specifications, the identifiers used in PROV
+documents have associated type information. An identifier can have
+more than one type, reflecting subtyping or allowed overlap between
+types, and so we define a set of types of each identifier, <span class="name">typeof(id)</span>. Some types are, however,
+required not to overlap (for example, no identifier can describe both
+an entity and an activity).
+In addition, an identifier cannot be used to identify both an object
+(that is, an entity, activity or agent) and a property (that is, a
+named event such as usage, generation, or a relationship such as
+attribution.)
+This specification includes <a href="#type-constraints">disjointness and typing constraints</a> that
+check these requirements. Here, we merely
+summarize the type constraints in <a href="#typing-table">Table 1</a>.
+</p>
+
+<div id="typing-table-fig">
+ <table id="typing-table" border="1"class="thinborder" style="margin-left: auto; margin-right: auto; border-color: black;">
+<caption id="typing-table-caption">Table 1: Summary of Typing Constraints</caption>
+<tr><td style="border-width: 0px; "></td><td style="border-width: 0px; "></td><td style="border-width: 0px; "></td></tr>
+ <tr>
+ <th>In relation...</th>
+ <th>identifier</th>
+ <th>has type(s)...</th>
+ </tr>
+ <tr align="center" >
+ <td class="name">entity(e,attrs)</td>
+ <td class="name" align="center">e</td>
+ <td class="name">'entity'</td>
+ </tr>
+ <tr align="center" >
+ <td class="name">activity(a,t1,t2,attrs)</td>
+ <td class="name">a</td>
+ <td class="name">'activity'</td>
+ </tr>
+ <tr align="center" >
+ <td class="name">agent(ag,attrs)</td>
+ <td class="name">ag</td>
+ <td class="name">'agent'</td>
+ </tr>
+ <tr align="center" >
+ <td rowspan="2" class="name">used(id; a,e,t,attrs)</td>
+ <td class="name">e</td>
+ <td class="name">'entity'</td>
+ </tr>
+ <tr align="center" >
+ <td class="name">a</td>
+ <td class="name">'activity'</td>
+ </tr>
+ <tr align="center" >
+ <td rowspan="2" class="name">wasGeneratedBy(id; e,a,t,attrs)</td>
+ <td class="name">e</td>
+ <td class="name">'entity'</td>
+ </tr>
+ <tr align="center">
+ <td class="name">a</td>
+ <td class="name">'activity'</td>
+ </tr>
+ <tr align="center">
+ <td rowspan="2" class="name">wasInformedBy(id; a2,a1,attrs)</td>
+ <td class="name">a1</td>
+ <td class="name">'activity'</td>
+ </tr>
+ <tr align="center">
+ <td class="name">a2</td>
+ <td class="name">'activity'</td>
+ </tr>
+ <tr align="center">
+ <td rowspan=3 class="name">wasStartedBy(id; a2,e,a1,t,attrs)</td>
+ <td class="name">a2</td>
+ <td class="name">'activity'</td>
+ </tr>
+ <tr align="center">
+ <td class="name">e</td>
+ <td class="name">'entity'</td>
+ </tr>
+ <tr align="center">
+ <td class="name">a1</td>
+ <td class="name">'activity'</td>
+ </tr>
+ <tr align="center">
+ <td rowspan="3" class="name">wasEndedBy(id; a2,e,a1,t,attrs)</td>
+ <td class="name">a2</td>
+ <td class="name">'activity'</td>
+ </tr>
+ <tr align="center">
+ <td class="name">e</td>
+ <td class="name">'entity'</td>
+ </tr>
+ <tr align="center">
+ <td class="name">a1</td>
+ <td class="name">'activity'</td>
+ </tr>
+ <tr align="center">
+ <td rowspan="2" class="name">wasInvalidatedBy(id; e,a,t,attrs)</td>
+ <td class="name">a</td>
+ <td class="name">'activity'</td>
+ </tr>
+ <tr align="center">
+ <td class="name">a</td>
+ <td class="name">'activity'</td>
+ </tr>
+ <tr align="center">
+ <td rowspan="3" class="name">wasDerivedFrom(id; e2,e1,a,g,u,attrs)</td>
+ <td class="name">e2</td>
+ <td class="name">'entity'</td>
+ </tr>
+ <tr align="center">
+ <td class="name">e1</td>
+ <td class="name">'entity'</td>
+ </tr>
+ <tr align="center">
+ <td class="name">a</td>
+ <td class="name">'activity'</td>
+ </tr>
+ <tr align="center">
+ <td rowspan="2" class="name">wasAttributedTo(id; e,ag,attr)</td>
+ <td class="name">e</td>
+ <td class="name">'entity'</td>
+ </tr>
+ <tr align="center">
+ <td class="name">ag</td>
+ <td class="name">'agent'</td>
+ </tr>
+ <tr align="center">
+ <td rowspan="3" class="name">wasAssociatedWith(id; a,ag,pl,attrs)</td>
+ <td class="name">a</td>
+ <td class="name">'activity'</td>
+ </tr>
+ <tr align="center">
+ <td class="name">ag</td>
+ <td class="name">'agent'</td>
+ </tr>
+ <tr align="center">
+ <td class="name">pl</td>
+ <td class="name">'entity'</td>
+ </tr>
+ <tr align="center">
+ <td rowspan="3" class="name">actedOnBehalfOf(id; ag2,ag1,a,attrs)</td>
+ <td class="name">ag2</td>
+ <td class="name">'agent'</td>
+ </tr>
+ <tr align="center">
+ <td class="name">ag1</td>
+ <td class="name">'agent'</td>
+ </tr>
+ <tr align="center">
+ <td class="name">a</td>
+ <td class="name">'activity'</td>
+ </tr>
+ <tr align="center">
+ <td rowspan="2" class="name">alternateOf(e1,e2)</td>
+ <td class="name">e1</td>
+ <td class="name">'entity'</td>
+ </tr>
+ <tr align="center">
+ <td class="name">e2</td>
+ <td class="name">'entity'</td>
+ </tr>
+ <tr align="center">
+ <td rowspan="2" class="name">specializationOf(e1,e2)</td>
+ <td class="name">e1</td>
+ <td class="name">'entity'</td>
+ </tr>
+ <tr align="center">
+ <td class="name">e2</td>
+ <td class="name">'entity'</td>
+ </tr>
+ <tr align="center">
+ <td rowspan="3" class="name">mentionOf(e1,e2,b)</td>
+ <td class="name">e1</td>
+ <td class="name">'entity'</td>
+ </tr>
+ <tr align="center">
+ <td class="name">e2</td>
+ <td class="name">'entity'</td>
+ </tr>
+ <tr align="center">
+ <td class="name">b</td>
+ <td class="name">'entity'</td>
+ </tr>
+ <tr align="center">
+ <td rowspan="2" class="name">hadMember(c,e)</td>
+ <td class="name">c</td>
+ <td class="name">'entity'<br /> 'prov:Collection'</td>
+ </tr>
+ <tr align="center">
+ <td class="name">e</td>
+ <td class="name">'entity'</td>
+ </tr>
+ <tr align="center">
+ <td class="name">entity(c,[prov:type='prov:EmptyCollection,...])</td>
+ <td class="name">c</td>
+ <td class="name">'entity'<br /> 'prov:Collection' <br /> 'prov:EmptyCollection'</td>
+ </tr>
+ </table>
+ </div>
+
+</section>
<section>
<h4>Validation Process Overview</h4>
@@ -804,7 +1005,7 @@
</p>
- <h2>Constants, Variables and Placeholders</h2>
+ <h4>Constants, Variables and Placeholders</h4>
<p>
PROV statements involve identifiers (URIs), literals,
placeholders, and attribute lists. However, in order to specify
@@ -839,7 +1040,7 @@
</p>
- <h2>Substitution</h2>
+ <h4>Substitution</h4>
<p>A substitution is a function that maps variables to terms. Concretely, since we only
need to consider substitutions of finite sets of variables, we can
write substitutions as <span class="math">[x_1 = t_1,...,x_n=t_n]</span>. A substitution
@@ -858,7 +1059,7 @@
- <h2>Formulas</h2>
+ <h4>Formulas</h4>
<p>
For the purpose of constraint checking, we view PROV statements
(possibly involving existential variables) as
@@ -897,7 +1098,7 @@
</ul>
- <h2>Satisfying definitions, inferences, and constraints</h2>
+ <h4>Satisfying definitions, inferences, and constraints</h4>
<p>
In logic, a formula's meaning is defined by saying when it is
<em>satisfied</em> in a situation. Likewise, we can view
@@ -911,7 +1112,7 @@
<li>Ordering constraints</li>
</ol>
-<h2>Merging</h2>
+<h4>Merging</h4>
<p>Merging is an operation that takes two terms and compares them to
see if they are equal, or can be made equal by substituting an
@@ -921,7 +1122,7 @@
</p>
- <h2>Applying definitions, inferences, and constraints</h2>
+ <h4>Applying definitions, inferences, and constraints</h4>
<p>Formulas can also be interpreted as having computational
content. That is, if an instance does not satisfy a formula, we can
often <em>apply</em> the formula to the instance to produce another
@@ -954,7 +1155,7 @@
</p>
- <h2>Termination</h2>
+ <h4>Termination</h4>
<p>
It is possible to define sets of formulas such that normalization
does not terminate, that is, such that there is an infinite sequence
@@ -987,7 +1188,7 @@
indirectly referenced in other relations.
</p>
- <h2>Checking ordering, typing, and impossibility constraints</h2>
+ <h4>Checking ordering, typing, and impossibility constraints</h4>
<p>
The ordering, typing, and impossibility constraints are checked
rather than applied. This means that they do not generate new
@@ -1023,7 +1224,7 @@
- <h2>Equivalence and Isomorphism</h2>
+ <h4>Equivalence and Isomorphism</h4>
<p> Given two normal forms, a natural question is whether they contain
the same information, that is, whether they are equivalent (if so,
then the original instances are also equivalent.) By analogy with
@@ -1054,7 +1255,7 @@
those obtained by the algorithm in this specification.
</p>
-<h2>From Instances to Documents</h2>
+<h4>From Instances to Documents</h4>
<p>PROV documents can contain multiple instances: a <a>toplevel
instance</a>, the set of statements not appearing within a bundle, and
@@ -1078,7 +1279,7 @@
<section>
<h4>Summary of constraints and inferences</h4>
-<p><a href="">Table 1</a> summarizes the definitions, inferences, and
+<p><a href="">Table 2</a> summarizes the definitions, inferences, and
constraints of this document.
</p>
@@ -1086,7 +1287,7 @@
<div id="prov-constraints-fig" style="text-align: left;">
<table class="thinborder" style="margin-left: auto; margin-right: auto; border-color: #0;">
-<caption id="prov-constraints">Table 1: Summary of definitions, constraints, and inferences for PROV Types and Relations</caption>
+<caption id="prov-constraints">Table 2: Summary of definitions, constraints, and inferences for PROV Types and Relations</caption>
<tr><td><a><b>Type or Relation Name</b></a></td><td><b>
Inferences and Constraints</b></td><td><b>Component</b></td></tr>
<tr><td style="border-width: 0px; "></td><td style="border-width: 0px; "></td><td style="border-width: 0px; "></td></tr>
@@ -1382,7 +1583,7 @@
All figures are for illustration purposes
only. Information in tables is normative if it appears in a
normative section; specifically, <a
- href="#expandable-parameters-fig">Table 2</a> is normative. Text in appendices and
+ href="#expandable-parameters-fig">Table 3</a> is normative. Text in appendices and
in boxes labeled "Remark" is informative. Where there is any apparent
ambiguity between the descriptive text and the formal text in a
"definition", "inference" or "constraint" box, the formal text takes
@@ -1642,7 +1843,7 @@
expandable parameter is one that can be omitted using the
placeholder <span class="name">-</span>, and if so, it is
to be replaced by a fresh existential identifier.
- <a href="#expandable-parameters-fig">Table 2</a> defines the <a>expandable
+ <a href="#expandable-parameters-fig">Table 3</a> defines the <a>expandable
parameter</a>s of the properties of PROV, needed in <a class="rule-ref"
href="#optional-placeholders"><span>TBD</span></a>. For emphasis, the four optional parameters
that are not <a title="expandable parameter">expandable</a> are
@@ -1652,7 +1853,7 @@
href="#optional-identifiers"><span>TBD</span></a>, are not listed.</p>
<div id="expandable-parameters-fig">
<table id="expandable-parameters" border="1" class="thinborder" style="margin-left: auto; margin-right: auto; border-color: black;">
-<caption id="expandable-parameters">Table 2: Expandable and
+<caption id="expandable-parameters">Table 3: Expandable and
Non-Expandable Parameters</caption>
<tr><td style="border-width: 0px; "></td><td style="border-width: 0px; "></td><td style="border-width: 0px; "></td></tr>
<tr>
@@ -1737,7 +1938,7 @@
<p> <a class="rule-ref"
href="#optional-placeholders"><span>TBD</span></a> states how parameters are to be expanded,
using the expandable parameters defined in <a
- href="#expandable-parameters-fig">Table 2</a>. The last two parts
+ href="#expandable-parameters-fig">Table 3</a>. The last two parts
indicate how to handle expansion of parameters for
<span class="name">wasDerivedFrom</span> expansion, which is only allowed for the
generation and use parameters when the activity is specified. A
@@ -1780,7 +1981,7 @@
}, if the <span class="name">i</span>th parameter
of <span class="name">r</span> is an <a>expandable parameter</a>
of <span class="name">r</span>
- as specified in <a href="#expandable-parameters-fig">Table 2</a>
+ as specified in <a href="#expandable-parameters-fig">Table 3</a>
then the following definition holds:
<p> <span class="name">r(a<sub>0</sub>;...,a<sub>i-1</sub>, -, a<sub>i+1</sub>, ...,a<sub>n</sub>) </span> <span class="conditional">IF AND ONLY IF</span> there exists <span class="name">a'</span>
such that <span class="name">r(a<sub>0</sub>;...,a<sub>i-1</sub>,a',a<sub>i+1</sub>,...,a<sub>n</sub>)</span>.
@@ -3002,9 +3203,9 @@
<ol>
<li>
<span class="conditional">IF</span>
-<span class="name">used(use; a,e,_t,_attrs)</span>
-and
<span class="name">wasStartedBy(start; a,_e1,_a1,_t1,_attrs1)</span>
+ and
+<span class="name">used(use; a,_e2,_t2,_attrs2)</span>
<span class="conditional">THEN</span>
<span class="name">start</span>
<a title="precedes">precedes</a>
@@ -3012,7 +3213,7 @@
</li>
<li>
<span class="conditional">IF</span>
-<span class="name">used(use; a,e,_t,_attrs)</span>
+<span class="name">used(use; a,_e1,_t1,_attrs1)</span>
and
<span class="name">wasEndedBy(end; a,_e2,_a2,_t2,_attrs2)</span>
<span class="conditional">THEN</span>
@@ -3035,9 +3236,9 @@
<ol>
<li>
<span class="conditional">IF</span>
-<span class="name">wasGeneratedBy(gen; _e,a,_t,_attrs)</span>
-and
<span class="name">wasStartedBy(start; a,_e1,_a1,_t1,_attrs1)</span>
+ and
+<span class="name">wasGeneratedBy(gen; _e2,a,_t2,_attrs2)</span>
<span class="conditional">THEN</span>
<span class="name">start</span>
<a title="precedes">precedes</a>
@@ -3325,9 +3526,9 @@
<ol>
<li>
<span class="conditional">IF</span>
-<span class="name">wasStartedBy(start; _a,e,_a1,_t1,_attrs1)</span>
+<span class="name">wasGeneratedBy(gen; e,_a1,_t1,_attrs1)</span>
and
-<span class="name">wasGeneratedBy(gen; e,_a2,_t2,_attrs2)</span>
+<span class="name">wasStartedBy(start; _a,e,_a2,_t2,_attrs2)</span>
<span class="conditional">THEN</span>
<span class="name">gen</span>
<a title="precedes">precedes</a>
@@ -3336,7 +3537,7 @@
<span class="conditional">IF</span>
<span class="name">wasStartedBy(start; _a,e,_a1,_t1,_attrs1)</span>
and
-<span class="name">wasInvalidatedBy(inv; e,_a3,_t3,_attrs3)</span>
+<span class="name">wasInvalidatedBy(inv; e,_a2,_t2,_attrs2)</span>
<span class="conditional">THEN</span>
<span class="name">start</span>
<a title="precedes">precedes</a>
@@ -3357,9 +3558,9 @@
<ol>
<li>
<span class="conditional">IF</span>
-<span class="name">wasEndedBy(end; _a,e,_a1,_t1,_attrs1)</span>
+<span class="name">wasGeneratedBy(gen; e,_a1,_t1,_attrs1)</span>
and
-<span class="name">wasGeneratedBy(gen; e,_a2,_t2,_attrs2)</span>
+ <span class="name">wasEndedBy(end; _a,e,_a2,_t2,_attrs2)</span>
<span class="conditional">THEN</span>
<span class="name">gen</span>
<a title="precedes">precedes</a>
@@ -3368,7 +3569,7 @@
<span class="conditional">IF</span>
<span class="name">wasEndedBy(end; _a,e,_a1,_t1,_attrs1)</span>
and
-<span class="name">wasInvalidatedBy(inv; e,_a3,_t3,_attrs3)</span>
+<span class="name">wasInvalidatedBy(inv; e,_a2,_t2,_attrs2)</span>
<span class="conditional">THEN</span>
<span class="name">end</span>
<a title="precedes">precedes</a>
@@ -3412,8 +3613,8 @@
<p>
<span class="conditional">IF</span> <span
class="name">specializationOf(e1,e2)</span> and <span
- class="name">wasInvalidatedBy(inv2; e2,_a2,_t2,_attrs2)</span> and
- <span class="name">wasInvalidatedBy(inv1; e1,_a1,_t1,_attrs1)</span>
+ <span class="name">wasInvalidatedBy(inv1; e1,_a1,_t1,_attrs1)</span> and
+ class="name">wasInvalidatedBy(inv2; e2,_a2,_t2,_attrs2)</span>
<span class="conditional">THEN</span> <span class="name">inv1</span> <a>precedes</a> <span class="name">inv2</span>.
</p>
</div>
@@ -3486,20 +3687,20 @@
and
<span class="name">wasStartedBy(start; a,_e5,_a5,_t5,_attrs5)</span>
and
-<span class="name">wasEndedBy(end1; ag,_e6,_a6,_t6,_attrs6)</span>
+<span class="name">wasEndedBy(end; ag,_e6,_a6,_t6,_attrs6)</span>
<span class="conditional">THEN</span>
<span class="name">start</span>
<a title="precedes">precedes</a>
-<span class="name">end1</span>.
+<span class="name">end</span>.
</li><li>
<span class="conditional">IF</span>
<span class="name">wasAssociatedWith(_assoc; a,ag,_pl,_attrs)</span>
and
-<span class="name">wasStartedBy(start1; ag,_e7,_a7,_t7,_attrs7)</span>
+<span class="name">wasStartedBy(start; ag,_e7,_a7,_t7,_attrs7)</span>
and
<span class="name">wasEndedBy(end; a,_e8,_a8,_t8,_attrs8)</span>
<span class="conditional">THEN</span>
-<span class="name">start1</span>
+<span class="name">start</span>
<a title="precedes">precedes</a>
<span class="name">end</span>.
</li>
@@ -3523,20 +3724,20 @@
<span class="conditional">IF</span>
<span class="name">wasAttributedTo(_at; e,ag,_attrs)</span>
and
-<span class="name">wasGeneratedBy(gen1; e,_a1,_t1,_attrs1)</span>
+<span class="name">wasGeneratedBy(gen1; ag,_a1,_t1,_attrs1)</span>
and
-<span class="name">wasGeneratedBy(gen2; ag,_a2,_t2,_attrs2)</span>
+<span class="name">wasGeneratedBy(gen2; e,_a2,_t2,_attrs2)</span>
<span class="conditional">THEN</span>
-<span class="name">gen2</span>
+<span class="name">gen1</span>
<a title="precedes">precedes</a>
-<span class="name">gen1</span>.
+<span class="name">gen2</span>.
</li><li>
<span class="conditional">IF</span>
<span class="name">wasAttributedTo(_at; e,ag,_attrs)</span>
and
-<span class="name">wasGeneratedBy(gen; e,_a3,_t3,_attrs3)</span>
+<span class="name">wasStartedBy(start; ag,_e3,_a3,_t3,_attrs3)</span>
and
-<span class="name">wasStartedBy(start; ag,_e4,_a4,_t4,_attrs4)</span>
+<span class="name">wasGeneratedBy(gen; e,_a4,_t4,_attrs4)</span>
<span class="conditional">THEN</span>
<span class="name">start</span>
<a title="precedes">precedes</a>
@@ -3605,8 +3806,7 @@
class="name">'prov:Collection'</span>) or because certain types are not
disjoint (such as <span class="name">'agent'</span> and <span class="name">'entity'</span>). The set of types
does not reflect all of the distinctions among objects, only those
- relevant for checking validity. In particular, subtypes such as
- <span class="name">'plan'</span> are omitted.
+ relevant for checking validity. In particular, subtypes such as <span class="name">'plan'</span> and <span class="name">'bundle'</span> are omitted, and statements such as <span class="name">wasAssociatedWith</span> and <span class="name">mentionOf</span> that have plan or bundle parameters only check that these parameters are entities.
</p>
<p>To check if a PROV instance satisfies type constraints, one obtains the types of identifiers by application of
@@ -3624,14 +3824,6 @@
<ol>
<li>
<span class='conditional'>IF</span>
- <span class='name'>wasGeneratedBy(gen; e,a,t,attrs)</span>
-<span class='conditional'>THEN</span>
-<span class="name">'entity' ∈ typeOf(e)</span> AND
-<span class="name">'activity' ∈ typeOf(a)</span>.
-
-
-<li>
-<span class='conditional'>IF</span>
<span class='name'>entity(e,attrs)</span>
<span class='conditional'>THEN</span>
<span class="name">'entity' ∈ typeOf(e)</span>.
@@ -3655,6 +3847,12 @@
<span class="name">'activity' ∈ typeOf(a)</span> AND
<span class="name">'entity' ∈ typeOf(e)</span>.
+<li>
+<span class='conditional'>IF</span>
+ <span class='name'>wasGeneratedBy(gen; e,a,t,attrs)</span>
+<span class='conditional'>THEN</span>
+<span class="name">'entity' ∈ typeOf(e)</span> AND
+<span class="name">'activity' ∈ typeOf(a)</span>.
<li>