Lambda Calculus ( Calculus)
Lambda Calculus (λ Calculus)
March 10, 2021
Outline
I what is lambda calculas
I beta reducton and alpha renaming
I lazy evaluation
I Church encoding
Overview
I The smallest programming language
I Syntax and examples
I α−renaming and β−reduction
I order of evaluation
I λ encoding
I Books: The Lambda Calculus. Its Syntax and Semantics, An
Introduction to Functional Programming Through Lambda Calculus
Smallest Universal Programming Language
I e ::= x |λx .e|e0 e1
I As a programming language, sometimes a concrete implementation
of lambda calculus also supports predefined constants such as ’0’ ’1’
and predefined functions such as ’+’ ’*’
Examples
I λx .x (lambda abstraction: building new function)
I (λx .x) y (function application)
The parenthesis is to separate function and function application.
What is λ Calculus and Why is it important?
1. A mathematical language; A formal computation model for
functional programming; a theoretical foundation for the family of
functional programming languages.
2. Study interactions between functional abstraction and function
applications
3. By in the 1930s
4. In 1920s – 1930s, the mathematicians came up different systems for
capturing the general idea of computation:
I Turing machines – Turing
I m-recursive functions – Gödel
I rewrite systems – Post
I the lambda calculus – Church
I combinatory logic – Schönfinkel, systems are all computationally equivalent in the sense that
each could encode and simulate the others.
The Mathematical Precursor to Scheme
Mathematical formalism to express computation using functions:
I Everything is a function. There are no other primitive types—no
integers, strings, objects, booleans … If you want these things, you
must encode (simulate) them using functions.
I No state or side effects. It is purely functional. Thus we can think
exclusively in terms of the substitution model.
I Only unary (one-argument) functions.
Implementation in Scheme/DrRacket
I Syntax implemented in Scheme:
Lambda Calculus: Review
I Smallest language
I Syntax
S → Name | Function | Application
x | λx .x λx .x y
(λx .x) y
(λx .x y)
(λ(x) y)
(Lambda(x) y)
(xλ(x) y)x
( ) helps with clarity
(x )x helps with clarity
I Turing machine is the model for imperative programming language,
and, λ calculus is the model for functional programming language.
They have equal computing power and can simulate each other.
Lambda Calculus Semantics
I β-reduction
(λx .x) x
Function definition Actual parameter
The bound variable x will be replaced by the argument expression in
the body expression x .
β-reduction
The AST view:
β-reduction
((λ(x) e1 ) e2) evaluates the expression e1 by replacing every (“free”)
occurrences of x in e1 using e2, denoted as e1[x→e2]
I ( (λ(x) (λ(y) (+ x y) ) ) 1)
I ( ( ( (λ (x) (λ(y) (λ (x) (+ x y) ) ) ) 1) 2) 3)
β-reduction (Contd.)
((λ(x) e1 ) e2) evaluates the expression e1 by replacing every (“free”)
occurrences of x in e1 using e2, denoted as e1[x→e2]
I ( (λ(x) (λ(y) (+ x y) ) ) 1)
output: (λ(y) (+ 1 y) )
β-reduction
((λ(x) e1 ) e2) evaluates the expression e1 by replacing every (“free”)
occurrences of x in e1 using e2, denoted as e1[x→e2]
I ( (λ(x) (λ(y) (+ x y) ) ) 1)
I ( ( ( (λ (x) (λ(y) (λ (x) (+ x y) ) ) ) 1) 2) 3)
= ( ( (λ(y) (λ (x) (+ x y) ) ) 2) 3)
= ( (λ (x) (+ x 2) ) 3)
= 5
α-renaming
Rename a variable:
I ( ( ( (λ(x) (λ(y) (λ(x) (+ x y) ) ) ) 1) 2) 3)
I ( ( ( (λ(x) (λ(y) (λ(z) (+ z y) ) ) ) 1) 2) 3)
The Order of Evaluation
The order of evaluation does not impact β-reduction results if the
evaluation terminates:
( (λ(x) (+ x 1)) ((λ(y) (+ y 1)) 2 ) )
Lazy Evaluation
I The evaluation is deferred until their results are needed.
I Arguments are not evaluated before they are passed to a function,
but only when their values are actually used.
( (λ(x) (+ x 1)) ((λ(y) (+ y 1)) 2 ) )
( (λ(x) 1) ((λ(y) (+ y 1)) 2 ) )
Simulating the Computation
What is the result of ((λ(x)x) (λ(y)y))
Soln: (λ(y)y)
Identity Function
(λ(x)x): this function applies to any entity return the entity itself
f(x) = x+0 or f(x) = x*1 or f(x) = x-0
Self-Application Function
(λ(x)(x x)): this function applies to any entity will return the entity
aplies to itself
((λ(x)(x x)) 3)
Soln: (3 3)
((λ(x)(x x)) (λ(y) y))
Soln: ((λ(y) y) (λ(y) y))
(λ(y) y)
More Examples
(λ(f) (λ(x) (f x) ))
I (f x) means application of function f on x.
I It is a function without formal parameter, cannot be reduced any
further through β-reduction.
( ((λ(f) (λ(x) (f x) )) (λ(y) y )) (λ(z) (z z) ))
F A1 A2
Let (λ(y) y ) = g and (λ(z) (z z) ) = v
((λ(x) (g x) ) v)
= (g v)
= ((λ(y) y ) v)
= v
= (λ(z) (z z) )
Church encoding
I In mathematics, Church encoding is a means of representing data
and operators in the lambda calculus
I The Church numerals are a representation of the natural numbers
using lambda notation.
I The method is named for , who first encoded data in
the lambda calculus this way.
Church encoding
Representing data and operations using functions:
I non-negative integers: 0, 1, 2 …, and their computation of addition,
subtraction, multiplication …
I boolean, true, false, and, or, not, ite (if then else control flow)
I pairs and lists
I rational numbers: may be encoded as a pair of signed numbers
I computable real numbers may be encoded by a limiting process that
guaranetees that the difference from the real value differs by a
number which maybe as small as we need (considering pi)
I complex numbers are naturally encoded as a pair of real numbers.
Encoding Natural Numbers (Church Numbers)
I Encoding of numbers: 0, 1, 2, . . . , as functions such that their
semantics follow the natural number semantics (e.g., counting,
sequencing)
I Intuition: The number n means how many times one can do certain
operation.
I A natural number encoding function takes two arguments (function
and entity on which the function is to be applied)
More examples of understanding the functions of natural
numbers
(two g) =
( (f λ(f ) (x λ(x)(f (f x))x)f g) =
(x λ(x)(g (g x))x)
This is a function that takes a parameter x and returns the result of
applying the function g twice on x.
( (z λ(z) ((three f ) z) )z two)
Soln:
(f ( f ( f two)))
Operations on natural numbers
the Successor functinon
Exercise
(succ (succ zero))
Encoding Add using the Successor functinon
Semantics of Addition: Addition takes two natural numbers as arguments
and produces a new natural number whose semantics/representation is
the sum of two inputs.
I Add requires two arguments and returns a natural number
representation:
(m λ(m)(n λ(n)(f λ(f )(x λ(x) … )x)f )n)m
The definition is follows:
I ( (m succ) n) generates:
(succ (succ (succ . . . (succ n)) . . . ))
This produces a natural number equivalent to m+n
I It should be applied to some function f to represent the natural
number
((( (m succ) n) f) x)
I Therefore, the add function is:
(m λ(m)(n λ(n)(f λ(f )(x λ(x) ((((m succ) n) f ) x) )x)f )n)m
Exericse
((add (succ zero)) (succ zero))
Natural Numbers Encoding in λ-calculus (Revisit)
Representation of:
Each number is represented by the number of times some function is
applied to some entity.
Natural Numbers Encoding in λ-calculus (Revisit)
I Develop a successor function succ that takes a natural number as an
argument and returns the next natural number.
I Example:
(succ zero) should return (f λ(f )(x λ(x) (f x)x)f = one
(succ one) should return (f λ(f )(x λ(x) (f (f x))x)f = two
Natural Numbers Encoding in λ-calculus (Revisit)
Boolean and if-then-else (ITE)
or a b:
( (ite a) true
((ite b) true false)
)
Boolean Operations
I Basic operators: and, or, not
I which then can be extended to xor, implication and equievelnce
More about Lambda Caculus
I there is no recursion in lambda calculus
I do we program in lambda calculus? mostly no
I it helps understand functional computation
I it helps design new functional programming languages
Problem Solving
I beta reduction:
I parsing the function
I understand what is the function, what is the actual parameters
I remember steps of function applications, even when functions and
actual parameters can be complex
I beta reduction and encoding recognition (e.g., what does this
function compute?):
I remember existing encoding and functions
I understand the semantics of certain functions and patterns, e.g.,
identity function, natural numbers …
Further Learning Materials
I Lambda calculus examples:
https://www.ics.uci.edu/~lopes/teaching/inf212W12/
readings/lambda-calculus-handout.pdf
I Programming Languages: Lambda Calculus – 1
I Programming Languages: Lambda Calculus – 2
https://www.ics.uci.edu/~lopes/teaching/inf212W12/readings/lambda-calculus-handout.pdf
https://www.ics.uci.edu/~lopes/teaching/inf212W12/readings/lambda-calculus-handout.pdf