eval API

eval 包为常见的归约策略命名，并用其中一种策略运行任意重写规则：单步、有界范式化或完整轨迹。它是 rewrite 之上的一层薄封装；规则本身（β、η 或某个领域化简）由调用者提供。

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

示例使用 Luna-Flow/type_theory/utlc/lambda（别名 @lambda）的 β 规则。这些策略的精确定义见 eval 设计。

`Strategy`

Strategy 选择下一步发生的位置。

pub(all) enum Strategy {
  NormalOrder
  ApplicativeOrder
  WeakHead
  FullNormal
} derive(Eq, @debug.Debug)

策略	下一个位置	是否进入绑定子和参数
`NormalOrder`	最左最外可约式（`@rewrite.top_down_once`）	是
`ApplicativeOrder`	最左最内可约式（`@rewrite.bottom_up_once`）	是
`WeakHead`	根，否则为应用的头部，递归进行	否
`FullNormal`	与 `NormalOrder` 相同	是

FullNormal 目前选择与 NormalOrder 相同的遍历；它表达“归约到完全范式”的意图，若将来加入另一种完全范式化遍历，则可能与 NormalOrder 不同。

`Strategy::equal`

Strategy::equal 比较两个策略。

pub fn Strategy::equal(Self, Self) -> Bool

它是提升的 Eq 实现；新代码中请使用 ==。

`reduce_once`

reduce_once 使用某个策略执行至多一步归约。

pub fn[T] reduce_once(@syntax.Term[T], @rewrite.RuleName, (@syntax.Term[T]) -> @syntax.Term[T]?, Strategy) -> @rewrite.StepResult[T]

结果遵循 @rewrite.StepResult 的契约：Reduced 报告一个被重写的位置及其路径。对于 NormalOrder、FullNormal 和 ApplicativeOrder，NoStep 表示规则在任何位置都不适用。对于 WeakHead，NoStep 表示规则既不适用于根，也不适用于应用脊上的任何头部位置；此时该项相对于该规则处于弱头范式，但在绑定子之下或参数中仍可能包含可约式。

test "weak head stops at a binder" {
  let x = @core.Name::new("x")
  let y = @core.Name::new("y")
  let z = @core.Name::new("z")
  let id : @syntax.Term[Int] = Bind(y, Variable(y))
  let term : @syntax.Term[Int] = Bind(x, Apply(id, [Variable(z)]))
  let beta = @rewrite.RuleName::unsafe_new("beta")
  assert_true(@eval.reduce_once(term, beta, @lambda.beta_rule, WeakHead) is NoStep)
  match @eval.reduce_once(term, beta, @lambda.beta_rule, NormalOrder) {
    Reduced(after~, path~, ..) => {
      assert_eq(after, Bind(x, Variable(z)))
      assert_eq(path.to_array(), [@rewrite.BinderBody])
    }
    NoStep => fail("expected a step under the binder")
  }
}

`evaluate`

evaluate 通过以某个策略重复 reduce_once 来范式化一个项。

pub fn[T] evaluate(@syntax.Term[T], @rewrite.RuleName, (@syntax.Term[T]) -> @syntax.Term[T]?, Strategy, Int) -> @rewrite.NormalizationResult[T]

evaluate(term, name, rule, strategy, max_steps) 即 @rewrite.normalize(term, t => reduce_once(t, name, rule, strategy), max_steps)，具有相同的步数契约：最多 max_steps 步，且仅当策略在某个项上找不到步骤时才返回 NormalForm。

test "normal order finds a normal form that applicative order misses" {
  let x = @core.Name::new("x")
  let y = @core.Name::new("y")
  let w = @core.Name::new("w")
  let self_apply : @syntax.Term[Int] = Bind(w, Apply(Variable(w), [Variable(w)]))
  let omega : @syntax.Term[Int] = Apply(self_apply, [self_apply])
  let term : @syntax.Term[Int] = Apply(Bind(x, Variable(y)), [omega])
  let beta = @rewrite.RuleName::unsafe_new("beta")
  assert_eq(
    @eval.evaluate(term, beta, @lambda.beta_rule, NormalOrder, 10),
    NormalForm(term=Variable(y), steps=1),
  )
  assert_true(
    @eval.evaluate(term, beta, @lambda.beta_rule, ApplicativeOrder, 10)
    is StepLimitReached(..),
  )
}

`trace`

trace 像 evaluate 一样范式化，并记录每一步。

pub fn[T] trace(@syntax.Term[T], @rewrite.RuleName, (@syntax.Term[T]) -> @syntax.Term[T]?, Strategy, Int) -> @rewrite.ReductionTrace[T]

它就是带有该策略步进函数的 @rewrite.trace。该轨迹满足 @rewrite.ReductionTrace 的链接不变式。

test "trace a two-step reduction" {
  let x = @core.Name::new("x")
  let y = @core.Name::new("y")
  let k : @syntax.Term[Int] = Bind(x, Bind(y, Variable(x)))
  let term : @syntax.Term[Int] = Apply(k, [Value(1), Value(2)])
  let beta = @rewrite.RuleName::unsafe_new("beta")
  let run = @eval.trace(term, beta, @lambda.beta_rule, NormalOrder, 10)
  assert_eq(run.steps().length(), 2)
  assert_eq(run.result(), NormalForm(term=Value(1), steps=2))
}