# Syntactic Regions for Concurrent Programs

Samuel Mimram, Aly-Bora Ulusoy

► To cite this version:

Samuel Mimram, Aly-Bora Ulusoy. Syntactic Regions for Concurrent Programs. Proceedings 37th Conference on Mathematical Foundations of Programming Semantics, MFPS 2021, Aug 2021, Salzburg, Austria. pp.184-199, 10.4204/EPTCS.351.12. [https://hal.science/hal-04244384v1](https://hal.science/hal-04244384v1)

HAL Id: hal-04244384

[https://hal.science/hal-04244384v1](https://hal.science/hal-04244384v1)

Submitted on 16 Oct 2023

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

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

Distributed under a Creative Commons CC BY 4.0 - Attribution - International License
Replace this file with `prentcsmacro.sty` for your meeting, or with `entcsmacro.sty` for your meeting.
Both can be found through links on the ENTCS Web Page.

# Syntactic regions for concurrent programs

Samuel Mimram Aly-Bora Ulusoy

École polytechnique, France

## Abstract

In order to gain a better understanding of the state space of programs, with the aim of making their verification more tractable, models based on directed topological spaces have been introduced, allowing to take in account equivalence between execution traces, as well as translate features of the execution (such as the presence of deadlocks) into geometrical situations. In this context, many algorithms were introduced, based on a description of the geometrical models as regions consisting of unions of rectangles. We explain here that these constructions can actually be performed directly on the syntax of programs, thus resulting in representations which are more natural and easier to implement. In order to do so, we start from the observation that positions in a program can be described as partial explorations of the program. The operational semantics induces a partial order on positions, and regions can be defined as formal unions of intervals in the resulting poset. We then study the structure of such regions and show that, under reasonable conditions, they form a boolean algebra and admit a representation in normal form (which corresponds to covering a space by maximal intervals), thus supporting the constructions needed for the purpose of studying programs. All the operations involved here are given explicit algorithmic descriptions.

**Keywords:** concurrent programming, geometric semantics, state space

## 1 Introduction

The verification of concurrent programs is notoriously complicated because of the combinatorics involved when performing a naive transposition of the techniques available for sequential programs. Namely, for a program consisting of multiple processes running in parallel, we have to make sure that no problem can arise for whichever respective scheduling of the processes, and the number of resulting execution traces to check is in general exponential in the size of the original program: this is sometimes called the “state-space explosion problem”. Moreover, some errors such as the presence of deadlocks are specific to concurrent programs and are not addressed by traditional techniques. In order to tackle these issues, starting in the 90s, a series of theoretical and practical tools have been introduced based on the *geometric semantics* of concurrent programs [10,11,7,6,4], which assigns to each such program a topological space, such that the possible states of the program can be interpreted as points in this space and an execution as a path which is *directed*, i.e. intuitively respects the direction of time. An important observation is that, in those semantics, two paths which are dihomotopic (can be continuously deformed one to the other while respecting the direction of time) correspond to executions which are equivalent from an operational point of view, and we can thus hope to reduce the state space of the program by considering paths up to dihomotopy. This approach is obviously inspired by the one taken in the algebraic study of spaces (which considers algebraic constructions which are invariant up to homotopy, such as the fundamental and higher homotopy groups), although the situation for programs is made more difficult because one has to take the direction of time in account.

While we believe that this line of research is conceptually enlightening and is very fruitful, the fact that one has to resort to topological spaces in order to study discrete structures such as the ones offered by programs is quite puzzling and it is natural to wonder if the topology is really necessary here. It turns out that it is not, and one of the main goals of this paper is to translate into purely combinatorial terms an important algorithmic construction in geometric semantics: the one of *cubical regions*. We refer the reader to [6, Chapter 5] for a detailed presentation but, roughly, it consists in describing the geometric semantics by covering it with cubes: in such a cube, any two paths are homotopic, and it is thus enough to check only one path in order to perform verification. The starting point of this paper consists in considering that an execution of a program consists in
a partial exploration of a “prefix” of this program, that we call here a *position* (on the logical side, similar ideas have been advocated by Girard when defining ludics [8]). A “portion” of the program can then be identified by an interval of positions, which plays the role of the cubes above: it denotes all the positions where we have explored more than the first and less than the second. We can finally reach a convenient description of regions in the program by taking finite unions of such intervals, that we call here *syntactic regions*. We formally define those here and study their properties. Given a set of positions, there are in general multiple regions which describe this set of positions: we show that, under mild assumptions, there is always a canonical region describing a set of positions, the *normal region*, which is in some sense the most economical way of describing it. Moreover, we show that such regions form a boolean algebra (Theorem 6.5) and provide explicit ways of computing corresponding canonical operations (union, intersection, complement) on syntactic regions, which is useful in practice. Typically, we can compute a representation of the state space of a concurrent program by first computing the region which is forbidden because of the use of mutual exclusion primitives, and then compute the state space as the complement of this region, on which we can use the traditional techniques mentioned above.

In addition to providing us with a better understanding of the “geometry of programs”, the aim of the techniques developed is to reduce the size of the state space in order to perform program verification, in a similar vein as partial order reduction (por) [9]. A detailed comparison between the two has been performed both from a practical point of view [5] and a theoretical one [12]: while the two techniques perform similarly on basic examples, geometric techniques sometimes outperform por. Our approach aims at being fully automated and is thus less powerful than techniques based on logic, where some user input or annotations are required (such as the Owicki-Gries method [16], rely/guarantee rules [1], concurrent separation logic [15], etc.). The effectiveness of our approach, which is simpler and easier to implement than previous ones, is illustrated with the online prototype [14], where concrete examples of programs on which it applies are provided (typically, producer-consumer algorithms).

We begin by introducing the programming language considered here as well as an original notion of position on its programs in Section 2, we then define the state space of concurrent programs in Section 3 and explain how it can be described using geometrical regions in Section 4. We generalize the notion of region to arbitrary posets in Section 5, characterize when regions in normal forms have a structure of boolean algebra in Section 6 and finally provide explicit constructions for regions coming from programs in Section 7.

## 2 Concurrent programs and their positions

In order to abstract away from practical details, we introduce here a simple concurrent imperative programming language. We will only be interested in the control-flow structure and thus the operations we use are not relevant for our matters: we simply suppose fixed a set $A = \{A, B, \dots\}$ of actions, which can be thought of as the effectful operations of our language, such as modifying a variable or printing a result. The present work would extend to more realistic languages without any difficulty directly related to the main points raised here.

**Definition 2.1** The collection of programs $P$ is generated by the following grammar:

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

A program is thus either an action $A$, or a sequential composition $P;Q$ of two programs $P$ and $Q$, or a conditional branching $P+Q$ which will execute either $P$ or $Q$, or a conditional loop $P^*$ which will execute $P$ a given number of times, or the execution $P \parallel Q$ of two subprograms $P$ and $Q$ in parallel. 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.

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

**Definition 2.2** 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+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+q$) and we are executing two programs in parallel ($p \parallel q$). 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 positions which are valid 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 position
of the form $p;q$ with $q \neq \perp$ is valid only when $p$ is $\top$. Similarly, in a conditional branching $P+Q$, we cannot execute both subprograms: a position $p+q$ is valid only when either $p$ or $q$ is $\perp$.

**Definition 2.3** We write $P \models p$ to indicate that a pre-position $p$ is a (valid) *position* of a program $P$, this predicate being defined inductively by the following rules:

$$ \begin{array}{ccc} \overline{P \models \perp} & \frac{P \models p}{P;Q \models p;\perp} & \frac{P \models p}{P+Q \models p+\perp} \\ \overline{P \models \top} & \frac{Q \models q}{P;Q \models \top;q} & \frac{Q \models q}{P+Q \models \top+q} \\ & & \frac{P \models p \quad Q \models q}{P \parallel Q \models p \parallel q} \end{array} $$

We write $\mathcal{P}(P)$ for the set of positions of a program $P$.

We can assimilate a position in a program to a possible state during its execution. With this point of view in mind, we can formalize the operational semantics of our programming language as a relation $P \models p \to p'$, which can be read as the fact that, in the position $p$, the program $P$ can reduce in one step and reach the position $p'$.

**Definition 2.4** The *reduction relation* is defined inductively by

$$ \begin{array}{cccc} \overline{A \models \perp \to \top} & & & \\ \overline{P;Q \models \perp \to \perp;\perp} & \overline{P+Q \models \perp \to \perp+\perp} & \overline{P^* \models \perp \to \perp^0} & \overline{P \parallel Q \models \perp \to \perp \parallel \perp} \\ \frac{P \models p \to p'}{P;Q \models p;\perp \to p';\perp} & \frac{P \models p \to p'}{P+Q \models p+\perp \to p'+\perp} & \frac{P \models p \to p'}{P^* \models p^n \to p'^n} & \frac{P \models p \to p' \quad Q \models q}{P \parallel Q \models p \parallel q \to p' \parallel q} \\ \frac{Q \models q \to q'}{P;Q \models \top;q \to \top;q'} & \frac{Q \models q \to q'}{P+Q \models \perp+q \to \perp+q'} & \frac{}{P^* \models \top^n \to \perp^{n+1}} & \frac{P \models p \quad Q \models q \to q'}{P \parallel Q \models p \parallel q \to p \parallel q'} \\ \overline{P;Q \models \top;\top \to \top} & \overline{P+Q \models \top+\perp \to \top} & \overline{P^* \models \top^n \to \top} & \overline{P \parallel Q \models \top \parallel \top \to \top} \\ & \overline{P+Q \models \perp+\top \to \top} & \overline{P^* \models \perp \to \top} & \end{array} $$

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 \perp \to \perp;\perp$ 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 upper left rule $A \models \perp \to \top$ which can be interpreted as executing an action $A$.

**Lemma 2.5** If $P \models p \to p'$ holds then both $P \models p$ and $P \models p'$ hold.

Suppose fixed a program $P$. The state space $G_P$ of this program is the graph whose vertices are the positions of $P$ (Definition 2.3) and edges are the reductions (Definition 2.4). An *execution path* of $P$ is a morphism of the free category $G_P^*$ over the graph $G_P$. We write $P \models \pi : p \to^* p'$ (or simply $\pi : p \to^* q$) to indicate that $\pi$ is an execution of $P$ from $p$ to $q$, we write $\pi \cdot \pi'$ for the composition (also called *concatenation*) of two paths $\pi : p \to^* p'$ and $\pi' : p' \to^* p''$, and we write $\varepsilon : p \to^* p$ for the identity execution (also called *empty path*). An execution is *elementary* when it consists of one reduction step. A *global execution* is an execution from $\perp$ and a *total execution* is a global execution to $\top$. We say that an execution $\pi'$ is a *prefix* of an execution $\pi$ when there exists an execution $\pi''$ such that $\pi = \pi' \cdot \pi''$. A position is *reachable* when there exists a global path $\pi : \perp \to^* p$ with this position as target. The following lemma, together with Lemma 2.5, formalizes the fact the notion of validity of Definition 2.3 captures exactly the expected positions.

**Lemma 2.6** Every *position* $p$ of $P$ is reachable.

As customary, we also write $P \models p \to^* p'$ (or sometimes simply $p \to^* p'$) when there exists an execution $P \models \pi : p \to^* p'$: the resulting relation $\to^*$ on positions of $P$ is the reflexive and transitive closure of the reduction relation $\to$. This relation is induced by a partial order relation, as we now explain.
**Definition 2.7** We write $\le$ for the smallest reflexive relation on the positions of P such that

