From cdb753772654d1874ed7606fcda675d7fbe77547 Mon Sep 17 00:00:00 2001 From: Wen Kokke Date: Wed, 24 Dec 2025 15:49:27 +0000 Subject: [PATCH 1/2] Ensure all code blocks are labeled and spaced --- courses/TSPL/2019/Assignment1.lagda.md | 10 +- courses/TSPL/2019/Assignment2.lagda.md | 106 ++++++++----- courses/TSPL/2019/Assignment3.lagda.md | 102 ++++++++----- courses/TSPL/2019/Assignment4.lagda.md | 75 ++++----- courses/TSPL/2019/tspl2019.md | 2 + courses/TSPL/2022/Assignment1.lagda.md | 16 +- courses/TSPL/2022/Assignment2.lagda.md | 43 ++++-- courses/TSPL/2022/Assignment3.lagda.md | 41 +++-- courses/TSPL/2022/Assignment4.lagda.md | 20 +-- courses/TSPL/2022/Eval.lagda.md | 61 +++++--- courses/TSPL/2022/Exam.lagda.md | 5 +- courses/TSPL/2022/tspl.md | 4 + courses/TSPL/2023/Assignment1.lagda.md | 16 +- courses/TSPL/2023/Assignment2.lagda.md | 35 ++++- courses/TSPL/2023/Assignment3.lagda.md | 33 ++-- courses/TSPL/2023/Assignment4.lagda.md | 38 ++++- courses/TSPL/2023/Eval.lagda.md | 61 +++++--- courses/TSPL/2023/Exam.lagda.md | 5 +- courses/TSPL/2023/tspl.md | 6 +- courses/TSPL/2024/Assignment1.lagda.md | 16 +- courses/TSPL/2024/Assignment2.lagda.md | 31 +++- courses/TSPL/2024/Assignment3.lagda.md | 33 ++-- courses/TSPL/2024/Assignment4.lagda.md | 38 ++++- courses/TSPL/2024/tspl.md | 1 + extra/DeMorgan.lagda.md | 2 +- extra/EvalContexts/Lambda.lagda.md | 100 +++++++----- extra/EvalContexts/Properties.lagda.md | 112 +++++++++----- extra/Frames/Lambda.lagda.md | 100 +++++++----- extra/Frames/Properties.lagda.md | 112 +++++++++----- extra/LambdaReduction.lagda.md | 18 +-- extra/Modules.lagda.md | 19 ++- extra/Reflection.lagda.md | 2 +- extra/Subtyping-phil.lagda.md | 12 +- extra/Subtyping.lagda.md | 44 ++++++ extra/bin-suggestion.lagda.md | 3 +- extra/extra/Lists.lagda.md | 2 +- extra/fixpoint-old/LambdaFixpoint.lagda.md | 101 ++++++++----- .../fixpoint-old/PropertiesFixpoint.lagda.md | 143 ++++++++++++------ extra/fixpoint/Lambda.lagda.md | 99 +++++++----- extra/fixpoint/Properties.lagda.md | 143 ++++++++++++------ extra/variants/CEK.lagda.md | 12 +- extra/variants/Evaluation.lagda.md | 69 ++++++--- extra/variants/Frame.lagda.md | 66 +++++--- src/plfa/part1/Connectives.lagda.md | 64 ++++++++ src/plfa/part1/Decidable.lagda.md | 56 +++++++ src/plfa/part1/Equality.lagda.md | 54 +++++++ src/plfa/part1/Induction.lagda.md | 20 ++- src/plfa/part1/Isomorphism.lagda.md | 31 ++++ src/plfa/part1/Lists.lagda.md | 81 ++++++++++ src/plfa/part1/Naturals.lagda.md | 25 +++ src/plfa/part1/Negation.lagda.md | 34 +++++ src/plfa/part1/Quantifiers.lagda.md | 38 ++++- src/plfa/part1/Relations.lagda.md | 48 ++++++ src/plfa/part2/Bisimulation.lagda.md | 16 ++ src/plfa/part2/Confluence.lagda.md | 2 + src/plfa/part2/DeBruijn.lagda.md | 55 ++++++- src/plfa/part2/Inference.lagda.md | 63 +++++++- src/plfa/part2/Lambda.lagda.md | 23 +++ src/plfa/part2/More.lagda.md | 3 + src/plfa/part2/Properties.lagda.md | 51 +++++++ src/plfa/part2/Untyped.lagda.md | 50 +++++- src/plfa/part3/Adequacy.lagda.md | 6 +- src/plfa/part3/Denotational.lagda.md | 2 + src/plfa/part3/Soundness.lagda.md | 2 + .../2019-07-12-migration-to-agda-2-6-0-1.md | 1 + .../2020-07-20-migration-to-agda-2-6-1.md | 2 +- 66 files changed, 2019 insertions(+), 665 deletions(-) diff --git a/courses/TSPL/2019/Assignment1.lagda.md b/courses/TSPL/2019/Assignment1.lagda.md index 73f9a5e78..2b7d85e5e 100644 --- a/courses/TSPL/2019/Assignment1.lagda.md +++ b/courses/TSPL/2019/Assignment1.lagda.md @@ -3,7 +3,7 @@ title : "Assignment1: TSPL Assignment 1" permalink : /TSPL/2019/Assignment1/ --- -``` +```agda module Assignment1 where ``` @@ -19,9 +19,11 @@ You don't need to do all of these, but should attempt at least a few. Exercises labelled "(practice)" are included for those who want extra practice. Submit your homework using the "submit" command. + ```bash submit tspl cw1 Assignment1.lagda.md ``` + Please ensure your files execute correctly under Agda! @@ -43,7 +45,7 @@ yourself, or your group in the case of group practicals). ## Imports -``` +```agda import Relation.Binary.PropositionalEquality as Eq open Eq using (_≡_; refl; cong; sym) open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; step-≡; _∎) @@ -89,12 +91,14 @@ Compute `5 ∸ 3` and `3 ∸ 5`, writing out your reasoning as a chain of equati A more efficient representation of natural numbers uses a binary rather than a unary system. We represent a number as a bitstring. -``` + +```agda data Bin : Set where nil : Bin x0_ : Bin → Bin x1_ : Bin → Bin ``` + For instance, the bitstring 1011 diff --git a/courses/TSPL/2019/Assignment2.lagda.md b/courses/TSPL/2019/Assignment2.lagda.md index 1c6748c7a..472006e95 100644 --- a/courses/TSPL/2019/Assignment2.lagda.md +++ b/courses/TSPL/2019/Assignment2.lagda.md @@ -3,7 +3,7 @@ title : "Assignment2: TSPL Assignment 2" permalink : /TSPL/2019/Assignment2/ --- -``` +```agda module Assignment2 where ``` @@ -19,9 +19,11 @@ You don't need to do all of these, but should attempt at least a few. Exercises labelled "(practice)" are included for those who want extra practice. Submit your homework using the "submit" command. + ```bash submit tspl cw2 Assignment2.lagda.md ``` + Please ensure your files execute correctly under Agda! @@ -41,7 +43,7 @@ yourself, or your group in the case of group practicals). ## Imports -``` +```agda import Relation.Binary.PropositionalEquality as Eq open Eq using (_≡_; refl; cong; sym) open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; step-≡; _∎) @@ -81,7 +83,7 @@ notation for `≡-Reasoning`. Define `≤-Reasoning` analogously, and use it to write out an alternative proof that addition is monotonic with regard to inequality. Rewrite all of `+-monoˡ-≤`, `+-monoʳ-≤`, and `+-mono-≤`. -``` +```agda -- Your code goes here ``` @@ -90,7 +92,9 @@ regard to inequality. Rewrite all of `+-monoˡ-≤`, `+-monoʳ-≤`, and `+-mon #### Exercise `≃-implies-≲` (practice) Show that every isomorphism implies an embedding. -``` + +```agda + postulate ≃-implies-≲ : ∀ {A B : Set} → A ≃ B @@ -98,22 +102,24 @@ postulate → A ≲ B ``` -``` +```agda -- Your code goes here ``` #### Exercise `_⇔_` (practice) {#iff} Define equivalence of propositions (also known as "if and only if") as follows: -``` + +```agda record _⇔_ (A B : Set) : Set where field to : A → B from : B → A ``` + Show that equivalence is reflexive, symmetric, and transitive. -``` +```agda -- Your code goes here ``` @@ -133,7 +139,8 @@ which satisfy the following property: from (to n) ≡ n Using the above, establish that there is an embedding of `ℕ` into `Bin`. -``` + +```agda -- Your code goes here ``` @@ -146,7 +153,7 @@ Why do `to` and `from` not form an isomorphism? Show that `A ⇔ B` as defined [earlier](/Isomorphism/#iff) is isomorphic to `(A → B) × (B → A)`. -``` +```agda -- Your code goes here ``` @@ -154,7 +161,7 @@ is isomorphic to `(A → B) × (B → A)`. Show sum is commutative up to isomorphism. -``` +```agda -- Your code goes here ``` @@ -162,7 +169,7 @@ Show sum is commutative up to isomorphism. Show sum is associative up to isomorphism. -``` +```agda -- Your code goes here ``` @@ -170,7 +177,7 @@ Show sum is associative up to isomorphism. Show empty is the left identity of sums up to isomorphism. -``` +```agda -- Your code goes here ``` @@ -178,21 +185,23 @@ Show empty is the left identity of sums up to isomorphism. Show empty is the right identity of sums up to isomorphism. -``` +```agda -- Your code goes here ``` #### Exercise `⊎-weak-×` (recommended) Show that the following property holds: -``` + +```agda postulate ⊎-weak-× : ∀ {A B C : Set} → (A ⊎ B) × C → A ⊎ (B × C) ``` + This is called a _weak distributive law_. Give the corresponding distributive law, and explain how it relates to the weak version. -``` +```agda -- Your code goes here ``` @@ -200,13 +209,15 @@ distributive law, and explain how it relates to the weak version. #### Exercise `⊎×-implies-×⊎` (practice) Show that a disjunct of conjuncts implies a conjunct of disjuncts: -``` + +```agda postulate ⊎×-implies-×⊎ : ∀ {A B C D : Set} → (A × B) ⊎ (C × D) → (A ⊎ C) × (B ⊎ D) ``` + Does the converse hold? If so, prove; if not, give a counterexample. -``` +```agda -- Your code goes here ``` @@ -218,7 +229,7 @@ Using negation, show that [strict inequality](/Relations/#strict-inequality) is irreflexive, that is, `n < n` holds for no `n`. -``` +```agda -- Your code goes here ``` @@ -236,7 +247,7 @@ that is, for any naturals `m` and `n` exactly one of the following holds: Here "exactly one" means that not only one of the three must hold, but that when one holds the negation of the other two must also hold. -``` +```agda -- Your code goes here ``` @@ -249,7 +260,7 @@ version of De Morgan's Law. This result is an easy consequence of something we've proved previously. -``` +```agda -- Your code goes here ``` @@ -273,7 +284,7 @@ Consider the following principles: Show that each of these implies all the others. -``` +```agda -- Your code goes here ``` @@ -281,14 +292,16 @@ Show that each of these implies all the others. #### Exercise `Stable` (stretch) Say that a formula is _stable_ if double negation elimination holds for it: -``` + +```agda Stable : Set → Set Stable A = ¬ ¬ A → A ``` + Show that any negated formula is stable, and that the conjunction of two stable formulas is stable. -``` +```agda -- Your code goes here ``` @@ -298,11 +311,13 @@ of two stable formulas is stable. #### Exercise `∀-distrib-×` (recommended) Show that universals distribute over conjunction: -``` + +```agda postulate ∀-distrib-× : ∀ {A : Set} {B C : A → Set} → (∀ (x : A) → B x × C x) ≃ (∀ (x : A) → B x) × (∀ (x : A) → C x) ``` + Compare this with the result (`→-distrib-×`) in Chapter [Connectives](/Connectives/). @@ -310,23 +325,27 @@ Chapter [Connectives](/Connectives/). #### Exercise `⊎∀-implies-∀⊎` (practice) Show that a disjunction of universals implies a universal of disjunctions: -``` + +```agda postulate ⊎∀-implies-∀⊎ : ∀ {A : Set} {B C : A → Set} → (∀ (x : A) → B x) ⊎ (∀ (x : A) → C x) → ∀ (x : A) → B x ⊎ C x ``` + Does the converse hold? If so, prove; if not, explain why. #### Exercise `∀-×` (practice) Consider the following type. -``` + +```agda data Tri : Set where aa : Tri bb : Tri cc : Tri ``` + Let `B` be a type indexed by `Tri`, that is `B : Tri → Set`. Show that `∀ (x : Tri) → B x` is isomorphic to `B aa × B bb × B cc`. @@ -334,7 +353,8 @@ Show that `∀ (x : Tri) → B x` is isomorphic to `B aa × B bb × B cc`. #### Exercise `∃-distrib-⊎` (recommended) Show that existentials distribute over disjunction: -``` + +```agda postulate ∃-distrib-⊎ : ∀ {A : Set} {B C : A → Set} → ∃[ x ] (B x ⊎ C x) ≃ (∃[ x ] B x) ⊎ (∃[ x ] C x) @@ -344,11 +364,13 @@ postulate #### Exercise `∃×-implies-×∃` (practice) Show that an existential of conjunctions implies a conjunction of existentials: -``` + +```agda postulate ∃×-implies-×∃ : ∀ {A : Set} {B C : A → Set} → ∃[ x ] (B x × C x) → (∃[ x ] B x) × (∃[ x ] C x) ``` + Does the converse hold? If so, prove; if not, explain why. @@ -364,7 +386,7 @@ 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 restated in this way. -``` +```agda -- Your code goes here ``` @@ -373,7 +395,7 @@ restated in this way. Show that `y ≤ z` holds if and only if there exists a `x` such that `x + y ≡ z`. -``` +```agda -- Your code goes here ``` @@ -381,13 +403,15 @@ Show that `y ≤ z` holds if and only if there exists a `x` such that #### Exercise `∃¬-implies-¬∀` (recommended) Show that existential of a negation implies negation of a universal: -``` + +```agda postulate ∃¬-implies-¬∀ : ∀ {A : Set} {B : A → Set} → ∃[ x ] (¬ B x) -------------- → ¬ (∀ x → B x) ``` + Does the converse hold? If so, prove; if not, explain why. @@ -418,7 +442,7 @@ And to establish the following properties: Using the above, establish that there is an isomorphism between `ℕ` and `∃[ b ](Can b)`. -``` +```agda -- Your code goes here ``` @@ -428,24 +452,26 @@ Using the above, establish that there is an isomorphism between `ℕ` and #### Exercise `__ infix 6 [_]·_ infix 6 _·[_] @@ -285,7 +290,8 @@ data _⊢_==>_ (Γ : Context) (C : Type) : Type → Set where ``` The plug function inserts an expression into the hole of a frame. -``` + +```agda _⟦_⟧ : ∀{Γ A B} → Γ ⊢ A ==> B → Γ ⊢ A @@ -300,7 +306,7 @@ _⟦_⟧ : ∀{Γ A B} ## Reduction -``` +```agda infix 2 _↦_ _—→_ data _↦_ : ∀ {Γ A} → (Γ ⊢ A) → (Γ ⊢ A) → Set where @@ -337,13 +343,14 @@ data _—→_ : ∀ {Γ A} → (Γ ⊢ A) → (Γ ⊢ A) → Set where ``` Notation -``` + +```agda pattern ξ E M—→N = ξξ E refl refl M—→N ``` ## Reflexive and transitive closure of reduction -``` +```agda infix 1 begin_ infix 2 _—↠_ infixr 2 _—→⟨_⟩_ @@ -369,7 +376,8 @@ begin M—↠N = M—↠N Values are irreducible. The auxiliary definition rearranges the order of the arguments because it works better for Agda. -``` + +```agda value-irreducible : ∀ {Γ A} {V M : Γ ⊢ A} → Value V ---------- @@ -388,7 +396,7 @@ value-irreducible v V—→M = nope V—→M v nope (ξ `suc[ E ] V↦M) (`suc v) = nope (ξ E V↦M) v ``` -``` +```agda redex : ∀{Γ A} (M : Γ ⊢ A) → Set redex M = ∃[ N ] (M ↦ N) ``` @@ -398,7 +406,7 @@ redex M = ∃[ N ] (M ↦ N) Every term that is well typed and closed is either blame or a value or takes a reduction step. -``` +```agda data Progress {A} (M : ∅ ⊢ A) : Set where step : ∀ {N : ∅ ⊢ A} @@ -435,15 +443,18 @@ progress (μ M) = step (ξ □ β-μ) ## Evaluation Gas is specified by a natural number: -``` + +```agda record Gas : Set where constructor gas field amount : ℕ ``` + When our evaluator returns a term `N`, it will either give evidence that `N` is a value, or indicate that it ran out of gas. -``` + +```agda data Finished {A} : (∅ ⊢ A) → Set where done : ∀ {N : ∅ ⊢ A} @@ -455,10 +466,12 @@ data Finished {A} : (∅ ⊢ A) → Set where ---------- → Finished N ``` + Given a term `L` of type `A`, the evaluator will, for some `N`, return a reduction sequence from `L` to `N` and an indication of whether reduction finished: -``` + +```agda data Steps {A} : ∅ ⊢ A → Set where steps : {L N : ∅ ⊢ A} @@ -467,8 +480,10 @@ data Steps {A} : ∅ ⊢ A → Set where ---------- → Steps L ``` + The evaluator takes gas and a term and returns the corresponding steps: -``` + +```agda eval : ∀ {A} → Gas → (L : ∅ ⊢ A) @@ -484,7 +499,7 @@ eval (gas (suc m)) L with progress L ## Examples -``` +```agda _ : 2+2 —↠ `suc `suc `suc `suc `zero _ = begin diff --git a/courses/TSPL/2022/Exam.lagda.md b/courses/TSPL/2022/Exam.lagda.md index 09a0f16a5..9bc60243d 100644 --- a/courses/TSPL/2022/Exam.lagda.md +++ b/courses/TSPL/2022/Exam.lagda.md @@ -735,7 +735,8 @@ module Problem3 where ``` A smart constructor, to make it easier to access a variable. -``` + +```agda S′ : ∀ {Γ x y A B} → {x≢y : False (x ≟ y)} → Γ ∋ x ⦂ A @@ -746,6 +747,7 @@ A smart constructor, to make it easier to access a variable. ``` Here is the result of typing two plus two on naturals: + ```agda ⊢2+2 : ∅ ⊢ 2+2 ↑ `ℕ ⊢2+2 = @@ -769,6 +771,7 @@ Here is the result of typing two plus two on naturals: We confirm that synthesis on the relevant term returns natural as the type and the above derivation: + ```agda _ : synthesize ∅ 2+2 ≡ yes ⟨ `ℕ , ⊢2+2 ⟩ _ = refl diff --git a/courses/TSPL/2022/tspl.md b/courses/TSPL/2022/tspl.md index 1b22dba64..3f8551e18 100644 --- a/courses/TSPL/2022/tspl.md +++ b/courses/TSPL/2022/tspl.md @@ -152,9 +152,11 @@ Instructions to do so are [here](https://help.gradescope.com/article/lcn4nfvcww- @@ -171,9 +173,11 @@ Talk to me about what you would like to submit. ## Mock exam diff --git a/courses/TSPL/2023/Assignment1.lagda.md b/courses/TSPL/2023/Assignment1.lagda.md index 54d052631..7107fb0a9 100644 --- a/courses/TSPL/2023/Assignment1.lagda.md +++ b/courses/TSPL/2023/Assignment1.lagda.md @@ -3,7 +3,7 @@ title : "Assignment1: TSPL Assignment 1" permalink : /TSPL/2023/Assignment1/ --- -``` +```agda module Assignment1 where ``` @@ -40,7 +40,7 @@ yourself, or your group in the case of group practicals). ## Naturals -``` +```agda module Naturals where import Relation.Binary.PropositionalEquality as Eq open Eq using (_≡_; refl) @@ -107,12 +107,14 @@ Compute `5 ∸ 3` and `3 ∸ 5`, writing out your reasoning as a chain of equati A more efficient representation of natural numbers uses a binary rather than a unary system. We represent a number as a bitstring: + ```agda data Bin : Set where ⟨⟩ : Bin _O : Bin → Bin _I : Bin → Bin ``` + For instance, the bitstring 1011 @@ -156,7 +158,7 @@ Confirm that these both give the correct answer for zero through four. ## Induction -``` +```agda module Induction where ``` @@ -165,6 +167,7 @@ module Induction where We require equality as in the previous chapter, plus the naturals and some operations upon them. We also require a couple of new operations, `cong`, `sym`, and `_≡⟨_⟩_`, which are explained below: + ```agda import Relation.Binary.PropositionalEquality as Eq open Eq using (_≡_; refl; cong; sym) @@ -172,10 +175,11 @@ and some operations upon them. We also require a couple of new operations, open import Data.Nat using (ℕ; zero; suc; _+_; _*_; _∸_) open import Data.Nat.Properties using (+-assoc; +-identityʳ; +-suc; +-comm) ``` + (Importing `step-≡` defines `_≡⟨_⟩_`.) -``` +```agda open import plfa.part1.Induction hiding () ``` @@ -292,7 +296,7 @@ Show the following three laws for all `m`, `n`, and `p`. -``` +```agda -- Your code goes here ``` @@ -325,7 +329,7 @@ For each law: if it holds, prove; if not, give a counterexample. ## Relations -``` +```agda module Relations where ``` diff --git a/courses/TSPL/2023/Assignment2.lagda.md b/courses/TSPL/2023/Assignment2.lagda.md index 7adca3514..1eab2c252 100644 --- a/courses/TSPL/2023/Assignment2.lagda.md +++ b/courses/TSPL/2023/Assignment2.lagda.md @@ -3,7 +3,7 @@ title : "Assignment2: TSPL Assignment 2" permalink : /TSPL/2023/Assignment2/ --- -``` +```agda module Assignment2 where ``` @@ -39,7 +39,7 @@ yourself, or your group in the case of group practicals). ## Connectives -``` +```agda module Connectives where ``` @@ -56,7 +56,7 @@ module Connectives where ``` -``` +```agda open import plfa.part1.Connectives hiding (⊎-weak-×; ⊎×-implies-×⊎) ``` @@ -106,10 +106,12 @@ Show empty is the right identity of sums up to isomorphism. #### Exercise `⊎-weak-×` (recommended) Show that the following property holds: + ```agda postulate ⊎-weak-× : ∀ {A B C : Set} → (A ⊎ B) × C → A ⊎ (B × C) ``` + This is called a _weak distributive law_. Give the corresponding distributive law, and explain how it relates to the weak version. @@ -121,10 +123,12 @@ distributive law, and explain how it relates to the weak version. #### Exercise `⊎×-implies-×⊎` (practice) Show that a disjunct of conjuncts implies a conjunct of disjuncts: + ```agda postulate ⊎×-implies-×⊎ : ∀ {A B C D : Set} → (A × B) ⊎ (C × D) → (A ⊎ C) × (B ⊎ D) ``` + Does the converse hold? If so, prove; if not, give a counterexample. ```agda @@ -135,7 +139,7 @@ Does the converse hold? If so, prove; if not, give a counterexample. ## Negation -``` +```agda module Negation where ``` @@ -219,10 +223,12 @@ Show that each of these implies all the others. #### Exercise `Stable` (stretch) Say that a formula is _stable_ if double negation elimination holds for it: + ```agda Stable : Set → Set Stable A = ¬ ¬ A → A ``` + Show that any negated formula is stable, and that the conjunction of two stable formulas is stable. @@ -233,7 +239,7 @@ of two stable formulas is stable. ## Quantifiers -``` +```agda module Quantifiers where ``` @@ -255,11 +261,13 @@ module Quantifiers where #### Exercise `∀-distrib-×` (recommended) Show that universals distribute over conjunction: + ```agda postulate ∀-distrib-× : ∀ {A : Set} {B C : A → Set} → (∀ (x : A) → B x × C x) ≃ (∀ (x : A) → B x) × (∀ (x : A) → C x) ``` + Compare this with the result (`→-distrib-×`) in Chapter [Connectives](/Connectives/). @@ -268,23 +276,27 @@ Hint: you will need to use [`∀-extensionality`](/Isomorphism/#extensionality). #### Exercise `⊎∀-implies-∀⊎` (practice) Show that a disjunction of universals implies a universal of disjunctions: + ```agda postulate ⊎∀-implies-∀⊎ : ∀ {A : Set} {B C : A → Set} → (∀ (x : A) → B x) ⊎ (∀ (x : A) → C x) → ∀ (x : A) → B x ⊎ C x ``` + Does the converse hold? If so, prove; if not, explain why. #### Exercise `∀-×` (practice) Consider the following type. + ```agda data Tri : Set where aa : Tri bb : Tri cc : Tri ``` + Let `B` be a type indexed by `Tri`, that is `B : Tri → Set`. Show that `∀ (x : Tri) → B x` is isomorphic to `B aa × B bb × B cc`. @@ -294,6 +306,7 @@ Hint: you will need to use [`∀-extensionality`](/Isomorphism/#extensionality). #### Exercise `∃-distrib-⊎` (recommended) Show that existentials distribute over disjunction: + ```agda postulate ∃-distrib-⊎ : ∀ {A : Set} {B C : A → Set} → @@ -303,11 +316,13 @@ Show that existentials distribute over disjunction: #### Exercise `∃×-implies-×∃` (practice) Show that an existential of conjunctions implies a conjunction of existentials: + ```agda postulate ∃×-implies-×∃ : ∀ {A : Set} {B C : A → Set} → ∃[ x ] (B x × C x) → (∃[ x ] B x) × (∃[ x ] C x) ``` + Does the converse hold? If so, prove; if not, explain why. #### Exercise `∃-⊎` (practice) @@ -339,6 +354,7 @@ Show that `y ≤ z` holds if and only if there exists a `x` such that #### Exercise `∃¬-implies-¬∀` (recommended) Show that existential of a negation implies negation of a universal: + ```agda postulate ∃¬-implies-¬∀ : ∀ {A : Set} {B : A → Set} @@ -346,6 +362,7 @@ Show that existential of a negation implies negation of a universal: -------------- → ¬ (∀ x → B x) ``` + Does the converse hold? If so, prove; if not, explain why. @@ -398,7 +415,7 @@ which is a corollary of `≡Can`. ## Decidable -``` +```agda module Decidable where ``` @@ -420,7 +437,7 @@ module Decidable where open import plfa.part1.Isomorphism using (_⇔_) ``` -``` +```agda open import plfa.part1.Decidable hiding (__ infix 6 [_]·_ infix 6 _·[_] @@ -285,7 +290,8 @@ data _⊢_==>_ (Γ : Context) (C : Type) : Type → Set where ``` The plug function inserts an expression into the hole of a frame. -``` + +```agda _⟦_⟧ : ∀{Γ A B} → Γ ⊢ A ==> B → Γ ⊢ A @@ -300,7 +306,7 @@ _⟦_⟧ : ∀{Γ A B} ## Reduction -``` +```agda infix 2 _↦_ _—→_ data _↦_ : ∀ {Γ A} → (Γ ⊢ A) → (Γ ⊢ A) → Set where @@ -337,13 +343,14 @@ data _—→_ : ∀ {Γ A} → (Γ ⊢ A) → (Γ ⊢ A) → Set where ``` Notation -``` + +```agda pattern ξ E M—→N = ξξ E refl refl M—→N ``` ## Reflexive and transitive closure of reduction -``` +```agda infix 1 begin_ infix 2 _—↠_ infixr 2 _—→⟨_⟩_ @@ -369,7 +376,8 @@ begin M—↠N = M—↠N Values are irreducible. The auxiliary definition rearranges the order of the arguments because it works better for Agda. -``` + +```agda value-irreducible : ∀ {Γ A} {V M : Γ ⊢ A} → Value V ---------- @@ -388,7 +396,7 @@ value-irreducible v V—→M = nope V—→M v nope (ξ `suc[ E ] V↦M) (`suc v) = nope (ξ E V↦M) v ``` -``` +```agda redex : ∀{Γ A} (M : Γ ⊢ A) → Set redex M = ∃[ N ] (M ↦ N) ``` @@ -398,7 +406,7 @@ redex M = ∃[ N ] (M ↦ N) Every term that is well typed and closed is either blame or a value or takes a reduction step. -``` +```agda data Progress {A} (M : ∅ ⊢ A) : Set where step : ∀ {N : ∅ ⊢ A} @@ -435,15 +443,18 @@ progress (μ M) = step (ξ □ β-μ) ## Evaluation Gas is specified by a natural number: -``` + +```agda record Gas : Set where constructor gas field amount : ℕ ``` + When our evaluator returns a term `N`, it will either give evidence that `N` is a value, or indicate that it ran out of gas. -``` + +```agda data Finished {A} : (∅ ⊢ A) → Set where done : ∀ {N : ∅ ⊢ A} @@ -455,10 +466,12 @@ data Finished {A} : (∅ ⊢ A) → Set where ---------- → Finished N ``` + Given a term `L` of type `A`, the evaluator will, for some `N`, return a reduction sequence from `L` to `N` and an indication of whether reduction finished: -``` + +```agda data Steps {A} : ∅ ⊢ A → Set where steps : {L N : ∅ ⊢ A} @@ -467,8 +480,10 @@ data Steps {A} : ∅ ⊢ A → Set where ---------- → Steps L ``` + The evaluator takes gas and a term and returns the corresponding steps: -``` + +```agda eval : ∀ {A} → Gas → (L : ∅ ⊢ A) @@ -484,7 +499,7 @@ eval (gas (suc m)) L with progress L ## Examples -``` +```agda _ : 2+2 —↠ `suc `suc `suc `suc `zero _ = begin diff --git a/courses/TSPL/2023/Exam.lagda.md b/courses/TSPL/2023/Exam.lagda.md index d85c577d4..30af9fbd5 100644 --- a/courses/TSPL/2023/Exam.lagda.md +++ b/courses/TSPL/2023/Exam.lagda.md @@ -737,7 +737,8 @@ module Problem3 where ``` A smart constructor, to make it easier to access a variable. -``` + +```agda S′ : ∀ {Γ x y A B} → {x≢y : False (x ≟ y)} → Γ ∋ x ⦂ A @@ -748,6 +749,7 @@ A smart constructor, to make it easier to access a variable. ``` Here is the result of typing two plus two on naturals: + ```agda ⊢2+2 : ∅ ⊢ 2+2 ↑ `ℕ ⊢2+2 = @@ -771,6 +773,7 @@ Here is the result of typing two plus two on naturals: We confirm that synthesis on the relevant term returns natural as the type and the above derivation: + ```agda _ : synthesize ∅ 2+2 ≡ yes ⟨ `ℕ , ⊢2+2 ⟩ _ = refl diff --git a/courses/TSPL/2023/tspl.md b/courses/TSPL/2023/tspl.md index 6fe3ab517..cecd5941b 100644 --- a/courses/TSPL/2023/tspl.md +++ b/courses/TSPL/2023/tspl.md @@ -159,9 +159,11 @@ or Bitbucket if you have not already. Instructions to do so are @@ -178,9 +180,11 @@ Talk to me about what you would like to submit. diff --git a/extra/DeMorgan.lagda.md b/extra/DeMorgan.lagda.md index 33f9aeb02..dd792aa94 100644 --- a/extra/DeMorgan.lagda.md +++ b/extra/DeMorgan.lagda.md @@ -1,4 +1,4 @@ -``` +```agda module DeMorgan where open import Relation.Binary.PropositionalEquality using (_≡_; refl) diff --git a/extra/EvalContexts/Lambda.lagda.md b/extra/EvalContexts/Lambda.lagda.md index f4d9f7191..b24ad32e3 100644 --- a/extra/EvalContexts/Lambda.lagda.md +++ b/extra/EvalContexts/Lambda.lagda.md @@ -3,7 +3,7 @@ title : "Lambda: Introduction to Lambda Calculus" permalink : /Lambda/ --- -``` +```agda module Lambda where ``` @@ -49,7 +49,7 @@ four. ## Imports -``` +```agda open import Data.Bool using (T; not) open import Data.Empty using (⊥; ⊥-elim) open import Data.List using (List; _∷_; []) @@ -98,7 +98,8 @@ Here is the syntax of terms in Backus-Naur Form (BNF): μ x ⇒ M And here it is formalised in Agda: -``` + +```agda Id : Set Id = String @@ -117,6 +118,7 @@ data Term : Set where case_[zero⇒_|suc_⇒_] : Term → Term → Id → Term → Term μ_⇒_ : Id → Term → Term ``` + We represent identifiers by strings. We choose precedence so that lambda abstraction and fixpoint bind least tightly, then application, then successor, and tightest of all is the constructor for variables. @@ -128,7 +130,8 @@ Case expressions are self-bracketing. Here are some example terms: the natural number two, a function that adds naturals, and a term that computes two plus two: -``` + +```agda two : Term two = `suc `suc `zero @@ -138,6 +141,7 @@ plus = μ "+" ⇒ ƛ "m" ⇒ ƛ "n" ⇒ [zero⇒ ` "n" |suc "m" ⇒ `suc (` "+" · ` "m" · ` "n") ] ``` + The recursive definition of addition is similar to our original definition of `_+_` for naturals, as given in Chapter [Naturals](/Naturals/#plus). @@ -159,7 +163,8 @@ second. This is called the _Church representation_ of the naturals. Here are some example terms: the Church numeral two, a function that adds Church numerals, a function to compute successor, and a term that computes two plus two: -``` + +```agda twoᶜ : Term twoᶜ = ƛ "s" ⇒ ƛ "z" ⇒ ` "s" · (` "s" · ` "z") @@ -170,6 +175,7 @@ plusᶜ = ƛ "m" ⇒ ƛ "n" ⇒ ƛ "s" ⇒ ƛ "z" ⇒ sucᶜ : Term sucᶜ = ƛ "n" ⇒ `suc (` "n") ``` + The Church numeral for two takes two arguments `s` and `z` and applies `s` twice to `z`. Addition takes two numerals `m` and `n`, a @@ -193,7 +199,7 @@ Write out the definition of a lambda term that multiplies two natural numbers. Your definition may use `plus` as defined earlier. -``` +```agda -- Your code goes here ``` @@ -205,7 +211,7 @@ two natural numbers represented as Church numerals. Your definition may use `plusᶜ` as defined earlier (or may not — there are nice definitions both ways). -``` +```agda -- Your code goes here ``` @@ -215,7 +221,8 @@ definition may use `plusᶜ` as defined earlier (or may not Some people find it annoying to write `` ` "x" `` instead of `x`. We can make examples with lambda terms slightly easier to write by adding the following definitions: -``` + +```agda ƛ′_⇒_ : Term → Term → Term ƛ′ (` x) ⇒ N = ƛ x ⇒ N ƛ′ _ ⇒ _ = ⊥-elim impossible @@ -231,6 +238,7 @@ case′ _ [zero⇒ _ |suc _ ⇒ _ ] = ⊥-elim impossible μ′ _ ⇒ _ = ⊥-elim impossible where postulate impossible : ⊥ ``` + We intend to apply the function only when the first term is a variable, which we indicate by postulating a term `impossible` of the empty type `⊥`. If we use C-c C-n to normalise the term @@ -246,7 +254,8 @@ used with care, since such postulation could allow us to provide evidence of _any_ proposition whatsoever, regardless of its truth. The definition of `plus` can now be written as follows: -``` + +```agda plus′ : Term plus′ = μ′ + ⇒ ƛ′ m ⇒ ƛ′ n ⇒ case′ m @@ -257,6 +266,7 @@ plus′ = μ′ + ⇒ ƛ′ m ⇒ ƛ′ n ⇒ m = ` "m" n = ` "n" ``` + Write out the definition of multiplication in the same style. @@ -355,7 +365,7 @@ as values; thus, `` plus `` by itself is considered a value. The predicate `Value M` holds if term `M` is a value: -``` +```agda data Value : Term → Set where instance @@ -458,7 +468,7 @@ which will be adequate for our purposes. Here is the formal definition of substitution by closed terms in Agda: -``` +```agda infix 9 _[_:=_] _[_:=_] : Term → Id → Term → Term @@ -501,7 +511,7 @@ simply push substitution recursively into the subterms. Here is confirmation that the examples above are correct: -``` +```agda _ : (ƛ "z" ⇒ ` "s" · (` "s" · ` "z")) [ "s" := sucᶜ ] ≡ ƛ "z" ⇒ sucᶜ · (sucᶜ · ` "z") _ = refl @@ -544,7 +554,7 @@ substitution. ## Evaluation contexts -``` +```agda infix 7 □·_ infix 7 _·□ infix 8 `suc□ @@ -616,7 +626,7 @@ case where we substitute by a term that is not a value. Here are the rules formalised in Agda: -``` +```agda infix 4 _—→_ data _—→_ : Term → Term → Set where @@ -700,7 +710,8 @@ We define reflexive and transitive closure as a sequence of zero or more steps of the underlying relation, along lines similar to that for reasoning about chains of equalities in Chapter [Equality](/Equality/): -``` + +```agda infix 2 _—↠_ infix 1 begin_ infixr 2 _—→⟨_⟩_ @@ -723,6 +734,7 @@ begin_ : ∀ {M N} → M —↠ N begin M—↠N = M—↠N ``` + We can read this as follows: * From term `M`, we can take no steps, giving a step of type `M —↠ M`. @@ -739,7 +751,8 @@ appealing way, as we will see in the next section. An alternative is to define reflexive and transitive closure directly, as the smallest relation that includes `—→` and is also reflexive and transitive. We could do so as follows: -``` + +```agda data _—↠′_ : Term → Term → Set where step′ : ∀ {M N} @@ -757,6 +770,7 @@ data _—↠′_ : Term → Term → Set where ------- → L —↠′ N ``` + 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). @@ -766,7 +780,7 @@ the two definitions are equivalent (indeed, one embeds in the other). Show that the first notion of reflexive and transitive closure above embeds into the second. Why are they not isomorphic? -``` +```agda -- Your code goes here ``` @@ -794,7 +808,7 @@ while if the top two lines stand for a single reduction step and the bottom two stand for zero or more reduction steps it is called the diamond property. In symbols: -``` +```agda postulate confluence : ∀ {L M N} → ((L —↠ M) × (L —↠ N)) @@ -810,7 +824,7 @@ postulate The reduction system studied in this chapter is deterministic. In symbols: -``` +```agda postulate deterministic : ∀ {L M N} → L —→ M @@ -828,7 +842,8 @@ systems studied in this text are trivially confluent. We start with a simple example. The Church numeral two applied to the successor function and zero yields the natural number two: -``` + +```agda _ : twoᶜ · sucᶜ · `zero —↠ `suc `suc `zero _ = begin @@ -845,7 +860,8 @@ _ = ``` Here is a sample reduction demonstrating that two plus two is four: -``` + +```agda _ : plus · two · two —↠ `suc `suc `suc `suc `zero _ = begin @@ -890,7 +906,8 @@ _ = ``` And here is a similar sample reduction for Church numerals: -``` + +```agda _ : plusᶜ · twoᶜ · twoᶜ · sucᶜ · `zero —↠ `suc `suc `suc `suc `zero _ = begin @@ -931,7 +948,7 @@ In the next chapter, we will see how to compute such reduction sequences. Write out the reduction sequence demonstrating that one plus one is two. -``` +```agda -- Your code goes here ``` @@ -951,7 +968,7 @@ Here is the syntax of types in BNF: And here it is formalised in Agda: -``` +```agda infixr 7 _⇒_ data Type : Set where @@ -1019,7 +1036,7 @@ and variable `` "z" `` with type `` `ℕ ``. Contexts are formalised as follows: -``` +```agda infixl 5 _,_⦂_ data Context : Set where @@ -1039,7 +1056,7 @@ to the list [ ⟨ "z" , `ℕ ⟩ , ⟨ "s" , `ℕ ⇒ `ℕ ⟩ ] -``` +```agda -- Your code goes here ``` @@ -1070,7 +1087,8 @@ the other variables. For example, Here `` "x" ⦂ `ℕ ⇒ `ℕ `` is shadowed by `` "x" ⦂ `ℕ ``. Lookup is formalised as follows: -``` + +```agda infix 4 _∋_⦂_ data _∋_⦂_ : Context → Id → Type → Set where @@ -1095,14 +1113,14 @@ variable with the same name to its left in the list. It can be rather tedious to use the `S` constructor, as you have to provide proofs that `x ≢ y` each time. For example: -``` +```agda _ : ∅ , "x" ⦂ `ℕ ⇒ `ℕ , "y" ⦂ `ℕ , "z" ⦂ `ℕ ∋ "x" ⦂ `ℕ ⇒ `ℕ _ = S (λ()) (S (λ()) Z) ``` Instead, we'll use a "smart constructor", which uses [proof by reflection](/Decidable/#proof-by-reflection) to check the inequality while type checking: -``` +```agda S′ : ∀ {Γ x y A B} → {x≢y : False (x ≟ y)} → Γ ∋ x ⦂ A @@ -1130,7 +1148,8 @@ For example: * `` ∅ ⊢ ƛ "s" ⇒ ƛ "z" ⇒ ` "s" · (` "s" · ` "z") ⦂ (`ℕ ⇒ `ℕ) ⇒ `ℕ ⇒ `ℕ `` Typing is formalised as follows: -``` + +```agda infix 4 _⊢_⦂_ data _⊢_⦂_ : Context → Term → Type → Set where @@ -1232,7 +1251,8 @@ The typing derivation is valid for any `Γ` and `A`, for instance, we might take `Γ` to be `∅` and `A` to be `` `ℕ ``. Here is the above typing derivation formalised in Agda: -``` + +```agda Ch : Type → Type Ch A = (A ⇒ A) ⇒ A ⇒ A @@ -1244,7 +1264,8 @@ Ch A = (A ⇒ A) ⇒ A ⇒ A ``` Here are the typings corresponding to computing two plus two: -``` + +```agda ⊢two : ∀ {Γ} → Γ ⊢ two ⦂ `ℕ ⊢two = ⊢suc (⊢suc ⊢zero) @@ -1261,6 +1282,7 @@ Here are the typings corresponding to computing two plus two: ⊢2+2 : ∅ ⊢ plus · two · two ⦂ `ℕ ⊢2+2 = ⊢plus · ⊢two · ⊢two ``` + In contrast to our earlier examples, here we have typed `two` and `plus` in an arbitrary context rather than the empty context; this makes it easy to use them inside other binding contexts as well as at the top level. @@ -1271,7 +1293,8 @@ contexts, the first where `"n"` is the last binding in the context, and the second after `"m"` is bound in the successor branch of the case. And here are typings for the remainder of the Church example: -``` + +```agda ⊢plusᶜ : ∀ {Γ A} → Γ ⊢ plusᶜ ⦂ Ch A ⇒ Ch A ⇒ Ch A ⊢plusᶜ = ⊢ƛ (⊢ƛ (⊢ƛ (⊢ƛ (⊢` ∋m · ⊢` ∋s · (⊢` ∋n · ⊢` ∋s · ⊢` ∋z))))) where @@ -1337,7 +1360,8 @@ will show how to use Agda to compute type derivations directly. The lookup relation `Γ ∋ x ⦂ A` is functional, in that for each `Γ` and `x` there is at most one `A` such that the judgment holds: -``` + +```agda ∋-functional : ∀ {Γ x A B} → Γ ∋ x ⦂ A → Γ ∋ x ⦂ B → A ≡ B ∋-functional Z Z = refl ∋-functional Z (S x≢ _) = ⊥-elim (x≢ refl) @@ -1356,7 +1380,7 @@ a formal proof that it is not possible to type the term requires that the first term in the application is both a natural and a function: -``` +```agda nope₁ : ∀ {A} → ¬ (∅ ⊢ `zero · `suc `zero ⦂ A) nope₁ (() · _) ``` @@ -1365,7 +1389,7 @@ As a second example, here is a formal proof that it is not possible to type `` ƛ "x" ⇒ ` "x" · ` "x" ``. It cannot be typed, because doing so requires types `A` and `B` such that `A ⇒ B ≡ A`: -``` +```agda nope₂ : ∀ {A} → ¬ (∅ ⊢ ƛ "x" ⇒ ` "x" · ` "x" ⦂ A) nope₂ (⊢ƛ (⊢` ∋x · ⊢` ∋x′)) = contradiction (∋-functional ∋x ∋x′) where @@ -1395,7 +1419,7 @@ or explain why there are no such types. Using the term `mul` you defined earlier, write out the derivation showing that it is well typed. -``` +```agda -- Your code goes here ``` @@ -1405,7 +1429,7 @@ showing that it is well typed. Using the term `mulᶜ` you defined earlier, write out the derivation showing that it is well typed. -``` +```agda -- Your code goes here ``` diff --git a/extra/EvalContexts/Properties.lagda.md b/extra/EvalContexts/Properties.lagda.md index 8738b3474..c80a78feb 100644 --- a/extra/EvalContexts/Properties.lagda.md +++ b/extra/EvalContexts/Properties.lagda.md @@ -3,7 +3,7 @@ title : "Properties: Progress and Preservation" permalink : /Properties/ --- -``` +```agda module EvalContexts.Properties where ``` @@ -16,7 +16,7 @@ sequences for us. ## Imports -``` +```agda open import Relation.Binary.PropositionalEquality using (_≡_; _≢_; refl; sym; cong; cong₂) open import Data.String using (String; _≟_) @@ -106,7 +106,8 @@ that `M —→ N`. To formulate this property, we first introduce a relation that captures what it means for a term `M` to make progress: -``` + +```agda data Progress (M : Term) : Set where step : ∀ {N} @@ -119,12 +120,14 @@ data Progress (M : Term) : Set where ---------- → Progress M ``` + A term `M` makes progress if either it can take a step, meaning there exists a term `N` such that `M —→ N`, or if it is done, meaning that `M` is a value. If a term is well typed in the empty context then it satisfies progress: -``` + +```agda progress : ∀ {M A} → ∅ ⊢ M ⦂ A ---------- @@ -146,6 +149,7 @@ progress (⊢case ⊢L ⊢M ⊢N) with progress ⊢L ... | done {{V-suc}} = step (ξ [] β-suc) progress (⊢μ ⊢M) = step (ξ [] β-μ) ``` + We induct on the evidence that the term is well typed. Let's unpack the first three cases: @@ -191,10 +195,12 @@ or introduce subsidiary functions. Instead of defining a data type for `Progress M`, we could have formulated progress using disjunction and existentials: -``` + +```agda postulate progress′ : ∀ M {A} → ∅ ⊢ M ⦂ A → Value M ⊎ ∃[ N ](M —→ N) ``` + This leads to a less perspicuous proof. Instead of the mnemonic `done` and `step` we use `inj₁` and `inj₂`, and the term `N` is no longer implicit and so must be written out in full. In the case for `β-ƛ` @@ -206,7 +212,7 @@ determine its bound variable and body, `ƛ x ⇒ N`, so we can show that Show that `Progress M` is isomorphic to `Value M ⊎ ∃[ N ](M —→ N)`. -``` +```agda -- Your code goes here ``` @@ -215,7 +221,7 @@ Show that `Progress M` is isomorphic to `Value M ⊎ ∃[ N ](M —→ N)`. Write out the proof of `progress′` in full, and compare it to the proof of `progress` above. -``` +```agda -- Your code goes here ``` @@ -223,7 +229,8 @@ proof of `progress` above. Combine `progress` and `—→¬V` to write a program that decides whether a well-typed term is a value: -``` + +```agda postulate value? : ∀ {A M} → ∅ ⊢ M ⦂ A → Dec (Value M) ``` @@ -318,7 +325,8 @@ for lambda expressions, and similarly for case and fixpoint. To deal with this situation, we first prove a lemma showing that if one context maps to another, this is still true after adding the same variable to both contexts: -``` + +```agda ext : ∀ {Γ Δ} → (∀ {x A} → Γ ∋ x ⦂ A → Δ ∋ x ⦂ A) ----------------------------------------------------- @@ -326,6 +334,7 @@ ext : ∀ {Γ Δ} ext ρ Z = Z ext ρ (S x≢y ∋x) = S x≢y (ρ ∋x) ``` + Let `ρ` be the name of the map that takes evidence that `x` appears in `Γ` to evidence that `x` appears in `Δ`. The proof is by case analysis of the evidence that `x` appears @@ -343,7 +352,8 @@ applying `ρ` to find the evidence that `x` appears in `Δ`. With the extension lemma under our belts, it is straightforward to prove renaming preserves types: -``` + +```agda rename : ∀ {Γ Δ} → (∀ {x A} → Γ ∋ x ⦂ A → Δ ∋ x ⦂ A) ---------------------------------- @@ -356,6 +366,7 @@ rename ρ (⊢suc ⊢M) = ⊢suc (rename ρ ⊢M) rename ρ (⊢case ⊢L ⊢M ⊢N) = ⊢case (rename ρ ⊢L) (rename ρ ⊢M) (rename (ext ρ) ⊢N) rename ρ (⊢μ ⊢M) = ⊢μ (rename (ext ρ) ⊢M) ``` + As before, let `ρ` be the name of the map that takes evidence that `x` appears in `Γ` to evidence that `x` appears in `Δ`. We induct on the evidence that `M` is well typed in `Γ`. Let's unpack the @@ -384,7 +395,8 @@ We have three important corollaries, each proved by constructing a suitable map between contexts. First, a closed term can be weakened to any context: -``` + +```agda weaken : ∀ {Γ M A} → ∅ ⊢ M ⦂ A ---------- @@ -397,12 +409,14 @@ weaken {Γ} ⊢M = rename ρ ⊢M → Γ ∋ z ⦂ C ρ () ``` + Here the map `ρ` is trivial, since there are no possible arguments in the empty context `∅`. Second, if the last two variables in a context are equal then we can drop the shadowed one: -``` + +```agda drop : ∀ {Γ x M A B C} → Γ , x ⦂ A , x ⦂ B ⊢ M ⦂ C -------------------------- @@ -417,6 +431,7 @@ drop {Γ} {x} {M} {A} {B} {C} ⊢M = rename ρ ⊢M ρ (S x≢x Z) = ⊥-elim (x≢x refl) ρ (S z≢x (S _ ∋z)) = S z≢x ∋z ``` + Here map `ρ` can never be invoked on the inner occurrence of `x` since it is masked by the outer occurrence. Skipping over the `x` in the first position can only happen if the variable looked for differs from @@ -425,7 +440,8 @@ found in the second position, which also contains `x`, this leads to a contradiction (evidenced by `x≢x refl`). Third, if the last two variables in a context differ then we can swap them: -``` + +```agda swap : ∀ {Γ x y M A B C} → x ≢ y → Γ , y ⦂ B , x ⦂ A ⊢ M ⦂ C @@ -441,6 +457,7 @@ swap {Γ} {x} {y} {M} {A} {B} {C} x≢y ⊢M = rename ρ ⊢M ρ (S z≢x Z) = Z ρ (S z≢x (S z≢y ∋z)) = S z≢y (S z≢x ∋z) ``` + Here the renaming map takes a variable at the end into a variable one from the end, and vice versa. The first line is responsible for moving `x` from a position at the end to a position one from the end @@ -467,7 +484,8 @@ variables the context grows. So for the induction to go through, we require an arbitrary context `Γ`, as in the statement of the lemma. Here is the formal statement and proof that substitution preserves types: -``` + +```agda subst : ∀ {Γ x N V A B} → ∅ ⊢ V ⦂ A → Γ , x ⦂ A ⊢ N ⦂ B @@ -492,6 +510,7 @@ subst {x = y} ⊢V (⊢μ {x = x} ⊢M) with x ≟ y ... | yes refl = ⊢μ (drop ⊢M) ... | no x≢y = ⊢μ (subst ⊢V (swap x≢y ⊢M)) ``` + We induct on the evidence that `N` is well typed in the context `Γ` extended by `x`. @@ -661,7 +680,7 @@ should factor dealing with bound variables into a single function, defined by mutual recursion with the proof that substitution preserves types. -``` +```agda -- Your code goes here ``` @@ -669,13 +688,15 @@ preserves types. ## Decomposition An evaluation context can be typed as follows. -``` + +```agda _⦂_==>_ : Eval → Type → Type → Set E ⦂ A ==> B = ∀(M : Term) → (∅ ⊢ M ⦂ A) → (∅ ⊢ E [ M ] ⦂ B) ``` We then have the following lemma. -``` + +```agda data Decompose (E : Eval) (M : Term) (B : Type) : Set where decompose : ∀{A : Type} → ∅ ⊢ M ⦂ A @@ -704,7 +725,7 @@ Once we have shown that substitution preserves types and decomposition, showing that reduction preserves types is straightforward: -``` +```agda preserve⊢→ : ∀ {M N A} → ∅ ⊢ M ⦂ A → M ⊢→ N @@ -786,7 +807,7 @@ and each `β` rule follows by the substitution lemma. -- well-typed term to its value, if it has one. -- Some terms may reduce forever. Here is a simple example: --- ``` +-- ```agda -- sucμ = μ "x" ⇒ `suc (` "x") -- _ = @@ -801,6 +822,7 @@ and each `β` rule follows by the substitution lemma. -- -- ... -- ∎ -- ``` + -- Since every Agda computation must terminate, -- we cannot simply ask Agda to reduce a term to a value. -- Instead, we will provide a natural number to Agda, and permit it @@ -822,15 +844,16 @@ and each `β` rule follows by the substitution lemma. -- By analogy, we will use the name _gas_ for the parameter which puts a -- bound on the number of reduction steps. `Gas` is specified by a natural number: --- ``` +-- ```agda -- record Gas : Set where -- constructor gas -- field -- amount : ℕ -- ``` + -- When our evaluator returns a term `N`, it will either give evidence that -- `N` is a value or indicate that it ran out of gas: --- ``` +-- ```agda -- data Finished (N : Term) : Set where -- done : @@ -842,10 +865,11 @@ and each `β` rule follows by the substitution lemma. -- ---------- -- Finished N -- ``` + -- Given a term `L` of type `A`, the evaluator will, for some `N`, return -- a reduction sequence from `L` to `N` and an indication of whether -- reduction finished: --- ``` +-- ```agda -- data Steps (L : Term) : Set where -- steps : ∀ {N} @@ -854,9 +878,10 @@ and each `β` rule follows by the substitution lemma. -- ---------- -- → Steps L -- ``` + -- The evaluator takes gas and evidence that a term is well typed, -- and returns the corresponding steps: --- ``` +-- ```agda -- eval : ∀ {L A} -- → Gas -- → ∅ ⊢ L ⦂ A @@ -868,6 +893,7 @@ and each `β` rule follows by the substitution lemma. -- ... | step {M} L—→M with eval (gas m) (preserve ⊢L L—→M) -- ... | steps M—↠N fin = steps (L —→⟨ L—→M ⟩ M—↠N) fin -- ``` + -- Let `L` be the name of the term we are reducing, and `⊢L` be the -- evidence that `L` is well typed. We consider the amount of gas -- remaining. There are two possibilities: @@ -898,15 +924,16 @@ and each `β` rule follows by the substitution lemma. -- -- We can now use Agda to compute the non-terminating reduction -- -- sequence given earlier. First, we show that the term `sucμ` -- -- is well typed: --- -- ``` +-- -- ```agda -- -- ⊢sucμ : ∅ ⊢ μ "x" ⇒ `suc ` "x" ⦂ `ℕ -- -- ⊢sucμ = ⊢μ (⊢suc (⊢` ∋x)) -- -- where -- -- ∋x = Z -- -- ``` + -- -- To show the first three steps of the infinite reduction -- -- sequence, we evaluate with three steps worth of gas: --- -- ``` +-- -- ```agda -- -- _ : eval (gas 3) ⊢sucμ ≡ -- -- steps -- -- (μ "x" ⇒ `suc ` "x" @@ -924,7 +951,7 @@ and each `β` rule follows by the substitution lemma. -- -- Similarly, we can use Agda to compute the reduction sequences given -- -- in the previous chapter. We start with the Church numeral two -- -- applied to successor and zero. Supplying 100 steps of gas is more than enough: --- -- ``` +-- -- ```agda -- -- _ : eval (gas 100) (⊢twoᶜ · ⊢sucᶜ · ⊢zero) ≡ -- -- steps -- -- ((ƛ "s" ⇒ (ƛ "z" ⇒ ` "s" · (` "s" · ` "z"))) · (ƛ "n" ⇒ `suc ` "n") @@ -942,6 +969,7 @@ and each `β` rule follows by the substitution lemma. -- -- (done (V-suc (V-suc V-zero))) -- -- _ = refl -- -- ``` + -- -- The example above was generated by using `C-c C-n` to normalise the -- -- left-hand side of the equation and pasting in the result as the -- -- right-hand side of the equation. The example reduction of the @@ -949,7 +977,7 @@ and each `β` rule follows by the substitution lemma. -- -- writing `twoᶜ` and `sucᶜ` in place of their expansions. -- -- Next, we show two plus two is four: --- -- ``` +-- -- ```agda -- -- _ : eval (gas 100) ⊢2+2 ≡ -- -- steps -- -- ((μ "+" ⇒ @@ -1110,11 +1138,12 @@ and each `β` rule follows by the substitution lemma. -- -- (done (V-suc (V-suc (V-suc (V-suc V-zero))))) -- -- _ = refl -- -- ``` + -- -- Again, the derivation in the previous chapter was derived by -- -- editing the above. -- -- Similarly, we can evaluate the corresponding term for Church numerals: --- -- ``` +-- -- ```agda -- -- _ : eval (gas 100) ⊢2+2ᶜ ≡ -- -- steps -- -- ((ƛ "m" ⇒ @@ -1179,6 +1208,7 @@ and each `β` rule follows by the substitution lemma. -- -- (done (V-suc (V-suc (V-suc (V-suc V-zero))))) -- -- _ = refl -- -- ``` + -- -- And again, the example in the previous section was derived by editing the -- -- above. @@ -1186,7 +1216,7 @@ and each `β` rule follows by the substitution lemma. -- -- Using the evaluator, confirm that two times two is four. --- -- ``` +-- -- ```agda -- -- -- Your code goes here -- -- ``` @@ -1196,7 +1226,7 @@ and each `β` rule follows by the substitution lemma. -- -- Without peeking at their statements above, write down the progress -- -- and preservation theorems for the simply typed lambda-calculus. --- -- ``` +-- -- ```agda -- -- -- Your code goes here -- -- ``` @@ -1212,7 +1242,7 @@ and each `β` rule follows by the substitution lemma. -- -- Find two counter-examples to subject expansion, one -- -- with case expressions and one not involving case expressions. --- -- ``` +-- -- ```agda -- -- -- Your code goes here -- -- ``` @@ -1220,19 +1250,19 @@ and each `β` rule follows by the substitution lemma. -- -- ## Well-typed terms don't get stuck -- -- A term is _normal_ if it cannot reduce: --- -- ``` +-- -- ```agda -- -- Normal : Term → Set -- -- Normal M = ∀ {N} → ¬ (M —→ N) -- -- ``` -- -- A term is _stuck_ if it is normal yet not a value: --- -- ``` +-- -- ```agda -- -- Stuck : Term → Set -- -- Stuck M = Normal M × ¬ Value M -- -- ``` -- -- Using progress, it is easy to show that no well-typed term is stuck: --- -- ``` +-- -- ```agda -- -- postulate -- -- unstuck : ∀ {M A} -- -- → ∅ ⊢ M ⦂ A @@ -1242,7 +1272,7 @@ and each `β` rule follows by the substitution lemma. -- -- Using preservation, it is easy to show that after any number of steps, -- -- a well-typed term remains well typed: --- -- ``` +-- -- ```agda -- -- postulate -- -- preserves : ∀ {M N A} -- -- → ∅ ⊢ M ⦂ A @@ -1253,7 +1283,7 @@ and each `β` rule follows by the substitution lemma. -- -- An easy consequence is that starting from a well-typed term, taking -- -- any number of reduction steps leads to a term that is not stuck: --- -- ``` +-- -- ```agda -- -- postulate -- -- wttdgs : ∀ {M N A} -- -- → ∅ ⊢ M ⦂ A @@ -1261,6 +1291,7 @@ and each `β` rule follows by the substitution lemma. -- -- ----------- -- -- → ¬ (Stuck N) -- -- ``` + -- -- Felleisen and Wright, who introduced proofs via progress and -- -- preservation, summarised this result with the slogan _well-typed terms -- -- don't get stuck_. (They were referring to earlier work by Robin @@ -1272,7 +1303,7 @@ and each `β` rule follows by the substitution lemma. -- -- Give an example of an ill-typed term that does get stuck. --- -- ``` +-- -- ```agda -- -- -- Your code goes here -- -- ``` @@ -1280,7 +1311,7 @@ and each `β` rule follows by the substitution lemma. -- -- Provide proofs of the three postulates, `unstuck`, `preserves`, and `wttdgs` above. --- -- ``` +-- -- ```agda -- -- -- Your code goes here -- -- ``` @@ -1293,7 +1324,7 @@ and each `β` rule follows by the substitution lemma. -- -- of congruence to deal with functions of four arguments -- -- (to deal with `case_[zero⇒_|suc_⇒_]`). It -- -- is exactly analogous to `cong` and `cong₂` as defined previously: --- -- ``` +-- -- ```agda -- -- cong₄ : ∀ {A B C D E : Set} (f : A → B → C → D → E) -- -- {s w : A} {t x : B} {u y : C} {v z : D} -- -- → s ≡ w → t ≡ x → u ≡ y → v ≡ z → f s t u v ≡ f w x y z @@ -1301,7 +1332,7 @@ and each `β` rule follows by the substitution lemma. -- -- ``` -- -- It is now straightforward to show that reduction is deterministic: --- -- ``` +-- -- ```agda -- -- det : ∀ {M M′ M″} -- -- → (M —→ M′) -- -- → (M —→ M″) @@ -1327,6 +1358,7 @@ and each `β` rule follows by the substitution lemma. -- -- det (β-suc _) (β-suc _) = refl -- -- det β-μ β-μ = refl -- -- ``` + -- -- The proof is by induction over possible reductions. We consider -- -- three typical cases: diff --git a/extra/Frames/Lambda.lagda.md b/extra/Frames/Lambda.lagda.md index f4d9f7191..b24ad32e3 100644 --- a/extra/Frames/Lambda.lagda.md +++ b/extra/Frames/Lambda.lagda.md @@ -3,7 +3,7 @@ title : "Lambda: Introduction to Lambda Calculus" permalink : /Lambda/ --- -``` +```agda module Lambda where ``` @@ -49,7 +49,7 @@ four. ## Imports -``` +```agda open import Data.Bool using (T; not) open import Data.Empty using (⊥; ⊥-elim) open import Data.List using (List; _∷_; []) @@ -98,7 +98,8 @@ Here is the syntax of terms in Backus-Naur Form (BNF): μ x ⇒ M And here it is formalised in Agda: -``` + +```agda Id : Set Id = String @@ -117,6 +118,7 @@ data Term : Set where case_[zero⇒_|suc_⇒_] : Term → Term → Id → Term → Term μ_⇒_ : Id → Term → Term ``` + We represent identifiers by strings. We choose precedence so that lambda abstraction and fixpoint bind least tightly, then application, then successor, and tightest of all is the constructor for variables. @@ -128,7 +130,8 @@ Case expressions are self-bracketing. Here are some example terms: the natural number two, a function that adds naturals, and a term that computes two plus two: -``` + +```agda two : Term two = `suc `suc `zero @@ -138,6 +141,7 @@ plus = μ "+" ⇒ ƛ "m" ⇒ ƛ "n" ⇒ [zero⇒ ` "n" |suc "m" ⇒ `suc (` "+" · ` "m" · ` "n") ] ``` + The recursive definition of addition is similar to our original definition of `_+_` for naturals, as given in Chapter [Naturals](/Naturals/#plus). @@ -159,7 +163,8 @@ second. This is called the _Church representation_ of the naturals. Here are some example terms: the Church numeral two, a function that adds Church numerals, a function to compute successor, and a term that computes two plus two: -``` + +```agda twoᶜ : Term twoᶜ = ƛ "s" ⇒ ƛ "z" ⇒ ` "s" · (` "s" · ` "z") @@ -170,6 +175,7 @@ plusᶜ = ƛ "m" ⇒ ƛ "n" ⇒ ƛ "s" ⇒ ƛ "z" ⇒ sucᶜ : Term sucᶜ = ƛ "n" ⇒ `suc (` "n") ``` + The Church numeral for two takes two arguments `s` and `z` and applies `s` twice to `z`. Addition takes two numerals `m` and `n`, a @@ -193,7 +199,7 @@ Write out the definition of a lambda term that multiplies two natural numbers. Your definition may use `plus` as defined earlier. -``` +```agda -- Your code goes here ``` @@ -205,7 +211,7 @@ two natural numbers represented as Church numerals. Your definition may use `plusᶜ` as defined earlier (or may not — there are nice definitions both ways). -``` +```agda -- Your code goes here ``` @@ -215,7 +221,8 @@ definition may use `plusᶜ` as defined earlier (or may not Some people find it annoying to write `` ` "x" `` instead of `x`. We can make examples with lambda terms slightly easier to write by adding the following definitions: -``` + +```agda ƛ′_⇒_ : Term → Term → Term ƛ′ (` x) ⇒ N = ƛ x ⇒ N ƛ′ _ ⇒ _ = ⊥-elim impossible @@ -231,6 +238,7 @@ case′ _ [zero⇒ _ |suc _ ⇒ _ ] = ⊥-elim impossible μ′ _ ⇒ _ = ⊥-elim impossible where postulate impossible : ⊥ ``` + We intend to apply the function only when the first term is a variable, which we indicate by postulating a term `impossible` of the empty type `⊥`. If we use C-c C-n to normalise the term @@ -246,7 +254,8 @@ used with care, since such postulation could allow us to provide evidence of _any_ proposition whatsoever, regardless of its truth. The definition of `plus` can now be written as follows: -``` + +```agda plus′ : Term plus′ = μ′ + ⇒ ƛ′ m ⇒ ƛ′ n ⇒ case′ m @@ -257,6 +266,7 @@ plus′ = μ′ + ⇒ ƛ′ m ⇒ ƛ′ n ⇒ m = ` "m" n = ` "n" ``` + Write out the definition of multiplication in the same style. @@ -355,7 +365,7 @@ as values; thus, `` plus `` by itself is considered a value. The predicate `Value M` holds if term `M` is a value: -``` +```agda data Value : Term → Set where instance @@ -458,7 +468,7 @@ which will be adequate for our purposes. Here is the formal definition of substitution by closed terms in Agda: -``` +```agda infix 9 _[_:=_] _[_:=_] : Term → Id → Term → Term @@ -501,7 +511,7 @@ simply push substitution recursively into the subterms. Here is confirmation that the examples above are correct: -``` +```agda _ : (ƛ "z" ⇒ ` "s" · (` "s" · ` "z")) [ "s" := sucᶜ ] ≡ ƛ "z" ⇒ sucᶜ · (sucᶜ · ` "z") _ = refl @@ -544,7 +554,7 @@ substitution. ## Evaluation contexts -``` +```agda infix 7 □·_ infix 7 _·□ infix 8 `suc□ @@ -616,7 +626,7 @@ case where we substitute by a term that is not a value. Here are the rules formalised in Agda: -``` +```agda infix 4 _—→_ data _—→_ : Term → Term → Set where @@ -700,7 +710,8 @@ We define reflexive and transitive closure as a sequence of zero or more steps of the underlying relation, along lines similar to that for reasoning about chains of equalities in Chapter [Equality](/Equality/): -``` + +```agda infix 2 _—↠_ infix 1 begin_ infixr 2 _—→⟨_⟩_ @@ -723,6 +734,7 @@ begin_ : ∀ {M N} → M —↠ N begin M—↠N = M—↠N ``` + We can read this as follows: * From term `M`, we can take no steps, giving a step of type `M —↠ M`. @@ -739,7 +751,8 @@ appealing way, as we will see in the next section. An alternative is to define reflexive and transitive closure directly, as the smallest relation that includes `—→` and is also reflexive and transitive. We could do so as follows: -``` + +```agda data _—↠′_ : Term → Term → Set where step′ : ∀ {M N} @@ -757,6 +770,7 @@ data _—↠′_ : Term → Term → Set where ------- → L —↠′ N ``` + 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). @@ -766,7 +780,7 @@ the two definitions are equivalent (indeed, one embeds in the other). Show that the first notion of reflexive and transitive closure above embeds into the second. Why are they not isomorphic? -``` +```agda -- Your code goes here ``` @@ -794,7 +808,7 @@ while if the top two lines stand for a single reduction step and the bottom two stand for zero or more reduction steps it is called the diamond property. In symbols: -``` +```agda postulate confluence : ∀ {L M N} → ((L —↠ M) × (L —↠ N)) @@ -810,7 +824,7 @@ postulate The reduction system studied in this chapter is deterministic. In symbols: -``` +```agda postulate deterministic : ∀ {L M N} → L —→ M @@ -828,7 +842,8 @@ systems studied in this text are trivially confluent. We start with a simple example. The Church numeral two applied to the successor function and zero yields the natural number two: -``` + +```agda _ : twoᶜ · sucᶜ · `zero —↠ `suc `suc `zero _ = begin @@ -845,7 +860,8 @@ _ = ``` Here is a sample reduction demonstrating that two plus two is four: -``` + +```agda _ : plus · two · two —↠ `suc `suc `suc `suc `zero _ = begin @@ -890,7 +906,8 @@ _ = ``` And here is a similar sample reduction for Church numerals: -``` + +```agda _ : plusᶜ · twoᶜ · twoᶜ · sucᶜ · `zero —↠ `suc `suc `suc `suc `zero _ = begin @@ -931,7 +948,7 @@ In the next chapter, we will see how to compute such reduction sequences. Write out the reduction sequence demonstrating that one plus one is two. -``` +```agda -- Your code goes here ``` @@ -951,7 +968,7 @@ Here is the syntax of types in BNF: And here it is formalised in Agda: -``` +```agda infixr 7 _⇒_ data Type : Set where @@ -1019,7 +1036,7 @@ and variable `` "z" `` with type `` `ℕ ``. Contexts are formalised as follows: -``` +```agda infixl 5 _,_⦂_ data Context : Set where @@ -1039,7 +1056,7 @@ to the list [ ⟨ "z" , `ℕ ⟩ , ⟨ "s" , `ℕ ⇒ `ℕ ⟩ ] -``` +```agda -- Your code goes here ``` @@ -1070,7 +1087,8 @@ the other variables. For example, Here `` "x" ⦂ `ℕ ⇒ `ℕ `` is shadowed by `` "x" ⦂ `ℕ ``. Lookup is formalised as follows: -``` + +```agda infix 4 _∋_⦂_ data _∋_⦂_ : Context → Id → Type → Set where @@ -1095,14 +1113,14 @@ variable with the same name to its left in the list. It can be rather tedious to use the `S` constructor, as you have to provide proofs that `x ≢ y` each time. For example: -``` +```agda _ : ∅ , "x" ⦂ `ℕ ⇒ `ℕ , "y" ⦂ `ℕ , "z" ⦂ `ℕ ∋ "x" ⦂ `ℕ ⇒ `ℕ _ = S (λ()) (S (λ()) Z) ``` Instead, we'll use a "smart constructor", which uses [proof by reflection](/Decidable/#proof-by-reflection) to check the inequality while type checking: -``` +```agda S′ : ∀ {Γ x y A B} → {x≢y : False (x ≟ y)} → Γ ∋ x ⦂ A @@ -1130,7 +1148,8 @@ For example: * `` ∅ ⊢ ƛ "s" ⇒ ƛ "z" ⇒ ` "s" · (` "s" · ` "z") ⦂ (`ℕ ⇒ `ℕ) ⇒ `ℕ ⇒ `ℕ `` Typing is formalised as follows: -``` + +```agda infix 4 _⊢_⦂_ data _⊢_⦂_ : Context → Term → Type → Set where @@ -1232,7 +1251,8 @@ The typing derivation is valid for any `Γ` and `A`, for instance, we might take `Γ` to be `∅` and `A` to be `` `ℕ ``. Here is the above typing derivation formalised in Agda: -``` + +```agda Ch : Type → Type Ch A = (A ⇒ A) ⇒ A ⇒ A @@ -1244,7 +1264,8 @@ Ch A = (A ⇒ A) ⇒ A ⇒ A ``` Here are the typings corresponding to computing two plus two: -``` + +```agda ⊢two : ∀ {Γ} → Γ ⊢ two ⦂ `ℕ ⊢two = ⊢suc (⊢suc ⊢zero) @@ -1261,6 +1282,7 @@ Here are the typings corresponding to computing two plus two: ⊢2+2 : ∅ ⊢ plus · two · two ⦂ `ℕ ⊢2+2 = ⊢plus · ⊢two · ⊢two ``` + In contrast to our earlier examples, here we have typed `two` and `plus` in an arbitrary context rather than the empty context; this makes it easy to use them inside other binding contexts as well as at the top level. @@ -1271,7 +1293,8 @@ contexts, the first where `"n"` is the last binding in the context, and the second after `"m"` is bound in the successor branch of the case. And here are typings for the remainder of the Church example: -``` + +```agda ⊢plusᶜ : ∀ {Γ A} → Γ ⊢ plusᶜ ⦂ Ch A ⇒ Ch A ⇒ Ch A ⊢plusᶜ = ⊢ƛ (⊢ƛ (⊢ƛ (⊢ƛ (⊢` ∋m · ⊢` ∋s · (⊢` ∋n · ⊢` ∋s · ⊢` ∋z))))) where @@ -1337,7 +1360,8 @@ will show how to use Agda to compute type derivations directly. The lookup relation `Γ ∋ x ⦂ A` is functional, in that for each `Γ` and `x` there is at most one `A` such that the judgment holds: -``` + +```agda ∋-functional : ∀ {Γ x A B} → Γ ∋ x ⦂ A → Γ ∋ x ⦂ B → A ≡ B ∋-functional Z Z = refl ∋-functional Z (S x≢ _) = ⊥-elim (x≢ refl) @@ -1356,7 +1380,7 @@ a formal proof that it is not possible to type the term requires that the first term in the application is both a natural and a function: -``` +```agda nope₁ : ∀ {A} → ¬ (∅ ⊢ `zero · `suc `zero ⦂ A) nope₁ (() · _) ``` @@ -1365,7 +1389,7 @@ As a second example, here is a formal proof that it is not possible to type `` ƛ "x" ⇒ ` "x" · ` "x" ``. It cannot be typed, because doing so requires types `A` and `B` such that `A ⇒ B ≡ A`: -``` +```agda nope₂ : ∀ {A} → ¬ (∅ ⊢ ƛ "x" ⇒ ` "x" · ` "x" ⦂ A) nope₂ (⊢ƛ (⊢` ∋x · ⊢` ∋x′)) = contradiction (∋-functional ∋x ∋x′) where @@ -1395,7 +1419,7 @@ or explain why there are no such types. Using the term `mul` you defined earlier, write out the derivation showing that it is well typed. -``` +```agda -- Your code goes here ``` @@ -1405,7 +1429,7 @@ showing that it is well typed. Using the term `mulᶜ` you defined earlier, write out the derivation showing that it is well typed. -``` +```agda -- Your code goes here ``` diff --git a/extra/Frames/Properties.lagda.md b/extra/Frames/Properties.lagda.md index d88a0b88f..1cdee0b20 100644 --- a/extra/Frames/Properties.lagda.md +++ b/extra/Frames/Properties.lagda.md @@ -3,7 +3,7 @@ title : "Properties: Progress and Preservation" permalink : /Properties/ --- -``` +```agda module Properties where ``` @@ -16,7 +16,7 @@ sequences for us. ## Imports -``` +```agda open import Relation.Binary.PropositionalEquality using (_≡_; _≢_; refl; sym; cong; cong₂) open import Data.String using (String; _≟_) @@ -105,7 +105,8 @@ that `M —→ N`. To formulate this property, we first introduce a relation that captures what it means for a term `M` to make progress: -``` + +```agda data Progress (M : Term) : Set where step : ∀ {N} @@ -118,12 +119,14 @@ data Progress (M : Term) : Set where ---------- → Progress M ``` + A term `M` makes progress if either it can take a step, meaning there exists a term `N` such that `M —→ N`, or if it is done, meaning that `M` is a value. If a term is well typed in the empty context then it satisfies progress: -``` + +```agda progress : ∀ {M A} → ∅ ⊢ M ⦂ A ---------- @@ -145,6 +148,7 @@ progress (⊢case ⊢L ⊢M ⊢N) with progress ⊢L ... | done {{V-suc}} = step β-suc progress (⊢μ ⊢M) = step β-μ ``` + We induct on the evidence that the term is well typed. Let's unpack the first three cases: @@ -190,10 +194,12 @@ or introduce subsidiary functions. Instead of defining a data type for `Progress M`, we could have formulated progress using disjunction and existentials: -``` + +```agda postulate progress′ : ∀ M {A} → ∅ ⊢ M ⦂ A → Value M ⊎ ∃[ N ](M —→ N) ``` + This leads to a less perspicuous proof. Instead of the mnemonic `done` and `step` we use `inj₁` and `inj₂`, and the term `N` is no longer implicit and so must be written out in full. In the case for `β-ƛ` @@ -205,7 +211,7 @@ determine its bound variable and body, `ƛ x ⇒ N`, so we can show that Show that `Progress M` is isomorphic to `Value M ⊎ ∃[ N ](M —→ N)`. -``` +```agda -- Your code goes here ``` @@ -214,7 +220,7 @@ Show that `Progress M` is isomorphic to `Value M ⊎ ∃[ N ](M —→ N)`. Write out the proof of `progress′` in full, and compare it to the proof of `progress` above. -``` +```agda -- Your code goes here ``` @@ -222,7 +228,8 @@ proof of `progress` above. Combine `progress` and `—→¬V` to write a program that decides whether a well-typed term is a value: -``` + +```agda postulate value? : ∀ {A M} → ∅ ⊢ M ⦂ A → Dec (Value M) ``` @@ -317,7 +324,8 @@ for lambda expressions, and similarly for case and fixpoint. To deal with this situation, we first prove a lemma showing that if one context maps to another, this is still true after adding the same variable to both contexts: -``` + +```agda ext : ∀ {Γ Δ} → (∀ {x A} → Γ ∋ x ⦂ A → Δ ∋ x ⦂ A) ----------------------------------------------------- @@ -325,6 +333,7 @@ ext : ∀ {Γ Δ} ext ρ Z = Z ext ρ (S x≢y ∋x) = S x≢y (ρ ∋x) ``` + Let `ρ` be the name of the map that takes evidence that `x` appears in `Γ` to evidence that `x` appears in `Δ`. The proof is by case analysis of the evidence that `x` appears @@ -342,7 +351,8 @@ applying `ρ` to find the evidence that `x` appears in `Δ`. With the extension lemma under our belts, it is straightforward to prove renaming preserves types: -``` + +```agda rename : ∀ {Γ Δ} → (∀ {x A} → Γ ∋ x ⦂ A → Δ ∋ x ⦂ A) ---------------------------------- @@ -355,6 +365,7 @@ rename ρ (⊢suc ⊢M) = ⊢suc (rename ρ ⊢M) rename ρ (⊢case ⊢L ⊢M ⊢N) = ⊢case (rename ρ ⊢L) (rename ρ ⊢M) (rename (ext ρ) ⊢N) rename ρ (⊢μ ⊢M) = ⊢μ (rename (ext ρ) ⊢M) ``` + As before, let `ρ` be the name of the map that takes evidence that `x` appears in `Γ` to evidence that `x` appears in `Δ`. We induct on the evidence that `M` is well typed in `Γ`. Let's unpack the @@ -383,7 +394,8 @@ We have three important corollaries, each proved by constructing a suitable map between contexts. First, a closed term can be weakened to any context: -``` + +```agda weaken : ∀ {Γ M A} → ∅ ⊢ M ⦂ A ---------- @@ -396,12 +408,14 @@ weaken {Γ} ⊢M = rename ρ ⊢M → Γ ∋ z ⦂ C ρ () ``` + Here the map `ρ` is trivial, since there are no possible arguments in the empty context `∅`. Second, if the last two variables in a context are equal then we can drop the shadowed one: -``` + +```agda drop : ∀ {Γ x M A B C} → Γ , x ⦂ A , x ⦂ B ⊢ M ⦂ C -------------------------- @@ -416,6 +430,7 @@ drop {Γ} {x} {M} {A} {B} {C} ⊢M = rename ρ ⊢M ρ (S x≢x Z) = ⊥-elim (x≢x refl) ρ (S z≢x (S _ ∋z)) = S z≢x ∋z ``` + Here map `ρ` can never be invoked on the inner occurrence of `x` since it is masked by the outer occurrence. Skipping over the `x` in the first position can only happen if the variable looked for differs from @@ -424,7 +439,8 @@ found in the second position, which also contains `x`, this leads to a contradiction (evidenced by `x≢x refl`). Third, if the last two variables in a context differ then we can swap them: -``` + +```agda swap : ∀ {Γ x y M A B C} → x ≢ y → Γ , y ⦂ B , x ⦂ A ⊢ M ⦂ C @@ -440,6 +456,7 @@ swap {Γ} {x} {y} {M} {A} {B} {C} x≢y ⊢M = rename ρ ⊢M ρ (S z≢x Z) = Z ρ (S z≢x (S z≢y ∋z)) = S z≢y (S z≢x ∋z) ``` + Here the renaming map takes a variable at the end into a variable one from the end, and vice versa. The first line is responsible for moving `x` from a position at the end to a position one from the end @@ -466,7 +483,8 @@ variables the context grows. So for the induction to go through, we require an arbitrary context `Γ`, as in the statement of the lemma. Here is the formal statement and proof that substitution preserves types: -``` + +```agda subst : ∀ {Γ x N V A B} → ∅ ⊢ V ⦂ A → Γ , x ⦂ A ⊢ N ⦂ B @@ -491,6 +509,7 @@ subst {x = y} ⊢V (⊢μ {x = x} ⊢M) with x ≟ y ... | yes refl = ⊢μ (drop ⊢M) ... | no x≢y = ⊢μ (subst ⊢V (swap x≢y ⊢M)) ``` + We induct on the evidence that `N` is well typed in the context `Γ` extended by `x`. @@ -660,7 +679,7 @@ should factor dealing with bound variables into a single function, defined by mutual recursion with the proof that substitution preserves types. -``` +```agda -- Your code goes here ``` @@ -670,7 +689,7 @@ preserves types. Once we have shown that substitution preserves types, showing that reduction preserves types is straightforward: -``` +```agda preserve : ∀ {M N A} → ∅ ⊢ M ⦂ A → M —→ N @@ -689,6 +708,7 @@ preserve (⊢case ⊢zero ⊢M ⊢N) β-zero = ⊢M preserve (⊢case (⊢suc ⊢V) ⊢M ⊢N) β-suc = subst ⊢V ⊢N preserve (⊢μ ⊢M) β-μ = subst (⊢μ ⊢M) ⊢M ``` + The proof never mentions the types of `M` or `N`, so in what follows we choose type name as convenient. @@ -751,7 +771,8 @@ function that computes the reduction sequence from any given closed, well-typed term to its value, if it has one. Some terms may reduce forever. Here is a simple example: -``` + +```agda sucμ = μ "x" ⇒ `suc (` "x") _ = @@ -766,6 +787,7 @@ _ = -- ... ∎ ``` + Since every Agda computation must terminate, we cannot simply ask Agda to reduce a term to a value. Instead, we will provide a natural number to Agda, and permit it @@ -787,15 +809,18 @@ per unit of gas. By analogy, we will use the name _gas_ for the parameter which puts a bound on the number of reduction steps. `Gas` is specified by a natural number: -``` + +```agda record Gas : Set where constructor gas field amount : ℕ ``` + When our evaluator returns a term `N`, it will either give evidence that `N` is a value or indicate that it ran out of gas: -``` + +```agda data Finished (N : Term) : Set where done : @@ -807,10 +832,12 @@ data Finished (N : Term) : Set where ---------- Finished N ``` + Given a term `L` of type `A`, the evaluator will, for some `N`, return a reduction sequence from `L` to `N` and an indication of whether reduction finished: -``` + +```agda data Steps (L : Term) : Set where steps : ∀ {N} @@ -819,9 +846,11 @@ data Steps (L : Term) : Set where ---------- → Steps L ``` + The evaluator takes gas and evidence that a term is well typed, and returns the corresponding steps: -``` + +```agda eval : ∀ {L A} → Gas → ∅ ⊢ L ⦂ A @@ -833,6 +862,7 @@ eval {L} (gas (suc m)) ⊢L with progress ⊢L ... | step {M} L—→M with eval (gas m) (preserve ⊢L L—→M) ... | steps M—↠N fin = steps (L —→⟨ L—→M ⟩ M—↠N) fin ``` + Let `L` be the name of the term we are reducing, and `⊢L` be the evidence that `L` is well typed. We consider the amount of gas remaining. There are two possibilities: @@ -863,15 +893,16 @@ remaining. There are two possibilities: -- We can now use Agda to compute the non-terminating reduction -- sequence given earlier. First, we show that the term `sucμ` -- is well typed: --- ``` +-- ```agda -- ⊢sucμ : ∅ ⊢ μ "x" ⇒ `suc ` "x" ⦂ `ℕ -- ⊢sucμ = ⊢μ (⊢suc (⊢` ∋x)) -- where -- ∋x = Z -- ``` + -- To show the first three steps of the infinite reduction -- sequence, we evaluate with three steps worth of gas: --- ``` +-- ```agda -- _ : eval (gas 3) ⊢sucμ ≡ -- steps -- (μ "x" ⇒ `suc ` "x" @@ -889,7 +920,7 @@ remaining. There are two possibilities: -- Similarly, we can use Agda to compute the reduction sequences given -- in the previous chapter. We start with the Church numeral two -- applied to successor and zero. Supplying 100 steps of gas is more than enough: --- ``` +-- ```agda -- _ : eval (gas 100) (⊢twoᶜ · ⊢sucᶜ · ⊢zero) ≡ -- steps -- ((ƛ "s" ⇒ (ƛ "z" ⇒ ` "s" · (` "s" · ` "z"))) · (ƛ "n" ⇒ `suc ` "n") @@ -907,6 +938,7 @@ remaining. There are two possibilities: -- (done (V-suc (V-suc V-zero))) -- _ = refl -- ``` + -- The example above was generated by using `C-c C-n` to normalise the -- left-hand side of the equation and pasting in the result as the -- right-hand side of the equation. The example reduction of the @@ -914,7 +946,7 @@ remaining. There are two possibilities: -- writing `twoᶜ` and `sucᶜ` in place of their expansions. -- Next, we show two plus two is four: --- ``` +-- ```agda -- _ : eval (gas 100) ⊢2+2 ≡ -- steps -- ((μ "+" ⇒ @@ -1075,11 +1107,12 @@ remaining. There are two possibilities: -- (done (V-suc (V-suc (V-suc (V-suc V-zero))))) -- _ = refl -- ``` + -- Again, the derivation in the previous chapter was derived by -- editing the above. -- Similarly, we can evaluate the corresponding term for Church numerals: --- ``` +-- ```agda -- _ : eval (gas 100) ⊢2+2ᶜ ≡ -- steps -- ((ƛ "m" ⇒ @@ -1144,6 +1177,7 @@ remaining. There are two possibilities: -- (done (V-suc (V-suc (V-suc (V-suc V-zero))))) -- _ = refl -- ``` + -- And again, the example in the previous section was derived by editing the -- above. @@ -1151,7 +1185,7 @@ remaining. There are two possibilities: -- Using the evaluator, confirm that two times two is four. --- ``` +-- ```agda -- -- Your code goes here -- ``` @@ -1161,7 +1195,7 @@ remaining. There are two possibilities: -- Without peeking at their statements above, write down the progress -- and preservation theorems for the simply typed lambda-calculus. --- ``` +-- ```agda -- -- Your code goes here -- ``` @@ -1177,7 +1211,7 @@ remaining. There are two possibilities: -- Find two counter-examples to subject expansion, one -- with case expressions and one not involving case expressions. --- ``` +-- ```agda -- -- Your code goes here -- ``` @@ -1185,19 +1219,19 @@ remaining. There are two possibilities: -- ## Well-typed terms don't get stuck -- A term is _normal_ if it cannot reduce: --- ``` +-- ```agda -- Normal : Term → Set -- Normal M = ∀ {N} → ¬ (M —→ N) -- ``` -- A term is _stuck_ if it is normal yet not a value: --- ``` +-- ```agda -- Stuck : Term → Set -- Stuck M = Normal M × ¬ Value M -- ``` -- Using progress, it is easy to show that no well-typed term is stuck: --- ``` +-- ```agda -- postulate -- unstuck : ∀ {M A} -- → ∅ ⊢ M ⦂ A @@ -1207,7 +1241,7 @@ remaining. There are two possibilities: -- Using preservation, it is easy to show that after any number of steps, -- a well-typed term remains well typed: --- ``` +-- ```agda -- postulate -- preserves : ∀ {M N A} -- → ∅ ⊢ M ⦂ A @@ -1218,7 +1252,7 @@ remaining. There are two possibilities: -- An easy consequence is that starting from a well-typed term, taking -- any number of reduction steps leads to a term that is not stuck: --- ``` +-- ```agda -- postulate -- wttdgs : ∀ {M N A} -- → ∅ ⊢ M ⦂ A @@ -1226,6 +1260,7 @@ remaining. There are two possibilities: -- ----------- -- → ¬ (Stuck N) -- ``` + -- Felleisen and Wright, who introduced proofs via progress and -- preservation, summarised this result with the slogan _well-typed terms -- don't get stuck_. (They were referring to earlier work by Robin @@ -1237,7 +1272,7 @@ remaining. There are two possibilities: -- Give an example of an ill-typed term that does get stuck. --- ``` +-- ```agda -- -- Your code goes here -- ``` @@ -1245,7 +1280,7 @@ remaining. There are two possibilities: -- Provide proofs of the three postulates, `unstuck`, `preserves`, and `wttdgs` above. --- ``` +-- ```agda -- -- Your code goes here -- ``` @@ -1258,7 +1293,7 @@ remaining. There are two possibilities: -- of congruence to deal with functions of four arguments -- (to deal with `case_[zero⇒_|suc_⇒_]`). It -- is exactly analogous to `cong` and `cong₂` as defined previously: --- ``` +-- ```agda -- cong₄ : ∀ {A B C D E : Set} (f : A → B → C → D → E) -- {s w : A} {t x : B} {u y : C} {v z : D} -- → s ≡ w → t ≡ x → u ≡ y → v ≡ z → f s t u v ≡ f w x y z @@ -1266,7 +1301,7 @@ remaining. There are two possibilities: -- ``` -- It is now straightforward to show that reduction is deterministic: --- ``` +-- ```agda -- det : ∀ {M M′ M″} -- → (M —→ M′) -- → (M —→ M″) @@ -1292,6 +1327,7 @@ remaining. There are two possibilities: -- det (β-suc _) (β-suc _) = refl -- det β-μ β-μ = refl -- ``` + -- The proof is by induction over possible reductions. We consider -- three typical cases: diff --git a/extra/LambdaReduction.lagda.md b/extra/LambdaReduction.lagda.md index 26cae0c33..5f8185436 100644 --- a/extra/LambdaReduction.lagda.md +++ b/extra/LambdaReduction.lagda.md @@ -3,19 +3,19 @@ title : "Full beta reduction of the untyped lambda calculus" permalink : /LambdaReduction/ --- -``` +```agda module plfa.LambdaReduction where ``` ## Imports -``` +```agda open import plfa.Untyped using (_⊢_; ★; _·_; ƛ_; _,_; _[_]) ``` ## Full beta reduction -``` +```agda infix 2 _—→_ data _—→_ : ∀ {Γ A} → (Γ ⊢ A) → (Γ ⊢ A) → Set where @@ -40,7 +40,7 @@ data _—→_ : ∀ {Γ A} → (Γ ⊢ A) → (Γ ⊢ A) → Set where → ƛ N —→ ƛ N′ ``` -``` +```agda infix 2 _—↠_ infix 1 start_ infixr 2 _—→⟨_⟩_ @@ -65,7 +65,7 @@ start_ : ∀ {Γ} {A} {M N : Γ ⊢ A} start M—↠N = M—↠N ``` -``` +```agda —↠-trans : ∀{Γ}{A}{L M N : Γ ⊢ A} → L —↠ M → M —↠ N @@ -76,7 +76,7 @@ start M—↠N = M—↠N ## Reduction is a congruence -``` +```agda —→-app-cong : ∀{Γ}{L L' M : Γ ⊢ ★} → L —→ L' → L · M —→ L' · M @@ -90,7 +90,7 @@ start M—↠N = M—↠N ## Multi-step reduction is a congruence -``` +```agda abs-cong : ∀ {Γ} {N N' : Γ , ★ ⊢ ★} → N —↠ N' ---------- @@ -99,7 +99,7 @@ abs-cong (M []) = ƛ M [] abs-cong (L —→⟨ r ⟩ rs) = ƛ L —→⟨ ζ r ⟩ abs-cong rs ``` -``` +```agda appL-cong : ∀ {Γ} {L L' M : Γ ⊢ ★} → L —↠ L' --------------- @@ -108,7 +108,7 @@ appL-cong {Γ}{L}{L'}{M} (L []) = L · M [] appL-cong {Γ}{L}{L'}{M} (L —→⟨ r ⟩ rs) = L · M —→⟨ ξ₁ r ⟩ appL-cong rs ``` -``` +```agda appR-cong : ∀ {Γ} {L M M' : Γ ⊢ ★} → M —↠ M' --------------- diff --git a/extra/Modules.lagda.md b/extra/Modules.lagda.md index 1fca8c1af..6f9dcf467 100644 --- a/extra/Modules.lagda.md +++ b/extra/Modules.lagda.md @@ -6,7 +6,7 @@ permalink : /Modules/ ** Turn this into a Setoid example. Copy equivalence relation and setoid from the standard library. ** -``` +```agda module plfa.Modules where ``` @@ -15,7 +15,7 @@ and proves some general results which will be useful later. ## Imports -``` +```agda import Relation.Binary.PropositionalEquality as Eq open Eq using (_≡_; refl; sym; trans; cong) open Eq.≡-Reasoning @@ -43,7 +43,7 @@ some definitions, where we represent collections as lists. (We would call collections *sets*, save that the name `Set` already plays a special role in Agda.) -``` +```agda Coll′ : ∀ {ℓ : Level} → Set ℓ → Set ℓ Coll′ A = List A @@ -60,7 +60,8 @@ essence of the definitions. Instead, we can define a module parameterised by the desired concepts, which are then available throughout. -``` + +```agda module Collection {ℓ : Level} (A : Set ℓ) (_≈_ : A → A → Set ℓ) where Coll : ∀ {ℓ : Level} → Set ℓ → Set ℓ @@ -74,7 +75,8 @@ module Collection {ℓ : Level} (A : Set ℓ) (_≈_ : A → A → Set ℓ) wher ``` Use of a module -``` + +```agda open Collection (ℕ) (_≡_) pattern [_] x = x ∷ [] @@ -93,7 +95,8 @@ ex (there (there ())) Say I want to define a type of stacks, with operations push and pop. I can define stacks in terms of lists, but hide the definitions from the rest of the program. -``` + +```agda abstract Stack : Set → Set @@ -120,9 +123,11 @@ abstract ## Standard Library Definitions similar to those in this chapter can be found in the standard library. -``` + +```agda -- EDIT ``` + The standard library version of `IsMonoid` differs from the one given here, in that it is also parameterised on an equivalence relation. diff --git a/extra/Reflection.lagda.md b/extra/Reflection.lagda.md index 40f7ea27f..e2af4b7e8 100644 --- a/extra/Reflection.lagda.md +++ b/extra/Reflection.lagda.md @@ -3,7 +3,7 @@ title : "Reflection: Proof by Reflection" permalink : /Reflection/ --- -``` +```agda module plfa.Reflection where open import plfa.Lambda hiding (ƛ′_⇒_; _≠_; Ch; ⊢twoᶜ) diff --git a/extra/Subtyping-phil.lagda.md b/extra/Subtyping-phil.lagda.md index 4f34e1b8a..63f6df28a 100644 --- a/extra/Subtyping-phil.lagda.md +++ b/extra/Subtyping-phil.lagda.md @@ -42,6 +42,7 @@ open import Relation.Nullary.Decidable using (True; toWitness) First, we get all our infix declarations out of the way. We list separately operators for judgments, types, and terms: + ```agda infix 4 _∈_ @@ -92,12 +93,14 @@ distinct {X} xs = ∀ (x : X) (x∈xs : x ∈ xs) (x∈xs′ : x ∈ xs) → x One list is a subset of another if every value that is an element of the first is also an element of the second. + ```agda _⊆_ : ∀ {X} (xs ys : List X) → Set xs ⊆ ys = ∀ {x} → x ∈ xs → x ∈ ys ``` Subset is reflexive and transitive. + ```agda ⊆-refl : ∀ {X} (xs : List X) → xs ⊆ xs ⊆-refl xs = id @@ -207,7 +210,7 @@ data _<:_ where ## Subtyping is Reflexive -``` +```agda <:-refl : ∀ (A : Type) → A <: A <:-refl `ℕ = <:-ℕ <:-refl (A ⇒ B) = <:-⇒ (<:-refl A) (<:-refl B) @@ -257,6 +260,7 @@ plays the role of a substructure of `⦗ as ⦂ AS ⦘{d}`. ... | a∈bs = <:-trans (AS<:BS a a∈as a∈bs) (BS<:CS a a∈bs a∈cs) ``` + In the final clause, we are given evidence that `a ∈ as` and `a ∈ cs`, and we use the fact that `cs ⊆ bs` to convert the second of these into evidence that `a ∈ bs`. @@ -362,6 +366,7 @@ data _⊢_ where _⊢*_ {as} Γ AS = ∀ (a : Field) → (a∈as : a ∈ as) → Γ ⊢ AS a a∈as ``` + The right-hand side of `Γ ⊢* AS` is equivalent to `dMap as (map (Γ ⊢_) AS)`. @@ -594,6 +599,7 @@ The statement and proof of progress is much as before, appropriately annotated. We no longer need to explicitly refer to the Canonical Forms lemma, since it is built-in to the definition of value: + ```agda progress : ∀ {A} → (M : ∅ ⊢ A) → Progress M progress (` ()) @@ -628,6 +634,7 @@ progress (M ↑ A<:B) with progress M The reflexive and transitive closure is exactly as before. We simply cut-and-paste the previous definition: + ```agda infix 2 _—↠_ infix 1 begin_ @@ -687,6 +694,7 @@ data Steps {A} : ∅ ⊢ A → Set where ``` The evaluator takes gas and a term and returns the corresponding steps: + ```agda eval : ∀ {A} → Gas @@ -852,7 +860,7 @@ _ = `zero ∎ -``` +```agda -- -- -- #### Exercise `intrinsic-records` (stretch) diff --git a/extra/Subtyping.lagda.md b/extra/Subtyping.lagda.md index 20452cc8b..6322705fd 100644 --- a/extra/Subtyping.lagda.md +++ b/extra/Subtyping.lagda.md @@ -148,11 +148,14 @@ module VecReplica where ``` We now import `Vec` from the Agda standard library. + ```agda open import Data.Vec using (Vec; []; _∷_; lookup) ``` + The following shows the construction of a vector of three integers and vector of two strings. + ```agda _ : Vec ℕ 3 _ = 0 ∷ 1 ∷ 2 ∷ [] @@ -188,12 +191,14 @@ module FinReplica where ``` We import the real `Fin` from the Agda standard library. + ```agda open import Data.Fin using (Fin; zero; suc) ``` The following shows the construction of two values of type `Fin 2`, `zero` and `suc zero`. + ```agda _ : Fin 2 _ = zero @@ -201,6 +206,7 @@ _ = zero _ : Fin 2 _ = suc zero ``` + Note that the value produced by `zero` for type `Fin 2` is not the same value as the value produced by `zero` for type `ℕ`. In general, values of type `Fin n` and of type `ℕ` are not interchangeable. @@ -233,6 +239,7 @@ guaranteed to be less than the length of the vector, so `lookup` is guaranteed to succeed and return an element of the vector. For example, the following example uses `lookup` to obtain the element `7` at index `2` of the vector. + ```agda _ : let vec : Vec ℕ 4 vec = (5 ∷ 0 ∷ 7 ∷ 2 ∷ []) @@ -284,6 +291,7 @@ vector of types. The field names of a record type must be distinct, which we define as follows. + ```agda distinct : ∀{A : Set}{n} → Vec A n → Set distinct [] = ⊤ @@ -292,12 +300,14 @@ distinct (x ∷ xs) = ¬ (x ∈ xs) × distinct xs The fields of one record are a *subset* of the fields of another record if every field of the first is also a field of the second. + ```agda _⊆_ : ∀{n m} → Vec Name n → Vec Name m → Set xs ⊆ ys = (x : Name) → x ∈ xs → x ∈ ys ``` This subset relation is reflexive and transitive. + ```agda ⊆-refl : ∀{n}{ls : Vec Name n} → ls ⊆ ls ⊆-refl {n}{ls} = λ x x∈ls → x∈ls @@ -397,6 +407,7 @@ The second premise of the record subtyping rule (`<:-rcd`) expresses _depth subtyping_, that is, it allows the types of the fields to change according to subtyping. The following is an abbreviation for this premise. + ```agda _⦂_<:_⦂_ : ∀ {m n} → Vec Name m → Vec Type m → Vec Name n → Vec Type n → Set _⦂_<:_⦂_ {m}{n} ks Ss ls Ts = (∀{i : Fin n}{j : Fin m} @@ -412,6 +423,7 @@ and `distinct`. If `y` is an element of vector `xs`, then `y` is at some index `i` of the vector. + ```agda lookup-∈ : ∀{ℓ}{A : Set ℓ}{n} {xs : Vec A n}{y} → y ∈ xs @@ -424,6 +436,7 @@ lookup-∈ {xs = x ∷ xs} (there y∈xs) If one vector `ms` is a subset of another `ns`, then for any element `lookup ms i`, there is an equal element in `ns` at some index. + ```agda lookup-⊆ : ∀{n m : ℕ}{ms : Vec Name n}{ns : Vec Name m}{i : Fin n} → ms ⊆ ns @@ -439,6 +452,7 @@ lookup-⊆ {suc n} {m} {x ∷ ms} {ns} {suc i} x∷ms⊆ns = ## Properties of `distinct` For vectors of distinct elements, lookup is injective. + ```agda distinct-lookup-inj : ∀ {n}{ls : Vec Name n}{i j : Fin n} → distinct ls @@ -478,6 +492,7 @@ distinct? (x ∷ xs) The following function converts irrelevant proofs of distinctness into relevant ones, using `⊥-elim-irrel` in the case where the result of the decision procedure contradicts the irrelevant proof. + ```agda distinct-relevant : ∀ {n}{fs : Vec Name n} .(d : distinct fs) → distinct fs distinct-relevant {n}{fs} d @@ -494,6 +509,7 @@ A` for any type `A`. The proof does not go by induction on the type with its use of `lookup`. We instead use induction on the size of the type. So we first define the size of a type and the size of a vector of types, as follows. + ```agda ty-size : (A : Type) → ℕ vec-ty-size : ∀ {n : ℕ} → (As : Vec Type n) → ℕ @@ -507,6 +523,7 @@ vec-ty-size (x ∷ xs) = ty-size x + vec-ty-size xs ``` The size of a type is always positive. + ```agda ty-size-pos : ∀ {A} → 0 < ty-size A ty-size-pos {A ⇒ B} = s≤s z≤n @@ -515,6 +532,7 @@ ty-size-pos {⦗ fs ⦂ As ⦘ } = s≤s z≤n ``` The size of a type in a vector is less-or-equal in size to the entire vector. + ```agda lookup-vec-ty-size : ∀{k} {As : Vec Type k} {j} → ty-size (lookup As j) ≤ vec-ty-size As @@ -525,6 +543,7 @@ lookup-vec-ty-size {suc k} {A ∷ As} {suc j} = Here is the proof of reflexivity, by induction on the size of the type. We discuss the cases below. + ```agda <:-refl-aux : ∀{n}{A}{m : ty-size A ≤ n} → A <: A <:-refl-aux {0}{A}{m} @@ -544,6 +563,7 @@ We discuss the cases below. let As[i]≤n = ≤-trans (lookup-vec-ty-size {As = As}{i}) (≤-pred m) in <:-refl-aux {n}{lookup As i}{As[i]≤n} ``` + The theorem statement uses `n` as an upper bound on the size of the type `A` and proceeds by induction on `n`. @@ -566,6 +586,7 @@ and proceeds by induction on `n`. is one smaller than the size of `⦗ ls ⦂ As ⦘`. The following corollary packages up reflexivity for ease of use. + ```agda <:-refl : ∀{A} → A <: A <:-refl {A} = <:-refl-aux {ty-size A}{A}{≤-refl} @@ -575,6 +596,7 @@ The following corollary packages up reflexivity for ease of use. The proof of transitivity is by induction on the derivations of `A <: B` and `B <: C`. We discuss the cases below. + ```agda <:-trans : ∀{A B C} → A <: B → B <: C @@ -787,6 +809,7 @@ section and postpone `subst-pres` to the [Preservation](#subtyping-preservation) section. Likewise for `rename`. We begin by defining the `ext` function on renamings. + ```agda ext : (Id → Id) → (Id → Id) ext ρ 0 = 0 @@ -795,6 +818,7 @@ ext ρ (suc x) = suc (ρ x) The `rename` function is defined mutually with the auxiliary `rename-vec` function, which is needed in the case for records. + ```agda rename-vec : (Id → Id) → ∀{n} → Vec Term n → Vec Term n @@ -816,6 +840,7 @@ rename-vec ρ (M ∷ Ms) = rename ρ M ∷ rename-vec ρ Ms With the `rename` function in hand, we can define the `exts` function on substitutions. + ```agda exts : (Id → Term) → (Id → Term) exts σ 0 = ` 0 @@ -824,6 +849,7 @@ exts σ (suc x) = rename suc (σ x) We define `subst` mutually with the auxiliary `subst-vec` function, which is needed in the case for records. + ```agda subst-vec : (Id → Term) → ∀{n} → Vec Term n → Vec Term n @@ -845,6 +871,7 @@ subst-vec σ (M ∷ Ms) = (subst σ M) ∷ (subst-vec σ Ms) As usual, we implement single substitution using simultaneous substitution. + ```agda subst-zero : Term → Id → Term subst-zero M 0 = M @@ -861,6 +888,7 @@ In a call-by-value language, a record is usually only considered a value if all its field initializers are values. Here we instead treat records in a lazy fashion, declaring any record to be a value, to save on some extra bookkeeping. + ```agda data Value : Term → Set where @@ -954,6 +982,7 @@ As in the [Properties](/Properties/) chapter, we define a `Canonical V ⦂ A` relation that characterizes the well-typed values. The presence of the subsumption rule impacts its definition because we must allow the type of the value `V` to be a subtype of `A`. + ```agda data Canonical_⦂_ : Term → Type → Set where @@ -980,6 +1009,7 @@ data Canonical_⦂_ : Term → Type → Set where ``` Every closed, well-typed value is canonical: + ```agda canonical : ∀ {V A} → ∅ ⊢ V ⦂ A @@ -1003,6 +1033,7 @@ canonical (⊢<: ⊢V (<:-rcd {ks = ks}{ls = ls}{d2 = dls} ls⊆ks ls⦂Ss<:ks ... | C-rcd {ks = ks′} ⊢Ms dks′ As<:Ss = C-rcd {dls = distinct-relevant dls} ⊢Ms dks′ (<:-trans As<:Ss (<:-rcd ls⊆ks ls⦂Ss<:ks⦂Ts)) ``` + The case for subsumption (`⊢<:`) is interesting. We proceed by cases on the derivation of subtyping. @@ -1022,6 +1053,7 @@ cases on the derivation of subtyping. If a term is canonical, then it is also a value. + ```agda value : ∀ {M A} → Canonical M ⦂ A @@ -1034,6 +1066,7 @@ value (C-rcd _ _ _) = V-rcd ``` A canonical value is a well-typed value. + ```agda typed : ∀ {V A} → Canonical V ⦂ A @@ -1105,6 +1138,7 @@ progress (⊢# {n}{Γ}{A}{M}{l}{ls}{As}{i}{d} ⊢M ls[i]=l As[i]=A) progress (⊢rcd x d) = done V-rcd progress (⊢<: {A = A}{B} ⊢M A<:B) = progress ⊢M ``` + * Case `⊢#`: We have `Γ ⊢ M ⦂ ⦗ ls ⦂ As ⦘`, `lookup ls i ≡ l`, and `lookup As i ≡ A`. By the induction hypothesis, either `M —→ M′` or `M` is a value. In the later case we conclude that `M # l —→ M′ # l` by rule `ξ-#`. On the other hand, if `M` is a value, @@ -1132,6 +1166,7 @@ proofs of these lemmas are adapted from the intrinsic versions of the We define the following abbreviation for a *well-typed renaming* from Γ to Δ, that is, a renaming that sends variables in Γ to variables in Δ with the same type. + ```agda _⦂ᵣ_⇒_ : (Id → Id) → Context → Context → Set ρ ⦂ᵣ Γ ⇒ Δ = ∀ {x A} → Γ ∋ x ⦂ A → Δ ∋ ρ x ⦂ A @@ -1139,6 +1174,7 @@ _⦂ᵣ_⇒_ : (Id → Id) → Context → Context → Set The `ext` function takes a well-typed renaming from Γ to Δ and extends it to become a renaming from (Γ , B) to (Δ , B). + ```agda ext-pres : ∀ {Γ Δ ρ B} → ρ ⦂ᵣ Γ ⇒ Δ @@ -1151,6 +1187,7 @@ ext-pres {ρ = ρ } ρ⦂ (S {x = x} ∋x) = S (ρ⦂ ∋x) Next we prove that both `rename` and `rename-vec` preserve types. We use the `ext-pres` lemma in each of the cases with a variable binding: `⊢ƛ`, `⊢μ`, and `⊢case`. + ```agda ren-vec-pres : ∀ {Γ Δ ρ}{n}{Ms : Vec Term n}{As : Vec Type n} → ρ ⦂ᵣ Γ ⇒ Δ → Γ ⊢* Ms ⦂ As → Δ ⊢* rename-vec ρ Ms ⦂ As @@ -1180,6 +1217,7 @@ ren-vec-pres {ρ = ρ} ρ⦂ (⊢*-∷ ⊢M ⊢Ms) = A *well-typed substitution* from Γ to Δ sends variables in Γ to terms of the same type in the context Δ. + ```agda _⦂_⇒_ : (Id → Term) → Context → Context → Set σ ⦂ Γ ⇒ Δ = ∀ {A x} → Γ ∋ x ⦂ A → Δ ⊢ subst σ (` x) ⦂ A @@ -1203,6 +1241,7 @@ exts-pres {σ = σ} σ⦂ (S {x = x} ∋x) = rename-pres {ρ = suc} S (σ⦂ ∋ Now we prove that both `subst` and `subst-vec` preserve types. We use the `exts-pres` lemma in each of the cases with a variable binding: `⊢ƛ`, `⊢μ`, and `⊢case`. + ```agda subst-vec-pres : ∀ {Γ Δ σ}{n}{Ms : Vec Term n}{A} → σ ⦂ Γ ⇒ Δ → Γ ⊢* Ms ⦂ A → Δ ⊢* subst-vec σ Ms ⦂ A @@ -1232,6 +1271,7 @@ subst-vec-pres {σ = σ} σ⦂ (⊢*-∷ ⊢M ⊢Ms) = The fact that single substitution preserves types is a corollary of `subst-pres`. + ```agda substitution : ∀{Γ A B M N} → Γ ⊢ M ⦂ A @@ -1248,6 +1288,7 @@ substitution {Γ}{A}{B}{M}{N} ⊢M ⊢N = subst-pres {σ = subst-zero M} G ⊢N We require just one last lemma before we get to the proof of preservation. The following lemma establishes that field access preserves types. + ```agda field-pres : ∀{n}{As : Vec Type n}{A}{Ms : Vec Term n}{i : Fin n} → ∅ ⊢* Ms ⦂ As @@ -1256,6 +1297,7 @@ field-pres : ∀{n}{As : Vec Type n}{A}{Ms : Vec Term n}{i : Fin n} field-pres {i = zero} (⊢*-∷ ⊢M ⊢Ms) refl = ⊢M field-pres {i = suc i} (⊢*-∷ ⊢M ⊢Ms) As[i]=A = field-pres ⊢Ms As[i]=A ``` + The proof is by induction on the typing derivation. * Case `⊢-*-[]`: This case yields a contradiction because `Fin 0` is uninhabitable. @@ -1270,6 +1312,7 @@ The proof is by induction on the typing derivation. We conclude this chapter with the proof of preservation. We discuss the cases particular to records and subtyping in the paragraph following the Agda proof. + ```agda preserve : ∀ {M N A} → ∅ ⊢ M ⦂ A @@ -1304,6 +1347,7 @@ preserve (⊢# {ls = ls}{i = i} ⊢M refl refl) (β-# {ls = ks}{Ms}{j = j} ks[j] Ms[k]⦂As[i] preserve (⊢<: ⊢M B<:A) M—→N = ⊢<: (preserve ⊢M M—→N) B<:A ``` + Recall that the proof is by induction on the derivation of `∅ ⊢ M ⦂ A` with cases on `M —→ N`. diff --git a/extra/bin-suggestion.lagda.md b/extra/bin-suggestion.lagda.md index cfc8edb9c..a00bf81e4 100644 --- a/extra/bin-suggestion.lagda.md +++ b/extra/bin-suggestion.lagda.md @@ -4,7 +4,7 @@ In the Quantifiers chapter, I found the Bin-isomorphism exercise difficult. I suggest the following variation. A canonical element is an element (to n). Hence the alternative definition of Can. -``` +```agda data Can': Bin -> Set where tocan : {b : Bin } -> ∃[ n ] (b ≡ to n) -> Can' b ``` @@ -12,6 +12,7 @@ data Can': Bin -> Set where With this definition the proof of the property, "if b is canonical, then `to (from b) = b`" becomes much simpler. ``` + tofrom: (b: Bin) -> Can' b -> to (from b) ≡ b tofrom b (tocan ⟨ n , btn ⟩) = Eq.trans (Eq.cong (to ∘ from) btn) (Eq.trans (Eq.cong to (fromto n)) (Eq.sym btn)) diff --git a/extra/extra/Lists.lagda.md b/extra/extra/Lists.lagda.md index f4a3eac7b..b66894196 100644 --- a/extra/extra/Lists.lagda.md +++ b/extra/extra/Lists.lagda.md @@ -2,7 +2,7 @@ Show that `Any P xs` is isomorphic to `∃[ x ] (x ∈ xs × P x)`. -``` +```agda Any-∃ : ∀ {A : Set} {P : A → Set} {xs : List A} → Any P xs ≃ ∃[ x ] (x ∈ xs × P x) Any-∃ {A} {P} {xs} = record { to = to diff --git a/extra/fixpoint-old/LambdaFixpoint.lagda.md b/extra/fixpoint-old/LambdaFixpoint.lagda.md index 108577b43..fbad5b74a 100644 --- a/extra/fixpoint-old/LambdaFixpoint.lagda.md +++ b/extra/fixpoint-old/LambdaFixpoint.lagda.md @@ -4,7 +4,7 @@ layout : page permalink : /LambdaFixpoint/ --- -``` +```agda module plfa.part2.LambdaFixpoint where ``` @@ -50,7 +50,7 @@ four. ## Imports -``` +```agda open import Data.Bool using (Bool; true; false; T; not) open import Data.Empty using (⊥; ⊥-elim) open import Data.List using (List; _∷_; []) @@ -100,7 +100,8 @@ Here is the syntax of terms in Backus-Naur Form (BNF): μ f ⇒ƛ x ⇒ M And here it is formalised in Agda: -``` + +```agda Id : Set Id = String @@ -128,6 +129,7 @@ data Func where tm : Func → Term tm (ƛ x ⇒ N) = ƛ x ⇒ N ``` + We represent identifiers by strings. We choose precedence so that lambda abstraction and fixpoint bind least tightly, then application, then successor, and tightest of all is the constructor for variables. @@ -139,7 +141,8 @@ Case expressions are self-bracketing. Here are some example terms: the natural number two, a function that adds naturals, and a term that computes two plus two: -``` + +```agda two : Term two = `suc `suc `zero @@ -149,6 +152,7 @@ plus = μ "+" ⇒ ƛ "m" ⇒ ƛ "n" ⇒ [zero⇒ ` "n" |suc "m" ⇒ `suc (` "+" · ` "m" · ` "n") ] ``` + The recursive definition of addition is similar to our original definition of `_+_` for naturals, as given in Chapter [Naturals](/Naturals/#plus). @@ -170,7 +174,8 @@ second. This is called the _Church representation_ of the naturals. Here are some example terms: the Church numeral two, a function that adds Church numerals, a function to compute successor, and a term that computes two plus two: -``` + +```agda twoᶜ : Term twoᶜ = ƛ "s" ⇒ ƛ "z" ⇒ ` "s" · (` "s" · ` "z") @@ -181,6 +186,7 @@ plusᶜ = ƛ "m" ⇒ ƛ "n" ⇒ ƛ "s" ⇒ ƛ "z" ⇒ sucᶜ : Term sucᶜ = ƛ "n" ⇒ `suc (` "n") ``` + The Church numeral for two takes two arguments `s` and `z` and applies `s` twice to `z`. Addition takes two numerals `m` and `n`, a @@ -204,7 +210,7 @@ Write out the definition of a lambda term that multiplies two natural numbers. Your definition may use `plus` as defined earlier. -``` +```agda -- Your code goes here ``` @@ -216,7 +222,7 @@ two natural numbers represented as Church numerals. Your definition may use `plusᶜ` as defined earlier (or may not — there are nice definitions both ways). -``` +```agda -- Your code goes here ``` @@ -226,7 +232,8 @@ definition may use `plusᶜ` as defined earlier (or may not Some people find it annoying to write `` ` "x" `` instead of `x`. We can make examples with lambda terms slightly easier to write by adding the following definitions: -``` + +```agda var? : (t : Term) → Bool var? (` _) = true var? _ = false @@ -258,7 +265,8 @@ implicit argument. Note the implicit argument's type reduces to `⊥` when term `t` is anything but a variable. The definition of `plus` can now be written as follows: -``` + +```agda plus′ : Term plus′ = μ′ + ⇒ m ⇒ ƛ′ n ⇒ case′ m @@ -269,6 +277,7 @@ plus′ = μ′ + ⇒ m ⇒ ƛ′ n ⇒ m = ` "m" n = ` "n" ``` + Write out the definition of multiplication in the same style. @@ -367,7 +376,7 @@ as values; thus, `` plus `` by itself is considered a value. The predicate `Value M` holds if term `M` is a value: -``` +```agda data Value : Term → Set where V-ƛ : ∀ {x N} @@ -472,7 +481,7 @@ which will be adequate for our purposes. Here is the formal definition of substitution by closed terms in Agda: -``` +```agda infix 9 _[_:=_] _[_:=_] : Term → Id → Term → Term @@ -516,7 +525,7 @@ simply push substitution recursively into the subterms. Here is confirmation that the examples above are correct: -``` +```agda _ : (ƛ "z" ⇒ ` "s" · (` "s" · ` "z")) [ "s" := sucᶜ ] ≡ ƛ "z" ⇒ sucᶜ · (sucᶜ · ` "z") _ = refl @@ -554,7 +563,7 @@ Rewrite the definition to factor the common part of these three clauses into a single function, defined by mutual recursion with substitution. -``` +```agda -- Your code goes here ``` @@ -612,7 +621,7 @@ case where we substitute by a term that is not a value. Here are the rules formalised in Agda: -``` +```agda infix 4 _—→_ data _—→_ : Term → Term → Set where @@ -713,7 +722,8 @@ We define reflexive and transitive closure as a sequence of zero or more steps of the underlying relation, along lines similar to that for reasoning about chains of equalities in Chapter [Equality](/Equality/): -``` + +```agda infix 2 _—↠_ infix 1 begin_ infixr 2 _—→⟨_⟩_ @@ -736,6 +746,7 @@ begin_ : ∀ {M N} → M —↠ N begin M—↠N = M—↠N ``` + We can read this as follows: * From term `M`, we can take no steps, giving a step of type `M —↠ M`. @@ -752,7 +763,8 @@ appealing way, as we will see in the next section. An alternative is to define reflexive and transitive closure directly, as the smallest relation that includes `—→` and is also reflexive and transitive. We could do so as follows: -``` + +```agda data _—↠′_ : Term → Term → Set where step′ : ∀ {M N} @@ -770,6 +782,7 @@ data _—↠′_ : Term → Term → Set where ------- → L —↠′ N ``` + 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). @@ -779,7 +792,7 @@ the two definitions are equivalent (indeed, one embeds in the other). Show that the first notion of reflexive and transitive closure above embeds into the second. Why are they not isomorphic? -``` +```agda -- Your code goes here ``` @@ -807,7 +820,7 @@ while if the top two lines stand for a single reduction step and the bottom two stand for zero or more reduction steps it is called the diamond property. In symbols: -``` +```agda postulate confluence : ∀ {L M N} → ((L —↠ M) × (L —↠ N)) @@ -823,7 +836,7 @@ postulate The reduction system studied in this chapter is deterministic. In symbols: -``` +```agda postulate deterministic : ∀ {L M N} → L —→ M @@ -841,7 +854,8 @@ systems studied in this text are trivially confluent. We start with a simple example. The Church numeral two applied to the successor function and zero yields the natural number two: -``` + +```agda _ : twoᶜ · sucᶜ · `zero —↠ `suc `suc `zero _ = begin @@ -858,7 +872,8 @@ _ = ``` Here is a sample reduction demonstrating that two plus two is four: -``` + +```agda _ : plus · two · two —↠ `suc `suc `suc `suc `zero _ = begin @@ -903,7 +918,8 @@ _ = ``` And here is a similar sample reduction for Church numerals: -``` + +```agda _ : plusᶜ · twoᶜ · twoᶜ · sucᶜ · `zero —↠ `suc `suc `suc `suc `zero _ = begin @@ -944,7 +960,7 @@ In the next chapter, we will see how to compute such reduction sequences. Write out the reduction sequence demonstrating that one plus one is two. -``` +```agda -- Your code goes here ``` @@ -964,7 +980,7 @@ Here is the syntax of types in BNF: And here it is formalised in Agda: -``` +```agda infixr 7 _⇒_ data Type : Set where @@ -1032,7 +1048,7 @@ and variable `` "z" `` with type `` `ℕ ``. Contexts are formalised as follows: -``` +```agda infixl 5 _,_⦂_ data Context : Set where @@ -1052,7 +1068,7 @@ to the list [ ⟨ "z" , `ℕ ⟩ , ⟨ "s" , `ℕ ⇒ `ℕ ⟩ ] -``` +```agda -- Your code goes here ``` @@ -1083,7 +1099,8 @@ the other variables. For example, Here `` "x" ⦂ `ℕ ⇒ `ℕ `` is shadowed by `` "x" ⦂ `ℕ ``. Lookup is formalised as follows: -``` + +```agda infix 4 _∋_⦂_ data _∋_⦂_ : Context → Id → Type → Set where @@ -1108,14 +1125,14 @@ variable with the same name to its left in the list. It can be rather tedious to use the `S` constructor, as you have to provide proofs that `x ≢ y` each time. For example: -``` +```agda _ : ∅ , "x" ⦂ `ℕ ⇒ `ℕ , "y" ⦂ `ℕ , "z" ⦂ `ℕ ∋ "x" ⦂ `ℕ ⇒ `ℕ _ = S (λ()) (S (λ()) Z) ``` Instead, we'll use a "smart constructor", which uses [proof by reflection](/Decidable/#proof-by-reflection) to check the inequality while type checking: -``` +```agda S′ : ∀ {Γ x y A B} → {x≢y : False (x ≟ y)} → Γ ∋ x ⦂ A @@ -1143,7 +1160,8 @@ For example: * `` ∅ ⊢ ƛ "s" ⇒ ƛ "z" ⇒ ` "s" · (` "s" · ` "z") ⦂ (`ℕ ⇒ `ℕ) ⇒ `ℕ ⇒ `ℕ `` Typing is formalised as follows: -``` + +```agda infix 4 _⊢_⦂_ infix 4 _⊢ᶠ_⦂_ @@ -1230,7 +1248,7 @@ As a simple consequence, we have that if a recursive term is well-typed then it has a function type, and hence cannot have type ` `ℕ `. -``` +```agda μ-type : ∀ {Γ f F A} → Γ ⊢ μ f ⇒ F ⦂ A ------------------------- @@ -1270,7 +1288,8 @@ The typing derivation is valid for any `Γ` and `A`, for instance, we might take `Γ` to be `∅` and `A` to be `` `ℕ ``. Here is the above typing derivation formalised in Agda: -``` + +```agda Ch : Type → Type Ch A = (A ⇒ A) ⇒ A ⇒ A @@ -1282,7 +1301,8 @@ Ch A = (A ⇒ A) ⇒ A ⇒ A ``` Here are the typings corresponding to computing two plus two: -``` + +```agda ⊢two : ∀ {Γ} → Γ ⊢ two ⦂ `ℕ ⊢two = ⊢suc (⊢suc ⊢zero) @@ -1299,6 +1319,7 @@ Here are the typings corresponding to computing two plus two: ⊢2+2 : ∅ ⊢ plus · two · two ⦂ `ℕ ⊢2+2 = ⊢plus · ⊢two · ⊢two ``` + In contrast to our earlier examples, here we have typed `two` and `plus` in an arbitrary context rather than the empty context; this makes it easy to use them inside other binding contexts as well as at the top level. @@ -1309,7 +1330,8 @@ contexts, the first where `"n"` is the last binding in the context, and the second after `"m"` is bound in the successor branch of the case. And here are typings for the remainder of the Church example: -``` + +```agda ⊢plusᶜ : ∀ {Γ A} → Γ ⊢ plusᶜ ⦂ Ch A ⇒ Ch A ⇒ Ch A ⊢plusᶜ = ⊢ƛ (⊢ƛ (⊢ƛ (⊢ƛ (⊢` ∋m · ⊢` ∋s · (⊢` ∋n · ⊢` ∋s · ⊢` ∋z))))) where @@ -1375,7 +1397,8 @@ will show how to use Agda to compute type derivations directly. The lookup relation `Γ ∋ x ⦂ A` is functional, in that for each `Γ` and `x` there is at most one `A` such that the judgment holds: -``` + +```agda ∋-functional : ∀ {Γ x A B} → Γ ∋ x ⦂ A → Γ ∋ x ⦂ B → A ≡ B ∋-functional Z Z = refl ∋-functional Z (S x≢ _) = ⊥-elim (x≢ refl) @@ -1394,7 +1417,7 @@ a formal proof that it is not possible to type the term requires that the first term in the application is both a natural and a function: -``` +```agda nope₁ : ∀ {A} → ¬ (∅ ⊢ `zero · `suc `zero ⦂ A) nope₁ (() · _) ``` @@ -1403,7 +1426,7 @@ As a second example, here is a formal proof that it is not possible to type `` ƛ "x" ⇒ ` "x" · ` "x" ``. It cannot be typed, because doing so requires types `A` and `B` such that `A ⇒ B ≡ A`: -``` +```agda nope₂ : ∀ {A} → ¬ (∅ ⊢ ƛ "x" ⇒ ` "x" · ` "x" ⦂ A) nope₂ (⊢ƛ (⊢` ∋x · ⊢` ∋x′)) = contradiction (∋-functional ∋x ∋x′) where @@ -1433,7 +1456,7 @@ or explain why there are no such types. Using the term `mul` you defined earlier, write out the derivation showing that it is well typed. -``` +```agda -- Your code goes here ``` @@ -1443,7 +1466,7 @@ showing that it is well typed. Using the term `mulᶜ` you defined earlier, write out the derivation showing that it is well typed. -``` +```agda -- Your code goes here ``` diff --git a/extra/fixpoint-old/PropertiesFixpoint.lagda.md b/extra/fixpoint-old/PropertiesFixpoint.lagda.md index 4fa2b9dc7..4fb0d5b42 100644 --- a/extra/fixpoint-old/PropertiesFixpoint.lagda.md +++ b/extra/fixpoint-old/PropertiesFixpoint.lagda.md @@ -4,7 +4,7 @@ layout : page permalink : /PropertiesFixpoint/ --- -``` +```agda module plfa.part2.PropertiesFixpoint where ``` @@ -17,7 +17,7 @@ sequences for us. ## Imports -``` +```agda open import Relation.Binary.PropositionalEquality using (_≡_; _≢_; refl; sym; cong; cong₂) open import Data.String using (String; _≟_) @@ -88,7 +88,8 @@ types without needing to develop a separate inductive definition of the ## Values do not reduce We start with an easy observation. Values do not reduce: -``` + +```agda V¬—→ : ∀ {M N} → Value M ---------- @@ -97,6 +98,7 @@ V¬—→ V-ƛ () V¬—→ V-zero () V¬—→ (V-suc VM) (ξ-suc M—→N) = V¬—→ VM M—→N ``` + We consider the three possibilities for values: * If it is an abstraction then no reduction applies @@ -108,13 +110,15 @@ We consider the three possibilities for values: that reduces, which by induction cannot occur. As a corollary, terms that reduce are not values: -``` + +```agda —→¬V : ∀ {M N} → M —→ N --------- → ¬ Value M —→¬V M—→N VM = V¬—→ VM M—→N ``` + If we expand out the negations, we have V¬—→ : ∀ {M N} → Value M → M —→ N → ⊥ @@ -132,7 +136,8 @@ and a zero or successor expression must be a natural. Further, the body of a function must be well typed in a context containing only its bound variable, and the argument of successor must itself be canonical: -``` + +```agda infix 4 Canonical_⦂_ data Canonical_⦂_ : Term → Type → Set where @@ -160,7 +165,7 @@ data Canonical_⦂_ : Term → Type → Set where Show that `Canonical V ⦂ A` is isomorphic to `(∅ ⊢ V ⦂ A) × (Value V)`, that is, the canonical forms are exactly the well-typed values. -``` +```agda -- Your code goes here ``` @@ -186,7 +191,8 @@ that `M —→ N`. To formulate this property, we first introduce a relation that captures what it means for a term `M` to make progress: -``` + +```agda data Progress (M : Term) : Set where step : ∀ {N} @@ -199,12 +205,14 @@ data Progress (M : Term) : Set where ---------- → Progress M ``` + A term `M` makes progress if either it can take a step, meaning there exists a term `N` such that `M —→ N`, or if it is done, meaning that `M` is a value. If a term is well typed in the empty context then it satisfies progress: -``` + +```agda progress : ∀ {M A} → ∅ ⊢ M ⦂ A ---------- @@ -279,10 +287,12 @@ or introduce subsidiary functions. Instead of defining a data type for `Progress M`, we could have formulated progress using disjunction and existentials: -``` + +```agda postulate progress′ : ∀ M {A} → ∅ ⊢ M ⦂ A → Value M ⊎ ∃[ N ](M —→ N) ``` + This leads to a less perspicuous proof. Instead of the mnemonic `done` and `step` we use `inj₁` and `inj₂`, and the term `N` is no longer implicit and so must be written out in full. In the case for `β-ƛ` @@ -294,7 +304,7 @@ determine its bound variable and body, `ƛ x ⇒ N`, so we can show that Show that `Progress M` is isomorphic to `Value M ⊎ ∃[ N ](M —→ N)`. -``` +```agda -- Your code goes here ``` @@ -303,7 +313,7 @@ Show that `Progress M` is isomorphic to `Value M ⊎ ∃[ N ](M —→ N)`. Write out the proof of `progress′` in full, and compare it to the proof of `progress` above. -``` +```agda -- Your code goes here ``` @@ -311,7 +321,8 @@ proof of `progress` above. Combine `progress` and `—→¬V` to write a program that decides whether a well-typed term is a value: -``` + +```agda postulate value? : ∀ {A M} → ∅ ⊢ M ⦂ A → Dec (Value M) ``` @@ -393,7 +404,8 @@ We often need to "rebase" a type derivation, replacing a derivation as every variable that appears in `Γ` also appears in `Δ`, and with the same type. To begin, we define renaming and term maps between contexts as follows. -``` + +```agda infix 4 _→ᴿ_ infix 4 _→ᵀ_ @@ -417,7 +429,8 @@ for lambda expressions, and similarly for case and fixpoint. To deal with this situation, we first prove a lemma showing that if one context maps to another, this is still true after adding the same variable to both contexts: -``` + +```agda ext : ∀ {Γ Δ y B} → Γ →ᴿ Δ ---------------------- @@ -425,6 +438,7 @@ ext : ∀ {Γ Δ y B} ext ρ Z = Z ext ρ (S x≢y ∋x) = S x≢y (ρ ∋x) ``` + Let `ρ` be the name of the map that takes evidence that `x` appears in `Γ` to evidence that `x` appears in `Δ`. The proof is by case analysis of the evidence that `x` appears @@ -442,7 +456,8 @@ applying `ρ` to find the evidence that `x` appears in `Δ`. With the extension lemma under our belts, it is straightforward to prove renaming preserves types: -``` + +```agda rename : ∀ {Γ Δ} → Γ →ᴿ Δ ------ @@ -455,6 +470,7 @@ rename ρ (⊢suc ⊢M) = ⊢suc (rename ρ ⊢M) rename ρ (⊢case ⊢L ⊢M ⊢N) = ⊢case (rename ρ ⊢L) (rename ρ ⊢M) (rename (ext ρ) ⊢N) rename ρ (⊢μ (⊢ƛ ⊢N)) = ⊢μ (⊢ƛ (rename (ext (ext ρ)) ⊢N)) ``` + As before, let `ρ` be the name of the map that takes evidence that `x` appears in `Γ` to evidence that `x` appears in `Δ`. We induct on the evidence that `M` is well typed in `Γ`. Let's unpack the @@ -483,7 +499,8 @@ We have three important corollaries, each proved by constructing a suitable map between contexts. First, a closed term can be weakened to any context: -``` + +```agda weaken-ρ : ∀ {Γ} ------ → ∅ →ᴿ Γ @@ -494,12 +511,14 @@ weaken : ∀ {Γ} → ∅ →ᵀ Γ weaken = rename weaken-ρ ``` + Here the map `ρ` is trivial, since there are no possible arguments in the empty context `∅`. Second, if the last two variables in a context are equal then we can drop the shadowed one: -``` + +```agda drop-ρ : ∀ {Γ x A B} ------------------------------ → Γ , x ⦂ A , x ⦂ B →ᴿ Γ , x ⦂ B @@ -512,6 +531,7 @@ drop : ∀ {Γ x A B} → Γ , x ⦂ A , x ⦂ B →ᵀ Γ , x ⦂ B drop = rename drop-ρ ``` + Here map `drop-ρ` can never be invoked on the inner occurrence of `x` since it is masked by the outer occurrence. Skipping over the `x` in the first position can only happen if the variable looked for differs from @@ -520,7 +540,8 @@ found in the second position, which also contains `x`, this leads to a contradiction (evidenced by `x≢x refl`). Third, if the last two variables in a context differ then we can swap them: -``` + +```agda swap-ρ : ∀ {Γ x y A B} → x ≢ y -------------------------------------- @@ -535,6 +556,7 @@ swap : ∀ {Γ x y A B} → Γ , y ⦂ B , x ⦂ A →ᵀ Γ , x ⦂ A , y ⦂ B swap x≢y = rename (swap-ρ x≢y) ``` + Here the renaming map takes a variable at the end into a variable one from the end, and vice versa. The first line is responsible for moving `x` from a position at the end to a position one from the end @@ -543,7 +565,8 @@ with `y` at the end, and requires the provided evidence that `x ≢ y`. We also require a few additional variants, to deal with substitution inside fixpoints. -``` + +```agda drop2-ρ : ∀ {Γ x f A B C} ---------------------------------------------- → Γ , x ⦂ A , f ⦂ B , x ⦂ C →ᴿ Γ , f ⦂ B , x ⦂ C @@ -583,7 +606,8 @@ variables the context grows. So for the induction to go through, we require an arbitrary context `Γ`, as in the statement of the lemma. Here is the formal statement and proof that substitution preserves types: -``` + +```agda subst : ∀ {Γ x N V A B} → ∅ ⊢ V ⦂ A → Γ , x ⦂ A ⊢ N ⦂ B @@ -609,6 +633,7 @@ subst {x = y} ⊢V (⊢μ {f = f} (⊢ƛ {x = x} ⊢N)) with f ≟ y | x ≟ y ... | no f≢y | yes refl = ⊢μ (⊢ƛ (rename drop2-ρ ⊢N)) ... | no f≢y | no x≢y = ⊢μ (⊢ƛ (subst ⊢V (rename (swap2-ρ f≢y x≢y) ⊢N))) ``` + We induct on the evidence that `N` is well typed in the context `Γ` extended by `x`. @@ -778,7 +803,7 @@ should factor dealing with bound variables into a single function, defined by mutual recursion with the proof that substitution preserves types. -``` +```agda -- Your code goes here ``` @@ -788,7 +813,7 @@ preserves types. Once we have shown that substitution preserves types, showing that reduction preserves types is straightforward: -``` +```agda preserve : ∀ {M N A} → ∅ ⊢ M ⦂ A → M —→ N @@ -806,6 +831,7 @@ preserve (⊢case ⊢zero ⊢M ⊢N) (β-zero) = ⊢M preserve (⊢case (⊢suc ⊢V) ⊢M ⊢N) (β-suc VV) = subst ⊢V ⊢N preserve ((⊢μ (⊢ƛ ⊢N)) · ⊢V) (β-μ VV) = subst (⊢μ (⊢ƛ ⊢N)) (⊢ƛ ⊢N) · ⊢V ``` + The proof never mentions the types of `M` or `N`, so in what follows we choose type names as convenient. @@ -868,7 +894,8 @@ function that computes the reduction sequence from any given closed, well-typed term to its value, if it has one. Some terms may reduce forever. Here is a simple example: -``` + +```agda loop = μ "f" ⇒ ƛ "x" ⇒ (` "f") · (` "x") _ = @@ -885,6 +912,7 @@ _ = -- ... ∎ ``` + Since every Agda computation must terminate, we cannot simply ask Agda to reduce a term to a value. Instead, we will provide a natural number to Agda, and permit it @@ -906,15 +934,18 @@ per unit of gas. By analogy, we will use the name _gas_ for the parameter which puts a bound on the number of reduction steps. `Gas` is specified by a natural number: -``` + +```agda record Gas : Set where constructor gas field amount : ℕ ``` + When our evaluator returns a term `N`, it will either give evidence that `N` is a value or indicate that it ran out of gas: -``` + +```agda data Finished (N : Term) : Set where done : @@ -926,10 +957,12 @@ data Finished (N : Term) : Set where ---------- Finished N ``` + Given a term `L` of type `A`, the evaluator will, for some `N`, return a reduction sequence from `L` to `N` and an indication of whether reduction finished: -``` + +```agda data Steps (L : Term) : Set where steps : ∀ {N} @@ -938,9 +971,11 @@ data Steps (L : Term) : Set where ---------- → Steps L ``` + The evaluator takes gas and evidence that a term is well typed, and returns the corresponding steps: -``` + +```agda eval : ∀ {L A} → Gas → ∅ ⊢ L ⦂ A @@ -952,6 +987,7 @@ eval {L} (gas (suc m)) ⊢L with progress ⊢L ... | step {M} L—→M with eval (gas m) (preserve ⊢L L—→M) ... | steps M—↠N fin = steps (L —→⟨ L—→M ⟩ M—↠N) fin ``` + Let `L` be the name of the term we are reducing, and `⊢L` be the evidence that `L` is well typed. We consider the amount of gas remaining. There are two possibilities: @@ -982,13 +1018,16 @@ remaining. There are two possibilities: We can now use Agda to compute the non-terminating reduction sequence given earlier. First, we show that the term `loop` is well-typed. -``` + +```agda ⊢loop : ∀ (A : Type) → ∅ ⊢ loop ⦂ `ℕ ⇒ A ⊢loop A = ⊢μ (⊢ƛ ((⊢` (S (λ()) Z)) · (⊢` Z))) ``` + To show the first four steps of the infinite reduction sequence, we evaluate with four steps worth of gas: -``` + +```agda _ : eval (gas 4) (⊢loop `ℕ · ⊢zero) ≡ steps ( @@ -1005,6 +1044,7 @@ _ : eval (gas 4) (⊢loop `ℕ · ⊢zero) ≡ out-of-gas _ = refl ``` + The example above was generated by using `C-c C-n` to normalise the left-hand side of the equation and pasting in the result as the right-hand side of the equation. @@ -1012,7 +1052,8 @@ right-hand side of the equation. Similarly, we can use Agda to compute the reduction sequences given in the previous chapter. We start with the Church numeral two applied to successor and zero. Supplying 100 steps of gas is more than enough: -``` + +```agda _ : eval (gas 100) (⊢twoᶜ · ⊢sucᶜ · ⊢zero) ≡ steps ( @@ -1029,6 +1070,7 @@ _ : eval (gas 100) (⊢twoᶜ · ⊢sucᶜ · ⊢zero) ≡ (done (V-suc (V-suc V-zero))) _ = refl ``` + Again, the example above was generated by using `C-c C-n` to normalise the left-hand side of the equation and pasting in the result as the right-hand side of the equation. The example reduction of the @@ -1036,7 +1078,8 @@ previous chapter was derived from this result, reformatting and writing `twoᶜ` and `sucᶜ` in place of their expansions. Next, we show two plus two is four: -``` + +```agda _ : eval (gas 100) ⊢2+2 ≡ steps ((μ "+" ⇒ @@ -1197,11 +1240,13 @@ _ : eval (gas 100) ⊢2+2 ≡ (done (V-suc (V-suc (V-suc (V-suc V-zero))))) _ = refl ``` + Again, the derivation in the previous chapter was derived by editing the above. Similarly, we can evaluate the corresponding term for Church numerals: -``` + +```agda _ : eval (gas 100) ⊢2+2ᶜ ≡ steps ((ƛ "m" ⇒ @@ -1266,6 +1311,7 @@ _ : eval (gas 100) ⊢2+2ᶜ ≡ (done (V-suc (V-suc (V-suc (V-suc V-zero))))) _ = refl ``` + And again, the example in the previous section was derived by editing the above. @@ -1273,7 +1319,7 @@ above. Using the evaluator, confirm that two times two is four. -``` +```agda -- Your code goes here ``` @@ -1283,7 +1329,7 @@ Using the evaluator, confirm that two times two is four. Without peeking at their statements above, write down the progress and preservation theorems for the simply typed lambda-calculus. -``` +```agda -- Your code goes here ``` @@ -1299,7 +1345,7 @@ Its opposite is _subject expansion_, which holds if Find two counter-examples to subject expansion, one with case expressions and one not involving case expressions. -``` +```agda -- Your code goes here ``` @@ -1307,19 +1353,22 @@ with case expressions and one not involving case expressions. ## Well-typed terms don't get stuck A term is _normal_ if it cannot reduce: -``` + +```agda Normal : Term → Set Normal M = ∀ {N} → ¬ (M —→ N) ``` A term is _stuck_ if it is normal yet not a value: -``` + +```agda Stuck : Term → Set Stuck M = Normal M × ¬ Value M ``` Using progress, it is easy to show that no well-typed term is stuck: -``` + +```agda postulate unstuck : ∀ {M A} → ∅ ⊢ M ⦂ A @@ -1329,7 +1378,8 @@ postulate Using preservation, it is easy to show that after any number of steps, a well-typed term remains well typed: -``` + +```agda postulate preserves : ∀ {M N A} → ∅ ⊢ M ⦂ A @@ -1340,7 +1390,8 @@ postulate An easy consequence is that starting from a well-typed term, taking any number of reduction steps leads to a term that is not stuck: -``` + +```agda postulate wttdgs : ∀ {M N A} → ∅ ⊢ M ⦂ A @@ -1348,6 +1399,7 @@ postulate ----------- → ¬ (Stuck N) ``` + Felleisen and Wright, who introduced proofs via progress and preservation, summarised this result with the slogan _well-typed terms don't get stuck_. (They were referring to earlier work by Robin @@ -1359,7 +1411,7 @@ showed _well-typed terms don't go wrong_.) Give an example of an ill-typed term that does get stuck. -``` +```agda -- Your code goes here ``` @@ -1367,7 +1419,7 @@ Give an example of an ill-typed term that does get stuck. Provide proofs of the three postulates, `unstuck`, `preserves`, and `wttdgs` above. -``` +```agda -- Your code goes here ``` @@ -1380,7 +1432,8 @@ Our proof will need a variant of congruence to deal with functions of four arguments (to deal with `case_[zero⇒_|suc_⇒_]`). It is exactly analogous to `cong` and `cong₂` as defined previously: -``` + +```agda cong₄ : ∀ {A B C D E : Set} (f : A → B → C → D → E) {s w : A} {t x : B} {u y : C} {v z : D} → s ≡ w → t ≡ x → u ≡ y → v ≡ z → f s t u v ≡ f w x y z @@ -1388,7 +1441,8 @@ cong₄ f refl refl refl refl = refl ``` It is now straightforward to show that reduction is deterministic: -``` + +```agda det : ∀ {M M′ M″} → (M —→ M′) → (M —→ M″) @@ -1418,6 +1472,7 @@ det β-zero β-zero = refl det (β-suc VL) (ξ-case L—→L″) = ⊥-elim (V¬—→ (V-suc VL) L—→L″) det (β-suc _) (β-suc _) = refl ``` + The proof is by induction over possible reductions. We consider three typical cases: diff --git a/extra/fixpoint/Lambda.lagda.md b/extra/fixpoint/Lambda.lagda.md index 1658f438a..46b77b190 100644 --- a/extra/fixpoint/Lambda.lagda.md +++ b/extra/fixpoint/Lambda.lagda.md @@ -4,7 +4,7 @@ layout : page permalink : /LambdaFixpoint/ --- -``` +```agda module plfa.part2.fixpoint.Lambda where ``` @@ -50,7 +50,7 @@ four. ## Imports -``` +```agda open import Data.Bool using (Bool; true; false; T; not) open import Data.Empty using (⊥; ⊥-elim) open import Data.List using (List; _∷_; []) @@ -100,7 +100,8 @@ Here is the syntax of terms in Backus-Naur Form (BNF): μ f ⇒ ƛ x ⇒ M And here it is formalised in Agda: -``` + +```agda Id : Set Id = String @@ -133,6 +134,7 @@ data Suc where data Func where ƛ_⇒_ : Id → Term → Func ``` + We represent identifiers by strings. We choose precedence so that lambda abstraction and fixpoint bind least tightly, then application, then successor, and tightest of all is the constructor for variables. @@ -144,7 +146,8 @@ Case expressions are self-bracketing. Here are some example terms: the natural number two, a function that adds naturals, and a term that computes two plus two: -``` + +```agda two : Term two = `suc `suc `zero @@ -154,6 +157,7 @@ plus = μ "+" ⇒ ƛ "m" ⇒ ƛ "n" ⇒ [ `zero ⇒ ` "n" ∥ `suc "m" ⇒ `suc (` "+" · ` "m" · ` "n") ] ``` + The recursive definition of addition is similar to our original definition of `_+_` for naturals, as given in Chapter [Naturals](/Naturals/#plus). @@ -175,7 +179,8 @@ second. This is called the _Church representation_ of the naturals. Here are some example terms: the Church numeral two, a function that adds Church numerals, a function to compute successor, and a term that computes two plus two: -``` + +```agda twoᶜ : Term twoᶜ = ƛ "s" ⇒ ƛ "z" ⇒ ` "s" · (` "s" · ` "z") @@ -186,6 +191,7 @@ plusᶜ = ƛ "m" ⇒ ƛ "n" ⇒ ƛ "s" ⇒ ƛ "z" ⇒ sucᶜ : Term sucᶜ = ƛ "n" ⇒ `suc (` "n") ``` + The Church numeral for two takes two arguments `s` and `z` and applies `s` twice to `z`. Addition takes two numerals `m` and `n`, a @@ -209,7 +215,7 @@ Write out the definition of a lambda term that multiplies two natural numbers. Your definition may use `plus` as defined earlier. -``` +```agda -- Your code goes here ``` @@ -221,7 +227,7 @@ two natural numbers represented as Church numerals. Your definition may use `plusᶜ` as defined earlier (or may not — there are nice definitions both ways). -``` +```agda -- Your code goes here ``` @@ -231,7 +237,8 @@ definition may use `plusᶜ` as defined earlier (or may not Some people find it annoying to write `` ` "x" `` instead of `x`. We can make examples with lambda terms slightly easier to write by adding the following definitions: -``` + +```agda var? : (t : Term) → Bool var? (` _) = true var? _ = false @@ -266,7 +273,8 @@ implicit argument. Note the implicit argument's type reduces to `⊥` when term `t` is anything but a variable. The definition of `plus` can now be written as follows: -``` + +```agda plus′ : Term plus′ = μ′ + ⇒ m ⇒ ƛ′ n ⇒ case′ m @@ -277,6 +285,7 @@ plus′ = μ′ + ⇒ m ⇒ ƛ′ n ⇒ m = ` "m" n = ` "n" ``` + Write out the definition of multiplication in the same style. @@ -375,7 +384,7 @@ as values; thus, `` plus `` by itself is considered a value. The predicate `Value M` holds if term `M` is a value: -``` +```agda data Value : Term → Set where V-ƛ : ∀ {x N} @@ -480,7 +489,7 @@ which will be adequate for our purposes. Here is the formal definition of substitution by closed terms in Agda: -``` +```agda infix 9 _[_:=_] _[_:=_] : Term → Id → Term → Term @@ -524,7 +533,7 @@ simply push substitution recursively into the subterms. Here is confirmation that the examples above are correct: -``` +```agda _ : (ƛ "z" ⇒ ` "s" · (` "s" · ` "z")) [ "s" := sucᶜ ] ≡ ƛ "z" ⇒ sucᶜ · (sucᶜ · ` "z") _ = refl @@ -562,7 +571,7 @@ Rewrite the definition to factor the common part of these three clauses into a single function, defined by mutual recursion with substitution. -``` +```agda -- Your code goes here ``` @@ -620,7 +629,7 @@ case where we substitute by a term that is not a value. Here are the rules formalised in Agda: -``` +```agda infix 4 _—→_ data _—→_ : Term → Term → Set where @@ -721,7 +730,8 @@ We define reflexive and transitive closure as a sequence of zero or more steps of the underlying relation, along lines similar to that for reasoning about chains of equalities in Chapter [Equality](/Equality/): -``` + +```agda infix 2 _—↠_ infix 1 begin_ infixr 2 _—→⟨_⟩_ @@ -744,6 +754,7 @@ begin_ : ∀ {M N} → M —↠ N begin M—↠N = M—↠N ``` + We can read this as follows: * From term `M`, we can take no steps, giving a step of type `M —↠ M`. @@ -760,7 +771,8 @@ appealing way, as we will see in the next section. An alternative is to define reflexive and transitive closure directly, as the smallest relation that includes `—→` and is also reflexive and transitive. We could do so as follows: -``` + +```agda data _—↠′_ : Term → Term → Set where step′ : ∀ {M N} @@ -778,6 +790,7 @@ data _—↠′_ : Term → Term → Set where ------- → L —↠′ N ``` + 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). @@ -787,7 +800,7 @@ the two definitions are equivalent (indeed, one embeds in the other). Show that the first notion of reflexive and transitive closure above embeds into the second. Why are they not isomorphic? -``` +```agda -- Your code goes here ``` @@ -815,7 +828,7 @@ while if the top two lines stand for a single reduction step and the bottom two stand for zero or more reduction steps it is called the diamond property. In symbols: -``` +```agda postulate confluence : ∀ {L M N} → ((L —↠ M) × (L —↠ N)) @@ -831,7 +844,7 @@ postulate The reduction system studied in this chapter is deterministic. In symbols: -``` +```agda postulate deterministic : ∀ {L M N} → L —→ M @@ -849,7 +862,8 @@ systems studied in this text are trivially confluent. We start with a simple example. The Church numeral two applied to the successor function and zero yields the natural number two: -``` + +```agda _ : twoᶜ · sucᶜ · `zero —↠ `suc `suc `zero _ = begin @@ -866,7 +880,8 @@ _ = ``` Here is a sample reduction demonstrating that two plus two is four: -``` + +```agda _ : plus · two · two —↠ `suc `suc `suc `suc `zero _ = begin @@ -911,7 +926,8 @@ _ = ``` And here is a similar sample reduction for Church numerals: -``` + +```agda _ : plusᶜ · twoᶜ · twoᶜ · sucᶜ · `zero —↠ `suc `suc `suc `suc `zero _ = begin @@ -952,7 +968,7 @@ In the next chapter, we will see how to compute such reduction sequences. Write out the reduction sequence demonstrating that one plus one is two. -``` +```agda -- Your code goes here ``` @@ -972,7 +988,7 @@ Here is the syntax of types in BNF: And here it is formalised in Agda: -``` +```agda infixr 7 _⇒_ data Type : Set where @@ -1040,7 +1056,7 @@ and variable `` "z" `` with type `` `ℕ ``. Contexts are formalised as follows: -``` +```agda infixl 5 _,_⦂_ data Context : Set where @@ -1060,7 +1076,7 @@ to the list [ ⟨ "z" , `ℕ ⟩ , ⟨ "s" , `ℕ ⇒ `ℕ ⟩ ] -``` +```agda -- Your code goes here ``` @@ -1091,7 +1107,8 @@ the other variables. For example, Here `` "x" ⦂ `ℕ ⇒ `ℕ `` is shadowed by `` "x" ⦂ `ℕ ``. Lookup is formalised as follows: -``` + +```agda infix 4 _∋_⦂_ data _∋_⦂_ : Context → Id → Type → Set where @@ -1116,14 +1133,14 @@ variable with the same name to its left in the list. It can be rather tedious to use the `S` constructor, as you have to provide proofs that `x ≢ y` each time. For example: -``` +```agda _ : ∅ , "x" ⦂ `ℕ ⇒ `ℕ , "y" ⦂ `ℕ , "z" ⦂ `ℕ ∋ "x" ⦂ `ℕ ⇒ `ℕ _ = S (λ()) (S (λ()) Z) ``` Instead, we'll use a "smart constructor", which uses [proof by reflection](/Decidable/#proof-by-reflection) to check the inequality while type checking: -``` +```agda S′ : ∀ {Γ x y A B} → {x≢y : False (x ≟ y)} → Γ ∋ x ⦂ A @@ -1151,7 +1168,8 @@ For example: * `` ∅ ⊢ ƛ "s" ⇒ ƛ "z" ⇒ ` "s" · (` "s" · ` "z") ⦂ (`ℕ ⇒ `ℕ) ⇒ `ℕ ⇒ `ℕ `` Typing is formalised as follows: -``` + +```agda infix 4 _⊢_⦂_ infix 4 _⊢ᶠ_⦂_ @@ -1263,7 +1281,8 @@ The typing derivation is valid for any `Γ` and `A`, for instance, we might take `Γ` to be `∅` and `A` to be `` `ℕ ``. Here is the above typing derivation formalised in Agda: -``` + +```agda Ch : Type → Type Ch A = (A ⇒ A) ⇒ A ⇒ A @@ -1275,7 +1294,8 @@ Ch A = (A ⇒ A) ⇒ A ⇒ A ``` Here are the typings corresponding to computing two plus two: -``` + +```agda ⊢two : ∀ {Γ} → Γ ⊢ two ⦂ `ℕ ⊢two = ⊢suc (⊢suc ⊢zero) @@ -1292,6 +1312,7 @@ Here are the typings corresponding to computing two plus two: ⊢2+2 : ∅ ⊢ plus · two · two ⦂ `ℕ ⊢2+2 = ⊢plus · ⊢two · ⊢two ``` + In contrast to our earlier examples, here we have typed `two` and `plus` in an arbitrary context rather than the empty context; this makes it easy to use them inside other binding contexts as well as at the top level. @@ -1302,7 +1323,8 @@ contexts, the first where `"n"` is the last binding in the context, and the second after `"m"` is bound in the successor branch of the case. And here are typings for the remainder of the Church example: -``` + +```agda ⊢plusᶜ : ∀ {Γ A} → Γ ⊢ plusᶜ ⦂ Ch A ⇒ Ch A ⇒ Ch A ⊢plusᶜ = ⊢ƛ (⊢ƛ (⊢ƛ (⊢ƛ (⊢` ∋m · ⊢` ∋s · (⊢` ∋n · ⊢` ∋s · ⊢` ∋z))))) where @@ -1368,7 +1390,8 @@ will show how to use Agda to compute type derivations directly. The lookup relation `Γ ∋ x ⦂ A` is functional, in that for each `Γ` and `x` there is at most one `A` such that the judgment holds: -``` + +```agda ∋-functional : ∀ {Γ x A B} → Γ ∋ x ⦂ A → Γ ∋ x ⦂ B → A ≡ B ∋-functional Z Z = refl ∋-functional Z (S x≢ _) = ⊥-elim (x≢ refl) @@ -1387,7 +1410,7 @@ a formal proof that it is not possible to type the term requires that the first term in the application is both a natural and a function: -``` +```agda nope₁ : ∀ {A} → ¬ (∅ ⊢ `zero · `suc `zero ⦂ A) nope₁ (() · _) ``` @@ -1396,7 +1419,7 @@ As a second example, here is a formal proof that it is not possible to type `` ƛ "x" ⇒ ` "x" · ` "x" ``. It cannot be typed, because doing so requires types `A` and `B` such that `A ⇒ B ≡ A`: -``` +```agda nope₂ : ∀ {A} → ¬ (∅ ⊢ ƛ "x" ⇒ ` "x" · ` "x" ⦂ A) nope₂ (⊢ƛ (⊢` ∋x · ⊢` ∋x′)) = contradiction (∋-functional ∋x ∋x′) where @@ -1426,7 +1449,7 @@ or explain why there are no such types. Using the term `mul` you defined earlier, write out the derivation showing that it is well typed. -``` +```agda -- Your code goes here ``` @@ -1436,7 +1459,7 @@ showing that it is well typed. Using the term `mulᶜ` you defined earlier, write out the derivation showing that it is well typed. -``` +```agda -- Your code goes here ``` diff --git a/extra/fixpoint/Properties.lagda.md b/extra/fixpoint/Properties.lagda.md index b87df953f..41bac03d0 100644 --- a/extra/fixpoint/Properties.lagda.md +++ b/extra/fixpoint/Properties.lagda.md @@ -4,7 +4,7 @@ layout : page permalink : /PropertiesFixpoint/ --- -``` +```agda module plfa.part2.fixpoint.Properties where ``` @@ -17,7 +17,7 @@ sequences for us. ## Imports -``` +```agda open import Relation.Binary.PropositionalEquality using (_≡_; _≢_; refl; sym; cong; cong₂) open import Data.String using (String; _≟_) @@ -88,7 +88,8 @@ types without needing to develop a separate inductive definition of the ## Values do not reduce We start with an easy observation. Values do not reduce: -``` + +```agda V—↛ : ∀ {M N} → Value M ---------- @@ -98,6 +99,7 @@ V—↛ V-zero () V—↛ (V-suc VM) (ξ-suc M—→N) = V—↛ VM M—→N V—↛ V-μ () ``` + We consider the three possibilities for values: * If it is an abstraction then no reduction applies @@ -109,13 +111,15 @@ We consider the three possibilities for values: that reduces, which by induction cannot occur. As a corollary, terms that reduce are not values: -``` + +```agda —→¬V : ∀ {M N} → M —→ N --------- → ¬ Value M —→¬V M—→N VM = V—↛ VM M—→N ``` + If we expand out the negations, we have V—↛ : ∀ {M N} → Value M → M —→ N → ⊥ @@ -133,7 +137,8 @@ and a zero or successor expression must be a natural. Further, the body of a function must be well typed in a context containing only its bound variable, and the argument of successor must itself be canonical: -``` + +```agda infix 4 Canonical_⦂_ data Canonical_⦂_ : Term → Type → Set where @@ -161,7 +166,7 @@ data Canonical_⦂_ : Term → Type → Set where Show that `Canonical V ⦂ A` is isomorphic to `(∅ ⊢ V ⦂ A) × (Value V)`, that is, the canonical forms are exactly the well-typed values. -``` +```agda -- Your code goes here ``` @@ -187,7 +192,8 @@ that `M —→ N`. To formulate this property, we first introduce a relation that captures what it means for a term `M` to make progress: -``` + +```agda data Progress (M : Term) : Set where step : ∀ {N} @@ -200,12 +206,14 @@ data Progress (M : Term) : Set where ---------- → Progress M ``` + A term `M` makes progress if either it can take a step, meaning there exists a term `N` such that `M —→ N`, or if it is done, meaning that `M` is a value. If a term is well typed in the empty context then it satisfies progress: -``` + +```agda progress : ∀ {M A} → ∅ ⊢ M ⦂ A ---------- @@ -279,10 +287,12 @@ or introduce subsidiary functions. Instead of defining a data type for `Progress M`, we could have formulated progress using disjunction and existentials: -``` + +```agda postulate progress′ : ∀ M {A} → ∅ ⊢ M ⦂ A → Value M ⊎ ∃[ N ](M —→ N) ``` + This leads to a less perspicuous proof. Instead of the mnemonic `done` and `step` we use `inj₁` and `inj₂`, and the term `N` is no longer implicit and so must be written out in full. In the case for `β-ƛ` @@ -294,7 +304,7 @@ determine its bound variable and body, `ƛ x ⇒ N`, so we can show that Show that `Progress M` is isomorphic to `Value M ⊎ ∃[ N ](M —→ N)`. -``` +```agda -- Your code goes here ``` @@ -303,7 +313,7 @@ Show that `Progress M` is isomorphic to `Value M ⊎ ∃[ N ](M —→ N)`. Write out the proof of `progress′` in full, and compare it to the proof of `progress` above. -``` +```agda -- Your code goes here ``` @@ -311,7 +321,8 @@ proof of `progress` above. Combine `progress` and `—→¬V` to write a program that decides whether a well-typed term is a value: -``` + +```agda postulate value? : ∀ {A M} → ∅ ⊢ M ⦂ A → Dec (Value M) ``` @@ -393,7 +404,8 @@ We often need to "rebase" a type derivation, replacing a derivation as every variable that appears in `Γ` also appears in `Δ`, and with the same type. To begin, we define renaming and term maps between contexts as follows. -``` + +```agda infix 4 _→ᴿ_ infix 4 _→ᵀ_ @@ -417,7 +429,8 @@ for lambda expressions, and similarly for case and fixpoint. To deal with this situation, we first prove a lemma showing that if one context maps to another, this is still true after adding the same variable to both contexts: -``` + +```agda ext : ∀ {Γ Δ y B} → Γ →ᴿ Δ ---------------------- @@ -425,6 +438,7 @@ ext : ∀ {Γ Δ y B} ext ρ Z = Z ext ρ (S x≢y ∋x) = S x≢y (ρ ∋x) ``` + Let `ρ` be the name of the map that takes evidence that `x` appears in `Γ` to evidence that `x` appears in `Δ`. The proof is by case analysis of the evidence that `x` appears @@ -442,7 +456,8 @@ applying `ρ` to find the evidence that `x` appears in `Δ`. With the extension lemma under our belts, it is straightforward to prove renaming preserves types: -``` + +```agda ren : ∀ {Γ Δ} → Γ →ᴿ Δ ------ @@ -455,6 +470,7 @@ ren ρ (⊢suc ⊢M) = ⊢suc (ren ρ ⊢M) ren ρ (⊢case ⊢L ⊢M ⊢N) = ⊢case (ren ρ ⊢L) (ren ρ ⊢M) (ren (ext ρ) ⊢N) ren ρ (⊢μ (⊢ƛ ⊢N)) = ⊢μ (⊢ƛ (ren (ext (ext ρ)) ⊢N)) ``` + As before, let `ρ` be the name of the map that takes evidence that `x` appears in `Γ` to evidence that `x` appears in `Δ`. We induct on the evidence that `M` is well typed in `Γ`. Let's unpack the @@ -483,18 +499,21 @@ We have three important corollaries, each proved by constructing a suitable map between contexts. First, a closed term can be weakened to any context: -``` + +```agda weaken : ∀ {Γ} ------ → ∅ →ᴿ Γ weaken () ``` + Here the map is trivial, since there are no possible arguments in the empty context `∅`. Second, if the last two variables in a context are equal then we can drop the shadowed one: -``` + +```agda drop : ∀ {Γ x A B} ------------------------------ → Γ , x ⦂ A , x ⦂ B →ᴿ Γ , x ⦂ B @@ -502,6 +521,7 @@ drop Z = Z drop (S x≢x Z) = ⊥-elim (x≢x refl) drop (S z≢x (S _ ∋z)) = S z≢x ∋z ``` + Here map `drop` can never be invoked on the inner occurrence of `x` since it is masked by the outer occurrence. Skipping over the `x` in the first position can only happen if the variable looked for differs from @@ -510,7 +530,8 @@ found in the second position, which also contains `x`, this leads to a contradiction (evidenced by `x≢x refl`). Third, if the last two variables in a context differ then we can swap them: -``` + +```agda swap : ∀ {Γ x y A B} → x ≢ y -------------------------------------- @@ -519,6 +540,7 @@ swap x≢y Z = S x≢y Z swap x≢y (S z≢x Z) = Z swap x≢y (S z≢x (S z≢y ∋z)) = S z≢y (S z≢x ∋z) ``` + Here the renaming map takes a variable at the end into a variable one from the end, and vice versa. The first line is responsible for moving `x` from a position at the end to a position one from the end @@ -527,7 +549,8 @@ with `y` at the end, and requires the provided evidence that `x ≢ y`. We also require a few additional variants, to deal with substitution inside fixpoints. -``` + +```agda drop2 : ∀ {Γ x f A B C} ---------------------------------------------- → Γ , x ⦂ A , f ⦂ B , x ⦂ C →ᴿ Γ , f ⦂ B , x ⦂ C @@ -567,7 +590,8 @@ variables the context grows. So for the induction to go through, we require an arbitrary context `Γ`, as in the statement of the lemma. Here is the formal statement and proof that substitution preserves types: -``` + +```agda sub : ∀ {Γ x N V A B} → ∅ ⊢ V ⦂ A → Γ , x ⦂ A ⊢ N ⦂ B @@ -593,6 +617,7 @@ sub {x = y} ⊢V (⊢μ {f = f} (⊢ƛ {x = x} ⊢N)) with f ≟ y | x ≟ y ... | no f≢y | yes refl = ⊢μ (⊢ƛ (ren drop2 ⊢N)) ... | no f≢y | no x≢y = ⊢μ (⊢ƛ (sub ⊢V (ren (swap2 f≢y x≢y) ⊢N))) ``` + We induct on the evidence that `N` is well typed in the context `Γ` extended by `x`. @@ -762,7 +787,7 @@ should factor dealing with bound variables into a single function, defined by mutual recursion with the proof that substitution preserves types. -``` +```agda -- Your code goes here ``` @@ -772,7 +797,7 @@ preserves types. Once we have shown that substitution preserves types, showing that reduction preserves types is straightforward: -``` +```agda preserve : ∀ {M N A} → ∅ ⊢ M ⦂ A → M —→ N @@ -790,6 +815,7 @@ preserve (⊢case ⊢zero ⊢M ⊢N) (β-zero) = ⊢M preserve (⊢case (⊢suc ⊢V) ⊢M ⊢N) (β-suc VV) = sub ⊢V ⊢N preserve ((⊢μ (⊢ƛ ⊢N)) · ⊢V) (β-μ VV) = sub (⊢μ (⊢ƛ ⊢N)) (⊢ƛ ⊢N) · ⊢V ``` + The proof never mentions the types of `M` or `N`, so in what follows we choose type names as convenient. @@ -852,7 +878,8 @@ function that computes the reduction sequence from any given closed, well-typed term to its value, if it has one. Some terms may reduce forever. Here is a simple example: -``` + +```agda loop = μ "f" ⇒ ƛ "x" ⇒ (` "f") · (` "x") _ = @@ -869,6 +896,7 @@ _ = -- ... ∎ ``` + Since every Agda computation must terminate, we cannot simply ask Agda to reduce a term to a value. Instead, we will provide a natural number to Agda, and permit it @@ -890,15 +918,18 @@ per unit of gas. By analogy, we will use the name _gas_ for the parameter which puts a bound on the number of reduction steps. `Gas` is specified by a natural number: -``` + +```agda record Gas : Set where constructor gas field amount : ℕ ``` + When our evaluator returns a term `N`, it will either give evidence that `N` is a value or indicate that it ran out of gas: -``` + +```agda data Finished (N : Term) : Set where done : @@ -910,10 +941,12 @@ data Finished (N : Term) : Set where ---------- Finished N ``` + Given a term `L` of type `A`, the evaluator will, for some `N`, return a reduction sequence from `L` to `N` and an indication of whether reduction finished: -``` + +```agda data Steps (L : Term) : Set where steps : ∀ {N} @@ -922,9 +955,11 @@ data Steps (L : Term) : Set where ---------- → Steps L ``` + The evaluator takes gas and evidence that a term is well typed, and returns the corresponding steps: -``` + +```agda eval : ∀ {L A} → Gas → ∅ ⊢ L ⦂ A @@ -936,6 +971,7 @@ eval {L} (gas (suc m)) ⊢L with progress ⊢L ... | step {M} L—→M with eval (gas m) (preserve ⊢L L—→M) ... | steps M—↠N fin = steps (L —→⟨ L—→M ⟩ M—↠N) fin ``` + Let `L` be the name of the term we are reducing, and `⊢L` be the evidence that `L` is well typed. We consider the amount of gas remaining. There are two possibilities: @@ -966,13 +1002,16 @@ remaining. There are two possibilities: We can now use Agda to compute the non-terminating reduction sequence given earlier. First, we show that the term `loop` is well-typed. -``` + +```agda ⊢loop : ∀ (A : Type) → ∅ ⊢ loop ⦂ `ℕ ⇒ A ⊢loop A = ⊢μ (⊢ƛ ((⊢` (S (λ()) Z)) · (⊢` Z))) ``` + To show the first four steps of the infinite reduction sequence, we evaluate with four steps worth of gas: -``` + +```agda _ : eval (gas 4) (⊢loop `ℕ · ⊢zero) ≡ steps ( @@ -989,6 +1028,7 @@ _ : eval (gas 4) (⊢loop `ℕ · ⊢zero) ≡ out-of-gas _ = refl ``` + The example above was generated by using `C-c C-n` to normalise the left-hand side of the equation and pasting in the result as the right-hand side of the equation. @@ -996,7 +1036,8 @@ right-hand side of the equation. Similarly, we can use Agda to compute the reduction sequences given in the previous chapter. We start with the Church numeral two applied to successor and zero. Supplying 100 steps of gas is more than enough: -``` + +```agda _ : eval (gas 100) (⊢twoᶜ · ⊢sucᶜ · ⊢zero) ≡ steps ( @@ -1013,6 +1054,7 @@ _ : eval (gas 100) (⊢twoᶜ · ⊢sucᶜ · ⊢zero) ≡ (done (V-suc (V-suc V-zero))) _ = refl ``` + Again, the example above was generated by using `C-c C-n` to normalise the left-hand side of the equation and pasting in the result as the right-hand side of the equation. The example reduction of the @@ -1020,7 +1062,8 @@ previous chapter was derived from this result, reformatting and writing `twoᶜ` and `sucᶜ` in place of their expansions. Next, we show two plus two is four: -``` + +```agda _ : eval (gas 100) ⊢2+2 ≡ steps ((μ "+" ⇒ @@ -1181,11 +1224,13 @@ _ : eval (gas 100) ⊢2+2 ≡ (done (V-suc (V-suc (V-suc (V-suc V-zero))))) _ = refl ``` + Again, the derivation in the previous chapter was derived by editing the above. Similarly, we can evaluate the corresponding term for Church numerals: -``` + +```agda _ : eval (gas 100) ⊢2+2ᶜ ≡ steps ((ƛ "m" ⇒ @@ -1250,6 +1295,7 @@ _ : eval (gas 100) ⊢2+2ᶜ ≡ (done (V-suc (V-suc (V-suc (V-suc V-zero))))) _ = refl ``` + And again, the example in the previous section was derived by editing the above. @@ -1257,7 +1303,7 @@ above. Using the evaluator, confirm that two times two is four. -``` +```agda -- Your code goes here ``` @@ -1267,7 +1313,7 @@ Using the evaluator, confirm that two times two is four. Without peeking at their statements above, write down the progress and preservation theorems for the simply typed lambda-calculus. -``` +```agda -- Your code goes here ``` @@ -1283,7 +1329,7 @@ Its opposite is _subject expansion_, which holds if Find two counter-examples to subject expansion, one with case expressions and one not involving case expressions. -``` +```agda -- Your code goes here ``` @@ -1291,19 +1337,22 @@ with case expressions and one not involving case expressions. ## Well-typed terms don't get stuck A term is _normal_ if it cannot reduce: -``` + +```agda Normal : Term → Set Normal M = ∀ {N} → ¬ (M —→ N) ``` A term is _stuck_ if it is normal yet not a value: -``` + +```agda Stuck : Term → Set Stuck M = Normal M × ¬ Value M ``` Using progress, it is easy to show that no well-typed term is stuck: -``` + +```agda postulate unstuck : ∀ {M A} → ∅ ⊢ M ⦂ A @@ -1313,7 +1362,8 @@ postulate Using preservation, it is easy to show that after any number of steps, a well-typed term remains well typed: -``` + +```agda postulate preserves : ∀ {M N A} → ∅ ⊢ M ⦂ A @@ -1324,7 +1374,8 @@ postulate An easy consequence is that starting from a well-typed term, taking any number of reduction steps leads to a term that is not stuck: -``` + +```agda postulate wttdgs : ∀ {M N A} → ∅ ⊢ M ⦂ A @@ -1332,6 +1383,7 @@ postulate ----------- → ¬ (Stuck N) ``` + Felleisen and Wright, who introduced proofs via progress and preservation, summarised this result with the slogan _well-typed terms don't get stuck_. (They were referring to earlier work by Robin @@ -1343,7 +1395,7 @@ showed _well-typed terms don't go wrong_.) Give an example of an ill-typed term that does get stuck. -``` +```agda -- Your code goes here ``` @@ -1351,7 +1403,7 @@ Give an example of an ill-typed term that does get stuck. Provide proofs of the three postulates, `unstuck`, `preserves`, and `wttdgs` above. -``` +```agda -- Your code goes here ``` @@ -1364,7 +1416,8 @@ Our proof will need a variant of congruence to deal with functions of five arguments (to deal with `case_[_⇒_∥_⇒_]`). It is exactly analogous to `cong` and `cong₂` as defined previously: -``` + +```agda cong₅ : ∀ {A B C D E F : Set} (f : A → B → C → D → E → F) {p v : A} {q w : B} {r x : C} {s y : D} {t z : E} → p ≡ v → q ≡ w → r ≡ x → s ≡ y → t ≡ z → f p q r s t ≡ f v w x y z @@ -1372,7 +1425,8 @@ cong₅ f refl refl refl refl refl = refl ``` It is now straightforward to show that reduction is deterministic: -``` + +```agda det : ∀ {M M′ M″} → (M —→ M′) → (M —→ M″) @@ -1402,6 +1456,7 @@ det β-zero β-zero = refl det (β-suc VL) (ξ-case L—→L″) = ⊥-elim (V—↛ (V-suc VL) L—→L″) det (β-suc _) (β-suc _) = refl ``` + The proof is by induction over possible reductions. We consider three typical cases: diff --git a/extra/variants/CEK.lagda.md b/extra/variants/CEK.lagda.md index b0cf83fd5..b81ce2b64 100644 --- a/extra/variants/CEK.lagda.md +++ b/extra/variants/CEK.lagda.md @@ -4,7 +4,7 @@ Siek, Thiemann, Wadler, 2 Aug 2022 [Currently not compiling] -``` +```agda module variants.CEK where open import Data.Nat using (ℕ; zero; suc; _+_) @@ -23,7 +23,7 @@ open import variants.Frame Evaluation context as a stack of frames -``` +```agda data _==>_ : Type → Type → Set where [] : A ==> A @@ -40,7 +40,7 @@ variable Extending a substitution -``` +```agda _►_ : Γ →ˢ Δ → Δ ⊢ A @@ -51,7 +51,8 @@ _►_ : ``` CEK configuration -``` + +```agda record CEK (A : Type) : Set where constructor cek field @@ -63,7 +64,8 @@ record CEK (A : Type) : Set where ``` CEK transitions -``` + +```agda data _~~>_ : CEK A → CEK A → Set where CEK-ξ-□· : diff --git a/extra/variants/Evaluation.lagda.md b/extra/variants/Evaluation.lagda.md index 4e2a547ea..a7f9c06b7 100644 --- a/extra/variants/Evaluation.lagda.md +++ b/extra/variants/Evaluation.lagda.md @@ -1,7 +1,8 @@ PCF with nested evaluation contexts Philip Wadler, 2 Aug 2022 -``` + +```agda module variants.Evaluation where open import Data.Nat using (ℕ; zero; suc; _+_) @@ -19,7 +20,7 @@ open import Relation.Nullary.Decidable using (⌊_⌋; True; toWitness; fromWitn ## Types -``` +```agda infixr 7 _⇒_ infix 8 `ℕ @@ -33,7 +34,7 @@ variable * Type environments -``` +```agda infixl 6 _▷_ data Env : Set where @@ -62,7 +63,7 @@ variable ## Terms -``` +```agda infix 4 _⊢_ infix 5 ƛ_ infix 5 μ_ @@ -115,7 +116,7 @@ variable ## Renaming maps, substitution maps, term maps -``` +```agda _→ᴿ_ : Env → Env → Set Γ →ᴿ Δ = ∀ {A} → Γ ∋ A → Δ ∋ A @@ -134,7 +135,7 @@ variable ## Renaming -``` +```agda ren▷ : (Γ →ᴿ Δ) ------------------ @@ -160,7 +161,7 @@ lift = ren S_ ## Substitution -``` +```agda sub▷ : (Γ →ˢ Δ) ------------------ @@ -182,7 +183,8 @@ sub σ (μ M) = μ (sub (sub▷ σ) M) ``` Special case of substitution, used in beta rule -``` + +```agda σ₀ : Γ ⊢ A ------------ @@ -200,7 +202,7 @@ _[_] N M = sub (σ₀ M) N ## Values -``` +```agda data Value : (Γ ⊢ A) → Set where ƛ_ : @@ -228,7 +230,8 @@ variable Extract term from evidence that it is a value. -``` + +```agda value : ∀ {Γ A} {V : Γ ⊢ A} → (v : Value V) ------------- @@ -239,7 +242,8 @@ value {V = V} v = V Renaming preserves values (not needed, but I wanted to check that automatic generalisation works) -``` + +```agda ren-val : (ρ : Γ →ᴿ Δ) → Value V @@ -255,7 +259,7 @@ ren-val ρ (μ M) = μ (ren (ren▷ ρ) M) ## Evaluation contexts -``` +```agda infix 6 [_]·_ infix 6 _·[_] infix 7 `suc[_] @@ -293,7 +297,8 @@ data _⊢_=>_ : Env → Type → Type → Set where ``` The plug function inserts an expression into the hole of a frame. -``` + +```agda _⟦_⟧ : Γ ⊢ A => B → Γ ⊢ A @@ -307,7 +312,8 @@ _⟦_⟧ : ``` Composition of two frames -``` + +```agda _∘_ : Γ ⊢ B => C → Γ ⊢ A => B @@ -321,7 +327,8 @@ _∘_ : ``` Composition and plugging -``` + +```agda ∘-lemma : (E : Γ ⊢ B => C) → (F : Γ ⊢ A => B) @@ -337,7 +344,7 @@ Composition and plugging ## Reduction -``` +```agda infix 2 _↦_ _—→_ data _↦_ : (Γ ⊢ A) → (Γ ⊢ A) → Set where @@ -378,13 +385,14 @@ data _—→_ : (Γ ⊢ A) → (Γ ⊢ A) → Set where ``` Notation -``` + +```agda pattern ξ E M—→N = ξ-refl E refl refl M—→N ``` ## Reflexive and transitive closure of reduction -``` +```agda infix 1 begin_ infix 2 _—↠_ infixr 2 _—→⟨_⟩_ @@ -413,7 +421,8 @@ begin M—↠N = M—↠N Values are irreducible. The auxiliary definition rearranges the order of the arguments because it works better for Agda. -``` + +```agda value-irreducible : Value V → ¬ (V —→ M) value-irreducible v V—→M = nope V—→M v where @@ -423,7 +432,8 @@ value-irreducible v V—→M = nope V—→M v ``` Variables are irreducible. -``` + +```agda variable-irreducible : ------------ ¬ (` x —→ N) @@ -435,7 +445,7 @@ variable-irreducible (ξ □ ()) Every term that is well typed and closed is either blame or a value or takes a reduction step. -``` +```agda data Progress : (∅ ⊢ A) → Set where step : @@ -478,15 +488,18 @@ progress (μ N) = done (μ N) ## Evaluation Gas is specified by a natural number: -``` + +```agda record Gas : Set where constructor gas field amount : ℕ ``` + When our evaluator returns a term `N`, it will either give evidence that `N` is a value, or indicate that blame occurred or it ran out of gas. -``` + +```agda data Finished : (∅ ⊢ A) → Set where done : @@ -498,10 +511,12 @@ data Finished : (∅ ⊢ A) → Set where ---------- Finished N ``` + Given a term `L` of type `A`, the evaluator will, for some `N`, return a reduction sequence from `L` to `N` and an indication of whether reduction finished: -``` + +```agda data Steps : ∅ ⊢ A → Set where steps : @@ -510,8 +525,10 @@ data Steps : ∅ ⊢ A → Set where ---------- → Steps L ``` + The evaluator takes gas and a term and returns the corresponding steps: -``` + +```agda eval : Gas → (L : ∅ ⊢ A) @@ -529,6 +546,7 @@ eval (gas (suc m)) L # Example Computing two plus two on naturals: + ```agda pattern two = `suc `suc `zero @@ -541,6 +559,7 @@ pattern plus = μ ƛ ƛ (case x′ y′ (`suc (p′ · x″ · y″))) ``` Next, a sample reduction demonstrating that two plus two is four: + ```agda _ : plus · two · two —↠ `suc `suc `suc `suc (`zero {∅}) _ = begin diff --git a/extra/variants/Frame.lagda.md b/extra/variants/Frame.lagda.md index 9d8a32b88..1b90d2bcb 100644 --- a/extra/variants/Frame.lagda.md +++ b/extra/variants/Frame.lagda.md @@ -2,7 +2,7 @@ PCF with frames Philip Wadler, 2 Aug 2022 -``` +```agda module variants.Frame where open import Data.Nat using (ℕ; zero; suc; _+_) @@ -20,7 +20,7 @@ open import Relation.Nullary.Decidable using (⌊_⌋; True; toWitness; fromWitn ## Types -``` +```agda infixr 7 _⇒_ infix 8 `ℕ @@ -34,7 +34,7 @@ variable * Type environments -``` +```agda infixl 6 _▷_ data Env : Set where @@ -63,7 +63,7 @@ variable ## Terms -``` +```agda infix 4 _⊢_ infix 5 ƛ_ infix 5 μ_ @@ -116,7 +116,7 @@ variable ## Type class to convert naturals to an arbitrary type -``` +```agda variable n : ℕ @@ -140,7 +140,7 @@ instance Testing! -``` +```agda _ : Γ ▷ `ℕ ⊢ `ℕ _ = # 0 @@ -151,7 +151,7 @@ _ = # 1 ## Renaming maps, substitution maps, term maps -``` +```agda infix 4 _→ᴿ_ infix 4 _→ˢ_ infix 4 _→ᵀ_ @@ -174,7 +174,7 @@ variable ## Renaming -``` +```agda ren▷ : (Γ →ᴿ Δ) ------------------ @@ -200,7 +200,7 @@ lift = ren S_ ## Substitution -``` +```agda sub▷ : (Γ →ˢ Δ) ------------------ @@ -222,7 +222,8 @@ sub σ (μ M) = μ (sub (sub▷ σ) M) ``` Special case of substitution, used in beta rule -``` + +```agda σ₀ : Γ ⊢ A ------------ @@ -240,7 +241,7 @@ _[_] N M = sub (σ₀ M) N ## Values -``` +```agda data Value : (Γ ⊢ A) → Set where ƛ_ : @@ -268,7 +269,8 @@ variable Extract term from evidence that it is a value. -``` + +```agda value : ∀ {Γ A} {V : Γ ⊢ A} → (v : Value V) ------------- @@ -279,7 +281,8 @@ value {V = V} v = V Renaming preserves values (not needed, but I wanted to check that automatic generalisation works) -``` + +```agda ren-val : (ρ : Γ →ᴿ Δ) → Value V @@ -295,7 +298,7 @@ ren-val ρ (μ M) = μ (ren (ren▷ ρ) M) ## Evaluation frames -``` +```agda infix 6 □·_ infix 6 _·□ infix 7 `suc□ @@ -327,7 +330,8 @@ data _⊢_=>_ : Env → Type → Type → Set where ``` The plug function inserts an expression into the hole of a frame. -``` + +```agda _⟦_⟧ : Γ ⊢ A => B → Γ ⊢ A @@ -341,7 +345,7 @@ _⟦_⟧ : ## Reduction -``` +```agda infix 2 _—→_ data _—→_ : (Γ ⊢ A) → (Γ ⊢ A) → Set where @@ -380,13 +384,14 @@ data _—→_ : (Γ ⊢ A) → (Γ ⊢ A) → Set where ``` Notation -``` + +```agda pattern ξ E M—→N = ξ-refl E refl refl M—→N ``` ## Reflexive and transitive closure of reduction -``` +```agda infix 1 begin_ infix 2 _—↠_ infixr 2 _—→⟨_⟩_ @@ -415,7 +420,8 @@ begin M—↠N = M—↠N Values are irreducible. The auxiliary definition rearranges the order of the arguments because it works better for Agda. -``` + +```agda value-irreducible : Value V → ¬ (V —→ M) value-irreducible v V—→M = nope V—→M v where @@ -425,7 +431,8 @@ value-irreducible v V—→M = nope V—→M v ``` Variables are irreducible. -``` + +```agda variable-irreducible : ------------ ¬ (` x —→ M) @@ -440,7 +447,7 @@ variable-irreducible (ξ-refl (case□ M N) () e x—→) Every term that is well typed and closed is either blame or a value or takes a reduction step. -``` +```agda data Progress : (∅ ⊢ A) → Set where step : @@ -483,15 +490,18 @@ progress (μ N) = done (μ N) ## Evaluation Gas is specified by a natural number: -``` + +```agda record Gas : Set where constructor gas field amount : ℕ ``` + When our evaluator returns a term `N`, it will either give evidence that `N` is a value, or indicate that blame occurred or it ran out of gas. -``` + +```agda data Finished : (∅ ⊢ A) → Set where done : @@ -503,10 +513,12 @@ data Finished : (∅ ⊢ A) → Set where ---------- Finished N ``` + Given a term `L` of type `A`, the evaluator will, for some `N`, return a reduction sequence from `L` to `N` and an indication of whether reduction finished: -``` + +```agda data Steps : ∅ ⊢ A → Set where steps : @@ -515,8 +527,10 @@ data Steps : ∅ ⊢ A → Set where ---------- → Steps L ``` + The evaluator takes gas and a term and returns the corresponding steps: -``` + +```agda eval : Gas → (L : ∅ ⊢ A) @@ -534,6 +548,7 @@ eval (gas (suc m)) L # Example Computing two plus two on naturals: + ```agda two : Γ ⊢ `ℕ two = `suc `suc `zero @@ -546,6 +561,7 @@ plus = μ ƛ ƛ (case (# 1) (# 0) (`suc (# 3 · # 0 · # 1))) ``` Next, a sample reduction demonstrating that two plus two is four: + ```agda _ : 2+2 —↠ `suc `suc `suc `suc `zero _ = diff --git a/src/plfa/part1/Connectives.lagda.md b/src/plfa/part1/Connectives.lagda.md index 6bbfc7c3a..4cbdb074a 100644 --- a/src/plfa/part1/Connectives.lagda.md +++ b/src/plfa/part1/Connectives.lagda.md @@ -42,6 +42,7 @@ open plfa.part1.Isomorphism.≃-Reasoning Given two propositions `A` and `B`, the conjunction `A × B` holds if both `A` holds and `B` holds. We formalise this idea by declaring a suitable datatype: + ```agda record _×_ (A B : Set) : Set where constructor ⟨_,_⟩ @@ -50,6 +51,7 @@ record _×_ (A B : Set) : Set where proj₂ : B open _×_ ``` + Evidence that `A × B` holds is of the form `⟨ M , N ⟩`, where `M` provides evidence that `A` holds and `N` provides evidence that `B` holds. @@ -84,23 +86,28 @@ holds---how to _use_ the connective.[^from-wadler-2015] Applying each destructor and reassembling the results with the constructor is the identity over products: + ```agda η-× : ∀ {A B : Set} (w : A × B) → ⟨ proj₁ w , proj₂ w ⟩ ≡ w η-× w = refl ``` + For record types, η-equality holds *by definition*. While proving `η-×`, we do not have to pattern match on `w` to know that η-equality holds. We set the precedence of conjunction so that it binds less tightly than anything save disjunction: + ```agda infixr 2 _×_ ``` + Thus, `m ≤ n × n ≤ p` parses as `(m ≤ n) × (n ≤ p)`. Alternatively, we can declare conjunction as a data type, and the projections as functions using pattern matching. + ```agda data _×′_ (A B : Set) : Set where @@ -122,15 +129,18 @@ proj₂′ : ∀ {A B : Set} → B proj₂′ ⟨ x , y ⟩′ = y ``` + The record type `_×_` and the data type `_×′_` behave similarly. One difference is that for for record types, η-equality holds *by definition*, but for data types have to pattern match know that η-equality holds: + ```agda η-×′ : ∀ {A B : Set} (w : A ×′ B) → ⟨ proj₁′ w , proj₂′ w ⟩′ ≡ w η-×′ ⟨ x , y ⟩′ = refl ``` + The pattern matching on the left-hand side is essential, since replacing `w` by `⟨ x , y ⟩′` allows both sides of the propositional equality to simplify to the same term. @@ -147,6 +157,7 @@ distinct members, and type `B` has `n` distinct members, then the type `A × B` has `m * n` distinct members. For instance, consider a type `Bool` with two members, and a type `Tri` with three members: + ```agda data Bool : Set where true : Bool @@ -157,6 +168,7 @@ data Tri : Set where bb : Tri cc : Tri ``` + Then the type `Bool × Tri` has six members: ⟨ true , aa ⟩ ⟨ true , bb ⟩ ⟨ true , cc ⟩ @@ -164,6 +176,7 @@ Then the type `Bool × Tri` has six members: For example, the following function enumerates all possible arguments of type `Bool × Tri`: + ```agda ×-count : Bool × Tri → ℕ ×-count ⟨ true , aa ⟩ = 1 @@ -181,6 +194,7 @@ isomorphism_. For commutativity, the `to` function swaps a pair, taking `⟨ x , y ⟩` to `⟨ y , x ⟩`, and the `from` function does the same (up to renaming). + ```agda ×-comm : ∀ {A B : Set} → A × B ≃ B × A ×-comm = @@ -208,6 +222,7 @@ former, corresponds to `⟨ aa , true ⟩`, which is a member of the latter. For associativity, the `to` function reassociates two uses of pairing, taking `⟨ ⟨ x , y ⟩ , z ⟩` to `⟨ x , ⟨ y , z ⟩ ⟩`, and the `from` function does the inverse. + ```agda ×-assoc : ∀ {A B C : Set} → (A × B) × C ≃ A × (B × C) ×-assoc = @@ -244,11 +259,13 @@ is isomorphic to `(A → B) × (B → A)`. Truth `⊤` always holds. We formalise this idea by declaring the empty record type. + ```agda record ⊤ : Set where constructor tt ``` + Evidence that `⊤` holds is of the form `tt`. The record construction `record {}` corresponds to the term `tt`. The constructor declaration allows us to write `tt`. @@ -261,19 +278,23 @@ us nothing new. The nullary case of `η-×` is `η-⊤`. While proving `η-⊤`, we do not have to pattern match on `w`---Agda *knows* it is equal to `tt`: + ```agda η-⊤ : ∀ (w : ⊤) → tt ≡ w η-⊤ w = refl ``` + Agda knows that *any* value of type `⊤` must be `tt`, so any time we need a value of type `⊤`, we can tell Agda to figure it out: + ```agda truth : ⊤ truth = _ ``` Alternatively, we can declare truth as a data type: + ```agda data ⊤′ : Set where @@ -281,13 +302,16 @@ data ⊤′ : Set where -- ⊤′ ``` + As with the product, the record type `⊤` and the data type `⊤′` behave similarly, but while η-equality holds *by definition* for the record type, it does not for the data type, so we need to pattern match on `w`: + ```agda η-⊤′ : ∀ (w : ⊤′) → tt′ ≡ w η-⊤′ tt′ = refl ``` + The pattern matching on the left-hand side is essential. Replacing `w` by `tt′` allows both sides of the propositional equality to simplify to the same term. @@ -298,6 +322,7 @@ whenever there is only one constructor. We refer to `⊤` as the _unit_ type. And, indeed, type `⊤` has exactly one member, `tt`. For example, the following function enumerates all possible arguments of type `⊤`: + ```agda ⊤-count : ⊤ → ℕ ⊤-count tt = 1 @@ -308,6 +333,7 @@ unit is the identity of product _up to isomorphism_. For left identity, the `to` function takes `⟨ tt , x ⟩` to `x`, and the `from` function does the inverse. The evidence of left inverse requires matching against a suitable pattern to enable simplification: + ```agda ⊤-identityˡ : ∀ {A : Set} → ⊤ × A ≃ A ⊤-identityˡ = @@ -333,6 +359,7 @@ For instance, `⟨ tt , true ⟩`, which is a member of the former, corresponds to `true`, which is a member of the latter. Right identity follows from commutativity of product and left identity: + ```agda ⊤-identityʳ : ∀ {A : Set} → (A × ⊤) ≃ A ⊤-identityʳ {A} = @@ -344,6 +371,7 @@ Right identity follows from commutativity of product and left identity: A ≃-∎ ``` + Here we have used a chain of isomorphisms, analogous to that used for equality. @@ -353,6 +381,7 @@ equality. Given two propositions `A` and `B`, the disjunction `A ⊎ B` holds if either `A` holds or `B` holds. We formalise this idea by declaring a suitable inductive type: + ```agda data _⊎_ (A B : Set) : Set where @@ -366,12 +395,14 @@ data _⊎_ (A B : Set) : Set where ----- → A ⊎ B ``` + Evidence that `A ⊎ B` holds is either of the form `inj₁ M`, where `M` provides evidence that `A` holds, or `inj₂ N`, where `N` provides evidence that `B` holds. Given evidence that `A → C` and `B → C` both hold, then given evidence that `A ⊎ B` holds we can conclude that `C` holds: + ```agda case-⊎ : ∀ {A B C : Set} → (A → C) @@ -382,6 +413,7 @@ case-⊎ : ∀ {A B C : Set} case-⊎ f g (inj₁ x) = f x case-⊎ f g (inj₂ y) = g y ``` + Pattern matching against `inj₁` and `inj₂` is typical of how we exploit evidence that a disjunction holds. @@ -395,27 +427,33 @@ the former are sometimes given the names `⊎-I₁` and `⊎-I₂` and the latter the name `⊎-E`. Applying the destructor to each of the constructors is the identity: + ```agda η-⊎ : ∀ {A B : Set} (w : A ⊎ B) → case-⊎ inj₁ inj₂ w ≡ w η-⊎ (inj₁ x) = refl η-⊎ (inj₂ y) = refl ``` + More generally, we can also throw in an arbitrary function from a disjunction: + ```agda uniq-⊎ : ∀ {A B C : Set} (h : A ⊎ B → C) (w : A ⊎ B) → case-⊎ (h ∘ inj₁) (h ∘ inj₂) w ≡ h w uniq-⊎ h (inj₁ x) = refl uniq-⊎ h (inj₂ y) = refl ``` + The pattern matching on the left-hand side is essential. Replacing `w` by `inj₁ x` allows both sides of the propositional equality to simplify to the same term, and similarly for `inj₂ y`. We set the precedence of disjunction so that it binds less tightly than any other declared operator: + ```agda infixr 1 _⊎_ ``` + Thus, `A × C ⊎ B × C` parses as `(A × C) ⊎ (B × C)`. Given two types `A` and `B`, we refer to `A ⊎ B` as the @@ -436,6 +474,7 @@ members: For example, the following function enumerates all possible arguments of type `Bool ⊎ Tri`: + ```agda ⊎-count : Bool ⊎ Tri → ℕ ⊎-count (inj₁ true) = 1 @@ -468,10 +507,12 @@ Show sum is associative up to isomorphism. False `⊥` never holds. We formalise this idea by declaring a suitable inductive type: + ```agda data ⊥ : Set where -- no clauses! ``` + There is no possible evidence that `⊥` holds. Dual to `⊤`, for `⊥` there is no introduction rule but an elimination rule. @@ -481,6 +522,7 @@ conclude anything! This is a basic principle of logic, known in medieval times by the Latin phrase _ex falso_, and known to children through phrases such as "if pigs had wings, then I'd be the Queen of Sheba". We formalise it as follows: + ```agda ⊥-elim : ∀ {A : Set} → ⊥ @@ -488,6 +530,7 @@ Sheba". We formalise it as follows: → A ⊥-elim () ``` + This is our first use of the _absurd pattern_ `()`. Here since `⊥` is a type with no members, we indicate that it is _never_ possible to match against a value of this type by using @@ -499,10 +542,12 @@ in the standard library. The nullary case of `uniq-⊎` is `uniq-⊥`, which asserts that `⊥-elim` is equal to any arbitrary function from `⊥`: + ```agda uniq-⊥ : ∀ {C : Set} (h : ⊥ → C) (w : ⊥) → ⊥-elim w ≡ h w uniq-⊥ h () ``` + Using the absurd pattern asserts there are no possible values for `w`, so the equation holds trivially. @@ -512,10 +557,12 @@ We can also use `()` in nested patterns. For instance, We refer to `⊥` as the _empty_ type. And, indeed, type `⊥` has no members. For example, the following function enumerates all possible arguments of type `⊥`: + ```agda ⊥-count : ⊥ → ℕ ⊥-count () ``` + Here again the absurd pattern `()` indicates that no value can match type `⊥`. @@ -556,6 +603,7 @@ converts evidence that `A` holds into evidence that `B` holds. Put another way, if we know that `A → B` and `A` both hold, then we may conclude that `B` holds: + ```agda →-elim : ∀ {A B : Set} → (A → B) @@ -564,6 +612,7 @@ then we may conclude that `B` holds: → B →-elim L M = L M ``` + In medieval times, this rule was known by the name _modus ponens_. It corresponds to function application. @@ -572,6 +621,7 @@ is referred to as _introducing_ a function, while applying a function is referred to as _eliminating_ the function. Elimination followed by introduction is the identity: + ```agda η-→ : ∀ {A B : Set} (f : A → B) → (λ (x : A) → f x) ≡ f η-→ f = refl @@ -596,6 +646,7 @@ three squared) members: For example, the following function enumerates all possible arguments of the type `Bool → Tri`: + ```agda →-count : (Bool → Tri) → ℕ →-count f with f true | f false @@ -625,6 +676,7 @@ we have the isomorphism Both types can be viewed as functions that given evidence that `A` holds and evidence that `B` holds can return evidence that `C` holds. This isomorphism sometimes goes by the name *currying*. + ```agda currying : ∀ {A B C : Set} → (A → B → C) ≃ (A × B → C) currying = @@ -635,6 +687,7 @@ currying = ; to∘from = λ{ g → refl } } ``` + Currying tells us that instead of a function that takes a pair of arguments, we can have a function that takes the first argument and returns a function that expects the second argument. Thus, for instance, our way of writing addition @@ -660,6 +713,7 @@ we have the isomorphism: That is, the assertion that if either `A` holds or `B` holds then `C` holds is the same as the assertion that if `A` holds then `C` holds and if `B` holds then `C` holds. The proof of the left inverse requires extensionality: + ```agda →-distrib-⊎ : ∀ {A B C : Set} → (A ⊎ B → C) ≃ ((A → C) × (B → C)) →-distrib-⊎ = @@ -682,6 +736,7 @@ we have the isomorphism: That is, the assertion that if `A` holds then `B` holds and `C` holds is the same as the assertion that if `A` holds then `B` holds and if `A` holds then `C` holds. + ```agda →-distrib-× : ∀ {A B C : Set} → (A → B × C) ≃ (A → B) × (A → C) →-distrib-× = @@ -698,6 +753,7 @@ is the same as the assertion that if `A` holds then `B` holds and if Products distribute over sum, up to isomorphism. The code to validate this fact is similar in structure to our previous results: + ```agda ×-distrib-⊎ : ∀ {A B C : Set} → (A ⊎ B) × C ≃ (A × C) ⊎ (B × C) ×-distrib-⊎ = @@ -718,6 +774,7 @@ this fact is similar in structure to our previous results: ``` Sums do not distribute over products up to isomorphism, but it is an embedding: + ```agda ⊎-distrib-× : ∀ {A B C : Set} → (A × B) ⊎ C ≲ (A ⊎ C) × (B ⊎ C) ⊎-distrib-× = @@ -734,6 +791,7 @@ Sums do not distribute over products up to isomorphism, but it is an embedding: } } ``` + Note that there is a choice in how we write the `from` function. As given, it takes `⟨ inj₂ z , inj₂ w ⟩` to `inj₂ z`, but it is easy to write a variant that instead returns `inj₂ w`. We have @@ -755,10 +813,12 @@ one of these laws is "more true" than the other. #### Exercise `⊎-weak-×` (recommended) Show that the following property holds: + ```agda postulate ⊎-weak-× : ∀ {A B C : Set} → (A ⊎ B) × C → A ⊎ (B × C) ``` + This is called a _weak distributive law_. Give the corresponding distributive law, and explain how it relates to the weak version. @@ -770,10 +830,12 @@ distributive law, and explain how it relates to the weak version. #### Exercise `⊎×-implies-×⊎` (practice) Show that a disjunct of conjuncts implies a conjunct of disjuncts: + ```agda postulate ⊎×-implies-×⊎ : ∀ {A B C D : Set} → (A × B) ⊎ (C × D) → (A ⊎ C) × (B ⊎ D) ``` + Does the converse hold? If so, prove; if not, give a counterexample. ```agda @@ -784,6 +846,7 @@ Does the converse hold? If so, prove; if not, give a counterexample. ## Standard library Definitions similar to those in this chapter can be found in the standard library: + ```agda import Data.Product using (_×_; proj₁; proj₂) renaming (_,_ to ⟨_,_⟩) import Data.Unit using (⊤; tt) @@ -791,6 +854,7 @@ import Data.Sum using (_⊎_; inj₁; inj₂) renaming ([_,_] to case-⊎) import Data.Empty using (⊥; ⊥-elim) import Function.Bundles using (_⇔_) ``` + The standard library constructs pairs with `_,_` whereas we use `⟨_,_⟩`. The former makes it convenient to build triples or larger tuples from pairs, permitting `a , b , c` to stand for `(a , (b , c))`. But it conflicts with diff --git a/src/plfa/part1/Decidable.lagda.md b/src/plfa/part1/Decidable.lagda.md index 7a1dfd84e..da17b0b96 100644 --- a/src/plfa/part1/Decidable.lagda.md +++ b/src/plfa/part1/Decidable.lagda.md @@ -39,6 +39,7 @@ Recall that Chapter [Relations](/Relations/) defined comparison as an inductive datatype, which provides _evidence_ that one number is less than or equal to another: + ```agda infix 4 _≤_ @@ -53,8 +54,10 @@ data _≤_ : ℕ → ℕ → Set where ------------- → suc m ≤ suc n ``` + For example, we can provide evidence that `2 ≤ 4`, and show there is no possible evidence that `4 ≤ 2`: + ```agda 2≤4 : 2 ≤ 4 2≤4 = s≤s (s≤s z≤n) @@ -62,6 +65,7 @@ and show there is no possible evidence that `4 ≤ 2`: ¬4≤2 : ¬ (4 ≤ 2) ¬4≤2 (s≤s (s≤s ())) ``` + The occurrence of `()` attests to the fact that there is no possible evidence for `2 ≤ 0`, which `z≤n` cannot match (because `2` is not `zero`) and `s≤s` cannot match @@ -69,13 +73,16 @@ no possible evidence for `2 ≤ 0`, which `z≤n` cannot match An alternative, which may seem more familiar, is to define a type of booleans: + ```agda data Bool : Set where true : Bool false : Bool ``` + Given booleans, we can define a function of two numbers that _computes_ to `true` if the comparison holds and to `false` otherwise: + ```agda infix 4 _≤ᵇ_ @@ -84,12 +91,14 @@ zero ≤ᵇ n = true suc m ≤ᵇ zero = false suc m ≤ᵇ suc n = m ≤ᵇ n ``` + The first and last clauses of this definition resemble the two constructors of the corresponding inductive datatype, while the middle clause arises because there is no possible evidence that `suc m ≤ zero` for any `m`. For example, we can compute that `2 ≤ᵇ 4` holds, and we can compute that `4 ≤ᵇ 2` does not hold: + ```agda _ : (2 ≤ᵇ 4) ≡ true _ = @@ -115,6 +124,7 @@ _ = false ∎ ``` + In the first case, it takes two steps to reduce the first argument to zero, and one more step to compute true, corresponding to the two uses of `s≤s` and the one use of `z≤n` when providing evidence that `2 ≤ 4`. @@ -127,11 +137,13 @@ and the one use of `()` when showing there can be no evidence that `4 ≤ 2`. We would hope to be able to show these two approaches are related, and indeed we can. First, we define a function that lets us map from the computation world to the evidence world: + ```agda T : Bool → Set T true = ⊤ T false = ⊥ ``` + Recall that `⊤` is the unit type which contains the single element `tt`, and the `⊥` is the empty type which contains no values. (Also note that `T` is a capital letter t, and distinct from `⊤`.) If `b` is of type `Bool`, @@ -141,19 +153,23 @@ no possible evidence that `T b` holds if `b` is false. Another way to put this is that `T b` is inhabited exactly when `b ≡ true` is inhabited. In the forward direction, we need to do a case analysis on the boolean `b`: + ```agda T→≡ : ∀ (b : Bool) → T b → b ≡ true T→≡ true tt = refl T→≡ false () ``` + If `b` is true then `T b` is inhabited by `tt` and `b ≡ true` is inhabited by `refl`, while if `b` is false then `T b` in uninhabited. In the reverse direction, there is no need for a case analysis on the boolean `b`: + ```agda ≡→T : ∀ {b : Bool} → b ≡ true → T b ≡→T refl = tt ``` + If `b ≡ true` is inhabited by `refl` we know that `b` is `true` and hence `T b` is inhabited by `tt`. @@ -161,12 +177,14 @@ Now we can show that `T (m ≤ᵇ n)` is inhabited exactly when `m ≤ n` is inh In the forward direction, we consider the three clauses in the definition of `_≤ᵇ_`: + ```agda ≤ᵇ→≤ : ∀ (m n : ℕ) → T (m ≤ᵇ n) → m ≤ n ≤ᵇ→≤ zero n tt = z≤n ≤ᵇ→≤ (suc m) zero () ≤ᵇ→≤ (suc m) (suc n) t = s≤s (≤ᵇ→≤ m n t) ``` + In the first clause, we immediately have that `zero ≤ᵇ n` is true, so `T (m ≤ᵇ n)` is evidenced by `tt`, and correspondingly `m ≤ n` is evidenced by `z≤n`. In the middle clause, we immediately have that @@ -180,11 +198,13 @@ We recursively invoke the function to get evidence that `m ≤ n`, which In the reverse direction, we consider the possible forms of evidence that `m ≤ n`: + ```agda ≤→≤ᵇ : ∀ {m n : ℕ} → m ≤ n → T (m ≤ᵇ n) ≤→≤ᵇ z≤n = tt ≤→≤ᵇ (s≤s m≤n) = ≤→≤ᵇ m≤n ``` + If the evidence is `z≤n` then we immediately have that `zero ≤ᵇ n` is true, so `T (m ≤ᵇ n)` is evidenced by `tt`. If the evidence is `s≤s` applied to `m≤n`, then `suc m ≤ᵇ suc n` reduces to `m ≤ᵇ n`, and we @@ -212,11 +232,13 @@ does the relation hold or does it not? Conversely, the evidence approach tells us exactly why the relation holds, but we are responsible for generating the evidence. But it is easy to define a type that combines the benefits of both approaches. It is called `Dec A`, where `Dec` is short for _decidable_: + ```agda data Dec (A : Set) : Set where yes : A → Dec A no : ¬ A → Dec A ``` + Like booleans, the type has two constructors. A value of type `Dec A` is either of the form `yes x`, where `x` provides evidence that `A` holds, or of the form `no ¬x`, where `¬x` provides evidence that `A` cannot hold @@ -227,6 +249,7 @@ is less than or equal to the other, and provides evidence to justify its conclus First, we introduce two functions useful for constructing evidence that an inequality does not hold: + ```agda ¬s≤z : ∀ {m : ℕ} → ¬ (suc m ≤ zero) ¬s≤z () @@ -234,6 +257,7 @@ an inequality does not hold: ¬s≤s : ∀ {m n : ℕ} → ¬ (m ≤ n) → ¬ (suc m ≤ suc n) ¬s≤s ¬m≤n (s≤s m≤n) = ¬m≤n m≤n ``` + The first of these asserts that `¬ (suc m ≤ zero)`, and follows by absurdity, since any evidence of inequality has the form `zero ≤ n` or `suc m ≤ suc n`, neither of which match `suc m ≤ zero`. The second @@ -243,6 +267,7 @@ form `s≤s m≤n` where `m≤n` is evidence that `m ≤ n`. Hence, we have a contradiction, evidenced by `¬m≤n m≤n`. Using these, it is straightforward to decide an inequality: + ```agda _≤?_ : ∀ (m n : ℕ) → Dec (m ≤ n) zero ≤? n = yes z≤n @@ -251,6 +276,7 @@ suc m ≤? suc n with m ≤? n ... | yes m≤n = yes (s≤s m≤n) ... | no ¬m≤n = no (¬s≤s ¬m≤n) ``` + As with `_≤ᵇ_`, the definition has three clauses. In the first clause, it is immediate that `zero ≤ n` holds, and it is evidenced by `z≤n`. In the second clause, it is immediate that `suc m ≤ zero` does @@ -271,6 +297,7 @@ to derive them from `_≤?_`. We can use our new function to _compute_ the _evidence_ that earlier we had to think up on our own: + ```agda _ : 2 ≤? 4 ≡ yes (s≤s (s≤s z≤n)) _ = refl @@ -278,6 +305,7 @@ _ = refl _ : 4 ≤? 2 ≡ no (¬s≤s (¬s≤s ¬s≤z)) _ = refl ``` + You can check that Agda will indeed compute these values. Typing `C-c C-n` and providing `2 ≤? 4` or `4 ≤? 2` as the requested expression causes Agda to print the values given above. @@ -290,6 +318,7 @@ trouble normalising evidence of negation.) #### Exercise `_ Date: Wed, 24 Dec 2025 16:19:49 +0000 Subject: [PATCH 2/2] Add markdownlint to pre-commit --- .markdownlint.yaml | 16 ++++++++++++++++ .pre-commit-config.yaml | 41 +++++++++++++++++++++++------------------ 2 files changed, 39 insertions(+), 18 deletions(-) create mode 100644 .markdownlint.yaml diff --git a/.markdownlint.yaml b/.markdownlint.yaml new file mode 100644 index 000000000..2b2218b1f --- /dev/null +++ b/.markdownlint.yaml @@ -0,0 +1,16 @@ +default: true +MD001: false +MD004: false +MD007: false +MD012: false +MD013: false +MD022: false +MD024: false +MD030: false +MD032: false +MD033: false +MD038: false +MD046: false +MD049: false +MD053: false +MD059: false diff --git a/.pre-commit-config.yaml b/.pre-commit-config.yaml index 8786b71ad..7af2d5d98 100644 --- a/.pre-commit-config.yaml +++ b/.pre-commit-config.yaml @@ -1,23 +1,28 @@ repos: -- repo: https://github.com/pre-commit/pre-commit-hooks + - repo: https://github.com/pre-commit/pre-commit-hooks rev: v6.0.0 hooks: - - id: check-added-large-files - - id: check-case-conflict - - id: check-executables-have-shebangs - - id: check-json - - id: check-merge-conflict - - id: check-shebang-scripts-are-executable - - id: check-symlinks - - id: check-vcs-permalinks - - id: check-yaml - - id: destroyed-symlinks - - id: detect-private-key - - id: fix-byte-order-marker - - id: file-contents-sorter + - id: check-added-large-files + - id: check-case-conflict + - id: check-executables-have-shebangs + - id: check-json + - id: check-merge-conflict + - id: check-shebang-scripts-are-executable + - id: check-symlinks + - id: check-vcs-permalinks + - id: check-yaml + - id: destroyed-symlinks + - id: detect-private-key + - id: fix-byte-order-marker + - id: file-contents-sorter args: [--unique] files: '\.epubcheck\.tsv|\.htmlvalidateignore' - - id: forbid-new-submodules - - id: end-of-file-fixer - - id: mixed-line-ending - - id: trailing-whitespace + - id: forbid-new-submodules + - id: end-of-file-fixer + - id: mixed-line-ending + - id: trailing-whitespace + - repo: https://github.com/igorshubovych/markdownlint-cli + rev: v0.47.0 + hooks: + - id: markdownlint + files: 'src/.*\.md'