16122 LABEL:LastPageApr. 23, 2019Feb. 20, 2020

# A syntactic approach to continuity
of T-definable functionals

Chuangjie Xu  Ludwig-Maximilians-Universität München<EMAIL_ADDRESS>
###### Abstract.

We give a _new_ proof of the well-known fact that all functions
$(\mathbb{N}\to\mathbb{N})\to\mathbb{N}$ which are definable in Gödel’s System
$\T$ are continuous via a _syntactic_ approach. Differing from the usual
syntactic method, we firstly perform a translation of System $\T$ into itself
in which natural numbers are translated to functions
$(\mathbb{N}\to\mathbb{N})\to\mathbb{N}$. Then we inductively define a
continuity predicate on the translated elements 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. Our constructions and proofs have been formalized in the
Agda proof assistant. Because Agda is also a programming language, we can
execute our proof to compute moduli of continuity of $\T$-definable functions.

###### Key words and phrases:

syntactic method, Gödel’s System $\T$, (uniform) continuity, Baire space,
Cantor space, logical relation, Agda.

##  1\. Introduction

The usual syntactic method for proving properties of terms in Gödel’s System
$\T$ works as follows: (1) Define a predicate $P_{\rho}\subseteq\rho$ for the
designated property by induction on the finite type $\rho$, _i.e._

$\begin{array}[]{rll}P_{\mathbb{N}}(n)&:\equiv&\cdots\\\\[2.0pt]
P_{\sigma\to\tau}(g)&:\equiv&\forall x^{\sigma}\left(P_{\sigma}(x)\to
P_{\tau}(g(x))\right).\end{array}$

(2) Prove that each term $t:\rho$ in $\T$ satisfies $P_{\rho}$ by induction on
$t$. Examples of properties for which such syntactic methods work include
totality [18] and majorizability [11]. Our goal is to recover the well-known
fact that all $\T$-definable functions
$(\mathbb{N}\to\mathbb{N})\to\mathbb{N}$ are continuous [2]. But the above
syntactic method does not seem to work directly, because we do not know how to
define the base case $P_{\mathbb{N}}$ such that
$P_{(\mathbb{N}\to\mathbb{N})\to\mathbb{N}}(f)$ expresses the continuity of
$f$.

Our idea is, as a step (0), to perform a translation $(t\mapsto
t^{\mathrm{b}}):\rho\to\rho^{\mathrm{b}}$ of System $\T$ into itself where
$\mathbb{N}^{\mathrm{b}}:\equiv(\mathbb{N}\to\mathbb{N})\to\mathbb{N}$, i.e.
natural numbers are translated to functions
$(\mathbb{N}\to\mathbb{N})\to\mathbb{N}$. Further, any function
$f:(\mathbb{N}\to\mathbb{N})\to\mathbb{N}$ in $\T$ is pointwise equal to
$f^{\mathrm{b}}(\Omega)$, where
$f^{\mathrm{b}}:(\mathbb{N}^{\mathrm{b}}\to\mathbb{N}^{\mathrm{b}})\to\mathbb{N}^{\mathrm{b}}$
is the translation of $f$ and
$\Omega:\mathbb{N}^{\mathrm{b}}\to\mathbb{N}^{\mathrm{b}}$ is a $\T$-definable
generic element in the sense of [3, 4, 5]. Then our step (1) is to inductively
define a continuity predicate $\mathrm{C}_{\rho}\subseteq\rho^{\mathrm{b}}$:
the base case $\mathrm{C}_{\mathbb{N}}(f)$ states the continuity of
$f:(\mathbb{N}\to\mathbb{N})\to\mathbb{N}$ and the one for function spaces is
defined in the usual way as above. And our step (2) is to prove
$\mathrm{C}_{\rho}(t^{\mathrm{b}})$ for all terms $t:\rho$ in $\T$ by
induction on $t$. Moreover, the generic element $\Omega$ also satisfies the
continuity predicate $\mathrm{C}$. We thus have
$\mathrm{C}_{\mathbb{N}}(f^{\mathrm{b}}(\Omega))$, i.e.
$f^{\mathrm{b}}(\Omega)$ is continuous, for any
$f:(\mathbb{N}\to\mathbb{N})\to\mathbb{N}$ in $\T$. Because continuity is
preserved under pointwise equality, we know that $f$ is also continuous. As
pointed out by one of the anonymous referees, our results that any term is
related to its translation (Lemma 1) and that the translation of any term
satisfies the continuity predicate (Lemma 4) are instances of the _fundamental
theorem of logical relations_ [19].

Our development is constructive and has been formalized in the Agda proof
assistant [1]. The main purpose of this formalization is to execute our Agda
proof which is also a computer program to compute moduli of continuity, rather
than merely certify the correctness of our work. Some sample computations of
moduli of continuity are provided in our Agda development [25].

### Motivation

Oliva and Steila [13] give a direct proof of Schwichtenberg’s theorem that the
terms of Gödel’s System $\T$ are closed under the rule of Spector’s bar
recursion of types 0 and 1 [16]. By induction on terms, they explicitly
construct a functional of their notion of _general bar recursion_ for each
term in $\T$, and then turn it into a functional of Spector’s bar recursion.
The author implemented their work in Agda [24] and recognized that some part
of their correctness proof [13, Theorem 3.4] can be adapted to compute moduli
of continuity. For each term $t$ in $\T$, a bar is constructed to control the
behavior of the general-bar-recursion functional for $t$. This bar essentially
contains the continuity information of $t$. The Agda code of this part of the
correctness proof was then separated, refined and further developed under the
inspiration of Escardó’s Agda development of dialogue trees [5], which led to
the first version of the Agda implementation of this paper [25].

### Related work

Kohlenbach [10] obtains the uniform continuity of terms
$(\mathbb{N}\to\mathbb{N})\to\mathbb{N}$ in System $\T$ as an application of
his pointwise version of strong majorization. In particular, his logical
relation for majorization on functions from natural numbers is given in a
pointwise way. He shows that every term $t:\rho$ in $\T$ is pointwise strongly
majorized by some $t^{*}:\rho$ in $\T$ by induction on $t$. For any
$f:(\mathbb{N}\to\mathbb{N})\to\mathbb{N}$ in $\T$, one can show in the
intuitionistic system WE-HAω that it is extensional. From such a proof,
Kohlenbach extracts a term via the Dialectica interpretation and then uses the
majorant of this term to construct a modulus of uniform continuity of $f$.

