λ可定义函数

在λ演算(参见拉姆达演算)中数字可表示的函数。在λ演算中引入组合算子：I=λx·x，K=λxy·x。则对任意λ项M，N，λ┝IM＝M，λ┝KMN=M。用［M，N］表示序偶，定义［M，N］=λx·xMN。于是可以在λ演算中定义一些表示自然数的项，称为数字。表示数n的项记作。归纳地定义如下：

定义(λ可定义函数) ①设f是n元函数。函数f是λ可定义的，当且仅当存在某个不含自由变元的λ项F使得

(*) f(k，…，k)=m 当且仅当 λ┝F…=。

如果(*)成立，则称f是由λ项F可定义的。

②设f是n元部分函数。函数f是λ可定义的，当且仅当对某个不含自由变元的项F，

f(k，…，k)=m 当且仅当

λ┝F…=，

并且

f(k，…，k)无定义 当且仅当 F…无范式。(关于λ项的范式，参见拉姆达演算。)

零函数Z(x)=0，后继函数S(x)=x+l，投影函数(x，…，x)=X，都是λ可定义的。定义它们的项分别是：Z＝λx·0(即λx·(λx·x))，S=λx·0［x，K］，=λx…x·x。

例如，对于Z，在λ演算中有

关于λ可定义函数有以下结果：

定理(克利尼) 设f为n元部分函数，则f是λ可定义的，当且仅当f是部分递归的。

定理(图灵) 一函数f是λ可定义的，当且仅当f是图灵可计算的。