utlc/nbe API

utlc/nbe パッケージは評価によって型なし De Bruijn 項を正規化する。eval は項を遅延意味領域で解釈し、quote は意味値を beta 正規形の項として読み戻し、normalize はその両方を行う。各フェーズは燃料を消費するため、発散する項は永遠に走り続けるのではなく FuelExhausted で終わる。

import {
  "Luna-Flow/type_theory/core",
  "Luna-Flow/type_theory/debruijn",
  "Luna-Flow/type_theory/utlc/nbe",
}

デフォルトのエイリアスは @nbe である。意味領域と正しさの論証は utlc/nbe の設計で説明する。

燃料

燃料は単位で測るステップ予算である。項ノードの評価、遅延値の強制、値の読み戻しはそれぞれ 1 単位を消費する。すべての結果は使用した単位数 consumed を報告する。燃料が <= 0 の呼び出しは何もせずに FuelExhausted(consumed=0) を返す（quote はまず負のレベルを拒否する）。呼び出しの結果は、消費した分を超える燃料には依存しない。燃料 $f$ の呼び出しが $c$ 単位を消費して正規形を返すなら、燃料が $c$ 以上のどの呼び出しも同じ結果を返す。

意味値

Semantic

Semantic[T] は不透明な意味値である。

pub struct Semantic[T] {
  inner : SemanticInner[T]
}

type SemanticInner[T]

意味値は、定数、クロージャ（環境付きの束縛子本体）、遅延引数、または中立値（自由変数、quote レベルの変数、あるいは引数に適用された中立値）のいずれかである。表現は非公開であり、値は eval と reflect_* 関数によって生成され、quote によって消費される。

reflect_free

reflect_free は自由名を中立意味値に変換する。

pub fn[T] reflect_free(@core.Name) -> Semantic[T]

これを quote すると Free(name) が得られる。

reflect_level

reflect_level は quote レベルを中立意味変数に変換する。

pub fn[T] reflect_level(Int) -> Semantic[T]?

負のレベルに対しては None を返す。レベル l の変数を深さ n > l で quote すると Bound(n - l - 1) が得られる。

test "reflect and quote neutral values" {
  let y = @core.Name::new("y")
  let free : @nbe.Semantic[Int] = @nbe.reflect_free(y)
  assert_true(@nbe.quote(free, 0, 10) is Quoted(term=Free(_), ..))
  match @nbe.reflect_level(0) {
    Some(v) => {
      let value : @nbe.Semantic[Int] = v
      // the variable of level 0, seen from depth 2, is index 1
      assert_true(@nbe.quote(value, 2, 10) is Quoted(term=Bound(1), ..))
    }
    None => fail("level 0 is valid")
  }
  let negative : @nbe.Semantic[Int]? = @nbe.reflect_level(-1)
  assert_true(negative is None)
}

評価と読み戻し

EvaluationResult

EvaluationResult[T] は eval の結果である。

pub(all) enum EvaluationResult[T] {
  Evaluated(value~ : Semantic[T], consumed~ : Int)
  FuelExhausted(consumed~ : Int)
  ScopeFailure(error~ : @debruijn.ScopeError, consumed~ : Int)
}

eval

eval は閉じた De Bruijn 項を遅延意味領域で弱頭部形まで評価する。

pub fn[T] eval(@debruijn.DbTerm[T], Int) -> EvaluationResult[T]

項はスコープが正しくなければならない（自由名は許される）。そうでなければ結果は consumed=0 の ScopeFailure となる。評価は名前呼びである。引数は遅延され、必要になったときにのみ評価される。評価はクロージャまたは中立値で停止し、束縛子の中には入らない。

QuoteResult

QuoteResult[T] は quote の結果である。

pub(all) enum QuoteResult[T] {
  Quoted(term~ : @debruijn.DbTerm[T], consumed~ : Int)
  FuelExhausted(consumed~ : Int)
  ScopeFailure(error~ : @debruijn.ScopeError, consumed~ : Int)
}

quote

quote は意味値を beta 正規形の De Bruijn 項として読み戻す。

pub fn[T] quote(Semantic[T], Int, Int) -> QuoteResult[T]

quote(value, level, fuel) は value を level 個の束縛子の下で読み戻す。クロージャは、現在のレベルの新しい変数に適用し、その結果を束縛子 1 つ分深い位置で読み戻すことで読み戻される。中立な適用は引数ごとに読み戻され、その際に遅延引数が強制される。eval から得た値には level = 0 を使う。負の level、あるいは level 未満でないレベル変数は ScopeFailure(NegativeIndex) となる。

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

正規化

NbeResult

NbeResult[T] は normalize の結果である。

pub(all) enum NbeResult[T] {
  NormalForm(term~ : @debruijn.DbTerm[T], consumed~ : Int)
  FuelExhausted(consumed~ : Int)
  ScopeFailure(error~ : @debruijn.ScopeError, consumed~ : Int)
} derive(Eq, @debug.Debug)
pub fn[T : Eq] NbeResult::equal(Self[T], Self[T]) -> Bool

normalize

normalize はスコープの正しい De Bruijn 項の beta 正規形を燃料予算内で計算する。

pub fn[T] normalize(@debruijn.DbTerm[T], Int) -> NbeResult[T]

項を検証し、評価し、結果をレベル 0 で quote する。これらは 1 つの予算を共有する。NormalForm(t, c)：t は beta 正規形であり、c 単位で到達した。FuelExhausted(c)：予算が尽きた。項は発散するかもしれないし、より多くの燃料が必要なだけかもしれない。ScopeFailure：入力にぶら下がった、または負のインデックスがある。

結果の適用は単項である。正規形 $f\,a\,b$ は Apply(Apply(f, [a]), [b]) として返されるが、@debruijn.normalize は入力の n 項スパイン Apply(f, [a, b]) を保つ。スパインを平坦化すれば両者は一致する。

test "lazy evaluation skips an unused divergent argument" {
  let w : @debruijn.DbTerm[Int] = Bind(Apply(Bound(0), [Bound(0)]))
  let omega : @debruijn.DbTerm[Int] = Apply(w, [w])
  let term : @debruijn.DbTerm[Int] = Apply(Bind(Value(7)), [omega])
  assert_true(@nbe.normalize(term, 100) is NormalForm(term=Value(7), ..))
  assert_true(@nbe.normalize(omega, 100) is FuelExhausted(_))
}