diff --git a/TSPL/2024/Assignment3/index.html b/TSPL/2024/Assignment3/index.html index 83aa1db03..919fdc424 100644 --- a/TSPL/2024/Assignment3/index.html +++ b/TSPL/2024/Assignment3/index.html @@ -14,153 +14,152 @@ open import plfa.part1.Isomorphism using (_≃_; _⇔_) 
  open import plfa.part1.Lists
     hiding (downFrom; Tree; leaf; node; merge)
-

Exercise reverse-++-distrib (practice) (recommended)

Show that the reverse of one list appended to another is the reverse of the second appended to the reverse of the first:

reverse (xs ++ ys) ≡ reverse ys ++ reverse xs

A function is an involution if when applied twice it acts as the identity function. Show that reverse is an involution:

reverse (reverse xs) ≡ xs

Exercise map-compose (practice)

Prove that the map of a composition is equal to the composition of two maps:

map (g ∘ f) ≡ map g ∘ map f

The last step of the proof requires extensionality.

  -- Your code goes here
-

Exercise map-++-distribute (practice)

Prove the following relationship between map and append:

map f (xs ++ ys) ≡ map f xs ++ map f ys
  -- Your code goes here
-

Exercise map-Tree (practice)

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:

map-Tree : ∀ {A B C D : Set} → (A → C) → (B → D) → Tree A B → Tree C D
  -- Your code goes here
-

Use fold to define a function to find the product of a list of numbers. For example:

product [ 1 , 2 , 3 , 4 ] ≡ 24
  -- Your code goes here
-

Exercise foldr-++ (practice) (was recommended)

Show that fold and append are related as follows:

foldr _⊗_ e (xs ++ ys) ≡ foldr _⊗_ (foldr _⊗_ e ys) xs
  -- Your code goes here
-

Exercise foldr-∷ (practice)

Show

foldr _∷_ [] xs ≡ xs

Show as a consequence of foldr-++ above that

xs ++ ys ≡ foldr _∷_ ys xs
  -- Your code goes here
-

Exercise map-is-foldr (practice)

Show that map can be defined using fold:

map f ≡ foldr (λ x xs → f x ∷ xs) []

The proof requires extensionality.

  -- Your code goes here
-

Exercise fold-Tree (practice)

Define a suitable fold function for the type of trees given earlier:

fold-Tree : ∀ {A B C : Set} → (A → C) → (C → B → C → C) → Tree A B → C
  -- Your code goes here
-

Exercise map-is-fold-Tree (practice)

Demonstrate an analogue of map-is-foldr for the type of trees.

  -- Your code goes here
-

