2 Assignments

Submission instructions are on the Marmoset page. Work is to be done individually. Please avoid excessive collaboration, and do not look for the answers to assignment questions on the Web or in other textbooks. Solutions will not be posted (this is a longstanding policy of mine, which I will be happy to explain to you).

The starting point for each assignment is the "completed" file available on the Handouts page (but also linked here). You must do the exercises with the label "747 exercise". These are a mix of exercises from PLFA (some adapted) and exercises of my own. The exercises labelled "PLFA exercise" alone refer to exercises from PLFA that I have not chosen as assignment questions. Completing these is optional, and your solutions need not be included.

Please do not delete anything from the completed files (including comments). Of course, you can modify the line that includes the hole that is the starting point for your solution. Don’t change the imports unless you have advance permission from me. If you cannot complete an exercise, leave the incomplete solution in your file for possible partial credit. Just make sure that the file compiles (possibly with warnings about "unsolved metas" and "unsolved interaction metas"). Please do not add any pragmas, even if the compiler suggests that you do so. They will interfere with my marking.

In light of the added pressures and complications imposed on all of us by COVID-19, I have relaxed my usual policy of strict deadlines. Please let me know if you need extra time for any assignment.

Repeated Warning: The starter and completed files contain Unicode, which your browser is probably capable of displaying, but may not be configured to do so. Do not cut and paste from your browser. Instead, download the files using Command-click, Control-click, Alt-click, or right-click, depending on your system and browser.

747Naturals.agda (due Jan 12)
Exercises: Exponentiation (1), Increment (1), To/From (2), BinAdd (2).
Total: 6.

747Induction.agda (due Jan 19)
Exercises: AddSwap (1), AddDistMult (2), MultAssoc (2), MultComm (3), LeftMonusZero (1), MonusAssocish (2), DoubleB (1), FromInc (1), FromToB (1), ToFromB (2), DblBInc (1), ToDbl (1), FromDblB (1), BinPlusLInc (2), PlusUnaryBinary (2).
Total: 23.

747Relations.agda (due Jan 26)
Exercises: LTTrans (1), Trichotomy (2), LEtoLTS (1), LEStoLT (1), LTtoSLE (1), LTStoLE (1), OPOE (2). Total: 9.

There are no exercises associated with 747Equality.agda.

747Isomorphism.agda (due Feb 2)
Exercises: IncCanOne (2), OneInc (1), CanToB (1), OneDblbX0 (1), OneToFrom (3), CanToFrom (1), OneUnique (2), CanUnique (1), Rewrap (1), IsoNCanR (2). Total: 15.

Note that the schedule is accelerated a bit over the next two weeks to accommodate the reading week.

747Connectives.agda (due Feb 7)
Exercises: IffIsoIfOnlyIf (1), SumCommIso (1), SumAssocIso (1), EmptyLeftIdIso (1), EmptyRightIdIso (1), SumOfProdImpProdOfSum (1). Total: 6.

747Negation.agda (due Feb 10)
Exercises: NotFourLTThree (1), LTIrrefl (1), LTTrich (3). Total: 5.

747Quantifiers.agda (due Feb 14)
Exercises: ForAllDistProd (1), SumForAllImpForAllSum (1), ExistsDistSum (2), ExistsProdImpProdExists (1), AltLE (3), ExistsNegImpNegForAll (1). Total: 9.

747Decidable.agda (due Feb 17)
Exercises: DecLT (3), DecNatEq (3), ErasBoolDec (3), ErasIFF (3). Total: 12.

747Lists.agda (due Mar 2)
Exercises: RevCommApp (1), RevInvol (1), MapCompose (1), MapAppendDist (1), FoldrOverAppend (1), MapIsFoldr (1), Foldl (1), FoldrMonFoldl (2). Total: 9.

Some of the files below import definitions from earlier files. Those additional definition files can be found on the Handouts page.

747Lambda.agda (due Mar 9)
Exercises: NatMul (1), ChurchMul (1), StepEmbedsIntoStepPrime (2), MulTyped (2), MulCTyped (2). Total: 8.

747Properties.agda (due Mar 16)
Exercises: AltProg (5), ValueEh (1), Unstuck (3). Total: 9.

There are no exercises associated with 747DeBruijn.agda.

747More.agda (due Mar 23)
Exercises: SumsEmpty (10). Total: 10.

747Inference.agda (due Mar 30)
Exercises: NatMul (1), ChurchMul (1), DecideBidirect (5), Decorate (3), ToTerm (2), ontoTerm (3). Total: 15.

There are no exercises associated with 747Untyped.agda.