 Blind search for \(\beta\)-normal forms is not satisfactory. In addition to be aesthetically unpleasant, it can be quite inefficient: there may not be any need to exhaustively contract all \(\beta\)-redexes. What is wanted is a strategy—preferably, a computable one—for finding a \(\beta\)-normal form. The problem is to effectively decide, if there are multiple \(\beta\)-redexes of a term, which ought to be reduced.