$$ \frac{\begin{array}{c} p \le p' \\ \top \le p \end{array}}{p \le \top} \quad \frac{\begin{array}{c} q \le q' \\ p; q \le p'; q' \\ p \le p' \\ p+q \le p'+q' \end{array}}{\begin{array}{c} q \le q' \\ p \| q \le p' \| q' \\ p' \le p' \end{array}} \quad \frac{\begin{array}{c} p \le p' \\ p \| q \le p' \| q' \end{array}}{p^n \le p'^n} \quad \frac{\begin{array}{c} p \le p' \\ p' \le p' \end{array}}{p^m \le p'^m} $$

for $m < n$.

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

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

**Proposition 2.10** The partial order $\le$ on $P(P)$ is a bounded lattice, with $\top$ and $\bot$ 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+\bot) \lor (p'+\bot) = (p \lor p')+\bot \\ (p \| q) \lor (p' \| q') = (p \lor p') \| (q \lor q') & p^m \lor p'^m = p'^n & (\bot+q) \lor (\bot+q') = \bot+(q \lor q') \\ & & (p+\bot) \lor (\bot+q) = \top \end{array} $$

for $m < n$, and where we suppose $(p, q) \neq (\bot, \bot)$ in the lower right rule. The infimum admits a similar description.

We recall that a poset $(X, \le)$ is a *well-order* when, for every infinite sequence $(x_i)_{i \in \mathbb{N}}$ of elements, there are indices $i < j$ such that $x_i \le x_j$. This is equivalent to requiring that the poset is both well-founded (every infinite decreasing sequence of elements is eventually stationary) and such that every antichain (set of pairwise incomparable elements) is finite. The following will be useful:

**Proposition 2.11** The poset $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 products, coproducts and contain $(\mathbb{N}, \le)$. $\square$

# 3 Concurrent programs with mutexes and their state space

In practice, in order to avoid unspecified behaviors due to concurrency, programs use primitive operations such as mutexes [3] with the aim of preventing that two subprograms access simultaneously to a shared resource such as memory (typically, the result of two concurrent writings at a same memory location is unspecified in many languages). In order to account for this, we suppose fixed a set $M$ of mutexes such that, for every $a \in M$, there are two associated actions $P_a$ and $V_a$ in $\mathcal{A}$, respectively corresponding to taking and releasing the mutex $a$, as defined in [3]. A mutex will be such that it can be taken by at most one subprogram: if another subprogram tries to take an already taken resource, it will be “frozen” until the mutex is available again, i.e. the first subprogram releases the mutex. This description is formalized below on the operational semantics, see also [6, Chapter 3].

The consumption of mutexes by an execution is kept track of by considering functions in $Z^M$ which to every mutex associate the number of times it has been taken or released (where releasing is considered as the opposite of taking). Given two functions $\mu, \mu' \in Z^M$, we write $\mu+\mu'$ for their pointwise sum, i.e. $(\mu+\mu')(a) = \mu(a)+\mu'(a)$ for $a \in M$, and similarly for the opposite $-\mu$ of a function $\mu$. Given $a \in M$, we write $\delta_a \in Z^M$ for the function such that $\delta_a(a) = 1$ and $\delta_b(a) = 0$ for $b \neq a$, we also write $\emptyset$ for the constant function equal to 0.

**Definition 3.1** Given an execution $P \models \pi : p \to^* p'$, we write $[[P \models \pi : p \to^* p')] : M \to Z$ (or sometimes simply $[[\pi]]$) for its consumption of mutexes. This function is defined for elementary executions by

* $[[P_a \models \pi : \bot \to \top]] = \delta_a$, for $a \in M$,

* $[[V_a \models \pi : \bot \to \top]] = -\delta_a$, for $a \in M$,

* for each reduction $\pi$, different from the two above, deduced with a rule of Definition 2.4 with no premise we have $[[\pi]] = \emptyset$,

* for each reduction $\pi$ deduced with a rule of Definition 2.4 with one reduction $\pi'$ as premise, we have $[[\pi]] = [[\pi']]$,
and extended as an action of the category of executions on the monoid of consumptions, i.e. $[[\varepsilon]] = \emptyset$ and $[[\pi \cdot \pi']]] = [[\pi']]] + [[\pi]]$.
**Example 3.2** Writing $\pi$ for any total execution of the program $P_a$; $(P_a \parallel V_b)$, with $a \neq b$, we have $\llbracket \pi \rrbracket(a) = 2$, $\llbracket \pi \rrbracket(b) = -1$ and $\llbracket \pi \rrbracket(c) = 0$ for $c \neq a$ and $c \neq b$.

A global execution $\pi$ is valid when for every prefix $\pi'$ of $\pi$, and any mutex $a \in \mathcal{M}$, we have $0 \le \llbracket \pi' \rrbracket(a) \le 1$. Such an execution is namely compatible with the semantics of mutexes in the sense that

* no mutex is taken twice (without having been released in between),

* no mutex is released without having been taken first.

A program is conservative when any two executions $\pi : p \to^* p'$ and $\pi' : p \to^* p'$ with the same source and the same target have the same resource consumption: $\llbracket \pi \rrbracket = \llbracket \pi' \rrbracket$. In the following, unless otherwise stated, we assume that all the programs we consider are conservative: it is often satisfied in practice and simplifies computations because we can consider validity of positions instead of executions. This assumption is classical in geometric semantics [6] and is based on the observation that the use of mutexes is quite costly (because they restrict parallelism) and therefore usually restricted to small and "local" portions of the code. This is the reason why it is usually satisfied, at least up to simple rewriting of the code (more complex code can also be handled by "duplicating" some of the positions so that the program becomes conservative). This condition can easily be tested as follows.

**Definition 3.3** The consumption of a program $P$ is the partial function $\Delta(P) : \mathcal{M} \to \mathbb{Z}$ defined by induction on $P$ by

$$ \Delta(P_a) = \delta_a \qquad \Delta(V_a) = -\delta_a \qquad \Delta(A) = \underline{0} \qquad \Delta(P;Q) = \Delta(P \parallel Q) = \Delta(P) + \Delta(Q) $$

and

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

Note that, because of the side conditions in the two last cases, $\Delta(P)$ is not always well defined, e.g. for $P_a^*$ or $P_a+P_b$.

**Proposition 3.4** A program $P$ is conservative if and only if $\Delta(P)$ is well-defined and, in this case, we have $\Delta(P) = \llbracket \pi \rrbracket$ for any total execution $\pi$ of $P$.

The above proposition gives a simple criterion to check for conservativity, by induction on programs. It is applicable even when the set $\mathcal{M}$ of mutexes is infinite because it is not difficult to show that, for any program $P$, $\Delta(P)$ is almost everywhere null when defined, i.e. the set $\{a \in \mathcal{M} \mid \Delta(P)(a) \neq 0\}$ is finite, so that the computations on consumption can easily be implemented in practice. For conservative programs, it makes sense to consider the resource consumption at a position (as opposed to along an execution):

**Definition 3.5** Given a conservative program, we define the consumption $\llbracket p \rrbracket : \mathcal{M} \to \mathbb{Z}$ of a position $p$ as $\llbracket p \rrbracket = \llbracket \pi \rrbracket$ for some global path $\pi : \bot \to p$.

