22.02.2012, 09:30, "wren ng thornton"
On 2/21/12 11:27 AM, MigMit wrote:
Ehm... why exactly don't domain products form domains?
One important property of domains[1] is that they have a unique bottom element. Given domains A and B, let us denote the domain product as:
(A,B) def= { (a,b) | a <- A, b <- B }
Which will inherit an ordering in the obvious/free way from the domain orderings on A and B. Since both A and B are domains, they have bottom elements:
exists a0:A. forall a:A. (a0 <=_A a) exists b0:B. forall b:B. (b0 <=_B b)
However, there is no free ordering on:
{ (a0,b) | b <- B } \cup { (a,b0) | a <- A }
What? By definition, since, a0 <= a and b0 <= b, we have (a0, b0) <= (a0, b) and (a0, b0) <= (a0, b0), so, (a0, b0) is clearly the bottom of A\times B.
So all of those are minimal elements of (A,B) but none of them is a unique minimum; hence (A,B) is not a domain.
The smash product gets around this because it takes all those elements and makes them equal, just like a strict tuple would in Haskell.
[1] This is in the sense of domain theory. It has nothing (per se) to do with the many other uses of the term "domain" in mathematics.
Sorry, isn't the domain theory a part of mathematics?