YOUR NAME AND EMAIL GOES HERE
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!
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)
Write out the definition of a lambda term that multiplies two natural numbers.
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.
The definition of substitution above has three clauses (
μ) 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
Show that the first notion of reflexive and transitive closure above embeds into the second. Why are they not isomorphic?
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.
Progress M is isomorphic to
Value M ⊎ ∃[ N ](M —→ N).
Write out the proof of
progress′ in full, and compare it to the
—→¬V to write a program that decides
whether a well-typed term is a value.
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
Using the evaluator, confirm that two times two is four.
Without peeking at their statements above, write down the progress and preservation theorems for the simply typed lambda-calculus.
We say that
M reduces to
M —→ N,
and conversely that
M expands to
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.
Give an example of an ill-typed term that does get stuck.
Provide proofs of the three postulates,