Colin Riba
email: riba@loria.fr

On the Stability by Union of Reducibility Candidates

We investigate some aspects of proof methods for the termination of (extensions of) the second-order λ-calculus in presence of union and existential types. We prove that Girard's reducibility candidates are stable by union iff they are exactly the non-empty sets of terminating terms which are downwardclosed w.r.t. a weak observational preorder. We show that this is the case for the Curry-style second-order λ-calculus. As a corollary, we obtain that reducibility candidates are exactly the Tait's saturated sets that are stable by reduction. We then extend the proof to a system with product, co-product and positive iso-recursive types.

Introduction

Since their introduction in [START_REF] Macqueen | An Ideal Model for Recursive Polymorphic Types[END_REF], union and existential types with type assignment rules are present in many type systems. From a foundational perspective, they are interesting as dual of respectively intersection and second-order types. The paper [START_REF] Barbanera | Intersection and Union Types: Syntax and Semantics[END_REF] provides detailed investigations on syntactic as well as semantics issues of union types. As a theoretical tool, they have been used in [START_REF] Dezani-Ciancaglini | A Filter Model for Concurrent Lambda-Calculus[END_REF]9] to prove that a kind of Böhm trees, called Lévy-Longo trees, distinguishes pure λ-terms exactly as does their observation in the lazy concurrent λ-calculus.

Interesting applications of union types are the XML processing languages XDuce [START_REF] Hosoya | Regular Expression Types for XML[END_REF] and CDuce [11]. They describe types of XML documents by means of regular expressions whose internal representation relies on union types.

Existentials and unions are also interesting tools for representing abstractions of programs. In the context of strictness analysis, unions are used in [START_REF] Jensen | Disjunctive Strictness Analysis[END_REF] to represent disjunctive properties of programs.

Frédéric Blanqui and the author proposed in [6] a termination criterion for higher-order conditional rewriting that use constrained types. Existential constraints arise naturally, for example when proving that some implementations of QuickSort preserves the size of its argument. This work relies on proof methods for the termination of typed λ-calculus plus rewriting in presence of existential types.

Usual proofs of strong normalization (i.e. termination) for typed λ-calculi assign to each type T a set of strongly normalizing terms T ρ (the interpretation of T , with an assignment ρ of its free variables). Then, they use soundness of this interpretation w.r.t. the type system: typable terms belong to the interpretation of their types. But soundness requires that types are not interpreted by arbitrary sets of terms. They must satisfy some closure conditions. The two most popular ones are Girard's reducibility candidates and Tait's saturated sets. See [12] for a detailed discussion and historical references. A comparison of Girard's and Tait's closure conditions can also be found in [START_REF] Werner | Une Théorie des Contructions Inductives[END_REF].

In order to handle elimination rules of union and existential types, it is convenient to interpret these types by using unions of interpretations: T 1 ∪ T 2 ρ = T 1 ρ ∪ T 2 ρ and ∃X.T ρ = C∈Cl T ρ[C/X] (Cl is the collection of closed sets under consideration). This making requires stability by union of closed sets: if C is a family of closed sets, then C = def C∈C C is closed. Approaches not relying on stability by union are briefly discussed in Sec. [START_REF] Dezani-Ciancaglini | A Filter Model for Concurrent Lambda-Calculus[END_REF].

It is well known (see e.g. [START_REF] Werner | Une Théorie des Contructions Inductives[END_REF]) that Tait's saturated sets for β-reduction are stable by union. However, their extension with additional computational rules can by cumbersome. On the other hand, Girard's reducibility candidates are more adjustable, in particular for dealing with rewriting [START_REF] Blanqui | Inductive-Data-Types Systems[END_REF]. However, their stability by union is known to be problematic [START_REF] Werner | Une Théorie des Contructions Inductives[END_REF].

In this paper, we prove the stability by union of reducibility candidates for the polymorphic λ-calculus λ2. To our knowledge, this property was hitherto unknown, and even often believed to be false. We extend the proof to λ2U + , the extension of λ2 with product, co-product and positive iso-recursive types (it is shown in [START_REF] Sp | Type Fixpoints: Iteration vs. Recursion[END_REF] that it is a proper extension of λ2).

The key observation is that reducibility candidates are stable by union iff they are exactly the non-empty sets of strongly-normalizing terms which are downward-closed w.r.t. a weak observational preorder (see [16] for a presentation and references on related topics). This is a very simple structure compared to the one appearing in the definition of reducibility candidates, which is not trivial and somehow mysterious. Hence, studying stability by union of reducibility candidates reveals important facts on their fundamental nature.

We show that the above condition is equivalent to say that some terms, called neutral, have a maximal reduct w.r.t. to that preorder. For the case of λ2 and λ2U + , we prove it by using a simple syntactic property called weakstandardization. It relies on the orthogonality of λ2 and λ2U + : computational rules are non-ambiguous and left-linear (no equality tests between open terms). As a by-product, we obtain that Girard's sets correspond exactly to the Tait's sets that are stable by reduction.

We present the syntax of λ2 in Sec. 2, and reducibility in Sec. 3. Our analysis of stability by union of reducibility candidates is presented in Sec. 4. Finally, the system λ2U + is presented in Sec. 6, and stability by union of its reducibility candidates in Sec. 7.

We assume familiarity with λ-calculus and types, and refer to [START_REF] Girard | Proofs and Types[END_REF][START_REF] Barendregt | Lambda Calculi with Types[END_REF] for detailed introductions.

The Polymorphic λ-Calculus λ2

The core language of the paper is the Curry-style second-order λ-calculus λ2, as presented in [START_REF] Barendregt | Lambda Calculi with Types[END_REF]. We recall the main notations below, and then discuss union and existential types.

Let X be a countable set of variables and Λ be the set of untyped λ-terms:

t, u ∈ Λ ::= x ∈ X | λx.t | t u .
They are considered equals modulo α-conversion.

(∀u (t → u ⇒ u ∈ SN )) ⇒ t ∈ SN .
Types are the formulas of second-order minimal logic, with variables in V:

T, U ∈ T ::= X ∈ V | T ⇒ U | ∀X.T .
We denote by X (t) (resp. V(T )) the set of free variables of t (resp. T ). An environment Γ is a finite set of declarations x : A such that x = y whenever (x : A), (y : B) ∈ Γ . Typing judgments are sequents of the form Γ t : A, derived with the following rules:

It is worth noting that such types are not subject to the Curry-Howard propositions-as-types isomorphism, in the sense that proofs trees do not corresponds to terms. It would require to reflect all types constructions at the term level, and this leads to use explicit constructs for disjunction and existential quantification, as discussed for e.g. in [START_REF] Girard | Proofs and Types[END_REF].

This is precisely what we want to avoid in [6], where existential quantifications are used in a constrained type system. We want terms typed in this system to be used in a constrained-free type system. Hence, constraints should not appear at the term level, and we are thus interested in implicit existential types.

On the other-hand, it is clear that the impredicative codings of unions and existential quantification given in [START_REF] Girard | Proofs and Types[END_REF] do not define union and implicit existential types. This motivates us to handle the soundness of rules (∪E) and (∃ E) by tools lying inside the reducibility framework. A first step is to study the behavior of Girard's reducibility candidates w.r.t. union. Since type quantifications of [6] are not the usual ones, presented above, that operate on the type structure, we study stability by union in a generic way, without committing to specific typing rules.

Reducibility

Strong normalization proofs of λ2 usually interpret types T ∈ T as sets of strongly normalizing terms T ρ ⊆ SN . Then strong normalization of typable terms follows from the soundness of the interpretation: If Γ t : T and σ(x) ∈ A ρ for all (x : A) ∈ Γ , then σ(t) ∈ T ρ.

( )

As said in the introduction, ( ) does not hold when types are interpreted by arbitrary subsets of SN . In this section, we focus on a well-known collection of suitable subsets of SN called Girard's reducibility candidates.

Definition 3.1 (Neutral Terms).

Terms not headed by an abstraction are called neutral. Let N be the set of neutral terms.

Let HN , the set of hereditary neutral terms, be the smallest set such that for all t ∈ N , (∀u

(t → u ⇒ u ∈ HN )) ⇒ t ∈ HN . Note that HN ⊆ SN . Let elimination contexts be E[ ] ::= [ ] | E[ ]t.
They correspond to call-by-name evaluation contexts, dual to call-by-value evaluation contexts of [START_REF] Felleisen | The Revised Report on the Syntactic Theories of Sequential Control and State[END_REF]. We borrowed from [START_REF] Abel | Termination Checking with Types[END_REF] their use in reducibility.

Remark 3.2. The general intuition behind neutral terms is linked to the duality between introductions and eliminations in natural deduction. Since neutral terms are not headed by introductions, they do not interact with elimination contexts:

if t ∈ N and E[t] → v then v = E [t ] with (E[ ], t) → (E [ ], t ). It follows that for t ∈ N , we have E[t] ∈ N and E[t] ∈ SN as soon as {E[u] | t → u} ⊆ SN . Definition 3.3 (Reducibility Candidates). The set of reducibility candi- dates, denoted by CR, is the set of all C ⊆ SN such that (CR0) if t ∈ C and t → u then u ∈ C, (CR1) if t ∈ N and (∀u (t → u ⇒ u ∈ C)) then t ∈ C.
The definition of SN directly implies that SN ∈ CR. Now, let us see why CR is stable by intersection (C ⊆ CR ⇒ C ∈ CR). Recall that a closure operator on a partial order (D, ≤) is a function • : D → D which is idempotent: X = X; extensive: X ≤ X; and monotone: X ≤ Y ⇒ X ≤ Y . It is well-known that the greatest lower bound of a family of closed elements is closed.

