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: |