Lambda.hs

   1 module Lambda where
   2
   3 import Data.Text as T
   4 import Data.Attoparsec.Text
   5 import Control.Applicative
   6
   7 type VarName = String
   8 data Term = Var VarName | Lambda VarName Term | App Term Term
   9
  10 instance Show Term where
  11   show (Var x) = x
  12   show (Lambda x t) = "\\" ++ x ++ "." ++ show t
  13   show (App t r) = "(" ++ show t ++ " " ++ show r ++ ")"
  14
  15 --instance Read Term where
  16 tRead :: String -> Term
  17 tRead s = case parseOnly (parseTerm <* endOfInput) (T.pack s) of
  18     (Right t) -> t
  19     (Left e) -> error e
  20
  21 parseVar :: Parser Term
  22 parseVar = do
  23   x <- many1 letter
  24   return $! Var x
  25
  26 parseLambda :: Parser Term
  27 parseLambda = do
  28   char '\\'
  29   (Var x) <- parseVar
  30   char '.'
  31   t <- parseTerm
  32   return $! Lambda x t
  33
  34 parseApp :: Parser Term
  35 parseApp = do
  36   char '('
  37   t <- parseTerm
  38   char ' '
  39   r <- parseTerm
  40   char ')'
  41   return $! App t r
  42
  43 parseTerm :: Parser Term
  44 parseTerm = parseVar <|> parseLambda <|> parseApp
  45
  46 -------------------------------------------------
  47
  48 isFreeIn :: VarName -> Term -> Bool
  49 isFreeIn x (Var v) = x == v
  50 isFreeIn x (App t u) = x `isFreeIn` t || x `isFreeIn` u
  51 isFreeIn x (Lambda v t) = x /= v && x `isFreeIn` t
  52
  53 rename :: Term -> Term
  54 rename (Lambda x t) = Lambda n (substitute x (Var n) t)
  55   where n = rnm x
  56         rnm v = if (v ++ "r") `isFreeIn` t then rnm (v ++ "r") else v ++ "r"
  57
  58 substitute :: VarName -> Term -> Term -> Term
  59 substitute a b (Var x) = if x == a then b else Var x
  60 substitute a b (Lambda x t)
  61   | x == a = Lambda x t
  62   | x `isFreeIn` b = substitute a b $ rename (Lambda x t)
  63   | otherwise = Lambda x (substitute a b t)
  64 substitute a b (App t u) = App (substitute a b t) (substitute a b u)
  65
  66 reduce :: Term -> Term
  67 reduce (Var x) = Var x
  68 reduce (Lambda x t) = Lambda x (reduce t)
  69 reduce (App t u) = app (reduce t) u
  70   where app (Lambda x v) w = reduce $ substitute x w v
  71         app a b = App a (reduce b)