Setup courses folder.
This commit is contained in:
Wen Kokke
parent
0b30c01a44
commit
48d7eefc3a
30 changed files with 3459 additions and 729 deletions
43
Makefile
43
Makefile
|
|
@ -1,7 +1,7 @@
|
|||
SHELL := /bin/bash
|
||||
agda := $(shell find . -type f -and \( -path '*/src/*' -or -path '*/tspl/*' \) -and -name '*.lagda.md')
|
||||
agdai := $(shell find . -type f -and \( -path '*/src/*' -or -path '*/tspl/*' \) -and -name '*.agdai')
|
||||
markdown := $(subst tspl/,out/,$(subst src/,out/,$(subst .lagda,,$(agda))))
|
||||
AGDA := $(shell find . -type f -and \( -path '*/src/*' -or -path '*/courses/*' \) -and -name '*.lagda.md')
|
||||
AGDAI := $(shell find . -type f -and \( -path '*/src/*' -or -path '*/courses/*' \) -and -name '*.agdai')
|
||||
MARKDOWN := $(subst courses/,out/,$(subst src/,out/,$(subst .lagda.md,.md,$(AGDA))))
|
||||
PLFA_DIR := $(shell dirname $(realpath $(lastword $(MAKEFILE_LIST))))
|
||||
AGDA2HTML_FLAGS := --verbose --link-to-local-agda-names --use-jekyll=out/
|
||||
AGDA_STDLIB_SED := ".agda-stdlib.sed"
|
||||
|
|
@ -12,6 +12,7 @@ else
|
|||
AGDA_STDLIB_URL := https://agda.github.io/agda-stdlib/v$(AGDA_STDLIB_VERSION)/
|
||||
endif
|
||||
|
||||
|
||||
# Build PLFA and test hyperlinks
|
||||
test: build
|
||||
ruby -S bundle exec htmlproofer _site
|
||||
|
|
@ -30,14 +31,24 @@ out/:
|
|||
mkdir -p out/
|
||||
|
||||
|
||||
# Build PLFA pages
|
||||
out/%.md: src/%.lagda.md | out/
|
||||
./highlight.sh $< $@
|
||||
# Convert literal Agda to Markdown
|
||||
define AGDA_template
|
||||
in := $(1)
|
||||
out := $(subst courses/,out/,$(subst src/,out/,$(subst .lagda.md,.md,$(1))))
|
||||
$$(out) : in = $(1)
|
||||
$$(out) : out = $(subst courses/,out/,$(subst src/,out/,$(subst .lagda.md,.md,$(1))))
|
||||
$$(out) : $$(in) | out/
|
||||
@echo "Processing $$(subst ./,,$$(in))"
|
||||
ifeq (,$$(findstring courses/,$$(in)))
|
||||
./highlight.sh $$(in) $$(out)
|
||||
else
|
||||
# Fix links to the file itself (out/<filename> to out/<filepath>)
|
||||
./highlight.sh $$(in) $$(out) --include-path $(realpath src) --include-path $$(realpath $$(dir $$(in)))
|
||||
@sed -i 's|out/$$(notdir $$(out))|$$(subst ./,,$$(out))|g' $$(out)
|
||||
endif
|
||||
endef
|
||||
|
||||
|
||||
# Build TSPL pages
|
||||
out/%.md: tspl/%.lagda.md | out/
|
||||
./highlight.sh $< $@ --include-path $(realpath src) --include-path $(realpath tspl)
|
||||
$(foreach agda,$(AGDA),$(eval $(call AGDA_template,$(agda))))
|
||||
|
||||
|
||||
# Start server
|
||||
|
|
@ -57,26 +68,26 @@ server-stop:
|
|||
|
||||
# Build website using jekyll
|
||||
build: AGDA2HTML_FLAGS += --link-to-agda-stdlib=$(AGDA_STDLIB_URL)
|
||||
build: $(markdown)
|
||||
build: $(MARKDOWN)
|
||||
ruby -S bundle exec jekyll build
|
||||
|
||||
|
||||
# Build website using jekyll offline
|
||||
build-offline: $(markdown)
|
||||
build-offline: $(MARKDOWN)
|
||||
ruby -S bundle exec jekyll build
|
||||
|
||||
|
||||
# Build website using jekyll incrementally
|
||||
build-incremental: AGDA2HTML_FLAGS += --link-to-agda-stdlib
|
||||
build-incremental: $(markdown)
|
||||
build-incremental: $(MARKDOWN)
|
||||
ruby -S bundle exec jekyll build --incremental
|
||||
|
||||
|
||||
# Remove all auxiliary files
|
||||
clean:
|
||||
rm -f $(AGDA_STDLIB_SED)
|
||||
ifneq ($(strip $(agdai)),)
|
||||
rm $(agdai)
|
||||
ifneq ($(strip $(AGDAI)),)
|
||||
rm $(AGDAI)
|
||||
endif
|
||||
|
||||
|
||||
|
|
@ -90,7 +101,7 @@ clobber: clean
|
|||
|
||||
# List all .lagda files
|
||||
ls:
|
||||
@echo $(agda)
|
||||
@echo $(AGDA)
|
||||
|
||||
.phony: ls
|
||||
|
||||
|
|
|
|||
|
|
@ -1,11 +1,11 @@
|
|||
---
|
||||
title : "PUC-Assignment1: PUC Assignment 1"
|
||||
title : "Assignment1: PUC Assignment 1"
|
||||
layout : page
|
||||
permalink : /PUC-Assignment1/
|
||||
permalink : /PUC/2019/Assignment1/
|
||||
---
|
||||
|
||||
```
|
||||
module PUC-Assignment1 where
|
||||
module Assignment1 where
|
||||
```
|
||||
|
||||
## YOUR NAME AND EMAIL GOES HERE
|
||||
|
|
@ -122,7 +122,7 @@ Give an example of an operator that has an identity and is
|
|||
associative but is not commutative.
|
||||
|
||||
|
||||
#### Exercise `finite-+-assoc` (stretch) {#finite-plus-assoc}
|
||||
#### Exercise `finite-|-assoc` (stretch) {#finite-plus-assoc}
|
||||
|
||||
Write out what is known about associativity of addition on each of the first four
|
||||
days using a finite story of creation, as
|
||||
|
|
@ -176,7 +176,7 @@ Show
|
|||
|
||||
for all naturals `n`. Did your proof require induction?
|
||||
|
||||
#### Exercise `∸-+-assoc` {#monus-plus-assoc}
|
||||
#### Exercise `∸-|-assoc` {#monus-plus-assoc}
|
||||
|
||||
Show that monus associates with addition, that is,
|
||||
|
||||
|
|
@ -1,11 +1,11 @@
|
|||
---
|
||||
title : "PUC-Assignment2: PUC Assignment 2"
|
||||
title : "Assignment2: PUC Assignment 2"
|
||||
layout : page
|
||||
permalink : /PUC-Assignment2/
|
||||
permalink : /PUC/2019/Assignment2/
|
||||
---
|
||||
|
||||
```
|
||||
module PUC-Assignment2 where
|
||||
module Assignment2 where
|
||||
```
|
||||
|
||||
## YOUR NAME AND EMAIL GOES HERE
|
||||
|
|
@ -1,11 +1,11 @@
|
|||
---
|
||||
title : "PUC-Assignment3: PUC Assignment 3"
|
||||
title : "Assignment3: PUC Assignment 3"
|
||||
layout : page
|
||||
permalink : /PUC-Assignment3/
|
||||
permalink : /PUC/2019/Assignment3/
|
||||
---
|
||||
|
||||
```
|
||||
module PUC-Assignment3 where
|
||||
module Assignment3 where
|
||||
```
|
||||
|
||||
## YOUR NAME AND EMAIL GOES HERE
|
||||
|
|
@ -1,11 +1,11 @@
|
|||
---
|
||||
title : "PUC-Assignment4: PUC Assignment 4"
|
||||
title : "Assignment4: PUC Assignment 4"
|
||||
layout : page
|
||||
permalink : /PUC-Assignment4/
|
||||
permalink : /PUC/2019/Assignment4/
|
||||
---
|
||||
|
||||
```
|
||||
module PUC-Assignment4 where
|
||||
module Assignment4 where
|
||||
```
|
||||
|
||||
## YOUR NAME AND EMAIL GOES HERE
|
||||
|
|
@ -1,11 +1,11 @@
|
|||
---
|
||||
title : "PUC-Assignment5: PUC Assignment 5"
|
||||
title : "Assignment5: PUC Assignment 5"
|
||||
layout : page
|
||||
permalink : /PUC-Assignment5/
|
||||
permalink : /PUC/2019/Assignment5/
|
||||
---
|
||||
|
||||
```
|
||||
module PUC-Assignment5 where
|
||||
module Assignment5 where
|
||||
```
|
||||
|
||||
## YOUR NAME AND EMAIL GOES HERE
|
||||
|
|
@ -1,7 +1,7 @@
|
|||
---
|
||||
title : "Exam: TSPL Mock Exam file"
|
||||
layout : page
|
||||
permalink : /Exam/
|
||||
permalink : /PUC/2019/Exam/
|
||||
---
|
||||
|
||||
|
||||
|
|
@ -419,4 +419,3 @@ Please delimit any code you add as follows.
|
|||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||
|
||||
\end{document}
|
||||
|
||||
|
|
@ -1244,5 +1244,3 @@ THIS EXAMINATION WILL BE MARKED ANONYMOUSLY
|
|||
|
||||
\status
|
||||
}
|
||||
|
||||
|
||||
|
|
@ -1,7 +1,7 @@
|
|||
---
|
||||
title : "PUC-Rio: Course notes"
|
||||
layout : page
|
||||
permalink : /PUC/
|
||||
permalink : /PUC/2019/
|
||||
---
|
||||
|
||||
## Staff
|
||||
|
|
@ -94,14 +94,14 @@ Lectures and tutorials take place Fridays and some Thursdays in 548L.
|
|||
|
||||
For instructions on how to set up Agda for PLFA see [Getting Started](/GettingStarted/).
|
||||
|
||||
* [PUC Assignment 1][PUC-Assignment1] due Friday 26 April.
|
||||
* [PUC Assignment 2][PUC-Assignment2] due Wednesday 22 May.
|
||||
* [PUC Assignment 3][PUC-Assignment3] due Wednesday 5 June.
|
||||
* [PUC Assignment 4][PUC-Assignment4] due Wednesday 19 June.
|
||||
* [PUC Assignment 5][PUC-Assignment5] due Tuesday 25 June.
|
||||
* [PUC Assignment 6](/tspl/first-mock.pdf) due Tuesday 25 June.
|
||||
Use file [Exam][Exam]. Despite the rubric, do **all three questions**.
|
||||
* [PUC Assignment 1](/PUC/2019/Assignment1/) due Friday 26 April.
|
||||
* [PUC Assignment 2](/PUC/2019/Assignment2/) due Wednesday 22 May.
|
||||
* [PUC Assignment 3](/PUC/2019/Assignment3/) due Wednesday 5 June.
|
||||
* [PUC Assignment 4](/PUC/2019/Assignment4/) due Wednesday 19 June.
|
||||
* [PUC Assignment 5](/PUC/2019/Assignment5/) due Tuesday 25 June.
|
||||
* [PUC Assignment 6](/courses/tspl/2018/Mock1.pdf) due Tuesday 25 June.
|
||||
Use file [Exam](/PUC/2019/Exam/). Despite the rubric, do **all three questions**.
|
||||
|
||||
Submit assignments by email to [wadler@inf.ed.ac.uk](mailto:wadler@inf.ed.ac.uk).
|
||||
Attach a single file named `PUC-Assignment1.lagda` or the like. Include
|
||||
Attach a single file named `Assignment1.lagda.md` or the like. Include
|
||||
your name and email in the submitted file.
|
||||
|
|
@ -1,7 +1,7 @@
|
|||
---
|
||||
title : "Assignment1: TSPL Assignment 1"
|
||||
layout : page
|
||||
permalink : /Assignment1/
|
||||
permalink : /TSPL/2018/Assignment1/
|
||||
---
|
||||
|
||||
```
|
||||
|
|
@ -125,7 +125,7 @@ Give an example of an operator that has an identity and is
|
|||
associative but is not commutative.
|
||||
|
||||
|
||||
#### Exercise `finite-+-assoc` (stretch) {#finite-plus-assoc}
|
||||
#### Exercise `finite-|-assoc` (stretch) {#finite-plus-assoc}
|
||||
|
||||
Write out what is known about associativity of addition on each of the first four
|
||||
days using a finite story of creation, as
|
||||
|
|
@ -179,7 +179,7 @@ Show
|
|||
|
||||
for all naturals `n`. Did your proof require induction?
|
||||
|
||||
#### Exercise `∸-+-assoc` {#monus-plus-assoc}
|
||||
#### Exercise `∸-|-assoc` {#monus-plus-assoc}
|
||||
|
||||
Show that monus associates with addition, that is,
|
||||
|
||||
|
|
@ -1,7 +1,7 @@
|
|||
---
|
||||
title : "Assignment2: TSPL Assignment 2"
|
||||
layout : page
|
||||
permalink : /Assignment2/
|
||||
permalink : /TSPL/2018/Assignment2/
|
||||
---
|
||||
|
||||
```
|
||||
|
|
@ -1,7 +1,7 @@
|
|||
---
|
||||
title : "Assignment3: TSPL Assignment 3"
|
||||
layout : page
|
||||
permalink : /Assignment3/
|
||||
permalink : /TSPL/2018/Assignment3/
|
||||
---
|
||||
|
||||
```
|
||||
|
|
@ -1,7 +1,7 @@
|
|||
---
|
||||
title : "Assignment4: TSPL Assignment 4"
|
||||
layout : page
|
||||
permalink : /Assignment4/
|
||||
permalink : /TSPL/2018/Assignment4/
|
||||
---
|
||||
|
||||
```
|
||||
678
courses/tspl/2018/Exam.lagda.md
Normal file
678
courses/tspl/2018/Exam.lagda.md
Normal file
|
|
@ -0,0 +1,678 @@
|
|||
---
|
||||
title : "Exam: TSPL Mock Exam file"
|
||||
layout : page
|
||||
permalink : /TSPL/2018/Exam/
|
||||
---
|
||||
|
||||
|
||||
```
|
||||
module Exam where
|
||||
```
|
||||
|
||||
**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
|
||||
|
||||
```
|
||||
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 Relation.Nullary using (¬_; Dec; yes; no)
|
||||
open import Relation.Binary using (Decidable)
|
||||
```
|
||||
|
||||
## Problem 1
|
||||
|
||||
```
|
||||
module Problem1 where
|
||||
|
||||
open import Function using (_∘_)
|
||||
```
|
||||
|
||||
Remember to indent all code by two spaces.
|
||||
|
||||
### (a)
|
||||
|
||||
### (b)
|
||||
|
||||
### (c)
|
||||
|
||||
|
||||
## Problem 2
|
||||
|
||||
Remember to indent all code by two spaces.
|
||||
|
||||
```
|
||||
module Problem2 where
|
||||
```
|
||||
|
||||
### Infix declarations
|
||||
|
||||
```
|
||||
infix 4 _⊢_
|
||||
infix 4 _∋_
|
||||
infixl 5 _,_
|
||||
|
||||
infixr 7 _⇒_
|
||||
|
||||
infix 5 ƛ_
|
||||
infix 5 μ_
|
||||
infixl 7 _·_
|
||||
infix 8 `suc_
|
||||
infix 9 `_
|
||||
infix 9 S_
|
||||
infix 9 #_
|
||||
```
|
||||
|
||||
### Types and contexts
|
||||
|
||||
```
|
||||
data Type : Set where
|
||||
_⇒_ : Type → Type → Type
|
||||
`ℕ : Type
|
||||
|
||||
data Context : Set where
|
||||
∅ : Context
|
||||
_,_ : Context → Type → Context
|
||||
```
|
||||
|
||||
### Variables and the lookup judgment
|
||||
|
||||
```
|
||||
data _∋_ : Context → Type → Set where
|
||||
|
||||
Z : ∀ {Γ A}
|
||||
----------
|
||||
→ Γ , A ∋ A
|
||||
|
||||
S_ : ∀ {Γ A B}
|
||||
→ Γ ∋ A
|
||||
---------
|
||||
→ Γ , B ∋ A
|
||||
```
|
||||
|
||||
### Terms and the typing judgment
|
||||
|
||||
```
|
||||
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
|
||||
```
|
||||
|
||||
### Abbreviating de Bruijn indices
|
||||
|
||||
```
|
||||
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
|
||||
```
|
||||
|
||||
### Renaming
|
||||
|
||||
```
|
||||
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)
|
||||
```
|
||||
|
||||
### Simultaneous Substitution
|
||||
|
||||
```
|
||||
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)
|
||||
```
|
||||
|
||||
### Single substitution
|
||||
|
||||
```
|
||||
_[_] : ∀ {Γ A B}
|
||||
→ Γ , B ⊢ A
|
||||
→ Γ ⊢ B
|
||||
---------
|
||||
→ Γ ⊢ A
|
||||
_[_] {Γ} {A} {B} N M = subst {Γ , B} {Γ} σ {A} N
|
||||
where
|
||||
σ : ∀ {A} → Γ , B ∋ A → Γ ⊢ A
|
||||
σ Z = M
|
||||
σ (S x) = ` x
|
||||
```
|
||||
|
||||
### Values
|
||||
|
||||
```
|
||||
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)
|
||||
```
|
||||
|
||||
### Reduction
|
||||
|
||||
```
|
||||
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 ]
|
||||
```
|
||||
|
||||
|
||||
### Reflexive and transitive closure
|
||||
|
||||
```
|
||||
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
|
||||
```
|
||||
|
||||
|
||||
### Progress
|
||||
|
||||
```
|
||||
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 (β-μ)
|
||||
```
|
||||
|
||||
### Evaluation
|
||||
|
||||
```
|
||||
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
|
||||
```
|
||||
|
||||
## Problem 3
|
||||
|
||||
Remember to indent all code by two spaces.
|
||||
|
||||
```
|
||||
module Problem3 where
|
||||
```
|
||||
|
||||
### Imports
|
||||
|
||||
```
|
||||
import plfa.DeBruijn as DB
|
||||
```
|
||||
|
||||
### Syntax
|
||||
|
||||
```
|
||||
infix 4 _∋_⦂_
|
||||
infix 4 _⊢_↑_
|
||||
infix 4 _⊢_↓_
|
||||
infixl 5 _,_⦂_
|
||||
|
||||
infix 5 ƛ_⇒_
|
||||
infix 5 μ_⇒_
|
||||
infix 6 _↑
|
||||
infix 6 _↓_
|
||||
infixl 7 _·_
|
||||
infix 8 `suc_
|
||||
infix 9 `_
|
||||
```
|
||||
|
||||
### Types
|
||||
|
||||
```
|
||||
data Type : Set where
|
||||
_⇒_ : Type → Type → Type
|
||||
`ℕ : Type
|
||||
```
|
||||
|
||||
### Identifiers
|
||||
|
||||
```
|
||||
Id : Set
|
||||
Id = String
|
||||
```
|
||||
|
||||
### Contexts
|
||||
|
||||
```
|
||||
data Context : Set where
|
||||
∅ : Context
|
||||
_,_⦂_ : Context → Id → Type → Context
|
||||
```
|
||||
|
||||
### Terms
|
||||
|
||||
```
|
||||
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⁻
|
||||
```
|
||||
|
||||
### Lookup
|
||||
|
||||
```
|
||||
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
|
||||
```
|
||||
|
||||
### Bidirectional type checking
|
||||
|
||||
```
|
||||
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
|
||||
```
|
||||
|
||||
|
||||
### Type equality
|
||||
|
||||
```
|
||||
_≟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
|
||||
```
|
||||
|
||||
### Prerequisites
|
||||
|
||||
```
|
||||
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
|
||||
ℕ≢⇒ ()
|
||||
```
|
||||
|
||||
|
||||
### Unique lookup
|
||||
|
||||
```
|
||||
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′
|
||||
```
|
||||
|
||||
### Unique synthesis
|
||||
|
||||
```
|
||||
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
|
||||
```
|
||||
|
||||
## Lookup type of a variable in the context
|
||||
|
||||
```
|
||||
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 ⟩
|
||||
```
|
||||
|
||||
### Promoting negations
|
||||
|
||||
```
|
||||
¬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
|
||||
```
|
||||
|
||||
|
||||
## Synthesize and inherit types
|
||||
|
||||
```
|
||||
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)
|
||||
```
|
||||
122
courses/tspl/2018/Instructions.tex
Normal file
122
courses/tspl/2018/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:
|
||||
421
courses/tspl/2018/Mock1.tex
Normal file
421
courses/tspl/2018/Mock1.tex
Normal file
|
|
@ -0,0 +1,421 @@
|
|||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||
%
|
||||
% 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}
|
||||
407
courses/tspl/2018/Mock2.tex
Normal file
407
courses/tspl/2018/Mock2.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}
|
||||
1246
courses/tspl/2018/examhons2018.cls
Normal file
1246
courses/tspl/2018/examhons2018.cls
Normal file
File diff suppressed because it is too large
Load diff
3
courses/tspl/2018/tspl2018.agda-lib
Normal file
3
courses/tspl/2018/tspl2018.agda-lib
Normal file
|
|
@ -0,0 +1,3 @@
|
|||
name: tspl
|
||||
depend: standard-library plfa
|
||||
include: .
|
||||
|
|
@ -1,7 +1,7 @@
|
|||
---
|
||||
title : "TSPL: Course notes"
|
||||
layout : page
|
||||
permalink : /TSPL/
|
||||
permalink : /TSPL/2018/
|
||||
---
|
||||
|
||||
## Staff
|
||||
|
|
@ -97,13 +97,13 @@ Lectures take place Monday, Wednesday, and Friday in AT 7.02. (Moved from AT 5.0
|
|||
|
||||
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/first-mock.pdf) cw5 due 4pm Thursday 22 November (Week 10)
|
||||
* [Assignment 1](/TSPL/2018/Assignment1/) cw1 due 4pm Thursday 4 October (Week 3)
|
||||
* [Assignment 2](/TSPL/2018/Assignment2/) cw2 due 4pm Thursday 18 October (Week 5)
|
||||
* [Assignment 3](/TSPL/2018/Assignment3/) cw3 due 4pm Thursday 1 November (Week 7)
|
||||
* [Assignment 4](/TSPL/2018/Assignment4/) cw4 due 4pm Thursday 15 November (Week 9)
|
||||
* [Assignment 5](/courses/tspl/2018/Mock1.pdf) cw5 due 4pm Thursday 22 November (Week 10)
|
||||
<br />
|
||||
Use file [Exam][Exam]. Despite the rubric, do **all three questions**.
|
||||
Use file [Exam](/TSPL/2018/Exam/). Despite the rubric, do **all three questions**.
|
||||
|
||||
|
||||
Assignments are submitted by running
|
||||
|
|
@ -114,5 +114,5 @@ where N is the number of the assignment.
|
|||
|
||||
## Mock exam
|
||||
|
||||
Here is the text of the [second mock](/tspl/second-mock.pdf)
|
||||
and the exam [instructions](/tspl/instructions.pdf).
|
||||
Here is the text of the [second mock](/courses/tspl/2018/Mock2.pdf)
|
||||
and the exam [instructions](/courses/tspl/2018/Instructions.pdf).
|
||||
17
highlight.sh
17
highlight.sh
|
|
@ -9,18 +9,27 @@ OUT="$1"
|
|||
OUT_DIR="$(dirname $OUT)"
|
||||
shift
|
||||
|
||||
# Extract the module name from the Agda file
|
||||
# NOTE: this fails if there is more than a single space after 'module'
|
||||
MOD_NAME=`grep -oP -m 1 "(?<=^module )(\\S+)(?=\\s+(\\S+\\s+)*where)" "$SRC"`
|
||||
|
||||
# Create temporary directory and compute path to output of `agda --html`
|
||||
# NOTE: this assumes $OUT is equivalent to out/ plus the module path
|
||||
HTML_DIR="$(mktemp -d)"
|
||||
HTML="${OUT#out/}"
|
||||
HTML="/${HTML//\//.}"
|
||||
HTML="$HTML_DIR/$HTML"
|
||||
SRC_EXT="$(basename $SRC)"
|
||||
SRC_EXT="${SRC_EXT##*.}"
|
||||
HTML="$HTML_DIR/$MOD_NAME.$SRC_EXT"
|
||||
|
||||
# Highlight Syntax using Agda
|
||||
set -o pipefail \
|
||||
&& agda --html --html-highlight=code --html-dir="$HTML_DIR" "$SRC" "$@" \
|
||||
| sed '/^Generating.*/d; /^Warning\: HTML.*/d; /^reached from the.*/d; /^\s*$/d'
|
||||
|
||||
# Check if the highlighted file was successfully generated
|
||||
if [[ ! -f "$HTML" ]]; then
|
||||
echo "File not generated: $FILE"
|
||||
exit 1
|
||||
fi
|
||||
|
||||
# Add source file to the Jekyll metadata
|
||||
sed -i "1 s|---|---\nsrc: $SRC|" "$HTML"
|
||||
|
||||
|
|
|
|||
4
index.md
4
index.md
|
|
@ -49,12 +49,12 @@ Pull requests are encouraged.
|
|||
|
||||
- Courses taught from the textbook:
|
||||
* Philip Wadler, University of Edinburgh,
|
||||
[2018](/TSPL/)
|
||||
[2018](/TSPL/2018/)
|
||||
* David Darais, University of Vermont,
|
||||
[2018](http://david.darais.com/courses/fa2018-cs295A/)
|
||||
* John Leo, Google Seattle, 2018--2019
|
||||
* Philip Wadler, Pontifícia Universidade Católica do Rio de Janeiro (PUC-Rio),
|
||||
[2019](/PUC/)
|
||||
[2019](/PUC/2019/)
|
||||
- A paper describing the book appeared in [SBMF][sbmf]
|
||||
|
||||
[wen]: https://github.com/wenkokke
|
||||
|
|
|
|||
|
|
@ -1,164 +0,0 @@
|
|||
---
|
||||
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)
|
||||
Binary file not shown.
Binary file not shown.
Binary file not shown.
Loading…
Reference in a new issue