The shape of the clauses of CR is sufficient for the existence of a closure operator • : P(SN ) → P(SN ) such that X is the least reducibility candidate containing X. Indeed, clauses (CR0) and (CR1) are closure rules in the sense of [START_REF] Dezani-Ciancaglini | Discrimination by Parallel Observers[END_REF], p.17, and the existence of • is insured by Thm. 2.6, see pages 16-18 of [START_REF] Dezani-Ciancaglini | Discrimination by Parallel Observers[END_REF]. We thus have X ∈ CR iff X = X.

It follows that (CR, ⊆) has all greatest lower bounds, and they are given by . As a consequence, it has CR as least element. It is thus an inf-semi lattice with greatest element SN , hence a complete lattice. Proposition 3.4. HN is the least element of CR.

Proof. We obviously have HN ⊆ C for all C ∈ CR, hence HN ⊆ CR. For the converse, it suffices to remark that HN ∈ CR.

We now define the interpretation of arrow types. Proof. Strong normalization and stability by reduction follows directly from that of B. For (CR1), we have to show that if t ∈ N , then (t) → ⊆ A ⇒ B implies t ∈ A ⇒ B, i.e. u ∈ A ⇒ tu ∈ B. The crucial point is given by Rem. 3.2: since tu ∈ N and t does not interact with the context [ ]u, we are done with (CR1) applied to B, using an induction on (t, u) ∈ SN × SN . Now, given ρ : V → CR, we can interpret types T ∈ T as reducibility candidates

T ρ ∈ CR, with X ρ = def ρ(X), U ⇒ T ρ = def U ρ ⇒ T ρ and ∀X.T ρ = def { T ρ[C/X] | C ∈ CR}.
We can then prove soundness ( ), and strong normalization is a consequence of X ⊆ HN and Prop. 3.4. See [START_REF] Girard | Proofs and Types[END_REF]12].

A General Study of Stability by Union of CR

We have seen that stability by intersection of CR is a consequence of the shape of the clauses (CR0) and (CR1). Such shallow observations do not imply stability by union, which must therefore be proved through a deeper analysis of CR. Indeed, given C ⊆ CR, in order to get C ∈ CR we must show that if t is a neutral term with (t) → ⊆ C, then every one-step reduct of t must be in the same C ∈ C.

We begin by stability by union of closure operators. In the next Proposition, we assume given a set D and a closure operator • : P(D) → P(D). Write x for {x} and P(D) for {X | X ⊆ D}. Proof. For all X ∈ P(D) we have X = {x | x ∈ X} since for all x ∈ X, x ⊆ X and x ∈ x. It follows that

P(D) ⊆ Ω. If C ⊆ Ω, then C = {x | x ∈ C} for all C ∈ C. Hence C = {x | x ∈ C},
. If X ∈ Ω then X = {x | x ∈ X}. But {x | x ∈ X} ⊆ Ω, hence {x | x ∈ X} ∈ Ω.
In other words, (D, Ω ∪ {∅}) is a topological space where the set of opens Ω ∪ {∅} contains all • -closed sets. Proposition 4.1 implies that it is moreover the coarser topology with this property: if Ω is a collection of opens that contains • -closed sets, then Ω ⊆ Ω. We now use these facts to study the stability by union of reducibility candidates.

Since we are concerned with properties independent from the calculus, we work with an extension λext of λ2. We assume that every term typable in λ2 is typable in λext and that λext is equipped with a rewrite relation, denoted by →, that is finitely branching and contains → β . Notations of Sec. 2 are imported in λext. Finally, we assume given a set of neutral terms of λext, still denoted by N , that contains the neutral terms of λ2. As with λ2, CR is the set of closed sets for a closure operator • : P(SN ) → P(SN ). An explicit inductive definition of • is useful:

Lemma 4.3 (The Closure Operator • of CR). Given X ⊆ SN , let X 0 = def (X) * → , and for all i ≥ 0, X i+1 = def X i ∪ {t ∈ N | (t) → ⊆ X i }.
Then, for all X ⊆ SN , X = def i≥0 X i is the smallest reducibility candidate containing X.

Proof. First, we show that X ∈ CR. (CR0) Let t → v and t ∈ X i with i as small as possible.

If i = 0, then t ∈ (X) * → , hence v ∈ (X) * → = X 0 . Otherwise, i = j + 1, and v ∈ X j . (CR1) Let t ∈ N such that for all v ∈ (t) → , there is i v with v ∈ X iv . Since → is
finitely branching, there is a j greater than every i v , thus t ∈ X j+1 . Second, by induction on i, we prove that if C ∈ CR and X ⊆ C, then X i ⊆ C. We have Before studying what insures the equality of CR and CR, let us have a look on the structure of the latter. We begin by a characterization of the membership t ∈ u that uses the weak observational preorder . Observational preorders where introduced to characterize behavioral equivalence: two pieces of programs are observationally equivalent iff when plugged in a program context, the obtained programs both diverges or evaluates to the same value. Contexts are arbitrary terms with a hole, including those of the form t[ ] and λx.[ ]. With closed terms, thanks to Milner's Context Lemma, this is equivalent to observation in applicative contexts (our elimination contexts). Of course, this fails for open terms. See [START_REF] Milner | Fully Abstract Models of Typed λ-Calculi[END_REF]16] for a presentation and references on the subject.

X 0 = (X) * → ⊆ C by (CR0). For i ≥ 0, if t ∈ X i+1 \ X i ,
In λ2, non-neutral terms are abstractions, hence closed non-neutral terms correspond to the usual notion of value. Moreover, we have t u iff for all

E[ ], for all v / ∈ N , (E[t] → * v ⇒ E[u] → * v).
Thus, with we observe the reduction to values of open terms plugged in elimination contexts. Hence the name weak observational preorder. We generalize these ideas to the system λ2U + in Sec. [START_REF] Danos | Disjunctive Tautologies as Synchronisation Schemes[END_REF].

In order to characterize t ∈ u with , we need a few properties. First, note that t → u implies u t. Proposition 4.5. Let X ⊆ SN . Then t ∈ X iff either t ∈ (X) * → or (t ∈ N and (t) → ⊆ X).

Proof. The "if" direction directly follows from (CR0) and (CR1). Conversely, let i be as small as possible such that t ∈ X i . Thus, either i = 0 and t ∈ (X) * → or i = j + 1, t ∈ X j+1 \ X j and by definition t ∈ N and (t) → ⊆ X j .

As a consequence, all non-neutral terms of X are in (X) * → . In other words, the values of X are entirely determined by X.

Proposition 4.6. Let t ∈ N ∩ SN and X ⊆ SN . Then (t) → ⊆ X iff for all v / ∈ N , t → * v ⇒ v ∈ (X) * → .
Proof. For the "only-if" direction, we reason by induction on t ∈ SN . Assume that (t) → ⊆ X and let t

→ * v / ∈ N . Since t ∈ N , we have t → v → * v with v ∈ X. If v /
∈ N , then by Prop. 4.5 we have v ∈ (X) * → , hence v ∈ (X) * → . Otherwise, since (v) → ⊆ X we can apply the induction hypothesis and get v ∈ (X) * → .

For the converse, we also reason by induction on t ∈ SN . If t ∈ (X) * → then we are done since (t

) → ⊆ (X) * → ⊆ X. Assume that t / ∈ (X) * → . Let v ∈ (t) → . If v /
∈ N , then by assumption v ∈ (X) * → , hence v ∈ X. Otherwise, using (CR1) it suffices to show that (v) → ⊆ X. But by assumption, every v ∈ (v) * → \ N belongs to (X) * → . Hence by induction hypothesis (v) → ⊆ X.

that X = {t | t ∈ X} = {u | ∃t(u SN t ∧ t ∈ X)}, i.e. X ∈ O.
It is surprising that we can give such a simple structure to CR. The most important, however, is the consequence on the stability by union of CR. The property of SN neutral terms expressed in Prop. 4.10 is that a reduct u of a neutral term t such that t SN u is in some sense a principal reduct of t: the values of t are exactly those of u. Moreover, u ∈ max SN (t) → , i.e. a principal reduct is maximal among all possible reducts.

For λ2, this has to be linked with call-by-name languages, in which terms to be evaluated are neutral, and the evaluation preserves possible values. Definition 4.11. A term u ∈ (t) → is a principal reduct (written p.r.) of t iff t u and t is said to have the principal reduct property (written p.r.p.) when either such a u exists or t is a normal form.

We reduce the stability by union of CR to the principal reduct property for neutral terms.

Corollary 4.12. We have C ⊆ CR ⇒ C ∈ CR iff every t ∈ N ∩ SN has the principal reduct property.

As pointed out by Prop. 3.5, in order for t ∈ N to belong to C ∈ CR, C uses information on the behavior of t in elimination contexts. This information is given by the values of t, and clause (CR1) relies on the fact since t ∈ N , its values are that of (t) → . But if t SN u, the values of t are also values of u. That is, if u ∈ C and t SN u then t ∈ C, and it follows that t SN u implies t ∈ u. Moreover, Lem. 4.7 says that this exactly characterizes u: if it contains t, then the values of t are values of u. Now, recall that given C ⊆ CR, in order to get C ∈ CR we must show that if t ∈ N has (t) → ⊆ C, then every v ∈ (t) → must be in fact the same C ∈ C. This amounts to say that (t) → contains an u such that t SN u, hence that t has a principal reduct.

Stability by Union of CR in λ2

