Re: PROV-ISSUE-630 (prov-sem-fpwd-review): PROV-SEM review for FPWD [Formal Semantics]

Hi James,

The document reads nicely, congratulations on getting it in such a good 
I have raised separately my comment on soundness. If I am right, we need 
to see what
changes need to be brought it to release the document. Otherwise, it's a 
good fpwd.
There may be a few easy fixes to make in the suggestions below before 


- sotd pagraph: (this document) is on prov-constraints, and self 
reference to [prov-sem] to be removed.

- section 2.2: for convenience, we assume the order is total. What is 
the implication of this choice?

- section 2.4: wasStartedBy/wasEndedBy are missing time

- section 2.4: no bundle here? Shouldnt' we? or too slippery topic?

- section 2.5: could the final version have a go at an interpretation of 
mentionOf, even if marked as more speculative and in appendix?

- section 3.2: term interaction not defined yet.

- section 3.2.1: Can we provide some intution for value(obj,a) \subseteq 
value(thingOf(obj),a,t). What does it tell us about entities vs things.

- section 3.2.4: (the first two sets may overlap) which? Why?
   Events is not defined yet.

- section lifetime(evt)={time(t)} isn't it time(evt)?

- section 3.3: EventActivity I think allows for an event not to be 
associated with any activity. Is this desirable?

- 3.3.1: function derivedFrom linking each derivation to ITS path:
   I would suggest
         function derivedFrom linking each derivation to SOME path.
      in the case wasDerivedFrom(e1,e2,-,-,-) there may be multiple paths.

- section 4.3.1: we could add some intution: not all attributes of an
   entity object are required to be present in an entity formula.

-  4.3.2, rule_13:
     "if st is specified", what do you mean? st is always present as a 
constant or variable.  Do you mean "if st is a variable"?
     How do we have to read min(lifetime(id))=st if st is variable?

    Elsewhere, when time occurs in a formula,  there is no clause "if t 
is specified".
    Why this differnce?

- formalism 16: who do we read time(evt)=t when t is variable?

- 4.4.7: nothing in the semantics seems to indicate that lifetime of
   agent precedes that of entity.

- 4.4.12: there is some occurrence of obj_1/obj_2   which should be 

- formalism 29 (precedes)

wasGeneratedBy(gen1; e, a1, 2011-11-16T16:05:00)
wasGeneratedBy(gen2; e, a2, 2012-11-16T16:05:00) //different date

gen1 <= gen2 and gen2 <= gen1

Formalism 29 implies: 2011-11-16T16:05:00 == 2012-11-16T16:05:00
(see separate email)

On 25/02/13 12:50, Provenance Working Group Issue Tracker wrote:
> PROV-ISSUE-630 (prov-sem-fpwd-review): PROV-SEM review for FPWD [Formal Semantics]
> Raised by: James Cheney
> On product: Formal Semantics
> Hi,
> I have completed a cleanup pass on the semantics.  There are definitely still (mostly clearly-marked) areas where work is needed.
> Satya, Simon, Paolo, and Khalid had indicated willingness to review by Thursday, so that we can vote on release with other documents as part of the PR release cycle.
> Please respond to this issue with comments so that they are tracked.
> Review questions:
> 1.  Is the purpose of the document clear and consistent with the working group's consensus about the semantics?  If not, can you suggest clarifications or improvements?
> 2.  Are there minor issues that can be corrected easily prior to FPWD release?
> 3.  Are there blocking issues that must be addressed prior to release as a first public working draft?
> 4.  Are there non-blocking, but important issues that should be discussed and resolved for future editions? (no need to list TODOs already reflected in the document itself, unless there is disagreement about how to resolve them).
> --James

Professor Luc Moreau
Electronics and Computer Science   tel:   +44 23 8059 4487
University of Southampton          fax:   +44 23 8059 2865
Southampton SO17 1BJ               email:
United Kingdom           

Received on Thursday, 28 February 2013 11:40:50 UTC