Proof Theory of Partially Normal Skew Monoidal Categories

The free skew monoidal category $\mathbf{Fsk}(\mathsf{At})$ over a set $\mathsf{At}$ (of atoms) can be viewed as a deductive system, which we refer to as the skew monoidal categorical calculus.

Objects of $\mathbf{Fsk}(\mathsf{At})$ are called formulae, and are inductively generated as follows: a formula is either an element $X$ of $\mathsf{At}$ (an atom); $\mathsf{I}$; or $A\otimes B$ where $A$, $B$ are formulae. We write $\mathsf{Fma}$ for the set of formulae.

Maps between two formulae $A$ and $C$ are derivations of (singleton-antecedent, singleton-succedent) sequents $A\Longrightarrow C$, constructed using the following inference rules:

and identified up to the congruence $\doteq$ induced by the equations:

In the term notation for derivations, we write $g\circ f$ for $\mathsf{comp}\,f\,g$ to agree with the standard categorical notation.

Mac Lane’s coherence theorem [19] says that, in the free monoidal category, there is exactly one map $A\Longrightarrow B$ if the formulae $A$ and $B$ have the same frontier of atoms and no such map otherwise.

For the free skew monoidal category, this does not hold. We have pairs of formulae that have the same frontier of atoms but no maps between them or multiple maps. There are no maps $X\Longrightarrow\mathsf{I}\otimes X$, no maps $X\otimes\mathsf{I}\Longrightarrow X$ and no maps $X\otimes(Y\otimes Z)\Longrightarrow(X\otimes Y)\otimes Z$. At the same time, we have two maps $\mathsf{id}\not\doteq\alpha\circ\rho\otimes\lambda:X\otimes(\mathsf{I}\otimes Y)\Longrightarrow X\otimes(\mathsf{I}\otimes Y)$ and two maps $\mathsf{id}\not\doteq\rho\otimes\lambda\circ\alpha:(X\otimes\mathsf{I})\otimes Y\Longrightarrow(X\otimes\mathsf{I})\otimes Y$.

In [24], we showed that the free skew monoidal category $\mathbf{Fsk}(\mathsf{At})$ admits an equivalent presentation as a sequent calculus. In the latter, sequents are triples $S\mid\Gamma\longrightarrow C$. The antecedent is a pair of a stoup $S$ together with a context $\Gamma$, while the succedent $C$ is a single formula. A stoup is an optional formula, meaning that it can either be empty (written ${-}$) or contain a single formula. A context is a list of formulae. For the empty list, we usually just leave a space, but where necessary for readability, we write $()$. Derivations in the sequent calculus are inductively generated by these inference rules:

($\mathsf{pass}$ for ‘passivate’, $\mathsf{L}$, $\mathsf{R}$ for introduction on the left (in the stoup) resp. right) and identified up to the congruence $\circeq$ induced by the equations:

Although these rules look very similar to the rules of the $\mathsf{I}$, $\otimes$ fragment of intuitionistic non-commutative linear logic [1] (the sequent calculus describing the free monoidal category)—in particular, there is no left exchange rule, weakening or contraction—, there are two crucial differences.

• •

  The left rules $\mathsf{I}\mathsf{L}$ and $\otimes\mathsf{L}$ are restricted to apply only to the formula within the stoup (in the conclusion-first reading of these rules). This restriction was also present in Zeilberger’s sequent calculus for the Tamari order [27]. In this calculus, it is possible to derive sequents corresponding to the right unitor $\rho:A\Longrightarrow A\otimes\mathsf{I}$ and the associator $\alpha:(A\otimes B)\otimes C\Longrightarrow A\otimes(B\otimes C)$:

  $$\small A\mid~{}\longrightarrow A\otimes\mathsf{I}\lx@proof@logical@and A\mid~{}\longrightarrow A{-}\mid~{}\longrightarrow\mathsf{I}\qquad(A\otimes B)\otimes C\mid~{}\longrightarrow A\otimes(B\otimes C)A\otimes B\mid C\longrightarrow A\otimes(B\otimes C)A\mid B,C\longrightarrow A\otimes(B\otimes C)\lx@proof@logical@and A\mid~{}\longrightarrow A{-}\mid B,C\longrightarrow B\otimes CB\mid C\longrightarrow B\otimes C\lx@proof@logical@and B\mid~{}\longrightarrow B{-}\mid C\longrightarrow CC\mid~{}\longrightarrow C$$

  On the other hand, since $\mathsf{I}\mathsf{L}$ and $\otimes\mathsf{L}$ only act on the formula in the stoup, there is no way of deriving sequents corresponding to inverses of $\rho$ and $\alpha$ for atomic $A$ resp. $A$, $B$, $C$.

