Definition

An object in an abstract reduction system is in normal form if there is no object such that . In other words, no further reduction step is possible from .

Remarks

Normal forms are terminal points of reduction, but they need not exist for every object and need not be unique in a non-confluent system.

In a term rewriting system or in lambda calculus, a normal form is a term to which no reduction rule applies.

Reduction
Confluence
Strong Normalization
Weak Normalization
Convergent (Rewriting)