16317 LABEL:LastPageSep. 05, 2019Sep. 09, 2020

# A unifying framework for continuity and complexity in higher types

Thomas Powell  Department of Computer Science, University of Bath, Bath, BA2
7AY, United Kingdom<EMAIL_ADDRESS>
###### 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 $({\rm Nature}\to{\rm
Nature})\to{\rm Nature}$ in (extensions of) System T, and (ii) a
characterisation of the time complexity of bar recursion.

###### Key words and phrases:

functional languages, logical relations, denotational semantics, bar recursion

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

$\displaystyle\mbox{Types:}\ \ \ \rho,\tau::=\delta\;|\;\rho\to\tau\ \ \
\mbox{for}\ \ \ \delta\in\mathtt{datatype}$ $\displaystyle\mbox{Terms:}\ \ \
s,t::=x\;|\;c\;|\;f\;|\;\lambda x.t\;|\;ts\ \ \ \mbox{for}\ \ \
c\in\mathtt{cons},f\in\mathtt{func}$ $\displaystyle\Gamma,x:\rho\vdash x:\rho\
\ \ \ \ \ \frac{\Gamma,x:\rho\vdash t:\tau}{\Gamma\vdash\lambda
x.t:\rho\to\tau}\ \ \ \ \ \ \frac{\Gamma\vdash t:\rho\to\tau\ \ \ \
\Gamma\vdash s:\rho}{\Gamma\vdash ts:\tau}$ $\displaystyle\Gamma\vdash
c:\delta_{1}\to\ldots\to\delta_{m}\to\delta\ \ \ \ \ \ \Gamma\vdash
f:\rho_{1}\to\ldots\to\rho_{n}\to\rho$ Figure 1. Types and terms of target
language

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

$\displaystyle\mbox{Patterns:}\ \ \ p,q::=x^{\rho}\;|\;cp_{1}\ldots p_{k}\ \ \
\mbox{for}\ \ \ k=\mathrm{ar}(c)$ $\displaystyle\mbox{Values:}\ \ \
u,v::=cv_{1}\ldots v_{i}\;|\;fv_{1}\ldots v_{j}\;|\;\lambda x.r\ \ \
\mbox{for}\ \ \ i\leq\mathrm{ar}(c),\ j<\mathrm{ar}(f),\ x:\rho\vdash r$
Figure 2. Patterns and values

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

$\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}$ Figure 3. Operational semantics of target
language

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

$fp_{1}\ldots p_{k}\leadsto r$

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

$\frac{\Gamma\vdash t_{1}:\rho_{1}\ \ \ \cdots\ \ \ \Gamma\vdash
t_{n}:\rho_{n}}{\Gamma\vdash ft_{1}\ldots t_{n}:\rho}$

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

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

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

$\mathtt{rec}_{\rho}\;x\;y\;\mathtt{0}\leadsto x\ \ \ \ \ \
\mathtt{rec}\;x\;y\;(\mathtt{s}z)\leadsto
y\;z\;(\mathtt{rec}_{\rho}\;x\;y\;z).$

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:

$\mathtt{rec}_{\rho}\;v_{1}\;v_{2}\;\mathtt{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}v\ \ \ \ \ \
uv\downarrow_{\rho}w}{\mathtt{rec}_{\rho}\;v_{1}\;v_{2}\;\mathtt{s}(\mathbf{n})\downarrow_{\rho}w}$

###  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

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

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:

$\mathtt{fold}_{\rho}\;x\;y\;\varepsilon\leadsto x\ \ \ \ \ \
\mathtt{fold}_{\rho}\;x\;y\;(zs\;\mathtt{::}\;z)\leadsto
y\;z\;(\mathtt{fold}_{\rho}\;x\;y\;zs)$

which gives rise to the derived rules

$\mathtt{fold}_{\rho}\;v_{1}\;v_{2}\;\varepsilon\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}v\ \ \ \ \ \
uv\downarrow_{\rho}w}{\mathtt{fold}_{\rho}\;v_{1}\;v_{2}\;(\mathbf{a}::\mathbf{n})\downarrow_{\rho}w}$

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

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

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

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

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

$\displaystyle\mathtt{ext}$ $\displaystyle:{\rm Nature}^{\ast}\to{\rm
Nature}\to{\rm Nature}$ $\displaystyle\mathtt{bar}$
$\displaystyle:\rho_{1}\to\rho_{2}\to\rho_{3}\to{\rm Nature}^{\ast}\to{\rm
Nature}$ $\displaystyle\mathtt{bar}_{1}$
$\displaystyle:\rho_{1}\to\rho_{2}\to\rho_{3}\to{\rm Nature}^{\ast}\to{\rm
Nature}\to{\rm Nature}$

where

$\displaystyle\rho_{1}$ $\displaystyle:=({\rm Nature}\to{\rm Nature})\to{\rm
Nature}$ $\displaystyle\rho_{2}$ $\displaystyle:={\rm Nature}^{\ast}\to{\rm
Nature}$ $\displaystyle\rho_{3}$ $\displaystyle:={\rm Nature}^{\ast}\to({\rm
Nature}\to{\rm Nature})\to{\rm Nature}$

which have defining equations

$\displaystyle\mathtt{ext}\;[x_{1},\ldots,x_{k}]\;\mathbf{n}$
$\displaystyle\leadsto\begin{cases}x_{n}&\mbox{if $n<k$}\\\
\mathtt{0}&\mbox{otherwise}\end{cases}$
$\displaystyle\mathtt{bar}\;f\;g\;h\;xs$
$\displaystyle\leadsto\mathtt{bar}_{1}\;f\;g\;h\;xs\;(f(\mathtt{ext}\;xs)<\mathtt{len}\;xs)$
$\displaystyle\mathtt{bar}_{1}\;f\;g\;h\;xs\;\mathtt{0}$
$\displaystyle\leadsto g\;xs$
$\displaystyle\mathtt{bar}_{1}\;f\;g\;h\;xs\;\mathtt{s}z$
$\displaystyle\leadsto h\;xs\;(\lambda x\;.\;\mathtt{bar}\;f\;g\;h\;(xs::x))$

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

$\displaystyle\frac{v_{1}(\mathtt{ext}\;\mathbf{a})\downarrow_{\rm
Nature}\mathbf{k}\ \ \ \ \ \ k<|a|\ \ \ \ \ \ v_{2}\;\mathbf{a}\downarrow_{\rm
Nature}\mathbf{n}}{\mathtt{bar}\;v_{1}\;v_{2}\;v_{3}\;\mathbf{a}\downarrow\mathbf{n}}$
$\displaystyle\frac{v_{1}(\mathtt{ext}\;\mathbf{a})\downarrow_{\rm
Nature}\mathbf{k}\ \ \ \ \ \ k\geq|a|\ \ \ \ \ \ v_{3}\;\mathbf{a}\;(\lambda
x\;.\;\mathtt{bar}\;v_{1}\;v_{2}\;v_{3}\;(\mathbf{a}::x))\downarrow_{\rm
Nature}\mathbf{n}}{\mathtt{bar}\;v_{1}\;v_{2}\;v_{3}\;\mathbf{a}\downarrow_{\rm
Nature}\mathbf{n}}$

