to the tree-like normalisation i.e $\exec(\Sigma)$ will be a shortcut for $\exec_{\mathcal{A}}^{\mathrm{tree}}(\Sigma)$ where $\mathcal{A}$ is a set of colour left implicit.

Multiplicative Linear Logic {#subsec:mll}
---------------------------

[.275]{} $$A, B = X_i \mid X_i^\bot \mid A \otimes B \mid A \parr B \quad \text{where $i \in \nat$}$$

[.275]{}

[.4]{}

[0.9]{}

Multiplicative linear logic (MLL) is a fragment of linear logic [@girard1987linear] restricted to the tensor $\otimes$ and par $\parr$ connectives. The set $\mathcal{F}_{\mathrm{MLL}}$ of MLL formulas is defined by the grammar of the figure \[subfig:mllformulas\]. Linear negation $(\cdot)^\bot$ is extended to formulas by involution and de Morgan laws: $X^{\bot\bot} = X$, $(A \otimes B)^\bot = A^\bot \otimes B^\bot$, and $(A \parr B)^\bot = A^\bot \parr B^\bot$.

Proofs of MLL can be written in the traditional sequent calculus fashion [@gentzen1935untersuchungen; @gentzen1935untersuchungen2] using the set of rules shown in figure \[subfig:mllsequent\]. In his seminal paper [@girard1987linear], Girard introduced an alternative syntax, akin to *natural deduction*, based on a graph-theoretic representation of proofs. In this syntax, one considers the notion of proof-structure, i.e. an directed hypergraph with vertices labelled by formulas and constructed from hyperedges[^5] labelled within $\{ax, cut, \otimes, \parr\}$ and satisfying the arities and labelling constraints shown in figure \[subfig:proofstructures\]. A proof-structure 