## Stream: general

### Topic: Normalization fails in lean

#### Mario Carneiro (Nov 18 2019 at 21:01):

Andreas Abel and Thierry Coquand have brought my attention to the following counterexample to normalization in impredicative type theories with proof irrelevance, such as Lean.

def false' := ∀ p : Prop, p
def true' := false' → false'
def omega : (∀ (A B : Prop), A = B) → false' :=
λ h A, @cast true' _ (h true' A) $λ z: false', z true' z def Omega : (∀ (A B : Prop), A = B) → false' := λ h, omega h true' (omega h) #reduce Omega -- timeout  #### Patrick Massot (Nov 18 2019 at 21:02): Should we care? #### Mario Carneiro (Nov 18 2019 at 21:05): It is news; this was the last remaining unresolved question in my MS thesis, and I had expected it to be true, so this counterexample is a surprise. Normalization is sometimes used for proofs of consistency, but in lean's case we have a model construction that achieves this goal by alternate means, so that at least is not at risk #### Mario Carneiro (Nov 18 2019 at 21:09): It does, however, put us more firmly in the "classical" camp, because our type theory can't be used to "just compute" anything that doesn't use axioms #### Mario Carneiro (Nov 18 2019 at 21:10): at this point I would prefer to just have a reflection axiom to deduce A is defeq to B from A = B and finish the job #### Mario Carneiro (Nov 18 2019 at 21:14): It does possibly open the door to performing arbitrary TM computations in the lean kernel. We already knew that this was possible in theory, but lean would not actually perform the required sequence of reductions, it would get stuck early on. The difference with this example is that lean actually goes ahead and does the infinite reduction. #### Mario Carneiro (Nov 18 2019 at 21:18): (It's not clear if this can be used to do useful computation, though, as, like the example in my paper, it requires an inconsistent context, so it's tricky to get the computation out into an inhabited context.) #### Simon Hudon (Nov 18 2019 at 21:42): In #reduce Omega -- timeout, Omega should be a lambda abstraction. Why does the reduction not stop there? #### Bryan Gin-ge Chen (Nov 18 2019 at 21:43): Are there options to control the number of steps #reduce takes? Is there any option to trace the reduction steps? #### Mario Carneiro (Nov 18 2019 at 21:46): #reduce will reduce the whole term to a normal form, it doesn't stop at whnf #### Mario Carneiro (Nov 18 2019 at 21:47): sadly there is no way to trace the reduction #### Bryan Gin-ge Chen (Nov 18 2019 at 21:48): How hard would it be to imitate the reduction in meta code? #### Mario Carneiro (Nov 18 2019 at 21:50): example (h) : Omega h = Omega h := calc Omega h = omega h true' (omega h) : rfl ... = @cast true' true' (h true' true') (λ z: false', z true' z) (omega h) : rfl ... = (λ z: false', z true' z) (omega h) : rfl ... = (omega h) true' (omega h) : rfl ... = Omega h : rfl  #### Jeremy Avigad (Nov 18 2019 at 21:54): Their result is a very pretty result, even though it is unfortunate for Lean. But it is not clear whether this result has any bearing on data, i.e. whether we can get a term of type nat that doesn't normalize. And even if we can, there is still hope for eval, which will erase nonsense like Omega. I don't know what to make of it. Definitional proof irrelevance is nice in practice, and it is hard to imagine someone formalizing mathematics stumbling across a non-normalizing term. I'd rather have a type theory that is theoretically bad but nice in practice than a type theory that is theoretically nice but bad in practice, but of course it would be better to have a theory with both the theoretical and the practical virtues. #### Mario Carneiro (Nov 18 2019 at 21:55): So the question of whether VM evaluation on a computable well typed term can run forever is still open #### Mario Carneiro (Nov 19 2019 at 09:46): Here's a modification of the example to act like a Y combinator: def false' := ∀ p : Prop, p def true' := false' → false' def y (f : false' → false') (h : ∀ (A B : Prop), A = B) : false' := λ A, @cast true' _ (h true' A)$ λ z: false', f (z true' z)

def Y (f : false' → false') (h : ∀ (A B : Prop), A = B) : false' :=
y f h true' (y f h)

example (f h) : Y f h = f (f (f (f (f (f (Y f h)))))) := rfl


Now we can compute with arbitrary functions on false' :P

#### Kevin Buzzard (Nov 19 2019 at 09:48):

It does, however, put us more firmly in the "classical" camp, because our type theory can't be used to "just compute" anything that doesn't use axioms

So in fact this is something to celebrate, as far as mathematicians are concerned!

#### Mario Carneiro (Nov 19 2019 at 10:08):

Embedded lambda calculus:

section
parameter (H : ∀ (A B : Prop), A = B)

def D := ∀ p : Prop, p
def F := D → D

def app (a b : D) : D := a F b
local infix  $:400 := app def lam (f : D → D) : D := λ A, @cast F _ (H F A) f local notation Λ binders ,  r:(scoped P, lam P) := r example (f x) : lam f$ x = f x := rfl

def y (f : F) : D := Λ z, f (z $z) def Y (f : F) : D := y f$ y f

#reduce lam id