Coquand and Jaber’s approach to continuity [3, 4] is also syntactic. The
difference is that they obtain continuity information by an operational
method: they extend dependent type theory with a new constant $\mathsf{f}$ for
a generic element, and then decorate its operational semantics with forcing
information to keep track of approximation information about $\mathsf{f}$ as
the computations proceed. The continuity information of a function $F$ is
extracted from the computation of $F(\mathsf{f})$. They tackle uniform
continuity of functions from the Cantor space $\mathbb{N}\to\mathbbm{2}$,
where $\mathbbm{2}:\equiv\\{0,1\\}$, and also discuss how to adapt their
argument for continuity of functions from the Baire space
$\mathbb{N}\to\mathbb{N}$ [4, Section 1.2.3]. They also provide a Haskell
implementation for System $\T$ using a monad combined by the list monad and
the state monad as an appendix in [4]. The algorithm to extract continuity
information in their operational method restricted to System $\T$ can be
represented as a monadic translation of System $\T$ into itself which is an
instance of [14, Section 4].

Inspired by Coquand and Jaber’s work, Escardó also employs a generic element
but in his dialogue tree model to prove (uniform) continuity of $\T$-definable
functions [5]. He has a concrete notion of generic element given by a function
$\tilde{\mathbb{N}}\to\tilde{\mathbb{N}}$, where $\tilde{\mathbb{N}}$ is the
set of dialogue trees. Suppose a function
$f:(\mathbb{N}\to\mathbb{N})\to\mathbb{N}$ is denoted by a term $t$ whose
dialogue interpretation is a function
$\tilde{f}:(\tilde{\mathbb{N}}\to\tilde{\mathbb{N}})\to\tilde{\mathbb{N}}$.
Applying $\tilde{f}$ to the generic element, a dialogue tree which contains
the (uniform) continuity information of $f$ is obtained. In one version of the
Agda implementation of [5], Escardó uses Church encodings of dialogue trees to
turn his semantic interpretation into a compositional translation of System
$\T$ into itself. In this way, he extracts from the Church encoding of the
dialogue tree interpreting $t$ a term $m$ in $\T$ which internalizes the
modulus of continuity of $f$. We provide a direct and explicit construction of
terms in $\T$ internalizing moduli of continuity in Section 4.1 .

Our method is also related to the sheaf model [26, 6, 22] introduced by
Escardó and the author. To prove uniform continuity of $\T$-definable
functions, it is sufficient to work with the subcategory of concrete sheaves
which admit a more intuitive description as what we call $\mathrm{C}$-spaces.
A $\mathrm{C}$-space is a set $X$ equipped with a certain collection of maps
${\mathbbm{2}^{\mathbb{N}}}\to X$ which are called probes on $X$, where
${\mathbbm{2}^{\mathbb{N}}}:\equiv\mathbb{N}\to\mathbbm{2}$. A
$\mathrm{C}$-continuous map of $\mathrm{C}$-spaces is a function whose
composition with a probe is again a probe. For instance, the set $\mathbb{N}$
with all uniformly continuous maps ${\mathbbm{2}^{\mathbb{N}}}\to\mathbb{N}$
forms a $\mathrm{C}$-space; so does ${\mathbbm{2}^{\mathbb{N}}}$ with all
uniformly continuous maps
${\mathbbm{2}^{\mathbb{N}}}\to{\mathbbm{2}^{\mathbb{N}}}$. A crucial tool in
this semantic method is the Yoneda Lemma which says that a function
${\mathbbm{2}^{\mathbb{N}}}\to X$ into a $\mathrm{C}$-space $X$ is
$\mathrm{C}$-continuous iff it is a probe on $X$. Each term
$t:(\mathbb{N}\to\mathbbm{2})\to\mathbb{N}$ in $\T$ is interpreted as a
$\mathrm{C}$-continuous map ${\mathbbm{2}^{\mathbb{N}}}\to\mathbb{N}$ in the
category of $\mathrm{C}$-spaces and thus, by the Yoneda Lemma, a probe on
$\mathbb{N}$, i.e. a uniformly continuous function. Interestingly, the proof
of one direction of the Yoneda Lemma is essentially the same proof of that
$\Omega$ satisfies a certain uniform-continuity predicate studied in Section
4.2. To investigate the relationship between our syntactic method and sheaf
models [7, 8, 9, 21] is left as one of our future tasks.

Another different approach to continuity is to use computational effects such
as exceptions [12, 15]. Suppose a function
$f:(\mathbb{N}\to\mathbb{N})\to\mathbb{N}$ and a sequence
$\alpha:\mathbb{N}\to\mathbb{N}$ are given. We can find a number $m$ such that
the value of $f(\alpha)$ depends only on the first $m$ positions of $\alpha$
(i.e. a modulus of continuity of $f$ at $\alpha$) as follows: An exception is
thrown if $f$ attempts to compute $\alpha(n)$ for $n\geq k$ where $k$ is a
variable parameter. We start with computing $f(\alpha)$ with $k=0$. Once an
exception is caught, we try $k+1$. At some point no exception happens and the
current value of $k$ is a modulus of continuity of $f$.

### Organization

Section 2 introduces the $\mathrm{b}$-translation of System $\T$ as a
preliminary for the syntactic method. Section 3 employs the syntactic method
on the $\mathrm{b}$-translation of System $\T$ to prove continuity of
$\T$-definable functions $(\mathbb{N}\to\mathbb{N})\to\mathbb{N}$. Section 4
strengthens the result by constructing terms in System $\T$ which internalize
moduli of continuity, and studies uniform continuity of $\T$-definable
functions $(\mathbb{N}\to\mathbbm{2})\to\mathbb{N}$. The last section
discusses how to generalize the method for proving properties of
$\T$-definable functions of arbitrary finite types.

##  2\. Gödel’s System $\T$ and the $\mathrm{b}$-translation

We work with Gödel’s System $\T$ in its lambda-calculus form. Recall that the
term language of $\T$ is (equivalent to) a simply typed lambda calculus
extended with natural numbers and a primitive recursor. The constants and
equations (i.e. computational rules) associated to the ground type
$\mathbb{N}$ include

  * •

the natural number $0:\mathbb{N}$,

  * •

the successor function $\mathrm{succ}:\mathbb{N}\to\mathbb{N}$, and

  * •

the primitive recursor
$\mathrm{rec}:\rho\to(\mathbb{N}\to\rho\to\rho)\to\mathbb{N}\to\rho$ with

$\mathrm{rec}(a)(f)(0)=a\qquad\mathrm{rec}(a)(f)(\mathrm{succ}\
n)=f(n)(\mathrm{rec}(a)(f)(n))$

for every finite type $\rho$.

