Kaustuv Chaudhuri
email: kaustuv.chaudhuri@inria.fr

Nicolas Guenot

Equality and Fixpoints in the Calculus of Structures

The standard proof theory for logics with equality and fixpoints suffers from limitations of the sequent calculus, where reasoning is separated from computational tasks such as unification or rewriting. We propose in this paper an extension of the calculus of structures, a deep inference formalism, that supports incremental and contextual reasoning with equality and fixpoints in the setting of linear logic. This system allows deductive and computational steps to mix freely in a continuum which integrates smoothly into the usual versatile rules of multiplicative-additive linear logic in deep inference.

Introduction

It is a common design pattern for computational logic proof systems to compartmentalize and separate the computational aspects from the rest of the system. Examples include µMALL [START_REF] Baelde | Least and greatest fixed points in linear logic[END_REF] and LINC [START_REF] Tiu | A Logical Framework for Reasoning about Logical Specifications[END_REF] that separate unification, Deduction Modulo [START_REF] Dowek | Theorem proving modulo[END_REF] and Super Deduction [START_REF] Brauner | Principles of superdeduction[END_REF] that separate term rewriting, and any proof system with constraints that separates algebraic manipulations of constraint terms. The record of a formal proof in these systems omits the computational traces, which are reconstructed as needed by the consumers of the proof, usually computerized proof checkers. While this design is fairly successful in automated certifying proof search, it has a number of undesirable features from the perspective of proof representation. First, because the nature of the omitted computations differs between systems, implementations of different systems cannot generally check each others' proofs -at least, not without reimplementing the computational kernels. Second, such proofs tend to restrict computations to rigid positions, such as the leaves, which limits the possibilities for reorganizing the proofs. Third, the computations tend to have a separate language that makes them opaque to ordinary logical manipulation. Finally, the computational phases are nearly always atomic, so it is inordinately difficult, if at all possible, to perform the computations incrementally, partially, or in parallel, or to substitute one computation inside another.

In this paper, we revisit the question of combining computation and deduction in proof systems, but with a change of foundational perspective. Instead of adding computational features to a deductive system, we start with a computational system from the outset that can perform deduction. Specifically, we use the calculus of structures (COS), which is a deep inference system that blurs the distinction between formula and sequent (or, equivalently, between formula and judgement). A COS proof is organized as a linear rewrite sequence from the desired formula to logical truth. Each step corresponds to the embedding of a valid entailment of the logic into a formula context, so it is just as natural to substitute a COS proof into another proof with a hole as it is to substitute a formula into a formula context. Moreover, the design of the COS does not preclude the use of shallow proofs. Indeed, not only can the COS simulate sequent proofs at any depth, but it also has deep manifestations of such proof-theoretic phenomena as cut-elimination and focusing, familiar from the sequent calculus [START_REF] Straßburger | Linear Logic and Noncommutativity in the Calculus of Structures[END_REF][START_REF] Chaudhuri | The Focused Calculus of Structures[END_REF].

The most striking feature of the COS is that its inference rules are largely incremental, meaning that they can be applied1 by performing a fixed and constant amount of work. To illustrate: multiplicative rules are implemented in the COS not by a global division of all the hypotheses into disjoint branches of the proof, but rather by a sequence of smaller routing steps where individual subformulas are sent to components of the multiplicative connective. This incremental nature gives the COS much more permutative freedom than in shallow systems such as the sequent calculus or natural deduction. It is natural in the COS, for instance, to share common subproofs across additive branches by performing the common proof before the additive split; this can only be achieved in shallow systems indirectly by means of cuts or extensions. The COS also supports natural metaphors for proof construction by direct manipulation that are not possible to express in shallow systems [START_REF] Chaudhuri | Subformula linking as an interaction method[END_REF].

Unfortunately, despite these desirable properties, the literature on the COS has some inexplicably wide gaps that has heretofore limited its use as a proof formalism for computational logic. Nearly the entirety of the published work on the COS deals with propositional logics, which are of no use for reasoning about data structures-particularly recursive data structures-that are the sine qua non of computation. The main contribution of this work is an extension of the COS to first-order classical multiplicative additive linear logic (MALL) with support for equality and fixpoint predicates, which raises the expressivity of the COS to the level of µMALL [START_REF] Baelde | Least and greatest fixed points in linear logic[END_REF] for first-order terms. Our treatment of these extensions stays as close to the spirit of the COS as possible; the rules for equality and fixponts are incremental and contextual, and can be freely interleaved and permuted with other inference rules. Indeed, we show that equality is a critical ingredient for an incremental treatment of the first-order predicates.

Supporting equality requires the addition of rules for decomposing equations on larger terms to those on smaller terms. For purely positive occurrences of equations, this amounts to the rules of a unification logic that essentially implement Robinson's unification algorithm. Symmetry and transitivity are freely admissible in this fragment. The atomic identity rule, which requires two & -linked dual atomic formulas, can be replaced with an incremental version that only requires dual predicate symbols; the term arguments are checked point-wise for equality. The situation becomes more complex in the presence of disequations-negative occurrences of equations-because symmetry and transitivity become essential rules. Transitivity is particularly problematic as it requires the invention of an interpolant that is not structurally present in the conclusion. Fortunately, we can leverage depth here to effectively eliminate this problem. The essential idea is that we can view transitivity not as (s = t) ⊗ (t = u) ⊢ (s = u) but as (t = u) ⊢ (s = t) ⊸ (s = u), which are logically equivalent, but the latter form contains all the terms on the right hand side, which forms the conclusion of the COS rule. All the inference rules become analytic on terms.

The most important use of equations in computational logic is in the theory of uninterpreted functions, where all term constants are viewed as constructors, i.e., they are injective and discriminating. We distinguish this equality from the mathematical notion by calling it intensional. Intensional disequations are very powerful: they are interpreted as an enumeration over all possible ways to prove the converse, which is the essence of reasoning by cases. In the µMALL sequent calculus [START_REF] Baelde | Least and greatest fixed points in linear logic[END_REF], this rule is written using the complete set of unifiers (csu) as follows:

for every θ ∈ csu(s, t), ⊢ θΓ ⊢ Γ, (s = t)
This rule has two big problems. First, as said before, the csu computation is not part of the proof system, so any proof consumer must be able to recompute the csu. This requirement is worse than it appears: when exchanging formal proof objects, the proof producer and consumer must agree not only on the contents of the csu but also on their order. This is a significant restriction on the independence of the consumer from the producer. Second, this rule makes a copy of the entire context Γ for every element of the csu. This copying is not mere additive sharing, which can often be implemented by shared pointers, because the various copies of the context are instantiated by different substitutions and hence may have significant varying subsets. To make the csu computation more incremental in the COS, we show how to express it using the connectives of MALL that already exist, and we then rely on the incremental nature of the rules for these connectives.

Intensional equality comes fully alive with the addition of least and greatest fixpoints. We show how to adapt the unfolding and coinduction rules of µMALL to an incremental and contextual form. The main challenge is that the coinduction rule of µMALL has the form of an essential cut where one of the premises establishes that the cut-formula is a post-fixpoint. This premise has to be isolated from the rest of the sequent, particularly the linear hypotheses. Such an isolation is not possible in the COS for MALL itself without making the coinduction rule non-contextual. Our solution is to extend MALL with a connective that simply records that its argument is isolated; in effect it is similar to the ! connective of the full linear logic, except it has no dual and cannot be contracted or weakened. The only operations allowed on this connective to delete it if its operand has successfully been rewritten to 1.

The addition of fixpoints also adds a new wrinkle to the atomic identity rule, which must now check that the same possible large fixpoint expression occurs in dual & -linked forms. We construct an incremental version of this rule that only checks for inclusion of the least fixpoint in the greatest fixpoint. Surprisingly, this turns out to be sound and complete by means of a fairly simple second-order substitution argument. Moreover, it can be seen as inlining a particular kind of coinduction where the least fixpoint is used as an invariant for the greatest fixpoint, so we re-use the isolation trick we already used to implement the (co-)induction rule.

The paper is structured as follows. In Section 2 we sketch the COS for first-order MALL. Section 3 incorporates equality into this calculus in stages, starting with purely positive occurrences and progressing to the full intensional equality. Section 4 then extends the system with least and greatest fixpoints, and gives a few illustrative examples. Related work and possibilities for future work are summarized in Section 5.

ξ{1} ξ{a & a} aid ξ{(A & B) & C} ξ{A & (B & C)} assoc ξ{B & A} ξ{A & B} comm ξ{(A & C) ⊗ B} ξ{(A ⊗ B) & C} swl ξ{B ⊗ (A & C)} ξ{A & (B ⊗ C)} swr ξ{1} ξ{1 ⊗ 1} onem ξ{A} ξ{A ⊕ B} chl ξ{B} ξ{A ⊕ B} chr ξ{[t/x]A} ξ{∃x. A} wit ξ{(A & B) & (A & C)} ξ{A & (B & C)} dist ξ{⊤}

