λ calculus

Standardization theorem

If a term has a normal form, normal-order reduction will find it.

Weak vs strong reduction systems

A strong reduction system allows redexs inside of abstractions. A weak one does not. Weak reduction is not confluent in the λ calculus.

_Extended_ weak reduction lets you reduce inside of an abstraction if the reduction does not refer to the bound variable. That is confluent.