module Assignment3 where

YOUR NAME AND EMAIL GOES HERE

Introduction

You must do all the exercises labelled “(recommended)”.

Exercises labelled “(stretch)” are there to provide an extra challenge. You don’t need to do all of these, but should attempt at least a few.

Exercises without a label are optional, and may be done if you want some extra practice.

Please ensure your files execute correctly under Agda!

Imports

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; cong; sym)
open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; _≡⟨_⟩_; _∎)
open import Data.Bool.Base using (Bool; true; false; T; _∧_; _∨_; not)
open import Data.Nat using (ℕ; zero; suc; _+_; _*_; _∸_; _≤_; s≤s; z≤n)
open import Data.Nat.Properties using
  (+-assoc; +-identityˡ; +-identityʳ; *-assoc; *-identityˡ; *-identityʳ)
open import Relation.Nullary using (¬_; Dec; yes; no)
open import Data.Product using (_×_; ∃; ∃-syntax) renaming (_,_ to ⟨_,_⟩)
open import Data.Empty using (⊥; ⊥-elim)
open import Function using (_∘_)
open import Algebra.Structures using (IsMonoid)
open import Level using (Level)
open import Relation.Unary using (Decidable)
open import plfa.part1.Relations using (_<_; z<s; s<s)
open import plfa.part1.Isomorphism using (_≃_; ≃-sym; ≃-trans; _≲_; extensionality)
open plfa.part1.Isomorphism.≃-Reasoning
open import plfa.part1.Lists using (List; []; _∷_; [_]; [_,_]; [_,_,_]; [_,_,_,_];
  _++_; reverse; map; foldr; sum; All; Any; here; there; _∈_)
open import plfa.part2.Lambda hiding (ƛ′_⇒_; case′_[zero⇒_|suc_⇒_]; μ′_⇒_; plus′)
open import plfa.part2.Properties hiding (value?; unstuck; preserves; wttdgs)

Exercise reverse-++-commute (recommended)

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

postulate
  reverse-++-commute : ∀ {A : Set} {xs ys : List A}
    → reverse (xs ++ ys) ≡ reverse ys ++ reverse xs

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

postulate
  reverse-involutive : ∀ {A : Set} {xs : List A}
    → reverse (reverse xs) ≡ xs

Exercise map-compose

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

postulate
  map-compose : ∀ {A B C : Set} {f : A → B} {g : B → C}
    → map (g ∘ f) ≡ map g ∘ map f

The last step of the proof requires extensionality.

Exercise map-++-commute

Prove the following relationship between map and append.

postulate
  map-++-commute : ∀ {A B : Set} {f : A → B} {xs ys : List A}
   →  map f (xs ++ ys) ≡ map f xs ++ map f ys

Exercise map-Tree

Define a type of trees with leaves of type A and internal nodes of type B.

data Tree (A B : Set) : Set where
  leaf : A → Tree A B
  node : Tree A B → B → Tree A B → Tree A B

Define a suitable map operator over trees.

postulate
  map-Tree : ∀ {A B C D : Set}
    → (A → C) → (B → D) → Tree A B → Tree C D

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

product [ 1 , 2 , 3 , 4 ] ≡ 24

Exercise foldr-++ (recommended)

Show that fold and append are related as follows.

postulate
  foldr-++ : ∀ {A B : Set} (_⊗_ : A → B → B) (e : B) (xs ys : List A) →
    foldr _⊗_ e (xs ++ ys) ≡ foldr _⊗_ (foldr _⊗_ e ys) xs

Exercise map-is-foldr

Show that map can be defined using fold.

postulate
  map-is-foldr : ∀ {A B : Set} {f : A → B} →
    map f ≡ foldr (λ x xs → f x ∷ xs) []

This requires extensionality.

Exercise fold-Tree

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

postulate
  fold-Tree : ∀ {A B C : Set}
    → (A → C) → (C → B → C → C) → Tree A B → C

Exercise map-is-fold-Tree

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

Exercise sum-downFrom (stretch)

Define a function that counts down as follows.

downFrom : ℕ → List ℕ
downFrom zero     =  []
downFrom (suc n)  =  n ∷ downFrom n

For example,

_ : downFrom 3 ≡ [ 2 , 1 , 0 ]
_ = refl

Prove that the sum of the numbers (n - 1) + ⋯ + 0 is equal to n * (n ∸ 1) / 2.

