Finite straight-line computational programs and real-arithmetic tapes

Fix an input dimension $n\ge 0$, finitely many operation nodes $1,\dots ,T$, and a designated output node $o$, either an input coordinate or an operation, whose value space is $\mathbb{R}$. Give input coordinate $i$ a label ${\mathrm{i}\mathrm{n}}_i$ distinct from all operation indices, and set $z_{{\mathrm{i}\mathrm{n}}_i}=x_i$ and $E_{{\mathrm{i}\mathrm{n}}_i}=\mathbb{R}$ with its standard Euclidean inner product. Operation node $j$ has an ordered list of parent slots $p_{j,1},\dots ,p_{j,r_j}$; each slot is either an input label ${\mathrm{i}\mathrm{n}}_i$ or an operation index $\mathrm{\ell }<j$. Repeated parent slots are allowed and count separately. The graph is a finite straight-line program because every operation reads only earlier values and there are no data-dependent loops.

For each operation $j$, choose a dimension $d_j\ge 0$, set $E_j={\mathbb{R}}^{d_j}$ with its standard Euclidean inner product, take an open set $U_j\subseteq E_{p_{j,1}}\times \cdots \times E_{p_{j,r_j}}$ with the product inner product, and choose a primitive map ${\varphi }_j:U_j\to E_j$. A smooth primitive is $C^1$: it is totally differentiable and its derivative matrix is continuous. For Hessian-vector products require the primitive to be $C^2$, meaning $C^1$ with a continuously differentiable derivative map. Derivatives are represented in these coordinates, and every transpose is the Euclidean transpose for the stated inner products; the gradient of a scalar output is the Euclidean gradient. The real-arithmetic primal recursion is $z_j={\varphi }_j(z_{p_{j,1}},\dots ,z_{p_{j,r_j}})$ whenever the parent tuple lies in $U_j$. Its admissible input domain is the set of $x\in {\mathbb{R}}^n$ for which every operation in this recursion is defined. The graph's scalar output function $f$ is the value at $o$: it is $x_i$ when $o$ is input coordinate $i$, and $z_j$ when $o$ is operation node $j$.

The primal tape is the finite ordered record of input and node values, parent-slot indices, primitive identities, and (when applicable) selected branch labels. A deterministic replay starts from the identical checkpoint state and applies the identical primitive maps in the identical order, so it reproduces the same real-arithmetic values and local derivative inputs. Opaque solver calls are not primitive operations unless their complete deterministic map and derivative rule are explicitly supplied.

A piecewise-$C^1$ primitive is specified by finitely many open branch regions and a $C^1$ formula on each region; its primal boundary value, if any, is specified separately. If the current parent tuple lies strictly inside exactly one declared branch, the program uses that branch and its derivative. At a branch boundary or ambiguous branch selection, forward or reverse AD returns NONDIFFERENTIABLE; it does not silently choose a subgradient or generalized derivative. If no primal value is specified at a boundary, that input is outside the program's domain. All correctness theorems below apply on a fixed strict branch. The same convention applies to piecewise-$C^2$ primitives for Hessian-vector products.