diff --git a/_config.yml b/_config.yml index 2abaf8ae..9bb5f605 100644 --- a/_config.yml +++ b/_config.yml @@ -10,7 +10,6 @@ description: > authors: - name: Philip Wadler email: wadler@inf.ed.ac.uk - github_username: wadler corresponding: true github_username: wadler - name: Wen Kokke diff --git a/index.md b/index.md index 8a1b7eec..8c4eeebd 100644 --- a/index.md +++ b/index.md @@ -39,10 +39,6 @@ Pull requests are encouraged. - [Inference: Bidirectional type inference]({{ site.baseurl }}{% link out/plfa/Inference.md %}) - [Untyped: Untyped lambda calculus with full normalisation]({{ site.baseurl }}{% link out/plfa/Untyped.md %}) -## Additional material - - - [SystemF: Inherently typed System F]({{ site.baseurl }}{% link out/plfa/SystemF.md %}) - ## Backmatter - [Acknowledgements]({{ site.baseurl }}{% link out/plfa/Acknowledgements.md %}) diff --git a/src/plfa/Acknowledgements.lagda b/src/plfa/Acknowledgements.lagda index 742e4d72..680ced36 100644 --- a/src/plfa/Acknowledgements.lagda +++ b/src/plfa/Acknowledgements.lagda @@ -1,7 +1,9 @@ --- title : "Acknowledgements" layout : page +prev : /Untyped/ permalink : /Acknowledgements/ +next : /Fonts/ --- Thank you to: @@ -16,17 +18,6 @@ this book is based, and for hand-holding: * Ulf Norell * Andreas Abel - -{%- if site.contributors -%} -For pull requests big and small: - -{%- else -%} -{%- endif -%} - For a note showing how much more compact it is to avoid raw terms: * David Darais @@ -45,3 +36,18 @@ For answering questions on the Agda mailing list: * N. Raghavendra * Roman Kireev * Amr Sabry + + + +{%- if site.contributors -%} +For pull requests big and small: + +{%- else -%} +{%- endif -%} + + diff --git a/src/plfa/DeBruijn.lagda b/src/plfa/DeBruijn.lagda index 5afcc7fd..9f505f90 100644 --- a/src/plfa/DeBruijn.lagda +++ b/src/plfa/DeBruijn.lagda @@ -1,7 +1,9 @@ --- title : "DeBruijn: Inherently typed de Bruijn representation" layout : page +prev : /Properties/ permalink : /DeBruijn/ +next : /More/ --- \begin{code} diff --git a/src/plfa/Dedication.lagda b/src/plfa/Dedication.lagda index 82543b83..783e05de 100644 --- a/src/plfa/Dedication.lagda +++ b/src/plfa/Dedication.lagda @@ -2,8 +2,11 @@ title : "Dedication" layout : page permalink : /Dedication/ +next : /Preface/ --- ## To Wanda -### _knock knock knock_ +### _amor da minha vida_ + +#### _knock knock knock_ diff --git a/src/plfa/Fonts.lagda b/src/plfa/Fonts.lagda index d740b368..55024758 100644 --- a/src/plfa/Fonts.lagda +++ b/src/plfa/Fonts.lagda @@ -1,10 +1,11 @@ --- title : "Fonts" layout : page +prev : /Acknowledgements/ permalink : /Fonts/ --- -Test page for fonts. All vertical bars should line up. +Test page for fonts. Preferably, all vertical bars should line up. \begin{code} {- @@ -48,25 +49,20 @@ ABCDEFGHIJKLMNOPQRSTUVWXYZ| ⊢⊢⊣⊣| ∷∷∷∷| ∎∎∎∎| +∅∅∅∅| ⦂⦂⦂⦂| ----| -} \end{code} -Here are some characters that are exactly two spaces wide. +Here are some characters that are often not monospaced. + \begin{code} {- ----| 😇😇| 😈😈| ----| --} -\end{code} - -Here are some characters that are not used because they are not monospaced. - -\begin{code} -{- ------------| ⟶⟶⟶⟶| ⟹⟹⟹⟹| diff --git a/src/plfa/Induction.lagda b/src/plfa/Induction.lagda index 6642c4b6..1682468b 100644 --- a/src/plfa/Induction.lagda +++ b/src/plfa/Induction.lagda @@ -580,7 +580,7 @@ judgements where the first number is less than _m_. There is also a completely finite approach to generating the same equations, which is left as an exercise for the reader. -#### Exercise `finite-+-assoc` {#finite-plus-assoc} +#### Exercise `finite-+-assoc` (stretch) {#finite-plus-assoc} Write out what is known about associativity of addition on each of the first four days using a finite story of creation, as @@ -738,7 +738,7 @@ typing `C-c C-r` will fill it in, completing the proof: +-assoc′ (suc m) n p rewrite +-assoc′ m n p = refl -#### Exercise `+-swap` {#plus-swap} +#### Exercise `+-swap` (recommended) {#plus-swap} Show diff --git a/src/plfa/Inference.lagda b/src/plfa/Inference.lagda index e2c456e6..6846815e 100644 --- a/src/plfa/Inference.lagda +++ b/src/plfa/Inference.lagda @@ -1,7 +1,9 @@ --- title : "Inference: Bidirectional type inference" layout : page +prev : /Bisimulation/ permalink : /Inference/ +next : /Untyped/ --- \begin{code} diff --git a/src/plfa/Lambda.lagda b/src/plfa/Lambda.lagda index 02d92559..b910f98d 100644 --- a/src/plfa/Lambda.lagda +++ b/src/plfa/Lambda.lagda @@ -1,7 +1,9 @@ --- title : "Lambda: Introduction to Lambda Calculus" layout : page +prev : /Lists/ permalink : /Lambda/ +next : /Properties/ --- \begin{code} diff --git a/src/plfa/More.lagda b/src/plfa/More.lagda index 1dacb4c7..44588d11 100644 --- a/src/plfa/More.lagda +++ b/src/plfa/More.lagda @@ -1,7 +1,9 @@ --- title : "More: Additional constructs of simply-typed lambda calculus" layout : page +prev : /DeBruijn/ permalink : /More/ +next : /Bisimulation/ --- \begin{code} diff --git a/src/plfa/Naturals.lagda b/src/plfa/Naturals.lagda index 9f29a58a..5b736b1d 100644 --- a/src/plfa/Naturals.lagda +++ b/src/plfa/Naturals.lagda @@ -1,6 +1,7 @@ --- title : "Naturals: Natural numbers" layout : page +prev : /Prelude/ permalink : /Naturals/ next : /Induction/ --- @@ -480,7 +481,7 @@ it can easily be inferred from the corresponding term. Compute `3 * 4`, writing out your reasoning as a chain of equations. -#### Exercise `_^_` {#power} +#### Exercise `_^_` (recommended) {#power} Define exponentiation, which is given by the following equations. @@ -545,7 +546,7 @@ _ = ∎ \end{code} -#### Exercise `∸-examples` {#monus-examples} +#### Exercise `∸-examples` (recommended) {#monus-examples} Compute `5 ∸ 3` and `3 ∸ 5`, writing out your reasoning as a chain of equations. diff --git a/src/plfa/Preface.lagda b/src/plfa/Preface.lagda index af831ec9..13ca509b 100644 --- a/src/plfa/Preface.lagda +++ b/src/plfa/Preface.lagda @@ -1,7 +1,9 @@ --- title : "Preface" layout : page +prev : /Dedication/ permalink : /Preface/ +next : /Naturals/ --- The most profound connection between logic and computation is a pun. diff --git a/src/plfa/Properties.lagda b/src/plfa/Properties.lagda index 00f29065..6494d652 100644 --- a/src/plfa/Properties.lagda +++ b/src/plfa/Properties.lagda @@ -1,7 +1,9 @@ --- title : "Properties: Progress and Preservation" layout : page +prev : /Lambda/ permalink : /Properties/ +next : /DeBruijn/ --- \begin{code} diff --git a/src/plfa/Relations.lagda b/src/plfa/Relations.lagda index cc49ec30..927a8c5a 100644 --- a/src/plfa/Relations.lagda +++ b/src/plfa/Relations.lagda @@ -531,7 +531,7 @@ and conversely. One can then give an alternative derivation of the properties of strict inequality, such as transitivity, by directly exploiting the corresponding properties of inequality. -#### Exercise `<-trans` {#less-trans} +#### Exercise `<-trans` (recommended) {#less-trans} Show that strict inequality is transitive. @@ -553,7 +553,7 @@ similar to that used for totality. Show that addition is monotonic with respect to strict inequality. As with inequality, some additional definitions may be required. -#### Exercise `≤-iff-<` {#leq-iff-less} +#### Exercise `≤-iff-<` (recommended) {#leq-iff-less} Show that `suc m ≤ n` implies `m < n`, and conversely. @@ -662,7 +662,7 @@ evidence that the first number is odd. If it is because it is the successor of an even number, then the result is odd because it is the successor of the sum of two even numbers, which is even. -#### Exercise `o+o≡e` {#odd-plus-odd} +#### Exercise `o+o≡e` (stretch) {#odd-plus-odd} Show that the sum of two odd numbers is even. @@ -670,13 +670,7 @@ Show that the sum of two odd numbers is even. Recall that Exercise [Bin][plfa.Naturals#Bin] -defines a datatype of bitstrings representing natural numbers. -\begin{code} -data Bin : Set where - nil : Bin - x0_ : Bin → Bin - x1_ : Bin → Bin -\end{code} +defines a datatype `Bin` of bitstrings representing natural numbers. Representations are not unique due to leading zeros. Hence, eleven may be represented by both of the following diff --git a/src/plfa/Statistics.lagda b/src/plfa/Statistics.lagda index 780b53da..f2e246cb 100644 --- a/src/plfa/Statistics.lagda +++ b/src/plfa/Statistics.lagda @@ -1,6 +1,7 @@ --- title : "Statistics: Line counts for each chapter" layout : page +prev : /Fonts/ permalink : /Statistics/ --- diff --git a/src/plfa/TSPL.lagda b/src/plfa/TSPL.lagda new file mode 100644 index 00000000..50a14bca --- /dev/null +++ b/src/plfa/TSPL.lagda @@ -0,0 +1,102 @@ +--- +title : "TSPL: Course notes" +layout : page +permalink : /TSPL/ +--- + +## Lectures + +Lectures take place Monday, Wednesday, and Friday in AT 4.12. +* **9.00--9.50am** Lecture +* **10.00--10.50am** Tutorial + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
WeekMonWedFri
117 Sep Naturals19 Sep Induction21 Sep Induction
224 Sep Relations (Chad)26 Sep Relations (Chad)28 Sep (no lecture)
31 Oct Equality3 Oct Isomorphism5 Oct Connectives
48 Oct Negation10 Oct Quantifiers12 Oct Decidable
515 Oct Lists17 Oct (no lecture)19 Oct Lists
622 Oct Lambda24 Oct Properties26 Oct (no lecture)
729 Oct DeBruijn31 Oct More2 Nov (no lecture)
85 Nov Bisimulation7 Nov Inference9 Nov (no lecture)
912 Nov Untyped14 Nov (no lecture)16 Nov (no lecture)
1019 Nov (tutorial only)21 Nov (no lecture)23 Nov (no lecture)
1126 Nov PaT28 Nov (no lecture)30 Nov (mock exam)
+ +## Assignments + +You must do _all_ the exercises labelled "(recommended)". + +Exercises labelled "(stretch)" are there to provide an extra challenge. +You don't need to do all of these, but should attempt at least a few. + +Exercises without a label are optional, and may be done if you want +some extra practice. + +* [Assignment 1][plfa.Assignment1] due 4pm Thursday 4 October (Week 3) +* Assignment 2 due 4pm Thursday 18 October (Week 5) +* Assignment 3 due 4pm Thursday 1 November (Week 7) +* Assignment 4 due 4pm Thursday 15 November (Week 9) +* Assignment 5 due 4pm Thursday 22 November (Week 10) diff --git a/src/plfa/Untyped.lagda b/src/plfa/Untyped.lagda index e0389096..c5775856 100644 --- a/src/plfa/Untyped.lagda +++ b/src/plfa/Untyped.lagda @@ -1,7 +1,9 @@ --- title : "Untyped: Untyped lambda calculus with full normalisation" layout : page +prev : /Inference/ permalink : /Untyped/ +next : /Acknowledgements/ --- \begin{code} diff --git a/src/tspl/TSPL.lagda b/src/tspl/TSPL.lagda deleted file mode 100644 index cb02f433..00000000 --- a/src/tspl/TSPL.lagda +++ /dev/null @@ -1,191 +0,0 @@ ---- -title : "TSPL: Course notes" -layout : page -permalink : /TSPL/ ---- - -## Lectures - -* **Mon 17 Sep** [Naturals][plfa.Naturals] -* **Wed 19 Sep** [Induction][plfa.Induction] -* **Fri 21 Sep** [Induction][plfa.Induction] -* **Mon 24 Sep** [Relations][plfa.Relations] (Chad) -* **Wed 26 Sep** [Relations][plfa.Relations] (Chad) -* **Fri 28 Sep** (no lecture) -* **Mon 1 Oct** [Equality][plfa.Equality] -* **Wed 3 Oct** [Isomorphism][plfa.Isomorphism] -* **Thu 4 Oct** _Assignment 1_ -* **Fri 5 Oct** [Connectives][plfa.Connectives] -* **Mon 8 Oct** [Quantifiers][plfa.Quantifiers] -* **Wed 10 Oct** [Negation][plfa.Negation] -* **Fri 12 Oct** [Decidable][plfa.Decidable] -* **Mon 15 Oct** [Lists][plfa.Lists] -* **Wed 17 Oct** (no lecture) -* **Thu 18 Oct** _Assignment 2_ -* **Fri 19 Oct** [Lists][plfa.Lists] -* **Mon 22 Oct** [Lambda][plfa.Lambda] -* **Wed 24 Oct** [Properties][plfa.Properties] -* **Fri 26 Oct** (no lecture) -* **Mon 29 Oct** [DeBruijn][plfa.DeBruijn] -* **Wed 31 Oct** [More][plfa.More] -* **Thu 1 Nov** _Assignment 3_ -* **Fri 2 Nov** (no lecture) -* **Mon 5 Nov** [Bisimulation][plfa.Bisimulation] -* **Wed 7 Nov** [Inference][plfa.Inference] -* **Fri 9 Nov** (no lecture) -* **Mon 12 Nov** [Untyped][plfa.Untyped] -* **Wed 14 Nov** (no lecture) -* **Thu 15 Nov** _Assignment 4_ -* **Fri 16 Nov** (no lecture) -* **Mon 19 Nov** (tutorial only) -* **Wed 21 Nov** (no lecture) -* **Thu 22 Nov** _Assignment 5_ -* **Fri 23 Nov** (no lecture) -* **Mon 26 Nov** Mock exam -* **Wed 28 Nov** (no lecture) -* **Fri 30 Nov** (no lecture) - -## Assignments - -You must do _all_ the exercises labelled "(recommended)". - -Exercises labelled "(stretch)" are there to provide an extra challenge. -You don't need to do all of these, but should attempt at least a few. - -Exercises without a label are optional, and may be done if you want -some extra practice. - -* Assignment 1. Due 4pm Thursday 4 October (Week 3) - - + Naturals - - `seven` - - `+-example` - - `*-example` - - `_^_` (recommended) - - `∸-examples` (recommended) - - `Bin` (stretch) - - + Induction - - `operators` (recommended) - - `finite-+-assoc` (recommended) - - `+-swap` (recommended) - - `*-distribʳ-+` (recommended) - - `*-assoc` (recommended) - - `*-comm` - - `0∸n≡n` - - `∸-+-assoc` - - `Bin-laws` (stretch) - - + Relations - - `orderings` (recommended) - - `≤-antisym-cases` (recommended) - - `*-mono-≤` (stretch) - - `<-trans` (recommended) - - `trichotomy` - - `+-mono-<` - - `≤-iff-<` (recommended) - - `<-trans-revisited` - - `o+o≡e` (recommended) - -* Assignment 2. Due 4pm Thursday 18 October (Week 5) - - + Equality - - `≤-reasoning` (stretch) - - + Isomorphism - - `≃-implies-≲` - - `Bin-embedding` (stretch) - - + Connectives - - `⊎-weak-×` (recommended) - - `⊎×-implies-×⊎` (recommended) - - `_⇔_` (recommended) - - + Negation - - `<-irreflexive` (recommended) - - `trichotomy` (recommended) - - `⊎-dual-×` (recommended) - - `Classical` (stretch) - - `Stable` (stretch) - - + Quantifiers - - `∀-distrib-×` (recommended) - - `⊎∀-implies-∀⊎` - - `∃-distrib-⊎` (recommended) - - `∃×-implies-×∃` - - `∃-even-odd` - - `∃-+-≤` - - `∃¬-implies-¬∀` (recommended) - - `Bin-isomorphism` (stretch) - - + Decidable - - `_