Weak Head Normalization

Stream: Type theory

[Cody Roux]

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.

[Mario Carneiro]

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

[Cody Roux]

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

[Mario Carneiro]

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