Normal form (abstract rewriting)
= Normal form
{disambiguate=abstract rewriting}
{wiki}
An expression in <normal form (abstract rewriting)> 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.