Amortized Resource Analysis and Typed Potentials

Prerequisites. Direct starred prerequisites: none. No later core chapter depends on this route.

A polynomial-time characterization says how expensive every representable program can be. It does not say how many cells one invocation of pairs allocates as a function of its input length. For that problem the bound must mention the input, and the proof must follow the program.

Consider $$\begin{array}{l}\mathsf{attach}(x,l)=\mathsf{match}l\mathsf{with}[]\mapsto []\mid y::ys\mapsto (x,y)::\mathsf{attach}(x,ys),\\ \mathsf{pairs}(l)=\mathsf{match}l\mathsf{with}[]\mapsto []\mid x::xs\mapsto \\ \mathsf{append}(\mathsf{attach}(x,xs),\mathsf{pairs}(xs)).\end{array}$$ If a pair cell and a cons cell each cost one unit, then $\mathsf{attach}(x,l)$ consumes two units per element. The call $\mathsf{pairs}(x::xs)$ also copies the list returned by $\mathsf{attach}(x,xs)$. A linear annotation on the original list cannot pay this linear cost once for every suffix. The missing quantity is potential: stored credit indexed by suffix length.

The fixed RAML calculus

The chapter uses the first-order call-by-value language of Hoffmann and Hofmann [HH10]. Expressions are in let normal form: Here $b\in \{\mathsf{true},\mathsf{false}\}$, $n\in \mathbb{Z}$, and every ground operation has constant cost. Zero-order types and first-order signatures have the forms $$A::=\mathsf{unit}\mid \mathsf{bool}\mid \mathsf{int}\mid L(A)\mid (A,A),F::=(A_1,\dots ,A_k)\to A.$$ A finite context is affine. Its disjoint union ${\mathrm{\Gamma }}_1,{\mathrm{\Gamma }}_2$ is defined only when the domains are disjoint. Contraction is therefore an explicit sharing rule rather than an implicit property of contexts.

Let $H$ be a finite heap from locations to values and let $V$ be a finite stack from variables to values. The resource judgment $$V,H{⊢}_{q^{\prime }}^{q}e\Downarrow v,H^{\prime }$$ means that evaluation starts with $q\in {\mathbb{Q}}_{\ge 0}$, never makes the counter negative, returns $v,H^{\prime }$, and leaves $q^{\prime }\in {\mathbb{Q}}_{\ge 0}$. Its consumption is $q-q^{\prime }$. The relation is terminating big-step evaluation: divergence has no derivation.

The rules are parameterized by constants $K_i^{\mathsf{c}}$. The superscript names a construct and the subscript separates the before- and after-costs of a compound rule. This chapter fixes the heap-cell metric $$K^{\mathsf{pair}}=K^{\mathsf{cons}}=1,K_i^{\mathsf{c}}=0\text{for every other construct and index.}$$ Thus allocation, not evaluation steps or reclaimed space, is counted. The pair and cons rules are $$\frac{\begin{array}{c}V(x_1)=v_1\\ V(x_2)=v_2\\ l\notin \mathrm{dom}(H)\end{array}}{V,H{⊢}_q^{q+K^{\mathsf{pair}}}(x_1,x_2)\Downarrow l,H[l\mapsto (v_1,v_2)]}\mathrm{E}-\mathrm{Pair}$$ $$\frac{\begin{array}{c}V(x_h)=v_h\\ V(x_t)=v_t\\ l\notin \mathrm{dom}(H)\end{array}}{V,H{⊢}_q^{q+K^{\mathsf{cons}}}\mathsf{cons}(x_h,x_t)\Downarrow l,H[l\mapsto (v_h,v_t)]}\mathrm{E}-\mathrm{Cons}$$ The two compound rules used below are $$\frac{\begin{array}{c}V,H{⊢}_{q_2}^{q_1-K_1^{\mathsf{let}}}{e}_1\Downarrow v_1,H_1\\ V[x\mapsto v_1],H_1{⊢}_{q_3+K_3^{\mathsf{let}}}^{q_2-K_2^{\mathsf{let}}}{e}_2\Downarrow v_2,H_2\end{array}}{V,H{⊢}_{q_3}^{q_1}\mathsf{let}x=e_1\mathsf{in}{e}_2\Downarrow v_2,H_2}\mathrm{E}-\mathrm{Let}$$ and, when $\mathrm{\Sigma }(f)=(A_1,\dots ,A_k)\stackrel{q/q^{\prime }}{\to }A$, the function body is $e_f$ with formal parameters $y_1^f,\dots ,y_k^f$, and $V(x_i)=v_i$, $$\frac{[y_1^f\mapsto v_1,\dots ,y_k^f\mapsto v_k],H{⊢}_{u^{\prime }+K_2^{\mathsf{app}}}^{u-K_1^{\mathsf{app}}}{e}_f\Downarrow v,H^{\prime }}{V,H{⊢}_{u^{\prime }}^{u}f(x_1,\dots ,x_k)\Downarrow v,H^{\prime }}\mathrm{E}-\mathrm{FunApp}.$$ Every rule is invariant under adding the same $a\ge 0$ to its two counters. This counter-shift property is needed in the let and function-call cases of soundness.

