Luna Flow
日本語

substitution チュートリアル

このチュートリアルでは変数を項で置き換える。テンプレートの具体化、変数の交換、何も捕獲せずに束縛子の下で代入すること、代入の合成、部分評価を扱う。例では算術を Term[String] としてエンコードし、演算子を値として表す。x+1x + 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/substitution",
}

x+1x + 1 の xx に 22 を代入する。

test "quick start: x + 1 with x := 2" {
  let x = @core.Name::new("x")
  let term : @syntax.Term[String] = Apply(Value("+"), [Variable(x), Value("1")])
  let s = @substitution.Substitution::singleton(x, @syntax.Value("2"))
  assert_eq(s.apply(term), Apply(Value("+"), [Value("2"), Value("1")]))
}

日常的な作業

以下の例は 2 つのヘルパーを共有する。

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

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

2 つの変数を交換する

代入のすべてのエントリは同時に適用されるので、交換に一時変数は要らない。

test "swap x and y" {
  let x = name("x")
  let y = name("y")
  let swap = @substitution.Substitution::singleton(x, @syntax.Term::Variable(y))
    .set(y, @syntax.Term::Variable(x))
  assert_eq(swap.apply(plus(Variable(x), Variable(y))), plus(Variable(y), Variable(x)))
}

束縛子の下で代入する

λy. x+y\lambda y.\, x + y の xx に yy を代入するとき、挿入した yy が束縛されたものになってはならない。束縛子は y_1 にリネームされる。

test "no capture under a binder" {
  let x = name("x")
  let y = name("y")
  let term : @syntax.Term[String] = Bind(y, plus(Variable(x), Variable(y)))
  let result = @substitution.Substitution::singleton(x, @syntax.Term::Variable(y))
    .apply(term)
  let y1 = name("y_1")
  let expected : @syntax.Term[String] = Bind(y1, plus(Variable(y), Variable(y1)))
  assert_eq(result, expected)
}

代入される変数自身の束縛子はそれを隠すので、内部では何も起こらない。

test "a binder shadows the substituted variable" {
  let x = name("x")
  let term : @syntax.Term[String] = Bind(x, Variable(x))
  let s = @substitution.Substitution::singleton(x, @syntax.Value("0"))
  assert_eq(s.apply(term), term)
}

部分評価する

分かっている変数だけを代入し、それ以外はそのまま残す。

test "partial evaluation" {
  let x = name("x")
  let y = name("y")
  let known = @substitution.Substitution::singleton(x, @syntax.Value("3"))
  let result = known.apply(plus(Variable(x), Variable(y)))
  assert_eq(result, plus(Value("3"), Variable(y)))
  assert_true(@syntax.free_variables(result).contains(y))
}

代入を合成する

first.then(second) は first を行ってから second を行う 1 つの代入である。1 回の走査で適用される。

test "compose two steps into one" {
  let x = name("x")
  let y = name("y")
  let first = @substitution.Substitution::singleton(x, plus(Variable(y), Value("1")))
  let second = @substitution.Substitution::singleton(y, @syntax.Value("5"))
  let both = first.then(second)
  let term = plus(Variable(x), Variable(y))
  assert_eq(both.apply(term), plus(plus(Value("5"), Value("1")), Value("5")))
  assert_true(@syntax.alpha_equal(both.apply(term), second.apply(first.apply(term))))
}

さらに進んで

beta 簡約を実装する

beta 簡約 (λx. b) a→b[x:=a](\lambda x.\,b)\,a \to b[x := a] は 1 回の代入である。@lambda.beta_rule はこのように動作する。

fn beta(t : @syntax.Term[String]) -> @syntax.Term[String]? {
  match t {
    Apply(Bind(x, body), [arg]) =>
      Some(@substitution.Substitution::singleton(x, arg).apply(body))
    _ => None
  }
}

test "beta via substitution" {
  let x = name("x")
  let y = name("y")
  let k : @syntax.Term[String] = Bind(x, Bind(y, Variable(x)))
  let result = beta(Apply(k, [Variable(y)]))
  let expected : @syntax.Term[String] = Bind(name("y_1"), Variable(y))
  assert_eq(result, Some(expected))
}

不動点まで自分で反復する

代入は 1 回だけ適用される。置き換える項が定義域の変数に言及しうる場合に、それらも置き換えたいなら、上限を設けて繰り返し適用する。この過程は停止するとは限らないからである（x:=x+1x := x + 1 を考えよ）。

fn apply_until_stable(
  s : @substitution.Substitution[String],
  t : @syntax.Term[String],
  limit : Int,
) -> @syntax.Term[String] {
  let mut current = t
  for _ in 0..<limit {
    let next = s.apply(current)
    if next == current {
      break
    }
    current = next
  }
  current
}

test "resolve a chain of definitions" {
  let x = name("x")
  let y = name("y")
  let defs = @substitution.Substitution::singleton(x, @syntax.Term::Variable(y))
    .set(y, @syntax.Value("7"))
  assert_eq(apply_until_stable(defs, Variable(x), 10), Value("7"))
}

独自の AST で代入する

GenericSubstitution は @syntax.BindingSyntax を実装する任意の AST 上で同じアルゴリズムを実行する。adapter チュートリアルではそのような AST を定義し、apply_once で代入する。

よくある落とし穴

  • 曖昧な構築子。 期待される型がないと @syntax.Variable(y) は曖昧である。BindingView にも Variable ケースがあるからである。@syntax.Term::Variable(y) と書くか、期待される型を注釈すること。
  • 繰り返しの代入を期待する。 xx に {x↦y, y↦7}\{x \mapsto y,\ y \mapsto 7\} を適用すると、77 ではなく yy になる。then を使うか、明示的に反復すること。
  • == による比較。 結果にはリネームされた束縛子（y_1）が含まれうる。正確な名前が分かっているのでなければ @syntax.alpha_equal で比較すること。
  • 値の内部の変数。 Value のペイロードの中には代入されない。

次のステップ