Mini project 3: mechanized metatheory

In this project you will formalize Assignment 3 in the Agda proof assistant. Recall that we proved canonicity for System T: for all closed terms of type nat e, there exists a number n such that e evaluates to the numeral representing n.

Installation

To install Agda, please follow the official guidelines here:

https://agda.readthedocs.io/en/latest/getting-started/installation.html

I recommend that you also setup VSCode with agda-mode:

https://marketplace.visualstudio.com/items?itemName=banacorn.agda-mode

Libraries

This project depends on the agda-soas library, which formalizes all of the syntactic metatheorems we need for the proof. You can find it here:

https://github.com/DimaSamoz/agda-soas

However, please make sure you check out commit 5bbb2a3673bd2bd462fee22345253ba151954c77 because that is the version of the library that is known to work for the project.

We will also need the Agda standard library, which is available here:

https://github.com/agda/agda-stdlib/blob/master/notes/installation-guide.md

A guide on library installation can be found here:

https://agda.readthedocs.io/en/v2.6.2.2.20221106/tools/package-system.html

Working with agda

Idiomatic Agda employs unicode characters that are nice to read. Please see the following guide for inputting special characters: https://agda.readthedocs.io/en/v2.6.2.2.20221106/tools/emacs-mode.html (note that the guide is for emacs but will work for VSCode with agda-mode installed).

A complete list of the characters you can input can be found here: https://github.com/agda/agda/blob/master/src/data/emacs-mode/agda-input.el

Navigating the project

The project contains the following files

• T -- defines the language T
  • Signature.agda -- types of T
  • Syntax.agda -- terms of T
• Assumptions.agda -- background mathematical assumptions
• OperationalSemantics.agda -- operational semantics of T
• LogicalRelation.agda -- defines candidates and the fundamental theorem
• Canonicity.agda -- canonicity

Syntax of the language

The directory T contains the syntax of the language T. The files in T are generated by the agda-soas library.

The language T is a small variation on the language we considered in Assignment 3: T features both (unary) products and (unary)sums, both under a call-by-name semantics. Moreover, because the language is equipped with products, we also replace the recursor with the iterator.

The file Signature.agda defines the types of T in a datatype ΛT:

data ΛT : Set where
  N   : ΛT
  _↣_ : ΛT → ΛT → ΛT
  𝟙   : ΛT
  _⊗_ : ΛT → ΛT → ΛT
  𝟘   : ΛT
  _⊕_ : ΛT → ΛT → ΛT

The file Syntax.agda defines the terms of T. First, variables are defined using de Bruijn indices:

data ℐ : ΛT → Ctx → Set where
  new : {α   : ΛT}{Γ : Ctx}          → ℐ α (α ∙ Γ)
  old : {α β : ΛT}{Γ : Ctx} → ℐ β Γ → ℐ β (α ∙ Γ)

Here contexts Γ are defined as lists of types:

data Ctx : Set where
  ∅   : Ctx
  _∙_ : (α : ΛT) → (Γ : Ctx) → Ctx

General terms are defined using this definition for variables:

data Λ : Family where
    var  : ℐ ⇾̣ Λ

    _$_   : Λ (α ↣ β) Γ → Λ α Γ → Λ β Γ
    ƛ_    : Λ β (α ∙ Γ) → Λ (α ↣ β) Γ
    triv  : Λ 𝟙 Γ
    ⟨_,_⟩ : Λ α Γ → Λ β Γ → Λ (α ⊗ β) Γ
    fst   : Λ (α ⊗ β) Γ → Λ α Γ
    snd   : Λ (α ⊗ β) Γ → Λ β Γ
    abort : Λ 𝟘 Γ → Λ α Γ
    inl   : Λ α Γ → Λ (α ⊕ β) Γ
    inr   : Λ β Γ → Λ (α ⊕ β) Γ
    case  : Λ (α ⊕ β) Γ → Λ γ (α ∙ Γ) → Λ γ (β ∙ Γ) → Λ γ Γ
    ze    : Λ N Γ
    su    : Λ N Γ → Λ N Γ
    iter  : Λ N Γ → Λ α Γ → Λ α (α ∙ Γ) → Λ α Γ

We write e : Λᴳ τ Γ for a term e of type τ in the context Γ. The datatype Λ defines an intrinsic encoding of syntax. Intrinsic encodings are sometimes convenient in a formal setting because it enforces the invariant that one can only write down well-typed terms. For example, the term ⟨_,_⟩ : Λ α Γ → Λ β Γ → Λ (α ⊗ β) Γ can be rendered as the following usual typing judgment:

Γ ⊢ e1 : τ1
Γ ⊢ e2 : τ2

------------

Γ ⊢ ⟨ e1 , e1 ⟩ : τ1

(Do not have to worry about what Family is since that mostly pertains to metavariables and metasubstitutions.)

Logical relations

Candidates may be encoded using a record type:

