--------------------------------------------------------------------
  A syntactic treatment of majorizability of T-definable functionals
 --------------------------------------------------------------------

                     Chuangjie Xu, May 2018


This is a self-contained Agda implementation of Howard's syntactic
approach to majorizability that is presented in §6.1 of [1].

There are some minor modifications:

1. The majorization relation is defined on Agda terms of finite types
   instead of T terms.

2. The majorization construction _ᴹ is defined on functions ℕ → ρ for
   arbitrary finite type ρ (following a standard construction of
   Kleisli extension), while §6.1 of [1] always assumes that ρ is
   function type with codomain ℕ.

3. Howard's statement of majorizability of closed T terms is
   generalized to terms with free variable, which is our main lemma.


Reference:

[1] Ulrich Kohlenbach. Applied Proof Theory: Proof Interpretations and
    their Use in Mathematics. Springer Monographs in Mathematics, 2008.

\begin{code}

module TMaj where

\end{code}

------------------
- A mini library -
------------------

\begin{code}

infix  _≡_

data _≡_ {A : Set} (a : A) : A → Set where
 refl : a ≡ a

infixr  _,_

record Σ {A : Set} (B : A → Set) : Set where
 constructor _,_
 field
  pr₁ : A
  pr₂ : B pr₁

open Σ public

data ℕ : Set where
 zero : ℕ
 succ : ℕ → ℕ

{-# BUILTIN NATURAL ℕ #-}

rec : {A : Set} → ℕ → A → (A → ℕ → A) → A
rec         a f = a
rec (succ n) a f = f (rec n a f) n

infix  _≤_ _≥_

data _≤_ : ℕ → ℕ → Set where
 ≤refl : {n : ℕ} → n ≤ n
 ≤succ : {n m : ℕ} → n ≤ m → n ≤ succ m

_≥_ : ℕ → ℕ → Set
n ≥ m = m ≤ n

≤trans : {n m l : ℕ} → n ≤ m → m ≤ l → n ≤ l
≤trans  ≤refl     s        = s
≤trans (≤succ r)  ≤refl    = ≤succ r
≤trans (≤succ r) (≤succ s) = ≤succ (≤trans (≤succ r) s)

zero≤ : {n : ℕ} →  ≤ n
zero≤ {}      = ≤refl
zero≤ {succ n} = ≤succ zero≤

succ≤ : {n m : ℕ} → n ≤ m → succ n ≤ succ m
succ≤  ≤refl    = ≤refl
succ≤ (≤succ r) = ≤succ (succ≤ r)

max : ℕ → ℕ → ℕ
max          m       = m
max (succ n)         = succ n
max (succ n) (succ m) = succ (max n m)

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)

\end{code}

--------------------
- Gödel's System T -
--------------------

\begin{code}

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

--
-- Finite type hierarchy
--
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 Tm (Γ : Cxt) : Ty → Set where
 Var  : {σ : Ty} → ∥ σ ∈ Γ ∥ → Tm Γ σ
 Lam  : {σ τ : Ty} → Tm (Γ ₊ σ) τ → Tm Γ (σ ⇾ τ)
 _·_  : {σ τ : Ty} → Tm Γ (σ ⇾ τ) → Tm Γ σ → Tm Γ τ
 Zero : Tm Γ ι
 Succ : Tm Γ (ι ⇾ ι)
 Rec  : {σ : Ty} → Tm Γ (ι ⇾ σ ⇾ (σ ⇾ ι ⇾ σ) ⇾ σ)

\end{code}

A natural interpretation of T into Agda

\begin{code}

--
-- Interpretation of types
--
⟦_⟧ʸ : Ty → Set
⟦ ι ⟧ʸ     = ℕ
⟦ σ ⇾ τ ⟧ʸ = ⟦ σ ⟧ʸ → ⟦ τ ⟧ʸ

--
-- Interpretation of contexts
--
⟦_⟧ˣ : Cxt → Set
⟦ Γ ⟧ˣ = {ρ : Ty} → ∥ ρ ∈ Γ ∥ → ⟦ ρ ⟧ʸ

--
-- The interpretation of the empty context
--
⟪⟫ : ⟦ ε ⟧ˣ
⟪⟫ ()

--
-- The interpretation of context extension
--
_ₓ_ : {Γ : Cxt} {ρ : Ty} → ⟦ Γ ⟧ˣ → ⟦ ρ ⟧ʸ → ⟦ Γ ₊ ρ ⟧ˣ
(γ ₓ a)  zero    = a
(γ ₓ a) (succ i) = γ i

--
-- Interpretation of terms
--
⟦_⟧ᵐ : {Γ : Cxt} {ρ : Ty} → Tm Γ ρ → ⟦ Γ ⟧ˣ → ⟦ ρ ⟧ʸ
⟦ Var i ⟧ᵐ   γ = γ i
⟦ Lam t ⟧ᵐ   γ = λ a → ⟦ t ⟧ᵐ (γ ₓ a)
⟦ f · a ⟧ᵐ   γ = ⟦ f ⟧ᵐ γ (⟦ a ⟧ᵐ γ)
⟦ Zero ⟧ᵐ    _ = 
⟦ Succ ⟧ᵐ    _ = succ
⟦ Rec {ρ} ⟧ᵐ _ = rec

--
-- The interpretation of closed terms
--
⟦_⟧ : {ρ : Ty} → Tm ε ρ → ⟦ ρ ⟧ʸ
⟦ t ⟧ = ⟦ t ⟧ᵐ ⟪⟫

--
-- T-definablity on the finite type hierarchy
--
T-definable : {ρ : Ty} → ⟦ ρ ⟧ʸ → Set
T-definable {ρ} a = Σ \(t : Tm ε ρ) → a ≡ ⟦ t ⟧

\end{code}

------------------
- Majorizability - on the finite type hierarchy
------------------

\begin{code}

maj : (σ : Ty) → ⟦ σ ⟧ʸ → ⟦ σ ⟧ʸ → Set
maj  ι      n m = n ≥ m
maj (σ ⇾ τ) f g = {x y : ⟦ σ ⟧ʸ} → maj σ x y → maj τ (f x) (g y)

_𝑚𝑎𝑗_ : {σ : Ty} → ⟦ σ ⟧ʸ → ⟦ σ ⟧ʸ → Set
_𝑚𝑎𝑗_ = maj _

majorizable : {σ : Ty} → ⟦ σ ⟧ʸ → Set
majorizable a = Σ \(aᴹ : ⟦ _ ⟧ʸ) → aᴹ 𝑚𝑎𝑗 a

_𝑚𝑎𝑗ˣ_ : {Γ : Cxt} → ⟦ Γ ⟧ˣ → ⟦ Γ ⟧ˣ → Set
γ 𝑚𝑎𝑗ˣ δ = {σ : Ty} (i : ∥ σ ∈ _ ∥) → (γ i) 𝑚𝑎𝑗 (δ i)

Lm[maj-ε] : ⟪⟫ 𝑚𝑎𝑗ˣ ⟪⟫
Lm[maj-ε] ()

Lm[maj-ext] : {Γ : Cxt} {ρ : Ty} {γ δ : ⟦ Γ ⟧ˣ} {a b : ⟦ ρ ⟧ʸ}
            → γ 𝑚𝑎𝑗ˣ δ → a 𝑚𝑎𝑗 b → (γ ₓ a) 𝑚𝑎𝑗ˣ (δ ₓ b)
Lm[maj-ext] ξ ζ  zero    = ζ
Lm[maj-ext] ξ ζ (succ i) = ξ i

--
-- Definition 6.1 of [§6.1, 1]
--
--   a majorization construction _ᴹ on functions ℕ → ρ
--
φ : (ℕ → ℕ) → ℕ → ℕ
φ x         = x 
φ x (succ z) = max (φ x z) (x (succ z))

φ-spec : {f : ℕ → ℕ} {n m : ℕ} → n ≥ m → φ f n ≥ f m
φ-spec {f} {}       ≤refl    = ≤refl
φ-spec {f} {succ n}  ≤refl    = max-spec₁ (φ f n) (f (succ n))
φ-spec {f} {succ n} (≤succ r) = ≤trans (φ-spec r) (max-spec₀ (φ f n) (f (succ n)))

infix  _ᴹ
--
-- Kleisli extension for the base type
--
_ᴹ : {ρ : Ty} → (ℕ → ⟦ ρ ⟧ʸ) → ℕ → ⟦ ρ ⟧ʸ
_ᴹ {ι}     = φ
_ᴹ {σ ⇾ τ} = λ f n a → _ᴹ (λ x → f x a) n

--
-- With _ᴹ defined as a Kleisli extension, Lemma[6·4] is easier to prove.
--
Lemma[6·4] : {ρ : Ty} {f g : ℕ → ⟦ ρ ⟧ʸ} → (∀ n → f n 𝑚𝑎𝑗 g n) → f ᴹ 𝑚𝑎𝑗 g
Lemma[6·4] {ι}     ξ r = ≤trans (ξ _) (φ-spec r)
Lemma[6·4] {σ ⇾ τ} ξ r = λ ζ → Lemma[6·4] (λ n → ξ n ζ) r

