- From: Graham Klyne <graham.klyne@zoo.ox.ac.uk>
- Date: Fri, 13 Jan 2012 15:18:23 +0000
- To: Paolo Missier <Paolo.Missier@ncl.ac.uk>
- CC: Khalid Belhajjame <Khalid.Belhajjame@cs.man.ac.uk>, W3C provenance WG <public-prov-wg@w3.org>

On 13/01/2012 12:44, Paolo Missier wrote: > Graham > > glad you agree, however meanwhile I spotted a problem in my own proposal that > entities should form a lattice. It doesn't sit well with your axiom, because > > alternateOf(a, b) and > alternateOf(c, d) > > it follows that a,b,c,d are /all/ alternate of each other (because their def. is > now based on specialization, and specialization is transitive, and there is a > Top where they all meet). Oh yes. I guess you need multiple non-overlapping lattices, where each tops out in its own "real world thing". > But this is too much :-) > > something has to give... let me sit on transitivity of alternate while I fix the > rest of the text Of course. Is the transitivity of alternativeOf actually important for anything? ... I just had a thought, but there may be errors here as my head isn't really in this context right now. Roughly, instead of defining: alternativeOf(a, b) == exists (c) : specializationOf(a,c) and specializationOf(b,c) use something like: alternativeOf(a, b) == exists (c) : specializationOf(a,c) and specializationOf(b,c) and not exists (d) : specializationOf(c,d) and I think all the other proofs using "specializationOf" still work. Hmmm... we still need to assert or prove uniqueness of the c above. How about defining a new relation: specializeTop(a, b) == specializationOf(a, b) and not exists (z) : specializationOf(b, z) Then we can assert: specializeTop(a, b) and specializeTop(a, c) => b = c (which is the lattice-like constraint) Then, if alternateOf is defined in terms of specializeTop, I think its transitivity then follows. Further, I think this notion of specializeTop reflects the intuition we're trying to capture (see my very first comment above) #g -- > -Paolo > > > > On 1/12/12 6:32 PM, Graham Klyne wrote: >> Paolo, >> >> Summary: I think we are in agreement. I may need to re-check the text to make >> sure it doesn't still lead me to one of the misunderstandings from my earlier >> message. >> >> On 12/01/2012 10:06, Paolo Missier wrote: >>> Graham >>> >>> sorry for letting this slip. To recall, the context is that I am tasked with >>> fixing the alternateOf section of PROV-DM. >>> >>> I have a few comments to yours and Khalid's. Original text copied where needed. >>> >>> My main comment is that I like your axiomatization of the two relations, but it >>> seems to lead to properties that are not exactly what we want. But there is a >>> simple fix. >> :) >> >>> Specifically: >>> >>>> In other words, what I am suggesting is that: >>>> specializationOf(e1,e2) implies alternateOf(e1,e2) >>> that's fine, I have no problems with that. >>> >>>> *BUT*, this is not what the current text allows, since specializationOf is >>>> defined to be anti-symmetric, which means that it is also anti-reflexive: >>>> >>>> forall (a, b) : specializationOf(a,b) => not specializationOf(b,a) >>>> >>>> setting b = a we see that specializationOf(a,a) must be false, since its truth >>>> would give rise to a contradiction. >>> not really. Anti-symmetry is defined differently. I hate to quote wikipedia, as >>> I don't have the provenance of the content handy :-), but it's just >>> convenient, so: >>> http://en.wikipedia.org/wiki/Antisymmetric_relation >>> >>> basically, an anti-symmetric relation can be reflexive so that's not a problem. >> That would be good. From memory, I wasn't going so much by a definition of >> "antisymmetry" but because I though the text was suggesting something like the >> implication above. But if that's not intended, we can focus on making sure the >> text doesn't confuse. >> >>> More interestingly, about transitivity of alternateOf(): I believe we can still >>> save your axiomatization: >>>> alternativeOf(a, b) == exists (c) : >>>> specializationOf(a,c) and >>>> specializationOf(b,c) >>> just by insisting that the set of all entities forms a lattice. In fact, we only >>> need an upper semi-lattice. >> Yes, I think that's about where I'd got to, but I wasn't sure how to axiomatize >> that cleanly. >> >>> This does not ensure that >>>> specializationOf(x, y) or specializationOf(y, x) >>> but it does ensure that for each x,y, there is some z such that >>> >>> specializationOf(x, z) and specializationOf(y, z). alternateOf(a,c) follows. >>> >>> Having a top element is quite natural in class hierarchies (see owl:Thing). But >>> this should come as no surprise as all we are doing is re-invent class >>> hierarchies with a a top element. >>> >>> So in summary: >>> - I am fine with your axiomatization, plus the easy condition that entities form >>> an upper semi-lattice. >>> - I think it belongs in PROV-SEM >>> - I am inclined to keep the properties of the two relations as they are. >>> >>> (and yes, more specific may be better than more concrete). >>> >>> are we in agreement? >> On the basis of what you say here, yes. >> >> Thanks. >> >> #g >> -- >> >>> On 1/6/12 4:44 PM, Graham Klyne wrote: >>>> Paolo, >>>> >>>> I've now looked at the text and am happy with the direction, but have some >>>> niggles with the details... >>>> >>>> First a nit: you say e1 and e2 provide a more *concrete* characterization than >>>> e1. I would say more *specific* rather than more *concrete*. >>>> >>>> For the rest, using Using Khalid's comments as a spingboard: >>>> >>>> On 05/01/2012 18:43, Khalid Belhajjame wrote: >>>>> Hi, >>>>> >>>>> The new Alternate and Specialization records seem to make sense to me. >>>>> >>>>> - Looking at the definitions of *specializationOf* and *alternateOf*, I for >>>>> few >>>>> seconds was wondering if it is a good idea to define a more general >>>>> relationship >>>>> that simply says that two entity records are representations of the same >>>>> entity, >>>>> without specifying if there is difference in abstraction or context. But, I >>>>> changed my mind as a result, and I now think that the general relationship >>>>> that >>>>> I was looking for is *alternateOf* itself. Indeed, such a relationship >>>>> seems to >>>>> be usable in both cases, i.e., different abstractions and/or different >>>>> contexts. >>>>> In other words, what I am suggesting is that: >>>>> specializationOf(e1,e2) implies alternateOf(e1,e2) >>>>> >>>>> Does that make sense? >>>>> >>>> I think this depends on how the definitions are set up. >>>> >>>> I see specializationOf as a primnitive using which alternativeOf can be >>>> defined: >>>> >>>> alternativeOf(a, b) == exists (c) : >>>> specializationOf(a,c) and >>>> specializationOf(b,c) >>>> >>>> My preference is for specializationOf to be reflexive; i.e. >>>> >>>> forall (a) : specializationOf(a, a) >>>> >>>> your result follows from this: >>>> >>>> given: >>>> specializationOf(e1,e2) [per premise] >>>> specializationOf(e2,e2) [per reflexivity] >>>> >>>> we set a=e1, b=e2, c=e2 to satisfy the RHS of alternativeOf definition, hence >>>> have alternativeOf(e1, e2) as you suggest. >>>> >>>> >>>> *BUT*, this is not what the current text allows, since specializationOf is >>>> defined to be anti-symmetric, which means that it is also anti-reflexive: >>>> >>>> forall (a, b) : specializationOf(a,b) => not specializationOf(b,a) >>>> >>>> setting b = a we see that specializationOf(a,a) must be false, since its truth >>>> would give rise to a contradiction. >>>> >>>> Which in turn means that the above proof of your suggested inference does not >>>> hold. >>>> >>>> ... >>>> >>>> So my question is this: is there any particular reason to require anti-symmetry >>>> of specializationOf? >>>> >>>> (An alternative would be to modify the definition of alternativeOf, thus: >>>> >>>> alternativeOf(a, b) == exists (c) : >>>> (specializationOf(a,c) or a = c) and >>>> (specializationOf(b,c) or b = c) >>>> >>>> Absent and particular reason to do otherwise, I'd rather go with the simpler >>>> definitions.) >>>> >>>> >>>>> - *alternateOf* is transitive. >>>> I think it should be, but let's see how this plays: >>>> >>>> alternativeOf(a, b) == exists (x) : >>>> specializationOf(a,x) and >>>> specializationOf(b,x) >>>> >>>> alternativeOf(b, c) == exists (y) : >>>> specializationOf(b,y) and >>>> specializationOf(c,y) >>>> >>>> If we can show specializationOf(x, y) or specializationOf(y, x) then the result >>>> can be derived using transitivity of specializationOf and the definition of >>>> alternativeOf. >>>> >>>> We have: >>>> specializationOf(b,x) and >>>> specializationOf(b,y) >>>> >>>> Intuitively a specializationOf relation holds between x and y as their is a >>>> single non-branching path from b to the "top" of the specialization tree. But I >>>> think we need more stated constraints to derive this. >>>> >>>> Right now, I'm not sure how best to capture this, and am thinking that simply >>>> asserting the required relation would be easiest; i.e. >>>> >>>> specializationOf(b,x) and >>>> specializationOf(b,y) >>>> |= >>>> specializationOf(x,y) or specializationOf(y,x) >>>> >>>> (If specialization is anti-reflexive, we need to add "or x = y" to the above >>>> constraint.) >>>> >>>> Or maybe: >>>> >>>> specializationOf(b,x) and >>>> specializationOf(b,y) >>>> |= >>>> exists (z) : specializationOf(x,z) and specializationOf(y,z) >>>> >>>> An alternative would be to not care about this, in which case alternativeOf is >>>> not inferrable from specializationOf. Does this actually matter? >>>> >>>> #g >>>> -- >>>> >>>>> On 15/12/2011 15:25, Paolo Missier wrote: >>>>>> Hi, >>>>>> >>>>>> in response to the comments about complementarity on the wiki and on the >>>>>> list, >>>>>> we have prepared a revised version of the section, >>>>>> where "complementarity" disappears in favour of "viewOf", and the definition >>>>>> is hopefully simplified and more in line with the >>>>>> expectations: >>>>>> http://dvcs.w3.org/hg/prov/raw-file/default/model/ProvenanceModel.html#record-complement-of >>>>>> >>>>>> >>>>>> (the anchor name hasn't changed :-)) >>>>>> >>>>>> this is for feedback as per today's agenda >>>>>> >>>>>> atb -Paolo >>>>>> >>>>>> >>> > >

Received on Friday, 13 January 2012 16:00:51 UTC