Overview

See also FormalSemantics.

The idea of this document is to sketch what aspects of the provenance model can be formalized and how they can be formalized, as a first step towards establishing a consensus on the (intended) meaning of the components of the model and the consistency constraints or inferences that can be applied to the model to distinguish good from bad provenance records.

This document is intended to synchronize with PROV-DM WD3.

Status

This is the WD3 semantics, which is being updated to become consistent with WD5.

Idea of the semantics

As a starting point, I will assume that we intend the assertions made in a PROV-DM instance to be intended to describe one, consistent state of the world, much like a logical formula is said to be satisfied in a mathematical model. That is, I propose an approach similar to that taken in model theory, where the PROV-DM instance corresponds to a formula or theory of a logic, and the semantics corresponds to what logicians call a model.

For example, the formula <math>\forall x. x \geq 0</math> is satisfied in a mathematical model where the individual elements denotable by <math>x</math> are natural numbers, and the ordering relation symbol <math>\geq</math> is interpreted as the usual ordering relation on natural numbers. Here, the goal is to come up with a plausible "intended model" for interpreting PROV-DM instances, where the formulas are assertions in PROV-DM and the individuals are things and agents. This is complicated by the fact that many statements about provenance involve talking about objects that change over time.

The modeling methodology I'm using below is similar to that used in some (old, but still relevant) work on preservation: see [1]

The word "world" is used in PROV-DM to talk about the actual state of affairs that the PROV-DM instance describes, which is what I would usually call a "model". The word "model" is used in PROV-DM mainly in the sense of "data model", that is, to talk about what I would otherwise call the syntax of PROV-DM. To avoid confusion with the uses of terms in PROV-DM, I will use "world model" to describe the mathematical structure that corresponds to actual state of affairs, and will try to avoid ambiguous, unqualified uses of the word "model".

Basics

I will use syntax for PROV-DM records (which I will usually call formulas) as described in the third working draft of PROV-DM (PROV-DM 3PWD).

A PROV-DM instance consisting of assertions <math>\phi_1</math>...<math>\phi_n</math> is interpreted as a conjunction, that is, the overall instance is considered to hold if each atomic formula in it holds.

The rest of the document will discuss the structure of the worlds and when an atomic assertion holds in a given world.

Identifiers

A lowercase symbol <math>x,y,...</math> on its own denotes an identifier. Identifiers may or may not be URIs. I view identifiers as being like variables in logic (or blank nodes in RDF): just because we have two different identifiers <math>x</math> and <math>y</math> doesn't tell us that they denote different things, since we could discover that they are actually the same later.

Times and Intervals

We assume an ordered set <math>(T,\leq)</math> of time instants. This could be a total order (i.e. a linear timeline) or a partial order describing events that are not necessarily reconciled to a single global clock.

We also consider a set <math>Intervals</math> of sets of time instants closed under "convexity", that is, such that if <math>t_1 \leq t \leq t_2</math> and <math>t_1,t_2 \in I</math> then <math>t \in I</math>. Sets of the form <math>{t \mid t_1 \leq t \leq t_2}</math> are called basic intervals - there can also be other intervals.

The common case is that <math>T</math> is a finite, linear order, for example, the set of time instants in a single place/time zone. In this case, we can represent all intervals as basic intervals, giving only the starting and ending time <math>[t_1,t_2]</math>. (If the order is infinite or dense, like the reals or rational numbers, then we need open intervals and infinite intervals too.)

Example

First consider an ordinary linear order <math>Monday < Tuesday < Wednesday < Thursday < Friday</math>. Then all of the intervals are of the form <math>[Monday,Wednesday]</math> or <math>[Tuesday,Friday]</math>.

Now consider the time point set <math>\{Monday,Tuesday, Tuesday, WednesdayNY, WednesdayCA\}</math>, where <math>Monday < Tuesday < WednesdayNY</math> and <math>Monday < Tuesday < WednesdayCA</math> are two basic intervals. The set of all time points in this example is also an interval, but it cannot be defined by taking just two time points.

Attributes and Values

We assume a set <math>Attributes</math> of attribute labels and a set <math>Values</math> of possible values of attributes.

Formulas

Summary of syntax of formulas from PROV-DM.

