Luigi Liquori
email: luigi.liquori@inria.fr

Simona Ronchi
email: ronchi@di.unito.it

Della Rocca

Intersection-Types à la Church

Keywords:

In this paper, we present Λ t ∧ , a fully typed λ-calculus based on the intersection-type system discipline, which is a counterpart à la Church of the type assignment system as invented by Coppo and Dezani. The relationship between Λ t ∧ and the intersection type assignment system is the standard isomorphism between typed and type assignment system, and so the typed language inherits from the untyped system all the good properties, like subject reduction and strong normalization. Moreover both type checking and type reconstruction are decidable.

Introduction

The implicative and conjunctive fragment of the intuitionistic logic (denoted by L ∧ → ), where the logical connectives "→" and "∧" denote the implication and the conjunction is a well-known powerful logical system: this logic is presented in Figure 1. Finding a typed λ-calculus à la Church, in the Curry-Howard sense is not a simple task [Hindley (1984)], because of the "anomalous" decoration of the rules dealing with conjunction.

The Intersection-Type Assignment System ( ∧ ) is a set of inference rules for assigning intersection-types to terms of the untyped λ-calculus. Intersectiontypes are formulae of the implicational and conjunctive fragment of propositional logic. The syntax and the typing rules are presented in Figure 2. Intersection-Let Σ = {σ 1 , . . . , σ n }, and Σ, σ = Σ ∪ {σ}

σ ∈ Σ Σ L ∧ → σ (Var) Σ, σ 1 L ∧ → σ 2 Σ L ∧ → σ 1 →σ 2 (→I) Σ L ∧ → σ 1 →σ 2 Σ L ∧ → σ 1 Σ L ∧ → σ 2 (→E) Σ L ∧ → σ 1 Σ L ∧ → σ 2 Σ L ∧ → σ 1 ∧ σ 2 (∧I) Σ L ∧ → σ 1 ∧ σ 2 Σ L ∧ → σ 1 (∧E L ) Σ L ∧ → σ 1 ∧ σ 2 Σ L ∧ → σ 2 (∧E R ) Figure 1. The Logic L ∧ → Syntax of Λ u ∧
Let α range over a denumerable set V of type-constants Let "∧" take precedence over "→"

M ::= x | λx.M | M M σ ::= α | σ→σ | σ ∧ σ
Type System for Λ u ∧ Let E = {x 1 :σ 1 , . . . , x n :σ n } (i = j implies x i ≡ x j ), and E, x:σ = E ∪ {x:σ}

x:σ ∈ E E ∧ x : σ (Var) E, x:σ 1 ∧ M : σ 2 E ∧ λx.M : σ 1 →σ 2 (→I) E ∧ M : σ 1 →σ 2 E ∧ N : σ 1 E ∧ M N : σ 2 (→E) E ∧ M : σ 1 E ∧ M : σ 2 E ∧ M : σ 1 ∧ σ 2 (∧I) E ∧ M : σ 1 ∧ σ 2 E ∧ M : σ 1 (∧E L ) E ∧ M : σ 1 ∧ σ 2 E ∧ M : σ 2 (∧E R )
Figure 2. The Intersection-Type Assignment System ∧ .

types were introduced by Coppo and Dezani, to increase the typability power of Curry's type assignment system for the λ-calculus [START_REF] Coppo | An Extension of the Basic Functionality Theory for the λ-calculus[END_REF]]. Since then, intersection-types have been fruitfully used for designing static semantics of programming languages (e.g. Algol-like [Reynolds (1996)]), for characterizing interesting classes of λ-terms (e.g. the strongly normalizing ones [Pottinger (1980)]), and for studying denotational semantics of various untyped λcalculi (e.g. [START_REF] Barendregt | A Filter Lambda Model and the Completeness of Type Assignment[END_REF]] and [START_REF] Coppo | Extended Type Structures and Filter Lambda Models[END_REF]]).

There are many versions in the literature of intersection-type assignment systems.

Here we choose that one presented as "System D" [ Krivine (1990)], characterized by the presence of non syntax-directed rules for dealing with the introduction and elimination of the intersection. Note that, differently from most of the systems presented in the literature, as for example [START_REF] Dezani-Ciancaglini | Intersection-types, Lambda-models and Böhm Trees[END_REF]], in this system the connective ∧ is neither commutative nor associative nor idempotent. The choice of this presentation has been taken since we are looking for a typed version of the calculus, where bound variables come decorated with their types, and in this setting it is natural to consider types as syntactical entities. In any case, this presentation does not have any consequence on the typability power of the intersection type assignment system, which is well known to characterize all and only the strongly normalizing terms [Krivine (1990), Pottinger (1980)].

Following the standard terminology, let us call à la Curry a system assigning types to untyped terms, and à la Church a system assigning types to typed terms, i.e.

where types are part of the syntax of terms, by decorating bound-variables in abstractions. Differently from other type assignment systems à la Curry, Λ u ∧ has no natural counterpart à la Church. The classical example is the polymorphic identity in Λ u ∧ that has the following type-derivation:

x:σ 1 ∧ x : σ 1 ∧ λx.x : σ 1 →σ 1 (→I) x:σ 2 ∧ x : σ 2 ∧ λx.x : σ 2 →σ 2 (→I) ∧ λx.x : (σ 1 →σ 1 )∧(σ 2 →σ 2 ) (∧I)
but is untypable using a naïve corresponding rule à la Church for the introduction of intersection-types [Hindley (1984)].

x:

σ 1 ∧ x : σ 1 ∧ λx:σ 1 .x : σ 1 →σ 1 (→I) x:σ 2 ∧ x : σ 2 ∧ λx:σ 2 .x : σ 2 →σ 2 (→I)
∧ λx: ? .x : (σ 1 →σ 1 )∧(σ 2 →σ 2 )

(∧I)
By the Curry-Howard isomorphism [Howard (1980)], a λ-term must record the shape of its type-derivation. A standard proof decoration would give rise to a language which is a λ-calculus extended with a pair construction. For example, according to [Ronchi Della Rocca (2002)], the previous proof would be decorated in the following way:

x:σ 1 ∧ x : σ 1 ∧ λx:σ 1 .x : σ 1 →σ 1 (→I) x:σ 2 ∧ x : σ 2 ∧ λx:σ 2 .x : σ 2 →σ 2 (→I) ∧ < λx:σ 1 .x, λx:σ 2 .x >: (σ 1 →σ 1 )∧(σ 2 →σ 2 ) (∧I)
The resulting language has a huge syntax, since the pairing construct can be applied only on terms, which can be different, but their below untyped versions must be identical. An example in the literature of λ-calculus typed à la Church with intersection types, where the syntax is exactly the classical one, but for types, is the language Forsythe in [Reynolds (1996)]. But it is incomplete, in the sense that the resulting typed system has less typability power than the type assignment one. In fact, in the Reynolds syntax, assuming that a term M has type τ under the assumption that the variable x has any one of the types σ i (1≤i≤n), we can form the typed term:

λx:σ 1 |σ 2 |...|σ n .M
having types (σ i →τ ) for 1≤i≤n, and all types derived from these by applying intersection introduction, intersection elimination and subtyping relations. So, for example, there is not a typed version of λx.λy.x, giving it the type ρ = (σ→(σ→σ)) ∧ (τ →(τ →τ )), where σ and τ are uncomparable. In fact, according to the Forsythe syntax, we can form the two terms, namely λx:σ|τ.λy:σ.x, having types σ→(σ→σ) and τ →(σ→τ ), and λx:σ|τ.λy:τ.x, having types τ →(τ →τ ) and σ→(τ →σ), but there is not a term relating the types of x and y in the desired way.

(this example has been taken from [START_REF] Wells | Branching Types[END_REF]]). Moreover, Forsythe appear something in between a typed and a type assignment calculus, since terms do not have unique types.

The problem is, as the skilled reader can understand, the presence of non syntaxdirected rules that disconnect the λ-term from its type-derivation (hence losing the Curry-Howard correspondence). It is important to point out that this problem does not depend on the chosen intersection-type assignment system; indeed, not one of the intersection type assignment systems presented in the literature is completely syntax directed (and not-even it cannot be!)

Our goal is to build a λ-calculus à la Church, and related intersection-type system Λ t ∧ , whose syntax is, as far as possible, similar to other typed λ-calculi. We want to design this calculus through a typed system, building typed terms together with their type, such that the typed system and the type assignment system Λ u ∧ are related by the standard path designed in [START_REF] Giannini | Type Inference: Some Results, Some Problems[END_REF], Liquori (1996), van Bakel et al. (1997)]. For this system, we are interested to catch as much as possible properties from the following list:

Desiderata

(1) typed and type assignment derivations are isomorphic, under the assumption that they share the same type syntax. I.e., the application of an erasing function E on all typed terms and contexts (in a typed derivation judgment) produces a derivable type assignment derivation with the same structure, and every type assignment derivation is obtained from a typed one with the same structure by applying the same erasure E. Such a kind of isomorphism has been studied in [van Bakel et al. (1997)]. Moreover, we want that the intersection calculus à la Church inherits all the properties of intersection type assignment à la Curry, namely:

(2) subject reduction;

(3) strong normalization of typable terms; plus the following ones:

(4) unicity of typing;

(5) decidability of type reconstruction and of type checking.

In order to find a solution to this challenge, we designed a calculus, whose terms are composed by two parts, carrying out the computational and logical information respectively. The first component (the marked-term) is a simply typed λ-term, but types are variable-marks, i.e., natural numbers representing store locations. The second component (the proof-term) records both the associations between variable-marks and types and the structure of the derivation. The technical tool for realizing this is an unusual formulation of context, which assigning types to term-variables at a given mark/location. The calculus of proof-terms can be defined per se, as decoration of the implicative and conjunctive fragment of intuitionistic logic; it codifies a set of proofs that is strictly bigger than these corresponding to intersection-type derivations (see [Ronchi Della Rocca and Roversi (2001)]).

As example, the typed identity with type

(σ 1 →σ 1 ) ∧ (σ 2 →σ 2 )
can be written in our proposal as the term

(λx:0.x)@(λ0:σ 1 .0)∧(λ0:σ 2 .0)
where 0 is a mark, and (λ0:σ 1 .0)∧(λ0:σ 2 .0) is the logical content of λx:0.x. The typed λ-calculus so obtained satisfies all the above requirements. As a nice consequence of these choices, we get decidability of the type reconstruction and type checking, both being also easy to define.

There are other proposals in the literature for a λ-calculus typed with intersection types. We already have cited Forsythe [Reynolds (1996)], which is not complete, as well as the language proposed in [START_REF] Pierce | Simple Type-theoretic Foundations for Object-oriented Programming[END_REF]]. The languages proposed in [START_REF] Capitani | Hyperformulae, Parallel Deductions and Intersection-Types[END_REF]], [START_REF] Wells | A Calculus with Polymorphic and Polyvariant Flow Types[END_REF]], and [START_REF] Wells | Branching Types[END_REF]] have been designed with other purposes, and they do not satisfy requirement 1. The language in [Ronchi Della Rocca (2002)] has been designed for logical purposes in order to satisfy the requirement 1, but its syntax and operational semantics are unsatisfying, from our point of view.

The paper is organized as follows: Section 2 presents the logical calculus. Section 3 shows the whole intersection-typed λ-calculus. Section 4 contains some examples, while Section 5 lists the metatheory and the type checking/type reconstruction algorithms. In Section 6 the soundness between Λ t ∧ and Λ u ∧ is proved. Conclusions and final remarks end the paper.

The Proof-calculus ΛP

The syntax of intersection-types is that of the formulas of the implicative and conjunctive fragment of the intuitionistic logic (denoted by L ∧ → ), where the logical connectives "→" and "∧" denote the implication and the conjunction. Unfortunately, the intersection-type assignment system Λ u ∧ does not correspond, in the Curry-Howard sense, to this logic [Hindley (1984)], because of the "anomalous" decoration of the rules dealing with conjunction.