In this section, we show the p.r.p. for λ2. This leads to observe that reducibility candidates are exactly the Tait's saturated sets which are stable by reduction. We do not give the proofs that are subsumed by those for λ2U + , presented in Sec. 7.

The p.r.p. is a consequence of the standardization theorem of λ2. However, since we only need this property on SN terms, it can be proved using a weaker property, called weak standardization.

This property was coined in [START_REF] Altenkirch | Constructions, Inductive Types and Strong Normalization[END_REF] as a consequence of standardization. However, it admits a much direct proof, which rely on the orthogonality of the calculus. By the way, it is less a weak standardization property than a standardization for the weak head reduction, which corresponds to reduction in elimination contexts. Definition 5.1 (Weak Head Reduction). The relation → H of weak head reduction is defined as t → H u iff t = E[t ], t → β u and E[u ] = u. We denote by HNF the set of terms in → H -normal form.

Lemma 5.2 (Weak Standardization). Let t → β u and assume that E[t] → v with v = E[u]. Then v = E [t ] with (E[ ], t) → (E [ ], t ) and there exists u such that t → β u and E[u] → * E [u ].
In order to show that strongly normalizing neutral terms have the p.r.p., we use in addition the fact that HNF ∩ N (i.e. the set of terms of the from E[x]), is stable by reduction. We then obtain stability by union of CR, thanks to Cor. 4.12. Lemma 5.3 (Principal Reduct Property). Let t ∈ N ∩ SN . If there is u such that t → H u then it is a p.r. of t, otherwise every u ∈ (t) → is a p.r. of t. The principal reduct property of neutral terms corresponds to the fact that reducibility candidates are stable by strongly normalizing weak head expansions.

Lemma 5.5 (Weak Head Expansion and Reducibility Candidates

). Let C ∈ CR. If E[s] ∈ C, t → β s and t ∈ SN then E[t] ∈ C.
Weak head reduction is the main notion of the Krivine Abstract Machine, and stability by weak head expansion is the main property required by truth values of Krivine and Danos [START_REF] Danos | Disjunctive Tautologies as Synchronisation Schemes[END_REF].

Thanks to Cor. 4.9, we have shown that CR = O, thus giving a nice straight structure to CR. Moreover, Lem. 5.3, 4.7 and 5.5 imply that for all C ∈ CR,

(SAT 1) if E[x] ∈ SN then E[x] ∈ C; and (SAT 2) if E[s] ∈ C, t → β s and t ∈ SN , then E[t] ∈ C.
Subsets of SN satisfying (SAT 1) and (SAT 2) are Tait's saturated sets.

Definition 5.6. Let SAT be the set of all subsets S ⊆ SN satisfying (SAT 1) and (SAT 2). We denote by SAT → the collection of S ∈ SAT that are stable by reduction: If t ∈ S and t → u then u ∈ S (SAT 0).

The definition makes sense since in (SAT 1) we have E[x] ∈ SN , and, in (SAT 2) we have E[t] ∈ SN by Lem. 5.5.

The stability by union of CR is therefore linked with the fact that every C ∈ CR is saturated. This inclusion has been coined in [12]. The converse is false, as shown by a counter-example given in [START_REF] Werner | Une Théorie des Contructions Inductives[END_REF] (Lem. 3.16 pp. 87-88). It relies on the fact that saturated sets are not stable by reduction. However, we can show that saturated sets that are stable by reduction are exactly the reducibility candidates. This seems to have not been remarked before. 6 The System λ2U + of Product, Co-Product and Positive Iso-Recursive Types

We now extend results of the previous section by applying Cor. 4.12 to a system with more elaborated types. The system considered, called λ2U + , features product, co-product, positive iso-recursive types and the final type 1. It is a proper extension of λ2 [START_REF] Sp | Type Fixpoints: Iteration vs. Recursion[END_REF]. Our presentation is inspired by that of [START_REF] Abel | Termination Checking with Types[END_REF]. Types are extended with:

T, U ∈ T ::= . . . | T × U | T + U | µX.T | 1
where, in µX.T , X occurs only positively in T : any path from the root of T to an occurrence of X chooses the left argument of ⇒ an even number of times. The syntax of terms is enriched with corresponding introductions and eliminations:

s, t ∈ Λ ::= . . . | () | t, u | π i t i ∈ {1, 2} | inj i t | case (u, x 1 .t 1 , x 2 .t 2 ) i ∈ {1, 2} | in t | out t
We consider the following extension of β-reduction:

Example 6.1. Our motivation to consider λ2U + is that it is a very atomic calculus for inductives types. For example, polymorphic lists can be encoded as follows:

List = def ∀Y.µX.1 + Y × X nil = def in (inj 1 ()) cons (x, xs) = def in (inj 2 x, xs )
In [START_REF] Sp | Type Fixpoints: Iteration vs. Recursion[END_REF], it is shown that higher-order primitive recursion can be defined using iso-recursives types and the rule out (in t) → β t, and moreover that this rule can not be simulated in λ2 by means of β-reductions.

Reducibility and Stability by Union for λ2U +

We now introduce tools for reducibility in λ2U + . We then prove the p.r.p. and equivalence of CR and a suitable version of SAT → .

We define the top reduction as → β , and still denote by TNF the set of terms in top-normal form. It is convenient to factorize the introduction-elimination duality of natural deduction with the following atomic contexts: atomic eliminations contexts (aec) denoted by [ ] and atomic introduction contexts (aic) denoted by ι[ ] are defined as follows:

[ ] ::= [ ]t | π1[ ] | π2[ ] | case ([ ], x1.t1, x2.t2) | out [ ] ; ι[ ] ::= λx.[ ] | [ ], t | t, [ ] | inj 1 [ ] | inj 2 [ ] | in [ ] | () .
Note that the introduction context for the terminal type constructor is not linear. Hence, the terms nil and cons(x, l) of Ex. 6.1 are not neutral. This strengthen our intuition that non-neutral terms corresponds to values. Note that elimination contexts are a generalization of applicative contexts to product, coproduct and iso-recursive types. We can now substantiate our claim that is a weak observational preorder.

Proposition 7.3. t u iff ∀E[ ] (E[t] → * ι[h] ⇒ E[u] → * ι[h]).

Proof. Obviously, ∀E[ ] (E[t]

E[u]) implies t u (take the empty context). Conversely, assume that t u.

If E[t] → * ι[h], we are in the case that E[t] → * E [ι [h ]] → * ι[h] with (E[ ], t) → * (E [ ], ι [t ]). Since t u, we have u → * ι [h ], hence E[u] → * E [ι [h ]] → * ι[h].
We obtain CR by instantiating Def. 4.2 with λ2U + and N . Notions of weak head reduction and weak head normal forms are directly adapted from Sec. 5, with the obvious update of elimination contexts. Recall that u ∈ HNF iff for all E[ ], t such that u = E[t], we have t ∈ TNF. It follows that untyped terms in HNF ∩ N need not to be of the form E[x]. However, stability by reduction of HNF ∩ N still holds. Proof. We reason by structural induction on t. The case t ∈ X is trivial. Assume t = [t 1 ] and let t → t . Since t ∈ HNF, we have t

= [t 1 ] with (t 1 , [ ]) → (t 1 , [ ]), hence t ∈ N . If t 1 ∈ N , then t 1 ∈ N ∩ HNF and by induction hypothesis t 1 ∈ N ∩HNF. It follows that t = [t 1 ] ∈ HNF. Otherwise, t 1 = ι[t 2 ] with [ ] ⊥ ι[ ]. Hence, t 1 = ι [t 2 ] with (t 2 , ι[ ]) → (t 2 , ι [ ]), and [ ] ⊥ ι [ ]. Hence t = [ι [t 2 ]] ∈ HNF.
Unlike reducibility candidates, saturated sets are modified. They use elimination contexts in an essential way. The new clauses for SAT are the following: (SAT 1) HNF ∩ SN ∩ N ⊆ S. (SAT 2) If s ∈ S, t → H s and t ∈ SN then t ∈ S. As in Def. 5.6, we denote by SAT → the collection of saturated sets that are stable by reduction (axiom (SAT 0)).

Non-emptiness of SAT follows from Lem. 7.9. The clauses given for SAT are not common. They are usually replaced by: (SAT 1 ) If E[x] ∈ SN then E[x] ∈ S. (SAT 2 ) If E[s] ∈ S, t → β s and t ∈ SN then E[t] ∈ S. First, according to Lem. 7.9, (SAT 2 ) is equivalent to (SAT 2). Second, for the strong normalization proof, (SAT 1 ) is sufficient. But for the correspondence with Girard sets we use (SAT 1). The following suggests that (SAT 1 ) would have been sufficient if CR and SAT → have consists of well typed terms only. Proof. We begin by showing that CR ⊆ SAT → . Let C ∈ CR. (SAT 0) follows from (CR0). For (SAT 1), we can reason by induction on →, since by Prop. 7.4, HNF ∩ N ∩ SN is stable by reduction. Finally, the satisfaction (SAT 2) directly follows from Lem. 7.9. Conversely, we show that SAT → ⊆ CR. Let S ∈ SAT → . As above, (CR0) follows from (SAT 0). For (CR1), we have to show that for every neutral term v such that (v) → ⊆ S, then v ∈ S. First, v ∈ SN since (v) → ⊆ S ⊆ SN . Thus, we conclude by (SAT 1) if v ∈ HNF. Otherwise, v = E[t] with t → β s and E[s] ∈ S. Thus v ∈ S by (SAT 2).

Conclusion and Related Works

