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

added mocks

Browse source
This commit is contained in:
Philip Wadler 2019-11-15 10:55:08 +00:00
parent b885666c03
commit 345d422605
6 changed files with 1508 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

678
courses/tspl/2019/Exam.lagda.md Normal file
View file

@ -0,0 +1,678 @@
---
title : "Exam: TSPL Mock Exam file"
layout : page
permalink : /TSPL/2019/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.part2.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)
```

BIN
courses/tspl/2019/Mock1.pdf Normal file
View file

Binary file not shown.

421
courses/tspl/2019/Mock1.tex Normal file
View 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}

BIN
courses/tspl/2019/Mock2.pdf Normal file
View file

Binary file not shown.

407
courses/tspl/2019/Mock2.tex Normal file
View 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}

5
courses/tspl/2019/tspl2019.md
View file

@ -123,9 +123,8 @@ For instructions on how to set up Agda for PLFA see [Getting Started]({{ site.ba
* [Assignment 2]({{ site.baseurl }}/TSPL/2019/Assignment2/) cw2 due 4pm Thursday 17 October (Week 5)
* [Assignment 3]({{ site.baseurl }}/TSPL/2019/Assignment3/) cw3 due 4pm Thursday 31 October (Week 7)
* [Assignment 4]({{ site.baseurl }}/TSPL/2019/Assignment4/) cw4 due 4pm Thursday 14 November (Week 9)
* Assignment 5 <!-- [Assignment 5]({{ site.baseurl }}/courses/tspl/2010/Mock1.pdf) --> cw5 due 4pm Thursday 21 November (Week 10)
<!-- <br />
Use file [Exam]({{ site.baseurl }}/TSPL/2018/Exam/). Despite the rubric, do **all three questions**. -->
* [Assignment 5]({{ site.baseurl }}/courses/tspl/2019/Mock1.pdf) cw5 due 4pm Thursday 21 November (Week 10)
Use file [Exam]({{ site.baseurl }}/TSPL/2019/Exam/). Despite the rubric, do **all three questions**.
Assignments are submitted by running