debruijn API

debruijn パッケージは束縛変数を De Bruijn インデックスで表す：Bound(i) は i 段上の束縛子を指す。名前付き構文との相互変換、スコープの検査、インデックスのシフトと代入を行い、リネームを一切伴わない最左最外 β簡約を実装する。自由変数は名前のまま保たれる。

import {
  "Luna-Flow/type_theory/core",
  "Luna-Flow/type_theory/syntax",
  "Luna-Flow/type_theory/rewrite",
  "Luna-Flow/type_theory/debruijn",
}

シフトとインスタンス化の定義、およびその性質の導出は debruijn の設計にある。

項とエラー

DbTerm

DbTerm[T] は名前のない束縛子を持つλ構文である。

pub(all) enum DbTerm[T] {
  Value(T)
  Free(@core.Name)
  Bound(Int)
  Apply(DbTerm[T], Array[DbTerm[T]])
  Bind(DbTerm[T])
} derive(Eq, @debug.Debug)

• Value(v) はドメイン定数であり、@syntax.Term と同様に不透明である。
• Free(x) は自由変数であり、名前で保持される。
• Bound(i) は i 番目の外側の Bind を指し、最も内側を 0 として数える。
• Apply(head, args) は n 項適用であり、カリー化されたスパインとして読む。
• Bind(body) は束縛子であり、その変数は body の中で Bound(0) である。

すべての Bound(i) が i 個より多くの束縛子の下にあるとき、項はスコープが正しいという。束縛子は名前を持たないので、スコープが正しい項に対する ==（DbTerm::equal）は α同値である。

DbTerm::equal

DbTerm::equal は 2 つの項を構造的に比較する。

pub fn[T : Eq] DbTerm::equal(Self[T], Self[T]) -> Bool

ScopeError

ScopeError は束縛子を指さないインデックスを表す。

pub(all) enum ScopeError {
  UnboundIndex(index~ : Int, depth~ : Int)
  NegativeIndex(index~ : Int)
  NegativeShift(index~ : Int, delta~ : Int, cutoff~ : Int)
} derive(Eq, @debug.Debug)
pub fn ScopeError::equal(Self, Self) -> Bool

• UnboundIndex(index, depth)：Bound(index) が depth 個の束縛子の下にしか出現しない。
• NegativeIndex(index)：負のインデックス。
• NegativeShift(index, delta, cutoff)：Bound(index) を delta だけシフトすると負になる。cutoff はその出現位置での実効カットオフである。

変換と検証

from_named

from_named は名前付き構文を De Bruijn 構文に変換する。

pub fn[T] from_named(@syntax.Term[T]) -> DbTerm[T]

外側の Bind によって束縛された変数は Bound(i) になる。ここで i は出現とその束縛子の間にある束縛子の数である（同名の場合は最も近い束縛子が優先される）。自由変数は Free になる。結果は常にスコープが正しく、α同値な名前付き項からは等しい結果が得られる。

to_named

to_named は De Bruijn 構文を、決定的な束縛子名を用いて名前付き構文に戻す。

pub fn[T] to_named(DbTerm[T]) -> Result[@syntax.Term[T], ScopeError]

束縛子には x、x_1、x_2、… と名前が付けられる：各束縛子には、この列のうち項の自由な名前でも外側の束縛子の名前でもない最初の名前が割り当てられる。スコープが正しくない項に対しては Err(NegativeIndex) または Err(UnboundIndex) を返す。スコープが正しい d について from_named(to_named(d)) は d であり、名前付きの t について to_named(from_named(t)) は t と α同値である。

test "named and nameless round trip" {
  let x = @core.Name::new("x")
  let y = @core.Name::new("y")
  let named : @syntax.Term[Int] = Bind(y, Apply(Variable(y), [Variable(x)]))
  let db = @debruijn.from_named(named)
  assert_eq(db, Bind(Apply(Bound(0), [Free(x)])))
  match @debruijn.to_named(db) {
    Ok(back) => {
      assert_true(@syntax.alpha_equal(back, named))
      assert_true(back is Bind(binder, _) && binder.text() == "x_1")
    }
    Err(_) => fail("well scoped")
  }
}

x は項の自由な名前なので、束縛子は x_1 になる。

validate

validate はすべての束縛インデックスが外側の束縛子を指していることを検査する。

pub fn[T] validate(DbTerm[T]) -> Result[Unit, ScopeError]

スコープが正しい項に対しては Ok(()) を返し、そうでなければ前順で最初に見つかったエラーを返す。

test "dangling index" {
  let bad : @debruijn.DbTerm[Int] = Bind(Bound(1))
  assert_eq(@debruijn.validate(bad), Err(UnboundIndex(index=1, depth=1)))
  let good : @debruijn.DbTerm[Int] = Bind(Bound(0))
  assert_eq(@debruijn.validate(good), Ok(()))
}

インデックス操作

shift

shift はカットオフに関して自由なすべてのインデックスに delta を加える。

pub fn[T] shift(DbTerm[T], Int, Int) -> Result[DbTerm[T], ScopeError]

shift(t, delta, cutoff) は操作 $\uparrow^{delta}_{cutoff}$ である：k 個の束縛子の下で、インデックス i >= cutoff + k は i + delta になり、それより小さいインデックスはそのままである。インデックスが負になる場合は Err(NegativeShift) を、入力に負のインデックスが含まれる場合は Err(NegativeIndex) を返す。

