An operational semantics for lambda-calculus normal order evaluation strategy

Question

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.

Apoorv · Accepted Answer · 2019-11-07 22:32:06Z

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$

answered Nov 6, 2019 at 22:03

Apoorv

6596 silver badges15 bronze badges

$\begingroup$ Your last rule evaluates under lambdas, which can cause otherwise terminating terms to diverge. Is this intentional? $\endgroup$
– jmite
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
Nov 7, 2019 at 22:31
$\begingroup$ (I would use the term "value" rather than "normal" in this case) $\endgroup$
– cody
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
Dec 9, 2021 at 5:10

Add a comment |

1 Answer 1