Chuck Liang
email: chuck.c.liang@hofstra.edu

Dale Miller
email: dale.miller@inria.fr

Unifying Classical and Intuitionistic Logics for Computational Control

We show that control operators and other extensions of the Curry-Howard isomorphism can be achieved without collapsing all of intuitionistic logic into classical logic. For this purpose we introduce a unified propositional logic using polarized formulas. We define a Kripke semantics for this logic. Our proof system extends an intuitionistic system that already allows multiple conclusions. This arrangement reveals a greater range of computational possibilities, including a form of dynamic scoping. We demonstrate the utility of this logic by showing how it can improve the formulation of exception handling in programming languages, including the ability to distinguish between different kinds of exceptions and constraining when an exception can be thrown, thus providing more refined control over computation compared to classical logic. We also describe some significant fragments of this logic and discuss its extension to second-order logic.

I. INTRODUCTION

Since it became clear that the Curry-Howard isomorphism can be extended to classical logic [START_REF] Griffin | The formulae-as-types notion of control[END_REF], several constructive classical systems have been formulated, including λµcalculus [START_REF] Parigot | λµ-calculus: An algorithmic interpretation of classical natural deduction[END_REF] and its variants. However, the gap between intuitionistic logic and classical logic is a large one. Collapsing all of intuitionistic logic into classical logic in order to obtain greater computational ability is not necessarily the best approach. For example, we may wish to obtain a computationally meaningful proof for a formula such as (A → B)∨A. In classical logic, there is no avoiding the fact that this formula is an instance of the excluded middle, and can be given a trivial proof. Such a situation can occur either with an explicit ∨, or implicitly when there are multiple conclusions in proofs. A λµ-term may be obtained, but it does not compute anything meaningful. We wish to have a logical way to constrain the interpretation of such a formula, so that B must be computed, in the sense that it must be the result of introductions and eliminations and not just the result of weakening, at least not until certain conditions are met.

Ideas from classical λµ-calculus have been used to formulate, for example, exception handling in programming languages. In particular, catch is represented by contraction, which saves a copy of the current continuation, and throw/raise is represented by weakening, which discards the current continuation and jumps back to the saved one (see [START_REF] Crolard | A confluent lambda-calculus with a catch/throw mechanism[END_REF]). However, there remains a gap between this form of exception handling and those of practical programming languages such as Java. We list three such gaps below.

• The type of the exception is not identified. In Java, for example, one specifies exceptions such as in catch IOException, catch ArithmeticException, etc. • Control over when an exception can be thrown is lacking. One must declare int p(..) throws IOException in Java if it is possible for p to throw this kind of exception. • Exception handling in languages such as Java and ML are dynamically scoped, whereas the λµ-calculus has the same variable capturing restrictions as λ-calculus.

We do not claim to have a system as rich as Java or ML but will offer at least some progress in each of these areas.

We unify classical and intuitionistic propositional logics into a new logic we call Polarized Control Logic (PCL). The polarity of a formula determines the availability of certain structural rules. Depending on the polarity of A and B, (A → B)∨A may be interpreted entirely classically, entirely intuitionistically, or somewhere in between. Such a use of polarization is not new, and much of what we have just described may sound like LC [START_REF] Girard | A new constructive logic: classical logic[END_REF] and related work on focusing proofs [START_REF] Andreoli | Logic programming with focusing proofs in linear logic[END_REF]. In fact our system will extend the polarization scheme of LC. It is based on the preservation of intuitionistic implication, which LC does not contain. PCL will contain not only intuitionistic and classical logics but also other meaningful fragments, including an intermediate logic that admits the law of excluded middle A ∨ ¬A but not involutive negation ¬¬A → A.

We will define a form of Kripke models to interpret polarized formulas and cement PCL's status as a new logic with a sequent calculus and proofs of cut elimination, soundness, and completeness. The main proof system for PCL will be a natural deduction system with proof terms. Existing constructive classical systems typically extend Gentzenstyle, single-conclusion intuitionistic systems with multiple conclusions. In contrast, the proof system for PCL will extend an intuitionistic system that already has multiple conclusions. This approach will reveal a greater range of computational capabilities, including a dynamically scoped version of the µ binder, the operator of λµ-calculus that enables a computationally meaningful form of contraction.

II. POLARIZATION AND SEMANTICS

We focus on propositional logic in this presentation. Formulas of PCL are build from atomic formulas, the connectives ∧, ∨ and →, and the constants 1, 0 and ⊥. The two constants for false define two forms of negation. We use the abbreviations ∼ A = A → 0, and ¬A = A → ⊥.

A. Polarization

Atomic formulas are polarized red or green. Polarization is extended to all formulas as follows:

• ⊥ is green; 0 and 1 are red.

• A ∧ B is green if A and B are green, otherwise, it is red.

• A ∨ B is green if A or B is green, otherwise, it is red. • A → B is green if B is green, otherwise, it is red.
We use the symbol R exclusively to represent red formulas and E to represent green formulas, with frequent reminders of this convention.

The polarization of ∧ and ∨ mirrors that of the LC system [START_REF] Girard | A new constructive logic: classical logic[END_REF]. However, LC does not contain implication 1 . In particular, the natural correspondence between polarization and focusing (focalization) no longer holds with implication. For these reasons we have named our polarities red and green instead of "positive" and "negative." We also do not insist on an a priori relationship of duality between the polarities. For example, ¬E is green even if E is green.

Conceptually, red means intuitionistic and green means classical and we formalize this correspondence below.

B. Kripke Models

We consider only Kripke frames that are (finitely) rooted: it is known that intuitionistic propositional models can also be assumed to have this restriction. Such frames are the basis of models of the form W, r, , |= , where is a transitive, reflexive ordering of the set of possible worlds W and r ∈ W is the unique root such that r u for all u ∈ W. The binary relation |= monotonically maps elements of W to sets of atomic formulas. We add another stipulation:

If q is a world properly above r (r ≺ q), then q |= e holds for all green atoms e. The |= relation is extended to all formulas as follows. Here we use u and v to represent arbitrary worlds.

• r |= ⊥ • q |= ⊥ for all q ≻ r • u |= 1; u |= 0 • u |= A ∧ B iff u |= A and u |= B 1 If A ⊥ ∨ B is
used for implication in LC (where A ⊥ is the De Morgan dual of A), then it is positive only when A is negative and B is positive. In PCL, only the head of the implication determines the polarity. This treatment of intuitionistic implication is also different from LU and from linear logic. PCL is not a fragment of these systems.

• u |= A ∨ B iff u |= A or u |= B • u |= A → B iff for all v u, v |= A implies v |= B.
Except for green atoms and ⊥, the |= relation is the same as in Kripke models for intuitionistic logic. The usual monotonicity property holds: if u v then u |= A implies v |= A for all formulas A.

We shall refer to this version of Kripke models as rmodels. A formula is considered valid in an r-model if it is valid in all its worlds. A formula is valid in PCL if it is valid in all r-models.

The semantic characterization of green formulas is consistent with that of ⊥ and green atoms: q |= E for all green E and worlds q ≻ r. The root r is the only classically consistent world. Since all worlds above r force ¬A, we have r |= A if and only if r |= ¬A, and thus A ∨ ¬A is valid in all worlds.

If a formula A is purely red (all subformulas are red), then A is valid if and only if it is intuitionistically valid. The root world balances the classical inconsistency of all others above. All worlds are intuitionistically consistent. This means that a red subformula of a green formula will retain its intuitionistic meaning, and vice versa. The r-models are a restricted class of the models that we formulated in [START_REF] Liang | Kripke semantics and proof systems for combining intuitionistic logic and classical logic[END_REF], but PCL retains intuitionistic implication in a stronger way.

The following properties hold of this semantics.

• ⊥ → E is valid for green E, 0 → A is valid for all A.

• A ∨ ¬A is valid, but not ∼A ∨ A nor ∼E ∨ E.

• ¬¬A → A is NOT valid.

• ¬¬E → E is valid for green E.

• ∼ ¬A → A is valid for all A.

• If ¬¬A is valid then A is also valid.

• ¬(A ∧ B) → (¬A ∨ ¬B)

• ((P → Q) → P) → P is valid if Q is green. These properties show, respectively, that there are two levels of consistency. The excluded middle is valid with ¬, but not with ∼. The following countermodel disproves ¬¬A → A: let there be a single world q ≻ r. For some red atom a, define r |= a and q |= a. Then there is a world q above r such that q |= ¬¬a but q |= a. However, two forms of negation means four of double negation, and one of these gives us the C control operator. The admissible rule stated does not contradict the non-involution of ¬. The De Morgan laws are valid with ¬. The version of Peirce's formula exemplifies how intuitionistic logic need not be crushed to obtain new computational ability (in this case call/cc). If P is red, then the innermost → is a classical implication while the other two stay intuitionistic.

The reader may have noticed, from the properties described above, that red atoms have the characteristics of universally quantified second order variables and that the green atoms are existentially quantified. This is indeed true. Although our main focus is on propositional logic, we discuss this further in Section VII.

The usual route of extending the Curry-Howard isomorphism is to start with a Gentzen-style, single-conclusion intuitionistic system (LJ/NJ), allow multiple conclusions, then add a stoup, i.e., some distinguished formula that represents the current formula being deduced. Our approach, which is used because one of our structural rules is context sensitive, starts with the multiple-conclusioned version of intuitionistic sequent calculus. This system is found in various sources and is a mirror image of the Beth-Fitting intuitionistic tableaux (and thus also simplifies the proof of semantic completeness). Two inference rules in this system stand out in contrast to Gentzen's LJ, namely

A, Γ ⊢ B Γ ⊢ A → B, Θ and Γ ⊢ A, B, Θ Γ ⊢ A ∨ B, Θ .
Contraction and weakening are also allowed on the righthand side. However, it is easy to see why (A → ⊥)∨A is still not provable with the scoping restriction on → introduction. We can form a natural deduction system from this sequent calculus as follows.

1) Introduce a stoup on the right-hand side but also allow formulas to freely enter and leave the stoup, so that the new system is obviously equivalent to the stoupless one. In particular, admissible cuts are preserved. 2) Apply cut-elimination to form the elimination rules.

