λ演算
字数 1990 2025-10-25 15:47:51

λ演算

λ演算是数理逻辑和计算机科学中的一个形式系统，用于描述函数定义、函数应用和递归。它是计算理论的基础，为研究计算过程提供了一个简洁而强大的数学模型。下面，我将从基本概念开始，逐步深入讲解λ演算的核心内容。

第一步：基本组成元素

λ演算只包含三种表达式：

  1. 变量（Variables）：例如 x, y, z。它们是表达式的基本符号。
  2. 抽象（Abstraction）：用于定义函数。格式为 λx. M。它可以理解为“一个函数，其参数是 x，函数体是 M”。这里的 λx. 将变量 x 绑定（或“捕获”）在表达式 M 中。例如，λx. x 表示一个“恒等函数”，即输入什么就输出什么。
  3. 应用（Application）：表示将一个函数应用于一个参数。格式为 (M N)。它表示将函数 M 应用于参数 N。例如，( (λx. x) y ) 表示将恒等函数应用于变量 y。

第二步：括号约定与自由/绑定变量

为了简化书写，我们有一些括号约定：

  • 函数应用是左结合的的：M N P 等价于 ((M N) P)。
  • λx. M N 等价于 λx. (M N)，而不是 (λx. M) N。函数体一直延伸到其右侧尽可能远的位置。

理解变量的作用域至关重要：

  • 在 λx. M 中，x 是一个绑定变量。
  • 一个在表达式中出现，但未被任何 λ 绑定的变量，称为自由变量。
  • 例如，在表达式 (λx. x y) (λz. z) 中：
    • 第一个 x 被 λx 绑定。
    • 第二个 x 是自由变量（它不属于任何函数的参数）。
    • y 是自由变量。
    • 两个 z 都被 λz 绑定。

第三步：核心操作——β-归约

β-归约是λ演算的“计算”引擎。它定义了如何执行函数应用。
规则是：一个应用 (λx. M) N 可以归约为 M[x := N]。
这个符号 M[x := N] 的意思是“将表达式 M 中所有自由出现的变量 x 替换为表达式 N”。

让我们看一个例子：归约 (λx. x x) y

  1. 识别出这是一个应用：函数是 (λx. x x)，参数是 y。
  2. 根据β-归约规则，我们将函数体 x x 中的自由变量 x 替换为 y。
  3. 替换后得到 y y。
    所以，(λx. x x) y → y y。这个箭头 → 表示一次β-归约。

第四步：归约策略与Church-Rosser定理

当一个表达式中有多个地方可以进行β-归约时，就产生了归约策略的问题。主要有两种：

  1. 正则序归约：总是优先归约最外、最左边的可归约式。
  2. 应用序归约：总是优先归约最内、最左边的可归约式。

一个关键定理——Church-Rosser定理（或合流定理）指出：如果一个λ表达式可以通过不同的归约路径得到多个结果，那么这些结果最终必定可以再归约到同一个结果。这意味着归约的最终结果（如果存在）是唯一的，与所选的归约路径无关。这保证了计算的确定性。

第五步：编码数据与运算

λ演算看似只有函数，但它足够强大，可以表示所有可计算的数据和操作。这是通过编码实现的。

  • Church布尔值：

    • TRUE := λx. λy. x （选择第一个参数）
    • FALSE := λx. λy. y （选择第二个参数）
    • 逻辑运算如 AND 可以定义为：AND := λp. λq. p q FALSE。你可以验证 AND TRUE FALSE 会归约为 FALSE。

  • Church数：用函数表示自然数。

    • 0 := λf. λx. x （应用 f 零次于 x）
    • 1 := λf. λx. f x （应用 f 一次于 x）
    • 2 := λf. λx. f (f x) （应用 f 两次于 x）
    • 后继函数 SUCC := λn. λf. λx. f (n f x)。例如，SUCC 1 会归约为 2。

第六步：递归与不动点组合子

如何在λ演算中定义递归函数（即调用自身的函数）？由于函数没有名字，我们无法直接通过名字调用自身。解决方案是使用不动点组合子。最著名的是 Y组合子：
Y := λf. (λx. f (x x)) (λx. f (x x))

Y组合子的关键特性是：对于任何函数 F，都有 Y F = F (Y F)。这意味着 Y F 是函数 F 的一个不动点。通过精巧地设计 F，我们可以让 Y F 表示我们想要的递归函数。例如，可以用它来定义阶乘函数。

λ演算虽然是上世纪30年代的发明，但它奠定了函数式编程语言（如Lisp， Haskell）的理论基础，并且是研究程序语义和计算复杂性的核心工具。

