Causality in Linear Logic
Abstract
Commuting conversions of Linear Logic induce a notion of dependency between rules inside a proof derivation: a rule depends on a previous rule when they cannot be permuted using the conversions. We propose a new interpretation of proofs of Linear Logic as causal invariants which captures exactly this dependency. We represent causal invariants using game semantics based on general event structures, carving out, inside the model of [6], a submodel of causal invariants. This submodel supports an interpretation of unitfree Multiplicative Additive Linear Logic with MIX (MALL\(^\)) which is (1) fully complete: every element of the model is the denotation of a proof and (2) injective: equality in the model characterises exactly commuting conversions of MALL\(^\). This improves over the standard fully complete game semantics model of MALL\(^\).
Keywords
Event structures Linear Logic Proof nets Game semantics1 Introduction
Proofs up to commuting conversions. In the sequent calculus of Linear Logic, the order between rules need not always matter: allowed reorderings are expressed by commuting conversions. These conversions are necessary for confluence of cutelimination by mitigating the sequentiality of the sequent calculus. The real proof object is often seen as an equivalence class of proofs modulo commuting conversions. The problem of providing a canonical representation of proofs up to those commuting conversions is as old as Linear Logic itself, and proves to be a challenging problem. The traditional solution interprets a proof by a graphical representation called proof net and dates back to Girard [17]. Girard’s solution is only satisfactory in the multiplicativeexponential fragment of Linear Logic. For additives, a wellknown solution is due to Hughes and van Glabbeck [22], where proofs are reduced to their set of axiom linkings. However, the correctness criterion relies on the difficult toggling condition.
Conversions essentially state that the order between rules applied to different premises does not matter, as evidenced in the two equivalent proofs of the sequent Open image in new window depicted on the right. These two proofs are equal in extensional models of Linear Logic because they have the same extensional behaviour. Unfortunately, characterising the image of the interpretation proved to be a difficult task in extensional models. The first fully complete models used game semantics, and are due to Abramsky and Melliès (MALL) [1] and Melliès (Full LL) [24]. However, their models use an extensional quotient on strategies to satisfy the conversions, blurring the concrete nature of strategies.
Contributions and outline. Drawing inspiration from the interpretation of proofs in terms of processes, we build a fully complete and injective model of unitfree Multiplicative Additive Linear Logic with MIX (MALL\(^\)), interpreting proofs as general event structures living in a submodel of the model introduced by [6]. Moreover, our model captures the dependency between rules, which makes sequentialisation a local operation, unlike in proof nets, and has a more uniform acyclicity condition than [22].
We first recall the syntax of MALL\(^\) and its reading in terms of processes in Sect. 2. Then, in Sect. 3, we present a slight variation on the model of [6], where we call the (pre)strategies causal structures, by analogy with proof structures. Each proof tree can be seen as a (sequential) causal structure. However, the space of causal structures is too broad and there are many causal structures which do not correspond to any proofs. A major obstacle to sequentialisation is the presence of deadlocks. In Sect. 4, we introduce a condition on causal structures, ensuring deadlockfree composition, inspired by the interaction between Open image in new window and \( \otimes \) in Linear Logic. Acyclic causal structures are still allowed to only explore partially the game, contrary to proofs which must explore it exhaustively, hence in Sect. 5, we introduce further conditions on causal structures, ensuring a strong sequentialisation theorem (Theorem 2): we call them causal nets. In Sect. 6, we define causal invariants as maximal causal nets. Every causal net embeds in a unique causal invariant; and a particular proof P embeds inside a unique causal invariant which forms its denotation Open image in new window . Moreover, two proofs embed in the same causal invariant if and only if they are convertible (Theorem 4). Finally, we show how to equip causal invariants with the structure of \( *\)autonomous category with products and deduce that they form a fully complete model of MALL\(^\) (Theorem 6) for which the interpretation is injective.
The proofs are available in the technical report [7].
2 MALL\(^\) and Its Commuting Conversions
In this section, we introduce MALL\(^\) formulas and proofs as well as the standard commuting conversions and cut elimination for this logic. As mentioned in the introduction, we use a processlike presentation of proofs following [27]. This highlights the communicating aspect of proofs which is an essential intuition for the model; and it offers a concise visualisation of proofs and conversions.
Formulas. We define the formulas of MALL\(^\): Open image in new window , where X and Open image in new window are atomic formulas (or ltterals) belonging to a set \(\mathbb A\). Formulas come with the standard notion of duality \((\cdot )^\perp \) given by the De Morgan rules: \(\otimes \) is dual to Open image in new window , and \(\oplus \) to Open image in new window . An environment is a partial mapping of names to formulas, instead of a multiset of formulas – names disambiguate which assumption a rule acts on.
Commutation rules and cut elimination. We now explain the valid commutations rules in our calculus. We consider contexts \(C\left[ []_1, \ldots , []_n\right] \) with several holes to accomodate Open image in new window which has two branches. Contexts are defined in Fig. 3, and are assigned a type Open image in new window . It intuitively means that if we plug proofs of \( \varGamma _i\) in the holes, we get back a proof of Open image in new window . We use the notation \(C[P_i]_i\) for \(C[P_1, \ldots , P_n]\) when \((P_i)\) is a family of processes. Commuting conversion is the smallest congruence \(\equiv \) satisfying all welltyped instances of the rule \(C[D[P_{i, j}]_j]_i \equiv D[C[P_{i, j}]_i]_j\) for C and D two contexts. For instance \(a[\mathtt{inl}].\, b{.}{} \mathtt{case}\,(P, Q) \equiv b{.}{} \mathtt{case}\,(a[\mathtt{inl}].\, P, a[\mathtt{inl}].\, Q)\). Figure 4 gives reduction rules \(P \rightarrow Q\). The first four rules are the principal cut rules and describe the interaction of two dual terms, while the last one allows cuts to move inside contexts.
3 Concurrent Games Based on General Event Structures
3.1 Games as Prime Event Structures with Polarities
Definition of games. Prime event structures [28] (simply event structures in the rest of the paper) are a causal model of nondeterministic and concurrent computation. We use here prime event structures with binary conflict. An event structure is a triple \((E, \le _E , \#_E)\) where \((E, \le _E)\) is a partial order and \(\#_E\) is an irreflexive symmetric relation (representing conflict) satisfying: (1) if \(e \in E\), then \([e] := \{ e' \in E \mid e' \le _E e \}\) is finite; and (2) if \(e \,\#_E \, e'\) and \(e \le _E e''\) then \(e'' \,\#_E\, e'\). We often omit the E subscripts when clear from the context.
A configuration of E is a downclosed subset of E which does not contain two conflicting events. We write \( \mathscr {C} (E)\) for the set of finite configurations of E. For any \(e \in E\), [e] is a configuration, and so is \([e) := [e] \setminus \{e\}\). We write Open image in new window for the immediate causal relation of E defined as \(e < e'\) with no event between. Similarly, a conflict \(e \# e'\) is minimal, denoted Open image in new window , when the \([e] \cup [e')\) and \([e) \cup [e']\) are configurations. When drawing event structures, only Open image in new window and Open image in new window are represented. We write \(\max (E)\) for the set of maximal events of E for \( \le _E\). An event e is maximal in x when it has no successor for \( \le _E\) in x. We write \(\max _E\, x\) for the maximal events of a configuration \(x \in \mathscr {C} (E)\).
An event structure E is confusionfree when (1) for all Open image in new window then \([e) = [e')\) and (2) if Open image in new window and Open image in new window then \(e = e''\) or Open image in new window . As a result, the relation Open image in new window is an equivalence relation whose equivalent classes \(\mathfrak a\) are called cells.
Definition 1
A game is a confusionfree event structure A along with an assignment \( pol :A \rightarrow \{, +\}\) such that cells contain events of the same polarity, and a function Open image in new window mapping every maximal event of A to an atom. Events with polarity − (resp. \(+\)) are negative (resp. positive).
Events of a game are usually called moves. The restriction imposes branching to be polarised (i.e. belonging to a player). A game is rooted when two minimal events are in conflict. Single types are interpreted by rooted games, while contexts are interpreted by arbitrary games. When introducing moves of a game, we will indicate their polarity in exponent, e.g. “let \(a^+ \in A\)” stands for assuming a positive move of A.
Interpretation of formulas. To interpret formulas, we make use of standard constructions on prime event structures. The event structure \(a \cdot E\) is E prefixed with a, i.e. \(E \cup \{a\}\) where all events of E depends on a. The parallel composition of E and \(E'\) represents parallel executions of E and \(E'\) without interference:
Definition 2
The parallel composition of event structures \(A_0\) and \(A_1\) is the event structure \(A_0 \parallel A_1 = (\{0 \} \times A_0\, \cup \, \{1\} \times A_1, \le _{A_0 \parallel A_1}, \#_{A_0 \parallel A_1})\) with \((i, a) \le _{A_0 \parallel A_1} (j, a')\) iff \(i = j\) and \(a \le _{A_i} a'\); and \((i, a) \,\#_{A_0 \parallel A_1} \, (j, a')\) when \(i = j\) and \(a\,\#_{A_j}\, a'\).
The sum of event structure \(E+F\) is the nondeterministic analogue of parallel composition.
Definition 3
The sum \(A_0 + A_1\) of the two event structures \(A_0\) and \(A_1\) has the same partial order as \(A_0 \parallel A_1\), and conflict relation \((i, a) \,\#_{A_0 + A_1}\, (j, a')\) iff \(i \ne j\) or \(i = j\) and \(a\,\#_{A_j}\, a'\).
Prefixing, parallel composition and sum of event structures extend to games. The dual of a game A, obtained by reversing the polarity labelling, is written \(A^\perp \). Given \(x \in \mathscr {C} (A)\), we define A / x (“A after x”) as the subgame of A comprising the events \(a \in A \setminus x\) not in conflict with events in x.
In diagrams, we write moves of a context following the syntactic convention: for instance \(u[\mathtt{inl}]\) denotes the minimal inl move of the u component. For tensors and pars, we use the notation u[v] and u(v) to make explicit the variables we use in the rest of the diagram, instead of \(\texttt {send}^+\) and \(\texttt {send}^\) respectively. For atoms, we use u : X and \(u: X^\perp \).
3.2 Causal Structures as Deterministic General Event Structures
As we discussed in Sect. 1, prime event structures cannot express disjunctive causalities deterministically, hence fail to account for the determinism of LL. Our notion of causal structure is based on general event structures, which allow more complex causal patterns. We use a slight variation on the definition of deterministic general event structures given by [6], to ensure that composition is welldefined without further assumptions.
Instead of using the more concrete representation of general event structures in terms of a set of events and an enabling relation, we use the following formulation in terms of set of configurations, more adequate for mathematical reasoning. Being only sets of configurations, they can be reasoned on with very simple settheoretic arguments.
Definition 4

Coincidencefreeness If \(e, e' \in x \in \sigma \) then there exists \(y \in \sigma \) with \(y \subseteq x\) and \(y \cap \{e, e'\}\) is a singleton.

Determinism for \(x, y \in \sigma \) such that \(x\,\cup \,y\) does not contain any minimal negative conflict, then \(x \cup y \in \sigma \).
Configurations of prime event structures satisfy a further axiom, stability, which ensures the absence of disjunctive causalities. When \( \sigma \) is a causal struct on A, we write \( \sigma : A\). We draw as regular event structures, using Open image in new window and Open image in new window . To indicate disjunctive causalities, we annotate joins with or. This convention is not powerful enough to draw all causal structs, but enough for the examples in this paper. As an example, on \(A = a \parallel b \parallel c\) the diagram on the right denotes the following causal struct \( \sigma = \{x \in \mathscr {C} (A) \mid c \in x \Rightarrow x \cap \{a, b\} \ne \varvec{\emptyset } \}\).
A minimal event of \( \sigma : A\) is an event \(a \in A\) with \(\{a\} \in \sigma \). An event \(a \in x \in \sigma \) is maximal in x when \(x \setminus \{a\} \in \sigma \). A prime configuration of \(a \in A\) is a configuration \(x \in \sigma \) such that a is its unique maximal event. Because of disjunctive causalities, an event \(a \in A\) can have several distinct prime configurations in \( \sigma \) (unlike in event structures). In the previous example, since c can be caused by either a or b, it has two prime configurations: \(\{a, c\}\) and \(\{b, c\}\). We write \(\max \sigma \) for the set of maximal configurations of \( \sigma \), ie. those configurations that cannot be further extended.
Lemma 1
If \( \sigma : A^\perp \parallel B\) and \( \tau :B^\perp \parallel C\) are causal structs then \( \tau \odot \sigma \) is a causal struct.
Composition of causal structs will be used to interpret cuts between proofs of Linear Logic. In concurrent game semantics, composition has a natural identity, asynchronous copycat [25], playing on the game \(A^\perp \parallel A\), forwarding negative moves on one side to the positive occurrence on the other side. Following [6], we define Open image in new window where \(x \subseteq ^p y\) means \(x \subseteq y\) and \( pol (y \setminus x) \subseteq \{p\}\).
However, in general copycat is not an identity on all causal structs, only \( \sigma \subseteq \ c\!\!\!\!c\,_A \odot \sigma \) holds. Indeed, copycat represents an asynchronous buffer, and causal structs which expects messages to be transmitted synchronously may be affected by composition with copycat. We call causal structs that satisfy the equality asynchronous. From [6], we know that asynchronous causal structs form a compactclosed category.
The syntactic tree. The syntactic tree of a derivation Open image in new window can be read as a causal struct \( Tr (P)\) on Open image in new window , which will be the basis for our interpretation. It is defined by induction:
We use the convention in the diagram, for instance u[v] means the initial \(\mathtt {send}\) move of the u component. An example of this construction is given in Fig. 5a. Note that it is not asynchronous.
4 Acyclicity of Causal Structures
The space of causal structs is unfortunately too broad to provide a notion of causal nets, due in particular to the presence of deadlocks during composition. As a first step towards defining causal nets, we introduce in this section a condition on causal structs inspired by the tensor rule in Linear Logic. In Sect. 4.1, we propose a notion of communication between actions, based on causality. In Sect. 4.2, we introduce a notion of acyclicity which is shown to be stable under composition and ensure deadlockfree composition.
4.1 Communication in Causal Structures
The tensor rule of Linear Logic says that after a tensor u[v], the proof splits into two independent subproofs, one handling u and the other v. This syntactic condition is there to ensure that there are no communications between u and v. More precisely, we want to prevent any dependence between subsequent actions on u and an action v. Indeed such a causal dependence could create a deadlock when facing a par rule u(v), which is allowed to put arbitrary dependence between such subsequent actions.
Communication in MLL. Let us start by the case of MLL, which corresponds to the case where games do not have conflicts. Consider the following three causal structs:
The causal structs \( \sigma _1\) and \( \sigma _2\) play on the game Open image in new window , while \( \sigma _3\) plays on the game Open image in new window . The causal structs \( \sigma _2\) and \( \sigma _3\) are very close to proof nets, and it is easy to see that \( \sigma _2\) represents a correct proof net while \( \sigma _3\) does not. In particular, there exists a proof P such that \( Tr (P) \subseteq \sigma _2\) but there are no such proof Q for \( \sigma _3\). Clearly, \( \sigma _3\) should not be acyclic. But should \( \sigma _2\)? After all it is sequentialisable. But, in all sequentialisations of \( \sigma _2\), the par rule v(z) is applied before the tensor u[w], and this dependency is not reflected by \( \sigma _2\). Since our goal is exactly to compute these implicit dependencies, we will only consider \( \sigma _1\) to be acyclic, by using a stronger sequentialisation criterion:
Definition 5
A causal struct Open image in new window is strongly sequentialisable when for all \(x \in \sigma \), there exists Open image in new window with \(x \in Tr (P)\) and \( Tr (P) \subseteq \sigma \).
To understand the difference between \( \sigma _1\) and \( \sigma _2\), we need to look at causal chains. In both \( \sigma _1\) and \( \sigma _2\), we can go from \(u:X^\perp \) to \(w:Y^\perp \) by following immediate causal links Open image in new window in any direction, but observe that in \( \sigma _1\) they must all cross an event below u[w] (namely v(z) or u[w]). This prompts us to define a notion of communication outside a configuration x:
Definition 6
Given \( \sigma : A\) and \(x \in \sigma \) we say that \(a, a' \in A \setminus x\) communicate outside x (written \(a \leftrightsquigarrow _{x, \sigma } a'\)) when there exists a chain Open image in new window where all the \(a_i \in A \setminus x\), and Open image in new window denotes the symmetric closure of Open image in new window .
Communication in MALL. In presence of additives, immediate causality is not the only vector of communication. Consider the following causal struct \( \sigma _4\), playing on the context Open image in new window where A is irrelevant:
This pattern is not strongly sequentialisable: the tensor u[w] must always go after the Open image in new window introduction on v, since we need this information to know how whether v should go with u or w when splitting the context. Yet, it is not possible to find a communication path from one side to the other by following purely causal links without crossing u[w]. There is however a path that uses both immediate causality and minimal conflict. This means that we should identify events in minimal conflict, since they represent the same ( Open image in new window introduction rule). Concretely, this means lifting the previous definition at the level of cells. Given an causal struct \( \sigma : A\) and \(x \in \sigma \), along with two cells \(\mathfrak a, \mathfrak a'\) of A / x, we define the relation Open image in new window when there exists \(a \in \mathfrak a\) and \(a' \in \mathfrak a'\) such that Open image in new window ; and \(\mathfrak a \leftrightsquigarrow _{x, \sigma } \mathfrak a'\) when there exists Open image in new window where all the \(\mathfrak a_i\) do not intersect x. For instance, the two cells which are successors of the tensor u[w] in \( \sigma _4\) communicate outside the configuration \(\{u[w]\}\) by going through the cell \(\{v(\mathtt {inl}), v(\mathtt {inr})\}\).
4.2 Definition of Acyclicity on Casual Structures
Since games are trees, two events \(a, a'\) are either incomparable or have a meet \(a \wedge a'\). If \(a \wedge a'\) is defined and positive, we say that a and \(a'\) have positive meet, and means that they are on two distinct branches of a tensor. If \(a \wedge a'\) is undefined, or defined and negative, we say that \(a \wedge a'\) has a negative meet. When the meet is undefined, it means that a and \(a'\) are events of different components of the context. We consider the meet to be negative in this case, since components of a context are related by an implicit par.
These definitions are easily extended to cells. The meet \(\mathfrak a \wedge \mathfrak a'\) of two cells \(\mathfrak a\) and \(\mathfrak a'\) of A is the meet \(a \wedge a'\) for \(a \in \mathfrak a\) and \(a' \in \mathfrak a'\): by confusionfreeness, it does not matter which ones are chosen. Similarly, we say that \(\mathfrak a\) and \(\mathfrak a'\) have positive meet if \(\mathfrak a \wedge \mathfrak a'\) is defined and positive; and have negative meet otherwise. These definitions formalise the idea of “the two sides of a tensor”, and allow us to define acyclicity.
Definition 7
A causal struct \( \sigma : A\) is acyclic when for all \(x \in \sigma \), for any cells \(\mathfrak a, \mathfrak a'\) not intersecting x and with positive meet, if \(\mathfrak a \leftrightsquigarrow _{x, \sigma } \mathfrak a'\) then \(\mathfrak a \wedge \mathfrak a' \not \in x\).
This captures the desired intuition: if \(\mathfrak a\) and \(\mathfrak a'\) are on two sides of a tensor a (ie. have positive meet), and there is a communication path outside x relating them, then a must also be outside x (and implicitly, the communication path must be going through a).
Reasoning on the interaction of acyclic strategies proved to be challenging. We prove that acyclic strategies compose, and their interaction are deadlockfree, when composition is on a rooted game B. This crucial assumption arises from the fact that in linear logic, cuts are on formulas. It entails that for any \(b, b' \in B\), \(b \wedge b'\) is defined, hence must be positive either from the point of view of \( \sigma \) or of \( \tau \).
Theorem 1
For acyclic causal structs \( \sigma : A^\perp \parallel B\) and \( \tau : B^\perp \parallel C\), (1) their interaction is deadlockfree: \( \tau \circledast \sigma = ( \sigma \parallel C) \cap (A \parallel \tau )\); and (2) the causal struct \( \tau \odot \sigma \) is acyclic.
As a result, acyclic and asynchronous causal structs form a category. We believe this intermediate category is interesting in its own right since it generalises the deadlockfreeness argument of Linear Logic without having to assume other constraints coming from Linear Logic, such as linearity. In the next section, we study further restriction on acyclic causal structs which guarantee strong sequentialisability.
5 Causal Nets and Sequentialisation
We now ready to introduce causal nets. In Sect. 5.1, we give their definition by restricting acyclic causal structs and in Sect. 5.2 we prove that causal nets are strongly sequentialisable.
5.1 Causal Nets: Totality and WellLinking Casual Structs
To ensure that our causal structs are strongly sequentialisable, acyclicity is not enough. First, we need to require causal structs to respect the linearity discipline of Linear Logic:
Definition 8
A causal struct \( \sigma : A\) is total when (1) for \(x \in \sigma \), if x is maximal in \( \sigma \), then it is maximal in \( \mathscr {C} (A)\); and (2) for \(x \in \sigma \) and \(a^\in A\setminus x\) such that \(x \cup \{a\} \in \sigma \), then whenever Open image in new window , we also have \(x \cup \{a'\} \in \sigma \) as well.
The first condition forces a causal struct to play until there are no moves to play, and the second forces an causal struct to be receptive to all Opponent choices, not a subset.
Our last condition constrains axiom links. A linking of a game A is a pair \((x, \ell )\) of a \(x \in \max \mathscr {C} (A)\), and a bijection \(\ell : (\max _A x)^ \simeq (\max _A x)^+\) preserving the \( atom \) labelling.
Definition 9
A total causal struct \( \sigma : A\) is welllinking when for each \(x \in \max (\sigma ) \), there exists a linking \(\ell _x\) of x, such that if y is a prime configuration of \(\ell _x(e)\) in x, then \(\max (y \setminus \{\ell _x(e)\}) = \{e\}\).
This ensures that every positive atom has a unique predecessor which is a negative atom.
Definition 10
A causal net is an acyclic, total and welllinking causal struct.
A causal net \( \sigma : A\) induces a set of linkings A, \(\textsf {link}( \sigma ) := \{ \ell _x \mid x \in \max \sigma \}\). The mapping \(\textsf {link}(\cdot )\) maps causal nets to the proof nets of [22].
5.2 Strong Sequentialisation of Causal Nets
Our proof of sequentialisation relies on an induction on causal nets. To this end, we provide an inductive deconstruction of parallel proofs. Consider \( \sigma : A\) a causal net and a minimal event \(a \in \sigma \) not an atom. We write A / a for \(A/\{a\}\). Observe that if Open image in new window , it is easy to see that there exists a context Open image in new window such that Open image in new window . Given a causal struct \( \sigma : A\), we define the causal struct \( \sigma /a = \{ x \in \mathscr {C} (A/a) \mid x \cup \{a\} \in \sigma \} : A/a\).
Lemma 2
\( \sigma /a\) is a causal net on A / a.
When a is positive, we can further decompose \( \sigma /a\) in disjoint parts thanks to acyclicity. Write \(\mathfrak a_1, \ldots , \mathfrak a_n\) for the minimal cells of A / a and consider for \(n \ge k > 0\), \(A_k = \{a' \in A/a \mid \text {cell}(a') \leftrightsquigarrow _{\{a\}, \sigma } \mathfrak a_k \}\). \(A_k\) contains the events of A / a which \( \sigma \) connects to the kth successor of a. We also define the set \(A_0 = A/a \setminus \bigcup _{1 \le k \le n} A_k\), of events not connected to any successor of a (this can happen with MIX). It inherits a game structure from A.
Each subset inherits a game structure from A / a. By acyclicity of \( \sigma \), the \(A_k\) are pairwise disjoint, so \(A/a \cong A_0 \parallel \ldots \parallel A_n\). For \(0 \le k \le n\), define \( \sigma _k = \mathscr {C} (A_k) \cap \sigma /a\).
Lemma 3
\( \sigma _k\) is a causal net on \(A_k\) and we have \( \sigma /a = \sigma _0 \parallel \ldots \parallel \sigma _n\).
This formalises the intuition that after a tensor, an acyclic causal net must be a parallel composition of proofs (following the syntactic shape of the tensor rule of Linear Logic). From this result, we show by induction that any causal net is strongly sequentialisable.
Theorem 2
If \( \sigma :A\) is a causal net, then \( \sigma \) is strongly sequentialisable.
We believe sequentialisation without MIX requires causal nets to be connected: two cells with negative meets always communicate outside any configuration they are absent from. We leave this lead for future work.
6 Causal Invariants and Completeness
Causal nets are naturally ordered by inclusion. When \( \sigma \subseteq \tau \), we can regard \( \tau \) as a less sequential implementation of \( \sigma \). Two causal nets which are upper bounded by a causal net should represent the same proof, but with varying degrees of sequentiality. Causal nets which are maximal for inclusion (among causal nets) are hence most parallel implementations of a certain behaviour and capture our intuition of causal invariants.
Definition 11
A causal invariant is a causal net \( \sigma : A\) maximal for inclusion.
6.1 Causal Invariants as Maximal Causal Nets
We start by characterising when two causal nets are upperbounded for inclusion:
Proposition 1
 1.
there exists a causal net \( \upsilon : A\) such that \( \sigma \subseteq \upsilon \) and \( \tau \subseteq \upsilon \),
 2.
the set \( \sigma \vee \tau = \{ x \cup y \mid x \in \sigma , y \in \tau , x \cup y \in \mathscr {C} (A) \}\) is a causal net on A,
 3.
\(\textsf {link}(\sigma )= \textsf {link}(\tau )\).
In this case we write \( \sigma \uparrow \tau \) and \( \sigma \vee \tau \) is the least upper bound of \( \sigma \) and \( \tau \) for \(\subseteq \).
It is a direct consequence of Proposition 1 that any causal net \( \sigma \) is included in a unique causal invariant \( \sigma ^ \uparrow : A\), defined as: \( \sigma ^ \uparrow = \bigvee _{ \sigma \subseteq \tau } \tau \), where \( \tau \) ranges over causal nets.
Lemma 4
For \( \sigma , \tau : A\) causal nets, \( \sigma \uparrow \tau \) iff \( \sigma ^ \uparrow = \tau ^ \uparrow \). Moreover, if \( \sigma \) and \( \tau \) are causal invariants, \( \sigma \uparrow \tau \) if and only if \( \sigma = \tau \).
The interpretation of a proof Open image in new window is simply defined as Open image in new window . Figure 5c illustrates the construction on a proof of MLL+mix. The interpretation features a disjunctive causality, as the tensor can be introduced as soon as one of the two pars has been.
Defining \(\textsf {link}(P) = \textsf {link}( Tr (P))\), we have from Lemma 4: \(\textsf {link}(P) = \textsf {link}(Q)\) if and only if Open image in new window . This implies that our model has the same equational theory than the proof nets of [22]. Such proof nets are already complete:
Theorem 3
([22]). For P, Q two proofs of \( \varGamma \), we have \(P \equiv Q\) iff \(\textsf {link}(P) = \textsf {link}(Q)\).
As a corollary, we get:
Theorem 4
For cutfree proofs P, Q we have \(P \equiv Q\) iff Open image in new window .
The technical report [7] also provides an inductive proof not using the result of [22]. A consequence of this result, along with strong sequentialisation is: Open image in new window This equality justifies our terminology of “causal completeness”, as for instance it implies that the minimal events of Open image in new window correspond exactly the possible rules in P that can be pushed to the front using the commuting conversions.
6.2 The Category of Causal Invariants
So far we have focused on the static. Can we integrate the dynamic aspect of proofs as well? In this section, we show that causal invariants organise themselves in a category. First, we show that causal nets are stable under composition:
Lemma 5
If \( \sigma : A^\perp \parallel B\) and \( \tau : B^\perp \parallel C\) are causal nets, then so is \( \tau \odot \sigma \).
Note that totality requires acyclicity (and deadlockfreedom) to be stable under composition. However, causal invariants are not stable under composition: \( \tau \odot \sigma \) might not be maximal, even if \( \tau \) and \( \sigma \) are. Indeed, during the interaction, some branches of \( \tau \) will not be explored by \( \sigma \) and viceversa which can lead to new allowed reorderings. However, we can always embed \( \tau \odot \sigma \) into \(( \tau \odot \sigma )^ \uparrow \):
Lemma 6
Rooted games and causal invariants form a category CInv, where the composition of \( \sigma : A^\perp \parallel B\) and \( \tau : B^\perp \parallel C\) is \(( \tau \odot \sigma )^ \uparrow \) and the identity on A is Open image in new window .
Note that the empty game is an object of \(\mathbf {CInv}\), as we need a monoidal unit.
Lemma 7
The tensor product defines a symmetric monoidal structure on CInv.
Define Open image in new window , \(\bot = 1 = \varvec{\emptyset }\) and Open image in new window .
Lemma 8
We have a bijection Open image in new window between causal invariants on \(A \parallel B \parallel C\) and on Open image in new window . As a result, there is an adjunction \(A \otimes \_ \dashv A \multimap \_\).
Lemma 8 implies that \(\mathbf {CInv}((A \multimap \bot ) \multimap \bot ) \simeq \mathbf {CInv}(A)\), and \(\mathbf {CInv}\) is \(*\)autonomous.
Cartesian products. Given two games A, B in \(\mathbf {CInv}\), we define their product Open image in new window . We show how to construct the pairing of two causal invariants concretely. Given \( \sigma \in \mathbf {CInv}(A, B)\) and \( \tau \in \mathbf {CInv}(A, C)\), we define the common behaviour of \( \sigma \) and \( \tau \) on A to be those \(x \in \mathscr {C} (A^\perp ) \cap \sigma \cap \tau \) such that for all \(\mathfrak a, \mathfrak a'\) outside of x with positive meet, \(\mathfrak a\leftrightsquigarrow _{x, \sigma } \mathfrak a'\) iff \(\mathfrak a\leftrightsquigarrow _{x, \tau } \mathfrak a'\). We write \( \sigma \cap _A \tau \) for the set of common behaviours of \( \sigma \) and \( \tau \) and define: \(\langle \sigma , \tau \rangle = (L^ \cdot \sigma ) \cup (R^ \cdot \tau ) \cup \sigma \cap _A \tau \). The projections are defined using copycat: Open image in new window (and similarly for \( \pi _2\)).
Theorem 5
CInv has products. As it is also \( *\)autonomous, it is a model of MALL.
It is easy to see that the interpretation of MALL\(^\) in \(\mathbf {CInv}\) following the structure is the same as Open image in new window , however it is computed compositionally without resorting to the \(^\uparrow \) operator. We deduce that our interpretation is invariant by cutelimination: if \(P \rightarrow Q\), then Open image in new window . Putting the pieces together, we get the final result.
Theorem 6
CInv is an injective and fully complete model of MALL\(^\).
7 Extensions and Related Work
The model provides a representation of proofs which retains only the necessary sequentiality. We study the phenomenon in Linear Logic, but commuting conversions of additives arise in other languages, eg. in functional languages with sums and products, where proof nets do not necessarily exist. Having an abstract representation of which reorderings are allowed could prove useful (reasoning on the possible commuting conversions in a language with sum types is notoriously difficult).
Extensions. Exponentials are difficult to add, as their conversions are not as canonical as those of MALL. Cyclic proofs [2] could be accomodated via recursive event structures.
We would also be interested in recast multifocusing [9] in our setting by defining a class of focussed causal nets, where there are no concurrency between positive and negative events, and show that sequentialisation always give a focused proof.
Related work. The first fully complete model of MALL\(^\) is based on closure operators [1], later extended to full Linear Logic [24]. True concurrency is used to define innocence, on which the full completeness result rests. However their model does not take advantage of concurrency to account for permutations, as strategies are sequential. This investigation has been extended to concurrent strategies by Mimram and Melliès [25, 26]. De Carvalho showed that the relational model is injective for MELL [11]. In another direction, [4] provides a fully complete model for MALL without game semantics, by using a glueing construction on the model of hypercoherences. [21] explores proof nets a weaker theory of commuting conversions for MALL.
The idea of having intermediate representations between proof nets and proofs has been studied by Faggian and coauthors using lnets [10, 13, 14, 15, 16], leading to a similar analysis to ours: they define a space of causal nets as partial orders and compare different versions of proofs with varying degree of parallelism. Our work recasts this idea using event structures and adds the notion of causal completeness: keeping jumps that cannot be undone by a permutation, which leads naturally to step outside partial orders, as well as full completeness: which causal nets can be strongly sequentialised?
The notion of dependency between logical rules has also been studied in [3] in the case of MLL. From a proof net R, they build a partial order Open image in new window which we believe is very related to Open image in new window where P is a sequentialisation of R. Indeed, in the case of MLL without MIX a partial order is enough to capture the dependency between rules. The work [12] shows that permutation rules of Linear Logic, understood as asynchronous optimisations on processes, are included in the observational equivalence. [19] studies mutual embedding between polarised proof nets [23] and the control \(\pi \)calculus [20]. In another direction, we have recently built a fullyabstract, concurrent game semantics model of the synchronous session \(\pi \)calculus [8]. The difficulty there was to understand name passing and the synchrony of the \(\pi \)calculus, which is the dual of our objective here: trying to understand the asynchrony behind the conversions of MALL\(^\).
Notes
Acknowledgements
We would like to thank Willem Heijltjes, Domenico Ruoppolo, and Olivier Laurent for helpful discussions, and the anonymous referees for their insightful comments. This work has been partially sponsored by: EPSRC EP/K034413/1, EP/K011715/1, EP/L00058X/1, EP/N027833/1, and EP/N028201/1.
References
 1.Abramsky, S., Melliés, P.A.: Concurrent games and full completeness. In: 14th Annual IEEE Symposium on Logic in Computer Science, Trento, Italy, 2–5 July 1999, pp. 431–442 (1999). http://dx.doi.org/10.1109/LICS.1999.782638
 2.Baelde, D., Doumane, A., Saurin, A.: Infinitary proof theory: the multiplicative additive case. In: CSL. Leibniz International Proceedings in Informatics (LIPIcs), vol. 62, pp. 42:1–42:17. Schloss DagstuhlLeibnizZentrum fuer Informatik (2016)Google Scholar
 3.Bagnol, M., Doumane, A., Saurin, A.: On the dependencies of logical rules. In: Pitts, A. (ed.) FoSSaCS 2015. LNCS, vol. 9034, pp. 436–450. Springer, Heidelberg (2015). https://doi.org/10.1007/9783662466780_28CrossRefzbMATHGoogle Scholar
 4.Blute, R., Hamano, M., Scott, P.J.: Softness of hypercoherences and MALL full completeness. Ann. Pure Appl. Logic 131(1–3), 1–63 (2005). https://doi.org/10.1016/j.apal.2004.05.002MathSciNetCrossRefzbMATHGoogle Scholar
 5.Caires, L., Pfenning, F.: Session types as intuitionistic linear propositions. In: Gastin, P., Laroussinie, F. (eds.) CONCUR 2010. LNCS, vol. 6269, pp. 222–236. Springer, Heidelberg (2010). https://doi.org/10.1007/9783642153754_16CrossRefGoogle Scholar
 6.Castellan, S., Clairambault, P., Winskel, G.: Observably deterministic concurrent strategies and intensional full abstraction for parallelor. In: 2nd International Conference on Formal Structures for Computation and Deduction, FSCD 2017, Oxford, UK, 3–9 September 2017, pp. 12:1–12:16 (2017). https://doi.org/10.4230/LIPIcs.FSCD.2017.12
 7.Castellan, S., Yoshida, N.: Causality in linear logic: full completeness and injectivity (unitfree multiplicativeadditive fragment). Technical report (2019). http://iso.mor.phis.me/publis/Causality_in_Linear_Logic_FOSSACS19.pdf
 8.Castellan, S., Yoshida, N.: Two sides of the same coin: session types and game semantics. Accepted for publication at POPL 2019 (2019)Google Scholar
 9.Chaudhuri, K., Miller, D., Saurin, A.: Canonical sequent proofs via multifocusing. In: Ausiello, G., Karhumäki, J., Mauri, G., Ong, L. (eds.) TCS 2008. IIFIP, vol. 273, pp. 383–396. Springer, Boston, MA (2008). https://doi.org/10.1007/9780387096803_26CrossRefGoogle Scholar
 10.Curien, P.L., Faggian, C.: Lnets, strategies and proofnets. In: Ong, L. (ed.) CSL 2005. LNCS, vol. 3634, pp. 167–183. Springer, Heidelberg (2005). https://doi.org/10.1007/11538363_13CrossRefGoogle Scholar
 11.de Carvalho, D.: The relational model is injective for multiplicative exponential linear logic. In: 25th EACSL Annual Conference on Computer Science Logic, CSL 2016, Marseille, France, 29 August–1 September 2016, pp. 41:1–41:19 (2016). https://doi.org/10.4230/LIPIcs.CSL.2016.41
 12.DeYoung, H., Caires, L., Pfenning, F., Toninho, B.: Cut reduction in linear logic as asynchronous sessiontyped communication. In: CSL, pp. 228–242 (2012)Google Scholar
 13.Giamberardino, P.D.: Jump from parallel to sequential proofs: additives. Technical report (2011). https://hal.archivesouvertes.fr/hal00616386
 14.Faggian, C., Maurel, F.: Ludics nets, a game model of concurrent interaction. In: 20th IEEE Symposium on Logic in Computer Science (LICS 2005), Chicago, IL, USA, 26–29 June 2005, Proceedings, pp. 376–385. IEEE Computer Society (2005). http://dx.doi.org/10.1109/LICS.2005.25
 15.Faggian, C., Piccolo, M.: A graph abstract machine describing event structure composition. Electr. Notes Theor. Comput. Sci. 175(4), 21–36 (2007). https://doi.org/10.1016/j.entcs.2007.04.014CrossRefzbMATHGoogle Scholar
 16.Di Giamberardino, P., Faggian, C.: Jump from parallel to sequential proofs: multiplicatives. In: Ésik, Z. (ed.) CSL 2006. LNCS, vol. 4207, pp. 319–333. Springer, Heidelberg (2006). https://doi.org/10.1007/11874683_21CrossRefGoogle Scholar
 17.Girard, J.Y.: Linear logic. Theor. Comput. Sci. 50(1), 1–101 (1987)MathSciNetCrossRefGoogle Scholar
 18.Heijltjes, W., Houston, R.: No proof nets for MLL with units: proof equivalence in MLL is PSPACEcomplete. In: CSLLICS 2014, pp. 50:1–50:10. ACM (2014)Google Scholar
 19.Honda, K., Laurent, O.: An exact correspondence between a typed picalculus and polarised proofnets. Theor. Comput. Sci. 411(22–24), 2223–2238 (2010). https://doi.org/10.1016/j.tcs.2010.01.028MathSciNetCrossRefzbMATHGoogle Scholar
 20.Honda, K., Yoshida, N., Berger, M.: Process types as a descriptive tool for interaction. In: Dowek, G. (ed.) RTA 2014. LNCS, vol. 8560, pp. 1–20. Springer, Cham (2014). https://doi.org/10.1007/9783319089188_1CrossRefGoogle Scholar
 21.Hughes, D.J.D., Heijltjes, W.: Conflict nets: efficient locally canonical MALL proof nets. In: Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2016, New York, NY, USA, 5–8 July 2016, pp. 437–446 (2016). http://doi.acm.org/10.1145/2933575.2934559
 22.Hughes, D.J.D., van Glabbeek, R.J.: Proof nets for unitfree multiplicativeadditive linear logic. ACM Trans. Comput. Logic 6(4), 784–842 (2005)MathSciNetCrossRefGoogle Scholar
 23.Laurent, O.: Polarized proofnets and \(\lambda \mu \)calculus. Theor. Comput. Sci. 290(1), 161–188 (2003). https://doi.org/10.1016/S03043975(01)002973MathSciNetCrossRefzbMATHGoogle Scholar
 24.Melliès, P.A.: Asynchronous games 4: a fully complete model of propositional linear logic. In: 20th IEEE Symposium on Logic in Computer Science (LICS 2005), Chicago, IL, USA, 26–29 June 2005, Proceedings, pp. 386–395 (2005). http://dx.doi.org/10.1109/LICS.2005.6
 25.Melliès, P.A., Mimram, S.: Asynchronous games: innocence without alternation. In: Caires, L., Vasconcelos, V.T. (eds.) CONCUR 2007. LNCS, vol. 4703, pp. 395–411. Springer, Heidelberg (2007). https://doi.org/10.1007/9783540744078_27CrossRefGoogle Scholar
 26.Mimram, S.: Sémantique des jeux asynchrones et réécriture 2dimensionnelle (asynchronous game semantics and 2dimensional rewriting systems). Ph.D. thesis, Paris Diderot University, France (2008). https://tel.archivesouvertes.fr/tel00338643
 27.Wadler, P.: Propositions as sessions. J. Funct. Program. 24(2–3), 384–418 (2014)MathSciNetCrossRefGoogle Scholar
 28.Winskel, G.: Event structures. In: Brauer, W., Reisig, W., Rozenberg, G. (eds.) ACPN 1986. LNCS, vol. 255, pp. 325–392. Springer, Heidelberg (1987). https://doi.org/10.1007/3540179062_31CrossRefGoogle Scholar
Copyright information
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.