Department of Computer Science
LMU Munich, Germany Institut für Logic and Computation 192/4
Technische Universität
Wienlorenz@leutgeb.xyzhttps://orcid.org/0000-0003-0391-3430 Department of
Computer Science
University of Innsbruck,
Austriageorg.moser@uibk.ac.athttps://orcid.org/0000-0001-9240-6128 Department
of Computer Science
University of Innsbruck,
Austriadavid.obwaller@uibk.ac.athttps://orcid.org/0000-0002-4925-4744 Institut
für Logic and Computation 192/4
Technische Universität
Wienzuleger@forsyte.athttps://orcid.org/0000-0003-1468-8398 Lorenz Leutgeb,
David Obwaller, Georg Moser, Florian Zuleger [100]F.3.2. Program Analysis John
Q. Open and Joan R. Access 2 42nd Conference on Very Important Topics (CVIT
2016) CVIT 2016 CVIT 2016 December 24–27, 2016 Little Whinging, United Kingdom
42 23

# Type-Based Analysis of Logarithmic Amortised Complexity

Martin Hofmann ${\dagger}$ Lorenz Leutgeb  Georg Moser  David Obwaller
Florian Zuleger

###### Abstract

We introduce a novel amortised resource analysis couched in a type-and-effect
system. Our analysis is formulated in terms of the physicist’s method of
amortised analysis, and is potential-based. The type system makes use of
logarithmic potential functions and is the first such system to exhibit
_logarithmic amortised complexity_. With our approach we target the automated
analysis of self-adjusting data structures, like splay trees, which so far
have only manually been analysed in the literature. In particular, we have
implemented a semi-automated prototype, which successfully analyses the zig-
zig case of _splaying_ , once the type annotations are fixed.

###### keywords:

analysis of algorithms; amortised resource analysis; functional programming;
self-adjusting data structures; automation

In Memoriam: Martin Hofmann

##  1 Introduction

Amortised analysis as pioneered by Sleator and Tarjan [52, 53] is a method for
the worst-case cost analysis of data structures. The innovation of amortised
analysis lies in considering the cost of a single data structure operation as
part of a sequence of data structures operations. The methodology of amortised
analysis allows one to assign a low (e.g., constant or logarithmic) amortised
cost to a data structure operation even though the worst-case cost of a single
operation might be high (e.g., polynomial or worse). The setup of amortised
analysis guarantees that for a sequence of data structure operations the
worst-case cost is indeed the number of data structure operations times the
amortised cost. In this way amortised analysis provides a methodology for
worst-case cost analysis.

Starting with the initial proposal, one of the objectives of amortised
analysis has been to conduct a worst-case cost analysis for self-adjusting
binary search trees, such as _splay trees_ [52, 53]. These data structures
have the behaviour that a single data structure operation might be expensive
(ie. linear in the size of the tree) but the cost is guaranteed to ‘average
out’ in a sequence of data structure operations (ie. logarithmic in the size
of the tree). Amortised analysis has been designed to provide a framework for
this kind of reasoning on the cost of data structure operations.

The automated cost analysis of imperative, functional, logic and object-
oriented programs as well as of more abstract programming paradigms such a
term rewriting systems is an active research topic [1, 3, 11, 20, 5, 2, 4, 21,
33, 6, 34, 8, 17, 19, 42]. Most research has focused on the inference of
polynomial bounds on the worst-case cost of the program under analysis. A few
papers also target the inference of exponential and logarithmic bounds [1, 5,
13, 54, 40, 55]. Some of the cited approaches are able to conduct an automated
amortised analysis in the sense of Sleator and Tarjan: The work on type-based
cost analysis by Martin Hofmann and his collaborators [32, 38, 37, 22, 24, 33,
34, 30, 31, 39, 26], which we discuss in more detail below, directly employs
potential functions as proposed by Sleator and Tarjan [52, 53]. For imperative
programs, a line of work infers cost bounds from lexicographic ranking
functions using arguments that implicitly achieve an amortised analysis [49,
50, 51, 16] (for details we refer the reader to [51]). The connection between
ranking functions and amortised analysis has also been discussed in the
context of term rewrite systems [33]. Proposals that incorporate amortised
analysis within the recurrence relations approach to cost analysis have been
discussed in [4, 17]. Still, to the best of our knowledge none of the cited
approaches is able to conduct a worst-case cost analysis for self-adjusting
binary search trees such as splay trees. One notable exception is [43] where
the correct amortised analysis of splay trees [52, 53] and other data
structures is certified in Isabelle/HOL with some tactic support. However, it
is not clear at all if the approach can be further automated.

In this article we take the first step towards the automated analysis of
logarithmic amortised cost. We extend the line of work by Martin Hofmann and
his collaborators on amortised analysis, where the search for suitable
potential functions is encoded as a type-and-effect systems. This line of work
has lead to several successful tools for deriving accurate bounds on the
resource usage of functional [24, 38, 6, 7], imperative programs [36, 29], as
well as term rewriting systems [8, 33, 34, 42]. The cited approaches employ a
variety of potential functions: While initially confined to inferring linear
cost [32], the methods were subsequently extended to cover polynomial [28],
multivariate polynomial [24], and also exponential cost [36]. We for the first
time propose a type system that supports logarithmic potential functions,
significantly extending and correcting an earlier note towards this goal [35].

Our analysis is couched in a simple core functional language just sufficiently
rich to provide a full definition of our motivating example: _splaying_. We
employ a big-step semantics, following similar approaches in the literature.
Further, our type system is geared towards runtime as computation cost (ie. we
assign a unit cost to each function call and zero cost to every other program
statement). It is straightforward to generalise this type system to other
monotone cost models. With respect to non-monotone costs, like eg. heap usage,
we expect the type system can also be readily be adapted, but this is outside
the scope of the paper.

The type system has been designed with the goal of automation. As in previous
work on type-based amortised analysis, the type system infers constraints on
unknown coefficients of template potential functions in a syntax directed way
from the program under analysis. Suitable coefficients can then be found
automatically by solving the collected constraints with a suitable constraint
solver (ie. an SMT solver that supports the theory of linear arithmetic). The
derivation of constraints is straightforward for all syntactic constructs of
our programming language. However, our automated analysis also requires
_sharing_ and _weakening_ rules. The latter supports the comparison of
different potential functions. As our potential functions are logarithmic, we
cannot directly encode the comparison between logarithmic expressions within
the theory of linear arithmetic. Here, we propose several ideas for
_linearising_ the required comparison of logarithmic expressions. The obtained
linear constraints can be then be added to the constraint system. Our proposed
linearisation makes use of  (i) mathematical facts about the logarithm,
referred to as _expert knowledge_ ,  (ii) Farkas’ lemma for turning the
universally-quantified premise of the weakening rule into an existentially-
quantified statement that can be added to the constraint system and  (iii)
finally a subtly modification of Schoenmakers potential.

We report on preliminary results for the automated amortised analysis of the
splay function. Our implementation semi-automatically verifies the correctness
of a type annotation with logarithmic amortised cost for the splay function
(more specifically for the zig-zig case of the splay function) using the
constraints generated by the type system. We believe that the ideas presented
in this article can be extended beyond the case of splay trees in order to
support the analysis of similar self-adjusting data structures such as the
ones used in the evaluation of [43]. Summarising, we make the following
contributions:

  * •

We propose a new class of template potential functions suitable for
logarithmic amortised analysis; these potential functions in particular
include a variant of Schoenmakers’ potential (a key building block for the
analysis of the splay function) and logarithmic expressions.

  * •

We present a type-and-effect system for potential-based resource analysis
capable of expressing logarithmic amortised costs, and prove its soundness.

  * •

We report on a preliminary implementation for the logarithmic amortised
analysis of the splay function. With respect to the zigzig-case of the splay
function, our prototype is able to automatically check that the amortised cost
is bounded by $3\log(t)+1$. All former results to this respect required a
manual analysis.

#### Outline

The rest of this paper is organised as follows. In Section 2, we review the
key concepts underlying type-based amortised analysis and present our ideas
for their extension. In Section 3, we introduce a simple core language
underlying our reasoning and provide a full definition of splaying, our
running example. The employed class of potential functions is provided in
Section 4, while the type-and-effect system is presented in Section 5. In
Section 7 we report on our ideas for implementing the _weakening_ rule.
Concretely, we see these ideas at work in Section 6, where we employ the
established type-and-effect system on the motivating example of _splaying_. In
Section 8, we present our implementation and design choices in automation. In
Section 9, we present related work and finally, we conclude in Section 10.

##  2 Setting the Stage

Our analysis is formulated in terms of the physicist’s method of amortised
analysis in the style of Sleator and Tarjan [52, 53]. This method assigns a
_potential_ to data structures of interest and defines the _amortised cost_ of
an operation as the sum of the actual cost plus the change of the potential
through execution of the operation, ie. the central idea of an amortised
analysis as formulated by Sleator and Tarjan is to choose a potential function
$\phi$ such that

$\phi(v)+a_{f}(v)=c_{f}(v)+\phi(f(v))\hbox to0.0pt{$\;$,\hss}$

holds for all inputs $v$ to a function $f$, where $a_{f}$, $c_{f}$ denote the
amortised and total cost, respectively, of executing $f$. Hofmann et al. [32,
23, 25, 24, 33, 34] provide a generalisation of this idea to a set of
potential functions $\phi,\psi$, such that

$\phi(v)\geqslant c_{f}(v)+\psi(f(v))\hbox to0.0pt{$\;$,\hss}$

holds for all inputs $v$. This allows to ready off an upper bound on the
amortised cost of $f$, ie. we have $a_{f}(v)\leqslant\phi(v)-\psi(v)$. We add
that the above inequality indeed generalises the original formulation, which
can be seen by setting $\phi(v)\mathrel{:=}a_{f}(v)+\psi(v)$.

In this paper, we present a type-based resource analysis based on the idea of
potential functions that can infer logarithmic amortised cost. Following
previous work by Hofmann et al., we tackle two key problems in order to
achieve a semi-automated logarithmic amortised analysis:  1) Automation is
achieved by a _type-and-effect system_ that uses _template potential
functions_ , ie. functions of a fixed shape with indeterminate coefficients.
Here, the key challenge is to identify templates that are suitable for
logarithmic analysis and that are closed under the basic operations of the
considered programming language.  2) In addition to the actual amortised
analysis with costs, we employ _cost-free_ analysis as a subroutine, setting
the amortised $a_{f}$ and actual costs $c_{f}$ of all functions $f$ to zero.
This enables a _size analysis_ of sorts, because the inequality
$\phi(v)\geqslant\psi(f(v))$ bounds the size of the potential $\psi(f(v))$ in
terms of the potential $\phi(v)$. The size analysis we conduct allows lifting
the analysis of a subprogram to a larger context, which is crucial for
achieving a _compositional analysis_.  We overview these two aspects in the
sequel of the section.

###  2.1 Type-and-effect System

To set the scene, we briefly review amortised analysis formulated as a type-
and effect system up to and including the multivariate polynomial analysis,
cf. [37, 28, 27, 23, 24, 33, 34, 26, 39].

_Polynomial Amortised Analysis._ Suppose that we have types
$\alpha,\beta,\gamma,\dots$ representing sets of values. We write
$\llbracket{\alpha}\rrbracket$ for the set of values represented by type
$\alpha$. Types may be constructed from base types such as Booleans and
integers, denoted by $\mathsf{Base}$, and by type formers such as list, tree,
product, sum, etc. For each type $\alpha$, we define a (possibly infinite) set
of _basic potential functions_
$\mathcal{BF}(\alpha)\colon\llbracket{\alpha}\rrbracket\to{\mathbb{R}^{+}_{0}}$.
Thus, if $p\in\mathcal{BF}(\alpha)$ and $v\in\llbracket{\alpha}\rrbracket$
then $p(v)\in{\mathbb{R}^{+}_{0}}$. An _annotated type_ is a pair of a type
$\alpha$ and a function
$Q:\mathcal{BF}(\alpha)\rightarrow{\mathbb{R}^{+}_{0}}$ providing a
coefficient for each _basic potential function_. The function $Q$ must be zero
on all but finitely many basic potential functions. For each annotated type
${\alpha}{\mid}{Q}$, the _potential function_
$\phi_{Q}:\llbracket{\alpha}\rrbracket\rightarrow{\mathbb{R}^{+}_{0}}$ is then
given by

$\phi_{Q}(v)\mathrel{:=}\sum_{p\in\mathcal{BF}(\alpha)}Q(p)\cdot p(v)\hbox
to0.0pt{$\;$.\hss}$

By introducing product types, one can regard functions with several arguments
as unary functions, which allows for technically smooth formalisations, cf.
[28, 27, 22]; the analyses in the cited papers are called _univariate_ as the
set of basic potential functions $\mathcal{BF}(\alpha)$ of a product type
$\alpha$ is given directly. In the later _multivariate_ versions of automated
amortised analysis [23, 24, 34] one takes a more fine-grained approach to
products. Namely, one then sets (for arbitrary $n$)

$\displaystyle\mathcal{BF}(\alpha_{1}\times\dots\times\alpha_{n})$
$\displaystyle\mathrel{:=}{\mathcal{BF}(\alpha_{1})}\times\dots\times{\mathcal{BF}(\alpha_{n})}\hbox
to0.0pt{$\;$,\hss}$ $\displaystyle(p_{1},\dots,p_{n})(v_{1},\dots,v_{n})$
$\displaystyle\mathrel{:=}\prod_{i=1}^{n}p_{i}(v_{i})\hbox to0.0pt{$\;$.\hss}$

Thus, the basic potential function for a product type is obtained as the
multiplication of the basic potential functions of its constituents.111Suppose
that for each type $\alpha$ there exists a distinguished element
$u\in\mathcal{BF}(\alpha)$ with $u(a)=1$ for all
$a\in\llbracket{\alpha}\rrbracket$. Then, the multivariate product types
contain all (linear combinations) of the basic potential functions, extending
earlier univariate definitions of product types.

_Automation._ The idea behind this setup is that the basic potential functions
$\mathcal{BF}(\alpha)$ are suitably chosen and fixed by the analysis designer,
the coefficients $Q(p)$ for $p\in\mathcal{BF}(\alpha)$, however, are left
indeterminate and will (automatically) be fixed during the analysis. For this,
constraints over the unknown coefficients are collected in a syntax-directed
way from the function under analysis and then solved by a suitable constraint
solver. The type-and-effect system formalises this collection of constraints
as typing rules, where for each construct of the considered programming
language a typing rule is given that corresponds to constraints over the
coefficients of the annotated types. Expressing the quest for suitable type
annotations as a type-and-effect system allows one to compose typing
judgements in a syntax-oriented way without the need for fixing additional
intermediate results, which is often required by competing approaches. This
syntax-directed approach to amortised analysis has been demonstrated to work
well for datatypes like lists or trees whose basic potential functions are
polynomials over the length of a list resp. the number of nodes of a tree. One
of the reasons why this works well is, e.g., that functional programming
languages typically include dedicated syntax for list construction and that
polynomials are closed under addition by one (ie. if $p(n)$ is a polynomial,
so is $p(n+1)$), supporting the formulation of a suitable typing rule for list
construction, cf. [28, 27, 22, 23, 24]. The syntax-directed approach has been
shown to generalise from lists and trees to general inductive data types, cf.
[33, 34, 41].

_Logarithmic Amortised Analysis._ We now motivate the design choices of our
type-and-effect system. The main objective of our approach is the automated
analysis of data-structures such as splay trees, which have _logarithmic_
amortised cost. The amortised analysis of splay trees is tricky and requires
choosing an adequate potential function: our work makes use of a variant of
Schoenmakers’ potential, $\operatorname{\mathsf{rk}}(t)$ for a tree $t$, cf.
[47, 43], defined inductively by

${\displaystyle\operatorname{\mathsf{rk}}(\textup{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\color[rgb]{0.10546875,0.00390625,0.375}\small{\@listingGroup{ltx_lst_keywords2}{\color[rgb]{0,0.578125,0.015625}\small
leaf}}}}}})$ $\displaystyle\mathrel{:=}1,$
${{{{\displaystyle\operatorname{\mathsf{rk}}(\textup{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\color[rgb]{0.10546875,0.00390625,0.375}\small(}}}{$l$}\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\color[rgb]{0.10546875,0.00390625,0.375}\small{\@listingGroup{ltx_lst_identifier}{,}}}}}
{$d$}\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\color[rgb]{0.10546875,0.00390625,0.375}\small{\@listingGroup{ltx_lst_identifier}{,}}}}}
{$r$}\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\color[rgb]{0.10546875,0.00390625,0.375}\small)}}}})$
$\displaystyle\mathrel{:=}\operatorname{\mathsf{rk}}(l)+\log(\lvert{l}\rvert)+\log(\lvert{r}\rvert)+\operatorname{\mathsf{rk}}(r)\hbox
to0.0pt{$\;$,\hss}$

where $l$, $r$ are the left resp. right child of the tree ($l$, $d$, $r$),
$\lvert{t}\rvert$ denotes the number of leaves of a tree $t$, and $d$ is some
data element that is ignored by the potential function. Besides Schoenmakers’
potential we need to add further basic potential functions to our analysis.
This is motivated as follows: Similar to the polynomial amortised analysis
discussed above we want that the basic potential functions can express the
construction of a tree, e.g., let us consider the function

${{{{f(x,d,y)\mathrel{:=}\textup{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\color[rgb]{0.10546875,0.00390625,0.375}\small(}}}{$x$}\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\color[rgb]{0.10546875,0.00390625,0.375}\small{\@listingGroup{ltx_lst_identifier}{,}}}}}
{$d$}\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\color[rgb]{0.10546875,0.00390625,0.375}\small{\@listingGroup{ltx_lst_identifier}{,}}}}}
{$y$}\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\color[rgb]{0.10546875,0.00390625,0.375}\small)}}}},$

which constructs the tree ($x$, $d$, $y$) from some trees $x,y$ and some data
element $d$, and let us assume a constant cost $c_{f}(x,y)=1$ for the function
$f$. A type annotation for $f$ is given by

$\displaystyle\underbrace{\operatorname{\mathsf{rk}}(x)+\log(\lvert{x}\rvert)+\operatorname{\mathsf{rk}}(y)+\log(\lvert{y}\rvert)+1}_{\phi(x,y)}\geqslant
c_{f}(x,y)+\underbrace{\operatorname{\mathsf{rk}}(f(x,d,y))}_{\psi(f(x,y))}\hbox
to0.0pt{$\;$,\hss}$

ie. the potential $\phi(x,y)$ suffices to pay for the cost $c_{f}$ of
executing $f$ and the potential of the result $\psi(f(x,y))$ (the correctness
of this type can be established directly from the definition of Schoenmakers’
potential). As mentioned above, the logarithmic expressions in $\phi(x,y)$,
ie. $\log(\lvert{x}\rvert)+\log(\lvert{y}\rvert)+1$, specify the _amortised
costs_ of the operation.

