 Normal form (abstract rewriting)

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.

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.