MALL in the Calculus of Structures

We begin by summarizing the calculus of structures for first-order classical multiplicative-additive linear logic (MALL), based on the design of [START_REF] Chaudhuri | The Focused Calculus of Structures[END_REF]. This logic is selected primarily because it is the basis for the µMALL system, but linearity gives us the additional ability to be precise about the multiplicities of formulas, and requires us to be explicit in our use of contraction and weakening. We omit the exponential connectives of linear logic as they are largely redundant with fixpoints. The terms (s, t, . . . ), atomic formulas (a, b, . . . ) and arbitrary formulas (A, B, . . . ) of our language have the following grammar, where x, y, . . . range over term variables, f, g, . . . range over function symbols, and p, q, . . . range over predicates. s, t, . . .

::= x | f(t 1 , . . . , t n ) a, b, . . . ::= p(t 1 , . . . , t n ) A, B, . . . ::= a | A ⊗ B | 1 | A ⊕ B | 0 | ∃x. A | a | A & B | ⊥ | A & B | ⊤ | ∀x. A
We assume that variables, function symbols, and predicate symbols are drawn from pairwise disjoint infinite sets, and that the arity of every function and predicate symbols is fixed. We write s to stand for a list of terms s 1 , . . . , s n (with n ≥ 0). By convention, we omit the empty argument list for nullary function and predicate symbols. We write A for the negation of A, defined as usual in terms of De Morgan duals. Formulas are in negation-normal form, so the only occurrence of negation in the syntax is in negated atoms, indicated with an overline. We write A ⊸ B as usual to stand for A & B, A ⊢ B to assert that the formula A ⊸ B is true in MALL, and A ⊣⊢ B to assert that A ⊢ B and B ⊢ A.

The main feature of the calculus of structures (COS) is that the rules are allowed to be applied in any formula context, which is a formula with a single occurrence of a hole ( ). The grammar of formula contexts (ξ, ρ, . . . ) is thus:

ξ, ρ, . . . ::= | A ⋆ ξ | ξ ⋆ A | Qx. ξ where ⋆ ∈ {⊗, ⊕,
& , &} and Q ∈ {∃, ∀}. We write ξ{A} for the replacement of the single hole in ξ with A, called a substitution, which is allowed to capture the free variables in A; we call A the selected formula in the notation ξ{A}. Substitutions are used to turn shallow entailments and admissible rules into their deep variants.

Theorem 1. For any A, B, and ξ,

• if A ⊢ B, then also ξ{A} ⊢ ξ{B}; and

• if the truth of A implies the truth of B, then the truth of ξ{A} implies the truth of ξ{B}.

Proof. By induction on the structure of ξ.

The inference rules for the system MAS for this logic are defined in terms of substitutions. The full system is shown in Figure 1. This system is a minor variant of the system LS from [START_REF] Chaudhuri | The Focused Calculus of Structures[END_REF]. Each rule contains exactly one premise and conclusion and corresponds to a valid entailment of linear logic. All the rules except assoc and comm are oriented in such a fashion that the premise is always simpler than the conclusion in the following sense: either the selected formula in the premise is a strict subformula of that of the conclusion, or one of the connectives &, ⊗, or ∀ has a larger scope in the premise than in the conclusion, or a selected 1 in the premise is ⊤ in the conclusion. We will adopt the convention of omitting mentions of the assoc and comm rules, but use them implicitly.

Definition 2 (standard notions). Let S be any unary formula inference system, i.e., a system where the sole premise and conclusion of each rule schema are formula schemas.

• An S-derivation φ of formula B from formula A, written φ : A S --→B, is a chained sequence of instances of the rules of S such that the topmost rule instance has premise A and the bottom-most rule instance has conclusion B.

• An S-proof π of A is a derivation π : 1 S --→A.
• The formula B is S-derivable from A, written as A S --→B, if there exists an S-derivation of B from A. The formula A is S-provable if there exists an S-proof of A.

• A schematic rule is S-admissible if in every instance of the schema whenever the premise is S-provable then so is the conclusion.

When S is understood, the prefix "S-" will be elided.

Theorem 3 (Soundness of MAS). For any formulas A and B, if

A MAS ----→B, then A ⊢ B.
Proof. Each inference rule of MAS is a valid entailment. The result follows from the composability of entailment for MALL, i.e., that A ⊢ B and

B ⊢ C imply that A ⊢ C. Theorem 4 (Completeness of MAS). If A is a true formula of MALL, then 1 MAS ----→A.
Sketch. If A is true, then there must be a derivation of ⊢ A in a cut-free sequent calculus for MALL, such as the one shown in Figure 4. It is immediate by inspection that each inference rule of this calculus can be simulated in MAS (for more detail on this correspondence, see [START_REF] Chaudhuri | The Focused Calculus of Structures[END_REF]). The occurrences of 1 corresponding to the branches of the sequent derivation are then combined with onem or onea.

It should be noted that MAS has a natural dual system where every inference rule is inverted and the premise and conclusion are dualized. The combination of MAS and its dual system is a purely symmetric system (a variant of SLS [START_REF] Straßburger | Linear Logic and Noncommutativity in the Calculus of Structures[END_REF]), which also includes the dual of the aid rule, ξ{a ⊗ a} ξ{⊥} acut General cuts in SLS can be reduced to these atomic cuts, which can then be shown to be admissible in MAS.

Much of this technique has been worked out for the full propositional linear logic in [START_REF] Straßburger | Linear Logic and Noncommutativity in the Calculus of Structures[END_REF][START_REF] Chaudhuri | The Focused Calculus of Structures[END_REF]. We expect that the extension of such results to the first order case would be straightforward.

The system MAS also admits a number of congruence rules that are standard in the literature on the COS, such as in [START_REF] Straßburger | Linear Logic and Noncommutativity in the Calculus of Structures[END_REF]. These rules are left out of MAS, but we will use them in the remainder of this paper if needed to simplify the presentation.

ξ{B * A} ξ{A * B} ξ{(A * B) * C} ξ{A * (B * C)} ξ{A} ξ{A * ‡}
Here, ( * , ‡) ∈ {(⊗, 1), (⊕, 0), (&, ⊤)}. We will also consider a derivation to be a proof if the premise can be derived from the simple rules on logical constants: {onea, onem, top, vac}.

Equality

Positive Equality and Incremental Unification

Let us turn to an ignored corner of MAS (Figure 1): the aid rule. This rule requires the same atom to be present in dual forms across the & . This requirement forces instantiations (the wit rule) to be performed before (i.e., below) the aid rule, which makes the calculus rigid with respect to instantiations. It also requires traversing arbitrarily large structures to check identity, which is against the incrementality principle. To make the rule incremental and more flexible, we replace it with the following variant.

ξ ( s = t ) ξ p( s ) & p( t ) match
Here, = is a binary predicate symbol (written infix, as usual) denoting that its two arguments are equal terms.

In this rule and in the rest of this paper, we will use the convention that if s = s 1 , . . . , s n and t = t 1 , . . . , t n , then the formula ( s = t ) stands for (s

1 = t 1 ) ⊗ • • • ⊗ (s n = t n ) if n ≥ 1 and for 1 if n = 0.
Thus, the requirement that the two dual atoms be exactly identical in the aid is relaxed to produce a collection of residual equality obligations for the term arguments.

To reason about such positive equalities, we need just the following rules of reflexivity (refl) and congruence (cong):

ξ{1} ξ{x = x} refl ξ ( s = t ) ξ f( s ) = f( t ) cong
Observe that the refl rule is limited to variables. This pair of rules suffices to prove s = s for any term s. Of course, these rules may now be interleaved with other logical rules, including instantiation.

An important side-effect of relaxing aid into match is that existential instantiation can fruitfully be made lazy as well by adding the following rule:

ξ{∃x. (A & B)} ξ{A & ∃x. B} ex
where, as with all, we require that x is not free in A. This rule is easily seen to be admissible in MAS, but it only becomes useful when aid is not forced to end a branch.

Definition 5 (System MAUS). Let MAUS stand for

(MAS \ {aid}) ∪ {match, refl, cong, ex}
Let us finish this short section on positive equalities by noting a few interesting features.

Example 6.

In MAUS there is a continuum between logic and unification. Consider this MAUS derivation:

∃x. ∀y. ∃z. (f(x) = f(f(c))) ⊗ (y = z) ∃x. ∀y. ∃z. p(f(x), y) ⊸ p(f(f(c)), z) match ∃x. ∀y. p(f(x), y) ⊸ ∃z. p(f(f(c)), z) ex ∃x. (∃y. p(f(x), y)) ⊸ ∃z. p(f(f(c)), z) all ∀x. ∃y. p(f(x), y)) ⊸ ∃z. p(f(f(c)), z) ex
Instantiations of the existential variables x and z are not forced before the application of match. The goal formula is reduced to a unification problem consisting only of the quantifiers and (conjunctions of) equality.

