David Baelde
email: david.baelde@irisa.fr

Amina Doumane
email: amina.doumane@ens-lyon.fr

Denis Kuperberg
email: denis.kuperberg@ens-lyon.fr

Alexis Saurin
email: alexis.saurin@irif.fr

Bouncing threads for circular and non-wellfounded proofs Towards compositionality with circular proofs

Keywords: Circular Proofs, Linear Logic, Cut Elimination, Decidability, Curry-Howard, Fixed points Cons : ( nat * Stream) → Stream. CoFixpoint drop (s : Stream) : Stream := match s with | Cons ( a, Cons BStream) → BStream

Given that (co)inductive types are naturally modelled as fixed points, it is unsurprising that fixed-point logics are of interest in the study of programming languages, via the Curry-Howard (or proofs-as-programs) correspondence. This motivates investigations of the structural proof-theory of fixedpoint logics and of their cut-elimination procedures.

Among the various approaches to proofs in fixed-point logics, circular -or cyclic -proofs, are of interest in this regard but suffer from a number of limitations, most notably from a quite restricted use of cuts. Indeed, the validity condition which ensures soundness of non-wellfounded derivations and productivity of their cut-elimination prevents some computationally-relevant patterns of cuts. As a result, traditional circular proofs cannot serve as a basis for a theory of (co)recursive programming by lack of compositionality: there are not enough circular proofs and they compose badly.

The present paper addresses some of these limitations by developing the circular and non-wellfounded proof-theory of multiplicative additive linear logic with fixed points (µMALL) beyond the scope of the seminal works of Santocanale and Fortier and of Baelde et al. We define bouncing-validity: a new, generalized, validity criterion for µMALL ∞ , which takes axioms and cuts into account. We show soundness and cut elimination theorems for bouncing-valid non-wellfounded proofs: as a result, even though bouncing-validity proves the same sequents (or judgments) as before, we have many more valid proofs at our disposal. We illustrate the computational relevance of bouncing-validity on a number of examples. Finally, we study the decidability of the criterion in the circular case: we prove it is undecidable in general but identify a hierarchy of decidable sub-criteria.

Introduction

Fixed points in computer science Fixed-point theory has proved to be a valuable tool in computer science, in particular for reasoning formally about software systems. Its explicit uses may be traced back to the first formal semantics of programming languages in the late 1960s [START_REF] Sangiorgi | On the origins of bisimulation and coinduction[END_REF] and it is now pervasive in programming language semantics, concurrency, automata theory and software verification techniques. As part of the increasing use of fixed points in computer science, logics featuring fixed points, generally referred to as µ-calculi, were developed and studied [START_REF] Kozen | Results on the Propositional mu-Calculus[END_REF][START_REF] Vaughan R Pratt | A decidable mu-calculus: Preliminary report[END_REF]. Decades later, fixed points are used in various specification languages, e.g. to specify temporal or spatial properties of program executions. Fixed points are also present in most programming languages as recursive types. More interestingly, the Curry-Howard correspondence, which allows to view proofs as programs and formulas as types, has been extended in various ways to encompass fixed-point types, e.g. in System F extended with least and greatest fixed point types [START_REF] Matthes | Monotone Fixed-Point Types and Strong Normalization[END_REF][START_REF] Mendler | Inductive Types and Type Constraints in the Second Order Lambda Calculus[END_REF], in Coq's calculus of (co)inductive constructions [START_REF] Giménez | Structural Recursive Definitions in Type Theory[END_REF], and in functional reactive programming types [START_REF] Cave | Fair Reactive Programming[END_REF].

Fixed-point logics and proofs. Proof systems for fixed point logics can naturally be obtained by taking (co)induction rules that closely reflect fixed point theorems, e.g. Knaster-Tarski's characterization of least fixed points as least pre-fixed points. This is the basis for Kozen's famous axiomatization [START_REF] Kozen | Results on the Propositional mu-Calculus[END_REF] of the µ-calculus and for other proof-systems [START_REF] Baelde | Least and greatest fixed points in linear logic[END_REF]. When building proofs for such logics, one must identify (co)invariants which may be significantly more complex than the property to establish -a phenomenon encountered by students learning to prove properties by induction on natural numbers.

An alternative to these explicit (co)induction rules is to consider proof systems featuring non-wellfounded derivation trees: this makes it possible to reason on fixed points . The system would be unsound if this derivation were declared valid for both σ = ν and σ = µ as the empty sequent could be derived thanks to the cut rule (least and greatest fixed points are logically dual of each other). However, the derivation when σ = ν should be accepted since νX .X ≡ ⊤ (a tautology).

In the case of arithmetic, this style of reasoning is akin to proofs by infinite descent rather than by induction, and has been formally studied in infinitary sequent calculus by Brotherston and Simpson [START_REF] Brotherston | Sequent calculi for induction and infinite descent[END_REF]. For propositional µ-calculus, several such infinitary deduction systems have been proposed [START_REF] Dax | A Proof System for the Linear Time µ-Calculus[END_REF][START_REF] Janin | Automata for the Modal mu-Calculus and related Results[END_REF][START_REF] Kozen | Results on the Propositional mu-Calculus[END_REF][START_REF] Streett | An Automata Theoretic Decision Procedure for the Propositional Mu-Calculus[END_REF]. Because they are easier to work with than the finitary proof systems (or axiomatizations) based on Kozen-Park (co)induction schemes, they are often found in completeness arguments for such finitary systems [START_REF] Doumane | Towards Completeness via Proof Search in the Linear Time µ-calculus: The case of Büchi inclusions[END_REF][START_REF] Kaivola | Axiomatising Linear Time Mu-calculus[END_REF][START_REF] Kozen | Results on the Propositional mu-Calculus[END_REF][START_REF] Walukiewicz | On Completeness of the mu-calculus[END_REF][START_REF] Walukiewicz | Completeness of Kozen's Axiomatisation of the Propositional mu-Calculus[END_REF][START_REF] Walukiewicz | Completeness of Kozen's Axiomatisation of the Propositional mu-Calculus[END_REF]. They are also better suited for automated reasoning [START_REF] Dax | A Proof System for the Linear Time µ-Calculus[END_REF][START_REF] Streett | An Automata Theoretic Decision Procedure for the Propositional Mu-Calculus[END_REF]. Among non-wellfounded proofs, regular derivation trees play a particular role. Such proofs, that we call circular, can be represented by a finite tree with back-edges: they can be easily finitely represented and algorithmically processed. As such, they have found many applications 1 .

Fixed-points in types. On the other end of the Curry-Howard correspondence, one finds programming languages equipped with (co)recursion constructs whose typing naturally reflects the Kozen-Park (co)induction rules [START_REF] Cave | Fair Reactive Programming[END_REF][START_REF] Mendler | Inductive Types and Type Constraints in the Second Order Lambda Calculus[END_REF]. Writing programs in these systems may be difficult, as it involves coming up with complex (co)invariants. These difficulties are only partially lifted through the use of guarded (co)recursion [START_REF] Giménez | Structural Recursive Definitions in Type Theory[END_REF] or sized types [START_REF] Abel | Mixed inductive/coinductive types and strong normalization[END_REF] in Coq or Agda respectively. Furthermore, (co)recursion involves a suspended computation which makes it difficult to analyze the behavior of a program.

In particular, retrictions such as Coq's guard condition results in a serious lack of compositionality properties as well known and analyzed by various authors [START_REF] Abel | Compositional Coinduction with Sized Types[END_REF][START_REF] Abel | Well-founded recursion with copatterns and sized types[END_REF][START_REF] Bertot | Interactive Theorem Proving and Program Development -Coq'Art: The Calculus of Inductive Constructions[END_REF][START_REF] Giménez | Structural Recursive Definitions in Type Theory[END_REF]. As an illustration, we show in Fig. 1 some example of Coq coinductive terms drop, incdrop and filter1everyk. While all are productive coinductive terms, only the first two are valid Coq terms, the third one does not pass the guard condition: 1) drop filters one elements every two of its input stream; 1 For instance using circular proofs [START_REF] Santocanale | A Calculus of Circular Proofs and Its Categorical Semantics[END_REF] as a system for representing morphisms in µ-bicomplete categories [START_REF] Santocanale | µ-Bicomplete Categories and Parity Games[END_REF][START_REF] Santocanale | Free µ-lattices[END_REF], to study the relationship between induction and infinite descent in first-order arithmetic [START_REF] Brotherston | Sequent calculi for induction and infinite descent[END_REF], to generate invariants for program verification in separation logic [START_REF] Brotherston | Cyclic Abduction of Inductively Defined Safety and Termination Preconditions[END_REF], or as an intermediate between ludics' designs and proofs in linear logic with fixed points [START_REF] Baelde | Least and Greatest Fixed Points in Ludics[END_REF].

2) incdrop takes an input stream of nats and filters one element every two, incrementing it; 3) filter1everyk's behaviour depends on a natural number k: it takes an input streams of booleans and filters one element out of k and returning, depending on the parity of k, either the chosen elements or their negation.

As an alternative, one could naturally consider infinitary (or circular) programs, equipped with a global validity condition ensuring that they behave well -in particular that they are terminating, or productive for inhabitants of coinductive types. There is surprisingly little work following this approach. We note the work of Hyvernat [START_REF] Hyvernat | The Size-Change Termination Principle for Constructor Based Languages[END_REF] whose use of size-change termination can be seen as a form of validity checking: it would be interesting to develop this work from a Curry-Howard perspective to compare it with infinitary proof systems. and foundations are missing.

This can be understood from the fact that the aforementioned infinitary proof systems for fixed point logics are all cut-free; hence, the role of the validity condition in (syntactic) cut-elimination remains unclear from these works. This shortcoming has been addressed first by Santocanale and Fortier: in [START_REF] Fortier | Cuts for circular proofs: semantics and cut-elimination[END_REF] they consider an infinitary sequent calculus for purely additive logic, featuring cuts and an extended notion of validity, and they show that cuts can be eliminated from valid proofs (in that setting, cut-elimination is not terminating but productive, and converges to a valid cut-free derivation). A key insight of this work is that the validity condition ensures both soundness of the infinitary proof system and productivity of cut-elimination. The result has been generalized later to the multiplicative and additive linear logic with fixed points, µMALL, at the cost of a more complex argument, by Baelde et al. [START_REF] Baelde | Infinitary Proof Theory: the Multiplicative Additive Case[END_REF]. Through these syntactic cut-elimination results, infinitary proofs for µMALL are given a computational content, which is an important step towards a Curry-Howard correspondence for that logic.

Lack of compositionality of circular proofs. Unfortunately, existing notions of validity impose a quite limited use of cuts in non-wellfounded proofs rejecting many proofs that could be accepted as valid. In particular, this prevents writing circular proofs in a compositional manner, as exemplified in the following (supported by Figure 2): Example 1.1. Consider formulas N = µX .1 ⊕ X and S = νY .N ⊗ Y encoding natural numbers and streams of natural numbers in µMALL. Indeed, in a typed language/proof assistant such as Coq, these definitions would correspond to the following constructs: These examples correspond (at a somehow informal level) to the Coq coinductive terms drop and incdrop of Fig. 1. The computational interpretation of the left-hand derivation is that of a function from streams of nats to streams of nats which drops its elements in odd position, keeping half of its elements only 3 . The rightmost proof has a slightly different computational interpretation: it drops one element every two but also increments the other element that is returned in the output stream. This is achieved by using a cut in the proof, depicted in the box, which corresponds to hdinc and does the increment. Although both proofs are productive when they are cut with streams of nats, only the leftmost proof is valid for [START_REF] Baelde | Infinitary Proof Theory: the Multiplicative Additive Case[END_REF] (up to axiom expansion): the rightmost proof has no valid thread inhabiting the infinite branch because of the cut with the boxed sub-proof occurring in a cycle.

Towards bouncing threads. This paper improves the compositionality of circular proofs, contributing to a line of research aiming at providing and analyzing the computational content of circular proofs. From the Curry-Howard perspective, considering more relaxed validity criteria is an interesting and important challenge as more circular proofs means more flexibility to write valid programs on coinductive types.

Indeed, while the previous related cut-elimination results [START_REF] Baelde | Infinitary Proof Theory: the Multiplicative Additive Case[END_REF][START_REF] Fortier | Cuts for circular proofs: semantics and cut-elimination[END_REF] were significant steps, they suffered from strong restrictions on the use of cuts along non-wellfounded branches (or cycles in proofs) as described above. We introduce here a new validity condition for µMALL ∞ , the infinitary proof system for MALL with fixed points. Taking inspiration from Geometry of Interaction [START_REF] Girard | Towards a Geometry of Interaction[END_REF], this criterion generalizes the existing one by enriching the structure of threads: bouncing threads can leave the branch they validate and "bounce" (i.e. change direction, moving upward but also downward along proof branches) on axioms and cut rules.

The circular derivation π 0 shown below illustrates the intuitive idea behind validation by bouncing threads: it is not valid according to straight threads since its only infinite branch contains no infinite thread at all, but it will be bouncing-valid (or "b-valid"). Remark that one can trace the coinductive progress by following νX .X upwards and µX .X downwards while changing directions and moving from a formula to its dual when reaching axioms and cuts. This is formalized by the bouncing thread represented in red. Indeed, after reducing twice the cut in each repetition of the cycle, it yields a cut-free proof which is validated by a (straight) thread, which can be viewed as the "straightened" version of the above mentioned bouncing thread:

π 0 = (Ax) ⊢ νX .X , µX .X (µ) ⊢ νX .X , µX .X ⊢ νX .X (ν ) ×2 ⊢ νX .X (Cut) ⊢ νX .X → 2 cut π 0 (ν ) ⊢ νX .X → ω cut ⊢ νX .X (ν ) ⊢ νX .X
We investigate the proof-theoretic properties of this new bouncing validity criterion for µMALL ∞ pre-proofs. We prove that it guarantees soundness (Theorem 5.4) and productivity of the cut-elimination process (Theorem 5.1). The criterion is compatible with simple compositions using cuts, as shown in Example 1.1. Even when considering straight threads only, our work already extends the results of [START_REF] Baelde | Infinitary Proof Theory: the Multiplicative Additive Case[END_REF][START_REF] Fortier | Cuts for circular proofs: semantics and cut-elimination[END_REF], as we provide a treatment of both axioms and multiplicatives. Dealing with the axioms actually introduces substantial difficulties in the soundness and cut-elimination proofs.

Decidability properties of the bouncing criterion. In Theorem 6.2, we show that this new bouncing validity condition is undecidable, already in the purely multiplicative case. The proof is intricate, and works by reducing the halting problem of two-counter machines into our bouncing criterion. The strong constraints on the proof system give rise to complex gadgets to propagate relevant information about the current configuration of the machine. Moreover, the linearity of the proof system forces a "reversibility" constraint on this encoding, which can be dealt with by using the same kind of technique as Bennett [START_REF] Bennett | Logical Reversibility of Computation[END_REF] to prove Turing-completeness of reversible Turing machines: a history of the computation is produced to guarantee reversibility, then this history is erased by rewinding the computation.

Although the criterion is undecidable, we show (Theorems 6.5 and 6.6) that it can be decomposed into a hierarchy of decidable criteria, via a parameter called "height": for each fixed height k ∈ N, the "b(k)-criterion", where height is

(Ax) N ⊢ N S ⊢ S (⊗ r ) N , S ⊢ N ⊗S (⊗ l ) N ⊗S ⊢ N ⊗S (ν l ) S ⊢ N ⊗S (ν r ) S ⊢ S (WNat l ) N , S ⊢ S (⊗ l ) N ⊗S ⊢ S (ν l ) S ⊢ S (Ax) N ⊢ N S ⊢ S (⊗ r ) N , S ⊢ N ⊗S (⊗ l ) N ⊗S ⊢ N ⊗S (Ax) N ⊢ N (⊕r2), (µr) N ⊢ N (Ax) S ⊢ S (⊗l),(⊗r) N ⊗S ⊢ N ⊗S (Cut) N ⊗S ⊢ N ⊗S (ν l ) S ⊢ N ⊗S (ν r ) S ⊢ S (WNat l ) N , S ⊢ S (⊗ l ) N ⊗S ⊢ S (ν l ) S ⊢ S Figure 2.
Examples of a valid and an invalid circular pre-proof.

• cut-free valid Pre-proofs Organization of the contributions. In Section 2 we recall the basic definitions for the non-wellfounded proof system µMALL ∞ . We then define, in Section 3 the cut-elimination procedure. In Section 4, we introduce our new bouncing validity condition, and show in Section 5 that it guarantees soundness of the system and productivity of the cutelimination procedure. We finally study in Section 6 the decidability of our criterion in the multiplicative case. Omitted proofs and developments can be found in appendices.

• s-valid Pre-proofs • b(k)-valid Pre-proofs . . . • b-valid Pre-proofs • Productive Pre-proofs • Pre-proofs

The pre-proofs of µMALL ∞

In this section we introduce the multiplicative additive linear logic extended with least and greatest fixed point operators, and a system of infinitary (pre-)proofs for that logic.

φ,ψ ::= a | a ⊥ a ∈ A, (atoms) | µX .φ | νX .φ | X X ∈ V (fixed points) | ⊥ | 1 | φ ψ | φ⊗ψ (multiplicatives) | 0 | ⊤ | φ ⊕ ψ | φ ψ .
(additives)

The connectives µ and ν bind the variable X in φ. µMALL ∞formulas are those pre-formulas without free fixed point variables. The formulas of µMLL ∞ , the multiplicative fragment, are those µMALL ∞ formulas which do not contain , ⊕, ⊤ or 0 (ie. omitting the last line in the grammar).

Definition 2.2 (Negation). (_) ⊥ is the involution on formulas satisfying:

(a ⊥ ) ⊥ = a; X ⊥ = X ; (νX .φ) ⊥ = µX .φ ⊥ ; ⊥ ⊥ = 1; (φ ψ ) ⊥ = φ ⊥ ⊗ψ ⊥ ; (φ ⊕ ψ ) ⊥ = φ ⊥ ψ ⊥ .
Setting X ⊥ = X would be incorrect when considering formulas with free variables, but it yields the proper dualization for closed formulas, e.g. (µX .X ) ⊥ = νX .X . Since negation is not a connective, formulas enjoy the positivity condition by construction: all fixed-point expressions are monotonic.

There are several presentations of sequents in the literature. Considering that we are aiming at the proofs-asprogram correspondence we could take sequents as lists of formulas or as sets of occurrences of formulas 4 . Here, we make the choice of sequents as named formulas that we call formula occurrences, following [START_REF] Baelde | Infinitary Proof Theory: the Multiplicative Additive Case[END_REF].

