## 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


Last updated: May 14 2021 at 00:42 UTC