feat: better universe normalization #8769
Conversation
|
Thanks for experimenting with this. This is blocking my idea of exposing these |
src/Lean/Level.lean
Outdated
| addOffset (mkIMaxAux l₁ l₂) k | ||
| match l₂ with | ||
| | max l₂ l₃ => | ||
| normalize (mkLevelMax (mkIMaxAux l₁ l₂) (mkIMaxAux l₁ l₃)) k |
There was a problem hiding this comment.
This might be a bad idea, since that adds a lot of duplication (also, dedent the match arms)
There was a problem hiding this comment.
I'm also not a fan of this particular branch. I wonder how many terms of the form imax u (max v w) appear in real world examples ? In my mental model of universes, maxes only appear when manipulating things that are already for sure in Types and not in arbitrary Sorts, as such, I don't see how such a thing could appear on the rhs of an imax ? Examples are welcome.
| @@ -359,10 +359,10 @@ private def isExplicitSubsumed (lvls : Array Level) (firstNonExplicit : Nat) : B | |||
| let max := lvls[firstNonExplicit - 1]!.getOffset | |||
| isExplicitSubsumedAux lvls max firstNonExplicit | |||
|
|
|||
| partial def normalize (l : Level) : Level := | |||
| partial def normalize (l : Level) (offset := 0): Level := | |||
| if isAlreadyNormalizedCheap l then l | |||
There was a problem hiding this comment.
I'm assuming this is meant to make normalize l off equivalent to addOffset (normalize l) off? Then surely the then part of here should return addOffset l off
There was a problem hiding this comment.
You're right, I'll just remove the offset for now (I mainly just wanted for the function to be tail-recursive).
…normalize` for now
|
Hmm this seems to introduce some problems, one of which being that |
Ideally, any As a sidenote, I am not fond of the fact that different normalizations steps are done when constructing terms, and when normalizing them during equality checking. I would much rather have an explicit pass that does all of this. This draft will probably be stale for a month or so (holiday+paper deadline incoming), but I've started on implementing a complete checker for universe equality instead of simply juggling with better normalization rules. This in particular, involves doing case splits on certain universe levels to get rid of problematic |
|
Yes, I agree that merely adding normalization rules won't solve the problem that the procedure is simply incomplete. I also had an idea of how to write a complete procedure and am interested in your approach. |
This PR attempts to make Lean's universe equality checker more complete, by improving the normalization procedure over universe le 8000 vels. In particular,
imax u (imax v w)now reduces toimax (max u v) w, andimax u (max v w)reduces tomax (imax u v) (imax u w)(both of these reductions are valid under Lean's usual model for universes)Taking advantage of the better normalisation procedure, this PR also improves the generation for linear
NoConfusions by being as Sort-polymorphic as the original quadratic algorithm.This is only a draft PR to experiment with this change, and bench the potential performance changes.