<figure><img src="image_64.png" /><figcaption>Figure 31.1: Correctness criterion as a way to test axioms (the computational essence of proofs). The interaction between axioms and test can be certified by either Girard’s long trip criterion or the Danos-Regnier criterion.</figcaption></figure>

a purely computational entity correspond to a proof-net? Cannot we simply work with
proof-nets as primitive objects directly? What is all this nonsense? The translation of
sequent calculus proofs into proof-structures even yields an inductive definition of proof-
nets. Correctness criterion are not even really used in practice. Moreover even if it had
a practical use, it does not even work well for full linear logic.

**§31.4 Correctness criteria as exit doors.** Correctness criteria are more interesting from a conceptual (not to say philosophical) point of view. They allow us to be *conscious of the format* we are in. They make us realise that something concrete and *material* regulate the logical entities we work with and their *use*. They exhibit the *shape* of logical constraints. Starting from proof-structures is actually a first step towards the dangerous computational and alogical world. We are testing the waters and there may be something beyond our format:

* what about starting from an even more general model of computation to go beyond proof-structures?

* if Danos-Regnier correctness is a way among others to test computational entities, what about considering other ways to test?

**§31.5 Correctness as testing.** Figure 31.1 shows that correctness hypergraphs can be seen as axiom links connected to a bottom part entirely definable from a sequent with a switching (since it corresponds to a switching applied to the syntax tree of a sequent).

* Axioms can be seen as a sort of program. They are invariant in the testing with switching hypergraphs. They hold the computational content of proofs.

* Switching hypergraphs can be seen as tests. A set of tests correspond to a specification.
It is similar to how programs are tested against several tests in order to check whether they have an expected behaviour or satisfy some specification. It makes logical correctness closer to the program testing of software engineering.

**§31.6 Making it explicit.** The theory of proof-nets suffers from several technical problems. Although a lot of them have been more or less solved, a question remains. What are we looking for? Are we satisfied? Is this the end of the history of logic?

* Logical correctness remains an *external* operation done on proof-structures. Hence logic is still *explained by us*. If we wish to understand logic more, we have to be able to reach an *internal explanation* without any “human intervention”.

* This implicit human intervention is actually very present. In correctness for multiplicative units, jumps can be seen as an external intervention.

* Another philosophically problematic point is that additive, exponentials and multiplicative units hides global operation dependent on a logical system, which makes proof-structures not so alogical. For instance: the two equal contexts of additive boxes can be seen as a hidden regulation.

Girard’s following quote at the end of the Blind Spot<fnref n="12" /> (2011) summarises his opinion on these problems:

> “Sequentialisation is not a dogma, it is a tool, which enabled one to find the procedural contents of nets; [...] But, on the whole, one has nothing against the idea of non-sequentialisable nets, as long as one can manipulate them: the ultimate meaning of logic is this ability to manipulate.

> – Jean-Yves Girard [Gir87a, Section 11.C.5]

This explains why Girard will later abandon the developments of original proof-nets to look for alternative spaces where linear logic can be expressed. In particular, he will strive for a more complete explicitation of those hidden assumptions of logical definitions where everything is syntax, including external and global operations.

**§31.7** This is nothing but abstract and vague intuitions. This is only starting from Girard’s transcendental syntax that these intuitions will be meaningful. But before reaching this point, the next destination is Girard’s geometry of interaction.

<footnote n="12">¹²I recently learned that there are actually at least three different versions of it.</footnote>
# Chapter 5

## The geometry of interaction

### 32 Towards a geometry of interaction

§32.1 Quickly following proof-nets, Girard introduced what he called a geometrical semantics of computation<fnref n="1" /> by starting from the multiplicative case [Gir87b]. With such a name, anyone would wonder if it is still about logic.

§32.2 In his paper "Multiplicatives", Girard remarks that proof-nets have something of a geometrical nature. We can actually forget formulas, connectives, everything and study proof-nets (and hence linear logic) only in terms of paths and shapes. This leads to a study of purely mathematical characterisations of proof-nets. Logic is not primitive but reconstructed from a notion of interaction corresponding to the now central cut-elimination procedure. He used simple permutations on natural number as a basis for proof-structures and was able to interpret MLL sequent calculus rules. This paper has later been developed by Danos and Regnier [DR89].

§32.3 It is only couple of years later that his new project has been presented under the name of "Geometry of Interaction" [Gir89b] (GoI) (a very confusing but cool name again). In this paper, he exposes his point of view on several topic of computer science and logic such as logic programming, denotational semantics and linear logic. What is striking is that this paper contains rather strong philosophical and conceptual insights. In particular, a very pragmatic point of view on linear logic is developed:

* MLL rules can be informally pictured with cables (cf. Figure 32.1). The connectives $\mathcal{Y}$ and $\otimes$ are two boxes in which the current flows differently;

* types/formulas are program specifications;

* a *dynamic* conception of meaning is defended;

* Girard opposes reductionism (which he associates with static interpretations of logic) and subjectivism (which he associates with bureaucracy, syntactic heaviness), and hence takes a philosophical position;

<footnote n="1">¹It seems that he was not yet too allergic to the word “semantics” at that time.</footnote>
<figure><img src="image_65.png" /><figcaption>Figure 32.1: MLL identity rules with cables.</figcaption></figure>

• vague links with physics or quantum computation are imagined at the end.

§32.4 What we now call “geometry of interaction” usually differ from Girard’s original motivations. It usually refers to:

• abstract machine exploring proof-nets or typed λ-terms (encoded as proof-nets) [DR99, AL95];

• categorical semantics taking dynamics into account [HS06].

But in this thesis, “geometry of interaction” refers to Girard’s original programme. Some
works more faithful to Girard’s original motivation exist. Thomas Seiller studied Girard’s
original geometry of interaction in his PhD thesis [Sei12b]. A categorical presentation
can also be found in Etienne Duchesne’s PhD thesis [Duc09].

§32.5 In Girard’s original programme, the theory of proof-structure is seen from the point of view of *paths*. Even more than the order of applications of logical rules, we forget almost everything: formulas, connectives, logical rules... Only paths are remaining. Cut-elimination is a computational procedure on paths and correctness criterion are criterion on paths. This opens the interpretation of linear logic to several models of paths.

**33 Multiplicative proofs with permutations**

This section is inspired by Seiller’s master thesis <fnref n="2" /> and PhD thesis [Sei12b] from which some
definitions are taken but explained in a different way.

<footnote n="2">²https://www.seiller.org/documents/pfnhyp.pdf</footnote>
<figure><img src="image_66.png" /><figcaption>(a) Correct proof-structure. There is a long trip 2-3-1-4-1-3-2.</figcaption></figure>

<figure><img src="image_67.png" /><figcaption>(b) Incorrect proof-structure. There are two short trips 1-4-1 and 2-3-2.</figcaption></figure>

Figure 33.1: Permutations associated with the two switchings of Figure 30.6.

<figure><img src="image_68.png" /><figcaption>Figure 33.2: Shifting proof-net theory to permutation theory.</figcaption></figure>
**§33.1** From the end of the previous section, we have seen that switching flow graphs and correctness hypergraphs can be divided into two disjoint parts: the *vehicle* (top, axioms) and a *test* (bottom, syntax forest of sequent). The rough idea is that if we look at the long trip criterion for a proof-structure for a given switching flow graph $S^\varphi$, paths do an alternation between vehicle and test. This decomposition is illustrated in Figure 33.2. If we only keep the mathematical content of the long trip criterion, both the vehicle and the test correspond to permutations over atomic formulas (represented by natural numbers standing for addresses of physical locations in the proof-structure). An example of translation of the paths of a proof-structure for two switchings (coming from Figure 30.6) into permutations is given in Figure 33.1.

**§33.2** Let $X = \{1, ..., n\} \subseteq \mathbb{N}^+$ be a finite sequence of strictly positive natural numbers representing atomic formulas in a proof. A *permutation* is a bijection $\sigma : X \to X$. It associates with each element of $X$ a unique other element of $X$. An association can be written $x \mapsto y$ when we have a permutation $\sigma$ such that $\sigma(x) = y$ (and $\sigma^{-1}(y) = x$). A permutation $\sigma$ can then be written $\{x_1 \mapsto y_1, ..., x_n \mapsto y_n\}$ or $\begin{bmatrix} x_1 & \cdots & x_n \\ y_1 & \cdots & x_n \end{bmatrix}$ when $\sigma(x_i) = y_i$. The association should be read from top to bottom in its matrix presentation.

**§33.3** From the trips of a switching hypergraph $S^\varphi$ with a given switching $\varphi$, it is possible to extract two permutations $\sigma_{ax}$ and $\sigma_\varphi$ corresponding to the axioms of $S$ and to $S^\varphi$ respectively. We enumerate each box corresponding to the $n$ atomic formulas and obtain a sequence of natural numbers $X = \{1, ..., n\}$.

* The permutation $\sigma_{ax} : X \to X$ is constructed by adding an association $n \mapsto m$ when there is a directed path from $n$ to $m$ from the top.

* The permutation $\sigma_\varphi : X \to X$ is constructed by adding an association $n \mapsto m$ when there is a directed path from $n$ to $m$ from the bottom.

For instance, the two permutations in Figure 33.1a can respectively be represented by $\begin{bmatrix} 1 & 2 & 3 & 4 \\ 4 & 3 & 2 & 1 \end{bmatrix}$ and the two permutations in Figure 33.1b by $\begin{bmatrix} 1 & 2 & 3 & 4 \\ 4 & 3 & 2 & 1 \end{bmatrix}$ and $\begin{bmatrix} 1 & 2 & 3 & 4 \\ 4 & 2 & 3 & 1 \end{bmatrix}$.

## Long-trip criterion with cyclic permutations

**§33.4 Cyclic permutations.** The point is now to characterise the long trip criterion only from permutations (which mean nothing in particular). Permutations can be composed like any functions. For instance, if we compose the two previous permutations $\sigma := \begin{bmatrix} 1 & 2 & 3 & 4 \\ 4 & 3 & 2 & 1 \end{bmatrix}$ and $\tau := \begin{bmatrix} 1 & 2 & 3 & 4 \\ 3 & 2 & 1 & 4 \end{bmatrix}$, it is possible to plug the associations vertically with $\sigma$ over $\tau$ to construct the sequence of associations $1 \mapsto 4 \mapsto 4$, $2 \mapsto 3 \mapsto 1$,
$3 \mapsto 2 \mapsto 2$ and $4 \mapsto 1 \mapsto 3$, written $\begin{bmatrix} 1 & 2 & 3 & 4 \\ 4 & 3 & 2 & 1 \\ 4 & 1 & 2 & 3 \end{bmatrix}$. This induces a new permutation

$\tau \circ \sigma = \begin{bmatrix} 1 & 2 & 3 & 4 \\ 4 & 1 & 2 & 3 \end{bmatrix}$. Composition is often written $\tau \sigma$ instead of $\tau \circ \sigma$.

We say that a permutation $\sigma : X \to X$ is *cyclic* when for $\sigma^0(1) \neq \sigma^1(1) \neq \dots \neq \sigma^{|X|-1}(1)$ with $1 \in X$. It means that starting from 1, if we move one step by following $\sigma$, we end on a different location (atomic formula), if we move one step further, we end again a location different from the previous and so on until we do $|X|-1$ moves which would be sufficient to traverse all natural numbers. It means that the permutation when composed with itself forms one big cycle (you should be able to see how it is related to long trips) by alternating between the two components of the composition.

**§33.5** If permutations are represented as in Figure 33.1, then to check if $\tau\sigma$ is cyclic, we can merge the two corresponding graphs along identical natural numbers. We start from 1. One application of $\tau\sigma$ correspond to moving one step along the edges. If we are able to always reach different numbers in 3 steps then we must have reached all the locations.

* If $\sigma := \sigma_{ax}$ and $\tau := \sigma_{\varphi}$ are extracted from the correct proof-structure of Figure 33.1a, then it appears that $\tau\sigma$ is cyclic because we have: $(\tau\sigma)^0(1) = 1$, $(\tau\sigma)^1(1) = 4$, $(\tau\sigma)^2(1) = 3$ and $(\tau\sigma)^3(1) = 2$.

* As for the two permutations of Figure 33.1b, we can see why their composition is not cyclic. If $\sigma$ is the composition of the two permutations extracted from the proof-structure, then $\sigma^0(1) = 1$, $\sigma^1(1) = 4$ and $\sigma^2(1) = 4$ which is a short trip.

**§33.6 Decomposition of permutation.** Any permutation can be decomposed into a composition of circular permutations with disjoint domains. Each circular permutation is closed under reachability by association of a permutation. This gives an alternative notation for permutation where $(x_1x_2\dots x_n)$ corresponds to a circular sequence of associations $x_1 \mapsto x_2 \mapsto \dots \mapsto x_n$. For instance (132) is the permutation $\begin{bmatrix} 1 & 2 & 3 \\ 3 & 1 & 2 \end{bmatrix}$ (1 gives 3 which gives 2 then 1 back again). The permutation $\begin{bmatrix} 1 & 2 & 3 & 4 \\ 4 & 3 & 2 & 1 \end{bmatrix}$ can be rewritten (14)(23) and $\begin{bmatrix} 1 & 2 & 3 & 4 \\ 3 & 2 & 1 & 4 \end{bmatrix}$ can be rewritten (13)(2)(4). We have that $\tau\sigma$ is cyclic when its decomposition is a unique cyclic permutation (corresponding to a long trip). Otherwise, each components of the decomposition correspond to a short trip.

**§33.7 Orthogonality.** We are now able to mathematically express the long trip criterion. We say that two permutations $\tau$ and $\sigma$ are *orthogonal*, written $\tau \perp \sigma$, when $\tau\sigma$ is cyclic. Orthogonality is symmetric since permutations are bijective and $\tau\sigma$ can be rewritten $\sigma^{-1}(\sigma\tau)\sigma$ [Gir87b, Section 2.3].
<figure><img src="image_69.png" /><figcaption>Figure 33.3: Cut-elimination for a proof-structure. We have the two following permutations: $\sigma_{ax} := \begin{bmatrix} 1 & 2 & 3 & 4 & 5 & 6 \\ 2 & 1 & 4 & 3 & 6 & 5 \end{bmatrix} = (12)(34)(56)$ and $\sigma_{cut} := \begin{bmatrix} 1 & 2 & 4 & 5 \\ 4 & 5 & 1 & 2 \end{bmatrix} = (14)(25)$.</figcaption></figure>

**§33.8 Theorem.** A proof-structure $\mathcal{S}$ is MLL-certifiable if and only if for all switchings $\varphi$ of $\mathcal{S}$, we have $\sigma_{\varphi} \perp \sigma_{ax}$ where $\sigma_{ax}$ and $\sigma_{\varphi}$ respectively correspond to the permutation associated with the axioms of $\mathcal{S}$ and the switching hypergraph $\mathcal{S}^{\varphi}$.

General interaction of permutation and cut-elimination

**§33.9** The verification of the cyclicity of a permutation $\tau\sigma$ corresponds to a sort of *interaction* between two permutations. It works as if we connected two permutations to look at all the possible alternating paths induced. But cut-elimination is also a sort of interaction between axioms and cuts since multiplicative cuts are way to reorganise atomic formulas by rewiring or contraction.

**§33.10** Cut-elimination can also be studied only from the notion of *paths*. A normal form makes explicit the shortcuts between input/output atomic formulas given by cuts. For instance, in Figure 33.3, the normal form connects 3 and 6. This normal form tells us that if we start from the input point 3, it is possible to reach 6 by following the rules of cut-elimination. Cuts also induce a permutation $\sigma_{cut}$ on atomic formulas with the rewiring obtained by eliminating all multiplicative cuts $\otimes/\mathbb{9}$. In Figure 33.3, the permutation corresponding to cuts is $\sigma_{cut} := \begin{bmatrix} 1 & 2 & 4 & 5 \\ 4 & 5 & 1 & 2 \end{bmatrix}$. The difference between verifying the long trip criterion and cut-elimination is that switching are *full* connexions between atomic formulas, represented by total permutations whereas cut-elimination only partially (potentially totally) connects atomic formulas. In the latter case, we must consider permutations over a subset of atoms.

**§33.11 Plugging.** Let $\sigma: X \cup Y \to X \cup Y$ and $\tau: Y \cup Z \to Y \cup Z$ be two permutations with $X, Y, Z$ sequences of natural numbers over $\mathbb{N}^+$ and $X \cap Z = \emptyset$. The two permutations can be decomposed with disjoint partial injections (we keep the notation of permutations) relating subsets of their domain. We write $\sigma[E, F] : E \to F$ for such bijections. We obtain:

* the decomposition $\sigma = \sigma_{[X,X]} + \sigma_{[Y,X]} + \sigma_{[X,Y]} + \sigma_{[Y,Y]}$;
<figure><img src="image_70.png" /><figcaption>Figure 33.4: Interaction between two permutations $\sigma : X \cup Y \to X \cup Y$ and $\tau : Y \cup Z \to Y \cup Z$ with $X \cap Z = \emptyset$ as the computation of a new permutation $\text{Ex}(\tau, \sigma) : X \cup Z \to X \cup Z$ which is defined only if we can always go out of the loop. The inputs are on the left and the outputs on the right.</figcaption></figure>

• the decomposition $\tau = \tau_{[X,X]} + \tau_{[Y,X]} + \tau_{[X,Y]} + \tau_{[Y,Y]}$

where $\sigma + \sigma' : X \cup X' \to Y \cup Y' = \begin{bmatrix} x_1 & \cdots & x_n & y_1 & \cdots & y_n \\ x'_1 & \cdots & x'_n & y'_1 & \cdots & y'_n \end{bmatrix}$ when $\sigma : X \to X' = \begin{bmatrix} x_1 & \cdots & x_n \\ x'_1 & \cdots & x'_n \end{bmatrix}$ and $\sigma : Y \to Y' = \begin{bmatrix} y_1 & \cdots & y_n \\ y'_1 & \cdots & y'_n \end{bmatrix}$. To define the plugging (or interaction) $\text{Ex}(\tau, \sigma)$ between $\sigma$ and $\tau$, we define a (potentially infinite) path starting either from $X$ or $Z$ to either $X$ or $Z$ by traversing the place of interaction $Y$ (potentially several times). We obtain the following definition of plugging:

$$ \text{Ex}(\tau, \sigma) := \text{Ex}(\tau, \sigma)_{[X,X]} + \text{Ex}(\tau, \sigma)_{[X,Z]} + \text{Ex}(\tau, \sigma)_{[Z,X]} + \text{Ex}(\tau, \sigma)_{[Z,Z]} \text{ with} $$

$$ \text{Ex}(\tau, \sigma)_{[X,X]} := \sigma_{[X,X]} + \sum_{k=0}^{\infty} \sigma_{[X,Y]} \tau_{[Y,Y]} (\sigma_{[Y,Y]} \tau_{[Y,Y]})^k \sigma_{[Y,X]}; $$

$$ \text{Ex}(\tau, \sigma)_{[Z,X]} := \sum_{k=0}^{\infty} \sigma_{[X,Y]} (\tau_{[Y,Y]} \sigma_{[Y,Y]})^k \tau_{[Y,Z]}; $$

$$ \text{Ex}(\tau, \sigma)_{[X,Z]} := \sum_{k=0}^{\infty} \tau_{[Z,Y]} (\sigma_{[Y,Y]} \tau_{[Y,Y]})^k \sigma_{[Y,X]}; $$

$$ \text{Ex}(\tau, \sigma)_{[Z,Z]} := \tau_{[Z,Z]} + \sum_{k=0}^{\infty} \tau_{[Z,Y]} \sigma_{[Y,Y]} (\tau_{[Y,Y]} \sigma_{[Y,Y]})^k \tau_{[Y,Z]}. $$

This new permutation $\text{Ex}(\tau, \sigma)$ may not always be defined (it is not when there are infinitely many paths). The process underlying the construction of $\text{Ex}(\tau, \sigma)$ is illustrated in Figure 33.4. The formula corresponding to $\sigma :: \tau$ is also known as the *execution formula*. I comment $\text{Ex}(\tau, \sigma)_{[X,X]}$ (and the other permutations follow the same reasoning). It either goes directly from $X$ to $X$ in one step or goes to $Y$ through $\sigma_{[Y,X]}$ then goes
<figure><img src="image_71.png" /><figcaption>Figure 33.5: Interaction between two permutations $\sigma : X \cup Y \to X \cup Y$ and $\tau : Y \to Y$ as the computation of a new permutation $\mathrm{Ex}(\tau, \sigma) : X \to X$ which is defined only if we can always go out of the loop. The inputs are on the left and the outputs on the right. The box $\tau$ is often omitted and replaced by a loop from $Y$ to $Y$ in the box $\sigma$.</figcaption></figure>

several times in a (potentially infinite) loop from $X$ to itself to finally exit by $X$.

§33.12 Plugging (simplified). In the above definition, $X$ and $Z$ correspond to the atoms of two disjoint proofs which are not related by cuts. For instance, in Figure 33.3, we would have $X = \emptyset$ and $Z = \{3, 6\}$. The atoms which interact are $Y = \{1, 2, 4, 5\}$. However, our definition is too general. It is sufficient to set $Z := \emptyset$ at put all atoms unrelated to cuts in $X$. This is because the connexion between two disjoint proofs can be seen as an interaction happening within a single proof (i.e. you either see the proof-structure of Figure 33.3 as connecting two proofs by a cut or see it as a unique proof, as a whole). In this case we obtain the simplified version of plugging between $\sigma : X \cup Y \to X \cup Y$ (axioms with some atoms unrelated to cuts in $X$) and $\tau : Y \to Y$ (cuts):

$$ \mathrm{Ex}(\tau, \sigma) = \mathrm{Ex}(\tau, \sigma)_{[X,X]}. $$

This situation of simplified plugging corresponds to the illustration of Figure 33.5 which simplifies Figure 33.4.

§33.13 We illustrate plugging with the proof-structure of Figure 33.3. We have

$$ \mathrm{Ex}(\sigma_{\mathrm{cut}}, \sigma_{\mathrm{ax}}) := \sigma_{\mathrm{ax}[X,X]} + \sum_{k=0}^{\infty} \sigma_{\mathrm{ax}[X,Y]} \sigma_{\mathrm{cut}[Y,Y]} (\sigma_{\mathrm{ax}[Y,Y]} \sigma_{\mathrm{cut}[Y,Y]})^k \sigma_{\mathrm{ax}[Y,X]} $$

with $X = \{3, 6\}$ and $Y = \{1, 2, 4, 5\}$. There is direct association from $X$ to $X$ in one step hence $\sigma_{\mathrm{ax}[X,X]} = \emptyset$ (paths of length 1). Now we compute the formula for different values of $k$.

◇ Case $k = 0$ (paths of length 3 from $X$ to $X$): we have