In what follows, we present a typed λ-calculus, obtained by decorating the proof of such a logic. The main peculiarity of this calculus is that it is defined on another categories of variables called variable-marks; the calculus will be used to record the structure of an intersection derivation, though an association between variablemarks and types.

Syntax of ΛP. We start with some useful definitions.

Definition 2.1

(1) Variable-marks (denoted by ι) range over Nat;

(2) Intersection-types are defined as follows:

σ ::= α | σ→σ | σ ∧ σ
where α ranges over a denumerable set V of constants;

(3) Proof-contexts are finite associations between variable-marks and types, and they are defined by the following grammar:

G ::= | G, ι:σ
(4) Pseudo-proof-trees are labeled unary/binary trees defined as follows:

∆ ::= ι | λι:σ.∆ | ∆ ∆ | ∆∧∆ | ∆ | ∆ (5) The set Fv(∆) of the variable-marks in a pseudo-proof-tree ∆ is Fv(ι) = {ι} Fv(λι:σ.∆) = Fv(∆) \ {ι} Fv(∆ ) = Fv(∆) Fv(∆ 1 ∆ 2 ) = Fv(∆ 1 ) ∪ Fv(∆ 2 ) Fv( ∆) = Fv(∆) Fv(∆ 1 ∧∆ 2 ) = Fv(∆ 1 ) ∪ Fv(∆ 2 ) A variable-mark is bound in ∆ if it is not free in ∆.
The Proof-calculus ΛP.

Let G = {ι 1 :σ 1 , . . . , ι n :σ n } (i = j implies ι i ≡ ι j ), and G, ι:σ = G ∪ {ι:σ}

ι:σ ∈ G G P ι : σ (Var) G, ι:σ 1 P ∆ : σ 2 G P λι:σ 1 .∆ : σ 1 →σ 2 (→I) G P ∆ 1 : σ 1 →σ 2 G P ∆ 2 : σ 1 G P ∆ 1 ∆ 2 : σ 2 (→E) G P ∆ 1 : σ 1 G P ∆ 2 : σ 2 G P ∆ 1 ∧∆ 2 : σ 1 ∧ σ 2 (∧I) G P ∆ : σ 1 ∧ σ 2 G P ∆ : σ 1 (∧E L ) G P ∆ : σ 1 ∧ σ 2 G P ∆ : σ 2 (∧E R )
Figure 3. The Proof-calculus ΛP.

Type System for ΛP. The system proves judgments of the shape:

G P ∆ : σ
where G is a proof-context, ∆ is a pseudo-proof-tree, and σ is a type. The pseudoproof-tree ∆ is a legal proof-tree if there are G and σ such that G P ∆ : σ. The rules of the system, obtained by decorating the rules of the logic L ∧ → , are showed in Figure 2. Note that ΛP is just an unusual syntax for the simply typed λ-calculus with pairs, which can be seen, via the Curry-Howard isomorphism, as a decoration of L ∧ → .

Reduction Semantics of ΛP. Being ΛP a calculus isomorphic to the typed λcalculus with pairs, its reduction rules are the well known ones:

(λι:σ.∆ 1 ) ∆ 2 → β ∆ 1 [∆ 2 /ι] (∆ 1 ∧∆ 2 ) → π 1 ∆ 1 (∆ 1 ∧∆ 2 ) → π 2 ∆ 2
By abuse of notation, → ι , → π 1 , → π 2 will denote the contextual closure of the above rules.

As usual, the ΛP calculus works modulo α-conversion, as the symmetric, transitive, reflexive, and contextual closure of the following rule:

λι 1 :σ.∆ → α λι 2 :σ.∆[ι 2 /ι 1 ]
where ι 2 is fresh

The following result holds:

Fact 1 (Strong Normalization of ΛP) ΛP is strongly normalizing.

3 The Intersection-Typed Calculus Λ t

∧

The key idea in the design of the intersection-typed system is to split the term into two parts, carrying out the computational and the logical information respectively. Namely, the first one is a term of a typed λ-calculus, while the second one is a proofterm (belonging to the language ΛP introduced in the previous section) describing the shape of the type derivation. The technical tool for connecting the two parts is an unusual formulation of contexts. In fact, a context associates to a variable both a variable-mark and a type, such that different variables are associated to different variable-marks.

This novel formulation of contexts allows to remember, in rule (→I), just the variable-mark, the corresponding type being stored in the proof-tree, built by the system in parallel with the typed term. In this way the underlying term is de facto a term of the classical untyped λ-calculus. Since the proof-tree describes the structure of the type-derivation, we also obtain the decidability of type reconstruction and type checking.

Syntax.

Definition 3.1

(1) Contexts are finite associations between variables and types at a given variable-mark, such that each variable and each variable-mark occur at least once in it. They are defined as follows:

Γ ::= | Γ, x@ι:σ

(2) Marked-terms are defined as follows:

M ::= x | λx:ι.M | M M
(3) A pseudo-term of Λ t ∧ has the shape M @∆, where M is a marked-term and ∆ is a proof-tree;

In what follows, the symbol ≡ denotes the syntactic equality for marked-terms, types, contexts, variable-marks and proof-trees, respectively.

Definition 3.2 (Fv)

(1) The set of free-variables of a marked-term is defined as follows: (2) The set of free variables and of free variable-marks of a pseudo term is defined as follows:

Fv(x) = {x} Fv((λx:ι.M )) = Fv(M ) \ {x} Fv((M N )) = Fv(M ) ∪ Fv(N )
Fv(M @∆) = Fv(M ) ∪ Fv(∆)
Type System . The type judgments of the intersection-typed calculus Λ t ∧ have the shape:

Γ M @∆ : σ
where Γ is a context, M is a marked-term, and ∆ is a proof-tree. Intuitively: in the judgment, the type-context Γ assigns intersection-types to the free-variables of M annotated by variable-marks; if Γ M @∆ : σ, then we say that M @∆ is a term of Λ t ∧ .

The proof-tree keeps track of the type of the used mark together with a trace of the skeleton of the derivation tree. The proof-tree ∆ plays the role of a road map to backtrack (i.e. roll back) the derivation tree. The typing rules are presented in Figure 3. Some comments are in order:

• (Var) gives types to free-variables at a given mark;

• (→I) is a quasi-classical abstraction rule, but it records in the term only the variable-mark associated to the abstracted variable; the proof-tree ∆ evolves in a new proof-tree enriched with the binding for the mark ι; • (→E) is a quasi-classical application rule; observe that the two type-stores of the premises become sub proof-trees in the conclusion (the hidden application operator being the root); • (∧I) is the most important rule; given two judgments for M assigning types σ 1 and type σ 2 , in the same context Γ but with different proof-trees ∆ 1 , and ∆ 2 , we can assign the intersection-type σ 1 ∧ σ 2 to M in the context Γ but in the new proof-tree ∆ 1 ∧∆ 2 . At this point the marked-term M loses the one-to-one correspondence with its proof. Luckily, the new proof-tree keeps track of the derivation and guarantees unicity of typing; • (∧E L ), and (∧E R ) are the two standard rules that eliminate intersection-types.

Also in this case the marked-term M loses the one-to-one correspondence with its (logical) proof, but the proof is memorized by the proof-tree, thanks to the two place-holders and , indicating the applied rule.

Reduction semantics. For a given term M @∆, the computational part (M ) and the logical part (∆) grow up together while they are built through application of rules (Var), (→I), and (→E), but they get disconnected when we apply (∧{I, E L , E R }) rules (that changes the ∆ but not the M ). This disconnection is "logged" in the ∆ via occurrences of operators ∧, , and .

As such:

• by (∧I) and from M @∆ 1 and M @∆ 2 , we get M @(∆ 1 ∧∆ 2 ). So ∆ 1 and ∆ 2 describe two different derivations sharing the same marked term. As a consequence, to a redex in M will correspond some redexes in ∆ 1 and ∆ 2 , that need to be performed in parallel with the redex in M in order to preserve the correct syntax of the term; • by (∧E L ) or (∧E R ) and from M @∆, we get M @( ∆) or M @(∆ ); so each reduction in M implies some reductions inside the wrapped ∆.

In order to correctly identify the reductions that need to be performed in parallel in the two parts of the term, we will define the notion of overlapping. Namely a redex is defining taking into account the surrounding context.

Definition 3.3 (Reduction Semantics)

(Contexts and Overlapping) The marked-term contexts C{ } and proof-term context D{ } and multi-hole proof-term context E{ } are defined as follows:

C{ } ::= { } | C{ } M | M C{ } | λx:ι.C{ } D{ } ::= { } | D{ } ∆ | ∆ D{ } | λι:σ.D{ } | D{ } | D{ } | D{ } ∧ ∆ | ∆ ∧ D{ } E{ } ::= { } | E{ } ∆ | ∆ E{ } | λι:σ.E{ } | E{ } | E{ } | E{ } ∧ E{ }
Note that, while C{ } and D{ } are contexts with exactly one hole, the context E{ } can have more than one hole. Let E{∆ i } i∈I denote a proof-context where the i-th hole has been filled by ∆ i , for i ∈ I. The notion of overlapping between marked-terms and proof-terms, denoted by C{ } E{ } is defined by induction on E{ } as follows:

{ } { } C{ } E{ } C{ } M E{ } ∆ C{ } E{ } M C{ } ∆ E{ } C{ } E{ } λx:ι.C{ } λι:σ.E{ } C{ } E{ } C{ } E{ } C{ } E{ } C{ } E{ } C{ } E 1 { } C{ } E 2 { } C{ } E 1 { } ∧ E 2 { }
(→) reduction The (→) reduction rule is the union of the three reduction rules defines as follows:

if C{ } E{ } then C{(λx:ι.M ) N } @ E{(λι:σ i .∆ i ) ∆ i } i∈I → β C{M [N/x]} @ E{∆ i [∆ i /ι]} i∈I M @ D{ (∆ 1 ∧∆ 2 )} → π 1 M @ D{∆ 1 } M @ D{(∆ 1 ∧∆ 2 ) } → π 2 M @ D{∆ 2 }
Note that the hypothesis of C{ } E{ } in the definition of the → β -reduction is essential in order to recover, for each β-redex in the marked term, the corresponding β-redexes, wrapped in the proof-term; those redexes must fired in parallel, in order to do not create exotic typed terms that would not have an untyped counterpart in the original system à la Curry.

α-conversion on well formed terms can be formally defined as follows:

Definition 3.4 (α-conversion) (λx:ι.M ) @ ∆ → α (λy:ι.M [y/x]) @ ∆ y fresh in M M @ (λι 1 :σ.∆) → α M [ι 2 /ι 1 ] @ (λι 2 :σ.∆[ι 2 /ι 1 ]) ι 2 fresh in ∆ 4 Examples
We show two notorious examples in order to justify how type derivations can be built for Λ t ∧ proof-terms starting for the corresponding untyped λ-terms à la Curry, and two further examples in order to illustrate the reduction rules of Λ t ∧ .

Example 4.1 (Classical polymorphic identity)

We show a derivation for a typed term corresponding to the typing in Λ u ∧ : ∧ λx.x : (σ 1 →σ 1 ) ∧ (σ 2 →σ 2 ).

x@0:σ 1 x@0 : σ 1 (Var) (λx:0.x)@(λ0:σ 1 .0) : σ 1 →σ 1 (→I)

x@0:σ 2 x@0 : σ 2 (Var) (λx:0.x)@(λ0:σ 2 .0) : σ 2 →σ 2 (→I) (λx:0.x)@((λ0:σ 1 .0)∧(λ0:σ 2 .0)) : (σ 1 →σ 1 )∧(σ 2 →σ 2 )

