人気ブログランキング |

ラムダ計算 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))))))

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

by tnomura9 | 2019-09-14 17:24 | Haskell | Comments(0)
<< ラムダ計算 再帰 ラムダ計算 pred >>