We recall next their formal definition. A formula occurrence is the pair of a formula and an address. In a derivation, all the conclusion (and cut) formula occurrences will have pairwise distinct and incomparable addresses: this invariant will be preserved by each inference. When a rule is applied to a formula occurrence, the addresses of its sub-occurrences will be extended by {l, r, i} (standing for left, right and inside respectively) in order to record their provenance. This is of great importance for our developments: the validity criterion traces the evolution of formulas, which is completely explicit in their addresses. Definition 2.3. Let A fresh be an infinite set of atomic addresses, A ⊥ fresh = {α ⊥ at | α at ∈ A fresh }, and Σ = {l, r, i}. An address is a word of the form α at .w, where α at ∈ A fresh ∪ A ⊥ fresh and w ∈ Σ * . Let us call Addr the set of addresses. We say that α ′ is a sub-address of α when α is a prefix of α ′ , written α ⊑ α ′ . We say that α and β are disjoint when α and β are incomparable wrt. ⊑. Definition 2.4. A formula occurrence, or simply occurrence, is given by a formula φ and an address α, and written φ α . Occurrences will be denoted by F , G, H . Occurrences are disjoint when their addresses are. The occurrences φ α and ψ β are structurally equivalent, written

φ α ≡ ψ β , if φ = ψ .
A sequent is a set of disjoint occurrences.

Example 2.5.

⊢ φ α l , φ α r ,ψ β ( ) ⊢ (φ φ) α ,ψ β
is an example of an occurrencebased inference (α and β are assumed to be disjoint). Note that the relation of sub-address is the inverse of the prefix relation, which is coherent with the sub-formula relation. For instance, in the example above, φ is a sub-formula of φ φ, but its address is αr while the address of φ φ is α.

We now define the rules of linear logic with fixed points in the framework of sequents as sets of occurrences. As seen above, inferences are address-sensitive: they look at the structure of the formula underlying an occurrence, decompose it following a standard µMALL rule, then assign addresses to its subformulas in the obvious way. One can make the address implicit in the inference by defining the syntax of µMALL ∞ to operate directly on occurrences: Definition 2.6. Logical connectives are lifted to operations on occurrences as:

• For any ⋆ ∈ { , ⊗, ⊕, }, if F = φ α l and G = ψ α r then F ⋆ G = (φ ⋆ ψ ) α . • For any σ ∈ {µ, ν }, if F = φ α i then σX .F = (σX .φ) α .
Definition 2.7. We define a duality over Addr by setting (α .w) ⊥ = α ⊥ .w and (α ⊥ .w) ⊥ = α .w for all α ∈ A fresh and w ∈ Σ * . We then define (φ α ) ⊥ = (φ ⊥ ) α ⊥ , and write F ⊥G when F ⊥ = G. We define substitution over occurrences as follows:

(φ α )[ψ β /X ] = (φ[ψ /X ]) α .
We are ready to introduce our infinitary sequent calculus. Definition 2.8. A µMALL ∞ pre-proof is a possibly infinite tree, coinductively generated by the rules of Fig. 4. Given a sequent s in a pre-proof π , we denote by premiss(s) the set of sequents which are premisses of the rule of conclusion s in π . Rules other than (Ax) and (Cut) are called logical rules. For every instance of one such rule we call principal occurrence the occurrence in its conclusion sequent that is decomposed to obtain the premisses.

The infinite derivations of µMALL ∞ may be quite complex trees, possibly not even computable. In practical uses one would turn to sub-systems, typically the fragment of circular pre-proofs [START_REF] Brotherston | Sequent calculi for induction and infinite descent[END_REF][START_REF] Doumane | Towards Completeness via Proof Search in the Linear Time µ-calculus: The case of Büchi inclusions[END_REF][START_REF] Fortier | Cuts for circular proofs: semantics and cut-elimination[END_REF][START_REF] Santocanale | A Calculus of Circular Proofs and Its Categorical Semantics[END_REF]. In a nutshell, a circular derivation is an infinite derivation which has only finitely many distinct sub-trees up to renaming of addresses [START_REF] Doumane | Théorie de la démonstration infinitaire pour les logiques à points fixes)[END_REF].

Notation 1 (Two-sided notation). While it is proof-theoretically convenient to work with one-sided sequents as in the previous definition, it is more illuminating for some examples, especially when aiming at illustrating the computational interpretation of some proofs, to allow to use the usual two-sided sequent calculi. In the following (and in the examples of the introduction), two-sided sequents may be used:

F 1 , . . . , F n ⊢ Γ should be read as ⊢ Γ, F ⊥ 1 , . . . , F ⊥ n .
Regarding the labelling of inference rules, we allow ourselves two conventions: either the inference rules are written with the labels introduced in Fig. 4 or, as in the introductory example, we use their two-sided names, for instance (⊗ l ) and (⊗ r ), in which case this is a notation for the corresponding rule in the one-sided sequent calculus, respectively ( ) and (⊗) here.

Example 2.9. In Fig. 5, π succ & π dup illustrate pre-proofs.

Pre-proofs are obviously unsound: any sequent can be derived. Hence, a validity condition shall be required for a pre-proof to be a proof. First we define cut-reduction.

The cut elimination process

In this section we introduce the cut-elimination rules for µMALL ∞ pre-proofs. In general, the cut-elimination procedure is not productive. However, we will show in Section 5 that when we restrict to valid pre-proofs (that will be defined in Section 4), the process is productive and outputs a valid pre-proof.

The multicut rule

In finitary proof theory, cut elimination may proceed by reducing topmost cuts. In the infinitary setting however, by non-wellfoundedness, there is no such thing, in general, as a topmost cut inference. In [START_REF] Baelde | Infinitary Proof Theory: the Multiplicative Additive Case[END_REF][START_REF] Fortier | Cuts for circular proofs: semantics and cut-elimination[END_REF], this issue is dealt with by reducing bottom-most cuts, and when encountering during the reduction a cut which is immediately above another one, instead of permuting two consecutive cuts, merging them into a new rule called multicut and noted (mcut). A multicut can be seen as a meta-rule to represent a finite tree of cuts.

We will also use this multicut approach 5 , but we now have to deal with axiom/cut reductions. This leads us to enrich

⊢ F , G, Γ ( ) ⊢ F G, Γ ⊢ Γ (⊥) ⊢ ⊥, Γ ⊢ F , Γ ⊢ G, Γ ( ) ⊢ F G, Γ (⊤) ⊢ ⊤, Γ ⊢ G[νX .G/X ], Γ (ν ) ⊢ νX .G, Γ F ≡ G (Ax) ⊢ F , G ⊥ ⊢ F , Γ ⊢ G, ∆ (⊗) ⊢ F ⊗G, Γ, ∆ (1)
⊢ 1

⊢ F i , Γ (⊕ i ), i ∈ {1, 2} ⊢ F 1 ⊕ F 2 , Γ (no rule for 0) ⊢ F [µX .F /X ], Γ (µ) ⊢ µX .F , Γ ⊢ Γ, F ⊢ F ⊥ , ∆ (Cut) ⊢ Γ, ∆ Figure 4. Rules of the proof system µMALL ∞ π succ = (Ax) N ⊢ N ′′ (⊕ 2 ) N ⊢ 1⊕N ′′ (µ) N ⊢ N ′ π dup = (µ),(⊕ 1 ), (1)
⊢ N 1

(µ),(⊕ 1 ), (1)
⊢ N 2

(⊥),(⊗) 1 ⊢ N 1 ⊗N 2 N ′ ⊢ N ′ 1 ⊗N ′ 2 π succ π succ ( ),(⊗) N ′ 1 ⊗N ′ 2 ⊢ N 1 ⊗N 2 (Cut) N ′ ⊢ N 1 ⊗N 2 (ν ),( ) N ⊢ N 1 ⊗N 2 Figure 5.
Examples of pre-proofs π succ and π dup .

the structure of multicuts, by allowing those to perform a renaming. A multicut is a rule written as:

⊢ Γ 1 . . . ⊢ Γ n mcut(ι, ⊥ ⊥) ⊢ Γ
and comes with a function ι which shows how the occurrences of the conclusion are distributed over the premisses (modulo renaming), and a relation |= specifying which occurrences are cut-connected. Below is an example of a multicut rule: the function ι is represented by the red lines, the relation |= is represented by the blue ones.

⊢ F ′ , G ⊢ G ⊥ , H ⊢ H ⊥ , K mcut(ι, ⊥ ⊥) ⊢ F , K
Precise definitions and more explanations are given in appendix A.2. Later, if clear from the context, we omit to specify ι and |= in the rule name. From now, we add the multicut rule to our proof system. Definition 3.1. We call µMALL ∞ m the infinitary proof system obtained from µMALL ∞ by adding the multicut rule.

Reduction rules and strategy

The reduction rules are the same as in [START_REF] Baelde | Infinitary Proof Theory: the Multiplicative Additive Case[END_REF][START_REF] Fortier | Cuts for circular proofs: semantics and cut-elimination[END_REF], adapting them in a straightforward way to account for the extra labellings ι, |= in multicut rules. We give examples of such reductions in this section.

There are two kinds of cut reductions: external ones that push the multicut deeper in the pre-proof (Example in fig. 6.a), and internal ones, that keep the multicut at the same level, and are not productive (Example in fig. 6.b). The rules in the first category are said to be productive, since they contribute to the output of the process. Intuitively, the cut-elimination process succeeds if infinitely many productive rules occur on each branch of the proof. An exhaustive description of the µMALL ∞ m cut-reduction rules is given in appendix A.3. We now describe a procedure to eliminate cuts from µMALL ∞ proofs, using as an intermediary framework the system with multicuts. We start by embedding µMALL ∞ in µMALL ∞ m by adding a unary multicut at the root of the pre-proof, with the identity as ι and |= = ∅. We then apply internal and external reduction rules to this multicut. We will require reduction sequences to be fair, in the sense that every redex is eventually fired.

The next section introduces the validity condition that will guarantee productivity of this cut elimination process.

Bouncing threads and pre-proof validity

We now formally introduce our bouncing threads and the corresponding notion of validity for pre-proofs. Given an alphabet A, we denote by A ω the set of infinite words over A, and define A ∞ to be A * ∪ A ω . We will make use of the letter λ to denote ordinals in ω + 1, i.e. either ω or a finite ordinal in N. For such an ordinal, recall that 1 + λ = λ iff λ = ω. Finally, we will make use of a special concatenation: given u = (u i ) i ≤n <ω and v = (v i ) i ∈λ such that u n = v 0 , we define u ⊙v as the standard concatenation of u and v without its first element, i.e. u • (v i ) i ∈λ\{0} . For example aba ⊙ aab = abaab.

Threads

We start with a naive notion of pre-thread, defined as a sequence of pointed sequents (i.e. sequents with a marked formula) with a direction: a pre-thread follows occurrences in consecutive sequents, travelling up-or downwards. Definition 4.1. A pre-thread is a sequence (F i , s i , d i ) i ∈λ of tuples of a formula, a sequent and a direction, such that for all i ∈ λ, F i ∈ s i , d i ∈ {↑, ↓} and if i + 1 ∈ λ then one of the following clauses holds:

• d i = d i+1 = ↑, s i+1 ∈ premiss(s i ), and
F i+1 ⊑ F i ; • d i = d i+1 = ↓, s i ∈ premiss(s i+1 ), and
F i ⊑ F i+1 ; • d i = ↓, d i+1 = ↑
, s i and s i+1 are the two premisses of the same cut rule, and

F i = F ⊥ i+1 ; • d i = ↑, d i+1 = ↓ and s i = s i+1 = {F i , F i+1 } is the conclusion of an axiom rule (so that F i ≡ F ⊥ i+1 ).
(a) Example of an external reduction rule:

C ⊢ ∆, F ′ [µX .F ′ /X ] (µ) ⊢ ∆, µX .F ′ (mcut) ⊢ Σ, µX .F -→ C ⊢ ∆, F ′ [µX .F ′ /X ] (mcut) ⊢ Σ, F [µX .F /X ] (µ) ⊢ Σ, µX .F (b) Examples of internal reduction rules: C ⊢ ∆, F ⊢ Γ, F ⊥ (Cut) ⊢ ∆, Γ (mcut) ⊢ Σ -→ C ⊢ ∆, F ⊢ F ⊥ , Γ (mcut) ⊢ Σ C ⊢ ∆, F [µX .F /X ] (µ) ⊢ ∆, µX .F ⊢ F ′⊥ [νX .F ′⊥ /X ], Γ (ν ) ⊢ νX .F ′⊥ , Γ (mcut) ⊢ Σ -→ C ⊢ ∆, F [µX .F /X ] ⊢ F ′⊥ [νX .F ′⊥ /X ], Γ (mcut)
⊢ Σ If λ = n + 1 is finite we call F 0 and F n the endpoints of the pre-thread.

Example 4.2. Consider the formulas φ = νX .X , F = φ α , F ′ = φ β , F ′′ = φ β .i where α and β are disjoint addresses. Let G, G ′ be two disjoint occurrences such that G ≡ G ′ . Below, the red and blue lines are two pre-threads6 :

(Ax) ⊢ F , F ′⊥ (Ax) ⊢ G, G ′⊥ ( , ⊗) ⊢ F G, F ′⊥ ⊗ G ′⊥ . . . ⊢ F ′′ , G ′ (ν ) ⊢ F ′ , G ′ ( ) ⊢ F ′ G ′ (Cut) ⊢ F G
We shall define threads as pre-threads satisfying a particular condition that will make them compatible with cut reduction, in the sense that they will have residuals after cut-elimination steps. In Example 4.2, the red thread has no residual if one performs a cut elimination step on F ′ G ′ , because it comes from the right-hand subformula of F ′⊥ ⊗G ′⊥ and goes to the left-hand subformula of F ′ G ′ . In contrast, the blue thread can meaningfully be simplified to persist over cut elimination steps: its residual is well-defined. Geometry of Interaction [START_REF] Girard | Towards a Geometry of Interaction[END_REF] provides a formalization of these notions, assigning weights to pre-threads and determining which weights correspond to meaningful computations. We follow this inspiration, adapting it to our framework. Definition 4.3. Let t = (F i , s i , d i ) i ∈1+λ be a pre-thread. The weight of t is a word (w i ) i ∈λ ∈ {l, r, i, l, r, ī, W, A, C} ∞ , written w(t) and defined as follows. For every i ∈ λ one of the following clauses holds:

• w i = x if F i = φ α and F i+1 = ψ α x for x ∈ {l, r, i}; • w i = x if F i = φ α x and F i+1 = ψ α for x ∈ {l, r, i}; • w i = A if d i = ↑ and d i+1 = ↓ (corresponding to
bouncing on an axiom rule);

• w i = C if d i = ↓ and d i+1 = ↑ (corresponding to
bouncing on a cut rule); The weight should be seen as a bracketed expression, where each symbol x, x ∈ {l, r, i}, is an opening bracket with matching closing bracket x. When defining threads from pre-threads, we will be particularly interested in the following classes of well-bracketed words: Definition 4.5. Let B and H be the set of words defined inductively as follows:

• w i = W if F i = F i+1 .
B := C | BW * AW * B | xW * BW * x H := ϵ | AW * B A (finite) pre-thread is called a b-path if w(t) ∈ B. It is called an h-path if w(t) ∈ H . It is called an ϵ-path. if w(t) ∈ W * H .
The b-paths start downwards and end upwards: they consist of a series of U-shapes centered around cuts, glued together by axioms. The endpoints of b-paths are negations of each other (up to renaming). The h-paths start and end going upwards, and their endpoints are structurally equivalent (up to renaming). Intuitively, h-paths will be simplified during cut elimination, and eventually disappear completely. Definition 4.6. A pre-thread t is a thread when it can be written ⊙ i ∈1+λ (H i ⊙ V i ) where for all i ∈ 1 + λ:

• w(H i ) ∈ H and it is non-empty if i 0.

• w(V i ) ∈ {l, r, i, W} ∞ and it is non-empty if i λ;

Notice that such a decomposition is unique, except possibly for some neutral W * factors, for which an arbitrary choice is made 7 . We call (V i ) i ∈1+λ the visible part of t, and we denote it by vp(t), and (H i ) i ∈1+λ its hidden part and we denote it by hp(t). A thread is stationary when its visible part is a finite sequence (of finite words), or when there exists k

∈ 1 + λ such that w(V i ) ∈ {W} ∞ for all k ≤ i ∈ 1 + λ.
For instance if a pre-thread t = (F i , s i , ↑) i ∈λ t of length λ t goes only upwards (w(t) ∈ {l, r, i, W} λ t ), then the above decomposition is given by λ = 0, H 0 = (F 0 , s 0 , ↑) and V 0 = t.

Example 4.7. Let us consider the blue pre-thread of Example 4.2. We can decompose it into a visible part (plain line) and a hidden part (dashed line) as shown below:

(Ax) ⊢ F , F ′⊥ (Ax) ⊢ G, G ′⊥ ( , ⊗) ⊢ F G, F ′⊥ ⊗ G ′⊥ . . . ⊢ F ′′ , G ′ (ν ) ⊢ F ′ , G ′ ( ) ⊢ F ′ G ′ (Cut) ⊢ F G
The blue pre-thread is then indeed a thread. On the contrary, the red pre-thread from example 4.2 admits no such decomposition.

If we consider the sequence of formulas followed by a non-stationary thread on its visible part, ignoring its hidden parts (which have equivalent formulas on their endpoints), and skipping the steps in the visible parts corresponding to W weights, we obtain an infinite sequence of formulas as in [START_REF] Baelde | Infinitary Proof Theory: the Multiplicative Additive Case[END_REF] where each formula is an immediate subformula or an unfolding of the previous formula. It is then well known [START_REF] Doumane | Théorie de la démonstration infinitaire pour les logiques à points fixes)[END_REF] that the formulas appearing infinitely often in that sequence admit a minimum w.r.t. the subformula ordering. We call this formula the minimal formula of the thread. Definition 4.8. A non-stationary thread is valid if its minimal formula is a ν -formula.

Consider for example the formula F = µX .νY .X . The minimal formula obtained by unfolding F infinitely often is F itself, a µ-formula, so the corresponding thread is invalid.

Pre-proof validity: the multiplicative case

The previous notion of valid thread suggests a first extension of the notion of valid proof based on straight threads [START_REF] Baelde | Infinitary Proof Theory: the Multiplicative Additive Case[END_REF]: one might say that a branch β is valid when there is a valid bouncing thread which meets β infinitely often, and declare a pre-proof valid when all its branches are. However, this notion of weak validity turns out to allow unsound proofs, as shown next.

Example 4.9. Let T := νX .X and F := µX .X . The following is a weakly valid proof of the empty sequent. The hidden part of the decomposition (and the prefix of the thread up to the first axiom) is dashed, the visible part (except the prefix of the thread up to the first axiom) is shown in green. The minimal formula along the thread is T .

