---------------------------------------------
                 A syntactic approach to continuity
             of Gödel's system T definable functionals
           ---------------------------------------------

                          Chuangjie Xu

                February 2018, updated in June 2018


This is another short and self-contained Agda proof that

  any Gödel's system T definable function (ℕ → ℕ) → ℕ is continuous.

We firstly perform a translation within T, which is inspired by Oliva
and Steila's proof of the bar recursion closure theorem [2].  By
structural induction on terms, we show that (the standard
interpretation of) the translation of any T term satisfies a certain
continuity predicate.  Then we use a parametrised logical relation due
to Escardó [1] to relate (the standard interpretations of) T terms and
their translations.  These together bring us the desired result.


Our Agda development is organised as follows:

 §0. Mini library

 §1. Gödel's system T and b-translation

 §2. Continuity of T-definable functionals

 §3. Experiments of computation


Reference.

[1] M.H. Escardó.  Continuity of Gödel's system T functionals via
    effectful forcing.  MFPS'2013.  Electronic Notes in Theoretical
    Computer Science 01/2013; 298:119–141, 2013.

[2] P. Oliva and S. Steila.  A direct proof of Schwichtenberg's bar
    recursion closure theorem.  The Journal of Symbolic Logic 83(1):
    70-83, 2018.


\begin{code}

module TCont where

\end{code}

======================
=                    =
=  §0  Mini library  =
=                    =
======================

\begin{code}

--
-- identity types
--
data _≡_ {} {A : Set } (a : A) : A  Set  where
 refl : a  a

ap : {A B : Set} (f : A  B) {x y : A}  x  y  f x  f y
ap f refl = refl

sym : {A : Set} {x y : A}  x  y  y  x
sym refl = refl

trans : {A : Set} {x y z : A}
       x  y  y  z  x  z
trans refl p = p

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

open Σ public

infixr 1 _×_ _,_

_×_ : Set  Set  Set
A × B = Σ \(_ : A)  B

--
-- the unit type
--
data 𝟙 : Set where
  : 𝟙

--
-- natural numbers
--
data  : Set where
 zero : 
 succ :   

{-# BUILTIN NATURAL  #-}

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

infix 2 _≤_

data _≤_ :     Set where
 ≤zero : {n : }  0  n
 ≤succ : {n m : }  n  m  succ n  succ m

≤refl : {n : }  n  n
≤refl {0}      = ≤zero
≤refl {succ n} = ≤succ ≤refl

max :     
max  0        m       = m
max (succ n)  0       = succ n
max (succ n) (succ m) = succ (max n m)

max-spec₀ : (n m : )  n  max n m
max-spec₀  0        m       = ≤zero
max-spec₀ (succ n)  0       = ≤refl
max-spec₀ (succ n) (succ m) = ≤succ (max-spec₀ n m)

max-spec₁ : (n m : )  m  max n m
max-spec₁  0        m       = ≤refl
max-spec₁ (succ n)  0       = ≤zero
max-spec₁ (succ n) (succ m) = ≤succ (max-spec₁ n m)

--
-- infinite sequences as functions from ℕ
--
_ᴺ : Set  Set
A  =   A

ℕᴺ : Set
ℕᴺ =  

head : {A : Set}  A   A
head α = α 0

tail : {A : Set}  A   A 
tail α i = α (succ i)

\end{code}


============================================
=                                          =
=  §1  Gödel's system T and b-translation  =
=                                          =
============================================


■ 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 30 _⇾_
infixl 20 _₊_
infixl 20 _·_

--
-- 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 Γ (σ  (ι  σ  σ)  ι  σ)

ν₀ : {Γ : 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)))

\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 ⟧ᵐ  _ = 0
 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}

■ b-translation

The first step of a usual syntactic treatment (e.g. of totality or
majorisability) is to inductively define a predicate on elements of
finite types whose base case is on natural numbers.  However, what we
want to prove is continuity of functions (ℕ → ℕ) → ℕ.  So we firstly
perform a translation within T to make it the base case of our
predicate.

\begin{code}

⟨_⟩ʸ : Ty  Ty
 ι ⟩ʸ     = (ι  ι)  ι
 σ  τ ⟩ʸ =  σ ⟩ʸ   τ ⟩ʸ

⟨_⟩ˣ : Cxt  Cxt
 ε ⟩ˣ     = ε
 Γ  ρ ⟩ˣ =  Γ ⟩ˣ   ρ ⟩ʸ