• •

  The stoup is allowed to be empty, permitting a distinction between antecedents of the form $A\mid\Gamma$ (with $A$ inside the stoup) and antecedents of the form ${-}\mid A,\Gamma$ (with $A$ outside the stoup). This distinction plays an important role in the right rule $\otimes\mathsf{R}$, which sends the formula in the stoup, when it is present, to the first premise. In this calculus, it is possible to derive a sequent corresponding to the left unitor $\lambda:\mathsf{I}\otimes A\Longrightarrow A$:

  $$\small\mathsf{I}\otimes A\mid~{}\longrightarrow A\mathsf{I}\mid A\longrightarrow A{-}\mid A\longrightarrow AA\mid~{}\longrightarrow A$$

  On the other hand, since $\otimes\mathsf{R}$ always send the formula in the stoup to the first premise, it is not possible to derive a sequent corresponding to the inverse of $\lambda$ for atomic $A$.

There are no primitive cut rules in this sequent calculus, but two forms of cut are admissible:

Sequent calculus derivations can be turned into categorical calculus derivations by means of a function $\mathsf{sound}:S\mid\Gamma\longrightarrow C\to\llbracket S\mid\Gamma\rrbracket\Longrightarrow C$, where the interpretation of an antecedent as a formula $\llbracket S\mid\Gamma\rrbracket$ is defined as $\llbracket S\mid\Gamma\rrbracket=\llbracket S\langle\langle\,\,\langle\langle\Gamma\rrbracket$ with

which means that $A\,\langle\langle A_{\_}1,A_{\_}2\ldots,A_{\_}n\rrbracket=(\ldots(A\otimes A_{\_}1)\otimes A_{\_}2)\ldots)\otimes A_{\_}n$. The interpretation of antecedents is functorial, i.e., we have the following inference rule:

The function $\mathsf{sound}$ is well-defined on $\circeq$-equivalence classes: given related derivations $f\circeq g$, then $\mathsf{sound}\;f\doteq\mathsf{sound}\;g$.

Categorical calculus derivations can be interpreted as sequent calculus derivations via a function $\mathsf{cmplt}:\llbracket S\mid\Gamma\rrbracket\Longrightarrow C\to S\mid\Gamma\longrightarrow C$, well-defined on $\doteq$-equivalence classes: given related derivations $f\doteq g$, then $\mathsf{cmplt}\;f\circeq\mathsf{cmplt}\;g$. The cut rule $\mathsf{scut}$ is fundamental for modelling the composition operation $\mathsf{comp}$ of the categorical calculus.

The functions $\mathsf{sound}$ and $\mathsf{cmplt}$ establish a bijection between derivations in the categorical calculus and the sequent calculus: $\mathsf{sound}\;(\mathsf{cmplt}\;f)\doteq f$ and $\mathsf{cmplt}\;(\mathsf{sound}\;g)\circeq g$, for all $f:\llbracket S\mid\Gamma\rrbracket\Longrightarrow C$ and $g:S\mid\Gamma\longrightarrow C$.

The congruence relation $\circeq$ can be considered as a term rewrite system, by directing every equation from left to right. The resulting rewrite system is weakly confluent and strongly normalizing, hence confluent with unique normal forms.

Normal-form derivations in our sequent calculus can be described as derivations in a focused subsystem. In the style of Andreoli [3], we present the focused subsystem as a sequent calculus with an additional phase annotation on sequents. In phase $\mathsf{L}$, sequents are of the form $S\mid\Gamma\overset{}{\longrightarrow_{\mathsf{L}}}C$, where $S$ is a general stoup. In phase $\mathsf{R}$, sequents take the form $T\mid\Gamma\overset{}{\longrightarrow_{\mathsf{R}}}C$, where $T$ is an irreducible stoup, that is an optional atom: either empty or an atomic formula. Derivations in the focused calculus are inductively generated by the following inference rules:

The focused rules define a sound and complete proof search strategy. The focused calculus is clearly sound: by erasing phase annotations, all of the rules are either rules of the original calculus or else (in the case of $\mathsf{switch}$) have the conclusion equal to the premise. So focused calculus derivations can be embedded into sequent calculus derivations via a function $\mathsf{emb}_{\_}P:S\mid\Gamma\longrightarrow_{P}C\to S\mid\Gamma\longrightarrow C$, where $P\in\{\mathsf{L},\mathsf{R}\}$.