There is neither a syntactic separation between the two kinds of problems, nor are deductive and unification phases necessarily separate. Unification can be done incrementally using the rules {refl, cong, wit}:

∀y. 1 ⊗ 1 ∀y. 1 ⊗ (y = y) refl ∀y. ∃z. 1 ⊗ (y = z) wit ∀y. ∃z. c = c ⊗ (y = z) refl ∀y. ∃z. (f(c) = f(c)) ⊗ (y = z) cong ∃x. ∀y. ∃z. (x = f(c)) ⊗ (y = z) wit ∃x. ∀y. ∃z. (f(x) = f(f(c))) ⊗ (y = z) cong Example 7.
Since MAUS derivations can postpone applications of the wit rule, it is important to ensure that it still respects the usual eigenvariable condition for quantifiers. Consider the following example of an invalid quantifier switch. The resulting unification problem is not solvable, because there is no capture-avoiding substitution for x that will make ∀w. x = w true.

Example 8 (Occurs Check). As MAUS has neither a rule of transitivity nor a means of introducing new ∃quantified variables, it follows that there are only a finite number of simplification steps (refl and cong) that can be applied to a given unification problem. In other words, MAUS can only establish the equality of finite terms. This can be seen a variant of the occurs check of Robinson's unification algorithm. To illustrate, the formula ∃x. p(x) ⊸ p(f(x)), which has no finite witnesses, has the (incomplete) MAUS derivation:

t = f(t) ∃x. x = f(x) wit ∃x. p(x) ⊸ p(f(x)) mat
The only way to proceed with that instance of wit is to exhibit a term t for which t = f(t).

The previous example indicates that one can often fold the occurs check for positive equality directly into wit as follows, where vars(t)

∩ ({x} ∪ bvs(ξ ′ )) = ∅. 2 ξ{[t/x]ξ ′ {1}} ξ{∃x. ξ ′ {x = t}}
However, using this rule instead of wit would make the system incomplete.

Theorem 9 (MAUS vs. MAS). For any

A free of =-subformulas, 1 MAUS ----→A if and only if 1 MAS ----→A.
Sketch. One direction is simple, since the rules {refl, cong} suffice to establish t = t, and the other rules of MAS are also derivable in MAUS. In the other direction, the MAUS rule ex is admissible in MAS. For applications of match in the MAUS proof, the relevant applications of wit must first be permuted below the rule, and the relevant applications of refl and cong (which do not interact with any other logical connective) must be permuted to above the instance of wit. These permutations are height-preserving, and the instances of cong and refl can only establish equalities. The entire argument then proceeds by induction on the height of the MAUS proof, splitting inductive cases from the bottom-most instance of match.

MAUS has no equality rules that can introduce new variables in the premise of a rule. Thus, in the usual flex-flex case of unification, where Robinson's algorithm would allocate a fresh variable to instantiate both operands of the equality, in MAUS we would just instantiate one variable with the other. For the first-order case this is not problematic, but it does become an issue for higher-order terms. To illustrate, the higher-order pattern unification problem ∀u, v, w. ∃X, Y. X u v = Y v w is solvable if we instantiate X with λx, y. Z y and Y with λx, y. Z x for some fresh existentially quantified variable Z, but there is no solution where one of X and Y is instantiated in terms of the other.

Disequations

Let us now turn to both positive and negative occurrences of equality, writing (s = t) for (s = t). Before proceeding further, there is an important matter to settle: the linear nature of equations. When equality has only positive occurrences, it is immaterial whether we give it a linear semantics or not, but with negative occurrences this becomes an important choice. If we were to treat disequalities too as linear, then we must accept that formulas such as (x = y) ⊸ (x = y) ⊗ (x = y) (which results from match on (x = y) ⊸ p(x, x) ⊸ p(y, y)) will be unprovable, since (x = y) will be consumed by the first equation. Note that it is not sufficient to alter match to be additive, i.e., to use & instead of ⊗ in the premise, as this still leaves the former formula unprovable.

If we had the full linear logic, we could use the exponential connectives to indicate that certain equalities are non-linear: !(x = y) ⊸ p(x, x) ⊸ p(y, y). This does not work in MALL, so we instead add rules to treat disequalities as implicitly exponential with the following rules.

ξ{⊥} ξ{s = t} qwk ξ{(s = t) & (s = t)} ξ{s = t} qct
This is tantamount to assuming the derivability of (s = t) ⊢ 1 and (s = t) ⊢ (s = t) ⊗ (s = t), i.e., of (s = t) ⊣⊢ !(s = t) and (s = t) ⊣⊢ ?(s = t). Note that this leaves the rest of the logic untouched; indeed, it is a conservative extension of MAUS.

An important property of the rules refl and cong of MAUS is that they simplify equations between two terms to a collection of equations on strict subterms. This suffices for the simple case of positive equations, but it is not complete in the general case. In particular, symmetry (∀x, y. (x = y) ⊸ (y = x)) and transitivity (∀x, y, z. (x = y) ⊸ (y = z) ⊸ (x = z)), which are part of the axioms of equality, are not derivable in MAUS. Both these properties require rewriting an equation into other equations on the same or unrelated terms.

Symmetry comes in two forms:

ξ{t = s} ξ{s = t} sym ξ{t = s} ξ{s = t} nsym
It turns out that these rules are stronger than strictly necessary, because the cong rule already reduces equations between arbitrary terms into equations where one operand is a variable. One can therefore limit sym to, for instance:

ξ{x = t} ξ{t = x}
where t stands for any term and x stands for a variable. Indeed, in an implementation we can further orient sym by only rewriting if the term t is lpo-larger than x, where the variables are given some arbitrary ordering. We do not make these refinements in this paper to keep things simple.

Likewise, transitivity might appear to be a simple rule.

ξ{(s = t) ⊗ (t = u)} ξ{s = u} (1)
However, this rule has the problem that it mentions a term t in the premise that is not necessarily in the conclusion. Inventing the interpolant t can also be arbitrarily expensive because the calculus does not constrain its shape in any way. Indeed, this is the only rule that breaks analyticity on terms. Fortunately, there is a simple fix: we observe that the rule corresponds to the entailment (s = t)⊗ (t = u)⊢ (s = u), which is equivalent to its curried form (t = u) ⊢ (s = t) ⊸ (s = u). Hence, we alter the rule to:

ξ{t = u} ξ{(s = t) & (s = u)} (2)
Now every term in the premise is also in the conclusion. However, even this rule is not entirely incremental, because the term s has two occurrences in the conclusion, which requires a potentially expensive computation when applying the rule. We can modify it to just check that the two occurrences are equal:

ξ{(s = u) ⊗ (t = v)} ξ{(s = t) & (u = v)} (3)
But, this form of rule, which is inter-derivable with (2), is just an instance of match for the = predicate, and therefore redundant! In other words, transitivity of equality is just a special case of match. This is not the full story: we also need to account for the transitivity of disequations, which is the contrapositive of the entailment (s = t) ⊗ (t = u) ⊢ (s = u).

ξ{(s = u)} ξ{(s = t) & (t = u)}
Once again, as t is repeated in the conclusion, we relax it to an equation to obtain the following rule, which is dual to [START_REF] Baelde | The Bedwyr system for model checking over syntactic expressions[END_REF]. Sketch. By admissibility of cut and the MAQS-derivability of ξ{s = s} for any ξ and s:

ξ{(t = u) ⊗ (s = v)} ξ{(s = t) & (u = v)
ξ{(s = u) ⊗ (u = t)} ξ{(u = s) ⊗ (u = t)} sym ξ{(u = u) & (s = t)} match ξ{1 ⊗ ((u = u) & (s = t))} ξ{(u = u) ⊗ ((u = u) & (s = t))} derivability of ξ{u = u} ξ{s = t} cut, swr
We will omit in this paper a formal soundness and completeness result for MAQS with respect to a sequent calculus. It is fairly easy to show by a straightforward induction that: (1) MAQS is a conservative extension of MAUS, and (2) that any MAQS derivation can be justified by a MAUS derivation where the end-formula is augmented by suitable instances of the following axioms. The last two axioms are schematic over f p.

Intensional Equality

The system MAQS is too weak to show that z = s(z) where z and s denote the natural number 0 and the successor operation. It also cannot reason fruitfully about disequations, such as to show that (s(x) = s(s(y))) ⊸ (x = s(y)). This weakness is not problematic for mathematics, where equality is given an extensional or Leibniz interpretation, and any additional properties of function symbols are added as axioms. For example, both the above properties are instances of the Peano axioms for the natural numbers. However, in a computational setting where terms are used to encode data, we will generally treat equality as intensional, with functions interpreted as term constructors, i.e., enjoying discrimination (applications of different function symbols are different) and injectivity (if two applications of the same function are equal, then the arguments must be equal).

In the next section where we consider fixpoints, we will rely critically on this intensional view of equality. Let us first consider the discrimination property. Once again, we have a choice of semantics. If we rewrite z = s(z) to 1, then it does not let us prove, for instance, that z = s(z) ⊸ 0. In µMALL, the corresponding sequent ⊢ z = s(z), 0 would be considered as provable because the set of unifiers of z and s(z) is empty. Therefore, we choose to use an additive semantics for discrimination, reflected in the following inference rule.

ξ{⊤} ξ f( s ) = g( t ) disc
Here, f and g denote different function symbols.

Related to discrimination is the topic of finiteness: because terms are assumed to be finite, a circular disequation should also be rewritten to ⊤. The prototypical scenario is the formula (x = f(x)) ⊸ 0, which in µMALL is true because x and f(x) cannot be unified. To make this formal in the COS, we first define term contexts (τ):

τ ::= f( s , τ * , t ) τ * ::= | τ
We will write τ{t} for the replacement of the single occurrence of the hole in τ with t. The finiteness rule is then; ξ{⊤} ξ{x = τ{x}} fin Note that this rule might appear to be non-incremental as it examines an entire term, but it can easily be made incremental by adding a not-occurs-in predicate on terms and giving it the obvious rules. We skip the straightforward elaboration of this basic idea in this paper.

Injectivity amounts to the reverse of the congruence axiom (Definition 12) for equality:

∀ x, y. f( x ) = f( y ) ⊸ ( x = y ). ( 4
)
Its contrapositive is a natural COS rule for disequation:

ξ ( s = t ) ξ f( s ) = f( t ) inj
where ( s = t ) stands for ( s = t ). Note that since we have qwk and qct, it is immaterial whether the premise uses & or ⊕: the two choices are inter-derivable.

1 ⊗ ⊤ (x = x) ⊗ ⊤ refl (x = x) ⊗ (z = s(z)) disc (z = x) & (x = s(z))
trans

We can show that MAIS is sound and complete with respect to QMALL, which is the fragment of µMALL without fixpoints and higher-order terms. The rules of QMALL are given in Figure 4.

Theorem 15. If A MAIS ----→B, then A ⊢ B in QMALL.
Proof. Each inference rule of MAIS is derivable as an entailment in QMALL, similar to Theorem 3.

In order to show completeness of MAIS with respect to QMALL, we will need to reason about the relation of term substitution and equations. Definition 16. A term substitution (θ, σ, . . . ) is a set of assignments of terms to variables, [t 1 /x 1 , . . . , t n /x n ], abbreviated as t/ x . We write θA to stand for the simultaneous capture-avoiding replacement of the variables in the domain of θ by their assigned terms in the syntactic entity (term, formula, context, etc) A. The equational representation of θ = t/ x , written Q θ , is the formula ( x = t ).

Theorem 17. The following rule is admissible in

MAIS: ξ{θA} ξ Q θ & A
Sketch. By induction on the structure of A. Note that all (dis)equations in MAIS are reduced to (dis)equations involving variables, which are then combined with the disequations in Q θ using match or trans.

Theorem 18.

If A is a true formula of QMALL, then 1

MAIS

----→A.

Proof. As before Theorem 4, we will show that the inference rules of QMALL are admissible in MAIS. There are only three interesting rules not accounted for already for MALL/MAS.

• The reflexivity rule of QMALL: ⊢ s = s =. This follows immediately by induction on the structure of s.

• The disequation rule of QMALL:

for every θ ∈ csu(s, t), ⊢ θΓ ⊢ Γ, s = t If csu(s, t) = ∅, then we are in exactly one of three possibilities: (1) s and t have different head function symbols, for which we use disc, (2) s and t have the same head function symbol but some of their arguments are point-wise non-unifiable, in which case we use inj and recurse, and (3) one of s or t is a variable and it occurs in the other, in which case we appeal to fin. If csu(s, t) = ∅, then we can show by an induction on the structure of s and t that the following rule is admissible in MAIS:

ξ Q mgu(s,t) ξ{s = t}
where mgu stands for the most general unifier for s and t, which exists (and is easy to compute) for first-order terms. We then appeal to Theorem 17.

Fixpoints

In this section we will show how to build fixpoint reasoning on top of MALL intensional equality as defined in Section 3.3. We will follow the tradition of µMALL [START_REF] Baelde | Least and greatest fixed points in linear logic[END_REF] and LINC [START_REF] Tiu | A Logical Framework for Reasoning about Logical Specifications[END_REF] and give least and greatest fixpoint semantics based on induction and coinduction rules. Case-branching and case-pruning in both these systems is performed by the rules for disequations. These proof systems are often also presented together with generic quantification (using the ∇-quantifier), which requires some additional reasoning about equality (known as equivariance) that is not part of MAIS; we leave this to future work.

To be concrete, we extend the grammar of predicates with two new De Morgan dual constructs: µp( x). A and νp( x). A, where in each case the predicate symbol p and the variables x = x 1 , . . . , x n are bound by the corresponding µ or ν in the formula body A. These predicates have the same arity as the number of elements of x, and fixpoint atoms are intended to be equivalent to their unfoldings.

(µp( x). A)( s ) ⊣⊢ [ s/ x][µp( s). A/p]A (µp( x). A)( s ) ⊣⊢ [ s/ x][µp( s). A/p]A

(5)

To simplify this paper, we will assume no mutual recursion between different fixpoint predicates; it is easy to extend the development to the general case. For global consistency, which is equivalent to termination of cut-elimination, such fixpoint predicates must be monotonic [2, Definition 2.1]. (Strictly speaking, MALL does not require monotonicity as all fixpoint definitions have solutions, but monotonicity vastly simplifies the meta-theory of µMALL.) Definition 19. A fixpoint predicate (µ or ν) is monotonic if no bound predicate symbols are negated in it.

The De Morgan dual of a fixpoint atom is defined as follows:

(µp( x ). A)( s ) = (νp( x ). [p/p]A)( s ) (νp( x ). A)( s ) = (µp( x ). [p/p]A)( s )
where the substitution [p/p] should be interpreted as replacements of atoms of the form p( t ) with p( t ).

Example 20. The following are standard inductive definitions of all (nat) and even (evn) natural numbers.

nat µnat(n). (n = z) ⊕ (∃m. (n = s(m)) ⊗ nat(m)) evn µevn(n). (n = z) ⊕ (∃m. (n = s(s(m))) ⊗ evn(m))
Here, is just a notation for abbreviations that has no manifestation in the syntax of formulas or the proof system. We will illustrate the following pair of formulas as motivating examples (both are intended to be true).

1. ∀n. nat(s(n)) ⊸ nat(n) 2. ∀n. nat(n) ⊸ (evn(n) ⊕ evn(s(n)))

Finite Unfolding

Let us first consider of fixpoints, without giving any least or greatest fixpoint semantics to µ and ν. As (5) defines equivalences, they are readily transformed into COS rules:

ξ{[ s/ x][µp( x). A/p]A} ξ{(µp( x). A)( s )} µunf ξ{[ s/ x][νp( x). A/p]A} ξ{(νp( x). A)( s )} νunf Example 21. Theorem 1 from
Example 20 is depicted in Figure 2. At the point marked ⋆, the problem has been reduced completely to a unification problem. Note that fixpoint predicates with arguments are treated as atomic formulas, so match is applicable.

Induction and Coinduction

Finite unfolding is not strong enough to prove inductive theorems, such as case (2) from Example 20. In µMALL [START_REF] Baelde | Least and greatest fixed points in linear logic[END_REF] (which uses concepts from LINC [START_REF] Tiu | A Logical Framework for Reasoning about Logical Specifications[END_REF]), such theorems are proved by the use of a specific coinduction rule:

⊢ ∀ x. (i( x ) ⊸ [i/p]A) ⊢ Γ, i( s ) ⊢ Γ, (νp( x ). A)( s ) 1 ⊤ & ∀m. (n = n) ⊗ (m = m) top, vac, onea, onem ⊤ & ∀m. (n = m) & (m = n) sym, match ⊤ & ∀m. (n = m) & nat(m) & nat(n) match ⋆ ⊤ & ∀m. (s(n) = s(m)) & nat(m) & nat(n) inj ⊤ & (∀m. (s(n) = s(m)) & nat(m)) & nat(n) all (s(n) = z) & nat(n) & (∀m. (s(n) = s(m)) & nat(m)) & nat(n) disc (s(n) = z) & (∀m. (s(n) = s(m)) & nat(m)) & nat(n) dist nat(s(n)) ⊸ nat(n) µunf Figure 2: Example 21, case (1).
Here, i schematically represents an invariant of the right arity, which can itself be a fixpoint predicate. Note that the first premise is entirely isolated from the context Γ, and therefore functions as a side-condition to the rule. This isolation from the context makes it difficult to import this rule into the COS tradition. The following is one possible formulation:

(∀x. i( x ) ⊸ [i/p]A) ⊗ ξ{i( s )} ξ{(νp( x ). A)( s )}
While sound, it is difficult to predict the impact such a non-contextual rule will have on the meta-theory. It is straightforward in the COS to give a meaning to a substitution of a derivation in a formula context by simply wrapping the context around each step of the derivation, but this kind of substitution would be disallowed by the above rule. An alternative would be to isolate the extra premise using the exponentials of the full linear logic:

ξ{!(∀x. i( x ) ⊸ [i/p]A) ⊗ i( s )} ξ{(νp( x ). A)( s )}
This rule can be shown to be sound with respect to µLL [1, sec. 4.4.1], which is the extension of µMALL with the exponential connectives. However, it is not satisfactory because it requires the exponential connectives that are largely redundant with fixpoint definitions in the first place. Moreover, the notion of monotonicity is not as straightforward for µLL as for µMALL.

The essential requirement of the coinduction rule is isolation, so the right question to ask is can we achieve isolation in a contextual form without exponentials? It is interesting to consider if this is possible in MALL itself, but we expect that it would require a non-trivial encoding of formulas. We will instead use a slight extension of MALL with a new modal connective † † † with a sole COS rule:

ξ{1} ξ{ † † † 1} isol
The syntax of formula contexts is extended with a new form, † † † ξ, as well, so rules can be applied inside † † †-formulas. However, because isol is the sole rule for † † †, it is the case that no external formula can interact with the operand of † † †.

The interpretation of this connective is the identity, i.e., † † † A and A are intended to be equi-provable. However, the connective † † † also lacks a De Morgan dual, and hence it cannot be used as a cut-formula in the admissible general cut rule. The only purpose of this extremely limited connective is to implement a contextualized version of the coinduction rule:

ξ{ † † †(∀x. i( x ) ⊸ [i/p]A) ⊗ i( s )} ξ{(νp( x ). A)(

Incremental Identity

The system µMAIS * has one remaining defect in the match rule, which for fixpoint predicates has the following form:

ξ ( s = t ) ξ (µp( x ). A)( s ) & (νp( x ). [p/p]A)( t )
The defect lies in the fact that A and A can be arbitrarily large formulas that must be found in different parts of the selected formula. This makes the rule inflexible and non-incremental, for it requires that the two fixpoint predicates be put in the right form earlier (lower) in the proof. In this section, we consider the question of whether this feature of match can be made incremental as well, in an analogous manner to the change from the aid rule of of MAS in comparison to match of MAQS.

In preparation for this modification, let us first consider the following variant of the init rule of µMALL [2, Figure 2.1]:

⊢ ∀ x . [i /p]A & [i/p]B) ⊢ (µp( x ). A)( s), (νp( x ). B)( s) fix-init
where i is a fresh predicate symbol of arity x that is not free in the conclusion. It is easy to see that this rule is stronger than init by the admissibility of arbitrary identity in µMALL. Soundness is more involved. Consider the following derivation, where the invariant i µp( x ). A.

⊢ [i /p]A, [i/p]B ⊢ ∀ x . i( x ) ⊸ [i/p]B ∀, ⊸, µ ⊢ (µp( x ). A)( s ), i( s ) init ⊢ (µp( x ). A)( s ), (νp( x ). B)( s ) ν
The unclosed left branch is proved for the specific i we chose. However, if we had a generic proof of the sequent with a free occurrence of p, then the particular instance with i substituted for p remains provable. Indeed, we can show by a simple induction that a µMALL proof remains a proof if an atomic formula in it substituted with an arbitrary formula. Through the lens of the COS, the fix-init rule becomes:

ξ † † †(∀ x. [q /p]A & [q/p]B) ⊗ ( s = t ) ξ (µp( x ). A)( s ) & (νp( x ). B)( t ) fix-match
with the side condition that q is not captured by ξ. (This can be explicitly written with a second-order quantifier ∀q. in an extension of the system of this paper to the second-order MALL.) Note that if p is not captured by ξ, then we can just reuse it and the substitution in one of the operands of the & in the premise is trivial. The † † † pseudo-connective of the previous section is reused here to isolate the check for the compatibility of the two fixpont predicates. It prevents other information from ξ from interfering with its validity. Definition 27. Let µMAIS stand for µMAIS * ∪ {fix-match}, with the understanding that match is limited to atomic predicate symbols and bound predicate symbols alone.

Theorem 28. The following rule is derivable in µMAIS:

ξ ( s = t ) ξ (µp( x ). A)( s ) & (νp( x ). A)( t )
Sketch. Note that this is the analogue of the match rule for fixpoint predicates. The proof is immediate by fix-match, isol, and the µMAIS-derivability of arbitrary identity:

ξ{1} ξ A & A .
Corollary 29. The system µMAIS is sound and complete with respect to µMAIS * .

Proof. The argument for the soundness of fix-match in µMAIS * follows the outline of the similar argument for µMALL above. The cases for the remaining rules are trivial.

Conclusion, Related Work, and Perspectives

We have now seen how to extend the calculus of structures for first-order multiplicative additive linear logic with a contextual and incremental treatment of intensional equality and inductive and coinductive fixpoints.

• Background on µMALL: We refer the interested reader to the comprehensive article [START_REF] Baelde | Least and greatest fixed points in linear logic[END_REF] for the related literature on µMALL. Classical and intuitionistic versions of µMALL also exist [START_REF] Baelde | A linear approach to the proof-theory of least and greatest fixed points[END_REF], which can be adapted into the corresponding COS calculi using the techniques of this paper.

• Equivariance: The logic µMALL forms the basis of the Bedwyr model checker [START_REF] Baelde | The Bedwyr system for model checking over syntactic expressions[END_REF], and an intuitionistic variant (the logic G) is the core of the Abella proof-assistant [START_REF] Gacek | A two-level logic approach to reasoning about computations[END_REF]. The main feature in these systems missing from µMALL is generic reasoning and nominal quantification (using the ∇-operator). Adding support for nominals to MAIS seems doable: we need to add rules for equivariance. These rules will be close to the actual implementation of equivariant unification that builds a renumbering substitution incrementally.

• Second-order: The COS has been extended to second-order propositional multiplicative linear logic [START_REF] Straßburger | Some observations on the proof theory of second order propositional multiplicative linear logic[END_REF].

There is a natural embedding of inductive and coinductive fixpoints into second-order MALL [START_REF] Baelde | Least and greatest fixed points in linear logic[END_REF]. Secondorder quantification also admits the powerful Leibniz equality. It would be interesting to see if we can give a contextual and incremental treatment to the second-order MALL. As mentioned in Section 4.3, using a second-order quantifier would simplify the fix-match rule, and make it even more incremental.

• Meta-theory and focusing: The system µMAIS is entirely compatible with the focused COS outlined in [START_REF] Chaudhuri | The Focused Calculus of Structures[END_REF]. However, the meta-theory of the focused version of µMAIS, particularly an internal completeness proof, remains for future work. An internal cut-elimination proof for µMAIS, such as one using splitting [START_REF] Straßburger | Linear Logic and Noncommutativity in the Calculus of Structures[END_REF], is also missing.

• Other deep inference systems: There are two main alternatives to the COS for deep inference: nested sequents [START_REF] Brünnler | Nested Sequents[END_REF][START_REF] Guenot | Nested Deduction in Logical Foundations for Computation[END_REF] and open deduction [START_REF] Guglielmi | A proof calculus which reduces syntactic bureaucracy[END_REF]. Unfortunately, even there the case of equality and fixpoints seems to be overlooked. At least for nested sequents it seems that the techniques outlined in sections 3 and 4 can be readily adapted. For open deduction, which further generalizes the COS to unite formulas and derivations in the same syntactic category, and admits connectives between derivations, the question of equality is obviously more complex.

• Other treatments of equality: For more mathematical uses of equality, the more standard treatment is based on paramodulation [START_REF] Robinson | Paramodulation and theorem-proving in first-order theories with equality[END_REF] rather than unification. While the paramodulation rule is certainly contextual, it is an interesting challenge to represent it in an incremental fashion. We expect the answer will be to construct a calculus of equality propagation, similar to the trans rule of Section 3.

• Alternatives to coinduction: Coinduction can also be done implicitly using cyclic proofs [START_REF] Brotherston | Sequent calculi for induction and infinite descent[END_REF]. However, it is unclear how to represent cyclic proofs in their full generality in a unary system like the COS. The cyclic structure of a branching proof can be fairly complex and is easily obscured by the interleaving of the different branches in COS proofs.

Instead of the fixpoint combinators µ and ν, we can also use definitions [START_REF] Schroeder-Heister | Rules of definitional reflection[END_REF], which are generally more user-friendly than combinators and forms the basis of the two-level approach for computaional logic [START_REF] Gacek | A two-level logic approach to reasoning about computations[END_REF]. Definitions can be straightforwardly compiled to combinators, so the approach outlined in this paper should already be sufficient, but we could also address the definition-left rule more directly by compiling it to a sequence of = rules.

• Higher-order considerations: In the higher-order case, where the relevant csus in the = rule can have more than one element, the incremental approach of µMAIS can have a real payoff over the sequent calculus. Instead of forcefully duplicating the whole sequent for each member of the csu (which can be infinite in general), we would apply the steps of Huet's algorithm as rules to simplify the higher-order equality. In fact, µMAIS can serve as a language for proof certificates for higher-order unification. The steps of higher-order unification can be interleaved with ordinary logical reasoning. This is indeed already the approach taken by most systems that implement higher-order (pattern) unification: it is common to build a constraint management system for higher-order equality assumptions that cannot be immediately discharged [START_REF] Reed | Higher-order constraint simplification in dependent type theory[END_REF]. Notes: in the ⊕ rule, i ∈ {1, 2}; in the ∀ rule, x is not free in Γ; the cut rule is admissible, but not part of the system; and this proof system is primarily drawn from [2, Figure 1]. Notes: in wit, the substitution [t/x]A is capture-avoiding; in all and ex, x is not free in A; in µMAIS * , the match rule is understood to apply to (free or bound) predicate symbols and fixpoint predicates; and In µMAIS, the match rule is understood to apply to (free or bound) predicate symbols only, and q is a predicate symbol that is not captured by ξ.

MALL ⊢ a, a init ⊢ Γ, a ⊢ ∆, a ⊢ Γ, ∆ cut ⊢ Γ, A ⊢ ∆, B ⊢ Γ, ∆, A ⊗ B ⊗ ⊢ 1 1 ⊢ Γ ⊢ Γ, ⊥ ⊥ ⊢ Γ, A i ⊢ Γ, A 1 ⊕ A 2 ⊕ ⊢ Γ, [t/x]A ⊢ Γ, ∃x. A ∃ ⊢ Γ, A, B ⊢ Γ, A & B & ⊢ Γ ⊢ Γ, ⊥ ⊥ ⊢ Γ, A ⊢ ∆, B ⊢ Γ, A & B & ⊢ Γ, ⊤ ⊤ ⊢ Γ, A ⊢ Γ,

Figure 1 :

 1 Figure 1: The system MAS.

  ∃x. ∀y. ∃z. ∀w. (x = w) ⊗ (y = z) ∃x. ∀y. ∃z. ∀w. p(x, y) ⊸ p(w, z) match ∃x. ∀y. ∃z. p(x, y) ⊸ (∀x ′ . p(x ′ , z)) all ∃x. ∀y. p(x, y) ⊸ (∃y ′ . ∀x ′ . p(x ′ , y ′ )) ex ∃x. (∃y. p(x, y)) ⊸ (∃y. ∀x ′ . p(x ′ , y)) all (∀x. ∃y. p(x, y)) ⊸ (∃y. ∀x. p(x, y)) ex

Definition 12 .

 12 The following (infinite set of) axioms characterize first-order equality. 3 ∀x. (x = x), ∀x, y. (x = y) ⊸ (y = x), ∀x, y, z. (x = y) ⊗ (y = z) ⊸ (x = z), ∀x, y. (x = y) ⊸ 1, ∀x, y. (x = y) ⊸ (x = y) ⊗ (x = y), ∀ x, y. ( x = y ) ⊸ f( x ) = f( y ), ∀ x, y. ( x = y ) ⊸ p( x ) ⊸ p( y ).

Figure 3 :

 3 Figure 3: Example 21, case (2).

  ∀x. A ∀ . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . QMALL = MALL ∪ ⊢ t = t = for every θ ∈ csu(s, t), ⊢ θΓ ⊢ Γ, s = t = . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . µMALL = QMALL ∪ ⊢ Γ, [ s/ x, (µp( x ). A)/p]A ⊢ Γ, (µp( x ). A)( s ) µ ⊢ Γ, i( s ) ⊢ ∀x. (i( x ) ⊸ [i/p]A) ⊢ Γ, (νp( x ). A)( s ) ν

Figure

  Figure 4: Sequent calculus for µMALL

  refl ξ ( s = t ) ξ f( s ) = f( t ) cong ξ{∃x. (A & B)} ξ{A & ∃x. B} ex . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . MAQS = MAUS ∪ ξ{⊥} ξ{s = t}qwkξ{(s = t) & (s = t)} ξ{s = t} qct ξ{t = s} ξ{s = t} sym ξ{t = s} ξ{s = t} nsym ξ{(t = u) ⊗ (s = v)} ξ{(s = t) & (u = v)}trans . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . MAIS = MAQS ∪ ξ{⊤} ξ f( s ) = g( t ) disc ξ{⊤} ξ{x = τ{x}} fin ξ ( s = t ) ξ f( s ) = f( t ) inj . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . µMAIS * = MAIS ∪ ξ{[ s/ x, (µp( x). A)/p]A} ξ{(µp( x). A)( s )} µunf ξ{ † † †(∀x. i( x ) ⊸ [i/p]A) ⊗ i( s )} ξ{(νp( x ). A)( s )} coind ξ{1} ξ{ † † † 1} isol . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . µMAIS = µMAIS * ∪ ξ † † †(∀ x. [q /p]A & [q/p]B) ⊗ ( s = t ) ξ (µp( x ). A)( s ) & (νp( x ). B)( t ) fix-match

Figure 5 :

 5 Figure 5: The COS systems comprising µMAIS * and µMAIS

  Definition 13 (System MAIS). Let MAIS stand for MAQS ∪ {disc, fin, inj} It is interesting to note that we can separate finiteness from discrimination in MAIS. Dropping fin, for instance, allows MAIS to reason naturally about infinite terms. Here is an example of discrimination interacting with transitivity in MAIS.

	Example 14.

  System µMAIS * ). Let µMAIS * stand for:

s )} coind Definition 22 (MAIS ∪ {µunf, coind, isol} Fact 23. µMAIS * is conservative over MAIS. Theorem 24. The νunf rule is derivable in µMAIS * . Proof. Use i( x ) [(νp( x ). A)/p]A for coind.

  ). Case[START_REF] Baelde | Least and greatest fixed points in linear logic[END_REF] of Example. 20 can be proved in µMAIS * with the invariant i(x) evn(x) & evn(s(x)). The proof begins as in Figure3, (a), and then the isolated subformula indicated by M is independently proved. It is a fairly straightforward matter to use µunf and the remaining rules of MAIS for it; one case is sketched in (b). A † † †-free formula is provable in µMAIS * if and only if it is provable in µMALL.Sketch. Straightforward extension of the proofs of theorems 15 and 18. The new rules of µMAIS * are all valid entailments or admissible rules in µMALL, assuming that † † † A is treated as equivalent to A, and the shallow coinduction, unfolding, and identity rules of µMALL can be simulated by µMAIS * .

	Theorem 26.

  4: Sequent calculus for µMALL . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

	MAX ξ{(A ξ{A & & (B B) & & C)} C}	assoc	ξ{B ξ{A	& &	A} B}	comm		ξ{(A ξ{(A ⊗ B) & C) ⊗ B} & C}	swl	ξ{B ⊗ (A ξ{A & (B ⊗ C)} & C)}	swr	ξ{1} ξ{1 ⊗ 1}	onem
	ξ{A} ξ{A ⊕ B}	chl	ξ{B} ξ{A ⊕ B}	chr	ξ{[t/x]A} ξ{∃x. A}	wit	ξ{(A ξ{A &	B) & (A & (B & C)} & C)}	dist	ξ{⊤} ξ{A & ⊤}	abs	ξ{1} ξ{⊤}	top	ξ{1} ξ{1 & 1}	onea
	ξ{A} ξ{A & ⊥}	bot	ξ{∀x. (A ξ{A & ∀x. B} & B)}	all	ξ{1} ξ{∀x. 1}	vac			. . . . .	MAS = MAX ∪	ξ{1} ξ{a & a}

