diff --git a/TSPL/2024/Assignment1/index.html b/TSPL/2024/Assignment1/index.html index 43b2bbc0a..ebcb1dbec 100644 --- a/TSPL/2024/Assignment1/index.html +++ b/TSPL/2024/Assignment1/index.html @@ -1,63 +1,63 @@ Programming Language Foundations in Agda – Assignment1
Programming Language Foundations in Agda

Assignment1: TSPL Assignment 1

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 labelled “(practice)” are included for those who want extra practice.

Submit your homework using Gradescope. Go to the course page under Learn. Select Assessment, then select Assignment Submission. Please ensure your files execute correctly under Agda!

Good Scholarly Practice.

Please remember the University requirement as regards all assessed work. Details about this can be found at:

https://web.inf.ed.ac.uk/infweb/admin/policies/academic-misconduct

You are required to take reasonable measures to protect your assessed work from unauthorised access. For example, if you put any such work on a public repository then you must set access permissions appropriately (generally permitting access only to yourself). Do not publish solutions to the coursework.

Naturals

module Naturals where
-  import Relation.Binary.PropositionalEquality as Eq
-  open Eq using (_≡_; refl)
-  open Eq.≡-Reasoning using (begin_; step-≡-∣; _∎)
-  open import Data.Nat using (ℕ; zero; suc; _+_; _*_; _∸_)
-

Exercise seven (practice)

Write out 7 in longhand.

  -- Your code goes here
-

You will need to give both a type signature and definition for the variable seven. Type C-c C-l in Emacs to instruct Agda to re-load.

Exercise +-example (practice)

Compute 3 + 4, writing out your reasoning as a chain of equations, using the equations for +.

  -- Your code goes here
-

Exercise *-example (practice)

Compute 3 * 4, writing out your reasoning as a chain of equations, using the equations for *. (You do not need to step through the evaluation of +.)

  -- Your code goes here
+

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 labelled “(practice)” are included for those who want extra practice.

Submit your homework using Gradescope. Go to the course page under Learn. Select Assessment, then select Assignment Submission. Please ensure your files execute correctly under Agda!

Good Scholarly Practice.

Please remember the University requirement as regards all assessed work. Details about this can be found at:

https://web.inf.ed.ac.uk/infweb/admin/policies/academic-misconduct

You are required to take reasonable measures to protect your assessed work from unauthorised access. For example, if you put any such work on a public repository then you must set access permissions appropriately (generally permitting access only to yourself). Do not publish solutions to the coursework.

Deadline and late policy

The deadline and late policy for this assignment are specified on Learn in the “Coursework Planner”. There are no extensions and no ETAs. Coursework is marked best three out of four. Guidance on late submissions is at

https://web.inf.ed.ac.uk/node/4533

Naturals

module Naturals where
+  import Relation.Binary.PropositionalEquality as Eq
+  open Eq using (_≡_; refl)
+  open Eq.≡-Reasoning using (begin_; step-≡-∣; _∎)
+  open import Data.Nat using (ℕ; zero; suc; _+_; _*_; _∸_)
+

Exercise seven (practice)

Write out 7 in longhand.

  -- Your code goes here
+

You will need to give both a type signature and definition for the variable seven. Type C-c C-l in Emacs to instruct Agda to re-load.

Exercise +-example (practice)

Compute 3 + 4, writing out your reasoning as a chain of equations, using the equations for +.

  -- Your code goes here
+

Exercise *-example (practice)

Compute 3 * 4, writing out your reasoning as a chain of equations, using the equations for *. (You do not need to step through the evaluation of +.)

  -- Your code goes here

Exercise _^_ (recommended)

Define exponentiation, which is given by the following equations:

m ^ 0        =  1
-m ^ (1 + n)  =  m * (m ^ n)

Check that 3 ^ 4 is 81.

  -- Your code goes here
-

Exercise ∸-example₁ and ∸-example₂ (recommended)

Compute 5 ∸ 3 and 3 ∸ 5, writing out your reasoning as a chain of equations.

  -- Your code goes here
-

Exercise Bin (stretch)

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
-    ⟨⟩ : Bin
-    _O : Bin → Bin
-    _I : Bin → Bin
+m ^ (1 + n)  =  m * (m ^ n)

Check that 3 ^ 4 is 81.

  -- Your code goes here
+

