Derivative of a Container

The notion of derivatives in calculus extends to containers in a surprising way preserving chain-rule and other properties.

Idea

Given a container, we might want to talk about the one-hole contexts of that container. This can be understood as a container with some datatype, where one position is may be occupied by a ‘hole’.

Definition

Given a container $F=S◁P$ its derivative is a container $F^{\prime }$ such that $F$ is

$$\begin{array}{rl}\partial FX& =\Sigma s:S.\Sigma p:Ps.(Ps-p)\to X\\ & =((\Sigma s:S.Ps)◁(Ps-p))X\end{array}$$

So in general,

$$\partial F=(\Sigma s:S.Ps)◁(Ps-p)$$

In cases where $Ps$ is emtpy then that shape is removed.

Partial Derivative

Given an $n$-ary container $S◁P$, Let $(S◁P)X:{\mathrm{Set}}^n\to \mathrm{Set}$; $i:[n]$,

$$\begin{array}{rl}{\partial }_k(S◁P)X& =\sum _{s:S}{\partial }_k{X}^{Pks}\prod _{i:[n]-k}{X}^{Pis}\\ & =\sum _{s:S}\left(\sum _{p:Pks}{X}^{Pks-p}\right)\prod _{i:[n]-k}{X}^{Pis}\end{array}$$

Derivative of a Fixpoint

Let $S◁P$ be an $[n]$-ary container. ${\mu }_k(S◁P):{\mathrm{Set}}^{[n]-k}\to \mathrm{Set}$

Examples

• $\partial (0◁0)=0◁0$ — empty container
• $\partial (C◁0)=0◁0$ — constant container has no place to insert a hole so it gets replaced with an empty container.
• $\partial (1◁1)=1◁0$ becomes the constant container $1$.
• $\partial X^{n+1}=(n+1)X^n$
• $\partial (F+G)=\partial F+\partial G$
• $\partial (F\cdot G)=\partial F\cdot G+G\cdot F$
• $\partial (\mu F)\cong (\partial F\cdot \mu F+\mu F)$
• $\partial (\mu F)\cong \partial (\mu F\circ F)=\partial F\cdot (\partial (\mu F)\circ F)$
• $\partial (G\circ F)=\partial F\cdot (\partial G\circ F)$

References

gylterud2011-symmetric-containers-thesis abbott2005-container-derivative