-------------------------------------------------------------------
--                                                               --
-- Infinite sets that admit fast exhaustive search               --
--                                                               --
-- Companion Haskell program for the paper with same title.      --
--                                                               --
-- Martin Escardo, Summer 2006.                                  --
--                                                               --
-- This will be rewritten to perfectly match the paper           --
--                                                               --
-------------------------------------------------------------------

type N = Integer
type Bit = Int
type Cantor = N -> Bit

-- Realizers for exhaustively searchable sets:

type Searcher d = (d -> Bool) -> d

-- Universal and existential quantifiers:

type Quantifier d = (d -> Bool) -> Bool

-- Basic examples.
--
-- Realizers for searchability are named after
-- the sets they search over:

bool :: Searcher Bool
bit  :: Searcher N
z    :: N -> Searcher N
l    :: [N] -> Searcher N

bool = \p -> p True
bit  = \p -> if p 0 then 0 else 1

z 0 = undefined
z 1 = \p -> 0
z n = \p -> if p (n-1) then n-1 else z(n-1) p

l [] = undefined
l [a] = \p -> a
l (a:s) = \p -> if p a then a else l s p

-- Boolean-valued quantifiers:

forsome, forevery :: Searcher d -> Quantifier d
forsome s p = p(s p)
forevery s p = not(forsome s(\x -> not(p x)))

-- Function equality:

equal :: Eq e => Searcher d -> (d -> e) -> (d -> e) -> Bool
equal s f g = forevery s(\x -> f x == g x)

-- Factory of exhaustively searchable sets:

image :: (d -> e) -> Searcher d -> Searcher e
image f s = \q -> f(s(\x -> q(f x)))

times :: Searcher d -> Searcher d' -> Searcher(d,d')
(s `times` s') p = (x,x')
     where x = s (\x -> forsome s'(\x' -> p(x,x')))
           x'= s'(\x'-> p(x,x'))


-- Without memoization (the name doesn't match the paper):

prod' :: (N -> Searcher d) -> Searcher(N -> d)
prod' e p n = e n (\x->q n x(prod'(\i->e(i+n+1))(q n x)))
  where q n x a = p(\i -> if i  < n then prod' e p i
                     else if i == n then x
                                    else a(i-n-1))

-- With:

prod :: (N -> Searcher d) -> Searcher(N -> d)
prod e p = b
  where b = id'(\n->e n (\x->q n x(prod(\i->e(i+n+1))(q n x))))
        q n x a = p(\i -> if i  < n then b i
                     else if i == n then x
                                    else a(i-n-1))

-- More interesting examples of exhaustively searchable subspaces:

bcantor :: Searcher (N -> Bool)
bcantor = prod(\i -> bool)

cantor, tcantor, qcantor :: Searcher (N -> N)
cantor = prod(\i -> bit)
tcantor = prod(\i -> z 3)
qcantor = prod(\i -> z 4)

factorial :: Searcher (N -> N)
factorial = prod(\i -> z(i+1))

cantorw :: Searcher(N -> N -> Bool)
cantorw = prod(\i -> bcantor)

-- Function memoization.
-- Amounts to convoluted implementation of the identity.
-- Adds logarithmic time overhead, but avoids re-evaluation.

data T x = B x (T x) (T x)

code :: (N -> x) -> T x
code f = B (f 0) (code(\n -> f(2*n+1))) 
                 (code(\n -> f(2*n+2)))

decode :: T x -> (N -> x)
decode (B x l r) n |  n == 0    = x
                   |  odd n     = decode l ((n-1) `div` 2)
                   |  otherwise = decode r ((n-2) `div` 2)

id' :: (N -> a) -> (N -> a)
id' = decode.code

-- Modulus of continuity on the Cantor space.

fan :: Eq y => ((N -> Bool) -> y) -> N
fan f = mu(\n->foreveryC(\a->foreveryC(\b->eq n a b ==> (f a == f b))))

mu :: (N -> Bool) -> N
mu p = if p 0 then 0 else 1 + mu(p.(1+))

foreveryC = forevery bcantor
foreveryZ n = forevery (z(n+1))

False==>p=True
True ==>p=p

eq n a b = foreveryZ n(\i -> a i == b i)

-- Another product functional

(x # a)(i) = if i == 0 then x else a(i-1)
tl a = \i -> a(i+1) 

prod'' e p = 
  let x = e 0(\x->p(x#(prod''(tl e)(\a->p(x#a)))))
  in x#(prod''(tl e)(\a->p(x#a)))

-- berger

berger :: (Cantor  -> Bool) -> Cantor
berger p = if p(0 # berger(\a -> p(0 # a)))
           then 0 # berger(\a -> p(0 # a))
           else 1 # berger(\a -> p(1 # a))


-- Set equality.

proj :: N -> (N -> Bool) -> Bool
proj n = \a -> a n

eqnat :: N -> N -> Bool
eqnat m n = equal bcantor (proj m) (proj n)

projset :: [N] -> ((N -> Bool) -> Bool)
projset [] = \a -> True
projset (n:l) = \a -> (a n) && (projset l a)

eqset :: [N] -> [N] -> Bool
eqset k l = equal bcantor (projset k) (projset l)

-- Concluding examples.
-- Much slower if we instead set id' = id.
-- But still can compare the following functions.

f,g,h :: (N -> N) -> N

f a = 10*a(3^400)+100*a(4^400)+1000*a(5^400)

g a = 10*a(3^400)+100*a(4^400)+1000*a(6^400)

h a = 10 + if a(4^400) == 1 then j+100 else j
    where i = if even(a(5^400)) then 0 else 1000
          j = if  odd(a(3^400)) then i else i-10

hh a = 100 + if a(4^400) == 0 then j-100 else j 
    where i = if a(5^400) == 0 then 0 else 1000
          j = if a(3^400) == 1 then 10+i else i
  
-- More:

f',g',h' :: (N -> N) -> N

        
f' a = a(10*a(3^80)+100*a(4^80)+1000*a(5^80))

g' a = a(10*a(3^80)+100*a(4^80)+1000*a(6^80))

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 

false2 = forsome cantor (\a->a(5^500)+a(6^600)+a(7^700)+a(8^800)+a(9^900)>=4^400)

false3 = forsome tcantor (\a->a(5^500)+a(6^600)+a(7^700)+a(8^800)+a(9^900)>=4^400)

false5 = forsome tcantor (\a->a(5^500)*a(6^600)*a(7^700)*a(8^800)*a(9^900) > 2^5)

w = [a(5^500),a(6^600),a(7^700),a(8^800),a(9^900)]
  where a = tcantor (\a->a(5^500)*a(6^600)*a(7^700)*a(8^800)*a(9^900) == 2^3)

w' = [a(5^500),a(6^600),a(7^700),a(8^800),a(9^900)]
  where a = qcantor (\a->a(5^500)*a(6^600)*a(7^700)*a(8^800)*a(9^900) == 2*3)

-- This is too slow, of course:

w'' = [a(5^500),a(6^600),a(7^700),a(8^800),a(9^900)]
  where a = factorial (\a->a(5^500)*a(6^600)*a(7^700)*a(8^800)*a(9^900) == 2*3*5*7)


-- But this is ok:

example = [a 2, a 3, a 4, a 5]
  where a = factorial (\a->a 2 * a 3 * a 4 * a 5== 2*2*3*4)


-- End of file.