(Ax) ⊢ F α l ,T β l (Ax) ⊢ T α ri , F β r (ν ) ⊢ T α r , F β r (⊗) ⊢ (F ⊗T ) α ,T β l , F β r ( ) ⊢ (F ⊗T ) α , (T F ) β ⊢ (F ⊗T ) β ⊥ (Cut) ⊢ F ⊗T α (Ax) ⊢ T α ⊥ l , F α ⊥ r ( ) ⊢ (T F ) α ⊥ (Cut) ⊢
A proper notion of validity must therefore be more constraining. We shall consider the following one, which requires that the visible part of the valid thread t is contained in the infinite branch β. Definition 4.10. Let π be a µMLL ∞ pre-proof. An infinite branch β of π is said to be valid if there is a valid thread t starting from one of its sequents, whose visible part is contained in this branch. A µMLL ∞ proof is a µMLL ∞ preproof in which every infinite branch is valid.

Ax) ⊢ (νX .X ) α , (µX .X ) β ⊢ (νX .X ) β ⊥ i (ν ) ⊢ (νX .X ) β ⊥ (Cut) ⊢ (νX .X ) α (Ax) ⊢ (νX .X ) α i , (µX .X ) β (ν ) ⊢ (νX .X ) α , (µX .X ) β ⊢ (νX .X ) β ⊥ (Cut) ⊢ (νX .X ) α
The topmost pre-proof is valid: its infinite branch is supported by the valid blue thread, whose visible part belongs to the infinite branch. The bottommost pre-proof is not valid, because the red thread, though valid, has a visible part that is not contained in the infinite branch.

Pre-proof validity: accommodating the additives

The previous definition of validity is too weak to ensure cut-elimination for µMALL ∞ , which is not a strictly linear sequent calculus (as µMLL ∞ is) since commutation/external reductions for the ( ) connective induce the duplication of a sub-proof. As a result, the extension of the validity condition in Section 4.2 fails to ensure productivity and validity of cut-elimination as shown in figure 7.(i). The result of cutelimination on the proofs in the sequence (π ′ k ) k ≥0 can be split into the following cases: (i) from π ′ 0 , cut-elimination is productive and produces a valid cut-free proof; (ii) from π ′ 1 , cut-elimination produces an invalid pre-proof (see Figure 7.(ii)): any infinite branch following only finitely many times the left back-edge is invalid; (iii) from π ′ k , for k ≥ 2 it is not even productive. Indeed, in these examples, each π ′ k contains exactly one infinite branch which is supported by a thread on T bouncing on the leftmost axiom and this thread is valid.

π ′ k = (Ax) † ⊢ T ,T ⊥ (⊥) ⊢ ⊥,T ,T ⊥ (Ax) ‡ ⊢ T ,T ⊥ (⊥) ⊢ ⊥,T ,T ⊥ (µ) k ⊢ ⊥,T ,T ⊥ ( ) ⊢ ⊥ ⊥,T ,T ⊥ ⊢ S,T (Cut) ⊢ ⊥ ⊥, S,T (µ),( ) ⊢ S,T (ν )
⊢ S,T

⊢S,T (⊥) ⊢ ⊥, S,T ⊢ S,T (⊥) ⊢ ⊥, S,T ( ) ⊢ ⊥ ⊥, S,T (µ),( ) ⊢ S,T (ν ) ⊢ S,T Sl(π ′ k ) ∋ (Ax) ⊢ T ,T ⊥ (⊥) ⊢ ⊥,T ,T ⊥ (µ) k ⊢ ⊥,T ,T ⊥ ( 2) ⊢ ⊥ ⊥,T ,T ⊥ ⊢ S,T (Cut) ⊢ ⊥ ⊥, S,T (µ),( ) ⊢ S,T (ν ) ⊢ S,T (i) (ii) (iii) Figure 7. (i) Pre-proof family (π ′ k ) k ∈N with S = µY .((⊥ ⊥) Y ),T = νX .X .
Note that we omit the occurrences and that k is a parameter fixing how many times the µ rule (in red) should be applied to the sequent ⊢ ⊥,T ,T ⊥ . (ii) Result of applying (infinitary) cut-elimination to π ′ 1 . (iii) Example of a slice of π ′ k .

To understand the problem, consider the first step of cutreduction (from π ′ k , for any k): it is a (Cut)/( ) commutation step, which copies the right-premiss of the cut (ie. the nonwellfounded part of the proof): after this step, the pre-proof contains two infinite branches, but only one thread to validate them. While the leftmost copy can be validated by the original thread, the rightmost copy does not contain a residual of the original thread. Of course, one might consider a thread originated in the cut inference, but that will not suffice to ensure validity, nor productivity, as π ′ 2 exemplifies: its rightmost branch produces the bottom rule.

Sliced proof system. This issue is solved by refining the criterion using slices [START_REF] Girard | Linear Logic[END_REF][START_REF] Girard | Locus Solum[END_REF][START_REF] Dominic | Proof nets for unit-free multiplicative-additive linear logic[END_REF][START_REF] Terui | Computational ludics[END_REF] and requiring that there exists a supporting thread not only for every infinite branch of the proof, but also for every infinite branch of every persistent slice of the pre-proof. In linear logic, an additive slice is a subtree of a sequent proof obtained by removing, for any of its ( ) inference, the subtree rooted in one of its premisses (see Appendix A.5 for details and precise definitions). Definition 4.12. µSMALL ∞ is obtained by extending µMALL ∞ with the following three inference rules:

⊢ A, Γ ( 1 )
⊢

A B, Γ ⊢ B, Γ ( 2 )
⊢ A B, Γ

(Ω) ⊢ Γ Definition 4.13 (Additive slice). Partially sliced pre-proofs are the non-wellfounded µSMALL ∞ pre-proofs. A slice is a ( )-free, (Ω)-free, µSMALL ∞ -pre-proof.

To a µMALL ∞ sequent (pre-)proof, one can associate a set of slices by keeping, for each ( ) inference, only one of its premisses and replacing the ( ) with the corresponding inference in ( 1 ), ( 2 ). More precisely: Definition 4.14 (Slicing of a pre-proof). The set of slices of π , Sl(π ), is defined corecursively by

Sl π 1 ⊢ A 1 , Γ π 2 ⊢ A 2 , Γ ( ) ⊢ A 1 A 2 , Γ =        π ′ i ⊢ A i , Γ ( i) ⊢ A 1 A 2 , Γ , π ′ i ∈ Sl(π i ), i ∈ {1, 2}       
(The other inferences are treated homomorphically.)

Example 4.15. Fig. 7.(iii) gives an example of a slice.

Cut-reductions for slices. Cut-reduction rules for (partial) slices of µSMALL ∞ extend those for µMALL ∞ with specific rules for sliced additives and (Ω). A problematic situation is when ( 1 ) interacts with (⊕ 2 ): cut-elimination cannot rely on sub-proofs as usual, and in this case (Ω) is used to solve this mismatch of inferences.

Definition 4.16 (Cut reductions for slices). The sliced additive principal case is reduced as follows, if

{A ⊥ 1 A ⊥ 2 , A ′ 1 ⊕ A ′ 2 } ∈ |= , with r = (princ, {A ⊥ 1 A ⊥ 2 , A ′ 1 ⊕ A ′ 2 }). C π i ⊢ A ⊥ i , Γ ( i ) ⊢ A ⊥ 1 A ⊥ 2 , Γ π ′ j ⊢ A ′ j , Γ (⊕ j ) ⊢ A ′ 1 ⊕ A ′ 2 , ∆ mcut(ι, ⊥ ⊥) ⊢ Σ -→ r                    (Ω) ⊢ Σ if i j C π i ⊢ A ⊥ i , Γ π ′ i ⊢ A ′ i , ∆ mcut(ι, ⊥ ⊥ ′ ) ⊢ Σ if i = j where |= ′ = |= ∪ {{A ⊥ i , A ′ i }} or C (Ω) ⊢ Γ mcut(ι, ⊥ ⊥) ⊢ Σ -→ r (Ω) ⊢ Σ with r = (princ, Ω).
Notions of b-paths and h-paths can be naturally extended to additive slices.

Persistent slices. Persistent slices are introduced precisely as those in which no case of the above mismatch ever occurs: Definition 4.17 (Persistent slice). Given a slice π , a ( i ) rule of principal formula A 1 A 2 occurring in π is said to be well-sliced if no b-path starting down from the A 1 A 2 occurrence of this sequent ends in a formula A ⊥ 1 ⊕ A ⊥ 2 that is the principal formula for a (⊕ j ) inference with i j. A slice is persistent if all its ( i ) occurrences are well-sliced.

. If π → * π ′ (resp. π → ω π ′ ) and S ′ ∈ Sl(π ′ ), then there is a S ∈ Sl(π ) such that S → * S ′ (resp. S → ω S ′ ).
Additive validity. Def 4.1 and 4.5 of (pre-)threads directly adapt to additive slices -as they are not specific to µMLL ∞and allow us to consider the following definition: Definition 4.21. A persistent slice is valid if it is valid in the sense of Definition 4.8 8 . A µMALL ∞ pre-proof π is valid if all its persistent slices are valid.

Example 4.22. Pre-proof π dup of Figure 5 is valid, the only infinite branch is validated by a straight. Among the preproofs of (π ′ k ) k ∈N given in Figure 7, only π ′ 0 is valid. The circular pre-proof of Figure 8 is valid. It corresponds to the last program considered in the introduction.

Cut elimination theorem for µMALL ∞

In this section, we shall establish our central result:

Theorem 5.1. Fair reduction sequences on µMALL ∞ m proofs produce cut-free µMALL ∞ proofs.

For expository reasons, we focus on the multiplicative case here. The treatment of additives, while bringing new cases, is similar and can be found in Appendix A. [START_REF] Baelde | Least and greatest fixed points in linear logic[END_REF].

The proof follows the same lines as the proof of [START_REF] Baelde | Infinitary Proof Theory: the Multiplicative Additive Case[END_REF] for straight threads. We only sketch it here and emphasize the new phenomena due to the presence of axioms and bouncing threads. The full proof can be found in Appendix A. [START_REF] Abel | Copatterns: programming infinite structures by observations[END_REF].

The proof of Theorem 5.1 is in two parts. We first prove that we cannot have an infinite fair reduction sequence made only of (unproductive) internal reductions. Hence cut elimination is productive, i.e., reductions of µMLL ∞ m proofs converge to cut-free µMLL ∞ pre-proofs. We then establish that the obtained pre-proof is a valid proof. In this section, we will only show productivity, validity of the resulting proof is shown in a similar way (See Appendix A.4).

To show productivity, we proceed by contradiction, assuming that there exists a fair infinite sequence of internal reductions from a given proof π of conclusion Γ. We will also assume w.l.o.g. that π has only one multicut at the root. Note that since we perform only internal reduction rules, and since the latter do not duplicate multicuts, there is only one multicut progressing in the proof during this sequence of reductions. In the following, we refer to it as "the" multicut.

Trace of a reduction sequence

Let us first introduce an important tool to analyse internal reduction sequences, called their trace. Along an internal reduction sequence (π i ) from a proof π , some sequents π become a premise of the multicut rule of some π i . The trace of an internal reduction sequence is defined as the collection of those sequents together with the conclusion sequent and the corresponding inference rules of the starting proof. By analyzing the reduction rules, it is easy to see that the trace of a proof is its proof tree from which some branches have been pruned and replaced by open leaves: Proposition 5.2. Given a µMLL ∞ proof π and a fair reduction sequent ρ, the trace of π after ρ is a subtree (possibly with open leaves) of the original proof π .

An example of a trace is shown below: sequents not in the trace are grayed.

. . .

(µ) ⊢ µX .X β i (µ) ⊢ µX .X β . . . (ν ) ⊢ µX .X β ⊥ ii , µX .X γ (ν ) ⊢ µX .X β ⊥ i , µX .X γ . . . (ν ) ⊢ νX .X γ ⊥ i , ⊥ α (ν ) ⊢ νX .X γ ⊥ , ⊥ α (Cut) ⊢ νX .X β ⊥ i , ⊥ α (ν ) ⊢ νX .X β ⊥ , ⊥ α (mcut) ⊢ ⊥ α
We shall get a contradiction using the trace in three steps:

1. We will define an extension of the proof system µMLL ∞ , and show that it is sound wrt. to a boolean semantics. 2. Then we will show that the trace can be seen as a proof of a false sequent in this extended proof system. 3. This contradicts soundness and concludes the proof.

The trace is almost a µMLL ∞ proof

As said above, we will need to see the trace as a genuine proof. Being a subtree of the original proof π , the trace is almost a µMLL ∞ proof; it may not be a proof for two reasons:

1) The trace may have unjustified sequents: this happens when a sequent S enters the multicut during the reduction sequence but never gets reduced. It will then be part of the trace but the subtree of π rooted in S will not. This is the case of the sequent ⊢ νX .X γ ⊥ i , ⊥ α in the example above.

2) The infinite branches of the trace may not be valid: they are of course also infinite branches of the proof π , and thus are supported by valid bouncing threads of π . However, since the threads can bounce, they might leave the branch and might not be entirely included in the trace.

We will show later how to handle the first problem of unjustified sequents. As for the second problem, we show that this actually never happens: Proposition 5.3. Let T be the trace of a reduction sequence starting from a proof π , and let β be an infinite branch of T . If t is a bouncing thread of π validating β, then t is also a bouncing thread of T . This is one of the difficulties specific to the bouncing threads. This result is trivial with straight threads [START_REF] Baelde | Infinitary Proof Theory: the Multiplicative Additive Case[END_REF], since threads belong to the branch they support.

π filter = π k ⊢ N (Ax) B ⊢ B S ⊢ S (ν l ),(⊗ l ),(ν r ),(⊗ r ) S ⊢ S (1 l ) 1, S ⊢ S N , S ⊢ S π neд B ⊢ B (Ax) S ⊢ S (ν l ),(⊗ l ),(ν r ),(⊗ r ) S ⊢ S (Cut) N , S ⊢ S (WBool l ) N , B, S ⊢ S (ν l ),(⊗ l ) N , S ⊢ S (µ l ),(⊕ 1 ) N , S ⊢ S (Cut) S ⊢ S Figure 8.
Example of an additive circular proof

Truncated proof system

To see the trace as a proof, we need to overcome the problem of unjustified sequents. For that, we will embed the trace in a so-called truncated proof system, extending µMLL ∞ . This proof system is parameterized by a partial function τ : Addr → {⊤, 0} (from addresses to the formulas ⊤, 0) called a truncation. To get a sound proof system, we impose a coherence condition on truncations: they should assign dual values to dual addresses. The rules of the truncated proof system are the same as those of µMLL ∞ , with an extra rule which allows to replace an occurrence by its image in τ . Pre-proofs and the validity condition are defined in the same way as for µMLL ∞ . The advantage of the truncated proof system is that it allows to close sequents easily: if the address of an occurrence of the sequent is mapped to ⊤ by τ , we can justify the sequent by a ⊤ rule.

The boolean semantics can be extended in the presence of truncations in a natural way: the occurrences whose addresses are in the domain of the truncation obtain as a boolean value their image by τ . Boolean values are propagated through the connectives as usual. We show that the truncated proof system is sound for this semantics.

Note that µMLL ∞ can be seen as a truncated proof system, where the truncation has empty domain. The truncated boolean semantics then coincides with the classical boolean semantics. Hence µMLL ∞ is sound for the boolean semantics, a result which can be extended to µMALL ∞ : Theorem 5.4. µMALL ∞ is sound for the boolean semantics.

Trace as a truncated proof

Let us see how to transform the trace into a proof in a truncated proof system. For this, we need to find a truncation τ that can allow us to close every unjustified sequent. In other words, we need to find a strategy for selecting an occurrence in each unjustified sequent, to which we will assign ⊤ by the truncation τ . This strategy should be coherent in the sense that it should not assign ⊤ to two dual occurrences.

In [START_REF] Baelde | Infinitary Proof Theory: the Multiplicative Additive Case[END_REF], such a strategy is given in a simpler setting: select the formula occurrence in the unjustified sequent that is principal in the proof π . Axioms complicate the situation: if F is the occurrence that has been selected in an unjustified sequent, then its dual might appear in an axiom rule ⊢ F ⊥ , G. By coherence of the truncation, the address of F ⊥ must be assigned 0 and the axiom rule cannot be soundly applied anymore. To justify ⊢ F ⊥ , G, we need to assign ⊤ to the address of G. Since the same can happen on the G side, we need to show that it remains possible to define τ in a coherent way.

To get our desired contradiction, we need in addition for τ to assign 0 to the conclusion, thereby obtaining a proof of a false sequent. This needs to be done while still respecting the aforementioned constraints induced by axioms. Summary. To sum up, we have found a truncation τ i) which assigns 0 to the conclusion formula and ii) for which the trace can be seen as a proof in the corresponding truncated proof system. Since the proof system is sound, we get a contradiction. This concludes the proof of productivity.

6 Decidability properties of µMLL ω

An operational approach to threads

In this section, we explain how threads can be recognized by a specific deterministic ω-pushdown automaton reading only the weight of a pre-thread. This allows us to define the height of a thread and the notion of constraint stack.

Let A thread be the deterministic ω-pushdown automaton described in Fig. 9, on alphabet Σ = {l, r, i, l, r, ī, A, C, W} and stack alphabet Γ = {l, r, i, ⊥} where ⊥ is the empty stack symbol. The transitions are labelled "(a, γ ) | τ ", where a ∈ Σ is the input letter, γ ∈ Γ is the topmost stack symbol, and τ is the action performed on the stack (no action if τ is not specified). If no stack symbol is specified, the stack is left unchanged. Symbol x stands for an element in {l, r, i}. No acceptance condition is specified: any run is accepting. Only the absence of an available transition can cause the automaton to reject its input, e.g. reading l with topmost stack symbol r in state ↑. The transition marked with a double arrow corresponds to the visible part of the thread.

The stack of A thread is referred to as the constraint stack.

↑ ↓ (x, ⊥) (x, x) | pop() W A ( x, γ ) | push(x) W C Figure 9. The deterministic ω-pushdown automaton A thread (Ax) ⊢ G, F ⊢G, F (µ, , ⊗) ⊢ G, F F (ν ) ⊢ G, F π R ⊢ G, F π M ⊢ G, F (Cut) ⊢ G, F (Cut) ⊢ G, F Figure 10
. A sketch of the main pre-proof P Lemma 6.1. Let t be a pre-thread. Then t is a thread if and only if w(t) is accepted by A thread .

Proof. Constraints on the stack of A thread match the grammar of Def. 4.5. □

Undecidability of bouncing validity

In this section we present the proof of the following result:

Theorem 6.2. The bouncing validity condition is already undecidable for µMLL ω .

This motivates the following section introducing decidable subcriteria constituting a hierarchy of criteria.

To show undecidability, we reduce from the halting problem for Minsky Machines, i.e. two-counter machines (2CM) able to perform increment, decrement, and zero test on the counters. The halting problem for 2CM is known to be Σ 0 1complete [START_REF] Minsky | Recursive Unsolvability of Post's Problem of "Tag" and other Topics in Theory of Turing Machines[END_REF].

