<figure><img src="image_104.png" /></figure>

Remark 2.2.15. Another possible way of defining the category of components w.r.t. the system of weak isomorphisms consists in using the localization [18, Definition 6.25] instead of the quotient. Both these definitions coincide on loop-free categories [18, Theorem 6.30], and none of these definitions give the expected results on categories with loops.

### 2.2.2 Computing the category of components of loop-free programs

The methods for computing the category of components given in [28] and [18] are both extremely costly, and it makes sense to try to reduce the size of the categories when we can. We have seen in Section 2.1 a method to factor programs in terms of independent processes (Definition 2.1.1), whose associated geometric semantics can then be factored, i.e. for two independent programs $P, Q$,

$$ \bar{\mathcal{G}}_{P\|Q} = \bar{\mathcal{G}}_P \times \bar{\mathcal{G}}_Q $$

Additionally, the functor computing the fundamental category and the one computing the category of components both preserve binary products.

**Proposition 2.2.16.** The fundamental category functor $\bar{\Pi}_1: \mathrm{dTop} \to \mathrm{Cat}$ preserves binary products i.e.

$$ \bar{\Pi}_1(X \times Y) = \bar{\Pi}_1(X) \times \bar{\Pi}_1(Y) $$

*Proof.* See [29, Proposition 5.2.12]. □

**Proposition 2.2.17.** The category of components functor $\bar{\Pi}_0: \mathrm{LFCat} \to \mathrm{LFCat}$ preserves binary products, i.e.

$$ \bar{\Pi}_0(\mathcal{C} \times \mathcal{D}) = \bar{\Pi}_0(\mathcal{C}) \times \bar{\Pi}_0(\mathcal{D}) $$

*Proof.* See [29, Proposition 8.5.11]. □

Thus, the fundamental category $\bar{\Pi}_1(\bar{\mathcal{G}}_{P\|Q})$ and category of components $\bar{\Pi}_0(\bar{\mathcal{G}}_{P\|Q})$ of a loop-free program $P\|Q$, where $P$ and $Q$ are independent, can be computed as the product of their category of components.

**Proposition 2.2.18.** Given two independent programs $P, Q$ i.e. such that $\bar{\mathcal{G}}_{P\|Q} = \bar{\mathcal{G}}_P \times \bar{\mathcal{G}}_Q$, we have:

$$ \bar{\Pi}_1(\bar{\mathcal{G}}_{P\|Q}) = \bar{\Pi}_1(\bar{\mathcal{G}}_P) \times \bar{\Pi}_1(\bar{\mathcal{G}}_Q) $$

$$ \bar{\Pi}_0(\bar{\mathcal{G}}_{P\|Q}) = \bar{\Pi}_0(\bar{\mathcal{G}}_P) \times \bar{\Pi}_0(\bar{\mathcal{G}}_Q) $$
Another approach to the factorization of programs would be to directly find factorizations of its model, and from there deducing a factorization of the program. The category of components, being finite, is a good candidate to try and find a product decomposition.

In the case of partial orders, the existence of a refinement for any pair of isomorphic product decomposition is a well-known result to which we refer as Hashimoto's theorem [26]. The category of (small) loop-free categories contains all the partially ordered sets, all the fundamental categories, and all the categories of component of the models of loop-free programs. These remarks motivate our successful attempt to extend Hashimoto's theorem to connected loop-free categories (Section 2.3). Theorem 2.3.36 even guarantees the existence of a maximal refinement for any finite loop-free category (in particular, for any category of component of a loop-free program).

## 2.3 Factoring loop-free categories

In this section we will introduce Hashimoto's Theorem (Theorem 2.3.3), which states that any pair of decompositions of a connected partial order have a common refinement. This is what we call the *strict refinement property* (Definition 2.3.2). We prove in Theorem 2.3.36 that this property extends to the more general case of loop-free categories. The structure of our proof diverges from Hashimoto's original paper [26] and instead follows more closely the presentation found in [49, Chapter 10].

We say that a poset is connected when any two pair of elements is connected by a "zigzag" of elements:

**Definition 2.3.1.** A poset is connected when for all elements $x$ and $y$ we have a sequence $x = z_0, z_1, \dots, z_n = y$ such that $z_i$ and $z_{i-1}$ are comparable for every $i \in \{1, \dots, n\}$.

**Definition 2.3.2.** A connected poset $X$ satisfies the *strict refinement property* if when the following isomorphism holds in the category **Pos** of posets:

$$X \cong \prod_{\alpha \in A} X_{\alpha} \cong \prod_{\beta \in B} Y_{\beta}$$

we have a family of posets $\{Z_{\alpha,\beta} | \alpha \in A; \beta \in B\}$ such that the isomorphisms

$$X_{\alpha} \cong \prod_{\beta \in B} Z_{\alpha, \beta} \quad \text{and} \quad Y_{\beta} \cong \prod_{\alpha \in A} Z_{\alpha, \beta}$$

hold for every $\alpha \in A$ and every $\beta \in B$.

**Theorem 2.3.3 (Hashimoto's Theorem, [26]).** Every connected poset has the strict refinement property.

A poset $X$ is said to be *irreducible* when $X \cong A \times B$ implies that either $A$ or $B$ has a single element (but not both!). One easily shows that every finite connected poset can be written as a finite product of *irreducible* posets in a unique way, up to reordering of factors. Indeed, for a finite poset, there exists a finite number of product decompositions, which are all isomorphic by definition. With the strict refinement property, we can then construct the refinement of all decomposition in a finite number of steps, which is still a product decomposition and cannot be refined any further.
*Example 2.3.4.* Let us consider the two following isomorphic decomposition of $\mathbb{R}^3$:

$$ \mathbb{R}^2 \times \mathbb{R} = X_1 \times X_2 $$

$$ \mathbb{R} \times \mathbb{R}^2 = Y_1 \times Y_2 $$

Then $\mathbb{R} \times \mathbb{R} \times \mathbb{R} = \mathbb{R} \times \mathbb{R} \times \{*\} \times \mathbb{R}$ is a refinement of these two decompositions by assigning:

$$ Z_{1,1} = \mathbb{R} $$

$$ Z_{1,2} = \mathbb{R} $$

$$ Z_{2,1} = \{*\} $$

$$ Z_{2,2} = \mathbb{R} $$

### 2.3.1 Properties of loop-free categories

Given an object $X$ of a category $\mathcal{C}$, we write $\mathrm{id}_X$ for the identity morphism on $X$. We generally omit the subscript when clear from the context. Given a morphism $f: X \to Y$, we write $\bar{f} = X$ (resp. $\underline{f} = Y$) for its *source* (resp. *target*).

The category of loop-free categories **LFCat** (Definition 2.2.5) is a full subcategory of the category of small categories **Cat**. **LFCat** contains the category **Pos** of partial orders as a full subcategory. The embedding **Pos** $\hookrightarrow$ **LFCat** has a left adjoint which to a category associates the poset obtained by identifying any two arrows with the same source and the same target.

**Lemma 2.3.5.** Given two morphisms $f, g$ of a loop-free category $\mathcal{C}$, we have that $f \circ g = \mathrm{id}$ implies $f = g = \mathrm{id}$

*Proof.* If $f \circ g = \mathrm{id}$, then both $f$ and $g$ have a return; it follows that both are identities because $\mathcal{C}$ is loop-free. □

**Definition 2.3.6.** Given a category $\mathcal{C}$ and any set of its objects $\{X_i\}_{i \in I}$, the product of $\{X_i\}_{i \in I}$ is, if it exists, an object denoted

$$ \prod_{i \in I} X_i \in \mathcal{C} $$

and equipped with morphisms

$$ \pi_j: \prod_{i \in I} X_i \to X_j $$

called *projections* for all $j \in I$, such that for any family of morphisms $\{f_i: Q \to X_i\}_{i \in I}$, there exists a unique morphism

$$ (f_i)_{i \in I}: Q \to \prod_{i \in I} X_i $$

such that all the following diagrams commute:

<figure><img src="image_105.png" /></figure>
**Proposition 2.3.7.** LFCat has all products.

*Proof.* LFCat is an epireflective subcategory of Cat ([28, Proposition 1.8]), a cartesian closed category. Thus, it has all products. □

**Definition 2.3.8.** In LFCat, consider a family $\{f_\alpha : X_\alpha \to Y_\alpha\}_{\alpha \in A}$ of morphisms. The product map $f : \coprod_{\alpha \in A} X_\alpha \to \coprod_{\alpha \in A} Y_\alpha$ is the unique morphism such that $\pi_\alpha f = f_\alpha$ for every $\alpha \in A$.

For the rest of the chapter we will often write $f = (f_\alpha)_{\alpha \in A}$ for the product map of the family $\{f_\alpha : X_\alpha \to Y_\alpha\}_{\alpha \in A}$. For binary products, we write $(f, g)$ the product map of $f$ and $g$.

**Proposition 2.3.9.** Given a category $\mathcal{C}$ with all products, and two morphisms $f_1 : X_1 \to Y_1$ and $f_2 : X_2 \to Y_2$ of $\mathcal{C}$, the following diagram commutes:

<figure><img src="image_106.png" /></figure>

**Lemma 2.3.10.** Given an isomorphism of small, loop-free categories $\Phi: \mathcal{C}_1 \times \mathcal{C}_2 \to \mathcal{D}_1 \times \mathcal{D}_2$ and an object $X$ of $\mathcal{C}_1$, for all morphisms $(f, g)$ of $\mathcal{D}_1 \times \mathcal{D}_2$ such that $\pi_1 \Phi^{-1}(f, g) = \text{id}_{\mathcal{D}_1}$, we have:

$$ \pi_1 \Phi^{-1}(f, \text{id}_{\mathcal{D}_1}) = \pi_1 \Phi^{-1}(f, \text{id}_{\mathcal{D}_2}) = \pi_1 \Phi^{-1}(\text{id}_{\mathcal{D}_1}, g) = \pi_1 \Phi^{-1}(\text{id}_{\mathcal{D}_2}, g) = \text{id}_{\mathcal{D}_1}. $$

*Proof.* By definition of the product, the following diagram on the left commutes:

<figure><img src="image_107.png" /></figure>

The category $\mathcal{P}$ is loop-free, thus by applying Lemma 2.3.5 we have

$$ \pi_1 \Phi^{-1}(\text{id}_{\mathcal{D}_1}, g) = \pi_1 \Phi^{-1}(f, \text{id}_{\mathcal{D}_1}) = \text{id}. $$

We prove in the same way that $\pi_1 \Phi^{-1}(\text{id}_{\mathcal{D}_1}, g) = \pi_1 \Phi^{-1}(f, \text{id}_{\mathcal{D}_1}) = \text{id}$. □

**Definition 2.3.11.** A fence is a family $(f_i)_{1 \le i \le n}$ of morphisms of $\mathcal{C}$ such that:

* $\underline{f_{2i}} = \underline{f_{2i+1}}$ and $\overline{f_{2i-1}} = \overline{f_{2i}}$

* or $\overline{f_{2i}} = \overline{f_{2i+1}}$ and $\underline{f_{2i-1}} = \underline{f_{2i}}$
The length of a fence $(f_i)_{1 \le i \le n}$ is its cardinal $n$

**Definition 2.3.12.** Two morphisms $f$ and $g$ of a category $\mathcal{C}$ are said to be connected if there exists a fence $(f_i)_{i \in [1, n]}$ such that $f = f_1$ and $f_n = g$. A category $\mathcal{C}$ is said to be connected if all its morphisms are connected.

**Proposition 2.3.13.** The set of objects $\text{Obj}(\mathcal{C})$ of a (small) loop-free category $\mathcal{C}$ is equipped with a partial order $\leq$ defined by

$$X \leq Y \iff \mathcal{C}(X, Y) \neq \emptyset.$$

*Proof.* Let $X, Y, Z$ in $\text{Obj}(\mathcal{C})$.

* Reflexivity: $\text{id}_X \in \mathcal{C}(X, X)$, thus $X \leq X$.

* Transitivity: $X \leq Y$ and $Y \leq Z$ implies the existence of $f \in \mathcal{C}(X, Y)$ and $g \in \mathcal{C}(Y, Z)$. Thus, $f \circ g \in \mathcal{C}(X, Z)$ i.e. $X \leq Z$.

* Anti-symmetry: Directly by the loop-freeness property.

□

**Proposition 2.3.14.** For $\mathcal{C}$ in $\text{LFCat}$, $\mathcal{C}$ is connected implies $\text{Obj}(\mathcal{C})$ is connected as a poset.

*Proof.* Let $X, Y \in \text{Obj}(\mathcal{C})$. By definition, $\text{id}_X, \text{id}_Y \in \mathcal{C}$, connected category. Such that there exists a fence $(f_i)_{i \in I}$ between $\text{id}_X, \text{id}_Y$. Then $\bar{f}_i = \bar{f}_i + 1$ implies $\bar{f}_i \leq \bar{f}_i \geq \bar{f}_{i+1}$ by definition of the order. Thus, if we fix $(X_i)_{1 \leq i \leq 2n}$ with $X_{2k} = \bar{f}_k$ and $X_{2k+1} = \bar{f}_{k+1}$, we have a sequence $X_1 \geq X_2 \leq \dots \geq X_{2n-1} \leq X_{2n}$ connecting $X, Y \in \text{Obj}(\mathcal{C})$. □

**Proposition 2.3.15.** Let $\Phi: \mathcal{C} \to \mathcal{D}$ be a morphism of connected loop-free categories. Let $\leq$ be the canonical order defined in Proposition 2.3.13. Then

$$\Phi|_{\text{Obj}}: (\text{Obj}(\mathcal{C}), \leq) \to (\text{Obj}(\mathcal{D}), \leq)$$

is an order-preserving morphism of connected posets. Furthermore, if $\Phi$ is an isomorphism, so is $\Phi|_{\text{Obj}}$.

*Proof.* Let $X, Y$ in $\text{Obj}(\mathcal{C})$ such that $X \leq Y$. Thus, there exists $f \in \mathcal{C}(X, Y)$ and by functoriality of $\Phi$, $\Phi(f) \in \mathcal{D}(\Phi(X), \Phi(Y))$ i.e. $\Phi(X) \leq \Phi(Y)$. □

*Remark 2.3.16.* The property above comes from the adjunction between $\text{LFCat}$ and $\text{Pos}$ talked about at the beginning of the section.

### 2.3.2 Hashimoto's theorem for loop-free categories

**Definition 2.3.17.** A (product) decomposition of a loop-free category $\mathcal{C}$ is an isomorphism $\Psi$ from $\mathcal{C}$ to a product $\prod_{\alpha \in A} X_\alpha$ of loop-free categories $X_\alpha$ for $\alpha \in A$.

Note that if $\mathcal{C}$ is non-empty, connected, and loop-free, then so are the categories $X_\alpha$.
**Definition 2.3.18.** A category $\mathcal{C}$ is said to have the *strict refinement property* if for any two decompositions $\Psi_A : \mathcal{C} \to \prod_{\alpha \in A} X_\alpha$ and $\Psi_B : \mathcal{C} \to \prod_{\beta \in B} Y_\beta$, there exists a family of loop-free categories $Z_{\alpha,\beta}$ with $\alpha \in A$ and $\beta \in B$, and for every $\alpha \in A$ and $\beta \in B$, decompositions

$$a_{\alpha} : X_{\alpha} \to \prod_{\beta \in B} Z_{\alpha, \beta} \quad \text{and} \quad b_{\beta} : Y_{\beta} \to \prod_{\alpha \in A} Z_{\alpha, \beta}$$

such that the following diagram commutes:

<figure><img src="image_108.png" /></figure>

where $\gamma : \prod_{\alpha \in A} \prod_{\beta \in B} Z_{\alpha, \beta} \to \prod_{\beta \in B} \prod_{\alpha \in A} Z_{\alpha, \beta}$ is the natural isomorphism sending $((z_{\alpha,\beta})_{\beta \in B})_{\alpha \in A}$ to $((z_{\alpha,\beta})_{\alpha \in A})_{\beta \in B}$.

Hashimoto's Theorem [26] states that every connected poset has the strict refinement property; we generalize this result to all connected loop-free categories:

**Theorem 2.3.36.** Every connected loop-free category has the strict refinement property.

As previously stated, we will follow the proof from [49], generalizing the key lemmas to the case of connected loop-free categories. We will first give a rough idea of the different steps of the proofs, before introducing some key technical lemmas, that will be used along the proof, before proving all the major steps.

### 2.3.2.1 Sketch of the proof

To prove Theorem 2.3.36 we will need to find the decompositions $(a_\alpha)_{\alpha \in A}$ and $(b_\beta)_{\beta \in B}$ of Eq. (2.1). For this we will first define some notions, that will be used in the presentation of the proof.

**Definition 2.3.19.** Given an element $s$ of a set product $\prod_{i \in I} S_i$, an index $j \in I$, and an element $x_j \in S_j$, we define $(s, x_j, j)_{i \in I}$ as the element of $\prod_{i \in I} S_i$ obtained by substituting $x_j$ to $s_j$ in $s$; in other words:

$$(s, x_j, j)_i = \begin{cases} x_j & \text{if } i = j \\ s_i & \text{otherwise.} \end{cases}$$
**Lemma 2.3.24.** Let $\Phi: \mathcal{P} \times \mathcal{Q} \to \mathcal{U} \times \mathcal{V}$ an isomorphism of connected loop-free categories. Let $(u, v)$ and $(u', v')$ two morphisms of $\mathcal{U} \times \mathcal{V}$ and $p$ a morphism of $\mathcal{P}$. Then $\pi_{\mathcal{P}}\Phi^{-1}(u, v) = \pi_{\mathcal{P}}\Phi^{-1}(u', v') = p$ implies $\pi_{\mathcal{P}}\Phi^{-1}(u, v') = p$.

Then, once this has been achieved, we need to prove that the diagram commutes to conclude the proof. To do this, we will first prove the commutation on a restriction of the diagram, by replacing for each $\alpha \in A$ the starting category $X_\alpha$ by the subcategory $X_\alpha^\mu$ as in Definition 2.3.21, for an arbitrary $\mu \in \beta$, giving us the diagram below.

$$ \begin{tikzcd}[column sep=2.8em, row sep=2.8em]
    \Pi_{\alpha \in A} X_{\alpha}^{\mu} \arrow[r, "\Phi"] & Y_{\mu}^{\phi(s)} \\
    \Pi_{\alpha \in A} \Pi_{\beta \in B} X_{\alpha}^{\beta} \arrow[r, "\gamma^{-1}", "\Phi"] & \Pi_{\beta \in B} \Pi_{\alpha \in A} X_{\alpha}^{\beta}
    \arrow[u, "\Psi_2"'] \arrow[u, "\Psi_1"'] &
    \end{tikzcd} \quad (2.3) $$

Then using the following Lemma 2.3.26, the commutation is extended along a given $\lambda \in A$.

**Lemma 2.3.26.** Let $\Phi: \mathcal{P} \times \mathcal{Q} \to \mathcal{U} \times \mathcal{V}$ be an isomorphism of connected loop-free categories. Let $\mathcal{Q}'$ a connected subcategory of $\mathcal{Q}$. Let $p$ a morphism of $\mathcal{P}$. Then $\pi_U \Phi(p, q) = \pi_U \Phi(p, q')$ for all $q, q' \in \mathcal{Q}'$ implies, for all $p' \in \mathcal{P}$, $\pi_U \Phi(p', q) = \pi_U \Phi(p', q')$ for all $q, q' \in \mathcal{Q}'$.

This leads to the commutation of the Diagram 2.4 below.

