circuits-diff
Safe HaskellNone
LanguageGHC2024

Circuit.Diff.RDC

Description

Cartesian reverse differential category structure on Diff.

A Cartesian reverse differential category (Cockett, Cruttwell, Gallagher, Lemay, MacAdam, Plotkin, Pronk, CSL 2020) is a Cartesian left-additive category with a combinator

R[f] : A × B → A

for every morphism f : A → B, satisfying seven coherence axioms [RD.1]– [RD.7]. For Diff the combinator is exactly the bundled pullback:

R[f](a, db) = snd (runDiff f a) db

This module exposes that combinator, the small Cartesian plumbing needed to state the axioms, and value-level checks for all seven axioms. [RD.6] is homogeneity of R[f] in its cotangent argument; [RD.7] is symmetry of mixed partials (Schwarz), checked via the scalar-line Jet tower.

Synopsis

Reverse derivative combinator

rdc :: forall {k} (p :: k) a b. Diff p a b -> (a, b) -> a Source #

Reverse derivative combinator.

For f : Diff p a b, the reverse derivative R[f] : (a, b) -> a maps a point a and an output cotangent db to the input cotangent da.

>>> import NumHask.Algebra.Field qualified as NHField
>>> import Circuit.Diff
>>> let x = Diff (\s -> (s, \db -> db)) :: Diff' Double Double
>>> rdc (NHField.sin x) (0.0, 1.0)
1.0

Cartesian helpers on Diff

fstD :: forall {k} b (p :: k) a. Additive b => Diff p (a, b) a Source #

First projection as a Diff morphism.

sndD :: forall {k} a (p :: k) b. Additive a => Diff p (a, b) b Source #

Second projection as a Diff morphism.

pairD :: forall {k} a (p :: k) b c. Additive a => Diff p a b -> Diff p a c -> Diff p a (b, c) Source #

Pairing of two Diff morphisms with the same source.

forkD :: forall {k} a (p :: k) b. Additive a => Diff p a b -> Diff p a (b, b) Source #

Fork a single morphism into a pair: forkD f = pairD f f.

terminalD :: forall {k} a (p :: k). Additive a => Diff p a () Source #

Unique morphism to the terminal object, returning the zero cotangent.

Axiom checks ([RD.1]–[RD.7])

rdcAdditive :: forall {k} a b (p :: k). (Additive a, Additive b, Fractional a, Ord a, Absolute a, Subtractive a) => a -> Diff p a b -> Diff p a b -> a -> b -> b -> Bool Source #

RD.1
The reverse derivative preserves addition: R[f + g] = R[f] + R[g] and R[0] = 0.

rdcLinear :: forall {k} a b (p :: k). (Additive a, Additive b, Fractional a, Ord a, Absolute a, Subtractive a) => a -> Diff p a b -> a -> b -> b -> b -> Bool Source #

RD.2
The reverse derivative is additive in its second (cotangent) argument: R[f](a, db1 + db2) = R[f](a, db1) + R[f](a, db2) and R[f](a, 0) = 0.

rdcHomogeneous :: forall {k} a (p :: k). (Multiplicative a, Fractional a, Ord a, Absolute a, Subtractive a) => a -> Diff p a a -> a -> a -> a -> Bool Source #

RD.6
The reverse derivative is homogeneous in its cotangent argument: R[f](a, c · db) = c · R[f](a, db).

This formulation restricts to endomorphisms f : A → A so that the scalar c and the input/output cotangents all live in the same carrier.

rdcIdentity :: (Fractional a, Ord a, Absolute a, Subtractive a) => a -> a -> a -> Bool Source #

RD.3
R[id] = π1: the reverse derivative of the identity is the second projection (the cotangent itself).

rdcFst :: (Additive b, Fractional a, Ord a, Absolute a, Subtractive a, Eq b) => a -> (a, b) -> a -> Bool Source #

RD.3
R[π0] = ι0 ∘ π1: the reverse derivative of first projection returns the cotangent in the first component and zero in the second.

rdcSnd :: (Additive a, Fractional a, Ord a, Absolute a, Subtractive a, Eq b) => a -> (a, b) -> b -> Bool Source #

RD.3
R[π1] = ι1 ∘ π1: the reverse derivative of second projection returns zero in the first component and the cotangent in the second.

rdcPairing :: forall {k} a b c (p :: k). (Additive a, Additive b, Additive c, Fractional a, Ord a, Absolute a, Subtractive a) => a -> Diff p a b -> Diff p a c -> a -> (b, c) -> (b, c) -> Bool Source #

RD.4
Reverse derivative of a pairing: R[g](a, (db, dc)) = R[f](a, db) + R[g](a, dc).

rdcTerminal :: (Additive a, Fractional a, Ord a, Absolute a, Subtractive a) => a -> a -> Bool Source #

RD.4
Reverse derivative of the terminal morphism is zero.

rdcChain :: forall {k} a (p :: k) b c. (Fractional a, Ord a, Absolute a, Subtractive a) => a -> Diff p a b -> Diff p b c -> a -> c -> Bool Source #

RD.5
Reverse chain rule: R[g ∘ f](a, dc) = R[f](a, R[g](f a, dc)).

rdcMixedPartials :: (ExpField a, TrigField a, FromInteger a, Fractional a, Ord a, Absolute a, Subtractive a) => a -> (forall b. (ExpField b, TrigField b, FromInteger b) => (b, b) -> b) -> (a, a) -> Bool Source #

RD.7
Symmetry of mixed partials (Schwarz's theorem).

For a scalar field f : A × A → A we compute the two second-order scalar jets obtained by differentiating first with respect to x and then y, and vice-versa, and assert they agree.

The function argument is rank-2 polymorphic so it can be interpreted both at the base carrier a and at the Jet carrier used for the scalar-line Taylor expansion.