Thomas Ehrhard
email: ehrhard@irif.fr

Farzad Jafarrahmani

Alexis Saurin
email: alexis.saurin@irif.fr

Polarized Linear Logic with Fixpoints

Keywords: linear logic, least and greatest fixed points, classical lambda-calculus, categorical semantics, relational semantics

We introduce and study µLLP, which can be viewed both as an extension of Laurent's Polarized Linear Logic, LLP, with least and greatest fixpoints, and as a polarized version of Baelde's Linear Logic with fixpoints (µMALL and µLL). We take advantage of the implicit structural rules of µLLP to introduce a term syntax for this language, in the spirit of the classical lambda-calculus and of system L in the style of Curien, Herbelin and Munch-Maccagnoni. We equip this language with a deterministic reduction semantics as well as a denotational semantics based on the notion of non-uniform totality spaces and the notion of categorical model for linear logic with fixpoint introduced by Ehrhard and Jafarrahmani. We prove an adequacy result for µLLP between these operational and denotational semantics, from which we derive a normalization property for µLLP thanks to the properties of the totality interpretation.

Introduction

One major feature of Linear Logic (LL) is that it gives a very clear and clean status to the polarity of formulas and connectives. Logical LL constants and connectives are organized in positive/negative dual pairs 0/⊤, ⊕/&, 1/⊥ and ⊗/`which are De Morgan dual pairs swapped by linear negation ( ) ⊥ . From a proof-search point of view, negative constants and connectives are characterized by the reversibility of the associated sequent calculus inference rules and positive ones by the focusing property, see [START_REF] Andreoli | Logic programming with focusing proofs in linear logic[END_REF]. From a Curry-Howard point of view polarization is also extremely meaningful. Positive formulas P , stable under the positive connectives and containing the positive constants as well as all the formulas of shape !A, are equipped with a canonical proof of P ⊸ !P . This implies that the negative formulas (the P ⊥ 's) have structural rules. This crucial property offers two ways to embed classical logic into LL (call-by-name and call-by-value) and each of these embeddings equip classical logic with an operationally meaningful cutelimination 5 . This canonical proof P ⊸ !P means that positive types are discardable and duplicable, that is, have an associated let construct, in other words, positive types are data-types (see [START_REF] Munch-Maccagnoni | Syntax and models of a non-associative composition of programs and proofs[END_REF] for discussions on this programming viewpoint, notably in connection with call-by-push-value [START_REF] Blain | Call-by-push-value: A functional/imperative synthesis[END_REF][START_REF]Call-by-push-value: Decomposing call-by-value and call-by-name[END_REF]). This version of LL which features two dual classes of positive and negative formulas exchanged by linear negation is called Polarized Linear Logic (LLP) and has been introduced and studied in [START_REF] Laurent | Etude de la polarisation en logique[END_REF], together with translations from the λµ-calculus [START_REF] Parigot | Lambda-mu-calculus: An algorithmic interpretation of classical natural deduction[END_REF] to LLP, a sequent calculus, a theory of proof-nets, translations to LL as well as a denotational semantics [START_REF] Laurent | About translations of classical logic into polarized linear logic[END_REF] which is based on the idea of representing positive formulas as objects of the Eilenberg-Moore category of the !-comonad of a categorical model of LL as suggested in [START_REF] Girard | A new constructive logic: Classical logic[END_REF]. In this system the exponential connectives allow to move from one polarity to the other one: if N is negative !N is positive and if P is positive ?P is negative.

So LLP can be considered as a kind of "classical λ-calculus" (in the sense that the structural rules are kept implicit) where the fine-grained LL resource-handling associated with the exponentials is nevertheless available. In the single-sided version of LLP that we use in this paper, there are two kinds of sequents: those which have only negative formula (called negative sequents) and those which have negative formulas and exactly one positive formula (called positive sequents) 6 . Various proof-term systems have been introduced to account for LLP-like formalisms in a syntactic way that is closer to the λ-calculus than the usual proof systems such as sequent calculus or proof-nets, such systems are often called system L see for instance [START_REF] Curien | The duality of computation[END_REF][START_REF] Munch-Maccagnoni | Syntax and models of a non-associative composition of programs and proofs[END_REF] and are based on the distinction between three kinds of expressions: (i) negative terms, (ii) positive terms and (iii) commands which are pairings (applications) of a negative term to a positive term representing logical cuts.

Many other polarized calculi have been considered in the literature, ranging from strictly logicallyoriented calculi to more programming-oriented calculi. On the programming side of this spectrum, one can refer to Abel et al's copatterns [START_REF] Abel | Well-founded recursion with copatterns and sized types[END_REF][START_REF] Abel | Copatterns: programming infinite structures by observations[END_REF][START_REF] Setzer | Unnesting of copatterns[END_REF], which account for the definition of codata by observations and which revealed to be flexible enough to be integrated to various programming environment even with rich type-systems, as well as Ariola and Downen computational calculi developed on system L [START_REF] Downen | The duality of construction[END_REF][START_REF]Beyond polarity: Towards a multi-discipline intermediate language with sharing[END_REF][START_REF]A computational understanding of classical (co)recursion[END_REF] which allow for the combination of various evaluation strategies. On the logical side, one can refer to Zeilberger's polarized calculi [START_REF] Zeilberger | Focusing and higher-order abstract syntax[END_REF][START_REF] Daniel | Focusing on binding and computation[END_REF][START_REF]Polarity and the logic of delimited continuations[END_REF], directly inspired by Andreoli's focusing, or Baelde et al's polarized calculus for µMALL [START_REF] Baelde | Least and greatest fixed points in ludics[END_REF] which follows a slightly different tradition on polarity [START_REF] Girard | Locus solum[END_REF]. On more related works from a categorical models point of view, one can mention [START_REF] Hamano | On geometry of interaction for polarized linear logic[END_REF], [START_REF] Hamano | A categorical semantics for polarized mall[END_REF] and [START_REF]Polarized category theory, modules, and game semantics[END_REF]. However, those models are more related to the proof-search paradigm and they deal with reversibility and focalization. And we emphasize on the fact that what we will provide as model of κµLLP is related to the Curry-Howard paradigm, that is to say it deals with structural rules (i.e.,negative formulas have canonical contraction and weakening rules).

In many of the above-mentioned works, polarities are instrumental in shaping the dual computational behaviour of inductive versus coinductive types: while inductive data is positive in nature, coinductive data is negative. This observation was made formal from a proof-theoretic point of view in the line of work initiated by Baelde's thesis and his follow up works [START_REF] Baelde | A linear approach to the proof-theory of least and greatest fixed points[END_REF][START_REF]Least and greatest fixed points in linear logic[END_REF][START_REF]Infinitary proof theory: the multiplicative additive case[END_REF] that the least fixpoint is a positive logical construct while the greatest fixpoint is negative: in linear logic with fixpoints, the fixpoint operators satisfy the focusing property, both in the finitary setting with Park's rules and in the non-wellfounded and circular setting.

In this paper, following the Curry-Howard-Lambek approach to the linear logic with least and greatest fixpoints µLL initiated in [START_REF] Ehrhard | Categorical models of linear logic with fixed points of formulas[END_REF], we study µLLP, an extension of LLP with least and greatest fixpoints (we refer to [START_REF] Baelde | A linear approach to the proof-theory of least and greatest fixed points[END_REF][START_REF] Ehrhard | Categorical models of linear logic with fixed points of formulas[END_REF] for a general introduction to µLL and the associated literature), by introducing and studying a system L calculus for a polarized version of µLL. The search for a maximal syntactic simplicity guided our design of this calculus, see Figure 2 where we use the Greek letter κ for the name binder instead of the more traditional µ/μ which would lead to confusions with the standard notation associated with least and greatest fixpoints (µ/ν). Related to this syntactical simplicity is that a negative term or a command can be typed by a negative or a positive sequent so that there are actually five kinds of typing judgments and this partitioning is taken into account by the semantics. The polarization of fixpoints means that least fixpoints allow to define data-types (integers, lists, trees etc.) while greatest fixpoints allow to define codata-types, that is types of data-consumers 7 . We refer to [START_REF] Abel | Copatterns: programming infinite structures by observations[END_REF] for a detailed discussion of the computational duality between data-and co-data-types. As in [START_REF]Least and greatest fixed points in linear logic[END_REF][START_REF] Ehrhard | Categorical models of linear logic with fixed points of formulas[END_REF] we use the two-premise Park's rule for introducing greatest fixpoints so that our terms are finite trees.

The typed calculus introduced in that way is called κµLLP. It features natural construction rules associated with the positive connectives and constants (pairing for ⊗, injections for ⊕ etc). It has a positive promotion construct s ! for putting a negative term s in a box (or thunk ) which can be used as a piece of data and a negative dereliction der(p) which allows to open such a box. Just as the λµ-calculus, κµLLP has names α, β . . . associated with the negative formulas of a sequent 8 . Since at most one positive formula can occur in an LLP sequent, we need only one variable that we denote as •. There are several binders for names: one general binder κα.c which allows to select a negative formula in the context, and the other ones are associated with ⊥, `and Park's rule. All these binders produce a negative term whose type is a negative formula made active for further uses. There is also a binder κ.c associated with the unique variable • which produces a positive term. One crucial feature of • is that it can occur only linearly in a command or negative term. Again, this is due to the fact that all the formulas in the context of a promotion must be negative. Notice also that • cannot occur free in a positive term due to the fact that a positive sequent has exactly one positive formula. All these binders apply to commands which are cuts s ⋆ p between a negative term s and a positive term p. Our operational semantics provides only reduction relations for commands and can be seen as describing the interactions between positive constructors and negative destructors. One specific critical command is κα.c ⋆ κ.d which could a priori lead to c [κ.d/α] or d [κα.c/•]; we choose the second option (see Remark 2.9) making our reduction semantics deterministic; we are actually defining a kind of abstract machine whose states are commands s⋆p where s is the program and p is the stack (there are no environments because substitutions are executed immediately). Our goal in this paper is twofold. On the one hand, we provide a categorical semantics of κµLLP building on [START_REF] Ehrhard | Categorical models of linear logic with fixed points of formulas[END_REF]. Given a model (L, -→ L ) (simply denoted as L) of µLL (in the sense of that paper) the main idea is standard: interpret a closed positive formula P as an object of the Eilenberg-Moore category L ! . This requires however to deal also with open positive formulas: we take them into account introducing in Section 4 the notion of positive functors which are strong functors (as specified by L) equipped with a distributive law wrt. the comonad !, they are a functorial generalization of the notion of !-coalgebra. We illustrate this semantics in the concrete models Rel and Nuts used in [START_REF] Ehrhard | Categorical models of linear logic with fixed points of formulas[END_REF].

On the other hand, we also prove some form of normalization (cut-elimination) for κµLLP. This turned out to be surprisingly difficult. The solution came from understanding that proving a termination property with respect to the relational semantics -saying very roughly that if a command has a non-empty relational semantics its reduction terminates -would be possible because the points of the relational model are finite trees on which induction is possible. Concretely this means that we associate sets of terms to points of the relational models and these sets are easily defined by induction. To make this proof of normalization more natural we also provide a presentation of the relational semantics of κµLLP as an intersection typing system. To derive from this relational normalization a standard normalization property, it is enough to prove that, in sufficiently many meaningful situations, when c ⊢ α : N , the command c has a non-empty relational semantics. We do that for N = ?nat where nat is a type of integers defined as a least fixpoint formula. The model Nuts of non-uniform totality spaces gives us precisely this information: any total subset of the relational interpretation of ?nat is non-empty and hence, in particular, the interpretation of c is non-empty.

The syntax

Remark 2.1 In this paper we present various deduction systems by means of inference rules. It is essential to keep in mind that, for all of these systems, we consider only finite deduction trees. Of course in other µLL-based logical systems [START_REF]Infinitary Proof Theory: the Multiplicative Additive Case[END_REF][START_REF] Doumane | On the infinitary proof theory of logics with fixed points[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] such as µMALL ∞ , some of these finite trees would be unfolded into infinite deduction trees (satisfying suitable global conditions), but such infinite deductions will never be considered here.

