Luna Flow
简体中文

debruijn 教程

本教程将命名 lambda 项转换为 De Bruijn 形式，利用这种形式比较项并在无需重命名的情况下归约它们，验证不可信的无名输入，并将结果转换回带名字的形式以便显示。

快速入门

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/debruijn",
}

λx. λy. x\lambda x.\,\lambda y.\,x 变为 λ. λ. 1\lambda.\,\lambda.\,1：该变量指向向外一层的绑定子。

test "quick start: the K combinator without names" {
  let x = @core.Name::new("x")
  let y = @core.Name::new("y")
  let k : @syntax.Term[Int] = Bind(x, Bind(y, Variable(x)))
  assert_eq(@debruijn.from_named(k), Bind(Bind(Bound(1))))
}

日常任务

在约束名字的意义下比较项

α-等价的命名项具有相同的 De Bruijn 形式，因此转换后的 == 可判定 α-等价：

test "alpha-equivalence by conversion" {
  let a : @syntax.Term[Int] = Bind(@core.Name::new("p"), Variable(@core.Name::new("p")))
  let b : @syntax.Term[Int] = Bind(@core.Name::new("q"), Variable(@core.Name::new("q")))
  assert_eq(@debruijn.from_named(a), @debruijn.from_named(b))
}

@syntax.alpha_equal 无需构建转换后的项即可给出相同的答案；当你需要保留无名形式做进一步处理时，转换才物有所值。

无需重命名的归约

在无名项上的 β-归约通过移位索引而不是重命名绑定子来完成。经典的捕获示例 (λx. λy. x) y(\lambda x.\,\lambda y.\,x)\,y 不需要新鲜名字：

test "beta without capture problems" {
  let y = @core.Name::new("y")
  let term : @debruijn.DbTerm[Int] = Apply(Bind(Bind(Bound(1))), [Free(y)])
  assert_eq(
    @debruijn.normalize(term, 10),
    NormalForm(term=Bind(Free(y)), steps=1),
  )
}

自由的 y 保持自由，因为它是一个名字；内层绑定子不需要新名字，因为它根本没有名字。

验证不可信的输入

手工构建或从外部读取的项可能包含超出所有绑定子的索引。请在归约之前检查它们：

test "reject a dangling index" {
  let bad : @debruijn.DbTerm[Int] = Bind(Apply(Bound(0), [Bound(2)]))
  match @debruijn.validate(bad) {
    Err(UnboundIndex(index~, depth~)) => {
      assert_eq(index, 2)
      assert_eq(depth, 1)
    }
    _ => fail("expected an unbound index")
  }
}

转换回带名字的形式以便显示

to_named 将绑定子命名为 x、x_1、…，并避开项中的自由名字：

test "readable names come back" {
  let x = @core.Name::new("x")
  let term : @debruijn.DbTerm[Int] = Bind(Bind(Apply(Bound(1), [Free(x)])))
  match @debruijn.to_named(term) {
    Ok(Bind(outer, Bind(inner, _))) => {
      inspect(outer.text(), content="x_1")
      inspect(inner.text(), content="x_2")
    }
    _ => fail("well scoped")
  }
}

绑定子跳过了 x，因为 x 在项中是自由的。

手工打开绑定子

instantiate(body, arg) 是 (λ. body) arg(\lambda.\,body)\,arg 的结果。在实现你自己的归约器或求值器时使用它：

test "open a binder" {
  // body of λ. (λ. 1 0): the outer variable applied to the inner one
  let body : @debruijn.DbTerm[Int] = Bind(Apply(Bound(1), [Bound(0)]))
  assert_eq(
    @debruijn.instantiate(body, Value(9)),
    Ok(Bind(Apply(Value(9), [Bound(0)]))),
  )
}

进阶

用无名归约器检验命名归约器

由于转换与 β-归约可交换，命名归约器与无名归约器必须在 α-等价意义下一致。对于你编写的任何归约器，这都是一个很好的性质测试：

fn named_beta(t : @syntax.Term[Int]) -> @syntax.Term[Int]? {
  match t {
    Apply(Bind(x, body), [arg]) =>
      Some(@substitution.Substitution::singleton(x, arg).apply(body))
    _ => None
  }
}

test "named and nameless beta agree" {
  let x = @core.Name::new("x")
  let y = @core.Name::new("y")
  let named : @syntax.Term[Int] = Apply(Bind(x, Bind(y, Apply(Variable(x), [Variable(y)]))), [
    Variable(y),
  ])
  match (named_beta(named), @debruijn.reduce_once(@debruijn.from_named(named))) {
    (Some(n), Reduced(after~, ..)) => assert_eq(@debruijn.from_named(n), after)
    _ => fail("both reduce")
  }
}

（此示例还导入了 Luna-Flow/type_theory/substitution。）

快速范式化

normalize 从根部反复执行一次“搜索并收缩”的步骤，简单且可追踪，但对于很长的归约很慢。对于大型无类型项，请使用 utlc/nbe，它作用于相同的 DbTerm 并返回相同的范式（在应用脊的形状意义下）。

常见陷阱

  • 从外向内计数索引。 Bound(0) 是最内层的绑定子。λx. λy. x\lambda x.\,\lambda y.\,x 是 Bind(Bind(Bound(1)))，而不是 Bound(0)。
  • 归约未经验证的项。 reduce_once 和 substitute_bound 不会检测未绑定的索引。对于不是用 from_named 构建的输入，请先调用 validate。
  • 期望绑定子名字得以保留。 to_named(from_named(t)) 与 t α-等价，但绑定子名字是重新生成的。
  • 应用脊。 Apply(f, [a, b]) 和 Apply(Apply(f, [a]), [b]) 表示同一个应用，但它们是不同的值；用 == 比较之前请先将它们规整为同一种形状。

后续步骤