Related Works. There are interesting alternatives approaches, which may not rely on stability by union. Using bi-orthogonality (see [START_REF] Danos | Disjunctive Tautologies as Synchronisation Schemes[END_REF]), Melliès and Vouillon present a semantic of types that is not stable by union, and instead relies on a closer adequation between the interpretations and the typing rules [START_REF] Vouillon | Semantic Types: A Fresh Look at the Ideal Model for Types[END_REF].

Without unions and existentials, bi-orthogonals work well for strong normalization, especially for classical logic [START_REF] Parigot | Proofs of Strong Normalization for Second Order Classical Natural Deduction[END_REF]. With non-ambiguous left-linear calculus, it is not unreasonable to expect that they can deal with existentials and union types, but the proof would rely on non-trivial properties of the calculus.

Concluding Remarks. We have shown that, with some well-behaved calculi, Girard's reducibility candidates are stable by union. This was commonly believed to be false. Moreover, and maybe more important, we have shown that their definition hide a very simple structure, namely that candidates are exactly the non empty subsets of SN that are downward-closed w.r.t. the weak observational preorder SN .

This shed new light on the semantics of strong normalization. In particular, we hope that this can lead to precise comparisons of bi-orthogonal and candidates. A related question is to know when the soundness of elimination rules of union and existentials types can be proved without stability by union of some type interpretation.

Proposition 3 . 5 (

 35 Arrow Type Constructor). The arrow type constructor ⇒: P(Λ) × P(Λ) → P(Λ), defined as A ⇒ B = def {t | ∀u(u ∈ A ⇒ tu ∈ B)}, maps reducibility candidates A and B to a reducibility candidate.

Proposition 4 . 1 (

 41 Topological Closure of • ). Given a closure operator • : P(D) → P(D), let Ω be the set of non-empty X ⊆ D such that X = {x | x ∈ X}. Then Ω is the smallest set such that P(D) ⊆ Ω and C ⊆ Ω ⇒ C, C ∈ Ω.

Definition 4 .

 4 2 (λext-Reducibility Candidates). The set of λext-reducibility candidates, denoted by CR, is the set of all C ⊆ SN such that (CR0) if t ∈ C and t → u then u ∈ C, (CR1) if t ∈ N and (∀u (t → u ⇒ u ∈ C)) then t ∈ C.

  then t ∈ N and by induction hypothesis, (t) → ⊆ X i ⊆ C. Hence t ∈ C by (CR1). Thanks to Lem. 4.3, we have an explicit definition of the closure operator of CR, denoted by • . Now, Prop. 4.1 gives us Ω, which is the topological closure of • . We let CR = def Ω. Proposition. 4.1 implies that CR ⊆ CR and that CR is stable by union iff CR = CR.

Definition 4 . 4 .

 44 Let t u iff for all v / ∈ N , t → * v ⇒ u → * v. We denote by SN the restriction of to SN .

Corollary 4 .

 4 9. CR is stable by union iff CR = O. The structure of reducibility candidates is at a first sight not trivial and somehow mysterious. It is therefore extremely interesting to understand what allows CR = O, giving them a so simple structure. Hence the question of their stability by union reveals important facts on their fundamental nature. The next step is to characterize what implies CR = O. Recall that Thm. 4.8 says that CR ⊆ O.

Proposition

Theorem 5 . 4 .

 54 If C ⊆ CR then C ∈ CR.

Theorem 5 . 7 .

 57 SAT → = CR.Proof. The inclusion CR ⊆ SAT has been coined in[12]. It is a direct consequence of Lem. 5.5 and the stability by reduction of head-normal forms.The converse, SAT → ⊆ CR, does not seem to have been published before. Let S ∈ SAT → . It satisfies (CR0) thanks to (SAT 0). As for (CR1), let v ∈ N such that (v) → ⊆ S. Thus v ∈ SN . If v ∈ HNF, then v = E[x] ∈ S by (SAT 0). Otherwise, v = E[t] with t → β uand E[u] ∈ S by assumption. Hence v ∈ S by (SAT 2).

Proposition 7 . 4 .

 74 If t ∈ HNF ∩ N and t → u, then u ∈ HNF ∩ N .

Proposition 7 . 10 .

 710 Well typed terms in N are the terms of the form E[t] where either t ∈ X or t / ∈ TNF. Theorem 7.11. SAT → = CR.

  Terms come with the usual notion of β-reduction, namely (λx.t)u → β t[u/x], where t[u/x] is the captureavoiding substitution of x by u in t. We let → be the smallest rewrite relation on Λ containing → β . In the following, we refer to → β as the top reduction and denote by TNF the set of terms in → β -normal form. We let (t) → = def {u | t → u} and (t) * → = def {u | t → * u}, where → * is the reflexive-transitive closure of →. We write (t 1 , . . . , t n ) → (t 1 , . . . , t n ) iff there is i such that t i → t i and t j = t j for all j = i. A term t is strongly normalizing iff every reduction sequence issued from t is finite. Let SN be the set of strongly-normalizing terms. Note that t ∈ SN iff either t is not reducible or all its reducts are in SN . It follows that SN is the smallest set such that for all t,

  and C ∈ Ω. Moreover, if t ∈ C, then for all C ∈ C, t ∈ C hence t ⊆ C. Therefore t ⊆ C, and it follows that C = {t | t ∈ C}, i.e. C ∈ Ω. Now, let Ω ⊇ P(D) be stable by union and intersection

  Thanks to Proposition 4.6, each t is in fact an initial segment w.r.t. SN . Lemma 4.7. For all t ∈ SN , t = {u | u SN t}. Proof. By Prop. 4.6, u ∈ t iff t, u ∈ SN and either t → * u or u ∈ N and (u) * → \ N ⊆ (t) * → . But this is exactly u SN t. This gives a nice straight structure to the elements of CR. Theorem 4.8. Let O be the set of non empty subsets of SN which are downward closed w.r.t. SN , i.e. X ∈ O iff ∅ = X ⊆ SN and for all t, u, if t ∈ X and u SN t then u ∈ X. Then we have CR = O. Proof. Thanks to Lem. 4.7, we have X ∈ CR iff it is a non-empty subset of SN such

  4.10. O ⊆ CR iff for all t ∈ N ∩ SN , there is u ∈ (t) → such that t SN u. Proof. Let C ∈ O. Since it is stable by reduction, it suffices to check that if t ∈ N and (t) → ⊆ C, then t ∈ C. But there is u ∈ (t) → such that t SN u, and u ∈ C implies t ∈ C. Therefore, C ∈ CR. Conversely, assume that O ⊆ CR. Let t ∈ N ∩ SN and X = def {u | t → u}. By Lem. 4.7, we have X ∈ O ⊆ CR, hence t ∈ X since t ∈ N and (t) → ⊆ X. It follows that there is some u ∈ (t) → such that t SN u.

  The columns of the above array define a relation written [ ] ⊥ ι[ ]. We have [ ] ⊥ ι[ ] when [ι[ ]] is a β-redex, except for the product, where we let Then, to each aec [ ] corresponds the set [ ] ⊥ of aic ι[ ] such that [ ] ⊥ ι[ ], and conversely, ι[ ] ⊥ is the set of aec [ ] such that [ ] ⊥ ι[ ]. In the following, we will sometime write unambiguously ι[ ] ⊥ [ ] instead of [ ] ⊥ ι[ ]. The extension of elimination contexts E[ ] is obvious: E[ ] ::= [ ] | [E[ ]]. Proposition 7.1. If E[ [t]] → v, then v = E [t ] with (E[ ], [t]) → (E [ ], t ).

		π 1 [ ] ⊥ [ ], t	and	π 2 [ ] ⊥ t, [ ]
	but	π 2 [ ] ⊥ [ ], t	and	π 1 [ ] ⊥ t, [ ] .

Proof. By structural induction on

E[ ]. The case E[ ] = [ ] is obvious. In the other cases, we have E[ ] = [F [ ]]. First, the reduction [F [ [t]]] → v can not be a top reduction. Hence we have v = [v ] with ( [ ], v) → ( [ ], v ),

and by induction hypothesis

v = F [t ] with (F [ ], t) → (F [ ], t ). Take E [ ] = [F [ ]].

Definition 7.2. We say that terms not of the form ι[t] are neutral and denote by N the set of neutral terms.

(Ax) Γ, x : T x : T(⇒ I) Γ, x : U t : T Γ λx.t : U ⇒ T (⇒ E) Γ t : U ⇒ T Γ u : U Γ tu : T (∀ I) Γ t : T Γ t : ∀X.T (X / ∈ V(Γ )) (∀ E) Γ t : ∀X.T Γ t : T [U/X]Existential and Union Types. Our main point is to prove the soundness (w.r.t. some closure operator) of elimination rules of union and implicit existential types. Such types are manipulated with type-assignment rules, in the spirit of[START_REF] Macqueen | An Ideal Model for Recursive Polymorphic Types[END_REF][START_REF] Barbanera | Intersection and Union Types: Syntax and Semantics[END_REF]. Typical rules for these systems are:(∃ I) Γ t : T [U/X] Γ t : ∃X.T (∃ E) Γ t : ∃X.T Γ, x : T u : U Γ u[t/x] : U (X / ∈ V(Γ, U )) (∪I) Γ t : Ti Γ t : T1 ∪ T2 (i ∈ {1, 2}) (∪E)Γ t : T1 ∪ T2 ∀i ∈ {1, 2}, Γ, x : Ti u : U Γ u[t/x] : U

