An Agda implementation of

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

                          Chuangjie Xu

         February 2018, updated in June and September 2018


We recover the well-known fact that

  all Gödel's system T definable functions (ℕ → ℕ) → ℕ are continuous

via a syntactic approach.  Differing from the usual syntactic method,
we firstly perform a translation of system T into itself where
particularly natural numbers are translated to functions (ℕ → ℕ) → ℕ.
Then we inductively define a continuity predicate on the elements of
translated types and show that the translation of any term in system T
satisfies the continuity predicate.  We obtain the desired result by
relating terms and their translations via a parametrized logical
relation.  We adapt and generalize our method to prove other notions
of continuity.

This Agda development contains the following sections of the paper

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

  §3. Continuity of T-definable functionals

  §4. T-definable moduli of continuity

  §5.1. Uniform continuity

In addition, we also implement the following

  Appendix I.  Continuity via a monadic interpretation of T

  Appendix II. Dialogue tree representation of T-definable functionals

that are briefly mentioned in the introduction of the paper.


\begin{code}

---------------------------------------------
-- §2. Gödel's system T and the b-translation
---------------------------------------------
import T

\end{code}

The first step of our syntactic method is to perform a translation

                      (t ↦ tᵇ) : ρ → ρᵇ

from system T to itself, which we call b-translation. In particular,
we define ℕᵇ :≡ (ℕ → ℕ) → ℕ.  Using a parametrized logical relation,
we show that any f : (ℕ → ℕ) → ℕ is pointwise equal to fᵇ(Ω), where
fᵇ : (ℕᵇ → ℕᵇ) → ℕᵇ is the b-translation of f and Ω : ℕᵇ → ℕᵇ is a
T-definable generic element.


\begin{code}

--------------------------------------------
-- §3. Continuity of T-definable functionals
--------------------------------------------
import Continuity

\end{code}

We inductively define a continuity predicate

                          C  ⊆  ρᵇ

whose base case C(f) states the continuity of f : (ℕ → ℕ) → ℕ.  By
induction on terms, we show that the b-translation of any term
satisfies C.  Moreover, we have C(Ω) and thus C(fᵇ(Ω)), i.e. fᵇ(Ω) is
continuous, for any f : (ℕ → ℕ) → ℕ in system T.  Because continuity
is preserved under pointwise equality, f is also continuous.


\begin{code}

---------------------------------------
-- §4. T-definable moduli of continuity
---------------------------------------
import TModuli

\end{code}

By restructuring the above proof, we adapt our b-translation to
directly construct T-definable moduli of continuity.  Now natural
numbers are translated to pairs of functions (ℕ → ℕ) → ℕ.  The idea is
that the second component is a modulus of continuity of the first one
which is the b-translation (of some term).  Working with a logical
relation and a predicate that are slightly different from above, we
show that every T-definable function (ℕ → ℕ) → ℕ has a T-definable
modulus of continuity.


\begin{code}

------------------------------------------------------
-- §5.1. Uniform continuity of T-definable functionals
------------------------------------------------------
import UniformContinuity

\end{code}

Working with a predicate UC ⊆ ρᵇ whose base case UC(f) states that the
restriction f↾𝟚ᴺ to the Cantor type ℕ → 𝟚 is uniformly continuous, we
show that if f : (ℕ → ℕ) → ℕ is T-definable then f↾𝟚ᴺ : (ℕ → 𝟚) → ℕ is
uniformly continuous.


\begin{code}

-----------------------------------------------------------
-- Appendix I. Continuity via a monadic interpretation of T
-----------------------------------------------------------
import TContMonad

\end{code}

In the introduction of the paper, we claim that the algorithm of
Coquand and Jaber's operational method can be represented by a monadic
translation of system T into itself.  Here we present such a monadic
interpretation of system T extended with a generic element into Agda.


\begin{code}

-----------------------------------------------------------------------
-- Appendix II. Dialogue tree representation of T-definable functionals
-----------------------------------------------------------------------
import Dialogue

\end{code}

The dialogue tree representing a function f : (ℕ → ℕ) → ℕ can be
considered as a notion of continuity of f which contains more
information than e.g. pointwise continuity.  Instead of building a
model of system T using dialogue trees, here we use our syntactic
method to show that every T-definable function (ℕ → ℕ) → ℕ has a
dialogue tree representation.