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!