人気ブログランキング |

ラムダ計算で遊ぶ 3


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

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

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

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)))) という2変数関数を返す。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)))))))

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

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

これは (3 f) が1変数関数で引数に関数 f を3回適用することを示している。したがって、((3 succ) 0) は0に succ 関数を3回適用することになるからこれは 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))

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

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

したがて、ペアを定義する関数 pair 、第1要素を取り出す関数 fst、第2要素を取り出す関数 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

0と真理値とが関連していたり、ペアとリストが同じものだったりとラムダ計算の振る舞いは面白い。これを利用してゼロを判別する関数 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))

0 を 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)

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

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

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

by tnomura9 | 2019-09-11 00:51 | Haskell | Comments(0)
<< ラムダ計算 関数の意味 ラムダ計算で遊ぶ 2 >>