Mackey-complete spaces and power series -- A topological model of Differential Linear Logic

TL;DR

This paper develops a denotational model of Intuitionist Linear Logic using Mackey-complete topological vector spaces and power series, providing a quantitative framework that captures differentiation and Taylor expansion of proofs.

Contribution

It introduces a novel topological model of Differential Linear Logic based on Mackey-complete spaces and power series, extending the interpretation of proofs to include differentiation.

Findings

Interpretation of formulas as Mackey-complete topological vector spaces

Use of power series to model non-linear proofs and differentiation

Proofs satisfy a Taylor expansion decomposition

Abstract

In this paper, we have described a denotational model of Intuitionist Linear Logic which is also a differential category. Formulas are interpreted as Mackey-complete topological vector space and linear proofs are interpreted by bounded linear functions. So as to interpret non-linear proofs of Linear Logic, we have used a notion of power series between Mackey-complete spaces, generalizing the notion of entire functions in C. Finally, we have obtained a quantitative model of Intuitionist Differential Linear Logic, where the syntactic differentiation correspond to the usual one and where the interpretations of proofs satisfy a Taylor expansion decomposition.