debruijn API

debruijn 包用 De Bruijn 索引表示约束变量：Bound(i) 指向向上第 i 层的绑定子。它在 De Bruijn 语法与具名语法之间相互转换，检查作用域，对索引进行移位和代换，并实现无需任何重命名的最左最外 β-归约。自由变量保持具名。

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

移位与实例化的定义及其性质的推导见 debruijn 设计。

项与错误

DbTerm

DbTerm[T] 是带无名绑定子的 λ 语法。

pub(all) enum DbTerm[T] {
  Value(T)
  Free(@core.Name)
  Bound(Int)
  Apply(DbTerm[T], Array[DbTerm[T]])
  Bind(DbTerm[T])
} derive(Eq, @debug.Debug)

• Value(v) 是领域常量，与 @syntax.Term 中一样是不透明的。
• Free(x) 是自由变量，按名字保存。
• Bound(i) 指向第 i 个外围 Bind，最内层从 0 开始计数。
• Apply(head, args) 是 n 元应用，按柯里化的脊（spine）来理解。
• Bind(body) 是绑定子；其变量在 body 中为 Bound(0)。

当每个 Bound(i) 都位于多于 i 个绑定子之下时，称该项是良作用域的。由于绑定子不携带名字，良作用域项上的 ==（DbTerm::equal）就是 α-等价。

DbTerm::equal

DbTerm::equal 按结构比较两个项。

pub fn[T : Eq] DbTerm::equal(Self[T], Self[T]) -> Bool

ScopeError

ScopeError 描述一个不指向任何绑定子的索引。

pub(all) enum ScopeError {
  UnboundIndex(index~ : Int, depth~ : Int)
  NegativeIndex(index~ : Int)
  NegativeShift(index~ : Int, delta~ : Int, cutoff~ : Int)
} derive(Eq, @debug.Debug)
pub fn ScopeError::equal(Self, Self) -> Bool

• UnboundIndex(index, depth)：Bound(index) 仅出现在 depth 个绑定子之下。
• NegativeIndex(index)：负索引。
• NegativeShift(index, delta, cutoff)：将 Bound(index) 移位 delta 会使其变为负数；cutoff 是该出现处的有效截断值。

转换与验证

from_named

from_named 将具名语法转换为 De Bruijn 语法。

pub fn[T] from_named(@syntax.Term[T]) -> DbTerm[T]

由外围 Bind 绑定的变量变为 Bound(i)，其中 i 计数该出现与其绑定子之间的绑定子个数（同名时最近的绑定子胜出）。自由变量变为 Free。结果总是良作用域的，且 α-等价的具名项给出相等的结果。

to_named

to_named 将 De Bruijn 语法转换回具名语法，并使用确定性的绑定子名字。

pub fn[T] to_named(DbTerm[T]) -> Result[@syntax.Term[T], ScopeError]

绑定子依次命名为 x、x_1、x_2、…：每个绑定子取该序列中第一个既不是项的自由名字、也不是外围绑定子名字的名字。对作用域不良的项返回 Err(NegativeIndex) 或 Err(UnboundIndex)。对良作用域的 d，from_named(to_named(d)) 就是 d；对具名项 t，to_named(from_named(t)) 与 t α-等价。

test "named and nameless round trip" {
  let x = @core.Name::new("x")
  let y = @core.Name::new("y")
  let named : @syntax.Term[Int] = Bind(y, Apply(Variable(y), [Variable(x)]))
  let db = @debruijn.from_named(named)
  assert_eq(db, Bind(Apply(Bound(0), [Free(x)])))
  match @debruijn.to_named(db) {
    Ok(back) => {
      assert_true(@syntax.alpha_equal(back, named))
      assert_true(back is Bind(binder, _) && binder.text() == "x_1")
    }
    Err(_) => fail("well scoped")
  }
}

绑定子变为 x_1，因为 x 是该项的自由名字。

validate

validate 检查每个约束索引都指向某个外围绑定子。

pub fn[T] validate(DbTerm[T]) -> Result[Unit, ScopeError]

对良作用域项返回 Ok(())，否则返回按前序遍历找到的第一个错误。

test "dangling index" {
  let bad : @debruijn.DbTerm[Int] = Bind(Bound(1))
  assert_eq(@debruijn.validate(bad), Err(UnboundIndex(index=1, depth=1)))
  let good : @debruijn.DbTerm[Int] = Bind(Bound(0))
  assert_eq(@debruijn.validate(good), Ok(()))
}

索引操作

shift

shift 将 delta 加到每个相对于截断值为自由的索引上。

pub fn[T] shift(DbTerm[T], Int, Int) -> Result[DbTerm[T], ScopeError]

shift(t, delta, cutoff) 即操作 $\uparrow^{delta}_{cutoff}$：在 k 个绑定子之下，索引 i >= cutoff + k 变为 i + delta，较小的索引保持不变。若某索引会变为负数则返回 Err(NegativeShift)，若输入包含负索引则返回 Err(NegativeIndex)。