aid MAUS = MAX ∪ ξ ( s = t ) ξ p( s ) & p( t ) match ξ{1} ξ{x = x}

In this paper, we will read inference rules from conclusion to premise(s).

We write bvs(ξ) for the variables bound in ξ that are visible at its hole.

These are the linear versions of the axioms from[13, p.236].

Acknowledgement: Thanks to Dale Miller and Lutz Straßburger for many useful discussions. This work was partially funded by the ERC Advanced Grant ProofCert, and the Demtech grant from the Danish Council for Strategic Research.


Histoires croisées des orphelins et de l'adoption

Histoires croisées des orphelins et de l'adoption Introduction

Abandon et adoption sont souvent associés dans la littérature et dans les sciences humaines et sociales comme une réponse à un problème social touchant l'enfance 1 . Considérée comme l'histoire d'un enfant sans parents qui rencontre un couple (ou un célibataire) sans enfant, l'adoption rassemble dans la même catégorie des adoptés des enfants orphelins et abandonnés. En effet, être sans parent ne signifie pas toujours être orphelin, d'où une confusion des termes et des situations qui se retrouve jusque dans un titre paradoxal comme : Les orphelins de mères vivantes… pour définir les enfants abandonnés 2 . Mettre en perspective l'histoire des orphelins et celle de l'adoption, c'est apporter des éléments d'explication à l'indifférenciation et l'invisibilité des orphelins.