A function is called $\T$-_definable_ if there exists a closed term in $\T$
denoting it. In the paper, we do not distinguish $\T$-definable functions and
their corresponding $\T$-terms. Moreover, we may write $n+1$ rather that
$\mathrm{succ}(n)$, and $\alpha_{i}$ rather than $\alpha(i)$ for
$\alpha:\mathbb{N}\to\mathbb{N}$ and $i:\mathbb{N}$.

As discussed earlier, it does not seem possible to directly apply the
syntactic method to prove continuity of $\T$-definable functions
$(\mathbb{N}\to\mathbb{N})\to\mathbb{N}$. Hence we ‘precook’ $\T$-terms so
that continuity becomes the base case of a predicate which all ‘precooked’
terms will satisfy. We call this procedure the $\mathrm{b}$-_translation_
where $\mathrm{b}$ stands for the Baire type/space, because natural numbers
are translated to functionals from the Baire type $\mathbb{N}\to\mathbb{N}$.

[$\mathrm{b}$-translation] For each finite type $\rho$ we associate a finite
type $\rho^{\mathrm{b}}$ inductively as follows:

$\begin{array}[]{rll}\mathbb{N}^{\mathrm{b}}&:\equiv&(\mathbb{N}\to\mathbb{N})\to\mathbb{N}\\\\[2.0pt]
(\sigma\to\tau)^{\mathrm{b}}&:\equiv&\sigma^{\mathrm{b}}\to\tau^{\mathrm{b}}.\end{array}$

Assume a given mapping of variables $x:\rho$ to variables
$x^{\mathrm{b}}:\rho^{\mathrm{b}}$. For any term $t:\rho$ in $\T$, we define
$t^{\mathrm{b}}:\rho^{\mathrm{b}}$ inductively as follows:

$\begin{array}[]{rll}(x)^{\mathrm{b}}&:\equiv&x^{\mathrm{b}}\\\\[2.0pt]
(\lambda x.u)^{\mathrm{b}}&:\equiv&\lambda
x^{\mathrm{b}}.u^{\mathrm{b}}\\\\[2.0pt]
(fa)^{\mathrm{b}}&:\equiv&f^{\mathrm{b}}a^{\mathrm{b}}\\\\[2.0pt]
0^{\mathrm{b}}&:\equiv&\lambda\alpha.0\\\\[2.0pt]
\mathrm{succ}^{\mathrm{b}}&:\equiv&\lambda
f\alpha.\mathrm{succ}(f\alpha)\\\\[2.0pt]
\mathrm{rec}^{\mathrm{b}}&:\equiv&\lambda
af.\mathrm{ke}(\mathrm{rec}(a)(\lambda k.f(\lambda\alpha.k)))\end{array}$

where
$\mathrm{ke}_{\rho}:(\mathbb{N}\to\rho^{\mathrm{b}})\to\mathbb{N}^{\mathrm{b}}\to\rho^{\mathrm{b}}$
is inductively defined by

$\begin{array}[]{rll}\mathrm{ke}_{\mathbb{N}}(g)(f)&:\equiv&\lambda\alpha.g(f\alpha)(\alpha)\\\\[2.0pt]
\mathrm{ke}_{\sigma\to\tau}(g)(f)&:\equiv&\lambda x.\mathrm{ke}_{\tau}(\lambda
k.g(k)(x))(f).\end{array}$

In the above definition, the only difficulty arrises when translating the
primitive recursor: To be a sound translation,
$\mathrm{rec}^{\mathrm{b}}:\rho^{\mathrm{b}}\to(\mathbb{N}^{\mathrm{b}}\to\rho^{\mathrm{b}}\to\rho^{\mathrm{b}})\to\mathbb{N}^{\mathrm{b}}\to\rho^{\mathrm{b}}$
has to preserve the computational rules of $\mathrm{rec}$, i.e.
$\mathrm{rec}^{\mathrm{b}}$ should satisfy

$\mathrm{rec}^{\mathrm{b}}(a)(f)(0^{\mathrm{b}})=a\qquad\mathrm{rec}^{\mathrm{b}}(a)(f)(\mathrm{succ}\
n)^{\mathrm{b}}=f(n^{\mathrm{b}})(\mathrm{rec}^{\mathrm{b}}(a)(f)(n^{\mathrm{b}}))$

where $k^{\mathrm{b}}:\mathbb{N}^{\mathrm{b}}$ is the constant function
$\lambda\alpha.k$ for any $k:\mathbb{N}$. One suitable candidate for such
$\mathrm{rec}^{\mathrm{b}}(a)(f):\mathbb{N}^{\mathrm{b}}\to\rho^{\mathrm{b}}$
is $\mathrm{rec}(a)(\lambda k.f(k^{\mathrm{b}}))$ but it has type
$\mathbb{N}\to\rho^{\mathrm{b}}$. In general, we can extend a function
$g:\mathbb{N}\to\rho^{\mathrm{b}}$ to
$g^{*}:\mathbb{N}^{\mathrm{b}}\to\rho^{\mathrm{b}}$ such that
$g^{*}(i^{\mathrm{b}})=g(i)$ for all $i:\mathbb{N}$, by induction on the
finite type $\rho$. We write $\mathrm{ke}$ to denote the extension function
($g\mapsto g^{*}$) as it behaves like a _Kleisli extension_ for functions
$\mathbb{N}\to\rho^{\mathrm{b}}$. However, in general, our
$\mathrm{b}$-translation does not seem to be a monad, let alone a functor.

Our first goal is to prove certain “equality” between any closed term
$f:{(\mathbb{N}\to\mathbb{N})\to\mathbb{N}}$ and its translation
$f^{\mathrm{b}}$ so that once $f^{\mathrm{b}}$ satisfies a predicate for some
property such as continuity in Section 3 then so does $f$. We firstly relate
terms and their $\mathrm{b}$-translations using the following _parametrized
logical relation_ that was introduced in a version of the Agda implementation
of [5]. For any $\alpha:\mathbb{N}\to\mathbb{N}$, we define a logical relation
$\mathrm{R}_{\rho}^{\alpha}\subseteq\rho^{\mathrm{b}}\times\rho$ by

$\begin{array}[]{rll}f\ \mathrm{R}_{\mathbb{N}}^{\alpha}\
n&:\equiv&f(\alpha)=n\\\\[2.0pt] g\ \mathrm{R}_{\sigma\to\tau}^{\alpha}\
h&:\equiv&\forall x^{\sigma^{\mathrm{b}}},y^{\sigma}\left(x\
\mathrm{R}_{\sigma}^{\alpha}\ y\to g(x)\ \mathrm{R}_{\tau}^{\alpha}\
h(y)\right).\end{array}$

