Keywords: Size-change, PSPACE-complete, Complexity, sequent calculus, non-wellfounded proofs, circular proofs, induction, coinduction, fixed points, proof-search, linear logic, muMALL, finitization. F

Titre : Représentations circulaires de preuves infinies pour les logiques à points fixes : expressivité et complexité.

Résumé : Dans le cadre des logiques adaptées aux plus petits et plus grands points fixes de formules, les preuves circulaires ont été proposées comme alternative aux principes d'induction et coinduction à invariants explicites. Ces preuves circulaires ont reçu un intérêt grandissant ces dernières années avec le développement simultané de leurs applications et de leur méta-théorie. Les preuves infinies sont maintenant bien implantées dans plusieurs sujets de la théorie de la démonstration tels que les prédicats inductifs à la Martin-Löf, la logique linéaire étendue avec des points fixes, etc.

Dans le cadre des preuves circulaires ou infinies, non bien-fondées, un critère de validité est nécessaire pour rétablir la cohérence logique. Ce critère sert à distinguer, parmi l'ensemble des prépreuves infinies ou circulaires, celles qui sont des preuves valides. Une approche maintenant standard est de considérer qu'une prépreuve est valide si chacune de ses branches infinies est justifiée par un thread qui progresse infiniment souvent.

Cette thèse étudie ces problèmes dans le cadre plus spécifique de MALL étendue avec des points fixes. On sait que, étant donnée une représentation circulaire finie d'une prépreuve non bien-fondée, il est possible de décider en espace polynomial si cette prépreuve est valide vis-à-vis du critère de threads. La première contribution de cette thèse est de démontrer que ce problème de décider le critère de threads pour µMALL ω est en fait PSPACE-complet. Notre démonstration est fondée sur une étude approfondie des liens entre le critère de threads et le principe de size-change termination, habituellement utilisé pour garantir la terminaison de programmes.

La deuxième contribution de cette thèse est de décrire un nouveau fragment de l'ensemble des représentations circulaires valides de prépreuves, fondé sur un critère de validité plus contraignant. Ce nouveau critère s'appuie sur un étiquetage des formules et des preuves, et sa validité est purement locale. Il permet à ce fragment d'être plus simple à manipuler, tout en restant suffisamment expressif pour contenir l'image des preuves finitaires du système µMALL de David Baelde, qui fonctionnent avec des invariants explicites d'induction et de coinduction. En particulier, il est possible de décider efficacement la validité d'une prépreuve circulaire vis-à-vis de ce nouveau critère, et de calculer efficacement un étiquetage qui certifie cette validité.

De plus, et ceci constitue la troisième contribution de cette thèse, la conjecture de Brotherston-Simpson est vraie pour ce fragment : nous décrivons une méthode qui permet de transformer toute preuve circulaire étiquetée de notre fragment en une preuve finitaire, avec des invariants d'induction et de coinduction explicites. Finalement, nous explorons des manières d'étendre ces résultats de validité et de finitisation à un plus grand fragment, en relâchant les contraintes de l'étiquetage tout en conservant (1) la possibilité de certifier localement la validité des preuves et (2) dans une certaine mesure, la possibilité de finitiser les preuves circulaires ainsi étiquetées.

Mots clefs : Size-change, PSPACE-complet, complexité, calcul des séquents, preuves non bien-fondées, preuves circulaires, induction, coinduction, points fixes, recherche de preuves, logique linéaire, muMALL, finitisation. Title: Circular representations of infinite proofs for fixed-points logics: expressiveness and complexity.

Abstract: In the context of logics with least and greatest fixed points, circular, i./,e. non wellfounded but regular proofs have been proposed as an alternative to induction and coinduction with explicit invariants. Those circular proofs have received increasing interest in recent years with the simultaneous development of their applications and metatheory: infinitary proof theory is now well-established in several proof-theoretical frameworks such as Martin-Löf's inductive predicates, linear logic with fixed points, etc.

In the setting of non wellfounded proofs, in order to recover logical consistency, it is necessary to consider a validity criterion which differentiates, among all infinite or circular derivation trees, a. k. a. preproofs, those which are logically valid proofs. A standard approach is to consider a preproof to be valid if every infinite branch is supported by an infinitely progressing thread. This thesis focuses on circular proofs for MALL with fixed points. It is known that given a finite circular representation of a non-wellfounded preproof, one can decide in PSPACE whether this preproof is valid with respect to the thread criterion. The first contribution of this thesis is to prove that the problem of deciding thread-validity for µMALL ω is in fact PSPACE-complete. Our proof is based on a deeper exploration of the connection between thread-validity and the size-change termination principle, which is usually used to ensure program termination.

The second contribution of this thesis is to describe a new fragment of all valid circular representations of preproofs, based on a stronger validity criterion. This new criterion is based on a labeling of formulas and proofs, whose validity is purely local. This allows this fragment to be easily handled, while being expressive enough to still contain all circular embeddings of Baelde's µMALL finite proofs with inductive and coinductive invariants. In particular, deciding validity and computing a certifying labelling can be done efficiently.

Moreover, and this is the third contribution of this thesis, the Brotherston-Simpson conjecture holds for this fragment: every labeled representation of a circular proof in the fragment is translated into a standard finitary proof. Finally, we explore how to extend these results to a bigger fragment, by relaxing the labeling discipline while retaining (1) the ability to locally certify the validity and (2) to some extent, the ability to finitize circular proofs.

Introduction

Generalities on least and greatest fixed points 1.Basic definitions

The general subject of this thesis is the study of least and greatest fixed points in logic.

The basic notions of least and greatest fixed points are easily described in the setting of ordered sets.

If (E, ) is an order and f : E → E is a non-decreasing endofunction, an element x ∈ E is a fixed point of f when f (x) = x.

More than general fixed points, what interests us are pre-and post-fixed points. An element x ∈ E is a pre-fixed point of f when f (x) x, and it is a post-fixed point of f when x f (x).

Even more precisely, what we want to talk about are least pre-fixed points and greatest post-fixed points. An element x ∈ E is a least pre-fixed point of f when f (x) x and ∀y ∈ E, f (y) y ⇒ x y. And x is a greatest post-fixed point of f when x f (x) and ∀y ∈ E, y f (x) ⇒ y x. There are usual notations for that: the least pre-fixed point of a non-decreasing function f is denoted, when it exists, by µxf (x), and similarly its greatest post-fixed point is denoted by νxf (x).

Note that the least pre-fixed point of a non-decreasing function is always a fixed point, and therefore it is its least fixed point.

Proving their existence

The main theorems on the existence of least and greatest fixed points are the following:

1 Introduction Theorem 1. Let (E, ) be an ordered set.

If every well-ordered subset of E has a least upper bound

(1.1) in which we recall that a subset A of E is said to be directed when every finite subset of A has an upper bound in A.

Proof elements and references.

• First remark that, as already mentionned above, a least pre-fixed point is always a fixed point and, therefore, (1.2) is stronger than (1.3). Similarly, every well-ordered subset of an order is either empty or directed. Hence (1.4) is stronger than (1.1).

That is why the two parts 1 and 2 of that theorem are indeed converse to each other.

• The direction 1 seems to be a folklore theorem which is difficult to trace back to a unique original author. Yet the first version of it seems to be that of Abian and [START_REF] Brown | A theorem on partially ordered sets, with applications to fixed point theorems[END_REF], although it is very close to a similar theorem by [START_REF] Bourbaki | Sur le theoreme de zorn[END_REF].

See [Lassez, Nguyen, and Sonenberg, 1982, Section 4] for a bibliographic study of its origins. See Davey and Priestley [2002, Exercise 8.19, p. 198] for a quick proof using ordinal induction.

• The direction 2 is more recent and has been proved by [START_REF] Markowsky | Chain-complete posets and directed sets with applications[END_REF].

To the reader interested by those questions, we recommend the book by Davey and Priestley [2002, in particular ch. 8, p. 175, and the bibliographic discussion p. 285], which contains more details and references about fixed-point theorems.

That theorem characterizes, in a sense, the preorders on which it makes sense to study the least fixed points of non-decreasing endofunctions. And it says that in these preorders,

1.1 Generalities on least and greatest fixed points those least fixed points are in fact least pre-fixed points. Those orders are called complete partial orders, or CPO.

Because of that theorem, we will commonly say "least fixed point" when talking about least pre-fixed points, and similarly for greatest fixed points.

Expressivity in logic

We will now motivate the will to add a connective to logic that has the behavior of forming a least fixed point by a first example, coming from temporal logic. We will see that least pre-fixed points and greatest post-fixed points give the possibility to define new formulas, and therefore add expressivity to the language. Such ideas are the basis of modal µ-calculus [START_REF] Kozen | Results on the propositional mu-calculus[END_REF].

Let us consider a logic like LTL [START_REF] Pnueli | The temporal logic of programs[END_REF], in which the truth of a proposition A may depend on an instant t ∈ N. The boolean denotation of a formula A is a A : N → {0, 1} and if t ∈ N, we denote by A t ∈ {0, 1} the truth value of A at t. As an alternative, we may write t A for A t = 1. We use one logical connective and two temporal connectives. For each of them, we give two equivalent definitions:

"or"

A ∨ B t = max A t , B t t A ∨ B ⇔ t A or t B "next" A t = A t+1 t A ⇔ t + 1 A "eventually" ♦A t = max A s | s t t ♦A ⇔ ∃s t, s A
We abuse the notation by using A B to denote the fact that ∀t ∈ N, A t B t , that is, equivalently: ∀t ∈ N, if t A then t B. Now we say that Proposition 1. For every formulas A and B, the following are true:

A ∨ ♦A ♦A (1.5) A ∨ B B ♦A B (1.6)
Proof.

1. Proof of (1.5)

1 Introduction

Assume that t ∈ N and t A ∨ ♦A. There are two cases:

t A

In that case t ♦A.

t ♦A

In that case t + 1 ♦A, that is ∃s t + 1, s A, so t ♦A.

Hence, in any case, t ♦A.

2. Proof of (1.6)

Let us assume that

A ∨ B B (1.7)
and show that ♦A B.

2.1. We first prove the following lemma: ∀u ∈ N, ∀t ∈ N, t + u A ⇒ t B.

Proof: By induction on u.

2.1.1. Case u = 0:

In that case we know that t A, hence t A ∨ B. By assumption (1.7) we get t B.

2.1.2. Case u = v + 1:

In that case we know that t + 1 + v A. Assume a t ∈ N and t ♦A, that is assume a s ∈ N, s t and s A. It remains to show that t B. This is exactly given by (1.8) above.

This relates to our previous description of least/greatest pre-/post-fixed points in the following way. If we consider as our order, we just proved that ♦A is a least pre-fixed point of F : X → A ∨ X, because we proved that F (♦A) ♦A and ∀B, F (B) B ⇒ ♦A B, with being .

That means that if we are allowed to use least pre-fixed points in the construction of the formulas, we do not need ♦ to be given as a primitive connective of the logic;

we could define it as ♦A := µX(A ∨ X). Dually, you can check that the "always" operator, denoted by A and defined equivalently by A t = min A s | s t or t A ⇔ ∀s t, s A could alternatively be defined as the greatest post-fixed point A := νX(A ∧ A).

Expressivity in programs

Least pre-fixed points and greatest post-fixed points can also be used to model inductive and coinductive datatypes in programming languages. We will try to show that on a second example.

In this example, we will use an OCaml-like syntax, although we are not writing strictly legit OCaml. We are trying to convey a general intuition, which probably apply mutatis mutandis to any programming language in which one can define inductive algebraic datatypes.

Let us consider the type of integer lists, which can be described as: 1 Introduction

type

C

In this example, for every two types α and β, let us say that α β when the type α -> β is inhabited. Then if we take F (α) to be the type α t, we have F (int list) int list because of inj. And each time we have a type α such that F (α) α, we also have int list α thanks to fold. So it makes sense to say that int list is a least pre-fixed point of t.

Another way of saying it is that int list = µα(1 + int * α). And the general idea is that inductive datatypes correspond to least pre-fixed points of functors. And, dually, coinductive datatypes correspond to greatest post-fixed points of functors. For instance, we could define a type of integer streams as int stream = να(int * α).

Remark 1. Actually the previous example is not totally complete. That example characterises int list as the least pre-fixed point of t, but it happens that the singleton type 1 could fit this description as well. In fact, the description of least and greatest fixed points in terms of orders or preorders does not give enough precision. To have a complete characterisation of int list as a least fixed point, we would need to talk about the computational behaviour of the functions, and we would need to shift from the setting of orders and preorders to the setting of categories, which is out of the scope of this introduction.

Usage in logic

There has been a lot of logics allowing the use of least and greatest fixed-point constructions in their formulas. Let us simply mention here some of the most noticeable.

de Bakker and de Roever [1972] define a logic with least fixed points to prove properties of recursively defined programs. [START_REF] Aczel | An introduction to inductive definitions[END_REF] study the extension of recursion theory with inductive definitions. [START_REF] Aho | The universality of data retrieval languages[END_REF] study the relational calculus, which may be understood as first-order logic, and suggest extending it by adding a least fixed-point operator, in order to make it more expressive. [START_REF] Gurevich | Fixed-point extensions of first-order logic[END_REF] study the expressive power of different extensions of first-order logic with fixed point induction. [START_REF] Dawar | Fixed point logics[END_REF] study the expressive power of fixed point logics.

Least and greatest fixed points in proof theory

Least and greatest fixed point of formulas may be seen as a way to formulate definitions by induction, or by coinduction. We will study those least and greatest fixed points from the 1.2 Least and greatest fixed points in proof theory point of view of proof theory. We believe that, through the proof-program correspondence, the analysis we make on proofs could also be applied to programs. The advantage of proofs over programs for our study is that they provide a system which makes things visible, decomposing things in simple elements: subformula property, cut-elimination, formulas occurrences, . . .

Proof theory

We do here a short recall of a few elements that made the success of modern proof theory and sequent calculus.

In usual sequent calculus, a proof is defined to be a finite proof tree.

The subformula property says that if you can prove a given conclusion then you can do it by using only subformulas of this conclusion. This is a fundamental property, saying, intuitively, that if I ask you a question ("Is this formula true ?"), you can answer it using only the concepts that are already present in the question, you do not need to introduce any new concept. You may still do it, because it may ease the task, but you do not need it.

The cut rule is the rule that allows you to do some deductive reasoning. It is a generalisation of two logical principles, modus ponens, which says that from a proof of A and a proof of A ⇒ B, you can build a proof of B, and the transitivity of implication, which says that from a proof of A ⇒ B and a proof of B ⇒ C you can build a proof of A ⇒ C.

One of the ideas that made sequent calculus so successful is that all inferences preserve the subformula property, except for the cut rule. When following this discipline, the subformula property amounts to saying that we can eliminate cuts from any proof.

Usage of fixed points in proof theory

Various logical settings have been introduced to reason about inductive and coinductive statements, both at the level of the logical languages modelling (co)induction (Martin Löf's inductive predicates vs. fixed-point logics, that is µ-calculi) and at the level of the proof-theoretical framework considered (finite proofs with (co)induction à la [START_REF] Park | Fixpoint induction and proofs of program properties[END_REF] vs. infinite proofs with fixed-point/inductive predicate unfoldings) [START_REF] Brotherston | Sequent calculus proof systems for inductive definitions[END_REF][START_REF] Brotherston | Complete sequent calculi for induction and infinite descent[END_REF][START_REF] Girard | The Blind Spot: lectures on logic[END_REF][START_REF] Baelde | Least and greatest fixed points in linear logic[END_REF][START_REF] Baelde | On the proof theory of regular fixed points[END_REF][START_REF] Baelde | Least and greatest fixed points in linear logic[END_REF].

Moreover, such proof systems have been considered over classical logic [START_REF] Brotherston | Sequent calculus proof systems for inductive definitions[END_REF][START_REF] Brotherston | Sequent calculi for induction and infinite descent[END_REF], intuitionistic logic [START_REF] Clairambault | Least and greatest fixpoints in game semantics[END_REF], linear-time or branching-time temporal logic [START_REF] Kozen | Results on the propositional mu-calculus[END_REF], Kaivola, 1995b[START_REF] Walukiewicz | On completeness of the mu-calculus[END_REF], 1995, 1 Introduction Dax, Hofmann, and Lange, 2006, Doumane, 2017b[START_REF] Doumane | Towards completeness via proof search in the linear time µ-calculus: The case of büchi inclusions[END_REF] or linear logic [START_REF] Santocanale | A calculus of circular proofs and its categorical semantics[END_REF][START_REF] Fortier | Cuts for circular proofs: semantics and cutelimination[END_REF][START_REF] Baelde | Least and greatest fixed points in linear logic[END_REF], Baelde, Doumane, and Saurin, 2016, Doumane, 2017b].

In all those proof systems, the treatment of inductive and coinductive reasoning brings some highly complex proof objects.

Finite proof systems for least and greatest fixed points

The first systems designed to reason about fixed points of formulas were systems with finite proofs, in which induction and coinduction principles are used in order to provide a finite proof theory for reasoning on formulas with least or greatest fixed points [START_REF] Kozen | On induction vs. *-continuity[END_REF][START_REF] Kozen | Results on the propositional mu-calculus[END_REF][START_REF] Baelde | Least and greatest fixed points in linear logic[END_REF].

But finite proof systems for least and greatest fixed points have some drawbacks.

• To introduce a greatest fixed point formula or to eliminate a least fixed point formula, you have to use a rule of induction or coinduction, and you have to provide an explicit invariant, which has to be a formula of the same system. This is a restriction because the language of formulas may not be expressive enough to express all the invariants you may need to prove formulas that should intuitively be true, as was shown, for instance, by Berardi andTatsuta [2017b, 2019] in the context of first-order classical logic with inductive definitions.

• It breaks the subformula property.

• Here, in the finitary setting for least and greatest fixed points of formulas, the failure of the subformula property can therefore be restated by saying that we cannot eliminate all cuts. Nevertheless, it makes sense to define a procedure of "cut elimination" for this setting. This procedure will not eliminate all cuts, but it will simplify them and eliminate some of them and it is still a terminating procedure, which leaves the proof in a normal form in which the only remaining cuts are of a very specific form, and are cuts that cannot be reduced anymore. The point is that in this setting, besides the fact that we cannot completely eliminate cuts, this procedure of cut elimination turns out to be quite complex.

For instance, in proof systems using (co)induction rules à la Park, the rules allowing to derive a coinductive property (or dually to use an inductive hypothesis) have a complex inference of the form of Figure 1.1 (when presented in the setting of fixed-point logichere we follow the one-sided sequent tradition of MALL that we will adopt in the rest of the thesis).

1.2 Least and greatest fixed points in proof theory but it is also problematic for at least two additional and more technical reasons: (i) it is hiding a cut rule that cannot be eliminated, which is problematic for extending the proof-program correspondence to fixed-points logics, and (ii) it breaks the subformula property, which is problematic for proof search: at each coinduction rule, one has to guess an invariant (in the same way as one has to guess an appropriate induction hypothesis in usual mathematical proofs).

Γ, S S ⊥ , F [S/X] (ν inv ) Γ, νXF

Infinite proof systems for least and greatest fixed points

Infinite proofs have been introduced to reason on (least and greatest) fixed points of formulas.

For all these reasons, infinite (non-wellfounded) proofs, which are infinite proofs satisfying a validity criterion, have been proposed, in recent years, as an alternative to induction and coinduction with explicit invariants [START_REF] Brotherston | Sequent calculus proof systems for inductive definitions[END_REF][START_REF] Brotherston | Complete sequent calculi for induction and infinite descent[END_REF][START_REF] Girard | The Blind Spot: lectures on logic[END_REF]. By replacing the coinduction rule with simple fixed-point unfoldings and allowing for non-wellfounded branches, those proof systems address the problem of the subformula property for the cut-free systems. The cut-elimination dynamics for inductive-coinductive rules is also much simpler. In particular, Baelde, Doumane, and Saurin [2016], inspired notably by [START_REF] Dax | A proof system for the linear time µcalculus[END_REF], proposed a very successful system of infinite proofs, called µMALL ∞ , to reason on least and greatest fixed points of formulas. Actually, this is for the propositional setting, but such ideas already existed to reason on inductive and coinductive predicates.

Infinite, non well-founded, proofs present the advantage over explicit induction or coinduction to offer a framework in which it is possible to recover the good structural properties of sequent calculus, such as cut-elimination, subformula property and focusing, making them a more suitable tool to automated proof search. Indeed, cut-elimination and focusing have recently been extended to non well-founded proofs for µMALL by Baelde, Doumane, and Saurin [2016], Doumane [2017b].

Now the problem is that if we take this approach too naively, by simply allowing proof trees to be infinite, then two bad things happen:

1. the system becomes inconsistent, meaning that every formula becomes provable;

1 Introduction . . . (µ) µXX, Γ (µ) µXX, Γ . . . (ν) νXX, Γ (ν) νXX, Γ (cut) Γ Figure 1.2
2. the cut-elimination procedure becomes a non-terminating, non-converging one.

The price to pay is that the consistency of the logical system is broken and that a validity criterion has to be added in order to ensure consistency.

More precisely, in those proof systems when considering all possible infinite, nonwellfounded derivations, or preproofs, it is straightforward to derive any sequent Γ (see Figure 1.2).

Such preproofs are therefore unsound and one needs to impose a validity criterion to distinguish, among all preproofs, those which are logically valid proofs from the unsound ones.

A solution to that is to say that all these infinite proof trees are only preproofs, and that only some of these preproofs are valid proofs. This means that we need a criterion to distinguish valid (pre)proofs from invalid preproofs, and to reflect the inductive and coinductive nature of our fixed-point connectives.

A standard approach [START_REF] Brotherston | Sequent calculus proof systems for inductive definitions[END_REF][START_REF] Brotherston | Complete sequent calculi for induction and infinite descent[END_REF][START_REF] Girard | The Blind Spot: lectures on logic[END_REF][START_REF] Santocanale | A calculus of circular proofs and its categorical semantics[END_REF], Baelde, Doumane, and Saurin, 2016] considers a preproof to be valid if every infinite branch is supported by an infinitely progressing thread. This is called the thread criterion.

However, doing so, the logical correctness of circular proofs becomes a non-local property, much in the spirit of proof nets correctness criteria [Girard, 1987, Danos and[START_REF] Danos | The structure of multiplicatives[END_REF]].

Finite representations and circular proof systems for least and greatest fixed points

The problem with infinite proofs, on the other hand, is mainly that they are infinite, which has two major drawbacks:

1.2 Least and greatest fixed points in proof theory

1. The first one is epistemic: we would like a proof to be a finite object, which I can communicate to you in finite time, and which you can check in finite time. The fact that a proof may be an infinite object means that I may not be able to give you a proof, but I will in fact give you the finite description of an infinite proof, formulated in the meta-theory.

2. The second one is practical: if we want our system to be used in an automated prover or in a proof assistant, we need those proofs to be finitely representable.

It means that whatever system of representation you chose, you will not be able to represent all infinite proofs, because there is an uncountable number of infinite proofs and your system of finite representations will only be able to represent a countable number of them.

