型無しラムダ計算

勉強のために作ってみました。もうちょっとさっぱり書けるようになるといいんですが。
チャーチ数で"1+1"はこんな感じです。

 $ghci Main.hs
 * Main> runS "(\\mnsz.ms(nsz))(\\sz.sz)(\\sz.sz)"
 "\\sz.s(sz)"

α変換はありません。これから勉強します。

import Text.ParserCombinators.Parsec hiding (parse)

data Exp = Abst String [Exp]
         | Paren [Exp]
         | Lambda String
         deriving (Show)

runE = eval . run

runS = concatMap toString . runE

run line = case runParser parse "" [] line of
               Right r -> r
               Left  l -> error $ show l

parse = do
        e  <- (try abst) <|> (try paren) <|> lambda
        es <- (try parse) <|> return []
        return (e:es)

abst = do
        char '('
        char '\\'
        b  <- many1 letter
        char '.'
        es <- parse
        char ')'
        return $ Abst b es

paren = do
        char '('
        x <- parse
        char ')'
        return $ Paren x

lambda = do
        l  <- noneOf "()"
        return $ Lambda [l]

eval :: [Exp] -> [Exp]
eval [] = []
eval [Paren x]  = [Paren (eval x)]
eval [Lambda x] = [Lambda x]
eval [Abst x y] = [Abst x (eval y)]
eval (Paren  x:y:xs) = eval $ (eval x) ++ (y:xs)
eval (Lambda x:Lambda y:xs) = eval (Lambda (x ++ y):xs)
eval (Lambda x:Abst y z:xs) = (Lambda x):(Abst y (eval z)):eval xs
eval (Lambda x:y:xs) = Lambda x:eval (y:xs)
eval (x@(Abst _ _):y:xs) = eval ((b_reduce x y) ++ xs)

b_reduce (Abst [] xs) y = xs ++ [y]
b_reduce (Abst [b] xs) y = b_reduce' b xs y
b_reduce (Abst (b:bs) xs) y = [Abst bs (b_reduce' b xs y)]

b_reduce' b [] y = []
b_reduce' b (x@(Lambda l):xs) y = let z = if [b] == l then y else x in z:(b_reduce' b xs y)
b_reduce' b (x@(Paren zs):xs) y = (Paren (b_reduce' b zs y)):(b_reduce' b xs y)
b_reduce' b (x@(Abst bs zs):xs) y = (Abst bs (b_reduce' b zs y)):(b_reduce' b xs y)

toString (Lambda x)   = x
toString (Paren xs)   = "(" ++ (concatMap toString xs) ++ ")"
toString (Abst [] xs) = concatMap toString xs
toString (Abst bs xs) = "\\" ++ bs ++ "." ++ (concatMap toString xs)