¶Standardization theorem

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

[Kashima2000] A Proof of the Standardization Theorem in λ-Calculus

¶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.

[Sestini2018] Normalization by Evaluation for Typed Weak λ-Reduction