λ計算で 1+2

その他

すっかり飽きる前にλ計算してみます。お題は 1+2 が 3 になるかどうか。
チャーチ数と足し算の定義はwikipediaのものを使います。

1 := λf x. f x
2 := λf x. f (f x)
3 := λf x. f (f (f x))

PLUS := λm n f x. m f (n f x)

PLUS 1 2 をβ変換(引数に変数を入れて計算すること)していった結果(正規形)が 3 になりますかどうか。
1 と 2 はα変換(変数名が重ならないように付け替えること)して、

1 := λg y. g y
2 := λh z. h (h z)

とします。式の意味は変わってません。
では、開始。

( λm n f x. m f (n f x) ) ( λg y. g y ) ( λh z. h (h z) )
→ ( λn f x. ( λg y. g y ) f (n f x) ) ( λh z. h (h z) )
→ ( λf x. ( λg y. g y ) f (( λh z. h (h z) ) f x) )
→ λf x. ( λy. f y ) (( λh z. h (h z) ) f x)
→ λf x. f (( λh z. h (h z) ) f x)
→ λf x. f (( λz. f (f z) ) x)
→ λf x. f ( f (f x) )

3 になった！ 1+2 ができただけなのに、とてもうれしいｗ
ついでに、間違いないよね？とドキドキしてます(^^;
1+2 ごときでｗ