Luna Flow
日本語

utlc/nbe チュートリアル

このチュートリアルでは、評価による正規化で型なしラムダ項を正規化する。燃料予算の範囲で De Bruijn 項の正規形を高速に得る。名前で書いた項を正規化し、予算を選び、consumed カウンタを読み、結果をスモールステップ簡約器と比較する。

クイックスタート

moon add Luna-Flow/type_theory@0.2.0
import {
  "Luna-Flow/type_theory/core",
  "Luna-Flow/type_theory/syntax",
  "Luna-Flow/type_theory/debruijn",
  "Luna-Flow/type_theory/utlc/nbe",
}
test "quick start: (λ. 0) 5" {
  let term : @debruijn.DbTerm[Int] = Apply(Bind(Bound(0)), [Value(5)])
  match @nbe.normalize(term, 100) {
    NormalForm(term=normal, consumed~) => {
      assert_eq(normal, Value(5))
      assert_true(consumed > 0)
    }
    _ => fail("small closed term")
  }
}

日常的な作業

名前付きの項を正規化する

名前で項を書き、from_named で変換し、正規化し、表示のために変換し戻す。

fn church(n : Int) -> @syntax.Term[Int] {
  let f = @core.Name::new("f")
  let x = @core.Name::new("x")
  let mut body : @syntax.Term[Int] = Variable(x)
  for _ in 0..<n {
    body = Apply(Variable(f), [body])
  }
  Bind(f, Bind(x, body))
}

test "2 * 3 = 6 with Church numerals" {
  let m = @core.Name::new("m")
  let n = @core.Name::new("n")
  let f = @core.Name::new("f")
  // times = λm. λn. λf. m (n f)
  let times : @syntax.Term[Int] = Bind(
    m,
    Bind(n, Bind(f, Apply(Variable(m), [Apply(Variable(n), [Variable(f)])]))),
  )
  let term : @syntax.Term[Int] = Apply(times, [church(2), church(3)])
  match @nbe.normalize(@debruijn.from_named(term), 10_000) {
    NormalForm(term=normal, ..) => assert_eq(normal, @debruijn.from_named(church(6)))
    _ => fail("normalizes")
  }
}

De Bruijn 形式を == で比較することは、α同値を除いて比較することである。

燃料予算を選ぶ

燃料が制限するのは時間ではなく作業量である。燃料が少なすぎると FuelExhausted になる。成功した実行の consumed の値は、その実行が必要とする正確な量である。

test "the budget a run needs" {
  let id : @debruijn.DbTerm[Int] = Bind(Bound(0))
  let term : @debruijn.DbTerm[Int] = Apply(id, [Apply(id, [Value(1)])])
  match @nbe.normalize(term, 1000) {
    NormalForm(consumed~, ..) => {
      assert_true(@nbe.normalize(term, consumed) is NormalForm(..))
      assert_true(@nbe.normalize(term, consumed - 1) is FuelExhausted(..))
    }
    _ => fail("normalizes")
  }
}

発散と遅延を見分ける

Ω\Omega は決して正規形に到達しないので、必ず予算を使い切る。使われない引数は決して評価されないので、Ω\Omega を定数関数に渡しても問題ない。

test "omega and a lazy argument" {
  let w : @debruijn.DbTerm[Int] = Bind(Apply(Bound(0), [Bound(0)]))
  let omega : @debruijn.DbTerm[Int] = Apply(w, [w])
  assert_true(@nbe.normalize(omega, 500) is FuelExhausted(consumed=500))
  let ignore : @debruijn.DbTerm[Int] = Bind(Value(0))
  assert_true(@nbe.normalize(Apply(ignore, [omega]), 500) is NormalForm(term=Value(0), ..))
}

スコープの正しくない入力を拒否する

normalize はまず検証を行い、ぶら下がったインデックスをデータとして報告する。

test "scope errors are reported" {
  let bad : @debruijn.DbTerm[Int] = Bind(Bound(3))
  assert_eq(
    @nbe.normalize(bad, 100),
    ScopeFailure(error=UnboundIndex(index=3, depth=1), consumed=0),
  )
}

さらに進んで

スモールステップ簡約と比較する

NbE は単項の適用を返し、@debruijn.normalize は n 項スパインを保つ。比較の前にスパインを平坦化する。

fn flatten(t : @debruijn.DbTerm[Int]) -> @debruijn.DbTerm[Int] {
  match t {
    Apply(head, args) => {
      let flat_args = args.map(flatten)
      match flatten(head) {
        Apply(h, inner) => Apply(h, [..inner, ..flat_args])
        h => Apply(h, flat_args)
      }
    }
    Bind(body) => Bind(flatten(body))
    other => other
  }
}

test "nbe agrees with small-step after flattening" {
  let f = @core.Name::new("f")
  // (λ. λ. f 1 0) 7 8
  let term : @debruijn.DbTerm[Int] = Apply(Bind(Bind(Apply(Free(f), [Bound(1), Bound(0)]))), [
    Value(7),
    Value(8),
  ])
  match (@nbe.normalize(term, 1000), @debruijn.normalize(term, 100)) {
    (NormalForm(term=a, ..), NormalForm(term=b, ..)) => {
      assert_false(a == b)
      assert_eq(flatten(a), flatten(b))
    }
    _ => fail("both normalize")
  }
}

パイプラインを直接使う

eval は不透明な意味値を生成し、quote はそれを読み戻す。両者を分けると、1 回だけ評価して選んだレベルで読み戻したり、reflect_free で作った中立値を読み戻したりできる。

test "eval and quote separately" {
  let k : @debruijn.DbTerm[Int] = Bind(Bind(Bound(1)))
  match @nbe.eval(k, 100) {
    Evaluated(value~, ..) =>
      assert_true(@nbe.quote(value, 0, 100) is Quoted(term=Bind(Bind(Bound(1))), ..))
    _ => fail("closed term")
  }
}

よくある落とし穴

  • スモールステップの結果と == で比較する。 スパインの形が異なる。先に平坦化すること。
  • FuelExhausted を発散とみなす。 これは予算が尽きたことを示すだけである。予算を増やすか、予算を必要としない型付きの stlc 正規化器を使うこと。
  • 重複した引数。 評価は共有なしの名前呼びである。高価な引数を何度も使う項は、そのたびにコストを払う。
  • ぶら下がったインデックスを持つ開いた項。 自由変数は Free(name) でなければならない。束縛子のない Bound インデックスはスコープエラーである。

次のステップ