The only extra difficulty, compared with the LJ-NJ translation, is in the → introduction and ∨ elimination cases. Fortunately, the invertibility of the multiplicative ∨-introduction rules (which can be proved by cutelimination) can be used to combine the right-hand side into a single formula. Alternatively, we can just show that the elimination rules are semantically sound. We now extend this system with an extra context of formulas on the right-hand side. Sequents of the proof system NPC for PCL are of the form Γ ⊢ S; Θ; [∆], where the stoup S consists of zero or one formula. An empty stoup means 0, which is intuitionistic false. The variables Γ, Θ and ∆ range over sets of formulas and the expression A, Γ, where Γ is any set of formulas, represents {A} ∪ Γ and does not preclude the possibility that A ∈ Γ. Intuitively, Θ is the intuitionistic multiple-conclusion context while [∆] represents the "locked" context which is only accessible once a green formula appears in Θ.

The semantic interpretation of the sequent Γ ⊢ S; Θ; [∆] is as for the formula (¬ ∆ ∧ Γ) → (S ∨ Θ). Here, Γ is the ∧conjunction of formulas in Γ, with an empty Γ representing 1, while Θ (and ∆) is the ∨-disjunction of formulas in Θ, with an empty Θ, and an empty stoup, representing 0.

Except for the stoup formula, all other formulas in a sequent are indexed by variables. We assume that variables indexing formulas in Γ (λ variables) are distinguishable from those in Θ and ∆ (µ variables) and that the usual variable conventions are applied. NPC is found in Figure 1. We prefer to associate a proof term with an entire subproof, and not just the stoup formula.

The following admissible rule indicates that contraction and weakening are available in Γ, Θ and [∆]:

s : C u , C v , Γ ⊢ F; A x , A y , Θ; [B d , B e , ∆] s[u/v, x/y, d/e] : C u , ΓΓ ′ ⊢ F; A x , ΘΘ ′ ; [B d , ∆∆ ′ ]
This is the uninteresting form of contraction and weakening and we usually use them implicitly. With these structural rules available, we are free to choose between multiplicative and additive treatments of contexts. We prefer multiplicative for its convenience when writing proofs.

A formula

A is provable if ⊢ A; ; [ ] is provable.
The proof terms for Open and Esc are those found in λµ-calculus. However, here they remain intuitionistic. The µ-binder is still important since it allows for structural reduction (rule (µd.s)t -→ µd.s{[d]wt/d[w]} remains valid), but with µ alone the reduction would be shallow since it cannot survive past a λ binder. Formulas can be locked in the boxed context [∆] prior to an → introduction (regarding proofs bottom-up), which can be unlocked only if a green formula E is found outside of the box. In NPC the separation between intuitionistic and non-intuitionistic proofs is indicated by the presence of ?, without which ! would also be useless (with apologies to linear logic: there is no direct connection). The ! operators replaces µ as the most meaningful operator since Lock enables contraction (B x may persist in Θ) between two distinct contexts.

Lock and U nlock can be used to prove ¬A ∨ A: since ⊥ is green, it can unlock the copy of A saved inside [ ]. A proof of Peirce's formula ((P → Q) → P ) → P , where Q is green and P is red, is found in Figure 2. Some steps moving formulas in and out of the stoup were combined.

Choosing a multiple-conclusion intuitionistic proof system as starting point does imply some non-determinism: the formula in the stoup is not always computed by introductions and eliminations. But this form of non-determinism does not survive past a β-redex (it also does not survive a ∨elimination), so it is limited in form. It is still possible to derive typed λ-terms from purely intuitionistic proofs in NPC. In classical λµ calculus, the µ binder can be considered as a constant of type ¬¬A → A, which has no equivalent λ-term. However, when seen in an intuitionistic context, µ has type (0 ∨ A) → A (and the contraction form of µ would be

A ∨ A → A). It is ! that is non-intuitionistic.
Recall that formulas B inside [ ] has the meaning of ¬B on the left-hand side. This means !, as a constant, has type

(¬B → B) → B (assuming B x ∈ Θ), which is a version of Peirce's formula.
We can also translate classical λµ-terms into "λµ!-terms." Each instance of a classical µd.s translates to µd.!d.s, and [d]s translates to ?d.[d]s. Classical λµ-terms thus translated are typable in NPC because we can choose green formulas

s : Γ ⊢; A x , Θ; [∆] µx.s : Γ ⊢ A; Θ; [∆] Open s : Γ ⊢ A; Θ; [∆] [d]s : Γ ⊢; A d , Θ; [∆] Esc s : Γ ⊢ F; Θ; [B x , ∆] !x.s : Γ ⊢ F; Θ, B x ; [∆] Lock s : Γ ⊢ E; Θ, B x ; [∆] ?x.s : Γ ⊢ E; Θ; [B x , ∆] U nlock s : A x , Γ ⊢ B; ; [∆] λx.s : Γ ⊢ A → B; Θ; [∆] → I s : Γ ⊢ A → B; Θ; [∆] t : Γ ′ ⊢ A; Θ ′ ; [∆ ′ ] (s t) : ΓΓ ′ ⊢ B; ΘΘ ′ ; [∆∆ ′ ] → E u : Γ ⊢ A; Θ; [∆] v : Γ ′ ⊢ B; Θ ′ ; [∆ ′ ] (u, v) : ΓΓ ′ ⊢ A ∧ B; ΘΘ ′ ; [∆∆ ′ ] ∧I s : Γ ⊢ A ∧ B; Θ; [∆] π ℓ (s) : Γ ⊢ A; Θ; [∆] ∧E 1 s : Γ ⊢ A ∧ B; Θ; [∆] π r (s) : Γ ⊢ B; Θ; [∆] ∧E 2 s : Γ ⊢ A; B d , Θ; [∆] ω ℓ d.s : Γ ⊢ A ∨ B; Θ; [∆] ∨I 1 s : Γ ⊢ B; A d , Θ; [∆] ω r d.s : Γ ⊢ A ∨ B; Θ; [∆] ∨I 2 s : Γ 1 ⊢ A ∨ B; Θ; [∆ 1 ] u : A x , Γ 2 ⊢ C; ; [∆ 2 ] v : B y , Γ 3 ⊢ C; ; [∆ 3 ] (λx.u, λy.v)s : Γ 1 Γ 2 Γ 3 ⊢ C; Θ; [∆ 1 ∆ 2 ∆ 3 ] ∨E x : A x , Γ ⊢ A; Θ; [∆] Id s : Γ ⊢ 0; Θ; [∆] A(s) : Γ ⊢ F; Θ; [∆] 0 E s : Γ ⊢ ⊥; Θ; [∆] B(s) : Γ ⊢ E; Θ; [∆] ⊥E exit : Γ ⊢ 1; Θ; [∆] 1I Figure 1.
The Natural Deduction System NPC; E in U nlock and ⊥E must be green

x : The ! operator is not a binder in the sense of λ and µ: x remains free in !x.s (and in ?x.s). However, !x.s does represent the start of a kind of scope, represented by s, in which x can be considered to have been pushed on to an alternate, global stack. Since x remains free, we would obviously be able to emulate a form of capturing substitution with respect to !. In particular, we may have !x.λy.s (typed by A → B in the stoup), and thus a valid reduction rule for ! is: (!x.s) t -→ !x.(s t). Such a rule will "capture" free occurrences of x in t inside the scope of !. This is clearly the behavior of dynamic scoping. Nested occurrences of !x may not seem necessary when building a cut-free proof, but they may certainly appear in proofs with cuts (β redexes), which represent programs.

((P → Q) → P ) x ⊢ (P → Q) → P ; ; [ ] Id y : ((P → Q) → P ) x ,
To be fair, it is also possible to give such an interpretation to ?x.s, and even to [d]s. At least the following special cases of µ also do not need to bind their variables:

s : Γ ⊢; A d , Θ; [∆] µ ′ d.s : Γ ⊢ A; A d , Θ; [∆] s : Γ ⊢; A d , Θ; [A d , ∆] µ ′′ d.s : Γ ⊢ A; Θ; [A d , ∆]
The µ ′ operator is not needed in classical λµ-calculus because it can be replaced by weakening, but it is a possible interpretation of µ, which also leads to some dynamic binding behavior. However, µ ′ cannot implement contraction, and therefore does not have the computational power of !. In contrast, since B x ∈ Θ is possible in the Lock rule, ! can be interpreted as a dynamic binder and implements contraction. It is also not just the kind of contraction that renames variables. This comparison shows that the dynamic behavior of ! is not just the result of a fortuitous interpretation. The multiple-conclusion intuitionistic context, when paired with the [ ] context, thus revealed a new computational capability.

Since µ ′ and µ ′′ can extend the effectiveness of ! as a dynamic binder, we shall admit them as well.

A. An Abstract Machine

We do not give a complete set of reduction/rewrite rules for NPC proof terms because an effective computational interpretation of these terms requires a specific evaluation strategy. In the original λµ calculus, certain valid reductions were also excluded to preserve confluence. The problem is exacerbated by the non-binding behavior of !: a specific reduction strategy is required for determinism and for type soundness (there are situations where at most one of several possible reductions may take place). We define such a strategy in the form of an abstract machine. This machine is not the only way to evaluate NPC terms but it demonstrates their computational effectiveness.

Krivine's machine for λ-terms, which computes weak head normal forms, was extended to λµ by adding an additional environment for saved continuations [START_REF] De Groote | An environment machine for the lambdamu calculus[END_REF], [START_REF] Streicher | Classical logic, continuation semantics and abstract machines[END_REF]. We also require a global environment to realize the dynamic binding behavior of !. We use nil for the empty list, :: for Cons, and assume that CE(x), LE(x) and GE(x) return the first (from left to right) closure or stack bound to x in a closure or stack environment. The transitions of the machine are found in Figure 3. Only the implicational fragment is shown.

The highlighted rules represent divergence from classical λµ. The machine interprets µ as the non-binding µ ′′ when possible, which means that all nested !x will behave dynamically. Only the outermost µx will bind statically.

B. Multiplicative Disjunction

It is quite natural to represent a multiplicative ∨introduction, in the presence of a stoup, using binders: here, ω ℓ and ω r . Additive disjunction is subsumed in this representation by ω ℓ/r d.s where d is not free is s. In such a case ω ℓ/r naturally degrade to the usual injection operators. But non-vacuous multiplicative disjunction has the potential for greater computational content. In the ∨-elimination rule, both implicit λ-terms are needed in the reduction. The principal reduction rules associated with ∨-elimination are

(u, v) (ω ℓ d.t) -→ µd.[d](u t{[d](v w)/[d]w}) (u, v) (ω r d.t) -→ µd.[d](v t{[d](u w)/[d]w})
Both u and v are involved in the reduction. In the terminology of λµ-calculus, one is logical while the other one is structural, and is applied to subproofs where the alternate disjunct enters the stoup. Since both u and v are required, an extra copy of C will be found in the conclusion, and thus a contraction, represented by µd.[d] . . . is required at the end.

