偏λ-演算 偏λ-演算是λ-演算的扩展，允许处理 部分函数 （即某些输入可能无定义的函数）。它与可计算性理论紧密相关，通过引入 显式无定义元素 （⊥）来建模非终止计算或错误状态。 1. 基本动机 在标准λ-演算中，所有项均被视为"全函数"（对任何输入均有输出），但实际计算中可能存在： 无限循环（如 (λx.xx)(λx.xx) ）； 错误输入（如除零）。 偏λ-演算通过扩展语法和归约规则，使无定义行为可被形式化讨论。 2. 语法扩展 在标准λ项（变量、抽象、应用）基础上，增加： 常量 ⊥ （读作"bottom"），表示无定义值。 条件构造 （可选）：例如 if M then N else P ，用于处理部分函数的控制流。 示例： (λx. if x=0 then 1 else ⊥) 表示仅在输入为0时有定义。 3. 归约规则 保留β-归约（ (λx.M)N → M[N/x] ），但增加： ⊥-传播规则 ：若子项无定义，则整体无定义。例如： ⊥ M → ⊥ （应用左部无定义） M ⊥ → ⊥ （应用右部无定义） λx.⊥ → ⊥ （抽象体内无定义） 这体现了计算中的"严格性"（strictness）。 4. 语义模型：部分等价关系（PER） 为赋予偏λ-演算数学含义，常用 域理论 （Domain Theory）建模： 构造包含⊥的域（偏序集），其中⊥是最小元素，表示"信息量最少"。 函数被解释为 单调且连续 的映射，保证不动点存在（用于递归定义）。 例如，项 Y = λf.(λx.f(xx))(λx.f(xx)) 在偏λ-演算中可表示递归函数，但其自应用 xx 可能触发⊥。 5. 与可计算性理论的联系 偏λ-演算能精确刻画 部分递归函数 ： 每个部分递归函数可被一个λ项表示，且输入无定义时对应项归约为⊥。 这与图灵机的不停机行为等价，强化了丘奇-图灵论题。 6. 应用场景 程序语言语义 ：形式化处理运行时错误或非终止。 程序验证 ：通过⊥区分安全与非安全计算。 类型系统扩展 ：如 部分类型 （partial types）或 效应系统 （effect systems），标记可能发散的计算。 通过偏λ-演算，可更贴近实际计算环境地研究函数的定义域与行为。