Zulip Chat Archive

Stream: Type theory

Topic: Weak Head Normalization

view this post on Zulip Cody Roux (Jul 16 2020 at 13:41):

Very idle question: I understand that Strong Normalization and even Weak Normalization don't hold in the Lean type theory. But what about Weak Head Normalization for closed terms? Is this plausible at all? This obviously implies consistency, and probably isn't that useful otherwise, but it'd be nice to know anyways.

This doesn't help much in the presence of axioms obviouosly (though it'd be fun to see if the argument extends with various computational interpretations of them).

I'm not sure how one would go about proving this at any rate, but I think some of the standard techniques might apply.

view this post on Zulip Mario Carneiro (Jul 16 2020 at 21:38):

Wouldn't any weak normalization counterexample contain a weak head normalization counterexample if you find the appropriate point in it? In particular, the Abel-Coquand Omega tern does not head normalize

view this post on Zulip Cody Roux (Jul 16 2020 at 23:57):

Not on closed terms though! Otherwise I'm pretty sure you're in trouble...

view this post on Zulip Mario Carneiro (Jul 17 2020 at 01:47):

Ah, I see. Indeed this is in the category of "not falsified yet, plausibly true", along with VM termination on well typed closed terms

Last updated: May 18 2021 at 10:14 UTC