Re: more closed-world chatter

On May 9, 11:20 pm, "Brian Selzer" <b..._at_selzer-software.com> wrote:
> "Marshall" <marshall.spi..._at_gmail.com> wrote in message
>
> > Well, the earlier question was, given
>
> > R1(a:t1)
> > R2(a:t2)
>
> > what is the type of a in R1 join R2?
>
> > TTM says most-specific-supertype(t1, t2);
>
> I could be wrong, but I think that t1 must be either a supertype or a
> subtype of t2. If that were not true, then due to specialization by
> constraint, the sets of elements for t1 and t2 must be disjoint, and any
> join would necessarily be empty.

Sure. However you say it like there are several cases at work here, and I think it's important to note that there is just one, which (as is the case with all operations) will produce different results depending on the operand values.

> Each and every value must have one and
> only one most specific subtype.

Yeah, everyone says that. It's common point in type theory. But it's not true in set theory, unless we consider it in the degenerate case where every values belong most specifically to the set containing only itself.

Programming language types are usually expressed as named sets of values with some common structure, but neither consideration exists in set theory. I speculate that we could just use unrestricted axiomatic set theory instead of type theory, and be able to express much more sophisticated theorems about source code.

Of course, this comes at a cost in complexity and decidability, but I think it's worth exploring.

> So the type of a in R1 join R2 would be the
> type, t1 or t2, that happens to be the supertype.

Yes, that's the D&D view. Not my view though.

Marshall Received on Thu May 10 2007 - 22:46:58 CEST