<math> \begin{array}{rcl}

 formula &::=& element\_formula\\
         & | & relation\_formula\\
 element\_formula
         &::= &entity(id,attrs) \\
         & |&  activity(id,st,et,attrs)\\
         & |&  agent(id,attrs)\\
 relation\_formula
         &::=& wasGeneratedBy(id,e,a,t,attrs)\\
         & |&  used(id,e,a,t,attrs)\\
         & |&  wasAssociatedWith(id,ag,act,pl,attrs)\\
         & |&  wasStartedBy(id,a,ag,attrs)\\
         & |&  wasEndedBy(id,a,ag,attrs)\\
         & |&  actedOnBehalfOf(if,ag2,ag1,act,attrs)\\
         & |&  wasDerivedFrom(id,e2,e1,act,g,u,attrs)\\
         & |&  wasDerivedFrom(id,e2,e1,t,[prov:steps=single,attrs])\\
         & |&  wasDerivedFrom(id,e2,e1,t,[prov:steps=any,attrs])\\
         & |&  alternateOf(e1,e2)\\
         & |&  specializationOf(e1,e2)

\end{array} </math>

Some additional features defined in PROV-DM 3PWD but not yet handled in the semantics are omitted. We exclude from attention derivation, annotations, accounts, and containers, since these features are in flux and non-obvious how to formalize. Also, we omit identifiers and attributes on alternateOf and specializationOf, anticipating that these features will be removed in future drafts.

World Models

Things

Things are things in the world. Each thing has a lifetime during which it exists and attributes whose values can change over time.

To model this, a world model <math>W</math> includes

• a set <math>Things</math> of things
• a function <math>lifetime : Things \to Intervals</math> from objects to time intervals
• a function <math>value : Things \times Attributes \times Times \to Values</math>

Note that this description does not say what the structure of an object is, only how it may be described in terms of its time interval and attribute values. An object could just be a record of fixed attribute values; it could be a bear; it could be the Royal Society; it could be a transcendental number like <math>\pi</math>. All that matters from our point of view is that we know how to map the object to its time interval and attribute mapping.

It is possible for two Things to be indistinguishable by their attribute values and lifetime, but have different identity.

Objects

A Object is described by a time interval and attributes with unchanging values. Objects encompass entities, interactions, and activities.

To model this, a world includes

• a set <math>Objects</math>
• a function <math>lifetime : Objects \to Intervals</math> from objects to time intervals
• a function <math>value : Objects \times Attributes \to Values</math>

Intuitively, <math>lifetime(e)</math> is the time interval during which object <math>e</math> exists; and for each <math>t \in lifetime(e)</math>, the value <math>value(e,a)</math> is the value of attribute <math>a</math> during the object's lifetime.

As with Things, it is also possible to have two different objects that are indistinguishable by their attributes and time intervals.

Entities

An entity is a kind of object that describes a time-slice of a thing, during which some of the thing's attributes are fixed. We assume:

• a set <math>Entities \subseteq Objects</math> of entities, disjoint from <math>Activities</math> and <math>Events</math> below.
• a function <math>thingOf : Entities \to Things</math> that associates each Entity with a Thing, such that for each <math>t \in lifetime(obj)</math>, and each attribute defined by <math>obj</math>, we have <math>value(obj,a) = value(thingOf(obj),a,t)</math>

Plans

We identify a specific subset of the entities called plans, <math>Plans \subseteq Entities</math>.

Agents

An agent is an entity that can act, by controlling, starting, ending, or participating in activities. Agents can act on behalf of other agents. We introduce:

• a set <math>Agents \subseteq Entities</math> of agents, which is disjoint from <math>Plans</math> and also necessarily disjoint from <math>Activities</math> and <math>Events</math>

Interactions

We consider Interactions which are split into Events between entities and activities, Associations between agents and activities, and Derivations that describe chains of generation and usage steps. (The first two sets may overlap.)

<math>Interactions = (Events \cup Associations) \uplus Derivations</math>

Events

An Event is an interaction whose lifetime is a single time instant, and relates an activity to an entity (which could be an agent). Events have types including usage, generation, starting and ending (possibly more may be added such as destruction/invalidation of an entity). Events are instantaneous. We introduce:

