tnomuraのブログ

Lemon

米須玄帥の「Lemon」はいろいろなカバーが YouTube で聞けて楽しい。

本人

米津玄師 MV「Lemon」

女子高生

【ガチ恋注意】米津玄師 Lemon 歌うま女子高生 文化祭最高レベルでうまい、、、

GIRLFRIEND

米津玄師さんの「Lemon」をGIRLFRIENDが歌ってみました！(カバー演奏)

Raon Lee

米津玄師 - Lemon ┃Cover by Raon Lee

MELOGAPPA

【男２人ハモリ】米津玄師「Lemon」(cover by MELOGAPPA) 歌詞付き

マトリョーシカ

ハチ MV「マトリョシカ」HACHI / MATORYOSHKA

ラムダ計算 再帰

ラムダ計算機でどうしてもやりたかったのが、Y コンビネータを使った再帰関数の記述だ。これを手入力で試すのは結構大変なので、次のような関数の定義ファイル defined.txt を作成して、ラムダ計算機 Ver 0.1 の :load コマンドで読み込んで検証することにする。defined.txt は次のようになる。

ファイル名： 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)))))))

これらの関数のうちで再帰関数に使うのが、

(= Y (lf.((lx.(f (x x))) (lx.(f (x x))))))

という Y コンビネータだ。この関数を β 簡約するともとの関数に戻ってしまうので β 簡約が永遠に終わらない。こんなもの何になるかと思うが Y の引数に関数 g を取ると次の用な関係が成り立つ。

(Y g) = g (Y g)

ここで g が関数 f と自然数 n を引数に取る場合、

g (Yg) n = g ( g (Y g) (n-1)) = g (g (g (Y g) (n-2)) = ... = g (g ( g ... (g (Y g) 0) ...)))

というような再帰関数を記述することができる。

実行例は次のようになる。

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

