The Smallest Universal Language

Alonzo Church

Developed in 1930s by Alonzo Church

• Studied in logic and computer science

Test bed for procedural and functional PLs

• Simple, Powerful, Extensible

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

Syntax: What Programs Look Like

e ::= x, y, z, ...
    | function(x){ return e }
    | e1(e2)

Three kinds of expressions

• e

Variables

• x, y, z (in JS x, y, z)

Function Definitions (Abstraction)

• \x -> e (in JS function(x){return e} or (x) => e)

Function Call (Application)

• e1 e2 (in JS e1(e2))

Complete Description

The Lambda Calculus

Application Is Left Associative

We write

e1 e2 e3 e4

instead of

(((e1 e2) e3) e4)

We write

\x1 -> \x2 -> \x3 -> \x4 -> e

instead of

\x1 -> (\x2 -> (\x3 -> (\x4 -> e)))

Examples

\x -> x             -- The Identity function
                    -- function (x) { return x ;}
                    -- (x) => x

\y -> (\x -> x)     -- A function that returns the Identity Fun
                    --   function(y){ return
                    --      function (x) { return x ;}
                    --   }

\f -> f (\x -> x)   -- A function that applies arg to the Identity Fun

Semantics : What Programs Mean

We define the meaning of a program with simple rules.

1. Scope
2. α-step (aka. renaming formals)
3. β-step (aka. function calls)

Semantics: Scope

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

• x is bound inside e

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

Semantics: Free vs Bound Variables

y is free inside e if

• y appears inside e, and
• y is not bound inside e

Formally,

free(x)       = {x}
free(\x -> e) = free(e)  - {x}
free(e1 e2)   = free(e1) + free(e2)

QUIZ

Let e be the expression \x -> x (\y -> x y z).

Which variables are free in e ?

A. x

B. y

C. z

D. x, y

E. x, y, z

Semantics: α-Equivalence

λ-terms E1 and E2 are α-equivalent if

• E2 can be obtained be renaming the bound variables of E1

or

• E1 can be obtained be renaming the bound variables of E2

Semantics: α-step

Example: The following three terms are α-equivalent

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

We write E1 =a> E2 if E1 is α-equivalent to E2.

• We can say E1 takes an α-step to E2.

α-step Makes Scope Clear

We often α-rename to make parameter names unique

For example, instead of

    \x -> x (\x -> x) x     -- Yucky scope

=a> \x -> x (\y -> y) x     -- Scope of bindings crystal clear

Semantics: Function Calls

In the λ-calculus, a “function call” (application) looks like (x -> E1) E2

How do we evaluate the function with the given argument?

1. Rename parameters to make them unique
2. Substitute all occurrences of x in E1 with E2!

If so, we say that

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

and we can write it as

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

Function Calls: β-step Example

Replace occurrences of parameter f with argument

(\f -> f (f x)) g        

   =b>     g (g x)

No need to rename, bindings already unique

Normal Forms

An redex is a λ-term of the form

(\x -> E1) E2

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

QUIZ

Is the term x in normal form ?

A. Yes

B. No

QUIZ

Is the term (x y) in normal form ?

A. Yes

B. No

QUIZ

Is the term (\x -> x) y in normal form ?

A. Yes

B. No

QUIZ

Is the term x (\y -> y) in normal form ?

A. Yes

B. No

Semantics: Evaluation

A λ-term E reduces/evaluates to a normal form E' if

there is a sequence of steps

E =?> E_1 =?> ... =?> EN =?> E'

where each =?> is

• An α-step =a> or
• A β-step =b>.

Examples of Evaluation

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

(\f -> f (\x -> x)) (\x -> x)
  =a> (\f -> f (\x -> x)) (\y -> y)
  =b> (\y -> y) (\x -> x)
  =b> (\x -> x)

Non-Terminating Evaluation

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

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

• Self replicating code!

λ-Calculus Review

Super tiny language

• E ::= x | \x -> E | (E E)

Many evaluation strategies

• Many steps possible, which to take?
• Call-by-name
• Call-by-value
• Call-by need

Church Rosser Theorem

• Regardless of strategy at most one normal form
• i.e. Programs can evaluate to a single result.

λ-calculus and CSE 130?

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

Huh? What was that Landin fellow going on about?

Programming with the λ-calculus

Real languages have lots of features

• Booleans done
• Branches done
• Records done
• Numbers
  • Representation : n as \f x -> f (f (f (f x)))
  • IsZero