From that it may seem that going from finite to infinite proofs was a mistake. But infinite proofs give great insights on least and greatest fixed points of formulas, on their different proof systems and on the dynamic of cut-elimination in those systems, including the finitary ones. In particular they provide us with a new way to understand the finitary systems. Each finitary proof can be translated into an infinitary one. This means that finitary proofs may be seen as one particular way to represent some of those infinitary proofs. So now we may transform the question of designing a finitary proof system for least and greatest fixed points of formulas into the question of identifying suitable fragments of the infinitary system, which have some nice-behaved representations.

Among those non-wellfounded proofs, circular proofs, that have infinite but regular derivation trees, have attracted a lot of attention for retaining the simplicity of the inferences of non-wellfounded proof systems but being amenable to a simple finite representation making it possible to have an algorithmic treatment of those proof objects.

In this context, a very natural way of representing some infinite proofs is to use finite proof trees with back edges. This means that instead of constructing explicitely an infinite branch, we are allowed to stop at some point and point out some previous step of the construction and say: from there, we start again at that point. Such a cyclic representation has a canonical unfolding into an infinite proof tree. This system of representations allows us to represent some of the infinite preproofs. Those preproofs that can be represented by such a proof tree with back edges are called circular preproofs. Those representations are called circular representations.

Despite the need for a validity condition, circular, i. e. non-wellfounded but regular proofs have received increasing interest in recent years with the simultaneous development of their applications and meta-theory: infinitary proof theory is now well-established in several proof-theoretical frameworks such as Martin Löf's inductive predicates, linear logic with fixed points, etc.

In this thesis

Statement of the contribution On the question of how much time and space it takes to check the thread criterion on a circular representation of an infinite preproof, it was known how to do it in PSPACE, and we prove in this thesis that this problem is PSPACE-complete, which means that we cannot do substantially better.

As we would like to be able to ckeck our proofs in polynomial time, we provide a new validity criterion, which is stronger than the thread criterion while accepting at least the translations of finitary proofs, and which can be checked in quadratic time.

We also would like a proof system in which there is no global criterion to check, in which a proof is correct as soon as each inference used in it is correct. This is made possible. We provide such a proof system, obtained by adding some labelling to the circular representations accepted by my new quadratic criterion.

Finally, this new proof system proves at least as much propositions than the finitary setting and it is legit to ask how much more it does prove exactly. The answer is: No more.

This result may look disappointing but what it says is that every circular representation of an infinite preproof that is valid for my quadratic criterion and every proof in my labelled system can be turned into a finitary proof with the same conclusion. And we provide an effective method to do it. In other words, we provide a method to synthetize some induction and coinduction invariants, finitize some circular proofs and partially answer the Brotherston-Simpson conjecture.

Fixed points in linear logic

This thesis focuses on circular proofs for MALL with fixed points. Least and greatest fixed point were already well-established in linear logic [START_REF] Baelde | Least and greatest fixed points in linear logic[END_REF][START_REF] Baelde | Least and greatest fixed points in linear logic[END_REF], Baelde, Doumane, and Saurin, 2016, Doumane, 2017b] and we build on this basis to contribute to several directions in the field of circular proofs:

1. the relationship between finite and circular proofs (at the level of provability and at the level of proofs themselves) and 2. the certification of circular proofs, that is the production of fast and/or small pieces of evidence to support validity of a circular preproof.

Addressed questions, proposed answers

Proof-checking Among all circular preproofs, some are valid proofs and some are not.

The thread criterion gives a non-ambiguous mathematical definition of whether a circular representation represents a valid (pre)proof or an invalid preproof. The first interesting question is whether there exist a method to tell whether the circular representation of a preproof is valid or not. In other words: is the thread criterion on circular preproofs decidable? Given a finite circular representation of a non-wellfounded preproof, can one decide whether this preproof is valid with respect to the thread criterion?

The answer to that is yes: there is an algorithm which is able to tell the difference between a valid circular representation of a preproof and an invalid one. In fact several such algorithms are known.

The next question would be: how difficult is this problem? What is its computational complexity? When we started to look at this problem, the state of the art was the following: all known algorithms for this problem ran in exponential time and ran or could be made to run un polynomial space. But no subexponential algorithm was known, there was no lower bound on its complexity and the exact complexity of checking the thread criterion was still unknown. Recall that P ⊆ NP ⊆ PSPACE ⊆ EXP. The first contribution of this thesis is to prove that this problem is in fact PSPACE-complete.

This implies in particular that this problem is probably not in NP and that there is probably no subexponential algorithm to solve it.

Our proof is based on a deeper exploration of the connection between thread-validity and the size-change termination principle [START_REF] Chin | The size-change principle for program termination[END_REF], which is usually used to ensure program termination.

Circular proofs have already proved useful in implementing efficient automatic provers, e. g. the Cyclist prover [START_REF] Gorogiannis | The cyclist theorem prover[END_REF]. The complexity avoided in the search, thanks to the fact that we need not to guess invariants, is counterbalanced by the complexity of the validity criterion at the time of proof checking. It seems however that this approach gives good performances in practice.

A new validity criterion Among all representations of valid circular proofs, a new fragment is described in Chapter 4, based on a stronger validity criterion. This new criterion is based on a labelling of formulas and proofs, whose validity is purely local.

This allows this fragment to be easily handled, while being expressive enough to still contain all circular embeddings of Baelde's µMALL finite proofs with (co)inductive invariants: in particular deciding validity and computing a certifying labelling can be done efficiently.

Finitization Comparing finite and infinite proofs is very natural. Informally, it amounts to considering the relative strength of inductive reasoning versus infinite descent: while infinite descent is a very old form of mathematical reasoning which appeared already in Euclid's Elements and was systematically investigated by Fermat, making precise its relationship with mathematical induction is still an open question for many proof formalisms. Their equivalence is known as the Brotherston-Simpson conjecture. While it is fairly straightforward to check that infinite descent (circular proofs) proves at least as many statements as inductive reasoning, the converse is complex and remains largely open. A few years ago, [START_REF] Simpson | Cyclic arithmetic is equivalent to peano arithmetic[END_REF], on the one hand, and Berardi and Tatsuta [2017b,a], on the other hand, made progress on this question but only in the framework of Martin Löf's inductive definitions, not in the setting of µ-calculi circular proofs in which invariant extraction is highly complex and known only for some fragments.

We will show that the Brotherston-Simpson conjecture holds for the fragment we present:

every labelled representation of a circular proof in the fragment is translated into a standard finitary proof.

Propositions of extensions Finally we explore how to extend these results to a bigger fragment, by relaxing the labelling discipline while retaining (i) the ability to locally certify the validity and (ii) to some extent, the ability to finitize circular proofs.

A complex example

We conclude this introduction by considering a typical example of a circular proof with a complex validating thread structure: while this infinite proof has a regular derivation tree, its branches and threads have a complex geometry. The circular proof of Figure 1.3 derives the sequent F, G, H, I, J where

F = µX((X `G) & (X `H)) G = νX(X ⊕ ⊥) H = νX(⊥ ⊕ X) I = µZ((Z `J)⊕⊥) J = µX((K `X)⊕⊥) K = νY µZ((Z `µX(Y `X)⊕⊥)⊕⊥)
This example of a circular derivation happens to be valid (it is a µMALL ω proof) but the description of its validating threads is quite complex. Indeed, each infinite branch β is validated by exactly one thread (see next section for detailed definitions) going through either G, H or K depending on the shape of the branch at the limit (infinite branches of this derivations can be described as ω-words on A = {l, r} depending on whether the left or right back edge is taken):

(i) if β ultimately follows always the left cycle (A • l ω ), the unfolding of H validates β;

(ii) if β ultimately follows always the right cycle (A • r ω ), the unfolding of G validates β;

(iii) if β endlessly switches between left and right cycles (A • (r

+ • l + ) ω ), K validates β.
The description of the thread validating this proof is thus complex. This is reflected in the difficulty to provide a local way to validate this proof and in the lack of a general

F `H, G, I, J (ν)(⊕ 0 ),(⊥) F `H, G, H, I, J (&) (F `G) & (F `H), G, H, I, J (µ) F , G, H, I, J Figure 1.3. Proof π ∞
method for finitizing this into a µMALL proof: to our knowledge, the usual finitization methods (working only for fragments of µMALL ω circular proofs) do not apply here.

Outline of this thesis

The subject of this thesis is the study of finite circular representations of infinite proofs and preproofs.

It consists of 6 chapters:

• Chapter 1, this chapter, is an informal introduction to the subject of the thesis.

• Chapter 2 covers the technical background needed to develop the results of the thesis.

• Chapters 3, 4 and 5 are the technical chapters, presenting the main results and contributions of this thesis.

• Chapter 6 is a conclusion chapter.

In Chapter 2, we provide the necessary technical background to our work. Section 2.1 covers infinitary and circular proof theory of multiplicative additive linear logic with least and greatest fixed points. We recall the formulas and rules of MALL (Section 2.1.1), how they can and have been extended with least and greatest fixed point to obtain µMALL which are the true subject of this thesis (Section 2.1.4). We also recall some basic elements of the theories of algorithmic complexity (Section 2.2) and of ω-automata (Section 2.3).

(Section 2.1.2),
Chapter 3 is concerned with the algorithmic complexity of the thread criterion. We start by recalling in Section 3.1 that the thread criterion is effectively decidable in PSPACE.

The main section of the first technical chapter is Section 3.2, in which we show the PSPACE-completeness of the thread criterion for µMALL ω , in Theorem 4. Section 3.3 is devoted to a discussion of our approach and a comparison with related works. We conclude this chapter in Section 3.4.

Chapter 4 studies an approach to circular proofs based on labellings of greatest fixed points. We first motivate in Section 4.1 such labellings as an alternative way to express the validating threads. Then, in Section 4.2 we introduce finite representations of preproofs and use such labellings in order to locally certify their validity. Finally, in Section 4.3, we turn to alternative characterizations of those circular proofs which can be labelled. The fragment of labellable proofs, while quite constrained (for instance, it does not include the example of Figure 1.3), is already enough to capture the circular proofs obtained by translation of µMALL proofs.

In Chapter 5 and Section 5.1, we address the converse: for any labelled derivation tree with back edges, we provide a corresponding µMALL proof by generating a (co)inductive invariant based on an inspection of the labelling structure. Therefore, we answer the Brotherston-Simpson conjecture in a restricted fragment. In Section 5.2, we introduce a more permissive labelling strategy that allows to label more proofs (in particular by allowing to loop not only on (ν) rules but on any rule) and that still ensures validity of the labellable derivations. For this relaxed labelling, we label the example of Figure 1.3 and show how to finitize it by adapting the method of Section 5.1. Nevertheless, there is not yet a general method applicable to the complete extended labelling fragment. We end this chapter by a discussion, in Section 5.5, of related works to both Chapters 4 and 5.

Relations between the various systems considered in these two chapters are summarized in Figure 1.4.

Technical background

2.1 Proof theory for least and greatest fixed points

Usual proof theory and MALL

Logic is generally built around two main concepts: formulas and proofs.

Formulas or propositions, model some statements that you may say, and which may, intuitively, be true or false such as "The cat is black" or "Earth is flat". But logic and proof theory are more interested in understanding the nature of the logical connectives and their dynamic than in what happens to be true in our world. That is why a formal language of formulas is generally built out of some propositional variables and some connectives. For instance a language of formulas for the classical logic LK may be defined by the following grammar:

A, B ::= X | X | A ∧ B | A ∨ B | | ⊥
where X ranges over a given set of propositional variables, which we denote by X, Y, Z, . . . ∧ denotes conjunction, "and", while ∨ denotes disjunction, "or". The constants and ⊥ represent their respective neutral elements, that is respectively a true statement and a false statement. The variables X, Y, Z, . . . represent some undetermined statements.

That means that, for instance, (X ∨ Y ) ∧ (Y ∨ Z) is a formula of LK, which you may read as "not X or Y , and not Y or Z".

The main logic we will use to apply our methods in this thesis is the logic MALL, composed of the Multiplicative and Additive fragments of Linear Logic. Linear logic was designed by [START_REF] Girard | Linear logic[END_REF] in a successful attempt to decompose the well-known connectives of classical and intuitionistic logics into more elementary components. For a detailed introduction to linear logic, see [START_REF] Girard | Linear logic[END_REF], [START_REF] Girard | Proofs and Types[END_REF]] or [START_REF] Girard | The Blind Spot: lectures on logic[END_REF].

The formulas of MALL are defined by the following grammar:

Definition 1 (MALL formulas).

A, B ::

= X | X | A ⊗ B | A `B | 1 | ⊥ | A ⊕ B | A & B | 0 |
where X ranges over a given set of propositional variables.

The set of all MALL formulas is denoted by Fml MALL .

⊗ and & are conjunctions of different natures and 1 and are their respective neutral elements. `and ⊕ are disjunctions of different natures and ⊥ and 0 are their respective neutral elements.

Remark 2 (Precedence rules). The usage is that ⊗ and `, the "multiplicative" connectives, have a higher precedence than ⊕ and &, the "additive" connectives. For instance

X Y & X `Y should be read as (X `Y ) & (X `Y ).
With such a syntax of formulas come a syntax for the positions of subformulas inside formulas. To that effect we use the following alphabet Let A Fml be the following alphabet:

P MALL = {⊗ 0 , ⊗ 1 , `0, `1, ⊕ 0 , ⊕ 1 , & 0 , & 1 }
We denote by P * MALL the free monoid of finite words on P MALL . Those words are used to denote the position of a subformula in a formula.

Definition 2 (Positions of subformulas in a formula). The set of positions of subformulas of a given formula A is defined by induction on A:

2.1 Proof theory for least and greatest fixed points

Example 1. The set of positions of subformulas of X ⊗ (⊥ ⊕ Y ) is { , ⊗ 0 , ⊗ 1 ⊕ 0 , ⊗ 1 ⊕ 1 }.
Those formulas are equipped with an involutive negation, denoted by • ⊥ and defined inductively as follows:

Definition 3.

X ⊥ = X X ⊥ = X (A ⊗ B) ⊥ = A ⊥ `B⊥ (A `B) ⊥ = A ⊥ ⊗ B ⊥ 1 ⊥ = ⊥ ⊥ ⊥ = 1 (A ⊕ B) ⊥ = A ⊥ & B ⊥ (A & B) ⊥ = A ⊥ ⊕ B ⊥ 0 ⊥ = ⊥ = 0
Proofs are certificates used to attest the truth of a formula. In this thesis, proofs are built in sequent calculus, following the usage of modern proof theory, initiated by Gentzen [1935aGentzen [ ,b, 1969]].

In sequent calculus, a proof is a finite tree built out of some given deduction rules. We recall the basics of that setting. We will exemplify it first on the particular case of MALL, then on MALL extended with least and greatest fixed point in the system µMALL. For a more detailed introduction to sequent calculus, you may look at [START_REF] Girard | Proofs and Types[END_REF]] or [START_REF] Girard | Proof theory and logical complexity[END_REF].

Definition 4 (Sequent). Given a set of formulas Fml, a sequent is defined to be a finite list of formulas. If Γ is a sequent of size n, we use the notation |Γ| to denote either n, the size of the list, or the set {0, . . . , n -1}, the set of indices of this list.1

A sequent is denoted by the symbol followed by its formulas. A sequent should be understood, intuitively, as the disjunction, in the `sense, of its formulas.

A proof is a tree made out of some logical inferences.

Definition 5 (Inference). An inference consists of :

• A finite number of sequents, Γ 0 , . . . , Γ n-1 , which are called the premises of the inference • A sequent Γ, which is called the conclusion of the inference

(id) A, A ⊥ Γ, A ∆, A ⊥ (cut) Γ, ∆ Γ, A ∆, B (⊗) Γ, ∆, A ⊗ B Γ, A, B (`) Γ, A `B (1) 1 Γ (⊥) Γ, ⊥ Γ, A (⊕ 0 ) Γ, A ⊕ B Γ, B (⊕ 1 ) Γ, A ⊕ B Γ, A Γ, B (&) Γ, A & B ( ) Γ, Figure 2.1. MALL inference rules • A partial function σ : |Γ 0 | + • • • + |Γ n-1 | |Γ| × P * where |Γ 0 | + • • • + |Γ n-1 | denotes the usual set-theoretic sum {0} × |Γ 0 | ∪ • • • ∪ {n -1} × |Γ n-1 |.
This function is called the threading function. It can equivalently be described by n partial functions

σ 0 : |Γ 0 | |Γ| × P * . . . σ n-1 : |Γ n-1 | |Γ| × P * This inference is written Γ 0 . . . Γ n-1 Γ
with the threading function σ generally left implicit.

The inference rules of MALL are given on Figure 2.1.

For instance, the rule

Γ, A ∆, B (⊗) Γ, ∆, A ⊗ B
should be understood, intuitively, as saying that for every lists of formulas Γ, ∆ and for every formulas A, B, whenever the sequents Γ, A and ∆, B are true, so is

Γ, ∆, A ⊗ B.
Formally, it should also be understood by this rule that in a (⊗) inference, the function σ sends any position of formula in Γ or ∆ in the premises to the corresponding position in the conclusion and the empty path, sends the position of A in the first premise on the position of A ⊗ B in the conclusion and the path ⊗ 0 and sends the position of B in the second premise on the position of A ⊗ B in the conclusion and the path ⊗ 1 . Meanwhile, the order of the formulas in the sequents is not imposed by the rule. For instance, this is a correct

(⊗) inference: X `X, X X, Y, Z (⊗) X ⊗ Y, X `X, X, Z
with the implicit function

σ : {0} × {0, 1} ∪ {1} × {0, 1, 2} {0, 1, 2, 3} × A * Fml (0, 0) → (1, ) (0, 1) → (0, ⊗ 0 ) (1, 0) → (2, ) (1, 1) → (0, ⊗ 1 ) (1, 2) → (3, )
Here this function happens to be total. The possibility to be partial is used in the (cut)

rule.

Definition 6 (Proof tree). A proof for MALL is any finite proof tree built with these inference rules.

Here is an example:

Example 2. (id) X, X (id) Y , Y (⊕ 0 ) Y , Y ⊕ Z (⊗) X, Y , X ⊗ (Y ⊕ Z) (`) X `Y , X ⊗ (Y ⊕ Z) (id) X, X (id) Z, Z (⊕ 1 ) Z, Y ⊕ Z (⊗) X, Z, X ⊗ (Y ⊕ Z) (`) X `Z, X ⊗ (Y ⊕ Z) (&) X `Y & X `Z, X ⊗ (Y ⊕ Z)
One of the interests of the threading functions is that they can be composed. This fact allows us to extend this definition in order to relate any two sequents which are connected by a chain of successive inferences:

Definition 7 (composition of threading functions). If

Definition 8 (Threading function associated to a path in a proof tree). Suppose a proof tree π. Suppose a sequence u = s 0 , s 1 , . . . , s n ) of positions of sequents in π and a sequence r 0 , r 1 , . . . , r n-1 of inferences in π such that ∀i ∈ 0, n -1 , s i is the conclusion of r i and s i+1 is a premise of r i . ∀i, let Γ i be the sequent at position s i in π. Then, by composing the threading functions of r 0 , r 1 , . . . , r n-1 , we get a function

σ(u) : |Γ n | |Γ 0 | × P * Example 3.
For instance, if we denote by u the following sequence of sequents and inferences, taken from the right of Example 2:

. . . . . . Z, Y (⊕ 1 ) Z, Y ⊕ Z (⊗) X, Z, X ⊗ (Y ⊕ Z) (`) X `Z, X ⊗ (Y ⊕ Z) (&) X `Y & X `Z, X ⊗ (Y ⊕ Z)
Then we have

σ(u) : |Z, Y | |X `Y & X `Z, X ⊗ (Y ⊕ Z)| 0 → (0, & 1 `1) 1 → (1, ⊗ 1 ⊕ 1 )
Definition 9 (Image of a subformula in an inference). Suppose a proof tree π and an

inference r = Γ 0 . . . Γ n-1 Γ in π. Let us denote by σ(r) the threading function of r. If Γ i is one of its premises, if A is a formula in Γ i , at position f ∈ |Γ i |, if p ∈ SubPos(A) is
a position of subformula in A, then to this position f • p of subformula in Γ i is associated, when possible, a position of subformula in Γ, denoted by t(r)(f • p) and defined as

t(r)(f • p) := g • q • p where (g, q) := σ(r)
This makes t(r) a partial function from positions of subformulas in the premises of r to positions of subformulas in the conclusion of r.

Similarly to what we did for threading functions in Definition 8, we can extend this definition of t from rules to paths in a proof tree:

Definition 10 (Image of a subformula through a path in a proof tree). Suppose a proof tree π. Suppose a sequence u = (s 0 , s 1 , . . . , s n ) of positions of sequents in π and a sequence r 0 , r 1 , . . . , r n-1 of inferences in π such that ∀i ∈ 0, n -1 , s i is the conclusion of r i and s i+1 is a premise of r i . ∀i, let Γ i be the sequent at position s i in π. Then, by composing the t(r i ), we get a partial function from the position of subformulas in Γ n to the positions of subformulas in Γ 0 , which we denote by t(u).

Proposition 2. With the notations of the previous definition, for every formula

A in Γ n , at position f ∈ |Γ n | and every position of of subformula p ∈ SubPos(A), if t(u)(f • p) is defined, then the subformula at position t(u)(f • p) in Γ 0 is identical to the subformula at position f • p in Γ n .
Proof. Immediate by induction on the length of u and examination of each possible rule. The threading functions have been chosen precisely to witness the subformula property.

Definition 11 (Path of subformula images). Suppose a proof tree π. Suppose a sequence u = s 0 , s 1 , . . . , s n ) of positions of sequents in π and a sequence r 0 , r 1 , . . . , r n-1 of inferences in π such that ∀i ∈ 0, n -1 , s i is the conclusion of r i and s i+1 is a premise of r i . ∀i, let Γ i be the sequent at position s i in π and let p be a subformula in one of the formulas of Γ n . We define a sequence of positions of subformulas p i 0 , . . . , p n , such that ∀i i 0 , p i is a subformula of a formula of Γ i . This sequence is defined as follows:

p n := p ∀i, p i-1 := t(r i-1 )(p i ) or, equivalently: ∀i, p i := t(s i , . . . , s n )(p)
The last defined index of this sequence, i 0 , is either 0 or the first i such that t(r i-1 )(p i ) is not defined, which happens if r i-1 is a cut and p i is in a cut formula. This sequence is denoted by T(u)(p) := p i 0 , . . . , p n

Finite proof trees: µMALL

In this section, we introduce the logic µMALL [START_REF] Baelde | Least and greatest fixed points in linear logic[END_REF], its formulas and proofs, which are finite sequent calculus proofs.

µMALL formulas The grammar of formulas is obtained by extending the formulas of MALL with two fixed-point connectives, µ and ν, denoting respectively least and greatest fixed points of formulas.

Formulas of µMALL are selected among a set of preformulas. Preformulas of µMALL are obtained by taking the usual formulas of MALL and adding two monadic second order binders, µ and ν:

Definition 12 (µMALL preformulas).

A, B ::