π i t 1 , t 2 → β t i case (inj i u, x 1 .t 1 , x 2 .t 2 ) → β t i [u/x i ] out (in t) → β t .We let → be the smallest rewrite relation on Λ containing → β . The type system is enriched with the following additional rules:(1 I) Γ () : 1 (×I) Γ t1 : T1 Γ t2 : T2 Γ t1, t2 : T1 × T2 (×E) Γ t : T1 × T2 Γ πit : Ti (i ∈ {1, 2}) (+I) Γ t : Ti Γ inj i t : T1 + T2 (i ∈ {1, 2}) (+E) Γ t : T1 + T2 Γ, x : Ti ti : U Γ case (t,x1.t1, x2.t2) : U (µI) Γ t : T [µX.T /X] Γ in t : µX.T (µE) Γ t : µX.T Γ out t : T [µX.T /X]

Acknowledgments. The author thanks Frédéric Blanqui and Claude Kirchner for useful advices, support and comments, and Marco Gaboardi for a plenty of interesting discussions. Antoine Reilles suggested interesting improvements in the presentation, and the anonymous referees made interesting insightful comments.

We now turn to weak standardization. It is stated and used for λ2U + in [START_REF] Abel | Termination Checking with Types[END_REF]. Proposition 7.5. If t → β u and t → v, then either v = u or there exists u such that v → β u ← * u.

Proof. By cases on t → β u. t = (λx.t 1 )t 2 . In this case,


Keywords: Phenotypic plasticity, Evolution, Gene expression, Review 44

Phenotypic plasticity, the ability of a given genotype to produce 21 different phenotypes in response to distinct environmental conditions, is 22 widely observed in the wild. It is believed to facilitate evolution and, under 23 the "flexible stem hypothesis", it is thought that an ancestral plastic species 24 can be at the origin of sister lineages with divergent phenotypes fixed by 25 genetic assimilation of alternative morphs. We review here the genetic 26 mechanisms underlying such phenomenon. We show several examples in 27 which the same gene shows transcriptional plasticity in response to 28 environmental factors and divergence of expression within or between 29 species. Thus, the same gene is involved both in the plasticity of a trait and 30 in the evolution of that trait. In a few cases, it can be traced down to cis--31 regulatory variation in this gene and, in one case, in the very same 32 regulatory sequence whose activity is modulated by the environment. 33 These data are compatible with the "flexible stem hypothesis" and also 34 suggest that the evolution of the plasticity of a trait and the evolution of the 35 trait are not completely uncoupled as they often involve the same locus. 36 Furthermore, the "flexible stem hypothesis" implies that it is possible to 37 canalize initially plastic phenotypes. Several studies have shown that it was 38 possible through modification of chromatin regulation or hormonal 39 signalling/response. Further studies of phenotypic plasticity in an 40 evolutionary framework are needed to see how much the findings 41 described in this review can be generalized.

The flexible stem hypothesis: evidence from genetic data 1 2 Jean--Michel Gibert 3 4 Sorbonne Universités, UPMC Univ Paris 06, CNRS, Biologie du Développement 5 Paris Seine, Institut de Biologie Paris Seine (LBD--IBPS), 75005 Paris, France. 6 7 e--mail: jean--michl.gibert@upmc.fr 8 tel: 00 33 1 44 27 58 42 9

Orcid number: 0000--0002--1579--0266 10 11

Acknowledgments: I thank Sophie Gournet for the drawings illustrating this 12 review. I thank Frédérique Peronnet, Emmanuèle Mouchel--Vielh and Virginie 13 Courtier--Orgogozo for critical reading of the manuscript and stimulating 14 discussions. I thank the two anonymous reviewers for comments that 15 significantly enriched the manuscript. 16 17 18 45

In developmental biology, the environment has long been thought to fulfil 46 essentially a permissive role, simply providing the required conditions for 47 normal development to occur. Thus, most developmental biology laboratories 48 still use standardized environmental conditions and focus on genetic factors to 49 dissect developmental mechanisms. However, in many cases the environment 50 has an instructive role, directing the development to particular alternative path 51 [START_REF] Gilbert | Ecological developmental biology: developmental biology 531 meets the real world[END_REF]. Phenotypic plasticity is a major concept which describes "the 52 property of a given genotype to produce different phenotypes in response to 53 distinct environmental conditions" [START_REF] Pigliucci | Phenotypic Plasticity, Beyond Nature and Nurture[END_REF]. It is widely observed in the 54 wild, and this concept was formulated by Bradshaw in the sixties (Bradshaw 55 1965). Phenotypic plasticity can be an adaptation to fluctuating environments 56 such as seasonal variations, presence/absence of predators, or population 57 density. It can also be non adaptive and Schmalhausen used the term "morphose" 58 to describe aberrant phenotypes induced by extreme environmental conditions 59 [START_REF] Schmalhausen | Factors of Evolution, The Theory of Stabilizing Selection[END_REF]. A major tool to illustrate phenotypic plasticity is the 60 reaction norm, first drawn by [START_REF] Woltereck | Weitere experimentelle unters¨uchungen ¨uber 649 artver¨anderung, speziell ¨uber das wesen quantitativer artunterschiede 650 bei daphniden[END_REF] [START_REF] Woltereck | Weitere experimentelle unters¨uchungen ¨uber 649 artver¨anderung, speziell ¨uber das wesen quantitativer artunterschiede 650 bei daphniden[END_REF], which 61 represents the value of a quantitative phenotype produced by a given genotype 62 in function of an environmental parameter. Note that "genotype" and "phenotype" 63 were defined only shortly after by [START_REF] Johannsen | The genotype conception of heredity[END_REF] who reinterpreted the 64 reaction norms of Woltereck [START_REF] Johannsen | The genotype conception of heredity[END_REF]. Indeed, Woltereck observed 65 that different pure lines could produce different morphologies in a given 66 environment but the same morphology in another environment. He interpreted 67 this as inconsistent with the existence of constant differences between the 68 genotypes. Because he did not distinguish between genotypes and phenotypes, 69 he thought that the different pure lines had the same genotype in a given 70 environment (when they had the same phenotype) and different genotypes in 71 another environment (when they had different phenotypes). When phenotypic 72 plasticity leads to discrete morphs, these morphs are called polyphenisms. 73

Phenotypic plasticity can generate, within a single species, morphological 74 differences of a magnitude usually observed between distantly related species. 75

As selection operates on phenotypes, this direct input of the environment on the 76 expression of the genotype must be taken into account to understand 77 evolutionary processes. This was clearly formulated by [START_REF] Schmalhausen | Factors of Evolution, The Theory of Stabilizing Selection[END_REF] 78 [START_REF] Schmalhausen | Factors of Evolution, The Theory of Stabilizing Selection[END_REF]: "Darwin has previously noted the fundamental importance 79 of inherited variability (mutations) for the evolution of organisms. However, 80 mutations have different expressions under diverse conditions. If natural selection 81 is the basic factor in evolution, then the concrete expression of individual 82 characteristics under given environmental conditions is of decisive importance in 83 this process ». Thus, the role of phenotypic plasticity in evolution has been 84

actively discussed [START_REF] Pfennig | Phenotypic plasticity's 571 impacts on diversification and speciation[END_REF][START_REF] Moczek | The role of developmental plasticity in 562 evolutionary innovation[END_REF][START_REF] Laland | Does evolutionary theory need a 547 rethink?[END_REF]Laland et al. , 85 2015;;[START_REF] Schneider | How plasticity, genetic assimilation and cryptic 589 genetic variation may contribute to adaptive radiations[END_REF]. The issue is complex and certain empirical 86 results suggest that it is important to distinguish between adaptive and non--87 adaptive plasticity as they may have opposite effects on genetic divergence 88 [START_REF] Ghalambor | Non--adaptive plasticity 516 potentiates rapid adaptive evolution of gene expression in nature[END_REF]. 89

The idea that an ancestral plastic species could have been at the origin of 90 divergent lineages with pronounced phenotypic differences has been proposed 91 by Mary--Jane West--Eberhard as the "flexible stem hypothesis" (West--Eberhard 92 2003). It is intimately linked to the process of genetic assimilation discovered by 93 Conrad Waddington more than 50 years ago [START_REF] Waddington | Selection of the genetic basis for an acquired character[END_REF][START_REF] Waddington | Genetic Assimilation of the Bithorax Phenotype[END_REF][START_REF] Waddington | Canalization of development and genetic assimilation of 626 acquired characters[END_REF]. In 94 his experiments on Drosophila, Waddington showed that a phenotype initially 95 induced by the environment can be fixed by selection and become constitutively 96 expressed even in the absence of the initial environmental factor. Most of these 97 experiments were based on developmental defects induced by stressors such as 98 heatshock (crossveinless phenotypes on wings) [START_REF] Waddington | Selection of the genetic basis for an acquired character[END_REF] or ether 99 vapour (bithorax phenocopies) [START_REF] Waddington | Genetic Assimilation of the Bithorax Phenotype[END_REF]). However, they could be 100 generalized to adaptive phenotypes and had therefore major evolutionary 101 implications. Indeed, in another Waddington experiment, the morphological 102 change induced by the environment, i.e. size increase of the anal papilla of larvae 103 in response to high salt concentration, was likely adaptive and was also 104 genetically assimilated [START_REF] Waddington | Canalization of development and genetic assimilation of 626 acquired characters[END_REF]. Importantly, genetic assimilation is a 105 genuine evolutionary process based on selection of genetic variation existing in 106 the population submitted to environmental changes. Indeed, Waddington 107 experiments were later repeated by Bateman on outbred or isogenized stocks 108 and it was shown that genetic assimilation did not happen in the absence of 109 genetic variation in the population [START_REF] Dworkin | Towards a genetic architecture of cryptic genetic variation and 505 genetic assimilation: the contribution of K. G. Bateman[END_REF]. This genetic variation is 110 cryptic in the original environment in which it accumulates as it has no 111 phenotypic consequences. This genetic variation translates into phenotypic 112 variation in the new environment, which allows genetic assimilation by 113 selection. Thus, a lineage characterized by a constitutively expressed morph 114 could evolve from a plastic ancestor by genetic assimilation of a phenotype 115 initially induced by environmental change. 116

