Hugo Herbelin
email: hugo.herbelin@inria.fr

Arnaud Spiwack
email: arnaud@spiwack.net

The Rooster and the Syntactic Bracket *

Keywords: 1998 ACM Subject Classification F.3.3 Studies of Program Constructs Coq, Calculus of inductive constructions, Impredicativity, Strictly positive type families, Inductive type families Digital Object Identifier 10.4230/LIPIcs.xxx.yyy.p = | eo : Even | es : Odd → Even with Odd : Type := | eo : EvenOdd true | es : EvenOdd false → EvenOdd true | os : EvenOdd true → EvenOdd false. Definition Even := EvenOdd true. Definition Odd := EvenOdd false

We propose an extension of pure type systems with an algebraic presentation of inductive and co-inductive type families with proper indices. This type theory supports coercions toward from smaller sorts to bigger sorts via explicit type construction, as well as impredicative sorts. Type families in impredicative sorts are constructed with a bracketing operation. The necessary restrictions of pattern-matching from impredicative sorts to types are confined to the bracketing construct. This type theory gives an alternative presentation to the calculus of inductive constructions on which the Coq proof assistant is an implementation.

Introduction

In the Coq proof assistant [14] inductive types are treated as toplevel definitions. If it makes sense from a convenience or an efficiency point of view, the monolithic nature of the definitions make it hard to describe what they precisely mean. As a matter of fact, inductive definitions mean different things depending on the type they are defined in: specifically, some types are interpreted differently in impredicative sorts like Prop or the impredicative variant of Set.

In this article, we present a calculus of inductive and co-inductive constructions where inductive and co-inductive types are presented algebraically. The algebraic presentation is an extension of a PTS [3] with inductive and co-inductive type families. Thanks to its modularity, it is meant to serve as a description which is simpler to expose and more mathematically amenable than the monolithic scheme which is found in a practical system such as Coq. For the sake of clarity, the system is given with a single universe and explicit subtyping, although Coq has an unbounded cumulative hierarchy of universes and implicit subtyping. Apart from these technicalities, it is believed that our calculus of algebraic inductive and co-inductive constructions expresses all the features of the Set-impredicative Calculus of Inductive Constructions that Coq implements, e.g. in its version 8.4 when launched with option -impredicative-set. This work draws most of its inspiration from Morris & al [9,10] for the algebraic presentation of inductive type families in a predicative sort, and Awodey & Bauer [2] for the treatment of impredicative sorts.

Γ ⊢ u : x:A B Γ ⊢ v : A Γ ⊢ u v : B[ x \ v ] Γ ⊢ u : A Γ ⊢ B : s A ≡ B Γ ⊢ u : B λx A . u v ❀ u[ x \ v ]
We use examples from Coq to illustrate the algebraic presentation. To differentiate expressions in Coq from expressions in the algebraic presentation, the former are typeset in a sans-serif font and the latter in a roman font. and ✷, together with the following axiom: Γ ⊢ Type : ✷ and the following product formation rule: Γ ⊢ A : s 1 Γ, x:A ⊢ B : s 2 Γ ⊢ x:A B : max s 1 s 2 where max s s = s and max Type ✷ = max ✷ Type = ✷ The sorts Type and ✷ are predicative. The sort ✷ plays a technical role in allowing type variable and the formation of type-level functions; it cannot, however, be referenced in terms. In the following sections, ✷ will also be used to be able to define types by pattern-matching (strong elimination).

To model the entire Coq system, Type and ✷ would be replaced with a hierarchy of predicative sorts Type i , such that Γ ⊢ Type i : Type i+1 are axioms. Adapting the presentation to a hierarchy of sorts is straightforward, but in the interest of keeping to the heart of the matter we give a presentation with two sorts. This encoding works as long as all the mutual definitions are all in the same sort. A variant for mutual definition involving Type and Prop is demonstrated in Section 4.3. When the types being defined are in different predicative sorts, however, we have to resort to another encoding which involves nested datatypes [4,Section 8.6].

We will not explore the latter kind of mutual definition. However, nested datatypeswhere recursive calls occur as arguments of another type -such as:

Inductive List (A:Type) : Type := | nil : List A | cons : A → List A → List A. Inductive Tree : Type := | node : List Tree → Tree.
are indeed modelled in the algebraic presentation.

Regular types

To be able to traverse terms of inductive type, the core pts constructions is extended with a recursive fixed point on functions:

Γ ⊢ x1:A1,. . . ,xn-1:An-1,xn:An B : s guarded f x 1 . . . x n-1 x n u Γ, f : x1:A1,. . . ,xn-1:An-1,xn:An B, x 1 :A 1 , . . . , x n-1 :A n-1 , x n :A n ⊢ u : B Γ ⊢ fix f x 1 :A 1 . . . x n-1 :A n-1 x n :A n ⇒ u : x1:A1,. . . ,xn-1:An-1,xn:An B
Recursive fixed points are unfolded when fully applied

(fix f x 1 :A 1 . . . x n :A n ⇒ u) v 1 . . . v n ❀ u[ x i \ v i ]
To ensure strong normalisation, this reduction rule is limited, and a guard condition is imposed on the recursive calls to f . It is not, however, the object of this article to discuss these restriction or the guard condition. Briefly, Coq currently relies on a single structural argument in the block x 1 , . . . , x n : fixed points are not unfolded until their structural argument starts with a constructor, and the guard condition ensures that each recursive call is performed on a subterm of said structural argument, for a relaxed notion of subterm. Other possibilities exist: Agda2 [11] uses any number of arguments as structural, and tries to find a lexicographic ordering. Yet another possibilities is to use sized types [1]. We shall simply assume that an adequate guard condition is given.

We now extend the grammar of type constructors. The presentation of this article is largely inspired by the synthetic definition of strictly positive families by Morris & al [9,10], but is adapted to intensional type theory. The presentation of [9,10] is designed for generic programming inside a type theory, they give codes for strictly positive families which are then decoded into an actual type of the ambient theory. No elimination principle needs to be given for the strictly positive families, as they are implicit in their decoding. Here, we are defining the syntax of inductive type families, including their elimination rules.

Sum type

Γ ⊢ A : Type Γ ⊢ B : Type Γ ⊢ A + B : Type Γ ⊢ A + B : s Γ ⊢ t : A Γ ⊢ inl t : A + B Γ ⊢ A + B : s Γ ⊢ u : B Γ ⊢ inr u : A + B Γ ⊢ u : A + B Γ, x:A + B ⊢ P : s Γ, y:A ⊢ v : P [ x \ inl y ] Γ, z:A ⊢ w : P [ x \ inr z ] Γ ⊢ match u as x return P with inl y ⇒ v inr z ⇒ w : P [ x \ u ] match inl u as x return P with inl y ⇒ v inr z ⇒ w ❀ v[ y \ u ] match inr u as x return P with inl y ⇒ v inr z ⇒ w ❀ w[ z \ u ] Unit type Γ ⊢ 1 : Type Γ ⊢ () : 1 Γ ⊢ u : 1 Γ, x:1 ⊢ P : s Γ ⊢ v : P [ x \ () ] Γ ⊢ match u as x return P with () ⇒ v : P [ x \ u ] match () as x return P with () ⇒ v ❀ v Empty type Γ ⊢ 0 : Type Γ ⊢ u : 0 Γ ⊢ A : Type Γ ⊢ match u return A with • : A Figure 2 Regular type constructors
often omit the typing predicate when it is clear from the context, especially when it does not depend on the branch. With this material we can define a first example type, namely the booleans:

     B = 1 + 1 true = inl () false = inr ()

Inductive type families

Inductive families differ from regular inductive types in that they are parametrised by indices, that is they are functions F : A → Type for some A. An inductive family of the form λx A . R, is said to be uniformly parametrised by A. In general, inductive families are not uniformly parametrised: the value of the index is allowed to vary in recursive calls, and constructors may build values of F x for certain x only. Remember, for instance, the EvenOdd family:

Inductive EvenOdd : bool → Type := | eo : EvenOdd true | es : EvenOdd false → EvenOdd true | os : EvenOdd true → EvenOdd false.
The inductive family constructors, presented in Figure 3, warrant individual discussion. First, notice that as a simplifying hypothesis, inductive families have exactly one index. This is, of course, not a limitation in expressive power as multiple indices can be encoded as a dependent sum, and the unit type allows us to write families without an index.

The construction µX A→Type . F constructs the inductive fixed point of F . It acts on type families, because indices vary through recursive calls to X. To be able to form an inductive fixed point, occurrences of X must be strictly positive in F , rules for strict positivity are given in Figure 4. The rules of Figure 4 are a simple set which suits the needs of this article, however in practice, we may want to consider strict positivity rules involving elimination rules and a finer treatment of application. Strict positivity ensures that no non-terminating term can be written without recursive fixed points, so that the guard condition suffices to enforce termination. Paradoxes which can be derived from non-positive or non-strictly positive inductive fixed points can be found in [13,Chapter 4,Section 4.2][8,Chapter 3][4,Chapter 8]. To avoid clutter, we give a presentation where inductive fixed points can be freely rolled and unrolled thanks to the conversion. An alternative can be to give an explicit term constructor for fixed points, see Section 3.4.

We will also use an inductive fixed point on nullary families, defined as:

µX Type . F = µY 1→Type . F [ X \ Y () ] ()
from which we have that µX Type . F can be freely rolled from or unrolled to F X \ µX Type . F . With inductive fixed points, we can, for instance, define the accessibility predicate. In Coq:

