public
Created

Hilbert's Epsilon

  • Download Gist
Epsilon.hs
Haskell
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142
{-# LANGUAGE NPlusKPatterns, RankNTypes #-}
 
-- ransacking infinite structures quickly without side-effects
 
import Data.Maybe (fromMaybe)
import Control.Applicative
import Data.Map (Map)
import qualified Data.Map as Map
import Control.Monad
import Control.Monad.Trans.Class
import Data.Functor.Identity
 
type Cantor = Int -> Bool
 
infixr 0 #
(#) :: Bool -> Cantor -> Cantor
(x # a) 0 = x
(x # a) (i + 1) = a i
 
berger :: (Cantor -> Bool) -> Cantor
berger p = if ex $ \a -> p $ False # a
then False # berger $ \a -> p $ False # a
else True # berger $ \a -> p $ True # a
where ex q = q (berger q)
 
escardo :: (Cantor -> Bool) -> Cantor
escardo p = branch x l r where
branch x l r n = case divMod n 2 of
(0, 0) -> x
(q, 1) -> l q
(q, 0) -> r (q - 1)
x = ex $ \l -> ex $ \r -> p $ branch True l r
l = escardo $ \l -> ex $ \r -> p $ branch x l r
r = escardo $ \r -> p $ branch x l r
ex q = q $ escardo q
 
newtype S s m a = S { runS :: s -> m (a, s) }
 
instance Monad m => Functor (S s m) where
fmap = liftM
 
instance Monad m => Applicative (S s m) where
pure = return
(<*>) = ap
 
instance Monad m => Monad (S s m) where
return a = S $ \s -> return (a, s)
S m >>= k = S $ \s -> do
(a, s') <- m s
runS (k a) s'
 
instance MonadTrans (S s) where
lift m = S $ \s -> liftM (\a -> (a, s)) m
 
modulusM :: (Monad m, Real a) => (forall f. (Applicative f, Monad f) => (a -> f b) -> f c) -> (a -> m b) -> m a
modulusM phi alpha = liftM snd $ runS (phi beta) 0 where
beta n = S $ \ i -> do
a <- alpha n
return (a, max i n)
 
modulus :: Real a => (forall f. (Applicative f, Monad f) => (a -> f b) -> f c) -> (a -> b) -> a
modulus phi alpha = runIdentity $ modulusM phi (Identity . alpha)
 
foo :: Int
foo = modulus (\a -> a 10 >>= a) (\n -> n * n)
 
newtype K r s m a = K { runK :: (a -> s -> m r) -> s -> m r }
 
instance Monad m => Functor (K r s m) where
fmap = liftM
 
instance Monad m => Applicative (K r s m) where
pure = return
(<*>) = ap
 
instance Monad m => Monad (K r s m) where
return a = K $ \k -> k a
K m >>= f = K $ \k -> m $ \a -> runK (f a) k
 
instance MonadTrans (K r s) where
lift m = K $ \k s -> m >>= \a -> k a s
 
type MonadHom f g = forall x. f x -> g x
 
-- we can also build hashable versions, pure Int-based versions, and ones that can operate purely off Eq with different asymptotics.
 
neighborhoodM :: (Monad m, Ord a) => (forall f. (Applicative f, Monad f) => MonadHom m f -> (a -> f Bool) -> f Bool) -> m (Map a Bool)
neighborhoodM phi = liftM snd $ runK (phi lift beta) (\a s -> return (a, s)) Map.empty where
beta n = K $ \k s -> case Map.lookup n s of
Just b -> k b s
Nothing -> k True (Map.insert n True s) >>= \(r,t) -> case r of
True -> return (True, t)
False -> k False (Map.insert n False s)
 
neighborhood :: Ord a => (forall f. (Applicative f, Monad f) => (a -> f Bool) -> f Bool) -> Map a Bool
neighborhood phi = runIdentity $ neighborhoodM (const phi)
 
bauerM :: (Monad m, Ord a) => (forall f. (Applicative f, Monad f) => MonadHom m f -> (a -> f Bool) -> f Bool) -> m (a -> Bool)
bauerM p = do
m <- neighborhoodM p
return $ \n -> fromMaybe True $ Map.lookup n m
 
bauer :: Ord a => (forall f. (Applicative f, Monad f) => (a -> f Bool) -> f Bool) -> a -> Bool
bauer phi = runIdentity $ bauerM (const phi)
 
newtype W m a = W { runW :: m a }
 
instance Monad m => Functor (W m) where
fmap = liftM
 
instance Monad m => Applicative (W m) where
pure = return
(<*>) = ap
 
instance Monad m => Monad (W m) where
return a = W (return a)
W m >>= f = W (m >>= runW . f)
 
instance MonadTrans W where
lift = W
 
existsM :: (Monad m, Ord a) => (forall f. (Applicative f, Monad f) => MonadHom m f -> (a -> f Bool) -> f Bool) -> m Bool
existsM phi = runW $ do
q <- W $ bauerM phi
phi W (return . q)
 
exists :: Ord a => (forall f. (Applicative f, Monad f) => (a -> f Bool) -> f Bool) -> Bool
exists phi = runIdentity $ do
q <- bauerM (const phi)
phi (return . q)
 
forAllM :: (Monad m, Ord a) => (forall f. (Applicative f, Monad f) => MonadHom m f -> (a -> f Bool) -> f Bool) -> m Bool
forAllM phi = liftM not $ existsM (\hom -> liftM not . phi hom)
 
forAll :: Ord a => (forall f. (Applicative f, Monad f) => (a -> f Bool) -> f Bool) -> Bool
forAll phi = runIdentity $ forAllM (const phi)
 
(===) :: (Applicative f, Eq a) => f a -> f a -> f Bool
(===) = liftA2 (==)
 
(/==) :: (Applicative f, Eq a) => f a -> f a -> f Bool
(/==) = liftA2 (/=)

Please sign in to comment on this gist.

Something went wrong with that request. Please try again.