Exercise ∸-example₁ and ∸-example₂ (recommended)

Compute 5 ∸ 3 and 3 ∸ 5, writing out your reasoning as a chain of equations.

  -- Your code goes here
+

Exercise Bin (stretch)

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
+    ⟨⟩ : Bin
+    _O : Bin → Bin
+    _I : Bin → Bin

For instance, the bitstring

1011

standing for the number eleven is encoded as

⟨⟩ I O I I

Representations are not unique due to leading zeros. Hence, eleven is also represented by 001011, encoded as:

⟨⟩ O O I O I I

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 (⟨⟩ I O I I) ≡ ⟨⟩ I I O O

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 ⟨⟩ O. Confirm that these both give the correct answer for zero through four.

  -- Your code goes here
-

Induction

module Induction where
-

Imports

We require equality as in the previous chapter, plus the naturals and some operations upon them. We also require a couple of new operations, cong, sym, and _≡⟨_⟩_, which are explained below:
  import Relation.Binary.PropositionalEquality as Eq
-  open Eq using (_≡_; refl; cong; sym)
-  open Eq.≡-Reasoning using (begin_; step-≡-∣; step-≡-⟩; _∎)
-  open import Data.Nat using (ℕ; zero; suc; _+_; _*_; _∸_; _^_)
-  open import Data.Nat.Properties using (+-assoc; +-identityʳ; +-suc; +-comm)
-

(Importing step-≡ defines _≡⟨_⟩_.)

  open import plfa.part1.Induction
-    hiding ()
-

Exercise operators (practice)

Give another example of a pair of operators that have an identity and are associative, commutative, and distribute over one another. (You do not have to prove these properties.)

Give an example of an operator that has an identity and is associative but is not commutative. (You do not have to prove these properties.)

Exercise finite-+-assoc (stretch)

Write out what is known about associativity of addition on each of the first four days using a finite story of creation, as earlier.

  -- Your code goes here
-

Exercise +-swap (recommended)

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.

  -- Your code goes here
-

Exercise *-distrib-+ (recommended)

Show multiplication distributes over addition, that is,

(m + n) * p ≡ m * p + n * p

for all naturals m, n, and p.

  -- Your code goes here
-

Exercise *-assoc (recommended)

Show multiplication is associative, that is,

(m * n) * p ≡ m * (n * p)

for all naturals m, n, and p.

  -- Your code goes here
-

Exercise *-comm (practice)

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.

  -- Your code goes here
-

Exercise 0∸n≡0 (practice)

Show

zero ∸ n ≡ zero

for all naturals n. Did your proof require induction?

  -- Your code goes here
-

Exercise ∸-+-assoc (practice)

Show that monus associates with addition, that is,

m ∸ n ∸ p ≡ m ∸ (n + p)

for all naturals m, n, and p.

  -- Your code goes here
+from : Bin → ℕ

For the former, choose the bitstring to have no leading zeros if it represents a positive natural, and represent zero by ⟨⟩ O. Confirm that these both give the correct answer for zero through four.

  -- Your code goes here
+

Induction

module Induction where
+

Imports

We require equality as in the previous chapter, plus the naturals and some operations upon them. We also require a couple of new operations, cong, sym, and _≡⟨_⟩_, which are explained below:
  import Relation.Binary.PropositionalEquality as Eq
+  open Eq using (_≡_; refl; cong; sym)
+  open Eq.≡-Reasoning using (begin_; step-≡-∣; step-≡-⟩; _∎)
+  open import Data.Nat using (ℕ; zero; suc; _+_; _*_; _∸_; _^_)
+  open import Data.Nat.Properties using (+-assoc; +-identityʳ; +-suc; +-comm)
+

(Importing step-≡ defines _≡⟨_⟩_.)

  open import plfa.part1.Induction
+    hiding ()
+

Exercise operators (practice)

Give another example of a pair of operators that have an identity and are associative, commutative, and distribute over one another. (You do not have to prove these properties.)

Give an example of an operator that has an identity and is associative but is not commutative. (You do not have to prove these properties.)

Exercise finite-+-assoc (stretch)

Write out what is known about associativity of addition on each of the first four days using a finite story of creation, as earlier.

  -- Your code goes here
+

Exercise +-swap (recommended)

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.

  -- Your code goes here
+

Exercise *-distrib-+ (recommended)