This definition makes sense because there is at least one such path $\pi$ by Lemma 2.6 and it does not depend on the choice of the path by the assumption of being conservative. This enables us to characterize valid executions as follows. We say that an execution $\pi : p \to^* p'$ visits a position $q$ when $q$ is the target of some prefix $\pi' : p \to^* q$ of $\pi$. We say that a position $p$ is valid if it satisfies $0 \le \llbracket p \rrbracket(a) \le 1$ for every mutex $a \in \mathcal{M}$.

**Proposition 3.6** A global execution $\pi$ is valid if and only if every position $p$ it visits is valid.

This motivates defining the *pruned state space* $\overline{G}_P$ of $P$ as the subgraph obtained from $G_P$ by removing every edge between invalid vertices, and all vertices whose incident edges have all been removed. Writing $\overline{G}_P^*$ for the free category it generates, which is a subcategory of $G_P^*$, we have

**Proposition 3.7** The morphisms of $\overline{G}_P^*$ are precisely the valid executions of $P$.

# 4 Geometric semantics

We now briefly recall (or rather illustrate) the geometric semantics of concurrent programs, and relate it to the previous point of view on programs. We refer to the textbook [6] as well as [13] for further reference on the subject.
<figure><img src="image_2.png" /><figcaption>Figure 1. Geometric semantics of a simple program.</figcaption></figure>

In order to take a concrete example, we suppose here only that our actions allow for traditional manipulations of variables, and consider the program

$$ (P_a ; P_b ; x := y+1 ; V_b ; V_a) \parallel (P_b ; P_a ; y := x+2 ; V_a ; V_b) $$

consisting of two processes executed in parallel. Here, we should think of *a* and *b* as protecting the variables *x* and *y* respectively: the program applies the discipline that whenever a variable is used, the corresponding mutex is taken beforehand and released afterward, in order to avoid any concurrent access to it. The idea behind geometric semantics is that to such a program we should associate the topological space on the left of Fig. 1, which consists of a square from which the grayed region has been removed (this is called the *forbidden region*). The horizontal axis corresponds to the execution of the first process and the vertical one to the second process (we have indicated the points corresponding to each instruction of the processes in abscissa and ordinate in order to make this clear). A point in this space can thus roughly be assimilated to a position in the program and the grayed removed area corresponds to removing forbidden positions. A (continuous) path in this space is said to be *directed* when it is increasing with respect to each component: such a path corresponds to an execution of the program. We sometimes say a *dipath* for a directed path. For instance, the dotted path on the left of Fig. 1 is directed and corresponds to a total execution where the second process gets wholly executed before the first one does. Finally, two dipaths are *dihomotopic* when the first can be continuously deformed to the second while going through directed paths only. In general, the definition of the geometric semantics is more involved than the above example shows (in particular, the notion of direction is subtle in presence of loops) and is detailed in the aforementioned references.

Let us now mention two main applications of geometric semantics. Firstly, under simple coherence assumptions, it can be shown that two dihomotopic dipaths have the same effect on the state: in order to ensure the absence of errors in a program (e.g. we are never dividing by 0), it is thus sufficient to use traditional techniques (e.g. abstract interpretation [2]) for one representative in each equivalence class. Secondly, it can be helpful to detect problems specific to concurrency in programs. For instance, the black dot in the figure on the left is a point which is not the final point (the upper right one) and is the source of no non-trivial directed path: this indicates the presence of a *deadlock* in the program. Namely, if the first process executes $P_a$ then $P_b$ and the second process executes $P_b$ then $P_a$ the program is locked and cannot proceed any further: the first process is waiting for the second to release the mutex *b* and the second process is waiting for the first to release the mutex *a*.

We do not develop these techniques much further here – they have already been elsewhere – and concentrate on the following question: how can we represent this geometric semantics in practice? For programs consisting of *n* processes in parallel, such as the one above, where each process consists of a sequence of actions, the geometric semantics will be an *n*-dimensional cube from which a finite number of *n*-dimensional cubes have been carved out, forming the forbidden region (more general cases are handled in [13]). For instance, in our example, the forbidden region consists of two cubes as shown in the figure in the middle of Fig. 1. This motivates investigating the notion of (*cubical*) region, which is a portion of the global cube obtained as a finite union of cubes. Interestingly, the geometric semantics, which is the complement of the forbidden region, can also be described as a union of cubes (8 in our example), and is thus a region, as pictured on the right of Fig. 1. In particular, by convexity, any two dipaths with the same endpoints within a cube are dihomotopic, which helps computing representatives in dihomotopy classes.

On Fig. 2, we have figured the state space associated to the above program: (for simplicity, we have omitted some intermediate positions such as $(\perp;\perp)\parallel\perp$, also we have omitted writing “;” in the positions). The dotted edges are those which have to be removed in order to obtain the pruned state space. One can see that, up to some minor details such as the added positions at the beginning and at the end, the pruned graph can
<figure><img src="image_3.png" /><figcaption>Figure 2. State space of a simple program.</figcaption></figure>

be thought of as an “algebraic counterpart” of the geometric semantics, which motivates the investigation of performing the computations directly on this representation, instead of going through an arbitrary encoding into spaces. In particular, we define and study here an abstract axiomatization of regions, which applies to such graphs.

# 5 Regions of posets

In this section we define our representation of the state-space of programs, replacing (maximal) cubical regions in geometric semantics [6] by (normal) *syntactic regions*. We show that, under mild assumptions, these regions satisfy the same fundamental properties as cubical regions (forming a boolean algebra, supporting the existence of canonical representatives, etc.) and provide explicit ways of computing corresponding canonical operations on syntactic regions. To the best of our knowledge all the constructions performed here are new, and based on the original notion of *position* introduced in Section 2.

## 5.1 Intervals

Suppose fixed a poset $(X, \leq)$. An interval $(x, y)$ in this poset is a pair of elements such that $x \leq y$. Given an interval $I = (x, y)$, we write $[I] = [x, y] = \{z \in X \mid x \leq z \leq y\}$ for the set of points it contains, also called its *support*. We write $z \in I$ instead of $z \in [I]$; we have $z \in (x, y)$ iff $x \leq z \leq y$. We also write $I \subseteq J$ instead of $[I] \subseteq [J]$; we have $(x, y) \subseteq J$ iff $x \in J$ and $y \in J$. Finally, we denote by $\mathcal{I}(X)$ the poset of intervals of $X$.

## 5.2 Regions

A region $R$ is a set of intervals: we write $\mathcal{R}(X) = \mathfrak{P}(X \times X)$ for the set of regions of $X$, where $\mathfrak{P}(-)$ denotes the powerset of a given set. A region is *finite* when it consists of a finite number of intervals. The *support* of a region $R$ is the set $[R] = \bigcup_{I \in R} [I]$ of points it contains.

Two regions are *equivalent* when they have the same support. Such regions are different ways of describing the same set of points: in order to be able to correctly manipulate regions, we should be able to decide when two regions are equivalent, and in order to be efficient, we should find the most compact representation of a region in its equivalence class. Intuitively, the “best” region with a given support $Y \subseteq X$ consists of all the maximal intervals (wrt $\subseteq$) contained in $Y$. We will call this region the *normal form* for a region $R$ and say that a region is in normal form when it is equal to its own normal form. In order to formalize this, we introduce the following preorder on regions: we write $\preceq$ for the pre-order on regions in $\mathcal{R}(X)$ defined by

$$R \preceq S \quad \text{iff} \quad \forall I \in R. \exists J \in S. I \subseteq J$$

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

**Lemma 5.1** *The functions $[-] : \mathcal{R}(X) \to \mathfrak{P}(X)$ and $\mathcal{I} : \mathfrak{P}(X) \to \mathcal{R}(X)$ are increasing and $[-]$ is left adjoint to $\mathcal{I}$.*
**Example 5.2** Consider the set $X = [0,1]^2$ equipped with the usual partial order, and consider the three following regions on it, whose support is $X$:

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

$$R_1 = \{[0, \frac{1}{2}] \times [0, 1], [\frac{1}{2}, 1] \times [0, 1]\}$$

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

$$R_2 = \{[0, 1] \times [0, 1]\}$$

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

$$R_3 = R_2 \cup \{[\frac{1}{4}, \frac{3}{4}] \times [\frac{1}{4}, \frac{3}{4}]\}$$

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

In the above example, the region $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, there are many other maximal elements such as $R_3$ (or, in fact, any other region obtained by adding intervals to $R_2$: the relation $\preceq$ is not antisymmetric). This motivates the introduction of the following refined order on regions, which is such that $R_1 < R_3 < R_2$:

**Definition 5.3** We define the relation $\leq$ on $\mathcal{R}(X)$ by $R \leq S$ if and only if $R \preceq S$, and $S \preceq R$ implies $S \subseteq R$ (i.e. every interval of $S$ belongs to $R$).

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

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

We expect that the “best description” of a subset of $X$ by a region is given by a right adjoint $N : \mathfrak{P}(X) \to \mathcal{R}(X)$ to the support function, which to a subset $Y$ of $X$ associates the normal region describing it. Namely, the adjoint functor theorem indicates that if the right adjoint exists it should satisfy

$$N(Y) = \bigvee \{R \in \mathcal{R}(X) \mid [R] \subseteq Y\} \qquad (1)$$

