CSE230 Slides 01: Lambda Calculus
Excerpt
UCSD CSE 230
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
Alonzo Church
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, …ConditionalsLoopsreturn
,break
,continue
- Functions
RecursionReferences / pointersObjects and classesInheritanceReflection
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
computee
”
- 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
andy
and returnsy
?
How do I apply a function to two arguments?
- e.g. apply
\x -> (\y -> y)
toapple
andbanana
?
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
- β-step (aka function call)
- α-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 ofx
-
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. 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
EXERCISE: 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
- β-step (aka function call)
- α-step (aka renaming formals)
Semantics: Redex
A redex is a term of the form
A function (\x -> e1)
x
is the parametere1
is the returned expression
Applied to an argument e2
e2
is the argument
Semantics: β-Reduction
A redex b-steps to another term …
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 toe1[x := e2]
Redex Examples
Is this right? Ask Elsa!
QUIZ
A. apple
B. \y -> apple
C. \x -> apple
D. \y -> y
E. \x -> y
QUIZ
A. apple apple apple apple
B. y apple y apple
C. y y y y
D. apple
QUIZ
A. apple (\x -> x)
B. apple (\apple -> apple)
C. apple (\x -> apple)
D. apple
E. \x -> x
EXERCISE
What is a λ-term fill_this_in
such that
ELSA: https://goto.ucsd.edu/elsa/index.html
Click here to try this exercise
A Tricky One
Is this right?
Something is Fishy
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:
where e1[x := e2]
means “e1
with all free occurrences of x
replaced with e2
”
e1
with all free occurrences ofx
replaced withe2
- as long as no free variables of
e2
get captured
Formally:
Oops, but what to do if y
is in the free-variables of e
?
- i.e. if
\y -> ...
may capture those free variables?
Rewrite Rules of Lambda Calculus
- β-step (aka function call)
- α-step (aka renaming formals)
Semantics: α-Renaming
-
We rename a formal parameter
x
toy
-
By replace all occurrences of
x
in the body withy
-
We say that
\x -> e
α-steps to\y -> e[x := y]
Example:
All these expressions are α-equivalent
What’s wrong with these?
Tricky Example Revisited
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
B. x y
C. (\x -> x) y
D. x (\y -> y)
E. C and D
Semantics: Evaluation
A λ-term e
evaluates to e'
if
- There is a sequence of steps
where each =?>
is either =a>
or =b>
and N >= 0
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 toe2
in 0 or more steps- where each step is
=a>
,=b>
, or=d>
- where each step is
e1 =~> e2
:e1
evaluates toe2
ande2
is in normal form
EXERCISE
Fill in the definitions of FIRST
, SECOND
and THIRD
such that you get the following behavior in elsa
ELSA: https://goto.ucsd.edu/elsa/index.html
Click here to try this exercise
Non-Terminating Evaluation
Some programs 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?
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:
When you are done, you should get the following behavior:
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?
- Pack two items into a pair, then
- Get first item, or
- 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?
ELSA: https://goto.ucsd.edu/elsa/index.html
Click here to try this exercise
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:
EXERCISE
Fill in the implementation of ADD
so that you get the following behavior
Click here to try this exercise
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]
- Lists
- Functions [we got those]
- Recursion
λ-calculus: Lists
Lets define an API to build lists in the λ-calculus.
An Empty List
Constructing a list
A list with 4 elements
intuitively CONS h t
creates a new list with
- head
h
- tail
t
Destructing a list
HEAD l
returns the first element of the listTAIL l
returns the rest of the list
λ-calculus: Lists
EXERCISE: Nth
Write an implementation of GetNth
such that
GetNth n l
returns the n-th element of the listl
Assume that l
has n or more elements
Click here to try this in elsa
λ-calculus: Recursion
I want to write a function that sums up natural numbers up to n
:
such that we get the following behavior
Can we write sum using Church Numerals?
Click here to try this in Elsa
QUIZ
You can write SUM
using numerals but its tedious.
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
- 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
- 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
onDEC n
- And BTW, I want
rec
to be the same function
Step 1: Pass in the function to call “recursively”
Step 2: Do some magic to STEP
, so rec
is itself
That is, obtain a term MAGIC
such that
λ-calculus: Fixpoint Combinator
Wanted: a λ-term FIX
such that
FIX STEP
callsSTEP
withFIX STEP
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:
and so now we compute:
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, Haskell Curry was very clever.
Next week: We’ll look at the language named after him (Haskell
)