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 rename :: Term -> Term
  49 rename (Lambda x t) = Lambda n (substitute x n t)
  50   where n = x ++ "r"
  51
  52 substitute :: VarName -> VarName -> Term -> Term
  53 substitute a b (Var x) = if x == a then Var b else Var x
  54 substitute a b (Lambda x t)
  55   | x == a = Lambda x t
  56   | x == b = substitute a b $ rename (Lambda x t)
  57   | otherwise = Lambda x (substitute a b t)
  58 substitute a b (App t u) = App (substitute a b t) (substitute a b u)