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])]
}

它表示映射 $\sigma$ ：对于条目 $(x, s)$ 有 $\sigma(x) = s$ ，对于其他所有名字有 $\sigma(x) = x$ （即变量本身）。这些条目在包外是只读的；每个名字至多有一个条目。

`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]

结果将每个满足 renaming.apply(x) != 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$ 得到 $y + 2$ ，而不是 $2 + 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