# Re: Some thoughts about the revised provenance Model document

From: James Cheney <jcheney@inf.ed.ac.uk>
Date: Thu, 29 Sep 2011 12:07:00 +0100
Cc: W3C provenance WG <public-prov-wg@w3.org>
Message-Id: <2CA55FA5-2E88-4152-8200-AF728EAB1546@inf.ed.ac.uk>
To: Graham Klyne <GK@ninebynine.org>
> <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
--
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.

Received on Thursday, 29 September 2011 11:07:48 UTC

This archive was generated by hypermail 2.3.1 : Tuesday, 6 January 2015 21:58:09 UTC