$$ \sigma_{\mathrm{ax}[X,Y]} \sigma_{\mathrm{cut}[Y,Y]} \sigma_{\mathrm{ax}[Y,X]} $$
$$ 
\begin{aligned}
&= \emptyset \circ \begin{bmatrix} 4 & 5 \\ 1 & 2 \end{bmatrix} \circ \begin{bmatrix} 3 & 6 \\ 4 & 5 \end{bmatrix} \\
&= \emptyset \text{ (undefined)};
\end{aligned}
$$

◇ Case $k = 1$ (paths of length 5 from X to X): we have

$$ 
\begin{aligned}
& \sigma_{ax[X,Y]} \sigma_{cut[Y,Y]} (\sigma_{ax[Y,Y]} \sigma_{cut[Y,Y]}) \sigma_{ax[Y,X]} \\
&= \begin{bmatrix} 5 & 4 \\ 6 & 3 \end{bmatrix} \circ \begin{bmatrix} 2 & 1 \\ 5 & 4 \end{bmatrix} \circ \begin{bmatrix} 1 & 2 \\ 2 & 1 \end{bmatrix} \circ \begin{bmatrix} 4 & 5 \\ 1 & 2 \end{bmatrix} \circ \begin{bmatrix} 3 & 6 \\ 4 & 5 \end{bmatrix};
\end{aligned}
$$

Remark that since we are alternating between axioms and cuts, only paths of odd length are considered. We see that there is a path of length 5 between 3 and 6, meaning that the proof-structure has a normal form.

§33.14 Correctness with general plugging. By using this more general definition of plugging, it is possible to characterise long trip correctness. The execution $Ex(\tau, \sigma)$ computes maximal alternating paths from inputs/outputs. The idea is to turn a long trip into a maximal path. This is what Seiller did with his interaction graphs using graphs instead of permutations [Sei12a]. It is sufficient to distinguish an edge (representing an association in a permutation) and consider a maximal path between the two disconnected vertices. The advantage of expressing orthogonality with execution is that a lot of results are usually free such that the adjunction property which ensure a correct interpretation of linear logic and the possibility to define a categorical model (*-autonomous category).

§33.15 Proof-structures are now fully characterised by vehicles corresponding to links between atoms. The orthogonality relation $\perp$ formalises the fact that a vehicle (or program) passes a test. A permutation is hence MLL-certifiable (logically correct) when it passes all the tests for a given set of tests corresponding to a sequent $\vdash \Gamma$. It remains to define the set of tests corresponding to a sequent.

### Interpretation of types/formulas

§33.16 Remark that in the world of permutations, there is no difference between vehicles and tests, they are of same nature. In particular, set of axioms (which can be seen as a type defined as a set of programs) opposes set of tests (which can be seen as way to assert that a program is of some type). We can construct arbitrary set of tests or vehicles by putting permutations in a set. Let $\mathbf{A}$ be such a set. We define its orthogonal $\mathbf{A}^{\perp} := \{\sigma \mid \forall \tau \in \mathbf{A}, \tau \perp \sigma\}$. Given a permutation $\sigma$, it is possible to say that it passes all the tests of a set $\mathbf{A}$ by writing $\sigma \in \mathbf{A}^{\perp}$. Not all sets will correspond to MLL formulas/types. The good sets are called behaviours and are closed by biorthogonal. The following definitions are very similar to realisability interpretations (cf. Section 22). An even more similar and notable work is Beffara's realisability interpretation used to
speak about concurrent computation and linear logic [Bef06]. His approach differs from the fact that he starts from process calculi but the same techniques are used. Beffara's work can be seen as an alternative interpretation of linear logic.

§33.17 **Definition (Behaviour)**. A set of permutations **A** is a *behaviour* when **A** = **A**⊥⊥.

§33.18 Behaviours corresponds to MLL formulas (in which linear negation is involutive). An intuitive way to understand this requirement is through the alternative equivalent definition.

§33.19 **Proposition**. Let **A** be set of permutations. We have that **A** is a behaviour if and only if there exists a set of permutations **B** such that **A** = **B**⊥.

*Proof.* The proof can be found in the literature [JS21, Proposition 15]. □

§33.20 This alternative definitions tells us that **A** is a behaviour when there is a set of tests **B** fully characterising **A**. In particular, all elements of **A** pass the tests of **B**. In other word, a behaviour is set of *testable* permutations. The idea is now to construct behaviours corresponding to all MLL formulas.

§33.21 As we have seen in the previous chapter, the proof-nets of $A \otimes B$ join two disjoint proof-nets (cf. Figure 29.8). It is then natural to define the tensor as a disjoint union of set of permutations. Moreover, the switchings for $\otimes$ (cf. Figure 30.3a) correspond to reunion of switching flow graphs. The only way to be orthogonal to them (by forming a long trip) is having two disjoint switching flow graphs (otherwise we would have short trips).

§33.22 **Definition (Support of set of permutations)**. Let **A** be a set of permutations. If all permutations $\sigma \in \mathbf{A}$ are defined on a same set $X$, then $X$ is called the *support of* **A**. The support of **A** is written $\text{dom}(\mathbf{A})$.

§33.23 **Definition (Tensor)**. Let **A** and **B** be two behaviours with disjoint support, i.e. $\text{dom}(\mathbf{A}) \cap \text{dom}(\mathbf{B}) = \emptyset$. We define their tensor as a new behaviour:

$$ \mathbf{A} \otimes \mathbf{B} := \{\sigma_A + \sigma_B \mid \sigma_A \in \mathbf{A}, \sigma_B \in \mathbf{B}\}^{\perp\perp}. $$

§33.24 The double orthogonality in the definition is there to ensure that $\mathbf{A} \otimes \mathbf{B}$ is a behaviour. Depending on the chosen orthogonality relation, it is not always the case. If we already have a behaviour, i.e. $\mathbf{A} \otimes \mathbf{B} = \{\sigma_A + \sigma_B \mid \sigma_A \in \mathbf{A}, \sigma_B \in \mathbf{B}\}$, then we say that the tensor satisfies the property of *internal completeness*.

§33.25 Finally, $\mathcal{Y}$ is defined by the orthogonal of $\otimes$. The tests correspond to disjoint unions of switching flow graphs waiting to be reunited. The proofs of $A \mathcal{Y} B$ then reunites a proof of **A** with a proof of **B**. We finally also obtain a definition of linear implication.
§33.26 **Definition (Par).** Let **A** and **B** be two behaviours with disjoint support. We define the new behaviour:

$$ \mathbf{A} \not\mathcal{Y} \mathbf{B} := (\mathbf{A}^{\perp} \otimes \mathbf{B}^{\perp})^{\perp}. $$

§33.27 **Definition (Linear implication).** Let **A** and **B** be two behaviours with disjoint support. We define the new behaviour:

$$ \mathbf{A} \to \mathbf{B} := \mathbf{A}^{\perp} \not\mathcal{Y} \mathbf{B}. $$

