COMP105 Assignment: Lambda Calculus

Setup and Instructions

  git clone /comp/105/git/lambda

Do all problems below.

• There are three problems on implementing the lambda calculus, which you can do with a partner, For problems 1-3, modify the linterp.sml file from the git repository.

• There are four problems on programming with Church numerals, which you'll do on your own. Put your answers for to these problems, 4-7, in a file called church.lam.

Introduction to the Lambda interpreter

Concrete syntax

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

  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

<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.

Modifying the Lambda Interpreter: Exercises for pairs

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. Just typing make should do it.

1. Evaluation—Basics (estimated difficulty *). This problem has two parts:

1. 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
   

2. Using cpsLambda, define a function toString of type term -> string that converts a term to a string in uScheme syntax. Your toString function should be independent of your representation. That is, it should work using the functions above.

My solution to this problem is under 30 lines of ML code.

2. Evaluation—Substitution (estimated difficulty **). Implement substitution on your term representation. Define a function subst of type string * term -> term -> term. To compute the substitution M[x|–>N], you should call subst (x, N) M.
Also define a function freeVars of type term -> string list which returns a list of all the free variables in a term.

My solution to this problem is under 40 lines of ML code.

3. Evaluation—Reductions (estimated difficulty ***). In this problem, you 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.

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

Work with Church Numerals: Exercises to do on your own

4. Church Numerals—parity (estimated difficulty *). Without using recursion or a fixed-point combinator, define a function even? which, when applied to a Church numeral, returns the Church encoding of true or false, depending on whether the numeral represents an even number or an odd number.

Ultimately, you will write your function in lambda notation acceptable to the lambda interpreter, but you may find it useful to try to write your initial version in Typed uScheme (or ML or uML or uScheme) to make it easier to debug.

Remember,

<church numerals and Booleans>=
0    = \f.\x.x;
succ = \n.\f.\x.f (n f x);
+    = \n.\m.n succ m;
*    = \n.\m.n (+ m) 0;

true  = \x.\y.x;
false = \x.\y.y;

You can load the initial basis with these definitions already created by typing: use basis.lam; in your interpreter.

5. Church Numerals—division by two (estimated difficulty ***). Without using recursion or a fixed-point combinator, define a function div2 which divides a Church numeral by two (rounding down). That is div2 applied to the numeral for 2n returns n, and div2 applied to the numeral for 2n + 1 also returns n.

Hint: For ideas, revisit the programming problems on the midterm.

6. Church Numerals—binary (estimated difficulty **) Implement the function binary from the Impcore homework. The argument and result should be Church numerals. For example,

<transcript for binary>=
-> binary 0;
\f.\x.x
-> binary 1;
\f.f
-> binary 2;
\f.\x.f (f (f (f (f (f (f (f (f (f x)))))))))
-> binary 3;
\f.\x.f (f (f (f (f (f (f (f (f (f (f x))))))))))

For this problem, you may use the Y combinator. If you do, remember to use noreduce when defining binary, e.g.,

  noreduce binary = ... ;

EXTRA CREDIT. Write a function binary-sym that takes three arguments: a symbol for zero, a symbol for one, and a Church numeral. Function binary-sym reduces to a term that "looks like" the binary representation of the given Church numeral. Examples:

<transcript for binary-sym>=
-> binary-sym _ | 0;      
_
-> binary-sym _ | 1;
|
-> binary-sym _ | 2;
| _
-> binary-sym _ | (+ 2 4);
| | _
-> binary-sym Zero One (+ 2 4);  
One One Zero

Note: I can't identify any practical value to binary-sym. It is purely for showing off your new skills.

7. Church Numerals—list selection (estimated difficulty ***). Write a function nth such that given a Church numeral n and a church-encoded list xs of length at least n+1, nth n xs returns the nth element of xs:

-> 0;
\f.\x.x
-> 2;
\f.\x.f (f x)
-> nth 0 (cons Alpha (cons Bravo (cons Charlie nil)));
Alpha
-> nth 2 (cons Alpha (cons Bravo (cons Charlie nil)));
Charlie

Don't even try to deal with the case where xs is too short.

Hint: One option is to go on the web or go to Rojas and learn how to tell if a Church numeral is zero and if not, and how to take its predecessor. There are other, better options.

Common mistakes, alarums, and excursions

The lambda intepreter

