1. Optipess strategies are not only regret-minimal (a fact established in [13]) but also admissible—note that there are regret-minimal strategies that are not admissible and *vice versa*. On the way, we show that for any strategy of Eve there is an admissible strategy that performs at least as well; this is a peculiarity of discounted-sum games.

*Structure of the Paper.* Notations and definitions are introduced in Sect. 2. The study of admissibility appears in Sect. 3, and is independent from the complexity analysis of regret. The main algorithm devised in this paper (point 2 above) is presented in Theorem 5, Sect. 6; it relies on technical lemmas that are the focus of Sects. 4 and 5. We encourage the reader to go through the statements of the lemma sections, then through the proof of Theorem 5, to get a good sense of the role each lemma plays.

In more details, in Sect. 4 we provide a crucial lemma that allows to represent long paths succinctly, and in Sect. 5, we argue that the important values of a game (regret, best-case, worst-case) have short witnesses. In Sect. 6, we use these lemmas to devise our algorithms.

# **2 Preliminaries**

We assume familiarity with basic graph and complexity theory. Some more specific definitions and known results are recalled here.

*Game, Play, History.* A *(discounted-sum) game* G is a tuple (V,v0, V∃, E, w, λ) where V is a finite set of vertices, v0 is the starting vertex, V∃ ⊆ V is the subset of vertices that belong to Eve, E ⊆ V × V is a set of directed edges, w: E → Z is an (edge-)weight function, and 0 <λ< 1 is a rational *discount factor*. The vertices in V \ V∃ are said to belong to Adam. Since we consider games played for an infinite number of turns, we will always assume that every vertex has at least one outgoing edge.

A *play* is an infinite path v1v2 ··· ∈ V ω in the digraph (V,E). A *history* h = v1 ··· vn is a finite path. The *length of* h, written |h|, is the number of *edges* it contains: |h| def = n − 1. The set **Hist** consists of all histories that start in v0 and end in a vertex from V∃.

*Strategies.* A *strategy of Eve* in G is a function σ that maps histories ending in some vertex v ∈ V∃ to a neighbouring vertex v (i.e., (v, v ) ∈ E). The strategy σ is *positional* if for all histories h, h ending in the same vertex, σ(h) = σ(h ). *Strategies of Adam* are defined similarly.

A history h = v1 ··· vn is said to be *consistent with a strategy* σ of Eve if for all i ≥ 2 such that vi ∈ V∃, we have that σ(v1 ··· vi−1) = vi. Consistency with strategies of Adam is defined similarly. We write **Hist**(σ) for the set of histories in **Hist** that are consistent with σ. A play is consistent with a strategy (of either player) if all its prefixes are consistent with it.

Given a vertex v and both Adam and Eve's strategies, τ and σ respectively, there is a unique play starting in v that is consistent with both, called the *outcome* of τ and σ on v. This play is denoted **out**v(σ, τ ).

For a strategy σ of Eve and a history h ∈ **Hist**(σ), we let σh be the strategy of Eve that assumes h has already been played. Formally, σh(h ) = σ(h · h ) for any history h (we will use this notation only on histories h that start with the ending vertex of h).

*Values.* The *value of a history* h = v1 ··· vn is the discounted sum of the weights on the edges:

$$\mathbf{Val}(h) \stackrel{\text{def}}{=} \sum\_{i=0}^{|h|-1} \lambda^i w(v\_i, v\_{i+1}) \ .$$

The *value of a play* is simply the limit of the values of its prefixes.

The *antagonistic value* of a strategy σ of Eve with history h = v1 ··· vn is the value Eve achieves when Adam tries to hinder her, after h:

$$\mathbf{a}\mathbf{V}\mathbf{a}\mathbf{l}^h(\sigma) \stackrel{\text{def}}{=} \mathbf{V}\mathbf{a}\mathbf{l}(h) + \lambda^{|h|} \cdot \inf\_{\tau} \mathbf{V}\mathbf{a}(\mathbf{out}^{v\_n}(\sigma\_h, \tau)) \ \ ,$$

where τ ranges over all strategies of Adam. The *collaborative value* **cVal**h(σ) is defined in a similar way, by substituting "sup" for "inf." We write **aVal**h (resp. **cVal**h) for the best antagonistic (resp. collaborative) value achievable by Eve with any strategy.

*Types of Strategies.* A strategy σ of Eve is *strongly worst-case optimal* (SWO) if for every history h we have **aVal**h(σ) = **aVal**h; it is *strongly best-case optimal* (SBO) if for every history h we have **cVal**h(σ) = **cVal**h.

We single out a class of SWO strategies that perform well if Adam turns out to be helping. A SWO strategy σ of Eve is *strongly best worst-case optimal* (SBWO) if for every history h we have **cVal**h(σ) = **acVal**h, where:

$$\mathbf{a}\mathbf{c}\mathbf{V}\mathbf{a}\mathbf{l}^h \stackrel{\text{def}}{=} \sup\{\mathbf{c}\mathbf{V}\mathbf{a}\mathbf{l}^h(\sigma') \mid \sigma' \text{ is a SWO strategy of Eve}\}\dots$$

In the context of discounted-sum games, strategies that are positional and strongly optimal always exist. Furthermore, the set of all such strategies can be characterized by local conditions.

**Lemma 1 (Follows from [20, Theorem 5.1]).** *There exist positional SWO, SBO, and SBWO strategies in every game.  The *regret* of a strategy σ of Eve is the maximal difference between the value obtained by using σ and the value obtained by using an alternative strategy:

$$\mathbf{Reg}\left(\sigma\right) \stackrel{\text{def}}{=} \sup\_{\tau} \left( \left( \sup\_{\sigma'} \mathbf{Val}(\mathbf{out}^{v\_0}(\sigma', \tau)) \right) - \mathbf{Val}(\mathbf{out}^{v\_0}(\sigma, \tau)) \right) \,,$$

where τ and σ range over all strategies of Adam and Eve, respectively. The *(minimal) regret of* G is then **Reg** def = infσ **Reg** (σ).

Regret can also be characterized by considering the point in history when Eve should have done things differently. Formally, for any vertices u and v let **cVal**u ¬v be the maximal **cVal**u(σ) for strategies σ verifying σ(u) = v. Then:

**Lemma 2 ([13, Lemma 13]).** *For all strategies* σ *of Eve:*

$$\mathbf{Reg}\left(\sigma\right) = \sup \left\{ \lambda^n \left( \mathbf{c} \mathbf{Val}\_{\neg\sigma\left(h\right)}^{v\_n} - \mathbf{aVal}^{v\_n}(\sigma\_h) \right) \, \middle| \, h = v\_0 \cdots v\_n \in \mathbf{Hist}(\sigma) \right\} \,\,\dots$$

*Switching and Optipess Strategies.* Given strategies σ1, σ2 of Eve and a *threshold function* t: V∃ → N∪{∞}, we define the *switching strategy* σ1 t →σ2 for any history h = v1 ··· vn ending in V∃ as:

$$
\sigma\_1 \xrightarrow{t} \sigma\_2(h) = \begin{cases}
\sigma\_2(h) & \text{if } (\exists i)[i \ge t(v\_i)], \\
\sigma\_1(h) & \text{otherwise.}
\end{cases}
$$

We refer to histories for which the first condition above holds as *switched histories*, to all others as *unswitched histories*. The strategy σ = σ1 t →σ2 is said to be *bipositional* if both σ1 and σ2 are positional. Note that in that case, for all histories h, if h is switched then σh = σ2, and otherwise σh is the same as σ but with t(v) changed to max{0, t(v) − |h|} for all v ∈ V∃. In particular, if |h| is greater than max{t(v) < ∞}, then σh is nearly positional: it switches to σ2 as soon as it sees a vertex with t(v) = ∞.

A strategy σ is *perfectly optimistic-then-pessimistic* (optipess, for short) if there are positional SBO and SBWO strategies σsbo and σsbwo such that σ = σsbo t →σsbwo where t(v) = inf i ∈ N λi (**cVal**v − **aVal**v) ≤ **Reg** .

**Theorem 1 ([13]).** *For all optipess strategies* σ *of Eve,* **Reg** (σ) = **Reg***.*

*Conventions. As we have done so far, we will assume throughout the paper that a game* G *is fixed—with the notable exception of the results on complexity, in which we assume that the game is given with all numbers in binary. Regarding strategies, we assume that bipositional strategies are given as two positional strategies and a threshold function encoded as a table with binary-encoded entries.*

*Example 1.* Consider the following game, where round vertices are owned by Eve, and square ones by Adam. The double edges represent Eve's positional strategy σ:

Eve's strategy has a regret value of 2λ2/(1 − λ). This is realized when Adam plays from v0 to v1, from v 1 to x, and from v 1 to y. Against that strategy, Eve ensures a discounted-sum value of 0 by playing according to σ while regretting not having played to v 1 to obtain 2λ2/(1 − λ). -

#### **3 Admissible Strategies and Regret**

There is no reason for Eve to choose a strategy that is consistently worse than another one. This classical idea is formalized using the notions of *strategy domination* and *admissible strategies*. In this section, which is independent from the rest of the paper, we study the relation between admissible and regret-minimal strategies. Let us start by formally introducing the relevant notions:

**Definition 1.** *Let* σ1, σ2 *be two strategies of Eve.  We say that* σ1 *is* dominated *by* σ2 *if* σ1 *is* weakly dominated *by* σ2 *but not conversely. A strategy* σ *of Eve is* admissible *if it is not dominated by any other strategy.*

In other words, admissible strategies are maximal elements for the weakdomination pre-order.

*Example 2.* Consider the following game, where the strategy σ of Eve is shown by the double edges:

This strategy guarantees a discounted-sum value of 6λ2(1−λ) against any strategy of Adam. Furthermore, it is worst-case optimal since playing to v1 instead of v2 would allow Adam the opportunity to ensure a strictly smaller value by playing to v 1 . The latter also implies that σ is admissible. Interestingly, playing to v1 is also an admissible behavior of Eve since, against a strategy of Adam that plays from v1 to v 1, it obtains 10λ2(1 − λ) > 6λ2(1 − λ). -

The two examples above can be used to argue that the sets of strategies that are regret minimal and admissible, respectively, are in fact incomparable.

**Proposition 1.** *There are regret-optimal strategies that are not admissible and admissible strategies that have suboptimal regret.*

*Proof (Sketch).* Consider once more the game depicted in Example 1 and recall that the strategy σ of Eve corresponding to the double edges has minimal regret. This strategy is *not* admissible: it is dominated by the alternative strategy σ of Eve that behaves like σ from v1 but plays to v 2 from v2. Indeed, if Adam plays to v1 from v0 then the outcomes of σ and σ are the same. However, if Adam plays to v2 then the value of the outcome of σ is 0 while the value of the outcome of σ is strictly greater than 0.

Similarly, the strategy σ depicted by double edges in the game from Example 2 is admissible but *not* regret-minimizing. In fact, her strategy σ that consists in playing v1 from v0 has a smaller regret.

In the rest of this section, we show that (1) any strategy is weakly dominated by an admissible strategy; (2) being dominated entails more regret; (3) optipess strategies are both regret-minimal and admissible. We will need the following:

**Lemma 3 ([6]).** *A strategy* σ *of Eve is admissible if and only if for every history* h ∈ **Hist**(σ) *the following holds: either* **cVal**h(σ) > **aVal**h *or* **aVal**h(σ) = **cVal**h(σ) = **aVal**h = **acVal**h*.*

The above characterization of admissible strategies in so-called *well-formed games* was proved in [6, Theorem 11]. Lemma 3 follows from the fact that discounted-sum games are well-formed.

