Re: complementOf -> viewOf: proposed text: however... :-)

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