Lambda Calculus & Encodings

History

Alonzo Church introduced the Lambda Calculus was in the early 1930s as part of an investigation into the foundations of mathematics.

* 1935 Stephen Kleene and J. Barkley Rosser proved the original version was logically inconsistent. * 1936 Developed the untyped lambda calculus. * 1940 Developed the simply-typed lambda calculus.

Essence of the Kleene–Rosser paradox is, roughly, “If this sentence is true, Harvey Mudd College is located in England”.

Recalling Key Ideas from the Video

• The Lambda Calculus is a way of defining functions.
• The Lambda Calculus is comprises only functions. There are no booleans, numbers, arithmetic operations, etc.

Concrete Syntax

Names for things

$\alpha$-equivalence

If we can change the variable of a lambda expression without changing the meaning, then the resulting expression is said to be $\alpha$-equivalent to the former. So $(\lambda x. x)$ is $\alpha$-equivalent to $(\lambda y. y)$.

Beware of binding or un-binding variables. For example, $(\lambda x. x + y)$ is not $\alpha$-equivalent to $(\lambda y. y + y)$. This is because in the former expression $y$ is a free variable, but in in the latter expression it is a bound variable. You can see this difference when we apply apply these functions to an expression. We see that $((\lambda x. x + y) 3) \to_\beta 3 + y$, but $((\lambda y. y + y) 3) \to_\beta 6$.

A lambda function with only bounded parameters is called a closed lambda function. For example, $(\lambda x. x)$ is a closed lambda function. A lambda function in which the variables are free is called an open lambda function. For example, $x$ is an open lambda function.

The Rule that Matters Most: β-reduction

$\beta$-reduction \[ ((\lambda x.M)\;N) \qquad \to_\beta \qquad M[x\mapsto N] \]

A β-redex (or just redex) is a (sub)expression that can be reduced by β-reduction. A lambda expression with no $\beta$-redexes is in normal form.

Note: $M[x\mapsto N]$ means “replace all (free!) occurrences of $x$ with $N$”, thus

• $((x \; y) \; z)[x \mapsto \heartsuit] = ((\heartsuit \; y) \; z)$
• $(\lambda x. ((x \; y) \; z))[z \mapsto \clubsuit] = (\lambda x. ((x\; y)\; \clubsuit))$

But...

• $(\lambda x.((x \; y) \; z))[x \mapsto \spadesuit] = (\lambda x.((x \; y) \; z))$

$\textbf{NOTE}$:We don't replace variables of the same name bound by inner lambdas while doing $\beta$-reduction.

When we can no longer $\beta$-reduce an expression, we say that an expression is in normal form. Some expressions don't have a normal form, for example the $\omega$ combinator (note that you likely don't need to know this combinator, unless it's mentioned later in the class) when applied to itself

\[ (\lambda x. (x \, x)) (\lambda x. (x \, x))\]

reduces to itself

\[ (\lambda x. (x \, x)) (\lambda x. (x \, x)) \to_\beta (\lambda x. (x \, x)) (\lambda x. (x \, x))\].

We can still do $\beta$-reductions on this expression, but we won't get anywhere, so we can't say that this expression has a normal form.

Currying

Currying is the act of representing multi-argument functions as nested single-argument functions.

(We'll suppose for a moment that somehow we have numbers and operators like addition, even though really we don't.)

A simple function

\[ (\lambda y. 7 + y) \]

Consider we have

\[ ((\lambda y. 7+y) 3) \to_\beta 7+3 \to_+ 10 \]

We can generalize it

\[ (\lambda x.(\lambda y. x + y)) \]

This is a function that returns a function. However, we can also view it as a function that takes in two arguments.

Consider applying this to 7:

\[ \begin{eqnarray} & & ((\lambda x.(\lambda y. x + y)) \; 7) \\\ & \to_\beta \qquad & (\lambda y. 7 + y) \end{eqnarray} \]

and similarly

\[ \begin{eqnarray} & & (((\lambda x.(\lambda y. x + y)) \; 7) \; 4) \\\ & \to_\beta \qquad & ((\lambda y. 7 + y) \; 4) \\\ & \to_\beta \qquad & 7 + 4 \end{eqnarray} \]

Currying isn't really as scary as it sounds: it is essentially just a complicated way of taking more than one parameter. The lambda calculus wasn't exactly defined with programming in mind, so we have to make do with the most primitive way of having multiple parameters. It may help to think of expressions like \[(\lambda x. (\lambda y. (\lambda z. ((x \, z) y))))\] as a single lambda, e.g. \[(\lambda x, y, z. ((x \, z) y))\] even though this is incorrect syntax.