#### **3.1 Any Strategy Is Weakly Dominated by an Admissible Strategy**

We show that discounted-sum games have the distinctive property that every strategy is weakly dominated by an admissible strategy. This is in stark contrast with most cases where admissibility has been studied previously [6].

#### **Theorem 2.** *Any strategy of Eve is weakly dominated by an admissible strategy.*

*Proof* (*Sketch).* The main idea is to construct, based on σ, a strategy σ that will switch to a SBWO strategy as soon as σ does not satisfy the characterization of Lemma 3. The first part of the argument consists in showing that σ is indeed weakly dominated by σ . This is easily done by comparing, against each strategy τ of Adam, the values of σ and σ . The second part consists in verifying that σ is indeed admissible. This is done by checking that each history h consistent with σ satisfies the characterization of Lemma 3, that is **cVal**h(σ ) > **aVal**h or **aVal**h(σ ) = **cVal**h(σ ) = **aVal**h = **acVal**h.

#### **3.2 Being Dominated Is Regretful**

**Theorem 3.** *For all strategies* σ, σ *of Eve such that* σ *is weakly dominated by* σ *, it holds that* **Reg** (σ ) ≤ **Reg** (σ)*.*

*Proof.* Let σ, σ be such that σ is weakly dominated by σ . This means that for every strategy τ of Adam, we have that **Val**(π) ≤ **Val**(π ) where π = **out**v0 (σ, τ ) and π = **out**v0 (σ , τ ). Consequently: we obtain

$$\left(\sup\_{\sigma^{\prime\prime}} \mathbf{Val}(\mathbf{out}^{v\_0}(\sigma^{\prime\prime}, \tau))\right) - \mathbf{Val}(\pi^{\prime}) \le \left(\sup\_{\sigma^{\prime\prime}} \mathbf{Val}(\mathbf{out}^{v\_0}(\sigma^{\prime\prime}, \tau))\right) - \mathbf{Val}(\pi) \quad \square$$

As this holds for any τ , we can conclude that supτ supσ-- (**Val**(**out**v0 (σ, τ )) − **Val**(**out**v0 (σ , τ ))) ≤ supτ supσ-- (**Val**(**out**v0 (σ, τ )) − **Val**(**out**v0 (σ, τ ))), that is **Reg** (σ ) ≤ **Reg** (σ).

It follows from Proposition 1, however, that the converse of the theorem is false.

#### **3.3 Optipess Strategies Are both Regret-Minimal and Admissible**

Recall that there are admissible strategies that are not regret-minimal and *vice versa* (Proposition 1). However, as a direct consequence of Theorems 2 and 3, there always exist regret-minimal admissible strategies. It turns out that optipess strategies, which are regret-minimal (Theorem 1), are also admissible:

**Theorem 4.** *All optipess strategies of Eve are admissible.*

*Proof.* Let σ = σsbo t →σsbwo be an optipess strategy; we show it is admissible. To this end, let h = v0 ...vn ∈ **Hist**(σ); we show that one of the properties of Lemma 3 holds. There are two cases:

*(* h *is switched.)* In that case, σh = σsbwo. Since σsbwo is an SBWO strategy, **cVal**h(σsbwo) = **acVal**h. Now if **acVal**h > **aVal**h, then:

$$\mathbf{c}\mathbf{V}\mathbf{a}^h(\sigma) = \mathbf{c}\mathbf{V}\mathbf{a}^h(\sigma^{\text{subwo}}) = \mathbf{a}\mathbf{c}\mathbf{V}\mathbf{a}^h > \mathbf{a}\mathbf{V}\mathbf{a}^h\ \ ,$$

and σ satisfies the first property of Lemma 3. Otherwise **acVal**h = **aVal**h and the second property holds: we have that **cVal**h(σ) = **acVal**h, and as σsbwo is an SWO and **aVal**h(σ) = **aVal**h(σsbwo), we also have that **aVal**h(σ) = **aVal**h.

*(* h *is unswitched.)* We show that **cVal**h(σ) > **aVal**h. Since h is unswitched, we have in particular that:

$$\mathbf{Reg}\left(\sigma\right) = \mathbf{Reg} < \lambda^n \left(\mathbf{cVal}^{v\_n} - \mathbf{aVal}^{v\_n}\right) \ . \tag{1}$$

Furthermore:

$$\begin{split} \lambda^n \left( \mathbf{c} \mathbf{V} \mathbf{al}^{v\_n} - \mathbf{a} \mathbf{V} \mathbf{al}^{v\_n} \right) &= \left( \mathbf{Val}(h) + \lambda^n \mathbf{c} \mathbf{Val}^{v\_n} \right) - \left( \mathbf{Val}(h) + \lambda^n \mathbf{a} \mathbf{Val}^{v\_n} \right) \\ &= \mathbf{c} \mathbf{Val}^h - \mathbf{a} \mathbf{Val}^h \end{split}$$

and combining the previous equation with Eq. 1, we obtain:

$$\mathbf{c} \mathbf{V} \mathbf{a}^h - \mathbf{R} \mathbf{e} \mathbf{g} \left( \sigma \right) > \mathbf{a} \mathbf{V} \mathbf{a}^h \ . $$

To conclude, we show that **Reg** (σ) ≥ **cVal**h − **cVal**h(σ). Consider a strategy τ of Adam such that h is consistent with both σsbo and τ and satisfying **Val**(**out**v0 (σsbo, τ )) = **cVal**h. (That such a τ exists is intuitively clear since σ has been following the SBO strategy σsbo along h.) It holds immediately that **cVal**h(σ) ≥ **Val**(**out**v0 (σ, τ )). Now by definition of the regret:

$$\begin{split} \mathbf{Reg}\left(\sigma\right) &\geq \mathbf{Val}(\mathbf{out}^{v\_{0}}(\sigma^{\text{sbo}},\tau)) - \mathbf{Val}(\mathbf{out}^{v\_{0}}(\sigma,\tau)) \\ &\geq \mathbf{cVal}^{h} - \mathbf{cVal}^{h}(\sigma) \ . \end{split}$$

### **4 Minimal Values Are Witnessed by a Single Iterated Cycle**

We start our technical work towards a better algorithm to compute the regret value of a game. Here, we show that there are succinctly presentable histories that witness small values in the game. Our intention is to later use this result to apply a modified version of Lemma 2 to bipositional strategies to argue there are small witnesses of a strategy having too much regret.

More specifically, we show that for any history h, there is another history h of the same length that has smaller value and such that h = α · βk · γ where |αβγ| is small. This will allow us to find the smallest possible value among exponentially long histories by guessing α, β, γ, and k, which will all be small. This property holds for a wealth of different valuation functions, hinting at possible further applications. For discounted-sum games, the following suffices to prove the desired property holds.

**Lemma 4.** *For any history* h = α · β · γ *with* α *and* γ *same-length cycles:*

min{**Val**(α2 · β), **Val**(β · γ2)} ≤ **Val**(h) .

Within the proof of the key lemma of this section, and later on when we use it (Lemma 9), we will rely on the following notion of cycle decomposition:

**Definition 2.** *A* simple-cycle decomposition *(SCD) is a pair consisting of paths and iterated simple cycles.  We write* D(j) = βk*j* j · αj *and* D( ) = α0 · D(1)D(2)··· D(n)*.*

By carefully iterating Lemma 4, we have:

**Lemma 5.** *For any history* h *there exists an history* h = α · βk · γ *with:*

*Proof.* In this proof, we focus on SCDs for which each path αi is simple; we call them ßCDs. We define a wellfounded partial order on ßCDs. Let D = (αi)n i=0,(βj , kj )n j=1 and D = (α i)n- i=0,(β j , k j )n- j=1 be two ßCDs; we write D < D iff all the following holds:

That this order has no infinite descending chain is clear. We show two claims:

Together they imply that for a smallest ßCD D, D( ) is of the required form. Indeed let j be the unique value for which kj > |V |, then the statement of the Lemma is satisfied by letting α = α0 · D(1)··· D(j − 1), β = βj , k = kj , and γ = αj · D(j + 1)··· D(n).

*Claim 1.* Suppose D has n > |V |. Since all cycles are simple, there are two cycles βj , βj- , j<j , of same length. We can apply Lemma 4 on the path βj · (αjD(j + 1)··· D(j − 1)) · βj- , and remove one of the two cycles while duplicating the other; we thus obtain a similar path of smaller value. This can be done repeatedly until we obtain a path with only one of the two cycles, say βj-, the other case being similar. Substituting this path in D( ) results in:

$$\alpha\_0 \cdot D(1) \cdots D(j) \cdot \left(\alpha\_j \cdot D(j+1) \cdot \cdots D(j'-1) \cdot \beta\_{j'}^{k\_j+k\_{j'}}\right) \cdot \alpha\_{j'} \cdot D(j'+1) \cdot \cdots D(n) \; . \; .$$

This gives rise to a smaller ßCD as follows. If αj−1αj is still a simple path, then the above history is expressible as an ßCD with a smaller number of cycles. Otherwise, we rewrite αj−1αj = α j−1β jα j where α j−1 and α j are simple paths and β j is a simple cycle; since |α j−1α j | < |αj−1αj |, the resulting ßCD is smaller.

*Claim 2.* Suppose D has two kj , kj- > |V |, j<j . Since each cycle in the ßCD is simple, kj and kj are greater than both |βj | and |βj- |; let us write kj = b|βj- | + r with 0 ≤ r < |βj- |, and similarly, kj- = b |βj | + r . We have:

$$D(j)\cdots D(j') = \beta\_j^r \cdot \left( (\beta\_j^{|\beta\_{j'}|})^b \cdot \alpha\_j \cdot D(j+1) \cdot \cdots D(j'-1) \cdot (\beta\_{j'}^{|\beta\_j|})^{b'} \right) \cdot \beta\_{j'}^{r'} \cdot \alpha\_{j'} \cdot \cdots$$

Noting that β|β*j* | j and β |β*j*- | j are cycles of the same length, we can transfer all the occurrences of one to the other, as in Claim 1. Similarly, if two simple paths get merged and give rise to a cycle, a smaller ßCD can be constructed; if not, then there are now at most r < |V | occurrences of βj- (or conversely, r of βj ), again resulting in a smaller ßCD.

### **5 Short Witnesses for Regret, Antagonistic, and Collaborative Values**

We continue our technical work towards our algorithm for computing the regret value. In this section, the overarching theme is that of *short witnesses*. We show that (1) the regret value of a strategy is witnessed by histories of bounded length; (2) the collaborative value of a game is witnessed by a simple path and an iterated cycle; (3) the antagonistic value of a strategy is witnessed by an SCD and an iterated cycle.

#### **5.1 Regret Is Witnessed by Histories of Bounded Length**

**Lemma 6.** *Let* σ = σ1 t →σ2 *be an arbitrary bipositional switching strategy of Eve and let* C = 2|V | + max{t(v) < ∞}*. We have that:*

$$\begin{aligned} \mathbf{Reg}\left(\sigma\right) = \max \left\{ \lambda^n \left( \mathbf{cVal}\_{\neg \sigma(h)}^{v\_n} - \mathbf{aVal}^{v\_n}(\sigma\_h) \right) \right\} \\ h = v\_0 \dots v\_n \in \mathbf{Hist}(\sigma), n \le C \right\} \dots \end{aligned}$$