Inductive Acc (A:Type) (R:A→A→Type) (x:A) : Type := | acc_intro : (forall y:A, R y x → Acc A R y) → Acc A R x.

Inductive fixed point

Γ ⊢ A : s Γ, X:A → Type ⊢ F : A → Type sp X F Γ ⊢ µX A→Type . F : A → Type µX A→s . F ≡ F X \ µX A→s . F Proper indices Γ ⊢ A : Type Γ ⊢ B : Type Γ, x:A ⊢ T : Type Γ, x:A ⊢ f : B Γ ⊢ f x:A T : B → Type Γ ⊢ f x:A T : B → s Γ ⊢ u : A Γ ⊢ v : T [ x \ u ] Γ ⊢ (u, v) f x:A.T : f x:A T (f [ x \ u ]) Γ ⊢ u : f x:A T b Γ, y:B, z: f x:A T y ⊢ P : s Γ, i:A, j:T i ⊢ v : P y \ f i , z \ (i, j) f x:A.T Γ ⊢ match u as z in y return P with (i, j) f x:A.T ⇒ v : P [ y \ b , z \ u ] match (u, v) f x:A.T as z in y return P with (i, j) f x:A.T ⇒ w ❀ w[ i \ u , j \ v ] Figure 3 Inductive type families sp X y sp X 0 sp X 1 X is fresh in A sp X B sp X ( x:A B) sp X A sp X B sp X (A + B) X is fresh in A sp X F sp X µY A . F X is fresh in A sp X T sp X λx A . T sp X U X is fresh in t sp X (U t) sp X B B ≡ A sp X A X is fresh in f sp X A sp X T sp X f x:A T Figure 4 Strict positivity condition
This type represents the generic form of termination proofs: any terminating recursive fixed point can be made structural over a proof of accessibility. In the algebraic presentation, it is defined as:

     Acc = λA Type R A→A→Type . µAcc A→Type . λx A . y:A R y x → Acc y acc intro = λA Type R A→A→Type x A f y:A R y x→Acc A R y . f
Because inductive fixed points are treated transparently, the constructor is rather trivial. However, notice how, in the definition of Acc, the parameter x is treated differently from A and R. The reason is that A and R are uniform parameters, in that they do not vary through recursive calls, whereas x does: it is a non-uniform parameter. The parameter x is, hence, represented as an index. However, such an index is not sufficient to encode types like EvenOdd.

Representing proper indices requires a new type construction, which we write f x:A T . This construction comes from [9,10], where it is inspired by a categorical point of view: in a sufficiently extensional setting, f x:A T is the right adjoint to a pullback functor. The similarity with the usual notation of dependent sum is not fortuitous, indeed we can define dependent sum as a special case of proper indexing:

     x:A B = () x:A B () (u, v) x:A.B = (u, v) () x:A.B
We also write A × B and (u, v) for x:A B and (u, v) x:A.B , respectively, when x is not free in B.

In the case of dependent sums, the index is trivial. When it is not, however, the pattern matching return clause P is allowed to depend on the value of the index. This is the purpose of Coq's in-pattern. With the algebraic presentation, the in-pattern has the pleasant property of being confined to the proper indexing construction, hopefully making its meaning more explicit. The syntax differs a little from that of Coq, however: Coq renders the in clause as a pattern with the type name at the head: match n as n' in EvenOdd b return P n' b with . . . end.

In the algebraic presentation, types not having a name, the in clause simply consists of a name for the index.

The prototype of proper indexing is the identity type, which we name Eq. In Coq:

Inductive Eq (A:Type) (x:A) :

A → Type := | eq_refl : Eq A x x
in the algebraic presentation:

   Eq = λA Type x A . x _:1 1 eq refl = λA Type x A . ((), ()) x _:1.1
In fact, dependent sums and identity types are sufficient to define proper indexing. Indeed f x:A T can be redefined as:

     f x:A T = λy B . x:A (Eq B y f ) × T (u, v) f x:A.T = (u, (eq refl B f [ x \ u ], v)) x:A.(Eq B (f [ x \ u ]) f )×T
