A Gentzen-style monadic translation of G\"odel's System T

TL;DR

This paper presents a syntactic translation of G"odel's System T using a monadic framework, revealing key properties of T-definable functionals, and formalized in Agda.

Contribution

It introduces a Gentzen-style monadic translation of System T and proves a fundamental logical relation theorem, connecting to classical logic translations.

Findings

Reveals properties like majorizability, continuity, and bar recursion of T-definable functionals.

Formalized the translation and proofs in Agda proof assistant.

Abstract

We introduce a syntactic translation of Goedel's System T parametrized by a weak notion of a monad, and prove a corresponding fundamental theorem of logical relation. Our translation structurally corresponds to Gentzen's negative translation of classical logic. By instantiating the monad and the logical relation, we reveal the well-known properties and structures of T-definable functionals including majorizability, continuity and bar recursion. Our development has been formalized in the Agda proof assistant.

Equations

$$A\to jA(A\to jB)\to jA\to jB(jA)[t/x]\leftrightarrow j(A[t/x]).$$

$$(A\to B{)}_j^{\mathrm{G}}$$

$$(A\wedge B{)}_j^{\mathrm{G}}$$

$$(\forall xA{)}_j^{\mathrm{G}}$$

$$\sigma ,\tau$$

$$t,u$$

$$\max :={\mathsf{rec}}_{\mathbb{N}\to \mathbb{N}}(\lambda n^{\mathbb{N}}.n,\lambda n^{\mathbb{N}}{f}^{\mathbb{N}\to \mathbb{N}}.{\mathsf{rec}}_{\mathbb{N}}(\mathsf{suc}n,\lambda m^{\mathbb{N}}{g}^{\mathbb{N}\to \mathbb{N}}.\mathsf{suc}(fm))).$$

$$\max (0,n)=n\max (m,0)=m\max (\mathsf{suc}m,\mathsf{suc}n)=\mathsf{suc}(\max (m,n))$$

$${\mathsf{rec}}_{\sigma }(a,f,0)=a{\mathsf{rec}}_{\sigma }(a,f,\mathsf{suc}n)=f(n,{\mathsf{rec}}_{\sigma }(a,f,n))$$

$$\eta :\mathbb{N}\to \mathsf{J}\mathbb{N}\kappa :(\mathbb{N}\to \mathsf{J}\mathbb{N})\to \mathsf{J}\mathbb{N}\to \mathsf{J}\mathbb{N}$$

$${\mathbb{N}}^{\mathsf{J}}$$

$$(\sigma \to \tau {)}^{\mathsf{J}}$$

$$(x{)}^{\mathsf{J}}$$

$$(\lambda x.t{)}^{\mathsf{J}}$$

$$(tu{)}^{\mathsf{J}}$$

$${\mathrm{ke}}_{\mathbb{N}}$$

$${\mathrm{ke}}_{\sigma \to \tau }$$

$$({\mathsf{rec}}_{\sigma }{)}^{\mathsf{J}}(x,f,0^{\mathsf{J}})=x({\mathsf{rec}}_{\sigma }{)}^{\mathsf{J}}(x,f,(\mathsf{suc}n{)}^{\mathsf{J}})=f(n^{\mathsf{J}},({\mathsf{rec}}_{\sigma }{)}^{\mathsf{J}}(x,f,n^{\mathsf{J}})).$$

$$f{\mathrm{R}}_{\sigma \to \tau }g:=\forall x^{\sigma }{a}^{{\sigma }^{\mathsf{J}}}\left(x{\mathrm{R}}_{\sigma }a\to fx{\mathrm{R}}_{\tau }ga\right).$$

$$\forall n^{\mathbb{N}}\left(n{\mathrm{R}}_{\mathbb{N}}\eta n\right)\text{and}\forall f^{\mathbb{N}\to \mathbb{N}}{g}^{\mathbb{N}\to \mathsf{J}\mathbb{N}}\left(\forall n^{\mathbb{N}}\left(fn{\mathrm{R}}_{\mathbb{N}}gn\right)\to f{\mathrm{R}}_{\mathbb{N}\to \mathbb{N}}\kappa g\right)$$

$$\forall f^{\mathbb{N}\to \sigma }{g}^{\mathbb{N}\to {\sigma }^{\mathsf{J}}}\left(\forall n^{\mathbb{N}}\left(fn{\mathrm{R}}_{\sigma }gn\right)\to f{\mathrm{R}}_{\mathbb{N}\to \sigma }{\mathrm{ke}}_{\sigma }(g)\right).$$

$$\forall n^{\mathbb{N}}\left({\mathsf{rec}}_{\sigma }(x,f,n){\mathrm{R}}_{\sigma }{\mathsf{rec}}_{{\sigma }^{\mathsf{J}}}(y,g\circ \eta ,n)\right).$$

$$n{◃}_{\mathbb{N}}m$$

$$f{◃}_{\sigma \to \tau }g$$

$$\eta (n):=n\begin{array}{rl}\kappa (g,0)& :=g(0)\\ \kappa (g,n+1)& :=\max \left(\kappa (g,n),g(n+1)\right).\end{array}$$

$$\eta (n):=\lambda x.n\kappa (g,f):=\lambda x.g(fx,x).$$

$$n{\mathrm{R}}_{\mathbb{N}}^{x}f$$

$$g{\mathrm{R}}_{\sigma \to \tau }^{x}h$$

$$\forall {\Omega }^{X^{\mathsf{J}}}\left(x{\mathrm{R}}_X^x\Omega \to fx=f^{\mathsf{J}}(\Omega ,x)\right).$$

$$Q_{\mathbb{N}}(f)$$

$$Q_{\sigma \to \tau }(h)$$

$$\forall n^{\mathbb{N}}{Q}_{\mathbb{N}}(\eta n)\text{and}\forall g^{\mathbb{N}\to X\to \mathbb{N}}\left(\forall n^{\mathbb{N}}{Q}_{\mathbb{N}}(gn)\to Q_{\mathbb{N}\to \mathbb{N}}(\kappa g)\right)$$

$$\mathsf{pair}:\sigma \to \tau \to \sigma \times \tau {\mathsf{pr}}_1:\sigma \times \tau \to \sigma {\mathsf{pr}}_2:\sigma \times \tau \to \tau$$

$${\mathrm{ke}}_{\sigma \times \tau }:=\lambda g^{\mathbb{N}\to {\sigma }^{\mathsf{J}}\times {\tau }^{\mathsf{J}}}{a}^{\mathsf{J}\mathbb{N}}.\mathsf{pair}\left({\mathrm{ke}}_{\sigma }({\mathsf{pr}}_1\circ g,a),{\mathrm{ke}}_{\tau }({\mathsf{pr}}_2\circ g,a)\right)$$

$$u{\mathrm{R}}_{\sigma \times \tau }v:=\left({\mathsf{pr}}_{1}u{\mathrm{R}}_{\sigma }{\mathsf{pr}}_{1}v\right)\wedge \left({\mathsf{pr}}_{2}u{\mathrm{R}}_{\tau }{\mathsf{pr}}_{2}v\right).$$

Full text

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

Chuangjie Xu

1 Introduction

Via a syntactic translation of Gödel’s System $\mathsf{T}$, Oliva and Steila [17] construct functionals of bar recursion whose terminating functional is given by a closed term in System $\mathsf{T}$. The author adapts their method to compute moduli of (uniform) continuity of functions $(\mathbb{N}\to\mathbb{N})\to\mathbb{N}$ that are definable in System $\mathsf{T}$ [27]. Inspired by the generalizations of negative translations which replace double negation by an arbitrary nucleus [8, 12, 25], we introduce a monadic translation of System $\mathsf{T}$ into itself which unifies those in [17, 27]. This monadic translation structurally corresponds to Gentzen’s negative translation.

Our translation is parametrized by a monad-like structure, which we call a nucleus, but without the restriction of satisfying the monad laws. We adopt the standard technique of logical relations to show the soundness of the translation in the sense that each term of $\mathsf{T}$ is related to its translation. Because the translation is parametrized by a nucleus, we have to assume that the logical relation holds for the nucleus. Such a soundness theorem is an instance of the fundamental theorem of logical relation [21] stating that if a logical relation holds for all constants then so does it for all terms.

Monadic translations have been widely used for assigning semantics to impure languages. Our goal is instead to reveal properties enjoyed by terms of $\mathsf{T}$ and to extract witnesses of these properties. For this purpose, the nuclei we work with are not extensions of $\mathsf{T}$, but just simple structures given by types and terms of $\mathsf{T}$, so that the translation remains in $\mathsf{T}$ and the extracted witnesses are terms of $\mathsf{T}$. The Gentzen-style translation looks simpler than the other variants [19, 24]. But we demonstrate its power and elegance via its various applications including majorizability, (uniform) continuity and bar recursion. Of course these properties of $\mathsf{T}$-definable functionals are well known [5, 7, 11, 13, 17, 19, 27]. The main contribution of the paper, however, is in obtaining these results in a single framework simply by choosing a suitable nucleus that satisfies the logical relation for the target property.

All the results in the paper are formalized in the Agda proof assistant [2], except the introductory section on negative translations of predicate logic. There are some differences in the Agda development. Firstly, it works with de Bruijn indices when representing the syntax of $\mathsf{T}$ to avoid handling variable names. Moreover, all the logical relations are defined between the Agda (or type-theoretic) interpretations of $\mathsf{T}$-types. What we have proved in Agda is that the interpretation of any $\mathsf{T}$-term is related to the one of its translation. In this way, we avoid dealing with the computation rules of $\mathsf{T}$ because they all hold judgmentally in the Agda interpretation. The Agda development is available at the author’s GitHub page to which the link is given above the introduction.

1.1 Proof-theoretic translations

Recall that Gentzen’s translation111Nowadays it is known as the Gödel-Gentzen negative translation. Gödel’s translation places a double negation also in front of the clause for implication, which makes it different from Gentzen’s one in affine logic [3]. simply places a double negation in front of atomic formulas, disjunctions and existential quantifiers [22]. One can replace double negation with a nucleus, that is, an endofunction $j$ on formulas such that for any formulas $A,B$ the following statements are provable:

[TABLE]

Nuclei are also known as lax modalities [1] and strong monad [8]. But in this paper we adopt the terminology and definition from [25] which brought the technical motivation to this work. Each nucleus determines a proof-theoretic translation of intuitionistic predicate logic $\mathrm{IQL}$ into itself, consisting of a formula translation $A\mapsto A^{\mathrm{G}}_{j}$ defined as follows

[TABLE]

and a soundness theorem stating that $\mathrm{IQL}\vdash A$ implies $\mathrm{IQL}\vdash A^{\mathrm{G}}_{j}$. Working with different nuclei, one embed a logic system into another:

• •

if $jA=(A\to\bot)\to\bot$, then $\mathrm{CQL}\vdash A$ implies $\mathrm{MQL}\vdash A^{\mathrm{G}}_{j}$;

• •

if $jA=(A\to R)\to R$ for some predicate variable $R$, then $\mathrm{CQL}\vdash A$ implies $\mathrm{IQL}\vdash A^{\mathrm{G}}_{j}$;

• •

if $jA=A\vee\bot$, then $\mathrm{IQL}\vdash A$ implies $\mathrm{MQL}\vdash A^{\mathrm{G}}_{j}$;

where $\mathrm{CQL}$ stands for classical predicate logic and $\mathrm{MQL}$ for minimal predicate logic. These results are well-known (see e.g. [12, 25]) and various instances of the translation have been applied in term extraction (see e.g. [8, 14])

Under the viewpoint of the proofs-as-programs correspondence, our translation of Gödel’s System $\mathsf{T}$ presented in Section 2 is exactly a term/program version of the above proof-theoretic translation on minimal propositional logic.

1.2 Gödel’s System T

Recall that the term language of Gödel’s System $\mathsf{T}$ can be given by the following grammar

[TABLE]

where $\mathbb{N}$ is the base type of natural numbers and $\sigma\to\tau$ the type of functions from $\sigma$ to $\tau$. A typing judgment takes the form $\Gamma\vdash t:\tau$, where $\Gamma$ is a context (i.e. a list of distinct typed variables $x:\sigma$), $t$ is a term and $\tau$ is a type. Here are the typing rules:

$\Gamma,x:\sigma\vdash x:\sigma$     

$\Gamma,x:\sigma\vdash t:\tau$

$\Gamma\vdash\lambda x^{\sigma}.t:\sigma\to\tau$

  

$\Gamma\vdash t:\sigma\to\tau$         $\Gamma\vdash u:\sigma$

$\Gamma\vdash tu:\tau$

$\Gamma\vdash 0:\mathbb{N}$        $\Gamma\vdash\mathsf{suc}:\mathbb{N}\to\mathbb{N}$        $\Gamma\vdash\mathsf{rec}_{\sigma}:\sigma\to(\mathbb{N}\to\sigma\to\sigma)\to\mathbb{N}\to\sigma$

We call $\Gamma\vdash t:\tau$ a well-typed term if it is derivable. We may omit the context $\Gamma$ and simply write $t:\tau$ or $t^{\tau}$ if it is unambiguous. When mentioning terms of $\mathsf{T}$ in the paper, we refer to only the well-typed ones. We often omit superscript and subscript types if they can be easily inferred, and may write:

• •

$\lambda x_{1}x_{2}\cdots x_{n}.t$ instead of $\lambda x_{1}.\lambda x_{2}.\cdots\lambda x_{n}.t$,

• •

$f(a_{1},a_{2},\cdots,a_{n})$ instead of $(((fa_{1})a_{2})\cdots)a_{n}$,

• •

$n+1$ instead of $\mathsf{suc}\,n$,

• •

$\tau^{\sigma}$ instead of $\sigma\to\tau$, and

• •

$f\circ g$ instead of $\lambda x.f(gx)$.

Using the primitive recursor, we can for instance define the function $\max:\mathbb{N}\to\mathbb{N}\to\mathbb{N}$ that returns the greater argument as follows:

[TABLE]

One can easily verify that the usual defining equations of $\max$

[TABLE]

hold using the computation rules of $\mathsf{rec}$

[TABLE]

where $a:\sigma$ and $f:\mathbb{N}\to\sigma\to\sigma$. For the ease of understanding, we will use defining equations rather than $\mathsf{T}$-terms involving $\mathsf{rec}$ in the paper.

2 A monadic translation of System T

Our syntactic translation of System $\mathsf{T}$ is parametrized by a nucleus, that is, a monad-like structure without the restriction of satisfying the monad laws.

Definition 2.1** (nuclei).**

A nucleus relative to $\mathsf{T}$ is a triple $(\mathsf{J}\mathbb{N},\eta,\kappa)$ consisting of a type $\mathsf{J}\mathbb{N}$ and two terms

[TABLE]

of System $\mathsf{T}$.

Note that a nucleus is not an extension of $\mathsf{T}$, but instead a simple structure given by a type and two terms of $\mathsf{T}$. Therefore, our translation of any term of $\mathsf{T}$ remains in $\mathsf{T}$ rather than some monadic metatheory such as in [19, 24]. The simplest example is the identity nucleus where $\mathsf{J}\mathbb{N}$ is just $\mathbb{N}$ and $\eta,\kappa$ are the identity functions of suitable types. More examples are available in Section 3. Though the first component of a nucleus is just a type, we denote it as $\mathsf{J}\mathbb{N}$ because in the generalized notion of a nucleus discussed in Section 4 it will be a map $\mathsf{J}$ on all the types of $\mathsf{T}$.

We are now ready to construct a syntactic translation of $\mathsf{T}$ into itself:

Definition 2.2** ($\mathsf{J}$-translation).**

Given a nucleus $(\mathsf{J}\mathbb{N},\eta,\kappa)$, we assign to each type $\rho$ of $\mathsf{T}$ a type $\rho^{\mathsf{J}}$ as follows:

[TABLE]

Each term $\Gamma\vdash t:\rho$ is translated to a term $\Gamma^{\mathsf{J}}\vdash t^{\mathsf{J}}:\rho^{\mathsf{J}}$, where $\Gamma^{\mathsf{J}}$ is a new context assigning each $x:\sigma\in\Gamma$ to a fresh variable $x^{\mathsf{J}}:\sigma^{\mathsf{J}}$, and $t^{\mathsf{J}}$ is translated inductively as follows:

[TABLE]

where $\mathrm{ke}_{\sigma}:(\mathbb{N}\to\sigma^{\mathsf{J}})\to\mathsf{J}\mathbb{N}\to\sigma^{\mathsf{J}}$ is an extension of $\kappa$ defined inductively on $\sigma$:

[TABLE]

We often write $\mathsf{J}$ to denote the nucleus $(\mathsf{J}\mathbb{N},\eta,\kappa)$ and call the above the $\mathsf{J}$-translation of $\mathsf{T}$.

Thanks to the inductive translation of function types into function types, the translation of the simply-typed-$\lambda$-calculus fragment of $\mathsf{T}$ is straightforward. There is no need of introducing a nonstandard, monadic notion of function application which plays an essential role in the other monadic translations [19, 24] as discussed in Section 4.

The more interesting part is the translation of the constants. Viewing $\eta$ as a unit operator and $\kappa$ as a bind operator in a monad $\mathsf{J}$ on $\mathbb{N}$ may reveal some intuition behind the translation of [math] and $\mathsf{suc}$: It is natural to expect ${\underline{n}}^{\mathsf{J}}=\eta\underline{n}$ for each numeral $\underline{n}\coloneqq\mathsf{suc}^{n}(0)$. This is indeed the case if the monad laws are satisfied, because $\kappa(\eta\circ-):(\mathbb{N}\to\mathbb{N})\to\mathsf{J}\mathbb{N}\to\mathsf{J}\mathbb{N}$ which is used to translate $\mathsf{suc}$ recovers exactly the ‘functoriality’ of $\mathsf{J}$. It is also natural to expect $(\mathsf{rec}_{\sigma})^{\mathsf{J}}$ to preserve the computation rules, i.e.

[TABLE]

A promising candidate of such $(\mathsf{rec}_{\sigma})^{\mathsf{J}}(x,f):\mathsf{J}\mathbb{N}\to\sigma^{\mathsf{J}}$ is $\mathsf{rec}_{\sigma^{\mathsf{J}}}(x,f\circ\eta):\mathbb{N}\to\sigma^{\mathsf{J}}$. Hence, we extend $\kappa$ to $\mathrm{ke}_{\sigma}:(\mathbb{N}\to\sigma^{\mathsf{J}})\to\mathsf{J}\mathbb{N}\to\sigma^{\mathsf{J}}$ to complete the translation of $\mathsf{rec}_{\sigma}$.

We adopt the standard technique of logical relations to show that the above translation is sound in the sense that each term of $\mathsf{T}$ is related to its translation222We owe the idea of proving a unified theorem of logical relation to Thomas Powell.. Because the translation is parametrized by a nucleus, we have to assume that the logical relation holds for the nucleus.

Theorem 2.3** (Fundamental Theorem of Logical Relation).**

Let $(\mathsf{J}\mathbb{N},\eta,\kappa)$ be a nucleus. Given a binary relation ${\mathrel{\mathrm{R}_{\mathbb{N}}}}\subseteq\mathbb{N}\times\mathsf{J}\mathbb{N}$ between terms of $\mathsf{T}$, we extend it to ${\mathrel{\mathrm{R}_{\rho}}}\subseteq\rho\times\rho^{\mathsf{J}}$ for arbitrary type $\rho$ of $\mathsf{T}$ by defining

[TABLE]

If ${\mathrel{\mathrm{R}_{\mathbb{N}}}}$ satisfies

[TABLE]

then $t\mathrel{\mathrm{R}_{\rho}}t^{\mathsf{J}}$ for any closed term $t:\rho$ of $\mathsf{T}$.

Proof 2.4**.**

We prove a more general statement that

for any term $\Gamma\vdash t:\rho$ of $\mathsf{T}$, if $\Gamma\mathrel{\mathrm{R}}\Gamma^{\mathsf{J}}$ then $t\mathrel{\mathrm{R}_{\rho}}t^{\mathsf{J}}$

where $(x_{1}:\sigma_{1},\ldots,x_{n}:\sigma_{n})\mathrel{\mathrm{R}}(x_{1}^{\mathsf{J}}:\sigma_{1}^{\mathsf{J}},\ldots,x_{n}^{\mathsf{J}}:\sigma_{n}^{\mathsf{J}})$ stands for $x_{1}\mathrel{\mathrm{R}_{\sigma_{1}}}x_{1}^{\mathsf{J}}\wedge\ldots\wedge x_{n}\mathrel{\mathrm{R}_{\sigma_{n}}}x_{n}^{\mathsf{J}}$, by structural induction over $t$.

• •

$t=x$. By the assumption $\Gamma\mathrel{\mathrm{R}}\Gamma^{\mathsf{J}}$.

• •

$t=\lambda x.u$. Assume $\Gamma\mathrel{\mathrm{R}}\Gamma^{\mathsf{J}}$ and $x\mathrel{\mathrm{R}_{\sigma}}x^{\mathsf{J}}$. We have $u\mathrel{\mathrm{R}}u^{\mathsf{J}}$ by induction hypothesis.

• •

$t=uv$. By induction hypothesis we have $u\mathrel{\mathrm{R}_{\sigma\to\tau}}u^{\mathsf{J}}$ and $v\mathrel{\mathrm{R}_{\sigma}}v^{\mathsf{J}}$. Then, by the definition of $\mathrel{\mathrm{R}_{\sigma\to\tau}}$, we have $uv\mathrel{\mathrm{R}_{\tau}}u^{\mathsf{J}}v^{\mathsf{J}}$.

• •

$t=0$. By the assumption (2.3) of $\eta$.

• •

$t=\mathsf{suc}$. By the assumption (2.3) of $\eta$, we have $\mathsf{suc}(n)\mathrel{\mathrm{R}_{\mathbb{N}}}\eta(\mathsf{suc}(n))$ for all $n:\mathbb{N}$. Then by the assumption (2.3) of $\kappa$, we have $\mathsf{suc}\mathrel{\mathrm{R}_{\mathbb{N}}}\kappa(\eta\circ\mathsf{suc})$.

• •

$t=\mathsf{rec}$. We prove $\mathsf{rec}\mathrel{\mathrm{R}}\mathsf{rec}^{\mathsf{J}}$ with the following claims:

For any type $\sigma$ of $\mathsf{T}$, the term $\mathrm{ke}_{\sigma}$ preserves the logical relation in the following sense:

[TABLE]

Proof.* By induction on $\sigma$. ∎* 2. 2.

For any $x^{\sigma}$ and $y^{\sigma^{\mathsf{J}}}$ with $x\mathrel{\mathrm{R}}y$, and any $f^{\mathbb{N}\to\sigma\to\sigma}$ and $g^{\mathsf{J}\mathbb{N}\to\sigma^{\mathsf{J}}\to\sigma^{\mathsf{J}}}$ with $f\mathrel{\mathrm{R}}g$,

[TABLE]

Proof.* By induction on $n$. ∎*

We get a proof of $\mathsf{rec}\mathrel{\mathrm{R}}\mathsf{rec}^{\mathsf{J}}$ simply by applying (1) to (2).

Remark 2.5**.**

The above proof can be carried out in the intuitionistic Heyting arithmetic in finite types $\mathsf{HA}^{\omega}$ [23], with the theorem formulated as

if $\mathsf{HA}^{\omega}$ proves (2.3) then, for each closed term $t$ of $\mathsf{T}$, $\mathsf{HA}^{\omega}$ proves $t\mathrel{\mathrm{R}}t^{\mathsf{J}}$.

So are all the results in Section 3. Hence, the verification system here can be $\mathsf{HA}^{\omega}$. We leave it unspecified in the theorem for several reasons. Firstly, we hope to study other properties whose verification may require a stronger system as in [19]. Moreover, what we have proved in the Agda formalization is a version of the theorem for the Agda embedding of System $\mathsf{T}$, namely that the Agda interpretations of any $\mathsf{T}$-term and its translation are related. But that is only an implementation choice as explained in the introduction.

3 Applications of the monadic translation

We now apply the above framework to reveal various properties and structures of $\mathsf{T}$-definable functions including majorizability, (uniform) continuity and bar recursion. Each example consists of an algorithm to construct the desired structure given by the monadic translation, and a correctness proof of the algorithm given by the fundamental theorem of logical relation. For this, one only needs to choose a suitable nucleus that satisfies the logical relation for the target property.

3.1 Majorizability

Our first application is to recover Howard’s majorizability proof of System $\mathsf{T}$ [11]. Majorizability plays an important role in models of higher-order calculi and more recently in the proof mining program [14]. Howard’s majorizability relation extends the usual ordering $\leq$ on natural numbers to the one $\mathrel{\triangleleft_{\rho}}$ on functionals of arbitrary finite type $\rho$ in the same way as in Theorem 2.3. Specifically $\mathrel{\triangleleft_{\rho}}$ is defined inductively on $\rho$ as follows:

[TABLE]

We say $t$ is majorized by $u$ if $t\mathrel{\triangleleft}u$, and call $u$ a majorant of $t$. Howard shows that each closed term of T is majorized by some closed term of T, which fits perfectly into our framework: Let us take $\mathsf{J}\mathbb{N}=\mathbb{N}$ and define $\eta:\mathbb{N}\to\mathbb{N}$ and $\kappa:(\mathbb{N}\to\mathbb{N})\to\mathbb{N}\to\mathbb{N}$ by

[TABLE]

The $\max$ function can be defined in $\mathsf{T}$ using $\mathsf{rec}$ as shown in Section 1.2, and thus so is $\kappa$. Intuitively $\kappa(g,n)$ is the maximum of the values $g0,g1,\ldots,gn$. Therefore, it satisfies the following property:

Lemma 3.1**.**

For any $g:\mathbb{N}\to\mathbb{N}$, we have $gm\leq\kappa(g,n)$ whenever $m\leq n$.

Proof 3.2**.**

By induction on $n$. If $n=0$, we are done because $m$ has to be [math]. If $m\leq n+1$, we have two cases: (i) If $m=n+1$, then $g(n+1)\leq\kappa(g,n+1)$ by definition. (ii) If $m\leq n$, then $g(m)\leq\kappa(g,n)\leq\kappa(g,n+1)$ by induction hypothesis and definition.

Corollary 3.3**.**

Each closed term $t:\rho$ of $\mathsf{T}$ is majorized by its translation $t^{\mathsf{J}}$.

Proof 3.4**.**

We only need to check that the two conditions (2.3) are fulfilled. The first one holds because the ordering $\leq$ is reflexive. For the second, let us assume $\forall n\left(fn\leq gn\right)$ and $n\leq m$. We have $gn\leq\kappa(g,m)$ by Lemma 3.1, and thus $fn\leq\kappa(g,m)$ by the transitivity of $\leq$.

We draw the reader’s attention to this simple example also because the nucleus defined above does not satisfy the monad laws: Here $\eta$ is the identity function on $\mathbb{N}$. If the left-identity law $\kappa(f,\eta x)=fx$ holds, then $\kappa$ has to be the identity function on $\mathbb{N}^{\mathbb{N}}$, which is not the case.

3.2 Lifting to higher-order functionals

In the previous example, we extend a relation on natural numbers to arbitrary finite types and then show that the resulting logical relation holds for all terms of $\mathsf{T}$. However, if one wants to prove a certain property $P$ of functions $X\to\mathbb{N}$, the above syntactic method may not work directly, because the property $P$ may not be captured by the inductively defined logical relation. Our monadic translation can serve a preliminary step to solve the problem by lifting natural numbers to functions $X\to\mathbb{N}$ so that the desired property $P$ becomes the base case of the logical relation.

Let $X$ be a type of $\mathsf{T}$. Consider the nucleus $(\mathsf{J}\mathbb{N},\eta,\kappa)$ with $\mathsf{J}\mathbb{N}=X\to\mathbb{N}$ and $\eta:\mathbb{N}\to\mathsf{J}\mathbb{N}$ and $\kappa:(\mathbb{N}\to\mathsf{J}\mathbb{N})\to\mathsf{J}\mathbb{N}\to\mathsf{J}\mathbb{N}$ defined by

[TABLE]

Clearly $\eta$ maps a natural number $n$ to a constant function with value $n$. The intuition of $\kappa(g,f):X\to\mathbb{N}$ is the following: Given an input $x$, we have an index $fx$ to get a function $g(fx)$ from the sequence $g$. Then we apply it to the input $x$ to get the final value.

Given $x:X$, we define a logical relation ${\mathrel{\mathrm{R}^{x}_{\rho}}}\subseteq\rho\times\rho^{\mathsf{J}}$ inductively as in Theorem 2.3:

[TABLE]

Clearly the conditions (2.3) hold; thus by Theorem 2.3 we have $t\mathrel{\mathrm{R}^{x}_{\rho}}t^{\mathsf{J}}$ for any closed term $t$ of $\mathsf{T}$. In particular, for any closed term $f:X\to\mathbb{N}$ of $\mathsf{T}$, we have

[TABLE]

For some type $X$ of $\mathsf{T}$, we may be able to construct a closed term $\Omega:X^{\mathsf{J}}$ such that $x\mathrel{\mathrm{R}^{x}_{X}}\Omega$ for all $x:X$, by unfolding the statement $x\mathrel{\mathrm{R}^{x}_{X}}\Omega$. For example, if $X=\mathbb{N}^{\mathbb{N}}$, then $x\mathrel{\mathrm{R}^{x}_{X}}\Omega$ is unfolded to $\forall n^{\mathbb{N}},f^{\mathbb{N}^{\mathbb{N}}\to\mathbb{N}}\left(n=fx\to xn=\Omega(f,x)\right)$; we thus define $\Omega(f,x)\coloneqq x(fx)$ as $fx=n$ by assumption and then have $x\mathrel{\mathrm{R}^{x}_{X}}\Omega$ by definition. Once we construct such a term $\Omega:X^{\mathsf{J}}$, we have $f=f^{\mathsf{J}}\Omega$ (up to pointwise equality). The term $\Omega:X^{\mathsf{J}}$ which preserves the logical relation in the sense of $x\mathrel{\mathrm{R}^{x}_{X}}\Omega$ for all $x:X$ is known as a generic element [6, 7].

Given a property $P$ of functions $X\to\mathbb{N}$, we define a predicate $Q_{\rho}\subseteq\rho^{\mathsf{J}}$ on elements of the translated type $\rho^{\mathsf{J}}$ inductively on $\rho$:

[TABLE]

Note that $Q$ is just an instance of the binary relation defined in Theorem 2.3. Once we prove the conditions (2.3) for $Q$, i.e.

[TABLE]

we have $Q(t^{\mathsf{J}})$ for any closed term $t$ of $\mathsf{T}$. If we prove also $Q_{X}(\Omega)$, then we have $P(f)$ for all closed terms $f:\mathbb{N}\to X$ of $\mathsf{T}$ because $Q_{\mathbb{N}}(f^{\mathsf{J}}\Omega)$ and $f=f^{\mathsf{J}}\Omega$.

All the remaining examples are about properties of $\mathsf{T}$-definable functions $\mathbb{N}^{\mathbb{N}}\to\mathbb{N}$ which can be proved following the above steps. We instead enrich the ‘lifting’ nucleus to reflect the computational content of the properties so that witnesses of the properties can be obtained as terms of $\mathsf{T}$ directly via the translation.

3.3 Continuity

The next applications of our monadic translation are to recover the well-known results that every $\mathsf{T}$-definable function $\mathbb{N}^{\mathbb{N}}\to\mathbb{N}$ is pointwise continuous and its restriction to any compact subspace is uniformly continuous [5].

There are various approaches to continuity: Kohlenbach [13] extracts a term from the extensionality proof via the Dialectica interpretation, and then uses the majorant of this term to construct a modulus of uniform continuity. Coquand and Jaber [6] extend type theory with a new constant for a generic element, decorate the operational semantics with forcing information, and then extract continuity information of a functional by applying it to the generic element. Escardó [7] also employs a generic element to compute continuity but in his model of dialogue trees, which is closely related to our syntactic approach as discussed in Remark 3.7. There are also various sheaf models [9, 10, 26] in which all functionals from the Baire space  $\mathbb{N}^{\mathbb{N}}$ are continuous and those from the Cantor space $\mathbf{2}^{\mathbb{N}}$ are uniformly continuous. Powell [19] introduces a monadic translation for some call-by-value functional languages, one of whose instantiations tackles also continuity of $\mathsf{T}$-definable functionals. His method corresponds to Kuroda’s negative translation as discussed in Section 4.3.

We enrich the ‘lifting’ nucleus (Section 3.2) so that moduli of (uniform) continuity are obtained directly from the translation. For the sake of convenience, we extend System $\mathsf{T}$ with products. Such extension can be avoided by working with sequences of types and terms as in the literature of functional interpretations such as [15].

3.3.1 Translating products

We extend System $\mathsf{T}$ with product type $\sigma\times\tau$ and constants

[TABLE]

satisfying the usual computation rules. Similarly to Gentzen’s translation of conjunction, we translate product type component-wise, i.e. $(\sigma\times\tau)^{\mathsf{J}}\coloneqq\sigma^{\mathsf{J}}\times\tau^{\mathsf{J}}$. Then the above constants are translated into themselves but of the translated types, e.g. $\mathsf{pr}_{1}^{\mathsf{J}}\coloneqq\mathsf{pr}_{1}:\sigma^{\mathsf{J}}\times\tau^{\mathsf{J}}\to\sigma^{\mathsf{J}}$. Recall that the primitive recursor is translated using $\mathrm{ke}_{\sigma}:(\mathbb{N}\to\sigma^{\mathsf{J}})\to\mathsf{J}\mathbb{N}\to\sigma^{\mathsf{J}}$ which is defined inductively on $\sigma$. So we have to add the following case

[TABLE]

into the definition of $\mathrm{ke}$ in order to complete the translation. For the fundamental theorem of logical relation, when extending a relation ${\mathrel{\mathrm{R}_{\mathbb{N}}}}\subseteq\mathbb{N}\times\mathsf{J}\mathbb{N}$ to ${\mathrel{\mathrm{R}_{\rho}}}\subseteq\rho\times\rho^{\mathsf{J}}$, we add the following case for product type

[TABLE]

and can easily show that the constants of product types are related to their translations. We often write $\left\langle a,\,b\right\rangle$ instead of $\mathsf{pair}(a,b)$ for the sake of readability.

3.3.2 Pointwise continuity

Recall that a function $M:\mathbb{N}^{\mathbb{N}}\to\mathbb{N}$ is a modulus of continuity of $f:\mathbb{N}^{\mathbb{N}}\to\mathbb{N}$ if

[TABLE]

where $\alpha=_{m}\beta$ stands for $\forall i\mathord{<}m\left(\alpha i=\beta i\right)$. Our goal is to find a suitable nucleus $\mathsf{J}$ so that we can obtain such a functional $M$ from the $\mathsf{J}$-translation of $f$ and then verify its correctness using the fundamental theorem of logical relation.

Let $\mathsf{J}\mathbb{N}=(\mathbb{N}^{\mathbb{N}}\to\mathbb{N})\times(\mathbb{N}^{\mathbb{N}}\to\mathbb{N})$. For $w:\mathsf{J}\mathbb{N}$ we write $\mathrm{V}_{w}$ to denote its first component and $\mathrm{M}_{w}$ the second, due to the intuition that $\mathrm{M}_{w}$ is a modulus of continuity of the value component $\mathrm{V}_{w}$. Then we define $\eta:\mathbb{N}\to\mathsf{J}\mathbb{N}$ by

[TABLE]

and $\kappa:(\mathbb{N}\to\mathsf{J}\mathbb{N})\to\mathsf{J}\mathbb{N}\to\mathsf{J}\mathbb{N}$ by

[TABLE]

Note that the ‘value’ components form a ‘lifting’ nucleus in the sense of Section 3.2 so that natural numbers are lifted to functions $\mathbb{N}^{\mathbb{N}}\to\mathbb{N}$. And the ‘modulus’ components will allow the translation to equip a continuity structure to the values. Reasonably $\eta(n)$ equips the constantly zero function as a modulus of continuity to the constant function $\lambda\alpha.n$ since its input is never accessed. As to $\kappa(g,w)$, its value at a point $\alpha$ has two possible moduli: one given by $g(\mathrm{V}_{w}(\alpha))$ and the other by $w$; thus the greater one is a modulus of continuity at $\alpha$.

We work with a logical relation ${\mathrel{\mathrm{R}^{\alpha}_{\rho}}}\subseteq\rho\times\rho^{\mathsf{J}}$ which is parametrized by $\alpha:\mathbb{N}^{\mathbb{N}}$. Specifically, its base case ${\mathrel{\mathrm{R}^{\alpha}_{\mathbb{N}}}}\subseteq\mathbb{N}\times\mathsf{J}\mathbb{N}$ is defined by

[TABLE]

The first component of $n\mathrel{\mathrm{R}^{\alpha}_{\mathbb{N}}}w$ states that the value of $w$ at $\alpha$ is $n$, while the second explains exactly the intuition of the type $\mathsf{J}\mathbb{N}$, namely that $\mathrm{M}_{w}(\alpha)$ is a modulus of continuity of $\mathrm{V}_{w}$ at $\alpha$. We leave the proof of (2.3) to the reader. By Theorem 2.3, we have $t\mathrel{\mathrm{R}^{\alpha}_{\rho}}t^{\mathsf{J}}$ for any $\alpha:\mathbb{N}^{\mathbb{N}}$ and for any closed term $t:\rho$ of $\mathsf{T}$. In particular, we have $f\mathrel{\mathrm{R}^{\alpha}_{\mathbb{N}^{\mathbb{N}}\to\mathbb{N}}}f^{\mathsf{J}}$ for every closed term $f:\mathbb{N}^{\mathbb{N}}\to\mathbb{N}$ of $\mathsf{T}$.

The last step is to construct the generic element $\Omega:\mathsf{J}\mathbb{N}\to\mathsf{J}\mathbb{N}$ such that $\alpha\mathrel{\mathrm{R}^{\alpha}_{\mathbb{N}^{\mathbb{N}}}}\Omega$ for all $\alpha:\mathbb{N}^{\mathbb{N}}$. Once we unfold $\alpha\mathrel{\mathrm{R}^{\alpha}_{\mathbb{N}^{\mathbb{N}}}}\Omega$, we can see that, for any $w:\mathsf{J}\mathbb{N}$, the value of $\Omega(w)$ has to be $\lambda\alpha.\alpha(\mathrm{V}_{w}(\alpha))$ as discussed in Section 3.2. Then we also need to construct its modulus of continuity. There are two possible moduli at $\alpha$: one is $\mathrm{V}_{w}(\alpha)+1$ because the modulus of continuity of $\lambda\alpha.\alpha n$ at $\alpha$ is $n+1$, and the other is $\mathrm{M}_{w}(\alpha)$. We just take the greater one and then end up with the following definition:

[TABLE]

One may have noticed that the above is highly similar to the definition of $\kappa$. Indeed, we have $\Omega=\kappa(\lambda n.\left\langle\lambda\alpha.\alpha n,\,\lambda\alpha.n+1\right\rangle)$.

Theorem 3.5**.**

Every closed term $f:\mathbb{N}^{\mathbb{N}}\to\mathbb{N}$ of $\mathsf{T}$ has a modulus of continuity given by the term $\mathrm{M}_{f^{\mathsf{J}}(\Omega)}$.

Proof 3.6**.**

Because $f\mathrel{\mathrm{R}^{\alpha}_{\mathbb{N}^{\mathbb{N}}\to\mathbb{N}}}f^{\mathsf{J}}$ and $\alpha\mathrel{\mathrm{R}^{\alpha}_{\mathbb{N}^{\mathbb{N}}}}\Omega$, we have $f\alpha\mathrel{\mathrm{R}^{\alpha}_{\mathbb{N}}}f^{\mathsf{J}}(\Omega)$ for any $\alpha:\mathbb{N}^{\mathbb{N}}$, which implies (i) $f=\mathrm{V}_{f^{\mathsf{J}}(\Omega)}$ up to pointwise equality, and (ii) $\mathrm{M}_{f^{\mathsf{J}}(\Omega)}$ is a modulus of continuity of $\mathrm{V}_{f^{\mathsf{J}}(\Omega)}$. Therefore, $\mathrm{M}_{f^{\mathsf{J}}(\Omega)}$ is also a modulus of continuity of $f$.

Remark 3.7**.**

The above development can be viewed as a syntactic (and simplified) version of Escardó’s approach via dialogue trees [7]. The algorithms to construct moduli of continuity in these two methods are exactly the same. On the other hand, though Powell works also with a monadic translation [19], his algorithm is different because he translates terms in the call-by-value manner. We will look into this in more detail in Section 4.3.

3.3.3 Uniform continuity

The objective here is to, for each closed term $f:\mathbb{N}^{\mathbb{N}}\to\mathbb{N}$ of $\mathsf{T}$, construct a modulus of uniform continuity $M:\mathbb{N}^{\mathbb{N}}\to\mathbb{N}$, i.e.

[TABLE]

where $\alpha\leq^{1}\beta$ stands for $\forall i(\alpha i\leq\beta i)$. The value $M\delta$ is called a modulus of uniform continuity of $f$ on $\{\alpha:\mathbb{N}^{\mathbb{N}}\mid\alpha\leq^{1}\delta\}$. The following fact of uniform continuity plays an important role in the construction:

Lemma 3.8**.**

If $f:\mathbb{N}^{\mathbb{N}}\to\mathbb{N}$ is uniformly continuous on $\{\alpha:\mathbb{N}^{\mathbb{N}}\mid\alpha\leq^{1}\delta\}$ with a modulus $m$, then it has a maximum image on $\{\alpha:\mathbb{N}^{\mathbb{N}}\mid\alpha\leq^{1}\delta\}$.

Proof 3.9**.**

We compute the maximum image $\Theta(m,f,\delta)$ by induction on the modulus $m$:

[TABLE]

where $i*\alpha$ is an infinite sequence with head $i$ and tail $\alpha$, and $\Phi:\mathbb{N}^{\mathbb{N}}\to\mathbb{N}\to\mathbb{N}$ defined by

[TABLE]

i.e.* $\Phi(\alpha,n)$ is the greatest $\alpha i$ for $i\leq n$ (note that $\Phi$ is the $\kappa$ of the ‘majorizability’ nucleus introduced in Section 3.1). In the base case of $\Theta$, the modulus is 0 and thus $f$ is constant with the value $f\delta$. To compute $\Theta(m+1,f,\delta)$, by induction hypothesis we have for each $i:\mathbb{N}$ the maximum image $\Theta\left(m,\lambda\alpha.f(i*\alpha),\delta\circ\mathsf{suc}\right))$ of the function $\lambda\alpha.f(i*\alpha)$ with a modulus $m$ on the inputs bounded by $\delta\circ\mathsf{suc}$. Because the inputs of $f$ are bounded by $\delta$, the greatest $\Theta\left(m,\lambda\alpha.f(i*\alpha),\delta\circ\mathsf{suc}\right))$ for $i<\delta 0$ is the maximum image of $f$, and we use $\Phi$ to find it. Note that both $\Phi$ and $\Theta$ can be defined in $\mathsf{T}$ using $\mathsf{rec}$.*

We are now ready to construct the nucleus. Let $\mathsf{J}\mathbb{N}=(\mathbb{N}^{\mathbb{N}}\to\mathbb{N})\times(\mathbb{N}^{\mathbb{N}}\to\mathbb{N})$. The ieda is exactly the same as in the previous treatment to pointwise continuity: For any $w:\mathsf{J}\mathbb{N}$, its second component $\mathrm{M}_{w}$ is (expected to be) a modulus of uniform continuity of the first component $\mathrm{V}_{w}$. Then we define $\eta:\mathbb{N}\to\mathsf{J}\mathbb{N}$ by

[TABLE]

and $\kappa:(\mathbb{N}\to\mathsf{J}\mathbb{N})\to\mathsf{J}\mathbb{N}\to\mathsf{J}\mathbb{N}$ by

[TABLE]

where $\Phi$ and $\Theta$ are defined in the proof of Lemma 3.8. Specifically, we construct a modulus of uniform continuity for the value of $\kappa(g,w)$ as follows: Given $\delta:\mathbb{N}^{\mathbb{N}}$, we have two possible moduli given by those of $g$ and $w$ at $\delta$ and thus we choose the larger one. Actually the only complication comes from the calculation of the modulus given by $g$. For each $i:\mathbb{N}$ we have a modulus $\mathrm{M}_{gi}(\delta)$. In the value of $\kappa(g,w)$, we apply $g$ to $\mathrm{V}_{w}(\alpha)$ for input $\alpha$. Because $\mathrm{V}_{w}$ has a maximum image computed using $\Theta$, we only need to find the greatest modulus $\mathrm{M}_{gi}(\delta)$ for $i$ not greater than the maximum image of $\mathrm{V}_{w}$, and we use $\Phi$ for this purpose.

Given $\delta:\mathbb{N}^{\mathbb{N}}$, the base case ${\mathrel{\mathrm{R}^{\delta}_{\mathbb{N}}}}\subseteq\mathbb{N}\times\mathsf{J}\mathbb{N}$ of the logical relation is defined by

[TABLE]

In words, $n\mathrel{\mathrm{R}^{\delta}_{\mathbb{N}}}w$ means that $n$ is the value of $w$ at $\delta$ and that $\mathrm{M}_{w}(\delta)$ is a modulus of uniform continuity of $\mathrm{V}_{w}$ on $\{\alpha:\mathbb{N}^{\mathbb{N}}\mid\alpha\leq^{1}\delta\}$. It is routine to check that both $\eta$ and $\kappa$ preserve the logical relation in the sense of (2.3), which we again leave to the reader. By Theorem 2.3 we have $t\mathrel{\mathrm{R}^{\delta}_{\rho}}t^{\mathsf{J}}$ for any $\delta:\mathbb{N}^{\mathbb{N}}$ and for any closed term $t:\rho$ of $\mathsf{T}$. Moreover, the generic element $\Omega:\mathsf{J}\mathbb{N}\to\mathsf{J}\mathbb{N}$ defined by

[TABLE]

also preserves the logical relation in the sense of $\delta\mathrel{\mathrm{R}^{\delta}_{\mathbb{N}^{\mathbb{N}}}}\Omega$ for all $\delta:\mathbb{N}^{\mathbb{N}}$.

With a proof similar to the one of Theorem 3.5, we get the following result:

Theorem 3.10**.**

Every closed term $f:\mathbb{N}^{\mathbb{N}}\to\mathbb{N}$ of $\mathsf{T}$ has a modulus of uniform continuity given by the term $\mathrm{M}_{f^{\mathsf{J}}(\Omega)}$.

3.4 General bar recursion

To prove Schwichtenberg’s theorem [20] that the System $\mathsf{T}$ definable functionals are closed under a rule-like version Spector’s bar recursion of type levels 0 and 1, Oliva and Steila [17] introduce a notion of general bar recursion whose termination condition is given by decidable monotone predicates on finite sequences. As the last example, we recover their construction of general-bar-recursion functionals ([17, Definitions 3.1 & 3.3]) via an instantiation of our translation. For this, we need the following notations:

• •

We represent decidable predicates as functions $\mathbb{N}^{*}\to\mathbf{2}$, where $\mathbb{N}^{*}$ is the type of finite sequences of natural numbers and $\mathbf{2}=\{0,1\}$ is the type of booleans.

• •

For any $S:\mathbb{N}^{*}\to\mathbf{2}$ and $s:\mathbb{N}^{*}$, we write $S(s)$ instead of $S(s)=1$.

• •

For any $s:\mathbb{N}^{*}$, we write $|s|:\mathbb{N}$ to denote its length and $\hat{s}:\mathbb{N}^{\mathbb{N}}$ the extension of $s$ with infinitely many [math]’s.

• •

For any $s:\mathbb{N}^{*}$ and $n:\mathbb{N}$, we write $s*n:\mathbb{N}^{*}$ to denote appending $n$ to $s$.

• •

For any $s:\mathbb{N}^{*}$ and $\alpha:\mathbb{N}^{\mathbb{N}}$, we write $s*\alpha:\mathbb{N}^{\mathbb{N}}$ to denote their concatenation.

Note that the treatment of $\mathbb{N}^{*}$ and $\mathbf{2}$ is not essential. For instance, we can represent a finite sequence $s$ by a pair $\left\langle\alpha,\,n\right\rangle$ and consider $s$ as the prefix of the infinite sequence $\alpha$ of length $n$ as in our Agda implementation. All the above operations on sequences are definable in $\mathsf{T}$. We also need the following definitions:

• •

We call $\xi:(\mathbb{N}^{*}\to\sigma)\to(\mathbb{N}^{*}\to\sigma^{\mathbb{N}}\to\sigma)\to\mathbb{N}^{*}\to\sigma$ a functional of general bar recursion for $S:\mathbb{N}^{*}\to\mathbf{2}$ if $\mathcal{GBR}_{S}(\xi)$ holds where $\mathcal{GBR}_{S}(\xi)$ is defined by

[TABLE]

• •

A predicate $S$ is monotone if $S(s)$ implies $S(s*n)$ for all $s:\mathbb{N}^{*}$ and $n:\mathbb{N}$.

• •

For $Y:\mathbb{N}^{\mathbb{N}}\to\mathbb{N}$, we say $S$ secures $Y$ if

[TABLE]

Let $Y:\mathbb{N}^{\mathbb{N}}\to\mathbb{N}$ be a closed term of $\mathsf{T}$. Oliva and Steila show (i) for any $S$ securing $Y$, from a functional of general bar recursion for $S$ we can construct a functional of Spector’s bar recursion for $Y$ [17, Theorem 2.4], and (ii) we can construct a monotone predicate $S$ that secures $Y$ and a functional of general bar recursion for $S$ [17, Theorem 3.4]. In this way, they give a new proof of Schwichtenberg’s bar recursion closure theorem with an explicit construction of Spector’s bar-recursion functionals.

We firstly construct a nucleus for general bar recursion. Fix a type $\sigma$ of $\mathsf{T}$. Let $\mathsf{J}\mathbb{N}=(\mathbb{N}^{\mathbb{N}}\to\mathbb{N})\times(\mathbb{N}^{*}\to\mathbf{2})\times((\mathbb{N}^{*}\to\sigma)\to(\mathbb{N}^{*}\to\sigma^{\mathbb{N}}\to\sigma)\hskip 1.0pt\mathord{\to}\hskip 1.0pt\mathbb{N}^{*}\to\sigma)$. Given $w:\mathsf{J}\mathbb{N}$, we write $\mathrm{V}_{w},\mathrm{S}_{w},\mathrm{B}_{w}$ to denote its three components. The intuition is that $\mathrm{S}_{w}$ is a monotone predicate securing $\mathrm{V}_{w}$ and $\mathrm{B}_{w}$ is a functional of general bar recursion for $\mathrm{S}_{w}$. We define $\eta:\mathbb{N}\to\mathsf{J}\mathbb{N}$ by

[TABLE]

and $\kappa:(\mathbb{N}\to\mathsf{J}\mathbb{N})\to\mathsf{J}\mathbb{N}\to\mathsf{J}\mathbb{N}$ by

[TABLE]

where $\min:\mathbb{N}\to\mathbb{N}\to\mathbb{N}$ returns the smaller argument. Lastly, we define the generic element $\Omega:\mathsf{J}\mathbb{N}\to\mathsf{J}\mathbb{N}$ by

[TABLE]

where $\mathrm{Le}:\mathbb{N}\to\mathbb{N}\to\mathbf{2}$ has value $1$ iff its first argument is strictly smaller than the second, and $\Psi n:(\mathbb{N}^{*}\to\sigma)\to(\mathbb{N}^{*}\to\sigma^{\mathbb{N}}\to\sigma)\to\mathbb{N}^{*}\to\sigma$ is a $\mathsf{T}$-definable functional of bar recursion for the constant function $Y=\lambda\alpha.n$ [17, Lemma 2.1], i.e.

[TABLE]

For any $n:\mathbb{N}$, it is clear that $\lambda s.\mathrm{Le}(n,|s|)$ is a monotone predicate that secures $\lambda\alpha.\alpha n$, and that $\Psi n$ is a functional of general bar recursion for $\lambda s.\mathrm{Le}(n,|s|)$.

Theorem 3.11**.**

For any closed term $Y:\mathbb{N}^{\mathbb{N}}\to\mathbb{N}$ of $\mathsf{T}$,

$\mathrm{S}_{Y^{\mathsf{J}}\Omega}$* is a monotone predicate securing $Y$, and* 2. 2.

$\mathrm{B}_{Y^{\mathsf{J}}\Omega}$* is a functional of general bar recursion of $\mathrm{S}_{Y^{\mathsf{J}}\Omega}$.*

Proof 3.12**.**

Given $\alpha:\mathbb{N}^{\mathbb{N}}$, we define the base case ${\mathrel{\mathrm{R}^{\alpha}_{\mathbb{N}}}}\subseteq\mathbb{N}\times\mathsf{J}\mathbb{N}$ of the logical relation by

[TABLE]

To apply the fundamental theorem of logical relation, we need to check the conditions (2.3):

• •

It is trivial to prove $n\mathrel{\mathrm{R}^{\alpha}_{\mathbb{N}}}\eta n$ for all $n:\mathbb{N}$.

• •

As to $\kappa$, given $f:\mathbb{N}\to\mathbb{N}$ and $g:\mathbb{N}\to\mathsf{J}\mathbb{N}$ such that $fi\mathrel{\mathrm{R}^{\alpha}_{\mathbb{N}}}gi$ for all $i:\mathbb{N}$, our goal is to prove $f\mathrel{\mathrm{R}^{\alpha}_{\mathbb{N}\to\mathbb{N}}}\kappa g$. Let $n:\mathbb{N}$ and $w:\mathsf{J}\mathbb{N}$ with $n\mathrel{\mathrm{R}^{\alpha}_{\mathbb{N}}}w$ be given.

• –

We have $fn=\mathrm{V}_{gn}(\alpha)=\mathrm{V}_{g(\mathrm{V}_{w}(\alpha))}(\alpha)=\mathrm{V}_{\kappa(g,w)}(\alpha)$ as in the previous examples.

• –

Because $S_{w}$ is monotone and so is $\mathrm{S}_{gi}$ for all $i:\mathbb{N}$ by assumption, the predicate $\mathrm{S}_{\kappa(g,w)}$ is also monotone.

• –

If $\mathrm{S}_{\kappa(g,w)}(s)$, then $\mathrm{S}_{w}(s)$ and $\mathrm{S}_{g(\mathrm{V}_{w}\hat{s})}(s)$ by definition. Given $\alpha:\mathbb{N}^{\mathbb{N}}$, we have $\mathrm{V}_{w}(s*\alpha)=\mathrm{V}_{w}(\hat{s})$ because $\mathrm{S}_{w}$ secures $\mathrm{V}_{w}$. Then we have $\mathrm{V}_{\kappa(g,w)}(s*\alpha)=\mathrm{V}_{g(\mathrm{V}_{w}(s*\alpha))}(s*\alpha)=\mathrm{V}_{g(\mathrm{V}_{w}(\hat{s}))}(s*\alpha)=\mathrm{V}_{g(\mathrm{V}_{w}(\hat{s}))}(\hat{s})=\mathrm{V}_{\kappa(g,w)}(\hat{s})$ because $\mathrm{S}_{g(\mathrm{V}_{w}\hat{s})}$ secures $\mathrm{V}_{g(\mathrm{V}_{w}\hat{s})}$. Hence $\mathrm{S}_{\kappa(g,w)}$ secures $\mathrm{V}_{\kappa(g,w)}$.

• –

Lastly we show that $\mathrm{B}_{\kappa(g,w)}$ is a functional of general bar recursion for $\mathrm{S}_{\kappa(g,w)}$. Let $G:{\mathbb{N}^{*}\to\sigma}$, $H:{\mathbb{N}^{*}\to\sigma^{\mathbb{N}}\to\sigma}$ and $s:{\mathbb{N}^{*}}$ be given. (1) If $\mathrm{S}_{\kappa(g,w)}(s)$, then $\mathrm{S}_{w}(s)$ and $\mathrm{S}_{g(\mathrm{V}_{w}\hat{s})}(s)$, and thus we have $\mathrm{B}_{\kappa(g,w)}(G,H,s)=G(s)$. (2) If $\neg\mathrm{S}_{\kappa(g,w)}(s)$, then we have two cases to check: (2.1) If $\mathrm{S}_{w}(s)$, then $\neg\mathrm{S}_{g(\mathrm{V}_{w}\hat{s})}(s)$ by definition. It is not hard to show $\mathrm{B}_{\kappa(g,w)}(G,H,s)=H(s,\lambda n.\mathrm{B}_{\kappa(g,w)}(G,H,s*n))$. (2.2) If $\neg(\mathrm{S}_{w}(s))$, then we always have $\mathrm{B}_{\kappa(g,w)}(G,H,s)=H(s,\lambda n.\mathrm{B}_{\kappa(g,w)}(G,H,s*n))$ no matter if $\mathrm{S}_{g(\mathrm{V}_{w}\hat{s})}(s)$ holds or not.

Hence, we have $fn\mathrel{\mathrm{R}^{\alpha}_{\mathbb{N}}}\kappa(g,w)$.

Given a closed term $Y:\mathbb{N}^{\mathbb{N}}\to\mathbb{N}$ of $\mathsf{T}$, for any $\alpha:\mathbb{N}^{\mathbb{N}}$ we have $Y\mathrel{\mathrm{R}^{\alpha}_{\mathbb{N}^{\mathbb{N}}\to\mathbb{N}}}Y^{\mathsf{J}}$ by Theorem 2.3. For any $n:\mathbb{N}$, we have $n\mathrel{\mathrm{R}^{\alpha}_{\mathbb{N}}}\left\langle\lambda\alpha.\alpha n,\,\lambda s.\mathrm{Le}(n,|s|),\,\Psi n\right\rangle$ by definition; thus, $\alpha\mathrel{\mathrm{R}^{\alpha}_{\mathbb{N}\to\mathbb{N}}}\Omega$ holds by (2.3) for $\kappa$ which we have just proved. Hence we have $Y\alpha\mathrel{\mathrm{R}^{\alpha}_{\mathbb{N}}}Y^{\mathsf{J}}\Omega$ for any $\alpha:\mathbb{N}^{\mathbb{N}}$. From this, we get (i) $Y=\mathrm{V}_{Y^{\mathsf{J}}\Omega}$ up to pointwise equality, (ii) $\mathrm{S}_{Y^{\mathsf{J}}\Omega}$ is a monotone predicate securing $\mathrm{V}_{Y^{\mathsf{J}}\Omega}$ and thus also $Y$, and (iii) $\mathrm{B}_{Y^{\mathsf{J}}\Omega}$ is a functional of general bar recursion for $\mathrm{S}_{Y^{\mathsf{J}}\Omega}$.

The above development is just a restructuring of the work of Oliva and Steila [17] that fits into our framework. But there are some small differences (or simplifications):

• •

[17] requires the predicate $S$ to satisfy the bar condition $\forall\alpha^{\mathbb{N}^{\mathbb{N}}}\exists n^{\mathbb{N}}S(\bar{\alpha}n)$, where $\bar{\alpha}n:\mathbb{N}^{*}$ is the prefix of $\alpha$ of length $n$. As pointed out by Makoto Fujiwara in a personal discussion, this condition is not needed for the result. So we remove it in the above development.

• •

[17] assumes that the closed terms $Y:\mathbb{N}^{\mathbb{N}}\to\mathbb{N}$ are of the form $\lambda\alpha.t$ where $\alpha:\mathbb{N}^{\mathbb{N}}$ is the only free variable in $t:\mathbb{N}$, and treats $\alpha$ as a special constant (for the generic element). Motivated by a version of Escardó’s Agda development of [7], we avoid such extension by using the lifting nucleus that is introduced in Section 3.2.

• •

The syntactic translation of $\mathsf{T}$ in [17, Definitions 3.1 & 3.3] contains only the construction of general-bar-recursion functionals while the one of monotone securing predicates is given in the proof of the main theorem [17, Theorem 3.4]. We combine both in the translation in order to split the constructions from the correctness proof.

As pointed out by an anonymous reviewer, this section unifies the results in Section 3.3 in the sense that moduli of (uniform) continuity can be defined from monotone securing bars and general-bar-recursion functionals: Let $Y:\mathbb{N}^{\mathbb{N}}\to\mathbb{N}$ be a closed term of $\mathsf{T}$. The monotone predicate $\mathrm{S}_{Y^{\mathsf{J}}\Omega}$ is a bar, i.e. $\forall\alpha^{\mathbb{N}^{\mathbb{N}}}\exists n^{\mathbb{N}}\mathrm{S}_{Y^{\mathsf{J}}\Omega}(\bar{\alpha}n)$, as shown in [17, Theorem 3.4]. This together with the fact that it secures $Y$ implies the pointwise continuity of $Y$. The witness of the fact that $\mathrm{S}_{Y^{\mathsf{J}}\Omega}$ is a bar obtained via e.g. modified realizability [14] is a continuity modulus of $Y$. Our translation in Section 3.3 is just an explicit procedure to get these witnesses that are blurred in the proof of [17, Theorem 3.4]. On the other hand, the reviewer points out that we can construct a modulus $M:\mathbb{N}^{\mathbb{N}}\to\mathbb{N}$ of uniform continuity of $Y$ by

[TABLE]

where $G(s)\coloneqq 0$, $H^{\delta}(s,f)\coloneqq 1+\max\{fn\mid n\leq\delta(|s|)\}$ and $\mathsf{nil}:\mathbb{N}^{*}$ is the empty sequence. The idea is that if $s$ is a prefix of $\delta$ then $\mathrm{B}_{Y^{\mathsf{J}}\Omega}(G,H^{\delta},s)$ is a modulus of uniform continuity of the function $\lambda\alpha.Y(s*\alpha)$ on $\{\alpha:\mathbb{N}^{\mathbb{N}}\mid\alpha\leq^{1}\delta\}$: If $\mathrm{S}_{Y^{\mathsf{J}}\Omega}(s)$, we know $\lambda\alpha.Y(s*\alpha)$ is a constant function because $\mathrm{S}_{Y^{\mathsf{J}}\Omega}$ secures $Y$. Then $\mathrm{B}_{Y^{\mathsf{J}}\Omega}(G,H^{\delta},s)=G(s)=0$ is a proper modulus. If $\neg\mathrm{S}_{Y^{\mathsf{J}}\Omega}(s)$, then the step functional $H^{\delta}$ finds the greatest value of the moduli of $\lambda\alpha.Y(s*n*\alpha)$ given by $\mathrm{B}_{Y^{\mathsf{J}}\Omega}(G,H^{\delta},s*n)$ for $n\leq\delta(|s|)$ and then adds 1 to get a modulus of $\lambda\alpha.Y(s*\alpha)$.

4 Generalization and variants of the monadic translation

We have developed a self-translation of System $\mathsf{T}$ in the spirit of Gentzen’s negative translation. We conclude the paper by generalizing it to translate sums and comparing it with another two monadic translations.

4.1 Translating sums

We generalize our Gentzen-style translation to translate also sums. Let us extend $\mathsf{T}$ with sum type $\sigma+\tau$ and the following constants

[TABLE]

In his translation, Gentzen places a double negation in front of disjunctions (see Section 1.1). Following this inspiration, the sum type $\sigma+\tau$ should be translated into $\mathsf{J}(\sigma^{\mathsf{J}}+\tau^{\mathsf{J}})$. But the simple notion of a nucleus given by a type and two terms does not suffice. We have to work with the following more general notion: A nucleus $(\mathsf{J},\eta,\kappa)$ consists of an endofunction $\mathsf{J}$ on types of (the extension of) $\mathsf{T}$, and terms

[TABLE]

for any types $\sigma,\tau$ of (the extension of) $\mathsf{T}$. Then we add the following clauses to Definition 2.2 to complete the translation:

[TABLE]

Generalizing the fundamental theorem of logical relation to cover sums is remained as a future task. Both natural numbers and sums, as instances of inductive types, are translated in a very similar way. Another future task is to generalize the translation to cover all (strictly positive) inductive and coinductive types.

4.2 The Kolmogorov-style monadic translation

Barthe and Uustalu’s call-by-name continuation passing style transformation [4] corresponds to Kolmogorov’s negative translation. By replacing the continuation monad with a nucleus, one obtains a Kolmogorov-style monadic translation which is studied in [24]. Kolmogorov places a double negation in front of every subformula. Similarly we place the nucleus in front of every subtype. Hence we have to work with the more general notion of a nucleus $(\mathsf{J},\eta,\kappa)$ where $\mathsf{J}$ is an endofunction on types. Specifically, each type $\rho$ of $\mathsf{T}$ is translated to $\mathsf{J}\langle\rho\rangle$ where $\langle\rho\rangle$ is defined inductively as follows

[TABLE]

Each term $t:\rho$ is translated to a term $\langle t\rangle:\mathsf{J}\langle\rho\rangle$. In order to translate function application, we have to consider a monadic notion of application. Given $f:\mathsf{J}(\sigma\to\mathsf{J}\tau)$ and $a:\sigma$, we ‘apply’ $f$ to $a$ as

[TABLE]

Then for any terms $t:\sigma\to\tau$ and $u:\sigma$, we define $\langle tu\rangle\coloneqq\langle t\rangle\diamond\langle u\rangle$. The rest of the translation can be found in the appendix.

4.3 The Kuroda-style monadic translation

There is also a Kuroda-style monadic translation of System $\mathsf{T}$ which has been studied by Powell in [18, 19], where each type $\rho$ is translated to $\mathsf{J}[\rho]$ with $[\rho]$ defined by

[TABLE]

Note that it actually corresponds to the variant of Kuroda’s negative translation where double negations are placed also in front of conclusions of implications (see [16, Section 6]). Here we need another notion of application for the term translation: Given $f:\mathsf{J}(\sigma\to\mathsf{J}\tau)$ and $a:\mathsf{J}\sigma$, we ‘apply’ $f$ to $a$ as

[TABLE]

The complete translation can be found in the appendix.

Powell makes use of the Kuroda-style translation to extract moduli of continuity [19, Section 5], similarly to our development in Section 3.3. However, our algorithms are different because the Kuroda-style translation is call-by-value while our Gentzen-style one is call-by-name. Consider the following example. Let $t=\lambda\alpha.\mathsf{rec}(\alpha 0,\lambda nm.0,1):\mathbb{N}^{\mathbb{N}}\to\mathbb{N}$ which is a constant function. If we apply the Kuroda-style translation to $t$ with the continuity nucleus (similar to the one given in Section 3.3 but generalized to arbitrary types of $\mathsf{T}$), then we get a modulus $\lambda\alpha.1$, because in the call-by-value strategy all the inputs of $\mathsf{rec}$ including $\alpha 0$ are evaluated. With the Gentzen-style translation, we get $\lambda\alpha.0$ because $\alpha 0$ is never evaluated in the call-by-name strategy.

Appendix A The Kolmogorov- and Kuroda-style monadic translations of T

We present the Kolmogorov- and Kuroda-style monadic translations of System $\mathsf{T}$ extended with products and sums, parametrized by a nucleus $(\mathsf{J},\eta,\kappa)$, where $\mathsf{J}$ is an endofunction on types of $\mathsf{T}$ and $\eta:\sigma\to\mathsf{J}\sigma$ and $\kappa:(\sigma\to\mathsf{J}\tau)\to\mathsf{J}\sigma\to\mathsf{J}\tau$ are terms of $\mathsf{T}$. Recall the following notions of monadic application that will be needed in the translations:

• •

Given $f:\mathsf{J}(\sigma\to\mathsf{J}\tau)$ and $a:\sigma$, we define

[TABLE]

• •

Given $f:\mathsf{J}(\sigma\to\mathsf{J}\tau)$ and $a:\mathsf{J}\sigma$, we define

[TABLE]

Definition A.1** (Kolmogorov-style monadic translation).**

We assign to each type $\rho$ a type $\mathsf{J}\langle\rho\rangle$ where $\langle\rho\rangle$ is defined as follows

[TABLE]

Each term $\Gamma\vdash t:\rho$ is translated to a term $\langle\Gamma\rangle\vdash\langle t\rangle:\mathsf{J}\langle\rho\rangle$, where $\langle\Gamma\rangle$ is a new context assigning each $x:\sigma\in\Gamma$ to a fresh variable $\hat{x}:\mathsf{J}\langle\sigma\rangle$, and $\langle t\rangle$ is defined inductively as follows:

[TABLE]

where $\mathsf{rec}^{\diamond}:\sigma\to(\mathsf{J}\mathbb{N}\to\mathsf{J}(\mathsf{J}\sigma\to\mathsf{J}\sigma))\to\mathbb{N}\to\mathsf{J}\sigma$ is defined by

[TABLE]

Definition A.2** (Kuroda-style monadic translation).**

We assign to each type $\rho$ a type $\mathsf{J}[\rho]$ where $[\rho]$ is defined as follows

[TABLE]

Each term $\Gamma\vdash t:\rho$ is translated to a term $[\Gamma]\vdash[t]:\mathsf{J}[\rho]$, where $[\Gamma]$ is a new context assigning each $x:\sigma\in\Gamma$ to a fresh variable $\bar{x}:[\sigma]$, and $[t]$ is defined inductively as follows:

[TABLE]

where $\mathsf{rec}^{\bullet}:\sigma\to(\mathbb{N}\to\mathsf{J}(\sigma\to\mathsf{J}\sigma))\to\mathbb{N}\to\mathsf{J}\sigma$ is defined by

[TABLE]