Exercise sum-downFrom (practice) (was 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:

sum (downFrom n) * 2 ≡ n * (n ∸ 1)
  -- Your code goes here
+

Exercise reverse-++-distrib (recommended)

Show that the reverse of one list appended to another is the reverse of the second appended to the reverse of the first:

reverse (xs ++ ys) ≡ reverse ys ++ reverse xs

A function is an involution if when applied twice it acts as the identity function. Show that reverse is an involution:

reverse (reverse xs) ≡ xs

Exercise map-compose (practice)

Prove that the map of a composition is equal to the composition of two maps:

map (g ∘ f) ≡ map g ∘ map f

The last step of the proof requires extensionality.

  -- Your code goes here
+

Exercise map-++-distribute (practice)

Prove the following relationship between map and append:

map f (xs ++ ys) ≡ map f xs ++ map f ys
  -- Your code goes here
+

Exercise map-Tree (practice)

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:

map-Tree : ∀ {A B C D : Set} → (A → C) → (B → D) → Tree A B → Tree C D
  -- Your code goes here
+

Use fold to define a function to find the product of a list of numbers. For example:

product [ 1 , 2 , 3 , 4 ] ≡ 24
  -- Your code goes here
+

Exercise foldr-++ (recommended)

Show that fold and append are related as follows:

foldr _⊗_ e (xs ++ ys) ≡ foldr _⊗_ (foldr _⊗_ e ys) xs
  -- Your code goes here
+

Exercise foldr-∷ (practice)

Show

foldr _∷_ [] xs ≡ xs

Show as a consequence of foldr-++ above that

xs ++ ys ≡ foldr _∷_ ys xs
  -- Your code goes here
+

Exercise map-is-foldr (practice)

Show that map can be defined using fold:

map f ≡ foldr (λ x xs → f x ∷ xs) []

The proof requires extensionality.

  -- Your code goes here
+

Exercise fold-Tree (practice)

Define a suitable fold function for the type of trees given earlier:

fold-Tree : ∀ {A B C : Set} → (A → C) → (C → B → C → C) → Tree A B → C
  -- Your code goes here
+

Exercise map-is-fold-Tree (practice)

Demonstrate an analogue of map-is-foldr for the type of trees.

  -- Your code goes here
+

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:

sum (downFrom n) * 2 ≡ n * (n ∸ 1)
  -- Your code goes here

Exercise foldl (practice)

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
  -- Your code goes here
-

Exercise foldr-monoid-foldl (practice)

Show that if _⊗_ and e form a monoid, then foldr _⊗_ e and foldl _⊗_ e always compute the same result.

  -- Your code goes here
-

Exercise Any-++-⇔ (practice) (was 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 _++_.

  -- Your code goes here
-

Exercise All-++-≃ (practice) (was stretch)

Show that the equivalence All-++-⇔ can be extended to an isomorphism.

  -- Your code goes here
-

Show that Any and All satisfy a version of De Morgan’s Law:

(¬_ ∘ Any P) xs ⇔ All (¬_ ∘ P) xs

(Can you see why it is important that here _∘_ is generalised to arbitrary levels, as described in the section on universe polymorphism?)

Do we also have the following?

(¬_ ∘ All P) xs ⇔ Any (¬_ ∘ P) xs

If so, prove; if not, explain why.

  -- Your code goes here
-

Exercise ¬Any≃All¬ (practice) (was stretch)

Show that the equivalence ¬Any⇔All¬ can be extended to an isomorphism. You will need to use extensionality.

  -- Your code goes here
-

Exercise All-∀ (practice)

Show that All P xs is isomorphic to ∀ x → x ∈ xs → P x.

  -- You code goes here
-

Exercise Any-∃ (practice)

Show that Any P xs is isomorphic to ∃[ x ] (x ∈ xs × P x).

  -- You code goes here
-

Exercise Any? (practice) (was 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 predicate holds for some element of a list. Give their definitions.

  -- Your code goes here
-

Exercise split (practice) (was stretch)

The relation merge holds when two lists merge to give a third list.
  data merge {A : Set} : (xs ys zs : List A) → Set where
+foldl _⊗_ e [ x , y , z ]  =  ((e ⊗ x) ⊗ y) ⊗ z
  -- Your code goes here
+

Exercise foldr-monoid-foldl (practice)

Show that if _⊗_ and e form a monoid, then foldr _⊗_ e and foldl _⊗_ e always compute the same result.

  -- Your code goes here
+

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 _++_.

  -- Your code goes here
+

Exercise All-++-≃ (stretch)

Show that the equivalence All-++-⇔ can be extended to an isomorphism.

  -- Your code goes here
+

Show that Any and All satisfy a version of De Morgan’s Law:

(¬_ ∘ Any P) xs ⇔ All (¬_ ∘ P) xs

(Can you see why it is important that here _∘_ is generalised to arbitrary levels, as described in the section on universe polymorphism?)

Do we also have the following?

(¬_ ∘ All P) xs ⇔ Any (¬_ ∘ P) xs

If so, prove; if not, explain why.

  -- Your code goes here
+

Exercise ¬Any≃All¬ (stretch)

Show that the equivalence ¬Any⇔All¬ can be extended to an isomorphism. You will need to use extensionality.

  -- Your code goes here
+

Exercise All-∀ (practice)

Show that All P xs is isomorphic to ∀ x → x ∈ xs → P x.

  -- You code goes here
+

Exercise Any-∃ (practice)

Show that Any P xs is isomorphic to ∃[ x ] (x ∈ xs × P x).

  -- You code goes here
+

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 predicate holds for some element of a list. Give their definitions.

  -- Your code goes here
+

Exercise split (stretch)

The relation merge holds when two lists merge to give a third list.
  data merge {A : Set} : (xs ys zs : List A) → Set where
 
-    [] :
-        --------------
-        merge [] [] []
+    [] :
+        --------------
+        merge [] [] []
 
-    left-∷ : ∀ {x xs ys zs}
-      → merge xs ys zs
-        --------------------------
-      → merge (x ∷ xs) ys (x ∷ zs)
+    left-∷ : ∀ {x xs ys zs}
+      → merge xs ys zs
+        --------------------------
+      → merge (x ∷ xs) ys (x ∷ zs)
 
-    right-∷ : ∀ {y xs ys zs}
-      → merge xs ys zs
-        --------------------------
-      → merge xs (y ∷ ys) (y ∷ zs)
-
For example,
  _ : merge [ 1 , 4 ] [ 2 , 3 ] [ 1 , 2 , 3 , 4 ]
-  _ = left-∷ (right-∷ (right-∷ (left-∷ [])))
+    right-∷ : ∀ {y xs ys zs}
+      → merge xs ys zs
+        --------------------------
+      → merge xs (y ∷ ys) (y ∷ zs)
+
For example,
  _ : merge [ 1 , 4 ] [ 2 , 3 ] [ 1 , 2 , 3 , 4 ]
+  _ = left-∷ (right-∷ (right-∷ (left-∷ [])))

Given a decidable predicate and a list, we can split the list into two lists that merge to give the original list, where all elements of one list satisfy the predicate, and all elements of the other do not satisfy the predicate.

Define the following variant of the traditional filter function on lists, which given a decidable predicate and a list returns a list of elements that satisfy the predicate and a list of elements that don’t, with their corresponding proofs.

split : ∀ {A : Set} {P : A → Set} (P? : Decidable P) (zs : List A)
-  → ∃[ xs ] ∃[ ys ] ( merge xs ys zs × All P xs × All (¬_ ∘ P) ys )
  -- Your code goes here
-

Lambda

module Lambda where
-

Imports

  open import Data.Bool using (Bool; true; false; T; not)
-  open import Data.Empty using (⊥; ⊥-elim)
-  open import Data.List using (List; _∷_; [])
-  open import Data.Nat using (ℕ; zero; suc)
-  open import Data.Product using (∃-syntax; _×_)
-  open import Data.String using (String; _≟_)
-  open import Data.Unit using (tt)
-  open import Relation.Nullary using (Dec; yes; no; ¬_)
-  open import Relation.Nullary.Decidable using (False; toWitnessFalse)
-  open import Relation.Nullary.Negation using (¬?)
-  open import Relation.Binary.PropositionalEquality using (_≡_; _≢_; refl)
-
  open import plfa.part2.Lambda
-    hiding (var?; ƛ′_⇒_; case′_[zero⇒_|suc_⇒_]; μ′_⇒_; plus′)
-

Write out the definition of a lambda term that multiplies two natural numbers. Your definition may use plus as defined earlier.

  -- Your code goes here
-

Exercise mulᶜ (practice)

Write out the definition of a lambda term that multiplies two natural numbers represented as Church numerals. Your definition may use plusᶜ as defined earlier (or may not — there are nice definitions both ways).

  -- Your code goes here
-

Exercise primed (stretch)

Some people find it annoying to write ` "x" instead of x. We can make examples with lambda terms slightly easier to write by adding the following definitions:
  var? : (t : Term) → Bool
-  var? (` _)  =  true
-  var? _      =  false
+  → ∃[ xs ] ∃[ ys ] ( merge xs ys zs × All P xs × All (¬_ ∘ P) ys )
  -- Your code goes here
+

Lambda

module Lambda where
+

Imports

  open import Data.Bool using (Bool; true; false; T; not)
+  open import Data.Empty using (⊥; ⊥-elim)
+  open import Data.List using (List; _∷_; [])
+  open import Data.Nat using (ℕ; zero; suc)
+  open import Data.Product using (∃-syntax; _×_)
+  open import Data.String using (String; _≟_)
+  open import Data.Unit using (tt)
+  open import Relation.Nullary using (Dec; yes; no; ¬_)
+  open import Relation.Nullary.Decidable using (False; toWitnessFalse; ¬?)
+  open import Relation.Binary.PropositionalEquality using (_≡_; _≢_; refl)
+
  open import plfa.part2.Lambda
+    hiding (var?; ƛ′_⇒_; case′_[zero⇒_|suc_⇒_]; μ′_⇒_; plus′)
+

Write out the definition of a lambda term that multiplies two natural numbers. Your definition may use plus as defined earlier.

  -- Your code goes here
+

Exercise mulᶜ (practice)

Write out the definition of a lambda term that multiplies two natural numbers represented as Church numerals. Your definition may use plusᶜ as defined earlier (or may not — there are nice definitions both ways).

  -- Your code goes here
+

Exercise primed (stretch)

Some people find it annoying to write ` "x" instead of x. We can make examples with lambda terms slightly easier to write by adding the following definitions:
  var? : (t : Term) → Bool
+  var? (` _)  =  true
+  var? _      =  false
 
-  ƛ′_⇒_ : (t : Term) → {_ : T (var? t)} → Term → Term
-  ƛ′_⇒_ (` x) N = ƛ x ⇒ N
+  ƛ′_⇒_ : (t : Term) → {_ : T (var? t)} → Term → Term
+  ƛ′_⇒_ (` x) N = ƛ x ⇒ N
 
-  case′_[zero⇒_|suc_⇒_] : Term → Term → (t : Term) → {_ : T (var? t)} → Term → Term
-  case′ L [zero⇒ M |suc (` x) ⇒ N ]  =  case L [zero⇒ M |suc x ⇒ N ]
+  case′_[zero⇒_|suc_⇒_] : Term → Term → (t : Term) → {_ : T (var? t)} → Term → Term
+  case′ L [zero⇒ M |suc (` x) ⇒ N ]  =  case L [zero⇒ M |suc x ⇒ N ]
 
-  μ′_⇒_ : (t : Term) → {_ : T (var? t)} → Term → Term
-  μ′ (` x) ⇒ N  =  μ x ⇒ N
+  μ′_⇒_ : (t : Term) → {_ : T (var? t)} → Term → Term
+  μ′ (` x) ⇒ N  =  μ x ⇒ N

Recall that T is a function that maps from the computation world to the evidence world, as defined in Chapter Decidable. We ensure to use the primed functions only when the respective term argument is a variable, which we do by providing implicit evidence. For example, if we tried to define an abstraction term that binds anything but a variable:

_ : Term
-_ = ƛ′ two ⇒ two

Agda would complain it cannot find a value of the bottom type for the implicit argument. Note the implicit argument’s type reduces to ⊥ when term t is anything but a variable.

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.

  -- Your code goes here
-

Exercise —↠≲—↠′ (practice)

Show that the first notion of reflexive and transitive closure above embeds into the second. Why are they not isomorphic?

  -- Your code goes here
-

Exercise plus-example (practice)

Write out the reduction sequence demonstrating that one plus one is two.

  -- Your code goes here
-

Exercise Context-≃ (practice)

Show that Context is isomorphic to List (Id × Type). For instance, the isomorphism relates the context

∅ , "s" ⦂ `ℕ ⇒ `ℕ , "z" ⦂ `ℕ

to the list

[ ⟨ "z" , `ℕ ⟩ , ⟨ "s" , `ℕ ⇒ `ℕ ⟩ ]
  -- Your code goes here