It is closer to the spirit of Coq, but in no way essential, to take a proper indexing construction rather than equality as primitive. In Morris & al [9,10], the dependent sum and equality of the ambient type theory is used to define f x:A T which is then taken as primitive. An other choice lies in the use of A + B as primitive. It is the only type construction which allows to define a type with distinct elements. However, a common alternative is to take B as primitive, in which case we can define A + B as: translates, in the algebraic presentation, to: Note that in the definition of Tree, we must β-reduce List Tree for the recursive definition to be strictly positive.

                         A + B = b:B match b with true ⇒ A false ⇒ B inl = λx A . (true,
               EvenOdd = µEvenOdd B→Type .
A more complex example is given by the type of lists indexed by their length, often called vectors:

Inductive Nat : Type := | o : Nat | s : Nat → Nat. Inductive Vector (A:Type) : Nat → Type := | vnil : Vector A o | vcons : forall n, A → Vector A n → Vector A (s n).
It is encoded in the algebraic presentation as:

                           Nat = µNat Type . 1 + Nat o = inl () s = λn Nat . inr n Vector = λA Type . µV Nat→Type . λn Nat . o _:1 1 n + s n ′ n ′ :Nat A × V n ′ n vnil = λA Type . inl ((), ()) o _:1.1 vcons = λA Type n Nat a A v Vector n a . inr (n, (a, v)) s n ′ n ′ :Nat.A×V n ′
Contrary to proper indices, the types of non-uniform parameters are allowed to be in ✷, this allows the definition of types such as the binary lists [12]: Inductive BList (A:Type) :

Type := | one : A → BList A | twice : BList (A * A) → BList A | stwice : A → BList (A * A) → BList A
which are rendered in the algebraic presentation as: A×A) . inr (inl l) stwice = λA Type x A l BList (A×A) . inr (inr (a, l))

           BList = µBList Type→Type . λA Type . A + (BList (A × A) + A × (BList (A × A))) one = λA Type x A . inl x twice = λA Type l BList (
In Coq, where there is a hierarchy of universe, types of proper indices can be in any sort. However, a proper index whose type is in Type i constrains the final type to be in Type i+1 or higher. Uniform parameters, of any type, do not constrain the type they parametrise.

Co-induction

In addition to inductive fixed points, Coq also has support for co-inductive fixed points. Co-inductive fixed points are required to be strictly positive, like inductive fixed points. We choose in this section, a presentation of co-inductive data where fixed points are explicitly introduced with a constructor. Below we will use this explicit presentation to give a variation on Coq's co-inductive fixed points.

Γ ⊢ A : s Γ, X:A → Type ⊢ F : A → Type sp X F Γ ⊢ νX A→Type . F : A → Type Γ ⊢ νX A→s . F : A → s Γ ⊢ i : A Γ ⊢ u : F X \ νX A→s . F i Γ ⊢ forced u : νX A→s . F i Γ ⊢ νX A→s . F : A → s Γ ⊢ i : A Γ ⊢ u : νX A→s . F i Γ, x: νX A→s . F i ⊢ P : s ′ Γ, y:F X \ νX A→s . F i ⊢ v : P [ x \ forced y ] Γ ⊢ match u as x return P with forced y ⇒ v : P [ x \ u ] match forced u as x return P with forced y ⇒ v ❀ v[ y \ u ]
Just like inductive data is destructed by a recursive fixed point operation, co-inductive data is constructed by a co-recursive fixed point operation, allowing co-inductive data to be infinite. The guard condition on co-recursive fixed points ensures that a finite number of unfolding will eventually produce a forced value. Γ ⊢ x1:A1,. . . ,xn:An νX A→s . F i : s coguarded f x 1 . . . x n u Γ, f : x1:A1,. . . ,xn:An νX A→s . F i, x 1 :A 1 , . . . , x n :A n ⊢ u : νX A→s . F i Γ ⊢ cofix f x 1 :A 1 . . . x n :A n ⇒ u : x1:A1,. . . ,xn:An νX A→s . F i Co-recursive fixed-point are meant to represent infinite data: they cannot be unfolded eagerly, lest they would fail to terminate. They are unfolded only when they appear at the head of a pattern-matching expression:

match (cofix f x 1 :A 1 . . . x n :A n ⇒ u) v 1 . . . v n as x return P with forced y ⇒ v ❀ match u[ f \ (cofix f x 1 :A 1 . . . x n :A n ⇒ u) , x i \ v i ] as x return P with forced y ⇒ v
The dependent elimination rule for co-inductive fixed points asserts, in essence, that every co-inductive data is of the form forced u. Even though it would be fine for inductive fixed points -this is why we could leave the unrolling to the conversion -this does not reflect well the computational aspects of co-inductive data: suspended co-recursive fixed points are values, and won't be evaluated until the context demands it. The fact that the elimination for co-inductive data claims that all values are forced gives rise to undesirable behaviour.

Take for instance the following simple co-inductive type, and data:

T = νX. X i = cofix i ⇒ forced i
So that i is effectively an infinite sequence of forced. Using the elimination principle above, it is possible to give a closed proof that Eq T i (forced i):

match i as x return Eq T x forced match x with forced y ⇒ y with forced y ⇒ eq refl T y

However, i and (forced i) are not convertible, yet, as every closed proof of equality does, this proof reduces to eq refl , hence should relate convertible terms. The dependent elimination rule of co-inductive fixed points compromises the type safety of the logic. Coq uses the above dependent elimination rule for co-inductive fixed points. It was a deliberate decision made for practical purposes. Nonetheless, one may want to weaken it to avoid the incompatibility between equality and conversion. To do so, it suffices to erase the dependency of the return predicate over the matched term:

Γ ⊢ νX A→s . F : A → s Γ ⊢ i : A Γ ⊢ u : νX A→s . F i Γ ⊢ P : s ′ Γ ⊢ v : P Γ ⊢
match u return P with forced y ⇒ v : P

Prop

With all the common baggage for predicative sorts set in place, we can add impredicative sorts to the algebraic presentation. The main such sort in Coq is the sort Prop of propositions.

The design of Prop is guided by proof irrelevance: even if it is not actually provable in Coq, different proofs of a proposition are thought of as being equal. This property is useful for program extraction: only the computationally relevant parts of a program need to be executed to get the final result. In other words: propositions are considered as static data.

It is why, with disjunction and existential defined as:

Inductive Or (A B:Prop) : Prop := | or_introl : A → A ∨ B | or_intror : B → A ∨ B.
Inductive Ex (A:Type) (P:A→Prop) : Prop := | ex_intro : forall x:A, P x → Ex A P.

the following terms are refused by type-checking:

match x with | or_introl _ ⇒ true | or_intror _ ⇒ false end.
and

match x with | ex_intro x _ ⇒ x end.
On the other hand, it is not the case of every inductive type defined in Prop, that they cannot be eliminated into Type. Conjunction and falsity are two counter-examples: Inductive False : Prop := . Inductive And (A B:Prop) :

Prop := | conj : A → B → A ∧ B.
Coq allows elimination over these two propositions into Type, and both following terms are well-typed: match x return Bool with end.

and This definition simply makes {A} a synonym of A, except of sort Type. It is strictly positive in A:

match x with | conj _ _ ⇒ true end. Γ ⊢ 0 : Prop Γ ⊢ 1 : Prop Γ ⊢ A : Prop Γ ⊢ B : Prop Γ, x:A ⊢ T : Prop Γ, x:A ⊢ f : B Γ ⊢ f x:A T : B → Prop
sp X A sp X {A}
The fact that Prop is impredicativei.e. supports the following product formation rules:

Γ ⊢ A : s Γ, x:A ⊢ B : Prop Γ ⊢ x:A B : Prop
is easily understood in terms of proof irrelevance. Indeed, if for all x, B has at most one element, so has the product over x. Even though it uses functional extensionality, which is not provable.

Singleton rules

The types which (ideally) preserve the proof irrelevance property are sometimes called singleton types in the setting of Coq. In our algebraic presentation, they correspond to inductive type family constructors with extra formation rules to make them preserve propositions. The rules are shown in Figure 5. This elucidates why Coq allows elimination over False and And into arbitrary type: False is implemented as 0 and And A B and A × B.

The elimination rules being unchanged, pattern-matching over proofs of False and And are unrestricted. Because restricted pattern-matching is often seen as the default, singleton types are said to enjoy singleton elimination.

Remark that, proofs of propositions being uninformative, there is essentially nothing to be gained from depending on, or being indexed over a proposition. In consequence, the type formation rule for proper indexing in Figure 5 is only useful, in practice, for the subcase of cartesian product.

Coq actually implements two other singleton rules. The first one is for inductive fixed points. In our algebraic presentation:

Γ ⊢ A : s Γ, X:A → Prop ⊢ F : A → Prop sp X F Γ ⊢ µX A→Prop . F : A → Prop
It allows to type the accessibility predicate Acc in Prop. This rule is sound in that fixed points indeed preserve proof irrelevance in presence of functional extensionality. It is also very useful for extraction: structural recursion over Acc allows the definition of functions whose termination cannot be proved automatically by the guard condition. However, the proof is no longer needed to ensure termination in the target languages of extraction. In this sense, at least, it is static data.

The last singleton rule allows properly indexed families in Prop (not how it is stronger than the rule dependent sum of Figure 5):

Γ ⊢ A : Prop Γ ⊢ B : Type Γ, x:A ⊢ T : Prop Γ, x:A ⊢ f : B Γ ⊢ f x:A T : B → Prop
It turns the identity type Eq into a proposition. It is known to be sound to accept that Eq is proof irrelevant [6]. It is also useful for extraction, as equal types, in a closed environment, are extracted to the same type. Hence a program may safely eliminate over Eq knowing that it will not affect the performances of the extracted code. In Coq, the index B in the rule above can be of any sort Type i , however, this wisdom has been challenged in recent years with the formulation of the univalence principle [15], of which a simple consequence is that Eq is not proof irrelevant at every type. Indeed, some extracted Coq programs written assuming the univalence principle crash.

To correct for the univalence principle, the singleton rule for proper indices can be simply dropped; but it can also be restricted to the lowest sort: B : Type 0 . More precisely the conjunction of the univalence principle and the proof irrelevance principle is consistent as long as the singleton rule of proper indices is restricted to sorts s such that there is no sort s ′ other than Prop such that s ′ : s. Because, if such a sort s ′ exists, B : s ′ and by univalence, Eq B has two distinct elements contradicting proof irrelevance.

For types which do not enjoy singleton elimination, turning them into propositions means restricting their elimination. We achieve this effect by adding a single type construction coercing from Type to Prop:

Γ ⊢ A : Type Γ ⊢ [A] : Prop Γ ⊢ u : A Γ ⊢ u : [A] Γ ⊢ u : [A] Γ, x: [A] ⊢ P : Prop Γ, y:A ⊢ v : P [ x \ y ] Γ ⊢ match u as x return P with y ⇒ v : P [ x \ u ] match u as x return P with y ⇒ v ❀ v[ y \ u ]
The important rule is the elimination rule, where the return clause is limited to be of sort Prop, whereas every other type construction can be eliminated to any sort. Apart from this restriction [A] is a synonym of A, except in Prop. In [2], the type theory is extensional, in that the identity type and the conversion relation coincide. The elimination rules for bracket is much finer and reflects precisely the fact that propositions are proof-irrelevant. In an intensional type theory, restricting with respect to sorts approximates this behaviour: even if we constrained propositions to be proof-irrelevant, not every proof irrelevant type will have type Prop. The bracketing construction is also strictly positive:

sp X A sp X [A]
It is actually possible, using only the impredicative dependent product to define a bracketing operation: P :Prop (A → P ) → P . Like [A] it behaves as A except it can only be used to form a proposition. However, the impredicative encoding is positive but not strictly, which motivates the introduction of the extra construction.

Examples

The logical connectives can be defined as follows:

                                       False = 0 And = λA Prop B Prop . A × B pair = λA Prop B Prop x A y B . (x, y) Or = λA Prop B Prop . [A + B] or introl = λA Prop B Prop x A . inl x or intror = λA Prop B Prop y B . inr y Ex = λA Type P A→Prop . x:A P x ex intro = λA Type P A→Prop x A p P x . (x, p) x:A.P
Note how, because of the brackets, existentials and disjunctions are prohibited from being eliminated to non-propositional types. Thanks to the singleton rules, however, conjunction and falsity do not require brackets.

As a final example, consider the type Ascending n p of ascending sequences of integers between p and n defined by mutual recursion with the proposition Ge m p which stands from m is greater than or equal to p: As Ascending has type Type, whereas Ge has type Prop, the translation to a single inductive type is not as straightforward as Even and Odd. The translation requires the use of brackets around the recursive calls:

                       AscendingGe = µX (Nat×Nat)+(Nat×Nat)→Type . λi (Nat×Nat)+(Nat×Nat) . inl (n,n) n:Nat 1 i + inl j j:Nat×Nat m:Nat [X (inr (m, s (π 2 j)))] × X (inl (π 1 j, m)) i + inr j j:Nat×Nat X (inl j) i Ascending = λn p. AscendingGe (inl (n, p)) Ge = λm p. [AscendingGe (inr (m, p))] Impredicative Set
In addition to the impredicative sort Prop, Coq has a sort Set which is predicative by default but can be turned impredicative with a flag. Where Prop is meant to be used in the context of separating static and dynamic information, the spirit of the impredicative sort Set is to be as powerful as possible without being inconsistent. In the algebraic presentation, that means being stable by every construction except dependent sums with the first projection in an arbitrary sort (strong sums).

To mirror the optional nature of the impredicativity of Set, the rules for a predicative sort Set are given in Figure 6; to turn impredicativity on, the rules of Figure 7 must be used in addition to those of predicative Set. This presentation makes immediately apparent that impredicative Set is an extension of predicative Set, in that every program of the latter typechecks in the former.

The rules of Set are the same as those of Prop, with the exception of A + B which is in Set when both A and B are -even with predicative Set. Hence, there are types in Set with several elementse.g. B. As a consequence, the bracketing operation which coerces types in Type to Set does not enjoy an explanation in terms of proof irrelevance, as was the case in Prop. As a matter of fact, there is no clear set-theoretical description at all. A close cousin of Set bracketing, however, can be found in homotopy type theory [15], where, roughly, groupoids are truncated to sets through a quotient of their homsets by the total relation.

Conclusion

The algebraic presentation of Coq makes the conversion between sorts explicit. The toplevel inductive definitions of Coq can be understood as implicitly inserting canonical bracketing operations when an inductive type is declared inside an impredicative sort but should be of a different sort due to its form; and inserting type coercion from a smaller sort to a bigger sort when applying a cumulativity rule. Monolithic type definitions like in Coq have a number of advantages over the algebraic presentation, they boil down to better type errors due to naming, better type inference and better memory representation due to n-ary sums and products. However, the value of the implicit coercions between sorts is less clear. In particular, the bracketing operation to impredicative sorts is probably a better guide for program extraction than the current method of figuring whether or not a given type is a proposition, which interacts badly with universe polymorphism [7]. Explicit coercions for extraction are also in the spirit of [5].

Figure 1

 1 Figure 1 Generic rules of pts

  x) b:B. match b with true ⇒ A false ⇒ B inr = λy B . (false, y) concludes the description of the predicative fragment of the algebraic presentation. We can now give definitions of the remaining inductive families we have encountered in terms of the algebraic presentation. Starting with EvenOdd: Inductive EvenOdd : bool → Type := | eo : EvenOdd true | es : EvenOdd false → EvenOdd true | os : EvenOdd true → EvenOdd false.

  Here is the definition of List in Coq:Inductive List (A:Type) : Type := | nil : List A | cons : A → List A → List A.and in the algebraic presentation: Type . µList Type . 1 + A × List nil = λA Type . inl () cons = λA Type x A l List A . inr (x, l) Finally the definition of Tree: Inductive Tree : Type := | node : List Tree → Tree. translates to: Tree = µTree Type . List Tree node = λf List Tree . f

  Inductive types are consumed by recursive fixed points. Using the implicit unfolding of inductive fixed points, we can pattern-match over the top constructor directly. The Coq function Fixpoint add (x y:Nat) : Nat := match y with | o ⇒ x | s y' ⇒ s (add x y') end is rendered in the algebraic presentation as add = fix add x:Nat y:Nat ⇒ match y as _ return Nat with inl _ ⇒ x inr y ′ ⇒ s (add x y ′ )

