Luna Flow
简体中文

utlc/lambda API

utlc/lambda 包是基于共享命名语法 @syntax.Term[T] 的无类型 lambda 演算：抽象与应用的构造器、β 规则与 η 规则，以及有界的正规序范式化器。它是本库的参考操作语义。

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

默认别名为 @lambda。在 lambda 项中，Bind(x, b) 是 λx. b\lambda x.\,b，Apply(f, [a]) 是 f af\,a，Value(v) 是不透明常量。这些规则在 utlc/lambda 设计中有说明。

构造器

abstraction

abstraction 构建 λx. body\lambda x.\,body。

pub fn[T] abstraction(@core.Name, @syntax.Term[T]) -> @syntax.Term[T]

它返回 Bind(parameter, body)。

application

application 构建一元应用 f af\,a。

pub fn[T] application(@syntax.Term[T], @syntax.Term[T]) -> @syntax.Term[T]

它返回 Apply(function, [argument])。

test "build (λx. x) y" {
  let x = @core.Name::new("x")
  let y = @core.Name::new("y")
  let id : @syntax.Term[Int] = @lambda.abstraction(x, Variable(x))
  let term = @lambda.application(id, Variable(y))
  assert_eq(term, Apply(Bind(x, Variable(x)), [Variable(y)]))
}

规则

beta_rule

beta_rule 收缩项根部的 β 可约式。

pub fn[T] beta_rule(@syntax.Term[T]) -> @syntax.Term[T]?

对于 Apply(Bind(x, body), [a, ..rest])，它返回避免捕获的代换 body[x := a]，当 rest 非空时再将其应用于 rest。对于其他所有项，它返回 None。它适用于任意领域类型 T，因为值从不被检查。

eta_rule

eta_rule 收缩项根部的 η 可约式。

pub fn[T] eta_rule(@syntax.Term[T]) -> @syntax.Term[T]?

对于 x 在 f 中不自由的 Bind(x, Apply(f, [Variable(x)]))，它返回 f；否则返回 None。只有一元应用才是 η 可约式：Bind(x, Apply(f, [a, Variable(x)])) 不会被收缩。

beta_eta_rule

beta_eta_rule 先尝试 beta_rule，若不适用再尝试 eta_rule。

pub fn[T] beta_eta_rule(@syntax.Term[T]) -> @syntax.Term[T]?

一个项不可能在根部既是 β 可约式又是 η 可约式（一个是 Apply，另一个是 Bind），因此顺序只是说明优先级。

test "beta and eta at the root" {
  let x = @core.Name::new("x")
  let y = @core.Name::new("y")
  let f = @core.Name::new("f")
  let k : @syntax.Term[Int] = Bind(x, Bind(y, Variable(x)))
  let expected : @syntax.Term[Int] = Bind(@core.Name::new("y_1"), Variable(y))
  assert_eq(@lambda.beta_rule(Apply(k, [Variable(y)])), Some(expected))
  let eta_redex : @syntax.Term[Int] = Bind(x, Apply(Variable(f), [Variable(x)]))
  assert_eq(@lambda.eta_rule(eta_redex), Some(Variable(f)))
  let not_eta : @syntax.Term[Int] = Bind(x, Apply(Variable(x), [Variable(x)]))
  assert_eq(@lambda.beta_eta_rule(not_eta), None)
}

范式化

normalize

normalize 在步数上限内用正规序归约把项归约到 beta-eta 范式。

pub fn[T] normalize(@syntax.Term[T], Int) -> @rewrite.NormalizationResult[T]

它就是 @eval.evaluate(term, "beta_eta", beta_eta_rule, NormalOrder, max_steps)：每一步收缩项中任意位置（包括绑定子之下）最左最外的 beta 或 eta 可约式。NormalForm(t, n) 表示 t 没有 beta 或 eta 可约式（按上文的一元意义），且在 n 步内得到；StepLimitReached 表示步数上限已用完。发散项（例如 Ω\Omega）总是以 StepLimitReached 结束。

test "normalize (λx. λy. x y) y" {
  let x = @core.Name::new("x")
  let y = @core.Name::new("y")
  let inner : @syntax.Term[Int] = Bind(y, Apply(Variable(x), [Variable(y)]))
  let term : @syntax.Term[Int] = Apply(Bind(x, inner), [Variable(y)])
  assert_eq(@lambda.normalize(term, 10), NormalForm(term=Variable(y), steps=2))
}

第一步是 beta，得到 λy1. y y1\lambda y_1.\,y\,y_1；第二步是 eta。