Exists.hs

Exists.hs

-- http://www.cs.bham.ac.uk/~mhe/papers/exhaustive.pdf
-- https://vimeo.com/32811801
type N = Int
type Cantor = N -> Bool

(#) :: Bool -> Cantor -> Cantor
(x # a) 0 = x
(x # a) n = a (n-1)

epsilon' :: (Cantor -> Bool) -> Cantor
epsilon' p =
 if exists' (\a -> p (False # a))
  then False # epsilon' (\a -> p (False # a))
  else True  # epsilon' (\a -> p (True # a))

exists' :: (Cantor -> Bool) -> Bool
exists' p = p (epsilon' p)

epsilon :: (Cantor -> Bool) -> Cantor
epsilon p = branch x l r
 where
  branch :: Bool -> Cantor -> Cantor -> N -> Bool
  branch x l r n
    | n == 0 = x
    | odd n = l ((n-1) `div` 2)
    | otherwise = r ((n-2) `div` 2)
  x::Bool
  l,r :: Cantor
  x = exists (\l -> (exists (\r -> p (branch True l r))))
  l = epsilon (\l -> (exists (\r -> p (branch x l r))))
  r = epsilon (\r -> p (branch x l r))

exists,forall :: (Cantor -> Bool) -> Bool
exists p = p (epsilon p)
forall p = not (exists (\x -> not (p x)))

equalC :: (Cantor -> N) -> (Cantor -> N) -> Bool
equalC f g = forall (\a -> f a == g a)

toN :: Bool -> N
toN True = 0
toN False = 1

f,g,h :: Cantor -> N
f a = a'(10 * a'(3^80)+100 * a'(4^80)+1000 * a'(5^80))
  where a' = toN . a
g a = a'(10 * a'(3^80)+100 * a'(4^80)+1000 * a'(6^80))
  where a' = toN . a
h a = if a'(4^80) == 0 then a' j else a'(100+j)
  where
    a' = toN . a
    i = if a'(5^80) == 0 then 0 else 1000
    j = if a'(3^80) == 1 then 10 + i else i

main = do
  print "works"
  print $ equalC (\a -> toN $ a 1) (\a -> toN $ a (10))
  print $ equalC (\a -> toN $ a 10) (\a -> toN $ a (10))
  print $ equalC f g
  print $ equalC f h