ラムダ計算において、前者は非常に難しい。整理した結果を共有する。JavaScript で動作するコード付き。
全体像の把握
インターネット上で容易にアクセスできる範囲でいうと、PRED の実装は 3 種類ある。それぞれの実装と、それを理解するのに一番わかりやすかったサイトをまとめる
- 実装A: すっきりした実装で、まるで魔法
PRED := λn f x. n (λg h. h (g f)) (λu. x) (λu. u)- Wikipedia に記載有
- 理解に有用なサイト: ラムダ計算のpredを理解する - clzの日記
- 実装B: 簡約を追えばなんとか・・・わかる
PRED := λn. n (λg k. (g 1) (λu. PLUS (g k) 1) k) (λv. 0) 0- Wikipedia に記載有
- 理解に有用なサイト: チャーチ数とpred関数 - うさぎ小屋
- 本稿でもう少し簡単な簡約が可能であることを示す：
PRED := λn. n (λg. (g 1) SUCC) (λv. 0) 0
- 実装C: 急がば回れ・凡人向け
-
PRED := λn. SECOND(n(NEXT)(PAIR(0)(0))) - 理解に有用なサイト: 東大の講義スライド
-
ひとこと:
- 簡約によって同値になる（はず）なので、実装は3つあっても構わない
- 遠回りであっても、実装Cが一番わかりやすい。実装Bも、上記の参考サイトをみながらであれば、式変形を追える。「なぜその式を思いついたのか？」もなんとかわかるような気がする
- どの実装も チャーチ数、後続、足し算が完全に理解できてからでないと絶対に理解できない。足し算の実装をみて、うんうんなるほど、といえるまでは手を出さない方が無難。
動作サンプル
JavaScript で動作する。実装A は PREDA, 実装B は PREDB, 実装C は PREDC という名前にしている。後続以外の実装については、私の昔の記事 「JavaScript でラムダ計算」に簡潔にまとめてあるので、併せてみてもらえると理解が進むと思う。
const TRUE = x => y => x;
const FALSE = x => y => y;
const ZERO = f => x => x;
const SUCC = n => f => x => f(n(f)(x));
const PAIR = x => y => f => f(x)(y);
const FIRST = p => p(TRUE);
const SECOND = p => p(FALSE);
const NEXT = p => PAIR(SUCC(FIRST(p)))(FIRST(p));
// PRED実装
const PREDA = n => f => x => n(g => h => h(g(f)))(u => x)(u => u);
const ONE = SUCC(ZERO);
const PREDB = n => n(g => k => g(ONE)(() => SUCC(g(k)))(k))(() => ZERO)(ZERO);
const PREDC = n => SECOND(n(NEXT)(PAIR(ZERO)(ZERO)));
// 動作確認
const one = SUCC(ZERO);
const two = SUCC(one);
const three = SUCC(two);
const four = SUCC(three);
const five = SUCC(four);
const numbers = [ZERO, one, two, three, four, five];
const display = f => f(n => n + 1)(0);
console.log(numbers.map(n => display(PREDA(n)))); // -> [ 0, 0, 1, 2, 3, 4 ]
console.log(numbers.map(n => display(PREDB(n)))); // -> [ 0, 0, 1, 2, 3, 4 ]
console.log(numbers.map(n => display(PREDC(n)))); // -> [ 0, 0, 1, 2, 3, 4 ]
実装B の納得のしかた
Wikipedia より
PRED := λn. n (λg k. (g 1) (λu. PLUS (g k) 1) k) (λv. 0) 0
部分式 (g 1) (λu. PLUS (g k) 1) k は、 g(1) がゼロとなるとき k に評価され、そうでないときは g(k) + 1 に評価されることに注意
少し変形して
F := λgk. (g 1) (λu. SUCC (g k)) k
PRED := λn. n F (λv. 0) 0
F の中身は、 (g 1) がゼロとなるとき k に評価され、そうでないときは SUCC (g k) に評価される
注意書きを確かめる。「(g 1) がゼロになるとき」は、ゼロの定義より（与えられた関数 λu. SUCC (g k) を一回も適用しないので）k に評価される。「(g 1) がゼロでない場合」は、定数関数を (g 1) 回適用するのだが、何回適用しようともただの定数関数なので、結局 SUCC(g k) に評価される。よって確かめられた。
しかし、この注意書きは真意を伝えきれていない。一番言いたいのは、F に g として以下の３つの関数を代入した時の挙動だ： a) (λn. 0) CZ と略記, b) λn. n ID と略記, c) λn. PLUS n 1 SUCC と略記:
- CZ を代入すると g 1 が 0 の場合なので、F CZ k = k
- ゆえに F CZ = ID
- ID を代入すると g 1 が 0 でないので、 F ID k = SUCC k
- ゆえに F ID = SUCC
- SUCC を代入すると g 1 が 0 でないので、F SUCC k = SUCC SUCC k
- ゆえに F SUCC = SUCC SUCC
これを図示するとこうなる:
CZ --(F適用)--> ID --(F適用)--> SUCC --(F適用)--> SUCC SUCC ...
よって CZ に F を n 回適用する関数 λn. n F CZ は SUCC を n-1 回 適用することと同値である。0 に SUCC を n-1 回適用するのが PRED であるから結局、
PRED := λn. n F CZ 0
となり導かれた。
実装 B の再発明
以上の事を逆から考えてみよう。
僕らは n という「n 回適用するツール」が手元にある。これをつかって「n-1 回適用するツール」である 数 n-1 を何とか作りたい。そのためには、「n回適用するけど そのうちの 1回は適用を免除される機構」があればよさそうだ。つまり、最初の 1 回目の適用では何もしない = ID であり、それ以降の 適用では SUCC になるような、擬似SUCC とでもいうべき関数を構成できれば、PRED の実装として望ましそうだ
PRED候補 := λn. n 擬SUCC 0
ただ、これは 擬SUCC の挙動は状態を持つので、うまく行かなさそうだ。そこで、クロージャっぽくこうする
PRED := λn. n F A 0
n F A でひとまとまりで、擬SUCC を n回適用する関数を作ろうという方針だ。 A はフラグのようなもので 1 回目の適用のみ ID に化けさせるために使う。こうすると、n F A は FFFFF.....FA となり、これが SSSSS....S ID となるというながれ。
よって探すべきは以下の性質をもつ A, F の組みあわせだ
F A = ID
F ID = SUCC
F SUCC = SUCC SUCC
ID, SUCC ともに number->number な関数であることに注意しよう。であれば、A も同じ型にしよう。また、F は入力に応じて「SUCC を 0,1,2 回適用する関数」を返す。 ID に 1 を割り振り、SUCC に 2 を割り振り、A に 0 を割り当てるような関数はなんだろうか？という考え方をすると ID 1 = 1, SUCC 1 = 2, A 1 = 0 というような「1 に適用する」という発想が出てくるはずだ。ということで、F, A の実装を見つけた。 A := λn. 0 F := λg. (g 1) SUCCだ。
以上より、PRED を以下のようにできるはずだ。
PRED := λn. n (λg. (g 1) SUCC) (λu. 0) 0
コードで確かめる。
const ZERO = f => x => x;
const SUCC = n => f => x => f(n(f)(x));
const PRED = n => n(g => g(SUCC(ZERO))(SUCC))(() => ZERO)(ZERO);
// [0, 1, ...9] --> [0, 0, 1, 2, ..., 8]
const numbers = [ZERO];
[...Array(9).keys()].forEach(() => numbers.push(SUCC(numbers[numbers.length - 1])));
const display = f => f(n => n + 1)(0);
console.log(numbers.map(n => display(PRED(n)))); // -> [0, 0, 1, 2, ..., 8]
実装A の納得の仕方
実装A は以下: PRED := λnfx. n (λgh. h (g f)) (λu. x) ID 日本語に読み直すと、 「n 回 const x に λgh. h (g f) を適用する関数 を ID に適用すると pred になる」と読めるので、実装B と基本的に構造が同じであることがわかる。
つまり、λu. x に λgh. h (g f) を何回か適用すると最初の 1回だけ適用が免除されて、残りの n-1 回は通常の適用、即ち f を適用するのと同じようにふるまうはずだ、と考えられる。
そこで、やってみる。
- 1回目の適用
(λgh. h (g f)) (λu. x) = λh. h x
- 2回目の適用
(λgh. h (g f)) (λh. h x) = λh. h (f x)
- 3回目の適用
(λgh. h (g f)) (λh. h (f x)) = λh. h (f (f x))
よって予想通り、λu. x に (λgh. h (g f)) を適用していく過程は:
λu. x --> λh. h x --> λh. h (f x) --> λh. h (f (f x)) -->
よって、 PRED = λnfx. (λh. h (f (f f(...(f x)) ID = λnfx. f(f(f(...f(x))))) となり、PRED の定義である「x に f を n-1 回適用する関数」が得られた。