Re: more closed-world chatter
Date: 8 May 2007 11:59:58 -0700
Message-ID: <1178650798.798932.125890_at_e51g2000hsg.googlegroups.com>
On May 7, 4:15 am, Jon Heggland <jon.heggl..._at_idi.ntnu.no> wrote:
>
> The crux of the matter in that prescription is the equivalence between
> R1 & R2 and R1 - (R1 - R2). How do you handle that?
On further reflection, I don't think they're equivalent.
We would say two expressions e1 and e2 on variables
A and B were equivalent if
forall A: forall B: e1(A) = e2(B)
But that's clearly not the case here. All we have here is
exists A: exists B: e1(A) = e2(B)
And that's not a very strong claim. By those criteria,
we could say that sqrt(x) and x/2 were equivalent,
because, you know, 4. The fact that there is a *category*
of A and B values for which the equation holds is
a distraction, and not compelling.
We could try to rephrase the issue in terms of unary relations, intersection, and subtraction, but that wouldn't be very interesting, because we don't care much about operators that only work on unary relations.
However, the *idea* of examining equivalences of values to see if there are equivalences of types or constraints is extremely interesting. However to get anywhere with that we have to figure out what real equivalences are. Fortunately Vadim has a nice set that applies to the Relational Lattice, and I'll be looking at those over the next few days.
Marshall Received on Tue May 08 2007 - 20:59:58 CEST