Show multiplication distributes over addition, that is,

(m + n) * p ≡ m * p + n * p

for all naturals m, n, and p.

  -- Your code goes here
+

Exercise *-assoc (recommended)

Show multiplication is associative, that is,

(m * n) * p ≡ m * (n * p)

for all naturals m, n, and p.

  -- Your code goes here
+

Exercise *-comm (practice)

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.

  -- Your code goes here
+

Exercise 0∸n≡0 (practice)

Show

zero ∸ n ≡ zero

for all naturals n. Did your proof require induction?

  -- Your code goes here
+

Exercise ∸-+-assoc (practice)

Show that monus associates with addition, that is,

m ∸ n ∸ p ≡ m ∸ (n + p)

for all naturals m, n, and p.

  -- Your code goes here

Exercise +*^ (stretch)

Show the following three laws

 m ^ (n + p) ≡ (m ^ n) * (m ^ p)  (^-distribˡ-+-*)
  (m * n) ^ p ≡ (m ^ p) * (n ^ p)  (^-distribʳ-*)
- (m ^ n) ^ p ≡ m ^ (n * p)        (^-*-assoc)

for all m, n, and p.

  -- Your code goes here
+ (m ^ n) ^ p ≡ m ^ (n * p)        (^-*-assoc)

for all m, n, and p.

  -- Your code goes here

Exercise Bin-laws (stretch)

Recall that Exercise 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 b over bitstrings:

from (inc b) ≡ suc (from b)
 to (from b) ≡ b
-from (to n) ≡ n

For each law: if it holds, prove; if not, give a counterexample.

  -- Your code goes here
-

Relations

module Relations where
-

Imports

  import Relation.Binary.PropositionalEquality as Eq
-  open Eq using (_≡_; refl; cong)
-  open import Data.Nat using (ℕ; zero; suc; _+_)
-  open import Data.Nat.Properties using (+-comm; +-identityʳ)
-  open import Data.Nat using (_≤_; z≤n; s≤s)
-  open import Data.Nat.Properties
-    using (≤-refl; ≤-trans; ≤-antisym; ≤-total;
-           +-monoʳ-≤; +-monoˡ-≤; +-mono-≤)
-

Exercise orderings (practice)

Give an example of a preorder that is not a partial order.

  -- Your code goes here
-

Give an example of a partial order that is not a total order.

  -- Your code goes here
-

Exercise ≤-antisym-cases (practice)

The above proof omits cases where one argument is z≤n and one argument is s≤s. Why is it ok to omit them?

  -- Your code goes here
-

Exercise *-mono-≤ (stretch)

Show that multiplication is monotonic with regard to inequality.

  -- Your code goes here
-

Exercise <-trans (recommended)

Show that strict inequality is transitive. Use a direct proof. (A later exercise exploits the relation between < and ≤.)

  -- Your code goes here
-

Exercise trichotomy (practice)

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.)

  -- Your code goes here
-

Exercise +-mono-< (practice)

Show that addition is monotonic with respect to strict inequality. As with inequality, some additional definitions may be required.

  -- Your code goes here
-

Exercise ≤→<, <→≤ (recommended)

Show that suc m ≤ n implies m < n, and conversely.

  -- Your code goes here
-

Exercise <-trans-revisited (practice)

Give an alternative proof that strict inequality is transitive, using the relation between strict inequality and inequality and the fact that inequality is transitive.

  -- Your code goes here
-

Exercise o+o≡e (stretch)

Show that the sum of two odd numbers is even.

  -- Your code goes here
+from (to n) ≡ n

For each law: if it holds, prove; if not, give a counterexample.

  -- Your code goes here
+

Relations

module Relations where
+

Imports

  import Relation.Binary.PropositionalEquality as Eq
+  open Eq using (_≡_; refl; cong)
+  open import Data.Nat using (ℕ; zero; suc; _+_)
+  open import Data.Nat.Properties using (+-comm; +-identityʳ)
+  open import Data.Nat using (_≤_; z≤n; s≤s)
+  open import Data.Nat.Properties
+    using (≤-refl; ≤-trans; ≤-antisym; ≤-total;
+           +-monoʳ-≤; +-monoˡ-≤; +-mono-≤)
+

Exercise orderings (practice)

Give an example of a preorder that is not a partial order.

  -- Your code goes here
+

