Conal Elliott

Why care about derivatives?

Derivatives are useful in a variety of application areas, including root-finding, optimization, curve and surface tessellation, and computation of surface normals for 3D rendering. Considering the usefulness of derivatives, it is worthwhile to find software methods that are

• simple (to implement and verify),
• convenient,
• accurate,
• efficient, and
• general.

Numeric approximation

One differentiation method numeric approximation, using simple finite differences. This method is based on the definition of (scalar) derivative:

The left-hand side reads "the derivative of f at x".

To approximate the derivative, use

for a small value of h. While very simple, this method is often inaccurate, due to choosing either too large or too small a value for h. (Small values of h lead to rounding errors.) More sophisticated variations improve accuracy while sacrificing simplicity.

Symbolic differentiation

A second method is symbolic differentiation. Instead of using the definition of deriv directly, the symbolic method uses a collection of rules, such as those below:

deriv (u + v)   ≡ deriv u + deriv v
deriv (u * v)   ≡ deriv v * u + deriv u * v
deriv (- u)     ≡ - deriv u
deriv (exp u)   ≡ deriv u * exp u
deriv (log u)   ≡ deriv u / u
deriv (sqrt u)  ≡ deriv u / (2 * sqrt u)
deriv (sin u)   ≡ deriv u * cos u
deriv (cos u)   ≡ deriv u * (- sin u)
deriv (asin u)  ≡ deriv u/(sqrt (1 - u^2))
deriv (acos u)  ≡ - deriv u/(sqrt (1 - u^2))
deriv (atan u)  ≡ deriv u / (u^2 + 1)
deriv (sinh u)  ≡ deriv u * cosh u
deriv (cosh u)  ≡ deriv u * sinh u
deriv (asinh u) ≡ deriv u / (sqrt (u^2 + 1))
deriv (acosh u) ≡ - deriv u / (sqrt (u^2 - 1))
deriv (atanh u) ≡ deriv u / (1 - u^2)

There are two main drawbacks to the symbolic approach to differentiation.

• As a symbolic method, it requires access to and transformation of source code, and placing restrictions on that source code.
• Implementations tend to be quite expensive and in particular perform redundant computation. (I wonder if this latter criticism is a straw man argument. Are symbolic methods necessarily expensive or just when implemented naïvely? For instance, can simply memoized symbolic differentiation be nearly as cheap as AD?)

A model for AD

I'm pretty sure AD has something to do with calculating a function's values and derivative values simultaneously, so I'll start there.

withD ∷ ⋯ ⇒ (a → a) → (a → D a)
withD f x = D (f x) (deriv f x)

Or, in point-free form,

withD f = liftA2 D f (deriv f)

Since, on functions,

liftA2 h f g = λ x → h (f x) (g x)

We don't have an implementation of deriv, so this definition of withD will serve as a specification, not an implementation.

If AD is structured as type class instances, then I'd want there to be a compelling interpretation function that is faithful to each of those classes, as in the principle of type class morphisms, which is to say that the interpretation of each method corresponds to the same method for the interpretation.

For AD, the interpretation function is withD. It's turned around this time (mapping to instead of from our type), as is sometimes the case. The Num, Fractional, and Floating morphisms provide the specifications of the instances:

withD (u + v) ≡ withD u + withD v
withD (u * v) ≡ withD u * withD v
withD (sin u) ≡ sin (withD u)
⋯

Note here that the methods on the left are on a → a, and on the right are on a → D a.

These (morphism) properties exactly define correctness of any implementation of AD, answering my first question:

What does it mean, independently of implementation?

Addition

Here is the addition specification:

withD (u + v) ≡ withD u + withD v

Start with the left-hand side:

   withD (u + v)
≡   {- def of withD -}
   liftA2 D (u + v) (deriv (u + v))
≡   {- deriv rule for (+) -}
   liftA2 D (u + v) (deriv u + deriv v)
≡   {- liftA2 on functions -}
   λ x → D ((u + v) x) ((deriv u + deriv v) x)
≡   {- (+) on functions -}
   λ x → D (u x + v x) (deriv u x + deriv v x)

Then start over with the right-hand side:

   withD u + withD v
≡   {- (+) on functions -}
   λ x → withD u x + withD v x
≡   {- def of withD -}
   λ x → D (u x) (deriv u x) + D (v x) (deriv v x)

We need a definition of (+) on D that makes these two final forms equal, i.e.,

   λ x → D (u x + v x) (deriv u x + deriv v x)
≡
   λ x → D (u x) (deriv u x) + D (v x) (deriv v x)

An easy choice is

D a a' + D b b' = D (a + b) (a' + b')

This definition provides the missing link and that completes the proof that

withD (u + v) ≡ withD u + withD v

Multiplication

The specification:

withD (u * v) ≡ withD u * withD v

Reason similarly to the addition case. Begin with the left hand side:

   withD (u * v)
≡   {- def of withD -}
   liftA2 D (u * v) (deriv (u * v))
≡   {- deriv rule for (*) -}
   liftA2 D (u * v) (deriv u * v + deriv v * u)