• A set <math>Events \subseteq Interactions</math> of events.
• A function <math>time : Events \to Times</math> giving the time of each event; i.e. <math>lifetime(evt) = {time(t)}</math>.
• The derived ordering on events given by <math>evt_1 \leq evt_2 \iff t(evt_1) \leq t(evt_2)</math>
• A function <math>type: Events \to \{start,end,use,generate\}</math> such that Events have types in <math>\{start,end,use,generate\}</math>.

Associations

An Association is an interaction relating an agent to an activity. Associations can overlap with events; for example, a start event is also an association. To model associations, we introduce:

• A set <math>Associations \subseteq Interactions</math>, such that every event <math>evt \in Events</math> that is a start or end event is also an association. That is, <math>type(evt) \in \{start,end\}</math> implies <math>evt \in Associations</math>

Associations are used below in the <math>ActsFor</math> and <math>AssociatedWith</math> relations.

Derivations

A Derivation is an interaction chaining one or more generation and use steps. Derivations can also carry attributes, so we introduce an explicit kind of interaction for them that can carry attributes.

• A set <math>Derivations \subseteq Interactions</math>, disjoint from <math>Events \cup Associations</math>.

See below for the associated derivation path and DerivedFrom relation.

Actvities

An activity is an object that encompasses a set of events. We introduce

• a set <math>Activities \subseteq Objects</math> of activities, disjoint from <math>Entities</math> and <math>Events</math>

Relations

(ISSUE-214: Luc suggests replaces <math>Generated,EventActivities</math> with <math>Generated : Events \times Entities \times Activities</math> and similar for <math>Used</math>).

Simple relations

The entities, interactions, and activities in a world model are related in the following ways:

• A relation <math>Used \subseteq Events \times Entities</math> saying when an event used an entity. An event can use at most one entity, and if <math>(evt,e)\in Used</math> then <math>time(evt) \in lifetime(e)</math> must hold.
• A relation <math>Generated \subseteq Events \times Entities</math> saying when an event generated an entity. An event can generate at most one entity, and an entity is generated by at most one event, and if <math>(evt,e)\in Generated</math> then <math>min(lifetime(e)) = time(evt)</math> must hold.
• A relation <math>EventActivity \subseteq Events \times Activities</math> associating activities with events, such that <math>(act,evt) \in EventActivity</math> implies <math>time(evt) \in lifetime(act)</math>.
• A relation <math>AssociatedWith \subseteq Association \times Agents \times Activities \times Plans^?</math> indicating when an agent is associated with an activity, and giving the identity of the association relationship, and an optional plan. This must satisfy the constraint that if <math>(assoc,ag,act,pl) \in AssociatedWith</math> then <math>lifetime(assoc) \subseteq lifetime(ag) \cap lifetime(act)</math>, i.e. the duration of the association must be within the lifetime of both the agent and the activity.
• A relation <math>ActsFor \subseteq Agents \times Agents \times Activities</math> indicating when one agent acts on behalf of another with respect to a given activity. This must satisfy the constraint that if <math>(ag_2,ag_1,act) \in ActsFor</math> then there is an association such that <math>(assoc,ag_1,act),(assoc,ag_2,act) \in AssociatedWith</math>, hence, both agents' lifetimes must overlap with some common time point in the lifetime of the activity.

Derivation paths and DerivedFrom

Recall that above we introduced a subset of interactions called Derivations. These identify paths of the form

<math>ent_n\cdot g_n\cdot act_n\cdot u_n\cdot ent_{n-1}\cdot ...\cdot ent_1\cdot g_1\cdot act_1\cdot u_1\cdot ent_0</math> where the <math>ent_i</math> are entities, <math>act_i</math> are activities, <math>g_i</math> are generations, and <math>u_i</math> are usages.

Formally, we consider the (regular) language:

• <math>DerivationPaths = Entities \cdot (Events \cdot Activities \cdot Events \cdot Entities)^+</math>

and we use this language to give meaning to derivations:

• A relation <math>derivedFrom : Derivations \to DerivationPaths</math> with the constraints that for each derivation path:

1. for each substring <math>ent\cdot g \cdot act</math> we have <math>(g,ent) \in Generated</math> (hence, <math>type(g) = generation</math>) and <math>(g,act) \in EventActivities</math>, and
2. for each substring <math>act \cdot u \cdot ent</math> we have <math>(u,ent) \in Used</math> (hence, <math>type(u) = used</math>) and <math>(u,act) \in EventActivities</math>.