Give an example of a partial order that is not a total order.

  -- Your code goes here
+

Exercise ≤-antisym-cases (practice)

The above proof omits cases where one argument is z≤n and one argument is s≤s. Why is it ok to omit them?

  -- Your code goes here
+

Exercise *-mono-≤ (stretch)

Show that multiplication is monotonic with regard to inequality.

  -- Your code goes here
+

Exercise <-trans (recommended)

Show that strict inequality is transitive. Use a direct proof. (A later exercise exploits the relation between < and ≤.)

  -- Your code goes here
+

Exercise trichotomy (practice)

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.)

  -- Your code goes here
+

Exercise +-mono-< (practice)

Show that addition is monotonic with respect to strict inequality. As with inequality, some additional definitions may be required.

  -- Your code goes here
+

Exercise ≤→<, <→≤ (recommended)

Show that suc m ≤ n implies m < n, and conversely.

  -- Your code goes here
+

Exercise <-trans-revisited (practice)

Give an alternative proof that strict inequality is transitive, using the relation between strict inequality and inequality and the fact that inequality is transitive.

  -- Your code goes here
+

Exercise o+o≡e (stretch)

Show that the sum of two odd numbers is even.

  -- Your code goes here

Exercise Bin-predicates (stretch)

Recall that Exercise 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:

⟨⟩ I O I I
 ⟨⟩ O O I O I I

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 bitstring 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 b
 ------------
@@ -70,5 +70,5 @@
 
 1 ≤ n
 ---------------------
-to (2 * n) ≡ (to n) O

The hypothesis 1 ≤ n is required for the latter, because to (2 * 0) ≡ ⟨⟩ O but (to 0) O ≡ ⟨⟩ O O.

  -- Your code goes here
+to (2 * n) ≡ (to n) O

The hypothesis 1 ≤ n is required for the latter, because to (2 * 0) ≡ ⟨⟩ O but (to 0) O ≡ ⟨⟩ O O.

  -- Your code goes here
\ No newline at end of file diff --git a/TSPL/2024/Assignment2/index.html b/TSPL/2024/Assignment2/index.html new file mode 100644 index 000000000..b2fe6d0bd --- /dev/null +++ b/TSPL/2024/Assignment2/index.html @@ -0,0 +1,116 @@ +Programming Language Foundations in Agda – Assignment2
Programming Language Foundations in Agda

Assignment2: TSPL Assignment 2

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 labelled “(practice)” are included for those who want extra practice.

Submit your homework using Gradescope. Go to the course page under Learn. Select Assessment, then select Assignment Submission. Please ensure your files execute correctly under Agda!

Good Scholarly Practice.

Please remember the University requirement as regards all assessed work. Details about this can be found at:

https://web.inf.ed.ac.uk/infweb/admin/policies/academic-misconduct

You are required to take reasonable measures to protect your assessed work from unauthorised access. For example, if you put any such work on a public repository then you must set access permissions appropriately (generally permitting access only to yourself). Do not publish solutions to the coursework.

Deadline and late policy

The deadline and late policy for this assignment are specified on Learn in the “Coursework Planner”. There are no extensions and no ETAs. Coursework is marked best three out of four. Guidance on late submissions is at

https://web.inf.ed.ac.uk/node/4533

Connectives

module Connectives where
+

Imports

  import Relation.Binary.PropositionalEquality as Eq
+  open Eq using (_≡_; refl)
+  open Eq.≡-Reasoning
+  open import Data.Nat using (ℕ)
+  open import Function using (_∘_)
+  open import plfa.part1.Isomorphism using (_≃_; _≲_; extensionality; _⇔_)
+  open plfa.part1.Isomorphism.≃-Reasoning
+  open import plfa.part1.Connectives
+    hiding (⊎-weak-×; ⊎×-implies-×⊎)
+

Exercise ⇔≃× (practice)

Show that A ⇔ B as defined earlier is isomorphic to (A → B) × (B → A).

  -- Your code goes here
+

Exercise ⊎-comm (recommended)

Show sum is commutative up to isomorphism.

  -- Your code goes here
+

Exercise ⊎-assoc (practice)

Show sum is associative up to isomorphism.

  -- Your code goes here
+

Exercise ⊥-identityˡ (recommended)

Show empty is the left identity of sums up to isomorphism.

  -- Your code goes here
