Proof System Proofs
Due on Thursday, December 4th at 11:59 PM. This is a team lab. You may work alone or you may work with a partner. If you’d like to work with a partner, make sure to indicate your preferred partner using Teammaker and be familiar with the Partner Etiquette guidelines. You may discuss the concepts of this lab with other classmates, but you may not share your code with anyone other than course staff and your lab partner(s). Do not look at solutions written by students other than your team. If your team needs help, please post on Courselore or contact the instructor. If you have any doubts about what is okay and what is not, it’s much safer to ask and learn than to guess!
Overview
For this lab, you will write proofs and counterexamples of properties of proof systems. The first part of the lab relates to operational equivalence; the second part of the lab involves proving language properties. As usual, you will use Teammaker to form your repositories.
Assignment Structure
This is a written assignment. As in the previous assignments, you are required to use LaTeX as well as the proof notation from the textbook. If you have any difficulty with the notation or how to use LaTeX to produce it, please ask your instructor.
Your repository contains a document assignment11.tex which you will build by running make assignment11.pdf. Write your answers in answers.tex, which may be built by running make answers.pdf or simply make. For inline code, please consider using \texttt or \verb. Remember that the source code for the assignment document itself – assignment11.tex – is available for your consideration if you’re not sure how to typeset something. Your instructor is also happy to help with any LaTeX issues you encounter.
Because the textbook does not include instruction on proof system proof techniques, your repository also contains inductionPractice.tex and inductionPracticeAnswers.tex, both of which may be transformed into PDFs via make. The first file contains several simpler practice questions; the second file contains answers for them as well as discussions of those answers. You are strongly encouraged not to read the practice answers before you attempt the practice problems yourself! The function of the practice material is to allow you to work through these challenges with material that you may freely discuss with your instructor or classmates before you approach the graded work.
A word of caution: make sure to observe the Academic Integrity Policy while working on this assignment. You are permitted to discuss the practice problems and answers at length and in detail with anyone you please; you are not permitted to discuss the answers to problems in assignment11.tex with anyone but your instructor and teammate. You are still allowed to discuss the problems at a high level with your other classmates, but please contact your instructor if you’re not sure whether something is okay. As a general rule: never share any content you intend to submit for a grade!
Deliverables
Only the written material in answers.tex will be graded for this assignment. It is your responsibility to ensure that your LaTeX document compiles without error; documents which cannot be compiled cannot be graded.
Submitting
It is not enough to push your work. In your repository, you will find a Python script called submit.py. In order to submit your lab assignment, it should be sufficient to run that script by typing python3 submit.py in your terminal. For this script to work correctly, you must have committed all uncommitted files in your repository and pushed your work so that your repository is in sync with your GitHub remote repository.
The aforementioned Python script is designed to create a Git tag: a name for a specific commit in your repository. (The script also performs a series of checks to help ensure that the tag you create contains what you likely think it contains.) The tag will be named using the words “submission”, the name of your assignment, and a version number. Your instructor will know that you have submitted your work because this tag will appear in your repository. If you need to resubmit your work to correct changes after receiving a grade, you can simply create new commits and then create another tag (preferrably with submit.py). At any given time, only your most recent outstanding submission will be graded.
Lab Questionnaire
In addition to completing the lab itself, you’ll also need to complete a questionnaire describing your experience in the lab. Under most circumstances, this questionnaire will take only about a minute to complete and is part of your participation grade. Please make sure to do this; the information lets me know whether I’m asking for the right amount of work and helps to ensure that it’s a good use of your time.
If You Have Trouble…
…then please contact your instructor! Courselore is the preferred method, but you can reach out via e-mail as well. Good luck!