Note: The reason why we need paths and not just individual derivation steps is that imprecise-n wasDerivedFrom edges can represent multiple derivation steps. Without this, we can simplify here.

Putting it all together

A world model W is a structure containing all of the above described data. If we need to talk about the objects or relations of more than one world model then we may write <math>W_1.Objects</math>; otherwise, to decrease notational clutter, when we consider a fixed world model then the names of the sets, relations and functions above refer to the components of that model.

Semantics

In what follows, let <math>W</math> be a fixed world model with the associated sets and relations discussed in the previous section, and let <math>I</math> be an interpretation of identifiers as objects in <math>W</math>.

The annotations [WF] refer to well-formedness constraints that could in principle be enforced by requiring a consistent typing of identifiers (i.e. by assuming that each identifier is associated with and can only denote an element of Entity, Agent, Note, Activity, Event, Association or Note). These could be factored out or eliminated for readability.

Interpretations

Note that the above discussion does not mention identifiers. We need to add structure to the world to link identifiers to the objects they denote. We do this using a function which we shall call an interpretation.

The mapping from identifiers to objects may not change over time. Thus, we consider interpretations as follows:

• An interpretation function <math>I : Identifiers \to Objects</math> describing which object is the target of each identifier. This is time-independent.

Satisfaction

Consider an assertion <math>\phi</math>, a world <math>W</math> and an interpretation <math>I</math>. We define notation <math>W,I \models \phi</math> which means that <math>\phi</math> is satisfied in <math>W,I</math>. For basic assertions, the definition of the satisfaction relation is given in the next few subsections. For a conjunction of assertions <math>\phi_1,\ldots,\phi_n</math> we write <math>W,I \models \phi_1,\ldots,\phi_n</math> to indicate that <math>W,I \models \phi_1</math> and ... and <math>W,I \models \phi_n</math> hold.

Attribute validity

Objects have attributes, and many

We say that an object <math>obj</math> has valid attributes <math>[attr_1=val_1,...]</math> in world <math>W</math> provided:

• for each attribute <math>attr_i</math>, we have <math>W.value(obj,attr_i) = val_i</math>.

This is sometimes abbreviated as: <math> valid(W,obj,attrs)</math>

Semantics of Element Records

Entity Records

PROV-DM refers to entity assertions <math>entity(id,attrs)</math>.

Entity assertions <math>entity(id,attrs)</math> can be interpreted as follows:

• <math>W,I \models entity(id,attrs)</math> if and only if:

1. [WF] <math>id</math> denotes an entity <math>ent = I(id) \in Entities</math>
2. the attributes are valid: <math>valid(W,ent, attrs)</math>.

Activity Records

An activity record is of the form <math>activity(id,plan,st,et,attrs)</math> where <math>id</math> is a identifier referring to the activity, <math>st</math> is a start time and <math>et</math> is an end time. There is also a set of attribute-value pairs describing additional features of the activity. We don't do anything to interpret the plan here, it is purely an annotation (e.g. pointing to a web page describing the program or service that was executed, to source code, or to some other information that might be useful).

• We say that <math>W,I \models activity(id,st,et,attrs)</math> if and only if:

1. [WF] The identifier <math>id</math> maps to an activity <math>act = I(id) \in Activities</math>
2. If <math>st</math> is specified then it is equal to the start time of the activity, that is: <math>min(lifetime(id)) = st</math>
3. If <math>et</math> is specified then it is equal to the end time of the activity, that is: <math>max(lifetime(id)) = et</math>
4. The attributes are valid: <math>valid(W,act,attrs)</math>.

Agent Records

For the purpose of the semantics so far, an agent record holds at a time instant or interval if the corresponding entity record holds and the entity denoted by the record identifier is an agent.

Agent assertions <math>agent(id,attrs)</math> can be interpreted as follows:

• <math>W,I \models agent(id,attrs)</math> if and only if:

1. [WF] <math>id</math> denotes an agent <math>ag = I(id) \in Agents</math>
2. The attributes are valid: <math>valid(W,ag,attrs)</math>.

Note records

Out of scope of the formalization.

Semantics of Relations

Entity-Activity

Generation

The generation assertion is of the form <math>wasGeneratedBy(id,e,a,t,attrs)</math> where <math>id</math> is an event (identifier), <math>e</math> is an object identifier, <math>a</math> is an activity identifier, <math>attrs</math> is a set of attribute-value pairs, and <math>t</math> is an optional time.