However, such an adjoint is not always well-defined, as illustrated in Example 5.7 below. The normal form of a region $R$ is, when defined, the region $N([R])$, where $N$ is defined by the formula (1) above. We say that a region is normalizable when it admits a normal form, and in normal form when it is further equal to its normal form.

**Lemma 5.6** Given $Y \subseteq X$ such that $N(Y)$ is defined, one has $[N(Y)] = Y$.

**Example 5.7** Consider the set $X = [0,1] \subseteq \mathbb{R}$ equipped with the usual order. We claim that the subset $Y = X \setminus \{1\}$ does not have a normal form. By contradiction, suppose that the region $N(Y)$ is well-defined. By the above Lemma 5.6, $[N(Y)] = Y = [0,1]$. Given $I \in N(Y)$, there exists $\varepsilon, \eta$ with $0 \leq \varepsilon \leq 1 - \eta < 1$ such that $I = [\varepsilon, 1 - \eta]$ and one easily checks that the region $R$ obtained from $N(Y)$ by removing this interval and replacing it by $[0, 1 - \eta/2]$ is such that $[R] = [N(Y)] = Y$ and $N(Y) < R$, contradicting (1). A very similar situation can be observed in the case of programs, by considering the program $P = A^*$ for some action $A$. We write $X = \mathcal{P}(P)$ for its poset of positions:

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

The subset $Y = X \setminus \{\top\}$ does not have a normal form for similar reasons as above.

**Remark 5.8** In order to accommodate with situations such as in previous example, one could think of allowing (semi-)open intervals in addition to closed ones in regions. However, the operations on those quickly become very difficult to handle because it turns out that, in the case of programs of the form $P \parallel Q$, we need to be able to specify whether bounds of intervals are open or not for each component of the parallel composition.

# 6 The boolean algebra of finitely complemented regions

Given a set $Y \subseteq X$, we write $\bar{Y} = X \setminus Y$ for its complement. For practical applications, given a region $R$ in $\mathcal{R}(X)$, we need to be able to compute a region $\bar{R}$ which covers the complement of the region, i.e. a region $\bar{R}$ such that $[\bar{R}] = [\bar{R}]$. Typically, we have explained in Section 3 that the pruned state space is obtained as the complement in the state space of the forbidden region. Moreover, even when the region $R$ is not in normal
form, we are able to compute the region $\overline{R}$ in normal form, which suggests that we should be able to compute the normal form of a region $R$ as $N([R]) = \overline{\overline{R}}$. Performing these computations will also involve computing intersections and unions of regions, so that we will show that – under suitable hypothesis – regions which admit a normal form have the structure of a boolean algebra, providing explicit algorithmic constructions for the corresponding operations. This generalizes the situation considered in [6] (which is limited to regions which are subsets of $\mathbb{R}^n$) and in [13] (which is limited to products of graphs). In order to ensure that our constructions are applicable in practice, we only consider regions 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.

## 6.1 The complement of an interval

We begin by investigating the computation of the region corresponding to the complement of an interval. As an illustration, 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

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

The normal form of its complement is the region

$$ \overline{R} = \{[\perp, y_1], [\perp, y_2], [x_1, \top], [x_2, \top]\} $$

with $\perp = (0, 0)$, $\top = (5, 5)$, $y_1 = (1, 5)$, $y_2 = (5, 1)$, $x_1 = (0, 4)$, $x_2 = (4, 0)$. Here, it should be noted that $\overline{R} = I^\downarrow \cup I^\uparrow$ where $I^\downarrow$ (resp. $I^\uparrow$) is the set of elements of $X$ which are not above $(2, 2)$ (resp. below $(3, 3)$), nor in fact above any element of $I$. Moreover, the points $y_1$ and $y_2$ are the maximal elements of the set $I^\downarrow$ and, similarly, the points $x_1$ and $x_2$ are the minimal element of $I^\uparrow$. We can generalize the situation as follows.

Given a set $Y \subseteq X$, its lower closure $\downarrow Y$ and lower complement $Y^\downarrow$ are respectively the sets

$$ \downarrow Y = \{x \in X \mid \exists y \in Y. x \leq y\} $$

$$ Y^\downarrow = \{x \in X \mid \forall y \in Y. x \not\leq y\} $$

The upper closure $\uparrow Y$ and lower complement $Y^\uparrow$ of $Y$ are defined dually. We write $\max Y$ for the set of maximal elements of $Y$, and $\min Y$ for the set of minimal elements. The set $Y$ is finitely lower generated when there exists a finite set $Y'$ such that $Y = \downarrow Y'$ (the notion of finitely upper generated is defined dually). By extension, we say that an element $x$ of $X$ is finitely lower (resp. upper) generated when $\{x\}$ is.

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

We say that a set $Y \subseteq X$ is finitely lower (resp. upper) complemented when $Y^\downarrow$ (resp. $Y^\uparrow$) is finitely lower (resp. upper) generated. By extension, we say that an element $x$ of $X$ is finitely lower (resp. upper) complemented when $\{x\}$ is. We say that $Y$ is finitely complemented when it is both finitely lower and upper complemented. We can finally characterize intervals which admit a complement in normal form as follows:

**Proposition 6.2** Given a bounded lattice $X$ and $I$ an interval, the region $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^\downarrow)\} \cup \{[x, \top] \mid x \in \min(I^\uparrow)\} $$

## 6.2 The complement of a region

Our aim is now to generalize Proposition 6.2, and characterize normalizable regions (as opposed to intervals) which admit a complement in normal form. The condition which emerged in order to capture such situations is the following one:

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

(i) given a finitely lower complemented element $x \in X$, every element of $\max(\{x\}^\downarrow)$ is finitely upper complemented,
(ii) given a finitely upper complemented element $x \in X$, every element of $\min(\{x\}^\uparrow)$ is finitely lower complemented.

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

We 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 2.11, is a reasonable restriction for the applications we have in mind. We write

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

for the poset (under inclusion) of normal supports (i.e. supports of regions in normal forms, whose complements are also supports of regions in normal forms). Our goal is to show the following theorem:

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

One of the implications is easily shown:

**Proposition 6.6** The left-to-right implication of Theorem 6.5 holds.

**Proof** By contraposition, suppose that $X$ is not finitely complemented. By Remark 6.4, the condition (i) in the Definition 6.3 is always satisfied, and therefore (ii) has to be falsified. This means there exists an upper complemented element $x \in X$ such that there exists an element $y \in \min(\{x\}^\uparrow)$ such that $y$ is not finitely lower generated. We show below that both $[\perp, y]$ and $[\perp, x]$ belong to $\mathcal{N}(X)$. But their intersection is not in $\mathcal{N}(X)$: the set $\mathcal{N}(X)$ is not closed under intersections and thus not a boolean algebra. Namely, an easy computation shows $[\perp, y] \cap [\perp, x] = [y, y]$ and we have that $[y, y] \notin \mathcal{N}(X)$ by Proposition 6.2, because $y$ is not finitely lower complemented.

It remains to be shown that $[\perp, y] \in \mathcal{N}(X)$. Since $y$ is upper complemented and $\perp$ is trivially lower complemented, we have that the interval $I = (\perp, y)$ is finitely complemented (by definition). Writing $R = \{I\}$, the region $R$ is trivially in normal form, and has a complement in normal form by Proposition 6.2, and therefore $I$ belongs to $\mathcal{N}(X)$. The proof that $[\perp, x] \in \mathcal{N}(X)$ is similar. $\square$

We say that a region $R$ is finitely complemented if it contains only intervals whose support is finitely complemented in the sense of Section 6.1. Beware that this definition does not state that the support of the region should be finitely complemented. We write

$$ \mathcal{F}(X) = \{Y \subseteq X \mid Y = [R] \text{ for some finitely complemented region } R\} $$

We also write

$$ \mathcal{R}_{\mathcal{F}}(X) = \{R \in \mathcal{R}(X) \mid R \text{ is finitely complemented}\} $$

so that the elements of $\mathcal{F}(X)$ are the supports of regions in $\mathcal{R}_{\mathcal{F}}(X)$. The plan of our proof for the missing implication of Theorem 6.5 is as follows: we first show that $\mathcal{F}(X)$ forms a boolean algebra by explicitly constructing the required operations on finitely complemented regions (Proposition 6.10) and then show that $\mathcal{F}(X)$ is isomorphic to $\mathcal{N}(X)$ (Proposition 6.11).

In the rest of this section, we suppose that the poset $X$ is finitely complemented. Given two intervals $I = (x, y)$ and $I' = (x', y')$, we write $(x, y) \cap (x', y') = (x \lor x', y \land y')$ for their intersection, which is always their infimum (wrt $\subseteq$ order) when defined (i.e. $x \lor x' \le y \land y'$).

**Definition 6.7** We define the following operations on regions $R, S$ in $\mathcal{R}_{\mathcal{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\}^\downarrow)\} \cup \{(x', \top) \mid x' \in \min(\{y\}^\uparrow)\})$

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

**Proof** The most subtle is intersection. It is shown by proving that finitely lower (resp. upper) complements of elements of $X$ are stable by $\lor$ (resp. $\land$). See Appendix A. $\square$
**Lemma 6.9** The above operations are compatible with the corresponding ones on supports: for regions $R, S \in \mathcal{R}_F(X)$, we have