-

Using the term mul you defined earlier, write out the derivation showing that it is well typed.

  -- Your code goes here
-

Exercise ⊢mulᶜ (practice)

Using the term mulᶜ you defined earlier, write out the derivation showing that it is well typed.

  -- Your code goes here
-

Properties

module Properties where
-

Imports

  open import Relation.Binary.PropositionalEquality
-    using (_≡_; _≢_; refl; sym; cong; cong₂)
-  open import Data.String using (String; _≟_)
-  open import Data.Nat using (ℕ; zero; suc)
-  open import Data.Empty using (⊥; ⊥-elim)
-  open import Data.Product
-    using (_×_; proj₁; proj₂; ∃; ∃-syntax)
-    renaming (_,_ to ⟨_,_⟩)
-  open import Data.Sum using (_⊎_; inj₁; inj₂)
-  open import Relation.Nullary using (¬_; Dec; yes; no)
-  open import Function using (_∘_)
-  open import plfa.part1.Isomorphism
-  open import plfa.part2.Lambda
-
  open import plfa.part2.Properties
-    hiding (value?; Canonical_⦂_; unstuck; preserves; wttdgs)
-  -- open Lambda using (mul; ⊢mul)
-

Exercise Canonical-≃ (practice)

Well-typed values must take one of a small number of canonical forms, which provide an analogue of the Value relation that relates values to their types. A lambda expression must have a function type, and a zero or successor expression must be a natural. Further, the body of a function must be well typed in a context containing only its bound variable, and the argument of successor must itself be canonical:
  infix  4 Canonical_⦂_