• <math>W,I \models wasGeneratedBy(id,e,a,t,attrs)</math> if and only if:

1. [WF] The identifier <math>id</math> denotes an event <math>evt = I(id) \in Events</math>
2. [WF] The identifier <math>e</math> denotes an object <math>obj = I(e) \in Objects</math>
3. [WF] The identifier <math>a</math> denotes an activity <math>act = I(a) \in Activities</math>.
4. The event <math>evt</math> is involved in <math>act</math>, that is, such that <math>(evt,act) \in EventActivities</math>.
5. The type of <math>evt</math> is <math>generation</math>, i.e. <math>type(evt) = generation</math>
6. The event <math>evt</math> occurred at time <math>t</math>, i.e. <math>time(evt) = t</math>
7. [Redundant?] The object <math>obj</math> came into existence at time <math>t</math>, that is, <math>min(lifetime(I(e))) = t</math>.
8. The event <math>evt</math> generated <math>obj</math>, i.e. <math>(evt,obj) \in Generated</math>.
9. The attribute values are valid: <math>valid(W,evt,attrs)</math>

Use

The use assertion is of the form <math>used(id,a,e,t,attrs)</math> where <math>id</math> denotes an event, <math>a</math> is an activity identifier, <math>e</math> is an object identifier, <math>attrs</math> is a set of attribute-value pairs, and <math>t</math> is an optional time.

• <math>W,I \models used(id,a,e,t,attrs)</math> if and only if:

1. The identifier <math>id</math> denotes an event <math>evt = I(id)

\in Events</math>.

1. [WF] The identifier <math>id</math> denotes an event <math>evt = I(id) \in Events</math>
2. [WF] The identifier <math>a</math> denotes an activity <math>act = I(id) \in Activities</math>
3. [WF] The identifier <math>e</math> denotes an object <math>obj = I(e) \in Objects</math>
4. The event <math>evt</math> is part of <math>act</math>, i.e. <math>(evt,act) \in EventActivities</math>.
5. The type of <math>evt</math> is <math>use</math>, i.e., <math>type(evt) = use</math>.
6. The event <math>evt</math> occurred at time <math>t</math>, i.e. <math>time(evt) = t</math>
7. [Redundant?] The entity <math>obj</math> existed at time <math>t</math>, i.e., <math>t \in lifetime(obj)</math>.
8. The event <math>evt</math> used <math>obj</math>, i.e. <math>(evt,obj) \in Used</math>.
9. The attribute values are valid: <math>valid(W,evt,attrs)</math>

Agent-Activity

Association Records

An association record has the form <math>wasAssociatedWith(id,a,ag,pl,attrs)</math>.

• <math>W,I \models wasAssociatedWith(id,a,ag,pl,attrs)</math> holds if and only if:

1. [WF] <math>assoc</math> denotes an association <math>assoc = I(id) \in Associations</math> is an association interaction
2. [WF] <math>a</math> denotes an activity <math>act = I(a) \in Activities</math> is an activity.
3. [WF] <math>ag</math> denotes an agent <math>agent = I(ag) \in Agents</math> is an agent.
4. [WF] <math>pl</math> denotes a plan <math>plan=I(pl) \in Plans</math> is a plan.
5. The association associates the agent with the activity and plan, i.e. <math>(assoc,agent,act,plan) \in AssociatedWith</math>.
6. The attributes are valid: <math>valid(W,assoc,attrs)</math>.

Start Records

A start record <math>wasStartedBy(id,a,ag,attrs)</math> is interpreted as follows:

• <math>W,I \models wasStartedBy(id,a,ag,attrs)</math> holds if and only if:

1. [WF] <math>id</math> denotes an event <math>evt = I(id) \in Events</math> that is also an association <math>evt \in Associations</math>
2. [WF] <math>a</math> denotes an activity <math>act = I(a)</math>
3. [WF] <math>ag</math> denotes an agent <math>agent = I(ag)</math>
4. The event <math>evt</math> has type <math>start</math>, i.e. <math>type(evt) = start</math>.
5. The agent was associated with the activity, i.e. <math>(id,ag,act) \in AssociatedWith</math>
6. The event was part of the activity, that is, <math>(act,evt) \in ActivitiesEvents</math>, and <math>min(lifetime(act)) = time(evt)</math>.
7. The attributes are valid: <math>valid(W,evt,attrs)</math>.

