Definition

An object in an abstract reduction system is weakly normalizing if there exists a reduction sequence from to a normal form.

An entire system is weakly normalizing if every element has some reduction sequence leading to a normal form.

Remarks

Weak normalization says that a successful terminating strategy exists, but it does not say that every strategy terminates. This makes it strictly weaker than strong normalization.

In a confluent system, any two terminating reduction paths from the same object must end at the same normal form.

Strong Normalization
Normal Form
Confluence
Lambda Calculus

References

baader1998-term-rewriting