Editing Lambda calculus (section)

== Normal forms and confluence ==
{{Further|Normalization property (abstract rewriting)}}
For the untyped lambda calculus, β-reduction as a [[rewrite system|rewriting rule]] is neither [[strongly normalising]] nor [[weakly normalising]].

However, it can be shown that β-reduction is [[confluence (abstract rewriting)|confluent]] when working up to α-conversion (i.e. we consider two normal forms to be equal if it is possible to α-convert one into the other).

Therefore, both strongly normalising terms and weakly normalising terms have a unique normal form. For strongly normalising terms, any reduction strategy is guaranteed to yield the normal form, whereas for weakly normalising terms, some reduction strategies may fail to find it.