This has lead Mary Jane West--Eberhard to propose that genes act more as 117 followers than as leaders during evolution [START_REF] West | Developmental plasticity and the origin of species 630 differences[END_REF]. Although very 118 stimulating, this idea cannot be generalized to the evolution of all traits. Indeed, 119 in many examples, genetic polymorphisms have played a major role in the origin 120 of a phenotype later fixed during evolution [START_REF] Schwander | Genes as leaders and followers in evolution[END_REF]. For 121 example, a particular allele of the pigmentation gene tan leading to lighter 122 pigmentation is segregating in Drosophila americana and has been fixed in its 123 sister species Drosophila novamexicana which has a derived pale phenotype 124 (Wittkopp et al. 2009). However, although the "plasticity first hypothesis" does 125 not apply to all traits, it is worth investigating it empirically. The flexible stem 126 model of adaptive radiation predicts that the pattern of phenotypic divergence 127 between derived lineages should mirror the pattern of developmental plasticity 128 in their common ancestor [START_REF] Wund | A test of the "flexible stem" model of 652 evolution: ancestral plasticity, genetic accommodation, and 653 morphological divergence in the threespine stickleback radiation[END_REF]. Several studies have provided 129 empirical morphological data strongly suggesting that it could occur in nature 130 [START_REF] Wund | A test of the "flexible stem" model of 652 evolution: ancestral plasticity, genetic accommodation, and 653 morphological divergence in the threespine stickleback radiation[END_REF]. For example, the pharyngeal jaws of midas cichlids show a 131 morphological plasticity in response to the hardness of the diet which parallels 132 the morphological diversity observed between specialised species (Muschick et 133 al. 2011). Similarly, stress--induced changes in mandible shape in Sorex shrews 134 correspond to traits showing divergence between species (Badyaev and 135 Foresman 2000). 136

What we would like to review and discuss in this article is the underlying genetic 137 bases of the flexible stem hypothesis. Indeed, under this hypothesis, it is 138 expected that the genetic mechanisms that generate the plastic phenotypes 139 should be the same as those that generate the phenotypic divergence. The idea 140 that phenotypic plasticity is under genetic control was initially developed by 141 Bradshaw [START_REF] Bradshaw | Evolutionary Significance of Phenotypic Plasticity in Plants[END_REF]) and a recurrent question was the existence and the 142 nature of "plasticity genes" [START_REF] Via | Adaptive phenotypic plasticity: 620 consensus and controversy[END_REF]. However, Via considered that 143 modifications of reaction norms was an indirect consequence of the selection on 144 the mean phenotype in each separate environment and that no plasticity genes 145 were required [START_REF] Via | Adaptive phenotypic plasticity: target or by--product of selection in a 618 variable environment?[END_REF]. Scheiner, Schlichting and Pigliucci objected to Via that 146 the plasticity of a trait could evolve independently of the mean of the trait 147 because the plasticity and the mean of the trait are under the control of different 148 genes [START_REF] Scheiner | Plasticity as a Selectable Trait: Reply to Via[END_REF][START_REF] Schlichting | Control of phenotypic plasticity via regulatory 585 genes[END_REF]. This debate settled down 149 in the mid nineties in favour of the existence of plasticity genes. Two kinds of 150 genetic mechanisms involved in phenotypic plasticity were proposed (Via et al. 151 1995). The first one, "allelic sensitivity", refers to alleles expressed differently in 152 distinct environment. This could correspond to a single gene showing 153 transcriptional plasticity or to an enzyme active in only some environmental 154 conditions for example. The second genetic mechanism, "gene regulation", 155 corresponds to a regulatory switch under environmental control, which would 156 lead to the activation of a panel of target genes depending on the environment. 157

Obviously, the two mechanisms may blur as the regulatory locus influences the 158 amount of products of its targets, thus mediating allelic sensitivity (Via et al. 159 1995). Clearly, a great deal of information could be gained by genetic dissection 160 of phenotypic plasticity in a variety of organisms. 161

A few empirical studies have identified genes involved in the phenotypic 162 plasticity of particular traits and in several cases, data are available regarding 163 genes involved in the variation within or between species of the traits of interest. 164 Thus, it is possible to analyse the genetic changes that underlie genetic 165 assimilation of initially plastic traits. Furthermore, several studies have dissected 166 the mechanisms involved in phenotypic plasticity and environmental 167 canalization. The typical questions we would like to address are the following: 168 What are the relationships between genes involved in phenotypic plasticity of a 169 trait and genes involved in the evolution of this trait? What kind of mutations are 170 selected during the evolution of these traits? Are they regulatory or coding 171 mutations? Do they target cis--regulatory sequences of a modulated gene or trans--172 acting factors? How is it possible to make independent of the environment an 173

Ether--induced Ultrabithorax phenocopies in Drosophila 185

Treatment of Drosophila embryos with ether vapor leads to phenocopies of the 186 bithorax mutant in adults [START_REF] Waddington | Genetic Assimilation of the Bithorax Phenotype[END_REF]). This corresponds to partial 187 homeotic transformation of the third thoracic segment into the second thoracic 188 segment. In Drosophila, like in all dipterans, the dorsal appendages of the third 189 thoracic segments are not wings but little round structures named halteres. In 190 bithorax phenocopies, halteres are partially transformed into wings and the 191 postnotum is partially transformed into an additional mesonotum (Figure 1). 192

Waddington showed that this ether--induced phenotype can be genetically 193 assimilated [START_REF] Waddington | Genetic Assimilation of the Bithorax Phenotype[END_REF]. By selection after ether treatment at each 194 generation, he could progressively increase the proportion of individual showing 195 the bithorax phenocopy. At the eighth generation, this phenotype was observed 196 in some individuals even in the absence of ether treatment (Figure 1). The 197 bithorax phenotype was therefore genetically assimilated. Waddington 198 experiments were repeated by Gibson and Hogness [START_REF] Gibson | Effect of polymorphism in the Drosophila 529 regulatory gene Ultrabithorax on homeotic stability[END_REF]. 199

They analysed the expression of the homeotic gene Ultrabithorax (Ubx) which is 200 expressed in haltere but not wing imaginal disc and is responsible for the 201 different identities of these organs. They showed that ether--induced bithorax 202 phenocopies are caused by clonal loss of expression of Ubx in the haltere 203 imaginal disc. Furthermore, using polymorphism in Ubx, they could show that 204 the frequency of particular alleles of Ubx increased during genetic assimilation of 205 the bithorax phenotype. The Ubx polymorphism was not the only source of 206 genetic variation affecting sensitivity to ether, but it had a major effect. Thus, Ubx 207 expression is sensitive to ether and during genetic assimilation of this 208 phenotype, artificial selection targeted the Ubx locus itself. 209 210

Transcriptional response to osmotic challenge in killifish: 211

The Atlantic killifish (Fundulus heteroclitus) can be found along a steep salinity 212 gradient in Atlantic coast estuaries and can quickly adjust to extremes in 213 environmental salinity (Figure 2). Thus, this species is able to occupy an 214 extremely wide osmotic niche. Hypo--osmotic challenge induces a change of 215 cellular morphology of the apical surface of the gill epithelium (Whitehead et al. 216 2011) (Figure 2). In sea water, the apical surface of the gill epithelium is made of 217 pavement cells interspersed with mitochondrion--rich cells possessing apical 218 crypt with small surface area [START_REF] Whitehead | Genomic mechanisms of 632 evolved physiological plasticity in killifish distributed along an 633 environmental salinity gradient[END_REF]. Exposure to fresh water 219 leads to enlargement of the apical surface of mitochondrion--rich cells. This 220 modification occurs within a few days, but its speed and the precise morphology 221 of the gill epithelium differs between populations originating from different 222 point of the salinity gradient. Analysis of the transcriptome of gills in fish 223 submitted to hypo--osmotic challenge allowed to identify sets of genes whose 224 expression was modulated by salinity [START_REF] Whitehead | Genomic mechanisms of 632 evolved physiological plasticity in killifish distributed along an 633 environmental salinity gradient[END_REF]. It was found that 225 genes showing transcriptional plasticity during osmotic challenge are more 226 likely to show divergence of expression between populations living in different 227 environment [START_REF] Whitehead | Genomic mechanisms of 632 evolved physiological plasticity in killifish distributed along an 633 environmental salinity gradient[END_REF][START_REF] Whitehead | Salinity--and population--636 dependent genome regulatory response during osmotic acclimation in the 637 killifish (Fundulus heteroclitus) gill[END_REF]. Indeed, many of the genes 228 modulated during hypo--osmotic challenge show adaptive divergence in 229 expression in populations living exclusively in freshwater habitat. Among these 230 genes, many have a well known role in osmotic regulation, for example 231 Aquaporin 3 (AQP3), the sodium/potassium transporting ATPAse ATP1A1 or 232 versican (VCAN) [START_REF] Whitehead | Salinity--and population--636 dependent genome regulatory response during osmotic acclimation in the 637 killifish (Fundulus heteroclitus) gill[END_REF]. 233 234

Plasticity of wing eyespots in the butterfly Bicyclus anynana 235

The African satyrine butterfly Bicyclus anynana shows seasonal polyphenisms. In 236 the wet season morph, conspicuous eyespots made of concentric rings of 237 differently pigmented scales are observed on the ventral wings. In the dry season 238 morph, the ventral eyespots are absent. Only a reduced version of the white spot 239 in the centre of the eyespot is visible. The wet and dry season morphs can be 240 produced in the laboratory by rearing the larvae at 27°C or 17°C respectively 241 [START_REF] Brakefield | Development, plasticity and evolution 497 of butterfly eyespot patterns[END_REF]) (Figure 3). 242

Many developmental regulatory genes are expressed in developing eyespots of 243

Bicyclus anynana, among which Distal--less (Dll) which is expressed in the future 244 centre of the eyespot [START_REF] Brakefield | Development, plasticity and evolution 497 of butterfly eyespot patterns[END_REF][START_REF] Shirai | Evolutionary history of the 598 recruitment of conserved developmental genes in association to the 599 formation and diversification of a novel trait[END_REF]. This is not 245 simply a correlation as it was recently shown by gain and loss of function 246 experiments using transgenic Bicyclus anynana that Dll is involved in eyespot 247 formation [START_REF] Monteiro | Distal--less regulates eyespot 564 patterns and melanization in Bicyclus butterflies[END_REF]. Indeed, overexpression of Dll increases eyespot 248 size and induces ectopic eyespots. Conversely, decreasing Dll expression reduces 249 eyespot size. Furthermore, the expression of Dll in presumptive eyespots is 250 modulated by temperature: it is stronger and wider in pupae grown at 27°C that 251 will produce the wet season morph [START_REF] Brakefield | Development, plasticity and evolution 497 of butterfly eyespot patterns[END_REF]. Thus, Dll is one of 252 the genes involved in eyespot plasticity. 253

It is possible to fix alternative morphs by artificial selection performed at 254 intermediate temperature. This lead to a LOW line and a HIGH line showing 255 almost non plastic dry season and wet season phenotypes, respectively 256 [START_REF] Brakefield | Development, plasticity and evolution 497 of butterfly eyespot patterns[END_REF]) (Figure 3). Thus, the wet or dry season morphs can be 257 genetically assimilated and become virtually independent of the rearing 258 temperature. This correlates with a modification of Dll expression, which is 259 stronger and wider in pupae of the HIGH line than in pupae of the LOW line 260 grown in the same environmental conditions. Thus, genetic assimilation of the 261 alternative seasonal morphs has involved modulation of Dll expression. Whether 262 this genetic assimilation was caused by selection at the Dll locus itself (cis 263 variation) or by trans--acting factors was not tested in this experiment. However, 264 another selection experiment targeting the size of dorsal eyespots (which 265 however are not plastic), showed that natural genetic variation in Dll was linked 266 to eyespot size variation in Bicyclus anynana [START_REF] Beldade | Contribution of Distal--less to 488 quantitative variation in butterfly eyespots[END_REF]. Thus, 267 variation at the Dll locus with significant impact on eyespot patterning exists in 268

Bicyclus anynana. 269

It is thought that the stem species in diplogastrid nematods was polyphenic 295 [START_REF] Kiontke | Phenotypic plasticity: different teeth for different 539 feasts[END_REF]. Many descendant species such as Pristionchus pacificus 296 have kept both morphs, but others have become exclusively Eu or St. 297 Interestingly, recent morphometric analysis of diplogastrid mouth structures in 298 a more global evolutionary framework revealed a rapid process of diversification 299 associated with developmental plasticity [START_REF] Susoy | Rapid diversification 608 associated with a macroevolutionary pulse of developmental plasticity[END_REF]: The gain of 300 dimorphic mouth structures was associated with an increase rate of evolution 301 and the appearance of numerous new species with diversified mouth parts. 302 303

Modulation of leaf margin dissection by temperature in Capsella 304

The two brassicaceae sister species Capsella rubella and Capsella grandiflora 305 show differences in leaf margin dissection [START_REF] Sicard | Repeated evolutionary changes of leaf 602 morphology caused by mutations to a homeobox gene[END_REF]. Leaf margin 306 dissection is more pronounced in Capsella rubella and is increased at low 307 temperature (16°C versus 22°C). It was shown that the major locus responsible 308 for the difference in leaf margin dissection between C. rubella and C. grandiflora 309 is the homeobox gene RCO--A which is expressed in sinuses between growing 310 lobes of developing leaves in C. rubella [START_REF] Sicard | Repeated evolutionary changes of leaf 602 morphology caused by mutations to a homeobox gene[END_REF]. This difference of 311 expression level is caused by insertions in the C. rubella RCO--A promoter. The 312 effect of the RCO--A region on leaf margin dissection is visible in nearly isogenic 313 lines differing only in the region of RCO--A, NILgg (carrying the RCO--A allele of C. 314 grandiflora) and NILrr (carrying the RCO--A allele of C. rubella) (Figure 5). In 315 addition, RCO--A expression is strongly modulated by temperature. Expression of 316 the C. grandiflora RCO--A allele is extremely weak at 22°C and the leaves show no 317 dissection. This allele is up--regulated more than 150 folds at 16°C compared to 318 22°C, which leads to leaf margin dissection. The C. rubella RCO--A allele is more 319 expressed than the C. grandiflora one at 22°C and is upregulated less than 5 folds 320 between 22°C and 16°C. Consequently, it leads to leaf margin dissection at both 321 temperatures in C. rubella. 322

In another brassicae species, Arabidopsis thaliana, the RCO--A locus is deleted and 323 there is no leaf margin dissection. Insertion of transgenes carrying Capsella 324 rubella RCO--A gene in Arabidopsis thaliana is sufficient to induce leaf margin 325 dissection [START_REF] Sicard | Repeated evolutionary changes of leaf 602 morphology caused by mutations to a homeobox gene[END_REF]. 326 Thus, the same locus is directly involved in phenotypic plasticity and species 327 divergence regarding leaf margin dissection. However, as the activity of the 328 regulatory sequences of RCO--A responsible for the difference of expression 329 between the two Capsella species was not studied with a reporter gene in 330 transgenic lines grown at different temperatures, it is not known whether they 331 also mediate the effect of the environment. 332 333

Thermal plasticity of abdominal pigmentation in Drosophila melanogaster 334 females 335

Cold induces melanism in many insects [START_REF] Gibert | Developmental constraints on an adaptive 526 plasticity: reaction norms of pigmentation in adult segments of 527 Drosophila melanogaster[END_REF][START_REF] Michie | Melanic through nature or 558 nurture: genetic polymorphism and phenotypic plasticity in Harmonia 559 axyridis[END_REF]336 Fedorka et al. 2013). This is thought to be beneficial as dark pigmentation 337 increases body temperature. However, pigmentation is highly pleiotropic and is 338 also correlated to many other traits such as longevity, fecundity or immunity 339 [START_REF] Wittkopp | Development and evolution of insect 640 pigmentation: genetic mechanisms and the potential consequences of 641 pleiotropy[END_REF][START_REF] Fedorka | Seasonality influences 512 cuticle melanization and immune defense in a cricket: support for a 513 temperature--dependent immune investment hypothesis in insects[END_REF][START_REF] Kutch | Thermoregulatory strategy 544 may shape immune investment in Drosophila melanogaster[END_REF]Rajpurohit 340 et al. 2016). In Drosophila melanogaster females, abdominal pigmentation is 341 strongly modulated by temperature (Figure 6). This is particularly pronounced 342 in the more posterior segments (A5, A6 and A7) [START_REF] Gibert | Developmental constraints on an adaptive 526 plasticity: reaction norms of pigmentation in adult segments of 527 Drosophila melanogaster[END_REF]. 343