We assume to be given an infinite set of literals denoted ζ, ξ, . . . . Positive formulas P, Q, . . . and negative formulas M, N, . . . are given in Figure 1. Linear negation is defined as usual by induction on formulas, it turns positive formulas into negative ones and conversely. The main cases are (ζ Although not strictly necessary, we adopt the convention that for a given literal ζ it is never the case that both ζ + and ζ -occur in a given formula. This property can be enforced by α-renaming for closed formulas.

+ ) ⊥ = ζ -, (ζ -) ⊥ = ζ + , (µζ.P ) ⊥ = νζ.P ⊥ and (νζ.N ) ⊥ = µζ.N ⊥ . P, Q, • • • := ζ + | 1 | P ⊗ Q | 0 | P ⊕ Q | µζ.P | !N M, N, • • • := ζ -| ⊥ | M `N | ⊤ | M & N | νζ.N | ?P
An important operation is substitution of formulas in formulas, it is defined in the obvious way (performing as usual α-renaming of type variables when needed). More precisely we define by induction on a negative or positive formula A:

• substitution of a positive formula P for a positive variable ζ + in A, written A [P/ζ + ] • and substitution of a negative formula N for a negative variable

ζ -in A, written A [N/ζ -],
both formulas having the same polarity as A. We use fv(A) for the set of free variable of the type A.

Lemma 2.3 One has

A [P/ζ + ] ⊥ = A ⊥ P ⊥ /ζ -and A [N/ζ -] ⊥ = A ⊥ N ⊥ /ζ + .
The proof is a simple induction on A. We shall quite often deal with formulas A where pairwise distinct positive variables ζ + 1 , . . . , ζ + k are substituted by P 1 , . . . , P k and pairwise distinct negative variables ξ - 1 , . . . , ξ - n are substituted by N 1 , . . . , N n in parallel. Again the definition is a straightforward induction on A but the use of such parallel substitutions can lead to quite heavy notations. We use letters such as π, ρ to denote such type valuations π

= (N 1 /ξ - 1 , . . . , N n /ξ - n , P 1 /ζ + 1 , . . . , P k /ζ + k ) and write A [π] rather than A N 1 /ξ - 1 , . . . , N n /ξ - n , P 1 /ζ + 1 , . . . , P k /ζ k . We set π ⊥ = (N ⊥ 1 /ξ + 1 , . . . , N ⊥ n /ξ + n , P ⊥ 1 /ζ - 1 , . . . , P ⊥ k /ζ - k ). We use dom(π) for the domain of π which is the set {ζ + 1 , . . . , ζ + k , ξ - 1 , . . . , ξ - n }. We use π • (P/ζ + ) and π • (N/ζ -) to denote extensions of such valuations (assuming of course that ζ + , ζ -/ ∈ dom(π)).
We say that π is closed if all formulas P i , N j are closed.

The syntax of terms is given in Figure 2. There are three kinds of terms: (i) positive terms denoted p, q, . . . , (ii) negative terms denoted s, t, . . . and (iii) commands (or processes) denoted c, d, . . . . A negative context is a sequence N = (α 1 : N 1 , . . . , α n : N n ) and a positive context is a sequence P = (α 1 : N 1 , . . . , α n : N n , P ). We use Γ or N [, P ] for contexts which are negative or positive.

Typing rules are provided in the same figure. Notice that there are actually five kinds of typing judgments:

• Positive term in a negative context ⊢ N | p : P ;

• negative term in a positive context ⊢ N , P | t : N ;

• command in a positive context c ⊢ N , P ;

• negative term in a negative context ⊢ N | t : N ;

• and command in a negative context c ⊢ N .

(This distinction will be crucial when dealing with the semantics.) It is also important to observe that in all of these judgments, all formulas are closed. One major difference wrt. the λ-calculus is that we put the context on the right side of the ⊢ symbol, which means that in our setting the formulas of the context are negated wrt. what they would be in a λ-calculus with context on the left. This is why a name α is a positive term and appears with a negative type in the context (see e.g. rule (t-n)).

Remark 2.4

The expression • should be considered as a variable, the unique variable of negative type. Because of this uniqueness we do not need to mention it in the context and N , P should be read as N , • : P . p, q, . . . In other words, we can use freely weakening on negative formulas in the context. Assume that ⊢ N , P | s : N . We have ⊢ N , α : N | α : N ⊥ and hence s ⋆ α ⊢ N , α : N, P so that ⊢ N , α : N | κ.(s ⋆ α) : P , we shall often use this kind of change of active formula.

:= α | () | (p 1 , p 2 ) | in i (p) | κ.c | fd(p) | t ! s, t, . . . := • | ⟨⟩ | ⟨t 1 , t 2 ⟩ | κα.c | κ ⊥ .c | κ(α 1 , α 2 ).c | κ N,ζ α.(c ; s) | der(p) c, d, . . . := t ⋆ p (t-n) ⊢ N , α : P ⊥ | α : P (t-1) ⊢ N | () : 1 ⊢ N | p 1 : P 1 ⊢ N | p 2 : P 2 (t-⊗) ⊢ N | (p 1 , p 2 ) : P 1 ⊗ P 2 ⊢ N | p : P i i ∈ {1, 2} (t-⊕) ⊢ N | in i (p) : P 1 ⊕ P 2 c ⊢ N , P (t-κ) ⊢ N | κ.c : P ⊢ N | p : P [µζ.P/ζ + ] (t-µ) ⊢ N | fd(p) : µζ.P ⊢ N | t : N (t-!) ⊢ N | t ! : !N (t-•) ⊢ N , P | • : P ⊥ (t-⊤) ⊢ Γ | ⟨⟩ : ⊤ ⊢ Γ | t 1 : N 1 ⊢ Γ | t 2 : N 2 (t-&) ⊢ Γ | ⟨t 1 , t 2 ⟩ : N 1 & N 2 c ⊢ N , α : N [, P ] (t-κ) ⊢ N [, P ] | κα.c : N c ⊢ Γ (t-⊥) ⊢ Γ | κ ⊥ .c : ⊥ c ⊢ N , α 1 : N 1 , α 2 : N 2 [, P ] (t-`) ⊢ N [, P ] | κ(α 1 , α 2 ).c : N 1 `N2 c ⊢ N , P, α : R ⊥ P ⊥ /ζ - ⊢ N [, Q] | s : P ⊥ (t-ν) ⊢ N [, Q] | κ R ⊥ ,ζ α.(c ; s) : νζ.R ⊥ ⊢ N | p : P (t-?) ⊢ N | der(p) : ?P ⊢ N [, P ] | t : N ⊢ N | p : N ⊥ (t-cut) t ⋆ p ⊢ N [, P ]

Substitution of terms in terms

Substitution for a variable α and for • are defined in the obvious way.

Lemma 2.6 Assume that ⊢ N | p : P .

• If c ⊢ N , α : P ⊥ [, Q] then c [p/α] ⊢ N [, Q], • if ⊢ N , α : P ⊥ [, Q] | t : N then ⊢ N [, Q] | t [p/α] : N • and if ⊢ N , α : P ⊥ | q : Q then ⊢ N | q [p/α] : Q. Lemma 2.7 Assume that ⊢ N [, Q] | t : N . • If c ⊢ N , N ⊥ then c [t/•] ⊢ N [, Q] and • if ⊢ N , N ⊥ | s : M then ⊢ N [, Q] | s [t/•] : M .
As a particular case of (t-ν), if c ⊢ N , P, α :

R ⊥ P ⊥ /ζ -then ⊢ N , P | κ R ⊥ ,ζ α.(c ; •) : νζ.R ⊥ since ⊢ N , P | • : P ⊥ .
We use (t-ν 1 ) for this most important derived rule and use the notation

κ R ⊥ ,ζ α.c = κ R ⊥ ,ζ α.(c ; •).

Substitution of terms in formulas

Assume that ⊢ N , P | s : N , let Q be a positive formula and let ζ be a variable. Let also π be a type valuation such that ζ + , ζ -/ ∈ dom(π). Then we define two negative terms

Q [π, s/ζ + ] and Q [π, s/ζ -] in s ⋆ κ.c → c [s/•] κα.c ⋆ p → c [p/α] if p / ∈ κ ⟨s 1 , s 2 ⟩ ⋆ in i (p) → s i ⋆ p κ(α 1 , α 2 ).c ⋆ (p 1 , p 2 ) → c [p 1 /α 1 , p 2 /α 2 ] κ ⊥ .c ⋆ () → c der(p) ⋆ s ! → s ⋆ p κ R ⊥ ,ζ α.(c ; s) ⋆ fd(p) → (R κ R ⊥ ,ζ α.c/ζ + ⋆ p) [κα.(c [s/•])/•]
⊢ N , Q π, P/ζ + | Q π, s/ζ + : Q ⊥ π ⊥ , N/ζ - ⊢ N , Q π, N/ζ -| Q π, s/ζ -: Q ⊥ π ⊥ , P/ζ + .
In the first case (called positive substitution) we assume that fv(Q) ⊆ dom(π) ∪ {ζ + } and in the second case (negative substitution), that fv(Q) ⊆ dom(π) ∪ {ζ -}. The definition is by induction on Q. We give only the most interesting cases, the others are in Appendix 6.1. ▷ Assume that Q = µξ.R and let us set In the same induction we define completely similarly the negative substitution Q [π, s/ζ -].

R P = R [P/ζ + ] and R N = R N ⊥ /ζ + . Let ρ = π • (µξ.R P [π] /ξ + ). By inductive hypothesis we have defined t = R [ρ, s/ζ + ] with ⊢ N , R P [ρ] | t : R ⊥ N ρ ⊥ . We have ⊢ N , α : R ⊥ N ρ ⊥ | κ.(t ⋆ α) : R P [ρ]. Notice that, due to the definition of ρ, we have R S [ρ] = R S [π] [µξ.R P [π] /ξ + ] for S = P, N . It follows that ⊢ N , α : R ⊥ N ρ ⊥ | fd(κ.(t ⋆ α)) : µξ.R P [π]. Therefore (• ⋆ fd(κ.(t ⋆ α))) ⊢ N , µξ.R P [π] , α : R ⊥ N ρ ⊥ = (R N [π] [µξ.R P [π] /ξ + ]) ⊥ so we define (µξ.R) [π, s/ζ + ] as κ R ⊥ N [π ⊥ ],ζ α.(• ⋆ fd(κ.(t ⋆ α))) by (t-ν 1 ). ▷ Assume last that Q = !R ⊥ . By inductive hypothesis we have defined t = R π ⊥ , s/ζ -which satisfies ⊢ N , R π ⊥ , N/ζ -| t : R ⊥ [π, P/ζ + ]. It follows that ⊢ N , α : R ⊥ [π, P/ζ + ] | κ.(t ⋆ α) : R π ⊥ , N/ζ -

Reduction relation

We equip commands with a deterministic rewriting relation → specified in Figure 3. We use κ for the set of all positive terms of shape κ.c. The reduction of κ R ⊥ ,ζ α.(c ; s) ⋆ fd(p) deserves some typing. We must have

⊢ N | p : R [µζ.R/ζ + ] so that ⊢ N | fd(p) : µζ.R, c ⊢ N , P, α : R ⊥ P ⊥ /ζ -and ⊢ N [, Q] | s : P ⊥ so ⊢ N [, Q] | κ R ⊥ ,ζ α.(c ; s) : νζ.R ⊥ by (t-ν) and hence κ R ⊥ ,ζ α.(c ; s) ⋆ fd(p) ⊢ N [, Q]. We also have ⊢ N , P | κ R ⊥ ,ζ α.c : νζ.R ⊥ by (t-ν 1 ). By positive substitution we get ⊢ N , R [P/ζ + ] | R κ R ⊥ ,ζ α.c/ζ + : R ⊥ νζ.R ⊥ /ζ -and hence R κ R ⊥ ,ζ α.c/ζ + ⋆ p ⊢ N , R [P/ζ + ]. Observe last that ⊢ N , P | κα.c : R ⊥ P ⊥ /ζ -thus ⊢ N [, Q] | κα.(c [s/•]) : R ⊥ P ⊥ /ζ -so that (R κ Q ⊥ ,ζ α.c/ζ + ⋆ p) [κα.(c [s/•])/•] ⊢ N [, Q].
As a special case of this reduction rule we have the following one that we shall often use:

κ R ⊥ ,ζ α.c ⋆ fd(p) → (R κ R ⊥ ,ζ α.c/ζ + ⋆ p) [κα.c/•]. Theorem 2.8 If c ⊢ Γ and c → c ′ then c ′ ⊢ Γ.
The proof is an easy verification, using Lemmas 2.6 and 2.7. We use SN for the set of all c's which are normalizing for this reduction relation. Remark 2.9 Our choice of reducing the "critical pair" κα.c ⋆ κ.d to d [κα.c/•] and not to c [κ.d/α] will be essential in our proof of normalization. However this choice is not as critical as in classical systems such as system L [START_REF] Curien | The duality of computation[END_REF] or the λµ-calculus [START_REF] Parigot | Lambda-mu-calculus: An algorithmic interpretation of classical natural deduction[END_REF][START_REF] Ong | A curry-howard foundation for functional computation with control[END_REF]: our denotational semantics is compatible with both choices.

a, b, • • • := * | (j, ζ) | (a, b) | (i, a) | [a 1 , . . . , a n ] | σ(a) with j ∈ I and i ∈ {1, 2} sz( * ) = sz (j, ζ) = 1 sz(a, b) = sz(a) + sz(b) sz (i, a) = sz(σ(a)) = 1 + sz(a) sz([a 1 , . . . , a n ]) = 1 + n i=1 sz(a i ) (p-var) (j, ζ) : ζ (p-1) * : 1 a : P b : Q ∀ξ(rg ξ a ∩ rg ξ b = ∅) (p-⊗) (a, b) : P ⊗ Q (a i : N ⊥ ) n i=1 ∀ξ ∀i ̸ = i ′ (rg ξ a i ∩ rg ξ a i ′ = ∅) (p-!) [a 1 , • • • , a n ] : !N a : P i (p-⊕) (i, a) : P 1 ⊕ P 2 a : P [µζ.P/ζ + ] (p-µ) σ(a) : µζ.P k ∈ N (s-1) * 1 k[ * ] a i P i [a i 1 , . . . , a i n ] for i = 1, 2 (s-⊗) (a 1 , a 2 ) P 1 ⊗ P 2 [(a 1 1 , a 2 1 ), . . . (a 1 n , a 2 n )] k = n i=1 J i (a j : N ⊥ ) k j=1 (s-!) [a 1 , . . . , a k ] !N [[a j | j ∈ J i ] | i = 1, . . . , n] i ∈ {1, 2} a P i [a 1 , . . . , a n ] (s-⊕) (i, a) P 1 ⊕ P 2 [((i, a 1 ), . . . , (i, a n ))] a R [µζ.R/ζ + ] [a j | j ∈ J] (s-µ) σ(a) µζ.R [σ(a j ) | j ∈ J]
Lemma 2.10 If c ⊢ N , P , c → c ′ and ⊢ N | s : P ⊥ then c [s/•] → c ′ [s/•]. If c ⊢ N , α : P ⊥ [, Q], c → c ′ and ⊢ N | p : P with p / ∈ κ then c [p/α] → c ′ [p/α].
The proof is a simple inspection of the reduction rules.

The example of integers

We define a type of integers as nat = µζ.(1 ⊕ ζ + ). We set 0 = fd(in 1 ()) so that ⊢ N | 0 : nat and given a positive term p such that ⊢ N | p : nat we set suc p = fd(in 2 (p)) so that ⊢ N | suc p : nat. Let p, t and s be such that ⊢ N | p : P , ⊢ N , P | t :

P ⊥ and ⊢ N [, Q] | s : P ⊥ . Then ⊢ N , P | ⟨κ ⊥ .(• ⋆ p), t⟩ : ⊥ & nat ⊥ and we set it(p, t ; s) = κ ⊥&ζ -,ζ α.((⟨κ ⊥ .(• ⋆ p), t⟩ ⋆ α) ; s) so that ⊢ N [, Q] | it(p, t ; s) : nat ⊥ and it(p, t ; s)
should be understood as iterating the function t with p as initial value and s as continuation. Indeed one can check that (1

⊕ ζ + ) [u/ζ + ] = ⟨κα.(• ⋆ in 1 α), κα.(• ⋆ in 2 (κ.(u ⋆ α)))⟩ from which it follows by simple computations that it(p, t ; s) ⋆ 0 → * s ⋆ p and it(p, t ; s) ⋆ suc q → * it(p, t ; t [s/•]) ⋆ q.
3 An intersection typing system

The syntax of points

Let I be an infinite and countable set of indices (we can take I = N). The syntax of relational types or points is given in Figure 4, as well as the size sz(a) of a point, which is an integer ≥ 1. Given a point a and a literal ξ, we define a finite subset rg ξ (a) of I as follows:

rg ξ * = ∅, rg ξ (a, b) = rg ξ a ∪ rg ξ b, rg ξ (j, ξ) = {j}, rg ξ (j, ζ) = ∅ if ζ ̸ = ξ, rg ξ (i, a) = rg ξ a, rg ξ [a 1 , . . . , a n ] = n i=1 rg ξ a i and rg ξ σ(a) = rg ξ a.
We give a typing system for these points in Figure 4. Its main purpose is to enforce that, when a : P , given a literal ζ, the indices of I associated with ζ in a are pairwise distinct. Given a 0 : R, a literal ζ and a family of points -→ b = (b j ) j∈rg ζ a 0 such that b j : P for all j and such that for any literal ξ the sets rg ξ b j are pairwise disjoint and disjoint from rg ξ a 0 (when these disjointness conditions hold we say that the pair (a 0 , -→ b ) is adapted ) then we define in the obvious way the point a 0 {b j /(j, ζ)} j∈J for J = rg ζ a 0 such that

(a i P i [ ]) i∈n\{j} (i-n) ⊢ Φ | α j : a j : P j (a i P i [ ]) n i=1 (i-1) ⊢ Φ | () : * : 1 (⊢ (α i : a j i : P ⊥ i ) n i=1 | p j : b j : Q j ) j=1,2 (a i P i [a 1 i , a 2 i ]) n i=1 (i-⊗) ⊢ Φ | (p 1 , p 2 ) : (b 1 , b 2 ) : Q 1 ⊗ Q 2 ⊢ Φ | p : a : Q i (i-⊕) ⊢ Φ | in i (p) : (i, a) : Q 1 ⊕ Q 2 c ⊢ Φ, a : P (i-κ) ⊢ Φ | κ.c : a : P ⊢ Φ | p : a : P [µζ.P/ζ + ] (i-µ) ⊢ Φ | fd(p) : σ(a) : µζ.P (⊢ (α i : a j i : P ⊥ i ) n i=1 | s : b j : N ) j∈J (a i P i [a j i | j ∈ J]) n i=1 (i-!) ⊢ Φ | s ! : [b j | j ∈ J] : !N (a i P i [ ]) n i=1 (i-•) ⊢ Φ, a : P | • : a : P ⊥ c ⊢ Φ, α : a : N [, b : P ] (i-κ) ⊢ Φ[, b : P ] | κα.c : a : N c ⊢ Φ, α 1 : a 1 : N 1 , α 2 : a 2 : N 1 [, b : P ] (i-`) ⊢ Φ[, b : P ] | κ(α 1 , α 2 ).c : (a 1 , a 2 ) : N 1 `N2 c ⊢ Φ[, a : P ] (i-⊥) ⊢ Φ[, a : P ] | κ ⊥ .c : * : ⊥ ⊢ Φ[, a : P ] | s i : b : N i ⊢ N [, P ] | s 3-i : N 3-i (i-&) ⊢ Φ[, a : P ] | ⟨s 1 , s 2 ⟩ : (i, b) : N 1 & N 2 ⊢ Φ | p : a : P (i-?) ⊢ Φ | der(p) : [a] : ?P ⊢ (α i : a 1 i : P ⊥ i )[, a : P ] | s : b : P ⊥ ⊢ (α i : a 2 i :) | p : b : P (a i P i [a 1 i , a 2 i ]) n i=1 (i-cut) (t ⋆ p) ⊢ Φ[, a : P ]
rg ξ a 0 {b j /(j, ζ)} j∈J = rg ξ a 0 ⊎ j∈rg ζ a 0 rg ξ b j . (1)
Crucially, this point substitution is in some sense reversible. Given a closed positive type P , we define a binary relation P between points a and multisets of points [a 1 , . . . , a n ]) where a, a 1 , . . . , a n : P . The definition is provided as a deduction system in Figure 4. Notice that in each of the deduction rules the sum of the sizes of the points occurring on the left in the premises is strictly smaller than the size of the point occurring on the left in the conclusion. So the size of such a deduction tree is upper-bounded by the size of the point occurring on the left in its conclusion.

The point typing system

A negative point typing context is a sequence Φ = (α 1 : a 1 : N 1 , . . . , α k : a k : N k ) where the α i 's are pairwise distinct and a i : N ⊥ i for each i. A positive point typing context is a sequence Φ, a : P with a : P . In these rules we use Φ to denote the context (α i : a i : P ⊥ i ) n i=1 and N for the ordinary typing context (α i :

P ⊥ i ) n i=1 .
All rules but (i-ν) are given in Figure 5. Notice that there are two instances of the rules (i-⊕) and (i-&), one for i = 1 and one for i = 2. We give now the lacking (i-ν) inference rule: if h : Q, d : R, (b l : P ) l∈L where L = rg ζ d, and

• ⊢ (α i : a ′′ i : P ⊥ i ) n i=1 [, h : Q] | s : b : P ⊥ • c ⊢ (α i : a ′ i : P ⊥ i ) n i=1 , b : P, α : d{b l /(l, ζ)} l∈L : R ⊥ P ⊥ /ζ - • (⊢ (α i : a l i : P ⊥ i ) n i=1 , b l : P | κ R ⊥ ,ζ α.c : f l : νζ.R ⊥ ) l∈L 8 • a i P i [a ′ i , a ′′ i ] + [a l i | l ∈ L] for i = 1, . . . , n then ⊢ Φ[, h : Q] | κ R ⊥ ,ζ α.(c ; s) : σ(d){f l /(l, ζ)} l∈L : νζ.R ⊥ .
Upon taking s = • we obtain the following derived rule (i-ν 1 ) (with the same notations as above). If

• c ⊢ (α i : a ′ i : P ⊥ i ) n i=1 , b : P, α : d{b l /(l, ζ)} l∈L : R ⊥ P ⊥ /ζ - • (⊢ (α i : a l i : P ⊥ i ) n i=1 , b l : P | κ R ⊥ ,ζ α.c : f l : νζ.R ⊥ ) l∈L • a i P i [a ′ i ] + [a l i | l ∈ L] for i = 1, . . . , n then ⊢ Φ, b : P | κ R ⊥ ,ζ α.c : σ(d){f l /(l, ζ)} l∈L : νζ.R ⊥ .

Interpretation of points

Given a set P of positive terms p such that ⊢| p : P , we set P • = {c | c ⊢ P and ∃p ∈ (P \ κ) c → * • ⋆ p} and P κ = P ∪ {κ.c | c ∈ P • } so that any p ∈ P κ satisfies ⊢| p : P . We set ' = SN. Given a : P we define '(a : P ) = |a| P

• and we set |a| P = ∥a∥ κ P where

• ∥ * ∥ 1 = {()} • ∥(a 1 , a 2 )∥ P 1 ⊗P 2 = {(p 1 , p 2 ) | p i ∈ |a i | P i for i = 1, 2} • ∥(i, a)∥ P 1 ⊕P 2 = {in i (p) | p ∈ |a| P i } for i = 1, 2 • ∥[a j | j ∈ J]∥ !N = {t ! | ∀j ∈ J ∀p ∈ |a j | N ⊥ t ⋆ p ∈ '} -notice that in that formula ⊢| t : N . • ∥σ(a)∥ µζ.P = {fd(p) | p ∈ |a| P [µζ.P/ζ + ] }.
Notice that ∥a∥ P = |a| P \ κ since ∥a∥ P ∩ κ = ∅. As an auxiliary notion, given a : P and b : N ⊥ we set |b| N (a : P ) = {s | ⊢ P | s : N and ∀p ∈ |b| N ⊥ s ⋆ p ∈ '(a : P )}. We will also use |b| N for the set of s such that ⊢| s : N and ∀p ∈ |b|

N ⊥ s ⋆ p ∈ '. Lemma 3.2 Let a : P , b : Q and s be such that ⊢ P | s : Q ⊥ . If ∀p ∈ ∥b∥ Q s ⋆ p ∈ '(a : P ) then s ∈ |b| Q ⊥ (a : P ).
: P ) k∈K such that a P [c k | k ∈ K] and c k P [b j | j ∈ J k ] for each k ∈ K.
Proof. Straightforward induction on the size of a.

2

Upon taking K = J = ∅ this implies in particular ∃e : P e P [ ]. Such an e is called a coneutral point of P . By Lemma 3.4, if a P [e, b] and e is coneutral then a = b, and if a : P there is a coneutral e such that a P [e, a] (which depends generally on a). Coneutral points are generally not unique: for instance in 1 ⊕ 1, both (1, * ) and (2, * ) are coneutral. Lemma 3.5 Let Q be a positive formula, η a literal, π a closed type valuation such that all free type variables of Q, but possibly η + , η -, are in dom(π).

Let d : Q [π], assume that ⊢ (α i : a j i : N i ) n i=1 , b j : P | s : c j : N for each j ∈ rg η d. If (a i : N ⊥ i ) n i=1 are such that for all i ∈ n one has a i N ⊥ i [a j i | j ∈ rg η d] then ⊢ (α i : a i : N i ), d{b j /(j, η)} j∈rg η d : Q [π, P/η + ] | Q [π, s/η + ] : d{c j /(j, η)} j∈rg η d : Q ⊥ π ⊥ , N/η -and ⊢ (α i : a i : N i ), d{c j /(j, η)} j∈rg η d : Q [π, N/η -] | Q [π, s/η -] : d{b j /(j, η)} j∈rg η d : Q ⊥ π ⊥ , P/η + .
Lemma 3.6 Let Q be a positive formula, η a literal, π a closed type valuation such that all free type variables of Q, but possibly η + , η -, are in dom(π) and let d :

Q [π]. If s ∈ |c j | N (b j : P ) for all j ∈ J = rg η d then Q [π, s/η + ] ∈ |d( - → c )| Q ⊥ [π ⊥ ,N/η -] (d( - → b ) : Q [π, P/η + ]) where d( - → b ) = d{b j /(j, η)} j∈rg η d and similarly for d( - → c ). And we have Q [π, s/η -] ∈ |d( - → b )| Q ⊥ [π ⊥ ,P/η + ] (d( - → c ) : Q [π, N/η -]).

Example: the integers

We continue the example initiated in Section 2.4. There is a bijection from N to the points a : nat which maps 0 to 0 = σ(1, * ) and n + 1 to n + 1 = σ(2, n). With these notations the following rules are derivable in the point typing system.

• If (a i N i [ ]) n i=1 then ⊢ (α i : a i : P i ) n i=1 | 0 : 0 : nat. • If ⊢ Φ | p : k : nat then ⊢ Φ | suc p : k + 1 : nat. • If ⊢ (α i : a 1 i : N i ) n i=1 | p : a : P , ⊢ (α i : a 2 i : N i ) n i=1 [, b : Q] | a : s : P ⊥ and (a i N ⊥ i [a 1 i , a 2 i ]) n i=1 then ⊢ (α i : a i : N i ) n i=1 [, b : Q] | it(p, t ; s) : 0 : nat ⊥ . • If ⊢ (α i : a 1 i : N i ) n i=1 [, b : Q] | s : a : P ⊥ , ⊢ (α i : a 2 i : N i ) n i=1 , a : P | t : a ′ : P ⊥ , ⊢ (α i : a 3 i : N i ) n i=1 , a ′ : P | it(p, t ; •) : n : nat ⊥ and (a i N ⊥ i [a 1 i , a 2 i , a 3 i ]) n i=1 then ⊢ (α i : a i : N i ) n i=1 [, b : Q] | it(p, t ; s) : n + 1 : nat ⊥ .

Interpretation Theorem

Using the previous lemmas it is not very hard to relate the point typing system with normalization.

Theorem 3.7 Let Φ = (α i : a i : P ⊥ i ) n i=1 be a point context and let a : P , let

p i ∈ |a i | P i for i = 1, . . . , n. (i) If c ⊢ Φ then c[p i /α i ] n i=1 ∈ '. (ii) If c ⊢ Φ, a : P then c[p i /α i ] n i=1 ∈ '(a : P ). (iii) If ⊢ Φ | s : b : N then s[p i /α i ] n i=1 ∈ |b| N . (iv) If ⊢ Φ, a : P | t : b : N then t[p i /α i ] n i=1 ∈ |b| N (a : P ). (v) If ⊢ Φ | p : a : P then p[p i /α i ] n i=1 ∈ |a| P .

Application: a normalization property

Anticipating on Section 5, we explain now how one can use Theorem 3.7, combined with the Nuts denotational semantics of Section 5.1, to prove "normalization" properties for κµLLP commands. More precisely we show that the reduction of programs of type integer in κµLLP terminates but of course many more applications are possible. We explain first why the type of such a program should be ?nat and not nat.

Imagine that we want to encode in κµLLP a typed λ-calculus extended with primitive recursion on some data types, in the spirit of Gödel's T; we shall simply call this system T. This calculus will have two kinds of types: data-types which are associated with positive formulas of κµLLP and function types σ ⇒ τ . In T there will be at least a data-type of integers ι associated with nat and possibly other ones, for instance a type of binary trees with leaves labeled by natural numbers associated with µζ.(nat

⊕ (ζ ⊗ ζ)).
We would like to use the Girard encoding (σ ⇒ τ ) -= !σ -⊸ τ -where as usual A ⊸ B = A ⊥ `B. In other words (σ ⇒ τ ) -= ?(σ -) ⊥ `τ -. The polarity constraints of κµLLP require σ -to be negative, this prevents us from setting simply ι -= nat since nat is positive. For benefiting from the structural rules available for free on all negative formulas in κµLLP we introduce also a positive translation defined by ι + = nat (and similarly for all data-types of T) and σ + = !σ -if σ is not a data-type and then the negative translation can be defined by ι -= ?nat (and similarly for all data-types) and (σ ⇒ τ

) -= (σ + ) ⊥ `τ -. For instance ((ι ⇒ ι) ⇒ ι) -= ?(nat ⊗ !nat ⊥ ) `?nat.
A closed term of type ι of T will therefore be translated into a κµLLP negative term t such that ⊢| t : ?nat and we can form c = t ⋆ α. Now we explain how we can extract effectively a value ∈ N from such a c which satisfies c ⊢ ?nat.

First we define two mutually recursive partial functions val (on terms p such that ⊢| p : nat) and val ⊕ (on terms q such that ⊢| q : 1 ⊕ nat) with values in N. If ⊢| p : nat then

• if p = fd(q) then we have ⊢| q : 1 ⊕ nat and we take val p = val ⊕ q;

• else if p = κ.c then if c → * • ⋆ p 0 ∈ ' (that is p 0 / ∈ κ) then ⊢| p 0 : nat and we take val p = val p 0 .

And if ⊢| q : 1 ⊕ nat then

• if q = in 1 r then if r = () or if r = κ.c and c → * • ⋆ (), then val ⊕ q = 0;

• if q = in 2 p ′ then we have ⊢| p ′ : nat and we take val ⊕ q = 1 + val p ′ ;

• if q = κ.c and c → * •⋆q 0 ∈ ' (that is q 0 / ∈ κ) then we have ⊢| q 0 : 1⊕nat and we take val ⊕ q = val ⊕ q 0 . Lemma 3.8 If ⊢| p : nat and p ∈ |n| nat for some n ∈ N then val p is defined and has n as value.

The proof is a straightforward application of the definition of |n| nat . This lemma means that when we know that p ∈ |n| nat for some n we can extract algorithmically the value of n from p.

Then we extend κµLLP with a constant • which is a new command, typed by • ⊢ N where N is an arbitrary negative context9 . We also extend the point typing system with the rule • ⊢ (α i : a i : N i ) n i=1 under the proviso that a i N ⊥ i [ ] for all i ∈ n. The benefit of this extension is that now ' contains closed commands.

We have ⊢| By the results of Section 4 and 5 we know that the interpretation of c ?nat in Rel belongs to T ( ?nat ) where ?nat is the interpretation of ?nat in Nuts (that is c ?nat is total in the interpretation of that type). As explained in Section 5.4 nat ⊥ = (N, {N}) and hence T ( !nat ⊥ ) = {M fin (N)}. Therefore c ?nat ∩ M fin (N) ̸ = ∅ that is c ?nat ̸ = ∅ so by Theorem 5.13 there is m : ?nat such that c ⊢ α : m : ?nat.

Assume c ⊢ ?nat and c does not contain •. By the considerations above the integer n = val α c is well defined (and we have given an algorithm to compute it consisting in executing κµLLP commands). Moreover c ⊢ α : m 1 + [n] : ?nat for some m 1 : ?nat. Using the model RelW introduced in [START_REF] Amini | On classical pcf, linear logic and the MIX rule[END_REF] (it is a variation on the relational model where each object is a set E equipped with a function E → Z) it is possible to prove that, because c does not contain •, one has m 1 = [ ]. So we actually have c ⊢ α : [n] : ?nat, that is, the value obtained by execution coincides with the value provided by the semantics.

Categorical semantic of κµLLP

We use the following conventions: The identity morphism on an object A is written as A, and we very often simply write Id for the sake of readability, when the object can easily be retrieved from the context. Alg A (F) (resp. Coalg A (F)) is the category of algebra (resp. co-algbera) of the endofunctor F on A. Other notations are based on [START_REF] Ehrhard | Categorical models of linear logic with fixed points of formulas[END_REF].

Let (L, -→ L = (L n ) n∈N ) be a categorical model of µLL in the sense of [START_REF] Ehrhard | Categorical models of linear logic with fixed points of formulas[END_REF], Definition 7. We recall that L is a categorical model of LL and that the elements F of L n are strong functors L n → L, that is F is a pair (F, F) where F : L n → L is a functor, and

F A, -→ B ∈ L(!A ⊗ F( - → B ), F(!A ⊗ - → B )
) is a natural transformation, called strength, satisfying monoidality and compatibility with dig, see [START_REF] Ehrhard | Categorical models of linear logic with fixed points of formulas[END_REF] Figure 1. Some additional closedness properties must be satisfied by the L n 's, see [START_REF] Ehrhard | Categorical models of linear logic with fixed points of formulas[END_REF], Definition 7. Definition 4.1 A (n, p)-positive functor P is a pair (P, P) where P ∈ L n+p and P-

→ A , -→ B ∈ L(P( - → A , -→ !B), !P( - → A , - → B )
) is a natural transformation called the distributive law of P. It is assumed moreover that the diagrams of Figure 6 commute, expressing the compatibility of P with der, dig, and P.

P(

- → A , -→ !B) !P(A, B) P( - → A , - → B ) P-→ A , - → B P( -→ A , der-→ B ) der P(A,B) P( - → A , -→ !B) !P( - → A , - → B ) P( - → A , !! - → B ) !P( - → A , -→ !B) !!P( - → A , - → B ) P-→ A , - → B P( -→ A , dig-→ B ) dig P( - → A , - → B ) P-→ A , -→ !B ! P-→ A , - → B !!C ⊗ P( - → A , -→ !B) P(!!C ⊗ - → A , !!C ⊗ -→ !B) !!C ⊗ !P( - → A , - → B ) P(!C ⊗ - → A , !(!C ⊗ - → B )) !(!C ⊗ P( - → A , - → B )) !P(!C ⊗ - → A , !C ⊗ - → B ) P !C,( - → A , - → B ) !!C⊗ P-→ A , - → B P(der !C ⊗ -→ A , µ 2 !C, - → B ) µ 2 !C,P( - → A , - → B ) P !C⊗ - → A ,!C⊗ - → B ! P C,( - → A , - → B )
Fig. 6. Compatibility of P with der, dig, and P Lemma 4.2 Any (n, p)-positive functor P induces a functor

P + : L n × (L ! ) p → L ! .
As a consequence of Lemma 4.2, a (0, 0)-positive functor P induces an object of L ! , and and in that case P = h P .

We write X, Y, • • • for objects of the category L ! , and A, B, • • • for those of L. We recall that L[Z] is the Kleisli category of the comonad (fc Z , W Z , C Z ) where fc Z : L → L is the functor which maps an object A to Z ⊗A and a morphism f to Z ⊗f , and W Z , C Z are weakening and contraction morphism respectively.

Given a strong functor F ∈ L k and object Z = (Z, h Z ) ∈ L ! , one can extend F to a functor F[Z] :

L[Z] k → L[Z]. On objects, one sets F[Z]( - → A ) = F( - → A ). And given a morphism - → f ∈ L[Z] k ( -→ A 1 , -→ A 2 ), we define F[Z]( - → f ) as (F( - → f )) • (F(der Z ⊗ -→ A 1 ) • (( F Z, -→ A 1 ) • (h Z ⊗ F(A 1 ))):
Lemma 4.3 Let P = (P, P) be a positive functor and f ∈ L ! (Z ⊗ X, Y ). If P is a (n, p + 1)-positive functor, then

P[Z]( - → Id , - → Id , f ) ∈ L ! (Z ⊗ P + ( - → A , -→ Y 1 , X), P + ( - → A , -→ Y 1 , Y )).
And if P is a (n + 1, p)-positive functor, then [START_REF] Ehrhard | Categorical models of linear logic with fixed points of formulas[END_REF]. The distributive law is defined as follows, and satisfies commutations of Fig. 6.

P[Z](f ⊥ , - → Id , - → Id ) ∈ L ! (Z ⊗ P + ((Y ) ⊥ , - → A , -→ Y 1 ), P + ((X) ⊥ , - → A , -→ Y 1 )).
F 1 , • • • , F n in L k , and (n ′ , p ′ )-positive functors Q 1 , • • • , Q p such that n ′ + p ′ = k, one can define a (n ′ , p ′ )-positive functor R = P • (F 1 , • • • , F n , Q 1 , • • • , Q p ): the strong functor R is just P • (F 1 , • • • , F n , Q 1 , • • • , Q p ) as

R(

- → A , -→ !B) = P((F i ( - → A , -→ !B)) n i=1 , (Q i ( - → A , -→ !B)) p i=1 ) P((F i ( - → A , - → B )) n i=1 , (!Q i ( - → A , - → B )) p i=1 ) !P((F i ( - → A , - → B )) n i=1 , (Q i ( - → A , - → B )) p i=1 ) = !R( - → A , - → B ) P((F i ( -→ A , der-→ B )) n i=1 , ( Q i ) p i=n+1 ) P (F i ( - → A , - → B )) n i=1 ,Q i ( - → A , - → B )
The bifunctor ⊗ can be turned into a (0, 2)-positive functor: the distributive law is µ 2 A,B ∈ L(!A ⊗ !B, !(A ⊗ B)), and it satisfies commutations of Fig. 6.

The bifunctor ⊕ can be turned into a (0, 2)-positive functor: the distributive law is [π 1 , π 2 ] ∈ L(!A ⊕ !B, !(A ⊕ B)), and it satisfies commutations of Fig. 6.

The functor ! is a (1, 0)-positive functor: the distributive law is dig A ∈ L(!A, !!A), and satisfies commutations of Fig. 6.

Let P be a (n, p)-positive functor. One can define the De Morgan dual of it, denoted as P ⊥ , as a strong functor: P ⊥ = P ⊥ and the last term is just P ⊥ .

Fixpoint of positive functors

Let P be a (n, p + 1)-positive functor. We must define a (n, p)-positive functor µP. We set µP = µP.

The distr. law µP must be a natural transf. µP-

→ A , -→ B ∈ L(µP( - → A , -→ !B), !µP( - → A , - → B )). To define it, we first notice that (!µP( - → A , - → B ), P-→ A ,( -→ B ,µP( -→ A , -→ B )) ) is an object of Coalg L (P-→ A , -→ B ). So, by the universal property of µP( - → A , -→ !B), there is a unique morphism µP-→ A , -→
B such that the following diagram commutes:

P( - → A , -→ !B, µP( - → A , -→ !B)) P( - → A , -→ !B, !µP( - → A , - → B )) µP( - → A , -→ !B) !µP( - → A , - → B ) !P( - → A , - → B , µP( - → A , - → B )) P( -→ A , -→ !B , µP-→ A , - → B ) ≃ P-→ A ,( - → B , µP( - → A , - → B )) µP-→ A , - → B ≃ Lemma 4.4 Given a strong functor F ∈ L k+1 and an object Z = (Z, h Z ) in L ! , there is a unique functor µ(F[Z]) : L[Z] k → L[Z] such that µ(F[Z])( - → A ) is the initial object of the category Alg L[Z] (F-→ A ) for any object - → A ∈ L k , and µ(F[Z])( - → f ) is the unique morphism satisfying commutation of the following diagram for any - → f ∈ L[Z] k ( -→ B 1 , -→ B 2 ): µ(F[Z])( -→ B 1 ) µ(F[Z])( -→ B 2 ) F-→ B 1 (µ(F[Z])( -→ B 1 )) F-→ B 1 (µ(F[Z])( -→ B 2 )) F-→ B 2 (µ(F[Z])( -→ B 2 )) µ(F[Z])( -→ f ) F-→ B 1 (µ(F[Z])( -→ f )) ≃ F( -→ f , Id) ≃ where the composition is considered in category L[Z]. Lemma 4.5 Given a morphism g ∈ L[Z](Q(Y ), Y ) where Q is a (0, 1)-positive functor, there is a unique morphism g ∈ L[Z](µQ, Y ) such that g ∈ Alg L[Z] (Q[Z])(µQ, Y ).
Lemma 4.6 Given a (0, 1)-positive functor Q, and a morphism g

∈ L ! (Z ⊗ Q + (Y ), Y ), then there is a unique morphism g ∈ L ! (Z ⊗ (µQ) + , Y ) such that g ∈ Alg L[Z] (Q[Z])(µQ, Y ).

Interpretation of proofs and formulas

Definition 4.7 ( -→ ζ -, -→ ξ + ) = (ζ - 1 , . . . , ζ - n , ξ + 1 , . . . , ξ + p ) is adapted to P (resp. N ) if ( -→ ζ -, -→ ξ +
) is repetition-free and all the free variables of P (resp. N ) appear in that list.

Given a positive formula P with an adapted list (

-→ ζ -, -→ ξ + ) = (ζ - 1 , . . . , ζ - n , ξ + 1 , . . . , ξ + p ), its interpreted is a (n, p)-positive functor P -→ ζ -, -→ ξ + .
If n = p = 0 we simply write P . For a negative formula N with an adapted list (

-→ ζ -, -→ ξ + ) = (ζ - 1 , . . . , ζ - n , ξ + 1 , . . . , ξ + p ), we define its inter- pretation N -→ ζ -, -→ ξ + as ( N ⊥ -→ ζ -, -→ ξ + ) ⊥ . One can define P -→ ζ -, -→
ξ + in the obvious way by induction on formulas and using the construction in the section 4.1:

P 1 ⊗ P 2 -→ ζ -, -→ ξ + = ⊗ • ( P 1 -→ ζ -, -→ ξ + , P 2 -→ ζ -, -→ ξ + ), P 1 ⊕ P 2 -→ ζ -, -→ ξ + = ⊕ • ( P 1 -→ ζ -, -→ ξ + , P 2 -→ ζ -, -→ ξ + ), !N -→ ζ -, -→ ξ + = ! • ( N ⊥ -→ ζ -, -→ ξ + ) ⊥ , and µZ.P -→ ζ -, -→ ξ + = µ( P -→ ζ -, -→ ξ + ,Z
).

Lemma 4.8 Let A be a formula and π be a type valuation

N 1 /ξ - 1 , . . . , N n /ξ - n , P 1 /ζ + 1 , . . . , P k /ζ + k . Then A [π] = A -→ ζ + , -→ ξ + • ( N 1 , • • • , N n , P 1 , • • • , P k ).
We define the interpretation of terms, as usual, by induction on proofs based on Figure 2. As we have different judgments, we must have different ways of interpreting terms which is explained as follows:

• if ⊢ N | p : P , then p + N ∈ L ! ( N ⊥ , P ); • if ⊢ N , P | t : N , then t + N ,P ∈ L ! ( N ⊥ ⊗ N ⊥ , P ); • if c ⊢ N , P , then c + N ,P ∈ L ! ( N ⊥ , P ); • if ⊢ N | t : N , then t N ∈ L( N ⊥ ⊗ N ⊥ , ⊥); • if c ⊢ N , then c N ∈ L( N ⊥ , ⊥).
We only give the details of the interpretation of κ N,ζ α.(c ; s), and the other cases are defined in 6. [START_REF]Execution time of λ-terms via denotational semantics and intersection types[END_REF]

[P ⊥ /ζ -] ∈ L ! ( N ⊥ ⊗ µ N ⊥ ζ + , P ).
And by the interpretation of formula, we know that µζ

+ .N ⊥ = µ N ⊥ ζ + . So, we have c + N ,P,N [P ⊥ /ζ -] ∈ L ! ( N ⊥ ⊗ µζ + .N ⊥ , P ). Notice that c + N ,P,N [P ⊥ /ζ -]
is a unique morphism by lemma 4.6, so, we just take the following morphism of category L ! as κ N,ζ α.(c ; s) + N ,Q :

N ⊥ ⊗ µζ + .N ⊥ N ⊥ ⊗ N ⊥ ⊗ µζ + .N ⊥ Q N ⊥ ⊗ P C N ⊥ ⊗Id Id ⊗ c + N ,P,N [P ⊥ /ζ -] s + N ,Q

Soundness

We first state the substitution lemmas (Lemmas 4.9, 4.10 & 4.11).

Lemma 4.9 Assume that ⊢ N | p : P .

If c ⊢ N , α : P ⊥ , then

N ⊥ N ⊥ ⊗ N ⊥ ⊥ N ⊥ ⊗ P C N ⊥ c[p/α] N Id ⊗ p + N c N ,P ⊥ If c ⊢ N , α : P ⊥ , Q, then N ⊥ N ⊥ ⊗ N ⊥ Q N ⊥ ⊗ P C N ⊥ c[p/α] + N Id ⊗ p + N c + N ,P ⊥ ,Q If ⊢ N , α : P ⊥ | t : N , then N ⊥ ⊗ N ⊥ N ⊥ ⊗ N ⊥ ⊗ N ⊥ ⊥ N ⊥ ⊗ P ⊗ N ⊥ C N ⊥ ⊗Id t[p/α] N Id ⊗ p + N ⊗Id cur -1 ( t N ,P ) If ⊢ N , α : P ⊥ , Q | t : N , then N ⊥ ⊗ N ⊥ N ⊥ ⊗ N ⊥ ⊗ N ⊥ Q N ⊥ ⊗ P ⊗ N ⊥ C N ⊥ ⊗Id t[p/α] + N Id ⊗ p + N ⊗Id t + N ,P ⊥ ,Q if ⊢ N , α : P ⊥ | q : Q, then N ⊥ N ⊥ ⊗ N ⊥ Q N ⊥ ⊗ P C N ⊥ q[p/α] + N Id ⊗ p + N q + N ,P ⊥ Lemma 4.10 Assume that ⊢ N , Q | t : N . If c ⊢ N , N ⊥ , then N ⊥ N ⊥ ⊗ N ⊥ Q N ⊥ ⊗ N ⊥ C N ⊥ c[t/•] + N ,Q Id ⊗ c + N ,N ⊥ t + N ,Q If ⊢ N , N ⊥ | s : M , then N ⊥ ⊗ M ⊥ N ⊥ ⊗ N ⊥ ⊗ M ⊥ Q N ⊥ ⊗ N ⊥ C N ⊥ ⊗Id s[t/•] + N ,Q Id ⊗ s + N ,N ⊥ t + N ,Q Lemma 4.11 Assume that ⊢ N | t : N . If c ⊢ N , N ⊥ , then N ⊥ N ⊥ ⊗ N ⊥ ⊥ N ⊥ ⊗ N ⊥ C N ⊥ c[t/•] N Id ⊗ c + N ,N ⊥ t N If ⊢ N , N ⊥ | s : M , then N ⊥ ⊗ M ⊥ N ⊥ ⊗ N ⊥ ⊗ M ⊥ ⊥ N ⊥ ⊗ N ⊥ C N ⊥ ⊗Id s[t/•] N Id ⊗ s + N ,N ⊥ t N
The following lemma relates syntactic functoriality (section 2.2) and the semantical one (Lemma 4.3).

Lemma 4.12 Assume that ⊢ N , P | s : N , let Q be a positive formula and let ζ be a variable. Let also π be a type valuation such that

ζ + , ζ -/ ∈ dom(π). Then Q [π, s/ζ + ] + N ,Q[π,P/ζ + ] = Q dom(π),ζ + [ N ⊥ ]( - → Id , - → Id , s + N ,P ) Q [π, s/ζ -] + N ,Q[π,N/ζ -] = Q dom(π),ζ -[ N ⊥ ](( s + N ,P ) ⊥ , - → Id , - → Id )
As a direct conclusion of Lemma 4.3 and Lemma 4.12, we can have the following corollary:

Corollary 4.13 Assume that ⊢ N , P | s : N , let Q be a positive formula and let ζ be a variable. Let also π be a type valuation such that Proof. By induction on the length of reductions from c to d, and using Lemma 4.14. 2

ζ + , ζ -/ ∈ dom(π). Then Q [π, s/ζ + ] + N ,Q[π,P/ζ + ] ∈ L ! ( N ⊥ ⊗ Q dom(π),ζ + + ( --→ N , --→ P , N ⊥ ), Q dom(π),ζ + + ( --→ N , --→ P , P )) Q [π, s/ζ -] + N ,Q[π,N/ζ -] ∈ L ! ( N ⊥ ⊗ Q dom(π),ζ + + ( P ⊥ , --→ N , --→ P ), Q dom(π),ζ + + ( N ⊥ ⊥ , --→ N , --→ P ))

Two concrete models of κµLLP

We recall briefly the main definitions concerning the models Rel and Nuts, more details can be found in [START_REF] Ehrhard | Categorical models of linear logic with fixed points of formulas[END_REF].

Sets and relations as a model of κµLLP

The category Rel has sets as objects, and given sets E and F , Rel(E, F ) = P(E × F ). Identity is the diagonal relation and composition is the usual composition of relations, denoted by simple juxtaposition.

If t ∈ Rel(E, F ) and u ⊆ E then t • u = {b ∈ F | ∃a ∈ u (a, b) ∈ t}. This category is a well-known model of LL in which 1 = ⊥ = { * }, E ⊗ F = (E ⊸ F ) = E `F = E × F so that (E) ⊥ = E. As to the additives, 0 = ⊤ = ∅ and &i∈I E i = ⊕ i∈I E i = ∪ i∈I {i} × E i .
The exponentials are given by !E = ?E = M fin (E) (finite multisets of elements of E). For the additives and multiplicatives, the operations on morphisms are defined in the obvious way. Let us be more specific about the exponentials. Given

