2018/11/30 by James Wallbridge
Computer Science · Mathematics · #Advanced Algebra and Logic #Algebra over a field #Category theory #Differential (mechanical device) #Differential algebra #Homotopy and Cohomology in Algebraic Topology #Interpretation (philosophy) #Linear logic #Logic, programming, and type systems #Manifold (fluid mechanics) #Morphism #cs.LO
paper · pdf · doi:10.1017/s0960129520000249
published as Math. Struct. Comp. Sci. 30 (2020) 865-891 · V2, 30 pages
openalex created_date 2018/11/29 · arxiv created 2019/12/28 · openalex publication_date 2020/09/01 · arxiv updated 2021/02/10 · openalex updated_date 2026/08/05
Abstract We prove that the category of vector bundles over a fixed smooth manifold and its corresponding category of convenient modules are models for intuitionistic differential linear logic. The exponential modality is modelled by composing the jet comonad, whose Kleisli category has linear differential operators as morphisms, with the more familiar distributional comonad, whose Kleisli category has smooth maps as morphisms. Combining the two comonads gives a new interpretation of the semantics of differential linear logic where the Kleisli morphisms are smooth local functionals, or equivalently, smooth partial differential operators, and the codereliction map induces the functional derivative. This points towards a logic, and hence a computational theory of non-linear partial differential equations and their solutions based on variational calculus.