utlc/lambda 教程

本教程使用无类型 lambda 演算进行计算：构建项、用 beta 和 eta 对其范式化、把布尔值和数编码为函数，并处理永不停止归约的项。

快速入门

moon add Luna-Flow/type_theory@0.2.0

import {
  "Luna-Flow/type_theory/core",
  "Luna-Flow/type_theory/syntax",
  "Luna-Flow/type_theory/rewrite",
  "Luna-Flow/type_theory/utlc/lambda",
}

test "quick start: (λx. x) 1" {
  let x = @core.Name::new("x")
  let id : @syntax.Term[Int] = @lambda.abstraction(x, Variable(x))
  let term = @lambda.application(id, Value(1))
  assert_eq(@lambda.normalize(term, 10), NormalForm(term=Value(1), steps=1))
}

日常任务

这些任务用几个辅助函数让项保持简短：

fn lv(s : String) -> @syntax.Term[Int] {
  @syntax.Term::Variable(@core.Name::new(s))
}

fn lam(s : String, body : @syntax.Term[Int]) -> @syntax.Term[Int] {
  @lambda.abstraction(@core.Name::new(s), body)
}

fn ap(f : @syntax.Term[Int], a : @syntax.Term[Int]) -> @syntax.Term[Int] {
  @lambda.application(f, a)
}

fn nf(t : @syntax.Term[Int]) -> @syntax.Term[Int] {
  match @lambda.normalize(t, 1000) {
    NormalForm(term~, ..) => term
    StepLimitReached(..) => abort("no normal form within 1000 steps")
  }
}

编码布尔值

Church 布尔值在两个参数之间做选择： $\mathsf{true} = \lambda t.\,\lambda f.\,t$ ， $\mathsf{false} = \lambda t.\,\lambda f.\,f$ ，且 $\mathsf{if}\;b\;x\;y = b\,x\,y$ 。

test "church booleans" {
  let tru = lam("t", lam("f", lv("t")))
  let fls = lam("t", lam("f", lv("f")))
  let not_ = lam("b", ap(ap(lv("b"), fls), tru))
  assert_true(@syntax.alpha_equal(nf(ap(not_, tru)), fls))
  assert_true(@syntax.alpha_equal(nf(ap(not_, fls)), tru))
}

编码数并相加

Church 数 $n$ 把函数应用 $n$ 次： $\overline{2} = \lambda f.\,\lambda x.\,f\,(f\,x)$ 。加法是 $\lambda m.\,\lambda n.\,\lambda f.\,\lambda x.\,m\,f\,(n\,f\,x)$ 。

fn numeral(n : Int) -> @syntax.Term[Int] {
  let mut body = lv("x")
  for _ in 0..<n {
    body = ap(lv("f"), body)
  }
  lam("f", lam("x", body))
}

test "2 + 2 = 4" {
  let plus = lam(
    "m",
    lam("n", lam("f", lam("x", ap(ap(lv("m"), lv("f")), ap(ap(lv("n"), lv("f")), lv("x")))))),
  )
  let four = nf(ap(ap(plus, numeral(2)), numeral(2)))
  assert_true(@syntax.alpha_equal(four, numeral(4)))
}

范式使用的绑定子名（f_1、…）可能与你预期的不同；alpha_equal 会忽略它们。

用 eta 简化包装

当 $x$ 不在 $g$ 中自由出现时， $\lambda x.\,g\,x$ 就是 $g$ 。normalize 会去掉这样的包装：

test "eta removes a wrapper" {
  let wrapped = lam("x", ap(lv("g"), lv("x")))
  assert_eq(@lambda.normalize(wrapped, 10), NormalForm(term=lv("g"), steps=1))
  let not_a_wrapper = lam("x", ap(lv("x"), lv("x")))
  assert_eq(
    @lambda.normalize(not_a_wrapper, 10),
    NormalForm(term=not_a_wrapper, steps=0),
  )
}

处理不终止的项

$\Omega = (\lambda w.\,w\,w)(\lambda w.\,w\,w)$ 永远归约到自身。步数上限把这变成一个你可以检测的结果：

test "omega hits the step limit" {
  let self_apply = lam("w", ap(lv("w"), lv("w")))
  let omega = ap(self_apply, self_apply)
  match @lambda.normalize(omega, 50) {
    StepLimitReached(steps~, ..) => assert_eq(steps, 50)
    NormalForm(..) => fail("omega has no normal form")
  }
  // a discarded omega is harmless under normal order
  assert_eq(nf(ap(lam("x", lv("y")), omega)), lv("y"))
}

进阶

只用 beta，或换一种策略

normalize 固定使用 beta-eta 和正规序。对于其他组合，把规则和策略传给 @eval.evaluate（导入 Luna-Flow/type_theory/eval）：

test "beta only, weak head" {
  let term = ap(lam("x", lam("y", ap(lv("x"), lv("y")))), lv("g"))
  let rule = @rewrite.RuleName::unsafe_new("beta")
  match @eval.evaluate(term, rule, @lambda.beta_rule, WeakHead, 10) {
    NormalForm(term=result, steps~) => {
      assert_eq(steps, 1)
      assert_true(@syntax.alpha_equal(result, lam("y", ap(lv("g"), lv("y")))))
    }
    StepLimitReached(..) => fail("one step")
  }
}

弱头策略下只用 beta 会停在 $\lambda y.\,g\,y$ ；normalize 还会把它 eta 归约为 $g$ 。

领域值

Value(v) 是一个从不归约、在代换中被复制的常量。用你自己的规则为常量添加归约规则（例如 Value(Int) 上的算术），并按 rewrite 教程所示把它与 beta_rule 组合。

更快的范式化

具名项上的正规序归约会重命名绑定子，并从根部重复搜索。对于大型项，请用 @debruijn.from_named 转换并使用 utlc/nbe。

常见陷阱

n 元应用与 eta。 Bind(x, …) 之下的 Apply(f, [a, x]) 不会被 eta 归约；如果依赖 eta，请用 application（一元）构建应用。
用 == 比较。 beta 会重命名绑定子以避免捕获；请使用 @syntax.alpha_equal。
把 StepLimitReached 理解为发散。 它只表示达到了上限。可范式化的项也可能需要很多步。
期望常量会计算。 Value(1) 作用于任何东西都会卡住；该演算没有内置算术。

后续步骤

utlc/lambda API：精确的契约。
utlc/lambda 设计：beta、eta 以及经典定理。
stlc 教程：每个项都可范式化的带类型演算。