Martin Escardo, 31 May 2013.

This is a set of exercises for PhD students at Warsaw University, who
know both topology and Haskell (a rare combination).

In this set of exercises, I ask you to generalize Berger's algorithm,
and other algorithms.

Let's first write a different version of Berger's algorithm for search
over the Cantor space.

> {-# LANGUAGE NPlusKPatterns #-}

> type N = Integer
> type Baire = N -> N

The Baire space is the type of sequences of natural numbers.

The Cantor space is the subset of binary sequences with values 0 and 1. 

> hd :: Baire -> N
> hd a = a 0

> tl :: Baire -> Baire
> tl a = \i -> a(i+1) 

> (#) :: N -> Baire -> Baire
> (n # a)    0  = n
> (n # a) (i+1) = a i

We have 
            hd(x # a) = x 
            tl(x # a) = a 
           (hd a) # (tl a) = a


> findCantor    :: (Baire -> Bool) -> Baire
> forsomeCantor :: (Baire -> Bool) -> Bool

> forsomeCantor p = p(findCantor p)

> findCantor p = if forsomeCantor(\a -> p(0 # a))
>                then 0 # findCantor(\a -> p(0 # a))
>                else 1 # findCantor(\a -> p(1 # a))                    

These functions search and quantify over the Cantor space. 

Q1. Topological exercise.

The Baire space has many other searchable subsets.

We know from the course that searchable sets must be compact. So let's
look at the compact subsets of Baire. Because Baire is Hausdorff, the
compact subsets are closed. Recall that we topologize Baire as
follows: We take the discrete topology on N, and the product topology
on N^N = Baire.

Q1(a) Argue that the compact subsets of Baire are precisely the closed
and bounded subsets, where we work with the pointwise order on
sequences to define boundedness.

Q1(b) Consider finitely branching trees in which each edge is labeled
by a natural number. There are no leaves: the trees are
non-well-founded and we are interested in the infinite paths starting
from the root. For example, the Cantor tree is the full binary tree
with edges labeled 0 on the left and 1 on the right. The paths are the
binary sequences.

Given such a tree, argue that its set of paths forms a compact subset
of Baire.

Q1(c) Conversely, argue that any compact subset arises as the set of
paths of such a tree.


Q2. Programming exercises.

Define in Haskell the type of finitely branching trees as follows:

> data T = Fork [(N,T)]

We consider two restrictions for the lists in the above definition:
(i) they must be nonempty (so that all paths are infinite), and (ii)
they must be finite, so that we get finitely branching trees as
discussed in the previous exercise. These conditions cannot be imposed
in Haskell (they can be imposed and verified in laguages with
dependent types such as e.g. Agda). Here we only promise to produce
correct outputs for correct trees, where the correctness is proved
externally to Haskell. Again, in dependently typed languages one can
prove the correctness in the languages themselves.

For example, the Cantor tree can be defined as follows:

> cantorTree :: T
> cantorTree = Fork [(0, cantorTree), (1, cantorTree)]

A more complicated family of finitely branching tree is this:

> unboundedBreadthTree :: N -> T
> unboundedBreadthTree n = Fork [(i, unboundedBreadthTree(n+1)) | i <- [0..n]]

Although the breadth is unbounded, the set of paths of
unboundedBreadthTree n is bounded by the infinite sequence n,n+1,n+2,
..., that is, the sequence \i -> n+i.

Q2(a) Define a generalization findT of Berger's algorithm to search
the paths of a finitely branching tree:

> findT    :: T -> (Baire -> Bool) -> Baire
> forsomeT :: T -> (Baire -> Bool) -> Bool

> forsomeT t p = p(findT t p)

> findT t p = undefined

You are supposed use the same idea as in Berger's algotithm. Any new
ideas should be reported in Q4 below.

Q2(b) We have seen that Berger's algorithm run-time is exponential in
the modulus of uniform continuity of p. We discussed the following
faster algorithm:

> findBit :: (N -> Bool) -> N
> findBit p = if p 0 then 0 else 1

> findCantor'    :: (Baire -> Bool) -> Baire
> forsomeCantor' :: (Baire -> Bool) -> Bool

> forsomeCantor' p = p(findCantor' p)

> findCantor' p = x # a 
>   where x = findBit(\x -> forsomeCantor'(\a -> p(x # a)))
>         a = findCantor'(\a -> p(x # a)) 

This is exponential in the cardinality of the indices of a that the
computation of p(a) potentially uses for an arbitrary a, and linear in
the largest index.

Define corresponding version:

> findT'    :: T -> (Baire -> Bool) -> Baire
> forsomeT' :: T -> (Baire -> Bool) -> Bool

> forsomeT' t p = p(findT' t p)

> findT' t p = undefined

Again, you are supposed the same idea as in the given algotithm. Any
new ideas should be reports in Q4 below.

Q2(c). There is also the "arboreal" algorithm for searching the Cantor
space, which reduces the above linear factor to its logarithm:

> fork :: N -> Baire -> Baire -> Baire
> fork x l r i   | i == 0    = x
>                | odd i     = l((i-1) `div` 2)
>                | otherwise = r((i-2) `div` 2)

> findCantor''    :: (Baire -> Bool) -> Baire
> forsomeCantor'' :: (Baire -> Bool) -> Bool

> forsomeCantor'' p = p(findCantor'' p)

> findCantor'' p = fork x l r 
>  where x = findBit(\x -> forsomeCantor''(\l -> forsomeCantor''(\r -> p(fork x l r))))
>        l = findCantor''(\l -> forsomeCantor''(\r -> p(fork x l r)))
>        r = findCantor''(\r -> p(fork x l r))

Generalize the arboreal algorithm to search the set of paths of any
finitely branching tree:

> findCantorT''    :: T -> (Baire -> Bool) -> Baire
> forsomeCantorT'' :: T -> (Baire -> Bool) -> Bool

> forsomeCantorT'' t p = p(findCantorT'' t p)

> findCantorT'' t p = undefined


Q3. It turns out that if epsilon : (Baire -> Bool) -> Baire is a
search operator for some undisclosed compact subset K of Baire, one
can reconstruct a finitely branching tree whose paths are the elements
of K. Write such an algorithm:

> undisclose :: ((Baire -> Bool) -> Baire) -> T
> undisclose epsilon = undefined

Hints. In the lectures, we wrote together such an undisclose function

  ((N->Bool)->N) -> [N] 

for subsets of N. This is in the file search.hs. You will need to use
this. Moreover, you may find it useful to use the fact that computable
images of searchable sets are searchable. In particular, there is a map 

  image :: (Baire -> N) -> ((Baire -> Bool) -> Baire) -> ((N->Bool)->N)
that can be used to compute the image of K under the projection 

  pi :: Baire -> N 

defined by pi a = a i.

Q4. Bonus, open ended, research question. (a) Can you find your own
better algorithms, in any suitable sense of "better"? (b) Can you
identify a particular set of predicates p:Baire->Bool which (b1) would
be both potentially useful for applications, and for which (b2) search
can be done in polynomial time?