ラムダ計算
自然数から自然数への関数 F: N → N が計算可能であるということは、全ての自然数の対 X, Y に対して F(X) = Y と f x == y が同値となるようなラムダ式 f が存在すること、と定義することができる。ここで、 x, y はそれぞれ X, Y に対応するチャーチ数によるラムダ式である。この定義は、計算可能性を定義する多くの方法のうちのひとつである。より詳しくは、チャーチ-チューリングの提唱の項を見よ。
xx)(\lambda x.xx)} である。自己適用 e ⌜ e ⌝ {\displaystyle e\ulcorner e\urcorner } を計算すると次のようになる。
e ⌜ e ⌝ {\displaystyle e\ulcorner e\urcorner }
if X ( A ⌜ e ⌝ ( N ⌜ e ⌝ ) ) then Ω else λ y . y {\displaystyle {\text{ if }}X(A\ulcorner e\urcorner (N\ulcorner e\urcorner )){\text{ then }}\Omega {\text{ else }}\lambda y.y}
if X ( A ⌜ e ⌝ ⌜ ⌜ e ⌝ ⌝ ) then Ω else λ y . y {\displaystyle {\text{ if }}X(A\ulcorner e\urcorner \ulcorner \ulcorner e\urcorner \urcorner ){\text{ then }}\Omega {\text{ else }}\lambda y.y}
if X ⌜ e ⌜ e ⌝ ⌝ then Ω else λ y . y {\displaystyle {\text{ if }}X\ulcorner e\ulcorner e\urcorner \urcorner {\text{ then }}\Omega {\text{ else }}\lambda y.
(1, if n = 0; and n·((Y g)(n − 1)), if n > 0)) 5 1, if 5 = 0; and 5·(g(Y g)(5 − 1)), if 5 > 0 5·(g(Y g) 4) 5·(λn. (1, if n = 0; and n·((Y g)(n − 1)), if n > 0) 4) 5·(1, if 4 = 0; and 4·(g(Y g)(4 − 1)), if 4 > 0) 5·(4·(g(Y g) 3)) 5·(4·(λ n. (1, if n = 0; and n·((Y g)(n− 1)), if n > 0) 3)) 5·(4·(1, if 3 = 0; and 3·(g(Y g)(3 − 1)), if 3 > 0)) 5·(4·(3·(g(Y g) 2)))
...
アルゴリズムの構造が再帰的に評価されているのがわかるだろう。再帰的に定義される関数は全て他の適当な関数の不動点となっているため、 Y を用いることで全ての再帰的な関数をラムダ式で表現することができる。たとえば、自然数に対する除算、乗算や比較述語を再帰を用いてよりきれいに定義することができる。
TRUE や FALSE といった真理値は慣習的に以下のように定義されることが多い。これらはチャーチ真理値(英語版)(英: Church booleans)とよばれている。
TRUE := λx y. x
FALSE := λx y. y
(この FALSE は前述のチャーチ数のゼロと同じ定義であることに注意せよ)
これらの真理値に対して論理記号を定義することができる。たとえば、以下のようなものがある。
AND := λp q. p q FALSE
OR := λp q. p TRUE q
NOT := λp. p FALSE TRUE
IFTHENELSE := λp x y. p x y
これらの記号を使った計算の例を挙げる。
AND TRUE FALSE = (λp q. p q FALSE) TRUE FALSE → TRUE FALSE FALSE = (λx y. x) FALSE FALSE → FALSE
以上より、 AND TRUE FALSE が FALSE と等しいことがわかる。
「述語」とは、真理値を返す関数のことである。計算論において最も基本的な述語は ISZERO で、これは引数がチャーチ数の 0であった場合には TRUE を、そうでなければ FALSE を返す関数であり、以下のように定義できる。
ISZERO := λn. n (λx. FALSE) TRUE