record cand (τ : ΛT) : Set1 where 
    field 
      -- underlying set of the candidate
      set : Set
      -- logical relation
      _⊩_ : P τ → set → Set 
      -- closure under reverse execution
      ← : {e e' : P τ} {a : set} → e ↦* e' → e' ⊩ a → e ⊩ a

Recall that part of Assignment three was proving that the (candidate) candidates defined in the assignment are well-defined. We formalize that here. For example, the natural numbers is equipped with a candidate is proved by defining the following record:

𝔑  : cand N 
𝔑  . set = ℕ 
𝔑  . _⊩_ = λ e n → e ⇓ numeral n 
𝔑  . ←  = head/exp

Where head expansion is the usual head expansion lemma for multi-step transition.

Doing this for every type of T, we obtain the following assignment:

  -- assignment of candidate to types of T
  𝓕 : (τ : ΛT) → cand τ
  𝓕 N = 𝔑
  𝓕 (σ ↣ τ) = ?
  𝓕 𝟙 = ?
  𝓕 (σ ⊗ τ) = ?
  𝓕 𝟘 = 𝔈
  𝓕 (σ ⊕ τ) = ?

The function 𝓕 induces the following, which gives us a better notation for referencing the underlying set of a candidate and the realizability relation:

⟦_⟧ : ΛT → Set 
⟦ τ ⟧ = 𝓕 τ . set 

_∣_⊩_ : (τ : ΛT) → P τ → ⟦ τ ⟧ → Set  
τ ∣ e ⊩ a =  (𝓕 τ) ._⊩_ e a

For instance τ ∣ e ⊩ a can be read as e realizes a in type τ.

Realizability is extended to open terms as expected:

 data _∣_▷_ : (Γ : Ctx) → Sub Λᴳ Γ ∅ → ⟦ Γ ⟧₁ → Set where 
    * : ∅ ∣ • ▷ tt
    _::_ : ∀ {Γ} {𝕤} {γ} {τ} {e} {a} → τ ∣ e ⊩ a → Γ ∣ 𝕤 ▷ γ → (τ ∙ Γ) ∣ (e ◂ 𝕤) ▷ (a , γ)

Here Sub Λᴳ Γ ∅ is the type representing closing substitutions for the context Γ, • is the empty substitution, and e ◂ 𝕤 is the substitution 𝕤 extended by a closed term e.

The fundamental theorem states that all terms are the realizers for some semantic function f:

ftlr : (Γ : Ctx) → (τ : ΛT) → 
         (e : Λᴳ τ Γ) → 
         Σ (⟦ Γ ⟧₁ → ⟦ τ ⟧) λ f → 
          (𝕤 : Sub Λᴳ Γ ∅) → (γ : ⟦ Γ ⟧₁ ) → Γ ∣ 𝕤 ▷ γ → 
            τ ∣ (𝕤𝕦𝕓 e (index 𝕤)) ⊩ f γ

Here 𝕤𝕦𝕓 e (index 𝕤) performs the substitution index 𝕤 on e. The function index converts the inductive substitution Sub Λᴳ Γ ∅ from above to the functional definition below:

_~[_]↝_ : Ctx → Ctx → Set
Γ ~[ Λᴳ ]↝ Δ = {τ : ΛT} → ℐ τ Γ → Λᴳ τ Δ

Again Γ ~[ Λᴳ ]↝ Δ is a substitution from Γ to Δ.

Tasks

You need to complete all definitions in LogicalRelation.agda and Canonicity.agda. When you first load a file, there will be holes indicating where an expected definition is missing. Below is a list of the definitions you should complete, annotated by the expected difficulty:

In LogicalRelation.agda:

[*] _⇒_ : cand σ → cand τ → cand (σ ↣ τ)

[*] 𝔘 : cand 𝟙

[*] 𝔈 : cand 𝟘

[*] _⊞_ : cand σ → cand τ → cand (σ ⊕ τ)

[*] _⊠_ : cand σ → cand τ → cand (σ ⊗ τ)

[-] ftlr : (Γ : Ctx) → (τ : ΛT) → (e : Λᴳ τ Γ) → Σ (⟦ Γ ⟧₁ → ⟦ τ ⟧) λ f → (𝕤 : Sub Λᴳ Γ ∅) → (γ : ⟦ Γ ⟧₁ ) → Γ ∣ 𝕤 ▷ γ → τ ∣ (𝕤𝕦𝕓 e (index 𝕤)) ⊩ f γ

In Canonicity.agda:

[*] canonicity : (e : P N) → Σ ℕ λ n → e ⇓ numeral n

* means that it should take around 10 minutes to complete the task

** means that it should take 30 to 90 minutes to complete the task

*** means that it may take several hours to complete the task

- For the fundamental theorem, the break down is as follows:

[**] ftlr Γ (σ ↣ τ) (ƛ e) = ?

[*] ftlr Γ τ (_$_ {α = σ} {β = ρ} e e1) = ?

[***] ftlr Γ τ (iter e e0 e1) = ?

[*] ftlr Γ .𝟙 triv = ?

[*] ftlr Γ τ (fst e) = ?

[*] ftlr Γ τ (snd e) = ?

[*] ftlr Γ τ (abort e) = ?

[*] ftlr Γ .(_ ⊕ _) (inl e) = ?

[*] ftlr Γ .(_ ⊕ _) (inr e) = ?

[**] ftlr Γ τ (case {α = σ} {β = ρ} e e₁ e₂) = ?

[*] ftlr Γ .N ze = ?

[*] ftlr Γ .N (su e) = ?

[*] ftlr Γ (σ ⊗ τ) ⟨ e1 , e2 ⟩ = ?