Due Monday, May 2 at 11:59PM.
This assignment will give you practice with lambda calculus, including how substitution, alpha-conversion, and reduction work. These concepts are fundamental to the lambda calculus and form the basis of the semantics for many programming languages.
Make a clone of the the following git-repository:
git clone linux.cs.tufts.edu:/comp/105/git/lambda
which should give you a directory lambda with files linterp.sml, Lhelp.ui, Lhelp.uo, Makefile, and basis.lam.
You will be implementing a small, interactive interpreter for the lambda calculus. This section explains how to use the interpreter and the syntax it expects. A reference implementation of the interpreter is available in /comp/105/bin/linterp.
Every definition must be terminated with a semicolon.
Comments are C++ style line comments, starting with the string //
and ending at the
next newline.
A definition can be a term, a binding, or a use
statement.
A use
statement loads a file into the interpreter as if it had been typed in directly.
A use
statement is of the form
-> use filename;
When a term is entered at the toplevel, any free variables in the term which appear in the environment are substituted with their bindings in the environment, then the term is reduced to normal form (if possible) and the result is printed.
-> term;
A binding first evaluates the term on the right hand side as above, and then binds the name on the left hand side to the resulting term in the environment. It is an error for the term on the right hand side to contain any free variables which are not bound in the environment. Bindings are of the form:
-> name = term;
or
-> noreduce name = term;
If the noreduce
keyword appears, the term on the right-hand side is not normalized.
This tactic can be useful for terms that have no normal form, such as
noreduce bot = (\x.x x)(\x.x x); noreduce Y = \f.(\x.f(x x))(\x.f(x x));
A lambda term can be either a variable, a lambda abstraction, an application, or a parenthesized lambda term. Precedence is as in ML. A lambda abstraction is written as follows. Note that each lambda abstraction abstracts over exactly one variable.
\name.term
Application of one term to another is written:
term1 term2
The lambda interpreter is very liberal about names of variables.
A name is any string of characters that contains neither whitespace,
nor control characters, nor any
of the following characters: \
(
)
.
=
/
.
Also, the string
use
is reserved and is therefore not a name.
So for example, the following are all legal:
1 = \f.\x.f x; True = \x.\y.x; one = True 1;
A healthy lambda interpreter should be capable of something like the following:
<transcript>= -> true = \x.\y.x; -> false = \x.\y.y; -> pair = \x.\y.\f.f x y; -> fst = \p.p (\x.\y.x); -> snd = \p.p (\x.\y.y); -> true; \x.\y.x -> fst (pair true false); \x.\y.x -> snd (pair true false); \x.\y.y -> if = \x.\y.\z.x y z; if -> (if true fst snd) (pair false true); \x.\y.y -> (if false fst snd) (pair true false); \x.\y.y
For more example definitions, see the basis.lam
file distributed
with the assignment.
For these problems, you may work on your own or with a partner. Please provide implementations for Exercises 1-3, described below. The purpose of these problems is to help you learn about substitution and reduction, the fundamental operations of the lambda calculus. The problems will also give you a little more practice in continuation passing, which is an essential technique in lambda-land.
For these problems, define appropriate types and functions in
linterp.sml
. When you are done, you will have a working lambda
interpreter. Some of the code we give you (Lhelp.ui and
Lhelp.uo) is object code only, so you will have to build the
interpreter using Moscow ML.
Typing make should do it.
1. Evaluation—Basics. Using ML, create a type definition for a type term, which should represent a term in the untyped lambda calculus. Using your representation, define the following functions with the given types:
lam : string -> term -> term (* lambda abstraction *) app : term -> term -> term (* application *) var : string -> term (* variable *) cpsLambda : (* observer *) forall 'a . term -> (string -> term -> 'a) -> (term -> term -> 'a) -> (string -> 'a) -> 'a
These functions must obey the following algebraic laws:
cpsLambda (lam x e) f g h = f x e cpsLambda (app e e') f g h = g e e' cpsLambda (var x) f g h = h x
The official solution to this problem is under 15 lines of ML code.
2. Evaluation—Substitution. Implement substitution on your term representation. To implement substitution, you should define the following two functions:
You should use the function cpsLambda to define these functions. Additional helper functions are likely useful. The official solution to this problem is just under 40 lines of ML code.
3. Evaluation—Reductions. In this problem, use your substitution function to implement two different evaluation strategies:
The official solution to this problem is under 20 lines of ML code.
You should submit two files:
When you are ready, run submit105-lambda-pair to submit your work. Note you can run this script multiple times; we will grade the last submission.
Here are some common mistakes to avoid in implementing the lambda calculus interpreter:
\x.M x --> M provided x is not free in MHere is a reduction in two eta steps:
\x.\y.cons x y --> \x.cons x --> consYour interpreters must eta-reduce when possible.
<transcript of interpreter without reductions>= -> thing = \x.\y.y x; thing -> thing; (\thing.thing) \x.\y.y x
Everything is correct here except that the code claims something is in normal form when it isn't. If you reduce the term by hand, you should see that it has the normal form you would expect.
Your ML code will be judged by the usual criteria, emphasizing
Back to the class home page