• Arithmetic
  • Incr
  • Add
  • Mul
  • Sub
• Functions (ok, we got those)
• Recursion

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

Hidden Motive

• Free your mind
• Build intuition about evaluation-by-substitution

QUIZ

let bar = (\x y -> x)

What does (bar apple orange) evaluate to?

A. bar orange

B. bar apple

C. apple

D. orange

E. bar

λ-calculus: Booleans

What can we do with a Boolean? - Make a binary choice

How can we encode choice as a function? - A Boolean is a function that - Takes two inputs - Returns one of them as output

True and False

let TRUE  = \x y -> x       -- returns FIRST  input
let FALSE = \x y -> y       -- returns SECOND input

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

• We don’t want to keep re-typing the whole expression out.

QUIZ

Given

let TRUE  = \x y -> x
let FALSE = \x y -> y

What does (TRUE apple orange) evaluate to?

A. apple

B. orange

C. None of the above

λ-calculus: Branches

A branch is a function that takes three inputs

let ITE = \b x y -> ...

• If b evaluates to TRUE return x
• If b evaluates to FALSE return y

In other languages like C or JavaScript you would write

 b ? x : y

How shall we implement ITE as a λ-expression?

let ITE   = \b x y -> b x y

Example: Branches

We want

• if TRUE then e1 else e2 to evaluate to e1

Does it?

eval ite_true:
  ITE TRUE e1 e2
  =d> (\b x y -> b    x  y) TRUE e1 e2    -- expand def ITE  
  =b>   (\x y -> TRUE x  y)      e1 e2    -- beta-step
  =b>     (\y -> TRUE e1 y)         e2    -- beta-step
  =b>            TRUE e1 e2               -- expand def TRUE
  =d>     (\x y -> x) e1 e2               -- beta-step
  =b>       (\y -> e1)   e2               -- beta-step
  =b> e1

Example: Branches

Now you try it! We want

• if FALSE then e1 else e2 to evaluate to e2

Can you fill in the blanks to make it happen?

eval ite_false:
  ITE FALSE e1 e2

  -- fill the steps in!

  =*> e2  

QUIZ

let TRUE  = \p q -> p
let FALSE = \p q -> q
let HAHA  = \b   -> ITE b FALSE TRUE

What does HAHA TRUE evaluate to?

A. HAHA TRUE B. TRUE C. FALSE D. HAHA E. HAHA FALSE

Boolean Operators: NOT

We can develop the Boolean operators from truth tables

We can encode the above as:

let NOT = \b -> ITE b FALSE TRUE

That is, HAHA is actually the NOT operator!

Boolean Operators: AND

Similarly, AND b1 b2 is defined by the truth table

We can encode the truth table as a function

let AND = \b1 b2 -> ITE b1 (ITE b2 TRUE FALSE) FALSE

which can be simplified to

let AND = \b1 b2 -> b1 b2 FALSE

(Can you see why?)

Boolean Operators: OR

Similarly, OR b1 b2 is defined by the truth table

We can encode the truth table as a function

let OR = \b1 b2 -> ITE b1 TRUE (ITE b2 TRUE FALSE)

which can be simplified to

let OR = \b1 b2 -> b1 TRUE b2

(Can you see why?)

λ-calculus: Records

What can we do with records ?

1. Pack two items into a record.
2. Get first item.
3. Get second item.

Records : API

(PACK v1 v2)  -- makes a pair out of v1, v2 s.t.
              -- { fst : v1, snd : v2 }
              -- (\b -> ITE b v1 v2)

(FST r)       -- returns the first element
              -- r.fst
              -- r TRUE

(SND r)       -- returns the second element
              -- r.snd
              -- r FALSE

such that

FST (PACK v1 v2) = v1   
-- var r = { fst : v1, snd : v2}; assert(r.fst === v1)

SND (PACK v1 v2) = v2
-- var r = { fst : v1, snd : v2}; assert(r.snd === v2)

Records: Implementation

A create a record as a function

let PACK = \v1 v2 -> (\b -> ITE b v1 v2)

• Is called with a Boolean b
• Returns first element if b is TRUE
• Returns second element if b is FALSE

We access a record by calling it with TRUE or FALSE

let FST  = \r -> r TRUE   -- call w/ TRUE, get first value

let SND  = \r -> r FALSE  -- call w/ FALSE, get second value

