Causality in Linear Logic

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 cut-elimination 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 multiplicative-exponential fragment of Linear Logic. For additives, a well-known 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.

Proof nets tend to be based on specific representations such as graphs or sets of linkings. Denotational semantics has not managed to provide a semantic counterpart to proof nets, which would be a model where every element is the interpretation of a proof (full completeness) and whose equational theory coincides with commuting conversions (injectivity). We believe this is because denotational semantics views conversions as extensional principles, hence models proofs with extensional objects (relations, functions) too far from the syntax.

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 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.

The true concurrency of conversions. Recent work [5] highlights an interpretation of Linear Logic as communicating processes. Rules become actions whose polarity (input or output) is tied to the polarity of the connective (negative or positive), and cut-elimination becomes communication. In this interpretation, each assumption in the context is assigned a channel on which the proof communicates. Interestingly, commuting conversions can be read as asynchronous permutations. For instance, the conversion mentioned above becomes the equation in the syntax of Wadler [27]:where \(u[\mathtt{inl}]\) corresponds to a \( \oplus _1\)-introduction rule on (the assumption corresponding to) u, and \([u \leftrightarrow v]\) is the counterpart to an axiom between the hypothesis corresponding to u and v. It becomes then natural to consider that the canonical object representing these two proofs should be a concurrent process issuing the two outputs in parallel. A notion of causality emerges from this interpretation, where a rule depends on a previous rule below in the tree when these two rules cannot be permuted using the commuting conversions. This leads us to causal models to make this dependency explicit. For instance, the two processes in (1) can be represented as the partial order depicted in Fig. 1a, where dependency between rules is marked with .

In presence of , a derivation stands for several execution (slices), given by different premises of a -rule (whose process equivalent is \(u{.}{} \mathtt{case}\, (P, Q)\) and represents pattern matching on an incoming message). The identity on \(X \oplus Y\), corresponding to the proofis interpreted by the event structure depicted in Fig. 1b. Event structures [28] combine a partial order, representing causality, with a conflict relation representing when two events cannot belong to the same execution (here, same slice). Conflict here is indicating with and separates the slices. The -introduction becomes two conflicting events.

Conjunctive and disjunctive causalities. Consider the process on the context \(u: (X \oplus X)^\perp , v: (Y \oplus Y)^\perp , w: (X \otimes Y) \oplus (X \otimes Y)\) implementing disjunction:Cuts of \(\mathtt {or}\) against a proof starting with \(u[\mathtt{inl}]\) or \(v[\mathtt{inl}]\) answer on w after reduction: where \((\nu u)(P\mid Q)\) is the process counterpart to logical cuts. This operational behaviour is related to parallel or, evaluating its arguments in parallel and returning true as soon as one returns true. Due to this intentional behaviour, the interpretation of or in prime event structures is nondeterministic (Fig. 2a), as causality in event structures is conjunctive (an event may only occur after all its predecessors have occurred). By moving to general event structures, however, we can make the disjunctive causality explicit and recover determinism (Fig. 2b).

Contributions and outline. Drawing inspiration from the interpretation of proofs in terms of processes, we build a fully complete and injective model of unit-free 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 deadlock-free composition, inspired by the interaction between 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 . 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].

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 process-like 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\(^-\): , where X and 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 , and \(\oplus \) to . An environment is a partial mapping of names to formulas, instead of a multiset of formulas – names disambiguate which assumption a rule acts on.

Proofs as processes. We see proofs of MALL\(^-\) (with MIX) as typing derivations for a variant of the \(\pi \)-calculus [27]. The (untyped) syntax for the processes is as follows:u(v).P denotes an input of v on channel u (used in -introduction) while \(u[v]{.}(P \mid Q)\) denotes output of a fresh channel v along channel u (used in \( \otimes \)-introduction); The term \([u \leftrightarrow v]\) is a link, forwarding messages received on u to v, corresponds to axioms, and conversely; and \((\nu u) (P\mid Q)\) represents a restriction of u in P and Q and corresponds to cuts; \(u{.}{} \mathtt{case}\,(P, Q)\) is an input branching representing -introductions, which interacts with selection, either \(u[\mathtt{inl}].\, R\) or \(u[\mathtt{inr}].\, R\); in \((\nu u) (P\mid Q)\), u is bound in both P and Q, in \(u(v).\, P\), v is bound in P, and in \(u[v].\, (P\mid Q)\), v is only bound in Q.

We now define MALL\(^-\) proofs as typing derivations for processes. The inference rules, recalled in Fig. 3, are from [27]. The links (axioms) are restricted to literals – for composite types, one can use the usual \(\eta \)-expansion laws. There is a straightforward bijection between standard (\( \eta \)-expanded) proofs of MALL\(^-\) and typing derivations.

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 which has two branches. Contexts are defined in Fig. 3, and are assigned a type . It intuitively means that if we plug proofs of \( \varGamma _i\) in the holes, we get back a proof of . 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 well-typed 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.

This section introduces a slight variation on the model of [6]. In Sect. 3.1, we define games as prime event structures with polarities, which are used to interpret formulas. We then introduce general event structures in Sect. 3.2, which are used to define 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 deadlock-free composition.

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.

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.

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.

Adding multiplicative units while keep determinism is difficult, as their commuting conversion is subtle (e.g. conversion for MLL is PSPACE-complete [18]), and exhibit apparent nondeterminism. For instance the following proofs are convertible in MLL:where \(a().\, P\) is the process counterpart to introduction of \(\bot \) and a[] of 1. Intuitively, b[] and c[] can be performed at the start, but as soon as one is performed, the other has to wait for the input on a. This cannot be modelled inside deterministic general event structures, as it is only deterministic against an environment that will emit on b. In contrast, proofs of MALL\(^-\) remain deterministic even if their environment is not total.

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 l-nets [10, 13‐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 which we believe is very related to 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 fully-abstract, 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\(^-\).