λ演算 λ演算是数理逻辑和计算机科学中的一个形式系统，用于描述函数定义、函数应用和递归。它是计算理论的基础，为研究计算过程提供了一个简洁而强大的数学模型。下面，我将从基本概念开始，逐步深入讲解λ演算的核心内容。 第一步：基本组成元素 λ演算只包含三种表达式： 变量（Variables） ：例如 x, y, z。它们是表达式的基本符号。 抽象（Abstraction） ：用于定义函数。格式为 λx. M 。它可以理解为“一个函数，其参数是 x ，函数体是 M ”。这里的 λx. 将变量 x 绑定（或“捕获”）在表达式 M 中。例如， λx. x 表示一个“恒等函数”，即输入什么就输出什么。 应用（Application） ：表示将一个函数应用于一个参数。格式为 (M N) 。它表示将函数 M 应用于参数 N 。例如， ( (λx. x) y ) 表示将恒等函数应用于变量 y 。 第二步：括号约定与自由/绑定变量 为了简化书写，我们有一些括号约定： 函数应用是左结合的的： M N P 等价于 ((M N) P) 。 λx. M N 等价于 λx. (M N) ，而不是 (λx. M) N 。函数体一直延伸到其右侧尽可能远的位置。 理解变量的作用域至关重要： 在 λx. M 中， x 是一个 绑定变量 。 一个在表达式中出现，但未被任何 λ 绑定的变量，称为 自由变量 。 例如，在表达式 (λx. x y) (λz. z) 中： 第一个 x 被 λx 绑定。 第二个 x 是自由变量（它不属于任何函数的参数）。 y 是自由变量。 两个 z 都被 λz 绑定。 第三步：核心操作——β-归约 β-归约是λ演算的“计算”引擎。它定义了如何执行函数应用。 规则是：一个应用 (λx. M) N 可以归约为 M[x := N] 。 这个符号 M[x := N] 的意思是“将表达式 M 中所有 自由出现 的变量 x 替换为表达式 N ”。 让我们看一个例子：归约 (λx. x x) y 识别出这是一个应用：函数是 (λx. x x) ，参数是 y 。 根据β-归约规则，我们将函数体 x x 中的自由变量 x 替换为 y 。 替换后得到 y y 。 所以， (λx. x x) y → y y 。这个箭头 → 表示一次β-归约。 第四步：归约策略与Church-Rosser定理 当一个表达式中有多个地方可以进行β-归约时，就产生了归约策略的问题。主要有两种： 正则序归约 ：总是优先归约最外、最左边的可归约式。 应用序归约 ：总是优先归约最内、最左边的可归约式。 一个关键定理—— Church-Rosser定理 （或合流定理）指出：如果一个λ表达式可以通过不同的归约路径得到多个结果，那么这些结果最终必定可以再归约到同一个结果。这意味着归约的最终结果（如果存在）是唯一的，与所选的归约路径无关。这保证了计算的确定性。 第五步：编码数据与运算 λ演算看似只有函数，但它足够强大，可以表示所有可计算的数据和操作。这是通过编码实现的。 Church布尔值 ： TRUE := λx. λy. x （选择第一个参数） FALSE := λx. λy. y （选择第二个参数） 逻辑运算如 AND 可以定义为： AND := λp. λq. p q FALSE 。你可以验证 AND TRUE FALSE 会归约为 FALSE 。 Church数 ：用函数表示自然数。 0 := λf. λx. x （应用 f 零次于 x ） 1 := λf. λx. f x （应用 f 一次于 x ） 2 := λf. λx. f (f x) （应用 f 两次于 x ） 后继函数 SUCC := λn. λf. λx. f (n f x) 。例如， SUCC 1 会归约为 2 。 第六步：递归与不动点组合子 如何在λ演算中定义递归函数（即调用自身的函数）？由于函数没有名字，我们无法直接通过名字调用自身。解决方案是使用 不动点组合子 。最著名的是 Y组合子 ： Y := λf. (λx. f (x x)) (λx. f (x x)) Y组合子的关键特性是：对于任何函数 F ，都有 Y F = F (Y F) 。这意味着 Y F 是函数 F 的一个不动点。通过精巧地设计 F ，我们可以让 Y F 表示我们想要的递归函数。例如，可以用它来定义阶乘函数。 λ演算虽然是上世纪30年代的发明，但它奠定了函数式编程语言（如Lisp， Haskell）的理论基础，并且是研究程序语义和计算复杂性的核心工具。