Level normalization

Stream: Type theory

[Mario Carneiro]

I just wanted to share an algorithm I just implemented for lean4lean based on a paper by @Yoan Géran which gives a complete normalization algorithm for imax expressions. Compared to Yoan's version, my version of the algorithm is able to reify expressions back into Level, rather than staying in the extended "sublevel" algebra used in the paper's normal form. Here are some fun equalities it can verify:

import Lean4Lean.Level

elab "normalize " l:level : command => do
  Elab.Command.runTermElabM fun _ => do
    logInfo m!"{(← Elab.Term.elabLevel l).normalize'}"

universe u v w
/-- info: max 1 u -/
#guard_msgs in normalize max u 1
/-- info: u -/
#guard_msgs in normalize imax 1 u
/-- info: max 1 (imax (u+1) u) -/
#guard_msgs in normalize u+1
/-- info: imax 2 u -/
#guard_msgs in normalize imax 2 u
/-- info: max v (imax (imax u v) w) -/
#guard_msgs in normalize max w (imax (imax u w) v)
/-- info: max v (imax (imax u v) w) -/
#guard_msgs in normalize max (imax (imax u v) w) (imax (imax u w) v)
/-- info: u -/
#guard_msgs in normalize imax u u
/-- info: max 1 (imax (u+1) u) -/
#guard_msgs in normalize imax u (u+1)

cc: @Arthur Adjedj since we talked about this at TYPES

[Aaron Liu]

amazing but why are those weird max 1 (imax (u+1) u)

[Mario Carneiro]

turns out u+1 has a funny normal form

[Mario Carneiro]

because it can be split into the max of two things that don't dominate each other, namely 1 and imax (u+1) u = if u=0 then 0 else u+1

[Aaron Liu]

interesting

[Aaron Liu]

does it work with metavariables

[Mario Carneiro]

no, but it would not be any different, it would just be another kind of variable

[Mario Carneiro]

unless you want to do unification

[Aaron Liu]

I guess unification would be hard?

[Mario Carneiro]

it seems ill defined

[Mario Carneiro]

I don't think it's that hard, the normal form is reasonably okay, but you have to decide what you actually want to get in the many ambiguous cases

[Aaron Liu]

I think "given a finite set of equations (pairs of universe formulas) with metavariables, find any assignment of metavariables satisfying all the equations or report no solution exists" could be described as unification

[Yoan Géran]

That's cool to see it implemented. I had planned to implement the algorithm in C++ for Lean, but couldn't find the time

[Yoan Géran]

@Aaron Liu Do we require the most general unifier (if it exists) or any unifier is good?

[Bas Spitters]

@Mario Carneiro interesting! How does it compare to the work by Bezem, Coquand, Sozeau which is being implemented in Rocq ?

[Bas Spitters]

https://msp.cis.strath.ac.uk/types2025/abstracts/TYPES2025_paper21.pdf

[Mario Carneiro]

I think Rocq's universe algebra is more complicated, but it also doesn't have imax I think

[Mario Carneiro]

the really hard part of this algorithm is dealing with imax expressions

[Bas Spitters]

Thanks. Yes, I don't see imax in their work.