Figure 5

 5 Figure 5 Singleton rules

Inductive

  Ascending : Nat → Nat → Type := | top : forall n, Ascending n n | up : forall n p m, Ge m (s p) → Ascending n m → Ascending n p with Ge : Nat → Nat → Prop := | ascend : forall m p, Ascending m p → Ge m p.

The Rooster and the Syntactic BracketΓ ⊢ A : s x is fresh in Γ Γ, x:A ⊢ x : A Γ ⊢ u : A Γ ⊢ B : s x is fresh in Γ Γ, x:B ⊢ u : A Γ ⊢ x:A B : s Γ, x:A ⊢ u : B Γ ⊢ λx A . u : x:A B

Pure type systemsTo model the type system of Coq, we start with the classic presentation of pure type systems (pts) ofBarendregt [3], which we will then extend to model type families. A pts is characterised by a single syntactic category of terms which are used both as λ-terms and as types. It has a single form of typing judgment Γ ⊢ u : A, where u and A are terms, and Γ a context assigning terms to variables. A pts has a set of sorts, which we shall denote schematically by the symbol s. Every sort is an atomic term. A pts has a conversion relation u ≡ v. Here we diverge from the presentation of [3] which always uses β-conversion. Coq, on the other hand, uses βη-conversion on the fragment described in this section. In this article we will take the conversion rule as abstract, not even requiring it to be decidable. We will only require that it contains all the reduction rules which are given in the form u ❀ v (in this section, we only have β-reduction).The typing rules of a pts comprise of a set of generic rules given in Figure1, together with a number of rules of the form ⊢ s 1 : s 2 called axioms, and rules of the form Γ ⊢ A : s 1 Γ, x:A ⊢ B : s 2 Γ ⊢ x:A B : s

of product formation rules. As usual we write A → B for x:A B when x does not bind a variable in B.As a starting point of the algebraic presentation, we shall use a pts with two sorts, Type

The regular type constructors, whose typing rules are given in Figure2, are the empty type 0, the unit type 1, and the sum of two types. The elimination rules are given in the form of dependent pattern-matching with a syntax made to remind of that of Coq. We shall

The object of this section is to make syntactically explicit what happens when an inductive type of Coq is declared to be of sort Prop. The description elaborated in this section has strong similarities with the system of bracket-types proposed byAwodey & Bauer [2]. They describe the propositions as the subset of types with at most one element, and introduce a left adjoint, written as brackets, to the inclusion of propositions into types. We will reuse their notation, even though, in our intensional setting, T:Prop does not enforce that T has a most one element, and the bracketing operation does not properly form an adjunction with the inclusion from Prop to Type.4.1 ImpredicativityLet us start by introducing the new sort Prop in the algebraic presentation: Γ ⊢ Prop : Type As in[2], propositions form a subset of types. Coq has a subtyping rule (also known as cumulativity) to make the inclusion transparent. We will, however, render it with a syntactic construct:Γ ⊢ A : Prop Γ ⊢ {A} : Type Γ ⊢ u : A Γ ⊢ prf u : {A} Γ ⊢ u : {A} Γ, x: {A} ⊢ P : s Γ, y:A ⊢ v : P [ x \ prf y ] Γ ⊢ match uas x return P with prf y ⇒ v : P [ x \ u ] match prf u as x return P with prf y ⇒ v ❀ v[ y \ u ]

All of the algebraic type constructors can actually be defined in Coq, except the two fixed-points because there is no way to abstract over strictly positive type families. So is it clear that expressions of the algebraic presentation which do not use inductive or co-inductive fixed points can be translated into Coq. Occurrences of the fixed points in a type must be λ-lifted and given a toplevel name. Some care must be given to avoiding the duplication of such definitions otherwise types which must be convertible for the expression to typecheck, might be seen as different in the Coq translation. Apart from this technicality, translation from the algebraic presentation to Coq is straightforward. We claim that, at least if we extend the algebraic presentation to a hierarchy of universes and the strict positivity condition is made a bit more fine-grained, Coq terms can be, conversely, translated into the algebraic presentation.

Γ ⊢ Set : Type Γ ⊢ A : Set Γ, x:A ⊢ B : Set Γ ⊢ x:A B : Set Γ ⊢ A : Set Γ, x:A ⊢ P : Set Γ ⊢ x:A P : Set Γ ⊢ A : Set Γ ⊢ B : Set Γ ⊢ A + B : Set Γ ⊢ 1 : Set Γ ⊢ 0 : Set Γ ⊢ A : s Γ, X:A → Set ⊢ F : A → Set sp X F Γ ⊢ µX A→Set . F : A → Set Γ ⊢ A : Set Γ ⊢ B : Set Γ, x:A ⊢ T : Set Γ, x:A ⊢ f : B Γ ⊢ f x:A T : B → Set Γ ⊢ A : s Γ, X:A → Set ⊢ F : A → Set sp X F Γ ⊢ νX A→Set . F : A → Set Γ ⊢ A : Set

The Rooster and the Syntactic BracketΓ ⊢ A : s Γ, x:A ⊢ B : Set Γ ⊢ x:A B : Set sp X A sp X [A] Set Γ ⊢ A : Type

* This research has received funding from the European Research Council under the FP7 grant agreement 278673, Project MemCAD


Did You Say Reference Conditions? Ecological and Socio-economic Perspectives on the European Water Framework

achieve the objectives must be compared in terms of cost and efficiency; and, 3) water quality data must be systematically collected and made public. Through this process, the European WFD regulations aim to make water-related policies more accountable, particularly to funders, in the form of quantitative indicators. The concept of reference conditions had never been used before the WFD in European water policy. We argue that it is a historically situated concept which corresponds to specific needs of the actors who promoted the WFD. The "driving-forces, pressures, state, impact, response" conceptual model that also imbues the WFD has older roots, but it similarly met some of the needs of the WFD writers.

. The scope of the second wave of directives (1988)(1989)(1990)(1991) regulated waste waters and natural waters affected by eutrophication. However, Member States could restrict the implementation of these directives to specific zones. In 1994, many natural waters remained out of the scope of European law.

Michelle Cini (1995) studied how employees of the Directorate-General for the environment (DG Environment) of the EC promoted the precautionary principle. She noticed that they developed a specific political discourse of ecological modernization which reconciles economic growth -a dominant motto in other DG-with environmental conservation in a specific manner. It consists in arguing that some elements of the environment are vital for human survival and must be protected at all costs by precaution, while the protection of others may be subjected to cost-benefit analyses. The WFD is influenced by this discourse. It prohibits the use of hazardous substances. It holds that the good ecological status must be achieved whatever the cost, except for the water bodies that are highly modified by profitable activities.

. A similar uniform baseline in ecology was yet lacking. The EQW draft (Commission of the European communities, 1994) did not set ecological requirements in quantitative terms. It integrated aesthetic and natural heritage considerations into restoration objectives. The focus was primarily on water quality and secondarily on biological connectivity in river systems. The term "reference conditions" was not used. The text prescribed high ecological water quality and sediment quality as meeting the needs of the ecosystem, especially the capacity for "self-purification", high level of biological diversity (aquatic plants, invertebrates, fish, amphibians, mammals and birds), and the absence of toxics and diseases linked to human activities. The objectives were articulated in terms of hydrosystem functions and 3 The Convention for the Protection of the marine Environment of the North-East Atlantic

Introduction

The European Water Framework Directive1 (WFD) aims to protect and improve the ecological status of aquatic systems in order to promote sustainable watershed use and ensure an adequate water supply. In all cases, Member States must reduce the use of hazardous substances and ensure that water pricing encourages conservation. Each Member State must define water quality objectives for every water body (river or consistent hydrogeological unit) within its jurisdiction, conduct a watershed assessment, and prescribe appropriate restoration measures within a given timeline. Member states and the Commission agreed upon a common implementation strategy, with a EU team of national experts working together in order to ensure harmonization across national assessment methods of water ecological quality. This process is known as the intercalibration exercise and is less than half completed [START_REF] Birk | Intercalibrating classifications of ecological status: Europe's quest for common management objectives for aquatic ecosystems[END_REF].