We may omit the subscript and simply write $\mathrm{R}^{\alpha}$ if it can be
inferred from the context.

######  Lemma 1.

For any term $t:\rho$ in $\T$, we have

$t^{\mathrm{b}}\ \mathrm{R}^{\alpha}\ t$

for all $\alpha:\mathbb{N}\to\mathbb{N}$, assuming $x^{\mathrm{b}}\
\mathrm{R}^{\alpha}\ x$ for all $x\in\mathrm{FV}(t)$.

######  Proof 2.1.

Let $\alpha:\mathbb{N}\to\mathbb{N}$ be given. We carry out the proof by
structural induction over $t$. As the others are trivial, here we prove only
the case $t\equiv\mathrm{rec}$ with the following claims:

  1. (1)

The Kleisli extension $\mathrm{ke}$ preserves the relation
$\mathrm{R}^{\alpha}$, i.e.

$\mathrm{ke}(g)\ \mathrm{R}_{\mathbb{N}\to\rho}^{\alpha}\ h$

for any $g:\mathbb{N}\to\rho^{\mathrm{b}}$ and $h:\mathbb{N}\to\rho$ with
$g(i)\ \mathrm{R}^{\alpha}\ h(i)$ for all $i:\mathbb{N}$.

######  Proof 2.2.

By induction on $\rho$.

  2. (2)

Given $x:\rho^{\mathrm{b}}$ and $y:\rho$ with $x\ \mathrm{R}^{\alpha}\ y$, and
$f:\mathbb{N}^{\mathrm{b}}\to\rho^{\mathrm{b}}\to\rho^{\mathrm{b}}$ and
$g:\mathbb{N}\to\rho\to\rho$ with $f\ \mathrm{R}^{\alpha}\ g$,

$\mathrm{rec}(x)(\lambda k.f(\lambda\alpha.k))(i)\ \mathrm{R}^{\alpha}\
\mathrm{rec}(y)(g)(i)$

for all $i:\mathbb{N}$.

######  Proof 2.3.

By induction on $i$.

By applying (1) to (2), we get a proof of $\mathrm{rec}^{\mathrm{b}}\
\mathrm{R}^{\alpha}\ \mathrm{rec}$.

Hence we have $f^{\mathrm{b}}\ \mathrm{R}^{\alpha}\ f$ for any closed
$f:(\mathbb{N}\to\mathbb{N})\to\mathbb{N}$. Unfolding it according to
Definition 2, we can see that a term
$\Omega:\mathbb{N}^{\mathrm{b}}\to\mathbb{N}^{\mathrm{b}}$ with $\Omega\
\mathrm{R}^{\alpha}\ \alpha$ is needed in order to get the equality
$f^{\mathrm{b}}(\Omega)(\alpha)=f(\alpha)$. Such a term $\Omega$ can be viewed
as a _generic element_ [3, 4] or _generic sequence_ [5], and can be easily
defined by unfolding $\Omega\ \mathrm{R}^{\alpha}\ \alpha$: because $\Omega\
\mathrm{R}^{\alpha}\ \alpha$ is unfolded to

$\forall
f^{(\mathbb{N}\to\mathbb{N})\to\mathbb{N}},n^{\mathbb{N}}\left(f(\alpha)=n\to\Omega(f)(\alpha)=\alpha(n)\right)$

by replacing $n$ by $f\alpha$ as they are equal by assumption, we define
$\Omega:\mathbb{N}^{\mathrm{b}}\to\mathbb{N}^{\mathrm{b}}$ by

$\Omega(f)(\alpha)\ :\equiv\ \alpha(f\alpha).$

Then the following lemma is trivial but is necessary for deriving our first
result.

######  Lemma 2.

For any $\alpha:\mathbb{N}\to\mathbb{N}$, we have

$\Omega\ \mathrm{R}^{\alpha}\ \alpha.$

Our first result follows directly from Lemmas 1 and 2.

######  Theorem 3.

For any closed term $f:(\mathbb{N}\to\mathbb{N})\to\mathbb{N}$ in $\T$,

$f^{\mathrm{b}}(\Omega)(\alpha)=f(\alpha)$

for all $\alpha:\mathbb{N}\to\mathbb{N}$.

##  3\. Continuity of $\T$-definable functionals

After “precooking” $\T$ as above, we can now carry out the steps of the usual
syntactic method. The crucial difference is that the predicate to work with is
defined instead on elements of the $\mathrm{b}$-translated types, so that
continuity of functions $(\mathbb{N}\to\mathbb{N})\to\mathbb{N}$ becomes the
base case of the predicate. With a proof by induction on terms, we show that
the $\mathrm{b}$-translation of any term in $\T$ satisfies the predicate. The
case for closed terms of type $(\mathbb{N}\to\mathbb{N})\to\mathbb{N}$ will
bring us the desired result.

Recall that a function $f:(\mathbb{N}\to\mathbb{N})\to\mathbb{N}$ is
_continuous_ if for any sequence $\alpha:\mathbb{N}\to\mathbb{N}$ there exists
$m:\mathbb{N}$, called a _modulus of continuity_ of $f$ at the point $\alpha$,
such that any sequence $\beta:\mathbb{N}\to\mathbb{N}$ which is equal to
$\alpha$ up to the first $m$ positions gives the same result. In e.g.
$\mathrm{HA}^{\omega}$, the continuity of $f$ can be formulated as

$\forall\alpha^{\mathbb{N}\to\mathbb{N}}\ \exists m^{\mathbb{N}}\
\forall\beta^{\mathbb{N}\to\mathbb{N}}\ \left(\alpha=_{m}\beta\to
f(\alpha)=f(\beta)\right)$

where $\alpha=_{m}\beta$ stands for $\forall i<m\ \alpha_{i}=\beta_{i}$. It is
obvious that continuity is preserved under pointwise equality in the sense
that if $f:(\mathbb{N}\to\mathbb{N})\to\mathbb{N}$ is continuous then so is
any function that is pointwise equal to $f$.

We define a continuity predicate on elements of the $\mathrm{b}$-translated
types and show that the $\mathrm{b}$-translation of any term in $\T$ satisfies
the predicate.

We define a unary predicate $\mathrm{C}_{\rho}\subseteq\rho^{\mathrm{b}}$
inductively on $\rho$ by

$\begin{array}[]{rll}\mathrm{C}_{\mathbb{N}}(f)&:\equiv&\text{$f$ is
continuous}\\\\[2.0pt] \mathrm{C}_{\sigma\to\tau}(g)&:\equiv&\forall
x^{\sigma^{\mathrm{b}}}\left(\mathrm{C}_{\sigma}(x)\to\mathrm{C}_{\tau}(g(x))\right).\end{array}$

