Luna Flow
简体中文

syntax 教程

本教程用 Term[T] 构建带绑定子的项、打印它们、询问哪些变量是自由的、在约束变量名不计的意义下比较项，并在不发生捕获的情况下重命名变量。最后你会编写一个适用于任何实现了 BindingSyntax 的 AST 的分析。

快速入门

moon add Luna-Flow/type_theory@0.2.0
import {
  "Luna-Flow/type_theory/core",
  "Luna-Flow/type_theory/syntax",
}

恒等函数 λx. x\lambda x.\,x 没有自由变量；λx. y\lambda x.\,y 有一个：

test "quick start: free variables" {
  let x = @core.Name::new("x")
  let y = @core.Name::new("y")
  let id : @syntax.Term[Int] = Bind(x, Variable(x))
  let k : @syntax.Term[Int] = Bind(x, Variable(y))
  assert_eq(@syntax.free_variables(id).length(), 0)
  assert_true(@syntax.free_variables(k).contains(y))
}

日常任务

用小型辅助函数构建项

到处写 @core.Name::new 会很啰嗦。一次性定义辅助函数：

fn v(name : String) -> @syntax.Term[Int] {
  @syntax.Variable(@core.Name::new(name))
}

fn lam(name : String, body : @syntax.Term[Int]) -> @syntax.Term[Int] {
  @syntax.Bind(@core.Name::new(name), body)
}

fn app(f : @syntax.Term[Int], args : Array[@syntax.Term[Int]]) -> @syntax.Term[Int] {
  @syntax.Apply(f, args)
}

test "the K combinator" {
  let k = lam("x", lam("y", v("x")))
  assert_true(k is Bind(_, Bind(_, Variable(_))))
  assert_eq(app(k, [v("a")]), @syntax.Apply(k, [v("a")]))
}

Term 没有自己的文本格式，因为合适的记法取决于它所编码的语言。lambda 记法的打印器是一个简短的递归函数：

fn show(t : @syntax.Term[Int]) -> String {
  match t {
    Value(n) => n.to_string()
    Variable(x) => x.text()
    Apply(f, args) => {
      let parts = [show(f), ..args.map(show)]
      "(" + parts.join(" ") + ")"
    }
    Bind(x, body) => "λ" + x.text() + ". " + show(body)
  }
}

test "print λf. f 1" {
  let f = @core.Name::new("f")
  let t : @syntax.Term[Int] = Bind(f, Apply(Variable(f), [Value(1)]))
  inspect(show(t), content="λf. (f 1)")
}

在约束名字的意义下比较项

== 按字面比较项。alpha_equal 忽略约束变量的名，这几乎总是你想要的：

test "λx. x and λy. y" {
  let x = @core.Name::new("x")
  let y = @core.Name::new("y")
  let a : @syntax.Term[Int] = Bind(x, Variable(x))
  let b : @syntax.Term[Int] = Bind(y, Variable(y))
  assert_false(a == b)
  assert_true(@syntax.alpha_equal(a, b))
}

安全地重命名自由变量

在 λy. x\lambda y.\,x 中把 x 重命名为 y 不能得到 λy. y\lambda y.\,y。rename_free 会先重命名绑定子：

test "renaming avoids capture" {
  let x = @core.Name::new("x")
  let y = @core.Name::new("y")
  let t : @syntax.Term[Int] = Bind(y, Apply(Variable(x), [Variable(y)]))
  let r = t.rename_free(@core.Renaming::singleton(x, y))
  let y1 = @core.Name::new("y_1")
  let expected : @syntax.Term[Int] = Bind(y1, Apply(Variable(y), [Variable(y1)]))
  assert_eq(r, expected)
}

自由的 x 变成了 y，而绑定子变成了 y_1，使新的 y 保持自由。

改变常量的类型

map_values 转换常量，不改动绑定结构。这里整数字面量变成浮点字面量：

test "map Int constants to Double" {
  let x = @core.Name::new("x")
  let t : @syntax.Term[Int] = Bind(x, Apply(Variable(x), [Value(2)]))
  let d : @syntax.Term[Double] = t.map_values(n => n.to_double())
  assert_true(d is Bind(_, Apply(_, [Value(2.0)])))
}

进阶

为所有感知绑定的 AST 编写分析

针对 BindingSyntax 编写的函数既适用于 Term[T]，也适用于任何实现了该 trait 的下游 AST。下面这个函数统计绑定子个数：

fn[N : @syntax.BindingSyntax] count_binders(node : N) -> Int {
  match @syntax.BindingSyntax::project(node) {
    Opaque | Variable(_) => 0
    Apply(head, args) =>
      args.fold(init=count_binders(head), (acc, a) => acc + count_binders(a))
    Bind(_, body) => 1 + count_binders(body)
  }
}

test "count binders generically" {
  let x = @core.Name::new("x")
  let t : @syntax.Term[Int] = Bind(x, Apply(Bind(x, Variable(x)), [Value(0)]))
  assert_eq(count_binders(t), 2)
}

adapter 教程为自定义 AST 实现了 BindingSyntax，之后 count_binders、泛型代换和泛型重写都能应用于它。

手动重命名绑定子

当你从部件构建绑定子时，alpha_rename_bound 会改变其变量的名，并拒绝已在体中使用的名：

test "rename the variable of a binder" {
  let x = @core.Name::new("x")
  let y = @core.Name::new("y")
  let z = @core.Name::new("z")
  let body : @syntax.Term[Int] = Apply(Variable(x), [Variable(y)])
  assert_true(body.alpha_rename_bound(x, y) is None)
  match body.alpha_rename_bound(x, z) {
    Some(renamed) => {
      let before : @syntax.Term[Int] = Bind(x, body)
      let after : @syntax.Term[Int] = Bind(z, renamed)
      assert_true(@syntax.alpha_equal(before, after))
    }
    None => fail("z is unused")
  }
}

常见陷阱

  • == 不是 α-等价。 代换和范式化的结果可能含有被重命名的绑定子，例如 y_1。请用 alpha_equal 比较。
  • 值内部的变量。 Value(T) 从不被检查。如果你的常量包含变量，请为你的 AST 实现 BindingSyntax，而不是把它包装进 Term。
  • 对绑定子调用 alpha_rename_bound。 它期望的是体：body.alpha_rename_bound(x, z)，而不是 Bind(x, body).alpha_rename_bound(...)，后者找不到可重命名的自由 x。
  • 方法风格的 trait 调用。 term.project() 已弃用；请写 @syntax.BindingSyntax::project(term)。

后续步骤