Theory meeting, 7/24/19, Lambda Calculus

Skip to first unread message

Lyle Kopnicky

Jul 18, 2019, 11:41:59 PM7/18/19
to pdxfunc
Hi folks,

We'll be going through the MGS 2019 course on Lambda Calculus ( To prepare for this meeting, you should read Chapter 3 of Constructing Infinity ( and try your hand at Exercise Sheet 1 ( We'll discuss our solutions in the meeting.

Wednesday, July 24th, 2018, 6:30-8:30pm

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

Jul 19, 2019, 6:01:27 PM7/19/19
to pdxfunc
I've attached my answers to Exercises 1.

There seems to be no shortage of online lambda-term evaluators. I came across one at that I've used to evaluate the lambda-terms I've assembled at Let me know if there is a preferred way to do this.
Exercises 1.pdf

Lyle Kopnicky

Jul 31, 2019, 2:24:30 AM7/31/19
to pdxfunc
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

Aug 14, 2019, 2:33:13 PM8/14/19
to pdxfunc
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).
Recursion Alternatives.pdf
Reply all
Reply to author
0 new messages