Luna Flow
简体中文

utlc/nbe 教程

本教程用基于求值的范式化来范式化无类型 lambda 项：在燃料预算内快速得到 De Bruijn 项的范式。你将范式化用名书写的项、选择预算、读取 consumed 计数器，并将结果与小步归约器比较。

快速入门

moon add Luna-Flow/type_theory@0.2.0
import {
  "Luna-Flow/type_theory/core",
  "Luna-Flow/type_theory/syntax",
  "Luna-Flow/type_theory/debruijn",
  "Luna-Flow/type_theory/utlc/nbe",
}
test "quick start: (λ. 0) 5" {
  let term : @debruijn.DbTerm[Int] = Apply(Bind(Bound(0)), [Value(5)])
  match @nbe.normalize(term, 100) {
    NormalForm(term=normal, consumed~) => {
      assert_eq(normal, Value(5))
      assert_true(consumed > 0)
    }
    _ => fail("small closed term")
  }
}

日常任务

范式化具名项

用名书写项，用 from_named 转换，范式化，再转换回来以便显示：

fn church(n : Int) -> @syntax.Term[Int] {
  let f = @core.Name::new("f")
  let x = @core.Name::new("x")
  let mut body : @syntax.Term[Int] = Variable(x)
  for _ in 0..<n {
    body = Apply(Variable(f), [body])
  }
  Bind(f, Bind(x, body))
}

test "2 * 3 = 6 with Church numerals" {
  let m = @core.Name::new("m")
  let n = @core.Name::new("n")
  let f = @core.Name::new("f")
  // times = λm. λn. λf. m (n f)
  let times : @syntax.Term[Int] = Bind(
    m,
    Bind(n, Bind(f, Apply(Variable(m), [Apply(Variable(n), [Variable(f)])]))),
  )
  let term : @syntax.Term[Int] = Apply(times, [church(2), church(3)])
  match @nbe.normalize(@debruijn.from_named(term), 10_000) {
    NormalForm(term=normal, ..) => assert_eq(normal, @debruijn.from_named(church(6)))
    _ => fail("normalizes")
  }
}

用 == 比较 De Bruijn 形式就是在 α-等价意义下比较。

选择燃料预算

燃料限制的是工作量，而不是时间。燃料太少会得到 FuelExhausted；成功运行的 consumed 值正是该次运行所需的确切数量：

test "the budget a run needs" {
  let id : @debruijn.DbTerm[Int] = Bind(Bound(0))
  let term : @debruijn.DbTerm[Int] = Apply(id, [Apply(id, [Value(1)])])
  match @nbe.normalize(term, 1000) {
    NormalForm(consumed~, ..) => {
      assert_true(@nbe.normalize(term, consumed) is NormalForm(..))
      assert_true(@nbe.normalize(term, consumed - 1) is FuelExhausted(..))
    }
    _ => fail("normalizes")
  }
}

识别发散与惰性

Ω\Omega 永远不会到达范式，因此总会耗尽预算。从不使用的参数从不被求值，因此把 Ω\Omega 传给常函数是没问题的：

test "omega and a lazy argument" {
  let w : @debruijn.DbTerm[Int] = Bind(Apply(Bound(0), [Bound(0)]))
  let omega : @debruijn.DbTerm[Int] = Apply(w, [w])
  assert_true(@nbe.normalize(omega, 500) is FuelExhausted(consumed=500))
  let ignore : @debruijn.DbTerm[Int] = Bind(Value(0))
  assert_true(@nbe.normalize(Apply(ignore, [omega]), 500) is NormalForm(term=Value(0), ..))
}

拒绝作用域不正确的输入

normalize 先做校验，并把悬空索引作为数据报告：

test "scope errors are reported" {
  let bad : @debruijn.DbTerm[Int] = Bind(Bound(3))
  assert_eq(
    @nbe.normalize(bad, 100),
    ScopeFailure(error=UnboundIndex(index=3, depth=1), consumed=0),
  )
}

进阶

与小步归约比较

NbE 返回一元应用；@debruijn.normalize 保留 n 元脊。比较前先展平脊：

fn flatten(t : @debruijn.DbTerm[Int]) -> @debruijn.DbTerm[Int] {
  match t {
    Apply(head, args) => {
      let flat_args = args.map(flatten)
      match flatten(head) {
        Apply(h, inner) => Apply(h, [..inner, ..flat_args])
        h => Apply(h, flat_args)
      }
    }
    Bind(body) => Bind(flatten(body))
    other => other
  }
}

test "nbe agrees with small-step after flattening" {
  let f = @core.Name::new("f")
  // (λ. λ. f 1 0) 7 8
  let term : @debruijn.DbTerm[Int] = Apply(Bind(Bind(Apply(Free(f), [Bound(1), Bound(0)]))), [
    Value(7),
    Value(8),
  ])
  match (@nbe.normalize(term, 1000), @debruijn.normalize(term, 100)) {
    (NormalForm(term=a, ..), NormalForm(term=b, ..)) => {
      assert_false(a == b)
      assert_eq(flatten(a), flatten(b))
    }
    _ => fail("both normalize")
  }
}

直接使用流水线

eval 产生不透明的语义值；quote 将其读回。把两者分开很有用：可以只求值一次再在选定的层级读回，或读回用 reflect_free 构造的中性值：

test "eval and quote separately" {
  let k : @debruijn.DbTerm[Int] = Bind(Bind(Bound(1)))
  match @nbe.eval(k, 100) {
    Evaluated(value~, ..) =>
      assert_true(@nbe.quote(value, 0, 100) is Quoted(term=Bind(Bind(Bound(1))), ..))
    _ => fail("closed term")
  }
}

常见陷阱

  • 用 == 与小步结果比较。 脊的形状不同；请先展平。
  • 把 FuelExhausted 当作发散。 它只说明预算用完了。请提高预算，或使用不需要预算的带类型 stlc 范式化器。
  • 重复的参数。 求值是无共享的传名调用；多次使用某个昂贵参数的项每次都要为它付出代价。
  • 带悬空索引的开项。 自由变量必须是 Free(name)；没有绑定子的 Bound 索引是作用域错误。

后续步骤