######  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.

$\displaystyle\mbox{Types:}\ \ \
\rho,\tau::=\gamma\;|\;|{\delta}|\;|\;\rho\times\tau\;|\;\rho\to\tau\ \ \
\mbox{for}\ \ \ \delta\in\mathtt{datatype}$ $\displaystyle\mbox{Terms:}\ \ \
r,s,t::=\iota\;|\;{t}_{+}\;|\;\\{{r},{s},{t}\\}\;|\;x\;|\;\langle{c}\rangle\;|\;\langle{f}\rangle\;|\;\lambda
x.t\;|\;ts\;|\;(s,t)\;|\;t_{l}\;|\;t_{r}\ \ \mbox{for}\ \ \
c\in\mathtt{cons},f\in\mathtt{func}$ $\displaystyle\Gamma\vdash\iota:\gamma\ \
\ \ \ \ \frac{\Gamma\vdash t:\gamma}{\Gamma\vdash{t}_{+}:\gamma}\ \ \ \ \ \
\frac{\Gamma\vdash r:\gamma\ \ \ \Gamma\vdash s:\gamma\ \ \ \Gamma\vdash
t:\gamma}{\Gamma\vdash\\{{r},{s},{t}\\}:\gamma}$
$\displaystyle\frac{\Gamma\vdash s:\rho\ \ \ \Gamma\vdash
t:\tau}{\Gamma\vdash(s,t):\rho\times\tau}\ \ \ \ \ \ \frac{\Gamma\vdash
t:\rho\times\tau}{\Gamma\vdash t_{l}:\rho}\ \ \ \ \ \ \frac{\Gamma\vdash
t:\rho\times\tau}{\Gamma\vdash t_{r}:\tau}$
$\displaystyle\Gamma\vdash\langle{c}\rangle:|{\delta_{1}}|\to\ldots\to|{\delta_{m}}|\to|{\delta}|\
\ \ \ \ \
\Gamma\vdash\langle{f}\rangle:|{\rho_{1}}|\to\ldots\to|{\rho_{n}}|\to\gamma\times|{\rho}|$
Figure 4. Types and terms of metalanguage

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

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

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

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

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

$\displaystyle\Gamma\vdash t:\rho$
$\displaystyle\mapsto|{\Gamma}|\vdash|{t}|:\gamma\times|{\rho}|$
$\displaystyle|{x}|$ $\displaystyle:=(\iota,x)$ $\displaystyle|{\lambda x.t}|$
$\displaystyle:=\lambda^{\ast}x\;.\;({|{t}|_{l}}_{+},|{t}|_{r})$
$\displaystyle|{ts}|$
$\displaystyle:=(\\{{|{t}|_{l}},{|{s}|_{l}},{(|{t}|_{r}|{s}|_{r})_{l}}\\},(|{t}|_{r}|{s}|_{r})_{r})$
$\displaystyle|{c}|$
$\displaystyle:=\lambda^{\ast}x_{1},\ldots,x_{m}\;.\;(\iota,\langle{c}\rangle
x_{1}\ldots x_{m})$ $\displaystyle|{f}|$
$\displaystyle:=\lambda^{\ast}x_{1},\ldots,x_{n}\;.\;\langle{f}\rangle
x_{1}\ldots x_{n}$ Figure 5. Translation from target to metalanguage

###  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]

$\llbracket{\gamma}\rrbracket:=C\ \ \ \ \ \
\llbracket{|{\delta}|}\rrbracket:=D_{\delta}\ \ \ \ \ \
\llbracket{\rho\times\tau}\rrbracket:=\llbracket{\rho}\rrbracket\times\llbracket{\tau}\rrbracket\
\ \ \ \ \
\llbracket{\rho\to\tau}\rrbracket:=\llbracket{\rho}\rrbracket\Rightarrow\llbracket{\tau}\rrbracket$

$\displaystyle\llbracket{\iota}\rrbracket\xi$ $\displaystyle:=\epsilon$
$\displaystyle\llbracket{{t}_{+}}\rrbracket\xi$
$\displaystyle:=\mathrm{inc}(\llbracket{t}\rrbracket\xi)$
$\displaystyle\llbracket{\\{{r},{s},{t}\\}}\rrbracket\xi$
$\displaystyle:=\mathrm{com}(\llbracket{r}\rrbracket\xi,\llbracket{s}\rrbracket\xi,\llbracket{t}\rrbracket\xi)$
$\displaystyle\llbracket{x}\rrbracket\xi$ $\displaystyle:=\xi(x)$
$\displaystyle\llbracket{\langle{c}\rangle}\rrbracket\xi$
$\displaystyle:=\overline{c}$
$\displaystyle\llbracket{\langle{f}\rangle}\rrbracket\xi$
$\displaystyle:=\overline{f}$ $\displaystyle\llbracket{\lambda
x.t}\rrbracket\xi$ $\displaystyle:=\mathop{\hbox to0.0pt{$\lambda$\hss}\mkern
2.0mu\raisebox{1.18399pt}{$\lambda$}}a.\llbracket{t}\rrbracket\xi\\{x\mapsto
a\\}$ $\displaystyle\llbracket{ts}\rrbracket\xi$
$\displaystyle:=\llbracket{t}\rrbracket\xi(\llbracket{s}\rrbracket\xi)$
$\displaystyle\llbracket{(s,t)}\rrbracket\xi$
$\displaystyle:=(\llbracket{s}\rrbracket\xi,\llbracket{t}\rrbracket\xi)$
$\displaystyle\llbracket{t_{l}}\rrbracket\xi$
$\displaystyle:=\pi_{0}(\llbracket{t}\rrbracket\xi)$
$\displaystyle\llbracket{t_{r}}\rrbracket\xi$
$\displaystyle:=\pi_{1}(\llbracket{t}\rrbracket\xi)$

Figure 6. Denotational semantics of metalanguage

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

$\Downarrow_{\rho}$ on $\mathtt{Cl}_{\rho}\times C\times\mathtt{Val}_{\rho}$
and $\lhd_{\delta}$ on
$\mathtt{Val}_{\delta}\times\llbracket{|{\delta}|}\rrbracket$,

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

$u\lhd_{\rho\to\tau}f:\Leftrightarrow(\forall
v\in\mathtt{Val}_{\rho},a\in\llbracket{|{\rho}|}\rrbracket)(v\lhd_{\rho}a\Rightarrow
uv\blacktriangleleft_{\tau}f(a))$

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

$e\blacktriangleleft_{\rho}a:\Leftrightarrow(\exists
v\in\mathtt{Val}_{\rho})(e\Downarrow^{\pi_{0}a}_{\rho}v\wedge
v\lhd_{\rho}\pi_{1}a),$

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

