Flag: a Self-Dual Modality for Non-Commutative Contraction and Duplication in the Category of Coherence Spaces

Christian Retoré
(LIRMM, Univ Montpellier & CNRS)

After reminding what coherences spaces are and how they interpret linear logic, we define a modality "flag" in the category of coherence spaces (or hypercoherences) with two inverse linear (iso)morphisms: "duplication" from (flag A) to ((flag A) < (flag A)) and "contraction" in the opposite direction — where < is the self dual and non-commutative connective known as "before" in pomset logic and known as "seq(ential)" in the deep inference system (S)BV. In addition, as expected, the coherence space A is a retract of its modal image (flag A). This suggests an intuitive interpretation of (flag A) as "repeatedly A" or as "A at any instant" when "before" is given a temporal interpretation. We hope the semantic construction of flag(A) will help to design proof rules for "flag" and we briefly discuss this at the end of the paper.

In Ugo Dal Lago and Valeria de Paiva: Proceedings Second Joint International Workshop on Linearity & Trends in Linear Logic and Applications (Linearity&TLLA 2020), Online, 29-30 June 2020, Electronic Proceedings in Theoretical Computer Science 353, pp. 157–174.
Published: 30th December 2021.

ArXived at: https://dx.doi.org/10.4204/EPTCS.353.8 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org