s ∈ Rel(E, F ), !s ∈ Rel(!E, !F ) is !s = {([a 1 , . . . , a n ], [b 1 , . . . , b n ]) | ∀i (a i , b i ) ∈ s}, der(E) ∈ Rel(!E, E) is given by der(E) = {([a], a) | a ∈ E} and dig E ∈ Rel(!E, !!E) is given by dig E = {(m 1 + • • • + m n , [m 1 , . . . , m n ]) | ∀i m i ∈ M fin (E)}. Last m 0 ∈ Rel(1, !⊤) is m 0 = {( * , [])} and

Rel and the point typing system

In Section 3 we have introduced a point typing system. The points of this typing system are essentially the same thing as points of the relational model, the only difference being that a point a : P contains the σb construct at places corresponding to occurrences of µ or ν type constructs in P . It is easy to see that there is a bijective correspondence between the a : P and the a ′ ∈ P in Rel. To simplify notations we consider this correspondence as the identity function. Lemma 5.12 Let P be a closed positive formula. Then a P

[a 1 , • • • , a n ] iff (a, [a 1 , • • • , a n ]) ∈ h P .
Theorem 5.13 Let Φ = (α 1 : a 1 : N 1 , . . . , α k : a k : N k ) be a negative point typing context and let N = (α 1 : N 1 , . . . , α n : N n ) . Then