The assessment of the ecological status of a water body is a relatively new and innovative policy for water quality management; earlier directives merely imposed standards for water chemistry and only targeted the waters used for specific purposes. The integration of biological criteria with water quality standards raises questions about how to quantify and assess biodiversity in aquatic ecosystems and how to address changes in those systems over time.

In this paper 2 , we combine perspectives from sociology and ecology to examine the concepts and tools associated with the WFD and identify challenges to implementing the WFD in the context of global climate change. We are particularly interested in the evolution of technical terms used by the scientific community over the last 20 years of WFD discussion and implementation to describe the concepts of reference conditions and the precautionary principle, from the production of the first version of the WFD in 1994 through the end of the European bioindicator intercalibration in April, 2012. We argue that such concepts used in the WFD are hardly grounded in current ecological theories and are difficult to apply in a context of changing environment and long-term interactions between man and nature. But they corresponded to specific needs from different institutions and stakeholders which promoted them. By integrating insights from multiple disciplines, we can identify the practical advances made possible by the WFD and build a foundation for developing management guidelines in the future.

We mainly focus on the use of reference condition in relation with biological indicators because the ecological assessment of water bodies, in comparison with the chemical assessment, is one of the most innovative characteristic of the WFD.

Reference conditions: a historically situated policy concept

The Water Framework Directive provides a specific framework for evaluating water policies: 1) water quality objectives must be set in relation to reference conditions; 2) actions to 3 services, rather than descriptors of biological communities. Each Member State was responsible for developing its own definition of "good conditions" and for implementing restoration measures.

In the following years, despite Council rejection of the text, policy-makers in DG Environment went on looking for more quantitative binding ecological standards and selected a small group of scientists willing to proceed in this direction [START_REF] Loupsans | L'expertise sous tensions. Cultures épistémiques et politiques à l'épreuve de l'écriture de la directive cadre européenne sur l'eau[END_REF]. The outcome of this process is Annex V of the WFD. Reference conditions can therefore be understood as a political concept EC policy-makers needed to anchor a uniform norm-setting for all European surface waters to ecology. However, the adoption of the concept in the WFD did not follow a linear path.

In 1995, the Dutch, French and British governments challenged the EQW directive and the classic community method for water policy all together. They released several position papers pointing the lack of coherence among existing EU water policy. They managed to convince the EC to adopt an integrated strategy, that would give Member States more flexibility in setting environmental standards and optimizing ways of goal attainment [START_REF] Dezalay | De la défense de l'environnement au développement durable. L'émergence d'un champ d'expertise des politiques européennes[END_REF]Santbergen, 2013:115-6). The drafting of the WFD followed. In 1998 and 1999, the Council tried to get rid of legally-binding ecological objectives but the Parliament reintroduced them during the codecision procedure [START_REF] Kaika | The EU water framework directive: part1 European policy making and the changing topography of lobbying[END_REF]. The Council eventually accepted this clause because the WFD included intrinsic exemptions (Article 4) offering ample provisions for local adaptation to regional conditions and economic considerations. The resulting ambition of the WFD is highly ambiguous, leaving many choices and interpretations open for the implementation phase [START_REF] Barone | La directive-cadre sur l'eau et ses traductions : que nous apprennent les sites 'innovants[END_REF][START_REF] Hering | The European Water Framework Directive at the age of 10: A critical review of the achievements with recommendations for the future[END_REF][START_REF] Junier | Implementing the Water Framework Directive: lessons for the second planning cycle[END_REF][START_REF] Keessen | European River Basin Districts: Are They Swimming in the Same Implementation Pool?[END_REF][START_REF] Santbergen | Ambiguous Ambitions in the Meuse Theatre[END_REF].

While the ecological content of the WFD (Annex V) is still framed according the community method, the rest of the WFD instead corresponds to a new governance model [START_REF] Scott | Mind the Gap: Law and New Approaches to Governance in the European Union[END_REF], with a focus on implementation procedures, such as consultation requirements, transparency concerns, and reporting obligations. [START_REF] Santbergen | Ambiguous Ambitions in the Meuse Theatre[END_REF] argues that this part of the WFD shows a strong influence of the British philosophy for managing the environment at the most cost-effective way [START_REF] Dezalay | De la défense de l'environnement au développement durable. L'émergence d'un champ d'expertise des politiques européennes[END_REF][START_REF] Knill | Environmental politics in the European Union[END_REF]. Indeed, the WFD holds that Member states shall "make judgments about the most cost-effective combination of measures" (Annex III). Comparing the cost-effectiveness of different measures requires a common "reference", which does not need to be a uniform ecological baseline throughout Europe. However the concept of reference conditions could do the job in combination with a general framework for comparing options of restoration. In the environmental field, the OECD developed such a conceptual framework (pressure, state, response) in 1993 to compare management actions (responses) that aim to reduce impacting activities (pressures) to achieve a desired state (OECD, 1993(OECD, , 1994)). This framework was subsequently amended (driving forces, pressure, state, impact, response or DPSIR) by the European Environment Agency and used to assess the state of European water bodies and the effectiveness of water quality policies [START_REF] Eea | Inland Waters -Europe's Environment: The Dobris Assessment 1994[END_REF]. The DPSIR model is a method for cost-benefit analysis based on mitigation logic [START_REF] Fernandez | Bringing politics back into water planning scenarios in Europe[END_REF]. The model aims to compensate for pressure from socioeconomic forces by using political and economic responses to influence human activities and prevent environmental degradation. Pressures and responses are made commensurable by selecting appropriate indicators. The logic of this model underlies the entire WFD, as evidenced by the high occurrence of the terms "impact" (67) "pressures" (26), "status" (242) and "measures" (126)

Author-produced version of the article produced in Environmental Science & Policy, 2015, 47, 32-41 The original publication is available at http://www.sciencedirect.com/science/article/pii/S1462901114002044 doi:10.1016/j.envsci. 2014.10.012 in this context in the English version4 . Apart from a few restrictions (see Part 4), the directive requires programs of measures (Art 11 of the WFD) to mitigate for "inevitable" pressures (see Figure 1). This model of compensation hinges on the target of the good state for each body of water, which is defined by a non-significant deviation to a reference value on the scale, and which is achieved through restoration actions.

Last but not least, the concept of reference conditions helps coordinating the work of expert committees towards a unified monitoring network. This issue was addressed in the intercalibration exercise which "yielded a fundamental and unified vision of what constitutes good ecology across Europe" [START_REF] Birk | Intercalibrating classifications of ecological status: Europe's quest for common management objectives for aquatic ecosystems[END_REF]. It is based on a "significant level of statistical abstraction" (ibid. :490) which contrasts with compliance indicators used in the classic community method that were easy to verify. Intercomparability (of waterbodies) and intercalibration (of indicators) raised technical stakes hardly accessible to the general public. Only experts commissioned by Member States may learn from each other through this process. This relates to the open method of coordination [START_REF] Kraemer | Environment and Water Management, Conference 'Sustainable Development in an Enlarged Union -Linking National Strategies & Strengthening European Coherence[END_REF][START_REF] Radaelli | The Open Method of Coordination: A new governance architecture for the European Union?[END_REF] inscribed in the Lisbon Strategy, which seeks Member States convergence through benchmarking rather than compliance to binding standards. The socio-historical background on environmental public policy given above allows us to understand the inclusion of the reference conditions concept in the WFD as a flexible concept that was compatible with three different philosophies: setting legally-binding standards, assessing the cost-effectiveness of measures, and coordinating the implementation of Member States with common benchmarks. . In Europe, the conceptual framework of the WFD was met with enthusiasm by several national organizations, which are responsible for the management of aquatic ecosystems, including river basin authorities and environmental agencies. Members of these organizations have long sought an economic argument to justify the protection of the environment and help establish priorities. However, the conceptual design of the WFD probably would not have withstood criticism from skeptics [START_REF] Moss | The Water Framework Directive: Total environment or political compromise?[END_REF]had it not also received input from other experts in building its quantitative methodological framework (scale of measurement, benchmarks and set of metrics).

Implementing the reference conditions as an operative concept in the WFD

The WFD defines the reference conditions for an ecological system as the conditions that prevail in the absence or near absence of human disturbance5 . This corresponds to hydromorphological, physico-chemical and biological characteristics of "undisturbed," pollutant concentrations close to zero, and synthetic and non-synthetic pollutants at levels below "background noise." To assess ecological characteristics, a regionalized aquatic typology is used that accounts for variation in biodiversity due to ecoregional characteristics (hydro-climatic, physical habitat and biotic trophic factors) in water bodies of a similar size [START_REF] Hughes | Ecoregions : an approach to surface water protection[END_REF][START_REF] Omernik | Ecoregions of the Conterminous United States[END_REF]. A 'good condition' refers to any size of deviation from the reference typology that does not lead to significant changes in biological communities. A more significant deviation is interpreted as a sign of disruption of the key factors that determine local biodiversity. This approach assumes a possible return to a 'good condition' if the cause of disturbance is suppressed, provided the disturbance has not caused irreversible harm.

