A unifying framework for continuity and complexity in higher types

TL;DR

This paper introduces a unified framework for analyzing higher-order computation concepts like termination, continuity, and complexity in functional languages, providing new methods for extracting moduli and characterizing complexity.

Contribution

It develops a parametrised monadic translation that unifies various notions in higher types and offers concrete instantiations for analyzing continuity and complexity.

Findings

Unified scheme for higher-order notions

Method for extracting moduli of continuity

Characterization of bar recursion complexity

Abstract

We set up a parametrised monadic translation for a class of call-by-value functional languages, and prove a corresponding soundness theorem. We then present a series of concrete instantiations of our translation, demonstrating that a number of fundamental notions concerning higher-order computation, including termination, continuity and complexity, can all be subsumed into our framework. Our main goal is to provide a unifying scheme which brings together several concepts which are often treated separately in the literature. However, as a by-product, we also obtain (i) a method for extracting moduli of continuity for closed functionals of type $(\mathbb{N}\to\mathbb{N})\to\mathbb{N}$ definable in (extensions of) System T, and (ii) a characterisation of the time complexity of bar recursion.

Equations

$$\text{mbox}Types:\rho ,\tau ::=\delta |\rho \to \tau \text{mbox}for\delta \in \mathtt{datatype}$$

$$\text{mbox}Terms:s,t::=x|c|f|\lambda x.t|ts\text{mbox}forc\in \mathtt{cons},f\in \mathtt{func}$$

$$\Gamma ,x:\rho ⊢x:\rho \frac{\Gamma ,x:\rho ⊢t:\tau }{\Gamma ⊢\lambda x.t:\rho \to \tau }\frac{\Gamma ⊢t:\rho \to \tau \Gamma ⊢s:\rho }{\Gamma ⊢ts:\tau }$$

$$\Gamma ⊢c:{\delta }_1\to \dots \to {\delta }_m\to \delta \Gamma ⊢f:{\rho }_1\to \dots \to {\rho }_n\to \rho$$

$$\text{mbox}Patterns:p,q::=x^{\rho }|c{p}_1\dots p_k\text{mbox}fork=\mathrm{ar}(c)$$

$$\text{mbox}Values:u,v::=c{v}_1\dots v_i|f{v}_1\dots v_j|\lambda x.r\text{mbox}fori\le \mathrm{ar}(c),j<\mathrm{ar}(f),x:\rho ⊢r$$

$$\displaystyle v\downarrow_{\rho}v\mbox{ \ \ for values $v$}$$

$$\displaystyle\frac{r[u/x]\downarrow_{\tau}v}{(\lambda x.r)u\downarrow_{\tau}v}\mbox{ \ \ for $x:\rho\vdash r$ and $u:\rho$ a value}$$

$$\displaystyle\frac{r\sigma\downarrow_{\rho}v}{fv_{1}\ldots v_{n}\downarrow_{\rho}v}\mbox{ \ \ for $v_{1},\ldots,v_{n}=p_{1}\sigma,\ldots,p_{n}\sigma$ and $fp_{1}\ldots p_{n}\leadsto r$}$$

$$\displaystyle\frac{e\downarrow_{\rho\to\tau}u\ \ \ \ \ e^{\prime}\downarrow_{\rho}v\ \ \ \ \ \ uv\downarrow_{\tau}w}{ee^{\prime}\downarrow_{\tau}w}\mbox{ \ \ \ if one of $e$, $e^{\prime}$ is not a value}$$

$$f{p}_1\dots p_k⇝r$$

$$\frac{\Gamma ⊢t_1:{\rho }_1\cdots \Gamma ⊢t_n:{\rho }_n}{\Gamma ⊢f{t}_1\dots t_n:\rho }$$

$$\mathtt{func}:=\{\mathtt{rec}^{\rho\to({\rm Nature}\to\rho\to\rho)\to{\rm Nature}\to\rho}_{\rho}\;:\;\mbox{$\rho$ a type}\}$$

$${\mathtt{rec}}_{\rho }xy0⇝x\mathtt{rec}xy(\mathtt{s}z)⇝yz({\mathtt{rec}}_{\rho }xyz).$$

$${\mathtt{rec}}_{\rho }{v}_1{v}_{2}0{\downarrow }_{\rho }{v}_1\frac{v_2\mathbf{n}{\downarrow }_{\rho \to \rho }u{\mathtt{rec}}_{\rho }{v}_1{v}_2\mathbf{n}{\downarrow }_{\rho }vuv{\downarrow }_{\rho }w}{{\mathtt{rec}}_{\rho }{v}_1{v}_2\mathtt{s}(\mathbf{n}){\downarrow }_{\rho }w}$$

$$\mathtt{func}:=\{\mathtt{fold}_{\rho}^{\rho\to({\rm Nature}\to\rho\to\rho)\to{\rm Nature}^{\ast}\to\rho}\;:\;\mbox{$\rho$ a type}\}\cup\{+,\times,<,\mathtt{len}\}$$

$${\mathtt{fold}}_{\rho }xy\epsilon ⇝x{\mathtt{fold}}_{\rho }xy(zs::z)⇝yz({\mathtt{fold}}_{\rho }xyzs)$$

$${\mathtt{fold}}_{\rho }{v}_1{v}_2\epsilon {\downarrow }_{\rho }{v}_1\frac{v_2\mathbf{n}{\downarrow }_{\rho \to \rho }u{\mathtt{fold}}_{\rho }{v}_1{v}_2\mathbf{a}{\downarrow }_{\rho }vuv{\downarrow }_{\rho }w}{{\mathtt{fold}}_{\rho }{v}_1{v}_2(\mathbf{a}::\mathbf{n}){\downarrow }_{\rho }w}$$

$$\displaystyle\mathbf{m}<\mathbf{n}\downarrow_{\rm Nature}\mathtt{0}\mbox{ \ \ if $m<n$, else \ \ }\mathbf{m}<\mathbf{n}\downarrow_{\rm Nature}\mathbf{1}.$$

$$\displaystyle\mathtt{len}\;\mathbf{a}\downarrow_{\rm Nature}\mathbf{k}\mbox{ \ \ for $k=|a|$}$$

$$B(\omega,\phi,\psi,a)=_{\mathbb{N}}\begin{cases}\phi(a)&\mbox{if $\omega(\hat{a})<|a|$}\\ \psi(a,\lambda x\;.\;B(\omega,\phi,\psi,a\ast x))&\mbox{otherwise}\end{cases}$$

$$\mathtt{ext}$$

$$\mathtt{bar}$$

$${\mathtt{bar}}_1$$

$${\rho }_1$$

$${\rho }_2$$

$${\rho }_3$$

$$\mathtt{ext}[x_1,\dots ,x_k]\mathbf{n}$$

$$\mathtt{bar}fghxs$$

$${\mathtt{bar}}_{1}fghxs0$$

$${\mathtt{bar}}_{1}fghxs\mathtt{s}z$$

$$\frac{v_1(\mathtt{ext}\mathbf{a}){\downarrow }_{\mathrm{Nature}}\mathbf{k}k<|a|v_2\mathbf{a}{\downarrow }_{\mathrm{Nature}}\mathbf{n}}{\mathtt{bar}{v}_1{v}_2{v}_3\mathbf{a}\downarrow \mathbf{n}}$$

$$\frac{v_1(\mathtt{ext}\mathbf{a}){\downarrow }_{\mathrm{Nature}}\mathbf{k}k\ge |a|v_3\mathbf{a}(\lambda x.\mathtt{bar}{v}_1{v}_2{v}_3(\mathbf{a}::x)){\downarrow }_{\mathrm{Nature}}\mathbf{n}}{\mathtt{bar}{v}_1{v}_2{v}_3\mathbf{a}{\downarrow }_{\mathrm{Nature}}\mathbf{n}}$$

$$\text{mbox}Types:\rho ,\tau ::=\gamma ||\delta ||\rho \times \tau |\rho \to \tau \text{mbox}for\delta \in \mathtt{datatype}$$

$$\text{mbox}Terms:r,s,t::=\iota |t_{+}|\{r,s,t\}|x|⟨c⟩|⟨f⟩|\lambda x.t|ts|(s,t)|t_l|t_r\text{mbox}forc\in \mathtt{cons},f\in \mathtt{func}$$

$$\Gamma ⊢\iota :\gamma \frac{\Gamma ⊢t:\gamma }{\Gamma ⊢t_{+}:\gamma }\frac{\Gamma ⊢r:\gamma \Gamma ⊢s:\gamma \Gamma ⊢t:\gamma }{\Gamma ⊢\{r,s,t\}:\gamma }$$

$$\frac{\Gamma ⊢s:\rho \Gamma ⊢t:\tau }{\Gamma ⊢(s,t):\rho \times \tau }\frac{\Gamma ⊢t:\rho \times \tau }{\Gamma ⊢t_l:\rho }\frac{\Gamma ⊢t:\rho \times \tau }{\Gamma ⊢t_r:\tau }$$

$$\Gamma ⊢⟨c⟩:|{\delta }_1|\to \dots \to |{\delta }_m|\to |\delta |\Gamma ⊢⟨f⟩:|{\rho }_1|\to \dots \to |{\rho }_n|\to \gamma \times |\rho |$$

$$|\rho \to \tau |:=|\rho |\to \gamma \times |\tau |.$$

$${\lambda }^{\ast }{x}^{\rho }.r:=(\iota ,\lambda x^{\rho }.r):\gamma \times |\rho \to \tau |$$

Full text

1. Introduction

Monads are a fundamental tool for analysing functional programs [23, 39]. They allow us to capture information about a program’s execution, such as its computational complexity, and similarly enable us to reason about intensional aspects of higher-order functionals, such as continuity properties enjoyed by terms of System T.

This paper comprises a general study of monads and their application to higher-order functional languages, with an emphasis on languages which pertain to proof theory and program extraction. We focus on a simple yet powerful technique frequently encountered in the literature, which can be roughly described as follows:

1. (1)

set up a mapping $|{\cdot}|$ which transforms terms $e$ of type $\rho$ in some pure functional language into terms $|{e}|$ of type $|{\rho}|$ in some monadic metalanguage, 2. (2)

establish a logical relation $\blacktriangleleft$ between $\rho$ and $|{\rho}|$, 3. (3)

appeal to induction over the structure of terms to prove that $e\blacktriangleleft|{e}|$ for all terms $e$ of type $\rho$.

We explore an abstract translation of this kind, which maps a higher-order call-by-value target language into a metalanguage based on the writer monad $C\times-$. Our mapping will actually be the composition of a syntactic monadic translation $|{\cdot}|$ together with a standard denotational semantics $\llbracket{\cdot}\rrbracket$, and we define a general logical relation $\blacktriangleleft$ on $\rho\times\llbracket{|{\rho}|}\rrbracket$ which comprises a monadic part $\Downarrow$ together with a semantic bounding relation $\lhd$.

Our first main result is to establish a general soundness theorem for $\blacktriangleleft$, which identifies a set of abstract conditions that guarantee that $e\blacktriangleleft\llbracket{|{e}|}\rrbracket$ for all terms of our target language. We then demonstrate that this combination of a monadic and bounding component is rich enough to express a variety of fundamental concepts from the theory of higher-order computation, including majorizability (in the sense of Howard [16]), continuity (on the Baire space) and several notions of time complexity.

In the case of continuity, we focus on terms of type level 2 that induce functionals $\mathbb{N}^{\mathbb{N}}\to\mathbb{N}$. It is well known that functionals of this sort that are definable as closed terms of Gödel’s System T are continuous in the sense that their output is determined by a finite part of their input. Moreover, explicit moduli of continuity can be defined within System T itself. In recent years there has been a renewed interest in syntactic approaches to continuity which provide explicit moduli of continuity, and several new proofs of the continuity of System T definable functionals have been given, including [8, 12, 14] and most recently [17, 29, 40]. We provide another proof of this fact via our abstract framework, which applies not just to System T but to arbitrary languages that satisfy the relevant conditions.

We then show that by adjusting the parameters of our translation, we are able to characterise the time complexity, or cost, of terms in our programming language. Here, we crucially consider the cost of a higher-order term to be a higher-order object itself. Though the analysis of higher-order complexity via higher-order cost expressions dates back to the 1980s and has been widely researched since (e.g. [1, 30, 34, 37]), our general bounding relation $\lhd$ allows us to also approach complexity along the lines of Danner et al. [9, 10], where datatypes are assigned abstract sizes and the translation seeks to provide upper bounds on the cost of programs.

The main significance of our work lies in our development an abstract semantics for reasoning about intensional properties of higher-order functionals, which encompasses a number of somewhat disparate concepts, ranging from majorizability, which is of fundamental importance to the proof mining program (Section 4.3), to the static cost analysis of functional programs (Section 6). This effort towards unification is not just of theoretical interest, but could potentially inform those working on the formalization of monadic translations111For example, in the case of continuity, both [12] and [40] have been formalised in Agda, while bounded complexity as set out in [10] comes with a Coq implementation.

A second novelty is that we focus not only on variants of Gödel’s System T, but also more complex forms of recursion such as Spector’s bar recursion [35]. Recursion of this kind is rarely treated in the context of static analysis, but has great importance in proof theory and particularly the area of program extraction, where it is used to give a computational interpretation to the axiom of countable choice. We carry out what is, to the best of our knowledge, the first static cost analysis of bar recursion as functional programs, and in doing so we hope more generally to provide another illustration of how monads enable us to better understand structures from proof theory.

2. A higher-order functional language

We start by outlining our target language, to which our monadic translation will be applied. This will be a standard call-by-value typed functional language, where for now we do not specify what our datatypes or function symbols will be. Rather we take these as parameters, and consider a number of concrete instantiations of the language later on.

Types and terms of the language are outlined in Figure 1. Types are built from a base set of datatypes $\mathtt{datatype}$, and a single rule which allows for the construction of function types. Terms are then built in the usual way via lambda abstraction and function application from a countable set of variables $x:\rho$ for each type together with a set of constructor terms $\mathtt{cons}$ and a set of function symbols $\mathtt{func}$. Each constructor term $c$ is assigned some type $\delta_{1}\to\ldots\to\delta_{k}\to\delta$, where the $\delta_{i}$ are datatypes and $k=\mathrm{ar}(c)$ is the arity of $c$. Similarly, each function symbol $f$ is assigned a type $\rho_{1}\to\ldots\to\rho_{k}\to\rho$, where now the $\rho_{i},\rho$ are arbitrary and $k=\mathrm{ar}(f)$ is a specified arity of $f$. Formal typing rules $\Gamma\vdash t:\rho$ for terms are included, though we often just write $t:\rho$ or $t^{\rho}$ where this is unambiguous and the context is not necessary. A closed term $e$ is a term without any free variables, or alternatively one typeable as $\emptyset\vdash e:\rho$.

In order to specify the operational semantics of our language, we introduce standard notions of patterns and values, which are defined as in Figure 2. Note that values are always closed terms - in the third clause this is ensured by the typing restriction that $r$ has no free variables other than $x:\rho$. We also need the notion of a substitution, and later that of a value environment. For $\Gamma,x:\rho\vdash t:\tau$ and $\Gamma\vdash s:\rho$ we write $\Gamma\vdash t[s/x]$ to denote the term obtained by substituting all free occurrences of $x$ in $t$ by $s$ (with the usual restrictions on free variables in $s$). This is formally definable by induction on the structure of $t$. For a term $\Gamma\vdash t:\rho$ with $\Gamma:\equiv x_{1}:\rho_{1},\ldots,x_{n}:\rho_{n}$, a value environment $\sigma$ is a mapping which assigns each variable $x_{i}:\rho_{i}$ a value $\sigma(x_{i})$ of type $\rho_{i}$. We denote by $t\sigma:\rho$ the closed term $t[\sigma(x_{1})/x_{1},\ldots,\sigma(x_{k})/x_{k}]$.

A big step operational semantics for our language is given in Figure 3.

Note that reductions are of the form $e\downarrow_{\rho}v$ where $e:\rho$ is a closed term and $v:\rho$ a value of the same type. We often omit the typing on $\downarrow_{\rho}$ when there is no risk of ambiguity. Reductions follow the usual rules for the call-by-value lambda calculus, together with a set of defining rules for each function symbol of the form

[TABLE]

where $p_{1},\ldots,p_{k}$ are patterns, $k=\mathrm{ar}(f)$ and $r$ is a term whose free variables are contained in those of $p_{1},\ldots,p_{k}$. We assume that the rules defining each function symbol are complete and orthogonal, by which we mean that for each $f$ of arity $k$ and any values $v_{1},\ldots,v_{k}$ of the appropriate type, there is exactly one rule $fp_{1}\ldots p_{k}\leadsto r$ such that $v_{1},\ldots,v_{n}=p_{1}\sigma,\ldots,p_{k}\sigma$ for a suitable environment $\sigma$. Note that for any closed term $e$, at most one rule in Figure 3 is applicable, and thus a simple induction over derivations proves that if $e\downarrow v$ and $e\downarrow v^{\prime}$ then $v=v^{\prime}$.

Remark 1**.**

A more traditional presentation of our target language would have been to instead take the formation rule

[TABLE]

as primitive, together with an analogous rule for the constructors. Then values would simply be terms of the form $cv_{1}\ldots v_{m}$ (for $m=\mathrm{ar}(c)$) or $\lambda x.r$, and the semantics would be altered accordingly. However, we have instead chosen to take the function symbols as primitive, as it is slightly more convenient for the purposes of setting up our monadic translation.

We now give some concrete instantiations of our parametrised language, all of which will play a role later.

2.1. Gödel’s System T (simple variant)

A call-by-value variant of System T is obtained in our setting by defining $\mathtt{datatype}:=\{{\rm Nature}\}$, $\mathtt{cons}:=\{\mathtt{0}^{\rm Nature},\mathtt{s}^{{\rm Nature}\to{\rm Nature}}\}$ and

[TABLE]

where the recursor $\mathtt{rec}_{\rho}$ has defining equations

[TABLE]

We write $\mathbf{n}:=\mathtt{s}^{(n)}(\mathtt{0})$ for the numeral representation of $n\in\mathbb{N}$. In this language, one can show by induction on the size of $v$ that the only values of type ${\rm Nature}$ are indeed those of the form $\mathbf{n}$, a fact which we will freely use throughout. The operational semantics of $\mathtt{rec}_{\rho}$ can be concisely expressed via the following derived rules:

[TABLE]

2.2. Gödel’s System T (list based variant)

A slightly richer (but computationally equivalent) version of System T is obtained by defining $\mathtt{datatype}:=\{{\rm Nature},{\rm Nature}^{\ast}\}$, $\mathtt{cons}:=\{\mathtt{0}^{\rm Nature},\mathtt{s}^{{\rm Nature}\to{\rm Nature}},\varepsilon^{{\rm Nature}^{\ast}},\;\mathtt{::}\;^{{\rm Nature}^{\ast}\to{\rm Nature}\to{\rm Nature}^{\ast}}\}$ and

[TABLE]

where $+,\times,<$ have type ${\rm Nature}\to{\rm Nature}\to{\rm Nature}$ and $\mathtt{len}$ has type ${\rm Nature}^{\ast}\to{\rm Nature}$. We adopt the usual convention of writing $s::t$ instead of $::\;s\;t$, and similarly for the operator symbols, and in addition we write $[s_{1},\ldots,s_{k}]$ for $(\ldots(\varepsilon::s_{1})::\dots)::s_{k}$. For $a=(a_{1},\ldots,a_{k})\in\mathbb{N}^{\ast}$ we write $\mathbf{a}:=[\mathbf{a}_{1},\ldots,\mathbf{a}_{k}]$. Again, a simple induction over the size of values establishes that any $v:{\rm Nature}^{\ast}$ is of the form $v=\mathbf{a}$ for some $a\in\mathbb{N}^{\ast}$. Along with the usual defining equation for the fold function:

[TABLE]

which gives rise to the derived rules

[TABLE]

we can incorporate basic operators into our language by defining each of them explicitly via a countable set of rules e.g. $\mathbf{m}+\mathbf{n}\leadsto\mathbf{k}$ for $k=m+n$ and so on, which then satisfy operational rules $\mathbf{m}+\mathbf{n}\downarrow_{\rm Nature}\mathbf{k}$. We define $<$ and $\mathtt{len}$ in an analogous fashion so that

[TABLE]

where $|a|$ denotes the length of $a\in\mathbb{N}^{\ast}$.

2.3. Spector’s bar recursion

The final language we consider here is an extension of the list language in Section 2.2 with Spector’s bar recursor of lowest type, originally introduced in [35] (but see e.g. [24] for a more modern introduction). This is a form of backward recursion over wellfounded trees, where for this particular variant, wellfoundedness is typically ensured by appealing to some form of continuity on the parameters of the recursion. In a simple equational calculus it would be given by the defining equation

[TABLE]

where the output type is $\mathbb{N}$ as indicated, and the input parameters have type $\omega:\mathbb{N}^{\mathbb{N}}\to\mathbb{N}$, $\phi:\mathbb{N}^{\ast}\to\mathbb{N}$ and $\psi:\mathbb{N}^{\ast}\times(\mathbb{N}\to\mathbb{N})\to\mathbb{N}$ and $a\in\mathbb{N}^{\ast}$ respectively. In addition, we have $a\ast x:=(a_{1},\ldots,a_{k},x)$ and $\hat{a}:\mathbb{N}\to\mathbb{N}$ is defined by $\hat{a}_{n}:=a_{i}$ for $i<n$ and otherwise [math]. Bar recursion will primarily play a role in Sections 4.2 and 6.2, where we focus on termination and complexity, respectively. For now, we simply give the main definitions we will need later. We first need to add three additional function symbols

[TABLE]

where

[TABLE]

which have defining equations

[TABLE]

It is not difficult to show that the operational semantics in this case give rise to the following derived rules for $\mathtt{bar}$ (here we eliminate the intermediate steps involving $\mathtt{bar}_{1}$)

[TABLE]

Remark 2**.**

The above formulation of bar recursion as a rewrite system is inspired by Berger [5], which in turn uses a trick due to Vogel [38]. There bar recursion is considered in its general form, where the type of $\mathbf{a}$ and the output can be arbitrary. Though such a generalisation can easily be incorporated here by encoding lists of type $\rho$ as objects of type ${\rm Nature}\to\rho$, for us bar recursion plays a predominantly illustrative role, and so for simplicity we restrict ourselves to the recursor of base type.

3. The main soundness theorem

In this section we present our main framework, first setting up our monadic translation and the associated logical relation, before proving that the translation is sound with respect to the relation. This soundness result, given as Theorem 4, is just an instance of the General Theorem of Logical Relations for our particular relation. As mentioned right at the beginning, our translation is actually the composition of a syntactic translation into a monadic metalanguage and a standard denotational semantics. We outline each of these in turn.

3.1. The monadic metalanguage

The metalanguage is defined similarly to our target language. However, here we only specify types and terms, which will then be assigned a denotational semantics in the next section. The monadic language is summarised in Figure 4.

Types are constructed from a special type $\gamma$ together with base types $|{\delta}|$ for all datatypes of the target language, and now allow both function types and cartesian product types. We extend the mapping $|{\cdot}|$ on datatypes of the target language to arbitrary types by defining

[TABLE]

Terms now include a symbol $\langle{c}\rangle$ resp. $\langle{f}\rangle$ for each constructor resp. function symbol in the target language, whose types are indicated in Figure 4. Together with the usual term forming rules of the lambda calculus (now with pairing and projection to account for the product), we have three nonstandard rules for forming terms of type $\gamma$: a constant $\iota$, a unary operation ${t}_{+}$ and a ternary operation $\{{r},{s},{t}\}$. The meaning of these will become clearer later on.

For the first step of our translation, we assign to each $\Gamma\vdash t:\rho$ in the target language a term $|{\Gamma}|\vdash|{t}|:\gamma\times|{\rho}|$ in the metalanguage as indicated in Figure 5, where for $\Gamma=x_{1}:\rho_{1},\ldots,x_{k}:\rho_{k}$, we define $|{\Gamma}|:=x_{1}:|{\rho_{1}}|,\ldots,x_{k}:|{\rho_{k}}|$. Here we also use the following shorthand: for $r:\gamma\times|{\tau}|$ we define

[TABLE]

and similarly for the iterated version $\lambda^{\ast}x_{1}^{\rho_{1}},\ldots,x_{k}^{\rho_{k}}.r:\gamma\times|{\rho_{1}\to\ldots\to\rho_{k}\to\tau}|$.

3.2. A denotational semantics for the metalanguage

We assign our metalanguage a denotational semantics as specified in Figure 6. We assign sets $C$ and $D_{\delta}$ to the base types $\gamma$ and $|{\delta}|$ respectively, for each $\delta\in\mathtt{datatype}$. We leave open the precise meaning of the function space $X\Rightarrow Y$ for now. In what follows we will typically work in total models, where function spaces will either be the full set-theoretic function space, or the space of continuous functions from $X$ to $Y$ in the sense of Kleene [19] or Kreisel [22]

Terms $\Gamma\vdash t:\rho$ of the metalanguage are assigned an interpretation $\llbracket{t}\rrbracket\xi\in\llbracket{\rho}\rrbracket$ in the usual way, where $\xi$ is an environment mapping each $x_{i}:\rho_{i}\in\Gamma$ to some $\xi(x_{i})\in\llbracket{\rho_{i}}\rrbracket$. We assume that we have chosen suitable interpretations $\overline{c}$, $\overline{f}$ for each $\langle{c}\rangle$ and $\langle{f}\rangle$ respectively. Terms of type $\gamma$ are interpreted via a triple $(\epsilon^{C},\mathrm{inc}^{C\to C},\mathrm{com}^{C\times C\times C\to C})$.

3.3. The logical relation

Let $\rho$ be a type of our target language. We denote the set of all closed terms of type $\rho$ by $\mathtt{Cl}_{\rho}$, and the set of all values by $\mathtt{Val}_{\rho}$. We now suppose that we are given a pair of relations

[TABLE]

where $\rho$ ranges over all types in our target language and $\delta$ over all datatypes. We will generalise $\lhd_{\rho}$ to arbitrary types via the inductive clause

[TABLE]

where the relation $\blacktriangleleft_{\rho}$ on $\mathtt{Cl}_{\rho}\times(C\times\llbracket{|{\rho}|}\rrbracket)$ is defined by

[TABLE]

where in what follows we often abbreviate the inner conjunction as $e\Downarrow^{\pi_{0}a}v\lhd\pi_{1}a$. In the remainder of this section we seek to establish conditions under which the translation $\llbracket{|{\cdot}|}\rrbracket$ is sound with respect to $\blacktriangleleft$, by which we mean the following: {defi}

Given a value environment $\sigma$ for $\Gamma:=x_{1}:\rho_{1},\ldots,x_{k}:\rho_{k}$ in our target language and some denotational environment $\xi$ for $|{\Gamma}|=x_{1}:|{\rho_{1}}|,\ldots,x_{k}:|{\rho_{k}}|$, we write $\sigma\lhd_{\Gamma}\xi$ if $\sigma(x_{i})\lhd_{\rho_{i}}\xi(x_{i})$ for all $i=1,\ldots,k$. We say that $\llbracket{|{\cdot}|}\rrbracket$ is sound w.r.t. $\blacktriangleleft$ if for all $\Gamma\vdash t:\rho$ in our target language, we have

[TABLE]

for all $\sigma,\xi$.

We start by focusing on the monadic part of our relation. {defi}

We say that $(\epsilon,\mathrm{inc},\mathrm{com})$ is compatible with $\Downarrow$ if the following rules are satisfied:

[TABLE]

Lemma 3**.**

Suppose that $(\epsilon,\mathrm{inc},\mathrm{com})$ is compatible with $\Downarrow$. For $f\in C\times(\llbracket{|{\rho}|}\rrbracket\to C\times\llbracket{|{\tau}|}\rrbracket)$ and $a\in C\times\llbracket{|{\rho}|}\rrbracket$, define

[TABLE]

Then whenever $e\blacktriangleleft_{\rho\to\tau}f$ and $e^{\prime}\blacktriangleleft_{\rho}a$ then $ee^{\prime}\blacktriangleleft_{\tau}f\circ a$.

Proof 3.1**.**

We have $e\Downarrow^{\pi_{0}f}u\lhd_{\rho\to\tau}\pi_{1}f$ and $e^{\prime}\Downarrow_{\rho}^{\pi_{0}a}v\lhd\pi_{1}a$ for some $u,v$, and thus $uv\blacktriangleleft_{\tau}(\pi_{1}f)(\pi_{1}a)$, or in other words $uv\Downarrow_{\tau}^{\pi_{0}((\pi_{1}f)(\pi_{1}a))}w\lhd_{\tau}\pi_{1}((\pi_{1}f)(\pi_{1}a))$ for some $w$. Thus by Definition 3.3 we have $ee^{\prime}\Downarrow^{\pi_{0}(f\circ a)}_{\tau}w\lhd_{\tau}\pi_{1}(f\circ a)$, which is just $ee^{\prime}\blacktriangleleft_{\tau}f\circ a$.

{defi}

We say that our interpretations $\overline{c}$ for the constructor terms are compatible with $\lhd$ if for all constructor symbols $c:\delta_{1}\to\ldots\to\delta_{m}\to\delta$ we have $cv_{1}\ldots v_{m}\lhd_{\delta}\overline{c}a_{1}\ldots a_{m}$ whenever $v_{i}\lhd_{\delta_{i}}a_{i}$ for all $i=1,\ldots,m$ and values $v_{i}$.

Theorem 4**.**

Suppose that $(\epsilon,\mathrm{inc},\mathrm{com})$ is compatible with $\Downarrow$ and the $\overline{c}$ are compatible with $\lhd$. Suppose in addition that for all function symbols $f:\rho_{1}\to\ldots\to\rho_{n}\to\rho$ we have $fv_{1}\ldots v_{n}\blacktriangleleft_{\rho}\overline{f}a_{1}\ldots a_{n}$ whenever $v_{i}\lhd_{\rho_{i}}a_{i}$ for all $i=1,\ldots,n$ and values $v_{i}$. Then $\llbracket{|{\cdot}|}\rrbracket$ is sound w.r.t. $\blacktriangleleft$.

Proof 3.2**.**

We use induction on the structure of terms $\Gamma\vdash t:\rho$ to prove that $t\sigma\blacktriangleleft_{\rho}\llbracket{|{t}|}\rrbracket\xi$ whenever $\sigma\lhd_{\Gamma}\xi$. For variables, $x\sigma\blacktriangleleft_{\rho}\llbracket{|{x}|}\rrbracket\xi=(\epsilon,\xi(x))$ follows from the fact that $\sigma(x)\Downarrow^{\epsilon}\sigma(x)$ and $\sigma(x)\lhd_{\rho}\xi(x)$. For constructor symbols, suppose that $c:\delta_{1}\to\ldots\to\delta_{m}\to\delta$. Then we have $c\Downarrow^{\epsilon}_{\rho}c$, and since $\llbracket{|{c}|}\rrbracket=(\epsilon,\llbracket{\lambda x_{1}\lambda^{\ast}x_{2},\ldots,x_{m}.(\iota,\langle{c}\rangle x_{1}\ldots x_{m})}\rrbracket)$ it remains to show that for $v_{1}\lhd_{\delta_{1}}a_{1}$ we have

[TABLE]

Continuing this way for $cv_{1}v_{2},\ldots$ we must ultimately show that

[TABLE]

which follows from the fact that $\overline{c}$ is compatible with $\lhd$. This argument is easily adapted to show that $f\blacktriangleleft\llbracket{|{f}|}\rrbracket$, using the main assumption of the theorem.

For function application, by the induction hypothesis we have $t\sigma\blacktriangleleft_{\rho\to\tau}\llbracket{|{t}|}\rrbracket\xi$ and $s\sigma\blacktriangleleft_{\rho}\llbracket{|{s}|}\rrbracket\xi$. Thus by Lemma 3 we have

[TABLE]

where the last equality follows from unwinding definitions. In remains to deal with abstraction. Suppose that $\sigma\lhd\xi$. We need to show that

[TABLE]

for $\xi_{a}:=\xi\{x\mapsto a\}$. But since $\lambda x.t\sigma\Downarrow^{\epsilon}_{\rho\to\tau}\lambda x.t\sigma$ this reduces to showing that for any $u\lhd_{\rho}a$ we have

[TABLE]

for some $v\in\mathtt{Val}_{\tau}$. Because $u\lhd_{\rho}a$ implies $\sigma\{x\mapsto u\}\lhd\xi_{a}$, by the induction hypothesis we have

[TABLE]

for some $v$, and thus the result follows from Definition 3.3.

This concludes the first main part of the article, where we introduce our target language and establish a sound monadic translation which acts on it. Up to this point everything has been fairly standard: The first component of our translation into the monadic metalanguage is a simple call-by-value monadic translation using the writer monad. Theorem 4 is then a confirmation that the logical relation defined on terms of our target language and denotations of our metalanguage acts as it should. We now move onto the applications, where we show that Theorem 4, though simple, is surprisingly versatile.

4. Some simple applications for $C=\{0\}$

Before we move on to our main applications of the translation, we demonstrate that in the simple case where $C=\{0\}$ is a terminal object, thus collapsing the monadic part of the translation, our soundness theorem can still be related to a number of key concepts in the literature. In each of the examples that follow, we define

[TABLE]

Note that in this case, $(\epsilon,\mathrm{inc},\mathrm{com})$ are uniquely defined as just constant functions, and are compatible with $\Downarrow$ since the conditions of Definition 3.3 follow from the definition of $\downarrow$ in Figure 3.

4.1. Reducibility predicates

Let’s first consider the case where in addition to $C=\{0\}$ we have $D_{\delta}=\{0\}$ for all datatypes, and thus $\llbracket{\rho}\rrbracket\cong\{0\}$ for all types of the metalanguage - where here we implicitly use the isomorphisms $\{0\}\times\{0\}\cong\{0\}$ and $(X\to\{0\})\cong\{0\}$. We define

[TABLE]

Now let us write $R_{\rho}(e):\Leftrightarrow e\blacktriangleleft_{\rho}0$ and $R^{\scriptsize{\mathrm{val}}}_{\rho}(v):\Leftrightarrow v\lhd_{\rho}0$. Then it is easy to show that

[TABLE]

and therefore $R(e)$ and $R^{\scriptsize{\mathrm{val}}}(v)$ act as reducibility predicates. Moreover, whatever our constant symbols are, the $\bar{c}\in\{0\}$ are trivially compatible with $\lhd$. Thus the following result follows directly from our abstract soundness theorem.

Theorem 5**.**

Suppose that all function symbols $f:\rho_{1}\to\ldots\rho_{n}\to\rho$ in our target language satisfy

[TABLE]

for all values $v_{1},\ldots v_{n}$ of the appropriate type. Then for any closed term $e:\rho$ there exists some value $v$ such that $e\downarrow v$.

The above result confirms that termination of our target language as a whole follows from termination of the function symbols. As a simple application, we prove that our call-by-value version of System T (Section 2.1) terminates.

Corollary 6**.**

System T is terminating.

Proof 4.1**.**

We need to show that for any $v_{1},v_{2}$ of the appropriate type and numeral $\mathbf{n}$ we have

[TABLE]

(note that $R^{\scriptsize{\mathrm{val}}}_{\rm Nature}(\mathbf{n})$ trivially holds). We do this by induction on $n\in\mathbb{N}$, using the derived rules for the recursor given in Section 2.1. For $n=0$ we have $\mathtt{rec}_{\rho}\;v_{1}\;v_{2}\;\mathtt{0}\downarrow v_{1}$ and since $R^{\scriptsize{\mathrm{val}}}_{\rho}(v_{1})$ holds by assumption it follows that $R_{\rho}(\mathtt{rec}_{\rho}\;v_{1}\;v_{2}\;\mathtt{0})$. Now for the induction step, we assume that $R_{\rho}(\mathtt{rec}_{\rho}\;v_{1}\;v_{2}\;\mathbf{n})$ for some $n\in\mathbb{N}$, which means that $\mathtt{rec}_{\rho}\;v_{1}\;v_{2}\;\mathbf{n}\downarrow v$ for some $v$ satisfying $R^{\scriptsize{\mathrm{val}}}_{\rho}(v)$. Since $R^{\scriptsize{\mathrm{val}}}_{{\rm Nature}\to\rho\to\rho}(v_{2})$ implies that $v_{2}\;\mathbf{n}\downarrow u$ for some $u$ with $R^{\scriptsize{\mathrm{val}}}_{\rho\to\rho}(u)$, we then have $R_{\rho}(uv)$, which means that $uv\downarrow_{\rho}w$ for some $w$ with $R^{\scriptsize{\mathrm{val}}}_{\rho}(w)$. Finally, by the derived rule for the recursor, we have $\mathtt{rec}_{\rho}\;v_{1}\;v_{2}\;\mathtt{s}(\mathbf{n})\downarrow w$ and thus $R_{\rho}(\mathtt{rec}_{\rho}\;v_{1}\;v_{2}\;\mathtt{s}(\mathbf{n}))$, and we’re done.

For the usual formulation of System T as an equational calculus, the above result roughly corresponds to the fact that any inner-most, left-most sequence of reductions terminates in some normal form (cf. Troelstra [36, Theorem 2.2.6]). It readily generalises to functional languages with more complex datatypes and other forms of wellfounded recursion. However, for languages involving bar recursion, such as that presented in Section 2.3, termination requires us to make use of our bounding component $\lhd$.

4.2. Termination via denotational semantics

We now instantiate $\lhd_{\rho}$ so that it mimics the logical relation used in Plotkin’s famous adequacy proof for PCF [27], and demonstrate that this allows us to prove termination of bar recursion. The key here is to interpret our metalanguage in a continuous model, and then appeal to properties of the model in order to establish termination. Our approach closely follows Berger [4, 5], who sets up a more general framework in which strong normalization of higher-order rewrite systems can be proven using domain theoretic means.

We work with the instance of our target language given in Example 2.3, which contains two datatypes ${\rm Nature}$ and ${\rm Nature}^{\ast}$. We define $C=\{0\}$ as before, but now let $D_{\rm Nature}:=\mathbb{N}$ and $D_{{\rm Nature}^{\ast}}:=\mathbb{N}^{\ast}$. In addition, we interpret the function space $X\Rightarrow Y$ in our denotational model as the space of all total continuous functionals from $X$ to $Y$. Thus our metalanguage is interpreted in the standard model $\mathcal{C}^{\omega}$ of total continuous functionals over base types $\mathbb{N}$ and $\mathbb{N}^{\ast}$, which has various presentations in the literature: Via limit spaces (Scarpellini [31]), encodings or neighbourhoods (Kleene/Kreisel [19, 22]) or as the extensional collapse of the partial continuous functionals (Ershov [11]).

We first observe that for any type $\rho$ in our target language, $\llbracket{|{\rho}|}\rrbracket$ is isomorphic to the usual (non-monadic) denotational semantics of that type, since

[TABLE]

and thus we can ignore the monadic part of our translation. We define our logical relation as in Section 4.1, but now with a semantic component as follows:

[TABLE]

and as such, $\blacktriangleleft_{\rho}$ takes the following simplified form:

[TABLE]

Interpreting the constructor symbols in the obvious way i.e.

[TABLE]

it is clear that these interpretations are compatible with $\lhd$. In addition, we interpret the operator function symbols of our target language in the usual way, where in particular i.e.

[TABLE]

Finally, for bar recursion we let

[TABLE]

Note that $\overline{\mathtt{bar}}$ is just the traditional defining equation of bar recursion, and is known to be an object of $\mathcal{C}^{\omega}$ as originally proven by Scarpellini [31]. We now prove that the program $\mathtt{bar}$ is terminating.

Lemma 7**.**

Whenever $v_{1}\lhd_{({\rm Nature}\to{\rm Nature})\to{\rm Nature}}\omega$, $v_{2}\lhd_{{\rm Nature}^{\ast}\to{\rm Nature}}g$, $v_{3}\lhd_{{\rm Nature}^{\ast}\to({\rm Nature}\to{\rm Nature})\to{\rm Nature}}h$ and $a\in\mathbb{N}^{\ast}$, we have

[TABLE]

Proof 4.2**.**

Assuming the hypotheses of the lemma throughout, we first claim that for all $a\in\mathbb{N}^{\ast}$, whenever

[TABLE]

for all $n\in\mathbb{N}$ then $\mathtt{bar}\;v_{1}\;v_{2}\;v_{3}\;\mathbf{a}\blacktriangleleft_{\rm Nature}\overline{\mathtt{bar}}(\omega,g,h,a)$. There are two cases to consider:

• •

Case 1: $\omega(\hat{a})<|a|$. Then since $\mathtt{ext}\;\mathbf{a}\lhd\hat{a}$ and $v_{1}\lhd\omega$ we have $v_{1}(\mathtt{ext}\;\mathbf{a})\blacktriangleleft_{\rm Nature}\omega(\hat{a})$ and thus $v_{1}(\mathtt{ext}\;\mathbf{a})\downarrow\mathbf{k}$ for $k=\omega(\hat{a})<|a|$. Since in addition $v_{2}\lhd g$ and thus $v_{2}\;\mathbf{a}\blacktriangleleft_{\rm Nature}g(a)$ it follows that $v_{2}\;\mathbf{a}\downarrow\mathbf{n}$ for $n=g(a)$, and thus by the first derived rule given in Section 2.3 we have $\mathtt{bar}\;v_{1}\;v_{2}\;v_{3}\;\mathbf{a}\downarrow\mathbf{n}$ for $n=\overline{\mathtt{bar}}(\omega,g,h,a)$.

• •

Case 2: $\omega(\hat{a})\geq|a|$. By the same reasoning, we have $v_{1}(\mathtt{ext}\;\mathbf{a})\downarrow\mathbf{k}$ for $k=\omega(\hat{a})\geq|a|$. Now, by our assumption $(\ast)$ we have

[TABLE]

for any $n$, and since $\mathbf{n}\lhd m$ iff $n=m$ it follows that

[TABLE]

Using in addition that $v_{3}\lhd h$ it is not hard to show that

[TABLE]

and thus $v_{3}\;\mathbf{a}\;(\lambda x\;.\;\mathtt{bar}\;v_{1}\;v_{2}\;v_{3}\;\mathbf{a}::x)\downarrow\mathbf{n}$ for $n=\overline{\mathtt{bar}}(\omega,g,h,a::x))$. Thus by the second derived rule we have $\mathtt{bar}\;v_{1}\;v_{2}\;v_{3}\;\mathbf{a}\downarrow\mathbf{n}$ for $n=\overline{\mathtt{bar}}(\omega,g,h,a)$.

Combining cases we obtain $\mathtt{bar}\;v_{1}\;v_{2}\;v_{3}\;\mathbf{a}\blacktriangleleft\overline{\mathtt{bar}}(\omega,g,h,a)$, which proves the claim. We now come to the crucial part of the proof in which we utilise properties of the model $\mathcal{C}^{\omega}$ to establish termination of bar recursive programs. Suppose that for some $a\in\mathbb{N}^{\ast}$ it is not the case that $\mathtt{bar}\;v_{1}\;v_{2}\;v_{3}\;\mathbf{a}\blacktriangleleft\overline{\mathtt{bar}}(\omega,g,h,a)$. Then using our claim (in its contrapositive form) together with dependent choice on a metalevel (which is permitted in $\mathcal{C}^{\omega}$) there is an infinite sequence of numbers $b:=b_{0},b_{1},b_{2},\ldots$ such that

[TABLE]

for all $l\in\mathbb{N}$, where $[{b}]({l}):=(b_{0},\ldots,b_{l-1})$ denotes the initial segment of $b$ of length $l$. But it can be shown using a standard continuity argument (cf. [31]) that for any $\omega:\mathbb{N}^{\mathbb{N}}\to\mathbb{N}$ that there exists some $L\in\mathbb{N}$ such that

[TABLE]

and thus by an identical argument to the first case above (note that only Case 2 appeals to the assumption $(\ast)$) we have

[TABLE]

a contradiction. Thus $\mathtt{bar}\;v_{1}\;v_{2}\;v_{3}\;\mathbf{a}\blacktriangleleft\overline{\mathtt{bar}}(\omega,g,h,a)$ for all $a\in\mathbb{N}^{\ast}$.

This establishes the requirement of Theorem 4 for the functional symbol $\mathtt{bar}$. A simple adaptation of Lemma 7 can be used to to show that the same condition holds for the auxiliary term $\mathtt{bar}_{1}$ together with a suitably defined $\overline{\mathtt{bar}_{1}}$, while a straightforward induction achieves the same for $\mathtt{fold}_{\rho}$, the details of which we also omit. As a result, Theorem 4 yields the following:

Theorem 8**.**

For all closed terms $e:\rho$ in the bar recursive target language of Section 2.3 we have $e\downarrow v$ for some $v$.

The above theorem represents a normalization result for bar recursion, where for illustrative purpose we only consider the bar recursor of lowest type. Strong normalization of bar recursion (of arbitrary type) was first established by [38], and then (without infinite terms) in [6]. Our approach, which also replaces infinite terms by appealing to the construction of choice sequences in the model, has been explored in much more detail by Berger [4, 5], where also normalization results for variants of bar recursion (including the so-called BBC functional [2] and open recursion [3]) are established. One crucial difference is that we work in a total model instead of a partial model, and it is open whether or not we can extend our framework (which works in total models) to incorporate other forms of recursion such as those mentioned above.

Remark 9**.**

A well known result of Schwichtenberg [33] asserts that bar recursion of lowest type when applied to primitive recursive parameters is actually definable within System T (a generalisation of which has been more recently presented in [26]). Thus our bar recursive language as presented here would technically also be definable in System T, and as such a detour through the continuous functionals is not strictly necessary in order to prove termination. However, as already pointed out in Remark 2, we could readily extend our language to include bar recursion of arbitrary type, and the termination proof given as Lemma 7 would generalise accordingly. We also note that our approach is modular, and thus any extension of our bar recursive language with new function symbols which can be given a suitable interpretation is also terminating as a whole.

4.3. Majorizability