*Proof.* Consider a history h of length greater than C, and write h = h1 · h2 with |h1| = max{t(v) < ∞}. Let h2 = p · p where p is the maximal prefix of h2 such that h1 · p is unswitched—we set p = if h is switched. Note that one of p or p is longer than |V |—say p, the other case being similar. This implies that there is a cycle in p, i.e., p = α · β · γ with β a cycle. Let h = h1 · α · γ · p ; this history has the same starting and ending vertex as h. Moreover, since |h1| is larger than any value of the threshold function, σh = σh- . Lastly, h is still in **Hist**(σ), since the removed cycle did not play a role in switching strategy. This shows:

$$\mathbf{c}\mathbf{V}\mathbf{al}^{v\_n}\_{\neg\sigma(h)} - \mathbf{a}\mathbf{V}\mathbf{al}^{v\_n}(\sigma\_h) = \mathbf{c}\mathbf{V}\mathbf{al}^{v\_n}\_{\neg\sigma(h')} - \mathbf{a}\mathbf{V}\mathbf{al}^{v\_n}(\sigma\_{h'}) \ .$$

Since the length of h is greater than the length of h , the discounted value for h will be greater than that of h, resulting in a higher regret value. There is thus no need to consider histories of size greater than C.

It may seem from this lemma and the fact that t(v) may be very large that we will need to guess histories of important length. However, since we will be considering bipositional switching strategies, we will only be interested in guessing *some* properties of the histories that are not hard to verify:

**Lemma 7.** *The following problem is decidable in* NP*: Given: A game, a bipositional switching strategy* σ*, a number* n *in binary, a Boolean* b*, and two vertices* v, v *Question: Is there a* h ∈ **Hist**(σ) *of length* n*, switched if* b*, ending in* v*, with* σ(h) = v *?*

*Proof.* This is done by guessing multiple flows within the graph (V,E). Here, we call *flow* a valuation of the edges E by integers, that describes the number of times a path crosses each edge. Given a vector in NE, it is not hard to check whether there is a path that it represents, and to extract the initial and final vertices of that path [17].

We first order the different thresholds from the strategy σ = σ1 t →σ2: let V∃ = {v1, v2,...,vk} with t(vi) ≤ t(vi+1) for all i. We analyze the structure of histories consistent with σ. Let h ∈ **Hist**(σ), and write h = h · h where h is the maximal unswitched prefix of h. Naturally, h is consistent with σ1 and h is consistent with σ2. Then h = h0h1 ··· hi, for some i < |V∃|, with:

To confirm the existence of a history with the given parameters, it is thus sufficient to guess the value i ≤ |V∃|, and to guess i connected flows (rather than paths) with the above properties that are consistent with σ1. Finally, we guess a flow for h consistent with σ2 if we need a switched history, and verify that it is starting at a switching vertex. The flows must sum to n + 1, with the last vertex being v , and the previous v.

#### **5.2 Short Witnesses for the Collaborative and Antagonistic Values**

**Lemma 8.** *There is a set* P *of pairs* (α, β) *with* α *a simple path and* β *a simple cycle such that:*

*–* **cVal**v0 = max{**Val**(α · βω) | (α, β) ∈ P} *and*

*– membership in* P *is decidable in polynomial time w.r.t. the game.*

*Proof.* We argue that the set P of all pairs (α, β) with α a simple path, β a simple cycle, and such that α · β is a path, gives us the result.

The first part of the claim is a consequence of Lemma 1: Consider positional SBO strategies τ and σ of Adam and Eve, respectively. Since they are positional, the path **out**v0 (σ, τ ) is of the form α · βω, as required, and its value is **cVal**v0 . We can thus let P be the set of all pairs obtained from such SBO strategies.

Moreover, it can be easily checked that for all pairs (α, β) such that α· β is a path in the game there exists a pair of strategies with outcome α·βω. (Note that verifying whether α · β is a path can indeed be done in polynomial time given α and β.) Finally, the value **Val**(α · βω) will, by definition, be at most **cVal**v0 .

**Lemma 9.** *Let* σ *be a bipositional switching strategy of Eve. There is a set* K *of pairs* (D, β) *with* D *an SCD and* β *a simple cycle such that:*

*Proof.* We will prove that the set K of all pairs (D, β) with D an SCD of polynomial length (which will be specified below), β a simple cycle, and such that D( ) · β is a path, satisfies our claims.

Let C = max{t(v) < ∞}, and consider a play π consistent with σ that achieves the value **aVal**v0 (σ). Write π = h · π with |h| = C, and let v be the final vertex of h. Naturally:

$$\mathbf{a}\mathbf{V}\mathbf{a}^{v\_0}(\sigma) = \mathbf{V}\mathbf{a}(\pi) = \mathbf{V}\mathbf{a}(h) + \lambda^{|h|}\mathbf{V}\mathbf{a}(\pi')\ .$$

We first show how to replace π by some α · βω, with α a simple path and β a simple cycle. First, since π witnesses **aVal**v0 (σ), we have that **Val**(π ) = **aVal**v(σh). Now σh is positional, because |h| ≥ C. 1 It is known that there are optimal positional antagonistic strategies τ for Adam, that is, that satisfy **aVal**v(σh) = **out**v(σh, τ ). As in the proof of Lemma 8, this implies that **aVal**v(σh) = **Val**(α · βω) = **Val**(π ) for some α and β; additionally, any (α, β) that are consistent with σh and a potential strategy for Adam will give rise to a larger value.

We now argue that **Val**(h) is witnessed by an SCD of polynomial size. This bears similarity to the proof of Lemma 7. Specifically, we will reuse the fact that histories consistent with σ can be split into histories played "between thresholds."

Let us write σ = σ1 t →σ2. Again, we let V∃ = {v1, v2,...,vk} with t(vi) ≤ t(vi+1) for all i and write h = h · h where h is the maximal unswitched prefix of h. We note that h is consistent with σ1 and h is consistent with σ2. Then h = h0h1 ··· hi, for some i < |V∃|, with:

We now diverge from the proof of Lemma 7. We apply Lemma 5 on each hj in the game where the strategy σ1 is hardcoded (that is, we first remove every edge (u, v) ∈ V∃ × V that does not satisfy σ1(u) = v). We obtain a history h 0h 1 ··· h i that is still in **Hist**(σ), thanks to the previous splitting of h. We also apply Lemma 5 to h , this time in the game where σ2 is hardcoded, obtaining h. Since each h j and h are expressed as α·βk · γ, there is an SCD D with no more

1 Technically, σ*h* is positional in the game that records whether the switch was made.

than |V∃| elements that satisfies **Val**(D( )) ≤ **Val**(h)—naturally, since **Val**(h) is minimal and D( ) ∈ **Hist**(σ), this means that the two values are equal. Note that it is not hard, given an SCD D, to check whether D( ) ∈ **Hist**(σ), and that SCDs that are not valued **Val**(h) have a larger value.

# **6 The Complexity of Regret**

We are finally equipped to present our algorithms. To account for the cost of numerical analysis, we rely on the problem PosSLP [2]. This problem consists in determining whether an arithmetic circuit with addition, subtraction, and multiplication gates, together with input values, evaluates to a positive integer. PosSLP is known to be decidable in the so-called counting hierarchy, itself contained in the set of problems decidable using polynomial space.

**Theorem 5.** *The following problem is decidable in* NPPosSLP*: Given: A game, a bipositional switching strategy* σ*, a value* r ∈ Q *in binary Question: Is* **Reg** (σ) > r*?*

*Proof.* Let us write σ = σ1 t →σ2. Lemma 6 indicates that **Reg** (σ) > r holds if there is a history h of some length n ≤ C = 2|V | + max{t(v) < ∞}, ending in some vn such that:

$$
\lambda^n \left( \mathbf{c} \mathbf{V} \mathbf{al}\_{\neg \sigma(h)}^{v\_n} - \mathbf{a} \mathbf{V} \mathbf{al}^{v\_n} (\sigma\_h) \right) > r \; . \tag{2}
$$

Note that since σ is bipositional, we do not need to know everything about h. Indeed, the following properties suffice: its length n, final vertex vn, v = σ(h), and whether it is switched. Rather than guessing h, we can thus rely on Lemma 7 to get the required information. We start by simulating the NP machine that this lemma provides, and verify that n, vn, and v are consistent with a potential history.

Let us now concentrate on the collaborative value that we need to evaluate in Eq. 2. To compute **cVal**, we rely on Lemma 8, which we apply in the game where vn is set initial, and its successor forced not to be v. We guess a pair (αc, βc) ∈ P; we thus have **Val**(αc · βω c ) ≤ **cVal**v*n* ¬σ(h), with at least one guessed pair (αc, βc) reaching that latter value.

Let us now focus on computing **aVal**v*n* (σh). Since σ is a bipositional switching strategy, σh is simply σ where t(v) is changed to max{0, t(v) − n}. Lemma 9 can thus be used to compute our value. To do so, we guess a pair (D, βa) ∈ K; we thus have **Val**(D( )·βω a ) ≥ **aVal**v*n* (σh), and at least one pair (D, βa) reaches that latter value.

Our guesses satisfy:

$$\mathbf{c}\mathbf{V}\mathbf{a}\mathbf{l}^{v\_n}\_{\neg\sigma(h)} - \mathbf{a}\mathbf{V}\mathbf{a}\mathbf{l}^{v\_n}(\sigma\_h) \ge \mathbf{V}\mathbf{a}(\alpha\_\mathbf{c} \cdot \beta\_\mathbf{c}^\omega) - \mathbf{V}\mathbf{a}(D(\star) \cdot \beta\_\mathbf{a}^\omega) \ \ ,$$

and there is a choice of our guessed paths and SCD that gives exactly the lefthand side. Comparing the left-hand side with r can be done using an oracle to PosSLP, concluding the proof.

**Theorem 6.** *The following problem is decidable in* coNPNPPosSLP *: Given: A game, a value* r ∈ Q *in binary Question: Is* **Reg** > r*?*

*Proof.* To decide the problem at hand, we ought to check that *every* strategy has a regret value greater than r. However, optipess strategies being regret-minimal, we need only check this for a class of strategies that contains optipess strategies: bipositional switching strategies form one such class.

What is left to show is that optipess strategies can be encoded in *polynomial space*. Naturally, the two positional strategies contained in an optipess strategy can be encoded succinctly. We thus only need to show that, with t as in the definition of optipess strategies (page 5), t(v) is at most exponential for every v ∈ V∃ with t(v) ∈ N. This is shown in the long version of this paper.

**Theorem 7.** *The following problem is decidable in* coNPNPPosSLP *: Given: A game, a bipositional switching strategy* σ *Question: Is* σ *regret optimal?*

*Proof.* A consequence of the proof of Theorem 5 and the existence of optipess strategies is that the value **Reg** of a game can be computed by a polynomial size arithmetic circuit. Moreover, our reliance on PosSLP allows the input r in Theorem 5 to be represented as an arithmetic circuit without impacting the complexity. We can thus verify that for all bipositional switching strategies σ (with sufficiently large threshold functions) and all possible polynomial size arithmetic circuits, **Reg**(σ) > r implies that **Reg**(σ ) > r. The latter holds if and only if σ is regret optimal since, as we have argued in the proof of Theorem 6, such strategies σ include optipess strategies and thus regret-minimal strategies.

### **7 Conclusion**

We studied *regret*, a notion of interest for an agent that does not want to assume that the environment she plays in is simply adversarial. We showed that there are strategies that both minimize regret, and are not consistently worse than any other strategies. The problem of computing the minimum regret value of a game was then explored, and a better algorithm was provided for it.

The exact complexity of this problem remains however open. The only known lower bound, a straightforward adaptation of [14, Lemma 3] for discounted-sum games, shows that it is at least as hard as solving parity games [15].

Our upper bound could be significantly improved if we could efficiently solve the following problem:

### **PosRatBase**

**Given:** (ai)n i=1 ∈ Zn, (bi)n i=1 ∈ Nn, and r ∈ Q all in binary, **Question:** Is n i=1 ai · rb*i* > 0?

This can be seen as the problem of comparing succinctly represented numbers in a rational base. The PosSLP oracle in Theorem 5 can be replaced by an oracle for this seemingly simpler arithmetic problem. The variant of PosRatBase in which r is an integer was shown to be in P by Cucker, Koiran, and Smale [8], and they mention that the complexity is open for rational values. To the best of our knowledge, the exact complexity of PosRatBase is open even for n = 3.

**Acknowledgements.** We thank Rapha¨el Berthon and Isma¨el Jecker for helpful conversations on the length of maximal (and minimal) histories in discounted-sum games, James Worrell and Jo¨el Ouaknine for pointers on the complexity of comparing succinctly represented integers, and George Kenison for his writing help.

# **References**

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

# **Causality in Linear Logic Full Completeness and Injectivity (Unit-Free Multiplicative-Additive Fragment)**

Simon Castellan(B) and Nobuko Yoshida

Imperial College London, London, UK<EMAIL_ADDRESS>
**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 unit-free 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 semantics

## **1 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 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

**Fig. 1.** Examples of causal invariants

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 - X⊥ ⊕X⊥, X ⊕X 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

$$
\begin{array}{ccc}
\overline{\vdash X^{\perp},X}^{\perp}Ax\\\hline \overline{\vdash X^{\perp},X\oplus X}^{\perp}\oplus\_{\mathbb{I}}\\\hline \overline{\vdash X^{\perp}\oplus X^{\perp},X\oplus X}^{\perp}\end{array}
\oplus\_{\mathbb{I}}\quad\begin{array}{c}
\overline{\vdash X^{\perp},X}^{\perp}Ax\\\hline \overline{\vdash X^{\perp}\oplus X^{\perp},X}^{\perp}\oplus\_{\mathbb{I}}\\\hline \overline{\vdash X^{\perp}\oplus X^{\perp},X\oplus X}^{\perp}\oplus\_{\mathbb{I}}
\end{array}
$$

are due to Abramsky and Melli`es (MALL) [1] and Melli`es (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]:

$$(1)\quad u[\mathtt{in1}].v[\mathtt{in1}].[u\hookrightarrow v] \equiv v[\mathtt{in1}].u[\mathtt{in1}].[u\hookrightarrow v] \not\simeq u: X^\perp \oplus X^\perp, v: X\oplus X,$$

where u[inl] corresponds to a ⊕1-introduction rule on (the assumption corresponding to) u, and [u ↔ 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.case (P, Q) and represents pattern matching on an incoming message). The identity on X ⊕ Y , corresponding to the proof

$$u.\mathsf{cases}\left(v[\mathsf{in1}].\left[u\leftrightarrow v\right],\ v[\mathsf{inr}].\left[u\leftrightarrow v\right]\right)\rhd u:X^\perp\&\ Y^\perp,v:X\oplus Y,$$

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

**Fig. 2.** Representations of or

*Conjunctive and disjunctive causalities.* Consider the process on the context u : (X ⊕ X)⊥, v : (Y ⊕ Y )⊥, w : (X ⊗ Y ) ⊕ (X ⊗ Y ) implementing disjunction:

$$\mathbf{for} = u.\mathbf{case}\begin{pmatrix} v.\mathbf{case}\ (w[\mathtt{in1}].P, w[\mathtt{in1}].P),\\ v.\mathbf{case}\ (w[\mathtt{in1}].P, w[\mathtt{in1}].P) \end{pmatrix}\text{ where }P = w[x].\newline([u \leftrightarrow w] \mid [v \leftrightarrow x]).$$

Cuts of or against a proof starting with u[inl] or v[inl] answer on w after reduction:

$$(\nu u)(\text{or} \mid u[\text{in1}]) \to^\* w[\text{in1}].v.\mathsf{case}\,(P,P) \quad (\nu v)(\text{or} \mid v[\text{in1}]) \to^\* w[\text{in1}].u.\mathsf{case}\,(P,P)$$

where (νu)(P | 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 ⊗ 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 P. 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 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−: T,S ::= X | X⊥ | T ⊗ S | T ` S | T ⊕S | T &S, where X and X⊥ are *atomic formulas* (or *ltterals*) belonging to a set A. Formulas come with the standard notion of duality (·)⊥ given by the De Morgan rules: ⊗ is dual to `, and ⊕ 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 π-calculus [27]. The (untyped) syntax for the processes is as follows:

$$\begin{array}{l} P,Q ::= u(v).P \mid u[v].(P \mid Q) \qquad \text{(multiplicative)}\\ \mid u.\mathsf{case}(P,Q) \mid u[\mathsf{in1}].P \mid u[\mathsf{inr}].P \quad \text{(additives)}\\ \mid u \gets v \mid (\nu u)(P \mid Q) \mid (P \mid Q) \qquad \text{(logical and mix)} \end{array}$$

u(v).P denotes an input of v on channel u (used in `-introduction) while u[v].(P | Q) denotes output of a fresh channel v along channel u (used in ⊗ introduction); The term [u ↔ v] is a *link*, forwarding messages received on u to v, corresponds to axioms, and conversely; and (νu)(P | Q) represents a restriction of u in P and Q and corresponds to cuts; u.case (P, Q) is an input branching representing &-introductions, which interacts with selection, either u[inl]. R or u[inr]. R; in (νu)(P | Q), u is bound in both P and Q, in u(v). P, v is bound in P, and in u[v].(P | 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 η-expansion laws. There is a straightforward bijection between standard (η-expanded) proofs of MALL− and typing derivations.

**Fig. 3.** Typing rules for MALL− (above) and contexts (below)

*Commutation rules and cut elimination.* We now explain the valid commutations rules in our calculus. We consider contexts C [[]1,..., []n] 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 Γi in the holes, we get back a proof of . We use the notation C[Pi]i for C[P1,...,Pn] when (Pi) is a family of processes. Commuting conversion is the smallest congruence ≡ satisfying all well-typed instances of the rule C[D[Pi,j ]j ]i ≡ D[C[Pi,j ]i]j for C and D two contexts. For instance a[inl]. b.case (P, Q) ≡ b.case (a[inl]. P, a[inl]. Q). Figure 4 gives reduction rules P → 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**

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.

**Fig. 4.** Cut elimination in MALL−

#### **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, ≤E, #E) where (E, ≤E) is a partial order and #E is an irreflexive symmetric relation (representing **conflict**) satisfying: (1) if e ∈ E, then [e] := {e ∈ E | e ≤E e} is finite; and (2) if e #E e and e ≤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 *C* (E) for the set of *finite* configurations of E. For any e ∈ E, [e] is a configuration, and so is [e) := [e] \ {e}. We write e e for the immediate causal relation of E defined as e<e with no event between. Similarly, a conflict e#e is **minimal**, denoted , when the [e] ∪ [e ) and [e) ∪ [e ] are configurations. When drawing event structures, only and are represented. We write max(E) for the set of maximal events of E for ≤E. An event e is maximal in x when it has no successor for ≤E in x. We write maxE x for the maximal events of a configuration x ∈ *C* (E).

An event structure E is **confusion-free** when (1) for all then [e) = [e ) and (2) if and then e = e or . As a result, the relation is an equivalence relation whose equivalent classes a are called **cells**.

**Definition 1.** *A game is a confusion-free event structure* A *along with an assignment pol* : A → {−, +} *such that cells contain events of the same polarity, and a function atom*: max(A) → A *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+ ∈ 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·E is E prefixed with a, *i.e.* E ∪ {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* A0 *and* A1 *is the event structure* A0  A1 = ({0} × A0 ∪ {1} × A1, ≤A0A1 , #A0A1 ) *with* (i, a) ≤A0A1 (j, a ) *iff* i = j *and* a ≤A*i* a *; and* (i, a) #A0A1 (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* A0 + A1 *of the two event structures* A0 *and* A1 *has the same partial order as* A0  A1*, and conflict relation* (i, a) #A0+A1 (j, a ) *iff* i = 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⊥. Given x ∈ *C* (A), we define A/x ("A after x") as the subgame of A comprising the events a ∈ A \ x not in conflict with events in x.

*Interpretation of formulas.* The interpretation of the atom X is the game with a single positive event simply written X with *atom*(X) = X, and the interpretation of X⊥ is X⊥, written simply X⊥ in diagrams. For composite formulas, we let (where send, inl and inr are simply labels):

Parallel composition is used to interpret contexts: u1 : T1,...,un : Tn = T1  ...  Tn. The interpretation commutes with duality: T⊥ = T ⊥.

In diagrams, we write moves of a context following the syntactic convention: for instance u[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 send+ and send− respectively. For atoms, we use u : X and u : X⊥.

#### **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 well-defined 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 set-theoretic arguments.

**Definition 4.** *A causal structure (abbreviated as causal struct) on a game* A *is a subset* σ ⊆ *C* (A) *containing ∅ and satisfying the following conditions:*

Configurations of prime event structures satisfy a further axiom, *stability*, which ensures the absence of disjunctive causalities. When σ is a causal struct on A, we write σ : A. We draw as regular event structures, using and . 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  b  c the diagram on the right denotes the following causal struct σ = {x ∈ *C* (A) | c ∈ x ⇒ x ∩ {a, b} = *∅*}.

A **minimal event** of σ : A is an event a ∈ A with {a} ∈ σ. An event a ∈ x ∈ σ is **maximal** in x when x \ {a} ∈ σ. A **prime configuration** of a ∈ A is a configuration x ∈ σ such that a is its unique maximal event. Because of disjunctive causalities, an event a ∈ A can have several distinct prime configurations in

σ (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 σ for the set of **maximal configurations** of σ, ie. those configurations that cannot be further extended.

Even though causality is less clear in general event structures than in prime event structures, we give here a notion of immediate causal dependence that will be central to define acyclic causal structs. Given a causal struct σ : A and x ∈ σ, we define a relation x,σ on x as follows: a x,σ a when there exists a prime configuration y of a such that x ∪ y ∈ σ, and that a is maximal in y \ {a }. This notion is compatible with the drawing above: we have a -*∅* c and b -*∅* c as c has two prime configurations: {a, c} and {b, c}. Causality needs to be contextual, since different slices can implement different causal patterns. Parallel composition and prefixing structures extend to causal structs:

$$\sigma \parallel \tau = \{ x \parallel y \in \ell^{\ell}(A \parallel B) \mid (x, y) \in \sigma \times \tau \} \qquad \qquad a \cdot \sigma = \{ x \in \ell^{\ell}(a \cdot A) \mid x \cap A \in \sigma \}.$$

*Categorical setting.* Causal structs can be composed using the definitions of [6]. Consider σ : A⊥  B and τ : B⊥  C. A **synchronised configuration** is a configuration x ∈ *C* (A  B  C) such that x ∩ (A  B) ∈ σ and x ∩ (B  C) ∈ τ . A synchronised configuration x is **reachable** when there exists a sequence (**covering chain**) of synchronised configurations x0 = *∅* ⊆ x1 ⊆ ... ⊆ xn = x such that xi+1 \xi is a singleton. The reachable configurations are used to define the interaction τ σ, and then after hiding, the composition τ σ:

τ σ = {x is a reachable synchronised configuration} τ σ = {x ∩ (A C) | x ∈ τ σ}.

Unlike in [6], our determinism is strong enough for τ σ to be a causal struct.

**Lemma 1.** *If* σ : A⊥  B *and* τ : B⊥  C *are causal structs then* τ σ *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⊥  A, forwarding negative moves on one side to the positive occurrence on the other side. Following [6], we define ccA = {x  y ∈ *C* (A⊥  A) | y ⊇− A x ∩ y ⊆+ A x} where x ⊆p y means x ⊆ y and *pol*(y \ x) ⊆ {p}.

However, in general copycat is not an identity on all causal structs, only σ ⊆ ccA σ 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 compact-closed category.

*The syntactic tree.* The syntactic tree of a derivation can be read as a causal struct *Tr* (P) on , which will be the basis for our interpretation. It is defined by induction:

$$\begin{aligned} \operatorname{Tr}(\mu(\upsilon).P) &= \mu(\upsilon) \cdot \operatorname{Tr}(P) & \operatorname{Tr}(\mu[\upsilon].(P \mid Q)) &= \iota[\upsilon] \cdot (\operatorname{Tr}(P) \mid \operatorname{Tr}(Q)) \\ \operatorname{Tr}(a.\mathsf{case}\,(P,Q)) &= (a(\operatorname{in} \mathsf{L}) \cdot \operatorname{Tr}(P)) \cup (a(\operatorname{in} \mathsf{r}) \cdot \operatorname{Tr}(Q)) \\ \operatorname{Tr}(a[\mathsf{in} \mathsf{l}].P) &= a[\mathsf{in} \mathsf{l}] \cdot \operatorname{Tr}(P) & \operatorname{Tr}(a[\mathsf{in} \mathsf{r}].P) &= a[\mathsf{in} \mathsf{r}] \cdot \operatorname{Tr}(P) \\ \operatorname{Tr}([a \leftrightarrow b]) &= a\_{\|X\|} \text{ where } \mathcal{A} = a: X^{\perp}, b: X & \operatorname{Tr}(P \mid Q) = \operatorname{Tr}(P) \parallel \operatorname{Tr}(Q) \\ \operatorname{Tr}((\nu a)(P \mid Q)) &= \operatorname{Tr}(P) \odot \operatorname{Tr}(Q) \end{aligned}$$

We use the convention in the diagram, for instance u[v] means the initial 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 deadlock-free 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 σ1 and σ2 play on the game u : X⊥ ⊗ Y ⊥, v : X ` Y , while σ3 plays on the game u : X⊥ ⊗ Y ⊥, v : X ⊗ Y . The causal structs σ2 and σ3 are very close to proof nets, and it is easy to see that σ2 represents a correct proof net while σ3 does not. In particular, there exists a proof P such that *Tr* (P) ⊆ σ2 but there are no such proof Q for σ3. Clearly, σ3 should not be acyclic. But should σ2? After all it is sequentialisable. But, in all sequentialisations of σ2, the par rule v(z) is applied *before* the tensor u[w], and this dependency is not reflected by σ2. Since our goal is exactly to compute these implicit dependencies, we will only consider σ1 to be acyclic, by using a stronger sequentialisation criterion:

**Definition 5.** *A causal struct* σ : Γ *is strongly sequentialisable when for all* x ∈ σ*, there exists with* x ∈ *Tr* (P) *and Tr* (P) ⊆ σ*.*

To understand the difference between σ1 and σ2, we need to look at causal chains. In both σ1 and σ2, we can go from u : X⊥ to w : Y ⊥ by following immediate causal links in any direction, but observe that in σ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* σ : A *and* x ∈ σ *we say that* a, a ∈ A \ x *communicate* outside x *(written* a ↭x,σ a *) when there exists a chain* a x,σ a0 σ ··· x,σ an σ a *where all the* ai ∈ A \ x*, and* x,σ *denotes the symmetric closure of* x,σ*.*

*Communication in MALL.* In presence of additives, immediate causality is not the only vector of communication. Consider the following causal struct σ4, playing on the context u : (A & A) ⊗ (A & A), v : (A ⊕ A)&(A ⊕ A) where A is irrelevant:

This pattern is not strongly sequentialisable: the tensor u[w] must always go after the &-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 (&-introduction rule). Concretely, this means lifting the previous definition at the level of cells. Given an causal struct σ : A and x ∈ σ, along with two cells a, a of A/x, we define the relation a x,σ a when there exists a ∈ a and a ∈ a such that a x,σ a ; and a ↭x,σ a when there exists a x,σ a0 x,σ ··· σ an σ a where all the ai do not intersect x. For instance, the two cells which are successors of the tensor u[w] in σ4 communicate outside the configuration {u[w]} by going through the cell {v(inl), v(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 ∧ a . If a ∧ 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 ∧ a is undefined, or defined and negative, we say that a ∧ 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 a ∧ a of two cells a and a of A is the meet a ∧ a for a ∈ a and a ∈ a : by confusion-freeness, it does not matter which ones are chosen. Similarly, we say that a and a have positive meet if a∧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* σ : A *is acyclic when for all* x ∈ σ*, for any cells* a, a *not intersecting* x *and with positive meet, if* a ↭x,σ a *then* a ∧ a ∈ x*.*

This captures the desired intuition: if a and 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 ∈ B, b ∧ b is defined, hence must be positive either from the point of view of σ or of τ .

**Theorem 1.** *For acyclic causal structs* σ : A⊥  B *and* τ : B⊥  C*, (1) their interaction is* deadlock-free*:* τ σ = (σ  C)∩(A  τ )*; and (2) the causal struct* τ σ *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 deadlock-freeness 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 Well-Linking 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* σ : A *is total when* (1) *for* x ∈ σ*, if* x *is maximal in* σ*, then it is maximal in C* (A)*; and* (2) *for* x ∈ σ *and* a− ∈ A \ x *such that* x ∪ {a} ∈ σ*, then whenever , we also have* x ∪ {a } ∈ σ *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, ) of a x ∈ max *C* (A), and a bijection : (maxA x)− (maxA x)+ preserving the *atom* labelling.

**Definition 9.** *A total causal struct* σ : A *is well-linking when for each* x ∈ max(σ)*, there exists a linking* x *of* x*, such that if* y *is a prime configuration of* x(e) *in* x*, then* max(y \ { 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 well-linking causal struct.* A causal net σ : A induces a set of linkings A, link(σ) := { x | x ∈ max σ}. The mapping link(·) 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 σ : A a causal net and a minimal event a ∈ σ not an atom. We write A/a for A/{a}. Observe that if , it is easy to see that there exists a context such that . Given a causal struct σ : A, we define the causal struct σ/a = {x ∈ *C* (A/a) | x ∪ {a} ∈ σ} : A/a.

**Lemma 2.** σ/a *is a causal net on* A/a*.*

When a is positive, we can further decompose σ/a in disjoint parts thanks to acyclicity. Write a1,..., an for the minimal cells of A/a and consider for n ≥ k > 0, Ak = {a ∈ A/a | cell(a ) ↭{a},σ ak}. Ak contains the events of A/a which σ connects to the k-th successor of a. We also define the set A0 = A/a\ - 1≤k≤n Ak, 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 σ, the Ak are pairwise disjoint, so A/a ∼= A0  ...  An. For 0 ≤ k ≤ n, define σk = *C* (Ak) ∩ σ/a.

**Lemma 3.** σk *is a causal net on* Ak *and we have* σ/a = σ0  ...  σ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* σ : A *is a causal net, then* σ *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 σ ⊆ τ , we can regard τ as a less sequential implementation of σ. 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* σ : A *maximal for inclusion.*

#### **6.1 Causal Invariants as Maximal Causal Nets**

We start by characterising when two causal nets are upper-bounded for inclusion:

#### **Proposition 1.** *Given two causal nets* σ, τ : A*, the following are equivalent:*

*In this case we write* σ ↑ τ *and* σ ∨ τ *is the least upper bound of* σ *and* τ *for* ⊆*.*

It is a direct consequence of Proposition 1 that any causal net σ is included in a unique causal invariant σ↑ : A, defined as: σ↑ = σ⊆τ τ , where τ ranges over causal nets.

**Lemma 4.** *For* σ, τ : A *causal nets,* σ ↑ τ *iff* σ↑ = τ ↑*. Moreover, if* σ *and* τ *are causal invariants,* σ ↑ τ *if and only if* σ = τ *.*

**Fig. 5.** Interpreting P = u(u ). v(v ). w[w ]. ([u ↔ w] | ([w ↔ v ] | [u ↔ v])) in the context u : X ` Z⊥, v : Z ` Y,w : X⊥ ⊗ Y ⊥

The interpretation of a proof is simply defined as P = *Tr* (P)↑. 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 link(P) = link(*Tr* (P)), we have from Lemma 4: link(P) = link(Q) if and only if P = Q. 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* Γ*, we have* P ≡ Q *iff link*(P) = *link*(Q)*.*

As a corollary, we get:

**Theorem 4.** *For cut-free proofs* P, Q *we have* P ≡ Q *iff* P = Q*.*

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: P = - Q≡P *Tr* (Q). This equality justifies our terminology of "causal completeness", as for instance it implies that the minimal events of P 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* σ : A⊥  B *and* τ : B⊥  C *are causal nets, then so is* τ σ*.*

Note that totality requires acyclicity (and deadlock-freedom) to be stable under composition. However, causal invariants are not stable under composition: τ σ might not be maximal, even if τ and σ are. Indeed, during the interaction, some branches of τ will not be explored by σ and vice-versa which can lead to new allowed reorderings. However, we can always embed τ σ into (τ σ)↑:

**Lemma 6.** *Rooted games and causal invariants form a category CInv, where the composition of* σ : A⊥  B *and* τ : B⊥  C *is* (τ σ)↑ *and the identity on* A *is* cc ↑ A*.*

Note that the empty game is an object of **CInv**, as we need a monoidal unit.

*Monoidal-closed structure.* Given two games A and B we define A⊗B as send+ · (A  B), and 1 as the empty game. There is an obvious isomorphism A ⊗ 1 ∼= A and A⊗(B ⊗C) ∼= (A⊗B)⊗C in **CInv**. We now show how to compute directly the functorial action of ⊗, without resorting to ↑. Consider σ ∈ **CInv**(A, B) and τ ∈ **CInv**(C, D). Given x ∈ *C* ((A ⊗ C)⊥  (B ⊗ D)), we define xσ = x ∩ (A⊥  B) and xτ = x ∩ (C⊥  D). If xσ ∈ σ and xτ ∈ τ , we say that x is connected when there exists cells a, b,c and d of A, B, C and D respectively such that a ↭x σ,σ c and b ↭x τ,τ d. We define:

$$\sigma \otimes \tau = \left\{ \begin{array}{l} x \in \mathfrak{G} \left( (A \otimes C)^{\perp} \parallel (B \otimes D) \right) \text{ such that } \colon \\ \quad \text{(1)} \ x \langle \sigma \rangle \in \sigma \text{ and } x \langle \tau \rangle \in \tau \\ \quad \text{(2)} \text{ if } x \text{ is connected and contains } \mathbf{send}^{+}, \text{ then } \mathbf{send}^{-} \in x \end{array} \right\}$$

In (2), send− refers to the minimal move of (A ⊗ C)⊥ and send+ to the one of B ⊗ D. (2) ensures that σ ⊗ τ is acyclic.

**Lemma 7.** *The tensor product defines a symmetric monoidal structure on CInv.*

Define A ` B = (A<sup>⊥</sup> ⊗ B⊥)⊥, ⊥ =1= *∅* and A B = A<sup>⊥</sup> ` B.

**Lemma 8.** *We have a bijection* `B,C *between causal invariants on* A  B  C *and on* A  (B ` C)*. As a result, there is an adjunction* A ⊗ A *.*

Lemma 8 implies that **CInv**((A ⊥) ⊥) **CInv**(A), and **CInv** is ∗-autonomous.

*Cartesian products.* Given two games A, B in **CInv**, we define their product A & B = inl− · A + inr− · B. We show how to construct the pairing of two causal invariants concretely. Given σ ∈ **CInv**(A, B) and τ ∈ **CInv**(A, C), we define the common behaviour of σ and τ on A to be those x ∈ *C* (A⊥) ∩ σ ∩ τ such that for all a, a outside of x with positive meet, a ↭x,σ a iff a ↭x,τ a . We write σ ∩A τ for the set of common behaviours of σ and τ and define: σ, τ = (L− · σ) ∪ (R− · τ ) ∪ σ ∩A τ . The projections are defined using copycat: π1 = {x ∈ *C* ((A & B)⊥  A) | x ∩ (A⊥  A) ∈ cc ↑ A} (and similarly for π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 **CInv** following the structure is the same as ·, however it is computed compositionally without resorting to the ↑ operator. We deduce that our interpretation is invariant by cut-elimination: if P → Q, then P = Q. 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.

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:

$$a(\text{)}.b[\text{]} \mid c[] \equiv a(\text{)}.(b[] \mid c[]) \equiv b[] \mid a(\text{)}.c[] \rhd a: \bot, b: 1, c: 1$$

where a(). P is the process counterpart to introduction of ⊥ 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`es [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 D`,⊗(R) which we believe is very related to P 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 π-calculus [20]. In another direction, we have recently built a fully-abstract, concurrent game semantics model of the synchronous session π-calculus [8]. The difficulty there was to understand name passing and the synchrony of the π-calculus, which is the dual of our objective here: trying to understand the asynchrony behind the conversions of MALL−.

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

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

# **Rewriting Abstract Structures: Materialization Explained Categorically**

Andrea Corradini1, Tobias Heindel2, Barbara K¨onig3, Dennis Nolte3(B) , and Arend Rensink4

> 1 Universit`a di Pisa, Pisa, Italy<EMAIL_ADDRESS>2 University of Hawaii, Honolulu, USA<EMAIL_ADDRESS>3 Universit¨at Duisburg-Essen, Duisburg, Germany {barbara<EMAIL_ADDRESS>4 University of Twente, Enschede, Netherlands<EMAIL_ADDRESS>
**Abstract.** The paper develops an abstract (over-approximating) semantics for double-pushout rewriting of graphs and graph-like objects. The focus is on the so-called materialization of left-hand sides from abstract graphs, a central concept in previous work. The first contribution is an accessible, general explanation of how materializations arise from universal properties and categorical constructions, in particular partial map classifiers, in a topos. Second, we introduce an extension by enriching objects with annotations and give a precise characterization of strongest post-conditions, which are effectively computable under certain assumptions.

# **1 Introduction**

Abstract interpretation [12] is a fundamental static analysis technique that applies not only to conventional programs but also to general infinite-state systems. Shape analysis [30], a specific instance of abstract interpretation, pioneered an approach for analyzing pointer structures that keeps track of information about the "heap topology", e.g., out-degrees or existence of certain paths. One central idea of shape analysis is *materialization*, which arises as companion operation to summarizing distinct objects that share relevant properties. Materialization, a.k.a. partial concretization, is also fundamental in verification approaches based on separation logic [5,6,24], where it is also known as rearrangement [26], a special case of frame inference. Shape analysis—construed in a wide sense—has been adapted to graph transformation [29], a general purpose modelling language for systems with dynamically evolving topology, such as network protocols and cyber-physical systems. Motivated by earlier work of shape analysis for graph

T. Heindel—Partially supported by AFOSR.

c The Author(s) 2019

M. Boja´nczyk and A. Simpson (Eds.): FOSSACS 2019, LNCS 11425, pp. 169–188, 2019. https://doi.org/10.1007/978-3-030-17127-8\_10

transformation [1,2,4,27,28,31], we want to put the materialization operation on a new footing, widening the scope of shape analysis.

A natural abstraction mechanism for transition systems with graphs as states "summarizes" all graphs over a specific *shape graph*. Thus a single graph is used as abstraction for all graphs that can be mapped homomorphically into it. Further annotations on shape graphs, such as cardinalities of preimages of its nodes and general first-order formulas, enable fine-tuning of the granularity of abstractions. While these natural abstraction principles have been successfully applied in previous work [1,2,4,27,28,31], their companion materialization constructions are notoriously difficult to develop, hard to understand, and are redrawn from scratch for every single setting. Thus, we set out to explain materializations based on mathematical principles, namely universal properties (in the sense of category theory). In particular, partial map classifiers in the topos of graphs (and its slice categories) cover the purely structural aspects of materializations; this is related to final pullback complements [13], a fundamental construction of graph rewriting [7,25]. Annotations of shape graphs are treated orthogonally via op-fibrations.

The first milestones of a general framework for shape analysis of graph transformation and more generally rewriting of objects in a topos are the following: - A rewriting formalism for graph abstractions that lifts the rule-based rewriting from single graphs to *abstract graphs*; it is developed for (abstract) objects in a topos.

*Related work:* The idea of shape graphs together with shape constraints was pioneered in [30] where the constraints are specified in a three-valued logic. A similar approach was proposed in [31], using first-order formulas as constraints. In partner abstraction [3,4], cluster abstraction [1,2], and neighbourhood abstraction [28] nodes are clustered according to local criteria, such as their neighbourhood and the resulting graph structures are enriched with counting constraints, similar to our constraints. The idea of counting multiplicities of nodes and edges is also found in canonical graph shapes [27]. The uniform treatment of monoid annotations was introduced in previous work [9,10,20], in the context of type systems and with the aim of studying decidability and closure properties, but not for abstract rewriting.

### **2 Preliminaries**

This paper presupposes familiarity with category theory and the topos structure of graphs. Some concepts (in particular elementary topoi, subobject and partial map classifiers, and slice categories) are defined in the full version of this paper [8], which also contains all the proofs.

The rewriting formalism for graphs and graph-like structures that we use throughout the paper is the double-pushout (DPO) approach [11]. Although it was originally introduced for graphs [16], it is well-defined in any category **C**. However, certain standard results for graph rewriting require that the category **C** has "good" properties. The category of graphs is an elementary topos—an extremely rich categorical structure—but weaker conditions on **C**, for instance adhesivity, have been studied [14,15,21].

**Definition 1 (Double-pushout rewriting).** *A* production *in* **C** *is a span of monos* L I R *in* **C***; the objects* L *and* R *are called left- and right-hand side, respectively. A* match *of a production* p: L I R

*to an object* X *of* **C** *is a mono* mL : L X *in* **C***. The production* p *rewrites* X *to* Y *at* mL *(resp. the match* mL *to the* co-match mR : R → Y *) if the production and the match (and the co-match) extend to a diagram in* **C***, shown to the right, such that both squares are pushouts.* LIR XCY mL (PO) (PO) mR

*In this case, we write* X p,mL =⇒ Y *(resp.* (L mL X) p ⇒ (R m →R Y )*). We also write* X p,mL =⇒ *if there exists an object* Y *such that* X p,mL =⇒ Y *and* X p ⇒ Y *if the specific match* mL *is not relevant.*

Given a production p and a match mL, if there exist arrows X ← C and C ← I that make the left-hand square of the diagram in Definition 1 a pushout square, then the *gluing condition* is satisfied.

If **C** is an adhesive category (and thus also if it is a topos [22]) and the production consists of monos, then all remaining arrows of double-pushout diagrams of rewriting are monos [21] and the result of rewriting—be it the object Y or the co-match mR—is unique (up to a canonical isomorphism).

#### **2.1 Subobject Classifiers and Partial Map Classifiers of Graphs**

A standard category for graph rewriting that is also a topos is the category of edge-labelled, directed graphs that we shall use in examples, as recalled in the next definition. Note that due to the generality of the categorical framework, our results also hold for various other forms of graphs, such as node-labelled graphs, hypergraphs, graphs with scopes or graphs with second-order edges.

**Definition 2 (Category of graphs).** *Let* Λ *be a fixed set of* edge labels*. A* (Λ-labelled) graph *is a tuple* G = (VG, EG, *src*G,*tgt*G, G) *where* VG *is a finite set of* nodes*,* EG *is a finite set of* edges*, src*G,*tgt*G : EG → VG *are the* source *and* target mappings *and* G : EG → Λ *is the* labelling function*.*

*Let* G, H *be two* Λ*-labelled graphs. A* graph morphism ϕ: G → H *consists of two functions* ϕV : VG → VH*,* ϕE : EG → EH*, such that for each edge* e ∈ EG *we have src*H(ϕE(e)) = ϕV (*src*G(e))*, tgt*H(ϕE(e)) = ϕV (*tgt*G(e)) *and* H(ϕE(e)) = G(e)*. If* ϕV , ϕE *are both bijective,* ϕ *is an isomorphism. The category having (*Λ*-labelled) graphs as objects and graph morphisms as arrows is denoted by* **Graph***.*

We shall often write ϕ instead of ϕV or ϕE to avoid clutter. The graph morphisms in our diagrams will be indicated by black and white nodes and thick edges. In the category **Graph**, where the objects are labelled graphs over the label alphabet Λ, the subobject classifier true is displayed to the right where every Λ-labelled edge represents several edges, one for each λ ∈ Λ.

The subobject classifier true: **1** Ω from the terminal object **1** to Ω allows us to single out a subgraph X of a graph Y , by mapping Y to Ω in such a way that all elements of X are mapped to the image of true.

Given arrows α, m as in the diagram in Definition 3, we can construct the most general pullback, called final pullback complement [7,13].

**Definition 3 (Final pullback complement).** *A pair of arrows* I γ → F β → G *is a* final pullback complement (FPBC) *of another pair* I α → L m → G *if*

LI I GF F α (FPBC) γ α- f γ- β β- f-

Final pullback complements and subobject classifiers are closely related to partial map classifiers (see [13, Corollary 4.6]): a category has FPBCs (over monos) and a subobject classifier if and only if it has a partial map classifier. These exist in all elementary topoi.

**Proposition 4 (Final pullback complements, subobject and partial map classifiers).** *Let* **C** *be a category with finite limits. Then the following are equivalent:*

#### **2.2 Languages**

The main theme of the paper is "simultaneous" rewriting of entire sets of objects of a category by means of rewriting a single *abstract* object that represents a collection of structures—the *language* of the abstract object. The simplest example of an abstract structure is a plain object of a category to which we associate the language of objects that can be mapped to it; the formal definition is as follows (see also [10]).

**Definition 5 (Language of an object).** *Let* A *be an object of a category* **C***. Given another object* X*, we write* X A *whenever there exists an arrow from* X *to* A*. We define the* language1 *of* A*, denoted by* L(A)*, as* L(A) = {X ∈ **C** | X A}*.*

Whenever X ∈ L(A) holds, we will say that X is *abstracted by* A, and A is called the *abstract object*. In the following we will also need to characterize a class of (co-)matches which are represented by a given (co-)match (which is a mono).

**Definition 6 (Language of a mono).** *Let* ϕ: L A *be a mono in* **C***. The* language *of* ϕ *is the set of monos* m *with source* L *that factor* ϕ *such that the square on the right is a pullback:*

$$\mathcal{L}(\varphi) = \{ m \colon L \longmapsto X \mid \exists (\psi \colon X \to A) \begin{array}{c} L \longmapsto \xrightarrow{m} X \\ \stackrel{id\_L}{\downarrow} \xleftarrow{(\mathbb{P}B)} \downarrow \psi \\ L \longmapsto \xrightarrow{} A \end{array} \tag{1}$$

Intuitively, for any arrow (L m → X) ∈ L(ϕ) we have X ∈ L(A) and X has a distinguished subobject L which corresponds precisely to the subobject L A. In fact ψ restricts and co-restricts to an isomorphism between the images of L in X and A. For graphs, no nodes or edges in X outside of L are mapped by ψ into the image of L in A.

# **3 Materialization**

Given a production p : L I R, an abstract object A, and a (possibly non-monic) arrow ϕ: L → A, we want to transform the abstract object A in order to characterize all successors of objects in L(A), i.e., those obtained by rewriting via p at a match compatible with ϕ. (Note that ϕ is not required to be monic, because a monic image of the left-hand side of p in an object of L(A) could be mapped non-injectively to A.) Roughly, we want to lift DPO rewriting to the level of abstract objects.

For this, it is necessary to use the materialization construction, defined categorically in Sect. 3.1, that enables us to concretize an instance of a left-hand side in a given abstract object. This construction is refined in Sect. 3.2 where we restrict to materializations that satisfy the gluing condition and can thus be rewritten via p. Finally in Sect. 3.3 we present the main result about materializations showing that we can fully characterize the co-matches obtained by rewriting.

1 Here we assume that **C** is essentially small, so that a language can be seen as a set instead of a proper class of objects.

#### **3.1 Materialization Category and Existence of Materialization**

From now on we assume **C** to be an elementary topos. We will now define the materialization, which, given an arrow ϕ: L → A, characterizes all objects X, abstracted over A, which contain a (monic) occurrence of the left-hand side compatible with ϕ.

**Definition 7 (Materialization).** *Let* ϕ: L → A *be an arrow in* **C***. The* materialization category *for* ϕ*, denoted* **Mat**ϕ*, has as*

**objects** *all factorizations* L X → A *of* ϕ *whose first factor* L X *is a mono, and as* **arrows** *from a factorization* L X → A *to another one* L Y → A*, all arrows* f : X → Y *in* **C** *such that the diagram to the right is made of a commutative triangle and a pullback square.*

*If* **Mat**ϕ *has a terminal object it is denoted by* L ϕ→ A *and is called the* materialization *of* ϕ*.*

Sometimes we will also call the object ϕ the materialization of ϕ, omitting the arrows.

Since we are working in a topos by assumption, the slice category over A provides us with a convenient setting to construct materializations. Note in particular that in the diagram in Definition 7 above, the span X L L is a partial map from X to L in the slice category over A. Hence the materialization ϕ corresponds to the partial map classifier for L in this slice category.

**Proposition 8 (Existence of materialization).** *Let* ϕ: L → A *be an arrow in* **C***, and let* ηϕ : ϕ → F(ϕ)*, with* F(ϕ): A¯ → A*, be the partial map classifier of* ϕ *in the slice category* **C**↓A *(which also is a topos).*2 *Then* L ηϕ → A¯ F (ϕ) → A *is the materialization of* ϕ*, hence* ϕ = A¯*.*

As a direct consequence of Propositions 4 and 8 (and the fact that final pullback complements in the slice category correspond to those in the base category [25]), the terminal object of the materialization category can be constructed for each arrow of a topos by taking final pullback complements.

**Corollary 9 (Construction of the materialization).** *Let* ϕ: L → A *be an arrow of* **C** *and let* trueA : A A × Ω *be the subobject classifier (in the slice category* **C** ↓ A*) from id*A : A → A *to the projection* π1 : A × Ω → A*.* ηϕ ϕ

*Then the terminal object* L ηϕ ϕ ψ → A *in the materialization category consists of the arrows* ηϕ *and* ψ = π1 ◦ χηϕ *, where* L ηϕ ϕ χηϕ → A × Ω *is the final pullback complement of* L ϕ → A trueA A × Ω*.* L ϕ --

χηϕ

ψ

-- A trueA A × Ω π1 (FPBC) A

2 This is by the Fundamental Theorem of topos theory [17, Theorem 2.31].

*Example 10.* We construct the materialization L ηϕ ϕ ψ → A for the following morphism ϕ: L → A of graphs with a single (omitted) label:

$$
\varphi \underbrace{\cdots \longrightarrow \cdots}\_{\ell}
$$

In particular, the materialization is obtained as a final pullback complement as depicted to the right (compare with the corresponding diagram in Corollary 9). Note that edges which are not in the image of ηϕ resp. trueA are dashed.

This construction corresponds to the usual intuition behind materialization: the left-hand side and the edges that are attached to it are "pulled out" of the given abstract graph.

We can summarize the result of our constructions in the following proposition:

**Proposition 11 (Language of the materialization).** *Let* ϕ: L → A *be an arrow in* **C** *and let* L ηϕ ϕ→ A *be the corresponding materialization. Then we have*

> L(L ηϕ ϕ ) = {L mL X | ∃ψ: (X → A). (ϕ = ψ ◦ mL)}.

#### **3.2 Characterizing the Language of Rewritable Objects**

A match obtained through the materialization of the left-hand side of a production from a given object may not allow a DPO rewriting step because of the gluing condition. We illustrate this problem with an example.

> L

*Example 12.* Consider the materialization L ϕ→ A from Example 10 and the production L I R shown in the diagram to the right. It is easy to see that the pushout complement of morphisms I L ϕ does not exist. ϕ

Nevertheless there exist factorizations L X → A abstracted by ϕ that could be rewritten using the production.

In order to take the existence of pushout complements into account, we consider a subcategory of the materialization category.

**Definition 13 (Materialization subcategory of rewritable objects).** *Let* ϕ: L → A *be an arrow of* **C** *and let* ϕL : I L *be a mono (corresponding to the left leg of a production). The* materialization subcategory of rewritable objects *for* ϕ *and* ϕL*, denoted* **Mat**ϕL ϕ *, is the full subcategory of* **Mat**ϕ *containing as objects all factorizations* L m X → A *of* ϕ*, where* m *is a mono and* I ϕL L m X *has a pushout complement.*

*Its terminal element, if it exists, is denoted by* L nL ϕ, ϕL→ A *and is called the* rewritable materialization*.*

We show that this subcategory of the materialization category has a terminal object.

**Proposition 14 (Construction of the rewritable materialization).** *Let* ϕ: L → A *be an arrow and let* ϕL : I L *be a mono of* **C***. Then the* rewritable materialization of ϕ w.r.t. ϕL *exists and can be constructed as the following factorization* L nL ϕ, ϕL ψ◦α −→ A *of* ϕ*. In the left diagram,* F *is obtained as the final pullback complement of* I ϕL L ϕ *, where* L ϕ ψ → A *is the materialization of* ϕ *(Definition 7). Next in the right diagram* L nL ϕ, ϕL β F *is the pushout of the span* L ϕL I F *and* α *is the resulting mediating arrow.*

*Example 15.* We come back to the running example (Example 12) and, as in Proposition 14, determine the final pullback complement I F ϕ of I ϕL L ϕ (see diagram below left) and obtain ϕ, ϕL by taking the pushout over L I F (see diagram below right).

It remains to be shown that L ϕ, ϕL→ A represents every factorization which can be rewritten. As before we obtain a characterization of the rewritable objects, including the match, as the language of an arrow.

**Proposition 16 (Language of the rewritable materialization).** *Assume there is a production* p: L ϕL I ϕR R *and let* L nL ϕ, ϕL *be the match for the rewritable materialization for* ϕ *and* ϕL*. Then we have*

$$\mathcal{L}(L \stackrel{n\_L}{\longmapsto} \langle \langle \varphi, \varphi\_L \rangle \rangle) = \{ L \stackrel{m\_L}{\longmapsto} X \mid \exists \psi \colon (X \to A) . \ (\varphi = \psi \circ m\_L \land X \stackrel{p, m\_L}{\Longrightarrow}) \}.$$

#### **3.3 Rewriting Materializations**

In the next step we will now rewrite the rewritable materialization ϕ, ϕL with the match L nL ϕ, ϕL , resulting in a co-match R B. In particular, we will show that this co-match represents all co-matches that can be obtained by rewriting an object X of L(A) at a match compatible with ϕ. We first start with an example.

*Example 17.* We can rewrite the materialization L ϕ, ϕL→ A as follows:

**Proposition 18 (Rewriting abstract matches).** *Let a match* nL : L A˜ *and a production* p: L I R *be given. Assume that* A˜ *is rewritten along the match* nL*, i.e.,* (L nL A˜) p ⇒ (R nR B)*. Then*

$$\mathcal{L}(R \stackrel{n\_R}{\rightleftarrows} B) = \{ R \stackrel{m\_R}{\rightleftarrows} Y \mid \exists (L \stackrel{m\_L}{\rightleftarrows} X) \in \mathcal{L}(L \stackrel{n\_L}{\rightleftarrows} \tilde{A}). \ \left( (L \stackrel{m\_L}{\rightleftarrows} X) \stackrel{p}{\Rightarrow} (R \stackrel{m\_R}{\rightleftarrows} Y) \} $$

If we combine Propositions 16 and 18, we obtain the following corollary that characterizes the co-matches obtained from rewriting a match compatible with ϕ: L → A.

**Corollary 19 (Co-match language of the rewritable materialization).** *Let* ϕ: L → A *and a production* p: L ϕL I ϕR R *be given. Assume that* ϕ, ϕL *is obtained as the rewritable materialization of* ϕ *and* ϕL *with match* L nL ϕ, ϕL *(see Proposition 14). Furthermore let* (L nL ϕ, ϕL ) p ⇒ (R nR B)*. Then*

$$\mathcal{L}(R \stackrel{n\_R}{\underset{}{\rightleftarrows}} B) = \{ R \stackrel{m\_R}{\underset{}{\rightleftarrows}} Y \mid \exists (L \stackrel{m\_L}{\underset{}{\rightleftarrows}} X), (X \stackrel{\psi}{\rightarrow} A). \ (\varphi = \psi \circ m\_L \land \varphi)$$

$$(L \stackrel{m\_L}{\underset{}{\rightleftarrows}} X) \stackrel{p}{\Rightarrow} (R \stackrel{m\_R}{\underset{}{\rightleftarrows}} Y))$$

This result does not yet enable us to construct post-conditions for languages of objects. The set of co-matches can be fully characterized as the language of a mono, which can only be achieved by fixing the right-hand side R and thus ensuring that exactly one occurrence of R is represented. However, as soon as we forget about the co-match, this effect is gone and can only be retrieved by adding annotations, which will be introduced next.

# **4 Annotated Objects**

We now endow objects with annotations, thus making object languages more expressive. In particular we will use ordered monoids in order to annotate objects. Similar annotations have already been studied in [20] in the context of type systems and in [10] with the aim of studying decidability and closure properties, but not for abstract rewriting.

**Definition 20 (Ordered monoid).** *An* ordered monoid (M, +, ≤) *consists of a set* M*, a partial order* ≤ *and a binary operation* + *such that* (M, +) *is a monoid with unit* 0 *(which is the bottom element wrt.* ≤*) and the partial order is compatible with the monoid operation. In particular* a ≤ b *implies* a + c ≤ b + c *and* c + a ≤ c + b *for all* a, b, c ∈ M*. An ordered monoid is commutative if* + *is commutative.*

*A tuple* (M, +, −, ≤)*, where* (M, +, ≤) *is an ordered monoid and* − *is a binary operation on* M*, is called an* ordered monoid with subtraction*.*

*We say that subtraction is* well-behaved *whenever for all* a, b ∈ M *it holds that* a − a = 0 *and* (a − b) + b = a *whenever* b ≤ a*.*

For now subtraction is just any operation, without specific requirements. Later we will concentrate on specific subtraction operations and demand that they are well-behaved.

In the following we will consider only commutative monoids.

**Definition 21 (Monotone maps and homomorphisms).** *Let* M1*,* M2 *be two ordered monoids. A map* h: M1 → M2 *is called* monotone *if* a ≤ b *implies* h(a) ≤ h(b) *for all* a, b ∈ M1*. The category of ordered monoids with subtraction and monotone maps is called* **Mon***.*

*A monotone map* h *is called a* homomorphism *if* h(0) = 0 *and* h(a + b) = h(a) + h(b)*. If* M1,M2 *are ordered monoids with subtraction, we say that* h *preserves subtraction if* h(a − b) = h(a) − h(b)*.*

*Example 22.* Let n ∈ N\{0} and take Mn = {0, 1, . . . , n, ∗} (zero, one, ... , n, many) with 0 ≤ 1 ≤ ··· ≤ n ≤ ∗ and addition as (commutative) monoid operation with the proviso that a+b = ∗ if the sum is larger than n. In addition a + ∗ = ∗ for all a ∈ Mn. Subtraction is truncated subtraction where a − b = 0 if a ≤ b. Furthermore ∗ − a = ∗ for all a ∈ N. It is easy to see that subtraction is well-behaved.

Given a set S and an ordered monoid (with subtraction) M, it is easy to check that also MS is an ordered monoid (with subtraction), where the elements are functions from S to M and the partial order, the monoidal operation and the subtraction are taken pointwise.

The following path monoid is useful if we want to annotate a graph with information over which paths are present. Note that due to the possible fusion of nodes and edges caused by the abstraction, a path in the abstract graph does not necessarily imply the existence of a corresponding path in a concrete graph. Hence annotations based on such a monoid, which provide information about the existence of paths, can yield useful additional information.

*Example 23.* Given a graph G, we denote by E+ G ⊆ VG×VG the transitive closure of the edge relation E→ G = {(*src*G(e),*tgt*G(e)) | e ∈ EG}. The *path monoid* PG of G has the carrier set P(E+ G). The partial order is simply inclusion and the monoid operation is defined as follows: given P0, P1 ∈ PG, we have

$$\begin{aligned} P\_0 + P\_1 = \{ (v\_0, v\_n) \mid \exists v\_1, \dots, v\_{n-1} \colon (v\_i, v\_{i+1}) \in P\_{ji}, \\ \quad j\_0 \in \{0, 1\}, j\_{i+1} = 1 - j\_i, i \in \{0, \dots, n-1\} \text{ and } n \in \mathbb{N} \} .\end{aligned}$$

That is, new paths can be formed by concatenating alternating path fragments from P0, P1. It is obvious to see that + is commutative and one can also show associativity. P = ∅ is the unit. Subtraction simply returns the first parameter: P0 − P1 = P0.

We will now formally define annotations for objects via a functor from a given category to **Mon**.

**Definition 24 (Annotations for objects).** *Given a category* **C** *and a functor* A: **C** → **Mon***, an* annotation based on A *for an object* X ∈ **C** *is an element* a ∈ A(X)*. We write* Aϕ*, instead of* A(ϕ)*, for the action of functor* A *on a* **C***-arrow* ϕ*. We assume that for each object* X *there is a* standard annotation *based on* A *that we denote by* sX*, thus* sX ∈ A(X)*.*

It can be shown quite straightforwardly that the forgetful functor mapping an annotated object X[a], with a ∈ A(X), to X is an op-fibration (or co-fibration [19]), arising via the Grothendieck construction.

Our first example is an annotation of graphs with global multiplicities, counting nodes and edges, where the action of the functor is to sum up those multiplicities.

*Example 25.* Given n ∈ N\{0}, we define the functor Bn : **Graph** → **Mon**: For every graph G, Bn(G) = MVG∪EG n . For every graph morphism ϕ: G → H and a ∈ Bn(G), we have Bn ϕ(a) ∈ MVH∪EH n with:

$$\mathcal{B}^n\_\varphi(a)(y) = \sum\_{\varphi(x) = y} a(x), \quad where \ x \in (V\_G \cup E\_G) \text{ and } y \in (V\_H \cup E\_H).$$

Therefore an annotation based on a functor Bn associates every item of a graph with a number (or the top value ∗). We will call such annotations *multiplicities*. Furthermore the action of the functor on a morphism transforms a multiplicity by summing up (in Mn) the values of all items of the source graph that are mapped to the same item of the target graph.

For a graph G, its *standard multiplicity* sG ∈ Bn(G) is defined as the function which maps every node and edge of G to 1.

As another example we consider local annotations which record the outdegree of a node and where the action of the functor is to take the supremum instead of the sum.

*Example 26.* Given n ∈ N\{0}, we define the functor Sn : **Graph** → **Mon** as follows: For every graph G, Sn(G) = MVG n . For every graph morphism ϕ: G → H and a ∈ Sn(G), we have Sn ϕ(a) ∈ MVH n with:

$$\mathcal{S}^n\_\varphi(a)(w) = \bigvee\_{\varphi(v) = w} a(v), \quad where \ v \in V\_G \text{ and } w \in V\_H.$$

For a graph G, its *standard annotation* sG ∈ Sn(G) is defined as the function which maps every node of G to its out-degree (or ∗ if the out-degree is larger than n).

Finally, we consider annotations based on the path monoid (see Example 23).

*Example 27.* We define the functor T : **Graph** → **Mon** as follows: For every graph G, T (G) = PG. For every graph morphism ϕ: G → H and P ∈ T (G), we have Tϕ(P) ∈ PH with:

$$\mathcal{T}\_{\varphi}(P) = \{ (\varphi(v), \varphi(w)) \mid (v, w) \in P \}.$$

For a graph G, its *standard annotation* sG ∈ T (G) is the transitive closure of the edge relation, i.e., sG = E+ G.

In the following we will consider only annotations satisfying certain properties in order to achieve soundness and completeness.

**Definition 28 (Properties of annotations).** *Let* A : **C** → **Mon** *be an annotation functor, together with standard annotations. In this setting we say that*

	- Aϕ : A(A) → A(B) *has a right adjoint red*ϕ : A(B) → A(A)*, i.e., red*ϕ *is monotone and satisfies* a ≤ *red*ϕ(Aϕ(a)) *for* a ∈ A(A) *and* Aϕ(*red*ϕ(b)) ≤ b *for* b ∈ A(B)*.* 3

3 This amounts to saying that the forgetful functor is a bifibration when we restrict to monos, see [19, Lem. 9.1.2].

*Furthermore, assuming that* Aϕ *has a right adjoint red*ϕ*, we say that*

*– the* pushout property *holds, whenever for each pushout as shown in the diagram to the right, with all arrows monos where* η = ψ1 ◦ ϕ1 = ψ2 ◦ ϕ2*, it holds that for every* d ∈ A(D)*:*

$$d = \mathcal{A}\_{\psi\_1}(red\_{\psi\_1}(d)) + (\mathcal{A}\_{\psi\_2}(red\_{\psi\_2}(d)) - \mathcal{A}\_{\eta}(red\_{\eta}(d))).$$

*We say that the* pushout property for standard annotations *holds if we replace* d *by* sD*, red* η(d) *by* sA*, red*ψ1 (d) *by* sB *and red*ψ2 (d) *by* sC *.*

*– the* Beck-Chevalley property *holds if whenever the square shown to the right is a pullback with* ϕ1*,* ψ2 *mono, then it holds for every* b ∈ A(B) *that*

$$\mathcal{A}\_{\varphi\_2}(red\_{\varphi\_1}(b)) = red\_{\psi\_2}(\mathcal{A}\_{\psi\_1}(b)).$$

Note that the annotation functor from Example 25 satisfies all properties above, whereas the functors from Examples 26 and 27 satisfy both the homomorphism property and the pushout property for standard annotations, but do not satisfy all the remaining requirements [8].

We will now introduce a more flexible notion of language, by equipping the abstract objects with two annotations, establishing lower and upper bounds.

**Definition 29 (Doubly annotated object).** *Given a topos* **C** *and a functor* A: **C** → **Mon***, a* doubly annotated object A[a1, a2] *is an object* A *of* **C** *with two annotations* a1, a2 ∈ A(A)*.An arrow* ϕ: A[a1, a2] → B[b1, b2]*, also called a* legal arrow*, is a* **C***-arrow* ϕ: A → B *such that* Aϕ(a1) ≥ b1 *and* Aϕ(a2) ≤ b2*.*

*The* language of a doubly annotated object A[a1, a2] *(also called the language of objects which are abstracted by* A[a1, a2]*) is defined as follows:*

$$\mathcal{L}(A[a\_1, a\_2]) = \{ X \in \mathbf{C} \mid \text{there exists a legal arrow } \varphi \colon X[s\_X, s\_X] \to A[a\_1, a\_2] \}$$

Note that legal arrows are closed under composition [9]. Examples of doubly annotated objects are given in Example 36 for global annotations from Example 25 (providing upper and lower bounds for the number of nodes resp. edges in the preimage of a given element). Graph elements without annotation are annotated by [0, ∗] by default.

**Definition 30 (Isomorphism property).** *An annotation functor* A: **C** → **Mon***, together with standard annotations, satisfies the* isomorphism property *if the following holds: whenever* ϕ: X[sX, sX] → Y [sY , sY ] *is legal, then* ϕ *is an isomorphism, i.e.,* L(Y [sY , sY ]) *contains only* Y *itself (and objects isomorphic to* Y *).*

# **5 Abstract Rewriting of Annotated Objects**

We will now show how to actually rewrite annotated objects. The challenge is both to find suitable annotations for the materialization and to "rewrite" the annotations.

#### **5.1 Abstract Rewriting and Soundness**

We first describe how the annotated rewritable materialization is constructed and then we investigate its properties.

**Definition 31 (Construction of annotated rewritable materialization).** *Let* p: L ϕL I ϕR R *be a production and let* A[a1, a2] *be a doubly annotated object. Furthermore let* ϕ: L → A *be an arrow.*

*We first construct the factorization* L nL ϕ, ϕL ψ → A*, obtaining the rewritable materialization* ϕ, ϕL *from Definition 13. Next, let* M *contain all maximal*4 *elements of the set*

$$\mathcal{A}\left\{(a\_1',a\_2')\in\mathcal{A}(\langle\langle\varphi,\varphi\_L\rangle\rangle)^2\mid\mathcal{A}\_{n\_L}(s\_L)\le a\_2',a\_1\le\mathcal{A}\_{\psi}(a\_1'),\mathcal{A}\_{\psi}(a\_2')\le a\_2\right\}.$$

*Then the doubly annotated objects* ϕ, ϕL [a 1, a 2] *with* (a 1, a 2) ∈ M *are the annotated rewritable materializations for* A[a1, a2]*,* ϕ *and* ϕL*.*

Note that in general there can be several such materializations, differing by the annotations only, or possibly none. The definition of M ensures that the upper bound a 2 of the materialization covers the annotations arising from the left-hand side. We cannot use a corresponding condition for the lower bound, since the materialization might contain additional structures, hence the arrow nL is only "semi-legal". A more symmetric condition will be studied in Sect. 5.2.