ラムダ定義可能

「ある関数$ 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 『計算モデルとプログラミング』.icon pp.142-143, 横内『プログラム意味論』.icon pp.24-27

上の補題の逆

ref 『計算モデルとプログラミング』.icon pp.142-143, 横内『プログラム意味論』.icon p.28

参考