Incremental Computing by Differential Execution

In this paper, we explore differential execution for a statement-based imperative programming language called Imp. Imp features numeric and Boolean values that can be used in assignments, conditionals, and repeat loops, which iterate a loop body a fixed number of times

We use a big-step reduction semantics $\sigma ⊢s\Rightarrow {\sigma }^{\prime }$ that takes a program $s$ and an initial store $\sigma$ as input, and yields an output store ${\sigma }^{\prime }$. We can use this language to compute epidemiological models.

Epidemiological models are essential tools for understanding the spread of infectious diseases and informing public health interventions [15]. For example, consider a simplified model that simulates disease spread over a fixed number of $n$ days:

We can now predict how a disease spreads in $n=6$ days given an initial infectious population $I=10$ and assuming a transmissibility of $\beta =0.3$ 1(a) shows the content of the store ${\sigma }_i$ after iteration $i$ of the loop (we omit n and $\alpha$ because they are constant). This constitutes the initial, non-incremental run of the program. Note that ${\sigma }_0$ shows the initial state of the model and ${\sigma }_{\mathrm{𝑜𝑢𝑡}}={\sigma }_6$ is the final prediction.

When epidemiologists revise the initial parameters of the model, we want to update our prediction efficiently. In the following, we discuss three change scenarios. First, consider we want to change the initial infected population from $10$ to $15$. The differential store $\mathrm{\Delta }{\sigma }_0$ in 1(b) models this change. Our goal is to determine how the final prediction changes, that is, what is $\mathrm{\Delta }{\sigma }_{\mathrm{𝑜𝑢𝑡}}$. To this end, we propose the use of differential execution: Essentially, we rerun the program but only consider and compute changes. Starting from $\mathrm{\Delta }{\sigma }_0$, differential execution of the loop body computes $\mathrm{\Delta }{\sigma }_1$, showing how $S$ and $I$ are affected by the initial change of $I$. Differential execution continues to iterate the loop body until we reach $\mathrm{\Delta }{\sigma }_6=\mathrm{\Delta }{\sigma }_{\mathrm{𝑜𝑢𝑡}}$. We observe that 5 additional infections on day 0 lead to 68 additional infections on day 6.

Providing the correct differential result is easy: Reexecute the program and compute the outputs’ difference. The challenge for differential execution is to compute output changes efficiently by avoiding recomputations. For example, an increase of $I$ in $\mathrm{\Delta }{\sigma }_0$ does not affect $\beta$, which is why $\beta$ does not occur in 1(b). Indeed, as we prove in Section 5, statements that do not read changed variables can be skipped during differential execution. It is shortcuts like this that we need to discover to make differential execution efficient.

For example, consider epidemiologists now want to know what happens after $9$ instead of $6$ days. We encode this change in $\mathrm{\Delta }{\sigma }_0$ of 1(c). Note that we assume the prior change of $I$ remains in place; changes occur in sequence and have to be undone explicitly if so desired. How can differential execution handle the change of $n$ efficiently? In general, it is necessary to repeat each loop iteration to ensure input changes are propagated correctly. However, in our case, $n$ only determines the number of iterations, but it is not used inside the loop body. We prove in Section 5 that in this case we can skip all previous iterations and directly continue with the new ones. Since iterations 7, 8, and 9 have not been executed before, we have to compute the resulting stores from scratch. The final result $\mathrm{\Delta }{\sigma }_{\mathrm{𝑜𝑢𝑡}}$ is then defined by ${\sigma }_9\ominus {\sigma }_6$. In general, when the original loop count $n$ is increased by $k$, we only need to perform $k$ instead of $n+k$ iterations, which yields significant speedups when $k\ll n$.

Lastly, consider epidemiologists want to rollback $n$ from $9$ to $4$. This is a case where incremental computing has to trade-off memory and running time. If we still have ${\sigma }_4$ cached, we can compute $\mathrm{\Delta }{\sigma }_{\mathrm{𝑜𝑢𝑡}}$ by ${\sigma }_4\ominus {\sigma }_9$. Otherwise, we may have to do more recomputation. In our study of a formal semantics for differential execution, we ignore all concerns regarding caching. Later, in Section 6, we discuss how we implemented the formal semantics in an efficient interpreter and what caching strategies we considered.

A particular challenge for all kinds of incremental computing is what we call branch switching. A branch switch occurs when a change to the input data alters the control flow, causing a different branch of a conditional to be executed compared to the original run. For a simple example, consider this extreme case:

