Theory meeting, Nov. 13th

5 views
Skip to first unread message

Lyle Kopnicky

unread,
Oct 28, 2019, 2:00:59 AM10/28/19
to pdxfunc
Hi folks,

We're going through the MGS 2019 course on Lambda Calculus (http://www.duplavis.com/venanzio/mgs_lambda/index.html). For this meeting, please read the Lecture 4 slides and Chapters 6 and 7 of the draft book (linked from the above page).

Wednesday, November 13th, 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.

Ed Snow

unread,
Nov 13, 2019, 1:17:45 PM11/13/19
to pdxfunc
I apologize for the last-minute notice, but I'm going to have to be a no-show at tonight's meeting. I look forward to the next one.

-- Ed

Lyle Kopnicky

unread,
Nov 13, 2019, 9:25:32 PM11/13/19
to pdxfunc
No worries! We're just going over what we were planning on going over last time. See you next time!

Lyle Kopnicky

unread,
Nov 24, 2019, 10:48:42 PM11/24/19
to pdxfunc
We had an interesting meeting! We got through all the lecture slides, but didn’t get into the draft book material. We figured out a lot of things, but were left with some questions, which perhaps would be answered in the book.

Some things we couldn’t quite understand just from reading the slides:
  • How exactly does the lambda calculus implementation of the Ackermann-Péter function work?
  • We aren’t quite clear how the concepts of “introduction” and “elimination” apply with the typing rules for recursion and corecursion.
One additional thing I pointed out was that the functions ‘in’ and ‘out’ in recursion and corecursion do nothing - they are just there to make the typing rules work out. This is an example of isorecursive typing, as opposed to equirecursive, which wouldn’t have the ‘in’ and ‘out’ keywords. But isorecursive types are easier to implement in practice. Here’s a lecture about recursive types from Cornell: https://www.cs.cornell.edu/courses/cs4110/2012fa/lectures/lecture27.pdf.

I also explained the Haskell code that I wrote for last time, to implement Ed’s pairing operation for simply typed lambda calculus.

We decided to start working on the exercises for next time, but also go over the book material to see if we can answer some of our questions. Look for an announcement about the next meeting, on Dec. 11th.

- 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/3a74569e-e311-488c-80be-07aa0c91879d%40googlegroups.com.

Lyle Kopnicky

unread,
Nov 24, 2019, 10:52:18 PM11/24/19
to pdxfunc
Oh, I also pointed out that “strictly positive” functors are also called “covariant” functors.
Reply all
Reply to author
Forward
0 new messages