Solutions to in-class reductions (Feb 24, 2022)

---

These are the same reductions as shown in the video, but they’re a little more careful about writing every step.

Normal order reduction: outermost, leftmost

The normal order reduction chooses the outermost, leftmost reducible expression (aka, redex) to beta-reduce. If you are having trouble finding redexes, try drawing the expression’s abstract syntax tree, as shown in class. For the normal order redex, look for the uppermost, leftmost application that has an abstraction as its left child.

1.	(λf.λx.f(f x)) (λz.(+ x z)) 2	given
2.	(λf.λa.[a/x]f(f x)) (λz.(+ x z)) 2	alpha reduce x with a†
3.	(λf.λa.f(f a)) (λz.(+ x z)) 2	do substitution
4.	([(λz.(+ x z))/f]λa.f(f a)) 2	beta reduce f with (λz.(+ x z))★
5.	(λa.(λz.(+ x z)) ((λz.(+ x z)) a)) 2	do substitution
6.	([2/a](λz.(+ x z)) ((λz.(+ x z)) a))	beta reduce a with 2
7.	((λz.(+ x z)) ((λz.(+ x z)) 2))	do substitution and eliminate parens
8.	(λb.[b/z](+ x z)) ((λz.(+ x z)) 2)	alpha reduce z with b‡
9.	(λb.(+ x b)) ((λz.(+ x z)) 2)	do substitution
10.	([((λz.(+ x z)) 2)/b](+ x b))	beta reduce b with ((λz.(+ x z)) 2)
11.	((+ x ((λz.(+ x z)) 2)))	do substitution and eliminate parens
12.	(+ x (([2/z](+ x z))))	beta reduce z with 2
13.	(+ x (((+ x 2))))	do substitution and eliminate parens
14.	(+ x (+ x 2))	done

★ Don't forget that when we see an expression of the form <expr><expr><expr>, we interpret it as (<expr><expr>)<expr> because application is left associative.

† We alpha reduce the bound variable x on the left because there is a free variable x on the right. We can choose any variable we want, so I chose a.

‡ We alpha reduce the bound variable z on the left because there is another bound variable z on the right. This step is not strictly necessary, but we do it because we're people, and people get confused easily. We can choose any variable we want, so I chose b.

---

Applicative order reduction: innermost, rightmost

The applicative order reduction chooses the innermost, rightmost redex to beta-reduce. If you draw the expression’s abstract syntax tree, the applicative order redex corresponds with the lowermost, rightmost application that has an abstraction as its left child.

Note that the normal order and applicative order reductions start out the same way because, in the beginning, there is only one reducible subexpression. Partway through the reduction (step 6), there are two redexes, and the applicative order reduction diverges from the normal order reduction.

1.	(λf.λx.f(f x)) (λz.(+ x z)) 2	given
2.	(λf.λa.[a/x]f(f x)) (λz.(+ x z)) 2	alpha reduce x with a
3.	(λf.λa.f(f a)) (λz.(+ x z)) 2	do substitution
4.	([(λz.(+ x z))/f]λa.f(f a)) 2	beta reduce f with (λz.(+ x z))
5.	(λa.(λz.(+ x z)) ((λz.(+ x z)) a)) 2	do substitution
6.	(λa.(λz.(+ x z)) (([a/z](+ x z)))) 2	beta reduce z with a†
7.	(λa.(λz.(+ x z)) (((+ x a)))) 2	do substitution and eliminate parens
8.	(λa.([(+ x a)/z](+ x z))) 2	beta reduce z with (+ x a)
9.	(λa.((+ x (+ x a)))) 2	do substitution and eliminate parens
10.	([2/a](+ x (+ x a)))	beta reduce a with 2
11.	((+ x (+ x 2)))	do substitution and eliminate parens
12.	(+ x (+ x 2))	done

† The applicative order reduction diverges from the normal order reduction at this step.