Regarder en arrière permet de constater que l'adoption a d'abord été pensée, définie et mise en pratique pour donner une nouvelle famille aux seuls orphelins. En effet, dans le passé, la société française a fait une nette distinction entre enfants abandonnés et enfants orphelins avant de les confondre au cours du XIX e siècle (I). A partir de 1923 et la possibilité d'adopter juridiquement un mineur, l'enfant adoptable a été chargé de nombreux fantasmes, dont celui de l'enfant vierge de tout passé. L'orphelin complet, sans père ni mère est considéré comme l'enfant idéal par beaucoup de candidats à l'adoption (II). Devenant surtout internationale à la fin du XX e siècle, l'adoption continue à entretenir l'amalgame entre enfants orphelins et enfants confiés en adoption. Ces derniers étant bien trop souvent considérés comme ayant perdu leurs parents, ce qui est rarement le cas (III).

I -La prise en charge spécifique des orphelins par l'adoption (XVI e -XIX e siècles)

Sous l'Ancien Régime, la distinction entre orphelins et enfants abandonnés est très nette. On oppose même les enfants trouvés dans les rues et les enfants abandonnés récupérés dans les « tours » des hôpitaux aux enfants orphelins. Des premiers on ne sait rien ou presque et ils sont très souvent considérés comme des bâtards, des seconds, légitimes, on connaît les origines et la parenté.

