Guillaume Burel
email: guillaume.burel@ensiie.fr

Cut Admissibility by Saturation

come

Whatever their origin, proofs rarely need to be searched for without context: Program verification requires arithmetic, theories of lists or arrays, etc. Mathematical theorems are in general not proved in pure predicate logic. Consequently, even if (automated and interactive) proof systems have achieved a high degree of maturity, they need to be able to deal with theories in an efficient way. This explains the particular interest focused on SMT (Satisfiability Modulo Theory) provers in the latter years. However, one of the drawbacks of the SMT approach is that the way theories are integrated is not completely generic, in the sense that each theory needs a special treatment.

A more generic approach to integrating theories into a proof system was proposed by Dowek, Hardin and Kirchner [START_REF] Dowek | Theorem proving modulo[END_REF]. In Deduction Modulo1 , a theory is represented by a congruence over formulae, and proofs are searched for modulo this congruence. In practice, this congruence is most often described as a rewriting system. However, using only term rewriting rules would not be enough to capture interesting theories. For instance, Vorobyov [START_REF] Vorobyov | On the arithmetic inexpressiveness of term rewriting systems[END_REF] showed that even quantifier-free Presburger arithmetic cannot be presented as a convergent term rewriting system. To overcome this, Deduction Modulo also deals with proposition rewriting rules, that rewrite atomic formulae into formulae. Thanks to this, it was possible to present many theories in Deduction Modulo: simple type theory (also known as higher-order logic), arithmetic, B set theory [START_REF] Jacquel | Tableaux modulo theories using superdeduction -an application to the verification of B proof rules with the Zenon automated theorem prover[END_REF], any pure type system, including the calculus of constructions which is the foundation of the proof assistant Coq [START_REF] Cousineau | Embedding pure type systems in the lambda-Pi-calculus modulo[END_REF], or, in fact, any first-order theory [START_REF] Burel | From axioms to rewriting rules[END_REF]. It is then possible to use automated theorem provers based on Deduction Modulo, such as iProver Modulo [START_REF] Burel | Experimenting with deduction modulo[END_REF] or Zenon Modulo [START_REF] Delahaye | Zenon modulo: When Achilles outruns the tortoise using deduction modulo[END_REF]. Moreover, proofs in those theories can be checked using Dedukti, a proof checker based on Deduction Modulo (https://www.rocq.inria.fr/deducteam/Dedukti/). Note that if one wants that the proof systems modulo a rewriting system behave well, in particular, if one wants the proof search methods to be complete, or the proof calculus to enjoy usual proof-theoretical properties such as the subformula property or the witness property, the rewriting system must have the following feature: The cut rule must be admissible in the sequent calculus modulo the rewriting system. This is true for the presentations of theories cited above.

Even if any first-order theory can be presented as a rewriting system with cut admissibility, these presentations may be quite unnatural. This is particularly the case when equality is involved. Indeed, the work [START_REF] Burel | From axioms to rewriting rules[END_REF] does not handle the equality predicate ≃ in a special way, and for instance an axiom s ≃ t would be presented by a proposition rewriting rule s ≃ t → ⊤ and not by a term rewriting rule s → t. There are also cases in which the most natural candidate to present an axiom as a rewriting rule would be a conditional rewriting rule, for instance in the case of an axiom of the shape A(x) ⇒ s(x) ≃ t(x). In particular, this is the case of one of the axioms of the theory used in the provers of the HOL family (HOL4, HOL Light, or even Isabelle/HOL). In the translation of proofs in the OpenTheory format [START_REF] Hurd | The OpenTheory standard theory library[END_REF] into proofs that can be checked by Dedukti [START_REF] Assaf | Translating HOL to Dedukti[END_REF], this axiom could not be easily presented as a rewriting rule, and should therefore remain as an axiom, losing partially the benefit of working modulo the theory. As we will see in Example 8, this axiom can be naturally presented as a conditional rewriting rule. In this paper, we therefore introduce Deduction Modulo Conditional Rewriting Rules, which strictly subsumes the usual presentation of Deduction Modulo.

We therefore need a criterion that ensures that cut admissibility holds in the sequent calculus modulo the conditional rewriting system. To do so, we study links between saturation processes and cut admissibility. In [START_REF] Dowek | Confluence as a cut elimination property[END_REF], Dowek proved that in the case were there are only term rewriting rules, cut admissibility is equivalent to the confluence of the rewriting system. In the case where there are proposition rewriting rules, this is no longer true; for instance the rule A → A ⇒ B is confluent but does not admit cuts. Now, consider a term rewriting system that does not admit cuts. Equivalently, it is not confluent. One way to recover confluence, and thus cut admissibility, is to use the completion technique of Knuth and Bendix [START_REF] Knuth | Simple word problems in universal algebras[END_REF], that has been refined into Unfailing Completion [START_REF] Bachmair | Completion without failure[END_REF]. Unfailing Completion is a saturation process: starting from a set of equations, new equations are generated, and older ones are simplified, until all newly generated equations are redundant. The set of equations is then called saturated, and in the case of Unfailing Completion, the corresponding rewriting system is convergent on ground terms. Consequently, cut admissibility is ensured for ground terms, which is enough for cut admissibility since we can restrict ourselves to ground sequents (if one considers Eigenvariables as constants). In other words, when it succeeds, Unfailing Completion allows to recover cut admissibility. In this paper, we investigate how a saturation technique can help at regaining cut admissibility in the more general case when there are proposition rewriting rules.

To better apprehend how it works, let us remark that there are usually two ways to see rewriting systems: The first one is to consider them as particular cases of abstract reduction systems whose objects are terms. The second one is to consider them as a set of equations oriented by some reduction ordering. It is this second point of view that is considered in Unfailing Completion, and more generally in the automated theorem proving community. Of course, the two views generally coincide, in particular in the case of terminating rewrite systems. Let us now look at what would correspond to a proposition rewriting rule following the second point of view. According to Dowek [START_REF] Dowek | Polarized resolution modulo[END_REF], a rewriting rule P → C would coincide to what he calls a one-way clause ¬P ∨ C, where ¬P is selected, which means it is the only literal that can be used to resolve the clause in the Resolution method. This idea of selected literal is reminiscent of Ordered Resolution with Selection [START_REF] Bachmair | Resolution theorem proving[END_REF], where literals are selected according to a well-founded ordering and a selection function choosing negative literals. Therefore, the analogue of seeing term rewriting rules as equations oriented by an ordering is to see proposition rewriting rules as clauses oriented by an ordering and a selection function. Then, Ordered Resolution with Selection can be used as a saturation process that allows to recover cut admissibility, as we prove in Theorem 7.

We can go a step further. Unfailing Completion and Ordered Resolution with Selection can be combined into Superposition, which is therefore a proof search method for first-order logic with equality. Superposition includes in particular the following inference rule:

s ≃ u ∨ C L[t] p ∨ D Superposition σ = mgu(s, t) σ(L[u] p ∨ C ∨ D)
with ordering restrictions to prevent the proliferation of such inferences. If we look at the inference rule, it behaves as if L[t] p was rewritten (or more precisely narrowed) into L[u] p , provided no condition in C holds. Following our analogy between rewriting rules, equations and clauses, we can therefore see the clause s ≃ u ∨ C as a conditional rewriting rule s → u if ¬C. We then prove that when a set of clauses is saturated using Superposition, its corresponding rewriting system, consisting of both proposition rewriting rules and conditional term rewriting rules, admits cuts (Theorem 7 again, since Ordered Resolution with Selection is a special case of Superposition when equality is not present).

In the following section, we will present Deduction Modulo in more details. Then in Section 2 we say a few words about saturation processes, in particular saturation up to compositeness which is a modular form of redundancy. In Section 3 we introduce Deduction Modulo Conditional Rewriting Rules, in particular by means of a sequent calculus. In Section 4, we prove the main result of this paper, namely that when a set of clauses is saturated up to compositeness, then a corresponding conditional rewriting system admits cuts.

1 Deduction Modulo

Sequent Calculi Modulo

We use standard definitions for terms, predicates, propositions (with connectives ¬, ⇒, ∧, ∨ and quantifiers ∀, ∃), sequents, substitutions, term rewriting rules and term rewriting. The substitution of a variable x by a term t in a term or a proposition A is denoted by {t/x}A, and more generally the application of a substitution σ in a term or a proposition A by σA. A literal is an atomic proposition or the negation of an atomic proposition. The negation of a literal L ⊥ is defined by P ⊥ = ¬P and ¬P ⊥ = P . A proposition is in clausal form if it is the universal quantification of a disjunction of literals ∀x 1 , . . . , x n . L 1 ∨ . . . ∨ L p where x 1 , . . . , x n are the free variables of L 1 , . . . , L p . In the following, we will often omit the quantifiers, and we will identify propositions in clausal form with clauses (i.e. set of literals) as if ∨ were associative, commutative and idempotent. This will be justified in Section 3. The symbol ⊓ ⊔ represents the empty clause. The polarity of a position in a proposition can be defined as follows: the root is positive, and the polarity switches when going under a ¬ or on the left of a ⇒.

In deduction modulo, term rewriting is extended to propositions by congruence on the proposition structure. In addition, there are also proposition rewriting rules whose left-hand side is an atomic proposition and whose righthand side can be any proposition. Such rules can also be applied to non-atomic propositions by congruence on the proposition structure. We call a rewriting system the combination of a term rewriting system and a proposition rewriting system. Deduction modulo consists in applying the inference rules of an existing proof system modulo such a rewriting system.

In this setting, rewriting rules can be applied indifferently to the left-or the right-hand side of a sequent. Consequently, they can be considered semantically as an equivalence between their left-and right-hand sides. To be able to consider implications, a polarized version of deduction modulo was introduced [START_REF] Dowek | What is a theory?[END_REF]. Proposition rewriting rules are tagged with a polarity + or -; they are then called polarized rewriting rules. A proposition A is rewritten positively into a proposition B (A -→ + B) if it is rewritten by a positive rule at a positive position or by a negative rule at a negative position. It is rewritten negatively (A -→ -B) if it is rewritten by a positive rule at a negative position or by a negative rule at a positive position. Intuitively, a positive rule A → + B (resp. a negative rule B → -A) corresponds to an implication B ⇒ A. Term rewriting rules (but not proposition rewriting rules) are considered as both positive and negative. * -→ ± is the reflexive transitive closure of -→ ± . This gives the polarized sequent calculus modulo, some of whose rules are presented in Figure 1. (dw can be seen as the Skolem symbol introduced by the CNF transformation of the definition of the subset relation, dw (A, B) is a witness that A is not included in B if it is the case.) We can build the following proof of the transitivity of the inclusion in the polarized sequent calculus modulo this system:

Example 1. Consider the polarized rewriting system

A ⊆ B → -∀x. x ∈ A ⇒ x ∈ B A ⊆ B → + ¬dw (A, B) ∈ A A ⊆ B → + dw (A, B) ∈ B ⌢ - A * -→ R -C + * ←- R B Γ, A -B, ∆ Γ, A -∆ Γ -B, ∆ - ⌣ A - * ←- R C * -→ R + B Γ -∆ Γ, B -∆ Γ -A, ∆ ⇒ - C * -→ R -A ⇒ B Γ, C -∆ Γ, A -∆ -¬ B * -→ R + ¬A Γ -B, ∆ Γ, {t/x}A -∆ ∀ - B * -→ R -∀x. A Γ, B -∆ Γ -A, B, ∆ -∵ C * -→ R + A C * -→ R + B Γ -C, ∆
⌢ -dw (A, C) ∈ C -A ⊆ C ⌢ -dw (A, C) ∈ B -dw (A, C) ∈ B ⇒ - dw (A, C) ∈ B ⇒ dw (A, C) ∈ C, dw (A, C) ∈ B -A ⊆ C ∀ -B ⊆ C, dw (A, C) ∈ B -A ⊆ C ⌢ -dw (A,C)∈A -dw (A,C)∈A ⇒ - dw (A, C) ∈ A ⇒ dw (A, C) ∈ B, B ⊆ C, dw (A, C) ∈ A -A ⊆ C ∀ - A ⊆ B, B ⊆ C, dw (A, C) ∈ A -A ⊆ C -¬ A ⊆ B, B ⊆ C -A ⊆ C, A ⊆ C -∵ A ⊆ B, B ⊆ C -A ⊆ C
We denote by Γ ⊢ R ∆ the fact that the sequent Γ -∆ is provable in the Polarized Sequent Calculus Modulo R. A theory Γ and a rewriting system R are called compatible if for all formulae A, then Γ ⊢ A (without rewriting) if and only if ⊢ R A.

The cut rule is admissible in the sequent calculus modulo R if, whenever a sequent can be proved in it, then it can be proved without using the cut rule ( - ⌣ in Figure 1). Abusing terminology, we say that a rewriting system R admits cut if the cut rule is admissible in the sequent calculus modulo R. The admissibility of the cut rule has a strong proof-theoretical as well as practical importance: it entails that normal forms exist for proofs; it implies the consistency of the theory associated to R; it is equivalent to the completeness of the proof search procedures based on deduction modulo R; etc.

Resolution Modulo and One-Way Clauses

An extension of resolution based on deduction modulo, called ENAR for Extended Narrowing and Resolution, was proposed by Dowek, Hardin and Kirchner [START_REF] Dowek | Theorem proving modulo[END_REF]. It consists of adding a new inference rule to the method of Robinson [20]. This rule, called Extended Narrowing, narrows a clause using the rewrite system modulo which the proof is searched for. However, in ENAR, there is a need to In Polarized Resolution Modulo, proposition rewrite rules are assumed to be clausal, which means that positive rewrite rules are of the form P → + ¬C, and negative rules are of the form P → -C, where C is in clausal form. This ensures that formulae generated by Extended Narrowing are still in clausal form.

P ∨ C ¬Q ∨ D Resolution σ = mgu(P, Q) σ(C ∨ D) L ∨ K ∨ C Factoring σ = mgu(L, K) σ(L ∨ C) P ∨ C Ext. Narr. - σ = mgu(P, Q) Q → -D ∈ R σ(D ∨ C) ¬Q ∨ D Ext. Narr. + σ = mgu(P, Q) P → + ¬C ∈ R σ(C ∨ D)
Applying Extended Narrowing to a clause P ∨ C using the rule Q → -D produces the same clause (namely σ(D ∨ C), where σ = mgu(P, Q)) as applying Resolution to this clause P ∨ C and the clause ¬Q ∨ D. Similarly, narrowing with P → + ¬C amounts to resolving with P ∨ C. Therefore, the polarized rewrite rule Q → -D (resp. P → + ¬C) can be identified with what Dowek [START_REF] Dowek | Polarized resolution modulo[END_REF] called the one-way clause ¬Q ∨ D (resp. P ∨ C) where two one-way clauses cannot be resolved together; -only the selected (underlined) literal of a one way-clause can be used in resolution.

Conversely, given a clause C and a literal L in C, it is always possible to associate a polarized rewrite rule polar (C, L): polar (P ∨ C, P ) is P → + ¬C and polar (¬Q∨D, ¬Q) is Q → -D. Therefore, the same way that it is possible to see a term rewriting rule as an equation in which one side is selected, it is possible to see clausal polarized rewriting rules as clauses in which a literal is selected.

Saturation

If there are only term rewriting rules in R, and no proposition rewriting rules, Dowek [START_REF] Dowek | Confluence as a cut elimination property[END_REF] showed that cut admissibility in the asymmetric sequent calculus modulo R is equivalent to confluence of R. If R is not confluent, a way to get an equivalent rewriting system which is confluent is to apply the Knuth-Bendix standard completion [START_REF] Knuth | Simple word problems in universal algebras[END_REF], which was extended into Unfailing Completion [START_REF] Bachmair | Completion without failure[END_REF]. Unfailing completion can be seen as a saturation process: one applies all possible inferences to a starting set of formulae (in that case, positive unit equations) until all newly inferred formulae are redundant, that is, can be simplified. In that case, the resulting set is called saturated, and the correctness of the procedure shows that a saturated set has the required property, namely ground convergence in the case of Unfailing Completion. Of course, since the required property is in general not decidable, the saturation process may not terminate. Resolution and its refinements can also be seen as saturation processes: the set of clauses is completed until either the empty clause is generated, in which case the initial set was inconsistent, or until all newly generated clauses are redundant, in which case it is possible to construct a model of the saturated set of clauses.

It would be preferable that the saturation process were modular, in the sense that, if a set Γ of formulae is saturated, then saturating Γ ∪ ∆ should not need to apply inferences between formulae of Γ only. (This is in particular crucial for implementing resolution using the given clause algorithm, to ensure that clauses that were redundant remains redundant when a new given clause is chosen.) Therefore, redundancy should be modular, in the sense that if C is redundant in Γ , then it should be redundant in Γ ∪ ∆. This refinement of redundancy is called compositeness by Bachmair and Ganziger [START_REF] Bachmair | Rewrite-based equational theorem proving with selection and simplification[END_REF]. In fact, resolution-based provers saturate their input in general not up to redundancy but up to compositeness (Bachmair and Ganziger call saturation up to compositeness completeness, but we will keep writing "saturation up to compositeness" to keep things clear.) Of course, saturation up to compositeness implies saturation up to redundancy.

To deal with full first-order logic with equality, and not only unit clauses, Unfailing Completion can be extended into Superposition [START_REF] Bachmair | Rewrite-based equational theorem proving with selection and simplification[END_REF], which is consequently a complete proof-search method for first-order logic with equality. In pure Superposition, the only predicate is the equality predicate (noted ≃), and clauses are therefore sets of equations and inequations. It is possible to encode other predicates using function symbols, as is done for instance in the prover E. However, to separate more clearly reasoning about equality and about propositions, we will use the inference for Superposition in addition to the rules for Ordered Resolution with Selection [START_REF] Bachmair | Resolution theorem proving[END_REF] (a refinement of resolution inspired by Superposition), as is done in the prover SPASS. As in Unfailing Completion, we consider a reduction ordering ≻, that is, an ordering that is stable under substitution and context. Literals are compared as the multisets of multisets {{s}, {t}} for the positive literal s ≃ t and {{s, ♭}, {t, ♭}} for the negative literal s ≃ t, where ♭ is a special symbol not part as the signature, which is assumed to be smaller than any term. A clause s ≃ t ∨ C is reductive for s ≃ t if t s and s ≃ t is strictly maximal in s ≃ t∨C. We also consider a selection function S that, given a clause C, returns a subset of the negative literals of C. Without considering simplifications, Superposition consists of the four inference rules presented in Figure 3, in addition to which we also consider the two rules of Ordered Resolution with Selection presented in Figure 4.

As we can see, Superposition has strong restrictions on the application of inference rules, which explain in part its efficiency. In particular, ordering restrictions are performed after the application of the unifier σ. Let us note notwithstanding that, thanks to the stability of ≻ by substitution, the calculus remains of course complete if the restriction is applied on the premises, although it makes the proof search space bigger.

In Superposition, compositeness can be defined as follows: A ground clause C is called composite with respect to Γ if there exists ground instances C of clauses of Γ such that C 1 , . . . , C n entails C and C ≻ C j for all 1 ≤ j ≤ n. A non-ground clause is called composite with respect to Γ if all its ground instances are. Lemma 11 of [START_REF] Bachmair | Rewrite-based equational theorem proving with selection and simplification[END_REF] tells us that if C is composite in Γ , then it is composite in Γ ∪∆, and that all composite clauses can be safely removed from Γ , as expected.

1 , . . . , C n s ≃ t ∨ C Equality Resolution σ(C) s ≃ u ∨ C ¬P [t]p ∨ D Negative Superposition σ(¬P [u]p ∨ C ∨ D) s ≃ u ∨ C P [t]p ∨ D Positive Superposition σ(P [u]p ∨ C ∨ D) s ≃ u ∨ t ≃ v ∨ C Eq. Factoring σ(u ≃ v ∨ t ≃ v ∨ C)
≃ u ∨ t ≃ v ∨ C) = ∅ and σ(s ≃ u) is maximal in σ(s ≃ u ∨ t ≃ v ∨ C); 7. in both Superpositions, if P [t]p is an equation v[t] p ′ ≃ w, then σw σv[t] p ′ .

