Luna Flow
日本語

debruijn チュートリアル

このチュートリアルでは、名前付きラムダ項を de Bruijn 形式に変換し、その形式を使って項を比較したり名前の付け替えなしに簡約したりし、信頼できない名前なしの入力を検証し、表示のために結果を名前付きの形に戻す。

クイックスタート

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

λx. λy. x\lambda x.\,\lambda y.\,x は λ. λ. 1\lambda.\,\lambda.\,1 になる。この変数は一段外側の束縛子を指している。

test "quick start: the K combinator without names" {
  let x = @core.Name::new("x")
  let y = @core.Name::new("y")
  let k : @syntax.Term[Int] = Bind(x, Bind(y, Variable(x)))
  assert_eq(@debruijn.from_named(k), Bind(Bind(Bound(1))))
}

日常的な作業

束縛された名前を除いて項を比較する

α同値な名前付き項は同じ de Bruijn 形式を持つので、変換後の == で α同値性を判定できる。

test "alpha-equivalence by conversion" {
  let a : @syntax.Term[Int] = Bind(@core.Name::new("p"), Variable(@core.Name::new("p")))
  let b : @syntax.Term[Int] = Bind(@core.Name::new("q"), Variable(@core.Name::new("q")))
  assert_eq(@debruijn.from_named(a), @debruijn.from_named(b))
}

@syntax.alpha_equal は変換後の項を構築せずに同じ答えを返す。変換が割に合うのは、名前なしの形式をさらなる処理のために保持する場合である。

名前の付け替えなしに簡約する

名前なしの項に対する β簡約は、束縛子の名前を付け替える代わりにインデックスをシフトする。古典的な捕獲の例 (λx. λy. x) y(\lambda x.\,\lambda y.\,x)\,y でも新しい名前は不要である。

test "beta without capture problems" {
  let y = @core.Name::new("y")
  let term : @debruijn.DbTerm[Int] = Apply(Bind(Bind(Bound(1))), [Free(y)])
  assert_eq(
    @debruijn.normalize(term, 10),
    NormalForm(term=Bind(Free(y)), steps=1),
  )
}

自由な y は名前なので自由なまま保たれ、内側の束縛子はそもそも名前を持たないので新しい名前は不要である。

信頼できない入力を検証する

手で構築した項や外部から読み込んだ項には、どの束縛子も越えた先を指すインデックスが含まれていることがある。簡約の前に検査すること。

test "reject a dangling index" {
  let bad : @debruijn.DbTerm[Int] = Bind(Apply(Bound(0), [Bound(2)]))
  match @debruijn.validate(bad) {
    Err(UnboundIndex(index~, depth~)) => {
      assert_eq(index, 2)
      assert_eq(depth, 1)
    }
    _ => fail("expected an unbound index")
  }
}

表示のために名前付きの形に戻す

to_named は束縛子に x、x_1、… と名前を付け、項の自由な名前を避ける。

test "readable names come back" {
  let x = @core.Name::new("x")
  let term : @debruijn.DbTerm[Int] = Bind(Bind(Apply(Bound(1), [Free(x)])))
  match @debruijn.to_named(term) {
    Ok(Bind(outer, Bind(inner, _))) => {
      inspect(outer.text(), content="x_1")
      inspect(inner.text(), content="x_2")
    }
    _ => fail("well scoped")
  }
}

x は項の中で自由なので、束縛子は x を飛ばしている。

束縛子を手で開く

instantiate(body, arg) は (λ. body) arg(\lambda.\,body)\,arg の結果である。独自の簡約器や評価器を実装するときに使う。

test "open a binder" {
  // body of λ. (λ. 1 0): the outer variable applied to the inner one
  let body : @debruijn.DbTerm[Int] = Bind(Apply(Bound(1), [Bound(0)]))
  assert_eq(
    @debruijn.instantiate(body, Value(9)),
    Ok(Bind(Apply(Value(9), [Bound(0)]))),
  )
}

さらに進んで

名前付きの簡約器を名前なしの簡約器と照合する

変換は β簡約と可換なので、名前付きと名前なしの簡約器は α同値を除いて一致しなければならない。これは自分で書いたどの簡約器に対しても良いプロパティテストになる。

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

test "named and nameless beta agree" {
  let x = @core.Name::new("x")
  let y = @core.Name::new("y")
  let named : @syntax.Term[Int] = Apply(Bind(x, Bind(y, Apply(Variable(x), [Variable(y)]))), [
    Variable(y),
  ])
  match (named_beta(named), @debruijn.reduce_once(@debruijn.from_named(named))) {
    (Some(n), Reduced(after~, ..)) => assert_eq(@debruijn.from_named(n), after)
    _ => fail("both reduce")
  }
}

（この例では Luna-Flow/type_theory/substitution もインポートしている。）

高速な正規化

normalize は根から「探索して縮約する」ステップを一つずつ繰り返す。これは単純で追跡しやすいが、長い簡約では遅い。大きな型なしの項には utlc/nbe を使うこと。これは同じ DbTerm 上で動作し、（適用スパインの形を除いて）同じ正規形を返す。

よくある落とし穴

  • インデックスを外側から数える。 Bound(0) は最も内側の束縛子である。λx. λy. x\lambda x.\,\lambda y.\,x は Bind(Bind(Bound(1))) であり、Bound(0) ではない。
  • 検証していない項を簡約する。 reduce_once と substitute_bound は束縛されていないインデックスを検出しない。from_named で構築したのではない入力には、まず validate を呼ぶこと。
  • 束縛子の名前が保たれると期待する。 to_named(from_named(t)) は t と α同値だが、束縛子の名前は生成し直される。
  • スパイン。 Apply(f, [a, b]) と Apply(Apply(f, [a]), [b]) は同じ適用を意味するが、異なる値である。== で比較する前に一つの形に揃えること。

次のステップ