######  Lemma 4.

For any term $t:\rho$ in $\T$, we have

$\mathrm{C}_{\rho}(t^{\mathrm{b}})$

assuming $\mathrm{C}(x^{\mathrm{b}})$ for all $x\in\mathrm{FV}(t)$.

######  Proof 3.1.

By induction on the term $t$. Here we prove only the case
$t\equiv\mathrm{rec}$ with two claims.

  1. (1)

The Kleisli extension $\mathrm{ke}$ preserves the predicate $\mathrm{C}$, i.e.

$\mathrm{C}_{\mathbb{N}\to\rho}(\mathrm{ke}(g))$

for any $g:\mathbb{N}\to\rho^{\mathrm{b}}$ such that $\mathrm{C}_{\rho}(g(i))$
for all $i:\mathbb{N}$.

######  Proof 3.2.

By induction on $\rho$. (i) $\rho=\mathbb{N}$. Given
$g:\mathbb{N}\to\mathbb{N}^{\mathrm{b}}$ with $g(i)$ continuous for all
$i:\mathbb{N}$ and $f:\mathbb{N}^{\mathrm{b}}$ continuous, we need to show
that $\mathrm{ke}(g)(f)$ is continuous. Given
$\alpha:\mathbb{N}\to\mathbb{N}$, let $m$ be the modulus of $g(f\alpha)$ at
$\alpha$ and let $n$ be the modulus of $f$ at $\alpha$. Take
$k:\equiv\max(m,n)$. Given $\beta:\mathbb{N}\to\mathbb{N}$ with
$\alpha=_{k}\beta$, we have

$\begin{array}[]{lllll}\mathrm{ke}(g)(f)(\alpha)&=&g(f\alpha)(\alpha)\\\
&=&g(f\alpha)(\beta)&&(\text{by the continuity of }g(f\alpha))\\\
&=&g(f\beta)(\beta)&&(f\alpha=f\beta\text{ by the continuity of }f)\\\
&=&\mathrm{ke}(g)(f)(\beta).\end{array}$

(ii) $\rho=\sigma\to\tau$. Given
$g:\mathbb{N}\to\sigma^{\mathrm{b}}\to\tau^{\mathrm{b}}$ with
$\mathrm{C}_{\sigma\to\tau}(g(i))$ for all $i:\mathbb{N}$,
$f:\mathbb{N}^{\mathrm{b}}$ with $\mathrm{C}_{\mathbb{N}}(f)$ and
$a:\sigma^{\mathrm{b}}$ with $\mathrm{C}_{\sigma}(a)$, we have to show
$\mathrm{C}_{\tau}(\mathrm{ke}(g)(f)(a))$. Define
$h:\mathbb{N}\to\tau^{\mathrm{b}}$ by $h(i):\equiv g(i)(a)$. Then we have
$\mathrm{ke}(h)(f)=\mathrm{ke}(g)(f)(a)$ by definition and
$\mathrm{C}_{\tau}(\mathrm{ke}(h)(f))$ by the induction hypothesis.

  2. (2)

Given $a:\rho^{\mathrm{b}}$ with $\mathrm{C}_{\rho}(a)$ and
$f:\mathbb{N}^{\mathrm{b}}\to\rho^{\mathrm{b}}\to\rho^{\mathrm{b}}$ with
$\mathrm{C}_{\mathbb{N}\to\rho\to\rho}(f)$, we have

$\mathrm{C}_{\rho}(\mathrm{rec}(a)(\lambda k.f(\lambda\alpha.k))(i))$

for all $i:\mathbb{N}$.

######  Proof 3.3.

By induction on $i$.

By applying (1) to (2), we get a proof of
$\mathrm{C}(\mathrm{rec}^{\mathrm{b}})$.

Another important fact is that the generic sequence also satisfies the
predicate $\mathrm{C}$.

######  Lemma 5.

We have

$\mathrm{C}_{\mathbb{N}\to\mathbb{N}}(\Omega).$

######  Proof 3.4.

Suppose a continuous $f:(\mathbb{N}\to\mathbb{N})\to\mathbb{N}$ is given. The
goal is to show that $\Omega(f)$ is also continuous. Let
$\alpha:\mathbb{N}\to\mathbb{N}$ be given. By the continuity of $f$, we have a
modulus $m$ of $f$ at the point $\alpha$. Take $n:\equiv\max(m,f\alpha+1)$.
Given $\beta:\mathbb{N}\to\mathbb{N}$ with $\alpha=_{n}\beta$, we have

$\begin{array}[]{lllll}\Omega(f)(\alpha)&=&\alpha(f\alpha)\\\
&=&\beta(f\alpha)&&(\alpha=_{n}\beta\text{ and }f\alpha<f\alpha+1\leq n)\\\
&=&\beta(f\beta)&&(f\alpha=f\beta\text{ by the continuity of $f$})\\\
&=&\Omega(f)(\beta)\end{array}$

and hence $\Omega(f)$ is continuous.

######  Theorem 6.

Every $\T$-definable function $f:(\mathbb{N}\to\mathbb{N})\to\mathbb{N}$ is
continuous.

######  Proof 3.5.

By Lemmas 4 and 5, we know $f^{\mathrm{b}}(\Omega)$ is continuous. Then $f$ is
also continuous, because $f$ and $f^{\mathrm{b}}(\Omega)$ are pointwise equal
by Theorem 3.

##  4\. Other notions of continuity

###  4.1. T-definable moduli of continuity

It is also well-known that any $\T$-definable function
$f:(\mathbb{N}\to\mathbb{N})\to\mathbb{N}$ has a $\T$-definable _modulus of
continuity_ [20, Theorem 2.7.8], that is, a function
$M:(\mathbb{N}\to\mathbb{N})\to\mathbb{N}$ such that

$\forall\alpha^{\mathbb{N}\to\mathbb{N}},\beta^{\mathbb{N}\to\mathbb{N}}\left(\alpha=_{M(\alpha)}\beta\to
f(\alpha)=f(\beta)\right).$

Here we present two ways to recover this fact.

The first approach was suggested by Ulrich Kohlenbach. During a
workshop111Workshop “Proofs and Computation”, July 2-6 2018, Hausdorff
Research Institute of Mathematics, Bonn, Germany. Website:
https://www.him.uni-bonn.de/application/types-sets-constructions/workshop-
proofs-and-computation/. in Bonn, he pointed out that our Theorem 6 can be
precisely formulated as