+_ = ƛ′ two ⇒ two

Agda would complain it cannot find a value of the bottom type for the implicit argument. Note the implicit argument’s type reduces to ⊥ when term t is anything but a variable.

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.

  -- Your code goes here
+

Exercise —↠≲—↠′ (practice)

Show that the first notion of reflexive and transitive closure above embeds into the second. Why are they not isomorphic?

  -- Your code goes here
+

Exercise plus-example (practice)

Write out the reduction sequence demonstrating that one plus one is two.

  -- Your code goes here
+

Exercise Context-≃ (practice)

Show that Context is isomorphic to List (Id × Type). For instance, the isomorphism relates the context

∅ , "s" ⦂ `ℕ ⇒ `ℕ , "z" ⦂ `ℕ

to the list

[ ⟨ "z" , `ℕ ⟩ , ⟨ "s" , `ℕ ⇒ `ℕ ⟩ ]
  -- Your code goes here
+

Using the term mul you defined earlier, write out the derivation showing that it is well typed.

  -- Your code goes here
+

Exercise ⊢mulᶜ (practice)

Using the term mulᶜ you defined earlier, write out the derivation showing that it is well typed.

  -- Your code goes here
+

Properties

module Properties where
+

Imports

  open import Relation.Binary.PropositionalEquality
+    using (_≡_; _≢_; refl; sym; cong; cong₂)
+  open import Data.String using (String; _≟_)
+  open import Data.Nat using (ℕ; zero; suc)
+  open import Data.Empty using (⊥; ⊥-elim)
+  open import Data.Product
+    using (_×_; proj₁; proj₂; ∃; ∃-syntax)
+    renaming (_,_ to ⟨_,_⟩)
+  open import Data.Sum using (_⊎_; inj₁; inj₂)
+  open import Relation.Nullary using (¬_; Dec; yes; no)
+  open import Function using (_∘_)
+  open import plfa.part1.Isomorphism
+  open import plfa.part2.Lambda
+
  open import plfa.part2.Properties
+    hiding (value?; Canonical_⦂_; unstuck; preserves; wttdgs)
+  -- open Lambda using (mul; ⊢mul)
+

Exercise Canonical-≃ (practice)

Well-typed values must take one of a small number of canonical forms, which provide an analogue of the Value relation that relates values to their types. A lambda expression must have a function type, and a zero or successor expression must be a natural. Further, the body of a function must be well typed in a context containing only its bound variable, and the argument of successor must itself be canonical:
  infix  4 Canonical_⦂_
 
-  data Canonical_⦂_ : Term → Type → Set where
+  data Canonical_⦂_ : Term → Type → Set where
 
-    C-ƛ : ∀ {x A N B}
-      → ∅ , x ⦂ A ⊢ N ⦂ B
-        -----------------------------
-      → Canonical (ƛ x ⇒ N) ⦂ (A ⇒ B)
+    C-ƛ : ∀ {x A N B}
+      → ∅ , x ⦂ A ⊢ N ⦂ B
+        -----------------------------
+      → Canonical (ƛ x ⇒ N) ⦂ (A ⇒ B)
 
-    C-zero :
-        --------------------
-        Canonical `zero ⦂ `ℕ
+    C-zero :
+        --------------------
+        Canonical `zero ⦂ `ℕ
 
-    C-suc : ∀ {V}
-      → Canonical V ⦂ `ℕ
-        ---------------------
-      → Canonical `suc V ⦂ `ℕ
-

Show that Canonical V ⦂ A is isomorphic to (∅ ⊢ V ⦂ A) × (Value V), that is, the canonical forms are exactly the well-typed values.

  -- Your code goes here
-

Exercise Progress-≃ (practice)

Show that Progress M is isomorphic to Value M ⊎ ∃[ N ](M —→ N).

  -- Your code goes here
-

Exercise progress′ (practice)

Write out the proof of progress′ in full, and compare it to the proof of progress above.

  -- Your code goes here
-

Exercise value? (practice)

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.

  -- Your code goes here
-

Using the evaluator, confirm that two times two is four.

  -- Your code goes here
-

Exercise: progress-preservation (practice)

Without peeking at their statements above, write down the progress and preservation theorems for the simply typed lambda-calculus.

  -- Your code goes here
-

Exercise subject_expansion (practice)

We say that M reduces to N if M —→ N, but we can also describe the same situation by saying that N expands to 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.

  -- Your code goes here
-

Exercise stuck (practice)

Give an example of an ill-typed term that does get stuck.

  -- Your code goes here
-

Provide proofs of the three postulates, unstuck, preserves, and wttdgs above.

  -- Your code goes here
-

DeBruijn

module DeBruijn where
-

Imports

  import Relation.Binary.PropositionalEquality as Eq
-  open Eq using (_≡_; refl)
-  open import Data.Empty using (⊥; ⊥-elim)
-  open import Data.Nat using (ℕ; zero; suc; _<_; _≤?_; z≤n; s≤s)
-  open import Relation.Nullary using (¬_)
-  open import Relation.Nullary.Decidable using (True; toWitness)
-
  open import plfa.part2.DeBruijn
-    hiding ()
-

Write out the definition of a lambda term that multiplies two natural numbers, now adapted to the intrinsically-typed de Bruijn representation.

  -- Your code goes here
-

Exercise V¬—→ (practice)

Following the previous development, show values do not reduce, and its corollary, terms that reduce are not values.

  -- Your code goes here
-

Using the evaluator, confirm that two times two is four.

  -- Your code goes here
+    C-suc : ∀ {V}
+      → Canonical V ⦂ `ℕ
+        ---------------------
+      → Canonical `suc V ⦂ `ℕ
+

Show that Canonical V ⦂ A is isomorphic to (∅ ⊢ V ⦂ A) × (Value V), that is, the canonical forms are exactly the well-typed values.

  -- Your code goes here
+

Exercise Progress-≃ (practice)

Show that Progress M is isomorphic to Value M ⊎ ∃[ N ](M —→ N).

  -- Your code goes here
+

Exercise progress′ (practice)

Write out the proof of progress′ in full, and compare it to the proof of progress above.

  -- Your code goes here
+

Exercise value? (practice)

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.

  -- Your code goes here
+

