From 8b646a85fda6e7bcd6458201642763e60dc3a625 Mon Sep 17 00:00:00 2001 From: Arthur Paulino Date: Thu, 19 Mar 2026 17:53:15 -0700 Subject: [PATCH] Make level comparison sound and complete MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Replace the incomplete level_leq heuristic with a complete algorithm: - Case-split on IMax: when IMax(a1, a2) has a2 that might be zero, substitute a param p from a2 with both Zero and Succ(p), checking the inequality in both cases - Handle Param(i) ≤ Succ(X) by recursing to Param(i) ≤ X - Distribute Succ over Max: Succ(Max(x,y)) → check Succ(x) and Succ(y) - Handle Param ≤ IMax on the right via the same case-split technique Adds three helpers: level_has_param, level_any_param, level_subst_reduce. --- Ix/IxVM/KERNEL.md | 16 +++--- Ix/IxVM/Kernel.lean | 119 ++++++++++++++++++++++++++++++++++++-------- 2 files changed, 105 insertions(+), 30 deletions(-) diff --git a/Ix/IxVM/KERNEL.md b/Ix/IxVM/KERNEL.md index d1a195ec..eb820682 100644 --- a/Ix/IxVM/KERNEL.md +++ b/Ix/IxVM/KERNEL.md @@ -151,11 +151,12 @@ If `B` is NOT in `Prop`, then `imax uA uB = max uA uB`, the standard predicative ### Level Comparison Two levels are equal if they evaluate to the same natural number under every assignment -of parameters. The Lean and Rust kernels use a canonical normalization algorithm. The -Aiur kernel uses a sound but incomplete heuristic: `level_equal(a, b) = level_leq(a, b) -∧ level_leq(b, a)`, where `level_leq` handles common cases (Zero ≤ anything, -Succ-vs-Succ, Max decomposition) but falls back to structural equality for complex -`IMax` forms. +of parameters. The Aiur kernel uses `level_equal(a, b) = level_leq(a, b) ∧ level_leq(b, a)`, +where `level_leq` is sound and complete. For `IMax` forms whose second argument might be +zero, `level_leq` case-splits on a parameter `p` from that argument: it substitutes `p → 0` +(eliminating the `IMax`) and `p → Succ(p)` (resolving `IMax` to `Max`), checking the +inequality in both cases. It also distributes `Succ` over `Max` and handles +`Param(i) ≤ Succ(X)` by recursing to `Param(i) ≤ X` (valid since levels are integer-valued). ### Level Instantiation @@ -952,11 +953,6 @@ termination relies on the well-foundedness of the input declarations. irrelevance won't trigger. This is conservative (never unsound) but incomplete. The Lean/Rust kernels store the type in the FVar head and can inspect it directly. -3. **Incomplete level comparison**: `level_leq` is a heuristic. For example, - `IMax(Param(0), Param(1)) ≤ Max(Param(0), Param(1))` is always true but may not - be detected. This is sound (never claims false equalities) but may reject valid - programs. - --- ## Appendix: Reading the Code diff --git a/Ix/IxVM/Kernel.lean b/Ix/IxVM/Kernel.lean index 00a34782..bfa4af84 100644 --- a/Ix/IxVM/Kernel.lean +++ b/Ix/IxVM/Kernel.lean @@ -198,7 +198,68 @@ def kernel := ⟦ } } - -- level_leq: check a <= b (heuristic, sound but incomplete) + -- Check if a level contains any Param + fn level_has_param(l: KLevel) -> G { + match l { + KLevel.Zero => 0, + KLevel.Param(_) => 1, + KLevel.Succ(&a) => level_has_param(a), + KLevel.Max(&a, &b) => + let ha = level_has_param(a); + match ha { + 1 => 1, + 0 => level_has_param(b), + }, + KLevel.IMax(&a, &b) => + let hb = level_has_param(b); + match hb { + 1 => 1, + 0 => level_has_param(a), + }, + } + } + + -- Find any Param index in a level. Precondition: level contains at least one Param. + fn level_any_param(l: KLevel) -> [G; 8] { + match l { + KLevel.Param(i) => i, + KLevel.Succ(&a) => level_any_param(a), + KLevel.Max(&a, &b) => + let ha = level_has_param(a); + match ha { + 1 => level_any_param(a), + 0 => level_any_param(b), + }, + KLevel.IMax(&a, &b) => + let hb = level_has_param(b); + match hb { + 1 => level_any_param(b), + 0 => level_any_param(a), + }, + KLevel.Zero => [0; 8], + } + } + + -- Substitute Param(p) with repl in a level, normalizing as we go + fn level_subst_reduce(l: KLevel, p: [G; 8], repl: KLevel) -> KLevel { + match l { + KLevel.Zero => KLevel.Zero, + KLevel.Param(i) => + let eq = u64_eq(i, p); + match eq { + 1 => repl, + 0 => KLevel.Param(i), + }, + KLevel.Succ(&a) => + KLevel.Succ(store(level_subst_reduce(a, p, repl))), + KLevel.Max(&a, &b) => + level_max(level_subst_reduce(a, p, repl), level_subst_reduce(b, p, repl)), + KLevel.IMax(&a, &b) => + level_imax(level_subst_reduce(a, p, repl), level_subst_reduce(b, p, repl)), + } + } + + -- level_leq: check a <= b for all param assignments (sound and complete) fn level_leq(a: KLevel, b: KLevel) -> G { match a { KLevel.Zero => 1, @@ -206,42 +267,60 @@ def kernel := ⟦ KLevel.Max(&a1, &a2) => level_leq(a1, b) * level_leq(a2, b), KLevel.Succ(&a1) => - match b { - KLevel.Succ(&b1) => level_leq(a1, b1), - KLevel.Max(&b1, &b2) => - let r1 = level_leq(a, b1); - match r1 { - 1 => 1, - 0 => level_leq(a, b2), + match a1 { + -- Distribute Succ over Max: succ(max(x,y)) = max(succ(x), succ(y)) + KLevel.Max(&x, &y) => + level_leq(KLevel.Succ(store(x)), b) * level_leq(KLevel.Succ(store(y)), b), + _ => + match b { + KLevel.Succ(&b1) => level_leq(a1, b1), + KLevel.Max(&b1, &b2) => + let r1 = level_leq(a, b1); + match r1 { + 1 => 1, + 0 => level_leq(a, b2), + }, + _ => 0, }, - _ => 0, }, KLevel.Param(i) => match b { KLevel.Param(j) => u64_eq(i, j), + -- Param(i) <= Succ(X) iff Param(i) <= X (levels are integers, so tight) + KLevel.Succ(&b1) => level_leq(a, b1), KLevel.Max(&b1, &b2) => let r1 = level_leq(a, b1); match r1 { 1 => 1, 0 => level_leq(a, b2), }, - _ => 0, + -- Param(i) <= IMax(b1, b2): case-split on a param in b2 + KLevel.IMax(&b1, &b2) => + let p = level_any_param(b2); + let sp = KLevel.Succ(store(KLevel.Param(p))); + let a0 = level_subst_reduce(a, p, KLevel.Zero); + let bfull = KLevel.IMax(store(b1), store(b2)); + let b0 = level_subst_reduce(bfull, p, KLevel.Zero); + let a1s = level_subst_reduce(a, p, sp); + let b1s = level_subst_reduce(bfull, p, sp); + level_leq(a0, b0) * level_leq(a1s, b1s), + KLevel.Zero => 0, }, KLevel.IMax(&a1, &a2) => - -- imax(a1, a2) where a2 is definitely not zero behaves as max(a1, a2) let not_zero = level_is_not_zero(a2); match not_zero { + -- imax(a1, a2) where a2 is definitely not zero behaves as max(a1, a2) 1 => level_leq(a1, b) * level_leq(a2, b), + -- Case-split: substitute a param from a2 with Zero and Succ(Param) 0 => - match b { - KLevel.Max(&b1, &b2) => - let r1 = level_leq(a, b1); - match r1 { - 1 => 1, - 0 => level_leq(a, b2), - }, - _ => level_eq(a, b), - }, + let p = level_any_param(a2); + let sp = KLevel.Succ(store(KLevel.Param(p))); + let afull = KLevel.IMax(store(a1), store(a2)); + let a0 = level_subst_reduce(afull, p, KLevel.Zero); + let b0 = level_subst_reduce(b, p, KLevel.Zero); + let a1s = level_subst_reduce(afull, p, sp); + let b1s = level_subst_reduce(b, p, sp); + level_leq(a0, b0) * level_leq(a1s, b1s), }, } }