Home What is the Derivative of a Program?
Post
Cancel

What is the Derivative of a Program?

This seems to be a nonsense question, programs discrete objects. It makes about as much sense to ask what is the derivative of a graph or a natural number. However, we often want to ask questions about how a program depends on things. In asymtotic analysis, the time/space complexity of a program is usually approimated by a differentiable function so it makes sense to ask the question: what is rate of change of the run-time as the input increases. For machine learning models with weights we are very accustomed to asking about differential behavior with respect to changes in the weights. For more general programs, is there a way to make sense of small changes in behavior corresponding to small changes in the algorithm?

In a previous post we introduced linear logic which we thought of as a linear (in the sense of linear algebra) version of a Gentzen-style sequent calculus – or equivalently by the Curry-Howard correspondence – of $\lambda$-calculus.

If it makes sense to identifty which programs or proofs are “linear” then surely there should be a way to “linearize” it. This is the idea behind the definitin of the derivative, it should be the “best” linear approximation of the program.

Differential Linear Logic

This post is licensed under CC BY 4.0 by the author.