substitute_bound

substitute_bound は自由なインデックスを項で置き換える。

pub fn[T] substitute_bound(DbTerm[T], Int, DbTerm[T]) -> Result[DbTerm[T], ScopeError]

substitute_bound(t, j, s) は $[j \mapsto s]\,t$ である：k 個の束縛子の下で、Bound(j + k) は k だけ上にシフトした s で置き換えられ、s の自由なインデックスが同じ束縛子を指し続けるようにする。他のインデックスは変わらず、結果の束縛子の数は調整されない。負の j や t 内の負のインデックスに対しては Err(NegativeIndex) を返す。未束縛のインデックスは検査しないので、それには validate を使うこと。

instantiate

instantiate は束縛子の本体を引数で開く。

pub fn[T] instantiate(DbTerm[T], DbTerm[T]) -> Result[DbTerm[T], ScopeError]

instantiate(body, arg) は $\uparrow^{-1}_0\big([0 \mapsto \uparrow^{1}_0 arg]\,body\big)$、すなわち β ステップ $(\lambda.\,body)\,arg$ の結果を計算する。スコープが正しい入力に対してはエラーを返さない。

test "instantiate a binder body" {
  let y = @core.Name::new("y")
  // body of λ. λ. 1 0, i.e. λ. (outer variable) applied to (inner variable)
  let body : @debruijn.DbTerm[Int] = Bind(Apply(Bound(1), [Bound(0)]))
  assert_eq(
    @debruijn.instantiate(body, Free(y)),
    Ok(Bind(Apply(Free(y), [Bound(0)]))),
  )
  let open_term : @debruijn.DbTerm[Int] = Bind(Apply(Bound(0), [Bound(1)]))
  assert_eq(
    @debruijn.shift(open_term, 2, 0),
    Ok(Bind(Apply(Bound(0), [Bound(3)]))),
  )
  let under_binder : @debruijn.DbTerm[Int] = Bind(Bound(1))
  assert_eq(
    @debruijn.substitute_bound(under_binder, 0, Bound(5)),
    Ok(Bind(Bound(6))),
  )
}

簡約

DbStepResult

DbStepResult[T] は De Bruijn 簡約を 1 回試みた結果である。

pub(all) enum DbStepResult[T] {
  NoStep
  Reduced(before~ : DbTerm[T], after~ : DbTerm[T], rule~ : @rewrite.RuleName, path~ : @rewrite.ReductionPath)
  ScopeFailure(ScopeError)
} derive(Eq, @debug.Debug)
pub fn[T : Eq] DbStepResult::equal(Self[T], Self[T]) -> Bool

NoStep と Reduced の意味は @rewrite.StepResult と同じであり、規則名は常に "beta" である。ScopeFailure は簡約基を縮約する際に遭遇したインデックスエラーを報告する。

reduce_once

reduce_once は最左最外の β ステップを 1 回行う。

pub fn[T] reduce_once(DbTerm[T]) -> DbStepResult[T]

簡約基は Apply(Bind(body), [a, ..rest]) であり、instantiate(body, a) になる。rest が空でなければそれを rest に適用する。探索順序は根、次に先頭、次に引数を左から右へであり、束縛子の本体にも入る。reduce_once は入力を検証しないので、項のスコープが正しくない可能性がある場合は先に validate を呼ぶこと。

DbNormalizationResult

DbNormalizationResult[T] は上限付き De Bruijn 正規化の結果である。

pub(all) enum DbNormalizationResult[T] {
  NormalForm(term~ : DbTerm[T], steps~ : Int)
  StepLimitReached(term~ : DbTerm[T], steps~ : Int)
  ScopeFailure(term~ : DbTerm[T], error~ : ScopeError, steps~ : Int)
} derive(Eq, @debug.Debug)
pub fn[T : Eq] DbNormalizationResult::equal(Self[T], Self[T]) -> Bool

ScopeFailure は失敗したステップが試みられた項と、それ以前に行われたステップ数を保持する。

normalize

normalize は、適用できるステップがなくなるか、ステップが失敗するか、ステップ数の上限に達するまで reduce_once を繰り返す。

pub fn[T] normalize(DbTerm[T], Int) -> DbNormalizationResult[T]

@rewrite.normalize と同じステップ数の契約を持つ：高々 max_steps ステップであり、最終項を分類するために reduce_once を 1 回余分に呼ぶ。

test "nameless beta reduction" {
  let f = @core.Name::new("f")
  // λ. f ((λ. 0) 7)
  let term : @debruijn.DbTerm[Int] = Bind(
    Apply(Free(f), [Apply(Bind(Bound(0)), [Value(7)])]),
  )
  match @debruijn.reduce_once(term) {
    Reduced(after~, path~, rule~, ..) => {
      assert_eq(after, Bind(Apply(Free(f), [Value(7)])))
      assert_eq(path.to_array(), [@rewrite.BinderBody, @rewrite.ApplyArgument(0)])
      inspect(rule.value(), content="beta")
    }
    _ => fail("expected a beta step")
  }
  assert_eq(
    @debruijn.normalize(term, 10),
    NormalForm(term=Bind(Apply(Free(f), [Value(7)])), steps=1),
  )
}