The abstract machine can be generalized to accommodate ∨-elimination with stack environment entries of the form (d, (C, S)) where C is an extra closure, which is placed in front of the closure for t in the rule for [d]t.

Our ω ℓ/r -binders are similar to the ones of [START_REF] Ritter | Proof-terms for classical and intuitionistic resolution[END_REF]. While their ∨-introduction rule is also multiplicative, their ∨-elimination is entirely different from ours.

IV. EXTENDING NPC FOR EXCEPTION HANDLING

We choose exception handling as the main example of the enriched computations that PCL can formulate because it is a subject that has been studied in the literature on λµ calculus and related systems. The use of multiple-conclusion proofs to represent exception handling was formulated in [START_REF] Nakano | A constructive formalization of the catch and throw mechanism[END_REF], and further studied in [START_REF] Crolard | A confluent lambda-calculus with a catch/throw mechanism[END_REF], [START_REF] Herbelin | An intuitionistic logic that proves Markov's principle[END_REF], where µd.[d]s is interpreted as catch, and µz.[d]w where z is free in w is considered throw (or raise). Our goal here is not to resolve every issue associated with exception handling but to demonstrate the additional expressiveness that PCL can contribute to formulating this kind of computation.

In λµ calculus, µ has the same variable capturing constraints as λ, which means that it implements statically scoped exception handling. However, exceptions are handled dynamically in practical programming languages. The ! operator represents contraction and binds dynamically. However, it does not always save the current continuation. We can designate the special instance of Lock that should represent catch as follows

s : Γ ⊢ A; Θ; [A d , ∆] !d.s : Γ ⊢ A; Θ, A d ; [∆] catch
Even when not in the restricted form above, ! can still serve as a kind of exception handler if one is willing to stretch the meaning of "current continuation." The catch must take place in the context of an outer µ binder, but it need not be a trivial context. When the context is trivial, i.e., in the form µd.

[d]!d.s, then the catch becomes a static one. Without !, µ alone would only implement a shallow form of catch.

A dynamically scoped catch can also be implemented using a µ ′′ d in conjunction with !:

s : Γ ⊢ A; Θ, A d ; [A d , ∆] µ ′′ d.[d]!d.s : Γ ⊢ A; Θ; [A d , ∆] catch
When this catch is executed on the abstract machine of Figure 3, which interprets µ as µ ′′ when possible, any previously saved continuation with label d will be overridden. The representation of throw can only be explained alongside other refinements. These refinements can be applied to both the static and the dynamic versions of catch.

In designing a type system for a programming language, we can use red types for data values (integers, strings, etc), while green types will represent errors. In existing formulations of exception handling using classical logic, a throw can occur at any point in the program and different types of exceptions are not distinguished. We wish to enforce stronger constraints for exception raising. PCL has the capability to implement this kind of constraint, but in NPC as given, all locked formulas are placed inside the same box. Under this interpretation, any error can trigger any kind of exception. We need to modify NPC as follows.

First, enumerate all green formulas as E 0 , E 1 , E 2 , . . ., with E 0 = ⊥.

Next, sequents are now Γ ⊢ F; Θ; [∆ i1 ] i1 . . . [∆ in ] in , where i 1 . . . i n are distinct non-negative integers. The boxes are considered unordered (placed inside a set of boxes). The new versions of Lock and Unlock are found in Figure 4. The restricted form of the right premise of U nlock i suffices for our purposes. The introduction rules are adjusted in the obvious way: the contents of each [ ] i that appears in a premise are merged in the conclusion.

The meaning of a formula A inside [ ] i is now A → E i on the left-hand side. The semantics easily assure us that these rules remain sound (because (B → E i ) ∨ B is valid). They are also complete since we can still choose to lock all formulas in [ ] 0 . Sequents are still finite since only a finite number of boxes would be needed in a proof. When interpreted as a constant, ! i (in the form that implements contraction) would be of type ((P → E i ) → P ) → P (the proof of this formula is an η-expansion of ! i if ! i is interpreted as a constant: this is to be expected.)

We shall refer to this version of NPC as NPC n . A procedure that could throw an exception will have a type of the form B → (R ∨∼∼E i ) where E i is the type of the exception. The double intuitionistic negation is used so that the disjunction is red, and so the implication remain red, i.e., intuitionistic, without which it would be possible for E i to escape scope just as in a classical logic setting. Using an explicit ∨ to represent an exception type may seem contrary to the very idea of exception handling, in which errors need not be handled locally. However, our ∨ is multiplicative, with an introduction rule that is also invertible. The following term can be used to invert any A∨ ∼∼E i to leave only A in the stoup, which then can be cut with an A → B without interference from ∼∼E i :

λx.(λu.u, λv.µz.[d]v)x :⊢ (A ∨ B) → A; B d ; .
In this context, the sequence of rules that constitutes throwing an exception is as follows (with some details elided):

x :∼E x i ⊢∼E i ; ; s : Γ ⊢ A, E e i , A d ; [∆] i . . . Γ ⊢ E i ; A d ; [∆] i . . . Γ ⊢ E i ; ; [A d , ∆] i . . . U nlock ∼E x i , Γ ⊢ 0; [A d , ∆] i . . . → E i Γ ⊢∼∼E i ; R z , Θ; [A d , ∆] i . . . → I Γ ⊢ R; ∼∼E y i , Θ; [A d , ∆] i . . .
Here, x and e are vacuous in s (weakened) and catch is similarly extended to catch i . The abstract machine of Figure 3 can be modified by tagging each entry in [GE] with an index (i.e., with dynamic type information). Figure 5 illustrates the execution of an exception throwing procedure, along with the integral throw i rule. Note that the procedure labeled g cannot throw an E i -type exception because of the scoping constraint of intuitionistic → introduction. Another refinement to note: in terms of Java, E 0 = ⊥ is the superclass Exception of all exceptions. Other exceptions can be represented by green atoms and superclasses by conjunctions of green atoms. Thus a catch IOException can also catch a SocketIOException, etc.

To be fair to classical logic, we should note that it is also possible to give a logical interpretation to the boxes [ ] i . Reserve a set of of unique atoms q 1 , q 2 , . . . The meaning of a formula P inside [ ] i would be P → q i on the left-hand side (but [ ] 0 for ⊥ cannot be emulated). Then Lock is admissible because ((P → q i ) → P ) → P is classically provable, and U nlock becomes → elimination, which is possible when q i appears on the right-hand side. However, what cannot be changed is that classical implication is equivalent to a disjunction. A sequent with (A → B ∨ q 1 ), (C → D ∨ q 2 ) is equivalent to (A → B ∨q 1 ∨q 2 ), (C → D ∨q 1 ), q 2 along with numerous other possible interpretations. Thus, such an effort in classical logic is bound to be fruitless.

This example illustrates the value of retaining intuitionistic implication while allowing for classical reasoning. PCL

s : Γ ⊢ F; Θ; [B x , ∆] i . . . ! i x.s : Γ ⊢ F; Θ, B x ; [∆] i . . . Lock i s : Γ ⊢ A; Θ, B d ; [∆] i . . . t : Γ ′ ⊢ E i → A; ; ? i x.(t s) : ΓΓ ′ ⊢ A; Θ; [B d , ∆] i . . . U nlock i
⊢ R; ∼∼ E y i , Θ; [A d , ∆] i . . . throw i C, Γ ⊢ A; ; [K d ] i g : Γ ⊢ C → A; ∼∼E x i ; [K d ] i → I Γ ⊢ K; E x i , K d ; [ ] i Γ ⊢ C; ∼∼E x i ; [K d ] i throw i Γ ⊢ A; ∼∼E x i ; [K d ] i → E Γ ⊢ A∨ ∼∼E i ; ; [K d ] i ∨I Figure 5
. throw E i and sample usage with saved continuation K is not a strengthening of intuitionistic logic or weakening of classical logic: it is a unified logic.

V. SEQUENT CALCULUS, CUT ELIMINATION, SOUNDNESS, AND COMPLETENESS

In this section, we establish some basic properties so that PCL can be called logic.

We begin with a sequent calculus, LPC, with the subformula property and is suitable for proving completeness. Sequents are of the form Γ ⊢ Θ; [∆]. The stoup is folded into the right-side context as there are no proof terms. In Figure 6, e represents ⊥ or a green atom, a represents an arbitrary atom, and A, B represent arbitrary formulas.

From the subformula property of this sequent calculus, it is plainly obvious that if a formula is purely red, then it can only have an intuitionistic proof: even a failed partial proof would be intuitionistic once useless Locks are discarded.

A formula with green subformulas may still have an intuitionistic proof if only intuitionistic rules are applied. This particular proof system reveals an important property.

Proposition 1: If a formula A is provable with an atom b colored red, then A is also provable with b colored green. Clearly this holds since the presence of a green atom can only lead to more proofs.

The correctness of other proof systems for PCL follow from the correctness of LPC once the following properties are established.

A. Cut Elimination

In a polarized system, it is important to understand the effect of polarization on cut elimination. The restriction to a green atom or ⊥ in the LPC U nlock rule (and the ⊥L rule) can, in fact, be relaxed to allow all green formulas. We used the restriction for two reasons. First, technically speaking, "sequent calculus" rules should only depend on the top-level structure of formulas. The second reason concerns cut elimination. Consider the following scenario involving the relaxed form of U nlock, labeled here as U nlock ′ :

Γ ⊢ E, Θ, B; [∆] Γ ⊢ E, Θ; [B, ∆] U nlock ′ E, Γ ⊢ R, Θ; [∆] Γ ⊢ R, Θ; [B, ∆] cut
Here, E is an arbitrary green formula and R is a red formula. The U nlock ′ rule is also semantically sound and should not destroy cut-elimination. In a natural deduction setting, the above situation is normalized by simple substitution. However, cut-elimination in sequent calculus requires us to permute the cut upwards, until E in both subproofs are introduced, forming a "key case." But if we permuted the cut up to the premise of U nlock ′ , we would get

