Hostname: page-component-cd9895bd7-dzt6s Total loading time: 0 Render date: 2024-12-23T08:15:39.371Z Has data issue: false hasContentIssue false
  • English
  • Français

Jets and differential linear logic

Published online by Cambridge University Press:  24 November 2020

James Wallbridge Open the ORCID record for James Wallbridge [Opens in a new window]
Get access Rights & Permissions [Opens in a new window]

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.

Keywords

Linear logicvector bundlesdifferential operatorsdifferential categories
Type
Paper
Information
Mathematical Structures in Computer Science , Volume 30 , Issue 8 , September 2020 , pp. 865 - 891
Check for updates
Copyright
© The Author(s), 2020. Published by Cambridge University Press

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

Adámek, J. and Rosický, J. (1994). Locally Presentable and Accessible Categories, Cambridge University Press, Cambridge, UK.CrossRefGoogle Scholar
Artin, M., Grothendieck, A. and Verdier, J. (1972). SGA 4, Théorie des topos et cohomologie étale des schémas, Lecture Notes in Mathematics 269, Springer-Verlag, Berlin.CrossRefGoogle Scholar
Barr, M. (1991). ∗-autonomous categories and linear logic. Mathematical Structures in Computer Science 1 (2) 159–178.CrossRefGoogle Scholar
Beck, J. (1969). Distributive laws. In: Seminar on Triples and Categorical Homology Theory, Springer, 119–140.CrossRefGoogle Scholar
Benton, P. N. (1994). A mixed linear and non-linear logic: Proofs, terms and models. In: International Workshop on Computer Science Logic, Springer, 121–135.Google Scholar
Bierman, G. M. (1995). What is a categorical model of intuitionistic linear logic? In: International Conference on Typed Lambda Calculi and Applications, Springer, 78–93.CrossRefGoogle Scholar
Blute, R., Cockett, J. R. B. and Seely, R. A. (2015). Cartesian differential storage categories. Theory and Applications of Categories 30 (18) 620–686.Google Scholar
Blute, R., Ehrhard, T. and Tasson, C. (2012). A convenient differential category. Cah. Topol. Géom. Différ. Catég 53 (3), 211–232.Google Scholar
Blute, R. F., Cockett, J. R. B., Lemay, J.-S. P. and Seely, R. A. G. (2020). Differential categories revisited. Applied Categorical Structures 28 171–235.CrossRefGoogle Scholar
Blute, R. F., Cockett, J. R. B. and Seely, R. A. (2006). Differential categories. Mathematical Structures in Computer Science 16 (6) 1049–1083.CrossRefGoogle Scholar
Blute, R. F., Cockett, J. R. B. and Seely, R. A. (2009). Cartesian differential categories. Theory and Applications of Categories 22 (23) 622–672.Google Scholar
Bucciarelli, A., Ehrhard, T. and Manzonetto, G. (2010). Categorical models for simply typed resource calculi. Electronic Notes in Theoretical Computer Science 265 213–230.CrossRefGoogle Scholar
Clift, J. and Murfet, D. (2020). Cofree coalgebras and differential linear logic. Mathematical Structures in Computer Science 30 (4) 416–457.CrossRefGoogle Scholar
Cockett, J. R. B. and Lemay, J.-S. (2019). Integral categories and calculus categories. Mathematical Structures in Computer Science 29 (2), 243–308.CrossRefGoogle Scholar
Cockett, R., Cruttwell, G., Gallagher, J., Lemay, J.-S. P., MacAdam, B., Plotkin, G. and Pronk, D. (2020). Reverse derivative categories. In: 28th EACSL Annual Conference on Computer Science Logic (CSL 2020).Google Scholar
Costello, K. and Gwilliam, O. (2016). Factorization Algebras in Quantum Field Theory, vol. 1, Cambridge University Press, Cambridge, UK.Google Scholar
Ehrhard, T. (2002). On Köthe sequence spaces and linear logic. Mathematical Structures in Computer Science 12 (5) 579–623.CrossRefGoogle Scholar
Ehrhard, T. (2005). Finiteness spaces. Mathematical Structures in Computer Science 15 (4) 615–646.CrossRefGoogle Scholar
Ehrhard, T. (2018). An introduction to differential linear logic: Proof-nets, models and antiderivatives. Mathematical Structures in Computer Science 28 (7) 995–1060.CrossRefGoogle Scholar
Ehrhard, T. and Regnier, L. (2003). The differential lambda-calculus. Theoretical Computer Science 309 1–41.CrossRefGoogle Scholar
Ehrhard, T. and Regnier, L. (2008). Uniformity and the taylor expansion of ordinary lambda-terms. Theoretical Computer Science 403 (2–3) 347–372.CrossRefGoogle Scholar
Frölicher, A. and Kriegl, A. (1988). Linear Spaces and Differentiation Theory , Pure and Applied Mathematics, Wiley, Chichester.Google Scholar
Girard, J.-Y. (1987). Linear logic. Theoretical Computer Science 50 (1) 1–101.CrossRefGoogle Scholar
Girard, J.-Y. (1999). Coherent banach spaces: A continuous denotational semantics. Theoretical Computer Science 227 (1–2) 275–297.CrossRefGoogle Scholar
Graves, A., Wayne, G., Reynolds, M., Harley, T., Danihelka, I., Grabska-Barwińska, A., Colmenarejo, S. G., Grefenstette, E., Ramalho, T., Agapiou, J., Puigdoménech Badia, A., Hermann, K. M., Zwols, Y., Ostrovski, G., Cain, A., King, H., Summerfield, C., Blunsom, P., Kavukcuoglu, K., Hassabis, D. (2016). Hybrid computing using a neural network with dynamic external memory. Nature 538 471–476.CrossRefGoogle ScholarPubMed
Grothendieck, A. (1960). Technique de descente et théoremes d’existence en géométrie algébrique. II. le théoreme d’existence en théorie formelle des modules. Séminaire Bourbaki 5 369–390.Google Scholar
Güneysu, B. and Pflaum, M. J. (2017). The profinite dimensional manifold structure of formal solution spaces of formally integrable pdes. Symmetry, Integrability and Geometry: Methods and Applications 13 1–44.Google Scholar
Hogbe-Nlend, H. (1977). Bornologies and Functional Analysis, Mathematics Studies 26, North-Holland, Amsterdam.Google Scholar
Hyland, M. and De Paiva, V. (1993). Full intuitionistic linear logic. Annals of Pure and Applied Logic 64 (3) 273–291.CrossRefGoogle Scholar
Kashiwara, M. (2003). D-Modules and Microlocal Calculus , Translations of Mathematical Monographs 217, American Mathematical Society, Providence, Rhode Island.Google Scholar
Kerjean, M. (2018). A logical account for linear partial differential equations. In: Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, ACM, 589–598.CrossRefGoogle Scholar
Kerjean, M. and Tasson, C. (2018). Mackey-complete spaces and power series–a topological model of differential linear logic. Mathematical Structures in Computer Science 28 (4) 472–507.CrossRefGoogle Scholar
Khavkine, I. and Schreiber, U. (2017). Synthetic geometry of differential equations: I. jets and comonad structure. arXiv preprint arXiv:1701.06238.Google Scholar
Kriegl, A. and Michor, P. W. (1997). The Convenient Setting of Global Analysis, Mathematical Surveys and Monographs 53, American Mathematical Society.CrossRefGoogle Scholar
Lagaris, I. E., Likas, A. and Fotiadis, D. I. (1998). Artificial neural networks for solving ordinary and partial differential equations. IEEE Transactions on Neural Networks 9 (5) 987–1000.CrossRefGoogle ScholarPubMed
Libermann, P. (1964). Sur la géométrie des prolongements des espaces fibrés vectoriels. Annales de l’institut Fourier 14 (1) 145–172.CrossRefGoogle Scholar
Long, Z., Lu, Y. and Dong, B. (2019). Pde-net 2.0: Learning pdes from data with a numeric-symbolic hybrid deep network. Journal of Computational Physics 399 108925.CrossRefGoogle Scholar
Mac Lane, S. (1971). Categories for the Working Mathematician , Graduate Texts in Mathematics 5, Springer-Verlag, New York.Google Scholar
Mackey, G. W. (1945). On infinite-dimensional linear spaces. Transactions of the American Mathematical Society 57 155–207.CrossRefGoogle Scholar
Manzonetto, G. (2012). What is a categorical model of the differential and the resource λ-calculi? Mathematical Structures in Computer Science 22 (3) 451–520.CrossRefGoogle Scholar
Marvan, M. (1987). A note on the category of partial differential equations. In: Differential Geometry and Its Applications, Proceedings of International Conference, Proc. Conf. Brno, 1986, J.E. Purkynĕ University, Brno 235–244.Google Scholar
Melliès, P.-A. (2009). Categorical semantics of linear logic. Panoramas et Syntheses 27 15–215.Google Scholar
Mesablishvili, B. (2014). Descent in locally presentable categories. Applied Categorical Structures 22 (5–6) 715–726.CrossRefGoogle Scholar
Olver, P. J. (1986). Applications of Lie Groups to Differential Equations , Graduate Texts in Mathematics 107, Springer-Verlag, New York.Google Scholar
Pham, H., Guan, M. Y., Zoph, B., Le, Q. V. and Dean, J. (2018). Efficient neural architecture search via parameter sharing. In: Proceedings of the 35th International Conference on Machine Learning.Google Scholar
Pommaret, J.-F. and Lichnerowicz, A. (1978). Systems of Partial Differential Equations and Lie Pseudogroups, Gordon and Breach Science Publishers, New York.Google Scholar
Saunders, D. (1989). The Geometry of Jet Bundles , London Mathematical Society Lecture Note Series 142, Cambridge University Press, Cambridge, UK.Google Scholar
Serre, J.-P. (1955). Faisceaux algébriques cohérents. Annals of Mathematics, 61 197–278.CrossRefGoogle Scholar
Vinogradov, A. (1980). Geometrija nelinejnych differencialnych uravnenij. Probl. Geom. II, Itogi Nauk. Tech.Google Scholar
Wallbridge, J. (2015). Homotopy theory in a quasi-abelian category. arXiv preprint arXiv:1510.04055.Google Scholar
Weinan, E., Han, J. and Jentzen, A. (2017). Deep learning-based numerical methods for high-dimensional parabolic partial differential equations and backward stochastic differential equations. Communications in Mathematics and Statistics 5 (4) 349–380.Google Scholar
Zoph, B. and Le, Q. V. (2017). Neural architecture search with reinforcement learning. In: Proceedings of the International Conference on Learning Representations.Google Scholar