Transcript PowerPoint - School of Computing Science

Types and Programming Languages
Lecture 6
Simon Gay
Department of Computing Science
University of Glasgow
2006/07
Lambda Calculus
Lambda calculus is a notation for functions, and can be viewed
as a core functional programming language, either untyped
(initially) or typed (later).
Syntax
Terms e are defined by this grammar, assuming a supply of
variables x, y, z, … :
e ::= x
| x.e
|ee
(variable)
(abstraction)
(application)
Convention:  has the lowest priority.
2006/07
Types and Programming Languages Lecture 6 - Simon Gay
2
Lambda Calculus
Examples
x.x
is a function which returns its parameter
x.y.xy
is a function which, given a parameter x, returns a
function which, given a parameter y, returns the
result of applying x to y.
To obtain more concrete examples, we can combine -notation
with the syntax of SEL:
x.x+1
x.y.x+y
x.y.if x==1 then y else y+1
2006/07
Types and Programming Languages Lecture 6 - Simon Gay
3
Scope and Variable Binding
x declares a new variable x with its own scope. Occurrences of
x within this scope are said to be bound. Variables which are not
bound are said to be free.
x.y+x
free
bound
The name of a bound variable is not important as long as it is the
same as the variable attached to the corresponding .
x.y+x is equivalent to z.y+z
Bound variables can be renamed as long as free variables are
not captured.
x.y+x is different from y.y+y
2006/07
Types and Programming Languages Lecture 6 - Simon Gay
4
Scope and Variable Binding
Renaming bound variables is called alpha-conversion and terms
which differ only in the names of bound variables are said to be
alpha-equivalent.
It is often convenient to assume that a term has been
alpha-converted so that the names of all bound variables are
different from each other and different from the names of all
free variables.
Variables are bound by the structurally nearest matching .
x.(y.x.xy)x
2006/07
is alpha-equivalent to
x.(y.z.zy)x
Types and Programming Languages Lecture 6 - Simon Gay
5
Variable Binding
Variable binding is a fundamental concept which occurs in many
places:
10
0 x
2
dx
n 2
i
i1
and of course in any programming language:
int f(int x) {
return x+1;
}
2006/07
{ int x = 1;
{ int y;
y = x + 1;
}
}
Types and Programming Languages Lecture 6 - Simon Gay
6
Substitution
To define the operational semantics of the lambda calculus we
need to define substitution, in a similar way to SFL.
x[e x]  e
x[e z]  x
if x and z are different variables
(e1e2 )[e3 x]  (e1[e3 x])(e2[e3 x])
(y.e1)[e x]  y.(e1[e x]) if y is not free in e
In general it may be necessary to rename bound variables to
avoid variable capture during substitution:
(y.x  y)[y x]  ? y.y  y
WRONG!
(z.x  z)[y x]  z.y  z
CORRECT
2006/07
Types and Programming Languages Lecture 6 - Simon Gay
7
Lambda Calculus: Operational Semantics
The reduction rule for function application:
(x.e)e'  e[e' x]
is similar to the rule in SFL. It is known as beta-reduction.
Example
(x.x+1)2  (x+1)[2/x] = 2+1  3
if we include the syntax and reduction rules of SEL.
(x.y.x+y)2  (y.x+y)[2/x] = y.2+y
an example of a function which returns a function.
2006/07
Types and Programming Languages Lecture 6 - Simon Gay
8
Lambda Calculus: Reduction Strategies
Different reduction strategies are based on where in a term it is
possible to apply beta reduction.
We will concentrate on call by value reduction, which means
adding the following rules:
e  e'
e1  e'1
ve  ve'
e1e2  e'1 e2
Values v are -abstractions, and any other values which we
might incorporate from SEL.
Other reduction strategies are possible (e.g. call by name), but
this has little effect on typing (which is what we are interested in).
2006/07
Types and Programming Languages Lecture 6 - Simon Gay
9
Lambda Calculus: what I’m not telling you
Lambda calculus is powerful enough to be a general-purpose
programming language: any computation can be expressed.
Data can be encoded as functions, for example:
true
x.y.x
false
x.y.y
if c then t else e
(c t) e
Non-terminating computation is possible, for example:
(x.xx)(x.xx)  (x.xx)(x.xx)
and recursive functions can be encoded.
2006/07
Types and Programming Languages Lecture 6 - Simon Gay
10
Lambda Calculus + Expressions
As a step towards a better functional language (BFL) we can
combine -calculus and SEL.
Syntax
v ::= integer literal
| true | false
| x.e
e ::= v
|x
| e + e | e == e | e & e | if e then e else e
| ee
“x” stands for any variable
2006/07
Types and Programming Languages Lecture 6 - Simon Gay
11
Lambda Calculus + Expressions
Reductions
The rules for SEL, and the following extra rules:
(x.e)v  e[v x]
(R-AppAbs)
e1  e'1
(R-AppL)
e1e2  e'1 e2
note: applied to a value
e  e'
(R-AppR)
ve  ve'
Remember that a -abstraction is a value.
2006/07
Types and Programming Languages Lecture 6 - Simon Gay
12
Do we have a Better Functional Language?
We have functions, e.g. x.x+2 is a function, but can we really
do functional programming?
It’s essential to be able to define recursive functions, but our
language has no direct support for recursive definitions. We have
no way of associating a name with a function.
It is possible to express nameless recursive functions in
-calculus, and it’s interesting to see how this works.
2006/07
Types and Programming Languages Lecture 6 - Simon Gay
13
Recursion in -calculus
Fixed points
If f is a function then a fixed point of f is a value v such that fv = v.
Fixed point combinators
It is possible to find a -term Y with the curious property that
for any term f, Yf is a fixed point of f. In other words, f(Yf) = Yf.
For example, define
Y = y.(x.y(xx))(x.y(xx))
Yf = (y.(x.y(xx))(x.y(xx)))f  (x.f(xx))(x.f(xx))
 f((x.f(xx))(x.f(xx))) = f(Yf)
(we haven’t said what ‘=’ means, but it should include reduction)
2006/07
Types and Programming Languages Lecture 6 - Simon Gay
14
Recursion in -calculus
Recursive definitions and fixed points
Here is a recursive function which we would like to define, but
can’t because we have no mechanism for naming functions:
f = x.if x==0 then 1 else x*f(x-1)
(1)
If we abstract on f we get the following, which we call F just for
convenience:
F = f.x.if x==0 then 1 else x*f(x-1)
Now imagine that g is a fixed point of F:
g = Fg  x.if x==0 then 1 else x*g(x-1))
which strongly suggests that the meaning of the recursive
definition (1) is given by a fixed point of F.
2006/07
Types and Programming Languages Lecture 6 - Simon Gay
15
Recursion in -calculus
Conclusion
Given a recursive function definition such as
f = x.if x==0 then 1 else x*f(x-1)
we can construct the corresponding functional:
F = f.x.if x==0 then 1 else x*f(x-1)
whose fixed point is the function we want. This fixed point can be
expressed as YF and written as a -term without naming.
Example
YF = (y.(x.y(xx))(x.y(xx)))(f.x.if x==0 then 1 else x*f(x-1))
(YF)3 * 6
2006/07
Types and Programming Languages Lecture 6 - Simon Gay
16
Reading
Pierce: 5
Exercises
Pierce: 5.2.1, 5.3.3, 5.3.7, 5.3.8
2006/07
Types and Programming Languages Lecture 6 - Simon Gay
17