src/Lambda.hs

   1 {-# OPTIONS_GHC -fno-warn-unused-do-bind #-}
   2 {-# LANGUAGE PatternSynonyms #-}
   3
   4 -- |
   5 -- Module      :  Lambda
   6 -- Copyright   :  Tomáš Musil 2014
   7 -- License     :  BSD-3
   8 --
   9 -- Maintainer  :  tomik.musil@gmail.com
  10 -- Stability   :  experimental
  11 --
  12 -- This is a toy λ-calculus implementation.
  13
  14 module Lambda
  15   ( -- * Types
  16     VarName
  17   , Term(..)
  18     -- * Parsing terms
  19   , parseTerm
  20   , tRead
  21     -- * Reduction
  22   , reduce
  23   , toNormalForm
  24   , Strategy(..)
  25   ) where
  26
  27
  28 import Data.Text as T hiding (map)
  29 import Data.Attoparsec.Text
  30 import Control.Applicative
  31 import Control.Monad.State
  32
  33 -- $setup
  34 -- >>> import Test.QuickCheck
  35 -- >>> import Control.Applicative
  36 -- >>> let aVarName = oneof . map (pure . (:[])) $ ['a'..'e']
  37 -- >>> let aVar = liftA Var aVarName
  38 -- >>> let aTerm 0 = aVar
  39 -- >>> let aTerm n = oneof [aVar, liftA2 Lambda aVarName $ aTerm (n - 1), liftA2 App (aTerm (n `div` 2)) (aTerm (n `div` 2))]
  40 -- >>> instance Arbitrary Term where arbitrary = sized aTerm
  41
  42 cP :: Term
  43 cP = tRead "(λa d c.(λa.e) b (λc.d)) ((λa.(λd.a) (λd c.b ((λa.a) a)) (a ((λa.(λd.e) ((λe.(λd b.a) (λa c.(λa a d.(λd.b (λa d.c) e) (λb b.c a (a d (λb d d e a.d (λb b.d))))) ((λb.a) c)) (d ((λc.(λd.a (λe.e)) (c d)) ((λe.b) a))) c (λa.d (e (λe.(λd c.b) a))) (c (b a)) a (λe.(λa b e b a.d) b)) ((λe.b) (λa.b)) ((λe d.b) b) e) b) ((λc c.a e) (λb.(λb.e) a)))) (λe.e) b (λd c e e c a.c)) a)"
  44
  45 cY :: Term
  46 cY = tRead "λf.(λx.f (x x)) (λx.f (x x))"
  47
  48 cI :: Term
  49 cI = tRead "λx.x"
  50
  51 cK :: Term
  52 cK = tRead "λx y.x"
  53
  54 type VarName = String
  55
  56 -- |
  57 -- >>> print $ Lambda "x" (Var "x")
  58 -- (λx.x)
  59
  60 data Term = Var VarName | Lambda VarName Term | App Term Term deriving (Eq)
  61
  62 pattern RedEx x t s = App (Lambda x t) s
  63 pattern AppApp a b c = App a (App b c)
  64 pattern EmLambda x y t = Lambda x (Lambda y t)
  65
  66
  67 instance Show Term where
  68   show (Var x) = x
  69   show (EmLambda x y t) = show (Lambda (x ++ " " ++ y) t)
  70   show (Lambda x t) = "(λ" ++ x ++ "." ++ show t ++ ")"
  71   show (AppApp a b c) = show a ++ " " ++ braced (App b c)
  72   show (App t r) = show t ++ " " ++ show r
  73
  74 braced :: Term -> String
  75 braced t = "(" ++ show t ++ ")"
  76
  77 -- |
  78 -- prop> t == tRead (show (t :: Term))
  79
  80 tRead :: String -> Term
  81 tRead s = case parseOnly (parseTerm <* endOfInput) (T.pack s) of
  82     (Right t) -> t
  83     (Left e) -> error e
  84
  85 parseVar :: Parser Term
  86 parseVar = do
  87   x <- many1 (letter <|> digit)
  88   return $! Var x
  89
  90 parseLambda :: Parser Term
  91 parseLambda = do
  92   char '\\' <|> char 'λ'
  93   vars <- sepBy1 parseVar (char ' ')
  94   char '.'
  95   t <- parseTerm
  96   return $! createLambda vars t
  97
  98 createLambda :: [Term] -> Term -> Term
  99 createLambda (Var x : vs) t = Lambda x $ createLambda vs t
 100 createLambda [] t = t
 101 createLambda _ _ = error "createLambda failed"
 102
 103 parseApp :: Parser Term
 104 parseApp = do
 105   aps <- sepBy1 (parseBraces <|> parseLambda <|> parseVar) (char ' ')
 106   return $! createApp aps
 107
 108 createApp :: [Term] -> Term
 109 createApp [t] = t
 110 createApp (t:ts:tss) = createApp (App t ts : tss)
 111 createApp [] = error "empty createApp"
 112
 113 parseBraces :: Parser Term
 114 parseBraces = do
 115   char '('
 116   t <- parseTerm
 117   char ')'
 118   return t
 119
 120 parseTerm :: Parser Term
 121 parseTerm = parseApp <|>
 122             parseBraces <|>
 123             parseLambda <|>
 124             parseVar
 125
 126 -------------------------------------------------
 127
 128 isFreeIn :: VarName -> Term -> Bool
 129 isFreeIn x (Var v) = x == v
 130 isFreeIn x (App t u) = x `isFreeIn` t || x `isFreeIn` u
 131 isFreeIn x (Lambda v t) = x /= v && x `isFreeIn` t
 132
 133 rename :: Term -> Term
 134 rename (Lambda x t) = Lambda n (substitute x (Var n) t)
 135   where n = rnm x
 136         rnm v = if (v ++ "r") `isFreeIn` t then rnm (v ++ "r") else v ++ "r"
 137 rename _ = error "TODO vymyslet reprezentaci, kde pujde udelat fce, ktera bere jen Lambdy"
 138
 139 substitute :: VarName -> Term -> Term -> Term
 140 substitute a b (Var x) = if x == a then b else Var x
 141 substitute a b (Lambda x t)
 142   | x == a = Lambda x t
 143   | x `isFreeIn` b = substitute a b $ rename (Lambda x t)
 144   | otherwise = Lambda x (substitute a b t)
 145 substitute a b (App t u) = App (substitute a b t) (substitute a b u)
 146
 147 -- | Reduce λ-term
 148 --
 149 -- >>> reduce $ tRead "(\\x.x x) (g f)"
 150 -- g f (g f)
 151
 152 reduce :: Term -> Term
 153 reduce (Var x) = Var x
 154 reduce (Lambda x t) = Lambda x (reduce t)
 155 reduce (App t u) = app (reduce t) u
 156   where app (Lambda x v) w = reduce $ substitute x w v
 157         app a b = App a (reduce b)
 158
 159 data Strategy = Eager | Lazy
 160
 161 reduceStep :: (Monad m) => Term -> m Term
 162 reduceStep (RedEx x s t) = return $ substitute x t s
 163 reduceStep t = return $ t
 164
 165 data Z = R Term Z | L Z Term | ZL VarName Z | E
 166 data D = Up | Down
 167 type TermZipper = (Term, Z, D)
 168
 169 move :: TermZipper -> TermZipper
 170 move (App l r, c, Down) = (l, L c r, Down)
 171 move (Lambda x t, c, Down) = (t, ZL x c, Down)
 172 move (Var x, c, Down) = (Var x, c, Up)
 173 move (t, L c r, Up) = (r, R t c, Down)
 174 move (t, R l c, Up) = (App l t, c, Up)
 175 move (t, ZL x c, Up) = (Lambda x t, c, Up)
 176 move (t, E, Up) = (t, E, Up)
 177
 178 unmove :: TermZipper -> TermZipper
 179 unmove (t, L c r, Down) = (App t r, c, Down)
 180 unmove x = x
 181
 182 travPost :: (Monad m) => (Term -> m Term) -> Term -> m Term
 183 travPost fnc term = tr fnc (term, E, Down)
 184   where
 185     tr f (t@(RedEx _ _ _), c, Up) = do
 186       nt <- f t
 187       tr f $ (nt, c, Down)
 188     tr _ (t, E, Up) = return t
 189     tr f (t, c, Up) = tr f $ move (t, c, Up)
 190     tr f (t, c, Down) = tr f $ move (t, c, Down)
 191
 192 travPre :: (Monad m) => (Term -> m Term) -> Term -> m Term
 193 travPre fnc term = tr fnc (term, E, Down)
 194   where
 195     tr f (t@(RedEx _ _ _), c, Down) = do
 196       nt <- f t
 197       tr f $ unmove (nt, c, Down)
 198     tr _ (t, E, Up) = return t
 199     tr f (t, c, Up) = tr f $ move (t, c, Up)
 200     tr f (t, c, Down) = tr f $ move (t, c, Down)
 201
 202 printT :: Term -> IO Term
 203 printT t = do
 204   print t
 205   return t
 206
 207 -- |
 208 --
 209 -- >>> toNormalForm Eager 100 cI
 210 -- Just (λx.x)
 211 --
 212 -- >>> toNormalForm Eager 100 $ App cI cI
 213 -- Just (λx.x)
 214 --
 215 -- >>> toNormalForm Eager 100 $ (App (App cK cI) cY)
 216 -- Nothing
 217 --
 218 -- >>> toNormalForm Lazy 100 $ (App (App cK cI) cY)
 219 -- Just (λx.x)
 220 --
 221 -- prop> (\ t u -> t == u || t == Nothing || u == Nothing) (toNormalForm Lazy 1000 x) (toNormalForm Eager 1000 x)
 222
 223
 224 toNormalForm :: Strategy -> Int -> Term -> Maybe Term
 225 toNormalForm Eager n = flip evalStateT 0 . travPost (cnt >=> short n >=> reduceStep)
 226 toNormalForm Lazy  n = flip evalStateT 0 . travPre  (cnt >=> short n >=> reduceStep)
 227
 228 cnt :: (Monad m) => Term -> StateT Int m Term
 229 cnt t@(RedEx _ _ _) = do
 230   modify (+ 1)
 231   return t
 232 cnt t = return t
 233
 234 short :: Int -> Term -> StateT Int Maybe Term
 235 short maxN t = do
 236   n <- get
 237   if n > maxN
 238     then lift Nothing
 239     else return t