(∧I) Example 4.2 (Polymorphic self-application) Let σ 2 = (σ 1 →σ 1 ) ∧ σ 1 . We show a term in Λ t ∧ corresponding to the typing of Λ u ∧ : ∧ λx.xx : σ 2 →σ 1 .
x@0:σ 2 x@0 : σ 2 (Var)

x@0:σ 2 x@( 0) : σ 1 →σ 1 (∧E L )

x:0:σ 2 x@0 : σ 2 (Var)

x:0:σ 2 x@(0 ) : σ 1 (∧E R )

x@0:σ 2 (x x)@( 0) (0 ) : σ 1 (→E) (λx:0.x x)@(λ0:σ 2 .( 0

) (0 )) : σ 2 →σ 1 (→I)
Note how the proof-tree memorizes exactly the skeleton of the type-derivation.

Example 4.3 (Reduction in Λ t ∧ ) A term in Λ t
∧ corresponding to the following typing in Λ u ∧ : y:σ 1 ∧ σ 2 ∧ (λx.x) y : σ 1 ∧ σ 2 can be constructed in the following way:

D 1 D 2 y@0:σ 1 ∧ σ 2 (λx:1.x) y@((λ1:σ 1 .1) 0) ∧ ((λ1:σ 2 .1) 0 ) : σ 1 ∧ σ 2 (∧I)
where D 1 is:

y@0:σ 1 ∧ σ 2 , x@1:σ 1 x@1 : σ 1 (Var) y@0:σ 1 ∧ σ 2 (λx:1.x)@(λ1:σ 1 .1) : σ 1 →σ 1 (→I) y@0:σ 1 ∧ σ 2 y@0 : σ 1 ∧ σ 2 (Var) y@0:σ 1 ∧ σ 2 y@ 0 : σ 1 (∧E L )
y@0:σ 1 ∧ σ 2 (λx:1.x) y@((λ1:σ 1 .1) 0) :

σ 1 (→E)
and D 2 is:

y@0:σ 1 ∧ σ 2 , x@1:σ 2 x@1 : σ 2 (Var)
y@0:σ 1 ∧ σ 2 (λx:1.x)@(λ1:σ 2 .1) : σ 2 →σ 2 (→I) y@0:σ 1 ∧ σ 2 y@0 :

σ 1 ∧ σ 2 (Var) y@0:σ 1 ∧ σ 2 y@0 : σ 2 (∧E R ) y@0:σ 1 ∧ σ 2 (λx:1.x) y@((λ1:σ 2 .1) 0 ) : σ 2 (→E)
This term can be written as: C{(λx:1.x) y}@E{(λ1:σ 1 .1) 0}{(λ1:σ 2 .1) 0 }, where the two overlapping contexts are respectively: C{ } ≡ { } and E{ } ≡ { } ∧ { }, so this term β-reduces to: y@ 0 ∧ 0 which is a well formed term, in fact it can be built in the following way:

y@0:σ 1 ∧ σ 2 y@0 : σ 1 ∧ σ 2 (Var) y@0:σ 1 ∧ σ 2 y@ 0 : σ 1 (∧E L ) y@0:σ 1 ∧ σ 2 y@0 : σ 1 ∧ σ 2 (Var) y@0:σ 1 ∧ σ 2 y@0 : σ 2 (∧E R ) y@0:σ 1 ∧ σ 2 y@ 0 ∧ 0 : σ 1 ∧ σ 2 (∧I)
Note that, if only one of the redexes in the proof-term would be reduced, then the resulting term will be not well formed. (λx:0.x x) ((λy:1.y) (λy:2.y))@(∆

1 ∆ 2 ) : σ ∧ τ Let δ = ((σ→σ) ∧ σ) ∧ ((τ →τ ) ∧ τ )
and

∆ 1 = λ0 : δ.∆ 3 ∆ 3 = ∆ 4 ∧ ∆ 5 ∆ 4 = ∆ 6 ∆ 7 ∆ 5 = ∆ 6 ∆ 7 ∆ 6 = ( 0) ∆ 7 = ( 0) ∆ 6 = (0 ) ∆ 7 = (0 ) ∆ 2 = ∆ 8 ∧ ∆ 9 ∆ 8 = ∆ 10 ∧ ∆ 11 ∆ 10 = ∆ 12 ∆ 13 ∆ 12 = λ1:σ 2 .2 ∆ 13 = λ2:σ.2 ∆ 11 = ∆ 14 ∆ 15 ∆ 14 = λ1:σ.1 ∆ 15 = λ2:α.2 ∆ 9 = ∆ 10 ∧ ∆ 11 ∆ 10 = ∆ 12 ∆ 13 ∆ 12 = λ1:τ 2 .1 ∆ 13 = λ2:τ.2 ∆ 11 = ∆ 14 ∆ 15 ∆ 14 = λ1:τ.1 ∆ 15 = λ2:β.1
Reducing the top-level β-redex (corresponding to the two overlapping contexts C{ } ≡ E{ } ≡ { }), leads to the term ((λy:1.y) (λy:2.y)) ((λy:1.y) (λy:2.y))@(( ( ∆ 2 )

π-red ) (( ∆ 2 ) ) π-red )∧(( (∆ 2 ) π-red ) ((∆ 2 ) π-red
))

Reducing all the four π-redexes leads to the following term ((λy:1.y) (λy:2.y)) ((λy:1.y) (λy:2.y))@(∆ 10 ∆ 11 ) ∧ (∆ 10 ∆ 11 )

that can be seen both as:

C{(λy:1.y) (λy:2.y)}@E{∆ 10 }{∆ 10 } and C{(λy:1.y) (λy:2.y)}@E{∆ 11 }{∆ 11 } by considering either the contexts C{ } ≡ { }((λy:1.y) (λy:2.y)) and E{ } ≡ { } ∆ 11 ∧ { } ∆ 11 or C{ } ≡ ((λy:1.y) (λy:2.y)){ } and E{ } ≡ ∆ 10 { } ∧ ∆ 10 { }.

By making the first choice, we obtain:

(λy:2.y) ((λy:1.y) (λy:2.y))@(∆ 13 ∆ 11 ) ∧ (∆ 13 ∆ 11 )

where the two overlapping contexts are: C{ } ≡ (λy:2.y) { } and E{ } ≡ (∆ 13 { }) ∧ (∆ 13 { }).

Reducing this β-redex leads to the following term (λy:2.y) (λy:2.y)@(∆ 13 ∆ 15 ) ∧ (∆ 13 ∆ 15 )

where the overlapping contexts C{ } ≡ { } and E{ } ≡ { } ∧ { } individuate the last β-redex. Reducing this β-redex we obtain the term in normal form (λy:2.y)@∆ 15 ∧ ∆ 15

5 The Isomorphism between Λ u ∧ and Λ t

∧

In this section we prove that the type system for Λ t ∧ is isomorphic to the classical system ∧ for Λ u ∧ of Coppo and Dezani [START_REF] Coppo | An Extension of the Basic Functionality Theory for the λ-calculus[END_REF]]. The isomorphism is given for a customization of the general definition of isomorphism given in [START_REF] Giannini | Type Inference: Some Results, Some Problems[END_REF], Liquori (1996), van Bakel et al. (1997)], to the case of intersection-types and proof-trees.

From the logical point of view, the existence of an isomorphism means that there is a one-to-one correspondence between the judgments that can be proved in the two systems, and the derivations correspond with each other rule by rule. In what follows, and with a little abuse of notation, marked-terms and untyped terms of the λ-calculus will be ranged over by M, N, . . ., the difference between marked-terms and untyped-terms being clear from the context (i.e. the judgment to be proved).

Definition 5.1 (Church vs. Curry)

(1) The type-erasing function E : Λ t ∧ ⇒ Λ is inductively defined on terms as follows:

E(x@_) = x E((λx:ι.M )@_) = λx.E(M @_) E((M N )@_) = E(M @_) E(N @_)
E can be extended to contexts in the following way:

E( ) = E(Γ, x@ι:σ) = E(Γ), x:σ (2) Let DerΛ u
∧ and DerΛ t ∧ be the sets of all (un)typed derivations in ∧ and , respectively. Let D, D 1 , . . . , D n range over (un)typed derivations. where ren is a is a simple function renaming the free occurrences of variable-marks;

Systems ∧ G x:σ ∈ E E ∧ x : σ (Var) =      x@ι:σ ∈ Γ Γ x@ι : σ (Var) E(Γ) = E ι is fresh G D : E, x:σ 1 ∧ M : σ 2 E ∧ λx.M : σ 1 →σ 2 (→I) =        G(D) : Γ, x@ι:σ 1 M @∆ : σ 2 Γ (λx:ι.M )@(λι:σ 1 .∆) : σ 1 →σ 2 (→I) E(Γ, x@ι:σ 1 ) = E, x:σ 1 & E(M @∆) = M G      D 1 : E ∧ M : σ 1 →σ 2 D 2 : E ∧ N : σ 1 E ∧ M N : σ 2 (→E)      =                G(D 1 ) : Γ M @∆ 1 : σ 1 →σ 2 G(D 2 ) : Γ N @∆ 2 : σ 1 Γ (M N )@(∆ 1 ∆ 2 ) : σ 2 (→E) E(Γ) = E & E(M @∆ 1 ) = M & E(N @∆ 2 ) = N G      D 1 : E ∧ M : σ 1 D 2 : E ∧ M : σ 2 E ∧ M : σ 1 ∧ σ 2 (∧I)      =                G(D 1 ) : Γ M @∆ 1 : σ 1 G(D 2 ) : Γ M @∆ 2 : σ 2 Γ M @(∆ 1 ∧∆ 2 ) : σ 1 ∧ σ 2 (∧I) E(Γ) = E & E(M @(∆ 1 ∧∆ 2 )) = M G D : E ∧ M : σ 1 ∧ σ 2 E ∧ M : σ 1 (∧E L ) =        G(D) : Γ M @∆ : σ 1 ∧ σ 2 Γ M @( ∆) : σ 1 (∧E L ) E(Γ) = E & E(M @∆) = M G D : E ∧ M : σ 1 ∧ σ 2 E ∧ M : σ 2 (∧E R ) =        G(D) : Γ M @∆ : σ 1 ∧ σ 2 Γ M @(∆ ) : σ 2 (∧E R ) E(Γ) = E & E(M @∆) = M
(d) (Faithfulness) Both F and G preserve the structure of derivations, (i.e., the tree obtained from a derivation by erasing all judgments, but not the names of the rules).

F x@ι:σ ∈ Γ Γ x@ι : σ (Var) =      x:σ ∈ E E ∧ x : σ (Var) E(Γ) = E F Γ, x@ι:σ 1 M @∆ : σ 2 (→I)
Γ (λx:ι.M )@(λι:σ 1 .∆) : Function F and G are described in Figures 6 and5.

σ 1 →σ 2 =        F(D) : E, x:σ 1 ∧ M : σ 2 E ∧ λx.M : σ 1 →σ 2 (→I) E(Γ, x@ι:σ 1 ) = E, x:σ 1 & E(M @∆) = M F      D 1 : Γ M @∆ 1 : σ 1 →σ 2 D 2 : Γ N @∆ 2 : σ 1 Γ (M N )@(∆ 1 ∆ 2 ) : σ 2 (→E)      =                F(D 1 ) : E ∧ M : σ 1 →σ 2 F(D 2 ) : E ∧ N : σ 1 E ∧ M N : σ 2 (→E) E(Γ) = E & E(M @∆ 1 ) = M & E(N @∆ 2 ) = N F      D 1 : Γ M @∆ 1 : σ 1 D 2 : Γ M @∆ 2 : σ 2 Γ M @(∆ 1 ∧∆ 2 ) : σ 1 ∧ σ 2 (∧I)      =                F(D 1 ) : E ∧ M : σ 1 F(D 2 ) : E ∧ M : σ 2 E ∧ M : σ 1 ∧ σ 2 (∧I) E(Γ) = E & E(M @(∆ 1 ∧∆ 2 )) = M F D : Γ M @∆ : σ 1 ∧ σ 2 Γ M @( ∆) : σ 1 (∧E L ) =        F(D) : E ∧ M : σ 1 ∧ σ 2 E ∧ M : σ 1 (∧E L ) E(Γ) = E & E(M @∆) = M F D : Γ M @∆ : σ 1 ∧ σ 2 Γ M @(∆ ) : σ 2 (∧E R ) =        F(D) : E ∧ M : σ 1 ∧ σ 2 E ∧ M : σ 2 (∧E R ) E(Γ) = E & E(M @∆) = M
Notice that the definition of isomorphism expresses more than just soundness and completeness of E. Indeed, soundness and completeness imply an isomorphism between the judgments of the two systems, but they do not imply necessarily a one-one correspondence between derivations. Figure 7 shows the various functions between typed and untyped systems of λ-calculi that realize the above relations between typed and untyped judgments and derivations.

