Re: Issues of PROV Constraints

Dear Antoine,

Thanks for your comment. We raised your comments as an issue (ISSUE-576)
within the working group and have begun discussing them. In order to not
send you too much email, we will discuss this on the working group mailing
list and get back you either a resolution or to ask about further
clarification. Once we have proposed a resolution, we'll ask you to confirm
whether it addresses the points.

You can follow the discussion at:

https://www.w3.org/2011/prov/track/issues/576

Thanks for your comments and interest in PROV.

Regards
Paul

On Mon, Oct 22, 2012 at 3:04 PM, Antoine Zimmermann <
antoine.zimmermann@emse.fr> wrote:

> Dear PROV working group,
>
>
>
> I'm sorry to send my comments so late, but I hope you will take a close
> attention to what I'm saying here.
>
>
> I've read PROV data model and PROV constraints and while I find PROV-DM
> satisfying, I have concerns about PROV Constraints.
>
> The document tries to define a kind of semantics for the PROV-DM, but
> it's not actually defining a proper semantics at all. And since it does
> not truly define a formal semantics, it has to redefine the terms that
> are borrowed from logic, and subtly diverge from the standard notions
> found in logic. For someone who knows about logic, it makes the document
> larger, more complicated than it should be, more difficult to read, and
> more difficult to implement. For someone who does not know about logic,
> it's not made at all simpler, on the contrary.
>
> To give an example before getting into the details, let us examine the
> notion of PROV-equivalence, in Section 2.4. Equivalence is a well known
> and understood notion in maths and logics, which is necessarily
> reflexive. In PROV, equivalence isn't reflexive! For X to be
> PROV-equivalent to Y, it is required that both X and Y are PROV-valid,
> which is the PROV term used to say "consistent".
>
> If a proper semantics was defined, there would be no way the document
> diverge from legacy logical concepts. There would be less chances for
> mistakes in the definitions and in the rules laters. There would be more
> flexibililty in the way implementations support the semantics.
>
> I see two escapes for this:
>   1)  define an ad hoc model theory for PROV-DM, in the line of what's
> sketched in PROV-SEM;
>   2)  rely on a well known logic (such as FOL), to which all PROV
> statements are mapped, and add FOL axioms to model the constraints.
>
> 1) is ambitious and I understand there is not enough time to investigate
> it enough. But 2) is really easy. PROV statements already look a lot
> like FOL predicates, and PROV Constraints already rely heavily on FOL
> notions and notations.
>
> Definitions and inferences of 4.1 are not needed if the semantics is
> defined on the abstract syntax. The abstract syntax is not PROV-N and
> does not have "syntactic sugar" or "syntactic shortcuts". Meaning,
> relations in abstract syntax always contain all the arguments, optional
> or not, possibly with existential variables. The short forms only exist
> in the surface syntax.
>
> Inferences in 4.2, 4.3, 4.4 and 4.5 are all writable as FOL axioms.
>
> Constraints require equality and an infinite total order (Time with
> order "precedes"). This does not make the logic more complicated than FOL.
>
>
> Detailed comments:
> -----------------
>
> Section 1.2:
> """
> We define validity and equivalence in terms of a concept called
> normalization.
> """
>
> This is not required and suggests that implementations have to rely on
> normalisation. The choice of formalisation, being entirely procedural,
> imposes that normalisation is explicitely mentioned in almost all
> definitions, which in turn asks for repeatedly marking that
> implementations are not forced to produce normal forms. This obfuscates
> the document, which could be smaller and simpler.
>
>
> """
> Definitions, inferences, and uniqueness constraints can be applied to
> normalize PROV instances, and event ordering, typing, and impossibility
> constraints can be checked on the normal form to determine validity.
> Equivalence of two PROV instances can be determined by comparing their
> normal forms.
> """
>
> This also strongly suggests normalising by "applying" constraints, as
> later defined, although it is said later that normalisation is not
> required in implementations.
>
>
> """
> For PROV documents, validity and equivalence amount to checking the
> validity or pairwise equivalence of their respective documents.
> """
>
> should be: "... of their respective instances."
>
>
> """
> This specification defines how validity and equivalence are to be
> checked, if an application elects to support them at all.
> """
>
> It was said before that implementations can choose the way they check
> validity or equivalence. Again, this is a very strong suggestion that
> implementation should be made according to the presented procedures.
>
>
> """
> Applications [...] should treat equivalent instances or documents in the
> same way.
> """
>
> Does it mean that an instance in a bundle can be safely replaced by
> another equivalent instance inside the bundle?  This is important
> because it may be understood that a bundle identifier identifies the
> exact set of PROV statements given in a PROV document, or that the
> bundle identifier simply identifies the logical content of the bundle,
> or even any content that logically "implies" the content of the bundle
> in the said document.
> The definitions of equivalence and inference suggests that it is the
> later option. Note that this is something that may have to be understood
> when writing PROV documents as RDF datasets, given that RDF 1.1 is not
> specifying any particular relationship between a graph IRI and the
> content of a named graph.
>
>
> Section 2.4:
>
> """
> Merging
>
> 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 existential
> variable with another term.
> """
>
> Normally, merging is an operation that takes two terms and produce a
> single term. I do not understand what this definition has to do with
> "merging". After, it is said:
>
> """
> Merging two terms t,t' results in either substitution S such that S(t) =
> S(t'), or failure indicating that there is no substitution that can be
> applied to both t and t' to make them equal.
> """
>
> Now, merging results in a substitution. Again, it is at odd with
> standard definitions of "merging".
>
>
> """
> Applying definitions, inferences, and constraints
> """
>
> This section is really not needed if all is defined in terms of FOL.
> This section very strongly suggests one way of implementing
> PROV-CONSTRAINTS, which is not good. The description, and what's
> presented later in the normative sections, almost imposes inference
> materialisation as the normal way to implement all the logical
> operations on PROV statements (even though the spec says later, in
> passing, that implementations that lead to the same results are OK).
>
> Using the notion of "failure" again strongly suggests that the spec is
> implemented with applications of operations indicated in this section
> and in Section 6, when in fact any consistency checker would be alright
> too.
>
>
> """
> Checking ordering, typing, and impossibility constraints
>
> The ordering, typing, and impossibility constraints are checked rather
> than applied.  This means that they do not generate new formulas
> expressible in PROV,
> """
>
> This sentence again strongly suggests that constraints are "applied", in
> the sense defined previously, indicating that implementations should
> follow the operations mentioned previously, when in fact there is no
> reason to force any materialisation or "normalisastion" at all.
> This is again supported by the following sentence:
>
> "Checking such constraints follows a saturation strategy similar to that
> for normalization"
>
> What follows is again dictating an implementation when everything is in
> fact just logical formulas that have to be consistency-checked.
>
> PROV then uses the word "valid" where logic would use "consistent". In
> logic, a formula is valid iff it is necessarily true (it's a tautology).
> The use of a different term does not help non-logician (they would not
> be disturbed by the term "consistent") but may be a problem for
> logicians who are used to other terms.
>
>
> """
> Equivalence and Isomorphism
>
> [...]  This is similar to the notion of equivalence used in [RDF]
> """
>
> RDF does not defined its own notion of equivalence. Equivalence in RDF
> is simply imposed by its formal semantics, following the standard notion
> of equivalence in all logics.
>
>
> """
> [...] to be considered equivalent, the two instances must also be valid
> """
>
> This is very strange, as "equivalence" is defined as a non-reflexive
> relationship. Again, the definition of equivalence would simply follow
> from a proper formalisation in FOL or model theory.
>
> Moreover, again, the paragraph strongly suggests relying on "applying"
> normalisation to check equivalence.
>
> See comments on Section 6.1.
>
>
> """
>  From Instances to Bundles and Documents
>
> [...] a toplevel instance consisting of the set of statements not
> appearing within a bundle
> """
>
> This /seems/ to indicate that a statement in the top-level instance
> cannot be repeated in a bundle, while the PROV data model does not have
> this constraint.
>
>
> """
> Analogously to blank nodes in [RDF], the scope of an existential
> variable in PROV is the instance level
> """
>
> This is true for RDF graphs, but RDF doesn't say anything about the
> scope of bnodes in complex structures formed out of multiple RDF graphs,
> such as RDF datasets. This is therefore a constraint that must be
> indicated and highlighted in PROV.
>
>
> Section 3:
>
> This section uses vocabulary that is not yet defined normatively at this
> position in the document.
>
> """
> If determining whether two PROV instances or documents are equivalent,
> an application must determine whether their normal forms are equal
> """
>
> This is once more dictating a way of implementing, while relying on
> normal forms should be completely irrelevant, as indicated by the
> following sentence.
>
>
> Section 4.1
>
> This section defines equivalence of syntactic constructs that are purely
> a PROV-N issue. There is no reason to put this in the logic of PROV
> structures.
>
>
> Section 5.1
>
> Merging is defined in a strange way, with a procedure, which makes it
> difficult to grasp what notion it is supposed to convey.
>
>
> Section 5.2
>
> It is never specified explicitly that "strictly-precedes" is
> irreflexive. Therefore, the algorithm given in Section 6.1 for checking
> validity, which relies on this assumption, provides strictly more
> information than the definition of validity.
>
>
> Section 6.1
>
> """
> A PROV instance is valid if its normal form exists and satisfies all of
> the validity constraints
> """
>
> Here, it is not clear what "satisfies" means. Satisfaction is a standard
> term in logic, provided that a proper semantics is defined. Here, there
> is no proper semantics so the notion of satisfaction would have to be
> defined. Assuming that PROV statements are indeed mapped to FOL, and
> constraints expressed as FOL axioms, then the standard notion of
> "satisfaction" would not work here. For example, the empty document
> doesn't satisfy any of the constraints (an empty FOL theory only
> satisfies tautologies, a.k.a., valid formulas, in the usual logical
> sense of "valid").
>
> There wouldn't be any problem and it would be very much shorter with a
> proper first order semantics.
>
>
> In this section, "equivalence" does not require validity, as opposed to
> Section 2.4.
>
> Equivalence is defined according to the notion of isomorphic normal
> form, which is never normatively defined (the only definition being in
> the non-normative Section 2.4). In any case, there is no reason to rely
> on isomorphims at all, if only the logic of PROV was properly defined.
>
> Unfortunately, since equivalence is given in terms of normal forms, and
> normal forms are given purely in procedural terms, there can be no
> sensible justification for 2 instances to be non-equivalent. The
> justification would be "because the procedure gave us different
> results", which isn't satisfactory at all. This is again a drawback of
> not providing an appropriate logical account of PROV statements.
>
>
> Best regards,
> --
> Antoine Zimmermann
> ISCOD / LSTI - Institut Henri Fayol
> École Nationale Supérieure des Mines de Saint-Étienne
> 158 cours Fauriel
> 42023 Saint-Étienne Cedex 2
> France
> Tél:+33(0)4 77 42 66 03
> Fax:+33(0)4 77 42 66 66
> http://zimmer.aprilfoolsreview.com/
>
>