チャーチ数の本質(nop と lambda の宣伝)

nop :
nop は no operation の略です。
マシン語などで何もしない命令を意味します。
この命令が重要であるのは逐次実行という
二項演算子の単位元であるからであります。
インドで 0 が発見されて以来、
我々は数多の単位元に感謝をささげてきました。
しかしながら nop は単位元として
正当に評価されていると本当にいえるのでしょうか。

lambda :
ご存知、ラムダ計算を象徴する文字で
ネクタイに縫い付けられたりします。
ラムダ計算は
f(x) = a*x+b
のような関数 f を
λx . a*x+b
のように書くことにしたものです。
面倒なので以下
\x -> a*x+b
としておきます。

普通の関数は domain が集合でないといけないのですが、
なんにも制限をしないことにします。
(\x -> x) (\x -> x)
のような気持ちの悪いことも許します。

α変換
\x -> a*x+b
から
\y -> a*y+b
に変換するのがα変換です。

β簡約
(\y -> y y) (\x -> x)
を
(\x -> x) (\x -> x)
に置き換えるのがβ簡約です。

重要な定理としては
チャーチ・ロッサー
「X をβ簡約しまくったものが二つ(A,B)あったとすると、
A と B をうまくβ簡約しまくると同じものに出来る」
決定不能
「A と B をβ簡約しまくって同じかどうかを判断する方法はない」

チャーチ数っていうのは
ラムダ計算上に自然数を構築する方法。
#> zero = lambda f : (lambda x : x) はとても理にかなってる。
#ということですけれども、ラムダ計算は相当複雑な構造がもてるので
#ここにも自然数構造が埋め込まれていた程度だと思っております。

こいつらには名前がついていることがあって、
ラフな理解では
I が恒等演算、K が定数関数作成関数、B が関数合成です。
ちょっと前に上がっていた Y がループっぽいのです。
他に R が再帰関数っぽいやつです。

ほかに重要なのは
チャーチ・チューリングのテーゼにもつながる
チューリングマシンと同程度の能力があること。

あとは、
型付ラムダ計算というのがあって、
ラムダ式のうちからお行儀のよいやつだけを選び出そうという企画で
もっとも単純な型のつけ方だと
正規化可能
「どんな型付ラムダ式もβ簡約しまくるとそれ以上できなくなる。
あと、その結果は一通り。」
ということが成立します。
なので Y の型付けは、普通つかないといったのはそういうことです、はい。

それから、プログラミング言語にあると便利。