W3C home > Mailing lists > Public > public-prov-wg@w3.org > September 2011

Re: Some thoughts about the revised provenance Model document

From: Graham Klyne <GK@ninebynine.org>
Date: Thu, 29 Sep 2011 14:01:23 +0100
Message-ID: <4E846C23.9060706@ninebynine.org>
To: public-prov-wg@w3.org
James,

Thanks for pointing out this to me.

#g
--

On 29/09/2011 12:07, James Cheney wrote:
>> <aside>
>> My suggested definition of IVPof might be something like this:
>>
>>   A IVPof B  iff  forall p : (Entity ->  Bool) . p(B) =>  p(A)
>>
>> where A, B are Entities, and the values of p are predicates on Entities.
>> </aside>
>>
>
> Hi Graham,
>
> Just to pick on this specifically, this definition may be too strong.  In ordinary higher-order logic or type theory, the right-hand side of the above definition is called "Leibniz equality" - it is reflexive, symmetric and transitive.  The non-obvious part is symmetry.  Suppose A IVPof B.  Take p = \lambda x. B IVPof x.  Then since B IVPof B, clearly also B IVPof A.
>
> One way to avoid this is to be more careful about what p can be , since the symmetry above results from instantiating p with a predicate involving IVPof.  For example, if p : Entity ->  Bool is restricted to, say, Boolean combinations of formulas involving attributes and values, then this would be fine.
>
> --James
Received on Thursday, 29 September 2011 14:34:49 GMT

This archive was generated by hypermail 2.2.0+W3C-0.50 : Thursday, 26 April 2012 13:06:42 GMT