• Don't forget the eta rule:

     \x.M x --> M   provided x is not free in M
  

  Here is an reduction in two eta steps:

    \x.\y.cons x y --> \x.cons x --> cons
  

  Your interpreters must eta-reduce when possible.

• Don't forget to reduce under lambdas.

• Don't forget to use normal-order reduction in the code you submit.

• Don't clone and modify your code for reduction strategies; too many people who do this wind up with wrong answers. The code should not be that long; just type in every case.

• Don't think that an application is in normal form just because one subterm is in normal form—you have to check both subterms. Most students do this using exception handlers, but if you are not comfortable with exception handlers, you can write your reducer in continuation-passing style instead.

• Don't try to be clever about a divergent term; just reduce it. (It's a common mistake to try to detect the possibility of an infinite loop. Mr Turing proved that you can't detect an infinite loop, so please don't try.)

  Do make sure to use normal-order reduction, so that you don't reduce a divergent term unnecessarily.

If you test an interpreter before implementing reduction, you may see some alarming-looking terms that have extra lambdas and applications. This is because the interpreter uses lambda to implement the substitution that is needed for the free variables in your terms. Here's a sample:

<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. A term that refers to even more defined variables could start to look very exciting indeed.

Programming with Church numerals

• Don't forget the question mark in the name of even?.

• When using a fixed-point combinator, don't forget noreduce.

• Don't use the list representation or primitives from Wikipedia. We will test your code using the representation and primitives described in class, which you will also find in the file basis.lam.

• Don't include any use directives in church.lam.

• Don't copy basis functions from basis.lam. We will load the basis before running your code.

  To make sure your code is well formed, load it using

    cat basis.lam church.lam | ./linterp
  

  If you want to build a test suite, run your tests by putting them in file test.lam, then running

    cat basis.lam church.lam test.lam | ./linterp
  

More Extra Credit

Solutions to any of the extra-credit problems below should be placed in your README file. Some may be accompanied by code in your linterp.sml file.

Extra Credit—Normalization. Write a higher-order function that takes as argument a reducing strategy (e.g., reduceA or reduceN) and returns a function that normalizes a term. Your function should also count the number of reductions it takes to reach a normal form. As a tiny experiment, report the cost of computing using Church numerals in both reduction strategies. For example, you could report the number of reductions it takes to reduce ``three times four'' to normal form.

This function should be doable in about 10 lines of ML.

Extra Credit—Normal forms galore. Discover what Head Normal Form and Weak Head Normal Form are and implement reduction strategies for them. Explain, in an organized way, the differences between the four reduction strategies you have implemented.

Extra Credit—Typed Equality. For extra credit, write down equality on Church numerals using Typed uScheme, give the type of the term in algebraic notation, and explain why this function can't be written in ML. (By using the ``erasure'' theorem in reverse, you can take your untyped version and just add type abstractions and type applications.)

What to submit

• Please use submit105-lambda-pair to submit your modified linterp.sml for the parts on evaluation.
• Please use submit105-lambda-solo to submit these files:
  • README
  • church.lam for the parts on Church Numerals

How your work will be evaluated

• Correct implementation of the lambda calculus
• Good form
• Names and contracts for helper functions
• Structure that exploits standard basis functions, especially higher-order functions, and that avoids redundant case analysis

Your lambda code will be judged on correctness, form, naming, and documentation, but not so much on structure. In particular, because the lambda calculus is such a low-level language, we will especially emphasize names and contracts for helper functions.

• This is low-level programming, and if you don't get your code exactly right, the only way we can recognize and reward your learning is by reading the code. It's your job to make it clear to us that even if your code isn't perfect, you understand what you're doing.

• Try to write your contracts in terms of higher-level data structures and operations. For example, even though the following function does some fancy manipulation on terms, it doesn't need much in the way of a contract:

     double = \n.\f.\x. n (\y.f (f y)) x;  // double a Church numeral
  

  Documenting lambda calculus is like documenting assembly code: it's often sufficient to say what's happening at a higher level of abstraction.

• Although it is seldom ideal, it can be OK to use higher-level code to document your lambda code. In particular, if you want to use Scheme or ML to explain what your lambda code is doing, this can work only because Scheme and ML operate at much higher levels of abstraction. Don't fall into the trap of writing the same code twice—if you are going to use code in a contract, it must operate at a significantly higher level of abstraction than the code it is trying to document.

In more detail, here are our criteria: