ラムダ計算機

ラムダ計算の β - 縮約を自動で計算するプログラムを作った。ラムダ記号の代わりに英小文字の l を使う。変数は一文字でも文字列でもよい。ラムダ抽象と関数適用の括弧は省略できない。関数適用は変数間にスペースが必要だ。= 記号を使って、ラムダ式を変数に束縛できる。などの特徴がある。

GitHub https://github.com/tnomura9/lambda-calculus

実際の使い方は次のようになる。

$ runghc lambda.hs
lambda> a
a
lambda> (lx.x)
(lx.x)
lambda> ((lx.x) a)
a
lambda> ((lx.(x y)) a)
(a y)
lambda> (= true (lx.(ly.x)))
lambda> ((true a) b)
a
lambda> :quit

ラムダ計算機 Ver 0.1

ラムダ計算機 Ver 0.1 ではテキストファイルから関数の定義を読み込めるように改良した。この改良でコマンドが :load と :quit の２つになった。:load コマンドでテキストファイルの (= name term) 形式の項を読み込んで関数の定義を登録できる。あとの使い方は前のプログラムと一緒だ。使用例は次のようになる。

$ runghc lambda.hs
lambda> :load
filename: defined.txt
lambda> true
(lx.(ly.x))
lambda> false
(lx.(ly.y))
lambda> 1
(ls.(lz.(s z)))
lambda> (succ 1)
(ls.(lz.(s (s z))))
lambda> :quit

:load コマンドで取り込む定義ファイルは次のように記述する。

$ cat defined.txt
(= true (lx.(ly.x)))
(= false (lx.(ly.y)))
(= NOT (lx.((x false) true))))
(= 0 (ls.(lz.z)))
(= succ (lw.(ls.(lz.(s ((w s) z))))))
(= 1 (succ 0))
(= 2 (succ 1))
(= 3 (succ 2))
(= 4 (succ 3))
(= 5 (succ 4))

lambda.hs プログラムのソースは次のようになる。

ファイル名: lambda.hs

import Data.Maybe
import Data.IORef
import qualified Data.Map as Map
import Text.Parsec
import System.Console.Haskeline
import Control.Monad.Trans
import Control.Monad.Identity
import qualified Control.Exception as Exc

type Name = String
data Term = Var Name
          | Abs Name Term
          | App Term Term
          | Bind Name Term
          deriving (Show)

type Env = Map.Map String Val

data Val = Atom String
         | FunVal Env String Term
         | Default Val Val
         deriving (Show)

evalTerm :: Env -> Term -> Eval0 Val
evalTerm env (Var x) = case Map.lookup x env of
                     Just val -> return val
                     Nothing -> return (Atom x)
evalTerm env (Abs s t) = return $ FunVal env s t
evalTerm env (App t1 t2) = do
                     v1 <- evalTerm env t1
                     v2 <- evalTerm env t2
                     case v1 of
                       FunVal env' s body -> evalTerm (Map.insert
 s v2 env') body
                       _ -> return $ Default v1 v2

type Eval0 a = Identity a

runEval0 :: Eval0 a -> a
runEval0 ev = runIdentity ev

parseTerm :: String -> Either ParseError Term
parseTerm input = parse term "lambda" input
  where
    term = var <|> abstr <|> appl <|> bind
    var = try (do
       x <- many1 alphaNum <* spaces
       return (Var x))
    abstr = try (do
       string "(l"
       x <- many1 alphaNum <* string "."
       e1 <- term
       string ")" <* spaces
       return (Abs x e1))
    appl = try (do
       string "(" <* spaces
       e1 <- term
       e2 <- term
       string ")" <* spaces
       return (App e1 e2))
    bind = try (do
       string "(=" <* spaces
       x <- many1 alphaNum <* spaces
       e1 <- term
       string ")" <* spaces
       return (Bind x e1))