+

Exercise ⊥-identityʳ (practice)

Show empty is the right identity of sums up to isomorphism.

  -- Your code goes here
+

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.

  -- Your code goes here
+

Exercise ⊎×-implies-×⊎ (practice)

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.

  -- Your code goes here
+

Negation

module Negation where
+

Imports

  open import Relation.Binary.PropositionalEquality using (_≡_; refl)
+  open import Data.Nat using (ℕ; zero; suc)
+  open import plfa.part1.Isomorphism using (_≃_; extensionality)
+  open import plfa.part1.Connectives
+  open import plfa.part1.Negation
+    hiding (Stable)
+

Exercise <-irreflexive (recommended)

Using negation, show that strict inequality is irreflexive, that is, n < n holds for no n.

  -- Your code goes here
+

Exercise trichotomy (practice)

Show that strict inequality satisfies 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 not only one of the three must hold, but that when one holds the negation of the other two must also hold.

  -- Your code goes here
+

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.

  -- Your code goes here
+

Do we also have the following?

¬ (A × B) ≃ (¬ A) ⊎ (¬ B)

If so, prove; if not, can you give a relation weaker than isomorphism that relates the two sides?

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.

  -- Your code goes here
+

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.

  -- Your code goes here
+

Quantifiers

module Quantifiers where
+

Imports

  import Relation.Binary.PropositionalEquality as Eq
+  open Eq using (_≡_; refl)
+  open import Data.Nat using (ℕ; zero; suc; _+_; _*_)
+  open import Relation.Nullary using (¬_)
+  open import Function using (_∘_)
+  open import plfa.part1.Isomorphism using (_≃_; extensionality; ∀-extensionality)
+  open import plfa.part1.Connectives
+    hiding (Tri)
+  open import plfa.part1.Quantifiers
+    hiding (∀-distrib-×; ⊎∀-implies-∀⊎; ∃-distrib-⊎; ∃×-implies-×∃; ∃¬-implies-¬∀; Tri)
+

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.

Hint: you will need to use ∀-extensionality.

Exercise ⊎∀-implies-∀⊎ (practice)

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 ∀-× (practice)

Consider the following type.
  data Tri : Set where
+    aa : Tri
+    bb : Tri
+    cc : Tri
+

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.

Hint: you will need to use ∀-extensionality.

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-×∃ (practice)

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 ∃-⊎ (practice)

Let Tri and B be as in Exercise ∀-×. Show that ∃[ x ] B x is isomorphic to B aa ⊎ B bb ⊎ B cc.

Exercise ∃-even-odd (practice)

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.

  -- Your code goes here
+

Exercise ∃-+-≤ (practice)

Show that y ≤ z holds if and only if there exists a x such that x + y ≡ z.

  -- Your code goes here
+

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)

Recall that Exercises Bin, Bin-laws, and Bin-predicates define a datatype Bin of bitstrings representing natural numbers, and asks 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 b
+---------------
+to (from b) ≡ b

Using the above, establish that there is an isomorphism between ℕ and ∃[ b ] Can b.

We recommend proving the following lemmas which show that, for a given binary number b, there is only one proof of One b and similarly for Can b.

≡One : ∀ {b : Bin} (o o′ : One b) → o ≡ o′
+
+≡Can : ∀ {b : Bin} (cb cb′ : Can b) → cb ≡ cb′

Many of the alternatives for proving to∘from turn out to be tricky. However, the proof can be straightforward if you use the following lemma, which is a corollary of ≡Can.

proj₁≡→Can≡ : {cb cb′ : ∃[ b ] Can b} → proj₁ cb ≡ proj₁ cb′ → cb ≡ cb′
  -- Your code goes here
+

Decidable

module Decidable where
+

Imports

  import Relation.Binary.PropositionalEquality as Eq
+  open Eq using (_≡_; refl)
+  open Eq.≡-Reasoning
+  open import Data.Nat using (ℕ; zero; suc)
+  open import Data.Product using (_×_) renaming (_,_ to ⟨_,_⟩)
+  open import Data.Sum using (_⊎_; inj₁; inj₂)
+  open import Relation.Nullary using (¬_)
+  open import Relation.Nullary.Negation using ()
+    renaming (contradiction to ¬¬-intro)
+  open import Data.Unit using (⊤; tt)
+  open import Data.Empty using (⊥; ⊥-elim)
+  open import plfa.part1.Relations using (_<_; z<s; s<s)
+  open import plfa.part1.Isomorphism using (_⇔_)
+  open import plfa.part1.Decidable
+    hiding (_<?_; _≡ℕ?_; ∧-×; ∨-⊎; not-¬; _iff_; _⇔-dec_; iff-⇔)
+

