Good meeting! We first went over Chapter 4 of The Construction of Infinity. New topics were evaluation strategies and infinite streams. I wrote an example term in lambda calculus on the board, and showed how the different evaluation strategies produced different derivations:
We then went over our solutions for Exercises 2. I've attached my solutions to this email. For the first problem, I expanded out the example case of

to prove to myself that I had solved it correctly. For the second problem, I certainly didn't need to define the constructors/selectors, but you can see it's quite easy to do with the Scott encoding.
Ed had a slightly different solution for the second problem that was more efficient than mine, if you consider the lambda calculus as implemented on a real machine. Though the lambda calculus itself is timeless, if you want to count the number of reductions, my

solution would take
)
reductions, whereas Ed's would take
)
.
Finally, we went over something we didn't have time to get to in the previous meeting. Ed had come up with a way of defining the

function on Church lists that didn't use the Y combinator, while mine used the Y combinator. He demonstrated how one solution could be transformed into the other. Essentially, he was using the same concept, just formulated in a slightly different way.
See you on Sept. 25th!
- Lyle