Submission Instructions

This is an individual assignment. Just as with all other homework, submitted work should be your own. Course staff runs plagiarism detectors and will treat excessive similarities between submissions as evidence of cheating. Submit in Submitty for autograding. Your Haskell file must be named Interpreter.hs. Submitty compiles your Interpreter module using The Glorious Glasgow Haskell Compilation System, version 8.6.5 and links it with various tests that call your functions.

Getting Started with Haskell

Download and install the Glasgow Haskell Compiler: https://www.haskell.org/ghc.

You can run GHC in interactive mode by running ghci from the command line. Try all examples from lecture before starting on the homework. You can type the functions from lecture into a file called, e.g., fun.hs: 

apply_n f n x = if n == 0 then x else apply_n f (n-1) (f x)
 
plus a b = apply_n ((+) 1) b a
 
mult a b = apply_n ((+) a) b 0
 
expon a b = apply_n ((*) a) b 1

 

Run ghci then load the file by typing 

 
:l fun.hs

 

and call these functions, e.g., plus 2 3. You can reload the file after making a change 

 
:r
 
Add ADTs and functions to your file. E.g., the Yabi interpreter from HW4 is a good exercise to start with and get more familiar with Haskell syntax and type error messages.

A Normal Order Normal Form Interpreter for the Lambda Calculus

Now, we will describe the actual homework. In lecture, we wrote several interpreters for the Lambda Calculus. They terminated when they reached an answer in Weak Head Normal Form. In this homework you will write a normal order interpreter that yields an answer in Normal Form (i.e., the expression cannot be further reduced).

Problem 1. Normal order Normal form interpreter

Your first task is to write an interpreter in the style we gave in lecture (Lecture 19). Please include your answer in comments in your Haskell file under heading Problem 1.

Problem 2. Coding the interpreter in Haskell

Next, you will code an interpreter in Haskell. Note however, that you will not be coding the recursive interpretation from Problem 1 but a step-by-step interpretation. The key function is the oneStep function. It takes a lambda expression and either (i) carries out one step of evaluation yielding the next expression, or (ii) yields Nothing, meaning that the expression is already in the target normal form.

 

A lambda expression is of the following form, as we discussed in class: 

 
data Expr =
 Var Name --- a variable
 | App Expr Expr --- function application
 | Lambda Name Expr --- lambda abstraction
Deriving
 (Eq,Show) --- the Expr data type derives from built-in Eq and Show classes,
 --- thus, we can compare and print expressions
 
type Name = String --- a variable name

You need to implement the following functions:

Free variables. Write the function to compute the list of free variables in an expression.

freeVars :: Expr -> [Name]

It takes an expression and returns the list of free variables in that expression. For example, freeVars (App (Var "x") (Var "x")) returns ["x"].

 

You will use freeVars to generate an (infinite) list of variables that are not free in an expression; variables from that list can be used as fresh variables when needed for substitution. For example, given expression Lambda "1_" (App (Var "x") (App (Var "1_") (Var "2_"))), the infinite list of potential fresh variables is ["1_","3_","4_","5_",..]. Remember, you will make use of the infinite list of integers [1..] for this purpose.

Substitution. Next, write the substitution function

subst :: (Name,Expr) -> Expr -> Expr

All functions in Haskell are curried: i.e., they take just one argument. The above function takes a variable x and an expression e, and returns a function that takes an expression E and returns E[e/x]. Important: subst needs to implement the algorithm we gave in class (Lecture 15). Specifically, when performing a substitution of x with e on a lambda expression λy.E1, where y≠x, subst replaces parameter y with the next fresh variable from the infinite list of potential fresh variables, even if y is not free in e and it would have been safe to leave it as is. (This is necessary for autograding on Submitty. An alternative would have been to normalize the expression using DeBruijn indices.) Remember, the infinite list of potential fresh variables is ["1_","2_","3_"..] excluding variables that are free in x, E1 or e.

 

A single step. Now write a function to do a single step of reduction:

normNF_OneStep :: Expr -> Maybe Expr

where the built-in Maybe type is defined as follows: 

data Maybe a =
 Nothing
 | Just a

normNF_OneStep takes an expression e. If there is a redex available in e, it picks the correct normal order redex and reduces e. If a reduction was carried out, resulting in a new expression expr', normNF_OneStep returns Just expr', otherwise, i.e., the input expression is already in normal form, normNF_OneStep returns Nothing.

Repetition. Finally, write a function

normNF_n :: Int -> Expr -> Expr

Given an integer n and an expression e, normNF_n does n reductions (or as many as possible) and returns the resulting expression.

Minimal starter code is provided here.

Notes on grading: This homework is worth a total of 50 points: 40 points will be awarded for functional correctness by the autograder and 10 points will be awarded for quality and completeness of Problem 1 and comments.

Errata

None yet. Check the Announcements on Submitty regularly.