======================
 =                    =
 =  Gödel's System T  =
 =                    =
 ======================

    Chuangjie Xu, July 2019

\begin{code}

{-# OPTIONS --without-K --safe #-}

module T where

open import Preliminaries

\end{code}

■ Types, contexts and terms of T

Here we work with the lambda-calculus version of system T, and with de
Bruijn indices instead of variables.

\begin{code}

infixr  _⇾_
infixl  _₊_
infixl  _·_

--
-- finite types
--
data Ty : Set where
 ι   : Ty
 _⇾_ : Ty → Ty → Ty

--
-- contexts as finite lists of types
--
data Cxt : Set where
 ε   : Cxt
 _₊_ : Cxt → Ty → Cxt

--
-- indices of types/variables in context
--
data ∥_∈_∥ (σ : Ty) : Cxt → Set where
 zero : {Γ : Cxt} → ∥ σ ∈ (Γ ₊ σ) ∥
 succ : {τ : Ty} {Γ : Cxt} → ∥ σ ∈ Γ ∥ → ∥ σ ∈ Γ ₊ τ ∥

--
-- terms
--
data T (Γ : Cxt) : Ty → Set where
 Var  : {σ : Ty} → ∥ σ ∈ Γ ∥ → T Γ σ
 Lam  : {σ τ : Ty} → T (Γ ₊ σ) τ → T Γ (σ ⇾ τ)
 _·_  : {σ τ : Ty} → T Γ (σ ⇾ τ) → T Γ σ → T Γ τ
 Zero : T Γ ι
 Succ : T Γ (ι ⇾ ι)
 Rec  : {σ : Ty} → T Γ (σ ⇾ (ι ⇾ σ ⇾ σ) ⇾ ι ⇾ σ)

\end{code}

■ The standard interpretation of T into Agda

\begin{code}

⟦_⟧ʸ : Ty → Set
⟦ ι ⟧ʸ     = ℕ
⟦ σ ⇾ τ ⟧ʸ = ⟦ σ ⟧ʸ → ⟦ τ ⟧ʸ

⟦_⟧ˣ : Cxt → Set
⟦ ε ⟧ˣ     = 𝟙
⟦ Γ ₊ ρ ⟧ˣ = ⟦ Γ ⟧ˣ × ⟦ ρ ⟧ʸ

_₍_₎ : {Γ : Cxt} {ρ : Ty} → ⟦ Γ ⟧ˣ → ∥ ρ ∈ Γ ∥ → ⟦ ρ ⟧ʸ
(_ , a) ₍ zero ₎   = a
(γ , _) ₍ succ i ₎ = γ ₍ i ₎

⟦_⟧ᵐ : {Γ : Cxt} {σ : Ty} → T Γ σ → ⟦ Γ ⟧ˣ → ⟦ σ ⟧ʸ
⟦ Var i ⟧ᵐ γ = γ ₍ i ₎
⟦ Lam t ⟧ᵐ γ = λ a → ⟦ t ⟧ᵐ (γ , a)
⟦ f · a ⟧ᵐ γ = ⟦ f ⟧ᵐ γ (⟦ a ⟧ᵐ γ)
⟦ Zero ⟧ᵐ  _ = 
⟦ Succ ⟧ᵐ  _ = succ
⟦ Rec ⟧ᵐ   _ = rec

⟦_⟧ : {ρ : Ty} → T ε ρ → ⟦ ρ ⟧ʸ
⟦ t ⟧ = ⟦ t ⟧ᵐ ⋆

--
-- An (Agda) element a is "T-definable" if one can find a closed T
-- term whose standard interpretation is a.
--
T-definable : {ρ : Ty} → ⟦ ρ ⟧ʸ → Set
T-definable {ρ} a = Σ \(t : T ε ρ) → ⟦ t ⟧ ≡ a

\end{code}

■ Some auxiliaries

\begin{code}

ν₀ : {Γ : Cxt} {ρ : Ty} → T (Γ ₊ ρ) ρ
ν₀ = Var zero

ν₁ : {Γ : Cxt} {ρ σ : Ty} → T (Γ ₊ ρ ₊ σ) ρ
ν₁ = Var (succ zero)

ν₂ : {Γ : Cxt} {ρ σ₀ σ₁ : Ty} → T (Γ ₊ ρ ₊ σ₀ ₊ σ₁) ρ
ν₂ = Var (succ (succ zero))

ν₃ : {Γ : Cxt} {ρ σ₀ σ₁ σ₂ : Ty} → T (Γ ₊ ρ ₊ σ₀ ₊ σ₁ ₊ σ₂) ρ
ν₃ = Var (succ (succ (succ zero)))

Max : {Γ : Cxt} → T Γ (ι ⇾ ι ⇾ ι)
Max = Rec · Lam ν₀ · Lam (Lam (Rec · (Succ · ν₁) · Lam (Lam (Succ · (ν₂ · ν₁)))))

max : ℕ → ℕ → ℕ
max = ⟦ Max ⟧

Max-spec₀ : (n m : ℕ) → n ≤ max n m
Max-spec₀          m       = ≤zero
Max-spec₀ (succ n)         = ≤refl
Max-spec₀ (succ n) (succ m) = ≤succ (Max-spec₀ n m)

Max-spec₁ : (n m : ℕ) → m ≤ max n m
Max-spec₁          m       = ≤refl
Max-spec₁ (succ n)         = ≤zero
Max-spec₁ (succ n) (succ m) = ≤succ (Max-spec₁ n m)

φ : ℕᴺ → ℕ → ℕ
φ α         = α 
φ α (succ n) = max (φ α n) (α (succ n))

φ-spec : {i j : ℕ} → i ≤ j → {α : ℕᴺ} → α i ≤ φ α j
φ-spec {i} {} ≤zero = ≤refl
φ-spec {i} {succ j} r with ≤-cases r
φ-spec {i} {succ j} r | inl refl = Max-spec₁ (φ _ j) _
φ-spec {i} {succ j} r | inr i≤j  = ≤trans (φ-spec i≤j) (Max-spec₀ _ _)

\end{code}