This definition of an ecologically 'good condition' is similar to that used in the United States in the Clean Water Act of 1972 (U.S. [START_REF] House | Report of the Committee on Public Works, United States House of Representatives, with additional and supplemental views. H.R. 11896 to amend the Federal Water Pollution Control Act, 92nd Congress[END_REF]. It refers to the "natural" character of the ecosystem (its structure and function) and is directly linked to the concept of biotic integrity [START_REF] Karr | Assessment of Biotic Integrity using fish communities[END_REF]. Recently, this concept and the criteria for evaluating a deviation from reference conditions have been codified in the United States [START_REF] Davies | The biological condition gradient: a descriptive model for interpreting change in aquatic ecosystems[END_REF] and Australia (Water Reform Framework in [START_REF] Stoddard | Setting expectations for the ecological condition of streams: the concept of reference condition[END_REF] . The description of the reference condition is based on knowledge of sites with desired characteristics. This can include knowledge of "pristine" (that is to say, "untouched") sites, but may also include historical knowledge, or even expert opinions or the results of simple modeling techniques.

The concept of reference conditions has been used for many years in other fields like forest ecology and paleolimnology, [START_REF] Swetnam | Applied historical ecology: using the past to manage the future[END_REF]. Interdisciplinary approaches are used to describe changes in ecosystems and/or landscapes over the long term (up to millennia). Such reconstructions have driven the evolution of a new academic field, "applied historical ecology," which explicitly uses the concept of reference conditions to guide restoration actions and the management of natural systems [START_REF] Egan | The Historical Ecology Handbook. A restorationist's guide on reference ecosystems[END_REF]. In forest ecology, historical reference conditions are viewed as reflecting the long term variability of the structure, composition and process of ecosystems over time [START_REF] Fulé | Determining reference conditions for ecosystem management of southwestern ponderosa pine forests[END_REF], providing insights to natural disturbance regimes [START_REF] Kaufmann | Forest reference conditions for ecosystem management in the Sacramento Mountains[END_REF]. Reference conditions are reconstructed from multiple sources depending of the spatial and temporal scale considered (documentary archives, dendrochronology, palynology, remote sensing…).

In comparison, Annex V of the WFD relies upon an assessment of the deviation from a state of stable reference conditions 6 , which are defined using criteria related to species abundance and taxa richness associated with regional environments. In the WFD, the biological indicators are restricted to aquatic environments. Hydro-morphological alterations are more taken into account in the WFD than in the EQW directive. As a result, the WFD definition of environmental objectives is imbued with what Steyaert and Ollivier (2007) named a "communitarian perspective" on environmental objectives, which excludes "human activities to build up the reference conditions of water" and gives "advantage to the pristine model of nature". This model is consistent with the concept of reference conditions. Considerations for humans are not to be found in the ecological part of the directive but in the economic part, which in contrast is inspired by a "utilitarian perspective" (ibid.; [START_REF] Bouleau | The WFD Dreams: between ecology and economics[END_REF]. In contrast with the EQW directive the WFD abandons natural heritage and aesthetic considerations and does not consider any more the terrestrial part of the fluvial corridor (riparian zone, bird, amphibians and mammals). The division of labor between ecology, which is responsible for determining environmental standards, and economics, which is responsible for optimizing regulations by determining prices once standards are set, corresponds to the neoclassical school of environmental economics [START_REF] Anderson | Free Market Environmentalism[END_REF].

Developing ecological standards raises the question of their social legitimacy. Why would some ecotypes, species or functions be preserved and not others? Historically, ecological indicators were constructed to quantify problems that were of public concern at specific scales and over certain time periods [START_REF] Bouleau | How ecological indicators construction reveals social changes -the case of lakes and rivers in France[END_REF][START_REF] Turnhout | The effectiveness of boundary objects: the case of ecological indicators[END_REF]. These indicators would not necessarily be appropriate at other spatial-temporal scales. The definition of "good" in the WFD aimed to standardize the various national methods of assessment and make a "good condition" in hydrosystems comparable across all Member States (i.e., the European intercalibration process). In practice, the implementation of these principles has been extremely variable from State to State based on the availability of data and resources, the bio-indicators and types of water bodies considered, and even the pre-existing schools of thought among freshwater biologists and managers. "Reference conditions" are alternatively defined by [START_REF] Stoddard | Setting expectations for the ecological condition of streams: the concept of reference condition[END_REF] as: -The biotic integrity or "natural" state for which long-term variability is acceptable within relatively narrow limits (steady state).

-A state corresponding to conditions encountered in minimally disturbed areas. Here we accept minimum disturbance over large areas.

-A condition or state that existed prior to any human modification considered "important" by the authors. For example, [START_REF] Wallin | Final guidance on establishing reference conditions and ecological status class boundaries for inland surface waters EU Common Implementation Strategy (CIS) for the Water Framework Directive[END_REF] consider the period prior to the development of intensive agriculture and/or industrialization (circa 1850 in England and 1750 in Germany) to be the reference condition, regardless of previous human impacts 7 . 6 The drafters of the WFD were aware that there would eventually be changes (spontaneous or anthropogenic) in ecological status (see infra note 8). In their minds, however, these changes would occur slowly over time and would not call into question the purpose of restoration. 7 These approaches do not take into account the effects of shifting cultivation or medieval land clearing on hydrosystems.

Author-produced version of the article produced in Environmental Science & Policy, 2015, 47, 32-41 The original publication is available at http://www.sciencedirect.com/science/article/pii/S1462901114002044 doi:10.1016/j.envsci.2014.10.012

-The least disturbed condition in a given area. Criteria (water quality, development, land use, etc.) are defined and used to select sites.

-The best state potentially achievable. This is the state that one can expect to achieve at a relatively degraded site if one applies all possible management measures in terms of ecological restoration (for example, in the Netherlands). This diversity of approaches reflects the contrasting views among the ecologists and scientists who were involved in the translation of the WFD into operational terms. The most common existing approach is the selection of conditions that are minimally disturbed or undisturbed based on certain anthropogenic pressures. Germany and Austria more strictly refer to the concept of biotic integrity, combining historical and expert approaches [START_REF] Schmutz | A multi-level concept for fish-based, river-type-specific assessment of ecological integrity[END_REF]. The recent intercalibration exercise conducted in Central-Baltic region of Europe revealed that the pressure criteria used to select reference sites needed further standardization [START_REF] Pardo | The European reference condition concept: A scientific and technical approach to identify minimallyimpacted river ecosystems[END_REF].

It is interesting to note that this difficulty in calibrating definitions is not an isolated case in European policy. Robert Salais, who is interested in the implementation of the Lisbon Strategy in employment issues, pointed to the lack of a common definition of unemployed or employed [START_REF] Salais | La politique des indicateurs. Du taux de chômage au taux d'emploi dans la stratégie européenne pour l'emploi (SEE)[END_REF]. Isabelle Bruno, who studied equal opportunity policies for men and women and programs for financing pensions, also noted that common definitions were very blurred in those policy fields [START_REF] Bruno | Europeanization through its instrumentation: benchmarking, mainstreaming and the open method of co-ordination... Toolbox or Pandora's box?[END_REF].

The ecological roots of the reference condition concept

The WFD appears to have been largely inspired by an old ecosystem paradigm that is based on an a priori vision of nature centered around species [START_REF] Clements | Research methods in ecology[END_REF][START_REF] Elton | Animal ecology and evolution[END_REF][START_REF] Tansley | The use and abuse of vegetational concepts and terms[END_REF]. Under this paradigm, each ecological unit is considered relatively constant in the face of environmental variability and is able to regulate itself, much like an organism (the "balance of nature" concept). Natural ecosystems move through a series of phases to reach a climax state, where they remain until there are major changes in the global environment on a large temporal scale. Ecosystems are predictable, although disturbance cycles are integral to the way they behave (following disturbance, ecosystems return to their previous "optimal" state). [START_REF] Odum | Fundamentals of ecology[END_REF] and [START_REF] Whittaker | Communities and Ecosystems[END_REF] popularized this concept and its associated holistic vision of ecosystems. The concept of reference conditions is grounded in this idea of a stable state. But the ecosystem paradigm described above has been challenged in recent decades on the grounds of i) species dispersal and metapopulation theory [START_REF] Hanski | Metapopulation Ecology[END_REF], and ii) the role of spatial heterogeneity on ecological process and the importance of flux in landscape between ecosystems [START_REF] Pickett | Landscape Ecology: Spatial Heterogeneity in Ecological Systems[END_REF]. Ecosystems are now seen as unstable, open, hierarchical and scaled [START_REF] O'neill | Is It Time To Bury The Ecosystem Concept? (With Full Military Honors, Of Course!)[END_REF]. The most important for our discussion is to call into question the idea of ecosystems as stable and predictable.

Initially, the concept of "resilience" accounted for variability in a system in a steady state by explaining the variability as a response to small perturbations. The resilience concept addressed variability in terms of return time to a stable state [START_REF] Pimm | The complexity and stability of ecosystems[END_REF] and suggested that there was a maximum level of disturbance that could be tolerated without significant alteration of functions [START_REF] Holling | Resilience and stability of ecological systems[END_REF]. More recently, as a response to repeated failed restoration efforts that have highlighted the irreversible nature of many of the changes sustained by natural systems, [START_REF] Scheffer | Catastrophic shifts in ecosystems[END_REF] proposed the concept of alternative stable states. Even in response to a continuous gradient of environmental change (natural or human-induced), ecosystem change occurs dramatically in a non-linear process from a given point. Ecosystems are not able to return to their original state when previous environmental conditions are restored. Multiple different stable states may persist in a single ecosystem. This theory identifies non-linear, and even "chaotic" systems-theory-based pathways of ecosystem change. In particular, river landscapes experience a complex entanglement of long-term and short term fluctuations which make idealistic to consider reverting to any previous stage, pristine or not [START_REF] Dufour | From the myth of a lost paradise to targeted river restoration: forget natural references and focus on human benefits[END_REF]. From a conceptual standpoint, climate change sheds light on the contradiction between the reference conditions concept and the dynamic trajectories of aquatic ecosystems. The consequences will be important for the distribution of many species, especially cold water species. Accessibility to refuge areas during periods of stress (i.e., low flow and thermal peaks) will become a major factor in maintaining these populations [START_REF] Buisson | Contrasted impacts of climate change on stream fish assemblages along an environmental gradient[END_REF][START_REF] Pont | Assessing river biotic condition at the continental scale: a European approach using functional metrics and fish assemblages[END_REF]. Climate change will not only change the ecological status of undisturbed areas, but will also interact with the impacts of human activities on biological communities (e.g., eutrophication and the coupling of thermal regimes and hydrology) and will exacerbate the uncertainties associated with the monitoring and assessment ((European communities, 2009). It is likely that the so-called reference biological communities are evolving and simulation exercises demonstrated the potential impact on the assessment of ecological status [START_REF] Logez | Global warming and potential shift in reference conditions: the case of functional fish based metrics[END_REF].

Another major challenge to the concept of reference conditions stems from the observation that significant environmental modifications by humans have occurred for several millennia. The notion of an undisturbed state no longer has ecological significance. Expanding upon the original concept of an ecosystem, the socio-systems concept [START_REF] Fischer-Kowalski | On the development of concept and methodology of society's metabolism[END_REF] recognizes the inseparability of natural and social aspects of these systems and the central role of humanenvironment interactions. In the academic field of environmental history, and more specifically history of ecology, there is an underlying premise that man and nature have co-evolved since Neolithic times.Human activities are not always perceived as synonymous with destruction [START_REF] Balée | Advances in Historical Ecology[END_REF]. Rather, it is recognized that human activities could also create, through long-term interactions with nature, cultural landscape having an higher value of biodiversity [START_REF] Balée | Advances in Historical Ecology[END_REF][START_REF] Farina | The cultural landscape as a model for the integration of ecology and economics[END_REF].

The distinction between natural and human-altered states is misleading. It implies that one can separate ecosystem characteristics that result directly from human actions from those which are natural characteristics of a dynamic system. Identifying human-induced characteristics is relatively possible at the local level, provided that managers allocate resources to making human impacts publicly visible and measurable with ecological status indicators [START_REF] Bouleau | How ecological indicators construction reveals social changes -the case of lakes and rivers in France[END_REF]. In contrast, for rivers that continuously experience flooding and chemical inputs from upstream, the millennial transformation of watersheds by humans (including changes to forest cover) make it impossible to define an ecosystem state that has not been impacted. A recent case study of the Drôme River, southeast France, shows the temporal succession of interactions between land drainage and river basin dynamics [START_REF] Pont | Conceptual framework and interdisciplinary approach for the sustainable management of gravel-bed rivers: the case of the Drôme River basin (S.E. France)[END_REF]. [START_REF] Gunderson | Panarchy: understanding transformations in human and natural systems[END_REF] proposed the concept of panarchy to account for the complex natural and human dynamics of watersheds. In a related discussion, [START_REF] Lévêque | L'anthroposystème : entité structurelle et fonctionnelle des interactions sociétés -milieux[END_REF] suggest the term anthroposystem. The dynamics of ecological systems can no longer be explained using bio-physico-chemical rules alone, and the distinction between natural and anthropogenic forces is artificial.

In a critical analysis of the WFD, [START_REF] Steyaert | The European Water Framework Directive: How Ecological Assumptions Frame Technical and Social Change[END_REF] conclude that the ecologists who participated in the writing of the text were overwhelmingly influenced by the concept of ecosystem stability and focused on systematically considering human activities as disturbance

Author-produced version of the article produced in Environmental Science & Policy, 2015, 47, 32-41 The original publication is available at http://www.sciencedirect.com/science/article/pii/S1462901114002044 doi:10.1016/j.envsci.2014.10.012

factors. Recently, Dufour and Piégay [START_REF] Dufour | From the myth of a lost paradise to targeted river restoration: forget natural references and focus on human benefits[END_REF] proposed to replace the restoration strategy aimed at achieving a defined, "natural," ideal ecological state (referencebased strategy, stemming from Leitbild (Kern, 1992a)) with a strategy that defines objectives based on the services provided by ecosystems.

Towards biological indicators based on functional criteria

In parallel to the drafting of the WFD, a conference, which took place in Vienna in 1998, focused on assessing the ecological integrity8 of rivers [START_REF] Jungwirth | Assessing the Ecological Integrity of Running Waters[END_REF]and developing WFD-compliant biological assessment methods [START_REF] Jungwirth | Assessing the Ecological Integrity of Running Waters[END_REF]. Most of the biological indicators presented were based on a static description of aquatic communities (micro and macro algae, invertebrates, fish) and by grouping water bodies into discrete categories (river zonation system). As the condition concept, these biomonitoring tools rely mainly to the long obsolete concept of climax (see before) and do not consider the modern idea of species turnover and continua of community structure along environmental gradient [START_REF] Friberg | Biomonitoring of human impacts in freshwater ecosystems: the good, the bad, and the ugly[END_REF].

Aquatic ecologists have expressed many criticisms about the lack of functional criteria used in such biological indicators [START_REF] Friberg | Biomonitoring of human impacts in freshwater ecosystems: the good, the bad, and the ugly[END_REF], both for conceptual reasons and because of the current emphasis on expert opinion. However, in spite of awareness about the limitations of the conceptual approach of the WFD, many European scientists paint a more positive picture of the first ten years of implementation of the directive [START_REF] Hering | The European Water Framework Directive at the age of 10: A critical review of the achievements with recommendations for the future[END_REF]. One main reason is that the implementation of the WFD has led to the establishment of networks of biological monitoring that use more standardized sampling techniques. Although the requirements outlined in the directive are based on a limited number of biological (and chemical) indicators, this has the advantage of focusing members' efforts on specific common protocols, thereby helping to improve the methods. The need to standardize methods across European countries has led to unprecedented development of international discussion and collaborative research projects, including more than 1100 publications related to the WFD in 10 years (Web of Science, July 2009). Because the WFD approach was very pragmatic, it was possible to apply it in most countries, despite its shortcomings. The implementation of the WFD has greatly improved the degree of comparability of the ecological quality of rivers across Europe.

Moreover, it should also be noted that most of recent WFD-compatible bioindicators are no more based on floro-faunal lists, but on functional criteria determined by ecological and/or biological characteristics. This is particularly the case in France for fish [START_REF] Oberdorff | Development and validation of a fishbased index for the assessment of 'river health' in France[END_REF] and invertebrates [START_REF] Mondy | A new macroinvertebrate-based multimetric index (I2M2) to evaluate ecological quality of French wadeable streams fulfilling the WFD demands: A taxonomical and trait approach[END_REF]. For example, a high level of omnivory is indicative of degradation, while specialization in breeding habitats indicates a low degree of physical alteration of the environment. The first advantage of these functional-type's indicator is that, by removing the taxonomic specificity, they can be used on a much wider geographic scale (i.e. the European scale) which solve the problem of intercalibrating the different national methods. The development of a paneuropean fish index [START_REF] Pont | Assessing river biotic condition at the continental scale: a European approach using functional metrics and fish assemblages[END_REF] demonstrated its feasibility even if the counterpart is a relative lack of sensitivity to some specific local situations. The second advantage is that the relation between stressor and response can be predicted based on clear mechanisms of cause-effect. Nevertheless, in the case of these functional-type bioindicators, the functions are only considered indirectly via the definition of functional specific guilds and bioindicators purely based on functional descriptors of ecosystem remain to be developed in the future.

Another major improvement is to not use any more typologies and pre-defined community types but to consider more realistic gradient-based measure of community change. The RIVPACS method was the first to attempt to predict, using site-specific variables, the expected macroinvertebrate community in the absence of disturbance and to compare with the observed one [START_REF] Wright | RIVPACS: A technique for evaluating the biological quality of rivers in the UK[END_REF]. Using both ecological-biological traits and modelling approach, [START_REF] Oberdorff | Development and validation of a fishbased index for the assessment of 'river health' in France[END_REF] and [START_REF] Pont | Assessing river biotic condition at the continental scale: a European approach using functional metrics and fish assemblages[END_REF] proposed multimetric predictive indexes to model the functional characteristic of fish assemblages in the absence of disturbance and to assess the ecological status of rivers.

In a recent work, [START_REF] Marzin | Uncertainty associated with river health assessment in a varying environment: the case of a predictive fish-based index in France[END_REF] developed a new predictive multimetric index considering the climatic conditions (air temperature and rainfall) prevailing during the ten years before the assessment period and associating an uncertainty to the ecological assessment of each site. In complement to establish long-term monitoring network, such tool could allow better considering the changing nature of the environment.

Nevertheless, the capacity of biological indicators to identify the precise causes of degradation remains questionable. The authors of the WFD assumed a direct relationship between a pressure and a set of indicators, which has been shown to be false for several reasons. They overestimated the capacity of biotic indicators to respond to different pressures in specific ways. Except for few cases, such as the response of phytoplankton to increased phosphorus levels, indicators generally respond to the different types of pressures [START_REF] Marzin | Ecological assessment of running waters: do macrophytes, macroinvertebrates, diatoms and fish show similar responses to human pressures?[END_REF] like water quality degradation and hydromorphological alteration. The results of the European intercalibration process showed that there were significant relationships between the sensitive bio-indicators and the main types of pressure, but these relationships were not as strong as national experts had previously suggested [START_REF] Pont | Water Framework Directive. Intercalibration Phase 2. River Fish European Intercalibration Group[END_REF]. This result is also due partly to the large uncertainties associated with the assessments [START_REF] Clarke | Errors and uncertainty in bioassessment methods -major results and conclusions from the STAR project and their application using STARBUGS[END_REF][START_REF] Marzin | Uncertainty associated with river health assessment in a varying environment: the case of a predictive fish-based index in France[END_REF]. And finally, most of rivers are affected by multiple pressures involving both the degradation of water quality and changes in stream morphology and hydrology [START_REF] Ormerod | Multiple Stressors in Freshwater Ecosystems[END_REF].

Summary and conclusions

The ambition to monitor the ecological conditions of all surface waters, rather than simply considering the physico-chemical qualities of some waterbodies, represents real progress from an environmental point of view. Nonetheless, the approach used by the WFD poses serious problems. Some of the problems are relatively new, and some have not yet been overcome, even fourteen years after the publication and implementation of the WFD.

The WFD is an ambiguous piece of law which includes legally-binding provisions in line with the classic community method and a much more flexible framework for comparing and assessing policy options based on economic criteria in line with new form of environmental governance. Both policy models require defining quantitative indicators. Yet the drive for establishing reference conditions relates to the legally-binding character of the WFD objectives. From the ecological point of view, the idea of stable reference conditions refers mainly to the concept of ecosystems reaching a "climax" state. It contradicts all the modern concepts in ecology, underestimates the continuously evolving nature of our environment and does not consider the long term interactions between man and nature. It should be noted, however, that the relative stability of an ecosystem over a discrete time period is often a useful reference for detecting and measuring a local change.

Conceptual debates about reference conditions do not prevent its implementation. Approaches to "identifying" reference conditions are usually pragmatic. Reference conditions are typically identified by examining relatively undisturbed sites based on a review of human pressures, without actually seeking to define a common theoretical vision. This approach has been applied in a variety of situations by adjusting the historical reference period, the frequency of measurement, and the sampling locations to characterize a particular ecological impact that posed a social problem. In practice, the new governance component of the WFD allowed experts to define an evaluation framework, identify impacted sites, and prioritize restoration actions to address those sites. The intercalibration process remains obscure for most lay people, but led most Member States to a pragmatic approach. It consisted, at a minimum, to set common reference conditions based on networks of undisturbed sites. In addition, the new generation of bio-indicators based on "functional" characteristics of biological communities is better able to provide a comparative analysis of water bodies at the European scale.

With regards to climate change and the assessment of ecological status, additional macroenvironmental variability resulting from climate change in the future will further challenge the use of the concept of reference conditions. However, the limited duration of the WFD time frame (2000-2027) could allow for revising local reference conditions to take into account new information about regional environmental conditions (monitoring networks, modeled reference conditions) 9 . In their management plans, Member States should at least assess the implications of climate change in the context of other anthropogenic impacts, consider climate change in their monitoring programs, and develop plans based on resilience strategies. The plans should favor restoration projects that implement "no regrets" measures, i.e., measures that are sufficiently reliable and robust to remain viable in a changing global context and that are not likely to counteract measures taken by other parties to mitigate the impacts of climate change (e.g. reestablishment of connectivity within river network in order to facilitate species migration, riparian forest development).

But the reference conditions issue will resurface at the next stage of implementation of the WFD as the primary objective of the management plans moves from assessment to restoration (2015-2021 and 2021-2027). One of the guiding principles for restoration actions is that the re-establishment of historical abiotic conditions and their associated disturbance regimes will result in the recovery of biological communities prevailing before degradation. This explicitly invokes the principle of community succession (and successional-based management efforts). In reality, however, the results of restoration projects are often not what we expect, and the system does not return to its previous state [START_REF] Suding | Alternative states and positive feedbacks in restoration ecology[END_REF]. This result can be explained by the lack of existing systems that can be used to define reference conditions; changes in conditions at large scales (landscape, watershed, and climate); an irreversible modification of certain environmental parameters; changes in connectivity at the basin scale; changes in the migration of species; and new biotic interactions and the alteration of biotic-abiotic feedbacks, which causes lasting changes in bio-geochemical conditions [START_REF] Henri | Restoration ecology of riverine wetlands: I. A scientific base[END_REF][START_REF] Nilsson | Restoring riverine landscapes: the challenge of identifying priorities, reference states, and techniques[END_REF][START_REF] Suding | Alternative states and positive feedbacks in restoration ecology[END_REF].

It is worth noting that the use of reference condition concept in WFD is more linked to stability and reversibility than in the thoughts of forest ecologist in North America [START_REF] Fulé | Determining reference conditions for ecosystem management of southwestern ponderosa pine forests[END_REF]. Reversibility concept remains acceptable when considering local and short term perturbations (e.g. recovery of a river from a local source of organic pollution), but is questionable when i) numerous anthropogenic pressures are acting on the whole catchment and ii) long term land use evolutions within a catchment have altered the large scale processes controlling the fluvial dynamic (e.g. trying to revert a river stretch to a previous braided state when the coarse sediment bed load is nowadays limited due to afforestation).