n'ont plus ni père, ni mère. Ces maisons (Saint Esprit, Enfants-Rouges, etc.) insistent bien sur la légitimité des enfants accueillis, qui ne doivent pas être confondus avec les enfants abandonnés, bien plus (trop) nombreux et ne suscitant pas la même compassion. Les familles ne se désintéressent pas des orphelins ainsi placés et leurs conditions de vie (alimentation, soins…) sont bien meilleures que celles des enfants abandonnés recueillis par le bureau des Enfants-Trouvés4 .

La déclaration des Droits de l'homme et du citoyen du 26 août 1789, en déclarant que « tous les hommes naissent et demeurent libres et égaux en droits » réduit la distinction entre orphelins et abandonnés, et donc les formes d'assistance spécifique aux premiers. L'adoption nationale créée par la Convention est certes réservée aux seuls orphelins, mais de parents ayant rendu de grands services à la Révolution comme les six enfants du canonnier Richer tué en Vendée. Il s'agit donc d'une forme d'adoption d'honneur. En 1795, des Maisons nationales des Orphelins sont organisées sur le modèle des hôpitaux pour orphelins de l'Ancien Régime, mais accueillent plus largement des enfants nécessiteux. Pendant toute la Révolution, de nombreux projets de rédaction d'une loi sur l'adoption des enfants se succèdent sans jamais être votés. Le texte de 1803 -intégré dans le code civil en 1804 -ne peut être en rien une réponse à l'orphelinat, puisqu'il réserve l'adoption aux seuls majeurs (21 ans). Néanmoins, le code a prévu une tutelle officieuse qui permet de prendre en charge un enfant isolé de moins de quinze ans. Ainsi, des orphelins collatéraux (neveux ou nièces) sont pris en charge puis adoptés à leur majorité. Mais il ne s'agit que d'un nombre limité et dans les familles aisées seulement.

Un décret de 1811 définit trois catégories d'enfants devant bénéficier de l'assistance publique. Avec les enfants trouvés et les enfants abandonnés, les orphelins pauvres sont définis comme « ceux, qui, n'ayant ni père, ni mère n'ont aucun moyen d'existence » (article 6). Les mêmes secours sont apportés aux uns et aux autres5 . Á Paris, en 1838, les orphelins et les enfants abandonnés sont rassemblés dans l'Hospice Saint-Vincent-de-Paul de la rue de l'enfer dont l'appellation officielle est désormais Hospice des Enfants-Trouvés et des Orphelins. En 1842, l'assimilation des enfants trouvés-enfants orphelins est décrétée par les pouvoirs publics. Un administrateur de l'hospice déplore la confusion des deux catégories de sans famille que sont les « enfants du vice » et les « enfants du malheur » (les orphelins) car elle leur fait perdre à ces derniers « la considération due à leur infortune ». Dans les faits, c'est la philanthropie privée qui va prendre en charge les seuls orphelins, l'hospice se chargeant des autres. Ainsi, la Société auxiliaire du Comité pour le placement et l'apprentissage des jeunes orphelins -dépendant de la Société de la Morale chrétienne -prend en charge quelques dizaines d'enfants. Des artisans demandent à « adopter » les orphelins placés chez eux en apprentissage6 .

L'abbé Maîtrias fonde en 1857 l'Oeuvre de l'Adoption qui a pour but d'accompagner des enfants trouvés ou abandonnés jusqu'à 18 ans pour les garçons, 21 ans pour les filles7 . Á une époque où l'adoption des enfants n'est pas prévue par la loi, l'appellation est trompeuse. En tout cas, « l'adoption » cesse d'être réservée aux orphelins. En 1866, l'abbé Roussel fonde ce qui deviendra l'Oeuvre des Orphelins-Apprentis d'Auteuil. Elle recueille en priorité des petits mendiants, orphelins ou pas8 . De même l'appellation « orphelinat » qui se généralise dans ces années-là ne nomme t-il pas un établissement exclusivement réservé aux orphelins.

Lorsque la Troisième République succède au Second Empire (1870), l'amalgame entre enfants abandonnés et orphelins est devenu prégnant. Á partir de 1904, les pupilles de l'État rassemblent tous les enfants de l'assistance publique.

II -Orphelins et enfants sans partage dans l'adoption contemporaine

Dans le contexte de la saignée démographique de la Grande Guerre, l'enfant représente une promesse d'avenir et l'orphelin de guerre est l'incarnation du sacrifice de toute une génération. Plusieurs lois définissent pour eux le statut de pupille de la nation, à ne pas confondre avec celui de pupille de l'État [START_REF] Olivier | L'appellation « pupille » se retrouve également dans les Pupilles de l'école publique (PEP), qui rassemblent dans l'après-guerre des orphelins de guerre, des orphelins civils mais aussi des enfants nécessiteux, voir Gardet Mathias[END_REF] . Néanmoins on peut dire que les pupilles de l'État, comme les pupilles de la nation, sont en quelque sorte tous « adoptés » par l'État, mais de manière très différente.

Á partir de 1923 les pupilles de l'État peuvent être adoptés par des familles. En effet, opérant un retournement de la finalité de l'adoption définie en 1804, la loi du 19 juin 1923 autorise l'adoption de mineurs par des adoptants âgés d'au moins 40 ans et sans enfant. Les liens avec la famille d'origine ne sont pas rompus. Jusqu'en 1939, le nombre d'adoptions varie entre 1 000 et 1 700 par an… ce qui est peu. Pourquoi ? Parce que les adoptants veulent des enfants sans partage ! Les enfants abandonnés peuvent toujours, à un moment ou à un autre, être réclamés par leurs parents avec lesquels les liens ne sont pas rompus sur le plan juridique. Dans ces conditions, l'enfant orphelin présente évidemment un avantage incomparable aux yeux des candidats à l'adoption.

Á l'automne 1936, des Français demandent à adopter des enfants espagnols réfugiés de la guerre civile que la presse considère comme des orphelins. Par exemple, plus de 300 d'entre eux partis du Pays basque arrivent à Angers en septembre. Dans leurs lettres les demandeurs précisent bien que c'est un orphelin qu'ils souhaitent adopter, le fait qu'il soit étranger diminue encore le risque de difficulté ultérieure. Mais les autorités comme les associations sont très méfiantes. Après vérification, l'Union Internationale de Secours aux Enfants peut indiquer que l'immense majorité de ces enfants ne sont pas orphelins et que l'adoption est inenvisageable pour les quelques enfants qui le sont vraiment puisqu'ils ont également vocation à rentrer en Espagne lorsque la situation le permettra [START_REF]Archives départementales de Maine-et-Loire, 13 α 13[END_REF] .

