Linear Läuchli semantics

DOI10.1016/0168-0072(95)00017-8MaRDI QIDQ1919529zbMATH OpenOpenAlexFDO

Publication date 11 February 1997

Published in Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/0168-0072(95)00017-8

dinatural transformations full completeness functorial polymorphism group actions Hopf algebras linear analogue of Läuchli's semantics for intuitionistic logic logical relations multiplicative linear logic noncommutative logic parametricity

Mathematics Subject Classification ID

Subsystems of classical logic (including intuitionistic logic) (03B20) Cut-elimination and normal-form theorems (03F05) Categorical logic, topoi (03G30)

Review text

We introduce a linear analogue of Läuchli's semantics for intuitionistic logic. In fact, our result is a strengthening of Läuchli's work to the level of proofs, rather than provability. This is obtained by considering continuous actions of the additive group of integers on a category of topological vector spaces. The semantics, based on functorial polymorphism, consists of dinatural transformations which are equivariant with respect to all such actions. Such dinatural transformations are called uniform. To any sequent in Multiplicative Linear Logic (MLL), we associate a vector space of ``diadditive uniform transformations. We then show that this space is generated by denotations of cut-free proofs of the sequent in the theory MLL\(+\)MIX. Thus we obtain a full completeness theorem in the sense of Abramsky and Jagadeesan, although our result differs from theirs in the use of dinatural transformations. As corollaries, we show that these dinatural transformations compose, and obtain a conservativity result: diadditive dinatural transformations which are uniform with respect to actions of the additive group of integers are also uniform with respect to the actions of arbitrary cocommutative Hopf algebras. Finally, we discuss several possible extensions of this work to noncommutative logic. It is well known that the intuitionistic version of Läuchli's semantics is a special case of the theory of logical relations, due to Plotkin and Statman. Thus, our work can also be viewed as a first step towards developing a theory of logical relations for linear logic and concurrency.

Recommendations

Cites work

Cited in

(24)

This page was built for publication: Linear Läuchli semantics

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1919529)