= X | A ⊗ B | A `B | 1 | ⊥ | A ⊕ B | A & B | 0 | | µXA | νXA
where X ranges over an infinite set of propositional variables.

The connectives µ and ν are binders and, as usual, preformulas are considered modulo renaming of bound variables. For instance, νX(X ⊗ X) and νY (Y ⊗ Y ) denote the same preformula.

Definition 13 (µMALL formulas). A formula is a closed preformula. We denote by

Fml the set of all formulas and we denote by the usual subformula ordering between formulas and preformulas.

Definition 14 (µMALL negation). An involutive negation • ⊥ is defined on every µMALL preformula, inductively specified by:

(A ⊗ B) ⊥ = A ⊥ `B⊥ 1 ⊥ = ⊥ X ⊥ = X (A ⊕ B) ⊥ = A ⊥ & B ⊥ 0 ⊥ = (µXA) ⊥ = νXA ⊥ Example 4. If A is any formula and F = νX(µY ((A⊗X)`Y )) then F ⊥ = µX(νY ((A ⊥ X) ⊗ Y )).
Remark 4. It may be counterintuitive that X ⊥ = X. Yet, in practice negation will only be applied to formulas, which are closed preformulas. This simple hack allows us to avoid In the presence of negative atoms, negation should be defined by:

Γ, A[µXA[X]] (µ) Γ, µXA[X] Γ, B B ⊥ , A[B] (ν inv ) Γ, νXA[X] Figure 2.2. µMALL rules for µ and ν Γ, A[µXA[X]] (µ) Γ, µXA[X] Γ, B B ⊥ , A[B] (ν inv ) Γ, νXA[X]
X ⊥ = X X ⊥ = X (µXA[X]) ⊥ = νXA[X] ⊥ (νXA[X]) ⊥ = µXA[X] ⊥
which does not change its definition on closed formulas. For instance, in Example 4 we would still have:

F ⊥ = (νX(µY ((A ⊗ X) `Y ))) ⊥ = µX(µY ((A ⊗ X) `Y )) ⊥ = µX(νY ((A ⊗ X) `Y ) ⊥ ) = µX(νY ((A ⊥ `X) ⊗ Y )) = µX(νY ((A ⊥ `X) ⊗ Y ))
µMALL inferences and proofs The proofs for µMALL are standard sequent calculus proofs, as described in Section 2.1.1. They are obtained by extending the inference system for MALL, in Remark 5. As it was mentionned in the informal introduction, in Section 1.2.3, the (ν inv )

rule of µMALL sequent calculus breaks the subformula property. Indeed, the B and B ⊥ that appears in the premises of the rule, on Figure 2.2, do not appear in its conclusion.

This means that anyone wanting to prove a ν formula by applying that rule has to find an appropriate B, which will act as an induction or coinduction invariant.

We recall two properties of µMALL, that will be used in Chapter 5. The first one is called functoriality:

Proposition 3. For every variable X and every formulas A[X], B, C of µMALL, the following rule is derivable in µMALL:

B, C [A] A ⊥ [B], A[C]
Proof. By induction on A. See [Baelde, 2012, Section 2.4] for a full proof.

The second one asserts the two following equivalences:

νXA[B[X]] ˛A[νXB[A[X]]] µXA[B[X]] ˛A[µXB[A[X]]]
Proposition 4. For every two formulas A[X], B[X] of µMALL, the following sequents are derivable in µMALL: Doumane, andSaurin, 2016, Doumane, 2017b] is a non well-founded proof system for an extension of MALL with least and greatest fixed points operators. It was designed to fix the defects of the (ν inv ) rule of µMALL.

νXA ⊥ [B ⊥ [X]], A[µXB[A[X]]] µXA ⊥ [B ⊥ [X]], A[νXB[A[X]]] Proof. Π 0 (A, B) = (id) B ⊥ [A ⊥ [νXB ⊥ [A ⊥ [X]]]], B[A[µXB[A[X]]]] (µ) B ⊥ [A ⊥ [νXB ⊥ [A ⊥ [X]]]], µXB[A[X]] [A] A ⊥ [B ⊥ [A ⊥ [νXB ⊥ [A ⊥ [X]]]]], A[µXB[A[X]]] (ν 0 inv ) νXA ⊥ [B ⊥ [X]], A[µXB[A[X]]] Γ, A[µXA[X]] (µ) Γ, µXA[X] Γ, A[νXA[X]] (ν) Γ, νXA[X] Figure 2.4. µMALL ∞ rules for µ and ν Γ, A[µXA[X]] (µ) Γ, µXA[X] Γ, A[νXA[X]] (ν) Γ, νXA[X] Figure 2.5. Threading functions for the (µ) and (ν) rules of µMALL ∞ Π 1 (A, B) = • • • • Π 0 (B ⊥ , A ⊥ ) B ⊥ [µXA ⊥ [B ⊥ [X]]], νXB[A[X]] [A] A ⊥ [B ⊥ [µXA ⊥ [B ⊥ [X]]]], A[νXB[A[X]]] (µ) µXA ⊥ [B ⊥ [X]], A[νXB[A[X]]] 2.1.3 Infinite proof trees: µMALL ∞ µMALL ∞ [Baelde,
Definition 16. The formulas of µMALL ∞ are the same as the formulas of µMALL, in the previous section.

Inference rules for µMALL ∞ . The proofs for µMALL ∞ will be defined as infinite, non well-founded proof trees. They are built out of a set of inference rules, which is given in the following definition.

Definition 17 (µMALL ∞ inference rules). The set of inference rules for µMALL ∞ is the union of the rules for MALL, given in Figure 2.1 and of the two rules given in Figures 2.4

and 2.5.

Preproofs for µMALL ∞ . Proofs for µMALL ∞ are selected among a set of preproofs, which are potentially infinite objects, defined by allowing ordinary proof trees (Definition 6) to be infinite.

Definition 18 (µMALL ∞ preproofs). A preproof for µMALL ∞ is any proof tree, finite or infinite, built with the inferences for µMALL ∞ given in Definition 17.

Example 5. Let F = µXνY (X `Y ) et G = νY µX(X `Y ).
The following are two µMALL ∞ preproofs.

π 1 = π 1 νXX, µX(X `G), µXX (ν) νXX, µX(X `G), µXX π 1 νXX, µX(X `G), µXX (ν) νXX, G, µXX (cut) νXX, µX(X `G), G, µXX (`) νXX, µX(X `G) `G, µXX (µ) νXX, µX(X `G), µXX
(2.1)

π 2 = π 2 νXX, νY (F `Y ), µXX (µ) νXX, F, µXX (ν) νXX, F, µXX π 2 νXX, νY (F `Y ), µXX (cut) νXX, F, νY (F `Y ), µXX (`) νXX, F `νY (F `Y ), µXX (ν) νXX, νY (F `Y ), µXX (2.2)
Remark 6 (Inconsistency of preproofs). Any µMALL sequent is the conclusion of a µMALL ∞ preproof. More precisely, for any sequent Γ, the following is a µMALL ∞ preproof:

. . .

Γ

Proofs and validity for µMALL ∞ The validity criterion used to distinguish proofs among preproofs will be given in Definition 35 and can be stated as: "every infinite branch must contain a valid thread". To make this formal, we will first define how a preproof induces two graphs and then define the "branches" and "threads" of a preproof as infinite paths in these graphs.

Definition 19 (thread of an infinite branch of a preproof). Given an infinite branch β of a preproof π, we define the set of threads of β as follows. A thread in β is a sequence (s n ) n∈N of positions of formulas in π such that:

• each s n belongs to a sequent of β

• ∀n ∈ N, s n is the immediate descendant of s n+1 in β, according to the threading functions of β.

The following lemma is the key to the notion of a valid thread, which is defined right after it. If s is a position of formula in a proof tree, we denote by fml(s) ∈ Fml the associated formula.

Definition 20. If t = (s n ) n∈N is an infinite thread in a preproof, we define inf(t) = {A ∈ Fml | ∀n 0 ∈ N, ∃n n 0 , s n is principal and fml(s n ) = A} i. e.
the set of formulas that are infinitely often principal in t.

Definition 21 (Valid thread). An infinite thread t is valid if inf(t) has a minimum, with respect to the subformula ordering, and this minimum is a ν-formula.

Definition 22 (proofs). We say that an infinite branch b of a preproof is valid if there is a valid infinite thread t on b.

A µMALL ∞ preproof is a proof if all its infinite branches are valid.

Finite proof trees with back edges: µMALL ω

The aim of µMALL ω is to have a system of finite proofs, as in µMALL, with only the rules of fixed point unfolding instead of a rule with an explicit invariant, as in µMALL ∞ .

As well as in µMALL ∞ , proofs of µMALL ω are selected among a set of preproofs.

Preproofs of µMALL ω are circular objects, defined by adding back edges to ordinary proof trees.

Definition 23 (µMALL ω formulas). The formulas of µMALL ω are the same as the formulas of µMALL and µMALL ∞ (Definition 13).

Definition 24 (Proof tree with open sequents). A proof tree with open sequents is a

proof tree in which it is not mandatory for a sequent to be the conclusion of a logical Definition 25 (lower, closer to the root). Whenever v, v are two vertices of a tree, we say that v is lower than v , or that v is below v , or that v is closer to the root than v when v appears on the path from v to the root.

The following definition aims at defining some representation for the fragment of all µMALL ∞ preproofs that are regular, that is those that have only a finite number of subtrees up to isomorphism. We will sometimes say simply preproof instead of b.e.-tree preproof, or circular preproof representation.

Example 6. Let π be the following proof tree, with three open sequents, and let us denote by s 0 , . . . , s 8 the positions of its sequents, as indicated:

s 4 : νX(X `X), µXX s 6 : νXX, νX(X `X), µXX (ν) s 5 : νXX, νX(X `X), µXX (cut) s 3 : νX(X `X), νX(X `X), µXX (`) s 2 : νX(X `X) `νX(X `X), µXX (ν) s 1 : νX(X `X), µXX s 8 : νXX (ν) s 7 : νXX (cut) s 0 : νX(X `X) then (π, {s 4 → s 1 , s 6 → s 5 , s 8 → s 7 }) is a µMALL ω b.e.
-tree preproof, that we will more simply denote by: νX(X `X), µXX νXX, νX(X `X), µXX

(ν) νXX, νX(X `X), µXX (cut) νX(X `X), νX(X `X), µXX (`) νX(X `X) `νX(X `X), µXX (ν) νX(X `X), µXX νXX (ν) νXX (cut) νX(X `X)
The validity criterion that will be used to distinguish µMALL ω proofs among preproofs is the same as in µMALL ∞ . We simply have to adapt the formalism to be able to talk about infinite branches and infinite threads of a finite circular representation. We will first define how a preproof induces two graphs and then define the "branches" and "threads" of a preproof as infinite paths in these graphs.

Definition 27 (Graph). In the following definitions, a "graph" always means a directed pseudograph, i. e. a directed graph which may have loops and in which there may be several edges between any pair of vertices. -tree preproof and G branch is its branch graph, we call an infinite branch of this preproof any infinite path in G branch starting from the root of π.

To clarify the following definitions, remember that in every proof tree π, for every inference I in π, every position of formula α in a premise of I has a unique immediate descendent in the conclusion of I, except if I is a cut and α is a cut formula, in which case α has no immediate descendent.

Example 7. The infinite branches of the preproof of Example 6 are s 0 (s 7 ) ω , s 0 (s 1 s 2 s 3 ) ω and all elements of {s 0 (s

1 s 2 s 3 ) k (s 5 ) ω | k ∈ N}.
Note that, in order to be totally rigorous, we should not only give the vertices of the paths but also the edges, i. e. when an inference has several premises, indicate explicitly which one was chosen. These details are omitted here for concision; they will cause no ambiguity on the validity of the preproof of Example 6.

νX(X `X), µXX νXX, νX(X `X), µXX (ν) νXX ι , νX(X `X) κ , µXX λ (cut) νX(X `X) ζ , νX(X `X) η , µXX θ (`) νX(X `X) `νX(X `X) δ , µXX (ν) νX(X `X) β , µXX γ νXX (ν) νXX ξ (cut) νX(X `X) α
The maximal threads of this preproof, that is those that cannot be extended in any direction, are (ξ) ω , γ θ(λ) ω , (ι) ω , α(βδζ) ω and the elements of {α(βδζ

) k βδη(κ) ω | k ∈ N}.
Once again, in order to be totally rigorous, we should explicitly include the explicit choice of a descendent relation, in cases where a position has several immediate ancestors.

U((ξ) ω ) = (s 7 ) ω U(γ θ(λ) ω ) = s 1 s 2 s 3 (s 5 ) ω U((ι) ω ) = (s 5 ) ω U(α(βδζ) ω ) = s 0 (s 1 s 2 s 3 ) ω ∀k ∈ N, U(α(βδζ) k βδη(κ) ω ) = s 0 (s 1 s 2 s 3 ) k+1 (s 5 ) ω
The definition of a valid thread is then the same as in µMALL ∞ : Example 10. Among the threads of Example 8:

Definition 33. If t = (s n ) n∈N is an infinite thread in a b.e.-
• (ξ) ω is valid: its smallest infinitely principal formula is νXX, which is principal at ξ;

• (ι) ω is valid: its smallest infinitely principal formula is νXX, which is principal at ι;

• α(βδζ) ω is valid: its smallest infinitely principal formula is νX(X `X), which is principal at β;

• γ θ(λ) ω is not valid: it has no principal formula;

• ∀k ∈ N, α(βδζ) k βδη(κ) ω is not valid: it has no principal formula after the last position of β.

Definition 35 (proofs). We say that an infinite branch b of a b.e.-tree preproof is valid if there is a valid infinite thread t of such that U(t) is a suffix of b.

A µMALL ω b.e.-tree preproof is a proof if all its infinite branches are valid.

We denote by Π(µMALL ω ) the set of all µMALL ω b.e.-tree proofs and we denote by Π(µMALL ω ) its complement in Π 0 (µMALL ω ), i. e. the set of all invalid b.e.-tree preproofs.

Example 11. The preproof of Example 6 is a proof:

• the branch s 0 (s 7 ) ω contains the valid thread (ξ) ω ;

• the branch s 0 (s 1 s 2 s 3 ) ω contains the valid thread (βδζ) ω ;

• ∀k ∈ N, the branch s 0 (s 1 s 2 s 3 ) k (s 5 ) ω contains the valid thread (ι) ω .

Link between circular representations and infinite preproofs

To every µMALL ω b.e.-tree preproof is associated a canonical µMALL ∞ preproof ∞ . The finite circular preproof may then be seen as a finite representation of the infinite preproof ∞ .

Without going into too much details, we give an explanation of how to define the transformation • ∞ . We first define a process F of expansion of a circular preproof.

Let be a circular preproof. We construct F ( ) as follows. We say that a back edge b is minimal in if the position of its target is minimal, meaning that no other back edge has a target strictly closer to the root of . For every minimal back edge b of , we substitute, in place of the source of b, the whole subtree of rooted at the target of b, including its back edges. This gives us F ( ). Remark that the proof tree of is a strict prefix of the proof tree of F ( ) and that the greatest prefix of without any target of back edge is, again, strictly smaller than the greatest prefix of F ( ) without any target of back edge. Said differently: the lowest target of back edges in F ( ) are strictly higher than in . By iterating F on we then obtain a strictly increasing sequence of circular preproofs, in which back edges targets are higher and higher and in which the prefix of the proof tree which is free of all back edge targets is increasing. ∞ is defined as the limit of those prefixes: ∞ = lim n→∞ F n ( ), in a sense that can be made formal.

Example 12. Let us denote A = µXνY (X ⊗ Y ) and consider the following circular preproof:

= A νY (A ⊗ Y ) (⊗) A ⊗ νY (A ⊗ Y ) (ν) νY (A ⊗ Y ) (µ)
A then its first step of unfolding is

F ( ) = A νY (A ⊗ Y ) (⊗) A ⊗ νY (A ⊗ Y ) (ν) νY (A ⊗ Y ) (µ) A νY (A ⊗ Y ) (⊗) A ⊗ νY (A ⊗ Y ) (ν) νY (A ⊗ Y ) (µ)
A

A second unfolding gives

F 2 ( ) = A νY (A ⊗ Y ) (⊗) A ⊗ νY (A ⊗ Y ) (ν) νY (A ⊗ Y ) (µ) A A νY (A ⊗ Y ) (⊗) A ⊗ νY (A ⊗ Y ) (ν) νY (A ⊗ Y ) (µ) A νY (A ⊗ Y ) (⊗) A ⊗ νY (A ⊗ Y ) (ν) νY (A ⊗ Y ) (⊗) A ⊗ νY (A ⊗ Y ) (ν) νY (A ⊗ Y ) (µ)
A and, at the limit, we get the infinite preproof ∞ which is such that

∞ = • • • • π νY (A ⊗ Y ) (µ) A with π = • • • • ∞ A • • • • π νY (A ⊗ Y ) (⊗) A ⊗ νY (A ⊗ Y ) (ν) νY (A ⊗ Y )
The principal remark that can be made about this unfolding is that F ( ), as a µMALL ∞ preproof, has the same branches as as a µMALL ω preproof. And each branch of F ( ) has the same threads as the corresponding branch of . Hence, F ( ) is valid as a µMALL ∞ preproof iff. is valid as a µMALL ω preproof. Or:

F ( ) is a µMALL ∞ proof iff.
is a µMALL ω proof. This is no coincidence and that remark is the origin of our formulation of the thread criterion for finite, circular representations.

The second natural remark is that this induces an equivalence on circular preproofs: and can be seen as representing the same infinite preproof when F ( ) = F ( ). By the previous remark, this equivalence relation is compatible with thread-validity.

Inner threads

Definition 36 (G νX(X `X), µXX νXX, νX(X `X), µXX

(ν) νXX ψ , νX(X `X) χ , µXX (cut) νX(X `X) τ , νX(X `X) υ , µXX (`) νX(X `X) ρ `νX(X `X) σ , µXX (ν) νX(X `X) π , µXX νXX (ν) νXX ψ (cut) νX(X `X) o
The maximal inner threads of this preproof are (ψ) ω , (ψ) ω , o(πρτ ) ω and the elements of

{o(πρτ ) k πσυ(χ) ω | k ∈ N}.
out((ψ) ω ) = (µ) ω out((ψ) ω ) = (ι) ω out(o(πρτ ) ω ) = α(βδζ) ω ∀k ∈ N, out(o(πρτ ) k πσυ(χ) ω ) = α(βδζ) k βδη(κ) ω
Definition 39 (Valid inner thread). An infinite inner thread t = (s n ) n∈N is valid if

∀n 0 ∈ N, ∃n n 0 , s n is principal.
Example 15. Among the inner threads of Example 13:

• (ψ) ω is valid: ψ is principal;

• (ψ) ω is valid: ψ is principal;

• o(πρτ ) ω is valid: π is principal;

• ∀k ∈ N, o(πρτ ) k πσυ(χ) ω is not valid: χ is not principal and it has no principal vertex after the last π.

Proposition 5 (Equivalence between the two definitions of valid infinite threads).

1. If t is a valid infinite inner thread then out(t) is a valid infinite thread.

2. If u is a valid infinite thread then there is a unique valid infinite inner thread t such that u = out(t).

Proof. • the branch s 0 (s 7 ) ω contains the valid inner thread (ψ) ω ;

t
• the branch s 0 (s 1 s 2 s 3 ) ω contains the valid inner thread (πρτ ) ω ;

• ∀k ∈ N, the branch s 0 (s 1 s 2 s 3 ) k (s 5 ) ω contains the valid inner thread (ψ) ω .

Much in the spirit of these inner threads, we can generalize Definitions 10 and 11 to the -tree preproof, if u = (s 0 , . . . , s n ) is a path in its G branch and p is a position of subformula in the sequent at position s n , then:

• T(u)(p) is the unique path p i 0 , . . . , p n such that -∀i, p i is a position of subformula in the sequent at position s i , -p n = p, -∀i, i 0 i < n ⇒ the formula containing p i in the sequent at position s i is the immediate descendant of the formula containing p i+1 in the sequent at position s i+1 , and p i is the image of p i+1 in that formula,

-either i 0 = 0 or p i 0 is in a cut formula, • t(u)(p) =    p 0 if i 0 = 0 undefined if i 0 > 0
In this last case, p i 0 is in a cut formula.

Remark 7. If, in the previous definition, the subformula at position p is a ν-formula, then

T(u)(p) is a path in G in thread .

Complexity theory

Generalities on complexity and PSPACE

We give here a brief and somewhat informal recall of the essential notions of algorithmic complexity that we will need in the thesis. For an in-depth perspective on that subject, see, for instance, [START_REF] Arora | Computational Complexity -A Modern Approach[END_REF]. If you understand French, you may also read the excellent book by [START_REF] Perifel | Complexité algorithmique[END_REF].

In particular we do not go here into the choice and definition of a precise model of computation. All programs are considered deterministic. We assume that the inputs and outputs of programs contain at least {0, 1} * , the finite words on {0, 1}, and that there is a pairing operation which allows to combine two entries x and y into a single one (x, y).

Definition 41 (Notations). If f is a program and x an entry for this program, we denote by x the size of the entry x, we denote by time(f, x) the execution time of f on x, which may be an integer or +∞, and we denote by space(f, x) the memory space used by the execution of f on x, which may be an integer or +∞.

Definition 42 (Problem, language). A problem or language is any subset of all possible program entries.

Definition 43.

• if t : N → N is a function, a language L is in DTIME(t(n)) if there is a program f such that -∀x ∈ L, f (x) = 1 -∀x / ∈ L, f (x) = 0 -∃α > 0, ∀x, time(f, x) α • t( x ) • if t : N → N is a function, a language L is in DSPACE(t(n)) if there is a program f such that -∀x ∈ L, f (x) = 1 -∀x / ∈ L, f (x) = 0 -∃α > 0, ∀x, space(f, x) α • t( x )
Definition 44.

• P := k∈N DTIME n k • EXP := k∈N DTIME 2 n k • PSPACE := k∈N DSPACE n k • NP := {A | ∃p polynomial, ∃B ∈ P, ∀x, (x ∈ A ⇔ ∃y ∈ {0, 1} p( x ) , (x, y) ∈ B)} Proposition 6. P ⊆ NP ⊆ PSPACE ⊆ EXP
The strictness of each one of these inclusions is an open problem. Experts of the domain seem to believe that all these inclusions are in fact strict. We still know for sure that not all of them can be equalities, as a consequence of Corollary 1 to Theorem 2 below.

Definition 45. A function t : N → N is time-constructible if there is a program f such that • ∀n ∈ N, f (1 n ) = 1 t(n)
(where 1 n is the word of length n made only of 1)

• ∃α > 0, ∀n ∈ N, time(f, 1 n ) α • t(n) Theorem 2 (Deterministic time hierarchy). If f, g : N → N are two functions such that • ∀n ∈ N, f (n) > 0 • g is time-constructible • g(n) f (n) • log(f (n)) then DTIME(f (n)) DTIME(g(n)).
Corollary

• A problem A is in PSPACE iff. its complement A is in PSPACE. • A problem A is PSPACE-complete iff. its complement A is PSPACE-complete.
Proof.

• Every DSPACE(n k ) is closed under complement: if f recognizes A, A is recognized by g(x) = 1 -f (x).
Hence PSPACE is closed under complement.

