Untyped Lambda Calculas
またまたHaskellで実装してみました。
変数名の衝突を避けるためにde Bruijn indiciesという方法を使ってます。
だいたい内側のラムダ抽象の引数から順に0,1,2...と番号をふる感じの方法です。
詳しいことは本で確認してもらえれば・・・。
{- Untyped Lambda Calculus -} data Term = LVar Int | LAbs Term | LApp Term Term deriving (Eq) newtype Context = Context [String] type Binding = String showTerm (LVar x) = show x showTerm (LAbs t) = "(lambda. " ++ (showTerm t) ++ ")" showTerm (LApp t1 t2) = "(" ++ (showTerm t1) ++ " " ++ (showTerm t2) ++ ")" instance Show Term where show t = showTerm t termShift :: Int -> Term -> Term termShift d t = walk 0 t where walk c td = case td of LVar x | x >= c -> LVar (x+d) | otherwise -> LVar x LAbs t1 -> LAbs (walk (c+1) t1) LApp t1 t2 -> LApp (walk c t1) (walk c t2) termSubst :: Int -> Term -> Term -> Term termSubst j s t = case t of LVar k | k == j -> s | otherwise -> LVar k LAbs t1 -> LAbs (termSubst (j+1) (termShift 1 s) t1) LApp t1 t2 -> LApp (termSubst j s t1) (termSubst j s t2) termSubstTop :: Term -> Term -> Term termSubstTop s t = termShift (-1) (termSubst 0 (termShift 1 s) t) isval :: Context -> Term -> Bool isval ctx t = case t of LAbs _ -> True _ -> False type ErrorMessage = String eval1 :: Context -> Term -> Either ErrorMessage Term eval1 ctx t = case t of LApp (LAbs t12) v2 | isval ctx v2 -> Right (termSubstTop v2 t12) LApp v1 t2 | (isval ctx v1) -> Right (LApp v1 t22) where Right t22 = eval1 ctx t2 LApp t1 t2 -> Right (LApp t11 t2) where Right t11 = eval1 ctx t1 _ -> Left "No Rule Applies" eval :: Context -> Term -> Term eval ctx t = case res of Left err -> t Right u -> eval ctx u where res = eval1 ctx t
使い方は
> let true = (LAbs (LAbs (LVar 1))) > let false = (LAbs (LAbs (LVar 0))) > let ifl = (LAbs (LAbs (LAbs (LApp (LApp (LVar 2) (LVar 1)) (LVar 0))))) > true (lambda. (lambda. 1)) > false (lambda. (lambda. 0)) > ifl (lambda. (lambda. (lambda. ((2 1) 0)))) > eval (Context []) (LApp (LApp (LApp ifl true) true) false) (lambda. (lambda. 1))
って感じです。
関数適用が左結合なのを実装に組み込めてないので、一つ一つ自分で書かないといけないのがちょっとうざいですね。
いよいよ次の章から型が登場するらしいです。わくわく
以下、本に乗ってた関数たち
-- Bools tru = (LAbs (LAbs (LVar 1))) fls = (LAbs (LAbs (LVar 0))) test = (LAbs (LAbs (LAbs (LApp (LApp (LVar 2) (LVar 1)) (LVar 0))))) andl = (LAbs (LAbs (LApp (LApp (LVar 1) (LVar 0)) fls))) orl = (LAbs (LAbs (LApp (LApp (LVar 1) tru) (LVar 0)))) notl = (LAbs (LApp (LApp (LVar 0) fls) tru)) -- Pair pairl = (LAbs (LAbs (LAbs (LApp (LApp (LVar 0) (LVar 2)) (LVar 1))))) fstl = (LAbs (LApp (LVar 0) tru)) sndl = (LAbs (LApp (LVar 0) fls)) -- Church Numerals c0 = (LAbs (LAbs (LVar 0))) scc = (LAbs (LAbs (LAbs (LApp (LVar 1) (LApp (LApp (LVar 2) (LVar 1)) (LVar 0)))))) plus = (LAbs (LAbs (LAbs (LAbs (LApp (LApp (LVar 3) (LVar 1)) (LApp (LApp (LVar 2) (LVar 1)) (LVar 0))))))) times = (LAbs (LAbs (LAbs (LApp (LApp (LVar 1) (LApp plus (LVar 0))) c0)))) iszro = (LAbs (LApp (LApp (LVar 0) (LAbs fls)) tru))