Library / Symbolic Computation
A normal form is an expression that cannot be rewritten any further by a chosen rule set. It is a local notion of completion, and it plays a major role in simplification, normalization, and symbolic reasoning.
If a rewrite system reaches an expression where none of its rules apply, that expression is in normal form with respect to that system. The important phrase is "with respect to that system." A normal form depends on the rule set and strategy you chose.
This is why normal forms are useful but also limited. They tell you that a given rewrite process has stopped, not necessarily that the expression is globally best or uniquely preferred.
A canonical form is usually meant to be a uniquely preferred representation among equivalent expressions. A normal form only says rewriting has stopped. If the system is not confluent, two different rewrite paths may lead to two different normal forms.
That distinction explains why people discuss normal forms together with confluence and termination.
A normal form gives a rewrite system an endpoint. That can make equivalence testing, simplification, and downstream symbolic work easier because the system is no longer carrying around arbitrary partially rewritten expressions.
If different rewrite orders lead to different irreducible expressions, then normal form is not yet a strong global guarantee. This is exactly the situation where confluence becomes important.
Many symbolic systems aim first for a reliable normal form before attempting more ambitious search. This can make simplification easier to reason about, reduce duplicate work, and create cleaner inputs for matching, solving, and verification. Even systems that later use richer equivalence structures often still rely on normalization as a helpful front-end step.
Normal forms connect directly to canonical forms, confluence, termination, and simplification strategy. Together these topics explain how symbolic systems decide when an expression is done.