Using the evaluator, confirm that two times two is four.

  -- Your code goes here
+

Exercise: progress-preservation (practice)

Without peeking at their statements above, write down the progress and preservation theorems for the simply typed lambda-calculus.

  -- Your code goes here
+

Exercise subject_expansion (practice)

We say that M reduces to N if M —→ N, but we can also describe the same situation by saying that N expands to 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.

  -- Your code goes here
+

Exercise stuck (practice)

Give an example of an ill-typed term that does get stuck.

  -- Your code goes here
+

Provide proofs of the three postulates, unstuck, preserves, and wttdgs above.

  -- Your code goes here
+

DeBruijn

module DeBruijn where
+

Imports

  import Relation.Binary.PropositionalEquality as Eq
+  open Eq using (_≡_; refl)
+  open import Data.Empty using (⊥; ⊥-elim)
+  open import Data.Nat using (ℕ; zero; suc; _<_; _≤?_; z≤n; s≤s)
+  open import Relation.Nullary using (¬_)
+  open import Relation.Nullary.Decidable using (True; toWitness)
+
  open import plfa.part2.DeBruijn
+    hiding ()
+

Write out the definition of a lambda term that multiplies two natural numbers, now adapted to the intrinsically-typed de Bruijn representation.

  -- Your code goes here
+

Exercise V¬—→ (practice)

Following the previous development, show values do not reduce, and its corollary, terms that reduce are not values.

  -- Your code goes here
+

Using the evaluator, confirm that two times two is four.

  -- Your code goes here
\ No newline at end of file diff --git a/plfa.epub b/plfa.epub index 59aa04a26..895060766 100644 Binary files a/plfa.epub and b/plfa.epub differ diff --git a/plfa.html b/plfa.html index d0f7c47e1..f0b67ae1b 100644 --- a/plfa.html +++ b/plfa.html @@ -1,4 +1,4 @@ -Programming Language Foundations in Agda – Programming Language Foundations in Agda

Programming Language Foundations in Agda

Philip Wadler

Wen Kokke

Jeremy G. Siek

2024-11

Creative Commons Attribution 4.0 International License

Front matter

Dedication

de Philip, para Wanda

amor da minha vida

knock knock knock

…

Preface

The most profound connection between logic and computation is a pun. The doctrine of Propositions as Types asserts that a certain kind of formal structure may be read in two ways: either as a proposition in logic or as a type in computing. Further, a related structure may be read as either the proof of the proposition or as a programme of the corresponding type. Further still, simplification of proofs corresponds to evaluation of programs.

Accordingly, the title of this book also has two readings. It may be parsed as “(Programming Language) Foundations in Agda” or “Programming (Language Foundations) in Agda” — the specifications we will write in the proof assistant Agda both describe programming languages and are themselves programmes.

The book is aimed at students in the last year of an undergraduate honours programme or the first year of a master or doctorate degree. It aims to teach the fundamentals of operational semantics of programming languages, with simply-typed lambda calculus as the central example. The textbook is written as a literate script in Agda. The hope is that using a proof assistant will make the development more concrete and accessible to students, and give them rapid feedback to find and correct misapprehensions.

The book is broken into two parts. The first part, Logical Foundations, develops the needed formalisms. The second part, Programming Language Foundations, introduces basic methods of operational semantics.

Personal remarks

Since 2013, I have taught a course on Types and Semantics for Programming Languages to fourth-year undergraduates and masters students at the University of Edinburgh. An earlier version of that course was based on Benjamin Pierce’s excellent TAPL. My version was based of Pierce’s subsequent textbook, Software Foundations, written in collaboration with others and based on Coq. I am convinced of Pierce’s claim that basing a course around a proof assistant aids learning, as summarised in his ICFP Keynote, Lambda, The Ultimate TA.

However, after five years of experience, I have come to the conclusion that Coq is not the best vehicle. Too much of the course needs to focus on learning tactics for proof derivation, to the cost of learning the fundamentals of programming language theory. Every concept has to be learned twice: e.g., both the product data type, and the corresponding tactics for introduction and elimination of conjunctions. The rules Coq applies to generate induction hypotheses can sometimes seem mysterious. While the notation construct permits pleasingly flexible syntax, it can be confusing that the same concept must always be given two names, e.g., both subst N x M and N [x := M]. Names of tactics are sometimes short and sometimes long; naming conventions in the standard library can be wildly inconsistent. Propositions as types as a foundation of proof is present but hidden.

I found myself keen to recast the course in Agda. In Agda, there is no longer any need to learn about tactics: there is just dependently-typed programming, plain and simple. Introduction is always by a constructor, elimination is always by pattern matching. Induction is no longer a mysterious separate concept, but corresponds to the familiar notion of recursion. Mixfix syntax is flexible while using just one name for each concept, e.g., substitution is _[_:=_]. The standard library is not perfect, but there is a fair attempt at consistency. Propositions as types as a foundation of proof is on proud display.