コンソールから Y だけを入力すると (f (f ... といつまでも f を出力し続ける。コントロール＋C で停止させないといけないがラムダ計算機自体も終了してしまう。

lambda> Y
(lf.(f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (

ラムダ計算機を再起動して (Y h) と入力すると今度は f が全て h に変わっている。(Y h) は束縛変数の f を h に置き換えるだけだから当たり前だが。(Y h) = h (h (h (h (Y h) .... と関数 h の再帰が延々と続いている。

$ runghc lambda.hs
lambda> :load
filename: defined.txt
lambda> (Y h)
(h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h (h

ところで、関数 g についてだが、これは関数 f と 自然数 n の２つを引数に取る。

g = (lf.(ln.(((isZero n) 1) ((mult n) (f (pred n)))))))

つまり、g は束縛変数の f に何かの関数を n に自然数 n を割り当てると、n が 0 のときには 1 を返し、それ以外の n のときは n * (f (n-1)) を返す。上の関数を読みやすく書き換えると次のようになる。

g f n = if n == 0 then 1 else n * (f (n-1))

何のことはない階乗の定義だ。これを Y コンビネータの引数にすると、

g (Y g) n

= g (g (g (g ( ... (g (Y g) 0)...))))

= g (g (g (g ( ... (1) ... ))))

= g (g (g (g ( ... (2 * 1) ... ))))

= g (g (g (g ( ... (3 * 2 * 1) ... ))))

= n * (n-1) * ... * 2 * 1

となって n の階乗が計算できる。Y の関数としての機能は関数 g に再帰を提供することだった。ただ、ラムダ計算の驚くべきところは、これらの計算が変数の置き換えだけで実現できているということだ。つまり関数適用 (f x) と言ってもラムダ式 f の中の束縛変数をラムダ式 x で置き換えるだけなのだ。そうして置き換えられたラムダ式は新しい文字列（ラムダ式）に変わるだけだ。

上のプログラムではいかにも自然数の階乗が計算できたように見えるが、その実、新しいラムダ式が生成されたに過ぎない。ラムダ計算機はこのラムダ式の置き換えという統語論的な操作を自動化しているだけなのだ。しかし、その文字列の操作に対しチャーチ数などの意味を与えることで、階乗の計算のような複雑なプログラムとして解釈することができる。

しかし、これはラムダ式に限ったことではなく、プログラム言語は全てがそうだ。プログラム言語といってもその実、最終的にビット列に翻訳され、そのビット列が別のビット列に自動変換されるだけなのだ。ラムダ計算はその文法が単純なゆえに、このようなコンピュータ・プログラムの実体を明らかにしてくれる。

Y コンビネータの詳しい仕組みについては、「ラムダ計算をちょっと勉強したので忘れないうちに書いておく」というサイトで説明されている。

この記事では、とにかくラムダ計算機 Ver 0.1 でも Y コンビネータとそれを使った再帰関数が記述できるということを検証してみた。

Text.Parsec の使い方から始まって、Parsec のソースコードの解読。Monad Transformers Step by Step の解読、ラムダ計算機のプログラムというように、プログラム言語の作り方を調べてきたが、これで一応区切りをつける。非常に簡単なプログラム言語だが、ラムダ計算機はプログラム言語のインタープリタとして働く。トイプログラムだが、夢だったプログラム言語のインタープリタの記述ができたので自己満足。しかし、ちょっと疲れてきたのでプログラムネタはしばらくお休みにする。

ラムダ計算 pred その2

pred の簡潔な定義について「ラムダ計算のpredを理解する」というページに説明されていた。その定義は次のようになる。

pred = λn. λs. λz. n (λx. λy. y (x s)) (λx. z) (λx. x)

複雑に見えるが、(λx.x) は恒等関数だし、(λx.z) は定数関数だ。また、整数 n は引数を n 回繰り返すという意味を持っている。そうするとポイントとなるラムダ式は (λx. λy. y (x s)) だということになる。これを n 回繰り返すのだから、これに仮に next という名前を付けてみることにする。

C:\Users\****>runghc lambda.hs
lambda> :load
filename: defined.hs
lambda> (= next (lx.(ly.(y (x s)))))

これを定数関数の (λx. z) に関数適用すると次のようになる。

lambda> (next (lx.z))
(ly.(y z))

これは、next の x を (lx.z) で置き換えたものだから次の式と同値だ。

lambda> (ly.(y ((lx.z) s)))
(ly.(y z))

(lx.z) は定数関数だから引数 x に何を与えてもその戻り値は z だ。

次に戻り値の (ly.(y z)) に next を関数適用してみる。

lambda> (next (ly.(y z)))
(ly.(y (s z)))

これは (ly.(y (x s))) の x を (ly.(y z)) に置き換えた次のラムダ式と同値だ。だから z の前に s が来ることが分かる。

lambda> (ly.(y ((ly.(y z)) s)))
(ly.(y (s z)))

この (ly.(y (s z))) は (ly.(y z)) の z が (s z) に置き換わっている。これにさらに next を関数適用する。

lambda> (next (ly.(y (s z))))
(ly.(y (s (s z))))

今度は、(ly.(y (s z))) の (s z) が (s (s z)) に置き換わっている。next を1回関数適用するたびに s が一つ先頭に増えていく。そこで next を 5 回 定数関数 lx.z に適用してみた。

lambda> (next (next (next (next (next (lx.z))))))
(ly.(y (s (s (s (s z))))))

z の頭に s が4個続いている。

(ly.(y が邪魔だから y に恒等関数を与えて y を消してみる。

lambda> ((next (next (next (next (next (lx.z)))))) (lx.x))
(s (s (s (s z))))

これに (ls.(lz. を付け加えたらチャーチ数の 4 だ。これは 5 のひとつ前の数だから (pred 5) = 4 だ。

lambda> 4
(ls.(lz.(s (s (s (s z))))))

したがってチャーチ数 n のひとつ前の数 pred を求めるラムダ式は次のようになる。

(ln.(ls.(lz.(((n next) (lx.z)) (lx.x)))))

lambda> (ln.(ls.(lz.(((n next) (lx.z)) (lx.x)))))
(ln.(ls.(lz.(((n (lx.(ly.(y (x s))))) (lx.z)) (lx.x)))))

このラムダ式を ped として定義すると、n から n-1 を求める pred 関数を作ることができる。

lambda> (= pred (ln.(ls.(lz.(((n next) (lx.z)) (lx.x))))))
lambda> (pred 2)
(ls.(lz.(s z)))
lambda> (pred 5)
(ls.(lz.(s (s (s (s z))))))

next 関数の定義をもう一度見てみよう。

next = (lx.(ly.(y (x s))))

これは、(ly.(y (s z)) という1変数関数を引数としてとり、(ly.(y (s z))) の y を s に置き換えた関数 (ly.(s (s z)))) を返す。引数と戻り値の関数は同じ型をしているので、next は次々に関数適用していける。おまけに、戻り値の s の数は引数に与えた n の数より一つだけ少ない。

(lx.(ly.(y (x s)))) を考えついた人は偉い。

(= pred (ln.(ls.(lz.(((n (lx.(ly.(y (x s))))) (lx.z)) (lx.x))))))

を設定ファイルに追加することにする。

ラムダ計算 pred

ラムダ計算で自然数 n の次の数 n+1 を計算する successor 関数は比較的簡単に書ける。

λwsz.s((ws)z)

がそれだ。変数 w に自然数 n を代入すると、

λsz.s((ns)z)

になる。λ式の body の部分の (ns) は引数に関数 s を n 回適用する関数になる。したがって、(ns)z は ss ... sz という引数 z に s を n 回関数適用したものになる。さらに、s((ns)z) はその上にもう一つ s を関数適用するので ss ... sz は z に s を n+1 回関数適用したものになる。したがって、

λs.z.ss ... sz (ただし s は n+1 個）

は自然数 n+1 になる。

これに比べて、n のひとつ前の数 n - 1 を計算するのは格段に難しい。アルゴリズムの概要は次のようになる。

まず、自然数のペア (n, m) に対し新しいペアを作る関数を次のように定義する。

nextPair (n, m) = (n+1, n)

これをペア (0,0) に関数適用すると次のようになる。

nexPair (0, 0) = (1, 0)

さらに、(1, 0) に nextPair を関数適用すると次のようになる。

nextPair (1,0) = (2, 1)

(2, 1) に nextPair を関数適用すると次のようになる。

nextPair (2, 1) = (3, 2)

このように nextPair を n 回関数適用するとき得られるペアは、

nextPair (n-1, n-2) = (n, n-1)

このペアの snd 部分を取り出すと n-1 と、自然数 n の前者 n-1 が得られる。これをラムダ計算でやればいいのだ。

これをラムダ計算プログラムで検証してみようというのが今回の記事の目的だ。この検証のためには「ラムダ計算機」に次の関数の定義をしておく必要がある。前回の「ラムダ計算機 Ver 0.1」はテキストファイルの定義を読み込んで定義できるのでそれを利用できる。

(= 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))))))
(= 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))
(= pair (lx.(ly.(lc.((c x) y)))))
(= fst (lp.(p true)))
(= snd (lp.(p false)))

「ラムダ計算機 Ver 0.1」での実行例は次のようになる。

C:\Users\****>runghc lambda.hs
lambda> :load
filename: defined.txt

lambda> (= zeroPair ((pair 0) 0))
lambda> (= nextPair (lp.((pair (succ (fst p))) (fst p))))
lambda> (= pred (ln.(snd ((n nextPair) zeroPair))))
lambda> (pred 3)
(ls.(lz.(s (s z))))

lambda> pred
(ln.(((n (lp.(lc.((c (ls.(lz.(s (((p (lx.(ly.x))) s) z))))) (p (lx.(ly.x))))))) (lc.((c (ls.(lz.z))) (ls.(lz.z))))) (lx.(ly.y))))

ラムダ計算機でも関数の定義を積み上げていけば、意味の分かるプログラムが書ける。

ラムダ計算機 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　（ソースファイルの文頭のアンダースコアはスペースで置き換える。エディタでアンダースコア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

ラムダ計算 関数の意味

ラムダ式は全て関数だ。関数とは何らかの働きのことだ。働きは目に見えないのでその意味をすぐには理解できない。関数の意味はそれを何らかの対象に関数適用してみてはじめて分かる。例えば λx.x は恒等関数だが、その意味は、いろいろな対象にそれを関数適用してみないと分からない。λx.x を a という対象に関数適用してみると (λx.x)a = a だ。また、b という対象に関数適用すると (λx.x)b = b だ。

lambda> ((lx.x) a)
a
lambda> ((lx.x) b)
b

全ての対象について検証しなくても、２，３の対象について λx.x を関数適用すれば、恒等関数の意味が、どんな対象に関数適用してもその対象そのものを返す関数であり、その意味は「何もしない関数」であることが分かる。しかし、依然として「何もしない」という意味は目には見えない。いろいろな対象に関数適用したときの結果を頭のなかで再現してその意味が分かる。

しかし、ラムダ計算ではこの目に見えない「働き」をラムダ式という対象として扱うことができる。そのことが関数型プログラム言語のプログラムを簡潔で柔軟なものとしている。

関数の意味は目に見えないがゆえに、逆にその意味を知ることは関数型のプログラム言語を活用するための重要な鍵となる。ラムダ計算が何もできないプログラム言語であるにもかかわらず面白いのは、関数の意味という抽象的なものを端的に扱うことができるからだろう。

そこでラムダ計算に現れるいろいろな関数の意味を考えてみることにする。

λx.x の意味は恒等関数だったが、λx.y の意味はなんだろうか。それは定数関数だ。つまり、どんな対象にこれを関数適用しても値は常に y となる。

lambda> ((lx.y) a)
y
lambda> ((lx.y) b)
y

ラムダ計算では 0 を表すチャーチ数は λsz.z だが、この関数の意味は何だろうか。変数 s について見るとこれは恒等関数であって s にどのような値を与えても常に λz.z という恒等関数を返す。

lambda> ((ls.(lz.z)) a)
(lz.z)
lambda> ((ls.(lz.z)) b)
(lz.z)

さらに λz.z は恒等関数という関数なのでこれにも意味がある。つまり、どのような対象に関数適用しても値はその対象そのものになるということだ。したがって、λsz.z には、「どのような関数に適用しても、恒等関数というどのような対象に対しても何もしない関数を返す関数である」という複合的な意味があることが分かる。

それではチャーチ数の 1 についてはどうだろうか。λsz.sz はチャーチ数の１だが、これを関数 f に関数適用すると λz.fz となる。これは「対象に関数 f を関数適用する関数」を作り出すことを意味している。

lambda> ((ls.(lz.(s z))) f)
(lz.(f z))
lambda> ((lz.(f z)) a)
(f a)

チャーチ数の 2 についてはどうだろうか。λsz.s(sz) を関数 f に関数適用すると λz.(f (fz)) なので、これは対象z に関数 f を２回関数適用してできる関数を表している。したがって、これを対象 a に関数適用すると f (f a) という値が得られる。

lambda> ((ls.(lz.(s (s z)))) f)
(lz.(f (f z)))
lambda> ((lz.(f (f z))) a)
(f (f a))

それでは、自然数の次の自然数を求める後者関数 λwsz.s(wsz) にはどのような意味があるのだろうか。変数の w には自然数が与えられるので、これを2 に関数適用してみると (λwsz.s(wsz))2 = λsz.s (2sz) である。2 は引数の関数を２回関数適用する関数を作る関数なので λsz.s (λx.(s(sx))z) = λsz.s(s(sz)) である。この関数の意味は「関数 s を３回対象 z に関数適用する関数」である。これはチャーチ数の 3 にあたる。

lambda> ((lw.(ls.(lz.(s ((w s) z))))) (ls.(lz.(s (s z)))))
(ls.(lz.(s (s (s z)))))
lambda> ((ls.(lz.(s (s (s z))))) f)
(lz.(f (f (f z))))
lambda> ((lz.(f (f (f z)))) a)
(f (f (f a)))

このようにラムダ計算のラムダ式には意味がある。しかし、その意味は目に見えない「作用」なのでその関数の様々な用例を頭の中でシミュレーションしてみなければ分からない。この抽象性が関数言語プログラムの難しいところである。しかし、一旦関数の意味を理解してしまうと、その抽象性から様々な用例に再利用することができる。これが、関数型プログラム言語のソースコードが劇的に簡潔になる理由だ。

関数の目に見えない「作用」の意味をつかまえることで、関数言語を扱う楽しさは倍増する。

ラムダ計算で遊ぶ ３

ラムダ計算では様々なデータ型を定義できる。まずは identity function だ。ラムダ計算の定義から最初に作られる関数だ。id は引数をそのまま返す関数だ。

$ runghc Lambda.hs
lambda> (= id (lx.x))
lambda> (id a)
a
lambda> (id b)
b

論理値の true と false は次のような２変数の関数だ。true は２つの引数をとり最初の引数を返す。false は２つの引数をとり２番めの引数を返す。

lambda> (= true (lx.(ly.x)))
lambda> (= false (lx.(ly.y)))
lambda> ((true a) b)
a
lambda> ((false a) b)
b

このような true とfalse を利用すると。条件分岐の if ~ then ~ else を次のように定義できる。

lambda> (= if (lc.(lx.(ly.((c x) y)))))
lambda> (((if true) a) b)
a
lambda> (((if false) a) b)
b

identity function (lz.z) に変数をひとつ付け加えたものが 0 だ。これは false と同じ関数になる。

lambda> (= 0 (ls.(lz.z)))

この 0 から suc (successor) 関数を使って自然数を次々に定義していくことができる。succ 関数の定義は次のようになる。succ 関数の引数の w に a を与えると、(ls.(lz.(s ((a s) z)))) という２変数関数を返す。body の部分は (s ((a s) z)) となり(a s) を z に関数適用した値に s を関数適用した値になる。

lambda> (succ a)
(ls.(lz.(s ((a s) z))))

(a s) の a が 0 のときは (a s) = lz.z = id となる。

lambda> (0 s)
(lz.z)

したがって ((a s) z) = z であるから (s ((0 s) z)) = (s (id z)) = (s z) となるので、(succ 0) = (ls.(lz.(s z))) となりこれが整数の 1 になる。

lambda> (succ 0)
(ls.(lz.(s z)))
lambda> (= 1 (succ 0))

同様に 2, 3, 4, 5 を succ 関数を使って作っていくことができる。整数の数と s の数は一致している。

lambda> (= 2 (succ 1))
lambda> 2
(ls.(lz.(s (s z))))
lambda> (= 3 (succ 2))
lambda> 3
(ls.(lz.(s (s (s z)))))
lambda> (= 4 (succ 3))
lambda> 4
(ls.(lz.(s (s (s (s z))))))
lambda> (= 5 (succ 4))
lambda> 5
(ls.(lz.(s (s (s (s (s z)))))))

自然数の本体は２変数の関数だ。したがって、これを他の関数に関数適用できる。f という関数に 3 を関数適用すると次のようになる。

lambda> (3 f)
(lz.(f (f (f z))))

これは (3 f) が１変数関数で引数に関数 f を３回適用することを示している。したがって、((3 succ) 0) は０に succ 関数を３回適用することになるからこれは 3 を返す。

lambda> ((3 suc) 0)
(ls.(lz.(s (s (s z)))))

ラムダ計算ではすべての変数が関数であるので、このようなことが起きる。数が関数であるというの今までになかった発想だ。このことを利用すると整数の加算が succ 関数を使って ((3 succ) 2) と表せる。

lambda> ((3 succ) 2)
(ls.(lz.(s (s (s (s (s z)))))))

数を関数に適用すると、その数の回数分引数の関数の適用を繰り返すことに注目すると整数の掛け算も簡単に定義できる。(n succ) は succ 関数を n 回繰り返す関数になるが、(m (n succ)) は n 回 succ を繰り返すことを m 回繰り返すことを意味しているからだ。

lambda> ((2 (3 succ)) 0)
(ls.(lz.(s (s (s (s (s (s z))))))))

これを利用して、自然数の掛け算 mult を次のように定義できる。

lambda> (= mult (lx.(ly.((x (y succ)) 0))))
lambda> ((mult 2) 3)
(ls.(lz.(s (s (s (s (s (s z))))))))

また、真理値も関数なので引数を与えることができる。(false a) のように false に任意の引数を与えるとこれは id 関数になる。(true に引数を与えるとこれは定数関数になる。

lambda> (false a)
(ly.y)

lambda> (true a)
(ly.a)

ラムダ関数のタプルのうちペアについては次のようになる。

lambda> (lw.((w a) b))
(lw.((w a) b))

これは１変数の関数で、true に関数適用すると第１の要素を、false に関数適用するとペアの第２の要素を取り出せる。

lambda> ((lw.((w a) b)) true)
a
lambda> ((lw.((w a) b)) false)
b

したがて、ペアを定義する関数 pair 、第１要素を取り出す関数 fst、第２要素を取り出す関数 snd を次のように定義できる。

lambda> (= pair (lx.(ly.(lw.((w x) y)))))
lambda> (= fst (lx.(x true)))
lambda> (= snd (lx.(x false)))
lambda> (= p1 ((pair a) b))
lambda> (fst p1)
a
lambda> (snd p1)
b

pair を作る関数はリストを作る関数 cons としても使うことができる。

lambda> (= cons (lx.(ly.(lw.((w x) y)))))
lambda> (= car (lx.(x true)))
lambda> (= cdr (lx.(x false)))
lambda> (= list1 ((cons a) b))
lambda> (= list2 ((cons c) list1))
lambda> (car list1)
a
lambda> (cdr list1)
b
lambda> (car list2)
c
lambda> (cdr list2)
(lw.((w a) b))
lambda> (car (cdr list2))
a

０と真理値とが関連していたり、ペアとリストが同じものだったりとラムダ計算の振る舞いは面白い。これを利用してゼロを判別する関数 isZero は次のように定義できる。これには論理演算子 NOT が必要なので次のように定義する。この定義の body 部分は条件分岐そのものだ。

lambda> (= NOT (lx.((x false) true)))
lambda> (NOT true)
(lx.(ly.y))
lambda> (NOT false)
(lx.(ly.x))

引数にした数値がゼロかどうかを判別する関数を作るために、数値を false に関数適用してみる。

lambda> (0 false)
(lz.z)
lambda> (1 false)
(lz.(ly.y))
lambda> (2 false)
(lz.(ly.y))
lambda> (3 false)
(lz.(ly.y))

０ を false に適用したときは id だがその他の場合は全て false になっている。そこで id と false を NOT に関数適用してみると、(id NOT) = NOT、(false NOT) = id、になることがわかる。

lambda> (id NOT)
(lx.((x (lx.(ly.y))) (lx.(ly.x))))
lambda> (false NOT)
(ly.y)

そこで引数が０かどうかを判定する関数 isZero は (((n false) NOT) false) で定義できる。

lambda> (= isZero (lx.(((x false) NOT) false)))
lambda> (isZero 0)
(lx.(ly.x))
lambda> (isZero 1)
(lx.(ly.y))

真理値や数が関数だったり、ペアとリストが同じものだったりラムダ計算のプログラムには驚かされることが多いが、普通のプログラミングにも参考にできそうなことも多い。ラムダ計算はそれ自身で表現力豊かなプログラム言語だ。

ラムダ計算で遊ぶ ２

ラムダ計算機には、変数と、関数抽象と、関数適用しかない。したがって、そのままでは数の計算もできないので、まず、これらを使って数を作る必要がある。

まず数の大本である 0 を作ることにする。これは identity function (lz.z) を利用して作る。変数と関数抽象と関数適用だけで作れる関数は最初はこれだけしかない。identity function は何もしない関数で、引数 a を取るとそのまま a を返す。変数名を z にしたのはおそらく zero にかけてあるのだろう。

$ runghc Lambda.hs

lambda> ((lz.z) a)
a

自然数の 0 はこの関数に変数 s を加えてラムダ抽象した関数である。s もおそらく successor (後者) からの連想だろう。明らかにこれは２変数の関数である。ラムダ計算では自然数は２変数の関数になる。すなわち 0 = λsz.z である。

lambda> (= 0 (ls.(lz.z)))

さらに、数の 1, 2, 3 はこの 0 を元に作っていくすなわち 1 = λsz.s(z), 2 = λsz.s(s(z)), 3 = λsz.s(s(s(z))) である。

lambda> (= 1 (ls.(lz.(s z))))
lambda> (= 2 (ls.(lz.(s (s z)))))
lambda> (= 3 (ls.(lz.(s (s (s z))))))

これは単に取り決めでそうされているわけではない。数を引数にそれより１つ多い数を作る関数、successor function (= suc) があるのだ。すなわち、suc = λwsz.s(wsz) だ。いかにも s をくっつけていきそうな関数だ。これは、ラムダ計算機ではつぎのように定義できる。

lambda> (= suc (lw.(ls.(lz.(s ((w s) z))))))

この suc 関数を数の 0 に適用してみよう。

lambda> (suc 0)
(ls.(lz.(s z)))
lambda> 1
(ls.(lz.(s z)))

確かに (suc 0) = 1 となっている。今度は 1, 2, 3, に suc を適用してみる。

lambda> (suc 1)
(ls.(lz.(s (s z))))
lambda> (suc 2)
(ls.(lz.(s (s (s z)))))
lambda> (suc 3)
(ls.(lz.(s (s (s (s z))))))

次々に z に関数適用される s の数が増えているのが分かる。１の場合 s は 1 個、２の場合 s は２個と、数と s の数が対応している。(suc 3) は名前をつけていなかったのでこれを 4 にする。また、(suc 4) は 5 にする。これを続けていけばどんどん数を増やして行ける。

lambda> (= 4 (suc 3))
lambda> 4
(ls.(lz.(s (s (s (s z))))))
lambda> (= 5 (suc 4))
lambda> 5
(ls.(lz.(s (s (s (s (s z)))))))

ところで、どのようにして suc 関数はこのような動作ができるのだろうか。それを知るために β 縮約を手計算でやってみる。つまり、次のラムダ式を β 縮約することで 0 から 1 を作り出す過程を見てみる。

suc(λsz.z) = λwsz.s(wsz)(λsz.z)

先ず関数抽象された w について、body の (wsz) の w を (λsz.z) で置き換える。このとき関数抽象の w は消えて s とz の２変数関数になる。

= λsz.s((λsz.z)sz)

ここで、(λsz.z)sz の関数抽象された s について引数の s で置き換える。λsz.z の body には s は現れないから単にλs が消えることになり、これは (λz.z).z になる。

= λsz.s((λz.z)z)

最後に λz.z を z に適用して z になるので次の結果になる。めでたく 1 = λsz.s(z) になった。

= λsz.s(z)

ラムダ計算の β 縮約と言っても関数抽象で指定された変数を、引数の文字列で置き換えるだけだ。この suc 関数を使うと自然数の加算を定義できる。つぎの例は 2 + 3 を suc 関数で実現したものだ。

lambda> ((2 suc) 3)
(ls.(lz.(s (s (s (s (s z)))))))

2 を suc に関数適用しているので奇妙な感じがするが、元々 2 は関数なので問題ない。実際 2 を a に関数適用すると次のようになる。

lambda> (2 a)
(lz.(a (a z)))

これは (2 a) が a を z に２回適用した関数を返すことを意味している。したがって、(2 suc) は引数 z に suc を２回適用した関数を返す。

lambda> (2 suc)
(lz.(ls.(lz.(s (s ((z s) z))))))

ラムダ計算では自然数に機能が付与されているのだ。加算の仕組みがわかったので、これを add 関数と定義する。

lambda> (= add (lx.(ly.((x suc) y))))
lambda> ((add 1) 2)
(ls.(lz.(s (s (s z)))))

ラムダ計算は数が関数なので機能を持っている。これを利用して数がゼロかどうかを判別させることができる。

先ず、真理値 T と F、否定論理演算子 NOT を次の様に定義する。

lambda> (= T (lx.(ly.x)))
lambda> (= F (lx.(ly.y)))
lambda> (= NOT (lx.((x F) T)))

0 は関数なのでこれを F に関数適用すると次のようになる。

lambda> (0 F)
(lz.z)

また、０以外の数を F に関数適用すると次のようになる。

lambda> (1 F)
(lz.(ly.y))
lambda> (2 F)
(lz.(ly.y))
lambda> (3 F)
(lz.(ly.y))

なぜこのようになるかは手計算をすれば理解できるがやや面倒だ。ここでは、この結果だけを利用することにする。そこで、(0 F) と (1 F) を NOT 関数に適用してみる。

lambda> ((0 F) NOT)
(lx.((x (lx.(ly.y))) (lx.(ly.x)))) ....... = NOT
lambda> ((1 F) NOT)
(ly.y)

そこで更にこれらを F に関数適用する。

lambda> (((0 F) NOT) F)
(lx.(ly.x)) ...... = T
lambda> (((1 F) NOT) F)
(lx.(ly.y)) ...... = F

したがって、この関係を利用すれば、引数が０かどうかを判別する isZero 関数を定義できる。全ては関数だというプログラミングスタイルが面白い。

lambda> (= isZero (lx.(((x F) NOT) F)))
lambda> (isZero 0)
(lx.(ly.x)) ..... = T
lambda> (isZero 3)
(lx.(ly.y)) ..... = F

変数と関数抽象と関数適用しかないプログラム言語のラムダ計算に自然数と加算が定義できた。また、引数が 0 かどうかを判別する isZero 関数もできてしまった。取っ付きにくかったラムダ計算が意外に面白い。β 縮約を自動でやってくれるラムダ計算機のおかげだ。

ラムダ計算で遊ぶ

ラムダ計算のインタープリタを作ったが、作りっぱなしでは面白くないので、A Tutorial Introduction to the Lambda Calculus をネタにラムダ計算によるプログラムをいろいろ試してみることにする。読解形式にはしないで、気ままにラムダ計算のプログラムを引用してラムダ計算機で実験していく。

ラムダ計算は「世界で最小の汎用プログラム言語」と呼ばれているようだが、すぐに思いつくのは次のような identity function くらいしかない。これは、単に引数を一つ取り、それを戻り値として返すだけだから何の面白みもない。

$ runghc Lambda.hs
lambda> (lx.x)
(lx.x)
lambda> ((lx.x) a)
a

ラムダ計算機ではこのように β 縮約を自動でできるが、ラムダ式の入力は括弧を省略しない形式でないとできない。したがって、参考書に出てくる括弧を省略した、λxy.MNL は (lx.(ly.((M N) L) というように括弧を補充する必要がある。

ラムダ計算では論理の真理値を定義できる。論理値の true と false は次のように定義される。

true = λxy.x

false = λxy.y

ラムダ計算機では (= var term) 式で変数 var にラムダ式 term を束縛できる。変数名は alphaNum なので数字と英数字の文字列になる。数字だけの変数にすることもできる。

lambda> (= true (lx.(ly.x)))
lambda> (= false (lx.(ly.y)))
lambda> true
(lx.(ly.x))
lambda> false
(lx.(ly.y))

true は引数 x y をとり、第１引数 x を返す関数だ。false は引数 x y をとり y を返す。

lambda> ((true a) b)
a
lambda> ((false a) b)
b

なぜこれが true と false なのだろうと不思議に感じるが、true と false がこのように定義されていると、if c then a else b という if ~ then ~ else 式が次のように簡単に定義できる。

if = λcxy.cxy

lambda> (=if (lc.(lx.(ly.((c x) y)))))
lambda> (((if true) a) b)
a
lambda> (((if false) a) b)
b

これでラムダ計算機もめでたく、条件分岐を記述できるようになった。

論理値が導入できたので論理記号も定義したい。NOT は次のように定義できる。

NOT = λx.xFT

true と false の別名 T と F を作って上の NOT を実装してみる。

lambda> (= T true)
lambda> (= F false)
lambda> (= NOT (lx.((x F) T)))
lambda> (NOT true)
(lx.(ly.y)) ..... false
lambda> (NOT false)
(lx.(ly.x)) ..... true

AND と OR の定義は次のようになる。

AND = λxy.xyF

OR = λxy.xTy

lambda> (= AND (lx.(ly.((x y) F))))
lambda> ((AND true) false)
(lx.(ly.y))
lambda> ((AND true) true)
(lx.(ly.x))

lambda> (= OR (lx.(ly.((x T) y))))
lambda> ((OR true) false)
(lx.(ly.x))
lambda> ((OR false) false)
(lx.(ly.y))

含意の定義は次のようになる。

lambda> (= IMPLY (lx.(ly.((OR (NOT x)) y))))
lambda> ((IMPLY true) true)
(lx.(ly.x))
lambda> ((IMPLY true) false)
(lx.(ly.y))

ラムダ計算機もだんだんプログラム言語らしくなってきた。一見不可解な true と false の定義で条件分岐や論理演算が定義できるのが面白い。

ラムダ計算機を使っていると、はるか昔にマイコンに機械語のプログラムを打ち込んでLEDを点滅させて感動していたときのことが思い出される。ラムダ計算の理論的なことは置いておいても、ラムダ計算機をいじるのは楽しい。

Monad Transformers Step by Step 6

Monad Transformers Step by Step のステップ５はログ機能の追加だ。使用モナドは Identity, StateT, ErrorT, ReaderT, WriterT の５つになる。だいぶ混み合ってきた。WriterT モナドトランスフォーマーが追加する機能は tell だ。do 記法の中でこの関数を使ってログを書き出す。以下に、動作確認したソースプログラムを示す。（文頭のアンダースコアはスペースに置き換える。）

ファイル名：eval5.hs

module Transformers where
import Control.Monad.Identity
import Control.Monad.Except
import Control.Monad.Reader
import Control.Monad.State
import Control.Monad.Writer

import Data.Maybe
import qualified Data.Map as Map

type Name = String
data Exp = Lit Integer
________ | Var Name
________ | Plus Exp Exp
________ | Abs Name Exp
________ | App Exp Exp
________ deriving (Show)
data Value = IntVal Integer
__________ | FunVal Env Name Exp
__________ deriving (Show)

type Env = Map.Map Name Value

type Eval5 a = ReaderT Env (ExceptT String
__________________________ (WriterT [String] (StateT Integer Identity))) a

runEval5 :: Env -> Integer -> Eval5 a -> ((Either String a, [String]), Integer)
runEval5 env st ev =
__runIdentity (runStateT (runWriterT (runExceptT (runReaderT ev env))) st)

tick :: (Num s, MonadState s m) => m ()
tick = do st <- get
__________put (st + 1)

eval5__________________:: Exp -> Eval5 Value
eval5 (Lit i)______= do tick
________________________return $ IntVal i
eval5 (Var n)______= do tick
________________________tell [n]
________________________env <- ask
________________________case Map.lookup n env of
________________________ Nothing -> throwError ("unbound variable: " ++ n)
________________________ Just val -> return val
eval5 (Plus e1 e2) = do tick
________________________e1' <- eval5 e1
________________________e2' <- eval5 e2
________________________case (e1', e2') of
__________________________(IntVal i1, IntVal i2) ->
____________________________ return $ IntVal (i1 + i2)
___________________________ -> throwError "type error in addition"
eval5 (Abs n e)____= do tick
________________________env <- ask
________________________return $ FunVal env n e
eval5 (App e1 e2)__= do tick
________________________val1 <- eval5 e1
________________________val2 <- eval5 e2
________________________case val1 of
__________________________FunVal env' n body ->
____________________________local (const (Map.insert n val2 env'))
______________________________ (eval5 body)
___________________________ -> throwError "type error in application"

exampleExp = Lit 12 `Plus` (App (Abs "x" (Var "x")) (Lit 4 `Plus` Lit 2))

Monad Transformers Step by Step の最後のステップは、Eval モナドの IO モナド化だ。これが非常に簡単で、Identity モナドを IO モナドに変更するだけだ。この変更のおかげで IO モナドの関数 print などが liftIO $ print ... のように使うことができる。print デバッグも可能になる。eval6.hs の実行例は次のようになる。

*Transformers> runEval6 Map.empty 0 (eval6 exampleExp)
12
4
2
((Right (IntVal 18),["x"]),8)

IO モナド化した eval 関数のソースは次のようになる。これで Monad Transformers Step by Step のソースコードは全てだ。関数のモナド化とモナドトランスフォーマーの利用によって、ソースコードの中心部分の大部分を変更することなく、機能を追加していくことができるのがわかった。

ファイル名： eval6.hs

module Transformers where
import Control.Monad.Identity
import Control.Monad.Except
import Control.Monad.Reader
import Control.Monad.State
import Control.Monad.Writer

import Data.Maybe
import qualified Data.Map as Map

type Name = String
data Exp = Lit Integer
________ | Var Name
________ | Plus Exp Exp
________ | Abs Name Exp
________ | App Exp Exp
________ deriving (Show)
data Value = IntVal Integer
__________ | FunVal Env Name Exp
__________ deriving (Show)

type Env = Map.Map Name Value

type Eval6 a = ReaderT Env (ExceptT String
__________________________ (WriterT [String] (StateT Integer IO))) a

runEval6 :: Env -> Integer -> Eval6 a -> IO ((Either String a, [String]), Integer)
runEval6 env st ev =
__runStateT (runWriterT (runExceptT (runReaderT ev env))) st

tick :: (Num s, MonadState s m) => m ()
tick = do st <- get
__________put (st + 1)

eval6__________________:: Exp -> Eval6 Value
eval6 (Lit i)______= do tick
________________________liftIO $ print i
________________________return $ IntVal i
eval6 (Var n)______= do tick
________________________tell [n]
________________________env <- ask
________________________case Map.lookup n env of
________________________ Nothing -> throwError ("unbound variable: " ++ n)
________________________ Just val -> return val
eval6 (Plus e1 e2) = do tick
________________________e1' <- eval6 e1
________________________e2' <- eval6 e2
________________________case (e1', e2') of
__________________________(IntVal i1, IntVal i2) ->
____________________________ return $ IntVal (i1 + i2)
___________________________ -> throwError "type error in addition"
eval6 (Abs n e)____= do tick
________________________env <- ask
________________________return $ FunVal env n e
eval6 (App e1 e2)__= do tick
________________________val1 <- eval6 e1
________________________val2 <- eval6 e2
________________________case val1 of
__________________________FunVal env' n body ->
____________________________local (const (Map.insert n val2 env'))
______________________________ (eval6 body)
___________________________ -> throwError "type error in application"

exampleExp = Lit 12 `Plus` (App (Abs "x" (Var "x")) (Lit 4 `Plus` Lit 2))