michael/csci8980-f21
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Updated TSPL

Browse source
This commit is contained in:
Philip Wadler 2018-09-15 20:34:02 +01:00
parent 905df9fe12
commit 1c0ff3b9fa
18 changed files with 152 additions and 231 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
_config.yml
View file

@ -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

4
index.md
View file

@ -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 %})

28
src/plfa/Acknowledgements.lagda
View file

@ -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
<span class="force-end-of-list"></span>
{%- if site.contributors -%}
For pull requests big and small:
<ul>
{%- for contributor in site.contributors -%}
<li><a href="https://github.com/{{ contributor.github_username }}">{{ contributor.name }}</a></li>
{%- endfor -%}
</ul>
{%- 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
<span class="force-end-of-list"></span>
{%- if site.contributors -%}
For pull requests big and small:
<ul>
{%- for contributor in site.contributors -%}
<li><a href="https://github.com/{{ contributor.github_username }}">{{ contributor.name }}</a></li>
{%- endfor -%}
<li>[Your name goes here]</li>
</ul>
{%- else -%}
{%- endif -%}

2
src/plfa/DeBruijn.lagda
View file

@ -1,7 +1,9 @@
---
title : "DeBruijn: Inherently typed de Bruijn representation"
layout : page
prev : /Properties/
permalink : /DeBruijn/
next : /More/
---
\begin{code}

5
src/plfa/Dedication.lagda
View file

@ -2,8 +2,11 @@
title : "Dedication"
layout : page
permalink : /Dedication/
next : /Preface/
---
## To Wanda
### _knock knock knock_
### _amor da minha vida_
#### _knock knock knock_

14
src/plfa/Fonts.lagda
View file

@ -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}
{-
------------|
⟶⟶⟶⟶|
⟹⟹⟹⟹|

4
src/plfa/Induction.lagda
View file

@ -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

2
src/plfa/Inference.lagda
View file

@ -1,7 +1,9 @@
---
title : "Inference: Bidirectional type inference"
layout : page
prev : /Bisimulation/
permalink : /Inference/
next : /Untyped/
---
\begin{code}

2
src/plfa/Lambda.lagda
View file

@ -1,7 +1,9 @@
---
title : "Lambda: Introduction to Lambda Calculus"
layout : page
prev : /Lists/
permalink : /Lambda/
next : /Properties/
---
\begin{code}

2
src/plfa/More.lagda
View file

@ -1,7 +1,9 @@
---
title : "More: Additional constructs of simply-typed lambda calculus"
layout : page
prev : /DeBruijn/
permalink : /More/
next : /Bisimulation/
---
\begin{code}

5
src/plfa/Naturals.lagda
View file

@ -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.

2
src/plfa/Preface.lagda
View file

@ -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.

2
src/plfa/Properties.lagda
View file

@ -1,7 +1,9 @@
---
title : "Properties: Progress and Preservation"
layout : page
prev : /Lambda/
permalink : /Properties/
next : /DeBruijn/
---
\begin{code}

14
src/plfa/Relations.lagda
View file

@ -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

1
src/plfa/Statistics.lagda
View file

@ -1,6 +1,7 @@
---
title : "Statistics: Line counts for each chapter"
layout : page
prev : /Fonts/
permalink : /Statistics/
---

102
src/plfa/TSPL.lagda Normal file
View file

@ -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
<table>
<tr>
<th>Week</th>
<th>Mon</th>
<th>Wed</th>
<th>Fri</th>
</tr>
<tr>
<td>1</td>
<td><b>17 Sep</b> <a href="/Naturals/">Naturals</a></td>
<td><b>19 Sep</b> <a href="/Induction/">Induction</a></td>
<td><b>21 Sep</b> <a href="/Induction/">Induction</a></td>
</tr>
<tr>
<td>2</td>
<td><b>24 Sep</b> <a href="/Relations/">Relations</a> (Chad)</td>
<td><b>26 Sep</b> <a href="/Relations/">Relations</a> (Chad)</td>
<td><b>28 Sep</b> (no lecture)</td>
</tr>
<tr>
<td>3</td>
<td><b>1 Oct</b> <a href="/Equality/">Equality</a></td>
<td><b>3 Oct</b> <a href="/Isomorphism/">Isomorphism</a></td>
<td><b>5 Oct</b> <a href="/Connectives/">Connectives</a></td>
</tr>
<tr>
<td>4</td>
<td><b>8 Oct</b> <a href="/Negation/">Negation</a></td>
<td><b>10 Oct</b> <a href="/Quantifiers/">Quantifiers</a></td>
<td><b>12 Oct</b> <a href="/Decidable/">Decidable</a></td>
</tr>
<tr>
<td>5</td>
<td><b>15 Oct</b> <a href="/Lists/">Lists</a></td>
<td><b>17 Oct</b> (no lecture)</td>
<td><b>19 Oct</b> <a href="/Lists/">Lists</a></td>
</tr>
<tr>
<td>6</td>
<td><b>22 Oct</b> <a href="/Lambda/">Lambda</a></td>
<td><b>24 Oct</b> <a href="/Properties/">Properties</a></td>
<td><b>26 Oct</b> (no lecture)</td>
</tr>
<tr>
<td>7</td>
<td><b>29 Oct</b> <a href="/DeBruijn/">DeBruijn</a></td>
<td><b>31 Oct</b> <a href="/More/">More</a></td>
<td><b>2 Nov</b> (no lecture)</td>
</tr>
<tr>
<td>8</td>
<td><b>5 Nov</b> <a href="/Bisimulation/">Bisimulation</a></td>
<td><b>7 Nov</b> <a href="/Inference/">Inference</a></td>
<td><b>9 Nov</b> (no lecture)</td>
</tr>
<tr>
<td>9</td>
<td><b>12 Nov</b> <a href="/Untyped/">Untyped</a></td>
<td><b>14 Nov</b> (no lecture)</td>
<td><b>16 Nov</b> (no lecture)</td>
</tr>
<tr>
<td>10</td>
<td><b>19 Nov</b> (tutorial only)</td>
<td><b>21 Nov</b> (no lecture)</td>
<td><b>23 Nov</b> (no lecture)</td>
</tr>
<tr>
<td>11</td>
<td><b>26 Nov</b> PaT</td>
<td><b>28 Nov</b> (no lecture)</td>
<td><b>30 Nov</b> (mock exam)</td>
</tr>
</table>
## 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)

2
src/plfa/Untyped.lagda
View file

@ -1,7 +1,9 @@
---
title : "Untyped: Untyped lambda calculus with full normalisation"
layout : page
prev : /Inference/
permalink : /Untyped/
next : /Acknowledgements/
---
\begin{code}

191
src/tspl/TSPL.lagda
View file

@ -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
- `_<?_` (recommended)
- `_≡ℕ?_`
- `erasure`
- `iff-erasure` (recommended)
* Assignment 3. Due 4pm Thursday 1 November (Week 7)
+ Lists
- `reverse-++-commute` (recommended)
- `reverse-involutive` (recommended)
- `map-compose`
- `map-++-commute`
- `map-Tree` (recommended)
- `product`
- `fold-++` (recommended)
- `map-is-foldr`
- `fold-Tree`
- `map-is-fold-Tree`
- `sum-downFrom` (stretch)
- `Any-++` (recommended)
- `¬Any≃All¬` (stretch)
- `any?` (recommended)
+ Lambda
- `mul` (recommended)
- `primed` (stretch)
- `_[_:=_]′` (stretch)
- `—↠≃—↠′`
- `plus-example`
- `mul-type` (recommended)
+ Properties
- `Progress-iso`
- `progress′`
- `value?`
- `subst′` (stretch)
- `mul-example` (recommended)
- `unstuck` (recommended)
+ DeBruijn
- `mul` (recommended)
- `V¬—→`
- `mul-example` (recommended)
* Assignment 4. Due 4pm Thursday 15 November (Week 9)
+ More
- `More` (recommended)
+ Bisimulation
- `_†`
- `~val⁻¹`
- `sim⁻¹`
- `products`
+ Inference
- `bidirectional-ps` (recommended)
- `bidirectional-rest` (stretch)
- `inference-p` (recommended)
- `inference-rest` (stretch)
+ Untyped
- `Type≃⊤`
- `Context≃ℕ`
- `variant-1` (recommended)
- `variant-2`
- `2+2≡four` (recommended)
- `encode-more` (stretch)
* Assignment 5. Due 4pm Thursday 22 November (Week 10)