• Suppose A is PSPACE-complete and B is PSPACE. We then show that B reduces to

A. As B is PSPACE, so is B.
Hence there is a polynomial-time many-one reduction

f from B to A. Then we show that f is also a reduction from B to A. Indeed, ∀x, x / ∈ B ⇔ x ∈ B ⇔ f (x) ∈ A, and then ∀x, x ∈ B ⇔ f (x) / ∈ A ⇔ f (x) ∈ A.
Remark 8. Although this will not be used in this thesis, we recall to the interested reader that we also have PSPACE = NPSPACE = coNPSPACE because of Savitch theorem. Proof. We reduce from the problem of termination for a more expressive language, which has been defined and proved PSPACE-complete by Jones in [START_REF] Neil | Computability and complexity -from a programming perspective[END_REF], under the name of BOOLE.

Parity automata

We recall here the basic definitions and property of parity automata. There are several definitions of parity automata, all of which are equivalent. We chose a definition that best suits our needs. For more informations on the subject of automata for infinite words, see, for instance, [START_REF] Grädel | Automata, Logics, and Infinite Games: A Guide to Current Research [outcome of a Dagstuhl seminar[END_REF] or [START_REF] Perrin | Infinite words: automata, semigroups, logic and games[END_REF].

We denote by ω the set of natural integers, and we also denote by ω the first infinite ordinal. We denote by ω + 1 the set ω ∪ {ω}, ordered by setting ω to be its maximum.

Parity automata

The ordinal ω is considered even. All of that is consistent with usual set-theoretic conventions.

Given an alphabet A, we denote by A ω the set of infinite words on A, that is the set of sequences of elements of A, indexed by the integers.

Definition 49 (Parity automaton). Given an alphabet A, a parity automaton on A consists of

• a set Q of states;

• a subset I ⊆ Q of initial states;

• a set T ⊆ Q × A × (ω + 1) × Q.
Such a parity automaton is finite if A, Q and T are finite. In T , elements of ω + 1 are called priorities.

Definition 50. A run, or path, in a parity automaton A is any infinite sequence q 0 q 1 q 2 q 3 . . .

a 0 p 0 a 1 p 1 a 2 p 2 such that • q 0 ∈ I • ∀n ∈ ω, (q n , a n , p n , q n+1 ) ∈ T
If r is such a run, we denote by label(r) the infinite word a 0 a 1 a 3

• • • ∈ A ω .
Definition 51. Such a run r is successful in the parity automaton if there is a p ∈ ω + 1 such that

• p is odd (which implies p = ω)

• there are only finitely many n ∈ ω such that p n < p

• there are infinitely many n ∈ ω such that p n = p Equivalently : p is an odd priority and it is the smallest priority appering infinitely often in the run r.

Definition 52 (Language of a parity automaton). The language of a parity automaton

A is the set L(A) := {label(p) | p is a successful run in A}.
And the main theorem that we will use is the following.

Theorem 3. The problem of equality of languages for finite parity automata is decidable in polynomial space.

Proof. We do not go into the details of this complex result. It relies on the fact that every parity automaton can be translated into an equivalent Bűchi automaton with a polynomial increase of size, which is folklore, and on the the fact that the problem of equality of languages for Bűchi automata is decidable in polynomial space, which was proven by [START_REF] Sistla | The complementation problem for büchi automata with appplications to temporal logic[END_REF].

PSPACE-completeness of the thread criterion

As we explained in the introduction, the subject of this thesis is the study of finite circular representations of infinite proofs and preproofs. In this context, the first question arising is to distinguish, among circular representations of preproofs, those denoting valid preproofs, i. e. proofs, from those denoting invalid preproofs.

It has already been shown by Doumane [2017b] that this problem is decidable in PSPACE.

In the first section of this chapter, we recall a proof of this result.

The second section of this chapter is devoted to its main result: that the problem We show in Section 3.2.4 how our method adapts to other systems such as µLJ and µLK.

Deciding thread validity in PSPACE

In this section, we recall that the problem of deciding whether the circular representation of a preproof is a valid proof is in PSPACE. Several algorithms can be used for deciding this problem in PSPACE. Here we reduce this problem to the problem of deciding equality of languages for parity ω-automata, which is known to be in PSPACE. See Section 2.3 of the technical background for more details on that. More precisely, given a preproof , we define two parity automata: the language of the first one is the set of infinite branches of and the language of the second one is the set of valid infinite branches of .

We will immediately give two examples to show how the algorithm works.

Let G := νY µX(X `Y ). The following preproof (3.1) is valid. The branches that ultimately always take the left back edge are valid because of a thread going through νXX and the branches that take infinitely often the right back edge are valid because of a thread going through µX(X `G) and G.

νXX, µX(X `G), µXX

(ν) νXX, µX(X `G), µXX νXX, µX(X `G), µXX (ν)
νXX, G, µXX

(cut) νXX, µX(X `G), G, µXX (`) νXX, µX(X `G) `G, µXX (µ) νXX, µX(X `G), µXX (3.1)
From this preproof, we build a first automaton, represented on Figure 3.1 p. 74, which recognizes the language of infinite branches of the preproof. It has one initial state and all paths are accepted. It recognizes the language (abcd + abef ) ω .

And from the same preproof (3.1) we build a second automaton, represented on Figure 3.2, p. 75, which recognizes the language of valid infinite branches of the preproof (3.1). No priority indicated on an edge implicitely means ω, which is the highest non-accepting priority. There are four initial states, at the bottom of the automaton. Three edges have a priority < ω νXX νXX

d 1 G µX(X `G) f 1 µX(X `G) µX(X `G) `G a 2
It recognizes the language (abcd + abef ) * (abcd) ω + ((abcd) * abef ) ω = (abcd + abef ) ω Now let F := µXνY (X `Y ). The following preproof (3.2), unlike the preproof (3.1), is not valid. The branches taking ultimately only the left back edge are valid because of a thread going through νXX, the branches taking ultimately only the right back edge are valid because of a thread going through νY (F `Y ) but the branches which takes infinitely often the left back edge and infinitely often the right back edge are not valid.

νXX, νY (F `Y ), µXX (µ) νXX, F, µXX (ν) νXX, F, µXX νXX, νY (F `Y ), µXX (cut) νXX, F, νY (F `Y ), µXX (`) νXX, F `νY (F `Y ), µXX (ν) νXX, νY (F `Y ), µXX (3.2)
The deduced automaton recognizing all infinite branches of preproof (3.

νY (F `Y ) F `νY (F `Y ) a 3 νXX νXX d 1 F νY (F `Y ) e 2
It recognizes the language (abcde + abf ) * (abcde) ω + (abcde + abf ) * (abf ) ω = (abcde + abf ) ω \ ((abf ) * abcde(abcde) * abf ) ω

We will now explain the procedure by which, in each case, those two automata were obtained.

Let be a b.e.-tree preproof. Let G branch be its branch graph, as defined in Definition 28.

Let A := E branch be the set of its edges. This will be the input alphabet of our automata.

The first ω-automaton is A branch := (Q branch , I branch , T branch ), where:

• The set of states is Q branch := V branch , the set of vertices of G branch , that is the set of closed positions of sequents in π.

• The set of initial states is the singleton I branch := {i branch }, where i branch is the position of the root of , that is the position of the conclusion sequent of .

• The set of transitions is

T branch := { s s e 1
| e is an edge from s to s in G branch }

This amounts to saying that the accepted paths in A branch are exactly the paths in G branch which start at the root of the proof tree. With that definition, the following lemma is immediate:

Lemma 3. The language L(A branch ) is the set of infinite branches of .

For our second automaton, we need a priority assignment Ω : Fml → ω. It will be used to reflect the condition of validity of threads in the parity condition of our automata. We need this priority assignment to have two main properties:

1. if A is a subformula of B then Ω(A) Ω(B);

2. ∀A, Ω(µXA) is even and Ω(νXA) is odd.

Remember that even priorities are rejecting and odd priorites are accepting (Definition 51).

Thus, those two properties reflect the condition of Definition 34.

Definition 53 (Ω : Fml → ω). A function Ω is defined by induction, which associate a priority to every preformula:

Ω(νXA) :=    Ω(A) if Ω(A) is odd Ω(A) + 1 if Ω(A) is even Ω(µXA) :=    Ω(A) if Ω(A) is even Ω(A) + 1 if Ω(A) is odd Ω(A B) := max{Ω(A), Ω(B)}
for any binary connective Ω(c) := 0 for any propositional constant c Ω(X) := 0

The following remarks are immediate: Lemma 4. For all formulas A and B:

• Ω(νXA) is odd and Ω(µXA) is even.

• If A is a subformula of B then Ω(A) Ω(B).

Our second automaton is a parity ω-automaton, with priorities in ω + 1 = ω ∪ {ω}, ω being even.1 This second automaton is defined as A thread = (Q thread , I thread , T thread ), where:

• the set of states is • the set of transitions is

Q thread := V thread + {⊥ s | s ∈ V branch }, i.
T thread := {⊥ s e -→ ω ⊥ s | e is an edge from s to s in G branch } ∪ { α β U(e) Ω(α)
| e is an edge from α to β in G out thread and α is principal}

∪ { α β U(e) ω
| e is an edge from α to β in G out thread and α is not principal}

∪ {⊥ s e -→ ω α | I is a (cut) inference in ,
s is the position of the conclusion sequent of I, s is the position of a premise of I, e is an edge induced by I in G branch from s to s and α is the position of the corresponding cut-formula in s }

where q e -→ i q denote a transition from state q ∈ Q thread to state q ∈ Q thread with label e ∈ A and priority i ∈ ω + 1.

The acceptance condition is the one given in our definition of parity automata in Definition 49: a run is accepted if the smallest priority appearing infinitely often is odd (ω being even).

Once again, it should be clear from Definitions 21 and 22 that:

• E = {0 0 → 1} ∪ { → (( + 1) mod (m + 1)) | I = "X := not X"} ∪ { + → , - → | I = "if X goto else "}
The following definition is the main object of this chapter. It describes a transformation that turns every boolean program b into a µMALL ω b.e.-tree-preproof, with the property that this preproof is thread-valid iff. the source program is non-terminating.

Definition 55 ( • : BOOLE false → Π 0 (µMALL ω )). For every boolean program b ∈ BOOLE false , we define a preproof b ∈ Π 0 (µMALL ω ). Let X 1 , . . . , X k be the variables of b and 1 : I 1 , . . . , m : I m its instructions. We first give names to the formulas that will appear in b : we define a unary operation ¿, three formulas A, B, C, a family of unary operations (¿ n ) and two families of formulas (D n ), (E n ):

A = ¿(νX¿X) B = νX(⊥ ⊕ X) C = µX(B `X) E n = ¿ n (νX¿ n X) ¿F = µX(F ⊕ (⊥ ⊕ (X `X))) ¿ n F = µX(⊥ ⊕ (X `(F `• • • `F n-1
)))

D n = µX(X & • • • & X n )
We now define b to be the preproof

• • • • 0: A 2k , B, C, D 2 , D m , E m m • • • • 1 : I 1 A 2k , B, C, D 2 , D m , E m m . . . • • • • m : I m A 2k , B, C, D 2 , D m , E m m (µ), (&) m-1 (Root) A 2k , B, C, D 2 , D m , E m m (3.3)
where A 2k is an abbreviation for A, . . . , A . We do so, for instance, on Note however that an infinite word u ∈ E ω has no reason a priori to be a path in G.

From now on, we will refer directly to infinite branches of the preproof by words u ∈ E ω .

Main theorem

We now prove that Π(µMALL ω ) is PSPACE-complete.

Remark 13 (Thread groups). We need to be more precise about the occurrences of formulas in the conclusion sequent of preproof b :

A, . . . , A 2k , B, C, D 2 , D m , E m , . . . , E m m
Let us label the occurrences of A in this sequent as follows:

A + 1 , A - 1 , . . . , A + k , A - k , B, C, D 2 , D m , E m , . . . , E m m
so that we can talk precisely about them. It can be seen by examining the definition of • (def. 55) that a valid thread in the preproof cannot pass through D 2 or D m , which contain no ν, and that the remaining formulas are divided into k + 2 groups

A + 1 , A - 1 , . . . , A + k , A - k , B, C , E m , . . . , E m
which cannot thread-interact with each other, in the sense that, for instance, no thread can contain a B and a E m , or a A and a A if = .

Lemma 6. An infinite branch u ∈ E ω in the preproof contains a validating thread

• in the E m group iff. no suffix of u is a valid path in G.

• in the B, C group iff. 0 occurs only finitely in u.

Proof. The proof goes by case on the instructions involved.

In order to prove the first part of the statement, that is that an infinite branch u ∈ E ω in the preproof contains a validating thread in the E m group iff. no suffix of u is a valid path in G, we reason by case on the instructions involved and remark that the E m formulas are touched only in the :goto parts of the preproof.

The E m formulas are touched only in the :goto parts of the preproof. Observe that in :goto all E m but one are erased, after which the remaining E m recreates all of them. As a consequence, every infinite branch u ∈ E ω in the preproof has exactly one thread in the E m group. Suppose a factor e 1 e 2 ∈ E 2 of u and suppose their respective sources and targets in G to be named 1 e 1 -→ 1 and 2 e 2 -→ 2 . The crucial observation is that the piece of the E m thread delimited by e 1 has minimal formula equal to

   E m (which is a µ-formula) if 1 = 2 νX¿ m X if 1 = 2
the formula νX¿ m X being a subformula of E m able to recreate E m . As a result:

• if u has a suffix which is a valid path in G then the principal formula of the E m thread is E m , hence this thread is a µ-thread, and there is no valid thread in the E m group.

• otherwise, the principal formula of the E m thread is νX¿ m X, and this thread is a ν-thread, infinitely progressing, hence a validating thread.

This diagram sums up the behavior of the threads of the E m group in :goto :

E (1) m • • • E ( -1) m E ( ) m E ( +1) m • • • E (m) m E (1) m • • • E ( -1) m E ( ) m E ( +1) m • • • E (m) m νX¿ m X νX¿ m X Em νX¿ m X νX¿ m X
In order to prove the second part of the statement, that is that an infinite branch u ∈ E ω in the preproof contains a validating thread in the B, C group iff. 0 occurs only finitely in u, we reason by case on the instructions involved.

First note that B is a ν-formula and that it is a subformula of C, which is a µ-formula.

Observe also that B can recreate B, but B cannot recreate C. Therefore a {B, C}-thread, in order to be validating, must end with an infinite alternation

B (ν) -→ (⊥ ⊕ B) (⊕ 1 ) -→ B (ν) -→ • • • Let
+ i , A - i } in 0 0u -→ + are A + i A - i A + i A - i νX¿X A 64 3.2 PSPACE-completeness if X i =

false at the end of u and

A + i A - i A + i A - i A νX¿X
if X i = true at the end of u; and if u is not a prefix of the execution of b then there is an i ∈ 1, m such that the threads of

{A + i , A - i } in 0 0u -→ + are A + i A - i A + i A - i νX¿X νX¿X
Proof. The proof goes by induction on the length of u.

1

If u has length 0, 0u = 0. It corresponds to having done 0 step of the execution of b, which implies that all variables have value false, and the threads of

{A + i , A - i } in p 0 are indeed A + i A - i A + i A - i νX¿X A
for all i. If u has length > 0, it decomposes as u = ve with e ∈ E \ {0}. There are then three cases : either ve is the beginning of the execution of b, or v is but ve is not, or v is already not the beginning of the execution of b. In the third case, by induction hypothesis, there is an i such that the threads of {A + i , A - i } in 0v are

A + i A - i A + i A - i νX¿X νX¿X
and, because e = 0, the threads of {A + i , A - i } in e are of one of the four following forms:

A + i A - i A + i A - i A + i A - i A + i A - i A + i A - i A + i A - i νX¿X A + i A - i A + i A - i νX¿X 65
3 PSPACE-completeness of the thread criterion hence, by composition, the threads of {A + i , A - i } in 0ve = 0u are still

A + i A - i A + i A - i νX¿X νX¿X
Otherwise v is a beginning of the execution of b. Then, by induction hypothesis, the threads of

{A + i , A - i } in 0 0v -→ + are A + i A - i A + i A - i νX¿X A
if X i = false at the end of v and

A + i A - i A + i A - i A νX¿X if X i = true at the end of v. The next instruction executed by b is either I :X i := not X i or I :if X i goto else .
If the next instruction is I :X i := not X i then e has to be → (( + 1) mod (m + 1)), so 0u = 0ve is still a beginning of the execution of b, and then: for every j = i, the threads of {A + j , A - j } in e are

A + i A - i A + i A -
i so the threads of {A + j , A - j } in 0u have the same form as those in 0v, while the value of X j has not changed, hence the invariant is still respected for j. As for the threads in

{A + i , A - i }, in e they are A + i A - i A + i A - i so if the threads of {A + i , A - i } in 0v are A + i A - i A + i A - i νX¿X A 66 3.2 PSPACE-completeness those in 0u are A + i A - i A + i A - i A νX¿X
and vice versa. As the value of X i is changed by this instruction, the invariant is still respected also for i. The last case we have to treat is when the next instruction executed by b after v is I :if X i goto else . That means that v ends in vertex , from which there are two edges: + → and -→ . There are four cases, depending on the value of the variable X i after v, and the choice of e ∈ { + , -}. If X i = false and e = l - then 0u = 0ve is still a prefix of the execution of b. The threads of {A + i , A - i } in 0v where, by induction hypothesis:

A + i A - i A + i A - i νX¿X A
and those in e = l -are

A + i A - i A + i A - i νX¿X
hence, by composition, the threads of {A + i , A - i } in 0u are still

A + i A - i A + i A - i νX¿X A
and the invariant is still respected. The situation is symmetric when X i = true and e = l + . If X i = true and e = l -then 0u = 0ve is not a prefix of the execution of b. The threads of {A + i , A - i } in 0v where, by induction hypothesis:

A + i A - i A + i A - i A νX¿X
and those in e = l -are

A + i A - i A + i A - i νX¿X 67
3 PSPACE-completeness of the thread criterion hence, by composition, the threads of {A + i , A - i } in 0u are

A + i A - i A + i A - i νX¿X νX¿X
(recall that νX¿X is a subformula of A). The situation is symmetric when X i = false and e = l + . So in all of these four cases the invariant is respected.

Proposition 10. • is a LOGSPACE reduction from Π(µMALL ω ) to B false .
Proof. For the LOGSPACE character: the only data that need to be remembered while constructing the preproof are integers like k, m, , . Because , m and the entry has size Ω(k + m), this takes a space at most logarithmic in the size of the entry.

As for the fact that it is indeed a reduction: let us assume a b ∈ BOOLE false and prove

that b / ∈ Π(µMALL ω ) ⇔ b ∈ B false . Let G = (V, E)
let P 1 = {vw ∞ | v ∈ E * , w ∞ ∈ E ω and w ∞ is a path in G} and P 2 = {v ∞ ∈ P 1 | 0 occurs infinitely in v ∞ }.
By construction, P 2 ⊆ P 1 ⊆ E ω . We will prove three facts:

that every branch v ∞ ∈ E ω \ P 1 is thread-valid, that every branch v ∞ ∈ P 1 \ P 2 is thread-valid and that every branch v ∞ ∈ P 2 is thread-valid. These three facts, together with the fact that (E ω \ P 1 ) ∪ (P 1 \ P 2 ) ∪ P 2 = E ω , are enough to conclude that every branch v ∞ ∈ E ω is thread-valid. The first fact, that every branch v ∞ ∈ E ω \ P 1 is thread-valid, is due to the thread going through the E m . The second fact, that every branch v ∞ ∈ P 1 \ P 2 is thread-valid, is due to the thread going through B. The third fact, that every branch v ∞ ∈ P 2 is thread-valid, is due to the fact that b is non-terminating and that, because of that, one of the 2k threads going through the A is valid.

Theorem 4. The problem Π(µMALL ω ) is PSPACE-hard: PSPACE Π(µMALL ω )
Proof. We reduce from B false , which is PSPACE-complete by Lemma 2. More precisely, we reduce B false to Π(µMALL ω ), the complement of Π(µMALL ω ). This is enough because PSPACE is closed under complements, in the same way as all deterministic classes. The reduction • : BOOLE false → Π 0 (µMALL ω ) is defined in Definition 55. It is a LOGSPACE reduction, by Proposition 10, hence it is also a polynomial-time reduction.

Remark 15. In fact, since our construction do not use the (cut) rule, the cut-free fragment of Π(µMALL ω ) is already PSPACE-hard.

Generalisation to other systems

Systems of circular proofs with least and greatest fixed points can and have been built for other logics, either with different connectives (LK, LJ) or with added modalities (LK , LK ♦). Such systems, which can also be seen as variants of µ-calculus, are described in [START_REF] Vardi | A temporal fixpoint calculus[END_REF], Kaivola, 1995a[START_REF] Dax | A proof system for the linear time µcalculus[END_REF][START_REF] Doumane | Towards completeness via proof search in the linear time µ-calculus: The case of büchi inclusions[END_REF], Doumane, 2017a,b]. They all share the fact that MALL can be seen as a fragment of them, and therefore it is easy to translate µMALL ω proofs into them and transfer to them our result of PSPACE-completeness:

Remark 16. There is a µLJ defined by [START_REF] Clairambault | Least and greatest fixpoints in game semantics[END_REF][START_REF] Clairambault | Logique et Interaction : une Étude Sémantique de la Totalité[END_REF], which is a finitary calculus in the spirit of µMALL, with explicit invariants of induction and coinduction.

The µLJ ω we are considering here is an infinitary one, in which proofs are distinguished from invalid preproofs by a thread criterion, in the spirit of µMALL ω .

Corollary 2 (to Theorem 4). The decidability of the thread criterion is also PSPACEcomplete in µLJ ω , µLK ω , µLK ω and µLK ♦ ω .

Proof. It is true for µLJ ω because every preproof π in µMALL ω can be translated to a preproof π * in µLJ ω , such that π * is thread-valid iff. π is, by translating MALL connectives into LJ connectives and translating Γ into |Γ ⊥ | ⊥.

It is true for the other mentionned systems because µLJ ω is a fragment of them, therefore every µLJ ω preproof is already a preproof in each of them.

Details of how the constructions adapt to LK and LJ are given below.

Remark 17. Note that the following adaptations from MALL to LK and LJ might be simplified by replacing F ∨ F by F , X ∧ X by X, ⊥ ∨ X by X and so on. A lot of the complexity of these formulas is there to simulate structural rules in the linear world. When we are in the classical world, these workaround may not be needed anymore. Anyway, the translation we present here is simply to show that even without thinking about that, a straightforward translation is possible, which gives the same PSPACE-completeness result with LK and LJ and their extensions.

Generalisation to µLK, µLK and µLK

♦ A = ¿(νX¿X) B = νX(⊥ ∨ X) C = µX(B ∨ X) E n = ¿ n (νX¿ n X) ¿F = µX(F ∨ (⊥ ∨ (X ∨ X))) ¿ n F = µX(⊥ ∨ (X ∨ (F ∨ • • • ∨ F n-1
)))

D n = µX(X ∧ • • • ∧ X n )
We define b to be the preproof