The focused calculus is also complete: we can define a normalization procedure $\mathsf{focus}:S\mid\Gamma\longrightarrow C\to\linebreak S\mid\Gamma\overset{}{\longrightarrow_{\mathsf{L}}}C$ sending each derivation in the sequent calculus to a canonical representative of its $\circeq$-equivalence class in the focused calculus. This means in particular that $\mathsf{focus}$ maps $\circeq$-related derivations to equal focused derivations.

The functions $\mathsf{focus}$ and $\mathsf{emb}_{\_}{\mathsf{L}}$ establish a bijection between derivations in the full sequent calculus (up to $\circeq$) and its focused subsystem: $\mathsf{emb}_{\_}{\mathsf{L}}\;(\mathsf{focus}\;f)\circeq f$ and $\mathsf{focus}\;(\mathsf{emb}_{\_}{\mathsf{L}}\;g)=g$, for all $f:S\mid\Gamma\longrightarrow C$ and $g:S\mid\Gamma\overset{}{\longrightarrow_{\mathsf{L}}}C$.

Putting this together with the results discussed in Section 2.2, it follows that the focused calculus is a concrete presentation of the free skew monoidal category $\mathbf{Fsk}(\mathsf{At})$. As such, the focused calculus solves the problem of characterizing the homsets of the free skew monoidal category, a.k.a. the coherence problem. Moreover, it solves two related algorithmic problems effectively:

• •

  Duplicate-free enumeration of all maps $A\Longrightarrow C$ in the form of representatives of $\doteq$-equivalence classes of categorical calculus derivations: For this, find all focused derivations of $A\mid~{}\overset{}{\longrightarrow_{\mathsf{L}}}C$, which is solvable by exhaustive proof search, which terminates, and translate them to the categorical calculus derivations.

• •

  Finding whether two given maps of type $A\Longrightarrow C$, presented as categorical calculus derivations, are equal, i.e., $\doteq$-related as derivations: For this, translate them to focused derivations of $A\mid~{}\overset{}{\longrightarrow_{\mathsf{L}}}C$ and check whether they are equal, which is decidable.

Different approaches to the coherence problem of skew monoidal categories have been considered before. Uustalu [23] identified a class of normal forms of objects in $\mathbf{Fsk}{(\mathsf{At})}$ and showed that there exists at most one map between an object and an object in normal form, and exactly one map between an object and that object’s normal form. In another direction, Lack and Street [15] addressed the problem of determining equality of maps by proving that there is a faithful, structure-preserving functor $\mathbf{Fsk}{(1)}\to\Delta_{\_}\bot$ from the free skew monoidal category on one generating object to the category of finite non-empty ordinals and first-element-and-order-preserving functions (which is an associative-normal skew-monoidal category under the ordinal sum with unit 1). This approach was further elaborated by Bourke and Lack [5] with a more explicit description of the homsets of $\mathbf{Fsk}{(1)}$.

Let us use the focused calculus to analyze where multiple maps $A\Longrightarrow C$ can come from. There are two sources of non-determinism in root-first proof search in the focused calculus: (i) in phase $\mathsf{L}$, when the stoup is empty, whether to apply $\mathsf{pass}$ or $\mathsf{switch}$, and (ii) in phase $\mathsf{R}$, when the succedent formula is a tensor and the rule $\otimes\mathsf{R}$ is to be applied, how to split the context into $\Gamma$ and $\Delta$. In the latter situation, only those choices where $|T|,|\Gamma|=|A|$ and $|\Delta|=|B|$ can possibly lead to a complete derivation; we write $|~{}|$ for the frontier of atoms in a formula, an optional formula or a list of formulae. But there can be multiple such choices if in the middle of the context there are closed formulae (i.e., formulae made of $\mathsf{I}$ and $\otimes$ only): those can be freely split between $\Gamma$ and $\Delta$.

The two maps $\mathsf{id}\not\doteq\alpha\circ\rho\otimes\lambda:X\otimes(\mathsf{I}\otimes Y)\Longrightarrow X\otimes(\mathsf{I}\otimes Y)$ translate to two different focused derivations of the sequent $X\otimes(\mathsf{I}\otimes Y)\mid~{}\overset{}{\longrightarrow_{\mathsf{L}}}X\otimes(\mathsf{I}\otimes Y)$ because of the non-determinism of type (i). Notice the choice between $\mathsf{pass}$ and $\mathsf{switch}$.

