Saturday, February 10, 2007

Definability and Continuity

In How Many Functions are There of Type Bool -> Bool?, I stated "The trick is to remember that if f is continuous, then f _|_ =/= _|_ implies that for all x, f x = f _|_". That is false. It would have been true had I said "… remember that if f is definable in Haskell, then …". The correct statement for continuous functions is: for all x, f x ≥ f _|_. The "≥" here is that used in domain theory to talk about CPOs.

In addition to only considering functions definable in Haskell, I was also only considering flat CPOs, in which each element is comparable only to itself and _|_. An example of a CPO that is not flat:

data Wrap = Wrap Unit
data Unit = Unit

In the CPO Wrap_|_, _|_ < Wrap _|_ < Wrap Unit. Though Wrap_|_ has three values, just like Bool_|_, there are only nine functions (continuous or definable in Haskell) of type Wrap_|_ -> Bool_|_. Furthermore, there are eleven continuous functions of type Wrap_|_ -> Wrap_|_, and all are definable in Haskell. (Thanks to Stefan O'Rear for pointing that out).

Clearly, the codomain isn't treated opaquely as it was in the last post: in order to count functions, we need to know the ordering on the codomain.

I have some more thinking to do about counting, continuity, and definability before I can make any more assertions about the cardinality of function types.


Stefan O'Rear pointed out an error in which I claimed certain functions were not definable in Haskell, when they actually are. A better example of a function that is continuous but not definable in Haskell is:

parallel_or _ True = True
parallel_or True _ = True
parallel_or False False = False

No comments: