Transcript Lambda Calculus

CS321 Functional Programming 2
The λ Calculus
This is a formal system to capture the ideas of function
abstraction and application introduced by Alzonzo Church
and Haskell B Curry in the 1930s.
A λ-term is defined as:a variable
x
conventionally a lower case letter
an abstraction
λx.(M)
an upper case letter conventionally represents any λ-term
an application
M N
a bracketed term (M)
Haskell has λ-terms – \x->M
Note that application groups to the left – MNK means (MN)K
© JAS 2005
4-1
CS321 Functional Programming 2
Function application is straightforward.
(λx.(f x)) y => f y substitute y for x in (f x)
(λx.(f x)) y == [y/x](f x)
(λx z.(z x)) y => (λx.(λz.(z x))) y
=> (λz.(z y))
(λx y.(y x)) y => (λx.(λy.(y x))) y
=> (λy.(y y ))
but the two y’s are different!
y is said to be a bound variable (an argument)
y is said to be a free variable (not bound)
© JAS 2005
4-2
CS321 Functional Programming 2
We need to define the difference between free and bound
variables.
1.
The variable x occurs free in the expression x.
No variable is bound in an expression consisting of a single
variable.
2.
The variable x occurs free (or bound) in YZ if and only if it
occurs free (or bound) in Y or Z.
3.
If a variable x does not occur in V then it occurs free (or
bound) in λV.Y iff it occurs free (or bound) in Y. All
occurrences of the elements of V are bound in λV.Y.
4.
The variable x occurs free (or bound) in (Y) iff it occurs
free (or bound) in Y.
© JAS 2005
4-3
CS321 Functional Programming 2
We can now define our substitution rules for [M/x]Y
Rule 1 – single variables
a) when Y is the variable x then
[M/x]Y => M
b) when Y is a variable other than x then
[M/x]Y => Y
Rule 2 – function applications
when Y is the application W Z then
[M/x]Y => ([M/x]W)([M/x]Z)
© JAS 2005
4-4
CS321 Functional Programming 2
Rule 3 – function abstraction
We will assume all bound variables are preceded by a λ
a) when Y is the abstraction λx.W then [M/x]Y => λx.W
b) when Y is the abstraction λy.W and there are no free
occurrences of x in W then [M/x]Y is λy.W
c) when Y is the abstraction λy.W and there are no free
occurrence of y in M then [M/x]Y is λy.[M/x]W
d) when Y is the abstraction λy.W and there is a free occurrence
of y in M then
[M/x]Y is λz.[M.x]([z/y]W)
where z is a variable name that does not occur free in M or Y.
Therefore the binding of abstraction takes precedence and
protects a function body from the effects of substitution if
there is a name clash.
© JAS 2005
4-5
CS321 Functional Programming 2
Simplifying λ-terms
There are 3 rules called conversion rules:α : if there are no free occurrences of y in Z then
λx.Z cnvα λy.[y/x]Z
β : (λx.M) N cnvβ [N/x] M
η: if there are no free occurrences of x in M then
(λx.M x) cnvη M
β and η usually simplify (reduce the complexity of)
expressions and are therefore called reduction rules.
© JAS 2005
4-6
CS321 Functional Programming 2
An expression that can be reduced is called a redex.
(λx.M) N is a β-redex.
(λx.M x) is an η-redex.
An expression containing no redexes is said to be in Normal Form
© JAS 2005
4-7
CS321 Functional Programming 2
The First Church-Rosser Theorem
If X cnv Y then there exists an expression Z such that
X red Z and Y red Z.
Corollary
If an expression reduces to two normal forms then they must
be inter-convertible using α-conversions.
© JAS 2005
4-8
CS321 Functional Programming 2
If A and B are two redexes in an expression M and the first
occurrence of λ in A is to the left of the first occurrence of
λ in B then A is said to be to the left of B.
If A is a redex in M and it is to the left of all other redexes in M
then A is called the leftmost redex of M.
The Second Church-Rosser Theorem
If X red Y and Y is in normal form then there is a reduction
sequence from X to Y that involves successively reducing
the leftmost redex.
This is known as Normal Order Reduction
© JAS 2005
4-9
CS321 Functional Programming 2
Extending the λ-Calculus
We will now add some simple extensions to the λ-calculus.
(We could actually define these extensions with our existing calculus).
• numerical and logical constants
• basic arithmetic and logical operations
• a conditional expression construct
plus = λx y. x + y
max = λab. if a > b then a else b
fib = λn.if n < 3 then 1 else fib(n-1)+fib(n-2)
© JAS 2005
4-10
CS321 Functional Programming 2
By simple referential transparency we should be able to substitute
the λ -expression for fib, but if we do this we get an infinite
expansion.
To avoid this problem we need to define the concept of a Fixed
Point of a function.
The fixed points of a function are the set of values for which the
function performs an identity transformation.
fixed points of f = {X| forall xєX ,f(x) = x}
F = λgn.if n<3 then 1 else g(n-1)+g(n-2)
fib is a fixed point of F
© JAS 2005
4-11
CS321 Functional Programming 2
Hypothesise existence of function Y that produces fixed point for
arbitrary function f.
f = Y F
Every function (in a functional programming language) has at least
one fixed point
This gives us a fixed point X of F as
X = ( λx.F(xx)) ( λx.F(xx))
X cnvβ F(( λx.F(xx))( λx.F(xx))) => F(X)
This gives us Y = λh.(( λx.h(xx))( λx.h(xx)))
© JAS 2005
4-12
CS321 Functional Programming 2
Theorem – Böhm
Given the expression G = λyf.f(yf), then M is a fixed
point operator iff M = GM.
Hence we can confirm that Y is a fixed point operator
Y = λh.((λx.h(xx))(λx.h(xx)))
cnvβ λh.h((λx.h(xx))(λx.h(xx)))
cnvβ λh.h((λf.λx.f(xx))(λx.f(xx)))h)
= λh.h(Yh)
= GY
© JAS 2005
4-13