Barendregt numeral
ラムダ計算体系で自然数をエンコードする方法としては、Church数が有名だけど、Barendregt numeralという方法もあるらしい。方法は、Church数の時と同様に、pair/false/0を
false = λxy.y
0 = λx.x
のように定義して、
n+1=
で再帰的に定義するらしい。Successor, Predecessor, Zero Testも定義できる
Barendregt numeralは定義としては、それほど不自然にも見えないけど、Church数のメリットとしては、どの数に対しても同じ型forall a.(a->a)->a->aが割り当て可能で、逆にこういう型を持つラムダ式は、Church数になるという点がある。Barendregt numeralは、例えばHaskellで型推論しても、それぞれ違う型になってしまう。それでも、Barendregt numeralに対するtotal recursive functionは全てラムダ式で書けるらしい。その証明は
http://www.amazon.com/Calculus-Semantics-Studies-Foundations-Mathematics/dp/0444875085
に書いてあるらしいけど、流石にその証明見るためだけに、本買う気はしない。
あと、total recursive functionが書けるなら、partial recursive functionも書ける気がするけど、そんなことないんだろうか。Church数の場合でもいいけど、Church数に対するpartial recursive functionでラムダ式で書けないものの有無って分かってるんだろうか
