# An operational semantics for lambda-calculus normal order evaluation strategy

Under the normal order strategy, the leftmost, outermost redex is always reduced first.

I understand this as a restriction of the full beta-reduction evaluation strategy, whose reduction rules are given as follows:

$$\frac{t_1 \to t_1'}{t_1 t_2 \to t_1' t_2}$$

$$\frac{t_2 \to t_2'}{t_1 t_2 \to t_1 t_2'}$$

$$\frac{t_1 \to t_1'}{λx. t_1 \to λx. t_1'}$$

$$\frac{(λx. t_1) t_2}{[x \to t_2] t_1}$$

My question is how to transform these rules so that the normal order strategy condition holds.

$$\frac{t_1 \longrightarrow t_1'}{t_1 t_2 \longrightarrow t_1' t_2}$$
$$(λx. t_1) t_2 \longrightarrow [x \mapsto t_2]t_1$$