Deduction Modulo Conditional Rewriting Rules

We now present an extension of deduction modulo to the case of conditional rewriting rules.

Definition 2 (Conditional rewriting rule).

A conditional rewriting rule is given by a pair of terms t and s and a set of formalae Γ . It is denoted by s → t if Γ .

A term u rewrites to a term v and conditions ∆ using the conditional rewriting rule s → t if Γ if there is a position p and a substitution θ such that u |p = θs, v = u[θt] p and ∆ = θΓ . This rewrite relation is denoted by u -→ v ≀ ∆. This is extended to propositions by congruence on the proposition structure.

Note that our definition of conditional rewriting differs from the usual definition as can be found in [START_REF] Dershowitz | Confluence of conditional rewrite systems[END_REF], because conditions are not checked before applying the rewriting rule, but they are delayed and, as we will see, they are checked using a proof system and not just using normalization. This allows to have arbitrary first-order formulae as conditions.

We can combine conditional (term) rewriting rules C with polarized (proposition) rewriting rules P to get what we call a polarized and conditional rewriting system : A proposition A rewrites positively to B and ∆ in CP

(A * -→ CP + B ≀ ∆) if -either A = B and ∆ = ∅ -or A * -→ CP + A ′ ≀ ∆ 1 and • either A ′ -→ P + B and ∆ = ∆ 1 • or A ′ -→ C B ≀ ∆ 2 and ∆ = θ∆ 1 ∪ ∆ 2
where θ is a renaming of the free variables of ∆ 1 to avoid clashes with those of ∆ 2 .

