Polynomial Time and Dependent Types

Robert Atkey

University of Strathclyde
26 Richmond Street
G1 1XH

We combine dependent types with linear type systems that soundly and
completely capture polynomial time computation. We explore two
systems for capturing polynomial time: one system that disallows
construction of iterable data, and one, based on the LFPL system of
Martin Hofmann, that controls construction via a payment
method. Both of these are extended to full dependent types via
Quantitative Type Theory, allowing for arbitrary computation in
types alongside guaranteed polynomial time computation in terms. We
prove the soundness of the systems using a realisability technique
due to Dal Lago and Hofmann.

Our long-term goal is to combine the extensional reasoning of type
theory with intensional reasoning about the resources intrinsically
consumed by programs. This paper is a step along this path, which we
hope will lead both to practical systems for reasoning about
programs' resource usage, and to theoretical use as a form of
synthetic computational complexity theory.

<concept_desc>Computer systems organization Embedded systems</concept_desc>
<concept_desc>Computer systems organization Redundancy</concept_desc>
<concept_desc>Computer systems organization Robotics</concept_desc>
<concept_desc>Networks Network reliability</concept_desc>

[500]Computer systems organization Embedded systems
[300]Computer systems organization Redundancy
Computer systems organization Robotics
[100]Networks Network reliability

§ INTRODUCTION

Type theory is often claimed to be ideal for Computer Science,
combining programming and proof in one unifying system, so a happy
programmer can verify while they program, and program while they
verify. From a broader Computer Science view, however, type theory
lacks the ability to talk about the very thing that makes Computer
Science interesting – the fact that computation is everywhere bounded
by the resources in time and space that we can afford to give it.

Typical Type Theory only speaks of the public face that programs
present to the world – if you input things like this, you get things
that look like that – but cannot bring itself to mention the true
cost of programs' execution. One can encode costs by embedding another
programming language in type theory, for example <cit.>,
or one can synthesise costs by treating resource counting as a
computational effect, for example <cit.>, but
neither of these capture the intrinsic costs of the programs we write
in type theory. These techniques deliver only conspicuous
consumption, not speaking of the real resources consumed.

In this paper, we propose a method for extending dependent type theory
with a means for constraining the intrinsic computational complexity
of programs written in the theory. We concentrate on linear type
systems that soundly and completely capture polynomial time
computation, the commonly used standard for feasible resource usage,
and extend these systems to dependent types. The additional
expressivity of dependent types allows us use these characterisations
of polytime to further functionally characterise the classes of
non-deterministic and probabilistic polynomial time.

We use techniques from Implicit Computational Complexity
theory, which provides intrinsic characterisations of complexity
classes in terms of logical systems or programming languages. We
review the techniques that we use in <ref>. To
adapt these systems to dependent types, we use Quantitative Type
Theory (QTT) <cit.>, a combination of linear
and dependent types. We review QTT in <ref>.

Our long-term goal is to combine the extensional reasoning of Type
Theory with intensional reasoning about the resources intrinsically
consumed by programs. This paper is a first step along this path,
which we hope will lead both to practical systems for reasoning about
programs' resource usage, and to theoretical use as a form of
synthetic computational complexity theory. We discuss these
possibilities further in <ref>.

§.§ Contributions and Content

This paper makes the following contributions to the theory and use of
linear dependent type theory and implicit computational complexity:

* We formulate two systems that combine linear type theory for
polytime computation with full dependent types, using Quantitative
Type Theory. The system is presented in <ref>. The
linear typing discipline required for enforcing polytime is provided
by QTT, but we also need to carefully add constructs for
non-iterable datatypes (<ref>) and the two kinds
of natural number iterator that we consider
(<ref> and <ref>). Porting
the natural number iterators from the simply typed to the
dependently typed setting requires careful annotation of the rules
to ensure that the correct information is available for type
checking, while also not allowing too much information to be made
available at runtime that would violate the polytime soundness
property. A further contribution of this paper is the addition of
reflection types to QTT, <ref>, which allow
statements about polytime realisability to be reflected into

* We demonstrate the utility of the combination of polytime and
dependent types in <ref>. Just as in
the simply typed world, we have an expressive language for writing
polytime programs. With the additional power of dependent types, we
can also prove properties of these programs. A simple example is
proving that a sorting program actually sorts. Using QTT reflection,
we can go further and represent the class of polytime problems, with
polytime reductions between them, as dependent pairs
(<ref>). Our final examples use dependent
types to give monadic presentations of the complexity classes of
Non-deterministic Polynomial (NP) time and Probabilistic Polynomial
(PP) time. Since these classes rely on specific correctness
criteria, it is not possible to capture them in a simply typed
system for polytime.

* We prove the polytime soundness of our systems via a
realisability argument in <ref>. Our construction
is an extension of the amortised complexity realisability
constructions of <cit.>. We extend their
work to our dependently typed setting, and also give a realisability
interpretation of datatypes directly, instead of via second-order
impredicative encodings. The technical content of this section has
been formalised in the Agda proof assistant
<cit.>, and is included in the supplementary

Before we get to the contributions above, we present, in
<ref>, two linear simply typed systems for
polytime, adaptations of systems already present in the
literature. Our paper concludes with a discussion of further related
work and the outlook for future work in <ref>.

§ AFFINE LINEAR TYPING AND POLYTIME

Not long after Girard introduced Linear Logic <cit.>, it was
observed that its resource sensitivity could be turned to describing
computational complexity classes by purely logical means. Typically, a
logical system is described for which the process of reducing a proof
to a normal form (often by cut elimination) is guaranteed to always be
accomplished within a certain complexity bound. Moreover, the system
is usually proven to be complete for the relevant complexity class, by
constructing a simulation of some known representation. Such systems
that characterise polytime include Bounded Linear Logic (BLL), which
uses explicit polynomials in the formulas <cit.> and Soft Affine
Logic (SAL) <cit.>, which does not explicitly represent time
information in formulas, but uses a restricted form of Linear Logic's
$\oc$ modality instead. Light Linear Logic (LLL) <cit.> is
another “counting-free” system for polytime.

Viewing logical systems though the lens of the Curry-Howard
correspondence, the idea arises that one could define functional
programming languages that characterise complexity classes such as
polytime. SAL has been transformed into a programming language by
<cit.>, and likewise for LLL by
<cit.>. <cit.> proposed a new programming
language, Linear Functional Programming Language (LFPL), that uses a
novel “payment” system to track iteration. In this section, we
review the use of linear types to capture polytime by presenting two
systems, one based on ideas from SAL and the second more explicitly
based on LFPL. With a view to extending to dependent types in
<ref>, we take an approach slightly different to much of
the polytime linear logic literature. We emphasise the use of explicit
datatypes and eliminators, rather than using impredicative encodings
via universal types. We are closer to Hofmann's original LFPL (though
not a later presentation of it by <cit.>) than
BLL, SAL or LLL.

For this section, the affine linear $\lambda$-calculus we will use
will have linear functions and $\otimes$-products:

Γ, x : A, Γ' ⊢x : A

Γ, x : A ⊢M : B
Γ⊢λx.M : A ⊸B

Γ_1 ⊢M : A ⊸B

Γ_2 ⊢N : A
Γ_1, Γ_2 ⊢M N : B

Γ_1 ⊢M : A
Γ_2 ⊢N : B
Γ_1, Γ_2 ⊢(M,N) : A ⊗B

Γ_1 ⊢M : A ⊗B
Γ_2, x : A, y : B ⊢N : C
Γ_1, Γ_2 ⊢ (x,y)=M  N : C

These rules are standard, so we do not describe them further except to
note how affine linear typing uses presence or absences in a context
to control resource usage. If a variable is in the context it must be
used at most once (variables that are not used are absorbed by the
additional context in the variable rule). The fact that this
discipline interferes with dependent types is one of the reasons we
turn to QTT when we wish to add dependent types in <ref>.

§.§ No Recursion, Only Case Analysis

It is not too difficult to see that reduction of linear
$\lambda$-terms always takes a number of steps linearly proprotional
to the size of the term. This is because every $\beta$-redex
substitutes into at most one variable, reducing the size of the term
by one each time.

We can increase the expressivity, but not the computational
complexity, of the system by adding datatypes that do not allow
iteration. These can be used for representation, but not for driving
computation. We include the rules here, to show how linearity must be
preserved in these rules, and to foreshadow their dependently typed
counterparts in <ref>. The first type is the
booleans, which are anyway non-recursive and so would not allow
iteration anyway:

⊢, :

Γ_1 ⊢M :
Γ_2 ⊢N_1 : A
Γ_2 ⊢N_2 : A
Γ_1, Γ_2 ⊢ M  N_1  N_2 : A

The if-then-else rule is careful to ensure that the resources used by
the eliminated $\BoolTy$ and the resources used by the chosen branch
are accounted for separately. The two branches must have the same
resource usage.

Construction and case analysis of lists are given by the following

⊢: (A)

Γ_1 ⊢M : A
Γ_2 ⊢N : (A)
Γ_1, Γ_2 ⊢(M,N) : (A)

Γ_1 ⊢M : (A)

Γ_2 ⊢N_1 : B

Γ_2, h : A, t : (A) ⊢N_2 : B
Γ_1, Γ_2 ⊢ M {↦N_1; (h,t) ↦N_2} : B

We can construct lists arbitrarily but only do case analysis on
them. If we wish to explore a list to a arbitrary depth it must be
driven by a type we can iterate over.

With booleans and lists, we can construct several other useful
types. For example, to simulate Turing machines, one can construct a
$\mathrm{Tape}$ type as a Zipper (<cit.>)
$\ListTy(\BoolTy) \otimes \BoolTy \otimes \ListTy(\BoolTy)$,
representing a position on the tape with the items before, under, and
after the head.

§.§ The Cons-free system

Polynomial time is usually seen as a proxy for “feasible”
computation. On the face of it, there does not seem to be any
particular reason why polynomials have anything to do with
feasibility. However, one can arrive at the definition of polynomial
time in three steps, by assuming that (i) iterating over the whole
input is feasible; (ii) if two computations are feasible, then so is
their composition; and (iii) performing a feasible computation for
every element of the input is also feasible. It is the last point that
allows complexities of arbitrary polynomial degree to be constructed
(we will see this in action in the completeness construction below and
soundness proofs in <ref>).

Following these ideas, let us assume that the input is a natural
number, so we assume that there is some type of natural numbers
$\tyNat$. For point (i), we must be able to iterate over these natural
numbers, so we use a linear iterator defined by this typing rule:

⊢M_z : A
x : A ⊢M_s : A
Γ⊢N :
Γ⊢ N {↦M_z; (x) ↦M_s} : A

Note that in the zero, $M_z$, and sucessor, $M_s$, cases, the context
is empty to ensure that these cases may be invoked as many times as
required. Point (ii) above is automatically satisfied by being in a
typed $\lambda$-calculus, where it is difficult to stop functions from
being composable. For point (iii), the iterator as given does not
allow us to nest iterations. Once the natural number input $n$ has
been used for an iteration, the linear typing discipine prevents us
from using it again (note the two separate contexts $\Gamma_1$,
$\Gamma_2$ in the rule for application). In order to allow nested
iterations, we add an operator to duplicate numbers:

Γ⊢M :
Γ⊢ M : ⊗

Somewhat surprisingly, this system is now sound and complete for
polynomial time. Crucially, this depends on the two things we have
not allowed. First, we have disallowed the construction of new
natural numbers via the $\conZero$ and $\conSucc$
constructors[Actually, $\conZero$ would be acceptable, as
well as any constant natural number. It is only unrestricted use of
$\conSucc$ that is dangerous.]. If we were to permit this, then we
could use iteration over the input to construct addition,
multiplication (by repeated addition), and then exponentials (by
repeated multiplication). We therefore refer to this system as the
Cons-Free system.  The second prohibited feature is the ability
to duplicate values of function type, even though we have allowed
duplication of iterable naturals. If we were to allow this, then we
would be able to sneak in a form of constructors for natural numbers
by encoding them as eliminators that duplicate a function for every
$\conSucc$ step.

We will see in <ref> that this system is sound
for polytime by a realisability argument. Completeness can be seen
more directly by constructing a function that iterates a function for
a statically known polynomial number of times in the size of the
input. Assume that we have a known polynomial
$p(n) = c_dn^d + \dots + c_0$ of degree $d$ with natural number
coefficients and some single step function
$f : \mathit{St} \multimap \mathit{St}$ over a state type
$\mathit{St}$ that runs to completion for input of size $n$ in $p(n)$
steps. Then, using the iterator above we can iterate $f$ over a
$\tyNat$ representing the size of the input:

I_1 : ⊸𝑆𝑡 ⊸𝑆𝑡

I_1 = λn. λs. n {↦s; (s) ↦f s }

To achieve higher degrees, we can use $\dupNat$ to nest iterations:

I_k+1 : ⊸𝑆𝑡 ⊸𝑆𝑡

I_k+1 = λn. λs.

(n,n') =  n

n {↦s; (s) ↦I_k n' s }

By further use of $\dupNat$ and composition to handle addition of
polynomials, the function $f$ can now be iterated $p(n)$ many times,
where $n$ is the input $\tyNat$. Thus, the Cons-free system can
represent all polytime computations.

§.§ Diamond Trading with LFPL

The Cons-free system is sound and complete for polytime, but is quite
awkward from the point of view of functional programming. It allows us
to iterate over natural numbers that come from the input but does not
allow us to build further values to do iteration on. For example, if
our input is a list, then we cannot transform it into a binary search
tree and then flatten it, we must always refer back to the original
natural number input. Even dividing the input into two halves to be
treated separately is difficult.

A more flexible system was proposed by <cit.>. Instead
of completely prohibiting construction of data, the Linear
Functional Programming Language (LFPL) allows construction if it is
paid for by values of type $\Diamond$ (“diamonds”):

Γ⊢M :
Γ⊢(M) :

Γ_1 ⊢M :
Γ_2 ⊢N :
Γ_1, Γ_2 ⊢(M, N) :

To construct a $\conZero$, we must have a $\Diamond$ to pay for it,
and likewise, to construct a $\conSucc$ we must pay a $\Diamond$. We
can think of $\Diamond$s as an unit of iterable data. Iterability is
“saved up” in data during construction, and released during
iteration. Diamonds cannot be created by a program itself, for the
same reason that constructors were prohibited in the Cons-free
system, but they are released from iterable data during iteration. The
LFPL natural number iterator has the following typing rule:

d : ⊢M_z : A
d : , x : A ⊢M_s : A
Γ⊢N :
Γ⊢ N {(d) ↦M_z; (d,x) ↦M_s } : A

The difference with the Cons-free iterator above is that the
$\conZero$ and $\conSucc$ cases now both have an additional binding of
type $\Diamond$. This allows some form nesting of iterations: during
an iteration over the input, the program can accumulate $\Diamond$s to
use for iteration over substructures that are smaller than the current
point in the iteration. A construction, due to <cit.>,
illustrates how this leads to all polytime computations. As above, we
assume a polynomial $p(n)$ and a step function
$f : \mathit{St} \multimap \mathit{St}$ that needs to be iterated
$p(n)$ times. We construct a linear iterator:

I_1 : (⊗𝑆𝑡) ⊸(⊗𝑆𝑡)

I_1 = λ(n, s).  n {

(d)   ↦   ((d), s);

(d,(n,s))    ↦    ((d,n),f s) }

Note that this iterator returns the natural number input as well as
the new state. LFPL does not allow duplication of iterable inputs, so
we must always reconstruct it if we want to do further
iteration. Addition of polynomials is accomplished by composition of
iterators. To raise the degree, we again use a nesting iterator:

I_k+1 : (⊗𝑆𝑡) ⊸(⊗𝑆𝑡)

I_k+1 = λ(n,s).  n {

(d)   ↦   ((d),s);

(d,(n,s))    ↦     (n,s)=I_k (n,s)  ((d,n), f s) }

Unlike in the Cons-free system, this iterator does not raise
the degree of the nested iterator directly. Rather the iterator $I_k$
performs $\binom{n}{k}$ iterations. As observed by Aelhig and
Schwictenberg, this is sufficient because the binomials form a basis
for the vector space of all polynomials.

Despite this slightly more involved completeness construction, the
advantage of LFPL is that it is now easy to have arbitrary iterable
datatypes and to transform between them. We need only take the
introduction and elimination rules for any inductive datatype and add
$\Diamond$ premises to the introduction rules and $\Diamond$ bindings
to the eliminators.

§ POLYTIME QUANTITATIVE TYPE THEORY

We have now seen the Cons-free and LFPL systems for
capturing polytime by means of linear typing and restricted
iteration. We now look to extend these systems to include dependent
types by building upon Quantitative Type Theory (QTT)
<cit.>. This section reviews QTT and describes
how we have adapted it to the polytime systems we saw in the previous

§.§ Quantitative Type Theory

Integrating linear and dependent types is not straightforward due to
the conflict between the linear typing discipline regarding presence
of a variable as only bestowing the right to use it once, and the
dependent typing regime that uses variables both in types (for
specification purposes) and in terms (for computational purposes),
syntactically yield multiple uses of the same variable.

QTT is a system that resolves this conflict by recording usage of
variables with annotations from a semiring. It sits in the general
area of systems that use semiring annotatons to measure resource usage
<cit.>. The key feature of QTT, an
insight owing to <cit.>, is that usage of variables in
types counts for $0$-usage in terms of the semiring used. This allows
us to use normal type theory as a specification language, while also
enjoying the benefits of linear typing for programs. The term typing
judgement of QTT has the following form:

x_1 ρ_1: S_1, …, x_n ρ_n: S_n ⊢M σ: T

where the annotations $\rho_i$ are all from the semiring being
used. The annotation $\sigma$ is either $0$ or $1$, indicating whether
we are in the erased ($\sigma = 0$) fragment, where all the normal
rules of type theory apply, or the in the non-erased (“present”,
“realisable”, $\sigma = 1$) fragment, where a restricted typing
discipline applies.  As we shall see below in the cases of
$\Sigma$-types, iterable types, and LFPL's $\Diamond$ type, the
separation of QTT into these two fragments allows an expressive
combination of reasoning using full type theory with the benefits of
linear typing.

In the remainder of this sub-section, we describe the core of QTT. As
well as the term typing judgement given above, QTT also has judgements
for well-formed contexts ($\Gamma~\isctxt$) and types
($\Gamma \vdash T~\istype$), and definitional equality of types and
terms ($\Gamma \vdash S \equiv T~\istype$ and
$\Gamma \vdash M \equiv N \stackrel\sigma: S$). It is an invariant of
the system that types are always well-formed in a context with all
annotations $0$, i.e., $\Gamma \vdash S~\istype$ implies
$0\Gamma = \Gamma$. An important admissible rule of the system, along
with weakening and substitution, is that of $0$-ing:

Γ⊢M 1: S
0Γ⊢M 0: S

This rule allows us to take any term $M$ in the $\sigma = 1$ fragment
and treat it as if it were in the $\sigma = 0$ fragment, and hence use
it for specification purposes in types. As we add novel rules to QTT
in the following sections, we will be careful to maintain the
admissibility of this rule.

§.§.§ Natural-number usages

We use an instantiation of QTT with the natural number semiring, with
the usual semiring structure of addition and multiplication. In a mild
generalisation of the original presentation of QTT, we also allow
sub-usaging via the reverse ordering on the naturals. That is,
if a variable is marked as usage $n$ and $m \geq n$, then we can also
regard it as usage $m$. This makes the system more like affine linear
logic, since $m \leq 0$ for all $m$, matching the system in
<ref>. We do not have an unrestricted
usage $\omega$, since this would allow the possibility of unrestricted
duplication, and hence violate our polytime soundness properties.

§.§.§ Contexts, variables, and conversion

As we saw above, contexts in QTT are comprised of variable
$\stackrel\rho:$ type triples, where $\rho$ is a natural number
indicating how many times the variable $x$ is available for use in a
$\sigma = 1$ term. There are two operations on raw contexts: scaling
$\pi\Gamma$, which multiplies each $\rho$ in $\Gamma$ by $\pi$, and
addition $\Gamma_1 + \Gamma_2$, which adds two contexts' usage
annotations assuming that the lengths and types are equal. Contexts
are ordered pointwise $\Gamma' \sqsubseteq \Gamma$ on the usage
annotations (which is the reverse ordering on naturals) The
basic usage-annotation discipline of QTT is demonstrated by the
context formation and variable rules:

Γ, x ρ: S

0Γ, x σ: S, 0Γ'
0Γ, x σ: S, 0Γ' ⊢x σ: S

Γ⊢M : S
Γ' ⊑Γ
Γ' ⊢M : S

As with most dependent type theories, contexts are built inductively
from the empty context $\epsilon$ and extension of a context by a
variable with a type that is well-formed in the preceding
context. Usage annotations $\rho$ on variables are arbitrary, and
types are always judged in a $0$-annotated context. The variable rule
marks unused variables as usage $0$ and the selected variable with
usage $\sigma$.

§.§.§ $\Pi$- and $\Sigma$-types

QTT's $\Pi$-types have the form $(x \stackrel\rho: S) \to T$,
indicating functions that, in the $\sigma = 1$ fragment, use their
arguments $\rho$-many times. The formation, introduction and
elimination rules are similar to the standard ones, except for the
addition of usage annotations:

0Γ, x 0: S ⊢T
0Γ⊢(x ρ: S) →T

Γ, x σρ: S ⊢M σ: T
Γ⊢λx.M σ: (x ρ: S) →T

Γ_1 ⊢M σ: (x ρ: S) →T

Γ_2 ⊢N σ': S

0Γ_1 = 0Γ_2

σ' = 0 ⇔(ρ= 0 σ= 0)
Γ_1 + ρΓ_2 ⊢M N σ: T[N/x]

The side conditions on the elimination rule state that (i) both
$\Gamma_1$ and $\Gamma_2$ erase to the same context, so their sum is
defined; and (ii) the argument $N$ is erased (i.e., $\sigma' = 0$) iff
either the function does not use its argument, or we are in the
$\sigma = 0$ fragment and everything is being erased. In the
following, when we write $S \to T$ for a non-dependent function type,
we mean that the argument is to be used linearly:
$(x \stackrel1: S) \to T$, where $x$ does not appear in $T$.

$\Sigma$-types are a little more involved, and demonstrate the
flexibility in QTT in allowing additional power in the $\sigma = 0$
fragment, where we do not need to care about polytime
realisability. Formation and introduction are given by the rules:

0Γ, x 0: S ⊢T
0Γ⊢(x π: S) ⊗T

Γ_1 ⊢M σ': S

Γ_2 ⊢N σ: T[M/x]

0Γ_1 = 0Γ_2

σ' = 0 ⇔(π= 0 σ= 0)
πΓ_1 + Γ_2 ⊢(M, N) σ: (x π: S) ⊗T

As with $\Pi$-typed, the first component of a $\Sigma$ type is
annotated with a usage for how many times it can be used, and this is
respected by the introduction rule. Elimination of $\Sigma$-types
depends on whether we are in the $\sigma = 0$ fragment or not. In the
$\sigma = 0$ fragment, we are free to disregard usage restrictions,
and use projections as normal:

Γ⊢M 0: (x π: S) ⊗T
Γ⊢fst(M) 0: S

Γ⊢M 0: (x π: S) ⊗T
Γ⊢snd(M) 0: T[fst(M)/x]

$\Sigma$-types are unrestricted in the $\sigma = 0$ fragment, and we
can use them as normal for type-theoretic constructions.  In the
$\sigma = 1$ fragment, we must take into account the resource content
of objects and use a pattern matching construct; the dependently typed
analogue of the $\otimes$-eliminator in <ref>:

0Γ, z 0: (x π: A) ⊗B ⊢C

Γ_1 ⊢M σ: (x π: A) ⊗B

Γ_2, x σπ: A, y σ: B ⊢N σ: C[(x,y)/z]

0Γ_1 = 0Γ_2
Γ_1 + Γ_2 ⊢let (x,y) = M in N σ: C[M/z]

QTT also supports a unit type $I$ with constructor $*$ and
pattern-matching <cit.>.

§.§.§ The Identity Type

QTT also supports an extensional equality type with equality reflection:

0Γ⊢M 0: S

0Γ⊢N 0: S
0Γ⊢M =_S N

Γ⊢M σ: S
Γ⊢(M) σ: M =_S M

Γ⊢N 0: M_1 =_S M_2
Γ⊢M_1 ≡M_2 0: S

The equality type also has an $\eta$ rule demonstrating $\conRefl(M)$
as the only proof of equality <cit.>. Note that
equality reflection only targets the $\sigma = 0$ fragment, we cannot
use equality reflection to convey realisability information.

§.§.§ Universe
QTT has universe types $\mathsf{U}$, as in
standard type theory <cit.>.

§.§.§ Datatypes
QTT, as we have presented it so far, has no
interesting base types to perform computation on. Following our
presentation of the simply typed linear systems in
<ref>, we add two kinds of datatype to
QTT. First, in <ref>, we add non-iterable
datatypes that allow construction and case analysis, but no
recursion. In <ref> we describe how to extend
QTT to be a dependently typed adaptation of the Cons-free system of
<ref>. In <ref>, we apply the
same treatment to the LFPL-style system.

§.§ Non-iterable Datatypes

§.§.§ Booleans
The boolean type for QTT was described in
<cit.>, but we repeat it here for completeness. Booleans
offer no possibility for iteration, but it is useful to see how the
QTT rules extend the simply typed rules from
<ref> before moving to more complex

0Γ⊢, σ:

0Γ_1, x 0: ⊢P

Γ_1 ⊢M σ:

Γ_2 ⊢N_t σ: P[/x]

Γ_2 ⊢N_f σ: P[/x]

0Γ_1 = 0Γ_2
Γ_1 + Γ_2 ⊢_x.P  M     N_t     N_f σ: P[M/x]

The introduction rules for booleans both use a $0$-d context,
indicating that construction of boolean values is free. Elimination of
booleans via a dependently typed if-then-else is more subtle with its
resource usage. The boolean to be eliminated must be constructed in a
context $\Gamma_1$, while the two branches are constructed in context
$\Gamma_2$. Since only one of the branches will be used, sharing
resources between the branches is expected.

One might wonder how, since constructing booleans is $0$-cost by their
introduction rules, the $\Gamma_1$ context will ever be non-$0$. This
is resolved by observing that booleans may be the output of processes
that consume time (e.g., the iteration constructs defined below), and
so $\Gamma_1$ will represent a requirement that the necessary resource
is provided.

§.§.§ Lists
Lists are a little more complex than booleans,
because the $\cCons$ constructor takes two arguments, so their
resource usage must be combined. The type formation and introduction
rules are as follows:

0Γ⊢σ: (T)

Γ_1 ⊢M σ: T

Γ_2 ⊢N σ: (T)

0Γ_1 = 0Γ_2
Γ_1 + Γ_2 ⊢(M,N) σ: (T)

Lists do have the potential for iteration by their recursive nature,
but in order to ensure the complexity guarantees we only permit
matching without recursion in the full calculus. Here is the rule for
dependently typed case analysis on lists:

0Γ_1, x 0: (T) ⊢P

Γ_1 ⊢M σ: (T)

Γ_2 ⊢N_1 σ: P[/x]

Γ_2, h σ: T, t σ: (T) ⊢N_2 σ: P[(h,t)/x]

0Γ_1 = 0Γ_2
Γ_1 + Γ_2 ⊢_x.P M { ↦N_1; (h,t) ↦N_2 } σ: P[M/x]

In the $\sigma = 0$ fragment, however, we are free to iterate on lists
because computations in this fragment are only meant for type-level
computation, not for the program itself. Put another way, the type
checker may perform arbitary recursion on lists to type check the
program, but the program itself may not do so without correctly
accounting its costs as described in the following sections. The
$\sigma = 0$ recursor for lists has the following typing rule, which
is the standard dependent eliminator for lists, with everything
annotated as $0$ usage.

0Γ, x 0: (T) ⊢P

0Γ⊢M 0: (T)

0Γ⊢N_1 0: P[/x]

0Γ, h 0: T, t 0: (T), p 0: P[t/x] ⊢N_2 0: P[(h,t)/x]
0Γ⊢recList_x.P M { ↦N_1; (h,t;p) ↦N_2 } 0: P[M/x]

§.§ Cons-free Natural Numbers and their Recursor

The datatypes of the previous section still only allow us to write
programs in the $\sigma = 1$ fragment that are constant time in the
size of their input. As with the simply typed linear system, if we are
handed a list of an unknown length, we can only explore it to a fixed
depth determined statically. To write programs that do work
proportional to the size of their input, we need some form of iterable
datatype. In both our Cons-free and LFPL-style QTT systems, we use a
natural number datatype.

The cons-free system cannot allow the programmer to construct natural
numbers in the $\sigma = 1$ fragment, as this would violate the
complexity guarantees. However, we can use the flexibility of QTT to
allow free construction of naturals in the $\sigma = 0$ fragment,
which allows us to use natural numbers freely in types. Therefore, we
have the following introduction rules, only usable in the $\sigma = 0$

Γ⊢M 0:
Γ⊢(M) 0:

The cons-free system allows free duplication of complete natural
numbers. This is accomplished by a special construct copying the
simply linear typed rule we gave above:

Γ⊢M σ:
Γ⊢dupNat(M) σ: ⊗

Anyone who has reasoned about the metatheory of or implemented a type
checker for dependent types will view this rule with unease as it
appears to grant the ability to construct non-canonical values of pair
type, and consequently generate non-canonical naturals. We fix this by
adding an equational rule to the $\sigma = 0$ fragment, ensuring
definitionally that $\mathrm{dupNat}$ acts as its name implies:

Γ⊢M 0:
Γ⊢dupNat(M) ≡(M,M) 0: ⊗

Note that this rule is well-typed by the $0$-needs-$0$ property of
QTT, and the fact that $0+0=0$.

The eliminator for these natural numbers takes the following
form. Disregarding the usage annotations, this has the same type
structure as the normal dependently typed recursor for natural

0Γ, x 0: ⊢P

Γ⊢M σ:

0Γ⊢N_z σ: P[/x]

0Γ, n 0: , p σ: P[n/x] ⊢N_s σ: P[(n)/x]
Γ⊢_x.P M {↦N_z; (n;p) ↦N_s} σ: P[M/x]

In the successor case, $N_s$, there are two bound variables: $n$ for
the natural number and $p$ for its induction hypothesis. Note that $n$
is required to be usage $0$ no matter what $\sigma$ is. We need the
variable $n$ to be present in order to correctly type the induction
hypothesis and the conclusion, but it must be marked as usage $0$ to
ensure that the resources captured by the number are not duplicated.

The reader is invited to compare this dependently typed rule with the
simply typed linear version in <ref>. Removing
the $0$-annotated parts of the rule, and the type dependency, yield
the exact same rule. Conversely, when $\sigma = 0$, this rule is
identical (up to $0$-annotations) to the usual dependently typed
recursor for natural numbers, and so we can use it in the types to
prove properties of programs just as we do in normal type theory. We
will see in <ref> that this rule is realisable
by polynomial-time computation, and so is sound for polynomial time.

§.§ LFPL-style Diamonds, Natural Numbers, and a Recursor that Gives Back

As explained in <ref>, the LFPL system differs from
the Cons-free system in that it is possible to construct natural
numbers (and other iterable datatypes), provided one has the necessary
diamonds to pay for the construction. As with the natural number type
in the Cons-free system, it ought not be possible to construct
diamonds in the $\sigma = 1$ fragment, as this would amount to the
free distribution of diamonds to all which would lead to a collapse in
the complexity guarantees of the system. It is possible construct
diamonds in the $\sigma = 0$, though:

0Γ⊢* 0:

Γ⊢M 0:
Γ⊢M ≡* 0:

The $\Diamond$ type also supports an $\eta$-rule in the $\sigma = 0$
fragment, indicating that, in this fragment, it acts the same as a
unit type. This allows us to use freely use diamonds in types, and to
not have to care about the identity of particular diamonds, since by
this rule all diamonds are definitionally
equal[Fungible, if one wishes to use a monetary

Construction of natural numbers now requires a $\Diamond$ for
$\conZero$ and a $\Diamond$ and a predecessor for $\conSucc$:

Γ⊢M σ:
Γ⊢(M) σ:

Γ_1 ⊢M σ:

Γ_2 ⊢N σ:

0Γ_1 = 0Γ_2
Γ_1 + Γ_2 ⊢(M,N) σ:

In the $\sigma = 0$ fragment, we can construct $\Diamond$s for free,
and so construct natural numbers freely as well just as we did for the
Cons-free system above.

The dependently typed recursor for LFPL-style natural numbers again
augments the simply typed linear recursor from
<ref> with dependency information:

0Γ, x 0: ⊢P

Γ⊢M σ:

0Γ, d σ: ⊢N_z σ: P[(*)/x]

0Γ, d σ: , n 0: , p σ: P[n/x] ⊢N_s σ: P[(*,n)/x]
Γ⊢ M {(d) ↦N_z; (d,n;p) ↦N_s} σ: P[M/x]

We have used $* : \Diamond$ as the value in the types for the zero and
successor cases. By the $\eta$-rule for diamonds, we could have
equally well used the $d$ variable that is in scope in each case.

Just as for the Cons-free system iterator above, in the $\sigma = 0$
fragment this rule is identical to the usual dependently typed
recursor for the natural numbers, so it can be used in the types to
reason about programs. Moreover, we will see in
<ref> that this rule is also sound for polynomial
time in a system with $\Diamond$s.

§.§ Reflection of Realisability

Our final addition to QTT is reflection of realisability. In
QTT thus far, it has been possible to reason about the non-resourced
behaviour of programs. This is because the $0$-ing process moving from
the $\sigma = 1$ fragment to the $\sigma = 0$ fragment erases all
resource information. This is sufficient for reasoning about the
extensional behaviour of programs via types, but it is useful to be
able to make statements like “this function is realisable in
polynomial time” in the types of QTT, something that is not currently
possible with the system we have seen so far.

We remedy this by adding a realisable type to QTT with the
following type formation and introduction and elimination rules:

0Γ⊢M 1: A
0Γ⊢(M) σ: (A)

Γ⊢M σ: (A)
Γ⊢(M) σ': A

Intuitively, the type $\Rtype(A)$ is inhabited whenever the type $A$
is realisable in the $\sigma = 1$ fragment of the system. In
particular, the type $\Rtype(\tyNat \to \tyNat)$ is the type of all
realisable functions from natural numbers to natural numbers. In the
polynomial time systems we are concerned with here, this is exactly
the type of polynomial functions. Note that in the introduction rule,
the premise is required to be in the $\sigma = 1$ fragment, to ensure
that the type is realisable, while in the elimination rule, the
conclusion is in an arbitrary fragment $\sigma'$. This flexibility is
require to maintain the admissibility of the $0$-ing rule.

With just the rules given here, the type $\Rtype(A)$ is no more than a
statement that a given type is realisable with a polytime
implementation. This is enough to do the constructions that we present
in the next section, e.g., that polytime functions are closed under
composition, but one could imagine stronger reflection principles that
allow deeper logical consequences of polytime realisability to be
proved internally. We discuss this further in

Readers familiar with <cit.>'s Linear/Non-linear system will
note that the $\Rtype(A)$ constructor is the QTT analogue of the right
adjont $G$ type constructor in that system. The $\Sigma$-types play
the role of the left adjoint $F$ types, in a similar way to the
dependent linear type system of <cit.>.

§ PROGRAMMING AND PROVING WITH POLYTIME

We now explore the possibilities afforded by the combination of
polytime guarantees with the specification expressivity of dependent

§.§ Building Datatypes

We have only defined an iterable natural number datatype for both of
our systems above. We could extend both systems to include further
iterable inductive types, although in the Cons-free system this
is not particularly useful due to the prohibition of on
construction. However, sticking with just the natural numbers, we can
use the power of dependent types with a universe to create further
datatypes whose size is measured by some iterable natural
number. Iteration on the size yields iteration over the full
datastructure. For example, in the LFPL system, we can define a type
of iterable lists by pairing a size with a type of elements defined by
recursion on the size:

IList A = (n 1: ) ⊗(rec_x.𝖴 n { (d) ↦I; (d,n;p) ↦A ⊗p })

The $\cNil$ and $\cCons$ constructors can now be defined in terms of
$\conZero$ and $\conSucc$, provided the caller supplies sufficient
$\Diamond$s. These definitions live in the $\sigma = 1$ fragment, so
we annotate them appropriately:

nil 1: →IList A

nil d = ((d), *)

cons 1: →A →IList A →IList A

cons d x 𝑥𝑠 = let (n,𝑒𝑙𝑒𝑚𝑠) = 𝑥𝑠 in ((d,n),(x,𝑒𝑙𝑒𝑚𝑠))

Using the LFPL iterator it is also possible to construct a dependently
typed iterator for $\mathrm{IList}\,A$ values. Unfortunately, the
current types of the LFPL system are not sufficient to type this as a
function, as we have no way of stating that the successor case must be
arbitrarily duplicable. Lifting this restrict by means of some
modality is future work. The typing rule for the derived list iterator

0Γ, x 0: IList A ⊢P

Γ⊢M σ: IList A

0Γ, d 1: ⊢N_1 σ: P[nil(*)/x]

0Γ, d 1: , x σ: A, xs 0: IList A, p σ: P[𝑥𝑠/x] ⊢N_2 σ: P[cons(*,x,𝑥𝑠)/x]
Γ⊢_x.P M {nil(d) ↦N_1; cons(d,x,𝑥𝑠;p) ↦N_2} σ: P[M/x]

Note that, in the cons case, we have access to the result of iterating
over the tail of the list ($p$), but not to the actual tail of the
list ($\mathit{xs}$).

With our list iterator, it is now possible to write interesting
polytime programs. For example, the example used by <cit.>
to demonstrate the expressivity of LFPL is insertion sort. First we
define insertion of a natural into a sorted list:

insert 1: →→IList →IList
which requires some ingenuity to write to handle the case where we
find the place to insert the item and need access to the remainder of
the list. Note that, also, the function consumes a $\Diamond$ to
construct the new element of the output list, and also that the items
in the list are themselves iterable natural numbers. This is needed to
account for the

Insertion sort is repeated insertion of elements from an original list
into a new list. The new list is constructed from the $\Diamond$s
yielded by the original list:

insertionSort 1: IList A →IList A

The immediate benefit of dependent types in this situation is that it
is now possible to state and prove the correctness property of this
sorting procedure. Using the fact that the $\sigma = 0$ fragment of
QTT is exactly normal type theory, we can use normal dependently typed
programmming techniques to establish:

insertionSortCorrect 0: (𝑥𝑠 1: IList A) →Sorted(𝑥𝑠,insertionSort xs)

where $\mathrm{Sorted}(x,y)$ is some predicate stating that $y$ is a
sorted permutation of $x$.  Note that, despite the $1$ annotation on
the $\Pi$-type here, we are free to duplicate $\mathit{xs}$ because
types are constructed in the $\sigma = 0$ fragment.

§.§ Polytime Problems

Define a decision problem to be a pair $(A, P)$, where $A$ is a type
in the universe $\mathsf{U}$, and $P : A \to \mathsf{U}$ is a
predicate on $A$. For what follows, we are only interested in whether
or not $P\,a$ is inhabited for each $a$. Therefore, we use
$P \Leftrightarrow Q$ to stand for equi-inhabitation of two
$P, Q : \mathsf{U}$, i.e.,
$P \Leftrightarrow Q \equiv (P \to Q) \times (Q \to P)$.

We can use the reflection type former defined in
<ref> to define a predicate on decision
problems that establishes whether or not they are polytime decision
problems. Specifically, we can state that there is a polytime
realisable boolean-value predicate that reports true exactly when the
given element of $a$ is in the predicate:

PTIME(A,P) =
(f 1: 𝐑(A →)) ⊗(a 1: A) →(𝐑^-1(f)  a = ) ⇔P a

Thus, $\mathrm{PTIME}(A,P)$ is a logical proposition stating that the
decision problem $(A,P)$ is deciable in polytime. We make two notes
about this definition: (i) this definition is intrinsic, in the sense
that, whichever of the polytime systems is chosen, proving that a
decision problem is solvable in polytime is a matter of programming,
without having to reason directly about machine models and step
counting; and (ii) we have defined problems to have arbitrary types
$A$ as domains, rather than bitstrings, and so the notion of size
attached to an input is intrinsic to the type $A$ chosen.

We can also declare a type of polytime reductions between
problems. A problem $(A, P)$ can be polytime reduced to a problem
$(B,Q)$ if there is an inhabitant of the following type:

(A,P) Poly⇒(B,Q) = (f 1: 𝐑(A →B)) ⊗(a 1: A) →Q(𝐑^-1(f) a) ⇔P a

In words, there must be a polytime function $f$ that preserves and
reflects decisions. With this definition, it is possible to prove in
our systems that polytime computations are closed under polytime
reductions. We note that this definition is, up to the reflection
modality, the same as the definition of cartesian container morphism,
well known in dependent type theory <cit.>, and speaks to a
general conception of containers as “problem/solution” pairings.

§.§ Polytime-based Complexity Classes

The fact that we can characterise polytime decision problems is
perhaps to be expected from a system designed to capture polynomial
time realisable programs. However, we can go further to capture the
complexity classes of Non-deterministic Polynomial time (NP) and
Probabilistic Polynomial time (PP), both of which are based on
polytime. We do this by augmenting our polytime functions with
additional power in the form of computation effects.

§.§.§ Non-deterministic Polynomial Time

To capture the complexity class NP, we use polynomial time programs
augmented with non-determinism, as one might expect. We will not need
to reason about equality of these non-deterministic programs, so we
can represent non-deterministic choices as additive binary
trees. We suppose a non-iterable datatype defined like so:

data ND (A : 𝖴) : 𝖴 where

𝗋𝖾𝗍𝗎𝗋𝗇 : A →ND A

𝖼𝗁𝗈𝗂𝖼𝖾 : (→ND A) →ND A

The crucial point here is that the subtrees are represented as a
function $\BoolTy \to \mathrm{ND}\,A$. By the typing rules of QTT,
this means that the two branches of this function can share resources
(see the encoding of the additive product types in
<cit.>). Thus, each branch of this tree is polynomial time,
not the whole tree itself.

The type $\mathrm{ND}$ supports a monad interface via the usual free
monad construction, as well as an effect
$\mathrm{flip} \stackrel1: \mathrm{ND}\,\BoolTy$ providing access to a
bit of non-deterministic information. Thus a program of type
$A \to \mathrm{ND}\,B$ in the $\sigma = 1$ fragment will be a polytime
program with access to an oracle. In the $\sigma = 0$ fragment, we can
write a function that resolves non-determinism using a list of
booleans. This function returns $\mathsf{nothing}$ if the list of
booleans is insufficient to resolve all the $\mathsf{choice}$s:

runWithOracle 0: ND A →() →Maybe A

With these definitions, we can define Non-deterministic Polynomial
time as a predicate on problems:

NP(A,P) =

(f 1: 𝐑(A →ND()))  ⊗

(a 1: A) →((𝑏𝑠 1: ()) ⊗(runWithOracle (𝐑^-1(f) a) 𝑏𝑠 = 𝗃𝗎𝗌𝗍 )) ⇔P a

Thus, a problem is in NP if there is a non-deterministic
boolean-valued polynomial time function that has a path to returning
$\cTrue$ exactly when the input is in predicate. Moreover, it is a
quick matter of programming to see that problems in NP are closed
under the type of polytime reductions given above.

§.§.§ Probabilistic Polynomial Time

By changing the computation effects supplied to a program, we can
change the complexity class. To capture Probabilistic Polynomial time,
we use a (non-iterable) data structure representing trees of
probabilistic choices, where $\mathbb{Q}[0,1]$ is some type of
(non-iterable) rationals in the closed interval $[0,1]$:

data Dist (A : 𝖴) : 𝖴 where

𝗋𝖾𝗍𝗎𝗋𝗇 : A →Dist A

𝖼𝗁𝗈𝗂𝖼𝖾 : ℚ[0,1] →( to Dist A) →Dist A

As in the non-deterministic case, a function $A \to \mathrm{Dist}\,B$
in the $\sigma = 1$ fragment is a polytime probabilistic
computation. Again, the use of a function type here ensures that each
branch of the tree is constructable in polynomial time, not the whole
tree. In the $\sigma = 0$ fragment we can write a function that
computes the probability of a $\mathrm{Dist}\,\BoolTy$ computation
being true:

probTrue 0: Dist →ℚ[0,1]

We can now define the class of probabilistic polynomial time decision
problems, where the decider is allowed to make probabilistic choices
as long as it is correct with probability at least $\frac{1}{3}$:

PP(A,P) =

(f 1: 𝐑(A →Dist()))   ⊗(a 1: A) →(probTrue (𝐑^-1(f) a) ≥1/3) ⇔P a

Again, problems in PP are easily seen to be closed under polytime

§ POLYTIME SOUNDNESS VIA REALISABILITY

In this section and the next, we establish the polytime soundness of
our extensions of QTT by adapting a realisability method due to
<cit.>. This approach is based on a three way
coupling between abstract mathematical elements (the what),
values from a machine model (the how), and resource potentials
(the fuel). Each type in the system is defined as a three way
relation between these elements. The set of abstract elements depends
on the type being interpreted (e.g., types of natural numbers will be
defined in terms of the set $\mathbb{N}$). The machine model is fixed
across all types. We describe the particular machine model we use for
this paper in <ref>. Potentials are arranged
into resource monoids that we define in
<ref>. Unlike <cit.>,
we explicitly construct realisers for inductive datatypes (both
iterable and non-iterable) instead of relying on second-order
polymorphic encodings and special $\oc$-style modalities. These
explicit constructions are essential to construct a model of dependent

Agda Formalisation The key soundness results in this
section have been formalised in the Agda proof assistant
<cit.>. The Agda formalisation can be found in
the supplementary material. After each definition and result we
provide a pointer to the Agda modules where the corresponding
formalisation can be found, and note interesting features of the

§.§ Machine Model and Operational Semantics

i,j    ∈   ℕ

E ∈   ::=    λE |* |(i, j) |||i | E_1  E_2 |i ·j | i  E | i E_1 E_2

V ∈   ::=    Eη |* |(V_1, V_2) ||

η   ::=     [] |η:: V

Evaluation: Construction

* [right=MkClo]

λE , η⇓_ Eη

* [right=MkUnit]

*, η⇓_ *

* [right=MkPair]
η[i] = V_1
η[j] = V_2
(i, j), η⇓_ (V_1, V_2)

* [right=MkTrue]

, η⇓_

* [right=MkFalse]

, η⇓_

Evaluation: Variable access and Sequencing

* [right=Access]
η[i] = v
i, η⇓_ v

* [right=Seq]
E_1, η⇓_k_1 V

E_2, (η:: V) ⇓_k_2 V'
E_1  E_2, η⇓_k_1 + + k_2 V'

Evaluation: Elimination

* [right=App]
η[i] = Eη'

η[j] = V

E , (η' :: Eη' :: V) ⇓_k V'
(i ·j), η⇓_+ k V'

* [right=LetPair]
η[i] = (V_1, V_2)

E, (η:: V_1 :: V_2) ⇓_k V
i  E, η⇓_+ k V

* [right=IfTrue]
η[i] =
E_1, η⇓_k V
i E_1 E_2, η⇓_+ k V

* [right=IfFalse]
η[i] =
E_2, η⇓_k V
i E_1 E_2, η⇓_+ k V

Language with CBV Big-step Costed Evaluation Semantics
Syntax and evaluation rules of the untyped CBV
$\lambda$-calculus used for realisers.

We demonstrate that every program that can be written in extensions of
QTT has the complexity bounds that we claim by translating QTT terms
into an untyped CBV $\lambda$-calculus with a costed operational
semantics. The syntax and rules of our target language are given in

Variables are represented as de Bruijn indicies $i, j$. Expressions
$E \in \ExpSet$ can be (anonymous) $\lambda$-abstractions, unit,
pairing and boolean values, variables, sequencing, application, pair
elimination, and conditionals. Note that, with the exception of
$\lambda$-abstraction and sequencing, expressions never contain nested
expressions; instead referring to variables already defined. Values
$V \in \ValSet$ can be closures $\clo{E}{\eta}$, where $\eta$ is an
environment for the closure, unit values, pairs and booleans.

Costed evaluation of expressions in environments is defined by a
big-step operational semantics $E, \eta \Downarrow_k V$, where $k$ is
the number of steps. For simplicity, all operations cost $1$ unit,
though this could be generalised to allow for different operations to
have different costs. We use $\eta[i]$ to access the $i$th variable in
the environment, counting from the right. The evaluation rules are
mostly as one would expect, except for the application rule which
includes a self reference to the closure being invoked, in order to
allow recursive definitions.

Agda Formalisation The machine model is defined in the
Agda module MachineModel. We use an intrinsicaly
well-scoped syntax, which ensures that all variable look up operations
are always well defined.

§.§ Resource Monoids

As we mentioned above, resource potentials are attached to values to
represent the amount of intrinsic potential they have to fuel
computation. Resource potentials are organised into resource
monoids. To be able to account for the combined potential attached to
composite data and programs (e.g., pairs, or functions applied to
arguments) we will require monoid structure on potentials. The action
of turning potential difference into fuel for computation will be
modelled by a difference function. Finally, we require that our
resource monoid contains sufficient elements to fuel constant time
operations. We gather these requirements into a formal definition as
follows, which is a slight reformulation of the resource monoids of

A resource monoid $M$ consists of:

* A carrier set $|M|$, whose elements represent amounts of
potential. We use Greek letters $\alpha$, $\beta$, $\gamma$ to
denote elements of a resource monoid.

* Commutative monoid structure $(\rplus,\rzero)$ on $|M|$, so
we can add potentials.

* a difference function $M : |M| \times |M| \to \natinf$,
where $\natinf$ is the natural numbers extended with a negative
infinity $- \infty$ and $- \infty + k = -\infty$. A difference
$M(\alpha, \beta) = k \in \mathbb{N}$ means that starting with
potential $\alpha$ and ending with potential $\beta$ yields $k$
units of fuel. A difference of $- \infty$ means that $\alpha$
contains insufficient potential to reach $\beta$. Differencing
must satisfy:

* for all $\alpha$, $M(\alpha,\alpha) = 0$; and

* for all $\alpha, \beta, \gamma$,
$M(\alpha, \beta) + M(\beta, \gamma) \leq M(\alpha, \gamma)$.

The latter is a “reverse triangle inequality”: the fuel
recoverable by moving between potential levels $\alpha$ and
$\gamma$ via $\beta$ may be less than the fuel recoverable
moving from $\alpha$ to $\gamma$ directly.

* Differencing and the commutative monoid structure must satisfy:

* $M(\alpha, \beta) \leq M(\alpha \rplus \gamma, \beta \rplus \gamma)$; and

* $M(\alpha, \rzero) = 0$.

* An accounting function
$\mathit{acct} : \mathbb{N} \to |M|$ such that for all $k$,
$k \leq M(\mathit{acct}(k),\rzero)$.

For any resource monoid $M$, we can define an action of $\mathbb{N}$
on $M$ as $n \cdot \alpha = \alpha \oplus \cdots \oplus \alpha$, where
the right-hand side has $n$ summands.

Alternative definition Every resource monoid induces a
pre-ordering on its carrier set by $\alpha \leq \beta$ iff
$0 \leq M(\alpha, \beta)$. Taking this idea further, we can
reformulate a resource monoid as a symmetric monoidal category
enriched in the symmetric monoidal category $\natinf$, where the
monoid structure is addition. The conditions in the definition above
amount to the usual identity and composition laws for enriched
categories. With this reading, we can see the value $M(\alpha,\beta)$
when it is $\geq 0$ as the possibility of moving from $\alpha$ to
$\beta$ levels of potential resource with some amount of residual
resource emitted for computation; when it is $-\infty$, moving from
$\alpha$ to $\beta$ is not possible.

Agda Formalisation Resource monoids are defined in the
module Algebra.ResourceMonoid. We use a formulation
closer to the enriched category theory definition for the actual
formalisation, because it avoids having to treat equality in the
monoid structure separately from the induced preorder on
elements. Thinking of proofs involving the resource monoid as a
process of finding a composable sequence of morphisms in a category
was a helpful intuition when constructing the realisability model

§.§.§ Specific Resource Monoids

The simplest example of a resource monoid is given by the natural
numbers $\mathbb{N}$, where each number stands directly an amount of
stored fuel.

Monoid structure is given by normal addition. Differencing is
defined as

ℕ(m,n) = {

m - n     m ≥n

- ∞    otherwise

and $\mathit{acct}(k) = k$. Note that this is the simplest possible
resource monoid due to the requirement that the $\mathit{acct}$
function must exist.

The differencing operator of the natural number resource monoid can
only supply as much fuel as is contained in the potential.

For the two polynomial time systems, we need more sophisticated
structures, both originally presented by Dal Lago and Hofmann. The
fundamental idea with both is to represent potentials as pairs
$(m,p)$, where $m$ is a natural number and $p$ is a polynomial. The
$m$ tracks the “size” of data as it pertains to the number of times
an operation will be repeated by iterating over it — for example, an
iterable natural number will have size equal to itself, but a
non-iterable natural number may be assigned zero size. The polynomial
$p$ tracks the complexity of a program as a function of the size of
the input. This leads to a differencing operator that evaluates the
polynomial with the size of the data:

The Max-Polynomial resource monoid $\MaxPoly$ has carrier set
consisting of pairs $(m,p)$ where $m$ is natural number and $p$ is a
polynomial with natural number coefficients. Addition of elements is
defined as $(m,p) \oplus (n,q) = (m \sqcup n, p+q)$, where $\sqcup$
is the max operator, with $\emptyset = (0,0)$. Difference is defined

((m,p),(n,q)) = {

p(m) - q(m)   m ≥n  and  ∀k ≥m. p(k) ≥q(k)

- ∞    otherwise

$\MaxPoly$ accounts for constant time with constant polynomials:
$\mathit{acct}(k) = (0,\lambda x.k)$.

The Plus-Polynomial resource monoid $\PlusPoly$ is defined
the same way as $\MaxPoly$ except that the monoid addition adds the
natural number components instead of taking their maximum:
$(m,p) \oplus (n,q) = (m + n, p+q)$.

It is perhaps easier to see how the differencing operator works in the
special case of the difference $\MaxPoly((m,p),(0,0)) = p(m)$. I.e.,
if we have code that contains data of size $m$ and a program with
complexity $p$, then running the combination with no expectation of
remaining potential yields $p(m)$ available steps. The $\MaxPoly$ and
$\PlusPoly$ resource monoids will be used for the Cons-free and
LFPL-style systems respectively, as we explain in
<ref> and show how these resource monoids
yield the required polytime bounds on programs.

Agda Formalisation The $\mathbb{N}$ resource monoid is
defined in Algebra.ResourceMonoid.Nat and the polynomial
monoids are both defined in
Algebra.ResourceMonoid.Polynomial. The definition is
parameterised by the “size monoid” operation (either $\sqcup$ or
$+$) used to compose sizes.

§.§.§ Resource sub-monoids

The separation between sizes of data and complexity of code in the
polynomial resource monoids motivates the use of resource sub-monoids
to ensure that programs themselves (as opposed to higher order code
which may contain closed over data) do not contain data that can be
iterated. We do this by requiring that programs' potential must come
from a specified resource sub-monoid:

A resource sub-monoid $M_0 \subseteq M$ of a resource monoid
$M$ consists of a subset $|M_0| \subseteq |M|$ that is closed under
the monoid operations and $\mathit{acct}$.

For both $\MaxPoly$ and $\PlusPoly$, the elements with zero size
component, i.e., of the form $(0,p)$, form a resource sub-monoid that
we will use for interpreting programs. We will call these sub-monoids
$\MaxPoly_0$ and $\PlusPoly_0$.

§.§ Models of Quantitative Type Theory from Indexed Preorders

<cit.> described a general class of QTT models termed
Quantitative Categories with Families (QCwFs). This class of
models fits well with the syntax of QTT, but to actually build models
it is convenient to construct them from certain indexed linear
preorders. The BCI-realisability model construction given by
<cit.> is a special case of this construction, so we only
sketch a special case here to concentrate on the specifics of
complexity bounded realisability.

A $\mathbb{N}$-linear preorder is a preordered set
$(L, \leq)$ with

* a commutative monoid $(I, -\otimes-)$ that is monotone
w.r.t. the order;

* is closed: there is an operation
$\multimap : L \times L \to L$ such that $x \otimes y \leq z$ iff
$x \leq y \multimap z$; and

* has a function $\oc : \mathbb{N} \to L \to L$, to interpret
resource requirement adjustments, satisfying:

* $\oc_0 X \simeq I$, for discarding;

* $\oc_{m+n} X \leq (\oc_m X) \otimes (\oc_n X)$, for duplication;

* $\oc_m\oc_n X \leq \oc_{mn} X$ for nesting;

* $\oc_1 X \leq X$ for extraction / dereliction;

* $(\oc_n X) \otimes (\oc_n Y) \leq \oc_n(X \otimes Y)$, for distribution; and

* $n \leq m$ implies $\oc_n X \leq \oc_m X$, for usage weakening.

The collection of all linear preorders and functions that preserve the
order and the operations forms a category $\LinPreorder$.

An indexed linear preorder $L : \Set^\op \to \LinPreorder$ is
a contravariant function, where we write $f^* : L(B) \to L(A)$ for
the action of $L$ on functions $f : A \to B$, such that such that
reindexing along projections has a right adjoint
$L_{\Sigma_{a \in A}.B}(\pi_1^*X, Y) \cong L_{A}(X, \forall_B Y)$
that commutes with reindexing.

Given an indexed linear preorder $L : \Set^\op \to \LinPreorder$, we
construct a QCwF model of QTT with the basic type formers from

* Define a category $\cat{L}$ of interpretations of contexts with
objects that are pairs $(A \in \Set, X \in L(A))$ and morphisms
$f : (A,X) \to (B, Y)$ that are functions $f : A \to B$ such that
$X \leq f^*Y$ (this is the Grothendieck category of $L$). There is a
faithful functor $U : \cat{L} \to \Set$. The category $\cat{L}$ will
be used for interpreting contexts in the $\sigma = 1$ fragment of

* Define scaling of objects of $\cat{L}$ by
$\pi(A,X) = (A, \oc_\pi X)$, and addition of $(A, X)$ and $(A, Y)$
as $(A, X \otimes Y)$.

* For each set $A$, define the collection of semantics types
$\Ty(A)$ as the collection of $B : A \to \Set$ and
$X \in L(\Sigma_{a \in A}.B(a))$. Thus a QTT type consists of an
extensional meaning $B$ and its realisability specification $X$.

* For each $A$ and $(B,X) \in \Ty(A)$, the $\sigma = 0$ fragment
terms $\Tm(A,(B,X))$ are functions $\Pi_{a \in A}.\,B(a)$. For each
context interpretation $(A, X)$ in $\cat{L}$ and type intepretation
$(B,Y) \in \Ty(A)$, the $\sigma = 1$ fragment terms
$\RTm((A,X),(B,Y))$ are functions $f : \Pi_{a \in A}.\,B(a)$ such
that $X \leq \overline{f}^*Y$, where
$\overline{f} : A \to \Sigma_{a \in A}.\,B(a)$ is the section
associated with $f$.

* The empty context is interpreted as $(\{*\}, I)$ and context
extension $(A,X).n(B,Y)$ (i.e., comprehension) by
$(\Sigma_{a \in A}.B(a), \pi_1^* X \otimes \oc_n Y)$.

* Given $(A,X) \in \Ty(C)$ and
$(B,Y) \in \Ty(\Sigma_{c \in C}.A(c))$, $\Sigma$-types are
interpreted similarly to context extension and $\Pi$-types are
interpreted as
$(\lambda c.~(\Pi_{a \in A(c)}.\,B(c,a)), \forall_{A}(X \multimap
(\mathit{ev}\,f)^*Y))$, where
$\mathit{ev}\,f : (\Sigma_{c \in C}.A(c)) \to (\Sigma_{c \in
C}.\Sigma_{a \in A(c)}.B(c,a))$ is defined using application of

* Universe and Equality types are interpreted as normal in $\Set$
with the realisability component set to $I$ in both cases. Note that
the universe of small types includes resource-relevant realisability
information for each type.

* Realisability reflection for a type $(B,X) \in \Ty(A)$ is
intepreted as the type
$(\lambda a. \{ b \in B(a) \mid I \leq (\lambda a. (a,b))^*X \},
I)$. Thus the set-component of the type is restricted to the
elements that are realisable, while the actual realisability
component is the “empty” $I$ realisability specification.

Agda Formalisation The indexed linear preorders are
defined in the Agda module IndexedLinear. We have not yet
completed a formalisation of the construction of a full model of QTT
from an indexed linear preorder so this part is currently unmechanised.

§.§ Amortised Complexity Realisability Model

Equipped with our underlying costed model of computation
(<ref>) and a compositional notion of resource
potential (<ref>), we can construct models of
QTT that witness the resource and type soundness of our complexity
constrained systems. We fix a resource monoid $M$ with sub-monoid
$M_0$ and proceed to build an indexed linear preorder of resource
accounted realisers.

§.§.§ Indexed Linear Preorder

We now define an indexed linear poset $L$ of realisers over $\Set$
that ties together our “mathematical” model of types in $\Set$ with
our machine model and resource monoid. This construction is a
reformulation of <cit.>'s realisability models
suitable for modelling dependent types. For a set $A$, the carrier of
$L(A)$ is the set of ternary relations
$X \subseteq A \times M \times \ValSet$ and we define the ordering
$X \leq Y$ to hold iff there exists realising expression
$E \in \ExpSet$ and potential $\gamma \in M_0$ such that for all
$a \in A$, $\alpha \in M$ and $v \in \ValSet$ with
$(a,\alpha,v) \in X$, we have that there exists a result
$v' \in \ValSet$, step count $k \in \mathbb{N}$ and result potential
$\beta \in M$ with:

* $E, v \Downarrow_k v'$ (evaluation successfully completes in $k$ steps);

* $(a, \beta, v') \in Y$ (the result is well-resourced and
satisfies $Y$); and

* $k \leq M(\alpha \rplus \gamma, \beta)$ (the step count is within the
difference between the initial potential and the result potential).

Note that the definition of realisablity is uniform in the element $a$
– the realising expression $E$ and the potential $\gamma$ must work
for all $a$ – thus the implementation and complexity measure of the
transition being modelled cannot depend on what the input is. Put in
implementation terms, the input $a$ is not present at
runtime. Moreover note that the potential $\gamma$ attached to the
expression $E$ must come from the sub-monoid $M_0$, indicating that is
intended to be data-free, while the potential $\alpha$ for the input
is from the full monoid $M$, so it can contain data and functions.

For $X, Y \in L(A)$, the required elements for symmetric monoidal
closed structure are defined as follows. For the tensor product
$X \otimes Y \in L(A)$, the realising value must be a pair $(v_1,v_2)$
and the potential of the pair must split into suitable potentials
$\alpha_1$, $\alpha_2$ for the components. For the residual
$X \multimap Y$, the realising value must be a closure with potential
to, when added to the potential of an input, compute the output with
enough remaining. Note that the potential attached to a closure
($\alpha$, here) need not be from the sub-monoid $M_0$. Unlike
top-level term interpretations, closures may contain data.

X ⊗Y    =    { (a, α, (v_1, v_2)) |∃α_1, α_2. 0 ≤M(α, α_1 α_2) X(a,α_1,v_1) Y(a,α_2,v_2) }

X ⊸Y    =    { (a, α, Eη) |
∀α' ∈M, v,w ∈. X(a,α',v) ⇒

∃v', k, β.
E, (η:: w :: v) ⇓_k v' Y(a,β,v') k ≤M(αα', β) }

The seemingly useless $w \in \ValSet$ in the formula for
$X \multimap Y$ is a dummy argument standing for the self-referential
reference to the closure used for defining recursive programs.

Each $L(A)$ has a terminal (i.e. top) element, which is also the unit
for $\otimes$, defined as
$I_A = \{(a, \alpha, *) \mid a \in A, \alpha \in M\}$. The potential
$\alpha$ here is unrestricted, so $I_A$ can consume an arbitrary

$\mathbb{N}$-Graded exponentials in each $L(A)$ are defined using the
action of $(\mathbb{N}, \leq)$ on $M$ defined above. The modality
$\oc_n$ has no effect on realising values. It only serves to alter the
resource potentials.

_n X = {(a,α,v) |∃α'. M(n ·α', α) = 0 (a, α', v) ∈X }

$L$ also has arbitrary $\Set$-indexed products, realised “lazily” as
functions that take dummy arguments. For $A \in \Set$ and
$B \in A \to \Set$ and $X \in L(\Sigma A.\,B)$, we define
$\forall_B X \in L(A)$ similarly to $\multimap$ above, but with
different resource and indexing requirements:

∀_B X = { (a,α,Eη) |∀b, v. ∃v', β, k. E, (η:: v :: *) ⇓_k v' X((a,b),β,v') k ≤M(α,β) }

Note, as with the definition of $X \leq Y$ above, the realiser closure
$\clo{E}{\eta}$ must be chosen uniformly for all $b$. This definition
also appears to allow arbitrary computation (paid for by $\alpha$) to
happen when the realising closure is applied, but the potential
$\alpha$ will only ever be greater than $\beta$ by enough to handle
the administrative costs of applying the function.

To complete the construction of $L$ as an indexed linear preorder, we
need to give realisers for each of the required inequalities in
def:indexed-linear-preorder. In each case, this is a matter
of programming in the language of <ref>. For
example, transitivity of the order is realised by sequencing of
expressions. The potentials are calculated by counting the steps in
the ensuing programs.

$L$, with $I$, $\otimes$, $\multimap$, $\oc_n$, and $\forall_{B}$
defined above, is an indexed linear preorder.

Agda Formalisation The construction of this indexed linear
preorder and the proof of prop:realisability-model are
formalised in the Adga module

§.§.§ Non-iterable Data Types

The model of QTT constructed in prop:realisability-model
does not yet include any useful base types. Iterable types, which are
the ones that induce non-constant time complexities, require specific
properties of resource monoids that we introduce in

Before that, we show how to define realisers for the representative
examples of non-iterable types from <ref>
and <ref>. Booleans are the simplest case, with
only two cases and no chance of iteration. Lists are more complex; we
can have non-iterable lists containing iterable data.

Booleans Fix $\mathbb{B} = \{ \mathit{tt}, \mathit{ff} \}$
as our set of boolean elements. We define an element of
$L(\mathbb{B})$ to represent boolean values:

Bool = { (𝑡𝑡, α, ) |α∈M } ∪{ (𝑓𝑓, α, ) |α∈M }

Thus, the boolean $\mathit{tt}$ is represented by the value $\synTrue$
and $\mathit{ff}$ is represented by $\synFalse$. In both case, we
allow arbitrary potential $\alpha$ to be attached.

Realisability of the construction and elimination of booleans amounts
to the existence of the following inequalities. In any preorder
$L(A)$, we have $I_A \leq \mathit{tt}^* \mathrm{Bool}$ and
$I_A \leq \mathit{ff}^* \mathrm{Bool}$ (treating $\mathit{tt}$ and
$\mathit{ff}$ as constant functions $A \to \mathbb{B}$). These
inequalities are realised by the corresponding $\synTrue/\synFalse$
expression. For conditionals, the types involved are a little more
complex to ensure agreement between boolean manipulations at the
$\Set$-level and the realising computations. To get a realiser for a
conditional, we require a set $A$, an element $X \in L(A)$ (standing for
the context) and an element $Y \in L(A \times \mathbb{B})$ (standing
for the target type) and the existence in $L(A)$ of inequalities
$X \leq (\lambda a. (a, \mathit{tt}))^* Y$, for the true case, and
$X \leq (\lambda a. (a, \mathit{ff}))^* Y$, for the false case. When
we have all these, we get in $L(A \times \mathbb{B})$ an inequality
$\pi_1^* X \otimes \pi_2^* \mathrm{Bool} \leq Y$. This construction
suffices to realise the rules for QTT booleans in

Lists Lists are a little more involved, due to the need to
explicitly manage a context that applies to all elements of the
list. Let $\mathrm{List}(B)$ be the set of lists with elements from a
set $B$. If we have $A : \Set$ and $B : A \to \Set$ and
$X \in L(\Sigma a:A.\, B a)$, then we the resourced lists predicate
$\mathrm{RList}(X) \in L(\Sigma a : A.\, \mathrm{List}(B a))$ must
satisfy the equation:

RList(X) =

{ ((a, []), α, (, *)) |α∈M }

((a, b :: bs), α, (, (v_1, v_2))) |

∃α_1, α_2. 0 ≤M(α, α_1 ⊕α_2) ((a, b), α_1, v_1) ∈X ((a, bs), α_2, v_2) ∈RList(X) }

This equation has a least solution, by induction on the length of the
list being realised. This definition is somewhat involved, but in
essence states that a list is represented by tagged pairs, where
$\synFalse$ represents nil and $\synTrue$ represents cons, and that
the potential is distributed amongst the elements of the list as

Agda Formalisation The construction of realisers for
booleans and lists are carried out in the Agda modules
AmortisedModel.Bool and AmortisedModel.List.

§ REALISING ITERATION FOR IMPLICIT POLYNOMIAL TIME

The models constructed in the previous section only allow for
constant-time programs to be realised. To interpret the iterators of
the Cons-free and LFPL-style systems, we need to use the
$\MaxPoly$ and $\PlusPoly$ resource monoids. We do this in this
section, where first we establish some operations that will be useful
to see how they capture the nesting of iterations inherent to polytime

§.§ Iteration Resource Monoids

To interpret iteration over a resource monoid $(M, M_0)$, we require
additional structure, which we call an Iteration Resource
Monoid to account for measurement of the sizes of iterable data
structures and the effects of iteration on potentials.

§.§.§ Definition

We require:

* a function $\mathit{size} : \mathbb{N} \to M$ that gives the
potential of an iterable data structure of a given

* a function $\mathit{raise} : M \to M$ that raises the
(polynomial) degree of some potential; and

* a function $\mathit{scale} : \mathbb{N} \times M \to M$ that
scales a potential for a fixed number of iterations.

These functions must satisfy the following properties:

* $M_0$ is closed under the $\mathit{raise}$ operation;

* for all $\alpha$ and $n$,
$0 \leq M(\mathit{raise}(\alpha) \oplus \mathit{size}(n),
\mathit{scale}(n,\alpha) \oplus \mathit{size}(n))$; and

* for all $\alpha \in M_0$ and $n$,
$0 \leq M(\mathit{scale}(1 + n, \alpha), \alpha \oplus
\mathit{scale}(n, \alpha))$.

The first property states that $\mathit{raise}$ is suitable as
potential for whole programs2, meaning that it does not make any
requirements on the existence of iterable data. Note that we do
not require $M_0$ to contain $\mathit{size}(n)$ – programs
themselves may not contain iterable data, all potential for iteration
must be delivered externally. A useful intuition is that
$\mathit{scale}(n,\alpha)$ represents the potential required for at
most $n$ iterations that require potential $\alpha$, whereas
$\mathit{raise}(\alpha)$ represents the potential required for a
number of iterations that depends on the context. This is the
motivation behind the second required property, which states that
having $\mathit{raise}(\alpha)$ potential implies having
$\mathit{scale}(n,\alpha)$ potential when the current size is $n$. The
third property states that $\mathit{scale}$ decomposes as expected on
potentials that do not include any size potential.

Note that $\mathit{scale}(n,\alpha)$ is not the same as the action
$n \cdot \alpha$ defined in <ref>. The latter
operation scales both size and function potential, but the former only
scales the function potential.

§.§.§ Polynomial Iteration Resource Monoids

Both of the polymonial resource monoids defined in
def:polynomial-resource-monoids support the structure of an
Iteration Resource Monoid. We define:

* $\mathit{size}(n) = (n, 0)$

* $\mathit{raise}(n, p) = (n, xp)$

* $\mathit{scale}(m, (n, p)) = (n, m \cdot p)$

Note that $\mathit{raise}$ does indeed raise the degree of the
polynomial involved. Property 2 above is satisfied because for any
polynomial we have $(m \cdot p)(x) \leq (xp)(x)$ whenever $m \leq x$.

§.§.§ Realising Iterable Natural Numbers

For any natural number $n$, we define its representation as a value
$\mathrm{natValue}(n) \in \ValSet$ by recursion:

natValue(0) = (, *)

natValue(1 + n) = (, natValue(n))

This representation uses a tagged pair approach similar to our
representation of lists in <ref>. Using this, we
can define what it means for a natural number to be realisable via
$\mathrm{Nat} \in L(\mathbb{N})$:

Nat = {(n, α, natValue(n)) |n ∈ℕ, 0 ≤M(α, 𝑠𝑖𝑧𝑒(n+1)) }

So a natural number $n$ is realised by the value
$\mathrm{natValue}(n)$ as long as we have at least
$\mathit{size}(n+1)$ potential (we add one to make the LFPL soundness
proof easier).  This gives us the ability to represent natural numbers
as a type in QTT, but in order to iterate (and construct in the case
of LFPL), we need to construct specific realisers for the
Cons-free and LFPL systems.

§.§ The Cons-Free System

The Cons-free system uses the $\MaxPoly$ resource monoid, with
the distinguished sub-monoid being those elements that are $0$ in the
size component. We enumerate the features of the Cons-free
system and justify their realisability with the $\MaxPoly$ resource

* Duplication of natural numbers by $\dupNat(M)$ is realisable by
the expression $(0,0)$, which creates a pair by copying the input
variable twice. By the cost semantics in
<ref>, this takes $1$ step of computation (we
assume that it is actually implemented via some pointer copy).  The
resource accounting for this realiser works because the size
component required for the output is the maximum of the size
components of the two elements, and since $n \sqcup n = n$, we have
enough resources to fulfil this.

* Construction of natural numbers is not realisable. In a putative
$\conSucc$ rule, we would need to get an additional unit of size
resource from nowhere.

* Iteration is realised by constructing a realising expression in
the expression language from the given expressions for the zero and
successor cases that uses the in-built recursion of the
language. The proof that resources are correctly accounted for is
carried out by induction on the natural being iterated over. For
$n$, we require potential
$\mathit{scale}(n,\mathit{acct}(4) \rplus \gamma_{\mathit{succ}})
\rplus (\mathit{acct}(2) \rplus \gamma_{\mathit{zero}})$, where
$\gamma_{\mathit{succ}}$ and $\gamma_{\mathit{zero}}$ are the
potentials required by the successor and zero cases respectively. By
Property (2) of iteration resource monoids, above, we know that
$\mathit{raise}(\mathit{acct}(4) \rplus \gamma_{\mathit{succ}})
\rplus (\mathit{acct}(2) \rplus \gamma_{\mathit{zero}})$ always
dominates this requirement when paired with the potential
$\mathit{size}(n)$ from the input. Therefore, this latter
expression, plus some administrative set up costs, is the required
potential for the whole iterator.

Together, we have a soundness result for the Cons-free system,
that ensures that every term in the $\sigma = 1$ fragment is
realisable by a correct program that terminates in polynomial
time for all inputs:

If we have a term $n : \tyNat \vdash M \stackrel1: T(n)$ then there
exists a realising expression $E$ and polynomial $p$ such that for
all $n \in \mathbb{N}$, there exists $v \in \ValSet$ and
$k \in \mathbb{N}$ such that
$E, [\mathrm{natValue}(n)] \Downarrow_k v$, $k \leq p(n)$ and $v$ is
a realising value for
$\llbracket M \rrbracket(n) \in \llbracket X \rrbracket(n)$.

Agda Formalisation The realisability of the
Cons-free system iterator and the soundness property of the
whole system are formalised in the Agda modules ConsFree
and ConsFree.Iterator. The soundness theorem is a
combination of this and the QTT model sketched in

§.§ The LFPL System

The LFPL system uses the $\PlusPoly$ resource monoid, with the
distinguished sub-monoid again being those elements that are $0$ in
the size component. With this resource monoid, the capabilities
offered at the QTT level are altered:

* We can no longer duplicate natural numbers, because
$\tyNat \otimes \tyNat$ requires twice as much size resource as
$\tyNat$, due to the combining operation on size potentials being

* We define the realisability specification for diamonds
$\Diamond \in L(1)$ to be
$\Diamond = \{ (*, \alpha, *) \mid 0 \leq M(\alpha,
\mathit{size}(1)) \}$.  Thus, a diamond represents at least one unit
of size resource, matching the intuitive explanation given in

* With this definition of realisability for $\Diamond$s, it is
possible to realise the $\conZero$ and $\conSucc$ constructors for
natural numbers. By the additive combination of size resources we
get $1$ from the diamond and $n+1$ from the predecessor to total
$n+2$ for a new number. Note that, even if we add a $\Diamond$ type
to the Cons-free system, it would still not be possible to
realise the constructors, because we would only have
$1 \sqcup (n+1) = n+1$ size resource for the output.

* The construction of the recursor follows a very similar proof to
the realisability of Cons-free iterator, up to some
additional work to make sure that the dummy $*$ values representing
the diamond components end up in the right places. This additional
work is revealed in the required potential for the LFPL iterator
$\mathit{raise}(\mathit{acct}(8) \rplus \gamma_{\mathit{succ}})
\rplus (\mathit{acct}(2) \rplus \gamma_{\mathit{zero}})$, so
slightly higher in the successor case.

Soundness for the LFPL system is similar to the Cons-free
system, except for a $+1$ to the input to the polynomial, to account
for the fact that we cost one size unit for the $\conZero$

If we have a term $n : \tyNat \vdash M \stackrel1: T(n)$ then there
exists a realising expression $E$ and polynomial $p$ such that for
all $n \in \mathbb{N}$, there exists $v \in \ValSet$ and
$k \in \mathbb{N}$ such that
$E, [\mathrm{natValue}(n)] \Downarrow_k v$, $k \leq p(n+1)$ and $v$
is a realising value for
$\llbracket M \rrbracket(n) \in \llbracket X \rrbracket(n)$.

The proofs of well-accounted realisability for the LFPL iterator, and
the Cons-free iterator, could be adapted to any other
inductively defined type that is finitely branching. This is not
immediately necessary, as evidenced by the construction of other
datatypes in <ref>. Nevertheless, native tree
type where the iterability is proportional to the total number of
nodes would be useful.

Agda Formalisation The realisability of the LFPL system
iterator and the soundness property of the whole system are formalised
in the Agda modules LFPL and LFPL.Iterator.

§ RELATED AND FUTURE WORK

We have presented two extensions of Quantitative Type Theory that
soundly and completely capture polynomial time. We have seen that this
allows for an expressive combination of verification and complexity
constrained computation. We now discuss some related work in implicit
computational complexity and linear dependent types, and take a look
at where the combination of resource conciousness and dependent types
could take us.

§.§ Related Work

Implicit Computational Complexity with Linear Types
Implicit Computational Complexity <cit.> is a vast field, so we
only survey closely related works. We have already mentioned the
Bounded Linear Logic <cit.>, Soft Affine Logic <cit.>,
Light Linear Logic <cit.> and LFPL <cit.> systems,
which all use linear typing to implicitly capture polynomial
time. <cit.> characterises polynomial time using first-order
functional programs without constructors. Thus it shares a method with
our Cons-free system, but we use linear typing to permit
controlled use of higher-order functions. Other approaches to
polynomial time use stratification or information flow tracking to
ensure that the outputs of iteration may not be used unrestrictedly to
drive further iteration. For example, <cit.> and
<cit.>. Below polynomial time, systems have be devised to
capture LOGSPACE <cit.>. Above polynomial time, systems such
as Elementary Affine Logic (EAL) capture all Elementary-time functions

We have used <cit.>'s technique to prove
soundness of our extension of QTT. This technique has been
successfully applied to many other linear typing based systems, such
as BLL <cit.> and LLL
<cit.> and EAL. In contrast to most of those systems, we do
not use restricted $\oc$-modalities and second order encodings to
express datatypes. Our explicit datatype approaches enabled our
combination of dependent types and polynomial time.

Explicit Resource Accounting with Dependent Types In
contrast to the implicit systems, previous works have constructed
systems that give explicit resource bounds via typing. Examples
include <cit.>'s Resource Allocated ML (RAML) and
<cit.>, both of which are based on ideas of type-based
amortised complexity analysis arising from <cit.>'s
ideas, via the work of <cit.>. More details are to be found
in the survey paper of <cit.>. A approach is to track
costs at the value level instead of the types. <cit.>
describes a system that uses a “tick” effect to count steps of
computation, which can be reasoned about via dependent
types. <cit.> take this idea further by employing a
modality-based phase separation to ensure that tick counting never
interferes with the functional business of
programs. <cit.> is another tick effect based system
in Coq. All of these techniques rely on the programmer correctly
annotating the program with tick effects to count the resource usage
they are interested in, in contrast to the intrinsic approach we have
taken here.

Linear and Substructural Dependent Types We chose QTT as
the particular combination of linear and dependent types for our
systems. Other systems include systems such as those by
<cit.> which all use a strict
separation between linear and non-linear variables. This strict
separation would mean that we could not as easily move programs from
the linear fragment into the types, as in
<ref>. Systems that are more like QTT in
that they do not have a strict separation of variables include those
of <cit.>. These systems differ from
QTT in that they do not include a complete copy of unrestricted type
theory as QTT does in its $\sigma = 0$ fragment, because they all
track usage in types as well as terms, so it is not clear how to use
them for unrestricted reasoning as we do with QTT. <cit.>
present a system that is closer to QTT but does not include a universe

§.§ Future Work

Implementation We currently lack an implementation of our
extension of QTT, which hampers further investigation of programming
and proving with polytime along the lines of
<ref>. Idris 2 <cit.> is an
implemenation of QTT, but cannot be used directly because its facility
for defining datatypes is too liberal, not making a distinction
between iterable and non-iterable datatypes. A further
implementation-focused question is whether or not the term-level
polytime guarantees can be turned to type-level guarantees to
guarantee polytime typechecking.

Other Complexity Classes, and Explicit Resource Tracking
It seems feasible to adapt the techniques presented here to other
complexity classes such as LOGSPACE and ELEMENTARY, given the simply
typed linear systems mentioned above. Also, our construction already
includes soundness of a system with intrinsic but explicit resource
tracking where $\Diamond$s are used to pay for every step of
computation but never returned, via the natural number resource monoid
defined in <ref>. Investigation of such a
system may yield a system that tracks costs intrinsically and

Towards Synthetic Computational Complexity Theory?

The realisability type $\mathbf{R}(A)$ described in
<ref> allows us to internalise the
realisability of certain functions into the logical ($\sigma = 0$)
fragment of the calculus. However, it is not possible to derive any
logical consequences from this other than turning it back into a
function. This limitation becomes acute when trying to prove results
from standard Computational Complexity theory. Even though we can
characterise the class NP, as we did in <ref>, we
cannot prove the Cook-Levin theorem that 3-SAT is NP-complete. This is
because the proofs relies on obtaining the source code of the
program solving an NP problem and then encoding that program in
3-SAT. To do this in our setting, we would need to internalise the
soundness property (thm:lfpl-soundness) as an axiom, stating
that for a realisable polytime function there (merely) exists a
realising expression $E$ that completes in polynomial time, and then
writing polytime enodings into 3-SAT. We hope that the addition of
such an axiom to our system would lead to an expressive machine-free
Synthetic Computational Complexity Theory, analogous to the
Church-Turing axiom for Synthetic Computability Theory <cit.>.

This work was funded by the EPSRCEngineering and
Physical Sciences Research
Councilhttps://www.ukri.org/about-us/epsrc/. Grant number
EPSRCEP/T026960/1, AISEC: AI Secure and
Explainable by Construction.

#1     #1#1#1     #1     #1     #1     #1#1          #1#1

[Abbott et al(2005)]
authorpersonMichael Gordon Abbott,
personThorsten Altenkirch, and personNeil Ghani.
Containers: Constructing strictly positive types.
journalTheor. Comput. Sci. volume342,
number1 (year2005), pages3–27.

authorpersonAndreas Abel.
Resourceful Dependent Types. In
booktitleAsbtract for 24th International Conference on Types
for Proofs and Programs.

[Aehlig and Schwichtenberg(2002)]
authorpersonKlaus Aehlig and personHelmut
Schwichtenberg. year2002.
A syntactical analysis of non-size-increasing
polynomial time computation.
journalACM Trans. Comput. Log.
volume3, number3 (year2002),

authorpersonRobert Atkey.
Syntax and Semantics of Quantitative Type Theory.
In booktitleProceedings of the 33rd Annual ACM/IEEE
Symposium on Logic in Computer Science, LICS 2018, Oxford, UK, July 09-12,
2018, editorpersonAnuj Dawar and
personErich Grädel (Eds.). publisherACM,

[Baillot et al(2010)]
authorpersonPatrick Baillot, personMarco
Gaboardi, and personVirgile Mogbil.
A PolyTime Functional Language from Light Linear
Logic. In booktitleProgramming Languages and Systems, 19th
European Symposium on Programming, ESOP 2010, Held as Part of the Joint
European Conferences on Theory and Practice of Software, ETAPS 2010,
Paphos, Cyprus, March 20-28, 2010. Proceedings
(seriesLecture Notes in Computer Science,
Vol. volume6012), editorpersonAndrew D.
Gordon (Ed.). publisherSpringer, pages104–124.

[Baillot and Mogbil(2004)]
authorpersonPatrick Baillot and
personVirgile Mogbil. year2004.
Soft lambda-Calculus: A Language for Polynomial
Time Computation. In booktitleFoundations of Software
Science and Computation Structures, 7th International Conference, FOSSACS
2004, Held as Part of the Joint European Conferences on Theory and Practice
of Software, ETAPS 2004, Barcelona, Spain, March 29 - April 2, 2004,
Proceedings (seriesLecture Notes in Computer Science,
Vol. volume2987), editorpersonIgor
Walukiewicz (Ed.). publisherSpringer, pages27–41.

authorpersonAndrej Bauer.
First Steps in Synthetic Computability Theory. In
booktitleProceedings of the 21st Annual Conference on
Mathematical Foundations of Programming Semantics, MFPS 2005, Birmingham,
UK, May 18-21, 2005 (seriesElectronic Notes in Theoretical
Computer Science, Vol. volume155),
editorpersonMartín Hötzel Escardó,
personAchim Jung, and personMichael W. Mislove
(Eds.). publisherElsevier, pages5–31.

[Bellantoni and Cook(1992)]
authorpersonStephen J. Bellantoni and
personStephen A. Cook. year1992.
A New Recursion-Theoretic Characterization of the
Polytime Functions.
journalComput. Complex.  volume2
(year1992), pages97–110.

authorpersonP. N. Benton.
A Mixed Linear and Non-Linear Logic: Proofs, Terms
and Models (Extended Abstract). In booktitleComputer
Science Logic, 8th International Workshop, CSL '94, Kazimierz, Poland,
September 25-30, 1994, Selected Papers (seriesLecture
Notes in Computer Science, Vol. volume933),
editorpersonLeszek Pacholski and
personJerzy Tiuryn (Eds.). publisherSpringer,

authorpersonEdwin C. Brady.
Idris 2: Quantitative Type Theory in Practice. In
booktitle35th European Conference on Object-Oriented
Programming, ECOOP 2021, July 11-17, 2021, Aarhus, Denmark (Virtual
Conference) (seriesLIPIcs, Vol. volume194),
editorpersonAnders Møller and
personManu Sridharan (Eds.). publisherSchloss
Dagstuhl - Leibniz-Zentrum für Informatik, pages9:1–9:26.

[Brunel et al(2014)]
authorpersonAloïs Brunel, personMarco
Gaboardi, personDamiano Mazza, and personSteve
Zdancewic. year2014.
A Core Quantitative Coeffect Calculus. In
booktitleProgramming Languages and Systems - 23rd European
Symposium on Programming, ESOP 2014. pages351–370.

[Cervesato and Pfenning(2002)]
authorpersonIliano Cervesato and
personFrank Pfenning. year2002.
A Linear Logical Framework.
journalInf. Comput. volume179,
number1 (year2002), pages19–75.

[Choudhury et al(2021)]
authorpersonPritam Choudhury,
personHarley Eades III, personRichard A. Eisenberg,
and personStephanie Weirich. year2021.
A graded dependent type system with a usage-aware
journalProc. ACM Program. Lang.
volume5, numberPOPL (year2021),

[Coppola and Martini(2001)]
authorpersonPaolo Coppola and personSimone
Martini. year2001.
Typing Lambda Terms in Elementary Logic with Linear
Constraints. In booktitleTyped Lambda Calculi and
Applications, 5th International Conference, TLCA 2001, Krakow, Poland, May
2-5, 2001, Proceedings (seriesLecture Notes in Computer
Science, Vol. volume2044),
editorpersonSamson Abramsky (Ed.).
publisherSpringer, pages76–90.

[Dal Lago(2011)]
authorpersonUgo Dal Lago.
A Short Introduction to Implicit Computational
Complexity. In booktitleLectures on Logic and Computation -
ESSLLI 2010 Copenhagen, Denmark, August 2010, ESSLLI 2011, Ljubljana,
Slovenia, August 2011, Selected Lecture Notes
(seriesLecture Notes in Computer Science,
Vol. volume7388), editorpersonNick
Bezhanishvili and personValentin Goranko (Eds.).
publisherSpringer, pages89–109.

[Dal Lago and Hofmann(2011)]
authorpersonUgo Dal Lago and
personMartin Hofmann. year2011.
Realizability models and implicit complexity.
journalTheor. Comput. Sci. volume412,
number20 (year2011), pages2029–2047.

[Dal Lago and Schöpp(2016)]
authorpersonUgo Dal Lago and
personUlrich Schöpp. year2016.
Computation by interaction for space-bounded
functional programming.
journalInf. Comput.  volume248
(year2016), pages150–194.

authorpersonNils Anders Danielsson.
Lightweight semiformal time complexity analysis for
purely functional data structures. In booktitleProceedings
of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming
Languages, POPL 2008, San Francisco, California, USA, January 7-12, 2008,
editorpersonGeorge C. Necula and
personPhilip Wadler (Eds.). publisherACM,

[Fu et al(2022)]
authorpersonPeng Fu, personKohei Kishida,
and personPeter Selinger. year2022.
Linear Dependent Type Theory for Quantum
Programming Languages.
journalLog. Methods Comput. Sci.
volume18, number3 (year2022).

[Ghica and Smith(2014)]
authorpersonDan R. Ghica and personAlex I.
Smith. year2014.
Bounded Linear Types in a Resource Semiring. In
booktitleProgramming Languages and Systems - 23rd European
Symposium on Programming, ESOP 2014. pages331–350.

authorpersonJean-Yves Girard.
Linear Logic.
journalTheor. Comput. Sci.  volume50
(year1987), pages1–102.

authorpersonJean-Yves Girard.
Light Linear Logic.
journalInf. Comput. volume143,
number2 (year1998), pages175–204.

[Girard et al(1992)]
authorpersonJean-Yves Girard, personAndre
Scedrov, and personPhilip J. Scott.
Bounded Linear Logic: A Modular Approach to
Polynomial-Time Computability.
journalTheor. Comput. Sci. volume97,
number1 (year1992), pages1–66.

[Guéneau et al(2018)]
authorpersonArmaël Guéneau,
personArthur Charguéraud, and
personFrançois Pottier. year2018.
A Fistful of Dollars: Formalizing Asymptotic
Complexity Claims via Deductive Program Verification. In
booktitleProgramming Languages and Systems - 27th European
Symposium on Programming, ESOP 2018, Held as Part of the European Joint
Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki,
Greece, April 14-20, 2018, Proceedings (seriesLecture
Notes in Computer Science, Vol. volume10801),
editorpersonAmal Ahmed (Ed.).
publisherSpringer, pages533–560.

[Hainry and Péchoux(2023)]
authorpersonEmmanuel Hainry and
personRomain Péchoux. year2023.
A General Noninterference Policy for Polynomial
journalProc. ACM Program. Lang.
volume7, numberPOPL (year2023),

[Hoffmann et al(2017)]
authorpersonJan Hoffmann, personAnkush Das,
and personShu-Chun Weng. year2017.
Towards automatic resource bound analysis for
OCaml. In booktitleProceedings of the 44th ACM SIGPLAN
Symposium on Principles of Programming Languages, POPL 2017, Paris, France,
January 18-20, 2017, editorpersonGiuseppe Castagna
and personAndrew D. Gordon (Eds.). publisherACM,

[Hoffmann and Jost(2022)]
authorpersonJan Hoffmann and personSteffen
Jost. year2022.
Two decades of automatic amortized resource
journalMath. Struct. Comput. Sci.
volume32, number6 (year2022),

authorpersonMartin Hofmann.
Syntax and Semantics of Dependent Types. In
booktitleSemantics and Logics of Computation.
publisherCambridge University Press, pages79–130.

authorpersonMartin Hofmann.
Linear Types and Non-Size-Increasing Polynomial
Time Computation. In booktitle14th Annual IEEE Symposium
on Logic in Computer Science, Trento, Italy, July 2-5, 1999.
publisherIEEE Computer Society, pages464–473.

authorpersonMartin Hofmann.
Linear types and non-size-increasing polynomial
time computation.
journalInf. Comput. volume183,
number1 (year2003), pages57–85.

[Hofmann and Jost(2003)]
authorpersonMartin Hofmann and
personSteffen Jost. year2003.
Static prediction of heap space usage for
first-order functional programs. In booktitleConference
Record of POPL 2003: The 30th SIGPLAN-SIGACT Symposium on Principles of
Programming Languages, New Orleans, Louisisana, USA, January 15-17, 2003,
editorpersonAlex Aiken and personGreg
Morrisett (Eds.). publisherACM, pages185–197.

[Hofmann and Scott(2004)]
authorpersonMartin Hofmann and
personPhilip J. Scott. year2004.
Realizability models for BLL-like languages.
journalTheor. Comput. Sci. volume318,
number1-2 (year2004), pages121–137.

authorpersonGérard P. Huet.
The Zipper.
journalJ. Funct. Program. volume7,
number5 (year1997), pages549–554.

authorpersonNeil D. Jones.
The expressive power of higher-order types or, life
without CONS.
journalJ. Funct. Program. volume11,
number1 (year2001), pages5–94.

[Krishnaswami et al(2015)]
authorpersonNeelakantan R. Krishnaswami,
personPierre Pradic, and personNick Benton.
Integrating Linear and Dependent Types. In
booktitleProceedings of the 42nd Annual ACM
SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL
2015, Mumbai, India, January 15-17, 2015,
editorpersonSriram K. Rajamani and
personDavid Walker (Eds.). publisherACM,

authorpersonYves Lafont.
Soft linear logic and polynomial time.
journalTheor. Comput. Sci. volume318,
number1-2 (year2004), pages163–180.

[Lago and Hofmann(2010a)]
authorpersonUgo Dal Lago and personMartin
Hofmann. year2010a.
Bounded Linear Logic, Revisited.
journalLog. Methods Comput. Sci.
volume6, number4 (year2010).

[Lago and Hofmann(2010b)]
authorpersonUgo Dal Lago and personMartin
Hofmann. year2010b.
A Semantic Proof of Polytime Soundness of Light
Affine Logic.
journalTheory Comput. Syst. volume46,
number4 (year2010), pages673–689.

authorpersonConor McBride.
I Got Plenty o' Nuttin'. In
booktitleA List of Successes That Can Change the World -
Essays Dedicated to Philip Wadler on the Occasion of His 60th Birthday
(seriesLecture Notes in Computer Science,
Vol. volume9600), editorpersonSam
Lindley, personConor McBride, personPhilip W.
Trinder, and personDonald Sannella (Eds.).
publisherSpringer, pages207–233.

[McCarthy et al(2016)]
authorpersonJay A. McCarthy, personBurke
Fetscher, personMax S. New, personDaniel Feltey,
and personRobert Bruce Findler.
A Coq Library for Internal Verification of
Running-Times. In booktitleFunctional and Logic Programming
- 13th International Symposium, FLOPS 2016, Kochi, Japan, March 4-6, 2016,
Proceedings (seriesLecture Notes in Computer Science,
Vol. volume9613), editorpersonOleg
Kiselyov and personAndy King (Eds.).
publisherSpringer, pages144–162.

[Moon et al(2021)]
authorpersonBenjamin Moon,
personHarley Eades III, and personDominic Orchard.
Graded Modal Dependent Type Theory. In
booktitleProgramming Languages and Systems - 30th European
Symposium on Programming, ESOP 2021, Held as Part of the European Joint
Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg
City, Luxembourg, March 27 - April 1, 2021, Proceedings
(seriesLecture Notes in Computer Science,
Vol. volume12648), editorpersonNobuko
Yoshida (Ed.). publisherSpringer, pages462–490.

[Niu et al(2022)]
authorpersonYue Niu, personJonathan
Sterling, personHarrison Grodin, and personRobert
Harper. year2022.
A cost-aware logical framework.
journalProc. ACM Program. Lang.
volume6, numberPOPL (year2022),

authorpersonUlf Norell.
Dependently typed programming in Agda. In
booktitleInternational school on advanced functional
programming. Springer, pages230–266.

[Orchard et al(2019)]
authorpersonDominic Orchard,
personVilem-Benjamin Liepelt, and
personHarley Eades III. year2019.
Quantitative program reasoning with graded modal
journalProc. ACM Program. Lang.
volume3, numberICFP (year2019),

[Rajani et al(2021)]
authorpersonVineet Rajani, personMarco
Gaboardi, personDeepak Garg, and personJan
Hoffmann. year2021.
A unifying type-theory for higher-order (amortized)
cost analysis.
journalProc. ACM Program. Lang.
volume5, numberPOPL (year2021),

authorpersonMatthijs Vákár.
Syntax and Semantics of Linear Dependent Types.
journalCoRR  volumeabs/1405.0033