> for each closed term $f:(\mathbb{N}\to\mathbb{N})\to\mathbb{N}$ in $\T$,
> $\mathrm{HA}^{\omega}$ proves that $f$ is continuous

whose proof remains the same. From the $\mathrm{HA}^{\omega}$ proof of the
continuity of $f$, we can extract a closed term
$M:(\mathbb{N}\to\mathbb{N})\to\mathbb{N}$ in $\T$ and a proof in
$\mathrm{HA}^{\omega}$ that $M$ is a modulus of continuity of $f$, via the
modified realizability [11, §5].

We can also “manually” extract moduli of continuity by combining the
construction with the $\mathrm{b}$-translation similarly to the construction
of general-bar-recursion functionals in [13]. For this, we extend System $\T$
with product type $\sigma\times\tau$ (and a pairing function
$\langle\,\text{-}\,\mathord{;}\,\text{-}\,\rangle$ and projections), and then
adapt Definition 2 to the following: The type translation
$(\rho\mapsto\rho^{\mathbf{{b}}})$ becomes

$\begin{array}[]{rll}\mathbb{N}^{\mathbf{{b}}}&:\equiv&\left((\mathbb{N}\to\mathbb{N})\to\mathbb{N}\right)\times\left((\mathbb{N}\to\mathbb{N})\to\mathbb{N}\right)\\\\[2.0pt]
(\sigma\to\tau)^{\mathbf{{b}}}&:\equiv&\sigma^{\mathbf{{b}}}\to\tau^{\mathbf{{b}}}.\end{array}$

For simplicity, we omit the trivial translation of product types and related
constants. Note that each term $w$ of type $\mathbb{N}^{\mathbf{{b}}}$ denotes
a pair of functionals. We write

  * •

$\mathrm{V}_{w}:(\mathbb{N}\to\mathbb{N})\to\mathbb{N}$ for the first
component of $w$, and

  * •

$\mathrm{M}_{w}:(\mathbb{N}\to\mathbb{N})\to\mathbb{N}$ for the second,

and hence have $w=\langle\mathrm{V}_{w};\mathrm{M}_{w}\rangle$. The idea is
that $\mathrm{V}_{w}$ is the _value_ (i.e. the $\mathrm{b}$-translation) of
some term while $\mathrm{M}_{w}$ is a _modulus of continuity_ of
$\mathrm{V}_{w}$. Because function types are translated in the same way as in
Definition 2, we need to change the term translation $(t\mapsto
t^{\mathbf{{b}}})$ only for the constants of $\mathbb{N}$:

$\begin{array}[]{rll}0^{\mathbf{{b}}}&:\equiv&\langle\lambda\alpha.0;\lambda\alpha.0\rangle\\\\[2.0pt]
\mathrm{succ}^{\mathbf{{b}}}&:\equiv&\lambda
x.\langle\lambda\alpha.\mathrm{succ}(\mathrm{V}_{x}(\alpha));\mathrm{M}_{x}\rangle\\\\[2.0pt]
\mathrm{rec}^{\mathbf{{b}}}&:\equiv&\lambda
af.\mathbf{ke}(\mathrm{rec}(a)(\lambda
k.f\langle\lambda\alpha.k;\lambda\alpha.0\rangle))\end{array}$

where the Kleisli extension
$\mathbf{ke}_{\rho}:(\mathbb{N}\to\rho^{\mathbf{{b}}})\to\mathbb{N}^{\mathbf{{b}}}\to\rho^{\mathbf{{b}}}$
is defined by

$\begin{array}[]{rll}\mathbf{ke}_{\mathbb{N}}(g)(f)&:\equiv&\langle\lambda\alpha.\mathrm{V}_{g(\mathrm{V}_{f}(\alpha))}(\alpha);\lambda\alpha.\max(\mathrm{M}_{g(\mathrm{V}_{f}(\alpha))}(\alpha),\mathrm{M}_{f}(\alpha))\rangle\\\\[2.0pt]
\mathbf{ke}_{\sigma\to\tau}(g)(f)&:\equiv&\lambda x.\mathbf{ke}_{\tau}(\lambda
k.g(k)(x))(f).\end{array}$

Note that the maximum function $\max:\mathbb{N}\times\mathbb{N}\to\mathbb{N}$
is primitive recursive and can be defined using $\mathrm{rec}$ in $\T$. The
“value” part of the above translation is exactly the $\mathrm{b}$-translation.
In the “modulus” part of the Kleisli extension
$\mathbf{ke}_{\mathbb{N}}(g)(f)$, there are two potential moduli of continuity
at $\alpha$: one is given by $g(\mathrm{V}_{f}(\alpha))$ and the other by $f$.
We of course take the greater one to be the modulus of continuity.

The generic sequence
$\mathbf{\Omega}:\mathbb{N}^{\mathbf{{b}}}\to\mathbb{N}^{\mathbf{{b}}}$ is
defined by

$\mathbf{\Omega}(f)\ :\equiv\
\langle\lambda\alpha.\alpha(\mathrm{V}_{f}(\alpha));\lambda\alpha.\max(\mathrm{M}_{f}(\alpha),\mathrm{V}_{f}(\alpha)+1)\rangle.$

For the “modulus” part, we again take the greater of the two potential moduli
of continuity: one is given by the input $f$, and the other is
$\mathrm{V}_{f}(\alpha)+1$ because $\alpha$ is applied to
$\mathrm{V}_{f}(\alpha)$.

We can show the following variant of Theorem 3

> any closed $f:(\mathbb{N}\to\mathbb{N})\to\mathbb{N}$ in $\T$ is pointwise
> equal to $\mathrm{V}_{f^{\mathbf{{b}}}(\mathbf{\Omega})}$

using a parametrized logical relation
$\mathbf{R}_{\rho}^{\alpha}\subseteq\rho^{\mathbf{{b}}}\times\rho$ that is
almost the same as Definition 2 except that the base case is defined by

$f\ \mathbf{R}_{\mathbb{N}}^{\alpha}\ n\ :\equiv\ \mathrm{V}_{f}(\alpha)=n.$

We also modify Definition 3 to get a predicate
$\mathbf{C}_{\rho}\subseteq\rho^{\mathbf{{b}}}$ with the following base case

$\mathbf{C}_{\mathbb{N}}(f)\ :\equiv\ \mathrm{M}_{f}\text{ is a modulus of
continuity of }\mathrm{V}_{f}.$

