Chapter 182Optional

Differentiable Semantics and Forward-Mode Automatic Differentiation

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

Let $g : R^{2} \to R$ be given by a program, and suppose we want $\partial g / \partial x_{1}$ at a point. Two answers present themselves and both fail.

Symbolic differentiation rewrites the expression $g$ into an expression for its derivative. It works for the grammar of arithmetic expressions, and it stops working as soon as the program contains a function-valued subterm: there is no rule for differentiating $λ f . f (f x)$ , because the expression to be differentiated is not built from $+$ , $*$ , and named smooth constants, and the intermediate object $f$ has no derivative until it is instantiated.

Numerical differencing evaluates $(g (x + ε e_{1}) - g (x)) / ε$ . It applies to any program, and it certifies nothing: for every finite set of tolerances and step sizes there are two smooth functions agreeing on all of them whose derivatives at $x$ differ, so agreement of a transformation with a difference quotient at finitely many points is not evidence that the transformation computes a derivative.

What is wanted is a source-to-source transformation, defined by induction on the program including its higher-order subterms, together with a theorem stating what the transformed program denotes. This chapter fixes one source language, defines that transformation, and proves the theorem at first-order input and output types, higher-order subterms being permitted inside. The proof is a logical relation between what the program denotes and what its transform denotes; the interesting clause is at function types, and it is forced, not chosen.

The invariant to be maintained

Before any syntax, fix what the transformed program is supposed to compute.

Definition 182.1 — Tangent pairing ¶