Γ ⊢ R, Θ, B; [∆].
Since R is red, the U nlock ′ may not be applicable beneath. By restricting to a green atom or ⊥, we can permute the cut upwards until the right subproof reaches Id at which point the cut is reduced by substitution just as in natural deduction. If the cut formula is ⊥, we similarly permute the cut up the right subproof until it reaches ⊥L, at which point the formula on the right-hand side of the conclusion of ⊥L is green, which means we can now permute the cut above the U nlock ′ . This is an example of how polarity information is used to control cut elimination, in a manner not unlike what is found in focused proof systems. However, that is not the principal use of polarization in PCL. Instances of cut 2 reduce to cut; they represent structural reduction. A crucial case of cut elimination occurs when cut is permuted above Lock, which can be a contraction: here cut 2 is applied to the copy of the cut formula inside [ ]. The inductive measure of the proof is the lexicographical ordering consisting of the size of the cut formula, followed by the number of Lock rules above the cut, then the heights of subproofs. The rest of the proof is fairly standard. Theorem 3: Both cut and cut 2 are admissible in LPC.

Γ ⊢ Θ; [B, ∆] Γ ⊢ Θ, B; [∆] Lock Γ ⊢ e, Θ, B; [∆] Γ ⊢ e, Θ; [B, ∆] U nlock A, Γ ⊢ B; [∆] Γ ⊢ A → B, Θ; [∆] → R Γ ⊢ A, B, Θ; [∆] Γ ⊢ A ∨ B, Θ; [∆] ∨R Γ ⊢ A, Θ; [∆] Γ ⊢ B, Θ; [∆] Γ ⊢ A ∧ B, Θ; [∆] ∧R Γ ⊢ A, Θ; [∆] B, Γ ⊢ Θ; [∆] A → B, Γ ⊢ Θ; [∆] → L A, Γ ⊢ Θ; [∆] B, Γ ⊢ Θ; [∆] A ∨ B, Γ ⊢ Θ; [∆] ∨L A, B, Γ ⊢ Θ; [∆] A ∧ B, Γ ⊢ Θ; [∆] ∧L 0, Γ ⊢ Θ; [∆] 0L ⊥, Γ ⊢ e, Θ; [∆] ⊥L Γ ⊢ 1, Θ; [∆] 1R a, Γ ⊢ a, Θ; [∆] Id

B. Soundness and Completeness

Soundness of LPC is proved by induction on proofs. Most important are the three non-intuitionistic rules. Lock is sound because ¬A ∨ A is always valid, while U nlock and ⊥L are sound because ⊥ → E is valid for green E. The other rules are all intuitionistically valid.

Completeness is proved by following the traditional strategy of Kripke, Smullyan and Fitting (especially the presentation of Fitting [START_REF] Fitting | Intuitionistic Logic Model Theory and Forcing[END_REF].) A sequent is considered consistent if it is not provable. Given an unprovable formula A, we can show, using cut elimination, that A ∨ ⊥ is also unprovable. We then construct a countermodel as a saturated tableau of consistent sequents starting with ⊢ A, ⊥; [ ]. All sequents will have the characteristics of Hintikka sets. However, the root sequent will also be maximally consistent with respect to ⊥ (Γ ⊢ ⊥; [ ] is not provable): enumerate all subformulas B of A and their negations ¬B and insert each into Γ ([ ] is absorbed into Γ because of its semantic meaning) if it keeps the sequent consistent with respect to both A and ⊥. Since B ∨ ¬B is provable, by the admissibility of cut it follows that exactly one of B or ¬B will be inserted into Γ in any such saturation. Thus whenever another formula is properly added to Γ by → R, forming a new possible world, it will always become ⊥-inconsistent. All such worlds force ⊥, but not Γ, which represents the root.

Theorem 4: A formula is valid in PCL if and only if it is provable in LPC.

Another basic property we can establish from cut elimination is that (propositional) PCL is decidable, following traditional arguments.

VI. CORE FRAGMENTS OF PCL

It is easy to identify the purely intuitionistic and purely classical fragments of PCL.

Intuitionistic Logic: Color all atoms red, and do not use ⊥. All formulas are red.

Classical Logic: Color all atoms green, and use ⊥ instead of 0. In this extreme, ¬ becomes involutive.

LC-style classical logic: Color all atoms red, but use ⊥ instead of 0. Furthermore, restrict all uses of → to ¬a where a is atomic. All formulas are in negation normal form. Define a syntactic-level operation (i.e, not a new connective) A ⊥ that represents the De Morgan dual of A:

1 ⊥ = ⊥, ⊥ ⊥ = 1, a ⊥ = ¬a, (¬a) ⊥ = a, (A ∨ B) ⊥ = A ⊥ ∧ B ⊥ , and (A ∧ B) ⊥ = A ⊥ ∨ B ⊥ .
Then A ⊥⊥ is syntactically identical to A. Red formulas are "positive" and green ones are "negative." Notice that A and A ⊥ are always of different polarities. In fact, it is valid to consider 1 as either green or red; we designated it red to preserve this LC-type duality. It is possible to construct a fully focused proof system that takes advantage of the perfect dualities of this fragment, but that has already been done [START_REF] Liang | Focusing and polarization in linear, intuitionistic, and classical logics[END_REF].

Intuitionistic Control Logic: The purpose of PCL was far more than to support intuitionistic and classical logics as independent fragments. If we colored all atoms red, but do not use 0, we get an intermediate logic with the excluded middle A ∨ ¬A but without involutive negation ¬¬A → A. If we further allowed the use of both ⊥ and 0, then we get a more expressive logic where both call/cc and the C control operators can be obtained. We regard this as an important fragment of PCL, and refer to it as intuitionistic control logic (ICL).

In the ICL fragment, formulas need not be considered polarized. Rather, the formula ⊥ is given unique treatment. Key to the validity of the unpolarized interpretation is Lemma 2, which showed that only green atoms and ⊥ need to be given a special role in proofs, in which case the polarity of non-atomic formulas lose their significance.

We further distill ICL down to its implicational fragment to present a compact natural deduction system NJC with terms (Figure 7). NJC sequents are of the form Γ ⊢ A; [∆], so it extends the single conclusioned NJ.

The stoup is always non-empty in NJC. The Esc rule of NJC combines the roles of Esc and U nlock in LPC. The rule Con (for contraction) and the γ binder replaces µ. However, Con keeps the stoup locked. The formula inside the stoup must be computed by intuitionistic introductions and eliminations, at least until ⊥ appears. NJC preserves NJ- style intuitionistic provability as much as possible. Weakening is only present as a result of 0-elimination, which is intuitionistically valid. The normalization rules of "λγ-calculus" consist of three reduction rules followed by three renaming rules:

t : A x , Γ ⊢ B; [∆] (λx.t) : Γ ⊢ A → B; [∆] → I t : Γ ⊢ A → B; [∆] s : Γ ′ ⊢ A; [∆ ′ ] (t s) : ΓΓ ′ ⊢ B; [∆∆ ′ ] → E s : Γ ⊢ 0; [∆] abort s : Γ ⊢ A; [∆] 0E exit : Γ ⊢ 1; [∆] ⊤I x : A x , Γ ⊢ A; [∆] Id t : Γ ⊢ A; [∆] [d]t : Γ ⊢ ⊥; [A d , ∆] Esc u : Γ ⊢ A; [A d , ∆] γd.u : Γ ⊢ A; [∆] Con
(λx.s)t -→ s[t/x] (γd.s)t -→ γd.(s{[d](wt)/[d]w}t) abort(s)t -→ abort(s) γa.s -→ s, when a is not free in s γa.γb.s -→ γa.s[a/b] [d]γa.s -→ [d]s[d/a].
We have proved that this system is confluent and strongly normalizing following traditional techniques. Of course, as in λµ calculus, confluence is possible because certain other reduction rules were excluded.

The following NJC proof shows that the C control operator [START_REF] Felleisen | A syntactic theory of sequential control[END_REF] can be obtained.

x :∼ ¬A x ⊢∼ ¬A; [ ] y :∼ ¬A x , A y ⊢ A; [ ] Id [d]y :∼ ¬A x , A y ⊢ ⊥; [A d ] Esc λy.[d]y :∼ ¬A x ⊢ ¬A; [A d ] → I x λy.[d]y :∼ ¬A x ⊢ 0; [A d ] → E abort (x λy.[d]y) :∼ ¬A x ⊢ A; [A d ] 0E γd.abort (x λy.[d]y) :∼ ¬A x ⊢ A; [ ] Con C = λx.γd.abort (x λy.[d]y) : ⊢ ∼¬A → A; [ ] → I
Compared to the original λµ calculus, there is no free variable in the C operator. A similar proof, of (¬P → P ) → P , derives the call/cc operator as λx.γd.(x λy.[d]y). Thus, NJC already captures the essential computational capabilities of λµ-calculus without destroying intuitionistic logic.

There is no known translation of PCL to intuitionistic logic, or to linear logic. We have reasons to consider such translations unlikely. Any double negation translation of PCL must allow A ∨ ¬A but deny ¬¬A → A. Linear logic also includes both classical and intuitionistic logics, but not every intermediate logic. One might be tempted to equate green formulas with linear logic formulas ?A: but consider Peirce's formula ((P → Q) → P ) → P translated as !(!(!P -•?Q) -• P ) -• P . This formula is still not provable. The challenge is to provide a translation that preserves provability while keeping at least the outer implication intuitionistic (equivalent to !A -• B) 3 . However, it is simple to translate PCL into ICL: for each green PCL atom e, reserve a unique ICL atom e ′ , and translate e as ¬e ′ . For example, ¬¬e → e becomes ¬¬¬e ′ → ¬e ′ , which is minimally valid. Thus, ICL forms a core fragment of PCL.

Nevertheless, PCL is significantly more expressive. It embeds classical logic more clearly than ICL. Having green formulas other than ⊥ means more expressive type systems. It also means that restricting the context outside of [ ] to a single formula becomes impractical. The combination of Lock and Open into a single Con rule in NJC hides potential computational capabilities.

VII. CONTINUING WORK: SECOND ORDER PCL

One problem that has faced polarized logics has been how to assign polarities to second order formulas, specifically to propositional variables that are bound by ∀ and ∃. One might consider two versions of each quantifier, which restricts also the polarity of formulas that can instantiate them. Another approach might be to keep bound variables unpolarized. None of these approaches seem satisfactory. Proposition 1, however, shows that provability is preserved if some red atoms were colored green instead. In PCL, one can prove a formula such as b → b with b considered red, so of course b can be replaced by any formula, red or green. On the other hand, one can show that there exists a formula ¬¬b → b that is provable only if b is considered green. The following important attributes form the basis of a second order propositional PCL: • In ∀X.P , the free occurrences of X in P are red; • In ∃X.P , the free occurrences of X in P are green.

• ∀X.P is green if P is green, otherwise it is red.

