# Lambda Calculus

Probably has lots of features:

• Assignment (`x = x + 1`)
• Booleans, integers, characters, strings, …
• Conditionals
• Loops
• `return`, `break`, `continue`
• Functions
• Recursion
• References / pointers
• Objects and classes
• Inheritance

Which ones can we do without?

What is the smallest universal language?

## What is computable?

### Before 1930s

Informal notion of an effectively calculable function: can be computed by a human with pen and paper, following an algorithm

### 1936: Formalization

What is the smallest universal language? Alan Turing Alonzo Church

The Lambda Calculus

## The Next 700 Languages Peter Landin

Whatever the next 700 languages turn out to be, they will surely be variants of lambda calculus.

Peter Landin, 1966

## The Lambda Calculus

Has one feature:

• Functions

No, really:

• Assignment (`x = x + 1`)
• Booleans, integers, characters, strings, …
• Conditionals
• Loops
• `return`, `break`, `continue`
• Functions
• Recursion
• References / pointers
• Objects and classes
• Inheritance
• Reflection

More precisely, all you can do is:

• define a function
• call a function

## Describing a Programming Language

• Syntax: what do programs look like?
• Semantics: what do programs mean?
• operational semantics: how do programs execute step-by-step?

## Syntax: What Programs Look Like

``````E ::= x
| \x -> E
| E1 E2``````

Programs are expressions `E` (also called λ-terms) of one of three kinds:

• Variable
• `x`, `y`, `z`
• Abstraction (aka nameless function definition)
• `\x -> E`
• `x` is the formal parameter, `E` is the body
• “for any `x` compute `E`
• Application (aka function call)
• `E1 E2`
• `E1` is the function, `E2` is the argument
• in your favorite language: `E1(E2)`

(Here each of `E`, `E1`, `E2` can itself be a variable, abstraction, or application)

## Example Expressions

``````apple               -- Variable named "apple"

apple banana        -- Application of variable "apple"
-- to variable "banana"

\x -> x             -- The identity function
-- ("for any x compute x")

(\x -> x) apple     -- Application of the identity function
-- to variable "apple"

\x -> (\y -> y)     -- A function that returns the identity function

\f -> f (\x -> x)   -- A function that applies its argument
-- to the identity function``````

## QUIZ

Which of the following terms are syntactically incorrect?

A. `\(\x -> x) -> y`

B. `\x -> x x`

C. `\x -> x (y x)`

D. A and C

E. all of the above

## Examples

``````\x -> x             -- The identity function
-- ("for any x compute x")

\x -> (\y -> y)     -- A function that returns the identity function

\f -> f (\x -> x)   -- A function that applies its argument
-- to the identity function``````

How do I define a function with two arguments?

• e.g. a function that takes `x` and `y` and returns `y`?

``````\x -> (\y -> y)     -- A function that returns the identity function
-- OR: a function that takes two arguments
-- and returns the second one!``````

How do I apply a function to two arguments?

• e.g. apply `\x -> (\y -> y)` to `apple` and `banana`?

``````(((\x -> (\y -> y)) apple) banana) -- first apply to apple,
-- then apply the result to banana``````

## Syntactic Sugar

`\x -> (\y -> (\z -> E))` `\x -> \y -> \z -> E`
`\x -> \y -> \z -> E` `\x y z -> E`
`(((E1 E2) E3) E4)` `E1 E2 E3 E4`

``````\x y -> y     -- A function that that takes two arguments
-- and returns the second one...

(\x y -> y) apple banana -- ... applied to two arguments``````

## Semantics : What Programs Mean

How do I “run” / “execute” a λ-term?

Think of middle-school algebra:

``````-- Simplify expression:

(x + 2)*(3x - 1)
=> -- RULE: mult. polynomials
3x^2 - x + 6x - 2
3x^2 + 5x - 2 -- no more rules to apply  ``````

Execute = rewrite step-by-step following simple rules, until no more rules apply

## Rewrite Rules of Lambda Calculus

1. α-step (aka renaming formals)
2. β-step (aka function call)

But first we have to talk about scope

## Semantics: Scope of a Variable

The part of a program where a variable is visible

In the expression `\x -> E`

• `x` is the newly introduced variable

• `E` is the scope of `x`

• any occurrence of `x` in `\x -> E` is bound (by the binder `\x`)

For example, `x` is bound in:

``````  \x -> x
\x -> (\y -> x)``````

