Theory of Lambda Calculi

Natural Numbers and Arithmetic

Learning Objectives

  • You understand Church encoding of booleans and natural numbers in lambda calculus.
  • You can implement boolean operators and arithmetic operations using Church encodings.
  • You can encode and decode data types between lambda calculus and host languages.
  • You understand how to build sugared syntax on top of lambda calculus.

Introduction

In this chapter, we will start exploring the surprising fact that lambda calculus has a lot of data types β€œhidden inside”. As a trivial example, abstractions in lambda calculus are exactly functions from functional programming. However, most would not consider functions to be data types, so what actual data types are definable in lambda calculus?

As it turns out, most of them: booleans, natural numbers, pairs, sum types, lists and algebraic data types in general. So lambda calculus is a surprisingly general and capable programming language.

We begin by learning about the Church encoding of the booleans, and then define natural numbers in lambda calculus. By the end of this chapter, we have a basically developed the language of conditional arithmetic on top of lambda calculus. You get to implement some of details like encoding and decoding Rust data types to and from lambda calculus.

In the next part, we will learn about recursion, which lambda calculus is also capable of!

As an excellent source for learning more, check out chapter 3 of Selinger: Lecture Notes on the Lambda Calculus.

Loading Exercise...

Church Encoded Booleans

Consider the following terms which are syntactically similar, but semantically quite different

π‘Ž)πœ†π‘₯.πœ†π‘¦.π‘₯𝑏)πœ†π‘₯.πœ†π‘¦.𝑦𝑐)πœ†π‘₯.π‘₯𝑑)πœ†π‘₯.𝑦

The first two terms (π‘Ž,𝑏) have the same shape, but are clearly different as the variable inside the inner abstraction refers to the first or the second argument respectively. The third 𝑐 is the identity function, which is distinct from the other three, although applying 𝑏 to anything gets us 𝑐. The fourth term 𝑑 is not closed, unlike the other three. It’s hard to say how 𝑑 should behave as its behavior depends on 𝑦.

Next, consider the following terms non-𝛼-equivalent terms

𝑒)πœ†π‘₯.π‘₯𝑓)(πœ†π‘₯.πœ†π‘₯.π‘₯)(πœ†π‘₯.π‘₯)

Notice that as 𝑓 𝛽-reduces to the identity function 𝑒, we consider the terms 𝛽-equivalent. 𝛽-equivalence is the characterization of having β€œsame behavior”1 with the condition that the terms normalize. We won’t study diverging terms as their (multi-step) 𝛽-reduction isn’t a total function.

Next, we try to analyze the behavior of π‘Ž,𝑏, as they have a special meaning when viewed from a certain perspective.

We begin by observing the the terms πœ†π‘₯.πœ†π‘¦.π‘₯ and πœ†π‘₯.πœ†π‘¦.𝑦 can be thought of as two-argument functions that return one of the two arguments. Observed from a type-theoretic perspective, the functions have the type 𝑇→𝑇→𝑇 for any type 𝑇. As it turns out, these two are the only two inhabitants of this type signature, up to 𝛽-equivalence.

This stems from the fact that the functions must be parametric in the generic type 𝑇, which means that they must not use any information about what 𝑇 can do. If 𝑇 was a function type, we could apply it to some term, but we cannot assume that 𝑇 is a function in general.

Another thing to note, the two functions must be closed to have a type, i.e. πœ†π‘₯.πœ†π‘¦.𝑧 does not have type 𝑇→𝑇→𝑇, or any type at all, if we know nothing about the type of 𝑧.

Hopefully you are somewhat convinced that these two terms are the only 𝛽-distinct inhabitants of the boolean-like type βˆ€π‘‡,𝑇→𝑇→𝑇, so we can name them as

trueβ‰”πœ†π‘₯.πœ†π‘¦.π‘₯falseβ‰”πœ†π‘₯.πœ†π‘¦.𝑦

Next, let’s think about what boolean operators would look like. We want to find a term that acts like the logical conjunction, a term and which satisfies the following β€œtruth table”

andtruetrue=𝛽trueandtruefalse=𝛽falseandfalsetrue=𝛽falseandfalsefalse=𝛽false

As true and false are normal forms, but and t1 t2 is not, the 𝛽-equivalence can be equivalently replaced with βŸΆβˆ—.

