Lambda Calculus¶
Review: 9/26 - Lambda Calculus
-
occurrence
¶ an appearance of a variable in an expression (binding does not count)
Quizzes¶
tiny.cc/
cse116-lambda-ind -> A
cse116-scope-ind -> C
cse116-beta1-ind -> D
cse116-beta2-ind -> A
cse116-norm-ind -> C
cse116-church-ind -> A
cse116-add-ind -> A
cse116-mult-ind -> B
cse116-sum-ind -> NO
Reductions¶
-
alpha-reduction
\x -> e =a> \y -> e[x := y]
| where not (y in FV(e))
-
beta-reduction
(\x -> e1) e2 =b> e1[x := e2]
“Replace all free occurrences of x in e1 with e2.”
x[x := e] = e
y[x := e] = y
(e1 e2)[x := e] = (e1[x := e]) (e2[x := e])
(\x -> e1)[x := e] = \x -> e1 -- since x in e1 is bound
(\y -> e1)[x := e]
| not (y in FV(e)) = \y -> e1[x := e]
| otherwise undefined
Normal Forms¶
A redex is a lambda-term of the form (\x -> e1) e2
(i.e. can be beta-reduced).
A lambda-term is in normal form if it contains no redexes (i.e. cannot be beta-reduced).
Semantics: Evaluation¶
A lambda-term e evaluates to e’ if:
1. There is a sequence of stops e =?> e_1 =?> ... =?> e'
Examples¶
(\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 lambda-terms¶
let ID = \x -> x
To substitute a name with its defn, use a =d> step
ID apple
=d> \x -> x apple
=b> apple
Evaluation¶
e1 =*> e2
- e1 reduces to e2 in 0 or more steps, where each step is in =a>, =b>, =d>
e1 =~> e2
- e1 evaluates to e2 (i.e. final output)
Non-Terminating Evaluation¶
(\x -> x x) (\x -> x x)
=b> (\x -> x x) (\x -> x x)
Programs can loop and never reduce to normal form!
This is called the omega-term.
What if we pass omega to another function?
let OMEGA = (\x -> x x) (\x -> x x)
(\x -> \y -> y) OMEGA
Lambda Calculus: Booleans¶
How do we encode T/F as a func?
With booleans, we make a binary choice (e.g. if b then e1 else e2
)
We need to define three functions:
let TRUE = \x y -> x
let FALSE = \x y -> y
let ITE = \b x y -> b x y
such that
ITE TRUE apple banana =~> apple
ITE FALSE apple banana =~> banana
eval ite_true:
ITE TRUE e1 e2
=d> (\b x y -> b x y) TRUE e1 e2
=b> (\x y -> TRUE x y) e1 e2
=b> (\y -> TRUE e1 y) e2
=b> TRUE e1 e2
=d> (\x y -> x) e1 e2
=b> (\y -> e1) e2
=b> e1
eval ite_false:
ITE FALSE e1 e2
=d> (\b x y -> b x y) FALSE e1 e2
=b> (\x y -> FALSE x y) e1 e2
=b> (\y -> FALSE e1 y) e2
=b> FALSE e1 e2
=d> (\x y -> y) e1 e2
=b> (\y -> y) e2
=b> e2
Now we can 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
(ITE
is redundant, so it can be removed from these defns)
Lambda Calculus: Records¶
Start with records w/ 2 fields (pairs)
- What do we want to do?
Pack two items into a pair
Get first
Get second
API¶
let PAIR = \x y -> (\b -> ITE b x y)
-- a function that returns a function
-- that takes a boolean asking which item you want
let FST = \p -> p TRUE
let SND = \p -> p FALSE
such that
FST (PAIR apple banana) =~> apple
SND (PAIR apple banana) =~> banana
Triples¶
let TRIPLE = \x y z -> PAIR x (PAIR y z)
let FST3 = \t -> FST t
let SND3 = \t -> FST (SND t)
let TRD3 = \t -> SND (SND t)
Lambda Calculus: Numbers¶
What about natural numbers [0..]?
Counters, arithmetic, comparisons
+, -, *, ==, <=, etc
We need to define:
a family of numerals
ZERO, ONE, TWO
, etcarithmetic functions
INC, DEC, ADD, SUB, MULT
comparisons
IS_ZERO, EQ
Implementation¶
Church numerals: A number N is encoded as a combinator that calls a function on an argument N times
let ZERO = \f x -> x
let ONE = \f x -> f x
let TWO = \f x -> f (f x)
let THREE = \f x -> f (f (f x))
...etc
Increment¶
-- call `f` on `x` one more time than `n` does
let INC = \n -> (\f x -> f (n f x))
-- ex
INC ZERO
=d> (\n f x -> f (n f x)) ZERO
=b> \f x -> f (ZERO f x)
=*> \f x -> f x
=d> ONE
Add¶
let ADD = \n m -> n INC m
-- n is a function that takes a function and number
-- i.e. apply INC n times to m
-- ex
eval add_one_zero:
ADD ONE ZERO
=d> (\n m -> n INC m) ONE ZERO
=b> (\m -> ONE INC m) ZERO
=b> ONE INC ZERO
=d> (\f x -> f x) INC ZERO
=b> INC ZERO
=*> ONE
eval add_two_one:
ADD TWO ONE
=d> (\n m -> n INC m) TWO ONE
=b> (\m -> TWO INC m) ONE
=b> TWO INC ONE
=d> (\f x -> f (f x)) INC ONE
=b> INC (INC ONE)
=*> THREE
Mult¶
let MULT = \n m -> n (ADD m) ZERO
-- ADD m returns a function
-- so we call ADD m on ZERO n times
-- similar to python partials
-- ex
eval two_times_one:
MULT TWO ONE
=d> (\n m -> n (ADD m) ZERO) TWO ONE
=b> (\m -> TWO (ADD m) ZERO) ONE
=b> TWO (ADD ONE) ZERO
=~> ADD ONE (ADD ONE ZERO)
=~> TWO
Lambda Calculus: Recursion¶
Ex. I want to write a number that sums up natural numbers to n.
\n -> ... -- = 1 + 2 + ... + n
Step 1: Pass in the function to call recursively
let STEP =
\rec ->
\n -> ITE (ISZ n)
ZERO
(ADD n (rec (DEC n)))
Step 2: Do something to STEP
so that the function passed as rec
becomes:
\n -> ITE (ISZ n) ZERO (ADD n (rec (DEC n)))
Note
Wanted: a combinator FIX
s.t. FIX STEP
calls STEP
with itself as the first argument
FIX STEP
=*> STEP (FIX STEP)
Note
It’s important that STEP
has some base case in it, or else you end up with STEP (STEP (STEP (STEP...)))
then, let SUM = FIX STEP
, so SUM =*> STEP SUM
eval sum_one:
SUM ONE
=*> STEP SUM ONE
=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
=b> ITE (ISZ ONE) ZERO (ADD ONE (SUM (DEC ONE)))
=*> ITE FALSE ZERO (ADD ONE (STEP SUM ZERO))
=*> ADD ONE (SUM ZERO)
=*> ADD ONE (STEP SUM ZERO)
=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))))
=*> ADD ONE (ITE TRUE ZERO (ADD ZERO (SUM (DEC ZERO))))
=*> ADD ONE ZERO
=~> ONE
So how do we define FIX
?
- Let’s look back at omega:
(\x -> x x) (\x -> x x) =b> (\x -> x x) (\x -> x x)
We need something similar but with control
Thus, the Y combinator (or fixpoint)
let FIX = \stp -> (\x -> stp (x x)) (\x -> stp (x x))
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)))
=d> STEP (FIX STEP)
Note
Example: MULT
using recursion
-- if we can use recursion by name:
let MULT x y =
ITE (ISZ y)
ZERO
ADD x (MULT x (DECR y))
-- replace the self ref with a passed func
let MULT1 f x y =
ITE (ISZ y)
ZERO
ADD x (f x (DECR y))
-- and use fixpt
let MULT = FIX MULT1
-- therefore, generally
let FUNC0 = \f n -> ... f (DECR n)
let FUNC = FIX FUNC0