Our final simple application for the case $C=\{0\}$ will be an adaptation of Howard’s majorizability relation [16] to higher-order rewrite systems. Majorizability is an extension of the usual ordering $\leq$ on $\mathbb{N}$ to functionals of arbitrary finite type. In addition to forming the basis for interesting models of higher-order calculi, majorizability plays an essential role in the proof mining program, where it is used in conjunction with Gödel’s functional interpretation to form the monotone functional interpretation (introduced in [20]), which is crucial for interpreting forms of compactness related to the binary König’s lemma (for a detailed background on majorizability and its use in proof mining, see [21]). For simplicity we work over a target language with a single base type ${\rm Nature}$ with $D_{\rm Nature}=\mathbb{N}$. We define

[TABLE]

In this case, the logical relation $e\blacktriangleleft_{\rho}a$ is just a variant of the usual majorizability relation $\;\mathrm{maj}_{\rho}\;$ at all finite type, which in an equational setting is defined as follows (cf. [16] or [21, Definition 3.34])

[TABLE]

We compare this to our relation, which is based on the same idea but now phrased in terms of our programming language, and can be expanded as follows:

[TABLE]

To illustrate this correspondence further, note that in an equational calculus we would have

[TABLE]

whereas in our setting this would be rendered as

[TABLE]

In fact, we can prove the following key lemma, which is analogous to [21, Lemma 3.35 (iii)]:

Lemma 10**.**

Suppose that $e:\rho$ for $\rho:=\rho_{1}\to\ldots\to\rho_{n}\to{\rm Nature}$. Then

[TABLE]

Proof 4.3**.**

Induction on $n$. For $n=0$ this is just the definition of $\blacktriangleleft_{\rm Nature}$, and for the induction step we have

[TABLE]

where for the last step we use $ev\downarrow w\Leftrightarrow(\exists u)(e\downarrow u\wedge uv\downarrow w)$, which follows directly from the operational semantics of the language.

The following lemma is analogous to [21, Lemma 3.66].

Lemma 11**.**

Suppose that $e:{\rm Nature}\to\rho$ for $\rho:=\rho_{1}\to\ldots\to\rho_{k}\to{\rm Nature}$ and that $e\;\mathbf{n}\blacktriangleleft_{\rho}g(n)$ for all $n\in\mathbb{N}$. Then $e\blacktriangleleft_{{\rm Nature}\to\rho}g^{M}$ for

[TABLE]

Proof 4.4**.**

By Lemma 10 we have that $e\blacktriangleleft g^{M}$ is equivalent to

[TABLE]

and the result then follows by a straightforward induction on $m$.

Now, supposing for example that we work in an instance of our language, as in Section 2.1, where there are just two constructor symbols $\mathtt{0}$ and $\mathtt{s}$, which we interpret in the usual way as $\overline{\mathtt{0}}:=0$ and $\overline{\mathtt{s}}(n):=n+1$ so that they are compatible with $\lhd$. In this case our main soundness theorem becomes

Theorem 12**.**

If for all function symbols $f:\rho_{1}\to\ldots\to\rho_{n}\to\rho$ of our language there is a suitably defined $\overline{f}$ satisfying $fv_{1}\ldots v_{n}\blacktriangleleft_{\rho}\overline{f}a_{1}\ldots a_{n}$ whenever $v_{i}\lhd_{\rho_{i}}a_{i}$ for all $i=1,\ldots,n$ and values $v_{i}$, then any term $t:\rho$ has an interpretation $\llbracket{|{t}|}\rrbracket\in\llbracket{\rho}\rrbracket$ which majorizes it, in the sense that $\sigma\lhd\xi$ implies $t\sigma\blacktriangleleft_{\rho}\llbracket{|{t}|}\rrbracket\xi$. In particular, whenever $t:{\rm Nature}$ and $\sigma\lhd\xi$, we have $e\sigma\downarrow\mathbf{n}$ with $n\leq\llbracket{|{t}|}\rrbracket\xi$.

Corollary 13**.**

Any term $t:\rho$ in System T has an interpretation $\llbracket{|{t}|}\rrbracket$ which majorizes it.

Proof 4.5**.**

We just need to interpret the recursor, to which end we define $R:\llbracket{\rho}\rrbracket\Rightarrow(\mathbb{N}\Rightarrow\llbracket{\rho}\rrbracket\Rightarrow\llbracket{\rho}\rrbracket)\Rightarrow\mathbb{N}\Rightarrow\llbracket{\rho}\rrbracket$ by

[TABLE]

then it’s easy to show that whenever $v_{1}\lhd_{\rho}a$, $v_{2}\lhd_{\rho}f$ and $n\in\mathbb{N}$ then

[TABLE]

using induction on $n$. Then by Lemma 11 it follows that

[TABLE]

and thus defining $\overline{\mathtt{rec}}(a,f,n)=R(a,f)^{M}(n)$ it follows that for $n\leq m$ we have $\mathtt{rec}\;v_{1}\;v_{2}\;\mathbf{n}\blacktriangleleft_{\rho}\overline{\mathtt{rec}}(a,f,m)$.

Corollary 13 is closely related to classic results of Howard [16] and Bezem [7] which show that various type structures of majorizable functionals are a model of System T. This also holds more generally for bar recursion, and we conjecture that a variant of Theorem 12 dealing with $\mathtt{bar}$ as defined in Section 2.3 can be proven within our framework, though we do not attempt to work out the details here. The most important property of our Theorem 12 is that it can be extended in a uniform way to a number of different programming languages.

5. Extracting moduli of continuity for functional languages

We now utilise the monadic part of our soundness theorem for the first time, to present a simple framework in which we can extract moduli of continuity from those functionals of type level $2$ which are definable by a term in our target language.

That all type level $2$ functionals definable in System T have a modulus of continuity also definable in T was apparently first presented by Kreisel in lectures from 1971/72, and early proofs can be found in e.g. [32] and [36] (Theorem 2.3.9). The approach presented here is more closely connected to recent work, where continuity and the extraction of corresponding moduli are established by appealing to monads and effects (e.g. [8, 12, 14, 17, 29, 40], though this list is by no means exhaustive). A related monadic translation in all finite types due to the present author, but using the state monad and working in an equational setting, is also the basis for [28].

Our main motivation in studying continuity lies not in the fact that this result is new or surprising in itself, but in demonstrating that it fits elegantly into our uniform framework, which can, moreover, be readily extended to other languages and forms of recursion.

5.1. The languages $\mathcal{P}$, $\mathcal{P}^{T}$ and $\mathcal{P}_{g}$

We illustrate our approach by working in a target language with a single datatype ${\rm Nature}$ and the usual constructors $\mathtt{0}$ and $\mathtt{s}$, and assume that we have fixed some collection of function symbols $\mathtt{func}$. We call this base language $\mathcal{P}$, and observe that our simple variant of System T outlined in Section 2.1 is an instance of $\mathcal{P}$, which we later label as $\mathcal{P}^{T}$.

Now, to an arbitrary function $g:\mathbb{N}^{\mathbb{N}}$ we associate a variant $\mathcal{P}_{g}$ (resp. $\mathcal{P}_{g}^{T}$) of our base language, whose function symbols are the same as those of $\mathcal{P}$ but now extended to include an oracle $\alpha:{\rm Nature}\to{\rm Nature}$ whose defining equations are given by

[TABLE]

for each $n\in\mathbb{N}$, where here $\mathbf{g(n)}$ denotes the numeral representation of $g(n)$. Note that for any two functions $g,h:\mathbb{N}^{\mathbb{N}}$ the languages $\mathcal{P}_{g}$ and $\mathcal{P}_{h}$ have the same terms, and so differ only in the operational semantics of $\alpha$. We clearly distinguish the operational semantics of $\mathcal{P}$ from that of $\mathcal{P}_{g}$ by using $e\downarrow_{g}v$ to denote the big-step relation of the latter, which also includes the derived rule $\alpha\;\mathbf{n}\downarrow_{g}\mathbf{g(n)}$.

5.2. The monadic translation

We now define $D_{\rm Nature}:=\mathbb{N}$ as usual, but this time set $C:=\mathbb{N}^{\ast}$. Fixing some $g:\mathbb{N}^{\mathbb{N}}$, we define the logical relation $\blacktriangleleft_{g}$ on terms of $\mathcal{P}_{g}$ via $\mathbf{n}\lhd m:\Leftrightarrow n=m$ and

[TABLE]

where

[TABLE]

Finally, our denotational semantics $\llbracket{\cdot}\rrbracket_{g}$ of the monadic metalanguage arising from $\mathcal{P}_{g}$, which is also parametrised by $g$, is defined by firstly instantiating our monadic components as

[TABLE]

and interpreting our constructors in the obvious way. We assume that for each function symbol we have an interpretation $\overline{f}$ which is independent of $g$, and as such, this parameter only plays a role in the interpretation of the oracle function symbol $\alpha:{\rm Nature}\to{\rm Nature}$, whereby we set $\overline{\alpha}_{g}:\mathbb{N}\Rightarrow\mathbb{N}^{\ast}\times\mathbb{N}$ to be

[TABLE]

If we are working in either the full set theoretic model $\mathcal{S}^{\omega}$ or a continuous model $\mathcal{C}^{\omega}$, everything up until now is well defined. As before, it is clear that the interpretation of the constructors is compatible with $\lhd_{\rm Nature}$, and we also have the following:

Lemma 14**.**

The tuple $(\epsilon,\mathrm{inc},\mathrm{com})$ is compatible with $\Downarrow_{g}$.

Proof 5.1**.**

We deal with each rule in turn. We have $v\downarrow_{h}v$ for any values and parameter $h$, and so $v\Downarrow^{c}_{g}v$ is true for any $c$, and in particular $c=[]$.

If $r[u/x]\Downarrow^{c}_{g}v$ then $r[u/x]\downarrow_{g}v$ and whenever $g=_{c}h$ then $r[u/x]\downarrow_{h}v$. But then $(\lambda x.r)u\downarrow_{g}v$ in $\mathcal{P}_{g}$, and since $g=_{\mathrm{inc}(c)}h$ is just $g=_{c}h$ we have $r[u/x]\downarrow_{h}v$, and so also $(\lambda x.r)u\downarrow_{h}v$ in $\mathcal{P}_{h}$.

Finally, if $e\Downarrow^{c_{0}}_{\rho\to\tau,g}u$, $e^{\prime}\Downarrow^{c_{1}}_{\rho,g}v$ and $uv\Downarrow^{c_{2}}_{\tau,g}w$, then we have $e\downarrow_{g}u$, $e^{\prime}\downarrow_{g}v$ and $uv\downarrow_{g}w$ and thus $ee^{\prime}\downarrow_{g}w$. Now suppose that $g=_{c_{0}\ast c_{1}\ast c_{2}}h$. Then we have $g=_{c_{i}}h$ for $i=0,1,2$, and thus $e\downarrow_{h}u$, $e^{\prime}\downarrow_{h}v$ and $uv\downarrow_{h}w$ and therefore $ee^{\prime}\downarrow_{h}w$. This establishes $ee^{\prime}\Downarrow^{c_{0}\ast c_{1}\ast c_{2}}_{\tau}w$.

Our main soundness theorem gives rise in this case to the following continuity theorem.

Theorem 15**.**

Suppose that for all non-oracle function symbols of $f:\rho_{1}\to\ldots\to\rho_{n}\to\rho$ in the base language $\mathcal{P}$ and any $g:\mathbb{N}^{\mathbb{N}}$ we have $fv_{1}\ldots v_{k}\blacktriangleleft_{\rho,g}\overline{f}a_{1}\ldots a_{k}$ whenever $v_{i}\lhd_{\rho_{i},g}a_{i}$. Let $e:({\rm Nature}\to{\rm Nature})\to{\rm Nature}$ be a closed term of $\mathcal{P}$. Then we have

[TABLE]

for $(c,n):=\llbracket{|{e\alpha}|}\rrbracket_{g}$.

Proof 5.2**.**

By assumption the translation $\llbracket{|{\cdot}|}\rrbracket_{g}$ is sound with respect to $\blacktriangleleft_{g}$ for the function symbols of $\mathcal{P}$ (i.e. the non-oracle function symbols of $\mathcal{P}_{g}$) so to verify soundness of the extended language $\mathcal{P}_{g}$ it remains to check the oracle symbol $\alpha$. But for any $n\in\mathbb{N}$ we have

[TABLE]

and thus $\alpha\;\mathbf{n}\blacktriangleleft_{{\rm Nature},g}([n],g(n))=\overline{\alpha}_{g}(n)$. Therefore it follows that for any closed $e^{\prime}:\rho$ in $\mathcal{P}_{g}$ we have $e^{\prime}\blacktriangleleft_{\rho,g}\llbracket{|{e^{\prime}}|}\rrbracket_{g}$. In particular, for $e:({\rm Nature}\to{\rm Nature})\to{\rm Nature}$, setting $e^{\prime}:=e\alpha:{\rm Nature}$ we obtain $e\alpha\blacktriangleleft_{{\rm Nature},g}(c,n)$ for $(c,n):=\llbracket{|{e\alpha}|}\rrbracket_{g}$. But this just means that $e\alpha\Downarrow^{c}_{g}\mathbf{n}$, which is exactly what we want to show.

Corollary 16**.**

Theorem 15 holds for $\mathcal{P}^{T}$ (i.e. System T as defined in Section 2.1).

Proof 5.3**.**

We need to find a suitable interpretation of the recursors $\mathtt{rec}_{\rho}$ independent of $g$, to which end we define $\overline{\mathtt{rec}}_{\rho}$ by

[TABLE]

where $\circ$ is as defined in Lemma 3. Then using Lemma 3 together with induction it is straightforward to show that for any parameter $g$, whenever $v_{1}\lhd_{\rho,g}a$ and $v_{2}\lhd_{{\rm Nature}\to\rho\to\rho,g}f$ then $\mathtt{rec}\;v_{1}\;v_{2}\;\mathbf{n}\blacktriangleleft_{\rho,g}\overline{\mathtt{rec}}(a,f,n)$.

To see this, note that for the base case we have $\mathtt{rec}\;v_{1}\;v_{2}\;\mathtt{0}\downarrow_{g}v_{1}\lhd_{\rho,g}a$, and since for any $h$ it’s also the case that $\mathtt{rec}\;v_{1}\;v_{2}\;\mathtt{0}\downarrow_{h}v_{1}$ this implies that $\mathtt{rec}\;v_{1}\;v_{2}\;\mathtt{0}\Downarrow_{g}^{[]}v_{1}$ and thus $\mathtt{rec}\;v_{1}\;v_{2}\;\mathtt{0}\blacktriangleleft_{\rho,g}([],a)$.

For the induction step, by $v_{2}\lhd_{{\rm Nature}\to\rho\to\rho,g}f$ we have $v_{2}\;\mathbf{n}\blacktriangleleft_{\rho\to\rho,g}fn$ and by the induction hypothesis $\mathtt{rec}\;v_{1}\;v_{2}\;\mathbf{n}\blacktriangleleft_{\rho,g}\overline{\mathtt{rec}}(a,f,n)$. Therefore by Lemma 3 we have

[TABLE]

which implies that $v_{2}\;\mathbf{n}\;(\mathtt{rec}\;v_{1}\;v_{2}\;\mathbf{n})\Downarrow_{g}^{c}w\lhd_{\rho,g}r$ for $(c,r):=\overline{\mathtt{rec}}(a,f,n+1)$. But since by our operational semantics $v_{2}\;\mathbf{n}\;(\mathtt{rec}\;v_{1}\;v_{2}\;\mathbf{n})\downarrow_{h}w$ implies $\mathtt{rec}\;v_{1}\;v_{2}\;\mathtt{s}(\mathbf{n})\downarrow_{h}w$ for any $h$, it follows that $\mathtt{rec}\;v_{1}\;v_{2}\;\mathtt{s}(\mathbf{n})\Downarrow^{c}_{g}w$ and hence $\mathtt{rec}\;v_{1}\;v_{2}\;\mathtt{s}(\mathbf{n})\blacktriangleleft_{\rho,g}(c,r)$.

5.3. Continuity of functionals $\mathbb{N}^{\mathbb{N}}\to\mathbb{N}$ definable in System T

We now use the main theorem above to prove a more traditional formulation of the continuity of System T functionals, namely that any set-theoretic object $F:\mathbb{N}^{\mathbb{N}}\to\mathbb{N}$ which is definable in System T is continuous in the following sense:

[TABLE]

where we write $g=_{N}h$ if $g(i)=h(i)$ for all $i<N$. We first set up a connection between $\mathcal{P}^{T}$ and the usual formulation of System T as subset of the set theoretic type structure $\mathcal{S}^{\omega}$. {defi}

For each $\Gamma\vdash t:\rho$ in our target language $\mathcal{P}^{T}$ we define the usual semantic interpretation $[\Gamma]\vdash[t]:[\rho]$ in $\mathcal{S}^{\omega}$ as follows: $[{\rm Nature}]:=\mathbb{N}$ and $[\rho\to\tau]:=[\rho]\Rightarrow[\tau]$, and on terms:

[TABLE]

This interpretation then eliminates any difference between our formulation of System T as a call-by-value language and those based on equational calculi: An object of $\mathcal{S}^{\omega}$ is definable in System T precisely when it is of the form $[e]$ for some closed term $e$ in $\mathcal{P}^{T}$. We now extend the above definition to incorporate our oracle symbol. {defi} For each $g\in\mathbb{N}^{\mathbb{N}}$ and $\Gamma\vdash t:\rho$ in $\mathcal{P}^{T}_{g}$, we define $[\Gamma]_{g}\vdash[t]_{g}:[\rho]$ by extending the clauses of Definition 5.3 with

[TABLE]

It is easy to prove that if $t$ is a term of $\mathcal{P}^{T}_{g}$ which does not contain $\alpha$, then it is also a term of $\mathcal{P}^{T}$ and moreover $[t]_{g}\eta=[t]\eta$ for any $\eta$.

We now need a result which confirms that the pure interpretation $[\cdot]_{g}$ can be related to the semantic part of $\llbracket{|{\cdot}|}\rrbracket_{g}$.

Lemma 17**.**

Define the auxiliary logical relation $\sim_{\rho}$ on $[\rho]\times\llbracket{|{\rho}|}\rrbracket$ as follows:

[TABLE]

We write $\eta\sim_{\Gamma}\xi$ if $\eta(x)\sim_{\rho}\xi(x)$ for all $x:\rho\in\Gamma$. Then for any $g\in\mathbb{N}^{\mathbb{N}}$ and $\Gamma\vdash t$ in $\mathcal{P}^{T}_{g}$, if $\eta\sim_{\Gamma}\xi$ then we have $[t]_{g}\eta\sim_{\rho}\pi_{1}(\llbracket{|{t}|}\rrbracket_{g}\xi)$.

Proof 5.4**.**

A simple induction on terms. For variables this follows directly. For abstraction, if $a\sim_{\rho}b$ then

[TABLE]

and thus $[t]_{g}\eta\sim_{\rho\to\tau}\pi_{1}(\llbracket{|{\lambda x.t}|}\rrbracket_{g}\xi)$. For application, since $[t]_{g}\eta\sim_{\rho\to\tau}\pi_{1}(\llbracket{|{t}|}\rrbracket_{g}\xi)$ and $[s]_{g}\eta\sim_{\rho}\pi_{1}(\llbracket{|{s}|}\rrbracket_{g}\xi)$ we have $[ts]_{g}\eta\sim_{\rho}\pi_{1}(\pi_{1}(\llbracket{|{t}|}\rrbracket_{g}\xi)(\pi_{1}(\llbracket{|{s}|}\rrbracket_{g}\xi)))=\pi_{1}(\llbracket{|{ts}|}\rrbracket_{g}\xi)$. For the constants the result is trivial, and for the recursor we must show that

[TABLE]

for all $n\in\mathbb{N}$, which is a simple induction appealing to a variant of the argument used for application. Finally, for the oracle symbol, we must show that

[TABLE]

for any $n\in\mathbb{N}$, which is the case by definition.

Corollary 18**.**

Suppose $e:({\rm Nature}\to{\rm Nature})\to{\rm Nature}$ is a closed term of $\mathcal{P}^{T}$. Then for any $g\in\mathbb{N}^{\mathbb{N}}$ we have $\pi_{1}(\llbracket{|{e\alpha}|}\rrbracket_{g})=[e](g)$.

Proof 5.5**.**

If $e:({\rm Nature}\to{\rm Nature})\to{\rm Nature}$ is a closed term of $\mathcal{P}^{T}$ then in particular it can be viewed as a term of $\mathcal{P}^{T}_{g}$ which does not contain $\alpha$, and as such we have $[e]_{g}=[e]$. Since $[\alpha]_{g}=g$ by definition, by Lemma 17 we have $[e\alpha]_{g}=\pi_{1}(\llbracket{|{e\alpha}|}\rrbracket_{g})$ and thus

[TABLE]

and we are done.

Theorem 19**.**

Suppose that $F:\mathbb{N}^{\mathbb{N}}\to\mathbb{N}$ is definable in System T. Then

[TABLE]

where $\Phi$ is defined by

[TABLE]

for some closed term $e$ representing $F$.

Proof 5.6**.**

If $F$ is definable in System T, there is some closed term $e:({\rm Nature}\to{\rm Nature})\to{\rm Nature}$ of $\mathcal{P}^{T}$ such that for all $f\in\mathbb{N}^{\mathbb{N}}$ we have $[e](f)=F(f)$. Observing that

[TABLE]

we have $g=_{\Phi(g)}h$ implies that $g=_{\pi_{0}(\llbracket{|{e\alpha}|}\rrbracket_{g})}h$. Thus by Theorem 15, which by Corollary 16 applies to $\mathcal{P}^{T}$, we have $e\alpha\downarrow_{g}\mathbf{n}$ and $e\alpha\downarrow_{h}\mathbf{n}$ for $n=\pi_{1}(\llbracket{|{e\alpha}|}\rrbracket_{g})$, and by Corollary 18 we have $\pi_{1}(\llbracket{|{e\alpha}|}\rrbracket_{g})=[e](g)=F(g)$. Now, by Theorem 15 again, we have $e\alpha\downarrow_{h}\mathbf{m}$ where $m=\pi_{1}(\llbracket{|{e\alpha}|}\rrbracket_{h})$. But by uniqueness of derivations in $\mathcal{P}^{T}_{h}$, we therefore have $\mathbf{n}=\mathbf{m}$ and therefore $n=m=\pi_{1}(\llbracket{|{e\alpha}|}\rrbracket_{h})=[e](h)=F(h)$ and thus $F(g)=F(h)$.

We also note that the term $\llbracket{|{e}|}\rrbracket$ is, in turn, constructed using only basic operations of the lambda calculus, cartesian product and list operations, together with primitive recursion, and can thus also be defined in some suitable variant of System T.

This section demonstrates how our main result on continuity (Theorem 15) can be reformulated in terms of continuity of functionals $\mathbb{N}^{\mathbb{N}}\to\mathbb{N}$. It goes without saying that our approach throughout this section could be extended to other systems, such as extensions of System T with bar recursion, though we don’t go through any of the details here.

6. A denotational cost semantics

In our final application, we show how various denotational complexity semantics of functional languages can be re-obtained in a uniform way in our setting. As mentioned in the introduction, the static cost analysis of functional programs dates back to at least the 1980s [30, 34], and has been explored more recently in a generalised categorical setting [37] and from the perspective of automating the analysis of synthesised programs [1], though naturally these papers constitute just a few representative examples of the very diverse literature on complexity in higher types.

A distinguishing feature shared by each of the works mentioned above is that they view the complexity of a higher-order functional as a higher-order object in its own right, namely a cost functional which not only tracks the number of steps it takes for a higher-order term $t$ to reduce to a normal form $\lambda x.u$, but encodes information about the cost of evaluating $(\lambda x.u)v$ for any input $v$, and so on. The synthesis of cost functionals from higher-order programs in this sense is readily accomplished in our setting by instantiating the monadic part of our translation as a simple step counting operation. In particular, the result of our translation is an object $\llbracket{|{e}|}\rrbracket$ which is always given as recursive equation in our model which reflects the syntactic structure of the original term $e$. This recursive equation can then be solved to give a closed form expression for the cost of evaluating $e$ (see Example 6.1 for an illustration of this in the case of Spector’s search functional).

However, we also show that different choices of our semantic component lead to interesting characterisations of complexity. In particular, by combining the aforementioned cost operation with a form of majorizability similar to that discussed in Section 4.3, we obtain in a uniform way the bounded cost semantics explored recently by Danner et al. in [9, 10].

On top of all this, we apply our translation not just to variants of System T, as is often the case in the literature, but to bar recursive extensions, for which soundness of our cost analysis requires us to appeal to semantic continuity principles as in Section 4.2.

6.1. Exact cost expressions for call-by-value languages

We begin by defining what we mean by the cost of a closed term $e$ in our parametrised target language. We do this using annotated big step relations $e\downarrow^{c}v$ for $c\in\mathbb{N}$, where intuitively, $e\downarrow^{c}v$ iff $e\downarrow v$ in $c$ rewrite steps. We define this formally in Figure 7.

Throughout this section our main illustrative example will be our list based variant of System T from Section 2.2, together with its bar recursive extension from Section 2.3. As such, we formulate our soundness theorem (Theorem 20) in terms of an arbitrary target language over datatypes ${\rm Nature}$ and ${\rm Nature}^{\ast}$ with constructors $\mathtt{0}$, $\mathtt{s}$ $\varepsilon$ and $\;\mathtt{::}\;$, noting that both of the aforementioned languages follow as simple instances of this. Our monadic translation for exact costs is based on setting $C:=\mathbb{N}$ with $D_{\rm Nature}:=\mathbb{N}$ and $D_{{\rm Nature}^{\ast}}:=\mathbb{N}^{\ast}$, and we define our logical relation via

[TABLE]

and thus $\blacktriangleleft_{\rho}$ becomes

[TABLE]

For our denotational semantics of terms, we define the monadic components by

[TABLE]

and interpret our constructors in the obvious way, so that the interpretations are in particular compatible with $\lhd$. Note that it is clear from the definition of cost that $(\epsilon,\mathrm{inc},\mathrm{com})$ is compatible with $\Downarrow$. Thus our main soundness proof (Theorem 4) results in the following characterisation of costs in higher types.

Theorem 20**.**

Suppose that for each function symbol $f$ in our target language there is a suitable interpretation $\overline{f}$ such that $fv_{1}\ldots v_{k}\blacktriangleleft\overline{f}a_{1}\ldots a_{k}$ whenever $v_{i}\lhd_{\rho_{i}}a_{i}$. Then for any closed $e:\rho$ we have

[TABLE]

for some value $v:\rho$.

It is relatively straightforward to apply the metatheorem above to the full list based variant of System T, and even its extension with bar recursion. For our basic operators, we have e.g. $\mathbf{n}+\mathbf{m}\blacktriangleleft_{{\rm Nature}}(1,n+m)$ and $\mathtt{ext}\;\mathbf{a}\;\mathbf{n}\blacktriangleleft_{{\rm Nature}}(1,\hat{a}_{n})$, and so on. {defi} For $c\in\mathbb{N}$ and $a\in\mathbb{N}\times\rho$ define $c\mathbin{{+}\mspace{-8.0mu}{+}}a:=(c+\pi_{0}a,\pi_{1}a)\in\mathbb{N}\times\rho$.

Lemma 21**.**

1. (1)

We have $\mathtt{fold}\;v_{1}\;v_{2}\;\mathbf{a}\blacktriangleleft\overline{\mathtt{fold}}(b,h,a)$ for any $v_{1}\lhd b$, $v_{2}\lhd h$ and $a\in\mathbb{N}^{\ast}$, where $\overline{\mathtt{fold}}$ is defined by

[TABLE] 2. (2)

We have $\mathtt{bar}\;v_{1}\;v_{2}\;v_{3}\;\mathbf{a}\blacktriangleleft\overline{\mathtt{bar}}(\omega,g,h,a)$ for any $v_{1}\lhd\omega$, $v_{2}\lhd g$, $v_{3}\lhd h$ and $a\in\mathbb{N}^{\ast}$. where $\overline{\mathtt{bar}}$ is defined by

[TABLE]

for $\omega_{i}(f):=\pi_{i}(\omega(f))$.

Proof 6.1**.**

Part (a) is a simple induction on the length of $a$, observing that the derived rules for $\mathtt{fold}$ give rise to the following cost rules:

[TABLE]

For part (b), we work in the continuous model $\mathcal{C}^{\omega}$ as in Section 4.2 and follows the same strategy as the proof of Lemma 7. By keeping track of costs we see that that the derived operational semantics of bar recursion give rise to the following derived cost rules:

[TABLE]

To formally derive each of these rules involves a careful analysis of the defining rules of the bar recursor constants, along with the cost semantics as set out in Figure 7. For the first, note that from the defining equation

[TABLE]

we can infer $\mathtt{bar}_{1}\;v_{1}\;v_{2}\;v_{3}\;\mathbf{a}\;\mathtt{0}\downarrow^{1+c_{1}}\mathbf{n}$ from $v_{2}\;\mathbf{a}\downarrow^{c_{1}}\mathbf{n}$. Now if $k<|a|$ it follows that $(\mathbf{k}<\mathtt{len}\;\mathbf{a})\downarrow^{2}\mathtt{0}$, since this involves the reduction of two elementary operations, and thus $(v_{1}(\mathtt{ext}\;\mathbf{a})<\mathtt{len}\;\mathbf{a})\downarrow^{2+c_{0}}\mathtt{0}$ follows from $v_{1}(\mathtt{ext}\;\mathbf{a})\downarrow^{c_{0}}_{\rm Nature}\mathbf{k}$. Putting this all together we obtain

[TABLE]

and from the defining equation

[TABLE]

we derive $\mathtt{bar}\;v_{1}\;v_{2}\;v_{3}\;\mathbf{a}\downarrow^{4+c_{0}+c_{1}}\mathbf{n}$. The second derived rule is established in a similar manner. Now, continuing with the main proof, we first note that \mathtt{ext}\;\mathbf{a}\lhd_{{\rm Nature}\to{\rm Nature}}\mathop{\hbox to0.0pt{\lambda\hss}\mkern 2.0mu\raisebox{1.18399pt}{\lambda}}i.(1,\hat{a}_{i}), and thus since $v_{1}\lhd\omega$ it follows that v_{1}(\mathtt{ext}\;\mathbf{a})\blacktriangleleft_{\rm Nature}\omega(\mathop{\hbox to0.0pt{\lambda\hss}\mkern 2.0mu\raisebox{1.18399pt}{\lambda}}i.(1,\hat{a}_{i})) and thus $v_{1}(\mathtt{ext}\;\mathbf{a})\downarrow^{c_{0}}_{\rm Nature}\mathbf{k}$ with

[TABLE]

As in Lemma 7, we now assume inductively that

[TABLE]

for some fixed $a\in\mathbb{N}^{\ast}$ and all $n\in\mathbb{N}$, and seek to establish $\mathtt{bar}\;v_{1}\;v_{1}\;v_{2}\;\mathbf{a}\blacktriangleleft\overline{\mathtt{bar}}(\omega,g,h,a)$. There are two cases to deal with.

• •

Case 1: $k<|a|$. Observing that from $v_{2}\lhd g$ we have $v_{2}\;\mathbf{a}\downarrow^{c_{1}}\mathbf{n}$ for $(c_{1},n)=g(a)$, it follows that $\mathtt{bar}\;v_{1}\;v_{2}\;v_{3}\;\mathbf{a}\downarrow^{4+c_{0}+c_{1}}\mathbf{n}$ where $(4+c_{0}+c_{1},n)=(4+c_{0})\mathbin{{+}\mspace{-8.0mu}{+}}g(a)$.

• •

Case 2: $k\geq|a|$. By our assumption $(\ast)$ we have

[TABLE]

for $(c,m):=\overline{\mathtt{bar}}(\omega,g,h,a::n)$ and thus

[TABLE]

from which we can infer

[TABLE]

Since $v_{3}\lhd h$ we then have $v_{3}\;\mathbf{a}\blacktriangleleft ha$ and thus by Lemma 3 it follows that

[TABLE]

for (c_{1},n)=ha\circ(0,\mathop{\hbox to0.0pt{\lambda\hss}\mkern 2.0mu\raisebox{1.18399pt}{\lambda}}n\;.\;1\mathbin{{+}\mspace{-8.0mu}{+}}\overline{\mathtt{bar}}(\omega,g,h,a::n)). Therefore by the second derived rule we have $\mathtt{bar}\;v_{1}\;v_{2}\;v_{3}\;\mathbf{a}\downarrow^{4+c_{0}+c_{1}}\mathbf{n}$ where (4+c_{0}+c_{1},n)=(4+c_{0})\mathbin{{+}\mspace{-8.0mu}{+}}ha\circ(0,\mathop{\hbox to0.0pt{\lambda\hss}\mkern 2.0mu\raisebox{1.18399pt}{\lambda}}n\;.\;1\mathbin{{+}\mspace{-8.0mu}{+}}\overline{\mathtt{bar}}(\omega,g,h,a::n)).

Putting both cases together we see that $\mathtt{bar}\;v_{1}\;v_{1}\;v_{2}\;\mathbf{a}\blacktriangleleft\overline{\mathtt{bar}}(\omega,g,h,a)$ holds whenever $(\ast)$ holds. We now suppose as in Lemma 7 that it is not the case that $\mathtt{bar}\;v_{1}\;v_{2}\;v_{3}\;\mathbf{a}\blacktriangleleft\overline{\mathtt{bar}}(\omega,g,h,a)$, and construct an infinite sequence $b$ on the metalevel such that

[TABLE]

for all $l\in\mathbb{N}$. This time we apply a continuity argument to $\omega_{1}:(\mathbb{N}\to\mathbb{N}\times\mathbb{N})\to\mathbb{N}$ and the sequence \beta:=\mathop{\hbox to0.0pt{\lambda\hss}\mkern 2.0mu\raisebox{1.18399pt}{\lambda}}i.(1,(a\ast b)_{i}), by which there exists some $N$ such that

[TABLE]

for all $\gamma:\mathbb{N}\to\mathbb{N}\times\mathbb{N}$. In particular setting $L:=\max\{N,\omega_{1}(\beta)+1-|a|\}$ we have

[TABLE]

Thus for input $a\ast[{b}]({L})$ Case 1 applies and we have

[TABLE]

a contradiction. Therefore it must be the case that $\mathtt{bar}\;v_{1}\;v_{2}\;v_{3}\;\mathbf{a}\blacktriangleleft\overline{\mathtt{bar}}(\omega,g,h,a)$ for all $a\in\mathbb{N}^{\ast}$, which completes the proof.

Corollary 22**.**

Let $e:\rho$ be a closed term definable in System T plus bar recursion (in the sense of Section 2.3). Then $e\downarrow^{\pi_{0}\llbracket{|{e}|}\rrbracket}v$ for some value $v$.

{exa}

Consider the so-called Spector search functional $\Phi:((\mathbb{N}\to\mathbb{N})\to\mathbb{N})\to(\mathbb{N}\to\mathbb{N})\to\mathbb{N}$ given by

[TABLE]

This functional was introduced by Howard in [15], though he attributes it to Kreisel. The idea is that $\Phi(\omega,\beta,[])$ forms a bound on how far we need to look to find some $N$ such that $\omega(\widehat{[{\beta}]({N})})<N$, confirming that such an $N$ can be computed using bar recursion.

The search functional can be defined in our target language via the closed term

[TABLE]

Then given $v_{1}\blacktriangleleft\omega$ and $v_{2}\blacktriangleleft g$, it is not too difficult to work out that

[TABLE]

where $\phi$ is defined as

[TABLE]

Unwinding the defining equations of $\overline{\mathtt{bar}}$ we obtain

[TABLE]

We now solve the complexity component of these equations to find a closed form expression for the complexity of the search functional. For any function $f:\mathbb{N}\to\mathbb{N}$ and $n\in\mathbb{N}$ define $f^{n}:\mathbb{N}\to\mathbb{N}\times\mathbb{N}$ by

[TABLE]

We now consider $\phi_{0}(\omega,g,[{g_{1}}]({n}))$. In the case that $\omega_{1}(g_{1}^{n})<n$ we have

[TABLE]

and otherwise we have

[TABLE]

Putting these together we obtain

[TABLE]

We can then use this to expand $\phi_{0}(\omega,g,[])$ until we reach a point $N\in\mathbb{N}$ such that $\omega_{1}(g_{1}^{N})<N$. More precisely, if $N$ is the first such point, we have

[TABLE]

This then forms a closed expression for the cost $c$ of evaluating $\mathtt{spec}\;v_{1}\;v_{2}\;\varepsilon$ whenever $v_{1}\blacktriangleleft\omega$ and $v_{2}\blacktriangleleft g$. Note that this cost expression would be formally defined using the Spector search function itself, just as the cost expression for primitive recursion is also a primitive recursive functional.

6.2. Bounded costs

In the final part of the paper, we show how we can modify our denotational cost semantics to provide upper bounds on the cost of derivations, along the lines of [10], which is generalised to a richer language with recursion over arbitrary datatypes in [9]. The main motivation for looking for upper bounds (rather than a precise measure of complexity) is that it allows us to abstract away certain parts of the program (for instance, treating all number inputs as the same) and thereby obtain simplified expressions for the cost of programs. We now no longer denote a numeral $\mathbf{n}$ by the corresponding natural number $n$, but assign all numerals a uniform size $1$. Lists are then interpreted by a single natural number that represents an upper bound on their length. In this way, we sacrifice precision for a simplified upper bound on the cost of running a program.

To be more precise, while we still have $C=\mathbb{N}$ we alter the semantic side of our denotational semantics by setting $D_{\rm Nature}=D_{{\rm Nature}^{\ast}}=\mathbb{N}$, and adapt our logical relation so that

[TABLE]

and thus $\blacktriangleleft_{\rho}$ becomes

[TABLE]

It is easy to see that $\epsilon:=0$, $\mathrm{inc}(c):=c+1$ and $\mathrm{com}(c_{0},c_{1},c_{2}):=c_{0}+c_{1}+c_{2}$ as defined in Section 6.1 is also compatible with our new definition of $\Downarrow$. However, this time we must interpret our constructors differently: We set $\overline{\mathtt{0}}:=1$ and $\overline{\mathtt{s}}(n):=1$, so that $\llbracket{|{\mathbf{n}}|}\rrbracket=(0,1)$ for all $n\in\mathbb{N}$, and for lists we define $\overline{\varepsilon}:=0$ and $\overline{::}(m,n):=m+1$, so that $\llbracket{|{\mathbf{a}}|}\rrbracket=(0,|a|)$ for all $a\in\mathbb{N}^{\ast}$. In this way, we ensure that our constructors are compatible with $\lhd$, which then gives rise to the following metatheorem:

Theorem 23**.**

Suppose that each function symbol $f$ of our target language is interpreted by some suitable $\overline{f}$ which satisfies $fv_{1}\ldots v_{k}\blacktriangleleft\overline{f}a_{1}\ldots a_{k}$ whenever $v_{i}\lhd_{\rho_{i}}a_{i}$. Then for any closed $e:\rho$ we have

[TABLE]

and some value $v:\rho$.

We now demonstrate how this metatheorem can be applied to our list based variant of System T. In order to do this we need to generalise the usual maximum operator between two natural numbers to arbitrary types. {defi}

For types $\rho$ of our target language, define $\vee_{\rho}:\llbracket{|{\rho}|}\rrbracket\times\llbracket{|{\rho}|}\rrbracket\to\llbracket{|{\rho}|}\rrbracket$ inductively by

[TABLE]

Lemma 24**.**

For all types $\rho$, if $u\lhd_{\rho}a$ then $u\lhd_{\rho}a\vee_{\rho}b$ and $u\lhd_{\rho}b\vee_{\rho}a$ for any $b\in\llbracket{|{\rho}|}\rrbracket$.

Proof 6.2**.**

Induction on types. We only prove $u\lhd a\vee b$ because the other way round is identical. For base types $\mathbf{n}\lhd m$ implies $1\leq m$, but since then $1\leq\max\{m,k\}$ we have $\mathbf{n}\lhd m\vee_{\rm Nature}k$. Similarly for lists: $\mathbf{a}\lhd_{{\rm Nature}^{\ast}}m$ implies $|a|\leq m\leq\max\{m,k\}$ and thus $\mathbf{a}\lhd_{{\rm Nature}^{\ast}}m\vee_{{\rm Nature}^{\ast}}k$.

For function types, suppose that $u\lhd_{\rho\to\tau}f$, which means that for any $v\lhd_{\rho}a$ we have $uv\downarrow^{c}w$ for some $c,w$ with $c\leq f_{0}a$ and $w\lhd_{\tau}f_{1}a$. But $c\leq\max\{f_{0}a,g_{0}a\}$ and by the induction hypothesis $w\lhd_{\tau}f_{1}a\vee_{\tau}g_{1}a$, and since $v,a$ were arbitrary we have $u\lhd_{\rho\to\tau}f\vee_{\rho\to\tau}g$.

Lemma 25**.**

We have $\mathtt{fold}\;v_{1}\;v_{2}\;\mathbf{a}\blacktriangleleft\overline{\mathtt{fold}}(b,h,n)$ for any $v_{1}\lhd b$, $v_{2}\lhd h$ and $a\in\mathbb{N}^{\ast}$ with $|a|\leq n$, where $\overline{\mathtt{fold}}$ is defined by

[TABLE]

Proof 6.3**.**

Induction on $n$. If $n=0$ then we must have $\mathbf{a}=[]$, and since $v_{1}\downarrow^{0}v_{1}\lhd_{\rho}a$ we have $\mathtt{fold}\;v_{1}\;v_{2}\;[]\downarrow^{1}v_{1}\lhd a$ and thus $\mathtt{fold}\;v_{1}\;v_{2}\;[]\blacktriangleleft_{\rho}(1,a)$.

For $n=n^{\prime}+1$ there are two possibilities. Either $\mathbf{a}=[]$ and $\mathtt{fold}\;v_{1}\;v_{2}\;[]\downarrow^{1}_{\rho}v_{1}\lhd a$ as before, and since $1\leq 1\mathbin{{+}\mspace{-8.0mu}{+}}h1\circ\overline{\mathtt{fold}}_{0}(a,h,n^{\prime})$ and (by Lemma 24) $v_{1}\lhd a\vee_{\rho}h1\circ\overline{\mathtt{fold}}_{1}(a,h,n^{\prime})$ we’re done. Otherwise $\mathbf{a}=\mathbf{a^{\prime}}::\mathbf{m}$. By the induction hypothesis we have $\mathtt{fold}\;v_{1}\;v_{2}\;\mathbf{a}^{\prime}\blacktriangleleft_{\rho}\overline{\mathtt{fold}}(a,h,n^{\prime})$, and since $\mathbf{m}\lhd_{\rm Nature}1$ and thus $v_{2}\;\mathbf{m}\blacktriangleleft_{\rho\to\rho}h1$ we have (by Lemma 3) $v_{2}\;\mathbf{m}\;(\mathtt{fold}\;v_{1}\;v_{2}\;\mathbf{a^{\prime}})\blacktriangleleft h1\circ\overline{\mathtt{fold}}(a,h,n^{\prime})$ which is just

[TABLE]

for $(c,b)=h1\circ\overline{\mathtt{fold}}(a,h,n^{\prime})$, and therefore

[TABLE]

Thus $\mathtt{fold}\;v_{1}\;v_{2}\;\mathbf{a}^{\prime}::\mathbf{m}\lhd\overline{\mathtt{fold}}(a,h,n^{\prime}+1)$ follows from another application of Lemma 24, and we’re done.

As a result of the above lemma, we obtain soundness of the translation for our list based variant of System T, which is analogous to Corollary 3 of [10]:

Corollary 26**.**

Let $e:\rho$ be a closed term of our list-based variant of System T. Then $e\downarrow^{c}v$ for some value $v$ and $c\leq\pi_{0}\llbracket{|{e}|}\rrbracket$.

Naturally, our approach can also be applied to arbitrary rewrite systems whose function symbols have a suitable interpretation, such as forms of recursion over more general data structures, as in [9]. Though the usual formulation of bar recursion does not have a bounded semantics of this kind, we could consider finite variants along the lines of [13, 25].

7. Conclusion

We have introduced a general monadic translation acting on higher-order functional languages, which combines both a monadic component and a semantic component, where the latter could play the role of a normal denotational semantics, or alternatively something more interesting, such a variant of the majorizability relation. Applications of our translation included a proof that functionals of type level two expressible by closed terms in our language are continuous, together with various denotational cost semantics for functional languages. The emphasis throughout was less on obtaining new results, and more on demonstrating that ideas from a range of different areas - from proof theory to static program analysis - can be brought together under the same framework. Nevertheless, as a side product we presented for the first time a cost analysis of Spector’s variant of bar recursion.

So far, our work only applies to functional languages whose function symbols give rise to terminating computations. An obvious next step would be to incorporate partiality into our setting, allowing us to reason about potentially non-terminating computations. In the context of normalization via denotational semantics (discussed here in Section 4.2), this has been explored in more generality by Berger [5], where a term $e$ is shown to be strongly normalizing if $\llbracket{e}\rrbracket\neq\bot$, where now $\llbracket{\cdot}\rrbracket$ represents a so-called strict denotational semantics. This approach also appeals to the notion of a stratified rewrite system, where function symbols $f$ are labelled with natural numbers in order to track the number of times they can be rewritten. A similar extension of Danner et al’s complexity framework to arbitrary PCF programs is given in [18]. It would be interesting to see if an approach along these lines, using stratified rewrite systems together with a partial denotational semantics, could be used to extend our framework to arbitrary PCF programs, without requiring the user to first prove that function symbols have a suitable interpretation.

There is also, naturally, the prospect of working with other monads and modelling other evaluation strategies, such as parallel computation. However, our simple call-by-value framework based on the writer monad is already rich enough to reason about extensional properties such as majorizability and continuity, and in addition allows us to characterise a variety of cost measures for higher order functional programs.

Acknowledgment

I am extremely grateful to the anonymous referee for their insightful comments and careful reading of the paper, which led to a much improved final version.