$$[R \cap_N S] = [R] \cap [S]$$

$$[R \cup_N S] = [R] \cup [S]$$

$$[\overline{R}^N] = [\overline{R}]$$

The finitely complemented regions $\mathcal{R}_F(X)$ thus form a sub-boolean algebra of $\mathfrak{P}(X)$:

**Corollary 6.10** The set $\mathcal{F}(X)$ is a boolean algebra.

**Proposition 6.11** Finitely complemented supports coincide with normal ones, i.e. we have $\mathcal{F}(X) = \mathcal{N}(X)$.

**Proof** $\mathcal{F}(X) \subseteq \mathcal{N}(X)$. Given $Y \in \mathcal{F}(X)$, there exists a region $R \in \mathcal{R}_F(X)$ such that $[R] = Y$. By Lemma 6.8, its complement $\overline{R}^N$ belongs to $\mathcal{R}_F(X)$, since it can be computed using a finite number of unions and intersections of finitely complemented regions. Then, it is easy to prove $\max \overline{R}^N = N([\overline{R}]) = N(\overline{Y})$. Applying this twice gives the normal form of $R$, and thus of $Y$.

$\mathcal{F}(X) \supseteq \mathcal{N}(X)$. Suppose given $Y \in \mathcal{N}(X)$. We are going to show $\overline{Y} \in \mathcal{F}(X)$ and by Proposition 6.11, we will conclude $Y \in \mathcal{F}(X)$. We define an extension $\overline{-}^\infty : \mathcal{R}(X) \to \mathcal{R}(X)$ of $\overline{-}^N$ for regions that are not finitely complemented by

$$\overline{R}^\infty = \bigcap_{(s,t) \in R} \{(\perp, x) \mid x \in s^\downarrow\} \cup_N \{(x, \top) \mid x \in \max t^\uparrow\}$$

and we show that $N(\overline{Y}) \subseteq \overline{N(Y)}^\infty$ and $\overline{N(Y)}^\infty \in \mathcal{R}_F(X)$, by Remark 6.4. Thus $N(\overline{Y}) \in \mathcal{R}_F(X)$, i.e. $\overline{Y} \in \mathcal{F}(X)$ and finally $Y \in \mathcal{F}(X)$. $\square$

We have thus shown the other implication of Theorem 6.5:

**Corollary 6.12** If $X$ is finitely complemented, the set $\mathcal{N}(X)$ is a boolean algebra.

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

# 7 Syntactic regions

In the case of syntactic regions, i.e. regions 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 6.7. Namely,

* the union of regions is immediate to implement,

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

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

Let us detail the last point. Given a position $p$ of a program $P$, we define, by induction on $P$, the following set $\inf_P(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 | p' \in \inf_P(p)\} & \text{if } p \neq \perp \text{ and } q = \perp \\ \{\top; q' | q' \in \inf_Q(q)\} & \text{if } p = \top \text{ and } q \neq \perp \end{cases}$$

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

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

$$\inf_{P \cdot}(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 | p' \in \inf_P(p)\} & \text{if } p \neq \perp \end{cases}$$
**Proposition 7.1** *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>↓</sup>).*

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*↑). We can finally show that the poset of positions of a programs satisfy the conditions of previous section:

**Proposition 7.2** *Given a program P, its poset of positions P(P) is a finitely complemented well-ordered lattice.*

The operations do not in general preserve the property of being normal for regions, but Theorem 6.5 and Proposition 7.2 however ensure that the property of being normalizable is preserved, and the normal form of a region can be computed as follows:

**Proposition 7.3** *With the implementation of operations described above, the normal form of a region *R* is* $N(\bar{R}) = \max(\bar{R})$, *i.e. it can be obtained by computing twice the complement of *R* and only keeping intervals* which are maximal wrt inclusion.

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

**Example 7.4** 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 region *R* and *S* below, the region *R* ∪ *N* *S* is not normal (the normal form is shown on the right):

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

Similarly, with the region *R* and *S* below, the region *R* ∩ *N* *S* is not normal because it contains the interval *I* pictured on the right

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

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

# 8 Future work

A toy implementation of the computations described in this paper can be tested online at [14]. It allows computing the forbidden region, the state space (called there the *fundamental region*) and the deadlocks of a program with loops (we also plan to implement of further analysis of programs, handling values with abstract domains as explained in the introduction). The positions for loops are defined there *without unfolding*: this allows handling the case of forbidden regions within loops, but the theory is more involved (the execution relation on position does not induce a partial order anymore) and left for future work. Various practical examples of concurrent programs are given on the website and the reader is welcome to try out some more of his own. We plan to investigate, in a near future, the investigation of the combination of this approach with abstract interpretation techniques in order to be able to meaningfully handle domains of values. Finally, we also plan to perform a formalization (in Agda) of the theory developed there in order to make sure that no corner case is omitted (as it can be observed in Section 7, the operations are defined by case analysis, requiring to distinguish many possibilities and the situation is even worse in generalizations).
References

[1] Coleman, J. W. and C. B. Jones, *A structural proof of the soundness of rely/guarantee rules*, Journal of Logic and Computation **17** (2007), pp. 807–841.

[2] Cousot, P. and R. Cousot, *Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints*, in: *Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages*, 1977, pp. 238–252.

[3] Dijkstra, E. W., *Solution of a problem in concurrent programming control*, Communications of the ACM **8** (1965), p. 569.

[4] Fajstrup, L., É. Goubault, E. Haucourt, S. Mimram and M. Raussen, *Trace spaces: An efficient new technique for state-space reduction*, in: *European Symposium on Programming*, Springer, 2012, pp. 274–294.

[5] Fajstrup, L., É. Goubault, E. Haucourt, S. Mimram and M. Raussen, *Trace Spaces: An Efficient New Technique for State-Space Reduction*, in: H. Seidl, editor, *Programming Languages and Systems*, Lecture Notes in Computer Science **7211**, Springer Berlin Heidelberg, 2012 p. 274–294.

[6] Fajstrup, L., É. Goubault, E. Haucourt, S. Mimram and M. Raussen, “Directed Algebraic Topology and Concurrency,” Springer International Publishing, 2016.

[7] Fajstrup, L., M. Raußen and É. Goubault, *Algebraic topology and concurrency*, Theoretical Computer Science **357** (2006), pp. 241–278.

[8] Girard, J.-Y., *Locus solum: From the rules of logic to the logic of rules*, Mathematical structures in computer science **11** (2001), p. 301.

[9] Godefroid, P., *Partial-order methods for the verification of concurrent systems - an approach to the state-explosion problem* (1995).

[10] Goubault, É., *Some geometric perspectives in concurrency theory*, Homology, Homotopy and Applications **5** (2003), pp. 95–136.

[11] Goubault, É. and E. Haucourt, *A practical application of geometric semantics to static analysis of concurrent programs*, in: *International Conference on Concurrency Theory*, Springer, 2005, pp. 503–517.

[12] Goubault, É., T. Heindel and S. Mimram, *A geometric view of partial order reduction*, Electronic Notes in Theoretical Computer Science **298** (2013), pp. 179–195.

[13] Haucourt, E., *The geometry of conservative programs*, Mathematical Structures in Computer Science **28** (2018), p. 1723–1769.

[14] Mimram, S. and A.-B. Ulusoy, *Sparkling* (2021), available at https://smimram.github.io/sparkling/.

[15] O'Hearn, P. W., *Resources, concurrency, and local reasoning*, Theoretical computer science **375** (2007), pp. 271–307.

[16] Owicki, S. and D. Gries, *An axiomatic proof technique for parallel programs I*, Acta informatica **6** (1976), pp. 319–340.
A Omitted proofs

**Proof** [Lemma 2.5] 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} $$

$$ \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. □

**Proof** [Lemma 2.6 and Proposition 2.8] We prove by induction on the program $P$ that, given positions $p$ and $p'$ of $P$, having the relation $p \le p'$ is equivalent to having reductions $p \to^* p'$. We suppose that $p$ and $p'$ are both distinct from $\perp$ and $\top$ below (these cases are easily handled separately).

* 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)$. We have $q+r \le r'+r'$ if and only if

* $q \le q'$ and $r = r' = \perp$, or

* $r \le r'$ and $q = q' = \perp$.

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

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

* $Q \parallel R$. Then $p = p \parallel q$ and $p' = q' \parallel r'$ for some $q, q' \in \mathcal{P}(Q)$ and $r, r' \in \mathcal{P}(R)$. By the inference rules of Definition 2.7, we have that $p \parallel q \le q' \parallel r'$ is equivalent to both $q \le q'$ and $r \le 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 \parallel R \models q \parallel r \rightarrow q' \parallel r} $$

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

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

* $Q;R$. Then $p = q;\perp$ or $p = \top; r$, and $p' = q';\perp$ or $p'\top; r'$ for some $q, q' \in \mathcal{P}(Q)$ and $r, r' \in \mathcal{P}(R)$. By the inference rules of Definition 2.7, we simply have to prove that

$$ Q \models q \le q' \text{ and } R \models r \le r' \text{ if and only if } Q;R \models q; \perp \to^* q'; \perp \to^* \top; \perp \to^* \top; r \to^* \top; r' $$

By induction hypothesis $Q \models q \le q'$ and $R \models r \le r'$ is equivalent to $q \to^* q'$ and $r \to^* r'$ which, by the rules

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