Correspondingly, the expression of several genes encoding the enzymes of the 344 cuticular pigment synthesis pathway in the abdominal epidermes of late pupae 345 and young adults is modulated by temperature [START_REF] Gibert | Phenotypic Plasticity 519 through Transcriptional Regulation of the Evolutionary Hotspot Gene tan 520 in Drosophila melanogaster[END_REF][START_REF] Gibert | Modulation of yellow expression 523 contributes to thermal plasticity of female abdominal pigmentation in 524 Drosophila melanogaster[END_REF]. 346 However, among them, the gene tan stands out, being expressed seven times 347 more in the abdominal epidermis of young females grown at 18°C than 29°C. The 348 activity of tan increases melanin production and genetic experiments showed 349 that temperature modulation of tan expression plays an essential role in thermal 350 plasticity of female abdominal pigmentation [START_REF] Gibert | Phenotypic Plasticity 519 through Transcriptional Regulation of the Evolutionary Hotspot Gene tan 520 in Drosophila melanogaster[END_REF]. Furthermore, 351 temperature modulates the activity of the tan abdominal enhancer (t_MSE) and 352 the level of the active histone mark H3K4me3 on tan promoter. Interestingly, tan 353 is well known for its involvement in pigmentation variation and divergence in 354 the Drosophila melanogaster species subgroup. In Drosophila melanogaster, 355 independent genome wide association studies performed on European, African 356 and American populations have identified single nucleotide polymorphisms in 357 the t_MSE involved in variation of female abdominal pigmentation (Bastide et al. 358 2013;[START_REF] Dembeck | Genetic Architecture of 502 Abdominal Pigmentation in Drosophila melanogaster[END_REF][START_REF] Endler | Reconciling Differences in 508 Pool--GWAS between Populations: A Case Study of Female Abdominal 509 Pigmentation in Drosophila melanogaster[END_REF]. In Drosophila erecta, female 359 dimorphic pigmentation is caused by genetic variation in the t_MSE maintained 360 by balancing selection [START_REF] Yassin | Ancient balancing selection at tan 656 underlies female colour dimorphism in Drosophila erecta[END_REF]. In Drosophila santomea, several 361 independent loss of function mutations located in the t_MSE have lead to the light 362 phenotype of this species, whereas in the sister species Drosophila yakuba a 363 functional t--MSE enhancer is associated with dark abdominal pigmentation 364 [START_REF] Jeong | The evolution of gene regulation 535 underlies a morphological difference between two Drosophila sister 536 species[END_REF]. Thus, in the Drosophila melanogaster species subgroup, 365 plasticity and variation between species of abdominal pigmentation work 366 through modulation of the same gene and involves genetic changes in the very 367 same regulatory sequence, t_MSE, that also mediates the effect of temperature on 368 tan expression in Drosophila melanogaster. 369 370

Discussion 371

These examples demonstrate that several genes showing transcriptional 372 plasticity in response to environmental changes are differentially expressed 373 within and/or between species and contribute to phenotypic variation and/or 374 divergence. Thus, the same genes respond to the environment and are involved 375 in evolution. It might seem predictable that the same genes are involved in the 376 plasticity of a trait and the variation/evolution of this trait. However, this is not 377 so obvious. Indeed, the same phenotypes can sometimes be produced by 378 different mechanisms. For example, Drosophila wing size can be modulated by 379 both temperature and clinal genetic variation. However, this occurs through 380 distinct mechanisms: temperature modulates cell size [START_REF] Azevedo | Temperature modulates epidermal 479 cell size in Drosophila melanogaster[END_REF], 381 whereas clinal genetic variation primarily affects cell number [START_REF] James | Cellular basis and developmental 533 timing in a size cline of Drosophila melanogaster[END_REF]. 382 Similar pigmentation phenotypes can be produced by modulating the expression 383 of different pigmentation genes [START_REF] Wittkopp | Drosophila pigmentation 646 evolution: divergent genotypes underlying convergent phenotypes[END_REF]. For example, melanin 384 production can be increased by up--regulating tan or down--regulating ebony, that 385 encode enzymes with antagonist activities (True et al. 2005). 386 In the case of RCO--A and tan, the variation or divergence in expression is caused 387 by mutations in the cis--regulatory sequences of the genes. This is also likely the 388 case for Ubx during genetic assimilation of the bithorax phenotype. Remarkably, 389 for tan, the same cis--regulatory sequence mediates, at least partly, the effect of 390 temperature. It is generally thought that cis--regulatory mutations are less 391 pleiotropic than mutations in trans--acting factors [START_REF] Prud'homme | Emerging principles of regulatory 575 evolution[END_REF]. 392 Thus, targeting tan, a gene encoding a pigmentation enzyme, or RCO--A, whose 393 expression is limited to the sinuses between growing leaf lobes, limit potential 394 deleterious effects. The recurrent involvement of RC0--A and tan in evolution lead 395

to their characterization as evolutionary hotspots [START_REF] Martin | The Loci of repeated evolution: a catalog of genetic 555 hotspots of phenotypic variation[END_REF]396 Sicard et al. 2014). Why are these two genes targets of recurrent evolution ? For 397 a given allele, temperature sensitivity of RCO--A and tan expression leads to 398 different phenotypes in different environments. Reciprocally, different alleles 399 will induce different phenotypes in the same environment. It follows that only 400 some genotypes will produce an optimal phenotype in a given environment. This 401 may lead to selection of different alleles of these genes in different environments 402 to reach an optimal phenotype. This is in particular the case if the phenotype 403 produced by the plastic response is not well adjusted to the environment. 404 Genetic variation will be selected to reduce or to increase the effect of the 405 environment. As the environment fluctuates spatially and temporally, adjusting 406 selection increases genetic variation with functional consequences at these loci. 407 This higher genetic variation facilitates the involvement of those loci in 408 evolution. 409

In the other cases presented in this review, the respective contributions of cis 410 and trans variations are not known (eud--1 in P. pacificus, genes modulated by 411 osmotic challenge in Fundulus, Dll in Bicyclus anynana) but the recent 412 identification of trans--regulators of eud--1 is a step towards answering this 413 question [START_REF] Serobyan | Chromatin remodelling and 594 antisense--mediated up--regulation of the developmental switch gene eud--595 1 control predatory feeding plasticity[END_REF]. However, what is clear is that evolution has 414 targeted components of the gene networks regulating the transcriptionally 415 plastic genes if not these genes themself. In most cases described in this review, 416 the gene showing transcriptional plasticity also exhibits genetic variation that 417 provides substrate for evolution through selection or simply drift. The fact that 418 the same networks, or even the same genes, are involved in plasticity and 419 evolution contradicts somehow Scheiner's ideas on the decoupling of the genetic 420 processes controlling the plasticity and the mean of a trait [START_REF] Scheiner | Plasticity as a Selectable Trait: Reply to Via[END_REF]. 421

In addition, the "flexible stem hypothesis" implies that it is mechanistically 422 possible for a trait initially plastic to undergo environmental canalization and 423 become independent of the environment. Several studies have dissected the 424 mechanisms behind phenotypic plasticity and environmental canalization. Two 425 major mechanisms have been identified: regulation of chromatin structure and 426 hormonal signalling/response. It is known that environmental conditions can 427 modulate DNA methylation [START_REF] Kucharski | Nutritional control of 541 reproductive status in honeybees via DNA methylation[END_REF], histone post--translational 428 modifications [START_REF] Simola | Epigenetic (re)programming of 605 caste--specific behavior in the ant Camponotus floridanus[END_REF][START_REF] Gibert | Phenotypic Plasticity 519 through Transcriptional Regulation of the Evolutionary Hotspot Gene tan 520 in Drosophila melanogaster[END_REF] or chromatin compaction 429 [START_REF] Leung | Open chromatin profiling in mice livers 552 reveals unique chromatin variations induced by high fat diet[END_REF]. Thus, stabilization of chromatin structure in an initially 430 plastic species, could lead to production of a constant phenotype independent of 431 the environment. For example, artificial down--regulation of DNA methylation in 432 honey--bees lead to the production of a queen phenotype from larvae that should 433 have developed as workers because on the diet they fed on (Kucharski et al. 434 2008). Some alleles might carry variation in their cis--regulatory sequences that 435 promotes the formation of a particular chromatin structure independently of the 436 environment. This might be the case for tan or Ubx and selection on this 437 variation might contribute to modify the sensitivity of their expression to the 438 environment. Regarding, hormonal regulation, it is known that differences of 439 plasticity between genotypes could be linked to differences of hormonal 440 signalling or response [START_REF] Suzuki | Evolution of a polyphenism by genetic 611 accommodation[END_REF]. In Manduca sexta larvae, 441 artificial selection on temperature induced pigmentation variation lead to the 442 production of a polyphenic and a monophenic lines differing by their juvenile 443 hormone titer and response [START_REF] Suzuki | Evolution of a polyphenism by genetic 611 accommodation[END_REF]. Interestingly a similar 444 are needed. In particular, it would be interesting to know whether the example 470 of tan and its t_MSE is just a particular case or whether it is predictive of a more 471 systematic involvement of the same regulatory sequences in phenotypic 472 plasticity and species variation and divergence. 473 474 475 east America, constitutes a range of water habitat with different salinity going 669 from pure sea water (dark blue) to pure fresh water (red), modified after 670 [START_REF] Whitehead | Genomic mechanisms of 632 evolved physiological plasticity in killifish distributed along an 633 environmental salinity gradient[END_REF]. Top right, populations of Atlantic killifish (Fundulus 671 heteroclitus) are locally adapted to particular salinities but are also able to 672 quickly adjust to osmotic challenges. Bottom right: modification of gill 673 epithelium after transfer form sea water to fresh water (after (Whitehead et al. 674 2012)). In sea water (32 ppt), the apical surface of the gill epithelium is made of 675 pavement cells (red asterisk) interspersed with mitochondrion--rich cells 676 possessing apical crypt with small surface area (green arrowhead). Exposure to 677 fresh water (0.1 ppt) leads to an enlargement of the apical surface of 678 mitochondrion--rich cells (green arrowhead). 679 680 HIGH line (bottom) with very limited plasticity (after [START_REF] Brakefield | Development, plasticity and evolution 497 of butterfly eyespot patterns[END_REF]). 686 687 posterior segments (A5, A6 and A7). Anterior is up, ventral is left (after (Gibert 706 et al. 2016)). 707 708

  initially plastic trait? We present here several examples of phenotypic plasticity, 174 chosen in animals or plants, whose genetic bases have been addressed through 175 candidate gene approach or global transcriptome analyses. Most of these 176 analyses are performed in an evolutionary context (either artificial or natural) or 177 can be complemented by other studies on the evolution of the particular traits of 178 interest in closely related species. Furthermore, we describe studies dissecting 179 the mechanisms involved in phenotypic plasticity and environmental 180 canalisation. Modulation of such mechanisms must be involved in the 181 environmental canalization of initially plastic traits involved in the flexible stem 182 hypothesis. 183 184

Figure 1 :Figure 2 :

 12 Figure legends: 660

Figure 3 :

 3 Figure 3: Top: natural populations of the satyrine butterfly Bicyclus anynana 681

Figure 4 :Figure 5 :Figure 6 :

 456 Figure 4: The diplogastrid nematod Pristionchus pacificus displays two 688