Wednesday, August 24, 2005

Pointed domains

In a denotational semantics for a language with non-termination, you use pointed domains, i.e., CPO's with a bottom element. But some of the usual constructions on compound domains such as pairs and sums end up combining multiple bottom elements into one domain. Because the existence of a bottom element is used for the proof of the existence of fixpoints for all functions, it's critical that every domain have a single bottom element. So that's what the "coalesced sum" and "smash product" constructions are for: they identify multiple bottom elements in multiple domains into a single bottom element in the combined domain. [Abramsky and Jung 94, 3.2]

No comments: