### 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.

###### Update:

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:

Post a Comment