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

TL;DR

This paper introduces a new modality 'flag' in coherence spaces that captures non-commutative contraction and duplication, providing a semantic foundation for temporal and sequential logic interpretations.

Contribution

It defines the 'flag' modality with inverse linear isomorphisms in coherence spaces, enabling non-commutative contraction and duplication, and offers an intuitive temporal interpretation.

Findings

'flag' modality has inverse linear isomorphisms

coherence space A is a retract of 'flag A'

semantic construction aids proof rule design

Abstract

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.