Start early and come to us with questions.

**Due:** 11pm on Wednesday, November 4, 2020

**Submission:**

Submit the following files via https://handins.ccs.neu.edu/courses/119:

`Assignment07.hs`

`Church.hs`

`Compiler.hs`

`Syntax.hs`

`Eval.hs`

This assignment is meant to be worked on and submitted in pairs, but you can choose to work on your own. Note, that you need to have a team on Handins to be able to submit (a singleton team or a pair).

At the very top, the file should contain a preamble following this template.

`{- | Module : Assignment07 Description : Assignment 7 submission for CS 4400. Copyright : (c) <your name> Maintainer : <your email> -} module Assignment07 where`

The file should contain a

`main`

function which runs all tests in the submission, as well as additional definitions required by this assignment.Every top-level definition must include a purpose statement (for functions) and a type signature, followed by one or more defining equations.

Double-check that you have named everything as required and that functions required by this assignment have the correct type signatures.

Make sure your file loads into GHCi or can be compiled by GHC without any errors.

**Your grade might be reduced by up to 50% if your code does not compile and run.**

**Purpose:** To experiment with translating a higher-level language to a minimal core calculus and to practice working with Church encodings.

# Overview

In this assignment, we will perform an experiment: we will take a subset of protoScheme and compile it into pure lambda calculus. This entails: translating values (booleans and numbers, restricted to naturals), translating arithmetic and boolean operations, an if conditional, and finally, translating function calls, and global value and function definitions.

We will limit ourselves to a subset of protoScheme outlined below. However, do not modify your `Syntax`

or `Eval`

module by removing things. This experiment will exist in parallel to your main implementation.

values: only integers ≥ 0 (i.e., natural numbers) and booleans

expressions:

```
<Expr> ::= <Variable>
| (+ <Expr> <Expr>)
| (- <Expr> <Expr>)
| (* <Expr> <Expr>)
| (let (<Variable> <Expr>) <Expr>)
| (if <Expr> <Expr> <Expr>)
| (and <Expr> <Expr>)
| (or <Expr> <Expr>)
| (not <Expr>)
| (< <Expr> <Expr>)
| (> <Expr> <Expr>)
| (= <Expr> <Expr>)
| (<Variable> <Expr> <Expr>*)
```

- programs: global definitions with an expression

The goal is to have enough in place to be able to compile a factorial program and run it by applying normal reduction to it.

You are expected to refer to the following notes provided online:

- “Introduction to Lambda Calculus”, https://vesely.io/teaching/CS4400f20/l/10/10.pdf
- “Programming in Pure Lambda Calculus”, https://vesely.io/teaching/CS4400f20/l/13/13.pdf

Do ask questions. This assignment doesn’t require you to write a huge amount of code, but some of the concepts might feel a little difficult at first. The deadline for this assignment should allow you to make use of more office hours than usual.

# Pack

The assignment pack contains the following:

`Lambda.hs`

Syntax of pure lambda calculus.

`Reduce.hs`

Normal order reduction for pure lambda calculus. Contains the functions

`normalize`

and`normalizeWithCount`

, which you will use in this assignment.`Church.hs`

Church encodings of values and operations.

**You will need to complete this file.**`Compiler.hs`

Compilation from protoScheme expressions/programs into pure lambda calculus.

**You will need to modify this file.**`SimpleTests{Color}.hs`

No changes.

`SExpression.hs`

No changes.

`Parser.hs`

No changes.

# Questions

[In

`Church.hs`

] Complete the implementation of`toChurchBool`

, a function converting Haskell booleans to Church-encoded booleans, and its reverse,`fromChurchBool`

, a function for converting a Church boolean (in normal form) into its Haskell counterpart:`toChurchBool :: Bool -> Lambda fromChurchBool :: Lambda -> Maybe Bool`

The function

`fromChurchBool`

should assume that the`Lambda`

term is normalized, that is, the term will be in the canonical form presented in the lecture (or the notes) for true or false. However, due to alpha-equivalence, do you should not assume anything about the names of bound variables. For any`Lambda`

term that is not a canonical Church boolean, the function should return`Nothing`

.The two conversion functions should satisfy the following property, for all

`b`

`== Just b fromChurchBool (toChurchBool b)`

Write tests as

`test_bools`

[In

`Church.hs`

] Implement a function converting an`Integer`

*x*, where*x*≥ 0 to a Church numeral and its reverse, a conversion from a Church numeral to an integer.`toNumeral :: Integer -> Lambda fromNumeral :: Lambda -> Maybe Integer`

The function

`fromNumeral`

should assume that the`Lambda`

term is normalized, that is, the Church numeral will be in the canonical form presented in the lecture (or the notes). However, do not assume anything about the names of bound variables. For any`Lambda`

term that is not a canonical Church numeral, the function should return`Nothing`

.These operations should satisfy the following, for all

`i`

≥ 0:`== Just i fromNumeral (toNumeral i)`

Write tests as

`test_numerals`

[In

`Church.hs`

] Complete the tests and definitions of Church-encoded value operations. Writing*at least*one test for each, in the style of the example provided for`cplus`

. Write the tests in the respective`test_`

definition, replacing`undefined`

.[In

`Compiler.hs`

] Complete the`compile :: Expr -> L.Lambda`

function which will translate a protoScheme expression into pure lambda calculus. You only need to cover the above constructs. For all other cases, return`Nothing`

.[In

`Compiler.hs`

] Complete the`compileProgram`

function, which should take a protoScheme program with global definitions and translate it into a pure lambda expression. Global definitions can be translated the same way let expressions are translated. Function definitions should be recursive, using the fixed point combinator, which we will discuss in class this week.[In

`Compile.hs`

] Complete the function`factorialProgram :: Integer -> String`

, which generates the source code for a protoScheme factorial program, calculating the factorial of the given number. Write a test which generates a program for a low but interesting number (greater than 2), parses it into a protoScheme expression, compiles it into pure lambda calculus, runs it using`normalize`

, (provided in`Reduce.hs`

) and converts the result back into an integer. Note: this will be*slow*. Like,*very*slow. Make sure you test your compiler with simpler functions first.Run the program with 4 as the parameter using

`normalizeWithCount`

. This function will return the normalized lambda term (which should represent the factorial of 4) paired up with the total number of reduction steps it took to normalize the lambda expression. In`Assignment07.hs`

, write the number of steps taken to reduce factorial of 4 as a global variable`fact4StepsBefore`

. Modify your`compileProgram`

function so that it normalizes function bodies (using`normalize`

). This is a simple optimization step, optimizing the function body before it runs on actual arguments. Rerun the factorial calculation with`normalizeWithCount`

and write the number of steps as`fact4StepsAfter`

in`Assignment07.hs`

. If you have time, try the above experiment with the factorial of 5 and add your results as`fact5StepsBefore`

and`fact5StepsAfter`

.