Collatz.hs

--partially derived from http://math.andrej.com/2007/09/28/seemingly-impossible-functional-programs/
module Collatz where

import Numeric.Natural
import qualified Data.Set as Set
import Data.Set (Set)

data Bit = Zero | One deriving (Eq, Show)
type Cantor = Natural -> Bit

(#) :: Bit -> Cantor -> Cantor
x # a = \i -> if i == 0 then x else a (i - 1)

forsome, forevery :: (Cantor -> Bool) -> Bool
find :: (Cantor -> Bool) -> Cantor

forsome p = p (find p)
forevery p = not $ forsome (not . p)

find = find_i
find_i p = if forsome (\a -> p (Zero # a))
           then Zero # find_i (\a -> p (Zero # a))
           else One # find_i (\a -> p (One # a))

search p = if forsome p then Just (find p) else Nothing

equal :: Eq y => (Cantor -> y) -> (Cantor -> y) -> Bool
equal f g = forevery (\a -> f a == g a)

ex1, ex2 :: Cantor
ex1 _ = One
ex2 = collatz

trick :: Cantor -> Natural -> Bool
trick p n = case p n of
    Zero -> False
    One -> True

data Result = Expected Int | Counterexample deriving Show
data PartialResult = Finished Result | InProgress (Set Natural) Natural deriving Show

ulam :: Natural -> Natural
ulam n = if n `mod` 2 == 0 then n `quot` 2 else 3*n + 1

syracuse :: Set Natural -> Natural -> PartialResult
syracuse s 1 = Finished (Expected (Set.size s))
syracuse s n
    | Set.member n s = Finished Counterexample
    | otherwise      = InProgress (n `Set.insert` s) (ulam n)

thwaites :: Set Natural -> Natural -> Result
thwaites s n = case syracuse s n of
    InProgress s n -> thwaites s n
    Finished r     -> r

collatz n = let (a, _) = collatz_ n in a
collatz_ :: Natural -> (Bit, Int)
collatz_ n = case thwaites Set.empty n of
    Expected x -> (One, x)
    Counterexample -> (Zero, 0)

coerce Zero = 0
coerce One = 1
proj i a = coerce (a i)
modulus f = least $ \n -> forevery $ \a -> forevery $ \b -> eq n a b --> (f a == f b)
p --> q = not p || q
least p = if p 0 then 0 else 1 + least(\n -> p (n + 1))

eq 0 a b = True
eq n a b = a m == b m && eq m a b
    where m = n - 1