Theory meeting, 9/11/19

5 views
Skip to first unread message

Lyle Kopnicky

unread,
Sep 6, 2019, 12:34:35 AM9/6/19
to pdxfunc
Hi folks,

We'll be going through the MGS 2019 course on Lambda Calculus (http://www.duplavis.com/venanzio/mgs_lambda/index.html). To prepare for this meeting, you should read Chapter 4 of Constructing Infinity (http://www.duplavis.com/venanzio/mgs_lambda/construction_infinity_chapter4.pdf) and try your hand at Exercise Sheet 2 (http://www.duplavis.com/venanzio/mgs_lambda/mgs-lambda-exercises2.pdf). We'll discuss our solutions in the meeting.

Wednesday, September 11th, 2019, 6:30-8:30pm

Location:
Collective Agency

3050 SE Division, Suite 245 · Portland, OR

We'll be in the second floor conference room, not in the Collective Agency suite. It's just off the lobby area in the middle of the second floor. Elevator access is available.


Lyle Kopnicky

unread,
Sep 23, 2019, 10:30:06 AM9/23/19
to pdxfunc
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:

IMG_8329.jpg

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 \mathsf{fact}\ \tilde{3} 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 \mathsf{depthFirst} solution would take O(n^2) reductions, whereas Ed's would take O(n).

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 \mathsf{length} 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

--
You received this message because you are subscribed to the Google Groups "pdxfunc" group.
To unsubscribe from this group and stop receiving emails from it, send an email to pdxfunc+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/pdxfunc/79675664-0d98-4dc0-a005-fe78bf15d169%40googlegroups.com.
exercises_2.pdf
Reply all
Reply to author
Forward
0 new messages