Overview

Lambda calculus is not just a universal model of computation—it is also a language you can use to communicate with educated people around the world. In this assignment,

• You use lambda calculus to write simple functions
• You implement lambda calculus using substitution, reduction, and alpha-conversion

Substitution, reduction, and alpha-conversion are found all over programming-language semantics, not just in lambda calculus.

Setup

TL;DR: download the template solution and compile with compile105-lambda. Everything will be fine.

Behind the curtain: For the first part, coding in lambda calculus, you will code things from scratch. For the second part, implementing lambda calculus, you will extend an interpreter I’ve written. But because you can work with ML modules now, you won’t be stuck modifying a huge pile of code. Instead, you’ll define several modules, for both implementation and testing, and you’ll use several of my interfaces.

The ML module system is nice, but Moscow ML’s module bureaucracy is not at all nice. I’ve hidden the bureaucracy behind a shell script, compile105-lambda. This script lives in /comp/105/bin, and if you run use comp105 at the command line, you have access to it. But if something goes wrong, you may wish to know about the pieces of the assignment. Here are the source codes:¹

church.lam	Your solutions to the first part
solution.sml	Your module implementing terms, substitution, and reduction
client.sml	Your module demonstrating term functions
string-tests.sml	Test cases for your classmates’ code
subst-tests.sml	Test cases for substitution
link-lambda.sml	Instructions for linking your code with mine
link-lambda-a.sml	More instructions for linking your code with mine
link-lamstep.sml	Even more instructions for linking your code with mine

Using these sources, the compile105-lambda script will create binaries:

./run-solution-unit-tests	Runs some of your unit tests
./run-client-unit-tests	Runs more unit tests
./run-string-tests	Runs more unit tests
./run-subst-tests	Runs the last of your unit tests
./linterp	Runs your complete interpreter (normal-order reduction)
./lamstep	Runs your interpreter, showing each reduction
./linterp-applicative	Runs your complete interpreter (applicative-order reduction)

Learning about the lambda calculus

There is no book chapter on the lambda calculus. Instead, we refer you to these resources:

1. The edited version of Raúl Rojas’s “A Tutorial Introduction to the Lambda Calculus” is short, easy to read, and covers the same points that are covered in lecture:

   • Syntax
   • Free and bound variables
   • Capture-avoiding substitution
   • Addition and multiplication with Church numerals
   • Church encoding of Booleans and conditions
   • The predecessor function on Church numerals
   • Recursion using the Y combinator

   Rojas doesn’t provide many details, but he covers everything you need to know in 9 pages, with no distracting theorems or proofs.

   When you want a short, easy overview to help you solidify your understanding, Rojas’s tutorial is your best source.

2. I have written a short guide to coding in Lambda calculus. It shows how to translate ML-like functions and data, which you already know how to program with, into lambda calculus.

   When you are solving the individual programming problems, this guide is your best source.

3. Prakash Panangaden’s “Notes on the Lambda-Calculus” cover the same material as Rojas, but with more precision and detail. Prakash is particularly good on capture-avoiding substitution and change of bound variables, which you will implement.

   Prakash also discusses more theoretical ideas, such as how you might prove inequality (or inequivalence) of lambda-terms. And instead of just presenting the Y combinator, Prakash goes deep into the ideas of fixed points and solving recursion equations—which is how you achieve recursion in lambda calculus.

   When you are getting ready to implement substitution, Prakash’s notes are your best source.

4. I have also written a short guide to reduction strategies. It is more useful than anything that could be found online in 2018. As a bonus, it also explains eta-reduction, which is neglected by other sources.

   When you have finished implementing substitution and are ready to implement reduction, this guide is your best source.

5. Wikipedia offers two somewhat useful pages:²

   • The Lambda Calculus page covers everything you’ll find in Rojas and much more besides. (If you wish, you can read what Wikipedia says about reduction strategies and evaluation strategies. But do not expect to be enlightened.)

   • The Church Encoding page goes into more detail about how to represent ordinary data as terms in the lambda calculus. The primary benefit relative to Rojas is that Wikipedia describes more kinds of arithmetic and other functions on Church numerals.

   You need to know that the list encoding used on Wikipedia is not the list encoding used in COMP 105. In order to complete the homework problems successfully, you must use the list encoding described in the guide to coding in lambda calculus.

Introduction to the lambda interpreter

You will implement the key components of an 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-nr.

Syntax

The syntax of definitions

Like the interpreters in the book, the lambda interpreter processes a sequence of definitions. The concrete syntax is very different from the “bridge languages” in the book. Every definition must be terminated with a semicolon. Comments are line comments in C++ style, starting with the string // and ending at the next newline.

The interpreter supports four forms of definition: a binding, a term, the extended definition “use”, and an extended definition “check-equiv”.

