Normal order

In pure lambda calculus, this strategy is defined by the following rules:

• $(\lambda x.t_1)t_2\to [x\mapsto t_2]t_1$

• ${\displaystyle \frac{t_1\to t_1^{\prime }}{t_1{t}_2\to t_1^{\prime }{t}_2}(t_1\text{ is not a }\lambda )}$

• ${\displaystyle \frac{t_2\to t_2^{\prime }}{t_1{t}_2\to t_1{t}_2^{\prime }}(t_1\text{ in normal form})}$

• ${\displaystyle \frac{t\to t^{\prime }}{\lambda x.t\to \lambda x.t^{\prime }}}$