Normal-order beta reduction
= Normal-order beta reduction
Normal-order beta reduction contracts the leftmost outermost <beta-redex>. If a <lambda term> has a <beta-normal form>, this strategy reaches it. It is useful for implementing <Church Boolean> conditionals because an unused branch can be discarded before it is evaluated.