Based on the type of and, it should take two booleans and return a boolean, so we can start defining it with nested abstractions:

and=πœ†π‘1.πœ†π‘2.?

Next, we need to fill in the hole using a term which evaluates to true if both 𝑏1 and 𝑏2 behave like true. Let’s refine and further by writing πœ†π‘₯.πœ†π‘¦.? inside it.

and=πœ†π‘1.πœ†π‘2.πœ†π‘₯.πœ†π‘¦.?

Now the only thing to do is to return π‘₯, if both 𝑏1 and 𝑏2 are true, and 𝑦 otherwise. Think about how to accomplish this task for a moment and answer the following quiz.

Loading Exercise...

First, let’s try to use 𝑏1. If 𝑏1 is false, we would like to return 𝑦 as and false _ is always false. This is enough information to refine the function further.

and=πœ†π‘1.πœ†π‘2.πœ†π‘₯.πœ†π‘¦.𝑏1 ? 𝑦

If, on the other hand, 𝑏1 is true, we need to check 𝑏2 and return π‘₯ if 𝑏2 is also true, and 𝑦 otherwise. Therefore, the final hole can be filled with 𝑏2 π‘₯ 𝑦

and=πœ†π‘1.πœ†π‘2.πœ†π‘₯.πœ†π‘¦.𝑏1 (𝑏2 π‘₯ 𝑦) 𝑦

Let’s check the β€œtypes” to make sure we didn’t make a mistake. Consider that 𝑏1,𝑏2 have type 𝑇→𝑇→𝑇, for any 𝑇, and that π‘₯,𝑦 hav type π‘ˆ. The result of applying 𝑏2 to π‘₯ and 𝑦 results in a value of type π‘ˆ, and applying 𝑏1 to 𝑏2 π‘₯ 𝑦 and 𝑦 which are both of type π‘ˆ results again in π‘ˆ, so the type of and is

and::(βˆ€π‘‡,𝑇→𝑇→𝑇)β†’(βˆ€π‘‡,𝑇→𝑇→𝑇)β†’(βˆ€π‘ˆ,π‘ˆβ†’π‘ˆβ†’π‘ˆ)

We use the polymorphic type quantifier βˆ€π‘ˆ to indicate that and𝑏1 𝑏2 can be applied to two term of any type π‘ˆ to get π‘ˆ. The type of booleans in Church encoding is βˆ€π‘‡,𝑇→𝑇→𝑇, and we have checked that and indeed takes two (Church) booleans and returns a (Church) boolean.

Notice that the type βˆ€π‘ˆ,π‘ˆβ†’π‘ˆβ†’π‘ˆ is alpha-equivalent with βˆ€π‘‡,𝑇→𝑇→𝑇 as π‘ˆ and 𝑇 are bound type variables, and consistently renaming 𝑇 to π‘ˆ (or vice versa) gets us one from the other.

As the lambda calculus we are working with is untyped, the types here are for demonstration purposes only β€” implementing polymorphic type checking is outside the scope of the course.

Loading Exercise...

Church Encoded Natural Numbers

The next set of lambda terms we will study is the Church encoding of natural numbers also called Church numerals. The idea is simple, a Church numeral is an abstraction over two variables (like the boolean) but instead of returning either on directly, it applies the first iteratively to the second.

0β‰”πœ†π‘“.πœ†π‘₯.π‘₯1β‰”πœ†π‘“.πœ†π‘₯.𝑓π‘₯2β‰”πœ†π‘“.πœ†π‘₯.𝑓(𝑓π‘₯)π‘›β‰”πœ†π‘“.πœ†π‘₯.𝑓…(π‘“βŸπ‘›timesπ‘₯)

As there can be any positive number of (or zero) occurrences of the first argument, we have an infinite set of numerals.

To get an idea of how Church numerals behave, let’s use the following abstraction as 𝑓:

πœ†π‘₯.plus_oneπ‘₯

Here plus_one is simply a free variable with an unusual name. Next, consider what happens when we apply different numerals to this abstraction:

0(πœ†π‘₯.plus_oneπ‘₯)βŸΆπœ†π‘₯.π‘₯1(πœ†π‘₯.plus_oneπ‘₯)βŸΆπœ†π‘₯.(πœ†π‘₯.plus_oneπ‘₯)π‘₯βŸΆπœ†π‘₯.plus_oneπ‘₯

