To submit your code, first commit and push your repository to GitHub.

You must include at the top level of your assignment repository a file called INTEGRITY.md that gives credit to all sources you used while working on the assignment. So that you have an idea of the level of detail that is expected, we have provided an example INTEGRITY.md file. Thorough citation is the way to avoid running afoul of accusations of misconduct.

When you have completed the assignment, submit your files to the autograder using autograder-py, which is the autograder's command-line client program (or "autograder client" for short).

You may already have the autograder client installed if you've used it in other classes. If not, install it by running the following command from the command line:

$ pip3 install autograder-py

(The $ above is not part of the command; it just indicates that the command should be run at the command line. We use this same convention throughout this assignment description.)

You need to have Python installed on your system to use the autograder client. If you are using the CSE 114A Dev Container, the autograder client is already installed.

To submit code to the autograder, you will need to specify some configuration settings at the command line.

Submit your code by running the following command from the command line when at the top level of your repository:

$ python3 -m autograder.run.submit INTEGRITY.md tests/* --user <email> --pass <password> --course <course>

where

• <email> is your UCSC email address;
• <password> is your autograder password (not your UCSC Blue or Gold password -- your autograder password is specific to the autograder, and you should receive an email with your own password);
• and <course> is an identifier specific to this course and section, which you can find on the Canvas assignment description for this assignment.

Running this command will submit your code to the autograder for evaluation and print out the results. Have patience -- it might take a minute or two to see output from the autograder. You can submit as many times as you like before the deadline, and only the last submission will be counted.

The autograder client has other commands that you can use to interact with the autograder. In particular, you can run python3 -m autograder.run.peek to see the results of your last submission, and python3 -m autograder.run.history to see the results of all your submissions. Refer to the autograder client documentation for more information.

The objective of this assignment is for you to understand the lambda calculus and the notion of computation-by-substitution.

You will write programs directly in the lambda calculus, and test them using an interpreter called Elsa. The Elsa overview is a useful reference for the kinds of things you can do with Elsa, which mostly break down into "define named lambda terms" (using let) and "verify lambda reductions" (using sequences of terms separated by arrows like =b>).

The assignment is in the files:

1. tests/01_bool.lc
2. tests/02_plus.lc
3. tests/03_minus.lc

You can edit these files and then run them in one of two ways:

• (RECOMMENDED) by running stack exec elsa <path> at the command line in the hw0 repository, where <path> is the path to the relevant file listed above (e.g., stack exec elsa tests/01_bool.lc if you are at the top level of the assignment directory).
• by copying them into the elsa online playground and editing them there.

If you want to use Elsa locally, you will need to have first run stack build in the assignment directory to force Elsa to be installed on your system.

If you want to use Elsa online, be sure to copy back the result into the corresponding local file before submitting.

Your functions/programs must compile and run with stack.

All the points will be awarded automatically, by evaluating your functions against a given test suite.

When you run

$ stack test

The output of stack test should include

All N tests passed (...)
OVERALL SCORE = ... / ...

or

K out of N tests failed
OVERALL SCORE = ... / ...

If your output does not have one of the above, your code will receive a zero.

The other lines will give you a readout for each test. You are encouraged to try to understand the testing code, but you will not be graded on this.

REMARK: For problems 1 and 2, when using =d>, you don't need to unfold every definition. It is often easier to keep some definitions folded until their code is needed.

NOTE: DO NOT use the =*> or =~> operators anywhere in your solution for this problem, or you will get 0 points for the assignment.

NOTE: YOU MAY replace =d> with =b> in the last line.

Complete a sequence of =b> (beta-substitution) and =d> (expand one or more definitions) steps needed to reduce NOT FALSE to TRUE. You may also use renaming steps (=a>) if that makes things easier for you.

Complete a sequence of =b> (beta-substitution) and =d> (expand one or more definitions) steps needed to reduce AND FALSE TRUE to FALSE. You may also use renaming steps (=a>) if that makes things easier for you.

Complete a sequence of =b> (beta-substitution) and =d> (expand one or more definitions) steps needed to reduce OR TRUE FALSE to TRUE. You may also use renaming steps (=a>) if that makes things easier for you.

NOTE: DO NOT use the =*> or =~> operators anywhere in your solution for this problem, or you will get 0 points for the assignment.

NOTE: YOU MAY replace =d> with =b> in the last line.

Complete a sequence of =b> (beta-substitution) and =d> (expand one or more definitions) steps needed to reduce INCR ONE to TWO. You may also use renaming steps (=a>) if that makes things easier for you.

Complete a sequence of =b> (beta-substitution) and =d> (expand one or more definitions) steps needed to reduce ADD ONE ZERO to ONE. You may also use renaming steps (=a>) if that makes things easier for you.

Complete a sequence of =b> (beta-substitution) and =d> (expand one or more definitions) steps needed to reduce ADD ONE TWO to THREE. You may also use renaming steps (=a>) if that makes things easier for you.

In this section, you will switch from evaluating lambda calculus expressions to programming in the lambda calculus. You'll write five lambda calculus functions: SKIP1, DECR, SUB, ISZ, and EQL.

NOTE: You only need to write lambda calculus definitions for SKIP1, DECR, SUB, ISZ, and EQL. If you modify any other part of the file you will get 0 points for the assignment.

PRO TIP: To test your definitions incrementally, replace undefined in the definitions of SKIP1, DECR, SUB, ISZ, and EQL with any syntactically valid lambda calculus expression. This should allow Elsa to parse the file so you can get results for the cases you are working on.

The SKIP1 function takes a function f and a pair p where the left-hand item in p indicates whether an application of f has been "skipped" yet, and the right-hand item in p is some lambda calculus expression expr.

SKIP1 returns a pair p', with the following characteristics:

• If the left-hand item of the original pair p is TRUE, indicating that an application of f has already been "skipped", the right-hand side of p' should be f applied to the expression expr.
• If the left-hand item of the original pair p is FALSE, indicating that an application of f has not yet been "skipped", then the right-hand side of p' should just be expr -- in other words, you will skip the application of f to expr.
• The left-hand item of p' indicates whether an application of f has ever been "skipped", either on this call to SKIP1 or on a previous call to SKIP1.

Replace the definition of SKIP1 with a suitable lambda calculus expression (i.e., replace undefined with a suitable term) so that the below reductions are valid.

eval skip1_false :
  SKIP1 INCR (PAIR FALSE ZERO)
  =~> (\b -> b TRUE ZERO)         --  PAIR TRUE ZERO :: No skip yet, so skip application here.

eval skip1_true_zero :
  SKIP1 INCR (PAIR TRUE ZERO)
  =~> (\b -> b TRUE ONE)          -- PAIR TRUE ONE :: Skip happened already, so apply INCR to ZERO

eval skip1_true_one :
  SKIP1 INCR (PAIR TRUE ONE)
  =~> (\b -> b TRUE TWO)          -- PAIR TRUE TWO :: Skip happened already, so apply INCR to ONE

The DECR function decrements a number by one. It takes a natural number n (encoded as a Church numeral) and returns the natural number n-1 (encoded as a Church numeral). If its argument is ZERO, however, it just returns ZERO.

Replace the definition of DECR with a suitable lambda calculus expression (i.e., replace undefined with a suitable term) so that the following reductions are valid:

eval decr_zero :
  DECR ZERO
  =~> ZERO

eval decr_one :
  DECR ONE
  =~> ZERO

eval decr_two :
  DECR TWO
  =~> ONE

The SUB function implements subtraction on natural numbers. It takes two arguments, natural numbers n and m, encoded as Church numerals, and returns the number n-m as a Church numeral. If n-m would be less than 0, then SUB just returns ZERO.

Replace the definition of SUB (subtract) with a suitable lambda calculus expression (i.e., replace undefined with a suitable term) so that the following reductions are valid:

eval sub_two_zero :
  SUB TWO ZERO
  =~> TWO

eval sub_two_one :
  SUB TWO ONE
  =~> ONE

eval sub_two_two :
  SUB TWO TWO
  =~> ZERO

eval sub_two_three :
  SUB ONE TWO
  =~> ZERO

The ISZ function takes a lambda calculus expression expr as its argument, and returns TRUE if expr evaluates to ZERO and FALSE otherwise.

Replace the definition of ISZ (is-equal-to-zero) with a suitable lambda calculus expression (i.e., replace undefined with a suitable term) so that the following reductions are valid:

eval isz_zero :
  ISZ ZERO
  =~> TRUE

eval isz_one :
  ISZ ONE
  =~> FALSE

The EQL function takes two natural numbers n and m encoded as Church numerals, and returns TRUE if n = m and FALSE otherwise.

Replace the definition of EQL (is-equal) with a suitable lambda-term (i.e., replace undefined with a suitable term) so that the following reductions are valid:

eval eq_zero_zero :
  EQL ZERO ZERO
  =~> TRUE

eval eq_zero_one :
  EQL ZERO ONE
  =~> FALSE

eval eq_one_two :
  EQL ONE TWO
  =~> FALSE

eval eq_two_two :
  EQL TWO TWO
  =~> TRUE

eval eq_two_one :
  EQL TWO ONE
  =~> FALSE