utlc/lambda チュートリアル

このチュートリアルでは型なしラムダ計算で計算する。項を構築し、beta と eta で正規化し、真偽値と数を関数としてエンコードし、簡約が止まらない項を扱う。

クイックスタート

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",
  "Luna-Flow/type_theory/utlc/lambda",
}

test "quick start: (λx. x) 1" {
  let x = @core.Name::new("x")
  let id : @syntax.Term[Int] = @lambda.abstraction(x, Variable(x))
  let term = @lambda.application(id, Value(1))
  assert_eq(@lambda.normalize(term, 10), NormalForm(term=Value(1), steps=1))
}

日常的な作業

項を短く保つために、いくつかのヘルパーを使う。

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

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

fn ap(f : @syntax.Term[Int], a : @syntax.Term[Int]) -> @syntax.Term[Int] {
  @lambda.application(f, a)
}

fn nf(t : @syntax.Term[Int]) -> @syntax.Term[Int] {
  match @lambda.normalize(t, 1000) {
    NormalForm(term~, ..) => term
    StepLimitReached(..) => abort("no normal form within 1000 steps")
  }
}

真偽値をエンコードする

Church 真偽値は 2 つの引数のどちらかを選ぶ。 $\mathsf{true} = \lambda t.\,\lambda f.\,t$ 、 $\mathsf{false} = \lambda t.\,\lambda f.\,f$ 、そして $\mathsf{if}\;b\;x\;y = b\,x\,y$ である。

test "church booleans" {
  let tru = lam("t", lam("f", lv("t")))
  let fls = lam("t", lam("f", lv("f")))
  let not_ = lam("b", ap(ap(lv("b"), fls), tru))
  assert_true(@syntax.alpha_equal(nf(ap(not_, tru)), fls))
  assert_true(@syntax.alpha_equal(nf(ap(not_, fls)), tru))
}

数をエンコードして足す

Church 数 $n$ は関数を $n$ 回適用する： $\overline{2} = \lambda f.\,\lambda x.\,f\,(f\,x)$ 。加算は $\lambda m.\,\lambda n.\,\lambda f.\,\lambda x.\,m\,f\,(n\,f\,x)$ である。

fn numeral(n : Int) -> @syntax.Term[Int] {
  let mut body = lv("x")
  for _ in 0..<n {
    body = ap(lv("f"), body)
  }
  lam("f", lam("x", body))
}

test "2 + 2 = 4" {
  let plus = lam(
    "m",
    lam("n", lam("f", lam("x", ap(ap(lv("m"), lv("f")), ap(ap(lv("n"), lv("f")), lv("x")))))),
  )
  let four = nf(ap(ap(plus, numeral(2)), numeral(2)))
  assert_true(@syntax.alpha_equal(four, numeral(4)))
}

正規形の束縛子名（f_1、…）は予想と異なることがあるが、alpha_equal はそれを無視する。

eta でラッパーを簡約する

$x$ が $g$ に自由に現れないとき、 $\lambda x.\,g\,x$ は単に $g$ である。normalize はこのようなラッパーを取り除く。

test "eta removes a wrapper" {
  let wrapped = lam("x", ap(lv("g"), lv("x")))
  assert_eq(@lambda.normalize(wrapped, 10), NormalForm(term=lv("g"), steps=1))
  let not_a_wrapper = lam("x", ap(lv("x"), lv("x")))
  assert_eq(
    @lambda.normalize(not_a_wrapper, 10),
    NormalForm(term=not_a_wrapper, steps=0),
  )
}

停止しない項を扱う

$\Omega = (\lambda w.\,w\,w)(\lambda w.\,w\,w)$ は永遠に自分自身へ簡約される。ステップ数の上限により、これは判定可能な結果になる。

test "omega hits the step limit" {
  let self_apply = lam("w", ap(lv("w"), lv("w")))
  let omega = ap(self_apply, self_apply)
  match @lambda.normalize(omega, 50) {
    StepLimitReached(steps~, ..) => assert_eq(steps, 50)
    NormalForm(..) => fail("omega has no normal form")
  }
  // a discarded omega is harmless under normal order
  assert_eq(nf(ap(lam("x", lv("y")), omega)), lv("y"))
}

さらに進んで

beta のみ、または別の戦略

normalize は beta-eta と正規順序に固定されている。他の組み合わせには、規則と戦略を @eval.evaluate に渡す（Luna-Flow/type_theory/eval をインポートする）。

test "beta only, weak head" {
  let term = ap(lam("x", lam("y", ap(lv("x"), lv("y")))), lv("g"))
  let rule = @rewrite.RuleName::unsafe_new("beta")
  match @eval.evaluate(term, rule, @lambda.beta_rule, WeakHead, 10) {
    NormalForm(term=result, steps~) => {
      assert_eq(steps, 1)
      assert_true(@syntax.alpha_equal(result, lam("y", ap(lv("g"), lv("y")))))
    }
    StepLimitReached(..) => fail("one step")
  }
}

弱頭部戦略で beta のみを使うと $\lambda y.\,g\,y$ で止まる。normalize ならさらに eta 簡約して $g$ にする。

ドメイン値

Value(v) は決して簡約されず、代入によってコピーされる定数である。定数に対する簡約規則（たとえば Value(Int) 上の算術）は独自の規則として追加し、rewrite チュートリアルに示すように beta_rule と組み合わせる。

より高速な正規化

名前付きの項に対する正規順序簡約は束縛子をリネームし、根から探索を繰り返す。大きな項では @debruijn.from_named で変換し、utlc/nbe を使うこと。

よくある落とし穴

n 項適用と eta。 Bind(x, …) の下の Apply(f, [a, x]) は eta 簡約されない。eta に頼る場合は application（単項）で適用を構築すること。
== による比較。 beta は捕獲を避けるために束縛子をリネームする。@syntax.alpha_equal を使うこと。
StepLimitReached を発散と読む。 これは上限に達したことを意味するだけである。正規化可能な項でも多くのステップを要することがある。
定数が計算することを期待する。 Value(1) を何に適用しても行き詰まったままである。この計算には組み込みの算術はない。

次のステップ

utlc/lambda API：正確な契約。
utlc/lambda の設計：beta、eta、古典的な定理。
stlc チュートリアル：すべての項が正規化される型付き計算。