- From: James Cheney <jcheney@inf.ed.ac.uk>
- Date: Thu, 29 Sep 2011 12:07:00 +0100
- To: Graham Klyne <GK@ninebynine.org>
- Cc: W3C provenance WG <public-prov-wg@w3.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