宇宙レベル

本節では、実装の観点から宇宙レベルについて説明し、読者が Lean の宣言を型チェックする際に知っておくべきことを取り上げます。Lean の型理論における宇宙レベルの役割についてのより深い説明は TPIL4 ¹ や Mario Carneiro の論文 の第二節を参照してください。

宇宙レベルの構文は以下のようになっています：

Level ::= Zero | Succ Level | Max Level Level | IMax Level Level | Param Name

読者が注意すべき Level 型の特徴は、宇宙レベルに半順序が存在すること、変数の存在（Param コンストラクタ）、そして Max と IMax の区別です。

Max は単純に左右の引数のうち大きい方を表す宇宙レベルを構築します。例えば、Max(1, 2) は 2 に単純化され、Max(u, u+1) は u+1 に単純化されます。IMax コンストラクタは左と右の引数のうち大きい方を表しますが、これは右の引数が Zero に単純 されない場合に限り 、またこの場合は IMax は 0 へと解決されます。

IMax の重要な点は、例えば forall (x y : Sort 3), Nat は Sort 4 と推論されるが、forall (x y : Sort 3), True は Prop と推論されるように型推論の処理と相互作用することにあります。

レベル上の半順序

Lean の Level 型は半順序を備えています。つまりレベルのペアに対して実行可能な「以下」の検査が存在します。以下のなかなか素晴らしい実装は Gabriel Ebner の Lean 3 チェッカである trepplein から持ってきています。カバーしなければならないケースはかなり多いですが、複雑なマッチは cases に依存しているものだけです。これは x ≤ y であるかどうかのチェックについて、パラメータ p に Zero が代入された時、および p に Succ p が代入されたときに x ≤ y が成り立つかどうか調べることで行っています。

  leq (x y : Level) (balance : Integer): bool :=
    Zero, _ if balance >= 0 => true
    _, Zero if balance < 0 => false
    Param(i), Param(j) => i == j && balance >= 0
    Param(_), Zero => false
    Zero, Param(_) => balance >= 0
    Succ(l1_), _ => leq l1_ l2 (balance - 1)
    _, Succ(l2_) => leq l1 l2_ (balance + 1)

    -- descend left
    Max(a, b), _ => (leq a l2 balance) && (leq b l2 balance)

    -- descend right
    (Param(_) | Zero), Max(a, b) => (leq l1 a balance) || (leq l1 b balance)

    -- imax
    IMax(a1, b1), IMax(a2, b2) if a1 == a2 && b1 == b2 => true
    IMax(_, p @ Param(_)), _ => cases(p)
    _, IMax(_, p @ Param(_)) => cases(p)
    IMax(a, IMax(b, c)), _ => leq Max(IMax(a, c), IMax(b, c)) l2 balance
    IMax(a, Max(b, c)), _ => leq (simplify Max(IMax(a, b), IMax(a, c))) l2 balance
    _, IMax(a, IMax(b, c)) => leq l1 Max(IMax(a, c), IMax(b, c)) balance
    _, IMax(a, Max(b, c)) => leq l1 (simplify Max(IMax(a, b), IMax(a, c))) balance


  cases l1 l2 p: bool :=
    leq (simplify $ subst l1 p zero) (simplify $ subst l2 p zero)
    ∧
    leq (simplify $ subst l1 p (Succ p)) (simplify $ subst l2 p (Succ p))

レベルの同値

Level 型では反対称律による同値が認められています。つまり、2つのレベル l1 と l2 は l1 ≤ l2 かつ l2 ≤ l1 ならば等しいです。

実装上の注記

エクスポータは Zero をエクスポートしないことに注意してください。しかし、これは Level の0番目の要素として仮定されます。

ただこう言ってはなんですが、Level の実装はパフォーマンスに大きな影響を与えないため、ここで積極的に最適化する必要はありません。