Solutions to in-class reductions (Feb 28, 2020)

---

Leftmost reduction

The leftmost reduction chooses the 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 leftmost 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.

---

Rightmost reduction

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

Note that the leftmost and rightmost 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 rightmost reduction diverges from the leftmost 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 rightmost reduction diverges from the leftmost reduction at this step.

---

Using the checker

If you want to try checking this reduction using the lambda calculus reduction checker, enter the expression as:

(((Lf.(Lx.(f(fx))))(Lz.((px)z)))t)

Note that, since the checker’s grammar does not support arithmetic expressions like (+ x z) or values, you will need to encode them to make it work. I encoded (+ x z) as ((px)z). I also encoded 2 as t. With a little thinking, you should be able to convince yourself that these encodings will have equivalent derivations.