チャーチ数
Church numerals
関数呼び出しの回数によって数を表現
数$ nは何かを$ n回する関数
自然数
0 = λsz.z
0 = ΛX. λs:X->X. λz:X. z
0: CNat
1 = λsz.sz
1 = ΛX. λs:X->X. λz:X. s z
1: CNat
2 = λsz.s(sz)
...
bodyに出現するsの個数が、それが表す自然数に対応していることがわかる
型注釈
CNat = ∀X. (X->X)->X->X
負数
チャーチ数の別な使い方
以下でnumはチャーチ数
num f xで「関数fをxにnum回適用する」になる」
num succ 0 =_β 2
後者関数succ
succ = λnsz.s(nsz)
succ = λn:CNat. ΛX. λs:X->X. λz:X. s(n[X] s z)
succ: CNat -> CNat
実際に、succ 2とかを簡約してみよう
https://gyazo.com/bfdfc59d07c0fb80696a36c3d3b4c275
前者関数pred
一つのチャーチ数を引数に取る
引数が0のときは、0を、nのときはn-1を返す
code:example
zz = pair 0 0;
ss = λp. pair (snd p) (plus 1 (snd p));
pred = λm. fst (m ss zz);
ゼロの判定
isZero = λ.x(tru fls)tru
簡約の例
https://gyazo.com/63fe34b07a2d2144e8575c2749343c61
字汚えなmrsekut.icon
加算
add = λ m n. m succ n
add = λ m n s z. m s(n s z)
add = λm:CNat. λn:CNat. ΛX. λs:X->X. λz:X. m[X] s(n[X] s z)
add: CNat -> CNat -> CNat
Church数を2つ引数に取る
(n s z)
sをzにn回適用. これをAと置く
m s A
その結果Aにsをm回適用
乗算
Church数を2つ引数に取る
mul = λ x y z. x(y z)
mul: CNat -> CNat -> CNat
もしくはmul = λxy.x(add y)0
関数適用により、引数を1つ取り、$ yを足す関数になる
これを$ \mathrm{yplus}:=F_x\;yという関数名とすると
$ x \;\mathrm{yplus}\; \overline{0}
yplusをzeroにx回適用する。と読める
例
5plusを0に3回適用する→15
減算
sub = λn λm. m succ pred n
sub: CNat -> CNat -> CNat
2つの引数n、mを取り、n-mを求める
n-mが負数になる場合は解は0になる
等価
eq = λm λn.isZero (sub m n)
eq: CNat -> CNat -> CNat
冪乗
code:example
power = λn. λm. m (times n) c1;
power = λn. λm. m n;
チャーチ数$ \overline{n}は、$ \overline{n}II\xrightarrow{\ast}_\beta Iが成り立つ
つまり、自然数$ nを表すチャーチ数$ \overline{n}は解決可能 参考