• • • • 0: A 2k , B, C, D 2 , D m , E m m • • • • 1 : I 1 A 2k , B, C, D 2 , D m , E m m . . . • • • • m : I m A 2k , B, C, D 2 , D m , E m m (µ), (∧) m-1 (Root) A 2k , B, C, D 2 , D m , E m m (3.4)
See the details of all branches on Figures 3.7 and 3.8.

Generalisation to µLJ

A = ¡(µX¡X) B = µX( ∧ X) C = νX(B ∧ X) E n = ¡ n (µX¡ n X) ¡F = νX(F ∧ ( ∧ (X ∧ X))) ¡ n F = νX( ∧ (X ∧ (F ∧ • • • ∧ F n-1
)))

D n = νX(X ∨ • • • ∨ X n )
We define b to be the preproof

• • • • 0: A 2k , B, C, D 2 , D m , E m m • • • • 1 : I 1 A 2k , B, C, D 2 , D m , E m m . . . • • • • m : I m A 2k , B, C, D 2 , D m , E m m (ν L ), (∨ L ) m-1 (Root)A 2k , B, C, D 2 , D m , E m m (3.5)
See the details of all branches on Figures 3.9 and 3.10.

Comments on our approach and discussion of related works

Remark 18. The interested open question is: does the result still stand in the guarded fragments of µLK ω and µLK ♦ ω ? We conjecture that it does and that the method we illustrate here on µMALL can apply as well to the guarded cases of µ-calculi with modalities.

Comments on our approach and discussion of related works

Our proof for the PSPACE-completeness of the thread criterion is an encoding and an adaptation to our setting of the proof used by Lee, Jones and Ben Amram to prove that size-change termination is PSPACE-complete [Lee, Jones, and Ben-Amram, 2001].

We reduce, as they do, from the problem of termination of boolean programs and the -tree-shaped preproofs. Furthermore, we could not have filled this gap by simply unfolding the graph into a tree with back edges, for it could lead, as shown in the following example, to an exponential blow-up in size, which would prevent the reduction to be LOGSPACE, or even P. The following boolean program:

1:if X then goto 2 else goto 2 2:if X then goto 3 else goto 3 . . . n:if X then goto n + 1 else goto n + 1 will be translated to a graph-shaped preproof of size Θ(n) but the unfolding of this preproof into a b.e.-tree-shaped preproof will have size Θ(2 n ). Therefore we had to be clever in order to target trees with back edges by simulating several vertices with a single one; this is accomplished by the E m and :goto .

This improvement of the reduction of Lee, Jones and Ben Amram could in fact be adapted in the other direction, to show that size-change termination is already PSPACE-complete even when restricted to programs with only one function (in the terminology of [START_REF] Chin | The size-change principle for program termination[END_REF]), that is when the corresponding call graph / control flow graph has only one vertex.

If, as it is commonly believed, NP = PSPACE, our result implies that there is no way to add a polynomial quantity of information to a preproof so that its thread-validity can be checked in polynomial time. This can be seen as a problem, both for the complexity of proof search and proof verification. It suggests trying to find restrictions of the thread criterion which will be either decidable or certifiable in polynomial time, while keeping enough expressivity to validate interesting proofs. This will be the subject of the Chapters 4 and 5 of this thesis.

We recalled in section 3.1 that thread validity is decidable in PSPACE, and we did so by reducing to the problem of language inclusion for ω-parity-automata. The original sizechange article [START_REF] Chin | The size-change principle for program termination[END_REF] gives two different methods to check size-change termination, the first one is based on reducing to inclusions of ω-languages defined by finite automata while the second one is a direct, graph-based approach. It is in fact possible to use this more direct method to decide the thread criterion, and this has already been done by [START_REF] Dax | A proof system for the linear time µcalculus[END_REF], who remark furthermore that this method leads to a more efficient implementation than the automata-based one.

Conclusion

In the present chapter, we analyzed the complexity of deciding the validity of circular proofs in µMALL logic: while the problem was already known to be in PSPACE, we established here its PSPACE-completeness. In doing so, we drew inspiration from the PSPACE-completeness proof of SCT even though we defer at some crucial points on order to build our reduction and carry our proof taking into account the specific forms of circular proofs.

Our proof adapt straightforwardly to a number of other circular proof systems based on sequent calculus such as intutionnistic or classical proof systems in addition to the linear case on which we focused here.

While our result can be seen as negative one for circular proofs, it does not prevent actual implementations to be tractable and usable on many situations as examplified by :goto := Back edge to (Root)

