# 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.

You can use the following rules:

$$\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$$

• Your last rule evaluates under lambdas, which can cause otherwise terminating terms to diverge. Is this intentional? – jmite Nov 7 '19 at 4:07
• @jmite: You are right. The third rule should not exist. I missed the fact that lambda terms are normal – Apoorv Ingle Nov 7 '19 at 22:31