≡   {- liftA2 on functions -}
   λ x → D ((u * v) x) ((deriv u * v + deriv v * u) x)
≡   {- (*) and (+) on functions -}
   λ x → D (u x * v x) (deriv u x * v x + * deriv v x * u x)

Then start over with the right-hand side:

   withD u * withD v
≡   {- (*) on functions -}
   λ x → withD u x * withD v x
≡   {- def of withD -}
   λ x → D (u x) (deriv u x) * D (v x) (deriv v x)

Sufficient definition:

D a a' * D b b' = D (a + b) (a' * b + b' * a)

Sine

Specification:

withD (sin u) ≡ sin (withD u)

Begin with the left hand side:

   withD (sin u)
≡   {- def of withD -}
   liftA2 D (sin u) (deriv (sin u))
≡   {- deriv rule for sin -}
   liftA2 D (sin u) (deriv u * cos u)
≡   {- liftA2 on functions -}
   λ x → D ((sin u) x) ((deriv u * cos u) x)
≡   {- sin, (*) and cos on functions -}
   λ x → D (sin (u x)) (deriv u x * cos (u x))

Then start over with the right-hand side:

   sin (withD u)
≡   {- sin on functions -}
   λ x → sin (withD u x)
≡   {- def of withD -}
   λ x → sin (D (u x) (deriv u x))

Sufficient definition:

sin (D a a') = D (sin a) (a' * cos a)

Or, using the chain rule operator,

sin = sin >-< cos

The whole implementation can be derived in exactly this style, answering my second question:

How does the implementation and its correctness flow gracefully from that meaning?

Addition

Left-hand side:

   withD (u + v)
≡   {- def of withD -}
   liftA2 D (u + v) (withD (deriv (u + v)))
≡   {- deriv rule for (+) -}
   liftA2 D (u + v) (withD (deriv u + deriv v))
≡   {- (fixed-point) induction withD and (+) -}
   liftA2 D (u + v) (withD (deriv u) + withD (deriv v))
≡   {- def of liftA2 and (+) on functions -}
   λ x → D (u x + v x) (withD (deriv u) x + withD (deriv v) x)

Right-hand side:

   withD u + withD v
≡   {- (+) on functions -}
   λ x → withD u x + withD v x
≡   {- def of withD -}
   λ x → D (u x) (withD (deriv u x)) + D (v x) (withD (deriv v x))

Again, we need a definition of (+) on D that makes the LHS and RHS final forms equal, i.e.,

   λ x → D (u x + v x) (withD (deriv u) x + with (deriv v) x)
≡
   λ x → D (u x) (withD (deriv u) x) + D (v x) (withD (deriv v) x)

Again, an easy choice is

D a a' + D b b' = D (a + b) (a' + b')

Multiplication

Left-hand side:

   withD (u * v)
≡   {- def of withD -}
   liftA2 D (u * v) (withD (deriv (u * v)))
≡   {- deriv rule for (*) -}
   liftA2 D (u * v) (withD (deriv u * v + deriv v * u))
≡   {- induction for withD/(+) -}
   liftA2 D (u * v) (withD (deriv u * v) + withD (deriv v * u))
≡   {- induction for withD/(*) -}
   liftA2 D (u * v) (withD (deriv u) * withD v + withD (deriv v) * withD u)
≡   {- liftA2, (*), (+) on functions -}
   λ x → liftA2 D (u x * v x) (withD (deriv u) x * withD v x + withD (deriv v) x * withD u x)

Right-hand side:

   withD u * withD v
≡   {- def of withD -}
   liftA2 D u (withD (deriv u)) * liftA2 D v (withD (deriv v))
≡   {- liftA2 and (*) on functions -}
   λ x → D (u x) (withD (deriv u) x) * D (v x) (withD (deriv v) x)

A sufficient definition:

a@(D a0 a') * b@(D b0 b') = D (a0 + b0) (a' * b + b' * a)

Because

withD u x ≡ D (u x) (withD (deriv u) x)

withD v x ≡ D (v x) (withD (deriv v) x)

Sine

Left-hand side:

   withD (sin u)
≡   {- def of withD -}
   liftA2 D (sin u) (withD (deriv (sin u)))
≡   {- deriv rule for sin -}
   liftA2 D (sin u) (withD (deriv u * cos u))
≡   {- induction for withD/(*) -}
   liftA2 D (sin u) (withD (deriv u) * withD (cos u))
≡   {- induction for withD/cos -}
   liftA2 D (sin u) (withD (deriv u) * cos (withD u))
≡   {- liftA2, sin, cos and (*) on functions -}
   λ x → D (sin (u x)) (withD (deriv u) x * cos (withD u x))

Right-hand side:

   sin (withD u)
≡   {- def of withD -}
   sin (liftA2 D u (withD (deriv u)))
≡   {- liftA2 and sin on functions -}
   λ x → sin (D (u x) (withD (deriv u) x))

To make the LHS and RHS final forms equal, define

sin a@(D a0 a') ≡ D (sin a0) (a' * cos a)