Negative rewriting can be defined similarly. Let us remark that a conditional rewriting step is therefore both a positive or a negative step. Definition 3. A formula does not involve equality if ≃ is not present in it. A conditional rewriting rule s → t if C does not involve equality if all formulae in C do not involve equality. Given a rewriting system that does not involve equality, we can define the Sequent Calculus Modulo Polarized and Conditional Rules. We only give the main rules in Figure 5, the others can be induced from them:

Γ -θA1, ∆ . . . Γ -θAn, ∆ ⌢ - A * -→ CP -C ≀ {A1; . . . ; Ai} and B * -→ CP + C ≀ {Ai+1; . . . ; An} Γ, A -B, ∆ Γ, A -∆ Γ -B, ∆ Γ -θA1, ∆ . . . Γ -θAn, ∆ - ⌣ C * -→ CP -A ≀ {A1; . . . ; Ai} C * -→ CP + B{Ai+1; . . . ; An} Γ -∆ Γ, B -∆ Γ -A, ∆ Γ -θA1, ∆ . . . Γ -θAn, ∆ ⇒ - C * -→ CP -A ⇒ B ≀ {A1; . . . ; An} Γ, C -∆ Γ -θA1, ∆ . . . Γ -θAn, ∆ -⊤ A * -→ CP + ⊤ ≀ {A1; . . . ; An} Γ -A, ∆ Γ, {t/x}A -∆ Γ -θA1, ∆ . . . Γ -θAn, ∆ ∀ - B * -→ CP -∀x. A ≀ {A1; . . . ; An} Γ, B -∆
where θ is a substitution of the free variables of all Ai. Example 4. Consider the following polarized and conditional rewriting system, inspired by Collatz conjecture:

syracuse(X) → syracuse(half (X)) if {even(X)} half (s(o)) → o if ∅ syracuse(X) → syracuse(tnpo(X)) if {odd(X)} half (o) → o if ∅ half (s(s(X)) → s(half (X)) if ∅ even(s(X)) → + odd(x) tnpo(s(X)) → s(s(s(tnpo(X)))) if ∅ odd(s(X)) → + even(x) tnpo(o) → s(o) if ∅ even(o) → + ⊤
and let us denote by n the term s(. . . s(

n times o)).
Then, syracuse(5) * -→ 1 ≀ {odd(5); even [START_REF] Hermant | Resolution is cut-free[END_REF]; even [START_REF] Degtyarev | Equality reasoning in sequent-based calculi[END_REF]; even(4); even(2)}, and we have the following proof of odd(syracuse( 5)):

-⊤odd( 5)

-⊤even( 16)

-⊤ -even(8) -⊤ -even(4) -⊤ -even (2)
-⊤

odd(syracuse( 5))

Note that Deduction Modulo Polarized and Conditional Rules strictly subsumes Polarized Deduction Modulo, which is exactly the case when there are no conditions in the term rewriting rules.

Lemma 5. The inference rules ∀ -, ∨ -, ¬ -and -¬ are invertible in the Sequent Calculus Modulo Polarized and Conditional Rules, which means that their conclusion is provable if and only if their premises are. Moreover, if the proof of the conclusion does not use - ⌣ , neither do the proofs of the premises. Proof. By induction on the proof of the conclusion.

⊓ ⊔

This lemma implies that we can handle formulae in clausal normal form as clauses, that is, set of literals. See for instance [START_REF] Hermant | Resolution is cut-free[END_REF].

Ensuring Cut Admissibility using Saturation

Given an ordering ≻ and a selection function S, we define the polarized and conditional rewriting system associated to a set of clauses, and state that the saturation of the set of clauses implies the cut admissibility for the corresponding rewriting system. Definition 6. Given a set of clauses Γ , an ordering on terms ≻ and a selection function S, then the rewrite system CS(Γ, ≻, S) contains all rewrites rules polar(C, L) for all clauses C such that S(C) = ∅ and for all L in S(C) that does not involve equality; -polar(C, L) for all clauses C such that S(C) = ∅ and for all L maximal in C w.r.t. ≻ that does not involve equality;

-s → t if {L ⊥ 1 , . . . , L ⊥ n } for all clauses C = s ≃ t ∨ L 1 ∨ • • • ∨ L n such that S(C) = ∅, s ≃ t is maximal in C and t ≻ s.
Theorem 7. If the set Γ of clauses is saturated by Superposition up to compositeness, and CS(Γ, ≻, S) does not involve equality, then the sequent calculus modulo CS(Γ, ≻, S) is compatible with Γ and it admits cuts.

Note that the Sequent Calculus Modulo Polarized and Conditional Rules is only defined to prove formulae that do not involve equality.

Before we prove Theorem 7, let us look at an example.

Example 8. In provers of the HOL family, it is possible to define a new type corresponding to the (non-empty) set of terms that satisfies a predicate p. To do so, two function symbols abs and rep are introduced that go respectively from the initial type to the new one and conversely, as is represented in the following figure:

p(X) ∨ ¬abs(rep(X)) ≃ X (1) ¬p(X) ∨ abs(rep(X)) ≃ X (2) rep(abs(Y )) ≃ Y (3)
Without a selection function, and with the lexicographic path ordering with precedence abs ≻ p and rep ≻ p, the resulting conditional rewriting system is

abs(rep(X)) → X if {p(X)} rep(abs(Y )) → Y if ∅
The sequent calculus modulo this system is not compatible with the initial theory. Indeed, it is not possible to prove ∀Y. p(abs(Y )), although this is a consequence of the axioms. This comes from the fact that the set of clauses is not saturated for Superposition. To saturate the set of clause, for instance using E, we only need to add a new clause, namely p(abs(Y )), obtained by applying Negative Superposition on (3) and (1), and then Equality Resolution on p(abs(X)) ∨ ¬abs(X) ≃ abs(X), which is then composite. Note that all other generated clauses are tautologies, and therefore are composite.

Consequently, the polarized and conditional rewriting system

abs(rep(X)) → X if {p(X)} rep(abs(Y )) → Y if ∅ p(abs(X)) → + ¬⊥
admits cut for formulae that do not involve equality.

Let us mention Holide [START_REF] Assaf | Translating HOL to Dedukti[END_REF], a translator of proofs in the OpenTheory [START_REF] Hurd | The OpenTheory standard theory library[END_REF] format into Dedukti, a proof checker based on deduction modulo. Most of the theory of HOL can be expressed as rewriting rules, except a few axioms that cannot be easily oriented. The first axiom defining rep and abs is one of these axioms, and as we have seen, it could be oriented as a conditional rewriting rule.

To prove Theorem 7, we need to prove that if A is proved in the sequent calculus modulo CS(Γ, ≻, S), then it can be proved in Γ , and that if A can be proved in Γ , then it can be proved in the sequent calculus modulo CS(Γ, ≻, S) without - ⌣ . The proof is partially based on the work of Dowek [START_REF] Dowek | Polarized resolution modulo[END_REF] who proves that a derivation in PRM can be translated into a cut-free proof in the polarized sequent calculus modulo.

Lemma 9. If A * -→ -B ≀ {L 1 , . . . , L n }, then Γ, A ⊢ B, L ⊥ 1 , . . . , L ⊥ n . If A * -→ + B ≀ {L 1 , . . . , L n }, then Γ, B ⊢ A, L ⊥ 1 , . . . , L ⊥ n .
Proof. By induction on the length of the derivation; several steps can be combined using - ⌣ . Note the importance of renaming free variables between several steps. A single step can be proved by induction on the rewritten formula. If the rewriting occurs in a subformula, we can use the induction hypothesis to conclude. Let us therefore assume that A is atomic. We have two cases depending on whether a polarized or a conditional rule is used. Proof. By induction on the proof, using Lemma 9 to convert rewriting steps. ⊓ ⊔ Lemma 11. If the set Γ of clauses is saturated by Superposition up to compositeness, and CS(Γ, ≻, S) does not involve equality, if A does not involve equality and A is valid in Γ , then it can be proved in the sequent calculus modulo CS(Γ, ≻, S) without - ⌣ . Proof. Since Superposition is complete, there is a derivation of the empty clause from Γ and Cℓ(¬A) (the clausal normal form of ¬A). We are going to translate this derivation into a cut-free proof of Cℓ(¬A) -, by induction of the length of the derivation.

-A -→ B ≀ {L 1 , . . . , L n }. There is a rule s → t if {L ′ 1 , . . . , L ′ n } in CS(Γ, ≻, S) and a substitution σ such that A |p = σs, B = A[σt] p and L k = σL ′ k . This rule corresponds to a clause s ≃ t ∨ L ′ 1 ⊥ ∨ • • • ∨ L ′ n ⊥ in Γ . From Γ, A one can therefore deduce B ∨ L 1 ⊥ ∨ L n ⊥ ,
Let us show that all new clauses in the derivation of ⊓ ⊔ do not involve equality: Since Γ is saturated up to compositeness, all inferences using only premises in Γ are redundant and therefore can be discarded. So by induction hypothesis at least one of the premises does not involve equality. The only way to obtain an equality would be to apply Resolution or Superposition on a literal L of a clause L ∨ C of Γ . In the former case, the restriction on the application of Resolution implies that polar (C, L) is in CS(Γ, ≻, S). Because it does not involve equality, this means that C, and thus the new clause, neither do. In the latter case, the clause involving equality is necessarily the left one in the Superposition inference rule, so that L = s ≃ t for some s and t, and C = L 1 ∨ • • • ∨ L n . The restriction on the application of Superposition implies that s → t if {L ⊥ 1 , . . . , L ⊥ n } is in CS(Γ, ≻, S), so that L 1 , . . . , L n do not involve equality, and thus the new clause neither.

Therefore, since Γ is saturated up to compositeness, we can assume that the derivation of ⊓ ⊔ does not contain applications of Equality Resolution or Equality Factoring. Let us look at the remaining cases. To ease the proof, we can decompose the application of the inference rules into the application of an instantiation and the application of the rule without unification, as in the PEIR calculus of [START_REF] Dowek | Polarized resolution modulo[END_REF]. We have the following cases:

-Instantiation of a clause C outside Γ into σC. By induction hypothesis we have a cut-free proof of ∆, C, σC -. We can build a cut-free proof of ∆, Cby applying a contraction of C and then ∀ -to instantiate the variables as in σ. (Remind that we omit to write quantifiers in clauses, so that C stands in fact for ∀x 1 , . . ⊥ for all 1 ≤ i ≤ n, which can be obtained by application of -¬ or inversion of ¬ -in the proofs above. Note that to make the proof more clear, we did not take the universal quantifiers into account: this is not a problem since ∀ -is invertible, and we took care of renaming the free variables of the conditions during rewriting.

p ∨ D, L[σt] p ∨ D ∨ L 1 ∨ • • • ∨ L n -. Since ∨ -is cut-free invertible,
The last point to show is that from a cut-free proof of Cℓ(¬A)one can build a cut-free proof of -A. This can be proved by slightly adapting the proof of Proposition 3 of [START_REF] Hermant | Resolution is cut-free[END_REF].

⊓ ⊔

Conclusion and Further Works

We have introduced an extension of Deduction Modulo that handles conditional rewriting rules. To get a criterion for cut admissibility in that setting, we have examined how rewriting rules can be seen as oriented equations and oriented clauses. This reflection has lead us to study how saturation techniques can help presenting a theory through a rewriting system with cut admissibility. Our main result is that whenever a set of clauses is saturated, we can build a corresponding rewriting system admitting cuts. We can therefore use state-of-the-art automated theorem provers, which are based on saturation techniques, to orient a theory so that it can be used in Deduction Modulo. These notable results could be extended in several directions. First, the conditions in the conditional rewriting rules obtained from a saturated set of clauses are simple, since they are only a set of literals. This comes from the fact that we start from clauses, and not arbitrary formulae. To get more interesting conditions, an idea would be to consider the work of Ganzinger and Stuber [START_REF] Ganzinger | Superposition with equivalence reasoning and delayed clause normal form transformation[END_REF] that extend Superposition with formulae that need not be in clausal normal form.

Second, our work is restricted to the case where equality appears only in the rewriting rules, not in the conditions nor in the formulae to be proved. If we allowed equations in them, Negative Superposition could be applied to clauses of the theory in which a negative equation is selected. Therefore, these clauses could not be discarded as it is the case in Definition 6. Another issue would be the design of a sequent calculus modulo for first-order logic with equality. It could be handled by extending one of the calculi of [START_REF] Degtyarev | Equality reasoning in sequent-based calculi[END_REF].

Third, saturation implies cut admissibility, but the converse is not true in general. It would be interesting to be able to characterize cut admissibility as precisely as can be done when only terms are rewritten, where it is equivalent to the well studied notion of confluence.

Finally, it would be interesting to see how our work on conditional rewriting rules can be extended to the λΠ-calculus modulo, the system at the heart of the proof checker Dedukti. By doing so, we would be able to orient the theory used in the provers of the HOL family without using axioms, thus improving the performance of the translator Holide [START_REF] Assaf | Translating HOL to Dedukti[END_REF].

Fig. 1 .

 1 Fig. 1. Some inference rules of the Polarized Sequent Calculus Modulo R

Fig. 2 .

 2 Fig. 2. Polarized Resolution Modulo

Fig. 3 .

 3 Fig. 3. Inference Rules of Superposition P ∨ C ¬Q ∨ D Resolution σ(C ∨ D)

Fig. 4 .

 4 Fig. 4. Inference Rules of Ordered Resolution with Selection

Fig. 5 .

 5 Fig. 5. Some Inference Rules of the Sequent Calculus Modulo Polarized and Conditional Rules

  satisfy the axioms ∀X. p(X) ⇔ abs(rep(X)) ≃ X and ∀Y. rep(abs(Y )) ≃ Y , which correspond to the clauses

Corollary 10 .

 10 and thus Γ, A ⊢ B, L ⊥ 1 , . . . , L ⊥ n . -A -→ -B. There exists a rule P → -C in CS(Γ, ≻, S) and a substitution σ such that A |p = σP and B = σC. Therefore, there is a clause ¬P ∨ C in Γ , and from Γ, A one can therefore deduce σC, thus Γ, A ⊢ B. ⊓ ⊔ If Π ⊢ CS(Γ,≻,S) ∆ then Γ, Π ⊢ ∆.

  . , x n , C where x 1 , . . . , x n are the free variable of C.) -Resolution between two clauses P ∨ C and ¬P ∨ D outside Γ . Let us suppose that we have a cut-free proof of ∆, P ∨ C, ¬P ∨ D, C ∨ D -, then Proposition 7 of [13] implies that we have a proof of ∆, P ∨ C, ¬P ∨ D -. -Resolution between a clause P ∨ C outside Γ and a clause obtained by instantiating a clause ¬Q ∨ D of Γ with substitution σ. Then Q → -D is in CS(Γ, ≻, S), and P * -→ -σD ≀ ∅. By induction hypothesis, we have a cut-free proof of ∆, P ∨ C, C ∨ σD -. We can obtain a cut-free proof of ∆, P ∨ Cby applying a contraction of P ∨ C and rewriting P into σD. -Resolution between a clause ¬P ∨ C outside Γ and a clause obtained by instantiating a clause Q ∨ D of Γ : similar to the previous case, except that we need to eliminate a double negation. -Superposition between an clause obtained by instantiating a clause s ≃ t ∨ L 1 ∨ •

  we therefore have (cut-free) proofs of ∆, L[σs] p ∨D, L[σt] p ∨Dand ∆, L[σs] p ∨ D, L ifor all 1 ≤ i ≤ n. Starting from ∆, L[σs] p ∨ D -, we can apply contraction and rewrite L[σs] p , so that it remains to prove ∆, L[σs] p ∨D, L[σt] p ∨ D -, which we have, and ∆, L[σs] p ∨ D -σL i

  Equality Resolution, either s ≃ t ∈ S(s ≃ u ∨ C), or (S(s ≃ u ∨ C) = ∅ and σ(s ≃ t) is maximal in σ(s ≃ u ∨ C); 3. in both Superpositions, σ(s ≃ u∨C) is reductive for σ(s ≃ u)and t is not a variable; 4. in Negative Superposition, either ¬P [t]p ∈ S(¬P [t]p, D) or S(¬P [t]p ∨ D) = ∅ and σ(¬P [t]p) is maximal in σ(¬P [t]p ∨ D); 5. in Positive Superposition, S(P [t]p ∨D) = ∅ and σ(P [t]p ∨D) is reductive for σ(P [t]p); 6. in Equality Factoring, S(s

	where
	1. in all rules above, σ = mgu(s, t);
	2. in

Although it may sound rather strange, the absence of subsequent to the term "modulo" follows the original works about this field.


João Serôdio
email: jserodio@ua.pt

João Ezequiel

Alexandre Barnett

Jean-Luc Mouget

Vona Méléder

Martin Laviale

Johann Lavaud

Efficiency of photoprotection in microphytobenthos: the role of vertical migration and the xanthophyll cycle against photoinhibition

Keywords: microphytobenthos, photoinhibition, photoprotection, xanthophyll cycle, vertical migration, non-photochemical quenching, chlorophyll fluorescence, diatoms

The capacity of estuarine microphytobenthos to withstand the variable and extreme conditions of the intertidal environment, prone to cause photoinhibition of the photosynthetic apparatus, has been attributed to particularly efficient photoprotection mechanisms. However, little is known regarding its actual photoprotection capacity or the mechanisms responsible for the protecting against photoinhibition. This study addressed these questions by (i) quantifying the photoprotection capacity and the extent of photoinhibition under high light exposure, (ii) estimating the contribution of vertical migration and the xanthophyll cycle to overall photoprotection and (iii) evaluating the effects of photoacclimation state. A new experimental protocol was developed, combining (i) chlorophyll fluorescence imaging, for the simultaneous measurement of replicates and experimental treatments, (ii) specific inhibitors for vertical migration and for the xanthophyll cycle, to quantify the relative contribution of each process, and (iii) recovery kinetics analysis of photosynthetic activity during light stress-recovery experiments, to distinguish reversible downregulation from photoinhibition. The results showed a high photoprotective capacity in both studied periods, May and October, with photoinhibition rates remaining below 20%. A clear change in photoacclimation state was obeserved, following the seasonal change in solar radiation, with acclimation to lower irradiances in autumn being associated with higher susceptibility to photoinhibition. Also the relative importance of vertical migration and the xanthophyll cycle varied between the sampling periods. While the two processes displayed a similar role in spring/summer, vertical migration became the dominant photoprotective process in autumn. However, the contribution of the two processes to overall photoprotection reached only ca. 20%, suggesting the participation of other photoprotective mechanisms.

INTRODUCTION

Benthic microalgae inhibiting estuarine intertidal flats are exposed to extreme and highly variable environmental conditions. Particularly during low tide, the sedimentary environment is characterized by the exposure to high levels of solar irradiance [START_REF] Serôdio | Fortnightly light and temperature variability on estuarine intertidal sediments and implications for microphytobenthos primary productivity[END_REF], including UV radiation [START_REF] Waring | Responses of estuarine intertidal microphytobenthic algal assemblages to enhanced ultraviolet B radiation[END_REF], Mouget et al. 2008), extreme temperatures and salinities (Brotas et al. 2003[START_REF] Rijstenbil | UV-and salinity-induced oxidative effects in the marine diatom Cylindrotheca closterium during simulated emersion[END_REF], intense rates of desiccation [START_REF] Coelho | Effects of desiccation on the photosynthetic activity of intertidal microphytobenthos biofilms as studied by optical methods[END_REF], supersaturated oxygen concentrations [START_REF] Chevalier | In situ photosynthetic activity and xanthophylls cycle development of undisturbed microphytobenthos in an intertidal mudflat[END_REF], and nutrient and carbon depletion [START_REF] Miles | Diel variation in microphytobenthic productivity in areas of different tidal amplitude[END_REF][START_REF] Cook | Advective relief of CO 2 limitation in microphytobenthos in highly productive sandy sediments[END_REF].

Being potentially damaging to the photosynthetic apparatus when acting individually, the combined effects of all these factors likely concur to the photoinhibition of photosynthesis of microphytobenthos microalgae. Of particular importance is the exposure to direct sunlight, which can result in excessive reductant pressure and in the formation of intracellular reactive oxygen species (ROS; [START_REF] Roncarati | Photosynthetic performance, oxidative damage and antioxidants in Cylindrotheca closterium in response to high irradiance, UVB radiation and salinity[END_REF][START_REF] Waring | Light-induced responses of oxygen photoreduction, reactive oxygen species production and scavenging in two diatom species[END_REF]. High levels of ROS cause the permanent inactivation of photosystem II (PSII) protein D1, negatively impacting on photosynthetic yield and on primary productivity (Nishiyama et al. 2006). Despite these harsh conditions, microphytobenthos of intertidal flats typically exhibit high growth rates, forming dense and diverse sedimentary biofilms, and are recognized as a major contributor to ecosystem-level carbon fixation and primary productivity [START_REF] Underwood | Primary production by phytoplankton and microphytobenthos in estuaries[END_REF]. Furthermore, the apparent lack of photoinhibition in microphytobenthic biofilms has been repeatedly reported [START_REF] Kromkamp | Determination of microphytobenthos PSII quantum efficiency and photosynthetic activity by means of variable chlorophyll fluorescence[END_REF][START_REF] Underwood | Adaptations of tropical marine microphytobenthic assemblages along a gradient of light and nutrient availability in Suva Lagoon, Fiji[END_REF], Blanchard & Cariou-LeGall 1994[START_REF] Herlory | Microstructure of microphytobenthic biofilm and its spatio-temporal dynamics in an intertidal mudflat (Aiguillon Bay, France)[END_REF][START_REF] Underwood | Patterns in microphytobenthic primary productivity: Species-specific variation in migratory rhythms and photosynthetic efficiency in mixed-species biofilms[END_REF][START_REF] Van Leeuwe | Photoacclimation in microphytobenthos and the role of xanthophyll pigments[END_REF]. This success in coping with high light stress may be explained by the combined operation of two processes, the xanthophyll cycle and vertical migration, which could result in an overall particularly efficient photoprotection [START_REF] Serôdio | Photosynthetic activity, photoprotection and photoinhibition in intertidal microphytobenthos as studied in situ using variable chlorophyll fluorescence[END_REF][START_REF] Perkins | Vertical cell movement is the primary response of intertidal benthic biofilms to increasing light dose[END_REF]. In diatoms, the group of microalgae that typically dominate in microphytobenthos assemblages, the xanthophyll cycle has been reported to provide an exceptionally high photoprotective capacity [START_REF] Lavaud | Fast Regulation of Photosynthesis in Diatoms: Mechanisms, Evolution and Ecophysiology[END_REF], Brunet & Lavaud 2010[START_REF] Goss | Regulation and function of xanthophyll cycle-dependent photoprotection in algae[END_REF]. This is particularly true for microphytobenthos in situ [START_REF] Serôdio | Non-photochemical quenching of chlorophyll fluorescence and operation of the xanthophyll cycle in estuarine microphytobenthos[END_REF], Van Leuwee et al. 2008[START_REF] Jordan | Diurnal changes of photoadaptive pigments in microphytobenthos[END_REF][START_REF] Chevalier | In situ photosynthetic activity and xanthophylls cycle development of undisturbed microphytobenthos in an intertidal mudflat[END_REF]. To this also seems to contribute the activation of the xanthophyll cycle in the dark, attributed to cholorespiratory activity, which has been considered as potentially advantageous during prolonged periods of darkness [START_REF] Jakob | Unusual pH-dependence of diadinoxanthin deepoxidase activation causes chlororespiratory induced accumulation of diatoxanthin in the diatom Phaeodactylum tricornutum[END_REF][START_REF] Cruz | Impact of chlororespiration on non-photochemical quenching of chlorophyll fluorescence and on the regulation of the diadinoxanthin cycle in the diatom Thalassiosira pseudonana[END_REF], a situation common in the sedimentary environment.

On the other hand, the negative phototactic behavior of benthic diatoms, mostly raphid pennates, under high light has long been interpreted as a form of avoidance of excessive light levels that would otherwise cause photoinhibition (Admiraal 1984[START_REF] Underwood | Primary production by phytoplankton and microphytobenthos in estuaries[END_REF][START_REF] Consalvey | The ups and downs of life in a benthic biofilm: migration of benthic diatoms[END_REF][START_REF] Waring | Responses of estuarine intertidal microphytobenthic algal assemblages to enhanced ultraviolet B radiation[END_REF].

This subject has attracted substantial attention in recent years, particularly centered on the effects of vertical migration on biofilm photophysiology [START_REF] Consalvey | The ups and downs of life in a benthic biofilm: migration of benthic diatoms[END_REF][START_REF] Jesus | Effects of vertical migrations by benthic microalgae on fluorescence measurements of photophysiology[END_REF][START_REF] Waring | Responses of estuarine intertidal microphytobenthic algal assemblages to enhanced ultraviolet B radiation[END_REF], Mouget et al. 2008[START_REF] Perkins | Vertical cell movement is the primary response of intertidal benthic biofilms to increasing light dose[END_REF], Cartaxana et al. 2011), and became facilitated by the introduction of a diatom motility inhibitor (Cartaxana et al. 2008). However, these studies have been focused on the response of photosynthetic activity during [START_REF] Waring | Responses of estuarine intertidal microphytobenthic algal assemblages to enhanced ultraviolet B radiation[END_REF][START_REF] Perkins | Vertical cell movement is the primary response of intertidal benthic biofilms to increasing light dose[END_REF] or shortly after light stress (Mouget et al. 2008), mostly through in vivo measurements of electron transport rate of PSII (ETR) or non-photochemical quenching (NPQ) of chlorophyll fluorescence (PAM fluorometry, see below; Table 1) (Perkins et al. 2011).

Perhaps surprisingly, none of these studies has actually evaluated the efficiency of the photoprotection provided by these two processes or compared their role against photoinhibition in microphytobenthos biofilms. The distinction between photoprotection and photoinhibition processes from chlorophyll fluorescence cannot be inferred from the decrease in ETR or formation of NPQ under high light, but requires the analysis of the recovery kinetics of photosynthetic activity following exposure to high light stress [START_REF] Horton | Studies on the induction of chlorophyll fluorescence in isolated barley protoplasts. 4. Resolution of non-photochemical quenching[END_REF][START_REF] Walters | Resolution of components of non-photochemical chlorophyll fluorescence quenching in barley leaves[END_REF], Müller et al. 2001). In diatoms, a rapid (within minutes) component of this recovery can be attributed to the reversal of the xanthophyll cycle (q E , or 'energy-dependent quenching') while photoinhibitory effects (q I , or 'photoinhibitory quenching') can be quantified from a second, much slower (within hours) component (Müller et al. 2001[START_REF] Lavaud | Fast Regulation of Photosynthesis in Diatoms: Mechanisms, Evolution and Ecophysiology[END_REF]. The q T (state-transition related quenching) component of NPQ recovery, which shows intermediate relaxation kinetics, does not exist in diatoms (Owens, 1986) This study was set out to address these questions, for which a new experimental protocol was designed, based on the combination of (i) chlorophyll fluorescence imaging, to allow the simultaneous measurement of a large number of samples and experimental treatments, (ii) the use of specific inhibitors for vertical migration and for the xanthophyll cycle, to quantify the relative contribution of each process to overall photoprotection, and (iii) the analysis of the recovery kinetics of photosynthetic activity following light stress, to distinguish downregulation due to the xanthophyll cycle and photoinhibition. This approach was further used to test the influence of photoacclimation state on photoprotection capacity and susceptibility to photoinhibition in microphytobenthic biofilms inhabiting a temperate intertidal mudflat.

MATERIALS AND METHODS

Sampling and sample preparation. Sediment samples were collected in the upper zone of an intertidal mudflat in the Baie de l'Aiguillon (46º15'18'' N, 01º08'33'' W), France, in late spring (May) and autumn (October) 2010, expected to show contrasting photoacclimation states following the seasonal variation in solar radiation (see below). The sampling site is composed of fine muddy sediments (< 63 µm) where microphytobenthic biofilms are largely dominated by diatoms [START_REF] Herlory | Microstructure of microphytobenthic biofilm and its spatio-temporal dynamics in an intertidal mudflat (Aiguillon Bay, France)[END_REF]).

During low tide, samples of the surface layers of sediment (approximately the top 1 cm) were collected using a spatula. In the laboratory, the sediment was sieved through a 500-µm mesh, to remove the mud snails Hydrobia sp. and other meio-and macrofauna, and was thoroughly mixed and spread in 4 cm deep plastic trays. The sediment was covered by water collected in the sampling site and left undisturbed overnight. In the next morning, at the start of the photoperiod, the slurries were again homogenized and identical portions of the resulting slurry were transferred to 24-well plates using a small spatula, filling the wells completely (ca. 3 ml). The well plates were exposed to homogeneous light field provided by two LED panels (equal contribution of red, farred, blue and white LEDs; FloraLEDs panels, Plant Climatics, Germany) delivering a constant irradiance of 70 µmol quanta m -2 s -1 at the sample surface, in order to induce the upward migration of microalgae and the formation of the biofilm. Daily global solar radiation were obtained from a Meteo-France weather station located approximately 9 kms southwest from the sampling site, for two-week periods preceding the sampling dates, 15-30 May and 5-20 Octorber 2010.

Fluorescence measurements. Chlorophyll fluorescence was measured using an imaging-PAM fluorometer (Maxi-PAM M-series, Walz GmbH, Effeltrich, Germany).

The measuring area of the fluorometer covered each entire well plate, so that up to a total of 24 sediment samples could be monitored simultaneously. All experiments were carried out after biofilm formation. This was determined by measuring the fluorescence level F s , taken as a proxy for surface microalgal biomass, in a replicated set of samples exposed to constant low light of 55 µmol quanta m -2 s -1 . Experiments were started after F s reached a plateau following the initial rise after on the onset of the light period which typically took 2-3 hours of low light exposure. For each sample, the fluorescence signal was calculated by averaging the values of all pixels included in an area of ca. 63.6 mm 2 (area of interest), which corresponded to ca. 1500 pixels, centered inside each well. This area is smaller than the total area of each well (95.0 mm 2 ), the difference being due to the exclusion of the edge of each sample, often not representative of the rest of the biofilm. To minimize sample heating during prolonged exposure to high light, the experiments were carried out in a temperature-controlled room, at 20 ºC, and the fluorometer Perspex hood was maintained open at all times.

Photoacclimation: light-response curves. The photoacclimation state of the samples was characterized by measuring light-response curves of ETR and of NPQ in the two sampling periods. Light-response curves were generated by sequentially exposing the samples to 7 levels of actinic light, up to 700 μmol quanta m -2 s -1 . Samples were exposed to each light level for 3 min (a period previously confirmed allowing for reaching a steady-state), after which a saturation pulse was applied and fluorescence levels F s and F m ' were recorded. Six replicated measurements (on six different wells) were made for each light level. For each irradiance level, E, the relative ETR was calculated from the product of E and the PSII effective quantum yield, ∆F/F m ' [START_REF] Genty | The relationship between the quantum yield of photosynthetic electron transport and quenching of chlorophyll fluorescence[END_REF]

: ' ' ETR m s m F F F E   (1)
ETR vs E curves were quantitatively described by fitting the model of [START_REF] Eilers | A model for the relationship between light intensity and the rate of photosynthesis in phytoplankton[END_REF], and by estimating the parameters α (the initial slope of the curve), ETR m (maximum ETR) and E k (the light-saturation, or photoacclimation, parameter):

c E b E a E E    2 ) ETR( (2)
  kt rec m m rec m m e F F F F F F t F F         ' , ' ' , ' / ) 0 ( / / ) ( / (6)
where t is the time during recovery, ∆F/F m '(0) and ∆F/F m ' ,rec represent the PSII quantum yield levels at the start of the recovery period and after full recovery (associated to q E ), and k is the rate constant of ∆F/F m ' recovery. The values of ∆F/F m ' estimated by the model for t = 10.5 min, expressed as a percentage of the pre-stress levels, were used for estimating the effective photoprotective capacity of the biofilm. The remaining relative difference between pre-and post-stress levels of ∆F/F m ' was used as an estimate of the photoinhibitory effects imposed by high light.

The photoprotective roles of vertical migration and of the xanthophyll cycle were studied by applying specific inhibitors of the two processes. Vertical migration was inhibited by the diatom motility inhibitor Latrunculin (Lat) A, shown to effectively inhibit cell motility without causing appreciable effects on the photosynthetic activity (Cartaxana et al. 2008). To inhibit the activity of the xanthophyll cycle, the inhibitor of the diadinoxanthin de-epoxidase (DDE) dithiothreitol (DTT) was used. DTT is commonly used to inhibit the conversion of the pigment diadinoxanthin (DD) into the photoprotective form diatoxanthin (DT) (Lavaud et al. 2002a). DTT was applied in combination with Lat A, in order to ensure that the cells having the xanthophyll cycle inhibited remained exposed to high light.

The contribution of vertical migration to overall photoprotection capacity of the biofilm was estimated by the difference between the levels of ∆F/F m ' recovery in control (free moving cells) and Lat A-treated (vertical migration inhibited) samples. The contribution of the xanthophyll cycle was estimated by comparing the levels of ∆F/F m ' recovery in the samples treated with Lat A (only vertical migration inhibited) and in those treated with both Lat A and DTT (both vertical migration and the xanthophyll cycle inhibited). The inhibitor solutions were added after biofilm was fully formed, in a total of 200 μL for both the Lat A and the Lat A + DTT solutions. The same volume of filtered seawater was added to the control samples. The solutions were added carefully to minimize biofilm disturbance, by pipetting small volumes onto the sediment surface.

A minimum of 30 min was given for the inhibitors to diffuse and for the biofilms to stabilize before measurements were started.

Inhibitor preparation and effective dosage. Solutions of Lat A of different concentrations, ranging from 5 to 15 μM, were prepared from a concentrated solution (1 mM) prepared from dissolving purified Lat A (Sigma-Aldrich) in dimethylsulfoxide.

The minimum effective dosage of Lat A to induce inhibition of vertical migration was determined following Cartaxana & Serôdio (2008). Samples treated with different concentrations of Lat A (final volume, 200 μL) were darkened close to the time expected for tidal flood, known to induce a rapid downward migration. The degree of migration inhibition was estimated from the decrease in surface biomass following darkening, as estimated from dark-adapted fluorescence level, F o . Three replicated samples were tested for each Lat A concentration.

DTT (BDH-Prolabo) was prepared fresh as in Lavaud et al. (2002a). A stock solution of 300 mM (in ethanol) was diluted in filtered seawater to prepare working solutions of concentrations ranging from 3.3 to 15 mM. The minimum effective dosage of DTT was determined by measuring NPQ development upon exposure to 400 µmol quanta m -2 s -1 for 30 min in samples treated with increasing concentration of DTT (final volume, 200 μL). Three replicated samples were tested for each DTT concentration. For the light stress experiments, samples were treated with 200 µL of a combined solution of Lat A and DTT, prepared using the concentration of each inhibitor determined from the effective dosage tests (see Results).

Taxonomic composition. In one of the trays, microalgae were collected by covering the sediment with two layers of a 100 µm-mesh. The trays were exposed to low indirect natural light from a north facing window (< 200 µmol quanta m -2 s -1 ) during the day following the sampling. The upper mesh was removed at the time of middle emersion period and it was washed with filtered (0.2 µm) natural sea water. The samples were fixed in Lugol and preserved at 4°C until their analysis. Diatom species were identified and counted using definitive mounts in Naphrax after cleaning the cells by cremation (2 h, 450°C) [START_REF] Méléder | Spatio-temporal changes in microphytobenthos assemblages in a macrotidal flat (Bourgneuf Bay, France)[END_REF]. Taxonomic determination was performed by microscope on the basis of morphological criteria. A total of ca. 300 diatom frustules were counted to determine specific abundances.

RESULTS

Taxonomic composition

In both sampling periods, the microphytobenthic assemblages were dominated by long biraphid diatoms (length > 30 µm). In May, the assemblages were mainly dominated by Navicula cf. spartinentensis (61%, n = 350). Staurophora salina represented less than 20% of the assemblages but this species was two times longer than N. cf. spartinentensis (22 µm and 44 µm long, respectively). In October, the assemblages were co-dominated by Plagiotropis seriata (22%, n = 335) and Staurophora salina (19%); the size of P. seriata (190 µm long) was four times the one of S. salina one (44 µm long) strengthening its dominance in terms of biovolume. A third species, Pleurosigma strigosum (300 µm length) represented more than 10% of the assemblage abundance.

Photoacclimation

Significant differences were found between the light-response of ETR measured in May and October. In comparison with the ETR vs E curves measured in May, the ones measured in October presented significantly higher values of α (+26.7%, t-test, p < 0.001) and lower values of ETR m (-41.5%, t-test, p < 0.001) (Fig. 1A). As a consequence, the photoacclimation parameter E k was significantly lower in October than in May (-53.5%; t-test, p < 0.001). Regarding NPQ, significant differences were found between the light-response curves measured in the two periods (Fig. 1B). NPQ vs E curves measured in May reached lower levels within the range of applied irradiances (on average, 2.19 and 3.25 at 700 μmol quanta m -2 s -1 , in May and October, respectively), although the values of NPQ m were not significantly different (t-test, p = 0.425). The light-response curves were more sigmoid in May than in October (t-test, p = 0.001), the largest differences being found regarding the light level required for induction of NPQ, indicated by the parameter E 50 , which was significantly lower in October than in May (-38.5%; t-test, p = 0.003).

The light conditions in the region of the sampling area varied greatly between the two-week periods preceding the sampling periods, with global solar radiation reaching a daily average of 2369 J cm -2 in May, more than double the value observed in October, 1008 J cm -2 .

Inhibitor dosage

Vertical migration was strongly inhibited for most of the Lat A concentrations tested, with an inhibition level above 75% being obtained with only 5 μM (Fig. 2). The inhibitory response to the increase in Lat A concentration presented a clear saturationlike pattern, with the increase from 10 to 15 μM resulting in an increase in inhibition of only 8.5%. Considering that 10 μM was enough to inhibit vertical migration by more than 90%, and the small increase obtained by applying the higher concentrations, solutions of 10 μM Lat A were used in all experiments.

The response of NPQ to the increase in DTT also showed a saturation-like pattern, characterized by a strong decrease for concentrations up to 5 mM, and a virtually constancy for concentrations above this value (NPQ decreased by 19% between 5 and 15 mM; Fig. 3). However, even when the highest DTT concentration was applied, NPQ was never completely eliminated, remaining above 1.0. In all further experiments, a concentration of DTT of 10 mM was used.

Light stress exposure and recovery

Figure 4 exemplifies the variation of ∆F/F m ' during a light stress-recovery experiment. On control samples, exposure to high light induced an immediate and marked decrease in ∆F/F m ' from ca. 0.63 to values slightly below 0.1 (Fig. 4). ∆F/F m ' further decreased to values close to zero during the first 15 min of exposure, after which it gradually recovered, stabilizing at values around 0.1 after 90 min and until the end of the high light period. On inhibitor-treated samples, ∆F/F m ' also decreased to values close to zero upon the start of high light exposure, but, as opposed to control samples, never showed any appreciable recovery, remaining below 0.05 (Fig. 4). However, ∆F/F m ' levels were usually higher in Lat A-treated samples than in those treated with both inhibitors (Figs. 4,5). Following the transition to low light, a clear recovery response was observed for all samples, with ∆F/F m ' reaching in all cases over 60% of initial values after 15 min. Treatment with Lat A effectively inhibited vertical migration during the whole experiment, as indicated by the small variation in F s in Lat A-treated samples (on average, -12.1% for samples treated with Lat A and Lat A+DTT) as compared with the controls (-43.5%; Fig. 6). The effects of inhibitors were particularly evident during recovery under low light, during which ∆F/F m ' followed the negative exponential pattern described by Eq. ( 6), the fit of which was very good in all cases (r 2 > 0.91; Fig. 7). Control samples recovered more rapidly than those treated with inhibitors, so that after 3 min after return to low light, ∆F/F m ' of non-inhibited samples was over 70% and 60% higher than on samples treated with Lat A in May and October, respectively. In both periods these differences were gradually reduced during exposure to low light, but after 10.5 min the percentage of recovery was significantly different among treatments and sampling periods (two-way ANOVA, p < 0.001 for both factors).

In both May and October, the recovery of ∆F/F m ' was higher in the controls than in the Lat A-treated samples (Control vs Lat A; Tukey's post-hoc test, p = 0.043 and p = 0.010, respectively), which was in turn higher than in samples treated with Lat A and DTT (Lat A vs Lat A+DTT; Tukey's post-hoc test, p = 0.042 and p = 0.030, respectively). The percentage of recovery was in all cases significantly higher in May than in October (Tukey's post-hoc test, p < 0.05), with the exception of samples treated with both inhibitors (Tukey's post-hoc test, p = 0.107).

Photoprotection efficiency and extent of photoinhibition

Depending on the species, the full recovery of the xanthophyll cycle after a transition from high to low light mainly occurs after 6 min to 15 min (Goss et al. 2006, Lepetit & Lavaud, pers. obs.). Considering the intermediate period of 10.5 min, the recovery of ∆F/F m ' at this time was used as an estimate of the photoprotection capacity and to calculate the extent of photoinhibition occurred. The results indicate that the microphytobenthos biofilms had a large photoprotective capacity in both periods, with a correspondingly low percentage of photoinhibition below 25%, although higher in May than in October (87.7 and 78.0%; Fig. 8, Table 2). From the reduction in the photoprotection capacity measured in samples treated with inhibitors, the contribution of vertical migration and of the xanthophyll cycle to overall photoprotection were estimated to reach a combined value only slightly above 20% (Table 2). While in May the two processes had a comparable contribution to photoprotection, the relative importance of the xanthophyll cycle was reduced to 7.2% in October.

DISCUSSION

Photoacclimation and susceptibility to photoinhibition

Comparatively to May, samples collected in October appeared acclimated to lower light levels, showing the pattern typically associated to 'shade-acclimation': a combination of higher values of α and of lower values of ETR m , resulting in lower values of E k , usually taken as an indication of photosynthesis saturating at lower irradiances. This change in photoacclimation state between May and October was consistent with the observed seasonal change in solar light conditions preceding the two sampling periods (i.e. global solar radiation more than two times higher in May than in October). These results also generally confirmed previous observations on the seasonal variability of microphytobenthos photosynthetic performance, showing patterns of acclimation to higher light levels during spring/summer and to lower levels in autumn/winter (Blanchard et al. 1997[START_REF] Migné | In situ measurements of benthic primary production during emersion: seasonal variations and annual production in the Bay of Somme (eastern English Channel, France)[END_REF][START_REF] Serôdio | Rapid light-response curves of chlorophyll fluorescence in microalgae: relationship to steady-state light curves and non-photochemical quenching in benthic diatom-dominated assemblages[END_REF]. They were also consistent with the photoacclimation response of benthic diatoms grown in culture exposed to low and high-light regimes [START_REF] Jesus | Effects of vertical migrations by benthic microalgae on fluorescence measurements of photophysiology[END_REF], Schumann et al. 2007, Cruz & Serôdio 2008). Increases of α, as the observed from May to October, are commonly attributed to an increase in the cellular content of light-harvesting pigments, increasing the fraction of incident light that is intercepted and absorbed for photosynthesis; decreases in ETR m are typically associated with the decrease of the activity of the electron transport chain or the Calvin cycle, limiting factors of light-saturated photosynthesis [START_REF] Henley | Measurement and interpretation of photosynthetic light-response curves in algae in the context of photoinhibition and diel changes[END_REF][START_REF] Macintyre | Photoacclimation of photosynthesis irradiance response curves and photosynthetic pigments in microalgae and cyanobacteria[END_REF], Behrenfeld et al. 2004).

A change in light response was also noticeable regarding NPQ, with the samples collected in October showing NPQ activation starting at lower light levels (lower E 50 ) and higher values of NPQ for most irradiances (higher NPQ m ). As with ETR, the observed variation in the NPQ vs E curves was consistent with the previously reported for microphytobenthos [START_REF] Serôdio | Rapid light-response curves of chlorophyll fluorescence in microalgae: relationship to steady-state light curves and non-photochemical quenching in benthic diatom-dominated assemblages[END_REF] or for benthic diatoms acclimated to different light regimes (Cruz & Serôdio 2008). However, while changes in the light-response of ETR may be interpreted and related to underlying physiological processes in a relatively straightforward manner, the physiological meaning of changes in NPQ levels is more difficult to ascertain. This is because the two components of NPQ, q E (photoprotection) and q I (photoinhibition) can only be distinguished through the analysis of the recovery kinetics after exposure to high light, but not from NPQ light curves. In this study, the light stress-recovery experiments allowed to conclude that the observed change in the NPQ light-response curves was due to a decrease in the q E component and a concomitant increase in the q I component. In the absence of information from NPQ recovery kinetics, similar increases in NPQ vs E curves in autumn/winter periods have been, perhaps wrongly, interpreted as being due to an increase in photoprotective capacity [START_REF] Serôdio | Non-photochemical quenching of chlorophyll fluorescence and operation of the xanthophyll cycle in estuarine microphytobenthos[END_REF][START_REF] Serôdio | Rapid light-response curves of chlorophyll fluorescence in microalgae: relationship to steady-state light curves and non-photochemical quenching in benthic diatom-dominated assemblages[END_REF].

Furthermore, the results from the light stress-recovery experiments revealed an association between photoacclimation status and photoprotection efficiency, not shown before for these communities. Whatever the cause (see below), the acclimation to high light levels in summer was associated to a high photoprotection capacity and the low light-acclimation in autumn to a general loss in photoprotection and a higher susceptibility to photoinhibition.

Photoprotection vs photoinhibition

A central finding of this study is that photoinhibition was in all cases considerably low (ca. 20%), indicating photoprotection to be particularly efficient in the studied microphytobenthos biofilms. Despite the general view that these assemblages are largely immune to photoinhibition [START_REF] Herlory | Microstructure of microphytobenthic biofilm and its spatio-temporal dynamics in an intertidal mudflat (Aiguillon Bay, France)[END_REF][START_REF] Waring | Responses of estuarine intertidal microphytobenthic algal assemblages to enhanced ultraviolet B radiation[END_REF], Mouget et al. 2008), this process has been shown to occur under in situ conditions [START_REF] Serôdio | Photosynthetic activity, photoprotection and photoinhibition in intertidal microphytobenthos as studied in situ using variable chlorophyll fluorescence[END_REF]. Curiously, the rates of photoinhibition estimated in the cited study, reaching up to ca. 18%, are similar to the values here reported, despite the fact that they were estimated from hysteresis patterns observed during entire low tide exposure periods. The results of the present study therefore confirm that the photoprotective mechanisms available to benthic diatoms are not completely efficient in preventing some degree of photoinhibitory damage. However, it should be stressed the difficulty in comparing the measured rates of photoinhibition with results published for other habitats, or for other estuarine primary producers such as phytoplankton, seagrasses or macroalgae. Apart from the light history and the species-specific differences, the extent of photoinhibition is directly related to light dosage, determined by light intensity and duration of exposure, both largely variable amongst the different experimental protocols used in different laboratory and field studies.

A number of unaccounted factors may have contributed for the measured low values of q I . Firstly, the well-known effect of depth-integration of subsurface fluorescence [START_REF] Forster | Modelling the effects of chlorophyll fluorescence from subsurface layers on photosynthetic efficiency measurements in microphytobenthic algae[END_REF][START_REF] Serôdio | Analysis of variable chlorophyll fluorescence in microphytobenthos assemblages: implications of the use of depth-integrated measurements[END_REF]). This effect is caused by the fact that only the cells at or near the surface are actually exposed to measured levels of high light, and that the fluorescence signal measured at the surface also accounts for cells positioned deeper in the photic zone and exposed to lower light levels. The expected effect is a light-dependent overestimation of biofilm-level ∆F/F m ' relatively to the inherent, physiological values of the cells at the surface, which is then expected to cause a systematic overestimation of q E and the underestimated of q I [START_REF] Serôdio | Analysis of variable chlorophyll fluorescence in microphytobenthos assemblages: implications of the use of depth-integrated measurements[END_REF]). However, besides this static effect, also dynamic effects can be expected. During prolonged exposure to high light, the downward migration of microalgae to less illuminated layers is likely to induce a gradual increase of ∆F/F m ' (as measured at the surface), independently of any photophysiological changes, thus causing the overestimation of q E . It is also conceivable that these types of effects may affect the measurement of ∆F/F m ' during the recovery under low light, due to upward migration as a response to the decrease in incident irradiance. This, however, seems less likely due to the relatively short time of this period and to the fact that a transition from high to low light is a weaker stimulus for vertical migration, especially if coinciding with the end of the low tide period [START_REF] Coelho | Endogenous versus environmental control of vertical migration by intertidal benthic microalgae[END_REF].

A second factor that might explain the low values of q I is the light doses applied during the light stress-recovery experiments in the laboratory. Because these (3 hrs, 1200 µmol quanta m -2 s -1 ) were likely lower than the ones received during a typical period of exposure at low tide (up to 8-10 hrs, 1500-2000 µmol quanta m -2 s -1 ), larger, but still ecologically relevant, light doses could have been applied which would likely induce larger cumulative photoinhibitory effects. The light exposure conditions applied in this study, both regarding light intensity and duration, resulted from a compromise between inducing measurable effects, instrument limitations (maximum PAR irradiance provided by the imaging fluorometer) and minimizing uncontrollable experimental conditions (excessive sample heating and desiccation caused by the fluorometer LED panel). Despite these limitations, mostly instrument-related, the laboratory experimental approach used in this study has the advantage over studies carried out under in situ conditions (e.g. [START_REF] Serôdio | Photosynthetic activity, photoprotection and photoinhibition in intertidal microphytobenthos as studied in situ using variable chlorophyll fluorescence[END_REF][START_REF] Perkins | Vertical cell movement is the primary response of intertidal benthic biofilms to increasing light dose[END_REF]) of allowing applying controlled and reproducible conditions, making it possible to directly compare the migratory and physiological responses of samples collected in different places and occasions.

The estimation of q E and q I is also directly affected by the type of analysis made on the recovery kinetics in order to distinguish the two components of NPQ. For higher plants, q E and q I are distinguished on the basis of the recovery rate of F v /F m , typically 10-15 min, assumed to correspond to the full reversal of the xanthophyll cycle [START_REF] Horton | Studies on the induction of chlorophyll fluorescence in isolated barley protoplasts. 4. Resolution of non-photochemical quenching[END_REF], Ruban & Horton 1995). Following the common practice for the distinction of q E and q I , in this study these two components of NPQ were estimated based on a relaxation time of the xanthophyll cycle of 10.5 min. However, to evaluate the possible effects of considering different times for the reversal of the xanthophyll cycle on the relative magnitude of q E and q I , a sensitivity analysis was performed, consisting on the re-calculation of these estimates when considering 6 and 15 min, values matching the range of relaxation times of the xanthophyll cycle expectable for diatoms (Gross et al. 2006, Lepetit & Lavaud, pers. obs.). The use of these different recovery periods did not alter significantly the general findings of the study, including high levels of recovery and low photoinhibition rates, the increase in photoinhibition levels from May to October, and a relatively low (< 30%) combined contribution of vertical migration and xanthophyll cycle to overall photoprotection (Table 2).

