From 8d40127af01105082f6ab9f85d827659c5f6e223 Mon Sep 17 00:00:00 2001 From: citrusmunch <citrusmunch@users.noreply.github.com> Date: Thu, 24 Oct 2019 21:30:59 -0400 Subject: [PATCH 1/9] consistent variable name typo --- src/plfa/part1/Relations.lagda.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/plfa/part1/Relations.lagda.md b/src/plfa/part1/Relations.lagda.md index 2d6b7591..9028fa51 100644 --- a/src/plfa/part1/Relations.lagda.md +++ b/src/plfa/part1/Relations.lagda.md @@ -773,7 +773,7 @@ if it consists of a single zero (representing zero). Show that increment preserves canonical bitstrings: - Can x + Can b ------------ Can (inc b) From 4dd9f2e37e2044dd317b87ff1469ba1510a95809 Mon Sep 17 00:00:00 2001 From: wadler <wadler@inf.ed.ac.uk> Date: Fri, 25 Oct 2019 18:55:14 +0100 Subject: [PATCH 2/9] Assignment 4 --- courses/tspl/2019/tspl2019.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/courses/tspl/2019/tspl2019.md b/courses/tspl/2019/tspl2019.md index 93ffb328..07471588 100644 --- a/courses/tspl/2019/tspl2019.md +++ b/courses/tspl/2019/tspl2019.md @@ -122,7 +122,7 @@ For instructions on how to set up Agda for PLFA see [Getting Started]({{ site.ba * [Assignment 1]({{ site.baseurl }}/TSPL/2019/Assignment1/) cw1 due 4pm Thursday 3 October (Week 3) * [Assignment 2]({{ site.baseurl }}/TSPL/2019/Assignment2/) cw2 due 4pm Thursday 17 October (Week 5) * [Assignment 3]({{ site.baseurl }}/TSPL/2019/Assignment3/) cw3 due 4pm Thursday 31 October (Week 7) -* Assignment 4 <!-- [Assignment 4]({{ site.baseurl }}/TSPL/2019/Assignment4/) --> cw4 due 4pm Thursday 14 November (Week 9) +* [Assignment 4]({{ site.baseurl }}/TSPL/2019/Assignment4/) cw4 due 4pm Thursday 14 November (Week 9) * Assignment 5 <!-- [Assignment 5]({{ site.baseurl }}/courses/tspl/2010/Mock1.pdf) --> cw5 due 4pm Thursday 21 November (Week 10) <!-- <br /> Use file [Exam]({{ site.baseurl }}/TSPL/2018/Exam/). Despite the rubric, do **all three questions**. --> From 1f624c0b4562f6f2ed578e6a2aaff87d4ec6e37f Mon Sep 17 00:00:00 2001 From: wadler <wadler@inf.ed.ac.uk> Date: Sat, 26 Oct 2019 10:10:40 +0100 Subject: [PATCH 3/9] Update year on Assignment 4 link --- courses/tspl/2019/Assignment4.lagda.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/courses/tspl/2019/Assignment4.lagda.md b/courses/tspl/2019/Assignment4.lagda.md index e1ee7734..81a5b661 100644 --- a/courses/tspl/2019/Assignment4.lagda.md +++ b/courses/tspl/2019/Assignment4.lagda.md @@ -1,7 +1,7 @@ --- title : "Assignment4: TSPL Assignment 4" layout : page -permalink : /TSPL/2018/Assignment4/ +permalink : /TSPL/2019/Assignment4/ --- ``` From 0e1c5d34ea10b0058f93c47f25b539ea03781dc7 Mon Sep 17 00:00:00 2001 From: Pedro Minicz <pedrominicz@gmail.com> Date: Sat, 26 Oct 2019 14:56:56 -0300 Subject: [PATCH 4/9] Fix: make capitalization consistent. --- src/plfa/part1/Lists.lagda.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/plfa/part1/Lists.lagda.md b/src/plfa/part1/Lists.lagda.md index de388e4f..0b013423 100644 --- a/src/plfa/part1/Lists.lagda.md +++ b/src/plfa/part1/Lists.lagda.md @@ -1031,7 +1031,7 @@ decidable, using `_∷_` rather than `⟨_,_⟩` to combine the evidence for the head and tail of the list. -#### Exercise `any?` (stretch) +#### Exercise `Any?` (stretch) Just as `All` has analogues `all` and `All?` which determine whether a predicate holds for every element of a list, so does `Any` have From 6f1933c141f4b5a9bbbaaa30c359324d3f30bd79 Mon Sep 17 00:00:00 2001 From: wadler <wadler@inf.ed.ac.uk> Date: Mon, 28 Oct 2019 11:14:22 +0000 Subject: [PATCH 5/9] minor fix to Inference --- src/plfa/part2/Inference.lagda.md | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/plfa/part2/Inference.lagda.md b/src/plfa/part2/Inference.lagda.md index aabd52ff..cd89e5c4 100644 --- a/src/plfa/part2/Inference.lagda.md +++ b/src/plfa/part2/Inference.lagda.md @@ -584,7 +584,7 @@ ext∋ : ∀ {Γ B x y} ----------------------------- → ¬ ∃[ A ]( Γ , y ⦂ B ∋ x ⦂ A ) ext∋ x≢y _ ⟨ A , Z ⟩ = x≢y refl -ext∋ _ ¬∃ ⟨ A , S _ ⊢x ⟩ = ¬∃ ⟨ A , ⊢x ⟩ +ext∋ _ ¬∃ ⟨ A , S _ ∋x ⟩ = ¬∃ ⟨ A , ∋x ⟩ ``` Given a type `A` and evidence that `Γ , y ⦂ B ∋ x ⦂ A` holds, we must demonstrate a contradiction. If the judgment holds by `Z`, then we @@ -604,7 +604,7 @@ lookup (Γ , y ⦂ B) x with x ≟ y ... | yes refl = yes ⟨ B , Z ⟩ ... | no x≢y with lookup Γ x ... | no ¬∃ = no (ext∋ x≢y ¬∃) -... | yes ⟨ A , ⊢x ⟩ = yes ⟨ A , S x≢y ⊢x ⟩ +... | yes ⟨ A , ∋x ⟩ = yes ⟨ A , S x≢y ∋x ⟩ ``` Consider the context: @@ -1027,7 +1027,7 @@ Next, we give the code to erase a lookup judgment: ``` ∥_∥∋ : ∀ {Γ x A} → Γ ∋ x ⦂ A → ∥ Γ ∥Cx DB.∋ ∥ A ∥Tp ∥ Z ∥∋ = DB.Z -∥ S x≢ ⊢x ∥∋ = DB.S ∥ ⊢x ∥∋ +∥ S x≢ ∋x ∥∋ = DB.S ∥ ∋x ∥∋ ``` It simply drops the evidence that variable names are distinct. From d2ff9564ce40193413d677cc5de7cf814f066067 Mon Sep 17 00:00:00 2001 From: wadler <wadler@inf.ed.ac.uk> Date: Mon, 28 Oct 2019 11:26:49 +0000 Subject: [PATCH 6/9] added midterm survey --- courses/tspl/2019/tspl2019.md | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/courses/tspl/2019/tspl2019.md b/courses/tspl/2019/tspl2019.md index 07471588..911c430b 100644 --- a/courses/tspl/2019/tspl2019.md +++ b/courses/tspl/2019/tspl2019.md @@ -144,6 +144,12 @@ but talk to me if you want to formalise something else. * Optional project cw6 due 4pm Thursday 28 November (Week 11) +## Midterm course feedback + +You may offer feedback on the course at +[https://www.surveymonkey.co.uk/r/YX7ZFYC](https://www.surveymonkey.co.uk/r/YX7ZFYC). +Please do so by 4pm Thursday 31 October. + <!-- From 749e6a9e57e1ecfa5ebb0909043d7fc8f6ce98cd Mon Sep 17 00:00:00 2001 From: wadler <wadler@inf.ed.ac.uk> Date: Mon, 28 Oct 2019 12:00:38 +0000 Subject: [PATCH 7/9] renamed exercises --- courses/tspl/2019/tspl2019.md | 1 + src/plfa/part2/Lambda.lagda.md | 4 ++-- 2 files changed, 3 insertions(+), 2 deletions(-) diff --git a/courses/tspl/2019/tspl2019.md b/courses/tspl/2019/tspl2019.md index 911c430b..598bd318 100644 --- a/courses/tspl/2019/tspl2019.md +++ b/courses/tspl/2019/tspl2019.md @@ -148,6 +148,7 @@ but talk to me if you want to formalise something else. You may offer feedback on the course at [https://www.surveymonkey.co.uk/r/YX7ZFYC](https://www.surveymonkey.co.uk/r/YX7ZFYC). + Please do so by 4pm Thursday 31 October. diff --git a/src/plfa/part2/Lambda.lagda.md b/src/plfa/part2/Lambda.lagda.md index 95ffff8a..bd190f55 100644 --- a/src/plfa/part2/Lambda.lagda.md +++ b/src/plfa/part2/Lambda.lagda.md @@ -1359,7 +1359,7 @@ or explain why there are no such types. 2. `` ∅ , "x" ⦂ A , "y" ⦂ B ⊢ ƛ "z" ⇒ ` "x" · (` "y" · ` "z") ⦂ C `` -#### Exercise `mul-type` (recommended) +#### Exercise `⊢mul` (recommended) Using the term `mul` you defined earlier, write out the derivation showing that it is well typed. @@ -1369,7 +1369,7 @@ showing that it is well typed. ``` -#### Exercise `mulᶜ-type` (practice) +#### Exercise `⊢mulᶜ` (practice) Using the term `mulᶜ` you defined earlier, write out the derivation showing that it is well typed. From 9f0ae6e4b6ee8226191a1e3ea455883030f931d9 Mon Sep 17 00:00:00 2001 From: wadler <wadler@inf.ed.ac.uk> Date: Mon, 28 Oct 2019 15:19:47 +0000 Subject: [PATCH 8/9] fixed exercise in List --- src/plfa/part1/Lists.lagda.md | 19 ++++++++++++++++--- 1 file changed, 16 insertions(+), 3 deletions(-) diff --git a/src/plfa/part1/Lists.lagda.md b/src/plfa/part1/Lists.lagda.md index 0b013423..1f0020d1 100644 --- a/src/plfa/part1/Lists.lagda.md +++ b/src/plfa/part1/Lists.lagda.md @@ -958,11 +958,11 @@ Show that the equivalence `All-++-⇔` can be extended to an isomorphism. -- Your code goes here ``` -#### Exercise `¬Any≃All¬` (recommended) +#### Exercise `¬Any⇔All¬` (recommended) Show that `Any` and `All` satisfy a version of De Morgan's Law: - (¬_ ∘ Any P) xs ≃ All (¬_ ∘ P) xs + (¬_ ∘ Any P) xs ⇔ All (¬_ ∘ P) xs (Can you see why it is important that here `_∘_` is generalised to arbitrary levels, as described in the section on @@ -970,11 +970,24 @@ to arbitrary levels, as described in the section on Do we also have the following? - (¬_ ∘ All P) xs ≃ Any (¬_ ∘ P) xs + (¬_ ∘ All P) xs ⇔ Any (¬_ ∘ P) xs If so, prove; if not, explain why. +``` +-- Your code goes here +``` + +#### Exercise `¬Any≃All¬` (stretch) + +Show that the equivalence `¬Any⇔All¬` can be extended to an isomorphism. +You will need to use extensionality. + +``` +-- Your code goes here +``` + #### Exercise `All-∀` (practice) Show that `All P xs` is isomorphic to `∀ {x} → x ∈ xs → P x`. From c0d9e7851e7a1e17a40811366cc5c74b7ac5f40e Mon Sep 17 00:00:00 2001 From: wadler <wadler@inf.ed.ac.uk> Date: Mon, 28 Oct 2019 16:29:01 +0000 Subject: [PATCH 9/9] Updated exercise in Lists and Assignment3 --- courses/tspl/2019/Assignment3.lagda.md | 23 ++++++++++++++++++++--- 1 file changed, 20 insertions(+), 3 deletions(-) diff --git a/courses/tspl/2019/Assignment3.lagda.md b/courses/tspl/2019/Assignment3.lagda.md index c1782e0b..5e00b72d 100644 --- a/courses/tspl/2019/Assignment3.lagda.md +++ b/courses/tspl/2019/Assignment3.lagda.md @@ -220,6 +220,7 @@ replacement for `_×_`. As a consequence, demonstrate an equivalence relating -- Your code goes here ``` + #### Exercise `All-++-≃` (stretch) Show that the equivalence `All-++-⇔` can be extended to an isomorphism. @@ -228,11 +229,12 @@ Show that the equivalence `All-++-⇔` can be extended to an isomorphism. -- Your code goes here ``` -#### Exercise `¬Any≃All¬` (recommended) + +#### Exercise `¬Any⇔All¬` (recommended) Show that `Any` and `All` satisfy a version of De Morgan's Law: - (¬_ ∘ Any P) xs ≃ All (¬_ ∘ P) xs + (¬_ ∘ Any P) xs ⇔ All (¬_ ∘ P) xs (Can you see why it is important that here `_∘_` is generalised to arbitrary levels, as described in the section on @@ -240,11 +242,26 @@ to arbitrary levels, as described in the section on Do we also have the following? - (¬_ ∘ All P) xs ≃ Any (¬_ ∘ P) xs + (¬_ ∘ All P) xs ⇔ Any (¬_ ∘ P) xs If so, prove; if not, explain why. +``` +-- Your code goes here +``` + + +#### Exercise `¬Any≃All¬` (stretch) + +Show that the equivalence `¬Any⇔All¬` can be extended to an isomorphism. +You will need to use extensionality. + +``` +-- Your code goes here +``` + + #### Exercise `All-∀` (practice) Show that `All P xs` is isomorphic to `∀ {x} → x ∈ xs → P x`.