$$ \frac{Q \models \top \qquad R \models r \rightarrow r'}{Q; R \models \perp; r \rightarrow \perp; r'} $$

implies $q;\perp \to^* q';\perp$ and $\perp; r \to^* \perp; r'$. By extension (with $q' = \top$ and $r = \perp$), we get the equivalence, by concatenation.

* $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 2.7, 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 \rightarrow q'}{Q^* \models q^n \rightarrow 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 paths :

$$ \frac{Q \models q' \to^* \top}{Q^* \models q^n \to^* \top^n} \qquad \frac{Q \models \bot \to^* \top}{Q^* \models \bot^k \to^* \top^k} \quad \text{for each } k, n \le k \le m \qquad \frac{Q \models \bot \to^* q'}{Q^* \models \bot^m \to^* \to^* q'^m} $$

gives the equivalence.

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

**Proof** [Proposition 2.9] The convexity and transitivity of $\le$ follows, by Proposition 2.8, from the convexity 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$ 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 $\bot$ 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$. Similar as above.

• $R \parallel Q$. Similar as above.

• $Q^*$. The positions are of the form $r^n$ and $q^m$. such that, $r^m \le q^n \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$. □

**Proof** [Proposition 2.10] Let us prove that $\vee$ corresponds to the supremum of both positions.

Given a program $P \models p_1, p_2$, we first remark that by definition, $\top \vee p = \top$ and $\bot \vee p = p$ corresponds to the supremum of the positions. we will thus suppose both $p_1$ and $p_2$ distinct from $\bot$ and $\top$ for the rest of the proof. We prove all other cases by an induction on the program $P$.

• $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 \vee q_2 \ge q_i \text{ and } r_1 \vee r_2 \ge r_i $$

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

$$ q \ge q_1 \vee q_2 \text{ and } r \ge r_1 \vee r_2 $$

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

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

We still need to prove that $P \models (q_1 \vee q_2); (r_1 \vee r_2)$.

• If $q_1 = q_2 = \top$ or $r_1 = r_2 = \bot$ the respective inference rules guarantee that $P \models p_1 \vee p_2$.

• Otherwise, $q_1 = \top$ and $r_2 = \bot$. Then $p_1 \vee p_2 = (\top \vee q_2); (r_1 \vee \bot) = \top; r_1$ and $Q;R \models \top; r_1$ by inference rules.

• $P = Q \parallel R$. Similar as 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 = \bot$. By the inference rules, positions of $P$ comparable with $p_i$ are $p = q+\bot$ with $q$ comparable to $q_i$ or $p = \top$ (not the supremum since $\top+\bot$ is a smaller upper bound). Thus similarly as above, the inference rules implies

$$ \sup(p_1, p_2) = (q_1 \vee q_2)+\bot = (q_1+\bot) \vee (q_2+\bot) $$

• The case where $q_1 = q_2 = \bot$ is similar.
· Otherwise, $p_1 = q_1 \perp \perp, p_2 = \perp \perp r_2$. $q_2 \neq \perp, r_1 \neq \perp$. 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$.

· 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 implies $(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}) $$

□

**Proof** [Proposition 2.11] Given a program $P$. We define $\mathcal{P}(P)^+ = \mathcal{P}(P) \setminus \{\perp, \top\}$. It is much easier to reason inductively on this set of position so we'll 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 antichain 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$. By the inference rules, $\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$. By inference rules, $\mathcal{P}(P)^+ = \mathcal{P}(R) \perp \perp \cup \perp \parallel \mathcal{P}(Q)$ equivalent to $\mathcal{P}(R) \sqcup \mathcal{P}(Q)$ with the canonical disjoint order.

· $P = R; Q$. By the inference rules $\mathcal{P}(P)^+ = (\mathcal{P}(R); \perp) \setminus \{\top; \perp\} \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^*$. By the inference rules, $\mathcal{P}(P)^+ = \{r^n | r \in \mathcal{P}(R), n \in \mathbb{N}\}$ is equivalent to $\mathbb{N} \times \mathcal{P}(R)$ equipped with 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 known to be closed by all the above operations.

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

□

**Proof** [Proposition 3.4] We prove the proposition by induction on the size of the program $P$.

• $P = A$. Trivial

• $P = Q; R$ or $P = Q \parallel R$. A path $\pi$ on $P$ is a concatenation of paths of the following form:

$$ P \models \pi_{\perp} : \perp \to^* \perp; \perp $$

$$ P \models \pi_{\top} : \top; \top \to^* \top $$

$$ P \models \pi_{Q,q,q'} : q; \perp \to^* q'; \perp $$

$$ P \models \pi_{R,r,r'} : \top; r \to^* \top; r' $$

A path $\pi$ on $P = Q \parallel R$ is a concatenation of paths of the following form:

$$ P \models \pi_{\perp} : \perp \to^* \perp; \perp $$

$$ P \models \pi_{\top} : \top \parallel \top \to^* \top $$

$$ P \models \pi_{Q,q,q'} : q \parallel r \to^* q'; \parallel r $$

$$ P \models \pi_{R,r,r'} : q \parallel r \to^* q \parallel r' $$

In both cases, by definition, we have

$$ [[\pi_{\perp}] = [[\pi_{\top}] = 0 $$

$$ [[\pi_{Q,q,q'}] = [[q \to^* q'] $$

$$ [[\pi_{R,r,r'}] = [[r \to^* r'] $$

Thus the program $P$ is conservative if and only if $Q$ and $R$ are. By induction hypothesis, this is equivalent to $\Delta(Q)$ and $\Delta(R)$ being well defined, and by extension $\Delta(P)$ being well-defined. The inference rules for parallel composition show that, by definition, if the explorations of both branches are interleaved, it is similar, in
terms of $[\pi]$, to fully exploring one side before fully exploring the second one. A total execution $P \models \pi$ can thus be divided as such:

$$ \pi = \pi_{\perp} \circ \pi_{Q, \perp, \top} \circ \pi_{R, \perp, \top} \circ \pi_{\top} $$

Thus in both cases

$$ [\pi] = 0 + [[Q \models \perp \rightarrow * \top] + [R \models \perp \rightarrow * \top]] + 0 $$

Thus

$$ [\pi] = \Delta(Q) + \Delta(R) = \Delta(P) $$

by induction hypothesis.

• $P = Q+R$. A path $\pi$ on $P$ is one of the two following concatenations of paths of the following form: either $\pi_Q$ obtained as the concatenation of

$$ P \models \pi_{\perp} : \perp \rightarrow * \perp + \perp $$

$$ P \models \pi_{Q,q,q'} : q + \perp \rightarrow * q' + \perp $$

$$ P \models \pi_{Q,\top} : \top + \perp \rightarrow * \top $$

or $\pi_R$ obtained as the concatenation of

$$ P \models \pi_{\perp} : \perp \rightarrow * \perp + \perp $$

$$ P \models \pi_{R,r,r'} : \perp + r \rightarrow * \perp + r' $$

$$ P \models \pi_{R,\top} : \top + \top \rightarrow * \top $$

By definition, we have

$$ [\pi_R] = \sum_{\pi_{R,r,r'} \in \pi_R} [[R \models r \rightarrow * r'] $$

$$ [\pi_Q] = \sum_{\pi_{R,q,q'} \in \pi_Q} [[R \models q \rightarrow * q'] $$

Thus the $P$ is conservative only if $Q$ and $R$ are. The only cases left for the equivalence are paths that can go by either side of the conditional branching. Typically,

$$ [P \models \perp \rightarrow * \top] = [[R \models \perp \rightarrow * \top] = [[Q \models \perp \rightarrow * \top]] $$

Thus for the equivalence, by induction hypothesis we also require $\Delta(Q) = \Delta(R)$. In that case,

$$ [P \models \perp \rightarrow * \top] = \Delta(Q) = \Delta(R) = \Delta(P) $$

• $P = Q^*$. A path $\pi$ on $P$ is a concatenation of paths of the following forms:

$$ P \models \pi_{\perp} : \perp \rightarrow * \perp^0 $$

$$ P \models \pi_n : \top^n \rightarrow * \perp^{n+1} $$

$$ P \models \pi_{n,q,q'} : q^n \rightarrow * q'^n \perp $$

$$ P \models \pi_{\top} : \top^n \rightarrow * \top $$

By definition, $[\pi_{n,q,q'}]$ is non-zero and depends only on the premise path $[[Q \models q \rightarrow * q']$. Thus, the program $P$ is conservative only if $Q$ is. Furthermore the paths

$$ \pi_0 = \pi_{0,\perp,\top} \circ \pi_{\top} $$

$$ \pi_1 = \pi_{0,\perp,\top} \circ \pi_0 \circ \pi_{1,\perp,\top} \circ \pi_{\top} $$

have same beginning and end. And in that case, by induction hypothesis, $[\pi_0] = \Delta(Q)$ and $[\pi_1] = 2\Delta(Q)$. Thus for $P$ to be conservative, we require also $\Delta(Q) = 0$. In that case we can easily that $P$ is conservative and $\Delta(P) = 0$. $\square$

**Proof** [Proposition 3.6] Consider a global path $P \models \pi : \perp \rightarrow * p$. For every prefix $\pi'$ of $\pi$, we have $P \models \pi' : \perp \rightarrow * p'$. Since $P$ is conservative,

$$ [P \models \pi' : \perp \rightarrow * p'] = [p'] $$

Thus $\pi'$ being valid is equivalent to $p'$ being valid. By definition, prefixes cover exactly all visited positions which implies the equivalence. $\square$

**Proof** [Lemma 5.1] We will prove the existence of an adjunction of posets (called a Galois connection) with $[-]$ the left adjoint to $\mathcal{I}$. First, we prove that both functions are increasing
• Given $R, S \in \mathcal{R}(X)$ such that $R \preceq S$, we have that for every $I \in R$ there exists $J_I \in S$ such that $I \subseteq J_I$, i.e. $[I] \subseteq [J_I]$ and thus

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

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

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

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

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

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

$$R \preceq T$$

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

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

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

**Proof** [Lemma 5.5] Given $R, S \in \mathcal{R}(X)$, such that $R \leq 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]$$

$\square$

**Proof** [Lemma 5.6] Given $Y \subseteq X$ such that $N(Y)$ is defined. The definition of a left adjoint states that for each $R \in \mathcal{R}(X)$, we have $[R] \subseteq Y$ if and only if $R \leq N(Y)$. By reflexivity of $\leq$, $N(Y) \leq N(Y)$ holds, so

$$[N(Y)] \subseteq Y$$

Furthermore $[-]$ increasing implies

$$Y = [\mathcal{I}(Y)] \subseteq [N(Y)]$$

Thus $N(Y) = Y$. $\square$

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

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

Given an element $y \in \max Y \subseteq Y = \downarrow \max G$, there exists $z \in \max G \subseteq Y$ such that $y \leq z$. Maximality wrt inclusion of elements of $\max Y$ implies $z = y$. Thus

$$\max Y \subseteq \max G$$

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

$$\max G \subseteq \max Y$$

Thus $\max Y = \max G$, finite and $\downarrow \max Y = \downarrow \max G = \downarrow G = Y$

$\square$

**Proof** [Proposition 6.2] Suppose given a poset $(X, \leq)$, $I = (s, t)$ an interval of $X$, and consider the region $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 region. We have to show that $I$ is finitely complemented, which means that the lower complement satisfies

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

with $\max(I^{\downarrow})$ 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 6.1, it is enough to show that $I^{\downarrow}$ is finitely generated. We show here that it is generated by the set

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

i.e.

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

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

* $I^{\downarrow} \subseteq \downarrow G$. Suppose given $x \in I^{\downarrow}$. Since $I^{\downarrow}$ is downward closed, we have $(\bot, x) \in \mathcal{I}(I^{\downarrow})$ and

$$ \begin{align*} \mathcal{I}(I^{\downarrow}) &\le \mathcal{I}(\overline{[R]}) && \text{because } I^{\downarrow} \subseteq \overline{[R]} \text{ and } \mathcal{I} \text{ is increasing} \\ &= \mathcal{I}([N(\overline{[R]})]) && \text{by hypothesis} \\ &\le N(\overline{[R]}) && \text{by (1), because } [\mathcal{I}([N(\overline{[R]})])] = [N(\overline{[R]})] = \overline{[R]} \end{align*} $$

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

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

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

$$ \overline{R} = \{[\bot, y] \mid y \in \max(I^{\downarrow})\} \cup \{[x, \top] \mid x \in \min(I^{\uparrow})\} $$

We write

$$ S = \{[\bot, y] \mid y \in \max(I^{\downarrow})\} $$

$$ T = \{[x, \top] \mid x \in \min(I^{\uparrow})\} $$

We first remark that

$$ \overline{[R]} = I^{\downarrow} \cup I^{\uparrow} = [S] \cup [T] = [S \cup T] $$

Namely, we have

$$ \begin{align*} I^{\downarrow} &= \downarrow \max(I^{\downarrow}) && \text{by Lemma 6.1 since } I \text{ supposed to be finitely lower complemented} \\ &= [S] \end{align*} $$

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

* $U \le \overline{R}$. By Lemma 5.1, we have $U \le \mathcal{I}([U]) \le \mathcal{I}(\overline{[R]})$) and it suffices to show that $\mathcal{I}(\overline{[R]}) \le \overline{R}$. We first show that we can express $\mathcal{I}(\overline{[R]}) = \mathcal{I}(\overline{[I]}) = \mathcal{I}(\overline{s, t})$ as

$$ \mathcal{I}(\overline{s, t}) = \mathcal{I}(s^{\downarrow}) \cup \mathcal{I}(t^{\uparrow}) $$
By definition of the complement, we have that $[s, t] = s^\downarrow \cup t^\uparrow$. Therefore,

$$ \begin{aligned} \mathcal{I}(\overline{[I]}) &= \mathcal{I}(I^\downarrow \cup I^\uparrow) \\ &= \mathcal{I}(I^\downarrow) \cup \mathcal{I}(I^\uparrow) \cup \{(a, b) \mid a \in s^\downarrow \setminus t^\uparrow \text{ and } b \in t^\uparrow \setminus s^\downarrow\} \cup \{(a, b) \mid a \in t^\uparrow \setminus s^\downarrow \text{ and } b \in s^\downarrow \setminus t^\uparrow\} \end{aligned} $$

Given $(a, b) \in \{(a, b) \mid a \in s^\downarrow \setminus t^\uparrow \text{ and } b \in t^\uparrow \setminus s^\downarrow\}$, we have $a \le t, s \le b$, thus $a \lor s \le b \land t$, and therefore $[a, b] \cap [s, t] = [a \lor s, b \land t] \ne \emptyset$, and thus $(a, b) \notin \mathcal{I}(\overline{[I]})$. Similarly, we have $\{(a, b) \mid a \in t^\uparrow \setminus s^\downarrow \text{ and } b \in s^\downarrow \setminus t^\uparrow\} \cap \mathcal{I}(\overline{[I]}) = \emptyset$, from which we conclude

$$ \mathcal{I}(\overline{[I]}) = \mathcal{I}(I^\downarrow) \cup \mathcal{I}(I^\uparrow) $$

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

$$ \mathcal{I}(\overline{[R]}) = \mathcal{I}(I^\downarrow) \cup \mathcal{I}(I^\uparrow) \preceq S \cup T = \overline{R} $$

* $\overline{R} \preceq U$ 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^\downarrow$ (indeed $v \ge s$ implies $[I] \cap I \supseteq \{(\perp, v)\} \cap I \ne \emptyset$). Furthermore by definition of $S$, for $v \in I^\downarrow$, there exists $y \in \max I^\downarrow$ such that $(\perp, v) \subseteq (\perp, y)$. Finally $(\perp, y)$ is an interval of $S$, such that

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

By definition of $\max I^\downarrow$ 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$

□

**Proof** [Proposition 6.6] Let us prove the right-to-left implication. We proceed by contraposition. Suppose given a well-ordered bounded lattice $X$ which is not finitely complemented. By Remark 6.4, the condition (i) in the Definition 6.3 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^\uparrow$ 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 6.4, all elements are finitely upper complemented, namely, $s$ and $t$ are both finitely upper complemented.

* Since $\perp^\downarrow = \emptyset$, we deduce that $\perp$ is finitely lower complemented.

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

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

By contraposition, we deduce the desired implication.

The left-to right implication is already proven in Proposition 6.6.

□

**Proof** [Lemma 6.8] 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^\downarrow \cup \max x_S^\downarrow) &= \downarrow \max x_R^\downarrow \cup \downarrow \max x_S^\downarrow \\
&= x_R^\downarrow \cup x_S^\downarrow \tag*{\text{by Lemma 6.1}} \\
&= \{x \in X \mid x \le x_R \text{ or } x \le x_S\} \\
\downarrow (\max x_R^\downarrow \cup \max x_S^\downarrow) &= (x_R \lor x_S)^\downarrow
\end{align*}
$$

By finitude of, $\max x_R^\downarrow$ and $\max x_S^\downarrow$, $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 interval $(x, y) \in R \cap_N S$. By definition, $R \cap_N S \in \mathcal{R}_F(X)$

• $\overline{\cap}^N$. Given $R \in \mathcal{R}_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^\downarrow$ (resp. $x' \in \min y^\uparrow$) are finitely upper (resp. lower) complemented. Thus $(\perp, y')$ and $(x', \top)$ finitely complemented. Furthermore, by definition $\{(\perp, y') \mid y' \in \max x^\downarrow\}$ and $\{(x', \top) \mid x' \in \min y^\uparrow\}$ are finite. Thus by the above proofs, as a result of a finite numbers of operations of union and intersection of elements of $\mathcal{R}_F$, we have $\overline{R}^N \in \mathcal{R}_F(X)$. $\square$

**Proof** [Lemma 6.9] Let $X$ a bounded lattice. Let $R, S \in \mathcal{R}_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}_F(X)$ and $(s, t) \in R$. We have $s$ (resp. $t$) finitely lower (resp. upper) complemented.

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

**Proof** [Proposition 6.11] 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 region $R \in \mathcal{R}_F(X)$, such that $[R] = Y$. Let us prove that $N(\bar{Y}) = \max \bar{R}^N$.
By Eq. (1) it suffices to show that for all regions $S$, such that $[S] \subseteq \bar{Y}$, we have $S \preceq \max \bar{R}^N$. Now suppose
given such a region $S$, we need to prove the following points :

• $S \preceq \max \bar{R}^N$. By Lemma 5.1, $[S] \subseteq \bar{Y}$ implies $S \preceq \mathcal{I}(\bar{Y})$. Furthermore, by finitude $\bar{R}^N \preceq \max \bar{R}^N$. Thus it suffices to show $\mathcal{I}(\bar{Y}) \preceq \bar{R}^N$.
Given $x \in \mathcal{I}(\bar{Y})$, we have $x \in \bigcap_{r \in R} \mathcal{I}(\bar{r})$. By Proposition 6.2, 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{I}(\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 6.9, $\max \bar{R}^N \in \mathcal{R}_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}_F $$

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

Given $Y \in \mathcal{N}(X)$, There exists a region $R \in \mathcal{R}(X)$ such that $[\emptyset|R) = Y$ and $R$ in normal form. By 6.10, it then suffices to show that $\bar{Y} \in \mathcal{R}_F(X)$ i.e. there exists a region $\bar{R} \in \mathcal{R}_F(X)$ such that $[\bar{R}] = \bar{Y}$, namely $N(\bar{Y})$. We first define an extension of $\overline{\phantom{N}}^N: \mathcal{R}(X) \to \mathcal{R}(X)$ to regions 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^{\downarrow}\} \cup_N \{(x, \top) \mid x \in \max t^{\uparrow}\} $$

We prove that for a region in normal form $R$, $N(\overline{[R]}) \subseteq \overline{\bar{R}}^{\infty} \in \mathcal{R}_F(X)$. By the same method as for $\overline{\phantom{N}}^N$ in the proof of Proposition 6.2 and Lemma 6.9 for $R \in \mathcal{R}(X)$ and $r \in R$,

$$ [\bar{R}^{\infty}] = [\overline{[R]}] \text{ and } \mathcal{I}(\bar{r}) \preceq \overline{\{r\}}^{\infty} $$

By Remark 6.4, all elements of $X$ are upper complemented i.e. all intervals $(\perp, x)$ and $(x, \top)$ with $x \in \max t^{\uparrow}$, for $t \in X$ are finitely complemented. Thus for a finite region $R$,

$$ \overline{\bar{R}}^{\infty} \in \mathcal{R}_F(X) $$

Suppose given $Y \in \mathcal{N}(X)$ and $x \in \mathcal{I}(\bar{Y})$, we have $x \in \bigcap_{r \in N(Y)} \mathcal{I}(\bar{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{\bar{N}(Y)}^{\infty}$. Thus,

$$ N(\bar{Y}) \preceq \mathcal{I}(\bar{Y}) \preceq \overline{\bar{N}(Y)}^{\infty} $$

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

**Proof** [Proposition 7.1] Given a program $P$, let us prove that by induction on $x \in \mathcal{P}(P)$, that $\max(x^{\downarrow}) = \inf_P(x)$.

• $x = \perp$. Immediately,

$$ \max(\perp^{\downarrow}) = \emptyset = \inf_P(\perp) $$

• $x = \top$. Let us prove $\max(\top^{\downarrow}) = \inf_P(\top)$ by induction on $P$.

• If $P = Q^*$. We have $\top^{\downarrow} = \{\perp\} \cup \{q^n \mid q \in \mathcal{P}(Q), n \in \mathbb{N}\}$. such that for all $q^n \in \top^{\downarrow}$, $q^n < q^{n+1} \in \top^{\downarrow}$. Thus

$$ \max(\top^{\downarrow}) = \emptyset = \inf_P(\top) $$

• For all other cases, $\top^{\downarrow}$ is trivially generated by the predecessors of $\top$ (e.g. $\top \parallel \top$, $\perp + \top$ and $\top + \perp$ ...).
Thus, $\max(\top) = \inf_P(\top)$.

* $P \models \bot; \bot$, or $P \models \bot^0$ or $P \models \bot \parallel \bot$ or $P \models \bot+\bot$. By the inferences rules

$$ \max(x^{\downarrow}) = \{\bot\} = \inf_P(x) $$

* $Q; R \models y; \bot$, with $y \neq \bot$. We have $y; \bot \in \downarrow\{\top; r \mid R \models r\}$ i.e. $x^{\downarrow} \cap \{\top; r \mid R \models r\} = \emptyset$. Thus

$$ \max x^{\downarrow} = \max\{q; \bot \mid q \not\leq y, Q \models q\} = \{P \models q; \bot \mid q \in \max y^{\downarrow}\} = \{P \models q; \bot \mid q \in \inf_Q(y)\} = \inf_P(x) $$

* $Q; R \models \top; y$ with $y \neq \bot$. We have $\{q; \bot \mid Q \models q\} \subseteq \downarrow\{\top; r \mid R \models r\}$. Thus by inference rules,

$$ \max x^{\downarrow} = \max(x^{\downarrow} \cap \{\top; r \mid R \models r\}) = \{\top; r \mid r \in \max y^{\downarrow}\} = \{\top; r \mid r \in \inf_R(y)\} = \inf_P(x) $$

* $Q \parallel R \models q \parallel r$ with $q \parallel r \neq \bot \parallel \bot$. By the inference rules, $q \parallel r \not\leq u \parallel v$ is equivalent to $r \not\leq v$ or $q \not\leq u$. Thus

$$ \begin{aligned} x^{\downarrow} &= \{P \models u \parallel v \mid q \not\leq u\} \cup \{P \models u \parallel v \mid r \not\leq v\} \\ &= \downarrow\{P \models u \parallel \top \mid u \in q^{\downarrow}\} \cup \downarrow\{P \models \top \parallel v \mid v \in r^{\downarrow}\} \end{aligned} $$

with both sets incomparable. Thus

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

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

• $Q^* \models \bot^n$ with $n > 0$. By the inference rule, $n \leq m$ equivalent to $x = \bot^n \leq q^m$. Thus

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

• $Q^* \models y^n$ with $y \neq \bot$ and $n \neq 0$.

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

$$ \max(x^{\downarrow}) = \max(x^{\downarrow} \cap \{q^n \mid Q \models q\}) = \{q^n \mid q \not\leq y\} = \{q^n \mid q \in \max y^{\downarrow}\} = \{q^n \mid q \in \inf_Q y\} = \inf_P(x) $$

* $P+Q \models q+\bot$. The inference rules give

$$ \begin{aligned} (q+\bot)^{\downarrow} &= \{P \models u+v \mid q \not\leq u \text{ or } \bot \not\leq v\} \cup \{\bot\} \\ &= \{P \models u+\bot \mid q \not\leq u\} \cup \{\bot+\upsilon\} \cup \{\bot\} \\ &= \downarrow\{P \models u+\bot \mid u \in q^{\downarrow}\} \cup \downarrow\{\bot+\top\} \end{aligned} $$

With $\{P \models u+\bot \mid u \in q^{\downarrow}\} \cap \downarrow\{\top+\top\} = \{\bot, \top+\bot\}$ and all other elements incomparable. Thus

$$ \max x^{\downarrow} = \{P \models u+\bot \mid u \in \max q^{\downarrow}\} \cup \{\top+\bot\} = \{P \models u+\bot \mid u \in \inf_Q q\} \cup \{\bot+\top\} = \inf_P(x) $$

* $P+Q \models \bot+\upsilon$. Similarly, $\max(x^{\downarrow}) = \inf_P(x)$.

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

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

**Proof** [Proposition 7.2] 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}{cccc} \overline{Q \vdash q} & \overline{Q \vdash q} & \overline{Q \vdash q} & \overline{Q^* \vdash \top} \\ \underline{Q;R \vdash q;\perp} & \underline{Q+R \vdash q+\perp} & \underline{Q \parallel R \vdash q \parallel r} & \underline{Q^* \vdash \top} \\ \underline{R \vdash r} & \underline{R \vdash r} & \underline{R \vdash r} & \underline{Q \vdash q \quad n \in \mathbb{N}} \\ \underline{Q;R \vdash \top; r} & \underline{Q+R \vdash \perp+\top} & \underline{Q \parallel R \vdash q \parallel r} & \underline{Q^* \vdash q^n} \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^\uparrow)$, 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 = \perp$. This implies $p^\downarrow = \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^\downarrow = \downarrow \top \setminus \{\top\}$

* $P = A$. We have $p^\downarrow = \{\perp\} = \downarrow\{\perp\}$. Thus $P \nvdash p$ and $p$ finitely lower complemented by Lemma 6.1.

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

* $P = Q^*$. Given $x \in \top^\downarrow \setminus \perp = \{q^n \mid n \in \mathbb{N}, Q \vdash q\}$, such that $x = y^n$. By definition, $x < y^{n+1} \in \top^\downarrow$. Thus $\max \top^\downarrow = \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)^\downarrow &= \{y \parallel z \mid y \not\geq q \text{ or } z \not\geq r\} \cup \{\perp\} \\ &= \downarrow(\{y \parallel \top \mid y \not\geq q\} \cup \{\top \parallel z \mid z \not\geq q\}) \\ &= (q \parallel \top)^\downarrow \cup (\top \parallel r)^\downarrow \end{align*} $$

As, $\{y \parallel \top \mid y \not\geq q\}$ and $\{\top \parallel z \mid z \not\geq q\}$ disjoint, $p^\downarrow$ is finitely lower generated if and only if both $(q \parallel \top)^\downarrow$ and $(\top \parallel r)^\downarrow$ 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$. $\square$