--- a/semantics/prov-sem.html Tue Apr 02 18:45:04 2013 +0100
+++ b/semantics/prov-sem.html Wed Apr 03 12:15:57 2013 +0100
@@ -910,7 +910,7 @@
// if you wish the publication date to be other than today, set this
- publishDate: "2013-04-30",
+ // publishDate: "2013-04-30",
// if the specification's copyright date is a range of years, specify
// the start date here:
@@ -1234,14 +1234,15 @@
</p>
</section>
-<!--
+
<section>
-<h3> Times and Intervals </h3>
+<h3> Times </h3>
<p>We assume an ordered set $(Times,\leq)$ of time instants, where
$Times \subseteq Val$ and $\leq$ is a linear order.
</p>
+
<div class="remark">
<p>Restricting attention to linearly-ordered times, and imposing this
order on events, is a simplifying assumption; it is more restrictive than required to model the
@@ -1260,7 +1261,7 @@
</section>
- -->
+
@@ -1688,7 +1689,7 @@
function $associatedWith : Associations \to Agents \times Activities \times Plans_\bot$.
</p>
</div>
-
+ </section>
<section>
<h5> Attributions </h5>
@@ -3501,11 +3502,192 @@
<section id="completeness">
<h3>Weak Completeness</h3>
-
+<p> In this section we give a translation from valid PROV instances to
+ structures, and show that a valid PROV instance has a model.</p>
+
+
+ <p> Let $I$ be a valid PROV instance that is in normal form.
+ We define a structure $M(I)$ as follows, by giving the sets,
+ functions and relations specified in the components in <a
+ href="#structures">Section 3</a>.</p>
+
+ <section>
+<h4>Sets</h4>
+ <p> The sets of structure $M(I)$ are: </p>
+
+ \[
+ \begin{eqnarray*}
+ Entities &=& \{id \mid entity(id,attrs) \in I\}\\
+ Plans &=& \{pl \mid wasAssociatedWith(id,ag,act,pl,attrs) \in I, pl
+ \neq \bot\}\\
+ Collections &=& \{e \mid memberOf(e',e) \in I\} \\
+ &\cup& \{e \mid
+ entity(e,attrs) \in I, prov:type=prov:emptyCollection \in attrs\}\\
+
+ Activities &=& \{id \mid activity(id,attrs) \in I\}\\
+ Agents &=& \{id \mid agent(id,attrs) \in I\}\\
+ \\
+ Usages &=& \{id \mid used(id,a,e,t,attrs) \in I\}\\
+ Generations &=& \{id \mid wasGeneratedBy(id,e,a,t,attrs) \in I\}\\
+ Invalidations &=& \{id \mid wasInvalidatedBy(id,e,a,t,attrs) \in I\}\\
+ Starts &=& \{id \mid wasStartedBy(id,a,e,a',t,attrs) \in I\}\\
+ Ends &=& \{id \mid wasEndedBy(id,a,e,a',t,attrs) \in I\}\\
+ Events &=& Usages \cup Generations \cup Invalidations \cup Starts
+ \cup Ends\\
+ \\
+ Associations &=& \{id \mid wasAssociatedWith(id,ag,act,pl,attrs) \in
+ I\}\\
+ Attributions &=& \{id \mid wasAttributedTo(id,e,ag,attrs) \in I\}\\
+ Delegations &=& \{id \mid actedOnBehalfOf(id,ag_2,ag_1,act,attrs) \in I\}\\
+ Communications &=& \{id \mid wasInformedBy(id,a_2,a_1,attrs) \in I\}\\
+ Derivations &=& \{id \mid wasDerivedFrom(id,e_2,e_1,a,g,u,attrs) \in I\}\\
+\\
+ Influences &=& Events \cup Associations \cup Attributions \cup
+ Communications \cup Delegations\\
+ &\cup & \{id \mid wasInfluencedBy(id,q_2,q_1,attrs) \in I\}\\
+ \\
+ Objects &=& Entities \cup Activities \cup Agents \cup Influences\\
+ \end{eqnarray*}
+ \]
+ <p> In addition, to define the set of $Things$, we introduce an
+ equivalence relation on $Entities$ as follows:
+ </p>
+ \[e_1 \equiv e_2 \iff alternateOf(e_1,e_2) \in I\]
+ <p>The fact that this is an equivalence relation follows from the
+ fact that $I$ is in normal form, since the constraints on
+ $alternateOf$ ensure that it is an equivalence relation. Recall
+ that givne an equivalence relation $\equiv$ on some set $X$, the
+ <em>equivalence class</em> of $x \in X$ is the set $[x]_\equiv = \{y
+ \in X \mid x
+ \equiv y\}$. The <em>quotient</em> of $X$ by an equivalence
+ relation on $X$ is the set of equivalence classes, $X_\equiv =
+ \{[x]_\equiv \mid x \in X\}$. Now we
+ define the set of $Things$ as equivalence classes of $Entities$
+ modulo $\equiv$.</p>
+
+\[Things = Entities /_{\equiv} = \{[e]_\equiv \mid e \in Entities\}\]
+
+<p> Observe that since $I$ is normalized and valid, entities and
+activities are disjoint, the influences are disjoint from entities,
+activities, and agents,
+and the different subsets of events and influences are pairwise
+disjoint, as required.</p>
+</section>
+<section>
+<h4>Functions</h4>
+
+<p> First, we consider the functions associated with $Entities$. We
+employ an auxiliary function $events:Entities \to P(Events)$ that collects the set of all
+events in which $e$ participated.</p>
+\[
+\begin{eqnarray*}
+events(e) &=& \{id \mid used(id,a,e,t,attrs) \in I\}\\
+&\cup& \{id \mid wasGeneratedBy(id,e,a,t,attrs) \in I\}\\
+&\cup& \{id \mid wasInvalidatedBy(id,e,a,t,attrs) \in I\}\\
+&\cup& \{id \mid wasStartedBy(id,a,e,a',t,attrs) \in I\}\\
+&\cup& \{id \mid wasEndedBy(id,a,e,a',t,attrs) \in I\}\\
+lifetime(e) &=& \{time(e) \mid evt \in events(e)\}\\
+value(e,a) &=& \{v \mid entity(e,attrs) \in I, a=v \in attrs\}\\
+thingOf(e) &=& [e]_\equiv
+\end{eqnarray*}
+\]
+<p> Similarly, for $Things$, we
+employ an auxiliary function $events:Things \to P(Events)$ that collects the set of all
+events in which one of the entities constituting the thing participated.</p>
+\[
+\begin{eqnarray*}
+events(T) &=& \bigcup_{e \in T} events(e)\\
+lifetime(e) &=& \{time(e) \mid evt \in events(T)\}\\
+value(T,a,t) &=& \bigcup_{e \in T, t \in lifetime(e)} value(e,a)\\
+\end{eqnarray*}
+\]
+<div class="note">
+ <p> TODO: The above treatment of time/lifetime is flawed, as we are
+defining lifetimes to be sets of times, not intervals. What if
+ some of the times are symbolic?</p>
+ </div>
+
+<p> The function $time$ mapping $Events$ to their $Times$ is defined
+ as follows:
+ </p>
+ \[\begin{eqnarray*}
+ time(id) &=& t \text{ where } used(id,a,e,t,attrs) \in I\\
+ time(id) &=& t \text{ where } wasGeneratedBy(id,e,a,t,attrs) \in I\\
+time(id) &=& t\text{ where } wasInvalidatedBy(id,e,a,t,attrs) \in I\\
+time(id) &=& t \text{ where } wasStartedBy(id,a,e,a',t,attrs) \in I\\
+time(id) &=& t \text{ where }wasEndedBy(id,a,e,a',t,attrs) \in I\\
+\end{eqnarray*}
+ \]
+
+
+ <p>Finally, the functions giving the interpretations of the
+ different identified influences are as follows:
+ </p>
+\[\begin{eqnarray*}
+ used(id) &=& (a,e) \text{ where } used(id,a,e,t,attrs) \in I\\
+ generated(id) &=& (e,a) \text{ where } wasGeneratedBy(id,e,a,t,attrs) \in I\\
+ invalidated(id) &=& (e,a) \text{ where } wasInvalidatedBy(id,e,a,t,attrs) \in I\\
+ started(id) &=& (a,e,a') \text{ where } wasStartedBy(id,a,e,a',t,attrs) \in I\\
+ ended(id) &=& (a,e,a') \text{ where }wasEndedBy(id,a,e,a',t,attrs) \in I\\
+ \\
+ associatedWith(id) &=& (ag,act,pl) \text{ where } wasAssociatedWith(id,ag,act,pl,attrs) \in
+ I\\
+ attributedTo(id) &=& (e,ag) \text{ where } wasAttributedTo(id,e,ag,attrs) \in I\\
+actedFor (id) &=& (ag_2,ag_1,act) \text{ where } actedOnBehalfOf(id,ag_2,ag_1,act,attrs) \in I\\
+ communicatedBy(id) &=& (u,g) \text{ where }
+ \{wasInformedBy(id,a_2,a_1,attrs),
+ wasGeneratedBy(g,e,a_1,t_1,attrs_1), used(u,a_2,e,t_2,attrs_2)\} \subseteq I\\
+ derivationPath(id) &=& e_2\cdot g \cdot a \cdot u \cdot e_1 \text{ where } wasDerivedFrom(id,e_2,e_1,a,g,u,attrs) \in I\\
+ derivationPath(id) &=& e_2\cdot g_{id} \cdot a_{id} \cdot u_{id} \cdot e_1 \text{ where } wasDerivedFrom(id,e_2,e_1,-,-,-,attrs) \in I\\
+ \end{eqnarray*}
+ \]
+ <p>Note that since $I$ is normalized and valid, by the uniqueness
+ constraints these functions are all well-defined. In the case for
+ imprecise derivations, we generate additional activities, generations
+ and usages linking $e_2$ to $e_1$.
+ </p>
<div class="note">
- TODO: Translate valid instances (via normal forms) to models, to
- obtain a weak form of completeness.
- </div>
+ <p>TODO: Communication is slightly weird, as the generation and use
+ might not be unique.</p>
+ <p> TODO: Derivation is also slightly weird, since there is no
+ guarantee that a multi-step derivation exists in the imprecise case
+ (and no way to force this). So in the case for imprecise we simply
+ generate a new one-step activity/generation/use path. We need to
+ add these to $Activities$, $Generations$ and $Usages$ along with
+ appropriate function values for $used$ and $generated$.</p>
+ </div>
+</section>
+<section>
+<h4>Relations</h4>
+<p>We introduced a relation $\equiv$ corresponding to $alternateOf$
+ above, in defining $Things$, but this relation is not a component of
+ the semantics.</p>
+ <p>The event ordering relation is defined as follows:</p>
+ \[evt \preceq evt' \iff (evt,evt') \in G_I\]
+ <p> Here, we are using a slight abuse of notation: we write $G_I$
+ for the directed graph that is used during validation of $I$ to
+ test for cycles amond event ordering constraints. See Sec. 7.1 of PROV-CONSTRAINTS [[PROV-CONSTRAINTS]].</p>
+
+ <p> Finally, the collection membership relation $MemberOf$ is
+ defined as follows:</p>
+ \[(e,c) \in MemberOf \iff memberOf(e,c) \in I\]
+
+</section>
+<section>
+<h4>Main results</h4>
+
+<p> The main results of this section are that if a valid PROV instance
+ $I$ normalizes to
+ $I'$, then $M(I') \models I$, and that furthermore $M(I')$
+ satisfies all of the inferences and constraints. Thus, a form of
+ completeness holds: every valid PROV instance has a model.</p>
+
+<div class="theorem">
+ <p>Suppose $I$ is a valid, normalized PROV instance, and let $M(I)$
+ be the corresponding structure. Then $M(I)$ satisfies all of the
+ inferences and constraints.</p>
+</section>
+
</section>
</section>