End Records

An activity end record <math>wasEndedBy(id,a,ag,attrs)</math> is interpreted as follows:

• <math>W,I \models wasEndedBy(id,a,ag,attrs)</math> holds if and only if:

1. [WF] <math>id</math> denotes an event <math>evt = I(id)</math> that is also an association <math>evt \in Associations</math>
2. [WF] <math>a</math> denotes an activity <math>act = I(a)</math>
3. [WF] <math>ag</math> denotes an agent <math>agent = I(ag)</math>
4. The event <math>evt</math> has type <math>end</math>, i.e. <math>type(evt) = end</math>.
5. The agent was associated with the activity, i.e. <math>(id,ag,act) \in AssociatedWith</math>
6. The event was part of the activity, that is, <math>(act,evt) \in ActivitiesEvents</math>, and <math>max(lifetime(act)) = time(evt)</math>.
7. The attributes are valid: <math>valid(W,evt,attrs)</math>.

Agent-Agent or Entity-Entity

Responsibility

The <math>actedOnBehalfOf(id,ag2,ag1,act,attrs)</math> relation is interpreted using the <math>ActsFor</math> relation as follows:

• <math>W,I \models actedOnBehalfOf(id,ag2,ag1,act,attrs)</math> holds if and only if:

1. [WF] <math>id</math> denotes an association <math>assoc=I(id) \in Associations</math> that is an association interaction, and <math>type(id) = responsibility</math>.
2. [WF] <math>a</math> denotes an activity <math>act=I(a) \in Activities</math> is an activity.
3. [WF] <math>ag1,ag2</math> denote agents <math>agent1=I(ag1), agent2=I(ag2) \in Agents</math> are agents.
4. The agent <math>agent2</math> acts for the agent <math>agent1</math> with respect to the activity <math>act</math>, i.e. <math>(agent2,agent1,act) \in ActsFor</math>.
5. [Redundant?] The association <math>id</math> associates both agents with the activity, i.e. <math>(assoc,agent1,act),(assoc,agent2,act) \in AssociatedWith</math>.
6. The attributes are valid: <math>valid(W,assoc,attrs)</math>.

Derivation

Precise-1

A precise-1 derivation record has the form <math>wasDerivedFrom(id,e2,e1,a,g,u,attrs)</math>.

• <math>W,I \models wasDerivedFrom(id,e2,e1,act,g,u,attrs)</math> if and only if:

1. [WF] <math>id</math> denotes a derivation <math>deriv = I(id) \in Derivations</math>
2. [WF] <math>e1,e2</math> denote entities <math>ent1 = I(e1), ent2=I(e2) \in Entities</math>
3. [WF] <math>a</math> denotes an activity <math>act = I(a) \in Activities</math>
4. [WF] <math>g</math> denotes a generation event <math>gen = I(g) \in Events</math> and <math>type(I(g)) = generation</math>
5. [WF] <math>u</math> denotes a use event <math>I(u) \in Events</math> and <math>type(I(u)) = used</math>
6. The derivation denotes a valid one-step derivation <math>derivedFrom(deriv) = I(e2) \cdot I(g) \cdot I(act) \cdot I(u) \cdot I(e1))</math>
7. The attribute values are valid: <math>valid(W,deriv,attrs)</math>.

Imprecise-1

An imprecise-1 derivation record has the form <math>wasDerivedFrom(id,e2,e1,t,[prov:steps=single,attrs])</math>.

• <math>W,I \models wasDerivedFrom(id,e2,e1,t,[prov:steps=single,attrs])</math> if and only if there exist <math>act \in Activities</math>, <math>g \in Events</math>, and <math>u \in Events</math> such that:

1. [WF] <math>id</math> denotes a derivation <math>deriv = I(id) \in Derivations</math>
2. [WF] <math>e1,e2</math> denote entities <math>ent1 = I(e1), ent2=I(e2) \in Entities</math>
3. <math>type(u) = used</math> and <math>type(g) = generation</math> and <math>time(g) = t</math>
4. <math>derivedFrom(deriv) = ent2 \cdot g \cdot act \cdot u \cdot ent1)</math>
5. The attribute values are valid: <math>valid(W,deriv,attrs)</math>.

