eval API

eval パッケージは一般的な簡約戦略に名前を与え、そのいずれかで任意の書き換え規則を実行する：1 ステップ、上限付き正規化、または完全なトレースである。これは 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 は 2 つの戦略を比較する。

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

これは昇格された Eq 実装である。新しいコードでは == を使うこと。

`reduce_once`

reduce_once は戦略に従って高々 1 ステップの簡約を行う。

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

結果は @rewrite.StepResult の契約に従う：Reduced は書き換えられた 1 つの位置とそのパスを報告する。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 は 1 つの戦略で 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))
}