Persistent Amortised Analysis, Operationally

The (worst-case) time complexity of our language is given by a big-step operational semantics. We write $\mathrm{\Gamma }:e{\Downarrow }_k\mathrm{\Delta }:w$ to mean “under heap $\mathrm{\Gamma }$, the expression $e$ evaluates to value $w$ with updated heap $\mathrm{\Delta }$ in $k$ steps”. A heap is defined as a mapping from pointers to heap values:

Our big-step semantics is specified using the inference rules below. Each rule specifies that if the premises above the line hold, then the conclusion below the line also holds. We write $[v/x]$ for the capture-avoiding substitution that replaces all free occurrences of $x$ with $v$. We may assume that each operation is performed on values of the correct shape: for example, a case-split is performed on either an $inlv$ or an $inrv$ value. If the shape of the value is incorrect, no rule applies and we say that the evaluation is stuck. We only write $\mathrm{\Gamma }:e{\Downarrow }_k\mathrm{\Delta }:w$ if the evaluation is not stuck.

In rules that allocate values into the heap, we require that the allocated pointer $a$ is fresh. To simplify matters, it is convenient to assume that this choice is deterministic. When we compare two evaluations of the same expression, we may assume that they allocate their heap values into the same memory cells. In addition, we assume that the chosen pointer is globally fresh. For example, when we have two evaluations of expressions $e_1$ and $e_2$ from the same heap, we may combine them into an evaluation of $letx=e_{1}in{e}_2$ by assuming that they never choose the same pointer for allocation. It is possible (but laborious) to lift both assumptions through the explicit maintenance of substitutions of pointers.

This operational semantics closely approximates the cost of executing a functional program in practice. Like Danielsson [4], we only count the steps that correspond to lambda application and function calls. It can be shown that, for a fixed expression, call-by-value semantics can be simulated by a random access machine using only constant overhead [3].

To model thunks, we extend our syntax and semantics. We add two new heap values: lazy thunks and memoised thunks. A lazy thunk holds a value and is annotated by the top-level function $F$ that should be applied to update the thunk. A memoised thunk holds the value that was computed by the update. We can force a thunk to obtain its memoised value, updating it if necessary. In practice, the function $F$ is not stored in the thunk itself, but inferred from its type during the force operation [22].

To extend our semantics with thunks, we use a variant of Launchbury’s natural semantics [17], which makes thunks first-order [22]. We allocate a thunk in a fresh memory cell using the (lazy) and (memo) rules. If a thunk is memoised, we retrieve its value using the (recall) rule at no cost. If a thunk is lazy, we have to force it using the (force) rule, where we remove it from the heap, run the computation and then store the memoised value back into the heap. Forcing itself is free, but involves a function call, which costs one step.

The banker’s method makes it possible to amortise expensive operations against cheap ones. Cheap operations may spend additional time to save credits on the heap. Credits may be spent during an expensive operation to reduce its cost. We model credits by a natural number $n$ that is attached to a heap allocation:

We add rules for saving credits on these cells and spending them later:

In the (save) rule, we take $m$ steps to add $m$ credits to a heap allocation. Conversely, in the (spend) rule, we may spend $m$ credits from the heap to reduce the number of steps we have to take. We do not allow negative credits: if we try to spend more credits than we have, this rule does not apply and evaluation is stuck.

To show that the (save) and (spend) rules are correct, we need to compare them to the rules defined earlier. The big-step rules defined in Section 2 give the worst-case number of steps that are needed to evaluate an expression under a given heap. We will call it the real semantics and denote it by ${\Downarrow }_k^{\mathrm{R}}$. The banker’s semantics extends the real semantics with the (save) and (spend) rules, and we denote it by ${\Downarrow }_k^{\mathrm{B}}$.

We show that the (save) and (spend) rules are correct by comparing the banker’s semantics to the real semantics. But this is tricky to do directly, since they use different syntaxes for heaps. We relate the heaps through an erasure function $⌜\cdot ⌝:{\mathrm{Heap}}^{\mathrm{B}}\to {\mathrm{Heap}}^{\mathrm{R}}$ that embeds the banker’s heaps with credits into the real heaps without credits.

We call a cost model sound if it yields the same result as the real semantics and allows us to prove an upper bound on the number of steps taken by the real semantics.

The banker’s method yields a sound cost model. The potential function ${\mathrm{\Phi }}^{\mathrm{B}}$ counts the total number of credits in the heap and the ${⌜\cdot ⌝}^{\mathrm{B}}$ function removes the credit annotations:

Additionally, we need to interpret the “$\mathrm{save}ma$” and “$\mathrm{spend}m\mathrm{from}a\mathrm{on}e$” expressions in the real semantics. We treat them as no-ops, where “$\mathrm{save}ma$” returns $a$ at no cost and “$\mathrm{spend}m\mathrm{from}a\mathrm{on}e$” evaluates $e$ without adjusting its cost.

To analyse the binary counter using the banker’s method, we define the heaps of binary counters inductively. The $\mathrm{Counter}(\mathrm{\Gamma }:v)$ predicate defines a counter as a list of zeros and ones, where we store a credit for each one-bit.

$\text{End}=inl()$  $\text{Cons}(n,a)=inr(n,a)$  $\text{Zero}=inl()$  $\text{One}=inr()$

We define the increment operation as follows. We must save a credit for each one-bit we create, but may spend a credit for each one-bit that we flip to a zero-bit.

This proof is standard for imperative languages, where each increment operation modifies the counter in place. However, this proof does not apply if the counter is used persistently. In functional languages it is possible to increment the same version of the counter multiple times:

In the program above, we create a counter with three one-bits, which gives us three credits. Then we perform two increments on the same counter. Each increment flips three one-bits to zero-bits and creates another one-bit. In total, the program spends six credits but only saves five credits. Clearly this is wrong: we cannot spend more credits than we have.

The problem is that Lemma 6 does not apply to the second increment. Given $\mathrm{Counter}(\mathrm{\Gamma }:\text{ones})$, we can perform the first increment, yielding $\mathrm{Counter}(\mathrm{\Delta }:c_1)$. But there is no guarantee that $\mathrm{Counter}(\mathrm{\Delta }:\text{ones})$ holds, which prevents us from applying the lemma again.

In fact, increments do not take $O(1)$ amortised time in a persistent setting:

To describe when an analysis holds in a persistent setting, we need to formalise how the heap may change during evaluation. Intuitively, an operational semantics is persistent if the heap only gets “better” during evaluation. First, we describe how the heap changes during evaluation using a preorder $⊑$ on heaps, which we call the accessibility relation [1].

Note that $⊑$ is fully determined by $\Downarrow$. However, it is convenient to have a succinct definition of $⊑$ that hides the concrete expression $e$. For this reason, we will define the $⊑$ relation explicitly using inference rules, and prove that our explicit rules yield accessible cost models. For the real cost model, the heap only changes by adding new allocations and forcing thunks:

Let us say that an analysis describes a sequence of operations $F_1,F_2,\mathrm{\dots },F_m$, and we ensure that each intermediate state ${\mathrm{\Gamma }}_i:v_i$ satisfies some invariant. This is enough to show soundness in a sequential setting. In a persistent setting, an operation may change the intermediate state ${\mathrm{\Gamma }}_i:v_i$ to ${\mathrm{\Delta }}_i:v_i$ for ${\mathrm{\Gamma }}_i⊑{\mathrm{\Delta }}_i$. Can we still apply the operation $F_i$ to ${\mathrm{\Delta }}_i:v_i$?

If the cost model is persistent, we can apply $F_i$ to ${\mathrm{\Delta }}_i:v_i$. It is guaranteed that this yields the same result $v_{i+1}$, does not take more steps, and that the new state ${\mathrm{\Delta }}_{i+1}:v_{i+1}$ is still accessible from ${\mathrm{\Gamma }}_{i+1}:v_{i+1}$. This allows us to inductively shift all subsequent operations to the extended heap:

In a persistent cost model, we can thus reason about persistent usage using sequential reasoning. We do not have to consider how the data structure may change in between operations, since our reasoning can be applied to any accessible state automatically. In particular, our reasoning does not have to establish monotonicity explicitly, since the evaluation itself is guaranteed to be monotonic.

The banker’s method is not persistent. To see why, consider how the heaps may change during evaluation. Because we can both save and spend credits, our accessibility relation has to account for arbitrary changes in the number of credits:

While the banker’s method allows credit annotations on all heap values, credit passing style only allows them on lazy thunks in the heap:

The (memo) and (recall) rules remain unchanged, but we need to modify the rules for lazy thunks. When we force a lazy thunk, we now take the credits stored on the thunk to pay for the computation. If the thunk does not have enough credits, the evaluation can get stuck. To ensure that enough credits are available, we add a (save) rule, which saves credits on a lazy thunk; credits saved on a memoised thunk are wasted.

We call this the credit passing semantics and write ${\Downarrow }_k^{\mathrm{C}}$ to refer to it. The potential function ${\mathrm{\Phi }}^{\mathrm{C}}$ counts the total number of credits in the heap and the ${⌜\cdot ⌝}^{\mathrm{C}}$ function removes the credit annotations:

Let us consider how the heaps evolve in the credit passing semantics. Our accessibility relation ${⊑}^{\mathrm{C}}$ extends ${⊑}^{\mathrm{R}}$ by the rules:

Unlike in the traditional banker’s method, the number of credits on a lazy thunk may only increase in this semantics. It can decrease when the thunk is forced, but at that point the thunk is replaced by a memoised value, which costs nothing to force. This ensures that the heaps can only become “better” over time:

To illustrate the credit passing technique, we add thunks to the binary counter. We consider thunks as internal nodes that correspond to a delayed increment operation. When we force a thunk, we perform one step of the increment operation:

Again, we define the heaps of binary counters inductively. This time, each zero-bit is followed by a lazy increment thunk. We assign one credit to increment thunks, but not to other heap allocations.
$\mathrm{Counter}(a\mapsto fold\text{End}:a)$ $\mathrm{Counter}(\mathrm{\Gamma }:a)⟹$ $\mathrm{Counter}(\mathrm{\Gamma },b\mapsto fold\text{Cons}(\text{One},a):b)$ $(b\notin \mathrm{dom}(\mathrm{\Gamma }))$ $\mathrm{Counter}(\mathrm{\Gamma }:a)⟹$ $\mathrm{Counter}(\mathrm{\Gamma },c\mapsto fold\text{Cons}(\text{Zero},b),b{\mapsto }_1{\mathrm{lazy}}_{\text{Incr}}a:c)$ $(b,c\notin \mathrm{dom}(\mathrm{\Gamma }))$

We change the increment operation as follows:

To increment a counter $c$, we just add an $\text{Incr}(c)$ thunk to the front, save two credits on it and force it. To show that this works, we have to prove that the thunk can be forced in two steps and the resulting counter is still well-formed.

Lorenzen [20] proposes credit inheritance to analyse Okasaki’s Banker’s Queue. Credit passing style cannot be used to analyse that data structure, as it wastes credits that are saved on a memoised thunk. To solve this issue, credit inheritance allows each thunk to designate another thunk as its heir. If a thunk has an excess of credits when forced, it may pass excess credits on to its heir instead of wasting them. Similarly, once a thunk is memoised, all credits saved on it are passed on to the heir as well.

We extend the syntax of heaps to add an heir $h$ on memoised thunks:

Similarly, we extend all existing rules to propagate the heir. Rules that do not have the judgement as a premise (like (value) or (unfold)) use the empty heir $\mathrm{\varnothing }$. The other rules propagate the heir from their premise. Since the (let) rule has two premises, we add a side-condition that the premises do not choose different heirs:

The key new rule is the (pass) rule, which allows us to designate another thunk as the heir $h$ and pass on credits from our computation to the heir. We record the heir on the reduction relation ${\Downarrow }_k^{\{h\}}$ of the current computation. This rule does not specify how many credits $m$ are passed on to the heir; this will be determined later by the (force) rule.

The (force) rule installs the heir annotation on the memoised thunk and removes it from the judgement. This time we ask that the computation in the thunk spends all the credits available on the thunk. This ensures that the number $m$ chosen in (pass) is as large as possible and no excess credits are wasted.

The (pass) rule allows us to choose the number of credits $m$ to pass on seemingly without constraint. However, the requirement that the (force) rule spends all credits implies that $m$ has to be the difference between the number of credits and the cost of the computation. It is unfortunate that the rules enforce this invariant only indirectly, but this seems unavoidable in a big-step semantics. In a small-step semantics, the (pass) rule would have direct access to the number of credits that are left on the thunk and could choose $m$ deterministically. This is done in the testing framework of Lorenzen [20].

Finally, the heir annotation allows us to provide the (inherit) rule. Unlike the (waste) rule, which discards credits placed on memoised thunks, the (inherit) rule allows us to retain these credits by passing them on to the heir.

We call this the credit-inheritance semantics and write ${\Downarrow }_k^{\mathrm{CI}}$ for ${\Downarrow }_k^{\mathrm{\varnothing }}$. The potential function ${\mathrm{\Phi }}^{\mathrm{CI}}={\mathrm{\Phi }}^{\mathrm{C}}$ counts the total number of credits in the heap and the ${⌜\cdot ⌝}^{\mathrm{CI}}$ function also removes the heir annotations (${⌜\mathrm{\Gamma },a{\mapsto }_h\mathrm{memo}v⌝}^{\mathrm{CI}}={⌜\mathrm{\Gamma }⌝}^{\mathrm{CI}},a\mapsto \mathrm{memo}v$). In the real semantics, we interpret “$\mathrm{pass}h$” as a no-op that returns $h$ without changing the heap.

The ${⊑}^{\mathrm{CI}}$ relation differs from ${⊑}^{\mathrm{C}}$ only in the new heir annotation in the [force] rule.

Okasaki defines the amortised cost of an operation informally as the unshared cost of actually performing work plus the number of debits discharged [25, page 60]. To formalise this, we track two numbers ${\Downarrow }_{k,k^{\prime }}$, where $k$ is the total number of time steps taken by the evaluation and $k^{\prime }$ is the number of debits discharged during the evaluation. All previous rules can be extended to this setting by either propagating $k^{\prime }$ from their single premise to their conclusions, returning $k^{\prime }=0$ if no premise exists, or, in the (let) rule, adding the $k^{\prime }$ numbers of the two premises.

In our heaps, we now allow debits to be placed on memoised thunks. Unlike credits, debits may be negative. We write $\mathrm{memo}w$ for a memoised thunk that has been accessed by the program and thus holds no debits. For a memoised thunk that has not yet been accessed, we write ${\mathrm{memo}}_{Fv}^{\mathrm{\Delta }}w$ to record the computation $Fv$ that computes $w$, as well as the new allocations $\mathrm{\Delta }$ created by the computation. These additional records are not necessary for reasoning, but enable us to connect this semantics to the real semantics later. Our syntax for heaps is now:

In the (lazy) rule, we now run the computation of the thunk immediately, but do not pay for it. Instead, we place the unshared cost as a debit on the resulting thunk. However, if the thunk itself pays off debits, this cost is propagated to the outside. The (force) rule allows us to access the value of a memoised thunk once the debt has been paid off. Once we access it, we remove the annotations from the thunk. Finally, the (save) rule allows us to pay off debits on a memoised thunk and if the thunk has no debits left, saved credits end up being wasted.

We call this the debit semantics and write ${\Downarrow }_{k+k^{\prime }}^{\mathrm{D}}$ for ${\Downarrow }_{k,k^{\prime }}$. To show that this semantics is sound, we need to undo the evaluation performed in the (lazy) rule. If a thunk still has an annotation, we restore it to the lazy state and remove all new allocations that were added during the computation. In the potential function, we count the number of debits that were paid off, where $k_{Fv}^{\mathrm{R}}$ is the real cost of evaluating the thunk and $n$ is its number of debits:
${\mathrm{\Phi }}^{\mathrm{D}}(\mathrm{\varnothing })=0{\mathrm{\Phi }}^{\mathrm{D}}(\mathrm{\Gamma },a{\mapsto }_n{\mathrm{memo}}_{Fv}^{\mathrm{\Delta }}w)={\mathrm{\Phi }}^{\mathrm{D}}(\mathrm{\Gamma })+k_{Fv}^{\mathrm{R}}-n{\mathrm{\Phi }}^{\mathrm{D}}(\mathrm{\Gamma },a\mapsto hv)={\mathrm{\Phi }}^{\mathrm{D}}(\mathrm{\Gamma })$ ${⌜\mathrm{\varnothing }⌝}^{\mathrm{D}}=\mathrm{\varnothing }{⌜\mathrm{\Gamma },a{\mapsto }_n{\mathrm{memo}}_{Fv}^{\mathrm{\Delta }}w⌝}^{\mathrm{D}}={⌜\mathrm{\Gamma }\setminus \mathrm{\Delta }⌝}^{\mathrm{D}},a\mapsto {\mathrm{lazy}}_{F}v{⌜\mathrm{\Gamma },a\mapsto hv⌝}^{\mathrm{D}}={⌜\mathrm{\Gamma }⌝}^{\mathrm{D}},a\mapsto hv$

Let us consider how the heaps evolve in the debit semantics. Our accessibility relation ${⊑}^{\mathrm{D}}$ on heaps is defined as follows:

Again, the number of debits on memoised thunks may only decrease in this semantics. This ensures that the heaps can only become “better” over time:

Perhaps the most surprising aspect of the debit semantics is that it has to track both $k$ and $k^{\prime }$, the unshared cost of evaluation and the number of debits discharged. This is necessary to split these costs in the (lazy) rule, where the cost $k^{\prime }$ may not be placed as a debit on the resulting thunk, but has to be propagated to the outside instead. Indeed, for a top-level computation that lives outside of any thunks, this distinction does not matter and we can specify the total cost as ${\Downarrow }_{k+k^{\prime }}^{\mathrm{D}}$ for ${\Downarrow }_{k,k^{\prime }}$.

To illustrate Okasaki’s reasoning, we analyse the binary counter using debits. Again, we define the heaps of counters inductively. We assume that all thunks are memoised, but place one debit on memoised thunks. For simplicity, we omit the annotations $Fv,\mathrm{\Delta }$ on unaccessed memoised thunks.
$\mathrm{Counter}(a\mapsto fold\text{End}:a)$ $\mathrm{Counter}(\mathrm{\Gamma }:a)⟹$ $\mathrm{Counter}(\mathrm{\Gamma },b\mapsto fold\text{Cons}(\text{One},a):b)$ $(b\notin \mathrm{dom}(\mathrm{\Gamma }))$ $\mathrm{Counter}(\mathrm{\Gamma }:a)⟹$ $\mathrm{Counter}(\mathrm{\Gamma },c\mapsto fold\text{Cons}(\text{Zero},b),b{\mapsto }_1\mathrm{memo}a:c)$ $(b,c\notin \mathrm{dom}(\mathrm{\Gamma }))$

The implementation of the persistent binary counter stays largely the same as in Section 4. The only difference is that we need to save one less credit on the increment thunks. That is, we modify the $\mathrm{incr}$ operation by replacing $\mathrm{save}\mathrm{\hspace{0.17em}2}({\mathrm{lazy}}_{\text{Incr}}c)$ with $\mathrm{save}\mathrm{\hspace{0.17em}1}({\mathrm{lazy}}_{\text{Incr}}c)$ and the lazy Incr function by replacing $\mathrm{save}\mathrm{\hspace{0.17em}1}({\mathrm{lazy}}_{\text{Incr}}a)$ with ${\mathrm{lazy}}_{\text{Incr}}a$. In our proof, we now assume that all thunks are evaluated upon creation and place the cost of that evaluation as a debit on the resulting thunk. As in the debit semantics, we account separately for the cost of paying off debits.

In Example 21, we saw that it is generally unsound to move debits between thunks. This is sound, however, if we can guarantee an evaluation order between the thunks. For example, we might know that $b$ will always be forced before $a$. Okasaki then allows $b$ to inherit the debit from $a$ [25, page 67].

An important special case where it is guaranteed that $b$ will always be forced before $a$ is if $a$ is created during the evaluation of $b$. Even though the (lazy) rule evaluates $b$ immediately, the result of that computation (and thus $a$) only becomes accessible once $b$ has been forced. This ensures that $a$ is only accessible from outside the thunk once $b$’s debit has been paid off.

To encode this in our semantics, we modify the (lazy) rule. For a freshly allocated thunk, we allow propagating some of the unshared work to the outside.

Our modification may seem counter-intuitive: rather than changing how thunks discharge debits, we change how freshly allocated thunks distribute their unshared cost. However, if $b$ is a thunk that creates $a$ during its evaluation, then this (lazy) rule allows us to place the unshared cost of $a$ on $b$. Note that this cannot be emulated by the $(save)$ rule, since $a$’s debits become part of the unshared cost $k$ of $b$, instead of the discharge cost $k^{\prime }$ of $b$.

This (lazy) rule captures Okasaki’s reasoning style for monolithic computations, which create new thunks that have to be forced in the computation itself. When reasoning about them, “all debits are usually assigned to the root” [25, page 61].

We call this the debit-inheritance semantics and write $\mathrm{\Gamma }:e{\Downarrow }_{k+k^{\prime }}^{\mathrm{DI}}\mathrm{\Delta }:w$ for $\mathrm{\Gamma }:e{\Downarrow }_{k,k^{\prime }}\mathrm{\Delta }:w$. We reuse the ${\mathrm{\Phi }}^{\mathrm{D}}$ and ${⌜\cdot ⌝}^{\mathrm{D}}$ defined for the debit semantics.

The ${⊑}^{\mathrm{DI}}$ relation differs from ${⊑}^{\mathrm{D}}$ only in that the new debit is $k_2$ instead of $k$ in the [lazy] rule.

Debit inheritance is in some sense dual to credit inheritance. While credit inheritance passes on excess credits from a thunk to one of its children, debit inheritance passes on debits from a child to its parent. Aside from this similarity, the two techniques are quite different though. For example, debit inheritance allows a parent to inherit the debits from multiple children, while credit inheritance only allows passing on credits to a single child.