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.


1 Answer 1


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$ Commented Nov 7, 2019 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
    Commented Nov 7, 2019 at 22:31
  • $\begingroup$ (I would use the term "value" rather than "normal" in this case) $\endgroup$
    – cody
    Commented Jul 30, 2021 at 19:41
  • $\begingroup$ I used the term normal as term rewriting normalizes or diverges. Values arise are when you want to talk about semantics and make a distinction between meaningful and garbage objects, which is not the focus of the question. $\endgroup$
    – Apoorv
    Commented Dec 9, 2021 at 5:10

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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