substitution API

substitution パッケージは、変数を捕獲することなく自由変数を項で置き換える。Substitution[T] は @syntax.Term[T] 上で動作し、GenericSubstitution[N] は @syntax.BindingSyntax を実装する任意の AST 上で動作する。どちらも有限・同時・不変である。

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

捕獲回避代入の定義とその法則の証明は代入の設計にある。

`Term` 上の代入

`Substitution`

Substitution[T] は名前から置換項への有限写像である。

pub struct Substitution[T] {
  entries : Array[(@core.Name, @syntax.Term[T])]
}

これは、項目 $(x, s)$ について $\sigma(x) = s$ 、それ以外のすべての名前について $\sigma(x) = x$ （変数そのもの）となる写像 $\sigma$ を表す。項目はパッケージ外からは読み取り専用であり、各名前につき項目は高々一つである。

`Substitution::empty`, `Substitution::singleton`, `Substitution::set`

以下の関数は代入を構築する。

pub fn[T] Substitution::empty() -> Self[T]
pub fn[T] Substitution::singleton(@core.Name, @syntax.Term[T]) -> Self[T]
pub fn[T] Substitution::set(Self[T], @core.Name, @syntax.Term[T]) -> Self[T]

set(x, s) は $x \mapsto s$ を追加する。x の項目が既にあればその場で置き換える。

`Substitution::get`

Substitution::get は名前に対する置換項があればそれを返す。

pub fn[T] Substitution::get(Self[T], @core.Name) -> @syntax.Term[T]?

`Substitution::without`, `Substitution::restrict`

以下のメソッドは代入の定義域を縮小する。

pub fn[T] Substitution::without(Self[T], @core.Name) -> Self[T]
pub fn[T] Substitution::restrict(Self[T], @hashset.HashSet[@core.Name]) -> Self[T]

without(x) は x の項目を取り除く。これは x の束縛子が行うことと同じである。restrict(names) は名前が names に含まれる項目だけを残す。

test "build and shrink substitutions" {
  let x = @core.Name::new("x")
  let y = @core.Name::new("y")
  let s : @substitution.Substitution[Int] = @substitution.Substitution::singleton(
    x,
    Value(1),
  ).set(y, Value(2))
  assert_eq(s.get(x), Some(@syntax.Value(1)))
  assert_eq(s.without(x).get(x), None)
  assert_eq(s.restrict(@hashset.HashSet([y])).get(x), None)
  assert_eq(s.restrict(@hashset.HashSet([y])).get(y), Some(@syntax.Value(2)))
}

`Substitution::apply`

Substitution::apply は項の自由変数を同時に置き換え、捕獲を避けるために束縛子の名前を変える。

pub fn[T] Substitution::apply(Self[T], @syntax.Term[T]) -> @syntax.Term[T]

定義域にある名前 x のすべての自由な出現は、その置換項で置き換えられる。挿入された置換項の内部では代入は行われない。Bind(y, body) の下では y の項目は無視される。実際に body に挿入される置換項が y を自由に含む場合は、まず束縛子を新しい名前に変えるので、置換項の自由変数は自由なまま保たれる。結果は新しい名前の選び方を除いて一意に定まり、その選び方自体も決定的である。

test "substitution avoids capture" {
  let x = @core.Name::new("x")
  let y = @core.Name::new("y")
  let term : @syntax.Term[Int] = Bind(y, Apply(Variable(x), [Variable(y)]))
  let result = @substitution.Substitution::singleton(x, Variable(y)).apply(term)
  let y1 = @core.Name::new("y_1")
  let expected : @syntax.Term[Int] = Bind(y1, Apply(Variable(y), [Variable(y1)]))
  assert_eq(result, expected)
}

`Substitution::then`

Substitution::then は二つの代入を合成し、self を先に適用する。

pub fn[T] Substitution::then(Self[T], Self[T]) -> Self[T]