Theorem 5.1 (Isomorphism) The systems and ∧ are isomorphic.

Proof. Soundness can be proved by induction on the structure of the derivation in the Λ t ∧ . Completeness can be proved by induction on the structure of the derivation in Λ u ∧ , using soundness. Inversion can be proved by induction on the structure of both the derivations, using the soundness and completeness result. Faithfulness is

G E(Γ) ∧ E(M @∆) : σ Γ M @∆ : σ - E E -1 F - L L L L L L L L L L L L L L L L L L L L L L Figure 7. Functions between Λ t
∧ s and Λ u ∧ s Judgments and Derivations.

immediate. 2

We can also explore the relationship between Λ t ∧ and the proof calculus ΛP by defining an erasure function E : Λ t ∧ ⇒ ΛP as follows:

E (_@∆) = ∆
The function E can be extended naturally to a function from contexts to proofcontexts:

E ( ) = E (Γ, x@ι:σ) = E (Γ), ι:σ
Then it is easy to define a function F : Der Λ t ∧ ⇒ Der ΛP such that D : Γ M @∆ : σ implies F (D) : E (Γ) P ∆ : σ. F consists in just applying E to all contexts and subjects of the derivation. Note that Λ t ∧ and ΛP are not isomorphic; for example, the statement ι 1 :σ P (λι 2 :τ.ι 2 ) ∧ ι 1 : (τ →τ ) ∧ σ in ΛP has no a corresponding counterpart in Λ t ∧ .

6 Metatheory of Λ t

∧

In this section we will prove properties [3-6] listed in the introduction. First we need to prove the Generation and Substitution lemmas.

Lemma 6.1 (Generation)

(1) If Γ M @∆ 1 ∧ ∆ 2 : σ, then σ ≡ σ 1 ∧ σ 2 and Γ M @∆ 1 : σ 1 and Γ M @∆ 2 : σ 2 ;

(2) If Γ M @ ∆ : σ then there exists τ , such that Γ M @∆ : σ ∧ τ ;

(3) If Γ M @∆ : σ then there exists τ , such that Γ M @∆ : τ ∧ σ; (4) If Γ x@ι : σ, then x@ι : σ ∈ Γ;

(5) If Γ (λx:ι.M )@(λι:σ 1 .∆) : σ 1 →σ 2 , then Γ, x@ι:σ 1 M @∆ : σ 2 ;

The further requirement we asked for is the unicity of typing. In general, for typed languages, typing is unique modulo α-conversion, i.e., modulo renaming of boundvariables.

Theorem 6.3 (Unicity of Typing of Λ t ∧ ) If D 1 : Γ M @∆ : σ 1 , and D 2 : Γ M @∆ : σ 2 , and M @∆ = α M @∆ , then σ 1 ≡ σ 2 , and D 1 ≡ D 2 .

Proof. By easy induction on the structure of the derivation D 1 . 2 We can finish this section by presenting the type reconstruction and the type checking algorithms for Λ t ∧ in Figure 6, and by proving that they are decidable. The soundness and completeness proofs follow. Theorem 6.4 (Type Reconstruction for Λ t ∧ )

(Completeness) By induction on the derivation of Γ M @∆ : σ.

(Var) Then M ≡ x and ∆ ≡ ι. By match-case number 4 we get Type ∧ (x, ι@σ) = σ. (→I) Then M ≡ λx:ι.M 1 and ∆ ≡ λι:σ 1 .∆ 1 and σ ≡ σ 1 →σ 2 . By induction we get Type ∧ ((Γ, x@ι:σ 1 ), M 1 @∆ 1 ) = σ 2 , and by match-case 5 we get Type ∧ ((λx:ι.M 1 )@(λι:σ 1 .∆ 1 )) = σ 1 →σ 2 . (→E) Then M ≡ M 1 M 2 and ∆ ≡ ∆ 1 ∆ 2 and σ ≡ σ 2 . By induction we get Type ∧ (Γ, M 1 @∆ 1 ) = σ 1 →σ 2 and Type ∧ (Γ, M 2 @∆ 2 ) = σ 1 , and by match-case 6 we get Type ∧ ((M 1 M 2 )@(∆ 1 ∆ 2 )) = σ 2 . (∧I) Then ∆ ≡ ∆ 1 ∧∆ 2 and σ ≡ σ 1 ∧σ 2 . By induction we get Type ∧ (M, ∆ 1 ) = σ 1 and Type ∧ (M, ∆ 2 ) = σ 2 , and by match-case 3 we get Type ∧ (M, (∆ 1 ∧∆ 2 )) = σ 1 ∧ σ 2 . (∧E L ) Then ∆ ≡ ∆ 1 and σ ≡ σ 1 . By induction we get Type ∧ (Γ, M @∆ 1 ) = σ 1 ∧ σ 2 , and by match-case 1 we get Type ∧ (M, ∆ 1 ) = σ 1 . (∧E R ) Then ∆ ≡ ∆ 1 and σ ≡ σ 2 . By induction we get Type ∧ (Γ, M @∆ 1 ) = σ 1 ∧ σ 2 , and by match-case 2 we get Type ∧ (M, ∆ 1 ) = σ 2 .

2 Theorem 6.5 (Type Checking for Λ t ∧ ) Γ M @∆ : σ, if and only if Typecheck ∧ (Γ, M @∆, σ) = true.

Proof. The ⇒ part can be proved using completeness of the type reconstruction algorithm (Theorem 6.4), while the ⇐ part can be proved using soundness of the type reconstruction algorithm. 2 Theorem 6.6 (Judgment Decidability) If is decidable whether the Λ t ∧ judgment Γ M @∆ : σ is derivable.

Proof. Routine. 2

Conclusions

We studied in this paper the problem of designing a λ-calculus à la Church corresponding to the intersection-type assignment system. In particular, we asked for a typed language such that its relationship with the intersection-type assignment system enjoys all the standard requirements we posed in [START_REF] Giannini | Type Inference: Some Results, Some Problems[END_REF], Liquori (1996),van Bakel et al. (1997)]. Examples of such "good" correspondences are respectively the Church and Curry version of the simple typed λ-calculus (if written using the same symbols), and the typed and type assignment version of the second order λ-calculus [Girard (1986), Leivant (1983)]. We succeed in designing a calculus based essentially on two basic and simple ideas: an imperative-like notion of typing, when types are assigned to variables "at a given mark", and a proofcalculus, describing intersection-type derivations, whose terms are used as prooftrees for the terms of the target calculus.

A reader interested in particular in programming applications could object that the used language is far for being "usable", since the user needs to specify not only the typed terms, but also their proof-trees, which are encoding of type-derivations.

The answer can be twofold. From a programming languages point of view, in every typed language the user, in order to write explicitly the type of a term, in some sense needs to "guess" the correct type-derivation assigning that type to the term itself.

Here obviously the type-derivations are more difficult than in the simple typed case. But if we think, for example, to Girard's Second Order Typed λ-calculus [Girard (1986)], in order to write the term Λβ.Λγ.λx:(∀α.α). x (β→γ) of type ∀β.∀γ.(∀α.α)→(β→γ)

one needs to know exactly how and the rules for introducing and eliminating the universal quantifier work. However, we think that the production of an usable language is not the only justification for the problem we studied, as it was especially for [Reynolds (1996), [START_REF] Pierce | Simple Type-theoretic Foundations for Object-oriented Programming[END_REF]]. The relationship between typed and type assignment systems is an important theoretical issue, that is interesting in itself.

Figure 4 .

 4 Figure 4. The Type System for Λ t ∧ .

  Example 4.4 (A complete reduction) Consider the typing in Λ u ∧ ∧ (λx.x x) ((λy.y) (λy.y)) : σ ∧ τ A corresponding term in Λ t ∧ is:

Figure 5 .

 5 Figure 5. The Function G.and are isomorphic, if and only if there exist F :DerΛ t ∧ ⇒ DerΛ u ∧ and G : DerΛ u ∧ ⇒ DerΛ t ∧ , such that: (a) (Soundness) If D : Γ M @∆ : σ, then F(D) : E(Γ) ∧ E(M @∆) : σ; (b) (Completeness) If D : E ∧ M : σ,then there exists Γ and ∆, such that G(D) : Γ M @∆ : σ, and E(Γ) ≡ E, with E(M @∆) ≡ M ;(c) (Inversion) F • G is the identity in DerΛ u ∧ , and G • F is the identity in DerΛ t ∧ , modulo uniform naming of variable-marks. I.e., G(F(Γ M @∆ : σ)) = ren(Γ) ren(M @∆) : σ

Figure 6 .

 6 Figure 6. The Function F.

x@ι:σ ∈ Γ Γ x@ι : σ(Var) Γ, x@ι:σ 1 M @∆ : σ 2 Γ (λx:ι.M )@(λι:σ 1 .∆) : σ 1 →σ 2 (→I) Γ M @∆ 1 : σ 1 →σ 2 Γ N @∆ 2 : σ 1 Γ (M N )@(∆ 1 ∆ 2 ) : σ 2 (→E) Γ M @∆ 1 : σ 1 Γ M @∆ 2 : σ 2 Γ M @(∆ 1 ∧∆ 2 ) : σ 1 ∧ σ 2 (∧I) Γ M @∆ : σ 1 ∧ σ 2 Γ M @( ∆) : σ 1 (∧E L ) Γ M @∆ : σ 1 ∧ σ 2 Γ M @(∆ ) : σ 2 (∧E R )

(Soundness) If Type ∧ (Γ, M @∆) = σ, then Γ M @∆ : σ (Completeness) If Γ M @∆ : σ, then Type ∧ (Γ, M @∆) = σ.Proof.(Soundness) By induction on the structure of (M @∆).(_@( ∆ 1 )) Then ∆ ≡ ∆ 1 and σ ≡ σ 1 . By induction, the judgment Γ M @∆ 1 : σ 1 ∧ σ 2 is derivable. Apply rule (∧E L ) to obtain a derivation for Γ M @( ∆ 1 ) : σ 1 . (_@(∆ 1 )) Then ∆ ≡ ∆ 1 and σ ≡ σ 2 . By induction, the judgment

Acknowledgment. Simona was kindly supported by QSL: Qualité et Sûrété du Logiciel, CPER, Région Lorraine, Nancy, and by INRIA; Luigi was supported by the French CNRS grant ACI Modulogic. Moreover both authors want warmly thank the two anonymous referees, for their very sharp and constructive suggestions.

(6) If Γ M N @∆ 1 ∆ 2 : σ, then there exists σ , such that Γ M @∆ 1 : σ →σ, and Γ N @∆ 2 : σ .

Proof. By induction on derivation. 2 Lemma 6.2 (Substitution) If Γ, x@ι:σ M @∆ : τ , and Γ N @∆ : σ, then Γ M [N/x]@∆[∆ /ι] : τ .

Proof. By induction on derivation. 2

