 Definition A \(\beta\)-reduction strategy is a function whose domain is the set of all \(\lambda\)-terms and whose value on a term \(M\) not in \(\beta\)-normal form is a redex subterm of \(M\), and whose value on all terms M in \(\beta\)-normal form is simply \(M\).