substitute_bound

substitute_bound 用一个项替换一个自由索引。

pub fn[T] substitute_bound(DbTerm[T], Int, DbTerm[T]) -> Result[DbTerm[T], ScopeError]

substitute_bound(t, j, s) 即 $[j \mapsto s]\,t$：在 k 个绑定子之下，Bound(j + k) 被替换为向上移位 k 的 s，使 s 的自由索引仍指向相同的绑定子。其他索引不变；结果的绑定子计数不作调整。对负的 j 或 t 中的负索引返回 Err(NegativeIndex)。它不检查未绑定的索引；请使用 validate 进行检查。

instantiate

instantiate 用一个实参打开绑定子的体。

pub fn[T] instantiate(DbTerm[T], DbTerm[T]) -> Result[DbTerm[T], ScopeError]

instantiate(body, arg) 计算 $\uparrow^{-1}_0\big([0 \mapsto \uparrow^{1}_0 arg]\,body\big)$，即 β 步 $(\lambda.\,body)\,arg$ 的结果。在良作用域输入上它从不返回错误。

test "instantiate a binder body" {
  let y = @core.Name::new("y")
  // body of λ. λ. 1 0, i.e. λ. (outer variable) applied to (inner variable)
  let body : @debruijn.DbTerm[Int] = Bind(Apply(Bound(1), [Bound(0)]))
  assert_eq(
    @debruijn.instantiate(body, Free(y)),
    Ok(Bind(Apply(Free(y), [Bound(0)]))),
  )
  let open_term : @debruijn.DbTerm[Int] = Bind(Apply(Bound(0), [Bound(1)]))
  assert_eq(
    @debruijn.shift(open_term, 2, 0),
    Ok(Bind(Apply(Bound(0), [Bound(3)]))),
  )
  let under_binder : @debruijn.DbTerm[Int] = Bind(Bound(1))
  assert_eq(
    @debruijn.substitute_bound(under_binder, 0, Bound(5)),
    Ok(Bind(Bound(6))),
  )
}

归约

DbStepResult

DbStepResult[T] 是一次 De Bruijn 归约尝试的结果。

pub(all) enum DbStepResult[T] {
  NoStep
  Reduced(before~ : DbTerm[T], after~ : DbTerm[T], rule~ : @rewrite.RuleName, path~ : @rewrite.ReductionPath)
  ScopeFailure(ScopeError)
} derive(Eq, @debug.Debug)
pub fn[T : Eq] DbStepResult::equal(Self[T], Self[T]) -> Bool

NoStep 和 Reduced 的含义与 @rewrite.StepResult 相同；规则名总是 "beta"。ScopeFailure 报告在收缩可约式时遇到的索引错误。

reduce_once

reduce_once 执行一步最左最外 β 归约。

pub fn[T] reduce_once(DbTerm[T]) -> DbStepResult[T]

可约式形如 Apply(Bind(body), [a, ..rest])；它变为 instantiate(body, a)，若 rest 非空则再应用于 rest。搜索顺序为：根，然后头部，然后从左到右的各参数，并且会进入绑定子的体。reduce_once 不验证其输入：如果项可能作用域不良，请先调用 validate。

DbNormalizationResult

DbNormalizationResult[T] 是有界 De Bruijn 范式化的结果。

pub(all) enum DbNormalizationResult[T] {
  NormalForm(term~ : DbTerm[T], steps~ : Int)
  StepLimitReached(term~ : DbTerm[T], steps~ : Int)
  ScopeFailure(term~ : DbTerm[T], error~ : ScopeError, steps~ : Int)
} derive(Eq, @debug.Debug)
pub fn[T : Eq] DbNormalizationResult::equal(Self[T], Self[T]) -> Bool

ScopeFailure 携带尝试失败步骤时所在的项，以及在此之前已执行的步数。

normalize

normalize 重复执行 reduce_once，直到没有可执行的步骤、某一步失败或达到步数上限。

pub fn[T] normalize(DbTerm[T], Int) -> DbNormalizationResult[T]

它遵循 @rewrite.normalize 的步数契约：最多 max_steps 步，并额外调用一次 reduce_once 来判定最终项。

test "nameless beta reduction" {
  let f = @core.Name::new("f")
  // λ. f ((λ. 0) 7)
  let term : @debruijn.DbTerm[Int] = Bind(
    Apply(Free(f), [Apply(Bind(Bound(0)), [Value(7)])]),
  )
  match @debruijn.reduce_once(term) {
    Reduced(after~, path~, rule~, ..) => {
      assert_eq(after, Bind(Apply(Free(f), [Value(7)])))
      assert_eq(path.to_array(), [@rewrite.BinderBody, @rewrite.ApplyArgument(0)])
      inspect(rule.value(), content="beta")
    }
    _ => fail("expected a beta step")
  }
  assert_eq(
    @debruijn.normalize(term, 10),
    NormalForm(term=Bind(Apply(Free(f), [Value(7)])), steps=1),
  )
}