---------------------------------------------------------
      A Gentzen-style monadic translation of Gödel's System T
     ---------------------------------------------------------

                   Chuangjie Xu, August 2019


We present a monadic translation of Gödel's System T into itself in
the spirit of Gentzen's negative translation of classical logic into
minimal logic.  The translation is parametrized by a notion of nucleus
relative to T, that is, an endofunction J on types of T equipped with
terms

          η : ρ → J ρ    and    κ : (σ → J ρ) → J σ → J ρ

for any types ρ and σ.  If they satisfy the monad laws (i.e. the
equations of Kleisi extension), then the translation preserves all the
computation rules.  Working with different nuclei, we reveal various
structures of T-definable functions, such as majorizability, (uniform)
continuity and bar recursion.


This Agda development is organized as follow:

1. Gödel's system T (extended with products and coproducts)

2. A Gentzen-style monadic translation of System T

3. Examples of nuclei and their applications

4. Other monadic translations of System T


All the files are tested in the safe mode of Agda version 2.6.0.1.

\begin{code}

{-# OPTIONS --safe #-}

\end{code}

■ Gödel's system T

we work with the lambda-calculus version of system T.  To illustrate
the correspondence between our syntactic translation and Gentzen's
negative translation, we extend T with products and coproducts in the
module Tplus.

\begin{code}

import T
import Tplus  -- Extension with products and coproducts

\end{code}

■ A Gentzen-style monadic translation

We define a syntactic translation of T into itself, parametrized by a
nucleus (J, η, κ) which is given as module parameters.

\begin{code}

import GentzenTranslation

\end{code}

■ Example I: lifting to higher types

We lift natural numbers to functions of type X → ℕ for type X of T.
This allows us to apply the syntactic method to prove properties of
functions of type X → ℕ.

\begin{code}

import Lifting

\end{code}

■ Example II: continuity

Given a term f : ℕᴺ → ℕ in T, we obtain a term M : ℕᴺ → ℕ which is a
modulus of continuity of f from the translation of f.

\begin{code}

import Continuity

\end{code}

For simplicity, in the following examples, we consider T without
coproducts and combine the monadic translation with the natural
embedding into Agda.

■ Example III : uniform continuity

Given a term f : ℕᴺ → ℕ in T, we obtain from the translation of f a
function M : ℕᴺ → ℕ such that, for any θ : ℕᴺ, M(θ) is a modulus of
uniform continuity of f restricted to inputs pointwise bounded by θ.

\begin{code}

import UniformContinuity

\end{code}

■ Example IV: majorizability

For any term t in T, the translation of t majorizes t.

\begin{code}

import Majorizability

\end{code}

■ Example V: bar recursion

Given Y : ℕᴺ → ℕ in T, we obtain a general-bar-recursion functional
form the translation of Y.

\begin{code}

import BarRecursion

\end{code}

■ Other monadic translations

We implement another two monadic translaitons, corresponding to the
negative translations due to Kuroda and Kolmogorov.

\begin{code}

import KurodaTranslation
import KolmogorovTranslation

\end{code}