チャーチ数
from Church encoding
Church numerals
関数呼び出しの回数によって数を表現
数nは何かをn回する関数
β正規形である
型注釈はSystem Fによるもの
自然数
0 = λsz.z チャーチブール値の
fls と同じ 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 とかを簡約してみよう
前者関数pred
一つのチャーチ数を引数に取る
引数が
0 のときは、 0 を、 n のときは n-1 を返すexamplezz = pair 0 0;
ss = λp. pair (snd p) (plus 1 (snd p));
pred = λm. fst (m ss zz);ゼロの判定
isZero = λ.x(tru fls)tru 簡約の例
字汚えな
加算
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 冪乗
examplepower = λn. λm. m (times n) c1;
power = λn. λm. m n;解決可能に関する補題
チャーチ数\overline{n}は、\overline{n}II\xrightarrow{\ast}_\beta Iが成り立つ
IはIコンビネータ
参考
算法表現論という本が詳しいらしい
TaPL5章