Luna Flow
日本語

rewrite チュートリアル

このチュートリアルでは、算術項の簡約化規則を書き、それを 1 ステップずつ適用し、ステップ上限のもとで正規形まで実行し、トレースを読んでどの規則がどこで発火したかを確認する。項は演算子を値とする Term[String] であり、x⋅1x \cdot 1 は Apply(Value("*"), [Variable(x), Value("1")]) である。

クイックスタート

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",
}

規則とは、項をその根で書き換えるか None を返す関数である。規則 t⋅1→tt \cdot 1 \to t は (x⋅1)⋅1(x \cdot 1) \cdot 1 を 2 ステップで簡約化する。

fn times_one(t : @syntax.Term[String]) -> @syntax.Term[String]? {
  match t {
    Apply(Value("*"), [other, Value("1")]) => Some(other)
    _ => None
  }
}

test "quick start: x * 1 * 1" {
  let x = @syntax.Term::Variable(@core.Name::new("x"))
  let term : @syntax.Term[String] = Apply(Value("*"), [
    Apply(Value("*"), [x, Value("1")]),
    Value("1"),
  ])
  let rule = @rewrite.RuleName::unsafe_new("times_one")
  let step = (t : @syntax.Term[String]) => @rewrite.top_down_once(t, rule, times_one)
  assert_eq(@rewrite.normalize(term, step, 10), NormalForm(term=x, steps=2))
}

日常的な作業

これらの例では、いくつかの補助関数と二つ目の規則 0+t→t0 + t \to t を共有する。

fn op(name : String, a : @syntax.Term[String], b : @syntax.Term[String]) -> @syntax.Term[String] {
  @syntax.Apply(@syntax.Value(name), [a, b])
}

fn lit(text : String) -> @syntax.Term[String] {
  @syntax.Value(text)
}

fn var_(text : String) -> @syntax.Term[String] {
  @syntax.Term::Variable(@core.Name::new(text))
}

fn zero_plus(t : @syntax.Term[String]) -> @syntax.Term[String]? {
  match t {
    Apply(Value("+"), [Value("0"), other]) => Some(other)
    _ => None
  }
}

1 ステップ実行し、どこで起きたかを見る

top_down_once は最外最左のマッチを書き換え、そこへのパスを報告する。

test "one step with its position" {
  let term = op("*", lit("2"), op("+", lit("0"), var_("y")))
  let rule = @rewrite.RuleName::unsafe_new("zero_plus")
  match @rewrite.top_down_once(term, rule, zero_plus) {
    Reduced(after~, path~, rule=used, ..) => {
      assert_eq(after, op("*", lit("2"), var_("y")))
      assert_eq(path.to_array(), [@rewrite.ApplyArgument(1)])
      inspect(used.value(), content="zero_plus")
    }
    NoStep => fail("expected a step")
  }
}

ApplyArgument(1) は根の * の第 2 引数である。

ステップ上限付きで正規化する

ステップ上限は止まらない規則から身を守る。どちらの結果が得られたかを確認すること。

test "normal form or limit" {
  let term = op("+", lit("0"), op("+", lit("0"), var_("z")))
  let rule = @rewrite.RuleName::unsafe_new("zero_plus")
  let step = (t : @syntax.Term[String]) => @rewrite.top_down_once(t, rule, zero_plus)
  match @rewrite.normalize(term, step, 1) {
    StepLimitReached(term~, steps~) => {
      assert_eq(steps, 1)
      assert_eq(term, op("+", lit("0"), var_("z")))
    }
    NormalForm(..) => fail("one step is not enough")
  }
  assert_eq(@rewrite.normalize(term, step, 5), NormalForm(term=var_("z"), steps=2))
}

トレースを読む

trace はすべてのステップを保持するので、簡約化の過程を説明できる。

