Assignment4: TSPL Assignment 4

module Assignment4 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 labelled “(practice)” are included for those who want extra practice.

Submit your homework using the “submit” command. Please ensure your files execute correctly under Agda!

Good Scholarly Practice.

Please remember the University requirement as regards all assessed work. Details about this can be found at:

https://web.inf.ed.ac.uk/infweb/admin/policies/academic-misconduct

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 ()

Exercise mul (recommended)

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

Exercise mul-example (recommended)

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)

Exercise More (recommended and practice)

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)

Please delimit any code you add as follows:

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

Exercise inference-multiplication (recommended)

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

Exercise inference-products (recommended)

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

Exercise multiplication-untyped (recommended)

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