cse130 https://ucsd-cse130.github.io/wi21/lectures/01-lambda.html
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?
1 of 69 1/7/21, 8:59 AM
cse130 https://ucsd-cse130.github.io/wi21/lectures/01-lambda.html
What is computable? Before 1930s
Informal notion of an e!ectively calculable function:
can be computed by a human with pen and paper, following an algorithm
1936: Formalization
2 of 69 1/7/21, 8:59 AM
cse130 https://ucsd-cse130.github.io/wi21/lectures/01-lambda.html
What is the smallest universal language?
Alan Turing
3 of 69 1/7/21, 8:59 AM
cse130 https://ucsd-cse130.github.io/wi21/lectures/01-lambda.html
Alonzo Church
The Next 700 Languages
Peter Landin
4 of 69 1/7/21, 8:59 AM
cse130 https://ucsd-cse130.github.io/wi21/lectures/01-lambda.html
Peter Landin, 1966
The Lambda Calculus
Has one feature: Functions
Whatever the next 700 languages turn out to be, they will surely be variants of lambda calculus.
5 of 69 1/7/21, 8:59 AM
cse130 https://ucsd-cse130.github.io/wi21/lectures/01-lambda.html
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
6 of 69 1/7/21, 8:59 AM
cse130 https://ucsd-cse130.github.io/wi21/lectures/01-lambda.html
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
7 of 69 1/7/21, 8:59 AM
cse130
https://ucsd-cse130.github.io/wi21/lectures/01-lambda.html
8 of 69
e ::= x
| (\x -> e)
ns ‘e’
| (e1 e2)
— variable ‘x’
— function that takes a parameter ‘x’ and retur
— call (function) ‘e1’ with argument ‘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)
OO lambda CSBowizi
Ieng6 looks like
rm rf
N1 stack
1/7/21, 8:59 AM
e
2C y Z
1 Lg e
l
Ce
Ea
wrk
cse130
https://ucsd-cse130.github.io/wi21/lectures/01-lambda.html
Examples
(\x -> x)
ts input
(\x -> (\y -> y))
(\f -> (f (\x -> x))) — A function that applies its argument to i
d
— The identity function (id) that returns i
— A function that returns (id)
QUIZ
Which of the following terms are syntactically incorrect?
ble
Iguana
yA. (\(\x->x)->y) B. (\x -> (x x))
41003J
C. (\x -> (x (y x))) D. A and C
9 of 69
1/7/21, 8:59 AM
cse130
https://ucsd-cse130.github.io/wi21/lectures/01-lambda.html
E. all of the above
Examples
(\x -> x) — The identity function (id) that returns i ts input
(\x -> (\y -> y)) — A function that returns (id)
(\f -> (f (\x -> x))) — A function that applies its argument to i
a
gum targe
How do I define a function with two arguments?
e.g. a function that takes x and y and returns y ?
fine Cx
d
e ez
T fine
E Arg
y return y
10 of 69
Ix
ly
y
1/7/21, 8:59 AM
cse130 https://ucsd-cse130.github.io/wi21/lectures/01-lambda.html
(\x -> (\y -> y)) — A function that returns the identity functi on
— 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 ?
11 of 69 1/7/21, 8:59 AM
cse130 https://ucsd-cse130.github.io/wi21/lectures/01-lambda.html
Cx
¦Ì
ly y X apple
e
banana
X
lx
1
3
(((\x -> (\y -> y)) apple) banana) — first apply to apple,
— then apply the result to ban
ana
Syntactic Sugar
instead of we write
12 of 69 1/7/21, 8:59 AM
cse130 https://ucsd-cse130.github.io/wi21/lectures/01-lambda.html
instead of
\x->(\y->(\z->e))
\x->\y->\z->e
(((e1 e2) e3) e4)
we write
\x->\y->\z->e
\x y z -> e
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
Look like
mean
Semantics : What Programs Mean
How do I ¡°run¡± / ¡°execute¡± a ¦Ë-term?
Syntax Semantic
13 of 69 1/7/21, 8:59 AM
cse130 https://ucsd-cse130.github.io/wi21/lectures/01-lambda.html
Think of middle-school algebra:
D
e
(1+2)*((3*8)-2)
==
3 *(24 -2) ==
3 *22 ==
D66
Execute = rewrite step-by-step
Following simple rules until no more rules apply
3 *((3*8)-2) Ie ==
d
ez
t
i
66
result
Rewrite Rules of Lambda Calculus
14 of 69 1/7/21, 8:59 AM
cse130
https://ucsd-cse130.github.io/wi21/lectures/01-lambda.html
15 of 69
1/7/21, 8:59 AM
1. ¦Â-step (aka function call)
2. ¦Á-step (aka renaming formals)
Programing
Scope
But first we have to talk about scope
var x cat
vain
3
is
fo
x
KK
cat
IT
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
D
return e
any occurrence of x in (\x -> e) is bound (by the binder \x ) u
For example, x is bound in: a
(\x -> x)
(\x -> (\y -> x))
funccx
cse130 https://ucsd-cse130.github.io/wi21/lectures/01-lambda.html
An occurrence of x in e is free if it¡¯s not bound by an enclosing abstraction as e
For example, x is free in: (x y)
r;
— no binders at all!
— no \x binder
((\x -> (\y -> y)) x) — x is outside the scope of the \x binde
a
(\y -> (x y))
a
se
QUIZ
— intuition: it’s not “the same” x
f
iz
Is x bound or free in the expression ((\x -> x) x) ?
A. first occurrence is bound, second is bound 4 Epee B. first occurrence is bound, second is free bound
16 of 69 1/7/21, 8:59 AM
cse130
https://ucsd-cse130.github.io/wi21/lectures/01-lambda.html
17 of 69
1/7/21, 8:59 AM
C. first occurrence is free, second is bound D. first occurrence is free, second is free
EXERCISE: Free Variables
An variable x is free in e if there exists a free occurrence of x in e
rose
appt
We can formally define the set of all free variables in a term like so:
FV(x) = ??? Ee FV(\x -> e) = ???
a
FV(e1 e2)
= ???
pv apple banane
tanana
fv
apple
appleban
lapple aapple
FV
pv dapple
banana
cse130
https://ucsd-cse130.github.io/wi21/lectures/01-lambda.html
18 of 69
1/7/21, 8:59 AM
Fv Ex FV the
a
f e a
fVce 9
Fuced
G
If e has no free variables it is said to be closed
F Vce Clo0sed Expressions
Closed expressions are also called combinators D
What is the shortest closed expression?
Ix
fine
o
sac
Rewrite Rules of Lambda Calculus
t
cse130
https://ucsd-cse130.github.io/wi21/lectures/01-lambda.html
19 of 69
1/7/21, 8:59 AM
1. ¦Â-step (aka function call) D
2. ¦Á-step (aka renaming formals)
Semantics: Redex
A redex is a term of the form
((\x -> e1) e2)
Tnc Irs A function (\x -> e1)
2tE ly
54
L
I
t 5
x is the parameter
e1 is the returned expression
Applied to an argument e2 O
e2 is the argument
5
5
q
cse130 https://ucsd-cse130.github.io/wi21/lectures/01-lambda.html
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 ¡±
so
dx s.ae apple b apple
Computation by search-aDnd-replace:
If you see an abstraction applied to an argument, t
In the body of the abstraction
Replace all free occurrences of the formal by that argument
20 of 69 1/7/21, 8:59 AM
cse130 https://ucsd-cse130.github.io/wi21/lectures/01-lambda.html
We say that (\x -> e1) e2 ¦Â-steps to e1[x := e2] DD
e ez b et x ed
Csx
Redex Examples
((\x D-> x) apple)
=b> apple
Is this right? Ask Elsa (https://goto.ucsd.edu/elsa/index.html)
21 of 69 1/7/21, 8:59 AM
cse130
https://ucsd-cse130.github.io/wi21/lectures/01-lambda.html
QUIZ
((\x -> (\y -> y)) apple)
=b> ???
Ixia
b e xi
x
ez
A. apple
B. \y -> apple C. \x -> apple D. \y->y
E. \x->y
yay
w
eD
apple
22 of 69
1/7/21, 8:59 AM
cse130 https://ucsd-cse130.github.io/wi21/lectures/01-lambda.html
Ixe ez bex
=b> ???
A. (((apple apple) apple) apple)
QUIZ
papplepaple
Eez
(\x -> (((y x) y) x)) apple
e
B. (((y apple) y) apple) 00
C. (((y y) y) y) D. apple
QUIZ
23 of 69 1/7/21, 8:59 AM
I
cse130
QUIZ ajb i a
https://ucsd-cse130.github.io/wi21/lectures/01-lambda.html
((\x -> (x (\x -> x))) apple)
ix s.ec =b> ???
er
e Ex ez
A. (apple (\x -> x)) t
fix funcGE
B. (apple (\apple -> apple)) C. (apple (\x -> apple))
D. apple
E. (\x -> x)
x Ix
def
123
33 6
EXERCISE
What is a ¦Ë-term fill_this_in such that
ez
fill_this_in apple
=b> banana
apple
24 of 69 D banana
1/7/21, 8:59 AM
xE1 3
return
x
binder useloccurrences
cse130
https://ucsd-cse130.github.io/wi21/lectures/01-lambda.html
25 of 69
Xx e Imai
Targ HE’D apply
body D appleapple 1/7/21, 8:59 AM
ELSA: https://goto.ucsd.edu/elsa/index.html
Click here to try this exercise (https://goto.ucsd.edu /elsa/index.html#?demo=permalink%2F1585434473_24432.lc)
Ix s apple banana
A Tricky One
banga
((\x -> (\y -> x)) y) I =b>\y->y
Make sure yourIPATH is set Gsblw
rm rf n 1stack
Is this right?
z
SYNTAX
e
X y ej formal eez arg
x
apple
b
banana x
i
lx body
function
REDEX
to make
downloading GHC
26 of 69
1/7/21, 8:59 AM
I
dy pp cse130 e a ed
Something is Fishy
https://ucsd-cse130.github.io/wi21/lectures/01-lambda.html
M
formal
c
body y
igars l(\x -> (\y -> x)) y
=b> (\y -> y)
D
body
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 di!erent from free-variables of argument!
cse130 https://ucsd-cse130.github.io/wi21/lectures/01-lambda.html
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 allgfree 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]
(e1 e2)[x := e]
(\x -> e1)[x := e]
anged?
= y — as x /= y
= (e1[x := e]) (e2[x := e])
= (\x -> e1) — Q: Why leave `e1` unch
(\y -> e1)[x := e] |not(yinFV(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?
27 of 69 1/7/21, 8:59 AM
cse130
https://ucsd-cse130.github.io/wi21/lectures/01-lambda.html
Rewrite Rules of Lambda Calculus
1. ¦Â-step (aka function call)
2. ¦Á-step (aka renaming formals)
functional
Nti
funchonly
return
function
return Etl’s 5
return
ytl
5
Semantics: ¦Á-Renaming 28 of 69 7x y Fa XyA y
1/7/21, 8:59 AM
cse130
https://ucsd-cse130.github.io/wi21/lectures/01-lambda.html
f
\x->e =a> \y->e[x:=y] where not (y in FV(e))
x TyyaAtz 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
Xx
What¡¯s wrong with these?
— (A)
(\f -> (f x)) =a>
— (B)
((\x -> (\fy -> y)) y) 29 of 69
(\x -> (x x))
outsidescopeofbinder
=a> ((\x -> (\z -> z)) z)
1/7/21, 8:59 AM
cse130 https://ucsd-cse130.github.io/wi21/lectures/01-lambda.html
Tricky Example Revisited
((\x -> (\y -> x)) y)
ure
— rename ‘y’ to ‘z’ to avoid capt
— now do b-step without capture!
=a> ((\x -> (\z -> x)) y)
=b> (\z -> y)
To avoid getting confused,
you can always rename formals,
so di”erent variables have di”erent names!
30 of 69 1/7/21, 8:59 AM
cse130 https://ucsd-cse130.github.io/wi21/lectures/01-lambda.html
Normal Forms
Recall redex is a ¦Ë-term of the form ((\x -> e1) e2)
A ¦Ë-term is in normal form if it contains no redexes.
Xx
QUIZ
Which of the following term are not in normal form ?
y
A. x
no redex
ie containfurther b steps
b redexes
31 of 69 1/7/21, 8:59 AM
cse130
Y’t https://ucsd-cse130.github.io/wi21/lectures/01-lambda.html
32 of 69
1/7/21, 8:59 AM
B. (x y) noredexjb
XX ee If
S
ez
daring
C. ((\x -> x) y) se e e
D. (x (\y -> y)) E. C and D
yesredex no redex
Chet
Semantics: Evaluation
A ¦Ë-term e evaluates to e’ if
1. There is a sequence of steps
223 11
3
normal
e=?>e_1=?>…=?>e_N=?>e’
where each =?> is either =a> or =b> and N >= 0
2. e’ is in normal form
4
1
cse130 https://ucsd-cse130.github.io/wi21/lectures/01-lambda.html
Examples of Evaluation
((\xE-> x) apple) =b> apple
(\f -> f (\x -> x)) (\x -> x)
=?> ???
(\x -> x x) (\x -> x)
=?> ???
Elsa shortcuts
Named ¦Ë-terms:
let ID = (\x -> x) — abbreviation for (\x -> x)
33 of 69 1/7/21, 8:59 AM
cse130 https://ucsd-cse130.github.io/wi21/lectures/01-lambda.html
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
X
b
EXERCISE
xxx yy
y
ay ay
yy yy
Fill in the definitions of FIRST , SECOND and THIRD such that you get the
34 of 69 1/7/21, 8:59 AM
cse130
https://ucsd-cse130.github.io/wi21/lectures/01-lambda.html
35 of 69
1/7/21, 8:59 AM
following behavior in elsa let FIRST = fill_this_in
let SECOND = fill_this_in let THIRD = fill_this_in
eval ex1 : 1 3
Ix
sx
Kr 2
n apple orange lxz lxz x
FIRST apple banana orange
=*> apple
eval ex2 :
SECOND apple banana orange
=*> banana
eval ex3 :
THIRD apple banana orange
=*> orange
x
apple
ban
orange
Click here to try this exercise (https://goto.ucsd.edu /elsa/index.html#?demo=permalink%2F1585434130_24421.lc)
Non-Terminating Evaluation
((\x -> (x x)) (\x -> (x x)))
=b> ((\x -> (x x)) (\x -> (x x)))
Some programs loop back to themselves … never reduce to a normal form! This combinator is called ¦¸
ELSA: https://goto.ucsd.edu/elsa/index.html
Xx
ban
cse130 https://ucsd-cse130.github.io/wi21/lectures/01-lambda.html
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
Il
Il
Booleans T F ifthenelse
Records (structs, tuples) Numbers 2 5 liststrees
fest snd
se y Z
3
Functions [we got those]
Recursion
is
36 of 69 1/7/21, 8:59 AM
cse130 https://ucsd-cse130.github.io/wi21/lectures/01-lambda.html
Lets see how to encode all of these features with the ¦Ë-calculus.
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
37 of 69 1/7/21, 8:59 AM
cse130 https://ucsd-cse130.github.io/wi21/lectures/01-lambda.html
boollcond
TRUE
res true
How can we encode Boolean values ( TRUE and FALSE ) as functions?
Well, what do we do with a Boolean b ? decisionsIcondition choice
## ¦Ë-calculus: Booleans
FALSE
res
false
38 of 69 1/7/21, 8:59 AM
cse130 https://ucsd-cse130.github.io/wi21/lectures/01-lambda.html
Make a binary choice ifbthene1elsee2
St
b et ez
Booleans: API
We need to define three functions
let TRUE = ??? let FALSE = ???
let ITE such that
lx ly x
ly y
— if b then x else y
x
ix
= \b x y -> ???
a00 b
y
ITE TRUE apple banana =~> apple
ITE FALSE apple banana =~> banana
(Here, let NAME = e means NAME is an abbreviation for e )
39 of 69 1/7/21, 8:59 AM
cse130 https://ucsd-cse130.github.io/wi21/lectures/01-lambda.html
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 readabili
ty)
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
— beta-step
— beta-step
— expand def TRUE
— beta-step
— beta-step
=b>
=b>
=b>
=d>
=b>
=b> e1
(\x y -> TRUE x y)
(\y -> TRUE e1 y)
TRUE e1 e2
(\x y -> x) e1 e2
(\y -> e1) e2
e1 e2 e2
40 of 69 1/7/21, 8:59 AM
cse130 https://ucsd-cse130.github.io/wi21/lectures/01-lambda.html
Example: Branches step-by-step
Now you try it!
Can you fill in the blanks to make it happen? (http://goto.ucsd.edu:8095 /index.html#?demo=ite.lc)
eval ite_false:
ITE FALSE e1 e2
— fill the steps in!
=b> e2
41 of 69 1/7/21, 8:59 AM
cse130
https://ucsd-cse130.github.io/wi21/lectures/01-lambda.html
EXERCISE: Boolean Operators
ELSA: https://goto.ucsd.edu/elsa/index.html Click here to try this exercise (https://goto.ucsd.edu /elsa/index.html#?demo=permalink%2F1585435168_24442.lc)
Now that we have ITE it¡¯s easy to define other Boolean operators:
Clet NOT = \b -> ??? let OR = \b1 b2 -> ??? let AND = \b1 b2 -> ???
When you are done, you should get the following behavior:
42 of 69
1/7/21, 8:59 AM
cse130 https://ucsd-cse130.github.io/wi21/lectures/01-lambda.html
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
AND TT AND FF
FF ns FF FF ng FF
AND
AND
FF TT ng TT TT
FF
TT
43 of 69 1/7/21, 8:59 AM
cse130
https://ucsd-cse130.github.io/wi21/lectures/01-lambda.html
Oo Lambda deadline
Programming in ¦Ë-calculus Booleans [done]
1
17 2351
r
Records (structs, tuples) Numbers
Recursion
Fg applefbaria apple
SNF’t banana
¦Ë-calculus: Records 44 of 69
LISTS
Functions [we got those]
NOT NEEDED for 00 launder ECORD
1/7/21, 8:59 AM
cse130 https://ucsd-cse130.github.io/wi21/lectures/01-lambda.html
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.
ME
y
X
index
Pairs : API
We need to define three functions
ITE
Y
let PAIR = \x yf-> ??? let FST = \p -> ???
a
let SND = \p -> ??? y
— Make a pair with elements x and y
— { fst : x, snd : y }
— Return first element
— p.fst
— Return second element
— p.snd
45 of 69 1/7/21, 8:59 AM
cse130
https://ucsd-cse130.github.io/wi21/lectures/01-lambda.html
such that
eval ex_fst:
FST (PAIR apple banana) =*> apple
eval ex_snd:
SND (PAIR apple banana) =*> banana
let PAIR
It
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
let lets ND
FST
X
It
y
ITE b se y t TRUE
t FALSE
lb
46 of 69 1/7/21, 8:59 AM
cse130 https://ucsd-cse130.github.io/wi21/lectures/01-lambda.html
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 (https://goto.ucsd.edu /elsa/index.html#?demo=permalink%2F1585434814_24436.lc)
47 of 69 1/7/21, 8:59 AM
cse130
https://ucsd-cse130.github.io/wi21/lectures/01-lambda.html
let TRIPLE = \x y z -> ??? letFST3 =\t->??? letSND3 =\t->??? letTHD3 =\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
TRIP
PAIR AIR app
Orage
Dppfbanf.org
ban
PAKXy
Programming in ¦Ë-calculus 48 of 69
¦ÌPLEKyt
PAlR
2
1/7/21, 8:59 AM
cse130
https://ucsd-cse130.github.io/wi21/lectures/01-lambda.html
49 of 69
1/7/21, 8:59 AM
Booleans [done]
Records (structs, tuples) [done] Numbers
Functions [we got those] Recursion
Represent
D
ONE two
OI zero B
9
2,3
¦Ë-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
three
four
If
If Ix fff
INC
IMINUST
IcomparisonsJ
fx ffffx
one
cse130 https://ucsd-cse130.github.io/wi21/lectures/01-lambda.html
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
…
50 of 69 1/7/21, 8:59 AM
cse130
https://ucsd-cse130.github.io/wi21/lectures/01-lambda.html
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 let FIVE let SIX …
= \f x -> f (f (f (f x)))
= \f x -> f (f (f (f (f x))))
= \f x -> f (f (f (f (f (f x)))))
N Ifx fl
N
Cf times
x
r vinen
TWO f x THREE x
Nf
QUIZ: Church Numerals
Which of these is a valid encoding of ZERO ? 51 of 69
x
fff x
f Cfcf xD
fffff
for r fer f Car
N
times
n
1/7/21, 8:59 AM
cse130 https://ucsd-cse130.github.io/wi21/lectures/01-lambda.html
52 of 69
A: let ZERO = \f x -> x
B: let ZERO = \f x -> f
zero
times
C: let ZERO = \f x -> f x
D: letZERO=\x->x E: None of the above
Does this function look familiar?
doesnottake henc
as
1
5 ONE
¦Ë-calculus: Increment
— Call `f` on `x` one more time than `n` does
let INC
f ooze
N times
one moretime 1/7/21, 8:59 AM
e
= \n -> (\f x -> ???)
Timber Fm ¦Ìf’on re
n
ln
x
Gfx f f sffxfnff.es
asf
n
ONE
f
S f
L
cse130 https://ucsd-cse130.github.io/wi21/lectures/01-lambda.html
53 of 69 1/7/21, 8:59 AM
ONE ONE TWO
INC ZERO
INC Inc
SIX
SEVEN
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
cse130 https://ucsd-cse130.github.io/wi21/lectures/01-lambda.html
EXERCISE
Fill in the implementation of ADD so that you get the following behavior Click here to try this exercise (https://goto.ucsd.edu
/elsa/index.html#?demo=permalink%2F1585436042_24449.lc)
let ZERO = \f x -> x
let ONE let TWO let INC
= \f x -> f x
= \f x -> f (f x)
= \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
54 of 69 1/7/21, 8:59 AM
cse130
QUIZ let ADD
How shall we implement ADD ?
A. let ADD = \n m -> n INC m mine w
B. let ADD = \n m -> INC n m
C. let ADD = \n m -> n m INC
n
D. let ADD = \n m -> n (m INC)
E. let ADD = \n m -> n (INC m)
https://ucsd-cse130.github.io/wi21/lectures/01-lambda.html
55 of 69
1/7/21, 8:59 AM
¦Ë-calculus: Addition
— Call `f` on `x` exactly `n + m` times
let ADD = \n m -> n INC m
In m
NC Nc
NUMBER
Nc rn N times
cse130
https://ucsd-cse130.github.io/wi21/lectures/01-lambda.html
Example:
eval add_one_zero :
ADD ONE ZERO
=~> ONE
QUIZ
How shall we implement MULT ? i
no add takes 2
A. let MULT = \n m -> n ADD m
B. let MULT = \n m -> n (ADD m) ZERO
v
1 35
in
C. let MULT = \n m -> m (ADD n) ZERO
D. let MULT = \n m -> n (ADD m ZERO)x
E. let MULT = \n m -> (n ADD m) ZERO
n
m
nm
Nam
Gam
56 of 69
la
7aoisiicamtm.mIe
ht ht 0
1/7/21, 8:59 AM
cse130
n
https://ucsd-cse130.github.io/wi21/lectures/01-lambda.html
57 of 69
1/7/21, 8:59 AM
Dm
Dm
m0 x
MUL nm Nf
N
LADD x fCfCt
CADD M
Dm
Dm GADDmy0
¦Ë-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
x Times
cse130
https://ucsd-cse130.github.io/wi21/lectures/01-lambda.html
58 of 69
1/7/21, 8:59 AM
In INC THREEJ
INC conc Programming in ¦Ë-calculus
n
LADD
Booleans [done]
Records (structs, tuples) [done]
Numbers [done]
Lists
Functions [we got those] Recursion
In
f
It TRUE
ISZERO In
I
11
TRUE if n ZERO FALSE o w
TRUE
FALSE FALSE TRUE
¦Ë-calculus: Lists
Lets define an API to build lists in the ¦Ë-calculus.
An Empty List
In
nl2
onlycalledwhere n FO
minus
Iz
FALSE
PAIR
TRIPLE
cse130
https://ucsd-cse130.github.io/wi21/lectures/01-lambda.html
59 of 69
1/7/21, 8:59 AM
NIL
cows
hat
Constructing a list
A list with 4 elements
NIL
ZERO
ZERI
ht
PAIR FST SNT
101iTJJ
cantaloupe dragon banana cantaloupe dragon
CONS apple (CONS banana (CONS cantaloupe (CONS dragon NIL))) intuitively CONS h t creates a new list with dragon
head h tail t
Destructing a list
apple banana cantaloupe dragon
IL I
I
HEAD
TAIL
F sND l
HEAD l returns the first element of the list
e
TAIL l returns the rest of the list
HEAD (CONS apple (CONS banana (CONS cantaloupe (CONS dragon NI
L))))
=~> apple
TAIL (CONS apple (CONS banana (CONS cantaloupe (CONS dragon NI
L))))
=~> CONS banana (CONS cantaloupe (CONS dragon NIL)))
cse130 https://ucsd-cse130.github.io/wi21/lectures/01-lambda.html
¦Ë-calculus: Lists
let NIL = ??? let CONS = ??? let HEAD = ??? let TAIL = ???
eval exHd:
HEAD (CONS apple (CONS banana (CONS cantaloupe (CONS dragon NI
L))))
=~> apple
eval exTl
TAIL (CONS apple (CONS banana (CONS cantaloupe (CONS dragon NI
L))))
=~> CONS banana (CONS cantaloupe (CONS dragon NIL)))
60 of 69 1/7/21, 8:59 AM
cse130 https://ucsd-cse130.github.io/wi21/lectures/01-lambda.html
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 = ???
head
n
N TA’LLd
In
l
HEAD
eval nth1 : Nuhead
GetNth ZERO (CONS apple (CONS banana (CONS cantaloupe NIL)))
=~> apple
eval nth1 :
GetNth ONE (CONS apple (CONS banana (CONS cantaloupe NIL)))
=~> banana
tainainhead
eval nth2 :
GetNth TWO (CONS apple (CONS banana (CONS cantaloupe NIL)))
=~> cantaloupe
Click here to try this in elsa (https://goto.ucsd.edu /elsa/index.html#?demo=permalink%2F1586466816_52273.lc)
61 of 69 1/7/21, 8:59 AM
cse130 https://ucsd-cse130.github.io/wi21/lectures/01-lambda.html
xX NOT NEEDED
I want to write a function that sums up natural numbers up to n : let SUM = \n -> … — 0 + 1 + 2 + … + n
such that we get the following behavior
eval exSum0: SUM ZERO =~> ZERO
eval exSum1: SUM ONE =~> ONE
eval exSum2: SUM TWO =~> THREE
eval exSum3: SUM THREE =~> SIX
Can we write sum using Church Numerals?
Click here to try this in Elsa (https://goto.ucsd.edu
/elsa/index.html#?demo=permalink%2F1586465192_52175.lc)
x
FOR Oo LAM_
¦Ë-calculus: Recursion
QUIZ
62 of 69 1/7/21, 8:59 AM
cse130 https://ucsd-cse130.github.io/wi21/lectures/01-lambda.html
You can write SUM using numerals but its tedious. Is this a correct implementation of SUM ?
letSUM=\n->ITE(ISZn) 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 yet defined!
Recursion:
63 of 69 1/7/21, 8:59 AM
cse130 https://ucsd-cse130.github.io/wi21/lectures/01-lambda.html
Inside this function
Want to call the same function on DEC n
Looks like we can¡¯t do recursion!
Requires being able to refer to functions by name,
But ¦Ë-calculus functions are anonymous. Right?
¦Ë-calculus: Recursion Think again!
Recursion:
Instead of
64 of 69 1/7/21, 8:59 AM
cse130 https://ucsd-cse130.github.io/wi21/lectures/01-lambda.html
Inside this function I want to call the same function on DEC n Lets try
Inside this function I want to call some function rec on DEC n And BTW, I want rec 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 some magic to STEP , so rec is itself
\n -> ITE (ISZ n) ZERO (ADD n (rec (DEC n)))
That is, obtain a term MAGIC such that MAGIC =*> STEP MAGIC
65 of 69 1/7/21, 8:59 AM
cse130 https://ucsd-cse130.github.io/wi21/lectures/01-lambda.html
¦Ë-calculus: Fixpoint Combinator Wanted: a ¦Ë-term FIX such that
FIX STEP calls STEP with FIX STEP 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 =*> FIX STEP =*> STEP (FIX STEP) =*> STEP SUM
and so now we compute:
66 of 69 1/7/21, 8:59 AM
cse130 https://ucsd-cse130.github.io/wi21/lectures/01-lambda.html
eval sum_two:
SUM TWO
=*> STEP SUM TWO
=*> ITE (ISZ TWO) ZERO (ADD TWO (SUM (DEC TWO)))
=*> ADD TWO (SUM (DEC TWO))
=*> ADD TWO (SUM ONE)
=*> ADD TWO (STEP SUM ONE)
=*> ADD TWO (ITE (ISZ ONE) ZERO (ADD ONE (SUM (DEC ONE))))
=*> ADD TWO (ADD ONE (SUM (DEC ONE)))
=*> ADD TWO (ADD ONE (SUM ZERO))
=*> ADD TWO (ADD ONE (ITE (ISZ ZERO) ZERO (ADD ZERO (SUM DEC ZER
O)))
=*> ADD TWO (ADD ONE (ZERO))
=*> THREE
How should we define FIX ???
The Y combinator
Remember ¦¸?
67 of 69 1/7/21, 8:59 AM
cse130 https://ucsd-cse130.github.io/wi21/lectures/01-lambda.html
(\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, Haskell Curry was very clever.
Next week: We¡¯ll look at the language named after him ( Haskell )
68 of 69 1/7/21, 8:59 AM
cse130 https://ucsd-cse130.github.io/wi21/lectures/01-lambda.html
(https://ucsd-cse130.github.io/wi21/feed.xml) (https://twitter.com/ranjitjhala) (https://plus.google.com/u/0/104385825850161331469) (https://github.com/ranjitjhala)
Generated by Hakyll (http://jaspervdj.be/hakyll), template by Armin Ronacher (http://lucumr.pocoo.org), suggest improvements here (https://github.com /ucsd-progsys/liquidhaskell-blog/).
69 of 69 1/7/21, 8:59 AM