test "explain a simplification" {
  let term = op("+", lit("0"), op("+", lit("0"), var_("z")))
  let rule = @rewrite.RuleName::unsafe_new("zero_plus")
  let step = (t : @syntax.Term[String]) => @rewrite.top_down_once(t, rule, zero_plus)
  let run = @rewrite.trace(term, step, 10)
  let lines = run
    .steps()
    .map(s => match s {
      Reduced(rule~, path~, ..) => "\{rule.value()} at depth \{path.to_array().length()}"
      NoStep => "none"
    })
  inspect(lines.join("; "), content="zero_plus at depth 0; zero_plus at depth 0")
}

最外か最内かを選ぶ

簡約基が入れ子になっているとき、top_down_once は外側を、bottom_up_once は内側を選ぶ。合流性を持つ規則集合では両者は同じ正規形に到達するが、ステップは異なる。

test "outermost and innermost first steps" {
  let inner = op("+", lit("0"), var_("z"))
  let term = op("+", lit("0"), inner)
  let rule = @rewrite.RuleName::unsafe_new("zero_plus")
  match @rewrite.top_down_once(term, rule, zero_plus) {
    Reduced(path~, ..) => assert_eq(path.to_array().length(), 0)
    NoStep => fail("expected a step")
  }
  match @rewrite.bottom_up_once(term, rule, zero_plus) {
    Reduced(path~, ..) => assert_eq(path.to_array(), [@rewrite.ApplyArgument(1)])
    NoStep => fail("expected a step")
  }
}

複数の規則を組み合わせる

規則を順に試すことで一つにまとめる。まとめた規則は一つの名前を持つので、そのことが分かる名前を付けること。

fn simplify(t : @syntax.Term[String]) -> @syntax.Term[String]? {
  match zero_plus(t) {
    Some(u) => Some(u)
    None => times_one(t)
  }
}

test "two rules, one normal form" {
  let term = op("+", lit("0"), op("*", var_("a"), lit("1")))
  let rule = @rewrite.RuleName::unsafe_new("simplify")
  let step = (t : @syntax.Term[String]) => @rewrite.top_down_once(t, rule, simplify)
  assert_eq(@rewrite.normalize(term, step, 10), NormalForm(term=var_("a"), steps=2))
}

どの規則が発火したかを知る必要がある場合は、規則ごとに top_down_once を一度ずつ（それぞれ固有の名前で）呼び出し、最初の Reduced を返すステップ関数を書く。この方法では、外側の位置にある二つ目の規則よりも、項のどこかにある一つ目の規則が優先される。

さらに進んで

束縛子の下の規則

走査は束縛子の本体に入るので、規則は開いた項を見ることになる。上の二つのように項の形だけを見る規則は、どこで使っても問題ない。束縛子をまたいで部分項を移動・複製する規則は、通常は代入を使って、束縛を自分で扱わなければならない。@lambda の β 規則が標準的な例である。

独自の AST を書き換える

generic_top_down_once と generic_normalize は @syntax.BindingSyntax を実装する任意の AST を受け付ける。規則は独自の型に対して書けばよい。完全な例は adapter チュートリアルにある。

戦略

eval はこれらの走査を名前付きの戦略（正規順序、適用順序、弱頭部）としてまとめ、1 つの evaluate 関数の背後に置く。

よくある落とし穴

  • 進展しない規則。 自身の入力 tt に対して Some(t) を返す規則や、別の規則を打ち消す規則は、正規化器をステップ数の上限まで空回りさせる。StepLimitReached を確認すること。
  • 合流しない規則。 2 つの規則が重なり合っていて合流しない場合、戦略によって異なる正規形が得られることがある。トレースを使って重なりを見つけること。
  • 入力に対する unsafe_new。 RuleName::unsafe_new("") はプログラムを中断する。リテラルでない名前には RuleName::new を使うこと。
  • 曖昧な構築子。 期待される型がない場合、@syntax.Variable(x) は曖昧である。@syntax.Term::Variable(x) と書くこと。

次のステップ