Alas, there is no textbook for programming language theory in Agda. Stump’s Verified Functional Programming in Agda covers related ground, but focusses more on programming with dependent types than on the theory of programming languages.

The original goal was to simply adapt Software Foundations, maintaining the same text but transposing the code from Coq to Agda. But it quickly became clear to me that after five years in the classroom I had my own ideas about how to present the material. They say you should never write a book unless you cannot not write the book, and I soon found that this was a book I could not not write.

I am fortunate that my student, Wen Kokke, was keen to help. She guided me as a newbie to Agda and provided an infrastructure that is easy to use and produces pages that are a pleasure to view.

Most of the text was written during a sabbatical in the first half of 2018.

— Philip Wadler, Rio de Janeiro, January–June 2018

A word on the exercises

Exercises labelled “(recommended)” are the ones students are required to do in the class taught at Edinburgh from this textbook.

Exercises labelled “(stretch)” are there to provide an extra challenge. Few students do all of these, but most attempt at least a few.

Exercises labelled “(practice)” are included for those who want extra practice.

You may answer the exercises by downloading the book from github and editing where it says “– Your code goes here”. Alternatively, you may be given a file to edit containing exercises for a given coursework.

In either case, you may need to import additional library functions required for the solution. You may also need to set up PLFA as an Agda library, as described in Getting Started.

Please do not post answers to the exercises in a public place.

There is a private repository of answers to selected questions on github. Please contact Philip Wadler if you would like to access it.

Getting Started

CIpre-commit.ci statusRelease Versionagdastandard-library

Getting Started for Readers

You can read PLFA online without installing anything. However, if you wish to interact with the code or complete the exercises, you need several things:

PLFA is tested against specific versions of Agda and the standard library, which are shown in the badges above. Agda and the standard library change rapidly, and these changes often break PLFA, so using older or newer versions usually causes problems.

There are several versions of Agda and its standard library online. If you are using a package manager, like Homebrew or Debian apt, the version of Agda available there may be out of date. Furthermore, Agda is under active development, so if you install the development version from the GitHub, you might find the developers have introduced changes which break the code here. Therefore, it’s important to have the specific versions of Agda and the standard library shown above.

On macOS: Install the XCode Command Line Tools

On macOS, you’ll need to install The XCode Command Line Tools. For most versions of macOS, you can install these by running the following command:

xcode-select --install

Install Git

You can check whether you have Git by running the following command:

git --version

If you do not have Git, see the Git downloads page.

Install GHC and Cabal

Agda is written in Haskell, so to install it we’ll need the Glorious Haskell Compiler and its package manager Cabal. PLFA should work with any version of GHC >=8.10, but is tested with versions 8.10 – 9.8. We recommend installing GHC and Cabal using ghcup. For instance, once ghcup is installed, by typing