For larger numerals we get

2(πœ†π‘₯.plus_oneπ‘₯)βŸΆβˆ—πœ†π‘₯.plus_one(plus_oneπ‘₯)3(πœ†π‘₯.plus_oneπ‘₯)βŸΆβˆ—πœ†π‘₯.plus_one(plus_one(plus_oneπ‘₯))

If instead, we used the negation of Church booleans, i.e. notβ‰”πœ†π‘.𝑏falsetrue, we would get

1(πœ†π‘.𝑏falsetrue)βŸΆπœ†π‘₯.(πœ†π‘.𝑏falsetrue)π‘₯βŸΆπœ†π‘₯.π‘₯falsetrue

Which is again equal to the input not up to alpha equivalence. However, applying 2 to not (composing not with itself twice) results in

2(πœ†π‘.𝑏falsetrue)βŸΆπœ†π‘₯.(πœ†π‘.𝑏falsetrue)((πœ†π‘.𝑏falsetrue)π‘₯)βŸΆπœ†π‘₯.((πœ†π‘.𝑏falsetrue)π‘₯)falsetrueβŸΆπœ†π‘₯.(π‘₯falsetrue)falsetrue

Applying this to any Church boolean returns back the same boolean, so it’s like a complicated way to express the identity function on booleans.

Loading Exercise...
Loading Exercise...

Church Numeral Arithmetic

As you have learned, it’s possible to implement various boolean operators directly in lambda calculus. Next, we will look at some examples of arithmetic operators that work with Church numerals.

First, to compare a Church numeral 𝑛 with zero, we can use 𝑛 for primitive β€œcase matching”. If 𝑛=0, it returns its second argument, which should be true.

is_zero=πœ†π‘›.𝑛?true

And if 𝑛 is not zero, we need to return false so we use a constant function πœ†π‘₯.false in place of ?

is_zero=πœ†π‘›.𝑛(πœ†π‘₯.false)true

For example is_zero2 evaluates to

is_zero2=(πœ†π‘›.𝑛(πœ†π‘₯.false)true)2⟢2(πœ†π‘₯.false)true=(πœ†π‘“.πœ†π‘₯.𝑓(𝑓π‘₯))(πœ†π‘₯.false)true⟢(πœ†π‘₯.(πœ†π‘₯.false)((πœ†π‘₯.false)π‘₯))true⟢(πœ†π‘₯.false)((πœ†π‘₯.false)true)⟢(πœ†π‘₯.false)false⟢false

Other arithmetic operators are defined as follows

plusβ‰”πœ†π‘š.πœ†π‘›.πœ†π‘“.πœ†π‘₯.π‘šπ‘“(𝑛𝑓π‘₯)multβ‰”πœ†π‘š.πœ†π‘›.πœ†π‘“.πœ†π‘₯.π‘š(𝑛𝑓)π‘₯expβ‰”πœ†π‘š.πœ†π‘›.𝑛(π‘šplus)1

Have a look at the Wikipedia article: Church encoding for more concrete examples.

0 = false

Due to the decision to define false as πœ†π‘₯.πœ†π‘¦.𝑦 rather than the other way around, we notice that the set of Church encoded booleans and numerals intersect:

0=πœ†π‘“.πœ†π‘₯.π‘₯=false

As an exercise, think about if 1=true or not.

Unfortunately this intersection of the sets means that there isn’t a general decoding function from Church encoded terms as it would have to decide whether to decode πœ†π‘₯.πœ†π‘¦.𝑦 to an integer or a boolean.


Loading Exercise...
Loading Exercise...

Church Encoding as Sugar

As we now know how to define basic functions in Church numeral arithmetic, let’s design a programming language with sugared surface syntax which uses lambda calculus under the hood.

Loading Exercise...
Loading Exercise...
Loading Exercise...

Footnotes

Footnotes

  1. There is also an even more general version of β€œsame behavior” which combines 𝛽-equivalence with so called πœ‚-equivalence. πœ‚-equivalence expands equality between lambda terms to be extensional. For example the terms πœ†π‘¦.π‘₯ 𝑦 and π‘₯ are πœ‚-equivalent even though they are not 𝛽-equivalent. ↩

← Multiple Steps and Normalization
Extensions to Lambda Calculus →