Lambda Calculus (λ Calculus)
March 10, 2021
Outline
what is lambda calculas
beta reducton and alpha renaming lazy evaluation
Church encoding
Overview
The smallest programming language
Syntax and examples
α−renaming and β−reduction
order of evaluation
λ encoding
Books: The Lambda Calculus. Its Syntax and Semantics, An Introduction to Functional Programming Through Lambda Calculus
Smallest Universal Programming Language
e ::= x|λx.e|e0 e1
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
λx.x (lambda abstraction: building new function) (λ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 Alonzo Church in the 1930s
4. In 1920s – 1930s, the mathematicians came up different systems for capturing the general idea of computation:
Turing machines – Turing
m-recursive functions – G ̈odel
rewrite systems – Post
the lambda calculus – Church
combinatory logic – Scho ̈nfinkel, Curry
These 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:
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.
No state or side effects. It is purely functional. Thus we can think exclusively in terms of the substitution model.
Only unary (one-argument) functions.
Implementation in Scheme/DrRacket
Syntax implemented in Scheme:
Lambda Calculus: Review
Smallest language
Syntax
S → Name
|
Function | λx.x
| Application λx.xy (λx.x) y (λx.x y) (λ(x) y) (Lambda(x) y) (xλ(x)y)x
(
(x
) helps with clarity )x helps with clarity
x
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
β-reduction
Function definition Actual parameter
The bound variable x will be replaced by the argument expression in the body expression x.
(λx.x) 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]
((λ(x)(λ(y)(+xy)))1)
((((λ(x)(λ(y)(λ(x)(+xy))))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]
((λ(x)(λ(y)(+xy)))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]
((λ(x)(λ(y)(+xy)))1)
((((λ(x)(λ(y)(λ(x)(+xy))))1)2)3) = ( ( (λ(y) (λ (x) (+ x y) ) ) 2) 3)
= ( (λ (x) (+ x 2) ) 3)
=5
α-renaming
Rename a variable:
((((λ(x)(λ(y)(λ(x)(+xy))))1)2)3) ((((λ(x)(λ(y)(λ(z)(+zy))))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
The evaluation is deferred until their results are needed.
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) ))
(f x) means application of function f on x.
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
In mathematics, Church encoding is a means of representing data and operators in the lambda calculus
The Church numerals are a representation of the natural numbers using lambda notation.
The method is named for Alonzo Church, who first encoded data in the lambda calculus this way.
Church encoding
Representing data and operations using functions:
non-negative integers: 0, 1, 2 …, and their computation of addition, subtraction, multiplication …
boolean, true, false, and, or, not, ite (if then else control flow)
pairs and lists
rational numbers: may be encoded as a pair of signed numbers
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)
complex numbers are naturally encoded as a pair of real numbers.
Encoding Natural Numbers (Church Numbers)
Encoding of numbers: 0, 1, 2, . . . , as functions such that their semantics follow the natural number semantics (e.g., counting, sequencing)
Intuition: The number n means how many times one can do certain operation.
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)((threef)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.
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:
( (m succ) n) generates:
(succ (succ (succ …(succ n)) …))
This produces a natural number equivalent to m+n
It should be applied to some function f to represent the natural number
((( (m succ) n) f) x)
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)
Develop a successor function succ that takes a natural number as an argument and returns the next natural number.
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
Basic operators: and, or, not
which then can be extended to xor, implication and equievelnce
More about Lambda Caculus
there is no recursion in lambda calculus
do we program in lambda calculus? mostly no
it helps understand functional computation
it helps design new functional programming languages
Problem Solving
beta reduction:
parsing the function
understand what is the function, what is the actual parameters
remember steps of function applications, even when functions and
actual parameters can be complex
beta reduction and encoding recognition (e.g., what does this function compute?):
remember existing encoding and functions
understand the semantics of certain functions and patterns, e.g.,
identity function, natural numbers …
Further Learning Materials
Lambda calculus examples: https://www.ics.uci.edu/~lopes/teaching/inf212W12/ readings/lambda-calculus-handout.pdf
Programming Languages: Lambda Calculus – 1 https://www.youtube.com/watch?v=v1IlyzxP6Sg
Programming Languages: Lambda Calculus – 2 https://www.youtube.com/watch?v=Mg1pxUKeWCk