def zero : D := Λ f x, x
def succ (n : D) : D := Λ f x, f $(n$ f $x) def of_nat : ℕ → D | 0 := zero | (n+1) := succ (of_nat n) def plus (m n : D) : D := Λ f x, m$ f $(n$ f $x) example : plus (of_nat 2) (of_nat 2) = of_nat 4 := rfl end  #### Gaëtan Gilbert (Nov 20 2019 at 10:40): (It's not clear if this can be used to do useful computation, though, as, like the example in my paper, it requires an inconsistent context, so it's tricky to get the computation out into an inhabited context.) It doesn't require an inconsistent context (but does require an axiom AFAICT), you can do the same manipulation using an hypothesis ∀ (A B : Prop), A → B → A = B (propext for inhabited propositions) and instead of inhabiting ∀ p : Prop, p inhabit ∀ p : Prop, p → p ie def top := ∀ p : Prop, p → p def ext := ∀ (A B : Prop), A → B → A = B def supercast (h : ext) (A B : Prop) (a : A) (b : B) : B := @cast A B (h A B a b) a def omega : ext → top := λ h A a, supercast h (top → top) A (λ z: top, z (top → top) (λ x, x) z) a def Omega : ext → top := λ h, omega h (top → top) (λ x, x) (omega h) #reduce Omega -- timeout  See also discussion at https://github.com/coq/coq/pull/10390 #### Mario Carneiro (Nov 20 2019 at 11:56): Right, here's another example shared by Andreas Abel: -- axiom propext {a b : Prop} : (a ↔ b) → a = b def True := ∀ p : Prop, p → p def om : True := λ A a, @cast (True → True) A (propext ⟨λ _, a, λ _, id⟩)  λ z: True, z (True → True) id z def Om : True := om (True → True) id om -- #reduce Om -- timeout example : Om = Om := calc Om = om (True → True) id om : rfl ... = @cast (True → True) (True → True) (propext ⟨λ _, id, λ _, id⟩) (λ z: True, z (True → True) id z) om : rfl ... = (λ z: True, z (True → True) id z) om : rfl ... = om (True → True) id om : rfl ... = Om : rfl  #### Mario Carneiro (Nov 20 2019 at 11:59): More lambda calculus: def D := ∀ p : Prop, p → p def F := D → D def app (a b : D) : D := a F id b local infix $ :400 := app

def lam (f : D → D) : D := λ A a, @cast F _ (propext ⟨λ _, a, λ _, id⟩) f
local notation Λ binders ,  r:(scoped P, lam P) := r



#### Wojciech Nawrocki (Nov 20 2019 at 18:34):

Am I misunderstanding something, or does this mean that Lean's algorithmic equivalence is also undecidable?

#### Wojciech Nawrocki (Nov 21 2019 at 00:23):

Oh well, it shouldn't be because these are Props, right? But then

def Omega' : pext → top := λ h, (λ p x, x)
theorem blah : Omega = Omega' := rfl


goes into a loop in the kernel (deep recursion was detected at 'replace' (potential solution: increase stack space in your system)). What's going on here - why does Lean seemingly reduce them instead of immediately coming back and saying "these are two proofs of pext → top, hence the same"?

#### Mario Carneiro (Nov 21 2019 at 01:35):

Am I misunderstanding something, or does this mean that Lean's algorithmic equivalence is also undecidable?

I think it is decidable, but lean's algorithm doesn't decide it. If you never reduce proofs then I think you might be able to dodge this bullet

#### Mario Carneiro (Nov 21 2019 at 01:38):

I'm not sure why your example loops. Perhaps lean doesn't notice that they are props? That seems unlikely...

#### Mario Carneiro (Nov 21 2019 at 14:23):

Abel and Coquand's paper with the original example is on arXiv: https://arxiv.org/abs/1911.08174

#### Wojciech Nawrocki (Dec 03 2019 at 21:35):

Just came across this: Cedille Cast #9: Impredicativity, proof-irrelevance, and normalization

#### Chris Hughes (Jan 28 2020 at 23:21):

No idea if this is related or interesting, but I stumbled upon this failing to reduce as well. It reduces if I replace false with empty.

def not' (α : Sort*) := α → false

prefix  ¬' :40 := not'

def X {p : Type} : ¬' ¬' (¬' ¬' p → p) :=
assume h : ¬' (¬' ¬' p → p),
h (λ hnnp, (hnnp (λ hp : p, h (λ hnnp, hp))).elim)

#reduce X


#### ice1000 (Jun 29 2021 at 20:50):

What's Lean developers' attitude towards this counterexample of normalization

#### Mario Carneiro (Jun 29 2021 at 21:01):

This issue occurs in proof normalization, which is not something that matters in practice (we have made efforts to limit/deprecate things requiring proof normalization over time). It is still an open question whether well typed lean terms can cause nonterminating VM computations, which is what we really care about. In any case, it doesn't impact soundness which is what use in mathematics requires of the system.

#### Mario Carneiro (Jun 29 2021 at 21:06):

Even if VM computations could be made to loop, this is not a significant issue since you can already just turn off the termination checker and write meta code, and in practice most lean code written for execution is meta because the tactic monad is meta

#### Mario Carneiro (Jun 29 2021 at 21:11):

Also, this example is specifically invoking the normalizer (aka #reduce). It is not an issue in definitional equality checking which is what is needed by the kernel and implemented by external checkers. I don't know how to turn this example into a nonterminating defeq check, because defeq of propositions is trivial. Combined with the fact that "ideal" defeq in lean is already known to be undecidable for other reasons, it does not represent a significant change of the status quo.

#### Sebastian Ullrich (Jun 29 2021 at 21:12):

Mario Carneiro said:

Even if VM computations could be made to loop, this is not a significant issue since you can already just turn off the termination checker and write meta code, and in practice most lean code written for execution is meta because the tactic monad is meta

And also in practice there is not much difference between non-termination and very slow termination. Totality really is mostly interesting for soundness of reduction.

#### Mario Carneiro (Jun 29 2021 at 21:13):

The conventional wisdom on #reduce is already "it's stupidly slow and times out on all non-toy examples". A fun example is #reduce 'a'

Last updated: Aug 03 2023 at 10:10 UTC