Luna Flow
日本語

utlc/lambda API

utlc/lambda パッケージは共有の名前付き構文 @syntax.Term[T] 上の型なしラムダ計算である。抽象と適用のコンストラクタ、β 規則と η 規則、そして有界な正規順序の正規化器を提供する。これはライブラリの参照操作的意味論である。

import {
  "Luna-Flow/type_theory/core",
  "Luna-Flow/type_theory/syntax",
  "Luna-Flow/type_theory/rewrite",
  "Luna-Flow/type_theory/utlc/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 を生成し、2 番目は eta である。