An occurrence of `x` in `E` is free if it’s not bound by an enclosing abstraction

For example, `x` is free in:

``````  x y                -- no binders at all!
\y -> x y          -- no \x binder
(\x -> \y -> y) x  -- x is outside the scope of the \x binder;
-- intuition: it's not "the same" x``````

## QUIZ

In the expression `(\x -> x) x`, is `x` bound or free?

A. bound

B. free

C. first occurrence is bound, second is free

D. first occurrence is bound, second and third are free

E. first two occurrences are bound, third is free

## Free Variables

A variable `x` is free in `E` if there exists a free occurrence of `x` in `E`

We can formally define the set of all free variables in a term like so:

``````FV(x)       = {x}
FV(\x -> E) = FV(E) \ {x}
FV(E1 E2)   = FV(E1) + FV(E2)``````

## Closed Expressions

If `E` has no free variables it is said to be closed

• Closed expressions are also called combinators

What is the shortest closed expression?

Answer: `\x -> x`

## Rewrite Rules of Lambda Calculus

1. α-step (aka renaming formals)
2. β-step (aka function call)

## Semantics: β-Reduction

``  (\x -> E1) E2   =b>   E1[x := E2]``

where `E1[x := E2]` means “`E1` with all free occurrences of `x` replaced with `E2`

Computation by search-and-replace:

• If you see an abstraction applied to an argument, take the body of the abstraction and replace all free occurrences of the formal by that argument

• We say that `(\x -> E1) E2` β-steps to `E1[x := E2]`

## Examples

``````(\x -> x) apple
=b> apple``````

``````(\f -> f (\x -> x)) (give apple)
=b> give apple (\x -> x)``````

## QUIZ

``````(\x -> (\y -> y)) apple
=b> ???``````

A. `apple`

B. `\y -> apple`

C. `\x -> apple`

D. `\y -> y`

E. `\x -> y`

## QUIZ

``````(\x -> x (\x -> x)) apple
=b> ???``````

A. `apple (\x -> x)`

B. `apple (\apple -> apple)`

C. `apple (\x -> apple)`

D. `apple`

E. `\x -> x`

## A Tricky One

``````(\x -> (\y -> x)) y
=b> \y -> y``````

Is this right?

## Something is Fishy

``````(\x -> (\y -> x)) y
=b> \y -> y``````

Is this right?

Problem: the free `y` in the argument has been captured by `\y`!

Solution: make sure that all free variables of the argument are different from the binders in the body.

## Capture-Avoiding Substitution

We have to fix our definition of β-reduction:

``  (\x -> E1) E2   =b>   E1[x := E2]``

where `E1[x := E2]` means `E1` with all free occurrences of `x` replaced with `E2`

• `E1` with all free occurrences of `x` replaced with `E2`, as long as no free variables of `E2` get captured
• undefined otherwise

Formally:

``````x[x := E]            = E
y[x := E]            = y            -- assuming x /= y
(E1 E2)[x := E]      = (E1[x := E]) (E2[x := E])
(\x -> E1)[x := E]   = \x -> E1     -- why do we leave `E1` alone?
(\y -> E1)[x := E]
| not (y in FV(E)) = \y -> E1[x := E]
| otherise         = undefined    -- wait, but what do we do then???``````

Answer: We leave `E1` above alone even though it might contain `x`, because in `\x -> E1` every occurrence of `x` is bound by `\x` (hence, there are no free occurrences of `x`)

## Rewrite Rules of Lambda Calculus

1. α-step (aka renaming formals)
2. β-step (aka function call)

## Semantics: α-Renaming

``````  \x -> E   =a>   \y -> E[x := y]
where not (y in FV(E))``````

• We can rename a formal parameter and replace all its occurrences in the body

• We say that `\x -> E` α-steps to `\y -> E[x := y]`

Example:

``\x -> x   =a>   \y -> y   =a>    \z -> z``

All these expressions are α-equivalent

What’s wrong with these?

``````-- (A)
\f -> f x    =a>   \x -> x x``````

Answer: it violates the side-condition for α-renaming that the new formal (`x`) must not occur freely in the body

``````-- (B)
(\x -> \y -> y) y   =a>   (\x -> \z -> z) z``````

Answer: we should only rename within the body of the abstraction; the second `y` is a free variable, and hence must remain unchanged

``````-- (C)
\x -> \y -> x y   =a>    \apple -> \orange -> apple orange``````

Answer: it’s fine, but technically it’s two α-steps and not one

## The Tricky One

``````(\x -> (\y -> x)) y
=a> (\x -> (\z -> x)) y
=b> \z -> y``````

To avoid getting confused, you can always rename formals, so that different variables have different names!

## Normal Forms

A redex is a λ-term of the form

`(\x -> E1) E2`

A λ-term is in normal form if it contains no redexes.

## QUIZ

Which of the following term are not in normal form ?

A. `x y`

B. `(\x -> x) y`

C. `x (\y -> y)`

D. `z ((\x -> x) y)`

E. B and D

## QUIZ

How many redexes does this expression have?

`(\f -> (\x -> x) f) (\x -> x)`

A. 0

B. 1

C. 2

D. 3

E. 4

## Semantics: Evaluation

A λ-term `E` evaluates to `E'` if

1. There is a sequence of steps

``E =?> E_1 =?> ... =?> E_N =?> E'``

where each `=?>` is either `=a>` or `=b>` and `N >= 0`

1. `E'` is in normal form

## Examples of Evaluation

``````(\x -> x) apple
=b> apple``````

``````(\f -> f (\x -> x)) (\x -> x)
=b> (\x -> x) (\x -> x)
=b> \x -> x``````

``````(\x -> x x) (\x -> x)
=b> (\x -> x) (\x -> x)
=b> \x -> x``````

## Elsa shortcuts

Named λ-terms:

``let ID = \x -> x  -- abbreviation for \x -> x``

To substitute name with its definition, use a `=d>` step:

``````ID apple
=d> (\x -> x x) apple  -- expand definition
=b> apple              -- beta-reduce``````

Evaluation:

• `E1 =*> E2`: `E1` reduces to `E2` in 0 or more steps
• where each step is `=a>`, `=b>`, or `=d>`
• `E1 =~> E2`: `E1` evaluates to `E2`

What is the difference?

## Non-Terminating Evaluation

``````(\x -> x x) (\x -> x x)
=b> (\x -> x x) (\x -> x x)``````

Oops, we can write programs that loop back to themselves…

and never reduce to a normal form!

This combinator is called Ω

What if we pass Ω as an argument to another function?

``````let OMEGA = (\x -> x x) (\x -> x x)

(\x -> \y -> y) OMEGA``````

Does this reduce to a normal form? Try it at home!

## Programming in λ-calculus

Real languages have lots of features

• Booleans
• Records (structs, tuples)
• Numbers
• Functions [we got those]
• Recursion

Lets see how to encode all of these features with the λ-calculus.

## λ-calculus: Booleans

How can we encode Boolean values (`TRUE` and `FALSE`) as functions?

Well, what do we do with a Boolean `b`?

Make a binary choice

• `if b then E1 else E2`

## Booleans: API

We need to define three functions

``````let TRUE  = ???
let FALSE = ???
let ITE   = \b x y -> ???  -- if b then x else y``````

such that

``````ITE TRUE apple banana =~> apple
ITE FALSE apple banana =~> banana``````

(Here, `let NAME = E` means `NAME` is an abbreviation for `E`)

## Booleans: Implementation

``````let TRUE  = \x y -> x        -- Returns its first argument
let FALSE = \x y -> y        -- Returns its second argument
let ITE   = \b x y -> b x y  -- Applies condition to branches

## Example: Branches step-by-step

``````eval ite_true:
ITE TRUE egg ham
=d> (\b x y -> b    x   y)  TRUE egg ham    -- expand def ITE
=b>   (\x y -> TRUE x   y)       egg ham    -- beta-step
=b>     (\y -> TRUE egg y)           ham    -- beta-step
=b>            TRUE egg ham                 -- expand def TRUE
=d>     (\x y -> x) egg ham                 -- beta-step
=b>     (\y -> egg)     ham                 -- beta-step
=b> egg``````

## Example: Branches step-by-step

Now you try it!

``````eval ite_false:
ITE FALSE egg ham
=d> (\b x y -> b     x   y) FALSE egg ham   -- expand def ITE
=b>   (\x y -> FALSE x   y)       egg ham   -- beta-step
=b>     (\y -> FALSE egg y)           ham   -- beta-step
=b>            FALSE egg ham                -- expand def FALSE
=d>      (\x y -> y) egg ham                -- beta-step
=b>        (\y -> y)     ham                -- beta-step
=b> ham``````

## Boolean Operators

Now that we have `ITE` it’s easy to define other Boolean operators:

``````let NOT = \b     -> ???

let AND = \b1 b2 -> ???

let OR  = \b1 b2 -> ???``````

``````let NOT = \b     -> ITE b FALSE TRUE

let AND = \b1 b2 -> ITE b1 b2 FALSE

let OR  = \b1 b2 -> ITE b1 TRUE b2``````

Or, since `ITE` is redundant:

``````let NOT = \b     -> b FALSE TRUE

let AND = \b1 b2 -> b1 b2 FALSE

let OR  = \b1 b2 -> b1 TRUE b2``````

Which definition to do you prefer and why?

## Programming in λ-calculus

• Booleans [done]
• Records (structs, tuples)
• Numbers
• Functions [we got those]
• Recursion

## λ-calculus: Records

What do we do with a pair?

1. Pack two items into a pair, then
2. Get first item, or
3. Get second item.

## Pairs : API

We need to define three functions

``````let MKPAIR = \x y -> ???    -- Make a pair with elements x and y
-- { fst : x, snd : y }
let FST    = \p -> ???      -- Return first element
-- p.fst
let SND    = \p -> ???      -- Return second element
-- p.snd``````

such that

``````FST (MKPAIR apple banana) =~> apple
SND (MKPAIR apple banana) =~> banana``````

## Pairs: Implementation

A pair of `x` and `y` is just something that lets you pick between `x` and `y`! (I.e. a function that takes a boolean and returns either `x` or `y`)

``````let MKPAIR = \x y -> (\b -> ITE b x y)
let FST    = \p -> p TRUE   -- call w/ TRUE, get first value
let SND    = \p -> p FALSE  -- call w/ FALSE, get second value``````

## Exercise: Triples?

How can we implement a record that contains three values?

``````let MKTRIPLE = \x y z -> MKPAIR x (MKPAIR y z)
let FST3  = \t -> FST t
let SND3  = \t -> FST (SND t)
let TRD3  = \t -> SND (SND t)``````

## Programming in λ-calculus

• Booleans [done]
• Records (structs, tuples) [done]
• Numbers
• Functions [we got those]
• Recursion

## λ-calculus: Numbers

What do we do with natural numbers?

• Count: `0`, `inc`
• Arithmetic: `dec`, `+`, `-`, `*`
• Comparisons: `==`, `<=`, etc

## Natural Numbers: API

We need to define:

• A family of numerals: `ZERO`, `ONE`, `TWO`, `THREE`, …
• Arithmetic functions: `INC`, `DEC`, `ADD`, `SUB`, `MULT`
• Comparisons: `IS_ZERO`, `EQ`

Such that they respect all regular laws of arithmetic, e.g.

``````IS_ZERO ZERO       =~> TRUE
IS_ZERO (INC ZERO) =~> FALSE
INC ONE            =~> TWO
...``````

## Natural Numbers: Implementation

Church numerals: a number `N` is encoded as a combinator that calls a function on an argument `N` times

``````let ONE   = \f x -> f x
let TWO   = \f x -> f (f x)
let THREE = \f x -> f (f (f x))
let FOUR  = \f x -> f (f (f (f x)))
let FIVE  = \f x -> f (f (f (f (f x))))
let SIX   = \f x -> f (f (f (f (f (f x)))))
...``````

## QUIZ: Church Numerals

Which of these is a valid encoding of `ZERO` ?

• A: `let ZERO = \f x -> x`

• B: `let ZERO = \f x -> f`

• C: `let ZERO = \f x -> f x`

• D: `let ZERO = \x -> x`

• E: None of the above

Does this function look familiar?

Answer: It’s the same as `FALSE`!

## λ-calculus: Increment

``````-- Call `f` on `x` one more time than `n` does
let INC   = \n -> (\f x -> f (n f x))``````

Example:

``````eval inc_zero :
INC ZERO
=d> (\n f x -> f (n f x)) ZERO
=b> \f x -> f (ZERO f x)
=*> \f x -> f x
=d> ONE``````

## QUIZ

How shall we implement `ADD`?

A. `let ADD = \n m -> n INC m`

B. `let ADD = \n m -> INC n m`

C. `let ADD = \n m -> n m INC`

D. `let ADD = \n m -> n (m INC)`

E. `let ADD = \n m -> n (INC m)`

``````--  Call `f` on `x` exactly `n + m` times
let ADD = \n m -> n INC m``````

