Lambda Calculus

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:

can be computed by a human with pen and paper, following an algorithm
can be computed by a human with pen and paper, following an algorithm





1936: Formalization

What is the smallest universal language?

Alan Turing
Alan Turing



Alonzo Church
Alonzo Church














The Next 700 Languages

Peter Landin
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, only thing 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



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)











Examples













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


How do I define a function with two arguments?

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

























How do I apply a function to two arguments?

  • e.g. apply \x -> (\y -> y) to apple and 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















Semantics : What Programs Mean


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


Think of middle-school algebra:


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:



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


For example, x is free in:












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

An 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:













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?













Rewrite Rules of Lambda Calculus


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













Semantics: β-Reduction



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


Is this right? Ask Elsa!















QUIZ


A. apple

B. \y -> apple

C. \x -> apple

D. \y -> y

E. \x -> y













QUIZ


A. apple (\x -> x)

B. apple (\apple -> apple)

C. apple (\x -> apple)

D. apple

E. \x -> x













A Tricky One


Is this right?













Something is Fishy


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:


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:












Rewrite Rules of Lambda Calculus


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













Semantics: α-Renaming



  • 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:

All these expressions are α-equivalent




What’s wrong with these?














The Tricky One




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

B. x y

C. (\x -> x) y

D. x (\y -> y)

E. C and D













Semantics: Evaluation

A λ-term e evaluates to e' if

  1. There is a sequence of steps

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

  1. e' is in normal form







Examples of Evaluation









Elsa shortcuts

Named λ-terms:



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



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

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?

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

such that

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













Booleans: Implementation













Example: Branches step-by-step







Example: Branches step-by-step

Now you try it!

Can you fill in the blanks to make it happen?













Boolean Operators

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




















Or, since ITE is redundant:


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?

  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

such that













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)













Exercise: Triples?

How can we implement a record that contains three values?













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.













Natural Numbers: Implementation

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













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?












λ-calculus: Increment













Example:













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)













λ-calculus: Addition




Example:













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




Example:













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:











QUIZ

Is this a correct implementation of SUM?

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



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”



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













λ-calculus: Fixpoint Combinator

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


(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:

Then by property of FIX we have:

How should we define FIX???













The Y combinator

Remember Ω?

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





The Y combinator discovered by Haskell Curry:



How does it work?






That’s all folks!