νXX, µX(X `G), µXX νXX, G, µXX νXX, µX(X `G), G, µXX νXX, µX(X `G) `G,
νXX µX(X `G) ⊥ µXX νXX ⊥ G µXX νXX µX(X `G) ⊥ G µXX νXX µX(X `G) `G ⊥ µXX νXX µX(X `G) ⊥ µXX
νXX F ⊥ µXX νXX F ⊥ µXX νXX F ⊥ νY (F `Y ) µXX νXX ⊥ F `νY (F `Y ) µXX νXX ⊥ νY (F `Y )
A, . . . , A, B, C, D 2 , D m , E m , . . . , E m (ν) m-1 A, . . . , A, B, C, D 2 , D m , νX¿ m X, . . . , νX¿ m X -1 , E m , νX¿ m X, . . . , νX¿ m X m- (µ), (⊕ 1 ), (`) m-1 A, . . . , A, B, C, D 2 , D m , E m ((µ), (⊕ 0 ), (⊥)) m-1 A, . . . , A 2k , B, C, D 2 , D m , E m , . . . , E m -1 , E m , E m , . . . , E m m- Figure 3.5. Back edges of the preproof 0: := • • • • 0:goto 1 (A, A) k , B, C, D 2 , D m , E m m (ν) k (νX¿X, A) k , B, C, D 2 , D m , E m m ((µ), (⊕ 0 )) k (A, A) k , B, C, D 2 , D m , E m m ((µ), (⊕ 1 ), (⊕ 1 ), (`)) k A k , B, C, D 2 , D m , E m m ((µ), (⊕ 1 ), (⊕ 0 ), (⊥)) k (A, A) k , B, C, D 2 , D m , E m m (µ), (`) A 2k , C, D 2 , D m , E m m (ν), (⊕ 0 ), (⊥) A 2k , B, C, D 2 , D m , E m m :X i := not X i := • • • • :goto ( + 1 mod m + 1) A 2(i-1) , A, A, A 2(k-i) , B, C, D 2 , D m , E m m (ν), (⊕ 1 ) A 2(i-1) , A, A, A 2(k-i) , B, C, D 2 , D m , E m m :if X i then goto else := • • • • :goto A 2(i-1) , A, A, A 2(k-i) , B, C, D 2 , D m , E m m (ν) A 2(i-1) , A, νX¿X, A 2(k-i) , B, C, D 2 , D m , E m m (µ), (⊕ 0 ) A 2(i-1) , A, A, A 2(k-i) , B, C, D 2 , D m , E m m • • • • :goto A 2(i-1) , A, A, A 2(k-i) , B, C, D 2 , D m , E m m (ν) A 2(i-1) , νX¿X, A, A 2(k-i) , B, C, D 2 , D m , E m m (µ), (⊕ 0 ) A 2(i-1) , A, A, A 2(k-i) , B, C, D 2 , D m , E m m (µ), (&) A 2k , B, C, D 2 , D m , E m m (ν), (⊕ 1 ) A 2k , B, C, D 2 , D m , E m m Figure 3.6. Premises p of the preproof 0: := • • • • 0:goto 1 (A, A) k , B, C, D 2 , D m , E m m (ν) k (νX¿X, A) k , B, C, D 2 , D m , E m m ((µ), (∨ 0 )) k (A, A) k , B, C, D 2 , D m , E m m ((µ), (∨ 1 ), (∨ 1 ), (∨)) k A k , B, C, D 2 , D m , E m m ((µ), (∨ 1 ), (∨ 0 ), (⊥)) k (A, A) k , B, C, D 2 , D m , E m m (µ), (∨) A 2k , C, D 2 , D m , E m m (ν), (∨ 0 ), (⊥) A 2k , B, C, D 2 , D m , E m m :X i := not X i := • • • • :goto ( + 1 mod m + 1) A 2(i-1) , A, A, A 2(k-i) , B, C, D 2 , D m , E m m (ν), (∨ 1 ) A 2(i-1) , A, A, A 2(k-i) , B, C, D 2 , D m , E m m :if X i then goto else := • • • • :goto A 2(i-1) , A, A, A 2(k-i) , B, C, D 2 , D m , E m m (ν) A 2(i-1) , A, νX(¿X), A 2(k-i) , B, C, D 2 , D m , E m m (µ), (∨0) A 2(i-1) , A, A, A 2(k-i) , B, C, D 2 , D m , E m m • • • • :goto A 2(i-1) , A, A, A 2(k-i) , B, C, D 2 , D m , E m m (ν) A 2(i-1) , νX(¿X), A, A 2(k-i) , B, C, D 2 , D m , E m m (µ), (∨0) A 2(i-1) , A, A, A 2(k-i) , B, C, D 2 , D m , E m m (µ), (∧) A 2k , B, C, D 2 , D m , E m m (ν), (∨1) A 2k , B, C, D 2 , D m , E m m Figure 3.7. Premises p of the preproof for µLK ω :goto := Back edge to (Root) A, . . . , A, B, C, D 2 , D m , E m , . . . , E m (ν) m-1 A, . . . , A, B, C, D 2 , D m , νX¿ m X, . . . , νX¿ m X -1 , E m , νX¿ m X, . . . , νX¿ m X m- (µ), (∨ 1 ), (∨) m-1 A, . . . , A, B, C, D 2 , D m , E m ((µ), (∨ 0 ), (⊥)) m-1 A, . . . , A 2k , B, C, D 2 , D m , E m , . . . , E m -1 , E m , E m , . . . , E m m-
: := • • • • 0:goto 1 (A, A) k , B, C, D 2 , D m , E m m (µ L ) k (µX¡X, A) k , B, C, D 2 , D m , E m m ((ν L ), (∧ L 0 )) k (A, A) k , B, C, D 2 , D m , E m m ((ν L ), (∧ L 1 ), (∧ L 1 ), (∧ L )) k A k , B, C, D 2 , D m , E m m ((ν L ), (∧ L 1 ), (∧ L 0 ), ( L )) k (A, A) k , B, C, D 2 , D m , E m m (ν L ), (∧ L ) A 2k , C, D 2 , D m , E m m (µ L ), (∧ L 0 ), ( L ) A 2k , B, C, D 2 , D m , E m m :X i := not X i := • • • • :goto ( + 1 mod m + 1) A 2(i-1) , A, A, A 2(k-i) , B, C, D 2 , D m , E m m (µ L ), (∧ L 1 ) A 2(i-1) , A, A, A 2(k-i) , B, C, D 2 , D m , E m m :if X i then goto else := • • • • :goto A 2(i-1) , A, A, A 2(k-i) , B, C, D 2 , D m , E m m (µ L ) A 2(i-1) , A, µX(¡X), A 2(k-i) , B, C, D 2 , D m , E m m (ν L ), (∧ L 0 ) A 2(i-1) , A, A, A 2(k-i) , B, C, D 2 , D m , E m m • • • • :goto A 2(i-1) , A, A, A 2(k-i) , B, C, D 2 , D m , E m m (µ L ) A 2(i-1) , µX(¡X), A, A 2(k-i) , B, C, D 2 , D m , E m m (ν L ), (∧ L 0 A 2(i-1) , A, A, A 2(k-i) , B, C, D 2 , D m , E m m (ν L ), (∨ L ) A 2k , B, C, D 2 , D m , E m m (µ L ), (∧ L 1 ) A 2k , B, C, D 2 , D m , E m m Figure 3.9. Premises p of the preproof for µLJ ω :goto := Back edge to (Root) A, . . . , A, B, C, D 2 , D m , E m , . . . , E m (µ L ) m-1 A, . . . , A, B, C, D 2 , D m , µX¡ m X, . . . , µX¡ m X -1 , E m , µX¡ m X, . . . , µX¡ m X m- (ν L ), (∧ L 1 ), (∧ L ) m-1 A, . . . , A, B, C, D 2 , D m , E m ((ν L ), (∧ L 0 ), ( L )) m-1 A, . . . , A 2k , B, C, D 2 , D m , E m , . . . , E m -1 , E m , E m , . . . , E m m-

A polynomial sub-criterion

We have shown in the previous chapter that deciding the validity of the circular representation of a preproof, with respect to the thread criterion, is a PSPACE-complete problem.

This implies in particular that there is probably no subexponential algorithm to check the validity of a circular representation. This also implies that there is probably no way to certify the validity of a circular preproof, so that it can be checked in polynomial time, without adding to it an exponential quantity of information.

We tackle both these problems by taking a different approach. Instead of trying to handle the existing criterion, we will look for a new criterion.

The thread criterion has very good properties. In particular, Baelde, Doumane, and

Saurin [2016] proved that it guarantees soundness with respect to boolean interpretation and full cut elimination. Therefore, we would like our new criterion to have the following properties:

• that any preproof valid for the new criterion is also valid for the thread criterion, so that it inherits its soundness properties,

• that this new criterion is decidable in reasonable time,

• that it is possible to add a reasonable amount of information to the circular representation of a preproof so that the validity of this certified preproof may be checked in linear time,

• that this new criterion is expressive enough.

In this chapter, we provide such a criterion, which we called the loop criterion.

There is an essential difference between the thread criterion and our loop criterion. In usual proof theory, a proof is a finite tree, made of logical inferences, and a proof is correct as soon as each one of its inferences is correct. This is not true anymore with logics such as µMALL ω , in which the soundness of each inference only ensure that the tree is a preproof, and a proof also has to pass the thread criterion, which is a global criterion. The PSPACE-complete nature of the thread criterion forbids that it could have a local definition. It is, and has to be, a global criterion, which cannot be turned into a local criterion. In contrast, our loop criterion gives rise to a proof system in which the validity of a proof is a purely local property. More precisely, with our loop criterion comes an enriched proof system, made of labelled proof trees, with two properties:

1. if the circular representation of a preproof is valid for our loop criterion, it is possible to label it so as to obtain a proof in our labelled proof system, 2. in this labelled proof system, a proof is correct if and only if each one of its individual inferences is correct.

This would not be possible with the thread criterion, or the labeling would probably need to be at least exponential in the size of the proof.

There is another important difference between the usual thread criterion and our new loop criterion. The thread criterion is really a criterion on the infinite preproof, not on its representation. This means that if you have two different circular representations of the same infinite preproof, either they are both valid or both invalid. In contrast, our criterion really depends on the finite, circular representation, and not only on the infinite preproof which is represented. This means that among the circular representations of a

given infinite preproof, it may happen that some of them are valid for our loop criterion and some other are not.

In this chapter we prove that:

• If a circular representation of an infinite preproof is valid for our loop criterion then this preproof is valid for the thread criterion.

• Our loop criterion can be decided in quadratic time.

• Every circular representation which is valid for our loop criterion can be labelled so as to be turned into a proof in our labelled proof system, in which the validity of the proof only depends on the validity of each individual inference, and is therefore checkable in linear time.

• There is a canonical translation of the finitary proofs in the style of [START_REF] Baelde | Least and greatest fixed points in linear logic[END_REF] into circular representations of infinite proofs, which are valid for the thread criterion.

Those representations are also valid for our more restricted loop criterion. In other words, our labelling method capture the image of all finitary µMALL proofs.

L-proofs: labelling as validity

In this subsection, we briefly mention an alternative approach to ensure validity of µMALL ∞ preproofs, aiming at motivating the tools used in the remainder of this chapter.

The idea is to witness thread progress by adding labels on some formulas, much in the spirit of [START_REF] Stirling | A tableau proof system with names for modal mu-calculus[END_REF], [START_REF] Afshari | Cut-free completeness for modal mu-calculus[END_REF].

Definition 56 (Labelled formulas). Let L be an infinite countable set of atoms and call labels any finite list of atoms. Let

F L := σ L | σ ∈ {µ, ν}, L ∈ list(L) . Labelled formulas,
or L-formulas, are defined as µMALL formulas, by replacing F = {µ, ν} with F L in the grammar of formulas, in Definition 12. Negation is lifted to labelled formulas, as

(µ L XA) ⊥ = ν L XA ⊥ .
We write σXA for σ ∅ XA, and standard, unlabelled formulas can thus be seen as labelled formulas where every label is empty. We define a label-erasing function • that associates to every L-formula A the µMALL-formula A obtained by erasing every label and satisfying σ L XB = σX B .

The standard µMALL ∞ proof system is adapted, to handle labels, by updating the (id)

and (ν) rules of Figures 2.1 and 2.4 as

A = B ⊥ (id ) A, B A[ν L,a XA[X]], Γ (ν b (a)) ν L XA[X], Γ
where, in (ν b (a)), a must be a fresh label name, meaning that a does not appear free in the conclusion sequent of (ν b (a)) (in particular, a / ∈ L).

Since we are in a one-sided framework, only labels on ν operators are relevant. Therefore, from now on, formulas have non-empty labels only on ν and we require, for the cut inference, that all labels of cut formulas are empty.

Definition 57. L-preproofs are, as in Definition 18, possibly infinite derivations using L-formulas, with the constraint that for every two inferences (ν b (a)) and (ν b (b)), if one is above the other, then a = b.

And the validity condition is expressed in terms of labels in the following definition:

Definition 58 (L-proof). An L-proof is an L-preproof such that for every infinite branch γ = (s i ) i∈ω (seen as a sequence of sequent occurrences), there exists a sequence (ν L i XG i ) i∈ω and a strictly increasing function on natural numbers such that for every

i ∈ ω, 1. the formula ν L i XG i is principal in s (i) 2. ν L i XG i = ν L i+1 XG i+1 and 3. ∀i 1, L i = (L i-1 , a i ) for some a i ∈ L.
The label-erasing function • is easily lifted to sequents and to L-preproofs. We then have the following property:

Proposition 11. If π is an L-proof, then π is a µMALL ∞ proof.
Proof. First, π is a µMALL ∞ preproof because, as we explained, if we remove the labels, every rule in a L-proof is a µMALL ∞ proof. Then, as we will show now, the definition of L-proofs precisely reflects the thread criterion.

Suppose an infinite branch γ = (s i ) i∈ω ; we will show that π has a valid infinite inner thread in γ (Definition 39). There exists a sequence (ν L i XG i ) i∈ω and a strictly increasing function on natural numbers as in Definition 58. ∀i, let p i be the position of the

ν L i XG i which is principal in s (i) .
Remark that any sequent contains only a finite number of atoms a ∈ L and therefore {i ∈ ω | a i appears in the endsequent of π} is a finite set. Let i 0 := 1 + max{i ∈ ω | a i appears in the endsequent of π}, so that ∀i i 0 , the symbol a i , contained by L i , does not appear in the endsequent of π.

First consider any i i 0 , any j ∈ ω and any position p of a subformula equal to ν L i XG i in s j . The extremity t(s 0 , . . . , s j )(p) of T(s 0 , . . . , s j )(p) is either in a cut formula or in the endsequent of π. In both cases, it does not contain a i , which is present in L i . Let us denote by g(p) the lowest point of T(s 0 , . . . , s j )(p) which contains a i , it has to be a subformula of the active formula of the premise of a (ν b (a i )) inference. Similarly, let us denote by f (p) the highest point of T(s 0 , . . . , s j )(p) which does not contain a i , it has to be the principal formula of this same inference (ν b (a i )). And, of course, there is an edge

f (p) → g(p) in T(s 0 , . . . , s j )(p), induced by this inference.
From the last paragraph, we deduce that ∀i i 0 , there is a (ν b (a i )) inference in γ. We also deduce that the principal formula of this inference is

ν L i-1 XG i-1 . Remark that this is the only (ν b (a i ))
inference in γbecause of the constraint of Definition 57. Let s φ(i) be the position of the conclusion of this inference, and let us denote by q i the position of the

ν L i-1 XG i-1 which is the principal formula of this inference.
The union of the T(s φ(i-1) , . . . , s φ(i) )(q i ), for i i 0 + 1, is an infinite path in G in thread , which contains an infinity of principal formulas. This is a valid inner thread in π .

• Let b 0 be the corresponding infinite branch in π.

• By Lemma 8, let S 0 be the occurrence of sequent in π which is the lowest back edge target infinitely often crossed by b 0 . Being the target of some back edge(s), S 0 is the conclusion of a (ν b (a)) rule, which unfolds some νXA[X].

• Let us decompose b 0 by making apparent each occurrence of S 0 :

b 0 = r * -→ u 0 S 0 * -→ u 1 S 1 → be S 0 * -→ u 2 S 2 → be S 0 • • •
where r is the root of π, "be" denotes a back edge, the S i (i 1) are the sources of the back edges to S 0 and ∀i, u i does not cross S 0 except at its source.

• Let p 0 be the position in S 0 of the νXA[X] which is its principal formula.

• Remark that, because of the existence of back edges from every S i+1 to S 0 , all S i are identical sequents, except for the fact that a does not appear in S 0 while it appears at the only position p 0 in S i+1 . In particular, p 0 is also the position of a νXA[X] in S i+1 .

• For i 1, T(u i )(p 0 ) is a ν-thread in u i . Its target is the position p 0 in S i , which is the position of a νXA[X] labelled with a. Its source is a position of νXA[X] in S 0 .

We show that this source position is the same position p 0 of the νXA[X] that is principal in S 0 .

Let us decompose u i as

u i = S 0 -→ e 0 S 0 * -→ u i
where S 0 is the position of sequent immediately above S 0 , that is the premise of at position p 0 in S 0 .

•

T(u i )(p 0 ) is then a thread (S 0 , p 0 ) * -→ T(u 1 )(p 1 )
(S 1 , p 0 ). It is progressing, because its source is the principal conclusion of the rule (ν b (a)).

• By glueing the T(u i )(p 0 ) together, we get an infinite inner thread

(S 0 , p 0 ) * -→ T(u 1 )(p 0 ) (S 1 , p 0 ) → be (S 0 , p 0 ) * -→ T(u 2 )(p 0 ) (S 2 , p 0 ) → be (S 0 , p 0 ) • • • This thread is valid because every T(u i )(p 0 ) is progressing. And it is indeed a thread of b 0 = r * → u 0 S 0 * → u 1 S 1 → be S 0 * → u 2 S 2 → be S 0 • • •
• Hence b 0 is valid, which concludes this demonstration.

Proposition 14. µMALL proofs can be translated to µMALL .

Proof. The target of the usual translation µMALL → µMALL ω [Doumane, 2017b] is included in µMALL . See key case of the translation on Figure 4.1.

A[B], B ⊥ B, Γ (ν 0 inv ) νXA[X], Γ ≡ ( (a)) ν a XA[X], B ⊥ [A] A[ν a XA[X]], A[B] ⊥ A[B], B ⊥ (cut) A[ν a XA[X]], B ⊥ (ν b (a)) νXA[X], B ⊥ B, Γ (cut) νXA[X], Γ

Two alternative characterizations of µMALL

In the two following sections, we give two characterizations of µMALL , through validating sets in Definition 64, and through a threading criterion over back edges in Definition 66.

This allows us to give effective algorithms to decide whether a µMALL ω b.e.-tree preproof is in µMALL and, in case it is, to produce a labelling witnessing that fact.

Definition 61. Given a directed graph G = (V, E) and a set S ⊆ V , the set of vertices accessibles from S is denoted as S↑ := {v ∈ V | ∃s ∈ S, s → * v}. Similarly S↓ is the set of vertices from which S is accessible.

induces edges 2 → 4, 2 → 6, 2 → 8, 1 → 5, 1 → 7 and 3 → 9. Moreover, if the conclusion of this last rule is the target of a back edge whose source is ν 10 X(ν 11 Y X ⊗ X), ν 12 XX then this back edge also induces edges 10 → 1, 11 → 2, 12 → 3.

In the case of a cut formula, the formula has no corresponding formula in the conclusion sequent and in this case it induces an ingoing edge from the extra vertex ⊥:

ν 2 XX µXX, ν 3 XX (cut)
ν 1 XX induces edges ⊥ → 2 and 1 → 3.

Remark 20. Note that a vertex of the above graph may therefore have

• many ingoing edges: in case it in a sequent which is the target of some back edges;

• no ingoing edges: essentially the extra vertex ⊥ and the ν-formulas in the conclusion of the proof if it is not a target of back edge;

• many outgoing edges: see a ν-rule with νX(X ⊗ X) or νX(X `X) as principal conclusion;

• no outgoing edges: see the νXX in the 1 ⊕ νXX principal conclusion of a (⊕ 1 )-rule.

In the following definition, we define, for each (ν) rule (r) of a b.e.-tree preproof π, a subgraph of G π (Definition 62) called G r . The aim of this subgraph is to contain all paths in G π that uses only sequents and back edges above (r). We also define two subsets of the vertices of G r , called S r and T r . As we will show in Proposition 16, π is not in µMALL iff. there is a (ν) rule (r) such that there is a path in G r with source in S r and target in T r . This gives us an effective way to check membership in µMALL (Proposition 17).

Definition 63 (G r , S r , T r ). Let π be a µMALL ω b.e.-tree preproof and (r) an occurrence of a (ν)-rule. We define a subgraph of G π , denoted by G r = (V r , E r ), and two subsets of V r , denoted by T r and S r :

• the vertices v ∈ V r are the extra vertex ⊥ plus all positions that are in the conclusion of (r) and in all above sequents, that is all sequents accessibles from the conclusion of (r), in the sense of Definition 61;

• the edges e ∈ E r are all edges of G π between those vertices, minus the edges of G π that are induced by the back edges of π targetting the conclusion of (r), if there are some.

• T r ⊆ V r is the set of all positions of the principal formulas of the sources sequents of the back edges targetting the conclusion of (r);

• S r ⊆ V r is the set of all positions of all subformulas of the conclusion of (r) except for the position of its principal formula, plus the extra vertex ⊥.

Definition 64. Let (r) be an occurrence of a (ν) rule in a µMALL ω b.e.-tree preproof π.

A validating set for (r) is a set L ⊆ V r such that L = L↓ and T r ⊆ L ⊆ (V r \ S r ).

Proposition 15. Let (r) be an occurrence of a (ν) rule of a µMALL ω b.e.-tree preproof π. The following are equivalent:

1. There exists a validating set for (r)

2. T r is not accessible from S r in G r 3. T r ↓ ⊆ V r \ (S r ↑).
And if they are true, T r ↓ is the smallest validating set of (r) and V r \ (S r ↑) is the biggest one.

Proof. We first prove that

If L is a validating set, then T r ↓ ⊆ L ⊆ V \ (S r ↑) (4.1)
If L is a validating set, then on the one hand we have

T r ⊆ L hence T r ↓ ⊆ L↓ = L.
And on the other hand

L ⊆ V \ S r hence V \ L ⊇ S r
and, because the complement of a downward-closed set is upward-closed,

V \ L = (V \ L)↑ ⊇ S r ↑ hence L ⊆ V \ (S r ↑).
Now the implication (1) ⇒ (3) is an immediate consequence of (4.1).

For (3) ⇒ (2): if

T r ↓ ⊆ V \ (S r ↑) then T r ⊆ T r ↓ ⊆ V \ (S r ↑) hence S r ↑ ∩ T r ⊆ ∅ hence T r is not accessible from S r .
Finally (2) ⇒ (1): if T r is not accessible from S r then

S r ∩ T r ↓ ⊆ ∅ hence T r ⊆ T r ↓ ⊆ V \ S r hence T r ↓ is a validating set.
Regarding the second part of the proposition:

• if (3) is true then T r ⊆ T r ↓ ⊆ V r \ (S r ↑) ⊆ V r \ S r
hence T r ↓ and V r \ (S r ↑) are validating sets

• if L is any other validating set, then by (4.1), T r ↓ ⊆ L ⊆ V \ (S r ↑).

93

The following proposition gives an alternative criterion for µMALL .

Proposition 16. A finite representation π of a µMALL ω preproof is the erasing of a µMALL lab proof iff. every occurrence of a (ν) rule of π has a validating set.

Proof. (⇐=) Let us assume that every (ν) rule of π has a validating set. There is a finite number of (ν) rules in π; we label them with distinct variables a 1 , . . . , a n , in such a way that if the (ν) rule labelled by a i is below the rule labelled by a j in the representation then i j. We denote by L i a validating set for (ν b (a i )). We then do the following for each i, going from 1 to n: for each occurrence of ν-formula ν V XA that is at a position belonging to L i , add the variable a i to V , that is replace this occurrence of ν V XA with ν V,a i XA. By doing this it may happen that we break the validity of some rules of the representation: because L i , although downward closed, is in general not upward closed, so we may end with a situation in which this

A, C[ν V XD] A, C[ν V XD] & A & B, C[ν V XD] becomes A, C[ν V,a XD] B, C[ν V XD] & A & B, C[ν V,a XD]
which is not anymore a valid rule. We then patch this by adding as many (LWk) rules as needed on the premises:

A, C[ν V,a XD] B, C[ν V XD] (LWk) B, C[ν V,a XD] & A & B, C[ν V,a XD]
Similarly it may happen that the source of a back edge gets a bigger labelling than the target of this back edge; we patch this by adding (LWk) rules under the source sequent of the back edge. When this operation has been done for every i, from 1 to n, we obtain a validly labelled proof of µMALL lab .

(=⇒) Conversely, let π 0 be a µMALL lab representation such that π = π 0 . Up to renaming, we can assume that all (ν b ) rules of π 0 are labelled with distinct variables. For every occurrence of a (ν) rule in π, consider the corresponding (ν b (a)) rule in π 0 and let L a be the set of all occurrences of ν-formulas in π 0 that carry the variable a in their labelling. The constraints on the labelling of µMALL lab proof precisely say that L a is a validating set for the considered occurrence of (ν b ) in π.

Proposition 17.

• Checking validity of a µMALL lab preproof is decidable.

• Membership in µMALL can be decided in a time quadratic in the size of the (circular) preproof.

Proof.

• For the first point, it is enough to check the validity of each inference of the proof.

• For the second point, first check that each back edge targets a (ν) rule, then use the characterization of µMALL by validating sets (Proposition 16): for each (ν) rule (r), build graph G r and sets S r and T r and checks whether T r is accessible from S r in G r . Such a test of accessibility in a graph can be done in linear time. As we have to do that for each (ν) rule, in total it may take a time quadratic in the size of the preproof, but no more than that.

Definition 65. Let π be a µMALL ω b.e.-tree preproof and e a back edge in π, from a position of sequent s 1 to a position of sequent s 0 . Let S be the set of all positions of sequents that are strictly above s 0 . We say that this back edge is strongly valid under two conditions:

1. Its target s 0 has to be the conclusion of a (ν) rule.

2. Let us denote by p the position in s 0 of the νXA which is the principal formula of that (ν) rule. This is also a position of the same formula in s 1 . The second condition is that for every path u in G branch , going from s 0 to s 1 , using only positions of sequents in S, t(u)(p) is, again, the position p in s 0 . targetting the conclusion of (r). More precisely, the position of t in the sequent at s is the same as the position of the principal formula of (r) in the conclusion of (r). Because the definition of G r follows the threading structure of the preproof, the source s of v is t(u)(t). By definition of S r , this position s = t(u)(t) is either in a cut formula or in the conclusion of (r), at a position different from the position of its principal formula. This

shows that (r) is not strongly valid.

Corollary 3. The fragments defined in Definitions 60 and 66 coincide.

Conclusion

As this chapter and the next one share a lot of ideas, discussion of related works for this chapter has been placed in Section 5.5.

This chapter introduced the loop criterion for circular representations of infinite preproofs of µMALL ω . This defines a fragment of the circular representations of µMALL ω which we called µMALL .

We also defined a new proof system called µMALL lab . The proofs of µMALL lab are labelings of circular representations of preproofs, valid for the loop criterion. While circular representation of preproofs make use of a global validity criterion such as the

Finitization

The first systems designed to handle least and greatest fixed points connectives were finitary systems. Infinitary and circular systems were then proposed as an alternative.

In each of these circular extensions of finitary systems, there is a canonical translation from finitary proofs to circular proofs. This implies in particular that any sequent that is provable in the finitary system is also provable in the circular system. The converse is known as the Brotherston-Simpson conjecture and was first stated by [START_REF] Brotherston | Sequent calculus proof systems for inductive definitions[END_REF]Simpson [2007, 2011] in the context of Martin-Löf's system of inductive definitions for first-ordre classical logic. It is also called the problem of finitization: can we turn an infinitary proof into a finitary one, and how? In the context of first-order classical logic with inductive definitions, it was proved by Berardi andTatsuta [2017b, 2019] that the conjecture is false in general, but it was shown by [START_REF] Simpson | Cyclic arithmetic is equivalent to peano arithmetic[END_REF], Berardi andTatsuta [2017a, 2018] that it becomes true as soon as you add Peano (or even Heyting) arithmetic to the circular and finitary systems. But the question is still open in the case of µMALL and µMALL ω , which is a quite different system, more in the family of µ-calculi.

In that setting, on one hand we do not have first-order predicates and the possibility to encode Peano arithmetic, on the other hand we have access to all possible inductive and coinductive definitions of formulas, including interleaving of least and greatest fixed points.

Here the question of finitization is: if a conclusion is provable by a circular proof, valid for the thread criterion, that is a proof in µMALL ω , is it already provable in the finitary system µMALL?

This question is, as of today, an open problem. Now, in the previous chapter, we provided a new criterion, the loop criterion, which defines a new logic µMALL , which has two properties:

• the canonical translation of any finitary proof is a circular representation which is valid for the loop criterion, so any conclusion which is provable in µMALL is also provable in µMALL

• if the circular representation of a preproof is valid for the loop criterion, then it is also valid for the thread criterion, so any conclusion that is provable in µMALL is 5.1 On Brotherston-Simpson's conjecture: finitizing circular proofs 2. for each formula A (with labels) occurring in the proof, a formula A without labels:

Definition 68 (Translation of labelled formulas to unlabelled formulas). We define by mutual induction:

1. Γ a := Γ ((a)) .

H

∅ [F ] := F and H V,a [F ] := ⊗Γ ⊥ a ⊕ H V [F ].
In other words,

H V [F ] a∈V ⊗Γ ⊥ a ⊕ F 3. By induction on formula A, A is: • ν V X.A := νXH V [ A ]
• it is homomorphic on other connectives: (a) (1)

X := X, 1 := 1, µXA := µX A , A ⊗ B := A ⊗ B , etc.
A[ν V X.A] , Γ (⊕ 1 ) |V | H V A[ν V X.A] , Γ (ν) ν V X.A , Γ (b) (⊗), (id) ⊗Γ ⊥ a , Γ a (⊕ 0 ) H V,a A[ν V,a X.A] , Γ a (ν) ν V,a X.A , Γ a (c) B[ν V X.A] , Γ B[ν V,a X.A] , Γ := (id) H V A[ν V X.A] , H V A[ν V X.A] (⊕ 1 ) H V,a A[ν V X.A] , H V A[ν V X.A] (µ) H V,a A[ν V X.A] , ν V X.A ⊥ (ν 0 inv ) ν V,a X.A , ν V X.A ⊥ [ B ] B[ν V,a X.A] , B[ν V X.A] ⊥ B[ν V X.A] , Γ (cut) B[ν V,a X.A] , Γ (d) A[ν V,a X.A] , Γ a ν b (a) ν V X.A , Γ a := A[ν V,a X.A] , Γ a (⊕ 1 ) |V | H V A[ν V,a X.A] , Γ a (`) H V A[ν V,a X.A] , `Γa (id) H V A[ν V,a X.A] , H V A[ν V,a X.A] (&) H V A[ν V,a X.A] , H V,a A[ν V,a X.A] (µ) H V A[ν V,a X.A] , ν V,a X.A ⊥ (⊗), (id) ⊗Γ ⊥ a , Γ a (⊕ 0 ) H V,a A[ν V,a X.A] , Γ a (ν) ν V,a X.A , Γ a (νinv) ν V X.A , Γ a
( ) L, L T (`)(⊗) D ⊗ L, L D ⊗ T (ν) L, L D ⊗ T (id) D D (1) ( ) L, L T (`)(⊗) L, D ⊗ L D ⊗ T (ν) L, L D ⊗ T (µ), (&) L, L T (1) (b) (id) D D (1) ( (a)) L a+ , L T (`)(⊗) D ⊗ L a+ , L D ⊗ T (ν)[a] L a-, L D ⊗ T (LWk(b-)) L a-, L b-D ⊗ T (id) D D (2) ( (b)) L a-, L b+ T (`)(⊗) L a-, D ⊗ L b+ D ⊗ T (ν)[b] L a-, L b-D ⊗ T (µ)(&) L a-, L b-T (2) (Rec(b)) L a-, L T (1) (Rec(a))
L, L T By replacing L 0 and T 0 with L := µX(D ⊗ X) and T := µX((D ⊗ X) & (D ⊗ X)), we get an example equally interesting and more readable, which we present in Figure 5.3. In this example, remember that a formula on the left on the sequent means its negation on the right and note that the labels we write on L are meant to be put on its fixed-point connective. That is, a L a on the left on the sequent means a ν a X(D ⊥ `X) on the right of the sequent. In this interleaving function, every recursive call leaves one of the two arguments untouched and makes the other one decrease. This guarantees that the tree of recursive calls is well-founded. Difficulties, however, arise from the fact that it is not necessarily always the same argument that will decrease.

More formally: every infinite branch in the preproof above has two interesting threads, going through the L formulas. In every branch going infinitely often to the left (resp. to the right), the thread going through the first L of the sequent (resp. the second L of the sequent) will be validating. That preproof is thus a valid µMALL ω proof. However, our previous labelling method cannot be applied here for two reasons:

1. in our previous setting, labelled pre-proof have the property that one can know which thread will validate a branch, just by knowing the lowest target of back edge that is visited infinitely often by the branch. This is not the case here, because the two back edges, while inducing different validating threads, have the same target;

•

T(u i )(p) is a ν-thread in u i ,
• its target is p in S i , which is labelled with a+,

• and its source is p in S 0 , which is labelled with a-.

An examination of the rules that may compose u i shows that the only way for that to be true is that T(u i )(p) is progressing. Now T 0 is an infinite tree with a finite number of roots and an arity bounded by Card(P 0 ), hence, by Kőnig's lemma, it has an infinite branch

(1, p 1 ) ← (2, p 2 ) ← (3, p 3 ) • • • .
This infinite branch induces in turn an infinite thread

(S 0 , p 0 ) * -→ T(u 1 )(p 1 ) (S 1 , p 1 ) → be (S 0 , p 1 ) * -→ T(u 2 )(p 2 ) (S 2 , p 2 ) → be (S 0 , p 2 ) • • • This thread is valid because every T(u i )(p i ) is progressing. And it is indeed a thread of b 0 = r * → u 0 S 0 * → u 1 S 1 → be S 0 * → u 2 S 2 → be S 0 • • • Hence b 0 is valid, which concludes this demonstration.
We now label our two examples with this new system. We will show that, while it is quite straightforward to label the interleaving example (Figure 5.3) with this new system, it requires, for π ∞ (Figure 5.2), to unfold one back edge.

π ∞ is presented, on Figure 5.5, labelled according to the extended labelling of Figure 5.5.

To be able to label π ∞ , two preliminary steps were necessary:

• To make K apparent as a subformula of I and J respectively by decomposing I and J as:

I = I [K] J = J [K]
where

J [Y ] := µX((Y `X) ⊕ ⊥) I [Y ] := µZ((Z `J [Y ]) ⊕ ⊥).
• To do one step of unfolding on the rightmost back edge.

After that, we can take advantage of the two new facilites of the extended labelling:

1. to add three (Rec) rules, corresponding to the three ways for a branch of π ∞ to be valid, as summarized in the following array.

Shape of the branch

A • l ω A • r ω l • (r + • l + ) ω Lowest (Rec) visited ∞ ly b a c Validating ν-formula H G K
2. to label the three formulas H, G and K at each corresponding (Rec), using for K the ability to label several occurrences at a time, and to label deeply ν-subformulas.

This indeed forms a correct labelling of π ∞ according to the extended labelling, hence ensuring its thread-validity.

Extending finitization

As we did in Section 5.1 for the labelling defined in Chapter 4, we will rely on the labelled presentation of the proofs in order to finitize them. More precisely, we will consider a fragment of the extended labelling of Definition 69, for which we will be able to finitize νXA, Γ in which only one occurrence of νXA is labelled, and this occurrence is a formula of the sequent and not a strict subformula.

Observe already that both the interleaving example (Figure 5.3) and π ∞ (Figure 5.2) respect the two constraints of Definition 70, except for the labelling of K in π ∞ .

We show now how to finitize any labelled representation which verify those two restrictions.

As the interleaving example of Figure 5.3 is labelled in this core fragment, it gives a finitization for the preproof of Figure 5.3. We will then show how to extend this method in an ad hoc way to finitize entirely π ∞ (Figure 5.2) from the labelling of Figure 5.5.

Definition 71. For any formula νXA and any unlabelled context Γ, we define the following formula translation: By Proposition 20, the rules of the core fragment of the extended labelling are translated to usual µMALL ω rules involving no label.

ν Γ-XA[X] e := νX A e [⊗Γ ⊥ ⊕ X] ν Γ+ XA[X] e := ⊗Γ ⊥ ⊕ ν Γ-XA[X] e Remark

Remark moreover that

A[ν Γ+ XA[X]] e , ∆ (ν)
ν Γ-XA[X] e , ∆ is the usual (ν) rule.

These allow to translate any labelled proof verifying the two constraints of Definition 70 into a µMALL finitary proof.

An ad hoc finitization of π ∞

The method of the previous section works almost as well for finitizing π ∞ based on the labelling of Figure 5.5: it allows to expand everything concerning the variables a and b. However, as it is, it cannot be applied directly to expand the variable c, for which the second conditions of Definition 70 is not verified. We can anyway finitize π ∞ , but at the cost of a somewhat ad hoc translation:

νXA e , ∆ (LWk(Γ-)) e ν Γ-XA e , ∆ = (id) νX A e [X], µX A ⊥ e [X] (⊕ 1 ) Γ ⊥ ⊕ νX A e [X], µX A ⊥ e [X] [ A e] A e [Γ ⊥ ⊕ νX A e [X]], A ⊥ e [µX A ⊥ e [X]] (µ) A e [Γ ⊥ ⊕ νX A e [X]], µX A ⊥ e [X] νX A e [X], ∆ (ν inv ) νX A e [Γ ⊥ ⊕ X], ∆ ( (Γ)) e ν Γ+ XA e , Γ = (⊗) * (id) ⊗Γ ⊥ , Γ (⊕ 0 ) ⊗Γ ⊥ ⊕ ν Γ-XA e , Γ ν Γ-XA e , ∆ (LWk(Γ+)) e ν Γ+ XA e , ∆ = ν Γ-XA e , ∆ (⊕ 1 ) ⊗Γ ⊥ ⊕ ν Γ-XA e , ∆ ν Γ-XA e , Γ (Rec (Γ)) e νXA e , Γ = (id) A e [ ν Γ+ XA e ], A e [ ν Γ+ XA e ] ⊥ (µ) A e [ ν Γ+ XA e ], ν Γ-XA ⊥ e ν Γ-XA e , Γ (`) * ν Γ-XA e , `Γ (id) ν Γ-XA e , ν Γ-XA ⊥ e (&) ν Γ-XA e , ν Γ+ XA ⊥ e (cut) A e [ ν Γ+ XA e ], ν Γ+ XA ⊥ e (⊗) * (id) ⊗Γ ⊥ , Γ (⊕ 0 ) ν Γ+ XA e , Γ (
Remark 22. In the following formulas, the notation µ_A is used to denote the formula µZA where Z is a variable which does not appear in A.

Γ c := F, G, H K c- e := νY µ_((⊗Γ ⊥ c ⊕ (I [Y ] `J [Y ])) ⊕ ⊥) I c+ := I + e = I [K c+ ] e := µ_((⊗Γ ⊥ c ⊕ (I [ K c- e ] `J [ K c- e ])) ⊕ ⊥) L c+ := I [K c+ ] `J [K c+ ] e := ⊗Γ ⊥ c ⊕ (I [ K c- e ] `J [ K c- e ])
These definitions allow to make finitary the derivation of are fully expanded, respectively, on Figures 5.8 and 5.9.

We now detail the analysis leading to this choice of formulas. To finitize π ∞ we try to apply the same method as for the interleaving example of Figure 5.3 p. 104, by expanding every labelled formula to a non-labelled one and expanding the rules that need it to match these transforms. This works perfectly for H and G, which appear respectively as formulas of the premises (Rec(b)) and (Rec(a)). But the situation is more delicate for K for which we have to face a double difficulty: in the premise of (Rec(c)), K is not a formula of the sequent but a subformula, and it appears in two different formulas.

Let us try to transform this situation into one that would fit our method. First we would like to have only one formula containing K instead of the two I and J. Unfortunately, none of them can be unlabelled without breaking the labelling. Fortunately the solution to that is easy: I, J is simply equivalent to I `J.

Now we would like I `J to be a ν-formula that we could label. We already made use, F, G a-, H, I + , J -

F, G a-, H, K c-, J -

(µ)(⊕ 0 )(`)
F, G a-, H, J -

(µ)(⊕ 1 )(⊥)
F, G a-, H, I + , J -

F, H, G a-, I + , J -

(`)
F `H, G a-, I + , J -

(ν)(⊕ 0 )(⊥)
F `H, G a-, H, I + , J - F, G a-, H, I c+ , J -

F, G a-, H, K c-, J -

(µ)(⊕ 0 )(`)
F, G a-, H, J -

(µ)(⊕ 1 )(⊥)
F, G a-, H, I c+ , J -

F, H, G a-, I c+ , J -

(`)
F `H, G a-, I c+ , J -

(ν)(⊕ 0 )(⊥)
F `H, G a-, H, I c+ , J - ⊥, 1 in which we use the notation µ_A to denote a µXA with X not appearing free in A.

(⊕ 1 ) (⊗Γ ⊥ a ⊕ G) ⊕ ⊥, 1 (&) (⊗Γ ⊥ a ⊕ G) ⊕ ⊥, G ⊥ & 1 (µ) (⊗Γ ⊥ a ⊕ G) ⊕ ⊥, G ⊥ (id) F, F ⊥ (id) G, G ⊥ (id) H, H ⊥ (⊗) 2 F, G, H, F ⊥ ⊗ G ⊥ ⊗ H ⊥ (⊕ 0 ) F, G, H, L c+ ⊕ 1 F, G, ⊥ ⊕ H, L c+ (ν) F, G, H, L c+ ⊕ 0 F, G, H, L c+ ⊕ ⊥ (µ)

F, G, H, I c+

This degenerate µ binder could be removed to simplify the formulas involved in the finitization, but we keep it to stay as close as possible to the original structure of I, trying to preserve its head connective.

When we stick all that together we get

I `J L [νY M [L [Y ]]] νY L [M [Y ]]
which is a ν-formula that we know, when labelled, how to expand into an unlabelled formula. If we stopped here our analysis, we would then define:

Γ c := F, G, H L c-:= νY L [M [⊗Γ ⊥ c ⊕ Y ]] L c+ := ⊗Γ ⊥ c ⊕ L c-.
However we will do yet a bit more work in order to get the structure of L c-closer to that of I `J.

Indeed the isomorphism (5.1) can be used in the other direction:

νY L [M [⊗Γ ⊥ c ⊕ Y ]] L [νY M [⊗Γ ⊥ c ⊕ L [Y ]]] = I [νY M [⊗Γ ⊥ c ⊕ L [Y ]]] `J [νY.M [⊗Γ ⊥ c ⊕ L [Y ]]].
This, finally, leads us to define:

Γ c := F, G, H and K c-:= νY M [⊗Γ ⊥ c ⊕ L [Y ]]
which allows to expand I [K c-] and J [K c-]. On the other hand, this is not sufficient to define an expansion of K c+ , and we still need an ad hoc treatment for formulas containing it:

"I [K c+ ]" :=

I c+ := M [⊗Γ ⊥ c ⊕ L [K c-]] "I [K c+ ] `J [K c+ ]" := L c+ := ⊗Γ ⊥ c ⊕ L [K c-]
With these expansions of labelled formulas into unlabelled formulas, we can finitize the derivation of Figure 5.5 into the very close derivation of Figure 5.6a, on which the rules dealing with labelling can be expanded into µMALL derivations.

Related works on Chapters 4 and 5

Labelling and local certification is the basis of our approach. The idea of labelling µformulas to gather information on fixed-points unfoldings is naturally not new, already to be found in fixed-point approximation methods (see [START_REF] Dax | A proof system for the linear time µcalculus[END_REF]] for instance). The closest work in this direction is [START_REF] Stirling | A tableau proof system with names for modal mu-calculus[END_REF]'s annotated proofs and the application [START_REF] Afshari | Cut-free completeness for modal mu-calculus[END_REF] made of such proofs in obtaining completeness for the modal µ-calculus. Our labelling system works quite differently since only fixed-point operators are labelled while, in Stirling's annotated proofs, every formula is labelled and labels are transmitted to immediate subformulas with a label extension on greatest fixed-points. Circular proof search triggered interest compared to proof system with explicit inductive invariants (lacking subformula property). As we already mentionned, this has actually been turned to practice by [START_REF] Brotherston | A generic cyclic theorem prover[END_REF].

Conclusion

In this chapter, we contributed to the theory of circular proofs for µMALL in two directions: (i) expanding the results of Chapter 4 by identifying larger fragments of circular proofs for which local conditions account for the validity of circular proof objects (in contrast to the global nature of thread conditions) and (ii) designing methods for translating circular proofs to finitary proofs (with explicit (co)induction rules). To do so, we introduced and studied several labelling systems, for circular proofs, and made the following contributions:

(i) First, we investigated how such labellings ensure validity of a labellable proof, turning a global and complex problem into a local and simpler one. Indeed, validity-checking is far from trivial in circular proof-theory for fixed-point logics: the best known bound for this problem is generally PSPACE and, in the case of µMALL and similar µ-calculi, we proved in Chapter 3 that checking thread-validity is in fact a PSPACEcomplete problem. We extended the results of Chapter 4 by defining a second, more liberal labelling, which does not force back edges to target (ν) inferences. We proved that this extended labelling still ensure thread-validity, and we were able to finitize a fragment of it.

(ii) Second, we provided evidence on the usability of such labellings as a helpful guide in the generation of (co)inductive invariants which are necessary to translate a circular proof in a finitary proof system with (co)induction rules à la Park. We provided a full finitization method for the fairly restricted labelling system of Chapter 4, which contains at least all the translations of µMALL proofs as well as for a core fragment of the extented labelling of this chapter, which subsumes the labelling of Chapter 4. However, this fragment is too constrained to treat standard examples that we discuss in the chapter, and which contain most of the difficulties in finitizing circular proofs, namely: (i) interleaving of fixed-points and (ii) interleaving of back edges resulting in various choices of a valid thread to support a branch.

Conclusion

General conclusion

We started this journey by explaining that the already existing finitary systems for least and greatest fixed points of formulas, with induction and coinduction rules [START_REF] Baelde | Least and greatest fixed points in linear logic[END_REF],

needing explicit invariants were not satisfactory. We explained that the infinitary setting designed by [Baelde, Doumane, and Saurin, 2016] was proposed as a solution to these issues. We then complained about the fact that these infinite proof trees are infinite and explained that this thesis is only concerned with the circular representations of infinite proofs. After proving that the thread criterion is PSPACE-complete on these circular representations, we argued for the search of a smaller, easier to check criterion, which would still be expressive enough for practical use. We provided such a criterion, the loop criterion, and we finally showed how any circular preproof valid for our loop criterion can be turned into a finitary proof à la Baelde with explicit induction and coinduction invariants.

It may seem that after all this work we finally reached our starting point.

But, as one may expect, we learned some valuable things through this journey.

• The result of PSPACE-completeness of the thread criterion (Theorem 4), which is the main contribution of Chapter 3, is, as far as we know, the first of its kind. Not only does it give a precise characterization of the complexity of the thread criterion, but its proof also made apparent the deep link that seems to exist between this global validity condition and program termination techniques such as size-change termination [START_REF] Chin | The size-change principle for program termination[END_REF]].

• The fragments of µMALL ω defined in Chapter 4 and in Section 5.2 combine advantages of both µMALL and µMALL ω . One one side, when they are viewed as unlabelled systems, they are circular systems, in it is not necessary to find and write explicit invariants when introducing a ν or eliminating a µ. On the other side, when they are viewed as circular systems, they do not necessitate a global validity criterion which may be subtle to understand, but they work with basic sequent calculus constructions in which the validity of the proof, which is finite, 121 6.2 Future works further since it may also be a key for our finitization objective. Note that the previous two directions would lead to a solution to the Brotherston-Simpson conjecture.

Our work in Chapter 5 helped closing the gap between µMALL ω and µMALL by proposing a rich fragment of µMALL ω that is equivalent µMALL. A very natural question for future work is to extend the still ad hoc finitization method presented in the last section to the whole fragment of relaxed labelled proofs, and maybe to all µMALL ω .

We also wish to investigate the potential use of labellings in circular proof-search. Indeed, there are several different labellings for a given finite derivation with back edges where the labels are weakened. Proposition 15 characterizes least and greatest validating sets: those extremal validating sets correspond to different strategies in placing the labels, which have different properties with respect to the ability to form back edges or to validate the proof that one may exploit in proof-search.

  int list = [] | ( :: ) of int * int list And let us consider the following type t, parameterized over a type a: type a t = Nil | Cons of int * a Remark that the type t is conceptually simpler than int list, because it is not a recursive type. If you are familiar with algebraic datatypes, you may see that this type could be written as a t = 1 + int * a where we use 1 to denote the singleton type: type 1 = () Now we can define two functions inj : int list t -> int list fold : ( a t -> a) -> int list -> a Nil | x :: xs -> f (Cons (x, fold f xs))

Figure 1 . 1 .

 11 Figure 1.1. Coinduction rule à la Park

  A, B, C are three sets and σ : A B × A * Fml and ρ : B C × A * Fml are two partial functions, we define their composite ρ • σ : A C × A * Fml a → (c, v • u) where (b, u) = σ(a) and (c, v) = ρ(b) Remark 3. The interested reader may recognize the Kleisli category of the monad _×A * Fml on Set, whose multiplication and unit are induced by the monoidal structure of A * Fml .

Figure 2 . 3 .

 23 Figure 2.3. Threading functions for the (µ) and (ν inv ) rules of µMALL

  Figure 2.1 with two rules. Those rules reflect the definitions of least and greatest fixed points of non-decreasing function on ordered sets that we gave in Section 1.1.1. Definition 15. The set of rules of the sequent calculus µMALL is the union of the rules for MALL, given in Figure 2.1 and of the two rules given in Figures 2.2 and 2.3.

  inference. Those positions of sequents that are not the conclusion of a logical inference are called positions of open sequents. The other positions are called positions of closed sequents.

  Definition 26 (Π 0 (µMALL ω ): µMALL ω b.e.-tree preproofs). A µMALL ω b.e.-tree preproof consists of a finite proof tree with open sequents π (Def. 24), composed using the rules of µMALL ∞ given above in Def. 17, together with a function back, which associates to each position s of an open sequent in π, a position back(s) of the same sequent in π, such that back(s) is strictly below s in π, i. e. between s and the root. We denote by Π 0 (µMALL ω ) the set of all µMALL ω b.e.-tree preproofs.

  Definition 28 (G branch , branch graph of a preproof). Let (π, back) be a µMALL ω b.e.-tree preproof. Its branch graph is the graph G branch defined as follows. The vertices of G branch are the positions of closed sequents in π. For each inference I with conclusion s in π and for each premise s of I, there is an edge in G branch , from s to s if s is a closed position of sequent in π, and from s to back(s ) if s is an open position of sequent in π. Definition 29 (Infinite branch). If (π, back) is a b.e.

  case of b.e.-tree-preproofs. Definition 40 (Generalization of t and T). The definitions of t (Definition 10) and T (Definition 11) are extended in the obvious way to the setting of µMALL ω b.e.-tree preproof: if (π, back) is a µMALL ω b.e.

  PSPACE-complete problems Definition 48 (BOOLE false and B false ). A program in BOOLE false is a sequence of instructions b = 1:I 1 2:I 2 . . . m:I m where an instruction can have one of the two following forms: I ::= X := ¬X | if X then goto else goto where X ranges over a finite set of variable names. The semantic is as expected, with all variables being equal to false at the beginning of the program, and the program halting when reaching instruction m + 1. Finally it is required of every program b ∈ BOOLE false that if b terminates then all variables have value false at the end of its execution. We also denote the set of terminating programs as: B false := {b ∈ BOOLE false | b terminates} Remark 9. The constraint on the values of the variables at the end of the program will be useful when reducing it, in Chapter 3, to the problem of validity of a µMALL ω b.e.-tree preproof. This preproof will encode the fact that the program b is terminating by connecting the final state to the initial one, hence the necessity that its initial and terminal states are the same. Lemma 2. B false is PSPACE-hard under LOGSPACE-reductions: PSPACE L B false

  of deciding the validity of a circular representation of a µMALL ω preproof is in fact PSPACE-complete. This result is established by a reduction from the problem of deciding the termination of a boolean program. Our proof takes a lot of inspiration from the proof of PSPACE-completeness of size-change termination by Lee, Jones and Ben Amram [Lee, Jones, and Ben-Amram, 2001]: in order to prove that deciding size-change termination is PSPACE-complete, they define a notion of boolean program and use the fact that the following set is complete in PSPACE: B = {b | b is a boolean program and b terminates.} then they reduce B to the problem of size-change termination. We adapt their method by reducing B to the problem of thread-validity in circular µMALL ω preproof. It would be very interesting to get a more precise understanding of the relation between threads in circular proofs and size-change termination.

  2), is represented on Figure 3.3, p. 76. It has one initial state. All paths are accepted. It recognizes the language (abcde + abf ) ω . And the automaton of valid infinite branches of preproof (3.2) is represented on Figure 3.4, p. 77. It has 4 initial states. The only three transitions with priorities < ω are

  e. the vertices of G out thread plus one extra vertex for each vertex of G branch • If we keep the notation i branch to denote the position of the endsequent of , the set of initial states I thread is the set of all positions of formulas in i branch , plus the extra vertex ⊥ i branch .

