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