One possible future strategy for restoration could combine considerations for ecosystem health, ecosystem services, and productivity in a sustainable manner for social benefit [START_REF] Aronson | Ecological restoration: a new frontier for nature conservation and economics[END_REF]. Identifying society's needs would require a more important participation of managers, users and stakeholders at different levels [START_REF] Dufour | From the myth of a lost paradise to targeted river restoration: forget natural references and focus on human benefits[END_REF]. Historical trajectories of systems remain an important point when targeting a better knowledge of the main processes to be restored. Due to the complex dynamic of ecosystems, it is necessary to consider ecological, social and economic values and the uncertainties about restoration objectives [START_REF] Hughes | Restoring riparian ecosystems: The challenge of accommodating variability and designing restoration trajectories[END_REF], Adaptive management, a problem-solving environmental management approach [START_REF] Aronson | Ecological restoration: a new frontier for nature conservation and economics[END_REF], appears as a promising way to handle restoration of European water bodies in the context of the WFD. In all cases, historical trajectories of systems help understanding the main processes to be restored. This knowledge is crucial when confronting society's demands and potential functioning. An interesting direction for future research would be to see how different social groups implement the WFD and its tools (monitoring networks, expertise, concepts, planning documents, and decision steps) for guiding future decisions about the environment in a changing context.