Bindings

A binding is something like a val form in μScheme. A binding has one of two forms: either

noreduce name = term;

or

name = term;

In both forms, every free variable in the term must be bound in the environment—if a right-hand side contains an unbound free variable, the result is a checked run-time error. The first step of computation is to substitute for each of the free variables: each occurrence of each free variable is replaced by that variable’s definition.

In the first form, where noreduce appears, no further computation takes place. The substituted right-hand side is simply associated with the name on the left, and this binding is added to the environment.

The noreduce form is intended only for terms that cannot be normalized, such as

noreduce bot = (\x.x x)(\x.x x);
noreduce Y   = \f.(\x.f(x x))(\x.f(x x));

The noreduce form is also needed for definitions that use terms like bot and Y.

If noreduce is absent, the interpreter substitutes for free variables, then reduces the term on the right until there are no more beta-redexes or eta-redexes. (You will implement the two reduction strategies presented in class.) If reduction doesn’t terminate, the interpreter might loop.

Loading files with use

The use extended definition loads a file into the interpreter as if it had been typed in directly. It takes the form

use filename;

Comparing normal forms with check-equiv

The check-equiv form immediately reduces two terms to normal form and compares them for equivalence. It has the form

check-equiv term = term;

And here are some examples:

-> check-equiv x = x;
The test passed
-> check-equiv \x.x = \y.y;
The test passed
-> check-equiv \x.x = \y.x;
The test failed: terms \x.x and \y.x do not have equivalent normal forms
-> check-equiv (\x.x)(\y.y) = \z.z;
The test passed
-> check-equiv \f.f = \f.\x.f x;
The test passed

Unlike the check-expect in the other interpreters, check-equiv is not “saved for later”—the given terms are normalized right away.

Terms as definitions

As in the book, a term can be entered at the read-eval-print loop, just as if it were a definition. Every free variable in the term is checked to see if it is bound in the environment; if so, each free occurrence is replaced by its binding. Free variables that are not bound in the environment are permissible; they are left alone.³ The term is reduced to normal form (if possible) and the result is printed.

-> term;

The syntax of terms

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 abstracts over exactly one variable; it is written as follows:

\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. But a name made up entirely of digits is OK; the lambda calculus has no numbers, and names like 105 have no special status.

As examples, all the following definitions are legal:

<1>  = \f.\x.f x;
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 predefined.lam file distributed with the assignment.

Software provided for you

Both capture-avoiding substitution and normal-order reduction can be tricky to implement.⁴ So that you may have a solid foundation on which to write your lambda code, I provide an interpreter linterp-nr. Running use comp105 should give you access to that interpreter.

Even with a correct interpreter, lambda code can be hard to debug. So I also provide an interpreter called lamstep-nr, which shows every reduction step. Some computations require a lot of reduction steps and produce big intermediate terms. Don’t be alarmed.

All questions and problems

• There are four problems on programming with Church numerals, which you’ll do on your own.

• There are four problems on implementing the lambda calculus, which you can do with a partner. Your solutions will go into a Standard ML module, which you will link with the rest of the interpreter.

Reading comprehension

These problems will help guide you through the reading. We recommend that you complete them before starting the other problems below. You can download the questions.

Programming in the lambda calculus (individual problems)

These problems give you a little practice programming in the lambda calculus. Most functions must terminate in linear time, and you must do these exercises by yourself. You can use the reference interpreter linterp-nr.

Lambda-calculus programs work at the same intellectual level as assembly-language programs. Therefore, every new helper function must be well named and must be accompanied by a contract. Detailed guidance can be found below.

Helper functions listed in the assignment are exempt from the contract requirement, as are the helper functions in predefined.lam.

Complete all four problems below, and place your solutions in file church.lam.

Not counting code copied from the lecture notes, my solutions to all four problems total less than fifteen lines of code. And all four problems rely on the same related reading.

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

-> binary <0>;
\f.\x.x
-> binary <1>;
\f.f
-> binary <2>;
\f.\x.f (f (f (f (f (f (f (f (f (f x))))))))) // f applied 10 times
-> binary <3>;
\f.\x.f (f (f (f (f (f (f (f (f (f (f x)))))))))) // f applied 11 times

  noreduce binary = ... ;

-> binary-sym O l <0>;
O
-> binary-sym O l <1>;
l
-> binary-sym O l <2>;
l O
-> binary-sym O l (+ <2> <4>);
l l O
-> binary-sym Zero One (+ <2> <4>);
One One Zero
-> binary-sym O l (+ <1> (* <4> (+ <1> <2>)));
l l O l

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

Implementing the lambda calculus (possibly with a partner)

