Theory meeting, 7/24/19, Lambda Calculus

[Lyle Kopnicky]

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 3 of Constructing Infinity (http://www.duplavis.com/venanzio/mgs_lambda/construction_infinity_chapter3.pdf) and try your hand at Exercise Sheet 1 (http://www.duplavis.com/venanzio/mgs_lambda/mgs-lambda-exercises1.pdf). We'll discuss our solutions in the meeting.

Wednesday, July 24th, 2018, 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.

RSVP at: https://www.meetup.com/Portland-Functional-Programming-Study-Group/events/hvmdfryzkbgc/

[Ed Snow]

I've attached my answers to Exercises 1.

There seems to be no shortage of online lambda-term evaluators. I came across one at https://crypto.stanford.edu/~blynn/lambda/ that I've used to evaluate the lambda-terms I've assembled at https://gist.github.com/es30/1edbf81fb19e92abcbc39ea3cebc37cd Let me know if there is a preferred way to do this.

[Lyle Kopnicky]

Thanks, Ed!

I've attached my answers to the first set of exercises.

In the meeting, we compared our answers.

I ended up using the Y combinator for recursion. It doesn't really seem fair, since we won't cover that until Lecture 2. But I didn't see any other way to write functions such as "length".

Ed came up with a solution which seems equivalent, but we didn't quite prove that equivalence. We did convince ourselves that both of our solutions are correct. Here was our attempt to reconcile them:

We ended up discussing the Scott encoding of lists, and of natural numbers. The Scott encoding works for any algebraic data type. The predecessor function is much easier to define than for the Church encoding:

I also showed how Church numerals can be written as Haskell functions, and readily decoded into Haskell Ints. However, writing type signatures for them got a little tricky. In some cases, it's better to let Haskell infer the type for you. In other cases, it won't work unless you specify the type. The central problem is that the lambda calculus is untyped, but we are being forced to specify types in Haskell.

We can define

    type Church t = (t -> t) -> (t -> t)

but sometimes the same Church numeral must be used at different instances of t. It may help to define it with a polymorphic data type:

    newtype Church = Church (forall t. (t -> t) -> (t -> t))

Yep... I tried that, and I stopped getting inscrutable types for my functions. Even the predecessor function is very simple, just

    churchPredAux :: Church -> (Church, Church)

    churchPredAux (Church n) = n (\x -> (snd x, churchSucc (snd x))) (churchZero, churchZero)

    churchPred :: Church -> Church

    churchPred = snd . churchPredAux

- Lyle

[Ed Snow]

On Tuesday, July 30, 2019 at 11:24:30 PM UTC-7, Lyle Kopnicky wrote:

Ed came up with a solution [to the "length" function in Exercise 1] which seems equivalent, but we didn't quite prove that equivalence.

Now armed with a better grasp on the Y combinator, I thought I'd give this another look (attached).