## Your Favorite Language

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:

### 1936: Formalization

What is the **smallest universal language**?

The **Turing Machine**

The **Lambda Calculus**

## The Next 700 Languages

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

*Correct answer:* **A**

## 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

instead of | we write |
---|---|

`\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
=> -- RULE: add monomials
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

*α*-step (aka*renaming formals*)*β*-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

*Correct answer:* **C**

## 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

*α*-step (aka*renaming formals*)*β*-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
```

Is this right? Ask Elsa!

```
(\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`

*Correct answer:* **D.**

## QUIZ

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

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

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

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

**D.** `apple`

**E.** `\x -> x`

*Correct answer:* **A.**

## 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

*α*-step (aka*renaming formals*)*β*-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

*Answer:* E

## QUIZ

How many redexes does this expression have?

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

**A.** 0

**B.** 1

**C.** 2

**D.** 3

**E.** 4

*Answer:* C

## Semantics: Evaluation

A *λ*-term `E`

**evaluates to** `E'`

if

There is a sequence of steps

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

where each `=?>`

is either `=a>`

or `=b>`

and `N >= 0`

`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>`

- where each step is
`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
-- (redundant, but improves readability)
```

## 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

Let’s start with records with *two* fields (aka **pairs**)

What do we *do* with a pair?

**Pack two**items into a pair, then**Get first**item, or**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

Let’s start with **natural numbers** (0, 1, 2, …)

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

*Answer:* A

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)`

*Answer:* A

*λ*-calculus: Addition

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

**Example:**

```
eval add_one_zero :
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`

*Answer:* B or C

*λ*-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
(ADD n (SUM (DEC n)))
```

**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)
=d> ADD ONE
((\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))))
=b> ADD ONE 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!