As inconvenient as it is, currying does have a nice benefit: partial application. Since we apply terms one-at-a-time, defining specific functions like \[\text{PlusFour} := (\lambda x. (x + 4))\] isn't necessary, since if we have a more general function like \[\text{Plus} := (\lambda x. (\lambda y. (x + y)))\] we can instead just do \[\text{PlusFour} := (\text{Plus} \, 4)\] Convenient, huh?

Note: While $\beta$-reduction generally simplifies functions, it can sometimes make them more complex. Consider the following curried function: \[ ((\lambda x. ((x \text{ } x) x)) (\lambda x. ((x \text{ } x) x))) \] After one $\beta$-reduction, we get the following result: \[ (((\lambda x. ((x \text{ } x) x)) (\lambda x. ((x \text{ } x) x))) (\lambda x. ((x \text{ } x) x))) \] Further $\beta$-reductions will simply increase the number of nested $(\lambda x. ((x \text{ } x) x))$'s that appear.

There may be multiple steps which can be $\beta$-reduced first. Reducing starting from the outside and moving in guarantees that if there is a normal form, you fill find it. For instance, the expression $((\lambda x. \text{False})((\lambda x. ((x \text{ } x) x)) (\lambda x. ((x \text{ } x) x))))$ leads to a never-ending string of $\beta$ reductions if the right-hand expression is reduced first. If the left-hand expression is reduced first, you observe that $(\lambda x. False)$ only ever returns False, meaning the entire expression reduces to False.

Note On Variable Scope

Think about how we might evaluate the following expression. \[ \begin{eqnarray} & & (((\lambda x.(\lambda x. x+x)) \; 17 ) \; 21 ) \\\ \end{eqnarray} \]

This expression might seem ambiguous, as it not clear to which $\lambda x$ is $x+x$ bound to. We can break the ambiguity by following this rule: Variables are bound by the innermost expression. Less formally, we could say that "x is always bound to the closest lambda".

\[ \begin{eqnarray} & & (((\lambda x.(\lambda x. x+x)) \; 17 ) \; 21 )\\\ & \to_\beta \qquad & ((\lambda x. x+x) \; 21) \\\ & \to_\beta \qquad & 21 + 21 \end{eqnarray} \]

Encodings

To program in the λ-calculus we need expressions that “act like”

• Booleans
• Numbers
• Conditionals
• Arithmetic operations
• Pairs and projections

Designing an Encoding

Tough, but you can do it.

You need to consider

• What it's used for
• How its used
• How you can make it all out of functions

You have to solve all these pieces all at once...

Booleans

How could we represent booleans?

Ask yourself

• What are booleans used for
• How could you use booleans do that, if booleans were functions
• How to write the λ-calculus functions to do what you need

We use booleans for if statements, so we will encode the ability to make if/else statements in booleans.

What Do Booleans Do, At Their Core?

Booleans are normally used for conditionals. \[\mathrm{\bf if}\;b\;\mathrm{\bf then}\;A\;\mathrm{\bf else}\;B\] In $\lambda$-calculus, we can write it as \[((b\;A)\;B)\] where $A$ is the True case, and $B$ is the False case.

Encoding Booleans

\[ \begin{eqnarray} \mathrm{TRUE} & \triangleq & (\lambda x.(\lambda y.x)) \\\ \mathrm{FALSE} & \triangleq & (\lambda x.(\lambda y.y)) \end{eqnarray} \]

NOT, AND and OR

From these definitions, we can construct functions which take in booleans and apply the same sort of boolean logic to spit out new functions!

\[ \begin{eqnarray} \mathrm{NOT} & \triangleq & (\lambda b.((b \ \mathrm{FALSE})\ \mathrm{TRUE}))\\\ \mathrm{AND} & \triangleq & (\lambda b.(\lambda c.(b\ c)\ \mathrm{FALSE}))\\\ \mathrm{OR} & \triangleq & (\lambda b.(\lambda c.(b \ \mathrm{TRUE})\ c))\\\ \end{eqnarray} \]

These aren't the only possible definitions, for example

\[ \begin{eqnarray} \mathrm{NOT} & \triangleq & (\lambda b.(\lambda t .(\lambda f . ((b f) t))))) \end{eqnarray} \]

How did we come up with these definitions? A good approach is to first try to implement them using tools that are more familiar to us, like python code. For example, while trying to encode AND, we can first try to code it only using "if ... then" statements. A posible solution does the following:

def and(m, n): if m: return n else: return false

Hopefully, with this implementation of AND it becomes more clear what we could do to write it in $\lambda$-calculus. We know we will need a curried function that will take two booleans, and it must choose between return the second or FALSE.

Pairs

