- From: Paolo Missier <Paolo.Missier@ncl.ac.uk>
- Date: Sat, 14 Jan 2012 15:41:12 +0000
- To: Graham Klyne <graham.klyne@zoo.ox.ac.uk>
- CC: Khalid Belhajjame <Khalid.Belhajjame@cs.man.ac.uk>, W3C provenance WG <public-prov-wg@w3.org>
Graham the bottom line is that if we want specializationOf to be a special case (a sub-relation of) alternateOf, as Khalid has proposed, then (it seems to me that) you cannot define alternateOf in terms of specializationOf: alternativeOf(a, b) == exists (c) : specializationOf(a,c) and specializationOf(b,c) (or variations as you show below). In fact Khalid and I now have come to believe that this definition is too strong, in addition to leading to problems for transitivity. And yes, transitivity seems quite natural for this relation. It leads not to a lattice of alternates for an entity, but more simply to a cluster of alternates. So I propose that alternateOf is a primitive relation, i.e., not defined in terms of any other, and on the other hand specializationOf \subset alternateOf (and I am still late in my updates to the doc, apologies) -Paolo problem is On 1/13/12 3:18 PM, Graham Klyne wrote: > 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 >>>>>>> >>>>>>> >> -- ----------- ~oo~ -------------- Paolo Missier - Paolo.Missier@newcastle.ac.uk, pmissier@acm.org School of Computing Science, Newcastle University, UK http://www.cs.ncl.ac.uk/people/Paolo.Missier
Received on Saturday, 14 January 2012 15:42:22 UTC