• ∃X.P is green if P is green, otherwise, it is red.

The inference rules for ∀ and ∃, in the context of LPC, are as follows Γ ⊢ A[B/X], Θ; The usual restrictions on variable occurrences apply. Note that just because ∃-quantified variables are green does not mean that they cannot be instantiated with red formulas in ∃R. If one can find an existential witness that is red, then so much the better. We can still universally quantify over green formulas using ∀X.(⊥ → X) → P : although ⊥ → X is not technically green, it implies equivalence with green formulas. No complementary form exists, however, to restrict ∃ to quantify over only red formulas. That would mean requiring something to be anything: a self-contradiction.

Polarization has been used elsewhere as a reflection of duality. The polarities of PCL, however, define two levels of provability. Nevertheless, a duality between the second-order ∀ and ∃ introduction rules is revealed. The natural role of polarization in second order PCL is possible because we did not insist on enforcing dualities when assigning polarities to formulas, because we did not insist on an involutive form of negation for all formulas.

VIII. CONCLUSION

The computational content of classical logic depends on how classical proofs are structured. PCL can still be considered classical logic in that every PCL proof is also a classical proof and, with the right polarity assignments, every classically provable formula has a PCL proof.

There are multiple approaches to controlling classical proofs. By the manner that polarities are assigned to formulas, PCL appears similar to LC. The similarity hides a much deeper distinction. The polarization of LC corresponds to dualities found in linear logic. This notion of polarization is principally concerned with the structure of proofs, with how it controls cut elimination. Focused proofs further advance this use of polarization, and we have contributed to focusing in some of our own work. Although polarization in PCL also impacts cut elimination as we have shown, it is mainly concerned not with the structure of proofs, but with provability. It is characterized by when a formula can be considered valid. Focusing in PCL is an issue that is orthogonal to its polarization.

In contrast to LC and focusing, the PCL approach to controlling proofs use restrictions on inference rules that are required for soundness, relative to a semantics of validity. The two approaches are not necessarily incompatible, and we hope to combine them in future work.

Figure 3 .

 3 Figure 3. An Abstract Machine For λµ!

Figure 4 .

 4 Figure 4. Lock and Unlock with multiple boxes s : Γ ⊢ A; E e i , A d ; [∆] i . . . µz.[y]λx.(x ?d.µe.[d]s) : Γ ⊢ R; ∼∼ E y i , Θ; [A d , ∆] i . . .

Figure 6 .

 6 Figure 6. Sequent Calculus LPC; (e is a green atom or ⊥)

Figure 7 .

 7 Figure 7. NJC Proof System for Intuitionistic Control Logic

  [∆] Γ ⊢ ∃X.A, Θ; [∆] ∃R A, Γ ⊢ Θ; [∆] ∃Y.A, Γ ⊢ Θ; [∆] ∃L, Y green Γ ⊢ A; [∆] Γ ⊢ ∀Y.A, Θ; [∆] ∀R, Y red A[B/X], Γ ⊢ Θ; [∆] ∀X.A, Γ ⊢ Θ; [∆] ∀L

  Most of the following definitions are inherited from the λµ machine. A machine state is defined inductively as St; [GE], where St is a stack that consists of a list of closures. A closure t, CE, LE consists of a λµ!-term t, a closure environment CE, and a (local) stack environment LE. A closure environment consists of a list of bindings (x, C) where x is a (λ) variable and C is a closure. A stack environment consists of a list of bindings (d, S) where d is a (µ) variable and S is a stack. [GE] is the global stack environment. Conceptually, a stack represents a sequence of cuts. A closure represents a subproof with pending cuts suspended in closure and stack environments. Each transition of the machine represents a cut reduction step.

  x, CE, LE :: S; [GE] -→ CE(x) :: S; [GE] (u v), CE, LE :: S; [GE] -→ u, CE, LE :: v, CE, LE :: S; [GE] λx.t, CE, LE :: C :: S; [GE] -→ t, (x, C) :: CE, nil :: S; [GE] µd.t, CE, LE :: S; [GE] -→ t, CE, (d, S) :: LE :: S; [GE] [d]t, CE, LE :: S; [GE] -→ t, CE, LE :: LE(d); [GE]

	!d.t, CE, LE :: S; [GE] -→ t, CE, LE :: S; [(d, LE(d)) :: GE]
	?d.t, CE, LE :: S; [GE] -→ t, CE, (d, GE(d)) :: LE :: S; [GE]

Not all versions of classical λµ calculus can be translated: the original λµ allowed proofs of theorems to contain free variables, which is not possible in N P C.

The relaxed form of U nlock is used in NPC proofs, so we establish its equivalence with the restricted version.Lemma 2: In a cut-free proof, every instance of U nlock ′ can be replaced by U nlock.The proof consists of permutation arguments, depending on the rule above U nlock ′ .Cut elimination is proved for LPC in two forms:Γ ⊢ A, Θ; [∆] A, Γ ′ ⊢ Θ ′ ; [∆ ′ ] ΓΓ ′ ⊢ ΘΘ ′ ; [∆∆ ′ ] cut Γ ⊢ Θ; [A, ∆] A, Γ ′ ⊢ B, Θ ′ ; [∆ ′ ] ΓΓ ′ ⊢ ΘΘ ′ ; [B, ∆∆ ′ ] cut 2

Furthermore, the translation should define valid synthetic connectives (i.e., preserve focus in the introduction rules).

Acknowledgments. The authors wish to thank Stéphane Lengrand and the anonymous reviewers for helpful comments.


Julien Mille

Sébastien Bougleux

Laurent D Cohen

Combination of paths for interactive segmentation

Active contours and minimal paths have been extensively studied theoretical tools for image segmentation. The recent geodesically linked active contour model, which basically consists in a set of vertices connected by paths of minimal cost, blend the benefits of both concepts. This makes up a closed piecewise-smooth curve, over which an edge or region energy functional can be formulated. As an important shortcoming, the geodesically linked active contour model in its initial formulation does not guarantee the curve to be simple, consistent with respect to the purpose of segmentation. In this paper, we propose to extract a relevant contour from a set of possible paths, such that the resulting structure fits the image data and is simple. Toward this goal, we introduce a novel term to favor the simplicity of the generated contour, as well as a local search method to choose the best combination among possible paths.

Introduction

Minimum cost paths for interactive two-phase segmentation provide a solid mathematical background and have proven to find suitable solutions in many practical situations. Provided a set of landmark points typically located along the boundary of interest, paths are computed between these points in order to build a closed contour. Optimality is the main advantage of such approaches, since in most cases, a minimum cost path can be efficiently found as the global solution of the corresponding minimization problem, like Dijkstra's algorithm for shortest paths in directed graphs with no negative cycle. Interactive segmentation methods based on a graph modeling of the image, making them discrete by nature, include the intelligent scissors (or live-wire) [START_REF] Mortensen | Interactive segmentation with intelligent scissors[END_REF] and their on-the-fly extension [START_REF] Falcão | An ultra-fast user-steered image segmentation paradigm: Live Wire on the Fly[END_REF], as well as the riverbed approach [START_REF] Miranda | Riverbed: A novel user-steered image segmentation method based on optimum boundary tracking[END_REF] based on the image foresting transform [START_REF] Falcão | The Image Foresting Transform: Theory, algorithms, and applications[END_REF]. As regards continous models, the minimal path method [START_REF] Cohen | Global minimum for active contour models: a minimal path approach[END_REF] achieved global minimization of the geodesic active contour functional [START_REF] Caselles | Geodesic active contours[END_REF], with fixed userprovided endpoints, using the Fast Marching method [START_REF] Sethian | A fast marching level set method for monotonically advancing fronts[END_REF][START_REF] Tsitsiklis | Efficient algorithms for globally optimal trajectories[END_REF]. An interactive extension was later proposed by [START_REF] Gérard | Real-time interactive path extraction with on-the-fly adaptation of the external forces[END_REF]. Since the control points are fixed and must be located on the target contour, the minimal path approach does not represent a curve which deforms its shape. Moreover, due to the restricted number of these points, the geodesic may fail to capture a relevant contour if the image is too noisy, not contrasted enough, or if the target contour is too lengthy. While several methods concentrate on avoiding this second drawback [START_REF] Appia | Active geodesics: Region-based active contour segmentation with a global edge-based constraint[END_REF][START_REF] Benmansour | Fast object segmentation by growing minimal paths from a single point on 2D or 3D images[END_REF][START_REF] Kaul | Detection of curves with unknown endpoints and arbitrary topology using minimal paths[END_REF], the geodesically linked active contour model of [START_REF] Mille | Geodesically linked active contours: evolution strategy based on minimal paths[END_REF] allows to overcome the first one, as it can be evolved thanks to a local search method. This latter model combines the advantages of geodesics with the ones of region-based energies, such as the minimal variance term proposed by [START_REF] Chan | Active contours without edges[END_REF]. Despite its robustness to local minima, this model can fail to construct a simple curve, i.e. without double point, from the initialization step to the end of the evolution.

To overcome this drawback, we propose to generate several relevant paths between landmark points and to select the combination of paths generating the best closed contour. In this extent, we introduce an energy functional, combining contour and region terms with a novel term favoring the simplicity of the curve, penalizing self-overlapping and self-intersections. Our three contributions, i.e. the construction of admissible paths, the simplicity energy as well as the selection of the optimal combination of paths, are described in details. The concepts on which relies the proposed approach are recalled in the following section.

Background: geodesic and piecewise-geodesic curves

To extract structures in a given image I : D → R d , [START_REF] Cohen | Global minimum for active contour models: a minimal path approach[END_REF] proposed to find curves of minimal length according to an heterogeneous isotropic metric defined from a potential P : D → R * + . In the context of contour extraction, curves should be located along edges. The potential is thus defined as P = g + w, where g : D → R + is a decreasing function of the gradient magnitude of I at some scale s:

g(x) = 1 1 + ∇G s * I(x) (1)
where G s is a Gaussian kernel and w ∈ R * + is a regularizing constant. Given two points a and b, the curve of minimal length, or geodesic path between them,