Let $g : R^{n} \to R$ . A function $h : (R \times R)^{n} \to R \times R$ is a tangent representation of $g$ when for all smooth $f_{1}, \dots, f_{n} : R \to R$ and all $x \in R$ , $\begin{aligned} h (f_{1} (x), f_{1}^{'} (x), \dots, f_{n} (x), f_{n}^{'} (x)) \\ = (g (f_{1} (x), \dots, f_{n} (x)), (g \circ (f_{1}, \dots, f_{n}))^{'} (x)) . \end{aligned}$

Referenced from 4 locations

Differentiable Semantics and Forward-Mode Automatic Differentiation

Equation 182.1 is a statement about composition, not about a single point, and that is what makes it usable as an induction hypothesis: it says that $h$ transports first-order Taylor data through $g$ . Instantiating it recovers the familiar quantities.

Example 182.2 — Partial derivatives from the invariant ¶

Take $n = 2$ , fix $a \in R^{2}$ , and let $f_{1} (x) : = x$ , $f_{2} (x) : = a_{2}$ , evaluated at $x = a_{1}$ . Then $f_{1}^{'} = 1$ and $f_{2}^{'} = 0$ , and equation 182.1 reads $h (a_{1}, 1, a_{2}, 0) = (g (a), \frac{\partial g}{\partial x_{1}} (a)) .$ Choosing $f_{1}^{'} = 0$ , $f_{2}^{'} = 1$ gives the other partial derivative, and a general pair of tangents gives the directional derivative. So a single $h$ satisfying equation 182.1 contains all first-order derivative information about $g$ , and one evaluation of $h$ yields one directional derivative at the cost of one evaluation of $g$ up to a constant factor.

Referenced from 5 locations

Differentiable Semantics and Forward-Mode Automatic Differentiation

Remark 182.3 — Why a difference quotient cannot replace this ¶

Let $g_{1} (x) : = 0$ and $g_{2} (x) : = ε_{0} \sin (x / ε_{0}^{2})$ for a fixed $ε_{0} > 0$ . For any finite set $E$ of step sizes one may choose $ε_{0}$ so that $g_{2}$ agrees with $g_{1}$ to within any prescribed tolerance on all quotients formed from $E$ at $0$ , while $g_{2}^{'} (0) = 1 / ε_{0}$ is arbitrarily large. Agreement of a transformation with difference quotients on finitely many inputs is therefore consistent with an arbitrarily wrong derivative, which is why the correctness statement below is an equation between denotations rather than a numerical comparison.

Referenced from 3 locations

Differentiable Semantics and Forward-Mode Automatic Differentiation

The source language

Definition 182.4 — Types and terms ¶

Fix for each $n \geq 0$ a set ${Op}_{n}$ of $n$ -ary operation symbols, containing a symbol $\underset{―}{c}$ for each $c \in R$ in ${Op}_{0}$ and containing $+, * \in {Op}_{2}$ . Types and terms are $τ, σ ::= real ∣ (τ_{1} * \dots * τ_{n}) ∣ τ \to σ,$ $\begin{aligned} t, s ::= & x ∣ op (t_{1}, \dots, t_{n}) ∣ ⟨ t_{1}, \dots, t_{n} ⟩ \\ ∣ & case t of ⟨ x_{1}, \dots, x_{n} ⟩ \to s ∣ λ x : τ . t ∣ t s . \end{aligned}$ The typing rules are the expected ones: a variable has its declared type; $op \in {Op}_{n}$ applied to $n$ terms of type $real$ has type $real$ ; a tuple of terms of types $τ_{i}$ has the product type; $case$ eliminates a product by binding its components; abstraction and application are as in chapter 2. We write $Γ ⊢ t : τ$ and use $let x = t in s$ for $(λ x . s) t$ .

Referenced from 5 locations

Definition 182.5 — Set-theoretic denotation ¶

Assume given for each $op \in {Op}_{n}$ a smooth function $[[op]] : R^{n} \to R$ , with $[[\underset{―}{c}]] = c$ , $[[+]]$ addition and $[[*]]$ multiplication. Interpret $[[real]] : = R$ , products as products of sets, and $[[τ \to σ]]$ as the set of all functions $[[τ]] \to [[σ]]$ . A context $Γ = x_{1} : τ_{1}, \dots, x_{m} : τ_{m}$ denotes the product of the $[[τ_{i}]]$ , and a derivation of $Γ ⊢ t : τ$ denotes a function $[[t]] : [[Γ]] \to [[τ]]$ by the usual clauses: variables project, $op$ applies $[[op]]$ , tuples pair, $case$ substitutes the components, abstraction curries, and application evaluates.

Referenced from 4 locations

Interpreting $τ \to σ$ by all functions is deliberately crude: it makes $[[t]]$ defined for every term, and it makes no claim of smoothness at function types, where no claim is yet available. The correctness theorem below never mentions $[[τ \to σ]]$ except through the logical relation.

The tangent macro

Definition 182.6 — The macro D ¶

On types, $\begin{aligned} D (real) & : = (real * real), & D (τ \to σ) & : = D τ \to D σ, \\ D (τ_{1} * \dots * τ_{n}) & : = (D τ_{1} * \dots * D τ_{n}) . \end{aligned}$ On terms, $D$ is the identity on variables and commutes with every constructor, $D (λ x : τ . t) : = λ x : D τ . D t, D (t s) : = (D t) (D s),$ and similarly for tuples and $case$ , except at operations: $\begin{aligned} D (op (t_{1}, \dots, t_{n})) : = & case D t_{1} of ⟨ x_{1}, x_{1}^{'} ⟩ \to \dots \\ case D t_{n} of ⟨ x_{n}, x_{n}^{'} ⟩ \to \\ ⟨ op (\vec{x}), \sum_{i = 1}^{n} \partial_{i} op (\vec{x}) * x_{i}^{'} ⟩, \end{aligned}$ where $\vec{x}$ abbreviates $x_{1}, \dots, x_{n}$ and $\partial_{i} op$ is a chosen term of the language, with free variables among $x_{1}, \dots, x_{n}$ , such that $[[\partial_{i} op]] = \partial [[op]] / \partial x_{i}$ . For a context $Γ$ , write $D Γ$ for the context with each type replaced by its image.

Referenced from 10 locations

Lemma 182.7 — The macro preserves typing ¶

If $Γ ⊢ t : τ$ then $D Γ ⊢ D t : D τ$ .

Referenced from 3 locations

Differentiable Semantics and Forward-Mode Automatic Differentiation

Proof of Lemma 182.7 — The macro preserves typing

Proof. Induction on the typing derivation. Every clause but the operation clause replaces each type by its image and leaves the rule shape unchanged, so the same rule applies. For $op (t_{1}, \dots, t_{n})$ , the induction hypothesis gives $D Γ ⊢ D t_{i} : (real * real)$ ; each $case$ then binds $x_{i}, x_{i}^{'}$ at type $real$ , the terms $op (x_{1}, \dots, x_{n})$ and $\partial_{i} op (x_{1}, \dots, x_{n})$ have type $real$ by the operation rule, and the displayed pair has type $(real * real) = D (real)$ . ◻

Example 182.8 — A first-order program ¶

Let $t : = x_{1} * x_{2} + x_{1}$ with $x_{1}, x_{2} : real$ . Writing $⟨ a, a^{'} ⟩$ for the pair bound to $x_{1}$ and $⟨ b, b^{'} ⟩$ for the pair bound to $x_{2}$ , the macro gives, after the $case$ bindings are performed, $D t = ⟨ a * b + a, (b * a^{'} + a * b^{'}) + a^{'} ⟩,$ using $\partial_{1} * (x_{1}, x_{2}) = x_{2}$ , $\partial_{2} * (x_{1}, x_{2}) = x_{1}$ , and $\partial_{1} + = \partial_{2} + = \underset{―}{1}$ . Evaluating at $a^{'} = 1, b^{'} = 0$ gives $(a b + a, b + 1)$ , which is the value together with $\partial (x_{1} x_{2} + x_{1}) / \partial x_{1}$ , as example 182.2 predicts.

Referenced from 2 locations

Differentiable Semantics and Forward-Mode Automatic Differentiation

Example 182.9 — A program with a higher-order subterm ¶

Let $t : = (λ f : real \to real . f (f x)) (λ y : real . y * y),$ so $x : real ⊢ t : real$ and $[[t]] (x) = x^{4}$ . The macro does not differentiate the higher-order subterm symbolically; it applies itself structurally, giving $D t = (λ f : D (real \to real) . f (f x)) (λ y : (real * real) . y *_{D} y),$ where $y *_{D} y$ abbreviates the operation clause at $*$ . Evaluating $D t$ at $⟨ a, 1 ⟩$ : the inner function sends $⟨ u, u^{'} ⟩$ to $⟨ u^{2}, 2 u u^{'} ⟩$ , so two applications give $⟨ a^{2}, 2 a ⟩$ and then $⟨ a^{4}, 2 a^{2} \cdot 2 a ⟩ = ⟨ a^{4}, 4 a^{3} ⟩$ . The derivative of $x^{4}$ is obtained without any rule for differentiating $λ f . f (f x)$ , which is the point: $D$ is defined on all terms, including those a symbolic differentiator has no rule for.

Referenced from 4 locations

Differentiable Semantics and Forward-Mode Automatic Differentiation

Exercise 182.1 ¶

★☆☆ Apply $D$ to $t : = ς (x_{1} * x_{2})$ for a unary operation $ς$ with $\partial_{1} ς = ς^{'}$ , and evaluate the result at $⟨ a, 1 ⟩, ⟨ b, 0 ⟩$ . Check the answer against the chain rule.

Referenced from 2 locations

Differentiable Semantics and Forward-Mode Automatic Differentiation

Exercise 182.2 ¶

★★☆ Show that $D (let x = t in s)$ and $let x = D t in D s$ are the same term, and explain why the analogous statement for a symbolic differentiator that substitutes $t$ for $x$ before differentiating changes the number of operations executed.

Referenced from 2 locations

Differentiable Semantics and Forward-Mode Automatic Differentiation

Correctness

The macro is defined by structural recursion, so its correctness proof must be by structural induction; and the statement to be proved cannot be equation 182.1 itself, because that statement mentions only $real$ and the induction passes through function types. The standard repair is to define, for every type, a relation between what a term denotes and what its transform denotes, arranged so that the function-type clause is preserved by application. Here the relation is between smooth curves, since equation 182.1 is itself a statement about curves.

Definition 182.10 — The tangent relation ¶

For each type $τ$ define $S_{τ} \subseteq (R \to [[τ]]) \times (R \to [[D τ]])$ by induction on $τ$ : $\begin{aligned} S_{real} & : = {(f, x \mapsto (f (x), f^{'} (x))) : f : R \to R smooth}, \\ S_{(τ_{1} * \dots * τ_{n})} & : = {((f_{1}, \dots, f_{n}), (g_{1}, \dots, g_{n})) : (f_{i}, g_{i}) \in S_{τ_{i}} for each i}, \\ S_{τ \to σ} & : = {(F, G) : for all (a, b) \in S_{τ}, \\ (x \mapsto F (x) (a (x)), x \mapsto G (x) (b (x))) \in S_{σ}} . \end{aligned}$ For a context $Γ = x_{1} : τ_{1}, \dots, x_{m} : τ_{m}$ , write $(γ, δ) \in S_{Γ}$ when the $i$ -th components are related by $S_{τ_{i}}$ for each $i$ .

Referenced from 8 locations

Differentiable Semantics and Forward-Mode Automatic Differentiation

The clause at $τ \to σ$ is the only one with a choice in it, and there is no choice: the induction step for application must turn related functions and related arguments into related results, and the displayed clause is exactly that requirement read as a definition. Note also what the clause does not say: it does not assign a derivative to a higher-order value. It relates a curve of functions to a curve of functions, and two different curves in $[[D (τ \to σ)]]$ may be related to the same curve in $[[τ \to σ]]$ .

Lemma 182.11 — Fundamental lemma ¶

Let $Γ ⊢ t : τ$ and let $(γ, δ) \in S_{Γ}$ . Then $(x \mapsto [[t]] (γ (x)), x \mapsto [[D t]] (δ (x))) \in S_{τ} .$

Referenced from 9 locations

Differentiable Semantics and Forward-Mode Automatic Differentiation

Proof of Lemma 182.11 — Fundamental lemma

Proof. Induction on the derivation of $Γ ⊢ t : τ$ .

Variable. Both sides are the corresponding components of $γ$ and $δ$ , related by hypothesis.

Abstraction. Let $t = λ x : σ . s$ with $Γ, x : σ ⊢ s : ρ$ . Let $(a, b) \in S_{σ}$ . Then $((γ, a), (δ, b)) \in S_{Γ, x : σ}$ , so the induction hypothesis gives that $x \mapsto [[s]] (γ (x), a (x))$ and $x \mapsto [[D s]] (δ (x), b (x))$ are related by $S_{ρ}$ . These are exactly the two curves required by the clause at $σ \to ρ$ applied to the curves $x \mapsto [[t]] (γ (x))$ and $x \mapsto [[D t]] (δ (x))$ .

Application. Immediate from the clause at $σ \to ρ$ and the two induction hypotheses.

Tuples and $case$ . Componentwise from the product clause; for $case$ , the induction hypothesis for the scrutinee gives related component curves, which extend the environments as in the abstraction case.

Operations. Let $t = op (t_{1}, \dots, t_{n})$ . By the induction hypothesis, for each $i$ there is a smooth $f_{i} : R \to R$ with $[[t_{i}]] (γ (x)) = f_{i} (x)$ and $[[D t_{i}]] (δ (x)) = (f_{i} (x), f_{i}^{'} (x))$ . Reading definition 182.6 at these values, the first component of $[[D t]] (δ (x))$ is $[[op]] (f_{1} (x), \dots, f_{n} (x))$ , which is $[[t]] (γ (x))$ , and the second is $\sum_{i = 1}^{n} \frac{\partial [[op]]}{\partial x_{i}} (f_{1} (x), \dots, f_{n} (x)) \cdot f_{i}^{'} (x) \overset{c h a i n r u l e}{=} ([[op]] \circ (f_{1}, \dots, f_{n}))^{'} (x) .$ The composite $[[op]] \circ (f_{1}, \dots, f_{n})$ is smooth, being a composite of smooth functions, so the pair lies in $S_{real}$ . ◻

Theorem 182.12 — Correctness at a first-order interface ¶

Let $Γ ⊢ t : real$ where every variable of $Γ = x_{1} : real, \dots, x_{n} : real$ has type $real$ . Let $\vec{f} : = (f_{1}, \dots, f_{n})$ be an $n$ -tuple of smooth functions $R \to R$ and write $\vec{f} (x)$ for the tuple of their values at $x$ . Then $[[t]] \circ \vec{f}$ is smooth and $[[D t]] (f_{1} (x), f_{1}^{'} (x), \dots, f_{n} (x), f_{n}^{'} (x)) = ([[t]] (\vec{f} (x)), ([[t]] \circ \vec{f})^{'} (x)) .$ That is, $[[D t]]$ is a tangent representation of $[[t]]$ in the sense of definition 182.1. In particular $[[D t]] (a_{1}, 1, a_{2}, 0, \dots, a_{n}, 0) = ([[t]] (a), \partial [[t]] / \partial x_{1} (a))$ whenever $[[t]]$ is differentiable in its first argument at $a$ .

Referenced from 14 locations

Proof of Theorem 182.12 — Correctness at a first-order interface

Proof. Consider the two curves $γ (x) : = \vec{f} (x), δ (x) : = (f_{1} (x), f_{1}^{'} (x), \dots, f_{n} (x), f_{n}^{'} (x)) .$ They satisfy $(γ, δ) \in S_{Γ}$ by definition 182.10. Apply lemma 182.11 and read off the clause $S_{real}$ : the first curve is smooth, and the second is the pair consisting of it and its derivative. The final sentence is example 182.2, taking $f_{1} = id$ and every other $f_{i}$ constant. ◻

Remark 182.13 — The exact boundary of the theorem ¶

Theorem 182.12 constrains $t$ only at its interface: the free variables and the result have type $real$ . Function types may occur anywhere inside $t$ , as in example 182.9, and the proof passes through them by definition 182.10. What the theorem does not provide is a derivative of a higher-order term. The relation $S_{τ \to σ}$ is not the graph of a function, and a term of type $(real \to real) \to real$ typically has several transforms all satisfying the relation. The statement also says nothing about recursion, iteration, conditionals on real comparisons, probabilistic primitives, or nonsmooth operations: each of these would add a term former, and each would need its own clause in definition 182.10 and its own case in lemma 182.11.

Referenced from 3 locations

Theorem 182.14 — Higher order and all first-order types; imported ¶

Let $k, R \geq 1$ and let $D^{(k, R)}$ be the macro of definition 182.6 with $D^{(k, R)} (real)$ the type of tuples of $(\binom{R + k}{k})$ reals and with the operation clause given by the multivariate Faà di Bruno formula.

For every $t$ with $x_{1} : real, \dots, x_{n} : real ⊢ t : real$ , the function $[[D^{(k, R)} t]]$ is the $(k, R)$ -Taylor representation of $[[t]]$ : it transports all partial derivatives of order at most $R$ of any $n$ -tuple of smooth maps $R^{k} \to R$ through $[[t]]$ .
For every first-order type $τ$ , every first-order context $Γ$ , and every $Γ ⊢ t : τ$ , the translation $D^{(k, R)}$ coincides with the $(k, R)$ -jet bundle functor, modulo canonical isomorphisms $[[D^{(k, R)} τ]] ≅ D^{(k, R)} [[τ]]$ .

Referenced from 4 locations

Clause (i) is Theorem 4.3 and clause (ii) is Theorem 6.6 of Huot, Staton, and Vákár, Higher Order Automatic Differentiation of Higher Order Functions, arXiv:2101.06757. Their proofs interpret the language in diffeological spaces — sets equipped with a family of plots $R^{k} \to X$ closed under smooth reparametrization — and run the argument of lemma 182.11 inside a category glued along plots; clause (ii) additionally uses that smooth maps out of a connected $R^{k}$ into a disjoint union of manifolds factor through one summand. Theorem 182.12 is the case $k = R = 1$ with first-order interface, proved above over ordinary sets because at that instance the relation of definition 182.10 is already reflexive on the curves it needs. What is imported is exactly (i) and (ii); nothing is imported about recursion, partiality, or nonsmooth primitives, which those authors exclude, and nothing about implementation cost.

Perturbation confusion

Implementations of forward differentiation usually do not implement definition 182.6. They implement a run-time operator $D$ on closures, defined by $D f x : = tg (f (x + 1 ϵ)),$ where $x + 1 ϵ$ builds a dual number and $tg$ extracts its tangent component. The two settings differ, and the difference is not cosmetic.

Example 182.15 — Confusion with one ε ¶

Evaluate $D (λ x . x * D (λ y . x + y) 1) 1$ . Mathematically the inner derivative is $1$ for every $x$ , so the function being differentiated is $x \mapsto x$ and the answer is $1$ . With a single $ϵ$ , the outer call binds $x : = 1 + 1 ϵ$ , the inner call binds $y : = 1 + 1 ϵ$ , and the inner body is $(1 + 1 ϵ) + (1 + 1 ϵ) = 2 + 2 ϵ$ , whose tangent is $2$ . The outer body is then $(1 + 1 ϵ) * 2 = 2 + 2 ϵ$ , whose tangent is $2$ . The answer is wrong by a factor of two, and the cause is that one symbol $ϵ$ was used for two different derivative calculations.

Referenced from 5 locations

Differentiable Semantics and Forward-Mode Automatic Differentiation

The repair is to allocate a fresh tag at each invocation of $D$ and to let ${tg}_{ϵ_{1}}$ pass through dual numbers tagged $ϵ_{2} \neq ϵ_{1}$ . That repairs example 182.15 and every first-order nesting. It is not sufficient in general.

Example 182.16 — Confusion surviving fresh tags; imported counterexample ¶

Define the offset operator $s u f x : = f (x + u)$ , of type $R \to (R \to R) \to R \to R$ . Then for all $f$ and $y$ , $D s 0 f y = \frac{\partial}{\partial u} [f (y + u)]_{u = 0} = f^{'} (y) = D f y,$ so $\hat{D} : = D s 0$ ought to equal $D$ . Manzyuk, Pearlmutter, Radul, Rush, and Siskind [MPR^+19] exhibit $h$ and $y$ for which $\hat{D} (\hat{D} h) y$ differs from $D (D h) y$ under the fresh-tag discipline extended to function-valued results by post-composition, ${tg}_{ϵ} \bar{g} : = {tg}_{ϵ} \circ \bar{g}$ . The cause is that $D s 0$ returns a function, so the tag allocated by the outer invocation is captured in a closure and is later reused by an invocation that should have received a distinct tag. Their paper analyses the failure and proposes two repairs, one delaying tag creation by eta expansion and one wrapping the outputs of derivative operators.

Referenced from 3 locations

Differentiable Semantics and Forward-Mode Automatic Differentiation

Remark 182.17 — Why the macro is not exposed to this ¶

Definition 182.6 allocates no tags, because it has no run-time derivative operator: differentiation happens once, at translation time, and the translated program is an ordinary program of the same language. The counterexamples above are therefore not counterexamples to theorem 182.12; they are counterexamples to the claim that a run-time $D$ with dynamically allocated tags implements the same mathematics. They belong here because they delimit the theorem: what has been proved is a statement about $D$ and $[[-]]$ , and an implementation that departs from definition 182.6 — by taking derivatives of closures at run time, for instance — is outside its scope and needs its own correctness argument. A reader who wants nested derivatives inside the frozen language obtains them by applying $D$ twice, which produces a term with no tags in it at all.

Referenced from 3 locations

Differentiable Semantics and Forward-Mode Automatic Differentiation

Exercise 182.3 ¶

★★☆ Compute $D (D t)$ for $t : = x * x$ and evaluate it at the value that example 182.2 prescribes for a second derivative. Check the result against $\partial^{2} (x^{2}) / \partial x^{2} = 2$ , and identify which component of the four-fold nested pair carries it.

Referenced from 2 locations

Differentiable Semantics and Forward-Mode Automatic Differentiation

Exercise 182.4 ¶

★★☆ Redo example 182.15 with distinct tags $ϵ_{1}$ for the outer invocation and $ϵ_{2}$ for the inner one, using the rule ${tg}_{ϵ_{1}} (a + b ϵ_{2}) = ({tg}_{ϵ_{1}} a) + ({tg}_{ϵ_{1}} b) ϵ_{2}$ for $ϵ_{1} \neq ϵ_{2}$ , and verify that the answer is $1$ . Then state precisely which step of your calculation would fail if the inner invocation reused $ϵ_{1}$ .

Referenced from 2 locations

Differentiable Semantics and Forward-Mode Automatic Differentiation

Comparisons

Syntactic differentiation. Chapter 181 differentiates a term without any notion of smooth function: its $\frac{\partial s}{\partial x} \cdot u$ places one linear copy of $u$ at one occurrence of $x$ and sums. The comparison is exact at one point and misleading elsewhere. Both operations satisfy a product rule and a chain rule, and both are defined by structural recursion. But the resource derivative is about use counting and its correctness criteria are confluence and the Taylor identity of that chapter, while $D$ is about numerical tangents and its correctness criterion is theorem 182.12. No theorem transfers in either direction.

Coherent differentiation. Ehrhard’s coherent differentiation develops a summability structure in which only certain pairs of terms may be added, so that differentiation makes sense without the unrestricted sums of chapter 181. It separates the two settings: the present chapter never adds two program values, because definition 182.6 produces pairs rather than sums, and the addition that appears in the operation clause is the addition of the object language at type $real$ .

Implementation comparisons. Typed array languages with index sets, such as Dex, implement forward mode with a type discipline that tracks which index sets a tangent belongs to. That design is a comparison only: no array language theorem is imported here, and theorem 182.12 says nothing about arrays. Elliott’s compositional derivation, the survey of Baydin, Pearlmutter, Radul, and Siskind [BPRS18], and the matrix calculus course of Edelman and Johnson [EJ23] supply the dual-number, computation-graph, and finite-difference prelude that section 182.1 compresses into one invariant.

Suggested first pass.

None of these problems is a prerequisite for a later chapter. Begin with exercise 182.5, then exercise 182.6; the implementation project exercise 182.8 may be attempted at any time.

Exercise 182.5 ¶

★★☆ Suppose the clause $S_{τ \to σ}$ of definition 182.10 were replaced by “ $F = G$ pointwise after erasing tangent components”. Show that lemma 182.11 then fails, by exhibiting a term whose application case cannot be discharged. Then show that the displayed clause is the weakest one that discharges the application case.

Referenced from 3 locations

Differentiable Semantics and Forward-Mode Automatic Differentiation

Exercise 182.6 ¶

★★★ Add to definition 182.4 a conditional on reals, written $if t < 0 then s_{1} else s_{2}$ , with the evident denotation, and extend $D$ by applying itself to both branches. Exhibit a closed term of type $real \to real$ for which theorem 182.12 becomes false, and identify the step of the proof of lemma 182.11 that breaks. Then state a restriction on the guard under which the proof goes through again, and prove the restricted statement.

Referenced from 3 locations

Differentiable Semantics and Forward-Mode Automatic Differentiation

Exercise 182.7 ¶

★★☆ Prove that for first-order $τ$ and $σ$ the relation $S_{τ \to σ}$ determines its second component uniquely: if $(F, G)$ and $(F, G^{'})$ are both in $S_{real \to real}$ then $G = G^{'}$ on the curves that occur. Then exhibit two distinct transforms of one term of type $(real \to real) \to real$ that are both related to it, showing that uniqueness fails at second order.

Referenced from 2 locations

Differentiable Semantics and Forward-Mode Automatic Differentiation

Exercise 182.8 ¶

★★★ Practical project.forward-tangent-macro Implement in Agda or Kappa the language of definition 182.4, its evaluator, and the macro $D$ of definition 182.6. Represent terms with typed de Bruijn indices so that lemma 182.7 is enforced by construction, and provide the operations $\underset{―}{c}, +, *, ς$ with their derivative terms.

The invariant to maintain is the one used in the proof of lemma 182.11: at every operation node the transformed program computes the pair whose components are $op (\vec{x})$ and $\sum_{i} \partial_{i} op (\vec{x}) * x_{i}^{'}$ , and no other node inspects a tangent component. The concrete result is a function taking a term $t$ with $n$ real inputs, a point $a$ , and a seed vector, and returning the pair produced by evaluating $D t$ .

Acceptance test. For $t = x_{1} * x_{2} + x_{1}$ at $a = (3, 5)$ with seeds $(1, 0)$ and $(0, 1)$ , the tool returns $(18, 6)$ and $(18, 3)$ ; for the higher-order term of example 182.9 at $a = 2$ with seed $1$ it returns $(16, 32)$ ; for the twice-transformed term $D (D (x * x))$ the second-order component is $2$ at every point; and the term of example 182.15, written in the frozen language by applying $D$ twice rather than by a run-time operator, returns $1$ rather than the $2$ of the confused evaluation. A mutation that drops the summation in the operation clause, keeping only the $i = 1$ summand, must fail the first test on the seed $(0, 1)$ .

The program evaluates finitely many closed terms at finitely many points. It illustrates theorem 182.12 and does not prove it; in particular agreement at the tested points is not evidence about any other point, which is the content of remark 182.3.

Referenced from 3 locations

Differentiable Semantics and Forward-Mode Automatic Differentiation

Bibliographic notes

The source language, the macro, and both correctness theorems are those of Huot, Staton, and Vákár, Higher Order Automatic Differentiation of Higher Order Functions, arXiv:2101.06757, whose Theorems 4.3 and 6.6 are imported as theorem 182.14; definition 182.1 is their equation (2.1) and definition 182.10 is the case $k = R = 1$ of their logical relation. The observation that the argument can be run over ordinary sets for a simple language, without the diffeological axioms, is due to Barthe and coauthors and is recorded in that paper; the proof of lemma 182.11 above takes that route, which is why no diffeological space appears in this chapter’s own theorem. Correctness for typed automatic differentiation in the presence of partial features is treated by Nunes and Vákár under explicit source-language restrictions; none of those extensions is claimed here.

The perturbation-confusion examples of section 182.5 are from Manzyuk, Pearlmutter, Radul, Rush, and Siskind [MPR^+19], whose analysis of the offset operator is reproduced in outline in example 182.16; the one-tag example goes back to Siskind and Pearlmutter. That paper owns no theorem in this chapter: it is used to delimit theorem 182.12, as remark 182.17 states. Blondel and Roulet’s book-length treatment supplies the one-feature-at-a-time example ladder and the modern terminology; the survey [BPRS18] and the course notes [EJ23] supply the numerical background.