Exercise _<?_ (recommended)

Analogous to the function above, define a function to decide strict inequality:
  postulate
+    _<?_ : ∀ (m n : ℕ) → Dec (m < n)
+
  -- Your code goes here
+

Exercise _≡ℕ?_ (practice)

Define a function to decide whether two naturals are equal:
  postulate
+    _≡ℕ?_ : ∀ (m n : ℕ) → Dec (m ≡ n)
+
  -- Your code goes here
+

Exercise erasure (practice)

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 ⌋
+
Give analogues of the _⇔_ operation from Chapter Isomorphism, 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 ⌋
+
  -- Your code goes here
+

Exercise False (practice)

Give analogues of True, toWitness, and fromWitness which work with negated properties. Call these False, toWitnessFalse, and fromWitnessFalse.

Exercise Bin-decidable (stretch)

Recall that Exercises Bin, Bin-laws, and Bin-predicates define a datatype Bin of bitstrings representing natural numbers, and asks you to define the following predicates:

One  : Bin → Set
+Can  : Bin → Set

Show that both of the above are decidable.

One? : ∀ (b : Bin) → Dec (One b)
+Can? : ∀ (b : Bin) → Dec (Can b)
\ No newline at end of file diff --git a/TSPL/2024/index.html b/TSPL/2024/index.html index 783334177..1f5a280c9 100644 --- a/TSPL/2024/index.html +++ b/TSPL/2024/index.html @@ -1 +1 @@ -Programming Language Foundations in Agda – TSPL
Programming Language Foundations in Agda

TSPL: Course notes (Fall 2024)

Staff

Lectures and tutorials

Lectures take place Tuesday, Wednesday, and Thursday weeks 4–10. Lectures on Tuesday and Thursday are immediately followed by a tutorial.

  • 12.10–14.00 Tuesday Lecture and Tutorial Teaching Room 13 (01M.473) - Doorway 3 - Medical School, Teviot
  • 12.10–13.00 Wednesday Lecture G.07 Meadows Lecture Theatre - Doorway 4 - Medical School, Teviot
  • 12.10–14.00 Thursday Lecture and Tutorial 5.3 - Lister Learning and Teaching Centre

Course textbook

Schedule

WeekMonWedFri
48 Oct Naturals9 Oct Induction10 Oct Relations
515 Oct Equality16 Oct Isomorphism17 Oct Connectives
622 Oct Negation23 Oct Quantifiers24 Oct Decidable
729 Oct Lists30 Oct Lambda31 Oct Lambda
85 Nov Properties6 Nov Properties7 Nov DeBruijn
912 Nov More13 Nov More14 Nov Inference
1019 Nov Inference20 Nov Untyped21 Nov Propositions as Types

Assessment

Assessment for the course is as follows.

  • four courseworks, marked best three out of four, 80%
  • project, take a research paper and formalise its development, 20%

Because there is no final, we need to be able to check that students can explain their work during tutorials. For this reason, you can only achieve marks on coursework if you have attended at least one of the four tutorial sessions in the week before it is due.

In order to conform with the University’s Common Marking Scheme, students may typically get only 10 points or less (out of 20) on the project. Attempting the project may not be a good use of time compared to other courses where there are easier marks to be had. Not all students are expected to attempt the project.

Coursework

For instructions on how to set up Agda for PLFA see Getting Started.

  • Assignment 1 cw1 due 12 noon Friday 18 October (Week 5)
  • Assignment 2 cw2 due 12 noon Friday 1 November (Week 7)
  • Assignment 3 cw3 due 12 noon Friday 15 November (Week 9)
  • Assignment 4 cw4 due 12 noon Friday 29 November (Week 11)
  • Essay cw5 due 12 noon Thursday 23 January 2025 (Week 2, Semester 2)

How to submit coursework

Go to the TSPL Learn course and select “Assessment” from the left hand menu. Select the “Assignment Submission” folder and then click on the link “submit your coursework here”. This will take you to the Gradescope interface.

