There are 25 points total for this assignment.
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:
Call-by-value multi-step operational semantics (evaluation of an expression by some number (including 0) of steps):
Questions:
a) [4 Points] Rewrite the operational semantics for variants using formal inductive rules. First, define the judgment e ++> e' as the single step evaluation function. Then, define the judgment e ++>* e' to be the judgment for multi-step evaluation in the language. The multi-step judgement will make use of the single step judgement.
b) [4 Points] 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. For example, the first few rules (the easy rules) might look like this:
--------- trans-var
x ==> x
e ==> t
------------ trans-lambda
\x.e ==> \x.t
e1 ==> t1 e2 ==> t2
--------------------------- trans-app
e1 e2 ==> t1 t2
e ==> t
------------------
inl e ==> ???
...
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 (as defined in your textbook. [4 Points] 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 (but don't you don't have to prove) a lemma about substitution.
d) [3 Points] 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) [4 Points] 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 the exception Negative if the input to cnum is negative.
exception Negative
cnum : int -> term
b) [6 Points] 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