Example:

``````eval add_one_zero :
=~> ONE``````

## QUIZ

How shall we implement `MULT`?

A. `let MULT = \n m -> n ADD m`

B. `let MULT = \n m -> n (ADD m) ZERO`

C. `let MULT = \n m -> m (ADD n) ZERO`

D. `let MULT = \n m -> n (ADD m ZERO)`

E. `let MULT = \n m -> (n ADD m) ZERO`

## λ-calculus: Multiplication

``````--  Call `f` on `x` exactly `n * m` times
let MULT = \n m -> n (ADD m) ZERO``````

Example:

``````eval two_times_three :
MULT TWO ONE
=~> TWO``````

## Programming in λ-calculus

• Booleans [done]
• Records (structs, tuples) [done]
• Numbers [done]
• Functions [we got those]
• Recursion

## λ-calculus: Recursion

I want to write a function that sums up natural numbers up to `n`:

``\n -> ...          -- 1 + 2 + ... + n``

## QUIZ

Is this a correct implementation of `SUM`?

``````let SUM = \n -> ITE (ISZ n)
ZERO

A. Yes

B. No

No!

• Named terms in Elsa are just syntactic sugar
• To translate an Elsa term to λ-calculus: replace each name with its definition
``````\n -> ITE (ISZ n)
ZERO
(ADD n (SUM (DEC n))) -- But SUM is not a thing!``````

Recursion:

• Inside this function I want to call the same function on `DEC n`

Looks like we can’t do recursion, because it requires being able to refer to functions by name, but in λ-calculus functions are anonymous.

Right?

## λ-calculus: Recursion

Think again!

Recursion:

• Inside this function I want to call the same function on `DEC n`
• Inside this function I want to call a function on `DEC n`
• And BTW, I want it to be the same function

Step 1: Pass in the function to call “recursively”

``````let STEP =
\rec -> \n -> ITE (ISZ n)
ZERO
(ADD n (rec (DEC n))) -- Call some rec``````

Step 2: Do something clever to `STEP`, so that the function passed as `rec` itself becomes

``\n -> ITE (ISZ n) ZERO (ADD n (rec (DEC n)))``

## λ-calculus: Fixpoint Combinator

Wanted: a combinator `FIX` such that `FIX STEP` calls `STEP` with itself as the first argument:

``````FIX STEP
=*> STEP (FIX STEP)``````

(In math: a fixpoint of a function f(x) is a point x, such that f(x)=x)

Once we have it, we can define:

``let SUM = FIX STEP``

Then by property of `FIX` we have:

``SUM =*> STEP SUM -- (1)``
``````eval sum_one:
SUM ONE
=*> STEP SUM ONE                 -- (1)
=d> (\rec n -> ITE (ISZ n) ZERO (ADD n (rec (DEC n)))) SUM ONE
=b> (\n -> ITE (ISZ n) ZERO (ADD n (SUM (DEC n)))) ONE
-- ^^^ the magic happened!
=b> ITE (ISZ ONE) ZERO (ADD ONE (SUM (DEC ONE)))
=*> ADD ONE (SUM ZERO)           -- def of ISZ, ITE, DEC, ...
=*> ADD ONE (STEP SUM ZERO)      -- (1)
((\rec n -> ITE (ISZ n) ZERO (ADD n (rec (DEC n)))) SUM ZERO)
=b> ADD ONE ((\n -> ITE (ISZ n) ZERO (ADD n (SUM (DEC n)))) ZERO)
=b> ADD ONE (ITE (ISZ ZERO) ZERO (ADD ZERO (SUM (DEC ZERO))))
=~> ONE``````

How should we define `FIX`???

## The Y combinator

Remember Ω?

``````(\x -> x x) (\x -> x x)
=b> (\x -> x x) (\x -> x x)``````

This is self-replcating code! We need something like this but a bit more involved…

The Y combinator discovered by Haskell Curry:

``let FIX   = \stp -> (\x -> stp (x x)) (\x -> stp (x x))``

How does it work?

``````eval fix_step:
FIX STEP
=d> (\stp -> (\x -> stp (x x)) (\x -> stp (x x))) STEP
=b> (\x -> STEP (x x)) (\x -> STEP (x x))
=b> STEP ((\x -> STEP (x x)) (\x -> STEP (x x)))
--       ^^^^^^^^^^ this is FIX STEP ^^^^^^^^^^^``````

That’s all folks!