Luna Flow
简体中文

rewrite 教程

本教程为算术项编写化简规则，逐步应用它们，在步数上限内将它们运行到范式，并阅读追踪记录以了解哪条规则在何处触发。项的类型是 Term[String]，运算符作为值：x⋅1x \cdot 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/rewrite",
}

规则是一个在项的根部改写该项或返回 None 的函数。规则 t⋅1→tt \cdot 1 \to t 用两步化简 (x⋅1)⋅1(x \cdot 1) \cdot 1：

fn times_one(t : @syntax.Term[String]) -> @syntax.Term[String]? {
  match t {
    Apply(Value("*"), [other, Value("1")]) => Some(other)
    _ => None
  }
}

test "quick start: x * 1 * 1" {
  let x = @syntax.Term::Variable(@core.Name::new("x"))
  let term : @syntax.Term[String] = Apply(Value("*"), [
    Apply(Value("*"), [x, Value("1")]),
    Value("1"),
  ])
  let rule = @rewrite.RuleName::unsafe_new("times_one")
  let step = (t : @syntax.Term[String]) => @rewrite.top_down_once(t, rule, times_one)
  assert_eq(@rewrite.normalize(term, step, 10), NormalForm(term=x, steps=2))
}

日常任务

这些示例共用几个辅助函数和第二条规则 0+t→t0 + t \to t：

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

fn lit(text : String) -> @syntax.Term[String] {
  @syntax.Value(text)
}

fn var_(text : String) -> @syntax.Term[String] {
  @syntax.Term::Variable(@core.Name::new(text))
}

fn zero_plus(t : @syntax.Term[String]) -> @syntax.Term[String]? {
  match t {
    Apply(Value("+"), [Value("0"), other]) => Some(other)
    _ => None
  }
}

执行一步并查看发生的位置

top_down_once 改写最外最左的匹配，并报告到达它的路径：

test "one step with its position" {
  let term = op("*", lit("2"), op("+", lit("0"), var_("y")))
  let rule = @rewrite.RuleName::unsafe_new("zero_plus")
  match @rewrite.top_down_once(term, rule, zero_plus) {
    Reduced(after~, path~, rule=used, ..) => {
      assert_eq(after, op("*", lit("2"), var_("y")))
      assert_eq(path.to_array(), [@rewrite.ApplyArgument(1)])
      inspect(used.value(), content="zero_plus")
    }
    NoStep => fail("expected a step")
  }
}

ApplyArgument(1) 是根部 * 的第二个参数。

在步数上限内范式化

步数上限可以防止永不停止的规则。请检查你得到的是哪种结果：

test "normal form or limit" {
  let term = op("+", lit("0"), op("+", lit("0"), var_("z")))
  let rule = @rewrite.RuleName::unsafe_new("zero_plus")
  let step = (t : @syntax.Term[String]) => @rewrite.top_down_once(t, rule, zero_plus)
  match @rewrite.normalize(term, step, 1) {
    StepLimitReached(term~, steps~) => {
      assert_eq(steps, 1)
      assert_eq(term, op("+", lit("0"), var_("z")))
    }
    NormalForm(..) => fail("one step is not enough")
  }
  assert_eq(@rewrite.normalize(term, step, 5), NormalForm(term=var_("z"), steps=2))
}

阅读追踪记录

trace 保留每一步，因此你可以解释一次化简过程：

test "explain a simplification" {
  let term = op("+", lit("0"), op("+", lit("0"), var_("z")))
  let rule = @rewrite.RuleName::unsafe_new("zero_plus")
  let step = (t : @syntax.Term[String]) => @rewrite.top_down_once(t, rule, zero_plus)
  let run = @rewrite.trace(term, step, 10)
  let lines = run
    .steps()
    .map(s => match s {
      Reduced(rule~, path~, ..) => "\{rule.value()} at depth \{path.to_array().length()}"
      NoStep => "none"
    })
  inspect(lines.join("; "), content="zero_plus at depth 0; zero_plus at depth 0")
}

选择最外或最内

当可约式嵌套时，top_down_once 选择外层的，bottom_up_once 选择内层的。对于具有合流性的规则集，两者到达相同的范式，但步骤不同：

test "outermost and innermost first steps" {
  let inner = op("+", lit("0"), var_("z"))
  let term = op("+", lit("0"), inner)
  let rule = @rewrite.RuleName::unsafe_new("zero_plus")
  match @rewrite.top_down_once(term, rule, zero_plus) {
    Reduced(path~, ..) => assert_eq(path.to_array().length(), 0)
    NoStep => fail("expected a step")
  }
  match @rewrite.bottom_up_once(term, rule, zero_plus) {
    Reduced(path~, ..) => assert_eq(path.to_array(), [@rewrite.ApplyArgument(1)])
    NoStep => fail("expected a step")
  }
}

组合多条规则

通过按顺序尝试，将多条规则组合成一条。组合后的规则只有一个名字；请给它一个能说明这一点的名字：

fn simplify(t : @syntax.Term[String]) -> @syntax.Term[String]? {
  match zero_plus(t) {
    Some(u) => Some(u)
    None => times_one(t)
  }
}

test "two rules, one normal form" {
  let term = op("+", lit("0"), op("*", var_("a"), lit("1")))
  let rule = @rewrite.RuleName::unsafe_new("simplify")
  let step = (t : @syntax.Term[String]) => @rewrite.top_down_once(t, rule, simplify)
  assert_eq(@rewrite.normalize(term, step, 10), NormalForm(term=var_("a"), steps=2))
}

如果需要知道是哪条规则触发了，请编写一个步进函数，对每条规则各调用一次 top_down_once（各自使用自己的名字），并返回第一个 Reduced。这样会优先选择项中任意位置的第一条规则，而不是更外层位置上的第二条规则。

进阶

绑定子之下的规则

遍历会进入绑定子的体，因此规则会看到开项。像上面两条那样只查看项的形状的规则，在任何位置都没有问题。跨越绑定子移动或复制子项的规则必须自己处理绑定，通常借助代换。@lambda 的 β 规则就是标准示例。

重写你自己的 AST

generic_top_down_once 和 generic_normalize 接受任何实现了 @syntax.BindingSyntax 的 AST。针对你自己的类型编写规则即可；adapter 教程给出了完整示例。

策略

eval 把这些遍历包装成具名策略（正规序、应用序、弱头），统一放在一个 evaluate 函数之后。

常见陷阱

  • 不推进的规则。 对自身输入 tt 返回 Some(t) 的规则，或抵消另一条规则的规则，会让范式化器一直忙到步数上限。请检查 StepLimitReached。
  • 非合流的规则。 如果两条规则重叠却不能汇合，不同策略可能给出不同的范式。用轨迹找出重叠之处。
  • 对输入使用 unsafe_new。 RuleName::unsafe_new("") 会中止程序。对非字面量的名使用 RuleName::new。
  • 有歧义的构造子。 没有期望类型时，@syntax.Variable(x) 有歧义；请写 @syntax.Term::Variable(x)。

后续步骤