Imprecise-n

An imprecise-n derivation record has the form <math>wasDerivedFrom(id,e2,e1,t,[prov:steps=any,attrs])</math>.

• <math>W,I \models wasDerivedFrom(id,e2,e1,t,[prov:steps=any,attrs])</math> if and only if there exists <math>path \in DerivationPaths</math> such that:

1. [WF] <math>id</math> denotes a derivation <math>deriv = I(id) \in Derivations</math>
2. [WF] <math>e1,e2</math> denote entities <math>ent1 = I(e1), ent2=I(e2) \in Entities</math>
3. <math>derivedFrom(deriv)= ent2 \cdot g \cdot w \cdot ent1</math> and <math> time(g) = t</math>
4. The attribute values are valid: <math>valid(W,deriv,attrs)</math>.

Specialization

The <math>specializationOf(e1,e2)</math> relation indicates when one entity record "provides a more concrete characterization of" another. This concept (like alternateOf) is in flux, but we attempt to provide a formalization to aid discussion.

• <math>W,I \models specializationOf(a,b)</math> if and only if:

1. [WF] Both <math>a</math> and <math>b</math> are entity identifiers, denoting <math>obj_1 = I(a)</math> and <math>obj_2 = I(b)</math>.
2. The two Entities refer to the same Thing, that is, <math>thingOf(obj_1) = thingOf(obj_2)</math>.
3. The lifetime of <math>obj_1</math> is contained in that of <math>obj_2</math>,i.e. <math>lifetime(obj_1) \subseteq lifetime(obj_2)</math>.
4. Every attribute <math>attr</math> of <math>obj_2</math> is also an attribute of <math>obj_1</math>, and for each such attribute we have <math>value(obj_1,attr) = value(obj_2,attr)</math>.

The second criterion says that the two Entities are descriptions of the same Things. Note that the third criterion allows <math>obj_1</math> and <math>obj_2</math> to have the same lifetime (or that of <math>obj_2</math> can be larger). The last criterion allows <math>obj_1</math> to define more attributes than <math>obj_2</math>, but they must agree on their common attributes.

Question: There has been controversy over whether <math>specializationOf</math> is transitive and/oranti-symmetric:

• Transitivity: If <math>specializationOf(a,b)</math> and <math>specializationOf(b,c)</math> hold then <math>specializationOf(a,c)</math> hold. This holds for the above definition.
• Antisymmetry: If <math>specializationOf(a,b)</math> and <math>specializationOf(b,a)</math> hold then <math>a=b</math>. This doesn't follow from the current definition (but it would if we stipulated that two entities that have the same interval, attribute and thing are equal).

Alternate

The <math>alternateOf</math> relation indicates when two entity records "provide different characterizations of the same thing".

• <math>W,I \models alternateOf(a,b)</math> if and only if:

1. [WF] Both <math>a</math> and <math>b</math> are entity identifiers, denoting <math>obj_1 = I(a)</math> and <math>obj_2 = I(b)</math>.
2. The lifetime of <math>obj_1</math> overlaps that of <math>obj_2</math>. That is, <math>lifetime(obj_1) \cap lifetime(obj_2) \neq \emptyset</math>.
3. The two objects refer to the same underlying Thing: <math>thingOf(obj_1) = thingOf(obj_2)</math>
4. For every attribute <math>attr</math> common to both <math>obj_1</math> and <math>obj_2</math>, we have <math>value(obj_1,attr) = value(obj_2,attr)</math>.

Question: There has been controversy whether <math>alternateOf</math> is symmetric and transitive:

• Symmetry: If <math>alternateOf(a,b)</math> holds then <math>alternateOf(b,a)</math> holds.
• Transitivity: If <math>alternateOf(a,b)</math> and <math>alternateOf(b,c)</math> hold then <math>alternateOf(a,c)</math> hold. This does not hold of the above definition because we require the intervals to overlap (<math>a</math> and <math>c</math> do not necessarily have overlapping lifetimes.)

We also consider the following properties which have been suggested:

• <math>specializationOf(e_1,e_2)</math> implies <math>alternateOf(e_1,e_2)</math>? (This holds at the moment.)
• <math>alternateOf(a, b)</math> if and only if there exists c such that <math>specializationOf(a,c)</math> and <math>specializationOf(b,c)</math>? (This does not necessarily hold without further assumptions about the Entities).

