5 Assignments
Submission instructions are on the Marmoset page. Work is to be done individually. Please avoid excessive collaboration (see the Plagiarism Policy below), and do not look for the answers to assignment questions on the Web or in books.
There are no late submissions for credit unless I have granted you an extension (please ask in a timely fashion, and provide reasons). No solutions will be posted. This is a longstanding policy of mine. I am happy to help you complete assignments (not for credit but for learning) long after the due dates.
In my last on-campus offering (Spring 2017), I did not schedule assignments in advance, but released questions when we had covered the material in lecture. For the intervening online-only offering (Fall 2020), there were no lectures, so I grouped questions into assignments. I have retained that grouping, even though we are back to having lectures.
All Marmoset projects will be available at the start of term. The schedule is generous in that you should be able to work faster (you can get ahead of lectures, since the material is available in LACI), but it gives you some slack to be able to make your own adjustments. If you let the schedule drive your engagement with the course, work will increase towards the end. You should read this whole page early on and work out a tentative schedule for yourself that might have you doing some assignments a little earlier than when they are due. You will not be able to fully judge in advance how long it will take you to read and code, but I have interspersed some suggestions below.
Some questions come with a starter file, which is mostly to save you from having Marmoset reject your work due to silly reasons like spelling mistakes or missing components. The starter files also may contain additional detail about what to submit. As with the Proust files, please ask your browser to download them; don’t cut and paste text from your browser window. Starter files will be available by the start of term.
The weights on assignments total 25.0, so each unit of weight counts for 4% of the final grade. There are also 2.5 units of bonus available, due on the last day of lectures. But, please, don’t obsess over the numbers.
5.1 Propositional Logic
In Spring 2017, the questions equivalent to the first three assignment groups below were due over a ten-day period. Now, as in Fall 2020, it is two weeks, so you should be able to work faster. The reading week break follows, but there is challenging work due right afterwards.
The first three assignment groups are also cumulative, that is, each one builds on the previous one.
5.1.1 Assignment 1 (due Thurs Sep 22)
Weight: 3.0
Reading: into LACI section 2.7 (conjunction)
LACI Exercise 0 (Proust proof, implication). Starter file: A1Q1-starter.rkt
LACI Exercise 1 (Proust programming, conjunction). Starter file: proust-imp-with-holes.rkt. Some further comments in A1Q2-comments.txt
LACI Exercise 2 (Proust proof, conjunction). Starter file: A1Q3-starter.rkt
5.1.2 Assignment 2 (due Thurs Sept 29)
Weight: 2.0
Reading: into LACI section 2.7 (disjunction)
LACI Exercise 3 (Proust programming, disjunction). Starter file: Your solution to A1Q2. Some further comments in A2Q1-comments.txt
LACI Exercise 4 (Proust proof, disjunction). Starter file: A2Q2-starter.rkt
5.1.3 Assignment 3 (due Thurs Oct 6)
Weight: 2.0
Reading: through LACI section 2.7 (negation)
LACI Exercise 5 (Proust programming, negation). Starter file: Your solution to A2Q1. Some further comments in A3Q1-comments.txt
LACI Exercise 6 (Proust proof, negation). Starter file: A3Q2-starter.rkt
5.1.4 Reading week
The reading week break is October 10-14. The next assignment, on Kripke models, was viewed as challenging by the students in Spring 2017. But they had to submit PDFs. This time, as in Fall 2020, I have made the questions more like the Proust material, with construction of a tool to help verify solutions. That, plus Marmoset feedback, should help, but the material is still challenging. I have marked it as optional reading in LACI, but it is required in this course.
5.1.5 Assignment 4 (due Thurs Oct 20)
Weight: 3.0
Reading: through LACI section 2.9 (Kripke models)
LACI Exercise 7 (Racket programming, Kripke models). Starter file: A4Q1-starter.rkt
LACI Exercise 8 (Proof, Kripke models). Starter file: A4Q2-starter.rkt
LACI Exercise 9 (Proust proof, double negation). Starter file: A4Q3-starter.rkt
5.2 Predicate Logic
The predicate logic material was due from one week to three weeks later in Spring 2017 than it is here. It took time to deliver the material in person. I reworked it for Fall 2020 and compressed the schedule. Another reason for the compression is that the next section has been expanded. This might be another place to consider working ahead of the schedule. The programming is only slightly more difficult, but there are more places where changes have to be made, relative to propositional logic.
The two assignment groups here are also cumulative.
5.2.1 Assignment 5 (due Thurs Oct 27)
Weight: 2.0
Reading: through LACI section 3.2.5 (equality and Booleans), including sections 3.2.3 and 3.2.4.
LACI Exercise 10 (Proust proof, equality). Starter file: A5Q1-starter.rkt
LACI Exercise 11 (Proust proof, Booleans). Starter file: A5Q2-starter.rkt
5.2.2 Assignment 6 (due Thurs Nov 3)
Note that LACI Exercise 14 is not required.
Weight: 5.0
Reading: through LACI section 3.2.6 (natural numbers and existentials)
LACI Exercise 12 (Proust programming, natural numbers). Starter file: proust-pred-bool.rkt. Some further comments in A6Q1-comments.txt
LACI Exercise 13 (Proust proof, natural numbers). Starter file: A6Q2-starter.rkt
LACI Exercise 15 (Proust programming, negation and existentials). Starter file: Your solution to A6Q1. Some further comments in A6Q3-comments.txt
LACI Exercise 16 (Proust proof, existentials). Starter file: A6Q4-starter.rkt. Because the solutions are not unique, this question will be handmarked. Marmoset just checks that definitions are provided.
LACI Exercise 17 (Proust proof, existentials and negation). Starter file: A6Q5-starter.rkt
5.3 Proof Assistants
In Fall 2016 and Spring 2017, this section of the course used Coq, which we are not using this term (LACI section 4.3 is optional reading). We will use Agda, as in Fall 2020. I think Agda is easier and more fun to use than Coq, but there may be a significant amount of work in installing the software and getting used to the editor. You should do this as early as possible. Don’t leave it to the last minute.
Coverage of this topic is expanded relative to Spring 2017, and there are some more open-ended bonus questions. Marmoset gives you much less information, and it won’t give you marks. The TAs and I will have to do some marking by hand. However, for most Agda questions, if the compiler accepts it, it is correct. (There are a few exceptions, where the type specification is not sufficient to conclude this.)
The Marmoset tests for Agda files just check that the submission compiles and that the types have not been changed. If your submission is incomplete, the compile will fail, and if you remove a required question from the file, the second check will fail. Try to avoid the second situation. We will check incomplete files by hand to assign part marks.
Working ahead here will let you tackle the bonus material.
5.3.1 Assignment 7 (due Thurs Nov 10)
Weight: 1.0
Reading: through LACI section 4.2.2 (logic in Agda)
To submit: logic.agda with the holes for Exercises 19, 20, 21, 22, 23 filled in.
I strongly recommend Exercise 24 but I am not requiring it, because I want you to have the pleasure of doing it without being required to. Also it is a pain to mark.
5.3.2 Assignment 8 (due Thurs Nov 17)
Weight: 2.0
Reading: through LACI section 4.2.5 (natural numbers in Agda)
To submit: nat.agda with the holes for Exercises 28, 29, 30, 31, 32 filled in. For Exercise 29, you may import the logical connectives and their introduction forms from the standard library.
5.3.3 Assignment 9 (due Thurs Nov 24)
Weight: 1.0
Reading: through LACI section 4.2.6 (more natural numbers in Agda)
To submit: nat.agda with the holes for Exercises 33, 34, 35 filled in.
5.3.4 Assignment 10 (due Thurs Dec 1)
Weight: 2.0
Reading: through LACI section 4.2.7 (sorting in Agda)
To submit: sorting.agda with the holes for Exercises 37, 38, 39, 40 filled in.
5.3.5 Assignment 11 (due Tues Dec 6)
Weight: 2.0
To submit: Exercise 41 from LACI, in the section on Braun trees.
Use the starter file nat-natb.agda and submit with the same file name. You may not change the imports given; besides those, your work should be self-contained.
5.3.6 Bonus (due Tues Dec 6)
Exercise 36 in nat.agda (weight 1.0).
Exercises 43, 44 in braun.agda (weight 1.5).
To submit: bonus.agda, structured as you see fit.
Marking will be subjective. Comments will definitely help.
5.4 Plagiarism Policy
You’ve seen this before but it is no less important than before, so please take the time to read it again. (Also please read the section on Intellectual Property on the Handouts page.)
All work for credit in CS 245E is to be done individually, with the exception of certain assignment questions which may allow a restricted form of collaboration (and will say so explicitly). The penalty for plagiarism is an assigned mark of zero on the assignment or test and a deduction of 5% from the final course grade, consistent with School of Computer Science and Faculty of Mathematics policy. In addition, a letter detailing the offense is sent to the Associate Dean of Undergraduate Studies, meaning that subsequent offenses will carry more severe penalties, up to suspension or expulsion. To avoid inadvertently incurring this penalty, you should discuss assignment issues with other students only in a very broad and high-level fashion, and preferably not at all. Do not take notes during such discussions, and avoid looking at anyone else’s code, on screen or on paper, or showing your code to others. If you find yourself stuck, contact the instructor or teaching assistants for help, instead of getting the solution from someone else. When trying to deal with difficulties, do not consult books or Web sources, unless explicitly authorized to do so.
Senate Undergraduate Council has asked us to post the following paragraphs:
Academic Integrity: In order to maintain a culture of academic integrity, members of the University of Waterloo community are expected to promote honesty, trust, fairness, respect and responsibility.
Grievance: A student who believes that a decision affecting some aspect of his/her university life has been unfair or unreasonable may have grounds for initiating a grievance. Read Policy 70 - Student Petitions and Grievances, Section 4.
Discipline: A student is expected to know what constitutes academic integrity, to avoid committing academic offenses, and to take responsibility for his/her actions. A student who is unsure whether an action constitutes an offense, or who needs help in learning how to avoid offenses (e.g., plagiarism, cheating) or about "rules" for group work/collaboration should seek guidance from the course professor, academic advisor, or the Undergraduate Associate Dean. When misconduct has been found to have occurred, disciplinary penalties will be imposed under Policy 71 - Student Discipline. For information on categories of offenses and types of penalties, students should refer to Policy 71 - Student Discipline.
Avoiding Academic Offenses: Most students are unaware of the line between acceptable and unacceptable academic behaviour, especially when discussing assignments with classmates and using the work of other students. For information on commonly misunderstood academic offenses and how to avoid them, students should refer to the Faculty of Mathematics Cheating and Student Academic Discipline Policy.
Appeals: A student may appeal the finding and/or penalty in a decision made under Policy 70 - Student Petitions and Grievances (other than regarding a petition) or Policy 71 - Student Discipline if a ground for an appeal can be established. Read Policy 72 - Student Appeals.