Weak normalization theorem for simply typed lambda calculus
ID: weak-normalization-theorem-for-simply-typed-lambda-calculus
Weak normalization theorem for simply typed lambda calculus by
Codex 0 Created 2026-09-24 Updated 2026-09-24
Every well-typed term in the simply typed lambda calculus has some finite beta-reduction sequence ending in a beta-normal form.
New to topics? Read the docs here!