Similarly to the proof of Theorem 6, by showing (i)
$\mathbf{C}_{\rho}(t^{\mathbf{{b}}})$ for all $t:\rho$ in $\T$ and (ii)
$\mathbf{C}(\mathbf{\Omega})$, we can conclude that for any
$f:(\mathbb{N}\to\mathbb{N})\to\mathbb{N}$ in $\T$, the term
$\mathrm{M}_{f^{\mathbf{{b}}}(\mathbf{\Omega})}$ is a modulus of continuity of
$f$. Note that $\mathrm{M}_{f^{\mathbf{{b}}}(\mathbf{\Omega})}$ is exactly the
term which is extracted from the proof of Theorem 6 via modified
realizability.

######  Theorem 7.

If $f:(\mathbb{N}\to\mathbb{N})\to\mathbb{N}$ is $\T$-definable, then it has a
$\T$-definable modulus of continuity.

###  4.2. Uniform continuity

Because each $\T$-definable function
$f:(\mathbb{N}\to\mathbb{N})\to\mathbb{N}$ is continuous, so is its
restriction
$f|_{\mathbbm{2}^{\mathbb{N}}}:(\mathbb{N}\to\mathbbm{2})\to\mathbb{N}$. Using
our syntactic method, we can show that these restrictions are actually
uniformly continuous.

Recall that a function $f:(\mathbb{N}\to\mathbbm{2})\to\mathbb{N}$ is
_uniformly continuous_ if there exists $m:\mathbb{N}$, called a _modulus of
uniform continuity_ of $f$, such that any binary sequences
$\alpha,\beta:\mathbb{N}\to\mathbbm{2}$ that agree at the first $m$ positions
give the same result. The uniform continuity of $f$ can be formulated in
$\mathrm{HA}^{\omega}$ as

$\exists
m^{\mathbb{N}}\,\forall\alpha^{\mathbb{N}\to\mathbbm{2}},\beta^{\mathbb{N}\to\mathbbm{2}}\left(\alpha=_{m}\beta\to
f(\alpha)=f(\beta)\right).$

The following lemma of uniform continuity will play an important role in our
proof.

######  Lemma 8.

For any $m:\mathbb{N}$ and $f:(\mathbb{N}\to\mathbbm{2})\to\mathbb{N}$, if $m$
is a modulus of uniform continuity of $f$, then $f$ has a maximum image.

######  Proof 4.1.

By induction on $m$.

We sketch out our proof of uniform continuity only with the key steps. Firstly
we define a predicate $\mathrm{UC}_{\rho}\subseteq\rho^{\mathrm{b}}$ by

$\begin{array}[]{rll}\mathrm{UC}_{\mathbb{N}}(f)&:\equiv&\text{$f|_{\mathbbm{2}^{\mathbb{N}}}$
is uniformly continuous}\\\\[2.0pt]
\mathrm{UC}_{\sigma\to\tau}(g)&:\equiv&\forall
x^{\sigma^{\mathrm{b}}}\left(\mathrm{UC}_{\sigma}(x)\to\mathrm{UC}_{\tau}(g(x))\right).\end{array}$

Then we show

  * •

$\mathrm{UC}_{\rho}(t^{\mathrm{b}})$ for all $t:\rho$ in $\T$, assuming
$\mathrm{UC}(x^{\mathrm{b}})$ for all $x\in\mathrm{FV}(t)$; and

  * •

$\mathrm{UC}_{\mathbb{N}\to\mathbb{N}}(\Omega)$.

Both are proved using Lemma 8. They together lead to the desired result.

######  Theorem 9.

If $f:(\mathbb{N}\to\mathbb{N})\to\mathbb{N}$ is $\T$-definable, then its
restriction
$f|_{\mathbbm{2}^{\mathbb{N}}}:{(\mathbb{N}\to\mathbbm{2})\to\mathbb{N}}$ is
uniformly continuous.

Using the Dialectica interpretation and his pointwise version of strong
majorization, Kohlenbach [10] obtains a more general result: for each term
$f:(\mathbb{N}\to\mathbb{N})\to\mathbb{N}$ in $\T$, he constructs a term
$\Phi:(\mathbb{N}\to\mathbb{N})\to\mathbb{N}$ in $\T$ such that $\Phi(\gamma)$
is a modulus of uniform continuity of $f$ on
$\\{\alpha^{\mathbb{N}\to\mathbb{N}}\,|\,\forall
i^{\mathbb{N}}\,\alpha_{i}\leq\gamma_{i}\\}$. Our syntactic method can also
provide a construction of such moduli of uniform continuity (see our Agda
implementation [23]).

##  5\. Generalization

The key step of our syntactic approach to continuity is the
$\mathrm{b}$-translation: natural numbers are translated to functionals from
the Baire type $\mathbb{N}\to\mathbb{N}$ so that continuity becomes the base
case of the predicate to work with. The translation can be generalized by
replacing the Baire type by arbitrary finite type $X$. In specific, the type
translation $\rho\mapsto\rho^{X}$ is defined by

$\begin{array}[]{rll}\mathbb{N}^{X}&:\equiv&X\to\mathbb{N}\\\\[2.0pt]
(\sigma\to\tau)^{X}&:\equiv&\sigma^{X}\to\tau^{X}\end{array}$

while the term translation remains the same as in Definition 2 (with the
superscribed $\mathrm{b}$ replaced by $X$). The parametrized logical relation
$\mathrm{R}_{\rho}^{\alpha}\subseteq\rho^{X}\times\rho$ for the
“$X$-translation” is defined exactly the same as in Definition 2 except that
the parameter $\alpha$ is of type $X$ instead of $\mathbb{N}\to\mathbb{N}$,
and similarly Lemma 1 for it can be shown with the same proof. The generic
sequence $\Omega$ which in this case has type $X^{X}$ (i.e. the
$X$-translation of $X$) can be defined by unfolding $\Omega\
\mathrm{R}^{\alpha}\ \alpha$ when $X$ is given concretely. For instance, when
$X\equiv\mathbb{N}$ we define $\Omega:\mathbb{N}\to\mathbb{N}$ by
$\Omega(n):\equiv n$, as $\Omega\ \mathrm{R}^{n}\ n$ is unfolded to
$\Omega(n)=n$.