unparse :: Val -> String
unparse (Atom x) = x
unparse (FunVal e x t) = "(l" ++ x ++ "." ++ (unparse (runEval0 (evalTerm
 e t))) ++ ")"
unparse (Default v1 v2) = "(" ++ (unparse v1) ++ " " ++ (unparse v2) ++ ")"

loadFile :: IORef Env -> InputT IO ()
loadFile ioref = do
  fname <- getInputLine "filename: "
  case fname of
    Just fnm -> lift $ bindAll ioref fnm
    Nothing -> outputStrLn "error"

loadTerm :: String -> IO [Either ParseError Term]
loadTerm fname = map parseTerm <$> lines <$> readFile fname

bindOneTerm :: IORef Env -> Either ParseError Term -> IO ()
bindOneTerm ioref tm = do
  env <- readIORef ioref
  case tm of
    Right (Bind x e) -> do
      val <- return $ runEval0 $ evalTerm env e
      writeIORef ioref (Map.insert x val env)
    Right exp -> do print exp; print "not written"
    Left err -> print err

bindAll :: IORef Env -> String -> IO ()
bindAll ioref fname = do
  Exc.catch ( do
    binds <- loadTerm fname
    mapM_ (bindOneTerm ioref) binds
    return ()
    ) $ \(SomeException e) -> print e

main :: IO ()
main = do
  global <- newIORef Map.empty
  runInputT defaultSettings (loop global)
    where
      loop :: (IORef (Map.Map Name Val)) -> InputT IO ()
      loop glb = do
        minput <- getInputLine "lambda> "
        case minput of
          Nothing -> return ()
          Just ":quit" -> return ()
          Just ":load" -> do loadFile glb; loop glb
          Just input -> do
            env <- lift $ readIORef glb
            expr <- return $ parseTerm input
            case expr of
              Right (Bind x e) -> do
                let val = runEval0 $ evalTerm env e
                lift $ writeIORef glb (Map.insert x val env)
              Right exp ->
                outputStrLn $ unparse $ runEval0 $ evalTerm env exp
              Left err ->
                outputStrLn $ show err
            loop glb

$ runghc lambda.hs
lambda> :load
filename: defined.txt
lambda> ((Y g) 3)
(ls.(lz.(s (s (s (s (s (s z))))))))

$ cat defined.txt
(= true (lx.(ly.x)))
(= false (lx.(ly.y)))
(= NOT (lx.((x false) true))))
(= AND (lx.(ly.((x y) false)))))
(= OR (lx.(ly.((x true) y)))))
(= IMPLY (lx.(ly.((OR (NOT x)) y))))
(= 0 (ls.(lz.z)))
(= succ (lw.(ls.(lz.(s ((w s) z))))))
(= pred (ln.(ls.(lz.(((n (lx.(ly.(y (x s))))) (lx.z)) (lx.x))))))
(= add (lx.(ly.((x succ) y))))
(= mult (lx.(ly.((x (y succ)) 0))))
(= 1 (succ 0))
(= 2 (succ 1))
(= 3 (succ 2))
(= 4 (succ 3))
(= 5 (succ 4))
(= 6 (succ 5))
(= 7 (succ 6))
(= 8 (succ 7))
(= 9 (succ 8))
(= isZero (lz.(((z false) NOT) false)))
(= pair (lx.(ly.(ls.((s x) y)))))
(= fst (lp.(p true)))
(= snd (lp.(p false)))
(= cons (la.(lb.(lf.((f a) b)))))
(= car (lx.(x true)))
(= cdr (lx.(x false)))
(= Y (lf.((lx.(f (x x))) (lx.(f (x x))))))
(= g (lf.(ln.(((isZero n) 1) ((mult n) (f (pred n)))))))
(= Z (lf.((lx.(f (ly.((x x) y)))) (lx.(f (ly.((x x) y)))))))
(= I (lx.x))
(= K (lx.(ly.x)))
(= S (lx.(ly.(lz.((x z) (y z))))))