added TSPL 2019
This commit is contained in:
Philip Wadler
parent
27bd94d314
commit
db46fd1539
2 changed files with 436 additions and 0 deletions
314
courses/tspl/2019/Assignment1.lagda.md
Normal file
314
courses/tspl/2019/Assignment1.lagda.md
Normal file
|
|
@ -0,0 +1,314 @@
|
|||
---
|
||||
title : "Assignment1: TSPL Assignment 1"
|
||||
layout : page
|
||||
permalink : /TSPL/2018/Assignment1/
|
||||
---
|
||||
|
||||
```
|
||||
module Assignment1 where
|
||||
```
|
||||
|
||||
## YOUR NAME AND EMAIL GOES HERE
|
||||
|
||||
## Introduction
|
||||
|
||||
<!-- This assignment is due **1pm Friday 26 April**. -->
|
||||
|
||||
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.
|
||||
|
||||
<!-- Submit your homework using the "submit" command. -->
|
||||
Please ensure your files execute correctly under Agda!
|
||||
|
||||
## Imports
|
||||
|
||||
```
|
||||
import Relation.Binary.PropositionalEquality as Eq
|
||||
open Eq using (_≡_; refl; cong; sym)
|
||||
open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; _≡⟨_⟩_; _∎)
|
||||
open import Data.Nat using (ℕ; zero; suc; _+_; _*_; _∸_; _≤_; z≤n; s≤s)
|
||||
open import Data.Nat.Properties using (+-assoc; +-identityʳ; +-suc; +-comm;
|
||||
≤-refl; ≤-trans; ≤-antisym; ≤-total; +-monoʳ-≤; +-monoˡ-≤; +-mono-≤)
|
||||
open import plfa.part1.Relations using (_<_; z<s; s<s; zero; suc; even; odd)
|
||||
```
|
||||
|
||||
## Naturals
|
||||
|
||||
#### Exercise `seven` {#seven}
|
||||
|
||||
Write out `7` in longhand.
|
||||
|
||||
|
||||
#### Exercise `+-example` {#plus-example}
|
||||
|
||||
Compute `3 + 4`, writing out your reasoning as a chain of equations.
|
||||
|
||||
|
||||
#### Exercise `*-example` {#times-example}
|
||||
|
||||
Compute `3 * 4`, writing out your reasoning as a chain of equations.
|
||||
|
||||
|
||||
#### Exercise `_^_` (recommended) {#power}
|
||||
|
||||
Define exponentiation, which is given by the following equations.
|
||||
|
||||
n ^ 0 = 1
|
||||
n ^ (1 + m) = n * (n ^ m)
|
||||
|
||||
Check that `3 ^ 4` is `81`.
|
||||
|
||||
|
||||
#### Exercise `∸-examples` (recommended) {#monus-examples}
|
||||
|
||||
Compute `5 ∸ 3` and `3 ∸ 5`, writing out your reasoning as a chain of equations.
|
||||
|
||||
|
||||
#### Exercise `Bin` (stretch) {#Bin}
|
||||
|
||||
A more efficient representation of natural numbers uses a binary
|
||||
rather than a unary system. We represent a number as a bitstring.
|
||||
```
|
||||
data Bin : Set where
|
||||
nil : Bin
|
||||
x0_ : Bin → Bin
|
||||
x1_ : Bin → Bin
|
||||
```
|
||||
For instance, the bitstring
|
||||
|
||||
1011
|
||||
|
||||
standing for the number eleven is encoded, right to left, as
|
||||
|
||||
x1 x1 x0 x1 nil
|
||||
|
||||
Representations are not unique due to leading zeros.
|
||||
Hence, eleven is also represented by `001011`, encoded as
|
||||
|
||||
x1 x1 x0 x1 x0 x0 nil
|
||||
|
||||
Define a function
|
||||
|
||||
inc : Bin → Bin
|
||||
|
||||
that converts a bitstring to the bitstring for the next higher
|
||||
number. For example, since `1100` encodes twelve, we should have
|
||||
|
||||
inc (x1 x1 x0 x1 nil) ≡ x0 x0 x1 x1 nil
|
||||
|
||||
Confirm that this gives the correct answer for the bitstrings
|
||||
encoding zero through four.
|
||||
|
||||
Using the above, define a pair of functions to convert
|
||||
between the two representations.
|
||||
|
||||
to : ℕ → Bin
|
||||
from : Bin → ℕ
|
||||
|
||||
For the former, choose the bitstring to have no leading zeros if it
|
||||
represents a positive natural, and represent zero by `x0 nil`.
|
||||
Confirm that these both give the correct answer for zero through four.
|
||||
|
||||
## Induction
|
||||
|
||||
#### Exercise `operators` {#operators}
|
||||
|
||||
Give another example of a pair of operators that have an identity
|
||||
and are associative, commutative, and distribute over one another.
|
||||
|
||||
Give an example of an operator that has an identity and is
|
||||
associative but is not commutative.
|
||||
|
||||
|
||||
#### 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
|
||||
[earlier][plfa.Naturals#finite-creation]
|
||||
|
||||
|
||||
#### Exercise `+-swap` (recommended) {#plus-swap}
|
||||
|
||||
Show
|
||||
|
||||
m + (n + p) ≡ n + (m + p)
|
||||
|
||||
for all naturals `m`, `n`, and `p`. No induction is needed,
|
||||
just apply the previous results which show addition
|
||||
is associative and commutative. You may need to use
|
||||
the following function from the standard library:
|
||||
|
||||
sym : ∀ {m n : ℕ} → m ≡ n → n ≡ m
|
||||
|
||||
|
||||
#### Exercise `*-distrib-+` (recommended) {#times-distrib-plus}
|
||||
|
||||
Show multiplication distributes over addition, that is,
|
||||
|
||||
(m + n) * p ≡ m * p + n * p
|
||||
|
||||
for all naturals `m`, `n`, and `p`.
|
||||
|
||||
#### Exercise `*-assoc` (recommended) {#times-assoc}
|
||||
|
||||
Show multiplication is associative, that is,
|
||||
|
||||
(m * n) * p ≡ m * (n * p)
|
||||
|
||||
for all naturals `m`, `n`, and `p`.
|
||||
|
||||
#### Exercise `*-comm` {#times-comm}
|
||||
|
||||
Show multiplication is commutative, that is,
|
||||
|
||||
m * n ≡ n * m
|
||||
|
||||
for all naturals `m` and `n`. As with commutativity of addition,
|
||||
you will need to formulate and prove suitable lemmas.
|
||||
|
||||
#### Exercise `0∸n≡0` {#zero-monus}
|
||||
|
||||
Show
|
||||
|
||||
zero ∸ n ≡ zero
|
||||
|
||||
for all naturals `n`. Did your proof require induction?
|
||||
|
||||
#### Exercise `∸-|-assoc` {#monus-plus-assoc}
|
||||
|
||||
Show that monus associates with addition, that is,
|
||||
|
||||
m ∸ n ∸ p ≡ m ∸ (n + p)
|
||||
|
||||
for all naturals `m`, `n`, and `p`.
|
||||
|
||||
#### Exercise `Bin-laws` (stretch) {#Bin-laws}
|
||||
|
||||
Recall that
|
||||
Exercise [Bin][plfa.Naturals#Bin]
|
||||
defines a datatype `Bin` of bitstrings representing natural numbers
|
||||
and asks you to define functions
|
||||
|
||||
inc : Bin → Bin
|
||||
to : ℕ → Bin
|
||||
from : Bin → ℕ
|
||||
|
||||
Consider the following laws, where `n` ranges over naturals and `x`
|
||||
over bitstrings.
|
||||
|
||||
from (inc x) ≡ suc (from x)
|
||||
to (from n) ≡ n
|
||||
from (to x) ≡ x
|
||||
|
||||
For each law: if it holds, prove; if not, give a counterexample.
|
||||
|
||||
|
||||
## Relations
|
||||
|
||||
|
||||
#### Exercise `orderings` {#orderings}
|
||||
|
||||
Give an example of a preorder that is not a partial order.
|
||||
|
||||
Give an example of a partial order that is not a preorder.
|
||||
|
||||
|
||||
#### Exercise `≤-antisym-cases` {#leq-antisym-cases}
|
||||
|
||||
The above proof omits cases where one argument is `z≤n` and one
|
||||
argument is `s≤s`. Why is it ok to omit them?
|
||||
|
||||
|
||||
#### Exercise `*-mono-≤` (stretch)
|
||||
|
||||
Show that multiplication is monotonic with regard to inequality.
|
||||
|
||||
|
||||
#### Exercise `<-trans` (recommended) {#less-trans}
|
||||
|
||||
Show that strict inequality is transitive.
|
||||
|
||||
#### Exercise `trichotomy` {#trichotomy}
|
||||
|
||||
Show that strict inequality satisfies a weak version of trichotomy, in
|
||||
the sense that for any `m` and `n` that one of the following holds:
|
||||
* `m < n`,
|
||||
* `m ≡ n`, or
|
||||
* `m > n`
|
||||
Define `m > n` to be the same as `n < m`.
|
||||
You will need a suitable data declaration,
|
||||
similar to that used for totality.
|
||||
(We will show that the three cases are exclusive after we introduce
|
||||
[negation][plfa.Negation].)
|
||||
|
||||
#### Exercise `+-mono-<` {#plus-mono-less}
|
||||
|
||||
Show that addition is monotonic with respect to strict inequality.
|
||||
As with inequality, some additional definitions may be required.
|
||||
|
||||
#### Exercise `≤-iff-<` (recommended) {#leq-iff-less}
|
||||
|
||||
Show that `suc m ≤ n` implies `m < n`, and conversely.
|
||||
|
||||
#### Exercise `<-trans-revisited` {#less-trans-revisited}
|
||||
|
||||
Give an alternative proof that strict inequality is transitive,
|
||||
using the relating between strict inequality and inequality and
|
||||
the fact that inequality is transitive.
|
||||
|
||||
#### Exercise `o+o≡e` (stretch) {#odd-plus-odd}
|
||||
|
||||
Show that the sum of two odd numbers is even.
|
||||
|
||||
#### Exercise `Bin-predicates` (stretch) {#Bin-predicates}
|
||||
|
||||
Recall that
|
||||
Exercise [Bin][plfa.Naturals#Bin]
|
||||
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
|
||||
|
||||
x1 x1 x0 x1 nil
|
||||
x1 x1 x0 x1 x0 x0 nil
|
||||
|
||||
Define a predicate
|
||||
|
||||
Can : Bin → Set
|
||||
|
||||
over all bitstrings that holds if the bitstring is canonical, meaning
|
||||
it has no leading zeros; the first representation of eleven above is
|
||||
canonical, and the second is not. To define it, you will need an
|
||||
auxiliary predicate
|
||||
|
||||
One : Bin → Set
|
||||
|
||||
that holds only if the bistring has a leading one. A bitstring is
|
||||
canonical if it has a leading one (representing a positive number) or
|
||||
if it consists of a single zero (representing zero).
|
||||
|
||||
Show that increment preserves canonical bitstrings.
|
||||
|
||||
Can x
|
||||
------------
|
||||
Can (inc x)
|
||||
|
||||
Show that converting a natural to a bitstring always yields a
|
||||
canonical bitstring.
|
||||
|
||||
----------
|
||||
Can (to n)
|
||||
|
||||
Show that converting a canonical bitstring to a natural
|
||||
and back is the identity.
|
||||
|
||||
Can x
|
||||
---------------
|
||||
to (from x) ≡ x
|
||||
|
||||
(Hint: For each of these, you may first need to prove related
|
||||
properties of `One`.)
|
||||
122
courses/tspl/2019/tspl2019.md
Normal file
122
courses/tspl/2019/tspl2019.md
Normal file
|
|
@ -0,0 +1,122 @@
|
|||
---
|
||||
title : "TSPL: Course notes"
|
||||
layout : page
|
||||
permalink : /TSPL/2019/
|
||||
---
|
||||
|
||||
## Staff
|
||||
|
||||
* **Instructor**
|
||||
[Philip Wadler](https://homepages.inf.ed.ac.uk/wadler)
|
||||
* **Teaching assistant**
|
||||
- [Wen Kokke](mailto:wen.kokke@ed.ac.uk)
|
||||
|
||||
## Lectures
|
||||
|
||||
Lectures take place Monday, Wednesday, and Friday in AT 5.07. (Room provisional.)
|
||||
* **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>16 Sep</b> <a href="{{ site.baseurl }}/part1/Naturals/">Naturals</a></td>
|
||||
<td><b>18 Sep</b> <a href="{{ site.baseurl }}/part1/Induction/">Induction</a></td>
|
||||
<td><b>20 Sep</b> <a href="{{ site.baseurl }}/part1/Relations/">Relations</a></td>
|
||||
</tr>
|
||||
<tr>
|
||||
<td>2</td>
|
||||
<td><b>23 Sep</b> (no class)</td>
|
||||
<td><b>25 Sep</b> (tutorial only)</td>
|
||||
<td><b>27 Sep</b> (no class)</td>
|
||||
</tr>
|
||||
<tr>
|
||||
<td>3</td>
|
||||
<td><b>30 Oct</b> <a href="{{ site.baseurl }}/part1/Equality/">Equality</a> &
|
||||
<a href="{{ site.baseurl }}/Isomorphism/">Isomorphism</a></td>
|
||||
<td><b>2 Oct</b> <a href="{{ site.baseurl }}/part1/Connectives/">Connectives</a></td>
|
||||
<td><b>4 Oct</b> <a href="{{ site.baseurl }}/part1/Negation/">Negation</a></td>
|
||||
</tr>
|
||||
<tr>
|
||||
<td>4</td>
|
||||
<td><b>7 Oct</b> <a href="{{ site.baseurl }}/part1/Quantifiers/">Quantifiers</a></td>
|
||||
<td><b>9 Oct</b> <a href="{{ site.baseurl }}/part1/Decidable/">Decidable</a></td>
|
||||
<td><b>11 Oct</b> (tutorial only)</td>
|
||||
</tr>
|
||||
<tr>
|
||||
<td>5</td>
|
||||
<td><b>14 Oct</b> <a href="{{ site.baseurl }}/part1/Lists/">Lists</a></td>
|
||||
<td><b>16 Oct</b> <!-- (tutorial only) --></td>
|
||||
<td><b>18 Oct</b> <!-- <a href="{{ site.baseurl }}/part1/Lists/">Lists</a> --></td>
|
||||
</tr>
|
||||
<tr>
|
||||
<td>6</td>
|
||||
<td><b>21 Oct</b> <!-- <a href="{{ site.baseurl }}/part1/Lambda/">Lambda</a> --></td>
|
||||
<td><b>23 Oct</b> <!-- (no class) --></td>
|
||||
<td><b>25 Oct</b> <!-- <a href="{{ site.baseurl }}/part1/Properties/">Properties</a> --></td>
|
||||
</tr>
|
||||
<tr>
|
||||
<td>7</td>
|
||||
<td><b>28 Oct</b> <!-- <a href="{{ site.baseurl }}/part1/DeBruijn/">DeBruijn</a> --></td>
|
||||
<td><b>30 Oct</b> <!-- <a href="{{ site.baseurl }}/part1/More/">More</a> --></td>
|
||||
<td><b>1 Nov</b> <!-- <a href="{{ site.baseurl }}/part1/Inference/">Inference</a> --></td>
|
||||
</tr>
|
||||
<tr>
|
||||
<td>8</td>
|
||||
<td><b>4 Nov</b> <!-- (no class) --></td>
|
||||
<td><b>6 Nov</b> <!-- (tutorial only) --></td>
|
||||
<td><b>8 Nov</b> <!-- <a href="{{ site.baseurl }}/part1/Untyped/">Untyped</a> --></td>
|
||||
</tr>
|
||||
<tr>
|
||||
<td>9</td>
|
||||
<td><b>11 Nov</b> <!-- (no class) --></td>
|
||||
<td><b>13 Nov</b> <!-- (tutorial only) --></td>
|
||||
<td><b>15 Nov</b> <!-- (no class) --></td>
|
||||
</tr>
|
||||
<tr>
|
||||
<td>10</td>
|
||||
<td><b>18 Nov</b> <!-- (no class) --></td>
|
||||
<td><b>20 Nov</b> <!-- Propositions as Types --></td>
|
||||
<td><b>22 Nov</b> <!-- (no class) --></td>
|
||||
</tr>
|
||||
<tr>
|
||||
<td>11</td>
|
||||
<td><b>25 Nov</b> <!-- (no class) --></td>
|
||||
<td><b>27 Nov</b> <!-- Quantitative (Wen)--></td>
|
||||
<td><b>29 Nov</b> (mock exam)</td>
|
||||
</tr>
|
||||
</table>
|
||||
|
||||
## Assignments
|
||||
|
||||
For instructions on how to set up Agda for PLFA see [Getting Started]({{ site.baseurl }}/GettingStarted/).
|
||||
|
||||
* [Assignment 1]({{ site.baseurl }}/TSPL/2019/Assignment1/) cw1 due 4pm Thursday 3 October (Week 3)
|
||||
* Assignment 2 <!-- [Assignment 2]({{ site.baseurl }}/TSPL/2019/Assignment2/) --> cw2 due 4pm Thursday 17 October (Week 5)
|
||||
* Assignment 3 <!-- [Assignment 3]({{ site.baseurl }}/TSPL/2019/Assignment3/) --> cw3 due 4pm Thursday 31 October (Week 7)
|
||||
* Assignment 4 <!-- [Assignment 4]({{ site.baseurl }}/TSPL/2019/Assignment4/) --> cw4 due 4pm Thursday 14 November (Week 9)
|
||||
* Assignment 5 <!-- [Assignment 5]({{ site.baseurl }}/courses/tspl/2010/Mock1.pdf) --> cw5 due 4pm Thursday 21 November (Week 10)
|
||||
<!-- <br />
|
||||
Use file [Exam]({{ site.baseurl }}/TSPL/2018/Exam/). Despite the rubric, do **all three questions**. -->
|
||||
|
||||
|
||||
Assignments are submitted by running
|
||||
``` bash
|
||||
submit tspl cwN AssignmentN.lagda
|
||||
```
|
||||
where N is the number of the assignment.
|
||||
|
||||
<!--
|
||||
|
||||
## Mock exam
|
||||
|
||||
Here is the text of the [second mock]({{ site.baseurl }}/courses/tspl/2018/Mock2.pdf)
|
||||
and the exam [instructions]({{ site.baseurl }}/courses/tspl/2018/Instructions.pdf).
|
||||
|
||||
-->
|
||||
Loading…
Reference in a new issue