型無しラムダ計算
勉強のために作ってみました。もうちょっとさっぱり書けるようになるといいんですが。
チャーチ数で"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)