eval 教程

本教程使用 eval 中的具名策略运行一条改写规则：正规序、应用序和弱头。你将看到它们在哪些地方一致、在哪些地方不同，以及如何编写你自己的策略。示例使用 utlc/lambda 中无类型 lambda 演算的 β 规则。

快速入门

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/eval",
  "Luna-Flow/type_theory/utlc/lambda",
}

将恒等函数应用于 42：

test "quick start: (λx. x) 42" {
  let x = @core.Name::new("x")
  let term : @syntax.Term[Int] = Apply(Bind(x, Variable(x)), [Value(42)])
  let beta = @rewrite.RuleName::unsafe_new("beta")
  assert_eq(
    @eval.evaluate(term, beta, @lambda.beta_rule, NormalOrder, 10),
    NormalForm(term=Value(42), steps=1),
  )
}

日常任务

各任务共用以下辅助函数：

fn nm(text : String) -> @core.Name {
  @core.Name::new(text)
}

fn omega() -> @syntax.Term[Int] {
  let w = nm("w")
  let self_apply : @syntax.Term[Int] = Bind(w, Apply(Variable(w), [Variable(w)]))
  Apply(self_apply, [self_apply])
}

fn beta_name() -> @rewrite.RuleName {
  @rewrite.RuleName::unsafe_new("beta")
}

选择一个会终止的策略

正规序是范式化的：如果一个项有范式，它就能找到。应用序先对参数求值，即使某个发散的参数最终被丢弃，也会在其上陷入死循环：

test "discarding a divergent argument" {
  let term : @syntax.Term[Int] = Apply(Bind(nm("x"), Value(0)), [omega()])
  assert_eq(
    @eval.evaluate(term, beta_name(), @lambda.beta_rule, NormalOrder, 20),
    NormalForm(term=Value(0), steps=1),
  )
  match @eval.evaluate(term, beta_name(), @lambda.beta_rule, ApplicativeOrder, 20) {
    StepLimitReached(steps~, ..) => assert_eq(steps, 20)
    NormalForm(..) => fail("applicative order should loop on omega")
  }
}

只求值到弱头范式

一旦项是抽象，或是头部不可归约的应用，WeakHead 就立即停止。它不会查看内部：

test "weak head normal form" {
  let x = nm("x")
  let f = nm("f")
  let id : @syntax.Term[Int] = Bind(x, Variable(x))
  let term : @syntax.Term[Int] = Apply(id, [Bind(f, Apply(id, [Variable(f)]))])
  match @eval.evaluate(term, beta_name(), @lambda.beta_rule, WeakHead, 10) {
    NormalForm(term=result, steps~) => {
      assert_eq(steps, 1)
      assert_true(result is Bind(_, Apply(_, _)))
    }
    StepLimitReached(..) => fail("one step suffices")
  }
}

结果 $\lambda f.\,(\lambda x.\,x)\,f$ 在绑定子之下仍包含一个可约式；NormalOrder 会将其归约。

追踪各个步骤

trace 记录每一步及其路径，这对于解释一次范式化或逐步比较两种策略很有用：

test "trace normal order" {
  let x = nm("x")
  let y = nm("y")
  let k : @syntax.Term[Int] = Bind(x, Bind(y, Variable(x)))
  let term : @syntax.Term[Int] = Apply(k, [Value(1), omega()])
  let run = @eval.trace(term, beta_name(), @lambda.beta_rule, NormalOrder, 10)
  let paths = run
    .steps()
    .map(s => match s {
      Reduced(path~, ..) => path.to_array().length()
      NoStep => -1
    })
  assert_eq(paths, [0, 0])
  assert_eq(run.result(), NormalForm(term=Value(1), steps=2))
}

两步都发生在根部：先在脊 $K\,1\,\Omega$ 内部收缩 $K\,1$，然后将结果应用于 $\Omega$，后者被丢弃。

使用领域规则

策略适用于任何规则，而不仅是 β。这里有一条折叠字面量加法的规则；正规序最后才折叠外层的加法：

fn fold_add(t : @syntax.Term[Int]) -> @syntax.Term[Int]? {
  match t {
    Apply(Variable(op), [Value(a), Value(b)]) if op.text() == "add" => Some(Value(a + b))
    _ => None
  }
}

test "fold additions" {
  let add = @syntax.Term::Variable(nm("add"))
  let term : @syntax.Term[Int] = Apply(add, [Apply(add, [Value(1), Value(2)]), Value(3)])
  let rule = @rewrite.RuleName::unsafe_new("fold_add")
  assert_eq(
    @eval.evaluate(term, rule, fold_add, NormalOrder, 10),
    NormalForm(term=Value(6), steps=2),
  )
}

进阶

编写你自己的策略

任何从项到 StepResult 的函数都是 @rewrite.normalize 的一种策略。下面这个只在根部归约，便于单独测试一条规则：

fn root_only(
  rule : (@syntax.Term[Int]) -> @syntax.Term[Int]?,
) -> (@syntax.Term[Int]) -> @rewrite.StepResult[Int] {
  t => match rule(t) {
    Some(after) =>
      Reduced(before=t, after~, rule=beta_name(), path=@rewrite.ReductionPath::root())
    None => NoStep
  }
}

test "a root-only strategy" {
  let x = nm("x")
  let term : @syntax.Term[Int] = Bind(x, Apply(Bind(x, Variable(x)), [Value(5)]))
  assert_eq(
    @rewrite.normalize(term, root_only(@lambda.beta_rule), 10),
    NormalForm(term~, steps=0),
  )
}

手写的步骤必须遵守 StepResult 的约定：after 恰好是将 before 在 path 处的子项改写后的结果。

相互检验策略

对于 β 这样具有合流性的规则，两个都到达范式的策略在 α-等价意义下一致。这构成了一种低成本的回归测试：

test "strategies agree when both terminate" {
  let x = nm("x")
  let y = nm("y")
  let term : @syntax.Term[Int] = Apply(Bind(x, Apply(Variable(x), [Variable(x)])), [
    Bind(y, Variable(y)),
  ])
  match
    (
      @eval.evaluate(term, beta_name(), @lambda.beta_rule, NormalOrder, 20),
      @eval.evaluate(term, beta_name(), @lambda.beta_rule, ApplicativeOrder, 20),
    ) {
    (NormalForm(term=a, ..), NormalForm(term=b, ..)) =>
      assert_true(@syntax.alpha_equal(a, b))
    _ => fail("both strategies terminate here")
  }
}

常见陷阱

• 把 WeakHead 的 NormalForm 当作完全范式。 它只表示弱头范式。
• 期望 FullNormal 与 NormalOrder 不同。 目前它们使用相同的遍历。
• 用 == 比较结果。 β-归约会重命名绑定子（y_1）；请用 @syntax.alpha_equal 比较。
• 步数上限太小。 StepLimitReached 并不意味着发散。请提高上限，或使用 utlc/nbe 进行快速的无类型范式化。

后续步骤

• eval API：确切的签名。
• eval 设计：各策略的定义及其背后的经典定理。
• utlc/lambda 教程：建立在这些策略之上的 lambda 演算。