\end{code}

--------------
- Main lemma : Every T-term is majorizable.
--------------

\begin{code}

MainLemma : {Γ : Cxt} {σ : Ty} (t : Tm Γ σ)
          → Σ \(tᴹ : ⟦ Γ ⟧ˣ → ⟦ σ ⟧ʸ) → {γ δ : ⟦ Γ ⟧ˣ} → γ 𝑚𝑎𝑗ˣ δ → tᴹ γ 𝑚𝑎𝑗 ⟦ t ⟧ᵐ δ
MainLemma (Var i) = (λ γ → γ i) , (λ ξ → ξ i)
MainLemma {Γ} (Lam {σ} {τ} t) = λtᴹ , prf
 where
  tᴹ  : ⟦ Γ ₊ σ ⟧ˣ → ⟦ τ ⟧ʸ
  tᴹ  = pr₁ (MainLemma t)
  λtᴹ : ⟦ Γ ⟧ˣ → ⟦ σ ⇾ τ ⟧ʸ
  λtᴹ γ a = tᴹ (γ ₓ a)
  mt  : {γ δ : ⟦ Γ ₊ σ ⟧ˣ} → γ 𝑚𝑎𝑗ˣ δ → tᴹ γ 𝑚𝑎𝑗 ⟦ t ⟧ᵐ δ
  mt  = pr₂ (MainLemma t)
  prf : {γ δ : ⟦ Γ ⟧ˣ} → γ 𝑚𝑎𝑗ˣ δ → λtᴹ γ 𝑚𝑎𝑗 ⟦ Lam t ⟧ᵐ δ
  prf ξ ζ = mt (Lm[maj-ext] ξ ζ)
MainLemma {Γ} {τ} (f · a) = fᴹaᴹ , prf
 where
  fᴹ = pr₁ (MainLemma f)
  aᴹ = pr₁ (MainLemma a)
  fᴹaᴹ : ⟦ Γ ⟧ˣ → ⟦ τ ⟧ʸ
  fᴹaᴹ γ = fᴹ γ (aᴹ γ)
  mf : {γ δ : ⟦ Γ ⟧ˣ} → γ 𝑚𝑎𝑗ˣ δ → fᴹ γ 𝑚𝑎𝑗 ⟦ f ⟧ᵐ δ
  mf = pr₂ (MainLemma f)
  ma : {γ δ : ⟦ Γ ⟧ˣ} → γ 𝑚𝑎𝑗ˣ δ → aᴹ γ 𝑚𝑎𝑗 ⟦ a ⟧ᵐ δ
  ma = pr₂ (MainLemma a)
  prf : {γ δ : ⟦ Γ ⟧ˣ} → γ 𝑚𝑎𝑗ˣ δ → fᴹaᴹ γ 𝑚𝑎𝑗 ⟦ f · a ⟧ᵐ δ
  prf ξ = mf ξ (ma ξ)
MainLemma Zero = (λ _ → zero)  , (λ _ → zero≤)
MainLemma Succ = (λ _ → succ)  , (λ _ → succ≤)
MainLemma Rec  = (λ _ → rec ᴹ) , (λ _ → prf)
 where
  claim : (n : ℕ) → rec n 𝑚𝑎𝑗 rec n 
                 -- x 𝑚𝑎𝑗 y → f 𝑚𝑎𝑗 g → rec n x f 𝑚𝑎𝑗 rec n y g
  claim         ξ ζ = ξ
  claim (succ n) ξ ζ = ζ (claim n ξ ζ) ≤refl
  prf : rec ᴹ 𝑚𝑎𝑗 rec
  prf = Lemma[6·4] claim

\end{code}

----------------
- Main theorem : Every T-definable element is majorizable.
----------------

\begin{code}

Theorem : {ρ : Ty} {a : ⟦ ρ ⟧ʸ}
        → T-definable a → majorizable a
Theorem {ρ} {a} (t , refl) = tᴹ , prf
 where
  tᴹ  : ⟦ ρ ⟧ʸ
  tᴹ  = pr₁ (MainLemma t) ⟪⟫
  prf : tᴹ 𝑚𝑎𝑗 a
  prf = pr₂ (MainLemma t) Lm[maj-ε]

\end{code}