The sequent calculus of skew monoidal categories

Tarmo Uustalu, Niccolò Veltri, Noam Zeilberger

Research output: Contribution to journalArticlepeer-review

4 Citations (Scopus)
218 Downloads (Pure)

Abstract

Szlachányi's skew monoidal categories are a well-motivated variation of monoidal categories in which the unitors and associator are not required to be natural isomorphisms, but merely natural transformations in a particular direction. We present a sequent calculus for skew monoidal categories, building on the recent formulation by one of the authors of a sequent calculus for the Tamari order (skew semigroup categories). In this calculus, antecedents consist of a stoup (an optional formula) followed by a context (a list of formulae), and the connectives unit and tensor behave like in intuitionistic non-commutative linear logic (the logic of monoidal categories) except that the left rules may only be applied in stoup position. We show the admissibility of two forms cut (stoup cut and context cut), and prove the calculus sound and complete with respect to existence of maps in the free skew monoidal category. We then introduce an equivalence relation on sequent calculus derivations and prove that there is a one-to-one correspondence between equivalence classes of derivations and maps in the free skew monoidal category. Finally, we identify a subcalculus of focused derivations, and establish that it contains exactly one canonical representative from each equivalence class. As an end result, we obtain simple algorithms both for deciding equality of maps in the free skew monoidal category and for enumerating any homset without duplicates, in particular, for deciding whether there is a map. We have formalized this development in the dependently typed programming language Agda.

Original languageEnglish
Pages (from-to)345-370
Number of pages26
JournalElectronic Notes in Theoretical Computer Science
Volume341
DOIs
Publication statusPublished - 1 Dec 2018

Keywords

  • Agda
  • cut admissibility
  • focusing
  • nonstandard sequent forms
  • sequent calculus
  • skew monoidal categories
  • substructural logics

ASJC Scopus subject areas

  • Theoretical Computer Science
  • General Computer Science

Fingerprint

Dive into the research topics of 'The sequent calculus of skew monoidal categories'. Together they form a unique fingerprint.

Cite this