Definition 54 (

 54 Call graph of a program). Assume a boolean program b with variables X 1 , . . . , X k and instructions 1 : I 1 , . . . , m : I m . Define the call graph of b to be G = (V, E) with • V = {0, 1, . . . , m}

  2k and E m m is an abbreviation for E m , . . . , E m m and the subtrees 0: , 1 : I 1 , . . . , m : I m will be defined below. Remark 10 (Short notation for long sequents). You just saw on Eq. (3.3) that, for any formula A, we use A n as an abbreviation for A, . . . , A n formulas . Similarly, for any formulas A and B, we may use (A, B) n as an abbreviation for A, B, . . . , A, B 2n formulas

Figure

  Figure 3.6.

B

  us now take a closer look at what happens to B and C in the different branches of the tree with back edges p. Formulas B and C are touched only at the bottom of the :I parts of the preproof b , in the following way: • when going through branch 0, B is erased and C forks into a new copy of B and a recreated C. • When going through any other branch, two threads are maintained: one at B and one at C, and the thread at B progresses.Therefore: if an infinite branch u goes infinitely through 0, u contains no infinite thread at B, only an infinite thread at C, which is a µ-thread, hence u has no validating thread in the B/C part of the root sequent. If, on the contrary, u goes only finitely many times through 0, it has then a thread at B, which is a ν-thread, and which is infinitely progressing, hence a validating thread.These two diagrams sum up the behavior of the threads in the {B, C} group in 0: and in all other : I respectively: Remark 14. Because of lemma 6, the only infinite branches of b whose validity is not known in advance are the u ∈ E ω which are valid paths in G going infinitely many times through edge 0, and we know that these infinite branches may have validating threads only in one of the k groups {A + i , A - i } 1 i k . Such an infinite branch can always be factorized into u 0 0u 1 0u 2 0 • • • where the u n do not contain 0. As the edge 0 ∈ E has source and target 0 0 -→ 1, and because of the hypothesis that u is a path in G, for n 1 every u n has source and target 1 , which does not contain the edge 0. If u is a prefix of the execution of b then the threads of {A

  be the call-graph of b, as defined in Definition 54. Following remark 12, we denote by elements of E ω the infinite branches of b . There are two cases: either b ∈ B false and we have to prove that p / ∈ Π(µMALL ω ), or b / ∈ B false and we have to prove that p ∈ Π(µMALL ω ). First case: if b ∈ B false : the execution of b induces a finite path u = 1 → * 0 in G. This finite path can be completed into v = 0 0. Then v ω is an invalid branch of p ω . Here we use the fact that when b terminates, every variable has value false. Second case: if b / ∈ B false :

  thread diagrams that we have used to describe the preproof generated by the reduction are very similar to the size-change graphs generated by their reduction; this is in fact what has guided the design of this preproof: formula A mimicks the X i , X i part of their graphs and formulas B and C adapt the Z part of their graphs. We had to add the formulas D 2 and D m in order to have branching rules in the preproof. One of the main novelties of our reduction, compared to the reduction of Lee, Jones and Ben Amram for size-change termination, lies in the E m and :goto part of the constructed preproof, which has no equivalent in the size-change graphs obtained by their reduction. This part of our construction allows us to construct a preproof which is a tree with back edges, hence proving that the thread criterion is PSPACE-complete even when preproofs are represented by trees with back edges. We could in fact drop the E m and :goto part of the construction by constructing b as a rooted graph instead of a tree with back edges. The constructions proofs are still correct -and shorter. The caveat is that it only proves the thread-criterion to be PSPACE-hard in graph-shaped preproofs and not in b.e.

  Figure 3.1. Automaton recognizing the branches of the preproof (3.1).

Figure 3 Figure 3

 33 Figure 3.2. Automaton recognizing the valid branches of the preproof (3.1).

Figure 3

 3 Figure 3.4. Automaton recognizing the valid branches of the preproof (3.2).

Figure 3 . 8 .

 38 Figure 3.8. Back edges of the preproof for µLK ω

  0

Figure 3 .

 3 Figure 3.10. Back edges of the preproof for µLJ ω

  the (ν b (a)), and e 0 is the edge induced by the (ν b (a)) rule.By definition of u i , the path u i does not cross (ν b (a)). By Lemma 9, the source of T(u i )(p 0 ) is a position labelled with a, in S 0 . Hence, this is a position p 0 of a νXA[X] in the unfolding A[νXA[X]] caused by (ν b (a)). The source of T(u i )(p 0 ) is then the image in S 0 of this νXA[X] at p 0 , that is the principal formula νXA[X]

Figure 4

 4 Figure 4.1. translation µMALL → µMALL lab

4.

  • is lifted from formulas to sequences of formulas, pointwise. This is well-founded because, since any two distinct ν b rules wear distinct variables, the only Γ b that are needed in the computation of Γ a are those with b < a. Note that A = A as soon as A has no label variable. We can now state and prove the finitization theorem:Theorem 5. Every provable sequent of µMALL is provable in µMALL. Proof. Let π be a µMALL lab proof and replace, everywhere, each formula A by A . All rules in this (almost) new derivation are now valid instances of µMALL rules, except for (ν b ), (LWk) and ( ) rules. Actually, images of these rules by sequent translation • are derivable in µMALL as shown in fig. 5.1 (a), (b) and (c) for ( ), (LWk) and (ν b ), respectively. Replacing each instance of a (ν b ), (LWk) or ( ) rule in π by its derived version, we get a fully valid proof of µMALL. If the conclusion of the original µMALL proof was Γ then what we get is a proof in µMALL of Γ , i. e. the conclusion of the original µMALL proof, if Γ contains no label variable.

Figure 5 . 1 .

 51 Figure 5.1. Derivability of (a) (ν f ) rule ; (b) ( ) rule ; (c) (LWk) rule and (d) (ν b )rule .

Figure 5

 5 Figure 5.3. (a) Interleaving example; (b) Interleaving example labelled.Corresponding sources and targets of back edges are denoted by parenthesized numbers.

  Core fragment of the extended labelling). A µMALL ω b.e.-tree preproof labelled with the extended labelling of Definition 69 is in the core fragment of this extended labelling if: 1. no ν-formula wears more than one variable 2. (Rec) is used only in the particular form ν a-XA, Γ (Rec (a))

  21. With these definitions, we have ν Γ-XA[X] e A e [ ν Γ+ XA[X] e ] through a simple ν-unfolding. Proposition 20. With the notations of Definition 71, the following rules are derivable: νXA e , ∆ (LWk(Γ-)) e ν Γ-XA e , ∆ ν Γ-XA e , ∆ (LWk(Γ+)) e ν Γ+ XA e , ∆ ν Γ-XA e , Γ (Rec (Γ)) e νXA e , Γ ( (Γ)) e ν Γ+ XA e , Γ Proof. See derivations on Figure 5.4. Proposition 21. If π is a µMALL ω preproof with endsequent Γ, if π is labelled with the core fragment of the extended labelling of Definition 70, then π can be turned into a µMALL proof of Γ.Proof. As for Theorem 5, it is enough, in order to turn a labelled formula into an unlabelled one, to translate the ν connectives, leaving all other connectives untouched.The translation of Definition 68 is adapted using Definition 71 and picking, for Γ (a) , the context of the rule (Rec(a)).

  Figure 5.4. Derivability of (LWk(Γ+)) e , ( (Γ)) e , (LWk(Γ-)) e and (Rec (Γ)) e

  Figure 5.5, by expanding every formula as explained above, and by replacing every rule dealing with labels with an appropriate derivation, while leaving untouched the structure of rules not dealing with labels. The result is presented on Figure 5.6a, in an abbreviated form, showing the similarity with the original proof. The left premise of the bottommost (&) of the finitization of π ∞ is fully expanded on Figure 5.7, the two premises of the topmost (&)

FF

  for the interleaving example of Figure5.3, of the isomorphismA[νXB[A[X]]] νXA[B[X]](5.1)to turn an almost-ν-formula into a real one. Let us apply that again.The formulaI `J is equal to L [K] where L [Y ] := I [Y ] `J [Y ], that is: I `J = L [νY I [Y ]].In order to apply an isomorphism of the form (5.1) we would likeI [Y ] to be of the form M [L [Y ]] for a given M . This is unfortunately not the case asI [Y ] is a subformula of L [Y ]. However, a careful examination of the flow of I, J and K along the loops of π ∞ makes apparent the fact thatI [Y ] = µZ((Z `J [Y ]) ⊕ ⊥) µ_((I [Y ] `J [Y ]) ⊕ ⊥) = M [L [Y ]] `G, H b-, I -, J - (ν)(⊕ 1 )(⊥) F `G, G, H b-, I -, J - ( (c)) F, G, H, I [K c+ ], J [K c+ ] `G, G, H, I + , J - (LWk(a-))F `G, G a-, H, I + , J -( (a))F, G a+ , H, I + , J - (ν)(⊕ 0 )

FF

  Figure 5.5. Labelling of π ∞ . We use the following abbreviations:I -= I [K c-], I + = I [K c+ ], J -= J [K c-] and J + = J [K c+ ].

F

  G) & (F `H), G a-, H, I c+ , J - (µ) F , G a-, H, I c+ , J - (Rec(a)) F, G, H, I c+ , J - `H, G, H, I -, J - (LWk(b-)) F `H, G, H b-, I -, J - (&) (F `G) & (F `H), G, H b-, I -, J - (µ) F , G, H b-, I -, J - (Rec(b)) F, G, H, I -, J - (Rec(c)) F, G, H, I [K], J [K](a) Finitization of π ∞ . Brackets • e shoud be put around every formula and rule name. They were omitted only for the sake of readability.

F

  Figure 5.7. Left premise of the bottommost (&) of the finitization of π ∞

FF

  Figure 5.8. Left premise of the topmost (&) of the finitization of π ∞

Finitization

  of circular proofs has been recently a very active topic with much research effort on solving Brotherston-Simpson's conjecture. The following recent contributions were made in the setting of Martin-Löf's inductive definitions: firstly, Berardi and Tatsuta [2017b] proved that, in general, the equivalence is false by providing a counter-example inspired by the Hydra paradox. Secondly, Simpson [2017] on the one hand and Berardi and Tatsuta [2017a] on the other hand provided a positive answer in the restricted frameworks when the proof system contains arithmetics. While Simpson used tools from reverse mathematics and internalized circular proofs in ACA 0 , a fragment of second-order arithmetic with a comprehension axiom on arithmetical statements, Tatsuta and Berardi proved an equivalent result by a direct proof translation relying on an arithmetical version of the Ramsey and Podelsky-Rybalchenko theorems.

  Definition 30 (G out thread , thread graph of a preproof). Let (π, back) be a µMALL ω b.e.tree preproof. Its thread graph is the graph G out thread defined as follows. The vertices of G out thread are the positions of formulas in the closed sequents of π. For each inference I with conclusion s in π, for each premise s of I and for each position of formula β in s which has an immediate descendent α in s, there is an edge in G out thread , from α to β if s is a closed position of sequent in π, and from α to the position of the formula corresponding to β in back(s ) if s is an open position of sequent in π.

Definition 31 (thread). A thread in a b.e.-tree preproof is simply a path (finite or infinite) in G out thread . Example 8. Let us denote by {α, β, γ, δ, , ζ, η, θ, ι, κ, λ, ξ} the vertices of G out thread for the preproof shown on Example 6, as indicated here:

  The images, by the morphism of Definition 32, of the threads of Example 8 are, with the notations of Example 6:

	Example 9.
	Definition 32 (U : G out thread → G branch ). For any b.e.-tree preproof, there is an obvious
	graph morphism from G out thread to G branch , associating to every position of a formula the
	sequent position it belongs to. We denote this graph morphism by U. If t is a path in
	G out thread (i. e. an outer thread), we will also denote by U(t) the corresponding path in
	G branch .

  tree preproof, we define inf(t) = {A ∈ Fml | ∀n 0 ∈ N, ∃n n 0 , s n is principal and fml(s n ) = A} i. e. the set of formulas that are infinitely often principal in t.

Definition 34

(Valid thread)

. An infinite thread t is valid if inf(t) has a minimum, with respect to the subformula ordering, and this minimum is a ν-formula.

  in thread , inner thread graph of a preproof). Let (π, back) be a µMALL ω b.e.-tree preproof. Its inner thread graph is the graph G in thread defined as follows. The vertices of G in thread are the positions of ν-subformulas in the closed sequents of π. For