Problem: The above definition is symmetric. However, it is not transitive. Suppose

• <math>lifetime(obj_1) = [1,2]</math>
• <math>lifetime(obj_2) = [2,3]</math>
• <math>lifetime(obj_3) = [3,4]</math>

and suppose <math>alternateOf(obj_1,obj_2)</math> and <math>alternateOf(obj_2,obj_3)</math> hold. Then <math>alternateOf(obj_1,obj_3)</math> cannot hold since the intervals of <math>obj_1,obj_3</math> do not overlap.

Annotation records

As with note records, annotation records are considered out of scope of the formal semantics.

Semantics of Bundles and Contextualization

DRAFT - VERY QUICK AND DIRTY!

Bundles

A bundle is a named set of PROV assertions.

<math> \begin{array}{rcl} bundle &::=& bundle~id ~formula\_set ~ endBundle\\ formula\_set &::=& {formula_1,...,formula_n} \end{array}

</math>

To model this, fixing a set of entities <math>Entities</math>, we define a new structure called a <emph>contextual world</emph>, consisting of a world, a set of <emph>contexts</emph> <math>Context</math>, and a function <math>worldOf : Contexts \to Worlds</math> assigning each <math>c \in Contexts</math> a world <math>worldOf(c)</math>.

This is analogous to a SPARQL Dataset, as I understand it (but haven't checked carefully). The main world corresponds to the toplevel assertions and the others correspond to named graphs.

Semantics in the presence of Bundles

To determine whether a top-level PROV statement holds in a contextual world <math>(D,Contexts,worldOf)</math>, we add the contextual world as a parameter and test satisfaction in the default world:

<math> CW,W,I \models formula \iff ...</math>

These are defined as before, ignoring the world model. We start with <math>W = D</math> to evaluate top-level assertions.

To determine whether a bundle is satisfied in a contextual world, we simply check that the set of statements it names is satisfied in the named world.

<math> CW,W,I \models bundle(b,{formula_1,...,formula_n}) \iff CW,CW.worldOf(I(b)),I \models formula_1 \wedge ... \wedge CW,CW.worldOf(I(b)),I \models formula_n</math>

NB. Contexts are entities. The entities of the contextual world are the union of those in the default worlds and context worlds, and the contexts themselves. The interpretation function maps identifiers to these entities; however, different things may be known about the entities in different worlds (corresponding to the toplevel and bundles). The identifiers of bundles are mapped to Context entities.

Contextualization

The contextualization relation <math>contextualizationOf(e,e_b,b)</math> links an entity <math>e</math> declared in the current bundle with another entity <math>e_b</math> in a remote bundle <math>b</math>.

Semantics of contextualization

Proposal 1:

It seems that to define what we mean by contextualization we need to keep track of the current context as well as the contextual world.

• <math>(D,Contexts,worldOf),W,I \models contextualizationOf(e,e_b,b)</math> holds if and only if:

1. <math>e</math> identifies an entity in <math>W</math>, i.e. <math>obj = I(e) \in W.Entities</math>.
2. <math>b</math> identifies a context <math>ctx</math>, i.e. <math>ctx = I(b) \in Contexts</math>, which in turn identifies a world <math>W_b = worldOf(ctx)</math>
3. <math>e_b</math> identifies an entity in <math>worldOf(I(b))</math>, i.e. <math>obj_b = I(e_b) \in worldOf(ctx).Entities </math>
4. The two Entities refer to the same Thing, that is, <math>thingOf(obj) = thingOf(obj_b)</math>.
5. The lifetime of <math>obj</math> in the current world is contained in that of <math>obj_b</math>,i.e. <math>W.lifetime(obj) \subseteq W_b.lifetime(obj_b)</math>.
6. Every attribute <math>attr</math> of <math>obj_b</math> in <math>W_b</math> is also an attribute of <math>obj</math> in <math>W</math>, and for each such attribute we have <math>W.value(obj,attr) = W_b.value(obj_b,attr)</math>.

This is not quite the same as specialization, since the attributes of the different (related) entities are in different worlds: those of <math>e</math> are in the current world, and those of <math>e_b</math> are in the remote world.

Need to be careful about the Things - these are also global, not local to worlds.