For problems 5 to 8 below, you may work on your own or with a partner. These problems help you learn about substitution and reduction, the fundamental operations of the lambda calculus. The first problem also gives you a little more practice in using continuation-passing to code an algebraic data type, which is an essential technique in lambda-land.

For each problem, you will implement types and functions described below. When you are done, the compile105-lambda script will link your code with mine to build a complete lambda interpreter. To simplify the configuration, most of the functions and types you must define will be placed in a module called SealedSolution, which you will implement in a single file called solution.sml. The module must be sealed with this interface:

signature SOLUTION = sig

  (************************* BASICS *************************)

  eqtype term
  val lam : string -> term -> term    (* lambda abstraction *)
  val app : term -> term -> term      (* application        *)
  val var : string -> term            (* variable           *)
  val cpsLambda :                     (* observer           *)
    (* forall 'answer . *)
    term -> 
    (string -> term -> 'answer) -> 
    (term -> term -> 'answer) -> 
    (string -> 'answer) -> 
    'answer

  (* These functions 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
   *)


  (********************** SUBSTITUTION **********************)

  val freeIn : string -> term -> bool
  
  val freeVars : term -> string list

  val subst : string * term -> (term -> term)
    (* subst (x, M) returns the capture-avoiding substitution
       of M for x ("x goes to M") *)


  (****************** REDUCTION STRATEGIES ******************)

  val reduceN : term Reduction.reducer  (* normal order *)
  val reduceA : term Reduction.reducer  (* applicative order *)

end

You can download a template solution.

structure S = SealedSolution
fun toString t = S.cpsLambda t
      (fn name => fn trm => "(lambda (" ^ name ^ ") " ^ toString trm ^ ")")
      (fn t1 => fn t2 => "(" ^ toString t1 ^ " " ^ toString t2 ^ ")")
      (fn name => name)
val N : S.term = S.app (S.app (S.var "fst") (S.var "x")) (S.var "y")
val checkExpectTerm = Unit.checkExpectWith toString
val () = checkExpectTerm "subst, case (a)" (fn () => S.subst ("x", N) (S.var "x")) N
val () = checkExpectTerm "subst, case (b)" ...
val () = checkExpectTerm "subst, case (c)" ...
val () = checkExpectTerm "subst, case (d)" ...
val () = checkExpectTerm "subst, case (e)" ...
val () = checkExpectTerm "subst, renaming" ...

Hints on the implementation of reduction

The return type of reduceA and reduceN is term Reduction.result, where Reduction.result is defined by this interface, which also defines some useful helper functions:

signature REDUCTION = sig
  datatype 'a result 
    = ONE_STEPS_TO of 'a
    | DOESN'T_STEP

  val rmap : ('a -> 'b) -> ('a result -> 'b result)
     (* laws: rmap f (ONE_STEPS_TO e) = ONE_STEPS_TO (f e)
              rmap f DOESN'T_STEP     = DOESN'T_STEP          *)

  type 'a reducer = 'a -> 'a result
  
  val nostep : 'a reducer

  val >=> : 'a reducer * 'a reducer -> 'a reducer
    (* Sequential composition: try left, then right.
       Associative, with identity nostep *)
end

The helper functions rmap, nostep, and >=> are used to implement the second of two possible implementation options:

• The first-order option is simply to take a term, break its representation down by cases, and in each case, define a right-hand side that combines all the rules for that case, including the Eta rule. The advantage of this option is it’s concrete, and the programming techniques are ones you’ve been using all along—break down the data by cases, apply the rules. The disadvantage is that there are a lot of cases, and the logic on the right hand side is complicated. Once you’ve written the code, it will be hard to understand and hard to debug. Students choosing this option often forget cases or botch cases.

• The higher-order option is to define each rule as its own function, then to compose the functions using the >=> operator in the Reduction module.⁶ The advantage of this option is that the construction of the reduction strategy makes it crystal clear what is going on and in what order—it becomes very hard to forget or botch a case. This option also makes it easy to implement and test one rule at a time. The disadvantage of this option is that it is abstract, and it is aggressively higher-order: you are using the >=> arrow to compose simple functions into more complex functions. Understanding the “reducer” abstraction well enough to implement it will take a little time.

Notes on the higher-order option

If you want to try the REDUCTION interface and the higher-order option, here are some notes:

• The type called 'a reducer is really a partial reducer: a function of this type implements some sequence of rules. Function nostep implements no rules, and the composition arrow >=> combines two functions to implement a combined sequence of rules. Your implementation task breaks down into two steps: first, define rule functions; second, compose them.

• The rmap function is the classic mapping idea (called “homomorphic”) which you have already seen in List.map and Option.map. It is especially useful in conjunction with curry, as in

  Reduction.rmap (curry lam x) (...)

  You may also find a use for flip.

• The composition arrow is mean to be used as an infix operator. In your solution file, copy these definitions:

  val >=> = Reduction.>=>
  infix 1 >=>

• The most beautiful code emerges if you define functions beta, eta, nu, mu, and xi, then compose them:

  val strategy = xi >=> mu >=> beta >=> ...  (* don't use this order *)

  But there’s a problem here: the nu, mu, and xi rules all need the capability of doing general reduction on a subterm, which means they have to be mutually recursive with the reducer. Mutually recursion can be handled in several ways, but the easiest is to define the individual rule functions inside the reducer, in a let binding. This easy way does, however, duplicate code. If you want to avoid the duplication, you can do something like this:

  fun xi_maker reducer term = (case term of ...) : term Reduction.result
  
  fun reduceZZZ m =
    let val this = reduceZZZ
        val xi = xi_maker this
        val mu = mu_maker this
        ...
        val reduce = xi >=> mu >=> beta >=> ...    (* don't use this order *)
    in  reduce m
    end

Overall, I think the higher-order option is worth the extra effort needed to understand the reducer type and its composition: when you split each rule into its own function, it’s much, much easier to get them all right. And it’s easy to reuse the same functions in multiple reduction strategies.

Debugging support

As shipped, the lambda-calculus interpreter reduces each term repeatedly, until it reaches a normal form. But when you are debugging reduction strategies, you may find it helpful to see the intermediate terms. The compile105-lambda script should produce an executable program ./lamstep, which will show the results of every reduction step. You can compare this interpreter with the reference version, called lamstep-nr.

Even more debugging support

If the ./lamstep interpreter doesn’t provide enough information (or provides too much), here is a way to print a status report after every n reductions:

fun tick show n f =  (* show info about term every n reductions *)
  let val count = ref 0
      fun apply arg =
        let val _ = if !count = 0 then
                      ( List.app print ["[", Int.toString (show arg), "] "]
                      ; TextIO.flushOut TextIO.stdOut
                      ; count := n - 1)
                    else
                      count := !count - 1
        in  f arg
        end
  in  apply
  end

I have defined a status function size that prints the size of a term. You can print whatever you like: a term’s size, the term itself, and so on. Here is how I show the size of the term after every reduction. Some “reductions” make terms bigger!

val reduceN_debug = tick size 1 reduceN  (* show size after every reduction *)

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 solution.sml file.

What and how to submit: Individual work

Using script submit105-lambda-solo, submit

• A README file containing
  • The names of the people with whom you collaborated
  • Any extra credit you may have earned
• File cqs.lambda.txt, containing your answers to the reading-comprehension questions
• File church.lam containing your solutions to the Church-numeral problems, including possibly the binary-sym extra credit

As soon as you have the files listed above, run submit105-lambda-solo to submit a preliminary version of your work. Keep submitting until your work is complete; we grade only the last submission.

What and how to submit: Pair work

Using script submit105-lambda-pair, submit

README	Collaborators, extra credit, and so on
solution.sml	Your module implementing terms, substitution, and reduction
subst-tests.sml	Test cases for substitution

As soon as you have the files listed above, and all the code compiles, run submit105-lambda-pair to submit a preliminary version of your work. Keep submitting until your work is complete; we grade only the last submission.

Avoid common mistakes

Common mistakes with Church numerals

Here are some common mistakes to avoid when programming with Church numerals:

• Don’t forget names and contracts for helper functions.

• Don’t forget a semicolon after each definition.

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

• When using a fixed-point combinator to define a function, don’t forget to use noreduce in the definition form.

• Don’t use the list representation or primitives from Wikipedia. We will test your code using the representation and primitives from Coding in Lambda Calculus, which you will also find in the file predefined.lam.

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

• Don’t copy predefined terms from predefined.lam. We will load the predefined terms before running your code.

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

  cat predefined.lam church.lam | linterp-nr

  If you want to build a test suite, put your tests in file test.lam and run

  cat predefined.lam church.lam test.lam | linterp-nr

Common mistakes with the lambda interpreter

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

• Don’t forget the Eta rule:

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

  Here is a 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 (the Xi rule).

• Don’t forget that in an application M₁ M₂, just because M₁ is in normal form doesn’t mean the whole thing is in normal form. If M₁ doesn’t step, you must try to reduce M₂.

• If you are using the first-order implementation option, don’t clone and modify your code for reduction strategies; people who do this wind up with wrong answers. The code should not be that long; use a clausal definition with nested patterns, and write every case from scratch.

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

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

• When implementing freshVar, don’t try to repurpose function freshTyvar from section 7.6. That function isn’t smart enough for your needs.

How your work will be evaluated

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

• 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 for names:

And here are our criteria for contracts: