COMP0020: Functional Programming Further Lambda Calculus
COMP0020 Functional Programming Lecture 3
Further Lambda Calculus
Christopher D. Clack (University College London) COMP0020: Functional Programming Academic Year 2019-2020 1 / 19
COMP0020: Functional Programming Further Lambda Calculus
Contents
Review : rules for evaluation
Review : representing numbers
β-reduction, name clashes and Free Variable Capture Reduction strategies and the Church Rosser theorem Different kinds of Normal Form
Christopher D. Clack (University College London) COMP0020: Functional Programming Academic Year 2019-2020 2 / 19
COMP0020: Functional Programming Further Lambda Calculus
Review : rules for evaluation
α-reduction
β-reduction
η-reduction
λx.E → λy.E[y/x]
(λx.E)z → E[z/x]
λx.(Ex) → E (if xisnotfreeinE)
δ-rules — there is a separate δ-rule for each operator (such as +, ×) ; e.g. the δ-rule for + says
that 3 + 4 evaluates to 7
Christopher D. Clack (University College London) COMP0020: Functional Programming Academic Year 2019-2020 3 / 19
COMP0020: Functional Programming Further Lambda Calculus
Review : η-reduction example
λx.((λx.(x + 1)) x) → In context (left hand side) :
λx.((λx.(x + 1)) x) 45 →
(λx.(x + 1))
(λx.(x + 1)) 45
(by η reduction)
(by β reduction)
Christopher D. Clack (University College London) COMP0020: Functional Programming
Academic Year 2019-2020
4 / 19
COMP0020: Functional Programming Further Lambda Calculus
Review : representing numbers
In the pure type-free λ-calculus there are no constants.
In the previous lecture we said that we can represent 0 and 1 by λf.λx.x and λf.λx.(f x). This extends to all whole numbers : e.g. the number 3 is represented by λf.λx.(f (f (f x)))
What makes this an effective representation is that we can write λ-calculus functions to perform arithmetic on thsese representation. For example, it is possible to write a function λx.λy.E that will take a representation of the number 1 and a representation of the number 2 and performs addition to return a representation of the number 3.
Challenge — can you write the λ-calculus function for addition, given this representation of numbers ?
Christopher D. Clack (University College London) COMP0020: Functional Programming Academic Year 2019-2020 5 / 19
COMP0020: Functional Programming Further Lambda Calculus
Name Clashes
Name Clashes
Example “name clash” with embedded function definitions using the same variable name : (λx.((λx.(x + 3)) (x + 4))) 5
Using a normal order reduction strategy, the next step is a β-reduction using the rule
(λx.E) z → E[z/x] where z = 5 and E = ((λx.(x + 3)) (x + 4)), but which occurrences of x in E should be replaced with z during the β-reduction? (NB we would never replace the x in “λx”)
→ ((λx.(5+3))(x+4)) ?
→ ((λx.(x+3))(5+4)) ?
→ ((λx.(5+3))(5+4)) ?
NB : E[z/x] means “for each free occurrence of x in E replace that x with z”. It can help to annotate each occurrence of x according to whether it is bound or free, as follows :
E = ((λx.(xbound + 3)) (xfree + 4)). Thus, the correct reduction result is ((λx.(x + 3)) (5 + 4))
Christopher D. Clack (University College London) COMP0020: Functional Programming Academic Year 2019-2020 6 / 19
COMP0020: Functional Programming Further Lambda Calculus
Free Variable Capture
Free Variable Capture
For β-reduction, identifying free variables in E is not enough!
Consider the “free variable capture” problem as demonstrated by the following example
subexpression where the first a is bound and the second a (in the argument) is free : 1 (λf.(λa.(f a))) (λf.(f a))
This β-reduces to the following, where both copies of the name a are now bound (the second a, previously free, has been “captured” and is now bound by the λa, which is not the behaviour we want) :
(λa.((λf .(f a)) a))
So β-reduction needs to be more sophisticated in the way that it operates.
1. Assume this subexpression is part of a larger enclosing expression which contains a lambda binding for the second a. Christopher D. Clack (University College London) COMP0020: Functional Programming Academic Year 2019-2020 7 / 19
COMP0020: Functional Programming Further Lambda Calculus
Free Variable Capture
Avoiding Free Variable Capture
During β-reduction of (λx.E) z, if z is an expression that contains any free variables that are bound inside E, then each such free variable must be α-converted inside E before performing the β-reduction substitution.
Thus :
(λf .(λa.(f a))) (λf .(f a)) → α reduce λa to λb (λf .(λb.(f b))) (λf .(f a)) → by β reduction (λb.((λf .(f a)) b))
Christopher D. Clack (University College London) COMP0020: Functional Programming Academic Year 2019-2020 8 / 19
COMP0020: Functional Programming Further Lambda Calculus
Reduction Strategies
Reduction Strategies
Any expression that matches the left-hand-side of a reduction rule is called a “reducible expression” or “redex”
An expression containing no redexes is said to be in “Normal Form” (or “NF”)
Execution is the successive application of reduction rules (primarily β-reduction) until Normal Form is reached.
Whether an arbitrary expression E has a NF is undecideable (it is equivalent to the Halting Problem).
Many different sequences of reductions are possible — how does this affect the result ?
Christopher D. Clack (University College London) COMP0020: Functional Programming Academic Year 2019-2020 9 / 19
COMP0020: Functional Programming Further Lambda Calculus
Reduction Strategies
Church-Rosser Theorem
The Church-Rosser theorem states that all reduction sequences (strategies) that terminate will converge on the same Normal Form.
Corollary : the Normal Form, for a given expression is unique (if it exists)
So β-reductions can be performed in any order (even in parallel!).
Christopher D. Clack (University College London) COMP0020: Functional Programming Academic Year 2019-2020 10 / 19
COMP0020: Functional Programming Further Lambda Calculus
Reduction Strategies
Normalising orders
Not all reduction strategies (orders of performing reductions) terminate
So which should we choose ?
Normal Order Reduction (“leftmost-outermost-first”) is guaranteed to terminate if termination is possible
Strategies that are guaranteed to terminate are called “normalising” reduction orders
Christopher D. Clack (University College London) COMP0020: Functional Programming Academic Year 2019-2020 11 / 19
COMP0020: Functional Programming Further Lambda Calculus
Reduction Strategies
Comparing strategies
Normal Order Reduction
“leftmost-outermost first”
Safe, but can be slow
Similar to “call-by-reference” passing of function arguments (though simple implementations can
suffer from duplication)
(λx.(x+x)) (3+5) →byβreduction → ((3+5)+(3+5))
(λx.3) ((λx.(x x)) (λx.(x x))) → by β reduction → 3
Applicative Order Reduction
“leftmost-innermost first”
Fast, but unsafe (may not terminate)
Similar to “call by value” passing of function arguments
(λx.(x +x)) (3+5) → by δ reduction → (λx.(x +x)) 8
(λx.3) ((λx.(x x)) (λx.(x x))) → by β reduction → (λx.3) ((λx.(x x)) (λx.(x x)))
Christopher D. Clack (University College London) COMP0020: Functional Programming Academic Year 2019-2020 12 / 19
COMP0020: Functional Programming Further Lambda Calculus
Different kinds of Normal Form
Different kinds of Normal Form
Practical implementations almost never reduce to full Normal Form (to avoid wasted computation)
Weak Head Normal Form (WHNF) and Head Normal Form (HNF) are successive stopping points on the journey to full Normal Form
The definitions consider all possible syntactic variants of an expression. Here we give definitions in terms of the simple untyped λ-calculus only, where an expression can either be a variable, an application, or a lambda abstraction (a function definition). 2
2. If we were to add data constructors to the lambda calculus (which is not strictly necessary), we would extend the definitions appropriately.
Christopher D. Clack (University College London) COMP0020: Functional Programming Academic Year 2019-2020 13 / 19
COMP0020: Functional Programming Further Lambda Calculus
Different kinds of Normal Form
Definition
An expression is in Normal Form if it does not contain a redex
Variable : x is in Normal Form
Application : MN is in Normal Form if M,N are in Normal Form and M is not a lambda abstraction Abstraction : (λx.E) is in Normal Form if E is in Normal Form
Normal Form is unique.
Christopher D. Clack (University College London) COMP0020: Functional Programming Academic Year 2019-2020 14 / 19
COMP0020: Functional Programming Further Lambda Calculus
Different kinds of Normal Form
Definition
An expression M is in Head Normal Form if it is of the form M≡λx1…xn .xN1…Nm wheren,m≥0andxisavariable
Note that in the above definition x is the “head variable”
Variable : x is in Head Normal Form (consider the definition where n = m = 0) Application : xN1 …Nm is in Head Normal Form (consider n = 0,m ≥ 1)3 Abstraction : λx.E is in Head Normal Form if E is in Head Normal Form
Head Normal Form is not unique.
3. We assume that the variable x will be bound to a lambda abstraction by some enclosing expression — here we just consider whether this subexpression is in HNF.
Christopher D. Clack (University College London) COMP0020: Functional Programming Academic Year 2019-2020 15 / 19
COMP0020: Functional Programming Further Lambda Calculus
Different kinds of Normal Form
Definition
An expression M is in Weak Head Normal Form if it is of one of the following two forms : M≡λx1…xn .xN1…Nm wheren,m≥0andxisavariable
or
M ≡ λx.N
Variable : x is in Weak Head Normal Form Application : xN is in Weak Head Normal Form Abstraction : λx.E is in Weak Head Normal Form
Weak Head Normal Form is not unique.
Christopher D. Clack (University College London) COMP0020: Functional Programming Academic Year 2019-2020 16 / 19
COMP0020: Functional Programming Further Lambda Calculus
Different kinds of Normal Form
Examples
WHNF
HNF
NF
λx .((λy .(+)) 4 (5 + 6))
λx.(+ (5 + 6))
λx.(+ 11)
Christopher D. Clack (University College London)
COMP0020: Functional Programming
Academic Year 2019-2020
17 / 19
COMP0020: Functional Programming Further Lambda Calculus
Different kinds of Normal Form
Summary
Review : rules for evaluation
β-reduction, name clashes and Free Variable Capture Reduction strategies and the Church Rosser theorem Different kinds of Normal Form
Christopher D. Clack (University College London) COMP0020: Functional Programming Academic Year 2019-2020 18 / 19
COMP0020: Functional Programming Further Lambda Calculus
Different kinds of Normal Form
END OF LECTURE
Christopher D. Clack (University College London) COMP0020: Functional Programming Academic Year 2019-2020 19 / 19