Binomial potential

A list annotation is a nonempty vector $\overrightarrow{p}=(p_1,\dots ,p_d)\in {\mathbb{Q}}_{\ge 0}^d$. Define $$\phi (n,\overrightarrow{p}):=\sum _{i=1}^d{p}_i(\genfrac{}{}{0ex}{}{n}{i}),\mathsf{C}(p_1,\dots ,p_d):=(p_1+p_2,\dots ,p_{d-1}+p_d,p_d).$$ The degree $d$ is fixed while constraints are generated. The coefficients are nonnegative in this basis; their expansion in the monomial basis may have negative coefficients.

Proof of Lemma 57.1 — Head–tail identity

Proof. Pascal’s identity places its reason on the decisive equality:  ◻

The resource-annotated types are $$A::=\mathsf{unit}\mid \mathsf{bool}\mid \mathsf{int}\mid L^{\overrightarrow{p}}(A)\mid (A_1,A_2).$$ If a heap value $v$ matches $A$, its potential ${\mathrm{\Phi }}_H(v:A)$ is defined by when $H(l)=(v,l^{\prime })$. Repeated use of lemma 57.1 gives $$H(l)=[v_1,\dots ,v_n]⟹{\mathrm{\Phi }}_H(l:L^{\overrightarrow{p}}(A))=\phi (n,\overrightarrow{p})+\sum _{i=1}^n{\mathrm{\Phi }}_H(v_i:A).$$ For a context, ${\mathrm{\Phi }}_{V,H}(\mathrm{\Gamma }):=\sum _{x\in \mathrm{dom}(\mathrm{\Gamma })}{\mathrm{\Phi }}_H(V(x):\mathrm{\Gamma }(x))$.

The source also extends the same mechanism to fixed-arity trees. The empty tree has zero potential. For a $k$-ary node $l$ with payload $v$ and children $l_1,\dots ,l_k$, This clause defines annotated-tree potential; no theorem in this chapter assumes that tree size is determined solely by height.

Sharing, weakening, and the typing invariant

Write when the two types have the same shape and $A$ carries at least the potential of $B$. The list clause is The sharing relation $\mathsf{share}(A;A_1,A_2)$ splits one value’s potential between two occurrences: $$\begin{array}{c}\mathsf{share}(C;C,C)(C\in \{\mathsf{unit},\mathsf{bool},\mathsf{int}\}),\\ {\displaystyle \frac{\begin{array}{c}\mathsf{share}(A;A_1,A_2)\\ \overrightarrow{p}=\overrightarrow{q}+\overrightarrow{r}\end{array}}{\mathsf{share}(L^{\overrightarrow{p}}(A);L^{\overrightarrow{q}}(A_1),L^{\overrightarrow{r}}(A_2))}},\\ {\displaystyle \frac{\begin{array}{c}\mathsf{share}(A;A_1,A_2)\\ \mathsf{share}(B;B_1,B_2)\end{array}}{\mathsf{share}((A,B);(A_1,B_1),(A_2,B_2))}}.\end{array}$$

Proof of Lemma 57.2 — Potential splits and weakens

Proof. Proceed by induction on the displayed sharing or subtype derivation. In the list-sharing case, the payload equality comes from the induction hypothesis, the head coefficient splits because $\overrightarrow{p}=\overrightarrow{q}+\overrightarrow{r}$, and the tail coefficients split because $\mathsf{C}$ is linear. Equation (57.3) then gives the required equality. In the list-subtype case, coefficientwise order implies $\phi (n,\overrightarrow{p})\ge \phi (n,\overrightarrow{q})$; the element-type induction hypothesis gives the remaining summands in (57.4). Ground and product cases follow directly from (57.3). ◻

The annotated signature assigns $(A_1,\dots ,A_k)\stackrel{q/q^{\prime }}{\to }A$ to each function. The judgment $$\mathrm{\Sigma };\mathrm{\Gamma }{⊢}_{q^{\prime }}^{q}e:A$$ means that input potential plus $q$ pays evaluation while output potential plus $q^{\prime }$ remains. Four rules show where the invariant performs work: $$\frac{\overrightarrow{p}=(p_1,\dots ,p_d)}{\mathrm{\Sigma };x_h:A,x_t:L^{\mathsf{C}(\overrightarrow{p})}(A){⊢}_0^{p_1+K^{\mathsf{cons}}}\mathsf{cons}(x_h,x_t):L^{\overrightarrow{p}}(A)}\mathrm{T}-\mathrm{Cons}$$ $$\frac{\begin{array}{c}\mathrm{\Sigma };{\mathrm{\Gamma }}_1{⊢}_p^{q-K_1^{\mathsf{let}}}{e}_1:A\\ \mathrm{\Sigma };{\mathrm{\Gamma }}_2,x:A{⊢}_{q^{\prime }+K_3^{\mathsf{let}}}^{p-K_2^{\mathsf{let}}}{e}_2:B\end{array}}{\mathrm{\Sigma };{\mathrm{\Gamma }}_1,{\mathrm{\Gamma }}_2{⊢}_{q^{\prime }}^q\mathsf{let}x=e_1\mathsf{in}{e}_2:B}\mathrm{T}-\mathrm{Let}$$ $$\frac{\begin{array}{c}\mathrm{\Sigma };\mathrm{\Gamma },x:A_1,y:A_2{⊢}_{q^{\prime }}^{q}e:B\\ \mathsf{share}(A;A_1,A_2)\end{array}}{\mathrm{\Sigma };\mathrm{\Gamma },z:A{⊢}_{q^{\prime }}^{q}e[z/x,z/y]:B}\mathrm{T}-\mathrm{Share}$$ $$\frac{\begin{array}{c}\mathrm{\Sigma };\mathrm{\Gamma }{⊢}_{q^{\prime }}^{q}e:B\\ x\notin \mathrm{dom}(\mathrm{\Gamma })\end{array}}{\mathrm{\Sigma };\mathrm{\Gamma },x:A{⊢}_{q^{\prime }}^{q}e:B}\mathrm{T}-\mathrm{Weak}$$ The paper calls the last rule T-Augment; it is the affine weakening rule. The remaining rules used by name below are $$\frac{\mathrm{\Sigma }(f)=(A_1,\dots ,A_k)\stackrel{q/q^{\prime }}{\to }A}{\mathrm{\Sigma };x_1:A_1,\dots ,x_k:A_k{⊢}_{q^{\prime }-K_2^{\mathsf{app}}}^{q+K_1^{\mathsf{app}}}f(x_1,\dots ,x_k):A}\mathrm{T}-\mathrm{FunApp}$$ $$\frac{A\mathsf{type}}{\mathrm{\Sigma };\varnothing {⊢}_0^{K^{\mathsf{nil}}}[]:L^{\overrightarrow{0}}(A)}\mathrm{T}-\mathrm{Nil}$$ $$\frac{\begin{array}{c}\mathrm{\Sigma };\mathrm{\Gamma }{⊢}_{p^{\prime }}^{p}e:B\\ q\ge p\\ q-p\ge q^{\prime }-p^{\prime }\end{array}}{\mathrm{\Sigma };\mathrm{\Gamma }{⊢}_{q^{\prime }}^{q}e:B}\mathrm{T}-\mathrm{Relax}.$$ The list match has two premises. The nil branch receives no list potential. The cons branch binds $x_h:A$ and $x_t:L^{\mathsf{C}(\overrightarrow{p})}(A)$, and its available constant increases by $p_1$. This is the inverse use of T-Cons forced by lemma 57.1.

Resource soundness

Write $H\vDash V:\mathrm{\Gamma }$ when $V(x)$ is a value matching $\mathrm{\Gamma }(x)$ in $H$ for every $x\in \mathrm{dom}(\mathrm{\Gamma })$.

Proof of Theorem 57.3 — Hoffmann–Hofmann soundness

Proof. The proof is simultaneous induction on the typing derivation and its fixed terminating evaluation. Strengthen the induction statement by retaining the arbitrary slack $r$; without this strengthening, the intermediate resource left by a let cannot be passed to its second premise.

Constructors. For T-Cons, the input potential is ${\mathrm{\Phi }}_H(V(x_h):A)+{\mathrm{\Phi }}_H(V(x_t):L^{\mathsf{C}(\overrightarrow{p})}(A))$. After paying $K^{\mathsf{cons}}$ and $p_1$, equation (57.3) gives exactly the output potential. The pair case uses additivity of product potential and pays $K^{\mathsf{pair}}$.

List elimination. If the scrutinee is null, the nil premise has the required resource because its potential is zero. If the scrutinee is a cons location, opening (57.3) yields $p_1$, the head potential, and the shifted tail potential. These are precisely the constant and context required by the cons premise. Applying the induction hypothesis to that premise gives the claimed postcondition.

Let. The first evaluation premise and first typing premise give an intermediate counter at least ${\mathrm{\Phi }}_{H_1}(v_1:A)+p+{\mathrm{\Phi }}_{V,H}({\mathrm{\Gamma }}_2)+r$; disjointness of ${\mathrm{\Gamma }}_1$ and ${\mathrm{\Gamma }}_2$ justifies the context split. Use that amount as the precondition for the second induction hypothesis. Its conclusion is the required bound for $v,H^{\prime }$. Counter shift aligns the concrete intermediate counters without changing consumption.

Function application. Let $\mathrm{\Sigma }(f)=(A_1,\dots ,A_k)\stackrel{p/p^{\prime }}{\to }A$, and let $V(x_i)=v_i$. Program well-formedness supplies the body derivation $\mathrm{\Sigma };y_1^f:A_1,\dots ,y_k^f:A_k{⊢}_{p^{\prime }}^p{e}_f:A$. From the caller precondition and T-FunApp, remove $K_1^{\mathsf{app}}$; the remainder is at least the formal environment’s potential plus $p+r$. Apply the induction hypothesis to the premise of E-FunApp. It leaves at least output potential plus $p^{\prime }+r$; restoring $K_2^{\mathsf{app}}$ gives the caller’s residual annotation $p^{\prime }-K_2^{\mathsf{app}}$. Counter shift supplies the exact concrete counters if either inequality is strict. Thus this case uses both signature well-formedness and the sign reversal between T-FunApp and E-FunApp.

Sharing and weakening. For T-Share, lemma 57.2 replaces the single potential of $z:A$ by the sum needed for $x:A_1,y:A_2$; substitution in the stack and expression preserves the evaluation. For T-Weak, the extra nonnegative potential is added to slack because $x$ is absent from the expression.

Order rules. Input supertype uses the inequality half of lemma 57.2; output subtype uses it in the opposite position. T-Relax uses its two numerical premises $q\ge p$ and $q-p\ge q^{\prime }-p^{\prime }$ to increase the initial allowance without reducing the promised remainder.

Remaining syntax. Constants, variables, and ground operations apply their corresponding evaluation rule and its fixed $K$-constants. A conditional selects the typing premise matching $V(x)$. Product elimination opens the two summands in product potential. T-Nil uses zero output potential. These cases exhaust the expression grammar and preserve the same slack $r$. ◻

The termination premise is substantive: the theorem bounds every terminating evaluation but does not prove that one exists. Nonnegative slack is also substantive; allowing would weaken the initial premise while retaining the same postcondition. Well-formedness is structural data required to define every potential in the statement.

From a derivation to linear constraints

Assign a fresh nonnegative rational variable to every coefficient and every constant annotation in a syntax-directed derivation. T-Cons generates $q=p_1+1$ under (57.1); list matching generates the shift equations; sharing generates coefficientwise addition; subtyping and relaxation generate inequalities. Every constraint is linear because $\mathsf{C}$ and sharing are linear in the coefficients.

For $\mathsf{pairs}$, choose output annotation $(1)$ and zero constant annotations $p=p^{\prime }=0$. At a cons branch, introduce fresh input coefficients $a_1,a_2$, split the shifted tail, and impose $$a_1=0,a_2=4,\mathsf{C}(a_1,a_2)=(4,4)=(4,0)+(0,4).$$ The first component pays the three allocations per attached element plus the one unit retained in the output; the second is the recursive input. Nil, sharing, and output subtyping add only nonnegativity and coefficientwise-order constraints. Thus the source derivation admits input annotation $(0,4)$. Instantiating theorem 57.3 with $r=0$ bounds consumption by input potential minus result potential: $${\mathsf{alloc}}_{\mathsf{pairs}}(n)\le 4(\genfrac{}{}{0ex}{}{n}{2})-(\genfrac{}{}{0ex}{}{n}{2})=3(\genfrac{}{}{0ex}{}{n}{2}).$$ The RAML prototype table prints the safe monomial bound $-3n+3n^2=6(\genfrac{}{}{0ex}{}{n}{2})$. It is a distinct, looser analyzer output; it does not replace the local bound in (57.7).

The extended report prints a bound for $\mathsf{startBreadth}$, but not its source program: it says that implementation was available on the then-current RAML website. The companion therefore checks a stated reconstruction, not that unavailable implementation. A compact node $(a,b,l_1,l_2)$ represents one pair of suffix positions: $a,b$ are their heads and $l_1,l_2$ their remaining suffixes. Its two child clauses advance the left suffix, or advance both suffixes. Starting from a list of length $n$, this yields $N(n)=1+2+\cdots +n=n(n+1)/2$ visited nodes. A two-list queue stores those nodes; dequeue reverses its input list only when the output list is empty.

The explicit chapter reconstruction charges twelve named constructor sites per visited node, two per reversal, and two at initialization. For its selected input has $R(n)=n$ reversals, so The artifact emits one event carrying one of those site names; this equation counts that trace and is not an inferred RAML typing. The paper’s displayed heap bound is $$14n+14n^2=28(\genfrac{}{}{0ex}{}{n}{1})+28(\genfrac{}{}{0ex}{}{n}{2}),$$ which dominates $B(n)$ for every $n\ge 0$. This comparison is only between the report’s bound and the reconstruction’s trace; it does not establish that the two programs coincide. The evaluation-step bounds $3+7n+9n^2$ and $17+45n+45n^2$ use a different cost assignment and are not oracles for the heap-cell artifact.

RAML 1.5 is an implementation and experiment source, not the theorem proved in theorem 57.3. In particular, the declarative rules do not prove inference completeness, asymptotic tightness, or machine independence.

Chapter seminar