The proof is only sketched here, and some technicalities have been abstracted away for clarity purposes. See Appendix A.6.1 for exact definitions and encodings.

We encode the halting problem of a 2CM M using a bouncing thread. The thread of interest will always follow a formula F = νX .(X X ) when going upwards, and its dual G = µX .(X ⊗X ) when going downwards. The idea is to use the constraint stack to encode the value of counters, and the position in the graph to encode the control state of the machine. The general shape of the main pre-proof P performing the desired reduction is represented in Fig. 10. Boldface formulas are those introduced in cuts, and grayed formulas are the ones that are not part of the thread of interest. We ignore addresses in this sketch, unless relevant to our encoding.

We build P so that the only branch which is not clearly validated is the one going infinitely many times through the loop. A thread validating this branch (in blue in Fig. 10) must go through the two cuts, and bounce on axioms in π M and π R . The trajectory of this thread in π M will simulate the run of M. It will be allowed to exit π M if and only if M terminates. We now give an example of one of the simplest gadgets used to perform this simulation: the increment gadget on the first counter. Consider a state p of the machine M, whose action is to increment the first counter and go to state q. Assume counter values (n, m) are encoded by a constraint stack l n rl m r, where l (resp. r) stands for a left (resp. right) constraint on the unfolding of F , i.e. a relative address il (resp. ir). This means that to increment the first counter, we need to add a left constraint at the top of the stack. This can be performed by the following gadget, where nodes labeled (p) and (q) encode the current control state:

(q) ⊢ G, F, A (Ax) ⊢ G l , F (∞) ⊢ G r , A (⊗) ⊢ G l ⊗G r , F , A (µ) ⊢ G, F , A (Acut) (p) ⊢ G, F , A
Here A is an auxiliary formula νX .(X X )⊗X , that can be duplicated as required and used to build axiom-less valid proofs, denoted by an (∞) meta-rule. The rule (Acut) denotes a cut combined with a duplication of A. A thread entering node (p) upwards with constraint stack l n rl m r will enter node (q) with constraint stack l n+1 rl m r.

In order to fully simulate the run of M, we also need to design gadgets simulating increment on the second counter, as well as decrement and zero test on both counters. The main difficulty lies in the tests performed by the machine: we want the thread to follow a conditional branching, depending on the value of the constraint stack. This can be done, but because of the linearity of the proof system, we cannot avoid leaving some extra constraints encoding the results of the tests. These "garbage constraints" will be collected by the thread on its path downwards in π M , after the simulation of the machine is completed. Since we want to finish with empty constraint, we need to erase these garbage constraints. To do this, we add a second gadget π R performing the computation in a dual way: garbage constraints are fed to the thread, which rewinds the computation while erasing these unwanted constraints. All gadgets in π R are dual versions of those in π M . This technique is reminiscent of the one used by Bennett [START_REF] Bennett | Logical Reversibility of Computation[END_REF] to prove Turing-completeness of reversible Turing machines, where a history of the computation is produced to guarantee reversibility, then this history is erased by rewinding the computation.

We can finally exit this detour with no constraint, and perform a visible ν -unfolding on the main branch (in red in Fig. 10), before looping back to the root of the proof.

The global pre-proof P will be a valid proof according to the criterion if and only if the machine M halts.

Notice that among the simplifications we made here for clarity of exposition, the auxiliary formula A needed in some gadgets has been removed from the main pre-proof P.

A hierarchy of decidable validity conditions

In order to recover a decidable criterion, we will consider restrictions on the constraint stack of valid threads. Definition 6.3. If t is a thread, we define its height h(t) ∈ ω + 1 to be the supremum of the size of the stack of A thread along its run on w(t). Definition 6.4. Let k ∈ N. An infinite branch is k-valid if there is a thread of height at most k validating it. A proof P is a k-proof if every infinite branch of P is k-valid.

The following two theorems show that the height parameter k induces a hierarchy of decidable criteria -see Figure 3 on page 4 -whose union matches the full validity criterion. Theorem 6.5. If P is a valid circular proof of µMLL ω , there exists k ∈ N such that P is a k-proof. Theorem 6.6. Given a circular pre-proof P of µMLL ω and an integer k, it is decidable whether P is a k-proof.

We now give a brief proof sketch to give an intuition on how to prove Theorems 6.5 and 6.6. See Appendix for details.

Proof. (Sketch) We will use the fact that once a starting point for a thread has been chosen, the thread evolves deterministically along the proof tree until a visible event occurs. We define the notion of minimal shortcut which is a part of a thread with no visible weight, bouncing on an axiom, and ending in the first point where the constraint stack is empty. It corresponds to an ϵ-path.

By bounding the maximal height of the stack by k, we can detect loops or declare stack overflow, and we are able to compute the unique minimal shortcut (if it exists) for each starting point in the finite proof graph. Now, checking validity of the proof can be done using an algorithm for straight threads [START_REF] Doumane | Théorie de la démonstration infinitaire pour les logiques à points fixes)[END_REF], allowing them to take these shortcuts. Theorem 6.5 is obtained by taking the maximal height reached by all minimal shortcuts of the proof graph. □ Combining Theorems 6.5 and 6.6, we obtain that validity of a circular pre-proof of µMLL ω is in Σ 0 1 , i.e. recursively enumerable. Together with the reduction from Sec. 6.2, we obtain the following corollary: Corollary 6.7. The problem of deciding whether a circular pre-proof of µMLL ω is a proof is Σ 0 1 -complete.

Conclusion

We have studied non-wellfounded and circular proofs of µMALL ∞ and defined an extended validity criterion for the pre-proofs of µMALL ∞ compared to previous works [START_REF] Baelde | Infinitary Proof Theory: the Multiplicative Additive Case[END_REF][START_REF] Fortier | Cuts for circular proofs: semantics and cut-elimination[END_REF]. We have shown that our criterion enjoys cut elimination and soundness, but reaches the barrier of undecidability: in the purely multiplicative fragment already, a parameter has to be bounded by an explicit value to make the criterion decidable.

mull For future work, we plan to investigate whether this decidability result still holds when adding the additives. We also want to extend these results to more relaxed criteria: we conjecture that requiring the visible parts to meet the validated branch infinitely often is sufficient to ensure productivity and soundness, generalizing Theorems 5.1 and 5.4 to a more relaxed validity condition. A less sequential variant of circular proofs has been developed by De et al. [START_REF] De | Canonical proofobjects for coinductive programming: infinets with infinitely many cuts[END_REF][START_REF] De | Infinets: the parallel syntax for non-wellfounded proof-theory[END_REF]: the canonicity and absence of commutation rules of proof nets may have good properties with respect to cut-elimination and we expect bouncing validity to be fruitful in that setting.

Finally, the present work is a first step in improving the compositionality of circular proofs. We demonstrated the flexibility of bouncing threads on a number of examples: current work is pursued to develop a proof-term syntax, in the style of system L, for circular µMALL. In addition to strengthening our cut-elimination result as mentioned above, we plan to investigate how one can import results from sized types [START_REF] Abel | Mixed inductive/coinductive types and strong normalization[END_REF] or copattern [START_REF] Abel | Copatterns: programming infinite structures by observations[END_REF] approach which also have good properties with respect to compositionality and may be used in an infinitary scenario [START_REF] Abel | Compositional Coinduction with Sized Types[END_REF][START_REF] Abel | Well-founded recursion with copatterns and sized types[END_REF].

A Appendices

A.1 On sequents as sets of occurrences

There are several presentations of sequents in the literature: a sequent can be defined as a set of formulas, a multiset of formulas, a list of formulas or a set of named formulas. The first two presentations (sets and multisets of formulas) are not suitable in a Curry-Howard perspective as they identify proofs having completely different computational behaviours: we need not only a "ressource-aware" notion of sequents but also an "occurrence-aware", essentially using lists of formulas or occurrences of formulas.

The last two presentations are the most used in the proofsas-programs framework. Considering sequents as lists of formulas requires a constant use of the exchange rule, which is very heavy. In this paper, we made the choice to work with sequents as sets of named formulas, also called formula occurrences.

A formula occurrence is a formula together with an address. In a derivation, all the conclusion (and cut) formula occurrences will have pairwise distinct addresses.

We consider a set of atomic addresses which is used to provide an infinite set of incomparable addresses (this could be achieved via words at the cost of an encoding). This intuition is that atomic addresses and their duals will be assigned to the conclusions and cut formulas, ensuring those occurrences are disjoint, and all the addresses appearing in the proofs will be sub-addresses of these addresses: disjointness is preserved by each inference rule.

When a rule is applied to a formula occurrence, the addresses of its sub-occurrences will be extended by {l, r, i} (standing for left, right and inside respectively) in order to record their provenance. This is of great importance for our developments: our validity criterion traces the evolution of formulas, and this evolution is completely explicit in their addresses.

Example A.1. We show in the following an example of an application of the rule in the framework of sequents as sets, as multisets and as sets of formula occurrences respectively:

⊢ φ ( ) ⊢ φ φ ⊢ φ, φ ( ) ⊢ φ φ ⊢ φ α l , φ α r ( ) ⊢ (φ φ) α
In the first case, the two subformulas of φ φ collapse into one formula, in the second framework we keep track of the multiplicity but we cannot distinguish between the formula coming from the right and the one coming from the left. In the framework of formula occurrences, we can do this thanks to the tags l and r in their addresses.

A.2 The multicut rule

A new phenomenon occurs in the presence of axioms. Consider for instance the following pre-proof where F = φ α and

G = φ β : (Ax) ⊢ F , G ⊥ π ⊢ G, Γ . . . (mcut) ⊢ F , Γ ′
In the finitary cut-elimination procedure, we would reduce this multicut to the derivation labelled (mcut 1 ) below. Doing so, we have to perform a substitution on addresses (denoted by [α/β]) to relocate the subderivation π on the required occurrence. Another option, described by the derivation (mcut 2 ) below, is to avoid the renaming by keeping a link explicitely in the multicut rule.

π [β/α] ⊢ F , Γ . . . (mcut1) ⊢ F , Γ ′ or π ⊢ G, Γ . . . (mcut2)
⊢ F , Γ ′

We choose the last option to avoid the global renaming, which would complicate our technical development.

A multicut rule will now be written as:

⊢ Γ 1 . . . ⊢ Γ n mcut(ι, ⊥ ⊥) ⊢ Γ
and comes with a function ι which shows how the occurrences of the conclusion are distributed over the premisses (modulo renaming), and a relation |= specifiying which occurrences are cut-connected. A precise definition of the multicut rule is given below. Definition A.2. Given sequents s, s 1 , . . . , s n where n > 0 and such that s i , s j are disjoint for all i j, a multicut of conclusion s and premisses (s i ) i ∈[1;n] is given by an injection ι : s → ∪ i ∈[1;n] s i and a symmetric relation We write this multicut rule as:

|= ⊆ (∪ i ∈[1;n] s i ) 2 such that: • For all F ∈ s, ι(F ) ≡ F . • For all F , G ∈ ∪ i ∈[1;n] s i , F |= G implies F ≡ G ⊥ . • dom( |= ) = (∪ i ∈[1;n] s i ) \ im(ι). • Given
s 1 . . . s n mcut(ι, ⊥ ⊥) s A.

Cut elimination rules

We detail the rules of cut elimination introduced in section 3. Remark 1. Note that the (⊗)/(mcut) external reduction yields multiple multicuts, though always on disjoint sub-trees. Thus, µMLL ∞ m is stable by external reductions.

In external reductions, we pushed a multicut away from the root, above a logical rule. If we start with a µMLL ∞ m preproof and apply a reduction sequence where external rules are applied infinitely often to each multicut, we will produce at the limit a cut-free proof. This is the reason why we say that external reductions are productive. This is not the case for the internal reduction rules given next.

Definition A.4. Internal reductions are the principal reductions given in fig. 12 together with the following two reductions:

• the merge (mcut)/(Cut) reduction

C ⊢ ∆, F ⊢ Γ, F ⊥ (Cut) ⊢ ∆, Γ mcut(ι, ⊥ ⊥) ⊢ Σ -→ r C ⊢ ∆, F ⊢ Γ, F ⊥ mcut(ι, ⊥ ⊥ ′ ) ⊢ Σ where |= ′ extends |= with F |= ′ F ⊥ and r = (merge, {F , F ⊥ }). • the axiom reduction (mcut)/(Ax) C (Ax) ⊢ F , F ′⊥ ⊢ F ′′ , Γ mcut(ι, ⊥ ⊥) ⊢ Σ -→ r C ⊢ F ′′ , Γ mcut(ι ′ , ⊥ ⊥ ′ ) ⊢ Σ
where r = (CutAx, {F , F ′⊥ }), F ′⊥ |= F ′′ and ι ′ , |= ′ are defined as follows:

-

for all G ∈ Σ, if ι(G) = F then ι ′ (G) = F ′′ , otherwise ι ′ (G) = ι(G); - |= ′ = |= ∪ {{F ′′ , G}|{F , G} ∈ |= }.
In internal reductions, the multicut remains at the root of the redex. Thus, if a sequence of multicut reductions eventually involved only internal reductions, it would not be productive.

The use of labels in reductions allows us to define in full details our notion of reduction sequence and fairness.

Definition A.5. A reduction sequence is a finite or infinite sequence σ = (π i , r i ) i ∈1+λ with λ ∈ ω + 1, where the π i are µMLL ∞ m pre-proofs, the r i are labels identifying multicut reduction rules and, for all i ∈ λ, π i -→ r i π i+1 . The sequence is fair if for all i ∈ λ and r such that π i -→ r π ′ there is some j ∈ λ such that j ≥ i and π j -→ r π j+1 .

A.4 Cut elimination for µMLL ∞

A.4.1 Trace of a reduction sequence

If R is a reduction sequence starting from π , we start by defining the trace of R to be the subtree of π whose sequents occur in the reduction sequence as premisses of some multicut. Note that each node of the trace corresponds to a well-formed inference: indeed, if sequents S and S ′ are premisses of a same inference (which must thus be a tensor or cut) and S enters a multicut at some point in the reduction sequence, then S ′ must also enter a multicut -though not necessarily the same one. However, the trace may have unjustified sequents: this happens when a sequents S enters the multicut during the reduction sequence but never leaves it; it will then be part of the trace but the subtree of π rooted in S will not.

The unjustified sequents of the trace are called its border sequents. Note that a border sequent cannot be the conclusion of an axiom rule nor a cut rule in the initial derivation π . If this were the case, by fairness, it would have been absorbed by an (Ax)/(mcut) or a (Cut)/(mcut) reduction respectively. This allows to define the distinguished occurrence of a border sequent as the principal occurrence of the logical rule applied to the border sequent in π .

There is another reason why the trace of a reduction sequence might not be a proof: its infinite branches may not be valid. The infinite branches of the trace are also infinite branches of the proof π , thus they are supported by valid threads of π , but these threads might not be included in the trace. We show that this actually never happens.

A.4.2 The bouncing threads of the trace belong to the trace

This section is dedicated to proving the following theorem.

Proposition A.6. Let T be the trace of a reduction sequence starting from a proof π , and let β be an infinite branch of T . If t is a thread of π validating β, then t is also a thread of T .

We now introduce a a useful technical tool called the residual of a pre-thread.

Definition A.7 (Residual of a pre-thread). Let R be a finite reduction path starting from π to π ′ and let t be a pre-thread of π . Let S ′ be the set of sequents of π ′ . We call the residual of t after the reduction R the pre-thread t ∩ {(F , s, d)|s ∈ S ′ , d ∈ {↑, ↓}}.

By definition, the length of the residual of t is smaller than the length of t.

Proposition A.8. Let R be a finite reduction path starting from π to π ′ , let T be its trace. Let t be a b-thread of π and t ′ its residual after R. Then t ′ is a b-thread. Furthermore, if t is a B-path of π , then t ′ is a B-path of T , and t ′ has the same endpoints as t.

C ⊢ ∆, F ′ ⊢ Γ, G ′ (⊗) ⊢ ∆, Γ, F ′ ⊗G ′ mcut(ι, ⊥ ⊥) ⊢ Σ ∆ , Σ Γ , F ⊗G -→ r C ∆ ⊢ ∆, F ′ mcut(ι ′ , ⊥ ⊥) ⊢ Σ ∆ , F C Γ ⊢ Γ, G ′ mcut(ι ′′ , ⊥ ⊥) ⊢ Σ Γ , G (⊗) ⊢ Σ ∆ , Σ Γ , F ⊗G C ⊢ ∆, F ′ , G ′ ( ) ⊢ ∆, F ′ G ′ mcut(ι, ⊥ ⊥) ⊢ Σ, F G -→ r C ⊢ ∆, F ′ , G ′ mcut(ι ′ , ⊥ ⊥) ⊢ Σ, F , G ( ) ⊢ Σ, F G C ⊢ ∆, F ′ [σX .F ′ /X ] (σ ) ⊢ ∆, σX .F ′ mcut(ι, ⊥ ⊥) ⊢ Σ, σX .F -→ r C ⊢ ∆, F ′ [σX .F ′ /X ] mcut(ι ′ , ⊥ ⊥) ⊢ Σ, F [σX .F /X ] (σ ) ⊢ Σ, σX .F C ⊢ ∆ (⊥) ⊢ ∆, ⊥ β mcut(ι, ⊥ ⊥) ⊢ Σ, ⊥ α -→ r C ⊢ ∆ mcut(ι ′ , ⊥ ⊥) ⊢ Σ (⊥) ⊢ Σ, ⊥ α (1)
⊢

1 β mcut(ι, ⊥ ⊥) ⊢ 1 α -→ r (1)
⊢ 1 α

In the first reduction ((⊗)/(mcut)) we require that ι(F ⊗G) = F ′ ⊗G ′ and take ι ′ and ι ′′ that coincide with ι on Σ ∆ and Σ Γ respectively, and such that ι ′ (F ) = F ′ and ι ′′ (G) = G ′ . In the other reductions ι and ι ′ are similarly constrained.

