COMP105 Assignment: Lambda Calculus

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.

Setup

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.


Introduction to the Lambda Interpreter

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.

Concrete syntax

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 short example transcript

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.


Pair Problems

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.

Problem Details

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:

  1. Implement normal-order reduction on terms. That is, write a function reduceN : term -> term that takes a term, performs a single reduction step (either beta or eta) in normal order, and returns a new term. If the term you are given is already in normal form, your code should raise the exception NormalForm, which you should define.

  2. Implement applicative-order reduction on terms. That is, write a function reduceA : term -> term that takes a term, performs a single reduction step (either beta or eta) in applicative order, and returns a new term. If the term you are given is already in normal form, your code should raise the exception NormalForm, which you should reuse from the previous part.

The official solution to this problem is under 20 lines of ML code.

What to submit: Pair Problems

You should submit two files:

How to submit: Pair Problems

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.


Hints and guidelines

The lambda intepreter

Here are some common mistakes to avoid in implementing the lambda calculus interpreter:

How your work will be evaluated

Your ML code will be judged by the usual criteria, emphasizing

Back to the class home page