γ a,b = argmin C⊂D L[C] = 1 0 P (C(u)) C ′ (u) du s.t. C(0) = a C(1) = b (2)
can be obtained by considering the geodesic distance map, also referred to as the minimal action map, U a : D → R + which assigns, to each point x ∈ D, the length of the minimal path connecting a to x. This map is the unique viscosity solution of the Eikonal equation, which makes it efficiently computable by the Fast Marching (FM) method [START_REF] Sethian | A fast marching level set method for monotonically advancing fronts[END_REF][START_REF] Tsitsiklis | Efficient algorithms for globally optimal trajectories[END_REF] in O(N log N ) operations, where N is the number of grid points. Once the distance map has been numerically computed, the minimal path between a and b can be extracted by a gradient descent on U a , starting from b until a is reached. The minimal path approach can fail to extract the desired curve, as depicted in Fig. 1(c). This happens for instance when P is too noisy or not contrasted enough, when the length of the target curve is too important, or when the regularization constant w is too high.

To address this issue, several approaches aim to find a piecewise-geodesic, i.e. a set of geodesics connecting pairs of successive landmark points or vertices (see Fig. 1(d)). Among them, the geodesically linked active contour (GLAC) model [START_REF] Mille | Geodesically linked active contours: evolution strategy based on minimal paths[END_REF] is generated by joining end-to-end geodesic paths built from a set of vertices V = {v i } 1≤i≤n . Given a curve concatenation operator ⋒,

(C 1 ⋒ C 2 ) (u) = C 1 (2u) if 0 ≤ u ≤ 1/2 C 2 (2u -1) if 1/2 < u ≤ 1 , (3)
which is valid only if C 1 (1) = C 2 (0), the closed curve resulting from the assembly of successive geodesics is Γ = γ v1,v2 ⋒γ v2,v3 ⋒...⋒γ vn-1,vn ⋒γ vn,v1 . It is important to keep in mind that a concatenation of geodesics is not a geodesic itself, thus it is relevant to refer to it as piecewise-geodesic. The GLAC approach consists in finding the sequence of n vertices which generates a piecewise-geodesic curve minimizing energy functional E:

E[Γ ] = ω edge E edge [Γ ] + ω region E region [Γ ], (4)
where ω edge and ω region are user-defined weights. The edge-based energy integrates the edge indicator function g of Eq. (1) along the geodesics, normalized by euclidean length |Γ | in order not to penalize lengthy contours. This ensures that short curves, which could be undesirable shortcuts, are not preferred over longer ones.

E edge [Γ ] = 1 |Γ | 1 0 g(Γ (u)) Γ ′ (u) du = 1 |Γ | n i=1 1 0 g(γ vi,vi+1 (u)) γ ′ vi,vi+1 (u) du.
(

) 5
In addition, following the piecewise constant model of [START_REF] Chan | Active contours without edges[END_REF], the region term is expressed as the sum of image variances inside and outside Γ . Since it is not used in the subsequently proposed approach, its mathematical expression is not detailed. Numerical minimization of E with respect to every v i is performed thanks to a greedy algorithm similar in principle to the one proposed in [START_REF] Williams | A fast algorithm for active contours and curvature estimation[END_REF]. Considering a local discrete window W i centered at each vertex v i , greedy evolution is performed, in several passes, by moving vertex v i to the position in the window leading to the GLAC having the smallest energy:

v (t+1) i = argmin ṽi∈Wi E [γ 1 ⋒ ...γ i-2 ⋒ γi-1 ⋒ γi ⋒ γ i+1 ⋒ ... ⋒ γ n ] ,
where γ are the geodesics, according to Eq. ( 2), between the current position in the window and the adjacent vertices of v i , and γ i is a shortened form for γ vi,vi+1 . While this model allows to blend the benefits of minimal paths and region-based terms, it turns out to have a significant drawback, as its initial state is not necessarily a simple closed curve. As depicted in Fig. 1(e), this can occur when the initial vertices are unevenly distributed around the target boundary. In this case, geodesics gather on particular sides of the target boundary, as γ v3,v1 overlaps γ v1,v2 and γ v2,v3 . The reason is that each geodesic is generated independently from the others, such that the obtained piecewise-geodesic curve does not depend on the visiting order of pairs of adjacent vertices. This undesirable phenomenon may occur either as soon as the geodesically linked contour is initialized, or after several evolution steps on a previously well initialized contour. One could consider imposing hard constraints on the overlapping between paths, or penalizing paths enclosing a region with excessively small area, but the independent construction of paths, which allows parallel implementation, prevents such constraints to be implemented. We address this shortcoming in what follows.

Combination of admissible paths

We study a more relevant contour construction preserving the advantages of piecewise geodesic curves. Assuming that a set of several possible relevant paths is available for each pair of successive vertices, we may select a single path from each set and combine these paths in order to build the best boundary curve. The relevancy of the generated contour is measured by an energy functional, combining existing contour and region terms with a novel term penalizing selftangencies and self-intersections, ensuring the contour to be simple.

Sets of admissible paths

Given an ordered pair of successive vertices (v i , v i+1 ), let A i be a set of K i admissible paths linking the two vertices,

A i = {γ i,j } 1≤j≤Ki ,
which we refer to as admissible set. To generate these admissible paths, one could first think about solving the K shortest paths problem [START_REF] Eppstein | Finding the k shortest paths[END_REF][START_REF] Yen | Finding the K shortest loopless paths in a network[END_REF]. However, it is unlikely to generate interesting contours in the context of real images, as the K -1 next shortest paths might be identical to the shortest one, up to some very small localized offset, bypassing the shortest path at one place. Moreover, the K shortest paths principle does not fit well into the continuous framework of minimal paths. A second intuitive technique consists in computing K disjoint paths, as in [START_REF] Mille | Minimally overlapping paths sets for closed contour extraction[END_REF], i.e. preventing each path to pass through points already visited by a previous path. This is achieved by setting P (x) to +∞ for all x belonging to each newly generated path. However, it would arbitrarily remove sections of contour that could be taken by other relevant paths. Moreover, in case of unsharp contours, low potential areas may get undesirably thick, so that two paths C 1 and C 2 may take the same contour section, C 2 being only an offset curve of C 1 .

To generate supplemental paths, we propose an approach based on the extraction of saddle points. Such critical points were already addressed in the case of minimal action maps, like in [START_REF] Deschamps | Fast extraction of minimal paths in 3D images and applications to virtual endoscopy[END_REF]. As explained in Section 2, the geodesic linking two points a and b is extracted by propagating the minimal action from a, stop when b is reached, and perform gradient descent from b. The opposite may also be done, provided that the path is reversed afterwards. A third way to compute γ a,b consists in propagating simultaneously from a and b, stopping at the first location where the two fronts meet, performing two gradient descents both sides apart from the meeting location, and assembling the two obtained paths adequately. This principle serves a basis for the generation of multiple paths. When propagation is performed from two source points, yielding the combined action map In order to extract robust local minima in spite of the effect of discretization, values of the action map are smoothed along m a,b . Not all saddle points are kept as starting points for path construction. In practice, we limit the number of admissible paths per set below a fixed threshold K max . As can be seen in Fig. 3(b), many saddle points are intentionally ignored because of their action too high or their proximity to lower saddle points. The contour resulting from the concatenation of selected paths should exhibit desirable properties in the image. One of these properties is that the generated contour should be simple, i.e. with no multiple point. Instead of imposing simplicity as a hard constraint, which might exclude relevant contours, it is encouraged by an additional energy. Indeed, it is reasonable to allow a certain degree of nonsimplicity, e.g. when vertices are located far from the target boundaries, which might cause several admissible paths to have common sections before splitting up, like in Fig. 1(e). The proposed term is based on a distinction between selftangency and self-intersection, which we present hereafter.

Self-overlap and twisting Consider a curve C closed and regular, i.e. non-singular in the parametric sense, meaning that its velocity vector C ′ vanishes nowhere. If C is non-simple, it has a number of multiple points that should be studied. We only consider double points1 , which may be of two kinds. Let (u, v) ∈ [0, 1]2 s.t. u = v be the unordered pair of curve positions identifying a double point: C(u) = C(v). On one hand, if (u, v) corresponds to a point of self-tangency, velocity vectors C ′ (u) and C ′ (v) are colinear. On the other hand, if (u, v) corresponds to a self-intersection -also known as an ordinary double point or crunode -velocity vectors point towards different directions, making the curve cross itself. This distinction allows to address separately two different defects on curves, which are not necessarily related. A curve with points of self-tangencies will exhibit self-overlapping segments, as depicted in Fig. 4(b), whereas a curve with self-intersections shown in Fig. 4(c) will split the image domain into more than two connected regions.

As regards the first kind of double points, the amount of overlapping is quantified by measuring the length of overlapping curve segments. Considering function φ measuring the Euclidean distance between two points on the curve, all pairs (u, u)). The length of Z C in the (u, v)-space corresponds to the total length of the overlapping segments:

φ C (u, v) = C(u) -C(v) , the zero level set of φ C , Z C = {(u, v) | C(u) = C(v)} is
|Z C | = 1 0 1 0 ∇H(φ C (u, v)) dudv = 1 0 1 0 δ(φ C (u, v)) ∇φ C (u, v) dudv (6)
where ∇ is the gradient operator in the (u, v)-space, H is the Heaviside step function and δ is the Dirac delta distribution. It can be proven that for any simple regular curve C, |Z C | = √ 22 , which can be intuitively understood by observing the plots of φ in the curve parameter space in Fig. 4, where dark lines correspond to self-overlapping segments. If the curve is non-simple,

|Z C | ≥ √ 2.
Moreover, it is advantageously intrinsic, i.e. independent from parameterization, and invariant to scaling. Note that intersection points may be viewed as overlapping segments of length zero, and thus have no contribution in |Z C |. Discretizing C as a 4-connected digital curve, made up of M points in Z 2 , the length of overlapping segments in Eq. ( 6) can be computed in O(M ) operations.

While tangent double points are used to measure overlapping, ordinary double points will serve as a basis for measuring the amount of twisting. Consider a regular closed curve C oriented clockwise with ordinary double points making self-intersections as shown in Fig. 5(a). It splits the image domain into disjoint subdomains, some of which are demarcated by inverted segments, i.e. portions of curves along which the normal vector C ′⊥ points outward (on a simple clockwiseoriented curve, C ′⊥ points inward). We propose to quantify the twisting of C as the proportion of area demarcated by inverted segments to the total area of C. This proportion is related to the energy that one would exert to untwist the curve. A self-intersecting curve can be thought of as a planar projection of a knot, i.e. an embedding of the unit circle into Euclidean R 3 space. Following the theory of knots [1, p. 13] [3], we consider twisted configurations of curves which corresponding knots could be unknotted by Reidemeister moves of type I and II (see Fig. 5(b) and 5(c), respectively). The simple loop, described by a single connected inverted segment and involving a single intersection, is related to the Reidemeister move of type I, whereas the double loop, consisting of two inverted segments and involving two intersections, is related to the Reidemeister move of type II. Let SL(C) ⊂ [0, 1] 2 be the set of ordered pairs of curve positions (u, v) s.t. u < v describing intersections involved in single loops, and DL(C) ⊂ [0, 1] 2 × [0, 1] 2 be the set of double ordered pairs ((u 1 , v 1 ), (u 2 , v 2 )) s.t. u 1 < u 2 and v 1 > v 2 describing the couples of intersections involved in double loops. The total inverted area I[C] is computed in linear time with respect to |C| using Green's theorem:

