# Assignment3: PUC Assignment 3

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)

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

ƛ′_⇒_ : 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 first notion of reflexive and transitive closure above embeds into the second. Why are they not 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.

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.

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