⟨_⟩ᵛ : {Γ : Cxt} {ρ : Ty}   ρ  Γ     ρ ⟩ʸ   Γ ⟩ˣ 
 zero ⟩ᵛ   = zero
 succ i ⟩ᵛ = succ  i ⟩ᵛ

KEᶥ : {Γ : Cxt} (ρ : Ty)
     T Γ ((ι   ρ ⟩ʸ)   ι ⟩ʸ   ρ ⟩ʸ)
KEᶥ  ι      = Lam (Lam (Lam (ν₂ · (ν₁ · ν₀) · ν₀)))
KEᶥ (_  ρ) = Lam (Lam (Lam (KEᶥ ρ · Lam (ν₃ · ν₀ · ν₁) · ν₁)))

⟨_⟩ᵐ : {Γ : Cxt} {ρ : Ty}  T Γ ρ  T  Γ ⟩ˣ  ρ ⟩ʸ
 Var i ⟩ᵐ   = Var  i ⟩ᵛ
 Lam t ⟩ᵐ   = Lam  t ⟩ᵐ
 f · a ⟩ᵐ   =  f ⟩ᵐ ·  a ⟩ᵐ
 Zero ⟩ᵐ    = Lam Zero
 Succ ⟩ᵐ    = Lam (Lam (Succ · (ν₁ · ν₀)))
 Rec {ρ} ⟩ᵐ = Lam (Lam (KEᶥ ρ · (Rec · ν₁ · Lam (ν₁ · Lam ν₁))))

--
-- A T-definable generic sequence in the sense of [1].
--
Ω : {Γ : Cxt}  T Γ ( ι  ι ⟩ʸ)
Ω = Lam (Lam (ν₀ · (ν₁ · ν₀)))

\end{code}

■ Relating terms and their b-translations

Following Escardo [1], we define a parametrised logical relation R
between the interpretations of terms and their b-translations.

\begin{code}

R : {ρ : Ty}  ℕᴺ    ρ ⟩ʸ ⟧ʸ   ρ ⟧ʸ  Set
R {ι    } α f n = f α  n
R {σ  τ} α f g = {x :   σ ⟩ʸ ⟧ʸ} {y :  σ ⟧ʸ}  R α x y  R α (f x) (g y)

 : {Γ : Cxt}  ℕᴺ    Γ ⟩ˣ ⟧ˣ   Γ ⟧ˣ  Set
 {ε}     _  _       _      = 𝟙
 {Γ  ρ} α (γ , a) (ξ , b) =  α γ ξ × R α a b

--
-- The Kleisli extension preserves R.
--
R[KEᶥ] : (ρ : Ty) (α : ℕᴺ) {f :     ρ ⟩ʸ ⟧ʸ} {g :    ρ ⟧ʸ}
        ((i : )  R α (f i) (g i))
        {Γ : Cxt} {γ :  Γ ⟧ˣ}
        R α ( KEᶥ ρ ⟧ᵐ γ f) g
R[KEᶥ]  ι      α ζ χ = trans (ζ _) (ap _ χ)
R[KEᶥ] (_  ρ) α ζ χ = λ η  R[KEᶥ] ρ α  i  ζ i η) χ

--
-- Variables in related contexts are related.
--
R[Var] : {Γ : Cxt} {ρ : Ty} {γ :   Γ ⟩ˣ ⟧ˣ} {ξ :  Γ ⟧ˣ} (α : ℕᴺ)
         α γ ξ  (i :  ρ  Γ )  R α (γ   i ⟩ᵛ ) (ξ  i )
R[Var] {ε}     α  _      ()
R[Var] {Γ  ρ} α (_ , θ)  zero    = θ
R[Var] {Γ  ρ} α (ζ , _) (succ i) = R[Var] α ζ i

--
-- Terms are related to their b-translations.
--
Lemma[R] : {Γ : Cxt} {ρ : Ty} (t : T Γ ρ) (α : ℕᴺ)
          {γ :   Γ ⟩ˣ ⟧ˣ} {ξ :  Γ ⟧ˣ}   α γ ξ
          R α (  t ⟩ᵐ ⟧ᵐ γ) ( t ⟧ᵐ ξ)
