Zulip Chat Archive

Stream: general

Topic: Normalization fails in lean


view this post on Zulip 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

view this post on Zulip Patrick Massot (Nov 18 2019 at 21:02):

Should we care?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.)

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Nov 18 2019 at 21:46):

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

view this post on Zulip Mario Carneiro (Nov 18 2019 at 21:47):

sadly there is no way to trace the reduction

view this post on Zulip Bryan Gin-ge Chen (Nov 18 2019 at 21:48):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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!

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

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

view this post on Zulip Mario Carneiro (Nov 20 2019 at 12:05):

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

view this post on Zulip Wojciech Nawrocki (Nov 20 2019 at 18:34):

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

view this post on Zulip 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"?

view this post on Zulip 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

view this post on Zulip 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...

view this post on Zulip 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

view this post on Zulip Wojciech Nawrocki (Dec 03 2019 at 21:35):

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

view this post on Zulip 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