人気ブログランキング |

ラムダ計算機 Ver 0.1


ラムダ計算機

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

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

$ 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 の2つになった。: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 (ソースファイルの文頭のアンダースコアはスペースで置き換える。エディタでアンダースコア2個をスペース2個に置換すると簡単。)

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
by tnomura9 | 2019-09-12 20:52 | Haskell | Comments(0)
<< ラムダ計算 pred ラムダ計算 関数の意味 >>