Normalization fails in lean

Stream: general

[Mario Carneiro]

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]

Should we care?

[Mario Carneiro]

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]

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]

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]

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]

(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]

In #reduce Omega -- timeout, Omega should be a lambda abstraction. Why does the reduction not stop there?

[Bryan Gin-ge Chen]

Are there options to control the number of steps #reduce takes? Is there any option to trace the reduction steps?

[Mario Carneiro]

#reduce will reduce the whole term to a normal form, it doesn't stop at whnf

[Mario Carneiro]

sadly there is no way to trace the reduction

[Bryan Gin-ge Chen]

How hard would it be to imitate the reduction in meta code?

[Mario Carneiro]

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]

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]

So the question of whether VM evaluation on a computable well typed term can run forever is still open

[Mario Carneiro]

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]

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]

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]

(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]

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]

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

example (f x) : lam f $$ x = f x := rfl

[Mario Carneiro]

However, it is still difficult to use this for actual computations, because they take place inside proof reduction, which is not something that lean will normally even do anyway. For example, the final example lam f $$ x = f x is a bit misleading, because even if I wrote lam f $$ x = f (f x) it would still be proved by rfl because both sides are proofs. The real demonstration that this encoding works is the observation that the LHS #reduces to the RHS:

variables (f : F) (x : D)
#reduce lam f $$ x -- f x

[Wojciech Nawrocki]

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

[Wojciech Nawrocki]

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]

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]

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

[Mario Carneiro]

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

[Wojciech Nawrocki]

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

[Chris Hughes]

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]

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

[Mario Carneiro]

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]

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]

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]

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]

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'

[Mario Carneiro]

Revisiting this old topic to add an important addendum: Above I claimed that this issue is limited to normalization of proofs, which only occurs in #reduce which is not used in practice. However, because subsingleton eliminators reduce proofs, we can actually use it to lift the counterexample to failure of normalization outside of proofs as well:

/-! Andreas-Abel construction of nontermination in proofs -/

def True' := ∀ p : Prop, p → p

def om : True' := fun A a =>
   @cast (True' → True') A (propext ⟨fun _ => a, fun _ => id⟩) <|
   fun z => z (True' → True') id z

def Om : True' := om (True' → True') id om

-- #reduce Om -- loops

/-! nontermination outside proofs: -/

inductive Foo : Prop where
  | mk : True' → Foo

def foo : Foo := Om _ (Foo.mk fun _ => id)

-- example : foo.recOn (fun _ => 1) = 1 := by rfl -- loops

So this is definitively a counterexample to strong normalization of lean, even with the restricted "algorithmic equality" judgment decided by the lean kernel.

[Mario Carneiro]

We can use any subsingleton eliminator in place of Foo, not just Acc but even And is affected:

def foo : And True True := Om _ ⟨trivial, trivial⟩

example : foo.recOn (fun _ _ => 1) = 1 := by rfl -- loops

[Mario Carneiro]

(although one has to be careful with these examples because some of them also loop in the elaborator, which is not supposed to be under test here)