§33.28 **Comparison with realisability interpretation.** This interpretation of linear logic matches with realisability interpretations in Section 22 (especially Krivine's classical realisability). The difference is that we are starting from permutations instead of $\lambda$-terms, there is no duality between $\lambda$-terms (programs) and stacks (tests) since they both are permutations in the GoI, and finally we are reconstructing multiplicative linear logic instead of classical logic. The pole is implicit in our case but could have been made explicit by defining orthogonality from execution. It is also possible to have an alternative definition of linear implication which would be closer to the definition of realisability.

§33.29 **Proposition.** Let **A** and **B** be two behaviours with disjoint support. We have:

$$ \mathbf{A} \to \mathbf{B} = \{ \sigma_F \mid \forall \sigma_A \in \mathbf{A}, \mathbf{Ex}(\sigma_F, \sigma_A) \in \mathbf{B} \}. $$

*Proof.* This is easily proven by using the *adjunction property* which is obtained by defining orthogonality from execution [Sei12a, Definition 26]. □

§33.30 **Generalised multiplicatives.** As illustrated in Figure 33.2, even though proof-net theory can be simulated with permutations, permutations are even more general than proof-structures. It is possible to construct permutations and make them interact without representing proof-structures. In particular, it is possible to define sets of tests not corresponding to MLL types and to obtain generalised formulas [Gir87b, Section 3]. A typical example is to mix tests coming from different formulas (by exchanging some $\not\mathcal{Y}$ and $\otimes$) because tests coming from MLL sequents are usually *uniform*. In some cases, the corresponding set of tests can have a non-empty orthogonal, meaning that it can be instantiated to actual proofs called *non-sequentialisable* since they do not correspond to sequent calculus proofs. However, the purpose of such generalised multiplicatives living outside usual MLL was not clear. It has been investigated later by Acclavio and Maieli by using partitions instead of permutations [AM20].

§33.31 **What about Danos-Regnier correctness?**. Since permutations are about binary links and that the test for tensor in Danos-Regnier correctness is a ternary edge (hyperedge), the interpretation of proofs with permutation can naturally express long trips but not Danos-Regnier switching hypergraphs. Other solutions will be proposed in the next sections (cf. Section 37). The transcendental syntax, which is the subject of this
thesis will also be a solution where both long trips and Danos-Regnier correctness can
be expressed. However, it is still possible to characterise MLL+MIX in another way
[NS19, Theorem 42] by using acyclicity for orthogonality, which can be expressed with
nilpotency of the interaction between two permutations.

§33.32 **A paradigm of uniform interaction.** More than a new interpretation of proof-nets, the GoI provides a paradigm in which proofs and tests are computationally interactive entities of same kind. In particular, the cut is a way to put two entities in conflict and cut-elimination is a way to trigger an interaction. The interpretation of types as behaviours provides a way to speak about the computational behaviour of logical entities depending of how they interact with other objects. This idea of paradigm of interaction has been discussed by Abramsky [Abr16, Section 5].

§33.33 **Communication without understanding.** The notion of “communication without understanding” is a recurrent idea in Girard’s papers. It appeared since the first paper on GoI [Gir89a, Section V.2] and served as a motivation until his project of transcendental syntax, succeeding the GoI. The idea is that when two logical entities Φ and Ψ interact (permutations or operators representing proof-nets), they are connected by points of reference (for instance a cut between A⊥∁B⊥ and A⊗B) making them able to react in a generic way through their “interface”. However, this communication is done without understanding since what happens in one entity is independent from the other entity. The computational reaction is only dependent on the points of reference which connects Φ and Ψ. Actually, we could change names or substitute the atoms Xᵢ by more complex proof-nets in Φ, Ψ would not be aware of that private change and still react in the same way. As Girard explains, it is as if Φ and Ψ corresponded to an internal language of thoughts for two persons (their consciousness?). These two persons have an illusion of mutual understanding through points of reference allowing a consensus, but those points are treated generically from each person’s point of view. For instance, two persons talk about “democracy” or left/right in politics but although they can recognise the words and react to it, they will both treat the word depending on their own point of view or understanding.

**34 Infinitary extension towards full linear logic**

§34.1 This idea of representing proofs by permutations has been extended to MELL in Girard's first official technical paper on the GoI [Gir89a]. This is the first paper of a series of six papers. Atomic formulas can now be duplicated or erased, hence there can be infinitely many copies of one atomic formula. We need to extend our interpretation to something which would look like permutations (or matrices since permutations induce matrices) over an infinite countable space. A natural<fnref n="3" /> solution has been suggested by Girard. There are a lot of equivalent formulation of this solutions which can be found in Girard's

<footnote n="3">³Apparently it is natural for mathematicians.</footnote>
article on GoI [Gir89a], Seiller PhD thesis [Sei12b, Section 4.1], one of Shirahata’s article [Shi03, Section 3] or Duchesne’s PhD thesis [Duc09]. This is due to the fact that the interpretation works in very “large” spaces but not all the power of these spaces is used. It is then sufficient to consider simpler interpretations. In Girard’s terms [Gir11a, Section 19.3.10], his solution is basically a “preposterous dressing of a theory of the partial permutations of N”.

§34.2 A canonical solution<fnref n="4" /> is to consider operators on the Banach space $B(\mathbb{H})$ of bounded operator on the Hilbert space $\mathbb{H} := l^2(\mathbb{N})$. This provides a sort of generalised algebra of matrices. Objects of $\mathbb{H}$ are infinite sequences of complex numbers indexed by natural numbers $z = (z_i)_{i \in \mathbb{N}} = (z_1, z_2, ...)$ such that $\sum_{i=0}^{\infty} z_i \bar{z}_i < \infty$ where $\overline{a + ib} = a - ib$. These sequences will represent atomic formulas in a proof-structure. The norm of $z$ is defined $\|z\| := \sqrt{\sum_{i=0}^{\infty} z_i \bar{z}_i}$. Operators $u$ (which are used to represent proofs by generalising finite permutations) are linear transformation<fnref n="5" /> on $\mathbb{H}$ such that $\sup\{\|u(z)\| \text{ such that } \|z\| = 1\}$ is finite. Given two sequences $x = (x_i)_{i \in \mathbb{N}}$ and $y = (y_i)_{i \in \mathbb{N}}$, it is possible to define their scalar product $\langle x, y \rangle = \sum_{i=0}^{\infty} x_i y_i$. From this scalar product, we can define an adjoint operation $u \mapsto u^*$ such that $\langle u(x), y \rangle = \langle x, u^*(y) \rangle$. You do not have to understand what that means<fnref n="6" />.

§34.3 We now have a lot of tools from this large space for linear logic. The most important elements we need is:

• a way to internalise $\mathbb{H} \oplus \mathbb{H}$ into $\mathbb{H}$, yielding $\mathbb{H} \oplus \mathbb{H} \simeq \mathbb{H}$ in order to interpret binary multiplicative connectives;

• an internalisation yielding $\mathbb{H} \otimes \mathbb{H} \simeq \mathbb{H}$ in order to interpret copies of atoms (for exponentials).

As explained by Seiller [Sei12b, Section 4.1], it is sufficient to use bijections on natural numbers yielding $\mathbf{N} \times \mathbf{N} \simeq \mathbf{N}$ and $\mathbf{N} + \mathbf{N} \simeq \mathbf{N}$ because a separation of the space of indices is sufficient to separate $\mathbb{H}$.

§34.4 **Interpretation of binary connectives.** The internalisation of direct sum takes the form of two operators<fnref n="7" /> $l: \mathbb{H} \to \mathbb{H}$ and $r: \mathbb{H} \to \mathbb{H}$ (more precisely, partial isometries). Which are ways to project elements of $\mathbb{H}$ to either the left or right part of a splitted space $\mathbb{H} \oplus \mathbb{H}$, exactly like the rule $\oplus$ of linear logic. We require that they satisfy $l^*r = r^*l = 0$ and $l^*l = r^*r = 1$ where 0 and 1 are respectively the null and identity operators which are guaranteed to exist. The point is that $l$ and $r$ can be composed to encode paths (as operators) in a proof-structure where $l$ means “go down left” and $r$ means “go down right”. The adjoint provides dual operations $l^*$ for “going up left” and $r^*$ for “going up right”. In particular, the equation $l^*l = r^*r = 1$ is consistent with $\mathfrak{Y} \otimes$ cut-elimination:

<footnote n="4">⁴According to Girard, it took him one year to achieve the extension to exponentials.</footnote>

<footnote n="5">⁵A mapping $u: \mathbb{H} \to \mathbb{H}$ such that $u(x + y) = u(x) + u(y)$ and $u(kz) = ku(z)$ for $k \in \mathbf{C}$ (the set of complex numbers).</footnote>

<footnote n="6">⁶Because neither I do.</footnote>

<footnote n="7">⁷Originally named *p* and *q*.</footnote>
going down from a premise of a direction *d* (left or right) then going up in the premise of same direction *d* as in Figure 33.3 (the path has to be reversed to follow operator composition). As for $l^*r = r^*l = 0$, it means that it is invalid to not be consistent with the chosen direction of premise because such paths are not preserved by cut-elimination and the composition of operator is hence cancelling.

**§34.5** It is possible to represent operators by matrices generalising the matrices associated with finite permutations. In MLL with finite permutations, boolean coefficient are sufficient: we have a coefficient 1 when there is an association $i \mapsto j$ in the permutation where $i$ is the index of rows (source) and $j$ the index of columns(target). The coefficient is 0 otherwise. An axiom link between two atoms 1 and 2 is represented by the permutation $\begin{bmatrix} 1 & 2 \\ 2 & 1 \end{bmatrix}$ which corresponds to the square matrix $\begin{pmatrix} 0 & 1 \\ 1 & 0 \end{pmatrix}$. As for cuts, they are represented with symmetric matrices since they are two-way linking of formulas. This corresponds to *partial symmetries* in Banach spaces. More generally, proofs can be represented by matrices of operators (recall that 0 and 1 are operators as well). Instead of the presence of a link, it is possible to encode the path with the partial isometries $p$ and $q$, relatively to a conclusion. Operators can also be interpreted by more compact big matrices featuring information about cuts [Shi03, Section 3.4]. Concrete examples of matrices can be found in Pistone's works [Pis15].

**§34.6** Interpretation of exponentials. The internalisation of tensor product provides a tensorisation of operators $u \otimes v$ such that $(u \otimes v)(x \otimes y) = ux \otimes vy$ allowing to attach (by pairing) and stack information. The rough idea is that it allows to add more information (that Girard calls “message space” [Gir11a, Section 19.3.5]) to paths in order to specify what I call a *copy identifier* which says whether we have a left or right copy (for the two branches of contraction link). The promotion turns an operator $u$ (corresponding to a proof) into $1 \otimes u$ (corresponding to a proof in an exponential box) where 1 is the location of a potential copy identifier. Weakening is handled by adding 0 coefficient for a new atom in the matrix of a proof. Contraction is handled with operators $x \otimes 1$ where $x \in \{l, r, l^*, r^*\}$ to specify that we are either entering or exiting a left or right copy of an atom (without altering the multiplicative part on the right). This is explained in Shirahata's paper [Shi03, Section 3.7].

**§34.7** Feedback equation and execution. In the same fashion as in Figure 33.4, it is possible to define an equation in terms of operators for which the solution corresponds to the cut-elimination of a proof. This equation is called *feedback equation* [Gir06]. Imagine that we have an operator $u : \mathbb{H} \oplus \mathbb{H}' \to \mathbb{H} \oplus \mathbb{H}'$ representing axioms such that $u(x \oplus y) = x' \oplus y'$ for some $x'$ and $y'$ (it is the box of $\sigma$ in Figure 33.4) and an operator $v : \mathbb{H}' \oplus \mathbb{H}'' \to \mathbb{H}' \oplus \mathbb{H}''$ representing another set of axioms such that $v(y' \oplus z) = y \oplus z'$ for some $z'$ (it corresponds to the box of $\tau$ in Figure 33.4). We obtain the following feedback
equation system:

$$u(\mathbf{x} \oplus \mathbf{y}) = \mathbf{x}' \oplus \mathbf{y}'$$

$$v(\mathbf{y}' \oplus \mathbf{z}) = \mathbf{y} \oplus \mathbf{z}'$$

As in Paragraph 33.12, the equation can be simplified and we obtain:

$$u(\mathbf{x} \oplus \mathbf{y}) = \mathbf{x}' \oplus \mathbf{y}'$$

$$\sigma(\mathbf{y}') = \mathbf{y}$$

where $\sigma$ is the partial symmetry associated with cuts. Similarly to the right picture of Figure 33.5, when it has a solution, the equation induces an operator $w : \mathbb{H} \to \mathbb{H}$ such that $w(\mathbf{x}) = \mathbf{x}'$. This operator is defined by the execution formula:

$$\mathrm{Ex}(u, \sigma) := (1 - \sigma^2)u(1 - \sigma u)^{-1}(1 - \sigma^2).$$

The expression $u(1 - \sigma u)^{-1}$ is a fancy way to write $\sum_{k=0}^{\infty} u(\sigma u)^k = u + u\sigma u + u\sigma u\sigma u + ...$ which is the sum of all possible alternation between axioms and cuts. The expression is an operator algebraic version of the simplified plugging of Paragraph 33.12. The expression $(1 - \sigma^2)$ is a way to filter the result in order to keep paths starting outside the space of cuts and terminating outside of cuts (so that we indeed represent a maximal path between two inputs/outputs). As explained by Shirahata [Shi03, 3.6], $\sigma^2$ is an operator projecting inputs into either the other side of the cut or 0. If $(\sigma^2)(\mathbf{x}) = \mathbf{y} \neq 0$, then there is a cut between $\mathbf{x}$ and $\mathbf{y}$. The operator $1 - \sigma^2$ projects its inputs to themselves if they are not part of cuts (which is equivalent to applying the identity operator doing nothing) or 0 (which would cancel the whole path).

§34.8 **Orthogonality by nilpotency.** It appears that the execution formula is not always defined (the intuition is that it can loop) but it is defined when $\sigma u$ is nilpotent$^8$, i.e. there exists $k \in \mathbb{N}$ such that $(\sigma u)^k = 0$. This ensures that there is a point where the infinite sum $\sum_{k=0}^{\infty} u(\sigma u)^k$ can stop. This naturally defines an orthogonality relation between operators (without even trying to characterise a specific correctness criterion). We say that two operators $u$ and $v$ are *orthogonal*, written $u \perp v$, when $uv$ is nilpotent. From this orthogonality relation (which is directly based on execution this time, unlike our original definition with cyclicity of finite permutations), it is possible to interpret formulas/types as set of operators, exactly as in Section 33. It has later been established that nilpotency is related to acyclicity of graphs, which characterises MLL+MIX correctness (and not MLL) [NS19, Theorem 42].

§34.9 **A mathematisation of algorithms.** Following this first technical paper on the GoI, Girard introduced a second paper [Gir16b] with more ambitions:

<footnote>$^8$Actually, as Seiller explained, weak nilpotency is sufficient [Sei12b, §4.1.17].</footnote>
> This paper is the main piece a general program of mathematisation of algorithmics, called geometry of interaction. We would like to define independently of any concrete machine, any extant language, the mathematical notion of an algorithm.

> - Jean-Yves Girard

The geometry of interaction is no more meant to be a mathematical explanation of linear logic or of proof-nets but a step towards the redefinition of the relation between logic and computation. Because the execution formula is able to mathematically express the computation appearing in logic independently of any computational system, Girard defines an algorithm by a pair of operators $(u, \sigma)$ which can be executed with $Ex(u, \sigma)$. In order to consider more general computation, Girard wanted to represent untyped $\lambda$-calculus by studying more general solutions of the feedback equation using *weak nilpotency* [Sei12b, §4.1.17] instead of nilpotency. The difficult is then to find a setting where this works because $1 - \sigma u$ (appearing in the execution formula) is not invertible in general (and we need it to be invertible because the execution formula is defined by $(1 - \sigma^2)u(1 - \sigma u)^{-1}(1 - \sigma^2)$) under the assumption of weak nilpotency. It seems that this project of *mathematisation of algorithms* has been postponed but recently restored by Seiller and Naibo.

§34.10 **From operators to logic.** In his third paper on GoI [Gir95], Girard introduced a new simplified interpretation by comparing his execution formula with the execution of logic programs (cf. Section 23). In particular, he tries to extend the interpretation to MALL. Since this topic deserves its own section (in the context of this thesis), it will be presented later in Section 37. The fourth paper [Gir06] is dedicated to a study of the feedback equation and its solutions [Sei12b, §4.2.6]. Finally, the fifth paper [Gir11b] will take into account an explicit consideration of the notion of *address* or *location*. Solutions of the feedback equation are extended with the notion of *determinant of a matrix* in which the execution formula appears under the assumption of invertibility of $1 - \sigma u$ [Sei12b, §4.2.7]. Shifts to new mathematical frameworks such as Type II Von Neumann algebras will also be considered in order to keep the interpretation of logic (especially exponentials) with a generalised notion of determinant (Fuglede-Kadison determinant). Philosophically speaking, the approach is novel and explicitly stated in the abstract of the fourth paper:

> the equation was essentially studied for those Hilbert space operators coming from actual logical proofs. In this paper, we take the opposite viewpoint, on the arguable basis that operator algebra is more primitive than logic: we study the general feedback equation of Geometry of Interaction”.

> - Jean-Yves Girard

In the abstract of the fifth paper, the claim is even stronger:
<figure><img src="image_72.png" /><figcaption>Figure 35.1: Proof-structure with labelled edges over an alphabet Σ of letters.</figcaption></figure>

> Geometry of Interaction (GoI) reacts against the absence of any satisfactory explanation for logic. The usual one is that of a symbolic calculus of truth values, which supposes that truth values pre-exist and formulas as well. [...] The aim of GoI is therefore to find a space where truth, commuting diagrams, etc. are no longer primitive and where dynamical processes (proof-search, rewriting, a.k.a. normalisation) are primitive.

> - Jean-Yves Girard

## 35 Danos and Regnier's algebra of paths for MLL

§35.1 Danos and Regnier suggested a very accessible reformulation of Girard's GoI in their paper "Proof-nets and the Hilbert space" [DR95]. This approach directly applies the novelties of the GoI to original proof-nets. We are, again, interested in characterising the paths in proof-nets but more especially the persistent paths which are preserved by cut-elimination. These paths are the essence of proof-nets. An algebra $L^*$ is defined to express weight on paths represented by words over $\{1, l, r, l^*, r^*\}$. If paths are not preserved, their corresponding weight will be cancelled. This is a simplified version of Girard's partial isometries $l$ and $r$.

### Paths in a proof-structure

§35.2 We consider proof-structures $(V, E, \text{in}, \text{out}, \ell_E)$ extended with a labelling of edges. Since we defined proof-structures as hypergraphs, we have to consider a bijective labelling $\ell_p : V \times E \to \Sigma$ where $\Sigma$ is a fixed alphabet of edge identifier. We write $\ell$ instead of $\ell_p$ when the labelling being used is obvious. An example of such labelled proof-structure is given in Figure 35.1.
§35.3 **Definition (Path).** Let $\mathcal{S}$ be a proof-structure extended with a labelling $\ell_p : V \times E \to \Sigma$ for some $\Sigma$. A *path* of $\mathcal{S}$ is a finite word over $(\Sigma \cup \Sigma^R)^*$ where $\Sigma^R := \{x^R | x \in \Sigma\}$. The symbol $a^R \in \Sigma^R$ represents the reverted edge associated with $a$. In particular, it defines an involution $(\cdot)^R$ such that $(a^R)^R = a$ and $(ab)^R = b^R a^R$.

If $p_i = a_1...a_n$ is a path then we must have that $a_k$ and $a_{k+1}$ are adjacent, i.e. if $\ell_p^{-1}(a_k) = (v, e)$ and $\ell_p^{-1}(a_{k+1}) = (v', e')$ then either $v = v'$ or $e = e'$.

§35.4 **Example.** An example of path from 1 to 6 in Figure 35.1 is $gkmn^Rj^Re^Rf$ (read from left to right).

§35.5 Danos and Regnier distinguished several classes of paths in order to represent good and ill-behaving paths [DR95, Section 2.2]. A path is

* non-bouncing if it does not contain $a^Ra$ for any $a$ (it does not retract his choice by going back in the previous point);

* non-twisting if it does not contain $a_1^Ra_2$ with $a_1$ and $a_2$ distinct premises of a same link (it does not go from one premise to another);

* straight if it is non-bouncing and non-twisting (the good paths we want).

§35.6 **Example.** The path $gkmn^Rj^Re^Rf$ of the previous example for the proof-structure in Figure 35.1 is straight. An example of bouncing path from 7 to 7 is $k^Rg^Rg$. An example of twisting path from 8 to 8 is $l^Ri^Rj$.

## Weight of a multiplicative path

§35.7 In this section, we associate weights with paths. These weights are words over

$$ \{1, l, r, l^*, r^*\} $$

specifying which are the direction taken in binary connectives. In particular, we would like to follow the rules of multiplicative cut-elimination: preserved paths are the one consistent with directions by going down left (respectively right), going through the cut, and going up left (respectively right) on the other side. We first define the algebraic language of those weights.

§35.8 **Definition (Involutive monoid $L^*$).** Let $L^*$ be the involutive monoid$^a$ generated by $\{1, r, 0\}$ and the following equations:

$$ 0x = x0 = 0 $$

$$ 1^*r = r^*1 = 0 $$

$$ 1^*1 = r^*r = 1 $$

<footnote>$^a$Monoid with a set $E$, an associative multiplication operator $\cdot$ with neutral element 1 and an involution $(\cdot)^*$ : $E \to E$ such that $x^{**} = x$, $0^* = 0$ and $(xy)^* = y^*x^*.$</footnote>
§35.9 **Definition (Regular path).** A path $\rho$ in a proof-structure $S$ is regular if and only if $\omega(\rho) \neq 0$ [DR95, Definition 4].

§35.10 Regular paths correspond to the paths which are not cancelled by the algebra of weight $L^*$, hence which are valid w.r.t. multiplicative cut-elimination. We now associate weights with paths.

§35.11 **Definition (Weight association).** Let $\rho = a_1...a_n$ be path in a proof-structure $S$. The weight $\omega(\rho)$ associated with $\rho$ is defined by $\omega(a_n)...\omega(a_1)$ where the weight $\omega(a)$ of a label $a$ such that $\ell_p^{-1}(a) = (v, e)$ is defined as follows:

• if $a \in \Sigma^R$, then $\omega(a) := \omega(a^R)^*$;

• if $v$ is the left premise of $e$ with $\ell_E(e) \in \{\otimes, \mathfrak{N}\}$, then $\omega(a) = 1$;

• if $v$ is the right premise of $e$ with $\ell_E(e) \in \{\otimes, \mathfrak{N}\}$, then $\omega(a) = r$;

• $\omega(a) = 1$ otherwise.

Notice that the path is reversed. This is because of a technical detail: the natural reading order for paths is from left to right but algebraic composition is read from right to left.

§35.12 **Example.** In the proof-structure of Figure 35.1, we have:

• an illegal straight path $c^R dilnm^R k^R h^R b^R a g k m n^R l^R j^R e^R f$ from 3 to 6, of weight

$$ \omega(\mathit{fe}^R j^R l^R n^R mkgab^R h^R k^R m^R nlidc^R) = \mathbf{r}^* \mathbf{l} \mathbf{r}^* \mathbf{l} = 00 = 0; $$

• a legal regular straight path $c^R dilnm^R k^R g^R a^R b h k m n^R l^R j^R e^R f$ from 3 to 6, of weight

$$ \omega(\mathit{fe}^R j^R l^R n^R m khba^R g^R k^R m^R nlidc^R) = \mathbf{r}^* \mathbf{l} \mathbf{r}^* \mathbf{l} = 11 = 1 \neq 0. $$

§35.13 **Definition (Execution formula).** The execution of a proof-structure $S$ is defined by

$$ \mathrm{Ex}(S) := \sum_{\rho \in \mathrm{Straight}(S)} \omega(\rho) $$

where Straight($S$) are the straight paths from conclusion to conclusion (hence maximal paths). This assumes that we have a disjoint union + extending our algebra of weights.

§35.14 **Example.** Let $S$ be the proof-structure in Figure 35.1. We have $\mathrm{Ex}(S) = 1 + 1$ (two valid paths).

§35.15 As shown in Danos and Regnier's paper, the execution computes all straight and persistent (equivalently, regular) paths which are the paths preserved by cut-elimination.
<figure><img src="image_73.png" /><figcaption>Figure 35.2: Valid path (traversing the $\mathcal{Y}$ link) erased during cut-elimination for MELL proof-structures.</figcaption></figure>

**§35.16 Theorem.** Let $\rho \in \text{Straight}(\mathcal{S})$ for a proof-structure $\mathcal{S}$. We have that $\rho$ is regular if and only if $\rho$ is persistent (not formally defined here).

*Proof.* Proven in Danos and Regnier's paper [DR95, Theorem 14]. □

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

**§35.17 The case of exponentials.** The difficult is to treat the behaviour of paths for boxes and structural rules. It has been investigated by Danos and Regnier [DR95] but I believe that it is better understood from the point of view of the *token machine* (also called *Interactive Abstract Machine* or *IAM*) [Lau01]. I only sketch the basic idea and do no develop more. We consider generalised ?-links as in Figure 29.14.

* Paths ending with a weakening link are not considered by the execution which only keeps paths from conclusion to conclusion.

* The only thing we require from dereliction links is that if go out of it from the top through a cut, we have to go to a box. And conversely, if we entering it from the bottom, we have to be coming from a box. We have to keep an information telling whether we are in an exponential path.

* Since boxes can be duplicated, we have to be able to tell which box we are talking about. In particular, depending on whether we are coming from the left or right premise of a contraction link, we are speaking about two distinct copies of a same box. A way to do that is to lift edge labels $a$ into a tensor $1 \otimes a$ (as in Girard's algebraic GoI). Then we can compose $1 \otimes a$ by $k \otimes 1$ to get $k \otimes a$ with $k \in \{\mathbf{l}, \mathbf{r}\}$ telling that we are either speaking about the left or right copy of a potential box. We have imbricate boxes by tensoring again: $1 \otimes a \mapsto 1 \otimes (1 \otimes a)$.

**§35.18 No exact preservation of exponential paths.** I expose a little problem regarding the GoI in the context of exponentials<fnref n="9" />. The GoI studies cut-elimination only by considering set of paths to characterise proofs. However, in proof-net theory (which tries

<footnote n="9">⁹I thank Olivier Laurent who told me about this.</footnote>
to mimic sequent calculus), some paths are valid but not preserved by cut-elimination.
There are three sort of exponential paths:

1. the ones entering the box by the ! link and going out through it. These paths are preserved and there are not problems about it;

2. the ones entering the box the ! link but go out through an auxiliary door (the context ?Γ of an exponential box). In this case<fnref n="10" />, paths are preserved in an alternative presentation of exponentials replacing the promotion rule by two rules: digging and functorial promotion (cf. Paragraph 27.21);

3. the most problematic paths are the one entering a box by an auxiliary door and going out from an auxiliary door. If the box containing this path interacts with a weakening, the path is erased even though it did not directly interact with the weakening and was valid. This is a collateral damage illustrated in Figure 35.2. The problem is that the GoI does not see that and it will appear in the result of the execution. In the other cases (dereliction and contraction) there should not be any problem.

This shows that the GoI is unable to exactly capture the behaviour of proof-nets only by considering paths. For that reason, approaches based on GoI often forbid ?A formula in the conclusion of a sequent since they may correspond to formulas going out of a box without passing through a ! link. It is also possible to simply exclude weakening links. But this is not necessarily a problem since these *junk residuals* can simply be ignored. Another solution is to shift to the paradigm of *intuitionistic game semantics* where sequents Γ ⊢ A has a distinguished output. This limits the space of path and it is then impossible to enter and exit by an auxiliary door for the same path.

**36 Token machine for the geometry of interaction**

§36.1 Studying cut-elimination only from the exploration of paths in a proof-structure has for consequence that the graph rewriting of proof-structure is not necessary: the execution of proofs and programs can be done by a process of exploration of a structure. In particular, it is possible to reduce λ-terms without syntactic transformation. Actual duplication is not necessary as well. This suggests ideas of sharing used in optimal reduction for λ-calculus (cf. Paragraph 29.29). The GoI also constitutes a tool for the study of dynamical processes occurring in logic.

§36.2 Since typed λ-terms can be encoded with proof-nets (and untyped λ-terms by proof-structures), it is possible to provide an execution of λ-terms by a computation of paths in the corresponding structure [AL95, DR99]. In order to make it implementable and

<footnote n="10">¹⁰According to a discussion I had with Olivier Laurent.</footnote>
<figure><img src="image_75.png" /><figcaption>Figure 36.1: Transition rules of the IAM for MLL. For each transition $c \rightsquigarrow_x c'$, the reverse transition $c' \rightsquigarrow_x^{-1} c$ is valid as well with reversed directions for $c$ and $c'$. The binary link $\odot$ corresponds to either $\mathfrak{R}$ or $\otimes$.</figcaption></figure>

closer to computer science, this execution is usually defined by a *token machine*<fnref n="11" /> which is a machine exploring a proof-structure and collection information during its travel [Lau01]. This machine is often called *Interaction Abstract Machine* (IAM). I describe the IAM for the multiplicative case.

**§36.3** Let $\mathcal{S} = (V, E, \text{in}, \text{out}, \ell_E)$ be a proof-structure. A *configuration* is a tuple $(d, v, \pi)$ where $d \in \{\bar{\Lambda}, \underline{\Lambda}\}$ is the direction of the current state, $v \in V$ the current vertex the machine is reading and $\pi$ is a stack defined by the grammar $\pi ::= \emptyset | \mathbf{1} \cdot \pi | \mathbf{r} \cdot \pi$. A configuration is *initial* when it is $(\bar{\Lambda}, x, \emptyset)$ where $x \in V$ is a conclusion of $\mathcal{S}$. It is *final* when it is $(\underline{\Lambda}, x, \emptyset)$ where $x \in V$ is a conclusion of $\mathcal{S}$. The IAM is defined by reversible transition rules between configurations given in Figure 36.1. Directions can be reversed with an involutive operation $(\cdot)^R$ such that $\bar{\Lambda}^R = \underline{\Lambda}$ and $\underline{\Lambda}^R = \bar{\Lambda}$. For each transition $(d, v, \pi) \rightsquigarrow_x (d', v', \pi')$, there is an additional reverse transition $(d'^R, v', \pi') \rightsquigarrow_x^{-1} (d^R, v, \pi)$. A *run* is

<footnote n="11">¹¹This use of the GoI is so famous that if you mention the GoI, a lot of people (if not most) who heard about it will say something like “Oh you’re talking about the token machine?”. I think it is not exaggerated to say that this application replaced Girard’s original definitions and motivations.</footnote>
<figure><img src="image_76.png" /><figcaption>Figure 36.2: Example of run from 3 to 6 with the IAM.</figcaption></figure>

a sequence of transitions from an initial to a final one. We write $\rightsquigarrow$ for $\rightsquigarrow ax \cup \rightsquigarrow cut$
$\cup \rightsquigarrow l_1 \cup \rightsquigarrow r_1 \cup \rightsquigarrow \overline{ax} \cup \rightsquigarrow \overline{cut} \cup \rightsquigarrow \overline{l_1} \cup \rightsquigarrow \overline{r_1}$ and $\rightsquigarrow^*$ for the reflexive transitive closure of $\rightsquigarrow$.

The rules for binary connectives presented push symbols and reverse rules pop symbols.
The idea is that the combination of push and pop will cancel $l^*l$ and $r^*r$ so to reproduce
the algebra $L^*$. An example of run is given in Figure 36.2.

§36.4 Machine for exponentials. A machine for full linear logic can be found in Olivier Laurent's works [Lau01]. The idea of exponentials is that we add transitions for boxes, auxiliary doors and structural rules. During transitions, we have to keep the exponential box (relatively to boxes) we are in and an identifier of copy so that we speak about the right copy of a box. To give a simplified and incomplete idea of Laurent's IAM, we can add two stacks $\delta$ for the exponential depth and $\sigma$ for exponential information. We have two injections $left: N \to N$ and $right: N \to N$ such that $img(left) \cap img(right) = \emptyset$.

* If we go down on a dereliction, we have $(\sim, x, \pi, \delta, \sigma) \rightsquigarrow (\vee, x', \pi, \delta, 0 \cdot \sigma)$. We add a special symbol $0$ to specify that we are in an exponential path and expecting a box. The reverse transition pop the symbol because we have finished to explore a box and the machine exit the exponential zone created by the dereliction.

* A path ending on a weakening link will never be valid as it will never reach a final configuration.

* If we go down on the left premise of a contraction, we have $(\sim, x, \pi, \delta, i \cdot \sigma) \rightsquigarrow (\sim, x', \pi, \delta, \mathit{left}(i) \cdot \sigma)$. We have a symbol $i$ meaning that we are in an exponential path and we split the index $i$ to say that we are targetting the left copy of a potential box.

* If it the same for the right premise: $(\sim, x, \pi, \delta, i \cdot \sigma) \rightsquigarrow (\sim, x', \pi, \delta, \mathit{right}(i) \cdot \sigma)$.
• If we enter a box from the bottom of a ! link, we have $(\bar{\lambda}, x, \pi, \delta, i \cdot \sigma) \rightsquigarrow (\bar{\lambda}, x', \pi, i \cdot \delta, \sigma)$ meaning that we have an exponential identifier that we push on $\delta$ to say that we enter a box (are that the machine enters in the next depth).

• If we go out of a box but through an auxiliary door and not through the ! link of the box, we have $(\underline{\lambda}, x, \pi, i \cdot \delta, j \cdot \sigma) \rightsquigarrow (\bar{\lambda}, x', \pi, \delta, \#(i,j) \cdot \sigma)$ where $\#(i,j) \in \mathbb{N}$ is an encoding of the pair $(i,j)$ as a natural number (as in Paragraph 16.9). We remove a depth (because we exit a box) but change the “signature” of the exponential path by saying that we are in an exponential path identifier by the box $i$ and the exponential path $j$.

§36.5 **Machine for lambda-terms.** Although $\lambda$-terms can be encoded as proof-structures, their translation always have a specific shape. It is possible to directly define a machine for $\lambda$-terms with more synthetic transitions. In particular, a transition for $\lambda$-terms corresponds to several transitions of the IAM. Such machines work by distinguishing a context and a part of the term which is read. And the syntax tree of the term is explored. It is possible to find definitions of that in Mazza's HdR thesis [Maz17, Section 3.3.4] (machine itself inspired by some notes of Accattoli and Dal Lago, according to Mazza).

§36.6 **Space-efficient computation.** Schöpp designed a type system capturing computation in logarithmic space, together with a related realisability interpretation inspired by the GoI [Sch06]. The idea later reappeared in the context of functional programming for sub-linear space with Dal Lago and Schöpp [LS10]. Using the GoI for $\lambda$-calculus has the particularity of executing by analysis of a static structure (the structure of the term). This seems space-efficient but the complexity is hidden in how the machine is treated (in particular, the data accumulated in stacks).

## 37 Alternative approaches

§37.1 We have already seen that there are several ways to approach the ideas proposed by the GoI. With operator algebras, with persistent paths of a proof-structure or with an abstract machine exploring a proof-structure. In this section I present notable alternative to these ideas. I present reformulations of the GoI with their own formalisms and problems but also related but not directly connected topics such as ludics.

### Flows and wirings

§37.2 In his third paper about GoI, Girard propose a new presentation of his algebraic GoI by using ideas coming from term unification logic programming (cf. Section 23):
> Geometry of interaction is most naturally handled by means of $C^*$-algebras; this yields surely more elegant proofs, but it obscures the concrete interpretation. So we prefer to follow a down to earth description of the interpretation. An unexpected feature will help us : the $C^*$-algebras used can in fact be interpreted in terms of logic programming, since the basic operators are very elementary PROLOG programs, and composition is resolution!

> - Jean-Yves Girard [Gir95, Section 1.8]

Hence, he remarked that what he was doing with operator algebra only used a small portion of the power of operator algebra. The interpretation of logic could equivalently be done with mechanisms of term unification similar to the ones of logic programming.

**§37.3 Dialects (idioms).** A novelty of this third paper is that Girard tries to extend his interpretation to MALL with what he calls *dialects* [Gir95, Section 1.6] (later renamed *idiom*). The idea is, similarly to the interpretation of exponentials, operators of a Hilbert space $\mathbb{H}$ are extended with an additional space of information $\mathbb{H} \otimes \mathbb{H}'$ where $\mathbb{H}'$ is a *dialect*, meant to be private. This is inspired by Girard's communication without understanding (cf. Paragraph 33.33) where logical entities have their own internal and private language. Technically speaking, the point is that we would like to superpose a proof of $\vdash \Gamma, A$ and a proof of $\vdash \Gamma, B$ to obtain a proof of $\vdash \Gamma, A \& B$. This is done by linking the two occurrences of proofs of $\vdash \Gamma$ to, a dialect associated with $A$ and a dialect associated with $B$ respectively. In case we have a proof of $\vdash A \oplus B$ coming from a proof of $\vdash A$, the proof of $\vdash \Gamma$ associated with $A$ will react correctly to it but the interaction fails for the other.

**§37.4** Apart from this interpretation of MALL that I do not detail, this third paper allows the study of the GoI only from term unification by interpreting links by *flows* and proof-structures by *wirings*. These notions have been developed by Bagnol [Bag14] and Aubert [AB14, AS16b, AS16a]. Since it will be useful for the understanding of the rest of this thesis, I formally introduce these new objects. I refer to the chapter on logic programming for basic definitions about term unification (cf. Section 23). We fix a signature $\mathcal{S}$ for terms.

**§37.5 Definition (Flow).** A *flow* $f$ is a pair of terms $(t, u)$, written $t \leftarrow u$, such that $\mathit{varst} = \mathit{varsu}$ (there exists relaxation with $\mathit{varst} \subseteq \mathit{varsu}$).

It is possible to compose two flows $t \leftarrow u$ and $v \leftarrow w$ by a product using term unification:

$$ (t \leftarrow u)(v \leftarrow w) := \theta\alpha t \leftarrow \theta w $$

where $\theta = \mathbf{solution}\{\alpha u \stackrel{?}{=} v\}$ for a renaming $\alpha$ such that $\mathit{vars}\alpha u \cap \mathit{vars}v = \emptyset$. The requirement of the renaming makes the two flows' variables independent: their variables are bound the flow they are in. We write $f \approx_{\alpha} g$ for two flows equivalent up
to renaming.

§37.6 **Example.** $(X \leftarrow f(X))(f(g(X)) \leftarrow X) \approx_{\alpha} (X \leftarrow f(X))(f(g(X')) \leftarrow X') = \theta X \leftarrow \theta X' = g(X') \leftarrow X'$ with the most general unifier $\theta = \{X \mapsto g(X')\}$.

§37.7 **Definition (Wiring).** A wiring $F$ is a set (or multiset or formal sum depending on the definitions) of flows.

The product of two wirings $F$ and $G$ is defined by:

$$FG := \bigcup_{f \in F, g \in G} \{fg \text{ when it is defined}\}.$$

We distinguish an absorbing wiring 0 such that $0F = F0 = 0$ for any wiring 0. The identity wiring $1_F$ is the set of flows $t \leftarrow t$ for all terms $t$ appearing in $F$.

§37.8 Flows represent the directed flow of information, as in Girard's long trips. The idea of the interpretation in modern presentation<fnref n="12" /> is that an atom $v$ of a proof-structure is represented as a term $v(X)$. For instance, an axiom between $u$ and $v$ becomes the wiring $\{u(X) \leftarrow v(X), v(X) \leftarrow u(X)\}$. We will write such two-way flows as a single expression $u(X) \iff v(X) := \{u(X) \leftarrow v(X), v(X) \leftarrow u(X)\}$. A product $(u(X) \iff v(X))(u'(X) \iff v'(X))$ then corresponds to a composition of path. Switching flow graphs can be represented as well and it is then possible to formulate Girard's correctness criterion.

§37.9 The variable $X$ is not necessary for MLL (we could simply work with constants) but it is useful for extensions to exponentials. The idea is that if we have a term $u(X)$ then it can be split into two terms $u(l(X))$ and $u(r(X))$. This corresponds to a use of contraction rule for atoms. If something wants to match terms of form $u(t)$, for instance some $v(t')$ through a cut $v(X) \iff u(X)$, then it has to be used in order to match both $u(l(X))$ and $u(r(X))$.

§37.10 Let $F$ be the wiring associated with the test of switching $\phi$, and $G$ be the wiring associated with the axioms of $S$. We have that $S$ is correct w.r.t. long trips if there exists a $k \in \mathbb{N}$ such that $(GF)^k = 1_{FG}$ (which corresponds to the condition of cyclicity).

§37.11 **Definition (Execution of a wiring).** A wiring $F$ interacting with a wiring $G$ can be executed with an execution formula:

$$\mathbf{Ex}(F, G) := (1 - G^2)F \sum_{k=0}^{\infty} GF(1 - G^2)$$

<footnote n="12">¹²Which has actually never been clearly written but since the idea is used in transcendental syntax (which has a very similar interpretation), we will explain it directly in the next chapters instead of developing the interpretation with flows. References about flows can be found in Bagnol or Baillot's works [Bag14, BP99].</footnote>
where $(1 - G^2)$ is the usual filtering of Paragraph 34.7 which has to be defined (this
could be done by an algebraic way exactly as in Paragraph 34.7).

**§37.12 Unary Horn clauses.** The link with logic programs comes from the fact that a flow $t \leftarrow u$ may be seen as a Horn clause $P(t) \vdash P(u)$ for a superficial predicate $P$ wrapping all terms of flows. The resolution rule (which can be seen as a cut-rule) connects the output of one clause to the input of another one. From $P(t) \vdash P(u)$ and $P(v) \vdash P(w)$, we get $P(\theta t) \vdash P(\theta w)$ where $\theta = \text{solution}\{\alpha u \stackrel{?}{=} v\}$. This is exactly the composition of flows. A whole program (set of clauses) then becomes a wiring. The execution formula corresponds to inferring all possible clauses from a given set of clauses, similarly to how we compute the answers of a query in logic programming.

Seiller's interaction graphs

**§37.13** Permutations over natural numbers can be represented by graphs. If we take this analogy seriously, then we can actually define the GoI by using interactive graphs which are connected along identical addresses. These graphs, introduced by Seiller [Sei16b] are a very convenient way to present the GoI on which various notions of graph theory can be applied. In particular, the execution is simply a computation of maximal alternating paths.

**§37.14** For instance, we present the permutations of Figure 33.1a as a plugging between inter-action graphs in Figure 37.1. We can then compute all maximal paths. All the ideas of GoI will then be about analysis and extension of these interactive graphs.

**§37.15 Definition (Graph plugging).** Let $G = (V, E_G)$ and $H = (V', E_H)$ be two graphs. Their *plugging* is defined by a graph $G \square H = (V \cup V', E_G \uplus E_H)$ and a colouring function $\delta : E_G \uplus E_H \to \{0, 1\}$ such that $\delta(e) = 0$ when $e \in E_G$ and $\delta(e) = 1$ when $e \in E_H$. This makes the edges of $E_G$ distinct from the edges of $E_H$.

**§37.16 Definition (Alternating paths).** Let $G = (V, E)$ be a graph. An *alternating path* in $G$ is a sequence of edges $(e_i)_{0 \le i \le n}$ for some $n$ such that $\delta(e_i) \ne \delta(e_{i+1})$ for $0 \le i \le n-1$.

**§37.17 Weighted interaction graphs.** Given a graph $G = (V, E)$, it is possible to add weights to edges with a function $\omega : E \to \Omega$ where $\Omega$ is a monoid of weights with multiplication $\cdot$ and neutral element $\varepsilon$. The weight $\omega(\rho)$ of a path $\rho = (e_1, \dots, e_n)$ in $G$ is then given by $e_1 \cdot \dots \cdot e_n$. By using these weights, we can analyse interaction graphs in a finer way. What we are interested in is weight of cycles which can help us recover the long trip criterion or various other orthogonality relations in a very generic way. Seiller defines the *quantification of cycles* between two graphs $F$ and $G$ as a function $[[F, G]] := \sum_{\rho \in \text{Cycles}(F, G)} m(\omega(\rho))$ for a function $m : \Omega \to \mathbf{R}^+ \cup \{\infty\}$. We then have to choose a wise weighting function and a function $m$ to have the interpretation we want. Notice that converging and diverging cycles are distinguished.
<figure><img src="image_77.png" /><figcaption>Figure 37.1: Connexion of interaction graphs and their execution.</figcaption></figure>
§37.18 **Interpretation of MLL proofs.** Proofs are interpreted by projects **a** = (a, A) where
a ∈ R+ is the wager, that is a primitive weight associated with the project and A is a
weighted graph (representing the proof-structure). We can then measure the interaction
between two projects **a** = (a, A) and **b** = (b, B) with ⟨**a**, **b**⟩ := a + b + ⟨[A, B]⟩. Seiller
defines his orthogonality relation as **a** ⊥ **b** when ⟨**a**, **b**⟩ ∉ {0, ∞}. Then the usual
definition of types inspired by classical realisability can be done.

§37.19 **Genericity of interaction graphs.** The theory of interaction graphs has the advantage to be able to express various orthogonality relations (hence correctness criteria) in a same framework by using generic tools such as quantification of cycles and measure of interaction.

* By choosing $m(x) = \infty$ in the quantification of cycles, one obtains orthogonality by nilpotency;

* By choosing $m(x) = -\log(1-x)$ one obtains Girard's orthogonality relation based on determinants.

Seiller is also able to express a property called *trefoil property* [Sei16a, Section 2.2]
which generalises the adjunction property. This property guarantees that we have a
sound model of MLL. Categorical interpretations with *-autonomous categories can be
constructed as well [Sei12a, Section 3].

§37.20 **Graphings.** Seiller later generalised interaction graphs to *graphings* [Sei17]. Graphings generalise both usual finite graphs for MLL and Girard's use of operator algebras for full linear logic. Instead of directed edges between vertices (points), we have (measurable) maps over subsets of some (measure) space. This makes plugging more complex but give a very general framework to speak about cycles and paths. Graphings are expressive enough to naturally define various models of computation such as automata and Turing machines [Sei18] by actions over spaces of states or configurations.

**Proofs as partitions of a set**

§37.21 Permutations are very convenient if we consider the long trips criterion but it is not natural for Danos-Regnier correctness which focus on the undirected structure of correctness and not its directed flows of information. An alternative to permutations using *partitions of a set* has been mentioned by Danos and Regnier [DR89] and later been developed by Acclavio and Maieli [AM20, MP05]. Partitions are able to naturally represent Danos-Regnier correctness hypergraphs.

§37.22 **Definition (Partition).** Let $X = \{1, ..., n\}$ be a finite sequence of natural numbers. A *partition* $P$ over $X$ is a set of sets $P = \{E_1, ..., E_k\}$ such that for $1 \le i \le k$, $E_i \subseteq X$ and:

• $\emptyset \notin P$;
<figure><img src="image_78.png" /></figure>

<figure><img src="image_79.png" /><figcaption>Figure 37.2: Example of partitions associated with Danos-Regnier tests. The first correctness hypergraph corresponds to the partition $\{{\{1, 2, r_5\}, \{3, r_6\}, \{4\}\}}, \{\{1, 2, r_5\}, \{3\}, \{4, r_6\}\}}$ and the second to $\{\{1, 2, r_5\}, \{3\}, \{4, r_6\}\}$.</figcaption></figure>

• all sets are disjoints, i.e. for all $i \neq j$, $E_i \cap E_j = \emptyset$;

• the reunion of all sets constitutes $X$, i.e. $\bigcup_{E \in P} E = X$.

§37.23 For instance, if we have $X = \{1, 2, 3, 4\}$, then some partitions of $X$ are $\{{\{1, 2, 3, 4\}\}}, \{{\{1, 2\}, \{3, 4\}\}}$ and $\{{\{1, 2\}, \{3\}, \{4\}\}}$. You can think of it as cutting a cake representing $X$ as you wish. You can make bigger slices if you want.

§37.24 **Interpretation of vehicles.** Vehicles are symmetric permutations over two natural numbers. They can be represented by partitions of binary set over a set of atoms $X$ (notice that the direction is irrelevant for axioms). For instance, the two vehicles of Figure 33.1 are both represented by $\{{\{1, 4\}}, \{2, 3\}\}$. As for the vehicle of Figure 35.1, it is represented by the partition $\{{\{1, 2\}, \{3, 4\}, \{5, 6\}\}}$.

• Not any partition corresponds to a permutation: the partition $\{{\{1, 2, 3\}, \{4\}, \{5\}\}}$ cannot be represented by a permutation;

• Conversely, it is possible to construct permutations such as $\begin{bmatrix} 1 & 2 & 3 \\ 2 & 3 & 1 \end{bmatrix}$ which cannot be represented by partitions.

The approaches are then concurrent and non-equivalent.

§37.25 **Interpretation of tests.** I use a variant of Acclavio and Maieli's pointed partitions [AM20, Definition 30] (sketched by Girard [Gir16b, Appendix A.1]) which I find more convenient to explain notions which will appear later in this thesis. A correctness hypergraph can be seen as a way to create a partition of the set of atoms. Tensor links will reunite atoms with $\otimes$ and the two switchings for $\mathcal{Y}$ are two different ways to separate atoms. Tests then induce several connected components. The partition associated with a test $S^\varphi$ of switching $\varphi$ is given by $P_\varphi := \{E_1, ..., E_k\}$ where $E_1, ..., E_k$ are uniquely associated with connected components $C_1, ..., C_k$ of $S^\varphi$ and $e \in E_i$ when $e$ is an atom in $C_i$. Moreover, each $E_i$ is extended with a special value $r_j$ for all conclusion $j$ appearing in $C_i$. Examples of partitions for Danos-Regnier tests are given in Figure 37.2. The additional values $r_j$ are called *roots* and they guarantee that we faithfully represent correctness hypergraphs by specifying where conclusions are located.
<figure><img src="image_80.png" /><figcaption>Figure 37.3: Example of connexions of partitions corresponding to correctness hypergraphs.</figcaption></figure>

<figure><img src="image_81.png" /><figcaption>Figure 37.4: Example of tests for a non-sequentialisable MLL formula.</figcaption></figure>

§37.26 It is possible to recover full correctness hypergraphs by connecting a vehicle with a test. Since vehicles and tests are independent entities in the GoI, we must patch things together by constructing a graph with edges linking identical atoms. If we connect the two tests of Figure 37.2 together with a same vehicle {{1,3}, {2,4}}, then we obtain the two connexions of partitions illustrated in Figure 37.3a.

§37.27 **Definition (Connexion of partitions)**. The *connexion* of two partitions P and Q of a same set X ⊆ N is defined by a graph G(P, Q) = (P ⊕ Q, E) where vertices are the sets of P and Q, and there is an edge between E_P ∈ P and E_Q ∈ Q for each elements of E_P ∩ E_Q.

§37.28 **Definition (Orthogonality)**. We say that two partitions P and Q are *orthogonal*, written $P \perp Q$, when $G(P, Q)$ is a tree containing all roots (or a forest if we are interested in MLL+MIX correctness).

§37.29 The fact that graphs of Figure 37.3a are trees means that the vehicle {{1,3}, {2,4}} passes the two tests and can be typed with a sequent $\vdash A^{\perp} \mathcal{Y} B^{\perp}, A \otimes B$ (from which the tests can be deduced). However, if we plug the tests to another vehicle such that {{1,2}, {3,4}} as in Figure 37.3b, then we obtain two connected component and a cycle. It means that the vehicle does not pass the tests.

§37.30 **Interpretation of types.** Types are constructed as in the GoI with permutations (cf. Section 33) except that we translate Danos-Regnier correctness hypergraphs instead of
$$ \frac{\begin{array}{ccc} \vdash X_1 & \vdash X_2, X_3 & \mathfrak{r} \\ \vdash X_1 \otimes X_2, X_3 & \mathfrak{r} & \rightsquigarrow \\ \vdash (X_1 \otimes X_2) \mathfrak{r} X_3 & \mathfrak{r} & \end{array}}{\begin{array}{ccc} \vdash X_1 & \vdash X_2, X_3 & R_1 \\ \vdash X_1 \otimes X_2, X_3 & \mathfrak{r} & \end{array}} $$

$$ \frac{\begin{array}{ccc} \vdash X_1, X_3 & \vdash X_2 & \mathfrak{r} \\ \vdash X_1 \otimes X_2, X_3 & \mathfrak{r} & \end{array}}{\begin{array}{ccc} \vdash (X_1 \otimes X_2) \mathfrak{r} X_3 & \mathfrak{r} & \end{array}} \rightsquigarrow \frac{\begin{array}{ccc} \vdash X_1, X_3 & \vdash X_2 & R_2 \\ \vdash (X_1 \otimes X_2) \mathfrak{r} X_3 & \mathfrak{r} & \end{array}}{\begin{array}{ccc} \vdash F(X_1, X_2, X_3) & \mathfrak{r} & \end{array}} $$

Figure 37.5: Generalised rules corresponding to two ways for splitting atoms from $\vdash$ ($X_1 \otimes X_2$) $\mathfrak{r}$ $X_3$ for the generalised connective $F$.

Girard's switching flow graphs. As in Paragraph 33.30, it is also possible to construct generalisations of MLL formulas. An example proposed by Acclavio and Maieli (which initially comes from Girard and which has been reformulated by Danos and Regnier) is the following set of partitions (we omit roots but it does not matter):

$$ G := \{\{1, 3\}, \{2\}, \{4\}\} \text{ and } \{\{2, 4\}, \{1\}, \{3\}\} $$

which is a set of tests that cannot be expressed by $\mathfrak{r}$ and $\otimes$. It can be seen as taking the two tests of Figure 37.4 which is *hybrid* and cannot come from the same proof-structure. However, they *do* yields an orthogonal:

$$ \{\{1, 2\}, \{3, 4\}\} \text{ and } \{\{2, 3\}, \{4, 1\}\} = G^{\perp} $$

which can be considered as vehicles of type $G$.

**§37.31 Interpretation of connectives.** It is possible to directly interpret *connectives* instead of formulas [Gir87b, Section 3]. It could have been defined with permutations but I find it more explicit with partitions. A *multiplicative connective* is defined by a parametrised expression $F(1, ..., n)$ where $1, ..., n$ represent occurrences of atoms (in natural order from left to right). Connectives are seen as collections of ways to *split* occurrences of atoms. Each splitting yields a generalised rule for that connective as illustrated in Figure 37.5. These generalised rules naturally yield partitions by how they split atoms. In Figure 37.5, the rule $R_1$ yields $\{\{1\}, \{2, 3\}\}$ and the rule $R_2$ yields $\{\{1, 2\}, \{3\}\}$. Connectives (including non-sequentialisable ones) are then associated with set of partitions (hence pre-behaviours). In particular, the two usual binary connectives $\mathfrak{r}$ and $\otimes$ are orthogonal special cases: $\mathfrak{r}(1, 2) := \{\{\{1, 2\}\}\}$ and $\otimes(1, 2) := \{\{\{1\}, \{2\}\}\}$, which correspond to reuniting and separating atoms.

**§37.32 Cut-elimination.** As far as I know, cut-elimination has never been expressed directly on partitions but it is possible to represent cuts exactly as for axioms. Examples of vehicles $P$ (top) and cuts $Q$ (bottom) interacting are given in Figure 37.6. Cut-elimination is defined as a graph rewriting procedure starting from $G(P, Q)$ which contracts edges
<figure><img src="image_82.png" /><figcaption>Figure 37.6: Example of cuts interacting with vehicles.</figcaption></figure>

$$ \frac{A_{[k,1]} \vdash \Delta_1 \quad \dots \quad A_{[k,n_k]} \vdash \Delta_{[n_k]}}{\vdash (A_{[1,1]}^{\perp} \otimes \dots \otimes A_{[1,n_1]}^{\perp}) \oplus \dots \oplus (A_{[m,1]}^{\perp} \otimes \dots \otimes A_{[m,n_m]}^{\perp}), \Delta} (+,k) \\ \frac{A_{[1,1]}, \dots, A_{[1,n_1]} \vdash \Delta \quad \dots \quad A_{[m,1]}, \dots, A_{[m,n_m]} \vdash \Delta}{(A_{[1,1]}^{\perp} \otimes \dots \otimes A_{[1,n_1]}^{\perp}) \oplus \dots \oplus (A_{[m,1]}^{\perp} \otimes \dots \otimes A_{[m,n_m]}^{\perp}) \vdash \Delta} (-) $$

Figure 37.7: Synthetic rules for linear logic. The use of negation ensures that we alternate between positive and negative formulas. For the positive rule (+,k), in a bottom-up reading, we choose the k-th tensor of formulas (with $1 \le k \le m$) and split it. We have $\Delta = \Delta_1 \uplus \dots \uplus \Delta_{n_k}$. For the negative rule (-), (which corresponds to a sequence of & over clauses of $\mathcal{N}$ but on the left), from a bottom-up reading, all sequences of tensors of formulas are proven independently with a shared context $\Delta$ and all formulas of these sequences are put into the same space of interaction.

and remove the associated values in the two connected sets. However, it is not very easy nor interesting to define, so I omit the formal definition. In Girard's transcendental, a more convenient model extending partitions will be defined with a formal definition of cut-elimination.

## Ludics

§37.33 Ludics has been imagined by Girard during his project of GoI in a the two-part paper “The meaning of logical rules” [Gir99, Gir00]. It has then been clearly defined in his paper “Locus Solum” [Gir01]. To quote Seiller [Sei12b, §4.2.1], if the GoI is seen as an abstraction of proof-nets removing as many superfluous details as possible, then ludics is the same but starting directly from sequent calculus instead. I choose to briefly present ludics because I find it interesting by itself and because it actually inspired Girard for his fifth paper on GoI where the notion of location takes an important role. It also contributed to the philosophy of the GoI and Girard’s transcendental syntax which came after. For more details, an introduction to both linear logic and ludics has been proposed by Curien in two parts [Cur05a, Cur05b].

§37.34 **Focalisation.** Ludics is related to the idea of logic-as-game (cf. Paragraph 28.3). A sequent calculus proof is seen as a sequence of moves between two opponents and only one wins. It sounds fine except that the two players are not very explicit. Starting
$$ \vdash_{\Gamma} \mathbf{\mathfrak{A}} \quad \frac{\dots \quad \xi.i \vdash \Delta_i \quad \dots}{\vdash \Delta, \xi} (+, \xi, I) \quad \frac{\dots \quad \xi.I \vdash \Delta_I \quad \dots}{\xi \vdash \Delta} (-, \xi, \mathfrak{R}) $$

<caption>Figure 37.8: Rules of ludics. We have $i \in I$ a set of indexes, $I \in \mathfrak{R}$ and $\Delta_I \subseteq \Delta$. The symbol $\xi$ represents the subject of the rule (which will be splitted into sublocations).</caption>

$$ \frac{\xi.1 \vdash \alpha \quad \xi.2 \vdash \beta}{\vdash \xi, \alpha, \beta, \gamma} (+, \xi, \{1, 2\}) \qquad \frac{\xi.\{1, 2\} \vdash \alpha, \beta \quad \xi.\{1, 3\} \vdash \alpha}{\xi \vdash \alpha, \beta, \gamma} (-, \xi, \{{1, 2}\}, \{1, 3\}) \\ \frac{\overline{\vdash \xi.2\{1, 2\}} (+, \xi.2\{1, 2\}, \emptyset) \quad \overline{\vdash \xi.2\{3\}, \alpha} \mathbf{\mathfrak{A}} \quad \overline{\vdash \xi.3\{7\}} (-, \xi.2, \{{1, 2}\}, \{3\})}{\underline{\underline{\xi.2 \vdash \alpha}}} \quad \frac{\overline{\vdash \xi.3 \vdash} (-, \xi.3, \{{7}\})}{\underline{\underline{\xi.3 \vdash}} (+, \xi, \{2, 3\})} \quad \overline{\mathbf{\mathfrak{A}}} $$

<caption>Figure 37.9: Example of application of rules in ludics. In the application of $(+, \xi, \{1, 2\})$ and $(-, \xi, \{{1, 2}\}, \{1, 3\})$, notice that the distribution of context is free. It is possible to simulate a weakening by providing a partial set of addresses for the positive rule so that we run out of addresses and are not being able to place every formula in a branch. As for the negative rule, it happens because all contexts of branches $\Delta_I$ must be included in $\Delta$ but they do not have to be disjoint. So it is possible to forget some locations such as $\gamma$. As for the last example, notice that we run out of addresses in the application of $(+, \xi.2\{1, 2\}, \emptyset)$.</caption>

from linear logic, we have already seen that connectives could be divided into positive (irreversible) and negative (reversible) connectives such that proving can be seen as applying all negative rules then positive rules. This idea initially comes from Andreoli [And92]. A proof is said to be *focalised* when it is an alternation between sequences of only positive or only negative rules. This yields a logical system called *hypersequentialised sequent calculus* [And92, Gir99]. The two players are therefore represented by positive and negative application of rules.

**§37.35 Synthetic rules.** In ludics, we consider synthetic rules (that I present in a bilateral fashion): one positive rule generalising $\otimes$ and $\oplus$ and one negative rule generalising $\mathfrak{R}$ and $\&$ (cf. Figure 37.7). Starting from that, ludics try to abstract from all the logical content to obtain interaction between alogical entities (exactly like proof-structures, permutations or partitions). We could use a monolateral definition of synthetic rules with $\mathfrak{R}$ and $\&$ for the negative rule but it would make the two rules structurally similar whereas the bilateral version exhibit structural differences as shown below.

**§37.36 Only location matters.** Now forget everything you assume about logic. Forget formu-
las. Sequent calculus rules are only about sequential manipulation of addresses. What we have done is dividing a formula into several disjoint locations. Even forget the sacred axiom rule which says that two locations are related. It is then only possible to *copy* from a *A* location to another *A'* which is a sort of axiom but impossible to say that two locations refer to the same thing<fnref n="13" />. Because axioms are forbidden, proofs have now infinite height. But because we can always split the current context into sublocations, proofs also have infinite width. If the interaction between two proofs by cut is a game or a dialogue then we have the possibility to never finish. A proof is completed either with a rule (⊠) called *Daimon* so that a player can abandon and stop, or if it cannot split any more. Proofs are called *designs* and use the rules of Figure 37.8. Simple examples of applications of rules taken from Seiller’s master thesis<fnref n="14" /> are given in Figure 37.9.

§37.37 **Chronicles and interaction.** A technical problem occurs: since the distribution of context is free, it is possible that two proofs only differ from how they manage their context. However, there is no way to distinguish these proofs by interaction. For that reason, we instead use *chronicles* which are trees of rule application satisfying some conditions such that the alternation between positive and negative rules or the subject of rules being all distinct. The *interaction* (representing cut-elimination) between two designs with root of opposite polarity is given by a maximal alternating path (as in GoI) between them. This path represents a dialogue or play between the two designs.

§37.38 **Reconstruction of formulas.** Formulas can be reconstructed in the usual way (cf. Section 33) by considering set of designs as pre-behaviours. Correct formulas correspond to behaviours. We usually want interaction to be terminating, hence two designs are orthogonal when their interaction terminates.

§37.39 Ludics has been developed by Basaldella and Faggian to include exponentials [BF11]. Quatrini and Lecomte developed applications to linguistics [LQ09] (especially in the context of *pragmatics*) which have been presented in books such as Lecomte’s “*Meaning, logic and ludics*” [Lec11] or Fouquéré et al.’s “*Mathématique du dialogue*”. One recent work of interest is Fouquéré, Pinto and Quatrini’s studies of dialogue with schizophrenic persons using ludics [FPQ21]. Finally, Terui has proposed a computational variant of ludics [Ter11] which could serve as a tool to analyse automata theory and computational complexity.

**38 Discussion: new insights on the notion of proof**

§38.1 So, what GoI says about reasoning? First, that linear logic can be understood from very basic operations: connecting locations in space. Axioms and cuts are about plugging wires (cf. Figure 32.1). Of course, it is much more complicated beyond MLL but the intuition is still there.

<footnote n="13">¹³The same idea appears in game semantics with *copycat strategies*.</footnote>

<footnote n="14">¹⁴https://www.seiller.org/documents/ludique.pdf</footnote>
§38.2 An old and serious problem of formal logic was the problem of justification of logic (cf. Paragraph 12.4). A common solution was to resort to external explanations such as models or languages commenting logic. But what we were doing was delegating explanation of logical syntax to... another logical syntax. But what justifies the latter? Probably another syntax. If we are not concerned with foundations of logic, this can be enough. The BHK interpretation (cf. Paragraph 21.1) and relations between computation and logic in general provide alternative computational explanations: we have ways to construct logical objects and use them. This already tells us that reasoning is about constructing tools and using them. However, these tools have to be justified. In the CHL correspondence, although logical entities have a computational ground, the shape of proofs is still decided by a sort of book of “what proofs should look like”. Of course, it is possible to use external mathematical tools and discover linear logic, then proof-nets. But how far can this reductionist approach go? Going from one book to another gives us new tools but does not necessarily enlighten us about the foundations of logic.

§38.3 **A uniform space of interaction.** In realisability interpretation (cf. Section 22), we can ground logic on almost anything providing it works. But in its original presentation, it still suffers from the conceptual problems described above: the objects are constructed but not justified apart from a priori normativity. Formulas represent computational behaviours. The case of classical realisability (cf. Section 22) is especially interesting because it puts λ-terms against stacks. Terms are justified by stacks and stacks are justified by terms in a dual and symmetric interaction. Hence, two classes of constructions are mutually justified. This suggests that logical syntax could be justified by another logical syntax itself justified by the first syntax, hence “closing the space” and preventing the infinite loop of external semantic explanations.

§38.4 The GoI (which is not a reductionist approach but a true *change of format* as in classical realisability) offers a uniform space for linear logic where interacting objects are of same kind and same degree of freedom in their construction and interaction. In Girardian terms, this is a *monist approach* instead of a *dualist* one. We do not assume any separation between two interacting classes of computational entities but study the interaction occurring within the same space of computation.

§38.5 The monist approach can be seen as an ideal for an interpretation of Schütte’s completeness proof [Sch56, BT09] in which a statement either has a proof or else a partial aborted proof can yield a counter model<fnref n="15" />. In the GoI, this counter model is turned into a pre-proof, exactly as proofs themselves. Meaning that we can construct both a pre-proof of A and a pre-proof of its negation A¹ and making them interact in GoI.

§38.6 **A general method.** The idea of GoI is generic. We start from a model of computation such as:

* finite permutations;

<footnote n="15">¹⁵Note that it looks like the term “monism” for logic arose with ludics.</footnote>
* finite matrices;

* operators in some algebra;

* wirings (made of flows);

* interaction graphs and graphings;

* designs (in ludics);

* partitions of a set

and use a realisability interpretation for linear logic. This interpretation is related to a categorical model known as *double glueing with biorthogonality* [HS03]. They all have in common that they can natively express *linear objects* as wires linking points (except for ludics which is directly related to the sequent calculus, considered as already correct w.r.t. proof-net theory). We then have more of less sophisticated mechanisms to handle exponentials. The common point between these interpretations is that they see proofs as sort of paths/networks (except for ludics). It is then natural to consider alternative or exotic models of paths to generalise the notion of logic.

**§38.7 The existentialist hell.** In Girard's papers, *essentialism* in logic refers to the approach of assuming types as primitive constructions and then programs are constructions following some typing rules. This is also known as *Church typing* in reference to Alonzo Church. It is the opposite of *existentialism* (or *Curry typing*) where types are constructed after programs. The GoI, ludics and classical realisability can be seen as existentialist approaches whereas usual approaches of logic are essentialist (type theory, model theory, truth interpretations, ...). The advantage of existentialism is that we are able to provide a type to *any* program whereas essentialist approaches can only construct programs from some given types (for instance, $\lambda x.xx$ is excluded as a type in simply typed $\lambda$-calculus). There is nevertheless a problem with existentialism: undecidability (cf. Paragraph 22.3). We are not always able to type a given program $\Phi$. In terms of realisability or GoI, this is due to the potentially infinite set of tests orthogonal to a program. In order to assert if $\Phi \in B^\perp$ for some set of tests $B$, $\Phi$ would have to pass infinitely many tests. We are not able to *name* things. As if we understood the concept of cat perfectly and studied it from all possible perspectives but could not even tell whether we had a cat in front of us<fnref n="16" />. Imagine if I was explaining the meaning of a word with all its possible contexts. The solution is to take inspiration from proof-nets where correctness is certified in an effective way with correctness criteria. This gives a *finite* definition by showing how our objects are *shaped*; what I like to call a *pictorial semantics*.

**§38.8 A space of decomposition.** What the GoI does is not opposing proof-nets or proof-structure against other objects as in classical realisability. Surprisingly, it rather shows that a proof-structure can *already* been seen as a connexion between two distinct and

<footnote n="16">¹⁶This occurred several times in the history of science (not for cats). For instance, researchers in biology were familiar with works related to living beings but are still having difficulties to properly define what a living being even is.</footnote>
dual parts: the vehicle (top, axioms) and a test (bottom, syntax tree of sequent). This decomposition is not innocent because it says that the objects we were manipulating actually feature a *computational* and a *logical* part. It is because we have a monism instead of a dualism. The computational content of MLL proofs lies only on axioms since the ax/cut elimination identifies some atoms and the $\forall/\otimes$ cut-elimination only re-organises the connexions later pushed to the top. Moreover, proof-structures can be seen as *pre-typed* since the bottom part specifies constraints on axioms. It opens the idea that we can speak of programs and tests independently in the context logic and study how they are related. In this point of view on logic, we do not manipulate “proofs” but computational entities (vehicle) relatively to some objects materialising normative constraints over computation (tests).

§38.9 **Internalising correctness.** In proof-net theory, we start from proof-structures as general computational objects and discriminate correct ones by an *external* method by considering alterations of $\forall$ nodes (for the Danos-Regnier correctness). One achievement of the GoI is putting both proof-nets and what makes them correct in the same space of interaction. Hence what makes proofs correct is *internal* to them. This offers a solution to the problem of justifying logical correctness. However, once a computational entity is certified by some finite set of tests (Danos-Regnier tests for instance), how can we tell that it will behave as expected, *i.e.* that the tests are sufficient? This is one important subject of the transcendental syntax introduced in the next chapter.
# Chapter 6

## Towards a transcendental syntax

The transcendental syntax (TS) is a series of four papers recently introduced by Girard as a natural successor for the geometry of interaction. It is a complete re-structuration of logic *from* computation and not an extension of the Curry-Howard-Lambek correspondence which merges scientific practices. It is meant to be a philosophical and technical search for fully internal and finitist explanations of logic. It offers new tools for the analysis and criticism of logical notions by providing a new point of view on logic, computation and their relations by taking inspiration from a lot of topics such as classical realisability, logic programming and developments of linear logic (mainly geometry of interaction and proof-nets). It can be understood as a sort of *critical theory* for logic.

Ideas of TS has been scattered for a long time in Girard's writings.

• In the end of the chapter about proof-nets in his "Blind Spot" [Gir11a, Section 11.C.5], he writes:

> "Sequentialisation is not a dogma, it is a tool, which enabled one to find the procedural contents of nets; [...] But, on the whole, one has nothing against the idea of non-sequentialisable nets, as long as one can manipulate them : the ultimate meaning of logic is this ability to manipulate.

> – Jean-Yves Girard

This emphasizes the idea of logic as exit doors stated in Paragraph 31.4.

• In the fifth paper on GoI, Girard remarks that negation internalises normative constraints:

> "For instance, formulas do not proceed from the sky; they proceed from their own operationality. What can be internalised by means of the negation, which thus takes in charge logical normativity: before
refuting, negation forbids.

– Jean-Yves Girard

”

* The recurrent idea of communication (cf. Paragraph 33.33) which is materialised with flows (cf. Section 37) will be a key point of the computational foundation of TS.

The first papers which can be as pre-figurations of TS are Girard’s “Geometry of Interaction VI: a blueprint for transcendental syntax” [Gir13a] and the paper associated with his invited talk “Three lightnings of logic” [Gir13b]. Technically speaking, the TS proposes:

* a philosophical and conceptual developments of ideas coming from the GoI, proof-nets and ludics;

* a Turing-complete computational basis for logic which I call “stellar resolution”;

* a reconstruction of linear logic from stellar resolution (inspired by his works on GoI);

* a new architecture of the logical activity;

* a new definition of first and second-order logic;

* new connectives for linear logic;

* an attempt at giving a better explanation of what happens in innocent operations such as using a deduction rule;

* an opening to new investigations about truth and the normative constraints of logical systems.

These novelties are only partially explored in this thesis.

## 39 Learning from the past

I recommend Michele Abrusci and Paolo Pistone’s paper [AP14] on the Kantian nature of the TS project for a precise and statement of problems occurring in formal logic, the potential solutions offered by the TS and a description of its philosophical ambitions.

**§39.1 Linguistic turn.** In Abrusci and Pistone’s paper, two main characteristics of mathematical logic are mentioned [AP14, Section 2], which are primitive definitions:

“The necessity to provide, in advance to the definition of “a logic”, a formal description of the syntactic devices to be used within such a definition (i.e. a definition of what is to be considered a formal language and a formal
”

system).

and linguistic explanations:

“

“The fact that the rules and axioms which constitute, within a formal sys-
tem, “the logic” under consideration, have to be validated by reference to
an interpretation, that is, a function assigning specific values, belonging to a
certain mathematical structure, to linguistic entities, so that the interpreta-
tions of those rules and axioms result in transformations preserving some of
those semantic values (typically, truth).”

”

This implies that primitive and rigorous manipulation of syntactic objects coming from
a shared conception of logic is a necessary condition for any logical discussion. Hence,
logic would be purely based on linguistic practices. But even more than that: it implies
an impossibility of analysing logic itself as it always escape any attempt. In particular,
Pistone has mentioned [Pis15] former Wittgenstein’s idea that “it takes rules to justify
the application of rules”, making any explanation of logic circular.

§39.2 **Geometric/morphologic turn.** TS (technically based on GoI) can be seen as an answer to these points. GoI and proof-nets already provided answers but only TS clearly states interpretations and refinements of the technical advancements of GoI.

1. The GoI shows that it is not necessary to start from logical definitions to speak about logic. It is possible to start from a computational basis (permutations, operators, graphs, ...) to reconstruct logical objects. However, it is only in TS that this idea of reconstructing logic is pushed to the extreme, by trying to justify points that the GoI did not treat such as the axiom rule, equality, finite verification, Danos-Regnier correctness and more that will be explained in this chapter.

2. Proof-nets show that logical objects can be justified by *shape*. Given a computational object, correctness criteria provide objects (correctness graphs) able to characterise the “shape of logical objects” (indeed with respects to our practice of logic in sequent calculus). However, this operation is still external (tests not expressed as proof-structures). In the GoI, tests and vehicles are objects of the same kind which are able to internally explain logic. However, this explanation is only partial and a lot are still yet to be justified in logic (as explained in the first point).

§39.3 **A pictorial semantics.** The lesson is that if we trap formal logic into a linguistic world, any linguistic object is necessarily explained by another linguistic object. Think of a dictionary in which everything is defined by words which are themselves explained by other words. Ultimately, either the explanation is circular or we have to stop with some words left unexplained and simply assumed because we “know and understand the
words”. A way to get out of this trap is to provide a *pictorial* explanation. You want to understand what a tree is? Forget your dictionary, I will show you few representative trees. This is what TS does by using *morphologic explanations* [Gir18a, Section 1.1.2]: the logical has a specific shape which can be made explicit by correctness criteria. Speaking about shapes breaks the separation between syntax and (external) semantics. This is because some classes of shapes (trees in forests) are already naturally present in our perception of reality that logical discussions are even possible (speaking about trees). Surprisingly, this looks like a return to... Aristotle (cf. Section 1) and (ironically) to a form of... essentialism (but a more refined one).

**§39.4 Archeofuturism.** TS is not a rupture with the past erasing previous conceptions of logic. We have to forget as much as possible what we know about logic but still with traditional logic in mind:

> Even if we want to construct logic from scratch, this can only be a reconstruction, which means that we roughly know what we are aiming at. For an obvious reason, by the way: logic is a very healthy activity, which only suffers from a metaphysical, prejudiced, approach, that of analytic philosophy.

> - Jean-Yves Girard [Gir17, Section 1.6]

Girard’s first objective in TS was to reconstruct logic from a more mature version of proof-net:

> The general task is to reconstruct logic [...]. Which amounts basically at finding the definite version of proof-nets.

> - Jean-Yves Girard [Gir17, Section 1.6]

The idea is to justify some parts of tradition instead of totally denying it or suggesting new cultures of logic totally replacing the previous ones. The future of logic would then be constructed upon justified vestiges of the past and old intuitions (which led to traditions).

**§39.5 The blind spot of logic.** In his course “*The Blind Spot*”, Girard explains the title which reflects his own philosophy of logic:

> About the title: it is while revising the text (Summer 2005) that I noticed the recurrence of the expression 'blind spot'. The blind spot, this is what one does not (is not) see(n), and one does not even know that one does not see

> it. - Jean-Yves Girard
It simply means “beware the appearance”. The logical concepts directly accessible to our intuitions hide a lot of mechanisms. We cannot content ourselves with simple ex- planations and justifications which would hide all the complexity of logic. In order to analyse the different blind spots of the past, Girard defines several levels called hells [Gir11c, Section 1.2]. Lower the level is, the more we see. In particular, you will remark that what changes is the complexity of the space of answers.

§39.6 Girard's hells: level -1 (alethic). Formulas are sort of questions for which proofs are answers. The level -1 corresponds to truth interpretations, modalities and models. The answer to a question is either yes (true) or no (false). We do not have more information. Proofs of $A \lor B$ coming from $A$ or coming from $B$ are not distinguished. They all have the same purpose of leading to the truth of $A \lor B$. All we have to do is to follow definitions of what being true means. This level is sensitive to incompleteness where a mismatch between truth and provability occurs.

§39.7 Girard's hells: level -2 (functional). We add the “why” to the answer. Answers are subject to constructions (categorical interpretations, CHL correspondence, intuitionistic logic) but this construction still follow some rules of “good practices” with a zoology of constructions. It is like having allowed and disallowed correctness tests and computational objects. Proofs are distinguished by their structure: a proof of $A \lor B$ coming from $A$ is different from a proof coming from $B$. They correspond to two different programs (left and right injection) which do not behave in the same way. This is also at this level that we find Kleene realisability and similar realisability interpretation (although they are more free in the choice of computational basis, logic is still constrained).

§39.8 Girard's hells: level -3 (interactive). We add the “how” to the answer. The answer is explained by all its possible interactions. Answers are proofs in the orthogonal of a set of tests associated with the question-formula (the negation/orthogonality is seen as an exchange of players in game semantics). At this level, we have game semantics (cf. Paragraph 28.3), Krivine realisability (cf. Section 22) and some approaches of GoI in which logic is primitive (interaction abstract machine). Some criteria make our objects correct and they define the notion of provability of a formula:

• winning strategies in game semantics;

• proof-likeness in Krivine realisability (that a term $t$ does not contain a continuation constant $k_\pi$);

• correctness criteria for a given formula in the GoI,

but these conditions still follow the rules of a given logical system and we cannot go outside of it.

§39.9 Girard's hells: level -4 (deontic). This deontic<fnref n="1" /> level makes explicit what makes possible the answer in a lawless world; what are its *conditions of possibility*. The root of

<footnote n="1">¹Relative to duty and obligations.</footnote>
<table><caption>Figure 39.1: Girard's hells.</caption><thead><tr><th>Level</th><th>Answers</th><th>Instance</th></tr></thead><tbody><tr><td>-1 (alethic)</td><td>true/false</td><td>model theory<br>truth interpretations</td></tr><tr><td>-2 (functional/static)</td><td>functions</td><td>category theory<br>CHL correspondence<br>Kleene realisability</td></tr><tr><td>-3 (interactive/dynamic)</td><td>strategies<br>logical paths/tests</td><td>game semantics<br>Krivine realisability<br>interaction abstract machine</td></tr><tr><td>-4 (deontic)</td><td>justified alogical paths<br>justified alogical tests</td><td>ludics<br>geometry of interaction<br>graphings<br>transcendental syntax</td></tr></tbody></table>

possibility is taken to be of computational and structural nature. Nothing is assumed, not even the axiom rule relating two occurrences of atoms. Not even the notion of occurrence itself. Every physical point of a proof is nothing but a location void of meaning. In this level, we make explicit all the logical constraints which were implicit in the previous levels. In particular, the use of logical rules assumes that the shape of our objects induces some expected behaviour by computational interaction. In order to obtain the previous levels, we have to reconstruct logical rules. In this level, we have the GoI in general and ludics but the transcendental syntax is the ideal instance of it.

§39.10 Girard's four hells are summarised in Figure 39.1.

§39.11 **The phantom of transparency.** After the idea of “blind spot”, the idea of *transparency* constitutes Girard’s next thesis [Gir16a]. According to Girard, what directed logic (especially around the crisis of mathematical foundations) was the wish for *absolute transparency*; the ability to see, know and understand everything through x-rays of knowledge. The wish of a transparent world with no secrets, that Girard associates with a dogmatic consideration of science (scientism). Science, by its wish for extreme rationalisation is trapped into systems as if we could only go from a chapel to another. By trapping ourselves into locked systems of thoughts, we leave no space for intuition<fnref n="2" /> and doubts<fnref n="3" />. Girard claims that all works on logic until today show that absolute transparency in logic *is not possible* (in particular because of incompleteness and undecidability). It is impossible to directly access reality from immediate perceptions. The access to reality has to be subject to a construction made intelligible to us.

<footnote n="2">²What the *mystical* had the most, while being the polar opposite of reason.</footnote>

<footnote n="3">³Some (often social and political) systems of thought leave almost no space to doubts or incomplete data, to the point that some causes and consequences are almost logically derived. For instance, the materialistic world view seeing capitalism as the root of all evil and problems. Another example is the very structured world view of some conspiracy theories.</footnote>
§39.12 **Soft scepticism.** The refusal of absolute transparency leads to an unavoidable scepticism. However, this scepticism has to be measured. In TS, the approach is to start from as less assumptions as possible and try to justify what we could already do. In the case of proof-nets, we consider links between points without any meaning. It is even more radical than proof-structures which are implicitly typed/pre-constrained (cf. Paragraph 38.8). On the top of that, in order to fully recover (at least) MLL proof-structures, we must add explicit constraints such as the fact that axioms link dual occurrences. We will also be led to a bit of controversial revisionism by questioning the most elementary things and rethink foundations.

• What is a proof? What is a formula?

• What is truth? What is provability?

• What is a logical rule? What allows us to use logical rules?

• What is a program? What is an algorithm?

• What is the purpose of logic?

• Why does $A \Rightarrow A$?

• Why does $a = a$?

• ...

This scepticism which can sound extreme is still limited since we cannot doubt of everything (otherwise we would do nothing and just wait for our death).

§39.13 **The search for internal explanations.** TS searches for internal explanations. Such explanations have already been found in the GoI (cf. Section 38) but an old (unintended) pre-figuration that Girard especially likes comes from Herbrand [Her30] works on predicate calculus and unification. The idea is better understood from *herbrandisation* which is dual to *skolemisation* (cf. Paragraph 23.10) by eliminating occurrences of existential quantifiers preceding a universal quantifier. We write $A[x_1, ..., x_n]$ and $t[x_1, ..., x_n]$ for a formula $A$ and a term $t$ containing variables $x_1, ..., x_n$. The idea is that the formula $\exists y. \forall x. A[x, y]$ can be proven by selecting some $y := t$ such that $A[x, t]$ holds for any $x$. However, this $t$ cannot depend upon $x$ because $\forall x$ comes after $\exists y$. There is, however, a dependency between quantifiers. This can be written by an equation $x = f(y) = f(t)$. The point is that if $t$ contains $x$ (which is written $t[x]$), then we have the unsolvable equation $x = f(t[x])$. The meaning of quantifiers is given by internal dependencies, without any reference to an external semantics. TS will be based on this idea applied to a new version of proof-nets.

§39.14 **No direct access to reality.** TS assumes no direct access to reality (in contrary to semantic realism). In particular, in the GoI, logic has always been defined from a choice of model of computation: permutation, partition, graphs, operators etc. Logic
is always accessed through a subjective medium<fnref n="4" /> providing an access to reality. There
are indeed better choices but no absolute and definitive choice<fnref n="5" />. It is only from a given
representation of reality that some patterns and structures will be distinguished and
define the logical. On the technical side, TS begins by choosing an appropriate model of
computation on which logic would be based. Since Girard uses a lot of inspiration coming
from proof-nets, this model should feature the elementary mechanics of proof-structures
while being as “large” as possible.

**40 The logical avant-gardism of computer science**

§40.1 In TS, we are not exactly looking for connexions with computer science but rather inspirations and roots *within* computer science. Girard shows (in some recent papers but more especially in his book *“Le fantôme de la transparence”* [Gir16a]) several times that simple ideas coming from computer science are enlightening for logic. I would like to develop and make explicit how. I personally believe that logic has a lot of things to learn from computer science and programming in general, even from the most elementary and practical notions<fnref n="6" />. This section emphasizes the idea of *logic as tool* (or Organon in Aristotelian terms).

§40.2 **The procedural content of logic.** First, from a computational point of view, it is possible to distinguish notions which are not distinguished by semantical explanations [Gir16a, Appendix B.2]. As explained in Paragraph 11.7, $A \Rightarrow B$ and $A \vdash B$ have the same semantics but computationally speaking, $A \Rightarrow B$ can be seen as a frozen function made of symbols. It can be erased or duplicated like any data, as if we were handling the code of a program instead of the program itself. However, $A \vdash B$, makes the function participate as a program. It puts the data of the function in the space of interaction of a sequent which can be subject to cuts and cut-elimination. The formula $A \Rightarrow B$ is therefore of a static nature whereas $A \vdash B$ is a of a dynamic nature. In the GoI, the meaning of an object is given by its possible interactions.

§40.3 **Radical inclusivity.** In traditional logic and type theory, we tend to reject some objects because they are not “logical”. Similarly to Curry’s Urlogik (cf. Paragraph 15.8) which accepts paradoxes, there is less rejection in computer science. In programming, we have viruses which are self-duplicating malicious programs. Servers are finitely described programs which never terminate but are still essential<fnref n="7" />. While we are thinking about whether there are several or only one single logic, programming admits several

<footnote n="4">⁴This may be related to Kant's transcendental subject but I do not have enough philosophical knowledge to tell more.</footnote>

<footnote n="5">⁵I asked Girard why the model of stars and constellation that he uses was the best analytic space and he told me that this was because there was nothing simpler. Apparently, he tried several things and it was the most natural formulation.</footnote>

<footnote n="6">⁶Funnily, it was originally the converse. At the time of the CHL correspondence, logical ideas were discovered several years before their computational counterpart.</footnote>

<footnote n="7">⁷Jean-Baptiste Joinet would probably say that there are “queer” λ-terms escaping type systems.</footnote>
(sometimes weird) languages with their own characteristics, use and culture even though
it seems there is only one notion of classical computation (an idea reinforced by the
Church-Turing thesis). There are programs (compilers and interpreters) translating one
language to another.

§40.4 Test of programs. In realisability and the GoI, the term of “test” is used to describe the computational opponents of programs. It makes even more sense with proof-nets where Danos-Regnier correctness hypergraphs (or Girard’s switching flow graphs) are finite and effective ways to tell if a given set of axioms has a sound behaviour w.r.t. cut-elimination, i.e. that it is correct. This idea of test can be explored from the point of view of computer science. In software engineering, there are several tools to test programs. For instance;

* in *unit testing*, a portion of a program (typically a function used in a bigger program) is tested as an independent part. Typically by using representative cases for a partition of the domain (possible inputs);

* in *black-box testing*, a program is tested without having any knowledge of how the program is implemented or how it works. It is similar to tests on living beings such as psychology tests, laboratory tests on animals, Turing tests or Voight-Kampff tests in the movie *Blade Runner*;

* in *white-box testing*, we are aware of how the program being tested is shaped. It is similar to how circuits are tested;

* it is also possible to test the security of a software (for instance in *destructive testing*) by attacking it. We can check if a software is sensitive to some types of attack or if it behaves well in case of true failure. For instance, code injection is a type of attack exploiting a vulnerability of a program in order to inject unwanted instructions which will be executed<fnref n="8" />.

§40.5 File format. The concept of *format* is essential in the philosophy of TS and can be easily understood from computer files [Gir16a, Section II.3]. For Girard, logic is a formatting of raw data which guarantees that logical entities will have a specific shape and interact as expected. It is exactly the same for computer files. We have raw data (which can be represented with binary or hexadecimal digits) and files can be associated with file extension (`.pdf`, `.exe`, `.png` or `.jpg`). File extensions indicate that a file containing raw data is organised in a particular way. For instance, picture files are mostly represented by a matrix of codes for the colour of each pixel of the picture. Pictures having the `.png` extension can represent transparent pixels while `.jpg` cannot. There are also extensions for the programming language of a source code. A file with `.c` extension is written in the C language and will not behave well when given to an interpreter for the Haskell language. Proof-structures are examples of raw data and correctness criteria

<footnote n="8">⁸I like to see Gödel’s first incompleteness theorem as a sort of code injection on an arithmetic system. We take advantage of the freedom of arithmetic expression to inject Gödel’s formula which, when interpreted, leads to a contradiction.</footnote>
are examples of formats for proof-nets. Proof-structures can be given the extension `.proofnet` when it passes the tests of some sequent.

**§40.6 Hidden files.** In a computer, some files are hidden. The reason is simple: we do not need to see them but it is possible to see them if we really want. These files typically contain configurations read by some software. They are important for the architecture of the system but not necessarily for us. According to Girard [Gir20a, Section 1.3], these hidden files exist in logic and can be revealed (however, since no direct access to reality is assumed, this is only a representation accessed by cognition and not *the* hidden files). For existence, the contradiction **0** of linear logic is usually thought to be empty (it has no proofs) but in the TS, it has a computational content. This is not so surprising if we consider that it is possible to interact with erroneous programs. This idea is directly related to Girard's "blind spot". In his fourth paper on TS [Gir20a], Girard roots his notion of truth in the idea of *visibility*. Are true the objects which are visible.

**§40.7 Modules and libraries.** In his recent unpublished papers, Girard compares logical systems to bunkers [Gir19, Section 2]. The reason is that in a logical system, we established fixed ways to do things correctly. Different logical systems live separately like hermetic clubs. One formula true in a system can be false in another and we avoid mixing systems to avoid inconsistency. According to Girard, logic should be more like modules in programming [Gir20b, Section 1.3]. In a same programming language, it is possible to import files containing several functions. These files are called *libraries* or *modules*. For instance, if we would like to use mathematical functions in the C language, we can write `#include <math.h>`. It is also possible to do partial importations. If we apply the idea to logic, it is like importing connectives from different logical systems and using them in a same context (a sort of "logical ecumenism"<fnref n="9" />).

**§40.8 Reverse engineering.** Reverse engineering corresponds to the process of opening up and dissecting a system to understand how it is functioning. It is typically used in software and electronic engineering but can be applied to other fields as well. For instance, it is possible to *disassemble* programs by translating the content of an executable program to an assembly language (a low-level language). By using this assembly representation of the program, it is possible to track some mechanisms and behaviours in order to partially understand the whole architecture of the software. It is then possible to modify or enhance some parts as we wish. It is a *reverse* approach in the sense that, usually, we first design the architecture of a system then implement it but in the case of reverse engineering, the system is already there and we would like to infer its underlying architecture. I personally like to see TS as a *reverse engineering of logic*<fnref n="10" />.

<footnote n="9">⁹Expression suggested by Jean-Baptiste Joinet.</footnote>

<footnote n="10">¹⁰We can also say *deconstruction*.</footnote>
<table><caption>Figure 41.1: Cognitive knitting of the transcendental syntax.</caption><thead><tr><th></th><th>Analytic / Brut</th><th>Synthetic / Formatted</th></tr></thead><tbody><tr><th>A posteriori / Explicit</th><td>Constat</td><td>Usine</td></tr><tr><th>A priori / Implicit</th><td>Performance</td><td>Usage</td></tr></tbody></table>

# 41 A new architecture for logic

All alternative references for this section are unfortunately in French. I recommend Girard's book "Le fantôme de la transparence" [Gir16a] (I think we ironically have to understand the TS first before understanding what Girard says in this book) and Sidney Congard's unpublished paper "La logique face à l'arbitraire" [Con22] which explains in simple terms the project and architecture of TS.

§41.1 TS suggests a new architecture to understand logic in light of computation. This architecture, called *cognitive knitting* by Girard, is apparently of Kantian inspiration<fnref n="11" />. This knitting is made of four interrelated categories (given in Figure 41.1) in which logic is about answering questions.

* The *analytic* is a world of lawless computation. This is where answers are expressed and where proofs/programs are shaped (only in their structure and not in their meaning). We can express “yes” or “no” but without context. It is objective.

* The *synthetic* corresponds to logic which has the role of *formatting* computation. It is where questions (formulas) are shaped by formatting answers (giving a context to computational objects to yield a proof). We provide a context for which words such as “yes” or “no” are answers to a question. It is subjective.

* These two categories are either *a posteriori* (explicit) or *a priori* (implicit). The correspondence with Kant<fnref n="12" /> is that the explicit (a posteriori) *depends on experience* because we need a method to reach it from the implicit, while the implicit (a priori) does not depends on experience. I can construct a program out of my mind but I need the process of execution to reach the result.

Unlike Kant's epistemology in which “analytic” and “synthetic” are characteristics of assertions, in TS, they refer to spaces of objects (answers and questions) which can be realised in mathematics. In the following sections, we explain this cognitive knitting in details.

<footnote n="11">¹¹I cannot tell how serious this is since I have never read a single line of Kant (but it seems that Girard neither, see https://www.youtube.com/watch?v=f7sT0J74pHI#t=3m18s).</footnote>

<footnote n="12">¹²Probably. Because I have never read Kant.</footnote>
**42 Analytic space / Answers**

§42.1 It can be intriguing that TS is introduced from the notion of *answer* instead of questions, because to have answers we must have questions first. How and what can we answer otherwise? Is it only provocation? Is it only an expression of anti-conformism? Not really<fnref n="13" />. Starting from answers is justified by the wish to justify logic from as less assumptions as possible. We would like to define a lawless and objective world of computation where logic does not exist. An anchor to all discussions. Starting from questions would mean that we already assume a format in which questions are expressed (a logical system for instance). Then the space of answers would necessarily be limited because of this constraint.

§42.2 Answers are objective because not engaged in a meaningful context. When I say “yes” or “no”, it means nothing without a context. If I have a sound confirming an operation (coming from a machine for instance) and isolate it from its context, it is just a raw sound but if it happens after I do something on my computer or any other machine, it can mean something. Since “yes” and “no” are very limited answers, we would like the largest space of answers as possible. In particular, answers should be reducible to more explicit answers (similarly to the explicitation occurring in explanations).

§42.3 A model of computation has to be chosen for this space of answers. However, it is possible to describe Girard's architecture independently of this choice. We write $\mathfrak{A}$ for the analytic space which is a countable space of objects $\Phi, \Psi$ called computational objects/entities<fnref n="14" /> (a term that I used a lot but which is only made clear here). The analytic space is understood from two categories: the Constat and the Performance which characterise requirements for the objects of $\mathfrak{A}$.

**Constat and performance**

§42.4 **Constat (result).** In the analytic space $\mathfrak{A}$, we must have objects corresponding to (final) *results*. Those results, called Constats are just there. Nothing happens with them. They are *explicit* (nothing is hidden). In the category of Constat, symbols can only be accumulated. Girard compares it with typewriters in which symbols can only be added without being subject to any dynamics (such as erasure or duplication). In the $\lambda$-calculus, it corresponds to terms in normal form which cannot be reduced. For instance $\lambda x.x$ or simply $x$.

§42.5 **Performance (dynamics).** The category of Performance corresponds to pairs $(\Phi, \Psi)$ with $\Phi, \Psi \in \mathfrak{A}$. Two objects can interact by *execution* (defined in $\mathfrak{A}$) and produce a new object $\mathrm{Ex}(\Phi, \Psi) \in \mathfrak{A}$. For instance, if we encoded circuits, $\Phi$ would be the structure of a circuit and $\Psi$ its evaluation function (turned into an interactive object of $\mathfrak{A}$). Objects of

<footnote n="13">¹³Probably a little bit actually.</footnote>

<footnote n="14">¹⁴They are sometimes called “epistate” in Girard’s terminology [Gir11c].</footnote>
the Performance are *implicit* since we need a method to extract the content they hide. Performance corresponds to reducible objects such as redexes of λ-calculus of the form (λx.M)N evaluated into {x := N}M by β-reduction. Girard compares it with computer keyboards which can do unexpected things such as launching a program.

§42.6 Similarly to the λ-calculus, we can choose to not execute a reducible term. It means that any performative object can be seen as a Constat in the case we are not interested in evaluating it. Girard uses the analogy of a cheque (or bill) which can be used to pay something but which can also be exposed on a wall (in reference to Paul Erdős' cheques). Hence, in $\mathfrak{A}$, we should be able to make some parts impossible to reduce or to make more explicit: there is an end to the explicit.

§42.7 **Separating Constat and Performance.** What links Performance and Constat is the notion of execution reducing objects of the former to objects of the latter. It is a way to go from the implicit to the explicit. But what separates them is *undecidability* (cf. Paragraph 13.9) which can be reformulated as follows: Performance cannot be reduced to Constat. We cannot always foresee what will happen if a function interacts with an input. The computation could be undefined or looping.

**The chosen one: stellar resolution**

§42.8 There are several possible choices of model of computation. We could start from any Turing-complete (or even stronger) model of computation. But we cannot choose any model. We have to choose something as close as possible to proof-nets (which is considered as the right notion of proof by Girard but which as to be improved). This model should be:

• *self-executing* with local interaction so that we do not assume an external way to execute our computational objects. As Girard says, everything is on the table, including the table itself. We want to make every computational mechanisms explicit. For instance, if we had boolean circuits, the evaluation function would be implemented as well and explicitly interacting with the circuit itself. Such mechanisms of self-interaction appear in tile systems (cf. Section 17). The untyped linear λ-calculus could be a good candidate but because β-reduction is an external procedure and that we require self-interaction, it is not satisfying enough. We could argue that the execution is a global and external computational procedure but the point is that we would like our objects to perform a computation when locally plugged to each other;

• *partially executable* by preventing computation on some parts of our objects. In λ-calculus, weak strategies choose to not execute under abstractions: *M* in λx.M is not executed. In programming in general, it is useless to execute the inside of a function when it is not used;
<table><caption>Figure 42.1: Comparison between GoI and TS.</caption><thead><tr><th></th><th>GoI</th><th>TS</th></tr></thead><tbody><tr><th>Correctness criterion</th><td>Long trips</td><td>Danos-Regnier</td></tr><tr><th>Minimal model (MLL)</th><td>Permutations</td><td>Partitions</td></tr><tr><th>Nature of tests</th><td>Directed graphs</td><td>Hypergraphs</td></tr><tr><th>Unification model</th><td>Flows</td><td>Stellar resolution</td></tr><tr><th>Seiller's models</th><td>Graphings</td><td>?</td></tr></tbody></table>

* expressing computation by *reducible links between addresses* so to interpret proof-structures and cut-elimination but also the idea of sending messages across a structure (as in the token machine for the GoI). This is also something which appears in automata theory in general where automata can be described as links between states in which messages are sent. This can also be related to concurrent computation with processes;

* as less constrained as possible and hence the model of computation should be untyped and be able to be “very free”. We cannot choose something like the simply typed λ-calculus for instance. A possible interpretation is that the analytic space contains at least all computable functions. Ideally, it is non-deterministic, symmetric (no distinction between input or output which is a constraint), parallel and asynchronous (order in sequential computation can be seen as a constraint).

§42.9 The model considered by Girard [Gir89a] is a variant of flows and wirings (cf. Section 37) made of *stars* and *constellations*. I call this model of computation “stellar resolution” for its similarity with usual first-order resolution (cf. Section 23). Flows are binary directed expressions and stars are *n*-ary *undirected* flows. If flows are sort of unification-based directed graphs then stars are unification-based hypergraphs. Flows can naturally express Girard’s long trips and stars can naturally express Danos-Regnier correctness. At a technical level, this makes TS a GoI for Danos-Regnier correctness. This difference between the two approaches are described in Figure 42.1. Notice that there is currently no equivalent to Seiller’s graphings [Sei17] in the TS but we could imagine sort of *hypergraphings*.

§42.10 We leave the proper definition of stellar resolution for the next chapter and keep on with the description of Girard’s architecture independently of a choice of model of computation.
**43 Synthetic space / Questions**

§43.1 The synthetic space is where questions are formulated, where everything takes its mean-
ing. It is the logical language. If my answers were “yes” or “no” then I can formulate
questions such that “Are you a man?” or “Are you a woman?”. If the space of answers is
large enough, we can even express more or less convincing proofs coming together with
the answer. The activity of logic will revolve around the adequacy between questions
and answers. Question should also be able to interact: if I have a positive answer to
“Does A implies B?” and a positive answer to the question A then I should be able to
produce an answer for the question B (this corresponds to the modus ponens).

§43.2 The synthetic is meant to *format* (or to give a format) to the analytic. A way to do that is to *classify* objects of $\mathfrak{A}$ by grouping them into sets. We write $\mathfrak{S}$ for the countable synthetic space made of sets $A, B \subseteq \mathfrak{A}$ called *pre-formulas*<fnref n="15" />.

§43.3 There exists two ways to give meaning to objects of $\mathfrak{A}$: Usine (factory) and Usage (the use). They respectively correspond to a variant of Church and Curry typing in the context of TS.

§43.4 **Choice of point of view.** In the synthetic, we have to choose symmetric orthogonality relations $⊥ \subseteq \mathfrak{A} \times \mathfrak{A}$ formalising a compatibility between two objects of $\mathfrak{A}$ in order to express that their interaction is sound. The soundness of interaction is subjective, it can be chosen freely. In particular, different choices lead to different logical interpretations. This orthogonality relation can be understood as a point of view on computational interaction.

**Usage / Curry typing**

§43.5 Usage corresponds to meaning as use. The meaning of $\Phi \in \mathfrak{A}$ is given by all its partners of interaction. It is like defining a word by all the contexts it can appear in. How do you know that you have a DVD player in front of you? Bring all the possible compatible DVD and insert them in the DVD player. If everything works fine then you do have a DVD player.

§43.6 It corresponds to Krivine realisability (cf. Section 22) and to the GoI interpretation (cf. Chapter 5). Given a pre-formula **A**, we can define all its partner of interaction by another pre-formula **A**<sup>⊥</sup> := {Φ ∈ **A** | ∀Φ' ∈ **A**, Φ ⊥ Φ'} which can be understood as a set of tests for **A**. To check whether Φ is in the class **A** (DVD players for instance), then we have to test it against all elements of **A**<sup>⊥</sup> (DVD). We are then interested in *formulas* (or *behaviours*) which are pre-formulas **A** such that **A** = **A**<sup>⊥⊥</sup>. Equivalently, it means that there exists some **B** such that **A** = **B**<sup>⊥</sup>, meaning that **A** is fully characterised by a set of tests **B**, or that **A** is *testable*. In the case of behaviours, **A**<sup>⊥</sup> are tests for **A** and **A**

<footnote n="15"><sup>15</sup>Or sometimes *dichologies* in Girard’s terminology [Gir11c].</footnote>
are tests for $A^{\perp}$. It is only a matter of point of view: a DVD can be tested by the set of all DVD players. This interpretation has been formally implemented in Section 33 and can be generalised by starting from any model of computation. Usage is an *existential* (Curry) way to type objects because types (essences) come after the object being typed (existence).

**§43.7 Ideal concepts.** In Usage, it is possible to define concepts by interaction and yield other concepts by orthogonality. It is in Girard's Usage that the tensor product of two formulas $A \otimes B$, its dual $A \N_B := (A^{\perp} \otimes B^{\perp})^{\perp}$ or the linear implication $A \dashrightarrow B := A^{\perp} \N_B$ are defined "by interaction". However, these notions are *idealised concepts* of tensor, par and implication. The possibility of having infinite tests makes formulas sort of god-given concepts which are perfectly defined and inferred from pure reason. However, this is also what makes them *too powerful* and unpracticable.

**§43.8** It is in Usage that elimination rules of natural deduction are justified. Typically, the modus ponens is seen as an interaction between $\Phi \in A \dashrightarrow B$ and $\Psi \in A$. It is possible to prove that under the right conditions, we have $\mathrm{Ex}(\Phi, \Psi) \in B$ for any $\Phi \in A \dashrightarrow B$ and $\Psi \in A$. Elimination rules are justified by their *use*, accordingly to old intuitions which are now made explicit (cf. Paragraph 12.4). See Pistone's works for more about how Girard's approach can serve as a justification of logical rules [Pis15].

**§43.9 The existentialist hell (again).** The problem (already stated in Paragraph 38.7) is that we cannot pass infinitely many tests in practice. It makes no sense to bring all possible compatible DVD to say that I indeed have a DVD player in front of me. It is like certifying a car in a factory by making it interact with all possible use cases including driving it forever to ensure that customers will be able to do the same. But how can you even sell such a product? It would not even get out of the factory. In the real world, we have no choice but to use *definitions* corresponding to a partial view of the object. We need *decidability* to be able to put words over things. If we are only interested in inferences on perfect, abstract and universal ideals, then we do not even need the orthogonality relation to be computable.

Usine / Church typing

**§43.10** The solution to the previous problem of infinite testing is to limit tests to a wisely chosen finite sampling. This is the meaning as finite testing corresponding to Girard's Usine which is the main novelty of TS. It is like testing a DVD player with a chosen set of representative DVD or to apply some sufficient tests to a car. Such partial view on an object correspond to partial definitions which allow to actually *name* and *qualify* the object we manipulate. However this notion of definition should not be understood as a linguistical definition but as a *recognition of shape*, which is independent of language (otherwise we would return to the problems stated in Paragraph 39.1).
§43.11 Such finite testing typically appear in vaccines. The choice of tests is either too strict (and we miss some use cases) or too lax (and we may accept many irrelevant use cases). Either vaccines get too much time and efforts to be validated or we kill some people by mistake (but in the first case some may die as well). Another illustration is chemical/biological testing. For instance, in allergy tests, we put a patient in contact with some allergen and wait for reactions. This is also similar to how tests for viruses or pregnancy tests work. It is acceptable to use several orthogonality relations in case we are expecting different sort of outputs.

§43.12 Once we have a method for effective testing, it is possible to *certify* objects like how we certify a vaccine or a car which passes all our tests. Common examples of our everyday life (especially in France) are various labels attached to products such as “BPA-free”, “Agriculture biologique”, “Made in France”, “Origine France Garantie”. We trust some tests of our everyday life without always understanding what they are about. In particular, the “Made in France” label is rather lax and makes us think that our product is entirely made in France while it only has to be partially made in France. In the case of proof-nets, a proof-structure is certified with a label “Proof-net” when it passes all the tests corresponding to a given sequent.

§43.13 We define a *type* as a syntactic expression *A* (representing a type label) associated with a finite set of tests *Tests*(*A*) and fix a *decidable* orthogonality relation $⊥$. We say that $\Phi \in \mathfrak{A}$ is of type *A*, written $\Phi : A$, when $\Phi \in \text{Tests}({A})^{\perp}$. Type checking (verifying whether $\Phi : A$ for a given *A*) can then be done in an effective way. It is an *essentialist* (Church) typing because types (essences) are defined *before* the objects being tested (existence). However, this is not plain essentialism because in TS, types will be *justified*: there will be some proof that the set of tests is sufficient to ensure that it is part of a corresponding formula. In terms of programming: that the tests are sufficient to guarantee the expected computational behaviour. Plain essentialism would correspond to certifying a vaccine but without verifying if the tests ensure that it will work well. We just have to trust our intuition. This is why I sometimes compare it with a sort of modern or rational essentialism. In proof-nets, type labels correspond to sequents. From a switching on a sequent $\vdash \Gamma$, it is possible to infer a set of tests (Danos-Regnier tests for instance) *Tests*($\vdash \Gamma$) such that if $\Phi$ is a set of axioms, $\Phi \in \text{Tests}^-(\vdash \Gamma)^{\perp}$ implies that $\Phi$ is a set of axioms for a proof-net of conclusion $\vdash \Gamma$.

§43.14 **Partial approximation of an ideal.** Another illustration of Usine that I especially like<fnref n="16" /> is the design of... a chair (yes). When we design a chair, we have in mind all the possible (idealised) positions and use of the chair. But it is impossible to capture them all. All we can do is approximating it as much as possible. The best designers are the ones who can perceive the most accurately those use cases. Formally speaking, tests

<footnote n="16">¹⁶Which comes from a discussion I had with Paul Séjourné after he made me watch a video about Charlotte Perriand’s work on modern design and architecture (I was not expecting that it could be related to logic).</footnote>
of Usine are usually approximations of behaviours of Usage. If we have a behaviour **A**,
then we would like to find a finite set of tests **B** such that **B**⊥ ⊆ **A**.

§43.15 **In defence of prejudice.** My personal interpretation is that Usine is a place where we can express the structure of our prejudices. By prejudices, I mean intuition or unverified belief, which is directly accessible from immediate perception. Those prejudices can then be justified and confirmed (or considered too inaccurate). Tests usually come from a generic structuration of our experience and perceptions. In programming, when designing tests or specifications (or simply writing a program), we are trying to produce a material structuration of a mental representation. Although prejudices can be socially shared (like prejudices thought to come from ignorance), in our case, they have a computational form allowing (more or less certain) checking and confirmation. Usine corresponds to an *awareness* of the structure of our own prejudices.

**Adequacy and certainty / Cut-elimination**

§43.16 Adequacy is what links Usine and Usage. It may sound exaggerated but adequacy is the *heart* of the rational: the justification of our prejudices or the fact that the shape of our objects (given by the tests of Usine) guarantee their use (Usage). It is what conveys *certainty*. If I design a chair, then it would be (in some sense) irrational to design a chair far from any possible use. For instance a chair with spikes. Modern art or fashion, in particular, is often playing with the irrational by materialising it. It seems to me that what is rational is justified beliefs (where defining “justified” is the job of logic).

§43.17 In logic, adequacy corresponds to the cut-elimination theorem (which may sound very surprising). The idea is that in TS, $\Phi \perp \Psi$ formalises and identifies two notions:

• that $\Phi$ passes the test $\Psi$;

• that the interaction (cut-elimination) between $\Phi$ and $\Psi$ representing vehicles of proof-structures behaves as expected.

This is because tests are seen as computational objects of the same kind as vehicles (sim-
ilarly to the GoI interpretation). We obtain a new interpretation of the cut-elimination
theorem. Assume that vehicles and tests are interpreted in a subspace $\mathfrak{P} \subseteq \mathfrak{A}$. The
cut-elimination theorem says that for all $\Phi, \Psi \in \mathfrak{P}, \Phi \perp \Psi$ (their interaction by cut-
elimination behaves well). This is not true in general (since vehicles are more general
than proof-structures for which cut-elimination can be ill-behaving). This is where log-
ical correctness appears: for all $\Phi, \Psi \in \mathfrak{P},$ if there exists $\vdash \Gamma$ and $\vdash \Gamma^{\perp}$ such that
$\Phi \in \text{Tests}(\vdash \Gamma)^{\perp}$ and $\Psi \in \text{Tests}(\vdash \Gamma^{\perp})^{\perp}$ (they are correct and dual), then $\Phi \perp \Psi$. In
terms of proof-structures, if two proof-structures are dual and correct (they correspond
to proof-nets) by passing correctness tests of some dual sequent then their interaction is
sound.

“If objects have the right shape, they will behave well.”
§43.18 **Relating answers and questions.** Usine and Usage correspond to two ways to tell whether an object is an answer to a question. However, only the adequacy justifies this relation by providing an effective verification that it corresponds to an approximation of an ideal. Notice a little change of terminology: in the GoI, ludics and game semantics, answers and questions are terms related to positive and negative connectives but in TS, they correspond to computation and logic. It seems to me that the two contexts are not related and that the terms “answers” and “questions” are too inaccurate in the situation of positive and negative connectives which rather corresponds to an interactive dialogue alternating between *expectations* and *assertions*.

§43.19 **Separating Usine and Usage.** In case we have a cut-elimination theorem, we are able to express an absolute certainty. However, some good logical systems do not enjoy a cut-elimination theorem. In that case, we have a gap between Usine and Usage meaning that Usine is never able to perfectly reach Usage. According to Girard, this limitation corresponds to Gödel’s incompleteness theorems (cf. Paragraph 5.4) corresponding to the logical version of undecidability. Our choice of effective tests in Usine leads either to a lack of consistency or a lack of completeness (it is either too strict or too lax). We cannot always capture all use cases of logical objects with finite and effectively checkable definitions. To illustrate this fact, think of trying to define a musical notation for all possible sounds. A good (French) article explaining the gap between Usine and Usage in my opinion is the first section of Regnier’s “*Les limites de la correspondance de Curry-Howard*”<fnref n="17" />.

§43.20 **Reasonable certainty.** Formal systems not enjoying a cut-elimination theorem introduce some doubts. However, as Girard claims, certainty can still be reasonable in some cases. For instance, it is exaggerated to doubt of the foundations of mathematics. A huge number of theories have been established and used without any foundational fears. Mathematics lies on a solid ground even though it is not absolutely certain. The more we do mathematics, the more doubts disappear (but doubts will always remain) [Gir16a, Envoi: le doute].

Towards a justification of logical rules

§43.21 We would like to justify the rules of natural deduction. As explained in Paragraph 11.3, introduction rules correspond to definitions of symbols (how they are shaped) and elimination rules to use of symbols (how they interact). A prowess of sequent calculus is to reorganise this relationship between definition and use: all logical rules are introduction rules (either to the left or the right of ⊢ but in the monolateral case, it is sufficient to consider only the right). We then have the cut rule which materialise the use. This is made explicit in the translation of natural deduction into sequent calculus (cf. Figure 11.3) where translating elimination rules reveals an interaction by cut between two proofs.

<footnote n="17">¹⁷https://www.i2m.univ-amu.fr/perso/laurent.regnier/articles/ch.pdf</footnote>
§43.22 This distinction between definition (cut-free proofs) and use (cut between proofs) coincides with Usine and Usage respectively. Sequent calculus rules can be analysed from proof-nets which focus on the structure of proofs and how formulas are related independently of the sequential application of rules.

* Usine will yield a translation of cut-free proof-nets. In this case, we are interested in how logical objects are shaped/defined independently of how they interact with other objects. It is the very principle of factories.

* Usage will yield a notion of interaction between cut-free proofs. Given two cut-free proofs, they can interact by using cuts which are sort of adapters linking points of the two proofs so that they can agree on common references.

## 44 Derealism / Animism

§44.1 In Girard's terminology, the term *derealism* (but also *animism*) refers to a subtle intertwining between computation (analytic/object) and logic (synthetic/subject) which is always present in the study of logic and computation. An ambition of TS is to go beyond this asymmetric distinction.

### Logic and computation entangled

§44.2 I claim that most objects manipulated in the context of logic and computation (especially in the CHL correspondence) are hybrid objects with a computational and a logical part. In Section 38, I explained that the GoI was able to separate the computational (vehicle) from the logical (test) content of a proof. Ultimately, the vehicle itself is a sort of test for tests so the roles of test and tested is symmetric and interchangeable. Nonetheless, we are still able to make this distinction.

§44.3 If we look at the CHL correspondence, the correspondence between natural deduction and λ-calculus is not a link between logic and computation but an identification of logico-computational hybrid objects. Since proof-nets are able to encode typed λ-terms, it is possible to analyse λ-terms by separating their computational core (vehicle) from their logical core (what makes the shape of the term, influencing its computational behaviour). Similarly, proof-nets come from sequent calculus proofs which analyse natural deductions proofs. Proofs in proof-systems are then both of a computational (interaction) and logical nature (shape).

§44.4 If we want to be more radical, then untyped λ-calculus is actually already implicitly logical because it treats computation in the context of specific shapes (the structure of λ-terms). These shapes are sort of primitive constraints for computation. This is not so surprising since we were able to split not only proof-nets but also *proof-structures* which encodes untyped λ-terms. However, cut-elimination (ax/cut), corresponding to
<figure><img src="image_83.png" /><figcaption>Figure 44.1: Local (left) and global (right) natural deduction rules.</figcaption></figure>

the execution of terms, is very primitive: as shown in the GoI (cf. Chapter 5), it is
only about reducing links by identifying points (atoms of proof-structures), which can
also be understood as sending messages or making a current flow. I do not count $\mathcal{Y}/\otimes$
or other logical cut-elimination cases because they are not purely computational but
logical as they only reorganise links by specifying right paths for messages, hence enforce
a structure for the computational current. They are implicitly part of tests (hence
the logical part of proof-structures). Proof-structures are also logical because of their
specific shape which makes the computational current flow in a specific way during
cut-elimination.

§44.5 From the radical statement above, we obtain hints about the nature of logic and computation:

* computation is *physical*. It is about current freely flowing, the process of sending information without any constraint. It is related to time;

* logic is *structural*. It is about primitive or constructed paths in which the current of computation flow. It is related to space.

This makes the analytic space a bit logical but it is not a problem since it is meant to be
an “anchor” space where any shape can be constructed (a playground for computational
constructions). The synthetic space then associates some shapes with a name or a use.

§44.6 When manipulating syntactic objects (in mathematics for instance), both space and time naturally enter in the play together because they have to be materialised by a shape and are subject to (usually sequential) syntactic transformations (which need time). I conjecture that this is why those logico-computational hybrid objects naturally appear everywhere. Logic and computation are constantly and naturally mixed together and derealism studies how the various mixes occur in syntax.

## Globality and locality in logical systems

§44.7 Mathematical logic historically mixed global and local operations. A lot of entities are generic without being defined as such. For instance, theorems of propositional calculus (cf. Section 6) such as $a \Rightarrow a$ are generic. They have the same interpretation for any valuation of $a$. Actually, it could be rewritten as a second-order formula: $\forall X.X \Rightarrow X$. Propositional calculus implicitly uses second-order quantification.
§44.8 In natural deduction, some rules are constructed in a *local* way by juxtaposition of objects already there. Figure 44.1 presents an example of local and global rule. The introduction $\wedge i$ is a typical local rule. We have $A$ and $B$ and put them next to each other to construct an expression $A \wedge B$. Some other rules are *global* or *generic* such as the elimination rule $\vee e$. The elements $A \vee B$, $A$ and $B$ are the elements already there but $C$ is a generic formula. Any formula $C$ can be chosen.

§44.9 **Subformula property and internal explanations.** These generic elements such as the $C$ in $\vee e$ or the $X$ in $\forall X$ invoke the huge *space of all propositions*. However, we cannot tell only from proofs or formulas what this space is made of. This space is externally formatted: this is what we mean by *logical system*. Therefore, generic statement implicitly refer to a system. This is related to the *subformula property* (cf. Paragraph 10.4). This property is a condition for internal explanation. It is preserved by local rule but not by global rules which summon something external. We obtain the following correspondences:

Global = Generic = External

Local = Specific = Internal

In particular, by only considering local rules without any genericity, we have a fully internal explanation of logic which can be expressed out of any system. This is what Girard calls *system-free logic* [Gir20a].

§44.10 This reference to external structures can be found in the second-order equality defining $a = b$ as $\forall X.X(a) \Leftrightarrow X(b)$ (cf. Paragraph 8.7). The variable $X$ refers to the set of all properties. A recurring criticism of Girard is that $X$ cannot refer to properties such as “being on the left of =” or “being on the right =” which would distinguish between the two occurrences of $a$ in $a = a$ and lead to $a \neq a$. But from what basis are we considering those properties logically wrong? An ambition of TS is to make explicit this structuration of the space of all propositions which is assumed in logical systems. This does not contradict “traditional logic” but relativise it by opening it to many choices of formatting the space of all formulas.

§44.11 From all these considerations, Girard adds to TS a distinction between:

* *apodictic*<fnref n="18" /> (first-order logic) in which all rules are local and no reference to external systems exist. It is system-free. We can find connectives such as $\otimes, \mathcal{Y}, \neg$ and limited exponentials;

* *epidictic* (second-order logic) in which we are summoning of the space of all propositions which has to be formatted by a logical system. We can find connectives such as $\oplus, \&,$ $\forall,$ $\exists,$ neutral elements and full exponentials ! and ? (because of the global behaviour of boxes). It appears that $\oplus, \&,$ !, ? and neutral elements can be expressed with $\forall,$ $\exists$ and first-order connectives.

<footnote n="18">¹⁸That Girard compares with anarchy because it works without a system.</footnote>
Note that first-order logic usually means predicate calculus. Girard actually suggests a change of terminology which can be confusing: first-order and second-order logic in TS do not correspond to usual predicate calculus and second-order logic. In particular, because of its genericity, predicate calculus itself is subsumed in Girard's second-order logic (epidictic).

§44.12 The distinction between apodictic and epidictic is close to the distinction between nature and culture<fnref n="19" />. In apodictic, logic is emerging, natural and self-organising. It is where cut-elimination and adequacy are not problematic and where absolute certainty can be expressed. The epidictic is man-made and has to be wisely designed. Certainty is not absolute in this case but only reasonable at best.

## Apodictics / First-order

§44.13 The difficulty of apodictics is to find it. If most logical objects we have are actually epidictic, then what can be apodictic? According to Girard, the only place where apodictics is clearly expressed is in proof-nets. If we take proof-nets without considering the generic nature of atoms/variables, they are indeed purely structural objects. It is only by external considerations that atoms can be replaced by other formula and hence by other proof-nets in the corresponding proof-net. This makes proof-structures independent from any logical system providing we forget genericity.

§44.14 In his fourth paper on TS [Gir20a], Girard defines a formula フ (“fu”) for first-order atoms. By using it, it is possible to establish a purely apodictic fragment of TS. In the same paper, Girard develops an apodictic fragment of TS and suggest notions of truth together with proofs of some axioms of Peano arithmetic.

§44.15 **How is absolute certainty possible?**. Good question. Because we cannot be sure of anything, right? It seems to me that what we mean by absolute certainty is that in the apodictic Usine, there are finitely many tests, orthogonality is computable and the adequacy is simple enough to only rely on simple combinatorics without even relying on parts of mathematics sensitive to incompleteness [Gir17, Section 4.4]. One can argue that it is exaggerated to speak about “absoluteness”. Absolute certainty in Girard’s terminology is a very reliable certainty.

## Epidictics / Second-order

§44.16 Epidictics, because of its implicit external summoning of a system, is harder to justify. In his third article on TS, Girard proposed a way to define epidictics in TS. The structure of the space of all propositions mentioned above is called *epidictic architecture*. It can be defined in both Usine and Usage.

<footnote n="19">¹⁹This nice illustration comes from a discussion I had with Pablo Donato.</footnote>
§44.17 **Case of Usage.** The epidictic architecture for Usage is defined by considering a subspace $\mathfrak{E} \subseteq \mathfrak{S}$. The set $\mathfrak{E}$ has to be closed under a set of connectives $\{C_1, ..., C_n\}$, orthogonal, bi-orthogonal, cut and have to satisfy other essential properties which will be stated later in the thesis and which depends on what we want. Epidictic requires constraints representing the characteristics of the system considered. For instance, in the case of MLL, we can consider a closure under $\otimes$ so that for any $\mathbf{A}$ and $\mathbf{B}$, $\mathbf{A} \otimes \mathbf{B} \in \mathfrak{E}$ and $\mathbf{A}^{\perp} \in \mathfrak{E}$ (which defines the $\mathfrak{S}$ connective): we are closing the space of questions. Although this looks like a limitation, this is what allows generic reasoning (we know what tools and shapes are available). As for quantifiers, they are interpreted with infinite intersection and union of formulas.

§44.18 **Case of Usine: universal case.** In the case of Usine, we have to consider finite tests for second-order quantifiers (which can generate other second-order connectives). In the case of $\forall X.A$, we have to ask a computational object to pass generic tests for all possible cases of formula that $X$ can range over. For instance, in the case of MLL, we have the following generic tests obtained by taking Tests($\vdash A$) and replacing $X$ and $X^{\perp}$:

* $X := \bullet$ and $X^{\perp} := \bullet$;

* $X := \bullet \otimes \bullet$ and $X^{\perp} := \bullet \mathfrak{S} \bullet$;

* $X := \bullet \mathfrak{S} \bullet$ and $X^{\perp} := \bullet \otimes \bullet$;

where $\bullet$ represents an atomic formula (this will be clearer when defining the actual interpretation in stellar resolution later in this thesis).

§44.19 **Case of Usine: existential case.** For $\exists X.A$, we have to design tests but it is impossible to foresee what the existential witness will look like. However, in proof theory, the existential witness comes with the proof. This is where the derealist approach is exploited: testing is usually opposing a computational object $\Phi$ against a test $\Psi$. However, the computational object now comes with a test $\Psi_T$ (called *mould*) for the existential witness $T$. We then test the union $\Phi \uplus \Psi_T$ against $\Psi$.

§44.20 **Difference between synthetics and epidictic.** Epidictic is indeed a formatting of computational objects. But then, how does it differ from synthetics? Synthetics is defined with a point of view (orthogonality) and tests (which can be finite or infinite). Epidictics is about meaning where synthetics is not sufficient. Typically, how to express that we “link dual atoms”? We need a human intervention to distinguish atoms and their dual and add the constraint that they must be linked in axioms.

**An original proposal: epidictic and apodictic models of computation**

§44.21 Remember that I claim that models of computation are actually logical. If the analytic space $\mathfrak{A}$ is the space of answers, then enforcing specific shapes and handling of objects of $\mathfrak{A}$ has consequence over the synthetic/logical space $\mathfrak{S}$. If we start from the lawless world of $\mathfrak{A}$ and try to define an automata or a circuit, we must define a starting point (initial
state or inputs) and describe how information flow in the structure (synchronised doors for circuits and linear run for automata). It makes models of computation restrictions over the space of information flows within a structure.

§44.22 An interesting idea which will be illustrated later in this thesis, is to first find what all classical models of computation have in common and then understand what makes their identity. I claim that we can distinguish between apodictic and epidictic models of computation.

§44.23 Apodictic models of computation are those which are self-organising and autonomous. Typically, tile systems such as Wang tiles are self-interacting objects with no external control. They only interact locally w.r.t. their primitive structures (colours on edges). Other examples such as the abstract tile assembly model with cooperating tiles (used in DNA computing) will be presented in this thesis.

§44.24 Epidictic models of computation are those who need human intervention or external control. Typically, in a lawless world, we could start from the final state and loop eternally without consuming a word. There is a right path to take and we have to enforce it to lawless objects of $\mathfrak{A}$. This control over computation can be related to focussing in linear logic (cf. Paragraph 28.7).

§44.25 An interesting question is whether external control can always be internalised, i.e. is epidictic reducible to apodictic. My conjecture is that the answer is negative. But it is still interesting to study those cases in which control can be internalised (it is the case of “cooperative” tile systems).

**45 Illustration: Transcendental Syntax applied to lambda-calculus**

§45.1 The architecture of TS is not made for the $\lambda$-calculus but we can try to apply it to $\lambda$-terms in order to illustrate the ideas of this chapter$^{20}$.

§45.2 **Analytic of lambda-calculus.** For the analytic space, we can either choose Krivine's $\lambda_c$-terms and stacks (cf. Section 22) or Riba's $\lambda$-terms and contexts (cf. Section 22). I choose Riba's interpretation leading to simple types. We have $\mathfrak{A} := \Lambda \cup E$. Constat is the set of all normal terms extended with contexts. Performance are redexes and we consider $\beta$-reduction with any strategy. Note that TS splits $\lambda$-terms themselves into vehicle and tests in a homogeneous monist space.

§45.3 **Synthetic of lambda-calculus.** Usage corresponds to Riba's realisability interpretation which can reconstruct simple types as behaviours. Although simple types are constructed, the interpretation is open to more types by choosing another orthogonality

<footnote>$^{20}$This is something Pablo Donato wanted to see because he wanted to find a better way to explain and communicate ideas of TS without depending on Girard's formalisms. It would also be a way to make TS more acceptable in front of the community of logic in computer science.</footnote>
<figure><img src="image_84.png" /><figcaption>Figure 46.1: Relations between the four cases of Girard’s cognitive knitting.</figcaption></figure>

relation. Usine defines tests by finite sets of either terms or contexts. However, is it
always possible to guarantee membership in a type by a finite set of tests? How to
finitely check whether $M \in \alpha \Rightarrow \beta$ for some primitive types $\alpha$ and $\beta$? Moreover, in TS,
contexts should be testable as well: everything should be justified. It seems that this
space of testing is rather weak: it looks like the interpretation is not able to characterise
a lot of interesting computational behaviours.

§45.4 **Apodictic and Epidictic of lambda-calculus.** We can now imagine what the apo-dictic fragment of our TS interpretation of $\lambda$-calculus would look like. The idea of the epidictic is to restrict $\mathcal{A}$. We could for instance restrict to linear $\lambda$-terms by allowing only terms having exactly one occurrence of their argument. However, this does not translate in the synthetic space $\mathcal{S}$: we cannot restrict the set of all behaviours so to obtain linear logic because interaction between terms and contexts is not expressive enough.

**46 Discussion: is it a right understanding of logic?**

§46.1 A fair question I encountered about TS is “why should we believe it is the right way to understand logic?”. The TS is not meant to be *the* right answer to the foundation of logic. It does not even assume the possibility to directly access to the “true” content of logic but only to access a representation of it through a subjective medium (a choice of model of computation) as explained in Paragraph 39.14. However, it provides an interesting and different way to look at logic and computation.

§46.2 **Solid foundations.** The architecture of TS is grounded on two unavoidable limits:

• *undecidability* splitting analytics by separating Constat and Performance;

• *incompleteness* splitting synthetics by separating Usine and Usage.
The four cases of the cognitive knitting are also linked with well-known central notions:

* *execution* linking Constat and Performance;

* *cut-elimination* linking Usine and Usage.

These relations are illustrated in Figure 46.1. It shows that TS lies on cold and down-to-earth facts and not abstract ideals. On the technical side, TS is based on GoI which succeed a series of analysis from natural deduction to proof-nets. In TS, one still wish for as much conservativity as possible by rescuing as many concepts and results of mathematical logic (but not necessarily all). Hence, TS is more about reorganising the notions we already know and putting order in mathematical logic.

§46.3 **The three layers of logic and computation.** Explanations of how logic works in transcendental syntax do not need an infinite hierarchy of semantic level as in the usual linguistic spiral. Here we only have three layers:

* the analytic space $\mathfrak{A}$;

* the synthetic space $\mathfrak{S}$ which constraints the space of answers;

* a chosen *epidictic architecture* which constraints the space of questions (we choose what questions can be asked).

The *epidictic architecture* is a sort of meta-level above the relationship between analytic (object) and synthetic (subject) in logic. Although the expression “meta” is taboo in Girard’s papers, it is not always problematic. We can, for instance, speak about *metapolitics* without any problem. The problem with the theory of metalogic is that we were barely touching what logic was really about. Metalogic did not say a lot of things about the mechanisms of logic. Hence, although we can argue that transcendental syntax still lives in some (mathematical, combinatorial or syntactical) metatheory, it is something we can tolerate. In the same fashion, computer scientists can build tools (programs), make them work and check whether they fit some specification (with a reasonable degree of reliability) without ending in a conceptual maze.

§46.4 In the next chapter, I formally present the stellar resolution which serves as a computational ground for TS. The chapter will be followed by a chapter thoroughly demonstrating the computational expressivity and power of stellar resolution in order to show that it is a model of computation of interest by itself.
# Chapter 7

## Stellar resolution

I refer to Appendix B for definitions related to term unification. These definitions are necessary to understand the definitions of this chapter.

Stellar resolution is the model of computation used as a computational ground for transcendental syntax. It can be understood from several different points of view:

* it is a *n*-ary generalisation of Girard's model of flows and wirings (cf. Section 37);

* it is a flexible tile system (cf. Section 17) based on term unification and Robinson's resolution (cf. Section 23);

* it is an extension of Robinson's resolution with disjunctive clauses (cf. Section 23) (on which logic programming is based);

* in a more conceptual way, it is a model of computation describing computation as pieces of information flowing inside a graph-like structure.

As we will see, stellar resolution actually generalises several models of computation such as: automata, circuits, logic programs, functional programs (by their translation to proof-nets), tile systems and more. I named it “stellar resolution” in reference to Girard’s terminology of stars and constellations and for its link with usual first-order resolution<fnref n="1" />. At the end of the chapter, comparisons with ideas of logic programming are made.

The idea is that objects of stellar resolution will encode proof-structures. The interpretation is similar to the one of flows and wirings but the difference is that whereas flows are able to represent the long trip correctness criterion, stellar resolution naturally interprets the Danos-Regnier correctness criterion.

<footnote n="1">¹But the main reason is because the name sounds pretty cool.</footnote>
<figure><img src="image_85.png" /><figcaption>(a) Lone star. Poor guy has no friend.</figcaption></figure>

<figure><img src="image_86.png" /><figcaption>(b) The star finds a partner and interact with it. They form a finite diagram. They communicate through dual rays.</figcaption></figure>

<figure><img src="image_87.png" /><figcaption>(c) Another star is added to the diagram. The diagram gets bigger.</figcaption></figure>

Figure 47.1: Connexion of stars.

# 47 Intuition behind stellar resolution

§47.1 In this section, I present the informal intuition behind the model of stellar resolution. The intuition can be understood from several ways depending on your background (as stated in the introduction). You may see it as logic programming, flexible tile system or extension of flows in GoI. Formal definitions are given in the next section. It is necessary to have knowledge on term unification (cf. Appendix B) and graph theory (cf. Appendix C) to understand this chapter.

§47.2 Figure 47.1a illustrates a star, which is a sort of flexible tile holding terms. It can also be written as a non-ordered finite sequence of terms [$X, +f(X), -h(Z, X)$] where some function symbols are polarised (in ${+,-}$) or not. Several stars form a constellation. In a constellation, stars can interact by connecting to each other along dual rays as in Figure 47.1b. Dual rays are those rays which are polarised with opposite polarity (+ against −) and which are unifiable up to renaming (what I call α-unification), considering the compatibility relation $\subset$ between potentially polarised function symbols. Connecting stars along rays allows to construct tilings called *diagrams*. As shown in Figure 47.1c it
$$ \begin{array}{c} [g(X), +a(X), -b(X)] \\ \big/ \\ [-a(f(Y)), +c(Y)] \end{array} $$

(a) Step 1: we have two stars connected along two rays in a diagram.

$$ \theta = \left. \begin{array}{l} [g(X), +a(X), -b(X)] \\ [a(f(Y)), +c(Y)] \end{array} \right\} $$

(b) Step 2: we choose a link to contract and compute the solution associated with its equation.

$$ [g(X), -b(X), +c(Y)] $$

(c) Step 3: the two stars interact by merging and erasing the rays related to the link.

$$ [g(f(Y)), -b(f(Y)), +c(Y)] $$

(d) Step 4: the solution $\theta$ of the link is propagated to the resulting star.

Figure 47.2: Evaluation of diagrams by resolution. The two terms $+a(X)$ and $-a(f(Y))$ are dual and then can be connected to form a diagram.

is possible to construct bigger diagrams involving more stars. We are usually interested in connected and saturated diagrams which are diagrams which cannot be extended by connecting more stars to the diagram.

**§47.3 Dynamics.** Now that we have diagrams, it is possible to evaluate them by an edge contraction merging stars by annihilating the connected rays and propagating the solution of their equation to other rays. The steps of this evaluation are presented with an example in Figure 47.2. The execution of a constellation evaluates all possible connected and saturated diagrams. It is a generalisation of the execution of wirings.

**§47.4** It is possible to imagine two ways of executing constellations. One we just described which constructs tilings and evaluates them. It has an *abstract* version which is more of a denotational nature and does not say how to construct tilings (they just mathematically pop out) and a *concrete* version which iteratively constructs diagrams. Another way called *interactive execution* starts from some stars and successively adds stars which directly interact on the fly with the available stars. It can be implemented more easily and
is more faithful to classical computation but do not exactly correspond to the previous
natural notion of execution.

## 48 Stars and constellations

**§48.1** Tiles are called stars and their flexible arms are *rays*. A tile set is called a *constellation*. Rays can contain special polarised function symbols analogous to the colours of Wang tiles. For instance, $+f$ and $-f$ are two *dual* terms. We expect terms such as $+c(f(X))$, $f(X)$, $Y$, $+d(X, -e)$ and $+c(f(+f(X), Y))$ to be rays.

**§48.2** **Definition (Polarised signature).** A *polarised signature* is a tuple

$$ \mathbb{P} = (V, F, \mathbf{ar}, \prec, \lceil \cdot \rceil) $$

where $(V, F, \mathbf{ar}, \prec)$ is a signature (cf. Appendix B). The set $F$ is defined as a partition $F_+ \uplus F_- \uplus F_0$ defining presence (polarity $+$ and $-$) or absence (polarity $0$) of polarities over symbols. Function symbols of $F_+ \uplus F_-$ are said to be *coloured* (or polarised) and those of $F_0$ are *uncoloured* (or neutral).

The *underlying symbol* of a function symbol is defined by a function $\lceil \cdot \rceil : F \to F_0$ satisfying the following requirements:

* $f = \lceil f \rceil$ for $f \in F_0$;

* the restriction of $\lceil \cdot \rceil$ to $F_+$ (resp. $F_-$) is bijective, hence every neutral element of polarity $0$ has a positive and negative version.

We define two maps attaching polarities to function symbols:

* $+$: $F_0 \to F_+$;

* $-$: $F_0 \to F_-$;

such that $+$ and $-$ are inverse of $\lceil \cdot \rceil$, i.e. for all $r$, we have $\lceil +r \rceil = r$ and $\lceil -r \rceil = r$.

Finally, the compatibility relation $\prec$ is defined by $c \prec d$ if and only if $\lceil c \rceil = \lceil d \rceil$ and one of the following requirements hold:

* $c \in F_+$ and $d \in F_-$;

* $c \in F_-$ and $d \in F_+$;

* $c \in F_0$ and $d \in F_0$

**§48.3** **Definition (Opposite).** We first define the *opposite* $\text{op}(f)$ of a function symbol. If $f \in F_0$ then $\text{op}(f) = f$. If $f \in F_+$ then $\text{op}(f) = -\lceil f \rceil$ and if $f \in F_-$ then $\text{op}(f) = +\lceil f \rceil$.
We define the opposite $\mathbf{op}(r)$ of a polarised ray $r$ by:

$$ \mathbf{op}(c(r_1, \dots, r_n)) = \mathbf{op}(c)(\mathbf{op}(r_1), \dots, \mathbf{op}(r_n)). $$

**§48.4** **Example.** Let $\mathbb{P} = (V, F, \mathbf{ar}, \prec, \lceil \cdot \rceil)$ be a polarised signature with $V = \{X\}$ and $F = F_0 \uplus F_+ \uplus F_-$ such that $F_0 = \{c, d\}$, $F_+ = \{+c, +d\}$ and $F_- = \{-c, +d\}$ (we omit arity). We have $+c \prec -c$ and $+d \prec -d$.

**§48.5** **Convention.** We assume the existence of a polarised signature $\mathbb{P} = (V, F, \mathbf{ar}, \prec, \lceil \cdot \rceil)$ unless we explicitly use a specific one.

**§48.6** **Internal colours.** Unlike the simplified description of the previous section, rays are not simply defined as terms with a polarity as prefix. For the interpretation of simple fragments of linear logic such as MLL, it is sufficient to consider polarised terms which indeed correspond to first-order atoms but if we are interested in interpreting Girard's second-order logic (epidictics), then rays with internal colours must be used [Gir18b, Section 4.1] (making it far more complicated than the dynamics of logic programming). The intuition is that rays with internal colours will be used for the interpretation of moulds (cf. Paragraph 44.19). Because these two class of rays are both used in different context, we will explicitly distinguish them.

**§48.7** **Definition (Rays).** A ray on a signature $\mathbb{P} = (V, F, \mathbf{ar}, \prec, \lceil \cdot \rceil)$ is a term $r \in \text{Term}(\mathbb{P})$ constructed with variables in $V$ and function symbols in $F$.

A ray $r$ is *coloured* if it contains a colour and it is *uncoloured* otherwise.

The underlying term of a ray is defined inductively as follows:

$$ \lfloor X \rfloor = X \qquad \lfloor c(r_1, \dots, r_n) \rfloor = \lfloor c \rfloor (\lfloor r_1 \rfloor, \dots, \lfloor r_n \rfloor) $$

with $x \in V$ and $c \in F$.

Let $r$ be a ray. It is either:

* *objective* if it is either uncoloured or it is a coloured ray $r = c(r_1, \dots, r_n)$ such $c$ is coloured and $r_1, \dots, r_n$ are uncoloured. They correspond to uncoloured terms prefixed by a colour;

* or *subjective* otherwise, if it is a coloured ray $r = f(r_1, \dots, r_n)$ such that at least one ray of $\{r_1, \dots, r_n\}$ is coloured.

**§48.8** **Definition (Set of colours of a ray).** The set of colours appearing in a ray is defined by:

* $\mathbf{colours}(t) = \emptyset$ if $t$ is uncoloured;

* $\mathbf{colours}(c(r_1, \dots, r_k)) = \{c\} \cup (\bigcup_{1 \le i \le k} \mathbf{colours}(r_i))$ if $c \in F_+ \uplus F_-$ and $k \in \mathbb{N}$;
<figure><img src="image_88.png" /><figcaption>Figure 48.1: Objective star with rays seen as either input, output or unpolarised.</figcaption></figure>

• `colours(f(r₁, ..., rₖ)) = (U₁≤i≤k colours(rᵢ))` otherwise.

**§48.9 Example.** Examples of objective rays are: `+c(X)`, `f(X, Y)` and `−d(h(X))`. Examples of subjective rays are `f(X, +h(Z))`, `+c(+d, −c(Y))` and `+c(−d(+h(X, Y)))`. We have `colours(+c(−d(+h(X, Y)))) = {+c, −d, +h}`.

**§48.10 Definition (Star).** A star $\phi$ over a polarised signature $\mathbb{P}$ is a finite indexed family (cf. Appendix A.2) of *rays* (Term($\mathbb{P}$), $I_{\phi}$, $\phi[\cdot]$). The set of variables appearing in $\phi$ is defined by `vars(\phi) := \bigcup_{i \in I_{\phi}} vars(\phi[i])$. For convenience, stars will be written as an unordered sequence $[r_1, ..., r_n]$.

The empty star is written `[]` and is defined by the set of indexes $I_{\emptyset} = \emptyset$.

Let $\phi = [r_1, ..., r_n]$ be a star. It is either:

• *objective* if $r_1, ..., r_n$ are objective;

• *subjective* if $r_1, ..., r_n$ are subjective<sup>a</sup>;

• or *animist*<sup>b</sup> otherwise (it has at least one objective and one subjective ray).

The shape of objective stars in illustrated in Figure 48.1.

**§48.11 Definition (Substitution applied on a star).** Let $\theta$ be a substitution (cf. Appendix B) and $\phi$ a star. The application of $\theta$ on $\phi$ is defined by a star $\theta\phi$ with $I_{\theta\phi} := I_{\phi}$ and $(\theta\phi)[i] = \theta\phi[i]$.

**§48.12 Definition (Alpha-equivalence of stars).** We say that two stars $\phi_1$ and $\phi_2$ are $\alpha$-equivalent, written $\phi_1 \approx_{\alpha} \phi_2$, when there exists a renaming $\alpha$ (cf. Appendix B) such that $\phi_1 = \alpha\phi_2$.

**§48.13** In this thesis, stars will be considered up to $\alpha$-equivalence. We therefore define `Star(\mathbb{P})` as the set of all stars over a polarised signature $\mathbb{P}$, quotiented by $\approx_{\alpha}$.

<footnote><sup>a</sup>I asked Girard what was the point of internal colours and he answered me “Ça ne sert à rien du tout” which means (in French) that it was totally useless. He then told me that he just needed a trick so to make sublocations of subjective rays subjective as well. My point of view is that it adds more combinatorics to express truth and meaning. In particular, correct proofs require a clear separation between fully subjective and fully objective stars.</footnote>

<footnote><sup>b</sup>Because it mixes object and subject.</footnote>
§48.14 **Definition (Constellation)**. A constellation $\Phi$ is a countable indexed family of stars (Star($\mathbb{P}$), $I_{\Phi}$, $\Phi[\cdot]$) with a possibly infinite set of indexes $I_{\Phi}$. For convenience, a finite constellation will be written as a sum of stars $\Phi = \phi_1 + \dots + \phi_n$.

We define the set of rays of a constellation $\Phi$ by $\text{IdRays}(\Phi) = \{(i, j) \mid i \in I_{\Phi}, j \in I_{\Phi[i]}\}$ (we keep track of the instance of star from which rays come) and $\pm\text{IdRays}(\Phi) := \{r \in \text{IdRays}(\Phi) \mid r \text{ is coloured}\}$ by its restriction to coloured rays.

The empty constellation is written $\emptyset$ and is defined by $I_{\emptyset} = \emptyset$.

§48.15 Constellations are meant to be sort of programs. As in logic programming (e.g. Prolog) or functional programming (e.g. $\lambda$-calculus), variables will be considered bound to their star (which can be seen as sort of declarations), hence the two $x$ in $[+f(x)] + [-f(x), y]$ are unrelated. This is similar to how the two $x$ in the $\lambda$-term $\lambda x.(\lambda x.M)$ are different.

§48.16 Now that all the elementary objects of the stellar resolution are defined, we give a very standard encoding of natural numbers which will be useful.

§48.17 **Definition (Encoding of natural numbers)**. We define the function symbol $\overline{n}$ for a natural number $n \in \mathbb{N}$ by $\overline{0} = 0$ and $\overline{n+1} = s(\overline{n})$ for a unary symbol $s$ and a constant $0$.

§48.18 **Example**. We give examples of finite and infinite constellations:

• $\Phi_N^+ := [+add(\overline{0}, Y, Y)] + [-add(X, Y, Z), +add(s(X), Y, s(Z))]$ (logic program for addition);

• $\Phi_N^{n+m} := \Phi_N^+ + [-add(\overline{n}, \overline{m}, R), R]$ (query for the computation of $n+m$);

• $\Phi_N$ is defined by $I_{\Phi_N} = \mathbb{N}$ and $\Phi_N[i] := [-nat(\overline{i}), +nat(\overline{i+1})]$ (infinite chain)

over the signature defined by the variables $V = \{X, Y, Z, R\}$, the symbols $F = \{+add, -add, add, +nat, -nat, nat, s, 0\}$, $\mathbf{ar}(add) = 3$, $\mathbf{ar}(nat) = \mathbf{ar}(s) = 1$, $\mathbf{ar}(0) = 0$. The constellation $\Phi_N^{n+m}$ corresponds to the following Horn clauses [Tär77] where $Add(X, Y, Z)$ states that $X + Y = Z$:

$$ \mathit{Add}(0, Y, Y) \quad \text{and} \quad \mathit{Add}(X, Y, Z) \Rightarrow \mathit{Add}(s(X), Y, s(Z)). $$

## 49 Abstract execution

§49.1 The first method of computation constructs tilings and evaluate them. In order to do so, we first construct a dependency graph showing how rays can be linked. Diagrams are extracted from this dependency graph by unfolding loops by using hypergraph homomorphisms. This method is purely mathematical and not effective. It does not say how to actually construct diagrams. In particular, it is *always* defined. Even when there are infinitely many diagrams, they do not appear at all in the result. The method is not
<figure><img src="image_89.png" /><figcaption>Figure 49.1: Example of finite deterministic automaton with a mapping from a word graph to its state graph.</figcaption></figure>

bothered by actual infinity. It makes abstract execution something of a *denotational* nature, similar to the denotational semantics of programming languages interpreting programs as mathematical objects.

## Evaluation of diagrams

§49.2 We are now interested in the formation of *diagrams* which correspond to tilings of stars (without any planarity constraints). Unlike tilings with Wang tiles or flexible tiles, it is possible to evaluate these diagrams by an edge contraction using Robinson's resolution rule (cf. Section 23).

§49.3 We first define the *dependency graph* of a constellation which defines the allowed connections between stars along dual rays. A diagram corresponds to an actual plugging of stars along dual rays, following those allowed connexions. The edges linking stars will induce an equation between terms and the whole diagram will induce a unification problem. The *evaluation* of a diagram will correspond to solving its associated unification problem and producing a new star.

§49.4 In order to approach this idea more intuitively, we explain a common occurrence of it in automata theory. A finite deterministic automaton is a machine reading an input word character by character. It starts from an initial state and moves from a state to another accordingly to the current character it reads. If it ends on the final state, it *accepts* the input word. Otherwise, it rejects the input. An example of automaton of final state $q_2$ is given in Figure 49.1 (on the top with vertices $q_0, q_1, q_2$). A word can be represented as a linear graph (on the bottom with vertices 1, 0, 1, 0 and 0) and finally, the reading of a word can be represented as a mapping from characters to states (links between the word graph and the state graph).
§49.5 The state graph of the automaton shows the allowed transitions (where loop can appear) and the word graph can be seen as tiling of states or a traversal of graph which follows those allowed transitions (sometimes by unfolding loops).

§49.6 Our diagrams generalise this idea. The state graph corresponds to a dependency graph and the word graph corresponds to a diagram. The difference is that a dynamics of term unification is present in our dependency graphs and diagrams can be any graph, not necessarily limited to the linear case as for automata. Mathematically speaking, a diagram will be associated with a graph homomorphism between a graph (representing the tiling) and the dependency graph, exactly like how word graphs are related to state graphs in automata theory.

§49.7 **Definition** (Duality between rays). Two polarised rays $r$ and $r'$ are dual or matchable written $r \bowtie r'$, when $r$ and $r'$ are $\alpha$-unifiable (with the compatibility relation $\subset$ for rays).

§49.8 **Proposition**. The relation $\bowtie$ is symmetric but anti-reflexive and anti-transitive.

*Proof.* Symmetry follows from the symmetry of $\alpha$-unifiability (cf. Lemma B.1.14). We show the two other statements.

* We cannot have $r \bowtie r$ since $r$ and $r$ have same polarities and two function symbols of same polarity cannot be compatible by $\subset$.

* Assume that $r_1 \bowtie r_2$ and $r_2 \bowtie r_3$. It means that $r_1$ and $r_2$ are of opposite polarities and so are $r_2$ and $r_3$. Since there are only two polarities (+ and $-$), $r_1$ and $r_3$ must have same polarities. Hence they cannot be dual (by definition of $\subset$).

□

§49.9 **Example**. We have $+c(X) \bowtie -c(0)$ and $-d(X) \bowtie +d(f(X))$ but not $+c(X) \bowtie f(Y)$ (presence of unpolarised ray), $+c(X) \bowtie -d(X)$ (different head symbol), $+c(X) \bowtie +c(f(Y))$ (polarities are not opposite) nor $+c(f(X)) \bowtie -c(g(Y))$ (terms are not $\alpha$-unifiable).

§49.10 **Definition** (Dependency graph). The *dependency graph* of a constellation $\Phi$ w.r.t. a set of colours $C \subseteq F_+ \uplus F_-$ is a multigraph (cf. Definition C.3.1)

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

where:

* $V := I_{\Phi}$ (the indexes of stars in $\Phi$);

* edges between two stars of index $i$ and $i'$ are unordered pairs $\{(i, j), (i', j')\}$ such that for $r := \Phi[i][j]$ and $r' := \Phi[i'][j']$:
<figure><img src="image_90.png" /><figcaption>Figure 49.2: Examples of dependency graphs for constellations of Example 48.18.</figcaption></figure>

<figure><img src="image_91.png" /><figcaption>Figure 49.3: Examples of diagrams for the constellation $\Phi_N^{2+2}$. The number of occurrences of $\phi_2$ corresponds to the number of recursive calls. They correspond to unfolding of the loop of Figure 49.2 corresponding to the possibility of recursive call.</figcaption></figure>