It would also be useful be able to create pairs. In math notation we'd say $(3, 7)$ for a pair of 3 and 7, but in the lambda calculus we can't say that—all we have are functions. So instead we'll have to say $\mathrm{PAIR} \; 3 \; 7$ as our way to make a pair, where $\mathrm{PAIR}$ is a suitably chosen lambda expression. (We could have also called the function $\mathrm{MAKEPAIR}$ since it's a function for creating pairs.)

We'll have to figure out what our $\mathrm{PAIR}$ function should return—obviously it needs to return some kind of lambda function.

A pair is a function.

What you can't say

Some students might be tempted to write

\[ \begin{eqnarray} \mathrm{PAIR} & \triangleq & (\lambda x.(\lambda y. (x, y))) \\\ \end{eqnarray} \]

But that's not allowed because $(x, y)$ isn't valid lambda calculus!

Some others might try

\[ \begin{eqnarray} \mathrm{PAIR} & \triangleq & (\lambda x.(\lambda y.(x\ y)))) \\\ \end{eqnarray} \]

But that wouldn't work either! If we did this, it would pass $y$ as an argument to $x$ (i.e., in this version if we tried to pair a pig and a cow, it'd give the cow to the pig as its argument, presumably causing the pig to eat the cow).

What we want

A pair is supposed to be something that gathers together holds two distinct things, and then lets you get at either of them when you need to. So a pair needs to have a way to retrieve the first part and second part of the pair. For some pair $p$, $\mathrm{FST}\ p$ should give us the first thing in the pair, and $\mathrm{SND} p$ should give us the second thing.

Mathematically, we'd say that this is what we want:

\[ \begin{eqnarray} (\mathrm{FST} \; ((\mathrm{PAIR} \; \heartsuit) \; \clubsuit)) \to^*_\beta \heartsuit \\\ (\mathrm{SND} \; ((\mathrm{PAIR} \; \heartsuit) \; \clubsuit)) \to^*_\beta \clubsuit \\\ \end{eqnarray} \]

How we'll do it

We have to figure out what lambda expressions to use for $\mathrm{PAIR}$, $\mathrm{FIRST}$ and $\mathrm{SECOND}$ so that the above code works.

We will encode a pair $(x, y)$ as a function that takes in a boolean and returns $x$ if the boolean is TRUE and $y$ if the boolean is FALSE.

In other words, our representation of the pair of $(\heartsuit, \clubsuit)$ should be

\[ (\lambda b. ((b\ \heartsuit)\ \clubsuit)) \]

As usual, this is a function. What would you pass to this function to get it to β-reduce to $\heartsuit$ and what would you pass it to get it to β-reduce to $\clubsuit$?

You pass it $\mathrm{TRUE}$ and $\mathrm{FALSE}$ respectively. For example,

\[ \begin{eqnarray} & & ((\lambda b. ((b\ \heartsuit)\ \clubsuit))\ \mathrm{TRUE}) \\\ & \equiv \qquad & (\lambda b.((b\ \heartsuit)\ \clubsuit)) (\lambda t.(\lambda f.t)) \\\ & \to_\beta \qquad & (((\lambda t.(\lambda f.t))\ \heartsuit)\ \clubsuit) \\\ & \to_\beta \qquad & ((\lambda f. \heartsuit)\ \clubsuit) \\\ & \to_\beta \qquad & \heartsuit \\\ \end{eqnarray} \]

So, how would we write $\mathrm{PAIR}$, $\mathrm{FIRST}$ and $\mathrm{SECOND}$?

Remember:

• $\mathrm{PAIR}$ is our function for making a pair value. It should take two arguments, $x$ and $y$, and return our encoding for pairs. Thus, we want: \[ \mathrm{PAIR}\ \spadesuit\ \diamondsuit \to \lambda b. b\ \spadesuit\ \diamondsuit \]
• $\mathrm{FST}$ is our function for getting the lefthand part from a pair value. It should take one argument, $p$ (the pair value), and return the first part of the pair. Thus, we want: \[ \mathrm{FST}\ (\lambda b. b\ \spadesuit\ \diamondsuit) \to \spadesuit \]
• $\mathrm{SND}$ is our function for getting the righthand part from a pair value. It should take one argument, $p$ (the pair value), and return the second part of the pair. Thus, we want: \[ \mathrm{SND}\ (\lambda b. b\ \spadesuit\ \diamondsuit) \to \diamondsuit \]

\[ \begin{eqnarray} \mathrm{PAIR} & \triangleq & (\lambda x.(\lambda y.(\lambda b.((b\ x)\ y)))) \\\ \mathrm{FST} & \triangleq & (\lambda p. (p\ \mathrm{TRUE}))\\\ \mathrm{SND} & \triangleq & (\lambda p. (p\ \mathrm{FALSE}))\\\ \end{eqnarray} \]

-- MelissaONeill - 29 Jan 2020