C ⊢ ∆, F ⊢ Γ, G (⊗) ⊢ ∆, Γ, F ⊗G ⊢ Θ, F ′⊥ , G ′⊥ ( ) ⊢ Θ, F ′⊥ G ′⊥ mcut(ι, ⊥ ⊥) ⊢ Σ -→ r C ⊢ ∆, F ⊢ Γ, G ⊢ Θ, F ′⊥ , G ′⊥ mcut(ι, ⊥ ⊥ ′ ) ⊢ Σ where F ⊗G |= G ′⊥ G ′⊥ and |= ′ coincides with |= except for F |= ′ F ′⊥ and G |= ′ G ′⊥ C ⊢ ∆, F ′ [µX .F ′ /X ] (µ) ⊢ ∆, µX .F ′ ⊢ Γ, F ⊥ [νX .F ⊥ /X ] (ν ) ⊢ Γ, νX .F ⊥ mcut(ι, ⊥ ⊥) ⊢ Σ -→ r C ⊢ ∆, F ′ [µX .F ′ /X ] ⊢ Γ, F ⊥ [νX .F ⊥ /X ] mcut(ι, ⊥ ⊥ ′ ) ⊢ Σ where µX .F ′ |= νX .F ⊥ and |= ′ coincides with |= except for F ′ [µX .F ′ /X ] |= ′ F ⊥ [νX .F ⊥ /X ] C ⊢ Γ (⊥) ⊢ Γ, ⊥ α (1) ⊢ 1 β mcut(ι, ⊥ ⊥) Σ -→ r C ⊢ Γ mcut(ι, ⊥ ⊥) Σ where ⊥ α |= 1 β Figure 12.
Principal reductions, where r = (princ, {F , F ′⊥ }) with {F , F ′⊥ } the principal occurrences that have been reduced.

Proof. It suffices to consider a single reduction step. Most of the claims follow from a simple inspection of the reduction rules. For the last one (i.e. t and t ′ have the same endpoints) we have to additionally rule out the possibility that, if s and s ′ are the endpoints of t, s gets reduced at some point of the reduction while s ′ does not: this could only happen if s (or s ′ ) was part of an (Ax)/(mcut) reduction, but that would mean that our B-path can be extended into an h-path (if the axiom is at the beginning of the path) or the reverse of an h-path (if the axiom is at the end). □ Definition A.9. A pre-thread t is a B-path of π if:

• it is a maximal b-path of π , i.e. there is no b-path of π which contains t as an infix; • it cannot be extended as an h-path or as the reverse of an h-path.

Intuitively, the second condition means that the path cannot be extended by an axiom on either side, possibly after silent steps corresponding to W weights.

Lemma A.10. Let R = {π i , r i } i ∈ω be a reduction sequence and let T = T r (R) be its trace. If t is a B-path of T , then there is an index i such that the endpoints of t are mcut-connected in the multicut of π i .

Proof. As reductions are performed, the thread t is simplified into residuals. As long as these residuals remain non-empty, they are still b-paths in their respective derivations, and they keep the same endpoints because the only way to reduce one endpoint without the other is through an (Ax)/(mcut) reduction. Moreover, the length of residuals only decreases. In fact, since t is in the trace, it strictly decreases infinitely often. Thus, at some point, the two endpoints of t are directly mcut-connected. □

Proof of proposition 5.3. Let t be a thread validating the branch β in π . The visible part of t belongs to β, hence its belongs to the trace T . One needs to prove that the hidden part belongs also to the trace. Suppose by contradiction that some H = (F i , s i , d i ) 1≤i ≤n ∈ hp(t) leaves the trace. Thus there is an index j ≤ n such that s j is a border sequent of the trace. Take the maximal such j. If d j = ↑ then, since the hidden part H ends in a sequent of β, there must be a position k with j < k < n such that the path exits the subtree rooted in s j to re-enter β: we would then have s k = s j , contradicting the maximality of j. Hence,

d j = ↓.
Since H is a b-path, and d j =↓, then there is k > j such that H [j, k] is a b-path: keeping with the intuition that b-paths are well-bracketed words, the opening bracket at position j must have a corresponding closing bracket at position k such that the word in between is well-bracketed, thus a b-path. By maximality of j, H [j, k] is in the trace.

Let k be maximal with this property. Note that H [j, k] is a maximal b-path in the trace, since s j is a border sequent and k is chosen to be maximal. Let us show that H [j, k] cannot be extended to an ϵ-path of the trace. Suppose by contradiction that this is the case. Since s j is a border sequent, H [j, k] can be extended only on the right. Thus there is l > k such that H [j, l] is an ϵ-path. Since H [j, l] starts with a downward direction, and since ϵ-paths have the same direction in their endpoints, we have that d l = ↓. Thus by the same reasoning as before, there is m > l such that H [l, m] is a b-path. Thus H [j, m] is a b-path, which contradicts the maximality of k.

We can now apply lemma A.10 to H [j, k]: at some point of the reduction, the sequents s j and s k are mcut-connected through the occurrences F j and F k . Note that s k+1 belongs to T (by maximality of j) and that F k +1 is a strict sub-occurrence of F k (otherwise, this would contradict the maximality of k). Since F k +1 is in the trace, this means that F j has been reduced which is not possible since s j is in the border of the trace.

□

In order to view a trace as a µMLL ∞ m proof, we shall devise a way to justify its border sequents. Intuitively, we will identify each distinguished occurrence with the true constant ⊤. To achieve this formally, we introduce a truncated proof system in the next section. Before that, let us mention a key technical result, which builds on the intuition that b-paths are simplified during cut elimination.

A.4.3 Truncated proof system

The truncated proof system builds on a truncation that forces a semantics on particular occurrences. Definition A.11. A truncation τ is a partial function from Σ * to {⊤, 0} such that:

• For any α ∈ Σ * , if α ∈ Dom(τ ), then α ⊥ ∈ Dom(τ ) and τ (α) = τ (α ⊥ ) ⊥ . • If α ∈ Dom(τ ) then for any β ∈ Σ + , α .β Dom(τ ).
Definition A.12. Given a truncation τ , the infinitary proof system µMLL ∞ τ is obtained by taking all the rules of µMLL ∞ together with the following rule for ⊤:

(⊤) ⊢ Γ, ⊤ α
with the following proviso. The rules of µMLL ∞ only apply when the address of their principal occurrence is not in the domain of τ , otherwise the following rule has to be applied:

⊢ τ (α) α i , ∆ (τ ) ⊢ φ α , ∆ if α ∈ Dom(τ )
The notions of thread and validity are the same as in µMLL ∞ .

As in [START_REF] Baelde | Infinitary Proof Theory: the Multiplicative Additive Case[END_REF] we define a classical truth semantics for our truncated proof system. Truncated occurrences (i.e. whose address is in Dom(τ )) are assigned their value under τ . The semantics of a unit ⊤ or 0 is itself. Then this semantics is propagated to more complex formulas inductively, interpreting as disjunction, ⊗ as conjunction, and µ, ν as least and greatest fixed points respectively. The semantics of an occurrence F under a truncation τ is noted F . We establish, in the same way as in [START_REF] Baelde | Infinitary Proof Theory: the Multiplicative Additive Case[END_REF] that µMLL ∞ τ is sound wrt. this semantics: Proposition A. [START_REF] Dax | A Proof System for the Linear Time µ-Calculus[END_REF].

If ⊢ Γ is provable in µMLL ∞ τ , then F = ⊤ for some F ∈ Γ.
Since µMLL ∞ is a sub-system of µMLL ∞ τ , we obtain as a corollary that µMLL ∞ is sound wrt. the boolean semantics.

A.4.4 From traces to truncated proofs

Definition A.14. Let π be a pre-proof. We define the relations ≈ π and |= π as follows: Proof. We proceed by contradiction. Let t 2 be the b-path from G to F , starting with a ↓ direction and ending with ↑. Let t 1 be the path from F to H . It must be an h-path, starting and ending with ↑. Indeed, the reverse of an h-path would reach H with a ↓ which is absurd since H is a distinguished occurrence of a border sequent. Let t be the b-path obtained by gluing the path from G to F with the path from F to H . This path is a B-path of T , since its endpoints are distinguished formulas, so they are in the border of the trace. By applying lemma A.10, there is a point in the reduction where the occurrences G and H are directly mcut-connected.

• F ≈ π G if there is an h-path in π from F to G, or from G to F . • F |= π G if
Since G and H are distinguished, they are principal occurrences of the rules applied to their border sequents in π . Thus, considering the point of the reduction where they are directly mcut-connected, there is an internal redex on G and H . By fairness it is reduced, which contradicts the fact that they are distinguished occurrences of border sequents. □ By proposition A.15 we can define the truncation and truncated proof associated to a trace. Definition A.16. Let R be a reduction sequence and T be its trace. The truncation τ associated with R is defined by setting:

•

τ (F ) = 0 if there is a distinguished occurrence G such that F |= T G, • τ (F ) = ⊤ if there is a distinguished occurrence G such that G ≈ T F .
Definition A.17. Let T be the trace of a infinite internal reduction sequence starting from π , and let τ be the truncation associated to this reduction. The truncated proof π τ is obtained from T by replacing every border sequent ⊢ φ α , Γ, whose distinguished occurrence is φ α by the following derivation:

(⊤) ⊢ ⊤ α .i , Γ (τ )
⊢ φ α , Γ

It is now easy to establish productivity of cut elimination.

Proposition A.18. Any fair reduction sequence produces a µMLL ∞ pre-proof.

Proof. By contradiction, consider a fair infinite sequence of internal multicut reductions starting from π . Let π τ be the truncated proof of its trace. Since no external reduction occurs, it means that an occurrence F in the conclusion of π τ can only be principal in an (Ax)/(mcut) reduction of the considered sequence. If ι is the injection associated to the multicut after that reduction, the same observation holds for ι(F ), and so on. In short, any occurrence F ′ ≈ π τ F will never be principal in a logical rule. Hence we can replace all these occurrences by occurrences of ⊥. We thus obtain a proof of the sequent ⊢ ⊥, . . . , ⊥ which contradicts the soundness of µMLL ∞ τ . □

A.4.5 Proof of cut elimination

We have shown in proposition A.18 that multicut reduction is productive. To establish cut-elimination (theorem 5.1), it only remains to prove that the resulting (cut-free) pre-proof is actually a valid proof.

Proof of theorem 5.1. Let π be a µMLL ∞ m proof of conclusion ⊢ A, and π ′ the cut-free pre-proof obtained by proposition A.18, i.e., the limit of the multicut reduction process. Any branch of π ′ corresponds to a multicut reduction path. For the sake of contradiction, assume that π ′ is invalid. It must thus have an invalid infinite branch β = (s i ) i ∈ω , corresponding to an infinite reduction path R. Let τ and θ be the associated truncation and truncated proof in µMLL ∞ τ . We set Froz(β) to be the set of occurrences of β which are never principal. For convenience we will use the weakening rule:

⊢ Γ (W) ⊢ Γ, ∆
Weakening is indeed admissible as long as the derivation on which it is applied contains an infinite branch, since one can let the weakened occurrences "travel" into this infinite branch. Without loss of generality, we now assume that all occurrences of Froz(β) have been weakened away in β.

We define the truncation τ ′ to be the truncation obtained by extending τ as follows. For every occurrence

F 1 F 2 which is principal in β, we set, for i ∈ {1, 2}, τ ′ (F i ) = 0 if F i ∈ Froz(β).
Let β ≥i be the suffix of β starting from the i th element. If ⊢ Γ is the conclusion of β ≥i , then for every ∆ ⊆ Γ, we define coinductively the proof β ≥i ⊥ (∆) of conclusion ⊢ ∆ ⊥ as follows. We proceed by case analysis on the rule applied to the conclusion of β. This rule can be either a logical rule or a weakening. If the rule is a weakening, then it is simulated by a weakening rule. If it is a logical rule, then let F be its principal occurrence. We set ∆ ′ = ∆ \ {F }. We have either:

• F = σX .G where σ ∈ {µ, ν }. We set σ to be the dual of σ , and:

β ⊥ ≥i (∆) = β ⊥ ≥i+1 (∆ ′ , G[F /X ]) ⊢ ∆ ′⊥ , G ⊥ [F ⊥ /X ] (σ ) ⊢ ∆ ′⊥ , F ⊥ • F = G ⊗ H . Suppose wlog. that G ∈ s i+1 (i.e.
, H left the branch β). We set ∆ ′′ = ∆ ′ ∩ s i+1 and:

β ⊥ ≥i (∆) = β ⊥ ≥i+1 (∆ ′′ , G) ⊢ ∆ ′′⊥ , G ⊥ (W) ⊢ ∆ ′⊥ , G ⊥ , H ⊥ ( ) ⊢ ∆ ′⊥ , F ⊥ • F = G H and G ∈ Dom(τ ′
) and H Dom(τ ′ ), or symmetrically. We set:

β ⊥ ≥i (∆) = (τ ′ ), (⊤) ⊢ G ⊥ β ⊥ ≥i+1 (∆ ′ , H ) ⊢ ∆ ′⊥ , H ⊥ (⊗) ⊢ ∆ ′⊥ , F ⊥ • F = G H , G ∈ Dom(τ ′
) and H ∈ Dom(τ ′ ). In this case we set:

β ⊥ ≥i (∆) = (τ ′ ), (⊤) ⊢ G ⊥ (τ ′ ), (⊤) ⊢ ∆ ′⊥ , H ⊥ (⊗) ⊢ ∆ ′⊥ , F ⊥ • F = G H , G Dom(τ ′
) and H Dom(τ ′ ). In this case we set:

β ⊥ ≥i (∆) = β ⊥ ≥i+1 (G) ⊢ G ⊥ β ⊥ ≥i+1 (∆ ′ , H ) ⊢ ∆ ′⊥ , H ⊥ (⊗) ⊢ ∆ ′⊥ , F ⊥
Observe now that β ⊥ := β ⊥ ≥0 is a proof in the truncated proof system µMLL ∞ τ ′ of conclusion A ⊥ . Indeed, its threads (which are necessarily straight threads since no cuts and axioms are involved) are the duals of the threads of the branch β, which are by hypothesis not valid.

Since µMLL ∞ τ ′ is sound, we have that A ⊥ = ⊤. But the truncated proof θ is a µMLL ∞ τ proof of conclusion A, and again by soundness we have that A = ⊤: contradiction. □

A.5 Extending µMLL ∞ cut-elimination to the additives

In this appendix, we give details on the proof of cut-elimination theorem for full µMALL ∞ . First, we provide precise definition for the sliced proof system and the associated partial cut-reduction relation and introduce persistent slices. We can then formulate precisely the additive validity criterion and prove the cut-elimination theorem. The proof schema of additive cut-elimination follows the same pattern as in the multiplicative case but we check that the multiplicative result can indeed be lifted. Most of the definitions can be very straightforwardly lifted to the additive but for the soundness result some work has to be done: we show that we do not need a full soundness result but that a soundness result wrt.

a specific class of derivations, called τ -adapted proofs, which then allows us to prove productivity of cut-elimination and preservation of validity by fair-reduction sequences.

A.5.1 Sliced proof system and its cut-reduction

To solve the previous issue, we will make use of slices, originally introduced by Girard in his seminal paper and later used in the analysis of interaction and cut-elimination of linear logic in the setting of Ludics [START_REF] Girard | Locus Solum[END_REF][START_REF] Terui | Computational ludics[END_REF] or in the design of additive proof-nets [START_REF] Dominic | Proof nets for unit-free multiplicative-additive linear logic[END_REF].

Definition A.19 (Additive slice). A sliced pre-proof is a pre-proof built on a variant of µMALL ∞ , µSMALL ∞ , where the inference rule ( ) has been replaced by the following two rules:

⊢ A, Γ ( 1 ) ⊢ A B, Γ ⊢ B, Γ ( 2 )
⊢ A B, Γ Definition A.20 (Slicing of a pre-proof). To a µMALL ∞ sequent (pre-)proof, one can associate a set of slices by keeping, for each ( ) inference, only one of its premisses and replacing the by the corresponding inference in ( 1 ), ( 2). More precisely, a slice of π is any µSMALL ∞ derivation obtained from π by applying corecursively one of the following two reductions (the other inferences are treated homomorphically):

π 1 ⊢ A 1 , Γ π 2 ⊢ A 2 , Γ ( ) ⊢ A 1 A 2 , Γ -→ π 1 ⊢ A 1 , Γ ( 1) ⊢ A 1 A 2 , Γ , π 2 ⊢ A 2 , Γ ( 2) ⊢ A 1 A 2 , Γ that is: Sl π 1 ⊢ A 1 , Γ π 2 ⊢ A 2 , Γ ( ) ⊢ A 1 A 2 , Γ =        π ′ i ⊢ A i , Γ ( i) ⊢ A 1 A 2 , Γ , π ′ i ∈ Sl(π i ), i ∈ {1, 2}       

A.5.2 Cut-reductions for sliced proofs

Cut-reduction rules for slices of µSMALL ∞ are identical to those for µMALL ∞ except for the sliced additives. In this case, one may have a problematic situation when a ( 1 ) shall interact with a (⊕ 2 ): cut-elimination cannot be performed. Among the several ways to cope with this problem, we choose here to introduce a special inference, (Ω), a generalized axiom rule allowing to derive any sequent, which denotes the fact that a bad interaction occurred.

(Ω) ⊢ Γ This does not impact the technical development since this serves essentially the purpose of defining those slices which avoid the mismatch.

Considering the (Ω) inference, cut-reductions for slices are specified as follows 9 : Definition A.21 (Cut reductions for slices). The sliced additive principal case is reduced as follows, if

{A ⊥ 1 A ⊥ 2 , A ′ 1 ⊕ A ′ 2 } ∈ |= , with r = (princ, {A ⊥ 1 A ⊥ 2 , A ′ 1 ⊕ A ′ 2 }). C π i ⊢ A ⊥ i , Γ ( i ) ⊢ A ⊥ 1 A ⊥ 2 , Γ π ′ j ⊢ A ′ j , Γ (⊕ j ) ⊢ A ′ 1 ⊕ A ′ 2 , ∆ mcut(ι, ⊥ ⊥) ⊢ Σ -→ r                    (Ω) ⊢ Σ if i j C π i ⊢ A ⊥ i , Γ π ′ i ⊢ A ′ i , ∆ mcut(ι, ⊥ ⊥ ′ ) ⊢ Σ if i = j where |= ′ = |= ∪ {{A ⊥ i , A ′ i }}
Notions of b-paths and ϵ-paths can be naturally extended to additive slices.

A.5.3 Persistent slices

To state the validity criterion for the additives, one needs to describe persistent slices that will never produce a (Ω): Definition A.22 (Persistent slice). Given a slice π , a ( i ) rule of principal formula A 1 A 2 occurring in π is said to be well-sliced if no b-path starting down from the A 1 A 2 occurrence of this sequent ends in a A ⊥ 1 ⊕ A ⊥ 2 which is the principal formula of a (⊕ j ) inference with i j. A slice is persistent if all its ( i ) occurrences are well-sliced.

Lemma A. [START_REF] Dominic | Proof nets for unit-free multiplicative-additive linear logic[END_REF]. In a persistent slice, ( i ) rules are characterized by the following property: (i) either there exists a b-path starting in A i , (ii) or there is a maximal pre-thread t starting from A i such that w(t) is prefix of a word in ends in the conclusion sequent or in the conclusion of a ⊤ rule (iii) or no such maximal pre-thread t (starting from A i such that w(t) is prefix of a word in B) exists and they mutually extend into an infinite pre-thead.