The two maps $\mathsf{id}\not\doteq\rho\otimes\lambda\circ\alpha:(X\otimes\mathsf{I})\otimes Y\Longrightarrow(X\otimes\mathsf{I})\otimes Y$ translate to distinct focused derivations of the sequent $(X\otimes\mathsf{I})\otimes Y\mid~{}\overset{}{\longrightarrow_{\mathsf{L}}}(X\otimes\mathsf{I})\otimes Y$ due to type-(ii) non-determinism. Here the first (from the endsequent) application of the tensor right rule $\otimes\mathsf{R}$ splits the context in two different ways: in the first derivation the unit in the context is sent to the first premise, while in the second derivation it is sent to the second premise.

The free left-normal skew monoidal category $\mathbf{Fsk}_{\mathsf{LN}}(\mathsf{At})$ on a set $\mathsf{At}$ is obtained by extending the grammar of derivations in the fully skew categorical calculus (1) with a new inference rule:

and extending the equivalence of derivations (2) with two new equations: $\lambda\circ\lambda^{-1}\doteq\mathsf{id}$ and $\lambda^{-1}\circ\lambda\doteq\mathsf{id}$.

An equivalent sequent calculus presentation of $\mathbf{Fsk}_{\mathsf{LN}}(\mathsf{At})$ is obtained by adding another right rule for the tensor $\otimes$ to the fully skew sequent calculus (3), which allows one to send the formula in the stoup to the second premise, provided that all of the context is also sent to the second premise (so the antecedent of the first premise is left completely empty).

The introduction of $\otimes\mathsf{R}_{2}$ makes it possible to derive a sequent corresponding to $\lambda^{-1}:A\Longrightarrow\mathsf{I}\otimes A$:

In particular this allows us to interpret categorical derivations into sequent calculus derivations for the left-normal case, extending the definition of the function $\mathsf{cmplt}$ introduced in Section 2.2.

Equivalence of derivations in the sequent calculus is the least congruence $\circeq$ induced by the equations in (4) together with the following equations:

The two cut rules in (5) are also admissible in the left-normal sequent calculus. The definition of $\mathsf{ccut}$ uses the following rule $\mathsf{act}$ (for ‘activate’), admissible in this sequent calculus (but not in the fully skew one) and inverting $\mathsf{pass}$ up to the congruence $\circeq$:

The transformation $\mathsf{sound}$ introduced in Section 2.2, interpreting the fully skew sequent calculus derivations as categorical calculus derivations, extends to the left-normal case. Given $f:{-}\mid~{}\longrightarrow A$ and $g:A^{\prime}\mid\Delta\longrightarrow B$, define $\mathsf{sound}\;(\otimes\mathsf{R}_{2}(f,g))$ as:

Again, the congruence relation $\circeq$ read as a term rewrite system is weakly confluent and strongly normalizing, and normal-form derivations in the sequent calculus can be described as derivations in a focused subsystem. Sequents in the left-normal focused calculus are annotated with two possible phase annotations, as in the fully skew focused calculus (7). The condition for switching phase is different: the formula in the stoup is still required to be irreducible, but if the stoup is empty we are allowed to switch phase only when the context is empty as well. In phase $\mathsf{R}$, we also include the new tensor right rule $\otimes\mathsf{R}_{2}$, in which both premises are required to be $\mathsf{R}$-phase derivations. Again $T$ is an irreducible stoup: either empty or an atomic formula.

All $\mathsf{R}$-phase sequents in a derivation of a sequent $S\mid\Gamma\overset{}{\longrightarrow_{\mathsf{L}}}C$ have the context empty if the stoup is empty.

The functions $\mathsf{emb}_{\_}{\mathsf{L}}$ and $\mathsf{emb}_{\_}{\mathsf{R}}$ embedding fully skew focused calculus derivations in the unfocused sequent calculus, discussed in Section 2.3, can clearly be adapted to the left-normal case. The same holds for the $\mathsf{focus}$ function, sending a sequent calculus derivation to its $\circeq$-normal form in the focused calculus. In particular, this means that $\mathsf{focus}$ maps two $\circeq$-equivalent derivations to the same focused derivation. Similarly to the fully skew case, $\mathsf{focus}$ and $\mathsf{emb}_{\_}\mathsf{L}$ establish a bijection between maps in the left-normal sequent calculus (up to $\circeq$) and its focused subsystem.