s.then(t) は s の定義域の各 x を t.apply(s(x)) に写し、t の定義域のそれ以外の各 x を t(x) に写す。任意の項について、s.then(t).apply(term) は t.apply(s.apply(term)) と α同値である。

test "composition agrees with sequential application" {
  let x = @core.Name::new("x")
  let y = @core.Name::new("y")
  let first : @substitution.Substitution[Int] = @substitution.Substitution::singleton(
    x,
    Variable(y),
  )
  let second = @substitution.Substitution::singleton(y, Value(42))
  let term : @syntax.Term[Int] = Apply(Variable(x), [Variable(y)])
  let both = first.then(second)
  assert_true(
    @syntax.alpha_equal(both.apply(term), second.apply(first.apply(term))),
  )
  assert_eq(both.apply(term), Apply(Value(42), [Value(42)]))
}

`from_renaming`

from_renaming は名前の付け替えを、与えられた名前の集合上の代入に変換する。

pub fn[T] from_renaming(Array[@core.Name], @core.Renaming) -> Substitution[T]

結果は、列挙された名前 x のうち renaming.apply(x) != x となるものそれぞれを Variable(renaming.apply(x)) に写す。項の自由変数が列挙された名前に含まれるとき、結果を適用したものは term.rename_free(renaming) と α同値である。

test "a renaming as a substitution" {
  let x = @core.Name::new("x")
  let y = @core.Name::new("y")
  let s : @substitution.Substitution[Int] = @substitution.from_renaming(
    [x],
    @core.Renaming::singleton(x, y),
  )
  assert_eq(s.apply(Variable(x)), Variable(y))
}

束縛を扱う AST 上の代入

`GenericSubstitution`

GenericSubstitution[N] は名前から下流の AST N のノードへの有限写像である。

pub struct GenericSubstitution[N] {
  entries : Array[(@core.Name, N)]
}

`GenericSubstitution::empty`, `singleton`, `set`, `get`, `without`

以下の関数は汎用の代入を構築・照会する。その振る舞いは対応する Substitution 版とまったく同じである。

pub fn[N] GenericSubstitution::empty() -> Self[N]
pub fn[N] GenericSubstitution::singleton(@core.Name, N) -> Self[N]
pub fn[N] GenericSubstitution::set(Self[N], @core.Name, N) -> Self[N]
pub fn[N] GenericSubstitution::get(Self[N], @core.Name) -> N?
pub fn[N] GenericSubstitution::without(Self[N], @core.Name) -> Self[N]

`GenericSubstitution::apply_once`

GenericSubstitution::apply_once は、同時かつ捕獲回避の一回のパスで代入をノードに適用する。

pub fn[N : @syntax.BindingSyntax] GenericSubstitution::apply_once(Self[N], N) -> N

アルゴリズムは Substitution::apply と同じもので、BindingSyntax::project を通して実行され、variable、apply、bind で再構築される。Opaque ノードはそのまま返される。「Once」とは、挿入された置換項を再び訪問しないという意味である。 $x + y$ において $x \mapsto y$ と $y \mapsto 2$ を代入すると、 $2 + 2$ ではなく $y + 2$ になる。

test "generic substitution on Term" {
  let x = @core.Name::new("x")
  let y = @core.Name::new("y")
  let s = @substitution.GenericSubstitution::singleton(x, @syntax.Term::Variable(y))
    .set(y, @syntax.Value(2))
  let term : @syntax.Term[Int] = Apply(Variable(x), [Variable(y)])
  assert_eq(s.apply_once(term), Apply(Variable(y), [Value(2)]))
}

Term[T] 上では、apply_once は Substitution::apply と一致する。下流の AST についてはアダプタのチュートリアルを参照。

substitution API

Term 上の代入

Substitution

Substitution::empty, Substitution::singleton, Substitution::set

Substitution::get

Substitution::without, Substitution::restrict

Substitution::apply

Substitution::then

from_renaming