• (a 1 , • • • , a n , b) ∈ t Rel N iff ⊢ Φ | t : b : N • (a 1 , • • • , a n , c, b) ∈ t Rel N ,P iff ⊢ Φ, c : P | t : b : N • (a 1 , • • • , a n , b) ∈ q Rel N iff ⊢ Φ | q : b : P • (a 1 , • • • , a n ) ∈ c Rel N iff c ⊢ Φ • (a 1 , • • • , a n , b) ∈ c Rel N ,P iff c ⊢ Φ, b : P
The proof of Theorem 5.13 is a simple verification, and it uses Lemma 5.12.

Examples of nat

As we can see in [START_REF] Ehrhard | Categorical models of linear logic with fixed points of formulas[END_REF], the interpretation of nat in Nuts is a totality space (N, {u ⊆

N | u ̸ = ∅}). So, nat ⊥ = (N, {N}). Hence !(nat ⊥ ) = (M fin (N), {M fin (N)}), since {M fin (N)} = ↑ {M fin (u) | u ∈ {N}}.
The inductive definition of h nat means this set is the least one satisfying

• (0, k[0]) ∈ h nat for any k ∈ N, and • If (n, [n 1 , • • • , n k ]) ∈ h nat , then (n + 1, [n 1 + 1, • • • , n k + 1]) ∈ h nat .
Hence we have

