- $r \not\to r'$ and

- $\mathbf{colours}(r) \cup \mathbf{colours}(r') \subseteq C$;

$$ \bullet \ \mathbf{end}(\{(i, j), (i', j')\}) = \{i, i'\}. $$

We simply write $\mathfrak{D}[\Phi]$ when links for all colours appearing in $\Phi$ are considered, i.e. when $C = F_+ \uplus F_-$.

§49.11 **Example.** Two examples of dependency graphs for the two constellations $\Phi_N^{n+m}$ and $\Phi_N$ of Example 48.18 are presented in Figure 49.2.

§49.12 **Definition** (Adjacent of a ray). Let $\Phi$ be a constellation and $\mathfrak{D}[\Phi; C] = (V, E, \mathbf{end})$ its dependency graph $w.r.t.$ a set of colours $C \subseteq F_+ \uplus F_-$. The set of rays $\mathbf{adjacent}$ to some given ray index $(i, j)$ of $\Phi$ is defined by:

$$ \mathbf{adj}_{\Phi}^{C}(i, j) := \{(i', j') \mid \exists e \in E, e = \{(i, j), (i', j')\}\}. $$

§49.13 **Definition** (Degree of a ray). Let $\Phi$ be a constellation and $\mathfrak{D}[\Phi; C] = (V, E, \mathbf{end})$ its dependency graph $w.r.t.$ a set of colours $C \subseteq F_+ \uplus F_-$. The degree of a ray $(i, j)$ is defined by $\deg_{\Phi}^{C}(i, j) := |\mathbf{adj}_{\Phi}^{C}(i, j)|$. We simply write $\deg_{\Phi}$ when the set of colours is omitted.

§49.14 **Definition** (Free, deterministic and branching rays). Let $\Phi$ be a constellation and $C \subseteq F_+ \uplus F_-$ a set of colours. We say that a ray $r$ of $\Phi$ is:

- free if $\deg_{\Phi}^{C}(r) = 0$;

- deterministic if $\deg_{\Phi}^{C}(r) = 1$;

- branching if $\deg_{\Phi}^{C}(r) > 1$;

- co-branching if there is some branching ray $r' \in \mathbf{adj}_{\Phi}^{C}(r)$.

§49.15 **Remark.** Unpolarised rays $f \in F_0$ are always free but polarised rays can be free as well if it has no dual rays in the constellation it is in.

§49.16 **Definition** (Diagram). A $C$-diagram (or simply *diagram* when $C = F_+ \uplus F_-$) over a set of colours $C \subseteq F_+ \uplus F_-$ and a constellation $\Phi$ of dependency graph $\mathfrak{D}[\Phi; C] := (V_{\mathfrak{D}}, E_{\mathfrak{D}}, \mathbf{end}_{\mathfrak{D}})$ is a pair $(G_{\delta}, \delta)$ where $\delta$ is hypergraph homomorphism (cf. Definition C.1.12) extended with other functions described below

$$ \delta : G_{\delta} \to \mathfrak{D}[\Phi; C] $$

from a non-empty finite connected multigraph $G_{\delta} = (V_{\delta}, E_{\delta}, \mathbf{end}_{\delta})$. The homomorphism $\delta$ is made of:

- a map $\delta : V_{\delta} \to V_{\mathfrak{D}}$ between vertices;

- a map $\delta : E_{\delta} \to E_{\mathfrak{D}}$ between edges;
<figure><img src="image_92.png" /><figcaption>Figure 49.4: Technical remark about the definition of diagram. On the left we have a diagram which is associated with a dependency graph on the right. Since we only have the information of a link from a star to itself in the dependency graph, we cannot infer the membership of rays in the diagram.</figcaption></figure>

• for all $v \in V_\delta$, an injection $\delta_v : \text{Neigh}(v) \to \text{IdRays}(\delta(v))$ associating edges incident to $v$ in $\text{Neigh}(v) := \{e \in E_\delta \mid v \in \text{end}(e)\}$ to a ray of $\delta(v)$ such that:

- for all $e \in E_\delta$, $(\delta(v), \delta_v(e)) \in \text{end}(\delta(e))$ (it is coherent w.r.t. $\delta$) and

- for all $v, v' \in V_\delta$ and $e \in E_\delta$ such that $\text{end}(e) = \{v, v'\}$, we have $\delta_v(e) \neq \delta_{v'}(e)$ ensuring that all selected rays are distinct (in particular, it implies that a same ray cannot be connected to other rays since it appears only once).

The graph $G_\delta$ is considered up to renaming of the vertices and edges and for convenience, we will often consider $V \subseteq \mathbb{N}$ in practice.

§49.17 **Example.** An example of three diagrams for the constellation $\Phi_{\mathbb{N}}^{2+2}$ (which is an instance of the constellation $\Phi_{\mathbb{N}}^{n+m}$ of Example 48.18) is given in Figure 49.3.

§49.18 **Remark.** The most natural definition of dependency graph and diagram uses undirected edges because edges represent equations linking rays. Since edges make explicit which star the rays come from, there is usually no ambiguity. However, in the case of loops, a problematic ambiguity occurs: when unfolding a loop by linking a star with one of its copies in a diagram, we do not know which rays is related to the link. Consider the constellation $\Phi := [+c(X), -c(X)]$ made of a unique star $\Phi[0] := [+c(X), -c(X)]$. The problem is illustrated in Figure 49.4. The dependency graph is made of a link from $\Phi[0]$ to itself. When constructing a diagram of size 2 (for instance), we have two occurrences of $\Phi[0]$ but the membership of rays are not distinguished. There are two possibilities: either $+c(X)$ is coming from the first instance or from the second instance. Although in this case it is not really a problem (the result will be the same), it shows that considering undirected edges does not give a faithful interpretation of the graphical and intuitive presentation of the model, which may be problematic in some cases. Hence, two directions (for each rays of the associated equation) must be distinguished. If we really want a problematic case, we can consider the constellation $[+a(f(X)), -a(X), +b(X)] + [-b(X)]$. There is a loop between $-a(X)$ and $+a(f(X))$ in the first star. But if it linked to a copy of itself then to $-b(X)$, depending on if it is linked through $-a(X)$ or $-a(f(X))$ we may (or not)
<figure><img src="image_93.png" /><figcaption>Figure 49.5: Order $\sqsubseteq$ on diagrams representing an idea of saturation.</figcaption></figure>

transmit $f(X)$ to $-b(X)$ by unification. This explains the need for injections $\delta_v$ for all vertices $v$ of a diagram. It explicitly shows what rays we are referring to.

§49.19 In order to make definitions more accurate, we must state when two diagrams are equivalent. Otherwise, there are confusions because of the fact that the names of vertices in diagrams can be freely changed. Intuitively, diagram equivalence should be related to tiling equivalence. Two diagrams should be equivalent when they refer to an equivalent tiling of stars in a given constellation.

§49.20 **Definition (Diagram equivalence).** Let $(G_\delta, \delta)$ and $(G_{\delta'}, \delta')$ be two diagrams. They are equivalent, written $\delta \simeq \delta'$, when $G_\delta \simeq G_{\delta'}$ with a graph isomorphism $\varphi$ such that $\delta = \delta' \circ \varphi$.

§49.21 **Notation (Free rays and closed diagrams).** Given a C-diagram $(G_\delta, \delta)$ of a constellation $\Phi$ with $G_\delta = (V_\delta, E_\delta, \text{end}_\delta)$, we define its multiset (cf. Appendix A.2) of free (unconnected) rays $\text{free}(\delta) \subseteq \text{IdRays}(\Phi)$ by:

$$ \text{free}(\delta) := \text{multiset}\{r \in \text{IdRays}(\Phi) \mid \deg_{\Phi}^{C}(r) = 0\}. $$

If $\text{free}(\delta) = \emptyset$, we say that $\delta$ is closed.

§49.22 We usually would like diagrams to be impossible to extend by connecting more stars, which corresponds to a notion of saturation. In terms of tiling it is understood as the construction of the largest constructible tiling with occurrences of tiles from a given tile set and in terms of programming, it corresponds to a complete computation to be done.

§49.23 **Definition (Saturated diagram).** We define a binary relation $\sqsubseteq$ (illustrated in Figure 49.5) on C-diagrams over a constellation $\Phi$ by: $\delta \sqsubseteq \delta'$ if there exists an isomorphism $\varphi$ from a graph $H \subseteq G_{\delta'}$ to $G_\delta$ such that $\delta = \delta' \circ \varphi$. A maximal C-diagram w.r.t. $\sqsubseteq$ is called saturated.
§49.24 **Proposition.** The relation $\sqsubseteq$ is a preorder.

*Proof.* We have $\delta \sqsubseteq \delta$ by taking the subgraph $G_\delta \subseteq G_\delta$. The isomorphism $\varphi$ is the identity function so we trivially have $\delta = \delta \circ \varphi$.

Assume we have $\delta_1 \sqsubseteq \delta_2$ and $\delta_2 \sqsubseteq \delta_3$. Hence, we have isomorphisms $\varphi_{1,2} : (H_2 \subseteq G_{\delta_2}) \simeq G_{\delta_1}$ and $\varphi_{2,3} : (H_3 \subseteq G_{\delta_3}) \simeq G_{\delta_2}$ such that $\delta_1 = \delta_2 \circ \varphi_{1,2}$ and $\delta_2 = \delta_3 \circ \varphi_{2,3}$. We can construct an isomorphism $\varphi_{1,2} \circ \varphi_{2,3}$ such that $\delta_1 = \delta_3 \circ \varphi$ and $G_{\delta_3}$ is indeed an extension of $G_{\delta_1}$ following the connexions of the same dependency graph. $\square$

§49.25 Links in a diagram have an underlying equation. It follows that a whole diagram is associated with a unification problem. A minor but important technical problem is that variables appearing in a constellation $\Phi$ are meant to be bound to their star. Hence, before evaluating, we must rename variables so to mark their membership to a star of $\Phi$. Fortunately, it is possible to define a canonical renaming by using the star indexes $I_\Omega$.

§49.26 **Convention.** Assume that the signature $\mathbb{P}$ contains a fresh symbol $x_v$ for each $v \in V$ such that all $x_v$ are pairwise distinct.

§49.27 **Definition** (Underlying equation and problem). Let $(G_\delta, \delta)$ be a $C$-diagram of a constellation $\Phi$ with $G_\delta = (V_\delta, E_\delta, \mathbf{end}_\delta)$. By Convention 49.26, all vertices $x \in V$ induce a family of renamings $\alpha_v(x) = x_v$ for any variable $x$.

The underlying equation of an edge $e \in E_\delta$ such that $\mathbf{end}_\delta(e) = \{v, v'\}$ and $\delta(e) = \{(i, j), (i', j')\}$ is defined by

$$ \mathbf{eq}(e) := \alpha_v[\Phi[i][j]] \stackrel{?}{=} \alpha_{v'}[\Phi[i'][j')] $$

and the underlying problem of $\delta$ is defined by

$$ \mathrm{Prob}(\delta) = \{\mathbf{eq}(e) \mid e \in E_\delta\}. $$

Underlying problems are considered up to $\alpha$-equivalence. In particular, the choice of renaming function is not relevant but variables should be distinguished when they come from two distinct stars.

§49.28 In Girard's original paper [Gir17, Section 2.3], the evaluation of diagrams is defined as an edge contraction. An edge $e$ between two stars $\phi$ and $\phi'$ contains an equation which is resolved and then the associated solution is propagated to both $\phi$ and $\phi'$. The two connected rays associated with $e$ are finally destructed in the process. It reminds of chemical interactions but also of how information is propagated and organised in a network. This process can fail in presence of errors during the execution of a unification algorithm. This corresponds exactly to Robinson's resolution (cf. Section 23) and it generalises the composition of flows (cf. Section 37).
<figure><img src="image_94.png" /></figure>

(a) Correct diagram computing $2+2$ (1 recursion) with the ray $R$ visible.

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

(b) Fusion of $\phi_1$ and $\phi_2$ with $\theta := \{X_2 \mapsto \bar{0}, Y_2 \mapsto Y_1, Z_2 \mapsto Y_1\}$.

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

(c) Fusion of $\phi_{1,2}$ and $\phi'_2$ with $\theta := \{X'_2 \mapsto s(\bar{0}), Y'_2 \mapsto Y_1, Z'_2 \mapsto s(Y_1)\}$

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

(d) Fusion of the two remaining stars with $\theta := \{R \mapsto \bar{4}\}$.

<figure><img src="image_98.png" /><figcaption>Figure 49.7: Illustration of a step of fusion where $\theta$ is the principal unifier of the underlying unification problem of the pair of rays $(r, r')$. The fusion of the two stars $\phi$ and $\phi'$ along the rays $r$ and $r'$ produces a new star $\psi$.</figcaption></figure>

§49.29 We define this step-by-step procedure of diagram contraction based on an operation of *fusion*, but also an alternative of evaluation called *actualisation* which can simulate steps of fusion by evaluating a diagram by solving the whole unification problem associated. It is similar to how small step evaluation differs from big step evaluation in the theory of programming languages [Ama16, Section 1.1].

§49.30 **Definition (Fusion).** Let $\phi_1 := \phi'_1 \uplus \{r_1\}$ and $\phi_2 := \phi'_2 \uplus \{r_2\}$ be two stars. We define their fusion $\phi_1 \underset{\nabla}{\uplus} \phi_2$ by $\theta\phi'_1 \uplus \theta\phi'_2$ where $\phi_1[j] \bowtie \phi_2[j']$ and $\theta := \text{solution}\{\phi_1[j] \stackrel{?}{=}{\phi_2[j']}\}$.

We write $\phi_1 \underset{\nabla}{\uplus} \phi_2$ for the renaming of variables of both $\phi_1$ and $\phi_2$ to make them distinct followed by their fusion.

We simply write $\phi_1 \nabla \phi_2$ (and $\phi_1 \nabla_\alpha \phi_2$) without indexes above when there is a unique
possible choice of index and we choose to leave them implicit. Fusion is illustrated in Figure 49.7.

§49.31 **Example.** Assume we have two stars $\phi_N^+ R := [-add(X, Y, Z), +add(s(X), Y, s(Z))]$ and $\phi_Q^{2+2} := [-add(\bar{2}, \bar{2}, R), R]$ indexed by natural numbers corresponding to their position. We have:

$$ \phi_N^+ R \nabla^{1,0} \phi_Q^{2+2} := [-add(\bar{1}, \bar{2}, Z), s(Z)]. $$

$$ \phi_N^+ R \nabla^{1,0}_{\alpha} (\phi_N^+ R \nabla^{1,0}_{\alpha} \phi_Q^{2+2}) := [-add(0, \bar{2}, Z'), s(s(Z'))]. $$

§49.32 **Lemma (Associativity of fusion).** Let $\phi_1, \phi_2$ and $\phi_3$ be stars. We have

$$ \phi_1 \stackrel{i,j}{\nabla} (\phi_2 \stackrel{i',j'}{\nabla} \phi_3) \approx_{\alpha} (\phi_1 \stackrel{i,j}{\nabla} \phi_2) \stackrel{i',j'}{\nabla} \phi_3, $$

if we assume that all these fusions succeed.

*Proof.* It does not matter if some stars or all are the same. In case some stars are the same, we will have to reduce loops but in the end, what matters are only the equations involved and loops only add equations with identical variables, i.e. we have $t \stackrel{?}{=} u$ such that variables of $t$ may appear in $u$ because we are in the same star. We can consider without loss of generality that all stars are distinct. Assume we have three stars:

$$ \phi_1 := [u_1, \dots, u_n, r_1], \quad \phi_2 := [v_1, \dots, v_m, r_2, r'_2], \quad \phi_3 := [s_1, \dots, s_k, r_3] $$

with $\phi_1[i] = r_1, \phi_2[j] = r_2, \phi_2[i'] = r'_2$ and $\phi_3[j'] = r_3$.

Assume that rays are uniquely connected and that we have:

* $\theta := \text{solution}\{r_1 \stackrel{?}{=} r_2\}, \theta' := \text{solution}\{r'_2 \stackrel{?}{=} r_3\}$;

* $\psi := \text{solution}\{\theta' r_1 \stackrel{?}{=} \theta' r_2\}, \psi' := \text{solution}\{\theta r'_2 \stackrel{?}{=} \theta r_3\}$.

If we try to apply the steps of fusion, we have:

* $\phi_1 \stackrel{i,j}{\nabla} (\phi_2 \stackrel{i',j'}{\nabla} \phi_3) = \phi_1 \stackrel{i,j}{\nabla} [\theta' v_1, \dots, \theta' v_m, \theta' s_1, \dots, \theta' s_k, \theta' r_1, \theta' r_2] = [\psi \theta' u_1, \dots, \psi \theta' u_n, \psi \theta' v_1, \dots, \psi \theta' v_m, \psi \theta' s_1, \dots, \psi \theta' s_k]$;

* $(\phi_1 \stackrel{i,j}{\nabla} \phi_2) \stackrel{i',j'}{\nabla} \phi_3 = [\theta u_1, \dots, \theta u_n, \theta v_1, \dots, \theta v_m, \theta r'_2, \theta r_3] \stackrel{i',j'}{\nabla} \phi_3 = [\psi' \theta u_1, \dots, \psi' \theta u_n, \psi' \theta v_1, \dots, \psi' \theta v_m, \psi' \theta s_1, \dots, \psi' \theta s_k]$.

We can think about how the substitutions are constructed. Both substitutions can be constructed from the same set of equations $\{r_1 \stackrel{?}{=} r_2, r'_2 \stackrel{?}{=} r_3\}$. The substitution $\psi \theta'$ is constructed by solving the equations of $r'_2 \stackrel{?}{=} r_3$ first then the equations of $r_1 \stackrel{?}{=} r_2$. The substitution $\psi' \theta$ is obtained by reversing the order: first the equations of $r_1 \stackrel{?}{=} r_2$ are
solved then the ones of $r'_2 \stackrel{?}{=} r_3$. By Theorem B.2.6, we can solve the equations in any order and obtain the same solution up to renaming. Hence $\psi\theta'$ and $\psi'\theta$ have the same action on terms up to renaming.

Remark that there is no need to consider failure because one failure is expected to make the whole diagram collapse. □

§49.33 **Definition (Diagram contraction)**. The operation of diagram contraction over a C-diagram $(G_\delta, \delta)$ for $C \subseteq F_- \uplus F_+$ with:

• $G_\delta := (V_\delta, E_\delta, \mathbf{end}_\delta)$;

• $\mathfrak{D}[\Phi; C] = (V_{\mathfrak{D}}, E_{\mathfrak{D}}, \mathbf{end}_{\mathfrak{D}})$

is defined as a graph rewriting of $G_\delta$ along some edge $e \in E_\delta$ such that $\mathbf{end}(e) = \{v, v'\}$ (possibly with $v = v'$) and $\delta(e) = \{(i, j), (i', j')\}$ (possibly with $i = i'$), which updates the homomorphism $\delta : G_\delta \to \mathfrak{D}[\Phi; C]$. It produces a new diagram $\stackrel{e}{\nabla}(G_\delta, \delta) = (G'_\delta, \delta')$ with $G'_\delta := (V_{\delta'}, E_{\delta'}, \mathbf{end}_{\delta'})$ and $\delta' : G_{\delta'} \to \mathfrak{D}[\Phi'; C]$, defined as follows:

• Assume $v \neq v'$. We want to do an edge contraction between two different vertices. We remove $v, v'$ and their incident edges and replace them by a new vertex $w$ inheriting their previous bonds, i.e. $V_{\delta'} := V_\delta - \{v, v'\} \cup \{w\}$ and for $e_1, \dots, e_n \in E_\delta$ with $\mathbf{end}_\delta(e_i) = \{v_i, v\}$ and for $e'_1, \dots, e'_m \in E_\delta$ with $\mathbf{end}_\delta(e'_i) = \{v'_i, v'\}$ we have $E_{\delta'} := (E_\delta - \{e, e_1, \dots, e_n, e'_1, \dots, e'_m\}) \cup \bigcup_{i=1}^n \{g_i\} \cup \bigcup_{i=1}^m \{g'_i\}$ such that $\mathbf{end}_{\delta'}(g_i) = (v_i, w)$ and $\mathbf{end}_{\delta'}(g'_i) = (v'_i, w)$. In the other cases, we have $\mathbf{end}_{\delta'}(x) = \mathbf{end}_{\delta}(x)$;

We adapt the homomorphism to the previous change.

– $\Phi'$ is defined by $I_{\Phi'} := I_\Phi - \{i, i'\}$, and $\Phi'[i_w] := \alpha_v \Phi[i] \underset{\nabla}{\stackrel{j,j'}{\cup}} \alpha_{v'} \Phi[i']$ for some fresh $i_w \notin I_\Phi$ and $\Phi'[k] := \Phi[k]$ otherwise, where $\alpha_u$ comes from Definition 49.27;

– $\delta'(w) = i_w$ and $\delta'(x) = \delta(x)$ otherwise;

– if $e_i = \{(\delta(v_i), j_i), (-, j'_i)\}$ then $\delta'(g_i) = \{(\delta(v_i), j_i), (i_w, j'_i)\}$ and if $e'_i = \{(\delta(v'_i), j_i), (-, j'_i)\}$ then $\delta'(g'_i) = \{(\delta(v'_i), j_i), (i_w, j'_i)\}$.

• Assume $v = v'$. We want to do an edge contraction linking one same vertex. We have $V_{\delta'} := V_\delta$ and $E_{\delta'} := E_\delta - \{e\}$. We have $\delta'(x) = \delta(x)$ (but $\delta'(e)$ is not defined anymore). Almost nothing changes except that we remove the edge $e$ and the only star $\delta(v) = \delta(v')$ is updated. The constellation $\Phi$ is defined by $I_{\Phi'} := I_\Phi$ such that $\Phi[\delta(v)]$ is a star $\phi$ such that $I_\phi := \theta(I_{\delta(v)} - \{j, j'\})$ with $\phi[j''] = \theta\Phi[\delta(v)][j'']$ for all $j'' \in I_\phi$ for $\theta$ the solution of eq(e).
We write $(G_\delta, \delta) \rightsquigarrow_e (G_{\delta'}, \delta')$ when $(G_{\delta'}, \delta') = \nabla^e(G_\delta, \delta)$ along the edge $e$, and write $(G_\delta, \delta) \rightsquigarrow^n (G_{\delta'}, \delta')$ when there is a series $n \ge 0$ of steps such that $(G_\delta, \delta) \rightsquigarrow_{e_1} \dots \rightsquigarrow_{e_n} (G_{\delta'}, \delta')$ for some edges $e_1, \dots, e_n$. We leave the edge $e$ implicit when obvious or not important and we can write $\rightsquigarrow^*$ instead of $\rightsquigarrow^n$ when the number of steps is implicit.

**§49.34 Definition** (Correct diagrams and their actualisation). A C-diagram $(G_\delta, \delta)$ of a constellation $\Phi$ is correct if $\text{Prob}(\delta)$ has a solution.

The actualisation of a correct diagram $(G_\delta, \delta)$ is the star $\Downarrow \delta$ defined by $I_{\Downarrow \delta} := \text{free}(\delta)$ such that $(\Downarrow \delta)[(i, j)] = (\psi \circ \theta)(\Phi[i][j])$, where $\psi := \text{solution}(\text{Prob}(\delta))$ and $\theta := \alpha_{v_1} \circ \dots \circ \alpha_{v_n}$ with $V^{G_\delta} = \{v_1, \dots, v_n\}$ is the composition of renamings of Definition 49.27.

**§49.35 Lemma** (Termination of diagram contraction). If $(G_\delta, \delta)$ is correct then there exists $(G_{\delta'}, \delta')$ such that $(G_\delta, \delta) \rightsquigarrow^* (G_{\delta'}, \delta')$ and there is no $(G_{\delta''}, \delta'')$ such that $(G_{\delta'}, \delta') \rightsquigarrow^* (G_{\delta''}, \delta'')$.

*Proof.* By Theorem B.2.3 and the fact that fusion always succeed for correct diagrams, since $(G_\delta, \delta)$ is correct, the underlying unification problem only has solvable equations and hence there exists a full execution or the algorithm. $\square$

**§49.36 Corollary** (Confluence of diagram contraction). For some diagrams $(G_\delta, \delta)$, $(G_{\delta_1}, \delta_1)$ and $(G_{\delta_2}, \delta_2)$, if $(G_\delta, \delta) \rightsquigarrow^* (G_{\delta_1}, \delta_1)$ and $(G_\delta, \delta) \rightsquigarrow^* (G_{\delta_2}, \delta_2)$ then there exists $(G_{\delta'}, \delta')$ such that $(G_{\delta_1}, \delta_1) \rightsquigarrow^* (G_{\delta'}, \delta')$ and $(G_{\delta_2}, \delta_2) \rightsquigarrow^* (G_{\delta'}, \delta')$.

*Proof.* By the associativity of fusion (cf. Lemma 49.32), and the fact that diagram contraction is a step of fusion inside the graph of a diagram, we can infer that we have com-mutation of diagram contraction, i.e. $(G_{\delta_1}, \delta_1) \rightsquigarrow_e D \rightsquigarrow_{e'} (G_{\delta_2}, \delta_2) = (G_{\delta_1}, \delta_1) \rightsquigarrow_{e'} D \rightsquigarrow_e (G_{\delta_2}, \delta_2)$ for some diagram $D$. From this result, we have local confluence of diagram contraction. Together with the termination of diagram contraction (cf. Lemma 49.35), it is possible to use the so-called Newman's lemma [BN98, Lemma 2.7.2] to infer the confluence of diagram contraction (actually the diamond property which is equivalent). $\square$

**§49.37 Lemma.** If $(G_\delta, \delta) \rightsquigarrow_e (G_{\delta'}, \delta')$ then $\Downarrow(G_\delta, \delta) = \Downarrow(G_{\delta'}, \delta')$.

*Proof.* Assume $(G_\delta, \delta) \rightsquigarrow_e (G_{\delta'}, \delta')$ with $e = \{(v, j), (v', j')\}$ and $(G_\delta, \delta)$ is defined over a constellation $\Phi$. There are two cases.

* Assume $v \neq v'$. We have done an edge contraction on $G_\delta$ where two vertices merged into one vertex $w$ such that $\Phi[\delta(w)] := \alpha_v \Phi[\delta(v)] \xrightarrow{j; j'} \alpha_{v'} \Phi[\delta(v')]$. It terms of equations, what we have done is computing $\theta := \text{solution}\{\alpha_v \Phi[\delta(v)][j] \stackrel{?}{=} \alpha_{v'} \Phi[\delta(v')][j']\}$ and applying it on the merge of the two interacting stars $\delta(v)$ and $\delta(v')$. The only difference between $(G_\delta, \delta)$ and $(G_{\delta'}, \delta')$ is this one equation $\text{eq}(e)$.
<figure><img src="image_99.png" /><figcaption>Figure 49.8: Illustration of the execution of a finite and strongly normalising constellation.</figcaption></figure>

which has been solved. If we translate this situation in terms of equation solving, it corresponds to the transition between $P \cup \{\mathbf{eq}(e)\}$ and $P \cup P'$ such that $\vec{P}' = \theta$ where $P$ contains the other equations of $(G_\delta, \delta)$. In particular, by confluence of the unification algorithm (cf. Theorem B.2.4), equations can be solved in any order and we would end up on the same result in any case. It follows that actualisation can first solve $\mathbf{eq}(e)$ and the remaining equations are the ones of $(G_{\delta'}, \delta')$.

* Assume $v = v'$. The reasoning is the same and an equation is still solved except that we have a connexion between two rays of a same star instead of a fusion between two occurrences of stars.

□

**§49.38 Theorem (Relation between diagram contraction and actualisation).** For all correct diagram $(G_\delta, \delta)$ such that $G_\delta := (V_\delta, E_\delta, \mathbf{end}_\delta)$, we have $(G_\delta, \delta) \rightsquigarrow^{|E_\delta|} \mathbf{D}(G_\delta, \delta)$.

*Proof.* By induction on $n = |E_\delta|$. If $n = 0$ then we have 0 links and $(G_\delta, \delta)$ reduces to itself in 0 step, which corresponds to $\mathbf{D}(G_\delta, \delta)$. For the inductive case, we have $n = n' + 1$ and we assume that $(G_{\delta'}, \delta') \rightsquigarrow^{n'} \mathbf{D}(G_{\delta'}, \delta')$ and show $(G_\delta, \delta) \rightsquigarrow^{n'+1} \mathbf{D}(G_\delta, \delta)$ or equivalently $(G_\delta, \delta) \rightsquigarrow (G_{\delta'}, \delta') \rightsquigarrow^{n'} \mathbf{D}(G_\delta, \delta)$ for some $(G_{\delta'}, \delta')$. By Lemma 49.37, if $(G_\delta, \delta) \rightsquigarrow (G_{\delta'}, \delta')$, we must have $\mathbf{D}(G_\delta, \delta) = \mathbf{D}(G_{\delta'}, \delta')$. It means that solving the equations for $\delta$ and $\delta'$ ultimately leads to the same result. Hence, by substitution on the induction hypothesis, we have $(G_{\delta'}, \delta') \rightsquigarrow^{n'} \mathbf{D}(G_\delta, \delta)$. Therefore, $(G_\delta, \delta) \rightsquigarrow^{n'+1} \mathbf{D}(G_\delta, \delta)$. □

**§49.39 Remark.** The actualisation of diagrams corresponds to a single star because diagrams are connected.
Execution of constellations

§49.40 The (abstract) execution of a constellation $\Phi$ consists in computing all the correct saturated diagrams of $\Phi$ and actualising them. This process is illustrated in Figure 49.8.

§49.41 **Notation** (Set of correct saturated diagrams). We write $\mathbf{SatDiags}_C(\Phi)$ for the set of all saturated diagrams obtained from $\mathfrak{D}[\Phi; C]$ for a constellation $\Phi$ and a set of colours $C \subseteq F$. We omit the set of colours and simply write $\mathbf{SatDiags}(\Phi)$ when $C$ is all colours of $F$.

We write $\mathbf{CSatDiags}_C(\Phi)$ for the set of all diagrams in $\mathbf{SatDiags}_C(\Phi)$ which are correct.

§49.42 **Definition** (Execution and normal form). The *execution* or *normal form* of a constellation $\Phi$ w.r.t. a set of colours $C \subseteq F$ is defined by $\mathbf{AEx}_C(\Phi) := \mathop{\llcorner}\mathbf{CSatDiags}_C(\Phi)$, where

$$ \llcorner \mathbf{CSatDiags}_C(\Phi) := \{\llcorner \delta \mid \delta \in \mathbf{CSatDiags}_C(\Phi)\}. $$

We write $\mathbf{AEx}(\Phi)$ when all colours in $\Phi$ participate in the execution.

§49.43 We define an operation of *concealing* which violently mutes the constellation by removing stars containing polarised rays, thus forbidding any communication with other stars.

§49.44 **Definition** (Concealing). Let $\Phi$ be a constellation. The *concealing* of $\Phi$ is the constellation $\mathfrak{I}\Phi$ defined by $\mathfrak{I}\Phi := \{i \in I_{\Phi} \mid \phi := \Phi[i], \forall j \in I_{\phi}, \phi[j] \text{ is uncoloured}\}$.

§49.45 We define an operation of *noise filtering* of a constellation which removes the empty stars which are irrelevant since they cannot be connected. However, they still are valuable for quantitative analyses as we will see in the interpretation of MLL.

§49.46 **Definition** (Noise filtering). Let $\Phi$ be a constellation. The *noise filtering* of $\Phi$ is the constellation $\mathfrak{h}\Phi := \{i \in I_{\Phi} \mid \Phi[i] \neq \emptyset\}$.

§49.47 The plurality of diagrams is related to the several parallel choices for branching rays (but branching rays do not necessarily yield several diagrams). The execution is defined as if we were considering all possible choices at once. It is not a problem because in logic programming for instance, inferences coming from a given query can lead to several answers and we are usually interested in all possible answers.

§49.48 It is possible to recover the notion of choice by simply picking a star of the normal form of a constellation. This is not very natural since we have to compute all possibilities before making the choice. It is however sufficient for abstract execution which is purely mathematical.
§49.49 **Definition (Non-deterministic choice)**. Let $\Phi$ be a constellation. A non-deterministic choice over $\Phi$ is defined by a constellation $\text{pick}_i(\Phi) := \Phi[i]$ where $i \in I_{\text{AEx}(\Phi)}$. We simply write $\text{pick}(\Phi)$ when we do not want to specify the index of the selected star.

## The dynamics of subjective rays

§49.50 Something which has barely been mentioned is the case of internal polarities, the main feature making our model different from original resolution. There are two important characteristics of the introduction of internal polarities:

1. they introduce new polarised rays during execution. For instance, in

$$[-f(+g(X))] + [X, +f(X)],$$

if we connect the two stars along $-f(+g(X))$ and $+f(X)$, we obtain $[+g(X)]$. We transformed an unpolarised ray $X$ into a new polarised ray $+g(X)$;

2. they introduce mechanisms of *synchronisation*. In the previous example, if we want to interact/communicate with $+g(X)$ we must first making $+f$ and $-f$ interact. This is reminiscent of the use of *semaphores* in programming.

§49.51 Now, how does our abstract execution react in presence of internal polarities? The first point previously mentioned is problematic because diagrams are *fixed* structures. Once you construct a diagram connecting $+f$ with $-f$, you cannot see that there is an interaction available with $+g(X)$ providing we unlock it by first interacting with the colour $\pm f$. We could change definitions and make execution conscious of that but that would be complicated and probably unnecessary. What internal polarities do is that even after fully executing a constellation, there may be new connexions left. For instance in:

$$[-f(+g(X))] + [X, +f(X)] + [-g(X), +f(X), a]$$

we can make two diagrams over the colour $\pm f$ and the whole constellation has the normal form $[+g(X)] + [-g(+g(X)), a]$. This constellation can be executed again but its stars should be extended with stars of the initial constellation which has been lost during the first execution. We see that $[+g(X)]$ can be connected with $[-g(+g(X)), a]$, leading to $[a]$ but also with $[-g(X), +f(X), a]$ and in that case we obtain $[+f(X), a]$ which can be extended with $[-f(+g(X))], leading to [a]$. We obtain $[a] + [a]$ which is the “real normal form”. We can then handle internal polarities with repeated execution corresponding to several sequential layers in computation (as in imperative programming or any sequential model of computation).

§49.52 **Definition (Iterated and hyper execution)**. Let $\Phi$ and $\Psi$ be constellations and $C \subseteq$
$F_+ \uplus F_-$ a set of colours. We define its iterated execution by the following constellation:

$$AEx_{\Phi,C}^{0}(\Psi) = \Psi \qquad AEx_{\Phi,C}^{1}(\Psi) = AEx_{C}(\Psi)$$

$$AEx_{\Phi,C}^{n+1}(\Psi) = AEx_{C}(\Psi' \uplus AEx_{\Phi,C}^{n}(\Psi)) \quad \text{for } n > 1$$

where $\Psi'$ is the constellation made of stars of $\Phi$ which are matchable with the stars of $AEx_{\Phi,C}^{n}(\Psi)$.

The hyper execution of $\Phi$ is a constellation $AEx_{C}^{\infty}(\Phi) := AEx_{\Phi,C}^{k}(\Phi)$ which is defined when there exists some $k \in \mathbb{N}$ such that $AEx_{\Phi,C}^{k}(\Phi) = AEx_{\Phi,C}^{k+1}(\Phi)$.

§49.53 **Example.** For the constellation

$$\Phi := [-f(+g(X))] + [X, +f(X)] + [-g(X), +f(X), a],$$

we have $AEx_{\Phi,C}^{1}(\Phi) = [+g(X)] + [-g(+g(X)), a]$ and $AEx_{C}^{\infty}(\Phi) = AEx_{\Phi,C}^{2}(\Phi) = [a] + [a]$.

§49.54 **Proposition (Objective full evaluation).** Let $(G_{\delta}, \delta)$ be a C-diagram for a constellation $\Phi$ such that all stars are objective. There is no pair of matchable rays in $\Downarrow(G_{\delta}, \delta)$.

*Proof.* First, free($\delta$) contains no pair of matchable rays, by definition. The only way to produce pairs of matchable rays is to have an equation $\{X \mapsto s\}$ in Prob($\delta$) replacing a variable $X$ by some subjective ray $s$. However, since all stars are objective and equations do not consider head polarities by definition of $\downarrow$, it follows that there is no such equation. Therefore, there cannot be pair of matchable rays in $\Downarrow(G_{\delta}, \delta)$. $\square$

§49.55 **Corollary (Idempotence of abstract execution).** For any constellation $\Phi$ and set of colours $C \subseteq F_+ \uplus F_-$, if $\Phi$ has only objective stars then $AEx_{C}(AEx_{C}(\Phi)) = AEx_{C}(\Phi)$.

*Proof.* By Proposition 49.54, since abstraction execution is made of the actualisation of all saturated and correct diagrams and that those diagrams do not have pairs of matchable rays, each star of $AEx_{C}(\Phi)$ has no pair of matchable rays. It remains to show that there are no pair of matchable rays between the distinct stars. If we had $\Phi[i][j] \bowtie \Phi[i'][j']$ with $i \neq i'$ then those two rays could have been connected and form a same diagram and are thus not free in $(G_{\delta}, \delta)$. It follows that no diagram can be constructed from $AEx_{C}(\Phi)$ if all stars are objective. Therefore, $AEx_{C}(AEx_{C}(\Phi)) = AEx_{C}(\Phi)$. $\square$

§49.56 **Proposition (Idempotence barrier).** For any constellation $\Phi$ and set of colours $C \subseteq F_+ \uplus F_-$, if $AEx_{C}^{\infty}(\Phi) = AEx_{C}^{k}(\Phi)$ for some $k \in \mathbb{N}$ then for all $l \in \mathbb{N}$, $AEx_{C}^{k+l}(\Phi) = AEx_{C}^{k+l}(\Phi)$.

*Proof.* Assume we have $AEx_{C}^{\infty}(\Phi) = AEx_{C}^{k}(\Phi)$. We know by the definition of $AEx_{C}^{\infty}(\Phi)$ that $AEx_{C}^{k+1}(\Phi) \stackrel{H}{=} AEx_{C}^{k}(\Phi)$. By induction on $l$.
◇ **Base case** If $l = 0$ then we have $\mathbf{AEx}_C^{k+1+0}(\Phi) = \mathbf{AEx}_C^{k+1}(\Phi) \stackrel{H}{=} \mathbf{AEx}_C^k(\Phi) = \mathbf{AEx}_C^{k+0}(\Phi)$.

◇ **Inductive case** Now assume $l = l' + 1$ and $\mathbf{AEx}_C^{k+1+l'}(\Phi) = \mathbf{AEx}_C^{k+l'}(\Phi)$ (induction hypothesis). By definition and by using the induction hypothesis, we have

$$ \begin{aligned} \mathbf{AEx}_C^{k+1+l}(\Phi) &= \mathbf{AEx}_C^{k+1+l'+1}(\Phi) = \mathbf{AEx}_C(\mathbf{AEx}_C^{k+1+l'}(\Phi)) \stackrel{IH}{=} \mathbf{AEx}_C(\mathbf{AEx}_C^{k+l'}(\Phi)) \\ &= \mathbf{AEx}_C^{k+l'+1}(\Phi) = \mathbf{AEx}_C^{k+l}(\Phi). \end{aligned} $$

□

§49.57 Although execution is always idempotent for objective constellations, we have seen in the previous example that it can be lost in presence of subjective rays. If there is a point in repeated execution where we reach idempotence then hyperexecution is idempotent (it is similar to the nilpotency property in GoI).

§49.58 **Corollary** (Idempotence of hyper execution). For any constellation $\Phi$ and set of colours $C \subseteq F_+ \uplus F_-$, if $\mathbf{AEx}_C^\infty(\Phi) = \mathbf{AEx}_C^k(\Phi)$ for some $k \in \mathbb{N}$ then $\mathbf{AEx}_C^\infty(\mathbf{AEx}_C^\infty(\Phi)) = \mathbf{AEx}_C^\infty(\Phi)$.

*Proof.* By hypothesis, we have $\mathbf{AEx}_C^\infty(\Phi) = \mathbf{AEx}_C^k(\Phi)$ for some $k \in \mathbb{N}$. Hence we have to prove $\mathbf{AEx}_C^k(\mathbf{AEx}_C^k(\Phi)) = \mathbf{AEx}_C^k(\Phi)$. By induction on $k$.

◇ **Base case** If $k = 0$ then $\mathbf{AEx}_C^0(\mathbf{AEx}_C^0(\Phi)) = \mathbf{AEx}_C^0(\Phi) = \Phi$.

◇ **Induction case** Assume $k = k' + 1$ and $\mathbf{AEx}_C^{k'}(\mathbf{AEx}_C^{k'}(\Phi)) = \mathbf{AEx}_C^{k'}(\Phi)$ (induction hypothesis). We have $\mathbf{AEx}_C^k(\mathbf{AEx}_C^k(\Phi)) = \mathbf{AEx}_C^2(\mathbf{AEx}_C^{k'}(\mathbf{AEx}_C^{k'}(\Phi))) \stackrel{IH}{=} \mathbf{AEx}_C^2(\mathbf{AEx}_C^{k'}(\Phi)) = \mathbf{AEx}_C^k(\mathbf{AEx}_C^{k'+1}(\Phi)) = \mathbf{AEx}_C^k(\mathbf{AEx}_C^{k}(\Phi)) = \mathbf{AEx}_C^{k+1}(\Phi)$. By Proposition 49.56 with $l := 0$, it is equal to $\mathbf{AEx}_C^k(\Phi)$ which is what we were looking for.

□

§49.59 I leave a small open question: is there always a $k \in \mathbb{N}$ such that $\mathbf{AEx}^\infty(\Phi)$ for any constellation $\Phi$ or if there is a constellation always leaving new pairs of matchable rays after abstract execution (by using the dynamics of internal colours).

§49.60 Hyper execution is not necessarily defined. It is possible that after abstract execution, there are always pairs of matchable rays. Hence, it is possible to never reach a normal form.

§49.61 **Example.** Consider the following constellation:

$$ \Phi := [X, +f(X)] + [-f(-g(X)), -g(X)] + [+g(X), +g(X), a]. $$

The two stars $[X, +f(X)]$ and $[-f(-g(X)), -g(X)]$ (which can be connected) are
duplicated in order to satisfy the rays of [+g(X), +g(X), a]. After abstract execution, we obtain [-g(X), -g(X), a] + [-g(X), -g(X), a]. However, these stars can also be connected to [X, +f(X)] + [-f(-g(X)), -g(X)] from Φ. Applying abstract execution again will create more occurrences of [-g(X), -g(X), a].

## 50 Concrete execution

**§50.1** In his first paper on TS, Girard already defined an effective way to execute constellations [Gir17, Section 2.3] by giving a method to construct diagrams. However, it was only valid for the deterministic case with tree-shaped diagrams, which is very simple. In the deterministic case, all rays are uniquely linked. The general idea is to find an *iterative* way to construct the saturated and correct diagrams of abstract execution. We extend Girard's idea to branching rays in which a ray can be dual to several other rays.

**§50.2** **Definition (Construction space).** A construction space is an expression

$$ \Phi \vdash_C \Delta \mid \Psi $$

where $C \subseteq F_+ \uplus F_-$ is a set of colours, $i \in \mathbf{N}$, $\Phi$ and $\Psi$ are constellations and $\Delta$ is a set of diagrams where two diagrams are identified by diagram equivalence (cf. Definition 49.20). We write $\vdash$ for $\vdash_{F_+ \uplus F_-}$.

**§50.3** The idea is that $\Phi \vdash \Delta \mid \Psi$ represents a state during the process of the construction of all diagrams for $\Phi$ (which is the constellation we would like to execute). The set $\Delta$ is the set of all diagrams being constructed incrementally. Finally, the constellation $\Psi$ will contain the normal form of $\Phi$ at the end. When diagrams are saturated, they are evaluated by actualisation and put in $\Psi$ when correct or are simply discarded.

**§50.4** **Definition (Diagram extension).** Let $(G, \delta)$ be a $C$-diagram of a constellation $\Phi$ for a set of colours $C \subseteq F_+ \uplus F_-$ with $G := (V, E, \text{end})$. We define two operations extending diagrams with a new edge (both illustrated in Figure 50.1):

$\diamond$ **Internal extension** $(G, \delta) \underset{\text{in}}{\oplus} (v, j)$ with $v, v' \in V$ and $(\delta(v), j), (\delta(v'), j') \in \pm\text{IdRays}(\Phi)$ only defined when

* $(\delta(v'), j') \in \text{adj}_{\Phi}^C(\delta(v), j)$ and

* $(\delta(v), j) \in \text{free}(G, \delta)$,

which defines a new diagram $(G', \delta')$ such that $G' := (V, E', \text{end}')$ with:

* $E' := E \cup \{e\}$ for a fresh $e$;

* $\text{end}'(e) = \{v, v'\}$ and $\text{end}'(x) = \text{end}(x)$ otherwise;

* $\delta'(e) = \{(\delta(v), j), (\delta(v'), j')\}$ and $\delta'(x) = \delta(x)$ otherwise.
<figure><img src="image_100.png" /><figcaption>(a) Internal extension with an edge e of a diagram with vertices $v_1, v_2$.</figcaption></figure>

<figure><img src="image_101.png" /><figcaption>(b) External extension with an edge e of a diagram with vertices $v_1, v_2$. A new vertex $v'$ is added for a new occurrence of star of the constellation.</figcaption></figure>

<caption>Figure 50.1: Diagram extensions.</caption>

This operation connects two rays of a same diagram together.

◇ **External extension** $(G, \delta) \overset{(v,j)}{\oplus}_{\text{out}} (i', j')$ with $v, v' \in V$ and

$$ (\delta(v), j), (i', j') \in \pm \text{IdRays}(\Phi) $$

only defined when

• $(i', j') \in \text{adj}_{\Phi}^{C}(\delta(v), j)$ and

• $(\delta(v), j) \in \text{free}(G, \delta)$,

which defines a new diagram $(G', \delta')$ such that $G' := (V', E', \text{end}')$ with:

• $V' := V \cup \{v'\}$ for a fresh $v$;

• $E' := E \cup \{e\}$ for a fresh $e$;

• $\text{end}'(e) = \{v, v'\}$ and $\text{end}'(x) = \text{end}(x)$ otherwise;

• $\delta(v') = i', \delta'(e) = \{(\delta(v), j), (i', j')\}$ and $\delta'(x) = \delta(x)$ otherwise.

This operation connects a ray of the diagram $(G, \delta)$ with a new occurrence of star from the constellation $\Phi$.

§50.5 **Definition (Stellar construction)**. Let $\Phi \vdash_C \Delta | \Psi$ be a construction space. A step of stellar construction takes all diagrams in $\Delta$ and extend it with:

$$ (\Phi \vdash_C \Delta | \Psi) \rightsquigarrow (\Phi \vdash_C \Delta' | \Psi') $$

where:
• if $\text{SatDiags}(\Delta)$ is the set of saturated diagrams in $\Delta$ then

$$ \Psi' := \Phi' \uplus \downarrow \text{SatDiags}(\Delta); $$

• for all $(G, \delta) \in \Delta - \text{SatDiags}(\Delta)$ such that $G := (V, E, \text{end})$, we select non-deterministically a ray $(i, j) \in I_{\delta(v)} \cap \text{free}(G, \delta)$ for some $v \in V$;

• for all $(i', j') \in \text{adj}_{\Phi}^{C}(i, j)$, we have $(G, \delta) \underset{\text{out}}{\overset{(i,j)}{\oplus}} (i', j') \in \Delta'$;

• for all $(\delta(v'), j') \in \text{adj}_{\Phi}^{C}(i, j)$ such that $v \in V$ and $(\delta(v'), j) \in \text{free}(G, \delta)$, we have $(G, \delta) \underset{\text{in}}{\overset{(i,j)}{\oplus}} (\delta(v'), j') \in \Delta'$.

As usual, we write $\rightsquigarrow^*$ for the reflexive transitive closure of $\rightsquigarrow$.

**§50.6 Definition (Concrete execution).** Let $\Phi$ be a constellation. Its concrete execution is defined by a constellation $\text{CEx}_C(\Phi)$ such that

$$ (\Phi \vdash_C (G_1, \delta_1), \dots, (G_n, \delta_n) | \emptyset) \rightsquigarrow^* (\Phi \vdash_C \emptyset | \text{CEx}_C(\Phi)) $$

and:

1. for $i \in I_{\Phi}$ with $1 \le i \le n$, $(G_i, \delta_i)$ where $G_i := (V_i, E_i, \text{end}_i)$ is a diagram containing only the star $\Phi[i]$, i.e. $V := \{v_i\}$, $\delta(v_i) = i$ and $E := \emptyset$;

2. no step of stellar construction can be applied on $(\Phi \vdash_C \emptyset | \text{CEx}_C(\Phi))$ (we say that the construction space is in normal form).

**§50.7 Theorem (Equivalence between abstract and concrete execution).** Let $\Phi$ be a constellation and $C \subseteq F_+ \uplus F_-$ be a set of colours. When $\text{CEx}_C(\Phi)$ is defined, we have $\text{AEx}_C(\Phi) = \text{CEx}_C(\Phi)$.

*Proof.* If $\text{CEx}_C(\Phi)$ is defined then $(\Phi \vdash_C (G_1, \delta_1), \dots, (G_n, \delta_n) | \emptyset) \rightsquigarrow^* (\Phi \vdash_C \emptyset | \text{CEx}_C(\Phi))$ with $\Phi \vdash_C \emptyset | \text{CEx}_C(\Phi)$ in normal form. We show that for construction space $(\Phi \vdash_C \Delta' | \Psi')$ occurring during concrete execution, $\Delta'$ contains all diagrams of $\Phi$ with $n$ edges, $\Psi'$ all actualisation of saturated diagrams of $\Phi$ with $n-1$ edges for $n$ the number of steps done starting from the initial construction space. By induction on $n$.

◇ **Base case** Assume $n = 0$. We have the initial construction space. By definition, the diagrams of $\Delta'$ are all diagrams of 0 edge. There is no saturated diagram of size $-1$ hence we have $\Psi' := \emptyset$;

◇ **Induction case** Assume $n = n' + 1$. Assume we have $(\Phi \vdash_C \Delta' | \Psi')$ with $\Delta'$ containing diagrams of $n'$ edges and $\Psi'$ actualisation of saturated diagrams of $n' - 1$ edges. We have one more step and obtain $(\Phi \vdash_C \Delta'' | \Psi'')$. By definition of stellar construction, $\Delta''$ extends diagrams of $\Delta'$ (which contains all diagrams of $n'$ edges) by an edge (either by connecting two vertices/stars of the diagram or adding another
occurrence of star from $\Phi$), hence $\Delta''$ contains all diagrams of $n' + 1$ edges. Again, by definition of stellar construction, a step actualise all saturated diagrams of $\Delta'$ and put them in $\Psi''$ which hence contains all actualisation of saturated diagrams of $n' - 1 + 1 = n'$ edges.

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

**§50.8** **Remark.** Concrete execution is only defined when the construction of diagrams is terminating. Hence, concrete execution is weaker than abstract execution in some sense since abstract execution can compute infinite constellations and is always defined. Concrete execution only produces finite constellations.

# 51 Interactive execution

**§51.1** When Girard presented stellar resolution (which was simply called “stars and constellations”), his execution was something along the lines of concrete execution. Concrete execution (in the deterministic case) is thus *Girard’s original notion of execution*. However, although concrete execution is rather intuitive and natural, it is only few months before my PhD defence that I defined it in my manuscript. When I first worked with Thomas Seiller on stellar resolution, we only worked with abstract execution because it was sufficient<fnref n="2" />. Since the beginning, I wanted to build something of a more computational fashion and I tried to implement it in Haskell<fnref n="3" />. This is what is presented in the section under the name of “interactive execution”. Oddly enough, it is also few months before my defence that is has been properly and formally defined.

**§51.2** The idea is not so different from concrete execution. Instead of constructing diagrams incrementally, we directly construct the actualisation of diagrams incrementally, by making stars interact by fusion “on the fly”. The big difference is that we lose the structure of graph and in particular we are not able to distinguish two stars which came from the same diagram (as in concrete execution which identifies diagrams up to isomorphism). Interactive execution hence considers different *execution traces* in which diagrams are not incrementally constructed in the same order. This is a sort of *directed version* of concrete execution. The drawback is that we may end up with a lot of redundancies in the normal form but we can cope with that by selecting the right initial stars and not necessarily all stars of the constellation we would like to execute. Typically, if we implemented an automata, we would choose the subconstellation representing the initial state.

<footnote n="2">²It also seems that this choice was influenced by Thomas Seiller’s mathematical taste. He liked the presentation of diagrams as graph homomorphism.</footnote>

<footnote n="3">³I called the program “Large Star Collider”. I’m currently working on another implementation in OCaml instead (because I wanted to practice OCaml).</footnote>
<figure><img src="image_103.png" /></figure>

(a) A particular diagram with 4 vertices corresponding to stars linked by 4 edges representing links between rays of those stars.

<figure><img src="image_104.png" /><figcaption>Figure 51.1: A diagram and 4 ways to construct it by iteratively adding edges.</figcaption></figure>

§51.3 **Definition (Interactive configuration)**. An *interactive configuration* is an expression

$$ \Phi \vdash_C \Psi $$

where $\Phi$ and $\Psi$ are constellations, and $C \subseteq F_+ \uplus F_-$ is a set of colours. We write $\vdash_C$ instead of $C = F_+ \uplus F_-$.

The constellation $\Phi$ is called *reference constellation* and $\Psi$ is called *interaction space*.

§51.4 In an interactive configuration $\Phi \vdash_C \Psi$, the reference constellation $\Phi$ corresponds to the constellation we would like to execute and the interaction space $\Psi$ corresponds to a space where stars will interact in order to construct the result (corresponding to partial evaluations of diagrams). Interaction configurations can be transformed by some rules corresponding to the iterative construction of diagrams. Those transformations are dependent on a selected ray. The goal is to trigger interaction with other rays until no interaction is possible anymore in the interaction configuration (this corresponds to the property of saturation for diagrams).

§51.5 It may technically be possible to filter out the superfluous stars in the normal form by using arguments from combinatorics. We need to make all stars of the constellation initial (hence we start with $\Phi \vdash_C \Phi$) and for all possible diagrams we need to think about how many ways/order a diagram can be constructed from, by iteratively adding edges. An example of diagram with 4 ways to construct it is given in Figure 51.1.

§51.6 **Definition** (Set of matchable rays). Let $\Phi$ be a constellation, $C \subseteq F_+ \uplus F_-$ a set of colours and $r$ any ray. We define the *set of rays identifiers matchable with r* in $\Phi$
w.r.t. C by:

$$ \mathbf{mat}_{\Phi}^{C}(r) := \{(i, j) \in \pm\mathrm{IdRays}(\Phi) \mid r \succcurlyeq \Phi[i][j], \mathrm{colours}(r) \cup \mathrm{colours}(\Phi[i][j]) \subseteq C\}. $$

As usual, we simply write $\mathbf{mat}_{\Phi}(r)$ when $C = F_{+} \uplus F_{-}$.

**§51.7 Definition (Self-interaction).** Let $\Phi[i]$ be a star of a constellation $\Phi$ with $i \in I_{\Phi}$. We define the self-interaction $\triangleright^{j,j'} \Phi[i]$ of $\Phi[i]$ along the rays $j$ and $j'$ as the star $\phi$ such that $I_{\phi} := \theta(I_{\Phi[i]} - \{j, j'\})$ with $\theta$ the solution of $\{\Phi[i][j] \stackrel{?}{=} \Phi[i][j']\}$.

**§51.8 Example.** Assume rays are indexed by natural numbers corresponding to their position in stars. We have that $\triangleright^{0,1} [+f(X), -f(g(X))]$ is undefined and

$$ \triangleright^{0,1} [+c(X), -c(X), a] = [a]. $$

**§51.9 Definition (Stellar interaction).** We define stellar interaction for an interactive configuration $\Phi \vdash_C \Psi$ w.r.t. some set of colours $C \subseteq F_{+} \uplus F_{-}$. Stellar interaction depends of some selected ray $(i, j) \in \pm\mathrm{IdRays}(\Psi)$. We set $\Psi := \Psi' + \Psi[i]$, hence the selected ray is $\Psi[i][j]$.

We have the following transition step:

$$ \Phi \vdash_C \Psi' + \Psi[i] $$

$$ \begin{align*} \underset{(i,j)}{\rightsquigarrow} \quad & \Phi \vdash \Psi' + \sum_{(i_k, j_k) \in \mathbf{mat}_{\Phi}^{C}(\Psi[i][j])} \Psi[i] \stackrel{j,j_k}{\nabla} \Phi[i_k] \\ & + \sum_{(i, j_k) \in \mathbf{mat}_{\Psi[i]}^{C}(\Psi[i][j])} \stackrel{j,j_k}{\triangleright} \Psi[i] \end{align*} $$

where:

* the first sum corresponds to all possible ways to interact with a new occurrence of star $\Phi[i_k]$ from $\Phi$ along a free ray $\Psi[i][j]$ of $\Phi[i]$ which is matchable with some $\Phi[i_k][j_k]$;

* the second sum corresponds to all possible ways to connect two free matchable rays in the same star $\Psi[i]$ (representing a partial diagram being constructed).

When a unification error occurs for $\psi \stackrel{k,k'}{\nabla} \psi'$ or $\triangleright^{k,k'} \psi$ then they disappears from the interaction space. We write $\rightsquigarrow^*$ for the reflexive transitive closure of $\rightsquigarrow$. We say that $\Phi \vdash_C \Psi$ is in normal form when no step of stellar interaction can be applied anymore.
§51.10 **Definition** (Interactive execution). Let $\Phi$ a constellation and $C \subseteq F_+ \uplus F_-$ a set of colours. We define its *interactive execution w.r.t. an initial subconstellation $\Psi$ of $\Phi$* by a constellation $\mathrm{IEx}_C(\Phi, \Psi)$ such that $\Phi \vdash_C \Psi \rightsquigarrow^* \mathrm{IEx}_C(\Phi, \Psi)$ and $\mathrm{IEx}_C(\Phi, \Psi)$ is in normal form. We write $\mathrm{IEx}_C(\Phi)$ for $\mathrm{IEx}_C(\Phi, \Phi)$.

§51.11 **Example** (Logic program for addition). We have

$$ \Phi_N^{2+2} := [\mathrm{add}(\bar{0}, Y, Y)] + [\mathrm{add}(X, Y, Z), \mathrm{add}(s(X), Y, s(Z))] + [\mathrm{add}(\bar{2}, \bar{2}, R), R] $$

with stars and rays indexed the natural indexing with natural numbers corresponding to their position. We put indexes on the top of rays to make things clearer.

• We compute $\mathrm{IEx}_C(\Phi_N^{2+2}, [-\mathrm{add}(\bar{2}, \bar{2}, R), R])$ by first selecting the ray (0, 0) of the interaction space.

<table><thead><tr><th>Step</th><th>Ψ[i][j]</th><th>Configuration</th><th>mat<sub>Φ</sub><sup>C</sup></th><th>mat<sub>Ψ[i]</sub><sup>C</sup></th></tr></thead><tbody><tr><td>0</td><td>(0, 0)</td><td>Φ<sub>N</sub><sup>2+2</sup> ⊢ [-add(2, 2, R), R]</td><td>{(1, 1)}</td><td>Ø</td></tr><tr><td>1</td><td>(0, 0)</td><td>Φ<sub>N</sub><sup>2+2</sup> ⊢ [-add(s(0), 2, Z), s(Z)]</td><td>{(1, 1)}</td><td>Ø</td></tr><tr><td>2</td><td>(0, 0)</td><td>Φ<sub>N</sub><sup>2+2</sup> ⊢ [-add(0, 2, Z), s(s(Z))]</td><td>{(0, 0)}</td><td>Ø</td></tr><tr><td>3</td><td></td><td>Φ<sub>N</sub><sup>2+2</sup> ⊢ [4]</td><td>Ø</td><td>Ø</td></tr></tbody></table>

– Step 0: we only have the query. It is matchable with a ray of the recursion star. We apply a step of fusion;

– Step 1: we can only use the recursion star again (only matchable ray is (1, 1) from $\Phi$);

– Step 2: the remaining star is only matchable with (0, 0) in $\Phi$, we apply a last step of fusion.

Remark that after “peeling” the query, we actually remove the potential non-determinism. When we reach 0 as first argument in the query, there is only one matchable ray which is [+add(0, Y, Y)].

• Interestingly, if we start from the wrong initial constellation (or consider $\Phi_N^{2+2} \vdash \Phi_N^{2+2}$), we may end up with an unwanted computational behaviour.
<table><thead><tr><th>Step</th><th>Ψ[i][j]</th><th>Configuration</th><th>mat<sub>Φ</sub><sup>C</sup></th><th>mat<sub>Ψ[i]</sub><sup>C</sup></th></tr></thead><tbody><tr><td>0</td><td>(0, 0)</td><td>Φ<sub>N</sub><sup>2+2</sup> ⊢ [+add(0, Y, Y)]</td><td>{(1, 0)}</td><td>Ø</td></tr><tr><td>1</td><td>(0, 0)</td><td>Φ<sub>N</sub><sup>2+2</sup> ⊢ [+add(s(0), Z, s(Z))]</td><td>{(1, 0)}</td><td>Ø</td></tr><tr><td>2</td><td>(0, 0)</td><td>Φ<sub>N</sub><sup>2+2</sup> ⊢ [+add(2, Z, Z + 2)]</td><td>{(1, 0), (2, 0)}</td><td>Ø</td></tr><tr><td>3</td><td>(0, 0)</td><td>Φ<sub>N</sub><sup>2+2</sup> ⊢ [+add(3, Z, Z + 3)] + [4]</td><td>{(1, 0)}</td><td>Ø</td></tr><tr><td>...</td><td>...</td><td>...</td><td>...</td><td>...</td></tr><tr><td>K+1</td><td>(0, 0)</td><td>Φ<sub>N</sub><sup>2+2</sup> ⊢ [+add(K, Z, Z + K)] + [4]</td><td>{(1, 0)}</td><td>Ø</td></tr></tbody></table>

This is not so surprising since there are infinitely many saturated diagrams which can be constructed but only one correct. Interactive execution has to compute all diagrams iteratively.

§51.12 **Observation (Logic programs).** The observation is that in order to correctly execute programs, we need control over the interactive execution of stellar resolution. This corresponds to the fact that Prolog uses SLD-resolution which is a controlled version of Robinson's original resolution. In particular, the interactive configuration must only have the query in its interaction space.

§51.13 **Remark.** In an interactive configuration $\Phi \vdash_C \Psi$, the reference constellation $\Phi$ is *non-linear* (infinite supply of stars) and the interaction space $\Psi$ is *linear* (stars are linearly consumed). This is reminiscent of intuitionistic sequents $!\Gamma \vdash_C \Delta$ in linear logic.

§51.14 **Example (Basic sanity check).** In this example we look at non-trivial constellations to make sure that our interpretation works as expected.

* The constellation $\Phi := [-a(X), +a(X)]$ has infinitely many saturated correct circular closed diagrams all actualising to [].

<table><thead><tr><th>Step</th><th>Φ[i][j]</th><th>Configuration</th><th>mat<sub>Φ</sub><sup>C</sup></th><th>mat<sub>Ψ[i]</sub><sup>C</sup></th></tr></thead><tbody><tr><td>0</td><td>(0, 0)</td><td>Φ ⊢ [-a(X), +a(X)]</td><td>{(0, 1)}</td><td>{(0, 1)}</td></tr><tr><td>1</td><td>(0, 0)</td><td>Φ ⊢ [-a(X), +a(X)] + []</td><td>{(0, 1)}</td><td>{(0, 1)}</td></tr><tr><td>2</td><td>(0, 0)</td><td>Φ ⊢ [-a(X), +a(X)] + [] + []</td><td>{(0, 1)}</td><td>{(0, 1)}</td></tr><tr><td>...</td><td>...</td><td>...</td><td>...</td><td>...</td></tr><tr><td>K</td><td>(0, 0)</td><td>Φ ⊢ [-a(X), +a(X)] + [] + K + []</td><td>{(0, 1)}</td><td>{(0, 1)}</td></tr></tbody></table>
• We have

$$ \Phi := [X^{(0,0)}, +a(X)] + [-a(1), +b(1)] + [-a(0), +b(0)] + [-b(1), -b(0)] $$

which should have for normal form $[0, 1] + [1, 0]$.

<table><thead><tr><th>Step</th><th>Ψ[i][j]</th><th>Configuration</th><th>mat<sub>Φ</sub><sup>C</sup></th><th>mat<sub>Ψ[i]</sub><sup>C</sup></th></tr></thead><tbody><tr><td>0</td><td>(0, 1)</td><td>Φ ⊢ [X, +a(X)]</td><td>{(1, 0), (2, 0)}</td><td>∅</td></tr><tr><td>1</td><td>(0, 1)</td><td>Φ ⊢ [0, +b(0)] + [1, +b(1)]</td><td>{(3, 1)}</td><td>∅</td></tr><tr><td>2</td><td>(0, 1)</td><td>Φ ⊢ [0, -b(1)] + [1, +b(1)]</td><td>{(1, 1)}</td><td>∅</td></tr><tr><td>3</td><td>(1, 1)</td><td>Φ ⊢ [0, -a(1)] + [1, +b(1)]</td><td>{(3, 0)}</td><td>∅</td></tr><tr><td>4</td><td>(1, 1)</td><td>Φ ⊢ [0, -a(1)] + [1, -b(0)]</td><td>{(2, 1)}</td><td>∅</td></tr><tr><td>5</td><td>(0, 1)</td><td>Φ ⊢ [0, -a(1)] + [1, -a(0)]</td><td>{(0, 1)}</td><td>∅</td></tr><tr><td>6</td><td>(1, 1)</td><td>Φ ⊢ [0, 1] + [1, -a(0)]</td><td>{(0, 1)}</td><td>∅</td></tr><tr><td>7</td><td></td><td>Φ ⊢ [0, 1] + [1, 0]</td><td>∅</td><td>∅</td></tr></tbody></table>

• If we reduce deterministic links in the previous example, we obtain the constellation $Φ := [X, -a(X)] + [+a(0), +a(1)]$. What happens if we start from $Φ[1][0]$?

<table><thead><tr><th>Step</th><th>Ψ[i][j]</th><th>Configuration</th><th>mat<sub>Φ</sub><sup>C</sup></th><th>mat<sub>Ψ[i]</sub><sup>C</sup></th></tr></thead><tbody><tr><td>0</td><td>(0, 1)</td><td>Φ ⊢ [+a(0), +a(1)]</td><td>{(0, 1)}</td><td>∅</td></tr><tr><td>1</td><td>(0, 0)</td><td>Φ ⊢ [+a(0), 1] + [0, +a(1)]</td><td>{(0, 0)}</td><td>∅</td></tr><tr><td>2</td><td>(1, 1)</td><td>Φ ⊢ [0, 1] + [0, +a(1)]</td><td>{(0, 0)}</td><td>∅</td></tr><tr><td>3</td><td>(1, 1)</td><td>Φ ⊢ [0, 1] + [0, 1]</td><td>∅</td><td>∅</td></tr></tbody></table>

• Consider the constellation $[+a(0)] + [+a(1)] + [X, -a(X), -b(X)] + [+b(0)] + [+b(1)]$ with normal form $[0] + [1]$.

<table><thead><tr><th>Step</th><th>Ψ[i][j]</th><th>Configuration</th><th>mat<sub>Φ</sub><sup>C</sup></th><th>mat<sub>Ψ[i]</sub><sup>C</sup></th></tr></thead><tbody><tr><td>0</td><td>(0, 0)</td><td>Φ ⊢ [+a(0)]</td><td>{(2, 2)}</td><td>∅</td></tr><tr><td>1</td><td>(0, 1)</td><td>Φ ⊢ [0, -b(0)] + [1, -b(1)]</td><td>{(3, 0)}</td><td>∅</td></tr><tr><td>2</td><td>(1, 1)</td><td>Φ ⊢ [0] + [1, -b(1)]</td><td>{(4, 0)}</td><td>∅</td></tr><tr><td>3</td><td></td><td>Φ ⊢ [0] + [1]</td><td>∅</td><td>∅</td></tr></tbody></table>
§51.15 **Lemma** (Diagram extension by interaction). Let $(G, \delta)$ be a $C$-diagram for a constellation $\Phi$. We have:

$$ \bullet \quad \Downarrow ((G, \delta) \underset{\text{in}}{\overset{(v,j)}{\oplus}} (v', j')) = \Downarrow(G, \delta) \underset{\nabla}{\overset{j,j'}{\nabla}} \Phi[\delta(v')]; $$

$$ \bullet \quad \Downarrow ((G, \delta) \underset{\text{out}}{\overset{(v,j)}{\oplus}} (i', j')) = \underset{\triangleright}{\overset{j,j'}{\triangleright}} \Downarrow(G, \delta). $$

*Proof.* By Theorem 49.38, a full contraction of a diagram can lead to the same result as its actualisation. We can then treat the evaluation of diagrams with diagram contraction. Consider the full contraction of the extended diagram. By the confluence of diagram contraction (cf. Corollary 49.36), it is possible to contract all edges except the edge $e$ linking the ray index $j$ and $j'$ without any effect on the result. At the end we contract $e$. This exactly corresponds to the computation of $\Downarrow(G, \delta) \underset{\nabla}{\overset{j,j'}{\nabla}} \Phi[\delta(v')]$ for external extension and $\underset{\triangleright}{\overset{j,j'}{\triangleright}} \Downarrow(G, \delta)$ for internal extension. $\square$

§51.16 **Theorem** (Relation between concrete and interactive execution). Let $\Phi$ be a constellation and $C \subseteq F_+ \uplus F_-$ be a set of colours. If $CEx_C(\Phi)$ is defined, then

$$ IEx_C(\Phi) \approx_{\alpha} CEx_C(\Phi) \uplus \Phi $$

where $\Phi'$ only contains occurrences (possibly none) of stars of $CEx_C(\Phi)$.

*Proof.* If $CEx_C(\Phi)$ is defined then $(\Phi \vdash_C (G_1, \delta_1), \dots, (G_n, \delta_n) | \emptyset) \rightsquigarrow^n (\Phi \vdash_C \emptyset | CEx_C(\Phi))$ with $\Phi \vdash_C \emptyset | CEx_C(\Phi)$ in normal form for some $n \in \mathbb{N}$. By induction on $n$ we show that for all construction spaces $(\Phi \vdash_C \Delta | \Psi)$ occurring during the concrete execution of $\Phi$, we have a sequence of stellar interaction steps $(\Phi \vdash_C \Phi) \rightsquigarrow^* (\Phi \vdash_C \Downarrow \Delta \uplus \Psi)$.

◇ **Base case** Assume $n = 0$. We start from the initial construction space $(\Phi \vdash_C (G_1, \delta_1), \dots, (G_n, \delta_n) | \emptyset)$. We do 0 step of stellar interaction and have $\Phi \vdash_C \Phi$. We indeed have $\Phi := \Downarrow \Delta \uplus \emptyset$ since $\Delta$ is the set of all diagrams of 0 edges (corresponding to the stars of $\Phi$).

◇ **Induction case** Assume $n = n' + 1$ for some $n'$. We reached some construction space $\Phi \vdash_C \Delta_{n'} | \Psi_{n'}$ after $n'$ steps and know that it can be simulated by a sequence of steps of stellar interaction $(\Phi \vdash_C \Phi) \rightsquigarrow^* (\Phi \vdash_C \Downarrow \Delta_{n'} \uplus \Psi_{n'})$. We add a new step of concrete execution and obtain $\Phi \vdash_C \Delta_{n'+1} | \Psi_{n'+1}$. We show that we can extend our interactive execution in order to obtain $\Phi \vdash_C \Downarrow \Delta_{n'+1} \uplus \Psi_{n'+1}$. By Lemma 51.15, what stellar interaction does on $(\Phi \vdash_C \Downarrow \Delta_{n'} \uplus \Psi_{n'})$ is basically computing the application of external and internal extensions of diagrams all in $\Delta_{n'}$, producing $\Delta_{n'+1}$. Since some stars cannot be extended because they correspond to the saturated diagram of $\Delta_{n'}$. When they are reunited with $\Psi_{n'}$ (corresponding to actualisations of saturated diagrams in concrete execution), we obtain $\Phi_{n'+1}$.
Since stellar interaction does not identify stars coming from equivalent diagrams (unlike concrete execution), we must have several duplicate stars corresponding to actualisation of equivalent diagrams, corresponding to the constellation $\Phi'$.

§51.17 The case of internal polarities. Interactive execution does not behave like abstract or concrete execution. Interactive execution construct diagrams *dynamically* and in an iterative way. Hence, we do not work with diagrams as *fixed and immutable structures* as with abstract execution. A consequence is that interactive polarities can work with subjective constellations without the need for repeated executions. Even if we create polarised rays by “unlocking” internal polarities, it is possible to make those new unlocked rays interact. However, the strategy we defined is not sufficient, as we will see in the next example.

§51.18 Example. We try to execute the constellation

$$ \Phi := [-f(+g(X))] + [X, +f(X)] + [-g(X), +f(X), \binom{2,0}{a}] $$

which contains internal polarities.

<table><thead><tr><th>Step</th><th>Ψ[i][j]</th><th>Configuration</th><th>mat<sub>Φ</sub><sup>C</sup></th><th>mat<sub>Ψ[i]</sub><sup>C</sup></th></tr></thead><tbody><tr><td>0</td><td>(0, 0)</td><td>Φ ⊢ [-f(+g(X))]</td><td>{(1, 1), (2, 1)}</td><td>Ø</td></tr><tr><td>1</td><td>(0, 0)</td><td>Φ ⊢ [+g(X)] + [-g(+g(X)), a]</td><td>{(2, 0)}</td><td>Ø</td></tr><tr><td>2</td><td>(0, 0)</td><td>Φ ⊢ [+f(X), a] + [-g(+g(X)), a]</td><td>{(0, 0)}</td><td>Ø</td></tr><tr><td>3</td><td></td><td>Φ ⊢ [a] + [-g(+g(X)), a]</td><td>Ø</td><td>Ø</td></tr></tbody></table>

The problem appears at the second step. The ray $+g(X)$ has been extracted from $-f(+g(X))$ and can interact with the ray $-g(X)$. This was not possible with abstract and concrete execution. However, this does not faithfully simulate hyperexecution since we could not connect $[+g(X)]$ with $[-g(+g(X)), a]$, which corresponds to the reunion of two evaluated diagrams. In the previous example, we thus have a ray $[-g(+g(X)), a]$ left although it should have been eliminated. A simple solution is to allow the interaction between two stars of the interaction space. This shows that non-trivial considerations have to be made in order to handle internal polarities.

§51.19 About the design of interactive execution. When I first defined interactive execution, I actually tried to make it match exactly with abstract execution by adding information on rays such as a unique occurrence identifier and the origin of rays (from which star of the initial constellation it comes from). The point was to identify stars coming from the same diagram constructed in a different way. However, we could always find counter-example and in the end the best way was to... keep the whole structure of diagram in memory. This is actually what splitted interactive execution and what led to the definition of concrete execution which came later.
§51.20 **Execution trace in interactive execution.** If we compute $\Phi \vdash \Phi$ we may compute several equivalent diagrams but they will lead to several occurrence of a same star. The reason is that those diagrams are not constructed in the same order. Although it may be seen as a technical drawback, it can be seen as a feature: we can put "directionality" in computation by choosing initial stars to start with. The strategy is usually to do a wise selection of exactly one star and one ray to start with for each connected component of the constellation we would like to execute. Some choice will lead to a well-defined result and other may lead to infinite loops.

## 52 Difference with Girard's stars and constellations

§52.1 The stellar resolution defined in this chapter is not exactly Girard's original model of stars and constellations defined in his sixth paper on GoI [Gir13a] and first paper on TS [Gir17]. Thomas Seiller and I designed some changes to make it more general but also to solve some technical problems and errors which occurred in formal definitions of the interpretation of MLL (that Girard did not formally establish).

§52.2 **Restriction to uniform stars.** In Girard’s original definition, rays of stars have some specific restrictions:

• they must have exactly the same variables. For instance $[X, +c(X)]$ is a correct star but not $[f(X, Y), +c(X)]$. This requirement is sufficient for MLL and is much simpler to study but it is later relaxed in order to treat exponentials [Gir16b];

• they must be pairwise non-matchable in order to avoid loops (cycles of size > 1 are still allowed). It simplifies a lot of things but in order to have more expressivity (so that we can interpret logic programs and other things), we choose to remove this requirement.

§52.3 **Constellations as indexed families instead of sets.** In Girard’s original definition, constellations are sets. Similarly to Wang tiles, it is actually sufficient to consider sets because stars of a given constellation can be duplicated in diagrams anyway. However, in our stellar resolution, we are not interested in diagrams themselves (which correspond to tilings) but in their evaluation. If two diagrams $\delta$ and $\delta'$ of a constellation $\Phi$ are both evaluated to a same star $\phi$ then we would like $\phi$ to appear in $\mathcal{A}\mathrm{Ex}(\Phi)$ to keep the quantitative information that two different diagrams produced $\phi$. Another difference is that the several occurrences of a same star actually matter in a constellation because two distinct diagrams can be constructed from the dependency graph. We have $\mathcal{A}\mathrm{Ex}([X, +c(X)] + [-c(X)]) = [X]$ but $\mathcal{A}\mathrm{Ex}([X, +c(X)] + [-c(X)] + [-c(X)]) = [X] + [X]$. It is not clear whether this feature is wanted or not but we leave it in our model.

§52.4 **Removal of the empty star.** Girard does not consider valid the empty star $\emptyset$ because it cannot be connected to another star. However, we choose to allow it because it still gives information: it comes from a correct diagram which had no free rays. But can
still recover Girard's execution by using the operator $\flat$ (cf. Definition 49.46) on the normal form to remove the empty star. This is useful when we do not want superfluous information.

§52.5 **Restriction to tree-like diagrams.** Girard only considers tree-like diagrams because they are sufficient to interpret logic. However, we choose to allow cyclic diagrams since they allow to express tile systems (tilings can be circular). We will see that it is also necessary to correctly interpret MLL proofs in an effective way (and that Girard's original definition is not exactly sufficient).

§52.6 **Different handling of maximality of diagrams.** As in the GoI, we need to consider maximal paths. In Girard's original definition, all possible connected tree-like diagrams are considered (without requirement of saturation). In a second step, all stars containing coloured rays are erased because coloured rays in the normal forms are considered as signs of incomplete computation. This forces diagrams to add as many stars as possible to fill the holes opened by coloured rays, thus only evaluations of maximal diagrams are considered. For more generality and to link the model with Seiller's works on interaction graphs [Sei16b], we allow coloured rays in the normal form (in exchange of a notion of saturation). This allows to compose executed constellations. Girard's execution can still be recovered by using the operator $\jfl$ (cf. Definition 49.44).

# 53 Discussion: comparison with other notions

§53.1 A question that I received several times is “is not stellar resolution exactly logic programming?”. Actually, if we remove some technical features such as internal colours or unpolarised rays, our model exactly corresponds to the semantics of first-order resolution with disjunctive clauses (cf. Section 23). But as far as I know, all models based on this semantics of term unification usually put *control* over it (SLD-resolution) or make the model subject to a logical interpretation whereas our model is purely computational, without any reference to any logic (Robinson’s resolution makes the expressions coincide with classical predicate calculus). Stellar resolution is unique and I believe the reason is simple: who would need something so complicated and chaotic? We usually design a model of computation a practical need but in Girard’s case, he was looking for a very flexible model in which he could express generalised proof-nets. We can still try to compare our model to other approaches in the field of logic programming and automated reasoning.

§53.2 **Original first-order resolution.** The closest model which comes to mind is simply Robinson's resolution logic. We use almost identical objects. We add unpolarised rays (but we can actually simulate it by using unused special predicate symbols). In resolution, we are usually interested in the reachability of the empty clause ([] in our case) representing a contradiction. In the stellar resolution, it does not have any meaning
and we use objects as query-free logic programs. Moreover, usual resolution is lim-
ited to tree derivations (corresponding to tree-like diagrams) whereas stellar resolution
allows cyclic diagrams in order to simulate tile systems. There are graph-based mod-
els [Sic76, Kow75, EO91] which are very similar to stellar resolution but they are still
different for the reasons mentioned above.

§53.3 **Horn clauses and logic programming.** In logic programming, we are usually interested in answering a query (or several queries) represented by a first-order atom (such as in Prolog, for instance). In order to answer the query, logic programming uses a backward reasoning by going up from the unique conclusion to the premises. Stellar resolution is naturally query-free (although queries can be simulated, there is no such distinguished objects). In particular, we can have several outputs and we do not distinguish between input and output. For instance, if we have a star representing an implication $A \Rightarrow B$, then we can connect a star to the output and only the input will survive. This does not make sense in logic programming because a direction from inputs to outputs is enforced in inference.

§53.4 **Stable model semantics.** There are several languages based on stable model semantics such as disjunctive logic programming [Min94, LRM91] itself based on a subset of Prolog called Datalog. The notion of stable model is also the basis of answer set programming (ASP) [Gel08, EIK09]. In these languages, a primitive handling of logical negation is used whereas we want our model to be purely computational, without any reference to logic.

§53.5 **Resolution operator.** In appearance, execution is very similar to the resolution operator [Lei12, Chapter 3] which is analogous to the consequence operator [DEGV01, Section 2.2] of logic programming. This operator computes a *full inference* from a given set of clauses. The difference is that we allow cyclic diagrams which makes our model closer to the construction of tilings in tile systems. As we later show when interpreting logic programs, allowing cyclic diagrams still preserves the interpretation of Horn clauses since cyclic diagrams are often wrong for logic programs: for the constellation $\Phi_N^{n+m}$ of Example 48.18, a loop can be constructed with

$$ [-add(X, Y, Z), +add(s(X), Y, s(Z))], $$

leading to the equation $X \stackrel{?}{=} s(X)$ which has no solution.

§53.6 **Lafont's interaction nets.** A remark I received is that stellar resolution may be equivalent to Lafont's interaction nets [Laf89] which are known to generalise proof-nets (and even proof-structures) [Laf95] and which can be simplified into a minimal set of interaction combinators [Laf97]. I admit that stellar resolution is indeed very close to interaction nets. I personally believe that stellar resolution can nicely encode interaction nets<fnref n="4" />, however I have never been able to figure out how close these models were. If we

<footnote n="4">⁴This is something I investigated a little bit with Julien Marquet but we never reached a conclusion.</footnote>
consider stars with internal colours then as far as I know there is no equivalent. Moreover,
everything can interact in interaction nets whereas stellar resolution features unpolarised
rays which cannot interact. But if we consider the objective polarised fragment of stellar
resolution, it seems to me that it already contains non-trivial elements which cannot be
represented by interaction nets which are purely based on structural graph rewriting.
Typically, in stellar resolution, we have equation solving which passes simple messages
based on first-order terms. Anyway, I think it can be interesting to connect our model
to Lafont's nets.

§53.7 **Generalised token machines.** There exists several extensions of the IAM for GoI (cf. Section 36). For instance, Dal Lago, Tanaka and Yoshimizu defined a token machine for Mazza’s multiport interaction combinators (a variant of the interaction combinators mentioned above) [DLTY17]. We can also mention Castellan and Clairambault’s “Multi-token Geometry of Interaction” [CC23]. Another recent work which can be mentioned is Chardonnet, Valiron and Vilmart work on ZX-calculus, a graph-based model for quantum computing [CVV21]. Their machine can be related to the concrete or interactive execution of stellar resolution but I currently do not know how similar these models are. It is likely that ZX-calculus can be expressed purely from term unification over more sophisticated equations with complex coefficients (instead of graph rewriting or a token machine) but I do not know why one would do that.
# Chapter 8

## Illustrating stellar resolution

§53.8 It is breaktime. In this chapter, we play with stars and constellations in order to encode several models of computation. It demonstrates the expressivity and computational power of stellar resolution. Most models of computation only need objective stars.

§53.9 The encodings show that stellar resolution can naturally express the main classes of models of computation given in Chapter 2:

* state machines (including Turing machines);

* $\lambda$-calculi (from their translation to proof-nets) – this will come later, during the interpretation of linear logic;

* tile systems (Wang tiles but also the abstract tile assembly model appearing in Paragraph 17.7);

* logic programs (with Horn clauses);

* generalised circuits (subsuming boolean and arithmetic circuits).

§53.10 In this chapter we focus on *interactive execution* instead of abstract or concrete execution because concrete execution is closer to the real behaviour of classical models of computation. In some cases, we use abstract (or concrete) execution because it is more convenient (for instance for tile systems).

## 54 Flows, wirings and graphs

§54.1 We start with the encoding of flows and wirings (defined in Section 37) since they are very close to stellar resolution: stars are $n$-ary symmetric flows.

§54.2 The main problem with the encoding of flows is that flows are asymmetric objects. The composition of two flows $t \leftarrow u$ and $v \leftarrow w$ only connects $u$ and $v$. In the meantime, even though we can use binary stars with polarities representing input and output, stars are natively symmetric. In the case of stars, $t$ can be connected to $u$ or even $v$. In order to encode the composition of flows, we have to restrict the possible connexions by distinguishing input and output.
§54.3 We fix a polarised signature $\mathbb{F} = (V, F, \mathbf{ar}, \oslash, [\cdot])$ for which we require the existence of colours $-S, +S, -T, +T \in C$ and function symbols $S, T$. The symbol $S$ stands for *source* and $T$ for *target*.

§54.4 **Definition** (Translation of flows and wirings). Let $t \leftarrow u$ be a flow. Its translation into a star is defined by $(t \leftarrow u)^\star := [S(t), T(u)]$. The translation extends to wirings $F$ by $F^\star := \sum_{f \in F} f^\star$.

§54.5 We could now treat $[S(t), T(u)]$ as a flow $t \leftarrow u$ and define composition exactly like the composition of flows. However, this is not very interesting. We are simply giving an alias to flows, an alternative notation but do not even use the mechanisms of stellar resolution. Another solution is to use the execution of stellar resolution to reproduce the composition of flows. However, because stars are symmetric and flows asymmetric, we need to play with polarities with external definitions (this is all we can do).

§54.6 **Definition** (Lateralisation). We define two colouring functions $\mu_l$ and $\mu_r$ called *lateralisations*, defined by:
$$ \mu_{\text{lat}}^l[S(t), T(u)] := [-S(t), T(u)] \quad \text{and} \quad \mu_{\text{lat}}^r[S(t), T(u)] := [S(t), +T(u)]. $$

§54.7 Now remark that even if we lateralise $(t \leftarrow u)^\star$ and $(v \leftarrow w)^\star$ respectively to the right and to the left, we would obtain $[S(t), +T(u)]$ and $[-S(v), T(w)]$ which means that only $+T(u)$ and $-S(v)$ can interact. However, since they do not share the same colour, we need an intermediate star $[-T(X), +S(X)]$ linking the two star. This star behaves like a cut in linear logic and execution becomes cut-elimination.

§54.8 **Theorem** (Simulation of composition and product). Let $f$ and $g$ be flows. We have:
1. $(fg)^\star = \mathbf{AEx}(\mu_{\text{lat}}^r(f^\star) + \mu_{\text{lat}}^l(g^\star) + [-T(X), +S(X)])$ and
2. $(FG)^\star = \mathbf{AEx}(\mu_{\text{lat}}^l(F^\star) \oplus \mu_{\text{lat}}^r(G^\star) + [-T(X), +S(X)])$.

*Proof.* By definition, if we have $f = t \leftarrow u$ and $g = v \leftarrow w$, then $fg = \theta t \leftarrow \theta w$ where $\theta := \text{solution}\{u \stackrel{?}{=} v\}$. By the translation of flows, we have $(fg)^\star = (\theta t \leftarrow \theta w)^\star = [S(\theta t), T(\theta w)]$. As for the right-hand side of the equality, we obtain

$$ \begin{aligned} & \mathbf{AEx}(\mu_{\text{lat}}^r(f^\star) + \mu_{\text{lat}}^l(g^\star) + [-T(X), +S(X)]) \\ & = \mathbf{AEx}([S(t), +T(u)] + [-S(V), T(W)] + [-T(X), +S(X)]). \end{aligned} $$

The third star $[-T(X), +S(X)]$ will connect the two other stars and we obtain the normal form $[S(\theta t), T(\theta w)]$. As for the product of wirings, we have $(FG)^\star = \{(fg)^\star | f \in F, g \in G, fg \text{ is defined}\}$ by definition and

$$ \mathbf{AEx}(\mu_{\text{lat}}^l(F^\star) \oplus \mu_{\text{lat}}^r(G^\star) + [-T(X), +S(X)]) $$
$$ = \{ \mathbf{AEx}(\mu_{\text{lat}}^{T}(f^{\star}) + \mu_{\text{lat}}^{I}(g^{\star}) + [-T(X), +S(X)]) | f \in F, g \in G, fg \text{ is defined} \} $$

We conclude with the simulation of flow composition proved above. □

**§54.9 Example.** We have $((X \leftarrow f(X))(Y \leftarrow h(Y))^{\star} = [S(X), T(h(f(X)))]$ which is also equal to $\mathbf{AEx}([S(X), +T(f(X))] + [-S(Y), T(h(Y))] + [-T(X), +S(X)])$.

**§54.10** When interpreting proof-nets or encoding bidirectional automata as in Aubert and Bagnolet's works [AB14], "biflows" $t \Leftrightarrow u := (t \Leftrightarrow u) + (u \Leftrightarrow t)$ are used instead in order to encode undirected edges in a graph (simple flows represent directed edges). Such biflows are translated into a constellation $(t \Leftrightarrow u)^{\star} = [S(t), T(u)] + [S(u), T(t)]$ (by the definition above). In case of a path $((t \Leftrightarrow u)(t' \Leftrightarrow u'))(t'' \Leftrightarrow u'')$ such that $u$ in only matchable with $t'$, $\theta u'$ only with $t''$ where $\theta := \mathbf{solution}\{u \stackrel{?}{\Leftrightarrow} t'\}$, the composition will be computed in stellar resolution as follows:

$$ \begin{aligned} & \mathbf{AEx}([S(t), +T(u)] + [S(u), +T(t)] + [-S(t'), T(u')]) + [-S(u'), T(t')]) \\ &= [S(\theta t), T(\theta u')] + [S(\theta u'), T(\theta t)] = (\theta t \Leftrightarrow \theta u')^{\star} \\ & \mathbf{AEx}([S(\theta t), +T(\theta u')] + [S(\theta u'), +T(\theta t)] + [-S(t''), T(u'')]) + [-S(u''), T(t'')]) \\ &= [S(\psi \theta u'), T(\psi t'')] + [S(\psi t''), T(\psi \theta u')] = (\psi \theta u' \Leftrightarrow \psi t'')^{\star} \end{aligned} $$

where $\psi := \mathbf{solution}\{\theta u' \stackrel{?}{\Leftrightarrow} t''\}$. Actually, with such use of flows, it is sufficient to use a simpler translation where biflows are translated into binary stars because of the introduction of symmetry.

**§54.11 Definition (Encoding of biflows).** Let $t \Leftrightarrow u$ be a biflow. Its encoding is defined by $(t \Leftrightarrow u)^{\star} := [+F(t), +F(u)]$.

**§54.12** We need to use a star $[-F(x), -F(x)]$ as a bridge between biflows. The previous computation becomes:

$$ \begin{aligned} & \mathbf{AEx}([+F(t), +F(u)] + [+F(u'), +F(t')]) + [+F(u''), +F(t'')] + [-F(X), -F(X)]) \\ &= [+F(\psi \theta u'), +F(\psi t'')] = \left( ((t \Leftrightarrow u)(t' \Leftrightarrow u'))(t'' \Leftrightarrow u'') \right)^{\star}. \end{aligned} $$

By using these ideas, it is easy to derive an encoding of graphs where edges are represented by binary stars since this was the initial purpose of flows.
## 55 Encoding of logic programs with Horn clauses

**§55.1** A natural illustration of the computational power of the stellar resolution is the encoding of logic programs since the stellar resolution directly generalises Robinson's first-order resolution which corresponds to the core of logic programming.

**§55.2** First, it is possible to do programming with predicate calculus [Kow74]. It is then known that formulas of predicate calculus can be normalised so that formulas are represented only by conjunctions of disjunctions (called clauses) with only universal quantifiers appearing as prefix [Hed04, Section 3.2]. Formulas are then of the shape $\forall x_1, ..., x_n. (A_1^1 \lor ... \lor A_n^1) \land ... \land (A_1^m \lor ... \lor A_k^m)$ where every $A_y^i$ is an atomic formula and where quantification is usually hidden. We use those normalised formulas of predicate calculus with at most one positive (without negation) atom in each clause. Such normalised formulas called *Horn clauses* represent sequents $\Gamma \vdash A$ for a set of hypotheses $\Gamma$ (cf. Section 23).

**§55.3** A *fact* is a closed (variable-free) first-order formula. Several facts form a *knowledge base*. We have *rules* which can be used to infer new facts from the available ones and thus expend the knowledge base. Rules are often represented as implications $A_1, ..., A_n \vdash B$ called *Horn clauses* [Hor51, Tär77]. A *query* asks if it is possible to infer a given fact from the knowledge base and is itself represented as a fact symbolising a goal. A *logic program* is a multiset of rules and facts.

**§55.4** The translation is direct. We use the use the polarities to distinguish between hypothesis and conclusion (or input and output). The translation of a fact is defined by

$$P(t_1, ..., t_n)^{\star} := [+P(t_1, ..., t_n)].$$

For a rule, the translation is defined by:

$$( \wedge_{i=1}^{m} P_1(t_1^i, ..., t_n^i) \vdash Q(u_1, ..., u_k) )^{\star} := ( \bigcup_{i=1}^{m} \{ -P_1(t_1^i, ..., t_n^i) \} ) \cup \{ +Q(u_1, ..., u_k) \}.$$

Finally, for a query, we have:

$$(?P(t_1, ..., t_n))^{\star} := [-P(t_1, ..., t_n), R_1, ..., R_m]$$

with $\{R_1, ..., R_m\} = \bigcup_{i=1}^{n} \text{vars}(t_i)$ which represents the information we would like to make visible in the output (see Example 48.18 where $[-add(\bar{n}, \bar{m}, r), r]$ is the query). A logic program $P := \bigcup_{i=1}^{n} \{C_i\}$ becomes $P^{\star} := \bigcup_{i=1}^{n} \{C_i^{\star}\}$.

**§55.5** The set of answers for a query $q$ on a program $P$ is defined by a set of substitutions $A_P^q = \{\theta_1, ..., \theta_k\}$ such that for all $\theta \in A_P^q$, we have $\theta q$ logically satisfied by $P$, written $P \models \theta q$. The answers are usually computed by iteratively applying the resolution rule between $q$ and all possible $C \in P$ until either no variables remain in $q$ or the resolution
rule is no more applicable. We refer to definitions of the SLD-resolution itself derived from Kowalski's SL-resolution [Kow74, KK71] for more details about the computation of answers.

**§55.6 Theorem (Simulation of logic programs).** Let $P$ be a logic program with query $q$ and $P^\star$ and $q^\star$ be their translation. For $n > 0$ and $|P| > 0$, if $\mathfrak{I} \nvDash \mathrm{IEx}(P^\star, q^\star) = \theta_1\phi_1 + \dots + \theta_n\phi_n$ for some $\theta_i$ is the answer of the query $q$ then $P \nvDash \theta_i q$.

*Proof.* The proof relies on the fact that

$$ \mathfrak{I} \nvDash \mathrm{IEx}(P^\star, q^\star) $$

exactly implements SLD-resolution [Kow74, KK71] which is known to be sound and complete for Horn clauses (cf. Section 23).

1. SLD-resolution selects a clause to be resolved. It corresponds to the query. This clause is fixed, meaning that we can mark it with a label “to be resolved”. The execution $\mathfrak{I} \nvDash \mathrm{IEx}(P^\star, q^\star)$ computes a normal form for $P^\star \vdash q^\star$ and in particular all fusion must applies to $q^\star$ with corresponds to the selected clause;

2. SLD-resolution make the marked clause linearly interact with clauses of $P$. Similarly, interactive execution make the only polarised ray of $q^\star$ interact with matchable rays of stars in $P^\star$. The same rule of interaction is used: resolution corresponds to fusion. The obtained clause is still marked as query;

3. In case of non-determinism, the marked clause is duplicated and interact with several clauses which are all marked as new queries and we have $P^\star \vdash q_1^\star + \dots + q_n^\star$;

4. We repeat the procedure on each obtained marked clause $q_i$ until we reach a fact. In this case, we end up with a substitution for the variables of the marked clause corresponding to the solution. If a marked clause cannot interact anymore without being resolved, it is erased. This is done by our operator $\mathfrak{I}$.

Additionally, we have to ensure that our relaxation to cyclic diagrams do not cause problems. In logic programming, we usually require that the rays of a star have exactly the same variables (all variables are bound). Because of this restriction, cycles in dependencies graphs of logic programs, when reduced to a loop on a single star, either involve equations of the shape $t \stackrel{?}{=} t$ or equations of the type $X \stackrel{?}{=} f(X)$. In the former case, if the associated rule is binary, i.e. of the shape $A \vdash B$, we obtain the empty star $\emptyset$ which is irrelevant in the computation and removed by the operator $\mathfrak{I}$. If the rule is not binary, e.g. of the shape $A_1, A_2, \dots, A_n \vdash B$, the equation $t \stackrel{?}{=} t$ associated with the loop is erased because it has no effect on the computation. In the latter case of the ill-behaving equation $X \stackrel{?}{=} f(X)$, the whole diagram is incorrect and ignored in the output. $\square$
§55.7 **Remark (Absence of solution).** The previous theorem assumed the existence of at least one solution for the query. If there are no solution at all for the query, then we obtain $\emptyset \subset \mathbf{IEx}(P^\star, q^\star) = \emptyset$. However we cannot say that we have $P \not\models \theta_i q$. In logic programming, we usually work with the "closed-world assumption", meaning that the absence of knowledge ($P$ does not satisfy the query) entails the falsity of a clause.

§55.8 **Remark.** There are additional features which could be added. We could also add rays $x \cdot X$ where $x$ is a constant representing the variable $X$ in order to keep the name of variable in the output. We would finally obtain a normal form made of stars $\phi_i = \bigcup_{i=1}^k \{x_i \cdot r_i\}$ such that $\phi_i$ corresponds to some $\theta \in A_P^q$. By doing so, which value corresponds to which variable in the solution (as in Prolog).

# 56 State machines

§56.1 Definitions of automata and Turing machines are taken from Sipser's introduction to the theory of computation [Sip06].

## Non-deterministic finite automata (NFA)

Let $\Sigma$ be an alphabet and $w \in \Sigma^*$ a word on some alphabet $\Sigma$. A non-deterministic automaton (NFA) on $\Sigma$ is a tuple $A = (\Sigma, Q, Q_0, \Delta, F)$ where $Q$ is the set of states, $Q_0$ and $F \subseteq Q$ are respectively the set of initial and final states, and $\Delta : Q \times \Sigma_\varepsilon \to \mathcal{P}(Q)$ is the transition function where $\Sigma_\varepsilon := \Sigma \cup \{\varepsilon\}$. The purpose of automata is to recognise languages by applying the transition function on the initial state and reaching either a final or non-final state.

A *partial run* in $A$ is a sequence of states $(q_0, \dots, q_n)$ such that $q_0 \in Q_0$ and $q_{i+1} \in \Delta(q_i, c_{i+1})$ for $0 \le i \le n-1$. A partial run $(q_0, \dots, q_n)$ is a *full run* (or simply *run*) when we also have $q_n \in Q_F$.

We say that $A$ accepts $w \in \Sigma^*$ from a state $q$, written $A(w, q) = 1$, when it has a full run starting with $q$. Otherwise, it is rejected and $A(w, q) = 0$. We define $A(w) := A(w, q_0)$ for $q_0$ the initial state of $A$ and say that $A$ *accepts* or *rejects* $w$. The language of $A$ is defined by $\mathcal{L}(A) = \{w \mid A(w) = 1\}$.

Links between tile systems and automata have already been studied [Tho91] but stellar resolution provides a framework where it is especially natural to express various classes of automata by simulating a linear run in a graph. Notice that it is possible to encode directed graphs by translating edges $(e, e')$ by binary stars $[-g(e), +g(e')]$. It is then possible to encode an NFA by first encoding its state graph then extending the rays so that the fusion triggers a flow of information. The final state will contain a dummy unpolarised ray *accept* so that the existence of a visible output in the normal form will
correspond to the acceptation a word. A similar approach has been studied with the model of flows [AB14, ABS16] where pointer machines are encoded.

§56.2 **Definition (Encoding of words)**. If $w = c_1...c_n$ is a word (cf. Appendix A.3) over some alphabet $\Sigma$ then $w^\star = [+i(c_1 \cdot \dots \cdot c_n \cdot \varepsilon)]$ with a constant $\varepsilon$ and the binary function symbol $\cdot$ which is considered right-associative, i.e. $a \cdot b \cdot c = a \cdot (b \cdot c)$.

§56.3 **Definition (Encoding of non-deterministic automata)**. Let $A = (\Sigma, Q, Q_0, \Delta, F)$ be an NFA. Its encoding is defined by $A^\star$ such that:

• for each $q_0 \in Q_0$, we have $[-i(W), +a(W, q_0)]$;

• for each $q_f \in F$, we have $[-a(\varepsilon, q_f), \mathbf{accept}]$;

• for each $q \in Q$ and if $c \in \Sigma_\varepsilon$ and for each $q' \in \Delta(q, c)$,
    - if $c = \varepsilon$, we have $[-a(W, q), +a(W, q')]$ (also known as epsilon transition);
    - otherwise, we have $[-a(W, q), +a(W, q')]$.

§56.4 **Lemma (Simulation of transitions)**. Let $w$ be a word and $A$ be an NFA. If $\Delta(c, q) = \{q_1, \dots, q_n\}$ then $A^\star \vdash [+a(c \cdot w, q)] \rightsquigarrow A^\star \vdash \sum_{i=1}^n [+a(w, q_i)]$.

*Proof.* Assume that we have $\Delta(c, q) = \{q_1, \dots, q_n\}$ and $A^\star \vdash [+a(c \cdot w, q)]$. By the encoding of NFA, we must have stars $\sum_{i=1}^n [-a(c \cdot W, q), +a(W, q_i)]$ in $A^\star$ representing the transitions $q_i \in \Delta(c, q)$. These are the only stars which are matchable with $[+a(c \cdot w, q)]$. By using a step of interactive execution, we obtain $A^\star \vdash [+a(c \cdot w, q)] \rightsquigarrow A^\star \vdash \sum_{i=1}^n [+a(w, q_i)]$ since $[-a(c \cdot W, q), +a(W, q_i)] \triangleright [+a(c \cdot w, q)] = [+a(w, q_i)]$. $\square$

§56.5 **Theorem (Simulation of non-deterministic finite automata)**. Let $w$ be a word and $A$ be an NFA. We have:

1. if $A(w) = 1$, then $[\mathbf{accept}] \in \mathfrak{IEx}(A^\star, w^\star)$;

2. if $A(w) = 0$, then $[\mathbf{accept}] \notin \mathfrak{IEx}(A^\star, w^\star)$;

*Proof.* We show the two statements.

1. Assume $A(w) = 1$. It means that there is a run $\rho := (q_0, \dots, q_n)$ from the initial state $q_0$ to $q_n \in F$. Since there is bijection between states of $\rho$ and symbols of $w$, we have $w = w_0 \dots w_n$. We have to compute $\mathfrak{IEx}(A^\star, w^\star)$. We start from $A^\star \vdash [+i(w)]$. By interacting with the initial star $[-i(w), +a(w, q_0)]$, we obtain $A^\star \vdash [+a(w, q_0)]$. By using $n$ times Lemma 56.4, for each transition $q_{i+1} \in \Delta(w_i, q_i)$, interactive execution will produce $A^\star \vdash [+a(w_{i+1} \dots w_n \cdot \varepsilon, q_{i+1})]$. By using the last transition $q_n \in \Delta(c_{n-1}, q_{n-1})$, we obtain $A^\star \vdash [+a(\varepsilon, q_n)]$ which can interact with the final star $[-a(\varepsilon, q_n), \mathbf{accept}]$. We then have an occurrence of $[\mathbf{accept}]$ on the right of $\vdash$ and other stars which did not reached the final state are erased by $\mathfrak{I}$. The star
<figure><img src="image_105.png" /></figure>

$$
\begin{aligned}
A^{\star} = & [-i(W), +a(W, q_0)] + [-a(\epsilon, q_2), \text{accept}] + [-a(0 \cdot W, q_0), +a(W, q_0)] + \\
           & [-a(1 \cdot W, q_0), +a(W, q_0)] + [-a(0 \cdot W, q_0), +a(W, q_1)] + [-a(0 \cdot W, q_1), +a(W, q_2)]
\end{aligned}
$$

<caption>Figure 56.1: An NFA accepting words finishing by 00 and its translation in stellar resolution. We have $\zeta \mathrm{IEx}(A^\star, [+i(0 \cdot 0 \cdot 0 \cdot \varepsilon)]) = [\mathrm{accept}]$.</caption>

[accept] cannot interact because its only ray is unpolarised. It follows that it must be part of the normal form and [accept] ∈ $\zeta \mathrm{IEx}(A^\star, w^\star)$.

We have to check that cyclic diagrams do not cause problems. Transitions are encoded as binary stars, hence a cyclic diagram is necessarily closed and will reduce into a loop on a binary star. This kind of loop involves an equation of the form $c \cdot W \stackrel{?}{=} W$ (because of the linear consumption of the input), which is impossible to solve. Such diagrams will be excluded in the computation of the normal form.

2. Assume $A(w) = 0$. It means that all runs are partial runs $\rho := (q_0, ..., q_n)$ where $q_n \notin F$. Since there is bijection between states of $\rho$ and symbols of $w$, we have $w = w_0...w_n$. By Lemma 56.4, these runs correspond to transitions $A^\star \vdash [+a(w, q_0)] \rightsquigarrow^* A^\star \vdash [+a(w, q_n)]$. Because of the operator $\zeta$, such polarised stars are erased. Hence, the normal form must be empty, i.e. $\zeta \mathrm{IEx}(A^\star, w^\star) = \emptyset$ and in particular $[\mathrm{accept}] \notin \zeta \mathrm{IEx}(A^\star, w^\star)$.

□

§56.6 **Remark (Incomplete path).** Remark that in the case $A(w) = 0$ of Lemma 56.4, partial runs lead to polarised stars which cannot interact anymore (or diagrams with polarised free rays). We could keep those incomplete paths but we choose to make them invisible by using the operator $\zeta$.

§56.7 Different encodings of words are also possible. For instance, in Aubert and Bagnol's works [AB14, ABS16], characters are encoded with flows forming a cyclic chain of $\alpha$-unifiable terms which interact with the encoding of the state graph of an automaton. This defines a representation of logspace computation where the input is explored with pointers.

§56.8 **Definition (Logspace words [AB14])**. Let $w = c_1..., c_n$ be a word together with distinct constants $p_0, p_1, ..., p_n$ where $p_i$ represents a position in $w$. The encoding of $w$ is
defined by:

$$
\begin{align*}
w^{\text{LOG}\star} &:= (\star \bullet r \bullet X \bullet (p_0 \bullet Y) \Leftrightarrow c_1 \bullet l \bullet X \bullet (p_1 \bullet Y))^{\star} \\
&\quad + \sum_{i=1}^{n-1} (c_i \bullet r \bullet X \bullet (p_i \bullet Y) \Leftrightarrow c_{i+1} \bullet l \bullet X \bullet (p_{i+1} \bullet Y))^{\star} \\
&\quad + (c_n \bullet r \bullet X \bullet (p_n \bullet Y) \Leftrightarrow \star \bullet l \bullet X \bullet (p_0 \bullet Y))^{\star}
\end{align*}
$$

where l, r are constants and • is a binary symbol considered right-associative, i.e. $t \bullet u \bullet v := t \bullet (u \bullet v)$.

Non-deterministic pushdown automata (NPDA)

§56.9 A non-deterministic pushdown automaton is an NFA with a stack defined as a tuple $P = (Q, \Sigma, \Gamma, \Delta, Q_0, \$, F)$ where $Q$ is the set of states, $\Sigma$ the alphabet of the input, $\Gamma$ the alphabet of the stack, $Q_0 \subseteq Q$ the set of initial states, $F \subseteq Q$ the set of final states, $\$ \in \Gamma$ is the initial stack symbol and $\Delta : Q \times \Sigma_{\varepsilon} \times \Gamma_{\varepsilon} \to \mathcal{P}(Q \times \Gamma_{\varepsilon})$ is the transition function.

§56.10 We say that $P$ accepts $w = c_1...c_n \in \Sigma^*$, written $P(w) = 1$, when there exists $q_0, ..., q_n \in Q$ and $s_0, ..., s_n \in \Gamma^*$ such that $q_0 \in Q_0$, $s_0 = \varepsilon$, $q_n \in F$ and for $0 \le i \le n-1$, we have $(q_{i+1}, b) \in \Delta(q_i, c_{i+1}, a)$ where $s_i = a \cdot t$ and $s_{i+1} = b \cdot t$ for some $a, b \in \Gamma_{\varepsilon}$ and $t \in \Gamma^*$. In particular, if $a = \varepsilon$, then $b$ is just added on the stack and if $b = \varepsilon$ then we simply pop $a$. Otherwise, we replace the symbol $a$ by $b$ on the top of the stack. Otherwise, $w$ is rejected by $P$, which is written $P(w) = 0$.

§56.11 **Definition (Encoding of non-deterministic pushdown automata).** The encoding of a NPDA $P = (Q, \Sigma, \Gamma, \Delta, Q_0, \$, F)$ is defined by $P^* \text{ such that:}$

- for each $q_0 \in Q_0$, we have $[-i(W), +p(W, q_0, \$)];$

- for each $q_f \in F$, we have $[-p(\varepsilon, q_f, S), \text{accept}]$;

- for each $q \in Q$, $c \in \Sigma_{\varepsilon}$ and for each $(q', b) \in \Delta(q, c, a)$ such that $a, b \in \Gamma_{\varepsilon}$, we have:

- $[-p(c \cdot W, q, S), +p(W, q', S)]$ when $a = \varepsilon$ and $b = \varepsilon$;

- $[-p(c \cdot W, q, S), +p(W, q', b \cdot S)]$ when $a = \varepsilon$ and $b \neq \varepsilon$;

- $[-p(c \cdot W, q, a \cdot S), +p(w, q', S)]$ when $a \neq \varepsilon$ and $b = \varepsilon$;

- $[-p(c \cdot W, q, a \cdot S), +p(w, q', b \cdot S)]$ when $a \neq \varepsilon$ and $b \neq \varepsilon$.

If $c = \varepsilon$, as for NFA, it disappears from the interpretation and we have simply $W$ instead of $\varepsilon \cdot W$ in the above four cases.
**§56.12 Lemma (Stack management).** Let $P$ be a NPDA and $w$ be a word. If $\Delta(q, c, a) = \{(q_1, b_1), \dots, (q_n, b_n)\}$, then for any term $s$ representing a stack:

1. $P^\star \vdash [+p(q, c \cdot w, s)] \rightsquigarrow P^\star \vdash \sum_{i=1}^n [+p(q_i, w, s)]$ when $a = \varepsilon$ and $b = \varepsilon$;

2. $P^\star \vdash [+p(q, c \cdot w, b \cdot s)] \rightsquigarrow P^\star \vdash \sum_{i=1}^n [+p(q_i, w, s)]$ when $a = \varepsilon$ and $b \neq \varepsilon$;

3. $P^\star \vdash [+p(q, c \cdot w, a \cdot s)] \rightsquigarrow P^\star \vdash \sum_{i=1}^n [+p(q_i, w, s)]$ when $a \neq \varepsilon$ and $b = \varepsilon$;

4. $P^\star \vdash [+p(q, c \cdot w, a \cdot s)] \rightsquigarrow P^\star \vdash \sum_{i=1}^n [+p(q_i, w, b \cdot s)]$ when $a \neq \varepsilon$ and $b \neq \varepsilon$.

*Proof.* The proof follows from matchability and case analysis of the encoding of NPDA. We only look at the last case and the other ones are similar. Assume $a \neq \varepsilon$ and $b \neq \varepsilon$. We have $P^\star \vdash [+p(q, c \cdot w, a \cdot s)]$. It can interact with stars $[-p(q, c \cdot W, a \cdot S), +p(q_i, W, b \cdot S)]$ encoding the transitions $(q_i, b_i) \in \Delta(q, c, a)$. By fusion, we have:

$$[+p(q, c \cdot w, a \cdot s)] \triangledown [-p(q, c \cdot W, a \cdot S), +p(q_i, W, b \cdot S)] = +p(q_i, w, b \cdot s).$$

Hence, we obtain $P^\star \vdash \sum_{i=1}^n [+p(q_i, w, b \cdot s)]$, as expected. $\square$

**§56.13 Theorem (Simulation of non-deterministic pushdown automata).** Let $P$ be a NPDA and $w$ be a word. We have:

1. if $P(w) = 1$, then $[accept] \in \mathfrak{IEx}(P^\star, w^\star)$;

2. if $P(w) = 0$, then $[accept] \notin \mathfrak{IEx}(P^\star, w^\star)$.

*Proof.* The proof follows exactly the same idea as in Theorem 56.5. NPDA are NFA extended with a stack, hence it only remains to show that the treatment of the stack is sound. This follows from Lemma 56.12. $\square$

**§56.14** An example of pushdown automata recognising the language $\{0^n1^n \mid n \ge 0\}$ is illustrated in Figure 56.2.

Finite sequential transducers (NFST)

**§56.15** Transducers are automata which can output symbols at each transition. When reaching a final state, a whole word is produced. The idea of the encoding is simple: we use a stack as in the encoding of NPDA and simply output this stack in the final state with an unpolarised variable replacing *accept*.

**§56.16** A finite sequential transducer is defined as a tuple $T = (\Sigma, \Gamma, Q, Q_0, \Delta, F)$ corresponding to an NFA $(\Sigma, Q, Q_0, \Delta, F)$ extended with a language of output $\Gamma$ and a transition function $\Delta : Q \times \Sigma_\varepsilon \to \mathcal{P}(Q \times \Gamma_\varepsilon)$.
<figure><img src="image_106.png" /></figure>

$$P^★ = [-i(W), +p(W, q_0, $)] + [-p(\epsilon, q_3, $), accept] +$$

$$[-p(0 \cdot W, q_0, S), +p(W, q_0, 0 \cdot S)] + [-p(1 \cdot W, q_0, 0 \cdot S), +p(W, q_1, S)] +$$

$$[-p(1 \cdot W, q_1, 0 \cdot S), +p(W, q_1, S)] + [-p(W, q_1, $), +p(W, q_2, $)]$$

Figure 56.2: A transition $a, b \to c$ means that we read $a$ and replace $b$ on the stack by $c$. The idea is to add 0 on the stack for each 0 read on the input then decrease by the same number for each 1 read. If we reach the initial stack symbol $>$, then we necessarily have as many 0s as 1s.

§56.17 **Definition** (Encoding of non-deterministic finite sequential transducers). Let $T = (Σ, Γ, Q, Q_0, Δ, F)$ be an NFST. Its encoding is defined by $A^★$ such that:

* for each $q_0 \in Q_0$, we have $[-i(W), +f(W, q_0, ε)]$;

* for each $q_f \in F$, we have $[-f(ε, q_f, S), S]$;

* for each $q \in Q$ and if $c \in Σ_ε$ and $c' \in Γ_ε$ and for each $(q', c') \in Δ(q, c)$, we have:

$$[-f(c \cdot W, q, S), +f(W, q', c' \cdot S)].$$

If $c = ε$, the transition is translated into $[-f(W, q, S), +f(W, q', c' \cdot S)]$. If $c' = ε$ then we have $S$ instead of $ε \cdot S$.

§56.18 It is possible to extend even more the encoding of transducers, by using two stacks which explores the input by going to the left or to the right, thus obtaining 2-way transducers [BC18]. But instead of exploring this idea, we will use these two stacks for the interpretation of Turing machines in order to assert the Turing completeness of stellar resolution.

## Non-deterministic Turing machines (NTM)

§56.19 Non-deterministic Turing machines (NTM) have been defined in Paragraph 16.5. For the encoding, we use the facts that Turing machines can be represented with two stacks in order to represent the left and right part of a tape. A move of the head will be represented as a manipulation of stack.

§56.20 We use terms $m(L, Q, X, R)$ where $L$ and $R$ are the left and right part of the tape relatively to the current position of the head. The variables $Q$ and $X$ respectively
represent the current state and symbol read by the head. We implicitly consider the
symbol • as left-associative (hence a • b • c = (a • b) • c) and ◦ right-associative (hence
a ◦ b ◦ c = a ◦ (b ◦ c)) so that it looks like we are traversing a tape.

§56.21 **Convention (New encoding of words).** For technical reasons, Turing machines use the same encoding of words as before but with · replaced by ◦ (but the priority does not change). This is because at the beginning of the machine, the word is loaded on the right-hand tape.

§56.22 **Definition (Encoding of non-deterministic Turing machines).** The encoding of an NTM $M = (Q, \Gamma, \Delta, q_0, q_a, q_r)$ is defined by a constellation $M^\star$ such that:

• $q_0$ is translated into $[-i(C \circ W), +m(\Box, q_0, C, W)] + [-i(\Box), +m(\Box, q_0, \Box, \Box)]$;

• $q_a$ is translated into $[-m(L, q_a, X, R), \mathbf{accept}]$;

• $q_r$ is translated into $[-m(L, q_r, X, R), \mathbf{reject}]$;

• for each $q \in Q$ and $c \in \Gamma_{\Box}$ such that $(q', c', d) \in \Delta(q, c)$:

- if $d = 1$ (going left) then we have $[-m(L \bullet X, q, c, R), +m(L, q', X, c' \circ R)]$;

- if $d = \mathbf{r}$ (going right) then we have $[-m(L, q, c, X \circ R), +m(L \bullet c', q', X, R)]$;

- if $d = \mathbf{s}$ (staying still) then we have $[-m(L, q, c, R), +m(L, q', c', R)]$;

• we add two additional “memory allocation stars”:

$$[-m(\Box, Q, C, R), +m(\Box \bullet \Box, Q, C, R)] + [-m(L, Q, C, \Box), +m(L, Q, C, \Box \circ \Box)].$$

§56.23 The two last stars are used to dynamically allocate space on the tape when necessary (similarly to `malloc()` in the C language). Instead of considering Turing machines as word acceptors, it is also possible to output the content of the tape and hence compute functions by translating $q_a$ into $[-m(L, q_a, X, R), \mathbf{accept}(L, X, R)]$.

§56.24 **Lemma (Simulation of transitions).** Let $M$ be an NTM and $w$ be a word. If

$$(q', c', d) \in \Delta(q, c),$$

then:

• if $d = 1$, then $M^\star \vdash [-m(l \bullet a, q, c, r)] \rightsquigarrow M^\star \vdash [+m(l, q', a, c' \circ r)]$;

• if $d = \mathbf{r}$, then $M^\star \vdash [-m(l, q, c, a \circ r)] \rightsquigarrow M^\star \vdash [+m(l \bullet c', q', a, r)]$;

• if $d = \mathbf{s}$, then $M^\star \vdash [-m(l, q, c, r)] \rightsquigarrow M^\star \vdash [+m(l, q', c', r)]$.

*Proof.* As for Theorem 56.13, this follows from a case analysis and from term unification.
We only do the first case and the other cases are similar. Assume that we have $d = 1$ and
$M^\star \vdash [-m(l \bullet a, q, c, r)]$. It can interact with $[-m(L \bullet X, q, c, R), +m(L, q', X, c' \circ R)]$. By fusion, we obtain $[+m(l, q', a, c' \circ r)]$. $\square$

**§56.25 Theorem (Simulation of non-deterministic Turing machines).** Let $M$ be an NTM and $w$ be a word. We have:

1. if $M(w) = 1$, then $M^\star \vdash w^\star \rightsquigarrow^* M^\star \vdash \Psi$ with $[accept] \in \Psi$;

2. if $M(w) = 0$, then $M^\star \vdash w^\star \rightsquigarrow^* M^\star \vdash \Psi$ with $[reject] \in \Psi$;

3. if $M(w) = \infty$ and $M^\star \vdash w^\star \rightsquigarrow^* M^\star \vdash \Psi$ then $[accept], [reject] \notin \Psi$.

*Proof.* The proof is similar to the proof of Theorem 56.5. We show the two statements.

1. Assume $M(w) = 1$. We must have a sequence of configurations $\rho := (C_0, \dots, C_n)$ such that $C_n = (l, q_0, r)$ and $C_n = (l', q_a, r')$ for some $l, l', r$ and $r'$. We start from $M^\star \vdash w^\star$. The star $w^\star$ can interact with the initial star and we obtain either $[+m(\sqcup, q_0, c, w)]$ for some word $c \circ w$ or $[+m(\sqcup, q_0, \sqcup, \sqcup)]$ depending on if $w \neq \varepsilon$ or $w = \varepsilon$. By Lemma 56.24, we can simulate the transitions of $M$. Each time there is a memory shortage, i.e. when we have $M^\star \vdash [+m(\sqcup, q', c', r')]$ and the next transition goes right, or $M^\star \vdash [+m(l', q', c', \sqcup)]$ and the next transition goes left, we need to allocate memory with the special memory allocation stars of the encoding. Without loss of generality, we only look at the case of right direction. We have $[+m(\sqcup, q', c', r')]$ which is matchable with $[-m(\sqcup, Q, C, R), +m(\sqcup \bullet \sqcup, Q, C, R)]$. By fusion, we obtain $[+m(\sqcup \bullet \sqcup, q', c', r')]$. We can then interact with the star encoding the next transition as in Lemma 56.24. By repeating this operation for all configurations of $\rho$, we will introduce duplications for non-deterministic choices. Eventually, since $M(w) = 1$, we should reach $[accept]$ which cannot interact, as in the proof of Theorem 56.5.

2. Assume $M(w) = 0$. This case is similar to the previous case since both are different classes of halting states.

3. Assume $M(w) = \infty$. The reasoning is the same as for Theorem 56.5. All sequences of configuration do not reach neither $q_a$ nor $q_r$. By simulating sequences of configurations with interactive execution, we can never reach $[accept]$ nor $[reject]$.

We have to check that cyclic diagrams cause no problems. Since Turing machines only use binary polarised stars, all cyclic diagrams must be closed. Consider such a cyclic diagram. If it is incorrect, then it does not appear in the normal form. In case it is correct, it represents a trivially infinite loop during the execution of the machine such as $[-m(L, q, c, R), +m(L, q, c, R)]$. This diagram has no effect on the presence or absence of $[accept]$ or $[reject]$ in the normal form. $\square$

**§56.26 Remark (Bounded memory allocation).** Remark that it is impossible to allocate too much memory because the allocation stars require that we have a tape equal to $\sqcup$.
Otherwise, we would have infinitely many diagrams for all the possible amount of
space allocation and no encoding of Turing machine would be strongly normalising.

§56.27 An example of Turing machine and its encoding is given in Figure 56.3. Although we have shown an example of *deterministic* Turing machine, it is easy to see how the non-deterministic case works. We can have several choices so that a same transition can match with several transitions. This will necessarily yield several diagrams corresponding to different runs. The whole machine accepts the input when at least one run accepts the word.

**57 More advanced machines**

**Alternating Turing machines (ATM)**

§57.1 Alternating Turing machines are Turing machines with two classes of states: existential (∨) and universal (�w) states. We use a function class : Q → {∃, ∧} in order to associate a class with states.

§57.2 The acceptation is slightly modified: in order for an ATM $M$ to accept a word $w$ (with the usual notation $M(w) \in \{1,0,\infty\}$), we require that in the computation tree of $M$, all children of $\wedge$ nodes are accepting paths and at least one of the children of $\vee$ paths is accepting. The idea is that universal states compute in parallel. More formally, by using the notation used for automata, $M(w,q) = 1$ when:

• if class(q) = ∨, then there exists a sequence of configurations (C₁, ..., Cₙ) with C₁ = (c, q, w) for some c which is accepting (as for NTM);

• if class(q) = ∧, then *all* sequences of configurations (C₁, ..., Cₙ) with C₁ = (c, q, w) for some c are accepting.

We have $M(w) = 1$ when for all state $q$ of $M$, we have $M(w,q) = 1$. Rejection is similar but with $q_r$ instead of $q_a$. The case of NTM is a special case where all states are of type $\vee$ (because non-determinism only requires one path to succeed).

§57.3 In order to reproduce the computation of an ATM $M$ on a word $w$, we need a trick for the treatment of $\wedge$ states. Instead of using the non-determinism of constellations which would induce several parallel diagrams, a $\wedge$ state $q \in Q$ of $n > 1$ outputs should be represented by a star of $n$ outputs (polarity $+$) so that all paths from $q$ are part of the same diagram. Since in our definition of NTM, all paths terminate either on **accept** or **reject**, it is sufficient to require that if $M(w) = 1$, then $\text{Ex}(M^\star + w^\star)$ contains at least one star [**accept**, ..., **accept**] for $k \ge 1$. Otherwise, if there is at least one **reject**, it means that some paths from a $\wedge$ state has been rejected or that no paths of $\vee$ states are accepting.
<figure><img src="image_107.png" /></figure>

$$
\begin{align*}
M^* &= [-i(C \circ W), +m(\Box, q_0, C, W)] + [-i(\Box), +m(\Box, q_0, \Box, \Box)] + \\
&\quad [-m(L, q_0, \Box, R), +m(L, q_a, \Box, R)] + [-m(L, q_2, \Box, R), +m(L, q_r, \Box, R)] + \\
&\quad [-m(L, q_0, \$C \circ R), +m(L \bullet \$, q_0, C, R)] + [-m(L, q_2, \$C \circ R), +m(L \bullet \$, q_2, C, R)] + \\
&\quad [-m(L, q_0, a, C \circ R), +m(L \bullet \$, q_2, C, R)] + [-m(L, q_2, a, C \circ R), +m(L \bullet a, q_2, C, R)] + \\
&\quad [-m(L, q_0, b, C \circ R), +m(L \bullet \$, q_3, C, R)] + [-m(L \bullet C, q_2, b, R), +m(L, q_1, C, \$ \circ R)] + \\
&\quad [-m(L, q_1, \Box, C \circ R), +m(L \bullet \Box, q_0, C, R)] + [-m(L, q_3, \Box, R), +m(L, q_r, \Box, R)] + \\
&\quad [-m(L \bullet C, q_1, \$R), +m(L, q_1, C, \$ \circ R)] + [-m(L, q_3, \$C \circ R), +m(L \bullet \$, q_3, C, R)] + \\
&\quad [-m(L \bullet C, q_1, a, R), +m(L, q_1, C, a \circ R)] + [-m(L \bullet C, q_3, a, R), +m(L, q_1, C, \$ \circ R)] + \\
&\quad [-m(L \bullet C, q_1, b, R), +m(L, q_1, C, b \circ R)] + [-m(L, q_3, b, C \circ R), +m(L \bullet b, q_3, C, R)] + \\
&\quad [-m(L, q_a, X, R), \mathbf{accept}] + [-m(L, q_r, X, R), \mathbf{reject}] + \\
&\quad [-m(\Box, Q, C, R), +m(\Box \bullet \Box, Q, C, R)] + [-m(L, Q, C, \Box), +m(L, Q, C, \Box \circ \Box)]
\end{align*}
$$

<caption>Figure 56.3: A Turing machine accepting words containing as many symbols **a** as symbols **b** where $a \to b, d$ from a state **q** to **q'** corresponds to a transition $\Delta(\mathbf{q}, a) = (\mathbf{q}', b, d)$. When computing $\mathbf{IEx}(M^*, a^*)$, we plug the input with the correct initial star and obtain $[+m(\Box, q_0, a, \Box)]$. No star can be connected, hence we have to connect to the right allocation star and obtain $[+m(\Box, q_0, a, \Box \circ \Box)]$. We can use the star corresponding to $a \to \$, \mathbf{r}$ and obtain $[+m(\Box \bullet \$, q_2, \Box, \Box)]$. Since we read $\Box$, we use the star corresponding to the transition $\Box \to \Box, \mathbf{s}$ and obtain $[+m(\Box \bullet \$, q_r, \Box, \Box)]$. We can only use the star corresponding to $q_r$ and obtain $\mathbf{reject}$. If we had a character **b** next to **a**, we would reach $\mathbf{accept}$.</caption>
**§57.4 Definition (Encoding of alternating Turing machines).** The encoding of an ATM $M = (Q, \Gamma, \Delta, q_0, q_a, q_r, \mathbf{class})$ is defined by a constellation $M^\star$ such that:

* $q_0, q_a$ and $q_r$ are translated as in Definition 56.22.

* for each $q \in Q$ and $c \in \Gamma_\varepsilon$ such that $(q', c', d) \in \Delta(q, c)$:

- if $\mathbf{class}(q') = \lor$, we have the star given in Definition 56.22;

- if $\mathbf{class}(q') = \land$, then for $q_i, c_i, d_i$ such that $(q_i, c_i, d_i) \in \Delta(q', c')$ for all $c'$ with $1 \le i \le k$, we have:

* $[-m(L \bullet X, q', c', R), +m(L, q_1, X, c_1 \circ R), \dots, +m(L, q_k, X, c_k \circ R)]$ when $d_i = 1$;

* $[-m(L, q', c', X \circ R), +m(L \bullet c_1, q_1, X, R), \dots, +m(L \bullet c_k, q_k, X, R)]$ when $d_i = 1$.

If $c = \varepsilon$ or $c' = \varepsilon$, then we do not write them in the stack as for Turing machines.

* we add two additional stars for memory allocation:

$$[-m(\Box, q, c, R), +m(\Box \bullet \Box, q, c, R)] + [-m(L, q, c, \Box), +m(L, q, c, \Box \circ \Box)].$$

**§57.5 Theorem (Simulation of alternating Turing machines).** Let $M$ be an ATM and $w$ a word. For $k > 0$, we have:

1. if $M(w) = 1$, then $M^\star \vdash w^\star \rightsquigarrow M^\star \vdash \Psi$ with $[\mathbf{accept}, \dots, \mathbf{accept}] \in \Psi$;

2. if $M(w) = 0$, then $M^\star \vdash w^\star \rightsquigarrow M^\star \vdash \Psi$ with $[\mathbf{reject}, \dots, \mathbf{reject}] \in \Psi$.

*Proof.* The proof follows the same idea as Theorem 56.25 since ATM are extensions of NTM. It remains to show that the behaviour associated with the types of states is correctly simulated. The case of $\lor$ states is identical to the behaviour of regular states in NTM. We show the first statement for $M(w) = 1$ with $w = c \circ w'$ for some $c$ and $w'$ (the case with $w = \varepsilon$ is similar to the one with Turing machines in Theorem 56.25). The case of $M(w) = 0$ is similar since these are both halting cases. Assume $M(w) = 1$. We show that for any universal state, interactive execution produces a star $[\mathbf{accept}, \dots, \mathbf{accept}]$ for some $n$.

We start from the interactive configuration $M^\star \vdash w^\star$. It will interact with the initial state and we obtain $M^\star \vdash w^\star \rightsquigarrow M^\star \vdash [+m(\Box, q_0, c, w)]$. Assume we have a non-deterministic transition to states $q_1, \dots, q_n, s_1, \dots, s_m$ such that $\mathbf{class}(q_i) = \lor$ and $\mathbf{class}(s_i) = \land$.

* For all $(q_i, c_i, d_i) \in \Delta(q_0, c)$, a copy of $[+m(\Box, q_0, c, w)]$ interacts with the star associated with the transition, as in Theorem 56.25. We obtain $\sum_{i=1}^n [+m(l_i, q_i, c'_i, r_i)]$ in the normal form with a choice of $l_i, c'_i$ and $r_i$ consistent with the translation of Turing machines into constellations.
* Without loss of generality, we consider the left case for directions $d_i = 1$. For all $(s_i, c_i, d_i) \in \Delta(q_0, c)$, a copy of $[+m(\llcorner, q_0, c, w)]$ interacts with the star $[-m(L \bullet X, q_0, c, R), +m(L, s_1, c_1, X \circ R), \dots, +m(L, s_m, c_m, X \circ R)]$. We have

$$ \phi := [+m(\llcorner, s_1, c_1, c \circ w), \dots, +m(\llcorner, q_m, c_k, c \circ w)] $$

in the normal form.

We finally obtain the stellar interaction:

$$ M^{\star} \vdash [+m(\llcorner, q_0, c, w)] \rightsquigarrow M^{\star} \vdash \sum_{i=1}^{n} [+m(l_i, q_i, c'_i, r_i)] + \phi $$

We can apply more transitions (either to existential or universal states) by triggering interaction between a selected ray on the right of $\vdash$ and stars associated with next transitions. During interactive execution we have interaction spaces $M^{\star} \vdash \sum_{i=1}^{n} \phi_i$ such that the $\phi_i$ are either stars $[+m(l', q', c', r')]$ for some $l', q', c'$ and $r'$ or stars

$$ [+m(l'_1, q'_1, c'_1, r'_1), \dots, +m(l'_n, q'_n, c'_n, r'_n)] $$

for some $l'_i, q'_i, c'_i$ and $r'_i$. By the proof of Theorem 56.25, each time a state reach the accepting state $q_a$, its corresponding ray is replaced by the unpolarised ray accept. If we obtain a star [accept, ..., accept] it means that all children of an universal state are accepting for one possible non-deterministic path. □

**§57.6** Remark that ATM are, structurally speaking, not so far from regular constellations. In stellar resolution, we have non-deterministic choices with several rays matchable with one single ray and branching with multiple rays in a star matchable which rays of other stars. The first situation generalises $\lor$ states and the second one $\land$ states. This may be coherent with known results regarding the linear relation between the complexity of logic programs and ATM [Sha84].

## Non-deterministic finite tree automata (NFTA)

**§57.7** The previous automata we described recognise words. In this section, we consider automata which recognise trees [CDG$^{+97}$]. By recognising trees, we can work on complex data types such as boolean formulas or arithmetic expressions for instance. In the literature, we usually have two types of NFTA: bottom-up NFTA which read the leaves and infer new states by going up and top-down NFTA which starts from the root and associate states with children. Since constellations deal with terms, we can naturally encode trees by using function symbols for nodes, which leads to an encoding of top-down NFTA.
$$[-ta(X, or(not(1), 1)), accept] + [+ta(q_0, 0)] + [+ta(q_1, 1)] + \\ [-ta(q_a, T_a), +ta(q_{max(a,b)}, or(T_a, T_b))] + [-ta(q_a, T_a), +ta(q_{1-a}, not(T_a))]$$

Figure 57.1: Constellation recognising trees correspond to true boolean formulas. In this example, it takes an instance of excluded middle as input.

§57.8 Formally, a top-down NFTA is a tuple $T = (Q, F, ar, Q_0, \Delta)$ where $Q$ is the set of states, $F$ is a set of function symbols, $ar: F \to N$ associates an arity with function symbols, $Q_0 \subseteq Q$ is the set of initial states and $\Delta$ is a set of transition rules of the form $q(f(x_1, ..., x_n)) \to f(q_1(x_1), ..., q_n(x_n))$ for $f \in F$, $ar(f) = n$, $q, q_1, ..., q_n \in Q$ and $x_1, ..., x_n$ variables. An input tree $t$ is accepted, written $T(t) = 1$, when it can be fully traversed by the transition rules by starting from a state $q \in Q_0$. Otherwise, it is rejected and we write $T(t) = 0$.

§57.9 **Definition (Syntactic encoding of trees).** Let $t$ be a tree. We define its encoding $t^\star$ inductively by:

* $X$ when $t$ is a leaf $x$;

* $f(t_1^\star, ..., t_n^\star)$ when $t$ is a node containing a symbol $f$ with $n$ children $t_1, ..., t_n$.

§57.10 **Definition (Encoding of top-down tree automata).** Let $T = (Q, F, ar, Q_0, \Delta)$ be a top-down NFTA. The encoding of $T$ is a constellation $T^\star$ defined as follows:

* for each $q_0 \in Q_0$, we have $[-i(T), +ta(q_0, T)];$

* for each $q(f(x_1, ..., x_n)) \to f(q_1(x_1), ..., q_n(x_n)) \in \Delta$, we have a constellation $[-ta(q, f(X_1, ..., X_n)), +ta(q_1, X_1)] + ... + [-ta(q, f(X_1, ..., X_n)), +ta(q_n, X_n)];$ and for each leaf $x$, we add the following star: $[-ta(q, X), accept]$.

§57.11 **Theorem (Simulation of top-down tree automata).** Let $t$ be a tree and $T$ be a top-down NFTA. We have $\llcorner \mathfrak{Ex}(T^\star + t^\star) \rrcorner \neq \emptyset$ if and only if $T(w) = 1$.

*Proof.* The simulation follows the same idea as for automata (cf. Theorem 56.5). Instead of a consumption of word, we have a decomposition of tree which has the same role. □

§57.12 Interestingly, bottom-up NFTA are encoded in the same way but with reversed polarities: we start from leaves and go up to the root. Moreover, since we start with all the leaves, we need final states instead of initial ones. Instead of deconstructing trees, we are constructing trees. An example of what would be constellation corresponding
to a bottom-up tree automaton recognising true booleans formulas is illustrated in Figure 57.1. By using these ideas, it is also possible to extend the previous models to trees instead of words.

## Krivine Abstract Machine (KAM) with call/cc

§57.13 The Krivine Abstract Machine (KAM) has already been defined in Section 22. I randomly had the idea to encode it into constellations but I am not very confident about the details. In this section, I only give the definitions without establishing any simulation result.

§57.14 The encoding of the $\lambda_c$-terms corresponds to an encoding of their syntax tree. We use the binding of variables already present in stellar resolution in order to create bound variables in $\lambda$-terms. We obtain a sort of $\lambda$-calculus with independent explicit substitutions [ACCL91]. The idea is that stars representing terms will be of shape $[-i(n_1, X_1), ..., -i(n_m, X_m), t]$ where $t$ is the encoding of a $\lambda_c$-term, $n_i$ are identifier of variables and $X_i$ are variables of stellar resolution appearing in $t$.

§57.15 To make things simple, we consider that variables under some scope of a $\lambda$ do not appear under another scope: there is no possible capture of variables. We can obtain this situation by simply renaming bound variables in a term. I tried to take scopes into account so that it would work for any $\lambda$-term but it was horrible to define and too technical to be understandable.

§57.16 **Definition (Encoding of processes).** We write $V_\lambda$ for the set of variables of $\lambda_c$-calculus and define a bijection $\sigma : V_\lambda \to \mathbb{N}$ between variables of $\lambda_c$-calculus and natural numbers and a bijection $\nu : V_\lambda \to V$ between variables of $\lambda_c$-calculus and variables of stellar resolution. First, we associate a term with $\lambda_c$-terms and stacks:

$$ 
\begin{array}{l@{\qquad}l@{\qquad}l@{\qquad}l}
x^{\bullet} & := \nu(x) & (\lambda x.M)^{\bullet} & := l(\overline{\sigma(x)}, M^{\bullet}) & (MN)^{\bullet} := a(M^{\bullet}, N^{\bullet}) & \text{cc}^{\bullet} := \text{cc} \\
& & \mathbf{k}_{\pi}^{\bullet} & := s(\pi^{\bullet}) & \varepsilon^{\bullet} := \varepsilon & (M \cdot \pi)^{\bullet} := M^{\bullet} \cdot \pi^{\bullet}
\end{array}
$$

The encoding of $\lambda_c$-terms and stacks is defined as follows with an index $\alpha \in \mathbb{N}$ associated with terms in order to construct their syntax tree:

$$ 
\begin{array}{l@{\qquad}l@{\qquad}l}
x_{\alpha}^{\star} & := [-i(\overline{\sigma(x)}, \nu(x)), +T_{\alpha}(x^{\bullet})] & (Y \neq \nu(x)) \\
(\lambda x.M)_{\alpha}^{\star} & := M_{\alpha \cdot 0}^{\star} + [-T_{\alpha \cdot 0}(X), +T_{\alpha}(l(\overline{\sigma(x)}, X))] & \\
(MN)_{\alpha}^{\star} & := M_{\alpha \cdot 0}^{\star} + N_{\alpha \cdot 1}^{\star} + [-T_{\alpha \cdot 0}(X), -T_{\alpha \cdot 1}(Y), +T_{\alpha}(a(X, Y))] & \\
\text{cc}_{\alpha}^{\star} & := [+T_{\alpha}(\text{cc}^{\bullet})] & (\mathbf{k}_{\pi})_{\alpha}^{\star} := [+T_{\alpha}(\mathbf{k}_{\pi}^{\bullet})] & \pi^{\star} := [+S(\pi^{\bullet})]
\end{array}
$$
Finally, processes $M \star \pi$ are constructed with a star

$$ (M \star \pi)^{\star} := \mathrm{Ex}(M_{\varepsilon}^{\star} + \pi^{\star} + [-T_{\varepsilon}(X), -S(Y), +P(X \star Y)]) $$

connecting terms and stacks where $\star$ is a binary infix symbol and $\varepsilon \cdot \alpha = \alpha$ and $\varepsilon$ is not written when alone. Since it will never be composed, we do not define priorities for $\star$.

**§57.17 Example.** We have $(\lambda x.x)^{\star} = [-i(0, X), +T_0(X)] + [-T_0(x), +T(l(0, x))]$ which normalises into $[-i(0, X), +T(l(0, X))]$. Notice that the ray $-i(0, X)$ acts as an explicit substitution bound to $X$. When providing $[+i(0, u)]$ for some term $u$, the two stars merge and we obtain $[+T(l(0, u))]$ which indeed corresponds to a substitution. The process of $\beta$-reduction can be simulated with a star

$$ [-T_{\alpha}(a(l(n, X), u)), +T_{\alpha}(X)] + [+i(n, u)] $$

which destructs a pattern of redex and produce a new term with the body of the function in which all occurrences of variables of identifier $n$ are replaced by $u$ thanks to the substitution star $[+i(n, u)]$.

**§57.18 Lemma.** Let $t$ be a $\lambda_c$-term. We have:

$$ \mathrm{Ex}(M_{\alpha}^{\star}) = [-i(\overline{\sigma(x_1)}, \nu(x_1)), \dots, -i(\overline{\sigma(x_n)}, \nu(x_n)), +T_{\alpha}(M^{\bullet})] $$

for $x_1, \dots, x_n$ the variables in $M$.

*Proof.* The translation of $\lambda_c$-term is designed so to give the encoding of their syntax tree. The only remaining free rays are the rays $-i(n, x)$ (for each variables appearing in the term) which corresponds to explicit substitutions $[x := \cdot]$ waiting for a value, and a ray $+T(M^{\bullet})$ where $M^{\bullet}$ is a representation of the $\lambda_c$-term being constructed. $\square$

**§57.19 Definition (Encoding of Krivine Abstract Machines).** The KAM is encoded as the constellation $K^{\star}$ made of the following stars:

$$ [-P(a(M, N) \star \pi), +P(M \star N \cdot \pi)] \qquad (\mathrm{Push}) $$

$$ [-P(l(X, M) \star N \cdot \pi), +P(M \star \pi), +i(X, N)] \qquad (\mathrm{Grab}) $$

$$ [-P(cc \star M \cdot \pi), +P(M \star k_{\pi} \cdot \pi)] \qquad (\mathrm{Save}) $$

$$ [-P(k_{\pi} \star M \cdot \pi'), +P(M \star \pi)] \qquad (\mathrm{Restore}) $$

**§57.20 Example.** We would to evaluate $(\lambda xy.x)z$. We start from the construction of the $\lambda_c$-term given by Lemma 57.18. It produces the star:

$$ [-i(0, X), -i(1, Y), -i(2, Z), +T(a(l(0, l(1, X)), Z))]. $$
When put together with an empty stack to form a process and we obtain:

$$[-i(0, X), -i(1, Y), -i(2, Z), +P(a(l(0, l(1, X)), Z) \star \varepsilon)].$$

By fusion with the push star then the grab star, we obtain:

$$ \begin{array}{l} \mathop{\text{push}} \limits_{\rightsquigarrow} \quad [-i(0, X), -i(1, Y), -i(2, Z), +P(l(0, l(1, X)) \star Z \cdot \varepsilon)] \\ \mathop{\text{grab}} \limits_{\rightsquigarrow} \quad [-i(1, Y), -i(2, Z), +P(l(1, Z) \star \varepsilon)] \\ \qquad = [-i(1, Y), -i(2, Z), +P((\lambda y.z)^{\bullet} \star \varepsilon)] \end{array} $$

# 58 Generalised circuits

§58.1 Boolean circuits have been introduced in Section 18. However, in this section, we do not directly encode boolean circuits but suggest a notion of *generalised circuits*. These circuits are acyclic and connected hypergraph structures in which information flows from inputs to a unique output and in which hyperedges are able to perform function calls from a semantics called *module*. This subsumes boolean circuits, arithmetic circuits but also opens the model of atypical circuits (or other variants with several outputs or other weird models we can imagine).

§58.2 **Definition (Module).** A module is a tuple $(X, L, \mathbf{ar}, [[\cdot]])$ where $X$ is a set of values, $L$ is a set of labels, $\mathbf{ar} : L \to \mathbf{N} \times \mathbf{N}$ a function associating an input-output arity to labels and $[[\cdot]]$ associates with any label $l \in L$ a computable total function $X^n \to X^m$ such that $\mathbf{ar}(l) = (n, m)$.

§58.3 **Example.** Boolean circuits are constructed with the module $(X, L, \mathbf{ar}, [[\cdot]])$ with:

* $X := \{0, 1\}$ and $V := \{x_i, i \in \mathbf{N}\}$;

* $L := \{0, 1, x_i \in V, s, \neg, \wedge, \vee, c\}$;

* $\mathbf{ar}(b) = (0, 1)$ for $b \in \{0, 1\}$ and $[[b]] = b$;

* $\mathbf{ar}(s) = (1, 2)$ and $[[s]](x) = (x, x)$;

* $\mathbf{ar}(\neg) = (1, 1)$ and $[[\neg]](x) = 1 - x$;

* $\mathbf{ar}(\wedge) = (2, 1)$ and $[[\wedge]](x, y) = \min(x, y)$;

* $\mathbf{ar}(\vee) = (2, 1)$ and $[[\vee]](x, y) = \max(x, y)$;

* $\mathbf{ar}(c) = (1, 0)$ and $[[c]](x)$ is undefined.
**§58.4 Definition (Generalised circuit).** A *generalised circuit* is a tuple $(C, M, \kappa)$ of:

• an acyclic and connected hypergraph $C = (V, E, \mathbf{in}, \mathbf{out})$ where elements of $V$ are called *ports* and elements of $E$ are called *gates*;

• a module $M = (X, L, \mathbf{ar}, [[\cdot]])$;

• the total function $\kappa : E \to L$ associates a label with each gate $e \in E$. We require that $|\mathbf{in}(e)| = n$ and $|\mathbf{out}(e)| = m$ when $\mathbf{ar}(\kappa(e)) = (n, m)$.

There exists some special gates:

• output gates $e$ such that $\mathbf{out}(e) = \emptyset$;

• input gates $e$ such that $\mathbf{in}(e) = \emptyset$.

We require that a generalised circuit has at least one input gate and a *unique* output gate.

**§58.5 Definition (Evaluation of generalised circuits).** Let $(C, M, \kappa)$ be a generalised circuit with $C = (V, E, \mathbf{in}, \mathbf{out})$ and $M = (X, L, \mathbf{ar}, [[\cdot]])$. Its evaluation is given by a function $\mathbf{val}$ such that $\mathbf{val}(C) \in X$. It is defined as follows, where $o$ is the only output gate of $C$:

• $\mathbf{val}(C) := \mathbf{val}(o)$;

• if $e \in E$ is an input gate then $\mathbf{val}(e) = [[e]]$;

• for all $e$ such that $\mathbf{in}(e) = \{i_1, ..., i_n\}$ with parents $\{e_k \in E \mid i_k \in \mathbf{out}(e_k)\}$, we have $\mathbf{val}(e) = [[\kappa(e)]](\mathbf{val}(e_1), ..., \mathbf{val}(e_n))$.

**§58.6 Example.** A boolean circuit is any generalised circuit using constructors of Example 58.3. It is easy to extend the interpretation to arithmetic circuits by changing the module and replacing boolean functions by computable arithmetic functions. Conjunction is replaced by multiplication and disjunction by addition. Theoretically, we are not limited to computable functions but using computable functions guarantees that the circuit can be realised in stellar resolution.

**§58.7 Imperative programs.** If we allow loops and define ways to handle them, it might be possible to also represent imperative programs by considering the structure of the execution flow graph of a program and then passing states containing a memory (representing as a matrix over $\{0, 1\}$ for instance). We are also able to do function calls since functions are attached to constructors. I do not investigate this idea here.

**§58.8 Definition (Encoding of generalised circuits and modules).** Let $(C, M, \kappa)$ be a generalised circuit with $C = (V, E, \mathbf{in}, \mathbf{out})$ and $M = (X, L, \mathbf{ar}, [[\cdot]])$. We translate $C$ into a constellation $C^\star := \sum_{e \in E} e^\star$. Assume that $\mathbf{in}(e) = \{i_1, ..., i_n\}$ and $\mathbf{out}(e) =$
`{o₁, ..., oₘ}`. The translation of *e* is defined by a star

$$e^{\star} := \begin{bmatrix} -i_1(X_1), & \dots, & -i_n(X_n), \\ +o_1(Y_1), & \dots, & +o_m(Y_m) \end{bmatrix}$$

If *e* is a conclusion gate, then we add unpolarised rays *Y*₁, ..., *Y*ₘ to output the result and remove the function call *-κ(e)(X₁, ..., Xₙ, Y₁, ..., Yₘ)*.

For all label *l* ∈ *L* such that `ar(l) = (n, m)`, we define a star `l^star` by any star such that `IEx(l^star, [-l(a₁, ..., aₙ, Y₁, ..., Yₘ), Y₁, ..., Yₘ]) = [b₁, ..., bₘ]` and `[[l]](a₁, ..., aₙ) = (b₁, ..., bₘ)`.

The module *M* is translated into the constellation $M^{\star} := \sum_{l \in L} l^{\star}$.

**§58.9 Example.** It is possible to design a circuit for excluded middle with 1 as input:

$$[-1(X), +c_0(X)] + [-c_0(X), -s(X, Y, Z), +c_1(Y), +c_2(Z)] + [-c_1(X), -\neg(X, R), +c_3(R)] + [-c_2(X), -c_3(Y), -\wedge(X, Y, R), +c_4(R)] + [-c_4(R), R].$$

We need the constellation module:

$$[+1(1)] + [+s(X, X, X)] + [\neg(1, 0)] + [\neg(0, 1)] + [\neg(1, X, X)] + [\neg(0, X, 0)]$$

Remark that unused parts of the module can remain in the normal form except if we use the operator `\Z`, as for automata.

**§58.10** Notice that generalised circuits are purely structural waiting for some "function definitions". We have to plug its constellation with a module giving the semantics of gates. It shows that stellar resolution computes by internalising external procedures. In some sense, the syntax interacts with the semantics by expliciting hidden procedures.

**§58.11** **Variables.** It is possible to hijack the encoding of generalised circuits in stellar resolution in order to express satisfiability of boolean expressions. If we do not use constants, then some variables will wait for a value. For any input ray $-c_x(X)$ which is free in the dependency graph of the constellation, we can add a star $\phi_x := [-i(X) + c_x(X)]$ for variables. We can add stars $\sum_{b \in X} [+i(b)]$ so that $\phi_x$ will face a non-deterministic choice for all values The execution of the whole constellation will produce several stars for each combinations of inputs. It is also possible to add a variant of conclusion star $[-c_x(1), ok]$ with an explicit constant in order to ask for satisfiability of the circuit. If the output is 1 then we obtain the unpolarised star [ok]. By using such constellations it is possible to express the NP-complete satisfiability problem.
§58.12 **Example.** It is possible to design a circuit for excluded middle with unknown boolean inputs:

$$[-i(X), +c_0(X)] + [-c_0(X), -s(X, Y, Z), +c_1(Y), +c_2(Z)] +[-c_1(X), -\neg(X, R), +c_3(R)] +[-c_2(X), -c_3(Y), -\wedge(X, Y, R), +c_4(R)] +[-c_4(R), R].$$

We then add $[+i(1)] + [+i(0)]$ in the module and these two stars can be linked with $[-i(X), +c_0(X)]$. We will then obtain one result for all possible combinations of value. The presence of one star $[ok]$ indicates that the corresponding formula is satisfiable. For $n$ inputs, the presence of $2^n$ occurrences of $[ok]$ indicates that we have a tautology.

§58.13 When considering such circuits with input variables, we can plug value stars as in the previous example to fill values. We then obtain several circuits without input variables. It is then sufficient to consider generalised circuits without input variables.

§58.14 **Theorem (Simulation of generalised circuits).** Let $(C, M, \kappa)$ be a generalised circuit without input variables. We have $\zeta AEx(C^\star \uplus M^\star) = [\text{val}(C)]$. □

*Proof.* Assume $C := (V, E, \text{in}, \text{out})$ and that we have a hyperedge $e$ which is incident to another hyperedge $e'$ through a vertex $v$. This situation is translated by stars $\phi \cup \{+c_x(X_1, ..., X_n)\}$ and $\phi' \cup \{-c_y(Y_1, ..., Y_n)\}$ for variables $X_i$ and $Y_i$. By applying fusion, we have $\theta\phi \cup \theta\phi'$ with $\theta$ the solution of the equation induced by the rays we connected. We can apply execution on all stars of $C^\star$ first (this is later justified with the partial pre-execution lemma of Lemma 64.9) and we obtain a star $[-f_1(...), ..., -f_k(...), r]$ where $f_i$ corresponds to unsolved function call waiting for an interaction with $M^\star$, and $r$ is the only unpolarised ray corresponding to the only conclusion of $C$. Now, if implementations of functions in $M^\star$ are indeed correct (consistently with Definition 58.8), then when the remaining star interacts with $M^\star$, we must obtain $[\varphi(C)]$. All unused stars of $M^\star$ are erased by the operator $\zeta$. □

# 59 Tile systems with the abstract tile assembly model

§59.1 In this section, I choose to only encode the abstract tile assembly model (aTAM) mentioned and defined in Paragraph 17.7. Other tile systems can easily be encoded. For instance, Wang tiles' encoding can be directly inferred from the encoding of aTAM and flexible tiles correspond to stars with polarised ray of nullary colour (hence a polarised constant).

§59.2 We suggest an encoding of the aTAM in $\mathbb{N}^2$ instead of $\mathbb{Z}^2$ which is more natural but not less powerful since it is known that $\mathbb{N}^2 \simeq \mathbb{Z}^2$ and also because we are able to compute any computable function (since we previously encoded Turing machines).
§59.3 **Definition (Encoding of tiles).** Tile types $t_i = (g_w^i, g_e^i, g_s^i, g_n^i)$ are encoded by a star $t_i^\star$:

$$ \begin{bmatrix} \bullet(\mathbf{gl}(g_w^i)(X), X, Y), & \bullet(\mathbf{gl}(g_s^i)(Y), X, Y), \\ \circ(\mathbf{gl}(g_e^i)(s(X)), s(X), Y), & \circ(\mathbf{gl}(g_n^i)(s(U)), X, s(Y)) \end{bmatrix} $$

where $gl(g)(X) := g(X) \cdot \overline{str(g)}$ for $str(g) \in \mathbb{N}$.

We define the translation of a set of tile types $T$ as the constellation $T^\star := \sum_{t_i \in T} t_i^\star$.

§59.4 The symbols $h$ (horizontal) and $v$ (vertical) represent axis of connexion. The key point of the encoding is that because of the dots $\bullet$ and $\circ$, tiles have to use an intermediate star to check whether a connexion is allowed.

§59.5 **Definition (Environment constellation).** The environment constellation for a temperature $\tau \in \mathbb{N}\{0\}$ is defined by $\Phi_{env}^\tau :=$

$$ [+\text{temp}(\bar{\tau})] + \begin{bmatrix} \bullet(g_1(X_1) \cdot N_1, X_1, Y_1), & \circ(g_2(X_3) \cdot N_2, X_3, Y_3), \\ \circ(g_3(X_5) \cdot N_3, X_5, Y_5), & \circ(g_4(X_7) \cdot N_4, X_7, Y_7), \\ \circ(g_1(X_2) \cdot N_1, X_2, Y_2), & \circ(g_2(X_4) \cdot N_2, X_4, Y_4), \\ \circ(g_3(X_6) \cdot N_3, X_6, Y_6), & \circ(g_4(X_8) \cdot N_4, X_8, Y_8), \\ -\text{add}(N_1, N_2, R_1), & -\text{add}(N_3, N_4, R_2), \\ -\text{add}(R_1, R_2, R), & -\text{geq}(R, T, \bar{1}), -\text{temp}(T) \end{bmatrix} $$

$$ \begin{align*} & +[-\circ(g(X) \cdot \bar{0}, X, Y)] + [\circ(g(X) \cdot \bar{0}, X, Y)] + [-\circ(g(X) \cdot \bar{0}, X, Y)] + [\circ(g(X) \cdot \bar{0}, X, Y)] \\ & +[\circ(g(X) \cdot \bar{0}, X, Y)] + [-\circ(g(X) \cdot \bar{0}, X, Y)] + [\circ(g(X) \cdot \bar{0}, X, Y)] + [-\circ(g(X) \cdot \bar{0}, X, Y)] \\ & +[\text{geq}(\bar{0}, \bar{0}, \bar{1})] + [\text{geq}(s(X), s(Y), R), -\text{geq}(X, Y, R)] + [\text{geq}(s(X), \bar{0}, \bar{0})] + \\ & +[\text{geq}(\bar{0}, s(Y), \bar{0})] + [\text{add}(\bar{0}, Y, Y)] + [-\text{add}(X, Y, Z), \text{add}(s(X), Y, s(Z))] \end{align*} $$

§59.6 **Theorem (Simulation of the aTAM).** Let $\mathcal{T} = (T, \tau)$ be a TAS. We have

$$ \mathrm{CSatDiags}(T^\star + \Phi_{env}^\tau) \simeq \mathcal{A} \llcorner [\mathcal{T}]. $$

*Proof.* It is sufficient to show that the computation of $\mathrm{CSatDiags}(T^\star + \Phi_{env}^\tau)$ behaves like the construction of tilings in aTAM.

Direct connexions between tiles without using $\Phi_{env}^\tau$ is forbidden because of the symbols $\circ$ and $\bullet$. Notice that the colours $v$ and $h$ force the connexions to be on the same axis in order to follow the geometric restriction of tiling in a plane. The tiles are designed so that a plugging increment a coordinate $X$ or $Y$ depending on the position/axis of the side. The purpose of this feature is to simulate a shifting of tile on a plane so that two tiles cannot connect on two sides at the same time.
Because of the symbols ◦ and • , we have to use the constellation Φ τ env as an intermediate for the connexion of two tile sides. We consider a tile t$_{i}$ ∈ dom ( α ) . We start with t ⋆ i . Assume t$_{i}$ can be connected to k other tiles in dom ( α ) . They can only be connected through Φ τ env by their connectable sides. Their glue type and strength for the connected sides have to match because of the shared variables for opposite sides in Φ τ env . All other unused sides of the connector star will be plugged by the unary stars used as fillers. By using principles of logic programming, the diagram can only be correct and saturated if the sum of connected sides of t$_{i}$ is greater or equal to τ (note that the filled unused sides add 0 to the sum). The stars sing symbols add and geq are common logic programs, hence their correctness is assumed.

Since all $t_i \in \text{dom}(\alpha)$ satisfy the above property, the two operations have the same dynam-
ics. Moreover, each tile corresponds exactly to a star and each of its sides corresponds to
a ray and we have a structural isomorphism between tiles and their translation. It fol-
lows that we have a bijection between the set of non-empty finite assemblies constructible
from $T$ at temperature $\tau$ and $\text{CSatDiags}(T^\star + \Phi_{\text{env}}^\tau)$. $\square$

§59.7 **Encoding of Wang tiles.** Wang tiles can be recovered by considering the case of non-cooperative tiles with temperature $\tau = 1$ [MW17], considering all strengths to be 0 and removing the environment constellation. Glue types then correspond to colours of Wang tiles. This works because like Wang tiles, tiles of aTAM are also bricks placed on a plane.

60 Discussion: a common language for classical computation?

§60.1 In this chapter, I presented the encoding of a lot of different models of computation. However, when I talk about it to other people, they often say “but your model is Turing-complete so it’s not very surprising. Any Turing-complete model can do the same”. But do all encodings have the same value? Intuition tells us that no: encoding $\lambda$-calculus into proof-nets seems more interesting that encoding $\lambda$-calculus with Turing machines. But why? I am not sure about that... How to differentiate an encoding which *reveals* more about the computational mechanisms of an object and another one which is only superfluous bureaucracy? Even though I do not have answer, I would like to write about several remarkable points appearing in the encodings I defined. I believe that it can potentially raise interesting questions about classical computation.

§60.2 **What models of computation share.** As discussed in Section 19, it seems to me that the main models of computation are all about basic information flowing inside a discrete structure (typically a graph or a hypergraph). This is the elementary mechanism that stellar resolution implements. Constellations are about basic information (expressed with terms) moving between points in a network.
* With Horn clauses, a path of inference trying to justify a query then several statement traverse the knowledge base of a logic program.

* In automata theory, we have information about states transferred from one state to another. Typical data exchanged are the different stacks of information such as information about how many characters are remaining in the input or information needed to start the next transition.

* In boolean and arithmetic circuits, data such as numbers or booleans moves from inputs to the unique output. During the traversal of the circuit, these data are altered by some functions (e.g. boolean gates).

* In tile systems it is more subtle but geometric information about position and the structure of space (coordinates in a plane) are exchanged between tiles.

* Finally, with the GoI (cf. Chapter 5), we have seen with the token machine and the long trip criterion that we could travel inside a proof-structure by following some rules in order to express cut-elimination and logical correctness.

This idea of basic information flowing inside a structure is very primitive. It seems to generalise most classical models of computation without serious rise of complexity or unnatural hacks. A similar idea has been developed with (labelled) transition systems used in model checking [BK08, Chapter 2]. Compared to other similar models, stellar resolution has the advantage of being self-sufficient, without the need for external procedures. It only uses term unification which is triggered when making two stars interact.

§60.3 Automata as constellations with stacks. I remarked a small but funny thing about the encoding of automata in stellar resolution. Notice that our encoding of words is simply a stack of characters and that consuming a character (by using a star `[-a(c · w), +a(w)]`) is the dual operation of adding a character (by using a star `[-a(w), +a(c · w)]`). In stellar resolution, these operations only differ by the polarity of terms and the direction of computation (given by the initial and final state). We obtain three types of stacks: *strictly decreasing* (SD), *strictly increasing* (SI) and *arbitrary* (A) which can be both increasing or decreasing. The difference between NFA and NPDA are the number of stacks they use and how these stack are used: SD-stack for NFA and both an SD-stack and an A-stack for NPDA.

§60.4 Using an additional SI-stack and replacing *accept* by the content of this new stack can actually naturally lead to transducers which have the additional feature of writing symbols. By assembling stacks of different types of stacks over the encoding of a graph, we obtain the most common state machines (Figure 60.1). It seems to me that it is also possible to manipulate collapsible pushdown automata [HMOS08] which manipulate higher order stacks (stacks of stacks). Since stacks in stellar resolution are terms (made by composition function symbols to stack symbols), they can be manipulated as any other terms.
<table><caption>Figure 60.1: Characterisation of automata by number and types of stacks.</caption><thead><tr><th rowspan="2">Automata</th><th colspan="3">Stacks to add</th></tr><tr><th>Input</th><th>Output</th><th>Auxiliary stack</th></tr></thead><tbody><tr><td>NFA</td><td>SD</td><td></td><td></td></tr><tr><td>NPDA</td><td>SD</td><td></td><td>A</td></tr><tr><td>NFST</td><td></td><td>SI</td><td></td></tr><tr><td>2-way NFST</td><td>2 × A</td><td>SI</td><td></td></tr><tr><td>NTM</td><td>2 × A</td><td></td><td></td></tr><tr><td>n-tape NTM</td><td>2 × A</td><td></td><td>2(n − 1) × A</td></tr><tr><td>NTM with output</td><td>2 × A</td><td></td><td></td></tr></tbody></table>

§60.5 We have a very general characterisation of the different sorts of automata in the stellar resolution. However, in order to consider more complex extensions of automata such as alternating Turing machines, tree automata or other features, adding stacks is not sufficient any more: we need more sophisticated changes.

§60.6 **Seiller's graphings as another computational basis.** Seiller has similar ideas with his graphings which are able to represent automata by actions on state spaces [Sei18]. The idea seems so general that Seiller uses graphings to represent models of computation in a more mathematical and generic way. From this idea, he hopes to give a mathematical definition to the notion of *algorithm* which would correspond to a specification for graphings. However, the notion is still unclear and no works in that direction have been published yet, at the time of this thesis.

§60.7 **Are models of computation logical.** The encodings presented in this chapter are formatting of constellations. We are constraining constellations by giving some paths that execution must take. The shapes of terms also limit the potential of execution. To take an elementary example, what would we do to characterise constellations representing finite automata? Automata must contain the star [+i(W), +a(W, q₀)] (exactly once), the star [-a(ε), accept] (exactly once) then only stars of the shape [-a(c · W, q), +a(W, q')] representing transitions with some symbol c and states q, q'. We then require that the corresponding dependency graph is connected. Given a constellation Φ in the wild, how do we determine if it is an automata? Probably by using tests (cf. Chapter 6), as with correctness criteria for linear logic (although no tests for automata have been defined in this thesis). I believe that this makes all models of computation as “logical” as mathematical proofs. In particular, it is not so surprising that computer science and proof theory converged in the CHL correspondence Section 21 since they share similar practices of mixing the computational (object) and the logical (subject).

§60.8 **Regulation of computation.** I claim that models of computation are logical because their shape are characterised by some chosen tests. However, this is not even sufficient. A “human intervention” seems to be needed in a lot of models of computation. Circuits, for instance, usually compute from inputs to the output. However, constellations seem
to operate an asynchronous and parallel computation. There is no explicit direction of computation nor initial point (inputs). If we are not interested in implementations (for instance by using abstract execution), then there is no impact on the result. A solution that I implemented in this chapter is to use interactive execution by only selecting stars representing initial states on the right of ⊢ in interaction spaces. This is sufficient for automata but not for circuits. Imagine that we are starting from the conclusion instead of inputs in a circuit. When reaching the term associated with a function call, for instance $\neg \lor (X, Y, R)$, we need to non-deterministically test all choices of rays $+ \lor (...)$. However, if we start from the inputs, it is possible to fix some values and limit the possible choices (erasure of non-determinism). Actually, if we would like to perfectly reproduce the computation of circuits, we need synchronisation and a computation layer by layer. All this shows that strategies must be considered for real-world computation (as in λ-calculus in which a lot of strategies are studied). I now claim that:

Model of computation = Stellar resolution + Logic + Strategy
Computational object = Constellation + Correctness tests + Regulated computation

A lot of models of computation already assume a strategy which affects the complexity of their operations. A possible solution which I did not explored is to use internal polarities to simulate synchronisation of execution.

§60.9 **Anarchy and authority.** We have seen that an external control is needed so that we faithfully reproduce the behaviour of existing models of computation. However, this is not the case of all models. This corresponds to Girard's apodictic and epidictic described in Section 44.

* Apodictic models of computation are typically tile systems which are sometimes qualified as *natural computation*. Computation does not need any external control or human intervention by choosing where to start and how to proceed. Interestingly, the aTAM (cf. Section 59) features self-cooperation without the need of external control. We have an “intermediate-free” or “permissionless”<fnref n="1" /> computation<fnref n="2" />. Computation is autonomous in these models and freed from any query to external procedures, structures of systems.

* Epidictic models contain circuits or logic programs in which computation has to be done in a certain way. We have to “educate” computation. However, what is the nature of those strategies? Can strategies always be implemented by terms or constellations so that we internalise this seemingly external control (as for aTAM)? For instance, those strategies would be checked by tests and we would have that “strategies=logic”. It seems possible in some cases by finding alternative and more sophisticated encodings but I do not believe it is always possible. For automata

<footnote n="1">¹Similarly to decentralised blockchain technologies, whereas banking systems are centralised with intermediates. Both have their advantages and drawbacks.</footnote>

<footnote n="2">²Which can be considered a requirement for Girard's ideal of analytic space (cf. Section 42).</footnote>
with interactive execution for instance, the arbitrary choice of initial states (al-
though it may be simulated by using internal polarities).

I currently have no idea about how to implement strategies in a satisfying and generic
way but I believe this is a serious and interesting problem which is in consistent with the
idea that TS reveals implicit operations. Moreover, these considerations has an effect
on computational complexity.
# Chapter 9

## Properties of execution for objective constellations

In this section, we present few things which can be said about constellations, their structure and their behaviour. By convention, we $Ex$ is written, we can mean either $AEx$ or $IEx$.

We focus on objective constellations since they are the ones which are studied and used the most in this thesis.

### 61 Computability of stellar resolution

§61.1 In this section, a few results about execution are detailed. First, our model is Turing-complete, which is not too surprising since it is very close to logic programming which is itself known to be Turing-complete (especially by considering Horn clauses [Hor51, Tär77]) but also able to simulate the aTAM which is also Turing-complete [Win98, Section 3.2.5] [Woo15, Section 2].

§61.2 **Proposition (Turing-completeness).** Stellar resolution is Turing-complete.

*Proof.* Consequence of Theorem 56.25. Although we can encode Turing machines, stellar resolution (with abstract execution) is actually “stronger” but for wrong reasons: the ability to compute infinite normal forms. In particular, it is possible to construct infinite non-uniform families of boolean circuits (cf. Section 58) which are known to be theoretically able to decide any language but without concrete implementation of how such families work (for that reason, we usually require families to be *uniform*, i.e. that they can be generated by a Turing machine). This is not a problem since we are usually interested in finite constellations and finite normal forms. Moreover, stellar resolution with concrete execution is not affected by this problem. □

§61.3 It is possible to construct decider-constellations corresponding to a computable function $f: \mathbb{N}^k \to \mathbb{N}$ on natural numbers (or boolean deciders $f: \mathbb{N}^k \to \{0,1\}$). We already have an encoding of natural numbers in Definition 48.17. Let $\Phi$ be a constellation. We say
that $\Phi$ computes a function $f: \mathbf{N}^k \to \mathbf{N}$ when $\mathbf{Ex}(\Phi + [+i(\overline{n_1}, \dots, \overline{n_k})]) = [\overline{f(n_1, \dots, f_k)}]$. In case of a function $f$ returning a boolean (or a natural number of $\{0, 1\}$), we say that $\Phi$ accepts $[+i(\overline{n_1}, \dots, \overline{n_k})]$ in case $\mathbf{Ex}(\Phi + [+i(\overline{n_1}, \dots, \overline{n_k})]) = [1]$ and we say that it rejects when $\mathbf{Ex}(\Phi + [+i(\overline{n_1}, \dots, \overline{n_k})]) = [0]$ (as in automata theory). We say that $\Phi$ recognises the set of constellations:

$$ \mathcal{L}(\Phi) := \{[+i(\overline{n_1}, \dots, \overline{n_k})] \mid \Phi \text{ recognises } [+i(\overline{n_1}, \dots, \overline{n_k})]\}. $$

As explained in Paragraph 16.9, we can encode most interesting classical datatypes with natural numbers.

# 62 Classes of constellations

## (Non-)Terminating constellations

§62.1 The most remarkable behaviour of constellations is (non-)termination of execution. There exists actually two notions of termination which are distinguished by concrete execution.

§62.2 **Definition (Visible normalisation).** A constellation $\Phi$ is visibly normalising w.r.t. to a set of colours $C \subseteq F$ when $\mathbf{AEx}_C(\Phi)$ is finite, written $|\mathbf{AEx}_C(\Phi)| < \infty$ or sometimes $|\mathbf{CSatDiags}_C(\Phi)| < \infty$.

§62.3 **Definition (Strong normalisation).** A constellation $\Phi$ is strongly normalising$^a$ w.r.t. to a set of colours $C \subseteq F_+ \uplus F_-$ when $\mathbf{IEx}_C(\Phi)$ terminates.

§62.4 The difference is clear in the constellation $[-c(X), +c(f(X))]$. With abstract execution, we will have $\mathbf{AEx}([-c(X), +c(f(X))]) = \emptyset$ because it is impossible to construct a saturated diagram. All diagrams will be infinite chains linking $-c(X)$ with $+c(f(X))$. Any cyclic diagram would connect $-c(X)$ with $+c(f(X))$ where the two occurrences of $X$ refer to the same variable but such diagram are incorrect because $\{X \stackrel{?}{=} f(X)\}$ has not solution. The visible output is finite. However, with concrete execution, we would have an infinite loop always introducing new occurrences of the star. There is no way to terminate since it is impossible to tell when to stop. Strong normalisation subsumes visible normalisation.

§62.5 **Black holes.** The previous example can be generalised to what I call a *black hole*. The feature we are looking for with black holes is their ability to erase a given connected constellation (or connected component of a constellation) $\Phi$. If $\phi$ is a black hole then we want to obtain $\mathbf{Ex}(\Phi + \phi) = \emptyset$. However, there is no generic black hole: they necessarily depends on the shape of $\Phi$.

<footnote>$^a$The term comes from $\lambda$-calculus in which strongly normalisation is the termination of all possible paths of reduction.</footnote>
* With abstract execution, a typical black hole is to choose a star

$$[r, -w(X), +w(f(X))]$$

where $r \triangleright r'$ for $r'$ a ray of $\Phi$. All diagram of $\Phi$ connected to $[r, -w(X), +w(f(X))]$ will never be saturated because it is always possible to add an occurrence of $[r, -w(X), +w(f(X))]$ and extend the diagram as we wish.

* With concrete execution, the previous black hole yields an infinite loop but not really the erasure we expect. There are several solutions such as embedding execution with an operator such as $\frac{1}{2}$ as for the interpretation of automata (cf. Section 56). We will introduce specific solutions when needed (for the interpretation of weakening in linear logic).

§62.6 What distinguishes terminating constellations from other constellations? It looks like cycles in dependency graphs are related to loops in concrete execution. Cyclic constellations can be non-terminating but also terminating (the logic program for unary addition in Example 48.18). A first intuition comes from rewriting theory and the theory of functional languages [BN98, Chapter 5]. A rewriting system is terminating when all sequences of applications of rewriting rules are decreasing w.r.t. some (usually polynomial) measure of the initial term. In other words, termination occurs in converging cycles consuming terms of a star.

§62.7 I give a typical example inspired from the consumption of words with finite automata. We have a star $[+a(0 \cdot 0 \cdot 0 \cdot \varepsilon)]$ meant to be consumed by a loop $[-a(0 \cdot W), +a(W)]$. The loop, by itself, is not terminating because we can repeat it as many times as we want. It can be connected with itself to produce $[-a(0 \cdot 0 \cdot W), +a(W)]$, $[-a(0 \cdot 0 \cdot 0 \cdot W), +a(W)]$ and so on. It is has not way to know when to stop, as in black holes. However, it is productive: the negative ray can be cancelled by a star. In particular, $[-a(0 \cdot 0 \cdot 0 \cdot W), +a(W)]$ can terminate by interaction with $[+a(0 \cdot 0 \cdot 0 \cdot \varepsilon)]$ and produce $+a(\varepsilon)$. Remark that the constant $\varepsilon$ forbids any possible additional looping (as if we had linearised the term<fnref n="1" />). This idea of loop stopped by a ray is the same idea as in recursion/induction where a base case in needed.

## Graph-structural classification of constellations

§62.8 The shape of $\mathcal{D}[\Phi; C]$ for a constellation $\Phi$ contains a lot of information about $\mathrm{Ex}_C(\Phi)$. By observing the shape of constellations (as in Chapter 8 for instance), we observe that only cycles make iteration/loops possible and that the plurality of diagrams is caused by branching rays. Since the relationship between the structure of $\mathcal{D}[\Phi; C]$ and the computational behaviour of $\mathrm{Ex}_C(\Phi)$ is a bit complex, we suggest a few structural classes of constellations and establish theorems which will be useful to reason with constellations.

<footnote n="1">¹This is what is actually used for the interpretation of dereliction in linear logic.</footnote>
§62.9 **Definition (Properties of constellation).** Let $\Phi$ be a constellation,

$$ \mathcal{D}[\Phi; C] = (V, E, \text{end}) $$

be its dependency graph over a set of colours $C \subseteq F_+ \uplus F_-$. We say that $\Phi$ is:

* finite if $I_{\Phi}$ is finite (and so are $V$ and $E$) and it is infinite otherwise;

* exact if for all $e \in E$ we have $e = \{(i, j), (i', j')\}$ such that $\lfloor \Phi[i][j] \rfloor$ is $\alpha$-equivalent to $\lfloor \Phi[i'][j'] \rfloor$;

* acyclic when $\mathcal{D}[\Phi; C]$ is acyclic and otherwise it is cyclic;

* connected when $\mathcal{D}[\Phi; C]$ is connected and otherwise it is disconnected;

* branching if it has some branching rays. There are two sub-classes of branching constellations. We say that $\Phi$ is:

- non-deterministic if $|\text{CSatDiags}_C(\Phi)| > 1$;

- replicating if $|\text{CSatDiags}_C(\Phi)| = 1$.

* deterministic is there is no branching rays.

All the definitions can be naturally parametrised with a set of colours $C \subseteq F_+ \uplus F_-.

§62.10 **A few words on replication and non-determinism.** Replication is a duplication occurring in a same diagram. Non-determinism is also a duplication but splitting diagrams. The two are not so different because they come from the same operation of duplication. The only difference is that the two diagrams can be joined in the case of replication but not in the case of non-determinism. We could talk about *linkable* and *non-linkable* duplication instead. Replication is like having two choices but realising that one choice links to the other: it is then an *illusionary choice*<fnref n="2" />.

§62.11 **Example.** We illustrate the properties defined above.

* The constellation $\Phi_N^{n+m}$ of Example 48.18 is connected, cyclic and branching (non-deterministic). The middle star handles recursion but the construction of diagrams can either continue or exit the loop.

* $[+a(X), +a(X)] + [-a(X), -a(X), X]$ is exact, connected, cyclic and branching (non-deterministic).

* $[X, -c(X)] + [+c(f(Y))] + [+c(g(Y))]$ is acyclic, connected and branching (non-deterministic).

* $[+a(\mathbf{l}), +a(\mathbf{r})] + [+b(\mathbf{l}), +b(\mathbf{r})] + [-a(X), -b(X)]$ is connected, cyclic and branching (replicating but not non-deterministic). Two choices are possible for the

<footnote n="2">²I got this idea from a discussion with Valentin Maestracci.</footnote>
negative rays but all the stars can appear in the same diagram by duplicating
$[-a(X), -b(X)]$ and connecting the 1 (resp. r) together.

All these constellations are finite.

§62.12 **Proposition.** If a constellation $\Phi$ with $\mathfrak{D}[\Phi; C] := (V_{\mathfrak{D}}, E_{\mathfrak{D}}, \mathbf{end}_{\mathfrak{D}})$ is finite and acyclic w.r.t. $C \subseteq F_+ \uplus F_-$ then for all diagram $(G_\delta, \delta)$ such that $G_\delta := (V_\delta, E_\delta, \mathbf{end}_\delta)$ and $\delta : D_\delta \to \mathfrak{D}[\Phi; C]$, we have that $\delta$ is injective.

*Proof.* Assume that for $v, v' \in D_\delta$, $\delta(v) = \delta(v')$. We have to show $v = v'$, meaning that $v$ and $v'$ do not correspond to two occurrences of a same star in $\mathfrak{D}[\Phi; C]$. Assume by contradiction that $v \neq v'$. The only way to have $v \neq v'$ while preserving the adjacency relation (which is required by the definition of diagram, which is a multigraph homomorphism) is to have a path $\rho$ from $v$ to $v'$ such that $\delta(\rho)$ is a path from $\delta(v) = \delta(v')$ to itself. However, this contradicts the acyclicity of $\Phi$. $\square$

§62.13 **Corollary (Termination of acyclic constellations).** If a constellation $\Phi$ with
$$ \mathfrak{D}[\Phi; C] := (V_{\mathfrak{D}}, E_{\mathfrak{D}}, \mathbf{end}_{\mathfrak{D}}) $$
is finite and acyclic w.r.t. $C \subseteq F_+ \uplus F_-$ then $|\mathbf{CSatDiags}_C(\Phi)| < \infty$.

*Proof.* Assume $\Phi$ is finite and acyclic. By Proposition 62.12, vertices of diagrams are uniquely taken from $V_{\mathfrak{D}}$ and since stars have finitely many rays which must be uniquely connected, there are finitely many edges. There are only finitely many graphs we can construct with finitely many vertices and edges and in particular $\mathbf{CSatDiags}_C(\Phi)$ is finite. $\square$

§62.14 **Lemma (Exactness).** Let $\Phi$ be a constellation which is exact w.r.t. a set of colours $C \subseteq F_+ \uplus F_-$. We have $\mathbf{SatDiags}_C(\Phi) = \mathbf{CSatDiags}_C(\Phi)$.

*Proof.* Let $\Phi$ be an exact constellation and $(G_\delta, \delta) \in \mathbf{SatDiags}_C(\Phi)$ one of its diagrams. We already have $\mathbf{CSatDiags}_C(\Phi) \subseteq \mathbf{SatDiags}_C(\Phi)$ by definition. It remains to show that we have $\mathbf{SatDiags}_C(\Phi) \subseteq \mathbf{CSatDiags}_C(\Phi)$ by showing that $(G_\delta, \delta)$ is correct. Since $\Phi$ is correct, all the $n$ equations associated with edges of $\mathfrak{D}[\Phi; C]$ are equations $t_i \stackrel{?}{=} u_i$ for $1 \le i \le n$ such that $t_i$ is $\alpha$-equivalent to $u_i$, meaning that any solution of $\{t_i \stackrel{?}{=} u_i\}$ must a renaming $\alpha$. We have to show that $\{t_1 \stackrel{?}{=} u_1, \dots, t_n \stackrel{?}{=} u_n\}$ has a solution. If we solve all equations independently, we obtain subproblems with only variables. The only rule which applies is “replace rule” (cf. Theorem B.2.4). We finally show that this rule never fails when we only have variables. Assume we have a unification problem $P$ with only variables. If we replace $X$ by $Y$, either $X \notin P$ and nothing happens or $X \in P$ and all occurrences of $X$ are replaced by $Y$. We obtain either equations $Y \stackrel{?}{=} Y$ which can
be removed by the “clear rule” or equations $X \stackrel{?}{=} Z$ with $X \neq Z$ and in this case there is no problem. $\square$

**§62.15 Definition.** Let $\Phi$ be a constellation. It is called *perfect* when it is finite, connected, exact, acyclic and deterministic.

**§62.16 Lemma (Perfection).** If a constellation $\Phi$ is perfect then it has a unique saturated diagram which is correct.

*Proof.* By Corollary 62.13, we know that $\Phi$ has finitely many saturated correct diagrams. By induction on the number $n$ of edges in $\mathcal{D}[\Phi]$.

◇ **Base case** If $n=0$ then $\Phi$ must be made of a unique star $\Phi[i]$, otherwise it would not be connected. We have a unique diagram $(G_\delta, \delta)$ with $G_\delta := (V, E, \text{end})$, $V := \{v\}$, $E := \emptyset$ and $\delta(v) = i$. This diagram is correct and we have $\downarrow(G_\delta, \delta) = \Phi[i]$;

◇ **Induction** Assume we have a perfect constellation $\Phi'$ with dependency graph $\mathcal{D}[\Phi'] := (V', E', \text{end}')$ with $|E'| = n'$ a unique diagram $(G'_{\delta}, \delta')$. We now consider a bigger constellation $\Phi$ with $\mathcal{D}[\Phi] := (V, E, \text{end})$ and $|E| = |E'| + 1$. We necessarily added a new star $\Phi[j]$, hence $\Phi := \Phi' + \Phi[j]$. Since $\Phi'$ is connected, $j$ is connected to the unique connected component of $\mathcal{D}[\Phi']$. Since $\Phi$ is deterministic then $\Phi[j]$ has been linked to a free polarised ray of $\Phi'$. The unique diagram $(G_\delta, \delta)$ of $\Phi'$ (given by induction hypothesis) can be extended with $\Phi[j]$ and by fusion we still obtain a unique bigger saturated diagram $(G_\delta, \delta)$. Since $\Phi'$ and $\Phi$ are both exact, it guarantees the correctness of $(G_\delta, \delta)$.

**§62.17 Lemma (Independence of connected components).** Let $\Phi$ be a constellation and $\mathcal{D}[\Phi; C]$ be its dependency graph for a set of colours $C \subseteq F_+ \uplus F_-$. We define $K$ as the set of connected components of $\mathcal{D}[\Phi; C]$ and for all $k \in K$, we define $\Phi_k$ as the restriction of $\Phi$ to the stars in $K$. We have $A\mathrm{Ex}_C(\Phi) = \bigsqcup_{k \in K} A\mathrm{Ex}_C(\Phi_k)$.

*Proof.* Consider a diagram $(G_\delta, \delta)$ such that $G_\delta := (V_\delta, E_\delta, \text{end}_\delta)$ and $\delta : D_\delta \to \mathcal{D}[\Phi; C]$. In the proof of Proposition 62.12, we have seen that diagrams preserve reachability of vertices because they preserve the adjacency relation of multigraphs. It follows that for all $v, v' \in V_\delta$, if there is no path from $\delta(v)$ to $\delta(v')$, then there cannot be a path from $v$ to $v'$. Since diagrams are connected, they must have a connected component of $\mathcal{D}[\Phi; C]$ as image. Therefore, $\mathrm{CSatDiags}_C(\Phi) = \bigcup_{k \in K} \mathrm{CSatDiags}_C(\Phi_k)$. Since execution is the actualisation of all correct saturated diagrams, it follows that $A\mathrm{Ex}_C(\Phi) = \bigsqcup_{k \in K} A\mathrm{Ex}_C(\Phi_k)$. $\square$

**§62.18 Corollary (Independence of isolated stars).** Let $\Phi$ be a constellation and $\mathcal{D}[\Phi; C]$ be its dependency graph for a set of colours $C \subseteq F_+ \uplus F_-$. For each star index $i \in I_\Phi$ such that $i$ is isolated (no adjacent vertex) in $\mathcal{D}[\Phi; C]$, there is $i' \in I_{A\mathrm{Ex}_C(\Phi)}$ such that
$AEx_C(\Phi)[i'] = \Phi[i']$.

*Proof.* By Lemma 62.17, in the particular case where we have a connected component $\Phi_l$ (with $l \in K$) made of a unique isolated star $\Phi[i]$, if $\Phi = \Phi' + \Phi[i]$ then we would have $AEx_C(\Phi' + \Phi[i]) = (\bigcup_{k \in K - \{l\}} AEx_C(\Phi_k)) + AEx_C(\Phi_l) = (\bigcup_{k \in K - \{l\}} AEx_C(\Phi_k)) + AEx_C(\Phi[i]) = (\bigcup_{k \in K - \{l\}} AEx_C(\Phi_k)) + \Phi[i]$ because the execution of a star is a star (no diagram can be constructed). In particular, if $i'$ is the index of $\Phi[i]$ in the normal form, we have $AEx_C(\Phi)[i'] = \Phi[i']$. $\square$

# 63 Stellar transformations

§63.1 From the definition of concrete execution (cf. Section 50), we can remark that it is possible to reduce all deterministic links without any impact on the normal form. This corresponds to a sort of pre-normalisation of constellations. It is then possible to only consider constellations without such links. We would only lose convenience or clarity because constellations would be more compact.

§63.2 **Definition** (Stellar compression and compact constellations). Let $\Phi$ be a constellation and $C \subseteq F_+ \uplus F_-$ be a set of colours. Its compression $compress(\Phi)$ is the constellation obtained by the following procedure:

* identify deterministic rays $\Phi[i][j]$ in $\mathfrak{D}[\Phi; C]$ such that $\mathrm{adj}_{\Phi}^C(i, j) = \{(i', j')\}$ and $\Phi[i][j]$ is also deterministic;

* for each such ray $r$, we transform $\Phi := \Phi' + \Phi[i]$ into $\Phi' + \Phi[i] \nabla^{j'j'} \Phi[i']$.

We say that a constellation $\Phi$ is *compact* when $compress(\Phi) = \Phi$.

§63.3 **Example.** For the constellation

$$ \Phi := [-1(X), +4(X)] + [-2(X)] + [-4(X), -3(X), +5(X)] + [-5(X), 5(X)], $$

we have $compress(\Phi) = [-1(X), -3(X), 5(X)] + [-2(X)]$.

§63.4 There are other operations which we could think of but that we will not be interested in here. For instance, we could think about splitting non-deterministic constellations into several deterministic ones (we make choices explicit with several slices of a same constellation). We could also think about unfolding loops. For instance, for the logic program $\Phi_N^{2+2}$, we could explicitly create a chain of stars unfolding the query so that the constellation is no longer cyclic. This is similar to how we would unfold loops in imperative programming.
$$ \Phi = [X, +c(X)] + [-c(\mathbf{1} \cdot X)] \qquad [-c(\mathbf{r} \cdot X)] = \Phi' $$

(a) We have $\mathrm{Ex}_{\{c\}}(\Phi) = [\mathbf{1} \cdot X]$ and $\mathrm{Ex}_{\{c\}}(\mathrm{Ex}_{\{c\}}(\Phi) \uplus \Phi') = [-c(\mathbf{r} \cdot X)] + [\mathbf{1} \cdot X]$, but $\mathrm{Ex}_{\{c\}}(\Phi \uplus \Phi') = [\mathbf{1} \cdot X] + [\mathbf{r} \cdot X]$ which is different. Notice that both $[-c(\mathbf{1} \cdot X)]$ and $[-c(\mathbf{r} \cdot X)]$ need $[X, +c(X)]$ but when executing $\Phi$, $\Phi'$ cannot be connected to it anymore.

$$ \Phi = [X, +c(X)] + [-c(X), a] \qquad [-c(X), b] = \Phi' $$

(b) We have $\mathrm{Ex}_{\{c\}}(\Phi) = [X, a]$ and $\mathrm{Ex}_{\{c\}}(\mathrm{Ex}_{\{c\}}(\Phi) \uplus \Phi') = [-c(X), b] + [X, a]$, but $\mathrm{Ex}_{\{c\}}(\Phi \uplus \Phi') = [X, a] + [X, b]$ which is different.

$$ \Phi = [-f(+g(X))] + [X, +f(X)] \qquad [-g(X), +f(X), a] = \Phi' $$

(c) We have $\mathrm{Ex}_{\{f\}}(\Phi) = [+g(X)]$ and $\mathrm{Ex}_{\{g\}}(\mathrm{Ex}_{\{f\}}(\Phi) \uplus \Phi') = [+f(X), a]$, but $\mathrm{Ex}_{\{f,g\}}(\Phi \uplus \Phi') = []$ (no saturated diagrams) which is different.

<caption>Figure 64.1: Counter-examples for partial pre-execution.</caption>

## 64 Partial pre-execution and confluence

§64.1 An important result is the possibility of partial execution by only reducing rays of some colours on some constellations first then the others without any effect on the normal form, i.e. that $\mathrm{Ex}_{C \cup D}(\mathrm{Ex}_D(\Phi) \uplus \Phi') = \mathrm{Ex}_{C \cup D}(\Phi \uplus \Phi')$ for some set of colours C and D. However, this is not valid in general as presented in Figure 64.1. The problem is that stars from two distinct constellations want to access a same ray and an execution of a constellation may erase some potential connexions which were present and required by another constellation. This problem is reminiscent of the idea of *mutual exclusion* in concurrent programming [Dij01]. Also notice that in Figure 64.1c, internal colours add even more complexity: some rays may indirectly access internal colours. Direct access occurs once the internal colour has been “unlocked” by a star extracting it. I choose to omit the case of subjective constellations in this thesis.

§64.2 This property of partial pre-execution is necessary in order to obtain a result of confluence and associativity of execution which are necessary for the definition of linear logic as explained at the end of this chapter. We need to design a precondition for which these properties are valid and from which it is possible to express linear logic.

§64.3 There are several possible choices depending on how demanding we want to be. A simple choice is to reason on the accessibility of rays in a dependency graph. We do not want a ray to be accessible from two different constellations such that one is pre-executed before
<figure><img src="image_108.png" /><figcaption>Figure 64.2: Example of interaction map for the constellation $\Phi \uplus \Phi'$ of Figure 64.1c where the internal ray is replaced by a variable $X$.</figcaption></figure>

the other. For instance, in Figure 64.1, the ray $[+c(X)]$ is accessible both from $\Phi$ and $\Phi'$.

**§64.4 Definition (Interaction map).** Let $C \subseteq F_+ \uplus F_-$ be a set of colours. The interaction map $\text{IM}_C(\Phi)$ of a constellation $\Phi$ over $C$ is a graph $(V, E)$ defined with:

• $V := \{(i, j) \in \pm\text{IdRays}(\Phi) \mid \text{colours}(\Phi[i][j]) \subseteq C\}$;

• $\{(i, j), (i', j')\} \in E$ when:
  - $\Phi[i][j]$ and $\Phi[i][j']$ are linked in $\mathfrak{D}[\Phi; C]$;
  - or $i = i'$ (in order to travel from one star to another).

**§64.5** An example of interaction map is given in Figure 64.2.

**§64.6 Observation (Idea for the case of subjective rays).** In order to consider subjective rays, an idea I had was to consider matchability between subrays in the interaction map in order to anticipate the possibility of connexion with internal colours.

**§64.7 Definition (Shared rays).** We define the set of rays shared the constellations

$$ \Phi_1, \dots, \Phi_n $$

w.r.t. a set of colours $C \subseteq F_+ \uplus F_-$ as the set:

$$ \mathfrak{m}_C(\Phi_1, \dots, \Phi_n) := \{ (\sum_{i=1}^n \Phi_i)[i][j] \mid $$

$$(\sum_{i=1}^n \Phi_i)[i][j] \text{ is reachable from some } \Phi_i[k][l] \text{ for all } 1 \le i \le n \text{ in } \text{IM}_C(\Phi)$$

with a non-empty path\}.

We omit the set of colour when we consider all colours.
<figure><img src="image_109.png" /><figcaption>Figure 64.3: Partial execution acts as a partial diagram contraction, which is only possible when $\Phi$ and $\Phi'$ do not act on the same variable. The “blow-up” obtained by inverting execution preserves the connexions between rays.</figcaption></figure>

§64.8 **Example.** In Figure 64.1, we have $\mathfrak{m}(\Phi, \Phi') = \{+c(X)\}$ in the two first examples and $\mathfrak{m}(\Phi, \Phi') = \{-f(X)\}$ in the third one.

§64.9 **Lemma (Partial pre-execution).** Let $\Phi$ and $\Phi'$ be constellations and $C, D \subseteq F_+ \uplus F_-$ be sets of colours such that $\mathfrak{m}_{C \cup D}(\Phi, \Phi') = \emptyset$. We have $\mathrm{Ex}_{C \cup D}(\mathrm{Ex}_D(\Phi) \uplus \Phi') = \mathrm{Ex}_{C \cup D}(\Phi \uplus \Phi')$.

*Proof.* We show the existence of an isomorphism $\varphi$ between $\mathrm{CSatDiags}_{C \cup D}(\mathrm{Ex}_D(\Phi) \uplus \Phi')$ and $\mathrm{CSatDiags}_{C \cup D}(\Phi \uplus \Phi')$. Assume we have a diagram

$$ (G^{PE}, \delta^{PE}) \in \mathrm{CSatDiags}_{C \cup D}(\mathrm{Ex}_D(\Phi) \uplus \Phi') $$

with $G^{PE} := (V^{PE}, E^{PE}, \mathrm{end}^{PE})$, where $PE$ stands for “partial execution” because a subconstellation is executed first. The goal is to associate $(G^{PE}, \delta^{PE})$ with a diagram $\varphi(G^{PE}, \delta^{PE}) \in \mathrm{CSatDiags}_{C \cup D}(\Phi \uplus \Phi')$ and to show that $\varphi$ is an isomorphism.

The idea, illustrated in Figure 64.3, is that $(G^{PE}, \delta^{PE})$ (on the left) can be decomposed into two parts:

* vertices $v \in V^{PE}$ such that $\delta^{C \cup D}(v) = k$, representing stars $\mathrm{Ex}_D(\Phi)[k]$ (in blue);

* vertices $v \in V^{PE}$ such that $\delta^{C \cup D}(v) = j$, representing stars $\Phi'[j]$ with:

- edges $E_{\Phi'} \subseteq E^{PE}$ linking stars of $\Phi'$ together (in red);

- edges $E_{\Phi, \Phi'} \subseteq E^{PE}$ linking stars of $\Phi'$ with stars $\mathrm{Ex}_D(\Phi)[k]$ (in red);

The stars $\mathrm{Ex}_D(\Phi)[k]$ come from diagrams $(G_k^D, \delta_k^D) \in \mathrm{CSatDiags}_D(\Phi)$, i.e. there are diagrams $(G_k^D, \delta_k^D) \in \mathrm{CSatDiags}_D(\Phi)$ such that $\downarrow(G_k^D, \delta_k^D) = \mathrm{Ex}_D(\Phi)[k]$, because these stars are part of the execution of $\Phi$, by definition of the abstract execution $\mathrm{Ex}_D := \mathcal{A}\mathrm{Ex}_D$. We can perform a “star expansion” (right diagram in Figure 64.3) on $\mathrm{Ex}_D(\Phi)[k]$ by replacing it with its corresponding diagram $(G_k^D, \delta_k^D)$. In some sense, we are reversing execution. The isomorphism $\varphi$ associates $(G^{PE}, \delta^{PE})$ with a new diagram $\varphi(G^{PE}, \delta^{PE})$
corresponding to $(G^{PE}, \delta^{PE})$ where this operation of star expansion has been applied on stars $\mathbf{Ex}_D(\Phi)[k]$ for all $k$. This operation works as follows:

1. we start from our diagram $(G^{PE}, \delta^{PE})$ and apply the same procedure on all stars $\mathbf{Ex}_D(\Phi)[k] = [r_1, ..., r_n]$ (blue circles on the left);

2. by definition of abstract execution, the star $\mathbf{Ex}_D(\Phi)[k]$ must come from some actualised diagram $\downarrow(G_k^D, \delta_k^D)$ such that each ray $r_i$ corresponds to a ray $\delta(v)[i_k]$;

3. we can construct a new diagram $\varphi(G^{PE}, \delta^{PE})$ (on the right) by taking $(G^{PE}, \delta^{PE})$, removing the vertex $u$ such that $\delta(u) = \mathbf{Ex}_D(\Phi)[k]$ and adding the subgraph $G_k^D$. We then extend $\delta^{PE}$ with $\delta_k^D$.

4. The links between rays $r_i$ and rays of $\Phi'$ with colour in $C$ (on the left) are then replaced by links between rays $r_i$ and rays $\delta(v)[i_k]$ (on the right).

5. By our hypothesis $\mathfrak{A}_{C \cup D}(\Phi, \Phi') = \emptyset$, the stars of $\Phi$ and of $\Phi'$ cannot interfere by acting on a same ray of a same star. It follows that the actualisation of diagrams $(G_k^D, \delta_k^D)$ preserve the links between rays $r_i$ and rays $\delta(v)[i_k]$. In other words, the execution of blue diagrams are independent from the rest of the diagram $\varphi(G^{PE}, \delta^{PE})$. Without this precondition, some connexions could disappear (as in Figure 64.1) and we would not preserve all connexions allowing this inversion of execution.

We obtain diagrams $\varphi(G_{\delta_k^D}, \delta_k^D)$ corresponding to diagrams $(G_{\delta_k^D}, \delta_k^D)$ extended with stars of $\Phi'$ in exactly the same way as how $\phi_k^D$ can be connected with $\Phi'$. We have $\varphi(\delta_k^D) \in \mathbf{CSatDiags}_{C \cup D}(\Phi \uplus \Phi')$ since it connects stars of both $\Phi$ and $\Phi'$.

It remains to show that $\varphi$ is invertible so that we have an isomorphism between

$$ \mathbf{CSatDiags}_{C \cup D}(\mathbf{Ex}_D(\Phi) \uplus \Phi') $$

and

$$ \mathbf{CSatDiags}_{C \cup D}(\Phi \uplus \Phi'). $$

Assume we have

$$ (G_{\delta'}, \delta') \in \mathbf{CSatDiags}_{C \cup D}(\Phi \uplus \Phi'). $$

We would like to define $\varphi^{-1}(G_{\delta'}, \delta')$. By the confluence of diagram reduction (cf. Corollary 49.36), we can apply fusion first on the stars coming from $\Phi$ using colours in $D$ and then on the colours in $C$. By doing so, we obtain a diagram $\varphi^{-1}(G_{\delta'}, \delta') \in \mathbf{CSatDiags}_{C \cup D}(\mathbf{Ex}_D(\Phi) \uplus \Phi')$. We have $\varphi(\varphi^{-1}(\delta)) = \delta$ and $\varphi^{-1}(\varphi(\delta)) = \delta$ because of the relationship between stars $\mathbf{Ex}_D(\Phi)[k]$ and the diagrams $(G_{\delta_k^D}, \delta_k^D)$ they come from. Actualising then expanding or the converse is equivalent to the identity homomorphism $\varphi_i d(G, \delta) = (G, \delta)$, by design. $\square$
§64.10 **Theorem (Confluence).** For any constellation $\Phi$, and $C, D \subseteq F_+ \uplus F_-$ two disjoint sets of colours, we have $\mathrm{Ex}_D(\mathrm{Ex}_C(\Phi)) = \mathrm{Ex}_{C \cup D}(\Phi) = \mathrm{Ex}_C(\mathrm{Ex}_D(\Phi))$.

*Proof.* By Lemma 64.9 with $\Phi' := \emptyset$ (in this case we trivially have $\cap_{C \cup D}(\Phi, \emptyset) = \emptyset$ which is the required precondition) we have $\mathrm{Ex}_{C \cup D}(\mathrm{Ex}_D(\Phi)) = \mathrm{Ex}_{C \cup D}(\Phi)$. Since $\mathrm{Ex}_D(\Phi)$ already applies fusion on all pairs of rays of colour in $D$ and there is nothing left of colour $D$ in $\mathrm{Ex}_{C \cup D}$, we have $\mathrm{Ex}_{C \cup D}(\mathrm{Ex}_D(\Phi)) = \mathrm{Ex}_C(\mathrm{Ex}_D(\Phi))$, hence $\mathrm{Ex}_C(\mathrm{Ex}_D(\Phi)) = \mathrm{Ex}_{C \cup D}(\Phi)$. Since $C \cup D = D \cup C$, we also have $\mathrm{Ex}_{C \cup D}(\Phi) = \mathrm{Ex}_{D \cup C}(\Phi)$. By using again Lemma 64.9, we finally obtain $\mathrm{Ex}_{D \cup C}(\Phi) = \mathrm{Ex}_D(\mathrm{Ex}_C(\Phi))$. $\square$

## 65 Discussion: the sufficient conditions for logical emergence

§65.1 Properties which are necessary to define (linear) logic as we know it do not naturally appear in stellar resolution which is very chaotic. It is then necessary to consider only constellations in some specific cases. Again, this characterisation of “logical constellations” may be characterised by tests (represented by constellations), consistently with the philosophy of transcendental syntax, as we will see later.

§65.2 The first necessary condition for (linear) logic is the idea of mutual exclusion previously defined. This condition led to confluence results. Why are they *necessary*? We will later see that confluence leads to associativity of execution, itself leading to a logical property called *adjunction*.

§65.3 **Adjunction.** Although already mentioned in Girard's writing [Gir11a, Section 14.2.1] and made explicit by Seiller [Sei12a, Section 2], the *adjunction property* is a necessary condition for the reconstruction of linear logic. The adjunction property is related to adjunctions in category theory. This property defines *linear implication*. In Seiller's work it is used as a way to prove that linear implication $\mathbf{A} \dashv \mathbf{B} := \mathbf{A} \perp \mathfrak{B} \mathbf{B}$ defined by realisability interpretation has a functional behaviour, i.e. in the case of stellar resolution, that:

$$ \mathbf{A} \dashv \mathbf{B} = \{ \Phi \mid \Psi \in \mathbf{A}, \mathrm{Ex}(\Phi \uplus \Psi) \in \mathbf{B} \}. $$

§65.4 **Trefoil property.** Seiller shows that the adjunction could be generalised by a property called *trefoil property* [Sei16a, Section 2.2]. This property is more general but sufficient for the definition of linear logic. For that reason, it will be used in the interpretation of linear logic in this thesis. This trefoil property is often the consequence of associativity of binary execution which comes itself from confluence. Both only hold under some conditions as explained above.

§65.5 The understanding of these necessary conditions is part of transcendental syntax and has yet to be explored. In particular, in his paper “La syntaxe Transcendantale, manifeste” [Gir11c, Section 2.4.3], Girard explicitly mentions that epidotic architectures must be closed by adjunction (cf. Paragraph 44.17).
# Chapter 10

## Stellar interpretation of multiplicative linear logic

In this chapter, we interpret linear logic with stellar resolution to provide a technical illustration of transcendental syntax. We start with multiplicative linear logic (MLL).

### 66 Proofs as constellations

**§66.1** The representation of MLL proofs is not very surprising: it directly follows the GoI interpretation of proofs as finite permutations but with terms instead. Actually, it is simply a variant of the interpretation with flows. However, a difference with flows is that we have a little trick with the representation of cuts and that we are able to express Danos-Regnier correctness.

**§66.2** **Convention (Basis of representation).** In order to encode proof-structures, we fix a *basis of representation* which is a polarised signature $\mathcal{B} := (V, F, \mathbf{ar}, \subset, [\cdot,])$ with any set of variables such that $X \in V$, function symbols $F := F_0 \oplus F_+ \oplus F_-$ with $F := \{\mathbf{1}, \mathbf{r}, \cdot\} \cup \bigcup_{u \in U} \{u\}$, $F_+ := \bigcup_{u \in U} \{+u\}$ and $F_- := \bigcup_{u \in U} \{-u\}$ for $U$ a set of elements which be used to represent vertices of proof-structures (we can set $U := \mathbf{N}$). We have $\mathbf{ar}(u) = 1$ for all $u \in U$, $\mathbf{ar}(\cdot) = 2$ and $\mathbf{ar}(\mathbf{1}) = \mathbf{ar}(\mathbf{r}) = 0$. The symbol $\cdot$ is considered right-associative, i.e. $t \cdot u \cdot v := t \cdot (u \cdot v)$.

**§66.3** Similarly to unlabelled proof-structures, constellations are purely “locative”: only “physical locations” appearing in a proof-structure $\mathcal{S}$ are translated, without giving any serious meaning to labels. We would like to associate a unique address in $\text{Term}(\mathbb{B})$ with atoms $v \in \text{Atoms}(\mathcal{S})$ of a proof-structure $\mathcal{S}$. The address of $v$ will be a term $v'(t)$ where $t$ is a path encoded as a sequence of $\mathbf{1}$ (left) and $\mathbf{r}$ (right) symbols representing the direction to follow in $\mathcal{S}$ to get from the conclusion $v' \in \text{Concl}(\mathcal{S})$ to the atom $v$. In other words, we are hard-coding the structure of proof-structures directly in axioms.

**§66.4** For convenience, we suggest an inductive definition of proof-structures based on their underlying hypergraph. It is from this inductive representation that address of atoms in a proof-structure will be defined.
<figure><img src="image_110.png" /><figcaption>Figure 66.1: Addressing of the atoms 1 and 3 in a proof-structure relatively to the conclusion they come from. Since the first instruction to reach 1 from 0 is to go right, the outermost symbol of the address of 0 should be **r**.</figcaption></figure>

§66.5 **Remark** (Inductive definition of proof-structures). A proof-structure with only one hyperedge is necessarily an axiom with two conclusions, written $Ax_{u,v}$. Then a proof-structure $S$ with $n$ hyperedges is either built from the union of two proof-structures, with respectively $k$ and $n-k$ hyperedges (written $S_1 \uplus S_2$), or from a proof-structure with $n-1$ hyperedges extended by either a $\otimes$, $\mathcal{Y}$, or cut hyperedge on two of its conclusions $u$ (left) and $v$ (right). Those latter proof-structures are written $\text{Tens}^{u,v}(S')$, $\text{Par}^{u,v}(S')$ and $\text{Cut}^{u,v}(S')$.

§66.6 **Definition** (Vertex above another one). A vertex $v$ is *above* another vertex $u$, written in a proof-structure if there exists a directed path from $v$ to $u$ going through only $\otimes$ and $\mathcal{Y}$ hyperedges.

§66.7 **Definition** (Address of an atom). We define the *path address* $\text{pAddr}_S(v)$ of an atom $v$ in a proof-structure $S$ inductively (cf. Remark 66.5):

• if $S \in \{Ax_{v,*}, Ax_{*,v}\}$ then $\text{pAddr}_S(v) = X$;

• if $S = S_1 \uplus S_2$ and $v \in V^{S_i}$ then $\text{pAddr}_S(v) = \text{pAddr}_{S_i}(v)$;

• if $S \in \{\text{Par}^{v',*}(S'), \text{Tens}^{v',*}(S')\}$ then $\text{pAddr}_S(v) = \mathbf{1} \cdot \text{pAddr}_{S'}(v)$ with $v$ being a conclusion such that $v$ is above $v'$;

• if $S \in \{\text{Par}^{*,v'}(S'), \text{Tens}^{*,v'}(S')\}$ then $\text{pAddr}_S(v) = \mathbf{r} \cdot \text{pAddr}_{S'}(v)$ with $v$ being a conclusion such that $v$ is above $v'$;

• $\text{pAddr}_S(v) = \text{pAddr}_{S'}(v)$ otherwise.

The path address to $v$ is uniquely defined w.r.t. to a conclusion $c \in \text{Concl}(S')$ where $S'$ is $S$ without cuts, i.e. $E^{S'} = E^S \setminus \text{Cuts}(S)$ and the rest of $S$ is defined as in $S'$.

The *address* of $v$ is then defined as the term $\text{addr}_S(v) := c(\text{pAddr}_S(v))$.
§66.8 **Example.** Figure 66.1 illustrates the idea of addressing of atoms. The address of the atom 1 in Figure 66.2 is $7(1 \cdot X)$ because it is reachable from the conclusion 7 by going to the left premise and the address of the atom 3 is $3(X)$ because it is directly reachable.

§66.9 **Proposition.** Let $\mathcal{S}$ be a proof-structure. For all $v, v' \in \text{Atoms}(\mathcal{S})$ such that $v \neq v'$, we have that $\text{addr}_{\mathcal{S}}(v) \neq \text{addr}_{\mathcal{S}}(v')$, meaning that all atoms have pairwise distinct addresses.

*Proof.* By definition, all vertices of $\mathcal{S}$ are distinct, and in particular all conclusions are. Assume $v$ is reachable from a conclusion $c \in \text{Concl}(\mathcal{S})$ but not from another conclusion $c' \in \text{Concl}(\mathcal{S})$ such that $c \neq c'$ whereas $v'$ is reachable from $c'$ but not $c$. The address of $v$ is of shape $c(...)$ whereas the address of $v'$ is of shape $c'(...)$, making the two addresses different. Now assume they both are reachable from the set conclusion $c$. We have that $\text{addr}_{\mathcal{S}}(v)$ is of shape $c(t)$ and $\text{addr}_{\mathcal{S}}(v')$ of shape $c(t')$ for some $t$ and $t'$. The terms $t$ and $t'$ are made of sequences of symbols $\mathbf{l}$ and $\mathbf{r}$ depending on if the atom is reachable by going on the left or the right of a $\mathcal{N}$ or $\otimes$ hyperedge (which have two inputs). If the two atoms $v$ and $v'$ are reached with exactly the same path then they must be identical atoms, which contradicts the hypothesis $v \neq v'$. Hence, they must have a different path and $t \neq t'$. It follows that $c(t) \neq c(t')$ and $\text{addr}_{\mathcal{S}}(v) \neq \text{addr}_{\mathcal{S}}(v')$. $\square$

§66.10 **Definition** (Set of addresses). We define the set of addresses as a set $\text{Addr}_x(\mathcal{S})$ containing terms $\text{addr}_\mathcal{S}(v)$ for any $v$, i.e. it is the countable set of all terms of the form $c(f_1 \cdots f_n \cdot X)$ where $c \in \text{Concl}(\mathcal{S})$ and $f_i \in \{\mathbf{l}, \mathbf{r}\}$.

§66.11 **Definition** (Translation of the computational content of a proof). The *vehicle* and the *cuts* of a proof-structure $\mathcal{S}$ are respectively defined by the following constellations:

$$ \Phi_S^{\text{ax}} := \sum_{e \in \text{Ax}(\mathcal{S})} [\mu(\text{addr}_S(\leftarrow e)), \mu(\text{addr}_S(\rightarrow e))], \quad \Phi_S^{\text{cut}} := \sum_{e \in \text{Cuts}(\mathcal{S})} [-\leftarrow e(X), -\rightarrow e(X)]. $$

such that $\mu(c(t)) = +c(t)$ when $c = \leftarrow e$ or $c = \rightarrow e$ for some $e \in \text{Cuts}(\mathcal{S})$ (it is related to a cut) and $\mu(x) = x$ otherwise. We define the *computational content* of $\mathcal{S}$ as the constellation $\Phi_S^{\text{comp}} := \Phi_S^{\text{ax}} \uplus \Phi_S^{\text{cut}}$.

§66.12 **Example.** An example of proof-structure translated into a constellation is given in Figure 66.2. Notice that the cut star can interact with the atoms of root 7 and 8. The trick mentioned in the introduction is that we have only one cut star, exactly as in proof-structures but it will duplicate during execution to connect to sub-formulas.
<figure><img src="image_111.png" /><figcaption>Figure 66.2: The above proof-structure is interpreted by the constellation [+7(1·X), +7(r·X)] + [3(X), +8(1·X)] + [+8(r·X), 6(X)] + [-7(X), -8(X)].</figcaption></figure>

# 67 Simulation of cut-elimination

§67.1 Cut-elimination in stellar resolution makes the vehicle interact with cuts by execution. Remark that the shape of proof-structures is directly embedded in the addresses of atoms of the vehicle. The consequence is that cut-elimination is nothing more than a process of contraction / transfer of information by resolution of addresses / conflicts. In particular, it shows that the ax/cut case of cut-elimination is the only “true” case of cut-elimination. The multiplicative case ⊗/⊲ purely depends on the shape of objects we are evaluating, and is therefore of a logical nature (in the sense of transcendental syntax).

§67.2 The idea is simply to execute the translation of the vehicle and cuts of a proof-structure. However, execution does not perfectly match the steps of cut-elimination. We start by looking at examples of execution of such constellations representing proof-structures. We expect diagrams to correspond to maximal paths from two ends of a proof-structure alternating between vehicle and cuts.

§67.3 **Example (Correct cut-elimination).** We have the following reduction $S \rightsquigarrow^* S'$ of proof-structure:

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

As shown in Figure 66.2, the proof-structure $S$ is translated into $\Phi_S^{\text{comp}} = [+7(1 \cdot X), +7(r \cdot X)] + [3(X), +8(1 \cdot X)] + [+8(r \cdot X), 6(X)] + [-7(X), -8(X)]$.
The ray $-7(X)$ can match either $+7(1 \cdot X)$ or $+7(r \cdot X)$ and it is the same for $8(X)$. In order to satisfy these requirements of $\alpha$-unification, the cut star must be duplicated and each occurrence of cut must connect rays with the same address, i.e. the path addresses $1 \cdot X$ together and not $1 \cdot X$ with $r \cdot X$. We obtain the following diagram:

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

By case analysis, it is easy to check that it is the only possible diagram. Since the $\alpha$-unification is trivial, it is simply a graph contraction doing no more than renamings and we get $\mathbf{AEx}(\Phi_S^{\text{comp}}) = [3(X), 6(X)] = \mathbf{AEx}(\Phi_{S'}^{\text{comp}})$.

If we were considering this proof-structure obtained after one step of multiplicative cut-elimination:

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

then the translation of axioms would be

$$[+1(X), +2(X)] + [3(X), +4(X)] + [+5(X), 6(X)].$$

Remark that a re-addressing of atoms occurs that the execution of constellations do not consider. Hence, execution do not faithfully and exactly simulate cut-elimination steps but it simulates full cut-elimination properly.

§67.4 In the previous example, although two occurrences of cuts appear in diagrams, exactly like how cuts are duplicated when eliminating $\otimes/\mathcal{Y}$ cuts in proof-structures. However, it is the actualisation of those diagrams that are considered. Actually, if we had other $\otimes$ and $\mathcal{Y}$ hyperedges above the vertices 1, 2, 4 or 5 of Example 67.3, execution of stellar resolution would duplicate and contract the cuts for all possible pairs of atoms without leaving intermediate cuts. It does not care about the structure of proof-structures since it is embedded as addresses of atoms themselves, they do not obstruct evaluation. I now present an example where cut-elimination should fail.