We see that in order to express the potential $\phi(x,y)$ we also need the
basic potential functions $\log(\lvert{t}\rvert)$ for a tree $t$. In fact, we
will choose the slightly richer set of basic potential functions

$p_{(a,b)}(t)=\log(a\lvert{t}\rvert+b)\hbox to0.0pt{$\;$,\hss}$

where $a,b\in{\mathbb{N}}$ and $t$ is a tree. We note that by setting $a=0$
and $b=2$ this choice allows us to represent the constant function $u$ with
$u(t)=1$ for all trees $t$. We further note that this choice of potential
functions is sufficiently rich to express that $p_{(a,b)}(t)=p_{(a,b+a)}(s)$
for trees $s,t$ with $\lvert{t}\rvert=\lvert{s}\rvert+1$, which is needed for
precisely expressing the change of potential when a tree is extended by one
node. Further, we define basic potential functions for products of trees by
setting

$p_{(a_{1},\dots,a_{n},b)}(t_{1},\dots,t_{n})=\log({a_{1}\cdot\lvert{t_{1}}\rvert}+\dots+{a_{n}\cdot\lvert{t_{n}}\rvert}+b)\hbox
to0.0pt{$\;$,\hss}$

where $a_{1},\dots,a_{n},b\in{\mathbb{N}}$ and $t_{1},\dots,t_{n}$ is a tuple
of trees. This is sufficiently rich to state the equality
$p_{(a_{0},a_{1},\dots,a_{n},b)}(x_{1},x_{1},\dots,x_{n})=p_{(a_{0}+a_{1},\dots,a_{n},b)}(x_{1},\dots,x_{n})$,
which supports the formulation of a _sharing_ rule, which in turn is needed
for supporting the let-construct in functional programming; cf. [23, 24, 34]
for a more detailed exposition on the sharing rule and the let-construct.

###  2.2 Cost-free Semantics

_Polynomial Amortised Analysis._ We begin by reviewing the cost-free semantics
underlying previous work [27, 22, 23, 24] on polynomial amortised analysis.
Assume that we want to analyse the composed function call
$g(f(\vec{x}),\vec{z})$ using already established analysis results for
$f(\vec{x})$ and $g(y,\vec{z})$. Suppose we have already established that for
all $\vec{x}$, $y$, $\vec{z}$ we have:

$\displaystyle\phi_{0}(\vec{x})\geqslant c_{f}(\vec{x})+\beta(f(\vec{x}))$ (1)
$\displaystyle\phi_{i}(\vec{x})\geqslant\phi^{\prime}_{i}(f(\vec{x}))\quad\text{for
all $i$ ($0<i\leqslant n$)}$ (2)
$\displaystyle\beta(y)+\gamma(\vec{z})+\sum_{i=1}^{n}\phi^{\prime}_{i}(y)\phi_{i}^{\prime\prime}(\vec{z})\geqslant
c_{g}(y,\vec{z})+\psi(g(y,\vec{z}))\hbox to0.0pt{$\;$,\hss}$ (3)

where as in the multivariate case above, $n$ is arbitrary and equations (1)
and (3) assume cost, while equation (2) is _cost-free_. Then, we can conclude
for all $\vec{x},\vec{z}$ that

$\underbrace{\phi_{0}(\vec{x})+\gamma(\vec{z})+\sum_{i=1}^{n}\phi_{i}(\vec{x})\phi_{i}^{\prime\prime}(\vec{z})}_{\phi(\vec{x},\vec{z})}\geqslant
c_{f}(\vec{x})+c_{g}(f(\vec{x}),\vec{z})+\psi(g(f(\vec{x}),\vec{z}))\hbox
to0.0pt{$\;$,\hss}$

guaranteeing that the potential $\phi(\vec{x},\vec{z})$ suffices to pay for
the cost $c_{f}(\vec{x})$ of computing $f(\vec{x})$, the cost
$c_{g}(f(\vec{x}),\vec{z})$ of computing $g(f(\vec{x}),\vec{z})$ and the
potential $\psi(g(f(\vec{x}),\vec{z}))$ of the result $g(f(\vec{x}),\vec{z})$.
We note that the correctness of this inference hinges on the fact that we can
multiply equation (2) with $\phi^{\prime\prime}_{i}(\vec{z})$ for $i=1\dots
n$, using the monotonicity of the multiplication operation (note that
potential functions are non-negative). We highlight that the multiplication
argument works well with cost-free semantics, and enables lifting the resource
analysis of $f(\vec{x})$ and $g(y,\vec{z})$ to the composed function call
$g(f(\vec{x}),\vec{z})$.

_Remark._ We point out that the above exposition of cost-free semantics in the
context of polynomial amortised analysis differs from the motivation given in
the literature [27, 22, 23, 24], where cost-free semantics are motivated by
the quest for _resource polymorphism_ , which is the problem of computing (a
representation of) all polynomial potential functions (up to a fixed maximal
degree) for the program under analysis; this problem has been deemed of
importance for the handling of non tail-recursive programs. We add that for
the amortised cost analysis of inductively generated data-types, the cost-free
semantics proved necessary even for handling basic data-structure
manipulations [33, 34, 42]. In our view, cost-free semantics incorporate a
_size analysis_ of sorts. We observe that equation (2) states that the
potential of the result of the evaluation of $f(\vec{x})$ is bounded by the
potential of the function arguments $\vec{x}$, without accounting for the
costs of this evaluation. Thus, for suitably chosen potential functions
$\phi_{i},\phi^{\prime}_{i}$ can act as _norms_ and capture the size of the
result of the evaluation $f(\vec{x})$ in relation to the size of the argument.
As stated above, a separated cost and size analysis enables a compositional
analysis, an insight that we also exploit for logarithmic amortised analysis.

_Logarithmic Amortised Analysis._ Similar to the polynomial case, we want to
analyse the composed function call $g(f(\vec{x}),\vec{z})$ using already
established analysis results for $f(\vec{x})$ and $g(y,\vec{z})$. However, now
we extend the class of potential functions to sublinear functions. Assume that
we have already established that

$\displaystyle\phi_{0}(\vec{x})\geqslant c_{f}(\vec{x})+\beta(f(\vec{x}))$ (4)
$\displaystyle\log(\phi_{i}(\vec{x}))\geqslant\log(\phi_{i}^{\prime}(\vec{x}))\qquad\text{for
all $i$ ($0<i\leqslant n$)}$ (5)
$\displaystyle\beta(y)+\gamma(\vec{z})+\sum_{i=1}^{n}\log(\phi^{\prime}_{i}(y)+\phi_{i}^{\prime\prime}(\vec{z}))\geqslant
c_{g}(y,\vec{z})+\psi(g(y,\vec{z}))\hbox to0.0pt{$\;$,\hss}$ (6)

where equations (4) and (6) assume cost, while equation (5) is _cost-free_.
Equations (4) and (5) represent the result of an analysis of $f(\vec{x})$
(note that these equations do not contain the parameters $\vec{z}$, which will
however be needed for the analysis of $g(f(\vec{x}),\vec{z})$), and equation
(6) the result of an analysis of $g(y,\vec{z})$. Then, we can conclude for all
$\vec{x},y,\vec{z}$ that

$\underbrace{\phi_{0}(\vec{x})+\gamma(\vec{z})+\sum_{i=1}^{n}\log(\phi_{i}(\vec{x})+\phi_{i}^{\prime\prime}(\vec{z}))}_{\phi(\vec{x},\vec{z})}\geqslant
c_{f}(\vec{x})+c_{g}(f(\vec{x}),\vec{z})+\psi(g(f(\vec{x}),\vec{z}))\hbox
to0.0pt{$\;$,\hss}$

guaranteeing that the potential $\phi(\vec{x},\vec{z})$ suffices to pay for
the cost $c_{f}(\vec{x})$ of computing $f(\vec{x})$, the cost
$c_{g}(f(\vec{x}),\vec{z})$ of computing $g(f(\vec{x}),\vec{z})$ and the
potential $\psi(g(f(\vec{x}),\vec{z}))$ of the result $g(f(\vec{x}),\vec{z})$.
Here, we crucially use monotonicity of the logarithm function, as formalised
in Lemma 5.4. This reasoning allows us to lift isolated analyses of the
functions $f(\vec{x})$ and $g(y,\vec{z})$ to the composed function call
$g(f(\vec{x}),\vec{z})$; this is what is required for a compositional
analysis!

_Example._ We now illustrate the compositional reasoning on an example. We
consider the function
${{{{f(x,d,y)\mathrel{:=}\textup{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\color[rgb]{0.10546875,0.00390625,0.375}\small(}}}{$x$}\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\color[rgb]{0.10546875,0.00390625,0.375}\small{\@listingGroup{ltx_lst_identifier}{,}}}}}
{$d$}\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\color[rgb]{0.10546875,0.00390625,0.375}\small{\@listingGroup{ltx_lst_identifier}{,}}}}}
{$y$}\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\color[rgb]{0.10546875,0.00390625,0.375}\small)}}}}$,
which takes two trees $x,y$ and some data element $d$ and returns the tree
($x$, $d$, $y$). Assume that we already have established that

$\displaystyle\psi(x)+\psi(y)+1\geqslant
c_{f}(x,y)+\operatorname{\mathsf{rk}}(f(x,d,y))$ (7)
$\displaystyle\log(\lvert{x}\rvert+\lvert{y}\rvert)\geqslant\log(\lvert{f(x,d,y)}\rvert)\hbox
to0.0pt{$\;$,\hss}$ (8)

where $\psi(u)=\operatorname{\mathsf{rk}}(u)+\log(\lvert{u}\rvert)$,
$c_{f}(x,y)=1$, and $d$ is an arbitrary data element, which is not relevant
for the cost analysis of $f$. We now want to analyse the composed function
$h(x,a,y,b,z):=f(f(x,a,y),b,z)$. We will use the above reasoning,
instantiating equations (4) and (5) with equations (7) and (8) for the inner
function call $f(x,a,y)$, and equation (6) with the sum of equations (7) and
(8) for the outer function call $f(u,b,z)$. As argued above, we can then
conclude for all $x,y,z$ that

$\displaystyle\psi(x)+\psi(y)+\psi(z)+\log(\lvert{x}\rvert+\lvert{y}\rvert)+\log(\lvert{x}\rvert+\lvert{y}\rvert+\lvert{z}\rvert)+2\geqslant{}$
$\displaystyle{}\geqslant
c_{f}(x,a,y)+c_{f}(f(x,a,y),b,z)+\psi(f(f(x,y),z))\hbox to0.0pt{$\;$,\hss}$

is a valid resource annotation for $h(x,a,y,b,z):=f(f(x,a,y),b,z)$; we have
used equation (8) twice in this derivation, once as
$\log(\lvert{x}\rvert+\lvert{y}\rvert)\geqslant\log(\lvert{f(x,a,y)}\rvert)$
and once lifted as
$\log(\lvert{x}\rvert+\lvert{y}\rvert+\lvert{z}\rvert)\geqslant\log(\lvert{f(x,a,y)}\rvert+\lvert{z}\rvert)$.
Kindly note that the above example appears in similar form as part of the
analysis of the splay function described in Section 6.

##  3 Motivating Example

In this section, we introduce the syntax of a suitably defined core (first-
order) programming language to be used in the following. Furthermore, we
recall the definition of _splaying_ , following the presentation by Nipkow in
[43]. Splaying constitutes the motivating examples for the type-based
logarithmic amortised resource analysis presented in this paper.

To make the presentation more succinct, we assume only the following types:
Booleans
${{\mathsf{Bool}=\\{\textup{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\color[rgb]{0.10546875,0.00390625,0.375}\small{\@listingGroup{ltx_lst_keywords2}{\color[rgb]{0,0.578125,0.015625}\small
true}}}}}},\textup{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\color[rgb]{0.10546875,0.00390625,0.375}\small{\@listingGroup{ltx_lst_keywords2}{\color[rgb]{0,0.578125,0.015625}\small
false}}}}}}\\}$, an abstract base type $\mathsf{Base}$ (abbrev. $\mathsf{B}$),
product types, and binary trees $\mathsf{Tree}$ (abbrev. $\mathsf{T}$), whose
internal nodes are labelled with elements ${b}{\colon}\\!{\mathsf{Base}}$. We
use lower-case Greek letters for the denotation of types. Elements
${t}{\colon}\\!{\mathsf{Tree}}$ are defined by the following grammar which
fixes notation.

${{{{{t::=\textup{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\color[rgb]{0.10546875,0.00390625,0.375}\small{\@listingGroup{ltx_lst_keywords2}{\color[rgb]{0,0.578125,0.015625}\small
leaf}}}}}}\mid\textup{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\color[rgb]{0.10546875,0.00390625,0.375}\small(}}}{$t_{1}$}\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\color[rgb]{0.10546875,0.00390625,0.375}\small{\@listingGroup{ltx_lst_identifier}{,}}}}}
{$b$}\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\color[rgb]{0.10546875,0.00390625,0.375}\small{\@listingGroup{ltx_lst_identifier}{,}}}}}
{$t_{2}$}\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\color[rgb]{0.10546875,0.00390625,0.375}\small)}}}}\hbox
to0.0pt{$\;$.\hss}$

The size of a tree is the number of leaves:
${\lvert{\textup{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\color[rgb]{0.10546875,0.00390625,0.375}\small{\@listingGroup{ltx_lst_keywords2}{\color[rgb]{0,0.578125,0.015625}\small
leaf}}}}}}}\rvert\mathrel{:=}1$,
${{{{\lvert{\textup{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\color[rgb]{0.10546875,0.00390625,0.375}\small(}}}{$t$}\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\color[rgb]{0.10546875,0.00390625,0.375}\small{\@listingGroup{ltx_lst_identifier}{,}}}}}
{$a$}\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\color[rgb]{0.10546875,0.00390625,0.375}\small{\@listingGroup{ltx_lst_identifier}{,}}}}}
{$u$}\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\color[rgb]{0.10546875,0.00390625,0.375}\small)}}}}}\rvert\mathrel{:=}\lvert{t}\rvert+\lvert{u}\rvert$.

Expressions are defined as follows and given in _let normal form_ to simplify
the presentation of the semantics and typing rules. In order to ease the
readability, we make use of some mild syntactic sugaring in the presentation
of actual code.

######  Definition 3.1.

$\displaystyle\circ$
${{{\displaystyle::=\textup{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\color[rgb]{0.10546875,0.00390625,0.375}\small\textless}}}}\mid\textup{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\color[rgb]{0.10546875,0.00390625,0.375}\small\textgreater}}}}\mid\textup{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\color[rgb]{0.10546875,0.00390625,0.375}\small=}}}}$
$\displaystyle e$ $\displaystyle::=f\ x_{1}\leavevmode\nobreak\
\dots\leavevmode\nobreak\ x_{n}$
${{\displaystyle\mid\textup{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\color[rgb]{0.10546875,0.00390625,0.375}\small{\@listingGroup{ltx_lst_keywords2}{\color[rgb]{0,0.578125,0.015625}\small
true}}}}}}\mid\textup{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\color[rgb]{0.10546875,0.00390625,0.375}\small{\@listingGroup{ltx_lst_keywords2}{\color[rgb]{0,0.578125,0.015625}\small
false}}}}}}\mid e_{1}\circ e_{2}$
${{{\displaystyle\mid\textup{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\color[rgb]{0.10546875,0.00390625,0.375}\small{\@listingGroup{ltx_lst_keyword}{\color[rgb]{0.87890625,0,0.2890625}\small
if}}}}}}\ x\
\textup{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\color[rgb]{0.10546875,0.00390625,0.375}\small{\@listingGroup{ltx_lst_keyword}{\color[rgb]{0.87890625,0,0.2890625}\small
then}}}}}}\ e_{1}\
\textup{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\color[rgb]{0.10546875,0.00390625,0.375}\small{\@listingGroup{ltx_lst_keyword}{\color[rgb]{0.87890625,0,0.2890625}\small
else}}}}}}\ e_{2}$
${{{{{\displaystyle\mid\textup{{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\color[rgb]{0.10546875,0.00390625,0.375}\small(}}}{$x_{1}$}\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\color[rgb]{0.10546875,0.00390625,0.375}\small{\@listingGroup{ltx_lst_identifier}{,}}}}}
{$x_{2}$}\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\color[rgb]{0.10546875,0.00390625,0.375}\small{\@listingGroup{ltx_lst_identifier}{,}}}}}
{$x_{3}$}\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\color[rgb]{0.10546875,0.00390625,0.375}\small)}}}}}\mid\textup{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\color[rgb]{0.10546875,0.00390625,0.375}\small{\@listingGroup{ltx_lst_keywords2}{\color[rgb]{0,0.578125,0.015625}\small
leaf}}}}}}$
${{{{{{{{{{{\displaystyle\mid\textup{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\color[rgb]{0.10546875,0.00390625,0.375}\small{\@listingGroup{ltx_lst_keyword}{\color[rgb]{0.87890625,0,0.2890625}\small
match}}}}}}\ x\
\textup{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\color[rgb]{0.10546875,0.00390625,0.375}\small{\@listingGroup{ltx_lst_keyword}{\color[rgb]{0.87890625,0,0.2890625}\small
with}}}}}}\
\textup{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\color[rgb]{0.10546875,0.00390625,0.375}\small\textbar}}}}\
\textup{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\color[rgb]{0.10546875,0.00390625,0.375}\small{\@listingGroup{ltx_lst_keywords2}{\color[rgb]{0,0.578125,0.015625}\small
leaf}}}}}}\
\mathrel{\textup{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\color[rgb]{0.10546875,0.00390625,0.375}\small-\textgreater}}}}}e_{1}\
\textup{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\color[rgb]{0.10546875,0.00390625,0.375}\small\textbar}}}}\
\textup{{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\color[rgb]{0.10546875,0.00390625,0.375}\small(}}}{$x_{1}$}\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\color[rgb]{0.10546875,0.00390625,0.375}\small{\@listingGroup{ltx_lst_identifier}{,}}}}}
{$x_{2}$}\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\color[rgb]{0.10546875,0.00390625,0.375}\small{\@listingGroup{ltx_lst_identifier}{,}}}}}
{$x_{3}$}\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\color[rgb]{0.10546875,0.00390625,0.375}\small)}}}}}\
\mathrel{\textup{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\color[rgb]{0.10546875,0.00390625,0.375}\small-\textgreater}}}}}e_{2}$
${{{\displaystyle\mid\textup{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\color[rgb]{0.10546875,0.00390625,0.375}\small{\@listingGroup{ltx_lst_keyword}{\color[rgb]{0.87890625,0,0.2890625}\small
let}}}}}}\ x\leavevmode\nobreak\
\textup{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\color[rgb]{0.10546875,0.00390625,0.375}\small=}}}}\leavevmode\nobreak\
e_{1}\
\textup{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\color[rgb]{0.10546875,0.00390625,0.375}\small{\@listingGroup{ltx_lst_keyword}{\color[rgb]{0.87890625,0,0.2890625}\small
in}}}}}}\ e_{2}$ $\displaystyle\mid x$