Figure 1 :

 1 Figure 1: Diagram of the mitigation model of the WFD

  Author-produced version of the article produced in EnvironmentalScience & Policy, 2015, 47, 32-41 The original publication is available at http://www.sciencedirect.com/science/article/pii/S1462901114002044 doi:10.1016/j.envsci.2014.10.012

The Water Framework Directive (2000/60/EC) was adopted on October

23, 2000 by the European Parliament and the Council. It established "a framework for community action in the field of water" (L 327, 22/12/2000, p. 0001 -0073).2 This paper is an extended and adapted version from a paper published in French: Bouleau, G.,Pont, D., 2014. Les conditions de référence de la directive cadre européenne sur l'eau face à la dynamique des hydrosystèmes et des usages. Natures Sciences Sociétés 22 (1), 3-14.

The word 'status' is used in the WFD to refer to the environmental conditions of a water body, and the word 'measures' refers to actions by States to restore the desired environmental conditions, i.e. the environmental state and the responses in DPSIR language.

The terms 'disturbed,' 'undisturbed' or 'disturbances' are used a total of 107 times in Annex V of the WFD, without being clearly defined.Author-produced version of the article produced in EnvironmentalScience & Policy, 2015, 47, 32-41 The original publication is available at http://www.sciencedirect.com/science/article/pii/S1462901114002044 doi:10.1016/j.envsci.2014.10.012

The concept of biotic integrity is of American origin and was popularized in Europe in the late 1980's in Germany and Austria. It is based on a vision or Leitbild for a specific river reach, primarily defined by reference to the florofaunal structures pre-dating industrialization.(Kern, K., 1992b. Rehabilitation of streams in South-western Germany, In: Boon, P., Calow, P., Petts, G. (Eds.), River Conservation and Management. JohnWiley & Sons, Chichester,

Annex V (1.3.1) states that Member States must establish monitoring programs to collect data that will be used to evaluate changes in natural conditions over the long term.Author-produced version of the article produced in EnvironmentalScience & Policy, 2015, 47, 32-41 The original publication is available at http://www.sciencedirect.com/science/article/pii/S1462901114002044 doi:10.1016/j.envsci.2014.10.012

Author-produced version of the article produced in EnvironmentalScience & Policy, 2015, 47, 32-41 The original publication is available at http://www.sciencedirect.com/science/article/pii/S1462901114002044 doi:10.1016/j.envsci.2014.10.012

Acknowledgments

This research was conducted in part with the support of the French National Research Agency (ANR), within the MAKARA project (Societal responses to surface water « quality » Changes: France, 19th-20th centuries) of the program "Sociétés & changements environnementaux 2012" (contract ANR-12-SENV-009). It has been also supported by IRSTEA within the project CHIFFRE (APR Indeco 2012) and by the European REFORM project (European Program FP7-ENV-2011, contract No. 282656, "REstoring rivers FOR effective catchment Management").

Author-produced version of the article produced in Environmental Science & Policy, 2015, 47, 32-