For anyone who has sat an online exam, Gradescope should look familiar. Gradescope programming assignments differ from exams in that it offers three options for submitting your work:

  • Drag and drop your code file(s) into Gradescope
  • Submit a GitHub repository
  • Submit a Bitbucket repository

For the last two, you need to link your account to submit from GitHub or Bitbucket if you have not already. Instructions to do so are here.

Project

The optional project is to take a research paper and formalise all or part of it in Agda. In the past, some students have submitted superb optional projects that contributed to ongoing research. Talk to me about what you would like to submit.

Additional reading

\ No newline at end of file +Programming Language Foundations in Agda – TSPL
Programming Language Foundations in Agda

TSPL: Course notes (Fall 2024)

Staff

Lectures and tutorials

Lectures take place Tuesday, Wednesday, and Thursday weeks 4–10. Lectures on Tuesday and Thursday are immediately followed by a tutorial.

  • 12.10–14.00 Tuesday Lecture and Tutorial Teaching Room 13 (01M.473) - Doorway 3 - Medical School, Teviot
  • 12.10–13.00 Wednesday Lecture G.07 Meadows Lecture Theatre - Doorway 4 - Medical School, Teviot
  • 12.10–14.00 Thursday Lecture and Tutorial 5.3 - Lister Learning and Teaching Centre

Course textbook

Schedule

WeekMonWedFri
48 Oct Naturals9 Oct Induction10 Oct Relations
515 Oct Equality16 Oct Isomorphism17 Oct Connectives
622 Oct Negation23 Oct Quantifiers24 Oct Decidable
729 Oct Lists30 Oct Lambda31 Oct Lambda
85 Nov Properties6 Nov Properties7 Nov DeBruijn
912 Nov More13 Nov More14 Nov Inference
1019 Nov Inference20 Nov Untyped21 Nov Propositions as Types

Assessment

Assessment for the course is as follows.

  • four courseworks, marked best three out of four, 80%
  • essay, take a research paper and formalise its development, 20%

Because there is no final, we need to be able to check that students can explain their work during tutorials. For this reason, you can only achieve marks on coursework if you have attended at least one of the four tutorial sessions in the week before it is due.

In order to conform with the University’s Common Marking Scheme, students may typically get only 10 points or less (out of 20) on the essay. Attempting the essay may not be a good use of time compared to other courses where there are easier marks to be had. Not all students are expected to attempt the essay.

Coursework

For instructions on how to set up Agda for PLFA see Getting Started.

  • Assignment 1 cw1 due 12 noon Friday 18 October (Week 5)
  • Assignment 2 cw2 due 12 noon Friday 1 November (Week 7)
  • Assignment 3 cw3 due 12 noon Friday 15 November (Week 9)
  • Assignment 4 cw4 due 12 noon Friday 29 November (Week 11)
  • Essay cw5 due 12 noon Thursday 23 January 2025 (Week 2, Semester 2)

How to submit coursework

Go to the TSPL Learn course and select “Assessment” from the left hand menu. Select the “Assignment Submission” folder and then click on the link “submit your coursework here”. This will take you to the Gradescope interface.

For anyone who has sat an online exam, Gradescope should look familiar. Gradescope programming assignments differ from exams in that it offers three options for submitting your work:

  • Drag and drop your code file(s) into Gradescope
  • Submit a GitHub repository
  • Submit a Bitbucket repository

For the last two, you need to link your account to submit from GitHub or Bitbucket if you have not already. Instructions to do so are here.

Essay

The essay is to take a research paper and formalise all or part of it in Agda. In the past, some students have submitted superb essays that contributed to ongoing research. Talk to Prof Wadler about what you would like to submit.

Additional reading

\ No newline at end of file diff --git a/plfa.epub b/plfa.epub index b4545e847..d33dd7c2b 100644 Binary files a/plfa.epub and b/plfa.epub differ diff --git a/rss.xml b/rss.xml index 7c8268229..d7166e0f1 100644 --- a/rss.xml +++ b/rss.xml @@ -8,7 +8,7 @@ en - Fri, 11 Oct 2024 13:37:00 +0000 + Sat, 12 Oct 2024 11:58:41 +0000 Migration to Agda 2.7.0 https://plfa.github.io//2024/09/05/migration-to-agda-2-7-0/index.html