Revert "Removed TSPL content from PLFA"
This reverts commit 3b842e8429.
This commit is contained in:
Wen Kokke
parent
5187a4cc6d
commit
570b3b4f45
16 changed files with 5408 additions and 3 deletions
12
Makefile
12
Makefile
|
|
@ -1,6 +1,6 @@
|
||||||
agda := $(shell find src -type f -name '*.lagda')
|
agda := $(shell find src tspl -type f -name '*.lagda')
|
||||||
agdai := $(shell find src -type f -name '*.agdai')
|
agdai := $(shell find src tspl -type f -name '*.agdai')
|
||||||
markdown := $(subst src/,out/,$(subst .lagda,.md,$(agda)))
|
markdown := $(subst tspl/,out/,$(subst src/,out/,$(subst .lagda,.md,$(agda))))
|
||||||
PLFA_DIR := $(shell dirname $(realpath $(lastword $(MAKEFILE_LIST))))
|
PLFA_DIR := $(shell dirname $(realpath $(lastword $(MAKEFILE_LIST))))
|
||||||
AGDA2HTML_FLAGS := --verbose --link-to-local-agda-names --use-jekyll=out/
|
AGDA2HTML_FLAGS := --verbose --link-to-local-agda-names --use-jekyll=out/
|
||||||
|
|
||||||
|
|
@ -21,6 +21,12 @@ out/%.md: src/%.lagda | out/
|
||||||
| sed '/^Generating.*/d; /^Warning\: HTML.*/d; /^reached from the.*/d; /^\s*$$/d'
|
| sed '/^Generating.*/d; /^Warning\: HTML.*/d; /^reached from the.*/d; /^\s*$$/d'
|
||||||
@sed -i '1 s|---|---\nsrc : $(<)|' $@
|
@sed -i '1 s|---|---\nsrc : $(<)|' $@
|
||||||
|
|
||||||
|
# should fix this -- it's the same as above
|
||||||
|
out/%.md: tspl/%.lagda | out/
|
||||||
|
agda2html $(AGDA2HTML_FLAGS) -i $< -o $@ 2>&1 \
|
||||||
|
| sed '/^Generating.*/d; /^Warning\: HTML.*/d; /^reached from the.*/d; /^\s*$$/d'
|
||||||
|
@sed -i '1 s|---|---\nsrc : $(<)|' $@
|
||||||
|
|
||||||
serve:
|
serve:
|
||||||
ruby -S bundle exec jekyll serve --incremental
|
ruby -S bundle exec jekyll serve --incremental
|
||||||
|
|
||||||
|
|
|
||||||
319
tspl/Assignment1.lagda
Normal file
319
tspl/Assignment1.lagda
Normal file
|
|
@ -0,0 +1,319 @@
|
||||||
|
---
|
||||||
|
title : "Assignment1: TSPL Assignment 1"
|
||||||
|
layout : page
|
||||||
|
permalink : /Assignment1/
|
||||||
|
---
|
||||||
|
|
||||||
|
\begin{code}
|
||||||
|
module Assignment1 where
|
||||||
|
\end{code}
|
||||||
|
|
||||||
|
## YOUR NAME AND EMAIL GOES HERE
|
||||||
|
|
||||||
|
## Introduction
|
||||||
|
|
||||||
|
This assignment is due **4pm Thursday 4 October** (Week 3).
|
||||||
|
|
||||||
|
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
|
||||||
|
|
||||||
|
\begin{code}
|
||||||
|
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.Relations using (_<_; z<s; s<s; zero; suc; even; odd)
|
||||||
|
\end{code}
|
||||||
|
|
||||||
|
## 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.
|
||||||
|
\begin{code}
|
||||||
|
data Bin : Set where
|
||||||
|
nil : Bin
|
||||||
|
x0_ : Bin → Bin
|
||||||
|
x1_ : Bin → Bin
|
||||||
|
\end{code}
|
||||||
|
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
|
||||||
|
|
||||||
|
\begin{code}
|
||||||
|
swap : ∀ (m n p : ℕ) → m + (n + p) ≡ n + (m + p)
|
||||||
|
swap m n p rewrite sym (+-assoc m n p) | +-comm m n | +-assoc n m p = {!!}
|
||||||
|
\end{code}
|
||||||
|
|
||||||
|
#### 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
|
||||||
|
|
||||||
|
\end{code}
|
||||||
|
(Hint: For each of these, you may first need to prove related
|
||||||
|
properties of `One`.)
|
||||||
365
tspl/Assignment2.lagda
Normal file
365
tspl/Assignment2.lagda
Normal file
|
|
@ -0,0 +1,365 @@
|
||||||
|
---
|
||||||
|
title : "Assignment2: TSPL Assignment 2"
|
||||||
|
layout : page
|
||||||
|
permalink : /Assignment2/
|
||||||
|
---
|
||||||
|
|
||||||
|
\begin{code}
|
||||||
|
module Assignment2 where
|
||||||
|
\end{code}
|
||||||
|
|
||||||
|
## YOUR NAME AND EMAIL GOES HERE
|
||||||
|
|
||||||
|
## Introduction
|
||||||
|
|
||||||
|
This assignment is due **4pm Thursday 18 October** (Week 5).
|
||||||
|
|
||||||
|
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
|
||||||
|
|
||||||
|
\begin{code}
|
||||||
|
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.Relations using (_<_; z<s; s<s)
|
||||||
|
open import Data.Product using (_×_; proj₁; proj₂) renaming (_,_ to ⟨_,_⟩)
|
||||||
|
open import Data.Unit using (⊤; tt)
|
||||||
|
open import Data.Sum using (_⊎_; inj₁; inj₂) renaming ([_,_] to case-⊎)
|
||||||
|
open import Data.Empty using (⊥; ⊥-elim)
|
||||||
|
open import Data.Bool.Base using (Bool; true; false; T; _∧_; _∨_; not)
|
||||||
|
open import Relation.Nullary using (¬_; Dec; yes; no)
|
||||||
|
open import Relation.Nullary.Decidable using (⌊_⌋; toWitness; fromWitness)
|
||||||
|
open import Relation.Nullary.Negation using (¬?)
|
||||||
|
open import Relation.Nullary.Product using (_×-dec_)
|
||||||
|
open import Relation.Nullary.Sum using (_⊎-dec_)
|
||||||
|
open import Relation.Nullary.Negation using (contraposition)
|
||||||
|
open import Data.Product using (Σ; _,_; ∃; Σ-syntax; ∃-syntax)
|
||||||
|
open import plfa.Relations using (_<_; z<s; s<s)
|
||||||
|
open import plfa.Isomorphism using (_≃_; ≃-sym; ≃-trans; _≲_; extensionality)
|
||||||
|
open plfa.Isomorphism.≃-Reasoning
|
||||||
|
\end{code}
|
||||||
|
|
||||||
|
## Equality
|
||||||
|
|
||||||
|
#### Exercise `≤-reasoning` (stretch)
|
||||||
|
|
||||||
|
The proof of monotonicity from
|
||||||
|
Chapter [Relations][plfa.Relations]
|
||||||
|
can be written in a more readable form by using an anologue of our
|
||||||
|
notation for `≡-reasoning`. Define `≤-reasoning` analogously, and use
|
||||||
|
it to write out an alternative proof that addition is monotonic with
|
||||||
|
regard to inequality. Rewrite both `+-monoˡ-≤` and `+-mono-≤`.
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
## Isomorphism
|
||||||
|
|
||||||
|
#### Exercise `≃-implies-≲`
|
||||||
|
|
||||||
|
Show that every isomorphism implies an embedding.
|
||||||
|
\begin{code}
|
||||||
|
postulate
|
||||||
|
≃-implies-≲ : ∀ {A B : Set}
|
||||||
|
→ A ≃ B
|
||||||
|
-----
|
||||||
|
→ A ≲ B
|
||||||
|
\end{code}
|
||||||
|
|
||||||
|
#### Exercise `_⇔_` (recommended) {#iff}
|
||||||
|
|
||||||
|
Define equivalence of propositions (also known as "if and only if") as follows.
|
||||||
|
\begin{code}
|
||||||
|
record _⇔_ (A B : Set) : Set where
|
||||||
|
field
|
||||||
|
to : A → B
|
||||||
|
from : B → A
|
||||||
|
|
||||||
|
open _⇔_
|
||||||
|
\end{code}
|
||||||
|
Show that equivalence is reflexive, symmetric, and transitive.
|
||||||
|
|
||||||
|
#### Exercise `Bin-embedding` (stretch) {#Bin-embedding}
|
||||||
|
|
||||||
|
Recall that Exercises
|
||||||
|
[Bin][plfa.Naturals#Bin] and
|
||||||
|
[Bin-laws][plfa.Induction#Bin-laws]
|
||||||
|
define a datatype of bitstrings representing natural numbers.
|
||||||
|
\begin{code}
|
||||||
|
data Bin : Set where
|
||||||
|
nil : Bin
|
||||||
|
x0_ : Bin → Bin
|
||||||
|
x1_ : Bin → Bin
|
||||||
|
\end{code}
|
||||||
|
And ask you to define the following functions:
|
||||||
|
|
||||||
|
to : ℕ → Bin
|
||||||
|
from : Bin → ℕ
|
||||||
|
|
||||||
|
which satisfy the following property:
|
||||||
|
|
||||||
|
from (to n) ≡ n
|
||||||
|
|
||||||
|
Using the above, establish that there is an embedding of `ℕ` into `Bin`.
|
||||||
|
Why is there not an isomorphism?
|
||||||
|
|
||||||
|
|
||||||
|
## Connectives
|
||||||
|
|
||||||
|
#### Exercise `⇔≃×` (recommended)
|
||||||
|
|
||||||
|
Show that `A ⇔ B` as defined [earlier][plfa.Isomorphism#iff]
|
||||||
|
is isomorphic to `(A → B) × (B → A)`.
|
||||||
|
|
||||||
|
#### Exercise `⊎-comm` (recommended)
|
||||||
|
|
||||||
|
Show sum is commutative up to isomorphism.
|
||||||
|
|
||||||
|
#### Exercise `⊎-assoc`
|
||||||
|
|
||||||
|
Show sum is associative up to ismorphism.
|
||||||
|
|
||||||
|
#### Exercise `⊥-identityˡ` (recommended)
|
||||||
|
|
||||||
|
Show zero is the left identity of addition.
|
||||||
|
|
||||||
|
#### Exercise `⊥-identityʳ`
|
||||||
|
|
||||||
|
Show zero is the right identity of addition.
|
||||||
|
|
||||||
|
#### Exercise `⊎-weak-×` (recommended)
|
||||||
|
|
||||||
|
Show that the following property holds.
|
||||||
|
\begin{code}
|
||||||
|
postulate
|
||||||
|
⊎-weak-× : ∀ {A B C : Set} → (A ⊎ B) × C → A ⊎ (B × C)
|
||||||
|
\end{code}
|
||||||
|
This is called a _weak distributive law_. Give the corresponding
|
||||||
|
distributive law, and explain how it relates to the weak version.
|
||||||
|
|
||||||
|
#### Exercise `⊎×-implies-×⊎`
|
||||||
|
|
||||||
|
Show that a disjunct of conjuncts implies a conjunct of disjuncts.
|
||||||
|
\begin{code}
|
||||||
|
postulate
|
||||||
|
⊎×-implies-×⊎ : ∀ {A B C D : Set} → (A × B) ⊎ (C × D) → (A ⊎ C) × (B ⊎ D)
|
||||||
|
\end{code}
|
||||||
|
Does the converse hold? If so, prove; if not, give a counterexample.
|
||||||
|
|
||||||
|
|
||||||
|
## Negation
|
||||||
|
|
||||||
|
#### Exercise `<-irreflexive` (recommended)
|
||||||
|
|
||||||
|
Using negation, show that
|
||||||
|
[strict inequality][plfa.Relations#strict-inequality]
|
||||||
|
is irreflexive, that is, `n < n` holds for no `n`.
|
||||||
|
|
||||||
|
|
||||||
|
#### Exercise `trichotomy`
|
||||||
|
|
||||||
|
Show that strict inequality satisfies
|
||||||
|
[trichotomy][plfa.Relations#trichotomy],
|
||||||
|
that is, for any naturals `m` and `n` exactly one of the following holds:
|
||||||
|
|
||||||
|
* `m < n`
|
||||||
|
* `m ≡ n`
|
||||||
|
* `m > n`
|
||||||
|
|
||||||
|
Here "exactly one" means that one of the three must hold, and each implies the
|
||||||
|
negation of the other two.
|
||||||
|
|
||||||
|
|
||||||
|
#### Exercise `⊎-dual-×` (recommended)
|
||||||
|
|
||||||
|
Show that conjunction, disjunction, and negation are related by a
|
||||||
|
version of De Morgan's Law.
|
||||||
|
|
||||||
|
¬ (A ⊎ B) ≃ (¬ A) × (¬ B)
|
||||||
|
|
||||||
|
This result is an easy consequence of something we've proved previously.
|
||||||
|
|
||||||
|
Do we also have the following?
|
||||||
|
|
||||||
|
¬ (A × B) ≃ (¬ A) ⊎ (¬ B)
|
||||||
|
|
||||||
|
If so, prove; if not, give a variant that does hold.
|
||||||
|
|
||||||
|
|
||||||
|
#### Exercise `Classical` (stretch)
|
||||||
|
|
||||||
|
Consider the following principles.
|
||||||
|
|
||||||
|
* Excluded Middle: `A ⊎ ¬ A`, for all `A`
|
||||||
|
* Double Negation Elimination: `¬ ¬ A → A`, for all `A`
|
||||||
|
* Peirce's Law: `((A → B) → A) → A`, for all `A` and `B`.
|
||||||
|
* Implication as disjunction: `(A → B) → ¬ A ⊎ B`, for all `A` and `B`.
|
||||||
|
* De Morgan: `¬ (¬ A × ¬ B) → A ⊎ B`, for all `A` and `B`.
|
||||||
|
|
||||||
|
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.
|
||||||
|
\begin{code}
|
||||||
|
Stable : Set → Set
|
||||||
|
Stable A = ¬ ¬ A → A
|
||||||
|
\end{code}
|
||||||
|
Show that any negated formula is stable, and that the conjunction
|
||||||
|
of two stable formulas is stable.
|
||||||
|
|
||||||
|
|
||||||
|
## Quantifiers
|
||||||
|
|
||||||
|
#### Exercise `∀-distrib-×` (recommended)
|
||||||
|
|
||||||
|
Show that universals distribute over conjunction.
|
||||||
|
\begin{code}
|
||||||
|
postulate
|
||||||
|
∀-distrib-× : ∀ {A : Set} {B C : A → Set} →
|
||||||
|
(∀ (x : A) → B x × C x) ≃ (∀ (x : A) → B x) × (∀ (x : A) → C x)
|
||||||
|
\end{code}
|
||||||
|
Compare this with the result (`→-distrib-×`) in
|
||||||
|
Chapter [Connectives][plfa.Connectives].
|
||||||
|
|
||||||
|
#### Exercise `⊎∀-implies-∀⊎`
|
||||||
|
|
||||||
|
Show that a disjunction of universals implies a universal of disjunctions.
|
||||||
|
\begin{code}
|
||||||
|
postulate
|
||||||
|
⊎∀-implies-∀⊎ : ∀ {A : Set} { B C : A → Set } →
|
||||||
|
(∀ (x : A) → B x) ⊎ (∀ (x : A) → C x) → ∀ (x : A) → B x ⊎ C x
|
||||||
|
\end{code}
|
||||||
|
Does the converse hold? If so, prove; if not, explain why.
|
||||||
|
|
||||||
|
#### Exercise `∃-distrib-⊎` (recommended)
|
||||||
|
|
||||||
|
Show that existentials distribute over disjunction.
|
||||||
|
\begin{code}
|
||||||
|
postulate
|
||||||
|
∃-distrib-⊎ : ∀ {A : Set} {B C : A → Set} →
|
||||||
|
∃[ x ] (B x ⊎ C x) ≃ (∃[ x ] B x) ⊎ (∃[ x ] C x)
|
||||||
|
\end{code}
|
||||||
|
|
||||||
|
#### Exercise `∃×-implies-×∃`
|
||||||
|
|
||||||
|
Show that an existential of conjunctions implies a conjunction of existentials.
|
||||||
|
\begin{code}
|
||||||
|
postulate
|
||||||
|
∃×-implies-×∃ : ∀ {A : Set} { B C : A → Set } →
|
||||||
|
∃[ x ] (B x × C x) → (∃[ x ] B x) × (∃[ x ] C x)
|
||||||
|
\end{code}
|
||||||
|
Does the converse hold? If so, prove; if not, explain why.
|
||||||
|
|
||||||
|
#### Exercise `∃-even-odd`
|
||||||
|
|
||||||
|
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.
|
||||||
|
|
||||||
|
#### Exercise `∃-+-≤`
|
||||||
|
|
||||||
|
Show that `y ≤ z` holds if and only if there exists a `x` such that
|
||||||
|
`x + y ≡ z`.
|
||||||
|
|
||||||
|
#### Exercise `∃¬-implies-¬∀` (recommended)
|
||||||
|
|
||||||
|
Show that existential of a negation implies negation of a universal.
|
||||||
|
\begin{code}
|
||||||
|
postulate
|
||||||
|
∃¬-implies-¬∀ : ∀ {A : Set} {B : A → Set}
|
||||||
|
→ ∃[ x ] (¬ B x)
|
||||||
|
--------------
|
||||||
|
→ ¬ (∀ x → B x)
|
||||||
|
\end{code}
|
||||||
|
Does the converse hold? If so, prove; if not, explain why.
|
||||||
|
|
||||||
|
|
||||||
|
#### Exercise `Bin-isomorphism` (stretch) {#Bin-isomorphism}
|
||||||
|
|
||||||
|
Recall that Exercises
|
||||||
|
[Bin][plfa.Naturals#Bin],
|
||||||
|
[Bin-laws][plfa.Induction#Bin-laws], and
|
||||||
|
[Bin-predicates][plfa.Relations#Bin-predicates]
|
||||||
|
define a datatype of bitstrings representing natural numbers.
|
||||||
|
|
||||||
|
data Bin : Set where
|
||||||
|
nil : Bin
|
||||||
|
x0_ : Bin → Bin
|
||||||
|
x1_ : Bin → Bin
|
||||||
|
|
||||||
|
And ask you to define the following functions and predicates.
|
||||||
|
|
||||||
|
to : ℕ → Bin
|
||||||
|
from : Bin → ℕ
|
||||||
|
Can : Bin → Set
|
||||||
|
|
||||||
|
And to establish the following properties.
|
||||||
|
|
||||||
|
from (to n) ≡ n
|
||||||
|
|
||||||
|
----------
|
||||||
|
Can (to n)
|
||||||
|
|
||||||
|
Can x
|
||||||
|
---------------
|
||||||
|
to (from x) ≡ x
|
||||||
|
|
||||||
|
Using the above, establish that there is an isomorphism between `ℕ` and
|
||||||
|
`∃[ x ](Can x)`.
|
||||||
|
|
||||||
|
|
||||||
|
## Decidable
|
||||||
|
|
||||||
|
#### Exercise `_<?_` (recommended)
|
||||||
|
|
||||||
|
Analogous to the function above, define a function to decide strict inequality.
|
||||||
|
\begin{code}
|
||||||
|
postulate
|
||||||
|
_<?_ : ∀ (m n : ℕ) → Dec (m < n)
|
||||||
|
\end{code}
|
||||||
|
|
||||||
|
#### Exercise `_≡ℕ?_`
|
||||||
|
|
||||||
|
Define a function to decide whether two naturals are equal.
|
||||||
|
\begin{code}
|
||||||
|
postulate
|
||||||
|
_≡ℕ?_ : ∀ (m n : ℕ) → Dec (m ≡ n)
|
||||||
|
\end{code}
|
||||||
|
|
||||||
|
|
||||||
|
#### Exercise `erasure`
|
||||||
|
|
||||||
|
Show that erasure relates corresponding boolean and decidable operations.
|
||||||
|
\begin{code}
|
||||||
|
postulate
|
||||||
|
∧-× : ∀ {A B : Set} (x : Dec A) (y : Dec B) → ⌊ x ⌋ ∧ ⌊ y ⌋ ≡ ⌊ x ×-dec y ⌋
|
||||||
|
∨-× : ∀ {A B : Set} (x : Dec A) (y : Dec B) → ⌊ x ⌋ ∨ ⌊ y ⌋ ≡ ⌊ x ⊎-dec y ⌋
|
||||||
|
not-¬ : ∀ {A : Set} (x : Dec A) → not ⌊ x ⌋ ≡ ⌊ ¬? x ⌋
|
||||||
|
\end{code}
|
||||||
|
|
||||||
|
#### Exercise `iff-erasure` (recommended)
|
||||||
|
|
||||||
|
Give analogues of the `_⇔_` operation from
|
||||||
|
Chapter [Isomorphism][plfa.Isomorphism#iff],
|
||||||
|
operation on booleans and decidables, and also show the corresponding erasure.
|
||||||
|
\begin{code}
|
||||||
|
postulate
|
||||||
|
_iff_ : Bool → Bool → Bool
|
||||||
|
_⇔-dec_ : ∀ {A B : Set} → Dec A → Dec B → Dec (A ⇔ B)
|
||||||
|
iff-⇔ : ∀ {A B : Set} (x : Dec A) (y : Dec B) → ⌊ x ⌋ iff ⌊ y ⌋ ≡ ⌊ x ⇔-dec y ⌋
|
||||||
|
\end{code}
|
||||||
|
|
||||||
382
tspl/Assignment3.lagda
Normal file
382
tspl/Assignment3.lagda
Normal file
|
|
@ -0,0 +1,382 @@
|
||||||
|
---
|
||||||
|
title : "Assignment3: TSPL Assignment 3"
|
||||||
|
layout : page
|
||||||
|
permalink : /Assignment3/
|
||||||
|
---
|
||||||
|
|
||||||
|
\begin{code}
|
||||||
|
module Assignment3 where
|
||||||
|
\end{code}
|
||||||
|
|
||||||
|
## YOUR NAME AND EMAIL GOES HERE
|
||||||
|
|
||||||
|
## Introduction
|
||||||
|
|
||||||
|
This assignment is due **4pm Thursday 1 November** (Week 7).
|
||||||
|
|
||||||
|
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
|
||||||
|
|
||||||
|
\begin{code}
|
||||||
|
import Relation.Binary.PropositionalEquality as Eq
|
||||||
|
open Eq using (_≡_; refl; cong; sym)
|
||||||
|
open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; _≡⟨_⟩_; _∎)
|
||||||
|
open import Data.Bool.Base using (Bool; true; false; T; _∧_; _∨_; not)
|
||||||
|
open import Data.Nat using (ℕ; zero; suc; _+_; _*_; _∸_; _≤_; s≤s; z≤n)
|
||||||
|
open import Data.Nat.Properties using
|
||||||
|
(+-assoc; +-identityˡ; +-identityʳ; *-assoc; *-identityˡ; *-identityʳ)
|
||||||
|
open import Relation.Nullary using (¬_; Dec; yes; no)
|
||||||
|
open import Data.Product using (_×_; ∃; ∃-syntax) renaming (_,_ to ⟨_,_⟩)
|
||||||
|
open import Data.Empty using (⊥; ⊥-elim)
|
||||||
|
open import Function using (_∘_)
|
||||||
|
open import Algebra.Structures using (IsMonoid)
|
||||||
|
open import Level using (Level)
|
||||||
|
open import Relation.Unary using (Decidable)
|
||||||
|
open import plfa.Relations using (_<_; z<s; s<s)
|
||||||
|
open import plfa.Isomorphism using (_≃_; ≃-sym; ≃-trans; _≲_; extensionality)
|
||||||
|
open plfa.Isomorphism.≃-Reasoning
|
||||||
|
open import plfa.Lists using (List; []; _∷_; [_]; [_,_]; [_,_,_]; [_,_,_,_];
|
||||||
|
_++_; reverse; map; foldr; sum; All; Any; here; there; _∈_)
|
||||||
|
open import plfa.Lambda hiding (ƛ′_⇒_; case′_[zero⇒_|suc_⇒_]; μ′_⇒_; plus′)
|
||||||
|
open import plfa.Properties hiding (value?; unstuck; preserves; wttdgs)
|
||||||
|
\end{code}
|
||||||
|
|
||||||
|
#### Exercise `reverse-++-commute` (recommended)
|
||||||
|
|
||||||
|
Show that the reverse of one list appended to another is the
|
||||||
|
reverse of the second appended to the reverse of the first.
|
||||||
|
\begin{code}
|
||||||
|
postulate
|
||||||
|
reverse-++-commute : ∀ {A : Set} {xs ys : List A}
|
||||||
|
→ reverse (xs ++ ys) ≡ reverse ys ++ reverse xs
|
||||||
|
\end{code}
|
||||||
|
|
||||||
|
#### Exercise `reverse-involutive` (recommended)
|
||||||
|
|
||||||
|
A function is an _involution_ if when applied twice it acts
|
||||||
|
as the identity function. Show that reverse is an involution.
|
||||||
|
\begin{code}
|
||||||
|
postulate
|
||||||
|
reverse-involutive : ∀ {A : Set} {xs : List A}
|
||||||
|
→ reverse (reverse xs) ≡ xs
|
||||||
|
\end{code}
|
||||||
|
|
||||||
|
#### Exercise `map-compose`
|
||||||
|
|
||||||
|
Prove that the map of a composition is equal to the composition of two maps.
|
||||||
|
\begin{code}
|
||||||
|
postulate
|
||||||
|
map-compose : ∀ {A B C : Set} {f : A → B} {g : B → C}
|
||||||
|
→ map (g ∘ f) ≡ map g ∘ map f
|
||||||
|
\end{code}
|
||||||
|
The last step of the proof requires extensionality.
|
||||||
|
|
||||||
|
#### Exercise `map-++-commute`
|
||||||
|
|
||||||
|
Prove the following relationship between map and append.
|
||||||
|
\begin{code}
|
||||||
|
postulate
|
||||||
|
map-++-commute : ∀ {A B : Set} {f : A → B} {xs ys : List A}
|
||||||
|
→ map f (xs ++ ys) ≡ map f xs ++ map f ys
|
||||||
|
\end{code}
|
||||||
|
|
||||||
|
#### Exercise `map-Tree`
|
||||||
|
|
||||||
|
Define a type of trees with leaves of type `A` and internal
|
||||||
|
nodes of type `B`.
|
||||||
|
\begin{code}
|
||||||
|
data Tree (A B : Set) : Set where
|
||||||
|
leaf : A → Tree A B
|
||||||
|
node : Tree A B → B → Tree A B → Tree A B
|
||||||
|
\end{code}
|
||||||
|
Define a suitabve map operator over trees.
|
||||||
|
\begin{code}
|
||||||
|
postulate
|
||||||
|
map-Tree : ∀ {A B C D : Set}
|
||||||
|
→ (A → C) → (B → D) → Tree A B → Tree C D
|
||||||
|
\end{code}
|
||||||
|
|
||||||
|
#### Exercise `product` (recommended)
|
||||||
|
|
||||||
|
Use fold to define a function to find the product of a list of numbers.
|
||||||
|
For example,
|
||||||
|
|
||||||
|
product [ 1 , 2 , 3 , 4 ] ≡ 24
|
||||||
|
|
||||||
|
#### Exercise `foldr-++` (recommended)
|
||||||
|
|
||||||
|
Show that fold and append are related as follows.
|
||||||
|
\begin{code}
|
||||||
|
postulate
|
||||||
|
foldr-++ : ∀ {A B : Set} (_⊗_ : A → B → B) (e : B) (xs ys : List A) →
|
||||||
|
foldr _⊗_ e (xs ++ ys) ≡ foldr _⊗_ (foldr _⊗_ e ys) xs
|
||||||
|
\end{code}
|
||||||
|
|
||||||
|
|
||||||
|
#### Exercise `map-is-foldr`
|
||||||
|
|
||||||
|
Show that map can be defined using fold.
|
||||||
|
\begin{code}
|
||||||
|
postulate
|
||||||
|
map-is-foldr : ∀ {A B : Set} {f : A → B} →
|
||||||
|
map f ≡ foldr (λ x xs → f x ∷ xs) []
|
||||||
|
\end{code}
|
||||||
|
This requires extensionality.
|
||||||
|
|
||||||
|
#### Exercise `fold-Tree`
|
||||||
|
|
||||||
|
Define a suitable fold function for the type of trees given earlier.
|
||||||
|
\begin{code}
|
||||||
|
postulate
|
||||||
|
fold-Tree : ∀ {A B C : Set}
|
||||||
|
→ (A → C) → (C → B → C → C) → Tree A B → C
|
||||||
|
\end{code}
|
||||||
|
|
||||||
|
#### Exercise `map-is-fold-Tree`
|
||||||
|
|
||||||
|
Demonstrate an anologue of `map-is-foldr` for the type of trees.
|
||||||
|
|
||||||
|
#### Exercise `sum-downFrom` (stretch)
|
||||||
|
|
||||||
|
Define a function that counts down as follows.
|
||||||
|
\begin{code}
|
||||||
|
downFrom : ℕ → List ℕ
|
||||||
|
downFrom zero = []
|
||||||
|
downFrom (suc n) = n ∷ downFrom n
|
||||||
|
\end{code}
|
||||||
|
For example,
|
||||||
|
\begin{code}
|
||||||
|
_ : downFrom 3 ≡ [ 2 , 1 , 0 ]
|
||||||
|
_ = refl
|
||||||
|
\end{code}
|
||||||
|
Prove that the sum of the numbers `(n - 1) + ⋯ + 0` is
|
||||||
|
equal to `n * (n ∸ 1) / 2`.
|
||||||
|
\begin{code}
|
||||||
|
postulate
|
||||||
|
sum-downFrom : ∀ (n : ℕ)
|
||||||
|
→ sum (downFrom n) * 2 ≡ n * (n ∸ 1)
|
||||||
|
\end{code}
|
||||||
|
|
||||||
|
|
||||||
|
#### Exercise `foldl`
|
||||||
|
|
||||||
|
Define a function `foldl` which is analogous to `foldr`, but where
|
||||||
|
operations associate to the left rather than the right. For example,
|
||||||
|
|
||||||
|
foldr _⊗_ e [ x , y , z ] = x ⊗ (y ⊗ (z ⊗ e))
|
||||||
|
foldl _⊗_ e [ x , y , z ] = ((e ⊗ x) ⊗ y) ⊗ z
|
||||||
|
|
||||||
|
|
||||||
|
#### Exercise `foldr-monoid-foldl`
|
||||||
|
|
||||||
|
Show that if `_⊕_` and `e` form a monoid, then `foldr _⊗_ e` and
|
||||||
|
`foldl _⊗_ e` always compute the same result.
|
||||||
|
|
||||||
|
|
||||||
|
#### Exercise `Any-++-⇔` (recommended)
|
||||||
|
|
||||||
|
Prove a result similar to `All-++-↔`, but with `Any` in place of `All`, and a suitable
|
||||||
|
replacement for `_×_`. As a consequence, demonstrate an equivalence relating
|
||||||
|
`_∈_` and `_++_`.
|
||||||
|
|
||||||
|
|
||||||
|
#### Exercise `All-++-≃` (stretch)
|
||||||
|
|
||||||
|
Show that the equivalence `All-++-⇔` can be extended to an isomorphism.
|
||||||
|
|
||||||
|
|
||||||
|
#### Exercise `¬Any≃All¬` (stretch)
|
||||||
|
|
||||||
|
First generalise composition to arbitrary levels, using
|
||||||
|
[universe polymorphism][plfa.Equality#unipoly].
|
||||||
|
\begin{code}
|
||||||
|
_∘′_ : ∀ {ℓ₁ ℓ₂ ℓ₃ : Level} {A : Set ℓ₁} {B : Set ℓ₂} {C : Set ℓ₃}
|
||||||
|
→ (B → C) → (A → B) → A → C
|
||||||
|
(g ∘′ f) x = g (f x)
|
||||||
|
\end{code}
|
||||||
|
|
||||||
|
Show that `Any` and `All` satisfy a version of De Morgan's Law.
|
||||||
|
\begin{code}
|
||||||
|
postulate
|
||||||
|
¬Any≃All¬ : ∀ {A : Set} (P : A → Set) (xs : List A)
|
||||||
|
→ (¬_ ∘′ Any P) xs ≃ All (¬_ ∘′ P) xs
|
||||||
|
\end{code}
|
||||||
|
|
||||||
|
Do we also have the following?
|
||||||
|
\begin{code}
|
||||||
|
postulate
|
||||||
|
¬All≃Any¬ : ∀ {A : Set} (P : A → Set) (xs : List A)
|
||||||
|
→ (¬_ ∘′ All P) xs ≃ Any (¬_ ∘′ P) xs
|
||||||
|
\end{code}
|
||||||
|
If so, prove; if not, explain why.
|
||||||
|
|
||||||
|
|
||||||
|
#### Exercise `any?` (stretch)
|
||||||
|
|
||||||
|
Just as `All` has analogues `all` and `all?` which determine whether a
|
||||||
|
predicate holds for every element of a list, so does `Any` have
|
||||||
|
analogues `any` and `any?` which determine whether a predicates holds
|
||||||
|
for some element of a list. Give their definitions.
|
||||||
|
|
||||||
|
|
||||||
|
#### Exercise `filter?` (stretch)
|
||||||
|
|
||||||
|
Define the following variant of the traditional `filter` function on lists,
|
||||||
|
which given a list and a decidable predicate returns all elements of the
|
||||||
|
list satisfying the predicate.
|
||||||
|
\begin{code}
|
||||||
|
postulate
|
||||||
|
filter? : ∀ {A : Set} {P : A → Set}
|
||||||
|
→ (P? : Decidable P) → List A → ∃[ ys ]( All P ys )
|
||||||
|
\end{code}
|
||||||
|
|
||||||
|
|
||||||
|
## Lambda
|
||||||
|
|
||||||
|
#### Exercise `mul` (recommended)
|
||||||
|
|
||||||
|
Write out the definition of a lambda term that multiplies
|
||||||
|
two natural numbers.
|
||||||
|
|
||||||
|
|
||||||
|
#### Exercise `primed` (stretch)
|
||||||
|
|
||||||
|
We can make examples with lambda terms slighly easier to write
|
||||||
|
by adding the following definitions.
|
||||||
|
\begin{code}
|
||||||
|
ƛ′_⇒_ : Term → Term → Term
|
||||||
|
ƛ′ (` x) ⇒ N = ƛ x ⇒ N
|
||||||
|
ƛ′ _ ⇒ _ = ⊥-elim impossible
|
||||||
|
where postulate impossible : ⊥
|
||||||
|
|
||||||
|
case′_[zero⇒_|suc_⇒_] : Term → Term → Term → Term → Term
|
||||||
|
case′ L [zero⇒ M |suc (` x) ⇒ N ] = case L [zero⇒ M |suc x ⇒ N ]
|
||||||
|
case′ _ [zero⇒ _ |suc _ ⇒ _ ] = ⊥-elim impossible
|
||||||
|
where postulate impossible : ⊥
|
||||||
|
|
||||||
|
μ′_⇒_ : Term → Term → Term
|
||||||
|
μ′ (` x) ⇒ N = μ x ⇒ N
|
||||||
|
μ′ _ ⇒ _ = ⊥-elim impossible
|
||||||
|
where postulate impossible : ⊥
|
||||||
|
\end{code}
|
||||||
|
The definition of `plus` can now be written as follows.
|
||||||
|
\begin{code}
|
||||||
|
plus′ : Term
|
||||||
|
plus′ = μ′ + ⇒ ƛ′ m ⇒ ƛ′ n ⇒
|
||||||
|
case′ m
|
||||||
|
[zero⇒ n
|
||||||
|
|suc m ⇒ `suc (+ · m · n) ]
|
||||||
|
where
|
||||||
|
+ = ` "+"
|
||||||
|
m = ` "m"
|
||||||
|
n = ` "n"
|
||||||
|
\end{code}
|
||||||
|
Write out the definition of multiplication in the same style.
|
||||||
|
|
||||||
|
#### Exercise `_[_:=_]′` (stretch)
|
||||||
|
|
||||||
|
The definition of substitution above has three clauses (`ƛ`, `case`,
|
||||||
|
and `μ`) that invoke a with clause to deal with bound variables.
|
||||||
|
Rewrite the definition to factor the common part of these three
|
||||||
|
clauses into a single function, defined by mutual recursion with
|
||||||
|
substitution.
|
||||||
|
|
||||||
|
|
||||||
|
#### Exercise `—↠≃—↠′`
|
||||||
|
|
||||||
|
Show that the two notions of reflexive and transitive closure
|
||||||
|
above are isomorphic.
|
||||||
|
|
||||||
|
|
||||||
|
#### Exercise `plus-example`
|
||||||
|
|
||||||
|
Write out the reduction sequence demonstrating that one plus one is two.
|
||||||
|
|
||||||
|
|
||||||
|
#### Exercise `mul-type` (recommended)
|
||||||
|
|
||||||
|
Using the term `mul` you defined earlier, write out the derivation
|
||||||
|
showing that it is well-typed.
|
||||||
|
|
||||||
|
|
||||||
|
## Properties
|
||||||
|
|
||||||
|
|
||||||
|
#### Exercise `Progress-≃`
|
||||||
|
|
||||||
|
Show that `Progress M` is isomorphic to `Value M ⊎ ∃[ N ](M —→ N)`.
|
||||||
|
|
||||||
|
|
||||||
|
#### Exercise `progress′`
|
||||||
|
|
||||||
|
Write out the proof of `progress′` in full, and compare it to the
|
||||||
|
proof of `progress` above.
|
||||||
|
|
||||||
|
|
||||||
|
#### Exercise `value?`
|
||||||
|
|
||||||
|
Combine `progress` and `—→¬V` to write a program that decides
|
||||||
|
whether a well-typed term is a value.
|
||||||
|
\begin{code}
|
||||||
|
postulate
|
||||||
|
value? : ∀ {A M} → ∅ ⊢ M ⦂ A → Dec (Value M)
|
||||||
|
\end{code}
|
||||||
|
|
||||||
|
|
||||||
|
#### Exercise `subst′` (stretch)
|
||||||
|
|
||||||
|
Rewrite `subst` to work with the modified definition `_[_:=_]′`
|
||||||
|
from the exercise in the previous chapter. As before, this
|
||||||
|
should factor dealing with bound variables into a single function,
|
||||||
|
defined by mutual recursion with the proof that substitution
|
||||||
|
preserves types.
|
||||||
|
|
||||||
|
|
||||||
|
#### Exercise `mul-example` (recommended)
|
||||||
|
|
||||||
|
Using the evaluator, confirm that two times two is four.
|
||||||
|
|
||||||
|
|
||||||
|
#### Exercise: `progress-preservation`
|
||||||
|
|
||||||
|
Without peeking at their statements above, write down the progress
|
||||||
|
and preservation theorems for the simply typed lambda-calculus.
|
||||||
|
|
||||||
|
|
||||||
|
#### Exercise `subject-expansion`
|
||||||
|
|
||||||
|
We say that `M` _reduces_ to `N` if `M —→ N`,
|
||||||
|
and conversely that `M` _expands_ to `N` if `N —→ M`.
|
||||||
|
The preservation property is sometimes called _subject reduction_.
|
||||||
|
Its opposite is _subject expansion_, which holds if
|
||||||
|
`M —→ N` and `∅ ⊢ N ⦂ A` imply `∅ ⊢ M ⦂ A`.
|
||||||
|
Find two counter-examples to subject expansion, one
|
||||||
|
with case expressions and one not involving case expressions.
|
||||||
|
|
||||||
|
|
||||||
|
#### Exercise `stuck`
|
||||||
|
|
||||||
|
Give an example of an ill-typed term that does get stuck.
|
||||||
|
|
||||||
|
|
||||||
|
#### Exercise `unstuck` (recommended)
|
||||||
|
|
||||||
|
Provide proofs of the three postulates, `unstuck`, `preserves`, and `wttdgs` above.
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
1169
tspl/Assignment4.lagda
Normal file
1169
tspl/Assignment4.lagda
Normal file
File diff suppressed because it is too large
Load diff
BIN
tspl/Assignment5.pdf
Normal file
BIN
tspl/Assignment5.pdf
Normal file
Binary file not shown.
422
tspl/Assignment5.tex
Normal file
422
tspl/Assignment5.tex
Normal file
|
|
@ -0,0 +1,422 @@
|
||||||
|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||||
|
%
|
||||||
|
% I N F O R M A T I C S
|
||||||
|
% Honours Exam LaTeX Template for Exam Authors
|
||||||
|
%
|
||||||
|
% Created: 12-Oct-2009 by G.O.Passmore.
|
||||||
|
% Last Updated: 10-Sep-2018 by I. Murray
|
||||||
|
%
|
||||||
|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||||
|
|
||||||
|
%%% The following define the status of the exam papers in the order
|
||||||
|
%%% required. Simply remove the comment (i.e., the % symbol) just
|
||||||
|
%%% before the appropriate one and comment the others out.
|
||||||
|
|
||||||
|
%\newcommand\status{\internal}
|
||||||
|
%\newcommand\status{\external}
|
||||||
|
\newcommand\status{\final}
|
||||||
|
|
||||||
|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||||
|
|
||||||
|
%%% The following three lines are always required. You may add
|
||||||
|
%%% custom packages to the one already defined if necessary.
|
||||||
|
|
||||||
|
\documentclass{examhons2018}
|
||||||
|
\usepackage{amssymb}
|
||||||
|
\usepackage{amsmath}
|
||||||
|
\usepackage{semantic}
|
||||||
|
\usepackage{stix}
|
||||||
|
|
||||||
|
%%% Uncomment the \checkmarksfalse line if the macros that check the
|
||||||
|
%%% mark totals cause problems. However, please do not make your
|
||||||
|
%%% questions add up to a non-standard number of marks without
|
||||||
|
%%% permission of the convenor.
|
||||||
|
%\checkmarksfalse
|
||||||
|
|
||||||
|
\begin{document}
|
||||||
|
|
||||||
|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||||
|
%
|
||||||
|
% Replace {ad} below with the ITO code for your course. This will
|
||||||
|
% be used by the ITO LaTeX installation to install course-specific
|
||||||
|
% data into the exam versions it produces from this document.
|
||||||
|
%
|
||||||
|
% Your choices are (in course title order):
|
||||||
|
%
|
||||||
|
% {anlp} - Acc. Natural Language Processing (MSc)
|
||||||
|
% {aleone} - Adaptive Learning Environments 1 (Inf4)
|
||||||
|
% {adbs} - Advanced Databases (Inf4)
|
||||||
|
% {av} - Advanced Vision (Inf4)
|
||||||
|
% {av-dl} - Advanced Vision - distance learning (MSc)
|
||||||
|
% {apl} - Advances in Programming Languages (Inf4)
|
||||||
|
% {abs} - Agent Based Systems [L10] (Inf3)
|
||||||
|
% {afds} - Algorithmic Foundations of Data Science (MSc)
|
||||||
|
% {agta} - Algorithmic Game Theory and its Apps. (MSc)
|
||||||
|
% {ads} - Algorithms and Data Structures (Inf3)
|
||||||
|
% {ad} - Applied Databases (MSc)
|
||||||
|
% {aipf} - Artificial Intelligence Present and Future (MSc)
|
||||||
|
% {ar} - Automated Reasoning (Inf3)
|
||||||
|
% {asr} - Automatic Speech Recognition (Inf4)
|
||||||
|
% {bioone} - Bioinformatics 1 (MSc)
|
||||||
|
% {biotwo} - Bioinformatics 2 (MSc)
|
||||||
|
% {bdl} - Blockchains and Distributed Ledgers (Inf4)
|
||||||
|
% {cqi} - Categories and Quantum Informatics (MSc)
|
||||||
|
% {copt} - Compiler Opimisation [L11] (Inf4)
|
||||||
|
% {ct} - Compiling Techniques (Inf3)
|
||||||
|
% {ccs} - Computational Cognitive Science (Inf3)
|
||||||
|
% {cmc} - Computational Complexity (Inf4)
|
||||||
|
% {ca} - Computer Algebra (Inf4)
|
||||||
|
% {cav} - Computer Animation and Visualisation (Inf4)
|
||||||
|
% {car} - Computer Architecture (Inf3)
|
||||||
|
% {comn} - Computer Comms. and Networks (Inf3)
|
||||||
|
% {cd} - Computer Design (Inf3)
|
||||||
|
% {cg} - Computer Graphics [L11] (Inf4)
|
||||||
|
% {cn} - Computer Networking [L11] (Inf4)
|
||||||
|
% {cp} - Computer Prog. Skills and Concepts (nonhons)
|
||||||
|
% {cs} - Computer Security (Inf3)
|
||||||
|
% {dds} - Data, Design and Society (nonhons)
|
||||||
|
% {dme} - Data Mining and Exploration (Msc)
|
||||||
|
% {dbs} - Database Systems (Inf3)
|
||||||
|
% {dmr} - Decision Making in Robots and Autonomous Agents(MSc)
|
||||||
|
% {dmmr} - Discrete Maths. and Math. Reasoning (nonhons)
|
||||||
|
% {ds} - Distributed Systems [L11] (Inf4)
|
||||||
|
% {epl} - Elements of Programming Languages (Inf3)
|
||||||
|
% {es} - Embedded Software (Inf4)
|
||||||
|
% {exc} - Extreme Computing (Inf4)
|
||||||
|
% {fv} - Formal Verification (Inf4)
|
||||||
|
% {fnlp} - Foundations of Natural Language Processing (Inf3)
|
||||||
|
% {hci} - Human-Computer Interaction [L11] (Inf4)
|
||||||
|
% {infonea} - Informatics 1 - Introduction to Computation(nonhons)
|
||||||
|
% different sittings for INF1A programming exams
|
||||||
|
% {infoneapone} - Informatics 1 - Introduction to Computation(nonhons)
|
||||||
|
% {infoneaptwo} - Informatics 1 - Introduction to Computation(nonhons)
|
||||||
|
% {infoneapthree} - Informatics 1 - Introduction to Computation(nonhons)
|
||||||
|
% {infonecg} - Informatics 1 - Cognitive Science (nonhons)
|
||||||
|
% {infonecl} - Informatics 1 - Computation and Logic (nonhons)
|
||||||
|
% {infoneda} - Informatics 1 - Data and Analysis (nonhons)
|
||||||
|
% {infonefp} - Informatics 1 - Functional Programming (nonhons)
|
||||||
|
% If there are two sittings of FP, use infonefpam for the first
|
||||||
|
% paper and infonefppm for the second sitting.
|
||||||
|
% {infoneop} - Informatics 1 - Object-Oriented Programming(nonhons)
|
||||||
|
% If there are two sittings of OOP, use infoneopam for the first
|
||||||
|
% paper and infoneoppm for the second sitting.
|
||||||
|
% {inftwoa} - Informatics 2A: Proc. F&N Languages (nonhons)
|
||||||
|
% {inftwob} - Informatics 2B: Algs., D.Structs., Learning(nonhons)
|
||||||
|
% {inftwoccs}- Informatics 2C-CS: Computer Systems (nonhons)
|
||||||
|
% {inftwocse}- Informatics 2C: Software Engineering (nonhons)
|
||||||
|
% {inftwod} - Informatics 2D: Reasoning and Agents (nonhons)
|
||||||
|
% {iar} - Intelligent Autonomous Robotics (Inf4)
|
||||||
|
% {it} - Information Theory (MSc)
|
||||||
|
% {imc} - Introduction to Modern Cryptography (Inf4)
|
||||||
|
% {iotssc} - Internet of Things, Systems, Security and the Cloud (Inf4)
|
||||||
|
% (iqc) - Introduction to Quantum Computing (Inf4)
|
||||||
|
% (itcs) - Introduction to Theoretical Computer Science (Inf3)
|
||||||
|
% {ivc} - Image and Vision Computing (MSc)
|
||||||
|
% {ivr} - Introduction to Vision and Robotics (Inf3)
|
||||||
|
% {ivr-dl} - Introduction to Vision and Robotics - distance learning (Msc)
|
||||||
|
% {iaml} - Introductory Applied Machine Learning (MSc)
|
||||||
|
% {iaml-dl} - Introductory Applied Machine Learning - distance learning (MSc)
|
||||||
|
% {lpt} - Logic Programming - Theory (Inf3)
|
||||||
|
% {lpp} - Logic Programming - Programming (Inf3)
|
||||||
|
% {mlpr} - Machine Learning & Pattern Recognition (Inf4)
|
||||||
|
% {mt} - Machine Translation (Inf4)
|
||||||
|
% {mi} - Music Informatics (MSc)
|
||||||
|
% {nlu} - Natural Language Understanding [L11] (Inf4)
|
||||||
|
% {nc} - Neural Computation (MSc)
|
||||||
|
% {nat} - Natural Computing (MSc)
|
||||||
|
% {nluplus} - Natural Language Understanding, Generation, and Machine Translation(MSc)
|
||||||
|
% {nip} - Neural Information Processing (MSc)
|
||||||
|
% {os} - Operating Systems (Inf3)
|
||||||
|
% {pa} - Parallel Architectures [L11] (Inf4)
|
||||||
|
% {pdiot} - Principles and Design of IoT Systems (Inf4)
|
||||||
|
% {ppls} - Parallel Prog. Langs. and Sys. [L11] (Inf4)
|
||||||
|
% {pm} - Performance Modelling (Inf4)
|
||||||
|
% {pmr} - Probabilistic Modelling and Reasoning (MSc)
|
||||||
|
% {pi} - Professional Issues (Inf3)
|
||||||
|
% {rc} - Randomness and Computation (Inf4)
|
||||||
|
% {rl} - Reinforcement Learning (MSc)
|
||||||
|
% {rlsc} - Robot Learning and Sensorimotor Control (MSc)
|
||||||
|
% {rss} - Robotics: Science and Systems (MSc)
|
||||||
|
% {sp} - Secure Programming (Inf4)
|
||||||
|
% {sws} - Semantic Web Systems (Inf4)
|
||||||
|
% {stn} - Social and Technological Networks (Inf4)
|
||||||
|
% {sapm} - Software Arch., Proc. and Mgmt. [L11] (Inf4)
|
||||||
|
% {sdm} - Software Design and Modelling (Inf3)
|
||||||
|
% {st} - Software Testing (Inf3)
|
||||||
|
% {ttds} - Text Technologies for Data Science (Inf4)
|
||||||
|
% {tspl} - Types and Semantics for Programming Langs. (Inf4)
|
||||||
|
% {usec} - Usable Security and Privacy (Inf4)
|
||||||
|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||||
|
|
||||||
|
\setcourse{tspl}
|
||||||
|
\initcoursedata
|
||||||
|
|
||||||
|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||||
|
%
|
||||||
|
% Set your exam rubric type.
|
||||||
|
%
|
||||||
|
% Most courses in the School have exams that add up to 50 marks,
|
||||||
|
% and your choices are:
|
||||||
|
% {qu1_and_either_qu2_or_qu3, any_two_of_three, do_exam}
|
||||||
|
% (which include the "CALCULATORS MAY NOT BE USED..." text), or
|
||||||
|
% {qu1_and_either_qu2_or_qu3_calc, any_two_of_three_calc, do_exam_calc}
|
||||||
|
% (which DO NOT include the "CALCULATORS MAY NOT BE USED..." text), or
|
||||||
|
% {custom}.
|
||||||
|
%
|
||||||
|
% Note, if you opt to create a custom rubric, you must:
|
||||||
|
%
|
||||||
|
% (i) **have permission** from the appropriate authority, and
|
||||||
|
% (ii) execute:
|
||||||
|
%
|
||||||
|
% \setrubrictype{} to specify the custom rubric information.
|
||||||
|
%
|
||||||
|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||||
|
|
||||||
|
\setrubric{qu1_and_either_qu2_or_qu3}
|
||||||
|
|
||||||
|
\examtitlepage
|
||||||
|
|
||||||
|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||||
|
%
|
||||||
|
% Manual override for total page number computation.
|
||||||
|
%
|
||||||
|
% As long as you run latex upon this document three times in a row,
|
||||||
|
% the right number of `total pages' should be computed and placed
|
||||||
|
% in the footer of all pages except the title page.
|
||||||
|
%
|
||||||
|
% But, if this fails, you can set that number yourself with the
|
||||||
|
% following command:
|
||||||
|
%
|
||||||
|
% \settotalpages{n} with n a natural number.
|
||||||
|
%
|
||||||
|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||||
|
|
||||||
|
|
||||||
|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||||
|
%
|
||||||
|
% Beginning of your exam text.
|
||||||
|
%
|
||||||
|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||||
|
|
||||||
|
\begin{enumerate}
|
||||||
|
|
||||||
|
\item \rubricqA
|
||||||
|
|
||||||
|
\newcommand{\Tree}{\texttt{Tree}}
|
||||||
|
\newcommand{\AllT}{\texttt{AllT}}
|
||||||
|
\newcommand{\AnyT}{\texttt{AnyT}}
|
||||||
|
\newcommand{\leaf}{\texttt{leaf}}
|
||||||
|
\newcommand{\branch}{\texttt{branch}}
|
||||||
|
\newcommand{\here}{\texttt{here}}
|
||||||
|
\renewcommand{\left}{\texttt{left}}
|
||||||
|
\renewcommand{\right}{\texttt{right}}
|
||||||
|
\newcommand{\ubar}{\texttt{\underline{~}}}
|
||||||
|
|
||||||
|
Consider a type of trees defined as follows.
|
||||||
|
\begin{gather*}
|
||||||
|
%
|
||||||
|
\inference[\leaf]
|
||||||
|
{A}
|
||||||
|
{Tree~A}
|
||||||
|
%
|
||||||
|
\quad
|
||||||
|
%
|
||||||
|
\inference[\ubar\branch\ubar]
|
||||||
|
{Tree~A \\
|
||||||
|
Tree~A}
|
||||||
|
{Tree~A}
|
||||||
|
%
|
||||||
|
\end{gather*}
|
||||||
|
|
||||||
|
Given a predicate $P$ over $A$, we define predicates $\AllT$ and
|
||||||
|
$\AnyT$ which hold when $P$ holds for \emph{every} leaf in the tree
|
||||||
|
and when $P$ holds for \emph{some} leaf in the tree, respectively.
|
||||||
|
\begin{gather*}
|
||||||
|
%
|
||||||
|
\inference[\leaf]
|
||||||
|
{P~x}
|
||||||
|
{\AllT~P~(\leaf~x)}
|
||||||
|
%
|
||||||
|
\quad
|
||||||
|
%
|
||||||
|
\inference[\ubar\branch\ubar]
|
||||||
|
{\AllT~P~xt \\
|
||||||
|
\AllT~P~yt}
|
||||||
|
{\AllT~P~(xt~\branch~yt)}
|
||||||
|
%
|
||||||
|
\\~\\
|
||||||
|
%
|
||||||
|
\inference[\leaf]
|
||||||
|
{P~x}
|
||||||
|
{\AnyT~P~(\leaf~x)}
|
||||||
|
%
|
||||||
|
\quad
|
||||||
|
%
|
||||||
|
\inference[\left]
|
||||||
|
{\AnyT~P~xt}
|
||||||
|
{\AnyT~P~(xt~\branch~yt)}
|
||||||
|
%
|
||||||
|
\quad
|
||||||
|
%
|
||||||
|
\inference[\right]
|
||||||
|
{\AnyT~P~yt}
|
||||||
|
{\AnyT~P~(xt~\branch~yt)}
|
||||||
|
%
|
||||||
|
\end{gather*}
|
||||||
|
|
||||||
|
\begin{itemize}
|
||||||
|
|
||||||
|
\item[(a)] Formalise the definitions above.
|
||||||
|
|
||||||
|
\marks{12}
|
||||||
|
|
||||||
|
\item[(b)] Prove $\AllT~({\neg\ubar}~\circ~P)~xt$
|
||||||
|
implies $\neg~(\AnyT~P~xt)$, for all trees $xt$.
|
||||||
|
|
||||||
|
\marks{13}
|
||||||
|
|
||||||
|
\end{itemize}
|
||||||
|
|
||||||
|
\newpage
|
||||||
|
|
||||||
|
\item \rubricqB
|
||||||
|
|
||||||
|
\newcommand{\COMP}{\texttt{Comp}}
|
||||||
|
\newcommand{\OK}{\texttt{ok}}
|
||||||
|
\newcommand{\ERROR}{\texttt{error}}
|
||||||
|
\newcommand{\LETC}{\texttt{letc}}
|
||||||
|
\newcommand{\IN}{\texttt{in}}
|
||||||
|
|
||||||
|
\newcommand{\Comp}[1]{\COMP~#1}
|
||||||
|
\newcommand{\error}[1]{\ERROR~#1}
|
||||||
|
\newcommand{\ok}[1]{\OK~#1}
|
||||||
|
\newcommand{\letc}[3]{\LETC~#1\leftarrow#2~\IN~#3}
|
||||||
|
|
||||||
|
\newcommand{\comma}{\,,\,}
|
||||||
|
\newcommand{\V}{\texttt{V}}
|
||||||
|
\newcommand{\dash}{\texttt{-}}
|
||||||
|
\newcommand{\Value}{\texttt{Value}}
|
||||||
|
\newcommand{\becomes}{\longrightarrow}
|
||||||
|
\newcommand{\subst}[3]{#1~\texttt{[}~#2~\texttt{:=}~#3~\texttt{]}}
|
||||||
|
|
||||||
|
You will be provided with a definition of intrinsically-typed lambda
|
||||||
|
calculus in Agda. Consider constructs satisfying the following rules,
|
||||||
|
written in extrinsically-typed style.
|
||||||
|
|
||||||
|
A computation of type $\Comp{A}$ returns either an error with a
|
||||||
|
message $msg$ which is a string, or an ok value of a term $M$ of type $A$.
|
||||||
|
Consider constructs satisfying the following rules:
|
||||||
|
|
||||||
|
Typing:
|
||||||
|
\begin{gather*}
|
||||||
|
\inference[$\ERROR$]
|
||||||
|
{}
|
||||||
|
{\Gamma \vdash \error{msg} \typecolon \Comp{A}}
|
||||||
|
\qquad
|
||||||
|
\inference[$\OK$]
|
||||||
|
{\Gamma \vdash M \typecolon A}
|
||||||
|
{\Gamma \vdash \ok{M} \typecolon \Comp{A}}
|
||||||
|
\\~\\
|
||||||
|
\inference[$\LETC$]
|
||||||
|
{\Gamma \vdash M \typecolon \Comp{A} \\
|
||||||
|
\Gamma \comma x \typecolon A \vdash N \typecolon \Comp{B}}
|
||||||
|
{\Gamma \vdash \letc{x}{M}{N} \typecolon \Comp{B}}
|
||||||
|
\end{gather*}
|
||||||
|
|
||||||
|
Values:
|
||||||
|
\begin{gather*}
|
||||||
|
\inference[\V\dash\ERROR]
|
||||||
|
{}
|
||||||
|
{\Value~(\error{msg})}
|
||||||
|
\qquad
|
||||||
|
\inference[\V\dash\OK]
|
||||||
|
{\Value~V}
|
||||||
|
{\Value~(\ok{V})}
|
||||||
|
\end{gather*}
|
||||||
|
|
||||||
|
Reduction:
|
||||||
|
\begin{gather*}
|
||||||
|
\inference[$\xi\dash\OK$]
|
||||||
|
{M \becomes M'}
|
||||||
|
{\ok{M} \becomes \ok{M'}}
|
||||||
|
\qquad
|
||||||
|
\inference[$\xi\dash\LETC$]
|
||||||
|
{M \becomes M'}
|
||||||
|
{\letc{x}{M}{N} \becomes \letc{x}{M'}{N}}
|
||||||
|
\\~\\
|
||||||
|
\inference[$\beta\dash\ERROR$]
|
||||||
|
{}
|
||||||
|
{\letc{x}{(\error{msg})}{t} \becomes \error{msg}}
|
||||||
|
\\~\\
|
||||||
|
\inference[$\beta\dash\OK$]
|
||||||
|
{\Value{V}}
|
||||||
|
{\letc{x}{(\ok{V})}{N} \becomes \subst{N}{x}{V}}
|
||||||
|
\end{gather*}
|
||||||
|
|
||||||
|
\begin{enumerate}
|
||||||
|
\item[(a)] Extend the given definition to formalise the evaluation
|
||||||
|
and typing rules, including any other required definitions.
|
||||||
|
\marks{12}
|
||||||
|
|
||||||
|
\item[(b)] Prove progress. You will be provided with a proof of progress for
|
||||||
|
the simply-typed lambda calculus that you may extend.
|
||||||
|
\marks{13}
|
||||||
|
\end{enumerate}
|
||||||
|
|
||||||
|
Please delimit any code you add as follows.
|
||||||
|
\begin{verbatim}
|
||||||
|
-- begin
|
||||||
|
-- end
|
||||||
|
\end{verbatim}
|
||||||
|
|
||||||
|
\newpage
|
||||||
|
|
||||||
|
\item \rubricqC
|
||||||
|
|
||||||
|
\newcommand{\TT}{\texttt{tt}}
|
||||||
|
\newcommand{\CASETOP}{{\texttt{case}\top}}
|
||||||
|
\newcommand{\casetop}[2]{\CASETOP~#1~{\texttt{[tt}\!\Rightarrow}~#2~\texttt{]}}
|
||||||
|
\newcommand{\up}{\uparrow}
|
||||||
|
\newcommand{\dn}{\downarrow}
|
||||||
|
|
||||||
|
You will be provided with a definition of inference for extrinsically-typed lambda
|
||||||
|
calculus in Agda. Consider constructs satisfying the following rules,
|
||||||
|
written in extrinsically-typed style that support bidirectional inference.
|
||||||
|
|
||||||
|
Typing:
|
||||||
|
\begin{gather*}
|
||||||
|
\inference[$\TT$]
|
||||||
|
{}
|
||||||
|
{\Gamma \vdash \TT \dn \top}
|
||||||
|
\\~\\
|
||||||
|
\inference[$\CASETOP$]
|
||||||
|
{\Gamma \vdash L \up \top \\
|
||||||
|
\Gamma \vdash M \dn A}
|
||||||
|
{\Gamma \vdash \casetop{L}{M} \dn A}
|
||||||
|
\end{gather*}
|
||||||
|
|
||||||
|
\begin{enumerate}
|
||||||
|
\item[(a)] Extend the given definition to formalise the typing rules,
|
||||||
|
and update the definition of equality on types.
|
||||||
|
\marks{10}
|
||||||
|
|
||||||
|
\item[(b)] Extend the code to support type inference for the new features.
|
||||||
|
\marks{15}
|
||||||
|
\end{enumerate}
|
||||||
|
|
||||||
|
Please delimit any code you add as follows.
|
||||||
|
\begin{verbatim}
|
||||||
|
-- begin
|
||||||
|
-- end
|
||||||
|
\end{verbatim}
|
||||||
|
|
||||||
|
\end{enumerate}
|
||||||
|
|
||||||
|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||||
|
%
|
||||||
|
% End of your exam text.
|
||||||
|
%
|
||||||
|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||||
|
|
||||||
|
\end{document}
|
||||||
|
|
||||||
164
tspl/Assignments.lagda
Normal file
164
tspl/Assignments.lagda
Normal file
|
|
@ -0,0 +1,164 @@
|
||||||
|
---
|
||||||
|
title : "Assignments: Summary of all assignments"
|
||||||
|
layout : page
|
||||||
|
permalink : /Assignments/
|
||||||
|
---
|
||||||
|
|
||||||
|
## 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][Assignment1] Due 4pm Thursday 4 October (Week 3)
|
||||||
|
|
||||||
|
+ Naturals
|
||||||
|
- `seven`
|
||||||
|
- `+-example`
|
||||||
|
- `*-example`
|
||||||
|
- `_^_` (recommended)
|
||||||
|
- `∸-examples` (recommended)
|
||||||
|
- `Bin` (stretch)
|
||||||
|
|
||||||
|
+ Induction
|
||||||
|
- `operators`
|
||||||
|
- `finite-+-assoc` (stretch)
|
||||||
|
- `+-swap` (recommended)
|
||||||
|
- `*-distribʳ-+` (recommended)
|
||||||
|
- `*-assoc` (recommended)
|
||||||
|
- `*-comm`
|
||||||
|
- `0∸n≡n`
|
||||||
|
- `∸-+-assoc`
|
||||||
|
- `Bin-laws` (stretch)
|
||||||
|
|
||||||
|
+ Relations
|
||||||
|
- `orderings`
|
||||||
|
- `≤-antisym-cases`
|
||||||
|
- `*-mono-≤` (stretch)
|
||||||
|
- `<-trans` (recommended)
|
||||||
|
- `trichotomy`
|
||||||
|
- `+-mono-<`
|
||||||
|
- `≤-iff-<` (recommended)
|
||||||
|
- `<-trans-revisited`
|
||||||
|
- `o+o≡e` (recommended)
|
||||||
|
- `Bin-predicates` (stretch)
|
||||||
|
|
||||||
|
* [Assignment 2][Assignment2]. Due 4pm Thursday 18 October (Week 5)
|
||||||
|
|
||||||
|
+ Equality
|
||||||
|
- `≤-reasoning` (stretch)
|
||||||
|
|
||||||
|
+ Isomorphism
|
||||||
|
- `≃-implies-≲`
|
||||||
|
- `_⇔_` (recommended)
|
||||||
|
- `Bin-embedding` (stretch)
|
||||||
|
|
||||||
|
+ Connectives
|
||||||
|
- `⇔≃×` (recommended)
|
||||||
|
- `⊎-comm` (recommended)
|
||||||
|
- `⊎-assoc`
|
||||||
|
- `⊥-identityˡ` (recommended)
|
||||||
|
- `⊥-identityʳ`
|
||||||
|
- `⊎-weak-×` (recommended)
|
||||||
|
- `⊎×-implies-×⊎`
|
||||||
|
|
||||||
|
+ Negation
|
||||||
|
- `<-irreflexive` (recommended)
|
||||||
|
- `trichotomy`
|
||||||
|
- `⊎-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`
|
||||||
|
- `product` (recommended)
|
||||||
|
- `fold-++` (recommended)
|
||||||
|
- `map-is-foldr`
|
||||||
|
- `fold-Tree`
|
||||||
|
- `map-is-fold-Tree`
|
||||||
|
- `sum-downFrom` (stretch)
|
||||||
|
- `foldl`
|
||||||
|
- `foldr-monoid-foldl`
|
||||||
|
- `Any-++-⇔` (recommended)
|
||||||
|
- `All-++-≃` (stretch)
|
||||||
|
- `¬Any≃All¬` (stretch)
|
||||||
|
- `any?` (stretch)
|
||||||
|
- `filter?` (stretch)
|
||||||
|
|
||||||
|
+ Lambda
|
||||||
|
- `mul` (recommended)
|
||||||
|
- `primed` (stretch)
|
||||||
|
- `_[_:=_]′` (stretch)
|
||||||
|
- `—↠≃—↠′`
|
||||||
|
- `plus-example`
|
||||||
|
- `mul-type` (recommended)
|
||||||
|
|
||||||
|
+ Properties
|
||||||
|
- `Progress-≃`
|
||||||
|
- `progress′`
|
||||||
|
- `value?` (recommended)
|
||||||
|
- `subst′` (stretch)
|
||||||
|
- `mul-example` (recommended)
|
||||||
|
- `progress-preservation`
|
||||||
|
- `subject-expansion`
|
||||||
|
- `stuck`
|
||||||
|
- `unstuck` (recommended)
|
||||||
|
|
||||||
|
* Assignment 4. Due 4pm Thursday 15 November (Week 9)
|
||||||
|
|
||||||
|
|
||||||
|
+ DeBruijn
|
||||||
|
- `mul` (recommended)
|
||||||
|
- `V¬—→`
|
||||||
|
- `mul-example` (recommended)
|
||||||
|
|
||||||
|
+ 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)
|
||||||
680
tspl/Exam.lagda
Normal file
680
tspl/Exam.lagda
Normal file
|
|
@ -0,0 +1,680 @@
|
||||||
|
---
|
||||||
|
title : "Exam: TSPL Mock Exam file"
|
||||||
|
layout : page
|
||||||
|
permalink : /Exam/
|
||||||
|
---
|
||||||
|
|
||||||
|
|
||||||
|
\begin{code}
|
||||||
|
module Exam where
|
||||||
|
\end{code}
|
||||||
|
|
||||||
|
**IMPORTANT** For ease of marking, when modifying the given code please write
|
||||||
|
|
||||||
|
-- begin
|
||||||
|
-- end
|
||||||
|
|
||||||
|
before and after code you add, to indicate your changes.
|
||||||
|
|
||||||
|
## Imports
|
||||||
|
|
||||||
|
\begin{code}
|
||||||
|
import Relation.Binary.PropositionalEquality as Eq
|
||||||
|
open Eq using (_≡_; refl; sym; trans; cong; _≢_)
|
||||||
|
open import Data.Empty using (⊥; ⊥-elim)
|
||||||
|
open import Data.Nat using (ℕ; zero; suc)
|
||||||
|
open import Data.List using (List; []; _∷_; _++_)
|
||||||
|
open import Data.Product using (∃; ∃-syntax) renaming (_,_ to ⟨_,_⟩)
|
||||||
|
open import Data.String using (String)
|
||||||
|
open import Data.String.Unsafe using (_≟_)
|
||||||
|
open import Relation.Nullary using (¬_; Dec; yes; no)
|
||||||
|
open import Relation.Binary using (Decidable)
|
||||||
|
\end{code}
|
||||||
|
|
||||||
|
## Problem 1
|
||||||
|
|
||||||
|
\begin{code}
|
||||||
|
module Problem1 where
|
||||||
|
|
||||||
|
open import Function using (_∘_)
|
||||||
|
\end{code}
|
||||||
|
|
||||||
|
Remember to indent all code by two spaces.
|
||||||
|
|
||||||
|
### (a)
|
||||||
|
|
||||||
|
### (b)
|
||||||
|
|
||||||
|
### (c)
|
||||||
|
|
||||||
|
|
||||||
|
## Problem 2
|
||||||
|
|
||||||
|
Remember to indent all code by two spaces.
|
||||||
|
|
||||||
|
\begin{code}
|
||||||
|
module Problem2 where
|
||||||
|
\end{code}
|
||||||
|
|
||||||
|
### Infix declarations
|
||||||
|
|
||||||
|
\begin{code}
|
||||||
|
infix 4 _⊢_
|
||||||
|
infix 4 _∋_
|
||||||
|
infixl 5 _,_
|
||||||
|
|
||||||
|
infixr 7 _⇒_
|
||||||
|
|
||||||
|
infix 5 ƛ_
|
||||||
|
infix 5 μ_
|
||||||
|
infixl 7 _·_
|
||||||
|
infix 8 `suc_
|
||||||
|
infix 9 `_
|
||||||
|
infix 9 S_
|
||||||
|
infix 9 #_
|
||||||
|
\end{code}
|
||||||
|
|
||||||
|
### Types and contexts
|
||||||
|
|
||||||
|
\begin{code}
|
||||||
|
data Type : Set where
|
||||||
|
_⇒_ : Type → Type → Type
|
||||||
|
`ℕ : Type
|
||||||
|
|
||||||
|
data Context : Set where
|
||||||
|
∅ : Context
|
||||||
|
_,_ : Context → Type → Context
|
||||||
|
\end{code}
|
||||||
|
|
||||||
|
### Variables and the lookup judgment
|
||||||
|
|
||||||
|
\begin{code}
|
||||||
|
data _∋_ : Context → Type → Set where
|
||||||
|
|
||||||
|
Z : ∀ {Γ A}
|
||||||
|
----------
|
||||||
|
→ Γ , A ∋ A
|
||||||
|
|
||||||
|
S_ : ∀ {Γ A B}
|
||||||
|
→ Γ ∋ A
|
||||||
|
---------
|
||||||
|
→ Γ , B ∋ A
|
||||||
|
\end{code}
|
||||||
|
|
||||||
|
### Terms and the typing judgment
|
||||||
|
|
||||||
|
\begin{code}
|
||||||
|
data _⊢_ : Context → Type → Set where
|
||||||
|
|
||||||
|
`_ : ∀ {Γ} {A}
|
||||||
|
→ Γ ∋ A
|
||||||
|
------
|
||||||
|
→ Γ ⊢ A
|
||||||
|
|
||||||
|
ƛ_ : ∀ {Γ} {A B}
|
||||||
|
→ Γ , A ⊢ B
|
||||||
|
----------
|
||||||
|
→ Γ ⊢ A ⇒ B
|
||||||
|
|
||||||
|
_·_ : ∀ {Γ} {A B}
|
||||||
|
→ Γ ⊢ A ⇒ B
|
||||||
|
→ Γ ⊢ A
|
||||||
|
----------
|
||||||
|
→ Γ ⊢ B
|
||||||
|
|
||||||
|
`zero : ∀ {Γ}
|
||||||
|
----------
|
||||||
|
→ Γ ⊢ `ℕ
|
||||||
|
|
||||||
|
`suc_ : ∀ {Γ}
|
||||||
|
→ Γ ⊢ `ℕ
|
||||||
|
-------
|
||||||
|
→ Γ ⊢ `ℕ
|
||||||
|
|
||||||
|
case : ∀ {Γ A}
|
||||||
|
→ Γ ⊢ `ℕ
|
||||||
|
→ Γ ⊢ A
|
||||||
|
→ Γ , `ℕ ⊢ A
|
||||||
|
-----------
|
||||||
|
→ Γ ⊢ A
|
||||||
|
|
||||||
|
μ_ : ∀ {Γ A}
|
||||||
|
→ Γ , A ⊢ A
|
||||||
|
----------
|
||||||
|
→ Γ ⊢ A
|
||||||
|
\end{code}
|
||||||
|
|
||||||
|
### Abbreviating de Bruijn indices
|
||||||
|
|
||||||
|
\begin{code}
|
||||||
|
lookup : Context → ℕ → Type
|
||||||
|
lookup (Γ , A) zero = A
|
||||||
|
lookup (Γ , _) (suc n) = lookup Γ n
|
||||||
|
lookup ∅ _ = ⊥-elim impossible
|
||||||
|
where postulate impossible : ⊥
|
||||||
|
|
||||||
|
count : ∀ {Γ} → (n : ℕ) → Γ ∋ lookup Γ n
|
||||||
|
count {Γ , _} zero = Z
|
||||||
|
count {Γ , _} (suc n) = S (count n)
|
||||||
|
count {∅} _ = ⊥-elim impossible
|
||||||
|
where postulate impossible : ⊥
|
||||||
|
|
||||||
|
#_ : ∀ {Γ} → (n : ℕ) → Γ ⊢ lookup Γ n
|
||||||
|
# n = ` count n
|
||||||
|
\end{code}
|
||||||
|
|
||||||
|
### Renaming
|
||||||
|
|
||||||
|
\begin{code}
|
||||||
|
ext : ∀ {Γ Δ} → (∀ {A} → Γ ∋ A → Δ ∋ A)
|
||||||
|
-----------------------------------
|
||||||
|
→ (∀ {A B} → Γ , B ∋ A → Δ , B ∋ A)
|
||||||
|
ext ρ Z = Z
|
||||||
|
ext ρ (S x) = S (ρ x)
|
||||||
|
|
||||||
|
rename : ∀ {Γ Δ}
|
||||||
|
→ (∀ {A} → Γ ∋ A → Δ ∋ A)
|
||||||
|
------------------------
|
||||||
|
→ (∀ {A} → Γ ⊢ A → Δ ⊢ A)
|
||||||
|
rename ρ (` x) = ` (ρ x)
|
||||||
|
rename ρ (ƛ N) = ƛ (rename (ext ρ) N)
|
||||||
|
rename ρ (L · M) = (rename ρ L) · (rename ρ M)
|
||||||
|
rename ρ (`zero) = `zero
|
||||||
|
rename ρ (`suc M) = `suc (rename ρ M)
|
||||||
|
rename ρ (case L M N) = case (rename ρ L) (rename ρ M) (rename (ext ρ) N)
|
||||||
|
rename ρ (μ N) = μ (rename (ext ρ) N)
|
||||||
|
\end{code}
|
||||||
|
|
||||||
|
### Simultaneous Substitution
|
||||||
|
|
||||||
|
\begin{code}
|
||||||
|
exts : ∀ {Γ Δ} → (∀ {A} → Γ ∋ A → Δ ⊢ A)
|
||||||
|
----------------------------------
|
||||||
|
→ (∀ {A B} → Γ , B ∋ A → Δ , B ⊢ A)
|
||||||
|
exts σ Z = ` Z
|
||||||
|
exts σ (S x) = rename S_ (σ x)
|
||||||
|
|
||||||
|
subst : ∀ {Γ Δ}
|
||||||
|
→ (∀ {A} → Γ ∋ A → Δ ⊢ A)
|
||||||
|
------------------------
|
||||||
|
→ (∀ {A} → Γ ⊢ A → Δ ⊢ A)
|
||||||
|
subst σ (` k) = σ k
|
||||||
|
subst σ (ƛ N) = ƛ (subst (exts σ) N)
|
||||||
|
subst σ (L · M) = (subst σ L) · (subst σ M)
|
||||||
|
subst σ (`zero) = `zero
|
||||||
|
subst σ (`suc M) = `suc (subst σ M)
|
||||||
|
subst σ (case L M N) = case (subst σ L) (subst σ M) (subst (exts σ) N)
|
||||||
|
subst σ (μ N) = μ (subst (exts σ) N)
|
||||||
|
\end{code}
|
||||||
|
|
||||||
|
### Single substitution
|
||||||
|
|
||||||
|
\begin{code}
|
||||||
|
_[_] : ∀ {Γ A B}
|
||||||
|
→ Γ , B ⊢ A
|
||||||
|
→ Γ ⊢ B
|
||||||
|
---------
|
||||||
|
→ Γ ⊢ A
|
||||||
|
_[_] {Γ} {A} {B} N M = subst {Γ , B} {Γ} σ {A} N
|
||||||
|
where
|
||||||
|
σ : ∀ {A} → Γ , B ∋ A → Γ ⊢ A
|
||||||
|
σ Z = M
|
||||||
|
σ (S x) = ` x
|
||||||
|
\end{code}
|
||||||
|
|
||||||
|
### Values
|
||||||
|
|
||||||
|
\begin{code}
|
||||||
|
data Value : ∀ {Γ A} → Γ ⊢ A → Set where
|
||||||
|
|
||||||
|
V-ƛ : ∀ {Γ A B} {N : Γ , A ⊢ B}
|
||||||
|
---------------------------
|
||||||
|
→ Value (ƛ N)
|
||||||
|
|
||||||
|
V-zero : ∀ {Γ}
|
||||||
|
-----------------
|
||||||
|
→ Value (`zero {Γ})
|
||||||
|
|
||||||
|
V-suc : ∀ {Γ} {V : Γ ⊢ `ℕ}
|
||||||
|
→ Value V
|
||||||
|
--------------
|
||||||
|
→ Value (`suc V)
|
||||||
|
\end{code}
|
||||||
|
|
||||||
|
### Reduction
|
||||||
|
|
||||||
|
\begin{code}
|
||||||
|
infix 2 _—→_
|
||||||
|
|
||||||
|
data _—→_ : ∀ {Γ A} → (Γ ⊢ A) → (Γ ⊢ A) → Set where
|
||||||
|
|
||||||
|
ξ-·₁ : ∀ {Γ A B} {L L′ : Γ ⊢ A ⇒ B} {M : Γ ⊢ A}
|
||||||
|
→ L —→ L′
|
||||||
|
-----------------
|
||||||
|
→ L · M —→ L′ · M
|
||||||
|
|
||||||
|
ξ-·₂ : ∀ {Γ A B} {V : Γ ⊢ A ⇒ B} {M M′ : Γ ⊢ A}
|
||||||
|
→ Value V
|
||||||
|
→ M —→ M′
|
||||||
|
--------------
|
||||||
|
→ V · M —→ V · M′
|
||||||
|
|
||||||
|
β-ƛ : ∀ {Γ A B} {N : Γ , A ⊢ B} {W : Γ ⊢ A}
|
||||||
|
→ Value W
|
||||||
|
-------------------
|
||||||
|
→ (ƛ N) · W —→ N [ W ]
|
||||||
|
|
||||||
|
ξ-suc : ∀ {Γ} {M M′ : Γ ⊢ `ℕ}
|
||||||
|
→ M —→ M′
|
||||||
|
----------------
|
||||||
|
→ `suc M —→ `suc M′
|
||||||
|
|
||||||
|
ξ-case : ∀ {Γ A} {L L′ : Γ ⊢ `ℕ} {M : Γ ⊢ A} {N : Γ , `ℕ ⊢ A}
|
||||||
|
→ L —→ L′
|
||||||
|
--------------------------
|
||||||
|
→ case L M N —→ case L′ M N
|
||||||
|
|
||||||
|
β-zero : ∀ {Γ A} {M : Γ ⊢ A} {N : Γ , `ℕ ⊢ A}
|
||||||
|
-------------------
|
||||||
|
→ case `zero M N —→ M
|
||||||
|
|
||||||
|
β-suc : ∀ {Γ A} {V : Γ ⊢ `ℕ} {M : Γ ⊢ A} {N : Γ , `ℕ ⊢ A}
|
||||||
|
→ Value V
|
||||||
|
-----------------------------
|
||||||
|
→ case (`suc V) M N —→ N [ V ]
|
||||||
|
|
||||||
|
β-μ : ∀ {Γ A} {N : Γ , A ⊢ A}
|
||||||
|
---------------
|
||||||
|
→ μ N —→ N [ μ N ]
|
||||||
|
\end{code}
|
||||||
|
|
||||||
|
|
||||||
|
### Reflexive and transitive closure
|
||||||
|
|
||||||
|
\begin{code}
|
||||||
|
infix 2 _—↠_
|
||||||
|
infix 1 begin_
|
||||||
|
infixr 2 _—→⟨_⟩_
|
||||||
|
infix 3 _∎
|
||||||
|
|
||||||
|
data _—↠_ : ∀ {Γ A} → (Γ ⊢ A) → (Γ ⊢ A) → Set where
|
||||||
|
|
||||||
|
_∎ : ∀ {Γ A} (M : Γ ⊢ A)
|
||||||
|
--------
|
||||||
|
→ M —↠ M
|
||||||
|
|
||||||
|
_—→⟨_⟩_ : ∀ {Γ A} (L : Γ ⊢ A) {M N : Γ ⊢ A}
|
||||||
|
→ L —→ M
|
||||||
|
→ M —↠ N
|
||||||
|
---------
|
||||||
|
→ L —↠ N
|
||||||
|
|
||||||
|
begin_ : ∀ {Γ} {A} {M N : Γ ⊢ A}
|
||||||
|
→ M —↠ N
|
||||||
|
------
|
||||||
|
→ M —↠ N
|
||||||
|
begin M—↠N = M—↠N
|
||||||
|
\end{code}
|
||||||
|
|
||||||
|
|
||||||
|
### Progress
|
||||||
|
|
||||||
|
\begin{code}
|
||||||
|
data Progress {A} (M : ∅ ⊢ A) : Set where
|
||||||
|
|
||||||
|
step : ∀ {N : ∅ ⊢ A}
|
||||||
|
→ M —→ N
|
||||||
|
-------------
|
||||||
|
→ Progress M
|
||||||
|
|
||||||
|
done :
|
||||||
|
Value M
|
||||||
|
----------
|
||||||
|
→ Progress M
|
||||||
|
|
||||||
|
progress : ∀ {A} → (M : ∅ ⊢ A) → Progress M
|
||||||
|
progress (` ())
|
||||||
|
progress (ƛ N) = done V-ƛ
|
||||||
|
progress (L · M) with progress L
|
||||||
|
... | step L—→L′ = step (ξ-·₁ L—→L′)
|
||||||
|
... | done V-ƛ with progress M
|
||||||
|
... | step M—→M′ = step (ξ-·₂ V-ƛ M—→M′)
|
||||||
|
... | done VM = step (β-ƛ VM)
|
||||||
|
progress (`zero) = done V-zero
|
||||||
|
progress (`suc M) with progress M
|
||||||
|
... | step M—→M′ = step (ξ-suc M—→M′)
|
||||||
|
... | done VM = done (V-suc VM)
|
||||||
|
progress (case L M N) with progress L
|
||||||
|
... | step L—→L′ = step (ξ-case L—→L′)
|
||||||
|
... | done V-zero = step (β-zero)
|
||||||
|
... | done (V-suc VL) = step (β-suc VL)
|
||||||
|
progress (μ N) = step (β-μ)
|
||||||
|
\end{code}
|
||||||
|
|
||||||
|
### Evaluation
|
||||||
|
|
||||||
|
\begin{code}
|
||||||
|
data Gas : Set where
|
||||||
|
gas : ℕ → Gas
|
||||||
|
|
||||||
|
data Finished {Γ A} (N : Γ ⊢ A) : Set where
|
||||||
|
|
||||||
|
done :
|
||||||
|
Value N
|
||||||
|
----------
|
||||||
|
→ Finished N
|
||||||
|
|
||||||
|
out-of-gas :
|
||||||
|
----------
|
||||||
|
Finished N
|
||||||
|
|
||||||
|
data Steps : ∀ {A} → ∅ ⊢ A → Set where
|
||||||
|
|
||||||
|
steps : ∀ {A} {L N : ∅ ⊢ A}
|
||||||
|
→ L —↠ N
|
||||||
|
→ Finished N
|
||||||
|
----------
|
||||||
|
→ Steps L
|
||||||
|
|
||||||
|
eval : ∀ {A}
|
||||||
|
→ Gas
|
||||||
|
→ (L : ∅ ⊢ A)
|
||||||
|
-----------
|
||||||
|
→ Steps L
|
||||||
|
eval (gas zero) L = steps (L ∎) out-of-gas
|
||||||
|
eval (gas (suc m)) L with progress L
|
||||||
|
... | done VL = steps (L ∎) (done VL)
|
||||||
|
... | step {M} L—→M with eval (gas m) M
|
||||||
|
... | steps M—↠N fin = steps (L —→⟨ L—→M ⟩ M—↠N) fin
|
||||||
|
\end{code}
|
||||||
|
|
||||||
|
## Problem 3
|
||||||
|
|
||||||
|
Remember to indent all code by two spaces.
|
||||||
|
|
||||||
|
\begin{code}
|
||||||
|
module Problem3 where
|
||||||
|
\end{code}
|
||||||
|
|
||||||
|
### Imports
|
||||||
|
|
||||||
|
\begin{code}
|
||||||
|
import plfa.DeBruijn as DB
|
||||||
|
\end{code}
|
||||||
|
|
||||||
|
### Syntax
|
||||||
|
|
||||||
|
\begin{code}
|
||||||
|
infix 4 _∋_⦂_
|
||||||
|
infix 4 _⊢_↑_
|
||||||
|
infix 4 _⊢_↓_
|
||||||
|
infixl 5 _,_⦂_
|
||||||
|
|
||||||
|
infix 5 ƛ_⇒_
|
||||||
|
infix 5 μ_⇒_
|
||||||
|
infix 6 _↑
|
||||||
|
infix 6 _↓_
|
||||||
|
infixl 7 _·_
|
||||||
|
infix 8 `suc_
|
||||||
|
infix 9 `_
|
||||||
|
\end{code}
|
||||||
|
|
||||||
|
### Types
|
||||||
|
|
||||||
|
\begin{code}
|
||||||
|
data Type : Set where
|
||||||
|
_⇒_ : Type → Type → Type
|
||||||
|
`ℕ : Type
|
||||||
|
\end{code}
|
||||||
|
|
||||||
|
### Identifiers
|
||||||
|
|
||||||
|
\begin{code}
|
||||||
|
Id : Set
|
||||||
|
Id = String
|
||||||
|
\end{code}
|
||||||
|
|
||||||
|
### Contexts
|
||||||
|
|
||||||
|
\begin{code}
|
||||||
|
data Context : Set where
|
||||||
|
∅ : Context
|
||||||
|
_,_⦂_ : Context → Id → Type → Context
|
||||||
|
\end{code}
|
||||||
|
|
||||||
|
### Terms
|
||||||
|
|
||||||
|
\begin{code}
|
||||||
|
data Term⁺ : Set
|
||||||
|
data Term⁻ : Set
|
||||||
|
|
||||||
|
data Term⁺ where
|
||||||
|
`_ : Id → Term⁺
|
||||||
|
_·_ : Term⁺ → Term⁻ → Term⁺
|
||||||
|
_↓_ : Term⁻ → Type → Term⁺
|
||||||
|
|
||||||
|
data Term⁻ where
|
||||||
|
ƛ_⇒_ : Id → Term⁻ → Term⁻
|
||||||
|
`zero : Term⁻
|
||||||
|
`suc_ : Term⁻ → Term⁻
|
||||||
|
`case_[zero⇒_|suc_⇒_] : Term⁺ → Term⁻ → Id → Term⁻ → Term⁻
|
||||||
|
μ_⇒_ : Id → Term⁻ → Term⁻
|
||||||
|
_↑ : Term⁺ → Term⁻
|
||||||
|
\end{code}
|
||||||
|
|
||||||
|
### Lookup
|
||||||
|
|
||||||
|
\begin{code}
|
||||||
|
data _∋_⦂_ : Context → Id → Type → Set where
|
||||||
|
|
||||||
|
Z : ∀ {Γ x A}
|
||||||
|
--------------------
|
||||||
|
→ Γ , x ⦂ A ∋ x ⦂ A
|
||||||
|
|
||||||
|
S : ∀ {Γ x y A B}
|
||||||
|
→ x ≢ y
|
||||||
|
→ Γ ∋ x ⦂ A
|
||||||
|
-----------------
|
||||||
|
→ Γ , y ⦂ B ∋ x ⦂ A
|
||||||
|
\end{code}
|
||||||
|
|
||||||
|
### Bidirectional type checking
|
||||||
|
|
||||||
|
\begin{code}
|
||||||
|
data _⊢_↑_ : Context → Term⁺ → Type → Set
|
||||||
|
data _⊢_↓_ : Context → Term⁻ → Type → Set
|
||||||
|
|
||||||
|
data _⊢_↑_ where
|
||||||
|
|
||||||
|
⊢` : ∀ {Γ A x}
|
||||||
|
→ Γ ∋ x ⦂ A
|
||||||
|
-----------
|
||||||
|
→ Γ ⊢ ` x ↑ A
|
||||||
|
|
||||||
|
_·_ : ∀ {Γ L M A B}
|
||||||
|
→ Γ ⊢ L ↑ A ⇒ B
|
||||||
|
→ Γ ⊢ M ↓ A
|
||||||
|
-------------
|
||||||
|
→ Γ ⊢ L · M ↑ B
|
||||||
|
|
||||||
|
⊢↓ : ∀ {Γ M A}
|
||||||
|
→ Γ ⊢ M ↓ A
|
||||||
|
---------------
|
||||||
|
→ Γ ⊢ (M ↓ A) ↑ A
|
||||||
|
|
||||||
|
data _⊢_↓_ where
|
||||||
|
|
||||||
|
⊢ƛ : ∀ {Γ x N A B}
|
||||||
|
→ Γ , x ⦂ A ⊢ N ↓ B
|
||||||
|
-------------------
|
||||||
|
→ Γ ⊢ ƛ x ⇒ N ↓ A ⇒ B
|
||||||
|
|
||||||
|
⊢zero : ∀ {Γ}
|
||||||
|
--------------
|
||||||
|
→ Γ ⊢ `zero ↓ `ℕ
|
||||||
|
|
||||||
|
⊢suc : ∀ {Γ M}
|
||||||
|
→ Γ ⊢ M ↓ `ℕ
|
||||||
|
---------------
|
||||||
|
→ Γ ⊢ `suc M ↓ `ℕ
|
||||||
|
|
||||||
|
⊢case : ∀ {Γ L M x N A}
|
||||||
|
→ Γ ⊢ L ↑ `ℕ
|
||||||
|
→ Γ ⊢ M ↓ A
|
||||||
|
→ Γ , x ⦂ `ℕ ⊢ N ↓ A
|
||||||
|
-------------------------------------
|
||||||
|
→ Γ ⊢ `case L [zero⇒ M |suc x ⇒ N ] ↓ A
|
||||||
|
|
||||||
|
⊢μ : ∀ {Γ x N A}
|
||||||
|
→ Γ , x ⦂ A ⊢ N ↓ A
|
||||||
|
-----------------
|
||||||
|
→ Γ ⊢ μ x ⇒ N ↓ A
|
||||||
|
|
||||||
|
⊢↑ : ∀ {Γ M A B}
|
||||||
|
→ Γ ⊢ M ↑ A
|
||||||
|
→ A ≡ B
|
||||||
|
-------------
|
||||||
|
→ Γ ⊢ (M ↑) ↓ B
|
||||||
|
\end{code}
|
||||||
|
|
||||||
|
|
||||||
|
### Type equality
|
||||||
|
|
||||||
|
\begin{code}
|
||||||
|
_≟Tp_ : (A B : Type) → Dec (A ≡ B)
|
||||||
|
`ℕ ≟Tp `ℕ = yes refl
|
||||||
|
`ℕ ≟Tp (A ⇒ B) = no λ()
|
||||||
|
(A ⇒ B) ≟Tp `ℕ = no λ()
|
||||||
|
(A ⇒ B) ≟Tp (A′ ⇒ B′)
|
||||||
|
with A ≟Tp A′ | B ≟Tp B′
|
||||||
|
... | no A≢ | _ = no λ{refl → A≢ refl}
|
||||||
|
... | yes _ | no B≢ = no λ{refl → B≢ refl}
|
||||||
|
... | yes refl | yes refl = yes refl
|
||||||
|
\end{code}
|
||||||
|
|
||||||
|
### Prerequisites
|
||||||
|
|
||||||
|
\begin{code}
|
||||||
|
dom≡ : ∀ {A A′ B B′} → A ⇒ B ≡ A′ ⇒ B′ → A ≡ A′
|
||||||
|
dom≡ refl = refl
|
||||||
|
|
||||||
|
rng≡ : ∀ {A A′ B B′} → A ⇒ B ≡ A′ ⇒ B′ → B ≡ B′
|
||||||
|
rng≡ refl = refl
|
||||||
|
|
||||||
|
ℕ≢⇒ : ∀ {A B} → `ℕ ≢ A ⇒ B
|
||||||
|
ℕ≢⇒ ()
|
||||||
|
\end{code}
|
||||||
|
|
||||||
|
|
||||||
|
### Unique lookup
|
||||||
|
|
||||||
|
\begin{code}
|
||||||
|
uniq-∋ : ∀ {Γ x A B} → Γ ∋ x ⦂ A → Γ ∋ x ⦂ B → A ≡ B
|
||||||
|
uniq-∋ Z Z = refl
|
||||||
|
uniq-∋ Z (S x≢y _) = ⊥-elim (x≢y refl)
|
||||||
|
uniq-∋ (S x≢y _) Z = ⊥-elim (x≢y refl)
|
||||||
|
uniq-∋ (S _ ∋x) (S _ ∋x′) = uniq-∋ ∋x ∋x′
|
||||||
|
\end{code}
|
||||||
|
|
||||||
|
### Unique synthesis
|
||||||
|
|
||||||
|
\begin{code}
|
||||||
|
uniq-↑ : ∀ {Γ M A B} → Γ ⊢ M ↑ A → Γ ⊢ M ↑ B → A ≡ B
|
||||||
|
uniq-↑ (⊢` ∋x) (⊢` ∋x′) = uniq-∋ ∋x ∋x′
|
||||||
|
uniq-↑ (⊢L · ⊢M) (⊢L′ · ⊢M′) = rng≡ (uniq-↑ ⊢L ⊢L′)
|
||||||
|
uniq-↑ (⊢↓ ⊢M) (⊢↓ ⊢M′) = refl
|
||||||
|
\end{code}
|
||||||
|
|
||||||
|
## Lookup type of a variable in the context
|
||||||
|
|
||||||
|
\begin{code}
|
||||||
|
ext∋ : ∀ {Γ B x y}
|
||||||
|
→ x ≢ y
|
||||||
|
→ ¬ ∃[ A ]( Γ ∋ x ⦂ A )
|
||||||
|
-----------------------------
|
||||||
|
→ ¬ ∃[ A ]( Γ , y ⦂ B ∋ x ⦂ A )
|
||||||
|
ext∋ x≢y _ ⟨ A , Z ⟩ = x≢y refl
|
||||||
|
ext∋ _ ¬∃ ⟨ A , S _ ⊢x ⟩ = ¬∃ ⟨ A , ⊢x ⟩
|
||||||
|
|
||||||
|
lookup : ∀ (Γ : Context) (x : Id)
|
||||||
|
-----------------------
|
||||||
|
→ Dec (∃[ A ](Γ ∋ x ⦂ A))
|
||||||
|
lookup ∅ x = no (λ ())
|
||||||
|
lookup (Γ , y ⦂ B) x with x ≟ y
|
||||||
|
... | yes refl = yes ⟨ B , Z ⟩
|
||||||
|
... | no x≢y with lookup Γ x
|
||||||
|
... | no ¬∃ = no (ext∋ x≢y ¬∃)
|
||||||
|
... | yes ⟨ A , ⊢x ⟩ = yes ⟨ A , S x≢y ⊢x ⟩
|
||||||
|
\end{code}
|
||||||
|
|
||||||
|
### Promoting negations
|
||||||
|
|
||||||
|
\begin{code}
|
||||||
|
¬arg : ∀ {Γ A B L M}
|
||||||
|
→ Γ ⊢ L ↑ A ⇒ B
|
||||||
|
→ ¬ Γ ⊢ M ↓ A
|
||||||
|
-------------------------
|
||||||
|
→ ¬ ∃[ B′ ](Γ ⊢ L · M ↑ B′)
|
||||||
|
¬arg ⊢L ¬⊢M ⟨ B′ , ⊢L′ · ⊢M′ ⟩ rewrite dom≡ (uniq-↑ ⊢L ⊢L′) = ¬⊢M ⊢M′
|
||||||
|
|
||||||
|
¬switch : ∀ {Γ M A B}
|
||||||
|
→ Γ ⊢ M ↑ A
|
||||||
|
→ A ≢ B
|
||||||
|
---------------
|
||||||
|
→ ¬ Γ ⊢ (M ↑) ↓ B
|
||||||
|
¬switch ⊢M A≢B (⊢↑ ⊢M′ A′≡B) rewrite uniq-↑ ⊢M ⊢M′ = A≢B A′≡B
|
||||||
|
\end{code}
|
||||||
|
|
||||||
|
|
||||||
|
## Synthesize and inherit types
|
||||||
|
|
||||||
|
\begin{code}
|
||||||
|
synthesize : ∀ (Γ : Context) (M : Term⁺)
|
||||||
|
-----------------------
|
||||||
|
→ Dec (∃[ A ](Γ ⊢ M ↑ A))
|
||||||
|
|
||||||
|
inherit : ∀ (Γ : Context) (M : Term⁻) (A : Type)
|
||||||
|
---------------
|
||||||
|
→ Dec (Γ ⊢ M ↓ A)
|
||||||
|
|
||||||
|
synthesize Γ (` x) with lookup Γ x
|
||||||
|
... | no ¬∃ = no (λ{ ⟨ A , ⊢` ∋x ⟩ → ¬∃ ⟨ A , ∋x ⟩ })
|
||||||
|
... | yes ⟨ A , ∋x ⟩ = yes ⟨ A , ⊢` ∋x ⟩
|
||||||
|
synthesize Γ (L · M) with synthesize Γ L
|
||||||
|
... | no ¬∃ = no (λ{ ⟨ _ , ⊢L · _ ⟩ → ¬∃ ⟨ _ , ⊢L ⟩ })
|
||||||
|
... | yes ⟨ `ℕ , ⊢L ⟩ = no (λ{ ⟨ _ , ⊢L′ · _ ⟩ → ℕ≢⇒ (uniq-↑ ⊢L ⊢L′) })
|
||||||
|
... | yes ⟨ A ⇒ B , ⊢L ⟩ with inherit Γ M A
|
||||||
|
... | no ¬⊢M = no (¬arg ⊢L ¬⊢M)
|
||||||
|
... | yes ⊢M = yes ⟨ B , ⊢L · ⊢M ⟩
|
||||||
|
synthesize Γ (M ↓ A) with inherit Γ M A
|
||||||
|
... | no ¬⊢M = no (λ{ ⟨ _ , ⊢↓ ⊢M ⟩ → ¬⊢M ⊢M })
|
||||||
|
... | yes ⊢M = yes ⟨ A , ⊢↓ ⊢M ⟩
|
||||||
|
|
||||||
|
inherit Γ (ƛ x ⇒ N) `ℕ = no (λ())
|
||||||
|
inherit Γ (ƛ x ⇒ N) (A ⇒ B) with inherit (Γ , x ⦂ A) N B
|
||||||
|
... | no ¬⊢N = no (λ{ (⊢ƛ ⊢N) → ¬⊢N ⊢N })
|
||||||
|
... | yes ⊢N = yes (⊢ƛ ⊢N)
|
||||||
|
inherit Γ `zero `ℕ = yes ⊢zero
|
||||||
|
inherit Γ `zero (A ⇒ B) = no (λ())
|
||||||
|
inherit Γ (`suc M) `ℕ with inherit Γ M `ℕ
|
||||||
|
... | no ¬⊢M = no (λ{ (⊢suc ⊢M) → ¬⊢M ⊢M })
|
||||||
|
... | yes ⊢M = yes (⊢suc ⊢M)
|
||||||
|
inherit Γ (`suc M) (A ⇒ B) = no (λ())
|
||||||
|
inherit Γ (`case L [zero⇒ M |suc x ⇒ N ]) A with synthesize Γ L
|
||||||
|
... | no ¬∃ = no (λ{ (⊢case ⊢L _ _) → ¬∃ ⟨ `ℕ , ⊢L ⟩})
|
||||||
|
... | yes ⟨ _ ⇒ _ , ⊢L ⟩ = no (λ{ (⊢case ⊢L′ _ _) → ℕ≢⇒ (uniq-↑ ⊢L′ ⊢L) })
|
||||||
|
... | yes ⟨ `ℕ , ⊢L ⟩ with inherit Γ M A
|
||||||
|
... | no ¬⊢M = no (λ{ (⊢case _ ⊢M _) → ¬⊢M ⊢M })
|
||||||
|
... | yes ⊢M with inherit (Γ , x ⦂ `ℕ) N A
|
||||||
|
... | no ¬⊢N = no (λ{ (⊢case _ _ ⊢N) → ¬⊢N ⊢N })
|
||||||
|
... | yes ⊢N = yes (⊢case ⊢L ⊢M ⊢N)
|
||||||
|
inherit Γ (μ x ⇒ N) A with inherit (Γ , x ⦂ A) N A
|
||||||
|
... | no ¬⊢N = no (λ{ (⊢μ ⊢N) → ¬⊢N ⊢N })
|
||||||
|
... | yes ⊢N = yes (⊢μ ⊢N)
|
||||||
|
inherit Γ (M ↑) B with synthesize Γ M
|
||||||
|
... | no ¬∃ = no (λ{ (⊢↑ ⊢M _) → ¬∃ ⟨ _ , ⊢M ⟩ })
|
||||||
|
... | yes ⟨ A , ⊢M ⟩ with A ≟Tp B
|
||||||
|
... | no A≢B = no (¬switch ⊢M A≢B)
|
||||||
|
... | yes A≡B = yes (⊢↑ ⊢M A≡B)
|
||||||
|
\end{code}
|
||||||
|
|
||||||
118
tspl/TSPL.lagda
Normal file
118
tspl/TSPL.lagda
Normal file
|
|
@ -0,0 +1,118 @@
|
||||||
|
---
|
||||||
|
title : "TSPL: Course notes"
|
||||||
|
layout : page
|
||||||
|
permalink : /TSPL/
|
||||||
|
---
|
||||||
|
|
||||||
|
## Staff
|
||||||
|
|
||||||
|
* **Instructor**
|
||||||
|
[Philip Wadler](https://homepages.inf.ed.ac.uk/wadler)
|
||||||
|
* **Teaching assistants**
|
||||||
|
- [Wen Kokke](mailto:wen.kokke@ed.ac.uk)
|
||||||
|
- [Chad Nester](mailto:chad.nester@gmail.com)
|
||||||
|
|
||||||
|
## Lectures
|
||||||
|
|
||||||
|
Lectures take place Monday, Wednesday, and Friday in AT 7.02. (Moved from AT 5.07 and 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 class)</td>
|
||||||
|
</tr>
|
||||||
|
<tr>
|
||||||
|
<td>3</td>
|
||||||
|
<td><b>1 Oct</b> <a href="/Equality/">Equality</a> & <a href="/Isomorphism/">Isomorphism</a></td>
|
||||||
|
<td><b>3 Oct</b> <a href="/Connectives/">Connectives</a></td>
|
||||||
|
<td><b>5 Oct</b> <a href="/Negation/">Negation</a></td>
|
||||||
|
</tr>
|
||||||
|
<tr>
|
||||||
|
<td>4</td>
|
||||||
|
<td><b>8 Oct</b> <a href="/Quantifiers/">Quantifiers</a></td>
|
||||||
|
<td><b>10 Oct</b> <a href="/Decidable/">Decidable</a></td>
|
||||||
|
<td><b>12 Oct</b> (tutorial only)</td>
|
||||||
|
</tr>
|
||||||
|
<tr>
|
||||||
|
<td>5</td>
|
||||||
|
<td><b>15 Oct</b> <a href="/Lists/">Lists</a></td>
|
||||||
|
<td><b>17 Oct</b> (tutorial only)</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> (no class)</td>
|
||||||
|
<td><b>26 Oct</b> <a href="/Properties/">Properties</a></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> <a href="/Inference/">Inference</a></td>
|
||||||
|
</tr>
|
||||||
|
<tr>
|
||||||
|
<td>8</td>
|
||||||
|
<td><b>5 Nov</b> (no class)</td>
|
||||||
|
<td><b>7 Nov</b> (tutorial only)</td>
|
||||||
|
<td><b>9 Nov</b> <a href="/Untyped/">Untyped</a></td>
|
||||||
|
</tr>
|
||||||
|
<tr>
|
||||||
|
<td>9</td>
|
||||||
|
<td><b>12 Nov</b> (no class)</td>
|
||||||
|
<td><b>14 Nov</b> (tutorial only)</td>
|
||||||
|
<td><b>16 Nov</b> (no class)</td>
|
||||||
|
</tr>
|
||||||
|
<tr>
|
||||||
|
<td>10</td>
|
||||||
|
<td><b>19 Nov</b> (no class)</td>
|
||||||
|
<td><b>21 Nov</b> Propositions as Types</td>
|
||||||
|
<td><b>23 Nov</b> (no class)</td>
|
||||||
|
</tr>
|
||||||
|
<tr>
|
||||||
|
<td>11</td>
|
||||||
|
<td><b>26 Nov</b> (no class)</td>
|
||||||
|
<td><b>28 Nov</b> Quantitative Type Theory (Wen)</td>
|
||||||
|
<td><b>30 Nov</b> (mock exam)</td>
|
||||||
|
</tr>
|
||||||
|
</table>
|
||||||
|
|
||||||
|
## Assignments
|
||||||
|
|
||||||
|
For instructions on how to set up Agda for PLFA see [Getting Started](/GettingStarted/).
|
||||||
|
|
||||||
|
* [Assignment 1][Assignment1] cw1 due 4pm Thursday 4 October (Week 3)
|
||||||
|
* [Assignment 2][Assignment2] cw2 due 4pm Thursday 18 October (Week 5)
|
||||||
|
* [Assignment 3][Assignment3] cw3 due 4pm Thursday 1 November (Week 7)
|
||||||
|
* [Assignment 4][Assignment4] cw4 due 4pm Thursday 15 November (Week 9)
|
||||||
|
* [Assignment 5](/tspl/Assignment5.pdf) cw5 due 4pm Thursday 22 November (Week 10)
|
||||||
|
<br />
|
||||||
|
Use file [Exam][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 [mock](/tspl/mock.pdf)
|
||||||
|
and the exam [instructions](/tspl/instructions.pdf).
|
||||||
1248
tspl/examhons2018.cls
Normal file
1248
tspl/examhons2018.cls
Normal file
File diff suppressed because it is too large
Load diff
BIN
tspl/instructions.pdf
Normal file
BIN
tspl/instructions.pdf
Normal file
Binary file not shown.
122
tspl/instructions.tex
Normal file
122
tspl/instructions.tex
Normal file
|
|
@ -0,0 +1,122 @@
|
||||||
|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||||
|
% Instructions for TSPL Exam
|
||||||
|
% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||||
|
|
||||||
|
\documentclass[12pt]{article}
|
||||||
|
\usepackage{a4,amssymb}
|
||||||
|
% \setlength{\oddsidemargin}{-1.5cm}
|
||||||
|
% \addtolength{\textwidth}{2cm}
|
||||||
|
% \addtolength{\textheight}{3cm}
|
||||||
|
|
||||||
|
\begin{document}
|
||||||
|
\pagestyle{empty}
|
||||||
|
\setcounter{page}{1}
|
||||||
|
|
||||||
|
\begin{center}
|
||||||
|
\large Types and Semantics for Programming Languages
|
||||||
|
\end{center}
|
||||||
|
|
||||||
|
\section*{Instructions}
|
||||||
|
|
||||||
|
\begin{enumerate}
|
||||||
|
|
||||||
|
\item
|
||||||
|
The exam lasts two hours.
|
||||||
|
|
||||||
|
\item
|
||||||
|
Place your student identity card face-up on the desk in front of you. The
|
||||||
|
invigilator may come to check your identity, and in this case you may be asked
|
||||||
|
to allow the invigilator to briefly use your computer. The exam time has been
|
||||||
|
calculated to allow time for such interruptions.
|
||||||
|
|
||||||
|
\item
|
||||||
|
You may log into your computer as soon as you are ready to do so.
|
||||||
|
|
||||||
|
\item
|
||||||
|
To download the exam paper, open a terminal window and type:
|
||||||
|
\begin{center}
|
||||||
|
\texttt{getpapers}
|
||||||
|
\end{center}
|
||||||
|
This will create a subdirectory \texttt{tspl-pe} in your home directory,
|
||||||
|
containing the following files.
|
||||||
|
\begin{center}
|
||||||
|
\begin{tabular}{ll}
|
||||||
|
\texttt{tspl-pe/papers/exam.pdf} & the exam \\
|
||||||
|
\texttt{tspl-pe/papers/instructions.pdf} & these instructions \\
|
||||||
|
\texttt{tspl-pe/templates/Exam.lagda} & exam template to edit \\
|
||||||
|
\texttt{tspl-pe/original\_templates/Exam.lagda} & backup of exam template
|
||||||
|
\end{tabular}
|
||||||
|
\end{center}
|
||||||
|
The directories \texttt{tspl-pe/papers} and
|
||||||
|
\texttt{tspl-pe/original\_templates}
|
||||||
|
are read only, but you may read and write \texttt{tspl-pe/templates}.
|
||||||
|
|
||||||
|
\item
|
||||||
|
To setup the Agda environment, open a second terminal window and type:
|
||||||
|
\begin{center}
|
||||||
|
\texttt{tspl-setup}
|
||||||
|
\end{center}
|
||||||
|
This will open a browser, with three tabs which contain the textbook
|
||||||
|
\emph{Programming Language Foundations in Agda}, the documentation for the
|
||||||
|
Agda standard library, and the documentation for Agda. (The browser may
|
||||||
|
also attempt to link to the internet, which brings up a tab labeled
|
||||||
|
``Problem loading page''; this is expected and not a problem.)
|
||||||
|
|
||||||
|
{\it (Note that internet access has been disabled.)}
|
||||||
|
|
||||||
|
\begin{center}
|
||||||
|
\textbf{Do nothing further until the start of the exam is announced!}
|
||||||
|
\end{center}
|
||||||
|
|
||||||
|
\hfill \textit{Please Turn Over}
|
||||||
|
\newpage
|
||||||
|
|
||||||
|
\item When the start of the exam is announced, open the exam paper
|
||||||
|
\begin{center}
|
||||||
|
\texttt{tspl-pe/papers/exam.pdf}
|
||||||
|
\end{center}
|
||||||
|
with the standard PDF viewer.
|
||||||
|
|
||||||
|
\item Change to the template directory
|
||||||
|
\begin{center}
|
||||||
|
\texttt{cd tspl-pe/templates}
|
||||||
|
\end{center}
|
||||||
|
and edit the file
|
||||||
|
\begin{center}
|
||||||
|
\texttt{Exam.lagda}
|
||||||
|
\end{center}
|
||||||
|
to include your answers, using Emacs or anything else suitable.
|
||||||
|
You are recommended to save your work on a regular basis.
|
||||||
|
|
||||||
|
\item Before submitting, make sure your file is processed by Agda
|
||||||
|
correctly. Code which prevents the file from compiling should be
|
||||||
|
made into comments. If you fail to solve part of a problem, you
|
||||||
|
may get more credit if you indicate clearly which part you have
|
||||||
|
not solved.
|
||||||
|
|
||||||
|
\item \emph{Please ensure before submission that the file}
|
||||||
|
\texttt{Exam.lagda} \emph{contains your solutions to the exam.} Submit
|
||||||
|
your file using the command:
|
||||||
|
\begin{center}
|
||||||
|
\texttt{examsubmit Exam.lagda}
|
||||||
|
\end{center}
|
||||||
|
If you get an error, please check carefully that your file is called
|
||||||
|
\texttt{Exam.lagda} and that you are in the same directory as this
|
||||||
|
file. If you continue to have problems, please contact one of the
|
||||||
|
invigilators.
|
||||||
|
|
||||||
|
Repeated submit commands are allowed, and will overwrite previous
|
||||||
|
submissions. The last file submitted will be the one marked.
|
||||||
|
|
||||||
|
\item When the invigilators announce the end of the exam, you must
|
||||||
|
submit and log out immediately.
|
||||||
|
|
||||||
|
\end{enumerate}
|
||||||
|
|
||||||
|
\end{document}
|
||||||
|
|
||||||
|
|
||||||
|
%%% Local Variables:
|
||||||
|
%%% mode: latex
|
||||||
|
%%% TeX-master: t
|
||||||
|
%%% End:
|
||||||
BIN
tspl/mock.pdf
Normal file
BIN
tspl/mock.pdf
Normal file
Binary file not shown.
407
tspl/mock.tex
Normal file
407
tspl/mock.tex
Normal file
|
|
@ -0,0 +1,407 @@
|
||||||
|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||||
|
%
|
||||||
|
% I N F O R M A T I C S
|
||||||
|
% Honours Exam LaTeX Template for Exam Authors
|
||||||
|
%
|
||||||
|
% Created: 12-Oct-2009 by G.O.Passmore.
|
||||||
|
% Last Updated: 10-Sep-2018 by I. Murray
|
||||||
|
%
|
||||||
|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||||
|
|
||||||
|
%%% The following define the status of the exam papers in the order
|
||||||
|
%%% required. Simply remove the comment (i.e., the % symbol) just
|
||||||
|
%%% before the appropriate one and comment the others out.
|
||||||
|
|
||||||
|
%\newcommand\status{\internal}
|
||||||
|
%\newcommand\status{\external}
|
||||||
|
\newcommand\status{\final}
|
||||||
|
|
||||||
|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||||
|
|
||||||
|
%%% The following three lines are always required. You may add
|
||||||
|
%%% custom packages to the one already defined if necessary.
|
||||||
|
|
||||||
|
\documentclass{examhons2018}
|
||||||
|
\usepackage{amssymb}
|
||||||
|
\usepackage{amsmath}
|
||||||
|
\usepackage{semantic}
|
||||||
|
\usepackage{stix}
|
||||||
|
|
||||||
|
%%% Uncomment the \checkmarksfalse line if the macros that check the
|
||||||
|
%%% mark totals cause problems. However, please do not make your
|
||||||
|
%%% questions add up to a non-standard number of marks without
|
||||||
|
%%% permission of the convenor.
|
||||||
|
%\checkmarksfalse
|
||||||
|
|
||||||
|
\begin{document}
|
||||||
|
|
||||||
|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||||
|
%
|
||||||
|
% Replace {ad} below with the ITO code for your course. This will
|
||||||
|
% be used by the ITO LaTeX installation to install course-specific
|
||||||
|
% data into the exam versions it produces from this document.
|
||||||
|
%
|
||||||
|
% Your choices are (in course title order):
|
||||||
|
%
|
||||||
|
% {anlp} - Acc. Natural Language Processing (MSc)
|
||||||
|
% {aleone} - Adaptive Learning Environments 1 (Inf4)
|
||||||
|
% {adbs} - Advanced Databases (Inf4)
|
||||||
|
% {av} - Advanced Vision (Inf4)
|
||||||
|
% {av-dl} - Advanced Vision - distance learning (MSc)
|
||||||
|
% {apl} - Advances in Programming Languages (Inf4)
|
||||||
|
% {abs} - Agent Based Systems [L10] (Inf3)
|
||||||
|
% {afds} - Algorithmic Foundations of Data Science (MSc)
|
||||||
|
% {agta} - Algorithmic Game Theory and its Apps. (MSc)
|
||||||
|
% {ads} - Algorithms and Data Structures (Inf3)
|
||||||
|
% {ad} - Applied Databases (MSc)
|
||||||
|
% {aipf} - Artificial Intelligence Present and Future (MSc)
|
||||||
|
% {ar} - Automated Reasoning (Inf3)
|
||||||
|
% {asr} - Automatic Speech Recognition (Inf4)
|
||||||
|
% {bioone} - Bioinformatics 1 (MSc)
|
||||||
|
% {biotwo} - Bioinformatics 2 (MSc)
|
||||||
|
% {bdl} - Blockchains and Distributed Ledgers (Inf4)
|
||||||
|
% {cqi} - Categories and Quantum Informatics (MSc)
|
||||||
|
% {copt} - Compiler Opimisation [L11] (Inf4)
|
||||||
|
% {ct} - Compiling Techniques (Inf3)
|
||||||
|
% {ccs} - Computational Cognitive Science (Inf3)
|
||||||
|
% {cmc} - Computational Complexity (Inf4)
|
||||||
|
% {ca} - Computer Algebra (Inf4)
|
||||||
|
% {cav} - Computer Animation and Visualisation (Inf4)
|
||||||
|
% {car} - Computer Architecture (Inf3)
|
||||||
|
% {comn} - Computer Comms. and Networks (Inf3)
|
||||||
|
% {cd} - Computer Design (Inf3)
|
||||||
|
% {cg} - Computer Graphics [L11] (Inf4)
|
||||||
|
% {cn} - Computer Networking [L11] (Inf4)
|
||||||
|
% {cp} - Computer Prog. Skills and Concepts (nonhons)
|
||||||
|
% {cs} - Computer Security (Inf3)
|
||||||
|
% {dds} - Data, Design and Society (nonhons)
|
||||||
|
% {dme} - Data Mining and Exploration (Msc)
|
||||||
|
% {dbs} - Database Systems (Inf3)
|
||||||
|
% {dmr} - Decision Making in Robots and Autonomous Agents(MSc)
|
||||||
|
% {dmmr} - Discrete Maths. and Math. Reasoning (nonhons)
|
||||||
|
% {ds} - Distributed Systems [L11] (Inf4)
|
||||||
|
% {epl} - Elements of Programming Languages (Inf3)
|
||||||
|
% {es} - Embedded Software (Inf4)
|
||||||
|
% {exc} - Extreme Computing (Inf4)
|
||||||
|
% {fv} - Formal Verification (Inf4)
|
||||||
|
% {fnlp} - Foundations of Natural Language Processing (Inf3)
|
||||||
|
% {hci} - Human-Computer Interaction [L11] (Inf4)
|
||||||
|
% {infonea} - Informatics 1 - Introduction to Computation(nonhons)
|
||||||
|
% different sittings for INF1A programming exams
|
||||||
|
% {infoneapone} - Informatics 1 - Introduction to Computation(nonhons)
|
||||||
|
% {infoneaptwo} - Informatics 1 - Introduction to Computation(nonhons)
|
||||||
|
% {infoneapthree} - Informatics 1 - Introduction to Computation(nonhons)
|
||||||
|
% {infonecg} - Informatics 1 - Cognitive Science (nonhons)
|
||||||
|
% {infonecl} - Informatics 1 - Computation and Logic (nonhons)
|
||||||
|
% {infoneda} - Informatics 1 - Data and Analysis (nonhons)
|
||||||
|
% {infonefp} - Informatics 1 - Functional Programming (nonhons)
|
||||||
|
% If there are two sittings of FP, use infonefpam for the first
|
||||||
|
% paper and infonefppm for the second sitting.
|
||||||
|
% {infoneop} - Informatics 1 - Object-Oriented Programming(nonhons)
|
||||||
|
% If there are two sittings of OOP, use infoneopam for the first
|
||||||
|
% paper and infoneoppm for the second sitting.
|
||||||
|
% {inftwoa} - Informatics 2A: Proc. F&N Languages (nonhons)
|
||||||
|
% {inftwob} - Informatics 2B: Algs., D.Structs., Learning(nonhons)
|
||||||
|
% {inftwoccs}- Informatics 2C-CS: Computer Systems (nonhons)
|
||||||
|
% {inftwocse}- Informatics 2C: Software Engineering (nonhons)
|
||||||
|
% {inftwod} - Informatics 2D: Reasoning and Agents (nonhons)
|
||||||
|
% {iar} - Intelligent Autonomous Robotics (Inf4)
|
||||||
|
% {it} - Information Theory (MSc)
|
||||||
|
% {imc} - Introduction to Modern Cryptography (Inf4)
|
||||||
|
% {iotssc} - Internet of Things, Systems, Security and the Cloud (Inf4)
|
||||||
|
% (iqc) - Introduction to Quantum Computing (Inf4)
|
||||||
|
% (itcs) - Introduction to Theoretical Computer Science (Inf3)
|
||||||
|
% {ivc} - Image and Vision Computing (MSc)
|
||||||
|
% {ivr} - Introduction to Vision and Robotics (Inf3)
|
||||||
|
% {ivr-dl} - Introduction to Vision and Robotics - distance learning (Msc)
|
||||||
|
% {iaml} - Introductory Applied Machine Learning (MSc)
|
||||||
|
% {iaml-dl} - Introductory Applied Machine Learning - distance learning (MSc)
|
||||||
|
% {lpt} - Logic Programming - Theory (Inf3)
|
||||||
|
% {lpp} - Logic Programming - Programming (Inf3)
|
||||||
|
% {mlpr} - Machine Learning & Pattern Recognition (Inf4)
|
||||||
|
% {mt} - Machine Translation (Inf4)
|
||||||
|
% {mi} - Music Informatics (MSc)
|
||||||
|
% {nlu} - Natural Language Understanding [L11] (Inf4)
|
||||||
|
% {nc} - Neural Computation (MSc)
|
||||||
|
% {nat} - Natural Computing (MSc)
|
||||||
|
% {nluplus} - Natural Language Understanding, Generation, and Machine Translation(MSc)
|
||||||
|
% {nip} - Neural Information Processing (MSc)
|
||||||
|
% {os} - Operating Systems (Inf3)
|
||||||
|
% {pa} - Parallel Architectures [L11] (Inf4)
|
||||||
|
% {pdiot} - Principles and Design of IoT Systems (Inf4)
|
||||||
|
% {ppls} - Parallel Prog. Langs. and Sys. [L11] (Inf4)
|
||||||
|
% {pm} - Performance Modelling (Inf4)
|
||||||
|
% {pmr} - Probabilistic Modelling and Reasoning (MSc)
|
||||||
|
% {pi} - Professional Issues (Inf3)
|
||||||
|
% {rc} - Randomness and Computation (Inf4)
|
||||||
|
% {rl} - Reinforcement Learning (MSc)
|
||||||
|
% {rlsc} - Robot Learning and Sensorimotor Control (MSc)
|
||||||
|
% {rss} - Robotics: Science and Systems (MSc)
|
||||||
|
% {sp} - Secure Programming (Inf4)
|
||||||
|
% {sws} - Semantic Web Systems (Inf4)
|
||||||
|
% {stn} - Social and Technological Networks (Inf4)
|
||||||
|
% {sapm} - Software Arch., Proc. and Mgmt. [L11] (Inf4)
|
||||||
|
% {sdm} - Software Design and Modelling (Inf3)
|
||||||
|
% {st} - Software Testing (Inf3)
|
||||||
|
% {ttds} - Text Technologies for Data Science (Inf4)
|
||||||
|
% {tspl} - Types and Semantics for Programming Langs. (Inf4)
|
||||||
|
% {usec} - Usable Security and Privacy (Inf4)
|
||||||
|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||||
|
|
||||||
|
\setcourse{tspl}
|
||||||
|
\initcoursedata
|
||||||
|
|
||||||
|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||||
|
%
|
||||||
|
% Set your exam rubric type.
|
||||||
|
%
|
||||||
|
% Most courses in the School have exams that add up to 50 marks,
|
||||||
|
% and your choices are:
|
||||||
|
% {qu1_and_either_qu2_or_qu3, any_two_of_three, do_exam}
|
||||||
|
% (which include the "CALCULATORS MAY NOT BE USED..." text), or
|
||||||
|
% {qu1_and_either_qu2_or_qu3_calc, any_two_of_three_calc, do_exam_calc}
|
||||||
|
% (which DO NOT include the "CALCULATORS MAY NOT BE USED..." text), or
|
||||||
|
% {custom}.
|
||||||
|
%
|
||||||
|
% Note, if you opt to create a custom rubric, you must:
|
||||||
|
%
|
||||||
|
% (i) **have permission** from the appropriate authority, and
|
||||||
|
% (ii) execute:
|
||||||
|
%
|
||||||
|
% \setrubrictype{} to specify the custom rubric information.
|
||||||
|
%
|
||||||
|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||||
|
|
||||||
|
\setrubric{qu1_and_either_qu2_or_qu3}
|
||||||
|
|
||||||
|
\examtitlepage
|
||||||
|
|
||||||
|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||||
|
%
|
||||||
|
% Manual override for total page number computation.
|
||||||
|
%
|
||||||
|
% As long as you run latex upon this document three times in a row,
|
||||||
|
% the right number of `total pages' should be computed and placed
|
||||||
|
% in the footer of all pages except the title page.
|
||||||
|
%
|
||||||
|
% But, if this fails, you can set that number yourself with the
|
||||||
|
% following command:
|
||||||
|
%
|
||||||
|
% \settotalpages{n} with n a natural number.
|
||||||
|
%
|
||||||
|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||||
|
|
||||||
|
|
||||||
|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||||
|
%
|
||||||
|
% Beginning of your exam text.
|
||||||
|
%
|
||||||
|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||||
|
|
||||||
|
\begin{enumerate}
|
||||||
|
|
||||||
|
\item \rubricqA
|
||||||
|
|
||||||
|
\newcommand{\key}{\texttt}
|
||||||
|
\newcommand{\List}{\key{list}}
|
||||||
|
\newcommand{\nil}{\texttt{[]}}
|
||||||
|
\newcommand{\cons}{\mathbin{\key{::}}}
|
||||||
|
\newcommand{\member}{\key{member}}
|
||||||
|
\newcommand{\sublist}{\key{sublist}}
|
||||||
|
|
||||||
|
This question uses the library definition of $\List$ in Agda.
|
||||||
|
Here is an informal definition of the predicates $\in$
|
||||||
|
and $\subseteq$. (In Emacs, you can type $\in$ as \verb$\in$ and $\subseteq$ as \verb$\subseteq$.)
|
||||||
|
$\subseteq$
|
||||||
|
\begin{gather*}
|
||||||
|
\inference[$\key{here}$]
|
||||||
|
{}
|
||||||
|
{x \in (x \cons xs)}
|
||||||
|
\qquad
|
||||||
|
\inference[$\key{there}$]
|
||||||
|
{x \in ys}
|
||||||
|
{x \in (y \cons ys)}
|
||||||
|
\\~\\
|
||||||
|
\inference[$\key{done}$]
|
||||||
|
{}
|
||||||
|
{\nil \subseteq ys}
|
||||||
|
\\~\\
|
||||||
|
\inference[$\key{keep}$]
|
||||||
|
{xs \subseteq ys}
|
||||||
|
{(x \cons xs) \subseteq (x \cons ys)}
|
||||||
|
\qquad
|
||||||
|
\inference[$\key{drop}$]
|
||||||
|
{xs \subseteq ys}
|
||||||
|
{xs \subseteq (y \cons ys)}
|
||||||
|
\end{gather*}
|
||||||
|
|
||||||
|
\begin{itemize}
|
||||||
|
|
||||||
|
\item[(a)] Formalise the definition above.
|
||||||
|
\marks{10}
|
||||||
|
|
||||||
|
\item[(b)] Prove each of the following.
|
||||||
|
\begin{itemize}
|
||||||
|
\item[(i)] $\key{2} \in \key{[1,2,3]}$
|
||||||
|
\item[(ii)] $\key{[1,3]} \subseteq \key{[1,2,3,4]}$
|
||||||
|
\end{itemize}
|
||||||
|
\marks{5}
|
||||||
|
|
||||||
|
\item[(c)] Prove the following.
|
||||||
|
\begin{center}
|
||||||
|
If $xs \subseteq ys$ then $z \in xs$ implies $z \in ys$ for all $z$.
|
||||||
|
\end{center}
|
||||||
|
\marks{10}
|
||||||
|
|
||||||
|
\end{itemize}
|
||||||
|
|
||||||
|
\newpage
|
||||||
|
|
||||||
|
\item \rubricqB
|
||||||
|
|
||||||
|
\newcommand{\Tree}{\texttt{Tree}}
|
||||||
|
\newcommand{\leaf}{\texttt{leaf}}
|
||||||
|
\newcommand{\branch}{\texttt{branch}}
|
||||||
|
\newcommand{\CASET}{\texttt{caseT}}
|
||||||
|
\newcommand{\caseT}[6]{\texttt{case}~#1~\texttt{[leaf}~#2~\Rightarrow~#3~\texttt{|}~#4~\texttt{branch}~#5~\Rightarrow~#6\texttt{]}}
|
||||||
|
\newcommand{\ubar}{\texttt{\underline{~}}}
|
||||||
|
\newcommand{\comma}{\,\texttt{,}\,}
|
||||||
|
\newcommand{\V}{\texttt{V}}
|
||||||
|
\newcommand{\dash}{\texttt{-}}
|
||||||
|
\newcommand{\Value}{\texttt{Value}}
|
||||||
|
\newcommand{\becomes}{\longrightarrow}
|
||||||
|
\newcommand{\subst}[3]{#1~\texttt{[}~#2~\texttt{:=}~#3~\texttt{]}}
|
||||||
|
|
||||||
|
|
||||||
|
You will be provided with a definition of intrinsically-typed lambda
|
||||||
|
calculus in Agda. Consider constructs satisfying the following rules,
|
||||||
|
written in extrinsically-typed style.
|
||||||
|
|
||||||
|
Typing:
|
||||||
|
\begin{gather*}
|
||||||
|
\inference[\leaf]
|
||||||
|
{\Gamma \vdash M \typecolon A}
|
||||||
|
{\Gamma \vdash \leaf~M \typecolon \Tree~A}
|
||||||
|
\quad
|
||||||
|
\inference[\branch]
|
||||||
|
{\Gamma \vdash M \typecolon \Tree~A \\
|
||||||
|
\Gamma \vdash N \typecolon \Tree~A}
|
||||||
|
{\Gamma \vdash M~\branch~N \typecolon \Tree~A}
|
||||||
|
\\~\\
|
||||||
|
\inference[\CASET]
|
||||||
|
{\Gamma \vdash L \typecolon \Tree~A \\
|
||||||
|
\Gamma \comma x \typecolon A \vdash M \typecolon B \\
|
||||||
|
\Gamma \comma y \typecolon \Tree~A \comma z \typecolon \Tree~A \vdash N \typecolon B}
|
||||||
|
{\Gamma \vdash \caseT{L}{x}{M}{y}{z}{N} \typecolon B}
|
||||||
|
\end{gather*}
|
||||||
|
|
||||||
|
Values:
|
||||||
|
\begin{gather*}
|
||||||
|
\inference[\V\dash\leaf]
|
||||||
|
{\Value~V}
|
||||||
|
{\Value~(\leaf~V)}
|
||||||
|
\qquad
|
||||||
|
\inference[\V\dash\branch]
|
||||||
|
{\Value~V \\
|
||||||
|
\Value~W}
|
||||||
|
{\Value~(V~\branch~W)}
|
||||||
|
\end{gather*}
|
||||||
|
|
||||||
|
Reduction:
|
||||||
|
\begin{gather*}
|
||||||
|
\inference[$\xi\dash\leaf$]
|
||||||
|
{M \becomes M'}
|
||||||
|
{\leaf{M} \becomes \leaf{M'}}
|
||||||
|
\\~\\
|
||||||
|
\inference[$\xi\dash\branch_1$]
|
||||||
|
{M \becomes M'}
|
||||||
|
{M~\branch~N \becomes M'~\branch~N}
|
||||||
|
\qquad
|
||||||
|
\inference[$\xi\dash\branch_2$]
|
||||||
|
{\Value~V \\
|
||||||
|
N \becomes N'}
|
||||||
|
{V~\branch~N \becomes V~\branch~N'}
|
||||||
|
\\~\\
|
||||||
|
\inference[$\xi\dash\CASET$]
|
||||||
|
{L \becomes L'}
|
||||||
|
{\begin{array}{c}
|
||||||
|
\caseT{L}{x}{M}{y}{z}{N} \becomes \\
|
||||||
|
{} \quad \caseT{L'}{x}{M}{y}{z}{N}
|
||||||
|
\end{array}}
|
||||||
|
\\~\\
|
||||||
|
\inference[$\beta\dash\leaf$]
|
||||||
|
{\Value~V}
|
||||||
|
{\caseT{(\leaf~V)}{x}{M}{y}{z}{N} \becomes \subst{M}{x}{V}}
|
||||||
|
\\~\\
|
||||||
|
\inference[$\beta\dash\branch$]
|
||||||
|
{\Value~V \\
|
||||||
|
\Value~W}
|
||||||
|
{\caseT{(V~\branch~W)}{x}{M}{y}{z}{N} \becomes \subst{\subst{N}{y}{V}}{z}{W}}
|
||||||
|
\end{gather*}
|
||||||
|
|
||||||
|
\begin{enumerate}
|
||||||
|
\item[(a)] Extend the given definition to formalise the evaluation and
|
||||||
|
typing rules, including any other required definitions.
|
||||||
|
\marks{12}
|
||||||
|
|
||||||
|
\item[(b)] Prove progress. You will be provided with a proof of
|
||||||
|
progress for the simply-typed lambda calculus that you may
|
||||||
|
extend.
|
||||||
|
\marks{13}
|
||||||
|
\end{enumerate}
|
||||||
|
|
||||||
|
Please delimit any code you add as follows.
|
||||||
|
\begin{verbatim}
|
||||||
|
-- begin
|
||||||
|
-- end
|
||||||
|
\end{verbatim}
|
||||||
|
|
||||||
|
\newpage
|
||||||
|
|
||||||
|
\item \rubricqC
|
||||||
|
|
||||||
|
\newcommand{\Lift}{\texttt{Lift}}
|
||||||
|
\newcommand{\delay}{\texttt{delay}}
|
||||||
|
\newcommand{\force}{\texttt{force}}
|
||||||
|
\newcommand{\up}{\uparrow}
|
||||||
|
\newcommand{\dn}{\downarrow}
|
||||||
|
|
||||||
|
You will be provided with a definition of inference for extrinsically-typed lambda
|
||||||
|
calculus in Agda. Consider constructs satisfying the following rules,
|
||||||
|
written in extrinsically-typed style that support bidirectional inference.
|
||||||
|
|
||||||
|
Typing:
|
||||||
|
\begin{gather*}
|
||||||
|
\inference[$\delay$]
|
||||||
|
{\Gamma \vdash M \dn A}
|
||||||
|
{\Gamma \vdash \delay~M \dn \Lift~A}
|
||||||
|
\\~\\
|
||||||
|
\inference[$\force$]
|
||||||
|
{\Gamma \vdash L \up \Lift~A}
|
||||||
|
{\Gamma \vdash \force~L \up A}
|
||||||
|
\end{gather*}
|
||||||
|
|
||||||
|
\begin{enumerate}
|
||||||
|
\item[(a)] Extend the given definition to formalise the typing rules,
|
||||||
|
and update the definition of equality on types.
|
||||||
|
\marks{10}
|
||||||
|
|
||||||
|
\item[(b)] Extend the code to support type inference for the new features.
|
||||||
|
\marks{15}
|
||||||
|
\end{enumerate}
|
||||||
|
|
||||||
|
Please delimit any code you add as follows.
|
||||||
|
\begin{verbatim}
|
||||||
|
-- begin
|
||||||
|
-- end
|
||||||
|
\end{verbatim}
|
||||||
|
|
||||||
|
\end{enumerate}
|
||||||
|
|
||||||
|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||||
|
%
|
||||||
|
% End of your exam text.
|
||||||
|
%
|
||||||
|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||||
|
|
||||||
|
\end{document}
|
||||||
3
tspl/tspl.agda-lib
Normal file
3
tspl/tspl.agda-lib
Normal file
|
|
@ -0,0 +1,3 @@
|
||||||
|
name: tspl
|
||||||
|
depend: standard-library plfa
|
||||||
|
include: .
|
||||||
Loading…
Reference in a new issue