Moreover, names are not so relevant since $\lambda x.x$ is equivalent to $\lambda y.y$. There are two classical solutions to avoid conflicts of variables:

* to use a rule called $\alpha$-conversion which allows to rename bound variables. This rule (which defines an equivalence relation called $\alpha$-equivalence) is defined by:

$$ \lambda x.M \equiv_{\alpha} \lambda y.\{x := y\}M $$

for any variable $y$. We would then have $\lambda x.M(\lambda x.N) \equiv_{\alpha} \lambda x.M(\lambda y.\{x := y\}N)$ and $\lambda x.x \equiv_{\alpha} \lambda y.y$;

* another solution suggested by De Bruijn<fnref n="11" /> is to use relative indexes. Instead of variable names and $\lambda x$, we would have natural numbers and a nameless $\lambda$. Natural numbers, called De Bruijn indexes, refer to the distance (to the left) of the $\lambda$ symbol they are linked to. For instance, $\lambda x.M(\lambda x.N)$ would be rewritten $\lambda M'(\lambda N')$. Any 1 in $N'$ is linked to the second $\lambda$ and any 2 is linked to the first $\lambda$. The left projection $\lambda x.\lambda y.x$ would simply be written $\lambda\lambda 2$. Note that when we say that these indexes refers to a distance, we are not speaking about literal distance in terms of characters but in term of scope. For instance, in the term $\lambda(\lambda 1(\lambda 1))(\lambda 21)$, the index 2 actually refers to the first $\lambda$.

§15.12 It is possible to consider recursion in $\lambda$-calculus (which can be seen as a way to loop in a program by calling itself) by using fixpoint operators. A fixpoint of a function $f$ in mathematics is a value $c$ such that $f(c) = c$. Fixpoint operators of $\lambda$-calculus are $\lambda$-terms fix such that fix $F$ reduces to $F$. A common fixpoint operator is the $Y$ operator defined by:

$$ Y := \lambda f.(\lambda x.f(xx))(\lambda x.f(xx)) $$

which can be used to define the factorial function $f(x) = x! = \prod_{i=2}^{x} i$. The template for any recursive function is to define a function $\lambda f.\lambda n.M$ where $f$ will correspond to the recursive call (which is a necessary trick since we cannot refer to the function being defined), $n$ is the argument of the function and $M$ is the body of the function. For the factorial function, we have

$$ F := \lambda f.\lambda n.\text{cond} (\text{is\_zero } n) \bar{1} (f (n - 1)). $$

We assume the existence of a subtraction operator on $\mathbb{N}$ such that $0 - 1 = 0$. We define $\text{fact} := Y F$ and we have the following reduction:

$$ \text{fact} = Y F \rightsquigarrow_{\beta} (\lambda x.F(xx))(\lambda x.F(xx)) $$

$$ \rightsquigarrow_{\beta} F((\lambda x.F(xx))(\lambda x.F(xx))) = F(YF) = F\text{ fact} $$

<footnote n="11">¹¹There are a lot of confusions about how to pronounce this name. I suggest that you listen to the pronunciation at least one.</footnote>
The notion of (simple) type

§15.13 Type theories have been introduced in logic mainly for the purpose of avoiding paradoxes making logical systems contradictory. Russell and Whitehead in particular contributed to the developments of these theories (cf. Paragraph 3.4). Since Church's system was originally a logical system, type theory can be applied to it. According to Hammache [Ham21, Section 9.1.1], Church wanted to keep the computational power of his system so he did not introduce typed λ-calculus for the only purpose of avoiding paradoxes. He especially wanted to constrain the space of λ-terms to a relevant subset such as the subset of normalisable terms. Church's type theory is a theory of control of computation.

§15.14 Church's original type theory [Chu40] has the following grammar of types:

$$ \alpha, \beta ::= \quad \iota | \ o | \alpha\beta \qquad \text{(Types)} $$

where $\iota$ is the type of individuals, $o$ is the type of propositions and $\alpha\beta$ is the type of functions from the type $\beta$ to the type $\alpha$ (a function type applied to an argument type). Types are directly integrated within λ-terms with the following grammar:

$$ M_{\alpha}, N_{\alpha} ::= \quad x | \lambda x_{\beta}. M_{\alpha} | (MN)_{\alpha} \qquad \text{(Terms)} $$

where $\lambda x_{\beta}.M_{\alpha}$ is of type $\alpha\beta$, and in $(MN)_{\alpha}$, $M$ is of type $\alpha\beta$ and $N$ of type $\beta$. The reduction now takes types into account:

$$ (\lambda x_{\beta}.M_{\alpha})_{\alpha\beta}N_{\alpha} \rightsquigarrow_{\beta} \{x := N\}M_{\beta} $$

Notice that types have a functional notations, exactly like λ-terms. It suggests the idea that types themselves can behave like functions as well. This elementary type system, now known as simple types is sufficient to exclude unwanted terms. For instance, the term $\lambda x.xx$ cannot be typed:

* it has to be of type $\alpha\beta$ because it is a function. We have the partial typing $\lambda x_{\beta}.(xx)_{\alpha}$;

* having $(xx)_{\alpha}$ implies that we must have the left $x$ of type $\alpha\alpha'$ and the right $x$ of type $\alpha'$;

* however, a same variable $x$ cannot be both of type $\alpha'$ and $\alpha\alpha'$, this is contradictory.

This term was not so innocent anyway, since it can form $(\lambda x.xx)(\lambda x.xx)$ which is known to normalise into itself and hence corresponding to an infinite loop.

§15.15 **Application in linguistics.** This is rather anecdotal in this thesis but I just would like to mention that Church's original type theory has applications in linguistics. Montague grammar for instance, makes use of λ-calculus and higher order predicate calculus to express meaning in natural language. A verb phrase (VP) such as "The man is walking"
$$ \overline{\Gamma, x : A \vdash x : A} \quad \text{var} \quad \frac{\Gamma, x : A \vdash M : B}{\Gamma \vdash \lambda x.M : A \to B} \quad \text{abs} \quad \frac{\Gamma \vdash M : A \to B \quad \Gamma \vdash N : A}{\Gamma \vdash MN : B} \quad \text{app} $$

<caption>Figure 15.2: Typing rules for simply typed λ-calculus.</caption>

$$ \begin{array}{ccc} \overline{x : \alpha, y : \beta \vdash x : \alpha} & \text{var} & \\ \frac{x : \alpha \vdash \lambda y.x : \beta \to \alpha}{\vdash \lambda x.\lambda y.x : \alpha \to \beta \to \alpha} & \text{abs} & \\ & \text{abs} & \end{array} $$

<caption>Figure 15.3: Typing derivation for a λ-term.</caption>

for instance is of type $\iota \to o$, it takes a subject (the man) and turns it into a proposition. It shows that types can also speak about the behaviour of computational entities.

§15.16 Curry considers untyped λ-terms as independent from types. We write $M : A$ for a type $M$ of type $A$. Types are written $A, B$ and atomic type variables $\alpha, \beta$ are considered instead of $\iota$ and $o$. We have the following grammar for types:

$$ A, B ::= \alpha, \beta, \dots | A \to B \qquad (\text{Terms}) $$

To still represent the fact that typed λ-terms cannot exist without types, the construction of terms have to be constructed by some rules. These rules use the notation of sequents of Paragraph 9.9. A sequent is an expression asserting the type of an expression. The sequent $\Gamma \vdash M : A$ says that the term $M$ is of type $A$ for a context or typing environment $\Gamma$ made of type assertions $x_1 : A_1, \dots, x_n : A_n$. The typing rules are given in Figure 15.2. Using typing rules, it is possible to construct trees exactly like we do in proof theory. The typing derivation of Figure 15.3 guarantees that $\lambda x.\lambda y.x$ can be attached to the type $\alpha \to \beta \to \alpha$.

§15.17 Types can be seen as constraints over computation so to prevent some behaviours from happening, but they also express a computational behaviour. A type derivation is a very important object since it acts like a certificate for a computational behaviour. The existence of such a certificate ensures that our computational object will have a specific behaviour and not another unexpected one. After Church, a lot of type systems have been developed in order to capture other behaviours. For instance, intersection types are able to give several types to terms so that the $x$ in $\lambda x.xx$ (which terminates) can be typed with the intersection $\langle A \to B, A \rangle$ because it acts both as a function and as an argument. It is also possible to extend λ-calculus with other constructions such as pairs $(M, N) : A \times B$ with $M : A$ and $N : B$.
<figure><img src="image_15.png" /><figcaption>Figure 16.1: Transition in a tape for a Turing machine.</figcaption></figure>

# 16 Computation as state machine

My references for this section are Petzold's book "The annotated Turing"<fnref n="12" /> (which is a commentary on Turing's seminal paper) and Sipser's introduction to the theory of computation [Sip06] for formal definitions.

## The mathematician-machine

§16.1 Alan Turing is without doubt one of the most famous figures of computer science. During his youth, it seems that Turing was fascinated by machines and more especially with their relation to the human mind [Pet08, Chapter 4]. Already interested in science as a young student, Russell's work on mathematical logic caught his interest very early. Hilbert's decision problem came to him through a course of Maxwell Herman Alexander Newman that he took in 1935. At this time, the idea of *mechanical process* did not refer to machines. This is after this course that he began to work on Hilbert's problem. He tried to design a machine which would reproduce the steps done by a mathematician. His machine could compute numbers in binary form (only with 0 and 1) but also well-known mathematical constants such as $\pi$ and $e$. More than that, he also designed a *universal machine* able to simulate the operations of another machine, exactly like how a program (such as a compiler) would read another program in today's programming. Turing was an independent researcher in the beginning<fnref n="13" />, which is probably part of why he came up with this unusual solution. Church already published about this problem at this time but his works were very connected to the literature, unlike Turing. This interests led to a collaboration with Church himself who became his PhD advisor.

§16.2 To quote Turing himself, his machines [Tur36] (now called *Turing machines*) consist of a “tape” (representing a piece of paper) divided into sections called “squares”. Each square can bear a symbol, and the machine can read the square of a tape and move to the left or to the right. Turing says that a square read by the machine is a *scanned square* which is the only square the machine is aware of. The design was motivated by the *use* of machines (e.g. computing numbers). A machine can be in a specific state

<footnote n="12">¹²One of the first books about computer science I have read!</footnote>

<footnote n="13">¹³According to Petzold's book, he even reinvented the binomial theory and developed his own notation for calculus.</footnote>
<table><caption>Figure 16.2: Transition table for a Turing machine.</caption><thead><tr><th colspan="2">Configuration</th><th colspan="3">Behaviour</th></tr><tr><th>State</th><th>Symbol read</th><th>Symbol written</th><th>Movement</th><th>New state</th></tr></thead><tbody><tr><td>q</td><td>0</td><td>1</td><td>right</td><td>q'</td></tr><tr><td>q'</td><td>0</td><td>1</td><td>left</td><td>q</td></tr><tr><td>q'</td><td>1</td><td>0</td><td>right</td><td>q''</td></tr><tr><td>...</td><td>...</td><td>...</td><td>...</td><td>...</td></tr></tbody></table>

<figure><img src="image_16.png" /><figcaption>Figure 16.3: State graph of a Turing machine recognising the language of words with as many a as b.</figcaption></figure>

called *m-configuration* (or simply *state*) which is a classification of situations the machine can be in. An intuitive example of states are the two or three colours of traffic lights. The machine goes from an *m-configuration* to another one depending on what symbol is read. Then, a symbol is written and the machine moves left or right. An example of move is given in Figure 16.1. The machines move accordingly to a *transition table* such as the table of Figure 16.2.

§16.3 Turing wanted to compute numbers and he had in mind *sequences* of digits such as $\pi$ or the decimals of $1 \div 3$. Interestingly, he wanted his machines to compute forever and distinguished two classes of machines: *circular* machines which get stuck and the others are *circle-free*. Although very powerful, Turing did not provide a lot of relevant examples illustrating the computational power of his machines.

§16.4 We now give a modern definition of *non-deterministic Turing machine* (NTM) with more
modern definitions and notations. Modern Turing machines can be either *deterministic* or *non-deterministic*. Deterministic ones have only one possible transition at every step, so no choices are possible whereas non-deterministic machines have several choices of transition. Turing machines can be used for two purposes (which differ from Turing's original machines):

* *accepting or rejecting* an input word, and then the machine is seen as a *recogniser* of a language;

* *computing a mathematical function* by stopping with a result left on the tape (which is closer to what Turing had in mind). In the case of partial functions, the machine is expected to loop on undefined inputs.

Our definition will include special states $q_a$ and $q_r$, respectively representing the state of acceptation and the state of rejection. Moreover, unlike Turing, we will be especially interested in machine computing mathematical functions in finite time instead of printing a sequence of digits. Looping will usually be seen as an *ill* behaviour. We refer to Appendix A.3 for technical definitions of language theory used in this section.

§16.5 A non-deterministic Turing machine is a tuple $M = (Q, \Gamma, \Delta, q_0, q_a, q_r)$ where $Q$ is the set of states, $\Gamma$ is the alphabet of the tape (cf. Appendix A.3), $\Delta: Q \times \Gamma_{\varepsilon} \to \mathcal{P}(Q \times \Gamma_{\varepsilon} \times \{1, \mathbf{r}\})$ is the transition function (which can be written as a transition table as in Figure 16.2), $q_0$ is the initial state, $\Gamma_{\varepsilon} := \Gamma \cup \{\varepsilon\}$ and finally, $q_a$ and $q_r \neq q_a$ are respectively the state of acceptation and rejection. We require that $\Delta(q_a, c) = \emptyset$ and $\Delta(q_r, c) = \emptyset$ for all $c \in \Gamma_{\varepsilon}$. We assume the existence of a symbol $\sqcup \in \Gamma$ representing the emptiness. An example of *state graph* of a Turing machine is illustrated in Figure 16.3. Vertices are states and arrows represent transitions.

§16.6 A configuration<fnref n="14" /> is a triple $(l, q, r)$ where $q \in Q$ and $l, r$ are tapes (sequence of characters in $\Gamma$). Configurations represent the position of the head of the machine on the tape and the associated state. We say that a configuration $C$ leads to $C'$ when moving the head in $C$ accordingly to $\Delta$ leads to $C'$. A word $w = c_1...c_n$ is accepted by $M$, written $M(w) = 1$, when there is an *accepting* sequence of configurations $C_1, ..., C_n$ such that:

1. $C_1 = (\sqcup, q_0, w)$;

2. $C_i$ leads to $C_{i+1}$;

3. $C_n = (l, q_a, r)$ for some $l$ and $r$.

If the last configuration has a state $q_r$ instead, we say that $M$ *rejects* $w$, which is written $M(w) = 0$. When $M$ *loops* infinitely on $w$ by never reaching a final state for any sequence of configuration, we write $M(w) = \infty$. We require that an NTM necessarily ends on $q_a$ or $q_r$ when it stops. For instance, the Turing machine of Figure 16.3 accepts *aabb* but rejects *aba*. The machine is designed so to accept all words having as many *a* as *b*.

<footnote n="14">¹⁴Note that this is different from what Turing called configuration (a state).</footnote>
<table><caption>Figure 16.4: Encoding of pair of natural numbers with natural numbers.</caption><tr><td>4</td><td>.</td><td>.</td><td>.</td><td>.</td><td>.</td><td>.</td></tr><tr><td>3</td><td>9</td><td>.</td><td>.</td><td>.</td><td>.</td><td>.</td></tr><tr><td>2</td><td>5</td><td>8</td><td>.</td><td>.</td><td>.</td><td>.</td></tr><tr><td>1</td><td>2</td><td>4</td><td>7</td><td>.</td><td>.</td><td>.</td></tr><tr><td>0</td><td>0</td><td>1</td><td>3</td><td>6</td><td>.</td><td>.</td></tr><tr><td></td><td>0</td><td>1</td><td>2</td><td>3</td><td>4</td><td>5</td><td>6</td></tr></table>

§16.7 A lot of extensions can be designed such as considering several heads, several tapes, tapes infinite and only one side, etc. But most interesting variants have been shown to be equivalent, which sounds very surprising. It shows how *robust* the class of computable functions is. This emphasises the fact that Turing machines capture the notion of effective procedure and is the right choice to define the class of computable functions. Surprisingly, Turing machines are able to simulate Church's λ-calculus and the converse holds as well!

§16.8 **Automata theory.** Turing machines can be weakened to produce what we call *automata* [Sip06, Part One]. The weakest form of commonly studied automata are *finite automata* which linearly consume their input and have no memory. Finite automata recognise a subset of recursive languages called *regular languages*. They can be extended to *pushdown automata* having a stack as memory (a sequence of stacked elements on which we can either extract the top element or add new elements over it) and recognising *context-free languages*. Considering several types of machines allows to consider a whole hierarchy of classes of languages called *Chomsky hierarchy*.

## A bit of hacking with Turing machines

§16.9 **Coding.** For someone not used to Turing machines (or even programming), it looks very cumbersome to solve problems. How can Turing machines solve problems about logical formulas or mathematical expressions? The idea is to *encode* inputs in a representation easy for a Turing machine to work with. Actually, even a binary language only consisting of the symbols 0 or 1 is sufficient. More generally, most objects of interest can be turned into natural numbers. There are known bijections between the set of natural numbers $N$ and the set of pairs of natural numbers $N \times N = N^2$. This allows to represent a pair $(n, m)$ as a single natural number $\#(n, m) \in N$. The idea is that we can construct an array with $N$ as vertical and horizontal axis (cf. Figure 16.4). By enumerating natural numbers on the diagonal, it is possible to associate a *unique* natural numbers with any pair $(n, m) \in N^2$. By convention, the first component corresponds to the horizontal axis and the second one corresponds to the vertical one. If we focus on $\#(x, 0)$, we remark that we must enumerate all natural numbers from 0 to $x$. At the first diagonal, we have enumerated 1 number (only 0), then $1 + 2$ at the second diagonal and so on. Hence
<figure><img src="image_17.png" /><figcaption>Figure 16.5: Attempt at enumerating all real numbers in the interval $[0, 1] \subseteq \mathbb{R}$.</figcaption></figure>

$\#(x, 0) = 1 + 2 + \dots + x = \frac{x(x+1)}{2}$. Now, what happens when we go $y$ steps up in the vertical axis? What we do is basically doing $y$ steps on the right in order to select the right diagonal to traverse, then increase by $y$ to represent the upward traversal of the diagonal. We obtain $\#(x, y) = \#(x + y, 0) + y = \frac{(x+y)(x+y+1)}{2} + y$. The idea can be generalised to any tuples with the recursive definition $\#(n_1, \dots, n_k) := \#(\dots\#(n_1, n_2), n_3), \dots, n_k)$ by iterating the encoding of pairs. Since these are bijections, a machine can decode inputs in a unique way.

**§16.10 Universality and simulation.** If most objects of interest can be encoded as numbers, so can be Turing machine themselves. Sets can be encoded as tuples and since a machine $M$ is a tuple, it can be encoded itself as a number $\#M$. It is then perfectly possible to consider machines taking other machines as input or even outputting a machine as result. In particular, it is possible to design what we call a *universal Turing machine* which is a Turing machine able to read the encoding of a machine as input (or its *code* in modern terms<fnref n="15" />) and simulate it by reproducing exactly the steps it would have done. More formally, if we have a universal machine $U$, then $U(\#M, w) = M(w)$.

**§16.11** Even more than objects and machines, it is possible to turn problems into set of numbers containing their solution. For instance, if $\#w$ is the encoding of a word into a natural number, then the problem of telling if two words are equal becomes the set $E := \{\#(\#w_1, \#w_2) \mid w_1 = w_2\} \subseteq \mathbb{N}$. Decidable problems become *recursive sets*, i.e. sets $A$ for which the (total) characteristic function $\chi_A$ such that $\chi_A(x) = 1$ when $x \in A$ and $\chi_A(x) = 0$ otherwise can be implemented by a terminating Turing machine. For instance, it is not difficult to design a Turing machine recognising the language $E$. It would be a machine accepting two equal input words. A weaker class of sets are *recursively enumerable sets* corresponding to sets which can be enumerated by a Turing machine. A way to formalise this is that recursively enumerable sets are sets $E$ for which there exists a partial function $f$ of domain $E$ which can be implemented by a Turing machine.

**§16.12 Cantor's diagonalisation method.** By using simulation and encoding, it is possible to do some little hacks on Turing machines. Using Cantor's diagonalisation method it is possible to infer the inexistence of some machines. Originally, Cantor's diagonalisation

<footnote n="15">¹⁵This is not so impressive in programming: it is what compilers and interpreters do.</footnote>
is a way to prove that $\mathbf{R}$ is uncountable, i.e. that there is no bijection between $\mathbf{N}$ and $\mathbf{R}$. It is sufficient to consider the interval $[0, 1] \subseteq \mathbf{R}$. The idea is to try to enumerate all these real numbers as in Figure 16.5, then show that it is always possible to construct a real number not in this enumeration (although it is initially thought to be complete). This problematic natural number $x$ is constructed as follows: makes the first decimal different from the first decimal of the sequence (for instance 2 is different from 1, do the same for the second decimal (for instance 2 is different from 9. At this point we have 0.22. We can do the same for every decimal: the $n$-th decimal of $x$ should be different from the $n$-th decimal of the $n$-th number of the sequence. We indeed obtain a real number theoretically not in the enumeration.

§16.13 The set of Turing machines is countable (hence bijective to $\mathbf{N}$) because they can be encoded as natural numbers and the set of all languages is uncountable, because in particular, the set of all infinite sequences of digits in uncountable (by Cantor's previous proof that $\mathbf{R}$ is not bijective to $\mathbf{N}$). Since the set of all languages cannot be put into correspondence with corresponding Turing machines recognising them, there must be some languages which cannot be recognised by Turing machines. This is a first interesting result which can be interpreted as the fact that some problems cannot be *computationally solved* (you can find more details in Sipser's introduction to the theory of computation [Sip06]). Now, it is interesting to exhibit such problems.

## Undecidable problems

§16.14 **Halting problem.** Now, I introduce the so-called halting problem<fnref n="16" />, showing that some problems are impossible to solve with a Turing machine. The halting problem asserts that “there is a machine $M$ such that for any machine $N$, $M(\#N) = 1$ when $N$ halts and $M(\#N) = 0$ when it does not”. We can define a weird machine $D$ (for *diagonal*, in reference to Cantor's diagonalisation method) taking the encoding of a machine $M$ as input:

$$D(\#M) = \begin{cases} \infty & \text{when } M(\#M) = 1 \\ 1 & \text{otherwise} \end{cases}$$

where we implicitly make use of a machine checking if a machine loops on an input. This machines $D$ loops for every machine accepting itself. The input of $D$ ranges over the set of all machines. In particular, $D$ itself is a machine of this set (it is similar to what happens in Russell's paradox). What happens when we would like to know the forbidden answer of $D(\#D)$?

$$D(\#D) = \begin{cases} \infty & \text{when } D(\#D) = 1 \\ 1 & \text{otherwise} \end{cases}$$

Assume that $D(\#D) = 1$ then by the definition of $D$... $D(\#D)$ loops. Now, if $D(\#D)$ loops, by the definition of $D$, $D(\#D) = 1$. This is contradictory. Hence, it is impossible

<footnote n="16">¹⁶Term apparently introduced by Davis [Dav58].</footnote>
to tell if a machine will loop on an input (which was the only assumption). A variant of
this problem called *acceptation problem* has exactly the same structure except that we
replace halting is replaced by rejection of the input. You can find more details in Sipser's
book [Sip06, Section 4.2] about how diagonalisation plays a role in this construction.

§16.15 **Post's correspondence problem.** Undecidability can also occur in very natural prob-
lems independent of Turing machines such as in Emil Post's correspondence problem
(PCP) [Pos46]. Dominos are pair words $\frac{w_1}{w_2}$. Given a list (ordered sequences) of dominos
$L = \frac{v_1}{w_1}, \dots, \frac{v_n}{w_n}$, the top words and bottom words form new words $v_1\dots v_n$ and $w_1\dots w_n$ by
concatenation. If $v_1\dots v_n = w_1\dots w_n$ then we say that $L$ is a *match*. Post's problem asks
whether a given set of dominos can produce a list (with possible repetitions of dominos
coming from the set) which is a match. For instance, Sipser's [Sip06, Section 5.2] ex-
ample of match is $\{\frac{b}{ca}, \frac{a}{ab}, \frac{ca}{a}, \frac{abc}{c}\}$ which can produce the list $\frac{a}{ab}, \frac{b}{ca}, \frac{ca}{a}, \frac{a}{ab}, \frac{abc}{c}$. However,
$\{\frac{abc}{ab}, \frac{ca}{a}, \frac{acc}{ba}\}$ cannot produce a match. This problem is known to be undecidable.

§16.16 **Busy Beaver.** A funny undecidable problems introduced by Radò [Rad62] is formulated
as a game. Given a number of state *n* and the alphabet {0, 1}, you have to design a
terminating Turing machine which outputs as many 1 symbols as possible. The winning
machine with the largest input is called BB-*n*. The problem of verifying if an input
machine *M* is a BB-*n* for some *n* is undecidable.

**Towards programming**

§16.17 **Post machines.** I recommend Liesbeth De Mol’s works for more details about Post’s
contributions. Although it is the name of Turing that is often mentioned as the “inventor
of computer science”, in the same year as Turing (1936), Emil Post actually designed a
Turing-complete model of computation independently [Pos36]. His model of computation
works with a two-way infinite sequence of spaces and boxes which be either marked or
unmarked. A “worker” operates on one box at a time accordingly to a given ordered
finite sequence of instructions<fnref n="17" />. The instructions which can be used are the following:

• marking the current box;

- erasing the mark in the current box;

• moving the current box to the right;

• moving the current box to the left.

Since the notion of recursiveness (which characterises the computable) already existed,
Emil Post already conjectured that his model of computation was equivalent to it, which
would make his model Turing-complete. It is also possible to think of several extensions
such as using several distinct ways to mark boxes or extending the primitive instructions.

<footnote n="17">¹⁷He almost invented Amazon’s logistics before computer science even existed.</footnote>
<figure><img src="image_18.png" /><figcaption>Figure 17.1: Tiling with two wang tiles.</figcaption></figure>

§16.18 **Wang machines.** In 1954, Hao Wang, a philosopher and mathematician introduced¹⁸ B-machines which are equivalent to Turing machines and close to Post machines [Wan57]. His paper also contained extensions such as the W-machine allowing an erasure instruction. His B-machines have a binary infinite tape and the following set of instructions:

• $\to$: move right;

• $\leftarrow$: move left;

• $*$: print $*$ (a mark) on the current square

• $C_n$: if the current square is marked then jump to the instruction $n$;

• $E$: erase the mark of the current square (only for W-machines).

This is often considered as the first presentation of Turing machines which is closer to today's programming. A *program* is an ordered sequence of pairs $(k, I)$ where $k \in \mathbb{N}$ is a line number and $I$ is one of instruction described above. For instance, $\{(1, *), (2, \to), (3, C_2), (4, \to), (5, \leftarrow)\}$ is a program.

§16.19 Today, various sort of programming languages exist to automate operations on a computer. A computer has several type of memories such as volatile memory (which is used for temporary operations) and non-volatile memory (mostly used for permanent storage). Programming languages allow to write programs executing tasks which manipulate the memory or other features of computers. These languages can be *imperative* like the sequence instructions of Post and Wang machines and they can be *functional* be extending the $\lambda$-calculus by the realisation of a mathematical function. They can also be both or coming from completely different traditions of computation. Programming opened a whole new fascinating field of interesting way to automate operations in very different ways.
# 17 Computation as tiling construction

**§17.1** After his Wang machines, Wang introduced a new model of computation: Wang tiles. It is a puzzle-like model which is very different from the previous models presented. It works by placing some pieces next to each other following some conditions in order to obtain a more complex construction. It is what happens with dominos. Dominos are objects having two sides which both contain a number between 1 and 6 (included). Dominos are put on a surface with two sides next to each other only when they hold exactly the same number. Wang tiles generalise this idea with a square of four sides (north, south, east, west) containing a colour (or equivalently a natural number). These tiles are then put on the plane $\mathbb{Z}^2$ (or equivalently a grid graph, cf. Appendix C). From a given set of tiles $T$, we can construct tilings with occurrences of tiles in $T$. An illustration in Figure 17.1 presents different connexions of Wang tiles.

**§17.2** **Wang tiles.** More formally, a tile type can be formalised by a tuple $t_i = (s_w^i, s_e^i, s_s^i, s_n^i)$ for $i$ in a finite set of indexes $I$. The components correspond to the four sides of the tile. A function $col \in \mathbb{N}$ associates a natural number of a side. For instance, the two tile types used in Figure 17.1 are $(s_w^1, s_e^1, s_s^1, s_n^1)$ with $col(s_w^1) = 2$, $col(s_e^1) = 2$, $col(s_s^1) = 1$, $col(s_n^1) = 3$ and $(s_w^2, s_e^2, s_s^2, s_n^2)$ with $col(s_w^2) = 2$, $col(s_e^2) = 1$, $col(s_s^2) = 3$, $col(s_n^2) = 4$. Instead of the plane $\mathbb{Z}^2$, we consider subgraph of square grid graphs with corresponds to connected subgraphs of the cartesian product $G \times G'$ of two linear graphs (cf. Appendix C). Vertices are associated with a coordinate $(x, y) \in \mathbb{Z}^2$. Given a set of tile types $T$, a tiling is a subgraph of square grid graph $G_\alpha = (V, E, \text{end})$ together with a (possibly partial) function $\alpha: V \to T$ associating a tile type $\alpha(v)$ to vertices of $G_\alpha$. For each tiling, we require that two vertices $v$ and $v'$ respectively of coordinates $(x, y)$ and $(x', y')$ and of tiles $\alpha(v) = (s_w^i, s_e^i, s_s^i, s_n^i)$ and $\alpha(v') = (s_w^j, s_e^j, s_s^j, s_n^j)$ for $i \neq j$ are adjacent when:

* if $v$ is on the left of $v'$ ($x = x' - 1$ and $y = y'$), then $col(s_e^i) = col(s_w^j)$;

* if $v$ is on the right of $v'$ ($x = x' + 1$ and $y = y'$), then $col(s_w^i) = col(s_e^j)$;

* if $v$ is above $v'$ ($x = x'$ and $y = y' + 1$), then $col(s_s^i) = col(s_n^j)$;

* if $v$ is below $v'$ ($x = x'$ and $y = y' + 1$), then $col(s_s^i) = col(s_n^j)$.

**§17.3** **Domino problem.** Wang's domino problem asks for a way to determine if a given set of tile types is able to produce infinite tilings able to fill all the plane $\mathbb{Z}^2$. In 1966, Robert Berger, one of Wang's student, gave a negative answer [Ber66]. He defined a translation from Turing machines to Wang tiles so that if the machine loops then the corresponding set of tile types tiles the plane $\mathbb{Z}^2$. Since the Halting problem is known to be undecidable (cf. Paragraph 16.14), it must be impossible to tell if a tile set is able to tile the plane.

<footnote n="18">¹⁸The idea has been presented to the ACM in 1954 although the corresponding paper has been published in 1957.</footnote>
<figure><img src="image_19.png" /><figcaption>Figure 17.2: Illustration of an assembly in an aTAM. Assume we are at temperature $τ = 2$. We can connect a new tile to an assembly because the glue types match and the sum of strengths involved is $1 + 1 \ge \tau$.</figcaption></figure>

§17.4 Another notion of interest for people working on Wang tiles is *aperiodicity*. A periodic tiling with a repeated pattern. Soon after Wang introduced his tiles, he conjectured that if a finite set of tiles can tile the plane, then there must be a periodic tiling as well. This is what led to his Domino problem and to Berger's negative answer. But another observation of Berger shows that there must be a finite set of tiles which can tile the plane *aperiodically* (hence without repeated pattern), which sounds very surprising. A quest of some researchers was to found such a finite set of tiles and actually several have been found (some being smaller than others) [CI96, JR15]. It has been shown in 2015 that a set of 11 tiles was the smallest possible.

§17.5 There are known links between tile systems, logic and automata [Tho91]. One link often presented is that set of Wang tiles induce *transducers* [CI96, JR15]. A transducer is a sequential state machine consuming an input word and writing symbols in an output. From the transducer corresponding to a set of Wang tiles it is then possible to reason about properties of (a)periodicity of tilings.

§17.6 Wang tiles are indeed a rather unusual way to compute and yet Berger implicitly showed that it was Turing-complete. Actually, such tile-based computation, although not so natural, found applications in biology where asynchronous communication between independent biological agents is a common thing. It seems that crystal formation, for instance, follows mechanisms of tilings for complex structures. In the remaining parts of this section, we will focus on *DNA computing* [See82]. In DNA computing, DNA strands can be used to compute in different ways with models we will present. DNA computing, although almost inexistent in my field of study, seems underestimated. Biological operations in general can be very long to compute (we have to wait for the end of a biological/chemical reaction but it has the advantage of being massively parallel) and rather cheap.

§17.7 **Abstract Tile Assembly Model.** A first model of DNA computing is the abstract tile assembly model (aTAM) [Win98, Pat14] which is an extension of Wang tiles. We refer to Lathrop et al. [LLS09] for more details<fnref n="19" />. Tiles $t_i = (s_w^i, s_e^i, s_s^i, s_n^i)$ are defined in

<footnote n="19">¹⁹However, we use a variant without seed assembly $\sigma$ because it is more natural in our case.</footnote>
<figure><img src="image_20.png" /><figcaption>Figure 17.3: Tiling of flexible tiles connected by two complementary flexible arms.</figcaption></figure>

the same way as for Wang tiles. Colours are called *glue types* and are usually represented by constants instead of natural numbers. Given a set of glue types $G$, we have a function $\text{str} : G \to \mathbb{N}^+$ providing the *strength* of a glue type.

Tiles live in an environment having a *temperature* which is a natural number $\tau \in \mathbb{N}^*$. The idea is that the temperature is a threshold of *cooperation*: a connexion involving several tiles happen only if the sum of strengths of the sides involved in the connexion is at least $\tau$.

A tile assembly system (TAS) is a pair $\mathcal{T} = (T, \tau)$ where $T$ is a set of tile types and $\tau \in \mathbb{N}^*$ is the temperature of $\mathcal{T}$.

Given a set of tile types $T$, a $T$-configuration is a partial function $\alpha : \mathbb{Z}^2 \to T$ pasting tiles to the plane. It is associated with a connected square grid graph $G_\alpha = (\text{dom}(\alpha), E)$ with an edge between two vertices representing tiles $t_i, t_j$ with $i \neq j$ when $g_d^i = g_{d'}^j$ for $d = \text{op}(d')$ where $\text{op}$ is the involution defined by $\text{op}(e) = w$ and $\text{op}(n) = s$.

We say that $\alpha$ is $\tau$-stable if it is impossible to cut $E^{G_\alpha}$ into two parts such that it breaks bonds of total strength at least $\tau$. In other words, it means that a new tile can be added to a $T$-configuration only if the total strength value of its bonding is at least $\tau$.

A $T$-assembly for $\tau$ is a $T$-configuration which is $\tau$-stable. Given a TAS $\mathcal{T} = (T, \tau)$, we write $A\square[\mathcal{T}]$ for the set of all $T$-assemblies for $\tau$ which are connected and maximal (impossible to extend with more tiles of a given set of tile types). An example of tiling is given in Figure 17.2.

In particular, the case of $\tau = 1$ is called *non-cooperative* since any compatible tiles can be connected independently of others without regards to any global constraints.

**§17.8 Flexible tiles.** Another (less known) model of computation of interest is the model of *flexible tiles* introduced by Nataša Jonoska [JM05] which is able to encode “planar” models (also known as *rigid tile systems*^20) such as Wang tiles [JM06]. This model is used for what we call DNA computing with *branched junction molecules* [EMJP19, Section 2]. The idea is to consider tiles with *flexible arms* with no constraint with planarity, similarly to cables which can be plugged with each other when complementary. An example of flexible tiling is illustrated in Figure 17.3.

<footnote>^20I once asked Jonoska why are we even doing DNA computation with rigid tiles since it intuitively seems more natural to use flexible tiles. Her answer was that it was experimentally easier to have control over rigid tile systems than over flexible tile systems.</footnote>
Again, the terminology changes. Glue types are called sticky-ends and sticky-end types identify sticky-ends (which correspond to sort of detached part of a DNA strand) having an identical sequence of nucleotides.

We define a Watson-Crick complementarity as an involution<fnref n="21" /> $\mathbf{op} : H \rightarrow H$. We assume that $\mathbf{op}(h) \neq h \neq \mathbf{op}(\mathbf{op}(h))$. Two sticky-end types $h$ and $h'$ can be connected when $\mathbf{op}(h) = h'$.

Given a set of sticky-end types $H$ and a Watson-Crick complementarity for $H$, we define a *port bonding system (PBS)* by a pair $(H, \mathbf{op})$.

§17.9 Jonoska, McColm and Staninska's choice [JMS11, Section 2.2] is to model flexible tiles with star-like graphs but I suggest an alternative (and more limited) definition that I personally prefer. A *tile type* is a multiset of sticky-end types and a *pot type* is a multiset of tile types.

For a given PBS $(H, \mathbf{op})$, the *dependency multigraph $\mathcal{D}[P]$* of a pot type $P$ defined with $H$ is a multigraph $(V, E, \ell)$ where the set of vertices is $V := P$ and there is an edge $e$ between two tile types for every pair $(p, p')$ of complementary sticky-end types inside them *w.r.t.* the involution $\mathbf{op}$ so that $\ell(e) = (p, p')$ is an edge-labelling function.

A *complex* (tiling) is a label-preserving graph homomorphism $\alpha : G_\alpha \rightarrow \mathcal{D}[P]$ from a non-empty finite connected multigraph $G_\alpha$. The vertices $v$ of $G_\alpha$ are (*flexible*) *tiles* of type $\alpha(v)$.

§17.10 The properties of interest for a given pot type $P$ are the following:

* a complex $\alpha$ is *stable* if $G_\alpha$ has no complementary pair of free (unconnected) sticky-ends in $P$ (which correspond to occurrences of sticky-end types of $G_\alpha$ not involved in any edge label);

* a complex $\alpha$ is *complete* if $G_\alpha$ has no free sticky-ends at all.

A use of flexible tiles is to provide sort of generators of graphs. It is then interesting to study which class of graphs can be generated by which set of flexible tiles.

# 18 Computation as flow of information

§18.1 It is possible to compute with what we call *circuits* which are directed acyclic graphs (DAG) in which information flows from (usually binary) some inputs to a unique input. In 1937, Claude Shannon have shown in his master thesis [Sha38] that Boolean algebra (which is a more mathematical formulation of Boole's original logic presented in Paragraph 2.2) could be used to simplify electronic machines of his time. This led to the construction of *digital circuits*. Since the History of circuits is a bit unclear and mixed with engineering and technologic developments, I will focus on technical and modern

<footnote n="21">²¹A function $f$ such that $f(f(x)) = x$.</footnote>
<figure><img src="image_21.png" /><figcaption>Figure 18.1: Boolean circuit computing $(x_1 \land x_2) \land x_3 \Rightarrow x_1 \land (x_2 \land x_3) \equiv \neg((x_1 \land x_2) \land x_3) \lor (x_1 \land (x_2 \land x_3)) \equiv ((\neg x_1 \lor \neg x_2) \lor \neg x_3) \lor (x_1 \land (x_2 \land x_3))$.</figcaption></figure>

mathematical definitions of circuits. Formal definitions can be found in general purpose books mentioning complexity theory<fnref n="22" /> such as Sipser's book [Sip06][Section 9.3] or Arora-Barak's book [AB09, Chapter 6]. I suggest a variant of these definitions here.

§18.2 We start with *boolean circuits*. The general idea is that boolean circuits are acyclic directed graphs showing how to produce a single output from a certain number of inputs (either constant or variables) by using logical operations called *gates* (disjunction, conjunction, negation or even more depending on the definitions). We provide a definition using the notion of *sharing* which allows to share the value of an input.

§18.3 A *boolean circuit* is a tuple $C = (V, E, \text{in}, \text{out}, \ell)$ where $(V, E, \text{in}, \text{out})$ is a directed acyclic graph and the function $\ell: V \to \{x_i, 0, 1, \wedge, \vee, \neg, \mathbf{s}, \mathbf{c}\}$ is a labelling function where $x_i$ for $i \in \mathbb{N}$ is a variable, $\mathbf{s}$ corresponds to a *sharing* operation and $\mathbf{c}$ to a conclusion. The *value val$_\Omega(v)$* associated with a vertex $v \in V$ is defined inductively as follows by using the usual definitions of boolean functions and an interpretation of variables $\Omega: \{x_i\}_{i \in \mathbb{N}} \to \{0, 1\}$:

$$ \triangleright \text{ if } \ell(v) \in \{x_i\}_{i \in \mathbb{N}}, \text{ in}(v) = \emptyset \text{ and } |\text{out}(v)| = 1, \text{ we have } \text{val}_{\Omega}(v) := \Omega(v); $$

$$ \triangleright \text{ if } \ell(v) \in \{0, 1\}, \text{ in}(v) = \emptyset \text{ and } |\text{out}(v)| = 1, \text{ we have } \text{val}_{\Omega}(v) := \ell(v); $$

<footnote n="22">²²Circuits are subject of a great interest in complexity theory.</footnote>
▷ if $\ell(v) = \mathbf{s}$, $\mathbf{in}(v) = \{v'\}$ and $|\mathbf{out}(v)| = 2$, we have $\mathbf{val}_{\Omega}(v) := \mathbf{val}_{\Omega}(v')$;

▷ if $\ell(v) = \mathbf{\neg}$, $\mathbf{in}(v) = \{v'\}$ and $|\mathbf{out}(v)| = 1$, we have $\mathbf{val}_{\Omega}(v) := |\mathbf{val}_{\Omega}(v') - 1|$;

▷ if $\ell(v) = \mathbf{\wedge}$, $\mathbf{in}(v) = \{v_1, v_2\}$ and $|\mathbf{out}(v)| = 1$, we have $\mathbf{val}_{\Omega}(v) := \min(\mathbf{val}_{\Omega}(v_1), \mathbf{val}_{\Omega}(v_2))$;

▷ if $\ell(v) = \mathbf{\vee}$, $\mathbf{in}(v) = \{v_1, v_2\}$ and $|\mathbf{out}(v)| = 1$, we have $\mathbf{val}_{\Omega}(v) := \max(\mathbf{val}_{\Omega}(v_1), \mathbf{val}_{\Omega}(v_2))$;

▷ if $\ell(v) = \mathbf{c}$, $\mathbf{in}(v) = \{v'\}$ and $|\mathbf{out}(v)| = 0$, we have $\mathbf{val}_{\Omega}(v) := \mathbf{val}_{\Omega}(v')$

with the global condition that there is a unique $v \in V$ such that $\ell(v) = \mathbf{c}$. If a vertex does not follow the above conditions, then the circuit is not well-formed. The *evaluation* of a circuit is defined by $\mathbf{val}_{\Omega}(C) := \mathbf{val}_{\Omega}(v)$ such that $v \in V$ and $\ell(v) = \mathbf{c}$. Such a vertex $v$ represents the unique conclusion of the circuit.

**§18.4** Figure 18.1 illustrates an example of circuit which is always true whatever the inputs we choose since the associated formula is a tautology (cf. Paragraph 6.11). Notice how the sharing gate allows to duplicate the value of an input. This makes boolean circuits different from the truth interpretation of formulas (cf. Definition 6.5) since the values of all occurrences of a variable has to be computed. Moreover, sharing is not limited to variables and hence allows for efficient representations of propositional formulas.

**§18.5** **Circuit families.** In terms of computability, boolean circuits implement *total* boolean functions $\{0,1\}^n \to \{0,1\}$ for $n$ inputs. However, Turing machines can compute for *any* input size. The only way to compute any input size with circuits is to consider *circuit families* which are set of circuits $(C_i)_{i \in \mathbb{N}}$ for $C_k$ a circuit of $k$ inputs. Such families are actually problematic: they are theoretically able to decide any language including the language associated with the halting problem (Turing machines implement *partial* functions). It looks miraculous but there is actually no way to give a concrete construction of such sets in the first place, hence this is an inaccessible miracle. The usual compromise is to consider *uniform* circuit families which are circuit families which can effectively and efficiently (several definitions can be considered) be constructed by a Turing machine.

**§18.6** **Arithmetic circuits.** Boolean circuits can be generalised to *arithmetic circuits* by considering any field $K$ (instead of $\{0,1\}$) and operations on it such as addition or multiplication. This allows to compute finite *polynomials* $\sum_{k=0}^{n} a_k x^k$ for some constants $a_k \in K$ (instead of boolean expressions). Circuits of any kind always have a shape of graph and only the mechanisms underlying gate changes. In particular, nothing prevents us to have more sophisticated functions or mechanisms for gates.
# 19 Discussion: a single materialisation of computation?

§19.1 Models of computation discussed here are “standard” ones. We are interested in classical, deterministic and finitely described models of computation. We thus choose to exclude models implementing quantum, probabilistic or analogue computation.

§19.2 Let us give a look at all these models from a more synthetic point of view. Some questions of interest to me are the following:

* what do these models have in common?

* cannot we have a single canonical representation of computation which would subsume all the models presented?

Plurality of representations is obviously of great importance since they materialise different practices coming from different computational cultures. However, I believe that these models can still be reunited and that there is something fundamental in how a lot of models of computation work.

§19.3 It seems to me that the models presented in this chapter are all about propagation of information propagated in a structure, thus directly generalising circuits:

* Turing machines but also automata can be represented as state graphs. A run on an input can be seen as propagating a configuration (state of memory and current character read) which is altered at each transition;

* tile systems can be replaced by dependency graphs $D$ and the flow traversing it is a graph-shaped exploration of $D$ representing a tiling construction (Paragraph 17.8). The data propagated and altered corresponds to information about the location of tiles in a particular geometry of space. For instance, in the case of planar tiling in $\mathbb{Z}^2$, tiles are associated with 2D coordinates;

* it is more subtle for functional computation such as $\lambda$-calculus but works on the geometry of interaction [Gir89a, DR95] show that $\lambda$-terms can be represented by proof-structures [Dan90, Chapter 11] (which are graphs) and reduction of terms can be represented by an exploration of proof-structures [AL95, DR99].

This is an idea shared by Thomas Seiller who represents models of computation by a *space of configurations* and primitive operations as monoid actions on that space [Sei20b, Section A]. It is then possible to define a universal space of computation on which features of models of computation (which define their identity) can be described as constraints over that space. For instance, if automata are seen as tile sets of transitions, choosing the right shape of tile can enforce sequentiality of runs (seen as linear tiling constructions). This shows how sequential computation can be understood as a constraint over a parallel and asynchronous model (tile systems).

§19.4 In order to properly define what would be a “universal” language of computation, fundamental questions about computation have to be answered first:
• what it is that we compute?

• what is a program?

• what is computation?

• what is an algorithm?

In modern terminology, a *program* is a computational entity which can be executed to produce a result. This process of execution is known as *computation* and an *algorithm* is simply a method which can be implemented by a program. However, it makes sense to search for more general and precise definitions.

§19.5 My (probably vague for some people) answer is that what is computed are *answers to questions*. When we compute we usually have a goal in mind (why would we compute otherwise?) and we are looking for an adequacy between the expression of that goal and the answer provided. A *program* corresponds to a construction in the space of answers (without context when it is not put against some goal). This answer can be constructed in an awkward manner, in such a way that it is not clear to us. But it can be explicit by a procedure<fnref n="23" />. This happens when we design a method to construct the answer. If the question is "4435241325 × 975746544 =?" (which is the kind of question a child would ask), the answer 4327671394674730800 does not come to mind instinctively. We usually construct a way to answer the question, which is indeed a sort of program (the method for multiplication we learn at school). Then we use the method to show that it leads to the answer: this is the *execution* (or *computation*) of our program. But the answer was already located in the composite object made of a program plugged to some inputs. It was just implicit. If execution is aborted without completion then it means that I was not able to explain how to get the answer. Lack of sound execution means lack of explanation. If the question is the expression of a goal then we can say that it is an *algorithm*. Algorithms are way to express what we would like to compute, they are sort of *specifications*. They are deeply related to logic which can be understood as a tool to formulate questions or in other words, constructions in a space of questions.

§19.6 These ideas are consistent with Seiller’s more formal proposition (at least for computation and programs at the time of this thesis) that:

• computation correspond to dynamical systems (physical world);

• programs correspond to actions on a state space (computational world);

• algorithms correspond to specifications (mathematical/logical world).

<footnote n="23">²³It reminds me of the beginning of Saint-Exupéry’s “The Little Prince”. The narrator tells a story about a child drawing of an elephant inside a boa but it looks like a hat in the point of view of adults. It is then possible to make the drawing more obvious by adding colours, adding eyes, making the boa transparent so that we can actually see the elephant.</footnote>
§19.7 In this thesis, I will present a finitist candidate for “universal” computation<fnref n="24" />. The idea is to define a chaotic space of computation in which computational features such as synchronicity, sequentiality and direction of computation (which are less “chaotic” form of computation) are *constraints* on it. Moreover, we would like to minimise as much as possible “external intervention” in computation. Such a language would be *autonomous* or *autarkic*. For instance, in the case of boolean circuits, the evaluation function would be implemented at the same level as circuits themselves and not as an external procedure. In the case of tile systems, geometric constraints would be expressed in the same language as tiles themselves.

<footnote n="24">²⁴It has to be noted that we are not looking for *the* universal model of computation but only a candidate or an attempt. It is basically the same but it sounds more modest.</footnote>
# Chapter 3

## Linking logic and computation

Logic and Computation have been presented independently in the two previous chapters. In this chapter, several links between them are introduced.

The link between logic and computation (and more precisely the Curry-Howard correspondence) is actually what made me study logic and led me to my current researches. This link is extremely fascinating and yet not so surprising after diving into details. What is fascinating is that the abstract and philosophical (I dare to say mystical) logic is related to down-to-earth and concrete computation, but also the possibility to *explain* and *justify* logic in concrete terms.

## 20 The different traditions of logic and computation

§20.1 According to Dale Miller's lecture notes<fnref n="1" /> *“Proof theory, proof search, and logic programming”*, two approaches can be distinguished in order to link logic and computation.

* *Computation-as-model* represents computation with structures of predicate calculus (cf. Definition 7.8) and logical statements are used as tools to express properties over computation. Hence, computation and logic are distinct but related notions. This is what happens in model checking [BK08]: a system is represented by an automaton or more generally by a transition system represented some structure *M* and logic can express facts about the (un)reachability of some states. Given a formula *A*, it is satisfied by *M* when $M \models A$ (cf. Paragraph 7.13);

* *Computation-as-deduction* makes syntactic elements of logic coincide with computation. Hence computation and logic are partially identified. It is itself divided into two approaches depending on what we consider as computation. There are two approaches:

- *proof normalisation* in which computation coincides with proof reduction (cf. Section 9) or cut-elimination (cf. Paragraph 10.5) for a given proof. We have a proof-program which is already there and we only have to reduce it;

<footnote n="1">¹http://www.lix.polytechnique.fr/Labo/Dale.Miller/mpri/ln2021-v3.pdf</footnote>
<figure><img src="image_22.png" /><figcaption>(a) Computation-as-model: computation and logic are distinguished notions. Logic is used to state properties about the representation of a computational system.</figcaption></figure>

<figure><img src="image_23.png" /><figcaption>(b) Computation-as-deduction (proof normalisation): we start from a whole given proof and reduce it with cut-elimination or proof reduction. Sequents are part of programs.</figcaption></figure>

<figure><img src="image_24.png" /><figcaption>(c) Computation-as-deduction (proof search): we start from a sequent and try to prove it with strategies. Sequents represent states during a computational process.</figcaption></figure>

<caption>Figure 20.1: The different traditions of linking logic and computation.</caption>
- *proof search* in which computation coincides with proof search (the process of automatically searching the proof of a given sequent). The proof itself is the result of the computation and it has to be constructed. The expression "computation as proof search" has been explicitly mentioned in Jean-Marc Andreoli's works in 1992 [And92].

§20.2 The different links between logic and computation are illustrated in Figure 20.1. In this chapter, only computation as deduction is explained in details (because I am more familiar with it, and otherwise this manuscript would be even longer than it already is).

# 21 Curry-Howard-Lambek correspondence

## Natural deduction and Lambda-calculi

§21.1 **Brouwer-Heyting-Kolmogorov.** The Brouwer-Heyting-Kolmogorov (BHK) interpretation is an attempt at giving an informal definition of what a (constructive) proof should be. It has been introduced by Brouwer and his student Heyting but also independently by Kolmogorov. Unlike the truth interpretation of classical logic which is empty of information because of its reference to an external semantics of truth (are you always satisfied by a yes or no to your questions?), the BHK interpretation explain how to actually *construct* a proof (thus providing the *why* of provable statements).

- A proof of $A \wedge B$ is a pair $(a, b)$ where $a$ is a proof of $A$ and $b$ a proof of $B$;

- A proof of $A \vee B$ is either a pair $(0, a)$ where $a$ is a proof of $A$ or $(1, b)$ with $b$ is a proof of $B$ (the value 0 and 1 indicates whether it is a proof of $A$ or $B$);

- A proof of $A \Rightarrow B$ is a *process/function/construction* turning a proof of $A$ into a proof of $B$;

- There is no proof of $\perp$;

- The special element $\emptyset$ is the unique proof of $\top$;

- A proof of $\forall x \in U.A$ is a function from $u \in U$ to a proof of $A$;

- A proof of $\exists x \in U.A$ is a pair $(t, a)$ where $t$ is a term (witness) and $a$ a proof of $A$ (certificate validating the witness).

As for atomic proofs, they are assumed to be given. The important point is that proofs of implication are functions. This is because proving that $A$ leads to $B$ can be seen as having a method to reach $B$ from $A$. But what sort of function is it? This ambiguity is actually precious because it can be any kind of function (or process). In particular, Kleene had in mind computable functions.
<figure><img src="image_25.png" /><figcaption>Figure 21.1: Correspondence between typing rule (simply typed λ-calculus) and logical rules (intuitionistic natural deduction).</figcaption></figure>

**§21.2 Lambda-terms as proofs.** A possible choice of functional and computable objects to instanciate the BHK interpretation are simply typed λ-terms (cf. Section 15). A proof of A ⇒ B becomes a term λx.M where x is a proof of A and M is a proof of B. This requirement exactly corresponds to the typing rule of function type in simply typed λ-calculus (cf. Figure 15.2). If we erase terms, we exactly obtain the natural deduction rule for implication (in sequent presentation). It shows that proving a statement A is the same as constructing a term of type A. Although a correspondence has already been remarked by Curry [Cur34] between combinatory logic and Hilbert (Frege) proof system, it is Howard [How80] who published the formal presentation of a proof-program correspondence for the λ-calculus. We give again the corresponding rules in Figure 21.1 in order to make the link even more obvious.

**§21.3** The correspondence matches so well that modus ponens naturally corresponds to the application of function (but not their execution) and proof reduction corresponds to the reduction of terms. The correspondence is in both objects and their dynamics. Recall that proof reduction for ⇒ corresponds to having an introduction of implication followed by its elimination, then reducing the initial proof to a new proof of B where the occurrences of A assumed in the proof of A ⇒ B are replaced by the proof of A which has been fed to the implication by the elimination rule ⇒e (cf. Figure 9.7). In terms of λ-calculus, this exactly corresponds the β-reduction (λx.M)N ↝$_{β}$ M[x := N] which the requirement that everything is well-typed w.r.t. simple types.

**§21.4** This formal correspondence is called *Curry-Howard-Lambek (CHL) correspondence* (or simply *Curry-Howard*). As Philip Wadler said<fnref n="2" />, this correspondence is not limited to those systems and it shows that some ideas have been discovered twice independently: once by a logician (usually the first) and once by a computer scientist. We have that:

* Church's simply typed λ-calculus corresponds to natural deduction for minimal logic, which is intuitionistic logic restricted to ⇒ as only connective (no negation as well);

* λ-calculus can be extended with more types and constructions illustrated in Figure 21.2:

<footnote n="2">²In his “Proposition as type” talk (https://www.youtube.com/watch?v=IOiZatlZtGU)</footnote>
$$ \frac{\Gamma \vdash a : A \quad \Delta \vdash b : B \quad \times \quad \Gamma \vdash (a,b) : A \times B}{\Gamma, \Delta \vdash (a,b) : A \times B} \times \frac{\Gamma \vdash a : A}{\Gamma \vdash a : A} \pi_1 \quad \frac{\Gamma \vdash A \times B}{\Gamma \vdash b : B} \pi_2 \\ \frac{\Gamma \vdash a : A}{\Gamma \vdash (0,a) : A + B} \text{ in}_1 \quad \frac{\Gamma \vdash b : B}{\Gamma \vdash (1,b) : A + B} \text{ in}_2 \quad \frac{\Gamma \vdash x : \perp}{\Gamma \vdash x : A} \perp \quad \frac{\vdash () : \top}{\vdash () : \top} \top \\ \frac{\Gamma \vdash e : A + B \quad \Delta_1, f_a : A \vdash C \quad \Delta_2, f_b : B \vdash C}{\Gamma, \Delta_1, \Delta_2 \vdash \text{ match}(e, f_a, f_b) : C} \vee e $$

<table><caption>Figure 21.2: Extended rules for typed λ-calculus. The proof reduction for × corresponds to an application of projection and the proof reduction for + corresponds to the application of pattern matching (which can be seen as the implication of a condition).</caption><thead><tr><th>Natural deduction</th><th>Typed λ-calculus</th></tr></thead><tbody><tr><td>Formula</td><td>Type</td></tr><tr><td>Implication A ⇒ B</td><td>Function type A → B</td></tr><tr><td>Sequent Γ ⊢ A</td><td>Typing assertion Γ ⊢ t : A</td></tr><tr><td>Logical rule</td><td>Term constructor</td></tr><tr><td>Proof</td><td>Typed λ-term</td></tr><tr><td>Proof reduction</td><td>Term reduction</td></tr><tr><td>Irreducible proof</td><td>Result</td></tr><tr><td>Proving</td><td>Programming (constructing a program)</td></tr><tr><td>Conjunction A ∧ B</td><td>Product type A × B</td></tr><tr><td>Conjunction introduction</td><td>Pair construction</td></tr><tr><td>Conjunction elimination</td><td>Par projection π<sup>1</sup>(x<sub>1</sub>, x<sub>2</sub>) = x<sub>i</sub></td></tr><tr><td>Disjunction A ∨ B</td><td>Sum type A + B</td></tr><tr><td>Disjunction introduction</td><td>Sum type construction</td></tr><tr><td>Disjunction elimination</td><td>Pattern matching</td></tr><tr><td>Top ⊤</td><td>Unit type</td></tr><tr><td>Bottom ⊥</td><td>Empty type</td></tr><tr><td>Second-order universal quantification</td><td>Polymorphic type</td></tr></tbody></table>

<caption>Figure 21.3: Curry-Howard-Lambek correspondence between natural deduction and typed λ-calculus.</caption>
$$ \frac{\Gamma, x : A \to \bot \vdash M : \bot \qquad \mathbf{S}}{\Gamma \vdash Sx.M : A} $$

$$ \frac{\Gamma, A \to \bot \vdash \bot \qquad \text{dne}}{\Gamma \vdash A} $$

- an empty type $\bot$ and a unit type $\top$ only having () as term;

- pairs $(a, b)$ of type $A \times B$ are *projections* allowing to extract a component (their typing rules exactly correspond to the rules of conjunction);

- sum $(i, x)$ of type $A + B$ with either $i = 0$ and $x : A$ or $i = 1$ and $x : B$ (its typing rules correspond to the introduction of disjunction). This dives two types into the same abstract type. The proof-term $(i, x)$ is often written $l_i(x)$ and is called *injection*. A typical example is the type $\mathbf{Maybe}(A) := A + \top$ which may be of type $A$ or nothing. This allows to represent partial functions;

- pattern matching which analyses a sum type and provide a result for each case. This corresponds to disjunction elimination.

* Polymorphic $\lambda$-calculus (where terms can have a generic type, e.g. $\lambda x.x : \forall X.X \Rightarrow X$) corresponds to System F which is second-order logic (cf. Section 8) without first-order quantification (it can also be called *pure* second-order logic);

* System T which is a computational system featuring built-in constants for natural numbers and booleans, together with primitive recursion (always terminating), corresponds to first-order Peano arithmetic (PA).

We obtain a big correspondence illustrated in Figure 21.3. The CHL correspondence is still an active subject of research at the time of this thesis. We refer to Sørensen and Urzyczyn's lectures for more details [SU06].

§21.5 Perhaps the most important consequence is the reunion of two communities: proof theorists and type theorists. Ideas can be shared and a common language emerges. Ideas appearing in one field can be implemented in the other. In particular, this cultural fusion can be made concrete with *category theory* (usually attributed to Joachim Lambek).

## The functional interpretation of classical logic

§21.6 The CHL correspondence was initially about *constructive* proofs because they are the ones which can materialise a (computational) process. For that reason, since classical is not constructive, it has been assumed that no computational correspondence existed for it.

§21.7 If we look at a classical proof in NK (for instance the one in Figure 9.6), we clearly see that something happens. The proof still *shows* something. By using the rule of double-negation elimination, what we do is making a formula $A$ storable (in a bottom-up reading): no operation can be done with $A$ but $\neg\neg A$ can introduce the hypothesis
¬A. We can then extend the CHL correspondence with a new term Sx.M with the rule of Section 21 which looks like the abstraction (abs) typing rule for λ-calculus. We then need more reduction rules not presented here but which can be found in the literature [SU06, Section 8.4].

§21.8 **Continuation-passing style programming.** The first hint of a CHL correspondence for classical logic has been accidentally<fnref n="3" /> discovered by Timothy G. Griffin [Gri89] (who actually worked on another subject) by remarking a relation between Peirce's law ((P ⇒ Q) ⇒ P) ⇒ P (which is a classical axiom) and an operation in the programming language Scheme known as `call/cc` (call with current continuation). This operator allows to save the current context and load it later.

§21.9 Since there exists several ways to express classical logic (depending on what axiom your choose or by allowing several conclusions), we can obtain several different computational systems for classical logic. In particular, Parigot's λμ-calculus [Par92] uses a multi-conclusion sequent calculus and Krivine's machine uses Peirce's law.

**The functional interpretation of quantification**

§21.10 The BHK interpretation (cf. Paragraph 21.1) features rather a satisfying interpretation of quantifiers. Remark that quantifiers are functions and pairs *depending* over some alogical entity: individuals. Because quantifiers hold a computational behaviour, it is not so surprising that first-order quantifiers also enjoy a CHL correspondence.

§21.11 **Dependent type.** A type system which illustrates this dependency is the theory of *dependent types* [SU06, Chapter 10] which has been introduced independently of Howard's paper. It has originally been implemented in languages such as De Bruijn's Automath<fnref n="4" /> for the verification of formal proofs using computers. It is common in mathematics to work with restricted objects depending on a parameter. For instance, we could have a type `Str(n)` of strings of $n \in \mathbb{N}$ characters and a type `Vect(n)` of vectors of size $n \in \mathbb{N}$.

§21.12 The theory of dependent types can be expressed in a calculus called λP in which only universal quantification is implemented. There are several categories of objects:

• λ-terms $M, N ::= x \mid \lambda x^A.M \mid MN$;

• dependent types A, B ::= α | ∀x^A.B | AM which can be of a certain kind κ and α is an atomic type (implication A → B is defined by ∀x^A.B where x does not appear free in A);

• kinds κ ::= * | Πx^A.κ where * represents the class of all types.

<footnote n="3">³According to what I have heard.</footnote>

<footnote n="4">⁴One of the first direct application of the Curry-Howard correspondence.</footnote>
Remark that we have a functional behaviour at the level of terms, types and kinds.
Kinds are sort of types over types: types *A* are of a certain kind $κ$, which is written
*A* : *κ*. We could define **Str** := Π*n*<sup>int.</sup>* and construct **Str**(n) : * with the rules of [SU06,
Section 10.2]. It is then possible to construct a term **fillZero** : ∀*n*<sup>int.</sup> **Str**(n) which
constructs a string of *n* characters 0. Of course, we also need more reduction rules to
apply arguments to types and not only the *β*-reduction which only applies to terms.
As for existential types ∃*x*.*A*, they correspond to a pair (*x*, *A*) of a term and a type,
expressing a dependency between *x* and *A*.

§21.13 Another precious idea appearing in Martin-Löf's intuitionistic type theory [MLS84] di-
rectly and explicitly implements the CHL correspondence. Terms are seen as proofs
and we write $M \in A$ to express the fact that $M$ is of type $A$, or that $M$ is a *proof*
of the formula $A$ (an ambiguity allowed by the CHL correspondence). This allows to
mix functional programming and proving; an essential feature of *proof assistants* such
as Coq. If we would like to prove some goal $\vdash A \Rightarrow B$, then it is sufficient to construct
a term (program) taking an input of type $A$ and producing any input of type $B$. For
instance, if we had a type *Nat* of natural numbers then the representation of the function
*succ*(n) = n + 1 in *λ*-calculus would be a proof of *Nat *⇒* *Nat*. More than proving with
programs, it is also possible to construct programs from a proof, thus producing *certified
programs* which are ensured to have the behaviour we wish for.

§21.14 How these results show how rich the CHL correspondence is. It can be applied for real-world situations and is still an active field of research with several branches and subcultures. It is not limited to natural deduction: we even have several term assignments to sequent calculus [SU06, Section 7.4] or construction of inductive types such as N which is defined by self-reference.

## 22 Realisability

My personal reference for this section is Etienne Miquey’s PhD thesis [Miq17]. Other useful references on the subject are Lionel Rieg’s PhD thesis [Rie14] and Alexandre Miquel’s HdR thesis [Miq09].

Kleene realisability

§22.1 BHK interpretation (*cf*. Paragraph 21.1) is very generic and can be instantiated by
other objects, not only computable functions or λ-terms. In realisability, instead of
proofs, more general objects called *realisers* are considered.

§22.2 **Realisability interpretation.** We write $t \Vdash A$ when $t$ is a realiser of $A$ (or that $A$ is realised by $t$). One of Kleene’s idea was to interpret intuitionistic formulas by encoding (cf. Paragraph 16.9) partial recursive functions (cf. Paragraph 13.8) by natural numbers
(he uses Gödel’s encoding in particular). We write $\varphi(n, m)$ for the application of the
function represented by $n$ to the argument represented by $m$. We write $\#(n, m)$ for the
encoding of pairs (cf. Paragraph 16.9). We obtain the following variant of BHK:

• nothing realises $\perp$;

• $0 \models T$;

• $\#(n, m) \models A \land B$ when $n \models A$ and $m \models B$;

• $\#(i, n) \models A \lor B$ when either $i = 0$ and $n \models A$ or $i = 1$ and $m \models B$;

• $n \models A \Rightarrow B$ when for all $m \models A$, we have $\varphi(n, m) \models B$.

§22.3 **Type theory and Realisability.** A question that quickly comes to mind (and it is
what I thought too in the beginning) is how it differs from typing as in typed $\lambda$-calculus.

• type theory is about using syntactic rules to verify the type of a term. It is about verifying the *shape* or *structure* of a term in order to ensure that it will behave well;

• realisability is about *associating* computational entities to formulas or giving computational representatives for formulas. Realisability is more abstract and computational as we can see in the definition of $n \models A \Rightarrow B$ which tests a function against all possible arguments. The realisation of implication is more about the *behaviour* of a function than its *structure*.

Actually, realisability generalises typing. This is represented by a property called *adequacy* formalised by the implication $t : A \Longrightarrow t \models A$ where $t : A$ is the fact that $t$ has type $A$. This can be understood as having the computational behaviour stated by $A$ when having the structure of $A$. Interestingly, because this is a computation association and not an inference about structure, nothing forbids contradictory, unprovable and undecidable formulas to be realised. It happens that some programs have a computational behaviour which is sound without fitting typing rules. Because of that it is undecidable in general to tell whether we have $t \models A$ for a given realiser $t$ and a formula $A$. According to Alexandre Miquel$^5$, in type theory, we are interested in correctness *w.r.t.* rules/typing and in realisability to correctness *w.r.t.* execution.

§22.4 The interpretation can be extended to first-order intuitionistic logic, called Heyting Arithmetic (HA). By the CHL correspondence, it corresponds to a computational system for primitive recursive functions called System T (attributed to Gödel), which can be presented as a variant of $\lambda$-calculus. Realisability gives tools to reason about the relationship between logic and computation. In particular, it is even possible to attribute a computational content to the axioms of HA. The choice of a realiser can be rather

<footnote n="5">⁵https://www.fing.edu.uy/~amiquel/realiz21/kleene.pdf</footnote>
arbitrary providing that it is computationally consistent. For instance, we can have the following realisation of axiom of HA:

$$ \lambda x.\lambda y.\lambda z.z \Vdash \forall x.\forall y.(s(x) = s(y) \Rightarrow x = y). $$

Some common properties which can be proven with the help of the realisability interpretation are the following:

* **Soundness** if $\vdash_{HA} A$ then there exists $t$ such that $t \Vdash A$;

* **Consistency** $\vdash_{HA} \perp$ (proven by the fact that $\perp$ cannot be realised).

But, what about classical logic?

## Krivine realisability

§22.5 An attempt of extending the interpretation to classical logic is given by Jean-Louis Krivine [KCHM09]. Krivine realisability is a complete reformulation of the theory of realisability [Miq17, Section 3.1.2] and has the ambition of giving a computational interpretation of important axiomatic systems such as ZFC axioms for set theory (cf. Paragraph 3.5). The extension to classical logic is related to the classical CHL correspondence using the call/cc operator (cf. Paragraph 21.8).

§22.6 **Lambda-calculus with continuations.** I will give an alternative definitions. A formula or type A can be seen as a set of realisers $|A|$. Krivine's realisers are $\lambda$-terms extended with continuations in a system called $\lambda_c$-calculus. Terms are executed w.r.t. a context or environment taking the form of a stack.

$$ M, N ::= x \mid \lambda x.M \mid MN \mid \mathbf{k}_{\pi} \mid \mathbf{cc} \qquad (\text{Terms}) $$

$$ \pi ::= \alpha \mid M \cdot \pi \qquad (\text{Stacks}) $$

where $\alpha$ is a stack constant coming from a set of stack constant. It is also possible to consider more instructions beside cc for terms. Notice that the constant $\mathbf{k}_{\pi}$ is associated with a whole stack. This will be used to store a context to load it later during the computation.

§22.7 **Krivine machine.** What is executed is not a term alone but a term in the context of a stack. We write $M \star \pi$ for a connexion between a term and a stack. Such connexions are called processes and are written with variables $p$ and $q$. The execution of a process is done by a *Krivine Abstract Machine* (KAM) which has 4 transition rules:

**Push** $MN \star \pi \rightsquigarrow M \star N \cdot \pi$ (argument is postponed)

**Grab** $\lambda x.M \star N \cdot \pi \rightsquigarrow \{x := N\}M$ (function application)

**Save** $cc \cdot M \cdot \pi \rightsquigarrow M \star \mathbf{k}_{\pi} \cdot \pi$ (the context is saved)

**Restore** $\mathbf{k}_{\pi} \star M \cdot \pi' \rightsquigarrow M \star \pi$ (the context is loaded)
We write $\rightsquigarrow^*$ for the reflexitive-transitive closure of $\rightsquigarrow$ (corresponding to multiple steps of reduction).

§22.8 **Example.** $(\lambda xy.x)z \star \varepsilon \stackrel{\text{push}}{\rightsquigarrow} \lambda xy.x \star z \stackrel{\text{grab}}{\rightsquigarrow} \lambda y.x\{x := z\} \star \varepsilon = \lambda y.z \star \varepsilon$.

§22.9 We now would like to study computational interpretations of classical logic by realizability. We write $\Lambda$ for the set of all $\lambda_c$-terms and $\Pi$ for the set of all stacks. The idea is to oppose terms and stacks such that stacks are sort of opponents for terms. The interpretation is then parametrised by a way to assert whether a term and a stack *interact correctly*.

§22.10 **Definition (Pole).** A pole is a chosen set $\perp \subseteq \Lambda \times \Pi$ which is closed under anti-evaluation, i.e. both $p \rightsquigarrow^* p'$ and $p' \in \perp$ implies $p \in \perp$ for all processes $p, p' \in \Lambda \times \Pi$.

§22.11 The requirement of anti-evaluation ensures that membership to the pole is sound w.r.t. execution by the steps of the KAM.

§22.12 **Test interpretation.** Given a pole $\perp$, a term $M$ and a stack $\pi$, the fact that $M \star \pi \in \perp$ formalises the fact that $M$ and $\pi$ interact correctly. It is then possible to see stacks as sort of tests that terms have to pass in order to be part of a some formula. For instance, consider that we have a set of stack $\|A\|$ associated with a formula $A$. Then the set of all $M$ such that $M \star \pi$ for all $\pi \in \|A\|$ defines the realisers of the formula $A$.

§22.13 **Orthogonality.** Given a pole $\perp$, it is possible to define an *orthogonality relation* between terms and stacks: we have $M \perp \pi$ if and only if $M \star \pi \in \perp$. It is then possible to define the orthogonal of sets of terms and stacks:

◇ For set of terms $S^\perp := \{\pi \in \Pi \mid \forall M \in S. M \perp \pi\}$;

◇ For set of stacks $S^\perp := \{M \in \Lambda \mid \forall \pi \in S. M \perp \pi\}$.

Such orthogonality relations are usually symmetric and is an alternative definition of “good interaction” or “passing a test”.

§22.14 **Behaviour.** Once an orthogonality relation is fixed, what will usually correspond to formula are *behaviours* which are set of terms $S$ such that $S = S^{\perp\perp}$. Although this definition seems abstract, it can be understood as a “closure by interaction”. Another equivalent definition is that $S$ is a behaviour when there is some set *Tests*($S$) such that $S = \text{Tests}(S)^{\perp}$, which can be understood as $S$ being *testable* or characterised by a set of tests.

§22.15 Using these definitions, it is then possible to give a computational interpretation of classical second-order Peano arithmetic (which was Krivine's initial goal) [Miq17, Definition 3.8]. It shows how realisability interpretation have the power to reconstruct logical systems from choosing a computational system and a right definition of pole.
## Reconstruction of simple types

§22.16 By using similar ideas, it is possible to consider simpler reconstructions. An interpretation of Colin Riba's "Strong Normalization as Safe Interaction" paper [Rib07] is that typed λ-calculus (a logical system) is reconstructed from untyped λ-calculus (a purely computational system without types).

§22.17 We consider the usual untyped λ-calculus with another notion of context (instead of stacks):

$M, N ::= x | λx.M | MN \quad \text{set } Λ \quad \text{(Terms)}$

$E[] ::= [] | E[]M | ME[] \quad \text{set } \mathcal{E} \quad \text{(Contexts)}$

with $E[M]$ defined by $E[]$ where $[]$ is replaced by $M$. A context is a λ-term with holes and we expect it to be filled by another term. It can also be seen as an incomplete term.

§22.18 We can define a pole $⊥$ defined by the set of all strongly normalising terms (all paths of reduction terminate). It is then possible to reconstruct simple types from the orthogonality relation associated with $⊥$ by an interpretation $[·]$:

• $[α] := ⊥$ (which is shown to be a behaviour by Riba [Rib07, Proposition 4.6]);

• $[A \Rightarrow B] := ([A] \cdot [B]^{\perp})^{\perp}$

where for $A \subseteq \Lambda$ and $B \subseteq \mathcal{E}$, $A \cdot B$ is defined by $A \cdot B := \{E[[M]] | M \in A, E[] \in B\}$.

§22.19 This result shows that type systems are not necessarily primitive notions and can be in some sense *justified* by computation (although Riba does not state it like that). The reconstruction with strongly normalising terms as basis is not the only solution. Riba also shows that there exist alternative definitions [Rib07, Section 6] and that both conjunction and disjunction can be defined as well.

# 23 Logic programming

## Reasoning with programs

§23.1 Predicate calculus is very convenient to express statements of natural language. For instance, the fact that my brother and I have the same mother can be represented by the formula $\mathbf{mother}(i) = \mathbf{mother}(\mathbf{brother}(i))$ where $i$ is a constant (or nullary function symbol) representing me. We can also express the fact that some brothers have a different father by the formula $\exists p. \exists p'. (\mathbf{brother}(p) = p') \wedge \neg (\mathbf{father}(p) = \mathbf{father}(p'))$.

§23.2 Kowalski's paper "Predicate logic as programming language" [Kow74] shows that predicate calculus can be seen as a programming language for symbolic reasoning. Not in the CHL sense that proofs correspond to programs but in the sense that:
```
add(0, Y, Y).
add(s(X), Y, s(Z)) :- add(X, Y, Z).
?add(s(s(0)), s(s(0)), R).
```

Figure 23.1: Example of logic program computing unary addition. The last line is the query.

* a set of assumed formulas can be seen as a database of facts or a knowledge base;

* formulas of predicate calculus can be seen as *goals*, *questions* or *queries*;

* formulas $(A_1 \wedge \dots \wedge A_n) \Rightarrow B$ can be seen as *inference rules*, that is, ways to infer a fact $B$ from facts $A_1, \dots, A_n$.

In particular, formulas representing questions can contain free variables and answers will not be truth values but terms replacing variables which are consistent with the facts.

§23.3 An example of logic program computing unary addition is given in Figure 23.1 where $B :- A$ stands for $A \Rightarrow B$ (if you wish to conclude $B$ then you have to justify $A$). A standard representation of natural numbers is to use unary numbers: a natural number is either 0 or the successor or a natural number, which can be represented by the application of a symbol $s$ over another natural number. A natural number is then a sequence of application of $s$ over 0. The expression $add(X, Y, Z)$ is a ternary predicate expressing the fact that $X + Y = Z$. The first expression says that $0 + Y = Y$ for any $Y$ and the second expression that if $X + Y = Z$ then $(X + 1) + Y = Z + 1$. The query asks for the result of the sum $2+2$. The next sections are dedicated to formalising this symbolic reasoning and providing ways to answer queries.

§23.4 Terms are used to represent statements. In particular, we are interested in solving equations $t \stackrel{?}{=} u$ between terms by searching for terms replacing variables such that it would make $t$ and $u$ equals. Equations between terms is usually attributed to Robinson [R+65] but Herbrand [Her30] already studied term unification before in the context of his investigations on mathematical equations and proof theory.

§23.5 We recall elementary definitions of term unification [Her30] in Appendix B. We refer the reader to the article of Lassez et al. [LMM88] for more details which are often omitted in the literature or Baader et al. [BN98] for a broader view. We use uppercase letters such as $X, Y, Z$ for variables and lowercase letters $a, b, c, f, g$ and $h$ for function symbols.

Normal forms

§23.6 Now that we have ways to construct sentences, we could simply use predicate calculus but it is not convenient enough to use it as it is. It has a lot of logical rules whereas what we wish for is simply an interaction between queries and clauses (either facts or
<table><caption>Figure 23.2: Transformation of Peirce law to its conjunctive normal form (CNF). Notice that two occurrences of excluded middle appear in conjunction (the *B* is not essential).</caption><tr><td>((A ⇒ B) ⇒ A) ⇒ A</td><td>translation of implication</td></tr><tr><td>≈ ¬(¬(¬A ∨ B) ∨ A) ∨ A</td><td>use De Morgan laws</td></tr><tr><td>≈ (¬¬(¬A ∨ B) ∧ ¬A) ∨ A</td><td>¬¬-elimination</td></tr><tr><td>≈ ((¬A ∨ B) ∧ ¬A) ∨ A</td><td>distribute ∨</td></tr><tr><td>≈ ((¬A ∨ B) ∨ A) ∧ (¬A ∨ A)</td><td>remove superfluous parentheses</td></tr><tr><td>≈ (¬A ∨ B ∨ A) ∧ (¬A ∨ A)</td><td></td></tr></table>

inference rules producing new goals). This section introduces ways to transform formulas in other more convenient forms.

**§23.7 Conjunctive normal form.** A simple transformation which can be done in propositional calculus is to transform formulas in conjunctions of disjunctions [HR04, Section 1.5.2]. This can be done with the following operation over formulas:

* translate all symbols (such as $⇒$) into formulas of the functionally complete set $\{\neg, \wedge, \vee\}$ for instance with:

$$ \neg A \Leftrightarrow B \Leftrightarrow (A \Rightarrow B) \wedge (B \Rightarrow A); $$

$$ \neg A \Rightarrow B \Leftrightarrow \neg A \vee B; $$

* first push all negations to atomic formulas with De Morgan laws and double-negation elimination:

$$ \neg \neg A \Leftrightarrow A; $$

$$ \neg(A \wedge B) \Leftrightarrow \neg A \vee \neg B; $$

$$ \neg(A \vee B) \Leftrightarrow \neg A \wedge \neg B; $$

* distribute disjunctions everywhere with:

$$ A \vee (B \wedge C) \Leftrightarrow (A \vee B) \wedge (A \vee C); $$

$$ (B \wedge C) \vee A \Leftrightarrow (B \vee A) \wedge (C \vee A). $$

* remove superfluous parentheses if you want, so that it is easier to read.

**§23.8** Formulas in conjunctive normal form (CNF) have the uniform shape $(A_1^1 \vee \dots \vee A_{n_1}^1) \wedge \dots \wedge (A_1^m \vee \dots \vee A_{n_m}^m)$ where the disjunctions are called (*disjunctive clauses*) and conjunctions can be seen as *collection of clauses*. This can be presented in a more friendly way: as multisets (*cf*. Appendix A.2) of clauses. We write clauses $[A_1, \dots, A_n]$ instead of $A_1 \vee \dots \vee A_n$ and multiset of clauses with a sum notation $C_1 + \dots + C_n$ instead of $C_1 \wedge \dots \wedge C_n$. An example of transformation of a formula into its CNF is given in Figure 23.2. The
alternative notation for that example would be [¬A, B, A] + [¬A, A]. It is also possible to transform formulas into disjunctive normal forms (DNF) corresponding to disjunctions of conjunctions.

**§23.9 Prenex normal form.** Now that we are able to normalise formulas of propositional calculus, we have to treat quantifiers to extend the normalisation to predicate calculus. What is usually done is to push all quantifiers to the front of the formula. We then obtain what we call a *prenex normal form* (PNF) [Hed04, Section 3.2.1]. This can be done with the following transformations:

• first translate the formula into an equivalent formula of {∀, ∃, ¬, ∧, ∨};

• apply (∀x.A) ∧ B ↦ (∀x.A ∧ B) and (∀x.A) ∨ B ↦ (∀x.A ∨ B) everywhere;

• apply (∃x.A) ∧ B ↦ (∃x.A ∧ B) and (∃x.A) ∨ B ↦ (∃x.A ∨ B) everywhere;

• apply ¬∃x.A ↦ ∀x.¬A and ¬∀x.A ↦ ∃x.¬A everywhere.

The first two rules only hold when *B* is independent from *A*, i.e. the variable *x* is not free in *B*. If it happens to be the case, the variable bound *x* in *A* can be renamed so that it is not in conflict with the free variable *x* in *B*. If we combine PNF with CNF then we can obtain a *prenex conjunctive normal form* (PCNF) $Q_1x_1...Q_nx_n.C_1+...+C_n$ where $C_i$ is a disjunctive clause and $Q_i \in \{\forall, \exists\}$.

**§23.10 Skolem normal form.** It is also possible to do even more by eliminating existential quantification. This transformation is known as *skolemisation* (or *Herbrandisation* if we remove universal quantification). A formula which is skolemised is said to be in *skolem normal form* (SNF) [Hed04, Section 3.2.2]. The idea is that whenever we have a universal quantification preceding an existential one as in $\forall x.\exists y.A$, it is the same as saying that there is a function *f* turning *x* into the “right” *y* which satisfies the formula. Existential quantification can then be removed by explicitly introducing a new function symbol *f* corresponding to that function. For instance, consider the formula $\forall n.\exists m.n < m$ stating that for all natural number *n*, there is a greater natural number *m*. We know that the function successor *s* takes a natural number *n* and produces its successor *n* < *s*(*n*). Hence the formula can be rewritten $\forall n.n < s(n)$. Without explicating what the function is, giving a universe or a model of the formula, the two formulas are logically equivalent and this is what matters anyway.

**§23.11 Skolemisation is applied over a formula $Q_1x_1...Q_nx_n.C_1+...+C_n$ in PCNF by successively selecting an existential quantifier from left to right until the last one.**

• if the selected $∃$ has no universal quantifier preceding it, then

$$∃x.A \rightsquigarrow \{x := c\}A$$

where *c* is a fresh constant not appearing in *A*;
$$ \frac{\Gamma \cup \{P(t_1, ..., t_n)\} \quad \Delta \cup \{\neg P(u_1, ..., u_n)\} \quad \text{Res} \quad \theta(\Gamma \cup \Delta)}{} $$

Figure 23.3: Robinson’s resolution rule. The substitution $\theta$ is defined as the solution of the equation underlying the two interacting atoms, that is $\theta := \mathbf{solution}P(\bigcup_{k=1}^n \{t_i \stackrel{?}{=} \alpha u_i\})$. We require that the two clauses are independent: there is a renaming $\alpha$ making all variables of $\Delta \cup \{\neg P(u_1, ..., u_n)\}$ disjoint from variables of $\Gamma \cup \{P(t_1, ..., t_n)\}$ (hence $\theta$ is an $\alpha$-unifier).

* if the selected $\exists$ has $n$ consecutive universal quantifiers preceding it, then

$$ \forall x_1...\forall x_n. \exists x. A \rightsquigarrow \forall x_1...\forall x_n. \{x := f(x_1, ..., x_n)\}A $$

where $f$ is a new function symbol not appearing in $A$, which depends upon $x_1, ..., x_n$.

§23.12 By combining all these transformations we can obtain a normal form for formula of predicates calculus. All formulas can be rewritten as a formula $\forall x_1...x_n.A$ where $A$ has no quantifiers and is in CNF. Universal quantifiers can even be hidden and the variables $x_1, ..., x_n$ occurring in $A$ will be simply considered generic.

## First-order resolution

§23.13 With the rise of computers, methods of automated reasoning began to appear. In particular, the DP algorithm (which has been extended to the DPLL algorithm$^6$) developed by Davis and Putnam [DP60] provided a way to check if a propositional formula in CNF was satisfiable.

§23.14 The idea of the DP(LL) algorithm is to construct a partial truth valuation and extend it while keeping consistency. It is more efficient than naive brute force search which would try all possibilities. It appears that all satisfiability algorithms have the same complexity: in the worst-case performance, their number of steps is exponential in the size of their input$^7$. What is meant by “keeping consistency” is that, for instance, if we had a clause $[A]$ then we can remove all occurrences of $\neg A$ in other clauses since both $A$ and $\neg A$ cannot hold at the same time. More generally, it is possible to deduce a general rule producing $C \lor D$ from $A \lor C$ and $\neg A \lor D$. This is known as the resolution rule.

<footnote>$^6$The DPLL algorithm was one of the first things I studied on my own. For some reasons, I was fascinated by it and the fact that computers could solve logical problems. I believe that implementing satisfiability algorithms is a good exercise. If you are interested in implementing automated reasoning algorithms then I think Harrison’s “Handbook of Practical Logic and Automated Reasoning” [Har09] is a good reference.</footnote>

<footnote>$^7$There a lot of optimisation giving a number of steps lesser than $2^n$ for an input of size $n$ but it is still very close. For instance, $2^{n/2} < 2^n$.</footnote>
<figure><img src="image_26.png" /><figcaption>Figure 23.4: Resolution tree for the refutation of $[A, B] + [\neg A, C] + [\neg B, D] + [\neg C] + [\neg D]$ with the resolution rule. Example taken from Hedman’s book [Hed04, Example 3.29].</figcaption></figure>

§23.15 **Resolution rule.** Robinson suggested an algorithm focussing on resolution [R$^+$65] as a way to refute statements of predicate calculus. Resolution can be seen as a logical rule over formulas in normal form (cf. Figure 23.3). In this context, predicate calculus has been so normalised to the extreme that the resolution rule is self-sufficient and no other logical rules are needed$^8$. The empty set of clause is written $\perp$ and corresponds to a contradiction. The goal is to construct a *resolution tree* to infer $\perp$ with a given set of clauses, by reusing as many occurrences of clauses as we want. The meaning of the resolution rule is that it produces a *consensus* between two clauses by *resolving* contradictions.

§23.16 **Independence of clauses.** Notice that in Figure 23.3, there is an additional requirement of independence between the two clauses being connected. This is due to the fact that $\forall x.A \land B$ is equivalent to $(\forall x.A) \land (\forall x.B)$. Hence each clause can have its own local bound variables. Without this requirement, we would not be able to infer *bot* from $[P(a,x)] + [\neg P(x,b)]$ since they share a variable which cannot be instantiated to both *a* and *b*. However, these two clauses are contradictory since they represent the formula $\forall x.P(a,x) \land \neg P(x,b) \equiv (\forall x.P(a,x)) \land (\forall x.\neg P(x,b))$ where $\forall x.P(a,x)$ can be instantiated to $P(a,b)$ and $\forall x.\neg P(x,b)$ to $\neg P(a,b)$ which is contradictory with $P(a,b)$.

§23.17 An example of resolution tree is given in Figure 23.4. If a set of clauses is inconsistent then there must be a resolution tree inferring $\perp$ from its clauses. Similarly to reasoning by contradiction, if we would like to show that a formula *A* is consequence of a set of clauses $C_1 + \dots + C_n$, then it is sufficient to provide a refutation of $C_1 + \dots + C_n + [\neg A]$ (assuming that *A* is false leads to a contradiction).

§23.18 Actually, if we are interested in the logical meaning of resolution, then the resolution rule alone is not exactly sufficient. If we consider the set of clauses $[A, B] + [\neg A, \neg B]$, although inconsistent, it will never reach the empty clause $\neg$. Additional rules such as “factoring” or other logical simplifications have to be considered. Since this is a minor technical detail that will not be used in this thesis, we choose to ignore it.

§23.19 Resolution trees are constructed from top to bottom. Their construction is non-trivial. It is as if we were only using the cut rule in sequent calculus. For that reason, it is not

<footnote>$^8$Notice that it is actually an instance of monolateral cut rule (cf. Figure 11.1).</footnote>
clear at all how we should apply the resolution rule: it is possible to get stuck or to loop although there was a good series of choices leading to ⊥ (when it is possible to infer it). This is related to the fact that the satisfiability of formulas for predicate calculus is undecidable. Hence refutation is subject to the same problem since refuting $\neg A$ is equivalent to showing satisfiability of $A$.

§23.20 Logic programming is based on the resolution principle. However, strategies and constraints have to be designed in order to have a practical use of it. For instance, it is usually not necessary to consider multiple conclusions when reasoning. It is sufficient to consider implications $(A_1 \wedge \dots \wedge A_n) \Rightarrow B$ as shown in Section 23.

Reasoning with Horn clauses

§23.21 Horn clauses [Hor51, Tär77] are type of clauses which are easier to use for practical applications. They correspond to clauses with at most one positive literal (without negation). For instance $[\neg A, B, C]$ is not a Horn clause but $[\neg A, \neg B, C]$ is. The intuition is that such clauses correspond to implications “if ... then ...” of the shape $(A_1 \wedge \dots \wedge A_n) \Rightarrow B$ because

$$ (A_1 \wedge \dots \wedge A_n) \Rightarrow B \equiv \neg(A_1 \wedge \dots \wedge A_n) \vee B \equiv \neg A_1 \vee \dots \vee \neg A_n \vee B. $$

We will sometimes write the more convenient sequent notation $A_1, \dots, A_n \vdash B$ where $A_1, \dots, A_n, B$ are atoms instead<fnref n="9" />.

§23.22 It is possible to distinguish three classes of Horn clauses. Clauses

• $\vdash A$ with one positive atom and no negative ones, called *facts* (they are assumed);

• $A_1, \dots, A_n \vdash A$ with exactly one positive atom, called *inference rules*;

• $A_1, \dots, A_n \vdash$ with no positive atom, called *queries*.

These classes correspond to the three kind of elements we needed for logic programming (cf. Section 23). The idea is that a query $P(t) \vdash$ corresponds to a clause $[\neg P(t)]$ which can interact either directly with a unifiable fact $\vdash P(u)$ or a unifiable conclusion $P(u)$ of an inference rule $A_1, \dots, A_n \vdash P(u)$. In the latter case, we need to answer the new query $A_1, \dots, A_n \vdash$.

§23.23 **SLD-resolution.** In order to reason with a computer, several resolution strategies have been designed [KK71]. The SLD-resolution is a strategy which selects a clause (usually in a query) and makes it successively interact with other clauses linearly in order to produce a new resulting clause (called *resolvent*). SLD stands for selective-linear-definite. It is also possible to enrich set of clauses with an order so that a query will connect to the first matching clause, as in the logic programming language Prolog [CR96].

<footnote n="9">⁹Remark that Horn clauses in sequent notation correspond to intuitionistic sequents.</footnote>
<figure><img src="image_27.png" /><figcaption>Figure 23.5: Answer of the query $2 + 2 \vdash$ for unary addition with Horn clauses and SLD-resolution. When reaching $\perp$, we can read the result located in $R$ by unifying the values of variables. We have $Z' = Y'' = s(s(0))$, hence $Z = s(s(s(0)))$. And since $R = s(Z)$, we finally have the result $R = s(s(s(s(0)))$, meaning that $2 + 2 = 4$.</figcaption></figure>

§23.24 An example of application of SLD-resolution is given in Figure 23.5. Answers are given by finding a consistent term replacing free variables of the query. There can be several answers for all the free variables of the query or no answer at all. The answer can just be "Yes" if there is no free variable and we are just trying to justify a query seen as a goal.

§23.25 Logic programming had a huge impact during the rise of computer science as several various resolution systems have been built [Lei12, Sic76, Kow75]. It also led to variants of logic programming such as answer set programming (ASP) [Gel08, EIK09] or disjunctive logic programming [LRM91, Min94]. After declining for a long time, it is coming back again with recent works such as Andreoli's [And92] work or Miller's works [Mil21] relating proof theory (with applications to linear logic) and logic programming.

## 24 Discussion: the limits of the proof-program correspondence

Although it is not related to what I present in this section, some notes of Laurent Regnier (which I find very interesting) discuss the limits of the CHL correspondence<fnref n="10" />.

§24.1 **The strict meaning of CHL.** Remark that, strictly speaking, not all logical and computational systems are concerned by CHL.

* Only logical systems enjoying a cut-elimination theorem are considered. It is not the case of all logical systems. A dynamics of proofs is needed because otherwise

<footnote n="10">¹⁰https://www.i2m.univ-amu.fr/perso/laurent.regnier/articles/ch.pdf</footnote>
we would not be able to execute the corresponding programs<fnref n="11" />.

* Usually, typed functional systems are considered. Untyped λ-calculus can produce contradictions (cf. Paragraph 15.9) and is rejected from the correspondence for that reason. It is not “logical”.

It is a very specific correspondence which cannot be (yet?) extended to all logic and computation. I would like to stress this point: the CHL correspondence is a *historical coincidence*. Actually we do not learn so much apart that two communities were doing more or less the same thing with different vocabulary and methods. More pessimistic: it may even mean that we were *not able* to distinguish the notion of computation from the notion of logic. They are densely mixed together and we are more and more confused with the meaning of the objects we work with. What logic and computation are is still unclear at this point.

§24.2 It seems to me that there are currently three main understanding of the link between logic and computation. I illustrate these points of view in Figure 24.1.

* The first understanding in Figure 24.1a corresponds to the famous (and exaggerated) slogan “proving is programming” which is full of hopes, as if computer science colonised logic and tried to civilise it. However, we were not able to completely merge two cultures, thus obtaining a sort of fake multiculturalism.

- The C language, Java, Turing machines, Wang tiles, Babbage's engines are computational but are they logical?

- When I discuss with people and use logical arguments, when I am thinking, when I am doing mathematics, I am probably logical but do I always compute? With the classical meaning of computation?

Even if the answers to the previous questions were affirmative, it does not necessarily mean that logic and computation are the same but only that they are difficult to distinguish from our point of view. They could be two distinct (but difficult to separate) dimensions of reality.

* The point of view in Figure 24.1b is what I thought to be true at the beginning of my PhD thesis. In this point of view, the CHL correspondence is only an intersection between the notion of logic and computation. A perfect point where they match. This might be because logic and computation are about a lot of different things but they both have a common part speaking about the *process of construction* to reach a syntactic goal and an evaluation from the implicit to the explicit. But, under which basis can we judge that Turing machines are not

<footnote n="11">¹¹This is probably more profound than we think. I once had a discussion with Paul Séjourné and we reached the conclusion that if cut-elimination (or proof reduction) is a procedure from the implicit to the explicit, it is a sort of *explanation*. What cannot be executed cannot be explained. Logical systems without execution are hence *transcendent* in some sense. This is related to my reflection in Section 19.</footnote>
Logic = Computation

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

(a) CHL is the tip of an iceberg hiding a uniform logico-computational space. Proving is programming.

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

(b) CHL is the intersection between logic and computation. Some logics are not computational and some models of computation are not logical (Turing machines).

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

(c) It is all about point of view, representations and models. We can identify some parts of one to some parts of the other. Logic and computation are distinct entities which can be related.

<caption>Figure 24.1: Three nuances of Curry-Howard-Lambek (CHL). There are, of course, other points of view such as logic subsumed by computation or the converse. Since these point of view does not seem to have serious foundations, I decided to exclude them.</caption>
logical? If we consider an intersection, it looks like we already assumed a sharp
distinction between logic and computation in the first place.

* While the two first points of view are like atheism and theism, the third point of view illustrated in Figure 24.1c is more nuanced but still unclear about what logic and computation are. We know that there are two notions that we constructed and, depending on the point of view, we have different ways to relate them (corresponding to the three points of view given in the introduction of this chapter).

§24.3 I personally believe that suggesting a sharp and refined understanding of both logic and computation is *essential* in order to progress in the right direction for two reasons:

* in the computational world, there exists some barriers, especially in complexity theory where there are great difficulties at separating complexity classes. Those difficulties may be related to a lack of understanding of the nature of logic and computation. In particular, logic already has a role as a constraint (implicit computational complexity) or descriptor (descriptive complexity) of complexity classes;

* in the logical world, there are philosophical motivations in the understanding of the nature of reasoning but also of the relationship between thought, language and reality. In particular, computation (which can be thought as more concrete and down-to-earth) seems to be able to reach an explanation and a justification for reasoning.

§24.4 In this thesis, I defend another understanding of the relation between logic and computation which is closer to the point of view in Figure 24.1c while being consistent with the two previous points of view as well. According to me:

* computation may be about time/dynamics and logic about space/shape (logic regulates the space in which computation flows);

* models of computation are “logical” (probably a very controversial statement);

* logic and computation are completely distinct entities but which are strongly related and so densely mixed that we naturally work with logico-computational hybrid objects most of the time;

* CHL and proof search are two instances of such intertwined mix between logic and computation. In particular, they may both live in the same space;

* the computation-as-model subsumes the two kinds of computation-as-deduction;

* it is possible to separate the logical part from the computational part of a hybrid logico-computational entity.

§24.5 This point of view is based on Jean-Yves Girard's transcendental syntax programme. In order to explain what it is, we need to first start from linear logic and its developments. My point of view on logic and computation changed many times during my PhD thesis and this is what I would like to share in this dissertation. However, I do not have Girard's
confidence nor his pretension so I would like to make clear that I am fully aware that it
is only a suggestion that I find interesting and not the *final solution*. There are probably
still a lot of blind spots in my understanding of logic. What I suggest are mostly potential
directions and inspirations.
# Chapter 4

## Linear logic

Linear logic has been introduced by Jean-Yves Girard [Gir87a]. I will not present the history of linear logic in details as I do not know it very well and I do not think it is very important for this thesis. Hence, I will simply present a short summary and introduce linear logic directly from the sequent calculus. Historical notes can be found in Girard's seminal paper [Gir87a, Section V].

## 25 The emergence of linear logic

§25.1 During the rise of the Curry-Howard-Lambek correspondence, there was interests in the denotational semantics of λ-calculus where λ-terms enjoy a mathematical interpretation defining their meaning. If Λ is the set of all λ-terms then we need a space *D* of denotations (mathematical meaning) and an interpretation function [[·]] : Λ → *D*. Now, if λ-terms are interpreted by functions *D* → *D*, we have the usual paradox of set theory since it would lead to *D* ≅ *D* → *D*. We must then restrict the space of functions. Dana Scott's [Sco82] solution was to use domains and continuous function.

§25.2 Girard (who was working on functional interpretations and cut-elimination for second-order arithmetic) independently worked on alternative semantics by choosing category theory to interpret λ-terms by normal functors [Gir88]. This is in this context that a decomposition of the intuitionistic disjunction $A \vee B := !A \oplus !B$ was discovered. It is only later that this decomposition has been translated into simplified interpretations such as Girard's coherence semantics [Gir87a, Section 3] and a decomposition of intuitionistic implication $A \Rightarrow B := !A \dashv!B$ has been introduced. At that time, two types of semantics for the λ-calculus were studied:

* qualitative semantics studying the relationship between input and output (domains, Scott semantics, coherence spaces);

* quantitative semantics such as Girard's normal functors which takes into account occurrences and how much a portion of data of the output is used in the output. It can eventually feature coefficients which are useful for probabilistic considerations.
**§25.3** Although linear logic and all its main developments are usually attributed to Girard, several prefigurations or independent (accidental) definitions of (parts of) linear logic deserve to be mentioned:

* the modal logic S4 reasoning on possibility and necessity (introduced by Clarence Irving Lewis) [FY19];

* Lambek calculus studying the syntax of natural languages (introduced by Joachim Lambek) [Pen92];

* $\*-autonomous$ (star autonomous) categories (introduced by Michael Barr) [Bar91].

**26 Seizing the means of production**

**§26.1** The removal of logical principles can teach a lot and sometimes even adds more than the design of new rules. In intuitionistic logic, the removal of classical principles (either classical rule or constraining the space of conclusions) adds a straightforward constructivity and a direct connexion with typed $\lambda$-calculus. Structural rules (contraction and weakening) have already been mentioned in Paragraph 9.10. They make provability and truth *eternal* because we can do these operations as much as we want as if we had an infinite supply of formulas. But what happens if we forbid these rules and stop this machine of unlimited truth?

**§26.2 Substructural logics.** The removal of structural rules yields several interesting logical systems called *substructural logics* [Res02]:

* (strict or strictly) *linear logic* which forbids all structural rules and formulas are seen as limited resources. In particular, the implication $\Rightarrow$ becomes the linear implication $\nrightarrow$ which uses its argument exactly once. It is *linear* for several reasons but a simple explanation is that linear implication represent functions *linearly* consuming their input ($n$ inputs induce $n$ consumptions);

* *affine logic* where the affine implication $\nrightarrow$ uses its argument at most once, hence weakening is allowed on the hypothesis. It means that it is fine to erase formulas but we cannot have more than what we already have;

* *relevance logic* which requires a *real causality* between the hypothesis and the conclusion: weakening is not possible on the hypothesis but contraction is. We cannot have $A \wedge B \nrightarrow B$ because $B$ is not a direct consequence of $A$.

**§26.3** If we apply this to the typing of $\lambda$-calculus, then strict linear logic is a type system for $\lambda$-terms with abstractions $\lambda a.t$ where $a$ occurs only once in $t$. The $\beta$-reduction $(\lambda a.t)u \stackrel{\sim}{\rightarrow} \{a := u\}t$ only replaces a unique occurrence of $a$ by $u$. Among $\lambda$-abstractions which are already linear, we can find $\lambda a.a$ and, if we allow pairs: $\lambda a.\lambda b.(a, b)$ and $\lambda a.\lambda b.(b, a)$. As for affine logic, we have the two terms $\lambda a.\lambda b.a$ and $\lambda a.\lambda b.b$ because they erase one
argument. As far as I know, relevance logic is not as studied as linear and affine logic in the context of the λ-calculus.

**§26.4 Additive and multiplicative operations.** This chapter will be focussed on linear logic only. Something remarkable happens when we forbid all logical rules. As stated in Paragraph 10.2, multiplicative and additive rules<fnref n="1" /> of linear logic are equivalent but it is only thanks to structural rules. If we forbid structural rules then additive and multiplicative rules are different operations giving rise to different connectives. In particular, in Figure 10.3, in a bottom-up reading, ∧^m splits its context and ∧^a shares it. These two rules are two different ways of handling formulas seen as resources and they both deserve their own connective.

• For conjunction, ∧^a yields & (with) and ∧^m yields ⊗ (tensor);

• For disjunction, ∨^a yields ⊕ (plus) and ∨^m yields ℘ (par).

This decomposition also applies to neutral elements.

• For the truth constant, ⊤^a yields ⊤ (top) which is neutral for & and ⊤^m yields 1 (one) which is neutral for ⊗;

• For the falsity constant, ⊥^m yields ⊥ (bottom) which is neutral for ℘ and we have a new constant 0 (zero) which is neutral for ⊕ corresponding to an additive ⊥ (note that it has no rule).

The removal of structural rules *revealed* new connectives underlying the usual logical connectives, as if we opened the clock of logic to look at its mechanisms.

**§26.5 Linear negation.** The linear negation (or orthogonal, or dual) of a formula *A* is written *A*⊥ which have several pronunciations depending on your preferences: *A* orthogonal, *A* dual, *A* perp<fnref n="2" />. We have just defined strict linear logic by just taking classical monolateral sequent calculus (*cf*. Section 11) and removing structural rules. Negation is not affected by this removal. Linear negation is still involutive, *i.e*. we have *A* ≡ *A*⊥⊥ and De Morgan laws still hold for linear logic. In a more general setting (for instance bilateral sequent calculus), linear implication can be defined with *A* ⊢ *B* := *A*⊥ ℘ *B*. Linear equivalence *A* ≡ *B* can be defined with (*A* ⊢ *B*) ⊗ (*B* ⊢ *A*).

**§26.6 From prohibition to regulation.** Forbidding structural rules is too severe and the logical system we obtain is too weak. We would like to have the power of classical and intuitionistic logical back while keeping the distinct operators of additive and multiplicative rules. In linear logic, it is possible to decompose the intuitionistic implication *A* ⇒ *B* into !*A* ⊢ *B* where:

<footnote n="1">¹The terminology “additive” and “multiplicative” comes from interpretation of linear logic where for-
mulas are associated with sets: |A| ⊗ B| = |A| × |B| and |A&B| = |A| + |B| (which makes the term
“exponential” even more relevant). Such interpretations can be found in introduction to coherent
spaces [Gir87a, Section 3] (note that this is not the original presentation of linear logic).</footnote>

<footnote n="2">²If you say this one, you have very bad taste.</footnote>
<figure><img src="image_31.png" /><figcaption>Figure 26.1: Relations between linear logic connectives.</figcaption></figure>

• $\neg$ is a linear implication using its argument exactly once,

• !A (called “of course”) corresponds to a potentially infinite supply of A in the world of hypotheses, and

• ?A (called “why not”) is the negation of ! and corresponds to a potentially infinite demand of A in the world of conclusions.

Although it is not possible to prove $A \dashv\neg (A \otimes A)$ because A is used twice and $\dashv\neg$ is linear, it is possible to prove $!A \dashv\neg (A \otimes A)^3$. Note that because !A is on the left hand-side of $\dashv\neg$, it becomes $?A^\perp$ in monolateral sequent calculus. The connectives ! and ? are called exponential modalities or simply exponentials. They will be explained later after formally introducing a sequent calculus for linear logic.

§26.7 These exponential modalities are one way among others to reintroduce the infinite potential of provability. However, it is also possible to consider other ways to restrict duplication and erasure to have a finer control over formulas seen as resources. These variant of regulations are also related to computational complexity [Gir98, Laf04].

§26.8 Exponentials ! and ? correspond to infinitary cases for $\otimes$ and $\aleph$ respectively. This is illustrated by the two equivalences $!A \equiv !A \otimes !A$ and $?A \equiv ?A \aleph ?B$. Quantifiers $\forall$ and $\exists$ correspond to infinitary cases for $\&$ and $\oplus$ respectively. This is because they are both known to generalise conjunction and disjunction but which one, now that we have several ones? Universal quantification does not feature a “context splitting” so it must be $\&$. As for existential quantification, in a bottom-up reading, its rule chooses a unique candidate for existential witness, which corresponds to the destructive intuitionistic choice of $\oplus$ ($\forall^a$). Does multiplicative quantification make sense? I do not know.

<footnote n="3">³People learning linear logic (including me) tend to think that this was how linear logic was introduced but this is not exact. It seems that the decomposition of intuitionistic disjunction $A \vee B = !A \oplus !B$ has been clearly stated first [Gir87a, Section V.1] and the decomposition of implication has been introduced and propagated for pedagogical purposes [Gir87a, Section IV].</footnote>
$$A, B = X_i | X_i^{\perp} | A \otimes B | A \nparallel B \quad i \in \mathbf{N} \qquad (\mathcal{F}_{\text{MLL}})$$

$$A, B = X_i | X_i^{\perp} | A \otimes B | A \nparallel B | A \& B | A \oplus B \quad i \in \mathbf{N} \qquad (\mathcal{F}_{\text{MALL}})$$

$$A, B = X_i | X_i^{\perp} | A \otimes B | A \nparallel B | !A | ?A \quad i \in \mathbf{N} \qquad (\mathcal{F}_{\text{MELL}})$$

$$A, B = X_i | X_i^{\perp} | A \otimes B | A \nparallel B | A \& B | A \oplus B | !A | ?A \quad i \in \mathbf{N} \qquad (\mathcal{F}_{\text{LL}})$$

<caption>Figure 27.1: Formulas of linear logic.</caption>

§26.9 We obtain the relations between connectives illustrated in Figure 26.1 (taken from Olivier Laurent's course notes<fnref n="4" />). Linear negation relates connectives with:

$$(A \otimes B)^{\perp} = A^{\perp} \nparallel B^{\perp} \qquad (A \nparallel B)^{\perp} = A^{\perp} \otimes B^{\perp} \qquad 1^{\perp} = \perp \qquad \perp^{\perp} = 1$$

$$(A \& B)^{\perp} = A^{\perp} \oplus B^{\perp} \qquad (A \oplus B)^{\perp} = A^{\perp} \& B^{\perp} \qquad \top^{\perp} = 0 \qquad 0^{\perp} = \top$$

$$(!A)^{\perp} = ?A^{\perp} \qquad (?A)^{\perp} = !A^{\perp} \qquad (\forall x.A)^{\perp} = \exists x.A^{\perp} \qquad (\exists x.A)^{\perp} = \forall x.A^{\perp}$$

and exponentials relate connectives with:

$$!(A \& B) \equiv !A \otimes !B \qquad ?(A \oplus B) \equiv ?A \nparallel ?B \qquad !\top \equiv 1 \qquad ?0 \equiv \perp$$

More relations can be found in Lafont's "Linear Logic Pages" [Laf99]. The reason exponentials are called exponentials is because they act like exponentials on numbers. If we interpret $\otimes$ by $\times$ and $\&$ by $+$ then, the equivalence $!(A \& B) \equiv !A \otimes !B$ corresponds to $e^{a+b} = e^a e^b$.

§26.10 **The forgotten case of exchange.** Technically speaking, the exchange rule is a structural rule as well. However it will not be covered at all in this thesis and the exchange rule will always be considered implicitly (it can be made explicit when needed). Removing the exchange rule leads to *non-commutative linear logic* where the order of arguments of binary connectives is relevant. It is not widely studied in linear logic but it has been studied by Abrusci [Abr91, AR99]. It is also related to linguistics where order matters as in Lambek's works on categorical grammars.

## 27 Classical linear logic sequent calculus

§27.1 Linear logic is usually introduced with several fragments, each having their own characteristics. Some fragments are also studied on their own. The grammar of formulas for the main fragments of linear logic are presented in Figure 27.1. We exclude first-order and second-order quantification because the rules are the same as in classical logic.

<footnote n="4">⁴https://perso.ens-lyon.fr/olivier.laurent/thdem11.pdf</footnote>
$$ \begin{array}{ccc} \text{ax} & \frac{\vdash \Gamma, A \quad \vdash \Delta, A^{\perp}}{\vdash \Gamma, A^{\perp}} & \text{cut} \quad \frac{\vdash \Gamma, A \quad \vdash \Delta, B}{\vdash \Gamma, \Delta, A \otimes B} \otimes \frac{\vdash \Gamma, A, B}{\vdash \Gamma, A, B} \not\vdash \} \\ \text{(a) Multiplicative Linear Logic.} & & \end{array} $$

$$ \frac{\vdash \Gamma, A \quad \vdash \Gamma, B}{\vdash \Gamma, A \& B} \& \quad \frac{\vdash \Gamma}{\vdash \Gamma, ?A} \quad \text{w} \quad \frac{\vdash \Gamma, A}{\vdash \Gamma, ?A} \quad \text{d} $$

$$ \frac{\vdash \Gamma, A_i}{\vdash \Gamma, A_1 \oplus A_2} \oplus_i \quad \frac{\vdash \Gamma, ?A, ?A}{\vdash \Gamma, ?A} \quad \text{c} \quad \frac{\vdash ?\Gamma, A}{\vdash ?\Gamma, !A} \neq! $$

(b) Additive rules.

(c) Exponential rules.

$$ \frac{\overline{\vdash 1}}{\vdash 1} \quad \frac{\vdash \Gamma}{\vdash \Gamma, \perp} \perp \quad \frac{\overline{\vdash \Gamma, \top}}{\vdash \Gamma, \top} \top $$

(d) Neutral elements.

<caption>Figure 27.2: Full Linear Logic (LL)</caption>

* Multiplicative linear logic (MLL) is the simplest fragment and treats the most elementary operations of reasoning such as the linear implication $\to$.

* Multiplicative-Additive linear logic (MALL) is an extension of MLL with operations managing choices during the process of proving. Purely additive linear logic (ALL) is sometimes studied by itself as well.

* Multiplicative-Exponential linear logic (MELL) is an extension of MLL which allows the duplication and erasure of formulas seen as resources.

Full linear logic (LL) corresponds to a system allowing all these principles. For a fragment $C$ of linear logic, we will write $C_u$ for the extension of $C$ with units (neutral elements). For instance, MLL with units is $\text{MLL}_u$ and its set of formulas is $\mathcal{F}_{\text{MLL}_u}$.

## Multiplicative fragment

§27.2 The sequent rules of MLL are presented in Figure 27.2a. MLL reveal a very simple symmetry and interaction in logic but also in computation. The relation with programming is nicely explained by Curien in his article "Symmetry and interactivity in programming" [Cur03]. If $A$ is seen as a supply of limited resource then $A^{\perp}$ can be interpreted as a demand of this resource. The axiom rule can then be interpreted as meeting offer and demand: we consume what we have. It is very similar to the supply/demand of classical monolateral sequent calculus (cf. Section 11) except that in linear logic, resources are limited and consumed.
$$ \frac{\overline{\vdash A, A^{\perp}}^{ax} \quad \vdash A, \Gamma}{\vdash A, \Gamma} \text{ cut} \rightsquigarrow \vdash A, \Gamma $$

$$ \frac{\vdash \Gamma, A \quad \vdash \Delta, B \quad \vdash \Xi, A^{\perp}, B^{\perp}}{\vdash \Gamma, \Delta, A \otimes B} \otimes \frac{\vdash \Xi, A^{\perp}, \mathfrak{g} B^{\perp}}{\vdash \Gamma, \Delta, \Xi} \text{ cut} \rightsquigarrow \frac{\vdash \Delta, B \quad \vdash \Xi, A^{\perp}, B^{\perp}}{\vdash \Gamma, \Delta, \Xi} \text{ cut} $$

(a) Multiplicative fragment. Just a rewiring.

$$ \frac{\vdash \Gamma, A_1 \quad \vdash \Gamma, A_2 \quad \vdash \Delta, A_k^{\perp}}{\vdash \Gamma, A_1 \ \& \ A_2} \oplus_k \frac{\vdash \Delta, A_1^{\perp} \oplus A_2^{\perp}}{\vdash \Gamma, \Delta} \text{ cut} \rightsquigarrow \frac{\vdash \Gamma, A_k \quad \vdash \Delta, A_k^{\perp}}{\vdash \Gamma, \Delta} \text{ cut} $$

(b) Additive fragment. Allows choices.

$$ \frac{\frac{\vdash ?\Gamma, A \quad \vdash \Delta}{\vdash ?\Gamma, !A \quad \vdash \Delta, ?A^{\perp}} \text{ w}}{\vdash ?\Gamma, \Delta} \text{ cut} \rightsquigarrow \frac{\vdash \Delta}{\vdash ?\Gamma, \Delta} \text{ w} $$

$$ \frac{\frac{\vdash ?\Gamma, A \quad \vdash \Delta, A^{\perp}}{\vdash ?\Gamma, !A \quad \vdash \Delta, ?A^{\perp}} \text{ d}}{\vdash ?\Gamma, \Delta} \text{ cut} \rightsquigarrow \frac{\vdash ?\Gamma, A \quad \vdash \Delta, A^{\perp}}{\vdash ?\Gamma, \Delta} \text{ cut} $$

$$ \frac{\frac{\vdash ?\Gamma, A \quad \vdash \Delta, ?A^{\perp}, ?A^{\perp}}{\vdash ?\Gamma, !A \quad \vdash \Delta, ?A^{\perp}} \text{ c}}{\vdash ?\Gamma, \Delta} \text{ cut} \rightsquigarrow \frac{\frac{\vdash ?\Gamma, A \quad \vdash ?\Gamma, !A \quad \vdash \Delta, ?A^{\perp}, ?A^{\perp}}{\vdash ?\Gamma, \Delta, ?A^{\perp}} \text{ cut}}{\frac{\vdash ?\Gamma, ?\Gamma, \Delta \quad \vdash ?\Gamma, \Delta}{\vdash ?\Gamma, \Delta} \text{ c}} $$

$$ \frac{\frac{\vdash ?\Gamma, A \quad \vdash ?\Delta, ?A^{\perp}, B}{\vdash ?\Gamma, !A \quad \vdash ?\Delta, ?A^{\perp}, !B} \text{ !}}{\vdash ?\Gamma, ?\Delta, !B} \text{ cut} \rightsquigarrow \frac{\frac{\vdash ?\Gamma, A \quad \vdash ?\Gamma, !A \quad \vdash ?\Delta, ?A^{\perp}, B}{\vdash ?\Gamma, ?\Delta, ?B} \text{ !}}{\vdash ?\Gamma, ?\Delta, !B} \text{ cut} $$

(c) Exponential fragment. Applies operations (duplication, erasure, linearisation) on a box containing A.

$$ \frac{\overline{\phantom{\Gamma}} 1 \quad \overline{\Gamma} \quad \perp}{\vdash 1 \quad \vdash \Gamma, \perp} \text{ cut} \rightsquigarrow \vdash \Gamma $$

(d) Neutral elements. Please tell me what it means because I do not know.

<caption>Figure 27.3: Main cut-elimination cases for linear logic.</caption>
<figure><img src="image_32.png" /><figcaption>Figure 27.4: Examples of proofs in multiplicative linear logic.</figcaption></figure>

§27.3 Cut-elimination cases are presented in Figure 27.3. They are the same as for classical sequent calculus and also enjoy the same computational interpretation. The cut-elimination between $\mathcal{N}$ and $\otimes$ is simply a rewiring of interaction (the left premises and right premises are connected together).

§27.4 MLL alone is sufficient as a linear type systems for $\lambda$-calculus as it is able to express the linear implication $A \to B = A^{\perp} \mathcal{N} B$. In particular, the linear modus ponens is purely multiplicative. But if we do not limit types to implications, then it is also possible to interpret pairs $(a, b) : X_1 \otimes X_2$. Even though the usual encoding of booleans are the affine terms $\lambda a. \lambda b. a$ and $\lambda a. \lambda b. b$, it is possible to define *linear booleans* with $\lambda a. \lambda b.(a, b) : X_1 \to X_1 \to X_1 \otimes X_1$ and $\lambda a. \lambda b.(b, a) : X_1 \to X_1 \to X_1 \otimes X_1$. Linear booleans are used to relate boolean circuits and proofs of MLL [Ter04].

§27.5 **Note on booleans.** The difference between the usual affine booleans and linear booleans is that boolean in MLL cannot be erased. Moreover, to keep computation linear, we have to keep some *garbage*, i.e. useless parts which will not be erased but ensure that we are in a linear world. The advantage is that linear booleans enjoy a more convenient interpretation of exclusive disjunction (XOR) [MT15, MT03]. Recently, Lê Thành Dũng Nguyễn (aka “Tito”) also introduced a non-commutative linear type for booleans [Ngu21, Section 7.2].

§27.6 An example of proof in MLL is given in Figure 27.4. The first proof is a proof of $(X_1 \otimes X_2) \to (X_1 \otimes X_2)$ which can be seen as the linear $\lambda$-term $\lambda(a,b).(a,b)$. The second proof is more subtle. It corresponds to a type derivation for the typing sequent $b : X_1 \vdash (\lambda a. a)b : X_1$ where $b$ is a free variable of type $X_1$ (which becomes $X_1^{\perp}$ by duality of monolateral sequent calculus). The left branch of the cut represents the function $(\lambda a. a) : X_1 \to X_1 = X_1^{\perp} \mathcal{N} X_1 \equiv X_1 \mathcal{N} X_1^{\perp}$. The connective $\otimes$ connects the argument $b : X_1^{\perp}$ together with an output of type $X_1$.

§27.7 **Non-idempotent intersection types.** There exists alternative ways to type terms. Another way is given by intersection types which type terms with conjunction of types $A \wedge B$ called *intersection types* [DC18]. The difference is that, instead of the computational interpretation with pairs, the expression $\vdash M : A \wedge B$ says that $M$ has two types or two behaviours. For instance, the term $\lambda x.xx$ is not typable with the usual simple types because $x$ is used both as a function $x : \alpha \to \beta$ but also as an argument
$x : \alpha$ of a function of type $\alpha \to \beta$. However, it cannot have both types since $\alpha \to \beta$ cannot be unified with $\alpha$. Nonetheless, it can be typed in intersection type systems with $\vdash \lambda x.xx : \alpha \wedge (\alpha \to \alpha) \to \alpha$ taking into account the two behaviours of $x$. In the non-idempotent case, we have that $A \wedge A$ is not equivalent to $A$, hence intersections are seen as collections of resources, exactly as in linear logic. Actually, $\wedge$ corresponds to $\otimes$ in this case. The advantage of non-idempotent types systems is that they can capture strong normalisation (termination) of terms but consequently, type checking becomes undecidable (otherwise we would be able to solve the Halting problem described in Paragraph 16.14). Intersection types can also be used for considerations on computational complexity as in Mazza's works [Maz17, Section 3.3.5].

## Neutral elements

§27.8 The rules for neutral elements (also called units) are presented in Figure 27.2d. The constants 1 and $\top$ are two sort of trivial statements (one without context and the other possibly within a context). The constant $\bot$ is an "acceptable error" which can be discarded. It represents an unprovable goal but other paths can be taken in $\Gamma$. Remark that if $\Gamma = \emptyset$ then we can be stuck with $\bot$. The constant 0 has no rule and represents a "fatal error".

§27.9 Cut-elimination for neutral elements is presented in Figure 27.3d. Because 0 is a fatal error, it cannot interact by cut-elimination. There is a rule for the interaction between 1 and $\bot$ but I do not know how to give an interesting interpretation of it so you can just look at it without comment.

## Additive fragment

§27.10 The additive rules are presented in Figure 27.2b. As in monolateral sequent calculus, they express binary non-deterministic choices. The formula $A \& B$ can be understood as a superposition (passive choice) between a proof of $A$ and a proof of $B$ requiring the same context $\Gamma$ and proofs of $A \oplus B$ are binary selectors (active choice).

§27.11 In MALL, it is possible to have another encoding of booleans which is closer to usual (functional) programming. A boolean is either a constant True or a constant False, which can be represent by the type **Bool** := 1 $\oplus$ 1. The proofs of **Bool** are either a left selection (representing True) or a right selection (representing False). The constants True and False are hence represented by proofs, accordingly to the CHL correspondence. They should not be confused with constants 0, 1, $\top$, $\bot$ which are types/formulas and not proofs. False is an object which can be used (for instance in conditions) whereas $\bot$ and 0 are types/formulas representing two sort of errors.
$$ \frac{\frac{\vdash \Gamma, A, \perp \quad \vdash \Gamma, A, \perp \quad \& \quad \vdash 1}{\vdash \Gamma, A, \perp \& \perp} \oplus 1}{\vdash \Gamma, A} \quad \rightsquigarrow \quad \frac{\vdash \Gamma, A, \perp \quad \vdash 1}{\vdash \Gamma, A} \quad \text{cut} \quad \rightsquigarrow \quad \vdash \Gamma, A $$

<caption>Figure 27.5: Example of proof using additive connectives. It represents the use of a condition. The formula A represents the output of the condition. The point is that the two branches of the rule & can be two different proofs (terms) of the same sequent.</caption>

§27.12 If we look at cut-elimination for additive connectives in Figure 27.3b, we can see that depending on whether the proof of $A_1^\perp \oplus A_2^\perp$ is a left ($\oplus_1$) or right selection ($\oplus_2$), it will only select one side of & and erase the other. Conditions can be represented with the connective &. However, the correspondence is not so exact. Consider a condition if *b* then *x* else *y* applied to true. The result should be *x*. This situation is represented by a cut-elimination between the condition and the boolean value. However, cut-elimination produces a new cut between the boolean value and the selected branch. If we assume that the two branches are of type $A_1$ and $A_2$, the result our interaction cannot be of type $A_1$ because it would disappear after its interaction with $A_1^\perp$. Only the contexts $\Gamma$ and $\Delta$ remain. Therefore, it we would like to encode conditions, the connective & must link two occurrences of $\perp$ artificially added in the encoding of the condition, so that it annihilates the constant 1 of the encoding of booleans. This is illustrated in Figure 27.5. Remark that the & connective now links those two occurrences of $\perp$ instead of the terms of the two branches of the condition. The condition must then have two branches of same type A.

§27.13 **Comment on linear equivalence.** In Paragraph 26.5, we defined the linear equivalence $A \equiv B$ as $(A \not\to B) \otimes (B \not\to A)$. However, there is an alternative definition with $(A \not\to B) \& (B \not\to A)$. In a lot of cases, these definitions are equivalent because the rule for $\otimes$ and $\&$ are equivalent in an empty context. They both prove either $\vdash A \& B$ or $\vdash A \otimes B$ from $\vdash A$ and $\vdash B$. There is no problem when equivalence is considered *alone* (for formulas $A \equiv B$ for any $A$ and $B$). However, when equivalence is negated (typically when it appears on the left of a linear implication), then depending on the chosen definition, we obtain either $(A \not\to B)^\perp \oplus (B \not\to A)^\perp$ or $(A \not\to B)^\perp \not\to (B \not\to A)^\perp$ which do not have the same behaviour since $\not\to$ keep premises in the same space of interaction and $\oplus$ makes an exclusive choice. For instance, if we consider the transitivity of equivalence $(A \equiv B) \otimes (B \equiv C) \not\to (A \equiv C)$, it is provable for $\otimes$ but not for $\&$. This example is illustrated in Figure 27.6.
Exponential fragment

§27.14 The rules for exponentials are presented in Figure 27.2c. Only connectives prefixed by the connective “?” can be duplicated or erased. The rule “d” is called *dereliction*<fnref n="5" />. From a bottom-up reading, it corresponds to linearising a formula so that duplication and erasure does not apply any more. From a top-down reading, it makes a linear formula non-linear. The most mysterious rule is the rule “!” called *promotion*. This rule wraps a linear formula with the connective !, but this is only possible when the context is fully non-linear. This connective is better understood when looking at cut-elimination.

§27.15 The cut-elimination steps for exponentials are presented in Figure 27.3c. I know they look scary but they are actually very intuitive. The rule ! on !A constructs a sort of box encapsulating A in a non-linear context. This box can then interact with a non-linear formula:

• in a $w/!$ interaction, the box is erased;

• in a $d/!$ interaction, the box is opened and its content $A$ interact with the linearised formula $A^\perp$;

• in a $c/!$ interaction, the box is duplicated<fnref n="6" />;

• in a $!/!$ interaction, what happens is more spectacular. This is a commutation case where two ! are related but do not interact directly. One wishes to interact with something deeper in the proof. For that reason, one box *enters* inside the other one.

§27.16 **Intuitionistic and classical translations.** Intuitionistic logic can be defined from linear logic. There are two translations introduced by Girard.

• $[[X_i]] = X_i$ and $[[A \Rightarrow B]] = ![[A]] \dashv [[B]]$ (the original translation which gave rise to linear logic). Non-linearity applies on the argument;

• $[[X_i]] = !X$ and $!([[[A]] \dashv [[B]]])$. Non-linearity applies on the whole implica-
tion/function.

It is possible to define a translation for classical logic by choosing the right combinations
of ! and ? to wrap formulas (which are known as *q*-translation and *t*-translation for the
systems LKQ and LKT [DJS95]) or using the formalism of *polarised linear logic* [LR03].

<footnote n="5">⁵According to the dictionary it means “failing to do what you should do”. In French, it is a literary word referring to a state of moral abandon or loneliness.</footnote>

<footnote n="6">⁶Because of this duplication, we can think that cut-elimination will not terminate but it actually does. It is sufficient to find a measure which decreases during cut-elimination. Methods for proof of termination can be found in the literature [BN98, Chapter 5].</footnote>
<figure><img src="image_33.png" /><figcaption>Figure 27.7: The lattice of exponentials modalities. The dot · represents the absence of modality.</figcaption></figure>

§27.17 Exponentials can be used to reconstruct a type system for simply typed λ-calculus (since linear logic decomposes intuitionistic logic). A type assertion Γ ⊢ M : A becomes ⊢ ?Γ⊥, A. The idea is that boxes represent arguments (the N in (λx.M)N). When applying the β-reduction which replaces all x in M by N, several types of operation can be done. The term N can be erased (if x does not appear in M) and it can also be duplicated (if several occurrences of x appear in M). It may also be possible to imagine other logical operations by thinking about what computational operation we would like to apply on an argument. By using λ-calculus, it is also possible to give an interpretation to the two intuitionistic translations. They correspond to two *evaluation strategies* for β-reduction known as “call-by-name” and “call-by-value” evaluation [MOTW99, Wad03]. The first evaluates functions first and the second the arguments first.

§27.18 **Hybrid calculi for linear logic.** The interpretation of simply typed λ-calculus corresponds to a restricted (intuitionistic) subset of MELL where we only consider non-linearity but it is also possible to construct a λ-calculus mixing both linearity and non-linearity [ABCJ98, ACJ97]. It is also possible to find a presentation and several extensions in Mazza's HdR thesis [Maz17, Section 1.1.2].

§27.19 **The lattice of linear modalities.** Not all combinations of exponential connectives such as !!!A or ?!??A can be distinguished. If the formula !A is interpreted as a potentially infinite supply of A then it is not so surprising that we have !!A ≡ !A (this is proven in Figure 27.8a). A combination of ! and ? is called a *modality*. In his PhD thesis, Joinet remarks that for any modalities μ, we have !A ⊢ μA and μA ⊢ ?A [Joi93, Section 5.2]. This induces an order over modalities. From that, he deduces a lattice of exponential modalities and distinguishes 7 equivalence classes presented in Figure 27.7. As a corollary, we have that all modalities are idempotent: for any modality μ, μA ≡ μμA. This has later been presented by Schellinx as well in his PhD thesis [Sch94, Section 1.1]. Similar facts also appeared independently in modal logic (especially S4) [FY19].

§27.20 Examples of proofs in MELL are presented in Figure 27.8. The third example in Fig-
<figure><img src="image_34.png" /></figure>

(a) Proof that limitlessness of limitlessness is limitlessness.

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

(b) Proof that exponentials link the additive and multiplicative conjunction.

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

(c) Type derivation for $(\lambda x.x)y$ in MELL.

Figure 27.8: Examples of proofs in multiplicative-exponential linear logic.
$$ \frac{\vdash \Gamma, ??A \quad \text{dig} \quad \vdash \Gamma, A \quad f!}{\vdash \Gamma, ?A} \quad \frac{\vdash ?\Gamma, !A \quad \text{dig}}{\vdash ?\Gamma, !A} $$

<caption>Figure 27.9: Rules for digging and functorial promotion (also called weak promotion). A proof that promotion can be derived from digging and functorial box is given.</caption>

$$ \frac{\vdash \Gamma, A, \dots, A \quad \text{mux}(n)}{\vdash \Gamma, ?A} \quad \frac{\vdash \Gamma, A \quad \text{mux}(1)}{\vdash \Gamma, ?A} \quad \frac{\vdash \Gamma \quad \text{mux}(0)}{\vdash \Gamma, ?A} \quad \frac{\vdash \Gamma, ?A, ?A \quad \text{mux}(2)}{\vdash \Gamma, ??A \quad \text{dig}} $$

<caption>Figure 27.10: Rules for multiplexing and derivation of other structural rules.</caption>

ure 27.8c is the exponential version of the type derivation of the linear term $(\lambda a.a)b$ in Figure 27.4. Remark that the argument is put in a box. If we had a contraction or weakening on the side of the function (? rule on the left), then it would trigger a duplication or erasure of the argument inside the box (! rule on the right).

**§27.21 Alternative exponentials.** Several variant of exponential rules exist. For instance, the digging and functorial promotion rules in Figure 27.9 can replace the promotion rule. These rules are useful for categorical interpretations or in implicit computational complexity using linear logic (especially light linear logics [Gir98] such as ELL and SLL). It is also possible to consider a *multiplexing* rule splitting ?A by duplicating it into n linearised copies. We obtain the following equivalences of rules:

* promotion ≅ functorial promotion + digging;

* dereliction + weakening ≅ multiplexing.

# 28 Some applications and intuitive interpretations

**§28.1 Logic of resources.** The most straightforward interpretation is that linear logic is a logic of limited resources and control over resources. It seems that it has generated a quite important type of “linear typing” in (functional) programming [Wad90] with implementations in Haskell or Rust. It is consistent with functional languages’ philosophy of strong typing<fnref n="7" /> where we would like to prevent unwanted behaviours of a program.

<footnote n="7">⁷I remember that during a course of compilers, Yann-Régis Gianas told us that there was a sort of duality between weakly typed languages such as Python who consider that programmers know what they are doing and should be free to do so (for instance condition returning objects of different types in the two branches) and strongly typed languages such as OCaml where programmers are considered dumb so the system limits what they can do so that they will not unintentionally break something</footnote>
Linear types can ensure that some data will never be duplicated or erased, and they could be used to represent “read-only” operations which can guarantee the safety of data. Typically, money is also a limited resource which can be regulated. It may be possible to use linear types to verify economic operations, as suggested by some vague applications to blockchain technologies [Mer15].

§28.2 Still in this interpretation of a logic of resources, biology, chemistry and physics also work with consumable entities. The chemical reactions mentioned in Paragraph 12.10 are linear. In the chemical equation $2H_2 + O_2 \rightarrow 2H_2O$, the relation $\rightarrow$ can be rewritten with $\to$ to signify that the same amount of input resources is found in the output: nothing is lost, nothing is created. However I am not aware of important works in that direction. As for biology, there exists few works relating biological systems and linear logic systems [dMDF+20, DFLO19, Des16].

§28.3 **Logic and games.** Logic has been related to the idea of game in several ways by several authors such as Gentzen, Lorenzen (in his "Logik und Agon") and Hintikka. Proving a statement can be seen as a dialogue between a prover and someone to convince. Hintikka imagines a language game between us and the "nature" [HS97]. This dialogue becomes even more explicit with linear logic.

• The connective $\&$ can be interpreted as a passive choice from “our side”. Its rules shows that we can consume all the resources $\Gamma$ to produce either $A$ or $B$ and it will works in the two cases. The formula $A \not\sim B$ is a way to express the fact that we wish to keep $A$ and $B$ in the same space of interaction. Both $\&$ and $\not\sim$ are risk-free moves for “us”. They have no influence on provability.

• The connective $\otimes$ is an active choice since we have to choose how to split the context. It is the same for $\oplus$ where we can either choose the left or right premise. However, these choices are not risk-free. We can make wrong choices. In some sense, it is the “nature” who chooses where provability is hidden.

We remark that $\&$ and $\not\sim$ are *reversible*. They are called *negative* (passive) connectives. As for $\oplus$ and $\otimes$, they are *irreversible*. They are called *positive* (active) connectives. These two classes of connectives are related by negation which can be seen as a change of point of view: “we” becomes “they” and vice-versa.

§28.4 Cut-elimination can then be interpreted as actually triggering a dialogue or a sort of battle in a game:

• in a $\not\sim/\otimes$ cut-elimination, a player ($\not\sim$) suggests two arguments $A$ and $B$ waiting in its space of interaction as a sort of question and the other player ($\otimes$) creates two threads in order to answer $A$ and $B$;

<footnote>somewhere. It was told in the tone of a joke but I think that it was actually very profound (and almost political).</footnote>
* in a $\&/\oplus$ cut-elimination, a player ($\&$) suggests two options by proposing the other player to either play against $\vdash \Gamma, A$ or $\vdash \Gamma, B$. Then, the other player ($\oplus$) makes a choice.

In the context of linear logic, a *game semantics* has been proposed by several authors but we can cite Blass [Bla92] and Abramsky [AJ94] among others. True/provable formulas will correspond to players having a “winning strategy”. In the simple case of axioms, a player of $A^{\perp} \not\models A$ is expected to win against $A \otimes A^{\perp}$. This interpretation with games makes linear logic a *logic of actions* as well as a logic of resources.

**§28.5** In Girard's ludics [Gir01], synthetic rules are considered: there is only one positive rule and one negative rule. In this particular case, dialogue can be infinite and a player wins when the other abandon with a special axiomatic rule called “Daimon” which proves anything. Ludics is used as a tool in the analysis of dialogues as explained in Fouquéré et al. “*Mathématique du dialogue*” (French book) and has been recently applied in the analysis of dialogues with schizophrenic individuals [FPQ21].

**§28.6** **Processes and sessions.** An early interpretation was also that linear logic was a *logic of interaction* [Abr16, Chapter 5]. In programming, concurrent programming studies the (usually asynchronous) interaction between independent agents which transmit information locally. Some languages such as the $\pi$-calculus [iln90] are dedicated to such systems of communication. Another form of communication are *sessions*. It happens that a (web) client communicate with a server by opening a session. During this session, several messages will be transmitted. At the end the session is closed. It appears that linear logic is able to type processes [Abr94] and sessions [Wad12]. This leads to an extension of the CHL correspondence with proofs as processes and formulas as session/process types. By using realisability theory (cf. Section 22), Emmanuel Beffara has suggested attempts at reconstructing linear logic from $\pi$-calculus. This realisability interpretation allows to use linear logic as a tool to study the behaviour of processes [Bef06].

**§28.7** **Logic programming and linear logic.** In the previous interpretations of linear logic with games, multiplicative and additive linear logic are classified into reversible and irreversible connectives. A consequence is that rules of reversible connectives can always been applied before any irreversible rules. From this fact, Jean-Marc Andreoli [And92] developed the idea of *focussing*. It is possible to consider strategies of proof by alternating between reversible and irreversible rules. This gave rise to several applications of linear logic to logic programming. More information can be found in Dale Miller's survey [Mil95].

## 29 Proof-structures and proof-nets

**§29.1** Until now, only sequent calculus for linear logic has been mentioned. But what about natural deduction? The advantage of natural deduction is that it is a quotient on
<figure><img src="image_37.png" /><figcaption>Figure 29.1: Two sequent calculus proofs of linear logic equivalent up to permutation of rules.</figcaption></figure>

<figure><img src="image_38.png" /><figcaption>Figure 29.2: Natural deduction rules for tensor.</figcaption></figure>

sequent calculus proofs: a single natural deduction proof potentially corresponds to several sequent calculus proofs. In Figure 29.1, we have two proofs of a same sequent. They only differ by the order of $\otimes$ rules. One can be applied before the other without risking to lose provability. The same thing occurs if we permute $\mathfrak{N}$ rules.

§29.2 As remarked by Girard [Gir11a, Section 11.1.5], it is possible to define a natural deduction for linear logic. The introduction and elimination rules for tensor are presented in Figure 29.2. The introduction rule is natural and not surprising. The elimination rule, on the other side, is not sufficient at all. It suffers from the same problem as for the rule $\forall e$ and will lead to complications although tensor is a very basic connective with a simple behaviour. In linear logic, negation is involutive and inputs can be seen as negated formula. Hence, because of the morphologic constraint of natural deduction, $[A]$ and $[B]$ are sort of wannabe negated conclusion formulas but an artificial bending through $C$ appears instead. For that reason, we can do better by choosing a structure of proofs which is a not tree-shaped stacking of rules. We have to find another way to capture the essence of proofs by providing a syntactic format in which proofs can express everything that have to say<fnref n="8" />.

<footnote n="8">⁸In the same fashion, Japanese square watermelons are grown in square boxes in order to obtain a square shape. This shape is more convenient to cut or to carry. More generally, you can think of the process of dwarfing in plants or animals. Another (sadder) example that I have learnt recently is that goldfishes growing in a fish bowl are subject to a painful dwarfing.</footnote>
<figure><img src="image_39.png" /><figcaption>Figure 29.3: Underlying formula graphs of the proofs of Figure 29.1.</figcaption></figure>

$$ \frac{\begin{array}{c} \vdash \Gamma, A, B, C, D \\ \vdash \Gamma, A, B, C \mathcal{N} D \\ \vdash \Gamma, A \mathcal{N} B, C \mathcal{N} D \end{array}}{\mathcal{N}} \quad \begin{array}{c} \mathcal{N} \\ \mathcal{N} \\ \mathcal{N} \end{array} \quad \leftrightarrow \quad \frac{\begin{array}{c} \vdash \Gamma, A, B, C, D \\ \vdash \Gamma, A \mathcal{N} B, C, D \\ \vdash \Gamma, A \mathcal{N} B, C \mathcal{N} D \end{array}}{\mathcal{N}} \quad \begin{array}{c} \mathcal{N} \\ \mathcal{N} \\ \mathcal{N} \end{array} $$

Figure 29.4: Commutation rule for $\mathcal{N}$. It states the equivalence of two proofs up to permutation of rules.

## Multiplicative unit-free proof-nets

§29.3 The skeleton of the essence of proofs. If we look at the two previous sequent calculus proofs of Figure 29.3, we remark that $\mathcal{N}$ splits two formulas kept in the same space of interaction and $\otimes$ distributes two formulas in disjoint spaces of interaction. By following how rules do these operations, it is possible to construct a graph linking formulas. Each node $A \otimes B$ (respectively $A \mathcal{N} B$) or the graph are connected to A and B in the top. The two proofs (which are equivalent up to permutation of rules) have the same graph. These graphs are then appropriate candidate for the essence of proofs where (almost) all superfluous information is removed. This ability to quotient proofs which are equivalent for wrong reasons is often called canonicity. Translation of proofs to such graphs should be invariant up to commutation rules such as the one presented in Figure 29.4. Sequent calculus proofs can then be seen as sequential recipes (algorithms?) to construct those graphs that Girard called a “parallel syntax” for proof theory [Gir96]. Those graphs are called proof-nets and they only make explicit how formulas are structurally related in a proof.

§29.4 Before introducing proof-nets, we introduce proof-structures which is the format in which proofs will now live<fnref n="9" />. They are purely computational and alogical graphs linking formulas. In the same spirit as Girard’s ludics [Gir01], “only location matters” at this point. The idea is that when considering the structure of proofs, formulas are nothing more

<footnote n="9">⁹If you have read my previous footnote on dwarfing of goldfishes, we now have an aquarium.</footnote>
<figure><img src="image_40.png" /><figcaption>Figure 29.5: Multiplicative proof-structures.</figcaption></figure>
than decorative labels which can be forgotten. In this syntax, proof-structures are defined with directed hypergraphs constructed with the hyperedges of Figure 29.5a. These hyperedges are the elementary bricks of proofs. Definitions of hypergraphs are formally given in Appendix C.

**§29.5 Definition (Proof-structure).** A proof-structure is defined by $\mathcal{S} = (V, E, \text{in}, \text{out}, \ell_E)$ where $(V, E, \text{in}, \text{out})$ is an ordered directed hypergraph (cf. Appendix C) and $\ell_E : E \to \{\otimes, \mathcal{N}, \text{ax}, \text{cut}\}$ is a labelling map on hyperedges. A proof-structure is subject to these additional constraints:

* hyperedges satisfy the arities and labelling constraints shown in Figure 29.5a;

* each vertex must be the target of exactly one hyperedge, and the source of at most one hyperedge;

* cut hyperedges must connect either:

- the conclusion of a $\mathcal{N}$ hyperedge with the conclusion of a $\otimes$ hyperedge, or

- two atoms.

**§29.6 Notation (Axioms and cuts).** Let $\mathcal{S}$ be a proof-structure. We define its set of axioms hyperedges: $\mathbf{Ax}(\mathcal{S}) := \{e \mid e \in E, \ell_E(e) = \text{ax}\}$, and its set of cut hyperedges: $\mathbf{Cuts}(\mathcal{S}) := \{e \mid e \in E, \ell_E(e) = \text{cut}\}$.

**§29.7 Convention (Left and right sources).** For practical purposes, the sources of hyperedges are ordered, and “left” and “right” sources are considered since there are never more than two; illustrations in Figure 29.5a implicitly represent the left (resp. right) source on the left (resp. right).

For a proof-structure $\mathcal{S}$ and a hyperedge $e$ of $\mathcal{S}$:

* if $\ell_E(e) = \text{ax}$ and $\text{out}(e) = (u, v)$, we define $\overleftarrow{e} := u$ and $\overrightarrow{e} := v$ for the left and right conclusion of $e$;

* if $\ell_E(e) \in \{\text{cut}, \otimes, \mathcal{N}\}$ and $\text{in}(e) = (u, v)$, we define $\overleftarrow{e} := u$ and $\overrightarrow{e} := v$ for the left and right premise of $e$.

**§29.8 Notation (Conclusions and atoms).** The conclusions of $\mathcal{S}$ are defined by the set $\text{Concl}(\mathcal{S}) = \{v \in V \mid \text{there is no } e \in E \text{ such that } v \in \text{in}(e)\}$. Similarly, the atoms of $\mathcal{S}$ are defined by the set $\text{Atoms}(\mathcal{S}) = \{v \in V \mid \exists e \in \mathbf{Ax}(\mathcal{S}) \text{ such that } v \in \text{out}(e)\}$. They are conclusions of axiom hyperedges.

**§29.9** The cut-elimination procedure (corresponding to program execution) is defined with two graph-rewriting rules in Figure 29.5b. Cut-elimination is made even more natural in proof-structures; the case ax/cut is a graph contraction identifying two atomic formulas and the case $\otimes/\mathcal{N}$ makes explicit the idea of rewiring. An example of proof-structure and its full cut-elimination is illustrated in Figure 29.6 and a formal definition of cut-elimination is given below.
<figure><img src="image_41.png" /><figcaption>Figure 29.6: Cut-elimination for a proof-structure.</figcaption></figure>

<figure><img src="image_42.png" /><figcaption>Figure 29.7: The MIX rule of MLL+MIX sequent calculus and an example of a sequent calculus proof of $A \otimes B \dashrightarrow A \not\Vdash B$ which is not provable in MLL.</figcaption></figure>

§29.10 **Definition (MLL cut-elimination)**. Let $S := (V, E, in, out, \ell_E)$ be an MLL proof-structure with a cut $e_{cut} \in E$ such that $in(e_{cut}) = (v_1, v_2)$ with both $v_1$ and $v_2$ being conclusions of some hyperedges $e_1$ and $e_2$.

◇ **Left axiom** If $\ell_E(e_1) = \text{ax}$ for $i \in \{1, 2\}$ and $\text{out}(e_1) = (v_0, v_1)$, then the elimination of $e_{cut}$ is a new proof-structure $S' := (V', E', in', out', \ell_E)$ such that $V' := V - \{v_1, v_2\}$, $E' := E - \{e_{cut}, e_1\}$ and finally, $\text{out}'(e') = v_0$ for any $e'$ such that $\text{out}(e') = v_2$ and $\text{out}'(x) = \text{out}(x)$ otherwise for any other $x \in E$.

◇ **Right axiom** We have a similar case for $\ell_E(e_2) = \text{ax}$ which correspond to the previous case in which we exchange $e_1$ (and $v_1$) for $e_2$ (and $v_2$).

◇ **Multiplicative** Assume we have $\ell_E(e_1) = \mathcal{N}$ and $\ell_E(e_2) = \otimes$ (or the converse) with $in(e_1) = (u_1, u_2)$ and $in(e_2) = (w_1, w_2)$. The elimination of $e_{cut}$ is a new proof-structure $S' := (V', E', in', out, \ell_E)$ with $V' := V - \{v_1, v_2\}$, $E' := (E - \{e_{cut}, e_1, e_2\}) \cup \{e_{cut}^1, e_{cut}^2\}$ and finally, $in'(e_{cut}^i) = (v_i, w_i)$ for $i \in \{1, 2\}$ and $in'(x) = in(x)$ otherwise for any other $x \in E$.

§29.11 There exists a remarkable extension of MLL with a rule called MIX (cf. Figure 29.7), initially studied by Fleury and Rétoré [FR94]. This rule corresponds to the axiom scheme $A \otimes B \dashrightarrow A \not\Vdash B$ and constitutes, together with the other rules of MLL, a new proof system called MLL+MIX. Beside this new rule, MLL+MIX works with the same
formulas as MLL. In particular, all MLL sequent calculus proofs are MLL+MIX sequent calculus proofs as well.

§29.12 We now would like to define the underlying proof-structure of an MLL+MIX sequent calculus proof, exactly as informally done in Figure 29.3. In order to do so, we define a labelling of the vertices of proof-structures (for which labels correspond to formulas) in order to make proof-structures look like actual proofs. By doing so, we already implicitly give a little bit of meaning to the purely computational proof-structures.

§29.13 **Definition (Labelled proof-structure).** A labelled proof-structure is a tuple

$$S = (V, E, \text{in}, \text{out}, \ell_V, \ell_E)$$

where $(V, E, \text{in}, \text{out}, \ell_E)$ is a proof-structure and $\ell_V : V \to \mathcal{F}_{\text{MLL}}$ is a function labelling vertices of $V$ by formulas.

We write $\vdash_S \Gamma$ with a set of formulae $\Gamma := \{\ell_V(v) \mid v \in \text{Concl}(S)\}$ in order to specify the formulas associated with the conclusions of $S$.

§29.14 In Figure 29.8, we define a translation $[\cdot]$ from MLL+MIX sequent calculus derivations to labelled proof-structures. Notice that this translation is not surjective, and that some proof-structures do not represent sequent calculus proofs. This is tackled by the *correctness criterion*, which characterises those proof-structures that do translate sequent calculus proofs through structural properties and which are considered “correct”. but for the time being, we give a preliminary definition of proof-net, the proof-structures coming from sequent calculus proofs. The relationship between proof-structures, proof-nets and sequent calculus proofs is illustrated in Figure 29.9.

§29.15 The MIX rule corresponds to allowing disjoint union of proof-structures as being “correct”. Although not “logical” (i.e. not coming from MLL sequent calculus which decomposes intuitionistic and classical logic), MLL+MIX proofs keep interesting computational properties which naturally appear in various models of linear logic such as coherence spaces [Gir87a, Chapter 4].

§29.16 **Definition (MLL and MLL+MIX proof-nets).** An MLL (*resp.* MLL+MIX) *proof-net* is a proof-structure $S$ for which there exists an MLL (*resp.* MLL+MIX) sequent calculus proof $\pi$ such that $S = [\pi]$.

§29.17 Once we get out of the multiplicative paradise, things are less simple. Even today, the theory of proof-nets suffer from a lot of various problems when trying to extend to other fragments of linear logic. In the next sections, I mention other fragments of linear logic with some being less detailed than others. Units and additives are rather considered problematic but exponential proof-nets are fine although not perfect. When designing extensions of proof-nets we have to think about the following points:
<figure><img src="image_43.png" /><figcaption>Figure 29.8: Translation of MLL+MIX sequent calculus proofs into labelled proof-structures.</figcaption></figure>

<figure><img src="image_44.png" /><figcaption>Figure 29.9: Proof-structures are general structures in which proof-nets can be defined as special cases coming from the translation of sequent calculus proofs. Correctness criteria are ways to tell if a proof-structure is correct, i.e. corresponds to a proof-net independently of sequent calculus proofs.</figcaption></figure>
◇ **Loss of canonicity** proof-nets are meant to capture the essence of proofs. In particular, it has to enjoy a good canonicity by providing a synthetic syntax for proofs. This is usually handled by considering "commutation rules" transforming sequent calculus proofs into equivalent proofs up to exchange of rules [HH16, Section 1]. Other equivalences of proofs can be considered as well but translation into proof-structures have to be invariant under these equivalences;

◇ **Simulation of cut-elimination** proof-structures must be able to faithfully simulate cut-elimination as it is done in the sequent calculus. This is not always the case because sequent calculus is often subject to some implicit operations which leave some unwanted parts or residuals in the cut-elimination of proof-structures (for instance the cut-elimination $\vdash/\vdash_k$ hides an erasure of either $\vdash \Gamma, A_1$ or $\vdash \Gamma, A_2$);

◇ **Effective correctness criterion** we must be able to computationally check if a proof-structure is correct, i.e. it is the translation of a sequent calculus proof. This means that we are able to characterise a fragment of linear logic.

◇ **Ad-hoc extensions** With all the previous points, it can happen that some ad-hoc technical and unnatural changes are made to proof-nets. Proof-nets should be able to provide an analysis of sequent calculus proofs for linear logic and if possible, of mathematical logic in general. The design of proof-nets should not get lost in laborious technicalities for the sole sake of making things work<sup>10</sup> (although it can indeed be theoretically interesting to develop further extensions).

## Multiplicative unit proof-nets

§29.18 The links and cut-elimination of multiplicative proof-structures are presented in Figure 29.10. The extension of the translation of sequent calculus proofs to proof-structures is straightforward. The proof of $\vdash 1$ becomes the link for $1$ and the proof of $\vdash \Gamma, \bot$ becomes the link for $\bot$ coming attached to a proof-net corresponding to $\Gamma$. If this $\bot$ interacts with a link $1$, then only the context $\Gamma$ associated with $\bot$ is left.

§29.19 **Forgotten dependency.** Notice that there is no way to tell what context $\Gamma$ a $\bot$ link is attached with, although $\bot$ constants are always in the same sequent as a context $\Gamma$ in sequent calculus. At this point it is not a problem since we only consider cut-elimination but correctness will be problematic as we will see later.
<figure><img src="image_45.png" /><figcaption>Figure 29.10: Multiplicative unit proof-structures.</figcaption></figure>

**Additive proof-nets**

§29.20 There are several different designs of additive proof-nets. The particularity of additive proof-nets is that the formula $A \& B$ has to share a same context $\Gamma$ for its to premises $A$ and $B$ (cf. Figure 27.2b). As for the cut-elimination (cf. Figure 29.11b), a branch of the & rule is selected but other one is erased. Problems regarding the different presentation of MALL proof-nets are presented in one of Marc Bagnol's notes<fnref n="11" />.

§29.21 **Additive boxes.** The solution of additive boxes [Gir96, Section 1.1] (I personally like Gimenez's PhD thesis for an accessible explanation of additive boxes [Gim09, Chapter 4]) is presented in Figure 29.11. The connective & is handled with a box having two disjoint parts. Each premise is wired in its own side. In the rule of &, a context $\Gamma$ is duplicated in two premise sequents $\vdash \Gamma$, $A$ and $\vdash \Gamma, B$, in the case of proof-structures a proof-structure corresponding to $\Gamma$ is duplicated and located in each side of the corresponding & box. Its conclusions can go outside the box to interact with other proof-structures. When a & box interacts with a selector $\oplus_k$, it opens one corresponding side of the box (left for $\oplus_1$ and right for $\oplus_2$) and destructs the other.

§29.22 **A return to sequentiality.** Additive boxes work quite well. If we are not too demanding, we can be satisfied and even use them as such as in Gimenez's PhD thesis [Gim09]. There are also reasons to not be satisfied:

<footnote n="10">¹⁰When people learn computer programming for the first time, they tend to think that a working program is sufficient. However, a program's life is not set in stone. People will read the code, want to change it for various reasons, or use it as a tool for another purpose. Therefore, programs should not only be working but also workable.</footnote>

<footnote n="11">¹¹https://www.normalesup.org/~bagnol/notes/additifs.pdf</footnote>
<figure><img src="image_46.png" /><figcaption>Figure 29.11: Additive proof-structures with additive boxes.</figcaption></figure>

<figure><img src="image_47.png" /><figcaption>Figure 29.12: Example of commutation rule for &. It states the equivalence of two proofs up to permutation of rules.</figcaption></figure>
* the context $\Gamma$ is duplicated although it could be truly *shared* (and thus exist in uniquely one copy) and

* a *global* erasure occurs during cut-elimination (hence a rather *external* mechanism), as if there was an implicit human intervention. But do we need it to speak about logic? Cannot it be made explicit?;

* Similarly, the two contexts $S_\Gamma$ in the left and right part have to be the *same*. This is a quite strong requirement for alogical objects. Maybe proof-structures are not so alogical after all;

* using boxes is a return to sequentiality. A part of a proof-structure is frozen and handled as a whole with some implicit and global operations. Actually, sequent calculus can be seen as having proof-nets where all links are boxes [Gir96, Section 1.1]. By using boxes (and thus introducing sequentiality), we can lose canonicity if we translate proofs such as the ones in Figure 29.12. With additive boxes, we would have one additive box duplicated inside the other and two different proof-nets. This can however be handled by adding more external congruence rules.

These are not necessarily problems but it is fair to not be satisfied and ask for better. If we have sequent calculus in mind, it may be fine but if we have bigger ambitions for a foundational theory of logic, it is difficult to be satisfied.

**§29.23 Boolean weights.** If we wish to get rid of boxes, another early solution is to use weights [Gir96, Section 1.4] where links are attached to a variable in a boolean algebra. It is then possible to identify the left and right premise/context of a $\&$ link and to act on it. This idea has been developed and modified by several authors such as Girard himself with monomial weights [Gir96, Section 1.4] or Laurent and Maieli [LM08].

**§29.24 Additive slices.** Another solution is to use *additive slices* [Gir96, Section A.1.6] by considering a proof of $\vdash \Gamma, A\&B$ as a sum of two independent proofs of $\vdash \Gamma, A$ and $\vdash \Gamma, B$. A MALL proof-net is then a sum of all its slices, as if we made explicit all the “additive universes” for each choice with $\&$ (think of representing a non-deterministic Turing machine as a sum of deterministic machines for all possible choices). The problem is that we obtain very big proofs: if the proof-structure is cut-free then it can have $2^n$ slices for $n$ the number of $\&$ connective. This idea has been developed by Hugues and Van Glabbeek [HVG03]. Another more recent solution is Heijltjes and Hugues’ conflict nets [HH16] which is able to obtain a local canonicity (invariance under “local” commutation rules).

Exponential proof-nets

**§29.25 Exponential boxes.** The most natural translation of MELL proofs uses exponential boxes [Gue04, Section 3] presented in Figure 29.13. The use of boxes is rather faithful because in the sequent calculus, the promotion rule ! could already be seen as a box
<figure><img src="image_48.png" /><figcaption>Figure 29.13: Exponential proof-structures with exponential boxes.</figcaption></figure>
<figure><img src="image_49.png" /><figcaption>Figure 29.14: Generalised links for structural rules.</figcaption></figure>

on which some operations could be done. The context $?\Gamma$ of the promotion rule is represented by links going out of a box without passing by the $!$ link. The conclusion of such links are called *auxiliary conclusions* passing through *auxiliary doors* of a box. The cut-elimination reductions of Figure 29.13b correspond to the erasure, opening, duplication and insertion of a box (in case a box interacts with an auxiliary conclusion of another box). For the $!/w$ cut-elimination, what remains is a weakening link for each conclusions appearing in the proof-structure $S_{?\Gamma}$, exactly as in the corresponding sequent calculus cut-elimination.

§29.26 **Generalised structural rules.** A problem with this formulation of structural rules is that it is possible to construct arbitrary binary trees by using contractions. By using two contraction links, it is possible to construct two different trees having the same behaviour. This is a loss of canonicity. A solution is to use reduction rules to merge structural rules as in Di Cosmo and Kesner's works [DCK97, Section 4], to define congruences rules on proof-structures or to use Danos and Regnier's generalised structural rules [Gue04, Section 4.3]. Danos and Regnier's links come from the fact that structural rules can be seen as the instance of a same rule (cf. Figure 29.14) similarly to the multiplexing rule of Paragraph 27.21. If only have one $n$-ary $?$ link which is always merging with the others connected to it and pushed out of boxes. This recover the canonicity lost by the original structural rules.

§29.27 **Lambda-calculus.** Since MELL is where the typed $\lambda$-calculus can be expressed, it is natural that we can also obtain a translation of typed $\lambda$-terms into proof-nets [Dan90, Reg92, Gue04]. More surprisingly, it is also possible to define untyped $\lambda$-calculus directly with proof-structures (and not proof-nets) since they are alogical (actually not exactly) [Dan90, Section 11]. This simulation is based on the translation of intuitionistic logic into linear logic. Regarding encodings of classical logic, it is possible to find encoding of $\lambda\mu$-calculus in proof-nets in Olivier Laurent's works [Lau03, Lau99]. Proof-nets are also able to provide a canonical presentation of $\lambda$-terms. Regnier shows that a subtle equivalence on terms known as $\sigma$-equivalence can be simulated by the elimination of some multiplicative cuts [Reg94]. This is also presented in English in Olivier Laurent's works [Lau03, Definition 11]. It is also possible to encode more sophisticated functional languages such as PCF [Gim09, Section 5.4].
§29.28 **Explicit substitutions.** In the context of λ-calculus, exponential boxes actually enjoy a computational interpretation by themselves: they correspond to *explicit substitutions* [ACCL91, Ros96]. In λ-calculus, the β-reduction is defined by $(\lambda x.M)N \leadsto \{x := N\}M$ which is an external operation. However, it can make sense to have explicit substitutions set in the syntax of terms. Such substitutions can be moved, erased, opened, duplicated freely. This exactly corresponds to exponential boxes which allow to manipulate a frozen section of a proof/program. Works in that direction have been led by Delia Kesner and Beniamino Accattoli [Acc18, DCKP03, DCK97].

§29.29 **Box-free approaches and optimal reduction.** In λ-calculus, when we have a redex $(\lambda x.M)N$, it happens that $N$ is duplicated several times (the same thing occurs with exponential boxes). However, this duplication is useless: it is sufficient for the part of $M$ requiring $N$ to access to a unique copy of $N$, which correspond to a *sharing* of $N$. Lévy formalised this notion in his PhD thesis [Lév78] and defined a notion of *optimal reduction* for λ-calculus. This is only more than ten years later that Lamping came up with an algorithm for optimal reduction [Lam89] which accidentally corresponded to a box-free approach to proof-nets which features sharing [GAL92b]. Even more surprising, this approach is actually related [GAL92a] to Girard's geometry of interaction [Gir89a] which develops the ideas of linear logic (it is presented in the next chapter). The story and techniques of optimal reduction are told in Guerrini's survey [Gue04, Chapter 5].

## 30 Correctness criteria

§30.1 Proof-structures are almost free of logical meaning. We have two hyperedges $\otimes$ and $\nparallel$ but it is only a matter of labels. Nothing truly differentiates them although they correspond to different logical operations in sequent calculus and have to be distinguished. For that reasons, correctness criteria have been developed. They are method asserting whether a proof-structure corresponds to a proof-net. There exists a lot of various correctness criteria for a lot of fragments of linear logic, the most simple and standard being the Danos-Regnier correctness criterion. More information about other correctness criteria can be found in Marc Bagnol, Amina Doumane and Alexis Saurin's "On the dependencies of logical rules" [BDS15] and in Lutz Straßburger "Proof Nets and the Identity of Proofs" [Str06, Section 2.5]. In this chapter, I first introduce Girard's long trips criterion then Danos-Regnier correctness.

§30.2 A proof-structure is logically correct when it is possible to define a labelling such that it corresponds to a proof-net (which is itself the translation of a sequent calculus proof). In particular, a proof-structure can correspond to several proof-nets depending on the labelling we choose.

§30.3 **Definition (MLL-certification and MLL+MIX-certification).** A proof-structure $S = (V, E, \text{in}, \text{out}, \ell_E)$ is *MLL-certifiable* (resp. *MLL+MIX-certifiable*) with $\vdash A_1, ..., A_n$
<figure><img src="image_50.png" /><figcaption>Figure 30.1: Ports and information flow of a binary connective.</figcaption></figure>

<figure><img src="image_51.png" /><figcaption>Figure 30.2: Flow of information inside an axiom, a cut and a conclusion.</figcaption></figure>

when there exists a vertex-labelling function $\ell_V$ such that (V, E, in, out, $\ell_V$, $\ell_E$) is an MLL (*resp.* MLL+MIX) proof-net.

When there exists $\vdash A_1, ..., A_n$ such that $S$ is MLL(+MIX)-certifiable with $\vdash A_1, ..., A_n$ then we simply say that $S$ is MLL(+MIX)-certifiable.

**Girard's long trip criterion**

**§30.4 Sequentialisation.** The original and first criterion is Girard's long trip criterion [Gir87a, Section 2.2] for multiplicative proof-structures. The goal is to recover sequentiality back from a proof-structure and produce a sequent calculus proof. This process is known as *sequentialisation theorem*. Girard imagined a sequential, continuous and circular path exploring all formulas of a proof-structures. Those correct paths are called *long trips* and the incorrect ones are called *short trips*. All connectives can be seen as boxes with input and output ports. It is then possible to travel from the bottom to the top or the converse (cf. Figure 30.1). If we have a long trip, it would be possible to extract a sequential application of rules and the path corresponds to the *contour* of the sequent calculus proof. In order to define how to traverse a proof-structure, we have to take into account that $\mathcal{N}$ and $\otimes$ have different behaviour and should not be traversed in the same way.

**§30.5 Case of axioms, cuts and conclusions.** The most basic cases of traversal are presented in Figure 30.2. They are very natural and there is nothing special about it.

**§30.6 Case of tensor.** The translation of sequent calculus proofs into proof-structures in Figure 29.8 shows that a correct tensor connects two disjoint proof-nets. It follows that when exploring from a tensor conclusion $A \otimes B$, we have to fully explore one premise, going back then exploring the other and returning to $A \otimes B$. Figure 30.3a shows that there is only two ways to that. These two choices of paths are called *switchings*. We have
<figure><img src="image_52.png" /></figure>

<figure><img src="image_53.png" /><figcaption>Figure 30.3: Flow of information in binary connectives.</figcaption></figure>

<figure><img src="image_54.png" /><figcaption>Figure 30.4: Example of situation where $\otimes_L$ succeeds but $\otimes_R$ fails. Based on a proof-structure construction from $\vdash (A \otimes B) \otimes (A^\perp \otimes B^\perp)$. The exact construction with other boxes is left implicit and we only look at how ports are related.</figcaption></figure>
<figure><img src="image_55.png" /><figcaption>Figure 30.5: Reunion of formulas in an axiom. We obtain two short trips.</figcaption></figure>

two switchings: $\otimes_L$ exploring the left premise first and $\otimes_R$ exploring the right premise first. Because the tensor splits in two disjoint components, switchings have to *reunite* the two branches in order to hope for a full connected traversal (long trip). An example is given in Figure 30.4 where for a same situation, $\otimes_L$ forms a long trip (success) but $\otimes_R$ forms three short trips (failure). This example can be obtained by constructing a proof-structure from the syntax tree of the sequent $\vdash (A \otimes B) \otimes (A^{\perp} \otimes B^{\perp})$.

**§30.7 Case of par.** For the $\mathcal{N}$ rule, this is the opposite situation. In Figure 29.8, we see that a $\mathcal{N}$ link connects two formulas in a *same* connected component. Switchings must then *splits* the two premises to avoid short trips. We obtain the two ways of traverse the proof-structure in Figure 30.3b. Without splitting, we would reunite two already connected formula and form a short trip, as shown in the reunion of conclusion of axiom in Figure 30.5. From the sequent $\vdash (A \mathcal{N} B) \otimes (B^{\perp} \mathcal{N} A^{\perp})$, it is possible to construct a situation where there is a long trip for a switching and not for another. This is illustrated in Figure 30.6.

**§30.8 Definition (Girard switching).** Let $\otimes(S)$ and $\mathcal{N}(S)$ respectively be the set of all $\otimes$ and $\mathcal{N}$ hyperedges in a proof-structure $S$. A (Girard) *switching* is a total function $\varphi$ defined as the union of two functions:

* $\varphi_{\otimes} : \otimes(S) \rightarrow \{\otimes_L, \otimes_R\}$;

* $\varphi_{\mathcal{N}} : \mathcal{N}(S) \rightarrow \{\mathcal{N}_L, \mathcal{N}_R\}$.

A switching of a proof-structure is hence a selection of a choice of traversal for any $\otimes$ and $\mathcal{N}$ hyperedges.

**§30.9 Definition (Switching flow graph).** Let $S$ be a proof-structure and $\varphi$ be a Girard switching. The *switching flow graph* $S\varphi$ associated with $\varphi$ is a directed multigraph $(V, E, \text{in}, \text{out})$ where $V := V^S$ and $E$ follows the rules of flow of information given in
<figure><img src="image_56.png" /><figcaption>Figure 30.6: Situation where a switching fails and the other succeed. Based on a proof-structure construction from $\vdash (A \not\to B) \otimes (B^{\perp} \not\to A^{\perp})$. A tensor is hidden below so you can just imagine that some construction is linking the two $\not\to$ conclusions.</figcaption></figure>
Figure 30.2, Figure 30.3b and Figure 30.3a. We use the notation $u \stackrel{e}{\mapsto} v$ of Appendix C for directed edges.

◇ **Axiom** if we have $e \in \mathbf{Ax}(S)$ such that $\mathbf{out}(e) = (u, v)$, then there are two edges $u \stackrel{e_1}{\mapsto} v$ and $v \stackrel{e_2}{\mapsto} u$;

◇ **Cut** it is similar for cuts;

◇ **Conclusion** for any conclusion $v$, we have a loop $v \stackrel{e}{\mapsto} v$;

◇ **Tensor** if we have $\ell_E(e) = \otimes$ with $\mathbf{out}(e) = v$ and $\mathbf{in}(e) = (v_l, v_r)$, there are two cases:

• if $\varphi(e) = \otimes_L$, then we have edges $v \stackrel{e_1}{\mapsto} v_l, v_l \stackrel{e_2}{\mapsto} v_r$ and $v_r \stackrel{e_3}{\mapsto} v$;

• if $\varphi(e) = \otimes_R$, then we have edges $v \stackrel{e_1}{\mapsto} v_r, v_r \stackrel{e_2}{\mapsto} v_l$ and $v_l \stackrel{e_3}{\mapsto} v$;

◇ **Par** there are two cases for each $v$ conclusion of an $\mathcal{N}$ hyperedge $e$ with left premise $v_l$ and right premise $v_r$:

• if $\varphi(e) = \mathcal{N}_L$, then we have edges $v \stackrel{e_1}{\mapsto} v_l, v_l \stackrel{e_2}{\mapsto} v$ and $v_r \stackrel{e_3}{\mapsto} v_r$;

• if $\varphi(e) = \mathcal{N}_R$, then we have edges $v \stackrel{e_1}{\mapsto} v_r, v_r \stackrel{e_2}{\mapsto} v$ and $v_l \stackrel{e_3}{\mapsto} v_l$.

**§30.10 Definition (Trips).** A *trip* in a switching flow graph $S^\varphi$ is a directed path in $S^\varphi$. It is a *long trip* if it is an Eulerian circuit (a path traversing all edges exactly once and returning to its starting point). Otherwise, it is a *short trip*.

**§30.11 Theorem (Girard correctness).** A proof-structure $S$ is MLL-certifiable if and only if $S$ has no short trip for any switching of $S$.

*Proof.* A proof based on combinatorial arguments can be found in Girard's papers [Gir87a, Section 2.1] [Gir11a, Section 11.3.3]. □

**§30.12 Question, answer and communication.** An intuition given by Girard about these trips [Gir11a, Section III.4.1] is that they correspond to the flow of questions and answers. Consider a function application $\lambda x.M : A \to B$ with an argument $N : A$, yielding the $\beta$-reduction $(\lambda x.M)N \leadsto_{\beta} \{x := N\}M$. The occurrences $x_i : A$ of $x$ can be seen as questions asking for values of type $A$. The occurrences $N_i : A$ of $N$ are then seen as answers. This interaction between inputs and outputs, or questions and answers can be understood through a notion of *communication*. Imagine a sequential communication exploring a proof-structure. We explore $M$ and end on the question $x_1$. We go out and look for the answer $N_1$, then go back in $M$ to find the next question and so on. The same idea appears for long trips criterion: there is a communication between axioms and the rest of the proof-structure (on which a switching has been applied). This dual communication between axioms and the rest of the switching flow graph will be made explicit in the next chapter about the geometry of interaction.
<figure><img src="image_57.png" /><figcaption>Figure 30.7: Undirected current flowing inside a proof-structure.</figcaption></figure>

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

(a) Correctness hypergraph corresponding to an axiom connected to a tensor (cf. Figure 30.5). We have a cycle.

(b) Correctness hypergraph corresponding to the failure of Figure 30.6 where two short trips appear. We have two connected components. If we had $\mathcal{Y}_L$ on the right, then it would succeed.

<caption>Figure 30.8: Two failing correctness hypergraphs.</caption>

## Danos-Regnier criterion for MLL+MIX

§30.13 The Danos-Regnier correctness criterion is a simplification of Girard's long trips criterion. Consider the long trip criterion. Instead of looking at paths of a flow of information inside a proof-structures, we simply look at the structure of the flow of information. Forget the directions of the current and see the boxes with ports as simple nodes. We obtain the undirected flow graph of Figure 30.7.

* The two switchings for $\otimes$ correspond to two three-way channels of communication. Since they have the same structure, they are identified and there is no need for a switching of $\otimes$ any more.

<figure><img src="image_59.png" /><figcaption>Figure 30.9: A proof-structure, all its switching hypergraphs and a possible labelling corresponding to a proof-net.</figcaption></figure>
• The two switchings for $\mathcal{N}$ correspond to disconnecting one premise for each $\mathcal{N}$ link.

If long trips are about directed graphs then Danos-Regnier correctness is about hyper-graphs induced by trips. It follows that it is sufficient to consider a disconnexion of one premise for each $\mathcal{N}$ link directly on a proof-structure and construct a *correctness hypergraph*. In particular, it is possible to show that all correctness hypergraphs for a proof-structure $S$ is connected and acyclic (a tree) if and only if $S$ has no short trip for any switching. In particular, all short trips induce either more than one connected component or a cycle. To illustrate this fact, two correctness hypergraphs corresponding to failure of finding a long trip are illustrated in Figure 30.8. An example of correct proof-structure is presented in Figure 30.9 together with its two only correctness hypergraphs and a possible corresponding proof-net.

**§30.14** Since the Danos-Regnier correctness criterion is very standard in linear logic, we provide more formal definitions which will be used later in this thesis. We define the *correctness hypergraphs* associated with a proof-structure $S$ as undirected copies of $S$ with one source of each $\mathcal{N}$-labelled hyperedge removed. The Danos-Regnier criterion states that a proof-structure is an MLL proof-net if and only if all its correctness hypergraphs are all connected and acyclic. Since the idea of logical correctness is purely structural as well, our definitions still deal with unlabelled proof-structures.

**§30.15** **Notation.** Given a proof-structure $S = (V, E, \text{in}, \text{out}, \ell_E)$, we write $\mathcal{N}(S)$ the subset $P \subseteq E$ of $\mathcal{N}$-labelled edges, i.e. $\mathcal{N}(S) = \{e \in E \mid \ell_E(e) = \mathcal{N}\}$.

**§30.16** **Definition (Correctness hypergraph).** Let

$$S = (V, E, \text{in}, \text{out}, \ell_E)$$

be a proof-structure. A (Danos-Regnier) *switching* is a map $\varphi : \mathcal{N}(S) \to \{\mathcal{N}_L, \mathcal{N}_R\}$. Its associated *correctness hypergraph* is the undirected hypergraph with labelled hyperedges $S^\varphi = (V, E', \text{end}, \ell_{E'})$ induced by the switching $\varphi$ which is defined with:

• $\text{end}(e) = \{u\}$ where $u = \overleftarrow{e}$ when $e \in \mathcal{N}(S)$ and $\varphi(e) = \mathcal{N}_L$;

• $\text{end}(e) = \{u\}$ where $u = \overrightarrow{e}$ when $e \in \mathcal{N}(S)$ and $\varphi(e) = \mathcal{N}_R$;

• $\text{end}(e) = \text{in}(e) \cup \text{out}(e)$ in all other cases.

The labelling $\ell_{E'}$ is defined by $\ell_{E'}(e) = \varphi(e)$ when $e \in \mathcal{N}(S)$ and $\ell_{E'}(e) = \ell_E(e)$ otherwise.

**§30.17** **Theorem (Danos-Regnier correctness).** A proof-structure $S$ is MLL-certifiable if and only if it is MLL+MIX-certifiable and $S^\varphi$ is connected for all switching $\varphi$.

*Proof.* Proven in Danos and Regnier’s “The structure of multiplicatives” [DR89, Theorem 4]. □
<table><caption>Figure 30.10: Switching for $\mathcal{N}_L$ seen from the point of view of natural deduction. The premise $A^{\perp}$ and $B^{\perp}$ become conclusions A and B in monolateral sequent calculus and proof-nets.</caption><thead><tr><th></th><th>Left switching</th><th>Right switching</th></tr></thead><tbody><tr><th>Natural deduction</th><td>A<sup>⊥</sup><br>⋮<br>B<br>A<sup>⊥</sup> -o B</td><td>B<sup>⊥</sup><br>⋮<br>A<br>B<sup>⊥</sup> -o A</td></tr><tr><th>Proof-structures</th><td>A ⋮ B<br> /<br> ⊢<sub>R</sub><br>|<br>A ⊢ B</td><td>A ⋮ B<br> /<br> ⊢<sub>L</sub><br>|<br>A ⊢ B</td></tr></tbody></table>

§30.18 Once we defined Danos-Regnier correctness criterion for MLL, the correctness criterion for MLL+MIX is not so far from that. Since MLL+MIX proof-nets allow disjoint union of MLL-certifiable proof-nets, it is sufficient to only consider acyclicity of correctness hypergraphs.

§30.19 **Theorem (MLL+MIX correctness).** A proof-structure $S$ is MLL+MIX-certifiable if and only if $S^{\varphi}$ is acyclic for all switching $\varphi$.

*Proof.* Proven in Fleury and Retoré's seminal paper [FR94, Theorem 4.7 and 4.8]. □

§30.20 Danos-Regnier can be puzzling when we are introduced to correctness criterion without intuitive explanations. Why do we need to disconnect either the left or right premise for each $\mathcal{N}$ link? This is mainly because of combinatorial considerations about sequent calculus rules as explained previously. However, in the “Blind Spot” [Gir11a, Section 11.3.2], Girard suggests an intuitive explanation to this switching: we would like to extract/distinguish a tree-shaped structure from the proof-structure and obtain a well-defined natural deduction proof for linear logic (as cumbersome it would be). The formula $A\mathcal{N}B$ is equivalent to both $A^{\perp} \to B$ and $B^{\perp} \to A$ (thanks to the commutativity of $\mathcal{N}$). The switching then corresponds to a choice of natural deduction writing.

* If $A \mathcal{N} B$ is written $A^{\perp} \to B$ then we have a premise reaching the conclusion $B$ from the top in order to construct $A^{\perp} \to B$. However, as we saw, premise $A$ are
<figure><img src="image_60.png" /><figcaption>Figure 30.11: Example of MLL<sub>u</sub> proof with a ⊥ constant.</figcaption></figure>

<figure><img src="image_61.png" /><figcaption>Figure 30.12: Jumps in MLL<sub>u</sub> for ⊥. In the two case, we have connected and acyclic graphs.</figcaption></figure>

negated conclusions $A^{\perp}$ and negated premises $A^{\perp}$ must be positive conclusions $A$.
Hence it means that a (virtual) conclusion $A$ is linked to $B$ to construct $A^{\perp} \dashrightarrow B$.
This is what happens with the switching $\mathcal{N}_R$.

* The other case of $B^{\perp} \dashrightarrow A$ is similar.

To make it clearer, the two situations are illustrated in Figure 30.10. The structure is correct when we have a tree in the two cases (since natural deduction proofs are trees).

§30.21 In the next sections, extensions of the multiplicative criterion to other fragments of linear logic are explained. Once again, we are leaving the multiplicative paradise. All extensions below are based on Danos-Regnier correctness since it is standard and simpler than Girard's long trips.

Criteria for multiplicative units

§30.22 Multiplicative units introduce two links $1$ and $⊥$ (cf. Figure 29.10). The unary link $1$ corresponds to an axiom (because its rule terminates a proof) and it causes no problem for correctness. The constant $1$ is typically introduced alone in its own branch, with a tensor for instance. Since there is no switching for $⊗$, the correctness of a proof-structure with $1$ will depend on the correctness of the rest of the proof-structure, without $1$.

§30.23 As for $⊥$, it is where things get problematic. A constant $⊥$ comes together with a context $Γ$ to which it can be attached or independent. Examples are given in Figure 30.11. Such proofs could be equivalently use $\mathcal{N}$ rules ($\vdash⊥, A^{\perp}, A$ is equivalent to $\vdash⊥, \mathcal{N}A^{\perp}, \mathcal{N}A$). If $⊥$ is disconnected or if we consider a switching $\mathcal{N}_L$ or $\mathcal{N}_R$ disconnecting it, then we lose connectedness which was essential for multiplicative correctness. But a $⊥$ in a correct proof is always related to a correct context $Γ$ and we would like to recover this. A
<figure><img src="image_62.png" /><figcaption>Figure 30.13: Cut-elimination with jumps does not preserve Danos-Regnier correctness. The initial proof-structure is correct but not its cut-elimination.</figcaption></figure>

<figure><img src="image_63.png" /><figcaption>Figure 30.14: Transformation from boxes to generalised axioms.</figcaption></figure>

solution is to use jumps [Gir96, Appendix A.2] which are artificial links relating each $⊥$ to a correct context. A correct context must always contain at least one constant 1 or an axiom. It is then sufficient to link occurrences of $⊥$ to any 1 or axiom. Two examples of jumps are given in Figure 30.13. A MLL$_u$ proof with jumps is correct when it is connected and acyclic (the Danos-Regnier correctness criterion is preserved).

§30.24 A problem with jumps is whether they are part of proof-structures themselves or something added when verifying correctness. In the first case, cut-elimination can erase the target of jumps as in Figure 30.13. We have to recreate a jump for the $⊥$ links. This is rather complicated and unnatural. In the two cases, we have a sort of implicit external human intervention.

§30.25 As for MLL+MIX with units, the links 1 and $⊥$ cannot create cycles, hence any correct proof-structures with 1 and $⊥$ added will yields a correct proof-structure with the usual MLL+MIX correctness criterion. If we consider MLL+MIX and not MLL then there is nothing to change for the verification correctness (no jumps).

Criteria for additive proof-structures

§30.26 Assume we use additive boxes (cf. Figure 29.11) to represent MALL proofs. Boxes are frozen part of a proof. It is sufficient to hide the content of boxes and see boxes are generalised axioms and check for multiplicative correctness (cf. Figure 30.14). Then the content of each box should be correct as well. This generalised axiom is an hyperedge connecting all conclusions of the boxes (the conclusion of the box and the conclusions of the contexts associated with the box).
§30.27 In more recent representations of additive proof-structures, it is possible to find other correctness criteria [HVG03, HH16].

**Criteria for exponential proof-structures**

§30.28 Correctness for MELL (cf. Figure 29.13) is similar to correctness for multiplicative units and additive boxes:

• boxes are seen as generalised axiom and multiplicative correctness is checked in that context then locally for the content of each box;

• the only problematic structural rule is weakening which acts exactly like $\perp$ (cf. Section 30). Hence either we must consider MELL+MIX or jumps.

§30.29 We have previously seen that it was possible to encode untyped $\lambda$-terms with proof-structures (cf. Paragraph 29.27). MELL correctness then corresponds to choosing a type assertion $\Gamma \vdash M : A$ and typechecking a term $M$, i.e. verifying if $M$ can be typed with $A$ in the typing context $\Gamma$.

**31 Discussion: the structure of normative constraints**

§31.1 So, what linear logic and proof-net theory teach us about the nature of logic? Linear logic teaches to beware the appearance. The logical notions which are naturally accessible to our intuition such as disjunction ($\vee$), conjunction ($\wedge$) or implication ($\Rightarrow$) can hide subtle mechanisms. It is possible to provide an analysis of existing logical notions such as the implication $A \Rightarrow B$. It does not mean that if we “opened the black box” of implication, we would find linear logic providing new black boxes waiting to be opened, as if we had reductionist Matryoshka dolls. Linear logic should probably be understood as a tool to analyse our practice of logic. In particular, it may be possible to construct even more refined tools.

§31.2 From linear logic sequent calculus proofs, it is possible to characterise a bit more the essence of proofs by considering proof-nets. A problem is: what the essence of proof even is? In what direction should we go to extract this essence of proof? Technical considerations tell us that the essence of proofs corresponds to a notion of canonicity, i.e. of invariance under some equivalences on sequent calculus proofs. However, developments in proof-net theory seem to tell us that logic lives beyond sequent calculus and that this relative canonicity is probably not sufficient if we are interested in foundational questions.

§31.3 **Are correctness criteria useless.** When looking back at the history of linear logic and the introduction of proof-nets, a question may come to our mind: what is the purpose of correctness criteria? Why would we even want to check whether a proof-structure,