$$ \begin{tikzcd}[column sep=2.8em, row sep=2.8em]
    \Pi_{\alpha \in A \setminus \lambda} X_{\alpha}^{\mu} \times X_{\lambda} \arrow[r, "\Phi"] & \Pi_{\beta \in B} Y_{\beta} \\
    (\pi_{\alpha} \Psi_2)_{\alpha \neq \lambda} \times \pi_{\lambda} \Psi_2 \arrow[u, "\Psi_1"'] &
    \Pi_{\alpha \in A} \Pi_{\beta \in B} X_{\alpha}^{\beta} \arrow[r, "\gamma^{-1}", "\Phi"] & \Pi_{\beta \in B} \Pi_{\alpha \in A} X_{\alpha}^{\beta}
    \arrow[u, "\Psi_2"'] \arrow[u, "\Psi_1"'] &
    \end{tikzcd} \quad (2.4) $$

Using Lemma 2.3.26 once more the commutativity can be extended to the full domain $\Pi_{\alpha \in A} X_\alpha$, thus ending the proof.

In our case a few necessary conditions that are less trivial will need to be detailed in Lemma 2.3.34 to perform the last steps of the proof, but the broad strokes will remain the same.

### 2.3.2.2 Technical Lemmas

The proof of Theorem 2.3.3 in [49] makes extensive use of the Proposition 2.3.22 and Proposition 2.3.23, which we will respectively extend to connected elements of LFCat in Lemma 2.3.24 and Lemma 2.3.26. As we have changed the formulation to make the proofs easier to follow, we give them here and refer to the original work for the proof.
These lemmas are at the core of the proof and are where the hypothesis that we are using loop-free and connected categories really comes into play, so it is important to keep them in mind.

**Proposition 2.3.22.** Given $\Phi: P \times Q \to U \times V$ an isomorphism of connected posets and $p \in P$,

$$ \pi_P \Phi^{-1}(u, v) = \pi_P \Phi^{-1}(u', v') = p \text{ implies } \pi_P \Phi^{-1}(u, v') = p $$

*Proof.* [49, Lemma 10.4.5]. □

**Proposition 2.3.23.** Given $\Phi: P \times Q \to U \times V$ an isomorphism of connected posets, if there exists $p \in P$ such that $\pi_U \Phi(p, q) = \pi_U \Phi(p, q')$, then for each $p' \in P$,

$$ \pi_U \Phi(p', q) = \pi_U \Phi(p', q') $$

*Proof.* [49, Lemma 10.4.8] □

In the two following proofs, as the objects in the commutative diagrams are of no importance, we have omitted them, replacing them by ● when not necessary.

**Lemma 2.3.24.** Let $\Phi: \mathcal{P} \times Q \to \mathcal{U} \times \mathcal{V}$ an isomorphism of connected loop-free categories. Let $(u, v)$ and $(u', v')$ two morphisms of $\mathcal{U} \times \mathcal{V}$ and $p$ a morphism of $\mathcal{P}$. Then $\pi_P \Phi^{-1}(u, v) = \pi_P \Phi^{-1}(u', v') = p$ implies $\pi_P \Phi^{-1}(u, v') = p$.

*Proof.* Given $p, q, q'$ such that $\Phi(p, q) = (u, v)$ and $\Phi(p, q') = (u', v')$. Let us prove that $\pi_P \Phi^{-1}(u, v') = p$. We proceed by induction on the length of the fence between $q$ and $q'$.

* A fence of length 2 implies $q = \underline{q}'$ or $\bar{q} = \bar{q}'$. First, let us suppose $q = \underline{q}'$, the other case being solved dually.

Let us prove that $\pi_P \Phi^{-1}(u, v') = p$.

First, let us define

$$ \Phi(p, \mathrm{id}_q) := (u^*, v^*) \qquad \Phi(\mathrm{id}_{\bar{p}}, q) := (u_q, v_q) \qquad \Phi(\mathrm{id}_{\bar{p}}, q') := (u'_q, v'_q) \quad (2.5) $$

such that:

$$ u = u_q \circ u^* $$

$$ u' = u'_q \circ u^* $$

$$ v = v_q \circ v^* $$

$$ v' = v'_q \circ v^* $$

By the Proposition 2.3.9, the following diagram commutes:

<figure><img src="image_109.png" /></figure>
Following the outer arrows, we get

$$ (u, v') = (u_q, v'_q) \circ (u^*, v^*) $$

By Eq. (2.5), $\pi_P \Phi^{-1}(u^*, v^*) = p$. We are thus left to prove $\pi_P \Phi^{-1}(u_q, v'_q) = \text{id}$. By construction $\underline{v_q} = \underline{v'_q} = \bar{v}^*$ such that by functoriality:

$$ \begin{aligned} \frac{\pi_P \Phi^{-1}(u_q, v'_q)}{\underline{\underline{\pi_P \Phi^{-1}(u_q, v'_q)}}} &= \pi_P \Phi^{-1}(\underline{u_q}, \underline{v'_q}) \\ &= \pi_P \Phi^{-1}(\underline{u_q}, \underline{v_q}) \\ &= \frac{\pi_P \Phi^{-1}(u_q, v_q)}{\underline{\underline{\pi_P \Phi^{-1}(u_q, v'_q)}}} \\ \underline{\underline{\underline{\pi_P \Phi^{-1}(u_q, v'_q)}}} &= \bar{p} \end{aligned} $$

By Proposition 2.3.15, $\Phi: \text{Obj}(\mathcal{P}) \times \text{Obj}(\mathcal{Q}) \to \text{Obj}(\mathcal{U}) \times \text{Obj}(\mathcal{V})$ is an order-preserving isomorphism of connected posets and such that $\pi_P \Phi^{-1}(\bar{u}_q, \bar{v}_q) = \pi_P \Phi^{-1}(\bar{u}'_q, \bar{v}'_q) = \bar{p}$. Hence,

$$ \begin{aligned} \bar{p} &= \pi_P \Phi^{-1}(\bar{u}_q, \bar{v}'_q) & \text{Proposition 2.3.22} \\ \bar{p} &= \frac{\pi_P \Phi^{-1}(u_q, v'_q)}{\underline{\underline{\pi_P \Phi^{-1}(u_q, v'_q)}}} & \text{by functoriality} \end{aligned} $$

Thus, $\pi_P \Phi^{-1}(u_q, v'_q) \in \mathcal{P}(\bar{p}, \bar{p})$, with $\mathcal{P}$ loop-free. This implies $\pi_P \Phi^{-1}(u_q, v'_q) = \text{id}_{\bar{p}}$, such that

$$ \begin{aligned} \pi_P \Phi^{-1}(u, v') &= \pi_P \Phi^{-1}(u_q, v'_q) \circ \pi_P \Phi^{-1}(u^*, v^*) \\ \pi_P \Phi^{-1}(u, v') &= p \end{aligned} $$

* Now let us suppose a fence $\cdot \xrightarrow{q'} \cdot \xleftarrow{r} \cdot \xrightarrow{q} \cdot$ of length $n=3$ between $q$ and $q'$. Let

$$ (u, v) := \Phi(p, q) \qquad (x, y) := \Phi(p, r) \qquad (u', v') := \Phi(p, q') \qquad (2.6) $$

such that $\Phi$ sends the commutative diagram on top to the one below.

<figure><img src="image_110.png" /></figure>
<figure><img src="image_111.png" /></figure>

We are going to use the same method as before, working on each 2-fence inside the 3-fence above. For that we'll decompose $(u, v')$ using the Diagram 2.7. By the Proposition 2.3.9, the following diagram commutes:

<figure><img src="image_112.png" /></figure>

such that

$$ (u, v') = (u_q, \mathrm{id}_{\bar{v}'}) \circ (u^*, y^*) \circ (\mathrm{id}_{u^*}, v'_q) \quad \text{By following the outer arrows} $$

$$ (u, v') = (u_q, \mathrm{id}_{\bar{v}_r}) \circ (u^*, y^*) \circ (\mathrm{id}_{\bar{u}_r}, v'_q) \quad \text{By the Diagram 2.7} $$

- Working on the 2-fence $\stackrel{q}{\leftarrow} \cdot \stackrel{r}{\rightarrow}$, let us prove $\pi_P \Phi^{-1}(u_q, \mathrm{id}_{\bar{v}_r}) = \mathrm{id}$

By Eq. (2.6) we have $\pi_P \Phi^{-1}(u, v) = \pi_P \Phi^{-1}(x, y) = p$. Thus, as proved for 2-fences above

$$ \begin{align*} p &= \pi_P \Phi^{-1}(u, y) \\ &= \pi_P \Phi^{-1}((u_q, v_r) \circ (u^*, v^*)) \quad \text{Diagram 2.7} \end{align*} $$

$$ = \pi_P \Phi^{-1}(u_q, v_r) \circ \pi_P \Phi^{-1}(u^*, v^*) \quad \text{Functoriality} $$

$$ p = \pi_P \Phi^{-1}(u_q, v_r) \circ p \quad \text{Diagram 2.7} $$

By loop-free property of $\mathcal{P}$, $\pi_P \Phi^{-1}(u_q, v_r) = \mathrm{id}_{\bar{p}}$. Which implies by Lemma 2.3.10,

$$ \pi_P \Phi^{-1}(u_q, \mathrm{id}_{\bar{v}_r}) = \mathrm{id}_{\bar{p}} $$

Similarly, $\pi_P \Phi^{-1}(\mathrm{id}_{\bar{u}_r}, v'_q) = \mathrm{id}_{\bar{p}}$. Hence

$$ \begin{align*} \pi_P \Phi^{-1}(u, v') &= \pi_P \Phi^{-1}(u_q, \mathrm{id}_{\bar{v}_r}) \circ \pi_P \Phi^{-1}(u^*, y^*) \circ \pi_P \Phi^{-1}(\mathrm{id}_{\bar{u}_r}, v'_q) \\ &= \mathrm{id}_{\bar{p}} \circ \pi_P \Phi^{-1}(u^*, y^*) \circ \mathrm{id}_{\bar{p}} \end{align*} $$

$$ \pi_P \Phi^{-1}(u, v') = \pi_P \Phi^{-1}(u^*, y^*) $$
- Let us prove now $\pi_P \Phi^{-1}(u^*, y^*) = p$. By commutativity of both projections the central square:

$$ 
\begin{align*}
(x, y) &= (u_r \circ u^*, y^* \circ v'_r) \\
&= (u_r, \mathrm{id}_{\overline{u^*}}) \circ (u^*, y^*) \circ (\mathrm{id}_{\overline{u^*}}, v'_r) \\
(x, y) &= (u_r, \mathrm{id}_{\overline{v_r}}) \circ (u^*, y^*) \circ (\mathrm{id}_{\overline{u'_r}}, v'_r)
\end{align*}
$$

As $\pi_P \Phi^{-1}(u_r, v_r) = \mathrm{id}_{\overline{p}}$, by Lemma 2.3.10, $\pi_P \Phi^{-1}(u_r, \mathrm{id}_{\overline{v_r}}) = \mathrm{id}_{\overline{p}}$. Similarly, we have $\pi_P \Phi^{-1}(\mathrm{id}_{\overline{u'_r}}, v'_r) = \mathrm{id}_{\overline{p}}$. Thus

$$ p = \pi_P \Phi^{-1}(x, y) = \pi_P \Phi^{-1}(u^*, y^*) $$

Such that

$$ \pi_P \Phi^{-1}(u, v') = p $$

- Now let us suppose that the property holds for all fences of length $1 \le k < n$, with $n > 3$. Let us suppose given $q, q'$, connected by a fence $(q_i)_{1 \le i \le n}$. We define $(u_i, v_i) := \Phi(p, q_i)$, for each $1 \le i \le n$ and

$$ 
\begin{align*}
(u, v) &:= (u_1, v_1) = \Phi(p, q_1) = \Phi(p, q) \\
(u', v') &:= (u_n, v_n) = \Phi(p, q_n) = \Phi(p, q')
\end{align*}
$$

By definition, $((p, q_i))_{1 \le i \le n-1}$ and $((p, q_i))_{2 \le i \le n}$ are fences of length $n-1$ respectively connecting $(p, q_1)$, $(p, q_{n-1})$ and $(p, q_2)$, $(p, q_n)$. By definition of $(u_i, v_i)$ we have,

$$ 
\begin{align*}
p &= \pi_P \Phi^{-1}(u_1, v_1) = \pi_P \Phi^{-1}(u_{n-1}, v_{n-1}) \\
p &= \pi_P \Phi^{-1}(u_2, v_2) = \pi_P \Phi^{-1}(u_n, v_n)
\end{align*}
$$

Thus, by induction hypothesis, this implies

$$ p = \pi_P \Phi^{-1}(u_1, v_{n-1}) \qquad p = \pi_P \Phi^{-1}(u_2, v_n) \qquad (2.8) $$

Now we suppose $\overline{q_1} = \overline{q_2}$ ($\overline{q_1} = \overline{q_2}$ can be treated dually). We'll have to proceed differently depending on the symmetry of the fence.

- If $\overline{q_{n-1}} = \overline{q_n}$, by functoriality of $\Phi$, $\overline{u_{n-1}}, \overline{v_{n-1}} = \overline{u_n}, \overline{v_n}$, such that $\overline{u_2}, \overline{v_n} = \overline{u_1}, \overline{v_{n-1}}$. This implies that $(u_1, v_{n-1})$ and $(u_2, v_n)$ are connected by a fence of length 2. Thus, $\pi_Q \Phi^{-1}(u_1, v_{n-1})$ and $\pi_Q \Phi^{-1}(u_2, v_n)$ are connected by a fence of length 2. By Eq. (2.8), we have $p = \pi_P \Phi^{-1}(u_2, v_n) = \pi_P \Phi^{-1}(u_1, v_{n-1})$. We can then apply our induction hypothesis, such that

$$ 
\begin{align*}
p &= \pi_P \Phi^{-1}(u_1, v_n) \\
p &= \pi_P \Phi^{-1}(u, v')
\end{align*}
$$

Which concludes this case.
- If $q_{n-1} = q_n$, by functoriality of $\Phi$, $u_{n-1}, v_{n-1} = u_n, v_n$. Thus, if we define $q_{2,n} = \pi_Q \Phi^{-1}(u_2, v_n)$ and $q_{1,n-1} = \pi_Q \Phi^{-1}(u_1, v_{n-1})$, we get the following fences:

<figure><img src="image_113.png" /></figure>

Thus, $q_{2,n}$ et $q_{1,n-1}$ are connected by a fence of length 3. We can apply our induction case for $k=3$ with the fence $(p, q_{1,n-1}), (p, \pi_Q \Phi^{-1}(u_1, v_n)), (p, q_{2,n})$. Indeed, we have $\Phi(p, q_{1,n-1}) = (u_1, v_{n-1})$ and $\Phi(p, q_{2,n}) = (u_2, v_n)$ (Eq. (2.8)). Thus, we get

$$ \pi_P \Phi^{-1}(u_1, v_n) = p $$

Thus, $\pi_P \Phi^{-1}(u, v) = \pi_P \Phi^{-1}(u', v') = p$ implies $\pi_P \Phi^{-1}(u, v') = p$, proving the induction step.

<figure><img src="image_114.png" /></figure>

This Lemma 2.3.24 is not restricted to binary product and easily extends to arbitrary products as shown in the following lemma.

**Corollary 2.3.25.** Let $\Phi: \coprod_{\alpha \in A} X_\alpha \to \coprod_{\beta \in B} Y_\beta$ an isomorphism of connected categories. Let $f^i = (f_\alpha^i)_{\alpha \in A}$ a morphism of $\coprod_{\alpha \in A} X_\alpha$ for $i=1,2$. Then for all $\lambda \in A$ and all $\mu \in B$ such that $\pi_\lambda f^1 = \pi_\lambda f^2$

$$ \pi_\lambda \Phi^{-1}(\Phi(f^1), \Phi(f^2)_{\mu}, \mu) = \pi_\lambda f^1 = \pi_\lambda f^2 $$

*Proof.* This follows directly from Lemma 2.3.24 by defining:

$$ P := X_\lambda \qquad Q := \coprod_{\alpha \in A, \alpha \neq \lambda} X_\alpha \qquad U := Y_\beta \qquad V := \coprod_{\beta \in B, \mu \neq \beta} Y_\beta $$

and by defining

$$ \begin{align*} (p, q) &:= \delta_\lambda^{-1}(f^1) & (p, q') &:= \delta_\lambda^{-1}(f^2) \\ (u, v) &:= \delta_\mu^{-1}\Phi(f^1) & (u', v') &:= \delta_\mu^{-1}\Phi(f^2) \end{align*} $$

With $\delta_\lambda$ and $\delta_\mu$ the natural isomorphisms:

$$ \delta_\lambda: X_\lambda \times \coprod_{\alpha \in A, \alpha \neq \lambda} X_\alpha \to \coprod_{\alpha \in A} X_\alpha \qquad \delta_\mu: Y_\mu \times \coprod_{\beta \in B, \mu \neq \beta} Y_\beta \to \coprod_{\beta \in B} Y_\beta $$

We get an isomorphisms $\Psi = \delta_\beta^{-1} \circ \Phi \circ \delta_\lambda: P \times Q \to U \times V$. Such that $f_\lambda^i = \pi_P \Psi^{-1}(u, v')$ for $i=1,2$. □

**Lemma 2.3.26.** Let $\Phi: \mathcal{P} \times \mathcal{Q} \to \mathcal{U} \times \mathcal{V}$ be an isomorphism of connected loop-free categories. Let $\mathcal{Q}'$ a connected subcategory of $\mathcal{Q}$. Let $p$ a morphism of $\mathcal{P}$. Then $\pi_U \Phi(p, q) = \pi_U \Phi(p, q')$ for all $q, q' \in \mathcal{Q}'$ implies, for all $p' \in \mathcal{P}$, $\pi_U \Phi(p', q) = \pi_U \Phi(p', q')$ for all $q, q' \in \mathcal{Q}'$.
*Proof.* Let $p$ a morphism of $\mathcal{P}$ Let $\mathcal{Q}'$ a connected sub-category of $\mathcal{Q}$, such that for all morphisms $q, q'$ in $\mathcal{Q}'$, $\pi_U\Phi(p, q) = \pi_U\Phi(p, q')$. Let us prove that for all $p'$ morphism of $\mathcal{P}$, $\pi_U\Phi(p', q') = \pi_U\Phi(p', q)$ by induction on the length $n$ of a given fence connecting $q, q'$.

* $n = 1$. Trivial.

* $n = 2$. $\pi_U\Phi(p, q) = \pi_U\Phi(p, q')$ for all morphisms $q, q'$ in $\mathcal{Q}'$ implies

$$ \underline{\pi_U\Phi(p, q)} = \underline{\pi_U\Phi(p, q')} $$

$$ \pi_U\Phi(\underline{p}, \underline{q}) = \pi_U\Phi(\underline{p}, \underline{q}') \quad \text{for all } q, q' \in \operatorname{Mor}(\mathcal{Q}) $$

$$ \pi_U\Phi(\underline{p}, \underline{Q}) = \pi_U\Phi(\underline{p}, \underline{Q}') \quad \text{for all } \underline{Q}, \underline{Q}' \in \operatorname{Obj}(\mathcal{Q}) $$

By Proposition 2.3.15 $\Phi|_{\operatorname{Obj}(\mathcal{Q})}$ is an isomorphism between $\operatorname{Obj}(\mathcal{P}) \times \operatorname{Obj}(\mathcal{Q})$ and $\operatorname{Obj}(\mathcal{U}) \times \operatorname{Obj}(\mathcal{V})$. By Proposition 2.3.23

$$ \text{for all } \underline{Q}, \underline{Q}' \in \operatorname{Obj}(\underline{\mathcal{Q}}), \pi_U\Phi(\underline{p}', \underline{Q}) = \pi_U\Phi(\underline{p}', \underline{Q}') \quad (2.9) $$

Thus for $\underline{q} \in \operatorname{Mor}(\mathcal{Q}')$ we have

$$ \begin{align*} \underline{\pi_U\Phi(\mathrm{id}_{\underline{p}'}, \underline{q})} &= \underline{\pi_U\Phi(\underline{p}', \underline{q})} \\ &= \underline{\pi_U\Phi(\underline{p}', \bar{\underline{q}})} \quad \text{By Eq. (2.9)} \\ &= \underline{\pi_U\Phi(\mathrm{id}_{\underline{p}'}, \bar{\underline{q}})} \end{align*} $$

$$ \underline{\pi_U\Phi(\mathrm{id}_{\underline{p}'}, \underline{q})} = \underline{\pi_U\Phi(\mathrm{id}_{\underline{p}'}, \underline{q})} $$

As $\mathcal{Q}'$ is loop-free, this implies $\pi_U\Phi(\mathrm{id}_{\underline{p}'}, \underline{q}) = \mathrm{id}$. Similarly, $\pi_U\Phi(\mathrm{id}_{\underline{p}'}, \underline{q}') = \mathrm{id}$.

Let us suppose that $\bar{\underline{q}} = \underline{q}'$, the other case being dual. By the above argument, the following diagrams commute

<figure><img src="image_115.png" /></figure>

Therefore, $\pi_U\Phi(\underline{p}', \underline{q}') = \pi_U\Phi(\underline{p}', \mathrm{id}_{\bar{\underline{q}}}) = \pi_U\Phi(\underline{p}', \underline{q})$.

* Now suppose a fence $(\underline{q} = q_0, q_1, \dots, q_n = \underline{q}')$ and the property true for all integers strictly smaller than $n$. Then there is a $n-1$-fence $(q_1, \dots, q_n)$ and a 1-fence $(q_0, q_1)$. By induction hypothesis, $\pi_U\Phi(\underline{p}', q_n) = \pi_U\Phi(\underline{p}', q_1) = \pi_U\Phi(\underline{p}', q_0)$.

$\mathcal{Q}'$ is connected so for all $\underline{p}' \in \mathcal{P}$, for all $\underline{q}, \underline{q}' \in \mathcal{Q}'$, $\pi_U\Phi(\underline{p}', \underline{q}') = \pi_U\Phi(\underline{p}', \underline{q})$. $\square$
### 2.3.2.3 Proof of Theorem 2.3.36

For the remainder of section, we will consider that $\Phi$ is an isomorphism of connected loop-free categories, $(X_\alpha)_{\alpha \in A}$ and $(Y_\beta)_{\beta \in B}$ families of connected loop-free categories.

As stated before, we will first prove that all the morphisms of the Diagram 2.2 are isomorphisms.

**Lemma 2.3.27.** Given a category $X = \coprod_{\alpha \in A} X_\alpha$, $\lambda \in A$, $s$ a morphism of $X$ and $\Xi_\lambda^s$ as defined in Definition 2.3.20, then

$$ \pi_\lambda \circ \Xi_\lambda^s = \mathrm{id}_{X_\lambda} $$

We say that $\Xi_\lambda^s$ is a section of the canonical projection $\pi_\lambda: \coprod_{\alpha \in A} X_\alpha \to X_\lambda$. Furthermore, $\Xi_\lambda^s$ is a full and faithful functor

*Proof.* Let $f \in \coprod_{\alpha \in A} X_\alpha((s, x_\lambda, \lambda), (s, y_\lambda, \lambda))$. Then $X_\alpha$ loop-free implies, $\pi_\alpha f = \mathrm{id}_{s_\alpha}$ if $\alpha \neq \lambda$ and $\pi_\lambda f := f_\lambda \in X_\lambda(x_\lambda, y_\lambda)$. Such that $f = \Xi_\lambda^s(f_\lambda)$. This proves that $\Xi_\lambda^s$ is full. Furthermore, it is clearly faithful. $\square$

**Corollary 2.3.28.** Given a category $X = \coprod_{\alpha \in A} X_\alpha$, $\lambda \in A$, $s$ a morphism of $X$ then $X_\lambda^s = \Xi_\lambda^s(X)$ is a connected, loop-free full sub-category of $X$ isomorphic to $X_\lambda$. Furthermore

$$ \pi_\lambda \circ \Xi_\lambda^s = \mathrm{id}_{X_\lambda} \quad \Xi_\lambda^s \circ \pi_\lambda|_{X_\lambda^s} = \mathrm{id}_{X_\lambda^s} $$

One last proposition that we will need from [49] is the fact that for any $\lambda \in A$, $s_\lambda$ object of $X_\lambda$, the object part of the functor $\Phi|_{X_\lambda^s}: X_\lambda^s \to \coprod_{\beta \in B} Y_\beta^\lambda$ is an isomorphism of the underlying objects of the category.

**Proposition 2.3.29.** [49, Lemma 10.4.7]

Let $\Phi: \coprod_{\alpha \in A} X_\alpha \to \coprod_{\beta \in B} Y_\beta$ be an isomorphism of connected posets. Let $s \in \coprod_{\alpha \in A} X_\alpha$ and $\lambda \in A$ and $X_\lambda^s$ be as in Lemma 2.3.27. Let $Y_\beta^\lambda = \pi_\beta \Phi[X_\lambda^s]$, then

$$ \Phi|_{X_\lambda^s}: X_\lambda^s \to \coprod_{\beta \in B} Y_\beta^\lambda $$

is an isomorphism of posets.

This proposition also translates to an isomorphism of connected categories.

**Proposition 2.3.30.** Let $\Phi: \coprod_{\alpha \in A} X_\alpha \to \coprod_{\beta \in B} Y_\beta$ be an isomorphism of connected loop-free categories. Let $s \in \coprod_{\alpha \in A} X_\alpha$ and $\lambda \in A$ and $X_\lambda^s$ be as in Lemma 2.3.27. Let $Y_\beta^\lambda = \pi_\beta \Phi[X_\lambda^s]$, then

$$ \Phi|_{X_\lambda^s}: X_\lambda^s \to \coprod_{\beta \in B} Y_\beta^\lambda $$

is an isomorphism of connected loop-free categories.
**Proof.** Let us show that $\Phi|_{X_{\lambda}^s}: X_{\lambda}^s \to \prod_{\beta \in B} Y_{\beta}^{\lambda}$ is essentially surjective. By Proposition 2.3.15, $\Phi_{\text{Obj}}|_{X_{\lambda}^s}$ is an isomorphism of posets. Thus, by Proposition 2.3.29,

$$ \begin{aligned} \Phi_{\text{Obj}}[X_{\lambda}^s] &= \prod_{\beta \in B} \pi_{\beta} \Phi_{\text{Obj}}[\text{Obj}(X_{\lambda}^s)] \\ &= \prod_{\beta \in B} \text{Obj}(\pi_{\beta} \Phi[X_{\lambda}^s]) \\ \Phi_{\text{Obj}}[X_{\lambda}^s] &= \text{Obj}(\prod_{\beta \in B} \pi_{\beta} \Phi[X_{\lambda}^s]) \end{aligned} $$

Thus $\Phi|_{X_{\lambda}^s}$ is essentially surjective. Furthermore, $\Phi|_{X_{\lambda}^s}$ is full and faithful as the restriction of a full and faithful functor to a full subcategory (Lemma 2.3.27 and Corollary 2.3.28). Thus, $\Phi|_{X_{\lambda}^s}$ is a fully faithful and essentially surjective functor, thus an isomorphism in LFCat □

**Proposition 2.3.31.** Let $\Phi: \prod_{\alpha \in A} X_{\alpha} \to \prod_{\beta \in B} Y_{\beta}$ an isomorphism of connected loop-free categories. Fix $\alpha \in A$ and $\beta \in B$. With

$$ Y_{\beta}^{\alpha} := \pi_{\beta} \Phi[X_{\alpha}^{s}] \qquad X_{\alpha}^{\beta} := \pi_{\alpha} \Phi^{-1}[Y_{\beta}^{\Phi(s)}] $$

The two following morphisms are inverse of each other

$$ \pi_{\alpha} \circ \Phi^{-1} \circ \Xi_{\beta}^{\Phi(s)} : Y_{\beta}^{\alpha} \to X_{\alpha}^{\beta} \qquad \pi_{\beta} \circ \Phi \circ \Xi_{\alpha}^{s} : X_{\alpha}^{\beta} \to Y_{\beta}^{\alpha} $$

**Proof.** Let us prove that

$$ \pi_{\beta} \Phi \circ \Xi_{\alpha}^{s} \pi_{\alpha} \circ \Phi^{-1} \Xi_{\beta}^{\Phi(s)}|_{Y_{\beta}^{\alpha}} : Y_{\beta}^{\alpha} \to Y_{\beta}^{\alpha} \text{ is the identity.} $$

First let us remark that $\pi_{\beta} \Phi \circ \Phi^{-1} \Xi_{\beta}^{\Phi(s)} = \text{id}_{Y_{\beta}^{\alpha}}$ and $\Xi_{\alpha}^{s} \pi_{\alpha}|_{X_{\alpha}^{s}} = \text{id}_{X_{\alpha}^{s}}$ (Corollary 2.3.28). But this contraction can only be made if we prove that $\Phi^{-1} \Xi_{\beta}^{\Phi(s)}$ sends $Y_{\beta}^{\alpha}$ to a subcategory of $X_{\alpha}^{s}$. As $\pi_{\beta} \Phi \Xi_{\alpha}^{s}: X_{\alpha} \to Y_{\beta}^{\alpha}$ is full and essentially surjective by Proposition 2.3.30, it is equivalent to proving that $\Phi^{-1} \Xi_{\beta}^{\Phi(s)} \pi_{\beta} \Phi \Xi_{\alpha}^{s}$ sends $X_{\alpha}$ to a subcategory of $X_{\alpha}^{s}$

Let $f_{\alpha} \in X_{\alpha}$ and $\lambda \in A, \lambda \neq \alpha$. By definition, $\pi_{\lambda} \text{id}_{s} = \pi_{\lambda} \Xi_{\alpha}^{s} f$. Thus, by Corollary 2.3.25,

$$ \pi_{\lambda} \Phi^{-1}(\Phi(\text{id}_{s}), \Phi(\Xi_{\alpha}^{s} f)_{\beta}, \beta) = \pi_{\lambda} \text{id}_{s} $$

$$ \text{i.e.} \qquad \pi_{\lambda} \Phi^{-1} \Xi_{\beta}^{\Phi(s)} \pi_{\beta} \Phi \Xi_{\alpha}^{s} f = \pi_{\lambda} \text{id}_{s} $$

Thus, $\Phi^{-1} \Xi_{\beta}^{\Phi(s)} \pi_{\beta} \Phi \Xi_{\alpha}^{s}$ sends $X_{\alpha}$ to a subcategory of $X_{\alpha}^{s}$. Such that,

$$ \begin{aligned} \pi_{\beta} \Phi \circ \Xi_{\alpha}^{s} \pi_{\alpha} \circ \Phi^{-1} \Xi_{\beta}^{\Phi(s)}|_{Y_{\beta}^{\alpha}} &= \pi_{\beta} \Phi \circ \Xi_{\alpha}^{s} \pi_{\alpha} \circ \Phi^{-1} \Xi_{\beta}^{\Phi(s)}|_{Y_{\beta}^{\alpha}} \\ &= \pi_{\beta} \circ \Phi \circ \Phi^{-1} \circ \Xi_{\beta}^{\Phi(s)}|_{Y_{\beta}^{\alpha}} \\ &= \pi_{\beta} \Xi_{\beta}^{\Phi(s)}|_{Y_{\beta}^{\alpha}} \end{aligned} $$

$$ \pi_{\beta} \Phi \circ \Xi_{\alpha}^{s} \pi_{\alpha} \circ \Phi^{-1} \Xi_{\beta}^{\Phi(s)}|_{Y_{\beta}^{\alpha}} = \text{id}_{Y_{\beta}^{\alpha}} \qquad \text{Corollary 2.3.28} $$

$$ \text{Similarly, } \pi_{\alpha} \Phi^{-1} \Xi_{\beta}^{\Phi(s)} \circ \pi_{\beta} \Phi \Xi_{\alpha}^{s}|_{X_{\alpha}^{\beta}} = \text{id}_{X_{\alpha}^{\beta}} \qquad \square $$
With this we have all we need to build the isomorphism $\Psi_1 = (b_\beta)_{\beta \in B} : \prod_{\beta \in B} Y_\beta \to \prod_{\alpha \in A, \beta \in B} X_\alpha^\beta$ and $\Psi_2 = (a_\alpha)_{\alpha \in A} : \prod_{\alpha \in A} X_\alpha \to \prod_{\alpha \in A, \beta \in B} X_\alpha^\beta$ from Definition 2.3.18, i.e. all the morphisms in Diagram 2.2 are isomorphisms.

**Proposition 2.3.32.** With the previous notations and with

$$ \Psi_1 = \left( \prod_{\beta \in B} \Phi^{-1} \circ \Xi_{\beta}^{\Phi(s)} \right) \qquad \Psi_2 = \prod_{\alpha \in A} \left( \prod_{\beta \in B} \left( \pi_{\alpha} \circ \Phi^{-1} \circ \Xi_{\beta}^{\Phi(s)} \right) \circ \Phi \circ \Xi_{\alpha}^{s} \right) $$

$\Psi \circ \Phi$ and $\Psi_2$ are isomorphisms of connected loop-free categories. Furthermore, for all $\alpha \in A$, $\beta \in B$, $\pi_\beta \Psi_1$ and $\pi_\alpha \Psi_2$ are isomorphisms.

*Proof.* • $\Psi_1$ is an isomorphism. Indeed, by Corollary 2.3.28 $\Xi_{\beta}^{\Phi(s)}: Y_{\beta} \to Y_{\beta}^{\Phi(s)}$ is an isomorphism. By 2.3.30, so is $\Phi^{-1}: Y_{\beta}^{\Phi(s)} \to \prod_{\alpha \in A} X_{\alpha}^{\beta}$. Thus, as products of isomorphism, all arrows in the following diagram are isomorphisms.

$$ \prod_{\beta \in B} Y_{\beta} \xrightarrow{\prod_{\beta \in B} \Xi_{\beta}^{\Phi(s)}} \prod_{\beta \in B} Y_{\beta}^{\Phi(s)} \xrightarrow{\prod_{\beta \in B} \Phi^{-1}} \prod_{\beta \in B} \prod_{\alpha \in A} X_{\alpha}^{\beta} $$

• Let us prove that $\Psi_2$ is an isomorphism. Indeed, by Corollary 2.3.28, resp. Proposition 2.3.30 resp. 2.3.31, the following functors are all isomorphisms:

$$ X_{\alpha} \xrightarrow{\Xi_{\alpha}^{s}} X_{\alpha}^{s} \xrightarrow{\Phi} \prod_{\beta \in B} Y_{\beta}^{\alpha} \xrightarrow{\prod_{\beta \in B} \pi_{\alpha} \circ \Phi^{-1} \circ \Xi_{\beta}^{\Phi(s)}} \prod_{\beta \in B} X_{\alpha}^{\beta} $$

It follows that $\Psi_2 = \prod_{\lambda \in A} \left( \prod_{\beta \in B} \left( \pi_{\alpha} \circ \Phi^{-1} \circ \Xi_{\beta}^{\Phi(s)} \right) \circ \Phi \circ \Xi_{\alpha}^{s} \right)$ is an isomorphism by composition and product of isomorphisms. Furthermore, each $\pi_{\alpha} \Psi_2$ is an isomorphism
$\square$

Now let us prove the commutativity of the Diagram 2.3.

**Proposition 2.3.33.** Let $\mu \in B$, $f \in \prod_{\alpha \in A} X_{\alpha}^{\mu} = \prod_{\alpha \in A} \pi_{\alpha} \Phi^{-1} [Y_{\mu}^{\Phi(s)}]$, with $\Psi_1$ and $\Psi_2$ as defined in Proposition 2.3.32. Then for all $\beta \in B$ and $\alpha \in A$

$$ \pi_{\beta} \pi_{\alpha} (\gamma^{-1} \circ \Psi_1 \circ \Phi)(f) = \pi_{\beta} \pi_{\alpha} \Psi_2(f) = \begin{cases} f_{\alpha} & \text{if } \beta = \mu \\ s_{\alpha} & \text{otherwise} \end{cases} $$

*Proof.* By definition of $\gamma$, the equality of Proposition 2.3.33 above is equivalent to

$$ (\Psi_1 \circ \Phi(f)_\beta)_\alpha = ((\gamma \circ \Psi_2(f))_\beta)_\alpha = \begin{cases} f_\alpha & \text{if } \beta = \mu \\ s_\alpha & \text{otherwise} \end{cases} $$

Let $f = (f_\alpha)_{\alpha \in A} \in \prod_{\lambda \in A} X_\lambda^\mu$. By Proposition 2.3.30, $\Phi(f) \in Y_\mu^{\Phi(s)}$ with $\Phi(f) = (\Phi(\mathrm{id}_s), \Phi(f)_\mu, \mu)$ and $\Phi(f)_\mu \in Y_\mu$.
* For $\Psi_1 \circ \Phi = \prod_{\beta \in B} \Phi^{-1} \circ \Xi_{\beta}^{\Phi(s)} \circ \pi_{\beta} \Phi$

$$ 
\begin{align*}
\pi_{\beta} \Psi_1 \circ \Phi(f) &= \Phi^{-1} \circ \Xi_{\beta}^{\Phi(s)} \circ \Phi(f)_{\beta} \\
&= \Phi^{-1}(\mathrm{id}_{\Phi(s)}, \Phi(f)_{\beta}, \beta) \tag*{Definition 2.3.20} \\
&= \Phi^{-1}(\mathrm{id}_{\Phi(s)}, (\mathrm{id}_{\Phi(s)}, \Phi(f)_{\mu}, \mu)_{\beta}, \beta)
\end{align*}
$$

$$ \pi_{\beta} \Psi_1 \circ \Phi(f) = \begin{cases} \Phi^{-1}(\mathrm{id}_{\Phi(s)}) = \mathrm{id}_s & \text{if } \mu \neq \beta \\ \Phi^{-1}(\mathrm{id}_{\Phi(s)}, \Phi(f)_{\mu}, \mu) = f & \text{if } \mu = \beta \end{cases} $$

* For $\gamma \circ \Psi_2 = \prod_{\alpha \in A} \left( \prod_{\beta \in B} \pi_{\alpha} \Phi^{-1} \circ \Xi_{\beta}^{\Phi(s)} \right) (\Phi \circ \Xi_{\alpha}^{s})$

$$ - \beta \neq \mu. $$

By definition, $\mathrm{id}_s = \Phi^{-1}\Phi(\mathrm{id}_s) \in \Phi^{-1}[Y_{\mu}^{\Phi(s)}] = \prod_{\alpha \in A} X_{\alpha}^{\mu}$, such that for all $\alpha \in A$, $\Xi_{\alpha}^{s}f_{\alpha} \in \prod_{\alpha \in A} X_{\alpha}^{\mu}$ i.e. $\Phi \circ \Xi_{\alpha}^{s}(f_{\alpha}) \in Y_{\mu}^{\Phi(s)}$ and thus for all $\beta \neq \mu$, $\pi_{\beta}\Phi \circ \Xi_{\alpha}^{s}(f_{\alpha}) = \Phi(\mathrm{id}_s)_{\beta}$.

Thus, for all $\beta \neq \mu$

$$ 
\begin{align*}
\pi_{\alpha} \pi_{\beta} \circ \gamma \circ \Psi_2(f) &= \pi_{\alpha} \Phi^{-1} \Xi_{\beta}^{\Phi(s)} \left( \pi_{\beta} \Phi \circ \Xi_{\alpha}^{s}(f_{\alpha}) \right) \\
&= \pi_{\alpha} \Phi^{-1} \Xi_{\beta}^{\Phi(s)} (\Phi(\mathrm{id}_s)_{\beta}) \\
\pi_{\alpha} \pi_{\beta} \circ \gamma \circ \Psi_2(f) &= \pi_{\alpha} \mathrm{id}_s
\end{align*}
$$

$- \mu = \beta$. Then, $f \in \prod_{\lambda \in A} X_{\lambda}^{\mu}$ therefore $\Phi(f) = (\Phi(\mathrm{id}_s), \Phi(f)_{\beta}, \beta)$. It follows that

$$ \forall g_{\beta} \in Y_{\beta}, (\Phi(f), g_{\beta}, \beta) = (\Phi(\mathrm{id}_{s}), g_{\beta}, \beta) \quad (2.10) $$

Furthermore $\pi_{\alpha} \Phi^{-1} \Phi(f) = \pi_{\alpha} \Phi^{-1} \Phi(\mathrm{id}_s, f_{\alpha}, \alpha) = f_{\alpha}$. Hence,

$$ 
\begin{align*}
f_{\alpha} &= \pi_{\alpha} \Phi^{-1}(\Phi(f), (\Phi(\mathrm{id}_{s}, f_{\alpha}, \alpha))_{\beta}, \beta) && \text{By Corollary 2.3.25} \\
&= \pi_{\alpha} \Phi^{-1}(\Phi(\mathrm{id}_{s}), (\Phi(\mathrm{id}_{s}, f_{\alpha}, \alpha))_{\beta}, \beta) && \text{By Eq. (2.10)}
\end{align*}
$$

$$ f_{\alpha} = \pi_{\alpha} \pi_{\beta} \gamma \circ \Psi_2(f) \qquad \text{By definition of } \Psi_2 $$

□

Now that commutativity of Diagram 2.3 is proven, we extend the commutativity along one of the $\lambda \in A$, thus proving the commutativity of the Diagram 2.2. First as explained in the outline, we will to prove the faithfulness of the restriction, which is less trivial in our case.

**Lemma 2.3.34.** With the previous notation, $\gamma: \prod_{\beta \in B} \prod_{\alpha \in A} X_{\alpha}^{\beta} \to \prod_{\alpha \in A} \prod_{\beta \in B} X_{\alpha}^{\beta}$ the natural isomorphism and with $\tilde{s}_{\lambda}$ the singleton category for a given $\lambda \in A$, the following restrictions are faithful functors.

$$ 
\begin{align*}
\pi_{\lambda} \gamma^{-1} \Psi_1 \circ \Phi |_{X_{\lambda}^s} &\qquad \pi_{\{\alpha \in A | \alpha \neq \lambda\}} \gamma^{-1} \Psi_1 \circ \Phi |_{\prod_{\alpha \neq \lambda} X_{\alpha} \times \tilde{s}_{\lambda}} \\
\pi_{\lambda} \Psi_2 |_{X_{\lambda}^s} &\qquad \pi_{\{\alpha \in A | \alpha \neq \lambda\}} \Psi_2 |_{\prod_{\alpha \neq \lambda} X_{\alpha} \times \tilde{s}_{\lambda}}
\end{align*}
$$
$$ \textit{Proof.} \quad \bullet \quad \Psi_1 \circ \Phi = \left( \prod_{\beta \in B} \Phi^{-1} \circ \Xi_{\beta}^{\Phi(s)} \right) \circ \Phi $$

Let $f = (f_\alpha)_{\alpha \in A} \in X_\lambda^s$, then $\pi_\alpha f = \pi_\alpha \mathrm{id}_s$ for all $\alpha \neq \lambda$. Thus, by Corollary 2.3.25, for all $\beta \in B$ and all $\alpha \neq \lambda$,

$$ \pi_{\alpha} \Phi^{-1}(\Phi(\mathrm{id}_s), \Phi(f)_{\beta}, \beta) = \pi_{\alpha} \mathrm{id}_s $$

i.e. $\pi_\alpha \pi_\beta \Psi_1 \circ \Phi(f) = \pi_\alpha \mathrm{id}_s$. Thus

$$ \begin{aligned} \Psi_1(f) \circ \Phi &= (\mathrm{id}_s, (\pi_\beta \Psi_1(f))_\lambda, \lambda)_{\beta \in B} \\ &= (\Xi_\lambda^s(\pi_\lambda \pi_\beta \Psi_1(f)))_{\beta \in B} \\ &= \left(\prod_{\beta \in B} \Xi_\lambda^s\right) (\pi_\lambda \pi_\beta \Psi_1(f))_{\beta \in B} \\ \Psi_1 \circ \Phi(f) &= \left(\prod_{\beta \in B} \Xi_\lambda^s\right) \circ (\pi_\lambda \gamma^{-1} \Psi_1 \circ \Phi)(f) \end{aligned} $$

This is true for all $f \in X_\lambda^s$, thus:

$$ \Psi_1 \circ \Phi|_{X_\lambda^s} = \left( \prod_{\beta \in B} \Xi_\lambda^s \right) \circ \left( \pi_\lambda \gamma^{-1} \Psi_1 \circ \Phi \right)|_{X_\lambda^s} $$

By faithfulness of $\Psi_1 \circ \Phi$ (Proposition 2.3.32) and $\Xi_\lambda^s$ (Lemma 2.3.27), this implies $\pi_\lambda \gamma^{-1} \Psi_1 \circ \Phi|_{X_\lambda^s}$ faithful.

Now let $f \in (f_\alpha)_{\alpha \in A} \in \prod_{\alpha \neq \lambda} X_\alpha \times \tilde{s}_\lambda$, then $\pi_\lambda f = \pi_\lambda \mathrm{id}_s$. By Corollary 2.3.25, this implies for all $\beta \in B$

$$ \pi_{\lambda} \Phi^{-1}(\Phi(\mathrm{id}_{s}), \Phi(f)_{\beta}, \beta) = \pi_{\lambda} \mathrm{id}_{s} $$

i.e. $\pi_\lambda \pi_\beta \Psi_1 \circ \Phi(f) = \pi_\lambda \mathrm{id}_s$ such that

$$ \begin{aligned} \Psi_1 \circ \Phi(f) &= (\pi_\beta \Psi_1 \circ \Phi(f), \mathrm{id}_{s_\lambda}, \lambda)_{\beta \in B} \\ &= ((\pi_\alpha \pi_\beta \Psi_1 \circ \Phi(f))_{\alpha \in A}, \mathrm{id}_{s_\lambda}, \lambda)_{\beta \in B} \end{aligned} \qquad \text{Corollary 2.3.25} $$

$$ \Psi_1 \circ \Phi(f) = ((\pi_\beta \pi_\alpha \gamma^{-1} \Psi_1 \circ \Phi(f))_{\alpha \in A}, \mathrm{id}_{s_\lambda}, \lambda)_{\beta \in B} $$

Faithfulness of $\Psi_1 \circ \Phi$ then implies the faithfulness of $((\pi_\beta \pi_\alpha \gamma^{-1} \Psi_1 \circ \Phi(\cdot))_{\alpha \neq \lambda})_{\beta \in B}$, i.e. the faithfulness of $\pi_{\alpha \neq \lambda} \gamma^{-1} \Psi_1 \circ \Phi$ on the subcategory $\prod_{\alpha \neq \lambda} X_\alpha \times \tilde{s}_\lambda$

$$ \bullet \quad \Psi_2 = \prod_{\alpha \in A} \left( \prod_{\beta \in B} \left( \pi_{\alpha} \circ \Phi^{-1} \circ \Xi_{\beta}^{\Phi(s)} \right) \circ \Phi \circ \Xi_{\alpha}^{s} \right) $$

By Proposition 2.3.32, each $\pi_\alpha \Psi_2$ is an isomorphism, thus a fortiori, the restriction $\pi_\alpha \Psi_2|_{X_\alpha^s}$ is faithful. Hence, $\pi_{\{\alpha \in A | \alpha \neq \lambda\}} \Psi_2|_{\prod_{\alpha \neq \lambda} X_\alpha \times \tilde{s}_\lambda}$ is faithful as a product of faithful functors.

□

**Proposition 2.3.35.** With the previous notation, $\Psi_1 \circ \Phi = \gamma \circ \Psi_2$
*Proof.* Let $\Psi \in \{\Psi_2, \gamma^{-1} \circ \Psi_1 \circ \Phi\}$ and $\mu \in B$. Let $f_\lambda^\mu \in X_\lambda^\mu$. By Proposition 2.3.33, $\Psi_2$ and $\gamma^{-1} \circ \Psi_1 \circ \Phi$ are equal when we restrict to $\prod_{\alpha \in A} X_\alpha^\mu$. As explained above, we wish to extend this equality to the full domain. Proposition 2.3.33 also implies that for all $g^\mu \in \prod_{\alpha \in A} X_\alpha^\mu$, $\pi_\lambda \Psi(g^\mu, f_\lambda^\mu, \lambda) = \pi_\lambda \Psi(s, f_\lambda^\mu, \lambda)$. Thus, by Lemma 2.3.26, for all $f_\lambda \in X_\lambda$, for all $g^\mu \in \prod_{\alpha \in A} X_\alpha^\mu$

$$ \pi_{\lambda}\Psi(g^{\mu}, f_{\lambda}, \lambda) = \pi_{\lambda}\Psi(s, f_{\lambda}, \lambda) = \pi_{\lambda}\Psi\Xi_{\lambda}^{s}(f_{\lambda}) \stackrel{\text{def}}{=} \Psi_{\lambda}(f_{\lambda}) \quad (2.11) $$

We want to prove that for all $\lambda \in A$, $\mu \in B$, $g^\mu \in \prod_{\alpha \in A} X_\alpha^\mu$, $f_\lambda \in X_\lambda$, the projection on any $\alpha \neq \lambda$ of $\Psi(g^\mu, f_\lambda, \alpha)$ depends only on $g^\mu$, i.e.

$$ (g^{\mu}, f_{\lambda}, \lambda) = \Psi^{-1}(\Psi(g^{\mu}), \Psi_{\lambda}(f_{\lambda}), \lambda) $$

* For $\alpha \neq \lambda$, $\pi_\alpha \Psi^{-1} \Psi(g^\mu, f_\lambda, \lambda) = g_\alpha^\mu = \pi_\alpha \Psi^{-1} \Psi(g^\mu)$. Thus, by Corollary 2.3.25,

$$ \pi_{\alpha}\Psi^{-1}(\Psi(g^{\mu}), \Psi(g^{\mu}, f_{\lambda}, \lambda)_{\lambda}, \lambda) = g_{\alpha}^{\mu} $$

By definition of $\Psi_\lambda(f_\lambda)$ (Eq. (2.11))

$$ \pi_{\alpha}\Psi^{-1}(\Psi(g^{\mu}), \Psi_{\lambda}(f_{\lambda}), \lambda) = g_{\alpha}^{\mu} \quad (2.12) $$

* For $\lambda$, By Eq. (2.12), $\Psi^{-1}(\Psi(g^\mu), \Psi_\lambda(f_\lambda), \lambda) \in (X_\alpha^\mu, X_\lambda, \lambda)$, such that by Eq. (2.11)

$$ \begin{aligned} \pi_{\lambda}\Psi\Xi_{\lambda}^{s}(\pi_{\lambda}\Psi^{-1}(\Psi(g^{\mu}), \Psi_{\lambda}(f_{\lambda}), \lambda)) &= \pi_{\lambda}\Psi\Psi^{-1}(\Psi(g^{\mu}), \Psi_{\lambda}(f_{\lambda}), \lambda) \\ &= \Psi_{\lambda}(f_{\lambda}) \end{aligned} $$ $$ \begin{aligned} \pi_{\lambda}\Psi\Xi_{\lambda}^{s}(\pi_{\lambda}\Psi^{-1}(\Psi(g^{\mu}), \Psi_{\lambda}(f_{\lambda}), \lambda)) &= \pi_{\lambda}\Psi\Xi_{\lambda}^{s}(f_{\lambda}) \quad \text{Eq. (2.11)} \end{aligned} $$

By faithfulness of $\pi_\lambda \Psi \Xi_\lambda^s$ (Lemma 2.3.34),

$$ \pi_{\lambda}\Psi^{-1}(\Psi(g^{\mu}), \Psi_{\lambda}(f_{\lambda}), \lambda) = f_{\lambda} \quad (2.13) $$

By Eq. (2.12) and Eq. (2.13), we have $(g^\mu, f_\lambda, \lambda) = \Psi^{-1}(\Psi(g^\mu), \Psi_\lambda(f_\lambda), \lambda)$ i.e.

$$ \Psi(g^{\mu}, f_{\lambda}, \lambda) = (\Psi(g^{\mu}), \Psi_{\lambda}(f_{\lambda}), \lambda) \quad (2.14) $$

So far Eq. (2.14) only holds when $g^\mu \in \prod_{\alpha \in A} X_\alpha^\mu$. Let us prove that it is in fact valid for all $g \in \prod_{\alpha \in A} X_\alpha$, i.e. for all $\lambda \in A$ and for all $f_\lambda \in X_\lambda$

$$ \Psi(g, f_{\lambda}, \lambda) = (\Psi(g), \Psi_{\lambda}(f_{\lambda}), \lambda) $$

Let $\rho \in A$, $\rho \neq \lambda$. By Eq. (2.14), for all $f_\lambda \in X_\lambda$, $\pi_\rho \Psi(g^\mu, f_\lambda, \lambda) = \pi_\rho \Psi(g^\mu)$. By Lemma 2.3.26 this implies, for all $g \in \prod_{\alpha \in A} X_\alpha$, for all $f_\lambda \in X_\lambda$

$$ \pi_{\bar{\lambda}}\Psi(g, f_{\lambda}, \lambda) = \pi_{\bar{\lambda}}\Psi(g) := \Psi_{\bar{\lambda}}(g) \quad (2.15) $$

where $\pi_{\bar{\lambda}}$ is the projection on $A \setminus \{\lambda\}$.

Thus, proving $\Psi(g, f_\lambda, \lambda) = (\Psi(g), \Psi_\lambda(f_\lambda), \lambda)$ is equivalent to proving,

$$ (\Psi(g, f_{\lambda}, \lambda), \Psi_{\lambda}(f_{\lambda}), \lambda) = \Psi(g, f_{\lambda}, \lambda) $$

i.e.

$$ \Psi^{-1}(\Psi(g, f_{\lambda}, \lambda), \Psi_{\lambda}(f_{\lambda}), \lambda) = (g, f_{\lambda}, \lambda) $$

Let us look at the different projections
* On $X_\lambda$. 
  $\pi_\lambda \Psi^{-1}(\Psi(g, f_\lambda, \lambda)) = \pi_\lambda \Psi^{-1}(\Psi \Xi_\lambda^s(f_\lambda)) = f_\lambda$ implies by Corollary 2.3.25

$$ 
\begin{aligned}
\pi_\lambda \Psi^{-1}(\Psi(g, f_\lambda, \lambda), \pi_\lambda \Psi \Xi_\lambda^s(f_\lambda), \lambda) &= f_\lambda \\
\pi_\lambda \Psi^{-1}(\Psi(g, f_\lambda, \lambda), \Psi_\lambda(f_\lambda), \lambda) &= f_\lambda \quad \text{Eq. (2.11)}
\end{aligned}
$$

* On $\prod \alpha \neq \lambda X_\alpha$ 
  By Eq. (2.15), for all $h \in \prod_{\alpha \in A} X_\alpha$, $\pi_\lambda \Psi(h, \mathrm{id}_{s_\lambda}, \lambda) = \pi_\lambda \Psi(h)$. Applying this to the element $h = \Psi^{-1}(\Psi(g, f_\lambda, \lambda), \Psi_\lambda(f_\lambda), \lambda)$ we get

$$ 
\begin{aligned}
\pi_\lambda \Psi(\Psi^{-1}(\Psi(g, f_\lambda, \lambda), \Psi_\lambda(f_\lambda), \lambda), \mathrm{id}_{s_\lambda}, \lambda) &= \pi_\lambda \Psi \Psi^{-1}(\Psi(g, f_\lambda, \lambda), \Psi_\lambda(f_\lambda), \lambda) \\
&= \pi_\lambda(\Psi(g, f_\lambda, \lambda), \Psi_\lambda(f_\lambda), \lambda) \\
&= \pi_\lambda \Psi(g, f_\lambda, \lambda)
\end{aligned}
\quad \text{Eq. (2.15)} 
$$

By faithfulness of $\pi_\lambda \Psi|_{(\prod_{\alpha \in A} X_\alpha, s_\lambda, \lambda)}$ (Lemma 2.3.34),

$$ 
\begin{aligned}
(\Psi^{-1}(\Psi(g, f_\lambda, \lambda), \Psi_\lambda(f_\lambda), \lambda), \mathrm{id}_{s_\lambda}, \lambda) &= (g, \mathrm{id}_{s_\lambda}, \lambda) \\
\pi_\lambda \Psi^{-1}(\Psi(g, f_\lambda, \lambda), \Psi_\lambda(f_\lambda)) &= \pi_\lambda g
\end{aligned}
$$

Thus $\Psi^{-1}(\Psi(g, f_\lambda, \lambda), \Psi_\lambda(f_\lambda), \lambda) = (g, f_\lambda, \lambda)$ and as such, for all $f_\lambda \in \lambda$, for all $g \in \prod_{\alpha \in A} X_\alpha$,

$$ \Psi(g, f_\lambda, \lambda) = (\Psi(g), \Psi_\lambda(f_\lambda), \lambda) $$

As this is true for any $f, g \in \prod_{\alpha \in A} X_\alpha$, and any $\lambda$, we get

$$ \Psi(f) = (\Psi_\alpha(f_\alpha))_{\alpha \in A} $$

All that is left to do is to prove that $\Psi_\alpha(f_\alpha)$ is the same whether $\Psi = \Psi_2$ or $\Psi = \gamma^{-1} \circ \Psi_1 \circ \Phi$. By Eq. (2.11)

$$ \Psi_\lambda(f_\lambda) = \pi_\lambda \Psi \Xi_\lambda^s(f_\lambda) $$

But, by definition

$$ 
\begin{aligned}
\pi_\beta \pi_\lambda \Psi_2(\Xi_\lambda^s f_\lambda) &= \pi_\beta \pi_\lambda (\Phi^{-1} \circ \Xi_\beta^{\Phi(s)} \circ \pi_\beta \circ \Phi \circ \Xi_\lambda^s)(\pi_\lambda(\Xi_\lambda^s f_\lambda)) \\
&= \pi_\beta \pi_\lambda (\Phi^{-1} \circ \Xi_\beta^{\Phi(s)} \circ \pi_\beta \circ \Phi \circ \Xi_\lambda^s)(f_\lambda) \quad \text{Lemma 2.3.27} \\
&= \pi_\beta \pi_\lambda (\Phi^{-1} \Xi_\beta^{\Phi(s)})(\pi_\beta \Phi)(\Xi_\lambda^s f_\lambda)
\end{aligned}
$$

$$ \pi_\beta \pi_\lambda \Psi_2(\Xi_\lambda^s f_\lambda) = \pi_\beta \pi_\lambda \gamma^{-1} \circ \Psi_1 \circ \Phi(\Xi_\lambda^s f_\lambda) \quad \text{by Definition of } \Psi_1 $$

This is true for all $\lambda$ and $\beta$, thus $\Psi_2 = \gamma^{-1} \circ \Psi_1 \circ \Phi$

<figure><img src="image_116.png" /></figure>

Finally, we have proven all the steps to prove our extension of Hashimoto's theorem.

**Theorem 2.3.36.** Every connected loop-free category has the strict refinement property.
# Chapter 3
## A syntactic model of programs

"I'm significant!...Screamed the dust speck."

– Bill Watterson, *Calvin & Hobbes*

Although topology offers a lot of interesting and powerful tools, programs are discrete objects, and we believe that such heavy machinery should not be necessary when studying them. In this chapter we present our result from [43] which introduces a new model of conservative programs. This model is based directly on the syntax of programs, and has as principal objective of making implementation of the tools introduced in the previous Section 1.3 much more practical. We follow the presentation of Section 1.3 to present our model and will translate all the different objects used in topological directed models according to the following table. Our main objective is to get back the powerful deadlock detection algorithms in our syntactic setting, which necessitates the compact representation by covers of the regions. Once again our first concern is to make these tools easier to implement and work with in practice and will influence many choices in the following sections.

<table><thead><tr><td>Geometric semantics</td><td>Syntactic semantics</td></tr></thead><tbody><tr><td>Directed topological spaces</td><td>Partially ordered sets</td></tr><tr><td>Pruned state space</td><td>Authorized positions</td></tr><tr><td>Points</td><td>Positions</td></tr><tr><td>Paths</td><td>Paths</td></tr><tr><td>n-cubes</td><td>(Syntactic) cubes</td></tr><tr><td>Cubical covers</td><td>(Syntactic) covers</td></tr><tr><td>Cubical regions</td><td>Support</td></tr><tr><td>Maximal cubical covers</td><td>Normal forms</td></tr></tbody></table>

In order to study and present this model, we first introduce a variant of the **PIMP** language we call **NPIMP**, focusing purely on the concurrent nature of the programs considered. Making full use of the nature of the language **NPIMP**, and of the notion
of conservativity, we represent the state (and execution traces) as positions of a partially ordered set, corresponding to prefixes of executions of our program.

Then to efficiently manipulate and describe the set of authorized positions, we introduce an analogous notion of cubical covers (Section 3.2.1) for the syntactic semantics of our program, where a (potentially infinite) set of positions called a support is described by a set of cubes (defined for generic posets) containing said points. We show in Section 3.2.3 that these “syntactic covers”, under reasonable assumptions, inherit the same boolean algebra structure as their topological equivalent. Using this structure, we define a canonical representative for the supports corresponding to actual “forbidden” and “authorized” region of programs, and explain how to implement its computation in Section 3.3.

These constructions allow us to implement the deadlock detection Algorithm 1.4.33 for the syntactic model in a fully automated tool *Sparkling*, which can be found in [42].

# 3.1 Syntactic semantics of concurrent programs

## 3.1.1 Positions in programs

As seen in the previous Chapter 1, for most of the models we introduced previously, reachability is undecidable, and many assumptions were made on the programs we consider in order to circumvent this difficulty (coherence of programs Definition 1.3.18, conservativity Definition 1.2.23) and focus on concurrency properties.

To further focus on the problems linked to the concurrent nature of our programs, we will remove arithmetic variables and boolean conditions altogether from **PIMP**. Indeed, the definitions for reachability, deadlocks, unsafe and doomed regions of Definition 1.3.59 does not take these into account, and we shall do the same.

In this chapter, we introduce a variant of the **PIMP** language: the non-deterministic **NPIMP**, or **NPIMP** for short. **NPIMP** uses similar constructors and actions but has no arithmetic expressions, nor boolean conditions and no variables, thus focusing purely on the parallel structure of the programs and their resource consumption.

**Definition 3.1.1.** Let $\mathcal{R}$ be a fixed, finite set of resources. Let $a \in \mathcal{R}$. The language **NPIMP** is generated by the following syntactic expressions, defined by their grammar:

* the set $\mathcal{X}$ of actions:

$$A ::= P_a | V_a | \mathbf{skip} | \dots$$

* the set $\mathcal{C}$ of commands, or programs:

$$P,Q ::= A | P;Q | P^* | P+Q | P \parallel Q$$

In this language, $P^*$ replaces while b do P and $P+Q$ replaces if b then P else Q. As explained above, we do not take variables into account, so that branching and looping is non-deterministic, but we could handle proper conditional branching and while loops in the same way that topological models do.

In a **NPIMP** program, we do not consider boolean conditions or arithmetic variables. Thus, a state $\sigma$ in our set of states $\Sigma$ for a program in **NPIMP** should be a function associating to each resource its consumption.
**Definition 3.1.2.** Given a program *P* in **NPIMP**, we write $\Sigma = \mathbb{Z}^R$ for the set of states of *P*, consisting of functions assigning an integer to each resource. The initial state $\sigma_0$ is the constant function equal to 0. The operational semantics of our programming language consists of two functions:

* $\llbracket - \rrbracket_X : \mathcal{X} \to \Sigma \to \Sigma$, describing the evaluations of actions

* $\llbracket - \rrbracket_C : C \to \Sigma \to \Sigma$, describing the evaluations of commands or programs.

As we only are considering resources, the function $\llbracket - \rrbracket_X$ is easy to define. $P_a$ increases the consumption of a resource, while $V_a$ diminishes it. All other actions are considered to have no effect.

**Definition 3.1.3.** Given a program *P* in **NPIMP**, the evaluation of the actions $P_a$ and $V_a$ are the functions $\llbracket P_a \rrbracket_X$, $\llbracket V_a \rrbracket_X : \Sigma \to \Sigma$ defined as follows for each $\sigma \in \Sigma$:

$$ \llbracket P_a \rrbracket_X(\sigma) = \delta_a^+(\sigma) \qquad \llbracket V_a \rrbracket_X(\sigma) = \delta_a^-(\sigma) $$

where

$$ \delta_a^+(\sigma)(b) = \begin{cases} \sigma(a) + 1 & \text{if } b = a \\ \sigma(a) & \text{otherwise} \end{cases} \qquad \delta_a^+(\sigma)(b) = \begin{cases} \sigma(a) - 1 & \text{if } b = a \\ \sigma(a) & \text{otherwise} \end{cases} $$

Instead of generating the state space inductively as in Definition 1.3.31 or Definition 1.3.13, we will instead generate the set of “states” or *positions* of our program directly.

By restraining ourselves to conservative programs, as in Section 1.2.3, the consumption of resources of an execution will depend only on its endpoints. For **NPIMP** consumption and evaluation of an execution is the same, as there is only resources. Thus, for such programs, we can define the semantics of programs solely for their *positions* (states).

### 3.1.1.1 Positions of a program

A *position* in a program describes where we are during a potential execution of the program and thus encodes the “prefix” of the program which has already been executed. Formally, we begin by the following definition.

**Definition 3.1.4.** The *pre-positions* $p$ are generated by the following grammar, with $n \in \mathbb{N}$:

$$ p, q ::= \bot \mid \top \mid p; q \mid p^n \mid p+\emptyset \mid \emptyset+q \mid p \parallel q $$

Those can be read as: we have not started (resp. we have finished) the execution ($\bot$, resp. $\top$), we are executing a sequence ($p; q$), we are in the $n$-th iteration of a loop ($p^n$), we are executing a branch of a conditional branching ($p+\emptyset$, $\emptyset+q$) and we are executing two programs in parallel ($p \parallel q$).

*Remark 3.1.5.* Note that the syntax of positions is essentially the same as the one of programs, except that actions have been replaced by $\bot$ and $\top$ (and loops are “unfolded” in the sense that we keep track of the loop number).
Next, we single out the pre-positions which are actual positions (states) for a program. For instance, we want that, in a program of the form $P;Q$, we can begin executing $Q$ only after $P$ has been fully executed: this means that a pre-position of the form $p;q$ with $q \neq \perp$ is a *position* only when $p$ is $\top$. Similarly, in a conditional branching $P+Q$, we cannot execute both subprograms: that is why positions of $P+Q$ are of the form $p+\emptyset$ and $\emptyset+q$.

*Remark 3.1.6.* In [43], we had previously defined positions of $P+Q$ as $p+\perp$ and $\perp+q$. This was changed in order to make some proofs easier to understand in Section 4.2. This has no effect on the results of this section and all proofs have been suitably modified to take this change into account.

**Definition 3.1.7.** Given a program $P$, we write $P \models p$ to indicate that a pre-position $p$ is a *position* of a program $P$, this predicate being defined inductively by the following rules, for any program $P, Q, R$:

$$ \frac{\begin{array}{l} P \neq Q \parallel R \\ P \models \perp \end{array}}{P \models \top} \qquad \frac{\begin{array}{l} P \models p \\ P;Q \models p;\perp \end{array}}{P+Q \models p+\emptyset} \qquad \frac{\begin{array}{l} P \models p \\ P^* \models p^n \end{array}}{P \models p} $$

For programs of the form $P \parallel Q$, we write $\perp$ (resp. $\top$) as a shorthand for $\perp \parallel \perp$ (resp. $\top \parallel \top$)
We write $\mathcal{P}(P)$ for the set of positions of a program $P$.

*Remark 3.1.8.* Contrary to what we did in [43], we do not have the positions $P \parallel Q \models \perp$ and $P \parallel Q \models \top$. This makes it easier to represent parallel composition of processes as multidimensional “cubes”. The surcharge of the notation $\perp$ and $\top$ will be justified in Proposition 3.1.24 as $\perp \parallel \perp$ and $\top \parallel \top$ serve the same role as $\perp$ and $\top$ respectively as lower and upper bound of the lattice $\mathcal{P}(P \parallel Q)$. All proofs from [43] have been adapted to reflect this change.

### 3.1.1.2 Operational semantics

We will now, as in Section 1.1.2, introduce an intermediate reduction relation to describe how our prefixes of executions (our positions, which are also our state) progress towards another. Here, we do not restrict the transitions to those which would lock resources more than their capacity or release unlocked resources as in Section 1.2.4. We will allow such paths for now and filter them out afterwards.
**Definition 3.1.9.** The *reduction* relation is defined inductively by

$$
\begin{array}{ccc}
\frac{}{P+Q \models \bot \rightarrow \emptyset + \bot} & \frac{}{P+Q \models \emptyset + q \rightarrow \emptyset + q'} & \frac{}{P+Q \models \emptyset + \top \rightarrow \top} \\[1.5em]
\frac{}{P+Q \models \bot \rightarrow \bot + \emptyset} & \frac{}{P+Q \models p \rightarrow p'} & \frac{}{P+Q \models \top + \emptyset \rightarrow \top} \\[1.5em]
\frac{}{P;Q \models \bot \rightarrow \bot; \bot} & \frac{P \models p \rightarrow p' \qquad Q \models q}{P \parallel Q \models p \parallel q \rightarrow p' + q} & \frac{P \models p \qquad Q \models q \rightarrow q'}{P \parallel Q \models p \parallel q \rightarrow p + q'} \\[1.5em]
\frac{}{P^* \models \bot \rightarrow \bot^0} & \frac{P \models p \rightarrow p'}{P^* \models p^n \rightarrow p'^n} & \frac{Q \models q \rightarrow q'}{P;Q \models \top; q \rightarrow \top; q'} \\[1.5em]
\frac{}{P^* \models p \rightarrow p'} & \frac{}{P^* \models \top^n \rightarrow \bot^{n+1}} & \frac{}{P^* \models \top^n \rightarrow \top} \\[1.5em]
\frac{A \in \mathcal{X}}{A \models \bot \rightarrow \top} & &
\end{array}
$$

Remark 3.1.10. The above operational semantics is very “fine-grained” in the sense that it features transitions which are not usually observable, such as $P;Q \models \bot \rightarrow \bot; \bot$ which corresponds to passing from a state where we have not yet started executing the program to a state where we have started executing a sequence, but not yet its components. The usual “real” actions correspond to executions of the lower left rule $A \models \bot \rightarrow \top$ which can be interpreted as executing an action $A$.

Furthermore, the relation is well-defined as proven by the following lemma. Combined with Corollary 3.1.26 this formalizes the fact that the positions in Definition 3.1.7 captures exactly the expected states of our program.

**Lemma 3.1.11.** If $P \models p \rightarrow p'$ holds then both $P \models p$ and $P \models p'$ hold.

*Proof.* This is proved by an easy induction on the derivation of the reduction. For instance, consider the case where the last rule is

$$ \frac{P \models p \rightarrow p' \qquad Q \models q}{P \parallel Q \models p \parallel q \rightarrow p' \parallel q} $$

By induction hypothesis, we have a derivation of $P \models p \rightarrow p'$ and thus both $P \models p$ and $P \models p'$ hold. We can use the rules

$$ \frac{P \models p \qquad Q \models q}{P \parallel Q \models p \parallel q} \qquad \frac{P \models p' \qquad Q \models q}{P \parallel Q \models p' \parallel q} $$

to show that both $P \parallel Q \models p \parallel q$ and $P \parallel Q \models p' \parallel q$ hold. Other cases are similar. $\square$

We can define the consumption of a path $\pi$. Each action $P_a$ or $V_a$ modifies the consumption according to intuition and the operational semantics already defined in Definition 3.1.3.

First, we recall and adapt some definitions from Section 1.1.2:
**Definition 3.1.12.** Given a program *P*, the state space *G*<sub>*P*</sub> of this program is the graph whose vertices are the positions of *P* (Definition 3.1.7) and edges are the reductions (Definition 3.1.9).

**Definition 3.1.13.** Given a program *P*, a *path* on *G*<sub>*P*</sub> is a sequence of reduction π = (*P* ⊢ *p*<sub>*i*</sub> → *p*<sub>*i*+1</sub>)<sub>0≤*i*<*n*</sub> also written *P* ⊢ π : *p* →<sub>*i*</sub><sup>*</sup> *p*<sub>*n*</sub> or π : *p*<sub>0</sub> →<sub>*</sub><sup>*</sup> *p*<sub>*n*</sub>. With the following constructions:

* Given two paths π: *p* →<sup>*</sup> *q* and π': *q* →<sup>*</sup> *p'* we write π' · π: *p* →<sup>*</sup> *p'* for their concatenation.

* The empty path on a state *p* is written ε<sub>*p*</sub>: *p* →<sup>*</sup> *p*.

Furthermore, we say that

* An execution trace π of *P* is a path *P* ⊢ π : ⊥ →<sub>*P*</sub><sup>*</sup> *p*. When *p* = ⊤<sub>*P*</sub>, i.e. *P* ⊢ π : ⊥ →<sup>*</sup> ⊤, we say that π is *total*.

* An execution trace π of *P* is *maximal* when it cannot be extended.

* An execution is *elementary* when it consists of one reduction step.

* A position *p* is reachable when there exists an execution trace π with *p* as target i.e. *P* ⊢ π : ⊥ →<sub>*P*</sub><sup>*</sup> *p*.

As customary, we also write $P \vdash p \to^* p'$ (or sometimes simply $p \to^* p'$) when there exists a path $P \vdash \pi : p \to^* p'$.

**Definition 3.1.14.** Given an execution $P \vdash \pi : p \to^* p'$, we write $[[P \vdash \pi : p \to^* p')] : \Sigma \to \Sigma$ (or sometimes simply $[[\pi]]$) for its *evaluation* or *consumption* of mutexes. This function is defined for elementary executions on each state $\sigma \in \Sigma$ by:

* For $a \in \mathcal{R}$, $[[P_a \vdash \pi : \bot \to \top]](\sigma) = [[P_a]]_X = \delta_a^+(\sigma)$,

$$ \delta_a^+(\sigma)(b) = \begin{cases} \sigma(a) + 1 & \text{if } b = a \\ \sigma(a) & \text{otherwise} \end{cases} $$

* For $a \in \mathcal{R}$, $[[V_a \vdash \pi : \bot \to \top]] = [[V_a]]_X = \delta_a^+(\sigma)$,

$$ \delta_a^+(\sigma)(b) = \begin{cases} \sigma(a) - 1 & \text{if } b = a \\ \sigma(a) & \text{otherwise} \end{cases} $$

* For each reduction π, different from the two above, deduced with a rule of Definition 3.1.9 with no premise we have $[[\pi]](\sigma) = \sigma$.

* For each reduction π deduced with a rule of Definition 3.1.9 with one reduction π' as premise, we have $[[\pi]] = [[\pi']]$.

And extended as a morphism of the category of executions on the monoid of consumptions, i.e. $[[\varepsilon]] = \text{id}$ and $[[\pi \cdot \pi')] = [[\pi']]] + [[\pi]]$.
**Definition 3.1.15.** A program *P* is *conservative* when for any pair of paths π, τ: *x* →*y* in *G*<sub>*P*</sub> with same source and target we have for any state σ ∈ Σ and any resource *a* ∈ 𝒜:

$$ \llbracket \pi \rrbracket(\sigma)(a) = \llbracket \tau \rrbracket(\sigma)(a) $$

*Example 3.1.16.* Writing π for any total execution of the program P<sub>*a*</sub>;(P<sub>*a*</sub>||V<sub>*b*</sub>), with *a* ≠ *b*, we have [[π]](*a*) = 2, [[π]](*b*) = -1 and [[π]](*c*) = 0 for *c* ≠ *a* and *c* ≠ *b*. Thus, P<sub>*a*</sub>;(P<sub>*a*</sub>||V<sub>*b*</sub>) is not conservative.

**Definition 3.1.17.** The *consumption* of a program *P* is the partial function Δ(*P*) : 𝒜 → ℤ defined by induction on *P* by

$$ \Delta(P_a) = \delta_a $$

$$ \Delta(V_a) = -\delta_a $$

$$ \Delta(A) = \underline{0} $$

$$ \Delta(P;Q) = \Delta(P \parallel Q) = \Delta(P) + \Delta(Q) $$

$$ \Delta(P+Q) = \Delta(P) \quad \text{if } \Delta(P) = \Delta(Q) $$

$$ \Delta(P^*) = \underline{0} \quad \text{if } \Delta(P) = \underline{0} $$

where $\underline{0}$ is the constant function equal to 0 and $\delta_a$ the indicator function of *a*.

**Proposition 3.1.18.** *The function Δ is only partially defined on programs. A program *P* is conservative if and only if Δ(*P*) is well-defined.*

*Proof.* See [43, Proposition 3.4]. □

<figure><img src="image_117.png" /></figure>

As in Section 1.2.3, the consumption of any path is only defined by its endpoints. Thus, we can define the *consumption* of mutexes directly on positions. Furthermore, for a program **NPIMP**, consumption and evaluation of a path are the same thing, as the states only contains information about the resources.

**Definition 3.1.19.** Given a conservative program *P* and a position *p* in *P*(*P*), we define the *consumption* of *p*, written [[*p*]]: 𝒜 → ℤ as follows:

$$ \llbracket p \rrbracket = \llbracket \pi \rrbracket(\sigma_0) $$

for some path π: ⊥<sub>*P*</sub> → *p* and σ<sub>0</sub> the initial state of *P* from Definition 3.1.2

The above definition is always well-defined as the consumption of a path in conservative program only depends on the endpoints and furthermore, such a path always exists π: ⊥<sub>*P*</sub> → *p*. This second point will be proven later on in Corollary 3.1.26.

**Definition 3.1.20.** We say that a position *p* is *valid* when for all resources *a* ∈ 𝒜, 0 ≤ [[*p*]] < κ<sub>*a*</sub>. We say that an execution π = (*p*<sub>*i*</sub> → *p*<sub>*i*+1</sub>)<sub>*i*∈I</sub> is *valid* when all positions *p*<sub>*i*</sub> are valid.

A valid execution is namely compatible with the expected semantics of resources in the sense that

* no resource is taken more than its capacity κ<sub>*a*</sub> (without having been released in between),
• no resource is released without having been taken first.

**Definition 3.1.21.** Given a program *P*, the *authorized region* is defined as the set of all valid position. Its complement is called the *forbidden region* and any position in the forbidden region is said to be *forbidden*.

The authorized region corresponds to the pruned state space of Section 1.3, but in our case we prefer not pruning the state formally, instead we designate the position as forbidden and try to find which “cubes” intersect or not the forbidden region. This choice is important to define a tractable definition of intervals/cubes on our state space.

Finally, we define $\llbracket - \rrbracket_C$, by the consumption of any path $\pi: \bot \to^* \top$, or alternatively simply by the consumption of $\top$.

**Definition 3.1.22.** Given a program *P* in **NPIMP**, its *evaluation* $\llbracket P \rrbracket_C: \Sigma \to \Sigma$ is defined as follows:

$$ \llbracket P \rrbracket_C(\sigma) = \llbracket \top \rrbracket + \sigma $$

When considering execution traces, this reduces to

$$ \llbracket P \rrbracket_C(\sigma_0) = \llbracket \top \rrbracket $$

It is easy to check that $\llbracket \mathbb{P}_a \rrbracket_C = \llbracket \mathbb{P}_a \rrbracket_\mathcal{X}$, and $\llbracket \mathbb{V}_a \rrbracket_C = \llbracket \mathbb{V}_a \rrbracket_\mathcal{X}$.

### 3.1.2 A partial order on positions

In this section we will show that the reduction relation $\to$ from Definition 3.1.9 induces a partial order on the set of positions (i.e. the state space) that is much more tractable for computations and proofs. This will allow us to define the syntactic semantics of our programs as simple posets. In this model, the partial order plays an analogous role to the notion of direction in the geometric semantics of Section 1.3.

**Definition 3.1.23.** We write $\le$ for the smallest reflexive relation on the positions of *P* such that

$$ \frac{P \neq Q \parallel R}{\bot \leq p} \qquad \frac{p \leq p' \qquad q \leq q'}{p; q \leq p'; q'} \qquad \frac{p \leq p' \qquad q \leq q'}{p \parallel q \leq p' \parallel q'} \qquad \frac{p \leq p'}{p^n \leq p'^n} \\ \frac{P \neq Q \parallel R}{p \leq \top} \qquad \frac{p \leq p'}{p+\emptyset \leq p'+\emptyset} \qquad \frac{q \leq q'}{\emptyset+q \leq \emptyset+q'} \qquad \frac{p^m \leq p'^m}{p^m \leq p'^n} $$

for $m < n$.

**Proposition 3.1.24.** Given a program *P* and a position *p* of *P*, we have $\bot \le p$ (resp. $p \le \top$)

*Proof.* Given a program *P* and a position *p* of *P*, let us prove that $\bot \le p$ by induction on the program *P*.

• $P = Q \parallel R$. Then $\bot = \bot \parallel \bot$ (Definition 3.1.7). And by Definition 3.1.7, $p = q \parallel r$ with $Q \models q$, $R \models r$. By induction hypothesis, $\bot \le q$ and $\bot \le r$. Thus, by the inference rules of Definition 3.1.23, we have

$$ \frac{\bot \le q \qquad \bot \le r}{\bot \parallel \bot \le q \parallel r} $$

Thus $\bot = \bot \parallel \bot \le q \parallel r = p$.
• Otherwise, the property is immediate by the rule $\frac{P \neq Q \| R}{\perp \leq p}$ from Definition 3.1.23.

The property $p \leq \top$ is proved in the same way. □

**Proposition 3.1.25.** *Given two positions p and p' of P, we have $p \leq p'$ if and only if $p \to^* p'$.*

*Proof.* We prove by induction on the program P that, given positions p and p' of P, having the relation $p \leq p'$ is equivalent to having reductions $p \to^* p'$. Let us proceed by induction on P.

• A. Trivial.

• $Q \| R$. Then $p = q \| r$ and $p' = q' \| r'$ for some $q, q' \in \mathcal{P}(Q)$ and $r, r' \in \mathcal{P}(R)$. By the inference rules of Definition 3.1.23, we have that $p \| q \leq q' \| r'$ is equivalent to both $q \leq q'$ and $r \leq r'$ which, by induction hypothesis, is equivalent to $q \to^* q'$ and $r \to^* r'$ which, by the rules

$$ \frac{Q \models q \rightarrow q' \qquad R \models r}{Q \models R \models q \parallel r \rightarrow q' \parallel r} $$

$$ \frac{Q \models q' \qquad R \models r \rightarrow r'}{Q \models R \models q' \parallel r \rightarrow q' \parallel r'} $$

is equivalent to $q \parallel r \to^* q' \parallel r'$.

For the rest of the cases, we suppose that $p$ and $p'$ are both distinct from $\perp$ and $\top$ below (these cases are easily handled separately).

• $Q+R$. Then $p = q+r$ and $p' = q'+r'$ for some $q, q' \in \mathcal{P}(Q) \cup \{\emptyset\}$ and $r, r' \in \mathcal{P}(R) \cup \{\emptyset\}$. We have $q+r \leq r'+r'$ if and only if

- $q \leq q'$ and $r = r' = \emptyset$, or

- $r \leq r'$ and $q = q' = \emptyset$.

Both are treated the same way, so let us suppose $q \leq q'$ and $r = r' = \emptyset$. By induction hypothesis, we have that $q \leq q'$ is equivalent to $q \to^* q'$ and thus to $q+\emptyset \to^* q'+\emptyset$ by the rule

$$ \frac{Q \models q \rightarrow q'}{Q+R \models q+\emptyset \rightarrow q'+\emptyset} $$

• $Q;R$. We separate the three following cases:

- $p = q;\perp$ and $p' = q';\perp$. Then $q;\perp \leq q';\perp$ is equivalent, by the inference rules of Definition 3.1.23, to $q \leq q'$. By induction hypothesis, this is equivalent to $Q \models q \rightarrow q'$. By the inference rule

$$ \frac{Q \models q \rightarrow q'}{Q;R \models q;\perp \rightarrow q';\perp} $$

This is equivalent to $Q;R \models q;\perp \rightarrow q';\perp$.

- $p = \top; r$ and $p' = \top; r'$. Similar to the case above.
- $p = q; \bot$ and $p' = \top; r'$. By definition $q \le \top$ and $\bot \le r'$. Hence, $p \le p'$ by inference rules. By induction hypothesis $Q \models q \le \top$ and $R \models \bot \le r'$ is equivalent to $q \to^* \top$ and $\bot \to^* r'$ which, by the rules

$$ \frac{Q \models q \to \top}{Q; R \models q; \bot \to \top; \bot} \qquad \frac{R \models \bot \to r'}{Q; R \models \top; \bot \to \top; r'} $$

implies, by concatenation, $Q; R \models p \to p'$.

* $P = Q^*$. Then $p = q^n$ and $p' = q'^m$ for some $q, q' \in \mathcal{P}(Q)$ and $n, n' \in \mathbb{N}$.

- If $n = m$, we have by the inference rules of Definition 3.1.23, that $q^n \le q'^n$ is equivalent to $q \le q'$ which, by induction hypothesis, is equivalent to $q \to^* q'$ which, by the rule

$$ \frac{Q \models q \to q'}{Q^* \models q^n \to q'^n} $$

is equivalent to $q^n \to^* q'^n$.

- If $n < m$, by the inference rules, $q \le \top$ equivalent to $q^k \to^* \top^k$ and $\bot \le q'$ equivalent to $\bot^k \to^* q'^k$. Thus, by concatenation of the following paths :

$$ \frac{Q \models q' \to^* \top}{Q^* \models q^n \to^* \top^n} $$

, with for $n \le k < m$

$$ \frac{Q \models \bot \to^* \top}{Q^* \models \bot^k \to^* \top^k} \qquad \frac{}{Q^* \models \top^k \to^* \bot^{k+1}} $$

and finally the path

$$ \frac{Q \models \bot \to^* q'}{Q^* \models \bot^m \to^* q'^m} $$

gives the equivalence.

By taking $p = p'$ we get the Corollary 3.1.26. The case where $p$ or $p'$ equals $\top$ or $\bot$ can also be deduced this way. $\square$

**Corollary 3.1.26.** *Given a program $P$, every position $p$ of $P$ is reachable for the relation $\to^*$.*

*Proof.* By Proposition 3.1.24, we have $\bot \le p$ for any position $p$ of $P$. Thus, by Proposition 3.1.25 we have the proposition. $\square$

**Proposition 3.1.27.** *The relation $\le$ is a partial order on the set $\mathcal{P}(P)$ of positions of $P$.*

*Proof.* The reflexivity and transitivity of $\le$ follows, by Proposition 3.1.25, from the relexivity and transitivity of $\to^*$, which are satisfied by definition.

Let us show the antisymmetry of $\le$. Given positions $p$ and $p'$ of $P$ such that both $p \le p'$ and $p' \le p$ hold. The case where $P \ne Q \parallel R$ and $p$ or $p'$ is either $\bot$ or $\top$ is immediate by definition of the order. For other cases, we reason by induction on $P$.
• A. By definition, $A \models p$ implies that $p$ is either $\perp$ or $\top$ and this case is handled above.

• $R;Q$. The two positions are of the form $r;q$ and $r';q'$ such that, $r;q \le r';q' \le r;q$. By inference rules we have $r \le r' \le r$ and $q \le q' \le q$ which gives by induction, $r=r'$ and $q=q'$.

• $R+Q$. Then as $p,p'$ are comparable, this implies that the two positions are of the form $r+\emptyset$ and $r'+\emptyset$ or $\emptyset+q$ and $\emptyset+q'$. Let us suppose that we are in the former case (the latter being treated dually), such that, $r+\emptyset \le r'+\emptyset \le r+\emptyset$. By inference rules we have $r \le r' \le r$ which gives by induction, $r=r'$.

• $R \parallel Q$. The two positions are of the form $r \parallel q$ and $r' \parallel q'$ such that, $r \parallel q \le r' \parallel q' \le r \parallel q$. By inference rules we have $r \le r' \le r$ and $q \le q' \le q$ which gives by induction, $r=r'$ and $q=q'$.

• $Q^*$. The positions are of the form $r^n$ and $q^m$ such that, $r^m \le q^m \le r^m$. By inference rules we have $n \le m \le n$. Thus, $m=n$ and $r \le q \le r$ by inference rules, which implies, by induction hypothesis $r=q$. $\square$

Thus, we can define the syntactic semantics as the set of positions, equipped with the partial order $\le$ on positions. By Proposition 4.1.33, two states are comparable, if there is an execution from one to the other.

**Definition 3.1.28.** The syntactic semantics associated to a program $P$ is the partially ordered set $(\mathcal{P}(P), \le_P)$ associated with a subset $\mathcal{P}_F$ of its forbidden positions (as in Definition 3.1.21).

*Example 3.1.29.* Let us revisit the program $P = P_a; V_a \parallel P_a; V_a$ from Example 1.4.3. Its syntactic semantics is given below, with arrows indicating comparability. The central point, whose associated transitions have been dotted corresponds to a “forbidden position” of the program (one where the resource *a* has been taken more than its capacity). Contrary to previous models, we do not prune these positions from the semantics.

<figure><img src="image_118.png" /></figure>

### 3.1.3 Syntactic semantics properties

The posets of positions of programs naturally exhibits some interesting properties. First of all incomparable elements are only generated by conditional branchings or parallelization
of processes. As there is a finite amount of those, this means that every antichain of our syntactic semantics is finite. Furthermore, from any state/position of our programs, there can only have been a finite number of steps to reach this position, i.e. our semantics is well-founded. These properties combined imply that we are dealing with a special class of partial orders called well-orders [33]. These properties will be useful later on, when we will prove that our syntactic equivalent of cubical covers form a boolean algebra in Theorem 3.2.38.

**Definition 3.1.30.** Let $(X, \leq)$ a partially ordered set. We say that $X$ is a *well-order* when one of the following equivalent properties hold

* for every infinite sequence $(x_i)_{i \in \mathbb{N}}$ of elements of $X$, there are indices $i < j$ such that $x_i \leq x_j$.

* $X$ is well-founded and every antichain is finite.

* Every decreasing sequence $(x_i)_{i \in \mathbb{N}}$ of elements of $X$ is stationary after a certain rank and every set of pairwise incomparable element is finite.

*Proof.* See [33, Basic Definitions and Tree Theorem] □

<figure><img src="image_119.png" /></figure>

**Proposition 3.1.31.** The poset $\mathcal{P}(P)$ is a well-order.

*Proof.* The proof proceeds by induction on $P$. The inductive cases are easily deduced from the fact that well-orders are closed under finite products, finite co-products and contain $(\mathbb{N}, \leq)$. A proof of this can be found in [48, Section 1.1.3].

Then, given a program $P$, we define

$$ \mathcal{P}(P)^+ = \begin{cases} \mathcal{P}(P) & \text{if } P \text{ of the form } Q \parallel R \\ \mathcal{P}(P) \setminus \{\perp, \top\} & \text{otherwise} \end{cases} $$

It is much easier to reason inductively on this set of positions, so we will first prove

$\mathcal{P}(P)$ is a well-order if and only if $\mathcal{P}(P)^+ $ is a well-order

Indeed both well-foundedness and finitude of antichains of these sets are equivalent:

* Given a decreasing sequence $(p_n)_{n \in \mathbb{N}} \in \mathcal{P}(P)^{\mathbb{N}}$. If there exists $m \in \mathbb{N}$ such that $p_m = \perp$ or for each $n \in \mathbb{N}, p_n = \top$, the sequence is trivially stationary after rank $m$.

* Given an antichain $A \in \mathcal{P}(P)^I$ indexed by some set $I$, we have that $|A| < \infty$ is equivalent to $|A \cap \mathcal{P}(P)^+| < \infty$.

By induction on the program $P$, we show that $\mathcal{P}(P)^+$ is a well-order.

* $P = A$. Since $\mathcal{P}(P) = \{\perp, \top\}$ is finite, it is a well-order.

* For all following cases:
- $P = R \parallel Q$. Using the inference rules

$$ \frac{P \vdash p \qquad Q \vdash q}{P \parallel Q \vdash p \parallel q} \qquad \frac{p \le p' \qquad q \le q'}{p \parallel q \le p' \parallel q'} $$

we have $\mathcal{P}(P)^+ = \mathcal{P}(P) = \mathcal{P}(R) \parallel \mathcal{P}(Q)$ equivalent to $\mathcal{P}(R) \times \mathcal{P}(Q)$ with the product order.

- $P = R+Q$. Using the inference rules

$$ \frac{P \vdash p \qquad Q \vdash q \qquad p \le p'}{P+Q \vdash p+\emptyset \qquad P+Q \vdash \emptyset+q \qquad p+\emptyset \le p'+\emptyset \qquad \emptyset+q \le \emptyset+q'} $$

we have $\mathcal{P}(P)^+ = \mathcal{P}(R)+\emptyset \cup \emptyset+\mathcal{P}(Q)$ equivalent to $\mathcal{P}(R) \sqcup \mathcal{P}(Q)$ with the canonical disjoint order.

- $P = R;Q$. Using the inference rules

$$ \frac{P \vdash p \qquad Q \vdash q \qquad p \le p' \qquad q \le q'}{P;Q \vdash p;\bot \qquad P;Q \vdash \top;q \qquad p;q \le p';q'} $$

we have $\mathcal{P}(P)^+ = (\mathcal{P}(R);\bot) \setminus \{\top;\bot\} \cup \top; \mathcal{P}(Q)$ is equivalent to $(\{0\} \times \mathcal{P}(R) \setminus \top) \cup (\{1\} \times \mathcal{P}(Q))$ equipped with the lexicographic order.

- $P = R^*$. Using the inference rules

$$ \frac{P \vdash p \qquad p \le p' \qquad m < n}{P^* \vdash p^n \qquad p^n \le p'^n \qquad p^m \le p'^m} $$

By the inference rules, $\mathcal{P}(P)^+ = \{r^n \mid r \in \mathcal{P}(R), n \in \mathbb{N}\}$ is equivalent to $\mathbb{N} \times \mathcal{P}(R)$ equipped with the lexicographic order.

The posets $\mathcal{P}(R)$ and $\mathcal{P}(Q)$ are well-orders by induction hypothesis, $\{0,1\}$ and $\mathbb{N}$ as well, and well-orders are closed by all the above operations [48, Section 1.1.3, 1.1..4].

Thus, $\mathcal{P}(P)^+$ is a well order. $\square$

**Proposition 3.1.32.** The partial order $\le$ on $\mathcal{P}(P)$ is a bounded lattice, with $\bot$ and $\top$ as smallest and largest elements, with supremum being determined by

$$ \begin{array}{l@{\qquad}l@{\qquad}l} (p;q) \lor (p';q') = (p \lor p'); (q \lor q') & p^n \lor p'^n = (p \lor p')^n & (p+\emptyset) \lor (p'+\emptyset) = (p \lor p')+\emptyset \\ (p \parallel q) \lor (p' \parallel q') = (p \lor p') \parallel (q \lor q') & p^m \lor p'^m = p'^m & (\emptyset+q) \lor (\emptyset+q') = \emptyset+(q \lor q') \\ & & (p+\emptyset) \lor (\emptyset+q) = \top \end{array} $$

for $m < n$. The infimum admits a similar description.

*Proof.* Given a program $P$, let us prove that for any two positions $P \vdash p_1, p_2$, $p_1 \lor p_2$ corresponds to the supremum $\sup(p_1, p_2)$ of $p_1$ and $p_2$ in the classical sense, i.e. $\sup(p_1, p_2) = \min\{p \in \mathcal{P}(P) \mid p \ge p_1, p \ge p_2\}$.

We first remark that by Proposition 3.1.24, $\top \lor p = \top$ and $\bot \lor p = p$ corresponds to the supremum of the positions. We will thus suppose both $p_1$ and $p_2$ distinct from $\bot$ and $\top$ when $P$ is not of the form $Q \parallel R$ and prove the property by induction on the program $P$. We remind that we differentiate the case $P = Q \parallel R$ because in this case $\bot = \bot \parallel \bot$ and removing it would complicate the argument.
• $R = A$. Trivial.

• $P = Q; R$. The positions are of the form $p_1 = q_1; r_1$ and $p_2 = q_2; r_2$. By induction hypothesis, for $i = 1, 2$, we have

$$q_1 \lor q_2 \geq q_i \text{ and } r_1 \lor r_2 \geq r_i$$

and for every position $q; r$ of $P$ such that $q; r \geq p_i$ for $i = 1, 2$, we have

$$q \geq q_1 \lor q_2 \text{ and } r \geq r_1 \lor r_2$$

By the inference rules, we therefore have $q; r \geq (q_1 \lor q_2); (r_1 \lor r_2) \geq q_i; r_i$, which proves

$$\sup(p_1, p_2) = (q_1; r_1) \lor (q_2; r_2) = (q_1 \lor q_2); (r_1 \lor r_2) = p_1 \lor p_2$$

We still need to prove that $P \models (q_1 \lor q_2); (r_1 \lor r_2)$. By inference rules, this is equivalent to $q_1 \lor q_2 = \top$ or $r_1 \lor r_2 = \bot$.

- If $q_1 = \top$ or $q_2 = \top$, by the inference rules, this implies $q_1 \lor q_2 = \top$.

- Otherwise, $q_1 \neq \top$ and $q_2 \neq \top$. Thus, $P \models p_1$ and $P \models p_2$ implies $r_1 = \bot = r_2$. Thus, $r_1 \lor r_2 = \bot$.

Thus, $P \models (q_1 \lor q_2); (r_1 \lor r_2)$.

• $P = Q \parallel R$. Similar to the case above.

• $P = Q+R$. We have $p_1 = q_1+r_1$ and $p_2 = q_2+r_2$

- Suppose that $r_1 = r_2 = \emptyset$. By the inference rules, positions of $P$ greater than $p_i$ are $p = q+\emptyset$ with $q$ greater than $q_i$ or $p = \top$ (not the supremum since $\top+\emptyset$ is a smaller upper bound). Thus, similarly as above, the inference rules imply

$$\sup(p_1, p_2) = (q_1 \lor q_2)+\emptyset = (q_1+\emptyset) \lor (q_2+\emptyset)$$

- The case where $q_1 = q_2 = \emptyset$ is similar.

- Otherwise, $p_1 = q_1+\emptyset, p_2 = \emptyset+r_2$. By inference rules, $p \geq p_i$ for $i = 1, 2$ implies $p = \top$. Thus,

$$\sup(p_1, p_2) = \top = p_1 \lor p_2$$

• $P = Q^*$. We have $p_1 = q_1^{n_1}$ and $p_2 = q_2^{n_2}$.

- If $n_1 > n_2$, then $p_1 > p_2$. Thus, $\sup(p_1, p_2) = p_1 = p_1 \lor p_2$. The case $n_2 > n_1$ is symmetric.

- Otherwise, suppose $n_1 = n_2 = n$. By induction, $q \geq q_i$ for $i = 1, 2$ implies $q \geq q_1 \lor q_2$ and thus by inference rules, $q^n \geq (q_1 \lor q_2)^n$. And by definition of the supremum, the inference rules imply $(q_1 \lor q_2)^n \geq q_i^n$. Thus

$$(q_1 \lor q_2)^n = \sup(q_1^{n_1}, q_2^{n_2}) \quad \square$$
## 3.2 The boolean algebra of syntactic regions

### 3.2.1 Cubes and regions of posets

In this section we define our representation of the state-space of programs, replacing (maximal) cubical covers in geometric semantics of Section 1.4.1 by (normal) *syntactic covers*. Instead of considering cubes between pairs of points, we consider cubes between syntactic positions. This makes implementation easier, as we can rely on the inductive nature of their definition for the different operators (intersection, complement, ...).

We show that, under mild assumptions, these regions satisfy the same fundamental properties as cubical covers (forming a boolean algebra, supporting the existence of canonical representatives, etc.) and provide explicit ways of computing corresponding canonical operations on syntactic covers.

#### 3.2.1.1 Intervals

We will replace the *n*-cubes of the directed topological models by a notion of cube on partially ordered sets, simply defined as pairs of points in our posets which represents/covers the set of points in between them.

**Definition 3.2.1.** Let $(X, \leq)$ a poset. A *cube* $(x, y)$ in this poset is a pair of elements such that $x \leq y$. We denote by $C(X)$, the set of all cubes of $X$.

To differentiate the cube as an object and as the set of point it represents, in the same way we separate cubical regions and cubical covers in Section 1.4.1, we introduce the *support* operator, which associate to a cube the associated region.

**Definition 3.2.2.** Let $(X, \leq)$ a poset. Let $I = (x, y) \in C(X)$. We write $[I] = [x, y] = \{z \in X | x \leq z \leq y\}$ for the set of points it contains, also called its *support*.

When considering, $\vec{I}^n$ with the standard product order, then the set $[x_1 \times \dots \times x_n, y_1 \times \dots \times y_n]$ corresponds to the region $\prod_{i=1}^n [x_i, y_i]$. The associated cube corresponds to the associated *n*-cube.

**Definition 3.2.3.** Given a poset $\mathcal{P}$, we call (syntactic) *region* of $\mathcal{P}$ any subset $X \subseteq \mathcal{P}$

There is a natural ordering on cubes based on the inclusion order of the set of points they represent.

**Definition 3.2.4.** Let $(X, \leq)$ a poset. Let $I, J \in C(X)$. We define the partial order relation $\subseteq$ on cubes as follows:

$$I \subseteq J \text{ if and only if } [I] \subseteq [J]$$

*Remark 3.2.5.* We write $z \in I$ instead of $z \in [I]$; we have $z \in (x, y)$ if and only if $x \leq z \leq y$.

#### 3.2.1.2 Syntactic covers

Now the syntactic equivalent of cubical covers (resp. cubical regions) is naturally defined as the syntactic cubical covers (resp. their support).
**Definition 3.2.6.** A syntactic (cubical) cover $R$ of a poset $X$ is a set of cubes of $X$. A cover is finite, when it contains a finite number of cubes. We write $\mathcal{R}(X) = \mathfrak{P}(X \times X)$ for the set of covers of $X$, where $\mathfrak{P}(-)$ denotes the power set of a given set.

**Definition 3.2.7.** The support of a cover $R$ is the set $[R]$ defined as follows:

$$[R] = \bigcup_{I \in R} [I]$$

Two covers are equivalent when they have the same support.

Equivalent covers are the syntactic equivalent of cubical covers of the same cubical regions. Such covers are different ways of describing the same underlying set of points of the state space. Just as there exists a maximal cubical cover, we should be able to exhibit a “most compact” representation of a region in its equivalence class.

We recall that for a syntactic cube, its maximal cubical cover is given by the set of all maximal cubes $C_n^{\max}(Y)$ included in the cubical region $Y$ (Proposition 1.4.11). Intuitively, the “best” syntactic cover with a given support $Y \subseteq X$ will then consist of all the maximal cubes (w.r.t. $\subseteq$) contained in $Y$. We will call this region the normal form for a cover $R$ and say that a cover is in normal form when it is equal to its own normal form.

In order to formalize this, we re-introduce the (pre)order relation on $n$-cubes from Definition 1.4.8 and Definition 1.4.10.

**Definition 3.2.8.** Let $R$ and $S$ be two covers of $X$. The relation $\preceq$ defined as follows is a pre-order on $\mathcal{R}(X)$

$$R \preceq S \iff \forall R^i \in R, \exists S^j \in S, R^i \subseteq S^j$$

*Example 3.2.9.* Let us consider the program $P_1; P_2 \parallel P_1; P_2$. The set of its positions $\mathcal{P}(P)$ is represented below. On the left, we consider the region $X \subseteq \mathcal{P}(P)$ in grey, and various maximal cubes on this region.

<figure><img src="image_120.png" /></figure>
<figure><img src="image_121.png" /></figure>

<figure><img src="image_122.png" /></figure>

With

$$R^1 = (\top; \bot, \top; \top) \times (\bot; \bot, \top; \bot)$$

$$R^3 = (\top; \bot, \top; \bot) \times (\bot; \bot, \top; \top)$$

$$R^2 = (\bot; \bot, \top; \top) \times (\top; \bot, \top; \top)$$

$$R^4 = (\bot; \bot, \top; \top) \times (\top; \bot, \top; \bot)$$

Both $R = \{R^1, R^2, R^3, R^4\}$ and $S = \{R^1, R^2\}$ are covers of $X$, but $S \leq R$, as we consider that $R$ carries more information about the region, as it has more of the maximal cubes included in $X$

*Example 3.2.10.* Given a program $P = P_1+P_2$, let us consider the region $X = \mathcal{P}(P)$ as well as the three following covers of support $X$:

<figure><img src="image_123.png" /></figure>

$$R_1 = \{(\bot, \top+\emptyset), (\emptyset+\bot, \top)\}$$

<figure><img src="image_124.png" /></figure>

$$R_2 = \{(\bot, \top)\}$$

<figure><img src="image_125.png" /></figure>

$$R_3 = \{(\bot, \top), (\top+\emptyset, \top)\}$$

We have $R_1 \prec R_2$ and $R_3 \preceq R_2$, as well as $R_2 \preceq R_3$.

**Lemma 3.2.11.** The support function $[-] : \mathcal{R}(X) \to \mathfrak{P}(X)$ is increasing if we equip the first with $\preceq$ and second with $\subseteq$ as partial orders.

*Proof.* Given $R, S \in \mathcal{R}(X)$, such that $R \preceq S$. For every $I \in R$ there exists $J_I \in S$ such that $I \subseteq J_I$, i.e. $[I] \subseteq [J_I]$. Then

$$[R] = \bigcup_{I \in R} [I] \subseteq \bigcup_{I \in R} [J_I] \subseteq \bigcup_{J \in S} [J] = [S] \quad \square$$

Furthermore

**Lemma 3.2.12.** The functions $[-] : \mathcal{R}(X) \to \mathfrak{P}(X)$ and $\mathcal{C} : \mathfrak{P}(X) \to \mathcal{R}(X)$ which associate to a region the set of all of its cubes are increasing and $[-]$ is left adjoint to $\mathcal{C}$. They form a Galois connection between the regions of $X$ and the covers of $X$ if we equip the first with $\subseteq$ and second with $\preceq$ as partial orders.

*Proof.* We will prove the existence of an adjunction of posets (called a Galois connection) with $[-]$ the left adjoint to $\mathcal{C}$. First, we prove that both functions are increasing
• [–] is increasing by Lemma 3.2.11.

• Given $P, Q \in \mathfrak{P}(X)$ such that $P \subseteq Q$, we have that $(x, y) \in \mathcal{C}(P)$ is equivalent to $[x, y] \subseteq P \subseteq Q$ and thus $(x, y) \in \mathcal{C}(Q)$, which proves $\mathcal{C}(P) \subseteq \mathcal{C}(Q)$.

And by definition $R \in \mathcal{R}(X)$, such that $[R] \subseteq P$ is equivalent to $R \subseteq \mathcal{C}(P)$. This is explicitly the definition of a Galois connection. □

In Example 3.2.10, the cover $R_2$ is clearly the most parsimonious way to represent the whole space, in the sense explained above, and is a maximal element with respect to the order. However, as we already explained in Section 1.4.2, there are many other maximal elements such as $R_3$ (or, in fact, any other cover obtained by adding cubes to $R_2$: the relation $\leq$ is not antisymmetric). This motivates the introduction of the following refined order on covers, which is such that $R_1 < R_3 < R_2$:

**Definition 3.2.13.** We can define a partial order $\leq$ on the covers of a partial order $X$ from the preorder $\leq$ as follows. Given $R, S$ two covers:

$$R \leq S \iff R \leq S \text{ and } S \leq R \text{ implies } S \subseteq R$$

When $R \leq S$ and $R$ and $S$ are equivalent, we think of $S$ as being a “more economical way” of describing the same support, because it uses bigger cubes: every cube of $R$ is contained in one of $S$.

**Lemma 3.2.14.** The relation $\leq$ is a partial order.

*Proof.* Consider $R, S, T \in \mathcal{R}(X)$ such that $R \leq S \leq T$.

• Reflexivity. By reflexivity of $\leq$ and $\subseteq$.

• Transitivity. Suppose $R \leq S$ and $S \leq T$. Thus, $R \leq S \leq T$, i.e. by transitivity of $\leq$,

$$R \leq T$$

Now suppose $T \leq R$, then by transitivity $S \leq R$ (resp. $T \leq S$). By definition, $R \leq S$ (resp. $S \leq T$) implies $R \subseteq S$ (resp. $S \subseteq T$). Thus, by transitivity of $\subseteq$,

$$T \leq R \text{ implies } R \subseteq T$$

• Antisymmetry. Suppose $R \leq S$ and $S \leq R$. This implies $R \leq S \leq R$. By definition of $\leq$, $R \leq S \leq R$ thus implies $R \subseteq S \subseteq R$. Hence, $R = S$. □

### 3.2.1.3 Normal form of regions

As in Section 1.4.2, we expect the “best description” of a subset of $X$ by a cover to be given by a right adjoint $N: (\mathfrak{P}(X), \subseteq) \to (\mathcal{R}(X), \leq)$ to the support function $[-]$, with $N$ associating to a subset $Y$ of $X$ the normal cover describing it. We already have an adjoint when $\mathcal{R}(X)$ is equipped with $\leq$, but as explained before, this is not enough to define a good description.

The special adjoint functor theorem [38, V.8, Theorem 1] indicates that if such a right adjoint exists it should be defined as a particular limit as explained in Proposition 3.2.15 below:
In the general case, for a partial order $X$, it is not easy to characterize exactly the supports $Y \subseteq X$ that admit a normal form $N(Y)$. Thankfully, as we will be considering state spaces of programs and not any posets, we can impose further restrictions. First, we have seen that the syntactic semantics of a program is a well order Proposition 3.1.31. Sadly, as shown in Example 3.2.17 this is not enough to ensure that all supports will have a normal form. What we do know is that, usually getting a cover of the forbidden region of a program is much easier than getting a cover of the authorized region directly. In Section 1.4.2, and especially for the Algorithm 1.4.33, the authorized region is computed (in normal form) as the complement of the forbidden region, which is naturally obtained in normal form. This suggests that the correct supports to be considering are the subsets $Y \subseteq X$ that admit a normal form and whose complement $Y^c = X \setminus Y$ also admits a normal form. Formally:

**Definition 3.2.19.** Suppose given a partial order $X$. We define the set $\mathcal{N}(X)$ of normal supports as follows:

$$ \mathcal{N}(X) = \{Y \subseteq X \mid \text{both } N(Y) \text{ and } N(Y^c) \text{ exists and are finite}\} $$

Thankfully, regions of $\mathcal{N}(X)$ are much easier to work with. Indeed, we will prove in Proposition 3.2.37 that, given suitable restrictions on $X$, these supports can be characterized as supports of a cover where all cubes admit a normalizable complement. This helps a lot as it is easy to determine if a cube admits such a complement Proposition 3.2.26. Furthermore, we will show that under reasonable assumptions the set $\mathcal{N}(X)$ forms a boolean algebra, similarly to the cubical covers of Section 1.4.

*Remark 3.2.20.* Later, in Proposition 3.3.2, we will give criterion to determine which supports are normal supports.

### 3.2.2 Finitely complemented regions

As explained before, for our practical applications, given a cover $R$ in $\mathcal{R}(X)$, we need to be able to compute a cover $\bar{R}$ which covers the complement of the cover, i.e. a cover $\bar{R}$ such that $[\bar{R}] = [R]$. Moreover, in Section 1.4.2, we are able to compute the normal form of the complement, even when the cover is not in normal form. This suggests that for a cover of an element of $\mathcal{N}(X)$, we can compute their normal form $N([R])$ as the bi-orthogonal construction $\bar{\bar{R}}$.

In order to do this, we will first prove that we can define intersection and union operators for cover with normal supports compatible with the standard operations on the supports and conserving the property of having a normal support. In more specific terms, we will show that – under suitable hypothesis – regions which admit a normal form (and whose complement admit a normal form) have a boolean algebra structure, providing explicit algorithmic constructions for the corresponding operations.

This generalizes the programs that are considered in [18] (which is limited to programs whose geometric semantics are subsets of $\mathbb{R}^n$) and in [30] (which is limited to products of graphs). In order to ensure that our constructions are applicable in practice, we only consider covers which are *finite* in the following (and showing that finiteness is preserved
by our constructions will be non-trivial). In particular, by a “normal form”, we always mean a finite region in normal form.

### 3.2.2.1 The complement of a cube

We begin by remarking that a cover $R = \{I\}$, consisting of single cube, is already in normal form (i.e. $N(R) = R$). Thus, $R \in \mathcal{N}(X)$ if and only if $[I]^c$ has a normal form. Hence, in order to characterize regions of $\mathcal{N}(X)$ we will first begin by investigating the covers corresponding to complements of a single cube.

As an example, let us consider the space $X = [0, 5]^2 \subseteq \mathbb{N}^2$ and $R = \{I\}$ with $I = [(2, 2), (3, 3)]$, as pictured on the left below:

<figure><img src="image_126.png" /></figure>

Then with:

$$ \bot = (0, 0) $$

$$ y_1 = (1, 5) $$

$$ y_2 = (5, 1) $$

$$ \top = (5, 5) $$

$$ x_1 = (0, 4) $$

$$ x_2 = (4, 0) $$

The normal form of the complement $[I]^c$ of $I$ is the cover

$$ \bar{R} = \{[\bot, y_1], [\bot, y_2], [x_1, \top], [x_2, \top]\} $$

Now if we define $I^{lc}$ (resp. $I^{uc}$) is the set of elements of $X$ which are not above $(2, 2)$ (resp. below $(3, 3)$). Then, as shown in the figure below, $[R]^c = I^{lc} \cup I^{uc}$.

<figure><img src="image_127.png" /></figure>

Moreover, the set $I^{lc}$ (resp. $I^{uc}$) corresponds to all the points lower than an element of the finite set $\{y_1, y_2\}$ (resp. $\{x_1, x_2\}$).
We will actually see that the set $I^{\text{lc}}$ (resp. $I^{\text{uc}}$) having a maximal (resp. minimal) antichain is actually the key to the existence of the normal form of the complement, and in that case we even have a description of the normal form (Proposition 3.2.26). First we need to introduce a few definitions before we can formalize this characterization.

**Definition 3.2.21.** Given a set $Y \subseteq X$, its lower closure $\downarrow Y$ and lower complement $Y^{\text{lc}}$ are respectively the sets

$$ \downarrow Y = \{x \in X \mid \exists y \in Y, x \le y\} \qquad Y^{\text{lc}} = (\uparrow Y)^c = \{x \in X \mid \forall y \in Y, x \not\le y\} $$

The *upper closure* $\uparrow Y$ and *upper complement* $Y^{\text{lc}}$ of $Y$ are defined dually:

$$ \uparrow Y = \{x \in X \mid \exists y \in Y, y \le x\} \qquad Y^{\text{uc}} = (\downarrow Y)^c = \{x \in X \mid \forall y \in Y, x \not\le y\} $$

**Definition 3.2.22.** Given a set $Y$ we write:

* $\max Y = \{y \in Y \mid \forall z \in y, z \not\ge y\}$ for the set of maximal elements of $Y$

* $\min Y = \{y \in Y \mid \forall z \in y, z \not\le y\}$ for the set of minimal elements of $Y$

**Definition 3.2.23.** Given a set $Y \subseteq X$ we say that

* $Y$ is *finitely lower generated* when there exists a finite set $Y'$ such that $Y = \downarrow Y'$

* $Y$ is *finitely upper generated* when there exists a finite set $Y'$ such that $Y = \uparrow Y'$

By extension, we say that an element $x$ of $X$ is finitely lower (resp. upper) generated when $\{x\}$ is.

**Lemma 3.2.24.** If $Y$ is finitely lower generated then $\max Y$ is finite and, we have $Y = \downarrow \max Y$.

*Proof.* Given a finitely lower generated poset $(Y, \leq)$. There exists a finite set $X \subseteq Y$ such that $Y = \downarrow X$. We want to prove that, $\max Y = \max X$ and that it is a lower generator of $Y$. By finiteness of $X$, any strictly increasing sequence $(z_i)_{i \in \mathbb{N}} \in X^{\mathbb{N}}$, is finite. This implies

$$ \downarrow \max X = \downarrow X \setminus \{z \in X \mid \exists z' \in X, z < z'\} = \downarrow X = Y $$

Given an element $y \in \max Y \subseteq Y = \downarrow \max X$, there exists $z \in \max X \subseteq Y$ such that $y \le z$. Maximality w.r.t. inclusion of elements of $\max Y$ implies $z = y$. Thus,

$$ \max Y \subseteq \max X $$

Now given an element $z \in \max X$ and $y \in Y$ such that $z < y$. By definition, $\downarrow \max X = Y$ implies the existence of $z' \in \max X$ such that $z < y \le z'$. This contradicts the definition of $\max X$. Thus, for all $y \in Y, z \not\le y$, i.e. $z \in \max Y$. And thus

$$ \max X \subseteq \max Y $$

$$ \text{Thus } \max Y = \max X, \text{ finite and } \downarrow \max Y = \downarrow \max X = \downarrow X = Y \qquad \square $$

**Definition 3.2.25.** Given a set $Y \subseteq X$, We say that $Y$ is
• finitely lower complemented when $Y^{\text{lc}}$ is finitely lower generated i.e. there exists $Y'$ a finite set such that $(\downarrow Y)^c = \downarrow Y'$

• finitely upper complemented when $Y^{\text{uc}}$ is finitely upper generated i.e. there exists $Y'$ a finite set such that $(\uparrow Y)^c = \uparrow Y'$

• finitely complemented when it is both finitely lower and upper complemented.

By extension, we say that an element $x$ of $X$ is finitely lower (resp. upper) complemented when $\{x\}$ is.

From this definition we can characterize the covers $R = \{I\}$ corresponding to a single cube, which are in $\mathcal{N}(X)$. Indeed, such a region $[R]$ is in $\mathcal{N}(X)$ if and only if $[I]$ is finitely complemented.

**Proposition 3.2.26.** Given a lattice $X$, bounded by $\perp$ and $\top$ and $I$ a cube of $X$, the cover $R = \{I\}$ has a complement in normal form if and only if $[I]$ is finitely complemented. In this case, the normal form of its complement is

$$ \overline{R} = \{[\perp, y] \mid y \in \max(I^{\text{lc}})\} \cup \{[x, \top] \mid x \in \min(I^{\text{uc}})\} $$

*Proof.* Suppose given a poset $(X, \leq)$, $I = (s, t)$ a cube of $X$, and consider the cover $R = \{I\}$.

Left-to-right implication. Suppose that $R$ has a complement in normal form, i.e. we have

$$ \overline{[R]} = [N(\overline{[R]})] $$

where $N(\overline{[R]})$ is a finite cover. We have to show that $I$ is finitely complemented, which means that the lower complement satisfies

$$ I^{\text{lc}} = \downarrow \max(I^{\text{lc}}) $$

with $\max(I^{\text{lc}})$ finite, and dually for complement (we only handle the case of the lower complement here, the property for the upper complement being similar). By Lemma 3.2.24 and Definition 3.2.25, it is enough to show that $I^{\text{lc}}$ is finitely lower generated. We show here that it is generated by the set

$$ G = \{x \in X \mid (\perp, x) \in N(\overline{[R]})\} $$

i.e.

$$ I^{\text{lc}} = \downarrow G $$

where $G$ is finite because $N(\overline{[R]})$ is supposed to be finite. We show the equality by showing both inclusions.

• $I^{\text{lc}} \subseteq \downarrow G$. Suppose given $x \in I^{\text{lc}}$. Since $I^{\text{lc}}$ is downward closed, we have $(\perp, x) \in \mathcal{C}(I^{\text{lc}})$. Furthermore, as $I^{\text{lc}} \subseteq \overline{[R]}$ and $\mathcal{C}$ is monotonic, we have

$$ \mathcal{C}(I^{\text{lc}}) \subseteq \mathcal{C}(\overline{[R]}) $$
Now, if $I^{\text{lc}} = \overline{[R]}$, then by definition $C(I^{\text{lc}}) \leq C(\overline{[R]})$. Otherwise, if $I^{\text{lc}} \subset \overline{[R]}$, we have $C(I^{\text{lc}}) \leq C(\overline{[R]})$ and $C(\overline{[R]}) \not\leq C(I^{\text{lc}})$ such that $C(I^{\text{lc}}) \leq C(\overline{[R]})$. Thus, in both cases, we have

$$ 
\begin{array}{l@{\qquad}l}
C(I^{\text{lc}}) \leq C(\overline{[R]}) & \\
\leq C([N(\overline{[R]})]) & \text{by hypothesis} \\
C(I^{\text{lc}}) \leq N(\overline{[R]}) & \text{by Proposition 3.2.15}
\end{array}
$$

This means that $(\perp, x) \subseteq (a, b)$ for some element $(a, b) \in N(\overline{[R]})$. And thus $a = \perp$ and $x \leq b$ with $b \in \downarrow G$.

* $\downarrow G \subseteq I^{\text{lc}}$. Since $I^{\text{lc}}$ is downward closed, it is enough to show $G \subseteq I^{\text{lc}}$. Fix $x \in G$. We have $(\perp, x) \in N(\overline{[R]})$. In order to show $x \in I^{\text{lc}}$, we have to show that $x \not\geq s$. Namely, if $x \geq s$, we would have $[\perp, x] \cap [I] \neq \emptyset$, which contradicts the hypothesis that $(\perp, x) \in N(\overline{[R]})$ and thus $[\perp, x] \subseteq \overline{[R]}$.

Right-to-left implication. Suppose that $[I]$ is finitely complemented, i.e. both $I^{\text{lc}}$ and $I^{\text{uc}}$ are finitely generated. Let us show that the normal form of $\overline{[R]}$ is

$$ \overline{R} = \{[\perp, y] \mid y \in \max(I^{\text{lc}})\} \cup \{[x, \top] \mid x \in \min(I^{\text{uc}})\} $$

We write

$$ S = \{[\perp, y] \mid y \in \max(I^{\text{lc}})\} \qquad T = \{[x, \top] \mid x \in \min(I^{\text{uc}})\} $$

We first remark that

$$ \overline{[R]} = I^{\text{lc}} \cup I^{\text{uc}} = [S] \cup [T] = [S \cup T] $$

Namely, we have, by Lemma 3.2.24 since $I$ supposed to be finitely lower complemented

$$ I^{\text{lc}} = \downarrow \max(I^{\text{lc}}) = [S] $$

and similarly $I^{\text{uc}} = [T]$. Therefore, $\overline{R}$ is a cover whose support is $\overline{[R]}$, and it remains to be shown that the cover $\overline{R}$ is in normal form, i.e. $\overline{R} = N(\overline{R})$. We then proceed by using the definition of $N(\overline{R})$ as a maximum for the covers of $\overline{[R]}$. Given a cover $U$ such that $[U] \subseteq \overline{[R]}$, let us show that $[U] \leq \overline{R}$.

* Let us prove $U \leq \overline{R}$. By Lemma 3.2.12, we have $U \leq C([U]) \leq C(\overline{[R]})$, and it suffices to show that $C(\overline{[R]}) \leq \overline{R}$. We first show that we can express $C(\overline{[R]}) = C(\overline{[I]}) = C([s, t])$ as

$$ C(\overline{[s, t]}) = C(s^{\text{lc}}) \cup C(t^{\text{uc}}) $$

By definition of the complement, we have that $[s, t] = s^{\text{lc}} \cup t^{\text{uc}}$. Therefore,

$$ 
\begin{align*}
C(\overline{[I]}) &= C(I^{\text{lc}} \cup I^{\text{uc}}) \\
C(\overline{[I]}) &= C(I^{\text{lc}}) \cup C(I^{\text{uc}}) \\
&\quad \cup \{(a, b) \mid a \in s^{\text{lc}} \setminus t^{\text{uc}} \text{ and } b \in t^{\text{uc}} \setminus s^{\text{lc}}\} \\
&\quad \cup \{(a, b) \mid a \in t^{\text{uc}} \setminus s^{\text{lc}} \text{ and } b \in s^{\text{lc}} \setminus t^{\text{uc}}\}
\end{align*}
$$
Given $(a, b) \in \{(a, b) | a \in s^{\text{lc}} \setminus t^{\text{uc}} \text{ and } b \in t^{\text{uc}} \setminus s^{\text{lc}}\}$, we have $a \le t, s \le b$, thus $a \vee s \le b \wedge t$, and therefore $[a, b] \cap [s, t] = [a \vee s, b \wedge t] \neq \emptyset$, and thus $(a, b) \notin C([\overline{I}])$. Similarly, we have $\{(a, b) | a \in t^{\text{uc}} \setminus s^{\text{lc}} \text{ and } b \in s^{\text{lc}} \setminus t^{\text{uc}}\} \cap C([\overline{I}]) = \emptyset$, from which we conclude

$$C([\overline{I}]) = C(I^{\text{lc}}) \cup C(I^{\text{uc}})$$

Now we show that $C(I^{\text{lc}}) \preceq S$. Given $(i, j) \in C(I^{\text{lc}})$. By definition of $S$, there exists $y \in \max I^{\text{lc}}$ such that $i \le j \le y$ i.e. $(i, j) \subseteq (\perp, y) \in S$. Thus, $C(I^{\text{lc}}) \preceq S$. Similarly, $C(I^{\text{uc}}) \preceq T$. Thus,

$$C([\overline{R}]) = C(I^{\text{lc}}) \cup C(I^{\text{uc}}) \preceq S \cup T = \overline{R}$$

* If $\overline{R} \preceq U$, this implies $\overline{R} \subseteq U$. We show that under those condition we have $S \subseteq U$. Given $(\perp, x) \in S$, $\overline{R} \preceq U$ trivially implies $S \preceq U$, i.e. there exists $[u, v] \in U, [\perp, x] \subseteq [u, v]$. Immediately, we get $u = \perp$ and $v \in I^{\text{lc}}$ (indeed $v \ge s$ implies $[\overline{I}] \cap I \supseteq \{(\perp, v)\} \cap I \neq \emptyset$). Furthermore, by definition of $S$, for $v \in I^{\text{lc}}$, there exists $y \in \max I^{\text{lc}}$ such that $(\perp, v) \subseteq (\perp, y)$. Finally, $(\perp, y)$ is a cube of $S$, such that

$$S \ni (\perp, x) \subseteq (u, v) = (\perp, v) \subseteq (\perp, y) \in S$$

By definition of $\max I^{\text{lc}}$ this implies $(\perp, x) = (u, v) = (\perp, y)$. Thus,

$$S \subseteq U$$

By the same reasoning we get $T \subseteq U$. Thus, $\overline{R} \preceq U$ implies $\overline{R} \subseteq U$

□

### 3.2.2.2 The complement of a cover

We now explain how to construct the complement of a cover by using the previous complement of a cube. Then, the complement of the cover will be defined as the intersection of all the complements of its cubes. Leveraging the fact that for a single cube, the complement is in normal form, we will also show that the complement of a cover will contain all maximal cubes of its support.

For the rest of this section we will suppose fixed an ambient bounded lattice $X$, in which the construction will be performed. For technical reasons, it will be convenient to suppose that $X$ is also well-ordered, which, by Proposition 3.1.31, is a reasonable restriction for the applications we have in mind. Our aim is now to generalize Proposition 3.2.26, and characterize normalizable covers (as opposed to cubes) which admit a complement in normal form. As we will show in Proposition 3.2.37, under suitable restrictions on $X$, normal supports coincide with the subset of $X$ corresponding to a cover containing only finitely complemented cubes.

**Definition 3.2.27.** Given a poset $X$ and a cover $R$ on $X$. We say that $R$ is finitely complemented if it contains only cubes whose support are finitely complemented in the sense of Definition 3.2.25. We write $R_X$ for the set of finitely complemented covers of $X$, defined as:

$$R_X(X) = \{R \in R(X) | R \text{ is finitely complemented}\}$$

And $\mathcal{F}(X)$ the set whose elements are the supports of covers in $R_X(X)$:

$$\mathcal{F}(X) = \{Y \subseteq X | Y = [\overline{R}] \text{ for some finitely complemented cover } R\}$$
*Remark 3.2.28.* We bring attention to the reader that this does not state that the support of the cover should be finitely complemented.

In order to apply Algorithm 1.4.33, we need to be able to perform the intersection, union and complementation of the cubical covers. In order to efficiently manipulate these intermediary covers, we will need to be able to normalize them, and thus guarantee that they do have a normal form. Thus, we will need to prove that $N(X)$ forms a boolean Algebra. This is not always the case as shown in Example 3.2.29 below.

*Example 3.2.29.* Let us construct an example of a well-ordered, bounded lattice, where $N(X)$ is not a boolean algebra. Consider the space $X$, on the left below, where the arrows indicate comparability w.r.t. the order on $X$, and dotted arrows indicate an infinite countable chain of ordered points. It is easy to show that $X$ verifies the required properties. Now let us consider the cubes $(\perp, s)$ and $(\perp, t)$. As shown on the right below, they are both normal supports i.e. in $N(X)$.

<figure><img src="image_128.png" /></figure>

<figure><img src="image_129.png" /></figure>

<figure><img src="image_130.png" /></figure>

Then, if we consider the intersection $[(\perp, s)] \cap [\overline{(\perp, t)}]$, we see that it is equal to the single point $s$ but, the complement of $(s, t)$ does not have a normal form: Indeed, as in Example 3.2.17 should we consider cubes of the form in the figure on the right below, we can show that there is no maximal element.

<figure><img src="image_131.png" /></figure>

<figure><img src="image_132.png" /></figure>

This implies that $(s, t)$ is not in $N(X)$ and as such $N(X)$ is not a boolean algebra.

The condition which emerged in order to capture such situations is the following one:

**Definition 3.2.30.** A poset $(X, \leq)$ is *finitely complemented* if

1. given a finitely lower complemented element $x \in X$, every element of $\max(\{x\}^{\text{lc}})$ is finitely upper complemented,

2. given a finitely upper complemented element $x \in X$, every element of $\min(\{x\}^{\text{uc}})$ is finitely lower complemented.

*Remark 3.2.31.* In the case where $X$ is a well-order, any upwards closed subset is necessarily finitely upper generated: the set $\min X$ of minimal elements of $X$ generates $X$ because it is well-founded, and is finite because it is an antichain. The first condition is thus always satisfied.

In the next section we will show the following theorem, justifying the restriction we imposed on $X$.
**Theorem 3.2.38.** Given a well-ordered bounded lattice X:

The poset $\mathcal{N}(X)$ is a boolean algebra if and only if X is finitely complemented

And furthermore, we will show that the set of normal support is, in fact, the set of finitely complemented ones.

**Proposition 3.2.37.** Given a well-ordered bounded finitely complemented lattice X, the finitely complemented supports coincide with normal ones, i.e. we have

$$ \mathcal{F}(X) = \mathcal{N}(X) $$

### 3.2.3 Boolean algebra of finitely complemented regions

In this section, we will prove that finitely complemented supports (and thus normal supports) form a boolean algebra (Theorem 3.2.38). We will also show that this extends to finitely complemented covers and normalizable covers.

The plan of our proof for Theorem 3.2.38 is as follows: we first show that $\mathcal{F}(X)$ forms a boolean algebra by explicitly constructing the required operations on finitely complemented covers (Corollary 3.2.36) and then show that $\mathcal{F}(X)$ is isomorphic to $\mathcal{N}(X)$ (Proposition 3.2.37).

In the rest of this section, we suppose that the poset X is finitely complemented.

**Definition 3.2.32.** Given a finitely complemented poset X, and two cubes $I = (x, y)$ and $J = (u, v)$ of X, we define their intersection, written $I \cap J$ as the following cube, when defined (i.e. when $x \lor x' \le y \land y'$):

$$ (x, y) \cap (u, v) = (x \lor u, y \land v) $$

**Definition 3.2.33.** We define the following operations on covers R, S in $\mathcal{R}_F(X)$:

* union: $R \cup_N S = R \cup S$

* intersection: $R \cap_N S = \{I \cap J \mid I \in R, J \in S \text{ and } I \cap J \text{ is defined}\}$

* complement: $\bar{R}^N = \bigcap_{(x,y) \in R} (\{(\perp, y') \mid y' \in \max(\{x\}^{\text{lc}})\} \cup \{(x', \top) \mid x' \in \min(\{y\}^{\text{uc}})\})$

**Lemma 3.2.34.** The above operations are well-defined on $\mathcal{R}_F(X)$.

*Proof.* Given $(X, \le)$, a finitely complemented bounded lattice.

* $\cup_N$. Trivial.

* $\cap_N$. Given $R, S \in \mathcal{R}_F(X)$, $(x, y) \in R \cap_N S$. By definition, $(x, y) = (x_R \lor x_S, y_R \land y_S)$ such that $(x_R, y_R), (x_S, y_S) \in R \times S$ both finitely complemented.

$$ \begin{align*} \downarrow(\max x_R^{\text{lc}} \cup \max x_S^{\text{lc}}) &= \downarrow \max x_R^{\text{lc}} \cup \downarrow \max x_S^{\text{lc}} \\ &= x_R^{\text{lc}} \cup x_S^{\text{lc}} \\ &= \{x \in X \mid x \le x_R \text{ or } x \le x_S\} \end{align*} $$

$$ \downarrow(\max x_R^{\text{lc}} \cup \max x_S^{\text{lc}}) = (x_R \lor x_S)^{\text{lc}} $$

By finitude of, $\max x_R^{\text{lc}}$ and $\max x_S^{\text{lc}}$, $x_R \lor x_S$ is finitely lower complemented. Dually, $y_R \land y_S$ is finitely upper complemented. Thus, $(x, y)$ is finitely complemented for each cube $(x, y) \in R \cap_N S$. By definition, $R \cap_N S \in \mathcal{R}_F(X)$
• $\overline{=}^N$. Given $R \in \mathcal{R}_\mathcal{F}(X)$, and $(x, y) \in R$. We have $(x, y)$ and $(\perp, \top)$ finitely complemented. By definition of a finitely complemented poset, all $y' \in \max x^{\text{lc}}$ (resp. $x' \in \min y^{\text{uc}}$) are finitely upper (resp. lower) complemented. Thus, $(\perp, y')$ and $(x', \top)$ finitely complemented. Furthermore, by definition $\{(\perp, y') | y' \in \max x^{\text{lc}}\}$ and $\{(x', \top) | x' \in \min y^{\text{uc}}\}$ are finite. Thus, by the above proofs, as a result of a finite number of operations of union and intersection of elements of $\mathcal{R}_\mathcal{F}$, we have $\overline{R}^N \in \mathcal{R}_\mathcal{F}(X)$. $\square$

**Lemma 3.2.35.** The above operations are compatible with the corresponding ones on supports: for covers $R, S \in \mathcal{R}_\mathcal{F}(X)$, we have

$$[R \cap_N S] = [R] \cap [S] \qquad [R \cup_N S] = [R] \cup [S] \qquad [\overline{R}^N] = [\overline{R}]$$

*Proof.* Let $X$ a bounded lattice. Let $R, S \in \mathcal{R}_\mathcal{F}(X)$.

• $R \cup_N S$.

$$[R \cup_N S] = \bigcup_{I \in R \cup_N S} [I] = \bigcup_{I \in R \cup S} [I] = \bigcup_{I \in R} [I] \cup \bigcup_{J \in S} [J] = [R] \cup [S]$$

• $R \cap_N S$.

$$[R \cap_N S] = \bigcup_{(I,J) \in R \times S} [I \cap J] = \bigcup_{I \in R} \left( [I] \cap \bigcup_{J \in S} [J] \right) = \bigcup_{I \in R} [I] \cap \bigcup_{J \in S} [J] = [R] \cap [S]$$

• $\overline{R}^N$. Given $R \in \mathcal{R}_\mathcal{F}(X)$ and $(s, t) \in R$. We have $s$ (resp. $t$) finitely lower (resp. upper) complemented.

$$\begin{align*}
[\overline{R}^N] &= [ \bigcap_N \overline{\{(s,t)\}^N} ] \\
&= [ \bigcap_N ( \{ (\perp, x) \mid x \in \max s^{\text{lc}} \} \cup \{ (y, \top) \mid y \in \min t^{\text{uc}} \} ) ] \\
&= \bigcap_{(s,t) \in R} ( \bigcup_{x \in \max s^{\text{lc}}} [\perp, x] \cup \bigcup_{y \in \min t^{\text{uc}}} [(y, \top)] ) \\
&= \bigcap_{(s,t) \in R} ( \bigcup_{x \in \max s^{\text{lc}}} \downarrow x \cup \bigcup_{y \in \min t^{\text{uc}}} \uparrow y ) \\
&= \bigcap_{(s,t) \in R} ( \downarrow \max s^{\text{lc}} \cup \uparrow \min t^{\text{uc}} ) \\
&= \bigcap_{(s,t) \in R} ( s^{\text{lc}} \cup t^{\text{uc}} ) \tag*{By Lemma 3.2.24} \\
&= \bigcap_{(s,t) \in R} [s, t] \\
[\overline{R}^N] &= [\overline{R}] \tag*{\square}
\end{align*}$$

The finitely complemented covers $\mathcal{R}_\mathcal{F}(X)$ thus form a sub-boolean algebra of $\mathfrak{P}(X)$.

**Corollary 3.2.36.** The set $\mathcal{F}(X)$ is a boolean algebra.
**Proposition 3.2.37.** Given a well-ordered bounded finitely complemented lattice X, the finitely complemented supports coincide with normal ones, i.e. we have

$$ \mathcal{F}(X) = \mathcal{N}(X) $$

*Proof.* Given a finitely complemented well-order $(X, \le)$, fix $Y \subseteq X$.

* $\mathcal{F}(X) \subseteq \mathcal{N}(X)$.

Suppose $Y \in \mathcal{F}(X)$: there exists a cover $R \in \mathcal{R}_\mathcal{F}(X)$, such that $[R] = Y$. Let us prove that $N(\bar{Y}) = \max \bar{R}^N$. By Proposition 3.2.15 it suffices to show that for all covers $S$, such that $[S] \subseteq \bar{Y}$, we have $S \preceq \max \bar{R}^N$. Now suppose given such a cover $S$, we need to prove the following points:

- $S \preceq \max \bar{R}^N$. By Lemma 3.2.12, $[S] \subseteq \bar{Y}$ implies $S \preceq \mathcal{C}(\bar{Y})$. Furthermore, by finitude $\bar{R}^N \preceq \max \bar{R}^N$. Thus, it suffices to show $\mathcal{C}(\bar{Y}) \preceq \bar{R}^N$.
  Given $x \in \mathcal{C}(\bar{Y})$, we have $x \in \bigcap_{r \in R} \mathcal{C}(\bar{r})$. By Proposition 3.2.26, for all $r \in R$ exists $n_r \in N(\bar{r}) = \overline{\{r\}}^N$ such that $x \subseteq n_r$ i.e. $x \subseteq \bigcap_{r \in R} n_r \in \bar{R}^N$. Thus, $\mathcal{C}(\bar{Y}) \preceq \bar{R}^N$.

- $\max \bar{R}^N \preceq S \implies \max \bar{R}^N \subseteq S$. Now suppose, $\max \bar{R}^N \preceq S$. Then for all $r \in \max \bar{R}^N$ there exists $s_r \in \max \bar{R}^N$ and $r_s \in S$ such that $r \le s_r \le r_s$. By definition of max, $r = r_s = s_r$. Thus,

$$ \max \bar{R}^N \preceq S \implies \max \bar{R}^N \subseteq S $$

Finally, $N(\bar{Y}) = \max \bar{R}^N$. By Lemma 3.2.35, $\max \bar{R}^N \in \mathcal{R}_\mathcal{F}(X)$. And by the same reasoning, $\max \overline{\bar{R}^N} = N(\bar{Y}) = N(Y)$. Thus,

$$ Y \in \mathcal{F} \text{ implies } Y \in \mathcal{N}(X) \text{ and } N(Y), N(\bar{Y}) \in \mathcal{R}_\mathcal{F} $$

* $\mathcal{F}(X) \supseteq \mathcal{N}(X)$.

Given $Y \in \mathcal{N}(X)$, There exists a cover $R \in \mathcal{R}(X)$ such that $[\emptyset] = Y$ and $R$ in normal form. By 3.2.36, it then suffices to show that $\bar{Y} \in \mathcal{R}_\mathcal{F}(X)$ i.e. there exists a cover $\bar{R} \in \mathcal{R}_\mathcal{F}(X)$ such that $[\bar{R}] = \bar{Y}$, namely $N(\bar{Y})$. We first define an extension of $\bar{R}^N : \mathcal{R}(X) \to \mathcal{R}(X)$ to covers which are not finitely complemented, which can be seen as a sort of “best overestimation” of the normal form of the complement.

$$ \bar{R}^\infty = \bigcap_{(s,t) \in R} \{(\perp, x) \mid x \in s^{\text{lc}}\} \cup_N \{(x, \top) \mid x \in \max t^{\text{uc}}\} $$

We prove that for a cover in normal form $R$, $N(\overline{[R]}) \subseteq \bar{R}^\infty \in \mathcal{R}_\mathcal{F}(X)$. By the same method as for $\bar{R}^N$ in the proof of Proposition 3.2.26 and Lemma 3.2.35 for $R \in \mathcal{R}(X)$ and $r \in R$,

$$ [\bar{R}^\infty] = [\bar{R}] \text{ and } \mathcal{C}(\bar{r}) \preceq \overline{\{r\}}^\infty $$
By Remark 3.2.31, all elements of $X$ are upper complemented i.e. all cubes $(\perp, x)$ and $(x, \top)$ with $x \in \max t^{\text{uc}}$, for $t \in X$ are finitely complemented. Thus, for a finite cover $R$,

$$ \overline{R}^{\infty} \in \mathcal{R}_{\mathcal{F}}(X) $$

Suppose given $Y \in \mathcal{N}(X)$ and $x \in \mathcal{C}(\overline{Y})$, we have $x \in \bigcap_{r \in N(Y)} \mathcal{C}(\overline{r})$. By the previous remark, for all $r \in N(Y)$ exists $n_r \in \overline{\{r\}}^{\infty}$ such that $x \subseteq n_r$ i.e. $x \subseteq \bigcap_{r \in N(Y)} n_r \in \overline{N(Y)}^{\infty}$. Thus,

$$ N(\overline{Y}) \subseteq \mathcal{C}(\overline{Y}) \subseteq \overline{N(Y)}^{\infty} $$

By definition of the normal form, $N(\overline{Y}) \subseteq \overline{N(Y)}^{\infty}$. Thus, $N(\overline{Y}) \in \mathcal{R}_{\mathcal{F}}(X)$, finite i.e. $\overline{Y} \in \mathcal{R}_{\mathcal{F}}(X)$. By Lemma 3.2.34, the cover $N(Y)$ also belongs to $\mathcal{R}_{\mathcal{F}}(X)$. i.e. $Y \in \mathcal{F}(X)$. And $N(Y)$ and $N(\overline{Y})$ are finitely complemented. $\square$

**Theorem 3.2.38.** Given a well-ordered bounded lattice $X$:

The poset $\mathcal{N}(X)$ is a boolean algebra if and only if $X$ is finitely complemented

*Proof.* Let $X$ a well-ordered bounded lattice.

* If $X$ is finitely complemented, then by Corollary 3.2.36, the set $\mathcal{F}(X)$ of finitely complemented supports form a boolean algebra, and by Proposition 3.2.37, $\mathcal{F}(X) = \mathcal{N}(X)$. Thus, $\mathcal{N}(X)$ forms a boolean algebra.

* Now suppose that $X$ is not finitely complemented. By Remark 3.2.31, the condition (i) in the Definition 3.2.30 is always satisfied, and therefore (ii) has to be falsified. This means there exists an upper complemented element $t$ such that there exists $s \in \min t^{\text{uc}}$ which is not finitely lower complemented. Let us prove that $\mathcal{N}(X)$ is not stable by intersection, and therefore it is not a Boolean algebra. We first make two remarks.

- By Remark 3.2.31, all elements are finitely upper complemented, namely, $s$ and $t$ are both finitely upper complemented.

- Since $\perp^{\text{lc}} = \emptyset$, we deduce that $\perp$ is finitely lower complemented.

Thus, both cubes $[\perp, s]$ and $[\perp, t]$ are finitely complemented, which implies by Proposition 3.2.26, that they have a complement in normal form. Furthermore, the cover $\{(\perp, s)\}$ (resp. $\{(\perp, t)\}$) is trivially the normal form of $[\perp, s]$ (resp. $[\perp, t]$). Thus, both cubes $[\perp, t]$ and $[\perp, s]$ belong to $\mathcal{N}(X)$. Let us show that the intersection of these two cubes of $\mathcal{N}(X)$ is not in $\mathcal{N}(X)$. Given $x \in [\perp, t] \cap [\perp, s]$, we have $x \in t^{\text{uc}}$ and $x \le s \in \min t^{\text{uc}}$. By definition of $\min t^{\text{uc}}$, we deduce $x = s$. Since $s$ is by definition not finitely lower complemented, the cube $[s, s]$ is not finitely complemented either. Thus, by Proposition 3.2.26,

$$ [\perp, t] \cap [\perp, s] = [s, s] \notin \mathcal{N}(X) $$

By contraposition, we deduce the desired implication.
<figure><img src="image_133.png" /></figure>

This thus shows that, in a finitely complemented poset, we can implement the usual
boolean operations on covers while preserving the property of being normalizable.

*Remark 3.2.39.* Both of these boolean algebras are atomic. Indeed, they are generated by the set of supports of single cubes.

## 3.3 Syntactic covers of programs

### 3.3.1 Computing covers and complements

In the case of syntactic covers, i.e. covers on the poset of positions of a program, the operations of boolean algebra can be effectively implemented, by induction on the structure of programs, following Definition 3.2.33. Namely,

* the union of covers is immediate to implement,

* following Proposition 3.1.32, the supremum and infimum of positions can be computed, from which we can compute the intersection of covers,

* we can compute the generators of the complement, from which we can compute the complement of covers.

Let us detail the last point.

**Definition 3.3.1.** Given a position *p* of a program *P*, we define, by induction on *P*, the following set *inf*<sub>*P*</sub>(*p*) of positions of *P*:

$$ \inf_P(\perp) = \emptyset \qquad \inf_{P;Q}(\top) = \{\top;\top\} \qquad \inf_{P+Q}(\top) = \{\top+\perp, \perp+\top\} $$

$$ \inf_A(\top) = \{\perp\} \qquad \inf_{P\parallel Q}(\top) = \{\top\parallel\top\} \qquad \inf_{P^*}(\top) = \emptyset $$

$$ \inf_{P;Q}(p;q) = \begin{cases} \{\perp\} & \text{if } p=q=\perp \\ \{p';\perp \mid p' \in \inf_P(p)\} & \text{if } p \neq \perp \text{ and } q=\perp \\ \{\top;q' \mid q' \in \inf_Q(q)\} & \text{if } p=\top \text{ and } q \neq \perp \end{cases} $$

$$ \inf_{P+Q}(\emptyset+q) = \begin{cases} \{\perp\} & \text{if } p = \perp \\ \{\emptyset+q' \mid q' \in \inf_Q(q)\} \cup \{\top+\emptyset\} & \text{otherwise} \end{cases} $$

$$ \inf_{P+Q}(p+\emptyset) = \begin{cases} \{\perp\} & \text{if } q = \perp \\ \{p'+\emptyset \mid p' \in \inf_P(p)\} \cup \{\emptyset+\top\} & \text{otherwise} \end{cases} $$

$$ \inf_{P\parallel Q}(p\parallel q) = \begin{cases} \{\perp\} & \text{if } p=q=\perp \\ \{p'\parallel\top \mid p' \in \inf_P(p)\} \cup \{\top\parallel q' \mid q' \in \inf_Q(q)\} & \text{if } p \neq \perp \text{ or } q \neq \perp \end{cases} $$

$$ \inf_{P^*}(p^n) = \begin{cases} \{\perp\} & \text{if } n=0 \text{ and } p=\perp \\ \{\top^{n-1}\} & \text{if } n>0 \text{ and } p=\perp \\ \{p^n \mid p' \in \inf_P(p)\} & \text{if } p \neq \perp \end{cases} $$
**Proposition 3.3.2.** Given a position *p* of a program *P*, the set inf<sub>*P*</sub>(*p*) is a well-defined set of positions and, we have inf<sub>*P*</sub>(*p*) = max(*p*<sup>lc</sup>).

*Proof.* Given a program *P*, let us prove that by induction on *x* ∈ P(*P*), that max(*x*<sup>lc</sup>) = inf<sub>*P*</sub>(*x*).

• *x* = ⊥. Immediately,

$$ \max(\perp^{\text{lc}}) = \emptyset = \inf_{P}(\perp) $$

• *x* = ⊤. Let us prove max(⊤<sup>lc</sup>) = inf<sub>*P*</sub>(⊤) by induction on *P*.

– If *P* = *Q*<sup>*</sup>. We have ⊤<sup>lc</sup> = {⊥} ∪ {q<sup>*n*</sup> | q ∈ P(*Q*), *n* ∈ N} such that for all q<sup>*n*</sup> ∈ ⊤<sup>lc</sup>, q<sup>*n*</sup> < q<sup>*n*+1</sup> ∈ ⊤<sup>lc</sup>. Thus,

$$ \max(\top^{\text{lc}}) = \emptyset = \inf_{P}(\top) $$

– For all other cases, ⊤<sup>lc</sup> is trivially generated by the predecessors of ⊤ (e.g. ⊤||⊤, Ø+⊤ and ⊤+Ø ...).

Thus, max(⊤<sup>lc</sup>) = inf<sub>*P*</sub>(⊤).

• *P* ⊢ ⊥; ⊥, or *P* ⊢ ⊥<sup>0</sup> or *P* ⊢ ⊥||⊥ or *P* ⊢ ⊥+⊥. By the inferences rules

$$ \max(x^{\text{lc}}) = \{\perp\} = \inf_{P}(x) $$

• *Q*; *R* ⊢ *q*; ⊥, with *q* ≠ ⊥. We have *q*; ⊥ ∈ ↓{⊤; *v* | *R* ⊢ *v*} i.e. *x*<sup>lc</sup>∩{⊤; *v* | *R* ⊢ *v*} = ∅. Thus,

$$ \begin{aligned} \max x^{\text{lc}} &= \max\{u; \perp \mid u \not\geq q, Q \vdash u\} \\ &= \{P \vdash u; \perp \mid u \in \max q^{\text{lc}}\} \\ &= \{P \vdash u; \perp \mid u \in \inf_{Q}(q)\} \end{aligned} $$

$$ \max x^{\text{lc}} = \inf_{P}(x) $$

• *Q*; *R* ⊢ ⊤; *r* with *r* ≠ ⊥. We have {*q*; ⊥ | *Q* ⊢ *q*} ⊆ ↓{⊤; *v* | *R* ⊢ *v*}. Thus, by inference rules,

$$ \begin{aligned} \max x^{\text{lc}} &= \max(x^{\text{lc}} \cap \{\top; v \mid R \vdash v\}) \\ &= \{\top; v \mid v \in \max r^{\text{lc}}\} \\ &= \{\top; v \mid v \in \inf_{R}(r)\} \end{aligned} $$

$$ \max x^{\text{lc}} = \inf_{P}(x) $$

• *Q*||*R* ⊢ *x* = *q*||*r* with *q*||*r* ≠ ⊥||⊥. By the inference rules, *q*||*r* ≤ *u*||*v* is equivalent to *r* ≤ *v* or *q* ≤ *u*. Thus,

$$ \begin{aligned} x^{\text{lc}} &= \{P \vdash u \parallel v \mid q \not\le u\} \cup \{P \vdash u \parallel v \mid r \le v\} \\ x^{\text{lc}} &= \downarrow\{P \vdash u \parallel \top \mid u \in q^{\text{lc}}\} \cup \downarrow\{P \vdash \top \parallel v \mid v \in r^{\text{lc}}\} \end{aligned} $$
with both sets incomparable. Thus,

$$
\begin{align*}
\max x^{\text{lc}} &= \{P \models u \parallel \top \mid u \in \max q^{\text{lc}}\} \cup \{P \models \top \parallel v \mid v \in \max r^{\text{lc}}\} \\
&= \{P \models u \parallel \top \mid u \in \inf_Q q\} \cup \{P \models \top \parallel v \mid v \in \inf_R r\} \\
\max x^{\text{lc}} &= \inf_P(x)
\end{align*}
$$

• $Q^* \models x$. We have $\mathcal{P}(P)^+ = \{q^n \mid n \in \mathbb{N}, Q \models q\}$

- $Q^* \models \perp^n$ with $n > 0$. By the inference rule, $n \le m$ equivalent to $x = \perp^n \le q^m$. Thus,

$$
\max x^{\text{lc}} = \max(\{q^m \mid Q \models q, m < n\}) = \top^{n-1} = \inf_P(x)
$$

- $Q^* \models y^n$ with $y \neq \perp$ and $n \neq 0$.

By inference, $m \neq n$ implies $q^m < \perp^n \le x$, and $m > n$ implies $q^m > x$. Thus, by inference rule

$$
\begin{align*}
\max(x^{\text{lc}}) &= \max(x^{\text{lc}} \cap \{q^n \mid Q \models q\}) \\
&= \{q^n \mid q \not\le y\} \\
&= \{q^n \mid q \in \max y^{\text{lc}}\} \\
&= \{q^n \mid q \in \inf_Q y\} \\
\max(x^{\text{lc}}) &= \inf_P(x)
\end{align*}
$$

• $Q+R \models x = q+\emptyset$. The inference rules give

$$
\begin{align*}
(q+\emptyset)^{\text{lc}} &= \{P \models u+\emptyset \mid q \not\le u\} \cup \{P \models \emptyset+v \mid R \models v\} \cup \{\perp\} \\
(q+\emptyset)^{\text{lc}} &= \downarrow\{P \models u+\emptyset \mid u \in q^{\text{lc}}\} \cup \downarrow\{\emptyset+\top\}
\end{align*}
$$

With $\{P \models u+\emptyset \mid u \in q^{\text{lc}}\} \cap \downarrow\{\emptyset+\top\} = \{\perp\}$ and all other elements incomparable.
Thus, by induction rules

$$
\begin{align*}
\max x^{\text{lc}} &= \{P \models u+\emptyset \mid u \in \max q^{\text{lc}}\} \cup \{\emptyset+\top\} \\
&= \{P \models u+\emptyset \mid u \in \inf_Q q\} \cup \{\emptyset+\top\} \\
\max x^{\text{lc}} &= \inf_P(x)
\end{align*}
$$

• $Q+R \models x = \emptyset+r$. Similarly, $\max(x^{\text{lc}}) = \inf_P(x)$.

Thus, for all P and all $x \in \mathcal{P}(P)$, $\max(x^{\text{lc}}) = \inf_P(x)$. $\square$

<figure><img src="image_134.png" /></figure>

Similarly, given a position *p* of a program *P*, one can define by induction on *P* a set sup<sub>*P*</sub>(*p*) of positions of *P* such that sup<sub>*P*</sub>(*p*) = min(*p*<sup>uc</sup>). We can finally show that the poset of positions of a program satisfy the conditions of previous section:
**Proposition 3.3.3.** Given a program *P*, its poset of positions *P*(*P*) is a finitely complemented well-ordered lattice.

*Proof.* Essentially, the main position which is not finitely lower complemented is $\top$ in programs on the form $Q^*$. For each program *P*, we thus define a predicate $\vdash$ on its positions such that $P \vdash p$ if and only if $p$ not finitely lower complemented, by taking the closure under context of the above position:

$$ \begin{array}{c} \frac{Q \vdash q}{Q; R \vdash q; \bot} \\ \frac{R \vdash r}{Q; R \vdash \top; r} \end{array} \quad \begin{array}{c} \frac{Q \vdash q}{Q+R \vdash q+\emptyset} \\ \frac{R \vdash r}{Q+R \vdash \emptyset+r} \end{array} \quad \begin{array}{c} \frac{Q \vdash q}{Q \parallel R \vdash q \parallel r} \\ \frac{R \vdash r}{Q \parallel R \vdash q \parallel r} \end{array} \quad \begin{array}{c} \frac{Q^* \vdash \top}{Q \vdash q \quad n \in \mathbb{N}} \\ \frac{Q^* \vdash q^n}{Q^* \vdash \top} \end{array} $$

We can remark that for each $p \in \mathcal{P}(P)$ and $x \in \sup_P(p)$ we have $P \nvdash x$. As we already proved that $\sup_P(p) = \min(p^{\text{uc}})$, to prove the finitely complemented nature of $\mathcal{P}(P)$ we prove for all $p \in \mathcal{P}(P)$, $P \vdash p$ if and only if $p$ not finitely lower complemented, by induction on *p*.

* $p = \bot$. This implies $p^{\text{lc}} = \emptyset$. Trivially $p \nvdash$ and $p \in \mathcal{P}(P)$

* $p = \top$. We remark for each $t \in \mathcal{P}(P), t \le \top$. This implies $p^{\text{lc}} = \downarrow \top \setminus \{\top\}$

- $P = A$. We have $p^{\text{lc}} = \{\bot\} = \downarrow\{\bot\}$. Thus, $P \nvdash p$ and $p$ finitely lower complemented by Lemma 3.2.24.

- $P = Q; R$, $P = Q+R$ and $P = Q \parallel R$. Similarly, there exists a maximum for $\downarrow p$ (namely $\top; \top, \top+\emptyset$ and $\emptyset+\top, \top \parallel \top$).

- $P = Q^*$. Given $x \in \top^{\text{lc}} \setminus \bot = \{q^n \mid n \in \mathbb{N}, Q \vdash q\}$, such that $x = y^n$. By definition, $x < y^{n+1} \in \top^{\text{lc}}$. Thus, $\max \top^{\text{lc}} = \emptyset$. And $Q^* \vdash \top$ by definition

We now prove the induction step.

* $p = q \parallel r$. Using the inference rule,

$$ \begin{align*} (q \parallel r)^{\text{lc}} &= \{y \parallel z \mid y \not\geq q \text{ or } z \not\geq r\} \cup \{\bot\} \\ &= \downarrow(\{y \parallel \top \mid y \not\geq q\} \cup \{\top \parallel z \mid z \not\geq q\}) \\ &= (q \parallel \top)^{\text{lc}} \cup (\top \parallel r)^{\text{lc}} \end{align*} $$

As, $\{y \parallel \top \mid y \not\geq q\}$ and $\{\top \parallel z \mid z \not\geq q\}$ disjoint, $p^{\text{lc}}$ is finitely lower generated if and only if both $(q \parallel \top)^{\text{lc}}$ and $(\top \parallel r)^{\text{lc}}$ are finitely lower generated. By induction hypothesis this is equivalent to $Q \nvdash q$ and $R \nvdash r$. And by the inference rules of $\vdash$, this is equivalent to $Q \parallel R \nvdash p$.

* The other cases are treated with a similar argument (with a single variable) $p$ finitely lower generated equivalent to $P \nvdash p$.

□

The operations do not in general preserve the property of being normal for regions, but Theorem 3.2.38 and Proposition 3.3.3 however ensure that the property of being normalizable is preserved, and the normal form of a cover can be computed as follows.
**Proposition 3.3.4.** With the implementation of operations described above, the normal form of a cover R is $N(R) = \max(\bar{R})$, i.e. it can be obtained by computing twice the complement of R and only keeping cubes which are maximal w.r.t. inclusion.

*Proof.* It can be observed that the definition of the complement is such that it contains all the maximal cubes. □

**Proposition 3.3.5.** When the normal cover $N(R)$ is defined, it is equal to the set of all maximal cubes of the support, i.e.

$$N(R) = C^{\max}(R) = \{c \in C(R) \mid \forall c' \in C(R), c \not\subset c'\}$$

*Proof.* By definition $C^{\max}(R)$ is maximal for the order Definition 3.2.13 □

*Example 3.3.6.* Let us illustrate the fact that the operations defined above do not preserve normality (again, they only preserve normalizability), consider the following examples. With the cover R and S below, the cover $R \cup_N S$ is not normal (the normal form is the single cube covering the whole region):

<figure><img src="image_135.png" /></figure>

Similarly, with the covers R and S below, the cover $R \cap_N S$ is not normal because it contains the cube I pictured on the right

<figure><img src="image_136.png" /></figure>

(the normal form contains 3 cubes which do not include I).

### 3.3.2 Implementation

We will now explain how to implement the Algorithm 1.4.33 on our syntactic model. First we will have to tweak the cubical partition from Definition 1.4.18 in order to go beyond the scope of simple programs.
### 3.3.2.1 Deadlock algorithm and cubical partition

For this algorithm, we will restrict ourselves to programs of the form $P = P_1 \| \dots \| P_n$, where $P_i$ is a sequential process (it may contain loops and conditional branchings, but no parallel composition operator).

To implement the algorithm, we need a way to compute a cubical partition, compatible with the normal cover of our allowed region.

*Remark 3.3.7.* With our definition of cubes (even it the case of non-looping programs) it doesn't make sense to talk about the coarsest partition compatible, as it does not necessarily exist. Indeed, let us look at the program:

$$((P_a+P_a);V_a) \| (P_a;V_a)$$

There are two coarsest cubical partition (compatible with the normal cover) given below:

<figure><img src="image_137.png" /></figure>

And fundamentally, there is no “right” choice of what should be the “good” partition, between any of these partitions.

Thus, if we were to use Definition 1.4.18 directly, we would not get a partition, as seen in Example 3.3.13 below. To get back a partition, we will iterate $\Gamma^m$ until we reach a fixpoint.

We recall the operators used in Definition 1.4.18.

**Definition 3.3.8.** Given a cover $R$ on a sequential program $P$, we define the following partition operator

$$\Gamma_1^m(R) = \bigcup_{\substack{U \cup V = R \\ U \neq \emptyset}} \mathcal{C}^{\max}(Z_{U,V})$$

$$\text{with } Z_{U,V} = \bigcap_{u \in U} [u] \bigcap_{v \in V} [v]^c$$

*Remark 3.3.9.* If we compute the intersection of covers $\bigcap_{u \in U} \bigcap_{v \in V} v^c$, we get a cover on $Z_{U,V}$, and we can compute $\mathcal{C}^{\max}(Z_{U,V})$ using Proposition 3.3.4 using cubes

**Definition 3.3.10.** Given a cover $R$ on the parallel composition of $n$ sequential programs $P = P_1 \| \dots \| P_n$, we define the *pre-generic cubical partition*

$$\Gamma_n^m(R) = \prod_{i=1}^n \Gamma_1^m(\{c_i \mid \exists (r_k)_{1 \le k \le n} \in R, r_i = c_i\})$$

*Remark 3.3.11.* When $n = 1$, $\Gamma_n^m = \Gamma_1^m$, so we will simply write $\Gamma^m$ when context makes it clear.
Now we define the generic cubical partition associated to a cover $R$ as the fixpoint of the iterated composition by $\Gamma^m$

**Definition 3.3.12.** Given a cover $R$ on a program $P$, we define then generic cubical partition $\Gamma^*(R)$ associated to a cover $R$ as:

$$ \Gamma^*(R) = \lim_{n \to \infty} \underbrace{\Gamma^m \circ \dots \circ \Gamma^m}_{n \text{ times}}(R) $$

*Example 3.3.13.* If we reconsider the example from Remark 3.3.7, we give the iterated application of $\Gamma^m$ on the maximal cubes of the allowed cover below.

<figure><img src="image_138.png" /></figure>

$\Gamma^m(R)$

<figure><img src="image_139.png" /></figure>

$\Gamma^*(R) = \Gamma^m \circ \Gamma^m(R)$

In this case, $\Gamma^*(R) = \Gamma^m \circ \Gamma^m(R)$. We will prove later on, that this is the case for any maximal cover $R$ of a program.

*Remark 3.3.14.* When $\Gamma^*$ is the coarsest partition, it is obtained in a single iteration (which is the case for simple programs).

For sequential programs, the generic cubical partition of a maximal cover is actually the coarsest cubical partition i.e. we simply need to apply $\Gamma^m$ once to the cover to recover our partition. In itself, this is not very interesting, as we interested in parallel composition, but it is a central argument to prove that $\Gamma^*$ can be computed in a finite number of steps (Proposition 3.3.22).

**Lemma 3.3.15.** Let $R$ a maximal cover on a program $P(P+Q)$. Then

* Given $(\perp, p'+\emptyset) \in R$, then $(\perp, p') \in C^{\max}(\{x \mid x + \emptyset \in [R]\})$

* Given $(p+\emptyset, p'+\emptyset) \in R$, then $(p, p') \in C^{\max}(\{x \mid x + \emptyset \in [R]\})$

Similar properties are easily deduced for the other cases.

*Proof.* Given a cover $R$ on $P(P+Q)$

* Given $(p+\emptyset, p'+\emptyset) \in R$. Let us suppose $(p, p') \subseteq (q, q') \in C^{\max}(\{x \mid x + \emptyset \in [R]\})$. Then, by definition $(q+\emptyset, q'+\emptyset) \subseteq [R]$, thus by maximality, $p = q$ and $p' = q'$. Thus, $(p, p')$ is maximal.

* Given $(\perp, p'+\emptyset) \in R$. Let us suppose $(\perp, p') \subseteq (q, q') \in C^{\max}(\{x \mid x + \emptyset \in [R]\})$. Then, by definition $q = \perp$ and $(\perp+\emptyset, q'+\emptyset) \subseteq [R]$. By induction rules, $(\perp, q'+\emptyset) \subseteq [R]$. Thus, by maximality, $p' = q'$. Thus, $(\perp, p')$ is maximal.
□

**Lemma 3.3.16.** Let $R$ a maximal cover on a program $\mathcal{P}(P; Q)$. Then

* Given $(p; \perp, q; \perp) \in R$, then $(p, q) \in C^{\max}(\{x \mid x; \perp \in R\})$

* Given $(\perp, p; \perp) \in R$, then $(\perp, q) \in C^{\max}(\{x \mid x; \perp \in R\})$

* Given $(p; \perp, \top; q) \in R$, then

$$ (p, \top) \in C^{\max}(\{x \mid x; \perp \in R\}) \text{ and } (\perp, q) \in C^{\max}(\{x \mid \top; x \in R\}) $$

Similar properties are easily deduced for the other cases.

*Proof.* Given a maximal cover $R$ on $P; Q$.

* Let us suppose $(p, q) \subseteq (p', q') \in C^{\max}(\{x \mid x; \perp \in R\})$. Then, by definition $(p; \perp, q'; \perp) \subseteq [R]$, thus by maximality, $p = q$ and $p' = q'$. Thus, $(p, q)$ is maximal.

* Similarly, $(\perp, q) \subseteq (p', q') \in C^{\max}(\{x \mid x; \perp \in R\})$, implies $(\perp, q'; \perp) \subseteq [R]$, and the maximality of $(\perp, q; \perp)$ implies $q = q'$ and thus, $(\perp, q) = (p', q')$ maximal.

* Let us suppose $(p, \top) \subseteq (p', \top) \in C^{\max}(\{x \mid x; \perp \in R\})$. Then, by definition $(p'; \perp, \top; q) \subseteq [R]$, thus by maximality, $p = q$ and $p' = q'$. Thus, $(p, \top)$ is maximal. Similarly, $(\perp, q)$ is maximal.

□

We'll say that two cubes are *disconnected* when there exists no path from an element of the support of the first cube to the second one, that only crosses elements of their respective support. This is important when considering the maximal cube of the partitions, as two disconnected cubes/supports can never be joined together to form a bigger cube.

**Definition 3.3.17.** Let $R = (R_i)_{i \in I}$ be a cubical partition of the poset $X$. We define the partial order $\triangleleft^*$ on elements of $R$ as the reflexive transitive closure of the following relation: $R_i \triangleleft R_j$ if and only if for all $x \in [R_i]$ there exists $y \in [R_j]$ and a path of $[R_i] \cup [R_j]$ from $x$ to $y$

**Definition 3.3.18.** Given a program $P$, two cubes $i, j \in C(P)$, and $\triangleleft$ defined in Definition 3.3.17, we say that $i$ and $j$ are *disconnected* when $\{i\} \triangleleft \{j\}$ and $\{j\} \triangleleft \{i\}$.

**Proposition 3.3.19.** Given a maximal cover $R$ on a sequential program $P$.

$$ \Gamma^*(R) = \Gamma^m(R) $$

*Proof.* To prove this, we only need to prove that the cubes of $\Gamma^m(R)$ are all disjoint i.e. for any partition $U \amalg V = R$, $U \neq \emptyset$, the cubes of $C^{\max}(Z_{U,V})$ are disjoint.

If $(\perp, \top) \in R$. Then, by maximality $R = (\perp, \top)$. Thus, $\Gamma^m(R) = R$ and $\Gamma^*(R) = \Gamma^m(R)$. For the rest of the proof we can then suppose

$$ (\perp, \top) \notin R $$
By Definition 3.2.32, as $U \neq \emptyset$, we know that there exists a cube $c$ of $P$ such that $\bigcap_{u \in U} u = c$. Furthermore, $(\perp, \top) \notin U$ implies that $c \neq (\perp, \top)$. Now we will prove by induction on $P$ that for any $v \in R$ and any $c \subseteq u \in U$, $[c] \cap [v]^c = \coprod_{i \in I} [c_i]$ where all $c_i$ are maximal and pairwise disconnected.

First let us remark that if $c$ or $v$ is a singleton, the property is immediately verified. Indeed,

• If $[c] = \{x\}$ then $[c] \cap [v]^c = \{x\}$ or $\emptyset$

• If $[v] = \{x\}$ then

- $\{x\} \subset [c]$ contradicts the maximality of $v$

- $\{x\} = [c]$ implies $[c] \cap [v]^c = \emptyset$

- $\{x\} \cap [c] = \emptyset$ implies $[c] \cap [v]^c = c$

Then

• $P = \alpha$. OK.

• $P = P; Q$. Let us remark that the cubes of $P; Q$ that are not $(\perp, \top)$ or singletons are all are in one of the following sets:

$$C_1 = \{(\perp, q; \perp)\}$$

$$C_7 = \{(\top; p, \top)\}$$

$$C_2 = \{(\perp, \top; q) \mid q > \perp\}$$

$$C_6 = \{(p; \perp, \top) \mid p < \top\}$$

$$C_3 = \{(p; \perp, q; \perp) \mid p < q\}$$

$$C_5 = \{(\top; p, \top; q) \mid p < q\}$$

$$C_4 = \{(p; \perp, \top; q)\}$$

- If $c \in C_1$ i.e. $c = (\perp, q; \perp)$

* $v \in C_1$ i.e. $v = (\perp, q'; \perp)$. Then

$$[c] \cap [v]^c = [\perp, q; \perp] \cap [\perp, q'; \perp]^c$$

$$[c] \cap [v]^c = [\perp; \perp, q; \perp] \cap [\perp, q'; \perp]^c$$

Thus we have reduced to the case $c \in C_3$, $v \in C_1$.

* $v \in C_2$. Then $c \cap v^c = \emptyset$.

* $v \in C_3$. Then

$$ \begin{aligned} [c] \cap [v]^c &= \{\perp\} \cup (\{\emptyset+\perp, \emptyset+q\} \cap \{\emptyset+p', \emptyset+q'\})^c \\ &= \{\perp\} \cup (\{x+\emptyset \mid x \in [\perp, q] \cap [p', q']\}) \end{aligned} $$

By the case $c \in C_3$ and $v \in C_3$, where we can apply the induction hypothesis by Lemma 3.3.16,

$$\{x+\emptyset \mid x \in [\perp, q] \cap [p', q']\} = \coprod_{i \in I} [c_i]$$

With all $c_i$ maximal and disconnected.
· If there are no $i \in I$ such that $c_i = (\perp; \perp, q_i)$. Then

$$[c] \cap [v]^c = [\perp, \perp] \coprod_{i \in I} [c_i]$$

And all cubes are disconnected and maximal.

· Otherwise, there is at most a single $j \in I$ such that $c_j = (\perp; \perp, q_j)$. Then

$$[c] \cap [v]^c = [\perp, q_j] \coprod_{\substack{i \in I \\ i \neq j}} [c_i]$$

and all cubes are disconnected and maximal.

∗ $v \in C_4 \cup C_6$ i.e. $v = (p'; \perp, q')$, $q' \ge \top; \perp$ Then

$$[c] \cap [v]^c = [\perp, q; \perp] \cap [p'; \perp, q']^c$$

$$[c] \cap [v]^c = [\perp, q; \perp] \cap [p'; \perp, \top; \perp]^c$$

Thus we have reduced to the case, $v \in C_3$, where we can apply the induction hypothesis by Lemma 3.3.16.

∗ $v \in C_5 \cup C_7$. Then $c \cap v^c = c$.

– If $c \in C_2$ i.e. $c = (\perp, \top; q)$.

∗ $v \in C_1 \cup C_3$. Then $v \subset c$, which contradicts maximality of $v$.

∗ $v \in C_2$ i.e. $v = (\perp, \top; q')$. Then

$$[c] \cap [v]^c = [\perp, \top; q] \cap [\perp, \top; q']^c$$

$$[c] \cap [v]^c = [\perp; \perp, \top; q] \cap [\perp, \top; q']^c$$

Thus we have reduced to the case $c \in C_4$, $v \in C_1$.

∗ $v \in C_4$ i.e. $v = (p'; \perp, \top; q')$. Then

$$[c] \cup [v] \subseteq [\perp, \top; \perp] \cup [\top; \perp, \top; q'] = [\perp, \top; q']$$

Such that $v \subset (\perp, \top; q') \in \mathcal{C}([R])$, which contradicts its maximality.

∗ $v \in C_5$ i.e. $v = (\top; p', \top; q')$. Then,

· $p' = \perp$ implies

$$[c] \cup [v] \subseteq [\perp, \top; \perp] \cup [\top; \perp, \top; q'] = [\perp, \top; q']$$

Such that $v \subset (\perp, \top; q') \in \mathcal{C}([R])$, which contradicts its maximality.

· $p' > \perp$.

$$[c] \cap [v]^c = [\perp, \top; q] \cap [\top; p', \top; q']^c$$

$$[c] \cap [v]^c = [\perp, \top; \perp] \cup [\top; \perp, \top; q] \cap [\top; p', \top; q']^c$$

Then, by the case $c \in C_5$, $v \in c_5$, we have that there exists a family of maximal disconnected cubes $(c_i)_{i \in I}$ such that

$$[\top; \perp, \top; q] \cap [\top; p', \top; q']^c = \coprod_{i \in I} c_i$$
Furthermore, $\top;\bot \in [\top;\bot, \top;\bot]$ and $[\top; p', \top; q']^c$ implies that there exists a single $j \in I$ such that $c_j = (\top;\bot, q_j)$. Then

$$[c] \cap [v]^c = [\bot, q_j] \coprod_{\substack{i \in I \\ i \neq j}} [c_i]$$

and all cubes are disconnected and maximal.

* $v \in C_6$. Then $[\bot, \top] = [c] \cup [v] \subseteq [R]$ implies $(\bot, \top) \in R$ which contradicts the maximality of $v$.

* $v \in C_7$ i.e. $v = (\top; p', \top)$. Then,

$$[c] \cap [v]^c = [\bot, \top; q] \cap [\top; p', \top]^c$$

$$[c] \cap [v]^c = [\bot, \top; q] \cap [\top; p', \top; \top]^c$$

Thus we have reduced to the case, $v \in C_5$ or the singleton, where we can apply the induction hypothesis by Lemma 3.3.16.

* If $c \in C_3$, i.e. $c = p; \bot, q; \bot$

* $v \in C_1$. i.e. $v = (\bot, q'; \bot)$. Then

$$[c] \cap [v]^c = [p; \bot, q; \bot] \cap [\bot, q'; \bot]^c$$

$$[c] \cap [v]^c = [\bot; \bot, q; \bot] \cap [\bot; \bot, q'; \bot]^c$$

Thus we have reduced to the case, $v \in C_3$, where we can apply the induction hypothesis by Lemma 3.3.16.

* $v \in C_2 \cup C_7$. Then $c \cap v^c = c$.

* $v \in C_3$ i.e. $v = (p'; \bot, q'; \bot)$. Then

$$[c] \cap [v]^c = [p; \bot, q; \bot] \cap [p'; \bot, q'; \bot]^c$$

$$[c] \cap [v]^c = \{x; \bot | x \in [p, q] \cap [p', q']\}$$

By induction hypothesis (which can be applied, by Lemma 3.3.15), $[p, q] \cap [p', q'] = \coprod_{i \in I} [p_i, q_i]$ with all $((p_i, q_i))_{i \in I}$ disconnected and maximal. Thus, by construction,

$$\{x; \bot | x \in [p, q] \cap [p', q']\} = \coprod_{i \in I} [p_i; \bot, q_i; \bot]$$

with all $((p_i; \bot, q_i; \bot))_{i \in I}$ disconnected and maximal.

* $v \in C_4 \cup C_6$, i.e. $v = (p'; \bot, q')$, $q' \ge \top; \bot$ Then

$$[c] \cap [v]^c = [p; \bot, q; \bot] \cap [p'; \bot, q']^c$$

$$[c] \cap [v]^c = [p; \bot, q; \bot] \cap [p'; \bot, \top; \bot]^c$$

Thus we have reduced to the case, $v \in C_3$, where we can apply the induction hypothesis by Lemma 3.3.16.

* $v \in C_5$ i.e. $v = \top; p', \top; q'$
· $q, p' \neq \top, \bot$ implies $c \cap v^c = c$

· Otherwise $p < q = \top$ implies $v \subset p; \top, \top; q'$ which contradicts its maximality.

— If $c \in C_4$.

* $v \in C_1$ i.e. $v = (\bot, q'; \bot)$. Then

$$[c] \cap [v]^c = [p; \bot, \top; q] \cap [\bot, q'; \bot]^c$$

$$[c] \cap [v]^c = [p; \bot, \top; q] \cap [\bot; \top, q'; \bot]^c$$

Thus we have reduced to the case $c \in C_4$, $v \in C_3$, where we can apply the induction hypothesis by Lemma 3.3.16.

* $v \in C_2$ i.e. $v = (\bot, \top; q')$, $q' > \bot$ Then

$$[c] \cap [v]^c = [p; \bot, \top; q] \cap [\bot, \top; q']^c$$

$$[c] \cap [v]^c = [\top; \bot, \top; q] \cap [\bot, \top; q']^c$$

Thus we have reduced to the case $c \in C_5$, $v \in C_2$ or to the case of $[c]$ singleton.

* $v \in C_3$ i.e. $v = (p'; \bot, q'; \bot)$. Then $q' = \top$ is a special case of the case of $v \in C_4$. So we can suppose $q' < \top$. Then

$$[c] \cap [v]^c = [p; \bot, \top; q] \cap [p'; \bot, q'; \bot]^c$$

$$[c] \cap [v]^c = [p; \bot, \top; \bot] \cap [p'; \bot, q'; \bot]^c \coprod [\top; \bot, \top; q]$$

Then, by the case $c \in C_2$, $v \in c_3$, where we can apply the induction hypothesis by Lemma 3.3.16, we have that there exists a family of maximal disconnected cubes $(c_i)_{i \in I}$ such that

$$[p; \bot, \top; \bot] \cap [p'; \bot, q'; \bot]^c = \coprod_{i \in I} c_i$$

Furthermore, $\top; \bot \in [p; \bot, \top; \bot] \cap [p'; \bot, q'; \bot]^c$ implies that there exists a single $j \in I$ such that $c_j = (p_j, \top+\bot)$. Then

$$[c] \cap [v]^c = [p_j, \top+q] \coprod_{\substack{i \in I \\ i \neq j}} [c_i]$$

and all cubes are disconnected and maximal.

* $v \in C_4$ i.e. $v = (p'; \bot, \top; q')$. Then

$$[c] \cap [v]^c = [p; \bot, \top; q] \cap [p'; \bot, \top; q']^c$$

$$[c] \cap [v]^c = [p; \bot, \top; \bot] \cap [p'; \bot, \top; \bot]^c \coprod [\top; \bot, \top; q] \cap [\top; \bot, \top; q']^c$$

With the cubes of $[p; \bot, \top; \bot] \cap [p'; \bot, \top; \bot]^c$ and $[\top; \bot, \top; q] \cap [\top; \bot, \top; q']^c$ disconnected, as $\top; \bot$ in both complements. Thus, we reduced to the case $c \in C_3$, $V \in C_3$ and $c \in C_5$, $v \in C_5$, where we can apply the induction hypothesis by Lemma 3.3.16.
* $v \in C_5$. Dual to $v \in C_3$.

* $v \in C_6$. Dual to $v \in C_2$.

* $v \in C_7$. Dual to $v \in C_1$.

- If $c \in C_5$. Dual to the case $c \in C_3$.

- If $c \in C_6$. Dual to the case $c \in C_2$.

- If $c \in C_7$. Dual to the case $c \in C_1$.

* $P = P+Q$. Let us start by remarking that the cubes of $P+Q$ that are not $(\perp, \top)$ all are in one of the following sets:

$$C_1 = \{(\perp, \emptyset + q)\}$$

$$C_6 = \{(\emptyset + p, \top)\}$$

$$C_2 = \{(\perp, q + \emptyset)\}$$

$$C_5 = \{(p + \emptyset, \top)\}$$

$$C_3 = \{(p + \emptyset, q + \emptyset) \mid p \le q\}$$

$$C_4 = \{(\emptyset + p, \emptyset + q) \mid p \le q\}$$

- If $c \in C_3$ i.e. $c = (p+\emptyset, q+\emptyset)$.

* $v \in C_1 \cup C_4 \cup C_6$. Then $[c] \cap [v]^c = [c]$.

* $v \in C_2$ i.e. $v = (\perp, q' + \emptyset)$. Then

$$[c] \cap [v]^c = [p+\emptyset, q+\emptyset] \cap [\perp, q' + \emptyset]^c$$

$$[c] \cap [v]^c = [p+\emptyset, q+\emptyset] \cap [\perp+\emptyset, q' + \emptyset]^c$$

Thus we have reduced this case to a special case of $c \in C_3$ and $v \in C_3$, where the induction hypothesis can be applied by Lemma 3.3.15

* $v \in C_3$ i.e. $c = (p'+\emptyset, q'+\emptyset)$. Then

$$[c] \cap [v]^c = [p+\emptyset, q+\emptyset] \cap [p'+\emptyset, q'+\emptyset]^c$$

$$[c] \cap [v]^c = \{x+\emptyset \mid x \in [p, q] \cap [p', q']\}$$

By induction hypothesis (which can be applied, by Lemma 3.3.15), $[p, q] \cap [p', q'] = \coprod_{i \in I} [p_i, q_i]$ with all $((p_i, q_i))_{i \in I}$ disconnected and maximal. Thus, by construction,

$$\{x+\emptyset \mid x \in [p, q] \cap [p', q']\} = \coprod_{i \in I} [p_i+\emptyset, q_i+\emptyset]$$

with all $((p_i+\emptyset, q_i+\emptyset))_{i \in I}$ disconnected and maximal.

* $v \in C_5$. Dual to the case $v \in C_2$.

- If $c \in C_1$ i.e. $c = (\perp, \emptyset + q)$.

* $v \in C_1$. i.e. $v = (\perp, \emptyset + q')$. Then

$$[c] \cap [v]^c = [\perp, \emptyset + q] \cap [\perp, \emptyset + q']^c$$

$$[c] \cap [v]^c = [\emptyset + \perp, \emptyset + q] \cap [\emptyset + \perp, \emptyset + q']^c$$

This case is a special case of $c \in C_3$ and $v \in C_3$, where we can apply the induction hypothesis thanks to the Lemma 3.3.15,
* $v \in C_2$ i.e. $v = (\perp, q' + \emptyset)$. Then $[\perp, \emptyset + q] \cap [\perp, q' + \emptyset]^c = [\emptyset + \perp, \emptyset + q]$.

* $v \in C_3 \cup C_5$. Then, $[c] \cap [v]^c = [c]$.

* $v \in C_4$ i.e. $v = (\emptyset + p', \emptyset + q')$. Then

$$ 
\begin{aligned}
[c] \cap [v]^c &= \{\perp\} \cup ( [\emptyset + \perp, \emptyset + q] \cap [\emptyset + p', \emptyset + q']^c ) \\
&= \{\perp\} \cup ( \{x + \emptyset \mid x \in [\perp, q] \cap [p', q']\} )
\end{aligned}
$$

By the case $c \in C_3$ and $v \in C_3$, where we can apply the induction hypothesis by Lemma 3.3.15,

$$ \{x + \emptyset \mid x \in [\perp, q] \cap [p', q']\} = \coprod_{i \in I} [c_i] $$

With all $c_i$ maximal and disconnected.

* If there are no $i \in I$ such that $c_i = (\emptyset + \perp, q_i)$. Then

$$ [c] \cap [v]^c = [\perp, \perp] \coprod_{i \in I} [c_i] $$

And all cubes are disconnected and maximal.

* Otherwise, there is at most a single $j \in I$ such that $c_j = (\emptyset + \perp, q_j)$. Then

$$ [c] \cap [v]^c = [\perp, q_j] \coprod_{\substack{i \in I \\ i \neq j}} [c_i] $$

and all cubes are disconnected and maximal.

* $v \in C_6$ i.e. $v = (\emptyset + p' \top)$. Then

$$ [c] \cap [v]^c = \{\perp\} \cup ( [\perp, \emptyset + q] \cap [\emptyset + p', \emptyset + \top]^c ) $$

Thus we have reduced this case to the case $v \in C_4$, where we can apply the induction hypothesis thanks to the Lemma 3.3.15.

- If $c \in C_2$. Symmetric to the case $c \in C_1$

- If $c \in C_4$. Symmetric to $c \in C_3$.

- If $c \in C_5$. Dual to $c \in C_2$.

- If $c \in C_6$. Dual to $c \in C_1$.

* $P = Q^*$. By assimilating $Q^*$ to an infinite sequential composition of copies of $Q$ and applying the case $Q;Q$ we obtain the desired result.

□

As we previously explained, for general programs of the form $P = P_1 \parallel \cdots \parallel P_n$, the generic cubical partition can be computed in only two steps of applying $\Gamma^m$.

Furthermore, as per the following Lemma 3.3.20 the computations of the iterated applications of $\Gamma^m$ to a cover $R$ can be done directly on the different projections of $R$ along each axis. And for each of these projections, the second application of $\Gamma^m$ can be done on independent subsets of cubes of $\Gamma^m(R)$ (Lemma 3.3.21)
**Lemma 3.3.20.** Given a cover R on a program P = P₁||...||Pₙ, with Pₖ sequential for all 1 ≤ k ≤ n. We have

$$ \Gamma^m \circ \Gamma^m(R) = \prod_{k=1}^{n} \Gamma^m \circ \Gamma^m(R_k) $$

with $R_k = \{x_k | \exists (r_i)_{1 \le i \le n} \in R, r_k = x_k\}$.

*Proof.* This result is obtained directly by applying the Definition 3.3.12 twice

$$ \begin{aligned} \Gamma^m \circ \Gamma^m(R) &= \Gamma^m\left(\prod_{k=1}^{n} \Gamma^m(R_k)\right) \\ &= \prod_{i=1}^{n} \Gamma^m\left(\{x_k \mid \exists (r_i)_{1 \le i \le n} \in \prod_{k=1}^{n} \Gamma^m(R_k), r_k = x_k\}\right) \\ &= \prod_{i=1}^{n} \Gamma^m\left(\{x_i \mid \exists r_i \in \Gamma^m(R_i), r_i = x_i\}\right) \\ \Gamma^m \circ \Gamma^m(R) &= \prod_{i=1}^{n} \Gamma^m(\Gamma^m(R_i)) \end{aligned} $$

□

As previously explained, computation of $\Gamma^m(R)$ scales greatly with the number of cubes. Furthermore, the number of cubes of $\Gamma^m(R)$ will always be greater than or equal to the number of cubes of R. Thus, when applying $\Gamma^m$ multiple times, the following Lemma 3.3.21 drastically reduce computation cost by instead allowing us to apply $\Gamma^m$ to subset of $\Gamma^m(R)$.

**Lemma 3.3.21.** Given a cover R on P sequential, we have

$$ \Gamma^m \circ \Gamma^m(R) = \bigcup_{\substack{U \sqcup V = R \\ U \neq \emptyset}} \Gamma^m(C^{\max}(Z_{U,V})) $$

*Proof.* By definition

$$ \Gamma^m(R) = \bigcup_{\substack{U \sqcup V = R \\ U \neq \emptyset}} C^{\max}(Z_{U,V}) $$

Furthermore, by definition, given $(U, V) \neq (U', V')$, we have $Z_{U,V} \cap Z_{U',V'} = \emptyset$ As the $Z_{U,V}$ that are empty can be ignored, we can consider that

$$ \Gamma^m(R) = \bigcup_{i \in I} C^{\max}(R_i) $$

with all $R_i \neq \emptyset$ and $R_i \cap R_j = \emptyset$. Now let us suppose given a partition $X \sqcup Y = \Gamma^m(R)$, $X \neq \emptyset$ and $Z_{X,Y} \neq \emptyset$. We define

$$ X_i = X \cap C^{\max}(R_i) $$

$$ Y_i = Y \cap C^{\max}(R_i) $$
such that

$$Z_{X,Y} = \bigcap_{j \in I} Z_{X_j, Y_j}$$

Then by contradiction, let us prove that there exists a single $i \in I$ such that $X_i \neq \emptyset$.

* First, as $X = \bigcup_{i \in I} X_i$, and $X \neq \emptyset$, there exists $i \in I$ such that $X_i \neq \emptyset$.

* Now let us suppose by contradiction that there exists two distinct indices $i \neq j$ such that $X_i$ and $X_j$ are non-empty. Then let $x_i, x_j \in X_i \times X_j$. By definition,

$$Z_{X,Y} \subseteq [x_i] \cap [x_j] \subseteq R_i \cap R_j = \emptyset$$

Which contradicts our hypothesis $Z_{X,Y} \neq \emptyset$.

Thus, there exists a unique $i \in I$, such that $X \cap C^{\max}(R_i) \neq \emptyset$. Now, let us suppose $j \in I, j \neq i$. Then as $R_i \cap R_j = \emptyset$, by definition,

$$ \begin{align*} Z_{X_i, Y_i} \cap Z_{X_j, Y_j} &= Z_{X_i, Y_i} \cap Z_{\emptyset, C^{\max}(R_j)} \\ &= Z_{X_i, Y_i} \cap \bigcap_{y \in C^{\max}(R_j)} [y]^c \\ &= Z_{X_i, Y_i} \cap (\bigcup_{y \in C^{\max}(R_j)} [y])^c \\ &= Z_{X_i, Y_i} \cap [R_j]^c \\ Z_{X_i, Y_i} \cap Z_{X_j, Y_j} &= Z_{X_i, Y_i} \end{align*} $$

Then, for all $X \in \mathcal{Y}$ such that $X \neq \emptyset$ and $Z_{X,Y} \neq \emptyset$, we have

$$Z_{X,Y} = \bigcap_{j \in I} Z_{X_j, Y_j} = Z_{X_i, Y_i}$$

Thus, with $Y_X = \Gamma^m(R) \setminus X$

$$ \begin{align*} \{X \subseteq \Gamma^m(R) \mid X \neq \emptyset, Z_{X,Y_X} \neq \emptyset\} &= \bigcup_{i \in I} \{X \subseteq C^{\max}(R_i) \mid X \neq \emptyset, Z_{X,Y_X} \neq \emptyset\} \\ \{X \subseteq \Gamma^m(R) \mid X \neq \emptyset, Z_{X,Y_X} \neq \emptyset\} &= \bigcup_{i \in I} \{X \subseteq C^{\max}(R_i) \mid X \neq \emptyset, Z_{X, C^{\max}(R_i) \setminus X} \neq \emptyset\} \end{align*} $$
Now we can finally prove our result

$$
\begin{align*}
\Gamma^m \circ \Gamma^m &= \bigcup_{\substack{X \sqcup Y \\ X \neq \emptyset}} Z_{X,Y} \\
&= \bigcup_{i \in I} \bigcup_{\substack{X \subseteq \mathcal{C}^{\max}(R_i) \\ X \neq \emptyset}} Z_{X, \Gamma^m(R) \setminus X} \\
&= \bigcup_{i \in I} \bigcup_{\substack{X \subseteq \mathcal{C}^{\max}(R_i) \\ X \neq \emptyset}} Z_{X, \mathcal{C}^{\max}(R_i) \setminus X} \\
&= \bigcup_{i \in I} \Gamma^m(\mathcal{C}^{\max}(R_i)) \\
\Gamma^m \circ \Gamma^m(R) &= \bigcup_{\substack{U \sqcup V = R \\ U \neq \emptyset}} \Gamma^m(\mathcal{C}^{\max}(Z_{U,V}))
\end{align*}
$$

□

Now we have everything to prove that the generic partition can indeed be obtained by applying our operator $\Gamma^m$ twice, with the previous lemmas mitigating the computation costs of the second iteration.

**Proposition 3.3.22.** Given a maximal cover $R$ on a program $P = P_1 \| \cdots \| P_n$, with $P_i$ a sequential program we have that $\Gamma^*(R) = \Gamma^m \circ \Gamma^m(R)$

*Proof.* We only need to prove that all cubes of $\Gamma^m \circ \Gamma^m(R)$ are disjoint to conclude the proof. By Lemma 3.3.20 we have that

$$ \Gamma^m \circ \Gamma^m(R) = \prod_{k=1}^{n} \Gamma^m \circ \Gamma^m(R_k) $$

with $R_k = \{x_k \mid \exists (r_i)_{1 \le i \le n} \in R, r_k = x_k\}$. By Lemma 3.3.21,

$$ \Gamma^m \circ \Gamma^m(R_k) = \bigcup_{\substack{U \sqcup V = R_k \\ U \neq \emptyset}} \Gamma^m(\mathcal{C}^{\max}(Z_{U,V})) $$

As all $Z_{U,V}$ are disjoint, we simply need to prove that the cubes of $\Gamma^m(\mathcal{C}^{\max}(Z_{U,V}))$ are disjoint. By definition $\mathcal{C}^{\max}(Z_{U,V})$ is maximal, we can then apply Proposition 3.3.19, which gives the desired result. □

### 3.3.2.2 Algorithm and implementation

With what we have proven so far in the chapter, we can finally implement Algorithm 1.4.33 for syntactic region. The algorithm is the same as before, with $\langle$ defined on syntactic cubes in Definition 3.3.17.

**Algorithm 3.3.23.** Let $R$ be the cover of the forbidden region of a program $P$, such that $X = \bar{R}$ is the authorized region (pruned state space) of $P$. We can compute

1. The normal cubical cover $N(X)$ of $X$ as maximal cubes of the complement of $X^c$
2. The generic cubical partition $\Gamma^*(N(X))$ compatible with $N(X)$

3. Deadlocks are the cubes of $\Gamma^*(N(X)) \setminus R_{max}$ that are maximal (w.r.t. $\triangle^*$). Where $R_{max}$ is the only cube of $\Gamma^*(N(X))$ containing $\top_P$

4. A cubical partition $\mathcal{U}(X)$ of the unsafe region as the downward closure (w.r.t. $\triangle$) of the deadlocks

5. A cubical partition $\mathcal{D}(X)$ of the doomed region as $\mathcal{U}(X) \setminus \mathcal{E}(X)$, where $\mathcal{E}(X)$ is the downwards closure (w.r.t. $\triangle^*$) of $R_{max}$

*Example 3.3.24.* Let us reconsider the Swiss Cross $(P_a; P_b; V_b; V_a) \parallel (P_b; P_a; V_a; V_b)$ whose maximal cubes are given below

<figure><img src="image_140.png" /></figure>

Algorithm 3.3.23 gives the following ordering of the generic cubical partition w.r.t. the maximal cover above.

<figure><img src="image_141.png" /></figure>

In light grey in the figure above we see all cubes that do not have transition to another cube. Then we obtain, the unique deadlock of our program as the upper corner of the cube with no transitions that is not the cube in the upper corner (the end of our program).

Then, the unsafe region is obtained on the left as the downwards closure of this cube. The downward closure of the maximal cube is given in the middle, and the doomed region, which correspond to the intersection of its complement with the unsafe region can be seen on the right.
<figure><img src="image_142.png" /></figure>

The steps of the algorithm are performed the same way as in the Example 1.4.34. Now let us recapitulate how to implement them. All these were effectively implemented in [42], using the OCaml language.

**Programs and positions** Any inductive structure works well for implementing the definitions of Section 3.1.

**Calculating the normal form.** The first step, calculating the normal form of a region, requires implementing the operations in Definition 3.2.33:

* Union is union of list.

* Intersection can be implemented by Definition 3.2.32. This requires the implementation of $\vee$ and $\wedge$ of Proposition 3.1.32, which is easily implemented with our data structure.

* Complement $\complement$ requires:

- Intersection (which is not a problem per the point above)

- Comparison of cubes. Though, as:

$$ (x, y) \subseteq (u, v) \iff u \le x \text{ and } y \le v \iff u \wedge x = u \text{ and } y \vee v = v $$

comparison can be done with the implementation of $\vee$ and $\wedge$ of Proposition 3.1.32.

- Calculating the generators of the lower and upper complement. This was already done in Definition 3.3.1 and Proposition 3.3.2.

**Calculating the coarsest cubical partition** The second step, finding the normal cubical partition requires only implementation of intersection, and the normal form of a region, whose implementation is already explained above.

**Deadlocks, unsafe and doomed regions** To implement these step the only additional operation to implement is comparing two cubes w.r.t. $\prec$. This can be done in the same way as for cubical partition of the geometric semantics of a program (Proposition 1.4.32):

**Proposition 3.3.25.** Given a program $P$, and two cubes $(p, q), (p', q') \in C(P)$, such that $(p, q) \cap (p', q') = \emptyset$ we have that

$$ (p, q) \prec (p', q') \iff \exists y' \in (p', q'), q \to y' \text{ or } \exists x \in (p, q), x \to p' $$
*Proof.* To prove this we will adapt [30, Proposition 7.5]. Given two disjoint cubes $(p, q)$, $(p', q')$ on a program $P$, $(p, q) \triangleleft (p', q')$ is by definition equivalent to: for all $u \in (p, q)$, there exists $v' \in (p', q')$ such that $u \to^* v$ i.e.

$$ \text{there exists } v, u' \in [p, q] \times [p', q'] \text{ such that } u \to^* v \to u' \to^* v' \quad (3.1) $$

Let us prove that this is equivalent to

$$ \exists y' \in (p', q'), q \to y' \text{ or } \exists x \in (p, q), x \to p' \quad (3.2) $$

The indirect implication 3.2 $\implies$ Eq. (3.1) is evident. Let us prove the direct 3.1 $\implies$ Eq. (3.2) by induction on $P$.

First let us remark that by definition:

$$ (x, v') \subseteq (p, q) \text{ and } (u', y') \subseteq (p', q') $$

Then by the fact that the cubes are disjoint we also have

$$ u' \notin (p, q) \text{ and } v \notin (p', q') $$

* $P = \alpha$. OK.

* $P = P_1; P_2$. We will differentiate according to the value of $v$.

- $v = \perp$. This implies by inference rules, $u' = \perp; \perp$. By our first remark, this implies $p' \le \perp; \perp$. As $v \notin (p', q')$, we have $p' > \perp$ i.e. $p' = \perp; \perp$. Thus taking $x = v$ concludes the case.

- $v = v_1; \perp, a < \top$. Then $u' = u'_1; \perp$. Supposing that $\perp < p$ and $q' < \top$, we have $p = p_1; \perp$ and two cases for $q'$:

$$ \begin{array}{l} * q' = q'_1; \perp. \text{ As } p \le u \le q \text{ and } p' \le v' \le q' \text{ we have} \\ u = u_1; \perp \text{ and } v = v_1; \perp \end{array} $$

Then the existence of a path $u \to^* v \to u' \to v'$ is by inference rules equivalent to the existence of a path $u_1 \to^* v_1 \to u'_1 \to^* v'_1$. By induction hypothesis this is equivalent to

$$ \exists y_1' \in (p_1', q_1'), q_1 \to y_1' \text{ or } \exists x_1 \in (p_1, q_1), x_1 \to p_1' $$

By inference rules this is equivalent to

$$ \exists \in (p_1'; \perp, q_1'; \perp), q_1; \perp \to y_1'; \perp \text{ or } \exists x_1; \perp \in (p_1; \perp, q_1; \perp), x_1; \perp \to p_1'; \perp $$

This concludes the case.

$$ \begin{array}{l} * q' = \top; q'_2. \text{ Remarking that } (p_1; \perp, q) \triangleleft (p', q') \text{ is equivalent to } (p_1; \perp, q) \triangleleft (p, \top; \perp) \text{ we reduce to the previous case.} \\ \text{Then, remarking that in the remaining case, } (\perp, q) \triangleleft (p', \top) \text{ is equivalent to} \\ \qquad (\perp; \perp, q) \triangleleft (p', \top; \top) \text{ we conclude the case} \end{array} $$

- $v = \top; a, a < \top$. Similar to the case above.
v = ⊤;⊤. This implies u' = ⊤ ad is dual to the case v = ⊥.

• P = P₁+P₂.

- v = ⊥. This implies by inference rules, u' = ⊥+Ø or u' = Ø+⊥. By our first remark, this implies p' ≤ ⊥+Ø or p' ≤ Ø+⊥. As v /∈ (p', q'), we have p' > ⊥ i.e. p' = ⊥+Ø or p' = Ø+⊥. Thus taking x = v concludes the case.

- v = v₁+Ø, v₁ < ⊤. Then u' = u'₁+Ø. Supposing that ⊥ < p and q' < ⊤, we have p = p₁+Ø and q' = q'₁+Ø. As p ≤ u ≤ q and p' ≤ v' ≤ q' we have

$u = u_1+\emptyset \text{ and } v = v_1+\emptyset$

By induction hypothesis this is equivalent to

$\exists y_1' \in (p_1', q_1'), q_1 \to y_1' \text{ or } \exists x_1 \in (p_1, q_1), x_1 \to p_1'$

By inference rules this is equivalent to

$\exists \in (p'_1+\emptyset, q'_1+\emptyset), q_1+\emptyset \to y'_1+\emptyset \text{ or } \exists x_1+\emptyset \in (p_1+\emptyset, q_1+\emptyset), x_1+\emptyset \to p'_1+\emptyset$

This concludes the case Then, remarking that in the remaining case, (⊥, q) ≺ (p', ⊤) is equivalent to (⊥+Ø, q) ≺ (p', ⊤+Ø) we conclude the case

- v = Ø+v₂, v₂ < ⊤. Symmetric to the case above.

- v = ⊤+Ø or v = Ø+⊤. Remarking that this implies u' = ⊤ it becomes dual to the case v = ⊥

• P = Q*. By remarking that the set of positions of Q* is the same as the set of positions of an infinite sequence of Q; Q; Q;···, we can treat this case in much the same way as the case P = P₁; P₂.

• P = P₁‖P₂ Remarking that (p₁‖p₂, q₁‖q₂) = (p₁, q₁) × (p₂, q₂), we have that

$$ (p_1 \parallel p_2, q_1 \parallel q_2) \triangleleft (p'_1 \parallel p'_2, q'_1 \parallel q'_2) \iff (p_1, q_1) \triangleleft (p'_1, q'_1) \text{ and } (p'_2, q'_2) \triangleleft (p'_2, q'_2) $$

We can directly apply the induction hypothesis, which concludes the case.

□

Remark 3.3.26. One way of checking the conditions of Proposition 3.3.25 is to check that

$$ [(p, y') | q \to y'] \cap \{(p', q')\} \cup [(p, q) | (x, q') | x \to p'] \neq \emptyset $$

The set {x | p → x} can be computed very easily using Definition 3.3.1.

Thus, we have shown that the algorithm is effectively implementable. Our implemen-
tation of this algorithm in the tool “Sparkling” can be found at [42]. This implementation
was done in Ocaml to fully maximize the use of the inductive structure of our positions.
In the Fig. 3.1 below, we can see the result given by the tool for the Swiss Cross from
previous examples. Many more examples of code are given in the tool, such as the floating
square and more complex programs such as a conservative version of the producer/con-
sumer problem [14, Section 4.1].

For now the tool doesn't explicitly give the intermediate partition in output, but does
compute it to calculate the possible deadlocks. For programs with loops, cubes whose
endpoints only differ by the iteration of the loop have been regrouped, replacing the loop
number by *.
Sparkling

Online demonstration of computations on syntactic regions of programs (the results you see below are computed by your browser). The
source code of this program is available on the dedicated github repository.

<figure><img src="image_143.png" /><figcaption>Figure 3.1: Sparkling tool running on the Swiss Cross</figcaption></figure>
*Example 3.3.27.* Let us look at the results of our tool Sparkling on the Swiss Cross $P = P_a; P_b; V_b; V_a \parallel P_b; P_a; V_a; V_b$ in more details. Its syntactic semantics is given below, where the notations of positions have been simplified to ease presentation. The forbidden regions in grey, is computed by looking at conflicts on the resources, giving us the two cubes below.

<figure><img src="image_144.png" /></figure>

Then, the maximal cubes of the authorized region are given by Sparkling:

<table><tr><td>⊥</td><td>-</td><td>((□;⊥;_;_)||(□;⊥;_;_))</td></tr><tr><td>(⊥||(□;□;T;_))</td><td>-</td><td>((□;⊥;_;_)||T)</td></tr><tr><td>((□;□;T;_)||⊥)</td><td>-</td><td>□;□;(T||(□;⊥;_;_))</td></tr><tr><td>((□;□;T;_)||(□;□;T;_))</td><td>-</td><td>T</td></tr></table>

These correspond to the maximal cubes in the semantics below on the left. The tool also outputs the cubes

<table><tr><td>⊥</td><td>-</td><td>(T||(⊥;_;_;_))</td><td>⊥</td><td>-</td><td>((⊥;_;_;_)||T)</td></tr><tr><td>(⊥||(□;□;□;T))</td><td>-</td><td>T</td><td>((□;□;□;T)||⊥)</td><td>-</td><td>T</td></tr></table>

with each column corresponding respectively to the middle and right cubes on the semantics below.

<figure><img src="image_145.png" /></figure>

We removed the first instructions □;□ in the positions. These correspond to the declaration of mutex, which for now are in the program in input, and clutters notations without changing the structure of the program.
### 3.3.2.3 Limitations

We chose to unfold all the loops in our model in the hope of dealing with programs with loops more easily. Although it is true that this allows to implement the algorithm on some program with loops, the only actual programs we can analyse are programs where, for each loop, the positions corresponding to a loop is either totally inside or totally outside the forbidden region. But this falls apart as soon as the forbidden region does not strictly contain the loops as seen in the Example 3.3.28 below. This is due to the fact that our algorithm only works when working with finite regions, and in such programs, the (normal form of the) forbidden region is infinite.

*Example 3.3.28.* Let us consider the looped Swiss Cross $(P_a; P_b; V_b; V_a)^* \parallel (P_b; P_a; V_a; V_b)$, a representation of its state space is given below and extends infinitely on the right. We can see that there will be an infinite number of cubes needed to cover the forbidden region (as well as the authorized).

<figure><img src="image_146.png" /></figure>

But looking more closely at the Example 3.3.28, we can see that the cubes from the forbidden and allowed regions are all iterations, of cubes of the loop “unfolded” only twice. For example, let us examine the cubes in between the loops in the Example 3.3.28 above. They are represented in the upper figure, and below is the 2-unfolding of the program.

<figure><img src="image_147.png" /></figure>

These notions are not new and have already been talked about in [17], where instead of unfolding loops an infinite amount of time as we did, the authors prove that this can be done in a finite number of unfolding. Thus, in the next chapter, we will try to see if we can use these notions to apply our algorithm to programs with loops in our model.
# Chapter 4

## Handling programs with loops

> "We dug for months, years — an eternity. And we were rewarded with madness."

> — Darkest Dungeon

The deadlock detection algorithm we introduced in Section 1.4.3 and Section 3.3.2 only works for programs without loops, or only when the forbidden region does not exist within the loops. In theory, we could unfold loops an infinite number of times, using the contextual equivalence from Remark 1.1.26, but this would not be satisfactory for practical applications.

In [17] it is shown that we can unfold loops a finite number of time and still keep the main properties of our state space. For example, if there is a deadlock in our base program, it will be found in a finite unfolding of our program.

These deadlocks can be found using a different deadlock detection algorithm than the one presented in Algorithm 1.4.33 that was introduced in [19], which was adapted to work even in the presence of loops in [17] using this finite unfolding. This algorithm works by computing intersections of maximal cubes of the cover of the forbidden region. Unfortunately, the size of the forbidden region grows in $O(k^n)$ where $k$ is the number of unfolding done and $n$ the number of parallel loops being unfolded.

Thus, keeping the number of unfolding to a minimum is crucial. For deadlock detection this is not a problem as a single unfolding suffice, but for other tasks, such as detecting the doomed region, only an upper bound is given in [17], which can get quite large.

Here, we improve upon their result, by showing that, for unsafe and doomed regions, unfolding only twice is always enough, thus resulting in much faster computations in theory. This necessitates the use of the slightly less efficient Algorithm 1.4.33 for detecting deadlocks on the unfolding. This was done to exhibit a closer connection between the two state spaces, showing that the unfolding can be done not only pointwise but can also be done by lifting the maximal covers of our regions.

We start this chapter by presenting the Algorithm 4.1.6 from [19] and the follow-up work [17] for deadlock detection in programs with loops using the unfolding.

Then we modify our syntactic model of programs from Chapter 3, folding back the loops. We also redefine a notion of syntactic cubes that works in our new semantics
(which are now pre-ordered sets instead of partial orders), and define the 2-unfolding of a semantic program.

Next, we prove that, the covers of the forbidden and authorized regions of conservative programs lifts from the base program to the unfolding and project back onto the correct regions.

Finally, we prove that applying a slightly modified version of Algorithm 3.3.23 to the unfolding of a program allows us to detect deadlocks, unsafe and doomed regions in the base program.

## 4.1 Finite unfolding of concurrent programs

### 4.1.1 Finite unfolding techniques in directed models

#### 4.1.1.1 A second deadlock detection algorithm

In this section, we present another algorithm for deadlock detection in loop-free concurrent programs introduced in [19], following the more recent description from [18]. This algorithm uses the forbidden region (more precisely its cubical cover) instead of the geometric semantics of the program. In most cases, the forbidden region of a concurrent program (especially program with mutexes only) is much smaller (in terms of size of the cubical cover) than the geometric semantics of the program.

The algorithm only works for spaces which verifies the *genericity* condition of Definition 4.1.1 below, which is always satisfied by the forbidden regions (more precisely the maximal cubical cover of the forbidden region) of a concurrent program.

**Definition 4.1.1.** Let $R = \{R^1, \dots, R^m\}$ be the cubical cover of a directed space $X$, such that $R^j = \bigcap_{i \le n} [x_i^j, y_i^j]$ for $j \le m$. Then, $R$ is *generic* when for each $j \ne k$, $R^j \cap R^k = \emptyset$ implies $x_i^j \ne x_i^k$ for all $i \le n$.

Indeed, for a program with mutexes, the lower corner of cubes of the forbidden region will always correspond to the concurrent locking of a certain mutex in the corresponding projection (i.e. process) of the program. So, the fact that cubes share this coordinate implies that both process lock the same mutex. Then the upper corners of the cubes correspond to the instant where the mutex is released, meaning that both end at the same point, which would imply that one is included in the other as in Example 4.1.2. Of course, if their intersection is empty, then this is not a problem (as shown in Example 4.1.3), as it is possible of locking, unlocking and then locking again the resource.

*Example 4.1.2.* Let us consider the following d-space, consisting of $\vec{I} \setminus (R^1 \cup R^2)$ where $R^1 \cup R^2$ is the greyed region below, consisting of the 2 maximal dotted cubes. Then, the point $z$ is the lower bound of an intersection of cubes, but is not a deadlock.

<figure><img src="image_148.png" /></figure>
*Example 4.1.3.* Of course, this condition does not apply when the two cubes are disjoint, as it is possible for a program to lock and release the same mutex multiple times. For example, one could take the program $P_a; V_a; P_a; V_a \parallel P_a; V_a$ whose semantics is given below:

<figure><img src="image_149.png" /></figure>

In the case of generic spaces, all deadlocks can be found as the lower bounds of the intersection $\bigcap_{i \le n} R^i$ of $n$ cubes $R_i$ of the forbidden region, where $n$ is the number of processes running in parallel in the program. Since the genericity condition above guarantees that cubes of the forbidden region do not share any coordinates if their intersection is non-empty, if we consider the lower bound of the resulting intersection, the progression of any execution from this point is blocked by exactly one cube in each direction.

*Example 4.1.4.* Let us consider the Swiss Cross program from Example 1.3.51. As there are two cubes $R^1, R^2$ in the maximal cover of the forbidden region, the only possible intersection of two cubes has the point $z$ as lower bound. In executions from this point, the cube $R^1$ prevents progression along the vertical axis and $R^2$ along the horizontal axis:

<figure><img src="image_150.png" /></figure>

Computing deadlocks this way might give points that are not inside the state space as in Example 4.1.5. Thus, for each of the points obtained this way, we need to check if it is at the border of the forbidden region in order to really be considered a deadlock.

*Example 4.1.5.* Consider the program $(P_a; P_b; P_c; V_c; V_b; V_a) \parallel (P_c; P_b; P_a; V_a; V_b; V_c)$, whose geometric semantics is given below. The lower bound of the intersection of the two dotted maximal cubes is inside the forbidden region, thus it should not be considered a deadlock.
<figure><img src="image_151.png" /></figure>

This gives us the following algorithm for detecting deadlocks ([18, Algorithm 5.13]).

**Algorithm 4.1.6.** For $X$ a generic $d$-space of dimension $n$, and a maximal cubical cover of its forbidden region $R = \{R^1, \dots, R^m\}$ of cardinal $m$, where $R^{j_k} = \prod_{i \le n} [x_i^{j_k}, y_i^{j_k}]$. The deadlocks can be found as follows.

1. Take an intersection of $n$ distinct cubes $R^{j_1}, \dots, R^{j_n}$ such that $\bigcap_{k \le n} R^{j_k} \ne \emptyset$.

2. Take $z$ such that $z_i = \max\{x_i^{j_k} | k \le n\}$ (the lower bound of their intersection).

3. If for all $k \le m$, $z \notin R^k$ then $z$ is a “deadlock”.

We refer to Example 4.1.4 for a quick illustration of this algorithm.

*Remark 4.1.7.* What this algorithm really detects is points without future, but these are not necessarily reachable (even when considering non-deterministic branchings). This does also affect the unsafe and doomed regions and is particularly important in programs with loops where reachability is harder to analyze, as illustrated below in Example 4.1.18. Even in programs without loops accessibility of a given point is not easily computed.

In order to find the doomed region, we can extend this and use a similar argument. Indeed, for each deadlock $z$, as long as a point is in the past along at least one coordinate $i$ of the lower corner of a forbidden cube that is itself lower than $z_i$, there is a path going “below” that cube (otherwise, it would contradict the maximality of the cubes). And conversely, if a point is in between $z_i$ and all other cubes’ lower corner alongside $i$ for each coordinate, it is easy to see that all paths lead to the deadlock $z$ eventually. Once again we refer to [18, Theorem 5.11] for a more detailed proof.

*Example 4.1.8.* Consider the Swiss Cross from Example 4.1.4, with the singular deadlock $z$. It is easy to see that any point below the dashed line (representing the past of the lower corner of a cube of the forbidden region) is not doomed. Conversely, points in the past of $z$ above both dashed line and on the right of the dotted line are doomed.
<figure><img src="image_152.png" /></figure>

Then we can compute the doomed region with the following algorithm ([18, Algorithm 5.14]) by applying this method recursively (removing the cubes of the “doomed” regions to the state space and iterating until we reach a fixed point).

**Algorithm 4.1.9.** For X a generic d-space of dimension n, as defined in 4.1.1, and a maximal cubical cover $R = \{R^1, \dots, R^m\}$ of its forbidden region of cardinal m where $R^j = \prod_{i \le n} [x_i^j, y_i^j]$, the doomed region can be found as follows.

1. Compute all deadlocks $z^1, \dots, z^p$ using Algorithm 4.1.6.

2. For each deadlock $z_k$, compute $u^k$ where $u_i^k = \max\{x_i^j | j \le m, x_i^j \ne z_i^k\}$ for all $i \le n$.

3. Add all cubes $[u_k, z_k]$ to the doomed region.

4. Add all cubes $[u_k, z_k]$ to the forbidden region and reiterate the algorithm until no new cubes are found.

*Example 4.1.10.* Let us consider the following program

$$P = (P_a; P_b; V_a; P_c; V_c; V_b) \parallel (P_c; P_a; V_a; P_b; V_b; V_c)$$

At first there is a single deadlock z, the first round of the algorithm gives us the first part of the doomed region, represented in the middle figure. Adding this new cube to the forbidden region, we get a new “deadlock” z', which generates a new cube of the doomed region. As no more deadlocks exist, the algorithm terminates.

<figure><img src="image_153.png" /></figure>
*Remark 4.1.11.* Unfortunately, this description of the doomed region is flawed: it might intersect the forbidden region as shown in Example 4.1.10, which requires a lot more work to get the correct cubical covering for later uses.

The deadlock detection also works in the case of loops contrary to the previous one, but this simple algorithm fails for the unsafe and doomed regions in the case of programs with even non-nested loops. In [17], a method is proposed to extend this algorithm to programs with loops.

### 4.1.1.2 Unfolding loops in programs

In [17], Fajstrup defines the *unfolding* of programs with loops. In this section we will present a slightly adapted version of her work, fitted to our previous notation. We only define unfolding for processes of the form $P; L^*; Q$ where $P, Q, L$ are sequences of instructions (without branchings or loops), but this method extends to multiple loops and even nested loops.

**Definition 4.1.12.** Let $P$ be a process in a concurrent simple program of the form $L^*$. We define the $k$-unfolding of $P$, $U_k(P)$ as the program where $L^*$ has been replaced by the sequential composition of $k$ copies of $L$ sequentially composed:

$$ U_k(P; L^*; Q) = P; \underbrace{L; \dots; L}_{k \text{ times}}; Q $$

*Remark 4.1.13.* The unfolding $U_-(\cdot)$ easily extends to the case where there are multiple loops, with the possibility of giving a different index (number of delooping) for each loop. It can also be extended to deal with nested loops by applying it recursively, with sets of indexes to capture the nested loops. This fundamentally does not change the core interest of the method, whose presentation we want to keep simple.

We recall that the geometric semantics of $L^*$ is obtained by identifying the initial and terminal point of the geometric realization of $L$ (with the associated quotient topology), and that the sequential composition of two process corresponds to identifying the endpoint of the geometric realization of the first with the starting point of the second.

*Example 4.1.14.* For a process of the form $P; L^*; Q$, the geometric semantics will be equivalent to the space on the left. Then, its 2-unfolding will be equivalent to the space on the right.

<figure><img src="image_154.png" /></figure>

Furthermore, all copies of $L$ and their geometric realization can be naturally projected onto the geometric realization of $L^*$ as previously mentioned by identifying the endpoints. This means we can define a projection from an unfolding to the original program.
**Definition 4.1.15.** Let $X$ the geometric realization of a program $P; L^*; Q$ and $X_k$ the geometric realization of its $k$-unlooping $\mathcal{U}_k(P; L^*; Q)$. The projection $\pi_k: X_k \to X$ is given by identifying all $k$ copies of $L$ and identifying their endpoints.

This system of projections verifies some nice properties: it sends the forbidden region of the unfolding onto the forbidden region of the base program [17, Lemma 4.7] and lifts dipaths of the base program to a path in one of the $k$-unlooping [17, Lemma 4.5] but most notably, as consequence of these properties, it sends the deadlocks of the unfolding onto deadlocks of the base. Again, the method finds all points with no future without care for reachability.

**Proposition 4.1.16 ([17, Lemma 4.12])**. A point $p \in X$ is a deadlock if and only if all points $x \in \pi_1^{-1}(p)$, $x$ are deadlocks in the 1-unfolding $X_1$ (Definition 4.1.15).

Then to find the deadlocks in a program with loops, we can simply unfold once and apply the deadlock detection Algorithm 4.1.6 to the unfolding. Then the projection will give back all deadlocks in the original program.

**Algorithm 4.1.17.** Given a program $P = P_1 \| \dots \| P_n$ with each $P_i$ a sequential process without branchings and possibly containing loops, the deadlocks of $P$ can be found by the following algorithm:

1. Calculate the 1-unfolding $\mathcal{U}_1(P_i)$ of $P_i$ for $i \le n$

2. Apply Algorithm 4.1.6 to $\mathcal{U}_1(P_1) \| \dots \| \mathcal{U}_1(P_n)$ to get the set of $z_1, \dots, z_m$ deadlocks of $\mathcal{U}_1(P_1) \| \dots \| \mathcal{U}_1(P_n)$.

3. Obtain the deadlocks of $P$ as $\pi_1(z_1), \dots, \pi_1(z_m)$.

To detect the doomed regions, a similar method can be used by applying Algorithm 4.1.9 to the unfolding, but in this case, a simple 1-unlooping might not suffice as shown in Example 4.1.18. Thankfully, it is shown in [17, Theorem 6.9] that the number of times one need to unfold is finitely bounded in the number of maximal cubes of the original program. Intuitively, this bound corresponds to the greatest number of iteration of the loop a path from a point has to go through before being able to exit the loop.

**Example 4.1.18.** Consider the conservative program $P_1 \| P_2$ with

$$P_1 = (P_a; P_b); L^*; (P_c; V_c) \qquad L = V_b; P_b; V_a; P_a$$

$$P_2 = P_c; P_a; V_a; P_b; V_b; V_c$$

Then if we look at the different successive unfolding of $P_1 \| P_2$, we get the following doomed regions. We see that it actually takes three iterations to find that no parts of the loop $L$ are doomed.

<figure><img src="image_155.png" /></figure>