```module Assignment4 where
```

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

## Good Scholarly Practice.

Furthermore, 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, or your group in the case of group practicals).

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

## More

```module More where
```
```  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.More
hiding (double-subst)
```

Formalise the remaining constructs defined in this chapter. Make your changes in this file. Evaluate each example, applied to data as needed, to confirm it returns the expected answer:

• sums (recommended)
• unit type (practice)
• an alternative formulation of unit type (practice)
• empty type (recommended)
• lists (practice)

``````-- begin
-- end``````

#### Exercise `double-subst` (stretch)

Show that a double substitution is equivalent to two single substitutions.
```  postulate
double-subst :
∀ {Γ A B C} {V : Γ ⊢ A} {W : Γ ⊢ B} {N : Γ , A , B ⊢ C} →
N [ V ][ W ] ≡ (N [ rename S_ W ]) [ V ]
```

Note the arguments need to be swapped and `W` needs to have its context adjusted via renaming in order for the right-hand side to be well typed.

## Inference

```module Inference where
```

## Imports

```  import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; sym; trans; cong; cong₂; _≢_)
open import Data.Empty using (⊥; ⊥-elim)
open import Data.Nat using (ℕ; zero; suc; _+_; _*_)
open import Data.String using (String; _≟_)
open import Data.Product using (_×_; ∃; ∃-syntax) renaming (_,_ to ⟨_,_⟩)
open import Relation.Nullary using (¬_; Dec; yes; no)
open import Relation.Nullary.Decidable using (False; toWitnessFalse)
```

Once we have a type derivation, it will be easy to construct from it the intrinsically-typed representation. In order that we can compare with our previous development, we import module `plfa.part2.More`:

```  import plfa.part2.More as DB
```

The phrase `as DB` allows us to refer to definitions from that module as, for instance, `DB._⊢_`, which is invoked as `Γ DB.⊢ A`, where `Γ` has type `DB.Context` and `A` has type `DB.Type`.

```  open import plfa.part2.Inference
hiding ()
```

#### Exercise `bidirectional-mul` (recommended)

Rewrite your definition of multiplication from Chapter Lambda, decorated to support inference.

```  -- Your code goes here
```

#### Exercise `bidirectional-products` (recommended)

Extend the bidirectional type rules to include products from Chapter More.

```  -- Your code goes here
```

#### Exercise `bidirectional-rest` (stretch)

Extend the bidirectional type rules to include the rest of the constructs from Chapter More.

```  -- Your code goes here
```

Apply inference to your decorated definition of multiplication from exercise `bidirectional-mul`, and show that erasure of the inferred typing yields your definition of multiplication from Chapter DeBruijn.

```  -- Your code goes here
```

Using your rules from exercise `bidirectional-products`, extend bidirectional inference to include products.

```  -- Your code goes here
```

#### Exercise `inference-rest` (stretch)

Extend the bidirectional type rules to include the rest of the constructs from Chapter More.

```  -- Your code goes here
```

## Untyped

```module Untyped where
```

## Imports

```  import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; sym; trans; cong)
open import Data.Empty using (⊥; ⊥-elim)
open import Data.Nat using (ℕ; zero; suc; _+_; _∸_)
open import Data.Product using (_×_) renaming (_,_ to ⟨_,_⟩)
open import Data.Unit using (⊤; tt)
open import Function using (_∘_)
open import Function.Equivalence using (_⇔_; equivalence)
open import Relation.Nullary using (¬_; Dec; yes; no)
open import Relation.Nullary.Decidable using (map)
open import Relation.Nullary.Negation using (contraposition)
open import Relation.Nullary.Product using (_×-dec_)
```
```  open import plfa.part2.Untyped
hiding ()
```

#### Exercise (`Type≃⊤`) (practice)

Show that `Type` is isomorphic to `⊤`, the unit type.

```  -- Your code goes here
```

#### Exercise (`Context≃ℕ`) (practice)

Show that `Context` is isomorphic to `ℕ`.

```  -- Your code goes here
```

#### Exercise (`variant-1`) (practice)

How would the rules change if we want call-by-value where terms normalise completely? Assume that `β` should not permit reduction unless both terms are in normal form.

```  -- Your code goes here
```

#### Exercise (`variant-2`) (practice)

How would the rules change if we want call-by-value where terms do not reduce underneath lambda? Assume that `β` permits reduction when both terms are values (that is, lambda abstractions). What would `2+2ᶜ` reduce to in this case?

```  -- Your code goes here
```

#### Exercise `plus-eval` (practice)

Use the evaluator to confirm that `plus · two · two` and `four` normalise to the same term.

```  -- Your code goes here
```

Use the encodings above to translate your definition of multiplication from previous chapters with the Scott representation and the encoding of the fixpoint operator. Confirm that two times two is four.

```  -- Your code goes here
```

#### Exercise `encode-more` (stretch)

Along the lines above, encode all of the constructs of Chapter More, save for primitive numbers, in the untyped lambda calculus.

```  -- Your code goes here
```