Luna Flow
简体中文

substitution 教程

本教程用项替换变量：实例化模板、交换变量、在绑定子之下代换而不捕获任何东西、复合代换以及部分求值。示例把算术编码为 Term[String]，运算符作为值：x+1x + 1 是 Apply(Value("+"), [Variable(x), Value("1")])。

快速入门

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

在 x+1x + 1 中用 22 代换 xx：

test "quick start: x + 1 with x := 2" {
  let x = @core.Name::new("x")
  let term : @syntax.Term[String] = Apply(Value("+"), [Variable(x), Value("1")])
  let s = @substitution.Substitution::singleton(x, @syntax.Value("2"))
  assert_eq(s.apply(term), Apply(Value("+"), [Value("2"), Value("1")]))
}

日常任务

下面的示例共用两个辅助函数：

fn name(text : String) -> @core.Name {
  @core.Name::new(text)
}

fn plus(a : @syntax.Term[String], b : @syntax.Term[String]) -> @syntax.Term[String] {
  @syntax.Apply(@syntax.Value("+"), [a, b])
}

交换两个变量

代换的所有条目同时生效，因此交换不需要临时变量：

test "swap x and y" {
  let x = name("x")
  let y = name("y")
  let swap = @substitution.Substitution::singleton(x, @syntax.Term::Variable(y))
    .set(y, @syntax.Term::Variable(x))
  assert_eq(swap.apply(plus(Variable(x), Variable(y))), plus(Variable(y), Variable(x)))
}

在绑定子之下代换

在 λy. x+y\lambda y.\, x + y 中用 yy 代换 xx 时，不能让插入的 yy 变成被约束的那个。绑定子会被重命名为 y_1：

test "no capture under a binder" {
  let x = name("x")
  let y = name("y")
  let term : @syntax.Term[String] = Bind(y, plus(Variable(x), Variable(y)))
  let result = @substitution.Substitution::singleton(x, @syntax.Term::Variable(y))
    .apply(term)
  let y1 = name("y_1")
  let expected : @syntax.Term[String] = Bind(y1, plus(Variable(y), Variable(y1)))
  assert_eq(result, expected)
}

被代换变量自身的绑定子会遮蔽它，因此内部什么也不会发生：

test "a binder shadows the substituted variable" {
  let x = name("x")
  let term : @syntax.Term[String] = Bind(x, Variable(x))
  let s = @substitution.Substitution::singleton(x, @syntax.Value("0"))
  assert_eq(s.apply(term), term)
}

部分求值

代换已知的变量，其余变量保持原位：

test "partial evaluation" {
  let x = name("x")
  let y = name("y")
  let known = @substitution.Substitution::singleton(x, @syntax.Value("3"))
  let result = known.apply(plus(Variable(x), Variable(y)))
  assert_eq(result, plus(Value("3"), Variable(y)))
  assert_true(@syntax.free_variables(result).contains(y))
}

复合代换

first.then(second) 是先做 first 再做 second 的单个代换。它在一次遍历中完成：

test "compose two steps into one" {
  let x = name("x")
  let y = name("y")
  let first = @substitution.Substitution::singleton(x, plus(Variable(y), Value("1")))
  let second = @substitution.Substitution::singleton(y, @syntax.Value("5"))
  let both = first.then(second)
  let term = plus(Variable(x), Variable(y))
  assert_eq(both.apply(term), plus(plus(Value("5"), Value("1")), Value("5")))
  assert_true(@syntax.alpha_equal(both.apply(term), second.apply(first.apply(term))))
}

进阶

实现 beta 归约

Beta 归约 (λx. b) a→b[x:=a](\lambda x.\,b)\,a \to b[x := a] 就是一次代换。@lambda.beta_rule 正是这样工作的：

fn beta(t : @syntax.Term[String]) -> @syntax.Term[String]? {
  match t {
    Apply(Bind(x, body), [arg]) =>
      Some(@substitution.Substitution::singleton(x, arg).apply(body))
    _ => None
  }
}

test "beta via substitution" {
  let x = name("x")
  let y = name("y")
  let k : @syntax.Term[String] = Bind(x, Bind(y, Variable(x)))
  let result = beta(Apply(k, [Variable(y)]))
  let expected : @syntax.Term[String] = Bind(name("y_1"), Variable(y))
  assert_eq(result, Some(expected))
}

自行迭代到不动点

代换只应用一次。如果替换内容可能提及定义域中的变量，而你也希望它们被替换，就要重复应用，并设定上限，因为这个过程未必终止（想想 x:=x+1x := x + 1）：

fn apply_until_stable(
  s : @substitution.Substitution[String],
  t : @syntax.Term[String],
  limit : Int,
) -> @syntax.Term[String] {
  let mut current = t
  for _ in 0..<limit {
    let next = s.apply(current)
    if next == current {
      break
    }
    current = next
  }
  current
}

test "resolve a chain of definitions" {
  let x = name("x")
  let y = name("y")
  let defs = @substitution.Substitution::singleton(x, @syntax.Term::Variable(y))
    .set(y, @syntax.Value("7"))
  assert_eq(apply_until_stable(defs, Variable(x), 10), Value("7"))
}

在你自己的 AST 中代换

GenericSubstitution 在任何实现了 @syntax.BindingSyntax 的 AST 上运行相同的算法。adapter 教程定义了这样一个 AST，并用 apply_once 在其中代换。

常见陷阱

  • 有歧义的构造子。 没有期望类型时 @syntax.Variable(y) 有歧义，因为 BindingView 也有一个 Variable 分支。请写 @syntax.Term::Variable(y)，或标注期望类型。
  • 期望重复代换。 {x↦y, y↦7}\{x \mapsto y,\ y \mapsto 7\} 作用于 xx 得到 yy，而不是 77。请使用 then 或显式迭代。
  • 用 == 比较。 结果可能包含被重命名的绑定子（y_1）。除非你知道确切的名，否则请用 @syntax.alpha_equal 比较。
  • 值内部的变量。 不会对 Value 的载荷进行代换。

后续步骤