| @amuresan, here is an attempt to answer your question, from a non-expert: --- In a variety of problems, one needs to compute minimum or maximum of some numeric function.
Later, the result of the above, is used to construct 'optimal' path, 'optimal solution'/etc. As an example, if one is writing a database optimization (eg what query path to take will (likely), take less time, or less resources). Or a distributed task scheduled... Min/Max of a computation is also a function (represented as a derivative). So to compute a derivative, we have to take a function that can be written in Math notation (symbolic differentiation is needed ), or as function in some programming language (automatic differentiation is needed) The transformation program (the one that finds the derivative of another computation express in some programming language) is what this paper is covering. How do we reason about these transformations? are they correct ?, how much memory will they need to store intermediate states? can some of these states be collapsed without negatively affecting results? So this paper is coming up with formalisms akin to operational calculus to describe these programs, and provides apparatus In their conclusion paragraph: "....
In this paper we presented a theoretical model for differentiable programming. Throughout the course of the paper we have shown the model to be a complete description of differentiable programming. Furthermore, the innate algebraic structure of the framework supplements the descriptive power of a language with the ability to reason about the programs it implements, by way of operational calculus. We believe operational calculus has a place in the evolution of computer science, where languages are to be endowed with algebraic constructs that hold power over analytic properties of the programs they implement.
…" Also, I think, that methods to formally describe classes of programs, are really good and useful. I am sure, some day, methods like this, and the whole machinery of Category theory will allow us to construct with 'correctness guarantees' and reason about -- not just numeric computations, but also the typical 'data donkey' transformations between data stores/message queues that are so often implemented by hand in the enterprises. |