each inference I with conclusion s in π, for each premise s of I, for each position of formula β 0 in s which has an immediate descendent α 0 in s and for each position of

ν-subformula β in β 0 , whose image in α 0 is denoted α, there is an edge in G in thread , from α to β if s is a closed

position of sequent in π, and from α to the position of the subformula corresponding to β in back(s ) if s is an open position of sequent in π. Definition 37 (Inner thread). An inner thread in a b.e.-tree preproof is simply a path (finite or infinite) in G in thread . Example 13. Let us denote by {o, π, ρ, σ, τ, υ, φ, χ, ψ} the vertices of G in thread for the preproof shown on Example 6, as indicated here:

  it belongs to. We denote this graph morphism by out. If t is a path in G in thread (i. e. an inner thread), we will also denote by out(t) the corresponding path in G out thread (i. e. the correponding thread). The images, by the morphism of Definition 38, of the inner threads of Example 13 are, with the notations of Example 8:

	position of formula Example 14.
	Definition 38 (out : G in thread → G out thread ). For any b.e.-tree preproof, there is an obvious
	graph morphism from G in thread to G out thread , associating to every position of subformula the

  Converse if t ∈ G outthread is valid, let νXA be its validating formula, let t = t 0 t 1 t 2 . . ., let i n be the sequence of all i such that t i is a principal position of νXA.If i n < i < i n+1 ,we define u i as the image of t i n+1 in t i . Then u = (u i ) i is a valid inner thread such that out(u) = t. It is easy to see that it is the only one, thanks to the following lemma.Proof. Otherwise, σXA[X] would be a subformula of A[X], which is impossible.

	Lemma 1. The positions of σXA[X] in A[σXA[X]] are exactly the positions of X in
	A[X].

valid ⇒ out(t) valid First remark that if A is a formula (i. e. closed) then the images or preimages of any of its positions along any descendent relation are still positions of A. Now, if t = (s n ) n∈N is an inner thread, let us denote by fml(t) = fml(s 0 ).

Then ∀n ∈ N, fml(s n ) = fml(t). Because t is valid, this fml(t) is a ν-formula.

Each sequent position at which t is principal is also a position at which fml(t) is principal in out(t), fml(t), hence fml(t) is infinitely principal in out(t). Finally, fml(t) is the smallest formula of out(t) because it is a subformula of every formula of out(t). Conclusion: out(t) is a valid infinite thread.

Example 16. The preproof of Example 6 is a proof:

  Polynomial-time many-one reduction). A polynomial-time many-one reduction from a language B to a language A is a program f which runs in polynomial time and such that ∀x, x ∈ B ⇔ f (x) ∈ A. If such a program exist, we say that B reduces to A and we denote it by B A.

	1.
	P EXP
	Definition 46 (

Definition 47. A problem A is PSPACE-complete if A is in PSPACE and every PSPACE problem reduces to A. Equivalently, A is PSPACE-complete iff. ∀B, B ∈ PSPACE ⇔ B A Proposition 7.

  Definition 66. A µMALL ω b.e.-tree preproof is strongly valid if all its back edges are strongly valid. Γ of a ν-rule in π and a path u in the subgraph above this ν-rule, going down, from the source of a back edge targetting this ν-rule, to the ν-rule itself, ending by this ν-rule. u has then premise and conclusion equal to νXA[X], Γ. Let us denote by L a validating set of this (ν) rule occurrence, and let us denote by t the maximal thread going down in u starting from the main νXA[X] in its premise. This occurrence of νXA[X] is in L, because L is a validating set. Then, because L is downward closed, all vertices of t are in L. Therefore the lowest vertex of t, which is a position in the νXA[X], Γ conclusion of the considered ν-rule, or ⊥, is also in L. But in this last sequent occurrence, the only position that is in L is the one of the main νXA[X], which is consequently the end point of t. (=⇒) Conversely, let us consider an occurrence (r) of a (ν) rule in π, whose conclusion has the form νXA[X], Γ, and let us assume that it has no validating set. By Proposition 15, there is a path v in G r with source s ∈ S r and target t ∈ T r . Let u be the corresponding path in G branch . By definition of T r (Definition 63), t is in the source of a back edge e

	(⇐=) Let us assume that π has a validating set. Let us consider one occurrence
	A[νXA[X]], Γ
	νXA[X],	(ν)
	Proposition 18. A µMALL ω b.e.-tree preproof π is strongly valid iff. it is the erasing
	of a µMALL lab proof.
	Proof. We will use our first characterization by validating sets (Proposition 16) and
	prove that a µMALL ω b.e.-tree preproof π is strongly valid iff. every ν-rule of π has a
	validating set.

This small abuse of notation is nothing more than the usual set-theoretic convention of identifying an integer (or an ordinal) with the set of integers (or ordinals) that are smaller than it: n = {m | m < n}

We use the usual set-theoretic convention that an ordinal is equal to the set of ordinals strictly below it: α = {β ∈ Ord | β < α}

Recall that t(u) and T(u) are defined in Definition 40, p. 48.

Lemma 5. The language L(A thread ) is the set of valid infinite branches of .

From these two lemmas it is immediate that Proposition 8. We have the inclusion L(A thread ) ⊆ L(A branch ) and the preproof is valid iff. this inclusion is an equality.

Deciding this equality can be done in PSPACE (c. f. Theorem 3), and the constructions of these automata are obviously PSPACE, so:

Proposition 9. The problem of deciding whether a µMALL ω b.e.-tree preproof is valid is in PSPACE.

PSPACE-completeness

Outline of the PSPACE-completeness proof

We now aim at proving that the problem of deciding the validity of a µMALL ω b.e.-tree preproof is PSPACE-complete. As it is already known that this problem is in PSPACE, it remains to prove that it is PSPACE-hard.

We follow the same methodology as Lee, Jones, and Ben-Amram [2001]: in order to prove that deciding size-change termination is PSPACE-complete, they define a notion of boolean program (see Definition 48) and use the fact that the following problem is PSPACE-complete: We try to adapt their method by reducing B to Π(µMALL ω ).

Definition of the reduction

We use the boolean programs that were defined in Definition 48. The following definition will be used in the proof of Proposition 10:

the Cyclist prover for instance. In such systems, validity checking does not seem to be the bottleneck in circular proof construction as compared with the complexity that is inherent to exploring and backtracking in the search tree [START_REF] Brotherston | A generic cyclic theorem prover[END_REF][START_REF] Reuben | Automatic cyclic termination proofs for recursive procedures in separation logic[END_REF][START_REF] Tellez | Automatically verifying temporal properties of pointer programs with cyclic proof[END_REF].

Our work suggests deep connections between thread-validity and SCT that we only touched upon in the previous section. This confirms connections previously hinted by other authors [START_REF] Dax | A proof system for the linear time µcalculus[END_REF][START_REF] Hyvernat | The size-change termination principle for constructor based languages[END_REF][START_REF] Hyvernat | The size-change principle for mixed inductive and coinductive types[END_REF][START_REF] Lepigre | Practical subtyping for curry-style languages[END_REF] that we plan to investigate further in the future.

Finite representations of circular L-proofs.

We now turn our attention to finite representations of (circular) L-proofs. Immediately a difficulty occurs in comparison to non-labelled proofs: whereas an infinite non-labelled proof may happen to be regular, a valid L-proof cannot be circular, because along every infinite branch, the sets of labels will grow endlessly. To form circular proofs with labels, some atoms must be forgotten when going bottom-up.

We introduce two more rules: ( (a)) and (LWk). The first one allows to forget one atom, just before recreating it by means of a back edge to an already encountered ν-rule. The other one allows to forget any atom that will not be used to validate the proof. It is used to synchronise the different labels in a sequent before travelling through a back edge.

• labelled back edge:

with the constraint that it must be the source of a back edge to the conclusion of a

• labelled weakening: Proof. Every rule of the labelled µMALL lab proof is sent by • to a valid rule of unlabelled µMALL ω , except for the (LWk) rule, which can safely be removed:

Definition 60 (µMALL ). We denote by µMALL the set of b.e.-tree preproofs that are obtained from µMALL lab by label-erasing. This is a subset of all µMALL ω b.e.-tree preproofs.

Proposition 13 (µMALL ⊆ µMALL ω ). Every preproof of µMALL ω that is the image of a proof in µMALL lab by label-erasing satisfies thread validity.

We immediately give a proof sketch of this proposition; we then prove the two Lemmas 8 and 9 before giving a full proof of Proposition 13.

Proof sketch of Proposition 13. Consider a preproof π in µMALL which is the image of an L-proof π in µMALL lab and an infinite branch b in π . We want to prove that b contains a valid thread (see Definition 21). Let b 0 be the corresponding infinite L-branch in π. We remark (Lemma 8) that there is a sequent S 0 which is the lowest target of back edge crossed infinitely often by b 0 . Besides, S 0 is the conclusion of a (ν b (a)) rule, which unfolds some ν L XA.

We decompose b 0 , with root r; S 0 conclusion of (ν b (a)) and ν L XA at position p 0 in S 0 ; for any i ≥ 1, S i conclusion of a back edge ( (a)) with ν L,a XA at position p i in S i . Then we notice that T(u i )(p 0 ) (Definition 40) is a thread (S 0 , p 0 ) * -→(S i , p i ) which is progressing, as its source is the principal conclusion of the rule (ν b (a)). By concatenating the T(u i )(p 0 )

and then erasing labels, we get a valid thread of b in π .

S i

Lemma 8. Let b be an infinite branch in a b.e.-tree preproof, i.e. an infinite ascending path in its branch graph, starting from the root.

Then there is an occurrence of sequent in this b.e.-tree preproof, i. e. a vertex s in its branch graph, which is the lowest one infinitely appearing on b.

Moreover, this occurrence of sequent (this vertex) is the target of a back edge.

Proof. This is essentially a graph-theoretic property, which does not rely on the logical content of the proof.

The crucial fact to notice is that, in general, in a tree, if S is a non empty, finite set of vertices that is connected for the relation of comparability, that is if ∀v, v ∈ S, v v or v v, then S has a minimum. This is proved by induction on the cardinal of S.

Take then for S the set of vertices occurring infinitely often on the branch b. It is a connected subgraph of G branch . Because of that, it is connected for comparability in the tree: if s 0 → s 1 in an edge in S then either it is induced by a logical inference, in which case s 0 is below s 1 , or it is induced by a back edge, in which case s 1 is below s 0 .

We can then apply the previous remark to S, and we obtain a vertex s, which is the lowest position of sequent infinitely appearing on b.

In particular, because s appears infinitely often on b, there must be another position s 0 in S and an edge s 0 → s. Because s is the lowest position in S, this edge must be induced by a back edge. Hence s is a target of back edge.

Lemma 9 (Follow-up of labels). If u is a path in the branch graph of a µMALL lab proof, if u does not cross the rule (ν b (a)), and if p is a position in the target sequent of u (its top sequent) that is labelled with a, then t(u)(p) (Definition 40) is defined and is a position labelled with a in the source sequent of u (its bottom sequent).

Proof. This is quite straightforward, by induction on the length of u, and by looking at the first (or the last) rule crossed by u. We use notably the fact that, when the induced thread T(u)(p) is followed top-down, the label a cannot be erased because we do not cross (Rec(a)) and the thread cannot reach a cut-formula because cut-formulas do not contain labels.

Proof of Proposition 13. Suppose π is a µMALL lab proof.

• Let π be its erasure. π is thus a µMALL ω b.e.-tree preproof.

• Suppose b an infinite branch of π , that is an infinite ascending path in the b.e.-tree π , starting from the root.

Given a µMALL ω b.e.-tree preproof, we will define a graph G π very similar to G in thread . In G in thread , we consider only positions of subformulas in closed sequents, and the positions of subformulas in a source of back edge, which is an open sequent, are identified to those in the target of that back edge. In contrast, in G π , we consider the positions in sources of back edges as distinct from the corresponding positions in their targets. The aim of G π is precisely to see how we can connect those positions through paths in the graph.

Definition 62 (G π ). Given a µMALL ω b.e.-tree preproof π, we define G π to be the following graph:

• its vertices are all positions of ν-formulas in all occurrences of sequents in π, plus the vertex ⊥:

• for its edges: for every position p of a ν-subformula, if q is its image in the sequent just below, as defined by the threading structure of the preproof, then there is an edge q -→ p in G π . Moreover, for every position p of a ν-subformula of a cut formula, there is an edge ⊥ -→ p.

We illustrate the construction of the edges of the graph defined in definition 62 with

the following examples in which we have indexed the apparent ν-formulas by numbers representing vertices of the graph:

induces edges 4 → 1, 5 → 2 and 6 → 3, and

thread criterion or the loop criterion, the validity of a proof in µMALL lab is a purely local property, which can be checked in linear time.

We proved in Propositions 16 and 18 that the b.e.-tree preproof obtained by erasing the labels of a µMALL lab proof is valid for the loop criterion and, conversely, that any circular representation that is valid for the loop criterion can be turned into a proof of µMALL lab by labelling some of its formulas.

We made that last property explicit by providing a procedure to check a circular representation with respect to the loop criterion and to turn it into a labelled proof of µMALL lab when it is valid. This algorithm runs in quadratic time.

Now that we have identified a fragment of µMALL ω which proves at least all sequents provables in µMALL, it is natural to wonder whether it proves strictly more than µMALL.

This question is the subject of the next and final chapter of this thesis. also provable in µMALL ω .

This allows us to split the problem of finitization into two subproblems:

• If a conclusion is provable in µMALL ω , is it already provable in µMALL ?

• If a conclusion is provable in µMALL , is it already provable in µMALL?

A positive answer to both questions would mean that finitization is possible and the Brotherston-Simpson conjecture is true for µMALL and µMALL ω .

In this chapter, we answer positively the second question: we prove that any conclusion provable in µMALL is already provable in µMALL. We do so by providing an explicit method which takes as input a circular representation of preproof, valid for the loop criterion, and output a standard, finitary µMALL proof.

On Brotherston-Simpson's conjecture: finitizing circular proofs

The aim of this section is to prove a converse of Proposition 14: Every provable sequent of µMALL is provable in µMALL.

This will be proved by defining a translation from every µMALL proof of a sequent Γ containing no label variable into a µMALL proof of the same sequent.

Let us consider a µMALL proof π. Up to renaming of bound variables, we can assume that all (ν b ) rules are labelled by distinct labels. For every two labels a and b occurring in π, we say that a b whenever (ν b (a)) is under (ν b (b)). This order is well-founded because finite.

Definition 67 (Context associated to a labelling atom). For every rule

we define Γ (a) to be Γ.

We now define 1. for each atom a a sequent Γ a formed of non-labelled formulas;

Relaxing the labelling of proofs

In this section, we define an extension of the labelling defined in Section 4.2, with the following properties:

• it allows to label more µMALL ω b.e.-tree-preproofs than the labelling of Section 4.2,

• it still ensures thread-validity,

• the validity of a labelled proof amounts to the local validity of each inference,

• to some extent, it preserves the ability to finitize circular proofs.

In order to motivate this extension, we shall consider two examples. The first one is the proof π ∞ , which is on Figure 5.2, and on which we will come back later. The second one, that we will present now, has been chosen to be simpler than π ∞ .

Example 17. Let D be an arbitrary formula. Lists of D can be represented as proofs of

and it is possible to encode in µMALL ω the function taking two lists and computing the tree of all their possible interleavings, as a proof with conclusion 1 L 0 , L 0 T 0 , where

1 In the following, we write A B for A ⊥ `B, and Γ ∆ for Γ ⊥ , ∆.

103 2. in our previous setting, back edges must target (ν) rules, which is not the case here.

Both difficulties have, in fact, the same origin, namely that in our previous setting the (ν) rule has two roles: being the target of a back edge and ensuring thread progression.

Both difficulties also have the same solution: dissociating these two roles. We therefore introduce, in Definition 69, a new rule (Rec), whose only effect is to allow its premise to be the target of a back edge, and to introduce a new label. Since (Rec) is disentangled from greatest fixed point unfolding, the labelling must account for the progression of a thread. That is why every atomic label is now given in one of two modes: a passive mode (a-) and an active one (a+). Only an unfolding by a (ν) can turn ainto a +.

Let us now turn back to our introductory example: π ∞ (Figure 5.2). For that example, separating the introduction of back edges and the coinductive progress is not enough to be able to label π ∞ in a way that certify its thread validity. Indeed, since targets of back edges do not require to unfold a ν, there is a priori no reason to require that the sequents contain some ν-formula. While this is slightly hidden in the interleaving example of Figure 5.3, π ∞ gives a clear example of this phenomenon and suggests that the (Rec)

inference should have the ability to add labels deeply in the sequent, that is not only on the topmost ν fixed-points, but also to greatest fixed points occurring under some other connectives. The same remark applies to the back edge rule since its conclusion sequents have the same structure as those of (Rec).

Driven by these observations, we now define a new labelling of circular preproofs and prove its correctness with respect to thread-validity.

Definition 69 (Extended labelling). Labelled formulas are built on the same grammar as in Definition 56, except that labels are lists of signed variables, that is of pairs of a variable and a symbol in {+, -}. Derivations are built with µMALL inferences plus the following rules:

and the constraints that:

• a cut-formula cannot contain a non-empty label;

• all (Rec) rules must wear distinct variables;

• every (Rec(a)) rule must have at least one occurrence of "a-" in its premise;

• each

via a back edge. This implies in particular that this ( (a)) must be above this (Rec(a))

and that the premise of this (Rec(a)) must be the same sequent as the conclusion of this ( (a)) except for the change of sign of a, at every of its occurrences in the sequent.

With the extended labelling of Definition 69, we have the following.

Proposition 19 (Soundness of extended labelling). If π is an extended labelled circular representation then π is a valid µMALL ω b.e.-tree proof.

Proof. First remark that Lemma 9, as it is stated on p. 87, still holds for this extended labelling. The proof is the same, keeping in mind to replace every mention of (ν b (a)) with

(Rec(a)). As for Proposition 13, the proof of this proposition crucially relies on it.

Suppose π is a labelled circular representation. Let π be its erasure. Remark that the positions labelled by a are the same in all S i , as there are back edges from every S i+1 to S 0 . The difference, however, is that these positions are labelled with a-in S 0 and with a+ in every S i+1 . Let P 0 be the set of those positions. P 0 is finite and non empty. Now we would like, as in the proof of Proposition 13, to construct an infinite thread along b 0 . However, because P 0 may contain more than one element, we cannot know by advance, for each S i , which p ∈ P 0 will support an infinite thread. Thus, we will use Kőnig's lemma to show the existence of such a thread. Let T 0 be the tree whose vertices are the pairs (i, p) where 1 i < ω and p ∈ P 0 , whose roots are the vertices of the form (1, p) and where, for i > 1, the father of (i, p) is 2 (i -1, t(u i )(p)). Here we have to prove that t(u i )(p) is defined and that it belongs to P 0 for every i and p ∈ P 0 . This is ensured by Lemma 9 thanks to the labels.

Remark that every edge in T 0 induces a progressing thread. Indeed, for i 1 and p ∈ P 0 : comes directly from the validity of each rule. Over all that, going from a labelled proof to an unlabelled one is immediate, and checking and labelling an unlabelled preproof is doable in quadratic time.

• The finitization results of Chapter 5 do not only tell that the different fragments of µMALL ω studied in Chapter 4 and in Section 5.2 do not have more expressivity than µMALL. These are constructive results, providing an explicite method to synthetize induction and coinduction invariants and to turn a circular proof into a finitary, well-founded one.

Future works

Our work in Chapter 3 suggests deep connections between thread-validity and size-change termination (SCT) [START_REF] Chin | The size-change principle for program termination[END_REF], which was already hinted by other authors [START_REF] Dax | A proof system for the linear time µcalculus[END_REF][START_REF] Hyvernat | The size-change termination principle for constructor based languages[END_REF][START_REF] Hyvernat | The size-change principle for mixed inductive and coinductive types[END_REF][START_REF] Lepigre | Practical subtyping for curry-style languages[END_REF]. More generally, the connection between SCT and thread validity in µ-calculi is not yet well understood despite those early investigations. More than a connection, this looks like an interplay: size-change termination is originally shown decidable by using Büchi automata and size-change graphs can be used to show validity of circular proofs [START_REF] Dax | A proof system for the linear time µcalculus[END_REF]. There seems to be connections with our labelling system too, that we plan to investigate further in the future.

We already underlined in Section 5.5 the similarities between our system and the systems by [START_REF] Dax | A proof system for the linear time µcalculus[END_REF], [START_REF] Stirling | A tableau proof system with names for modal mu-calculus[END_REF], [START_REF] Afshari | Cut-free completeness for modal mu-calculus[END_REF]. Despite their differences, the relationships of those systems should be investigated further (in particular the role of the annotation restriction rule of Stirling [2014, Definition 4]).

In addition to investigating more closely those connections, we have several directions for improving our labelled proof system. The first task is to lift the results of Chapter 4 and Section 5.1 to the extended labelling system of Section 5.2. Indeed, for the more restricted fragment and given a circular proof presented as a graph with back edges, we provided a method to effectively check that one can assign labels. It is therefore natural to expect extending these results to the relaxed framework. Another point we plan to investigate is whether every circular µMALL proof can be labelled. Even though this can look paradoxical given the complexity of checking validity of circular proofs, one should keep in mind that it might well be the case that, in order to label a circular proof presented as a tree with back edges, one has to unfold some of the back edges, or possibly pick a different finite representation of the proof which may result in a space blow up.

Related to this question is the connection of our labelling methods with size-change termination methods. Indeed, in designing the extended labelling, one gets closer to the kind of constructions one finds in SCT-based approaches: this should be investigated