ラムダ計算
再帰とは自分自身を関数として使用することで、ラムダ計算では表面上は再帰操作は許されていないように見える。しかし少し工夫することによってラムダ計算でも再帰を実現できる。例として階乗を計算する関数 f(n) を考えてみよう。この関数は再帰的に以下のように定義できる。
f(n) := 1, if n = 0; and n × f(n − 1), if n > 0
ラムダ計算では自分自身を含む関数は定義できない。この問題を解決するためにまず、 f を引数にとり n を引数にとる関数を返すg という関数を考える。
g := λf n. (1, if n = 0; and n × f(n − 1), if n > 0)
関数 g は 1 か n × f(n − 1) を返すような関数を返す。上述の ISZERO や算術、論理記号の定義を用いれば、この関数 g はラムダ式で定義することができる。
しかし、これでは g 自身はまだ再帰的ではない。 g を用いて再帰的な階乗関数を作り出すためには、 g に対して引数 f として渡されている関数が、ある性質を持つ必要がある。
自然数をラムダ式で表現する方法はいくつか異なる手法が知られているが、その中でもっとも一般的なのはチャーチ数(英語版)(英: Church numerals)と呼ばれるもので、以下のように定義されている。
0 := λf x. x
1 := λf x. f x
2 := λf x. f (f x)
3 := λf x. f (f (f x))
以下同様である。直感的には、数 n はラムダ式では f という関数をもらってそれを n 回適用したものを返す関数である。つまり、チャーチ数は1引数関数を受け取り、1引数関数を返す高階関数である。(チャーチの提唱した元々のラムダ計算は、ラムダ式の引数が少なくとも一回は関数の本体に出現していなくてはならないことになっていた。そのため、その体系では上に挙げた 0 の定義は不可能である。)
上のチャーチ数の定義のもとで、後続(後者)を計算する関数、すなわち n を受け取って n + 1 を返す関数を定義することができる。それは以下のようになる。
SUCC := λn f x. f (n f x)
また、加算は以下のように定義できる。
PLUS := λm n f x. m f (n f x)