a seemingly impossible functional program: for any
f from infinite bit sequences
Bool, his total function
f to an infinite bit sequence, such that if
True on any sequence then
find f is the least such sequence. It’s a good read
and I recommend it. (Update:
he wrote a follow-up article that defines a monad of searchable
find performs an exhaustive search by
depth-first backtracking. It’s impressive that
can be programmed totally and without inspecting the source code of
f, even though there are an uncountable
number of infinite bit sequences. Escardó makes
go faster using lazy evaluation in Haskell: his
find_iii uses an infinite sequence of lazily evaluated
bits. But it wasn’t clear to me what role lazy evaluation plays in
find_vii, which is his final, fastest version of
what some people inexplicably seem to think, I don’t know from
category theory, and I haven’t read Escardó’s paper or
LICS 2007. Still, I suspect the/an essence of
is to replace an infinite sequence of lazily evaluated bits by a
lazily evaluated binary tree of bits. To confirm this hypothesis, I
reimplemented his algorithm as follows. You can download
this post as a program.
module Exhaustive where
We represent a function from natural numbers to some type
a by an infinite binary tree whose nodes are labeled
a. To be more precise: the root node stores what
the function returns at 0; the left branch stores the return values
at positive odd integers, and the right branch stores the return
values at positive even integers.
data T a = T a (T a) (T a)
Of course, the container
T is a functor.
instance Functor T where fmap f (T z o e) = T (f z) (fmap f o) (fmap f e)
Given a value
a and a tree representing a function
f, it is easy to build another tree representing the
function g defined by g(0) =
g(n+1) = f(n).
cons :: a -> T a -> T a cons a (T z o e) = T a (cons z e) o
It is also easy to represent the identity function.
infinite :: (Num i) => T i infinite = T 0 o (fmap (1+) o) where o = fmap (\n -> n * 2 + 1) infinite
index function converts a tree back to the
function on natural numbers that it represents.
index :: (Integral i) => T a -> i -> a index _ i | i < 0 = error "index: out of range" index (T z _ _) 0 = z index (T _ o e) i | k == 0 = index e (j-1) | otherwise = index o j where (j,k) = divMod i 2
Finally, given a natural number
i and two trees
representing the functions f and g, we can build
another tree representing the function h defined by
h(n) = f(n) if
takeAppend :: (Integral i) => i -> T a -> T a -> T a takeAppend i _ _ | i < 0 = error "takeAppend: out of range" takeAppend 0 _ t = t takeAppend i (T z1 o1 e1) (T z2 o2 e2) | k == 0 = T z1 (takeAppend j o1 o2 ) (takeAppend (j-1) e1 ze2) | otherwise = T z1 (takeAppend j o1 ze2) (takeAppend j e1 o2 ) where (j,k) = divMod i 2 ze2 = cons z2 e2
Now we can define
find. It uses the tree
representation above to skip constructing long unused parts of the
infinite bit sequence.
find :: (T Bool -> Bool) -> T Bool find p = b where b = fmap (\n -> p (takeAppend n b (cons True (find (\a -> p (takeAppend n b (cons True a))))))) infinite
find by comparing computable
functions on integer sets.
type Cantor = Integer -> Bool forsome, forevery :: (Cantor -> Bool) -> Bool forsome p = p (index (find (p . index))) forevery p = not (forsome (not . p)) equal :: (Eq y) => (Cantor -> y) -> (Cantor -> y) -> Bool equal f g = forevery (\a -> f a == g a) coerce :: Bool -> Integer coerce True = 0 coerce False = 1 f',g',h' :: Cantor -> Integer f' a = a'(10*a'(3^80)+100*a'(4^80)+1000*a'(5^80)) where a' i = coerce (a i) g' a = a'(10*a'(3^80)+100*a'(4^80)+1000*a'(6^80)) where a' i = coerce (a i) h' a = a' k where i = if a'(5^80) == 0 then 0 else 1000 j = if a'(3^80) == 1 then 10+i else i k = if a'(4^80) == 0 then j else 100+j a' i = coerce (a i)
On my laptop, this code takes only several times more time and
space than Escardó’s to compare
h' to each other.
*Exhaustive> :set +s *Exhaustive> equal f' g' False (38.20 secs, 2786375560 bytes) *Exhaustive> equal f' h' True (14.10 secs, 1055343780 bytes) *Exhaustive> equal g' h' False (39.12 secs, 2762261544 bytes) *Exhaustive> equal f' f' True (13.87 secs, 1055610904 bytes) *Exhaustive> equal g' g' True (13.65 secs, 972683784 bytes) *Exhaustive> equal h' h' True (14.20 secs, 1054789196 bytes)
I take this experiment to show that a main essence of Escardó’s
algorithm is to represent a set of integers by a lazily evaluated
binary tree of bits. Maybe it’s worth defining a type class
class Find a where find :: (a -> Bool) -> a