From 8f27869bebd69598f5d510994600030223c3ce3c Mon Sep 17 00:00:00 2001 From: Reza Gharibi Date: Thu, 15 Aug 2019 20:44:16 +0430 Subject: [PATCH] Added (practice) label to unlabeled exercises --- src/plfa/part1/Connectives.lagda.md | 6 +++--- src/plfa/part1/Decidable.lagda.md | 4 ++-- src/plfa/part1/Induction.lagda.md | 8 ++++---- src/plfa/part1/Isomorphism.lagda.md | 4 ++-- src/plfa/part1/Lists.lagda.md | 20 ++++++++++---------- src/plfa/part1/Naturals.lagda.md | 6 +++--- src/plfa/part1/Negation.lagda.md | 2 +- src/plfa/part1/Quantifiers.lagda.md | 12 ++++++------ src/plfa/part1/Relations.lagda.md | 10 +++++----- src/plfa/part2/BigStep.lagda.md | 4 ++-- src/plfa/part2/Bisimulation.lagda.md | 8 ++++---- src/plfa/part2/Confluence.lagda.md | 2 +- src/plfa/part2/DeBruijn.lagda.md | 2 +- src/plfa/part2/Lambda.lagda.md | 10 +++++----- src/plfa/part2/More.lagda.md | 2 +- src/plfa/part2/Properties.lagda.md | 12 ++++++------ src/plfa/part2/Untyped.lagda.md | 10 +++++----- src/plfa/part3/Denotational.lagda.md | 2 +- 18 files changed, 62 insertions(+), 62 deletions(-) diff --git a/src/plfa/part1/Connectives.lagda.md b/src/plfa/part1/Connectives.lagda.md index 5b549bb4..9968c87b 100644 --- a/src/plfa/part1/Connectives.lagda.md +++ b/src/plfa/part1/Connectives.lagda.md @@ -431,7 +431,7 @@ Show sum is commutative up to isomorphism. -- Your code goes here ``` -#### Exercise `⊎-assoc` +#### Exercise `⊎-assoc` (practice) Show sum is associative up to isomorphism. @@ -502,7 +502,7 @@ Show empty is the left identity of sums up to isomorphism. -- Your code goes here ``` -#### Exercise `⊥-identityʳ` +#### Exercise `⊥-identityʳ` (practice) Show empty is the right identity of sums up to isomorphism. @@ -742,7 +742,7 @@ distributive law, and explain how it relates to the weak version. ``` -#### Exercise `⊎×-implies-×⊎` +#### Exercise `⊎×-implies-×⊎` (practice) Show that a disjunct of conjuncts implies a conjunct of disjuncts: ``` diff --git a/src/plfa/part1/Decidable.lagda.md b/src/plfa/part1/Decidable.lagda.md index aa19749e..76135a87 100644 --- a/src/plfa/part1/Decidable.lagda.md +++ b/src/plfa/part1/Decidable.lagda.md @@ -303,7 +303,7 @@ postulate -- Your code goes here ``` -#### Exercise `_≡ℕ?_` +#### Exercise `_≡ℕ?_` (practice) Define a function to decide whether two naturals are equal: ``` @@ -535,7 +535,7 @@ indicating that the order of the equations determines which of the first or the second can match. This time the answer is different depending on which matches; but either is equally valid. -#### Exercise `erasure` +#### Exercise `erasure` (practice) Show that erasure relates corresponding boolean and decidable operations: ``` diff --git a/src/plfa/part1/Induction.lagda.md b/src/plfa/part1/Induction.lagda.md index e2c2c557..565ec395 100644 --- a/src/plfa/part1/Induction.lagda.md +++ b/src/plfa/part1/Induction.lagda.md @@ -71,7 +71,7 @@ distributes over another operator. A careful author will often call out these properties---or their lack---for instance by pointing out that a newly introduced operator is associative but not commutative. -#### Exercise `operators` {#operators} +#### Exercise `operators` (practice) {#operators} Give another example of a pair of operators that have an identity and are associative, commutative, and distribute over one another. @@ -900,7 +900,7 @@ for all naturals `m`, `n`, and `p`. ``` -#### Exercise `*-comm` {#times-comm} +#### Exercise `*-comm` (practice) {#times-comm} Show multiplication is commutative, that is, @@ -914,7 +914,7 @@ you will need to formulate and prove suitable lemmas. ``` -#### Exercise `0∸n≡0` {#zero-monus} +#### Exercise `0∸n≡0` (practice) {#zero-monus} Show @@ -927,7 +927,7 @@ for all naturals `n`. Did your proof require induction? ``` -#### Exercise `∸-|-assoc` {#monus-plus-assoc} +#### Exercise `∸-|-assoc` (practice) {#monus-plus-assoc} Show that monus associates with addition, that is, diff --git a/src/plfa/part1/Isomorphism.lagda.md b/src/plfa/part1/Isomorphism.lagda.md index 7e3df932..88c39ae4 100644 --- a/src/plfa/part1/Isomorphism.lagda.md +++ b/src/plfa/part1/Isomorphism.lagda.md @@ -436,7 +436,7 @@ module ≲-Reasoning where open ≲-Reasoning ``` -#### Exercise `≃-implies-≲` +#### Exercise `≃-implies-≲` (practice) Show that every isomorphism implies an embedding. ``` @@ -451,7 +451,7 @@ postulate -- Your code goes here ``` -#### Exercise `_⇔_` {#iff} +#### Exercise `_⇔_` (practice) {#iff} Define equivalence of propositions (also known as "if and only if") as follows: ``` diff --git a/src/plfa/part1/Lists.lagda.md b/src/plfa/part1/Lists.lagda.md index 44fa9b28..b3f5887d 100644 --- a/src/plfa/part1/Lists.lagda.md +++ b/src/plfa/part1/Lists.lagda.md @@ -525,7 +525,7 @@ parameterised on _n_ types will have a map that is parameterised on _n_ functions. -#### Exercise `map-compose` +#### Exercise `map-compose` (practice) Prove that the map of a composition is equal to the composition of two maps: ``` @@ -535,7 +535,7 @@ postulate ``` The last step of the proof requires extensionality. -#### Exercise `map-++-commute` +#### Exercise `map-++-commute` (practice) Prove the following relationship between map and append: ``` @@ -544,7 +544,7 @@ postulate → map f (xs ++ ys) ≡ map f xs ++ map f ys ``` -#### Exercise `map-Tree` +#### Exercise `map-Tree` (practice) Define a type of trees with leaves of type `A` and internal nodes of type `B`: @@ -640,7 +640,7 @@ postulate ``` -#### Exercise `map-is-foldr` +#### Exercise `map-is-foldr` (practice) Show that map can be defined using fold: ``` @@ -650,7 +650,7 @@ postulate ``` This requires extensionality. -#### Exercise `fold-Tree` +#### Exercise `fold-Tree` (practice) Define a suitable fold function for the type of trees given earlier: ``` @@ -663,7 +663,7 @@ postulate -- Your code goes here ``` -#### Exercise `map-is-fold-Tree` +#### Exercise `map-is-fold-Tree` (practice) Demonstrate an analogue of `map-is-foldr` for the type of trees. @@ -781,7 +781,7 @@ foldr-monoid-++ _⊗_ e monoid-⊗ xs ys = ∎ ``` -#### Exercise `foldl` +#### Exercise `foldl` (practice) Define a function `foldl` which is analogous to `foldr`, but where operations associate to the left rather than the right. For example: @@ -794,7 +794,7 @@ operations associate to the left rather than the right. For example: ``` -#### Exercise `foldr-monoid-foldl` +#### Exercise `foldr-monoid-foldl` (practice) Show that if `_⊗_` and `e` form a monoid, then `foldr _⊗_ e` and `foldl _⊗_ e` always compute the same result. @@ -1005,7 +1005,7 @@ for some element of a list. Give their definitions. ``` -#### Exercise `All-∀` +#### Exercise `All-∀` (practice) Show that `All P xs` is isomorphic to `∀ {x} → x ∈ xs → P x`. @@ -1014,7 +1014,7 @@ Show that `All P xs` is isomorphic to `∀ {x} → x ∈ xs → P x`. ``` -#### Exercise `Any-∃` +#### Exercise `Any-∃` (practice) Show that `Any P xs` is isomorphic to `∃[ x ∈ xs ] P x`. diff --git a/src/plfa/part1/Naturals.lagda.md b/src/plfa/part1/Naturals.lagda.md index 3b78adc3..381c5600 100644 --- a/src/plfa/part1/Naturals.lagda.md +++ b/src/plfa/part1/Naturals.lagda.md @@ -76,7 +76,7 @@ after zero; and `2` is shorthand for `suc (suc zero)`, which is the same as `suc 1`, the successor of one; and `3` is shorthand for the successor of two; and so on. -#### Exercise `seven` {#seven} +#### Exercise `seven` (practice) {#seven} Write out `7` in longhand. @@ -426,7 +426,7 @@ is not like testimony in a court which must be weighed to determine whether the witness is trustworthy. Rather, it is ironclad. The other word for evidence, which we will use interchangeably, is _proof_. -#### Exercise `+-example` {#plus-example} +#### Exercise `+-example` (practice) {#plus-example} Compute `3 + 4`, writing out your reasoning as a chain of equations. @@ -487,7 +487,7 @@ Here we have omitted the signature declaring `_ : 2 * 3 ≡ 6`, since it can easily be inferred from the corresponding term. -#### Exercise `*-example` {#times-example} +#### Exercise `*-example` (practice) {#times-example} Compute `3 * 4`, writing out your reasoning as a chain of equations. diff --git a/src/plfa/part1/Negation.lagda.md b/src/plfa/part1/Negation.lagda.md index dcd985b8..53c9400d 100644 --- a/src/plfa/part1/Negation.lagda.md +++ b/src/plfa/part1/Negation.lagda.md @@ -197,7 +197,7 @@ is irreflexive, that is, `n < n` holds for no `n`. ``` -#### Exercise `trichotomy` +#### Exercise `trichotomy` (practice) Show that strict inequality satisfies [trichotomy]({{ site.baseurl }}/Relations/#trichotomy), diff --git a/src/plfa/part1/Quantifiers.lagda.md b/src/plfa/part1/Quantifiers.lagda.md index ecf6b58d..2eeff87b 100644 --- a/src/plfa/part1/Quantifiers.lagda.md +++ b/src/plfa/part1/Quantifiers.lagda.md @@ -92,7 +92,7 @@ postulate Compare this with the result (`→-distrib-×`) in Chapter [Connectives]({{ site.baseurl }}/Connectives/). -#### Exercise `⊎∀-implies-∀⊎` +#### Exercise `⊎∀-implies-∀⊎` (practice) Show that a disjunction of universals implies a universal of disjunctions: ``` @@ -103,7 +103,7 @@ postulate Does the converse hold? If so, prove; if not, explain why. -#### Exercise `∀-×` +#### Exercise `∀-×` (practice) Consider the following type. ``` @@ -244,7 +244,7 @@ postulate ∃[ x ] (B x ⊎ C x) ≃ (∃[ x ] B x) ⊎ (∃[ x ] C x) ``` -#### Exercise `∃×-implies-×∃` +#### Exercise `∃×-implies-×∃` (practice) Show that an existential of conjunctions implies a conjunction of existentials: ``` @@ -254,7 +254,7 @@ postulate ``` Does the converse hold? If so, prove; if not, explain why. -#### Exercise `∃-⊎` +#### Exercise `∃-⊎` (practice) Let `Tri` and `B` be as in Exercise `∀-×`. Show that `∃[ x ] B x` is isomorphic to `B aa ⊎ B bb ⊎ B cc`. @@ -361,7 +361,7 @@ follows by `odd-suc`. This completes the proof in the backward direction. -#### Exercise `∃-even-odd` +#### Exercise `∃-even-odd` (practice) How do the proofs become more difficult if we replace `m * 2` and `1 + m * 2` by `2 * m` and `2 * m + 1`? Rewrite the proofs of `∃-even` and `∃-odd` when @@ -371,7 +371,7 @@ restated in this way. -- Your code goes here ``` -#### Exercise `∃-|-≤` +#### Exercise `∃-|-≤` (practice) Show that `y ≤ z` holds if and only if there exists a `x` such that `x + y ≡ z`. diff --git a/src/plfa/part1/Relations.lagda.md b/src/plfa/part1/Relations.lagda.md index ea7e7617..1cf5c738 100644 --- a/src/plfa/part1/Relations.lagda.md +++ b/src/plfa/part1/Relations.lagda.md @@ -229,7 +229,7 @@ lack---for instance by saying that a newly introduced relation is a partial order but not a total order. -#### Exercise `orderings` {#orderings} +#### Exercise `orderings` (practice) {#orderings} Give an example of a preorder that is not a partial order. @@ -347,7 +347,7 @@ and `suc n ≤ suc m` and must show `suc m ≡ suc n`. The inductive hypothesis `≤-antisym m≤n n≤m` establishes that `m ≡ n`, and our goal follows by congruence. -#### Exercise `≤-antisym-cases` {#leq-antisym-cases} +#### Exercise `≤-antisym-cases` (practice) {#leq-antisym-cases} The above proof omits cases where one argument is `z≤n` and one argument is `s≤s`. Why is it ok to omit them? @@ -593,7 +593,7 @@ Show that strict inequality is transitive. -- Your code goes here ``` -#### Exercise `trichotomy` {#trichotomy} +#### Exercise `trichotomy` (practice) {#trichotomy} Show that strict inequality satisfies a weak version of trichotomy, in the sense that for any `m` and `n` that one of the following holds: @@ -611,7 +611,7 @@ similar to that used for totality. -- Your code goes here ``` -#### Exercise `+-mono-<` {#plus-mono-less} +#### Exercise `+-mono-<` (practice) {#plus-mono-less} Show that addition is monotonic with respect to strict inequality. As with inequality, some additional definitions may be required. @@ -628,7 +628,7 @@ Show that `suc m ≤ n` implies `m < n`, and conversely. -- Your code goes here ``` -#### Exercise `<-trans-revisited` {#less-trans-revisited} +#### Exercise `<-trans-revisited` (practice) {#less-trans-revisited} Give an alternative proof that strict inequality is transitive, using the relation between strict inequality and inequality and diff --git a/src/plfa/part2/BigStep.lagda.md b/src/plfa/part2/BigStep.lagda.md index 9becdb9e..cec7e83f 100644 --- a/src/plfa/part2/BigStep.lagda.md +++ b/src/plfa/part2/BigStep.lagda.md @@ -120,7 +120,7 @@ data _⊢_⇓_ : ∀{Γ} → ClosEnv Γ → (Γ ⊢ ★) → Clos → Set where call-by-value. -#### Exercise `big-step-eg` +#### Exercise `big-step-eg` (practice) Show that `(ƛ ƛ # 1) · ((ƛ # 0 · # 0) · (ƛ # 0 · # 0))` terminates under big-step call-by-name evaluation. @@ -374,7 +374,7 @@ cbn→reduce {M}{Δ}{δ}{N′} M⇓c ⟨ subst (exts σ) N′ , rs ⟩ ``` -#### Exercise `big-alt-implies-multi` +#### Exercise `big-alt-implies-multi` (practice) Formulate an alternative big-step semantics, of the form `M ↓ N`, for call-by-name that uses substitution instead of environments. diff --git a/src/plfa/part2/Bisimulation.lagda.md b/src/plfa/part2/Bisimulation.lagda.md index 29e43080..dfe23bc3 100644 --- a/src/plfa/part2/Bisimulation.lagda.md +++ b/src/plfa/part2/Bisimulation.lagda.md @@ -169,7 +169,7 @@ However, leaving the simulation small let's us focus on the essence. It's a handy technical trick that we can have a large source language, but only bother to include in the simulation the terms of interest. -#### Exercise `_†` +#### Exercise `_†` (practice) Formalise the translation from source to target given in the introduction. Show that `M † ≡ N` implies `M ~ N`, and conversely. @@ -198,7 +198,7 @@ commutes with values. That is, if `M ~ M†` and `M` is a value then It is a straightforward case analysis, where here the only value of interest is a lambda abstraction. -#### Exercise `~val⁻¹` +#### Exercise `~val⁻¹` (practice) Show that this also holds in the reverse direction: if `M ~ M†` and `Value M†` then `Value M`. @@ -456,7 +456,7 @@ In its structure, it looks a little bit like a proof of progress: we have `N [ x := V ] ~ N† [ x := V† ]`. -#### Exercise `sim⁻¹` +#### Exercise `sim⁻¹` (practice) Show that we also have a simulation in the other direction, and hence that we have a bisimulation. @@ -465,7 +465,7 @@ a bisimulation. -- Your code goes here ``` -#### Exercise `products` +#### Exercise `products` (practice) Show that the two formulations of products in Chapter [More]({{ site.baseurl }}/More/) diff --git a/src/plfa/part2/Confluence.lagda.md b/src/plfa/part2/Confluence.lagda.md index 64617bfb..ad1f9489 100644 --- a/src/plfa/part2/Confluence.lagda.md +++ b/src/plfa/part2/Confluence.lagda.md @@ -141,7 +141,7 @@ data _⇛*_ : ∀ {Γ A} → (Γ ⊢ A) → (Γ ⊢ A) → Set where ``` -#### Exercise `par-diamond-eg` +#### Exercise `par-diamond-eg` (practice) Revisit the counter example to the diamond property for reduction by showing that the diamond property holds for parallel reduction in that diff --git a/src/plfa/part2/DeBruijn.lagda.md b/src/plfa/part2/DeBruijn.lagda.md index 444cd841..94747e8f 100644 --- a/src/plfa/part2/DeBruijn.lagda.md +++ b/src/plfa/part2/DeBruijn.lagda.md @@ -966,7 +966,7 @@ Substitution preserves types, and Preservation. We now turn to proving the remaining results from the previous development. -#### Exercise `V¬—→` +#### Exercise `V¬—→` (practice) Following the previous development, show values do not reduce, and its corollary, terms that reduce are not diff --git a/src/plfa/part2/Lambda.lagda.md b/src/plfa/part2/Lambda.lagda.md index 69cfc817..cc506e1f 100644 --- a/src/plfa/part2/Lambda.lagda.md +++ b/src/plfa/part2/Lambda.lagda.md @@ -196,7 +196,7 @@ defined earlier. ``` -#### Exercise `mulᶜ` +#### Exercise `mulᶜ` (practice) Write out the definition of a lambda term that multiplies two natural numbers represented as Church numerals. Your @@ -740,7 +740,7 @@ The three constructors specify, respectively, that `—↠′` includes `—→` and is reflexive and transitive. A good exercise is to show that the two definitions are equivalent (indeed, one embeds in the other). -#### Exercise `—↠≲—↠′` +#### Exercise `—↠≲—↠′` (practice) Show that the first notion of reflexive and transitive closure above embeds into the second. Why are they not isomorphic? @@ -901,7 +901,7 @@ _ = In the next chapter, we will see how to compute such reduction sequences. -#### Exercise `plus-example` +#### Exercise `plus-example` (practice) Write out the reduction sequence demonstrating that one plus one is two. @@ -1002,7 +1002,7 @@ data Context : Set where ``` -#### Exercise `Context-≃` +#### Exercise `Context-≃` (practice) Show that `Context` is isomorphic to `List (Id × Type)`. For instance, the isomorphism relates the context @@ -1381,7 +1381,7 @@ showing that it is well typed. ``` -#### Exercise `mulᶜ-type` +#### Exercise `mulᶜ-type` (practice) Using the term `mulᶜ` you defined earlier, write out the derivation showing that it is well typed. diff --git a/src/plfa/part2/More.lagda.md b/src/plfa/part2/More.lagda.md index f72f058d..82279766 100644 --- a/src/plfa/part2/More.lagda.md +++ b/src/plfa/part2/More.lagda.md @@ -1199,7 +1199,7 @@ _ = ∎ ``` -#### Exercise `More` +#### Exercise `More` (practice) Formalise the remaining constructs defined in this chapter. Make your changes in this file. diff --git a/src/plfa/part2/Properties.lagda.md b/src/plfa/part2/Properties.lagda.md index f86d2a80..4af99aca 100644 --- a/src/plfa/part2/Properties.lagda.md +++ b/src/plfa/part2/Properties.lagda.md @@ -332,7 +332,7 @@ this requires that we match against the lambda expression `L` to determine its bound variable and body, `ƛ x ⇒ N`, so we can show that `L · M` reduces to `N [ x := M ]`. -#### Exercise `Progress-≃` +#### Exercise `Progress-≃` (practice) Show that `Progress M` is isomorphic to `Value M ⊎ ∃[ N ](M —→ N)`. @@ -340,7 +340,7 @@ Show that `Progress M` is isomorphic to `Value M ⊎ ∃[ N ](M —→ N)`. -- Your code goes here ``` -#### Exercise `progress′` +#### Exercise `progress′` (practice) Write out the proof of `progress′` in full, and compare it to the proof of `progress` above. @@ -349,7 +349,7 @@ proof of `progress` above. -- Your code goes here ``` -#### Exercise `value?` +#### Exercise `value?` (practice) Combine `progress` and `—→¬V` to write a program that decides whether a well-typed term is a value: @@ -1276,7 +1276,7 @@ Using the evaluator, confirm that two times two is four. ``` -#### Exercise: `progress-preservation` +#### Exercise: `progress-preservation` (practice) Without peeking at their statements above, write down the progress and preservation theorems for the simply typed lambda-calculus. @@ -1286,7 +1286,7 @@ and preservation theorems for the simply typed lambda-calculus. ``` -#### Exercise `subject_expansion` +#### Exercise `subject_expansion` (practice) We say that `M` _reduces_ to `N` if `M —→ N`, but we can also describe the same situation by saying @@ -1353,7 +1353,7 @@ Milner, who used denotational rather than operational semantics. He introduced `wrong` as the denotation of a term with a type error, and showed _well-typed terms don't go wrong_.) -#### Exercise `stuck` +#### Exercise `stuck` (practice) Give an example of an ill-typed term that does get stuck. diff --git a/src/plfa/part2/Untyped.lagda.md b/src/plfa/part2/Untyped.lagda.md index 65e86718..29ffc8fe 100644 --- a/src/plfa/part2/Untyped.lagda.md +++ b/src/plfa/part2/Untyped.lagda.md @@ -99,7 +99,7 @@ data Type : Set where ★ : Type ``` -#### Exercise (`Type≃⊤`) +#### Exercise (`Type≃⊤`) (practice) Show that `Type` is isomorphic to `⊤`, the unit type. @@ -118,7 +118,7 @@ data Context : Set where ``` We let `Γ` and `Δ` range over contexts. -#### Exercise (`Context≃ℕ`) +#### Exercise (`Context≃ℕ`) (practice) Show that `Context` is isomorphic to `ℕ`. @@ -402,7 +402,7 @@ data _—→_ : ∀ {Γ A} → (Γ ⊢ A) → (Γ ⊢ A) → Set where → ƛ N —→ ƛ N′ ``` -#### Exercise (`variant-1`) +#### Exercise (`variant-1`) (practice) How would the rules change if we want call-by-value where terms normalise completely? Assume that `β` should not permit reduction @@ -412,7 +412,7 @@ unless both terms are in normal form. -- Your code goes here ``` -#### Exercise (`variant-2`) +#### Exercise (`variant-2`) (practice) How would the rules change if we want call-by-value where terms do not reduce underneath lambda? Assume that `β` @@ -738,7 +738,7 @@ Because `` `suc `` is now a defined term rather than primitive, it is no longer the case that `plus · two · two` reduces to `four`, but they do both reduce to the same normal term. -#### Exercise `plus-eval` +#### Exercise `plus-eval` (practice) Use the evaluator to confirm that `plus · two · two` and `four` normalise to the same term. diff --git a/src/plfa/part3/Denotational.lagda.md b/src/plfa/part3/Denotational.lagda.md index f13d912e..e6c687f4 100644 --- a/src/plfa/part3/Denotational.lagda.md +++ b/src/plfa/part3/Denotational.lagda.md @@ -500,7 +500,7 @@ arguments. ↦-elim2 d₁ d₂ lt = ↦-elim d₁ (sub d₂ lt) ``` -#### Exercise `denot-plusᶜ` +#### Exercise `denot-plusᶜ` (practice) What is a denotation for `plusᶜ`? That is, find a value `v` (other than `⊥`) such that `∅ ⊢ plusᶜ ↓ v`. Also, give the proof of `∅ ⊢ plusᶜ ↓ v`