We skip the standard definition of integer constants $n\in{\mathbb{Z}}$ as
well as variable declarations, cf. [45]. Furthermore, we omit binary
operations and focus on the bare essentials for the comparison operators. For
the resource analysis these are not of importance, as long as we assume that
no actual costs are emitted.

A _typing context_ is a mapping from variables $\mathcal{V}$ to types. Type
contexts are denoted by upper-case Greek letters. A program $\mathsf{P}$
consists of a signature $\mathcal{F}$ together with a set of function
definitions of the form $f(x_{1},\dots,x_{n})=e$, where the $x_{i}$ are
variables and $e$ an expression. A _substitution_ or (_environment_) $\sigma$
is a mapping from variables to values that respects types. Substitutions are
denoted as sets of assignments: $\sigma=\\{{x_{1}\mapsto
t_{1}},\dots,{x_{n}\mapsto t_{n}}\\}$. We write
$\operatorname{\mathsf{dom}}(\sigma)$ ($\operatorname{\mathsf{rg}}(\sigma)$)
to denote the domain (range) of $\sigma$. Let $\sigma$, $\tau$ be
substitutions such that
$\operatorname{\mathsf{dom}}(\sigma)\cap\operatorname{\mathsf{dom}}(\tau)=\varnothing$.
Then we denote the (disjoint) union of $\sigma$ and $\tau$ as
$\sigma\mathrel{\uplus}\tau$. We employ a simple cost-sensitive big-step
semantics based on eager evaluation, whose rules are given in Figure 1. The
judgement ${\sigma}\sststile{}{\ell}{{e}\Rightarrow{v}}$ means that under
environment $\sigma$, expression $e$ is evaluated to value $v$ in exactly
$\ell$ steps. Here only rule applications emit (unit) costs. If we do not take
costs into account, we simply write
${\sigma}\sststile{}{}{{e}\Rightarrow{v}}$.

${\sigma}\sststile{}{0}{{\text{\small\color[rgb]{0,0.578125,0.015625}{{false}}}}\Rightarrow{\text{\small\color[rgb]{0,0.578125,0.015625}{{false}}}}}$
${\sigma}\sststile{}{0}{{\text{\small\color[rgb]{0,0.578125,0.015625}{{true}}}}\Rightarrow{\text{\small\color[rgb]{0,0.578125,0.015625}{{true}}}}}$
${\sigma}\sststile{}{0}{{\text{\small\color[rgb]{0,0.578125,0.015625}{{leaf}}}}\Rightarrow{\text{\small\color[rgb]{0,0.578125,0.015625}{{leaf}}}}}$
${\sigma}\sststile{}{0}{{\text{\text{\small\color[rgb]{0,0.578125,0.015625}{(}}{$x_{1}$}\text{\small\color[rgb]{0.10546875,0.00390625,0.375}{,}}{$x_{2}$}\text{\small\color[rgb]{0.10546875,0.00390625,0.375}{,}}{$x_{3}$}\text{\small\color[rgb]{0,0.578125,0.015625}{)}}}}\Rightarrow{\text{\text{\small\color[rgb]{0,0.578125,0.015625}{(}}{$t$}\text{\small\color[rgb]{0.10546875,0.00390625,0.375}{,}}{$b$}\text{\small\color[rgb]{0.10546875,0.00390625,0.375}{,}}{$u$}\text{\small\color[rgb]{0,0.578125,0.015625}{)}}}}}\lx@proof@logical@and
x_{1}\sigma=tx_{2}\sigma=bx_{3}\sigma=u$
${\sigma}\sststile{}{0}{{x}\Rightarrow{v}}x\sigma=v$
${\sigma}\sststile{}{0}{{x_{1}\circ x_{2}}\Rightarrow{b}}\text{$b$ is value of
$x_{1}\sigma\circ x_{2}\sigma$}$
${\sigma}\sststile{}{\ell+1}{{\text{\small\color[rgb]{0.10546875,0.00390625,0.375}{{f
}}}x_{1}\leavevmode\nobreak\ \ldots\leavevmode\nobreak\
x_{k}}\Rightarrow{v}}\lx@proof@logical@and
f(x_{1},\ldots,x_{k})=e\in\mathsf{P}{\sigma}\sststile{}{\ell}{{e}\Rightarrow{v}}$
${\sigma}\sststile{}{\ell_{1}+\ell_{2}}{{\text{\small\color[rgb]{0.87890625,0,0.2890625}{{let
}}}x\text{\small\color[rgb]{0.10546875,0.00390625,0.375}{{ =
}}}e_{1}\text{\small\color[rgb]{0.87890625,0,0.2890625}{{ in
}}}e_{2}}\Rightarrow{v}}\lx@proof@logical@and{\sigma}\sststile{}{\ell_{1}}{{e_{1}}\Rightarrow{w}}{\sigma[x\mapsto
w]}\sststile{}{\ell_{2}}{{e_{2}}\Rightarrow{v}}$
${\sigma}\sststile{}{\ell}{{\text{\small\color[rgb]{0.87890625,0,0.2890625}{{match
}}}x\text{\small\color[rgb]{0.87890625,0,0.2890625}{{
with}}}\begin{array}[t]{l}\text{\small\color[rgb]{0.10546875,0.00390625,0.375}{{|
}}}\text{\small\color[rgb]{0,0.578125,0.015625}{{leaf}}}\text{\small\color[rgb]{0.10546875,0.00390625,0.375}{{
-> }}}e_{1}\\\ \text{\small\color[rgb]{0.10546875,0.00390625,0.375}{{|
}}}\text{\text{\small\color[rgb]{0,0.578125,0.015625}{(}}{$x_{0}$}\text{\small\color[rgb]{0.10546875,0.00390625,0.375}{,}}{$x_{1}$}\text{\small\color[rgb]{0.10546875,0.00390625,0.375}{,}}{$x_{2}$}\text{\small\color[rgb]{0,0.578125,0.015625}{)}}}\text{\small\color[rgb]{0.10546875,0.00390625,0.375}{{
-> }}}e_{2}\end{array}}\Rightarrow{v}}\lx@proof@logical@and
x\sigma=\text{\small\color[rgb]{0,0.578125,0.015625}{{leaf}}}{\sigma}\sststile{}{\ell}{{e_{1}}\Rightarrow{v}}$
${\sigma}\sststile{}{\ell}{{\text{\small\color[rgb]{0.87890625,0,0.2890625}{{if
}}}x\text{\small\color[rgb]{0.87890625,0,0.2890625}{{ then
}}}e_{1}\text{\small\color[rgb]{0.87890625,0,0.2890625}{{ else
}}}e_{2}}\Rightarrow{v}}\lx@proof@logical@and
x\sigma=\text{\small\color[rgb]{0.87890625,0,0.2890625}{{false}}}{\sigma}\sststile{}{\ell}{{e_{2}}\Rightarrow{v}}$
${\sigma}\sststile{}{\ell}{{\text{\small\color[rgb]{0.87890625,0,0.2890625}{{match
}}}x\text{\small\color[rgb]{0.87890625,0,0.2890625}{{
with}}}\begin{array}[t]{l}\text{\small\color[rgb]{0.10546875,0.00390625,0.375}{{|
}}}\text{\small\color[rgb]{0,0.578125,0.015625}{{leaf}}}\text{\small\color[rgb]{0.10546875,0.00390625,0.375}{{
-> }}}e_{1}\\\ \text{\small\color[rgb]{0.10546875,0.00390625,0.375}{{|
}}}\text{\text{\small\color[rgb]{0,0.578125,0.015625}{(}}{$x_{0}$}\text{\small\color[rgb]{0.10546875,0.00390625,0.375}{,}}{$x_{1}$}\text{\small\color[rgb]{0.10546875,0.00390625,0.375}{,}}{$x_{2}$}\text{\small\color[rgb]{0,0.578125,0.015625}{)}}}\text{\small\color[rgb]{0.10546875,0.00390625,0.375}{{
-> }}}e_{2}\end{array}}\Rightarrow{v}}\lx@proof@logical@and
x\sigma=\text{\text{\small\color[rgb]{0,0.578125,0.015625}{(}}{$t$}\text{\small\color[rgb]{0.10546875,0.00390625,0.375}{,}}{$a$}\text{\small\color[rgb]{0.10546875,0.00390625,0.375}{,}}{$u$}\text{\small\color[rgb]{0,0.578125,0.015625}{)}}}{\sigma^{\prime}}\sststile{}{\ell}{{e_{2}}\Rightarrow{v}}$
${\sigma}\sststile{}{\ell}{{\text{\small\color[rgb]{0.87890625,0,0.2890625}{{if
}}}x\text{\small\color[rgb]{0.87890625,0,0.2890625}{{ then
}}}e_{1}\text{\small\color[rgb]{0.87890625,0,0.2890625}{{ else
}}}e_{2}}\Rightarrow{v}}\lx@proof@logical@and
x\sigma=\text{\small\color[rgb]{0.87890625,0,0.2890625}{{true}}}{\sigma}\sststile{}{\ell}{{e_{1}}\Rightarrow{v}}$
Here $\sigma[x\mapsto w]$ denotes the update of the environment $\sigma$ such
that $\sigma[x\mapsto w](x)=w$ and the value of all other variables remains
unchanged. Furthermore, in the second match rule, we set
$\sigma^{\prime}\mathrel{:=}\sigma\mathrel{\uplus}\\{x_{0}\mapsto
t,x_{1}\mapsto a,x_{2}\mapsto u\\}$.

Figure 1: Big-Step Semantics

⬇

1splay a t = match t with

2 | leaf -> leaf

3 | (cl, c, cr) ->

4 if a = c then (cl, c, cr)

5 else if a < c then match cl with

6 | leaf -> (cl, c, cr)

7 | (bl, b, br) ->

8 if a = b then (bl, a, (br, c, cr))

9 else if a < b

10 then if bl = leaf then (bl, b, (br, c, cr))

11 else match splay a bl with

12 | (al, a’, ar) -> (al, a’, (ar, b, (br, c, cr)))

13 else if br = leaf then (bl, b, (br, c, cr))

14 else match splay a br with

15 | (al, a’, ar) -> ((bl, b, al), a’, (ar, c, cr))

16 else match cr with

17 | leaf -> (cl, c, cr)

18 | (bl, b, br) ->

19 if a = b then ((cl, c, bl), a, br)

20 else if a < b

21 then if bl = leaf then ((cl, c, bl), b, br)

22 else match splay a bl with

23 | (al, a’, ar) -> ((cl, c, al), a’, (ar, b, br))

24 else if br = leaf then ((cl, c, bl), b, br)

25 else match splay a br with

26 | (al, x, xa) -> (((cl, c, bl), b, al), x, xa)

Figure 2: Function splay.

_Splay trees_ have been introduced by Sleator and Tarjan [52, 53] as self-
adjusting binary search trees with strictly increasing in-order traversal.
There is no explicit balancing condition. All operations rely on a tree
rotating operation dubbed _splaying_ ; splay a t is performed by rotating
element $a$ to the root of tree $t$ while keeping in-order traversal intact.
If $a$ is not contained in $t$, then the last element found before leaf is
rotated to the tree. The complete definition is given in Figure 2. Based on
splaying, searching is performed by splaying with the sought element and
comparing to the root of the result. Similarly, the definition of insertion
and deletion depends on splaying. As an example the definition of insertion
and delete is given in Figure 3 and 4 respectively. See also [43] for full
algorithmic, formally verified, descriptions.

All basic operations can be performed in $O(\log n)$ amortised runtime. The
logarithmic amortised complexity is crucially achieved by local rotations of
subtrees in the definition of splay. Amortised cost analysis of splaying has
been provided for example by Sleator and Tarjan [52], Schoenmakers [47],
Nipkow [43], Okasaki [44], among others. Below, we follow Nipkow’s approach,
where the actual cost of splaying is measured by counting the number of calls
to
${\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\color[rgb]{0.10546875,0.00390625,0.375}\small{\@listingGroup{ltx_lst_identifier}{splay}}}}}}\colon\mathsf{B}\times\mathsf{T}\to\mathsf{T}$.

⬇

1insert a t = if t = leaf then (leaf, a, leaf)

2 else match splay a t with

3 | (l, a’, r) ->

4 if a = a’ then (l, a, r)

5 else if a < a’ then (l, a, (leaf, a’, r))

6 else ((l, a’, leaf), a, r)

Figure 3: Function insert.

⬇

1delete a t = if t = leaf then leaf

2 else match splay a t with

3 | (l, a’, r) ->

4 if a = a’ then if l = leaf then r

5 else match splay_max l with

6 | (l’, m, r’) -> (l’, m, r)

7 else (l, a’, r)

8

9splay_max t = match t with

10 | leaf -> leaf

11 | (l, b, r) -> match r with

12 | leaf -> (l, b, leaf)

13 | (rl, c, rr) ->

14 if rr = leaf then ((l, b, rl), c, leaf)

15 else match splay_max rr with

16 | (rrl, x, xa) -> (((l, b, rl), c, rrl), x, xa)

Figure 4: Functions delete and splay_max.

##  4 Resource Functions

In this section, we detail the basic potential functions employed and clarify
the definition of potentials used.

Only trees are assigned non-zero potential. This is not a severe restriction
as potentials for basic datatypes would only become essential, if the
construction of such types would emit actual costs. This is not the case in
our context. Moreover, note that lists can be conceived as trees of particular
shape. The potential $\Phi(t)$ of a tree $t$ is given as a non-negative linear
combination of basic functions, which essentially amount to “sums of logs”,
cf. Schoenmakers [47]. It suffices to specify the basic functions for the type
of trees $\mathsf{T}$. As already mentioned in Section 2, the _rank_
$\operatorname{\mathsf{rk}}(t)$ of a tree is defined as follows

${\displaystyle\operatorname{\mathsf{rk}}(\textup{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\color[rgb]{0.10546875,0.00390625,0.375}\small{\@listingGroup{ltx_lst_keywords2}{\color[rgb]{0,0.578125,0.015625}\small
leaf}}}}}})$ $\displaystyle\mathrel{:=}1$
${{{{\displaystyle\operatorname{\mathsf{rk}}(\textup{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\color[rgb]{0.10546875,0.00390625,0.375}\small(}}}{$t$}\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\color[rgb]{0.10546875,0.00390625,0.375}\small{\@listingGroup{ltx_lst_identifier}{,}}}}}
{$a$}\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\color[rgb]{0.10546875,0.00390625,0.375}\small{\@listingGroup{ltx_lst_identifier}{,}}}}}
{$u$}\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\color[rgb]{0.10546875,0.00390625,0.375}\small)}}}})$
$\displaystyle\mathrel{:=}\operatorname{\mathsf{rk}}(t)+\log^{\prime}(\lvert{t}\rvert)+\log^{\prime}(\lvert{u}\rvert)+\operatorname{\mathsf{rk}}(u)\hbox
to0.0pt{$\;$.\hss}$

We set $\log^{\prime}(n)\mathrel{:=}\log_{2}(\max\\{n,1\\})$, that is, the
(binary) logarithm function is defined for all numbers. This is merely a
technicality, introduced to ease the presentation. In the following, we will
denote the modified logarithmic function, simply as $\log$. Furthermore,
recall that $\lvert{t}\rvert$ denotes the number of leaves in tree $t$. The
definition of “rank” is inspired by the definition of potential in [47, 43],
but subtly changed to suit it to our context.

######  Definition 4.1.

The _basic potential functions_ of $\mathsf{Tree}$ are

  * •

$\lambda t.\operatorname{\mathsf{rk}}(t)$, or

  * •

$p_{(a,b)}\mathrel{:=}\lambda t.\log(a\cdot\lvert{t}\rvert+b)$, where $a,b$
are natural numbers.

The basic functions are denoted as $\mathcal{BF}$. Note that the constant
function $1$ is representable: $1=\lambda
t.\log(0\cdot\lvert{t}\rvert+2)=p_{(0,2)}$.

Following the recipe of the high-level description in Section 2, potentials or
more generally _resource functions_ become definable as linear combinations of
basic potential functions.

######  Definition 4.2.

A _resource function_
$r\colon\llbracket{\mathsf{T}}\rrbracket\to{\mathbb{R}^{+}_{0}}$ is a non-
negative linear combination of basic potential functions, that is,

$r(t)\mathrel{:=}\sum_{i\in{\mathbb{N}}}q_{i}\cdot p_{i}(t)\hbox
to0.0pt{$\;$,\hss}$

where $p_{i}\in\mathcal{BF}$. The set of resource functions is denoted as
$\mathcal{RF}$.

We employ $\ast$, natural numbers $i$ and pairs of natural numbers
$(a,b)_{a,b\in{\mathbb{N}}}$ as indices of the employed basic potential
functions. A _resource annotation over $\mathsf{T}$_, or simply _annotation_ ,
is a sequence $Q=[q_{\ast}]\cup[(q_{(a,b)})_{a,b\in{\mathbb{N}}}]$ with
$q_{\ast},q_{(a,b)}\in{\mathbb{Q}^{+}_{0}}$ with all but finitely many of the
coefficients $q_{\ast},q_{(a,b)}$ equal to 0. It represents a (finite) linear
combination of basic potential functions, that is, a resource function. The
empty annotation, that is, the annotation where all coefficients are set to
zero, is denoted as $\varnothing$.

######  Remark 4.3.

We use the convention that the sequence elements of resource annotations are
denoted by the lower-case letter of the annotation, potentially with
corresponding sub- or superscripts.

######  Definition 4.4.

The _potential_ of a tree $t$ with respect to an annotation $Q$, that is,
$Q=[q_{\ast}]\cup[(q_{(a,b)})_{a,b\in{\mathbb{N}}}]$, is defined as follows.

$\Phi({t}{\mid}{Q})\mathrel{:=}q_{\ast}\cdot\operatorname{\mathsf{rk}}(t)+\sum_{a,b\in{\mathbb{N}}}q_{(a,b)}\cdot
p_{(a,b)}(t)\hbox to0.0pt{$\;$,\hss}$

Recall that $p_{(a,b)}=\log(a\cdot\lvert{t}\rvert+b)$ and that
$\operatorname{\mathsf{rk}}$ is the rank function, defined above.

######  Example 4.5.

Let $t$ be a tree, then its potential could be defined as follows:
$\operatorname{\mathsf{rk}}(t)+3\cdot\log(\lvert{t}\rvert)+1$. With respect to
the above definition this potential becomes representable by setting
$q_{\ast}\mathrel{:=}1,q_{(1,0)}\mathrel{:=}3,q_{(0,2)}\mathrel{:=}1$. Thus,
$\Phi({t}{\mid}{Q})=\operatorname{\mathsf{rk}}(t)+3\cdot\log(\lvert{t}\rvert)+1$.
∎

We emphasise that the linear combination defined above is not independent.
Consider, for example $\log(2\lvert{t}\rvert+2)=\log(\lvert{t}\rvert+1)+1$.

_Analysis of Products of Trees._ We now lift the basic potential functions
$p_{(a,b)}$ of a single tree to products of trees. As discussed in Section 2,
we define the potential functions $p_{(a_{1},\dots,a_{m},b)}$ for a sequence
of $m$ trees $t_{1},\dots,t_{m}$, by setting:

$p_{(a_{1},\dots,a_{m},b)}(t_{1},\dots,t_{m})\mathrel{:=}\log({a_{1}\cdot\lvert{t_{1}}\rvert}+\dots+{a_{m}\cdot\lvert{t_{m}}\rvert}+b)\hbox
to0.0pt{$\;$,\hss}$

where $a_{1},\dots,a_{m},b\in{\mathbb{N}}$. Equipped with this definition, we
generalise annotations to sequences of trees. An annotation for a sequence of
length $m$ is a sequence
$Q=[q_{1},\dots,q_{m}]\cup[(q_{(a_{m},\dots,a_{n},b)})_{a_{i},b\in{\mathbb{N}}}]$,
again vanishing almost everywhere. Note that an annotation of length $1$ is
simply an annotation as defined above, where the coefficient $q_{1}$ is set
equal to the coefficient $q_{\ast}$. Based on this, the potential of a
sequence of trees $t_{1},\dots,t_{m}$ is defined as follows:

######  Definition 4.6.

Let $t_{1},\dots,t_{m}$ be trees and let
$Q=[q_{1},\dots,q_{m}]\cup[(q_{(a_{1},\dots,a_{m},b)})_{a_{i},b\in{\mathbb{N}}}]$
be an annotation of length $m$ as above. We define

$\Phi({t_{1},\dots,t_{m}}{\mid}{Q})\mathrel{:=}\sum_{i=1}^{m}q_{i}\cdot\operatorname{\mathsf{rk}}(t_{i})+\sum_{a_{1},\dots,a_{m},b\in{\mathbb{N}}}q_{(a_{1},\dots,a_{m},b)}\cdot
p_{(a_{1},\dots,a_{m},b)}(t_{1},\dots,t_{m})\hbox to0.0pt{$\;$,\hss}$

where
$p_{(a_{1},\dots,a_{m},b)}(t_{1},\dots,t_{m})\mathrel{:=}\log({a_{1}\cdot\lvert{t_{1}}\rvert}+\dots+{a_{m}\cdot\lvert{t_{m}}\rvert}+b)$
as defined above. Note that for an empty sequence of trees, we have
$\Phi({\epsilon}{\mid}{Q})\mathrel{:=}\sum_{b\in{\mathbb{N}}}q_{b}\log(b)$.

Let $t$ be a tree. Note that the rank function $\operatorname{\mathsf{rk}}(t)$
amounts to the sum of the logarithms of the size of subtrees of $t$. In
particular if the tree $t$ simplifies to a list of length $n$, then
$\operatorname{\mathsf{rk}}(t)=(n+1)+\sum_{i=1}^{n}\log(i)$. Moreover, as
$\sum_{i=1}^{n}\log(i)\in\Theta(n\log n)$, the above defined potential
functions are sufficiently rich to express linear combinations of sub- and
super-linear functions.

Let $\sigma$ denote a substitution, let $\Gamma$ denote a typing context and
let ${{x_{1}}{\colon}\\!{\mathsf{T}}},\dots,{{x_{m}}{\colon}\\!{\mathsf{T}}}$
denote all tree types in $\Gamma$. A _resource annotation for $\Gamma$_ or
simply _annotation_ is an annotation for the sequence of trees
${x_{1}\sigma},\dots,{x_{m}\sigma}$. We define the _potential_ of
$\Phi({\Gamma}{\mid}{Q})$ with respect to $\sigma$ as
$\Phi({\sigma};{\Gamma}{\mid}{Q})\mathrel{:=}\Phi({{x_{1}\sigma},\dots,{x_{m}\sigma}}{\mid}{Q})$.

######  Definition 4.7.

An _annotated signature_ $\overline{\mathcal{F}}$ is a mapping from functions
$f$ to sets of pairs consisting of the annotation type for the arguments of
$f$, ${\alpha_{1}\times\dots\times\alpha_{n}}{\mid}{Q}$ and the annotation
type ${\beta}{\mid}{Q^{\prime}}$ for the result:

$\overline{\mathcal{F}}(f)\mathrel{:=}\left\\{{\alpha_{1}\times\dots\times\alpha_{n}}{\mid}{Q}\to{\beta}{\mid}{Q^{\prime}}\colon\text{\parbox{215.2771pt}{$f$
takes $n$ arguments of which $m$ are trees, $Q$ is a resource annotation of
length $m$ and $Q^{\prime}$ a resource annotation of length
$1$}}\right\\}\hbox to0.0pt{$\;$.\hss}$

Note that $m\leqslant n$ by definition.

We confuse the signature and the annotated signature and denote the latter
simply as $\mathcal{F}$. Instead of
${\alpha_{1}\times\dots\times\alpha_{n}}{\mid}{Q}\to{\beta}{\mid}{Q^{\prime}}\in\mathcal{F}(f)$,
we typically write
${f}{\colon}\\!{{\alpha_{1}\times\dots\times\alpha_{n}}{\mid}{Q}\to{\beta}{\mid}{Q^{\prime}}}$.
As our analysis makes use of a _cost-free semantics_ any function symbol is
possibly equipped with a _cost-free_ signature, independent of $\mathcal{F}$.
The cost-free signature is denoted as $\mathcal{F}^{\text{cf}}$.

######  Example 4.8.

Consider the function splay: $\mathsf{B}\times\mathsf{T}\to\mathsf{T}$. The
induced annotated signature is given as
${\mathsf{B}\times\mathsf{T}}{\mid}{Q}\to{\mathsf{T}}{\mid}{Q^{\prime}}$,
where $Q\mathrel{:=}[q_{\ast}]\cup[(q_{(a,b)})_{a,b\in{\mathbb{N}}}]$ and
$Q^{\prime}\mathrel{:=}[q^{\prime}_{\ast}]\cup[(q^{\prime}_{(a,b)})_{a,b\in{\mathbb{N}}}]$.
The logarithmic amortised cost of splaying is then expressible through the
following setting: $q_{\ast}\mathrel{:=}1$, $q_{(1,0)}=3$, $q_{(0,2)}=1$,
$q^{\prime}_{\ast}\mathrel{:=}1$. All other coefficients are zero.

This amounts to a potential of the arguments
$\operatorname{\mathsf{rk}}(t)+3\log(\lvert{t}\rvert)+1$, while for the result
we consider only its rank, that is, the annotation expresses
$3\log(\lvert{t}\rvert)+1$ as the logarithmic cost of splaying. The
correctness of the induced logarithmic amortised costs for the zig-zig case of
splaying is verified in Section 6 and is also automatically verified by our
prototype. ∎

Suppose $\Phi({t_{1},\dots,t_{n},u_{1},u_{2}}{\mid}{Q})$ denotes an annotated
sequence of length $n+2$. Suppose $u_{1}=u_{2}$ and we want to _share_ the
values $u_{i}$, that is, the corresponding function arguments appear multiple
times in the body of the function definition. Then we make use of the operator
$\curlyvee\\!({Q})$ that adapts the potential suitably. The operator is also
called _sharing operator_.

######  Lemma 4.9.

Let $t_{1},\dots,t_{n},u_{1},u_{2}$ denote a sequence of trees of length $n+2$
with annotation $Q$. Then there exists a resource annotation
$\curlyvee\\!({Q})$ such that
$\Phi({t_{1},\dots,t_{n},u_{1},u_{2}}{\mid}{Q})=\Phi({t_{1},\dots,t_{n},u}{\mid}{\curlyvee\\!({Q})})$,
if $u_{1}=u_{2}=u$.

######  Proof 4.10.

Wlog. we assume $n=0$. Thus, let
$Q=[q_{1},q_{2}]\cup[(q_{(a_{1},a_{2},b)})_{a_{i}\in{\mathbb{N}}}]$. By
definition

$\Phi({u_{1},u_{2}}{\mid}{Q})=q_{1}\cdot\operatorname{\mathsf{rk}}(u_{1})+q_{2}\cdot\operatorname{\mathsf{rk}}(u_{2})+\sum_{a_{1},a_{2},b\in{\mathbb{N}}}q_{(a_{1},a_{2},b)}\cdot
p_{(a_{1},a_{2},b)}(u_{1},u_{2})\hbox to0.0pt{$\;$,\hss}$

where
$p_{(a_{1},a_{2},b)}(u_{1},u_{2})=\log(a_{1}\cdot\lvert{u_{1}}\rvert+a_{2}\cdot\lvert{u_{2}}\rvert+b)$.
By assumption $u=u_{1}=u_{2}$. Thus, we obtain

$\displaystyle\Phi({u,u}{\mid}{Q})$
$\displaystyle=q_{1}\cdot\operatorname{\mathsf{rk}}(u)+q_{2}\cdot\operatorname{\mathsf{rk}}(u)+\sum_{a_{1},a_{2},b\in{\mathbb{N}}}q_{(a_{1},a_{2},b)}\cdot
p_{(a_{1},a_{2},b)}(u,u)$
$\displaystyle=(q_{1}+q_{2})\operatorname{\mathsf{rk}}(u)+\sum_{a_{1}+a_{2},b\in{\mathbb{N}}}q_{(a_{1}+a_{2},b)}\cdot
p_{(a_{1}+a_{2},b)}(u)$ $\displaystyle=\Phi({u}{\mid}{\curlyvee\\!({Q})})\hbox
to0.0pt{$\;$,\hss}$

for suitable defined annotation $\curlyvee\\!({Q})$, whose definition can be
directly read off from the above constraints.

We emphasise that the definability of the sharing annotation
$\curlyvee\\!({Q})$ is based on the fact that the basic potential functions
$p_{(a_{1},\dots,a_{m},b)}$ have been carefully chosen so that

$p_{(a_{0},a_{1},a_{2},\dots,a_{m},b)}(x_{1},x_{1},\dots,x_{m})=p_{(a_{0}+a_{1},a_{2},\dots,a_{m},b)}(x_{1},x_{2},\dots,x_{m})\hbox
to0.0pt{$\;$,\hss}$

holds, cf. Section 2.

######  Remark 4.11.

We observe that the proof-theoretic analogue of the sharing operation
constitutes in a contraction rule, if the type system is conceived as a proof
system.

Let $Q=[q_{\ast}]\cup[(q_{(a,b)})_{a,b\in{\mathbb{N}}}]$ be an annotation and
let $K\in{\mathbb{Q}^{+}_{0}}$. Then we define $Q^{\prime}\mathrel{:=}Q+K$ as
follows:
$Q^{\prime}=[q_{\ast}]\cup[(q^{\prime}_{(a,b)})_{a,b\in{\mathbb{N}}}]$, where
$q^{\prime}_{(0,2)}\mathrel{:=}q_{(0,2)}+K$ and for all $(a,b)\not=(0,2)$
$q_{(a,b)}^{\prime}\mathrel{:=}q_{(a,b)}$. By definition the annotation
coefficient $q_{(0,2)}$ is the coefficient of the basic potential function
$p_{(0,2)}(t)=\log(0\lvert{t}\rvert+2)=1$, so the annotation $Q+K$, adds cost
$K$ to the potential induced by $Q$. Further, we define the multiplication of
an annotation $Q$ by a constant $K$, denoted as $K\cdot Q$ pointwise.
Moreover, let $P=[p_{\ast}]\cup[(p_{(a,b)})_{a,b\in{\mathbb{N}}}]$ be another
annotation. Then the addition $P+Q$ of annotations $P,Q$ is similarly defined
pointwise.

##  5 Logarithmic Amortised Resource Analysis

${\varnothing}{\mid}{Q+k}\vdash{\text{\small\color[rgb]{0,0.578125,0.015625}{{leaf}}}}{\colon}\\!{\mathsf{T}}{\mid}{Q^{\prime}}\lx@proof@logical@and\forall
c\geqslant 2\ q_{(c)}=\sum_{a+b=c}q^{\prime}_{(a,b)}k=q^{\prime}_{\ast}$
${\Gamma}{\mid}{Q+K}\vdash{e}{\colon}\\!{\alpha}{\mid}{Q^{\prime}+K}\lx@proof@logical@and{\Gamma}{\mid}{Q}\vdash{e}{\colon}\\!{\alpha}{\mid}{Q^{\prime}}K\geqslant
0$
${\Gamma,{x}{\colon}\\!{\alpha}}{\mid}{Q}\vdash{e}{\colon}\\!{\beta}{\mid}{Q^{\prime}}\lx@proof@logical@and{\Gamma}{\mid}{R}\vdash{e}{\colon}\\!{\beta}{\mid}{Q^{\prime}}r_{i}=q_{i}r_{(\vec{a},b)}=q_{(\vec{a},0,b)}$
${{x_{1}}{\colon}\\!{\mathsf{T}},{x_{2}}{\colon}\\!{\mathsf{B}},{x_{3}}{\colon}\\!{\mathsf{T}}}{\mid}{Q}\vdash{\text{\small\color[rgb]{0,0.578125,0.015625}{(}}{x_{1}}\text{\small\color[rgb]{0.10546875,0.00390625,0.375}{,}}{x_{2}}\text{\small\color[rgb]{0.10546875,0.00390625,0.375}{,}}{x_{3}}\text{\small\color[rgb]{0,0.578125,0.015625}{)}}}{\colon}\\!{\mathsf{T}}{\mid}{Q^{\prime}}\lx@proof@logical@and
q_{1}=q_{2}=q^{\prime}_{\ast}q_{(1,0,0)}=q_{(0,1,0)}=q^{\prime}_{\ast}q_{(a,a,c)}=q^{\prime}_{(a,c)}$
${{x_{1}}{\colon}\\!{\alpha},{x_{2}}{\colon}\\!{\alpha}}{\mid}{Q}\vdash{x_{1}\circ
x_{2}}{\colon}\\!{\mathsf{Bool}}{\mid}{Q}\circ\in\\{<,>,=\\}$
${\Gamma,{x}{\colon}\\!{\mathsf{Bool}}}{\mid}{Q}\vdash{\text{\small\color[rgb]{0.87890625,0,0.2890625}{{if
}}}x\text{\small\color[rgb]{0.87890625,0,0.2890625}{{ then
}}}e_{1}\text{\small\color[rgb]{0.87890625,0,0.2890625}{{ else
}}}e_{2}}{\colon}\\!{\alpha}{\mid}{Q^{\prime}}\lx@proof@logical@and{\Gamma}{\mid}{Q}\vdash{e_{1}}{\colon}\\!{\alpha}{\mid}{Q^{\prime}}{\Gamma}{\mid}{Q}\vdash{e_{2}}{\colon}\\!{\alpha}{\mid}{Q^{\prime}}$
${\Gamma,{x}{\colon}\\!{\mathsf{T}}}{\mid}{Q}\vdash{\text{\small\color[rgb]{0.87890625,0,0.2890625}{{match
}}}x\text{\small\color[rgb]{0.87890625,0,0.2890625}{{ with
}}}\text{\small\color[rgb]{0.10546875,0.00390625,0.375}{{|
}}}\text{\small\color[rgb]{0,0.578125,0.015625}{{leaf}}}\text{\small\color[rgb]{0.10546875,0.00390625,0.375}{{
-> }}}e_{1}\text{\small\color[rgb]{0.10546875,0.00390625,0.375}{{|
}}}\text{\small\color[rgb]{0,0.578125,0.015625}{(}}{x_{1}}\text{\small\color[rgb]{0.10546875,0.00390625,0.375}{,}}{x_{2}}\text{\small\color[rgb]{0.10546875,0.00390625,0.375}{,}}{x_{3}}\text{\small\color[rgb]{0,0.578125,0.015625}{)}}\text{\small\color[rgb]{0.10546875,0.00390625,0.375}{{
->
}}}e_{2}}{\colon}\\!{\alpha}{\mid}{Q^{\prime}}\lx@proof<EMAIL_ADDRESS>$r_{(\vec{a},a,a,b)}=q_{(\vec{a},a,b)}$\\\
$p_{(\vec{a},c)}=\sum_{a+b=c}q_{(\vec{a},a,b)}$\\\
${\Gamma}{\mid}{P+q_{m+1}}\vdash{e_{1}}{\colon}\\!{\alpha}{\mid}{Q^{\prime}}$
\end{minipage}\begin{minipage}[b]{150.69397pt} $r_{m+1}=r_{m+2}=q_{m+1}$ \\\
$r_{(\vec{0},1,0,0)}=r_{(\vec{0},0,1,0)}=q_{m+1}$ \\\
${\Gamma,{x_{1}}{\colon}\\!{\mathsf{T}},{x_{2}}{\colon}\\!{\mathsf{B}},{x_{3}}{\colon}\\!{\mathsf{T}}}{\mid}{R}\vdash{e_{2}}{\colon}\\!{\alpha}{\mid}{Q^{\prime}}$
\end{minipage}q_{i}=r_{i}=p_{i}$
${\Gamma,\Delta}{\mid}{Q}\vdash{\text{\small\color[rgb]{0.87890625,0,0.2890625}{{let
}}}x\text{\small\color[rgb]{0.10546875,0.00390625,0.375}{{ =
}}}e_{1}\text{\small\color[rgb]{0.87890625,0,0.2890625}{{ in
}}}e_{2}}{\colon}\\!{\beta}{\mid}{Q^{\prime}}\begin{minipage}[b]{353.05444pt}
\centering$p_{i}=q_{i}$ \quad$p_{(\vec{a},c)}=q_{(\vec{a},\vec{0},c)}$
\quad$r_{j}=q_{m+j}$ \quad$r_{k+1}=p^{\prime}_{\ast}$
\quad$r_{(\vec{0},d,e)}=p^{\prime}_{(d,e)}$
\quad$\forall\vec{b}\neq\vec{0}\left(r_{(\vec{b},0,0)}=q_{(\vec{0},\vec{b},0)}\right)$
\\\ $\forall\vec{b}\neq\vec{0},\vec{a}\neq\vec{0}\lor c\neq 0\
\left(q_{(\vec{a},\vec{b},c)}=\sum_{(d,e)}p^{(\vec{b},d,e)}_{(\vec{a},c)}\right)$
\\\ $\forall\vec{b}\neq\vec{0},d\neq 0\lor e\neq 0\
\left(r_{(\vec{b},d,e)}={p^{\prime}}^{(\vec{b},d,e)}_{(d,e)}\wedge\forall(d^{\prime},e^{\prime})\neq(d,e)\
\left({p^{\prime}}^{(\vec{b},d,e)}_{(d^{\prime},e^{\prime})}=0\right)\wedge{}\right.$\\\
$\left.{}\land\sum_{(a,c)}p^{(\vec{b},d,e)}_{(\vec{a},c)}\geq{p^{\prime}}^{(\vec{b},d,e)}_{(d,e)}\land\forall\vec{a}\neq\vec{0}\lor
c\neq 0\ \left(p^{(\vec{b},d,e)}_{(\vec{a},c)}\neq
0\rightarrow{p^{\prime}}^{(\vec{b},d,e)}_{(d,e)}\leqslant
p^{(\vec{b},d,e)}_{(\vec{a},c)}\right)\right)$\\\
${\Gamma}{\mid}{P}\vdash{e_{1}}{\colon}\\!{\mathsf{T}}{\mid}{P^{\prime}}$
\hfill$\forall{\vec{b}\neq\vec{0},d\neq 0\lor e\neq 0}\
\left({\Gamma}{\mid}{P^{(\vec{b},d,e)}}\vdash^{\text{cf}}{e_{1}}{\colon}\\!{\mathsf{T}}{\mid}{{P^{\prime}}^{(\vec{b},d,e)}}\right)$
\hfill${\Delta,{x}{\colon}\\!{\mathsf{T}}}{\mid}{R}\vdash{e_{2}}{\colon}\\!{\beta}{\mid}{Q^{\prime}}$
\@add@centering\end{minipage}$
${\Gamma,\Delta}{\mid}{Q}\vdash{\text{\small\color[rgb]{0.87890625,0,0.2890625}{{let
}}}x\text{\small\color[rgb]{0.10546875,0.00390625,0.375}{{ =
}}}e_{1}\text{\small\color[rgb]{0.87890625,0,0.2890625}{{ in
}}}e_{2}}{\colon}\\!{\beta}{\mid}{Q^{\prime}}\lx@proof<EMAIL_ADDRESS>$p_{i}=q_{i}$ \quad$p_{(\vec{a},c)}=q_{(\vec{a},\vec{0},c)}$\\\
${\Gamma}{\mid}{P}\vdash{e_{1}}{\colon}\\!{\alpha}{\mid}{\varnothing}$
\end{minipage}\begin{minipage}[b]{107.63855pt}
$q_{(\vec{0},\vec{b},c)}=r_{(\vec{b},c)}$ \ ($\vec{b}\not=\vec{0}$) \\\
${\Delta,{x}{\colon}\\!{\alpha}}{\mid}{R}\vdash{e_{2}}{\colon}\\!{\beta}{\mid}{Q^{\prime}}$
\end{minipage}\begin{minipage}[b]{51.6665pt} $r_{j}=q_{m+j}$\\\
$\alpha\not=\mathsf{T}$ \end{minipage}$
${\Gamma,{z}{\colon}\\!{\alpha}}{\mid}{\curlyvee\\!({Q})}\vdash{e[z,z]}{\colon}\\!{\beta}{\mid}{Q^{\prime}}{\Gamma,{x}{\colon}\\!{\alpha},{y}{\colon}\\!{\alpha}}{\mid}{Q}\vdash{e[x,y]}{\colon}\\!{\beta}{\mid}{Q^{\prime}}$
${\Gamma}{\mid}{Q}\vdash{e}{\colon}\\!{\alpha}{\mid}{Q^{\prime}}\lx@proof@logical@and{\Gamma}{\mid}{P}\vdash{e}{\colon}\\!{\alpha}{\mid}{P^{\prime}}\Phi({\Gamma}{\mid}{P})\leqslant\Phi({\Gamma}{\mid}{Q})\Phi({\Gamma}{\mid}{P^{\prime}})\geqslant\Phi({\Gamma}{\mid}{Q^{\prime}})$
${{x}{\colon}\\!{\alpha}}{\mid}{Q}\vdash{x}{\colon}\\!{\alpha}{\mid}{Q}\text{$x$
a variable}$
${{x_{1}}{\colon}\\!{\alpha_{1}},\dots,{x_{n}}{\colon}\\!{\alpha_{n}}}{\mid}{P+K\cdot
Q}\vdash{f(x_{1},\dots,x_{n})}{\colon}\\!{\beta}{\mid}{(P^{\prime}+K\cdot
Q^{\prime})-1}\lx@proof@logical@and{\alpha_{1}\times\cdots\times\alpha_{n}}{\mid}{P}\to{\beta}{\mid}{P^{\prime}}\in\mathcal{F}(f){\alpha_{1}\times\cdots\times\alpha_{n}}{\mid}{Q}\to{\beta}{\mid}{Q^{\prime}}\in\mathcal{F}^{\text{cf}}(f)K\in{\mathbb{Q}^{+}_{0}}$
To ease notation, we set $\vec{a}\mathrel{:=}a_{1},\dots,a_{m}$,
$\vec{b}\mathrel{:=}b_{1},\dots,b_{k}$ for vectors of indices
$a_{i},b_{j}\in{\mathbb{N}}$. Further, $i\in\\{1,\dots,m\\}$,
$j\in\\{1,\dots,k\\}$ and $a,b,c,d,e\in{\mathbb{N}}$. Sequence elements of
annotations, which are not constrained are set to zero.

Figure 5: Type System for Logarithmic Amortised Resource Analysis

In this section, we present the central contribution of this work. We
delineate a novel type-and-effect system incorporating a potential-based
amortised resource analysis capable of expressing _logarithmic_ amortised
costs. Soundness of the approach is established in Theorem 5.6.

Our potential-based amortised resource analysis is couched in a type system,
given in Figure 5. If the type judgement
${\Gamma}{\mid}{Q}\vdash{e}{\colon}\\!{\alpha}{\mid}{Q^{\prime}}$ is
derivable, then the worst-case cost of evaluating the expression $e$ is bound
from above by the difference between the potential
$\Phi({\sigma};{\Gamma}{\mid}{Q})$ before the execution and the potential
$\Phi({v}{\mid}{Q^{\prime}})$ of the value $v$ obtained through the evaluation
of the expression $e$. The typing system makes use of a _cost-free_ semantics,
which does not attribute any costs to the calculation. The cost-free typing
judgement is denoted as
${\Gamma}{\mid}{Q}\vdash^{\text{cf}}{e}{\colon}\\!{\alpha}{\mid}{Q^{\prime}}$
and based on a cost-free variant of the application rule, denoted as
$(\mathsf{{app:cf}})$. The rule $(\mathsf{{app:cf}})$ is defined as the rule
$(\mathsf{{app}})$, however, no costs are accounted for. Wrt. the cost-free
semantics, the _empty signature_ , denoted as
${\alpha_{1}\times\dots\times\alpha_{n}}{\mid}{\varnothing}\to{\beta}{\mid}{\varnothing}$,
is always admissible.

######  Remark 5.1.

Note, that if
${\alpha_{1}\times\dots\times\alpha_{n}}{\mid}{P}\to{\beta}{\mid}{P^{\prime}}$
and
${\alpha_{1}\times\dots\times\alpha_{n}}{\mid}{Q}\to{\beta}{\mid}{Q^{\prime}}$
are both cost-free signatures for a function $f$, then any linear combination
is admissable as cost-free signature of $f$. Ie. we can assume
${\alpha_{1}\times\dots\times\alpha_{n}}{\mid}{K\cdot P+L\cdot
Q}\to{\beta}{\mid}{K\cdot P^{\prime}+L\cdot
Q^{\prime}}\in\mathcal{F}^{\text{cf}}(f)$, where $K,L\in{\mathbb{Q}^{+}_{0}}$.

######  Remark 5.2.

Principally the type system can be parameterised in the resource metric (see
e.g.[24]). In this paper, we focus on amortised and worst-case runtime
complexity, symbolically measured through the number of function applications.
It is straightforward to generalise this type system to other monotone cost
models. Wrt. non-monotone costs, like eg. heap usage, we expect the type
system can also be readily be adapted, but this is outside the scope of the
paper.

We consider the typing rules in turn; recall the convention that sequence
elements of annotations are denoted by the lower-case letter of the
annotation. Further, note that sequence elements which do not occur in any
constraint are set to zero. The variable rule $(\mathsf{{var}})$ types a
variable of unspecified type $\alpha$. As no actual costs are required the
annotation is unchanged. Similarly no resources are lost through the use of
control operators. Hence the definition of the rules $(\mathsf{{cmp}})$ and
$(\mathsf{{ite}})$ is straightforward.

As exemplary constructor rules, we have rule $(\mathsf{{leaf}})$ for the empty
tree and rule $(\mathsf{{node}})$ for the node constructor. Both rules define
suitable constraints on the resource annotations to guarantee that the
potential of the values is correctly represented.

The application rule $(\mathsf{{app}})$ represents the application of a rule
given in $\mathsf{P}$. Each application emits actual cost $1$, which is
indicated in the addition of $1$ to the annotation $Q$. In its simplest form,
that is, for the factor $K=1$, the rule allows to directly read off the
required annotations for the typing context

In the pattern matching rule $(\mathsf{{match}})$ the potential freed through
the destruction of the tree construction is added to the annotation $R$, which
is used in the right premise of the rule. Note that the length of the
annotation $R$ is $m+2$, where $m$ equals the number of tree types in the type
context $\Gamma$.

The constraints expressed in the typing rules $(\mathsf{{let:T}})$ and
$(\mathsf{{let:gen}})$, guarantee that the potential provided through
annotation $Q$ is distributed among the call to $e_{1}$ and $e_{2}$, that is,
this rule takes care of function composition. The numbers $m$, $k$,
respectively, denote the number of tree types in $\Gamma$, $\Delta$. Due to
the sharing rule—discussed in a moment—we can assume wlog. that each variable
in $e_{1}$ and $e_{2}$ occurs at most once.

First, consider the rule $(\mathsf{{let:gen}})$, that is, the expression
$e_{1}$ evaluates to a value $w$ of arbitrary type $\alpha\not=\mathsf{Tree}$.
In this case the resulting value $w$ cannot carry any potential. This is
indicated through the empty annotation $\varnothing$ in the typing judgement
${\Gamma}{\mid}{P}\vdash{e_{1}}{\colon}\\!{\alpha}{\mid}{\varnothing}$.
Similarly, in the judgement
${\Delta,{x}{\colon}\\!{\alpha}}{\mid}{R}\vdash{e_{2}}{\colon}\\!{\beta}{\mid}{Q^{\prime}}$
for the expression $e_{2}$, all available potential prior to the execution of
$e_{2}$ stems from the potential embodied in the type context $\Delta$ wrt.
annotation $Q$. This is enforced by the corresponding constraints. Suppose for
$\vec{a}\not=\vec{0}$ and $\vec{b}\not=\vec{0}$, $q_{(\vec{a},\vec{b},c)}$
would be non-zero. Then the corresponding shared potential between the
contexts $\Gamma$ and $\Delta$ wrt. $Q$ is discarded by the rule, as there is
no possibility this potential is attached to the result type $\alpha$.

Second, consider the more involved rule $(\mathsf{{let:T}})$. To explain this
rule, we momentarily assume that in $Q$ no potential is shared, that is,
$q_{(\vec{a},\vec{b},c)}=0$, whenever
$\vec{a}\not=\vec{0},\vec{b}\not=\vec{0}$. In this sub-case the rule can be
simplified as follows:

${\Gamma,\Delta}{\mid}{Q}\vdash{\text{\small\color[rgb]{0.87890625,0,0.2890625}{{let
}}}x\text{\small\color[rgb]{0.10546875,0.00390625,0.375}{{ =
}}}e_{1}\text{\small\color[rgb]{0.87890625,0,0.2890625}{{ in
}}}e_{2}}{\colon}\\!{\beta}{\mid}{Q^{\prime}}\lx@proof<EMAIL_ADDRESS>$p_{i}=q_{i}$\\\ $p_{(\vec{a},c)}=q_{(\vec{a},\vec{0},c)}$\\\
${\Gamma}{\mid}{P}\vdash{e_{1}}{\colon}\\!{\mathsf{T}}{\mid}{P^{\prime}}$
\end{minipage}\begin{minipage}[b]{129.16626pt}
$r_{(\vec{b},0,c)}=q_{(\vec{0},\vec{b},c)}$ \ ($\vec{b}\not=\vec{0}$) \\\
${\Delta,{x}{\colon}\\!{\mathsf{T}}}{\mid}{R}\vdash{e_{2}}{\colon}\\!{\beta}{\mid}{Q^{\prime}}$
\end{minipage}\begin{minipage}[b]{86.11084pt} $r_{j}=q_{m+j}$\\\
$r_{k+1}=p^{\prime}_{\ast}$\\\ $r_{(\vec{0},a,c)}=p^{\prime}_{(a,c)}$
\end{minipage}$

Again the potential in $\Gamma,\Delta$ (wrt. annotation $Q$) is distributed
for the typing of the expressions $e_{1}$, $e_{2}$, respectively, which is
governed by the constraints on the annotations. The simplified rule is
obtained, as the assumption that no shared potential exists, makes almost all
constraints vacuous. In particular, the cost-free derivation
${\Gamma}{\mid}{P^{(\vec{b},d,e)}}\vdash^{\text{cf}}{e_{1}}{\colon}\\!{\mathsf{T}}{\mid}{{P^{\prime}}^{(\vec{b},d,e)}}$
is not required.

Finally, consider the most involved sub-case, where shared potentials are
possible. Contrary to the simplified rules discussed above, such shared
potential cannot be split between the type contexts $\Gamma$ and $\Delta$,
respectively. Thus, the full rule necessarily employs the _cost-free
semantics_. Consequently, the premise
${\Gamma}{\mid}{P^{(\vec{b},d,e)}}\vdash^{\text{cf}}{e_{1}}{\colon}\\!{\alpha}{\mid}{{P^{\prime}}^{(\vec{b},d,e)}}$
expresses that for all non-zero vectors $\vec{b}$ and arbitrary indices $d$,
$e$, the potentials $\Phi({\Gamma}{\mid}{P^{(\vec{b},d,e)}})$ suffices to
cover the potential $\Phi({\alpha}{\mid}{{P^{\prime}}^{(\vec{b},d,e)}})$, if
no extra costs are emitted (compare Section 2). Intuitively this represents
that the values do not increase during the evaluation of $e_{1}$ to value $w$.

At last, the type system makes use of structural rules, like the _sharing_
rule $(\mathsf{{share}})$ and the weakening rules $(\mathsf{{w:var}})$ and
$(\mathsf{{w}})$. The _sharing_ rule employs the sharing operator, defined in
Lemma 4.9. Note that the variables $x,y$ introduced in the assumption of the
typing rule are fresh variables, that do not occur in $\Gamma$. Similarly, the
rule $(\mathsf{{shift}})$ allows to shift the potential before and after
evaluation of the expression $e$ by a constant $K$.

Note that the weakening rules embody changes in the potential of the type
context of expressions considered. This amounts to the comparison on
logarithmic expressions, principally a non-trivial task that cannot be
directly represented as constraints in the type system. Instead, the rule
$(\mathsf{{w}})$ employs a symbolic potential expressions for these
comparisons, replacing actual values for tree by variables. Let $\Gamma$
denote a type context containing the type declarations
${x_{1}}{\colon}\\!{\mathsf{T}},\dots,{x_{m}}{\colon}\\!{\mathsf{T}}$ and let
$Q$ be an annotation of length $m$. Then the _symbolic potential_ , denoted as
$\Phi({\Gamma}{\mid}{Q})$, is defined as follows.

$\Phi({x_{1},\dots,x_{m}}{\mid}{Q})\mathrel{:=}\sum_{i=1}^{m}q_{i}\cdot\operatorname{\mathsf{rk}}(x_{i})+\sum_{a_{1},\dots,a_{m},b\in{\mathbb{N}}}q_{(a_{1},\dots,a_{m},b)}\cdot
p_{(a_{1},\dots,a_{m},b)}(x_{1},\dots,x_{m})\hbox to0.0pt{$\;$,\hss}$

where
$p_{(a_{1},\dots,a_{m},b)}(x_{1},\dots,x_{m})=\log({a_{1}\cdot\lvert{x_{1}}\rvert}+\dots+{a_{m}\cdot\lvert{x_{m}}\rvert}+b)$.
In order to actually solve these constraints over symbolic potentials, we have
to _linearise_ the underlying comparisons of logarithmic expressions. This is
taken up again in Section 7.

######  Definition 5.3.

A program $\mathsf{P}$ is called _well-typed_ if for any rule
$f(x_{1},\dots,x_{k})=e\in\mathsf{P}$ and any annotated signature
${\alpha_{1}\times\dots\times\alpha_{k}}{\mid}{Q}\to{\beta}{\mid}{Q^{\prime}}\in\mathcal{F}(f)$,
we have
${{x_{1}}{\colon}\\!{\alpha_{1}},\dots,{x_{k}}{\colon}\\!{\alpha_{k}}}{\mid}{Q}\vdash{e}{\colon}\\!{\beta}{\mid}{Q^{\prime}}$.
A program $\mathsf{P}$ is called _cost-free_ well-typed, if the cost-free
typing relation is employed.

Before we state and proof the soundness of the presented type-and-effect
system, we establish the following auxiliary result, employed in the correct
assessment of the transfer of potential in the case of function composition,
see Figure 5. See also the high-level description provided in Section 2.

######  Lemma 5.4.

Assume $\sum_{i}q_{i}\log a_{i}\geqslant q\log b$ for some rational numbers
$a_{i},b>0$ and $q_{i}\geqslant q$. Then, $\sum_{i}q_{i}\log(a_{i}+c)\geqslant
q\log(b+c)$ for all $c\geqslant 1$.

######  Proof 5.5.

Wlog. we can assume $q=1$ and $q_{i}\geqslant 1$, as otherwise we simply
divide the assumed inequality by $q$. Further, observe that the assumption
$\sum_{i}q_{i}\log a_{i}\geqslant q\log b$ is equivalent to

$\prod_{i}a_{i}^{q_{i}}\geqslant b\hbox to0.0pt{$\;$.\hss}$ (9)

First, we prove that

$(x+y)^{r}\geqslant x^{r}+y^{r}\quad r\geqslant 1\quad x,y\geqslant 0\hbox
to0.0pt{$\;$.\hss}$ (10)

This is proved as follows. Fix some $x\geqslant 0$ and consider $(x+y)^{r}$
and $x^{r}+y^{r}$ as functions in $y$. It is then sufficient to observe that
$(x+y)^{r}\geqslant x^{r}+y^{r}$ for $y=0$ and that
$\nicefrac{{d}}{{dy}}(x+y)^{r}\geqslant\nicefrac{{d}}{{dy}}(x^{r}+y^{r})$ (the
derivatives with regard to $y$) for all $y\geqslant 0$. Indeed, we have
$\nicefrac{{d}}{{dy}}(x+y)^{r}=r(x+y)^{r-1}$ and
$\nicefrac{{d}}{{dy}}(x^{r}+y^{r})=ry^{r-1}$. Because of $r\geqslant 1$ and
$x\geqslant 0$, we can thus deduce that
$\nicefrac{{d}}{{dy}}(x+y)^{r}\geqslant\nicefrac{{d}}{{dy}}(x^{r}+y^{r})$ for
all $y\geqslant 0$.

Now we consider some $c\geqslant 1$. Combining (9) and (10), we get

$\prod_{i}(a_{i}+c)^{q_{i}}\geqslant\prod_{i}(a_{i}^{q_{i}}+c^{q_{i}})\geqslant\prod_{i}a_{i}^{q_{i}}+\prod_{i}c^{q_{i}}\geqslant
b+c\hbox to0.0pt{$\;$,\hss}$

where we have used that $i\geq 1$, and that $q_{i}\geqslant 1$ and $c\geqslant
1$ imply $\prod_{i}c^{q_{i}}\geqslant c$. By taking the logarithm on both
sides of the inequality we obtain the claim.

Finally, we obtain the following soundness result, which roughly states that
if a program $\mathsf{P}$ terminates, then the difference in potential has
paid its execution costs.222A stated, soundness assumes termination of
$\mathsf{P}$, but our analysis is not restricted to terminating programs. In
order to avoid the assumption the soundness theorem would have to be
formulated wrt. to a partial big-step or a small step semantics, cf. [27, 42].
We consider this outside the scope of this work.

######  Theorem 5.6 (Soundness Theorem).

Let $\mathsf{P}$ be well-typed and let $\sigma$ be a substitution. Suppose
${\Gamma}{\mid}{Q}\vdash{e}{\colon}\\!{\alpha}{\mid}{Q^{\prime}}$ and
${\sigma}\sststile{}{\ell}{{e}\Rightarrow{v}}$. Then
$\Phi({\sigma};{\Gamma}{\mid}{Q})-\Phi({v}{\mid}{Q^{\prime}})\geqslant\ell$.
Further, if
${\Gamma}{\mid}{Q}\vdash^{\text{cf}}{e}{\colon}\\!{\alpha}{\mid}{Q^{\prime}}$,
then $\Phi({\sigma};{\Gamma}{\mid}{Q})\geqslant\Phi({v}{\mid}{Q^{\prime}})$.

######  Proof 5.7.

The proof embodies the high-level description given in Section 2. It proceeds
by main induction on $\Pi\colon{\sigma}\sststile{}{\ell}{{e}\Rightarrow{v}}$
and by side induction on
$\Xi\colon{\Gamma}{\mid}{Q}\vdash{e}{\colon}\\!{\alpha}{\mid}{Q^{\prime}}$,
where the latter is employed in the context of the weakening rules. We
consider only a few cases of interest. For example, for a case not covered:
the variable rule $(\mathsf{{var}})$ types a variable of unspecified type
$\alpha$. As no actual costs are required the annotation is unchanged and the
theorem follows trivially.

_Case_. $\Pi$ derives
${{{\sigma}\sststile{}{0}{{\textup{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\color[rgb]{0.10546875,0.00390625,0.375}\small{\@listingGroup{ltx_lst_keywords2}{\color[rgb]{0,0.578125,0.015625}\small
leaf}}}}}}}\Rightarrow{\textup{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\color[rgb]{0.10546875,0.00390625,0.375}\small{\@listingGroup{ltx_lst_keywords2}{\color[rgb]{0,0.578125,0.015625}\small
leaf}}}}}}}}$. Then $\Xi$ consists of a single application of the rule
$(\mathsf{{leaf}})$:

${{\varnothing}{\mid}{Q+K}\vdash{\textup{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\color[rgb]{0.10546875,0.00390625,0.375}\small{\@listingGroup{ltx_lst_keywords2}{\color[rgb]{0,0.578125,0.015625}\small
leaf}}}}}}}{\colon}\\!{\mathsf{T}}{\mid}{Q^{\prime}}\lx@proof@logical@and\forall
c\geqslant 2\ q_{(c)}=\sum_{a+b=c}q^{\prime}_{(a,b)}K=q^{\prime}_{\ast}\hbox
to0.0pt{$\;$.\hss}$

By assumption $Q=[(q_{(c)})_{c\in{\mathbb{N}}}]$ is an annotation for the
empty sequence of trees. On the other hand
$Q^{\prime}=[(q^{\prime}_{(a,b)})_{a,b\in{\mathbb{N}}}]$ is an annotation of
length $1$. Note that
${\operatorname{\mathsf{rk}}(\textup{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\color[rgb]{0.10546875,0.00390625,0.375}\small{\@listingGroup{ltx_lst_keywords2}{\color[rgb]{0,0.578125,0.015625}\small
leaf}}}}}})=1$ by definition. Thus, we obtain:

$\displaystyle\Phi({\epsilon}{\mid}{Q+K})$
$\displaystyle=K+\sum_{c}q_{(c)}\cdot\log(c)$ $\displaystyle=K+\sum_{c\geq
2}q_{(c)}\cdot\log(c)$ $\displaystyle=q^{\prime}_{\ast}+\sum_{a+b\geq
2}q^{\prime}_{(a,b)}\cdot\log(a+b)$
$\displaystyle=q^{\prime}_{\ast}+\sum_{a,b}q^{\prime}_{(a,b)}\cdot\log(a+b)$
${{{\displaystyle=q^{\prime}_{\ast}\operatorname{\mathsf{rk}}(\textup{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\color[rgb]{0.10546875,0.00390625,0.375}\small{\@listingGroup{ltx_lst_keywords2}{\color[rgb]{0,0.578125,0.015625}\small
leaf}}}}}})+\sum_{a,b}q^{\prime}_{(a,b)}p_{(a,b)}(\textup{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\color[rgb]{0.10546875,0.00390625,0.375}\small{\@listingGroup{ltx_lst_keywords2}{\color[rgb]{0,0.578125,0.015625}\small
leaf}}}}}})=\Phi({\textup{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\color[rgb]{0.10546875,0.00390625,0.375}\small{\@listingGroup{ltx_lst_keywords2}{\color[rgb]{0,0.578125,0.015625}\small
leaf}}}}}}}{\mid}{Q^{\prime}})\hbox to0.0pt{$\;$.\hss}$

_Case_. Suppose $\Pi$ has the following from:

${\sigma}\sststile{}{0}{{\text{\text{\small\color[rgb]{0,0.578125,0.015625}{(}}{$x_{1}$}\text{\small\color[rgb]{0.10546875,0.00390625,0.375}{,}}{$x_{2}$}\text{\small\color[rgb]{0.10546875,0.00390625,0.375}{,}}{$x_{3}$}\text{\small\color[rgb]{0,0.578125,0.015625}{)}}}}\Rightarrow{\text{\text{\small\color[rgb]{0,0.578125,0.015625}{(}}{$t$}\text{\small\color[rgb]{0.10546875,0.00390625,0.375}{,}}{$b$}\text{\small\color[rgb]{0.10546875,0.00390625,0.375}{,}}{$u$}\text{\small\color[rgb]{0,0.578125,0.015625}{)}}}}}\lx@proof@logical@and
x_{1}\sigma=tx_{2}\sigma=bx_{3}\sigma=u\hbox to0.0pt{$\;$.\hss}$

Wlog. $\Xi$ consists of a single application of the rule $(\mathsf{{node}})$:

${{x_{1}}{\colon}\\!{\mathsf{T}},{x_{2}}{\colon}\\!{\mathsf{B}},{x_{3}}{\colon}\\!{\mathsf{T}}}{\mid}{Q}\vdash{\text{\small\color[rgb]{0,0.578125,0.015625}{(}}{x_{1}}\text{\small\color[rgb]{0.10546875,0.00390625,0.375}{,}}{x_{2}}\text{\small\color[rgb]{0.10546875,0.00390625,0.375}{,}}{x_{3}}\text{\small\color[rgb]{0,0.578125,0.015625}{)}}}{\colon}\\!{\mathsf{T}}{\mid}{Q^{\prime}}\lx@proof@logical@and
q_{1}=q_{2}=q^{\prime}_{\ast}q_{(1,0,0)}=q_{(0,1,0)}=q^{\prime}_{\ast}q_{(a,a,b)}=q^{\prime}_{(a,b)}$

By definition, we have
$Q=[q_{1},q_{2}]\cup[(q_{(a_{1},a_{2},b)})_{a_{i},b\in{\mathbb{N}}}]$ and
$Q^{\prime}=[q^{\prime}_{\ast}]\cup[(q^{\prime}_{(a^{\prime},b^{\prime})})_{a^{\prime},b^{\prime}\in{\mathbb{N}}}]$.
We set
$\Gamma\mathrel{:=}{x_{1}}{\colon}\\!{\mathsf{T}},{x_{2}}{\colon}\\!{\mathsf{B}},{x_{3}}{\colon}\\!{\mathsf{T}}$
as well as $x_{1}\sigma=u$, $x_{2}\sigma=b$, and $x_{3}\sigma=v$. Thus
$\Phi({\sigma};{\Gamma}{\mid}{Q})=\Phi({u,v}{\mid}{Q})$ and we obtain:

$\displaystyle\Phi({u,v}{\mid}{Q})$
$\displaystyle=q_{1}\cdot\operatorname{\mathsf{rk}}(u)+q_{2}\cdot\operatorname{\mathsf{rk}}(v)+\sum_{a_{1},a_{2},b}q_{(a_{1},a_{2},b)}\cdot\log(a_{1}\cdot\lvert{u}\rvert+a_{2}\cdot\lvert{v}\rvert+b)$
$\displaystyle\geqslant
q^{\prime}_{\ast}\cdot\operatorname{\mathsf{rk}}(u)+q^{\prime}_{\ast}\cdot\operatorname{\mathsf{rk}}(v)+q_{(1,0,0)}\cdot\log(\lvert{u}\rvert)+q_{(0,1,0)}\cdot\log(\lvert{v}\rvert)+{}$
$\displaystyle\quad{}+\sum_{a,b}q_{(a,a,b)}\cdot\log(a\cdot\lvert{u}\rvert+a\cdot\lvert{v}\rvert+b)$
$\displaystyle=q^{\prime}_{\ast}\cdot(\operatorname{\mathsf{rk}}(u)+\operatorname{\mathsf{rk}}(v)+\log(\lvert{u}\rvert)+\log(\lvert{v}\rvert))+{}$
$\displaystyle\quad{}+\sum_{a,b}q^{\prime}_{(a,b)}\cdot\log(a\cdot(\lvert{u}\rvert+\lvert{v}\rvert)+b)$
${{{{{{{{{{{{\displaystyle=q^{\prime}_{\ast}\cdot\operatorname{\mathsf{rk}}(\textup{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\color[rgb]{0.10546875,0.00390625,0.375}\small(}}}{$u$}\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\color[rgb]{0.10546875,0.00390625,0.375}\small{\@listingGroup{ltx_lst_identifier}{,}}}}}
{$b$}\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\color[rgb]{0.10546875,0.00390625,0.375}\small{\@listingGroup{ltx_lst_identifier}{,}}}}}
{$v$}\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\color[rgb]{0.10546875,0.00390625,0.375}\small)}}}})+\sum_{a,b}q^{\prime}_{(a,b)}\cdot
p_{(a,b)}(\textup{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\color[rgb]{0.10546875,0.00390625,0.375}\small(}}}{$u$}\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\color[rgb]{0.10546875,0.00390625,0.375}\small{\@listingGroup{ltx_lst_identifier}{,}}}}}
{$b$}\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\color[rgb]{0.10546875,0.00390625,0.375}\small{\@listingGroup{ltx_lst_identifier}{,}}}}}
{$v$}\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\color[rgb]{0.10546875,0.00390625,0.375}\small)}}}})=\Phi({\textup{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\color[rgb]{0.10546875,0.00390625,0.375}\small(}}}{$u$}\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\color[rgb]{0.10546875,0.00390625,0.375}\small{\@listingGroup{ltx_lst_identifier}{,}}}}}
{$b$}\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\color[rgb]{0.10546875,0.00390625,0.375}\small{\@listingGroup{ltx_lst_identifier}{,}}}}}
{$v$}\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\color[rgb]{0.10546875,0.00390625,0.375}\small)}}}}}{\mid}{Q^{\prime}})\hbox
to0.0pt{$\;$.\hss}$

_Case_. Suppose ${\sigma}\sststile{}{\ell}{{e}\Rightarrow{v}}$ and let the
last rule in $\Xi$ be of the following form:

${\Gamma}{\mid}{Q+K}\vdash{e}{\colon}\\!{\alpha}{\mid}{Q^{\prime}+K}{\Gamma}{\mid}{Q}\vdash{e}{\colon}\\!{\alpha}{\mid}{Q^{\prime}}\hbox
to0.0pt{$\;$,\hss}$

where $K\geqslant 0$. By SIH, we have that
$\Phi({\sigma};{\Gamma}{\mid}{Q})-\Phi({v}{\mid}{Q^{\prime}})\geqslant\ell$,
from which we immediately obtain:

$\Phi({\sigma};{\Gamma}{\mid}{Q})+K-\Phi({v}{\mid}{Q^{\prime}})-K=\Phi({\sigma};{\Gamma}{\mid}{Q})-\Phi({v}{\mid}{Q^{\prime}})\geqslant\ell\hbox
to0.0pt{$\;$.\hss}$

_Case_. Consider the first $(\mathsf{{match}})$ rule, where $\Pi$ ends as
follows:

${{\sigma}\sststile{}{\ell}{{\text{\small\color[rgb]{0.87890625,0,0.2890625}{{match
}}}x\text{\small\color[rgb]{0.87890625,0,0.2890625}{{
with}}}\text{\small\color[rgb]{0.10546875,0.00390625,0.375}{{|
}}}\text{\small\color[rgb]{0,0.578125,0.015625}{{leaf}}}\text{\small\color[rgb]{0.10546875,0.00390625,0.375}{{
-> }}}e_{1}\\\ \text{\small\color[rgb]{0.10546875,0.00390625,0.375}{{|
}}}\text{\text{\small\color[rgb]{0,0.578125,0.015625}{(}}{$x_{0}$}\text{\small\color[rgb]{0.10546875,0.00390625,0.375}{,}}{$x_{1}$}\text{\small\color[rgb]{0.10546875,0.00390625,0.375}{,}}{$x_{2}$}\text{\small\color[rgb]{0,0.578125,0.015625}{)}}}\text{\small\color[rgb]{0.10546875,0.00390625,0.375}{{
-> }}}e_{2}}\Rightarrow{v}}\lx@proof@logical@and
x\sigma=\textup{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\color[rgb]{0.10546875,0.00390625,0.375}\small{\@listingGroup{ltx_lst_keywords2}{\color[rgb]{0,0.578125,0.015625}\small
leaf}}}}}}{\sigma}\sststile{}{\ell}{{e_{1}}\Rightarrow{v}}\hbox
to0.0pt{$\;$.\hss}$

Wlog. we may assume that $\Xi$ ends with the related application of the
$(\mathsf{{match}})$ rule:

${\Gamma,{x}{\colon}\\!{\mathsf{T}}}{\mid}{Q}\vdash{\text{\small\color[rgb]{0.87890625,0,0.2890625}{{match
}}}x\text{\small\color[rgb]{0.87890625,0,0.2890625}{{ with
}}}\text{\small\color[rgb]{0.10546875,0.00390625,0.375}{{|
}}}\text{\small\color[rgb]{0,0.578125,0.015625}{{leaf}}}\text{\small\color[rgb]{0.10546875,0.00390625,0.375}{{
-> }}}e_{1}\text{\small\color[rgb]{0.10546875,0.00390625,0.375}{{|
}}}\text{\small\color[rgb]{0,0.578125,0.015625}{(}}{x_{1}}\text{\small\color[rgb]{0.10546875,0.00390625,0.375}{,}}{x_{2}}\text{\small\color[rgb]{0.10546875,0.00390625,0.375}{,}}{x_{3}}\text{\small\color[rgb]{0,0.578125,0.015625}{)}}\text{\small\color[rgb]{0.10546875,0.00390625,0.375}{{
->
}}}e_{2}}{\colon}\\!{\alpha}{\mid}{Q^{\prime}}\lx@proof<EMAIL_ADDRESS>$r_{(\vec{a},a,a,b)}=q_{(\vec{a},a,b)}$\\\
$p_{(\vec{a},c)}=\sum_{a+b=c}q_{(\vec{a},a,b)}$\\\
${\Gamma}{\mid}{P+q_{m+1}}\vdash{e_{1}}{\colon}\\!{\alpha}{\mid}{Q^{\prime}}$
\end{minipage}\begin{minipage}[b]{150.69397pt} $r_{m+1}=r_{m+2}=q_{m+1}$ \\\
$r_{(\vec{0},1,0,0)}=r_{(\vec{0},0,1,0)}=q_{m+1}$ \\\
${\Gamma,{x_{1}}{\colon}\\!{\mathsf{T}},{x_{2}}{\colon}\\!{\mathsf{B}},{x_{3}}{\colon}\\!{\mathsf{T}}}{\mid}{R}\vdash{e_{2}}{\colon}\\!{\alpha}{\mid}{Q^{\prime}}$
\end{minipage}q_{i}=r_{i}=p_{i}\hbox to0.0pt{$\;$.\hss}$

Let $Q$ be an annotation of length $m+1$ while $Q^{\prime}$ is of length $1$.
Thus annotations $P$, $R$ have lengths $m$, $m+2$, respectively. We write
$\vec{t}\mathrel{:=}t_{1},\dots,t_{n}$ for the substitution instances of the
variables in $\Gamma$. Further
${x\sigma=\textup{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\color[rgb]{0.10546875,0.00390625,0.375}\small{\@listingGroup{ltx_lst_keywords2}{\color[rgb]{0,0.578125,0.015625}\small
leaf}}}}}}$, where the latter equality follows from the assumption on $\Pi$.
By definition and the constraints given in the rule, we obtain:

$\displaystyle\Phi({\sigma};{\Gamma,{x}{\colon}\\!{\mathsf{T}}}{\mid}{Q})$
${{\displaystyle=\sum_{i}q_{i}\operatorname{\mathsf{rk}}(t_{i})+q_{m+1}\operatorname{\mathsf{rk}}(\textup{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\color[rgb]{0.10546875,0.00390625,0.375}\small{\@listingGroup{ltx_lst_keywords2}{\color[rgb]{0,0.578125,0.015625}\small
leaf}}}}}})+\sum_{\vec{a},a,c}q_{(\vec{a},a,c)}\log(\vec{a}\lvert{\vec{t}}\rvert+a\lvert{\textup{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\color[rgb]{0.10546875,0.00390625,0.375}\small{\@listingGroup{ltx_lst_keywords2}{\color[rgb]{0,0.578125,0.015625}\small
leaf}}}}}}}\rvert+c)$
${\displaystyle=\sum_{i}q_{i}\operatorname{\mathsf{rk}}(t_{i})+q_{m+1}(\operatorname{\mathsf{rk}}(\textup{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\color[rgb]{0.10546875,0.00390625,0.375}\small{\@listingGroup{ltx_lst_keywords2}{\color[rgb]{0,0.578125,0.015625}\small
leaf}}}}}}))+\sum_{\vec{a},a,c}q_{(\vec{a},a,c)}\log(\vec{a}\lvert{\vec{t}}\rvert+a+c)$
$\displaystyle=\Phi({\sigma};{\Gamma}{\mid}{P})+q_{m+1}\hbox
to0.0pt{$\;$.\hss}$

Thus
$\Phi({\sigma};{\Gamma,{x}{\colon}\\!{\mathsf{T}}}{\mid}{Q})=\Phi({\sigma};{\Gamma}{\mid}{P+q_{m+1}})$
and the theorem follows by an application of MIH.

Now, consider the second $(\mathsf{{match}})$ rule, that is, $\Pi$ ends as
follows:

${\sigma}\sststile{}{\ell}{{\text{\small\color[rgb]{0.87890625,0,0.2890625}{{match
}}}x\text{\small\color[rgb]{0.87890625,0,0.2890625}{{
with}}}\text{\small\color[rgb]{0.10546875,0.00390625,0.375}{{|
}}}\text{\small\color[rgb]{0,0.578125,0.015625}{{leaf}}}\text{\small\color[rgb]{0.10546875,0.00390625,0.375}{{
-> }}}e_{1}\\\ \text{\small\color[rgb]{0.10546875,0.00390625,0.375}{{|
}}}\text{\text{\small\color[rgb]{0,0.578125,0.015625}{(}}{$x_{0}$}\text{\small\color[rgb]{0.10546875,0.00390625,0.375}{,}}{$x_{1}$}\text{\small\color[rgb]{0.10546875,0.00390625,0.375}{,}}{$x_{2}$}\text{\small\color[rgb]{0,0.578125,0.015625}{)}}}\text{\small\color[rgb]{0.10546875,0.00390625,0.375}{{
-> }}}e_{2}}\Rightarrow{v}}\lx@proof@logical@and
x\sigma=\text{\text{\small\color[rgb]{0,0.578125,0.015625}{(}}{$t$}\text{\small\color[rgb]{0.10546875,0.00390625,0.375}{,}}{$a$}\text{\small\color[rgb]{0.10546875,0.00390625,0.375}{,}}{$u$}\text{\small\color[rgb]{0,0.578125,0.015625}{)}}}{\sigma^{\prime}}\sststile{}{\ell}{{e_{2}}\Rightarrow{v}}\hbox
to0.0pt{$\;$.\hss}$

As above, we may assume that $\Xi$ ends with the related application of the
$(\mathsf{{match}})$ rule. In this subcase, the assumption on $\Pi$ yields
${{{{t\mathrel{:=}x\sigma=\textup{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\color[rgb]{0.10546875,0.00390625,0.375}\small(}}}{$u$}\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\color[rgb]{0.10546875,0.00390625,0.375}\small{\@listingGroup{ltx_lst_identifier}{,}}}}}
{$b$}\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\color[rgb]{0.10546875,0.00390625,0.375}\small{\@listingGroup{ltx_lst_identifier}{,}}}}}
{$v$}\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\color[rgb]{0.10546875,0.00390625,0.375}\small)}}}}$.
By definition and the constraints given in the rule, we obtain:

$\displaystyle\Phi({\sigma};{\Gamma,{x}{\colon}\\!{\mathsf{T}}}{\mid}{Q})$
${{{{{{{{\displaystyle=\sum_{i}q_{i}\operatorname{\mathsf{rk}}(t_{i})+q_{m+1}\operatorname{\mathsf{rk}}(\textup{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\color[rgb]{0.10546875,0.00390625,0.375}\small(}}}{$u$}\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\color[rgb]{0.10546875,0.00390625,0.375}\small{\@listingGroup{ltx_lst_identifier}{,}}}}}
{$b$}\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\color[rgb]{0.10546875,0.00390625,0.375}\small{\@listingGroup{ltx_lst_identifier}{,}}}}}
{$v$}\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\color[rgb]{0.10546875,0.00390625,0.375}\small)}}}})+\sum_{\vec{a},a,c}q_{(\vec{a},a,c)}\log(\vec{a}\lvert{\vec{t}}\rvert+a\lvert{\textup{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\color[rgb]{0.10546875,0.00390625,0.375}\small(}}}{$u$}\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\color[rgb]{0.10546875,0.00390625,0.375}\small{\@listingGroup{ltx_lst_identifier}{,}}}}}
{$b$}\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\color[rgb]{0.10546875,0.00390625,0.375}\small{\@listingGroup{ltx_lst_identifier}{,}}}}}
{$v$}\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\color[rgb]{0.10546875,0.00390625,0.375}\small)}}}}}\rvert+c)$
$\displaystyle=\sum_{i}q_{i}\operatorname{\mathsf{rk}}(t_{i})+q_{m+1}(\operatorname{\mathsf{rk}}(u)+\log(\lvert{u}\rvert)+\log(\lvert{v}\rvert)+\operatorname{\mathsf{rk}}(v))+{}$
$\displaystyle\phantom{=}{}+\sum_{\vec{a},a,c}q_{(\vec{a},a,c)}\log(\vec{a}\lvert{\vec{t}}\rvert+a(\lvert{u}\rvert+\lvert{v}\rvert)+c)$
$\displaystyle=\Phi({\sigma};{\Gamma,{x_{1}}{\colon}\\!{\mathsf{T}},{x_{2}}{\colon}\\!{\mathsf{B}},{x_{3}}{\colon}\\!{\mathsf{T}}}{\mid}{R})\hbox
to0.0pt{$\;$,\hss}$

where we write $\vec{a}\lvert{\vec{t}}\rvert$ as shorthand to denote
componentwise multiplication.

Thus
$\Phi({\sigma};{\Gamma,{x}{\colon}\\!{\mathsf{T}}}{\mid}{Q})=\Phi({\sigma};{\Gamma,{x_{1}}{\colon}\\!{\mathsf{T}},{x_{2}}{\colon}\\!{\mathsf{B}},{x_{3}}{\colon}\\!{\mathsf{T}}}{\mid}{R})$
and the theorem follows by an application of MIH.

_Case_. Consider the $(\mathsf{{let}})$ rule, that is, $\Pi$ ends in the
following rule:

${\sigma}\sststile{}{\ell_{1}+\ell_{2}}{{\text{\small\color[rgb]{0.87890625,0,0.2890625}{{let
}}}x\text{\small\color[rgb]{0.10546875,0.00390625,0.375}{{ =
}}}e_{1}\text{\small\color[rgb]{0.87890625,0,0.2890625}{{ in
}}}e_{2}}\Rightarrow{v}}\lx@proof@logical@and{\sigma}\sststile{}{\ell_{1}}{{e_{1}}\Rightarrow{w}}{\sigma[x\mapsto
w]}\sststile{}{\ell_{2}}{{e_{2}}\Rightarrow{v}}\hbox to0.0pt{$\;$,\hss}$

where $\ell=\ell_{1}+\ell_{2}$. First, we consider the sub-case, where the
type of $e_{1}$ is an arbitrary type $\alpha$ but not of type $\mathsf{Tree}$.
Ie. we assume that $\Xi$ ends in the following application of the
$(\mathsf{{let:gen}})$-rule

${\Gamma,\Delta}{\mid}{Q}\vdash{\text{\small\color[rgb]{0.87890625,0,0.2890625}{{let
}}}x\text{\small\color[rgb]{0.10546875,0.00390625,0.375}{{ =
}}}e_{1}\text{\small\color[rgb]{0.87890625,0,0.2890625}{{ in
}}}e_{2}}{\colon}\\!{\beta}{\mid}{Q^{\prime}}\lx@proof<EMAIL_ADDRESS>$p_{i}=q_{i}$ \quad$p_{(\vec{a},c)}=q_{(\vec{a},\vec{0},c)}$\\\
${\Gamma}{\mid}{P}\vdash{e_{1}}{\colon}\\!{\alpha}{\mid}{\varnothing}$
\end{minipage}\begin{minipage}[b]{107.63855pt}
$q_{(\vec{0},\vec{b},c)}=r_{(\vec{b},c)}$ \ ($\vec{b}\not=\vec{0}$) \\\
${\Delta,{x}{\colon}\\!{\alpha}}{\mid}{R}\vdash{e_{2}}{\colon}\\!{\beta}{\mid}{Q^{\prime}}$
\end{minipage}\begin{minipage}[b]{43.05542pt} $r_{j}=q_{m+j}$\\\
$\alpha\not=\mathsf{T}$ \end{minipage}\hbox to0.0pt{$\;$.\hss}$

Recall that $\vec{a}=a_{1},\dots,a_{n}$, $\vec{b}=b_{1},\dots,b_{m}$,
$i\in\\{1,\dots,m\\}$, $j\in\\{1,\dots,k\\}$ and $a_{i},b_{j},a,b,c,d,e$ are
natural numbers. Further, the annotations $Q$, $P$, $R$ are of length $m+k$,
$m$ and $k$, respectively, while the corresponding resulting annotations
$Q^{\prime}$, $P^{\prime}$ and $R^{\prime}$, are of length $1$.

By definition and due to the constraints expressed in the typing rule, we
have:

$\displaystyle\Phi({\sigma};{\Gamma,\Delta}{\mid}{Q})$
$\displaystyle=\sum_{i}q_{i}\operatorname{\mathsf{rk}}(t_{i})+\sum_{j}q_{m+j}\operatorname{\mathsf{rk}}(u_{j})+\sum_{\vec{a},\vec{b},c}q_{(\vec{a},\vec{b},c)}\log(\vec{a}\lvert{\vec{t}}\rvert+\vec{b}\lvert{\vec{u}}\rvert+c)$
$\displaystyle\Phi({\sigma};{\Gamma}{\mid}{P})$
$\displaystyle=\sum_{i}q_{i}\operatorname{\mathsf{rk}}(t_{i})+\sum_{\vec{a},c}q_{(\vec{a},\vec{0},c)}\log(\vec{a}\lvert{\vec{t}}\rvert+c)$
$\displaystyle\Phi({w}{\mid}{\varnothing})$ $\displaystyle=0$
$\displaystyle\Phi({\sigma};{\Delta,{x}{\colon}\\!{\mathsf{Tree}}}{\mid}{R})$
$\displaystyle=\sum_{j}q_{m+j}\operatorname{\mathsf{rk}}(u_{j})+r_{k+1}\operatorname{\mathsf{rk}}(w)+\sum_{\vec{b},a,c}q_{(\vec{0},\vec{b},c)}\log(\vec{b}\lvert{\vec{u}}\rvert+c)\hbox
to0.0pt{$\;$,\hss}$

where we set $\vec{t}\mathrel{:=}t_{1},\dots,t_{m}$ and
$\vec{u}\mathrel{:=}u_{1},\dots,u_{k}$, denoting the substitution instances of
the variables in $\Gamma$, $\Delta$, respectively. Thus, we obtain

$\Phi({\sigma};{\Gamma,\Delta}{\mid}{Q})\geqslant\Phi({\sigma};{\Gamma}{\mid}{P})+\Phi({\sigma};{\Delta,{x}{\colon}\\!{\alpha}}{\mid}{R})\hbox
to0.0pt{$\;$.\hss}$

By main induction hypothesis, we conclude that
$\Phi({\sigma};{\Gamma}{\mid}{P})-\Phi({w}{\mid}{\varnothing})\geqslant\ell_{1}$
and
$\Phi({\sigma};{\Delta,{x}{\colon}\\!{\alpha}}{\mid}{R})-\Phi({v}{\mid}{Q^{\prime}})\geqslant\ell_{2}$,
from which the sub-case follows.

Second, we consider the more involved sub-case, where $e_{1}$ is of
$\mathsf{Tree}$ type. Thus, wlog. $\Xi$ ends in the following application of
the $(\mathsf{{let:T}})$-rule.

${\Gamma,\Delta}{\mid}{Q}\vdash{\text{\small\color[rgb]{0.87890625,0,0.2890625}{{let
}}}x\text{\small\color[rgb]{0.10546875,0.00390625,0.375}{{ =
}}}e_{1}\text{\small\color[rgb]{0.87890625,0,0.2890625}{{ in
}}}e_{2}}{\colon}\\!{\beta}{\mid}{Q^{\prime}}\begin{minipage}[b]{353.05444pt}
\centering$p_{i}=q_{i}$ \quad$p_{(\vec{a},c)}=q_{(\vec{a},\vec{0},c)}$
\quad$r_{j}=q_{m+j}$ \quad$r_{k+1}=p^{\prime}_{\ast}$
\quad$r_{(\vec{0},d,e)}=p^{\prime}_{(d,e)}$
\quad$\forall\vec{b}\neq\vec{0}\left(r_{(\vec{b},0,0)}=q_{(\vec{0},\vec{b},0)}\right)$
\\\ $\forall\vec{b}\neq\vec{0},\vec{a}\neq\vec{0}\lor c\neq 0\
\left(q_{(\vec{a},\vec{b},c)}=\sum_{(d,e)}p^{(\vec{b},d,e)}_{(\vec{a},c)}\right)$
\\\ $\forall\vec{b}\neq\vec{0},d\neq 0\lor e\neq 0\
\left(r_{(\vec{b},d,e)}={p^{\prime}}^{(\vec{b},d,e)}_{(d,e)}\wedge\forall(d^{\prime},e^{\prime})\neq(d,e)\
\left({p^{\prime}}^{(\vec{b},d,e)}_{(d^{\prime},e^{\prime})}=0\right)\wedge{}\right.$\\\
$\left.{}\land\sum_{(a,c)}p^{(\vec{b},d,e)}_{(\vec{a},c)}\geq{p^{\prime}}^{(\vec{b},d,e)}_{(d,e)}\land\forall\vec{a}\neq\vec{0}\lor
c\neq 0\ \left(p^{(\vec{b},d,e)}_{(\vec{a},c)}\neq
0\rightarrow{p^{\prime}}^{(\vec{b},d,e)}_{(d,e)}\leqslant
p^{(\vec{b},d,e)}_{(\vec{a},c)}\right)\right)$\\\
${\Gamma}{\mid}{P}\vdash{e_{1}}{\colon}\\!{\mathsf{T}}{\mid}{P^{\prime}}$
\hfill$\forall{\vec{b}\neq\vec{0},d\neq 0\lor e\neq 0}\
\left({\Gamma}{\mid}{P^{(\vec{b},d,e)}}\vdash^{\text{cf}}{e_{1}}{\colon}\\!{\mathsf{T}}{\mid}{{P^{\prime}}^{(\vec{b},d,e)}}\right)$
\hfill${\Delta,{x}{\colon}\\!{\mathsf{T}}}{\mid}{R}\vdash{e_{2}}{\colon}\\!{\beta}{\mid}{Q^{\prime}}$
\@add@centering\end{minipage}\hbox to0.0pt{$\;$,\hss}$

where the annotations $Q$, $P$, $R$, $Q^{\prime}$, $P^{\prime}$ and the
sequences $\vec{a}$, $\vec{b}$ are as above. Further, for each sequence
$\vec{b}\not=\vec{0}$, $P^{(\vec{b},u,v)}$ and ${P^{\prime}}^{(\vec{b},u,v)}$
denote annotations of length $m$. By definition and due to the constraints
expressed in the typing rule, we have for all $\vec{b}\not=\vec{0}$:

$\displaystyle\Phi({\sigma};{\Gamma,\Delta}{\mid}{Q})$
$\displaystyle=\sum_{i}q_{i}\operatorname{\mathsf{rk}}(t_{i})+\sum_{j}q_{j}\operatorname{\mathsf{rk}}(u_{j})+\sum_{\vec{a}\neq\vec{0}\lor\vec{b}\neq\vec{0}\lor
c\neq
0}q_{(\vec{a},\vec{b},c)}\log(\vec{a}\lvert{\vec{t}}\rvert+\vec{b}\lvert{\vec{u}}\rvert+c)$
$\displaystyle\Phi({\sigma};{\Gamma}{\mid}{P})$
$\displaystyle=\sum_{i}q_{i}\operatorname{\mathsf{rk}}(t_{i})+\sum_{\vec{a}\neq\vec{0}\lor
c\neq 0}q_{(\vec{a},\vec{0},c)}\log(\vec{a}\lvert{\vec{t}}\rvert+c)-K$
$\displaystyle\Phi({w}{\mid}{P^{\prime}})$
$\displaystyle=r_{k+1}\operatorname{\mathsf{rk}}(w)+\sum_{a\neq 0\lor c\neq
0}r_{(\vec{0},a,c)}\log(a\lvert{w}\rvert+c)$
$\displaystyle\Phi({\sigma};{\Gamma}{\mid}{P^{(\vec{b},d,e)}})$
$\displaystyle=\sum_{\vec{a}\neq\vec{0}\lor c\neq
0}p^{(\vec{b},d,e)}_{(\vec{a},c)}\log(\vec{a}\lvert{\vec{t}}\rvert+c)$
$\displaystyle\Phi({w}{\mid}{{P^{\prime}}^{(\vec{b},d,e)}})$
$\displaystyle={p^{\prime}}^{(\vec{b},d,e)}_{(d,e)}\log(d\lvert{w}\rvert+e)$
$\displaystyle\Phi({\sigma};{\Delta,{x}{\colon}\\!{\mathsf{T}}}{\mid}{R})$
$\displaystyle=\sum_{j}q_{j}\operatorname{\mathsf{rk}}(u_{j})+r_{k+1}\operatorname{\mathsf{rk}}(w)+\sum_{\vec{a}\neq\vec{0}\lor
d\neq 0\lor e\neq
0}r_{(\vec{b},d,e)}\log(\vec{b}\lvert{\vec{u}}\rvert+d\lvert{w}\rvert+e)+K\hbox
to0.0pt{$\;$,\hss}$

where we set $\vec{t}\mathrel{:=}t_{1},\dots,t_{m}$ and
$\vec{u}\mathrel{:=}u_{1},\dots,u_{k}$, denoting the substitution instances of
the variables in $\Gamma$, $\Delta$, respectively.

By main induction hypothesis, we conclude that
$\Phi({\sigma};{\Gamma}{\mid}{P})-\Phi({w}{\mid}{P^{\prime}})\geqslant\ell_{1}$.
Further, for all $\vec{b}\not=\vec{0},d\neq 0\lor e\neq 0$, we have, due to
the cost-free typing constraints
$\Phi({\sigma};{\Gamma}{\mid}{P^{(\vec{b},d,e)}})\geqslant\Phi({w}{\mid}{{P^{\prime}}^{(\vec{b},d,e)}})$.
The latter yields more succinctly (for all $\vec{b}\not=\vec{0},d\neq 0\lor
e\neq 0$) that

$\sum_{\vec{a},c}p^{(\vec{b},d,e)}_{(\vec{a},c)}\log(\vec{a}\lvert{\vec{t}}\rvert+c)\geqslant{p^{\prime}}^{(\vec{b},d,e)}_{(d,e)}\log(d\lvert{w}\rvert+e)\hbox
to0.0pt{$\;$.\hss}$ (11)

A third application of MIH yields that
$\Phi({\sigma};{\Delta,{x}{\colon}\\!{\mathsf{T}}}{\mid}{R})-\Phi({v}{\mid}{Q^{\prime}})\geqslant\ell_{2}$.
Due to the conditions
$\sum_{(a,c)}p^{(\vec{b},d,e)}_{(\vec{a},c)}\geq{p^{\prime}}^{(\vec{b},d,e)}_{(d,e)}$,
for all $(d^{\prime},e^{\prime})\neq(d,e)$,
${p^{\prime}}^{(\vec{b},d,e)}_{(d^{\prime},e^{\prime})}=0$ and for all
$\vec{a}$, $c$ $\left(p^{(\vec{b},d,e)}_{(\vec{a},c)}\neq
0\rightarrow{p^{\prime}}^{(\vec{b},d,e)}_{(d,e)}\leqslant
p^{(\vec{b},d,e)}_{(\vec{a},c)}\right)$, we can apply Lemma 5.4 to Equation
(11) and obtain

$\sum_{\vec{a}\neq\vec{0}\lor c\neq
0}p^{(\vec{b},d,e)}_{(\vec{a},c)}\log(\vec{a}\lvert{\vec{t}}\rvert+\vec{b}\lvert{\vec{u}}\rvert+c)\geqslant{p^{\prime}}^{(\vec{b},d,e)}_{(d,e)}\log(\vec{b}\lvert{\vec{u}}\rvert+d\lvert{w}\rvert+e)\hbox
to0.0pt{$\;$.\hss}$

Due to the condition
$\left(q_{(\vec{a},\vec{b},c)}=\sum_{(d,e)}p^{(\vec{b},d,e)}_{(\vec{a},c)}\right)$
for all $\vec{b}\neq\vec{0},\vec{a}\neq\vec{0}\lor c\neq 0$, we can sum those
equations for all $d\neq 0\lor e\neq 0$ and obtain (for all
$\vec{b}\not=\vec{0},d\neq 0\lor e\neq 0$) that

$\sum_{\vec{a}\neq\vec{0}\lor c\neq
0}q_{(\vec{a},\vec{b},c)}\log(\vec{a}\lvert{\vec{t}}\rvert+\vec{b}\lvert{\vec{u}}\rvert+c)\geqslant\sum_{d\neq
0\lor e\neq
0}r_{(\vec{b},d,e)}\log(\vec{b}\lvert{\vec{u}}\rvert+d\lvert{w}\rvert+e)\hbox
to0.0pt{$\;$.\hss}$

We can combine the above fact to conclude the case.

_Case._ Finally, we consider the application rules $(\mathsf{{app}})$ and
$(\mathsf{{app:cf}})$. As the cost-free variant only differs in sofar that
costs are not counted by $(\mathsf{{app:cf}})$, it suffices to consider the
rule $(\mathsf{{app}})$. Let $f(x_{1},\dots,x_{k})=e\in\mathsf{P}$ and let
$\Pi$ derives
${\sigma}\sststile{}{\ell+1}{{f(x_{1},\dots,x_{k})}\Rightarrow{v}}$. We
consider the costed typing
${{x_{1}}{\colon}\\!{\alpha_{1}},\dots,{x_{k}}{\colon}\\!{\alpha_{k}}}{\mid}{(P+K\cdot
Q)+1}\vdash^{\text{cf}}{f(x_{1},\dots,x_{k})}{\colon}\\!{\alpha}{\mid}{P^{\prime}-1+K\cdot
Q^{\prime}}$, where $K\in{\mathbb{Q}^{+}_{0}}$. Set
$\Gamma\mathrel{:=}{x_{1}}{\colon}\\!{\alpha_{1}},\dots,{x_{k}}{\colon}\\!{\alpha_{k}}$.
As $\mathsf{P}$ is well-typed, we have

${\Gamma}{\mid}{P}\vdash{e}{\colon}\\!{\beta}{\mid}{P^{\prime}}\qquad\text{and}\qquad{\Gamma}{\mid}{Q}\vdash^{\text{cf}}{e}{\colon}\\!{\beta}{\mid}{Q^{\prime}}\hbox
to0.0pt{$\;$.\hss}$

We can apply MIH wrt. the evaluation $\Pi^{\prime}$ of
${\sigma}\sststile{}{\ell}{{e}\Rightarrow{v}}$ to conclude
$\Phi({\sigma};{\Gamma}{\mid}{P})-\Phi({v}{\mid}{P^{\prime}})\geqslant\ell$ as
well as
$\Phi({\sigma};{\Gamma}{\mid}{Q})\geqslant\Phi({v}{\mid}{Q^{\prime}})$. By
monotonicity of addition and multiplication:

$\displaystyle\Phi({\sigma};{\Gamma}{\mid}{P+K\cdot Q})$
$\displaystyle=\Phi({\sigma};{\Gamma}{\mid}{P})+K\cdot\Phi({\sigma};{\Gamma}{\mid}{Q})$
$\displaystyle\geqslant(\Phi({v}{\mid}{P^{\prime}})+\ell)+K\cdot\Phi({v}{\mid}{Q^{\prime}})=\Phi({v}{\mid}{P^{\prime}+K\cdot
Q^{\prime}})+\ell\hbox to0.0pt{$\;$.\hss}$

Thus

$\displaystyle\Phi({\sigma};{\Gamma}{\mid}{P+K\cdot
Q})-\Phi({v}{\mid}{P^{\prime}-1+K\cdot Q^{\prime}})={}$
$\displaystyle{}=(\Phi({\sigma};{\Gamma}{\mid}{P+K\cdot
Q})-\Phi({v}{\mid}{P^{\prime}+K\cdot Q^{\prime}}))+1\geqslant\ell+1\hbox
to0.0pt{$\;$.\hss}$

From this, the case follows, which completes the proof of the soundness
theorem.

######  Remark 5.8.

We note that the basic resource functions can be generalised to additionally
represent linear functions in the size of the arguments. The above soundness
theorem is not affected by this generalisation.

In the next section, we exemplify the use of the proposed type-and-effect
system, cf. Figure 5, on the motivating example.

##  6 Analysis

As promised, we apply in this section the proposed type-and-effect system to
obtain an optimal analysis of the amortised costs of the zig-zig case of
_splaying_ , once the type annotations are fixed. As a preparatory step, also
to emphasise the need for the cost-free semantics, we precise the informal
account of compositional reasoning given in Section 2.

###  6.1 Let-Normal Form

We consider the expression ($al$, $a$, ($ar$, $b$, ($br$, $c$, $cr$))) =: t’,
which becomes the following expression $e$ in let-normal form

⬇

1 let t’’’ = (br, c, cr) in (

2 let t’’ = (ar, b, t’’’) in ((al, a, t’’))

3 )

The expression $e$ is typable with the following derivation, where the
expression $e^{\prime}$ abbreviate let t’’ = (ar, b, t’’’) in ((al, a, t’’)).
(We have ignored expressions of base type to increase readability.)

${{br}{\colon}\\!{\mathsf{T}},{cr}{\colon}\\!{\mathsf{T}},{ar}{\colon}\\!{\mathsf{T}},{al}{\colon}\\!{\mathsf{T}}}{\mid}{Q}\vdash{e}{\colon}\\!{\mathsf{T}}{\mid}{Q^{\prime}}\lx@proof@logical@and{{br}{\colon}\\!{\mathsf{T}},{cr}{\colon}\\!{\mathsf{T}}}{\mid}{Q_{1}}\vdash{(br,c,cr)}{\colon}\\!{\mathsf{T}}{\mid}{Q^{\prime}_{1}}{{ar}{\colon}\\!{\mathsf{T}},{al}{\colon}\\!{\mathsf{T}},{t^{\prime\prime\prime}}{\colon}\\!{\mathsf{T}}}{\mid}{Q_{2}}\vdash{e^{\prime}}{\colon}\\!{\mathsf{T}}{\mid}{Q^{\prime}}\lx@proof@logical@and{{ar}{\colon}\\!{\mathsf{T}},{t^{\prime\prime\prime}}{\colon}\\!{\mathsf{T}}}{\mid}{Q_{3}}\vdash{(ar,b,t^{\prime\prime\prime})}{\colon}\\!{\mathsf{T}}{\mid}{Q^{\prime}_{3}}\begin{minipage}{129.16626pt}
$q^{3}_{1}=q^{3}_{2}={q^{\prime}}^{3}_{\ast}$\\\
$q^{3}_{(1,0,0)}=q^{3}_{(0,1,0)}={q^{\prime}}^{3}_{\ast}$\\\
$q^{3}_{(1,1,0)}={q^{\prime}}^{3}_{(1,0)}$
\end{minipage}\qquad\eqref{eq:subtree}$

Here, we employ the derivability of the following type judgement (12) by a
single application of $(\mathsf{{node}})$, wrt. the annotation $Q_{4}$,
$Q^{\prime}$ given below.

${{al}{\colon}\\!{\mathsf{T}},{t^{\prime\prime}}{\colon}\\!{\mathsf{T}}}{\mid}{Q_{4}}\vdash{(al,a,t^{\prime\prime})}{\colon}\\!{\mathsf{T}}{\mid}{Q^{\prime}}\hbox
to0.0pt{$\;$.\hss}$ (12)

It is not difficult to check, that the above derivation indeed proves well-
typedness of the expression $e$ wrt. the below given type annotations.

$\displaystyle Q$ $\displaystyle\colon
q_{1}=q_{2}=q_{3}=q_{4}=1;{\color[rgb]{1,0,0}q_{(1,1,1,0,0)}=1};q_{(1,1,0,0,0)}=1;q_{(0,0,0,0,2)}=1\hbox
to0.0pt{$\;$,\hss}$ $\displaystyle\quad
q_{(1,0,0,0,0)}=q_{(0,1,0,0,0)}=q_{(0,0,1,0,0)}=q_{(0,0,0,1,0)}=1\hbox
to0.0pt{$\;$,\hss}$ $\displaystyle Q^{\prime}$ $\displaystyle\colon
q^{\prime}_{\ast}=1,q^{\prime}_{(0,2)}=1\hbox to0.0pt{$\;$,\hss}$
$\displaystyle Q_{1}$ $\displaystyle\colon
q^{1}_{1}=q_{1}=1;q^{1}_{2}=q_{2}=1;q^{1}_{(0,0,2)}=q_{(0,0,0,0,2)}=1\hbox
to0.0pt{$\;$,\hss}$ $\displaystyle\quad
q^{1}_{(1,1,0)}=q_{(1,1,0,0,0)};q^{1}_{(1,0,0)}=q_{(1,0,0,0,0)}=1;q^{1}_{(0,1,0)}=q_{(0,1,0,0,0)}=1\hbox
to0.0pt{$\;$,\hss}$ $\displaystyle Q^{\prime}_{1}$
$\displaystyle\colon{q^{\prime}}^{1}_{\ast}=1;{q^{\prime}}^{1}_{(1,0)}=1;{q^{\prime}}^{1}_{(0,2)}=1\hbox
to0.0pt{$\;$,\hss}$ $\displaystyle P^{(1,0,1,0)}$
$\displaystyle\colon{\color[rgb]{1,0,0}{p}^{(1,0,1,0)}_{(1,1,0)}=q_{(1,1,1,0,0)}=1}\hbox
to0.0pt{$\;$,\hss}$ $\displaystyle{P^{\prime}}^{(1,0,1,0)}$
$\displaystyle\colon{\color[rgb]{1,0,0}{p^{\prime}}^{(1,0,1,0)}_{(1,0)}=1}\hbox
to0.0pt{$\;$,\hss}$ $\displaystyle Q_{2}$ $\displaystyle\colon
q^{2}_{1}=q_{3}=1;q^{2}_{2}=q_{4}=1;q^{2}_{3}={q^{\prime}}^{1}_{\ast}=1;\hbox
to0.0pt{$\;$,\hss}$
$\displaystyle\quad{q}^{2}_{(1,0,0,0)}=q_{(0,0,1,0,0)}=1;{q}^{2}_{(0,1,0,0)}=q_{(0,0,0,1,0)}=1;\hbox
to0.0pt{$\;$,\hss}$
$\displaystyle\quad{q}^{2}_{(0,0,1,0)}={q^{\prime}}^{1}_{(1,0)}=1;{q}^{2}_{(0,0,0,2)}={q^{\prime}}^{1}_{(0,2)}=1;{\color[rgb]{1,0,0}q^{2}_{(1,0,1,0)}={p^{\prime}}^{(1,0,1,0)}_{(1,0)}=1}\hbox
to0.0pt{$\;$,\hss}$ $\displaystyle Q_{3}$ $\displaystyle\colon
q^{3}_{1}=q^{2}_{1}=1;q^{3}_{2}=q^{2}_{3}=1;q^{3}_{(0,0,2)}={q}^{2}_{(0,0,0,2)}=1$
$\displaystyle\quad
q^{3}_{(1,0,0)}={q^{2}}_{(1,0,0,0)}=1;q^{3}_{(0,1,0)}={q^{2}}_{(0,0,1,0)}=1;q^{3}_{(1,1,0)}={q^{2}}_{(1,0,1,0)}=1\hbox
to0.0pt{$\;$,\hss}$ $\displaystyle Q_{3}^{\prime}$
$\displaystyle\colon{q^{\prime}}^{3}_{\ast}=1,{q^{\prime}}^{3}_{(1,0)}=1,{q^{\prime}}^{3}_{(0,2)}=1$
$\displaystyle Q_{4}$ $\displaystyle\colon
q^{4}_{1}=q^{2}_{2}=1;q^{4}_{(0,0,2)}={q^{\prime}}^{3}_{(0,2)}=1;q^{4}_{(1,0,0)}={q}^{2}_{(0,1,0,0)}=1;q^{4}_{(0,1,0)}={q^{\prime}}^{3}_{(1,0)}=1$

In the inference marked with $(\ast)$, we employ the (almost trivial)
correctness of the following _cost-free_ typing derivation for
${{br}{\colon}\\!{\mathsf{T}},{cr}{\colon}\\!{\mathsf{T}}}{\mid}{P^{(1,0,1,0)}}\vdash^{\text{cf}}{(br,c,cr)}{\colon}\\!{\mathsf{T}}{\mid}{{P^{\prime}}^{(1,0,1,0)}}$.
(For instantiation of the rule $(\mathsf{{let:T}})$ note $\vec{b}=(1,0)$.)

${{br}{\colon}\\!{\mathsf{T}},{cr}{\colon}\\!{\mathsf{T}}}{\mid}{P^{(1,0,1,0)}}\vdash^{\text{cf}}{(br,c,cr)}{\colon}\\!{\mathsf{T}}{\mid}{{P^{\prime}}^{(1,0,1,0)}}p^{(1,0,1,0)}_{(1,1,0)}={p^{\prime}}^{(1,0,1,0)}_{(1,0)}\hbox
to0.0pt{$\;$.\hss}$ (13)

For all $\vec{b}\not=(0)$, $\vec{b}\not=(1)$ and arbitrary $d$, $e$, we set
$P^{(\vec{b},d,e)}={P^{\prime}}^{(\vec{b},d,e)}\mathrel{:=}\varnothing$. Our
prototype fully automatically checks correctness of the above given
annotations.

We emphasise that the involved $(\mathsf{{let}})$-rule, employed in step
$(\ast)$ cannot be avoided. In particular, the additional cost-free derivation
(13) is essential. Observe the annotation marked in red in the calculation
above. Eventually these amount to a shared potential employed in step
($\ast$). The cost-free semantics allows us to exploit this shared potential,
which otherwise would have to be discarded.

To wit, assume momentarily the rule $(\mathsf{{let}})$ would not make use of
cost-free reasoning, similar to the simplified $(\mathsf{{let}})$-rule, that
we have used in the explanations on page 5. Then the shared potential
represented by the coefficient $q_{(1,1,1,0,0)}\in Q$ is discarded by the
rule. However, this potential is then missing, if we attempt to type the
judgement

${{ar}{\colon}\\!{\mathsf{T}},{al}{\colon}\\!{\mathsf{T}},{t^{\prime\prime\prime}}{\colon}\\!{\mathsf{T}}}{\mid}{R}\vdash{e^{\prime}}{\colon}\\!{\mathsf{T}}{\mid}{Q^{\prime}}\hbox
to0.0pt{$\;$,\hss}$

where $R$ is defined as $Q_{2}$, except that $r_{(1,0,1,0)}=0$. Thus, this
attempt fails. (Note that the corresponding coefficient of $Q_{2}$, marked in
red, is non-zero.)

######  Remark 6.1.

To some extent this is in contrast to the use of cost-free semantics in the
literature [22, 24, 34, 26, 42]. While cost-free semantics appear as an add-on
in these works, essential only if we want to capture non tail-recursive
programs, cost-free semantics is essential in our context—it is already
required for the representation of simple values.

###  6.2 Splay Trees

${{{{{{{{{{{{{{{{{{{{{{{{{{a}{\colon}\\!{\mathsf{B}},{t}{\colon}\\!{\mathsf{T}}}{\mid}{Q}\vdash{\textup{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\color[rgb]{0.10546875,0.00390625,0.375}\small{\@listingGroup{ltx_lst_keyword}{\color[rgb]{0.87890625,0,0.2890625}\small
match}}}}}}\ t\
\textup{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\color[rgb]{0.10546875,0.00390625,0.375}\small{\@listingGroup{ltx_lst_keyword}{\color[rgb]{0.87890625,0,0.2890625}\small
with}}}}}}\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\color[rgb]{0.10546875,0.00390625,0.375}\small\textbar}}}}\textup{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\color[rgb]{0.10546875,0.00390625,0.375}\small{\@listingGroup{ltx_lst_keywords2}{\color[rgb]{0,0.578125,0.015625}\small
leaf}}}}}}\
\mathrel{\textup{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\color[rgb]{0.10546875,0.00390625,0.375}\small-\textgreater}}}}}\
\textup{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\color[rgb]{0.10546875,0.00390625,0.375}\small{\@listingGroup{ltx_lst_keywords2}{\color[rgb]{0,0.578125,0.015625}\small
leaf}}}}}}\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\color[rgb]{0.10546875,0.00390625,0.375}\small\textbar}}}}\text{\small\color[rgb]{0,0.578125,0.015625}{(}}{cl}\text{\small\color[rgb]{0.10546875,0.00390625,0.375}{,}}{c}\text{\small\color[rgb]{0.10546875,0.00390625,0.375}{,}}{cr}\text{\small\color[rgb]{0,0.578125,0.015625}{)}}\
\mathrel{\textup{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\color[rgb]{0.10546875,0.00390625,0.375}\small-\textgreater}}}}}\