postulate
  sum-downFrom : ∀ (n : ℕ)
    → sum (downFrom n) * 2 ≡ n * (n ∸ 1)

Exercise foldl

Define a function foldl which is analogous to foldr, but where operations associate to the left rather than the right. For example,

foldr _⊗_ e [ x , y , z ]  =  x ⊗ (y ⊗ (z ⊗ e))
foldl _⊗_ e [ x , y , z ]  =  ((e ⊗ x) ⊗ y) ⊗ z

Exercise foldr-monoid-foldl

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

Exercise Any-++-⇔ (recommended)

Prove a result similar to All-++-↔, but with Any in place of All, and a suitable replacement for _×_. As a consequence, demonstrate an equivalence relating _∈_ and _++_.

Exercise All-++-≃ (stretch)

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

Exercise ¬Any≃All¬ (stretch)

First generalise composition to arbitrary levels, using [universe polymorphism][plfa.Equality#unipoly].

_∘′_ : ∀ {ℓ₁ ℓ₂ ℓ₃ : Level} {A : Set ℓ₁} {B : Set ℓ₂} {C : Set ℓ₃}
  → (B → C) → (A → B) → A → C
(g ∘′ f) x  =  g (f x)

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

postulate
  ¬Any≃All¬ : ∀ {A : Set} (P : A → Set) (xs : List A)
    → (¬_ ∘′ Any P) xs ≃ All (¬_ ∘′ P) xs

Do we also have the following?

postulate
  ¬All≃Any¬ : ∀ {A : Set} (P : A → Set) (xs : List A)
    → (¬_ ∘′ All P) xs ≃ Any (¬_ ∘′ P) xs

If so, prove; if not, explain why.

Exercise any? (stretch)

Just as All has analogues all and all? which determine whether a predicate holds for every element of a list, so does Any have analogues any and any? which determine whether a predicates holds for some element of a list. Give their definitions.

Exercise filter? (stretch)

Define the following variant of the traditional filter function on lists, which given a list and a decidable predicate returns all elements of the list satisfying the predicate.

postulate
  filter? : ∀ {A : Set} {P : A → Set}
    → (P? : Decidable P) → List A → ∃[ ys ]( All P ys )

Lambda

Write out the definition of a lambda term that multiplies two natural numbers.

Exercise primed (stretch)

We can make examples with lambda terms slightly easier to write by adding the following definitions.

ƛ′_⇒_ : Term → Term → Term
ƛ′ (` x) ⇒ N  =  ƛ x ⇒ N
ƛ′ _ ⇒ _      =  ⊥-elim impossible
  where postulate impossible : ⊥

case′_[zero⇒_|suc_⇒_] : Term → Term → Term → Term → Term
case′ L [zero⇒ M |suc (` x) ⇒ N ]  =  case L [zero⇒ M |suc x ⇒ N ]
case′ _ [zero⇒ _ |suc _ ⇒ _ ]      =  ⊥-elim impossible
  where postulate impossible : ⊥

μ′_⇒_ : Term → Term → Term
μ′ (` x) ⇒ N  =  μ x ⇒ N
μ′ _ ⇒ _      =  ⊥-elim impossible
  where postulate impossible : ⊥

The definition of plus can now be written as follows.

plus′ : Term
plus′ = μ′ + ⇒ ƛ′ m ⇒ ƛ′ n ⇒
          case′ m
            [zero⇒ n
            |suc m ⇒ `suc (+ · m · n) ]
  where
  +  =  ` "+"
  m  =  ` "m"
  n  =  ` "n"

Write out the definition of multiplication in the same style.

Exercise _[_:=_]′ (stretch)

The definition of substitution above has three clauses (ƛ, case, and μ) that invoke a with clause to deal with bound variables. Rewrite the definition to factor the common part of these three clauses into a single function, defined by mutual recursion with substitution.

Exercise —↠≃—↠′

Show that the two notions of reflexive and transitive closure above are isomorphic.

Exercise plus-example

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

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

Properties

Exercise Progress-≃

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

Exercise progress′

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

Exercise value?

Combine progress and —→¬V to write a program that decides whether a well-typed term is a value.

postulate
  value? : ∀ {A M} → ∅ ⊢ M ⦂ A → Dec (Value M)

Exercise subst′ (stretch)

Rewrite subst to work with the modified definition _[_:=_]′ from the exercise in the previous chapter. As before, this should factor dealing with bound variables into a single function, defined by mutual recursion with the proof that substitution preserves types.

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.

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