Proof. By case distinction, the fourth case being disabled by the condition of well-sliced ( i ) rules. □

In establishing the cut-elimination result, an intermediate proof system will be useful, that of partially sliced µMALL ∞ pre-proofs, in which both ( ), ( 1) and ( 2 ) occur:

The reader will notice that the additive -inferences occurring in the trace of a reduction path will always be sliced inferences (( 1 ) or ( 2 )).

Proposition A.24. All reducts of a persistent slice are (Ω)free.

Proof. The property relies on the simple observation that (i) any cut-reduction step from a persistent slice results in a persistent slice and (ii) if there is a reduction step from slice S which creates a (Ω) rule, then S is non-persistent. □ Proposition A.25 (Pull-back property). If π → * π ′ (resp. π → ω π ′ ) and S ′ is a slice of π ′ , then there is a slice S of π such that S → * S ′ (resp. S → ω S ′ ).

Proof. In the case of the finitary reduction, this is a wellknown property of slices.

For the infinite fair reductions, it results from the fact that fair reductions are strongly convergent in the sense of infinitary rewriting. As a consequence, for any position in the resulting slice, one can find a finite prefix of the reduction sequence which produces it and we can trace it back to a set of slices of the original proof which can produce this prefix. The intersection of all those sets define a non-empty set of slices of which any element can be considered. The obtained slice is of course persistent since it reduces to S ′ . □

A.5.4 Additive bouncing validity criterion

Definitions 4.1 and 4.5 of (pre-)threads directly adapt to the additives as they are not specific to the multiplicative fragment.

Definition A.26 (Validity). A slicing is valid if it is persistent and if it is valid in the multiplicative sense 10 . A µMALL ∞ pre-proof π is valid if all its persistent slicings are valid.

A.5.5 Additive cut-elimination theorem

We now state the cut-elimination theorem and give a schema of the proofs.

Theorem A.27. Fair infinite cut-reduction on µMALL ∞ proofs is productive and produces valid proofs.

Schema of the proof For cut-elimination, the proof goes by contradiction: assuming that we have a non productive fair cut-elimination, we may assume that it consists only of internal reduction steps and the trace of this cut-elimination is actually a slice with open premisses. It is actually contained in a persistent slice of π . As a consequence, there is an infinite branch of π which is entirely visited by the trace and this branch is visited by a thread thanks to additive validity. By adapting the truncated proof system to the additives and proving a restricted soundness result, we transform the valid persistent slice in a truncated derivation of the empty sequent by pruning the conclusion formulas which are never principal in the trace, from which results the contradiction.

For proving validity, it goes also by contradiction: assume the produced cut-free proof of ⊢ F π ′ contains a persistent slice S ′ containing an invalid branch β ′ . By the pull-back property, we find a persistent slice S of π reducing to S ′ which is valid by assumption. From the invalid branch β ′ one can build a cut-free proof β ′⊥ of ⊢ F ⊥ together with a truncation τ ′ ensuring that F is interpreted a 0 while validity of S and adaptation wrt. τ ′ ensures that F is interpreted as ⊤, a contradiction.

We now establish productivity of µMALL ∞ cut-elimination:

Theorem A.28. Fair reduction sequences of µMALL ∞ are productive.

To do so, first notice that the following notions of appendix A.4 can be straightforwardly adapted to the additive case (or to additive slices):

• Definition A.7 and Lemma A.10 adapt without change to persistent slices as it is not specific to the multiplicative case (but persistency is needed). • Proposition 5.3 applies to the trace of a persistent slice π . • Missing and unjustified sequents can be extended to reduction paths of µMALL ∞ pre-proofs (non-sliced) for the ( ) connective as done already in [START_REF] Baelde | Infinitary Proof Theory: the Multiplicative Additive Case[END_REF]. • While truncations need no adaptation, the truncated semantics shall be adapted to the additives by adding the following clauses:

(φ ψ ) α E = φ α l E ∧ ψ α r E , (φ ⊕ ψ ) α E = φ α l E ∨ ψ α r E
• The truncated proof system is extended in the most natural way (as in [START_REF] Baelde | Infinitary Proof Theory: the Multiplicative Additive Case[END_REF]). • Truncation induced by a reduction path is lifted to the additive case and it is well-defined since the additive inference would simply add a tricky case of missing sequent for a premiss erased when reducing a (Cut)/( ) cut but there cannot be an ϵ-path in this case. Therefore the only case to treat is that of distinguished occurrences of unjustified sequents of type 1 which works as for the multiplicative. As for adapting soundness (Prop. A.13), we actually do not need the full soundness result but only soundness wrt. a class of derivations that we introduce now:

Definition A.29. Given a truncation τ , a τ -adapted µMALL ∞ τ derivation π is a µMALL ∞ τ pre-proof such that (i) for all (φ ψ ) α occurring in π , either α ∈ Dom(τ ) or {αl, αr} ∩ τ -1 (⊤) ∅. (ii) given a ( ) occurring in π of conclusion sequent s and principal formula (φ 1 φ 2 ) α , if αl Dom(τ ) (resp. αr Dom(τ )) there is no b-path starting down from the (φ 1 φ 2 ) α occurrence of s ending in a (φ ⊥ 1 ⊕ φ ⊥ 2 )
β which principal formula of a (⊕ j ) inference with i j.

We will use soundness for τ -adapted proofs: Proposition A.30. Given a truncation τ and a valid τ -adapted µMALL ∞ τ derivation π of conclusion ⊢ Γ, there exists a formula F ∈ Γ such that F = ⊤.

Proof. The soundness proof for µMLL ∞ τ of proposition A.13 can be extended to this setting: first notice that the relation ≤ on pointed sequents that is used to transfer the marking through ϵ-path can be extended and we will use it in the following consistently with the underlying slice τ -adaptation suggests.

Construction of (s i ) shall now treat the additive inferences: (i) for the (⊕) rule, nothing is to be changed since the rule is unary: s i+1 is the premiss of s i ; (ii) for the ( ) inference on s i of principal occurrence G = H K, we reason as in [START_REF] Baelde | Infinitary Proof Theory: the Multiplicative Additive Case[END_REF]: since [f i (G)] = 0 and f i (G) is of the form H m K m where H m and K m are marking of H and K respectively, then either [H m ] = 0 or [K m ] = 0. Moreover, by τ -adaptation, we know that the address of one of H, K is in τ -1 (⊤) and therefore we necessarily choose the other disjunct suppose w.l.o.g. that [H m ] = 0. We set s i+1 to be the premiss of s i that contains H .

The definition of the sequence of markings (f i ) is trivially extended (more precisely the clauses for the and ⊕ are those used in [START_REF] Baelde | Infinitary Proof Theory: the Multiplicative Additive Case[END_REF].

The multiplicative soundness argument can be carried over in this setting since by τ -adaptation, the branch we have built is part of the persistent valid slice induced by τ (that is the purpose for the τ -adaptation requirement) and we therefore have a thread for which the decreasing sequence of ordinal can be applied concluding soundness for those derivations. □ Note that even this restricted soundness for the truncated µMALL proof-system ensure soundness for the (untruncated) µMALL ∞ b-valid proofs. Indeed, assuming some valid proof π derives a sequent S which can be valued to ⊥. One can define a truncation τ for which π is τ -adapted and such that for any formula which is principal in π and interpreted as false, at least one of its premisses interpreted as false is not in the domain of the truncation, which is possible thanks to inhabitation of any persistent slice by a bouncing thread. From which the previous result can be applied providing the desired contradiction. Hence: Theorem A.31. µMALL ∞ is sound for the boolean semantics.

We can finally establish productivity of cut-elimination:

Proof. Let π be a µMALL ∞ valid proof. By contradiction, assume that π has a fair infinite sequence of internal reductions. Wlog. we can assume that all reductions steps from π are internal.

For each ( ) inference of π , the trace of this cut-elimination contains at most one premiss ie. it is contained in a slice: one can actually find a persistent slice S which contains the trace.

The previous remark ensures that for each formula principal in the trace, the truncation τ of the reduction path contains one of its subformulas in its domain and that the truncated proof π τ associated with the trace is τ -adapted.

Since the reduction contains only internal reductions, the conclusion formulas of π τ are never principal in the π τ and therefore we can erase them resulting in π ′ τ which is a τadapted µMALL ∞ τ valid derivation of the empty sequent which cannot be by soundness (prop A.30). □ Theorem A.32. Given π a µMALL ∞ proof, any fair mcutreduction from π produces a µMALL ∞ proof.

Proof. Let π be a µMALL ∞ m proof of conclusion ⊢ F and π ′ the cut-free pre-proof resulting from the previous property.

By contradiction, assume π ′ is non-valid. That means there exists a slice S ′ of π ′ (π ′ is cut-free so there is no persistency assumption applying here) and an infinite branch β ′ of S ′ such that β ′ is supported by no valid thread. By the pull-back property, S ′ has been built by reducing a persistent slice S of π and therefore β ′ corresponds to a reduction path from S. Since we are working in a persistent additive slice, the multiplicative validity can be extended in order to extract an infinite branch β invalid in S. The construction of the proof β ′⊥ used to obtain the contradiction is lifted to the additive case as follows:

• first one shall define truncation τ ′ not only by considering the occurrences of F 1 F 2 which are principal in β ′ , but also those of F 1 ⊕ F 2 and extend the truncation to τ ′ (F i ) = 0 if F 1 ⊕ F 2 is the principal occurrence of a (⊕ j ) rule with i j. • then the construction of the dual of branch β, β ⊥ , is extended with the following clauses to the definition of page 20:

-F = G H . Suppose wlog. that G ∈ s i+1 (i.e., H left the branch β). β ⊥ ≥i (∆) = β ⊥ ≥i+1 (∆ ′ , G) ⊢ ∆ ′⊥ , G ⊥ (⊕ 1 ) ⊢ ∆ ′⊥ , F ⊥ -F = G ⊕ H and G ∈ Dom(τ ′
) and H Dom(τ ′ ). We set:

β ⊥ ≥i (∆) = (τ ′ ), (⊤) ⊢ ∆ ′⊥ , G ⊥ β ⊥ ≥i+1 (∆ ′ , H ) ⊢ ∆ ′⊥ , H ⊥ ( ) ⊢ ∆ ′⊥ , F ⊥
β ′⊥ is cut-free and valid (therefore valid in the sense of [START_REF] Baelde | Infinitary Proof Theory: the Multiplicative Additive Case[END_REF]) since its threads are dual of the threads of β (which are invalid).

β ′⊥ is τ ′ -adapted (as β ⊥ is cut-free, this amounts to checking that the appropriate premiss of each ( ) has its formula in the domain of τ ′ which is by design) and by proposition A.30, we conclude the desired contradiction since one the one hand we have F = ⊤ and on the other hand we have F ⊥ = ⊤. □

A.6 (Un)decidability properties

In this appendix, we prove the undecidability of the general bouncing criterion and introduce a hierarchy of decidable sub-criteria.

Proof of decidability for the bounded height criterion

We start by detailing some structure of proofs, via the notion of shortcut.

Definition A.33. A shortcut is a finite pre-thread t = uv where w(u) ∈ W * A and v is a b-path. A shortcut t is minimal if no strict prefix of t is a shortcut.

Notice that if t is a shortcut, then t is an ϵ-path.

We will note (F , s) a pointed sequent: s is a sequent of the proof, and F ∈ s. We want to be able to follow threads where shortcuts have been removed. These threads behave like straight threads, except on cuts where they are allowed to jump from the starting point of a shortcut to its end. We will now formalize a description of such "jumping" threads.

Let Σ jump = {W, i, l, r, c l , c r }, where c l (resp. c r ) stands for left (resp. right) cut occurrences. A word τ ∈ Σ * jump will be called a relative address. If P is a pre-proof and (F , s) is a pointed sequent of P, then a relative address τ points to another pointed sequent τ @(F , s) in P. We define this by induction on τ :

• If τ = ϵ then τ @(F , s) = (F , s). • If τ = Wτ ′ then τ @(F , s) = τ ′ @(F , s ′ )
, where s ′ is the premiss of s containing F .

• If τ = iτ ′ , F = σX .G (for some σ ∈ {µ, ν }) is principal in s with premiss s ′ , then τ @F = τ ′ @(G[F /X ], s ′ ). • If τ = lτ ′ (resp. τ = rτ ′ ), F = G ⋆ H (for some ⋆ ∈ { , ⊗}) is principal in s, then τ @(F , s) = τ ′ @(F ′ , s ′ )
where

F ′ = G (resp. F ′ = H ) and s ′ is the premiss of s containing F ′ . • If τ = c l τ ′ (resp. τ = c r τ ′ )
, and the rule applied to s in P is a cut, then τ @(F , s) = τ ′ @(F ′ , s ′ ), where F ′ is the occurrence introduced by the cut on the left (resp. right) premiss s ′ of this cut. • Otherwise, τ @(F , s) is undefined.

Lemma A.34. Let P be a circular pre-proof. If t is a minimal shortcut from (F , s) to (F ′ , s ′ ), then F ≡ F ′ . Moreover, there is a relative address τ such that (F ′ , s ′ ) = τ @(F , s). This τ is called the effect of t and noted effect(t). For each pointed sequent (F , s), there is at most one minimal shortcut starting in (F , s) Proof. Since the weight of minimal shortcut starts with W * A, no choice is possible before an axiom is encountered. When going downwards, constraints will be pushed on the constraint stack, and the shortcut is again uniquely defined. When going upwards (i.e. after having seen a cut, and before the next axiom), two cases can occur. Either the constraint stack is not empty, and therefore it uniquely determines the path followed by the shortcut, or it is empty, which marks the end of the minimal shortcut t. The relative address τ is given by the position of the end of t relatively to the beginning of t in the proof tree. The fact that F ≡ F ′ follows from the fact that any shortcut is an ϵ-path. □

If P is a pre-proof and (F , s) is a pointed sequent in P, we note short(F , s) the minimal shortcut starting in (F , s) if it exists. If not, we fix short(F , s) := ϵ. We also fix effect(ϵ) = ϵ. We will abbreviate effect(short(F , s)) by effect(F , s) to lighten notations.

Remark 2. If P is a circular pre-proof, and (F , s), (F ′ , s ′ ) are two pointed sequents of P corresponding to the same occurrence in the finite graph of P, then effect(F , s) = effect(F ′ , s ′ ).

This remark allows us to compute only finitely many effects: one for each pointed sequent in the finite proof graph. Definition A. [START_REF] Santocanale | A Calculus of Circular Proofs and Its Categorical Semantics[END_REF]. An s-thread is a sequence (F i , s i , ↑) i ∈ω that obeys the same rules as a thread going only upwards, with some relaxation in the constraints between (F i , s i , ↑) and (F i+1 , s i+1 , ↑) defining a pre-thread. Indeed we add a new clause allowing the s-thread to take minimal shortcuts: (F i+1 , s i+1 ) can be reached from (F i , s i ) following the relative address effect(F i , s i ), i.e. (F i+1 , s i+1 ) = effect(F i , s i )@(F i , s i ).

The weight of an s-thread is defined by generalizing the definition of weight of a thread, matching this new clause with w i = W. The notion of visible part and validity of an s-thread is then induced by this definition.

Notice that the visible part of an s-thread is obtained by simply removing steps introduced by this new clause, corresponding to shortcuts.

Lemma A.36. An infinite branch is validated by a thread if and only if it is validated by an s-thread.

Proof. The s-thread is obtained from the thread by compressing minimal shortcuts and replacing them with the new clause. Conversely, the thread can be obtained from the sthread by replacing the new clause with minimal shortcuts. This transformation preserves the visible part.

□

We now give the proof of Theorem 6.5, stating that any valid proof of µMLL ω is a k-proof for some k ∈ N.

Proof. Let P be a valid proof of µMLL ω . Each pointed sequent in P can be annotated with its effect, and with the height of its minimal shortcut (or with (ϵ, 0) if this minimal shortcut does not exist).

By Lemma A.36, all infinite branches of P are validated by s-threads, following effects annotating P. Let k be the maximal height annotating a pointed sequent in P. We obtain that P is a k-proof. □

The rest of the section is devoted to proving Theorem 6.6, stating that given a pre-proof P and an integer k, it is decidable whether P is a k-proof.

Proof. Let us note

effect k (F , s) = effect(F , s) if short(F , s) has height ≤ k ϵ otherwise
For each (F , s) in the graph, effect k (F , s) can be computed in a finite time. Indeed, it suffices to follow the only possible thread starting in (F , s) in the graph of P, until we find a minimal shortcut or we detect a failure. Reasons for failure are:

• The weight does not begin with W * A, i.e. an unfolding happen before the first axiom,

• the constraint stack gets higher than k,

• we detect a loop: the same pointed sequent is visited twice with identical stack content.

This corresponds to turning the automaton A thread into a DFA, by bounding the size of the stack to k, and accept words of the form W * AΣ * C by empty stack. This allows us to annotate each pointed sequent (F , s) with effect k (F , s).

We can now verify that the pre-proof is a k-proof, using a nondeterministic parity automaton A s reading branches of P and guessing the existence of an s-thread. This automaton is identical to the one in [START_REF] Doumane | Théorie de la démonstration infinitaire pour les logiques à points fixes)[END_REF] for straight threads, except that it can follow effects. While following the relative address given by an effect, the thread is considered hidden, and the action preformed on it does not influence the accepting condition of A s . Since the length of effects is globally bounded (there are finitely many of them), the relative adresses to follow can be stored in the state space of the automaton. The pre-proof P is a k-proof if and only if A s accepts all branches. □

A.6.1 Details on the undecidability proof

We show that the validity condition is already undecidable for the proof system µMLL ω . We reduce from the halting problem for two-counter machines (2CM), known to be Σ 0 1 -complete [START_REF] Minsky | Recursive Unsolvability of Post's Problem of "Tag" and other Topics in Theory of Turing Machines[END_REF]. Here is a brief outline of the proof. We start by recalling the definition of 2CM in the next section. These are finite-state deterministic machines manipulating two counters, able to perform Zero test, increment and decrement on each counter.

We then show how to encode the halting problem of a 2CM M using bouncing threads. The idea is to use the constraint stack to encode the value of counters, and position in the graph to encode the control state. Gadgets allow to increment or decrement each counter. The main difficulty lies in the tests performed by the machine: we want to design a conditional branching on the thread, depending on the value of the constraint stack. This can be done, but because of the linearity of the proof system, we cannot avoid leaving some extra constraints encoding the results of the tests, that will be collected by the thread later. Since we want to finish with empty constraint, we need to erase this extra information. To do this, we add a second gadget performing the computation in a dual way: results of tests are fed to the thread, that rewinds the computation while erasing these extra constraints. We can finally exit the detour with (almost) no constraints, and perform a visible ν -unfolding on the main branch, before looping back to the root of the proof.

The global pre-proof will be a valid proof according to the criterion if and only if the machine M halts.

Two Counter Machines

