An expression in normal form admits no further reductions. A term is strongly normalizing when every reduction sequence from it terminates; weak normalization requires only one terminating sequence. Strong normalization theorem for simply typed lambda calculus establishes the stronger property for well-typed terms.
This theorem establishes strong normalization in the normal form sense. Every well-typed simply typed lambda term admits no infinite beta-reduction sequence.
Articles by others on the same topic
In the context of abstract rewriting systems, "normal form" refers to a state in which an expression (or term) cannot be rewritten or simplified any further according to the rules of the rewriting system. This means that no applicable rewrite rules can be applied to the expression to produce a different expression. ### Key Concepts: 1. **Abstract Rewriting Systems**: These involve a set of expressions (terms) and a set of rewrite rules that describe how one expression can be transformed into another.