Notes on PL 14: Lambda Calculus Encodings

Lambda Calculus Encodings

Booleans

The pure -calculus contains only functions as values. It is not exactly easy to write large or interesting programs in the pure -calculus. We can however encode objects, such as booleans, and integers.

Let us start by encoding constants and operators for booleans. That is, we want to define functions TRUE, FALSE, AND, NOT, IF, and other operators that behave as expected. For example:

Let’s start by defining TRUE and FALSE:

Thus, both TRUE and FALSE are functions that take two arguments; TRUE returns the first, and FALSE returns the second. We want the function IF to behave like

The definitions for TRUE and FALSE make this very easy.

Definitions of other operators are also straightforward.

Church numerals

Church numerals encode a number as a function that takes and , and applies to times.

In the definition for SUCC, the expression applies to times (assuming that variable is the Church encoding of the natural number ). We then apply to the result, meaning that we apply to times.