#
Models of Linear Logic based on the Schwartz $\varepsilon$-product

##
Yoann Dabrowski and Marie Kerjean

From the interpretation of Linear Logic multiplicative disjunction as
the epsilon product defined by Laurent Schwartz, we construct several
models of Differential Linear Logic based on the usual mathematical
notions of smooth maps. This improves on previous results by Blute,
Ehrhard and Tasson based on convenient smoothness where only
intuitionist models were built. We isolate a completeness condition,
called k-quasi-completeness, and an associated notion which is stable
under duality called k-reflexivity, allowing for a star-autonomous
category of k-reflexive spaces in which the dual of the tensor product
is the reflexive version of the epsilon-product. We adapt Meise's
definition of smooth maps into a first model of Differential Linear
Logic, made of k-reflexive spaces. We also build two new models of
Linear Logic with conveniently smooth maps, on categories made
respectively of Mackey-complete Schwartz spaces and Mackey-complete
Nuclear Spaces (with extra reflexivity conditions). Varying slightly
the notion of smoothness, one also recovers models of DiLL on the same
star-autonomous categories. Throughout the article, we work within the
setting of Dialogue categories where the tensor product is exactly the
epsilon-product (without reflexivization).

Keywords:
Topological vector spaces, $\ast$-autonomous and dialogue categories,
differential linear logic

2010 MSC:
03B47, 18C50, 18D15, 46A20, 46M05, 46E50, 68Q55

*Theory and Applications of Categories,*
Vol. 34, 2019,
No. 45, pp 1440-1525.

Published 2019-12-18.

http://www.tac.mta.ca/tac/volumes/34/45/34-45.pdf

TAC Home