A syntactic approach to continuity of T-definable functionals

TL;DR

This paper presents a new syntactic proof that all functions definable in G"odel's System T are continuous, using a translation into itself and formalization in Agda to compute moduli of continuity.

Contribution

It introduces a novel syntactic translation and a continuity predicate, providing a formalized, executable proof of continuity for T-definable functions.

Findings

Proof formalized in Agda

Able to compute moduli of continuity

New syntactic approach to continuity

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\"odel'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.

Equations

$$\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}$$

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

$$\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}$$

$$\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}$$

$$\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}$$

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

$$\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}$$

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

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

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

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

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

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

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

$$\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)$$

$$\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}$$

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

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

$$\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}$$

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

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

$$\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}$$

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

$$\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}$$

$$\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}$$

$$\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}$$

$$\mathbf{\Omega }(f):\equiv ⟨\lambda \alpha .\alpha ({\mathrm{V}}_f(\alpha ));\lambda \alpha .\max ({\mathrm{M}}_f(\alpha ),{\mathrm{V}}_f(\alpha )+1)⟩.$$

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

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

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

Full text

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.

[TABLE]

(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

[TABLE]

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}$.

{defi}

[$\mathrm{b}$-translation]

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

[TABLE]

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:

[TABLE]

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

[TABLE]

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

[TABLE]

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]. {defi}

For any $\alpha:\mathbb{N}\to\mathbb{N}$, we define a logical relation $\mathrm{R}_{\rho}^{\alpha}\subseteq\rho^{\mathrm{b}}\times\rho$ by

[TABLE]

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

[TABLE]

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.

[TABLE]

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$,

[TABLE]

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

[TABLE]

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

[TABLE]

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

[TABLE]

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$,

[TABLE]

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

[TABLE]

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.

{defi}

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

[TABLE]

Lemma 4**.**

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

[TABLE]

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.

[TABLE]

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

[TABLE]

(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

[TABLE]

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

[TABLE]

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

[TABLE]

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

[TABLE]

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

[TABLE]

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}$:

[TABLE]

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

[TABLE]

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

[TABLE]

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

[TABLE]

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

[TABLE]

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

[TABLE]

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

[TABLE]

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

[TABLE]

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.