Definition
An object in an abstract reduction system is strongly normalizing if there is no infinite reduction sequence starting from . Equivalently, every reduction sequence beginning at eventually terminates.
A system is strongly normalizing if every element of it is strongly normalizing. In the rewriting literature this is often called termination.
Relation to Weak Normalization
Strong normalization is stronger than weak normalization. An object may admit some terminating reduction path while still having other reduction paths that continue forever.
Related Concepts
Weak Normalization
Normal Form
Confluence
Convergent (Rewriting)
Lambda Calculus