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





1936: Formalization

What is the smallest universal language?

Alan Turing

The Turing Machine



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


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)











Examples

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

\x -> (\y -> y)     -- A function that returns (id)

\f -> (f (\x -> x)) -- A function that applies its argument to id













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: multiply polynomials
  3x^2 - x + 6x - 2
=> -- RULE: add monomials
  3x^2 + 5x - 2


Execute = rewrite step-by-step

  • Following simple rules
  • until no more rules apply













Rewrite Rules of Lambda Calculus


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


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. first occurrence is bound, second is bound

B. first occurrence is bound, second is free

C. first occurrence is free, second is bound

D. first occurrence is free, second is free


Correct answer: B












EXERCISE: 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 function call)
  2. α-step (aka renaming formals)













Semantics: Redex

A redex (reducible expression) is a term of the form


  (\x -> e1) e2

A function (\x -> e1)

  • x is the parameter
  • e1 is the returned expression

Applied to an argument e2

  • e2 is the argument













Semantics: β-Reduction


A redex b-steps to another term …

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













Redex Examples


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

Is this right? Ask Elsa! (https://goto.ucsd.edu/elsa/index.html)













QUIZ


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

A. apple apple apple apple

B. y apple y apple

C. y y y y

D. apple


Correct answer: B.












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.












EXERCISE

What is a λ-term fill_this_in such that


fill_this_in apple
=b> banana

ELSA: https://goto.ucsd.edu/elsa/index.html

Click here to try this exercise












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 in body!


Solution: Ensure that formals in the body are different from free-variables of argument!












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


Formally:

x[x := e]            = e

y[x := e]            = y          -- when x /= y

(e1 e2)[x := e]      = (e1[x := e]) (e2[x := e])

(\x -> e1)[x := e]   = \x -> e1   -- Q: Why leave `e1` unchanged?

(\y -> e1)[x := e] 
  | not (y in FV(e)) = \y -> e1[x := e]

Oops, but what to do if y is in the free-variables of e?

  • i.e. if \y -> ... may capture those free variables?

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 function call)
  2. α-step (aka renaming formals)













Semantics: α-Renaming


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


  • We rename a formal parameter x to y

  • By replace all occurrences of x in the body with y

  • 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














Tricky Example Revisited


    (\x -> (\y -> x)) y
                                -- rename 'y' to 'z' to avoid capture
    =a> (\x -> (\z -> x)) y
                                -- now do b-step without capture!
    =b> \z -> y



To avoid getting confused,

  • you can always rename formals,

  • so different variables have different names!













Normal Forms

Recall 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: C













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

  2. 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













EXERCISE

What is a λ-term fill_this_in such that the evaluation of (\x -> x x) fill_this_in loops, i.e.:

eval loop : 
  (\x -> x x) fill_this_in
  =b> (\x -> x x) fill_this_in
  =b> (\x -> x x) fill_this_in
  =b> ...

ELSA: https://goto.ucsd.edu/elsa/index.html

Click here to try this exercise








Non-Terminating Evaluation

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

Some programs loop back to themselves…

… and never reduce to a normal form!

This combinator is called Ω







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) 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 and e2 is in normal form











Programming in λ-calculus

Real languages have lots of features

  • Functions [we got those]
  • Booleans
  • Records (structs, tuples)
  • Numbers
  • Lists
  • 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 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 step-by-step

Now you try it!

Can you fill in the blanks to make it happen?

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













EXERCISE: Boolean Operators

ELSA: https://goto.ucsd.edu/elsa/index.html

Click here to try this exercise

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

let NOT = \b     -> ITE b FALSE TRUE 

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

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

When you are done, you should get the following behavior:

eval ex_not_t:
  NOT TRUE =*> FALSE
  
eval ex_not_f:
  NOT FALSE =*> TRUE 
  
eval ex_or_ff:
  OR FALSE FALSE =*> FALSE

eval ex_or_ft:
  OR FALSE TRUE =*> TRUE
  
eval ex_or_ft:
  OR TRUE FALSE =*> TRUE

eval ex_or_tt:
  OR TRUE TRUE =*> TRUE
  
