eval チュートリアル

このチュートリアルでは、eval の名前付き戦略（正規順序、適用順序、弱頭部）で書き換え規則を実行する。それらがどこで一致し、どこで異なるか、また独自の戦略をどう書くかを見ていく。例では utlc/lambda の型なしラムダ計算の β 規則を使う。

クイックスタート

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/eval",
  "Luna-Flow/type_theory/utlc/lambda",
}

恒等関数を 42 に適用する。

test "quick start: (λx. x) 42" {
  let x = @core.Name::new("x")
  let term : @syntax.Term[Int] = Apply(Bind(x, Variable(x)), [Value(42)])
  let beta = @rewrite.RuleName::unsafe_new("beta")
  assert_eq(
    @eval.evaluate(term, beta, @lambda.beta_rule, NormalOrder, 10),
    NormalForm(term=Value(42), steps=1),
  )
}

日常的な作業

各作業では以下の補助関数を共有する。

fn nm(text : String) -> @core.Name {
  @core.Name::new(text)
}

fn omega() -> @syntax.Term[Int] {
  let w = nm("w")
  let self_apply : @syntax.Term[Int] = Bind(w, Apply(Variable(w), [Variable(w)]))
  Apply(self_apply, [self_apply])
}

fn beta_name() -> @rewrite.RuleName {
  @rewrite.RuleName::unsafe_new("beta")
}

停止する戦略を選ぶ

正規順序は正規化的である。項が正規形を持つなら、それを見つける。適用順序は引数を先に評価するので、発散する引数があると、それが捨てられる場合でも無限ループに陥る。

test "discarding a divergent argument" {
  let term : @syntax.Term[Int] = Apply(Bind(nm("x"), Value(0)), [omega()])
  assert_eq(
    @eval.evaluate(term, beta_name(), @lambda.beta_rule, NormalOrder, 20),
    NormalForm(term=Value(0), steps=1),
  )
  match @eval.evaluate(term, beta_name(), @lambda.beta_rule, ApplicativeOrder, 20) {
    StepLimitReached(steps~, ..) => assert_eq(steps, 20)
    NormalForm(..) => fail("applicative order should loop on omega")
  }
}

弱頭部正規形までだけ評価する

WeakHead は、項が抽象になるか、頭部が簡約できない適用になった時点で停止する。内部は見ない。

test "weak head normal form" {
  let x = nm("x")
  let f = nm("f")
  let id : @syntax.Term[Int] = Bind(x, Variable(x))
  let term : @syntax.Term[Int] = Apply(id, [Bind(f, Apply(id, [Variable(f)]))])
  match @eval.evaluate(term, beta_name(), @lambda.beta_rule, WeakHead, 10) {
    NormalForm(term=result, steps~) => {
      assert_eq(steps, 1)
      assert_true(result is Bind(_, Apply(_, _)))
    }
    StepLimitReached(..) => fail("one step suffices")
  }
}

結果 $\lambda f.\,(\lambda x.\,x)\,f$ は束縛子の下にまだ簡約基を含んでいる。NormalOrder ならそれを簡約する。

ステップを追跡する

trace は各ステップをそのパスとともに記録する。これは正規化を説明したり、二つの戦略をステップごとに比較したりするのに役立つ。

test "trace normal order" {
  let x = nm("x")
  let y = nm("y")
  let k : @syntax.Term[Int] = Bind(x, Bind(y, Variable(x)))
  let term : @syntax.Term[Int] = Apply(k, [Value(1), omega()])
  let run = @eval.trace(term, beta_name(), @lambda.beta_rule, NormalOrder, 10)
  let paths = run
    .steps()
    .map(s => match s {
      Reduced(path~, ..) => path.to_array().length()
      NoStep => -1
    })
  assert_eq(paths, [0, 0])
  assert_eq(run.result(), NormalForm(term=Value(1), steps=2))
}

どちらのステップも根で起こる。まずスパイン $K\,1\,\Omega$ の中で $K\,1$ が縮約され、次にその結果が $\Omega$ に適用され、この引数は捨てられる。

ドメイン規則を使う

戦略は β だけでなく任意の規則で動作する。ここではリテラルの加算を畳み込む規則を使う。正規順序では外側の加算が最後に畳み込まれる。

fn fold_add(t : @syntax.Term[Int]) -> @syntax.Term[Int]? {
  match t {
    Apply(Variable(op), [Value(a), Value(b)]) if op.text() == "add" => Some(Value(a + b))
    _ => None
  }
}

test "fold additions" {
  let add = @syntax.Term::Variable(nm("add"))
  let term : @syntax.Term[Int] = Apply(add, [Apply(add, [Value(1), Value(2)]), Value(3)])
  let rule = @rewrite.RuleName::unsafe_new("fold_add")
  assert_eq(
    @eval.evaluate(term, rule, fold_add, NormalOrder, 10),
    NormalForm(term=Value(6), steps=2),
  )
}

さらに進んで

独自の戦略を書く

項から StepResult への任意の関数は @rewrite.normalize の戦略である。次のものは根でのみ簡約するので、規則を単独でテストするのに便利である。

fn root_only(
  rule : (@syntax.Term[Int]) -> @syntax.Term[Int]?,
) -> (@syntax.Term[Int]) -> @rewrite.StepResult[Int] {
  t => match rule(t) {
    Some(after) =>
      Reduced(before=t, after~, rule=beta_name(), path=@rewrite.ReductionPath::root())
    None => NoStep
  }
}

test "a root-only strategy" {
  let x = nm("x")
  let term : @syntax.Term[Int] = Bind(x, Apply(Bind(x, Variable(x)), [Value(5)]))
  assert_eq(
    @rewrite.normalize(term, root_only(@lambda.beta_rule), 10),
    NormalForm(term~, steps=0),
  )
}

手書きのステップは StepResult の約束を守らなければならない。after は、before の path にある部分項だけを書き換えたものである。

戦略同士を照合する

β のように合流性を持つ規則では、どちらも正規形に到達する二つの戦略は α同値を除いて一致する。これは安価な回帰テストになる。

test "strategies agree when both terminate" {
  let x = nm("x")
  let y = nm("y")
  let term : @syntax.Term[Int] = Apply(Bind(x, Apply(Variable(x), [Variable(x)])), [
    Bind(y, Variable(y)),
  ])
  match
    (
      @eval.evaluate(term, beta_name(), @lambda.beta_rule, NormalOrder, 20),
      @eval.evaluate(term, beta_name(), @lambda.beta_rule, ApplicativeOrder, 20),
    ) {
    (NormalForm(term=a, ..), NormalForm(term=b, ..)) =>
      assert_true(@syntax.alpha_equal(a, b))
    _ => fail("both strategies terminate here")
  }
}

よくある落とし穴

• WeakHead の NormalForm を完全な正規形と読む。 それは弱頭部正規形を意味するにすぎない。
• FullNormal が NormalOrder と異なると期待する。 現時点では両者は同じ走査を使っている。
• 結果を == で比較する。 β簡約は束縛子の名前を付け替える（y_1）。@syntax.alpha_equal で比較すること。
• ステップ上限が小さすぎる。 StepLimitReached は発散を意味しない。上限を上げるか、高速な型なしの正規化には utlc/nbe を使うこと。

次のステップ

• eval API：正確なシグネチャ。
• eval の設計：戦略の定義と、その背後にある古典的な定理。
• utlc/lambda チュートリアル：これらの戦略の上に構築されたラムダ計算。