Lambda Calculus
Purpose
To give you practice with the lambda calculus:
- Syntax
- Rules of inference
Due dates
You must submit your answers to the questions via electronic mail
by 9:00am on
Tuesday, October 4.
Your submission must be an attachment, and must contain your name(s) and
the assignment subject.
The attachment must be a PDF file, whose name is of the form
``First.Last.pdf'' (e.g. ``John.Doe.pdf'').
This assignment is worth 30 points.
Background
According to the Oxford English Dictionary a calculus is ``a
system or method of calculation, `a certain way of performing mathematical
investigations and resolutions' (Hutton)''.
The Lambda Calculus is a method for investigating and resolving identifier
bindings.
It is formal because (again according to the OED) it is
``concerned with the form, as distinguished from the matter, of
reasoning''. It is ``free from the descriptive content that would restrict
it to any particular subject-matter''.
In its simplest form, the Lambda Calculus is untyped.
Identifiers are simply bound by lambda expressions, and no type is
associated with the identifier.
The form of the expressions in the untyped Lambda Calculus
can be found in any elementary programming languages text.
Extending the untyped Lambda Calculus by associating a type with each
constant and binding results in the formalism described in the
text.
Questions
- (4 points)
Consider the definition of the syntax of pre-expressions on page 124 of the
text.
Assume that all of the constants mentioned in the first paragraph are
included.
Write each of the following C fragments as a Lambda expression
(do not use infix operators; use the corresponding operations):
- 1 + 2 * 3
- 1 + 2 + 3
- { int a = 1; int b = 2; c = b + a; }
- { int a = 1; int b = a * 2; c = b + a; }
- (6 points)
Simplify each of the following expressions in the untyped Lambda Calculus
as much as possible:
- ((((λf.(λg.(λx.((f g)(g x)))))
(λm.(λn.(n m))))(λn.z))p)
- ((λx.(x x))(λx.(x x)))
- (5 points)
Rewrite the formal definition of the collection of pre-expressions given on
page 124 of the text using the notation
defined in Section 1.1 of the
ALGOL 60 Revised Report.
Use, but do not define, the metalinguistic variables
<identifier> and <constant>.
- (10 points)
Suppose that we consider only functions that contain no assignments.
Does the typed Lambda Calculus provide an exact formalization of
Section 4.7.3 of the
ALGOL 60 Revised Report?
Explain briefly.
- (5 points)
Compare Figure 8.1 of the text with
Section 12 of the CoolAid.
Carefully explain the essential differences (if any).
Be specific!