Removed TSPL 2018, PUC 2019, Padova 2019, and ICFP 2019 from courses.
This commit is contained in:
Wen Kokke
parent
32978b5651
commit
5d022d7014
24 changed files with 0 additions and 8440 deletions
|
|
@ -1,158 +0,0 @@
|
|||
----------------------------------------------------------------------
|
||||
ICFP 2019
|
||||
24th ACM SIGPLAN International Conference on Functional Programming
|
||||
|
||||
August 18 - 23, 2019
|
||||
Berlin, Germany
|
||||
https://icfp19.sigplan.org/
|
||||
|
||||
TUTORIAL PROPOSAL FORM
|
||||
|
||||
----------------------------------------------------------------------
|
||||
|
||||
This form is due May 10th, 2019.
|
||||
|
||||
|
||||
NAME OF THE TUTORIAL:
|
||||
|
||||
Programming Language Foundations in Agda
|
||||
|
||||
|
||||
PRESENTER(S):
|
||||
|
||||
(Please complete the following table for each presenter.)
|
||||
|
||||
Name : Philip Wadler
|
||||
Address : LFCS, School of Informatics, University of Edinbugh
|
||||
Email : wadler@inf.ed.ac.uk
|
||||
Phone : +44 131 650 5174 (after 21 July)
|
||||
Mobile : +55 71 99652 2018 (before 13 July)
|
||||
+44 7976 507 543 (after 14 July)
|
||||
|
||||
|
||||
ABSTRACT:
|
||||
|
||||
This course is in two parts, each three hours long. Part I is an
|
||||
introduction to formal methods in Agda, covering datatypes,
|
||||
recursion, structural induction, indexed datatypes, dependent
|
||||
functions, and induction over evidence; with focus on formal
|
||||
definitions of naturals, addition, and inequality, and their
|
||||
properties. Part II is an introduction to formal models of
|
||||
simply-typed lambda calculus in Agda, including reduction, type
|
||||
rules, and progress and preservation, and (as a consequence)
|
||||
evaluation of lambda terms. Part II depends on Part I, but Part I
|
||||
can be skipped by those already familiar with Agda.
|
||||
|
||||
The textbook is freely available online:
|
||||
Programming Language Foundations in Agda
|
||||
plfa.inf.ed.ac.uk
|
||||
github.com/plfa/plfa.github.io/
|
||||
|
||||
The books has been used for teaching by me at:
|
||||
University of Edinburgh (Sep-Dec 2018)
|
||||
Pontifícia Universidade Católica do Rio de Janeiro (PUC-Rio) (Mar-Jul 2019)
|
||||
University of Padova (Jun 2019)
|
||||
and by others at
|
||||
University of Vermont
|
||||
Google Seattle.
|
||||
The book is described in a paper (of the same title) at the XXI
|
||||
Brazilian Symposium on Formal Methods, 28--30 Nov 2018, which is
|
||||
available here:
|
||||
http://homepages.inf.ed.ac.uk/wadler/topics/agda.html#sbmf
|
||||
The paper won the SBMF 2018 Best Paper Award, 1st Place.
|
||||
|
||||
|
||||
REQUIRED PARTICIPANT BACKGROUND:
|
||||
|
||||
(What background knowledge and skills will be assumed? Is the
|
||||
tutorial primarily intended for industrial users of functional
|
||||
programming, researchers in functional programming, or some other
|
||||
audience?)
|
||||
|
||||
No prerequisites required. Any or all of the following will be
|
||||
helpful:
|
||||
* Familiarity with functional programming, particularly
|
||||
data types, recursion, and pattern matching.
|
||||
* Familiarity with proof by induction.
|
||||
* Familiarity with a proof assistant.
|
||||
* Familiarity with Emacs.
|
||||
|
||||
|
||||
LEARNING OUTCOMES:
|
||||
|
||||
(What will participants be able to do after the tutorial?)
|
||||
|
||||
Part I: Formulate and prove in Agda properties of
|
||||
operations of naturals (such as addition and multiplication), and
|
||||
relations on naturals (such as inequality), using structural
|
||||
induction and induction over evidence of a relation.
|
||||
|
||||
Part II: Formulate and prove in Agda formal models of simply-typed
|
||||
lambda calculus in Agda, including reduction, type rules, and
|
||||
progress and preservation, and (as a consequence) evaluation of
|
||||
lambda terms.
|
||||
|
||||
|
||||
SPECIAL REQUIREMENTS:
|
||||
|
||||
(Does the tutorial need Internet access for the presenter? For the
|
||||
participants?)
|
||||
|
||||
If the participants follow the instructions under 'Participant
|
||||
Preparation' in advance, then no internet access is required.
|
||||
|
||||
|
||||
|
||||
SCHEDULING CONSTRAINTS:
|
||||
(Are there any days on which you cannot hold the tutorial?)
|
||||
|
||||
None
|
||||
|
||||
|
||||
PARTICIPANT PREPARATION:
|
||||
|
||||
(What preparation is required? Do participants need to bring
|
||||
laptops? If so, do they need to have any particular software?)
|
||||
|
||||
Clone the repository at
|
||||
https://github.com/plfa/plfa.github.io/
|
||||
This is the textbook for the course.
|
||||
|
||||
Install Agda, the Agda standard library, and configure the
|
||||
plfa library. This can be done by following the instructions
|
||||
under the heading
|
||||
Getting Started with PLFA
|
||||
at
|
||||
https://plfa.github.io/GettingStarted/
|
||||
|
||||
|
||||
PLANS FOR PUBLICITY:
|
||||
|
||||
(Including, but not limited to, web pages, mailing lists, and
|
||||
newsgroups.)
|
||||
|
||||
I will advertise on my home page and blog, and on the home page for
|
||||
the textbook, and mail to Types and other standard lists.
|
||||
|
||||
|
||||
ADDITIONAL INFORMATION:
|
||||
|
||||
(If there is any additional information that you would like
|
||||
to make us aware of, please include the details here.
|
||||
|
||||
For example, you may wish to indicate a preference for particular
|
||||
dates, or that the tutorial should not be run in parallel with
|
||||
certain workshops; in such cases, please also include the
|
||||
reasons for your preference.)
|
||||
|
||||
None.
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
|
@ -1,44 +0,0 @@
|
|||
---
|
||||
title : "Padova: Course notes"
|
||||
layout : page
|
||||
permalink : /Padova/2019/
|
||||
---
|
||||
|
||||
## Staff
|
||||
|
||||
* **Instructor**
|
||||
[Philip Wadler](https://homepages.inf.ed.ac.uk/wadler)
|
||||
|
||||
* **Host**
|
||||
[Maria Emilia Maietti](https://www.math.unipd.it/~maietti/)
|
||||
|
||||
## Schedule
|
||||
|
||||
* 12.30--15.30, Wed 28 May 2019, Lecture and lab
|
||||
* 12.30--15.30, Thu 29 May 2019, Lecture and lab
|
||||
|
||||
<table>
|
||||
<tr>
|
||||
<td><b>Wed 28 May</b></td>
|
||||
<td><a href="{{ site.baseurl }}/Naturals/">Naturals</a>,
|
||||
<a href="{{ site.baseurl }}/Induction/">Induction</a> & <a href="{{ site.baseurl }}/Relations/">Relations</a></td>
|
||||
</tr>
|
||||
<tr>
|
||||
<td><b>Thu 29 May</b></td>
|
||||
<td><a href="{{ site.baseurl }}/Lambda/">Lambda</a> &
|
||||
<a href="{{ site.baseurl }}/Properties/">Properties</a></td>
|
||||
</tr>
|
||||
</table>
|
||||
|
||||
|
||||
## Assignments
|
||||
|
||||
For instructions on how to set up Agda for PLFA see [Getting Started]({{ site.baseurl }}/GettingStarted/).
|
||||
|
||||
* Wed 28 May
|
||||
- Naturals (`_^_`)
|
||||
- Induction (`+-swap`, `*-distrib-+`)
|
||||
- Relations (`<-trans`)
|
||||
* Wed 29 May
|
||||
- Lambda (`mul`, `mul-type`)
|
||||
- Properties (`mul-eval`)
|
||||
|
|
@ -1,311 +0,0 @@
|
|||
---
|
||||
title : "Assignment1: PUC Assignment 1"
|
||||
layout : page
|
||||
permalink : /PUC/2019/Assignment1/
|
||||
---
|
||||
|
||||
```
|
||||
module Assignment1 where
|
||||
```
|
||||
|
||||
## YOUR NAME AND EMAIL GOES HERE
|
||||
|
||||
## Introduction
|
||||
|
||||
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.
|
||||
|
||||
Please ensure your files execute correctly under Agda!
|
||||
|
||||
## Imports
|
||||
|
||||
```
|
||||
import Relation.Binary.PropositionalEquality as Eq
|
||||
open Eq using (_≡_; refl; cong; sym)
|
||||
open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; _≡⟨_⟩_; _∎)
|
||||
open import Data.Nat using (ℕ; zero; suc; _+_; _*_; _∸_; _≤_; z≤n; s≤s)
|
||||
open import Data.Nat.Properties using (+-assoc; +-identityʳ; +-suc; +-comm;
|
||||
≤-refl; ≤-trans; ≤-antisym; ≤-total; +-monoʳ-≤; +-monoˡ-≤; +-mono-≤)
|
||||
open import plfa.part1.Relations using (_<_; z<s; s<s; zero; suc; even; odd)
|
||||
```
|
||||
|
||||
## Naturals
|
||||
|
||||
#### Exercise `seven` {#seven}
|
||||
|
||||
Write out `7` in longhand.
|
||||
|
||||
|
||||
#### Exercise `+-example` {#plus-example}
|
||||
|
||||
Compute `3 + 4`, writing out your reasoning as a chain of equations.
|
||||
|
||||
|
||||
#### Exercise `*-example` {#times-example}
|
||||
|
||||
Compute `3 * 4`, writing out your reasoning as a chain of equations.
|
||||
|
||||
|
||||
#### Exercise `_^_` (recommended) {#power}
|
||||
|
||||
Define exponentiation, which is given by the following equations.
|
||||
|
||||
n ^ 0 = 1
|
||||
n ^ (1 + m) = n * (n ^ m)
|
||||
|
||||
Check that `3 ^ 4` is `81`.
|
||||
|
||||
|
||||
#### Exercise `∸-examples` (recommended) {#monus-examples}
|
||||
|
||||
Compute `5 ∸ 3` and `3 ∸ 5`, writing out your reasoning as a chain of equations.
|
||||
|
||||
|
||||
#### Exercise `Bin` (stretch) {#Bin}
|
||||
|
||||
A more efficient representation of natural numbers uses a binary
|
||||
rather than a unary system. We represent a number as a bitstring.
|
||||
```
|
||||
data Bin : Set where
|
||||
nil : Bin
|
||||
x0_ : Bin → Bin
|
||||
x1_ : Bin → Bin
|
||||
```
|
||||
For instance, the bitstring
|
||||
|
||||
1011
|
||||
|
||||
standing for the number eleven is encoded, right to left, as
|
||||
|
||||
x1 x1 x0 x1 nil
|
||||
|
||||
Representations are not unique due to leading zeros.
|
||||
Hence, eleven is also represented by `001011`, encoded as
|
||||
|
||||
x1 x1 x0 x1 x0 x0 nil
|
||||
|
||||
Define a function
|
||||
|
||||
inc : Bin → Bin
|
||||
|
||||
that converts a bitstring to the bitstring for the next higher
|
||||
number. For example, since `1100` encodes twelve, we should have
|
||||
|
||||
inc (x1 x1 x0 x1 nil) ≡ x0 x0 x1 x1 nil
|
||||
|
||||
Confirm that this gives the correct answer for the bitstrings
|
||||
encoding zero through four.
|
||||
|
||||
Using the above, define a pair of functions to convert
|
||||
between the two representations.
|
||||
|
||||
to : ℕ → Bin
|
||||
from : Bin → ℕ
|
||||
|
||||
For the former, choose the bitstring to have no leading zeros if it
|
||||
represents a positive natural, and represent zero by `x0 nil`.
|
||||
Confirm that these both give the correct answer for zero through four.
|
||||
|
||||
## Induction
|
||||
|
||||
#### Exercise `operators` {#operators}
|
||||
|
||||
Give another example of a pair of operators that have an identity
|
||||
and are associative, commutative, and distribute over one another.
|
||||
|
||||
Give an example of an operator that has an identity and is
|
||||
associative but is not commutative.
|
||||
|
||||
|
||||
#### Exercise `finite-|-assoc` (stretch) {#finite-plus-assoc}
|
||||
|
||||
Write out what is known about associativity of addition on each of the first four
|
||||
days using a finite story of creation, as
|
||||
[earlier][plfa.Naturals#finite-creation]
|
||||
|
||||
|
||||
#### Exercise `+-swap` (recommended) {#plus-swap}
|
||||
|
||||
Show
|
||||
|
||||
m + (n + p) ≡ n + (m + p)
|
||||
|
||||
for all naturals `m`, `n`, and `p`. No induction is needed,
|
||||
just apply the previous results which show addition
|
||||
is associative and commutative. You may need to use
|
||||
the following function from the standard library:
|
||||
|
||||
sym : ∀ {m n : ℕ} → m ≡ n → n ≡ m
|
||||
|
||||
|
||||
#### Exercise `*-distrib-+` (recommended) {#times-distrib-plus}
|
||||
|
||||
Show multiplication distributes over addition, that is,
|
||||
|
||||
(m + n) * p ≡ m * p + n * p
|
||||
|
||||
for all naturals `m`, `n`, and `p`.
|
||||
|
||||
#### Exercise `*-assoc` (recommended) {#times-assoc}
|
||||
|
||||
Show multiplication is associative, that is,
|
||||
|
||||
(m * n) * p ≡ m * (n * p)
|
||||
|
||||
for all naturals `m`, `n`, and `p`.
|
||||
|
||||
#### Exercise `*-comm` {#times-comm}
|
||||
|
||||
Show multiplication is commutative, that is,
|
||||
|
||||
m * n ≡ n * m
|
||||
|
||||
for all naturals `m` and `n`. As with commutativity of addition,
|
||||
you will need to formulate and prove suitable lemmas.
|
||||
|
||||
#### Exercise `0∸n≡0` {#zero-monus}
|
||||
|
||||
Show
|
||||
|
||||
zero ∸ n ≡ zero
|
||||
|
||||
for all naturals `n`. Did your proof require induction?
|
||||
|
||||
#### Exercise `∸-|-assoc` {#monus-plus-assoc}
|
||||
|
||||
Show that monus associates with addition, that is,
|
||||
|
||||
m ∸ n ∸ p ≡ m ∸ (n + p)
|
||||
|
||||
for all naturals `m`, `n`, and `p`.
|
||||
|
||||
#### Exercise `Bin-laws` (stretch) {#Bin-laws}
|
||||
|
||||
Recall that
|
||||
Exercise [Bin][plfa.Naturals#Bin]
|
||||
defines a datatype `Bin` of bitstrings representing natural numbers
|
||||
and asks you to define functions
|
||||
|
||||
inc : Bin → Bin
|
||||
to : ℕ → Bin
|
||||
from : Bin → ℕ
|
||||
|
||||
Consider the following laws, where `n` ranges over naturals and `x`
|
||||
over bitstrings.
|
||||
|
||||
from (inc x) ≡ suc (from x)
|
||||
to (from n) ≡ n
|
||||
from (to x) ≡ x
|
||||
|
||||
For each law: if it holds, prove; if not, give a counterexample.
|
||||
|
||||
|
||||
## Relations
|
||||
|
||||
|
||||
#### Exercise `orderings` {#orderings}
|
||||
|
||||
Give an example of a preorder that is not a partial order.
|
||||
|
||||
Give an example of a partial order that is not a preorder.
|
||||
|
||||
|
||||
#### Exercise `≤-antisym-cases` {#leq-antisym-cases}
|
||||
|
||||
The above proof omits cases where one argument is `z≤n` and one
|
||||
argument is `s≤s`. Why is it ok to omit them?
|
||||
|
||||
|
||||
#### Exercise `*-mono-≤` (stretch)
|
||||
|
||||
Show that multiplication is monotonic with regard to inequality.
|
||||
|
||||
|
||||
#### Exercise `<-trans` (recommended) {#less-trans}
|
||||
|
||||
Show that strict inequality is transitive.
|
||||
|
||||
#### Exercise `trichotomy` {#trichotomy}
|
||||
|
||||
Show that strict inequality satisfies a weak version of trichotomy, in
|
||||
the sense that for any `m` and `n` that one of the following holds:
|
||||
* `m < n`,
|
||||
* `m ≡ n`, or
|
||||
* `m > n`
|
||||
Define `m > n` to be the same as `n < m`.
|
||||
You will need a suitable data declaration,
|
||||
similar to that used for totality.
|
||||
(We will show that the three cases are exclusive after we introduce
|
||||
[negation][plfa.Negation].)
|
||||
|
||||
#### Exercise `+-mono-<` {#plus-mono-less}
|
||||
|
||||
Show that addition is monotonic with respect to strict inequality.
|
||||
As with inequality, some additional definitions may be required.
|
||||
|
||||
#### Exercise `≤-iff-<` (recommended) {#leq-iff-less}
|
||||
|
||||
Show that `suc m ≤ n` implies `m < n`, and conversely.
|
||||
|
||||
#### Exercise `<-trans-revisited` {#less-trans-revisited}
|
||||
|
||||
Give an alternative proof that strict inequality is transitive,
|
||||
using the relating between strict inequality and inequality and
|
||||
the fact that inequality is transitive.
|
||||
|
||||
#### Exercise `o+o≡e` (stretch) {#odd-plus-odd}
|
||||
|
||||
Show that the sum of two odd numbers is even.
|
||||
|
||||
#### Exercise `Bin-predicates` (stretch) {#Bin-predicates}
|
||||
|
||||
Recall that
|
||||
Exercise [Bin][plfa.Naturals#Bin]
|
||||
defines a datatype `Bin` of bitstrings representing natural numbers.
|
||||
Representations are not unique due to leading zeros.
|
||||
Hence, eleven may be represented by both of the following
|
||||
|
||||
x1 x1 x0 x1 nil
|
||||
x1 x1 x0 x1 x0 x0 nil
|
||||
|
||||
Define a predicate
|
||||
|
||||
Can : Bin → Set
|
||||
|
||||
over all bitstrings that holds if the bitstring is canonical, meaning
|
||||
it has no leading zeros; the first representation of eleven above is
|
||||
canonical, and the second is not. To define it, you will need an
|
||||
auxiliary predicate
|
||||
|
||||
One : Bin → Set
|
||||
|
||||
that holds only if the bistring has a leading one. A bitstring is
|
||||
canonical if it has a leading one (representing a positive number) or
|
||||
if it consists of a single zero (representing zero).
|
||||
|
||||
Show that increment preserves canonical bitstrings.
|
||||
|
||||
Can x
|
||||
------------
|
||||
Can (inc x)
|
||||
|
||||
Show that converting a natural to a bitstring always yields a
|
||||
canonical bitstring.
|
||||
|
||||
----------
|
||||
Can (to n)
|
||||
|
||||
Show that converting a canonical bitstring to a natural
|
||||
and back is the identity.
|
||||
|
||||
Can x
|
||||
---------------
|
||||
to (from x) ≡ x
|
||||
|
||||
(Hint: For each of these, you may first need to prove related
|
||||
properties of `One`.)
|
||||
|
|
@ -1,556 +0,0 @@
|
|||
---
|
||||
title : "Assignment2: PUC Assignment 2"
|
||||
layout : page
|
||||
permalink : /PUC/2019/Assignment2/
|
||||
---
|
||||
|
||||
```
|
||||
module Assignment2 where
|
||||
```
|
||||
|
||||
## YOUR NAME AND EMAIL GOES HERE
|
||||
|
||||
## Introduction
|
||||
|
||||
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.
|
||||
|
||||
Please ensure your files execute correctly under Agda!
|
||||
|
||||
## Imports
|
||||
|
||||
```
|
||||
import Relation.Binary.PropositionalEquality as Eq
|
||||
open Eq using (_≡_; refl; cong; sym)
|
||||
open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; _≡⟨_⟩_; _∎)
|
||||
open import Data.Nat using (ℕ; zero; suc; _+_; _*_; _∸_; _≤_; z≤n; s≤s)
|
||||
open import Data.Nat.Properties using (+-assoc; +-identityʳ; +-suc; +-comm;
|
||||
≤-refl; ≤-trans; ≤-antisym; ≤-total; +-monoʳ-≤; +-monoˡ-≤; +-mono-≤)
|
||||
open import Data.Product using (_×_; proj₁; proj₂) renaming (_,_ to ⟨_,_⟩)
|
||||
open import Data.Product using (Σ; ∃; Σ-syntax; ∃-syntax)
|
||||
open import Data.Unit using (⊤; tt)
|
||||
open import Data.Sum using (_⊎_; inj₁; inj₂) renaming ([_,_] to case-⊎)
|
||||
open import Data.Empty using (⊥; ⊥-elim)
|
||||
open import Data.Bool.Base using (Bool; true; false; T; _∧_; _∨_; not)
|
||||
open import Relation.Nullary using (¬_; Dec; yes; no)
|
||||
open import Relation.Nullary.Decidable using (⌊_⌋; toWitness; fromWitness)
|
||||
open import Relation.Nullary.Negation using (¬?)
|
||||
open import Relation.Nullary.Product using (_×-dec_)
|
||||
open import Relation.Nullary.Sum using (_⊎-dec_)
|
||||
open import Relation.Nullary.Negation using (contraposition)
|
||||
open import Relation.Unary using (Decidable)
|
||||
open import Function using (_∘_)
|
||||
open import Level using (Level)
|
||||
open import plfa.part1.Relations using (_<_; z<s; s<s)
|
||||
open import plfa.part1.Isomorphism using (_≃_; ≃-sym; ≃-trans; _≲_; extensionality)
|
||||
open plfa.part1.Isomorphism.≃-Reasoning
|
||||
open import plfa.part1.Lists using (List; []; _∷_; [_]; [_,_]; [_,_,_]; [_,_,_,_];
|
||||
_++_; reverse; map; foldr; sum; All; Any; here; there; _∈_)
|
||||
```
|
||||
|
||||
## Equality
|
||||
|
||||
#### Exercise `≤-reasoning` (stretch)
|
||||
|
||||
The proof of monotonicity from
|
||||
Chapter [Relations][plfa.Relations]
|
||||
can be written in a more readable form by using an analogue of our
|
||||
notation for `≡-reasoning`. Define `≤-reasoning` analogously, and use
|
||||
it to write out an alternative proof that addition is monotonic with
|
||||
regard to inequality. Rewrite both `+-monoˡ-≤` and `+-mono-≤`.
|
||||
|
||||
|
||||
|
||||
## Isomorphism
|
||||
|
||||
#### Exercise `≃-implies-≲`
|
||||
|
||||
Show that every isomorphism implies an embedding.
|
||||
```
|
||||
postulate
|
||||
≃-implies-≲ : ∀ {A B : Set}
|
||||
→ A ≃ B
|
||||
-----
|
||||
→ A ≲ B
|
||||
```
|
||||
|
||||
#### Exercise `_⇔_` (recommended) {#iff}
|
||||
|
||||
Define equivalence of propositions (also known as "if and only if") as follows.
|
||||
```
|
||||
record _⇔_ (A B : Set) : Set where
|
||||
field
|
||||
to : A → B
|
||||
from : B → A
|
||||
|
||||
open _⇔_
|
||||
```
|
||||
Show that equivalence is reflexive, symmetric, and transitive.
|
||||
|
||||
#### Exercise `Bin-embedding` (stretch) {#Bin-embedding}
|
||||
|
||||
Recall that Exercises
|
||||
[Bin][plfa.Naturals#Bin] and
|
||||
[Bin-laws][plfa.Induction#Bin-laws]
|
||||
define a datatype of bitstrings representing natural numbers.
|
||||
```
|
||||
data Bin : Set where
|
||||
nil : Bin
|
||||
x0_ : Bin → Bin
|
||||
x1_ : Bin → Bin
|
||||
```
|
||||
And ask you to define the following functions:
|
||||
|
||||
to : ℕ → Bin
|
||||
from : Bin → ℕ
|
||||
|
||||
which satisfy the following property:
|
||||
|
||||
from (to n) ≡ n
|
||||
|
||||
Using the above, establish that there is an embedding of `ℕ` into `Bin`.
|
||||
Why is there not an isomorphism?
|
||||
|
||||
|
||||
## Connectives
|
||||
|
||||
#### Exercise `⇔≃×` (recommended)
|
||||
|
||||
Show that `A ⇔ B` as defined [earlier][plfa.Isomorphism#iff]
|
||||
is isomorphic to `(A → B) × (B → A)`.
|
||||
|
||||
#### Exercise `⊎-comm` (recommended)
|
||||
|
||||
Show sum is commutative up to isomorphism.
|
||||
|
||||
#### Exercise `⊎-assoc`
|
||||
|
||||
Show sum is associative up to isomorphism.
|
||||
|
||||
#### Exercise `⊥-identityˡ` (recommended)
|
||||
|
||||
Show zero is the left identity of addition.
|
||||
|
||||
#### Exercise `⊥-identityʳ`
|
||||
|
||||
Show zero is the right identity of addition.
|
||||
|
||||
#### Exercise `⊎-weak-×` (recommended)
|
||||
|
||||
Show that the following property holds.
|
||||
```
|
||||
postulate
|
||||
⊎-weak-× : ∀ {A B C : Set} → (A ⊎ B) × C → A ⊎ (B × C)
|
||||
```
|
||||
This is called a _weak distributive law_. Give the corresponding
|
||||
distributive law, and explain how it relates to the weak version.
|
||||
|
||||
#### Exercise `⊎×-implies-×⊎`
|
||||
|
||||
Show that a disjunct of conjuncts implies a conjunct of disjuncts.
|
||||
```
|
||||
postulate
|
||||
⊎×-implies-×⊎ : ∀ {A B C D : Set} → (A × B) ⊎ (C × D) → (A ⊎ C) × (B ⊎ D)
|
||||
```
|
||||
Does the converse hold? If so, prove; if not, give a counterexample.
|
||||
|
||||
|
||||
## Negation
|
||||
|
||||
#### Exercise `<-irreflexive` (recommended)
|
||||
|
||||
Using negation, show that
|
||||
[strict inequality][plfa.Relations#strict-inequality]
|
||||
is irreflexive, that is, `n < n` holds for no `n`.
|
||||
|
||||
|
||||
#### Exercise `trichotomy`
|
||||
|
||||
Show that strict inequality satisfies
|
||||
[trichotomy][plfa.Relations#trichotomy],
|
||||
that is, for any naturals `m` and `n` exactly one of the following holds:
|
||||
|
||||
* `m < n`
|
||||
* `m ≡ n`
|
||||
* `m > n`
|
||||
|
||||
Here "exactly one" means that one of the three must hold, and each implies the
|
||||
negation of the other two.
|
||||
|
||||
|
||||
#### Exercise `⊎-dual-×` (recommended)
|
||||
|
||||
Show that conjunction, disjunction, and negation are related by a
|
||||
version of De Morgan's Law.
|
||||
|
||||
¬ (A ⊎ B) ≃ (¬ A) × (¬ B)
|
||||
|
||||
This result is an easy consequence of something we've proved previously.
|
||||
|
||||
Do we also have the following?
|
||||
|
||||
¬ (A × B) ≃ (¬ A) ⊎ (¬ B)
|
||||
|
||||
If so, prove; if not, give a variant that does hold.
|
||||
|
||||
|
||||
#### Exercise `Classical` (stretch)
|
||||
|
||||
Consider the following principles.
|
||||
|
||||
* Excluded Middle: `A ⊎ ¬ A`, for all `A`
|
||||
* Double Negation Elimination: `¬ ¬ A → A`, for all `A`
|
||||
* Peirce's Law: `((A → B) → A) → A`, for all `A` and `B`.
|
||||
* Implication as disjunction: `(A → B) → ¬ A ⊎ B`, for all `A` and `B`.
|
||||
* De Morgan: `¬ (¬ A × ¬ B) → A ⊎ B`, for all `A` and `B`.
|
||||
|
||||
Show that each of these implies all the others.
|
||||
|
||||
|
||||
#### Exercise `Stable` (stretch)
|
||||
|
||||
Say that a formula is _stable_ if double negation elimination holds for it.
|
||||
```
|
||||
Stable : Set → Set
|
||||
Stable A = ¬ ¬ A → A
|
||||
```
|
||||
Show that any negated formula is stable, and that the conjunction
|
||||
of two stable formulas is stable.
|
||||
|
||||
|
||||
## Quantifiers
|
||||
|
||||
#### Exercise `∀-distrib-×` (recommended)
|
||||
|
||||
Show that universals distribute over conjunction.
|
||||
```
|
||||
postulate
|
||||
∀-distrib-× : ∀ {A : Set} {B C : A → Set} →
|
||||
(∀ (x : A) → B x × C x) ≃ (∀ (x : A) → B x) × (∀ (x : A) → C x)
|
||||
```
|
||||
Compare this with the result (`→-distrib-×`) in
|
||||
Chapter [Connectives][plfa.Connectives].
|
||||
|
||||
#### Exercise `⊎∀-implies-∀⊎`
|
||||
|
||||
Show that a disjunction of universals implies a universal of disjunctions.
|
||||
```
|
||||
postulate
|
||||
⊎∀-implies-∀⊎ : ∀ {A : Set} { B C : A → Set } →
|
||||
(∀ (x : A) → B x) ⊎ (∀ (x : A) → C x) → ∀ (x : A) → B x ⊎ C x
|
||||
```
|
||||
Does the converse hold? If so, prove; if not, explain why.
|
||||
|
||||
#### Exercise `∃-distrib-⊎` (recommended)
|
||||
|
||||
Show that existentials distribute over disjunction.
|
||||
```
|
||||
postulate
|
||||
∃-distrib-⊎ : ∀ {A : Set} {B C : A → Set} →
|
||||
∃[ x ] (B x ⊎ C x) ≃ (∃[ x ] B x) ⊎ (∃[ x ] C x)
|
||||
```
|
||||
|
||||
#### Exercise `∃×-implies-×∃`
|
||||
|
||||
Show that an existential of conjunctions implies a conjunction of existentials.
|
||||
```
|
||||
postulate
|
||||
∃×-implies-×∃ : ∀ {A : Set} { B C : A → Set } →
|
||||
∃[ x ] (B x × C x) → (∃[ x ] B x) × (∃[ x ] C x)
|
||||
```
|
||||
Does the converse hold? If so, prove; if not, explain why.
|
||||
|
||||
#### Exercise `∃-even-odd`
|
||||
|
||||
How do the proofs become more difficult if we replace `m * 2` and `1 + m * 2`
|
||||
by `2 * m` and `2 * m + 1`? Rewrite the proofs of `∃-even` and `∃-odd` when
|
||||
restated in this way.
|
||||
|
||||
#### Exercise `∃-|-≤`
|
||||
|
||||
Show that `y ≤ z` holds if and only if there exists a `x` such that
|
||||
`x + y ≡ z`.
|
||||
|
||||
#### Exercise `∃¬-implies-¬∀` (recommended)
|
||||
|
||||
Show that existential of a negation implies negation of a universal.
|
||||
```
|
||||
postulate
|
||||
∃¬-implies-¬∀ : ∀ {A : Set} {B : A → Set}
|
||||
→ ∃[ x ] (¬ B x)
|
||||
--------------
|
||||
→ ¬ (∀ x → B x)
|
||||
```
|
||||
Does the converse hold? If so, prove; if not, explain why.
|
||||
|
||||
|
||||
#### Exercise `Bin-isomorphism` (stretch) {#Bin-isomorphism}
|
||||
|
||||
Recall that Exercises
|
||||
[Bin][plfa.Naturals#Bin],
|
||||
[Bin-laws][plfa.Induction#Bin-laws], and
|
||||
[Bin-predicates][plfa.Relations#Bin-predicates]
|
||||
define a datatype of bitstrings representing natural numbers.
|
||||
|
||||
data Bin : Set where
|
||||
nil : Bin
|
||||
x0_ : Bin → Bin
|
||||
x1_ : Bin → Bin
|
||||
|
||||
And ask you to define the following functions and predicates.
|
||||
|
||||
to : ℕ → Bin
|
||||
from : Bin → ℕ
|
||||
Can : Bin → Set
|
||||
|
||||
And to establish the following properties.
|
||||
|
||||
from (to n) ≡ n
|
||||
|
||||
----------
|
||||
Can (to n)
|
||||
|
||||
Can x
|
||||
---------------
|
||||
to (from x) ≡ x
|
||||
|
||||
Using the above, establish that there is an isomorphism between `ℕ` and
|
||||
`∃[ x ](Can x)`.
|
||||
|
||||
|
||||
## Decidable
|
||||
|
||||
#### Exercise `_<?_` (recommended)
|
||||
|
||||
Analogous to the function above, define a function to decide strict inequality.
|
||||
```
|
||||
postulate
|
||||
_<?_ : ∀ (m n : ℕ) → Dec (m < n)
|
||||
```
|
||||
|
||||
#### Exercise `_≡ℕ?_`
|
||||
|
||||
Define a function to decide whether two naturals are equal.
|
||||
```
|
||||
postulate
|
||||
_≡ℕ?_ : ∀ (m n : ℕ) → Dec (m ≡ n)
|
||||
```
|
||||
|
||||
|
||||
#### Exercise `erasure`
|
||||
|
||||
Show that erasure relates corresponding boolean and decidable operations.
|
||||
```
|
||||
postulate
|
||||
∧-× : ∀ {A B : Set} (x : Dec A) (y : Dec B) → ⌊ x ⌋ ∧ ⌊ y ⌋ ≡ ⌊ x ×-dec y ⌋
|
||||
∨-× : ∀ {A B : Set} (x : Dec A) (y : Dec B) → ⌊ x ⌋ ∨ ⌊ y ⌋ ≡ ⌊ x ⊎-dec y ⌋
|
||||
not-¬ : ∀ {A : Set} (x : Dec A) → not ⌊ x ⌋ ≡ ⌊ ¬? x ⌋
|
||||
```
|
||||
|
||||
#### Exercise `iff-erasure` (recommended)
|
||||
|
||||
Give analogues of the `_⇔_` operation from
|
||||
Chapter [Isomorphism][plfa.Isomorphism#iff],
|
||||
operation on booleans and decidables, and also show the corresponding erasure.
|
||||
```
|
||||
postulate
|
||||
_iff_ : Bool → Bool → Bool
|
||||
_⇔-dec_ : ∀ {A B : Set} → Dec A → Dec B → Dec (A ⇔ B)
|
||||
iff-⇔ : ∀ {A B : Set} (x : Dec A) (y : Dec B) → ⌊ x ⌋ iff ⌊ y ⌋ ≡ ⌊ x ⇔-dec y ⌋
|
||||
```
|
||||
|
||||
## Lists
|
||||
|
||||
#### Exercise `reverse-++-commute` (recommended)
|
||||
|
||||
Show that the reverse of one list appended to another is the
|
||||
reverse of the second appended to the reverse of the first.
|
||||
```
|
||||
postulate
|
||||
reverse-++-commute : ∀ {A : Set} {xs ys : List A}
|
||||
→ reverse (xs ++ ys) ≡ reverse ys ++ reverse xs
|
||||
```
|
||||
|
||||
#### Exercise `reverse-involutive` (recommended)
|
||||
|
||||
A function is an _involution_ if when applied twice it acts
|
||||
as the identity function. Show that reverse is an involution.
|
||||
```
|
||||
postulate
|
||||
reverse-involutive : ∀ {A : Set} {xs : List A}
|
||||
→ reverse (reverse xs) ≡ xs
|
||||
```
|
||||
|
||||
#### Exercise `map-compose`
|
||||
|
||||
Prove that the map of a composition is equal to the composition of two maps.
|
||||
```
|
||||
postulate
|
||||
map-compose : ∀ {A B C : Set} {f : A → B} {g : B → C}
|
||||
→ map (g ∘ f) ≡ map g ∘ map f
|
||||
```
|
||||
The last step of the proof requires extensionality.
|
||||
|
||||
#### Exercise `map-++-commute`
|
||||
|
||||
Prove the following relationship between map and append.
|
||||
```
|
||||
postulate
|
||||
map-++-commute : ∀ {A B : Set} {f : A → B} {xs ys : List A}
|
||||
→ map f (xs ++ ys) ≡ map f xs ++ map f ys
|
||||
```
|
||||
|
||||
#### Exercise `map-Tree`
|
||||
|
||||
Define a type of trees with leaves of type `A` and internal
|
||||
nodes of type `B`.
|
||||
```
|
||||
data Tree (A B : Set) : Set where
|
||||
leaf : A → Tree A B
|
||||
node : Tree A B → B → Tree A B → Tree A B
|
||||
```
|
||||
Define a suitable map operator over trees.
|
||||
```
|
||||
postulate
|
||||
map-Tree : ∀ {A B C D : Set}
|
||||
→ (A → C) → (B → D) → Tree A B → Tree C D
|
||||
```
|
||||
|
||||
#### Exercise `product` (recommended)
|
||||
|
||||
Use fold to define a function to find the product of a list of numbers.
|
||||
For example,
|
||||
|
||||
product [ 1 , 2 , 3 , 4 ] ≡ 24
|
||||
|
||||
#### Exercise `foldr-++` (recommended)
|
||||
|
||||
Show that fold and append are related as follows.
|
||||
```
|
||||
postulate
|
||||
foldr-++ : ∀ {A B : Set} (_⊗_ : A → B → B) (e : B) (xs ys : List A) →
|
||||
foldr _⊗_ e (xs ++ ys) ≡ foldr _⊗_ (foldr _⊗_ e ys) xs
|
||||
```
|
||||
|
||||
|
||||
#### Exercise `map-is-foldr`
|
||||
|
||||
Show that map can be defined using fold.
|
||||
```
|
||||
postulate
|
||||
map-is-foldr : ∀ {A B : Set} {f : A → B} →
|
||||
map f ≡ foldr (λ x xs → f x ∷ xs) []
|
||||
```
|
||||
This requires extensionality.
|
||||
|
||||
#### Exercise `fold-Tree`
|
||||
|
||||
Define a suitable fold function for the type of trees given earlier.
|
||||
```
|
||||
postulate
|
||||
fold-Tree : ∀ {A B C : Set}
|
||||
→ (A → C) → (C → B → C → C) → Tree A B → C
|
||||
```
|
||||
|
||||
#### Exercise `map-is-fold-Tree`
|
||||
|
||||
Demonstrate an analogue of `map-is-foldr` for the type of trees.
|
||||
|
||||
#### Exercise `sum-downFrom` (stretch)
|
||||
|
||||
Define a function that counts down as follows.
|
||||
```
|
||||
downFrom : ℕ → List ℕ
|
||||
downFrom zero = []
|
||||
downFrom (suc n) = n ∷ downFrom n
|
||||
```
|
||||
For example,
|
||||
```
|
||||
_ : downFrom 3 ≡ [ 2 , 1 , 0 ]
|
||||
_ = refl
|
||||
```
|
||||
Prove that the sum of the numbers `(n - 1) + ⋯ + 0` is
|
||||
equal to `n * (n ∸ 1) / 2`.
|
||||
```
|
||||
postulate
|
||||
sum-downFrom : ∀ (n : ℕ)
|
||||
→ sum (downFrom n) * 2 ≡ n * (n ∸ 1)
|
||||
```
|
||||
|
||||
|
||||
#### Exercise `foldl`
|
||||
|
||||
Define a function `foldl` which is analogous to `foldr`, but where
|
||||
operations associate to the left rather than the right. For example,
|
||||
|
||||
foldr _⊗_ e [ x , y , z ] = x ⊗ (y ⊗ (z ⊗ e))
|
||||
foldl _⊗_ e [ x , y , z ] = ((e ⊗ x) ⊗ y) ⊗ z
|
||||
|
||||
|
||||
#### Exercise `foldr-monoid-foldl`
|
||||
|
||||
Show that if `_⊕_` and `e` form a monoid, then `foldr _⊗_ e` and
|
||||
`foldl _⊗_ e` always compute the same result.
|
||||
|
||||
|
||||
#### Exercise `Any-++-⇔` (recommended)
|
||||
|
||||
Prove a result similar to `All-++-⇔`, but with `Any` in place of `All`, and a suitable
|
||||
replacement for `_×_`. As a consequence, demonstrate an equivalence relating
|
||||
`_∈_` and `_++_`.
|
||||
|
||||
|
||||
#### Exercise `All-++-≃` (stretch)
|
||||
|
||||
Show that the equivalence `All-++-⇔` can be extended to an isomorphism.
|
||||
|
||||
|
||||
#### Exercise `¬Any≃All¬` (stretch)
|
||||
|
||||
First generalise composition to arbitrary levels, using
|
||||
[universe polymorphism][plfa.Equality#unipoly].
|
||||
```
|
||||
_∘′_ : ∀ {ℓ₁ ℓ₂ ℓ₃ : Level} {A : Set ℓ₁} {B : Set ℓ₂} {C : Set ℓ₃}
|
||||
→ (B → C) → (A → B) → A → C
|
||||
(g ∘′ f) x = g (f x)
|
||||
```
|
||||
|
||||
Show that `Any` and `All` satisfy a version of De Morgan's Law.
|
||||
```
|
||||
postulate
|
||||
¬Any≃All¬ : ∀ {A : Set} (P : A → Set) (xs : List A)
|
||||
→ (¬_ ∘′ Any P) xs ≃ All (¬_ ∘′ P) xs
|
||||
```
|
||||
|
||||
Do we also have the following?
|
||||
```
|
||||
postulate
|
||||
¬All≃Any¬ : ∀ {A : Set} (P : A → Set) (xs : List A)
|
||||
→ (¬_ ∘′ All P) xs ≃ Any (¬_ ∘′ P) xs
|
||||
```
|
||||
If so, prove; if not, explain why.
|
||||
|
||||
|
||||
#### Exercise `any?` (stretch)
|
||||
|
||||
Just as `All` has analogues `all` and `all?` which determine whether a
|
||||
predicate holds for every element of a list, so does `Any` have
|
||||
analogues `any` and `any?` which determine whether a predicates holds
|
||||
for some element of a list. Give their definitions.
|
||||
|
||||
|
||||
#### Exercise `filter?` (stretch)
|
||||
|
||||
Define the following variant of the traditional `filter` function on lists,
|
||||
which given a list and a decidable predicate returns all elements of the
|
||||
list satisfying the predicate.
|
||||
```
|
||||
postulate
|
||||
filter? : ∀ {A : Set} {P : A → Set}
|
||||
→ (P? : Decidable P) → List A → ∃[ ys ]( All P ys )
|
||||
```
|
||||
|
|
@ -1,181 +0,0 @@
|
|||
---
|
||||
title : "Assignment3: PUC Assignment 3"
|
||||
layout : page
|
||||
permalink : /PUC/2019/Assignment3/
|
||||
---
|
||||
|
||||
```
|
||||
module Assignment3 where
|
||||
```
|
||||
|
||||
## YOUR NAME AND EMAIL GOES HERE
|
||||
|
||||
## Introduction
|
||||
|
||||
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.
|
||||
|
||||
Please ensure your files execute correctly under Agda!
|
||||
|
||||
## Imports
|
||||
|
||||
```
|
||||
import Relation.Binary.PropositionalEquality as Eq
|
||||
open Eq using (_≡_; refl; cong; sym)
|
||||
open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; _≡⟨_⟩_; _∎)
|
||||
open import Data.Bool.Base using (Bool; true; false; T; _∧_; _∨_; not)
|
||||
open import Data.Nat using (ℕ; zero; suc; _+_; _*_; _∸_; _≤_; s≤s; z≤n)
|
||||
open import Data.Nat.Properties using
|
||||
(+-assoc; +-identityˡ; +-identityʳ; *-assoc; *-identityˡ; *-identityʳ)
|
||||
open import Relation.Nullary using (¬_; Dec; yes; no)
|
||||
open import Data.Product using (_×_; ∃; ∃-syntax) renaming (_,_ to ⟨_,_⟩)
|
||||
open import Data.Empty using (⊥; ⊥-elim)
|
||||
open import Function using (_∘_)
|
||||
open import Algebra.Structures using (IsMonoid)
|
||||
open import Level using (Level)
|
||||
open import Relation.Unary using (Decidable)
|
||||
open import plfa.part1.Relations using (_<_; z<s; s<s)
|
||||
open import plfa.part1.Isomorphism using (_≃_; ≃-sym; ≃-trans; _≲_; extensionality)
|
||||
open plfa.part1.Isomorphism.≃-Reasoning
|
||||
open import plfa.part1.Lists using (List; []; _∷_; [_]; [_,_]; [_,_,_]; [_,_,_,_];
|
||||
_++_; reverse; map; foldr; sum; All; Any; here; there; _∈_)
|
||||
open import plfa.part2.Lambda hiding (ƛ′_⇒_; case′_[zero⇒_|suc_⇒_]; μ′_⇒_; plus′)
|
||||
open import plfa.part2.Properties hiding (value?; unstuck; preserves; wttdgs)
|
||||
```
|
||||
|
||||
## Lambda
|
||||
|
||||
#### Exercise `mul` (recommended)
|
||||
|
||||
Write out the definition of a lambda term that multiplies
|
||||
two natural numbers.
|
||||
|
||||
|
||||
#### Exercise `primed` (stretch)
|
||||
|
||||
We can make examples with lambda terms slightly easier to write
|
||||
by adding the following definitions.
|
||||
```
|
||||
ƛ′_⇒_ : Term → Term → Term
|
||||
ƛ′ (` x) ⇒ N = ƛ x ⇒ N
|
||||
ƛ′ _ ⇒ _ = ⊥-elim impossible
|
||||
where postulate impossible : ⊥
|
||||
|
||||
case′_[zero⇒_|suc_⇒_] : Term → Term → Term → Term → Term
|
||||
case′ L [zero⇒ M |suc (` x) ⇒ N ] = case L [zero⇒ M |suc x ⇒ N ]
|
||||
case′ _ [zero⇒ _ |suc _ ⇒ _ ] = ⊥-elim impossible
|
||||
where postulate impossible : ⊥
|
||||
|
||||
μ′_⇒_ : Term → Term → Term
|
||||
μ′ (` x) ⇒ N = μ x ⇒ N
|
||||
μ′ _ ⇒ _ = ⊥-elim impossible
|
||||
where postulate impossible : ⊥
|
||||
```
|
||||
The definition of `plus` can now be written as follows.
|
||||
```
|
||||
plus′ : Term
|
||||
plus′ = μ′ + ⇒ ƛ′ m ⇒ ƛ′ n ⇒
|
||||
case′ m
|
||||
[zero⇒ n
|
||||
|suc m ⇒ `suc (+ · m · n) ]
|
||||
where
|
||||
+ = ` "+"
|
||||
m = ` "m"
|
||||
n = ` "n"
|
||||
```
|
||||
Write out the definition of multiplication in the same style.
|
||||
|
||||
#### Exercise `_[_:=_]′` (stretch)
|
||||
|
||||
The definition of substitution above has three clauses (`ƛ`, `case`,
|
||||
and `μ`) that invoke a with clause to deal with bound variables.
|
||||
Rewrite the definition to factor the common part of these three
|
||||
clauses into a single function, defined by mutual recursion with
|
||||
substitution.
|
||||
|
||||
|
||||
#### Exercise `—↠≲—↠′`
|
||||
|
||||
Show that the first notion of reflexive and transitive closure
|
||||
above embeds into the second. Why are they not isomorphic?
|
||||
|
||||
|
||||
#### Exercise `plus-example`
|
||||
|
||||
Write out the reduction sequence demonstrating that one plus one is two.
|
||||
|
||||
|
||||
#### Exercise `mul-type` (recommended)
|
||||
|
||||
Using the term `mul` you defined earlier, write out the derivation
|
||||
showing that it is well-typed.
|
||||
|
||||
|
||||
## Properties
|
||||
|
||||
|
||||
#### Exercise `Progress-≃`
|
||||
|
||||
Show that `Progress M` is isomorphic to `Value M ⊎ ∃[ N ](M —→ N)`.
|
||||
|
||||
|
||||
#### Exercise `progress′`
|
||||
|
||||
Write out the proof of `progress′` in full, and compare it to the
|
||||
proof of `progress` above.
|
||||
|
||||
|
||||
#### Exercise `value?`
|
||||
|
||||
Combine `progress` and `—→¬V` to write a program that decides
|
||||
whether a well-typed term is a value.
|
||||
```
|
||||
postulate
|
||||
value? : ∀ {A M} → ∅ ⊢ M ⦂ A → Dec (Value M)
|
||||
```
|
||||
|
||||
|
||||
#### Exercise `subst′` (stretch)
|
||||
|
||||
Rewrite `subst` to work with the modified definition `_[_:=_]′`
|
||||
from the exercise in the previous chapter. As before, this
|
||||
should factor dealing with bound variables into a single function,
|
||||
defined by mutual recursion with the proof that substitution
|
||||
preserves types.
|
||||
|
||||
|
||||
#### Exercise `mul-example` (recommended)
|
||||
|
||||
Using the evaluator, confirm that two times two is four.
|
||||
|
||||
|
||||
#### Exercise: `progress-preservation`
|
||||
|
||||
Without peeking at their statements above, write down the progress
|
||||
and preservation theorems for the simply typed lambda-calculus.
|
||||
|
||||
|
||||
#### Exercise `subject-expansion`
|
||||
|
||||
We say that `M` _reduces_ to `N` if `M —→ N`,
|
||||
and conversely that `M` _expands_ to `N` if `N —→ M`.
|
||||
The preservation property is sometimes called _subject reduction_.
|
||||
Its opposite is _subject expansion_, which holds if
|
||||
`M —→ N` and `∅ ⊢ N ⦂ A` imply `∅ ⊢ M ⦂ A`.
|
||||
Find two counter-examples to subject expansion, one
|
||||
with case expressions and one not involving case expressions.
|
||||
|
||||
|
||||
#### Exercise `stuck`
|
||||
|
||||
Give an example of an ill-typed term that does get stuck.
|
||||
|
||||
|
||||
#### Exercise `unstuck` (recommended)
|
||||
|
||||
Provide proofs of the three postulates, `unstuck`, `preserves`, and `wttdgs` above.
|
||||
|
|
@ -1,739 +0,0 @@
|
|||
---
|
||||
title : "Assignment4: PUC Assignment 4"
|
||||
layout : page
|
||||
permalink : /PUC/2019/Assignment4/
|
||||
---
|
||||
|
||||
```
|
||||
module Assignment4 where
|
||||
```
|
||||
|
||||
## YOUR NAME AND EMAIL GOES HERE
|
||||
|
||||
|
||||
## Introduction
|
||||
|
||||
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.
|
||||
|
||||
Please ensure your files execute correctly under Agda!
|
||||
|
||||
**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; cong₂; _≢_)
|
||||
open import Data.Empty using (⊥; ⊥-elim)
|
||||
open import Data.Nat using (ℕ; zero; suc; _+_; _*_)
|
||||
open import Data.Product using (_×_; ∃; ∃-syntax) renaming (_,_ to ⟨_,_⟩)
|
||||
open import Data.String using (String; _≟_)
|
||||
open import Relation.Nullary using (¬_; Dec; yes; no)
|
||||
```
|
||||
|
||||
|
||||
## DeBruijn
|
||||
|
||||
|
||||
```
|
||||
module DeBruijn where
|
||||
```
|
||||
|
||||
Remember to indent all code by two spaces.
|
||||
|
||||
```
|
||||
open import plfa.part2.DeBruijn
|
||||
```
|
||||
|
||||
|
||||
#### Exercise (`mul`) (recommended)
|
||||
|
||||
Write out the definition of a lambda term that multiplies
|
||||
two natural numbers, now adapted to the inherently typed
|
||||
DeBruijn representation.
|
||||
|
||||
|
||||
#### Exercise `V¬—→`
|
||||
|
||||
Following the previous development, show values do
|
||||
not reduce, and its corollary, terms that reduce are not
|
||||
values.
|
||||
|
||||
|
||||
#### Exercise `mul-example` (recommended)
|
||||
|
||||
Using the evaluator, confirm that two times two is four.
|
||||
|
||||
|
||||
## More
|
||||
|
||||
```
|
||||
module More where
|
||||
```
|
||||
|
||||
Remember to indent all code by two spaces.
|
||||
|
||||
|
||||
### Syntax
|
||||
|
||||
```
|
||||
infix 4 _⊢_
|
||||
infix 4 _∋_
|
||||
infixl 5 _,_
|
||||
|
||||
infixr 7 _⇒_
|
||||
infixr 8 _`⊎_
|
||||
infixr 9 _`×_
|
||||
|
||||
infix 5 ƛ_
|
||||
infix 5 μ_
|
||||
infixl 7 _·_
|
||||
infixl 8 _`*_
|
||||
infix 8 `suc_
|
||||
infix 9 `_
|
||||
infix 9 S_
|
||||
infix 9 #_
|
||||
```
|
||||
|
||||
### Types
|
||||
|
||||
```
|
||||
data Type : Set where
|
||||
`ℕ : Type
|
||||
_⇒_ : Type → Type → Type
|
||||
Nat : Type
|
||||
_`×_ : Type → Type → Type
|
||||
_`⊎_ : Type → Type → Type
|
||||
`⊤ : Type
|
||||
`⊥ : Type
|
||||
`List : Type → Type
|
||||
```
|
||||
|
||||
### Contexts
|
||||
|
||||
```
|
||||
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}
|
||||
→ Γ ∋ B
|
||||
---------
|
||||
→ Γ , A ∋ B
|
||||
```
|
||||
|
||||
### Terms and the typing judgment
|
||||
|
||||
```
|
||||
data _⊢_ : Context → Type → Set where
|
||||
|
||||
-- variables
|
||||
|
||||
`_ : ∀ {Γ A}
|
||||
→ Γ ∋ A
|
||||
-----
|
||||
→ Γ ⊢ A
|
||||
|
||||
-- functions
|
||||
|
||||
ƛ_ : ∀ {Γ A B}
|
||||
→ Γ , A ⊢ B
|
||||
---------
|
||||
→ Γ ⊢ A ⇒ B
|
||||
|
||||
_·_ : ∀ {Γ A B}
|
||||
→ Γ ⊢ A ⇒ B
|
||||
→ Γ ⊢ A
|
||||
---------
|
||||
→ Γ ⊢ B
|
||||
|
||||
-- naturals
|
||||
|
||||
`zero : ∀ {Γ}
|
||||
------
|
||||
→ Γ ⊢ `ℕ
|
||||
|
||||
`suc_ : ∀ {Γ}
|
||||
→ Γ ⊢ `ℕ
|
||||
------
|
||||
→ Γ ⊢ `ℕ
|
||||
|
||||
case : ∀ {Γ A}
|
||||
→ Γ ⊢ `ℕ
|
||||
→ Γ ⊢ A
|
||||
→ Γ , `ℕ ⊢ A
|
||||
-----
|
||||
→ Γ ⊢ A
|
||||
|
||||
-- fixpoint
|
||||
|
||||
μ_ : ∀ {Γ A}
|
||||
→ Γ , A ⊢ A
|
||||
----------
|
||||
→ Γ ⊢ A
|
||||
|
||||
-- primitive numbers
|
||||
|
||||
con : ∀ {Γ}
|
||||
→ ℕ
|
||||
-------
|
||||
→ Γ ⊢ Nat
|
||||
|
||||
_`*_ : ∀ {Γ}
|
||||
→ Γ ⊢ Nat
|
||||
→ Γ ⊢ Nat
|
||||
-------
|
||||
→ Γ ⊢ Nat
|
||||
|
||||
-- let
|
||||
|
||||
`let : ∀ {Γ A B}
|
||||
→ Γ ⊢ A
|
||||
→ Γ , A ⊢ B
|
||||
----------
|
||||
→ Γ ⊢ B
|
||||
|
||||
-- products
|
||||
|
||||
`⟨_,_⟩ : ∀ {Γ A B}
|
||||
→ Γ ⊢ A
|
||||
→ Γ ⊢ B
|
||||
-----------
|
||||
→ Γ ⊢ A `× B
|
||||
|
||||
`proj₁ : ∀ {Γ A B}
|
||||
→ Γ ⊢ A `× B
|
||||
-----------
|
||||
→ Γ ⊢ A
|
||||
|
||||
`proj₂ : ∀ {Γ A B}
|
||||
→ Γ ⊢ A `× B
|
||||
-----------
|
||||
→ Γ ⊢ B
|
||||
|
||||
-- alternative formulation of products
|
||||
|
||||
case× : ∀ {Γ A B C}
|
||||
→ Γ ⊢ A `× B
|
||||
→ Γ , A , B ⊢ C
|
||||
--------------
|
||||
→ Γ ⊢ C
|
||||
|
||||
```
|
||||
|
||||
### 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} → Γ , A ∋ B → Δ , A ∋ B)
|
||||
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)
|
||||
rename ρ (con n) = con n
|
||||
rename ρ (M `* N) = rename ρ M `* rename ρ N
|
||||
rename ρ (`let M N) = `let (rename ρ M) (rename (ext ρ) N)
|
||||
rename ρ `⟨ M , N ⟩ = `⟨ rename ρ M , rename ρ N ⟩
|
||||
rename ρ (`proj₁ L) = `proj₁ (rename ρ L)
|
||||
rename ρ (`proj₂ L) = `proj₂ (rename ρ L)
|
||||
rename ρ (case× L M) = case× (rename ρ L) (rename (ext (ext ρ)) M)
|
||||
```
|
||||
|
||||
## Simultaneous Substitution
|
||||
|
||||
```
|
||||
exts : ∀ {Γ Δ} → (∀ {A} → Γ ∋ A → Δ ⊢ A) → (∀ {A B} → Γ , A ∋ B → Δ , A ⊢ B)
|
||||
exts σ Z = ` Z
|
||||
exts σ (S x) = rename S_ (σ x)
|
||||
|
||||
subst : ∀ {Γ Δ} → (∀ {C} → Γ ∋ C → Δ ⊢ C) → (∀ {C} → Γ ⊢ C → Δ ⊢ C)
|
||||
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)
|
||||
subst σ (con n) = con n
|
||||
subst σ (M `* N) = subst σ M `* subst σ N
|
||||
subst σ (`let M N) = `let (subst σ M) (subst (exts σ) N)
|
||||
subst σ `⟨ M , N ⟩ = `⟨ subst σ M , subst σ N ⟩
|
||||
subst σ (`proj₁ L) = `proj₁ (subst σ L)
|
||||
subst σ (`proj₂ L) = `proj₂ (subst σ L)
|
||||
subst σ (case× L M) = case× (subst σ L) (subst (exts (exts σ)) M)
|
||||
```
|
||||
|
||||
## Single and double substitution
|
||||
|
||||
```
|
||||
_[_] : ∀ {Γ A B}
|
||||
→ Γ , A ⊢ B
|
||||
→ Γ ⊢ A
|
||||
------------
|
||||
→ Γ ⊢ B
|
||||
_[_] {Γ} {A} N V = subst {Γ , A} {Γ} σ N
|
||||
where
|
||||
σ : ∀ {B} → Γ , A ∋ B → Γ ⊢ B
|
||||
σ Z = V
|
||||
σ (S x) = ` x
|
||||
|
||||
_[_][_] : ∀ {Γ A B C}
|
||||
→ Γ , A , B ⊢ C
|
||||
→ Γ ⊢ A
|
||||
→ Γ ⊢ B
|
||||
---------------
|
||||
→ Γ ⊢ C
|
||||
_[_][_] {Γ} {A} {B} N V W = subst {Γ , A , B} {Γ} σ N
|
||||
where
|
||||
σ : ∀ {C} → Γ , A , B ∋ C → Γ ⊢ C
|
||||
σ Z = W
|
||||
σ (S Z) = V
|
||||
σ (S (S x)) = ` x
|
||||
```
|
||||
|
||||
## Values
|
||||
|
||||
```
|
||||
data Value : ∀ {Γ A} → Γ ⊢ A → Set where
|
||||
|
||||
-- functions
|
||||
|
||||
V-ƛ : ∀ {Γ A B} {N : Γ , A ⊢ B}
|
||||
---------------------------
|
||||
→ Value (ƛ N)
|
||||
|
||||
-- naturals
|
||||
|
||||
V-zero : ∀ {Γ} →
|
||||
-----------------
|
||||
Value (`zero {Γ})
|
||||
|
||||
V-suc_ : ∀ {Γ} {V : Γ ⊢ `ℕ}
|
||||
→ Value V
|
||||
--------------
|
||||
→ Value (`suc V)
|
||||
|
||||
-- primitives
|
||||
|
||||
V-con : ∀ {Γ n}
|
||||
---------------------
|
||||
→ Value {Γ = Γ} (con n)
|
||||
|
||||
-- products
|
||||
|
||||
V-⟨_,_⟩ : ∀ {Γ A B} {V : Γ ⊢ A} {W : Γ ⊢ B}
|
||||
→ Value V
|
||||
→ Value W
|
||||
----------------
|
||||
→ Value `⟨ V , W ⟩
|
||||
```
|
||||
|
||||
Implicit arguments need to be supplied when they are
|
||||
not fixed by the given arguments.
|
||||
|
||||
## Reduction
|
||||
|
||||
```
|
||||
infix 2 _—→_
|
||||
|
||||
data _—→_ : ∀ {Γ A} → (Γ ⊢ A) → (Γ ⊢ A) → Set where
|
||||
|
||||
-- functions
|
||||
|
||||
ξ-·₁ : ∀ {Γ 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} {V : Γ ⊢ A}
|
||||
→ Value V
|
||||
--------------------
|
||||
→ (ƛ N) · V —→ N [ V ]
|
||||
|
||||
-- naturals
|
||||
|
||||
ξ-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 ]
|
||||
|
||||
-- fixpoint
|
||||
|
||||
β-μ : ∀ {Γ A} {N : Γ , A ⊢ A}
|
||||
----------------
|
||||
→ μ N —→ N [ μ N ]
|
||||
|
||||
-- primitive numbers
|
||||
|
||||
ξ-*₁ : ∀ {Γ} {L L′ M : Γ ⊢ Nat}
|
||||
→ L —→ L′
|
||||
-----------------
|
||||
→ L `* M —→ L′ `* M
|
||||
|
||||
ξ-*₂ : ∀ {Γ} {V M M′ : Γ ⊢ Nat}
|
||||
→ Value V
|
||||
→ M —→ M′
|
||||
-----------------
|
||||
→ V `* M —→ V `* M′
|
||||
|
||||
δ-* : ∀ {Γ c d}
|
||||
-------------------------------------
|
||||
→ con {Γ = Γ} c `* con d —→ con (c * d)
|
||||
|
||||
-- let
|
||||
|
||||
ξ-let : ∀ {Γ A B} {M M′ : Γ ⊢ A} {N : Γ , A ⊢ B}
|
||||
→ M —→ M′
|
||||
---------------------
|
||||
→ `let M N —→ `let M′ N
|
||||
|
||||
β-let : ∀ {Γ A B} {V : Γ ⊢ A} {N : Γ , A ⊢ B}
|
||||
→ Value V
|
||||
-------------------
|
||||
→ `let V N —→ N [ V ]
|
||||
|
||||
-- products
|
||||
|
||||
ξ-⟨,⟩₁ : ∀ {Γ A B} {M M′ : Γ ⊢ A} {N : Γ ⊢ B}
|
||||
→ M —→ M′
|
||||
-------------------------
|
||||
→ `⟨ M , N ⟩ —→ `⟨ M′ , N ⟩
|
||||
|
||||
ξ-⟨,⟩₂ : ∀ {Γ A B} {V : Γ ⊢ A} {N N′ : Γ ⊢ B}
|
||||
→ Value V
|
||||
→ N —→ N′
|
||||
-------------------------
|
||||
→ `⟨ V , N ⟩ —→ `⟨ V , N′ ⟩
|
||||
|
||||
ξ-proj₁ : ∀ {Γ A B} {L L′ : Γ ⊢ A `× B}
|
||||
→ L —→ L′
|
||||
---------------------
|
||||
→ `proj₁ L —→ `proj₁ L′
|
||||
|
||||
ξ-proj₂ : ∀ {Γ A B} {L L′ : Γ ⊢ A `× B}
|
||||
→ L —→ L′
|
||||
---------------------
|
||||
→ `proj₂ L —→ `proj₂ L′
|
||||
|
||||
β-proj₁ : ∀ {Γ A B} {V : Γ ⊢ A} {W : Γ ⊢ B}
|
||||
→ Value V
|
||||
→ Value W
|
||||
----------------------
|
||||
→ `proj₁ `⟨ V , W ⟩ —→ V
|
||||
|
||||
β-proj₂ : ∀ {Γ A B} {V : Γ ⊢ A} {W : Γ ⊢ B}
|
||||
→ Value V
|
||||
→ Value W
|
||||
----------------------
|
||||
→ `proj₂ `⟨ V , W ⟩ —→ W
|
||||
|
||||
-- alternative formulation of products
|
||||
|
||||
ξ-case× : ∀ {Γ A B C} {L L′ : Γ ⊢ A `× B} {M : Γ , A , B ⊢ C}
|
||||
→ L —→ L′
|
||||
-----------------------
|
||||
→ case× L M —→ case× L′ M
|
||||
|
||||
β-case× : ∀ {Γ A B C} {V : Γ ⊢ A} {W : Γ ⊢ B} {M : Γ , A , B ⊢ C}
|
||||
→ Value V
|
||||
→ Value W
|
||||
----------------------------------
|
||||
→ case× `⟨ V , W ⟩ M —→ M [ V ][ W ]
|
||||
```
|
||||
|
||||
## 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
|
||||
```
|
||||
|
||||
|
||||
## Values do not reduce
|
||||
|
||||
```
|
||||
V¬—→ : ∀ {Γ A} {M N : Γ ⊢ A}
|
||||
→ Value M
|
||||
----------
|
||||
→ ¬ (M —→ N)
|
||||
V¬—→ V-ƛ ()
|
||||
V¬—→ V-zero ()
|
||||
V¬—→ (V-suc VM) (ξ-suc M—→M′) = V¬—→ VM M—→M′
|
||||
V¬—→ V-con ()
|
||||
V¬—→ V-⟨ VM , _ ⟩ (ξ-⟨,⟩₁ M—→M′) = V¬—→ VM M—→M′
|
||||
V¬—→ V-⟨ _ , VN ⟩ (ξ-⟨,⟩₂ _ N—→N′) = V¬—→ VN N—→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 β-μ
|
||||
progress (con n) = done V-con
|
||||
progress (L `* M) with progress L
|
||||
... | step L—→L′ = step (ξ-*₁ L—→L′)
|
||||
... | done V-con with progress M
|
||||
... | step M—→M′ = step (ξ-*₂ V-con M—→M′)
|
||||
... | done V-con = step δ-*
|
||||
progress (`let M N) with progress M
|
||||
... | step M—→M′ = step (ξ-let M—→M′)
|
||||
... | done VM = step (β-let VM)
|
||||
progress `⟨ M , N ⟩ with progress M
|
||||
... | step M—→M′ = step (ξ-⟨,⟩₁ M—→M′)
|
||||
... | done VM with progress N
|
||||
... | step N—→N′ = step (ξ-⟨,⟩₂ VM N—→N′)
|
||||
... | done VN = done (V-⟨ VM , VN ⟩)
|
||||
progress (`proj₁ L) with progress L
|
||||
... | step L—→L′ = step (ξ-proj₁ L—→L′)
|
||||
... | done (V-⟨ VM , VN ⟩) = step (β-proj₁ VM VN)
|
||||
progress (`proj₂ L) with progress L
|
||||
... | step L—→L′ = step (ξ-proj₂ L—→L′)
|
||||
... | done (V-⟨ VM , VN ⟩) = step (β-proj₂ VM VN)
|
||||
progress (case× L M) with progress L
|
||||
... | step L—→L′ = step (ξ-case× L—→L′)
|
||||
... | done (V-⟨ VM , VN ⟩) = step (β-case× VM VN)
|
||||
```
|
||||
|
||||
|
||||
## 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
|
||||
```
|
||||
|
||||
## Examples
|
||||
|
||||
```
|
||||
cube : ∅ ⊢ Nat ⇒ Nat
|
||||
cube = ƛ (# 0 `* # 0 `* # 0)
|
||||
|
||||
_ : cube · con 2 —↠ con 8
|
||||
_ =
|
||||
begin
|
||||
cube · con 2
|
||||
—→⟨ β-ƛ V-con ⟩
|
||||
con 2 `* con 2 `* con 2
|
||||
—→⟨ ξ-*₁ δ-* ⟩
|
||||
con 4 `* con 2
|
||||
—→⟨ δ-* ⟩
|
||||
con 8
|
||||
∎
|
||||
|
||||
exp10 : ∅ ⊢ Nat ⇒ Nat
|
||||
exp10 = ƛ (`let (# 0 `* # 0)
|
||||
(`let (# 0 `* # 0)
|
||||
(`let (# 0 `* # 2)
|
||||
(# 0 `* # 0))))
|
||||
|
||||
_ : exp10 · con 2 —↠ con 1024
|
||||
_ =
|
||||
begin
|
||||
exp10 · con 2
|
||||
—→⟨ β-ƛ V-con ⟩
|
||||
`let (con 2 `* con 2) (`let (# 0 `* # 0) (`let (# 0 `* con 2) (# 0 `* # 0)))
|
||||
—→⟨ ξ-let δ-* ⟩
|
||||
`let (con 4) (`let (# 0 `* # 0) (`let (# 0 `* con 2) (# 0 `* # 0)))
|
||||
—→⟨ β-let V-con ⟩
|
||||
`let (con 4 `* con 4) (`let (# 0 `* con 2) (# 0 `* # 0))
|
||||
—→⟨ ξ-let δ-* ⟩
|
||||
`let (con 16) (`let (# 0 `* con 2) (# 0 `* # 0))
|
||||
—→⟨ β-let V-con ⟩
|
||||
`let (con 16 `* con 2) (# 0 `* # 0)
|
||||
—→⟨ ξ-let δ-* ⟩
|
||||
`let (con 32) (# 0 `* # 0)
|
||||
—→⟨ β-let V-con ⟩
|
||||
con 32 `* con 32
|
||||
—→⟨ δ-* ⟩
|
||||
con 1024
|
||||
∎
|
||||
|
||||
swap× : ∀ {A B} → ∅ ⊢ A `× B ⇒ B `× A
|
||||
swap× = ƛ `⟨ `proj₂ (# 0) , `proj₁ (# 0) ⟩
|
||||
|
||||
_ : swap× · `⟨ con 42 , `zero ⟩ —↠ `⟨ `zero , con 42 ⟩
|
||||
_ =
|
||||
begin
|
||||
swap× · `⟨ con 42 , `zero ⟩
|
||||
—→⟨ β-ƛ V-⟨ V-con , V-zero ⟩ ⟩
|
||||
`⟨ `proj₂ `⟨ con 42 , `zero ⟩ , `proj₁ `⟨ con 42 , `zero ⟩ ⟩
|
||||
—→⟨ ξ-⟨,⟩₁ (β-proj₂ V-con V-zero) ⟩
|
||||
`⟨ `zero , `proj₁ `⟨ con 42 , `zero ⟩ ⟩
|
||||
—→⟨ ξ-⟨,⟩₂ V-zero (β-proj₁ V-con V-zero) ⟩
|
||||
`⟨ `zero , con 42 ⟩
|
||||
∎
|
||||
|
||||
swap×-case : ∀ {A B} → ∅ ⊢ A `× B ⇒ B `× A
|
||||
swap×-case = ƛ case× (# 0) `⟨ # 0 , # 1 ⟩
|
||||
|
||||
_ : swap×-case · `⟨ con 42 , `zero ⟩ —↠ `⟨ `zero , con 42 ⟩
|
||||
_ =
|
||||
begin
|
||||
swap×-case · `⟨ con 42 , `zero ⟩
|
||||
—→⟨ β-ƛ V-⟨ V-con , V-zero ⟩ ⟩
|
||||
case× `⟨ con 42 , `zero ⟩ `⟨ # 0 , # 1 ⟩
|
||||
—→⟨ β-case× V-con V-zero ⟩
|
||||
`⟨ `zero , con 42 ⟩
|
||||
∎
|
||||
```
|
||||
|
||||
|
||||
#### Exercise `More` (recommended in part)
|
||||
|
||||
Formalise the remaining constructs defined in this chapter.
|
||||
Evaluate each example, applied to data as needed,
|
||||
to confirm it returns the expected answer.
|
||||
|
||||
* sums (recommended)
|
||||
* unit type
|
||||
* an alternative formulation of unit type
|
||||
* empty type (recommended)
|
||||
* lists
|
||||
|
|
@ -1,454 +0,0 @@
|
|||
---
|
||||
title : "Assignment5: PUC Assignment 5"
|
||||
layout : page
|
||||
permalink : /PUC/2019/Assignment5/
|
||||
---
|
||||
|
||||
```
|
||||
module Assignment5 where
|
||||
```
|
||||
|
||||
## YOUR NAME AND EMAIL GOES HERE
|
||||
|
||||
|
||||
## Introduction
|
||||
|
||||
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.
|
||||
|
||||
Please ensure your files execute correctly under Agda!
|
||||
|
||||
**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; cong₂; _≢_)
|
||||
open import Data.Empty using (⊥; ⊥-elim)
|
||||
open import Data.Nat using (ℕ; zero; suc; _+_; _*_)
|
||||
open import Data.Product using (_×_; ∃; ∃-syntax) renaming (_,_ to ⟨_,_⟩)
|
||||
open import Data.String using (String; _≟_)
|
||||
open import Relation.Nullary using (¬_; Dec; yes; no)
|
||||
```
|
||||
|
||||
|
||||
## Inference
|
||||
|
||||
```
|
||||
module Inference where
|
||||
```
|
||||
|
||||
Remember to indent all code by two spaces.
|
||||
|
||||
### Imports
|
||||
|
||||
```
|
||||
import plfa.part2.More as DB
|
||||
```
|
||||
|
||||
### Syntax
|
||||
|
||||
```
|
||||
infix 4 _∋_⦂_
|
||||
infix 4 _⊢_↑_
|
||||
infix 4 _⊢_↓_
|
||||
infixl 5 _,_⦂_
|
||||
|
||||
infixr 7 _⇒_
|
||||
|
||||
infix 5 ƛ_⇒_
|
||||
infix 5 μ_⇒_
|
||||
infix 6 _↑
|
||||
infix 6 _↓_
|
||||
infixl 7 _·_
|
||||
infix 8 `suc_
|
||||
infix 9 `_
|
||||
```
|
||||
|
||||
### Identifiers, types, and contexts
|
||||
|
||||
```
|
||||
Id : Set
|
||||
Id = String
|
||||
|
||||
data Type : Set where
|
||||
`ℕ : Type
|
||||
_⇒_ : Type → Type → Type
|
||||
|
||||
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⁻
|
||||
```
|
||||
|
||||
### Sample terms
|
||||
|
||||
```
|
||||
two : Term⁻
|
||||
two = `suc (`suc `zero)
|
||||
|
||||
plus : Term⁺
|
||||
plus = (μ "p" ⇒ ƛ "m" ⇒ ƛ "n" ⇒
|
||||
`case (` "m") [zero⇒ ` "n" ↑
|
||||
|suc "m" ⇒ `suc (` "p" · (` "m" ↑) · (` "n" ↑) ↑) ])
|
||||
↓ `ℕ ⇒ `ℕ ⇒ `ℕ
|
||||
|
||||
2+2 : Term⁺
|
||||
2+2 = plus · two · two
|
||||
```
|
||||
|
||||
### 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)
|
||||
```
|
||||
|
||||
### Erasure
|
||||
|
||||
```
|
||||
∥_∥Tp : Type → DB.Type
|
||||
∥ `ℕ ∥Tp = DB.`ℕ
|
||||
∥ A ⇒ B ∥Tp = ∥ A ∥Tp DB.⇒ ∥ B ∥Tp
|
||||
|
||||
∥_∥Cx : Context → DB.Context
|
||||
∥ ∅ ∥Cx = DB.∅
|
||||
∥ Γ , x ⦂ A ∥Cx = ∥ Γ ∥Cx DB., ∥ A ∥Tp
|
||||
|
||||
∥_∥∋ : ∀ {Γ x A} → Γ ∋ x ⦂ A → ∥ Γ ∥Cx DB.∋ ∥ A ∥Tp
|
||||
∥ Z ∥∋ = DB.Z
|
||||
∥ S x≢ ⊢x ∥∋ = DB.S ∥ ⊢x ∥∋
|
||||
|
||||
∥_∥⁺ : ∀ {Γ M A} → Γ ⊢ M ↑ A → ∥ Γ ∥Cx DB.⊢ ∥ A ∥Tp
|
||||
∥_∥⁻ : ∀ {Γ M A} → Γ ⊢ M ↓ A → ∥ Γ ∥Cx DB.⊢ ∥ A ∥Tp
|
||||
|
||||
∥ ⊢` ⊢x ∥⁺ = DB.` ∥ ⊢x ∥∋
|
||||
∥ ⊢L · ⊢M ∥⁺ = ∥ ⊢L ∥⁺ DB.· ∥ ⊢M ∥⁻
|
||||
∥ ⊢↓ ⊢M ∥⁺ = ∥ ⊢M ∥⁻
|
||||
|
||||
∥ ⊢ƛ ⊢N ∥⁻ = DB.ƛ ∥ ⊢N ∥⁻
|
||||
∥ ⊢zero ∥⁻ = DB.`zero
|
||||
∥ ⊢suc ⊢M ∥⁻ = DB.`suc ∥ ⊢M ∥⁻
|
||||
∥ ⊢case ⊢L ⊢M ⊢N ∥⁻ = DB.case ∥ ⊢L ∥⁺ ∥ ⊢M ∥⁻ ∥ ⊢N ∥⁻
|
||||
∥ ⊢μ ⊢M ∥⁻ = DB.μ ∥ ⊢M ∥⁻
|
||||
∥ ⊢↑ ⊢M refl ∥⁻ = ∥ ⊢M ∥⁺
|
||||
```
|
||||
|
||||
|
||||
#### Exercise `bidirectional-mul` (recommended) {#bidirectional-mul}
|
||||
|
||||
Rewrite your definition of multiplication from
|
||||
Chapter [Lambda][plfa.Lambda], decorated to support inference.
|
||||
|
||||
|
||||
#### Exercise `bidirectional-products` (recommended) {#bidirectional-products}
|
||||
|
||||
Extend the bidirectional type rules to include products from
|
||||
Chapter [More][plfa.More].
|
||||
|
||||
|
||||
#### Exercise `bidirectional-rest` (stretch)
|
||||
|
||||
Extend the bidirectional type rules to include the rest of the constructs from
|
||||
Chapter [More][plfa.More].
|
||||
|
||||
|
||||
#### Exercise `inference-mul` (recommended)
|
||||
|
||||
Using the definition from exercise [bidirectional-mul](#bidirectional-mul),
|
||||
infer the corresponding inherently typed term.
|
||||
Show that erasure of the inferred typing yields your definition of
|
||||
multiplication from Chapter [DeBruijn][plfa.DeBruijn].
|
||||
|
||||
|
||||
#### Exercise `inference-products` (recommended)
|
||||
|
||||
Extend bidirectional inference to include products from
|
||||
Chapter [More][plfa.More].
|
||||
|
||||
|
||||
#### Exercise `inference-rest` (stretch)
|
||||
|
||||
Extend bidirectional inference to include the rest of the constructs from
|
||||
Chapter [More][plfa.More].
|
||||
|
||||
## Untyped
|
||||
|
||||
#### Exercise (`Type≃⊤`)
|
||||
|
||||
Show that `Type` is isomorphic to `⊤`, the unit type.
|
||||
|
||||
#### Exercise (`Context≃ℕ`)
|
||||
|
||||
Show that `Context` is isomorphic to `ℕ`.
|
||||
|
||||
#### Exercise (`variant-1`)
|
||||
|
||||
How would the rules change if we want call-by-value where terms
|
||||
normalise completely? Assume that `β` should not permit reduction
|
||||
unless both terms are in normal form.
|
||||
|
||||
#### Exercise (`variant-2`)
|
||||
|
||||
How would the rules change if we want call-by-value where terms
|
||||
do not reduce underneath lambda? Assume that `β`
|
||||
permits reduction when both terms are values (that is, lambda
|
||||
abstractions). What would `2+2ᶜ` reduce to in this case?
|
||||
|
||||
#### Exercise `plus-eval`
|
||||
|
||||
Use the evaluator to confirm that `plus · two · two` and `four`
|
||||
normalise to the same term.
|
||||
|
||||
#### Exercise `multiplication-untyped` (recommended)
|
||||
|
||||
Use the encodings above to translate your definition of
|
||||
multiplication from previous chapters with the Scott
|
||||
representation and the encoding of the fixpoint operator.
|
||||
Confirm that two times two is four.
|
||||
|
||||
#### Exercise `encode-more` (stretch)
|
||||
|
||||
Along the lines above, encode all of the constructs of
|
||||
Chapter [More][plfa.More],
|
||||
save for primitive numbers, in the untyped lambda calculus.
|
||||
|
|
@ -1,678 +0,0 @@
|
|||
---
|
||||
title : "Exam: TSPL Mock Exam file"
|
||||
layout : page
|
||||
permalink : /PUC/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)
|
||||
```
|
||||
|
|
@ -1,3 +0,0 @@
|
|||
name: puc2019
|
||||
depend: standard-library plfa
|
||||
include: .
|
||||
|
|
@ -1,107 +0,0 @@
|
|||
---
|
||||
title : "PUC-Rio: Course notes"
|
||||
layout : page
|
||||
permalink : /PUC/2019/
|
||||
---
|
||||
|
||||
## Staff
|
||||
|
||||
* **Instructor**
|
||||
[Philip Wadler](https://homepages.inf.ed.ac.uk/wadler)
|
||||
|
||||
* **Host**
|
||||
[Roberto Ierusalimschy](http://www.inf.puc-rio.br/~roberto/)
|
||||
|
||||
## Schedule
|
||||
|
||||
Lectures and tutorials take place Fridays and some Thursdays in 548L.
|
||||
* **13.00--14.30pm** Lecture
|
||||
* **14.30--16.00pm** Tutorial
|
||||
|
||||
<table>
|
||||
<tr>
|
||||
<td><b>Fri 29 Mar</b></td>
|
||||
<td><a href="{{ site.baseurl }}/Naturals/">Naturals</a></td>
|
||||
</tr>
|
||||
<tr>
|
||||
<td><b>Fri 5 Apr</b></td>
|
||||
<td><a href="{{ site.baseurl }}/Induction/">Induction</a> & <a href="{{ site.baseurl }}/Relations/">Relations</a></td>
|
||||
</tr>
|
||||
<tr>
|
||||
<td><b>Thu 11 Apr</b></td>
|
||||
<td><a href="{{ site.baseurl }}/Relations/">Relations</a></td>
|
||||
</tr>
|
||||
<tr>
|
||||
<td><b>Fri 19 Apr</b></td>
|
||||
<td>(Miami)</td>
|
||||
</tr>
|
||||
<tr>
|
||||
<td><b>Fri 26 Apr</b></td>
|
||||
<td><a href="{{ site.baseurl }}/Equality/">Equality</a> &
|
||||
<a href="{{ site.baseurl }}/Isomorphism/">Isomorphism</a> &
|
||||
<a href="{{ site.baseurl }}/Connectives/">Connectives</a></td>
|
||||
</tr>
|
||||
<tr>
|
||||
<td><b>Fri 3 May</b></td>
|
||||
<td><a href="{{ site.baseurl }}/Negation/">Negation</a> &
|
||||
<a href="{{ site.baseurl }}/Quantifiers/">Quantifiers</a> &
|
||||
<a href="{{ site.baseurl }}/Decidable/">Decidable</a> &
|
||||
<a href="{{ site.baseurl }}/Lists/">Lists</a></td>
|
||||
</tr>
|
||||
<tr>
|
||||
<td><b>Fri 10 May</b></td>
|
||||
<td>(Melbourne)</td>
|
||||
</tr>
|
||||
<tr>
|
||||
<td><b>Fri 17 May</b></td>
|
||||
<td>(Sydney)</td>
|
||||
</tr>
|
||||
<tr>
|
||||
<td><b>Fri 24 May</b></td>
|
||||
<td><a href="{{ site.baseurl }}/Lambda/">Lambda</a> &
|
||||
<a href="{{ site.baseurl }}/Properties/">Properties</a></td>
|
||||
</tr>
|
||||
<tr>
|
||||
<td><b>Fri 31 May</b></td>
|
||||
<td>(Padova)</td>
|
||||
</tr>
|
||||
<tr>
|
||||
<td><b>Fri 7 June</b></td>
|
||||
<td><a href="{{ site.baseurl }}/DeBruijn/">DeBruijn</a> &
|
||||
<a href="{{ site.baseurl }}/More/">More</a></td>
|
||||
</tr>
|
||||
<tr>
|
||||
<td><b>Fri 14 June</b></td>
|
||||
<td>(Buenos Aires)</td>
|
||||
</tr>
|
||||
<tr>
|
||||
<td><b>Fri 21 June</b></td>
|
||||
<td><a href="{{ site.baseurl }}/Inference/">Inference</a> &
|
||||
<a href="{{ site.baseurl }}/Untyped/">Untyped</a></td>
|
||||
</tr>
|
||||
<tr>
|
||||
<td><b>Fri 28 June</b></td>
|
||||
<td>Propositions as Types & mock exam</td>
|
||||
</tr>
|
||||
<tr>
|
||||
<td><b>Fri 5 July</b></td>
|
||||
<td>exam</td>
|
||||
</tr>
|
||||
</table>
|
||||
|
||||
|
||||
## Assignments
|
||||
|
||||
For instructions on how to set up Agda for PLFA see [Getting Started]({{ site.baseurl }}/GettingStarted/).
|
||||
|
||||
* [PUC Assignment 1]({{ site.baseurl }}/PUC/2019/Assignment1/) due Friday 26 April.
|
||||
* [PUC Assignment 2]({{ site.baseurl }}/PUC/2019/Assignment2/) due Wednesday 22 May.
|
||||
* [PUC Assignment 3]({{ site.baseurl }}/PUC/2019/Assignment3/) due Wednesday 5 June.
|
||||
* [PUC Assignment 4]({{ site.baseurl }}/PUC/2019/Assignment4/) due Wednesday 19 June.
|
||||
* [PUC Assignment 5]({{ site.baseurl }}/PUC/2019/Assignment5/) due Tuesday 25 June.
|
||||
* [PUC Assignment 6]({{ site.baseurl }}/courses/tspl/2018/Mock1.pdf) due Tuesday 25 June.
|
||||
Use file [Exam]({{ site.baseurl }}/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 `Assignment1.lagda.md` or the like. Include
|
||||
your name and email in the submitted file.
|
||||
|
|
@ -1,314 +0,0 @@
|
|||
---
|
||||
title : "Assignment1: TSPL Assignment 1"
|
||||
layout : page
|
||||
permalink : /TSPL/2018/Assignment1/
|
||||
---
|
||||
|
||||
```
|
||||
module Assignment1 where
|
||||
```
|
||||
|
||||
## YOUR NAME AND EMAIL GOES HERE
|
||||
|
||||
## Introduction
|
||||
|
||||
<!-- This assignment is due **1pm Friday 26 April**. -->
|
||||
|
||||
You must do _all_ the exercises labelled "(recommended)".
|
||||
|
||||
Exercises labelled "(stretch)" are there to provide an extra challenge.
|
||||
You don't need to do all of these, but should attempt at least a few.
|
||||
|
||||
Exercises without a label are optional, and may be done if you want
|
||||
some extra practice.
|
||||
|
||||
<!-- Submit your homework using the "submit" command. -->
|
||||
Please ensure your files execute correctly under Agda!
|
||||
|
||||
## Imports
|
||||
|
||||
```
|
||||
import Relation.Binary.PropositionalEquality as Eq
|
||||
open Eq using (_≡_; refl; cong; sym)
|
||||
open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; _≡⟨_⟩_; _∎)
|
||||
open import Data.Nat using (ℕ; zero; suc; _+_; _*_; _∸_; _≤_; z≤n; s≤s)
|
||||
open import Data.Nat.Properties using (+-assoc; +-identityʳ; +-suc; +-comm;
|
||||
≤-refl; ≤-trans; ≤-antisym; ≤-total; +-monoʳ-≤; +-monoˡ-≤; +-mono-≤)
|
||||
open import plfa.part1.Relations using (_<_; z<s; s<s; zero; suc; even; odd)
|
||||
```
|
||||
|
||||
## Naturals
|
||||
|
||||
#### Exercise `seven` {#seven}
|
||||
|
||||
Write out `7` in longhand.
|
||||
|
||||
|
||||
#### Exercise `+-example` {#plus-example}
|
||||
|
||||
Compute `3 + 4`, writing out your reasoning as a chain of equations.
|
||||
|
||||
|
||||
#### Exercise `*-example` {#times-example}
|
||||
|
||||
Compute `3 * 4`, writing out your reasoning as a chain of equations.
|
||||
|
||||
|
||||
#### Exercise `_^_` (recommended) {#power}
|
||||
|
||||
Define exponentiation, which is given by the following equations.
|
||||
|
||||
n ^ 0 = 1
|
||||
n ^ (1 + m) = n * (n ^ m)
|
||||
|
||||
Check that `3 ^ 4` is `81`.
|
||||
|
||||
|
||||
#### Exercise `∸-examples` (recommended) {#monus-examples}
|
||||
|
||||
Compute `5 ∸ 3` and `3 ∸ 5`, writing out your reasoning as a chain of equations.
|
||||
|
||||
|
||||
#### Exercise `Bin` (stretch) {#Bin}
|
||||
|
||||
A more efficient representation of natural numbers uses a binary
|
||||
rather than a unary system. We represent a number as a bitstring.
|
||||
```
|
||||
data Bin : Set where
|
||||
nil : Bin
|
||||
x0_ : Bin → Bin
|
||||
x1_ : Bin → Bin
|
||||
```
|
||||
For instance, the bitstring
|
||||
|
||||
1011
|
||||
|
||||
standing for the number eleven is encoded, right to left, as
|
||||
|
||||
x1 x1 x0 x1 nil
|
||||
|
||||
Representations are not unique due to leading zeros.
|
||||
Hence, eleven is also represented by `001011`, encoded as
|
||||
|
||||
x1 x1 x0 x1 x0 x0 nil
|
||||
|
||||
Define a function
|
||||
|
||||
inc : Bin → Bin
|
||||
|
||||
that converts a bitstring to the bitstring for the next higher
|
||||
number. For example, since `1100` encodes twelve, we should have
|
||||
|
||||
inc (x1 x1 x0 x1 nil) ≡ x0 x0 x1 x1 nil
|
||||
|
||||
Confirm that this gives the correct answer for the bitstrings
|
||||
encoding zero through four.
|
||||
|
||||
Using the above, define a pair of functions to convert
|
||||
between the two representations.
|
||||
|
||||
to : ℕ → Bin
|
||||
from : Bin → ℕ
|
||||
|
||||
For the former, choose the bitstring to have no leading zeros if it
|
||||
represents a positive natural, and represent zero by `x0 nil`.
|
||||
Confirm that these both give the correct answer for zero through four.
|
||||
|
||||
## Induction
|
||||
|
||||
#### Exercise `operators` {#operators}
|
||||
|
||||
Give another example of a pair of operators that have an identity
|
||||
and are associative, commutative, and distribute over one another.
|
||||
|
||||
Give an example of an operator that has an identity and is
|
||||
associative but is not commutative.
|
||||
|
||||
|
||||
#### Exercise `finite-+-assoc` (stretch) {#finite-plus-assoc}
|
||||
|
||||
Write out what is known about associativity of addition on each of the first four
|
||||
days using a finite story of creation, as
|
||||
[earlier][plfa.Naturals#finite-creation]
|
||||
|
||||
|
||||
#### Exercise `+-swap` (recommended) {#plus-swap}
|
||||
|
||||
Show
|
||||
|
||||
m + (n + p) ≡ n + (m + p)
|
||||
|
||||
for all naturals `m`, `n`, and `p`. No induction is needed,
|
||||
just apply the previous results which show addition
|
||||
is associative and commutative. You may need to use
|
||||
the following function from the standard library:
|
||||
|
||||
sym : ∀ {m n : ℕ} → m ≡ n → n ≡ m
|
||||
|
||||
|
||||
#### Exercise `*-distrib-+` (recommended) {#times-distrib-plus}
|
||||
|
||||
Show multiplication distributes over addition, that is,
|
||||
|
||||
(m + n) * p ≡ m * p + n * p
|
||||
|
||||
for all naturals `m`, `n`, and `p`.
|
||||
|
||||
#### Exercise `*-assoc` (recommended) {#times-assoc}
|
||||
|
||||
Show multiplication is associative, that is,
|
||||
|
||||
(m * n) * p ≡ m * (n * p)
|
||||
|
||||
for all naturals `m`, `n`, and `p`.
|
||||
|
||||
#### Exercise `*-comm` {#times-comm}
|
||||
|
||||
Show multiplication is commutative, that is,
|
||||
|
||||
m * n ≡ n * m
|
||||
|
||||
for all naturals `m` and `n`. As with commutativity of addition,
|
||||
you will need to formulate and prove suitable lemmas.
|
||||
|
||||
#### Exercise `0∸n≡0` {#zero-monus}
|
||||
|
||||
Show
|
||||
|
||||
zero ∸ n ≡ zero
|
||||
|
||||
for all naturals `n`. Did your proof require induction?
|
||||
|
||||
#### Exercise `∸-+-assoc` {#monus-plus-assoc}
|
||||
|
||||
Show that monus associates with addition, that is,
|
||||
|
||||
m ∸ n ∸ p ≡ m ∸ (n + p)
|
||||
|
||||
for all naturals `m`, `n`, and `p`.
|
||||
|
||||
#### Exercise `Bin-laws` (stretch) {#Bin-laws}
|
||||
|
||||
Recall that
|
||||
Exercise [Bin][plfa.Naturals#Bin]
|
||||
defines a datatype `Bin` of bitstrings representing natural numbers
|
||||
and asks you to define functions
|
||||
|
||||
inc : Bin → Bin
|
||||
to : ℕ → Bin
|
||||
from : Bin → ℕ
|
||||
|
||||
Consider the following laws, where `n` ranges over naturals and `x`
|
||||
over bitstrings.
|
||||
|
||||
from (inc x) ≡ suc (from x)
|
||||
to (from n) ≡ n
|
||||
from (to x) ≡ x
|
||||
|
||||
For each law: if it holds, prove; if not, give a counterexample.
|
||||
|
||||
|
||||
## Relations
|
||||
|
||||
|
||||
#### Exercise `orderings` {#orderings}
|
||||
|
||||
Give an example of a preorder that is not a partial order.
|
||||
|
||||
Give an example of a partial order that is not a preorder.
|
||||
|
||||
|
||||
#### Exercise `≤-antisym-cases` {#leq-antisym-cases}
|
||||
|
||||
The above proof omits cases where one argument is `z≤n` and one
|
||||
argument is `s≤s`. Why is it ok to omit them?
|
||||
|
||||
|
||||
#### Exercise `*-mono-≤` (stretch)
|
||||
|
||||
Show that multiplication is monotonic with regard to inequality.
|
||||
|
||||
|
||||
#### Exercise `<-trans` (recommended) {#less-trans}
|
||||
|
||||
Show that strict inequality is transitive.
|
||||
|
||||
#### Exercise `trichotomy` {#trichotomy}
|
||||
|
||||
Show that strict inequality satisfies a weak version of trichotomy, in
|
||||
the sense that for any `m` and `n` that one of the following holds:
|
||||
* `m < n`,
|
||||
* `m ≡ n`, or
|
||||
* `m > n`
|
||||
Define `m > n` to be the same as `n < m`.
|
||||
You will need a suitable data declaration,
|
||||
similar to that used for totality.
|
||||
(We will show that the three cases are exclusive after we introduce
|
||||
[negation][plfa.Negation].)
|
||||
|
||||
#### Exercise `+-mono-<` {#plus-mono-less}
|
||||
|
||||
Show that addition is monotonic with respect to strict inequality.
|
||||
As with inequality, some additional definitions may be required.
|
||||
|
||||
#### Exercise `≤-iff-<` (recommended) {#leq-iff-less}
|
||||
|
||||
Show that `suc m ≤ n` implies `m < n`, and conversely.
|
||||
|
||||
#### Exercise `<-trans-revisited` {#less-trans-revisited}
|
||||
|
||||
Give an alternative proof that strict inequality is transitive,
|
||||
using the relating between strict inequality and inequality and
|
||||
the fact that inequality is transitive.
|
||||
|
||||
#### Exercise `o+o≡e` (stretch) {#odd-plus-odd}
|
||||
|
||||
Show that the sum of two odd numbers is even.
|
||||
|
||||
#### Exercise `Bin-predicates` (stretch) {#Bin-predicates}
|
||||
|
||||
Recall that
|
||||
Exercise [Bin][plfa.Naturals#Bin]
|
||||
defines a datatype `Bin` of bitstrings representing natural numbers.
|
||||
Representations are not unique due to leading zeros.
|
||||
Hence, eleven may be represented by both of the following
|
||||
|
||||
x1 x1 x0 x1 nil
|
||||
x1 x1 x0 x1 x0 x0 nil
|
||||
|
||||
Define a predicate
|
||||
|
||||
Can : Bin → Set
|
||||
|
||||
over all bitstrings that holds if the bitstring is canonical, meaning
|
||||
it has no leading zeros; the first representation of eleven above is
|
||||
canonical, and the second is not. To define it, you will need an
|
||||
auxiliary predicate
|
||||
|
||||
One : Bin → Set
|
||||
|
||||
that holds only if the bistring has a leading one. A bitstring is
|
||||
canonical if it has a leading one (representing a positive number) or
|
||||
if it consists of a single zero (representing zero).
|
||||
|
||||
Show that increment preserves canonical bitstrings.
|
||||
|
||||
Can x
|
||||
------------
|
||||
Can (inc x)
|
||||
|
||||
Show that converting a natural to a bitstring always yields a
|
||||
canonical bitstring.
|
||||
|
||||
----------
|
||||
Can (to n)
|
||||
|
||||
Show that converting a canonical bitstring to a natural
|
||||
and back is the identity.
|
||||
|
||||
Can x
|
||||
---------------
|
||||
to (from x) ≡ x
|
||||
|
||||
(Hint: For each of these, you may first need to prove related
|
||||
properties of `One`.)
|
||||
|
|
@ -1,363 +0,0 @@
|
|||
---
|
||||
title : "Assignment2: TSPL Assignment 2"
|
||||
layout : page
|
||||
permalink : /TSPL/2018/Assignment2/
|
||||
---
|
||||
|
||||
```
|
||||
module Assignment2 where
|
||||
```
|
||||
|
||||
## YOUR NAME AND EMAIL GOES HERE
|
||||
|
||||
## Introduction
|
||||
|
||||
<!-- This assignment is due **4pm Thursday 18 October** (Week 5). -->
|
||||
|
||||
You must do _all_ the exercises labelled "(recommended)".
|
||||
|
||||
Exercises labelled "(stretch)" are there to provide an extra challenge.
|
||||
You don't need to do all of these, but should attempt at least a few.
|
||||
|
||||
Exercises without a label are optional, and may be done if you want
|
||||
some extra practice.
|
||||
|
||||
<!-- Submit your homework using the "submit" command. -->
|
||||
Please ensure your files execute correctly under Agda!
|
||||
|
||||
## Imports
|
||||
|
||||
```
|
||||
import Relation.Binary.PropositionalEquality as Eq
|
||||
open Eq using (_≡_; refl; cong; sym)
|
||||
open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; _≡⟨_⟩_; _∎)
|
||||
open import Data.Nat using (ℕ; zero; suc; _+_; _*_; _∸_; _≤_; z≤n; s≤s)
|
||||
open import Data.Nat.Properties using (+-assoc; +-identityʳ; +-suc; +-comm;
|
||||
≤-refl; ≤-trans; ≤-antisym; ≤-total; +-monoʳ-≤; +-monoˡ-≤; +-mono-≤)
|
||||
open import Data.Product using (_×_; proj₁; proj₂) renaming (_,_ to ⟨_,_⟩)
|
||||
open import Data.Unit using (⊤; tt)
|
||||
open import Data.Sum using (_⊎_; inj₁; inj₂) renaming ([_,_] to case-⊎)
|
||||
open import Data.Empty using (⊥; ⊥-elim)
|
||||
open import Data.Bool.Base using (Bool; true; false; T; _∧_; _∨_; not)
|
||||
open import Relation.Nullary using (¬_; Dec; yes; no)
|
||||
open import Relation.Nullary.Decidable using (⌊_⌋; toWitness; fromWitness)
|
||||
open import Relation.Nullary.Negation using (¬?)
|
||||
open import Relation.Nullary.Product using (_×-dec_)
|
||||
open import Relation.Nullary.Sum using (_⊎-dec_)
|
||||
open import Relation.Nullary.Negation using (contraposition)
|
||||
open import Data.Product using (Σ; _,_; ∃; Σ-syntax; ∃-syntax)
|
||||
open import plfa.part1.Relations using (_<_; z<s; s<s)
|
||||
open import plfa.part1.Isomorphism using (_≃_; ≃-sym; ≃-trans; _≲_; extensionality)
|
||||
open plfa.part1.Isomorphism.≃-Reasoning
|
||||
```
|
||||
|
||||
## Equality
|
||||
|
||||
#### Exercise `≤-reasoning` (stretch)
|
||||
|
||||
The proof of monotonicity from
|
||||
Chapter [Relations][plfa.Relations]
|
||||
can be written in a more readable form by using an anologue of our
|
||||
notation for `≡-reasoning`. Define `≤-reasoning` analogously, and use
|
||||
it to write out an alternative proof that addition is monotonic with
|
||||
regard to inequality. Rewrite both `+-monoˡ-≤` and `+-mono-≤`.
|
||||
|
||||
|
||||
|
||||
## Isomorphism
|
||||
|
||||
#### Exercise `≃-implies-≲`
|
||||
|
||||
Show that every isomorphism implies an embedding.
|
||||
```
|
||||
postulate
|
||||
≃-implies-≲ : ∀ {A B : Set}
|
||||
→ A ≃ B
|
||||
-----
|
||||
→ A ≲ B
|
||||
```
|
||||
|
||||
#### Exercise `_⇔_` (recommended) {#iff}
|
||||
|
||||
Define equivalence of propositions (also known as "if and only if") as follows.
|
||||
```
|
||||
record _⇔_ (A B : Set) : Set where
|
||||
field
|
||||
to : A → B
|
||||
from : B → A
|
||||
|
||||
open _⇔_
|
||||
```
|
||||
Show that equivalence is reflexive, symmetric, and transitive.
|
||||
|
||||
#### Exercise `Bin-embedding` (stretch) {#Bin-embedding}
|
||||
|
||||
Recall that Exercises
|
||||
[Bin][plfa.Naturals#Bin] and
|
||||
[Bin-laws][plfa.Induction#Bin-laws]
|
||||
define a datatype of bitstrings representing natural numbers.
|
||||
```
|
||||
data Bin : Set where
|
||||
nil : Bin
|
||||
x0_ : Bin → Bin
|
||||
x1_ : Bin → Bin
|
||||
```
|
||||
And ask you to define the following functions:
|
||||
|
||||
to : ℕ → Bin
|
||||
from : Bin → ℕ
|
||||
|
||||
which satisfy the following property:
|
||||
|
||||
from (to n) ≡ n
|
||||
|
||||
Using the above, establish that there is an embedding of `ℕ` into `Bin`.
|
||||
Why is there not an isomorphism?
|
||||
|
||||
|
||||
## Connectives
|
||||
|
||||
#### Exercise `⇔≃×` (recommended)
|
||||
|
||||
Show that `A ⇔ B` as defined [earlier][plfa.Isomorphism#iff]
|
||||
is isomorphic to `(A → B) × (B → A)`.
|
||||
|
||||
#### Exercise `⊎-comm` (recommended)
|
||||
|
||||
Show sum is commutative up to isomorphism.
|
||||
|
||||
#### Exercise `⊎-assoc`
|
||||
|
||||
Show sum is associative up to ismorphism.
|
||||
|
||||
#### Exercise `⊥-identityˡ` (recommended)
|
||||
|
||||
Show zero is the left identity of addition.
|
||||
|
||||
#### Exercise `⊥-identityʳ`
|
||||
|
||||
Show zero is the right identity of addition.
|
||||
|
||||
#### Exercise `⊎-weak-×` (recommended)
|
||||
|
||||
Show that the following property holds.
|
||||
```
|
||||
postulate
|
||||
⊎-weak-× : ∀ {A B C : Set} → (A ⊎ B) × C → A ⊎ (B × C)
|
||||
```
|
||||
This is called a _weak distributive law_. Give the corresponding
|
||||
distributive law, and explain how it relates to the weak version.
|
||||
|
||||
#### Exercise `⊎×-implies-×⊎`
|
||||
|
||||
Show that a disjunct of conjuncts implies a conjunct of disjuncts.
|
||||
```
|
||||
postulate
|
||||
⊎×-implies-×⊎ : ∀ {A B C D : Set} → (A × B) ⊎ (C × D) → (A ⊎ C) × (B ⊎ D)
|
||||
```
|
||||
Does the converse hold? If so, prove; if not, give a counterexample.
|
||||
|
||||
|
||||
## Negation
|
||||
|
||||
#### Exercise `<-irreflexive` (recommended)
|
||||
|
||||
Using negation, show that
|
||||
[strict inequality][plfa.Relations#strict-inequality]
|
||||
is irreflexive, that is, `n < n` holds for no `n`.
|
||||
|
||||
|
||||
#### Exercise `trichotomy`
|
||||
|
||||
Show that strict inequality satisfies
|
||||
[trichotomy][plfa.Relations#trichotomy],
|
||||
that is, for any naturals `m` and `n` exactly one of the following holds:
|
||||
|
||||
* `m < n`
|
||||
* `m ≡ n`
|
||||
* `m > n`
|
||||
|
||||
Here "exactly one" means that one of the three must hold, and each implies the
|
||||
negation of the other two.
|
||||
|
||||
|
||||
#### Exercise `⊎-dual-×` (recommended)
|
||||
|
||||
Show that conjunction, disjunction, and negation are related by a
|
||||
version of De Morgan's Law.
|
||||
|
||||
¬ (A ⊎ B) ≃ (¬ A) × (¬ B)
|
||||
|
||||
This result is an easy consequence of something we've proved previously.
|
||||
|
||||
Do we also have the following?
|
||||
|
||||
¬ (A × B) ≃ (¬ A) ⊎ (¬ B)
|
||||
|
||||
If so, prove; if not, give a variant that does hold.
|
||||
|
||||
|
||||
#### Exercise `Classical` (stretch)
|
||||
|
||||
Consider the following principles.
|
||||
|
||||
* Excluded Middle: `A ⊎ ¬ A`, for all `A`
|
||||
* Double Negation Elimination: `¬ ¬ A → A`, for all `A`
|
||||
* Peirce's Law: `((A → B) → A) → A`, for all `A` and `B`.
|
||||
* Implication as disjunction: `(A → B) → ¬ A ⊎ B`, for all `A` and `B`.
|
||||
* De Morgan: `¬ (¬ A × ¬ B) → A ⊎ B`, for all `A` and `B`.
|
||||
|
||||
Show that each of these implies all the others.
|
||||
|
||||
|
||||
#### Exercise `Stable` (stretch)
|
||||
|
||||
Say that a formula is _stable_ if double negation elimination holds for it.
|
||||
```
|
||||
Stable : Set → Set
|
||||
Stable A = ¬ ¬ A → A
|
||||
```
|
||||
Show that any negated formula is stable, and that the conjunction
|
||||
of two stable formulas is stable.
|
||||
|
||||
|
||||
## Quantifiers
|
||||
|
||||
#### Exercise `∀-distrib-×` (recommended)
|
||||
|
||||
Show that universals distribute over conjunction.
|
||||
```
|
||||
postulate
|
||||
∀-distrib-× : ∀ {A : Set} {B C : A → Set} →
|
||||
(∀ (x : A) → B x × C x) ≃ (∀ (x : A) → B x) × (∀ (x : A) → C x)
|
||||
```
|
||||
Compare this with the result (`→-distrib-×`) in
|
||||
Chapter [Connectives][plfa.Connectives].
|
||||
|
||||
#### Exercise `⊎∀-implies-∀⊎`
|
||||
|
||||
Show that a disjunction of universals implies a universal of disjunctions.
|
||||
```
|
||||
postulate
|
||||
⊎∀-implies-∀⊎ : ∀ {A : Set} { B C : A → Set } →
|
||||
(∀ (x : A) → B x) ⊎ (∀ (x : A) → C x) → ∀ (x : A) → B x ⊎ C x
|
||||
```
|
||||
Does the converse hold? If so, prove; if not, explain why.
|
||||
|
||||
#### Exercise `∃-distrib-⊎` (recommended)
|
||||
|
||||
Show that existentials distribute over disjunction.
|
||||
```
|
||||
postulate
|
||||
∃-distrib-⊎ : ∀ {A : Set} {B C : A → Set} →
|
||||
∃[ x ] (B x ⊎ C x) ≃ (∃[ x ] B x) ⊎ (∃[ x ] C x)
|
||||
```
|
||||
|
||||
#### Exercise `∃×-implies-×∃`
|
||||
|
||||
Show that an existential of conjunctions implies a conjunction of existentials.
|
||||
```
|
||||
postulate
|
||||
∃×-implies-×∃ : ∀ {A : Set} { B C : A → Set } →
|
||||
∃[ x ] (B x × C x) → (∃[ x ] B x) × (∃[ x ] C x)
|
||||
```
|
||||
Does the converse hold? If so, prove; if not, explain why.
|
||||
|
||||
#### Exercise `∃-even-odd`
|
||||
|
||||
How do the proofs become more difficult if we replace `m * 2` and `1 + m * 2`
|
||||
by `2 * m` and `2 * m + 1`? Rewrite the proofs of `∃-even` and `∃-odd` when
|
||||
restated in this way.
|
||||
|
||||
#### Exercise `∃-+-≤`
|
||||
|
||||
Show that `y ≤ z` holds if and only if there exists a `x` such that
|
||||
`x + y ≡ z`.
|
||||
|
||||
#### Exercise `∃¬-implies-¬∀` (recommended)
|
||||
|
||||
Show that existential of a negation implies negation of a universal.
|
||||
```
|
||||
postulate
|
||||
∃¬-implies-¬∀ : ∀ {A : Set} {B : A → Set}
|
||||
→ ∃[ x ] (¬ B x)
|
||||
--------------
|
||||
→ ¬ (∀ x → B x)
|
||||
```
|
||||
Does the converse hold? If so, prove; if not, explain why.
|
||||
|
||||
|
||||
#### Exercise `Bin-isomorphism` (stretch) {#Bin-isomorphism}
|
||||
|
||||
Recall that Exercises
|
||||
[Bin][plfa.Naturals#Bin],
|
||||
[Bin-laws][plfa.Induction#Bin-laws], and
|
||||
[Bin-predicates][plfa.Relations#Bin-predicates]
|
||||
define a datatype of bitstrings representing natural numbers.
|
||||
|
||||
data Bin : Set where
|
||||
nil : Bin
|
||||
x0_ : Bin → Bin
|
||||
x1_ : Bin → Bin
|
||||
|
||||
And ask you to define the following functions and predicates.
|
||||
|
||||
to : ℕ → Bin
|
||||
from : Bin → ℕ
|
||||
Can : Bin → Set
|
||||
|
||||
And to establish the following properties.
|
||||
|
||||
from (to n) ≡ n
|
||||
|
||||
----------
|
||||
Can (to n)
|
||||
|
||||
Can x
|
||||
---------------
|
||||
to (from x) ≡ x
|
||||
|
||||
Using the above, establish that there is an isomorphism between `ℕ` and
|
||||
`∃[ x ](Can x)`.
|
||||
|
||||
|
||||
## Decidable
|
||||
|
||||
#### Exercise `_<?_` (recommended)
|
||||
|
||||
Analogous to the function above, define a function to decide strict inequality.
|
||||
```
|
||||
postulate
|
||||
_<?_ : ∀ (m n : ℕ) → Dec (m < n)
|
||||
```
|
||||
|
||||
#### Exercise `_≡ℕ?_`
|
||||
|
||||
Define a function to decide whether two naturals are equal.
|
||||
```
|
||||
postulate
|
||||
_≡ℕ?_ : ∀ (m n : ℕ) → Dec (m ≡ n)
|
||||
```
|
||||
|
||||
|
||||
#### Exercise `erasure`
|
||||
|
||||
Show that erasure relates corresponding boolean and decidable operations.
|
||||
```
|
||||
postulate
|
||||
∧-× : ∀ {A B : Set} (x : Dec A) (y : Dec B) → ⌊ x ⌋ ∧ ⌊ y ⌋ ≡ ⌊ x ×-dec y ⌋
|
||||
∨-× : ∀ {A B : Set} (x : Dec A) (y : Dec B) → ⌊ x ⌋ ∨ ⌊ y ⌋ ≡ ⌊ x ⊎-dec y ⌋
|
||||
not-¬ : ∀ {A : Set} (x : Dec A) → not ⌊ x ⌋ ≡ ⌊ ¬? x ⌋
|
||||
```
|
||||
|
||||
#### Exercise `iff-erasure` (recommended)
|
||||
|
||||
Give analogues of the `_⇔_` operation from
|
||||
Chapter [Isomorphism][plfa.Isomorphism#iff],
|
||||
operation on booleans and decidables, and also show the corresponding erasure.
|
||||
```
|
||||
postulate
|
||||
_iff_ : Bool → Bool → Bool
|
||||
_⇔-dec_ : ∀ {A B : Set} → Dec A → Dec B → Dec (A ⇔ B)
|
||||
iff-⇔ : ∀ {A B : Set} (x : Dec A) (y : Dec B) → ⌊ x ⌋ iff ⌊ y ⌋ ≡ ⌊ x ⇔-dec y ⌋
|
||||
```
|
||||
|
|
@ -1,374 +0,0 @@
|
|||
---
|
||||
title : "Assignment3: TSPL Assignment 3"
|
||||
layout : page
|
||||
permalink : /TSPL/2018/Assignment3/
|
||||
---
|
||||
|
||||
```
|
||||
module Assignment3 where
|
||||
```
|
||||
|
||||
## YOUR NAME AND EMAIL GOES HERE
|
||||
|
||||
## Introduction
|
||||
|
||||
<!-- This assignment is due **4pm Thursday 1 November** (Week 7). -->
|
||||
|
||||
You must do _all_ the exercises labelled "(recommended)".
|
||||
|
||||
Exercises labelled "(stretch)" are there to provide an extra challenge.
|
||||
You don't need to do all of these, but should attempt at least a few.
|
||||
|
||||
Exercises without a label are optional, and may be done if you want
|
||||
some extra practice.
|
||||
|
||||
<!-- Submit your homework using the "submit" command. -->
|
||||
Please ensure your files execute correctly under Agda!
|
||||
|
||||
## Imports
|
||||
|
||||
```
|
||||
import Relation.Binary.PropositionalEquality as Eq
|
||||
open Eq using (_≡_; refl; cong; sym)
|
||||
open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; _≡⟨_⟩_; _∎)
|
||||
open import Data.Bool.Base using (Bool; true; false; T; _∧_; _∨_; not)
|
||||
open import Data.Nat using (ℕ; zero; suc; _+_; _*_; _∸_; _≤_; s≤s; z≤n)
|
||||
open import Data.Nat.Properties using
|
||||
(+-assoc; +-identityˡ; +-identityʳ; *-assoc; *-identityˡ; *-identityʳ)
|
||||
open import Relation.Nullary using (¬_; Dec; yes; no)
|
||||
open import Data.Product using (_×_; ∃; ∃-syntax) renaming (_,_ to ⟨_,_⟩)
|
||||
open import Data.Empty using (⊥; ⊥-elim)
|
||||
open import Function using (_∘_)
|
||||
open import Algebra.Structures using (IsMonoid)
|
||||
open import Level using (Level)
|
||||
open import Relation.Unary using (Decidable)
|
||||
open import plfa.part1.Relations using (_<_; z<s; s<s)
|
||||
open import plfa.part1.Isomorphism using (_≃_; ≃-sym; ≃-trans; _≲_; extensionality)
|
||||
open plfa.part1.Isomorphism.≃-Reasoning
|
||||
open import plfa.part1.Lists using (List; []; _∷_; [_]; [_,_]; [_,_,_]; [_,_,_,_];
|
||||
_++_; reverse; map; foldr; sum; All; Any; here; there; _∈_)
|
||||
open import plfa.part2.Lambda hiding (ƛ′_⇒_; case′_[zero⇒_|suc_⇒_]; μ′_⇒_; plus′)
|
||||
open import plfa.part2.Properties hiding (value?; unstuck; preserves; wttdgs)
|
||||
```
|
||||
|
||||
#### Exercise `reverse-++-commute` (recommended)
|
||||
|
||||
Show that the reverse of one list appended to another is the
|
||||
reverse of the second appended to the reverse of the first.
|
||||
```
|
||||
postulate
|
||||
reverse-++-commute : ∀ {A : Set} {xs ys : List A}
|
||||
→ reverse (xs ++ ys) ≡ reverse ys ++ reverse xs
|
||||
```
|
||||
|
||||
#### Exercise `reverse-involutive` (recommended)
|
||||
|
||||
A function is an _involution_ if when applied twice it acts
|
||||
as the identity function. Show that reverse is an involution.
|
||||
```
|
||||
postulate
|
||||
reverse-involutive : ∀ {A : Set} {xs : List A}
|
||||
→ reverse (reverse xs) ≡ xs
|
||||
```
|
||||
|
||||
#### Exercise `map-compose`
|
||||
|
||||
Prove that the map of a composition is equal to the composition of two maps.
|
||||
```
|
||||
postulate
|
||||
map-compose : ∀ {A B C : Set} {f : A → B} {g : B → C}
|
||||
→ map (g ∘ f) ≡ map g ∘ map f
|
||||
```
|
||||
The last step of the proof requires extensionality.
|
||||
|
||||
#### Exercise `map-++-commute`
|
||||
|
||||
Prove the following relationship between map and append.
|
||||
```
|
||||
postulate
|
||||
map-++-commute : ∀ {A B : Set} {f : A → B} {xs ys : List A}
|
||||
→ map f (xs ++ ys) ≡ map f xs ++ map f ys
|
||||
```
|
||||
|
||||
#### Exercise `map-Tree`
|
||||
|
||||
Define a type of trees with leaves of type `A` and internal
|
||||
nodes of type `B`.
|
||||
```
|
||||
data Tree (A B : Set) : Set where
|
||||
leaf : A → Tree A B
|
||||
node : Tree A B → B → Tree A B → Tree A B
|
||||
```
|
||||
Define a suitable map operator over trees.
|
||||
```
|
||||
postulate
|
||||
map-Tree : ∀ {A B C D : Set}
|
||||
→ (A → C) → (B → D) → Tree A B → Tree C D
|
||||
```
|
||||
|
||||
#### Exercise `product` (recommended)
|
||||
|
||||
Use fold to define a function to find the product of a list of numbers.
|
||||
For example,
|
||||
|
||||
product [ 1 , 2 , 3 , 4 ] ≡ 24
|
||||
|
||||
#### Exercise `foldr-++` (recommended)
|
||||
|
||||
Show that fold and append are related as follows.
|
||||
```
|
||||
postulate
|
||||
foldr-++ : ∀ {A B : Set} (_⊗_ : A → B → B) (e : B) (xs ys : List A) →
|
||||
foldr _⊗_ e (xs ++ ys) ≡ foldr _⊗_ (foldr _⊗_ e ys) xs
|
||||
```
|
||||
|
||||
|
||||
#### Exercise `map-is-foldr`
|
||||
|
||||
Show that map can be defined using fold.
|
||||
```
|
||||
postulate
|
||||
map-is-foldr : ∀ {A B : Set} {f : A → B} →
|
||||
map f ≡ foldr (λ x xs → f x ∷ xs) []
|
||||
```
|
||||
This requires extensionality.
|
||||
|
||||
#### Exercise `fold-Tree`
|
||||
|
||||
Define a suitable fold function for the type of trees given earlier.
|
||||
```
|
||||
postulate
|
||||
fold-Tree : ∀ {A B C : Set}
|
||||
→ (A → C) → (C → B → C → C) → Tree A B → C
|
||||
```
|
||||
|
||||
#### Exercise `map-is-fold-Tree`
|
||||
|
||||
Demonstrate an analogue of `map-is-foldr` for the type of trees.
|
||||
|
||||
#### Exercise `sum-downFrom` (stretch)
|
||||
|
||||
Define a function that counts down as follows.
|
||||
```
|
||||
downFrom : ℕ → List ℕ
|
||||
downFrom zero = []
|
||||
downFrom (suc n) = n ∷ downFrom n
|
||||
```
|
||||
For example,
|
||||
```
|
||||
_ : downFrom 3 ≡ [ 2 , 1 , 0 ]
|
||||
_ = refl
|
||||
```
|
||||
Prove that the sum of the numbers `(n - 1) + ⋯ + 0` is
|
||||
equal to `n * (n ∸ 1) / 2`.
|
||||
```
|
||||
postulate
|
||||
sum-downFrom : ∀ (n : ℕ)
|
||||
→ sum (downFrom n) * 2 ≡ n * (n ∸ 1)
|
||||
```
|
||||
|
||||
|
||||
#### Exercise `foldl`
|
||||
|
||||
Define a function `foldl` which is analogous to `foldr`, but where
|
||||
operations associate to the left rather than the right. For example,
|
||||
|
||||
foldr _⊗_ e [ x , y , z ] = x ⊗ (y ⊗ (z ⊗ e))
|
||||
foldl _⊗_ e [ x , y , z ] = ((e ⊗ x) ⊗ y) ⊗ z
|
||||
|
||||
|
||||
#### Exercise `foldr-monoid-foldl`
|
||||
|
||||
Show that if `_⊕_` and `e` form a monoid, then `foldr _⊗_ e` and
|
||||
`foldl _⊗_ e` always compute the same result.
|
||||
|
||||
|
||||
#### Exercise `Any-++-⇔` (recommended)
|
||||
|
||||
Prove a result similar to `All-++-↔`, but with `Any` in place of `All`, and a suitable
|
||||
replacement for `_×_`. As a consequence, demonstrate an equivalence relating
|
||||
`_∈_` and `_++_`.
|
||||
|
||||
|
||||
#### Exercise `All-++-≃` (stretch)
|
||||
|
||||
Show that the equivalence `All-++-⇔` can be extended to an isomorphism.
|
||||
|
||||
|
||||
#### Exercise `¬Any≃All¬` (stretch)
|
||||
|
||||
First generalise composition to arbitrary levels, using
|
||||
[universe polymorphism][plfa.Equality#unipoly].
|
||||
```
|
||||
_∘′_ : ∀ {ℓ₁ ℓ₂ ℓ₃ : Level} {A : Set ℓ₁} {B : Set ℓ₂} {C : Set ℓ₃}
|
||||
→ (B → C) → (A → B) → A → C
|
||||
(g ∘′ f) x = g (f x)
|
||||
```
|
||||
|
||||
Show that `Any` and `All` satisfy a version of De Morgan's Law.
|
||||
```
|
||||
postulate
|
||||
¬Any≃All¬ : ∀ {A : Set} (P : A → Set) (xs : List A)
|
||||
→ (¬_ ∘′ Any P) xs ≃ All (¬_ ∘′ P) xs
|
||||
```
|
||||
|
||||
Do we also have the following?
|
||||
```
|
||||
postulate
|
||||
¬All≃Any¬ : ∀ {A : Set} (P : A → Set) (xs : List A)
|
||||
→ (¬_ ∘′ All P) xs ≃ Any (¬_ ∘′ P) xs
|
||||
```
|
||||
If so, prove; if not, explain why.
|
||||
|
||||
|
||||
#### Exercise `any?` (stretch)
|
||||
|
||||
Just as `All` has analogues `all` and `all?` which determine whether a
|
||||
predicate holds for every element of a list, so does `Any` have
|
||||
analogues `any` and `any?` which determine whether a predicates holds
|
||||
for some element of a list. Give their definitions.
|
||||
|
||||
|
||||
#### Exercise `filter?` (stretch)
|
||||
|
||||
Define the following variant of the traditional `filter` function on lists,
|
||||
which given a list and a decidable predicate returns all elements of the
|
||||
list satisfying the predicate.
|
||||
```
|
||||
postulate
|
||||
filter? : ∀ {A : Set} {P : A → Set}
|
||||
→ (P? : Decidable P) → List A → ∃[ ys ]( All P ys )
|
||||
```
|
||||
|
||||
|
||||
## Lambda
|
||||
|
||||
#### Exercise `mul` (recommended)
|
||||
|
||||
Write out the definition of a lambda term that multiplies
|
||||
two natural numbers.
|
||||
|
||||
|
||||
#### Exercise `primed` (stretch)
|
||||
|
||||
We can make examples with lambda terms slightly easier to write
|
||||
by adding the following definitions.
|
||||
```
|
||||
ƛ′_⇒_ : Term → Term → Term
|
||||
ƛ′ (` x) ⇒ N = ƛ x ⇒ N
|
||||
ƛ′ _ ⇒ _ = ⊥-elim impossible
|
||||
where postulate impossible : ⊥
|
||||
|
||||
case′_[zero⇒_|suc_⇒_] : Term → Term → Term → Term → Term
|
||||
case′ L [zero⇒ M |suc (` x) ⇒ N ] = case L [zero⇒ M |suc x ⇒ N ]
|
||||
case′ _ [zero⇒ _ |suc _ ⇒ _ ] = ⊥-elim impossible
|
||||
where postulate impossible : ⊥
|
||||
|
||||
μ′_⇒_ : Term → Term → Term
|
||||
μ′ (` x) ⇒ N = μ x ⇒ N
|
||||
μ′ _ ⇒ _ = ⊥-elim impossible
|
||||
where postulate impossible : ⊥
|
||||
```
|
||||
The definition of `plus` can now be written as follows.
|
||||
```
|
||||
plus′ : Term
|
||||
plus′ = μ′ + ⇒ ƛ′ m ⇒ ƛ′ n ⇒
|
||||
case′ m
|
||||
[zero⇒ n
|
||||
|suc m ⇒ `suc (+ · m · n) ]
|
||||
where
|
||||
+ = ` "+"
|
||||
m = ` "m"
|
||||
n = ` "n"
|
||||
```
|
||||
Write out the definition of multiplication in the same style.
|
||||
|
||||
#### Exercise `_[_:=_]′` (stretch)
|
||||
|
||||
The definition of substitution above has three clauses (`ƛ`, `case`,
|
||||
and `μ`) that invoke a with clause to deal with bound variables.
|
||||
Rewrite the definition to factor the common part of these three
|
||||
clauses into a single function, defined by mutual recursion with
|
||||
substitution.
|
||||
|
||||
|
||||
#### Exercise `—↠≃—↠′`
|
||||
|
||||
Show that the two notions of reflexive and transitive closure
|
||||
above are isomorphic.
|
||||
|
||||
|
||||
#### Exercise `plus-example`
|
||||
|
||||
Write out the reduction sequence demonstrating that one plus one is two.
|
||||
|
||||
|
||||
#### Exercise `mul-type` (recommended)
|
||||
|
||||
Using the term `mul` you defined earlier, write out the derivation
|
||||
showing that it is well-typed.
|
||||
|
||||
|
||||
## Properties
|
||||
|
||||
|
||||
#### Exercise `Progress-≃`
|
||||
|
||||
Show that `Progress M` is isomorphic to `Value M ⊎ ∃[ N ](M —→ N)`.
|
||||
|
||||
|
||||
#### Exercise `progress′`
|
||||
|
||||
Write out the proof of `progress′` in full, and compare it to the
|
||||
proof of `progress` above.
|
||||
|
||||
|
||||
#### Exercise `value?`
|
||||
|
||||
Combine `progress` and `—→¬V` to write a program that decides
|
||||
whether a well-typed term is a value.
|
||||
```
|
||||
postulate
|
||||
value? : ∀ {A M} → ∅ ⊢ M ⦂ A → Dec (Value M)
|
||||
```
|
||||
|
||||
|
||||
#### Exercise `subst′` (stretch)
|
||||
|
||||
Rewrite `subst` to work with the modified definition `_[_:=_]′`
|
||||
from the exercise in the previous chapter. As before, this
|
||||
should factor dealing with bound variables into a single function,
|
||||
defined by mutual recursion with the proof that substitution
|
||||
preserves types.
|
||||
|
||||
|
||||
#### Exercise `mul-eval` (recommended)
|
||||
|
||||
Using the evaluator, confirm that two times two is four.
|
||||
|
||||
|
||||
#### Exercise: `progress-preservation`
|
||||
|
||||
Without peeking at their statements above, write down the progress
|
||||
and preservation theorems for the simply typed lambda-calculus.
|
||||
|
||||
|
||||
#### Exercise `subject-expansion`
|
||||
|
||||
We say that `M` _reduces_ to `N` if `M —→ N`,
|
||||
and conversely that `M` _expands_ to `N` if `N —→ M`.
|
||||
The preservation property is sometimes called _subject reduction_.
|
||||
Its opposite is _subject expansion_, which holds if
|
||||
`M —→ N` and `∅ ⊢ N ⦂ A` imply `∅ ⊢ M ⦂ A`.
|
||||
Find two counter-examples to subject expansion, one
|
||||
with case expressions and one not involving case expressions.
|
||||
|
||||
|
||||
#### Exercise `stuck`
|
||||
|
||||
Give an example of an ill-typed term that does get stuck.
|
||||
|
||||
|
||||
#### Exercise `unstuck` (recommended)
|
||||
|
||||
Provide proofs of the three postulates, `unstuck`, `preserves`, and `wttdgs` above.
|
||||
File diff suppressed because it is too large
Load diff
|
|
@ -1,678 +0,0 @@
|
|||
---
|
||||
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.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)
|
||||
```
|
||||
Binary file not shown.
|
|
@ -1,122 +0,0 @@
|
|||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||
% 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:
|
||||
Binary file not shown.
|
|
@ -1,421 +0,0 @@
|
|||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||
%
|
||||
% 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}
|
||||
Binary file not shown.
|
|
@ -1,407 +0,0 @@
|
|||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||
%
|
||||
% 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}
|
||||
File diff suppressed because it is too large
Load diff
|
|
@ -1,3 +0,0 @@
|
|||
name: tspl2018
|
||||
depend: standard-library plfa
|
||||
include: .
|
||||
|
|
@ -1,118 +0,0 @@
|
|||
---
|
||||
title : "TSPL: Course notes"
|
||||
layout : page
|
||||
permalink : /TSPL/2018/
|
||||
---
|
||||
|
||||
## Staff
|
||||
|
||||
* **Instructor**
|
||||
[Philip Wadler](https://homepages.inf.ed.ac.uk/wadler)
|
||||
* **Teaching assistants**
|
||||
- [Wen Kokke](mailto:wen.kokke@ed.ac.uk)
|
||||
- [Chad Nester](mailto:chad.nester@gmail.com)
|
||||
|
||||
## Lectures
|
||||
|
||||
Lectures take place Monday, Wednesday, and Friday in AT 7.02. (Moved from AT 5.07 and AT 4.12.)
|
||||
* **9.00--9.50am** Lecture
|
||||
* **10.00--10.50am** Tutorial
|
||||
|
||||
<table>
|
||||
<tr>
|
||||
<th>Week</th>
|
||||
<th>Mon</th>
|
||||
<th>Wed</th>
|
||||
<th>Fri</th>
|
||||
</tr>
|
||||
<tr>
|
||||
<td>1</td>
|
||||
<td><b>17 Sep</b> <a href="{{ site.baseurl }}/Naturals/">Naturals</a></td>
|
||||
<td><b>19 Sep</b> <a href="{{ site.baseurl }}/Induction/">Induction</a></td>
|
||||
<td><b>21 Sep</b> <a href="{{ site.baseurl }}/Induction/">Induction</a></td>
|
||||
</tr>
|
||||
<tr>
|
||||
<td>2</td>
|
||||
<td><b>24 Sep</b> <a href="{{ site.baseurl }}/Relations/">Relations</a> (Chad)</td>
|
||||
<td><b>26 Sep</b> <a href="{{ site.baseurl }}/Relations/">Relations</a> (Chad)</td>
|
||||
<td><b>28 Sep</b> (no class)</td>
|
||||
</tr>
|
||||
<tr>
|
||||
<td>3</td>
|
||||
<td><b>1 Oct</b> <a href="{{ site.baseurl }}/Equality/">Equality</a> & <a href="{{ site.baseurl }}/Isomorphism/">Isomorphism</a></td>
|
||||
<td><b>3 Oct</b> <a href="{{ site.baseurl }}/Connectives/">Connectives</a></td>
|
||||
<td><b>5 Oct</b> <a href="{{ site.baseurl }}/Negation/">Negation</a></td>
|
||||
</tr>
|
||||
<tr>
|
||||
<td>4</td>
|
||||
<td><b>8 Oct</b> <a href="{{ site.baseurl }}/Quantifiers/">Quantifiers</a></td>
|
||||
<td><b>10 Oct</b> <a href="{{ site.baseurl }}/Decidable/">Decidable</a></td>
|
||||
<td><b>12 Oct</b> (tutorial only)</td>
|
||||
</tr>
|
||||
<tr>
|
||||
<td>5</td>
|
||||
<td><b>15 Oct</b> <a href="{{ site.baseurl }}/Lists/">Lists</a></td>
|
||||
<td><b>17 Oct</b> (tutorial only)</td>
|
||||
<td><b>19 Oct</b> <a href="{{ site.baseurl }}/Lists/">Lists</a></td>
|
||||
</tr>
|
||||
<tr>
|
||||
<td>6</td>
|
||||
<td><b>22 Oct</b> <a href="{{ site.baseurl }}/Lambda/">Lambda</a></td>
|
||||
<td><b>24 Oct</b> (no class)</td>
|
||||
<td><b>26 Oct</b> <a href="{{ site.baseurl }}/Properties/">Properties</a></td>
|
||||
</tr>
|
||||
<tr>
|
||||
<td>7</td>
|
||||
<td><b>29 Oct</b> <a href="{{ site.baseurl }}/DeBruijn/">DeBruijn</a></td>
|
||||
<td><b>31 Oct</b> <a href="{{ site.baseurl }}/More/">More</a></td>
|
||||
<td><b>2 Nov</b> <a href="{{ site.baseurl }}/Inference/">Inference</a></td>
|
||||
</tr>
|
||||
<tr>
|
||||
<td>8</td>
|
||||
<td><b>5 Nov</b> (no class)</td>
|
||||
<td><b>7 Nov</b> (tutorial only)</td>
|
||||
<td><b>9 Nov</b> <a href="{{ site.baseurl }}/Untyped/">Untyped</a></td>
|
||||
</tr>
|
||||
<tr>
|
||||
<td>9</td>
|
||||
<td><b>12 Nov</b> (no class)</td>
|
||||
<td><b>14 Nov</b> (tutorial only)</td>
|
||||
<td><b>16 Nov</b> (no class)</td>
|
||||
</tr>
|
||||
<tr>
|
||||
<td>10</td>
|
||||
<td><b>19 Nov</b> (no class)</td>
|
||||
<td><b>21 Nov</b> Propositions as Types</td>
|
||||
<td><b>23 Nov</b> (no class)</td>
|
||||
</tr>
|
||||
<tr>
|
||||
<td>11</td>
|
||||
<td><b>26 Nov</b> (no class)</td>
|
||||
<td><b>28 Nov</b> Quantitative (Wen)</td>
|
||||
<td><b>30 Nov</b> (mock exam)</td>
|
||||
</tr>
|
||||
</table>
|
||||
|
||||
## Assignments
|
||||
|
||||
For instructions on how to set up Agda for PLFA see [Getting Started]({{ site.baseurl }}/GettingStarted/).
|
||||
|
||||
* [Assignment 1]({{ site.baseurl }}/TSPL/2018/Assignment1/) cw1 due 4pm Thursday 4 October (Week 3)
|
||||
* [Assignment 2]({{ site.baseurl }}/TSPL/2018/Assignment2/) cw2 due 4pm Thursday 18 October (Week 5)
|
||||
* [Assignment 3]({{ site.baseurl }}/TSPL/2018/Assignment3/) cw3 due 4pm Thursday 1 November (Week 7)
|
||||
* [Assignment 4]({{ site.baseurl }}/TSPL/2018/Assignment4/) cw4 due 4pm Thursday 15 November (Week 9)
|
||||
* [Assignment 5]({{ site.baseurl }}/courses/tspl/2018/Mock1.pdf) cw5 due 4pm Thursday 22 November (Week 10)
|
||||
<br />
|
||||
Use file [Exam]({{ site.baseurl }}/TSPL/2018/Exam/). Despite the rubric, do **all three questions**.
|
||||
|
||||
|
||||
Assignments are submitted by running
|
||||
``` bash
|
||||
submit tspl cwN AssignmentN.lagda
|
||||
```
|
||||
where N is the number of the assignment.
|
||||
|
||||
## Mock exam
|
||||
|
||||
Here is the text of the [second mock]({{ site.baseurl }}/courses/tspl/2018/Mock2.pdf)
|
||||
and the exam [instructions]({{ site.baseurl }}/courses/tspl/2018/Instructions.pdf).
|
||||
Loading…
Add table
Reference in a new issue