$\sigma\lhd_{\Gamma}\xi\Rightarrow
t\sigma\blacktriangleleft_{\rho}\llbracket{|{t}|}\rrbracket\xi$

for all $\sigma,\xi$. We start by focusing on the monadic part of our
relation. We say that $(\epsilon,\mathrm{inc},\mathrm{com})$ is compatible
with $\Downarrow$ if the following rules are satisfied:

$\displaystyle v\Downarrow^{\epsilon}_{\rho}v\mbox{ \ \ for values $v$}$
$\displaystyle\frac{r[u/x]\Downarrow^{c}_{\tau}v}{(\lambda
x.r)u\Downarrow^{\mathrm{inc}(c)}_{\tau}v}\mbox{ \ \ for $x:\rho\vdash r$ and
$u:\rho$ a value}$ $\displaystyle\frac{e\Downarrow^{c_{0}}_{\rho\to\tau}u\ \ \
\ \ e^{\prime}\Downarrow^{c_{1}}_{\rho}v\ \ \ \ \ \
uv\Downarrow^{c_{2}}_{\tau}w}{ee^{\prime}\Downarrow^{\mathrm{com}(c_{0},c_{1},c_{2})}_{\tau}w}$

######  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

$f\circ
a:=(\mathrm{com}(\pi_{0}f,\pi_{0}a,\pi_{0}((\pi_{1}f)(\pi_{1}a))),\pi_{1}((\pi_{1}f)(\pi_{1}a)))\in
C\times\llbracket{|{\tau}|}\rrbracket.$

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

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

$cv_{1}\blacktriangleleft\llbracket{\lambda^{\ast}x_{2},\ldots,x_{m}.(\iota,\langle{c}\rangle
x_{1}\ldots x_{m})}\rrbracket\\{x_{1}\mapsto a_{1}\\}.$

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

$cv_{1}\ldots v_{m}\blacktriangleleft\llbracket{(\iota,\langle{c}\rangle
x_{1}\ldots x_{m})}\rrbracket\\{x_{1},\ldots,x_{m}\mapsto a_{1},\ldots
a_{m}\\}=(\epsilon,\bar{c}a_{1}\ldots a_{m})$

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

$(ts)\sigma=(t\sigma)(s\sigma)\blacktriangleleft_{\tau}\llbracket{|{t}|}\rrbracket\xi\circ\llbracket{|{s}|}\rrbracket\xi=\llbracket{|{ts}|}\rrbracket\xi$

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

$(\lambda x.t)\sigma=(\lambda
x.t\sigma)\blacktriangleleft_{\rho\to\tau}\llbracket{\lambda^{\ast}x\;.\;({|{t}|_{l}}_{+},|{t}|_{r})}\rrbracket\xi=(\epsilon,\mathop{\hbox
to0.0pt{$\lambda$\hss}\mkern
2.0mu\raisebox{1.18399pt}{$\lambda$}}a\;.\;(\mathrm{inc}(\pi_{0}(\llbracket{|{t}|}\rrbracket\xi_{a})),\pi_{1}(\llbracket{|{t}|}\rrbracket\xi_{a})))$

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

$(\lambda
x.t\sigma)u\Downarrow_{\tau}^{\mathrm{inc}(\pi_{0}(\llbracket{|{t}|}\rrbracket\xi_{a}))}v\lhd_{\tau}\pi_{1}(\llbracket{|{t}|}\rrbracket\xi_{a})$

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

$t\sigma\\{x\mapsto
u\\}=t\sigma[u/x]\Downarrow_{\tau}^{\pi_{0}(\llbracket{|{t}|}\rrbracket\xi_{a})}v\lhd_{\tau}\pi_{1}(\llbracket{|{t}|}\rrbracket\xi_{a})$

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

$e\Downarrow_{\rho}^{0}v:\Leftrightarrow e\downarrow v$

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

$v\lhd_{\delta}0:\Leftrightarrow\mathsf{T}.$

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

$R_{\delta}(e)\Leftrightarrow(\exists v)(e\downarrow v)\ \ \ \ \ \
R_{\rho\to\tau}(e):\Leftrightarrow(\exists u)(e\downarrow u\wedge(\forall
v)(R^{\scriptsize{\mathrm{val}}}_{\rho}(v)\Rightarrow R_{\tau}(uv)))$

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

$R^{\scriptsize{\mathrm{val}}}_{\rho_{1}}(v_{1})\wedge\ldots\wedge
R^{\scriptsize{\mathrm{val}}}_{\rho_{n}}(v_{n})\Rightarrow
R_{\rho}(fv_{1}\ldots v_{n})$

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

$R^{\scriptsize{\mathrm{val}}}_{\rho}(v_{1})\wedge
R^{\scriptsize{\mathrm{val}}}_{{\rm Nature}\to\rho\to\rho}(v_{2})\Rightarrow
R_{\rho}(\mathtt{rec}_{\rho}\;v_{1}\;v_{2}\;\mathbf{n})$

(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

$\llbracket{|{\rho\to\tau}|}\rrbracket=\llbracket{|{\rho}|}\rrbracket\Rightarrow\\{0\\}\times\llbracket{|{\tau}|}\rrbracket\cong\llbracket{|{\rho}|}\rrbracket\Rightarrow\llbracket{|{\tau}|}\rrbracket$

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:

$\mathbf{n}\lhd_{\rm Nature}m:\Leftrightarrow n=m\ \ \ \ \ \
\mathbf{a}\lhd_{{\rm Nature}^{\ast}}b:\Leftrightarrow a=b,$

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

$\displaystyle e\blacktriangleleft_{\rho}a$
$\displaystyle:\Leftrightarrow(\exists v)(e\downarrow v\wedge v\lhd_{\rho}a)$
$\displaystyle u\lhd_{\rho\to\tau}f$ $\displaystyle:\Leftrightarrow(\forall
v,a)(v\lhd_{\rho}a\Rightarrow uv\blacktriangleleft_{\tau}f(a)).$

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

$\overline{0}:=0\ \ \ \ \ \ \overline{\mathtt{s}}(n):=n+1\ \ \ \ \ \
\overline{\varepsilon}:=[]\ \ \ \ \ \ \overline{::}(a,n):=a\ast n$

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.

$\overline{\mathtt{len}}(a):=|a|\ \ \ \ \ \
\overline{\mathtt{ext}}(a):=\hat{a}.$

Finally, for bar recursion we let

$\displaystyle\overline{\mathtt{bar}}(\omega,g,h,a)$
$\displaystyle=\begin{cases}g(a)&\mbox{if $\omega(\hat{a})<|a|$}\\\
h(a,\mathop{\hbox to0.0pt{$\lambda$\hss}\mkern
2.0mu\raisebox{1.18399pt}{$\lambda$}}x\;.\;\overline{\mathtt{bar}}(\omega,g,h,a\ast
x))&\mbox{otherwise}\end{cases}$

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

$\displaystyle\mathtt{bar}\;v_{1}\;v_{2}\;v_{3}\;\mathbf{a}\blacktriangleleft_{\rm
Nature}\overline{\mathtt{bar}}(\omega,g,h,a).$

######  Proof 4.2.

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

$(\ast)\ \ \
\mathtt{bar}\;v_{1}\;v_{2}\;v_{3}\;\mathbf{a}::\mathbf{n}\blacktriangleleft_{\rm
Nature}\overline{\mathtt{bar}}(\omega,g,h,a\ast n)$

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

$(\mathtt{bar}\;v_{1}\;v_{2}\;v_{3}\;\mathbf{a}::x)[\mathbf{n}/x]\blacktriangleleft_{\rm
Nature}\overline{\mathtt{bar}}(\omega,g,h,a::x)\\{x\mapsto n\\}$

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

$\lambda x\;.\;\mathtt{bar}\;v_{1}\;v_{2}\;v_{3}\;\mathbf{a}::x\lhd_{{\rm
Nature}\to{\rm Nature}}\mathop{\hbox to0.0pt{$\lambda$\hss}\mkern
2.0mu\raisebox{1.18399pt}{$\lambda$}}x\;.\;\overline{\mathtt{bar}}(\omega,g,h,a::x).$

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

$v_{3}\;\mathbf{a}\;(\lambda
x\;.\;\mathtt{bar}\;v_{1}\;v_{2}\;v_{3}\;\mathbf{a}::x)\blacktriangleleft_{\rm
Nature}h(a,\mathop{\hbox to0.0pt{$\lambda$\hss}\mkern
2.0mu\raisebox{1.18399pt}{$\lambda$}}x\;.\;\overline{\mathtt{bar}}(\omega,g,h,a::x))$

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

$\neg(\mathtt{bar}\;v_{1}\;v_{2}\;v_{3}\;(\mathbf{a}::\mathbf{b}_{0}::\cdots::\mathbf{b}_{l-1})\blacktriangleleft\overline{\mathtt{bar}}(\omega,g,h,a\ast[{b}]({l})))$

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

$\omega(\widehat{a\ast[{b}]({L})})<|a|+L$

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

$\mathtt{bar}\;v_{1}\;v_{2}\;v_{3}\;(\mathbf{a}::\mathbf{b}_{0}::\cdots::\mathbf{b}_{L-1})\blacktriangleleft\overline{\mathtt{bar}}(\omega,g,h,a\ast[{b}]({L}))$

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

$\mathbf{n}\lhd_{\rm Nature}m:\Leftrightarrow n\leq m.$

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])

$\displaystyle x^{\ast}\;\mathrm{maj}_{{\rm Nature}}\;x$
$\displaystyle:\Leftrightarrow x^{\ast}\geq x$ $\displaystyle
x^{\ast}\;\mathrm{maj}_{\rho\to\tau}\;x$ $\displaystyle:\Leftrightarrow\forall
y^{\ast},y(y^{\ast}\;\mathrm{maj}_{\rho}\;y\Rightarrow
x^{\ast}y^{\ast}\;\mathrm{maj}_{\tau}\;xy).$

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:

$\displaystyle e\blacktriangleleft_{\rm Nature}m$
$\displaystyle\Leftrightarrow(\exists
n\in\mathbb{N})(e\downarrow\mathbf{n}\wedge n\leq m)$ $\displaystyle
e\blacktriangleleft_{\rho\to\tau}f$ $\displaystyle\Leftrightarrow(\exists
u)(e\downarrow u\wedge(\forall v,a)(v\lhd_{\rho}a\Rightarrow(\exists
w)(uv\downarrow w\lhd_{\tau}f(a)))).$

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

$x^{\ast}\;\mathrm{maj}_{{\rm Nature}\to{\rm
Nature}}\;x:\Leftrightarrow\forall y^{\ast},y(y^{\ast}\geq y\Rightarrow
x^{\ast}y^{\ast}\geq xy)$

whereas in our setting this would be rendered as

$e\blacktriangleleft_{{\rm Nature}\to{\rm Nature}}f\Leftrightarrow(\exists
u)(e\downarrow u\wedge(\forall n,m)(n\leq m\Rightarrow(\exists
k)(u\mathbf{n}\downarrow\mathbf{k}\wedge k\leq fm))).$

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

$e\blacktriangleleft_{\rho}g\Leftrightarrow(\forall
v_{1},a_{1},\ldots,v_{n},a_{n})\left(\bigwedge_{i=1}^{n}v_{i}\lhd
a_{i}\Rightarrow(\exists k)(ev_{1}\ldots v_{n}\downarrow\mathbf{k}\wedge k\leq
g(a_{1},\ldots,a_{n}))\right)$

######  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

$\displaystyle e\blacktriangleleft g$ $\displaystyle\Leftrightarrow$
$\displaystyle(\exists u)(e\downarrow u\wedge(\forall v_{0},a_{0})(v_{0}\lhd
a_{0}\Rightarrow uv_{0}\blacktriangleleft g(a_{0}))$
$\displaystyle\Leftrightarrow$ $\displaystyle(\exists u)(e\downarrow
u\wedge(\forall v_{0},a_{0},\ldots v_{n},a_{n})(\bigwedge_{i=0}^{n}v_{i}\lhd
a_{i}\Rightarrow(\exists k)(uv_{0}\ldots v_{n}\downarrow\mathbf{k}\wedge k\leq
g(a_{0},\ldots a_{n})))$ $\displaystyle\Leftrightarrow$ $\displaystyle(\forall
v_{0},a_{0},\ldots v_{n},a_{n})(\bigwedge_{i=0}^{n}v_{i}\lhd
a_{i}\Rightarrow(\exists k)(ev_{0}\ldots v_{n}\downarrow\mathbf{k}\wedge k\leq
g(a_{0},\ldots a_{n}))$

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

$g^{M}(m,a_{1},\ldots,a_{k}):=\max\\{g(i,a_{1},\ldots,a_{k})\;|\;i\leq m\\}$

######  Proof 4.4.

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

$(\forall m,n,v_{1},a_{1},\ldots,v_{k},a_{k})(m\leq
n\wedge\bigwedge_{i=1}^{k}v_{i}\lhd a_{i}\Rightarrow(\exists
l)(e\mathbf{n}v_{1}\ldots v_{k}\downarrow\mathbf{l}\wedge l\leq
g^{M}(m,a_{1},\ldots,a_{k})))$

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

$R(a,f,n)=\begin{cases}a&\mbox{if $n=0$}\\\
f(n^{\prime},R(a,f,n^{\prime}))&\mbox{if $n=n^{\prime}+1$}.\end{cases}$

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

$\mathtt{rec}\;v_{1}\;v_{2}\;\mathbf{n}\blacktriangleleft_{\rho}R(a,f,n)$

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

$\mathtt{rec}\;v_{1}\;v_{2}\blacktriangleleft_{{\rm
Nature}\to\rho}R(a,f)^{M},$

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

$\alpha\;\mathbf{n}\leadsto\mathbf{g(n)}$

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

$e\Downarrow^{c}_{g}v:\Leftrightarrow(e\downarrow_{g}v\wedge\forall
h(g=_{c}h\Rightarrow e\downarrow_{h}v))$

where

$g=_{c}h:\Leftrightarrow(\forall i\in c)(g(i)=h(i))$

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

$\epsilon:=[]\ \ \ \ \ \ \mathrm{inc}(c):=c\ \ \ \ \ \
\mathrm{com}(c_{0},c_{1},c_{2}):=c_{0}\ast c_{1}\ast c_{2}.$

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

$\overline{\alpha}_{g}(n):=([n],g(n)).$

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

$(\forall
g,h\in\mathbb{N}^{\mathbb{N}})(e\alpha\downarrow_{g}\mathbf{n}\wedge(g=_{c}h\Rightarrow
e\alpha\downarrow_{h}\mathbf{n}))$

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

$\alpha\;\mathbf{n}\downarrow_{g}\mathbf{g(n)}\wedge(g=_{[n]}h\Rightarrow\alpha\;\mathbf{n}\downarrow_{h}\mathbf{h(n)}=\mathbf{g(n)})$

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

$\overline{\mathtt{rec}}(a,f,n)=\begin{cases}([],a)&\mbox{if $n=0$}\\\
fn^{\prime}\circ\overline{\mathtt{rec}}(a,f,n^{\prime})&\mbox{if
$n=n^{\prime}+1$}\end{cases}$

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

$v_{2}\;\mathbf{n}\;(\mathtt{rec}\;v_{1}\;v_{2}\;\mathbf{n})\blacktriangleleft_{\rho,g}fn\circ\overline{\mathtt{rec}}(a,f,n)=\overline{\mathtt{rec}}(a,f,n+1)$

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:

$\forall g\exists N\forall h(g=_{N}h\Rightarrow F(f)=F(g)),$

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

$\displaystyle[x]\eta:=\eta(x)\ \ \ \ \ \ [\lambda x.t]\eta:=\mathop{\hbox
to0.0pt{$\lambda$\hss}\mkern
2.0mu\raisebox{1.18399pt}{$\lambda$}}a.[t]\eta\\{x\mapsto a\\}\ \ \ \ \ \
[ts]\eta:=[t]\eta([s]\eta)$ $\displaystyle[\mathtt{0}]:=0\ \ \ \ \ \
[\mathtt{s}](n):=n+1$ $\displaystyle[\mathtt{rec}_{\rho}](a,h,0):=a\ \ \ \ \ \
[\mathtt{rec}_{\rho}](a,h,n+1)=hn([\mathtt{rec}](a,h,n))$

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

$[\alpha]_{g}(n):=g(n).$

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:

$m\sim_{\rm Nature}n:\Leftrightarrow m=_{\mathbb{N}}n\ \ \ \ \ \
f\sim_{\rho\to\tau}g:\Leftrightarrow\forall a,b(a\sim_{\rho}b\Rightarrow
fa\sim_{\tau}\pi_{1}(gb))$

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

$[\lambda x.t]_{g}\eta(a)=[t]_{g}\eta\\{x\mapsto
a\\}\sim_{\tau}\pi_{1}(\llbracket{|{t}|}\rrbracket_{g}\xi\\{x\mapsto
b\\})=\pi_{1}(\pi_{1}(\llbracket{|{\lambda x.t}|}\rrbracket_{g}\xi(b)))$

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

$a\sim_{\rho}a^{\prime}\wedge h\sim_{{\rm
Nature}\to\rho\to\rho}h^{\prime}\to[\mathtt{rec}_{\rho}](a,h,n)\sim_{\rho}\pi_{1}(\overline{\mathtt{rec}}_{\rho}(a^{\prime},h^{\prime},n))$

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

$[\alpha]_{g}(n)=\pi_{1}(\overline{\alpha}_{g}(n))=g(n)$

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

$[e](g)=[e]_{g}([\alpha]_{g})=[e\alpha]_{g}=\pi_{1}(\llbracket{|{e\alpha}|}\rrbracket_{g})$

and we are done.

######  Theorem 19.

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

$\forall g,h(g=_{\Phi(g)}h\Rightarrow F(g)=F(h))$

where $\Phi$ is defined by

$\Phi(g):=\max\\{j\;:\;j\in\pi_{0}(\llbracket{|{e}|}\rrbracket\circ([],\mathop{\hbox
to0.0pt{$\lambda$\hss}\mkern
2.0mu\raisebox{1.18399pt}{$\lambda$}}n.([n],gn)))\\}+1$

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

$\llbracket{|{e\alpha}|}\rrbracket_{g}=\llbracket{|{e}|}\rrbracket\circ\llbracket{|{\alpha}|}\rrbracket_{g}=\llbracket{|{e}|}\rrbracket\circ([],\mathop{\hbox
to0.0pt{$\lambda$\hss}\mkern 2.0mu\raisebox{1.18399pt}{$\lambda$}}n.([n],gn))$

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.

$\displaystyle v\downarrow^{0}_{\rho}v\mbox{ \ \ for values $v$}$
$\displaystyle\frac{r[u/x]\downarrow^{c}_{\tau}v}{(\lambda
x.r)u\downarrow^{c+1}_{\tau}v}\mbox{ \ \ for $x:\rho\vdash r$ and $u:\rho$ a
value}$ $\displaystyle\frac{r\sigma\downarrow^{c}_{\rho}v}{fv_{1}\ldots
v_{n}\downarrow^{c+1}_{\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^{c_{0}}_{\rho\to\tau}u\ \ \
\ \ e^{\prime}\downarrow^{c_{1}}_{\rho}v\ \ \ \ \ \
uv\downarrow^{c_{2}}_{\tau}w}{ee^{\prime}\downarrow^{c_{0}+c_{1}+c_{2}}_{\tau}w}\mbox{
\ \ \ if one of $e$, $e^{\prime}$ is not a value}$ Figure 7. Cost semantics of
target language

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

$e\Downarrow^{c}_{\rho}v:\Leftrightarrow e\downarrow^{c}_{\rho}v\ \ \ \ \ \
\mathbf{n}\lhd_{\rm Nature}m:\Leftrightarrow n=m\ \ \ \ \ \
\mathbf{a}\lhd_{{\rm Nature}^{\ast}}b:\Leftrightarrow a=b$

and thus $\blacktriangleleft_{\rho}$ becomes

$\displaystyle e\blacktriangleleft_{\rho}(c,a)$
$\displaystyle:\Leftrightarrow(\exists v)(e\downarrow^{c}_{\rho}v\wedge
v\lhd_{\rho}a)$ $\displaystyle u\lhd_{\rho\to\tau}f$
$\displaystyle:\Leftrightarrow(\forall v,a)(v\lhd_{\rho}a\Rightarrow
uv\blacktriangleleft_{\tau}f(a)).$

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

$\epsilon:=0\ \ \ \ \ \ \mathrm{inc}(c):=c+1\ \ \ \ \ \
\mathrm{com}(c_{0},c_{1},c_{2}):=c_{0}+c_{1}+c_{2}$

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

$e\downarrow^{\pi_{0}\llbracket{|{e}|}\rrbracket}v$

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

$\overline{\mathtt{fold}}(b,h,a):=1\mathbin{{+}\mspace{-8.0mu}{+}}\begin{cases}(0,b)&\mbox{if
$a=[]$}\\\ hn\circ\overline{\mathtt{fold}}(b,h,a^{\prime})&\mbox{if
$a=a^{\prime}\ast n$}.\end{cases}$

  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

$\displaystyle\overline{\mathtt{bar}}(\omega,g,h,a):=$ $\displaystyle
4+\omega_{0}(\mathop{\hbox to0.0pt{$\lambda$\hss}\mkern
2.0mu\raisebox{1.18399pt}{$\lambda$}}i.(1,\hat{a}_{i}))$
$\displaystyle\mathbin{{+}\mspace{-8.0mu}{+}}\begin{cases}g(a)&\mbox{if
$\omega_{1}(\mathop{\hbox to0.0pt{$\lambda$\hss}\mkern
2.0mu\raisebox{1.18399pt}{$\lambda$}}i.(1,\hat{a}_{i}))<|a|$}\\\
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\ast
n))&\mbox{otherwise}\end{cases}$

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:

$\mathtt{fold}_{\rho}\;v_{1}\;v_{2}\;\varepsilon\downarrow^{1}_{\rho}v_{1}\ \
\ \ \ \ \frac{v_{2}\;\mathbf{n}\downarrow^{c_{0}}_{\rho\to\rho}u\ \ \ \ \ \
\mathtt{fold}_{\rho}\;v_{1}\;v_{2}\;\mathbf{a}\downarrow^{c_{1}}_{\rho}v\ \ \
\ \ \
uv\downarrow^{c_{2}}_{\rho}w}{\mathtt{fold}_{\rho}\;v_{1}\;v_{2}\;\mathbf{a}::\mathbf{n}\downarrow^{1+c_{0}+c_{1}+c_{2}}_{\rho}w}$

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:

$\displaystyle\frac{v_{1}(\mathtt{ext}\;\mathbf{a})\downarrow^{c_{0}}_{\rm
Nature}\mathbf{k}\ \ \ \ \ \ k<|a|\ \ \ \ \ \
v_{2}\;\mathbf{a}\downarrow^{c_{1}}_{\rm
Nature}\mathbf{n}}{\mathtt{bar}\;v_{1}\;v_{2}\;v_{3}\;\mathbf{a}\downarrow^{4+c_{0}+c_{1}}\mathbf{n}}$
$\displaystyle\frac{v_{1}(\mathtt{ext}\;\mathbf{a})\downarrow^{c_{0}}_{\rm
Nature}\mathbf{k}\ \ \ \ \ \ k\geq|a|\ \ \ \ \ \ v_{3}\;\mathbf{a}\;(\lambda
x\;.\;\mathtt{bar}\;v_{1}\;v_{2}\;v_{3}\;(\mathbf{a}::x))\downarrow^{c_{1}}_{\rm
Nature}\mathbf{n}}{\mathtt{bar}\;v_{1}\;v_{2}\;v_{3}\;\mathbf{a}\downarrow^{4+c_{0}+c_{1}}_{\rm
Nature}\mathbf{n}}$

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

$\mathtt{bar}_{1}\;f\;g\;h\;xs\;\mathtt{0}\leadsto g\;xs$

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

$\mathtt{bar}_{1}\;v_{1}\;v_{2}\;v_{2}\;\mathbf{a}\;(v_{1}(\mathtt{ext}\;\mathbf{a})<\mathtt{len}\;\mathbf{a})\downarrow^{3+c_{0}+c_{1}}\mathbf{n}$

and from the defining equation

$\mathtt{bar}\;f\;g\;h\;xs\leadsto\mathtt{bar}_{1}\;f\;g\;h\;xs\;(f(\mathtt{ext}\;xs)<\mathtt{len}\;xs)$

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

$(c_{0},k):=\omega(\mathop{\hbox to0.0pt{$\lambda$\hss}\mkern
2.0mu\raisebox{1.18399pt}{$\lambda$}}i.(1,\hat{a}_{i})).$

As in Lemma 7, we now assume inductively that

$\mathtt{bar}\;v_{1}\;v_{2}\;v_{3}\;\mathbf{a}::\mathbf{n}\blacktriangleleft\overline{\mathtt{bar}}(\omega,g,h,a\ast
n)$ ($\ast$)

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

$(\mathtt{bar}\;v_{1}\;v_{2}\;v_{3}\;\mathbf{a}::x)[\mathbf{n}/x]\downarrow^{c}\mathbf{m}$

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

$(\lambda
x\;.\;\mathtt{bar}\;v_{1}\;v_{2}\;v_{3}\;\mathbf{a}::x)\mathbf{n}\downarrow^{c+1}\mathbf{m}$

from which we can infer

$\lambda
x\;.\;\mathtt{bar}\;v_{1}\;v_{2}\;v_{3}\;\mathbf{a}::x\blacktriangleleft_{{\rm
Nature}\to{\rm Nature}}(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)).$

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

$v_{3}\;\mathbf{a}\;(\lambda
x\;.\;\mathtt{bar}\;v_{1}\;v_{2}\;v_{3}\;\mathbf{a}::x)\downarrow^{c_{1}}\mathbf{n}$

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

$\neg(\mathtt{bar}\;v_{1}\;v_{2}\;v_{3}\;(\mathbf{a}::\mathbf{b}_{0}::\ldots::\mathbf{b}_{l-1})\blacktriangleleft\overline{\mathtt{bar}}(\omega,g,h,a\ast[{b}]({l})))$

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

$\omega_{1}([{\beta}]({|a|+N})\ast\gamma)=\omega_{1}(\beta)$

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

$\omega_{1}(\mathop{\hbox to0.0pt{$\lambda$\hss}\mkern
2.0mu\raisebox{1.18399pt}{$\lambda$}}i.(1,(\widehat{a\ast[{b}]({L})})_{i})=\omega_{1}(\beta)<|a|+L.$

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

$\mathtt{bar}\;v_{1}\;v_{2}\;v_{3}\;(\mathbf{a}::\mathbf{b_{0}}::\ldots::\mathbf{b}_{L-1})\blacktriangleleft\overline{\mathtt{bar}}(\omega,g,h,a\ast[{b}]({L})),$

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

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

$\Phi(\omega,\beta,a)=\begin{cases}0&\mbox{if $\omega(\hat{a})<|a|$}\\\
1+\Phi(\omega,\beta,a::\beta(|a|)).&\mbox{otherwise}\end{cases}$

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

$\mathtt{spec}:=\lambda x,y,z\;.\;\mathtt{bar}\;x\;(\lambda
x^{\prime}.\mathtt{0})(\lambda
z^{\prime},p\;.\;\mathtt{s}(p(y(\mathtt{len}\;z^{\prime}))))\;z.$

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

$\mathtt{spec}\;v_{1}\;v_{2}\;\mathbf{a}\blacktriangleleft_{{\rm
Nature}}\phi(\omega,g,a)$

where $\phi$ is defined as

$\phi(\omega,g,a)=\overline{\mathtt{bar}}(\omega,\mathop{\hbox
to0.0pt{$\lambda$\hss}\mkern
2.0mu\raisebox{1.18399pt}{$\lambda$}}b^{\prime}.(1,0),\mathop{\hbox
to0.0pt{$\lambda$\hss}\mkern
2.0mu\raisebox{1.18399pt}{$\lambda$}}b\;.\;(1,\mathop{\hbox
to0.0pt{$\lambda$\hss}\mkern
2.0mu\raisebox{1.18399pt}{$\lambda$}}f\;.\;(4+g_{0}(|b|)+f_{0}(g_{1}(|b|)),1+f_{1}(g_{1}(|b|)))),a).$

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

$\displaystyle\phi(\omega,g,a)$ $\displaystyle=4+\omega_{0}(\mathop{\hbox
to0.0pt{$\lambda$\hss}\mkern
2.0mu\raisebox{1.18399pt}{$\lambda$}}i.(1,\hat{a}_{i}))\mathbin{{+}\mspace{-8.0mu}{+}}\begin{cases}(1,0)&\mbox{if
$\omega_{1}(\mathop{\hbox to0.0pt{$\lambda$\hss}\mkern
2.0mu\raisebox{1.18399pt}{$\lambda$}}i.(1,\hat{a}_{i}))<|a|$}\\\
r&\mbox{otherwise}\end{cases}$ $\displaystyle\mbox{where }r$
$\displaystyle:=(6+g_{0}(|a|)+\phi_{0}(\omega,g,a\ast
g_{1}(|a|)),1+\phi_{1}(\omega,g,a\ast g_{1}(|a|)))$

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

$f^{n}:=\mathop{\hbox to0.0pt{$\lambda$\hss}\mkern
2.0mu\raisebox{1.18399pt}{$\lambda$}}i.(1,\widehat{[{f}]({n})_{i}}).$

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

$\phi_{0}(\omega,g,[{g_{1}}]({n}))=4+\omega_{0}(g_{1}^{n})+1$

and otherwise we have

$\phi_{0}(\omega,g,[{g_{1}}]({n}))=4+\omega_{0}(g_{1}^{n})+6+g_{0}(n)+\phi_{0}(\omega,g,[{g_{1}}]({n+1}))$

Putting these together we obtain

$\phi_{0}(\omega,g,[{g_{1}}]({n}))=5+\omega_{0}(g_{1}^{n})+\begin{cases}0&\mbox{if
$\omega_{1}(g_{1}^{n})<n$}\\\
5+g_{0}(n)+\phi_{0}(\omega,g,[{g_{1}}]({n+1}))&\mbox{otherwise}\end{cases}$

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

$\phi_{0}(\omega,g,[])=10N+5+\sum_{i=0}^{N}\omega_{0}(g^{i}_{1})+\sum_{i=0}^{N-1}g_{0}(i).$

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

$\displaystyle e\Downarrow^{c}v$ $\displaystyle:\Leftrightarrow(\exists
c^{\prime})(e\downarrow^{c^{\prime}}v\wedge c^{\prime}\leq c)$
$\displaystyle\mathbf{n}\lhd_{\rm Nature}m$ $\displaystyle:\Leftrightarrow
1\leq m$ $\displaystyle\mathbf{a}\lhd_{{\rm Nature}^{\ast}}m$
$\displaystyle:\Leftrightarrow|a|\leq m$

and thus $\blacktriangleleft_{\rho}$ becomes

$\displaystyle e\blacktriangleleft_{\rho}(c,a)$
$\displaystyle:\Leftrightarrow(\exists
v,c^{\prime})(e\downarrow^{c^{\prime}}_{\rho}v\wedge c^{\prime}\leq c\wedge
v\lhd_{\rho}a)$ $\displaystyle u\lhd_{\rho\to\tau}f$
$\displaystyle:\Leftrightarrow(\forall v,a)(v\lhd_{\rho}a\Rightarrow
uv\blacktriangleleft_{\tau}f(a)).$

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

$e\downarrow^{c}v\mbox{ \; for some \;
}c\leq\pi_{0}\llbracket{|{e}|}\rrbracket$

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. For types
$\rho$ of our target language, define
$\vee_{\rho}:\llbracket{|{\rho}|}\rrbracket\times\llbracket{|{\rho}|}\rrbracket\to\llbracket{|{\rho}|}\rrbracket$
inductively by

$\displaystyle m\vee_{\delta}n$ $\displaystyle:=\max\\{m,n\\}\mbox{ for
$\delta={\rm Nature},{\rm Nature}^{\ast}$}$ $\displaystyle
f\vee_{\rho\to\tau}g$ $\displaystyle:=\mathop{\hbox
to0.0pt{$\lambda$\hss}\mkern
2.0mu\raisebox{1.18399pt}{$\lambda$}}a\;.\;(\max\\{f_{0}a,g_{0}a\\},f_{1}a\vee_{\tau}g_{1}a).$

######  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

$\overline{\mathtt{fold}}(a,h,n)=1\mathbin{{+}\mspace{-8.0mu}{+}}\begin{cases}(0,a)&\mbox{if
$n=0$}\\\
(h1\circ\overline{\mathtt{fold}}_{0}(a,h,n^{\prime}),a\vee_{\rho}h1\circ\overline{\mathtt{fold}}_{1}(a,h,n^{\prime}))&\mbox{if
$n=n^{\prime}+1$}\end{cases}$

######  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

$v_{2}\;\mathbf{m}\;(\mathtt{fold}\;v_{1}\;v_{2}\;\mathbf{a}^{\prime})\downarrow^{c^{\prime}}w\wedge
c^{\prime}\leq c\wedge w\lhd_{\rho}b$

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

$\mathtt{fold}\;v_{1}\;v_{2}\;\mathbf{a}^{\prime}::\mathbf{m}\downarrow^{c^{\prime}+1}w\wedge
c^{\prime}+1\leq c+1\wedge w\lhd_{\rho}b.$

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.

## References

  * [1] R. Benzinger.  Automated higher-order complexity analysis.  Theoretical Computer Science, 318(1-2):79–103, 2004.
  * [2] S. Berardi, M. Bezem, and T. Coquand.  On the computational content of the axiom of choice.  Journal of Symbolic Logic, 63(2):600–622, 1998.
  * [3] U. Berger.  A computational interpretation of open induction.  In Proceedings of Logic in Computer Science (LICS ’04), pages 326–334. IEEE Computer Society, 2004.
  * [4] U. Berger.  Strong normalization for applied lambda calculi.  Logical Methods in Computer Science, 1(2):1–14, 2005.
  * [5] U. Berger.  Continuous semantics for strong normalization.  Mathematical Structures in Computer Science, 16:751–762, 2006.
  * [6] M. Bezem.  Strong normalization of barrecursive terms without using infinite terms.  Archiv für mathematische Logik und Grundlagenforschung, 25:175–181, 1985.
  * [7] M. Bezem.  Strongly majorizable functionals of finite type: A model for bar recursion containing discontinuous functionals.  Journal of Symbolic Logic, 50:652–660, 1985.
  * [8] Thierry Coquand and Guilhem Jaber.  A computational interpretation of forcing in type theory.  In P. Dybjer, S. Lindström, E. Palmgren, and G. Sundholm, editors, Epistemology versus Ontology, volume 27 of Logic, Epistemology, and the Unity of Science, pages 203–213. Springer, 2012.
  * [9] N. Danner, D. Licata, and R. Ramyaa.  Denotational cost semantics for functional languages with inductive types.  In Proceedings International Conference of Functional Programming (ICFP ’15), volume 50 of ACM SIGPLAN Notices, pages 140–151, 2015.
  * [10] N. Danner, J. Paykin, and J.S. Royer.  A static cost analysis for a higher-order language.  In M. Might and D.V. Horn, editors, Proceedings of the 7th Workshop on Programming Languages meet Program Verification, ACM Press, pages 25–34, 2013.
  * [11] Y. L. Ershov.  Model ${C}$ of partial continuous functionals.  In R. Gandy and M. Hyland, editors, Logic Colloquium 76, pages 455–467. North Holland, Amsterdam, 1977\.
  * [12] M. Escardó.  Continuity of Gödel’s system T functionals via effectful forcing.  In Proceedings of Mathematical Foundations of Programming Semantics (MFPS ’13), volume 298 of Electronic Notes in Theoretical Computer Science, pages 119–141, 2013.
  * [13] M. Escardó, P. Oliva, and T. Powell.  System T and the product of selection functions.  In Proceedings of Computer Science Logic (CSL ’11), volume 12 of LIPIcs, pages 233–247, 2011.
  * [14] M.-D. Hernest.  Synthesis of moduli of uniform continuity by the monotone Dialectica interpretation.  Electronic Notes in Theoretical Computer Science, 174(5):141–149, 2007.
  * [15] W. A. Howard.  Functional interpretation of bar induction by bar recursion.  Compositio Mathematica, 20:107–124, 1968.
  * [16] W. A. Howard.  Hereditarily majorizable functionals of finite type.  In A. Troelstra, editor, Metamathematical Investigation of Intuitionistic Arithmetic and Analysis, volume 344 of Lecture Notes in Mathematics, pages 454–461. Springer, 1973.
  * [17] T. Kawai.  Representing definable functions of HAω by neighbourhood functions.  Annals of Pure and Applied Logic, 170(8):891–909, 2019.
  * [18] T.-S. Kim.  Cost semantics for Plotkin’s PCF.  Master’s thesis, Wesleyan University, 2016.
  * [19] S. C. Kleene.  Countable functionals.  In A. Heyting, editor, Constructivity in Mathematics, pages 81–100. North-Holland, Amsterdam, 1959.
  * [20] U. Kohlenbach.  Analysing proofs in analysis.  In W. Hodges, M. Hyland, C. Steinhorn and J. Truss, editors, Logic: from Foundations to Applications, European Logic Colloquium 1993, pages 225–260. Oxford University Press, 1996.
  * [21] U. Kohlenbach.  Applied Proof Theory: Proof Interpretations and their Use in Mathematics.  Monographs in Mathematics. Springer, 2008.
  * [22] G. Kreisel.  Interpretation of analysis by means of functionals of finite type.  In A. Heyting, editor, Constructivity in Mathematics, pages 101–128. North-Holland, Amsterdam, 1959.
  * [23] E. Moggi.  Notions of computation and monads.  Information and Computation, 93(1):55–92, 1991.
  * [24] P. Oliva.  Understanding and using Spector’s bar recursive interpretation of classical analysis.  In Proceedings of Computability in Europe (CiE ’06), volume 3988 of LNCS, pages 423–234, 2006.
  * [25] P. Oliva and T. Powell.  On Spector’s bar recursion.  Mathematical Logic Quarterly, 58:356–365, 2012.
  * [26] P. Oliva and S. Steila.  A direct proof of Schwichtenberg’s bar recursion closure theorem.  Journal of Symbolic Logic, 83(1):70–83, 2018.
  * [27] G. D. Plotkin.  LCF considered as a programming language.  Theoretical Computer Science, 5:223–255, 1977.
  * [28] T. Powell.  A functional interpretation with state.  In Proceedings of Logic in Computer Science (LICS ’18), pages 839–848. ACM, 2018.
  * [29] V. Rahli and M. Bickford.  Validating Brouwer’s continuity principle for numbers using named exceptions.  Mathematical Structures in Computer Science, 28(6):942–990, 2018\.
  * [30] D. Sands.  Calculi for Time Analysis of Functional Programs.  PhD thesis, University of London, 1990.
  * [31] B. Scarpellini.  A model for bar recursion of higher types.  Compositio Mathematica, 23:132–153, 1971.
  * [32] H. Schwichtenberg.  Proof theory: Some applications of cut elimination.  In J. Barwise, editor, Handbook of Mathematical Logic, pages 867–895. North-Holland, Amsterdam, 1977.
  * [33] H. Schwichtenberg.  On bar recursion of types $0$ and $1$.  The Journal of Symbolic Logic, 44:325–329, 1979.
  * [34] J. Shultis.  On the complexity of higher-order programs.  Technical Report CU-CS-288-85, University of Colorado at Boulder, 1985\.
  * [35] C. Spector.  Provably recursive functionals of analysis: a consistency proof of analysis by an extension of principles in current intuitionistic mathematics.  In F. D. E. Dekker, editor, Recursive Function Theory: Proc. Symposia in Pure Mathematics, volume 5, pages 1–27. American Mathematical Society, Providence, Rhode Island, 1962.
  * [36] A. S. Troelstra.  Metamathematical Investigation of Intuitionistic Arithmetic and Analysis, volume 344 of Lecture Notes in Mathematics.  Springer, 1973.
  * [37] K. Van Stone.  A Denotational Approach to Measuring Complexity in Functional Programs.  PhD thesis, Carnegie Mellon University, 2003.
  * [38] H. Vogel.  Ein starker Normalisationssatz für die barrekursiven Funktionale.  Archiv für mathematische Logik und Grundlagenforschung, 18:81–84, 1976.
  * [39] P. Wadler.  The essence of functional programming.  In Proceedings of Symposium of Principles of Programming Languages (POPL ’92), pages 1–14. ACM Press, 1992.
  * [40] Chuangjie Xu.  A syntactic approach to continuity of T-definable functionals.  Logical Methods in Computer Science, 16(1), 2020.