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