「ある関数f」を、「ラムダ抽象で計算可能である」ことを表す

ラムダ式ではない任意の関数fを、ラムダ式で表現できるかどうか、という話

fが全域関数なら、そのラムダ表現Fは常に正規形を持つ

定義

自然数上の関数f:\mathbb{N}^n\to\mathbb{N}について、ラムダ式Fが以下の2条件を満たすとき、fはラムダ定義可能という

f(x_1,x_2,\cdots,x_n)=kのとき、F\overline{x_1}\overline{x_2}\cdots\overline{x_n}\xrightarrow{\ast}_\beta \overline{k}

f(x_1,x_2,\cdots,x_n)が未定義のとき、F\overline{x_1}\overline{x_2}\cdots\overline{x_n}は解決不能である

このときFをfのラムダ表現という

補題

全ての帰納的関数はラムダ定義可能

ref pp.142-143, pp.24-27

全てのラムダ定義可能な関数は、帰納的関数

上の補題の逆

ref pp.142-143, p.28

参考

『計算モデルとプログラミング』 p.141

横内『プログラム意味論』 p.24-