The left-normal focused calculus has less non-determinism than the fully skew focused calculus. The non-determinism of type (i) is not there: In phase $\mathsf{L}$, $\mathsf{switch}$ cannot be applied unless the context is empty while $\mathsf{pass}$ only applies if it is non-empty. The non-determinism of type (ii) remains much like in the fully skew case except that there are two tensor right-rules, $\otimes\mathsf{R}$ and $\otimes\mathsf{R}_{2}$. In a choice that can lead to a completed derivation, we must be able to take $|T|,|\Gamma|=|A|$ and $|\Delta|=|B|$ in $\otimes\mathsf{R}$ or $()=|A|$ and $X,|\Delta|=|B|$ in $\otimes\mathsf{R}_{2}$. There may be multiple such choices if in the middle of the context we have closed formulae.

In the free left-normal skew monoidal category, we have $\mathsf{id}\doteq\alpha\circ\rho\otimes\lambda:X\otimes(\mathsf{I}\otimes Y)\Longrightarrow X\otimes(\mathsf{I}\otimes Y)$:

This collapse is reflected by there being exactly one focused derivation of the sequent $X\otimes(\mathsf{I}\otimes Y)\mid~{}\overset{}{\longrightarrow_{\mathsf{L}}}X\otimes(\mathsf{I}\otimes Y)$. Compare this with the two distinct derivations of the sequent in the fully skew focused calculus, displayed in (8). In the left-normal focused calculus, we are forced to use $\mathsf{pass}$, we cannot apply $\mathsf{switch}$ since the stoup is empty but the context is not.

The left-normal sequent calculus admits also a stoup-free presentation. This is because the rule $\mathsf{pass}$ is invertible. Here we only show the focused subsystem of the stoup-free variant. In phase $\mathsf{L}$, sequents are of the form $\Gamma\longrightarrow_{\mathsf{L}}C$, where $\Gamma$ is a general list of formulae. In phase $\mathsf{R}$, sequents take the form $\Lambda\longrightarrow_{\mathsf{R}}C$, where $\Lambda$ is an irreducible list of formulae, meaning that it is either empty or the formula in its head is an atom.

Derivations of a sequent $S\mid\Gamma\overset{}{\longrightarrow_{\mathsf{L}}}C$ are in a bijection with derivations of $\llbracket S\langle\langle\,,\Gamma\longrightarrow_{\mathsf{L}}C$ where $\llbracket S\langle\langle\,$ is the interpretation of a stoup as a formula introduced in Section 2.2.

The free right-normal skew monoidal category $\mathbf{Fsk}_{\mathsf{RN}}(\mathsf{At})$ on a set $\mathsf{At}$ is obtained by extending the grammar of derivations in the fully skew categorical calculus (1) with a new inference rule:

and extending the equivalence of derivations (2) with two new equations: $\rho\circ\rho^{-1}\doteq\mathsf{id}$ and $\rho^{-1}\circ\rho\doteq\mathsf{id}$.

An equivalent sequent calculus presentation of $\mathbf{Fsk}_{\mathsf{RN}}(\mathsf{At})$ is realized by adding additional left rules for $\mathsf{I}$ and $\otimes$ to the fully skew sequent calculus (3), relaxing the condition for deleting the unit and decomposing tensors in the antecedent:

Here and later, $J$ and $J^{\prime}$ stand for closed formulae. The introduction of $\mathsf{IC}$ makes it possible to derive a sequent corresponding to $\rho^{-1}:A\otimes\mathsf{I}\Longrightarrow A$ for any $A$, including $A=X$:

The rule $\otimes\mathsf{C}^{\mathrm{c}}$ is needed since it is important to allow deletion in the context of any closed formula and not just $\mathsf{I}$: we need to be able to derive, e.g., the sequent $X\mid\mathsf{I}\otimes\mathsf{I}\longrightarrow X$. Analogously, in the left-normal sequent calculus of Section 3.1, it was important to be able to derive the sequent $X\mid~{}\longrightarrow(\mathsf{I}\otimes\mathsf{I})\otimes X$, which was possible since the first premise of the inference rule $\otimes\mathsf{R}_{2}$ is a sequent ${-}\mid~{}\longrightarrow A$, which is derivable precisely when $A$ is closed.

Equivalence of derivations in the sequent calculus is the least congruence $\circeq$ induced by the equations in (4) together with the following equations: