syntax API

syntax 包定义了带绑定子的命名语法：泛型项类型 Term[T]、其上的分析（自由变量、全部名字、α-等价）、重命名，以及开放 trait BindingSyntax——下游 AST 借助它获得同样的分析，以及其他包中的泛型代换与改写。

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

这些函数背后的定义及其定律的证明见语法设计。

项

`Term`

Term[T] 是命名语法，包含领域值、变量、n 元应用和单变量绑定。

pub(all) enum Term[T] {
  Value(T)
  Variable(@core.Name)
  Apply(Term[T], Array[Term[T]])
  Bind(@core.Name, Term[T])
} derive(Eq, @debug.Debug)

Value(v) 是领域常量。其载荷 T 是不透明的：它被视为闭合的，因此任何分析都不会查看其内部。
Variable(x) 是名字 x 的一次出现。
Apply(head, args) 将 head 应用于一串参数。lambda 演算相关的包将其解读为柯里化应用 $head\ a_1\ \cdots\ a_n$ 。
Bind(x, body) 在 body 中绑定 x。在 lambda 演算中它是 $\lambda x.\,body$ ；下游语言可以将其解读为任意单变量绑定子。

==（Term::equal）是结构相等：绑定子名字必须字面一致。若要在约束变量重命名的意义下比较项，请使用 alpha_equal。

test "build the term λx. f x 1" {
  let x = @core.Name::new("x")
  let f = @core.Name::new("f")
  let term : @syntax.Term[Int] = Bind(
    x,
    Apply(Variable(f), [Variable(x), Value(1)]),
  )
  assert_true(term is Bind(_, Apply(_, [_, Value(1)])))
}

`Term::equal`

Term::equal 按结构比较两个项。

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

它是提升而来的 Eq 实现。λx.x 与 λy.y 并不 equal。

`Term::map_values`

Term::map_values 对每个领域值应用一个函数，并保留变量和绑定子。

pub fn[T, U] Term::map_values(Self[T], (T) -> U) -> Self[U]

它是函子映射：t.map_values(v => v) 就是 t，先映射 f 再映射 g 等于映射 v => g(f(v))。自由变量保持不变。

test "map domain values" {
  let x = @core.Name::new("x")
  let term : @syntax.Term[Int] = Apply(Value(2), [Variable(x), Value(3)])
  let shown = term.map_values(v => v.to_string())
  assert_eq(shown, Apply(Value("2"), [Variable(x), Value("3")]))
}

分析

`free_variables`

free_variables 返回在项中自由出现的名字。

pub fn[T] free_variables(Term[T]) -> @hashset.HashSet[@core.Name]

当没有外层的 Bind(x, _) 绑定 x 的某次出现时，该出现是自由的。值不贡献任何名字。代价：对大小为 $n$ 的项需要 $O(n)$ 次集合运算。

`all_names`

all_names 返回项中的每个名字：自由变量、约束出现和绑定子名字。

pub fn[T] all_names(Term[T]) -> @hashset.HashSet[@core.Name]

为项选取新鲜名字时，可将其用作“已使用”集合。

test "free and all names" {
  let x = @core.Name::new("x")
  let y = @core.Name::new("y")
  let z = @core.Name::new("z")
  let term : @syntax.Term[Int] = Bind(x, Apply(Variable(x), [Variable(z)]))
  let fv = @syntax.free_variables(term)
  assert_true(fv.contains(z))
  assert_false(fv.contains(x))
  assert_true(@syntax.all_names(term).contains(x))
  assert_false(@syntax.all_names(term).contains(y))
}

`alpha_equal`

alpha_equal 判定两个项在约束变量名字的意义下是否相等。

pub fn[T : Eq] alpha_equal(Term[T], Term[T]) -> Bool

值用 == 比较，自由变量按名字比较，约束变量按其所指的绑定子比较。该关系是等价关系，并通过对两个项的一趟同时遍历来判定。

test "alpha-equivalence ignores binder names" {
  let x = @core.Name::new("x")
  let y = @core.Name::new("y")
  let z = @core.Name::new("z")
  let left : @syntax.Term[Int] = Bind(x, Apply(Variable(x), [Variable(z)]))
  let right : @syntax.Term[Int] = Bind(y, Apply(Variable(y), [Variable(z)]))
  assert_true(@syntax.alpha_equal(left, right))
  assert_false(left == right)
  let other : @syntax.Term[Int] = Bind(y, Apply(Variable(y), [Variable(y)]))
  assert_false(@syntax.alpha_equal(left, other))
}

重命名

`Term::rename_free`

Term::rename_free 对项的自由变量应用重命名，并在必要时重命名绑定子以避免捕获。

pub fn[T] Term::rename_free(Self[T], @core.Renaming) -> Self[T]

在 Bind(x, body) 之下，重命名会失去 x 的条目，因为被绑定的 x 是另一个变量。如果重命名剩余的某个目标等于 x，会先将绑定子重命名为新鲜名字。结果与教科书中避免捕获的重命名 α-等价。

test "rename a free variable without capture" {
  let x = @core.Name::new("x")
  let y = @core.Name::new("y")
  let term : @syntax.Term[Int] = Bind(y, Variable(x))
  let renamed = term.rename_free(@core.Renaming::singleton(x, y))
  let expected : @syntax.Term[Int] = Bind(@core.Name::new("y_1"), Variable(y))
  assert_eq(renamed, expected)
}

`Term::alpha_rename_bound`

Term::alpha_rename_bound 重命名被外层绑定子约束的某个变量的各次出现，并拒绝可能被捕获的目标名字。

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

请在绑定子的体上调用它：body.alpha_rename_bound(from, to_) 将 from 在 body 中自由（因而被外层 Bind(from, body) 约束）的出现替换为 to_。名为 from 的内层绑定子会阻止重命名。当 to_ 出现在 body 中任何位置时结果为 None，当 from == to_ 时结果为 Some(body)。成功时，Bind(from, body) 与 Bind(to_, result) α-等价。

test "checked bound renaming" {
  let x = @core.Name::new("x")
  let y = @core.Name::new("y")
  let z = @core.Name::new("z")
  let body : @syntax.Term[Int] = Bind(y, Variable(x))
  assert_true(body.alpha_rename_bound(x, y) is None)
  let expected : @syntax.Term[Int] = Bind(y, Variable(z))
  assert_eq(body.alpha_rename_bound(x, z), Some(expected))
}

感知绑定的 AST

`BindingView`

BindingView[N] 是泛型算法所检查的节点的单层视图。

pub(all) enum BindingView[N] {
  Opaque
  Variable(@core.Name)
  Apply(N, Array[N])
  Bind(@core.Name, N)
}

Opaque 标记内部不含变量的节点，例如字面量。其他情形与 Term 的构造器一一对应，子节点保留为下游类型 N。

`BindingSyntax`

BindingSyntax 是开放 trait，下游 AST 实现它即可使用泛型绑定算法。

pub(open) trait BindingSyntax {
  fn project(Self) -> BindingView[Self]
  fn variable(@core.Name) -> Self
  fn apply(Self, Array[Self]) -> Self
  fn bind(@core.Name, Self) -> Self
}

project(node) 告诉算法该节点是什么。
variable、apply 和 bind 分别重建各类节点。

实现必须使 project 与三个构造器保持一致：project(variable(x)) 为 Variable(x)，project(apply(h, args)) 为 Apply(h, args)，project(bind(x, b)) 为 Bind(x, b)，并且重建一个投影得到的 Apply 或 Bind 节点会得到等价的节点。Opaque 节点不得包含变量。适配器设计解释了这些定律；适配器教程为一个小型 AST 实现了它们。

请通过 trait 调用 trait 方法，例如 @syntax.BindingSyntax::project(node)。

`impl BindingSyntax for Term`

Term[T] 以显然的投影实现了 BindingSyntax。

pub impl[T] BindingSyntax for Term[T]

Value 投影为 Opaque，其他每个构造器投影为同名的情形，因此下面的泛型函数在 Term 值上与其 Term 版本一致。

test "project a term" {
  let x = @core.Name::new("x")
  let term : @syntax.Term[Int] = Bind(x, Variable(x))
  match @syntax.BindingSyntax::project(term) {
    Bind(name, _) => assert_eq(name, x)
    _ => fail("expected a binder")
  }
}

`generic_free_variables`, `generic_all_names`

以下函数为任意 BindingSyntax 类型计算自由变量和全部名字。

pub fn[N : BindingSyntax] generic_free_variables(N) -> @hashset.HashSet[@core.Name]
pub fn[N : BindingSyntax] generic_all_names(N) -> @hashset.HashSet[@core.Name]

在 Term[T] 上，它们返回与 free_variables 和 all_names 相同的集合。

`generic_alpha_rename_bound`

generic_alpha_rename_bound 是适用于任意 BindingSyntax 类型的 Term::alpha_rename_bound。

pub fn[N : BindingSyntax] generic_alpha_rename_bound(N, @core.Name, @core.Name) -> N?

当目标名字出现在节点中时，它返回 None；它通过 variable、apply 和 bind 重建重命名后的节点。

test "generic analyses on a term" {
  let x = @core.Name::new("x")
  let z = @core.Name::new("z")
  let term : @syntax.Term[Int] = Apply(Variable(x), [Bind(z, Variable(z))])
  assert_true(@syntax.generic_free_variables(term).contains(x))
  assert_false(@syntax.generic_free_variables(term).contains(z))
  let renamed = @syntax.generic_alpha_rename_bound(term, x, @core.Name::new("w"))
  assert_true(renamed is Some(Apply(Variable(_), [_])))
}

已弃用

已弃用	替代项
`term.project()`	`@syntax.BindingSyntax::project(term)`
`Term::variable(name)` 方法形式	`Term::Variable(name)`
`Term::apply(head, args)` 方法形式	`Term::Apply(head, args)`
`Term::bind(name, body)` 方法形式	`Term::Bind(name, body)`
`term.not_equal(other)`	`term != other`
`term.to_repr()`	`Repr(term)` 或 `@debug.to_string(term)`

这些方法形式原本是 trait 方法的隐式提升。保留它们（隐藏且已弃用）是为了让旧的调用者仍能编译。

syntax API

项

Term

Term::equal

Term::map_values

分析

free_variables

all_names

alpha_equal

重命名

Term::rename_free

Term::alpha_rename_bound