什么是 lambda 演算

\(\lambda\) 演算（Lambda Calculus）是一种形式体系，它仅通过函数定义（抽象化）与函数应用这两种极为简单的操作来表达计算。它虽然简单，却是图灵完备的，可以模型化任何计算，并构成了函数式编程语言的理论基础。

PS: 什么是形式系统?

形式系统是一个使用精确定义的符号、规则和公理来研究推理和计算的数学或逻辑框架。

它通常包括：

  1. 形式语言: 一套符号（字母表）和形成合式公式（句子）的规则（语法）。
  2. 公理: 一组被假定为真的初始公式。
  3. 推论规则: 从公理或其他已被证明的公式推导出新公式（定理）的规则。

形式系统旨在消除歧义，使推理过程完全形式化和机械化。

形式语言

Lambda Calculus 的形式语言（语法）非常简单，只包含三种基本构造：

  1. 变量 (Variable): 一个标识符，例如 x, y, z 。

    • 例子: x

  2. 抽象 (Abstraction): 定义一个匿名函数，形式为 λ<变量>. <项> 。读作 “lambda <变量> 点 <项>” 。

    • 例子: λx. x (这是一个接收参数 x 并返回 x 的函数，即恒等函数 identity function)。
    • 例子: λy. z (这是一个接收参数 y 但总是返回 z 的函数，即常数函数)。
    • js 例子: x => x+1

  3. 应用 (Application): 将一个函数应用于一个参数，形式为 (<项1> <项2>) 。 项1 通常是函数， 项2 是参数。括号有时可省略。

    • 例子: (λx. x) y (将恒等函数 λx. x 应用于参数 y)。根据计算规则，这会化简为 y
    • 例子: f x (如果 f 是函数， x 是参数，这是 (f x) 的简写)。
    • 例子: (λf. λx. f (f x)) (λy. y) (将一个“应用两次”的函数 λf. λx. f (f x) 应用于恒等函数 λy. y)。
    • js 例子: (x => x + 1)(4)

任何合法的 Lambda Calculus 表达式（称为 lambda 项）都是由这三种基本构造组合而成的。

推论规则

严格来说，Lambda演算与其说是一个公理系统，不如说是一个基于项重写规则的计算模型。其核心规则如下：

  1. α转换 (alpha-conversion) ：可以更改约束变量的名称（例：λx.x 与 λy.y 等价）。
  2. β归约 (beta-reduction) ：对函数应用进行求值（例：(λx.M) N 可重写为 M[x/N]，即将 M 中的 x 替换为 N）。
  3. η转换 (eta-conversion) ：表示函数的外延性（例：如果 x 在 M 中不是自由出现，则 λx.(M x) 与 M 等价）。

这些规则构成了定义 Lambda 项（表达式）等价性的基础。

α转换 (Alpha Conversion)

  • 核心思想 ：重命名绑定变量。
  • 目的 ：避免变量名冲突，它声明了绑定变量的具体名称是不重要的。只要不引起歧义（比如新名称与自由变量冲突），可以随意更改 λ 抽象中绑定的变量名及其在函数体内的所有对应引用。
  • 例子 ： λx.x 和 λy.y 是 α-等价的。 λx.(λy. x y) 可以 α-转换为 λz.(λy. z y) 。
  • js 例子 ： x => x+1 和 y => y+1 完全等价

β归约 (Beta Reduction)

  • 核心思想 ：函数应用（执行计算）。
  • 目的 ：这是 Lambda 演算中最核心的计算规则。当一个 λ 抽象（函数）被应用到一个参数上时，将函数体中所有与 λ 绑定变量同名的*自由*变量替换为该参数。
  • 规则 ： (λx.M) N β-归约为 M[x/N] （表示 M 中所有 x 被 N 替换）。
  • 例子 ： (λx.x + 1) 5 β-归约为 5 + 1=。=(λx.λy. x) z β-归约为 λy. z 。需要注意避免变量捕获（Variable Capture），必要时先进行 α 转换。
  • js 例子 ： (x => x + x + 1)(5) -> 5 + 5 + 1 或者 (x => y => x + y) (5) -> y => 5 + y

η转换 (Eta Conversion)

  • 核心思想 ：函数外延性（Extensionality）或简化。
  • 目的 ：它关联了一个函数与其“接收一个参数并立即应用该参数”的版本。如果一个函数 f 和另一个函数 g 对于所有可能的输入 x 都有 f x = g x=，那么 =f 和 g 是 η-等价的。
  • 规则 (η-归约) ： λx.(M x) 可以 η-归约为 M=，前提是 =x 在 M 中*不是自由变量*。这是一种简化形式。 js: x => add(x) -> add
  • 规则 (η-展开) ： M 可以 η-展开为 λx.(M x)=，前提是 =x 在 M 中不是自由变量。 js: add -> x => add(x)
  • 例子 ： λx.(concat "hello" x) η-等价于 concat "hello" （假设 x 不在 concat "hello" 这个表达式或其定义中自由出现）。