Author: Marie Kerjean
Paper Information
| Title: | A Logical Account for Linear Partial Differential Equations |
| Authors: | Marie Kerjean |
| Proceedings: | LICS PDF files |
| Editors: | Anuj Dawar and Erich Grädel |
| Keywords: | Differential Linear Logic, Functional Analysis, Differential Equations, Categorical Semantics |
| Abstract: | ABSTRACT. Differential Linear Logic (DiLL), introduced by Ehrhard and Regnier, extends linear logic with a notion of linear approximation of proofs. While DiLL is a classical logic, classical models of it in which this notion of differentiation corresponds to the usual one of functional analysis were missing. We solve this issue by constructing a model, without higher order, based on nuclear topological vector spaces and distributions with compact support. This interpretation sheds a new light on the rules of DiLL as we are able to understand them as the computational steps for the resolution of Linear Partial Differential Equations. We thus introduce D-DiLL, a deterministic refinement of DiLL with a D-exponential, for which we exhibit a cut-elimination procedure, and a categorical semantics. We recover the rules of DiLL as a special case. For any D Linear Partial Differential operator with constant coefficient, we construct a model of D-DiLL where the D-exponential represent the space of distributions on spaces of functions f such that Dg=f, and where cut-elimination resolves the equation, that is computes g from f. |
| Pages: | 10 |
| Talk: | Jul 10 14:20 (Session 55E) |
| Paper: | ![]() |
