Re: PROV-ISSUE-660 (TomDN): Constraints of PROV-Dictionary [PROV-DICTIONARY]

I am closing this issue after the vote last Thursday.

A final check of the constraints by someone to check for
typos/inconsistencies would be very helpful.

Tom

2013/4/15 Tom De Nies <tom.denies@ugent.be>

> I've made the revision, as I believe that the inferences D4 and D5 we now
> have, imply the old D8 we had, and are much more elegant and clear.
>
> https://dvcs.w3.org/hg/prov/raw-file/default/dictionary/Overview.html#membership-insertion-membership-inference
> I've also included a remark explaining this, and which constraints
> guarantee completeness.
>
> If there are objections to this change, please let us know before the vote
> on Thursday.
>
> ISSUE-660 now marked pending review.
>
> Regards,
> Tom
>
> 2013/4/15 James Cheney <jcheney@inf.ed.ac.uk>
>
>> I don't think it was discussed.  I don't have an objection, but haven't
>> had a chance to think about it very hard.  Either way, I suggest flagging
>> this as a point to revisit if there is any future activity on this (e.g.
>> formalization).  That is, if you remove a constraint that you think should
>> be implied, please mention it in a remark as something that should be
>> checked later.  If you leave it in, leave a remark saying that it appears
>> redundant (which would mean that implementations can skip it).
>>
>> --James
>>
>> On Apr 15, 2013, at 10:49 AM, Tom De Nies <tom.denies@ugent.be> wrote:
>>
>> I would have liked some feedback on this before we implement it. Any
>> thoughts?
>> Was anything said about this during last week's telecon?
>> Thanks.
>> - Tom
>>
>>
>> 2013/4/11 Tom De Nies <tom.denies@ugent.be>
>>
>>> Small correction, we need to have enough to guarantee that insertions
>>> and removals do not introduce *or remove* any key-entity pairs, other
>>> than those specified.
>>>
>>> I think the two proposed constraints are sufficient for this, unless I'm
>>> missing something.
>>>
>>> 2013/4/11 Provenance Working Group Issue Tracker <sysbot+tracker@w3.org>
>>>
>>>> PROV-ISSUE-660 (TomDN): Constraints of PROV-Dictionary [PROV-DICTIONARY]
>>>>
>>>> http://www.w3.org/2011/prov/track/issues/660
>>>>
>>>> Raised by: Tom De Nies
>>>> On product: PROV-DICTIONARY
>>>>
>>>> Luc raised some interesting ideas for the constraints.
>>>>
>>>> Note that we now have this inference:
>>>>
>>>> https://dvcs.w3.org/hg/prov/raw-file/default/dictionary/Overview.html#membership-insertion-membership-inference
>>>> Inference D4 (membership-insertion-membership) Here, KV1 is a set of
>>>> key-entity pairs and K1 is the key-set of KV1.
>>>> 1. IF prov:hadDictionaryMember(d1, e, k) and
>>>> prov:derivedByInsertionFrom(d2, d1, KV1) and k ∉ K1 THEN
>>>> prov:hadDictionaryMember(d2, e, k)
>>>> 2. IF prov:hadDictionaryMember(d2, e, k) and
>>>> prov:derivedByInsertionFrom(d2, d1, KV1) and k ∉ K1 THEN
>>>> prov:hadDictionaryMember(d1, e, k)
>>>>
>>>> (2nd part suggested by Luc)
>>>> I do have one immediate question: do we introduce an infinite loop by
>>>> doing this? (consequent of 1. appears in antecedent of 2., and vice versa)
>>>> Or is this covered by http://www.w3.org/TR/prov-constraints/#overview ?
>>>>
>>>> This got me thinking. If we have this, do we really need Inference D8?
>>>> https://dvcs.w3.org/hg/prov/raw-file/default/dictionary/Overview.html#insertion-removal-membership-inference
>>>>
>>>> Couldn't we just specify the same constraint as D4, but for removal?
>>>> Suggestion:
>>>> Inference D... (membership-removal-membership) Here, K1 is a set of
>>>> keys.
>>>> 1. IF prov:hadDictionaryMember(d1, e, k) and
>>>> prov:derivedByRemovalFrom(d2, d1, K1) and k ∉ K1 THEN
>>>> prov:hadDictionaryMember(d2, e, k)
>>>> 2. IF prov:hadDictionaryMember(d2, e, k) and
>>>> prov:derivedByRemovalFrom(d2, d1, K1) THEN prov:hadDictionaryMember(d1, e,
>>>> k)
>>>> Note that in the second case, k ∉ K1 is always true, otherwise
>>>> constraint D9 is violated.
>>>>
>>>> Do we then have enough to guarantee that insertions and removals do not
>>>> introduce any new key-entity pairs, other than those specified? (which is
>>>> why we had Inference D8)
>>>> I think so, so I'd like to propose this solution. Could we have your
>>>> support or objections via mail or on today's call?
>>>>
>>>> Regards,
>>>> Tom
>>>>
>>>>
>>>>
>>>>
>>>>
>>>>
>>>>
>>>>
>>>
>>
>>
>> The University of Edinburgh is a charitable body, registered in
>> Scotland, with registration number SC005336.
>>
>>
>