Exercise: Records with 3 values?

How can we implement a record that contains three values?

-- let NULL = FALSE
-- {fst : 'orange', snd : FALSE}
-- {fst : 'banana', {fst : 'orange', snd : FALSE}}
-- {fst : 'apple' , {fst : 'banana', {fst : 'orange', snd : FALSE}}}
-- {fst : 'durian'
        , {fst : 'apple'
               , {fst : 'banana'
                      , {fst : 'orange'
                            , snd : FALSE}}}}

-- PACK durian (PACK apple (PACK orange FALSE))

-- PACK (
      (PACK durian apple)
      (PACK orange banana)
   )


snd : 'orange'}
-- {fst : 'apple' , snd : {fst : 'banana', snd : 'orange'}}
-- {fst : 'durian', snd : {fst : 'apple' , snd : {fst : 'banana', snd : 'orange'}}}


-- {fst : {fst : 'durian', snd : 'apple'},
   ,snd :{fst : 'banana', snd : 'orange'} }


-- {fst : {fst : 'orange', snd : 'apple'}, snd : 'banana' }
-- r.fst.fst === 'orange'
-- r.fst.snd === 'apple'
-- {fst : {fst : {fst : 'orange', snd : 'apple'}, snd : 'banana' }, snd : 'melon'}

let PACK3 = \v1 v2 v3 -> PACK v1 (PACK v2 v3)
let FST3  = \r -> FST r
let SND3  = \r -> FST (SND r)
let THD3  = \r -> SND (SND r)


let BOB ZERO  = (PACK ZERO FALSE)
let BOB ONE   = PACK ONE (PACK ZERO FALSE)
let BOB TWO   = PACK TWO (PACK ONE (PACK ZERO FALSE))
let BOB THREE = PACK THREE (PACK TWO (PACK ONE (PACK ZERO FALSE)))

λ-calculus: Numbers

n f s means run f on s exactly n times

-- | represent n as  \f x. f (f (f  ...   (f x)
--                         '--- 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)))

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!

λ-calculus: Arithmetic (IsZero)

Lets implement a small API for numbers:

-- TRUE if n = ZERO and FALSE otherwise
let IsZero = \n -> ...

λ-calculus: Arithmetic (Incr)

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

An example!

eval incr_one :
  Incr ONE
  =d> (\n f x -> f (n f x)) ONE
  =b> \f x -> f (ONE f x)
  =*> \f x -> f (f x)
  =d> TWO

eval incr_two :
  Incr TWO
  =d> (\n f x -> f (n f x)) TWO
  =b> \f x -> f (TWO f x)
  =*> \f x -> f (f (f x))
  =d> THREE

QUIZ

How shall we implement Plus?

--  Call `f` on `x` exactly `n + m` times
let Plus = \n m -> ???  

eval plus_zero_zero :
  Plus ZERO ZERO =~> ZERO

eval plus_two_one :
  Plus TWO ONE =~> THREE

eval plus_two_two :
  Plus TWO TWO =~> FOUR

A. let Plus = \n m -> (n Incr) m

B. let Plus = \n m -> Incr n m

C. let Plus = \n m -> n m Incr

D. let Plus = \n m -> n (m Incr)

E. let Plus = \n m -> n (Incr m)

λ-calculus: Arithmetic (Plus)

--  Call `f` on `x` exactly `n + m` times
let Plus = \n m -> ???

An example!

eval plus_zero_zero :
  Plus ZERO ZERO
  =~> ZERO

eval plus_two_two :
  Plus TWO TWO
  =~> FOUR

QUIZ

How shall we implement MULT?

--  Call `f` on `x` exactly `n * m` times
let Mult = \n m -> ???  

eval mult_zero_two :
  Mult ZERO TWO =~> ZERO

eval mult_two_one :
  Mult TWO ONE =~> TWO

eval mult_two_three :
  Mult TWO THREE =~> SIX

A. let Mult = \n m -> n Plus m

B. let Mult = \n m -> n (Plus m) ZERO

E. let Mult = \n m -> m (Plus n) ZERO

C. let Mult = \n m -> n (Plus m ZERO) D. let Mult = \n m -> (n Plus m) ZERO

λ-calculus: Arithmetic (Mult)

--  Call `f` on `x` exactly `n * m` times
let Mult = \n m -> ???

eval mul_two_three :
  mul two three
  =*> six

λ-calculus: Recursion

The final frontier …