categories: Abstract differential operator

[Frank Atanassow <franka@cs.uu.nl>]

Conor McBride has written a paper [1] in which he argues that, by applying the
familiar rules of symbolic differentiation to a "polynomial" (i.e., generated
from finite sums and tuples) functor F, one obtains a "derivative" functor F'
s.t. sequences of values of type F'(mu F) are one-hole contexts of values of
type mu F (the initial F-algebra).

For example, if FX=1+X^2, the signature of binary trees, then F'X = 2*X and
a sequence over 2*(mu F) can be regarded as a path into a tree, which
also records the subtree on the other side of each choice point.

I'm interested in the semantics of this construction. Does it sound familiar?
Is there a thing resembling differentiation in such a discrete setting?
Any pointers would be appreciated.

[1] Conor McBride. The Derivative of a Regular Type is its Type of One-Hole
    Contexts. Unpublished. http://www.dur.ac.uk/~dcs1ctm

-- 
Frank Atanassow, Information & Computing Sciences, Utrecht University
Padualaan 14, PO Box 80.089, 3508 TB Utrecht, Netherlands
Tel +31 (030) 253-3261 Fax +31 (030) 251-3791