Project 1

Due October 1, 2007
11:59:59pm (via the submit server)

Corrections

Fixed small bug in the stated type of steps and eval for arithmetic expressions (to match what's in imp.ml).

Introduction

For this project you will implement two interpreters: one for a simple imperative language, one for an extension of the lambda calculus we'll call F. We'll then use your F interpreter to play with lambda calculus encodings.

What to Submit

You should submit three files: imp.ml for part 1; f.ml for part 2, and p1.f for part 3. Partial implementations of these files, and supporting files, can be downloaded here.

Part 1: Interpreter for an imperative language IMP

In this part we will implement the operational semantics for the language we saw in lecture. This has two pieces: a language of arithmetic expressions, and a language of imperative commands. In the file imp.ml (and its signature), these pieces are broken into two modules Exp and Command, respectively. An implementation of the the small-step semantics for arithmetic expressions has been provided for you in the function Exp.step. You need to implement two more functions in this module:

Implement the function Exp.steps : env -> exp -> int which is the reflexive, transitive closure of the step function. Your implementation should call the step function.
Implement the function Exp.eval : env -> exp -> int using the big-step semantics provided in the lecture slides. It should be the case that (steps g e) = (eval g e)

You will have to implement all of the Command module:

Implement the function Command.step : env -> comm -> result using the small step semantics. A result is either a final store (of type env) or else a reduced state, which is a pair of a store and a command:
```
type result = Env of env | Command of comm * env
```
The first case (for skip) has been implemented for you. You should use the interpreter you developed in the Exp module as a subroutine.
Implement the steps and eval functions for the command language, which have the same meaning (but applied to the full command language) as for the Arith module, described above.

To test your code, you should use the top-level, or make test cases on your own, constructing values of types exp and comm and env to test the various functions.

Part 2: F: an extended (untyped) lambda calculus

In this part we will implement the operational semantics for an extension to the lambda calculus. Here is the datatype declaration for the language:

type term =
    Int of int
  | Var of string
  | Lam of string * (typ option) * term
  | App of term * term
  | Plus of term * term
  | Let of string * term * term
  | Eq of term * term * term * term

(* Ignore types for now (we'll use them in the next project) *)
and typ =
    TInt
  | TFun of typ * typ

You will be implementing the untyped lambda calculus for now, but as you can see, the definition of term optionally includes types. Just ignore these for the moment; we'll be making use of them in the next project.

A program is a list of term definitions, binding variables (strings) to terms, followed by a final term (which you can think of as the body of main). You will implement two functions, eval and eval_lazy, each having type (string -> term option) -> term -> term, in f.ml. The first argument is the global environment, represented as a function that takes a string (a variable) and returns a term bound by that string, if one exists. The second argument is the final term. The function eval then returns the final result, following a big-step call-by-value semantics. The function eval_lazy also follows big-step semantics, but uses call-by-name instead. Feel free to implement any number of functions in support of these two functions.

The semantics of integers, variables, lambda abstractions, application, and let binding are just as in the slides. The semantics of addition should be self-explanatory. Finally, the semantics of Eq (e1,e2,e3,e4) is like an if expression: if e1, when evaluated, is syntactically equal to the fully-evaluated e2, then evaluate e3, otherwise evaluate e4.

To make it easier to test, we have provided the skeleton of an interpreter for you. If you type make it should build an executable finterp. This takes a single argument, which is the file to parse and evaluate (or no arguments, and you can provide the input on the command line); it will pretty-print the definitions it receives along with the result of the final expression. If you provide the flag -lazy it will use your eval_lazy function; by default it uses your eval function. A sample input file has been provided in the file p1.f. The concrete syntax uses S-expressions. Top-level definitions have the form

(Def var term)

where var is a variable name, and term is a term. A program is one or more top-level definitions followed by a final expression, which is just a term. A term has the syntax

term ::= I
     |   V
     |   (+ term term)
     |   (term term)
     |   (Eq term term term term)
     |   (Let V term term)
     |   (Lam V term)

Here, I is represents an integer constant, and V is a variable (an alphanumeric string beginning with a letter). The word term is a non-terminal; all other syntax is concrete. Hopefully the file p1.f (and the implementation of the parser/lexer in fparse.mly and flex.mll) makes things clear enough. Finally, comments are as in OCaml, contained within (* and *) delimiters (which can be nested).

Things to think about

Substituion is tricky: make sure you properly handle variable renaming so as to ensure it is "capture avoiding."
You might want to use the pretty printer to print intermediate representations of terms during evaluation for debugging.
As a quick test of your lazy vs. eager semantics, try evaluating ((t 1) (w w)). This should fail with a stack overflow for the eager case, and should evaluate to 1 in the lazy case.

Part 3: Programming with Lambda calculus

Now that you have implemented a lambda calculus interpreter, you can use your implementation to play with encodings of the lambda calculus. In particular, extend the file p1.f to include implementations the following functions (delimit the functions for each problem using comments, e.g., (* problem 1 *), (* problem 2 *), etc.).

As discussed in class, we can implement recursion via a fixpoint operator, like the Y combinator (or Z for call-by-value). The prelude of pl.f has the definitions of both. Use them to implement the following functions (which should work for both call-by-name and call-by-value):
1. The times function, which multiples two (normal, not Church) integers together. You can implement this in terms of addition.
2. The fact function to compute the factorial function.
3. The fact_encode function, which is the factorial function using normal integers, but with an encoding of booleans. Use the provided function int_iszero which takes a single argument n and returns an encoding for true if n is equal to 0, and the encoding for false otherwise:
```
(Def int_iszero (Lam n (Eq n 0 t f)))
```
  Then adapt your fact function to use these encodings. Does the function provided work for both call-by-name and call-by-value? If it doesn't work for both, how can you change the encoding of booleans so that it does? If it does work for both, explain why the evaluation strategy doesn't make any difference in this case? You can use the Z combinator to implement your function for both strategies.
p1.f contains encodings of Church numerals in the definitions zero, one, and two, along with predicates iszero which returns 0 if the given Church numeral is 0, and succ which adds one to a Church numeral.
1. Implement the function ctoi which converts a Church numeral to an integer. This will be useful for "printing".
2. Implement the function itoc which converts a normal integer to a Church numeral (you will have to use recursion!).
3. Consider the following function cwhat:
```
(Def cwhat (Lam m (Lam n (Lam f (Lam x ((m f) ((n f) x)))))))
```
  What well-known arithmetic function does this compute? Justify your answer by including some experiments.
4. Implement the two-argument function cmul that multiples Church numerals. This is considerably simpler than the definition of cwhat, above.
5. Implement exponentiation function cexp that takes two arguments m and n and computes m to the n power. This is even simpler than multliplication!

Note that the answers to many of these questions can be found in Pierce. Don't look at the answers until you've given the questions a solid try!

Also, if you don't manage to get part 2 working, feel free to implement this part in Scheme instead. The syntax of F is quite similar.

Academic Integrity

The Campus Senate has adopted a policy asking students to include the following statement on each assignment in every course: "I pledge on my honor that I have not given or received any unauthorized assistance on this assignment." Consequently your program is requested to contain this pledge in a comment near the top.

Please carefully read the academic honesty section of the course syllabus. Any evidence of impermissible cooperation on projects, use of disallowed materials or resources, or unauthorized use of computer accounts, will be submitted to the Student Honor Council, which could result in an XF for the course, or suspension or expulsion from the University. Be sure you understand what you are and what you are not permitted to do in regards to academic integrity when it comes to project assignments. These policies apply to all students, and the Student Honor Council does not consider lack of knowledge of the policies to be a defense for violating them. Full information is found in the course syllabus---please review it at this time.