Simply-typed Differential and Resource Lambda-Calculus
Date:
The differential λ-calculus augments the λ-calculus with differential operators that mimic the rules of the standard differential calculus. The extension, and an equivalent calculus, the resource λ-calculus, give expression to resource usage of a computation. Bucciarelli et al. have shown that cartesian closed differential categories are models of simply-typed differential λ-theories. This project proves the converse, which is a form of completeness: given a typed differential λ-theory, we construct the “smallest” category in which one can soundly model the theory. Moreover, we show that, under reasonable assumptions, differential λ-theory is the internal language of cartesian closed differential category. Finally, we present the relational model as a cartesian closed differential category and show that it is in- complete.