- From: Stian Soiland-Reyes <soiland-reyes@cs.manchester.ac.uk>
- Date: Mon, 3 Sep 2012 14:56:14 +0100
- To: James Cheney <jcheney@inf.ed.ac.uk>
- Cc: Jun Zhao <jun.zhao@zoo.ox.ac.uk>, public-prov-wg@w3.org
I have reviewed section 2.4 Validation Process Overview in http://dvcs.w3.org/hg/prov/raw-file/default/model/prov-constraints.html#validation-process-overview-1 Over all, this is a very solid section. I would change a few tiny things: > An inference of the form IF A1 and ... and Al THEN there exists y1...ym such that B1 and ... and Bk can be thought of as a formula ∀ x1,....,xn. A1 ∧ ... ∧ Al ⇒ ∃ y1...ym . B1 ∧ ... ∧ Bk, where x1...xn are the free variables of the inference. I would change "Al" to "Ah" (or a different letter not used already!) - as l (L) and 1 (one) look very similar with the fonts chosen. > In our setting, the defined formulas A are never used in other formulas, so it is sufficient to replace all occurrences of A with their definitions. The formula A is then redundant, and can be removed from the instance. I checked this - and it's true, except for this: > Inference 16 (alternate-reflexive) > IF entity(e) THEN alternateOf(e,e). entity(e) --> entity(e, _attrs) (Otherwise it would be wiped by definition 2!) > Constraint 48 (specialization-invalidation-ordering) > IF specializationOf(e1,e2) and wasInvalidatedBy(inv1; e1,_a1,_t1,_attrs1) and class="name">wasInvalidatedBy(inv2; e2,_a2,_t2,_attrs2) THEN inv1 precedes inv2. Fix HTML error. With regards to this issue (ISSUE-465) about infinite inferences, the section as it now explains it is good, and the issue can be closed (which I have). On Thu, Aug 30, 2012 at 7:20 PM, James Cheney <jcheney@inf.ed.ac.uk> wrote: > Hi all, > > PROV-CONSTRAINTS has been revised as planned, and I have gone through the comments to ensure that we've addressed all remaining substantive issues. > > The "Validation Process Overview" now contains the promised text to explain the design. > > Please check whether this satisfactorily addresses the infinite inference issue. (I will be adding details of the proof that this can't happen soon, but it is important to make sure it's also explained well to people that won't want to read the proof.) > > Please review so that we can close this issue by next Thursday, when the vote on last call release is planned. > > --James > > On Aug 9, 2012, at 5:06 PM, Stian Soiland-Reyes wrote: > >> Looks like this is the right direction. I'm not closing the issue yet, >> as the section is not finished, but you have addressed my concern. >> >> On Thu, Aug 9, 2012 at 3:03 PM, James Cheney <jcheney@inf.ed.ac.uk> wrote: >>> Hi, >>> >>> To (begin to ) address the issue and hopefully also satisfy requests from reviewers for better intuition about how normalization/validity checking/equivalence checking work, I have added an outline of the validation process (complementing Tim's contributed figure). >>> >>> This is work in progress, but I hope it can give people confidence that this issue is addressed (and can be explained so that it is clear to other readers that it is addressed). >>> >>> I have marked this pending review, hopefully we can close it or identify further action to take to resolve it during the meeting. >>> >>> --James >>> >>> On Aug 9, 2012, at 11:25 AM, Jun Zhao wrote: >>> >>>> James and Stian, >>>> >>>> On 08/08/2012 11:33, James Cheney wrote: >>>>> OK, I will revise to make this clearer. This can be done by adding explanation rather than by making technical changes, though, so we should focus on resolving the other issues now. >>>>> >>>> >>>> +1 >>>> >>>> -- Jun >>>> >>>> >>>>> --James >>>>> >>>>> On Aug 8, 2012, at 11:02 AM, Stian Soiland-Reyes wrote: >>>>> >>>>>> On Wed, Aug 8, 2012 at 10:47 AM, James Cheney <jcheney@inf.ed.ac.uk> wrote: >>>>>>> I understand your concern. At a purely technical level, we avoid nontermination, but only by drawing a fine distinction between having an entity(e) statement in the instance, and "knowing e is an entity" (represented by entity' \in typeOf(e)). >>>>>>> >>>>>>> We (me, Luc, Paolo, Tom) discussed three ways of avoiding this problem, before finalizing the review copy: >>>>>>> >>>>>>> 1. Drop the entity-generation-invalidation and activity-start-end inferences altogether. >>>>>>> 2. Add some limitation to inference (such as your suggestion of not triggering inferences on generated existential variables, or applying the ) that recovers finiteness. >>>>>>> 3. [what we have done] demote the type inferences to only infer constraints like 'entity' in typeof(id) , not add new statements like entity(e) to the PROV instance. >>>>>>> >>>>>>> Of the three, the one with strongest consensus was (3). Some of us strongly felt that the e-g-i and a-s-e inferences are needed. Others, including me, strongly felt that (2) would be a bad idea, as it breaks the connection to logic (i.e., the e-g-i and a-s-e and may have more radical unforeseen consequences. >>>>>> >>>>>> OK, I see now that you have thought about this. It would be useful if >>>>>> some of those considerations shone through to the document. I can >>>>>> agree on argument 3 if we formulate it well, explicitly. >>>>>> >>>>>> I agree that the inferences are needed, or at least useful. >>>>>> >>>>>>> We believed that (3) was an acceptable compromise (if a bit hacky), but, I'm not sure how the group as a whole would feel. That is why I'm laying out the options we considered. >>>>>>> So, my proposal would be to make this distinction clearer (and explain why) so that it does not surprise or bite people... >>>>>> >>>>>> I would think this is the best approach, rather than dropping the >>>>>> inferences all together, as the rest of the constraints rely on them. >>>>>> >>>>>> -- >>>>>> Stian Soiland-Reyes, myGrid team >>>>>> School of Computer Science >>>>>> The University of Manchester >>>>>> >>>>>> >>>>> >>>>> >>>> >>>> -- >>>> Jun Zhao, PhD >>>> EPSRC Postdoctoral Fellow >>>> Department of Zoology >>>> University of Oxford >>>> Tinbergen Building, South Parks Road >>>> Oxford, OX1 3PS, UK >>>> >>>> >>> >>> >>> -- >>> The University of Edinburgh is a charitable body, registered in >>> Scotland, with registration number SC005336. >>> >> >> >> >> -- >> Stian Soiland-Reyes, myGrid team >> School of Computer Science >> The University of Manchester >> >> > > > -- > The University of Edinburgh is a charitable body, registered in > Scotland, with registration number SC005336. > -- Stian Soiland-Reyes, myGrid team School of Computer Science The University of Manchester
Received on Monday, 3 September 2012 13:57:05 UTC