COMP2022: Formal Languages and Logic – 2018, Semester 2, Week 1
COMP2022: Formal Languages and Logic
2018, Semester 2, Week 1
Joseph Godbehere
2nd August, 2018
COMMONWEALTH OF AUSTRALIA
Copyright Regulations 1969
WARNING
This material has been reproduced and communicated to you by or
on behalf of the University of Sydney pursuant to part VB of the
Copyright Act 1968 (the Act).
The material in this communication may be subject to copyright
under the Act. Any further copying or communication of this
material by you may be subject of copyright protect under the Act.
Do not remove this notice.
Background Math notions Fun Programming Lambda Calculus Review
Outline
▶ Why study formal languages and logic?
▶ Mathematical notions and definitions
▶ Introduction to Functional Programming
▶ Introduction to the lambda calculus
3/46
Background Math notions Fun Programming Lambda Calculus Review
Why should we study theory?
Computers are complex machines and theory provides a new
viewpoint, an elegant side to computation
Studying theory expands your mind. IT evolves quickly. Whilst
specific technical knowledge is quickly outdated, theory is not.
▶ Know how to express yourself clearly
▶ Know how to prove your work
▶ Know when you have, or have not, solved a problem.
Theory provides conceptual tools which are used in computer
engineering
4/46
Background Math notions Fun Programming Lambda Calculus Review
How this course will help
Most problems in computer science involve answering:
▶ Can the problem be solved by a computer program?
▶ If not, can you modify the problem so that it can?
▶ If so, can a program solve the problem in workable time?
▶ Can you prove that your program is correct?
▶ Can you prove that your program is efficient?
5/46
Background Math notions Fun Programming Lambda Calculus Review
How this course will help
Lambda calculus (functional programming paradigm)
▶ Relationships between data
▶ Some notable properties:
▶ Elegant
▶ Efficiency – parallelism, laziness
▶ Security
▶ Some example uses:
▶ implementing programming languges (compilers)
▶ concurrent and parallel systems
▶ secure systems
▶ … and more generally, anything computable
6/46
Background Math notions Fun Programming Lambda Calculus Review
How this course will help
Automata Theory (imperative programming paradigm)
▶ Transformations of program state
▶ Some notable properties:
▶ Easy to design
▶ Easy to reason about
▶ Some example uses:
▶ Text processing / pattern matching (e.g. regular expressions)
▶ Model checking (e.g. to verify correctness of communication
protocols and electronic circuits)
▶ Agent based game ‘AI’
▶ Hardware design
▶ …
7/46
Background Math notions Fun Programming Lambda Calculus Review
How this course will help
Formal languages (grammars, especially context-free grammars)
▶ How we structure information
▶ Some example uses:
▶ Compilers and programming langauges (syntax)
▶ Natural Language Processing (e.g. machine translation, AI)
▶ Data storage (e.g. XML)
▶ …
8/46
Background Math notions Fun Programming Lambda Calculus Review
How this course will help
Logic: Meaning
▶ Program logic – logic gates, conditional statements
▶ Software verification
▶ Databases
▶ Artificial Intelligence
▶ Automated Reasoning
▶ …
9/46
Background Math notions Fun Programming Lambda Calculus Review
Understanding limitations of computing
▶ When developing solutions to real problems, we need to
understand the limitations of what software can do, and
design solutions which are realistic and efficient.
▶ Undecidable problems: no program/algorithm can do it (for all
possible inputs)
▶ Intractable problems: there could be programs/algorithms, but
too slow to be usable
▶ Theory will help you understand and recognise these
10/46
Background Math notions Fun Programming Lambda Calculus Review
Course topics
▶ Lambda Calculus
▶ Rewrite rules, reductions
▶ Encodings, commutative diagrams
▶ y-combinator, functional programming
▶ Automata Theory
▶ Regular Languages
▶ Finite automata, regular expressions
▶ Context-free Languages
▶ Pushdown Automata, C-F grammars, parsers
▶ Turing Machines
▶ Church-Turing thesis
▶ Computability, decidability, tractability
▶ Logic
▶ Propositional and predicate logic
▶ Logic formal proofs
11/46
Background Math notions Fun Programming Lambda Calculus Review
Gottfried Wilhelm Leibniz
▶ Polymath and Philosopher (17th C)
▶ Amongst MANY achievements, invents the
Entscheidungsproblem
1. Suppose we have a univeral language in
which all problems can be stated (e.g. set
theory + predicate logic)
2. Can we find a decision method to solve all
the problems?
12/46
Background Math notions Fun Programming Lambda Calculus Review
Alonzo Church
▶ Mathematician, logician
▶ Created lambda calculus
▶ Proved that the Entscheidungsproblem is
undecidable
▶ Proved Peano arithmetic is undeciable
▶ Church-Turing thesis
13/46
Background Math notions Fun Programming Lambda Calculus Review
Alan Turing
▶ Founder of computer science, mathematician,
philosopher, code breaker, visionary
▶ Created abstract machines called Turing
machines in the 1930s, before computers
existed
▶ Church-Turing thesis
▶ Turing test
▶ Can machines think?
▶ The Imitation Game
▶ Enigma code breaker
14/46
Background Math notions Fun Programming Lambda Calculus Review
Noam Chomsky
▶ Linguist, philosopher, cognitive scientist,
logician, historian, political critic and activist
▶ Chomsky Hierarchy: a containment hierarchy
of classes of formal languages (applies to
human language and computer theory)
Regular
(DFA)
Context-
free
(PDA)
Context-
sensitive
(LBA)
Recursively-
enumerable
(TM)
15/46
Background Math notions Fun Programming Lambda Calculus Review
Outline
▶ Why study formal languages and logic?
▶ Mathematical notions and definitions
▶ Introduction to Functional Programming
▶ Introduction to the lambda calculus
16/46
Background Math notions Fun Programming Lambda Calculus Review
Set
Set: An unordered group of unique objects
▶ unordered: A = {a, b, c} = {b, c, a} = {c, b, a}
▶ contains: a ∈ A denotes that a is in A
▶ subsets: if X ⊆ A then every element x ∈ X is also in A
▶ {a, c} ⊆ A
▶ {b} ⊆ A
▶ {a, d} ̸⊆ A
▶ size: |A| denotes the number of objects in A
▶ The empty set contains no elements (denoted ∅ or {})
17/46
Background Math notions Fun Programming Lambda Calculus Review
2-Tuple
Pair or 2-Tuple: an ordered list of two objects
▶ ordered: (a, b) ̸= (b, a)
▶ duplicates allowed: (a, a) is allowed
18/46
Background Math notions Fun Programming Lambda Calculus Review
Set Operations
▶ Union
▶ Denoted A ∪ B
▶ The set of elements belonging to at least one of A or B
▶ x ∈ A ∪ B if and only if x ∈ A or x ∈ B (or both)
▶ Intersection
▶ Denoted A ∩ B
▶ The set of elements belonging to both A and B
▶ x ∈ A ∩ B if and only if x ∈ A and x ∈ B
▶ Subtraction
▶ Denoted A \ B
▶ The set of elements belonging to A which do not belong to B
▶ x ∈ A \ B if and only if x ∈ A and not x ∈ B
19/46
Background Math notions Fun Programming Lambda Calculus Review
Set Operations
▶ Union
▶ Denoted A ∪ B
▶ The set of elements belonging to at least one of A or B
▶ x ∈ A ∪ B if and only if x ∈ A or x ∈ B (or both)
▶ Intersection
▶ Denoted A ∩ B
▶ The set of elements belonging to both A and B
▶ x ∈ A ∩ B if and only if x ∈ A and x ∈ B
▶ Subtraction
▶ Denoted A \ B
▶ The set of elements belonging to A which do not belong to B
▶ x ∈ A \ B if and only if x ∈ A and not x ∈ B
19/46
Background Math notions Fun Programming Lambda Calculus Review
Set Operations
▶ Union
▶ Denoted A ∪ B
▶ The set of elements belonging to at least one of A or B
▶ x ∈ A ∪ B if and only if x ∈ A or x ∈ B (or both)
▶ Intersection
▶ Denoted A ∩ B
▶ The set of elements belonging to both A and B
▶ x ∈ A ∩ B if and only if x ∈ A and x ∈ B
▶ Subtraction
▶ Denoted A \ B
▶ The set of elements belonging to A which do not belong to B
▶ x ∈ A \ B if and only if x ∈ A and not x ∈ B
19/46
Background Math notions Fun Programming Lambda Calculus Review
Power Set
P(A) denotes the Power Set of A, which is the set of all the
subsets of A.
▶ Including ∅, the empty set
Examples:
▶ If A = {0, 1} then P(A) = {∅, {0}, {1}, {0, 1}}
▶ If A = {a, b, c} then
P(A) = {∅, {a}, {b}, {c}, {a, b}, {a, c}, {b, c}, {a, b, c}}
20/46
Background Math notions Fun Programming Lambda Calculus Review
Cartesian product of two sets A and B
▶ The set of all pairs where the first element is in A and the
second element is in B , denoted A× B
▶ (x , y) ∈ A× B if and only if x ∈ A and y ∈ B
▶ {0, 1} × {a, b} = {(0, a), (0, b), (1, a), (1, b)}
21/46
Background Math notions Fun Programming Lambda Calculus Review
Function f : A → B
▶ Defines an input-output relationship from the set A to B
▶ The set of possible inputs to f is the domain D ⊆ A
▶ The set of possible outputs is the co-domain, or range R ⊆ B
▶ For each a ∈ D , f produces exactly one output f (a) ∈ R.
▶ multiple inputs can produce the same output
▶ i.e. a many-to-one function
▶ e.g. if A = {0, 1, 2},B = {a, b}, then we might define
f : A → B as f (0) = f (1) = a and f (2) = b
▶ f can be thought of as a subset of A× B
▶ e.g. in the example above, f = {(0, a), (1, a), (2, b)}
22/46
Background Math notions Fun Programming Lambda Calculus Review
Outline
▶ Why study formal languages and logic?
▶ Mathematical notions and definitions
▶ Introduction to Functional Programming
▶ Introduction to the lambda calculus
23/46
Background Math notions Fun Programming Lambda Calculus Review
Historical Origins
▶ The imperative and functional models grew out of work
undertaken Alan Turing, Alonzo Church, Stephen Kleene,
Emil Post, etc. ∼1930’s�
▶ different formalizations of the notion of an algorithm, or
effective procedure, based on automata, symbolic manipulation
recursive function definitions, and combinatorics
▶ These results led Church to conjecture that any intuitively
appealing model of computing would be equally powerful as
well�
▶ This conjecture is known as Church’s thesis
24/46
Background Math notions Fun Programming Lambda Calculus Review
Historical Origins
Turing’s model of computing was the Turing machine, a sort of
pushdown automaton using an unbounded storage “tape”
▶ The Turing machine computes in an imperative way, by
changing the values written on its tape, analogous to how
higher level imperative programs compute by changing the
values of variables.
▶ We will explore this when we cover Automata Theory in the
middle part of this unit of study.
25/46
Background Math notions Fun Programming Lambda Calculus Review
Historical Origins
▶ Church’s model of computation is called the Lambda
Calculus
▶ Based on the notation of parameterised expressions, with each
parameter introduced by a letter λ (lambda)
▶ Lambda calculus was the inspiration for functional
programming
▶ You can use it to compute by substituting parameters into
expressions, like passing arguments to functions
26/46
Background Math notions Fun Programming Lambda Calculus Review
Functional Programming Concepts
▶ Functional languages are an attempt to realize Church’s
lambda calculus in practical form as a programming language
▶ e.g. Lisp, Scheme, FP, ML, Miranda, Haskell, …
▶ The key idea: do everything by function composition
▶ No mutable state → no side effects
27/46
Background Math notions Fun Programming Lambda Calculus Review
Expressions
▶ Expressions are compositions of functions
▶ Constants are functions with no domains (e.g. f() = 1)
▶ Examples:
append ( append ( ”a” , ”b” ) , ” c ” )
( i f x ( i f y 1 2) 3)
28/46
Background Math notions Fun Programming Lambda Calculus Review
Programs
▶ A functional program is an expression E , which represents
both the program and the input
▶ We compute E by reducing it using rewrite rules
▶ Each reduction replaces some subexpression P of E with P ′ by
applying one of the rewrite rules
▶ Schematic representation:
E [P ] → E [P ′]
where P → P ′ holds according to the rewrite rules
▶ This process is repeated until no more reductions are
applicable
▶ We say the resulting expression is in Normal Form
29/46
Background Math notions Fun Programming Lambda Calculus Review
Programs
▶ A functional program is an expression E , which represents
both the program and the input
▶ We compute E by reducing it using rewrite rules
▶ Each reduction replaces some subexpression P of E with P ′ by
applying one of the rewrite rules
▶ Schematic representation:
E [P ] → E [P ′]
where P → P ′ holds according to the rewrite rules
▶ This process is repeated until no more reductions are
applicable
▶ We say the resulting expression is in Normal Form
29/46
Background Math notions Fun Programming Lambda Calculus Review
Programs
▶ A functional program is an expression E , which represents
both the program and the input
▶ We compute E by reducing it using rewrite rules
▶ Each reduction replaces some subexpression P of E with P ′ by
applying one of the rewrite rules
▶ Schematic representation:
E [P ] → E [P ′]
where P → P ′ holds according to the rewrite rules
▶ This process is repeated until no more reductions are
applicable
▶ We say the resulting expression is in Normal Form
29/46
Background Math notions Fun Programming Lambda Calculus Review
Programs
▶ A functional program is an expression E , which represents
both the program and the input
▶ We compute E by reducing it using rewrite rules
▶ Each reduction replaces some subexpression P of E with P ′ by
applying one of the rewrite rules
▶ Schematic representation:
E [P ] → E [P ′]
where P → P ′ holds according to the rewrite rules
▶ This process is repeated until no more reductions are
applicable
▶ We say the resulting expression is in Normal Form
29/46
Background Math notions Fun Programming Lambda Calculus Review
Programs
▶ A functional program is an expression E , which represents
both the program and the input
▶ We compute E by reducing it using rewrite rules
▶ Each reduction replaces some subexpression P of E with P ′ by
applying one of the rewrite rules
▶ Schematic representation:
E [P ] → E [P ′]
where P → P ′ holds according to the rewrite rules
▶ This process is repeated until no more reductions are
applicable
▶ We say the resulting expression is in Normal Form
29/46
Background Math notions Fun Programming Lambda Calculus Review
Programs
▶ A functional program is an expression E , which represents
both the program and the input
▶ We compute E by reducing it using rewrite rules
▶ Each reduction replaces some subexpression P of E with P ′ by
applying one of the rewrite rules
▶ Schematic representation:
E [P ] → E [P ′]
where P → P ′ holds according to the rewrite rules
▶ This process is repeated until no more reductions are
applicable
▶ We say the resulting expression is in Normal Form
29/46
Background Math notions Fun Programming Lambda Calculus Review
Example
▶ Consider these rewrite rules (a reduction system)
▶ a + b 7→ c where c is the addition of a and b
▶ a × b 7→ c where c is the multiplication of a and b
▶ … and this algebraic expression: (1 + 2)× (3 + 2)
▶ Reductions into Normal Form:
Step E P P ′ rule
1 (1 + 2)× (3 + 2) 1 + 2 3 a + b 7→ c
2 3× (3 + 2) 3 + 2 5 a + b 7→ c
3 3× 5 3× 5 15 a × b 7→ c
4 15
30/46
Background Math notions Fun Programming Lambda Calculus Review
Example
▶ Consider these rewrite rules (a reduction system)
▶ a + b 7→ c where c is the addition of a and b
▶ a × b 7→ c where c is the multiplication of a and b
▶ … and this algebraic expression: (1 + 2)× (3 + 2)
▶ Reductions into Normal Form:
Step E P P ′ rule
1 (1 + 2)× (3 + 2) 1 + 2 3 a + b 7→ c
2 3× (3 + 2) 3 + 2 5 a + b 7→ c
3 3× 5 3× 5 15 a × b 7→ c
4 15
30/46
Background Math notions Fun Programming Lambda Calculus Review
Church-Rosser Property
Reduction systems are usually designed to satisfy the
Church-Rosser property – that an expression’s normal form is
independent of the order of evaluation of the subexpressions.
Step E P P ′ rule
1 (1 + 2)× (3 + 2) 1 + 2 3 a + b 7→ c
2 3× (3 + 2) 3 + 2 5 a + b 7→ c
3 3× 5 3× 5 15 a × b 7→ c
4 15
Step E P P ′ rule
1 (1 + 2)× (3 + 2) 3 + 2 5 a + b 7→ c
2 (1 + 2)× 5 1 + 2 3 a + b 7→ c
3 3× 5 3× 5 15 a × b 7→ c
4 15
31/46
Background Math notions Fun Programming Lambda Calculus Review
Outline
▶ Why study formal languages and logic?
▶ Mathematical notions and definitions
▶ Introduction to Functional Programming
▶ Introduction to the lambda calculus
32/46
Background Math notions Fun Programming Lambda Calculus Review
Application
The first basic operation of the λ-calculus is application:
(F ·A)
denotes the application of some algorithm F to some input A.
For example, suppose A was simply the number 3, and F was the
function x 7→ x + 1, then the normal form of (F ·A) would be 4.
Often, we omit the · and simply write FA.
33/46
Background Math notions Fun Programming Lambda Calculus Review
Application
The first basic operation of the λ-calculus is application:
(F ·A)
denotes the application of some algorithm F to some input A.
For example, suppose A was simply the number 3, and F was the
function x 7→ x + 1, then the normal form of (F ·A) would be 4.
Often, we omit the · and simply write FA.
33/46
Background Math notions Fun Programming Lambda Calculus Review
Application
The first basic operation of the λ-calculus is application:
(F ·A)
denotes the application of some algorithm F to some input A.
For example, suppose A was simply the number 3, and F was the
function x 7→ x + 1, then the normal form of (F ·A) would be 4.
Often, we omit the · and simply write FA.
33/46
Background Math notions Fun Programming Lambda Calculus Review
Application
Note that F and A can be arbitrary expressions.
So, continuing with our example (A is 3, F is x 7→ x + 1), we can
also compute recursive expressions like:
(F · (F · (F ·A)))
→ (F · (F · (F · 3)))
→ (F · (F · 4))
→ (F · 5)
→ 6
34/46
Background Math notions Fun Programming Lambda Calculus Review
Application
Note that F and A can be arbitrary expressions.
So, continuing with our example (A is 3, F is x 7→ x + 1), we can
also compute recursive expressions like:
(F · (F · (F ·A))) → (F · (F · (F · 3)))
→ (F · (F · 4))
→ (F · 5)
→ 6
34/46
Background Math notions Fun Programming Lambda Calculus Review
Application
Note that F and A can be arbitrary expressions.
So, continuing with our example (A is 3, F is x 7→ x + 1), we can
also compute recursive expressions like:
(F · (F · (F ·A))) → (F · (F · (F · 3)))
→ (F · (F · 4))
→ (F · 5)
→ 6
34/46
Background Math notions Fun Programming Lambda Calculus Review
Application
Note that F and A can be arbitrary expressions.
So, continuing with our example (A is 3, F is x 7→ x + 1), we can
also compute recursive expressions like:
(F · (F · (F ·A))) → (F · (F · (F · 3)))
→ (F · (F · 4))
→ (F · 5)
→ 6
34/46
Background Math notions Fun Programming Lambda Calculus Review
Application
Note that F and A can be arbitrary expressions.
So, continuing with our example (A is 3, F is x 7→ x + 1), we can
also compute recursive expressions like:
(F · (F · (F ·A))) → (F · (F · (F · 3)))
→ (F · (F · 4))
→ (F · 5)
→ 6
34/46
Background Math notions Fun Programming Lambda Calculus Review
Abstraction
The second basic operation of the λ-calculus is abstraction.
λx .M [x ]
denotes the function x 7→ M [x ].
i.e. some expression M , where any instance of the variable x in M
has been replaced with the input.
Examples
▶ λx .x is the function x 7→ x , i.e. f (x ) = x
▶ λx .4 is the function x 7→ 4, i.e. f (x ) = 4
▶ λx .(square · x ) is the function x 7→ (square · x ), i.e.
f (x ) = x 2
35/46
Background Math notions Fun Programming Lambda Calculus Review
Abstraction
The second basic operation of the λ-calculus is abstraction.
λx .M [x ]
denotes the function x 7→ M [x ].
i.e. some expression M , where any instance of the variable x in M
has been replaced with the input.
Examples
▶ λx .x is the function
x 7→ x , i.e. f (x ) = x
▶ λx .4 is the function x 7→ 4, i.e. f (x ) = 4
▶ λx .(square · x ) is the function x 7→ (square · x ), i.e.
f (x ) = x 2
35/46
Background Math notions Fun Programming Lambda Calculus Review
Abstraction
The second basic operation of the λ-calculus is abstraction.
λx .M [x ]
denotes the function x 7→ M [x ].
i.e. some expression M , where any instance of the variable x in M
has been replaced with the input.
Examples
▶ λx .x is the function x 7→ x , i.e. f (x ) = x
▶ λx .4 is the function
x 7→ 4, i.e. f (x ) = 4
▶ λx .(square · x ) is the function x 7→ (square · x ), i.e.
f (x ) = x 2
35/46
Background Math notions Fun Programming Lambda Calculus Review
Abstraction
The second basic operation of the λ-calculus is abstraction.
λx .M [x ]
denotes the function x 7→ M [x ].
i.e. some expression M , where any instance of the variable x in M
has been replaced with the input.
Examples
▶ λx .x is the function x 7→ x , i.e. f (x ) = x
▶ λx .4 is the function x 7→ 4, i.e. f (x ) = 4
▶ λx .(square · x ) is the function
x 7→ (square · x ), i.e.
f (x ) = x 2
35/46
Background Math notions Fun Programming Lambda Calculus Review
Abstraction
The second basic operation of the λ-calculus is abstraction.
λx .M [x ]
denotes the function x 7→ M [x ].
i.e. some expression M , where any instance of the variable x in M
has been replaced with the input.
Examples
▶ λx .x is the function x 7→ x , i.e. f (x ) = x
▶ λx .4 is the function x 7→ 4, i.e. f (x ) = 4
▶ λx .(square · x ) is the function x 7→ (square · x ), i.e.
f (x ) = x 2
35/46
Background Math notions Fun Programming Lambda Calculus Review
Application and abstraction
We can easily combine the rules, for example, suppose we have
▶ f : x 7→ x + 1
▶ g : x 7→ x 2
Then the following expressions reduce like this:
▶ ((λy .(f · y)) · 3) → (f · 3) → 4
▶ ((λy .(g · y)) · 3) → (g · 3) → 9
▶ (λz .((λy .(g · y)) · z ) · 5) → ((λy .(g · y)) · 5) → (g · 5) → 25
36/46
Background Math notions Fun Programming Lambda Calculus Review
Application and abstraction
We can easily combine the rules, for example, suppose we have
▶ f : x 7→ x + 1
▶ g : x 7→ x 2
Then the following expressions reduce like this:
▶ ((λy .(f · y)) · 3) → (f · 3) → 4
▶ ((λy .(g · y)) · 3) → (g · 3) → 9
▶ (λz .((λy .(g · y)) · z ) · 5) → ((λy .(g · y)) · 5) → (g · 5) → 25
36/46
Background Math notions Fun Programming Lambda Calculus Review
Application and abstraction
We can easily combine the rules, for example, suppose we have
▶ f : x 7→ x + 1
▶ g : x 7→ x 2
Then the following expressions reduce like this:
▶ ((λy .(f · y)) · 3) → (f · 3) → 4
▶ ((λy .(g · y)) · 3) → (g · 3) → 9
▶ (λz .((λy .(g · y)) · z ) · 5) → ((λy .(g · y)) · 5) → (g · 5) → 25
36/46
Background Math notions Fun Programming Lambda Calculus Review
Application and abstraction
We can easily combine the rules, for example, suppose we have
▶ f : x 7→ x + 1
▶ g : x 7→ x 2
Then the following expressions reduce like this:
▶ ((λy .(f · y)) · 3) → (f · 3) → 4
▶ ((λy .(g · y)) · 3) → (g · 3) → 9
▶ (λz .((λy .(g · y)) · z ) · 5) →
((λy .(g · y)) · 5) → (g · 5) → 25
36/46
Background Math notions Fun Programming Lambda Calculus Review
Application and abstraction
We can easily combine the rules, for example, suppose we have
▶ f : x 7→ x + 1
▶ g : x 7→ x 2
Then the following expressions reduce like this:
▶ ((λy .(f · y)) · 3) → (f · 3) → 4
▶ ((λy .(g · y)) · 3) → (g · 3) → 9
▶ (λz .((λy .(g · y)) · z ) · 5) → ((λy .(g · y)) · 5) →
(g · 5) → 25
36/46
Background Math notions Fun Programming Lambda Calculus Review
Application and abstraction
We can easily combine the rules, for example, suppose we have
▶ f : x 7→ x + 1
▶ g : x 7→ x 2
Then the following expressions reduce like this:
▶ ((λy .(f · y)) · 3) → (f · 3) → 4
▶ ((λy .(g · y)) · 3) → (g · 3) → 9
▶ (λz .((λy .(g · y)) · z ) · 5) → ((λy .(g · y)) · 5) → (g · 5) → 25
36/46
Background Math notions Fun Programming Lambda Calculus Review
Parentheses, parentheses everywhere…
You might’ve noticed by now that I’ve been writing a lot of
parentheses, for example, do we really need to write:
(F · (F · (F · 3)))
No! We could write this trivial expression unambiguously as FFF3
So far we’ve only considered functions with:
▶ 1 parameter (e.g. “square”, “increment”)
▶ 0 parameters (constants, e.g. 1, 2, 3.).
… It quickly gets more complex as we use abstraction (λ).
Next week we’ll learn about when it is – or isn’t – safe to simplify
the notation.
Until then, we’ll keep writing everything out in full.
37/46
Background Math notions Fun Programming Lambda Calculus Review
Parentheses, parentheses everywhere…
You might’ve noticed by now that I’ve been writing a lot of
parentheses, for example, do we really need to write:
(F · (F · (F · 3)))
No! We could write this trivial expression unambiguously as FFF3
So far we’ve only considered functions with:
▶ 1 parameter (e.g. “square”, “increment”)
▶ 0 parameters (constants, e.g. 1, 2, 3.).
… It quickly gets more complex as we use abstraction (λ).
Next week we’ll learn about when it is – or isn’t – safe to simplify
the notation.
Until then, we’ll keep writing everything out in full.
37/46
Background Math notions Fun Programming Lambda Calculus Review
Parentheses, parentheses everywhere…
You might’ve noticed by now that I’ve been writing a lot of
parentheses, for example, do we really need to write:
(F · (F · (F · 3)))
No! We could write this trivial expression unambiguously as FFF3
So far we’ve only considered functions with:
▶ 1 parameter (e.g. “square”, “increment”)
▶ 0 parameters (constants, e.g. 1, 2, 3.).
… It quickly gets more complex as we use abstraction (λ).
Next week we’ll learn about when it is – or isn’t – safe to simplify
the notation.
Until then, we’ll keep writing everything out in full.
37/46
Background Math notions Fun Programming Lambda Calculus Review
Free and bound variables
λx .(y · x )
▶ x is a bound variable, because the λ binds it.
▶ y is a free variable, because it is not bound by any λ.
38/46
Background Math notions Fun Programming Lambda Calculus Review
Free and bound variables
x · (λx .(y · x ))
▶ The first occurrence of x is a free variable.
▶ The second occurrence of x is a bound variable.
▶ y is a free variable.
39/46
Background Math notions Fun Programming Lambda Calculus Review
Free and bound variables
(λx .(y · x )) · x
▶ The first occurrence of x is a bound variable.
▶ The second occurrence of x is a free variable, because it is
not in the scope of the λx
▶ y is a free variable.
40/46
Background Math notions Fun Programming Lambda Calculus Review
Free and bound variables
(λx .(x · (λx .(x · x )))
▶ The first occurrence of x is bound to the first λ.
▶ The second occurrence of x is bound to the second λ.
▶ The third occurrence of x is also bound to the second λ.
41/46
Background Math notions Fun Programming Lambda Calculus Review
β-reduction (abstraction)
We can now define the abstraction operation more formally. It is
the axiom:
(λx .M ) ·N = M [x := N ]
This means the output of (λx .M ) ·N is the result of replacing
every free occurrence of x in M with N .
Important: Only the free occurrences! Example:
(yx (λx .x ))[x := N ] = yN (λx .x )
42/46
Background Math notions Fun Programming Lambda Calculus Review
β-reduction (abstraction)
We can now define the abstraction operation more formally. It is
the axiom:
(λx .M ) ·N = M [x := N ]
This means the output of (λx .M ) ·N is the result of replacing
every free occurrence of x in M with N .
Important: Only the free occurrences! Example:
(yx (λx .x ))[x := N ] = yN (λx .x )
42/46
Background Math notions Fun Programming Lambda Calculus Review
Renaming bound variables
▶ (λx .x ) · x is confusing because the first occurrence of x is
bound, but the second is free.
▶ Bound variables have a similar scope to variable scope in
imperative programming languages
▶ e.g. in Java
i n t x = 1 ;
{ i n t x = 2 ; System . out . p r i n t l n ( x ) ; }
System . out . p r i n t l n ( x ) ;
would output 2, 1.
▶ We can apply the same notion of scope to rename the
occurences of a variable bound by a particular λ.
▶ Example: (λx .x ) · x = (λy .y) · x
43/46
Background Math notions Fun Programming Lambda Calculus Review
Renaming bound variables
▶ (λx .x ) · x is confusing because the first occurrence of x is
bound, but the second is free.
▶ Bound variables have a similar scope to variable scope in
imperative programming languages
▶ e.g. in Java
i n t x = 1 ;
{ i n t x = 2 ; System . out . p r i n t l n ( x ) ; }
System . out . p r i n t l n ( x ) ;
would output 2, 1.
▶ We can apply the same notion of scope to rename the
occurences of a variable bound by a particular λ.
▶ Example: (λx .x ) · x = (λy .y) · x
43/46
Background Math notions Fun Programming Lambda Calculus Review
Don’t relabel any occurences that weren’t bound to that λ:
▶ Mistake: ((λx .(y · x )) · x ) ̸= ((λz .(y · z )) · z )
▶ Correct: ((λx .(y · x )) · x ) = ((λz .(y · z )) · x )
Don’t skip any of the occurrences bound to that λ:
▶ Mistake: (λx .(x · x )) ̸= (λy .(y · x ))
▶ Correct: (λx .(x · x )) = (λy .(y · y))
Don’t change the binding of the other variables (use a new label)
▶ Mistake: (λx .(x · y)) ̸= (λy .(y · y))
▶ Correct: (λx .(x · y)) = (λz .(z · y))
44/46
Background Math notions Fun Programming Lambda Calculus Review
Don’t relabel any occurences that weren’t bound to that λ:
▶ Mistake: ((λx .(y · x )) · x ) ̸= ((λz .(y · z )) · z )
▶ Correct: ((λx .(y · x )) · x ) = ((λz .(y · z )) · x )
Don’t skip any of the occurrences bound to that λ:
▶ Mistake: (λx .(x · x )) ̸= (λy .(y · x ))
▶ Correct: (λx .(x · x )) = (λy .(y · y))
Don’t change the binding of the other variables (use a new label)
▶ Mistake: (λx .(x · y)) ̸= (λy .(y · y))
▶ Correct: (λx .(x · y)) = (λz .(z · y))
44/46
Background Math notions Fun Programming Lambda Calculus Review
Don’t relabel any occurences that weren’t bound to that λ:
▶ Mistake: ((λx .(y · x )) · x ) ̸= ((λz .(y · z )) · z )
▶ Correct: ((λx .(y · x )) · x ) = ((λz .(y · z )) · x )
Don’t skip any of the occurrences bound to that λ:
▶ Mistake: (λx .(x · x )) ̸= (λy .(y · x ))
▶ Correct: (λx .(x · x )) = (λy .(y · y))
Don’t change the binding of the other variables (use a new label)
▶ Mistake: (λx .(x · y)) ̸= (λy .(y · y))
▶ Correct: (λx .(x · y)) = (λz .(z · y))
44/46
Background Math notions Fun Programming Lambda Calculus Review
Make sure you know which variables are bound to which λ!
(λx .(x · (λx .x )) · x ) · x
▶ the first occurrence of x is
bound to the first λ
▶ the second occurrence of x is bound to the second λ
▶ the third occurrence of x is bound to the first λ
▶ the fourth occurrence of x is a free variable
▶ … so confusing!
Rename the first λ with y :
(λy .(y · (λx .x ) · y) · x
Rename the second λ with z :
(λy .(y · (λz .z )) · y) · x
45/46
Background Math notions Fun Programming Lambda Calculus Review
Make sure you know which variables are bound to which λ!
(λx .(x · (λx .x )) · x ) · x
▶ the first occurrence of x is bound to the first λ
▶ the second occurrence of x is
bound to the second λ
▶ the third occurrence of x is bound to the first λ
▶ the fourth occurrence of x is a free variable
▶ … so confusing!
Rename the first λ with y :
(λy .(y · (λx .x ) · y) · x
Rename the second λ with z :
(λy .(y · (λz .z )) · y) · x
45/46
Background Math notions Fun Programming Lambda Calculus Review
Make sure you know which variables are bound to which λ!
(λx .(x · (λx .x )) · x ) · x
▶ the first occurrence of x is bound to the first λ
▶ the second occurrence of x is bound to the second λ
▶ the third occurrence of x is
bound to the first λ
▶ the fourth occurrence of x is a free variable
▶ … so confusing!
Rename the first λ with y :
(λy .(y · (λx .x ) · y) · x
Rename the second λ with z :
(λy .(y · (λz .z )) · y) · x
45/46
Background Math notions Fun Programming Lambda Calculus Review
Make sure you know which variables are bound to which λ!
(λx .(x · (λx .x )) · x ) · x
▶ the first occurrence of x is bound to the first λ
▶ the second occurrence of x is bound to the second λ
▶ the third occurrence of x is bound to the first λ
▶ the fourth occurrence of x is
a free variable
▶ … so confusing!
Rename the first λ with y :
(λy .(y · (λx .x ) · y) · x
Rename the second λ with z :
(λy .(y · (λz .z )) · y) · x
45/46
Background Math notions Fun Programming Lambda Calculus Review
Make sure you know which variables are bound to which λ!
(λx .(x · (λx .x )) · x ) · x
▶ the first occurrence of x is bound to the first λ
▶ the second occurrence of x is bound to the second λ
▶ the third occurrence of x is bound to the first λ
▶ the fourth occurrence of x is a free variable
▶ … so confusing!
Rename the first λ with y :
(λy .(y · (λx .x ) · y) · x
Rename the second λ with z :
(λy .(y · (λz .z )) · y) · x
45/46
Background Math notions Fun Programming Lambda Calculus Review
Make sure you know which variables are bound to which λ!
(λx .(x · (λx .x )) · x ) · x
▶ the first occurrence of x is bound to the first λ
▶ the second occurrence of x is bound to the second λ
▶ the third occurrence of x is bound to the first λ
▶ the fourth occurrence of x is a free variable
▶ … so confusing!
Rename the first λ with y :
(λy .(y · (λx .x ) · y) · x
Rename the second λ with z :
(λy .(y · (λz .z )) · y) · x
45/46
Background Math notions Fun Programming Lambda Calculus Review
Make sure you know which variables are bound to which λ!
(λx .(x · (λx .x )) · x ) · x
▶ the first occurrence of x is bound to the first λ
▶ the second occurrence of x is bound to the second λ
▶ the third occurrence of x is bound to the first λ
▶ the fourth occurrence of x is a free variable
▶ … so confusing!
Rename the first λ with y :
(λy .(y · (λx .x ) · y) · x
Rename the second λ with z :
(λy .(y · (λz .z )) · y) · x
45/46
Background Math notions Fun Programming Lambda Calculus Review
Review
▶ Motivation for studying theory
▶ Mathematical notions and notation
▶ Introduction to functional programming
▶ Functions
▶ Expressions
▶ Rewrite rules
▶ Introduction to the lambda calculus
▶ Function application
▶ Abstraction (β-reduction)
▶ Free and bound variables
▶ Renaming
46/46
Background
outline
why
history
Math notions
outline
Subsection 1
Fun Programming
outline
functional programming
Lambda Calculus
outline
lambda calculus
Review
review