Skip to main content
OverflowAI is here! AI power for your Stack Overflow for Teams knowledge community. Learn more

Questions tagged [normalization]

The tag has no usage guidance.

Filter by
Sorted by
Tagged with
16 votes
3 answers
1k views

Can we prove weak normalization for System F by induction on a transfinite ordinal

Weak normalization for the simple typed lambda calculus can be proved (Turing) by induction on $\omega^2$. An extended lambda calculus with recursors on natural numbers (Gentzen) has a weak ...
user avatar
16 votes
1 answer
584 views

Are innermost reductions perpetual in untyped λ-calculus?

(I have already asked this at MathOverflow, but got no answers there.) Background In the untyped lambda calculus, a term may contain many redexes, and different choices about which one to reduce may ...
kow's user avatar
  • 163
6 votes
1 answer
659 views

Strong normalization property of CoC inside CoC

Wikipedia says that The CoC is strongly normalizing, although, by Gödel's incompleteness theorem, it is impossible to prove this property within the CoC since it implies inconsistency. Why is ...
amakarov's user avatar
  • 163
2 votes
1 answer
532 views

Is there a formalization of normalization of impredicative system F?

In particular Agda seems not strong enough to prove that. Is the predicative Calculus of Inductive Constructions universes (Coq without Prop) sufficient? How about with the impredicative Prop?
Łukasz Lew's user avatar
  • 1,187