Nonetheless, this analysis shows some effects, although largely expected from the asymptotic pattern of ∆F/F m ' recovery during the considered period: the use of a shorter period resulted in the estimation of lower rates of recovery, leading to a likely overestimation of photoinhibition rates; conversely, longer periods resulted in larger rates of recovery and probably overestimated levels of photoprotection (Table 2).

Moreover, due to the different relaxation patterns of samples exposed to different treatments, the evaluation of the relative importance of vertical migration and the xanthophyll cycle was also affected by the time period considered, with shorter and longer recovery periods resulting in a higher apparent contribution of vertical migration and of the xanthophyll cycle, respectively. These effects, however, did not affect substantially the overall pattern of variation of the role of the two photoprotective processes between the two sampling periods.

Recently, more sophisticated methods, based on the mathematical modeling and deconvolution of the recovery curve, were proposed to trace the recovery of each individual component of NPQ [START_REF] Roháček | Method for resolution and quantification of components of the nonphotochemical quenching (q N )[END_REF]). This method could not be applied in this study because of the particularities of the xanthophyll cycle in diatoms, which may not verify the assumptions of the method. Firstly, the lack of q T (the state-transition quenching) in diatoms (Owens 1986[START_REF] Lavaud | Fast Regulation of Photosynthesis in Diatoms: Mechanisms, Evolution and Ecophysiology[END_REF][START_REF] Goss | Regulation and function of xanthophyll cycle-dependent photoprotection in algae[END_REF], which called for the modification of this model to a two-component NPQ. Secondly, the impossibility of using changes in F v /F m in biofilms as an indication of photoinhibition, as this requires the darkening of the samples, known to induce changes in F m levels due to vertical migration. Furthermore, in benthic diatoms, dark adaptation often causes the F m level to decrease to values below F m ' levels measured under low light [START_REF] Serôdio | Rapid light-response curves of chlorophyll fluorescence in microalgae: relationship to steady-state light curves and non-photochemical quenching in benthic diatom-dominated assemblages[END_REF]. These reasons also prevented the use of other recently proposed methods to quantify the components of NPQ (Ahn et al. 2009[START_REF] Guadagno | A revised energy partitioning approach to assess the yields of non-photochemical quenching components[END_REF].

The formation of DT in the dark and thus anoxic subsurface layers of the sediment, known to occur in diatoms [START_REF] Jakob | Unusual pH-dependence of diadinoxanthin deepoxidase activation causes chlororespiratory induced accumulation of diatoxanthin in the diatom Phaeodactylum tricornutum[END_REF], and especially in benthic assemblages [START_REF] Serôdio | Rapid light-response curves of chlorophyll fluorescence in microalgae: relationship to steady-state light curves and non-photochemical quenching in benthic diatom-dominated assemblages[END_REF], is a likely explanation for the apparent impossibility to completely eliminate NPQ by applying the xanthophyll cycle inhibitor DTT (Fig. 3).

The DT thus formed would remain present despite the treatment with DTT, which prevents new conversion of DD to DT, but does not induce the reversed reaction. Upon exposure to high light, the oxygenation of DT-rich subsurface layers would allow for the observed rise in NPQ, as the formation of NPQ from DT is known to be inhibited by anoxia [START_REF] Cruz | Impact of chlororespiration on non-photochemical quenching of chlorophyll fluorescence and on the regulation of the diadinoxanthin cycle in the diatom Thalassiosira pseudonana[END_REF].

Photoprotection: vertical migration vs xanthophyll cycle

The use of specific inhibitors for vertical migration and for the operation of the xanthophyll cycle allowed estimating the relative contribution of each of these processes to overall photoprotection of the biofilm. The results showed a change with season and photoacclimation state of their relative importance. While in May the two processes seemed to contribute similarly to biofilm photoprotection, the loss of photoprotection capacity from May to October was associated to a decrease in the contribution of the xanthophyll cycle, so that vertical migration became the dominant photoprotective process. The observed change in the species composition of the microphytobenthic assemblage may explain this difference as the activity of the xanthophyll cycle can differ from a species to another (Lavaud et al. 2004[START_REF] Goss | The importance of a highly active and ΔpH-regulated diatoxanthin epoxidase for the regulation of the PS II antenna function in diadinoxanthin containing algae[END_REF]). It may be also hypothesized that this difference is related to the decrease in rates of enzymatic conversion between DD and DT associated to photoacclimation or due to acclimation to lower temperatures (Van Leuwee et al. 2008), an effect that is also species-related [START_REF] Salleh | The effects of temperature on the photosynthetic parameter s and recovery of two temperate benthic microalgae, Amphora cf. coffeaeformis and cocconeis cf. sublittoralis (Bacillariophyceae)[END_REF]. Nevertheless, these results indicate that behavioral photoprotection seems able to maintain the overall photoprotection capacity, compensating for the decrease in the contribution of the xanthophyll cycle during the winter season.

The change in species composition, involving a dominance of larger cells in October, could also have affected the migratory response of the assemblages to high light. However, although some studies have shown a relation between migratory cell size and migratory behaviour in sediments [START_REF] Hay | The speed of diatom migration through natural and artificial substrata[END_REF][START_REF] Underwood | Patterns in microphytobenthic primary productivity: Species-specific variation in migratory rhythms and photosynthetic efficiency in mixed-species biofilms[END_REF], there is no evidence that cell size is an important factor regarding the migratory response to light stress.

Vertical migration and the xanthophyll cycle have been considered as the main photoprotective mechanisms in microphytobenthos biofilms [START_REF] Serôdio | Non-photochemical quenching of chlorophyll fluorescence and operation of the xanthophyll cycle in estuarine microphytobenthos[END_REF][START_REF] Jesus | Effects of vertical migrations by benthic microalgae on fluorescence measurements of photophysiology[END_REF], Mouget et al. 2008, Serôdio et al. 2008;[START_REF] Perkins | Vertical cell movement is the primary response of intertidal benthic biofilms to increasing light dose[END_REF]. A perhaps surprising result of this study is the relative low contribution of these two processes to global photoprotection. This calls for the potential role of other processes responsible for the observed low rates of photoinhibition. Likely candidates include the cyclic electron flow around PSII (Lavaud et al. 2002b[START_REF] Lavaud | Fast Regulation of Photosynthesis in Diatoms: Mechanisms, Evolution and Ecophysiology[END_REF], the efficient scavenging of reactive oxygen species [START_REF] Roncarati | Photosynthetic performance, oxidative damage and antioxidants in Cylindrotheca closterium in response to high irradiance, UVB radiation and salinity[END_REF][START_REF] Waring | Light-induced responses of oxygen photoreduction, reactive oxygen species production and scavenging in two diatom species[END_REF]) or high turnover rates of the PSII protein D1 [START_REF] Wu | Distinctive photosystem II photoinactivation and protein dynamics in marine diatoms[END_REF].

Use of inhibitors on microphytobenthic biofilms

An aim of this study was the introduction of a new experimental protocol to estimate photoprotection efficiency and the extent of photoinhibition in microphytobenthos biofilms. This involved the combination of: (i) the use of specific inhibitors for different photoprotective processes, applied alone and in combination with each other, allowing the estimation of the relative contribution of each process to overall photoprotection, and (ii) the use of imaging fluorometry on replicated samples in well plates, taking advantage of the self-forming nature of microphytobenthos biofilms from homogenized sediments, which allowed for adequate replication and low variability between replicates, and for the simultaneous testing of different treatments. Some potential pitfalls exist regarding the use of inhibitors on biofilms and the interpretation of results. Firstly, it must be noted that when comparing controls (no inhibitor added) with Lat A-treated samples, it is likely that the differences in fluorescence parameters observed over time may not be attributed only to changes in cell physiological conditions but also to changes in cell composition in the upper layers of the sediment. This is because in the controls, as opposed to Lat A-treated samples, cells initially at the surface likely migrated down into layers below the photic zone, therefore changing the contribution to the fluorescence signal measured at the surface.

As a consequence, any observed differences are expected to represent mainly changes at the biofilm (i.e., community)-level, and not only changes in the physiology of individual cells. This also explains the need to combine Lat A and DTT if the effect of inhibiting the xanthophyll cycle is to be evaluated in the same microalgal assemblage.

By adding DTT to samples treated with Lat A, it is ensured that the same cells remain in the photic zone of the sediment and that measured changes in fluorescence are due to changes in their physiological status and not to changes in community composition. If only DTT is applied [START_REF] Perkins | Vertical cell movement is the primary response of intertidal benthic biofilms to increasing light dose[END_REF], only biofilm-level effects can be evaluated, as

  photoinhibition in microphytobenthos biofilms?', 'What is the relative contribution of

  Photoprotection vs photoinhibition: light stress-recovery experiments. The

  photoinhibition in intertidal microphytobenthos. J Phycol 40:692-696

  Photoinhibition12.3 ± 0.55

Fig. 4 .

 4 Fig. 4. Light stress-recovery experiment. Variation of PSII quantum yield, ∆F/F m ', during sequential exposure to low light (pre-stress, 55 µmol quanta m -2 s -1 ), light stress under high light (high light, 1200 µmol quanta m -2 s -1 , 180 min) and recovery under low light (recovery, 55 µmol quanta m -2 s -1 , 10.5 min) for controls and for samples treated

Figure 8

 8 Figure 8

Acknowledgements. We thank Dr. Céline Vincent for providing solar radiation data.

This study was supported by FCT -Fundação para a Ciência e a Tecnologia, through grants SFRH/BSAB/962/2009 (J. Serôdio), SFRH/BD/44860/2008 (J. Ezequiel), and project MigROS (PTDC/MAR/112473/2009), and by the CNRS -Centre National de la Recherche Scientifique ('chercheurs invités' program, J. Serôdio and J. Lavaud), the region Charente-Maritime/CG17 (A. Barnett Ph.D. grant), and the French consortium CPER-Littoral., . We thank two anonymous reviewers for critical comments on the manuscript.

many cells will likely respond to high light by migrating downward and become unobservable (Oxborough et al. 2000). NPQ m , maximum NPQ level in a NPQ vs E curve PAR, photosynthetically active radiation PSII, photosystem II q E , energy-dependent quenching q I , photoinhibitory quenching t, time during recovery following light stress XC, xanthophyll cycle first low light exposure (pre-stress, 55 µmol quanta m -2 s -1 ), at the end of high light exposure (high light, 1200 µmol quanta m -2 s -1 , 180 min) and following recovery under low light (recovery, 55 µmol quanta m -2 s -1 , 10.5 min). Three replicated areas of interest for each treatment. Fig. 6. Images of fluorescence level F s (false color scale) as measured in the sediment samples used in the light stress experiment described in Fig. 4. at the end of first low light exposure (pre-stress, 55 µmol quanta m -2 s -1 ), and after recovery following end of high light exposure (high light, 1200 µmol quanta m -2 s -1 , 180 min; recovery, 55 µmol quanta m -2 s -1 , 10.5 min). Three replicated areas of interest for each treatment.