COMP0020: Functional Programming Section 2 : The Lambda Calculus
COMP0020 Functional Programming Lecture 2
The Lambda Calculus :
A Simple Introduction
Christopher D. Clack (University College London) COMP0020: Functional Programming Academic Year 2019-2020 1 / 18
COMP0020: Functional Programming Section 2 : The Lambda Calculus
Contents
Low-level target language and computational model for functional languages Very simple syntax
Simple rules for evaluation
Order of applying the rules
Terminology : “bound” and “free”
Christopher D. Clack (University College London) COMP0020: Functional Programming Academic Year 2019-2020 2 / 18
COMP0020: Functional Programming Section 2 : The Lambda Calculus
High-level functional languages may be translated by a compiler into the lambda calculus (though there are other implementation routes) ; the λ-calculus might then then translated to an even simpler run-time representation.
The λ-calculus is very simple — few operators and few rules
The λ-calculus views functions as rules for generating an answer given a certain input.
Although the λ-calculus was initially conceived as being sequential, there are many non-sequential implementations (e.g. much work was done in the 1980s to use functional languages – based on the λ-calculus – for parallel processing).
Christopher D. Clack (University College London) COMP0020: Functional Programming Academic Year 2019-2020 3 / 18
COMP0020: Functional Programming Section 2 : The Lambda Calculus
A program is an expression (like an arithmetic expression) rather than a sequence of instructions All a program does is to return a value
There are no “side effects” — the only purpose of the program is to return a value, and the only purpose of each part of the program is to return a value
In a programming language based on the λ-calculus, the value returned by the program might be an instruction to the operating system (e.g. to write to a file, or to print to the screen)
Christopher D. Clack (University College London) COMP0020: Functional Programming Academic Year 2019-2020 4 / 18
COMP0020: Functional Programming Section 2 : The Lambda Calculus
The Untyped (or “Type-Free”) Lambda Calculus Syntax
Untyped (or “Type-Free”) Lambda Calculus Syntax
program : :
expression : : |
|
expression
x
expression expression λx . expression
Variable : the name x indicates a variable name — it can be any name
Application : when one expression follows another, the former is normally taken to be a function and the latter is taken to be the argument, thus expression1 expression2 indicates the function expression1 applied to the argument expression2.
Abstraction : the lambda abstraction λx.expression indicates a function of one argument x and with function body expression. The name x can be used inside expression and represents the value to which the function is applied. We will assume that it is permissible for x to not appear inside expression (there are different versions of the λ-calculus : some permit this, and some do not).
Christopher D. Clack (University College London) COMP0020: Functional Programming Academic Year 2019-2020 5 / 18
COMP0020: Functional Programming Section 2 : The Lambda Calculus
The Untyped (or “Type-Free”) Lambda Calculus Syntax
The type-free λ-calculus can compute anything that is computable. However, the minimal syntax is cumbersome. For example, the numbers 0 and 1 are represented as functions : λf. λx . x
λf . λx . f x
The syntax is therefore often extended with : Constant values such as 3
Operators such as +, ×
Initially, all operators are prefix (the operator appears to the left of its argument(s)) Extra brackets for grouping (such as (x) )
Types (such as char, bool)
But we will not cover the typed lambda calculus 1
Lambda abstractions with more than one argument : these can already be accommodated as nested abstractions (e.g. λx.λy.expression or λx.(λy.expression)) but the syntax can be extended to permit the equivalent λx1x2.expression or in general λx1 . . . xn.expression
1. Note that whilst the untyped λ-calculus is Turing-equivalent, the typed λ-calculus typically is not (it depends on the properties of the type system)
Christopher D. Clack (University College London) COMP0020: Functional Programming Academic Year 2019-2020 6 / 18
COMP0020: Functional Programming Section 2 : The Lambda Calculus
The Untyped (or “Type-Free”) Lambda Calculus Syntax
Untyped Lambda Calculus — extended syntax
program expression
: :
: : | | | | |
expression
x
constant
operator
expression expression λx . expression (expression)
Christopher D. Clack (University College London) COMP0020: Functional Programming Academic Year 2019-2020 7 / 18
COMP0020: Functional Programming Section 2 : The Lambda Calculus
Lambda Calculus Functions
Lambda calculus functions
Functions do NOT have names !
Functions can be defined but must be used immediately Function arguments DO have names
that can only be used inside the function body (zero or more times) Functions can be arguments to other functions (they are higher order)
that way they can have names when they are passed as arguments to other functions
and can be used zero or more times inside the other function
and it is also possible for a function to return a function as its result
Christopher D. Clack (University College London) COMP0020: Functional Programming Academic Year 2019-2020 8 / 18
COMP0020: Functional Programming Section 2 : The Lambda Calculus
Lambda Calculus Functions
Defining and applying a Lambda calculus function
To define the (anonymous) function taking one argument (the argument is called x) which adds 1 to x and returns the sum as its result :
λx .((+x )1)
Often simplified to one of the following :
λx.(+x 1) [because function application associates to the left]
λx.(x + 1) [but we must extend the syntax to permit infix operators] To apply the previously defined function to the constant number 3 :
(λx.(x + 1)) 3
Christopher D. Clack (University College London) COMP0020: Functional Programming Academic Year 2019-2020 9 / 18
COMP0020: Functional Programming Section 2 : The Lambda Calculus
Extended Syntax with Infix Operators
Untyped Lambda Calculus — extended syntax with infix operators
program expression
: :
: : | | | | | |
expression
x
constant
operator
expression expression
expression operator expression λx . expression
(expression)
Christopher D. Clack (University College London) COMP0020: Functional Programming Academic Year 2019-2020 10 / 18
COMP0020: Functional Programming Section 2 : The Lambda Calculus
Lambda Calculus Reduction Rules
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
NB : E[y/x] means “for each free occurrence of x in E replace that x with y”. This becomes important if E contains another function definition that re-uses the name x for its argument. The embedded function definition binds the name x to a new value, thus the enclosing expression E sees all occurrences of x inside the embedded function definition as being bound (i.e. not free).
Christopher D. Clack (University College London) COMP0020: Functional Programming Academic Year 2019-2020 11 / 18
COMP0020: Functional Programming Section 2 : The Lambda Calculus
Lambda Calculus Reduction Rules
Terminology
Binding — a BINDING links a name to a value. This happens whenever a function is applied. Bound and Not Bound (a.k.a. “Free”). In the following expression :
(λx.(x + y))
we say that x is BOUND and y is NOT BOUND (alternatively, we say that y is FREE). This is because we know what value x refers to – it is the argument to this function, but the value of y is unknown (presumably this expression occurs inside the function body of a function that binds y, but we don’t know how deeply nested we might be inside function definitions inside other function definitions)
Christopher D. Clack (University College London) COMP0020: Functional Programming Academic Year 2019-2020 12 / 18
COMP0020: Functional Programming Section 2 : The Lambda Calculus
Lambda Calculus Reduction Rules
Order of evaluation (“reduction order”)
Normal Order Reduction
“leftmost-outermost” first
guaranteed to terminate (if termination is possible)
Other possible reduction orders
applicative order reduction
parallel reduction
All evaluation strategies are guaranteed to give the same result for an expression (caveat termination). That unique result is called the Normal Form of the expression.
Christopher D. Clack (University College London) COMP0020: Functional Programming Academic Year 2019-2020 13 / 18
COMP0020: Functional Programming Section 2 : The Lambda Calculus
Lambda Calculus Examples
Lambda Calculus Examples
Example 1 :
(5+3) →byδrulefor+ 8
Example 2 :
(λx .(x + 3)) 5
(5 + 3) 8
→ by β reduction → by δ rule for +
Example 3 :
(λy.((λx.(x + y)) 5)) 3 (λx .(x + 3)) 5
(5 + 3)
8
→ byβ reduction → by β reduction → by δ rule for +
Christopher D. Clack (University College London)
COMP0020: Functional Programming
Academic Year 2019-2020
14 / 18
COMP0020: Functional Programming Section 2 : The Lambda Calculus
Lambda Calculus Examples
Lambda Calculus Examples
Example 4 :
(λx.((λx.(x + 3)) x)) 5 (λy.((λx.(x + 3)) y)) 5 (λx .(x + 3)) 5
(5 + 3)
8
Example 5 :
(λx .(x 5)) (λx .(x + 3)) ((λx .(x + 3)) 5)
(5 + 3)
8
→ byα reduction → byβ reduction → by β reduction → by δ rule for +
→ by β reduction → by β reduction → by δ rule for +
Christopher D. Clack (University College London)
COMP0020: Functional Programming
Academic Year 2019-2020
15 / 18
COMP0020: Functional Programming Section 2 : The Lambda Calculus
Lambda Calculus Examples
Lambda Calculus Examples
Example 6 :
λx.((x 5) + (x 4)) (λx.(x + 3)) ((λx.(x + 3)) 5) + ((λx.(x + 3)) 4) (5 + 3) + ((λx.(x + 3)) 4)
(5 + 3) + (4 + 3)
8 + (4 + 3)
8 + 7
15
→ byβ reduction → byβ reduction → byβ reduction → by δ rule for + → by δ rule for + → by δ rule for +
Christopher D. Clack (University College London)
COMP0020: Functional Programming
Academic Year 2019-2020
16 / 18
COMP0020: Functional Programming Section 2 : The Lambda Calculus
Summary
Summary
Low-level target language and computational model for functional languages Very simple syntax
Only four rules for evaluation
Apply the rules in any order (caveat termination)
“Normal Order” guaranteed to terminate (if termination is possible) Terminology : “bound” and “free”
Christopher D. Clack (University College London) COMP0020: Functional Programming Academic Year 2019-2020 17 / 18
COMP0020: Functional Programming Section 2 : The Lambda Calculus
Summary
END OF LECTURE
Christopher D. Clack (University College London) COMP0020: Functional Programming Academic Year 2019-2020 18 / 18