Après plusieurs projets législatifs, le décret-loi du 29 juillet 1939 (Code de la Famille) réforme l'adoption ordinaire : pour les moins de 16 ans, la rupture avec la famille d'origine devient possible sur décision du tribunal. Surtout une « légitimation adoptive » est instituée : par jugement un couple (l'un des deux devant être âgé de plus de 35 ans) peut prendre en charge un enfant de moins de 5 ans. Mention est faite sur l'acte de naissance. L'adopté a les mêmes droits et obligations qu'un enfant légitime. Il porte le nom des adoptants, le but recherché est de se rapprocher au maximum du modèle familial. Le statut moderne de l'adopté naît avec cette loi. En 1941 et 1943 d'autres textes vont dans ce sens. En 1949, les adoptants peuvent changer le prénom de l'enfant adopté [START_REF] Mécary | L'adoption[END_REF] .

La loi de 1939 entraîne aussitôt l'augmentation du nombre des adoptions, surtout des légitimations adoptives qui devient la forme d'adoption la plus prisée. Dans l'après-guerre, environ 4 000 enfants très jeunes sont ainsi adoptés chaque année. Parmi eux, des orphelins que des intermédiaires placent auprès de familles en vue de légitimation adoptive : la Croix-Malte participèrent à l'évacuation d'enfants biafrais vers le Gabon et la Côte d'Ivoire. Les autorités françaises s'opposèrent à toute adoption de ces soi-disant orphelins, au motif que « les enfants devaient être maintenus dans leur environnement africain habituel et à proximité de leurs familles » 18 . Seuls quelques enfants sont accueillis en France pour des raisons très particulières. D'après une autobiographie publiée récemment, une petite fille de cinq ans, réputée orpheline a été accueillie en France en 1970 afin de soigner son handicap. A l'âge de douze ans, elle découvre que son père et sa mère sont vivants et que le gouvernement nigérian exige qu'elle rentre au pays [START_REF] Ubanatu | La petite fille qui dansait dans sa tête[END_REF] .

Dans les années 1970 arrivent en France des enfants boat people. Sans papier, leur statut d'orphelin n'est pas prouvable. Il n'est donc pas question de les faire adopter malgré de nombreuses offres. Un reportage diffusé à la télévision en juillet 1980 sur les enfants cambodgiens du vaste camp de Kao i Dang (Thaïlande) pose bien la question de l'adoptabilité. Pour les humanitaires présents sur place, il est impossible de savoir si les enfants sont orphelins. Dans les désordres de l'exil, beaucoup sont perdus. Un grand panneau affiche des photos d'enfants que leurs parents recherchent alors qu'une bénévole française tient dans ses bras un bébé qu'elle veut adopter. Toute la question est là 20 .

A partir des années 1980, les trois-quarts des enfants adoptés en France sont des enfants étrangers que les adoptants sont allés chercher ou qu'ils ont fait venir. Parmi eux, combien d'orphelins ? Impossible à préciser, mais bien peu. La grande majorité des enfants étrangers adoptés ont des parents qui ont consenti à leur adoption, y compris l'enfant adopté par Madonna au Malawi en 2006. Beaucoup d'enfants des orphelinats du monde ne sont pas orphelins. Mais la demande crée l'offre, ce qui est propice à toutes les déviances. Les exemples sont nombreux dans l'Amérique latine des années 1980 et 1990 d'enfants proposés à l'adoption en tant qu'orphelins mais dont les parents ont été abusés [START_REF] Yves | Des enfants venus de loin[END_REF] .

En 2002, un couple accueille deux enfants centrafricains dont la mère est morte du SIDA et le père disparu en brousse selon l'organisme agréé pour l'adoption qui les leur a confiés. Mais l'intermédiaire en Afrique de l'association a dissimulé la vérité : la mère des deux enfants est bien vivante et a cru les confier pour le temps de leur éducation seulement alors qu'on lui a fait signer un papier (qu'elle ne savait lire) indiquant son accord pour un placement en adoption [START_REF] Libération | Adoption : les ratages du contrôle[END_REF] . L'affaire de l'Arche de Zoé au Tchad est l'un des derniers épisodes en date de ce genre.

Conclusion

L'histoire des orphelins et celle de l'adoption sont étroitement associées jusqu'au XIX e siècle. L'enfant orphelin, victime innocente, est considéré comme insérable dans une autre famille alors que l'enfant abandonné, taré de par ses origines, est l'objet de méfiance et ne suscite pas la même compassion. Paradoxalement, ceux-ci plus que ceux-là peuplent alors les orphelinats. La prise en charge par l'État de tous les enfants à secourir impose lentement une indifférenciation entre eux. Bien moins nombreux, les orphelins en deviennent presque invisibles. L'adoption des mineurs telle qu'elle est instituée en 1923 ne leur est plus réservée, heureusement peut-on dire. Cependant l'enfant orphelin demeure dans l'inconscient collectif l'enfant adoptable par excellence. Combien de couples adoptants ont ramené d'un « orphelinat » étranger un enfant… qui n'est pas orphelin ? L'histoire des orphelins demeure largement à faire autour des enfants eux-mêmes et de leur spécificité sans les confondre avec d'autres, sans recréer non plus des distinctions basées sur des considérations d'une autre époque. Dans cette perspective, l'histoire de l'adoption peut apporter une contribution intéressante.

Yves Denéchère Professeur d'histoire contemporaine Université d'Angers -UMR CERHIO

Dès 1536, la Charité de Lyon pratique l'adoption hospitalière d'enfants légitimes, orphelins de père et de mère, âgés de 7 à 14 ans. Mais tous les enfants adoptables ne sont pas adoptés : c'est en quelque sorte un privilège réservé à quelques-uns. L'orphelin adopté voit tout ou partie de ses biens administrés par l'hôpital et reçoit une éducation soignée. Mais pour léguer, tester ou se marier il doit obtenir une autorisation de l'établissement. De 1630 à 1650 plusieurs arrêts du Parlement de Paris clarifient les procédures et l'adoption se fait de plus en plus au cours d'une cérémonie solennelle. D'autres orphelins des hôpitaux sont recueillis par des particuliers « pour l'amour de Dieu », ce qui donne lieu parfois à la siganture d'actes officiels. En 1635, un mercenaire suisse et son épouse confient leur petite fille à un habitant de Beaune. Devenue orpheline, Élisabeth est adoptée par acte notarial en 1653. Elle se marie peu après, ceci expliquant sans doute cela 3 .Un récent ouvrage consacré aux orphelins de Paris aux XVI e -XVIII e siècles montre qu'il existe de nombreux secours organisés pour leurs venir en aide. Les hôpitaux pour orphelins sont des établissements spécialisés auxquels les familles confient des enfants qui1 Trillat Brigitte (dir.), Abandon et adoption. Liens du sang, liens d'amour, Revue Autrement, série Mutations, n°96, février 1988. 2 Charles François, Les orphelins de mères vivantes, Paris, La Pensée Universelle, 1982. 3 Gutton Jean-Pierre, Histoire de l'adoption en France, Paris, Publisud, 1993, pp.64-85.

Robin-Romero Isabelle, Les orphelins de Paris. Enfants et assistance aux XVI e -XVIII e siècles, Paris, Presses de l'Université Paris-Sorbonne, 2007.

Décret du 19 janvier 1811 concernant les enfants trouvés ou abandonnés et les orphelins pauvres.

Leplaige Danielle, Sans famille à Paris. Orphelins et enfants abandonnés de la Seine au XIX e siècle, Paris, Le Centurion, 1989.

Dahyot-Dolivet Mgr, Et le Seigneur m'a recueilli. L'Abbé Maîtrias et l'oeuvre de l'adoption, Paris, SOS, 1980.

Gardet Mathias et Vilbrod Alain, Les Orphelins-Apprentis d'Auteuil. Histoire d'une oeuvre, Paris, Belin, 2000.

Hazan Katy, Les orphelins de la Shoah. Les maisons de l'espoir 1944-1960, Paris, Éditions Belles Lettres, 2000.

Launay Clément, Soulé Michel, Veil Simone, L'adoption. Données médicales, psychologiques et sociales, Paris, Éditions ESF, 1971, pp.27-28 et 34.

« Dans mon village » (Henry Lemarchand -Francis Lopez), 1956.

Centre des archives diplomatiques de Nantes, fonds de l'ambassade de France à Bogotá série C, carton n°41, dossier Joséphine Baker.

Pour des repères sur l'adoption internationale, voir Denéchère Yves, Des enfants venus de loin. Histoire de l'adoption internationale en France, Paris, Armand Colin, 2011.

Kaiser Edmond, La marche aux enfants, Lausanne, Éditions Pierre-Marcel Favre, 1979, p.393.