11:59:59pm (via the submit server)

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

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.

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.

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

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

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 * typYou will be implementing the untyped lambda calculus for now, but as you can see, the definition of

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

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

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

- 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):- The
`times`function, which multiples two (normal, not Church) integers together. You can implement this in terms of addition. - The
`fact`function to compute the factorial function. - 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.

- The
`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.- Implement the function
`ctoi`which converts a Church numeral to an integer. This will be useful for "printing". - Implement the function
`itoc`which converts a normal integer to a Church numeral (you will have to use recursion!). - 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. - Implement the two-argument function
`cmul`that multiples Church numerals. This is considerably simpler than the definition of`cwhat`, above. - Implement exponentiation function
`cexp`that takes two arguments`m`and`n`and computes`m`to the`n`power. This is even simpler than multliplication!

- Implement the function

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.

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.