Therefore, our method can be generalized for proving various properties of
$\T$-definable functions of _arbitrary_ finite type: Suppose the goal is to
prove a certain property of $\T$-definable functions $X\to\mathbb{N}$. As
discussed above, we already have the “$X$-translation” of $\T$. Then we define
a predicate $P_{\rho}\subseteq\rho^{X}$ whose base case $P_{\mathbb{N}}(f)$
expresses the targeting property of $f:X\to\mathbb{N}$. Once we show
$P_{\rho}(t^{X})$ for all $t:\rho$ in $\T$, we achieve the goal. For instance,
when taking $X\equiv\mathbb{N}\to\mathbb{N}$ (or
$\mathbb{N}\to\mathbb{N}\to\mathbb{N}$), the above method is essentially Oliva
and Steila’s technique of proving the closure property of System $\T$ terms
under the rule of Spector’s bar recursion of type 0 (respectively 1) [13].
When taking $X\equiv\mathbb{N}$, we should be able to use the above method to
prove Schwichtenberg’s theorem that every $\T$-definable function
$\mathbb{N}\to\mathbb{N}$ is eventually bounded by the slow growing hierarchy
[17, Theorem 4.8] (but this is left as a future task). We have not found
applications when $X$ is higher than 1.

## Acknowledgment

This research was supported by the Alexander von Humboldt Foundation. A part
of this paper was written during the trimester “Types, Sets and Constructions”
at the Hausdorff Research Institute for Mathematics (HIM), University of Bonn,
May to August 2018. This visit was supported by HIM. Both this support and the
hospitality of HIM are gratefully acknowledged. The author is grateful to
Paulo Oliva and Martín Escardó for their motivations, and to Thierry Coquand,
Peter Dybjer, Fredrik Nordvall Forsberg, Ulrich Kohlenbach, Sam Sanders,
Helmut Schwichtenberg and the anonymous reviewers for various useful comments
and suggestions.

## References

  * [1] Agda Community.  The Agda Wiki.  Available at http://wiki.portal.chalmers.se/agda/pmwiki.php.
  * [2] Michael J. Beeson.  Foundations of Constructive Mathematics.  Springer, 1985.
  * [3] Thierry Coquand and Guilhem Jaber.  A note on forcing and type theory.  Fundamenta Informaticae, 100(1-4):43–52, 2010.
  * [4] Thierry Coquand and Guilhem Jaber.  A computational interpretation of forcing in type theory.  In Epistemology versus Ontology, volume 27, pages 203–213. Springer Netherlands, 2012.
  * [5] Martín Hötzel Escardó.  Continuity of Gödel’s system T functionals via effectful forcing.  MFPS’2013. Electronic Notes in Theoretical Computer Science, 298:119–141, 2013.
  * [6] Martín Hötzel Escardó and Chuangjie Xu.  A constructive manifestation of the Kleene–Kreisel continuous functionals.  Annals of Pure and Applied Logic, 167(9):770–793, 2016.  Fourth Workshop on Formal Topology (4WFTop).
  * [7] Michael P. Fourman.  Notions of choice sequence.  In A.S. Troelstra and D. van Dalen, editors, The L. E. J. Brouwer Centenary Symposium, volume 110 of Studies in Logic and the Foundations of Mathematics, pages 91–105. Elsevier, 1982.
  * [8] Michael P. Fourman.  Continuous truth I, non-constructive objects.  In G. Lolli, G. Longo, and A. Marcja, editors, Logic Colloquium ’82, volume 112 of Studies in Logic and the Foundations of Mathematics, pages 161–180. Elsevier, 1984.
  * [9] Michael P. Fourman.  Continuous truth II: reflections.  In L. Libkin, U. Kohlenbach, and R. de Queiroz, editors, Logic, Language, Information, and Computation (WoLLIC 2013), volume 8071 of Lecture Notes in Computer Science, pages 153–167. Springer Berlin Heidelberg, 2013.
  * [10] Ulrich Kohlenbach.  Pointwise hereditary majorization and some applications.  Archive for Mathematical Logic, 31(4):227–241, 1992.
  * [11] Ulrich Kohlenbach.  Applied Proof Theory: Proof Interpretations and Their Use in Mathematics.  Springer-Verlag Berlin Heidelberg, 2008.
  * [12] John Longley.  When is a functional program not a functional program?  In Proceedings of the Fourth ACM SIGPLAN International Conference on Functional Programming (ICFP ’99), pages 1–7. ACM, 1999.
  * [13] Paulo Oliva and Silvia Steila.  A direct proof of Schwichtenberg’s bar recursion closure theorem.  The Journal of Symbolic Logic, 83(1):70–83, 2018.
  * [14] Thomas Powell.  A functional interpretation with state.  Accepted for Proceedings of Logic in Computer Science (LICS 2018), 2018\.
  * [15] Vincent Rahli and Mark Bickford.  Validating Brouwer’s continuity principle for numbers using named exceptions.  Mathematical Structures in Computer Science, 28(6):942–990, 2018\.
  * [16] Helmut Schwichtenberg.  On bar recursion of types 0 and 1.  The Journal of Symbolic Logic, 44(3):325–329, 1979.
  * [17] Helmut Schwichtenberg.  Proofs as programs.  In P. Aczel, H. Simmons, and S. Wainer, editors, Proof Theory: A selection of papers from the Leeds Proof Theory Programme 1990, pages 79–114. Cambridge University Press, 1993.
  * [18] Helmut Schwichtenberg and Stanley S. Wainer.  Proofs and Computations.  Cambridge University Press, 2012.
  * [19] Richard Statman.  Logical relations and the typed lambda calculus.  Information and Control, 65:85–97, 1985.
  * [20] Anne Sjerp Troelstra.  Models and computability.  In A. S. Troelstra, editor, Metamathematical Investigation of Intuitionistic Arithmetic and Analysis, volume 344 of Lecture Notes in Mathematics, pages 97–174. Springer Berlin Heidelberg, 1973.
  * [21] Gerrit van der Hoeven and Ieke Moerdijk.  Sheaf models for choice sequences.  Annals of Pure and Applied Logic, 27(1):63–107, 1984.
  * [22] Chuangjie Xu.  A continuous computational interpretation of type theories.  PhD thesis, School of Computer Science, University of Birmingham, 2015\.
  * [23] Chuangjie Xu.  A Gentzen-style monadic translation of Gödel’s System T.  Agda development available at http://cj-xu.github.io/agda/ModTrans/index.html, August 2019.
  * [24] Chuangjie Xu.  An agda implementation of Oliva & Steila’s “A direct proof of Schwichtenberg’s bar recursion closure theorem”.  Available at http://cj-xu.github.io/agda/BRCT/BRCT.html, March 2018\.
  * [25] Chuangjie Xu.  A syntactic approach to continuity of Gödel’s system T definable functionals.  Agda development available at http://cj-xu.github.io/agda/TCont/index.html, September 2018.
  * [26] Chuangjie Xu and Martín Hötzel Escardó.  A constructive model of uniform continuity.  In Typed Lambda Calculi and Applications, volume 7941 of Lecture Notes in Computer Science, pages 236–249. Springer Berlin Heidelberg, 2013.