We continue with subject reduction Theorem 6.1 (Subject reduction) If Γ M @∆ : σ and M @∆ → N @∆ , then Γ N @∆ : σ.

Proof. We will treat the case → is → β ; the cases → π 1 and → π 2 are easier. By definition, there are two contexts C{ } and E{ }, such that C{ } E{ }, and M @∆ ≡ C{(λx:ι.P ) Q}@E{(λι:

By induction on C{ }. Let C{ } ≡ { }. We proceed now by induction on E{ }. If E{ } ≡ { }, then, by Generation Lemma.

(5 -6) the derivation is of the shape:

Γ, x@ι:τ P @∆ : σ Γ λx:ι.P @λι:τ.∆ : τ →σ

Γ Q@∆ : τ Γ (λx:ι.P ) Q@(λι:τ.∆) ∆ : σ

Then, by Substitution Lemma, we get Γ P [Q/x]@∆[∆ /ι] : σ.

Then, by Generation Lemma.

(1), we have σ ≡ σ 1 ∧ σ 2 and Γ (λx:ι.P )

and the proof follows, by rule (∧I).

The cases for E{ } ≡ E 1 { }, or E{ } ≡ E 1 { } follow easily by induction. No other cases can apply.

For the inductive case, we will show the proof in case

By the Generation Lemma, there exists σ , such that Γ R@∆ : σ →σ, and Γ C 1 {(λx:ι.P ) Q}@E 1 {(λι: Type ∧ (Γ, M @∆)

= match (M @∆) with The strong normalization of Λ t ∧ is proved from the strong normalization of ΛP.

∧ is strongly normalizing.

Proof. Let D : Γ M @∆ : σ, and let us assume, by absurdum, that there is an infinite reduction sequence starting from M @∆, i.e.,

where A{ } is a context either of the shape C{ }, or of the shape E{ }. In the first case the reduction is a β-reduction, in the second one is a π-reduction. By applying the function F , defined at the end of Section 5, on each element of the reduction sequence, we get an infinite sequence of proof-terms

. ., such that, for all j ≥ 0, we have that

, either by a π-reduction or by a strictly positive number of β-reductions. But this is impossible, since ΛP enjoys the strong normalization property (Fact 1).

2 Γ M @∆ 1 : σ 1 ∧ σ 2 is derivable. Apply rule (∧E R ) to obtain a derivation for Γ M @(∆ 1 ) : σ 2 . (_@(∆ 1 ∧∆ 2 )) Then σ ≡ σ 1 ∧ σ 2 . By induction, the judgments Γ M @∆ 1 : σ 1 and Γ M @∆ 2 : σ 2 are derivable. Apply rule (∧I) to obtain a derivation for Γ M @(∆ 1 ∧∆ 2 ) : σ 1 ∧ σ 2 . (x@_) Then M ≡ x and ∆ ≡ ι, since the Type ∧ algorithm (that works via a classical ML-like match-case analysis) has already ruled out the cases of ∆ ∈ { ∆ 1 , ∆ 1 , ∆ 1 ∧∆ 2 }, and since the case ∆ ≡ λι:σ 1 .∆ 1 does not apply. By hypothesis we get x@ι:σ ∈ Γ. Apply rule (Var) to obtain a derivation for Γ x@ι : σ. ((λx:ι.M 1 )@(λι:σ 1 .∆ 1 )) Then M ≡ λx:ι.M 1 and ∆ ≡ λι:σ 1 .∆ 1 and σ ≡ σ 1 →σ 2 . By induction, the judgment Γ, x@ι:σ 1 M 1 @∆ 1 : σ 2 is derivable. Apply rule (→I) to obtain a derivation for Γ (λx:ι.M 1 )@(λι:σ 1 .∆ 1 ) : σ 1 →σ 2 . ((M 1 M 2 )@(∆ 1 ∆ 2 )) Then M ≡ M 1 M 2 and ∆ ≡ ∆ 1 ∆ 2 and σ ≡ σ 2 . By induction, the judgments Γ M 1 @∆ 1 : σ 1 →σ 2 and Γ M 2 @∆ 2 : σ 1 are derivable. Apply rule (→E) to obtain a derivation for Γ (M 1 M 2 )@(∆ 1 ∆ 2 ) : σ 2 . (_@_) This case does not apply since σ = false.


Aurélie Goutte
email: goutte@cebc.cnrs.fr

Christophe Barbraud

Alizée Meillère

Alice Carravieri

Paco Bustamante

Pierre Labadie

Hélène Budzinski

Karine Delord

Yves Cherel

Henri Weimerskirch

Olivier Chastel

Demographic consequences of heavy metals and persistent organic pollutants in a vulnerable long-lived bird, the wandering albatross

Keywords: capture-recapture, Diomedea exulans, mercury, polybrominated diphenyl ethers (PBDE), polychlorinated biphenyl, pesticides

niveau recherche, publiés ou non, émanant des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

Introduction

Free-living animal populations are affected by a wide range of anthropogenic pressures. Chronic exposure to metallic and organic pollutants may compromise survival and long-term fecundity, thereby leading to population decline. For instance, mercury (Hg) is a globally distributed heavy metal of particular concern for aquatic biota, because of the harmful effects of its organic form (methyl-Hg) on embryo development, neurology, immune system, physiology and behaviour [START_REF] Tan | The endocrine effects of mercury in humans and wildlife[END_REF][START_REF] Frederick | Altered pairing behaviour and reproductive success in white ibises exposed to environmentally relevant concentrations of methylmercury[END_REF][START_REF] Tartu | To breed or not to breed: endocrine response to mercury contamination by an arctic seabird[END_REF]. Another ubiquitous heavy metal, cadmium (Cd), causes irreversible renal tubular damage, leading to reduced skeletal calcium content [START_REF] Larison | Cadmium toxicity among wildlife in the Colorado Rocky Mountains[END_REF].

Persistent organic pollutants (POPs), such as organochlorine pesticides (HCB, HCH, DDE, DDD and DDT), polychlorinated biphenyls (PCBs) and brominated diphenyl ethers (BDEs), can persist in the environment for decades and trigger a suite of detrimental effects in vertebrates, including endocrine disruption, immunotoxicity, embryo mortality and behavioural impairments [START_REF] Barron | Comparative reproductive and developmental toxicology of PCBs in birds[END_REF][START_REF] Vos | Health effects of endocrine-disrupting chemicals on wildlife, with special reference to the European situation[END_REF][START_REF] Bustnes | Ecological effects of organochlorine pollutants in the Arctic: a study of the glaucous gull[END_REF].

Although toxic effects of heavy metals and POPs have been well described at the individual level and under controlled laboratory conditions, their population level effects have been virtually neglected in free-living vertebrates because of the dearth of long-term datasets.

In aquatic birds, there is no evidence of an impact of heavy metals on adult mortality [START_REF] Wayland | Survival rates and blood metal concentrations in two species of free-ranging North American sea ducks[END_REF][START_REF] Hallinger | Mercury exposure and survival in free-living tree swallows (Tachycineta bicolor)[END_REF]. In two Catharacta skua species, breeding failure in the following year, but not adult survival rate, was positively related to Hg exposure [START_REF] Goutte | Demographic responses to mercury exposure in two closely related Antarctic top predators[END_REF], as highlighted by the use of long-term datasets and multi-state mark-recapture models (MSMR [START_REF] Lebreton | Multistate recapture models: modelling incomplete individual histories[END_REF]). Concerning POPs, very high concentrations of organochlorine compounds were related to increased mortality in the glaucous gull Larus hyperboreus [START_REF] Erikstad | Persistent organic pollution in a high-Arctic top predator: sex-dependent thresholds in adult survival[END_REF], but their effects on long-term fecundity were not explored in that study.

The present study aimed to relate demographic parameters to pollutants in wandering albatrosses Diomedea exulans. The effects of Hg and Cd in red blood cells and ∑ POPs in plasma on apparent probabilities of adult survival, return to the breeding colony, breeding, hatching and fledgling, were investigated by using a MSMR approach. According to recent studies on long-lived seabirds [START_REF] Goutte | Demographic responses to mercury exposure in two closely related Antarctic top predators[END_REF][START_REF] Erikstad | Persistent organic pollution in a high-Arctic top predator: sex-dependent thresholds in adult survival[END_REF], a deleterious effect of Hg was expected on long-term breeding performances and a possible lethal effect of POPs was expected in the most contaminated wandering albatrosses. Then, population-level responses to an increase in Hg and POPs levels were assessed by establishing a life cycle for the wandering albatross and by including Hg-or POP-dependent demographic traits in the matrix population models [START_REF] Caswell | Matrix population models: constructions, analysis and interpretation[END_REF].

Despite high pollution burdens in albatrosses [START_REF] Finkelstein | Albatross species demonstrate regional differences in North Pacific marine contamination[END_REF][START_REF] Anderson | Element patterns in albatrosses and petrels: influence of trophic position, foraging range and prey type[END_REF][START_REF] Tavares | Influence of age, sex and breeding status on mercury accumulation patterns in the wandering albatross Diomedea exulans[END_REF], the effects of contaminants on demographic parameters and population growth rate are unknown. Albatrosses are among the most highly endangered of the world's birds, with 18 of 22 species considered as threatened and the remaining four species considered as near threatened [START_REF]IUCN Red List of threatened species[END_REF]. In this population of wandering albatrosses, population growth rate remained relatively stable during the 1960s (about 850 breeding pairs), before a first decline between the early 1970s and 1986, and a second decline since 2003 down to 380 breeding pairs [START_REF] Delord | Population trends in a community of large Procellariiforms of Indian Ocean: potential effects of environment and fisheries interactions[END_REF]. Causes of decline in albatross populations have been attributed to fishery bycatch, climate change and disease [START_REF] Barbraud | Effects of climate change and fisheries bycatch on Southern Ocean seabirds: a review[END_REF]. This study thus gives a new dimension to the overall picture of environmental threats in albatross populations.

Material and Methods

a) Study area and species

The study was conducted at Ile de la Possession in the Crozet Archipelago (46° S, 52° E), Southern Indian Ocean, where 300-400 pairs of wandering albatrosses nest each year. Adults return to their breeding grounds in December and females lay a single egg in late Decemberearly January. Both parents incubate alternately until hatching in March and most young are fledged in November. Up to 6% of the birds that fledged a chick bred again in the following year, and the wandering albatross is considered to be a quasi-biennial breeding species [START_REF] Barbraud | Estimating survival and reproduction in a quasibiennially breeding seabird with uncertain and unobservable states[END_REF].

Approximately 80% of birds that failed to breed in the previous year engage in another breeding attempt in the following year. All wandering albatrosses had been ringed and sexed as part of a long-term mark-recapture programme [START_REF] Weimerskirch | Population dynamics of wandering albatross Diomedea exulans and Amsterdam albatross D. amsterdamensis in the Indian Ocean and their relationships with long-line fisheries: conservation implications[END_REF]. In December, pre-breeding adults are controlled over the whole island. From mid-January to mid-February, at least three visits are carried out every 10 days at each nest to determine the identity and breeding status (egg laid/egg hatched) of each individual. In mid-April, June and August, all nests are checked to monitor the chicks' survival. as 1 for birds that successfully fledged a chick, and as 0 for those that failed at the egg or chick stage. Analyses were performed using R [START_REF] Core | R: a language and environment for statistical computing[END_REF].

b) Blood sampling

e) Estimating the effects of blood heavy metals and persistent organic pollutants on demographic parameters

The capture-recapture data of sampled individuals from 2008 to 2012 were used to evaluate the effects of blood Hg, Cd and POPs on demographic parameters 1 . A MSMR model was constructed, as developed by Pardo et al. [START_REF] Pardo | When celibacy matters: incorporating nonbreeders improves demographic parameter estimates[END_REF][START_REF] Pardo | Females better face senescence in the wandering albatross[END_REF], and included eight states: dead, failed breeder on egg (FBE, defined as an individual that was observed with one egg that failed to hatch), failed breeder on chick (FBC, defined as an individual that was observed with one chick but that failed to fledge the chick), successful breeder (SB, defined as an individual that fledged one chick), observable non-breeder (ONB, defined as an individual that was observed at the colony but that was not observed with an egg or a chick) and three unobservable states (UNB) consisting of non-breeders that were observed at the colony during the previous breeding attempt (PONB), non-breeders whose previous breeding attempt failed (PFB) and non-breeders whose previous breeding attempt was successful (PSB). The state coded as 'dead' ( †) absorbed all those individuals that had either died or permanently emigrated from the study areas. The UNBs account for temporary absence, corresponding to birds that skip breeding in one year after breeding unsuccessfully or successfully during the previous year.

Models were parametrized in terms of the probability of survival (s), the probability of returning to the colony given survival (r), the probability of breeding given return to the colony (β), the probability of successful hatching given breeding (ω), the probability of successful fledgling given hatching (γ) and the detection probability (p). Transition probabilities between states were thus modelled with a five-step procedure where s, r, β, ω and γ were considered as five successive steps in transition matrices. Parameters of the model are defined in the electronic supplementary material. We chose a MSMR approach as this allows us to take into account the probability of detecting individuals given their return to the study site, as well as the previous breeding state of individuals in order to obtain unbiased estimates of demographic parameters [START_REF] Lebreton | Multistate recapture models: modelling incomplete individual histories[END_REF].

This MSMR model was parametrized by the survival-transition probabilities matrix:

Several constraints were made to ensure that the parameters of the model were estimable. The state 'dead' being explicitly included in the model but never being encountered, initial state probability was fixed at 0, transition probabilities from the state 'dead' to the other states were fixed at 0 and capture probability was fixed at 0 [START_REF] Pradel | Multievent: an extension of multistate capture-recapture models to uncertain states[END_REF][START_REF] Choquet | Program ESURGE: a software application for fitting multievent models[END_REF]. The probability of seeing individuals in UNBs and transitions between UNBs was constrained to 0. Since some individuals were observed breeding in the year consecutive to a successful breeding event [START_REF] Barbraud | Estimating survival and reproduction in a quasibiennially breeding seabird with uncertain and unobservable states[END_REF], βSB was not constrained to 0. To limit redundancy in survival parameters, models where survival probabilities all varied separately were not considered [START_REF] Hunter | Rank and redundancy of multistate mark-recapture models for seabird populations with unobservable states[END_REF]. Because of the limited number of individual capture histories, the limited number of recapture occasions and the relatively large number of UNBs, we constrained (i) all parameters to be constant over time, (ii) r to be identical for ONB, PFB, PSB and PONB and (iii) β to be identical for PFB, PSB and PONB. With these constraints, the initial model was full-rank. Note that the model where all demographic parameters were time-and state-dependent was highly rank deficient.

Once The effect of C was first tested on each demographic parameter separately and for different states. Because some parameters were estimated as 100% [100-100%] (electronic supplementary material), we did not test the effects of C on the return probability of males previously observed as (FBE and FBC) or as (ONB, PFB, PSB and PONB), and on the breeding probability of unobservable non-breeders. The 95% confidence interval (CI) of the slope parameters was used, as well as Akaike's information criterion corrected (AICc) for small sample size [START_REF] Burnham | Model selection and multimodel inference: a practical information theoretic approach[END_REF] for inference. We considered a contaminant's effect to be statistically supported when 0 was outside the 95% CI of the mean of the slope of the relationship [START_REF] Grosbois | Assessing the impact of climate variation on survival in vertebrate populations[END_REF]. A composite model was then constructed by combining all the covariates that were detected to have an effect on demographic parameters. Composite models were constructed for heavy metals and POPs separately, as sample sizes differed. In composite models, an effect was not supported if the 95% CI of the slope parameter included 0 [START_REF] Grosbois | Assessing the impact of climate variation on survival in vertebrate populations[END_REF].

We tested the goodness-of-fit (GOF) of the time-dependent MSMR model using U-CARE [START_REF] Choquet | U-CARE: utilities for performing goodness of fit tests and manipulating capture-recapture data[END_REF]. All models were run under program E-SURGE 1.8.5 allowing splitting transition probabilities between states [START_REF] Choquet | Program ESURGE: a software application for fitting multievent models[END_REF]. To avoid estimating parameters at a local minimum of the likelihood function, each model was run five times with random initial values.

(f ) Modelling population dynamics

To evaluate the population-level effects of contaminants, we constructed population models using pre-breeding matrices [START_REF] Caswell | Matrix population models: constructions, analysis and interpretation[END_REF] structured by age and reproductive status classes. We built a two-sex age-and stage-classified matrix population model [START_REF] Caswell | Matrix population models: constructions, analysis and interpretation[END_REF], because Hg and POPs concentrations affected the demographic parameters of males and females differently (see §3).

Based on a detailed demographic study on wandering albatrosses [START_REF] Barbraud | Fisheries bycatch as an inadvertent human-induced evolutionary mechanism[END_REF], the model consists of five juvenile age classes, one pre-breeder class and seven stage-classes according to the breeding status (SB, FBE, FBC, ONB, PSB, PFB and PONB). Parameters entering the model were the recruitment probability, s of adult males, females and juveniles, r of SB and other states, β of SB, FB, ONB and UNB for males and females separately, ω and γ of breeders and non-breeders. We assumed a 1 : 1 sex ratio.

We first built a deterministic matrix model with no stochasticity, which included the mean estimates of the demographic parameters from our MSMR model results and from Barbraud et al. [START_REF] Barbraud | Fisheries bycatch as an inadvertent human-induced evolutionary mechanism[END_REF] for juvenile survival and recruitment probability. From these matrix analyses, we estimated the deterministic population growth rate [START_REF] Caswell | Matrix population models: constructions, analysis and interpretation[END_REF]. We then focused on stochastic matrix models to estimate the stochastic growth rate. Environmental stochasticity was included in two different ways. When a vital rate had no significant relationship with levels of contaminant (C), its yearly values were sampled from a beta distribution [START_REF] Morris | Quantitative conservation biology: the theory and practice of population viability analysis[END_REF], with (10 000 iterations) using package popbio [START_REF] Stubben | Estimating and analyzing demographic models using the popbio package in R[END_REF] implemented in R [START_REF] Core | R: a language and environment for statistical computing[END_REF].

Results

(a) Effects of blood heavy metal and persistent organic pollutants on current breeding output

Blood levels of contaminants are given in the electronic supplementary material.

When considering only breeders in 2008, current breeding success was not related to Hg (d.f. = 1,105, χ² = 0.126, p = 0.723), Cd (d.f. = 1,105, χ² = 0.008, p = 0.929) or ∑ POPs concentrations (d.f. = 1,81, χ² < 0.001, p = 0.993).

(b) Demographic consequences of blood heavy metal levels

The GOF of the MSMR model was overall not significant (males: χ² = 16.327, d.f. = 22, p = 0.799 and females: χ² = 7.078, d.f. = 16, p = 0.972). The effects of sex and states on demographic parameters and the estimation of parameters are detailed in the electronic supplementary material.

Model selection and slope estimates suggested negative effects of Hg on the breeding probability of females previously in state ONB, and on hatching probability and fledging probability of individuals previously in states FB and SB (Table 1a). There was no detectable effect of Cd on demographic parameters (Table 1b). Slope estimates obtained from the composite model (

(d) Modelling population dynamics

The deterministic population growth rate was 1.038, and the respective generation time was 23.8. The stochastic population growth rates were 1.008 when accounting for mean Hg effects from MSMR analyses, 1.002 when accounting for mean POPs effects and 0.991 when accounting for both mean Hg and POPs effects (Figure 3). A doubling in mean Hg concentration would decelerate the population growth rate of 0.68%. A doubling in mean ∑ POPs concentration would decelerate the population growth rate of 0.11%. Doublings in mean Hg and ∑ POPs concentrations would decelerate the population growth rate of 1.31% (Figure 3).

Discussion

Using a unique long-term dataset and MSMR models, this study explores the demographic effects of both metallic and organic pollutants in a wild vertebrate population.

Contaminant levels were associated with a lower breeding probability, a higher hatching failure and a higher fledgling failure, but not with adult survival rate in the wandering albatross. At the population level, a demographic decline was projected in response to increasing Hg and ∑ POP levels.

(a) Effects of contaminants on current breeding output

Contrary to previous studies [START_REF] Tan | The endocrine effects of mercury in humans and wildlife[END_REF][START_REF] Frederick | Altered pairing behaviour and reproductive success in white ibises exposed to environmentally relevant concentrations of methylmercury[END_REF][START_REF] Barron | Comparative reproductive and developmental toxicology of PCBs in birds[END_REF][START_REF] Bustnes | Ecological effects of organochlorine pollutants in the Arctic: a study of the glaucous gull[END_REF], no negative effect of blood Hg, Cd and ∑ POPs was detected on breeding success at the year of sampling. The lack of relationship is probably due to the sampling protocol, since blood sampling was mainly conducted during the incubating period. Some effect of contaminants on early nest desertion and skipped breeding [START_REF] Tartu | To breed or not to breed: endocrine response to mercury contamination by an arctic seabird[END_REF] may have been missed.

(b) Survival and contaminants

Estimated demographic parameters were similar to those previously estimated in the same population using all ringed individuals [START_REF] Barbraud | Estimating survival and reproduction in a quasibiennially breeding seabird with uncertain and unobservable states[END_REF][START_REF] Pardo | Females better face senescence in the wandering albatross[END_REF]. The survival rate of wandering albatrosses was not jeopardized by Hg, Cd and POPs. An effect of POPs was detected on survival rate in one of the most polluted seabirds, the glaucous gull breeding in the Norwegian Arctic, but only the most contaminated individuals had lower survival [START_REF] Erikstad | Persistent organic pollution in a high-Arctic top predator: sex-dependent thresholds in adult survival[END_REF]. Concerning heavy metals, these findings corroborate previous studies that did not evidence an effect of Hg and Cd on adult mortality in birds [START_REF] Wayland | Survival rates and blood metal concentrations in two species of free-ranging North American sea ducks[END_REF][START_REF] Hallinger | Mercury exposure and survival in free-living tree swallows (Tachycineta bicolor)[END_REF][START_REF] Goutte | Demographic responses to mercury exposure in two closely related Antarctic top predators[END_REF]. However, our study did not exclude the possibility that contaminants could jeopardize the survival rate of immature wandering albatrosses, as they have a higher pollution burden [START_REF] Tavares | Influence of age, sex and breeding status on mercury accumulation patterns in the wandering albatross Diomedea exulans[END_REF] and a lower survival rate [START_REF] Barbraud | Fisheries bycatch as an inadvertent human-induced evolutionary mechanism[END_REF] than sexually mature adults.

(c) Long-term fecundity and heavy metals

A negative effect of blood Hg was detected on breeding probability of females observed as non-breeders. Concerning the proximate mechanisms, Hg, in its methylated form, is known to disrupt reproductive hormones [START_REF] Tan | The endocrine effects of mercury in humans and wildlife[END_REF] such as the luteinizing hormone, a key pituitary hormone for the onset of breeding [START_REF] Tartu | To breed or not to breed: endocrine response to mercury contamination by an arctic seabird[END_REF].

As found in two southern Catharacta skua species [START_REF] Goutte | Demographic responses to mercury exposure in two closely related Antarctic top predators[END_REF], Hg negatively impacted hatching probability of albatrosses, but only in individuals previously observed as breeders.

Energetic and time-dependent costs of reproduction may have downstream consequences for reproductive investment during the following breeding season (carry-over effect [START_REF] Catry | Carry-over effects from breeding modulate the annual cycle of a long-distance migrant: an experimental demonstration[END_REF]). Hence, Hg load may have exacerbated these carry-over effects in individuals that previously bred.

Concerning the possible proximate mechanisms, Hg may have caused long-term endocrine disruption of the reproductive system and behavioural impairments [START_REF] Tan | The endocrine effects of mercury in humans and wildlife[END_REF][START_REF] Frederick | Altered pairing behaviour and reproductive success in white ibises exposed to environmentally relevant concentrations of methylmercury[END_REF]. In addition, the maternal transfer of Hg into the egg may have altered embryo development [START_REF] Kenow | Effects of injected methylmercury on the hatching of common loon (Gavia immer) eggs[END_REF].

(d) Long-term fecundity and ∑ POPs

POP burdens reduced the long-term breeding probability of females previously observed as non-breeders and fledging probability of individuals that were previously nonbreeders. Interestingly, POPs appeared to mostly affect albatrosses that skipped the preceding breeding attempt, suggesting a possible segregation of foraging areas between breeders and non breeders. Alternatively, non-breeding females may suffer from higher deleterious effects of POPs on long-term fecundity, because their loads of POPs were not eliminated through the egg.

During the incubating and chick-rearing periods, POPs may weaken the secretion of prolactin, a hormone closely involved in the mediation of parental care, as shown in glaucous gulls [START_REF] Verreault | Changes in prolactin in a highly organohalogen contaminated Arctic top predator seabird, the glaucous gull[END_REF]. In turn, a durable Hg-induced attenuation of prolactin release may result in fledgling failure.

The link between contaminants and reduced fecundity could be a by-product of agedependant mechanisms. However, in this population, fecundity declined in the oldest individuals (35þ years old [START_REF] Pardo | Females better face senescence in the wandering albatross[END_REF][START_REF] Lecomte | Patterns of aging in the long-lived wandering albatross[END_REF]), while Hg levels tended to decrease with age [START_REF] Tavares | Influence of age, sex and breeding status on mercury accumulation patterns in the wandering albatross Diomedea exulans[END_REF] and POP levels were unrelated to age (data not shown). Moreover, age (6-48þ years old) did not affect humoural immunity, oxidative stress, antioxidant defences or hormone levels in wandering albatrosses [START_REF] Lecomte | Patterns of aging in the long-lived wandering albatross[END_REF]. Hence, it is unlikely that age was a confounding factor in the correlation between contaminants and physiological mechanisms underlying breeding performance.

(e) Modelling population dynamics

Translating individual-level effects of contaminants to population-level processes is a crucial and ultimate goal of modern ecological research. Our population models suggested that the actual Hg and POPs levels could decelerate the population growth rate (0.991), whereas the population growth rate would increase (1.027) with zero concentrations of blood Hg and POPs. In addition, doublings in mean blood Hg and POPs levels would decelerate the growth rate of this wandering albatross population by 1.31%. These predictions could undoubtedly be worsened by other anthropogenic perturbations. For instance, climate change can impact transport, distribution, bioavailability, bioaccumulation and effects of pollutants [START_REF] Noyes | The toxicology of climate change: environmental contaminants in a warming world[END_REF][START_REF] Stern | How does climate change influence arctic mercury?[END_REF][START_REF] Cossa | 1448.794 2.885 Effect of Cd on survival rate of males Cd13 24 1449.048 3.139 Effect of Cd on breeding probability of males previously in states FBE or FBC Cd5 24 1449.054 3.145 Effect of Cd on fledgling success of individuals previously in states FB or SB Cd1 24 1449.129 3.220 Effect of Cd on breeding probability of males previously in state SB Cd7 24 1449.159 3.250 Effect of Cd on breeding probability of males previously in state ONB Cd9 24 1449.215 3.306 Effect of Cd on breeding probability of females previously in states PFB[END_REF] and triggers steep population declines in albatrosses [START_REF] Barbraud | Effects of climate change and fisheries bycatch on Southern Ocean seabirds: a review[END_REF]. In that respect, a future avenue for ecotoxicological and conservation research could be dedicated to evaluating and predicting the coupled effects of climatic and chemical perturbations on wildlife population viability.

Figure 1: Effect of standardized blood Hg levels on (a) breeding probability of females previously observable as non-breeders (ONB), and (b) hatching probability of individuals previously observed as breeders. Dotted lines represent 95% CIs estimated using the delta method [START_REF] Seber | The estimation of animal abundance and related parameters[END_REF]. Histograms represent the measured blood Hg levels (c). Analyzer spectrophotometer (Altec AMA 254). At least two aliquots ranging from 5 to 10 mg dry weight were analyzed for each individual and measurement quality was certified by reference material, as described by [START_REF] Bustamante | Total and organic Hg concentrations in cephalopods from the North East Atlantic waters: influence of geographical origin and feeding ecology[END_REF]. Accuracy was checked using a certified reference material (CRM, Tort-2 Lobster Hepatopancreas, NRC, Canada; certified Hg concentration: 0.27 ± 0.06 μg g-1 dry mass). Mass of CRM was adjusted to represent the same amount of Hg introduced in the AMA compared to that in blood samples. Blanks were analysed at the beginning of each set of samples and the detection limit of the method was 0.005 μg g-1 dry mass.

Concerning Cd assays, two aliquots of lyophilized red blood cells (~300 mg of dry sample) were digested with 3 ml of 65% HNO3 and 2 ml of 37% HCl (both from Merck and suprapur quality). Acidic mineralization was performed at room temperature overnight, then in a microwave during 30 min with increasing temperature until 105°C, and 15 min at 105°C (1200 W). After the mineralization process, each sample was diluted to 30 with milli-Q quality water. Cd was analysed using a Varian Vista-Pro ICP-OES and a Thermo Elemental were added gravimetrically: PCBs 30, 103, 155 and 198 were used to quantify PCBs, p,p'-DDT-d8 was used to quantify pesticides, and F-BDE-47 was used to quantify PBDE; standards were provided by either Dr Ehrenstorfer GmbH or Cambridge Isotope Laboratory (via Cluzeau Info Labo, Sainte-Foy-La-Grande, France). POPs were extracted with 1 mL of pentane/dichloromethane (90/10; v/v); after centrifugation (2000 rpm, 2 min at 4°C), the organic layer was collected and the operation was repeated. Both extracts were combined and purified on an acid silica gel column (40% H2SO4). After extract loading, analytes were eluted with 3 x 5 mL of pentane/dichloromethane (90/10; v/v). The so-obtained extract was then concentrated using a RapidVap vacuum evaporation system from Labconco (Kansas City, MO, USA) to a volume of 1 mL; it was then further concentrated under a gentle stream of nitrogen (40°C) after addition of 100 µL of isooctane as solvent keeper. A syringe standard (octachloronaphtalene, 1 ng) was finally added to quantify internal standards and to assess their recovery rate for each sample (68-108%). Final extracts were analysed by gas chromatography coupled with electron capture detection (GC-ECD) as described elsewhere [START_REF] Tapie | PBDE and PCB contamination of eels from the Gironde estuary: From glass eels to silver eels[END_REF].

Quality control consisted in the analysis of procedural blanks (clean and empty glass tubes treated like a sample, one run for 8 samples). Chicken plasma samples (Sigma-Aldrich, St Quentin Fallavier, France) spiked at 3 ng g-1 were analysed; the recovery rates of PCBs and organochlorine pesticides were in the range 77-103% with coefficients of variation lower than 17% (n=5), except for CB-52 (22%) and mirex (29%). POPs levels were blank corrected and the detection limit (LoD) was set at two times the mean blank value; for analytes that were not detected in blanks, LoD was determined as the concentration with a signal to noise ratio of 3. Overall, LoDs ranged from 0.09 to 0.76 ng g-1wet weight. Additionally, plasma total lipids were measured on an aliquot of 10 µL by the sulfo-phospho-vanillin (SPV) method for colorimetric determination [START_REF] Frings | Improved determination of total serum lipids by the sulfo-phospho-vanillin reaction[END_REF].

Definition of parameters used in

From 21

 21 December 2007 to 04 March 2008, 147 sexually mature adults (i.e. observed as incubating or chick-rearing at least once before or during the current breeding season) were captured. A sample of venous blood was taken from the tarsus with a 1-ml heparinized syringe and a 25-gauge needle. Only one bird was sampled per nest. The volume of the blood draws never exceeded 0.05% of the bird's body mass (8-12 kg). c) Laboratory analyses Hg and Cd were analysed in red blood cells at the Littoral Environnement et Sociétés (LIENSs), La Rochelle, France. POPs (PCBs: CB-28, -52, -101, -118, -138, -153 and -180; , Heptachlore, 2,4' DDE (dichlorodiphenyldichloroethylene), Cischlordane, trans-nonachlor, 4,4' DDD (dichlorodiphenyldichloroethane), 2,4' DDT (dichlorodiphenyltrichloroethane), 4,4' DDT, Mirex; and BDE-47) were analysed in plasma at the EPOC-LPTC, Bordeaux, France. Further details about analyses are reported in the electronic supplementary material. d) Estimating the effects of blood heavy metals and persistent organic pollutants on breeding output during the year of sampling Generalized linear models (GLMs) with binomial error distribution and a logit link function were used to test whether breeding success in 2007-2008 was linked to blood Hg, Cd or POP levels in individuals sampled as breeders in 2007-2008. Breeding success was coded

  the best model structure was identified (Model 21, electronic supplementary material), effects of blood Hg, Cd and POPs were tested on demographic parameters to investigate whether contamination levels in one breeding season may influence the long-term survival and breeding outputs of an individual over the four following years. MSMR models were built where each demographic parameter θ was modelled as a function of an individual covariate C (standardized level of Hg, Cd or sum of POPs (log-transformed)) using a logit link function: logit (θ) = a + b X Ci, where a is an intercept, b is a slope and Ci is the covariate for individual i. When b < 0, or b > 0, C has a negative or positive effect on θ, respectively.

  mean and variance equal to those estimated from the MSMR model selected. When a vital rate had a significant relationship with C levels, its value was modelled as θ = logit -1 (a + b x Ċ), where Ċ is the mean value of the contaminant levels for all individuals. C values were sampled from a log-normal distribution for all individuals sampled. The values of a and b were recalculated for non-standardized C values representing the absolute values for Hg and log-transformed values for ∑ POPs. To assess the population-level effects of C, we estimated stochastic population growth rates according to changes in mean C levels within the range of observed C values. The matrix population models were analysed by Monte Carlo simulations

  812 (-1.551; -0.072) for the effects of ∑ POPs on breeding probability of females previously in state ONB (Figure 2a,c) and on fledging probability of individuals previously in states ONB or UNB (Figure 2b,c), respectively.

Figure 2 :

 2 Figure 2: Effect of standardized blood Σ POPs (log-transformed) on (a) breeding probability of females previously observed as non-breeders and (b) fledgling success of individuals previously observed as non-breeders or unobserved. Dotted lines represent 95% confidence intervals estimated using the delta method [45]. Histograms represent the measured blood POP levels in the sampled individuals (c).

Figure 3 :Figure 1 Figure 2 :

 312 Figure3: Isoclines of population growth rate (λ) of wandering albatrosses as projected with the population models, which included the responses to mercury levels (x-axis) and POPs (log-transformed) levels (y-axis) within the range of observed mercury and POPs levels

Figure 3 : 4 :

 34 Figure 3 :

Figure 2 :

 2 Figure2: Effect of standardized ∑ POPs (log-transformed) on (a) breeding probability of females previously observed as non-breeders and (b) fledgling probability of individuals previously observed as non-breeders or unobserved. Dotted lines represent 95% confidence intervals estimated using the delta method[START_REF] Seber | The estimation of animal abundance and related parameters[END_REF]. Histograms represent the measured blood ∑ POP levels (c).

Figure 3 .

 3 Figure 3. Isoclines of population growth rate in wandering albatrosses as projected with the population models, which included the responses to blood Hg levels and blood ∑ POPs (logtransformed) within the range of observed Hg and ∑ POP levels.

  Series II Varian ICP-MS Data of Hg and Cd concentrations are presented relative to the dry weight (dw).

(

  ii) Analysis of POPs concentrations POPs were analysed from plasma (N = 115 samples) at the EPOC-LPTC, Université Bordeaux 1, France. The targeted compounds included 7 indicator PCBs (CB-28, -52, -101, -118, -138, -153 and -180), 10 organochlorine pesticides (HCB, Gamma HCH, Heptachlore, 2,4' DDE, Cis-chlordane, trans-nonachlor, 4,4' DDD, 2,4' DDT, 4,4' DDT, Mirex) and BDE-47. Certified solutions containing all analytes at 2 ng µL -1 each were obtained from LGC Standards (Molsheim, France). To a plasma sample of 100 µL, internal standards (1 ng each)

  .807 (-1.645;0.032) for the effects of Hg on breeding probability of females previously in state ONB (Figure1a,c), hatching probability of individuals previously in states FB and SB (Figure1b,c) and fledging probability of individuals previously in states FB and SB, Model selection and slope estimates suggested a negative effect of ∑ POPs on fledging probability of individuals previously in states ONB or UNB and on breeding probability of females previously in state ONB (Table2). Other models were not supported, because 95% CI of slope parameter values included 0 (Table2). Slope estimates obtained from the

	respectively. The last effect was not supported, because 95% CI included 0 in the composite
	model.
	(c) Demographic consequences of blood ∑ POP levels

Table 1c) were -2.114 (95% CI: (-4.213; 20.015)), -0.620 (-1.234; -0.005) and -0composite model were -0.976 (-1.917; -0.035) and -0.

Table 2 :

 2 Modeling the effects of blood ∑ POP levels (log-transformed and standardized) on demographic parameters (N = 115 individuals). The estimated slope and 95% confidence intervals (CI) for models with a lower AICc than the intercept model (POP0) are given.

	Hypothesis

the multistate mark-recapture model

  Probability that an individual in state s at time t survives to time t + 1 and does not permanently emigrate from the study area r t

	Parameter Definition
	s t	s

s

  Probability that an individual in state s at time t returns at the colony to time t + 1 given that it survives to t + 1 β t

s

  Probability that an individual in state s at time t breeds at time t + 1 given that it survives to and returns at the colony at time t + 1 γ t

s

  Probability that an individual in state s at time t incubates successfully at time t + 1 given that it survives to, returns at the colony and breeds at time t + 1Probability that an individual in state s at time t is encountered at time t

	δ t	s	Probability that an individual in state s at time t raises successfully one chick at
				time t + 1 given that it survives to, returns at the colony and incubates
				successfully at time t + 1
	p t	s

3. Testing for the effects of sex and states on demographic parameters Initial

  model (# 1) considers sex-difference and no difference among states on survival (s) ; sex-difference and difference among failed breeder at the egg stage FBE, failed breeder at the chick stage FBC, successful breeder SB, and (observable non breeder ONB, post failed breeder PFB, post successful breeder PSB, post observable non-breeders PONB) on return at the colony (r) ; sex-difference and differences among FBE, FBC, SB, ONB, and (PFB PSB PONB) on breeding (β) ; sex-difference and differences among FB, SB, ONB, UNB on hatching (ω) ; sex-difference and differences among FB, SB, ONB, UNB on fledgling (γ) ; sex-difference and differences among FBE, FBC, SB and ONB on detection (p). The parentheses indicate that the demographic parameter was identical for all states into the parentheses. UNB indicates that all unobservable states (i.e. PFB, PSB and PONB) were constrained to have the same demographic parameter.The best model according to AICc (model #21) suggested that males and females differed in survival rate and breeding probability, but not in return probability, hatching success and fledgling success. Return probabilities differed between individuals previously (i.e. the preceding year) in states failed breeder (FB = FBE and FBC), SB and non-breeder (ONB, PFB, PSB and PONB). Breeding probability differed between individuals previously in states FB, SB, ONB and unobservable non-breeders (UNB). Hatching success and fledgling success differed among individuals previously in states breeders (FB and SB) and non-breeders.

	Testing for the effects of sex on s, r, β, ω, γ, and p	# Rank Deviance ΔAICc
	Sex-differences in s and β	7	31	1628.94	0
	Sex-differences in s, β and γ	6	35	1624.95	5.24
	Sex-differences in s, β, ω and γ	4	39	1624.90	14.57
	Sex-differences in r, β, ω and γ	3	42	1626.13	22.95
	Sex-differences in s, r, β, ω and γ	2	43	1622.89	22.12
	Sex-differences in s, r, β, ω, γ, and p	1	47	1618.47	27.42
	Sex-differences in s, ω and γ	5	34	1666.45	44.42
	Testing for the effects of states on p	# Rank Deviance ΔAICc
	Differences among (FBE FBC), SB and ONB	8	30	1629.69	0
	Differences among FBE, FBC, SB and ONB	7	31	1628.94	1.53
	Similitude among FBE, FBD, SB and ONB	9	28	1667.71	33.49
	Testing for the effects of states on r	# Rank Deviance ΔAICc
	Differences among (FBE FBC) SB, and (ONB PFB PSB PONB)	10	29	1629.97	0
	Differences among FBE,FBC,SB, and (ONB PFB PSB PONB)	8	30	1629.69	1.99
	Differences among (FBE FBC SB) and (ONB PFB PSB PONB)	11	28	1691.79	59.56
	Similitudes among FBE FBC SB ONB PFB PSB PONB	12	27	1737.14 102.66
	Testing for the effects of states on β	# Rank Deviance ΔAICc
	Differences among (FBE FBC), SB, ONB, and (PFB PSB PONB) 13	27	1634.18	0
	Differences among FBE, FBC, SB, ONB, and (PFB PSB PONB)	10	29	1629.97	0.30
	Differences among (FBE, FBC, SB), ONB, and (PFB PSB
	PONB)	14	25	1673.25	34.60
	Differences among (FBE FBC), SB, and (ONB PFB PSB PONB) 15	25	1713.04	74.39
	Similitudes among FBE, FBC, SB, ONB, PFB, PSB, PONB	16	21	1733.53	86.05
	Testing for the effects of states on ω	# Rank Deviance ΔAICc
	Differences between (FB SB) and (ONB UNB)	18	25	1636.16	0
	Differences among FB, SB and (ONB UNB)	17	26	1635.98	2.06
	Differences among FB, SB, ONB, UNB	13	27	1634.18	2.49
	Similitudes among FB, SB, ONB, UNB	19	24	1651.54	13.16
	Testing for the effects of states on γ	# Rank Deviance ΔAICc
	Differences between (FB SB) and (ONB UNB)	21	23	1636.55	0
	Differences among FB, SB and (ONB UNB)	20	24	1636.30	1.96
	Differences among FB, SB, ONB, UNB	18	25	1636.16	4.04
	Similitudes among FB, SB, ONB, UNB	22	22	1651.45	12.70

4.

Estimation of parameters (mean and CI) calculated from the best model (model # 21).

	State	Survival	Return probability	Breeding	Hatching	Fledging	Detection
		probability (%)	(%)	probability (%)	probability (%)	probability (%)	probability (%)
	SB male	91.8 [87.3 ; 94.8] 34.8 [26.6 ; 43.9] 14.0 [5.2 ; 32.5]	61.7 [49.1 ; 72.8]	60.6 [43.7 ; 75.3]	98.8 [56.4 ; 100]
	SB female	95.9 [92.1 ; 97.9] 34.8 [26.6 ; 43.9] 28.0 [14.2 ; 47.6] 61.7 [49.1 ; 72.8]	60.6 [43.7 ; 75.3]	98.8 [56.4 ; 100]
	FBE male	91.8 [87.3 ; 94.8] 100 [100 ; 100]	79.2 [60.0 ; 90.6] 61.7 [49.1 ; 72.8]	60.6 [43.7 ; 75.3]	75.4 [53.3 ; 89.2]
	FBE female	95.9 [92.1 ; 97.9] 100 [100 ; 100]	86.6 [68.5 ; 95.0] 61.7 [49.1 ; 72.8]	60.6 [43.7 ; 75.3]	75.4 [53.3 ; 89.2]
	FBC male	91.8 [87.3 ; 94.8] 100 [100 ; 100]	79.2 [60.0 ; 90.6] 61.7 [49.1 ; 72.8]	60.6 [43.7 ; 75.3]	75.4 [53.3 ; 89.2]
	FBC female	95.9 [92.1 ; 97.9] 100 [100 ; 100]	86.6 [68.5 ; 95.0] 61.7 [49.1 ; 72.8]	60.6 [43.7 ; 75.3]	75.4 [53.3 ; 89.2]
	ONB male	91.8 [87.3 ; 94.8] 100 [100 ; 100]	20.0 [12.8 ; 29.7] 87.6 [80.4 ; 92.4]	92.2 [85.4 ; 96.0]	55.7 [43.8 ; 66.9]
	ONB female	95.9 [92.1 ; 97.9] 100 [100 ; 100]	82.1 [60.9; 93.1]	87.6 [80.4 ; 92.4]	92.2 [85.4 ; 96.0]	55.7 [43.8 ; 66.9]
	PSB male	91.8 [87.3 ; 94.8] 100 [100 ; 100]	100 [100 ; 100]	87.6 [80.4 ; 92.4]	92.2 [85.4 ; 96.0]
	PSB female	95.9 [92.1 ; 97.9] 100 [100 ; 100]	96.9 [57.5 ; 99.9] 87.6 [80.4 ; 92.4]	92.2 [85.4 ; 96.0]
	PFB male	91.8 [87.3 ; 94.8] 100 [100 ; 100]	100 [100 ; 100]	87.6 [80.4 ; 92.4]	92.2 [85.4 ; 96.0]
	PFB female	95.9 [92.1 ; 97.9] 100 [100 ; 100]	96.9 [57.5 ; 99.9] 87.6 [80.4 ; 92.4]	92.2 [85.4 ; 96.0]
	PONB male	91.8 [87.3 ; 94.8] 100 [100 ; 100]	100 [100 ; 100]	87.6 [80.4 ; 92.4]	92.2 [85.4 ; 96.0]
	PONB female 95.9 [92.1 ; 97.9] 100 [100 ; 100]	96.9 [57.5 ; 99.9] 87.6 [80.4 ; 92.4]	92.2 [85.4 ; 96.0]
	5

. Blood heavy metals and POP concentrations in the wandering albatross.

  Mean and standard deviation are given. Nm indicates the sample size of males and Nf indicates the sample size of females. Generalized linear models (GLMs) with normal error and identity link function were used to test sex-differences.

	Contaminants	Nm	Males	Nf	Females	Statistics
	Hg in red blood cells (in μg g -1 dw) 90	6.2 ± 3.0	57	10.7± 0.5	F1,141= 63.630, p < 0.001
	Cd in red blood cells (in μg g -1 dw) 90	0.05 ± 0.03	57	0.07 ± 0.04	F1,141 = 12.121, p < 0.001
	Σ POPs in plasma (in ng g -1 lw)	72	6363 ± 10002	39	2726± 4398	F1,109 = 10.514, p = 0.002

Acknowledgments

The authors thank V. Lecomte and A. Jaeger for data collection; H. Maheo and M. Berlincourt for their assistance in the field and all the wintering fieldworkers involved in the long-term monitoring programmes; C. Churlaud and S. Tartu for their help in laboratory analyses; D. Besson for managing the long-term database; and the reviewers for their constructive and helpful comments. Funding statement. This project was supported by l'Agence Nationale de la Recherche (ANR PolarTop, O.C.), the French Polar Institute (IPEV, program 109, H.W.), the Terres Australes et Antarctiques Françaises and the Zone Atelier de Recherches sur l'Environnement Antarctique et Subantarctique (CNRS-INEE).