Weak vs Strong Normalisation

What is Normalisation?

Normalisation means reducing a lambda expression until no more reductions are possible.

Normal form = The computation has finished.

An expression is weakly normalising if:

There exists at least one way to reduce it to a final result.

Practical Meaning:

Simple analogy:

"The program can finish, but only if you run it the right way."

An expression is strongly normalising if:

Every possible reduction path eventually terminates.

Practical Meaning:

Simple analogy:

"The program always finishes, no matter how you run it."

Feature	Weak Normalisation	Strong Normalisation
Termination Guarantee	Some strategies terminate	All strategies terminate
Risk of Infinite Loop	Possible	Impossible
Safety Level	Conditional	Guaranteed
Used In	General programming languages	Proof assistants & total languages

        Weak normalisation: A result exists, but evaluation order matters.

        Strong normalisation: Termination is guaranteed in all cases.

Score: 0 / 0