Re: Operationalize orthogonality
Date: 8 Jun 2006 07:23:32 -0700
Message-ID: <1149776612.608660.217120_at_j55g2000cwa.googlegroups.com>
> Tony made an assertion that I read as saying that one could build a
> type generator using only booleans (which are not bits) and relations
> and I cannot see how this can be done.
Did I ? Did I /really/ ? I seem to remember asserting
"We start from ground zero (booleans, relations, type generator)." (31st May)
And in another reply to a post, I seem to remember asserting
"You're missing the type generator out, which is crucial." (1st June)
So I'm fairly sure I haven't asserted what you seem to think I did. Additionally, you asked,
"Just how does one get from the sub-sub-basement (booleans and relations) to ground zero (booleans, relations, type generator)? " (June 6th)
We have to assume that some bits of maths work to let us define anything. This is why I tend towards the type system described by Milner et al over the last 30 years or so, as it has a sufficiently formal basis to be brought into this type of framework. Date & Darwen's, although it has some nice properties, doesn't appear to have that level of rigour, or study directed at it.
Predicate calculus + lambda calculus = some form of Nirvana ? Worth the trying, I'd say. Received on Thu Jun 08 2006 - 16:23:32 CEST