ラムダ計算で自然数を定義する

$ c_n = \lambda{fx.f^nx}

ただし，ラムダ式MとNについて，以下のように定義する

こうすると，

$ C_0 = \lambda{fx.x}

$ C_1 = \lambda{fx.fx}

$ C_2 = \lambda{fx.ffx}

というようになる

足し算の定義

$ A_+ = \lambda xypq.xp(ypq)

以下が成り立つ

$ A_+c_nc_m = c_{m+n}

証明

$ A_+c_nc_m = \lambda{pq.c_np(c_mpq)}

$ = \lambda{pq.(\lambda{fx.f^nx})p((\lambda{fx.f^m})pq)}

$ = \lambda{pq.(\lambda{x.p^nx})(p^mq)}

$ = \lambda{pq.p^n(p^mq)}

$ = \lambda{pq.p^{n + m}q}

$ = \lambda fx.{f^{n+m}x}

$ = c_{n+m}

留意

この記事では厳密同値(形式的に同値)とベータ変換可能という意味での同値をごっちゃにしている