PROV-ISSUE-581 (avoid-specifying-algorithm): Suggestion to avoid wording that 'almost requires' using normalization to implement constraints [prov-dm-constraints]

PROV-ISSUE-581 (avoid-specifying-algorithm): Suggestion to avoid wording that 'almost requires' using normalization to implement constraints  [prov-dm-constraints]

http://www.w3.org/2011/prov/track/issues/581

Raised by: James Cheney
On product: prov-dm-constraints

A sub-issue of ISSUE-576.

>From Antoine Zimmermann's email:
http://lists.w3.org/Archives/Public/public-prov-comments/2012Oct/0004.html



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.

...

"""
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.


...


"""
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.

Received on Thursday, 25 October 2012 16:21:42 UTC