h nat = {(n, k[n]) | k, n ∈ N}.

Conclusion

We have decomposed the proof of termination results for κµLLP (such as in Section 3.6) in two steps: first a normalization result for a non-idempotent intersection typing system in the style of [START_REF] Daniel De | Execution time of lambda-terms via denotational semantics and intersection types[END_REF][START_REF]Execution time of λ-terms via denotational semantics and intersection types[END_REF][START_REF] Amini | On classical pcf, linear logic and the MIX rule[END_REF] and then a purely semantical result: non-uniform totality spaces are a denotational model of κµLLP where proofs have the same interpretation as in Rel. This approach was particularly useful here since, due to the presence of the κ construct and the alternation of polarities in κµLLP, we have not (yet) been able to define a direct realizability interpretation of κµLLP formulas as sets of terms. In some sense we have handled denotationally the logically complex part of this intended realizability semantics. One can also see our construction as a realizability interpretation of formulas graded by the points of the relational model. This method does not seem to say anything interesting about formulas which have an empty interpretation in Rel. This drawback is not so dramatic since, as explained in the conclusion of [START_REF] Ehrhard | Categorical models of linear logic with fixed points of formulas[END_REF], no finite information (of type nat typically) can be extracted internally to κµLLP from proofs of such formulas. Nevertheless the problem of proving some form of normalization for them is an interesting challenge.

Another goal for further work will be to analyze the expressive power of κµLLP as a programming language. It seems clear that we can embed faithfully a version of Gödel's T in κµLLP but we can certainly do much more.

A further direction of work will consist in investigating a related polarized calculus for the circular setting: while the construction κ N,ζ α.c would be much simplified, the challenge will be to account for the global validity condition.

▷ Assume last that Q = !R ⊥ . By inductive hypothesis we have defined t = R π ⊥ , s/ζ -which satisfies ⊢ N , R π ⊥ , N/ζ -| t : R ⊥ [π, P/ζ + ]. It follows that ⊢ N , α : R ⊥ [π, P/ζ + ] | κ.(t ⋆ α) : R π ⊥ , N/ζ -and hence ⊢ N , α : R ⊥ [π, P/ζ + ] | der(κ.(t ⋆ α)) : ?R π ⊥ , N/ζ -so that ⊢ N , β : ?R π ⊥ , N/ζ -| κα.(der(κ.(t ⋆ α)) ⋆ β) : R ⊥ [π, P/ζ + ]. Next we obtain ⊢ N , β : ?R π ⊥ , N/ζ -| κα.(der(κ.(t ⋆ α)) ⋆ β) ! : !R ⊥ [π, P/ζ + ] so that ⊢ N , !R ⊥ [π, P/ζ + ] | κβ.(• ⋆ κα.(der(κ.(t ⋆ α)) ⋆ β) ! ) : ?R π ⊥ , N/ζ -and we define !R ⊥ [π, s/ζ + ] as the term κβ.(• ⋆ κα.(der(κ.(t ⋆ α)) ⋆ β) ! ).
In the same induction we define the negative substitution Q [π, s/ζ -]; this is done as follows.

▷ If Q is a variable, it cannot be ζ -since Q is positive and we must have

Q = ζ + i . It follows that Q [π, N/ζ -] = P i and Q ⊥ π ⊥ , P/ζ + = P ⊥ i so that we set Q [π, s/ζ -] = •. The cases Q = 1 and Q = 0 are similar. ▷ Assume Q = Q 1 ⊗ Q 2 . Let s i = Q i [π, s/ζ -] so that ⊢ N , Q i [π, N/ζ -] | s i : Q ⊥ i π ⊥ , P/ζ + . It follows that ⊢ N , α i : Q ⊥ i π ⊥ , P/ζ + | κ.(s i ⋆ α i ) : Q i [π, N/ζ -] for i = 1, 2. Hence ⊢ N , α 1 : Q ⊥ 1 π ⊥ , P/ζ + , α 2 : Q ⊥ 2 π ⊥ , P/ζ + | (κ.(s 1 ⋆ α 1 ), κ.(s 2 ⋆ α 2 )) : (Q 1 ⊗ Q 2 ) [π, N/ζ -]. So we set (Q 1 ⊗ Q 2 ) [π, s/ζ + ] = κ(α 1 , α 2 ).(• ⋆ (κ.(s 1 ⋆ α 1 ), κ.(s 2 ⋆ α 2 )))
. The other cases are similarly analogous to the definition of the positive substitution.

Proof of Lemma 3.1

Proof. By induction on a assuming that we have a derivation of a : R [P/ζ + ]. We consider several cases, according to the shape of R.

▷ If R = ζ + we choose j ∈ J and set a 0 = (j, ζ), b j = a. ▷ If R = ξ + ̸ = ζ +
we must have a = (j, ξ) and we set a 0 = a. In that case we have rg ζ a 0 = ∅ and so we have no b k 's to define. ▷ If R = 1 we must have a = * and we take a 0 = a. As before rg ζ a 0 = ∅ and so we have no b k 's to define.

▷ If R is R 1 ⊗ R 2 so that a = (a 1 , a 2
) with a i : R i [P/ζ + ] for i = 1, 2. Let J 1 , J 2 ⊆ J be disjoint and infinite. By inductive hypothesis, for i = 1, 2, we can find a 0 i : R with rg ζ a 0 i ⊆ J i as well as families

-→ b(i) = (b(i) j ) j∈rg ζ a 0 i such that ∀j b(i) j : P , (a 0 i , -→ b(i)) is adapted and a i = a 0 i {b(i) j /(j, ζ)} j∈rg ζ a 0 i . For j ∈ rg ζ a 0 = rg ζ a 0 1 ⊎ rg ζ a 0 2 we set b j = b(i) j where i ∈ {1, 2} is uniquely determined by j ∈ rg ζ a 0 i , defining - → b = (b j ) j∈rg ζ a 0 . Let ξ be a literal, j, j ′ ∈ rg ξ a 0 with j ̸ = j ′ and let K = rg ξ b j ∩ rg ξ b j ′ . If j, j ′ ∈ rg ξ a 0 i for i = 1 or i = 2 then K = ∅ since (a 0 i , -→ b(i))
is adapted. If j ∈ rg ξ a 0 i and j ′ ∈ rg ξ a 0 3-i then K = ∅ because we know that rg ξ b j ⊆ rg ξ a i : this is due to the fact that, by inductive hypothesis

a i = a 0 i {b k /(k, ζ)} k∈rg ζ a 0 i . Similarly rg ξ b j ′ ⊆ rg ξ a 3-i and moreover rg ξ a i ∩ rg ξ a 3-i = ∅ because a : R 1 [P/ζ + ] ⊗ R 2 [P/ζ + ]. For the same reason, if j ∈ rg ζ a 0 i we have rg ξ b(i) j ∩ rg ξ a 0 3-i = ∅. It follows that the pair (a 0 , - → b
) is adapted. The fact that a = a 0 {b j /(j, ζ)} j∈rg ζ a 0 is an immediate consequence of the inductive hypothesis. The case R = !R 0 (and hence a = [a 1 , . . . , a n ]) is dealt with similarly (applying the inductive hypothesis to the a i 's) and the case R = R 1 ⊕ R 2 is straightforward: we have a = (i, a 0 ) with a 0 : R i [P/ζ + ] for i = 1 or i = 2 and the inductive hypothesis directly applies to a 0 . ▷ Last if that R = µξ.Q with ξ ̸ = ζ and ξ does not occur in P , so that a = σ(a 0 ) and that we have a derivation of a 0 : R ′ where R

′ = Q [P/ζ + ] [µξ.Q [P/ζ + ]/ξ + ] = Q [R/ξ + ] [P/ζ + ]
. By inductive hypothesis applied to a 0 there is a 0 0 : Q [R/ξ + ] and a family (c j ) j∈rg ξ (a 0 0 ) satisfying the required properties wrt. a 0 . We take a 0 = σ(a 0 0 ) so that rg ζ a 0 = rg ζ a 0 0 and we set b j = c j for each j in that set. 2

6.3 Proof of Lemma 3.2 Proof. Let p = κ.c ∈ |b| Q . This means that c → * • ⋆ q with q ∈ |b| Q \ κ = ∥b∥ Q . It follows that s ⋆ p → c [s/•] → * (• ⋆ q) [s/•] = s ⋆ q ∈ '
(a : P ) (notice that • cannot occur free in q since q is a typed positive term). It follows that s ⋆ p ∈ '(a : P ). 2

Proof of Lemma 3.3

Proof. By induction on the derivation of a P [a 1 , . . . , a n ] we prove that ∥a∥ P ⊆ ∥a i ∥ P which implies the announced inclusions. If the derivation consists of (s-1) then we have P = 1 and ∀i a = a i = * so that the statement obviously holds. If the derivation ends with (s-⊗) then P = P 1 ⊗ P 2 , a = (a 1 , a 2 ), a i = (a 1 i , a 2 i ) and a j P j [a j 1 , . . . , a j n ] for j = 1, 2. The inductive hypothesis gives ∥a j ∥ P j ⊆ ∥a j i ∥ P j for j = 1, 2 and for each i whence the anounced inclusion by definition of ∥(a 1 , a 2 )∥ P 1 ⊗P 2 . The case where the last rule is (s-⊕) is similar. If the last rule is (s-!) then

P = !N , a = [b 1 , . . . , b k ], a i = [b j | j ∈ J i ] with k = n i=1 J i . Let p ∈ ∥a∥ P so that p = s ! with ∀j ∈ k∀q ∈ |b j | N ⊥ s ⋆ q ∈ '. So a fortiori for each i ∈ n one has ∀j ∈ J i ∀q ∈ |b j | N ⊥ s ⋆ q ∈ ', that is p ∈ ∥a i ∥ P . Assume that the last rule is (s-µ) so that P = µζ.Q, a = σ(b), a i = σ(b i ) for i ∈ n and we have b Q [P/ζ + ] [b i , . . . , b n ]. Let p ∈ |a| P , which means that p = fd(q) with q ∈ |b| Q[P/ζ + ] . For i ∈ n we have q ∈ ∥b i ∥ Q[P/ζ + ]
by inductive hypothesis and hence p ∈ ∥a i ∥ P . 2

6.5 Proof of Lemma 3.5

Proof. By induction on the pairs (Q, d), ordered lexicographically, following the definition of substitution of terms in formulas in Section 2.2. It is important to notice that the universal quantification on π is part of the statement we prove by induction. We set J = rg η d.

▷ If Q = 1 then d = * , J = ∅, Q [π, s/η + ] = •, d{b j /(j, η)} j∈J = d{c j /(j, η)} j∈J = * and (a i P i [ ]) n i=1 . We have ⊢ (α i : a i : N i ) n i=1 , * : 1 | • : * : ⊥ as required. The case Q = ζ + ̸ = η + is similar. ▷ If Q = η + , d = (j, η) for some j ∈ I then J = {j} and hence d{b k /(k, η)} k∈J = b j and d{c k /(k, η)} k∈J = c j . Moreover we have (a j i P i [a i ]
) n i=1 so that a j i = a i for each i ∈ n by Lemma 3.4. We have Q [π, s/η + ] = s and the first conclusion is identical to the typing assumption on s. Since Q [π, s/η -] = • the second conclusion is obtained as in the previous cases.

▷ If Q = Q 1 ⊗ Q 2 then d = (d 1 , d 2 ) with (d k : Q k [π]) k=1,2 . Let K = {1, 2} and J k = rg η d k for k ∈ K so that J = J 1 ⊎ J 2 . By Lemma 3.4, for each i ∈ n and k ∈ K there is a(k) i : N ⊥ i such that (a(k) i N ⊥ i [a j i | j ∈ J k ]) n i=1 for k ∈ K and (a i N ⊥ i [a(1) i , a(2) i ]) n i=1
. By inductive hypothesis we have ⊢ (α i : a(k) i :

N i ) n i=1 , d k {b j /(j, η)} j∈J k : Q [π, P/η + ] | Q k [π, s/η + ] : d k {c j /(j, η)} j∈J k : Q ⊥ π ⊥ , N/η -for k ∈ K. Pick some coneutral (e i : N ⊥ i ) n i=1 and f k : Q k π, N ⊥ /η + , we have ⊢ (α i : e i : N i ) n i=1 , β k : d k {c j /(j, η)} j∈J k : Q ⊥ k π ⊥ , N/η -, β 3-k : f 3-k : Q ⊥ 3-k π ⊥ , N/η -| β k : d k {c j /(j, η)} j∈J k : Q k π, N ⊥ /η + . Since (a(k) i N ⊥ i [e i , a(k) i ]) n i=1 we get s k ⋆ β k ⊢ (α i : a(k) i : N i ) n i=1 , d k {b j /(j, η)} j∈J k : Q k [π, P/η + ] , β k : d k {c j /(j, η)} j∈J k : Q ⊥ k π ⊥ , N/η -, β 3-k : f 3-k : Q ⊥ 3-k π ⊥ , N/η -where s k = Q k [π, s/η + ] and conse- quently ⊢ (α i : a(k) i : N i ) n i=1 , β k : d k {c j /(j, η)} j∈J k : Q ⊥ k π ⊥ , N/η -, β 3-k : f 3-k : Q ⊥ 3-k π ⊥ , N/η -| κ.(s k ⋆ β k ) : d k {b j /(j, η)} j∈J k : Q [π, P/η + ]. Using the fact that (a i N ⊥ i [a(1) i , a(2) i ]) n i=1 and the coneu- trality of f 1 , f 2 we get ⊢ (α i : a i : N i ) n i=1 , β 1 : d 1 {c j /(j, η)} j∈J 1 : Q ⊥ 1 π ⊥ , N/η -, β 2 : d 2 {c j /(j, η)} j∈J 2 : Q ⊥ 2 π ⊥ , N/η -| (κ.(s 1 ⋆ β 1 ), κ.(s 2 ⋆ β 2 )) : (d 1 {b j /(j, η)} j∈J 1 , d 2 {b j /(j, η)} j∈J 2 ) : Q [π, P/η + ].
Since we have d{b j /(j, η)} j∈J = (d 1 {b j /(j, η)} j∈J 1 , d 2 {b j /(j, η)} j∈J 2 ) and similarly for d{c j /(j, η)} j∈J , we finally get ⊢ (α i : i , a l i :

a i : N i ) n i=1 , d{b j /(j, η)} j∈J : Q [π, P/η + ] | κ(β 1 , β 2 ).(• ⋆ (κ.(s 1 ⋆ β 1 ), κ.(s 2 ⋆ β 2 ))) : d{c j /(j, η)} j∈J : Q ⊥ π ⊥ , N/η -as contended. The case Q = Q 1 ⊕ Q 2 is similar. The second conclusion is obtained in the same way. The case Q = Q 1 ⊕ Q 2 is similar. ▷ Assume that Q = !R ⊥ , so that d = [d k | k ∈ K] with d k : R π ⊥ . For k ∈ K let J k = rg η d k so that J = J k . By Lemma 3.4, for each i ∈ n and k ∈ K there is a(k) i : N ⊥ i such that (a(k) i N ⊥ i [a j i | j ∈ J k ]) n i=1 for k ∈ K and (a i N ⊥ i [a(k) i | k ∈ K]) n i=1 .
i : N i ) n i=1 , γ : [d k {b j /(j, η)} j∈J k ] : ?R [π, N/η -] | κβ.(der(κ.(t ⋆ β)) ⋆ γ) : d k {c j /(j, η)} j∈J k : R ⊥ π ⊥ , P/η + . Since (a i N ⊥ i [a(k) i | k ∈ K]) n i=1 and [d k {c j /(j, η)} j∈J k | k ∈ K] !R ⊥ [π ⊥ , N ⊥ /η + ] [[d k {c j /(j, η)} j∈J k ] | k ∈ K] we have ⊢ (α i : a i : N i ) n i=1 , γ : [d k {b j /(j, η)} j∈J k | k ∈ K] : ?R [π, N/η -] | κβ.(der(κ.(t ⋆ β)) ⋆ γ) ! : [d k {c j /(j, η)} j∈J k | k ∈ K] : !R ⊥ π ⊥ , P/η + and therefore we have ⊢ (α i : a i : N i ) n i=1 , [d k {c j /(j, η)} j∈J k | k ∈ K] : !R ⊥ π
N ⊥ i such that a i N ⊥ i [a ′ i ] + [a l i | l ∈ L] and a ′ i N ⊥ i [a j i | j ∈ J ′ ] and a l i N ⊥ i [a j i | j ∈ J l ]
, for all i = 1, . . . , n. Let l ∈ L. We set f l = d l {b j /(j, η)} j∈J l and g l = d l {c j /(j, η)} j∈J l . By inductive hypothesis (since sz d l ≤ sz d 0 < sz d) we have, for all l ∈ L,

⊢ (α i : a l i : N i ) n i=1 , f l : µζ.R P [π] | Q π, s/η + : g l : νζ.R ⊥ N π ⊥ (2) Let ρ = π • (µζ.R P [π] /ζ + ).
Notice that all the free variables of R, but possibly η + , η -are in dom(ρ). Let d 1 = f {f l /(l, ζ)} l∈L so that d 1 : R [ρ] since f : R [π] and f l : µζ.R P [π]. Notice that rg η d 1 = J ′ . We apply the inductive hypothesis to (R, d 1 ) and get ⊢ (α i :

a ′ i : N i ) n i=1 , d 1 {b j /(j, η)} j∈J ′ : R [ρ, P/η + ] | R [ρ, s/η + ] : d 1 {c j /(j, η)} j∈J ′ : R ⊥ ρ ⊥ , N/η -. Notice that R [ρ, P/ζ + ] = R P [π] [µζ.R P [π]/ζ + ] and R ρ, N ⊥ /ζ + = R N ⊥ [π] [µζ.R P [π]/ζ + ] so that • ⋆ fd(κ.(R ρ, s/η + ⋆ α)) ⊢ (α i : a ′ i : N i ) n i=1 , σ(d 1 {b j /(j, η)} j∈J ′ ) : µζ.R P [π], α : d 1 {c j /(j, η)} j∈J ′ : R N [π] ⊥ (µζ.R P [π]) ⊥ /ζ -(3)
We have σ(d 1 {b j /(j, η)} j∈J ′ ) = d{b j /(j, η)} j∈J d 1 {c j /(j, η)} j∈J ′ = f {c j /(j, η)} j∈J ′ {f l /(l, ζ)} l∈L hence by ( 2) and (3) applying rule (i-ν 1 ) and using also the fact that

a i N ⊥ i [a ′ i ] + [a l i | l ∈ L], we get ⊢ (α i : a i : N i ) n i=1 , d{b j /(j, η)} j∈J : µζ.R P [π] | µζ.R [π, s/η + ] : σ(f ){c j /(j, η)} j∈J ′ {g l /(l, ζ)} l∈L : νζ.(R N [π]
) ⊥ and notice that σ(f ){c j /(j, η)} j∈J ′ {g l /(l, ζ)} l∈L = d{c j /(j, J)} j∈rg η d since g l = d l {c j /(j, η)} j∈J l and d = σ(f ){d l /(l, ζ)} l∈L ; the announced statement is proven. For the second conclusion we proceed similarly. 2

= η + are trivial. ▷ If Q = Q 1 ⊗ Q 2 then d = (d 1 , d 2 ) with (d k : Q k [π]) k=1,2 and J = J 1 ⊎ J 2 where J k = rg η d k and by inductive hypothesis we have s k = Q k [π, s/η + ] ∈ |g k | N k (f k : P k ) where f k = d k ( - → b ), N k = Q ⊥ k π ⊥ , N/η -, g k = d k ( - → c ) and P k = Q k [π, P/η + ] for k = 1, 2. It suffices to prove that t ∈ |(g 1 , g 2 )| N 1 `N2 ((f 1 , f 2 ) : P 1 ⊗ P 2 ) where t = κ(β 1 , β 2 ).(• ⋆ (κ.(s 1 ⋆ β 1 ), κ.(s 2 ⋆ β 2 ))
). We use Lemma 3.2 so let q k ∈ |g k | Q ⊥ k for k = 1, 2, we have t ⋆ (q 1 , q 2 ) → (• ⋆ (κ.(s 1 ⋆ q 1 ), κ.(s 2 ⋆ q 2 ))). We have s k ⋆ q k ∈ '(f k : P k ) and hence (κ.(s 1 ⋆ q 1 ), κ.(s 2 ⋆ q 2 )) ∈ ∥(f 1 , f 2 )∥ P 1 ⊗P 2 so that • ⋆ (κ.(s 1 ⋆ q 1 ), κ.(s 2 ⋆ q 2 )) ∈ '((f 1 , f 2 ) : P 1 ⊗ P 2 ) and hence t ⋆ (q 1 , q 2 ) ∈ '((f 1 , f 2 ) :

P 1 ⊗ P 2 ). The case Q = Q 1 ⊕ Q 2 is similar. ▷ If Q = !R ⊥ then d = [d 1 , . . . , d k ] with J = k l=1 J l where J l = rg η d l for each l ∈ k. By inductive hypothesis s ′ = R π ⊥ , s/η -∈ |d l ( - → b )| R ⊥ [π,P/η + ] (d l ( - → c ) : R π ⊥ , N/η -) for each l ∈ k and we must prove that t ∈ |[d l ( - → c ) | l ∈ L]| ?R[π ⊥ ,N/η -] ([d l ( - → b ) | l ∈ L] : !R ⊥ [π, P/η + ]) where t = !R ⊥ [π, s/η + ] =
κβ.(• ⋆ (κα.(der(κ.(s ′ ⋆ α)) ⋆ β)) ! ) where s ′ = R π ⊥ , s/η -and for this we apply Lemma 3.2. Let s 1 ∈

l∈L |d l ( - → c )| R ⊥ [π,N ⊥ /η + ] , it suffices to prove that t ⋆ s 1 ! ∈ '([d l ( - → b ) | l ∈ L] : !R ⊥ [π, P/η + ]). We have t ⋆ s 1 ! → • ⋆ (κα.(der(κ.(s ′ ⋆ α)) ⋆ s 1 ! ))
! so it is sufficents to prove (κα.(der(κ.(s

′ ⋆ α)) ⋆ s 1 ! )) ! ∈ |[d l ( - → b ) | l ∈ L]| !R ⊥ [π,P/η + ]
, and hence it is enough to prove that κα.(der(κ.(s

′ ⋆ α)) ⋆ s 1 ! ) ∈ l∈L |d l ( - → b )| R ⊥ [π,P/η + ] . So let q ∈ l∈L |d( - → b )| R[π ⊥ ,P ⊥ /η -]
, it suffices to prove that (der(κ.(s

′ ⋆ q)) ⋆ s 1 ! ) ∈ '. Let l ∈ L, since s ′ ∈ |d l ( - → b )| R ⊥ [π,P/η + ] (d l ( - → c ) : R π ⊥ , N/η -) we have s ′ ⋆ q ∈ '(d l ( - → c ) : R π ⊥ , N/η -) and hence κ.(s ′ ⋆ q) ∈ |d l ( - → c )| R[π ⊥ ,N/η -] and this holds for all l ∈ L, that is κ.(s ′ ⋆ q) ∈ l∈L |d l ( - → c )| R[π ⊥ ,N/η -] . Since s 1 ∈ l∈L |d l ( - → c )| R ⊥ [π,N ⊥ /η + ] it follows that s 1 ⋆ κ.(s ′ ⋆ q) ∈ ', hence der(κ.(s ′ ⋆ q)) ⋆ s 1 ! ∈ ' as expected since der(κ.(s ′ ⋆ q)) ⋆ s 1 ! → s 1 ⋆ κ.(s ′ ⋆ q). ▷ Assume that Q = µζ.R. We set R P = R [P/η + ] and R N = R N ⊥ /η + , Q P = Q [P/η + ] and Q N = Q N ⊥ /η + , and also t = Q [π, s/η + ]. We also use ρ = π • (Q P [π] /ζ + ). We have d = σ(d 0 ) with d 0 : R [π] [Q [π] /ζ + ]
. By Lemma 3.1 we can find f : R [π] as well as a family (d l :

Q [π]) l∈L where L = rg ζ f such that d 0 = f {d l /(l, ζ)} l∈L . Let J = rg η d, we have J = J ′ ⊎ l∈L J l where J ′ = rg η f and J l = rg η d l for each l ∈ L. By inductive hypothesis applied to (Q, d l ) (since sz d l ≤ sz d 0 < sz d) we have t ∈ |g l | Q ⊥ N [π ⊥ ] (f l : Q P [π]) where f l = d l ( - → b ) and g l = d l ( - → c ) for each l ∈ L, since sz d l ≤ sz d 0 < sz d. Notice that f ( - → c ){g l /(l, ζ)} l∈L = d 0 ( - → c
) by definition of the g l 's. We must prove that

t ∈ |d( - → c )| Q ⊥ N [π ⊥ ] (d( - → b ) : Q P [π]) so let p ∈ ∥d( - → c )∥ Q N [π] , it suffices to prove that t ⋆ p ∈ '(d( - → b ) : Q P [π]).
We have p = fd(q) with q ∈ |d 0 ( -

→ c )| R N [π,Q N [π]/ζ + ] . We have (see Section 2.2) t = Q [π, s/η + ] = κ Q ⊥ N [π ⊥ ],ζ α.c where c = • ⋆ fd(κ.(s ′ ⋆ α)) where s ′ = R [ρ, s/η + ]. So t ⋆ p → (R N [π, t/ζ + ] ⋆ q) [κα.c/•]. Notice that f ( - → c ) = f {c j /(j, η)} j∈J ′ satistfies f ( - → c ) : R N [π] and hence by inductive hypothesis applied to (R, f ( - → c )) we have that R N [π, t/ζ + ] belongs to the set |f ( - → c ){g l /(l, ζ)} l∈L | R ⊥ N [π ⊥ ,Q ⊥ N [π ⊥ ]/ζ -] (f ( - → c ){f l /(l, ζ)} l∈L : R N [π, Q P [π] /ζ + ]) since we have seen that t ∈ |g l | Q ⊥ N [π ⊥ ] (f l : Q P [π]) for each l ∈ L. Since q ∈ |d 0 ( - → c )| R N [π,Q N [π]/ζ + ] and d 0 ( - → c ) = f ( - → c ){g l /(l, ζ)} l∈L it follows that c ′ = R N [π, t/ζ + ] ⋆ q ∈ '(f ( - → c ){f l /(l, ζ)} l∈L : R N [π, Q P [π] /ζ + ]) which means c ′ → * • ⋆ r for some r ∈ ∥f ( - → c ){f l /(l, ζ)} l∈L ∥ R N [π,Q P [π]/ζ + ] and therefore c ′ [κα.c/•] → * κα.c ⋆ r = κα.(• ⋆ fd(κ.(s ′ ⋆ α))) ⋆ r → • ⋆ fd(κ.(s ′ ⋆ r)). Notice next that f ′ = f {f l /(l, ζ)} l∈L : R [π, Q P [π] /ζ + ] = R [ρ]. Hence by ind. hyp. applied to (R, f ′ ) and since f ′ ( - → c ) = f ( - → c ){f l /(l, ζ)} l∈L we have s ′ ∈ |f ′ ( - → c )| R ⊥ [ρ ⊥ ,N/η -] (f ′ ( - → b ) : R [ρ, P/η + ]) and hence s ′ ⋆ r ∈ '(f ′ ( - → b ) : R [ρ, P/η + ]). Notice that f ′ ( - → b ) = d 0 ( - → b ) and hence we have κ.(s ′ ⋆ r) ∈ |d 0 ( - → b )| R[ρ,P/η + ]
and therefore, by definition of ρ, fd(κ.(s

′ ⋆r)) ∈ ∥d( - → b )∥ Q P [π] . So we have •⋆fd(κ.(s ′ ⋆r)) ∈ '(d( - → b ) : Q P [π]) and hence t ⋆ p ∈ '(d( - → b ) : Q P [π]
) as contended. ▷ The second statement of the lemma is proved similarly in the same induction of course since the case Q = !R ⊥ (change of polarity) for a given statement uses the other one as an inductive hypothesis. 2 ▷ δ ends with (i-⊥) and we are in case (iv) with N = ⊥, b = * , s = κ ⊥ .c and δ has a subderivation δ 1 whose conclusion is c ⊢ Φ. We have s ′ ⋆ () = κ ⊥ .c ′ ⋆ () → c ′ and since, by inductive hypothesis, c ′ ∈ '(a : P ), if follows that s ′ ∈ | * | ⊥ (a : P ). ▷ δ ends with (i-`) and we are in case (iii) with N = N 1 `N2 , a = (a 1 , a 2 ), s = κ(α 1 , α 2 ).c and we have a subderivation δ 1 whose conclusion is c ⊢ Φ, α 1 : a

1 : N 1 , α 2 : a 2 : N 2 . Let p ∈ ∥(a 1 , a 2 )∥ N ⊥ 1 ⊗N ⊥ 2
, that is p = (q 1 , q 2 ) with q j ∈ |a j | N ⊥ j for j ∈ 2. We have s ′ ⋆ p → c ′ [q 1 /α 1 , q 2 /α 2 ] ∈ ' by inductive hypothesis. It follows that s ′ ∈ |a| N . ▷ δ ends with (i-`) and we are in case (iv) with

N = N 1 `N2 , b = (b 1 , b 2 ), s = κ(α 1 , α 2 ).c and we have a subderivation δ 1 whose conclusion is c ⊢ Φ, α 1 : b 1 : N 1 , α 2 : b 2 : N 2 , a : P . Let p ∈ ∥(b 1 , b 2 )∥ N ⊥ 1 ⊗N ⊥ 2 ,
that is p = (q 1 , q 2 ) with q j ∈ |b j | N ⊥ j for j ∈ 2. We have s ′ ⋆ p → c ′ [q 1 /α 1 , q 2 /α 2 ] ∈ '(a : P ) by inductive hypothesis. It follows that s ′ ∈ |b| N (a : P ). ▷ δ ends with (i-?) so that we are in case (iii) (notice that there no case (iv) for this rule) with N = ?Q, a = [b], s = der(p) and δ has a subderivation δ 1 whose conclusion is

⊢ Φ | p : b : Q. Let p ∈ ∥[b]∥ !Q ⊥ , that is p = t ! where t ∈ |b| Q ⊥ . We have s ′ ⋆ p → t ⋆ p ′ ∈ ' since p ′ ∈ |b| Q by inductive hypothesis.
▷ δ ends with (i-cut) and we are in case (i) with c = s ⋆ p and δ has two subderivations δ 1 and δ 2 with conclusions ⊢ (α i : a 1 i :

P ⊥ i ) n i=1 | s : b : Q ⊥ and ⊢ (α i : a 2 i : P ⊥ i ) n i=1 | p : b : Q and a i P i [a 1 i , a 2
i ] for all i ∈ n so that by Lemma 3.3 we have p i ∈ |a j i | P i for all i ∈ n and j ∈ 2. By inductive hypothesis we have

s ′ ∈ |b| Q ⊥ and p ′ ∈ |b| Q so that c ′ = s ′ ⋆ p ′ ∈ '.
▷ δ ends with (i-cut) and we are in case (ii) with c = s ⋆ p and δ has two subderivations δ 1 and δ 2 with conclusions ⊢ (α i : a 1 i :

P ⊥ i ) n i=1 , a : P | s : b : Q ⊥ and ⊢ (α i : a 2 i : P ⊥ i ) n i=1 | p : b : Q and a i P i [a 1 i , a 2
i ] for all i ∈ n so that by Lemma 3.3 we have p i ∈ |a j i | P i for all i ∈ n and j ∈ 2. By inductive hypothesis we have s ′ ∈ |b| Q ⊥ (a : P ) and p ′ ∈ |b| Q so that c ′ = s ′ ⋆ p ′ ∈ '(a : P ). ▷ δ ends with (i-ν), remember that this rule is given at the beginning of Section 3.2. Assume that we are in case (iv) with N = νζ.R ⊥ , s = κ R ⊥ ,ζ α.(c ; t), we have a point d : R, a subderivation δ ′′ of δ whose conclusion is ⊢ (α i : a ′′ i : P ⊥ i ), a : P | t : h : Q ⊥ , a subderivation δ ′ of δ whose conclusion is c ⊢ (α i : a ′ i : P ⊥ i ), h : Q, α : d{h l /(l, η)} l∈L : R ⊥ Q ⊥ /ζ -, and for each l ∈ L = rg ζ d we have a subderivation δ l of δ whose conclusion is ⊢ (α i : a l i :

P ⊥ i ) n i=1 , h l : Q | u : f l : νζ.R ⊥ where u = κ R ⊥ ,ζ α.c = κ R ⊥ ,ζ α.(c ; •). With these notations we have b = σ(d){f l /(l, ζ)} l∈L . Moreover a i P i [a ′ i , a ′′ i ] + [a l i | l ∈ L]
so that by Lemma 3.3 we have p i ∈ |a l i | P i for all i ∈ n and l ∈ L, and

p i ∈ |a ′ i | P i , p i ∈ |a ′′ i | P i for all i ∈ n. Let p ∈ ∥b∥ N ⊥ so that p = fd(q) with q ∈ |d{f l /(l, ζ)} l∈L | R[N ⊥ /ζ + ] . Then we have s ′ ⋆p → (R [u ′ /ζ + ]⋆q) [κα.c ′ [t ′ /•] /•]. By inductive hypothesis applied to the δ l 's we have u ′ ∈ |f l | N (h l : Q) for each l ∈ L and hence by Lemma 3.6, R [u ′ /ζ + ] ∈ |d{f l /(l, ζ)} l∈L | R[N/ζ -] (d{h l /(l, ζ)} l∈L : R [Q/ζ + ]), therefore: R [u ′ /ζ + ] ⋆ q ∈ '(d{h l /(l, ζ)} l∈L : R [Q/ζ + ]) which means that R [u ′ /ζ + ] ⋆ q → * • ⋆ r with r ∈ ∥d{h l /(l, ζ)} l∈L ∥ R[Q/ζ + ] . It follows that (R [u ′ /ζ + ] ⋆ q) [κα.c ′ [t ′ /•] /•] → * κα.c ′ [t ′ /•] ⋆ r → c ′ [r/α] [t ′ /•] since r /
∈ κ, r is closed and t ′ has no free names. By inductive hypothesis applied to δ ′ (with substituting positive terms the p i 's and r which satisfies

r ∈ |d{h l /(l, ζ)} l∈L | R[Q/ζ + ] as required) we have c ′ [r/α] ∈ '(h : Q) and hence κ.(c ′ [r/α]) ∈ |h| Q . We also have t ′ ∈ |h| Q ⊥ (a : P ) by inductive hypothesis and hence t ′ ⋆ κ.(c ′ [r/α]) ∈ '(a : P ) so that c ′ [r/α] [t ′ /•]
∈ '(a : P ) and hence s ′ ⋆ p ∈ '(a : P ). Since this holds for all p ∈ ∥b∥ N ⊥ we have proven that s ′ ∈ |b| N (a : P ) as required. ▷ δ ends with (i-ν) and we are in case (iii) with N = νζ.R ⊥ , s = κ R ⊥ ,ζ α.(c ; t), we have a point d : R, a subderivation δ ′′ of δ whose conclusion is ⊢ (α i : a ′′ i :

P ⊥ i ) | t : h : Q ⊥ ,
P(f 1 , f 2 ) P( -→ A 1 , h-→ Y 1 ) P( -→ A 2 , h-→ Y 2 ) P-→ A 1 , -→ Y 1 P-→ A 2 , -→ Y 2 !P(f 1 , f 2 ) 2
6.9 Proof of Lemma 4.3

Proof.

The first item hold because of commutation of the following diagram :

Z ⊗ P( - → A , -→ Y 1 , X) P( - → A , -→ Y 1 , Y ) !(Z ⊗ P( - → A , -→ Y 1 , Y )) !P( - → A , -→ Y 1 , Y ) P[Z]( -→ Id , -→ Id , f ) h Z⊗P + ( - → A , -→ Y 1 ,X) h P + ( - → A , -→ Y 1 ,Y ) !(P[Z](f ⊥ , -→ Id , -→ Id ))
And the second item is similar to the first one. 2 6.10 Proof of Lemma 4.4

Proof.

Since F ∈ L k+1 , there is a functor µF : L k → L such that µF( -→ A ) is the initial object of the category Alg L (F-→ A ) for any object A ∈ L.

Z ⊗ µF( - → A ) B Z ⊗ Z ⊗ F-→ A (µF( - → A )) Z ⊗ F-→ A (µF( - → A )) Z ⊗ F-→ A (B) Z ⊗ Z ⊗ F-→ A (µF(A)) Z ⊗ F-→ A (Z ⊗ µF( - → A )) Z ⊗ !Z ⊗ F-→ A (µF(A)) Z ⊗ F-→ A (!Z ⊗ µF(A))
Z ⊗ Q[Z](Y ) = Z ⊗ Q(Y ) Y g 2 6.
12 Proof of Lemma 4.6

Proof.

By definition, we have µQ + = µQ = µQ = µQ. The following diagram commutes which shows that g is indeed a co-algebra morphism.

!Z ⊗ µQ Y !(!Z ⊗ µQ) !Y g h !Z⊗µQ h Y ! g Z ⊗ µQ Y Z ⊗ Q(µQ) Z ⊗ Z ⊗ Q(µQ) Z ⊗ !Z ⊗ Q(µQ) Z ⊗ Q(!Z ⊗ µQ) Z ⊗ Q(Z ⊗ µQ) Z ⊗ Q(Y ) !Z ⊗ Q(!µQ) !Z ⊗ !Z ⊗ Q(!µQ) !Z ⊗ !!Z ⊗ Q(!µQ) !Z ⊗ Q(!!Z ⊗ !µQ) !Z ⊗ Q(!Z ⊗ !µQ) !Z ⊗ Q(!Y ) !Z ⊗ !µQ !Z ⊗ !(Q(µQ)) !Z ⊗ !Z ⊗ !Q(µQ) !Z ⊗ !!Z ⊗ !Q(µQ) !Z ⊗ Q(!(!Z ⊗ µQ)) !Z ⊗ Q(!(Z ⊗ µQ)) !Z ⊗ !Q(Y ) !Z ⊗ !(Z ⊗ Q(µQ)) !Z ⊗ !(!Z ⊗ Q(µQ)) !Z ⊗ !(Q(!Z ⊗ µQ)) !Z ⊗ !(Q(Z ⊗ µQ)) !(Z ⊗ Q(µQ)) !(Z ⊗ Z ⊗ Q(µQ)) !(Z ⊗ !Z ⊗ Q(µQ)) !(Z ⊗ Q(!Z ⊗ µQ)) !(Z ⊗ Q(Z ⊗ µQ)) !(Z ⊗ Q(Y )) !(Z ⊗ µQ) !Y g h Z ⊗h µQ + h Y ≃ C Z ⊗Id h Z ⊗Q(h µQ ) Id ⊗h Z ⊗Id h Z ⊗h Z ⊗Q(h µQ ) Id ⊗ Q h Z ⊗dig Z ⊗Q(h

Fig. 1 .

 1 Fig. 1. Syntax of formulas Remark 2.2 With each literal ζ are associated two distinct variables ζ + and ζ -which are formulas (a literal is not a formula). In the formula µζ.P , only the occurrences of ζ + are bound and dually for νζ.N which binds only ζ -.Although not strictly necessary, we adopt the convention that for a given literal ζ it is never the case that both ζ + and ζ -occur in a given formula. This property can be enforced by α-renaming for closed formulas.

Lemma 2 . 5

 25 If α does not occur in negative context N , the following holds. If c ⊢ N [, P ] then c ⊢ N , α : N [, P ]. If ⊢ N [, P ] | t : M then ⊢ N , α : N [, P ] | t : M . If ⊢ N | p : P then ⊢ N , α : N | p : P .

Fig. 2 .

 2 Fig. 2. Syntax of terms and typing rules

Fig. 3 .

 3 Fig. 3. Reduction of commands

  and hence ⊢ N , α : R ⊥ [π, P/ζ + ] | der(κ.(t ⋆ α)) : ?R π ⊥ , N/ζ -so that ⊢ N , β : ?R π ⊥ , N/ζ -| κα.(der(κ.(t ⋆ α)) ⋆ β) : R ⊥ [π, P/ζ + ]. Next we obtain ⊢ N , β : ?R π ⊥ , N/ζ -| κα.(der(κ.(t ⋆ α)) ⋆ β) ! : !R ⊥ [π, P/ζ + ] so that ⊢ N , !R ⊥ [π, P/ζ + ] | κβ.(• ⋆ κα.(der(κ.(t ⋆ α)) ⋆ β) ! ) : ?R π ⊥ , N/ζ -and we define !R ⊥ [π, s/ζ + ] as the term κβ.(• ⋆ κα.(der(κ.(t ⋆ α)) ⋆ β) ! ).

Fig. 4 .

 4 Fig. 4. Syntax, size, typing rules and structural relation for points

Fig. 5 .

 5 Fig. 5. Point deduction system -the rule (i-ν) is given in the body of Section 3.2. a 0 {b j /(j, ζ)} j∈J : R [P/ζ + ]. One proves easily that, for any literal ξ

Lemma 3 . 1

 31 Let R and P be positive formulas and let ζ be a literal. Let a be a point such that a : R [P/ζ + ]. Let J ⊆ I be an infinite set. There is a point a 0 such that a 0 : R and rg ζ a 0 ⊆ J and there is a family of points -→ b = (b j ) j∈rg ζ a 0 such that b j : P for all j ∈ rg ζ a 0 , (a 0 , -→ b ) is adapted and a = a 0 {b j /(j, ζ)} j∈rg ζ a 0 .

Lemma 3 . 3

 33 If a P [a 1 , . . . , a n ]. Then ∥a∥ P ⊆ ∥a i ∥ P and |a| P ⊆ |a i | P for 1 ≤ i ≤ n. Lemma 3.4 Let P be a closed positive formula and let a : P . If b : P , one has a P [b] iff a = b. Let (b j : P ) j∈J , (J k ) k∈K be such that k∈K J k = J. Then one has a P [b j | j ∈ J] iff there is (c k

() : 1 ,

 1 ⊢ 1 | • : ⊥ and ⊢| κ ⊥ .• : ⊥. Therefore ⊢| rd = it((), • ; κ ⊥ .•) : nat ⊥ . This negative term is a "reader of integer" which behaves as follows: rd ⋆0 → * • and rd ⋆ suc p → * rd ⋆p. By induction on n ∈ N it is not hard to check that ∀n ∈ N ⊢| rd : n : nat ⊥ . Let m = [n 1 , . . . , n k ] : ?nat, we have therefore ⊢| rd ! : m : !nat ⊥ and hence rd ! ∈ ∥m∥ !nat ⊥ by Theorem 3.7. If c ⊢ α : m = [n 1 , . . . , n k ] : ?nat then by Theorem 3.7 we have c rd ! /α ∈ '. By Lemma 2.10 this implies that the reduction of c terminates, so that c → * t ⋆ α where ⊢ α : m 1 : ?nat | t : m 2 : ?nat, t is not of shape κβ.d and m = m 1 + m 2 . So we must have t = der(p) with ⊢ α : m 1 : ?nat | p : n : nat for some n ∈ N and m 2 = [n]. So by Theorem 3.7 we have p rd ! /α ∈ |n| nat and hence by Lemma 3.8 val p = n. As a whole we have described an algorithm which, under the assumption that c ⊢ α : m : ?nat for some m, produces an integer n that we denote as val α c, and we have m = m 1 + [n].

4. 1

 1 Operations on positive functors 4.1.1 LL operations on positive functors Given a (n, p)-positive functor P, strong functors

Lemma 4 . 14

 414 If c → d, then either c N = d N or c + N ,P = d + N ,P depending on the typing derivation of c and d. Theorem 4.15 If c → ⋆ d, then either c N = d N or c + N ,P = d + N ,P depending on the typing derivation of c and d.

  ⊥ , P/η + | κγ.(• ⋆ κβ.(der(κ.(t ⋆ β)) ⋆ γ) ! ) : [d k {b j /(j, η)} j∈J k | k ∈ K] : ?R [π, N/η -] as required. The second conclusion is dealt with similarly. ▷ Assume that Q = µζ.R. We set R P = R [P/η + ] and R N = R N ⊥ /η + . We have d = σ(d 0 ) with d 0 : R [π] [Q [π] /ζ + ]. By Lemma 3.1 we can find f : R [π] as well as a family (d l : Q [π]) l∈L where L = rg ζ f such that d 0 = f {d l /(l, ζ)} l∈L . Let J = rg η d, we have J = J ′ ⊎ l∈L J l where J ′ = rg η f and J l = rg η d l for each l ∈ L. By Lemma 3.4 we can find a ′

6. 6

 6 Proof of Lemma 3.6 Proof. By induction on the pairs (Q, d), ordered lexicographically, following the definition of substitution of terms in formulas in Section 2.2. ▷ The cases Q = 1 and Q

  a subderivation δ ′ of δ whose conclusion is c ⊢ (α i : a ′ i :P ⊥ i ), h : Q, α : d{h l /(l, η)} l∈L : R ⊥ Q ⊥ /ζ -,and for each l ∈ L = rg ζ d we have a subderivation δ l of δ whose conclusion is ⊢ (α i : a l i :P ⊥ i ) n i=1 , h l : Q | u : f l : νζ.R ⊥ where u = κ R ⊥ ,ζ α.c = κ R ⊥ ,ζ α.(c ; •). With these notations we have b = σ(d){f l /(l,

g 2 6. 11

 211 Id ⊗(W Z ⊗≃)C Z ⊗Id C Z ⊗Id g Id ⊗h Z Id Id ⊗F-→ A ( g) Id ⊗ F-→ A Id ⊗F-→ A (der Z ⊗Id) Proof of Lemma 4.5Proof.By Lemma 4.4, we know that there is a unique objectµ(Q[Z]) ∈ L[Z] which is (µQ)[Z]. We also know that µQ is the initial object in Alg L (Q), since Q ∈ L. And (µQ)[Z] is same as µQ (considering µQ, equivalently, as µQ : 1 → L). So, to define morphism g∈ L[Z](µ(Q[Z]), Y ), one need to provide a morphism g in L[Z](Q[Z](Y ), Y) which is as follows:

Fig. 7 . 2 C N ⊥ p 1 +N ⊗ p 2 P [ t 1 +N ,P , t 2 +N▷

 721212 Fig. 7. Proof of Lemma 4.6

  By inductive hypothesis, for each k ∈ K we have ⊢ (α i : a(k) i :N i ) n i=1 , d k {c j /(j, η)} j∈J k : R [π, N/η -] | t : d k {b j /(j, η)} j∈J k : R ⊥ π ⊥ , P/η + , where t = R [π, s/η -], so ⊢ (α i : a(k) i : N i ) n i=1 , β : d k {b j /(j, η)} j∈J k : R ⊥ π ⊥ , P/η + | κ.(t ⋆ β) : d k {c j /(j, η)} j∈J k : R [π, N/η -]. So ⊢ (α i : a(k) i : N i ) n i=1 , β : d k {b j /(j,η)} j∈J k : R ⊥ π ⊥ , P/η + | der(κ.(t ⋆ β)) : [d k {c j /(j, η)} j∈J k ] : ?R [π, N/η -] and hence ⊢ (α i : a(k)

  ζ)} l∈L . Moreover a i P i [a ′ i , a ′′ i ] + [a l i | l ∈ L]so that by Lemma 3.3 we have p i ∈ |a l i | P i for all i ∈ n and l ∈ L, andp i ∈ |a ′ i | P i , p i ∈ |a ′′ i | P i for all i ∈ n. Let p ∈ ∥b∥ N ⊥ so that p = fd(q) with q ∈ |d{f l /(l, ζ)} l∈L | R[N ⊥ /ζ + ] . Then we have s ′ ⋆p → (R [u ′ /ζ + ]⋆q) [κα.c ′ [t ′ /•] /•]. By inductive hypothesis applied to the δ l 's we have u ′ ∈ |f l | N (h l : Q) for each l ∈ L and hence, by Lemma 3.6, R [u ′ /ζ + ] ∈ |d{f l /(l, ζ)} l∈L | R[N/ζ -] (d{h l /(l, ζ)} l∈L : R [Q/ζ + ]), therefore R [u ′ /ζ + ] ⋆ q ∈ '(d{h l /(l, ζ)} l∈L : R [Q/ζ + ]) which means that R [u ′ /ζ + ] ⋆ q → * • ⋆ r with r ∈ ∥d{h l /(l, ζ)} l∈L ∥ R[Q/ζ + ] . It follows that (R [u ′ /ζ + ] ⋆ q) [κα.c ′ [t ′ /•] /•] → * κα.c ′ [t ′ /•] ⋆ r → c ′ [r/α] [t ′ /•] since r / ∈ κ,r is closed and t ′ is closed. By inductive hypothesis applied to δ ′ (with substituting positive terms the p i 's and r which satisfies r ∈ |d{h l/(l, ζ)} l∈L | R[Q/ζ + ] as required) we have c ′ [r/α] ∈ '(h : Q) and hence κ.(c ′ [r/α]) ∈ |h| Q . We also have t ′ ∈ |h| Q ⊥ by inductive hypothesis and hence t ′ ⋆ κ.(c ′ [r/α]) ∈ ' so that c ′ [r/α] [t ′ /•] ∈ ' and hence s ′ ⋆ p ∈ '.Since this holds for all p ∈ ∥b∥ N ⊥ we have proven that s ′ ∈ |b| N as required. 26.8 Proof of Lemma 4.2Let (f 1 , f 2 ) ∈ (L n × (L ! ) p )(()), we define P + (f 1 , f 2 ) ∈ L ! (P + ( , f 2 ). And the following diagram commutes which shows that P(f 1 , f 2 ) is indeed a morphism in L ! .

	Proof. Given (	-→ A ,	-→ Y ) ∈ L n × (L ! ) p where	-→ Y = ( -→ Y , h-→ Y ), we define P + ( -→ A ,	-→ Y ) as P( -→ A ,	-→ Y ) and h P ′ ( -→ A ,	-→ Y ) as the
	following composition of morphisms in L:
	P( -→ A ,	-→ Y )	P( -→ A , -→ h Y )	P( -→ A ,	-→ !Y )	P-→ A ,Y	!P( -→ A , Y )
							-→ A 1 ,	-→ Y 1 ), (	-→ A 2 ,	-→ Y 2 -→ A 1 ,	-→ Y 1 ), P + (	-→ A 2 ,	-→ Y 2 )) as
	P(f 1 P( -→ A 1 ,	-→ Y 1 )	P( -→ A 2 ,	-→ Y 2 )
							P( -→ A 1 ,	-→ !Y 1 )	P(	-→ A 2 ,	-→ !Y 2 )
							!P(	-→ A 1 ,	-→ Y 1 )	!P( -→ A 2 ,	-→ Y 2 )

This simple dichotomy relies on the fact that, in LLP, the introduction of an !-connective is possible only on a negative sequent which corresponds to the fact that in LL promotion requires the context to have only ?-formulas.

This strongly suggests that lists and streams are not of the same nature, streams are not data but data consumers.

Indeed in the λµ-calculus all formulas are negative and the names are associated with the formulas occurring on the right side of a sequent whereas variables are associated with formulas on the left.

This may seem surprising at first sight but remember that weakening is freely available for all negative formulas. So the real meaning of this rule is • ⊢ which is the familiar 0-ary mix rule of LL. It is easy to check that all properties of κµLLP proven so far are still valid for this extension.

Weakening w E ∈ Rel(!E, 1) and contr E ∈ Rel(!E, !E ⊗ !E) are given by w E = {([], * )} and contr E = {(m 1 + m 2 , (m 1 , m 2 )) | m i ∈ M fin (E) for i = 1, 2}.

Positive functors on Rel

Definition 5.1 An n-ary variable set is a strong functor F : Rel n → Rel such that F is locally continuous and and maps inclusions to inclusions.

Definition 5.2 A positive n + p-ary variable set is a (n, p)-positive functor P : Rel n+p → Rel such that P is an n + p-ary variable set.

5.2 Non-uniform totality spaces as a model of κµLLP

Basic definitions.

Let E be a set and let T ⊆ P(E). We define

If S ⊆ T ⊆ P(E) then (T ) ⊥ ⊆ S ⊥ . We also have T ⊆ T ⊥⊥ and therefore T ⊥⊥⊥ = T ⊥ . One nice feature of this duality is:

A non-uniform totality space (NUTS) is a pair X = (|X|, T (X)) where |X| is a set and T (X) ⊆ P(|X|) satisfies T (X) = T (X) ⊥⊥ , that is T (X) = ↑T (X). Of course we set X ⊥ = (|X|, T (X) ⊥ ). We define four basic NUTS: 0 = (∅, ∅), ⊤ = (∅, {∅}) and 1 = ⊥ = ({ * } , {{ * }}). Given NUTS X 1 and X 2 we define a NUTS

We define the category Nuts whose objects are the NUTS and Nuts(X, Y ) = T (X ⊸ Y ), composition being defined as the usual composition in Rel (relational composition) and identities as the diagonal relations. Lemma 5.4 shows that we have indeed defined a category.

Multiplicative structure

We turn now ⊗ into a functor, its action on morphisms being defined as in Rel. Lemma 5.6 and by the equation

. This functor is monoidal, with unit 1 and symmetric monoidality isomorphisms λ, ρ, γ and α defined as in Rel.

The SMC category Nuts is closed, with X ⊸ Y as internal hom object from X to Y , and evaluation morphism ev = {(((a, b), a), b | a ∈ |X| and b ∈ |Y |} which indeed belongs to Nuts((X ⊸ Y ) ⊗ X, Y ) by Lemma 5.6. This category Nuts is also *-autonomous with dualizing object ⊥ = 1.

Additive structure.

Let (X i ) i∈I be an at most countable family of objects of Nuts. We define X = &i∈I

It is clear that T (X) = ↑T (X) and hence X is an object of Nuts. By definition of X and by Lemma 5.4 we have ∀i ∈ I π i ∈ Nuts(X, X i ). Given -→ t = (t i ) i∈I with ∀i ∈ I t i ∈ Nuts(Y, X i ), we have ⟨ -→ t ⟩ ∈ Nuts(Y, X) as easily checked (using Lemma 5.4 again). It follows that ( &i∈I X i , (π i ) i∈I ) is the cartesian product of the X i 's in Nuts. This shows that the category Nuts has all countable products and hence is cartesian. Since it is *-autonomous, the category Nuts is also cocartesian. Notice that the final object is ⊤ = (∅, {∅}) and that 0 = ⊤ ⊥ = (∅, ∅).

Exponential.

It is an extension of the multiset exponential of Rel with totality.

We set |!X| = M fin (|X|) and

Remark 5.8 A formula is interpreted as exactly the same set in Rel and Nuts (with the additional totality structure in Nuts of course). Similarly a proof is interpreted as the same set in both models; Nuts gives us additionally that this set is total.

Variable non-uniform totality spaces (VNUTS)

Let E be a set, we use Tot(E) for the set of all totality candidates on E, that is, of all subsets T of P(E) such that T = T ⊥⊥ (remember that

In other words T ∈ Tot(E) means that ↑T by Lemma 5.3. Ordered by ⊆, this set Tot(E) is a complete lattice.

Lemma 5.11 Any n + p-ary positive VNUTS P : Nuts n+p → Nuts induces a (n, p)-positive functor P : Nuts n+p → Nuts which satisfies

and P can be retrieved from P.

Appendix

6.1 Definition of substitution of terms in formulas

we use the same notations as for ⊗. We have ⊢ N , α i :

) by (t-ν 1 ).

Proof of Theorem 3.7

Proof. By induction on the point derivation δ for c, t and p. To increase readibility we use c ′ for c[p i /α i ] n i=1 and similarly for s and p. In the induction, we use the notations introduced in the statement of the theorem to avoid boring sentences introducing new symbols. But one has to keep in mind that the satement proven by induction contains the universal quantification on the p i 's. ▷ δ consists of (i-n) so that we are in case (v) with p = α j for some j ∈ n, and a = a j . In that case we have p ′ = p j and the expected conclusion follows from ∥a j ∥ P j ⊆ |a j | P j . ▷ δ consists of (i-1) so that we are in case (v) with p = () and a = * We have p ′ = () so that p ′ ∈ ∥ * ∥ 1 ⊆ | * | 1 . ▷ δ ends with a (i-⊗) so that we are in case (v) with p = (q 1 , q 2 ), a = (b 1 , b 2 ) and we have subderivations δ j of ⊢ (α i : a j i :

i ] for all i ∈ n. For each i ∈ n we know that p i ∈ ∥a i ∥ P i and hence by Lemma 3.3 we have p i ∈ ∥a j i ∥ P i for each i ∈ n and j ∈ 2. Hence by inductive hypothesis

▷ δ ends with a left (i-⊕) the case of a right (i-⊕) being of course completely similar. We are in case (v) and P = Q 1 ⊕ Q 2 , p = in 1 (q) and a = (1, b) and we have a subderivation

▷ δ ends with a (i-κ). We are in case (v) with p = κ.c and we have a subderivation δ 1 of δ which has c ⊢ Φ, a : P as conclusion. By inductive hypothesis we have c ′ ∈ '(a : P ) = |a| P • = ∥a∥ P • and hence p ′ = κ.c ′ ∈ |a| P as required. ▷ δ ends with (i-µ) so that we are in case (v) with P = µζ.Q, p = fd(q) and a = σ(b) and δ has a subderivation δ 1 whose conclusion is

▷ δ ends with (i-!) so that we are in case (v) with P = !N , p = s ! and a = [b j | j ∈ J] and δ has a subderivation δ j of ⊢ (α i : a j i : P ⊥ i ) | s : b j : N for each j ∈ J and moreover we have a i P i [a j i | j ∈ J] for each i ∈ n. Since ∥a i ∥ P i ⊆ ∥a j i ∥ P i for each i ∈ n and j ∈ J we have s ′ ∈ |b j | N by inductive hypothesis applied to δ j for each j ∈ J and hence

▷ δ is (i-•) so that we are in case (iv) with N = P ⊥ , s = •, b = a and a i P i [ ] for each i ∈ n. We have s ′ = • so that for all p ∈ ∥a∥ P we have s ′ ⋆ p ∈ '(a : P ) which means that s ′ ∈ |a| P ⊥ (a : P ) as required. ▷ δ ends with a left (i-&) (the case of a right (i-&) is of course completely similar) and we are in case (iii) with N = N 1 &N 2 , a = (1, a 1 ), s = ⟨s 1 , s 2 ⟩ and we have a subderivation δ 1 whose conclusion is ⊢ Φ | s 1 : a 1 : N 1 . The other subderivation δ 2 makes sure that s 2 is well typed in the typing system of Figure 2

by inductive hypothesis and hence s ′ ∈ |a| N . ▷ δ ends with a left (i-&) (the case of a right (i-&) is of course completely similar) and we are in case (iv) with

The other subderivation δ 2 makes sure that s 2 is well typed in the typing system of Figure 2.

We take (µF)[Z] as the unique functor µ(F[Z]). Let us take an object A ∈ L. We have (µF

where h is the following:

) which is as follows:

So, g is cur ′ -1 ( g ′ ), and it satisfies the following diagram:

One can see that the following diagram is just unfolding of Diagram 4:

6.14 Proof of Lemma 4.14

Proof. We prove it by case analysis of c and d based on the reduction system in Figure 3.