Merge branch 'dev' of https://github.com/plfa/plfa.github.io into dev
This commit is contained in:
Jeremy Siek
commit
e890fec7ab
12 changed files with 2290 additions and 15 deletions
|
|
@ -10,6 +10,12 @@ next : /Negation/
|
|||
module plfa.Connectives where
|
||||
\end{code}
|
||||
|
||||
<!-- The ⊥ ⊎ A ≅ A exercise requires a (inj₁ ()) pattern,
|
||||
which the reader will not have seen. Restore this
|
||||
exercise, and possibly also associativity? Take the
|
||||
exercises from the final sections on distributivity
|
||||
and exponentials? -->
|
||||
|
||||
This chapter introduces the basic logical connectives, by observing a
|
||||
correspondence between connectives of logic and data types, a
|
||||
principle known as _Propositions as Types_:
|
||||
|
|
|
|||
|
|
@ -651,9 +651,10 @@ What does the following term step to?
|
|||
2. `` (ƛ "x" ⇒ ` "x") · (ƛ "x" ⇒ ` "x") ``
|
||||
3. `` (ƛ "x" ⇒ ` "x") · (ƛ "x" ⇒ ` "x") · (ƛ "x" ⇒ ` "x") ``
|
||||
|
||||
What does the following term step to? (Where `two` and `sucᶜ` are as defined above.)
|
||||
What does the following term step to? (Where `twoᶜ` and `sucᶜ` are as
|
||||
defined above.)
|
||||
|
||||
two · sucᶜ · `zero —→ ???
|
||||
twoᶜ · sucᶜ · `zero —→ ???
|
||||
|
||||
1. `` sucᶜ · (sucᶜ · `zero) ``
|
||||
2. `` (ƛ "z" ⇒ sucᶜ · (sucᶜ · ` "z")) · `zero ``
|
||||
|
|
@ -668,7 +669,7 @@ the reflexive and transitive closure `—↠` of the step relation `—→`.
|
|||
|
||||
We define reflexive and transitive closure as a sequence of zero or
|
||||
more steps of the underlying relation, along lines similar to that for
|
||||
reasoning about chains of equalities
|
||||
reasoning about chains of equalities in
|
||||
Chapter [Equality][plfa.Equality]:
|
||||
\begin{code}
|
||||
infix 2 _—↠_
|
||||
|
|
|
|||
|
|
@ -888,7 +888,7 @@ possible evidence for `3 ≡ 0`, `3 ≡ 1`, `3 ≡ 0`, `3 ≡ 2`, and
|
|||
## All and append
|
||||
|
||||
A predicate holds for every element of one list appended to another if and
|
||||
only if it holds for every element of each list:
|
||||
only if it holds for every element of both lists:
|
||||
\begin{code}
|
||||
All-++-⇔ : ∀ {A : Set} {P : A → Set} (xs ys : List A) →
|
||||
All P (xs ++ ys) ⇔ (All P xs × All P ys)
|
||||
|
|
@ -913,7 +913,7 @@ All-++-⇔ xs ys =
|
|||
|
||||
#### Exercise `Any-++-⇔` (recommended)
|
||||
|
||||
Prove a result similar to `All-++-↔`, but with `Any` in place of `All`, and a suitable
|
||||
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 `_++_`.
|
||||
|
||||
|
|
@ -1005,10 +1005,28 @@ for some element of a list. Give their definitions.
|
|||
\end{code}
|
||||
|
||||
|
||||
#### Exercise `All-∀`
|
||||
|
||||
Show that `All P xs` is isomorphic to `∀ {x} → x ∈ xs → P x`.
|
||||
|
||||
\begin{code}
|
||||
-- You code goes here
|
||||
\end{code}
|
||||
|
||||
|
||||
#### Exercise `Any-∃`
|
||||
|
||||
Show that `Any P xs` is isomorphic to `∃[ x ∈ xs ] P x`.
|
||||
|
||||
\begin{code}
|
||||
-- You code goes here
|
||||
\end{code}
|
||||
|
||||
|
||||
#### 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
|
||||
which given a decidable predicate and a list returns all elements of the
|
||||
list satisfying the predicate:
|
||||
\begin{code}
|
||||
postulate
|
||||
|
|
|
|||
|
|
@ -16,7 +16,7 @@ and classical logic.
|
|||
## Imports
|
||||
|
||||
\begin{code}
|
||||
open import Relation.Binary.PropositionalEquality using (_≡_)
|
||||
open import Relation.Binary.PropositionalEquality using (_≡_; refl)
|
||||
open import Data.Nat using (ℕ; zero; suc)
|
||||
open import Data.Empty using (⊥; ⊥-elim)
|
||||
open import Data.Sum using (_⊎_; inj₁; inj₂)
|
||||
|
|
@ -102,7 +102,6 @@ We cannot show that `¬ ¬ A` implies `A`, but we can show that
|
|||
-------
|
||||
→ ¬ A
|
||||
¬¬¬-elim ¬¬¬x = λ x → ¬¬¬x (¬¬-intro x)
|
||||
-- ¬¬¬-elim ¬¬¬x x = ¬¬¬x (¬¬-intro x)
|
||||
\end{code}
|
||||
Let `¬¬¬x` be evidence of `¬ ¬ ¬ A`. We will show that assuming
|
||||
`A` leads to a contradiction, and hence `¬ A` must hold.
|
||||
|
|
|
|||
|
|
@ -103,6 +103,19 @@ postulate
|
|||
Does the converse hold? If so, prove; if not, explain why.
|
||||
|
||||
|
||||
#### Exercise `∀-×`
|
||||
|
||||
Consider the following type.
|
||||
\begin{code}
|
||||
data Tri : Set where
|
||||
aa : Tri
|
||||
bb : Tri
|
||||
cc : Tri
|
||||
\end{code}
|
||||
Let `B` be a type indexed by `Tri`, that is `B : Tri → Set`.
|
||||
Show that `∀ (x : Tri) → B x` is isomorphic to `B aa × B bb × B cc`.
|
||||
|
||||
|
||||
## Existentials
|
||||
|
||||
Given a variable `x` of type `A` and a proposition `B x` which
|
||||
|
|
@ -241,6 +254,11 @@ postulate
|
|||
\end{code}
|
||||
Does the converse hold? If so, prove; if not, explain why.
|
||||
|
||||
#### Exercise `∃-⊎`
|
||||
|
||||
Let `Tri` and `B` be as in Exercise `∀-×`.
|
||||
Show that `∃[ x ] B x` is isomorphic to `B aa ⊎ B bb ⊎ B cc`.
|
||||
|
||||
|
||||
## An existential example
|
||||
|
||||
|
|
|
|||
|
|
@ -625,7 +625,7 @@ 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
|
||||
using the relation between strict inequality and inequality and
|
||||
the fact that inequality is transitive.
|
||||
|
||||
\begin{code}
|
||||
|
|
|
|||
|
|
@ -1,5 +1,5 @@
|
|||
---
|
||||
title : "Assignment1: PUC Assignment 1"
|
||||
title : "Assignment1: TSPL Assignment 1"
|
||||
layout : page
|
||||
permalink : /Assignment1/
|
||||
---
|
||||
|
|
|
|||
315
tspl/PUC-Assignment1.lagda
Normal file
315
tspl/PUC-Assignment1.lagda
Normal file
|
|
@ -0,0 +1,315 @@
|
|||
---
|
||||
title : "PUC-Assignment1: PUC Assignment 1"
|
||||
layout : page
|
||||
permalink : /PUC-Assignment1/
|
||||
---
|
||||
|
||||
\begin{code}
|
||||
module PUC-Assignment1 where
|
||||
\end{code}
|
||||
|
||||
## 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
|
||||
|
||||
\begin{code}
|
||||
import Relation.Binary.PropositionalEquality as Eq
|
||||
open Eq using (_≡_; refl; cong; sym)
|
||||
open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; _≡⟨_⟩_; _∎)
|
||||
open import Data.Nat using (ℕ; zero; suc; _+_; _*_; _∸_; _≤_; z≤n; s≤s)
|
||||
open import Data.Nat.Properties using (+-assoc; +-identityʳ; +-suc; +-comm;
|
||||
≤-refl; ≤-trans; ≤-antisym; ≤-total; +-monoʳ-≤; +-monoˡ-≤; +-mono-≤)
|
||||
open import plfa.Relations using (_<_; z<s; s<s; zero; suc; even; odd)
|
||||
\end{code}
|
||||
|
||||
## Naturals
|
||||
|
||||
#### Exercise `seven` {#seven}
|
||||
|
||||
Write out `7` in longhand.
|
||||
|
||||
|
||||
#### Exercise `+-example` {#plus-example}
|
||||
|
||||
Compute `3 + 4`, writing out your reasoning as a chain of equations.
|
||||
|
||||
|
||||
#### Exercise `*-example` {#times-example}
|
||||
|
||||
Compute `3 * 4`, writing out your reasoning as a chain of equations.
|
||||
|
||||
|
||||
#### Exercise `_^_` (recommended) {#power}
|
||||
|
||||
Define exponentiation, which is given by the following equations.
|
||||
|
||||
n ^ 0 = 1
|
||||
n ^ (1 + m) = n * (n ^ m)
|
||||
|
||||
Check that `3 ^ 4` is `81`.
|
||||
|
||||
|
||||
#### Exercise `∸-examples` (recommended) {#monus-examples}
|
||||
|
||||
Compute `5 ∸ 3` and `3 ∸ 5`, writing out your reasoning as a chain of equations.
|
||||
|
||||
|
||||
#### Exercise `Bin` (stretch) {#Bin}
|
||||
|
||||
A more efficient representation of natural numbers uses a binary
|
||||
rather than a unary system. We represent a number as a bitstring.
|
||||
\begin{code}
|
||||
data Bin : Set where
|
||||
nil : Bin
|
||||
x0_ : Bin → Bin
|
||||
x1_ : Bin → Bin
|
||||
\end{code}
|
||||
For instance, the bitstring
|
||||
|
||||
1011
|
||||
|
||||
standing for the number eleven is encoded, right to left, as
|
||||
|
||||
x1 x1 x0 x1 nil
|
||||
|
||||
Representations are not unique due to leading zeros.
|
||||
Hence, eleven is also represented by `001011`, encoded as
|
||||
|
||||
x1 x1 x0 x1 x0 x0 nil
|
||||
|
||||
Define a function
|
||||
|
||||
inc : Bin → Bin
|
||||
|
||||
that converts a bitstring to the bitstring for the next higher
|
||||
number. For example, since `1100` encodes twelve, we should have
|
||||
|
||||
inc (x1 x1 x0 x1 nil) ≡ x0 x0 x1 x1 nil
|
||||
|
||||
Confirm that this gives the correct answer for the bitstrings
|
||||
encoding zero through four.
|
||||
|
||||
Using the above, define a pair of functions to convert
|
||||
between the two representations.
|
||||
|
||||
to : ℕ → Bin
|
||||
from : Bin → ℕ
|
||||
|
||||
For the former, choose the bitstring to have no leading zeros if it
|
||||
represents a positive natural, and represent zero by `x0 nil`.
|
||||
Confirm that these both give the correct answer for zero through four.
|
||||
|
||||
## Induction
|
||||
|
||||
#### Exercise `operators` {#operators}
|
||||
|
||||
Give another example of a pair of operators that have an identity
|
||||
and are associative, commutative, and distribute over one another.
|
||||
|
||||
Give an example of an operator that has an identity and is
|
||||
associative but is not commutative.
|
||||
|
||||
|
||||
#### Exercise `finite-+-assoc` (stretch) {#finite-plus-assoc}
|
||||
|
||||
Write out what is known about associativity of addition on each of the first four
|
||||
days using a finite story of creation, as
|
||||
[earlier][plfa.Naturals#finite-creation]
|
||||
|
||||
|
||||
#### Exercise `+-swap` (recommended) {#plus-swap}
|
||||
|
||||
Show
|
||||
|
||||
m + (n + p) ≡ n + (m + p)
|
||||
|
||||
for all naturals `m`, `n`, and `p`. No induction is needed,
|
||||
just apply the previous results which show addition
|
||||
is associative and commutative. You may need to use
|
||||
the following function from the standard library:
|
||||
|
||||
sym : ∀ {m n : ℕ} → m ≡ n → n ≡ m
|
||||
|
||||
|
||||
#### Exercise `*-distrib-+` (recommended) {#times-distrib-plus}
|
||||
|
||||
Show multiplication distributes over addition, that is,
|
||||
|
||||
(m + n) * p ≡ m * p + n * p
|
||||
|
||||
for all naturals `m`, `n`, and `p`.
|
||||
|
||||
#### Exercise `*-assoc` (recommended) {#times-assoc}
|
||||
|
||||
Show multiplication is associative, that is,
|
||||
|
||||
(m * n) * p ≡ m * (n * p)
|
||||
|
||||
for all naturals `m`, `n`, and `p`.
|
||||
|
||||
#### Exercise `*-comm` {#times-comm}
|
||||
|
||||
Show multiplication is commutative, that is,
|
||||
|
||||
m * n ≡ n * m
|
||||
|
||||
for all naturals `m` and `n`. As with commutativity of addition,
|
||||
you will need to formulate and prove suitable lemmas.
|
||||
|
||||
#### Exercise `0∸n≡0` {#zero-monus}
|
||||
|
||||
Show
|
||||
|
||||
zero ∸ n ≡ zero
|
||||
|
||||
for all naturals `n`. Did your proof require induction?
|
||||
|
||||
#### Exercise `∸-+-assoc` {#monus-plus-assoc}
|
||||
|
||||
Show that monus associates with addition, that is,
|
||||
|
||||
m ∸ n ∸ p ≡ m ∸ (n + p)
|
||||
|
||||
for all naturals `m`, `n`, and `p`.
|
||||
|
||||
#### Exercise `Bin-laws` (stretch) {#Bin-laws}
|
||||
|
||||
Recall that
|
||||
Exercise [Bin][plfa.Naturals#Bin]
|
||||
defines a datatype `Bin` of bitstrings representing natural numbers
|
||||
and asks you to define functions
|
||||
|
||||
inc : Bin → Bin
|
||||
to : ℕ → Bin
|
||||
from : Bin → ℕ
|
||||
|
||||
Consider the following laws, where `n` ranges over naturals and `x`
|
||||
over bitstrings.
|
||||
|
||||
from (inc x) ≡ suc (from x)
|
||||
to (from n) ≡ n
|
||||
from (to x) ≡ x
|
||||
|
||||
For each law: if it holds, prove; if not, give a counterexample.
|
||||
|
||||
|
||||
## Relations
|
||||
|
||||
|
||||
#### Exercise `orderings` {#orderings}
|
||||
|
||||
Give an example of a preorder that is not a partial order.
|
||||
|
||||
Give an example of a partial order that is not a preorder.
|
||||
|
||||
|
||||
#### Exercise `≤-antisym-cases` {#leq-antisym-cases}
|
||||
|
||||
The above proof omits cases where one argument is `z≤n` and one
|
||||
argument is `s≤s`. Why is it ok to omit them?
|
||||
|
||||
|
||||
#### Exercise `*-mono-≤` (stretch)
|
||||
|
||||
Show that multiplication is monotonic with regard to inequality.
|
||||
|
||||
|
||||
#### Exercise `<-trans` (recommended) {#less-trans}
|
||||
|
||||
Show that strict inequality is transitive.
|
||||
|
||||
#### Exercise `trichotomy` {#trichotomy}
|
||||
|
||||
Show that strict inequality satisfies a weak version of trichotomy, in
|
||||
the sense that for any `m` and `n` that one of the following holds:
|
||||
* `m < n`,
|
||||
* `m ≡ n`, or
|
||||
* `m > n`
|
||||
Define `m > n` to be the same as `n < m`.
|
||||
You will need a suitable data declaration,
|
||||
similar to that used for totality.
|
||||
(We will show that the three cases are exclusive after we introduce
|
||||
[negation][plfa.Negation].)
|
||||
|
||||
#### Exercise `+-mono-<` {#plus-mono-less}
|
||||
|
||||
Show that addition is monotonic with respect to strict inequality.
|
||||
As with inequality, some additional definitions may be required.
|
||||
|
||||
#### Exercise `≤-iff-<` (recommended) {#leq-iff-less}
|
||||
|
||||
Show that `suc m ≤ n` implies `m < n`, and conversely.
|
||||
|
||||
#### Exercise `<-trans-revisited` {#less-trans-revisited}
|
||||
|
||||
Give an alternative proof that strict inequality is transitive,
|
||||
using the relating between strict inequality and inequality and
|
||||
the fact that inequality is transitive.
|
||||
|
||||
#### Exercise `o+o≡e` (stretch) {#odd-plus-odd}
|
||||
|
||||
Show that the sum of two odd numbers is even.
|
||||
|
||||
#### Exercise `Bin-predicates` (stretch) {#Bin-predicates}
|
||||
|
||||
Recall that
|
||||
Exercise [Bin][plfa.Naturals#Bin]
|
||||
defines a datatype `Bin` of bitstrings representing natural numbers.
|
||||
Representations are not unique due to leading zeros.
|
||||
Hence, eleven may be represented by both of the following
|
||||
|
||||
x1 x1 x0 x1 nil
|
||||
x1 x1 x0 x1 x0 x0 nil
|
||||
|
||||
Define a predicate
|
||||
|
||||
Can : Bin → Set
|
||||
|
||||
over all bitstrings that holds if the bitstring is canonical, meaning
|
||||
it has no leading zeros; the first representation of eleven above is
|
||||
canonical, and the second is not. To define it, you will need an
|
||||
auxiliary predicate
|
||||
|
||||
One : Bin → Set
|
||||
|
||||
that holds only if the bistring has a leading one. A bitstring is
|
||||
canonical if it has a leading one (representing a positive number) or
|
||||
if it consists of a single zero (representing zero).
|
||||
|
||||
Show that increment preserves canonical bitstrings.
|
||||
|
||||
Can x
|
||||
------------
|
||||
Can (inc x)
|
||||
|
||||
Show that converting a natural to a bitstring always yields a
|
||||
canonical bitstring.
|
||||
|
||||
----------
|
||||
Can (to n)
|
||||
|
||||
Show that converting a canonical bitstring to a natural
|
||||
and back is the identity.
|
||||
|
||||
Can x
|
||||
---------------
|
||||
to (from x) ≡ x
|
||||
|
||||
\end{code}
|
||||
(Hint: For each of these, you may first need to prove related
|
||||
properties of `One`.)
|
||||
557
tspl/PUC-Assignment2.lagda
Normal file
557
tspl/PUC-Assignment2.lagda
Normal file
|
|
@ -0,0 +1,557 @@
|
|||
---
|
||||
title : "PUC-Assignment2: PUC Assignment 2"
|
||||
layout : page
|
||||
permalink : /PUC-Assignment2/
|
||||
---
|
||||
|
||||
\begin{code}
|
||||
module PUC-Assignment2 where
|
||||
\end{code}
|
||||
|
||||
## YOUR NAME AND EMAIL GOES HERE
|
||||
|
||||
## Introduction
|
||||
|
||||
<!-- This assignment is due **4pm Thursday 18 October** (Week 5). -->
|
||||
|
||||
You must do _all_ the exercises labelled "(recommended)".
|
||||
|
||||
Exercises labelled "(stretch)" are there to provide an extra challenge.
|
||||
You don't need to do all of these, but should attempt at least a few.
|
||||
|
||||
Exercises without a label are optional, and may be done if you want
|
||||
some extra practice.
|
||||
|
||||
<!-- Submit your homework using the "submit" command. -->
|
||||
Please ensure your files execute correctly under Agda!
|
||||
|
||||
## Imports
|
||||
|
||||
\begin{code}
|
||||
import Relation.Binary.PropositionalEquality as Eq
|
||||
open Eq using (_≡_; refl; cong; sym)
|
||||
open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; _≡⟨_⟩_; _∎)
|
||||
open import Data.Nat using (ℕ; zero; suc; _+_; _*_; _∸_; _≤_; z≤n; s≤s)
|
||||
open import Data.Nat.Properties using (+-assoc; +-identityʳ; +-suc; +-comm;
|
||||
≤-refl; ≤-trans; ≤-antisym; ≤-total; +-monoʳ-≤; +-monoˡ-≤; +-mono-≤)
|
||||
open import plfa.Relations using (_<_; z<s; s<s)
|
||||
open import Data.Product using (_×_; proj₁; proj₂) renaming (_,_ to ⟨_,_⟩)
|
||||
open import Data.Unit using (⊤; tt)
|
||||
open import Data.Sum using (_⊎_; inj₁; inj₂) renaming ([_,_] to case-⊎)
|
||||
open import Data.Empty using (⊥; ⊥-elim)
|
||||
open import Data.Bool.Base using (Bool; true; false; T; _∧_; _∨_; not)
|
||||
open import Relation.Nullary using (¬_; Dec; yes; no)
|
||||
open import Relation.Nullary.Decidable using (⌊_⌋; toWitness; fromWitness)
|
||||
open import Relation.Nullary.Negation using (¬?)
|
||||
open import Relation.Nullary.Product using (_×-dec_)
|
||||
open import Relation.Nullary.Sum using (_⊎-dec_)
|
||||
open import Relation.Nullary.Negation using (contraposition)
|
||||
open import Data.Product using (Σ; _,_; ∃; Σ-syntax; ∃-syntax)
|
||||
open import plfa.Relations using (_<_; z<s; s<s)
|
||||
open import plfa.Isomorphism using (_≃_; ≃-sym; ≃-trans; _≲_; extensionality)
|
||||
open plfa.Isomorphism.≃-Reasoning
|
||||
open import plfa.Lists using (List; []; _∷_; [_]; [_,_]; [_,_,_]; [_,_,_,_];
|
||||
_++_; reverse; map; foldr; sum; All; Any; here; there; _∈_)
|
||||
\end{code}
|
||||
|
||||
## Equality
|
||||
|
||||
#### Exercise `≤-reasoning` (stretch)
|
||||
|
||||
The proof of monotonicity from
|
||||
Chapter [Relations][plfa.Relations]
|
||||
can be written in a more readable form by using an anologue of our
|
||||
notation for `≡-reasoning`. Define `≤-reasoning` analogously, and use
|
||||
it to write out an alternative proof that addition is monotonic with
|
||||
regard to inequality. Rewrite both `+-monoˡ-≤` and `+-mono-≤`.
|
||||
|
||||
|
||||
|
||||
## Isomorphism
|
||||
|
||||
#### Exercise `≃-implies-≲`
|
||||
|
||||
Show that every isomorphism implies an embedding.
|
||||
\begin{code}
|
||||
postulate
|
||||
≃-implies-≲ : ∀ {A B : Set}
|
||||
→ A ≃ B
|
||||
-----
|
||||
→ A ≲ B
|
||||
\end{code}
|
||||
|
||||
#### Exercise `_⇔_` (recommended) {#iff}
|
||||
|
||||
Define equivalence of propositions (also known as "if and only if") as follows.
|
||||
\begin{code}
|
||||
record _⇔_ (A B : Set) : Set where
|
||||
field
|
||||
to : A → B
|
||||
from : B → A
|
||||
|
||||
open _⇔_
|
||||
\end{code}
|
||||
Show that equivalence is reflexive, symmetric, and transitive.
|
||||
|
||||
#### Exercise `Bin-embedding` (stretch) {#Bin-embedding}
|
||||
|
||||
Recall that Exercises
|
||||
[Bin][plfa.Naturals#Bin] and
|
||||
[Bin-laws][plfa.Induction#Bin-laws]
|
||||
define a datatype of bitstrings representing natural numbers.
|
||||
\begin{code}
|
||||
data Bin : Set where
|
||||
nil : Bin
|
||||
x0_ : Bin → Bin
|
||||
x1_ : Bin → Bin
|
||||
\end{code}
|
||||
And ask you to define the following functions:
|
||||
|
||||
to : ℕ → Bin
|
||||
from : Bin → ℕ
|
||||
|
||||
which satisfy the following property:
|
||||
|
||||
from (to n) ≡ n
|
||||
|
||||
Using the above, establish that there is an embedding of `ℕ` into `Bin`.
|
||||
Why is there not an isomorphism?
|
||||
|
||||
|
||||
## Connectives
|
||||
|
||||
#### Exercise `⇔≃×` (recommended)
|
||||
|
||||
Show that `A ⇔ B` as defined [earlier][plfa.Isomorphism#iff]
|
||||
is isomorphic to `(A → B) × (B → A)`.
|
||||
|
||||
#### Exercise `⊎-comm` (recommended)
|
||||
|
||||
Show sum is commutative up to isomorphism.
|
||||
|
||||
#### Exercise `⊎-assoc`
|
||||
|
||||
Show sum is associative up to ismorphism.
|
||||
|
||||
#### Exercise `⊥-identityˡ` (recommended)
|
||||
|
||||
Show zero is the left identity of addition.
|
||||
|
||||
#### Exercise `⊥-identityʳ`
|
||||
|
||||
Show zero is the right identity of addition.
|
||||
|
||||
#### Exercise `⊎-weak-×` (recommended)
|
||||
|
||||
Show that the following property holds.
|
||||
\begin{code}
|
||||
postulate
|
||||
⊎-weak-× : ∀ {A B C : Set} → (A ⊎ B) × C → A ⊎ (B × C)
|
||||
\end{code}
|
||||
This is called a _weak distributive law_. Give the corresponding
|
||||
distributive law, and explain how it relates to the weak version.
|
||||
|
||||
#### Exercise `⊎×-implies-×⊎`
|
||||
|
||||
Show that a disjunct of conjuncts implies a conjunct of disjuncts.
|
||||
\begin{code}
|
||||
postulate
|
||||
⊎×-implies-×⊎ : ∀ {A B C D : Set} → (A × B) ⊎ (C × D) → (A ⊎ C) × (B ⊎ D)
|
||||
\end{code}
|
||||
Does the converse hold? If so, prove; if not, give a counterexample.
|
||||
|
||||
|
||||
## Negation
|
||||
|
||||
#### Exercise `<-irreflexive` (recommended)
|
||||
|
||||
Using negation, show that
|
||||
[strict inequality][plfa.Relations#strict-inequality]
|
||||
is irreflexive, that is, `n < n` holds for no `n`.
|
||||
|
||||
|
||||
#### Exercise `trichotomy`
|
||||
|
||||
Show that strict inequality satisfies
|
||||
[trichotomy][plfa.Relations#trichotomy],
|
||||
that is, for any naturals `m` and `n` exactly one of the following holds:
|
||||
|
||||
* `m < n`
|
||||
* `m ≡ n`
|
||||
* `m > n`
|
||||
|
||||
Here "exactly one" means that one of the three must hold, and each implies the
|
||||
negation of the other two.
|
||||
|
||||
|
||||
#### Exercise `⊎-dual-×` (recommended)
|
||||
|
||||
Show that conjunction, disjunction, and negation are related by a
|
||||
version of De Morgan's Law.
|
||||
|
||||
¬ (A ⊎ B) ≃ (¬ A) × (¬ B)
|
||||
|
||||
This result is an easy consequence of something we've proved previously.
|
||||
|
||||
Do we also have the following?
|
||||
|
||||
¬ (A × B) ≃ (¬ A) ⊎ (¬ B)
|
||||
|
||||
If so, prove; if not, give a variant that does hold.
|
||||
|
||||
|
||||
#### Exercise `Classical` (stretch)
|
||||
|
||||
Consider the following principles.
|
||||
|
||||
* Excluded Middle: `A ⊎ ¬ A`, for all `A`
|
||||
* Double Negation Elimination: `¬ ¬ A → A`, for all `A`
|
||||
* Peirce's Law: `((A → B) → A) → A`, for all `A` and `B`.
|
||||
* Implication as disjunction: `(A → B) → ¬ A ⊎ B`, for all `A` and `B`.
|
||||
* De Morgan: `¬ (¬ A × ¬ B) → A ⊎ B`, for all `A` and `B`.
|
||||
|
||||
Show that each of these implies all the others.
|
||||
|
||||
|
||||
#### Exercise `Stable` (stretch)
|
||||
|
||||
Say that a formula is _stable_ if double negation elimination holds for it.
|
||||
\begin{code}
|
||||
Stable : Set → Set
|
||||
Stable A = ¬ ¬ A → A
|
||||
\end{code}
|
||||
Show that any negated formula is stable, and that the conjunction
|
||||
of two stable formulas is stable.
|
||||
|
||||
|
||||
## Quantifiers
|
||||
|
||||
#### Exercise `∀-distrib-×` (recommended)
|
||||
|
||||
Show that universals distribute over conjunction.
|
||||
\begin{code}
|
||||
postulate
|
||||
∀-distrib-× : ∀ {A : Set} {B C : A → Set} →
|
||||
(∀ (x : A) → B x × C x) ≃ (∀ (x : A) → B x) × (∀ (x : A) → C x)
|
||||
\end{code}
|
||||
Compare this with the result (`→-distrib-×`) in
|
||||
Chapter [Connectives][plfa.Connectives].
|
||||
|
||||
#### Exercise `⊎∀-implies-∀⊎`
|
||||
|
||||
Show that a disjunction of universals implies a universal of disjunctions.
|
||||
\begin{code}
|
||||
postulate
|
||||
⊎∀-implies-∀⊎ : ∀ {A : Set} { B C : A → Set } →
|
||||
(∀ (x : A) → B x) ⊎ (∀ (x : A) → C x) → ∀ (x : A) → B x ⊎ C x
|
||||
\end{code}
|
||||
Does the converse hold? If so, prove; if not, explain why.
|
||||
|
||||
#### Exercise `∃-distrib-⊎` (recommended)
|
||||
|
||||
Show that existentials distribute over disjunction.
|
||||
\begin{code}
|
||||
postulate
|
||||
∃-distrib-⊎ : ∀ {A : Set} {B C : A → Set} →
|
||||
∃[ x ] (B x ⊎ C x) ≃ (∃[ x ] B x) ⊎ (∃[ x ] C x)
|
||||
\end{code}
|
||||
|
||||
#### Exercise `∃×-implies-×∃`
|
||||
|
||||
Show that an existential of conjunctions implies a conjunction of existentials.
|
||||
\begin{code}
|
||||
postulate
|
||||
∃×-implies-×∃ : ∀ {A : Set} { B C : A → Set } →
|
||||
∃[ x ] (B x × C x) → (∃[ x ] B x) × (∃[ x ] C x)
|
||||
\end{code}
|
||||
Does the converse hold? If so, prove; if not, explain why.
|
||||
|
||||
#### Exercise `∃-even-odd`
|
||||
|
||||
How do the proofs become more difficult if we replace `m * 2` and `1 + m * 2`
|
||||
by `2 * m` and `2 * m + 1`? Rewrite the proofs of `∃-even` and `∃-odd` when
|
||||
restated in this way.
|
||||
|
||||
#### Exercise `∃-+-≤`
|
||||
|
||||
Show that `y ≤ z` holds if and only if there exists a `x` such that
|
||||
`x + y ≡ z`.
|
||||
|
||||
#### Exercise `∃¬-implies-¬∀` (recommended)
|
||||
|
||||
Show that existential of a negation implies negation of a universal.
|
||||
\begin{code}
|
||||
postulate
|
||||
∃¬-implies-¬∀ : ∀ {A : Set} {B : A → Set}
|
||||
→ ∃[ x ] (¬ B x)
|
||||
--------------
|
||||
→ ¬ (∀ x → B x)
|
||||
\end{code}
|
||||
Does the converse hold? If so, prove; if not, explain why.
|
||||
|
||||
|
||||
#### Exercise `Bin-isomorphism` (stretch) {#Bin-isomorphism}
|
||||
|
||||
Recall that Exercises
|
||||
[Bin][plfa.Naturals#Bin],
|
||||
[Bin-laws][plfa.Induction#Bin-laws], and
|
||||
[Bin-predicates][plfa.Relations#Bin-predicates]
|
||||
define a datatype of bitstrings representing natural numbers.
|
||||
|
||||
data Bin : Set where
|
||||
nil : Bin
|
||||
x0_ : Bin → Bin
|
||||
x1_ : Bin → Bin
|
||||
|
||||
And ask you to define the following functions and predicates.
|
||||
|
||||
to : ℕ → Bin
|
||||
from : Bin → ℕ
|
||||
Can : Bin → Set
|
||||
|
||||
And to establish the following properties.
|
||||
|
||||
from (to n) ≡ n
|
||||
|
||||
----------
|
||||
Can (to n)
|
||||
|
||||
Can x
|
||||
---------------
|
||||
to (from x) ≡ x
|
||||
|
||||
Using the above, establish that there is an isomorphism between `ℕ` and
|
||||
`∃[ x ](Can x)`.
|
||||
|
||||
|
||||
## Decidable
|
||||
|
||||
#### Exercise `_<?_` (recommended)
|
||||
|
||||
Analogous to the function above, define a function to decide strict inequality.
|
||||
\begin{code}
|
||||
postulate
|
||||
_<?_ : ∀ (m n : ℕ) → Dec (m < n)
|
||||
\end{code}
|
||||
|
||||
#### Exercise `_≡ℕ?_`
|
||||
|
||||
Define a function to decide whether two naturals are equal.
|
||||
\begin{code}
|
||||
postulate
|
||||
_≡ℕ?_ : ∀ (m n : ℕ) → Dec (m ≡ n)
|
||||
\end{code}
|
||||
|
||||
|
||||
#### Exercise `erasure`
|
||||
|
||||
Show that erasure relates corresponding boolean and decidable operations.
|
||||
\begin{code}
|
||||
postulate
|
||||
∧-× : ∀ {A B : Set} (x : Dec A) (y : Dec B) → ⌊ x ⌋ ∧ ⌊ y ⌋ ≡ ⌊ x ×-dec y ⌋
|
||||
∨-× : ∀ {A B : Set} (x : Dec A) (y : Dec B) → ⌊ x ⌋ ∨ ⌊ y ⌋ ≡ ⌊ x ⊎-dec y ⌋
|
||||
not-¬ : ∀ {A : Set} (x : Dec A) → not ⌊ x ⌋ ≡ ⌊ ¬? x ⌋
|
||||
\end{code}
|
||||
|
||||
#### Exercise `iff-erasure` (recommended)
|
||||
|
||||
Give analogues of the `_⇔_` operation from
|
||||
Chapter [Isomorphism][plfa.Isomorphism#iff],
|
||||
operation on booleans and decidables, and also show the corresponding erasure.
|
||||
\begin{code}
|
||||
postulate
|
||||
_iff_ : Bool → Bool → Bool
|
||||
_⇔-dec_ : ∀ {A B : Set} → Dec A → Dec B → Dec (A ⇔ B)
|
||||
iff-⇔ : ∀ {A B : Set} (x : Dec A) (y : Dec B) → ⌊ x ⌋ iff ⌊ y ⌋ ≡ ⌊ x ⇔-dec y ⌋
|
||||
\end{code}
|
||||
|
||||
## 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.
|
||||
\begin{code}
|
||||
postulate
|
||||
reverse-++-commute : ∀ {A : Set} {xs ys : List A}
|
||||
→ reverse (xs ++ ys) ≡ reverse ys ++ reverse xs
|
||||
\end{code}
|
||||
|
||||
#### Exercise `reverse-involutive` (recommended)
|
||||
|
||||
A function is an _involution_ if when applied twice it acts
|
||||
as the identity function. Show that reverse is an involution.
|
||||
\begin{code}
|
||||
postulate
|
||||
reverse-involutive : ∀ {A : Set} {xs : List A}
|
||||
→ reverse (reverse xs) ≡ xs
|
||||
\end{code}
|
||||
|
||||
#### Exercise `map-compose`
|
||||
|
||||
Prove that the map of a composition is equal to the composition of two maps.
|
||||
\begin{code}
|
||||
postulate
|
||||
map-compose : ∀ {A B C : Set} {f : A → B} {g : B → C}
|
||||
→ map (g ∘ f) ≡ map g ∘ map f
|
||||
\end{code}
|
||||
The last step of the proof requires extensionality.
|
||||
|
||||
#### Exercise `map-++-commute`
|
||||
|
||||
Prove the following relationship between map and append.
|
||||
\begin{code}
|
||||
postulate
|
||||
map-++-commute : ∀ {A B : Set} {f : A → B} {xs ys : List A}
|
||||
→ map f (xs ++ ys) ≡ map f xs ++ map f ys
|
||||
\end{code}
|
||||
|
||||
#### Exercise `map-Tree`
|
||||
|
||||
Define a type of trees with leaves of type `A` and internal
|
||||
nodes of type `B`.
|
||||
\begin{code}
|
||||
data Tree (A B : Set) : Set where
|
||||
leaf : A → Tree A B
|
||||
node : Tree A B → B → Tree A B → Tree A B
|
||||
\end{code}
|
||||
Define a suitabve map operator over trees.
|
||||
\begin{code}
|
||||
postulate
|
||||
map-Tree : ∀ {A B C D : Set}
|
||||
→ (A → C) → (B → D) → Tree A B → Tree C D
|
||||
\end{code}
|
||||
|
||||
#### Exercise `product` (recommended)
|
||||
|
||||
Use fold to define a function to find the product of a list of numbers.
|
||||
For example,
|
||||
|
||||
product [ 1 , 2 , 3 , 4 ] ≡ 24
|
||||
|
||||
#### Exercise `foldr-++` (recommended)
|
||||
|
||||
Show that fold and append are related as follows.
|
||||
\begin{code}
|
||||
postulate
|
||||
foldr-++ : ∀ {A B : Set} (_⊗_ : A → B → B) (e : B) (xs ys : List A) →
|
||||
foldr _⊗_ e (xs ++ ys) ≡ foldr _⊗_ (foldr _⊗_ e ys) xs
|
||||
\end{code}
|
||||
|
||||
|
||||
#### Exercise `map-is-foldr`
|
||||
|
||||
Show that map can be defined using fold.
|
||||
\begin{code}
|
||||
postulate
|
||||
map-is-foldr : ∀ {A B : Set} {f : A → B} →
|
||||
map f ≡ foldr (λ x xs → f x ∷ xs) []
|
||||
\end{code}
|
||||
This requires extensionality.
|
||||
|
||||
#### Exercise `fold-Tree`
|
||||
|
||||
Define a suitable fold function for the type of trees given earlier.
|
||||
\begin{code}
|
||||
postulate
|
||||
fold-Tree : ∀ {A B C : Set}
|
||||
→ (A → C) → (C → B → C → C) → Tree A B → C
|
||||
\end{code}
|
||||
|
||||
#### Exercise `map-is-fold-Tree`
|
||||
|
||||
Demonstrate an anologue of `map-is-foldr` for the type of trees.
|
||||
|
||||
#### Exercise `sum-downFrom` (stretch)
|
||||
|
||||
Define a function that counts down as follows.
|
||||
\begin{code}
|
||||
downFrom : ℕ → List ℕ
|
||||
downFrom zero = []
|
||||
downFrom (suc n) = n ∷ downFrom n
|
||||
\end{code}
|
||||
For example,
|
||||
\begin{code}
|
||||
_ : downFrom 3 ≡ [ 2 , 1 , 0 ]
|
||||
_ = refl
|
||||
\end{code}
|
||||
Prove that the sum of the numbers `(n - 1) + ⋯ + 0` is
|
||||
equal to `n * (n ∸ 1) / 2`.
|
||||
\begin{code}
|
||||
postulate
|
||||
sum-downFrom : ∀ (n : ℕ)
|
||||
→ sum (downFrom n) * 2 ≡ n * (n ∸ 1)
|
||||
\end{code}
|
||||
|
||||
|
||||
#### Exercise `foldl`
|
||||
|
||||
Define a function `foldl` which is analogous to `foldr`, but where
|
||||
operations associate to the left rather than the right. For example,
|
||||
|
||||
foldr _⊗_ e [ x , y , z ] = x ⊗ (y ⊗ (z ⊗ e))
|
||||
foldl _⊗_ e [ x , y , z ] = ((e ⊗ x) ⊗ y) ⊗ z
|
||||
|
||||
|
||||
#### Exercise `foldr-monoid-foldl`
|
||||
|
||||
Show that if `_⊕_` and `e` form a monoid, then `foldr _⊗_ e` and
|
||||
`foldl _⊗_ e` always compute the same result.
|
||||
|
||||
|
||||
#### Exercise `Any-++-⇔` (recommended)
|
||||
|
||||
Prove a result similar to `All-++-⇔`, but with `Any` in place of `All`, and a suitable
|
||||
replacement for `_×_`. As a consequence, demonstrate an equivalence relating
|
||||
`_∈_` and `_++_`.
|
||||
|
||||
|
||||
#### Exercise `All-++-≃` (stretch)
|
||||
|
||||
Show that the equivalence `All-++-⇔` can be extended to an isomorphism.
|
||||
|
||||
|
||||
#### Exercise `¬Any≃All¬` (stretch)
|
||||
|
||||
First generalise composition to arbitrary levels, using
|
||||
[universe polymorphism][plfa.Equality#unipoly].
|
||||
\begin{code}
|
||||
_∘′_ : ∀ {ℓ₁ ℓ₂ ℓ₃ : Level} {A : Set ℓ₁} {B : Set ℓ₂} {C : Set ℓ₃}
|
||||
→ (B → C) → (A → B) → A → C
|
||||
(g ∘′ f) x = g (f x)
|
||||
\end{code}
|
||||
|
||||
Show that `Any` and `All` satisfy a version of De Morgan's Law.
|
||||
\begin{code}
|
||||
postulate
|
||||
¬Any≃All¬ : ∀ {A : Set} (P : A → Set) (xs : List A)
|
||||
→ (¬_ ∘′ Any P) xs ≃ All (¬_ ∘′ P) xs
|
||||
\end{code}
|
||||
|
||||
Do we also have the following?
|
||||
\begin{code}
|
||||
postulate
|
||||
¬All≃Any¬ : ∀ {A : Set} (P : A → Set) (xs : List A)
|
||||
→ (¬_ ∘′ All P) xs ≃ Any (¬_ ∘′ P) xs
|
||||
\end{code}
|
||||
If so, prove; if not, explain why.
|
||||
|
||||
|
||||
#### Exercise `any?` (stretch)
|
||||
|
||||
Just as `All` has analogues `all` and `all?` which determine whether a
|
||||
predicate holds for every element of a list, so does `Any` have
|
||||
analogues `any` and `any?` which determine whether a predicates holds
|
||||
for some element of a list. Give their definitions.
|
||||
|
||||
|
||||
#### Exercise `filter?` (stretch)
|
||||
|
||||
Define the following variant of the traditional `filter` function on lists,
|
||||
which given a list and a decidable predicate returns all elements of the
|
||||
list satisfying the predicate.
|
||||
\begin{code}
|
||||
postulate
|
||||
filter? : ∀ {A : Set} {P : A → Set}
|
||||
→ (P? : Decidable P) → List A → ∃[ ys ]( All P ys )
|
||||
\end{code}
|
||||
192
tspl/PUC-Assignment3.lagda
Normal file
192
tspl/PUC-Assignment3.lagda
Normal file
|
|
@ -0,0 +1,192 @@
|
|||
---
|
||||
title : "PUC-Assignment3: PUC Assignment 3"
|
||||
layout : page
|
||||
permalink : /PUC-Assignment3/
|
||||
---
|
||||
|
||||
\begin{code}
|
||||
module PUC-Assignment3 where
|
||||
\end{code}
|
||||
|
||||
## YOUR NAME AND EMAIL GOES HERE
|
||||
|
||||
## Introduction
|
||||
|
||||
<!-- This assignment is due **4pm Thursday 1 November** (Week 7). -->
|
||||
|
||||
You must do _all_ the exercises labelled "(recommended)".
|
||||
|
||||
Exercises labelled "(stretch)" are there to provide an extra challenge.
|
||||
You don't need to do all of these, but should attempt at least a few.
|
||||
|
||||
Exercises without a label are optional, and may be done if you want
|
||||
some extra practice.
|
||||
|
||||
<!-- Submit your homework using the "submit" command. -->
|
||||
Please ensure your files execute correctly under Agda!
|
||||
|
||||
## Imports
|
||||
|
||||
\begin{code}
|
||||
import Relation.Binary.PropositionalEquality as Eq
|
||||
open Eq using (_≡_; refl; cong; sym)
|
||||
open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; _≡⟨_⟩_; _∎)
|
||||
open import Data.Bool.Base using (Bool; true; false; T; _∧_; _∨_; not)
|
||||
open import Data.Nat using (ℕ; zero; suc; _+_; _*_; _∸_; _≤_; s≤s; z≤n)
|
||||
open import Data.Nat.Properties using
|
||||
(+-assoc; +-identityˡ; +-identityʳ; *-assoc; *-identityˡ; *-identityʳ)
|
||||
open import Relation.Nullary using (¬_; Dec; yes; no)
|
||||
open import Data.Product using (_×_; ∃; ∃-syntax) renaming (_,_ to ⟨_,_⟩)
|
||||
open import Data.Empty using (⊥; ⊥-elim)
|
||||
open import Function using (_∘_)
|
||||
open import Algebra.Structures using (IsMonoid)
|
||||
open import Level using (Level)
|
||||
open import Relation.Unary using (Decidable)
|
||||
open import plfa.Relations using (_<_; z<s; s<s)
|
||||
open import plfa.Isomorphism using (_≃_; ≃-sym; ≃-trans; _≲_; extensionality)
|
||||
open plfa.Isomorphism.≃-Reasoning
|
||||
open import plfa.Lists using (List; []; _∷_; [_]; [_,_]; [_,_,_]; [_,_,_,_];
|
||||
_++_; reverse; map; foldr; sum; All; Any; here; there; _∈_)
|
||||
open import plfa.Lambda hiding (ƛ′_⇒_; case′_[zero⇒_|suc_⇒_]; μ′_⇒_; plus′)
|
||||
open import plfa.Properties hiding (value?; unstuck; preserves; wttdgs)
|
||||
\end{code}
|
||||
|
||||
## 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.
|
||||
\begin{code}
|
||||
ƛ′_⇒_ : Term → Term → Term
|
||||
ƛ′ (` x) ⇒ N = ƛ x ⇒ N
|
||||
ƛ′ _ ⇒ _ = ⊥-elim impossible
|
||||
where postulate impossible : ⊥
|
||||
|
||||
case′_[zero⇒_|suc_⇒_] : Term → Term → Term → Term → Term
|
||||
case′ L [zero⇒ M |suc (` x) ⇒ N ] = case L [zero⇒ M |suc x ⇒ N ]
|
||||
case′ _ [zero⇒ _ |suc _ ⇒ _ ] = ⊥-elim impossible
|
||||
where postulate impossible : ⊥
|
||||
|
||||
μ′_⇒_ : Term → Term → Term
|
||||
μ′ (` x) ⇒ N = μ x ⇒ N
|
||||
μ′ _ ⇒ _ = ⊥-elim impossible
|
||||
where postulate impossible : ⊥
|
||||
\end{code}
|
||||
The definition of `plus` can now be written as follows.
|
||||
\begin{code}
|
||||
plus′ : Term
|
||||
plus′ = μ′ + ⇒ ƛ′ m ⇒ ƛ′ n ⇒
|
||||
case′ m
|
||||
[zero⇒ n
|
||||
|suc m ⇒ `suc (+ · m · n) ]
|
||||
where
|
||||
+ = ` "+"
|
||||
m = ` "m"
|
||||
n = ` "n"
|
||||
\end{code}
|
||||
Write out the definition of multiplication in the same style.
|
||||
|
||||
#### Exercise `_[_:=_]′` (stretch)
|
||||
|
||||
The definition of substitution above has three clauses (`ƛ`, `case`,
|
||||
and `μ`) that invoke a with clause to deal with bound variables.
|
||||
Rewrite the definition to factor the common part of these three
|
||||
clauses into a single function, defined by mutual recursion with
|
||||
substitution.
|
||||
|
||||
|
||||
#### Exercise `—↠≃—↠′`
|
||||
|
||||
Show that the two notions of reflexive and transitive closure
|
||||
above are isomorphic.
|
||||
|
||||
|
||||
#### Exercise `plus-example`
|
||||
|
||||
Write out the reduction sequence demonstrating that one plus one is two.
|
||||
|
||||
|
||||
#### Exercise `mul-type` (recommended)
|
||||
|
||||
Using the term `mul` you defined earlier, write out the derivation
|
||||
showing that it is well-typed.
|
||||
|
||||
|
||||
## Properties
|
||||
|
||||
|
||||
#### Exercise `Progress-≃`
|
||||
|
||||
Show that `Progress M` is isomorphic to `Value M ⊎ ∃[ N ](M —→ N)`.
|
||||
|
||||
|
||||
#### Exercise `progress′`
|
||||
|
||||
Write out the proof of `progress′` in full, and compare it to the
|
||||
proof of `progress` above.
|
||||
|
||||
|
||||
#### Exercise `value?`
|
||||
|
||||
Combine `progress` and `—→¬V` to write a program that decides
|
||||
whether a well-typed term is a value.
|
||||
\begin{code}
|
||||
postulate
|
||||
value? : ∀ {A M} → ∅ ⊢ M ⦂ A → Dec (Value M)
|
||||
\end{code}
|
||||
|
||||
|
||||
#### Exercise `subst′` (stretch)
|
||||
|
||||
Rewrite `subst` to work with the modified definition `_[_:=_]′`
|
||||
from the exercise in the previous chapter. As before, this
|
||||
should factor dealing with bound variables into a single function,
|
||||
defined by mutual recursion with the proof that substitution
|
||||
preserves types.
|
||||
|
||||
|
||||
#### Exercise `mul-example` (recommended)
|
||||
|
||||
Using the evaluator, confirm that two times two is four.
|
||||
|
||||
|
||||
#### Exercise: `progress-preservation`
|
||||
|
||||
Without peeking at their statements above, write down the progress
|
||||
and preservation theorems for the simply typed lambda-calculus.
|
||||
|
||||
|
||||
#### Exercise `subject-expansion`
|
||||
|
||||
We say that `M` _reduces_ to `N` if `M —→ N`,
|
||||
and conversely that `M` _expands_ to `N` if `N —→ M`.
|
||||
The preservation property is sometimes called _subject reduction_.
|
||||
Its opposite is _subject expansion_, which holds if
|
||||
`M —→ N` and `∅ ⊢ N ⦂ A` imply `∅ ⊢ M ⦂ A`.
|
||||
Find two counter-examples to subject expansion, one
|
||||
with case expressions and one not involving case expressions.
|
||||
|
||||
|
||||
#### Exercise `stuck`
|
||||
|
||||
Give an example of an ill-typed term that does get stuck.
|
||||
|
||||
|
||||
#### Exercise `unstuck` (recommended)
|
||||
|
||||
Provide proofs of the three postulates, `unstuck`, `preserves`, and `wttdgs` above.
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
1169
tspl/PUC-Assignment4.lagda
Normal file
1169
tspl/PUC-Assignment4.lagda
Normal file
File diff suppressed because it is too large
Load diff
|
|
@ -91,11 +91,11 @@ Lectures and tutorials take place Fridays and some Thursdays in 548L.
|
|||
|
||||
For instructions on how to set up Agda for PLFA see [Getting Started](/GettingStarted/).
|
||||
|
||||
* [Assignment 1][Assignment1] due Friday 26 April.
|
||||
* [Assignment 2][Assignment2] due Wednesday 8 May.
|
||||
* [Assignment 3][Assignment3] due Wednesday 12 June.
|
||||
* [Assignment 4][Assignment4] due Wednesday 26 June.
|
||||
* [Assignment 5](/tspl/Assignment5.pdf) due Wednesday 26 June.
|
||||
* [PUC-Assignment 1][PUC-Assignment1] due Friday 26 April.
|
||||
* [PUC-Assignment 2][PUC-Assignment2] due Wednesday 22 May.
|
||||
* [PUC-Assignment 3][PUC-Assignment3] due Wednesday 12 June.
|
||||
* [PUC-Assignment 4][PUC-Assignment4] due Tuesday 25 June.
|
||||
* [Assignment 5](/tspl/Assignment5.pdf) due Tuesday 25 June.
|
||||
Use file [Exam][Exam]. Despite the rubric, do **all three questions**.
|
||||
|
||||
Submit assignments by email to [wadler@inf.ed.ac.uk](mailto:wadler@inf.ed.ac.uk).
|
||||
|
|
|
|||
Loading…
Reference in a new issue