eval ex_and_ff:
  AND FALSE FALSE =*> FALSE

eval ex_and_ft:
  AND FALSE TRUE =*> FALSE
  
eval ex_and_ft:
  AND TRUE FALSE =*> FALSE

eval ex_and_tt:
  AND TRUE TRUE =*> TRUE












Programming in λ-calculus

  • Functions [we got those]
  • Booleans [done]
  • Records (structs, tuples)
  • Numbers
  • Lists
  • 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

let PAIR = \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

eval ex_fst: 
  FST (PAIR apple banana) =*> apple

eval ex_snd:
  SND (PAIR 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 PAIR = \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?

ELSA: https://goto.ucsd.edu/elsa/index.html

Click here to try this exercise

let TRIPLE = \x y z -> ???
let FST3   = \t -> ???
let SND3   = \t -> ???
let THD3   = \t -> ???

eval ex1:
  FST3 (TRIPLE apple banana orange)
  =*> apple

eval ex2:
  SND3 (TRIPLE apple banana orange)
  =*> banana 

eval ex3:
  THD3 (TRIPLE apple banana orange)
  =*> orange
let TRIPLE = \x y z -> PAIR x (PAIR y z)
let FST3  = \t -> FST t
let SND3  = \t -> FST (SND t)
let THD3  = \t -> SND (SND t)













Programming in λ-calculus

  • Functions [we got those]
  • Booleans [done]
  • Records (structs, tuples) [done]
  • Numbers
  • Lists
  • 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













EXERCISE

Fill in the implementation of ADD so that you get the following behavior

Click here to try this exercise

let ZERO = \f x -> x
let ONE  = \f x -> f x
let TWO  = \f x -> f (f x)
let INC  = \n f x -> f (n f x)

let ADD  = fill_this_in 

eval add_zero_zero: 
  ADD ZERO ZERO =~> ZERO

eval add_zero_one: 
  ADD ZERO ONE =~> ONE

eval add_zero_two: 
  ADD ZERO TWO =~> TWO 

eval add_one_zero: 
  ADD ONE ZERO =~> ONE

eval add_one_zero: 
  ADD ONE ONE =~> TWO

eval add_two_zero: 
  ADD TWO ZERO =~> TWO













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

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













λ-calculus: Lists

Records had fixed length:

PAIR apple banana
TRIPLE apple banana cherry

Now we want to build lists of arbitrary length.

Can we do it like this?

LIST apple banana
LIST apple banana cherry










That’s unlikely to work (requires a function with a variable number of arguments).

But we can construct lists like this:

CONS apple (CONS banana NIL)
CONS apple (CONS banana (CONS cherry NIL))

where

  • NIL denotes the empty list
  • CONS h t denotes a non-empty list with head h and tail t










Destructing a list

  • HEAD l returns the first element of the list
  • TAIL l returns the rest of the list
HEAD (CONS apple (CONS banana (CONS cherry NIL)))
=*> apple

TAIL (CONS apple (CONS banana (CONS cherry NIL)))
=*> CONS banana (CONS cherry NIL)













Lists: API

We need to define five functions

let CONS = ???
let HEAD = ???
let TAIL = ???

let NIL  = ???
let IS_EMPTY = ???

such that

eval elem0:
  HEAD (CONS apple (CONS banana (CONS cherry NIL)))
  =~> apple

eval elem1: 
  HEAD (TAIL (CONS apple (CONS banana (CONS cherry NIL))))
  =~> banana

eval elem2: 
  HEAD (TAIL (TAIL (CONS apple (CONS banana (CONS cherry NIL)))))
  =~> cherry

eval empty_nil:
  IS_EMPTY NIL
  =~> TRUE

eval empty_cons:
  IS_EMPTY (CONS apple (CONS banana (CONS cherry NIL)))
  =~> FALSE













The first three are easy:

let CONS = \h t -> PAIR h t
let HEAD = \l -> FST l
let TAIL = \l -> SND l













EXERCISE: Nth

Write an implementation of GetNth such that

  • GetNth n l returns the n-th element of the list l

Assume that l has n or more elements

let GetNth = ???

eval nth1 :
  GetNth ZERO (CONS apple (CONS banana (CONS cherry NIL)))
  =~> apple 

eval nth1 :
  GetNth ONE (CONS apple (CONS banana (CONS cherry NIL)))
  =~> banana

eval nth2 :
  GetNth TWO (CONS apple (CONS banana (CONS cherry NIL)))
  =~> cherry

Click here to try this in elsa









IS_EMPTY and NIL

We need to define IS_EMPTY and NIL such that

IS_EMPTY (CONS e1 e2) =~> FALSE -- for any e1 and e2!

IS_EMPTY NIL =~> TRUE








    IS_EMPTY (CONS e1 e2)
=*>  -- by def. of CONS, PAIR
    IS_EMPTY (\b -> b e1 e2)    
=d> -- let's make IS_EMPTY apply its pair to something:
    (\l -> l SOMETHING) (\b -> b e1 e2)
=b>
    (\b -> b e1 e2) SOMETHING
=b>
    SOMETHING e1 e2
=~>
    FALSE

What is such a SOMETHING that SOMETHING e1 e2 is always FALSE?




let SOMETHING = \x y -> FALSE

i.e.

let IS_EMPTY = \l -> l (\x y -> FALSE)













EXERCISE: NIL

Now define NIL such that:

let IS_EMPTY = \l -> l (\x y -> FALSE)
let NIL = ???

eval is_empty_nil :
  IS_EMPTY NIL
  =~> TRUE

Click here to try this in elsa













Programming in λ-calculus

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













λ-calculus: Recursion


I want to write a function LEN that computes the length of a list, i.e.:

eval len_nil: 
  LEN NIL =~> ZERO
  
eval len_1:
  LEN (CONS apple NIL) =~> ONE

eval len_2:
  LEN (CONS apple (CONS banana NIL)) =~> TWO

Can we write LEN using Church Numerals?







Yes, if know the maximum possible length of a list.

Try it in Elsa!

But what if we don’t?







We need to use recursion!











QUIZ

Is this a correct implementation of LEN?

let LEN = \l -> ITE (IS_EMPTY l) 
                ZERO 
                (INC (LEN (TAIL l)))

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
let LEN = \l -> ITE (IS_EMPTY l) 
                ZERO 
                (INC (LEN (TAIL l))) -- But LEN is not a thing!



Recursion:

  • Inside this function I want to call the same function on TAIL l



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 TAIL l
  • Inside this function I want to call a function on TAIL l
  • And BTW, I want it to be the same function



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

let STEP = 
  \rec -> \l -> ITE (IS_EMPTY l) 
                    ZERO 
                    (INC (rec (TAIL l))) -- Call some rec



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

\l -> ITE (IS_EMPTY l) ZERO (INC (rec (TAIL l)))













λ-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 LEN = FIX STEP

Then by property of FIX we have:

LEN =*> STEP LEN -- (1)
LEN (CONS a NIL)
  =*> -- (1) 
STEP LEN (CONS a NIL)
  =d>
(\rec l -> ITE (IS_EMPTY l) ZERO (INC (rec (TAIL l)))) LEN (CONS a NIL)
  =b> 
(\    l -> ITE (IS_EMPTY l) ZERO (INC (LEN (TAIL l))))     (CONS a NIL) 
  =b>                               -- ^^^ the magic happened!
ITE (IS_EMPTY l) ZERO (INC (LEN (TAIL (CONS a NIL))))
=*> -- def of IS_EMPTY, ITE, TAIL, ... 
INC (LEN NIL)
=*> -- (1)
INC (STEP LEN NIL)
=d> 
INC ((\rec l -> ITE (IS_EMPTY l) ZERO (INC (rec (TAIL l)))) LEN NIL)
=b> 
INC ((\l -> ITE (IS_EMPTY l) ZERO (INC (LEN (TAIL l)))) NIL)
=*> 
INC (ITE (IS_EMPTY NIL) ZERO (INC (LEN (TAIL NIL))))
=*> 
INC 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-replicating 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, Haskell Curry was very clever.

Next week: We’ll look at the language named after him (Haskell)