TAPL book, page 56 reads:

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$

  • $\begingroup$ Your last rule evaluates under lambdas, which can cause otherwise terminating terms to diverge. Is this intentional? $\endgroup$
    – jmite
    Nov 7 '19 at 4:07
  • $\begingroup$ @jmite: You are right. The third rule should not exist. I missed the fact that lambda terms are normal $\endgroup$
    – Apoorv
    Nov 7 '19 at 22:31
  • $\begingroup$ (I would use the term "value" rather than "normal" in this case) $\endgroup$
    – cody
    Jul 30 at 19:41

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.