Lemma[R] (Var i)  α ζ = R[Var] α ζ i
Lemma[R] (Lam t)  α ζ = λ χ  Lemma[R] t α (ζ , χ)
Lemma[R] (f · a)  α ζ = Lemma[R] f α ζ (Lemma[R] a α ζ)
Lemma[R] Zero     _ _ = refl
Lemma[R] Succ     α _ = ap succ
Lemma[R] (Rec{ρ}) α _ {x} {y} χ {f} {g} η = goal
 where
  claim : (i : )  R {ρ} α (rec x  k  f  _  k)) i) (rec y g i)
  claim  0       = χ
  claim (succ i) = η refl (claim i)
  goal : R {ι  ρ} α ( KEᶥ ρ ⟧ᵐ _ (rec x  k  f  _  k)))) (rec y g)
  goal = R[KEᶥ] ρ α claim

--
-- A particular case of Lemma[R]
--
Lemma[R]ᶥ : (t : T ε ((ι  ι)  ι))
           (α : ℕᴺ)    t ⟩ᵐ · Ω  α   t  α
Lemma[R]ᶥ t α = Lemma[R] t α  (ap α)

\end{code}


===============================================
=                                             =
=  §2  Continuity of T-definable functionals  =
=                                             =
===============================================


■ Continuity of functions ℕᴺ → ℕ

\begin{code}

--
-- α ≡[ n ] β  expresses that the first n bits of α and β are equal
--
data _≡[_]_ {A : Set} : A     A   Set where
 ≡[zero] : {α β : A }  α ≡[ 0 ] β
 ≡[succ] : {α β : A } {n : }  head α  head β  tail α ≡[ n ] tail β  α ≡[ succ n ] β

≡[≤] : {A : Set} {α β : A } {n m : }
      α ≡[ n ] β  m  n  α ≡[ m ] β
≡[≤]  en             ≤zero    = ≡[zero]
≡[≤] (≡[succ] e en) (≤succ r) = ≡[succ] e (≡[≤] en r)

≡[]-< : {A : Set} {α β : A } {n i : }
       α ≡[ n ] β  succ i  n  α i  β i
≡[]-< (≡[succ] e en) (≤succ ≤zero)     = e
≡[]-< (≡[succ] e en) (≤succ (≤succ r)) = ≡[]-< en (≤succ r)

continuous : (ℕᴺ  )  Set
continuous f = (α : ℕᴺ)  Σ \(m : )  (β : ℕᴺ)  α ≡[ m ] β  f α  f β

continuity-extensional : {f g : ℕᴺ  }
                        ((α : ℕᴺ)  f α  g α)  continuous f  continuous g
continuity-extensional {f} {g} e cf α = m , prf
 where
  m : 
  m = pr₁ (cf α)
  prf : (β : ℕᴺ)  α ≡[ m ] β  g α  g β
  prf β em = trans (sym (e α)) (trans (pr₂ (cf α) β em) (e β))

\end{code}

■ A continuity predicate

\begin{code}

C : (ρ : Ty)    ρ ⟩ʸ ⟧ʸ  Set
C  ι      f = continuous f
C (σ  τ) f = {a :   σ ⟩ʸ ⟧ʸ}  C σ a  C τ (f a)

 : {Γ : Cxt}    Γ ⟩ˣ ⟧ˣ  Set
 {ε}            = 𝟙
 {Γ  ρ} (γ , a) =  γ × C ρ a

--
-- The generic sequence satisfies C
--
C[Ω] : C (ι  ι)  Ω 
C[Ω] {f} cf α = m , prf
 where
  n₀ : 
  n₀ = pr₁ (cf α)
  n₁ : 
  n₁ = succ (f α)
  m : 
  m = max n₀ n₁
  prf : (β : ℕᴺ)  α ≡[ m ] β  α (f α)  β (f β)
  prf β em = trans e₂ e₁
   where
    e₀ : f α  f β
    e₀ = pr₂ (cf α) β (≡[≤] em (max-spec₀ n₀ n₁))
    e₁ : β (f α)  β (f β)
    e₁ = ap β e₀
    e₂ : α (f α)  β (f α)
    e₂ = ≡[]-< em (max-spec₁ n₀ n₁)

--
-- The Kleisli extension preserves C.
--
C[KEᶥ] : (ρ : Ty)
        {g :     ρ ⟩ʸ ⟧ʸ}  ((i : )  C ρ (g i))
        {Γ : Cxt} {γ :  Γ ⟧ˣ}
        C (ι  ρ) ( KEᶥ ρ ⟧ᵐ γ g)
C[KEᶥ] ι {g} cg {_} {_} {f} cf = goal
 where
  goal : continuous  α  g (f α) α)
  goal α = m , prf
   where
    n₀ n₁ : 
    n₀ = pr₁ (cg (f α) α)
    n₁ = pr₁ (cf α)
    m : 
    m = max n₀ n₁
    prf : (β : ℕᴺ)  α ≡[ m ] β  g (f α) α  g (f β) β
    prf β em = trans e₂ e₁
     where
      e₀ : f α  f β
      e₀ = pr₂ (cf α) β (≡[≤] em (max-spec₁ n₀ n₁))
      e₁ : g (f α) β  g (f β) β
      e₁ = ap  i  g i β) e₀
      e₂ : g (f α) α  g (f α) β
      e₂ = pr₂ (cg (f α) α) β (≡[≤] em (max-spec₀ n₀ n₁))
C[KEᶥ] (_  ρ) cg cf = λ ca  C[KEᶥ] ρ  i  cg i ca) cf

--
-- Variables satisfy C.
--
C[Var] : {Γ : Cxt} {ρ : Ty} {γ :   Γ ⟩ˣ ⟧ˣ}
         γ  (i :  ρ  Γ )  C ρ (γ   i ⟩ᵛ )
C[Var] {ε}      _      ()
C[Var] {Γ  ρ} (δ , θ)  zero    = θ
C[Var] {Γ  ρ} (δ , θ) (succ i) = C[Var] δ i

--
-- The b-translation of any T term satisfies C.
--
Lemma[C] : {Γ : Cxt} {ρ : Ty} (t : T Γ ρ)
          {γ :   Γ ⟩ˣ ⟧ˣ}   γ  C ρ (  t ⟩ᵐ ⟧ᵐ γ)
Lemma[C] (Var i) δ = C[Var] δ i
Lemma[C] (Lam t) δ = λ θ  Lemma[C] t (δ , θ)
Lemma[C] (f · a) δ = Lemma[C] f δ (Lemma[C] a δ)
Lemma[C] Zero _ = λ α  (0 , λ _ _  refl)
Lemma[C] Succ _ {f} cf α = m , prf
 where
  m : 
  m = pr₁ (cf α)
  prf : (β : ℕᴺ)  α ≡[ m ] β  succ (f α)  succ (f β)
  prf β em = ap succ (pr₂ (cf α) β em)
Lemma[C] (Rec {ρ}) _ {a} ca {f} cf = C[KEᶥ] ρ cg
 where
  g :     ρ ⟩ʸ ⟧ʸ
  g = rec a  k  f  _  k))
  cg : (i : )  C ρ _
  cg  0       = ca
  cg (succ i) = cf  _  0 ,  _ _  refl)) (cg i)

\end{code}

■ Main result

\begin{code}

Theorem[TCont] : (f : ℕᴺ  )  T-definable f  continuous f
Theorem[TCont] f (t , refl) = cont-f
 where
  claim₀ : (α : ℕᴺ)    t ⟩ᵐ · Ω  α   t  α
  claim₀ = Lemma[R]ᶥ t
  claim₁ : continuous (  t ⟩ᵐ · Ω )
  claim₁ = Lemma[C] t  C[Ω]
  cont-f : continuous f
  cont-f = continuity-extensional claim₀ claim₁

\end{code}


====================================
=                                  =
=  §3  Experiments of computation  =
=                                  =
====================================


Because MLTT/Agda proofs are programs, we can run the main theorem to
compute moduli of continuity of T-definable functions.  We develop
some experiments to illustrate this.


■ (External) modulus-of-continuity functional M

\begin{code}

M : T ε ((ι  ι)  ι)  ℕᴺ  
M t α = pr₁ (Theorem[TCont]  t  (t , refl) α)

M-spec : (t : T ε ((ι  ι)  ι))
        (α β : ℕᴺ)  α ≡[ M t α ] β   t  α   t  β
M-spec t α = pr₂ (Theorem[TCont]  t  (t , refl) α)

\end{code}

■ Some auxiliaries

\begin{code}

Num :   {Γ : Cxt}  T Γ ι
Num  0       = Zero
Num (succ k) = Succ · Num k

Plus : {Γ : Cxt}  T Γ ι  T Γ ι  T Γ ι
Plus N M = Rec · N · Lam Succ · M

_+_ :     
n + m = rec n  _  succ) m

 : ℕᴺ
 i = 0

δ : ℕᴺ
δ i = i

infixr 1 _✶_

_✶_ :   ℕᴺ  ℕᴺ
(k  α)  0       = k
(k  α) (succ i) = α i

\end{code}

■ Examples of closed T terms

t₀ is a constant function

\begin{code}

t₀ : T ε ((ι  ι)  ι)
t₀ = Lam (Num 4)

t₀-interpretation :  t₀   λ α  4
t₀-interpretation = refl

result₀ :  M t₀   0
        ×  M t₀ δ  0
        ×  M t₀ succ  0
        ×  M t₀ (12  67  8  99  3  )  0
result₀ = refl , refl , refl , refl

\end{code}

t₁ is a non-trivial constant function: it applies the identity
function α₁₇ (the 18th bit of α) times on value 4.

\begin{code}

t₁ : T ε ((ι  ι)  ι)
t₁ = Lam (Rec · Num 4 · Lam (Lam ν₀) · (ν₀ · Num 17))

t₁-interpretation :  t₁   λ α  rec 4  _ k  k) (α 17)
t₁-interpretation = refl

result₁ :  M t₁   18
        ×  M t₁ δ  18
        ×  M t₁ succ  18
        ×  M t₁ (12  67  8  99  3  )  18
result₁ = refl , refl , refl , refl

\end{code}

t₂ is a simple function returning the 18th bit of the input.

\begin{code}

t₂ : T ε ((ι  ι)  ι)
t₂ = Lam (ν₀ · Num 17)

t₂-interpretation :  t₂   λ α  α 17
t₂-interpretation = refl

result₂ :  M t₂   18
        ×  M t₂ δ  18
        ×  M t₂ succ  18
        ×  M t₂ (12  67  8  99  3  )  18
result₂ = refl , refl , refl , refl

\end{code}

t₃ is taken from [2]:  λα.α(α(…(α0)…))  with α0 applications of α.

\begin{code}

t₃ : T ε ((ι  ι)  ι)
t₃ = Lam (Rec · Num 0 · Lam ν₁ · (ν₀ · Num 0))

t₃-interpretation :  t₃   λ α  rec 0  _  α) (α 0)
t₃-interpretation = refl

result₃ :  M t₃   1
        ×  M t₃ δ  1
        ×  M t₃ succ  1
        ×  M t₃ (12  67  8  99  3  )  13
result₃ = refl , refl , refl , refl

\end{code}

t₄ is taken from [1] in which is named t₃.

\begin{code}

t₄ : T ε ((ι  ι)  ι)
t₄ = Lam (Rec · (ν₀ · Num 1) · (Lam ν₁) · (Plus (ν₀ · Num 2) (ν₀ · Num 3)))

t₄-interpretation :  t₄   λ α  rec (α 1)  _  α) (α 2 + α 3)
t₄-interpretation = refl

result₄ :  M t₄   4
        ×  M t₄ δ  4
        ×  M t₄ succ  9
        ×  M t₄ (12  67  8  99  3  )  68
result₄ = refl , refl , refl , refl

\end{code}

t₅ is also taken from [1]. The evaluations of this complicated example
are instantaneous.

\begin{code}

t₅ : T ε ((ι  ι)  ι)
t₅ = Lam (Rec · (ν₀ · (Rec · (ν₀ · (Rec · (ν₀ · Num 17) · Lam ν₁ · (ν₀ · Num 17)))
                           · Lam ν₁
                           · (Rec · (Plus (ν₀ · (ν₀ · Num 2)) (ν₀ · Num 3))
                                  · Lam ν₁
                                  · (Rec · (ν₀ · Num 1) · Lam ν₁ · (Plus (ν₀ · Num 2) (ν₀ · Num 3))))))
              · (Lam ν₁)
              · (ν₀ · Num 2))

t₅-interpretation :  t₅   λ α  rec (α (rec (α (rec (α 17)  _  α) (α 17)))
                                                _  α)
                                               (rec (α (α 2) + α 3)
                                                     _  α)
                                                    (rec (α 1)  _  α) (α 2 + α 3)))))
                                        _  α)
                                       (α 2)
t₅-interpretation = refl

result₅ :  M t₅   18
        ×  M t₅ δ  18
        ×  M t₅ succ  58
        ×  M t₅ (12  67  8  99  3  )  68
result₅ = refl , refl , refl , refl

\end{code}