ghcup install ghc 9.4.8
+Programming Language Foundations in Agda – Programming Language Foundations in Agda
Programming Language Foundations in Agda
Philip Wadler
Wen Kokke
Jeremy G. Siek
2024-11
Creative Commons Attribution 4.0 International License
Front matter
Dedication
de Philip, para Wanda
amor da minha vida
knock knock knock
…
Preface
The most profound connection between logic and computation is a pun. The doctrine of Propositions as Types asserts that a certain kind of formal structure may be read in two ways: either as a proposition in logic or as a type in computing. Further, a related structure may be read as either the proof of the proposition or as a programme of the corresponding type. Further still, simplification of proofs corresponds to evaluation of programs.
Accordingly, the title of this book also has two readings. It may be parsed as “(Programming Language) Foundations in Agda” or “Programming (Language Foundations) in Agda” — the specifications we will write in the proof assistant Agda both describe programming languages and are themselves programmes.
The book is aimed at students in the last year of an undergraduate honours programme or the first year of a master or doctorate degree. It aims to teach the fundamentals of operational semantics of programming languages, with simply-typed lambda calculus as the central example. The textbook is written as a literate script in Agda. The hope is that using a proof assistant will make the development more concrete and accessible to students, and give them rapid feedback to find and correct misapprehensions.
The book is broken into two parts. The first part, Logical Foundations, develops the needed formalisms. The second part, Programming Language Foundations, introduces basic methods of operational semantics.
Personal remarks
Since 2013, I have taught a course on Types and Semantics for Programming Languages to fourth-year undergraduates and masters students at the University of Edinburgh. An earlier version of that course was based on Benjamin Pierce’s excellent TAPL. My version was based of Pierce’s subsequent textbook, Software Foundations, written in collaboration with others and based on Coq. I am convinced of Pierce’s claim that basing a course around a proof assistant aids learning, as summarised in his ICFP Keynote, Lambda, The Ultimate TA.
However, after five years of experience, I have come to the conclusion that Coq is not the best vehicle. Too much of the course needs to focus on learning tactics for proof derivation, to the cost of learning the fundamentals of programming language theory. Every concept has to be learned twice: e.g., both the product data type, and the corresponding tactics for introduction and elimination of conjunctions. The rules Coq applies to generate induction hypotheses can sometimes seem mysterious. While the notation construct permits pleasingly flexible syntax, it can be confusing that the same concept must always be given two names, e.g., both subst N x M and N [x := M]. Names of tactics are sometimes short and sometimes long; naming conventions in the standard library can be wildly inconsistent. Propositions as types as a foundation of proof is present but hidden.
I found myself keen to recast the course in Agda. In Agda, there is no longer any need to learn about tactics: there is just dependently-typed programming, plain and simple. Introduction is always by a constructor, elimination is always by pattern matching. Induction is no longer a mysterious separate concept, but corresponds to the familiar notion of recursion. Mixfix syntax is flexible while using just one name for each concept, e.g., substitution is _[_:=_]. The standard library is not perfect, but there is a fair attempt at consistency. Propositions as types as a foundation of proof is on proud display.
Alas, there is no textbook for programming language theory in Agda. Stump’s Verified Functional Programming in Agda covers related ground, but focusses more on programming with dependent types than on the theory of programming languages.
The original goal was to simply adapt Software Foundations, maintaining the same text but transposing the code from Coq to Agda. But it quickly became clear to me that after five years in the classroom I had my own ideas about how to present the material. They say you should never write a book unless you cannot not write the book, and I soon found that this was a book I could not not write.
I am fortunate that my student, Wen Kokke, was keen to help. She guided me as a newbie to Agda and provided an infrastructure that is easy to use and produces pages that are a pleasure to view.
Most of the text was written during a sabbatical in the first half of 2018.
— Philip Wadler, Rio de Janeiro, January–June 2018
A word on the exercises
Exercises labelled “(recommended)” are the ones students are required to do in the class taught at Edinburgh from this textbook.
Exercises labelled “(stretch)” are there to provide an extra challenge. Few students do all of these, but most attempt at least a few.
Exercises labelled “(practice)” are included for those who want extra practice.
You may answer the exercises by downloading the book from github and editing where it says “– Your code goes here”. Alternatively, you may be given a file to edit containing exercises for a given coursework.
In either case, you may need to import additional library functions required for the solution. You may also need to set up PLFA as an Agda library, as described in Getting Started.
Please do not post answers to the exercises in a public place.
There is a private repository of answers to selected questions on github. Please contact Philip Wadler if you would like to access it.
Getting Started
CIpre-commit.ci statusRelease Versionagdastandard-library
Getting Started for Readers
You can read PLFA online without installing anything. However, if you wish to interact with the code or complete the exercises, you need several things:
PLFA is tested against specific versions of Agda and the standard library, which are shown in the badges above. Agda and the standard library change rapidly, and these changes often break PLFA, so using older or newer versions usually causes problems.
There are several versions of Agda and its standard library online. If you are using a package manager, like Homebrew or Debian apt, the version of Agda available there may be out of date. Furthermore, Agda is under active development, so if you install the development version from the GitHub, you might find the developers have introduced changes which break the code here. Therefore, it’s important to have the specific versions of Agda and the standard library shown above.
On macOS: Install the XCode Command Line Tools
On macOS, you’ll need to install The XCode Command Line Tools. For most versions of macOS, you can install these by running the following command:
xcode-select --install
Install Git
You can check whether you have Git by running the following command:
git --version
If you do not have Git, see the Git downloads page.
Install GHC and Cabal
Agda is written in Haskell, so to install it we’ll need the Glorious Haskell Compiler and its package manager Cabal. PLFA should work with any version of GHC >=8.10, but is tested with versions 8.10 – 9.8. We recommend installing GHC and Cabal using ghcup. For instance, once ghcup is installed, by typing
ghcup install ghc 9.4.8
 ghcup install cabal recommended
 
 ghcup set ghc 9.4.8
diff --git a/rss.xml b/rss.xml
index 9e6cd652f..7c75ed1b1 100644
--- a/rss.xml
+++ b/rss.xml
@@ -8,7 +8,7 @@
     
     en
     
-    Tue, 05 Nov 2024 11:24:45 +0000
+    Wed, 06 Nov 2024 00:18:00 +0000
         
       Migration to Agda 2.7.0
       https://plfa.github.io//2024/09/05/migration-to-agda-2-7-0/index.html