はじめに
プログラミング言語 Lazy K とは何か、どのように書けるのか、実際に使うときに気をつけないといけないことまでを追っていきたいと思っています。
今回は、ラムダ計算で様々な処理を行う方法について理解を深めていきたいと思います。
第１回：コンビネータとラムダ計算
第２回：Lazy K の入出力とチャーチ数
第３回：ラムダ計算のいろいろ ← いまここ
第４回：(Lazy K プログラムを書いてみる)[https://qiita.com/amoyris/items/cc146c54f156a283cb6b]
論理値
ラムダ計算での論理値の扱いを見ていきます。
ラムダ計算で論理値は一般的に次のように扱います。
TRUE := λx. λy. x
FALSE := λx. λy. y
このように定義することで、前回のCARやCDRは次のように表せます。
CAR := λp. p TRUE
CDR := λp. p FALSE
論理値の演算は次のようになります。
AND := λp. λq. p q FALSE
OR := λp. λq. p TRUE q
NOT := λp. p FALSE TRUE
これらについては、実際にTRUEとFALSEを入れてみればわかるでしょう。
ということで、これで任意の論理演算ができるようになりました。
述語
論理値をみてきたので、いくつか論理値を返す関数を紹介します。
代表的なものは数値が $0$ かどうかを判定する関数ISZEROです。
これは次のように定義できます。
ISZERO := λn. n (λx. FALSE) TRUE
このように定義すると、 $n=0$ の時(n := λf. λx. x)TRUE、$n>0$ の時(n := λf. λx. f ... x)FALSEが返ります。
この関数を用いることで「$m$ が $n$ 以上か」を判定する関数GEを次のように定義できます。
GE := λm. λn. ISZERO (SUB n m)
$m\ge n$の場合、$n-m \le 0$ になるため、これが成立します。
これを使って $\le$ (LE)、 $\gt$ (GT)、 $\lt$ (LT)、を以下のように定義できます。
LE := λm. λn. GE n m
GT := λm. λn. NOT (GE n m)
LT := λm. λn. NOT (GE m n)
また、$=$ (EQ)は次のように定義できます。
EQ := λm. λn. AND (GE m n) (LE m n)
数値に関してはここまで定義できていれば良いでしょう。
次にリストに関してですが、前回はリストの末尾であるNILをFALSEとしておけば良いとしていましたが、FALSEや0と同じであると混乱するので、以下のように定義することとします。
NIL := λx. TRUE
このように定義すると、リストpがNILかどうかを判定する関数ISNILは次のように定義できます。
ISNIL := λp. p (λx. λy. FALSE)
pがNILなら
ISNIL NIL = (λp. p (λx. λy. FALSE)) (λx. TRUE)
→β (λx. TRUE) (λx. λy. FALSE)
→β TRUE
pがリストなら
ISNIL (λf. f x y) = (λp. p (λx. λy. FALSE)) (λf. f x y)
→β (λf. f x y) (λx. λy. FALSE)
→β (λx. λy. FALSE) x y
→β FALSE
となり、確かめられます。
他の定義のしかた
例えば次のように定義しても良いと思います。
NIL := λx. FALSE
ISNIL := λp. p (λx. λy. TRUE) FALSE TRUE
他にもいろいろな方法があると思うので考えてみてください。
分岐
論理演算がわかったところで分岐(IF)について考えます。
と言ってもやることは単純で、pを論理値、Tをp = TRUEの時の処理、Fをp = FALSEの時の処理とすると、IFは次のように書けます。
IF := λp. p T F
簡単ですね。
別にIFを使わなくてもp T Fとしても良いです。
ということで先のように論理値を定めると分岐を簡単に実装できることがわかりました。
再帰
次は再帰について考えます。
例えば、階乗を計算する関数f(n)を定義したいとします。
再帰を使って書くと以下のようになります（ラムダ計算ではないです）。
f(n) := 1 if n = 0; n * f(n - 1) if n > 0;
これをラムダ計算で実現したいです。
とりあえずこのようなfをパラメータとして受け取ってf(n)を返すような関数gについて考えると、
g := λf. λn. IF (ISZERO n) (1) (MULT n (f (PRED n)))
と表すことができます。
ここで、g(f)=fとなっています。
つまり、fはgの不動点です。
不動点コンビネータというものを導入します。
不動点コンビネータとは、任意の関数 $g$ に対し
$$g(h(g)) = h(g)$$
となるような関数 $h$ を指します。
ここでfをh(g)とすれば、これを満たすことができます。
不動点コンビネータとしてYコンビネータというものが存在します。
定義は以下のとおりです。
Y := λg. (λx. g (x x)) (λx. g (x x))
実際にY gを計算してみると、
Y g = (λg. (λx. g (x x)) (λx. g (x x))) g
→β (λx. g (x x)) (λx. g (x x))
→β g ((λx. g (x x)) (λx. g (x x)))
= g (Y g)
となり、Y g = g (Y g)となっていることがわかります。
よって、g f n = g (Y g) n = Y g nはf nと同じになります。
実際にY g 2を計算してみます。
Y g 2 = g (Y g) 2
= (λf. λn. IF (ISZERO n) (1) (MULT n (f (PRED n)))) (Y g) 2
= IF (ISZERO 2) (1) (MULT 2 ((Y g) (PRED 2)))
= IF FALSE (1) (MULT 2 ((Y g) (1)))
= MULT 2 ((Y g) (1))
= MULT 2 (g (Y g) (1))
= MULT 2 (IF (ISZERO 1) (1) (MULT 1 ((Y g) (PRED 1))))
= MULT 2 (IF FALSE (1) (MULT 1 ((Y g) (0))))
= MULT 2 (MULT 1 ((Y g) (0)))
= MULT 2 (MULT 1 (IF (ISZERO 0) (1) (MULT 0 ((Y g) (PRED 0)))))
= MULT 2 (MULT 1 (IF TRUE (1) (MULT 0 ((Y g) (0)))))
= MULT 2 (MULT 1 1)
確かにできています。
このようにYコンビネータを使用することで、再帰を実現することができます。
数値とリスト（再考）
ここまでみてきたことを踏まえて、前回の数値やリストについてもう一度考えてみましょう。
まずは、前回スキップした除算から見ていきましょう。
除算
$m \div n$ について考えてみましょう。
ただし、ここで考える除算とは整数範囲です（ラムダ計算では数値は非負整数なので）。
$d=m \div n$ とは、プログラム的に書くと以下のようにあります。
define div:
d = 0
while m >= n:
d += 1
m -= n
return d
$m \ge n$ である限り $d$ に $1$ を足していくというのが除算です。
これをラムダ計算式に直すと、以下のようになります。
DIV := λm. λn. Y (λf. λk. IF (GE k n) (SUCC (f (SUB k n))) (0)) m
同時にあまり(MOD)は以下のようになります。
MOD := λm. λn. Y (λf. λk. IF (GE k n) (f (SUB k n)) (k)) m
再帰を使用することが除算のポイントでした。
これで四則演算が全てできるようになりました。
数値の表現
数字はλf. λx. f ... xで表すことができますが、大きな数になるととても長くなります。
例えばLazy KにおけるEOFは $256$ ですが、fをいちいち $256$ 回書いていたらとんでもないことになります。
もっと短くかきたい、というときには加算、乗算、累乗を組み合わせると良いです。
特に、一般的に長さは累乗<乗算<加算になるのでなるべく累乗で対応できると短くなります。
以下は一例です。
4 := (λn. n n) 2
16 := (λn. n n n) 2
256 := (λn. n n) ((λn. n n) 2)
インデックスアクセス
ここからはリストについてみていきます。
まずはインデックスアクセスを考えましょう。
リスト$l$ の $n$ 番目のデータにアクセスする関数NTHは以下のようになります。
NTH := λl. λn. CAR (n CDR l)
$n$ 回CDRを取ったもののCARをとれば良いです。
反転
リストの反転です。
以下のようになります。
REVERSE := λl. Y (λf. λl. λr. IF (ISNIL l) r (f (CDR l) (CONS (CAR l) r))) l NIL
lは元のリスト、rは反転済みのリストです。
これら2つを引数にして関数を作るのがポイントでした。
結合
リストの結合です。
以下のようになります。
APPEND := λl. λr. Y (λf. λl. λr. IF (ISNIL l) r (CONS (CAR l) (f (CDR l))))
後ろのリストに一つずつ前のリストのデータをつけていくことで実現できます。
終わりに
今回は、ラムダ計算による処理についてみてきました。
次回はこれらを組み合わせて実際にLazy Kのコードを組み立てていきたいと思います。