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:
type result = Env of env | Command of comm * envThe first case (for skip) has been implemented for you. You should use the interpreter you developed in the Exp module as a subroutine.
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 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).
(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.
(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.
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.