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