Rules for collaboration: You may discuss the problem sets with other students to increase your understanding of the material. However, what you write down and turn in should be your own work.

All problem sets are due at 11:00 a.m. in class on the due date.

1.  Read Pierce, chapter 5.

2.  Consider adding variants (similar to ML datatypes) to the untyped lambda calculus, according to the following specification.

Syntax

e ::= x | \x.e | e e | inl e | inr e | case e of (inl x => e | inr x  => e)

(I am using the symbol "\" for the Greek letter lambda simply because I can't figure out how to get the text editor I am using to create this HTML document to format the Greek letter lambda properly right now. When you turn in your solutions, you can either use "\" or a real lambda... I don't care)

The values in this variant of the lambda calculus are

v ::= \x.e | inl v | inr v

Call-by-value single-step operational semantics:

• the normal call-by-value evaluation rules for functions and function application.
• if e takes a single step and results in e' then (inl e) steps to (inl e') in a single step.  A similar rule applies for (inr e). 
• if e1 is inl(v), where v is a value, then (case e1 (inl x => e2 | inr x => e3)) reduces to e2 with the variable x replaced by v.  And similarly when e1 is inr(v).

Call-by-value multi-step operational semantics (evaluation of an expression by some number (including 0) of steps):

• reflexivity: any expression evaluates to itself in some number of steps
• transitivity: if an expression e can evaluate in a single step to some intermediate expression and then that intermediate expression can evaluate in some number of steps to another expression e', then e itself can evaluate in some number of steps to e'.

Questions:

a)  Rewrite the operational semantics for variants using formal inductive rules as follows.  First, write down the rules for capture-avoiding substitution e[e'/x] (assume that we identify terms up to renaming of their bound variables).  Next, define the judgment e ++> e' as the single step evaluation function.  Finally, define the judgment e ++>* e' to be the judgment for multi-step evaluation in the language. 

b) Show how to encode variants in the untyped lambda calculus (without variants) formally by defining a translation function that maps any expression in the language defined above (ie: in the untyped lambda calculus + variants) into the pure untyped lambda calculus (ie: untyped lambda calculus with no inr, inl, case expressions).  In other words, I want you to define a judgment that expresses the translation. The translation judgment should have the form:

e ==> t

where e is a expression in "untyped lambda calculus + variants" and t is an expression that uses only lambda terms.

c)  Rhetorical question:  What does it mean for your translation to be correct?  One way to demonstrate the correctness of the translation is to prove that your translation preserves the evaluation semantics of the source language.  Let t -->* t' be the judgment for the multistep call-by-value evaluation of pure lambda terms. Prove the following theorem:

Theorem:  If e ==> t and e ++>* e' then there exists t' such that e' ==> t' and t -->* t'.

Like good programs, good proofs are well-structured objects.  In particular, good proofs use lemmas to capture the "key ideas" in the proof.  As a part of your proof, state and prove a useful lemma about single-step evaluation.  Also, if necessary, state and prove a lemma about substitution.

d)  The theorem above only captures a part of the correctness criterion for the translation.  Formally state another general theorem that captures a different element of the correctness criterion.  Explain what your theorem means in plain English.  Hint: What other similarities should hold between the source and target language evaluation relation that are not captured by the theorem above?

3.  This question is about implementing the lambda calculus in ML.  A first-order representation strategy for the lambda calculus in ML represents variables in the lambda calculus using strings.  In other words, a first-order representation strategy might use the following datatype definition to represent the syntax of the lambda calculus:

datatype fstterm = Var of string | Lambda of string * fstterm | App of fstterm * fstterm

To represent the function \x.\y. x y we would build the following data type:

Lambda ("x",Lambda ("y", App (Var "x", Var "y")))

This is quite a reasonable thing to do.  However, in order to implement an evaluator for these lambda-terms, we have to put a fair amount of work into defining alpha-renaming and substitution properly.  In other words, we need to write explicit ML functions that recurse over terms in order to implement substitution.

An alternative technique is to use a higher-order representation strategy.  A higher-order strategy uses ML variables to implement lambda calculus variables.  In order to make this work, whenever we have a binding occurrence of a variable (like the x in \x.e), we will represent the binding occurrence using an ML function.  The body of the ML function will simply be an ML datatype that represents the body of the lambda calculus term.

Here is the datatype that gives rise to a higher-order representation strategy for the lambda calculus:

datatype term = Lambda of term -> term | App of term * term

Notice that there is no datatype alternative for variables.  We will use ML variables with ML type "term" to stand for variables in the lambda calculus.  Also observe that functions in the lambda calculus are implemented using functions in the ML.  To represent the function \x.\y. x y we would build the following data type:

Lambda (fn (x : term) =>

                  Lambda (fn (y : term) => App (x, y)))

Cool huh?  To understand what is going on here, it will probably help to open up the ML interpreter and type in this expression yourself.  Notice that the expression is well-typed in ML.  Try typing in a couple of other terms.

Questions:

a)  Implement a function called cnum in ML that translates natural numbers into their Church representation in the lambda calculus implemented using the higher-order representation strategy given above.  See Pierce, chapter 5.2 (pp 60-63) for the Church representation of numbers.  You can raise an exception if the input to cnum is negative.

cnum : int -> term

b)  Implement an evaluator for the lambda calculus.  Your function eval should implement your rules for the multi-step, call-by-value operational semantics as directly as possible.  If complete evaluation of the term e produces a value, then this value should be returned as the result of (eval e).  Clearly, implementing evaluation for "App" will be the hard part.

eval : term -> term

c)  Extend the higher-order datatype definition so that the lambda calculus contains variants (inl, inr, case) as described earlier this assignment.  Extend the evaluator you wrote in part b so that it handles variants.  If no evaluation rules are defined for a particular term and it is not a value, then you should raise an exception when asked to evaluate it.  For example, if you are asked to evaluate an expression such as

App (Inl v, Inl v')

that requires that you use a value such as "Inl v" as if it was a function, then you should raise an exception. 

For this part of the assignment, hand in the code for your function from part a, the final data type declaration and the final evaluator.  Also hand in the result of running your evaluator on a couple of different lambda terms to demonstrate that it operates correctly.