When x changes from negative to positive, the entire behavior of the program shifts: Instead of running foo, we end up running bar. This has two important consequences. First, the worst-case complexity of differential execution is at best equal to regular execution. Second, we must retain (or be able to reconstruct) the original state $\sigma$ that is valid at the beginning of a branch. This state is necessary when a branch switch occurs, as input for executing the other branch. This indicates a lower bound on the memory necessary for differential execution if we want to avoid reconstructing previously seen states.

Does this mean that all hope is lost? No, not at all. Many conditionals do not amount to a reconfiguration of the program, but have a rather limited scope. For example, an improved epidemiological model may consider emergency measures, which are active when infections exceed a threshold $T$ of 40 patients:

When we change the input variable $I$, this can now affect the control flow and lead to branch switching. However, the cost of re-executing one of the branches is limited in this case, and only results in different subsequent changes to $\beta$. One interesting issue that persists is that branch switching requires diffing between the original and the new state to determine the subsequent changes. In Section 5, we present an optimization that avoids this cost when branches execute similar code.

Changes must support two fundamental operations: diffing to produce changes from values ($\mathrm{𝑛𝑒𝑤}\ominus \mathrm{𝑜𝑙𝑑}$), and patching to apply changes to values ($\mathrm{𝑏𝑎𝑠𝑒}\oplus \mathrm{𝑐ℎ𝑎𝑛𝑔𝑒})$. Patching and diffing should act as inverses: $v_1\oplus (v_2\ominus v_1)=v_2$ and $(v\oplus \mathrm{\Delta }v)\ominus v=\mathrm{\Delta }v$. These laws are elemental for differential execution as they justify optimizations that avoid redundant work.

However, handling changes correctly is subtle and it is easy to break the second property. For example, consider $v=2$ and $\mathrm{\Delta }v=\text{dec }5$ for the naturals with $2\oplus \text{dec }5=0$. Then,

The problem is that we tried to patch $v=2$ with $\mathrm{\Delta }v=\text{dec }5$, which is invalid because $2-5$ does not yield a natural number, and defaulting to $0$ contradicts our inversion properties. The same problem occurs for other data types, such as strings, sets, and lists. For example, we get . Again, we tried to apply a patch that has an undefined behavior, and defaulting to the empty string breaks our inversion laws. Therefore, we follow the incremental lambda calculus [9] and restrict patching to valid changes. But rather than using Coq’s dependent typing, we rely on a dedicated typing judgment $v⊢\mathrm{\Delta }v$. Patching and diffing then must satisfy the following properties:

Patching is only defined when $v⊢\mathrm{\Delta }v$ and yields a value of the same type as $v$. Diffing is defined for any $v_1$ and $v_2$ of the same type, and it yields a valid change that can be applied to $v_1$. When defining differential execution, it is our responsibility to define changes $\mathrm{\Delta }v$, validity $v⊢\mathrm{\Delta }v$, patching $\oplus$, and diffing $\ominus$ such that these typing rules hold.

On top of these typing rules for patching and diffing, we can now stipulate the inversion properties we require.

Note how the latter property uses equivalence $\equiv$ on changes rather than equality. This is due to the fact that changes often have non-unique representations and diffing might choose any equivalent representation. For example, $\text{inc }0$ and $\text{dec }0$ are equivalent but not equal. In general, $\mathrm{\Delta }{v}_1\equiv \mathrm{\Delta }{v}_2$ iff for all $v$, $v⊢\mathrm{\Delta }{v}_1\leftrightarrow v⊢\mathrm{\Delta }{v}_2$ and $v\oplus \mathrm{\Delta }{v}_1=v\oplus \mathrm{\Delta }{v}_2$.

The above properties justify our use of noc, representing no change. Specifically, for any $v$, we have $v\oplus (v\ominus v)=v$ and therefore $\text{noc}\equiv v\ominus v$. In practice, it is usually easy to decide if a given $\mathrm{\Delta }v$ is equivalent to noc.

Our imperative language Imp uses unsigned integers and Boolean values. We define changes for each type:

Numeric changes consist of no change (${\text{noc}}_{\mathbb{N}}$), increasing ($\text{inc }k$), and decreasing ($\text{dec }k$), where $k$ is any natural number. Boolean changes consist of no change (${\text{noc}}_{𝔹}$) and negation (neg). Changes are only valid for an appropriately typed value, and $\text{dec }k$ is only valid for numbers larger or equal to $k$:

Whenever $v⊢\mathrm{\Delta }v$, we can patch $v$ while retaining its type as required by T-Patch. Moreover, differencing ensures $v_1⊢v_2\ominus v_1$ as required by V-Diff.

We have modeled these changes and their operations in Rocq, where we proved they satisfy the respective typing rules as well as patch-diff and diff-patch inversion.

We have established how patching and diffing operate on individual values, but our imperative programs range over variables that map to values. Therefore, we need to lift changes and their operations from single values to entire stores $\sigma :x\to v$ that map variables to values. To this end, we define differential stores $\mathrm{\Delta }\sigma :x\to \mathrm{\Delta }v$, which map variables to value changes. Differential stores must satisfy the same properties as differential values: well-typed patching and diffing according to T-Patch and V-Diff, such that patch-diff and diff-patch inversion hold.

We start off by requiring stores to be well-typed given a store type $\mathrm{\Gamma }:x\to \tau$. We define store typing $\mathrm{\Gamma }⊢\sigma$ and differential store validity $\sigma ⊢\mathrm{\Delta }\sigma$ pointwise:

Then the following definitions of patching and diffing satisfy T-Patch and V-Diff:

Patch-diff inversion holds because

and conversely diff-patch inversion is due to

Again, we have modeled differential stores in Rocq and proved the above properties formally there. This shows how to lift changes from values to stores, which provides the foundation for our differential semantics. The Rocq formalization is provided at

We already introduced the syntax of Imp expressions, statements, and stores in Section 2. Figure 2 shows the standard semantics for Imp using two judgments. For expressions, we write $\sigma ⊢e\Rightarrow v$ to denote that expression $e$ evaluates to value $v$ under store $\sigma$. Expressions can read but cannot change the content of the store. The last reduction rule for expressions handles binary expressions $e_1\odot e_2$. Imp supports a few binary operators $\odot \in \{+,-,\ast ,>,\mathrm{𝖾𝗑𝗉}\}$, and we assume that $v_1\odot v_2$ follows the standard arithmetic interpretation of these operators.

For statements, we write $\sigma ⊢s\Rightarrow {\sigma }^{\prime }$ to denote that statement $s$ executes under store $\sigma$, yielding a possibly updated store ${\sigma }^{\prime }$. In these rules, the notation $[x\mapsto v]\sigma$ represents the store obtained from $\sigma$ by updating the mapping of variable $x$ to value $v$, while leaving all other mappings unchanged. For repeat loops, we skip the body when the iteration count is zero. Otherwise, we recursively evaluate the loop with a decremented count, followed by running the body. We opted for this left-recursive loop unrolling to simplify some of the proofs.

A differential semantics describes how a program’s output changes in reaction to input changes. The inputs of our Imp programs are stores $\sigma$. We have described store changes $\mathrm{\Delta }\sigma$ in Subsection 3.3. The output of an Imp program is also a store, but we first only consider Imp expressions. An Imp expression computes a value $v$, hence the differential semantics for Imp expressions computes a value change $\mathrm{\Delta }v$. To this end, we define a differential reduction relation $\sigma ,\mathrm{\Delta }\sigma ⊢e{\Rightarrow }_{\mathrm{\Delta }}\mathrm{\Delta }v$ to compute how $e$’s output changes:

The first rules handle an expression $e$ that is a Boolean or numeric constant. The value of constant expressions can not change, hence the output is a no change (noc). A variable $x$ changes in accordance with $\mathrm{\Delta }\sigma$. In particular, when an input is changed, reading from that input yields its change, which can then be propagated.

The last rule handles binary operators $\odot$ and delegates their differential behavior to dedicated functions ${\odot }_{\mathrm{\Delta }}$. We allow these functions to use the original input values ($v_1$, $v_2$) and their changes ($\mathrm{\Delta }{v}_1$, $\mathrm{\Delta }{v}_2$). For example, for a differential multiplication $m\ast (n\oplus \text{inc }k)$, we need to know the original arguments to compute the output change $\text{inc }(m\ast k)$. While our implementation supports various operators, in this paper and the Rocq formalization we focus on establishing the core differential semantics. A complete treatment of differential operators is outside the scope of this paper.

Note that we required the original store $\sigma$ during the differential execution of expressions only to recover the original arguments of binary operators. In places like these, we can expect an actual implementation to cache the previous evaluation result of each operand where needed. We highlight opportunities for caching in the reduction rules by putting preconditions in parentheses ​​$(\text{cached})$​​ and slightly shading their background.

We define the differential semantics for statements using the relation

which executes statement $s$ under differential store $\mathrm{\Delta }\sigma$ and original store $\sigma$ to yield an updated differential store $\mathrm{\Delta }{\sigma }^{\prime }$. The inference rules are shown in Figure 3.

Rule ​D-Assign evaluates the assigned expressions differentially and then updates the differential store. The store update is a destructive update, overwriting the previous change assigned to $x$. Together with rule ​D-Seq, this realizes change propagation behavior. For example, assume a program $x:=a;y:=x$ with $\mathrm{\Delta }\sigma (a)=\mathrm{\Delta }v$. Rule ​D-Seq runs the assignments in order. The first assignment sets $\mathrm{\Delta }\sigma (x)=\mathrm{\Delta }v$ because $\sigma ,\mathrm{\Delta }\sigma ⊢a{\Rightarrow }_{\mathrm{\Delta }}\mathrm{\Delta }v$. Then the second assignment sets $\mathrm{\Delta }\sigma (y)=\mathrm{\Delta }v$ because ${\sigma }^{\prime },\mathrm{\Delta }{\sigma }^{\prime }⊢x{\Rightarrow }_{\mathrm{\Delta }}\mathrm{\Delta }v$ Note that ​D-Seq also runs the first statement non-incrementally, but only to obtain ${\sigma }^{\prime }$, which is needed as input for $s_2$. The highlighting of this and other preconditions in Figure 3 indicates that the precondition’s result can be retrieved from a cache in an actual implementation.

For conditional statements, we generally distinguish two situations: branch constant and branch switching. A conditional behaves branch-constant if the value of the condition does not change, handled by rules ​D-IF${}_{\text{tt}}$ and ​D-IF${}_{\text{ff}}$. These rules simply propagate changes to the relevant branch that was selected originally. Rules ​D-IF${}_{\text{tf}}$ and ​D-IF${}_{\text{ft}}$ handle branch switching, which happens when the condition’s value changes. If the original value of the condition was true and now becomes false, then rule ​D-IF${}_{\text{tf}}$ fires and performs branch switching as introduced in Subsection 2.2. Originally, we have executed $s_1$, but now we need to run $s_2$. Therefore, we execute $s_2$ from scratch and compute how its output differs from $s_1$. Rule ​D-IF${}_{\text{ft}}$ is analogous and handles the case when the condition switches from false to true.

Finally, we provide four rules to handle repeat loops. The differential semantics for $\text{repeat}es$ depends crucially on how the iteration count changes. When the differential evaluation of $e$ yields ${\text{noc}}_{\mathbb{N}}$, the iteration count remains the same as in the original execution. In this case, we replay the loop but only do change propagation. If the iteration count is zero ($\sigma ⊢e\Rightarrow 0$), we simply return the input differential store unchanged, as no iterations need to be replayed. For a positive count ($\sigma ⊢e\Rightarrow n+1$), we unroll the loop recursively followed by a differential run of the loop body $s$. The resulting $\mathrm{\Delta }{\sigma }^{\prime \prime }$ captures the cumulative effect of differentially executing all iterations.

When the iteration count is decreased ($\sigma ,\mathrm{\Delta }\sigma ⊢e{\Rightarrow }_{\mathrm{\Delta }}\text{dec }k$), the process is more complicated. First, we propagate the changes for $(n-k)$ iterations to obtain $\mathrm{\Delta }{\sigma }^{\prime }$. Then we retrieve the original output after $(n-k)$ iterations ${\sigma }^{\prime }$ and patch it with $\mathrm{\Delta }{\sigma }^{\prime }$. This represents the updated output after $(n-k)$ iterations, but we need to know how it changed compared to $n$ iterations. To this end, we compute the difference with ${\sigma }^{\prime \prime }$, which is the original output after $n$ iterations.

Lastly, when the iteration count grows ($\sigma ,\mathrm{\Delta }\sigma ⊢e{\Rightarrow }_{\mathrm{\Delta }}\text{inc }k$), we use a two-phase strategy. First, we execute the original $n$ iterations differentially to obtain $\mathrm{\Delta }{\sigma }^{\prime }$. However, from here on out, we are dealing with iterations that have not occurred before. Therefore, in the second phase, we execute the additional $k$ iterations non-incrementally. To this end, we compute the updated output after $n$ iterations using $\mathrm{\Delta }{\sigma }^{\prime }$ and feed it as input for the remaining $k$ iterations. Finally, we compute the difference with ${\sigma }^{\prime }$, which was the original output.

Our differential semantics aims to replace recomputation with change-based execution. That is, when the original input $\sigma$ is changed to ${\sigma }^{\prime }=\sigma \oplus \mathrm{\Delta }\sigma$, the differential semantics must be able to process $\mathrm{\Delta }\sigma$ directly. For this to work, we need three guarantees:

Completeness:

Whenever a program can execute under the original $\sigma$ and the updated ${\sigma }^{\prime }$, then the differential semantics must derive an output change for $\mathrm{\Delta }\sigma$.

Output validity:

The output change must be valid for the original output.

From-scratch consistency

Patching the original output with the output changes is consistent with a recomputation starting with ${\sigma }^{\prime }$.

That is: We can obtain changes using the differential semantics, the changes can be used to patch the original output, and the patched output is correct. We have formalized these properties in Rocq and have a mechanized proof that shows our differential semantics satisfies them. Here, we only present the formal formulation of the properties.

In general, we only make claims about well-typed programs $\mathrm{\Gamma }⊢s$. The typing relation for statements and expressions is standard: variables are global and cannot change type. With this, we can formulate the properties of differential semantics.

We formalized the differential semantics of Imp in Rocq and proved completeness, output validity, and from-scratch consistency. The Rocq code is available open-source.²²2https://gitlab.rlp.net/plmz/artifacts/autoinc-interp-formalization-ecoop25 The Rocq formalization consists of approximately 1,450 lines of code and was important in shaping our theory of changes. A key challenge emerged when proving the diff-patch inversion property (Property 3.2) introduced in Section 3. While standard equality was sufficient for proving the patch-diff property (Property 3.1), we discovered it was inadequate for the diff-patch case. We needed a custom equivalence relation because multiple differential values (noc, incr 0, decr 0) can represent the same change semantically

The consistency proof (Theorem 4.3) was particularly challenging, especially for the increment case of repeat statements. The complexity of this case revealed that our initial induction hypothesis wasn’t strong enough – an observation we only gained after successfully proving all other cases. This led to a reformulation of the theorem with a stronger induction hypothesis.

In our opinion, for the number of results we proved, our Rocq code is reasonably compact. This was achieved through careful proof automation: we developed custom tactics for common proof patterns and registered them as hints for Rocq’s eauto system. This automation strategy significantly reduced the proof size.

Short-circuiting rules enable bypassing differential computations entirely under certain conditions. We begin with a special case where all variables of a store map to no change. Then we generalize this rule to handle programs where only referenced variables are unchanged.

The $\epsilon$-Store rule shows that when every variable in the differential store maps to noc, differential execution preserves the input differential store unchanged. This optimization is useful because when no variables have changed at all, we can completely bypass differential execution, avoiding differential computations entirely. The rule is fundamentally sound since a program operating on unchanged inputs must produce unchanged outputs. The premise $\sigma ⊢s\Rightarrow {\sigma }^{\prime }$ in the rule establishes that $s$ executes successfully in the standard semantics, which is necessary for proving the rule’s admissibility.

Consider the following program:

With the differential store $\mathrm{\Delta }\sigma =\{x\mapsto \text{noc},y\mapsto \text{noc},z\mapsto \text{noc},w\mapsto \text{noc},v\mapsto \text{noc}\}$, the rule lets us skip differential execution entirely.

To handle more realistic scenarios where a differential store might contain changes to many variables but a specific program fragment only references unchanged variables, we need to precisely characterize when a fragment is unaffected by changes. We do this through the No-Change relation.

Using this relation, we formulate our second optimization rule as follows: The No-Change rule generalizes the $\epsilon$-Store rule: when no variables referenced in $s$ are affected by changes ($\mathrm{\Gamma },\mathrm{\Delta }\sigma {⊢}_s^{0}s$), any differential execution of $s$ must preserve the input differential store. This optimization is particularly valuable as it allows us to skip computations even when some variables in the program have changed, as long as they aren’t referenced in the code being optimized.

Consider our earlier program fragment in a larger context:

With differential store $\mathrm{\Delta }\sigma =\{x\mapsto \text{noc},y\mapsto \text{noc},z\mapsto \text{noc},w\mapsto \text{noc},v\mapsto \text{noc},a\mapsto \text{inc }5\}$, the No-Change rule lets us skip the first two assignments even though $a$ changes elsewhere in the program. This local reasoning about variable usage avoids wasteful expression evaluation – we don’t compute changes that would inevitably be noc.

Loop constructs often dominate execution time in incremental computations. We present three optimization rules for loops, each handling a different scenario where full recomputation can be avoided. We start with loop idempotence, then present rules for handling changes to iteration counts.

The Loop-Idemp rule provides a significant optimization opportunity: when we can prove that a loop body preserves both the store and differential store in a single iteration and there is no change in the number of loop iterations, we can completely skip executing the remaining iterations. This is valuable because without this rule, we would need to execute each iteration even though we know the final result would be unchanged.

Consider a loop with operations that cancel out:

When $\mathrm{\Delta }\sigma =\{x\mapsto \text{noc},y\mapsto \text{noc}\}$, we can skip all iterations since each iteration preserves the store through these reversing computations. While this example is deliberately simple, the Loop-Idemp rule becomes particularly powerful with richer language features. For instance, in a language with arrays and objects, this rule would recognize loops that appear to modify data structures but actually preserve their state, allowing us to skip such loops entirely when we can prove that their operations are self-cancelling.

Our two most powerful loop optimizations address scenarios where the loop count changes, but the loop body remains unaffected by changes in the differential store. That is, all variables in the loop are assigned noc in the input differential store. This optimization reduces computational effort by focusing only on the additional iterations introduced by the change in the loop count, thereby avoiding redundant execution of the unchanged loop body.

The Loop-Incr rule handles increases in iteration count. When the loop count increases by $m$ iterations and the loop body references no changed variables ($\mathrm{\Gamma },\mathrm{\Delta }\sigma {⊢}_s^{0}s$), we can optimize by doing the following.

• $\mathrm{■}$

  Reusing the result ${\sigma }^{\prime }$ of the original execution

• $\mathrm{■}$

  Computing only the additional $m$ iterations from ${\sigma }^{\prime }$ to get ${\sigma }^{\prime \prime }$

• $\mathrm{■}$

  Computing the differential results as $({\sigma }^{\prime \prime }\oplus \mathrm{\Delta }\sigma )\ominus {\sigma }^{\prime }$

The differential output captures how the loop’s output differs after running the additional iterations. With cached results from the original execution, we only compute the $m$ new iterations: ${\sigma }^{\prime }⊢\text{repeat}ms\Rightarrow {\sigma }^{\prime \prime }$ – precisely the work that must be done. This optimization avoids redoing unchanged iterations while still performing the genuinely new computation. However, when any variable read in the loop body changes (for example, if an array being summed changes), we cannot apply this optimization. This restriction is necessary – changes to variables in the loop body would produce different results in every iteration, invalidating our assumption that earlier iterations remain unchanged and in process invalidating the cached result ${\sigma }^{\prime }$.

Consider the following example where we accumulate a sum with a variable count:

With $\mathrm{\Delta }\sigma =\{n\mapsto \text{inc }2,\text{sum}\mapsto \text{noc},i\mapsto \text{noc}\}$, both sum and i are unchanged in the input store, allowing us to safely reuse cached results. After the original 5 iterations, we compute just 2 more iterations with values we haven’t seen before. If instead we had $\mathrm{\Delta }\sigma =\{n\mapsto \text{inc }2,i\mapsto \text{inc }1\}$, the change to i would affect every iteration’s computation, forcing us to recompute all iterations with the new initial value.

When all premises remain as in the increment case, but with $\sigma ,\mathrm{\Delta }\sigma ⊢e{\Rightarrow }_{\mathrm{\Delta }}\text{dec }m$ replacing the increment, we obtain an elegant formulation for the decrement case as shown below.

For decreased iteration counts, the Loop-Decr rule is even more efficient than the increment case. If we have cached the original computation, we have access to both the original output ${\sigma }^{\prime }$ and the intermediate store ${\sigma }^{\prime \prime }$ after the ${(n-m)}^{th}$ iteration. Then, we can compute the final result directly with just a patch and a diff operation, without any loop execution. This makes the decrement case even more efficient than the increment case, where we still needed to perform $m$ additional iterations. Again, this optimization requires $\mathrm{\Gamma },\mathrm{\Delta }\sigma {⊢}_s^{0}s$, as changes to loop body variables would invalidate our cached states.

Using the same summation example but with $n$ decreasing from 5 to 3 and $\mathrm{\Delta }\sigma =\{n\mapsto \text{dec }2,\text{sum}\mapsto \text{noc},i\mapsto \text{noc}\}$, we don’t need to compute anything new from the normal execution. We can directly use our cached state after 3 iterations to compute the change.

In both the increment and the decrement case, we see that caching the original computation is important for efficiency. We discuss various strategies for caching computations in Section 6.1.

One of the main challenges in differential execution is handling branch switches efficiently, as we typically need to execute both branches and compare their stores. Consider a common pattern in imperative programs, where an if-statement contains only assignments to the same variable in both branches:

With branch switching, the standard differential semantics would compute the result by diffing the resulting stores corresponding to the two different branches that are taken. However, since only variable x changes between branches, we can update just one entry instead of the entire store. This targeted update of x based on the expressions’ difference provides orders of magnitude in speedup over store-wide diffing, especially pronounced for large stores. We develop two optimizations here based on this insight.

The If-T-F rule handles the case where a condition switches from true to false. The rule requires both stores to be well-typed and the conditional statement itself to be well-typed. When the conditional expression $e$ switches from true to false and both branches are assignments to the same variable $x$, we can directly compute the change to $x$ as $v_2\ominus v_1$, where $v_1$ is $e_1$’s value in the original store and $v_2$ is $e_2$’s value in the patched store.

For our example, suppose $y$ was initially true and we have $\mathrm{\Delta }\sigma =\{y\mapsto \text{neg},x\mapsto \text{noc},z\mapsto \text{noc}\}$ causing a branch switch. Instead of recomputing the entire store, we only need to update the entry corresponding to $x$ as $(z-1)\ominus (z+1)=\text{dec }2$. However, if branches modified different variables (e.g., x = z + 1 vs y = z - 1), this optimization cannot apply – the changes aren’t localized to a single variable.

The If-F-T rule handles the symmetric case where the condition switches from false to true. Its structure mirrors the true-to-false case, but computes $v_1\ominus v_2$ since we are switching to the first branch.

This optimization significantly improves performance when stores are large, but changes are localized. In our Bellman-Ford implementation (Figure 5), this optimization avoids diffing the entire shortest-path table on each branch switch within the inner loop’s conditional, leading to substantial speedups as shown in Section 7.

The differential semantics requires access to previous execution states when handling control flow constructs. Consider an if statement $\text{if}e{s}_1{s}_2$ where branch switching occurs, that is, when the condition’s value changes from true to false or vice versa. We reiterate the relevant rule ​D-IF${}_{\text{tf}}$ from Figure 3, highlighting in gray the computations that can be cached from the previous execution:

Applying this rule requires performing new computations while accessing cached results from the previous execution. Specifically, we must differentially evaluate the condition to get neg and execute the new branch $s_2$, while we can reuse the original condition evaluation result and the result of executing $s_1$. A similar requirement exists for repeat statements, which need stores from previous iterations to enable differential execution. This dependency on previous states explains why our differential reduction relation $\sigma ,\mathrm{\Delta }\sigma ⊢s{\Rightarrow }_{\mathrm{\Delta }}\mathrm{\Delta }{\sigma }^{\prime }$ takes the previous store $\sigma$ as input.

Re-computing previous results and propagating old states throughout differential execution incurs significant performance overhead. To address this, we develop an initializing interpreter that caches execution states. However, uniquely identifying cached states requires more than just statement identifiers, particularly for loops. Consider $\text{repeat}5s$ where $s$ executes five times – each iteration operates on a different store and thus requires its own cached state.

We solve this through path-sensitive identifiers that precisely track loop nesting structure. A path $P$ starts at root $R$ (nesting level 0) and records each enclosing loop’s iteration count. For example, path $R,2,1$ indicates execution within the first iteration of an inner loop, nested within the second iteration of an outer loop. Our cache maps each execution point to its corresponding program state: $\text{cache}:\text{UID}\times 𝐏\mapsto 𝐒$, where UID uniquely identifies statements in the program, $P$ captures the loop nesting context through iteration counts, and $S$ represents the program state we need to cache.

Our caching strategy for conditional statements preserves three key pieces: the store before evaluating the condition, the condition’s evaluated result, and the store after executing the chosen branch. This enables direct access to previously computed states, eliminating redundant recomputation during differential execution.

For repeat statements, we implement two strategies: a basic strategy that caches the initial store, iteration count, and final store, and an enhanced strategy that additionally caches intermediate states after each iteration. The enhanced strategy enables efficient implementation of the decrement optimization (Section 5.2) by providing direct access to any intermediate store from the original execution, eliminating the need for additional computation.

We have implemented a differential interpreter that supports more constructs than present in the formalization. In addition to integer and boolean values, we also support string values. In the same vein, the language supports more than just the addition operator. It can call arbitrary operators based on an operator interface which requires an init function and an inc function:

The type Change[T] marks a change of value type T. Note that operators themselves can keep track of local state that is required for implementing efficient incremental operators. Additionally, the language enables first-order function calls of user-defined top-level functions. Each function ranges over its own local store.

One major difference is that the language supports a mutable 2-dimensional table ranging over integers which is global to all functions. To this end, the language supports a table-write statement $\text{table}[i,j]=e$ and a table-read expression $\text{table}[i,j]$. Note that we currently assume that the indices cannot change between the initialization and a differential run. This is a restriction we want to address in the future work.

To enable efficient differential execution, we implemented various optimizations. We describe optimizations in the formalization as overlapping rules, where we decide manually which rule to apply. Our implementation always applies the optimization rule whenever possible. One could imagine that there are multiple applicable optimization rules. This leads to optimization strategies which select the optimization rule to apply at a given point at execution time. We want to investigate optimization strategies in future work.

We implemented the short-circuiting optimizations from Section 5.1 by preemptively computing read/written variables within statements and expressions. Because our language supports a 2-dimensional global table, this analysis extends to tracking table cell accesses. Building on the branch switching optimization from Section 5.3, we handle table operations efficiently:

When branches differ only in their expressions ($e_1$ vs $e_2$), we can avoid expensive table diffing operations by directly computing $\mathrm{\Delta }t[(i,j)\mapsto v_2\ominus v_1]$ where $\sigma ⊢e1\Rightarrow v_1$ and $\sigma \oplus \mathrm{\Delta }\sigma ⊢e2\Rightarrow v_2$.

To evaluate our differential interpreter, we designed a graph structure that exhibits interesting incremental behavior. The graph is a cycle where we can configure its size by setting the number of nodes $X\in \{10,30,\mathrm{\dots },130,150\}$:

The weight of the back edge $X\to 1$ is chosen to introduce new shortest paths, ensuring that small input changes can trigger significant output changes. We compute shortest paths starting from node 1 for different values of $X$ and evaluate two types of changes:

1. (i)

   Adding an edge $1\to (X-1)$ with weight ${10}^9$. This introduces an alternative path that does not affect the shortest path solution.

2. (ii)

   Adding six edges forming cross-connections: $1\to (X-1)$, $2\to (X-2)$, $6\to (X-2)$, $(X-5)\to 6$, $(X-3)\to 3$, and $(X-1)\to 2$, each with weight ${10}^9$. Despite creating multiple new paths, these additions do not affect the shortest path solution.

We conducted experiments on an Apple M4 Pro chip with 24GB memory running 64-bit OSX 15.1.1 and OpenJDK 23.0.1. Using the JMH benchmarking framework³³3https://github.com/openjdk/jmh, we performed 5 warmup runs followed by 10 measurement runs for each configuration.

In Figure 6, we compare the running times of differential interpretation against normal interpretation on the patched input. On the left we show the running times for change (i) and on the right we show them for change (ii). The differential interpreter outperforms normal interpretation for change (i). While Bellman-Ford has a time complexity of $O(X^3)$, the differential interpreter can skip most iterations because we employ an optimization that skips loop iterations when the changed table entries are not affected by the iteration. Since change (i) modifies just a single table entry without introducing new shortest paths, we can skip almost all iterations, yielding significant running time savings. The same benefits apply to change (ii), though to a lesser degree as fewer iterations are skippable.

A second critical optimization avoids diffing when branch switches occur, significantly reducing the differential interpreter’s running time. Without this optimization, all branch switches for the inner if statement within the nested repeat loops would require diffing the old and new result tables, incurring an $O(X^2)$ cost. Instead, we apply constant-time updates to the current delta table.

To evaluate stability over extended use, we executed 40 consecutive changes (Change (ii)) on graphs of varying sizes (10-150 nodes). We measured performance at five points in this sequence (1${}^{\text{st}}$, 10${}^{\text{th}}$, 20${}^{\text{th}}$, 30${}^{\text{th}}$, and 40${}^{\text{th}}$ change), with 5 warmup and 10 measurement runs per point. After filtering outliers using the interquartile range (IQR) method, our analysis confirms that execution times remain consistent across the change sequence for each graph size. The Coefficient of Variation (CV), which measures relative variability as standard deviation divided by mean, is remarkably low (average 8%, maximum 13%), indicating that our differential approach maintains stable performance throughout extended use without degradation. While execution times scale with graph size as expected, the consistent performance within each size category demonstrates that repeated incremental updates do not compromise efficiency, further justifying the one-time initialization cost.

In Figure 7 we compare the running times of the initializing interpreter to normal interpretation on the initial input. On the left we show the running times for change (i) and on the right for change (ii). The graphs show that initialization requires significantly more time than normal interpretation. Normal interpretation takes roughly 1.5s for processing the initial graph where $X=150$. In contrast, the initialization interpreter requires roughly 15s, a 10x increase. This overhead comes from caching states by inserting entries into hash tables. This overhead is an implementation artifact that we believe can be substantially reduced through engineering improvements and smarter caching strategies.

These results demonstrate that differential interpretation of dynamic algorithms like Bellman-Ford is feasible and can achieve order-of-magnitude speedups, provided we have: 1)  optimizations that reduce work by skipping unaffected program fragments, enabled by precise change descriptors, and 2) efficient caching strategies to minimize initialization overhead. Additionally, reducing initialization time remains an important area for improvement.