A 2CM M is a tuple (Q, q 0 , q f , δ ) where Q is a finite set of states, q 0 is the initial state, q f is the final state, and δ is the transition function. The machine has access to two counters storing nonnegative integer values. The counters are initialized to 0.

The possible actions of the machine are the following, where τ ∈ {1, 2} identifies one of the counters:

• Inc τ (q) : increment counter τ , and jump to state q • Dec τ (q) : decrement counter τ , and jump to state q • Test τ (q Z , q P ): if the current value of counter τ is 0, jump to q Z , else jump to q P . Let Act = {Inc τ (q) | τ ∈ {1, 2}, q ∈ Q } ∪ {Dec τ (q) | τ ∈ {1, 2}, q ∈ Q } ∪ {Test τ (q Z , q P ) | τ ∈ {1, 2}, q Z , q P ∈ Q } be the set of possible actions.

The transition function of M is a function δ : Q \ {q f } → Act, specifying which action is executed when each state is reached. No action is mapped to q f , since the run stops when q f is reached.

A configuration of the machine M is a triple (p, k [START_REF] Abel | Mixed inductive/coinductive types and strong normalization[END_REF], k [START_REF] Abel | Compositional Coinduction with Sized Types[END_REF]) ∈ Q × N 2 specifying the current state and the values for the two counters.

A run of the machine M is a sequence of configurations

(p i , k[1] i , k[2] i ) 0≤i ≤n such that p 0 = q 0 , k[1] 0 = k[2] 0 = 0, p n = q f ,
and consistent with δ , i.e. for all i ∈ [0, n -1] :, we have

• if δ (p i ) = Inc τ (q) then p i+1 = q and k[τ ] i+1 = k[τ ] i + 1. • if δ (p i ) = Dec τ (q) then p i+1 = q and k[τ ] i+1 = k[τ ] i - 1. • if δ (p i ) = Test τ (q Z , q P ), then k[τ ] i+1 = k[τ ] i , and -if k[τ ] i = 0 then p i+1 = q Z . -if k[τ ] i > 0 then p i+1 = q P .
In all cases the other counter is left unchanged, i.e.

k[3 - τ ] i+1 = k[3 -τ ] i
Without loss of generality, we can also assume that the run ends with both counter values equal to 0, i.e. k [START_REF] Abel | Mixed inductive/coinductive types and strong normalization[END_REF]

n = k[2] n = 0.
The next theorem states that the halting problem is undecidable for Two Counter Machines.

Theorem A.37. [START_REF] Minsky | Recursive Unsolvability of Post's Problem of "Tag" and other Topics in Theory of Turing Machines[END_REF] Given a Two Counter Machine M = (Q, q 0 , q f , δ ), it is undecidable to determine whether M has a run, by a reduction from Turing Machines halting problem.

From machines to proofs

We will now encode the halting problem for 2CM into the problem of deciding whether a pre-proof is a proof.

We fix a machine M = (Q, q 0 , q f , δ ).

We will build a pre-proof P such that the leftmost infinite branch can be validated by a bouncing thread if and only if there exists a run of the machine M. All the other branches of P will be validated by non-bouncing threads.

We will use throughout the proof the formulas F , G, where F = νX .(X X ), G = F ⊥ = µX .(X ⊗X ), and auxiliary formulas A = νX .(X X )⊗X and B = µX .(X A A). Their addresses will sometimes be omitted, keep in mind that a letter can represent different occurrences in a proof tree.

The thread will always follow a formula F when going upwards, and G when going downwards. The formula A will be used to ensure that all infinite branches except the leftmost one are validated by non-bouncing threads.

The conclusion of the proof P is the sequent G, F , B.

The idea of the construction is to use a bouncing thread to encode a run of M, by storing the current configuration on M in the stack of constraints that the thread must satisfy.

The general shape of the pre-proof P is given in Figure 13. By convention, formulas introduced in cuts will always be F on the left and G on the right. This means that a thread going upwards following a formula F will always turn right on cuts, bounce on axioms in the right part, and finally come back to visit the left part of the cut.

Auxiliary formulas are grayed to emphasize the trajectory of the thread of interest.

The thread on the branch with infinitely many (⋆) must use formula F , as it is the only one performing a ν -unfolding. This means it has to go through the two cuts and bounce on axioms in π M and π R . All other infinite branches are validated by non-bouncing threads.

As described in the outline, the goal of π M is to use the bouncing thread stemming from F to simulate a run of M in a deterministic way, accumulating "garbage constraints" for every test. The role of π R is to erase these garbage constraints, by mirroring the behaviour of π M .

After π R , the formula F is unfolded twice before looping back to the root. The first unfolding is used to match a leftover constraint, that cannot be erased in π R for technical reasons detailed later. The second unfolding contributes to the visible part of the thread.

Encoding of counters in the constraint stack

We describe here how the pre-proof π M will be able to simulate a run of M via a thread following formula F .

When F is unfolded, a thread following F can either go to the left disjunct or to the right, corresponding to weights il or ir. We will use the alias l for il and r for ir, since unfoldings will always alternate with left/right choices. We will refer to the word u ∈ {l, r} * storing the current constraints as the constraint stack. For instance if the constraint stack u is of the form lv, then when the thread goes up and encounters an unfolding of F , it has to follow the left disjunct, and update the constraint stack from u to v. Constraints are updated according to the stack of the pushdown automaton A thread described in Section 6.1.

We are now ready to detail how configurations of the machine will be encoded in the constraint stack. A counter of value n will be encoded by the sequence of constraints (rl n r). Therefore, when the thread is simulating the run of M, its constraint stack is of the form (rl n r)(rl m r) to denote that k

(Ax) ⊢ G l , F l ⊢G rl , F rl , B (Ax) ⊢ G rr , F rr (µ, ν, , ⊗) ⊢ G r , F r , B (µ, ν, , ⊗) ⊢ G, F , B π R ⊢ G, F , A (Cut) ⊢ G, F , B, A π M ⊢ G, F , A (Cut) ⊢ G, F , B, A, A (µ, ) ⊢ G, F , B
[1] = n and k[2] = m.
The current state is not encoded in the constraint stack, but in the current position of the thread in the pre-proof: for instance if the thread is in the node labeled (q 0 ) in the proof graph, then the current state of the corresponding run is q 0 . "Garbage constraints" are constraints that will not be part of the constraint stack during the simulation of the run of M, but will be pushed on the stack by the thread when the simulation has succeeded, i.e. after the node labeled (q f ) has been reached by the thread. In order to exit the cut, the thread must go down from (q f ) to (q 0 ), and that is where garbage constraints may be pushed. These extra constraints will encode the results of all tests performed during the computation. The result of a test is r if the tested counter was Zero, and l otherwise, so in general it is a letter X ∈ {r, l}. Garbage constraints will be of the form rX for a test on the first counter, and of the form rl k rrX for a test on counter, where X is the result of the test and k is the value of the first counter.

Auxiliary metarules for π M

In order to make the construction readable and modular, we start by describing metarules that will be used as building blocks throughout the section.

Rules relative to A

We will use the ∞ notation to denote an infinite tree obtained by unfolding a proof of A. This yields a valid cut-free proof tree that contains no axiom.

We explicit this from sequent Γ, A, where Γ can be any sequent.

(∞) ⊢ Γ, A ≡ (△) (♠) (♠) (⊗, ) ⊢ A, (A A)⊗A (ν ) (♠) ⊢ A, A (⊗, ) ⊢ Γ, (A A)⊗A (ν ) (△) ⊢ Γ, A
We will often want to duplicate A using its connective. Let us define the following metarule, valid for any sequent Γ, A:

⊢ Γ, A, A ( A ) ⊢ Γ, A ≡ ⊢ Γ, A, A ( ) ⊢ Γ, A A (∞) ⊢ A (⊗) ⊢ Γ, (A A)⊗A (ν ) ⊢ Γ, A
We will define an alias for a cut rule allowing to duplicate the A formula on both sides, noted (Acut). The effect of rule (Acut) is simply a cut for formulas F , G, so it can be considered as such for threads of interests following F upwards and G downwards.

⊢ G, F , A ⊢ G, F , A (Acut) ⊢ G, F , A ≡ ⊢ G, F , A ⊢ G, F , A (Cut)
⊢ G, F , A, A

( A ) ⊢ G, F , A

Copying left and right constraints

We now describe a helpful metarule: the expanding rule (exp), represented in Fig. 14. It allows to unfold F and G once, pairing the left (resp. right) unfolding of F with the left (resp. right) unfolding of G. This ensures that if the thread goes left (resp. right) upwards on F , it will also go left (resp. right) downwards on G. This can therefore be understood as a copying operator: the bit of the constraint stack will be the same before and after bouncing on the current cut. As before, we will gray formulas that will always be avoided by the thread of interest. In most constructions, the left (resp. right) conjunct of F will be paired with the left (resp. right) conjunct of G when both are expanded, so we will often omit the labels. The left expansions will be represented on the left branch of the proof.

We give metarule (l) (resp. (r)) forcing the reading and copying of a left (resp. right) constraint on the stack. This is enforced by preventing the thread from bouncing on an axiom if the forbidden bit is read, thanks to the axiomless infinite proofs described by the (∞) metarules.

⊢ G l , F l , A ⊢ G r , F r , A (exp) ⊢ G, F , A ≡ ⊢ G l , F l , A ⊢ G r , F r , A (⊗) ⊢ G l ⊗G r , F l , F r , A, A (µ, ν, ) ⊢ G, F , A, A ( A ) ⊢ G, F , A Figure 14. the metarule (exp) ⊢ G, F , A (l) ⊢ G, F , A ≡ ⊢ G l , F l , A (∞) ⊢ G r , F r , A (exp) ⊢ G, F , A ⊢ G, F , A (r) ⊢ G, F , A ≡ (∞) ⊢ G l , F l , A ⊢ G r , F r , A (exp)
⊢ G, F , A

Constraint introduction

We might also want to push a right constraint without popping one. For instance this is needed at the beginning when the stack is empty. This can be done via the following metarules π r i and (r i ), where i stands for "Introduction". We define both variants because we might want to use one or the other depending on the context. Let π r i be the following pre-proof:

π r i ⊢ G, F , A ≡ (∞) ⊢ G l , A (Ax)
⊢ G r , F