I[C] = - (s,t)∈SL(C) min 0, t s C ⊥ • C ′ 2 du - ((s1,t1),(s2,t2))∈DL(C) min 0, s2 s1 C ⊥ • C ′ 2 du + t1 t2 C ⊥ • C ′ 2 du ( 7
)
where the line integrals involved will be negative for inverted segments.

Optimization The computation of an admissible closed contour can be formulated as determining the sequence of labels {x 1 , x 2 , . . . ,

x n } minimizing E γ 1,x1 ⋒ γ 2,x2 ⋒ ... ⋒ γ n-1,xn-1 ⋒ γ n,xn
, where label x i corresponds to the chosen path in set A i . Energy E extends Eq. ( 4) involved in the GLAC. It is designed to penalize contours exhibiting strongly overlapping sections or self-intersections, poorly fitting to edges, or splitting regions with indistinct color statistics:

E[Γ ] = E simplicity [Γ ] + ω edge E edge [Γ ] + ω region E region [Γ ]. (8)
Weights ω edge and ω region are user-defined parameters controlling the relative significance of the edge and region terms over the simplicity term. This last one involves the normalized self-overlapping and twisting measures defined in Eqs. ( 6) and ( 7),

E simplicity [Γ ] = |Z Γ | - √ 2 √ 2 + 1 |Ω in (Γ )| I[Γ ]
whereas the edge term is defined as in Eq. ( 5). For the region term, instead of using the piecewise-constant model as in the GLAC, which limits the segmentation to relatively homogeneous objects and backgrounds, we use the Bhattacharyya coefficient between the color probability distributions inside and outside Γ , following [START_REF] Michailovich | Image segmentation using active contours driven by the Bhattacharyya gradient flow[END_REF]:

E region [Γ ] = C p in (Γ, α)p out (Γ, α)dα (9)
Probability distribution functions (PDF), for a given color α, are estimated using a Gaussian kernel-based histogram:

p in (Γ, α) = 1 |Ω in (Γ )| Ωin(Γ ) G σ (α -I(x))dx p out (Γ, α) = 1 |Ω out (Γ )| Ωout(Γ ) G σ (α -I(x))dx
where Ω in and Ω out are the regions inside and outside Γ , respectively. To determine the best sequence of labels {x 1 , . . . , x n }, a brute-force search would yield an exponential complexity of O(K n max ). To avoid testing all possible configurations, we propose a greedy search in O(n 2 K max ) relying on a specific ordering of paths. In each admissible set A i , paths are sorted according to increasing exteriority X , i.e. the signed area, calculated with Green's theorem, formed by a given path C and the line segment from C(1) returning to C(0)3 :

X [C] = 1 2 1 0 C ⊥ • C ′ du + 1 2 C(1) ⊥ • C(0)
If the straight line from C(0) to C( 1) is taken as a reference horizontal axis, the exteriority is negative (resp. positive) if C is predominantly below (resp. above) the axis. The vertices being located clockwise, admissible paths are sorted from the innermost to the outermost (see Fig. 3(c-f) ). Starting from an initial labelling corresponding to the most interior configuration, i.e. {1, . . . , 1}, labels are changed according to a local search, by iteratively testing candidate labellings. At each iteration, given a current sequence of labels S, candidate sequences are tested that differ from a single label from S, by increasing labels only. For instance, if {2, 3, 1} is the current sequence, candidate sequences will be {3, 3, 1}, {2, 4, 1} and {2, 3, 2}. The candidate sequence leading to the smallest energy, regardless of the current energy, is chosen as the base sequence for the next iteration, while the globally minimal sequence is kept along the iterations. Generating candidate sequences by solely increasing labels makes the contour grow monotonically.

Experiments and discussion

We demonstrate the ability of the model to recover closed boundaries of objects in natural color images, given a variable number of user-provided points along the target boundary. Experiments were carried out on the Grabcut dataset [START_REF] Rother | Grabcut: Interactive foreground extraction using iterated graph cuts[END_REF] in comparison with the original GLAC method [START_REF] Mille | Geodesically linked active contours: evolution strategy based on minimal paths[END_REF] (without deformation, i.e. the piecewise-geodesic curve only), in order to show the benefits brought by the use of admissible paths and additional energy terms.

To keep a critical look at our contribution, Fig. 6 depicts typical cases where the current approach provides strong global improvements over the GLAC, as well as slight localized improvements, for the same given sets of vertices. As regards the selection of parameters, both methods were evaluated in the most favorable configuration, i.e. parameters such as the regularization weight wfor both methods -or the energy weights ω edge and ω region -specifically for the proposed algorithm -, were tuned separately each time, in order to achieve the most relevant segmentation. The appropriate color space was also chosen for each image, i.e. RGB or the more perceptually uniform Lab, which affects potential P for both methods and the color PDFs involved in the region energy [START_REF] Eppstein | Finding the k shortest paths[END_REF].

The BANANA image (row 1) depicts a situation where our approach does not improve segmentation over the GLAC, for this particular configuration of initial points. Despite the complex background and object containing many inner edges, boundaries are well defined and vertices are evenly distributed along the boundary so that the original GLAC manages to extract the object. The FLOWER (row 2) and DOLL (row 3) images are cases where the GLAC exhibits strong overlapping between geodesics when few vertices are provided, although the vertices are reasonably well distributed along the object boundary. Since it does not have any non-overlapping constraint, the GLAC systematically favors portions of contours with the lowest potential. Hence, smooth boundary segments are ignored, not because of their length, but because they may contain sparsely weak edges making the potential increase in small parts of the contour. Conversely, these boundary segments, despite from not being part of the minimal path, make valleys in the distance map and are very likely to be considered as parts of admissible paths by our approach. This proves the proposed method to be inherently less sensitive to weak edges. The CERAMIC (row 4) and TEDDY (row 5) images depicts situations where the GLAC makes shortcuts through the object, due to the presence of inner edges stronger than the actual boundaries. Both simplicity and region energies contribute to solve this issue in our algorithm. The former prevents overlapping while the latter favors high discrepancy between inner and outer color distributions, hence avoiding to select the undesirable shortcuts, which would yield to less distinct color histograms than the actual boundaries would. Finally, the MUSHROOM (row 6) combines the issues of inner shortcut and strong self-overlapping. quantifies the self-overlap of C.

Proposition:

If C is simple, i.e. without self-intersection and self-tangency, then

|Z C | = L √ 2
Proof: As a preliminary calculation, let us express the gradient of φ (partial derivatives are written using the indexed notation):

∇φ(u, v) = [φ u (u, v) φ v (u, v)] T = p C(u) -C(v) p-2 C ′ (u) • (C(u) -C(v)) -C ′ (v) • (C(u) -C(v))
If C is regular and simple, varying with respect to u in range [0, L], φ(u, v) is nowhere zero except when u = v. Hence, for a fixed v, we have:

δ(φ(u, v)) = δ(u -v) |φ u (v, v)| (11)
Integrating ( 11) into [START_REF] Falcão | The Image Foresting Transform: Theory, algorithms, and applications[END_REF] and applying the definition of measure δ:

|Z C | =

B Exteriority term

Let C be a piecewise-smooth regular curve parameterized over [0, 1],

C : u -→ C(u) = [x(u) y(u)] T .
If it is simple and positively oriented such that normal vector C ′⊥ points inward, its inner area may be expressed using Green's theorem:

|Ω in (C)| = 1 2 1 0 C ⊥ (u) • C ′ (u) du = 1 2 1 0
x(u)y ′ (u) -x ′ (u)y(u) du

When one calculates the previous expression on a non-simple closed curve, one gets the signed area, in which positively and negatively oriented connected components have positive and negative contributions, respectively.

C

C(0) Fig. 7. The exteriority of an open curve is measured as the signed area of the multiple connected region that it forms with the line segment joining its two endpoints

Proposition:

The signed area formed by an open curve C over [0, 1] and the line segment from C(1) returning to C(0) (see Fig. 7), which we use to as the exteriority measure in the paper, may be expressed as:

X [C] = 1 2 1 0 C ⊥ • C ′ du + 1 2 C ⊥ (1) • C(0)
Proof:

Let S be the parametrization of the line segment joining C(1) and C(0), over [0, 1]:

S(u) = (1 -u)C(1) + uC(0)
The signed area is then obtained by applying Green's theorem on a piecewise basis:

X [C] = 1

Fig. 1 .

 1 (a) Potential P (b) Geodesic between two given points. (c) Undesirable shortcut. (d) Piecewise geodesic curve. (e) Undesirable overlapping with unevenly spaced vertices

Fig. 2 .

 2 Fig. 2. Saddle points for determining relevant admissible paths between a and b: (a) Potential highlights two possible distinctive paths, (b) Action map with two admissible paths with their respective saddle points located halfway and (c) corresponding 3D plot

  U a,b = min(U a , U b ), the two propagation fronts meet at the saddle points of U a,b (see Fig 2(a) and 2(b)). If one intuitively imagine the action as the height in a mountainous area, the saddle points are the mountain passes on the different roads travelling from a to b, as depicted in Fig. 2(c). These roads can share common sections, but each road lies in the bottom of a particular valley. Let m a,b : [0, 1] -→ D be the medial curve, assumed to be of class C 2 , sweeping along the points geodesically equidistant to a and b, i.e. {x | U a (x) = U b (x)}. It forms a crest on the combined action map and contains only critical points, put another way ∇U a,b is not defined over m a,b . However, U a,b may be differentiated along the medial curve, which allows to define the saddle points as the local minima of U a,b along m a,b .

Fig. 3 .Fig. 4 .Fig. 5 .

 345 Fig. 4. Distances φC plotted in (u, v)-space for several types of curve: (a) On a simple closed curve, φC vanishes only the graph diagonal. (b) On a curve with a section of self-tangency, φC additionally exhibits two symetrical zero lines. (c) On a curve with self-intersections, φC additionally exhibits isolated zeros

Fig. 6 .

 6 Fig. 6. Results on the Grabcut dataset. For each image, left: potential, center: GLAC without deformation (piecewise-geodesic curve), right: combination of paths

  v) |φ u (v, v)| dvTrivially, φ(v, v) = 0. However expanding the gradient gives:′ (v) • (C(v) -C(v))) 2 p C(v) -C(v) p-2 |C ′ (v) • (C(v) -C(v))| dv =

(( 1 -( 1 -( 1 -C

 111 u)C ⊥ (1) + uC ⊥ (0)) • (C(0) -C(1u)C ⊥ (1) • C(0) -uC ⊥ (0) • C(u)C ⊥ (1) • C(0) + uC ⊥ (1) • C(⊥ • C ′ du + 1 2 C ⊥ (1) • C(0)

In our framework, curves with points of multiplicity>

are detected and excluded from the search

See detailed proof in appendix A

See detailed proof in appendix B

ConclusionBy searching the best paths configuration among sets of admissible paths, given an energy functional combining edge and region data terms with a novel term favoring the simplicity of the curve, we aimed at solving some important issues arising in geodesic-based segmentation, namely shortcuts and self-overlapping or intersecting contours. Comparison against the geodesically linked active contour model, which has similar input and purpose, demonstrated the advantages of the approach. Due to the limited space, an overview of the experiments was given. A thorough evaluation needs to be performed in an extended version of the current paper, including quantification of segmentation accuracy with respect to ground truth segmentations, and evaluation of the sensitivity to several parameters (distribution of initial vertices along the contour, regularization weight, etc.), as well as comparison with related approaches, such as[START_REF] Miranda | Riverbed: A novel user-steered image segmentation method based on optimum boundary tracking[END_REF].

Appendix A Self-overlap term

Let C be a regular curve parameterized over [0, L]. Let φ be a C 1 function defined over [0, L] 2 representing the distance between two positions on the curve: [START_REF] Falcão | The Image Foresting Transform: Theory, algorithms, and applications[END_REF]


Céline Gwenaëlle Quentin

Yves Barbin

Lucio Bellomo

Philippe Forget

Joël Gagelli

Samuel Grosdidier

Charles-Antoine Guérin

Karen Guihou

Julien Marmain

Anne Molcard

Céline Quentin
email: celine.quentin@univ-tln.fr

Joel Gaggelli

Bruno Zakardjian

Pascal Guterman

Karim Bernardet

HF radar in French Mediterranean Sea: an element of MOOSE Mediterranean Ocean Observing System on Environment

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

INTRODUCTION

The MOOSE concept is based on Eulerian observatories and autonomous mobile platforms to support the Mediterranean observation. The main objectives are to observe the long-term evolution of the NW Mediterranean Sea in the context of climate change and anthropogenic pressure and to supply and maintain long-term time series, which are the only relevant data to evidence climatic trends and identify long-term environmental anomalies.

Today, High Frequency Surface Wave Radar (HFSWR) is routinely used for the remote sensing of the ocean surface. Current measurements are obtained from the Doppler shift of the first-order Bragg-resonant echoes ( [Crombie, 1955, 681-682]). Recent oceanographic studies in the Gulf of Lion (NW Mediterranean) have shown the existence of vortex structures and instabilities in a wide range of scales. These properties of the coastal circulation have been well evidenced in the context of the ECOLO campaign [START_REF] Schaeffer | Generation mechanism of mesoscale eddy in the Gulf of Lions: radar observation and modelling[END_REF]([Schaeffer et al., , 1587([Schaeffer et al., -1609]]), where a certain number of in situ and remote sensors have been collocated: SST and water color satellite imagery, satellite-based drifting buoy trajectories and radar derived surface currents.

Our laboratory (MIO) has proven its expertise in radar measurement of surface currents ([Broche et al., 1987, 69-75], [Molcard et al., 2009, s79-s89]) and has been assigned the task to deploy the HF radar network for the MOOSE program.

HF RADAR DEPLOYMENT IN NORTH WESTERN MEDITERRANEAN SEA

The chosen sites for this HF radar network have been identified in order to cover the regions of interest for the MOOSE program (Fig. 1.). The main difficulties for deploying HF radars lie in the hardware costs, the frequency licenses, and the site finding, especially when considered coast is irregular and steep or close to touristic and crowded regions.

The first target area off the coast of Toulon (ANTARES) is a key zone conditioning the behavior of the North Current (NC) downstream of the Gulf of Lions, and the exchanges across the shelf edges. This fully operational site is monitored by two Wellen Radar (WERA [Gurgel et al., 1998, 219-234]) systems manufactured at Helzel Messtechnik GmbH and provide real-time data. The first radar system has been installed at the Cap Sicié in 2010 and works in monostatic configuration. In May 2012 it has been complemented with a second radar system working in bistatic configuration, with a receiver located at Cap Bénat and a transmitter on Porquerolles Island. This specific configuration has required some new processing adapted for bistatism ( [START_REF] Barbin | High Resolution Surface Currents Mapping using Direction Finding Method in Bistatic Radar Configuration[END_REF]). It also allowed us to study the bistatism effects on the HF doppler spectra in realistic conditions and it shows good relevance for the purpose of wave spectrum inversion ( [START_REF] Grosdidier | Simulation of HF bistatic ocean radar system in experimental conditions[END_REF]). The upcoming implementation of a second HFSWR site, by the end of the year 2013, in the Ligurian area (DYFAMED) will extent the radar observation to the full coastal area between Toulon and Nice. This should allow to monitor seasonal and high frequency variability of the current across the North front and its interactions with the coastal circulation in the vicinity of the reference sites. The selected equipment to cover the DYFAMED area is a pair of more compact HF radar system, namely two SeaSondes from CODAR Ocean Sensors ( [START_REF] Barrick | CODAR: A coastal HF radar for real-time current mapping[END_REF]).

The ever-increasing deployment of HFSW radars has led the community to look for new rules for frequency sharing. Our radars follow the ITU recommendations and operate in the frequency sub-band specified for oceanographic purposes, within only half of the hundred kHz ITU sub-bands.

FIRST RESULTS AND APPLICATIONS

HF radar-based measurements can provide a good description of the variability of the Northern current and are key element of the observatory network, which also includes also gliders and moored lines.

In the first step of the ANTARES implementation (2010-2011), one single radar was working at Peyras site and could only provide one radial component of the Northern Current. During this period, prior to the complete installation of the system with the second bistatic component Porquerolles-Bénat, even if it could provide only a partial information, the Vortex Identification Method (VIM) was successfully tested and revealed some eddy-like structures ( [START_REF] Marmain | Derivation of ocean surface current properties from a single-site HF/VHF radar[END_REF][Marmain et al., , 1967[Marmain et al., -1979]]). During the PHYOCE campaign (march 31 st -april 3 rd 2011), the radial velocities field from the one single radar allowed to described in surface the variability of the current flow and was used in complement to in-situ measurement to confirm the existence of coastal eddies acting at mesoscales which match with the numerical model of circulation GLAZUR-64 ([Guihou et al., 2013, 793-808]). This leads that radar data assimilation is now conceivable.

Full vector current maps are now available since 2012. First results, as shown in Fig. 2., confirm that radar measurements of surface currents are in good agreement with the structure revealed by the sea surface temperature remote sensed and are some good indicators of hydrodynamics structure. The radar data put in evidence the meso-scale structures and the interruption of the Northern current due to strong wind episodes ( [START_REF] Bellomo | Observational evidence of mesoscale variability of the Northern Current (North-Western Mediterranean Sea): a combined study via gliders, HF RADAR, surface drifters, and vessel data[END_REF]).

During the TOSCA (MedProgram) campaign, a comprehensive data set of surface radial currents measured by HFSWR, surface drifter trajectories, and gliders was collected. The data gathered by the project have been combined into a web based decision tool designed for authorities in charge of maritime crisis. The system provide critical data and applications, as the visualization of the surface currents and dispersion of an oil spill.

The potential of this real-time observation lies also through the data assimilation, as it can correct the baroclinic oceanic forcings and improve the surface currents ( [START_REF] Marmain | Optimization of boundary conditions of a North Western Mediterranean coastal zone using HF radar measurements[END_REF]).

CONCLUSION

A network of HF radar is currently being deployed by the MIO. It should be very helpful to provide long-term current data of the French Mediterranean coastal area in the context of the MOOSE program. First results based on the already operated radar site are very promising and provide real time maps of the current vector. The HFSWR data can be viewed in real time on http://hfradar.univ-tln.fr

As the radar data are provided almost in real time, it gives the ability to schedule a scenario to have a precise sampling of the hydrodynamic structure with in-situ instrument (drifters, gliders or ADCP) deployed on asking. During the TOSCA project, which intends to optimize the response to marine accidents in Mediterranean sea, we demonstrate that the radar data assimilation represents a great advantage to describe with more accuracy surface currents.

HFSWR is a relevant tool to study the coastal dynamic circulation. HFSWR network needs to be deployed to have a permanent focus on the sea surface circulation and its variability. The measurements could also be integrated into crisis management system. For this aim, it is important that the HFSWR network is constantly maintained and monitored.

Fig. 1 .

 1 Fig. 1. Map of the HFSWR sites: #1 ANTARES-TOULON, #2 DYFAMED/Ligure.On site 1 ANTARES: the configuration is one monostatic radar at Cap Sicié (Peyras), one standalone transmitter on Porquerolles island, and its receiver at Cap Bénat (18 km far away). On site 2 DYFAMED: it will be covered with two radar seasondes, one located at Cap Ferrat, and the other at Dramont. The arc of circles show the approximate radar coverage area of each system

Fig. 2 .

 2 Fig. 2. On the top, the two radial velocity maps in color scale from (a) on right Peyras, (b) on left Porquerolles-Bénat. Positive values are going to the radar, and negative are coming from the radar. On the bottom (c), the combination of the two radial maps gives the surface currents (black arrows) measured by HFSWR and the background image is the sea surface temperature (colored pixels product from "MyOcean": http://www.myocean.eu.org/). This illustrates a flow disturbed by the presence of a cyclonic vortex south of the North current

ACKNOWLEDGMENT

The National Institute for Earth Science and Astronomy (INSU) of CNRS supports MOOSE with the Alliance ALLENVI on behalf of the French research organizations on the environment. The first deployments of HF radar around Toulon was made possible through the contribution of national programs whose LEFE IDAO/ECCOP and by TOSCA (Tracking Oil Spills & Coastal Awareness network), a project cofinanced by the European Regional Development Fund in the framework of the MED Program.