A Logical Account for Linear Partial Differential Equations

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

Talk:Jul 10 14:20 (Session 55E)