⊗) ⊢ G l ⊗G r , F , A (
⊢ G, F , A This pre-proof allows a thread to go upwards following F without any event, bounce on an axiom, and go downwards following G while pushing a right constraint.

We now combine π r i with a cut in order to go back to a thread going upwards, having a constraint stack starting with an extra r.

⊢ G, F , A (r i ) ⊢ G, F , A ≡ ⊢ G, F , A π r i ⊢ G, F , A (Acut) ⊢ G, F , A
This means that the effect of the rule (r i ) on the constraint stack can be summarized by ϵ → r, adding an extra r at the top of the constraint stack.

The above rule can be similarly defined to introduce a l constraint instead, by simply switching the G, F axiom to the left premiss instead of the right in π r i . This dual version will be noted by π l i and metarule (l i ).

The initialization metarule

We describe here the first metarule encountered in π M . Its role is to initialize the constraint stack to encode two counters with value 0, and go to the (q 0 ) node to start the simulation of the run of M.

It must therefore allow the thread to enter with empty constraint stack and exit the cut with a constraint stack (rr)(rr). This is straightforward now that we have the (r i ) rule:

(q 0 ) ⊢ G, F , A (init) ⊢ G, F , A ≡ (q 0 ) ⊢ G, F , A (r i ) ⊢ G, F , A (r i ) ⊢ G, F , A (r i ) ⊢ G, F , A (r i ) ⊢ G, F , A
In the following, we describe how to build the pre-proof π M , by connecting nodes of the form (p) to their successors in the computation. So for each p ∈ Q, a pre-proof of "local root" (p) will be built with hypotheses of the form (q) with q ∈ Q. Once such a pre-proof has been built for each node (p), the hypotheses (q) are connected to their corresponding "local root" node trough back loops.

Encoding the action Inc

We now assume that we are at a node of the proof graph labeled by (p), where p is a state of the machine M, and that the current constraint stack encodes the counter value as described earlier, i.e. (rl k [1] r)(rl k [2] r).

Assume δ (p) = Inc 1 (q) with q ∈ Q. We will build a metarule (Inc 1 ) updating the configuration by acting on the constraint stack, and ending up in node (q):

(q) ⊢ G, F , A (Inc 1 ) (p) ⊢ G, F , A ≡ (q) ⊢ G, F , A π l i ⊢ G r , F r , A (r)
⊢ G, F , A

(p) ⊢ G, F , A (Acut)
Notice that in order to bounce on the axiom, the thread must see r while going up, and rl on the way down. The rest of the current stack (of the form l * r(rl * r)) is left unchanged. This rule turns a stack of the form ru into rlu, thereby incrementing the first counter. We will abbreviate this action r → rl.

We might also need to increment the second counter, which is deeper in the stack. For this, let us devise another auxiliary metarule (counter), allowing us to skip the part of the stack encoding the first counter.

⊢ G, F , A (counter) ⊢ G, F , A ≡ ( †) ⊢ G rl , F rl , A ⊢ G rr , F rr , A (exp) ( †) ⊢ G r , F r , A (r)
⊢ G, F , A This metarule processes constraints of the form (rl * r) on the way up, and these same constraints will be copied back when the thread returns downwards from the formula G of the hypothesis. This means that this gadget allows the right premiss sequent to access the encoding of the second counter, while leaving the first one untouched.

We can now give the pre-proof allowing to increment the second counter, by simply adding the (counter) metarule at the appropriate place:

(q) ⊢ G, F , A (Inc 2 ) (p) ⊢ G, F , A ≡ (q) ⊢ G, F , A π l i ⊢ G r , F r , A (r)
⊢ G, F , A

⊢ G, F , A

(p) ⊢ G, F , A (Acut)
The effect of this metarule is (rl * r)r → (rl * r)rl This achieves the treatment of states performing an increment. For all nodes (p) where p performs an increment of counter τ before going to q, we link node (p) of the proof with node (q) through the metarule (Inc τ ).

Encoding the action Dec

Assume δ (p) = Dec 1 (q) with q ∈ Q.

This means we want to build a metarule with action rl → r on the stack, in order to decrease the value of the first counter by 1. This is done by the following metarule (Dec 1 ):

(q) ⊢ G, F , A (∞) G l , F l , F rr , A (Ax) G r , F rl (⊗) ⊢ G l ⊗G r , F l , F rl , F rr , A (ν, ) ⊢ G l ⊗G r , F l , F r , A (µ, ν, ) ⊢ G, F , A (Acut) (p) ⊢ G, F , A
Notice that if the thread does not start with rl, it gets lost in an (∞) proof, corresponding to a failure of the run.

If δ (p) = Dec 2 (q), the construction is similar, using again the metarule (counter) to leave the first counter untouched and access the second one. This is done by the following metarule (Dec 2 ).

(q) ⊢ G, F , A (∞) G l , F l , F rr , A (Ax) G r , F rl (⊗) ⊢ G l ⊗G r , F l , F rl , F rr , A (ν, ) ⊢ G l ⊗G r , F l , F r , A (µ, ν, ) ⊢ G, F , A (counter) ⊢ G, F , A (Acut) (p) ⊢ G, F , A

Encoding the action Test

It remains to describe how to modify the constraint stack for actions of type Test.

Test on the first counter

Let us assume first that δ (p) = Test 1 (q Z , q P ).

Notice that a zero test can be performed by simply testing whether the stack starts with rr or with rl, i.e. by identifying the second letter of the stack. Therefore, these first two letters can be used to branch to the result of the test. However, since they must be still be part of the encoding, we need to reintroduce them in the stack after having read them. We define the metarule (Test 1 ) accordingly:

(q P ) ⊢ G, F , A (l i ) ⊢ G, F , A (r i ) ⊢ G rl , F rl , A (q Z ) ⊢ G, F , A (r i ) ⊢ G, F , A (r i ) ⊢ G rr , F rr , A (exp) ⊢ G r , F r , A (r)
(p) ⊢ G, F , A This metarule allows the thread to go to (q Z ) if the counter was zero, or to (q P ) if the counter was strictly positive, leaving the stack unchanged in both cases.

Notice that this metarule also leaves some garbage constraints in the following sense: when going back down from (q Z ) (resp. (q P )) to (p), the thread will push extra constraints rr (resp. rl) on top of the pile, due to the (exp) and (r) rule in (Test 1 ).

Test on the second counter

We now assume that δ (p) = Test 2 (q Z , q P ), and we want to encode the corresponding metarule, linking (p) to (q Z ) and (q P ) in the pre-proof π M . This is more tricky, because we need to access the relevant bit encoding the result of this test, and copy the value of the first counter after it to restore the stack. This corresponds to copying an unbounded amount of information, so this cannot be done directly in the same way as in the previous construction for Test [START_REF] Abel | Mixed inductive/coinductive types and strong normalization[END_REF] .

We therefore design auxiliary gadgets allowing us to copy the information bit by bit. The result T of a test will be encoded by T = rrr for zero and T = rrl for not zero.

Bouncing threads for circular and non-wellfounded proofs

Long version of the LICS 2022 paper, 07/22, The pre-proof π shift , represented Fig. 15 has effect l k +1 T → l k T l, with T ∈ {rrr, rrl}. The proof can be built thanks to the following table, that explicits the transformation of the relevant prefix constraint stack: before: ll lrrl lrrr after:

ll rrll rrrl

Notice that all axioms in the right part of the cut in π shift are paired according to the table above.

The main interesting phenomenon in π shift occurs on the (•) loop. In the case where the result starts with l, this loop allows to enter the cut again, after the popping of one l constraint. This will therefore perform the wanted transformation on the constraint stack. Let us take an explicit example to see this gadget at work: consider a thread entering π shift with constraint u = llrrr. The thread will bounce on axiom G ll , F ll , leaving this constraint unchanged, and it will enter the (•) node with constraint lrrr. This time, the detour will enter π aux , and will pop lrrr and push rrrl onto the stack. When exiting the cut, the thread will have a constraint starting with r and therefore will immediately bounce on the axiom. When going back, it will push back the first l on the way down to the original root. It will finally exit with constraint lrrrl, which is the wanted result of the mapping l k T → l k -1 T l.

We can now iterate π shift in order to move the result T on top of the stack.

Let us start with an auxiliary metarule (copy l ) (Fig. 16) copying the first letter of the stack if it is l, and do nothing if the stack starts with r. I.e. it has action l → ll r → r on the stack. It will actually be the case that if the constraint starts with r, it starts with rr.

We now build the proof π move (Fig. 17), iterating π shift , allowing to copy an unbounded quantity of information past the test result T . The proof π move has the following action on the stack:

l k T → l k T l k r → r
. The principle is to first duplicate the leading l, so that the extra occurrence can be used to test whether we want to perform a shifting using π shift . If the stack starts with r (actually with rr), then the (copy l ) metarule will do nothing, and the thread will just bounce on the right axiom. This allows us to iteratively call π shift , until we reach the encoded result T . When exiting this gadget, the last π shift leaves constraint T l k , and one extra l is collected by each (⋆) loop. That is why the constraint afer π move is l k T l k . Another auxiliary metarule (prep) (Fig. 18) will allow us to prepare the input for π move from the standard counter encoding, i.e. performing action rl k rrX → rl k (rrX )rrX , with X ∈ {r, l}. The parenthesized expression is the T that we will want to move to the top. Notice that this corresponds to a copying of the counter rl k r, followed by a mapping rrX → rX rrX . The dots in Fig. 18 represents (∞) proofs, not detailed for concision.

Let us now combine these gadgets to define a metarule (result), moving the test result at the wanted place, while producing extra stack content before it. This metarule has action rl k T → l k T l k T , with T ∈ {rrl, rrr}, and leaves a garbage constraint r that will be seen later on the way down. We can finally build the metarule for Test 2 , performing the wanted test and leaving garbage constraint of the form rl k rrX with X ∈ {l, r}.

(♣) ⊢ G l , F l , A (q P ) ⊢ G, F , A (r i ) ⊢ G rrl , F rrl , A (q Z ) ⊢ G , F , A (r i ) ⊢ G rrr , F rrr , A (exp)
⊢ G rr , F rr , A The principle of this gadget is the following: after preparing the stack via the (result) metarule, the (♣) loops and the (r) rule first pop the garbage prefix l k rr. The following bit X ∈ {l, r} is the wanted test result, and allows us to enter (q Z ) or (q P ) with a remaining stack that encodes the next configuration of the machine (after adding the leading r to complete the valid encoding).

Final state q f

It remains to describe what happens to a thread entering the node labelled by the final state q f . We will simply allow it to finally bounce on an axiom, thereby starting a downwards path that will gather all the garbage constraints, exit π M , and enter the second cut and the proof π R .

We just need to evacuate the formula A from the sequent. Since we know that the constraint stack starts with r, this can be done in the following way:

(∞) ⊢ G l , F l , A (Ax) ⊢ G r , F r (µ, ν, , ⊗) (q f ) ⊢ G, F , A
• if the test is on the second counter, then u i = rl k rrX ,

where k is the value of the first counter at the time of the test.

Proof. It is straightforward to prove by induction of the length of the thread/run: a thread entering π M with empty constraint can reach node (p) with constraint (rl n r)(rl m r) if and only if their is a partial run of M reaching state p with counter values n, m. Moreover, the garbage constraints that will be pushed back from (p) on the way back to the root of π M encode the results of tests as described in the statement of the Lemma. The r 4 following garbage constraints is the constraint stack reached in (q f ) at the end of computation, encoding two counters of value 0, as we assumed M ends with this configuration. □ However, we want the thread to be back on the main branch with a bounded number of constraints. We therefore must erase all these garbage constraints. This will be the role of the pre-proof π R .

The reverse simulation proof π R

The goal of the proof π R will be to erase the garbage constraints instead of creating them. To achieve this, we will aim at building a dual version of the pre-proof π M . A convenient way to think about it is the following: we try to reproduce the proof π M , but considering this time that the thread of interest t ′ originates in the sequent G. Therefore it will always follow G upwards and F downwards. We call such a thread a G-thread, and the previous version used in π M a F -thread.

The principle is that if the G-thread t ′ creates garbage constraints u, i.e. has a visible weight u ∈ Σ * then its dual, the identical thread considered in reverse and originating in F , has a visible weight dual(u), where the function dual : Σ * → Σ * is defined as follows. Let v → v : Σ * → Σ * be the length-preserving morphism defined on letters by the following correspondence:

x : l r i l r ī A C W x : l r ī l r i A C W
Let v R be the reverse of a word v, defined by induction: ϵ R = ϵ and if (u, a) ∈ Σ * × Σ then (ua) R = a(u R ).

We now define dual(u) = ūR .

Lemma A.39. Let t be a thread from φ α to ψ β , and dual(t) be the identical thread considered in the other direction, from ψ β to φ α . Then vp(t R ) = dual(vp(t))

Let t M be the F -thread of the main pre-proof P going through the π M cut and ending with the cut rule, and t R be the analog F -thread for the π R cut. We want to build π R such that vp((t R ) R ) = vp(t M ). By Lemma A.39, this implies vp(t R ) = dual(vp(t M )), and moreover vp(t M ) ⊆ { l, r , ī} * , and w(t M ) ends with C. Therefore vp(t M t R ) = ϵ.

In the following, we will describe how gadgets of π M are dualized to create π R , where the run of the machine is simulated by a G-thread.

Dual auxiliary metarules

Rules relatives to A are left unchanged, so we will freely used (∞), ( A ), (Acut).

The rules (exp), (r), (l) also stay identical.

The main difference will occur when we want to introduce or delete a constraint, since they will now be reversed. In particular, in the previous construction, we saw that introducing a constraint could be done at will without any assumption, but removing a constraint as done in (Dec 1 ) needed the presence of a known bit occuring before the constraint to be removed.

We therefore redefine constraint introduction gadgets π r ′ i and (r ′ i ), with the notable change that the effect on stack is now r → rr, i.e. we always assume that the stack starts with r. We keep the convention for cuts, i.e. the newly introduced cut formulas are written on the inside (left F and right G).

π r ′ i ⊢ G, F , A ≡ (∞) G l , F l , F rl , A (Ax)
G r , F rr

(⊗) ⊢ G l ⊗G r , F l , F rl , F rr , A (ν, ) ⊢ G l ⊗G r , F l , F r , A (µ, ν, ) ⊢ G, F , A ⊢ G, F , A (r ′ i ) ⊢ G, F , A ≡ π r ′ i ⊢ G, F , A ⊢ G, F , A (Acut)
⊢ G, F , A

It is easily verified that a G-thread entering with constraint r will exit with constraint rr.

As before, we also define the left analog π l ′ i and (l ′ i ), with effect r → rl.

Initialisation of π R

We now want to initialize the dual thread. However, since the introduction rule needs to assume an r constraint already on the stack, we will need to assume this for the G-thread entering π R . This means that in the end, the F -thread exiting π R via G (the real thread of interest) will have a leftover constraint r, that we will need to evacuate on the main branch, as done in the main pre-proof P.

Thus, we only need to add three r constraints to the one already assumed:

(q ′ 0 ) ⊢ G, F , A (init ′ ) ⊢ G, F , A ≡ (q ′ 0 ) ⊢ G, F , A (r ′ i ) ⊢ G, F , A (r ′ i ) ⊢ G, F , A (r ′ i )
⊢ G, F , A We will use the (p ′ ) notation with p ∈ Q for state-labelled nodes of π R , to distinguish them from nodes in π M .

  Inductive nat := O: nat | S : nat -> nat. CoInductive Stream := Cons : (nat * Stream) -> Stream.

Figure 2

 2 Figure2presents two circular derivation trees, in the twosided µMALL ∞ sequent calculus2 .These examples correspond (at a somehow informal level) to the Coq coinductive terms drop and incdrop of Fig.1. The computational interpretation of the left-hand derivation is that of a function from streams of nats to streams of nats which drops its elements in odd position, keeping half of its elements only3 . The rightmost proof has a slightly different computational interpretation: it drops one element every two but also increments the other element that is returned in the output stream. This is achieved by using a cut in the proof, depicted in the box, which corresponds to hdinc and does the increment. Although both proofs are productive when they are cut with streams of nats, only the leftmost proof is valid for[START_REF] Baelde | Infinitary Proof Theory: the Multiplicative Additive Case[END_REF] (up to axiom expansion): the rightmost proof has no valid thread inhabiting the infinite branch because of the cut with the boxed sub-proof occurring in a cycle.

Figure 1 .

 1 Figure 1. Examples of coinductive definitions in Coq.

Figure 3 .

 3 Figure 3. Hierarchy of validity conditions

Definition 2 . 1 .

 21 Given infinite sets of atoms A = {a, b, . . . } and of fixed-point variables V = {X , Y , . . . }, µMALL ∞pre-formulas are built over the following syntax:

Figure 6 .

 6 Figure 6. Examples of external and internal reduction rules.

Example 4 . 4 .

 44 The blue pre-thread of Example 4.2 has a weight of the form WlWA lWCli . . . .

Example 4 .

 4 [START_REF] Brotherston | Sequent calculi for induction and infinite descent[END_REF] (valid and invalid pre-proofs).

(

Example 4 . 18 .

 418 The slice in Fig.7.(iii) is trivially persistent as it contains no ⊕ inference. The sliced ( ) rule depicted in definition 4.16 is well-sliced if, and only if, i = j.The following two properties of persistent slices are the key for the cut-elimination property (see proof in A.5): Proposition 4.19. All reducts of a persistent slice are (Ω)free, and therefore are slices. Proposition 4.20 (Pull-back property)

Definition A. 3 .

 3 External reductions are defined in fig. 11. In the first external rule, the sets C ∆ and C Γ are the subsets of C which are respectively connected to ∆ and Γ respectively. More precisely, C ∆ = {s | ∃s ′ , s |= * s ′ and s ′ is |= -connected to ⊢ ∆, Γ, F ⊗ G on an occurrence of ∆}, where |= * is the transitive closure of the relation |= on sequents. C Γ is defined similarly.

Figure 11 .

 11 Figure 11. External reduction rules, where r = (ext, F ) and F is the principal occurrence.

  there is a b-path in π between F and G. The relations |= π and ≈ π are symmetric -note that the reverse of a b-path from F to G is a b-path from G to F . The relation ≈ π is reflexive. Proposition A.15. Let R be a reduction. The trace of R cannot contain an occurrence F and two distinguished occurrences G and H such that F |= T G and F ≈ T H .

Figure 13 .

 13 Figure 13. The main pre-proof P

  We can detail the stack modifications in (result):(rl k )T (prep) -----→ rl k TT (r) --→ l k TT π move ----→ l k T l k T .

⊢

  G r , F r , A (exp) (♣) ⊢ G, F , A (result) (p) ⊢ G, F , A

  two sequents s i and s j , we say that they are |= -connected on the formula occurrences F , G when F ∈ s i and G ∈ s j such that F

				|= G. We say that they are
	|=	-connected, and we write s i	|=	s j , when they are	|=	-
	connected on some F , G. The relation	|=	on sequents
	must satisfy two conditions:
	-two sequents must be	|=	-connected on at most one
	pair of occurrences F , G;
	-the graph of the relation	|=	must be connected and
	acyclic.

Details on the formulations of sequents can be found in Appendix A.1.

Note that there are various approaches to cut-elimination in infinitary settings, for non-wellfounded derivations or for logics including an Ω-rule, in particular Mints continuous cut-elimination[START_REF] Grigori | Finite investigations of transfinite derivations[END_REF].

... which respectively correspond to the following sequences:t r = (F G; ⊢ F G; ↑ ) • (F G; ⊢ F G, F ′⊥ ⊗G ′⊥ ; ↑ ) • (F ; ⊢ F, F ′⊥ ; ↑ ) • (F ′⊥ ; ⊢ F, F ′⊥ ; ↓) • (F ′⊥ ⊗G ′⊥ ; ⊢ F G, F ′⊥ ⊗G ′⊥ ; ↓) • (F ′ G ′ ; ⊢ F ′ G ′ ; ↑) • (F ′ ; ⊢ F ′ , G ′ ; ↑) • (F ′′ ; ⊢ F ′′ , G ′ ; ↑) and t b = (F G; ⊢ F G; ↑) • (F G; ⊢ F G, F ′⊥ ⊗G ′⊥ ; ↑) • (G; ⊢ G, G ′⊥ ; ↑) • (G ′⊥ ; ⊢ G, G ′⊥ ; ↓) •(F ′⊥ ⊗G ′⊥ ; ⊢ F G, F ′⊥ ⊗G ′⊥ ; ↓) •(F ′ G ′ ; ⊢ F ′ G ′ ; ↑) • (F ′ ; ⊢ F ′ , G ′ ; ↑) • (F ′′ ; ⊢ F ′′ , G ′ ; ↑).

It can happen that a W * factor can be put either in the visible part or the hidden part. Since such choices will play no role in the following, we can make now an arbitrary choice for these factors, and consider the decomposition unique.

That is, every infinite branch of the slice is visited by a valid thread having its visible part contained in the branch.

This reduction is straightforwardly extended to multicuts and some care shall be taken in treating (Ω), in particular any cut involving (Ω) is reduced to (Ω) itself as standard in ludics.

That is, every infinite branch of the slicing is visited by a valid thread having its visible part contained in the branch.

* This research has been partially supported by ANR project RECIPROG, project reference ANR-21-CE48-019-01.

⊢ G rrll , F lrrl

⊢ G rrrl , F lrrr

⊢ G r , F lr , A

. The pre-proof π shift with its auxiliary π aux ⊢ G, F , A

⊢ G, F , A

. The metarule (copy l )

⊢ G r , F r

⊢ G, F , A This concludes the description of the proof π M , starting with

⊢ G, F , A , and built as described by linking statelabelled nodes using rules we defined for the action performed by each state according to δ . This construction ensures the following Lemma:

Lemma A.38. A thread entering π M with empty constraint will be able to exit it if and only if M has a run. If this is the case, the constraint after the exit is a word u 1 u 2 . . . u k r 4 , where k is the number of tests performed, and u i encodes the results X ∈ {l, r} of the i th test in the following way:

• if the test is on the first counter, then u i = rX ,

Dual encoding of action Inc

Assume δ (p) = Inc 1 (q) with q ∈ Q. We want to define a metarule (Inc ′ 1 ) updating the configuration reached in (p ′ ) by acting on the constraint stack, and ending up in node (q ′ ), with effect r → rl on the stack. Therefore it suffices to use the l introduction defined before:

To manipulate the second counter instead, we can use the (counter) rule which is identical as in π M . Thus the metarule (Inc ′

2 ) is defined as follows:

The effect of this metarule on a G-thread is (rl * r)r → (rl * r)rl

Dual encoding of action Dec

We now need to encode a metarule having the effect rl → r on G-thread. This is done by metarule (Dec ′ 1 ), described here:

To manipulate the second counter, again we just need to have a (counter) metarule, as shown in metarule (Dec ′

2 ):

Dual encoding of action Test

If δ (p) = Test 1 (q Z , q P ), we can define the Test rule in a similar way as in π M . However, extra care is needed for introduction rules, as they cannot be used as freely as before. Thus, we first define the metarule (rXcop) (Fig. 19), with effect rX → rX rX on a G-thread, for X ∈ {l, r}.

We can now give the metarule (Test ′ 1 ), that uses the first rX output by (rXcop) to perform the zero test:

If the G-thread enters with constraint prefix rr, this prefix will be copied, the first copy will be read, put in the garbage to be collected later, and the G-thread will enter (q ′ Z ). Similarly if the constraint started with rl, the G-thread will go to (q ′ P ) with unchanged stack and garbage rl.

To treat the case of the second counter, i.e. δ (p) = Test 2 (q Z , q P ), we just need to describe dual versions of all gadgets from (Test 2 ) in π M . We design them so that the effect on the Gthread is exactly the same as the one of their original version on the F -thread.

The only difficulty to keep in mind is that the introduction rules now assume that the constraint stack starts with r. We start with π ′ shift described Fig. 20, where the pairing between G and F formulas in axioms is recalled in the table: before: ll lrrl lrrr after:

ll rrll rrrl

For readability, we separated π ′ aux , described Fig. 21: As before, the effect of π ′ shift on the G-thread is l k +1 T → l k T l with T ∈ {rrr, rrl}. We continue with the dual (copy ′ l ) of (copy l ), represented Fig. 22, with action l → ll rr → rr . Notice that we now use the fact that in the present context, a stack starting with r actually starts with rr, as mentioned when defining the gadget (copy l ).

We turn to π ′ move , represented Fig. 23, iterating π shift with effect l k T → l k T l k and rr → rr, functioning along the same principle as π move :

The rule (prep ′ ) (Fig. 24) will again allow us to prepare the input for π ′ move , using the same pairing as before. This rule has effect (rl k r)rX → (rl k r)rX rrX , with X ∈ {l, r}. We will note Γ F for a sequent composed of several non-pertinent occurrences of formula F , for concision. We continue with the metarule (result ′ ), having action rl k T → l k T l k T on the Gthread, with T ∈ {rrl, rrr}, and leaving a garbage constraint r that will be seen later on the way down.

Since the dual form of the (r i ) rule used in (Test 2 ) needs extra care, we will devise another auxiliary gadget rule (rXr i ) (Fig. 25), with effect rX → rX r with X ∈ {l, r}. This is to restore the stack content after the bit X encoding the test result to its original value starting with r. We can finally build the metarule for Test 2 (Fig. 26), performing the wanted

⊢ G rr , F rr

⊢ G, F , A test and leaving garbage constraint of the form rl k rrX with X ∈ {l, r}. After entering (Test ′ 2 ) with stack content u, the Gthread will reach node (q ′ Z ) (resp. (q ′ P )) if the second counter value is zero (resp. not zero), with same stack content u.

Dual final state q ′ f As before, when reaching the node (q ′ f ), we just need bounce on an axiom after evacuating the formula A from the sequent. The same gadget as in π M can be used:

Correctness of the pre-proof P and conclusion

By construction, if the machine M does not halt, then the F -thread entering π M will never exit it, so it cannot validate the branch looping through the (⋆) nodes, and the pre-proof P is not a proof. Conversely, if M halts, then the F -thread will exit π M with a constraint u encoding the results of the tests as described in Lemma A. [START_REF] Terui | Computational ludics[END_REF]. Moreover, the G-thread t ′ entering π R with a single constraint r will exit on the same node with the same constraints u. This means that the F -thread going through π M and π R will exit π R with a single constraint r. This constraint will be popped on the first unfolding of F , and the second (left) unfolding of F will be on the visible part of the thread. The thread then reaches node (⋆), and loops back to the root to go through the same path infinitely many times. Thus the F -thread starting in the root validates the branch containing infinitely many (⋆) nodes. All other infinite branches of P are validated by non-bouncing thread following formulas A, that can also be originated in the root of P, in the formula B.

Therefore, we showed the following theorem:

G rl , F rlr

The metarule (rXr i )

⊢ G rr , F rr , A

⊢ G r , F r , A

⊢ G r , F r , A

Theorem A.40. The pre-proof P is a proof if and only if the 2CM M has a run.

By Theorem A.37, we obtain that deciding whether a circular pre-proof of µMLL ω is a proof is undecidable, and more precisely it is Σ 0 1 -hard. In the next section, we show that this problem is recursively enumerable, so we obtain Cor. 6.7, stating that deciding validity of a circular pre-proof of

The pre-proofs of µMALL ∞ 4 3

The cut elimination process 5 3.1

The