utlc/nbe API

utlc/nbe 包通过求值来范式化无类型 De Bruijn 项：eval 在惰性语义域中解释项，quote 把语义值读回为 beta 范式项，normalize 则两者都做。每个阶段都会消耗燃料，因此发散项以 FuelExhausted 结束，而不会永远运行下去。

import {
  "Luna-Flow/type_theory/core",
  "Luna-Flow/type_theory/debruijn",
  "Luna-Flow/type_theory/utlc/nbe",
}

默认别名为 @nbe。语义域和正确性论证见 utlc/nbe 设计。

燃料

燃料是以单位计量的步数预算：每次对项节点求值、每次强制延迟值、每次读回值都花费一个单位。所有结果都报告 consumed，即所用的单位数。燃料 <= 0 的调用不做任何事，直接返回 FuelExhausted(consumed=0)（quote 会先拒绝负的层级）。调用结果与超出其消耗量的燃料无关：若燃料为 $f$ 的调用在消耗 $c$ 个单位后返回范式，则任何燃料至少为 $c$ 的调用都返回相同的结果。

语义值

Semantic

Semantic[T] 是不透明的语义值。

pub struct Semantic[T] {
  inner : SemanticInner[T]
}

type SemanticInner[T]

语义值是常量、闭包（带有环境的绑定子体）、延迟参数或中性值（自由变量、某个 quote 层级上的变量，或作用于参数的中性值）。其表示是私有的；值由 eval 和 reflect_* 函数产生，由 quote 消费。

reflect_free

reflect_free 把自由名转换为中性语义值。

pub fn[T] reflect_free(@core.Name) -> Semantic[T]

对其 quote 得到 Free(name)。

reflect_level

reflect_level 把 quote 层级转换为中性语义变量。

pub fn[T] reflect_level(Int) -> Semantic[T]?

层级为负时返回 None。在深度 n > l 处对层级 l 的变量 quote 得到 Bound(n - l - 1)。

test "reflect and quote neutral values" {
  let y = @core.Name::new("y")
  let free : @nbe.Semantic[Int] = @nbe.reflect_free(y)
  assert_true(@nbe.quote(free, 0, 10) is Quoted(term=Free(_), ..))
  match @nbe.reflect_level(0) {
    Some(v) => {
      let value : @nbe.Semantic[Int] = v
      // the variable of level 0, seen from depth 2, is index 1
      assert_true(@nbe.quote(value, 2, 10) is Quoted(term=Bound(1), ..))
    }
    None => fail("level 0 is valid")
  }
  let negative : @nbe.Semantic[Int]? = @nbe.reflect_level(-1)
  assert_true(negative is None)
}

求值与读回

EvaluationResult

EvaluationResult[T] 是 eval 的结果。

pub(all) enum EvaluationResult[T] {
  Evaluated(value~ : Semantic[T], consumed~ : Int)
  FuelExhausted(consumed~ : Int)
  ScopeFailure(error~ : @debruijn.ScopeError, consumed~ : Int)
}

eval

eval 在惰性语义域中把闭 De Bruijn 项求值为弱头形式。

pub fn[T] eval(@debruijn.DbTerm[T], Int) -> EvaluationResult[T]

项必须是良作用域的（允许自由名）；否则结果为 ScopeFailure，且 consumed=0。求值采用传名调用：参数被延迟，仅在需要时求值；求值在闭包或中性值处停止，不进入绑定子。

QuoteResult

QuoteResult[T] 是 quote 的结果。

pub(all) enum QuoteResult[T] {
  Quoted(term~ : @debruijn.DbTerm[T], consumed~ : Int)
  FuelExhausted(consumed~ : Int)
  ScopeFailure(error~ : @debruijn.ScopeError, consumed~ : Int)
}

quote

quote 把语义值读回为 beta 范式的 De Bruijn 项。

pub fn[T] quote(Semantic[T], Int, Int) -> QuoteResult[T]

quote(value, level, fuel) 在 level 个绑定子之下读回 value。闭包的读回方式是：把它作用于当前层级的一个新变量，再在多一层绑定子之下读回结果；中性应用逐个参数读回，这会强制延迟参数。对来自 eval 的值使用 level = 0。负的 level，或不小于 level 的层级变量，会得到 ScopeFailure(NegativeIndex)。

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

范式化

NbeResult

NbeResult[T] 是 normalize 的结果。

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

normalize

normalize 在燃料预算内计算良作用域 De Bruijn 项的 beta 范式。

pub fn[T] normalize(@debruijn.DbTerm[T], Int) -> NbeResult[T]

它校验项、对其求值并在层级 0 对结果 quote，三者共享同一预算。NormalForm(t, c)：t 是 beta 范式，用 c 个单位得到。FuelExhausted(c)：预算耗尽；该项可能发散，也可能需要更多燃料。ScopeFailure：输入含有悬空或负的索引。

结果中的应用是一元的：范式 $f\,a\,b$ 以 Apply(Apply(f, [a]), [b]) 返回，而 @debruijn.normalize 保留输入的 n 元脊 Apply(f, [a, b])。将脊展平后两者一致。

test "lazy evaluation skips an unused divergent argument" {
  let w : @debruijn.DbTerm[Int] = Bind(Apply(Bound(0), [Bound(0)]))
  let omega : @debruijn.DbTerm[Int] = Apply(w, [w])
  let term : @debruijn.DbTerm[Int] = Apply(Bind(Value(7)), [omega])
  assert_true(@nbe.normalize(term, 100) is NormalForm(term=Value(7), ..))
  assert_true(@nbe.normalize(omega, 100) is FuelExhausted(_))
}