Pierre-Louis Curien

Sequential algorithms as bistable maps

We exhibit Cartwright-Curien-Felleisen's model of observably sequential algorithms as a full subcategory of Laird's bistable biorders, thereby reconciling two views of functions: functions-as-algorithms (or programs), and functions-as-relations. We then characterize affine sequential algorithms as affine bistable functions in the full subcategory of locally boolean orders.

Introduction

This paper reconciles two views of functions: functions-as-algorithms (or programs), and functions-as-relations. Our functions-as-algorithms are the observably sequential algorithms on sequential data structures of Cartwright, Curien and Felleisen [START_REF] Cartwright | Observable sequentiality and full abstraction[END_REF][START_REF] Cartwright | Fully abstract semantics for observably sequential languages[END_REF][START_REF] Curien | On the symmetry of sequentiality[END_REF], and our functions-as-relations are Laird's bistable and pointwise monotonous functions on bistable biorders [START_REF] Laird | Bistability: an extensional characterization of sequentiality[END_REF]. We exhibit a full embedding from the former to the latter.

Since the moment when the first version of these notes has circulated privately, Laird has further improved the understanding of the connection by defining a full sub-category of bistable biorders, the category of locally boolean domains, whose intensional behaviour may be "synthesized" through decomposition theorems. A consequence of these theorems is that every locally boolean domain is isomorphic to a sequential data structure. Hence the results presented here actually yield an equivalence of categories (and another one between the respective subcategories of affine morphisms).

In order to make the paper relatively self-contained, we provide the necessary definitions in sections 2 and 3. The main full embedding result is proved in section 4, and the affine case is addressed in section 5.

Sequential data structures

We define sequential data structures, which are concrete descriptions of partial orders whose elements are called strategies (there is indeed a game semantical reading of these structures, see e.g. [START_REF] Curien | On the symmetry of sequentiality[END_REF]). 1 Definition 2.1 A sequential data structure (sds) [START_REF] Amadio | Domains and Lambda-calculi[END_REF] is a triple S = (C, V, P ), where

• C is a set of cells,
• V is a set of values (C and V disjoint),

• P is a prefix-closed set of non-empty alternating sequences c 1 v 1 c 2 . . . (with the c i 's in C and the v i 's in V ), which are called positions,

• Q (resp. R) is the subset of sequences of odd (resp. even) length of P , which are called queries (resp. responses).

One moreover assumes two special values ⊥ and ⊤, not in V (nor in C) (in earlier work [START_REF] Cartwright | Fully abstract semantics for observably sequential languages[END_REF], ⊤ was called error, and in ludics [START_REF] Girard | Locus Solum[END_REF] it is called demon). We let w range over V ∪ {⊥, ⊤}.

Definition 2.2 A strategy is a set x ⊆ R ∪ {q⊤ | q ∈ Q} ∪ {q⊥ | q ∈ Q}
which satisfies the following properties:

• x is closed under (even length) prefixes,

• whenever qw 1 , qw 2 ∈ x, then w 1 = w 2 ,

• whenever r ∈ x, then for all c such that rc ∈ Q, there exists w such that rcw ∈ x.

The second condition is the crucial one: it tells that queries are answered uniquely in a strategy. The other conditions are there for technical convenience.

Here is a syntax for the strategies of a sds:

rc ∈ Q c⊥ : strat(rc) rc ∈ Q c⊤ : strat(rc) rc 0 v 0 ∈ R x c : strat(rc 0 v 0 c) (rc 0 v 0 c ∈ Q) c 0 v 0 {x c | rc 0 v 0 c ∈ Q} : strat(rc 0 ) x c : strat(c) (c ∈ Q) {x c | c ∈ Q} : strat A strategy is a set x = {x c | c ∈ Q} : strat.
The strategy-as-set-of-responses associated to a strategy-as-term is defined as {r | r ∈ x}, where r ∈ x is defined by the following rules:

c⊥ ∈ c⊥ c⊤ ∈ c⊤ r 1 ∈ x c 1 c 0 v 0 r 1 ∈ c 0 v 0 {x c | rc 0 v 0 c ∈ Q} c 0 v 0 ∈ c 0 v 0 {x c | rc 0 v 0 c ∈ Q} r ∈ x c r ∈ {x c | c ∈ Q}
This defines an injection, whose image is easily seen to be the set of strategies x that do not have any infinite branch, in the sense that there is no sequence

c 1 v 1 c 2 v 2 . . . c n v n . . .
whose even prefixes all belong to x. We shall call such strategies finitary.

We denote the set of strategies by D ⊤ (S), and we use D(S) for the set of strategies obtained by removing the rule introducing c⊤. We write:

• q ∈ A(x) if q⊥ ∈ x, • q ∈ F (x) if qv ∈ x for some v ∈ V or if q⊤ ∈ x, and
• x < q y when q ∈ A(x) and q ∈ F (y).

If q 1 = r 1 c 1 , . . . , q n = r n c n ∈ A(x), we denote by x[q 1 ← x 1 , . . . , q n ← x n ] the strategy obtained by replacing c i ⊥ by x i : strat(q i ), for all i, in x. We shall abbreviate q = rc ← c⊥ as q ← ⊥, and similarly with ⊤. We shall use the convention that writing x = x[q 0 ← ⊥, . . . , q n ← ⊥] means that A(x) = {q 0 , . . . , q n }.

Definition 2.3

We define four orders ≤ s (stable), ≤ c (costable) , ≤ (bistable), and ⊑ (pointwise) as the congruence closures of, respectively:

for ≤ s : rc ∈ Q x ∈ strat(rc) c⊥ ≤ s x for ≤ c : x ∈ strat(rc)
x ≤ c c⊤ for ≤:

rc ∈ Q c⊥ ≤ c⊤ for ⊑: rc ∈ Q x ∈ strat(rc) c⊥ ⊑ x rc ∈ Q x ∈ strat(rc)
x ⊑ c⊤

By congruence closure, we mean, say for ⊑, the following rules:

rc 0 v 0 ∈ R x c ⊑ y c (rc 0 v 0 c ∈ Q) c 0 v 0 {x c | rc 0 v 0 c ∈ Q} ⊑ c 0 v 0 {y c | rc 0 v 0 c ∈ Q} x c ⊑ y c (c ∈ Q) {x c | c ∈ Q} ⊑ {y c | c ∈ Q}
In words, replacing a ⊥ by a (correctly typed) tree results in a stable increase, while removing a subtree and replacing it by ⊤ results in a costable increase. The bistable order is the intersection of the stable and the costable order: an increase in this order consists only in changing ⊥'s to ⊤'s. The bistable order turns out to play a crucial role in the axiomatization (see section 3). The pointwise order is the order generated by the union of the stable and the costable orders.

Streicher has remarked that ⊑ and ≤ make an sds a bistable biorder. This is an easy check left to the reader (after reading of section 3). Here, we extend this to a full and faithful embedding of the category of sds's and sequential algorithms into the category of bistable and ⊑-monotonous maps. Therefore, we now move on to define the relevant categories [START_REF] Amadio | Domains and Lambda-calculi[END_REF][START_REF] Laird | Bistability: an extensional characterization of sequentiality[END_REF]. Definition 2.4 Given sets A, B ⊆ A, for any word w ∈ A * , we define w⌈ B as follows:

ǫ⌈ B = ǫ (wm)⌈ B = w⌈ B if m ∈ A\B (w⌈ B )m if m ∈ B .
Definition 2.5 Given two sds's S = (C, V, P ) and S ′ = (C ′ , V ′ , P ′ ), we define S ⊸ S ′ = (C ′′ , V ′′ , P ′′ ) as follows. The sets C ′′ and V ′′ are disjoint unions:

C ′′ = C ′ ∪ V V ′′ = V ′ ∪ C .
P ′′ consists of the alternating positions s starting with a c ′ , and which are such that: s⌈ S ′ ∈ P ′ , (s⌈ S = ǫ or s⌈ S ∈ P ), and s has no prefix of the form scc ′ .

The strategies of S ⊸ S ′ are called observably affine sequential algorithms from S to S ′ .

A typical response of S ⊸ S ′ is thus of the form

c ′ c 1 v 1 . . . c n v n v ′ ,
and reads as follows: the initial query c ′ of the output prompts a query c 1 to the input. If the answer to this query is v 1 , then the strategy wants to further explore the input and asks the query c 1 v 1 c 2 , and so on, until enough of the input is known to answer the query c ′ .

We next move on to define observably sequential algorithms (not necessarily affine). Our model follows linear logic's decomposition S → S ′ = (!S) ⊸ S ′ [START_REF] Girard | Linear logic[END_REF]. The decomposition for sequential algorithms on sequential data structures was discovered by Lamarche [START_REF] Lamarche | Sequentiality, games and linear logic[END_REF][START_REF] Curien | On the symmetry of sequentiality[END_REF]. Definition 2.6 (exponential -sds) Let S = (C, V, P ) be a sds. The following recursive clauses define a set P ! of alternating words over Q ∪ R = P :

(r = ǫ or r ∈ P ! ) q ∈ A(state(r)) rq ∈ P ! q ∈ P ! and state(qr) ∈ D(S) qr ∈ P !
where state is the following function mapping responses (or ǫ) of P ! to strategies of M:

state(ǫ) = {c⊥ | c initial} q = r 1 c 1 r = qv 1 state(rqr) = state(r)[q ← c 1 v 1 {c⊥ | rc ∈ Q}] The sds (Q, R, P ! ) is called !S.
The above definition looks technical, but it just amounts to say that the cells and values of !S are the queries and the responses of S, and that the queries and responses of !S are sequences obtained from some tree traversal of the strategies of S. This is in spirit similar to the coherence space semantics of linear logic [START_REF] Girard | Linear logic[END_REF]. Definition 2.7 Given two sds's S and S ′ , the strategies of !S ⊸ S ′ are called observably sequential algorithms from S to S ′ .

Despite their appearance, observably sequential algorithms are (in bijection with) functions: this key insight did not wait for Laird's work, and was indeed one of the contributions of Cartwright and Felleisen [START_REF] Cartwright | Observable sequentiality and full abstraction[END_REF][START_REF] Cartwright | Fully abstract semantics for observably sequential languages[END_REF][START_REF] Amadio | Domains and Lambda-calculi[END_REF] to the older work of Berry and Curien on sequential algorithms on concrete data structures [START_REF] Berry | Sequential algorithms on concrete data structures[END_REF]. Definition 2.8 Let f be an observably sequential algorithm from S to S ′ and x an observable strategy of S. We define f • x (also written f (x)) as the normal form of f | | x for the following rewriting system, which is easily seen to be confluent (no critical pairs) and terminating on finitary strategies.

c ′ v ′ {x ′′ i | i ∈ I} | | x → c ′ v ′ { x ′′ i | | x | i ∈ I} c ′ ⊥ | | x → c ′ ⊥ c ′ ⊤ | | x → c ′ ⊤ c ′ q{x ′′ r | r ′′ c ′ qr ∈ Q ′′ } | | x → c ′ ?( x ′′ r 0 | | x ) (r 0 ∈ x) (in strat(r ′′ c ′ )) c ′ q{x ′′ r | r ′′ c ′ qr ∈ Q ′′ } | | x → c ′ ⊥ (q⊥ ∈ x) (in strat(r ′′ c ′ )) c ′ q{x ′′ r | r ′′ c ′ qr ∈ Q ′′ } | | x → c ′ ⊤ (q⊤ ∈ x) (in strat(r ′′ c ′ )) r 0 q{x ′′ r | r ′′ r 0 qr ∈ Q ′′ } | | x → x ′′ r 1 | | x (r 1 ∈ x) (in strat(r ′′ r 0 )) ?( r 0 q{x ′′ r | r ′′ r 0 qr ∈ Q ′′ } | | x ) → ⊥ (q⊥ ∈ x) (in strat(r ′′ r 0 )) ?( r 0 q{x ′′ r | r ′′ r 0 qr ∈ Q ′′ } | | x ) → ⊤ (q⊤ ∈ x) (in strat(r ′′ r 0 )) ?( rv ′ {x ′′ i | i ∈ I} | | x ) → v ′ { x ′′ i | | x | i ∈ I} ?( r⊥ | | x ) → ⊥ ?( r⊤ | | x ) → ⊤ For example, if c ′ c 1 v 1 . . . c n v n v ′ c ′ 1 c v v ′ 1 ∈ f and c 1 v 1 . . . c n v n c v ∈ x, then c ′ v ′ c ′ 1 v ′ 1 ∈ f • x.
(The reader should have in mind here that potentially f (resp. x) branches after c 1 , . . . , c n , c (resp. after v 1 , . . . , v n ), and that the strategies's choices determine alternately which branch to choose.) Definition 2.9 Let S and S ′ be two sds's. A ≤ s -monotonous function f : D ⊤ (S) → D ⊤ (S ′ ) is called sequential at x if for any q ′ ∈ A(f (x)) one of the following properties hold:

1. ∀ y ≥ s x q ′ ∈ F (f (y)).

∃ q

∈ A(x) ∀ y > x (f (x) < c ′ f (y) ⇒ x < c y).
A query q satisfying condition (2) is called a sequentiality index of f at (x, q ′ ). The index is called strict if (1) does not hold. If (1) holds, then any q in A(x) is a (vacuous) sequentiality index.

If q is a sequentiality index at (x, q ′ ) and if moreover q ′ ⊤ ∈ f (x[q ← ⊤]), then we say that f is observably sequential at x, q ′ , with index q (note then that the index is strict and that there can be no other sequentiality index).

The function f is called sequential (resp. observably sequential) from S to S ′ if it is sequential (resp. observably sequential) at all points.

With the notation introduced above and using the ≤ s monotonicity, we can rephrase the definition more symmetrically as follows, at x = x[q 1 ← ⊥, . . . , q n ← ⊥]:

∀x 1 , . . . , x i-1 , x i+1 , . . . , x n q ′ ⊥ ∈ x[q 1 ← x 1 , . . . q i-1 ← x i-1 , q i ← ⊥, q i+1 ← x i+1 , . . . , q n ← x n ] ∀x 1 , . . . , x i-1 , x i+1 , . . . , x n q ′ ⊤ ∈ x[q 1 ← x 1 , . . . q i-1 ← x i-1 , q i ← ⊤, q i+1 ← x i+1 , . . . , q n ← x n ]
Or, alternatively, using instead the ⊑-monotonicity (which is established below), we get the following quantifier-free definition:

q ′ ⊥ ∈ x[q 1 ← ⊤, . . . q i-1 ← ⊤, q i ← ⊥, q i+1 ← ⊤, . . . , q n ← ⊤] q ′ ⊤ ∈ x[q 1 ← ⊥, . . . q i-1 ← ⊥, q i ← ⊤, q i+1 ← ⊥, . . . , q n ← ⊥]
Theorem 2.10 Observably sequential algorithms and observably sequential functions are in one-to-one correspondence, and under the bijection, the pointwise (resp. the stable) (resp. the bistable) ordering defined above indeed becomes the pointwise ordering (resp. Berry's stable ordering [START_REF] Berry | Stable models of typed lambda-calculi[END_REF]) (resp. Laird's bistable ordering [START_REF] Laird | Bistability: an extensional characterization of sequentiality[END_REF]):

f ⊑ g ⇔ (∀ x f • x ⊑ g • x) f ≤ s g ⇔ (f ⊑ g and (∀ x, y (x ≤ s y ⇒ f (x) = f (y) ∧ s g(x)))) f ≤ g ⇔ (f ⊑ g and (∀ x, y (x ≤ y ⇒ f (x) = f (y) ∧ g(x)
) and g(y) = f (y) ∨ g(x)))

(the notation ∧ s denotes the greatest lower bound with respect to the stable ordering).

Proof. Except for the last equivalence, the theorem is proved in [START_REF] Cartwright | Fully abstract semantics for observably sequential languages[END_REF]. We check here only that if f, g are observably sequential, f ≤ g, and x ≤ y, then g(y) = g(x) ∨ f (y). Suppose that g(y) > g(x) ∨ f (y). Let q ′ filled in g(y) and accessible from g(x) ∨ f (y). It follows that q ′ is accessible from g(x) and from f (y). The only way for g to make the difference w.r.t. f on input y is to use one of its additional ⊤'s, say, q ′ ⊤, in the interaction with y. More precisely, one of the ⊤'s of g is responsible for the filling of q ′ . But the interaction of g with y is the same as with x. Hence q ′ must be filled in g(x), contrarily to our assumption.

As an illustration of what is going on, suppose that f 1 , f 2 : S → S ′ are ≤ s -minimal observably sequential algorithms such that

c ′ c 1 (c 1 v 1 ) c 2 (c 2 v 2 ) c ∈ f 1 c ′ c 2 (c 2 v 2 ) c 1 (c 1 v 1 ) c ∈ f 2
It looks like f 1 and f 2 define the same function (and indeed they do define the same function from D(S) to D(S ′ )), but on x = {c 1 ⊥, c 2 ⊤} we have:

f 1 • x = {c ′ ⊥} f 2 • x = {c ′ ⊤}
Here, both ⊥ and ⊤ act very much like colors used in chemical experiments: they track the presence of a proper value in c 1 and c 2 , respectively. The special values ⊥ and ⊤ play entirely symmetric role as long as no infinite computations take place.

If we allow general, non finitary strategies, the abstract machine of definition 2.8 may well diverge (i.e. not terminate). Following Scott-Ershov's tradition, a non-terminnating computation receives ⊥ as value, and then ⊥ and ⊤ cease to be symmetrical, since ⊥ has become overloaded: it is both a symbol for non-termination, and an explicit symbol for a special error value that could be called "stop by lack of information". The other error value ⊤ could be called "deliberate stop" (see [START_REF] Curien | Symmetry and interactivity in programming[END_REF][START_REF] Girard | Locus Solum[END_REF][START_REF] Curien | Introduction to Linerar logic and ludics, parts I and II[END_REF]).

Bistable biorders

So far, so good: we have a charaterization of our notion of functions-as-algorithms as functions-as-relations. But still, the definition of sequential function (originally due to Kahn and Plotkin [START_REF] Kahn | Concrete domains[END_REF]) requires a rather concrete, "algorithmic" definition of domain (here, sequential data structures). We can get rid of this too, using Laird's notion of bistability, which can be defined more abstractly. In this section, we recall Laird's definitions [START_REF] Laird | Bistability: an extensional characterization of sequentiality[END_REF]. Definition 3.1 A bistable biorder is a set (D, ≤, ⊑) equipped with two partial orders, such that whenever x, y have a lower or an upper bound for ≤ then x ∨ y and x ∧ y exist (for ≤), and then x ∨ y = x ⊔ y and x ∧ y = x ⊓ y, i.e. the two orders coincide for ≤-connected components. Moreover ∧ and ∨ distribute over each other in each component. One writes x y when x, y have a ≤-upper bound (or equivalently a ≤-lower bound). A bistable function is a ≤-monotonous function such that for any x y:

f (x ∧ y) = f (x) ∧ f (y) f (x ∨ y) = f (x) ∨ f (y)
(we refer to the two halves of this property as ∧-bistability and ∨-bistability, rexpectively).

We observe (for the reader with some linear logic culture) that the preservation of ∨ in the above definition is not a requirement of linearity, as it is taken with respect to ≤, not ≤ s .

In [START_REF] Laird | Bistability: an extensional characterization of sequentiality[END_REF] the following theorem is proved:

Proposition 3.2
The category of bistable biorders and bistable and ⊑-monotonous functions is cartesian closed.

Full embedding

From now on, for simplicity, we limit ourselves to finite strategies.. Clearly, the finite strategies are the finitary strategies x with finite branching, i.e. such that

∀ r ∈ x {rc | rc ∈ Q} is finite .
Of course, if the sds is finite, i.e. has only finitely many cells, values, and positions, then all strategies are finite.

In this section, we show that the category of observably sequential algorithms embeds fully in Laird's category of bistable biorders and bistable and ⊑-monotonous functions. This amounts to the following proposition: Theorem 4.1 Given two sds's S and S', a function f : D ⊤ (S) to D ⊤ (S ′ ) is observably sequential if and only if it is bistable and ⊑-monotonous.

Proof. The proof of (f ⊑-monotonous and bistable ⇒ f sequential) follows the steps of (and generalizes) Laird's proof of this property at x = ⊥ [START_REF] Laird | Bistability: an extensional characterization of sequentiality[END_REF]. Suppose that q ′ is accessible from f (x) (with x = x[q 0 ← ⊥, . . . , q n ← ⊥]), and suppose moreover that none of the q i 's is a sequentiality index. Then by ⊑ monotonicity we have that q ′ is filled in all of the f (x[q 0 ← ⊤, . . . , q i-1 ← ⊤, q i ← ⊥, q i+1 ← ⊤, . . . , q n ← ⊤]). By ≤-monotonicity it is also filled in f (x[q 0 ← ⊤, . . . , q n ← ⊤]), and hence it is filled with the same value in all of the f (x[q 0 ← ⊤, . . . , q i-1 ← ⊤, q i ← ⊥, q i+1 ← ⊤, . . . , q n ← ⊤]). Now, by ∧-bistability, it should also be filled in f (x) since x = i=1...n

x[q 0 ← ⊤, , . . . , q i-1 ← ⊤, q i ← ⊥, q i+1 ← ⊤, . . . , q n ← ⊤] .

We show that if f is ⊑-monotonous and bistable, then it is observably sequential. That is, we have to show that if f has, say, q 0 as sequentiality index at (x, q ′ ), then q ′ ⊤ ∈ f (x[q 0 ← ⊤]). Suppose not. Then, if y is such that x ≤ s y and q ′ is filled in f (y), we have y ⊑ y[q 0 ← ⊤] and x[q 0 ← ⊤] ≤ y[q 0 ← ⊤]. Since by pointwise monotonicity q ′ is filled in f (y[q 0 ← ⊤]), there exists a sequentiality index q 1 for f at (x[q 0 ← ⊤], q ′ ). Continuing in this way, we would exhaust all the ⊥'s of x. So we get that q ′ is filled in, say, f (x[q 0 ← ⊤, q 1 ← ⊤, . . . , q n ← ⊤]), and hence by ∨-bistability in one of the f (x[q i ← ⊤]). But it cannot be an i > 0 since q 0 is a sequentiality index at x, hence it is i = 0, which contradicts the assumption.

Conversely, if f observably sequential, we first show that f is ⊑-monotonous. It is enough to check that if x ≤ c y then f (x) ≤ c f (y). To show this -actually, the natural thing to show is that more generally if f ≤ c g and x ≤ c y then f (x) ≤ c f (y) -, we extend the definition of ≤ c by congruence to all the terms involved in the rewriting system of Definition 2.8. It is straightforward to show, for each of the rules of the rewriting system, that if t ≤ c t ′ and t ′ → t ′ 1 then there exists t 1 such that t → t 1 . Informally, the only difference of behaviour is that g | | y might terminate before f | | x , because of a new ⊤ in g or y. Notice that this argument is the same as the one used in the separation theorem of ludics (and, by the way, Girard's designs also form a bistable biorder) [START_REF] Girard | Locus Solum[END_REF][START_REF] Curien | Introduction to Linerar logic and ludics, parts I and II[END_REF].

Finally, we show that if f is observably sequential then it is bistable. One proves that f is ≤-monotonous much in the same way as for ⊑-monotonicity. The argument for ∧bistability is standard. One proves actually the preservation of all ≤ s compatible binary ≤ s glb's. Suppose that x, y ≤ s z and f (x ∧ s y) < s f (x) ∧ s f (y). Let q ′ be accessible from f (x ∧ s y) and filled in f (x) and f (y). Let q be a sequentiality index at x ∧ s y, c ′ . Then by sequentiality q is filled in both x and y, and with the same value since x, y have a ≤ s upper bound. But then q is also filled in x ∧ s y, contrarily to the assumption. This shows a fortiori ∧-bistability since x y implies a fortiori that x, y have a ≤ s -upper bound, and that x ∧ y = x ∧ s y.

As for ∨-bistability, suppose that f (x) ∨ f (y) < f (x ∨ y). Let q ′ be accessible from f (x) ∨ f (y) and filled in f (x ∨ y). Then q ′ must be already accessible from f (x ∧ y), as the order ≤ does not add new queries. Let q be the sequentiality index for q ′ at x ∧ y. Then we have that q is filled in x ∨ y by sequentiality, i.e. it is filled in either x or y, say, in x. By definition of ≤, since q is accessible from x ∧ y, q must be filled with ⊤ in x. But then q ′ is filled with ⊤ in f (x) (and a fortiori in f (x ∨ y)), by observable sequentiality: contradiction. Proof. This is an easy corollary of theorem 4.1, proposition 3.2, and theorem 2.10. Indeed, all we have to check for a full subcategory of a cartesian closed category to be itself cartesian-closed is that the (product and) function space construction of the larger category, when applied to objects of the smaller, yields an object of the smaller. Laird's function space D(S) → D(S ′ ) is the set of bistable and ⊑-monotonous functions, equipped with the pointwise and bistable orderings, which is isomorphic to D(S → S ′ ).

A direct proof of proposition 4.2 is given in [START_REF] Cartwright | Fully abstract semantics for observably sequential languages[END_REF], but it is more complicated than the proof of proposition 3.2.

We end the section by briefly sketching what adjustments have to be made to remove the finiteness restriction (both in this section and in the following one). This is rather standard domain theory: bistable biorders have to be directed complete, and bistable functions have to be Scott-continuous. We refer to [START_REF] Laird | Bistability: an extensional characterization of sequentiality[END_REF] for the relevant definitions. With a little care, all our arguments go through, making use of the continuity assumption. For example, to prove observable sequentiality, we used the finiteness assumption when writing this paper for the definition, which takes as primitive an operation of involution which in terms of sds's consists in exchanging ⊥' with ⊤'). In fact, as Laird shows by means of elegant abstract decompositions, every locally boolean domain is isomorphic to a sds, so that we end up with an equivalence (actually two equivalences) of categories.

Proposition 5.3 The categories of sds's and (observably) sequential algorithms and of locally boolean domains and ⊑-monotonous and bistable functions are equivalent. This equivalence cuts down to an equivalence between the respective subcategories of affine morphisms (Definitions 2.5 and 5.1).

Proof. Propositions 4.1 and 5.2 have established full embeddings. The equivalence of categories follows from the fullness on objects of the functors co-restricted to locally boolean domains.

Since both in [START_REF] Lamarche | Sequentiality, games and linear logic[END_REF][START_REF] Curien | On the symmetry of sequentiality[END_REF] and [START_REF] Laird | Locally boolean domains[END_REF] the comonads leading to models of (affine) linear logic are defined as adjoint to the inclusion functor, the two linear decompositions are the same up to isomorphism. In other words, Laird's work provides completely a traditional domain theory account of Berry-Cartwright-Curien-Felleisen-Lamarche's sequential algorithms model of (affine) linear logic.

Finally, we mention two properties which add to the ambiant symmetry: The proofs are not difficult and are in the same vein as the ones given above.

Conclusion

We should note that a restricted version of the full embedding was proved indirectly in Laird's paper [START_REF] Laird | Bistability: an extensional characterization of sequentiality[END_REF]: he proves that the bistable model is fully abstract for the language Λ ⊤ ⊥ (the simply typed λ-calculus with a single base type, and two constants ⊥ and ⊤ of base type). This calculus is essentially the same as Cartwright-Curien-Felleisen's language SPCF with respect to which the model of sequential algorithms is fully abstract [START_REF] Cartwright | Fully abstract semantics for observably sequential languages[END_REF]. Hence, by uniqueness up to isomorphism of fully abstract models, the two models are isomorphic on the simply typed hierarchy. Our result is more general and does not refer to (the interpretation of) types.

As for every correspondence result, there are mutual benefits in the equivalence that we have proved. The algorithmic side provides an operational explanation of the various orders. The abstract domain-theoretic side provides simpler proofs sometimes (for example, of cartesian closedness), and opens the way to extend the coverage of standard domain-theoretic tools for reasoning about sequential languages. Current work of Laird goes in that direction.

Proposition 4 . 2

 42 The category of sds's and observably sequential algorithms is cartesian closed.

Proposition 5.4 1 . 2 .

 12 Observably sequential functions are costable, i.e.: ∀x, y (∃z z ≤ c z and z ≤ c y) ⇒ f (x ∨ c y) = f (x) ∨ c f (y) Affine observably sequential functions are coaffine, i.e. : ∀x, y (∃z z ≤ c z and z ≤ c y) ⇒ f (x ∧ c y) = f (x) ∧ c f (y)

x = x[q 0 ← ⊥, . . . , q n ← ⊥], with n finite. If instead we have x = x[q 0 ← ⊥, . . . , q n ← ⊥, . . . , ] ,

then the proof of sequentiality goes through because by continuity the ∧-bistability extends to preservation of greatest lower bounds of arbitrary subsets of a -component. For the proof of observavle sequentiality, the finiteness of n was essential. But continuity saves us again: by continuity, we can take x, y finite, and we need only care about the q j 's which are filled in y, which are finitely many.

Affine decomposition

In this section, we prove that affine sequential algorithms can also be defined as observably sequential functions that are affine with respect to the stable order, and hence as affine bistable and ⊑-monotonous functions (provided this makes sense, see below). Definition 5.1 An affine function is a function that preserves stable upper bounds of stably compatible elements.

(The difference with linear functions, which may be more familiar to the linear logic oriented reader, is that preservation of ⊥ is not required.) Proposition 5.2 Affine sequential algorithms are in order-isomorphic correspondence with affine observably sequential functions.

Proof. Let f be a sequential algorithm which is not affine. It contains at least a query of the form r c ′ q 1 r 1 q 2 , where r 1 is not a prefix of q 2 . Let x be the input strategy read off along the path from the root up to q 2 . Formally, x = state(r), where r is the projection of r c ′ q 1 r 1 on the input sds. Let y = (x \ {r 1 }) ∪ {q 2 ⊤}. Let q ′ be the projection of rc ′ on the output sds. Then q ′ is filled neither in f (x) nor in f (y), but is filled (with ⊤) in f (x ∨ s y). Conversely, suppose that f is an affine sequential algorithm, and let q ′ w ′ ∈ f (x ∨ s y). Let s be the position of f visited along the normalisation against x ∨ s y towards q ′ w ′ (it is obtained by travelling in f from the root starting with the initial move of q ′ , and solving ambiguities using x ∨ s y and q ′ w ′ when going up after a player's move, cf. definition 2.8). Consider the last input response r on this position of f . Then r belongs to either x or y, say x. But all other responses along the path are prefixes of r, by the constraint of affinity, hence all belong to x. Therefore q ′ w ′ ∈ f (x) (or q ′ w ′ ∈ f (y)).

However, bistable biorders are too poor to express the stable ordering. In further work, Laird [START_REF] Laird | Locally boolean domains[END_REF] has defined the full subcategory of locally boolean domains in which not only the pointwise and bistable orders can be defined, but also the stable one [START_REF] Laird | Locally boolean domains[END_REF] (we refer to


Philippe Woloszyn
email: philippe.woloszyn@cerma.archi.fr

FRACTAL SCATTERING INDICATORS FOR URBAN SOUND DIFFUSION

Keywords: Acoustic Diffusion, Scattering, Minkowski Sausage

Irregular surfaces like urban frontages produce an anomalous back-scattered region, creating an acoustic interference field in their neighborhood. Thus, in order to be able to detect that scattered energy's minima and maxima through taking the frontage morphological characterization into account, we propose a new measurement method of the building geometry, with using mathematical morphology techniques. Results of this geometrical approach provide two types of indicators, global and local. The global one, the structure factor of the urban frontage, is related to the multiscale characterization of the whole building geometry through the computation of the spatial Fourier transform of the scatterers. The complementary local indicator evaluates the vertex multiscale densitometrical distribution at each incidence angle, provided through a fractal evaluation technique, the Minkowski sausage. This densitometry computation reveals the characteristic directions of scattering, which has to be calculated through the scattering pressure function along the lateral active diffraction zone.

Introduction: Problematic and purpose

The exterior frontage of a typical urban building does not reflect noise in a purely specular manner. Because the dimensions of the irregularities (decorative elements, windows, balconies,...) are comparable to the sound wavelengths, the major type of early reflexions on the buildings is scattering, inducing a global diffusion behaviour of sound in an urban street. Consequently, irregular surfaces like urban frontages produces an anomalous back-scattered region, with the creation of an acoustic interference field in its neighborhood. Thus, in order to be able to detect that scattered energy's minima and maxima, we have to take into account both incidence angle and multiscale characterization for diffusive evaluation of urban surfaces through mathematical morphology techniques.

Diffusion through oblique incident wave

A first approximation: the Rayleigh criterion

Historically, the first attempt at determining the scattering amplitudes was made in 1893 by Lord Rayleigh, who assumed a unique solution for the wave equation for the whole boudary of a Λ-corrugated surface [START_REF] Rayleigh | The theory of Sound[END_REF]. Concerning the inferior diffusion limit frequence, Rayleigh's work proposes a phase grating calculation between two acoustic rays related in [START_REF] Beckmann | The Scattering of Electromagnetic Waves from Rough Surfaces[END_REF], which takes into account the source incidence angle. Taking the walk difference ∆d between two rays with wavelength λ and incidence angle α regarding a surface with depth Λ into account provides the following phase grating calculation between the two rays:

∆α = ∆d (2π / λ) = cos α (4 π Λ / λ) (1)
Fractal Scattering Indicators for Urban Sound Diffusion.doc submitted to World Scientific : 10/07/2003 : 18:36 1/10 with the walk difference : ∆d = 2 Λ cos α. For a weak walk difference ∆d, rays are coherent and the acoustic wave is specularly reflected. Increasing of ∆d will interfere rays, till to phase opposition (∆d = π), so that no energy is displayed in the specular direction : sound energy is diffused. Rayleigh criterion defines the limit between specular and diffuse behaviour of an incident source, corresponding to the frontage depth irregularities as : Λ < l / 8 cos α. The specular reflexion zone is defined under the minimal values of the frontages depths irregularities, taking the frequency and the angle of the incident wave into account.

Diffraction densitometry of an indented plane

Following those non-specularity conditions, the propagation directions specified by the unit vectors v(d) = (φ d , 0, γ d ) for a given regular plane division, repeating n times a spatial unit of width Λ are defined as the characteristic directions of scattering associated with the localization length Λ:

α λ α sin 2 sin - Λ = n p d , ( 2 )
where α d is the grazing diffraction angle made by vectors v(d) = (φ d , 0, γ d ) in the direction 0x, with φ d = cos α d and γ d = sin α d , , and p the diffraction order. For Λ = 0, equality between incident and reflected angle remaining true (specular conditions). We can note here that, ignoring the specular component sinα, the first term of the previous equation can be compared to Bragg's Law, leading to the following expression:

, 2 sin d pλ α = ( 3 )
where the integer p is the order of diffraction, d= nΛ, the distance between two reflexion planes, λ, the wavelength of the incident beam and α its incidence angle.

This law, also used in the field of cristallographic diffractometry, enounces the conditions for constructive interference rays, which are producing strong diffraction. When in phase, those reflections lead to constructive interference rays, conditionned with Bragg's Law's equation. For p=1, all planes inside the cosine scatter in phase, providing maximal diffraction. For p=1-Λ, the diffraction cancels.

In the same way, Bragg's law and Rayleigh criterion defines the conditions of interfeering behaviour, for acoustic waves reflected on micrometer or meter-scaled parallel planes. Consequently, the pure diffracted energy part of an urban indented surface can be expressed through Bragg's Law, considering the path difference between two frontage surfaces, as between two crystal planes for the constructive interference conditions: pλ=2nΛ sinα, where nΛ is the frontage indentation depth. Moreover, the two-dimensional polar response of a given indented surface can be expressed through the diffraction orders (p, q), taking the angles of incidence and diffraction into account:

λ α α sin sin 2 2 + Λ = + d n q p ( 4 )
The characteristic directions are those along which the waves emanating from the individual frontage indentation depth Λ are exactly in phase. This constructive interference condition is both conditioned with the adimensional modulus λ / Λ , which quantifies the energy of non-evanescent scattering losses, represented by the area of scattering intensity pattern lobes, and with the previous Bragg's equation pλ=2nΛ sinα. Indeed, this modulus is conditioning the solutions of equation ( 4), as λ / Λ = 0 traduces specular reflection (as the diffraction order p is null through the limit of the diffusion), and as this modulus value conditions its number of real solutions, corresponding to the diffraction directions (lobes of the surface's radiated energy).

Diffraction and structure factor of a multiscale rough boundary surface

For all other directions, the reflected waves will destructively interfere, resulting in complete cancellation for a self-similar periodic structure. For non-or pre-fractal structures as urban frontages, the scattered field will show mainlobes in the characteristic directions, and sidelobes elsewhere for a done sound frequency).

Phase of diffraction

Those interference conditions can be also expressed with defining the phases of the incident wave vector k 0 and the diffracted vector k, which both have an amplitude equal to the reciprocical of the wavelength. In order to calculate the phase of the diffracted wave, taking the path lengths difference ∆d = 2 nΛ cosα into account, we will consider the difference between the path of the sonic particle (phonon) along the incident beam k 0 r and its path along the diffracted beam kr. With expressing this path length difference ∆d = 2 nΛ cosα = k 0 r -kr, the overall diffraction phase will be expressed as -2π (k 0 r -

kr) = 2π (k -k 0 ) r (figure 2).
Fractal Scattering Indicators for Urban Sound Diffusion.doc submitted to World Scientific : 10/07/2003 : 18:36 3/10 Considering rcosα, the component of r in the direction of the diffraction vector s, all points with the same value of sr are lying on a plane perpendicular to vector s, allowing the same diffraction phase (figure 3).

² ² ² ² ² ² 1 c l b k a h d + + = ∆ α cos 2 1 Λ = ( 5 )
where (h, k, l) , the Miller indices, specify the direction and the period of the tridimensional cosine wave cos(2π / [hx/ a + ky/ b + lz/ c]).

Structure factor indications: spatial scattering function

When measuring several phonons located at different points, the diffraction at each point will be the sum of the waves scattered by each phonon. So, the expression of this sum with Euler's equation gives us, for the j th phonon with coordinates (x j , y j , z j ):

) . 2 exp( ) ( ∑ = j j i F r s s π ( 6
)
This wave is represented here by its structure factor, which is the Fourier transform of the scatterers of equal strength on all points of the diffraction plane. Continous expression of this previous equation involves the phonon's density ρ(r) as:

∫ = space dr i F ) 2 exp( ) ( ) ( r s r s π ρ ( 7 )
Fractal Scattering Indicators for Urban Sound Diffusion.doc submitted to World Scientific : 10/07/2003 : 18:36

4/10

As shown through this expression of the structure factor, the diffraction pattern is defined as the Fourier transform of the phonon density.

Taking into account the tridimensional distribution of phonons into the diffusive structure involving Miller indices (h, k, l), as the plane perpendicular to vector s can be written as: sr j = hx j + ky j + lz j , we can afford the previous spatial expression of the structure factor in the three dimensions of space with integrating the tridimensional cosine wave as:

∫∫∫ + + = me PhononVolu hkl dxdydz lz ky hx i z y x F )) ( 2 exp( ) , , ( π ρ (8)
The acoustic field is then expressed through the phonon's density ρ(x, y, z), which is useful to calculation of the mean square diffracted sound pressure P d by the whole volume for a given distance of the structure [START_REF] Makarewicz | Reflexion of noise from a building's facade[END_REF]:

dV P r P V d d 2 2 0 2 cos cos ∫∫∫ = π α α ρ ` (9)
where represents the distance from the receiver to the structure, and P the incident wave pressure. One can remark that the function of the cosine of the angle between the direction of observation and the normal to the surface in the observation point reminds us the Lamberts law [START_REF] Lewers | A Combined Beam Tracing and Radiant Exchange Computer Model of Room Acoustics[END_REF], which is assumed to represent the physical behaviour of sound or light after reflection on an ideally diffusing surface. As mentionned previously, the angular repartition of the sound energy is computed with the Miller indices, involved through the individual phase contributions 0 r

) ( 2 j j j lz ky hx i + + π
, which represents the spatial scattering function of the reference volume V (equation ( 8)).

Dynamic scattering function

This leads us to consider the structure factor as a function of time, called dynamic structure factor, or dynamic scattering function, with introducing time t through a random walk in random environment [START_REF] Hollander | Dynamic Structure Factor in a Random Diffusion Model[END_REF]:

dt t t F ∫ ∞ = 0 ) , ( ) , cos( 2 ) , ( r s ρ ω ω ( 1 0 )
The dynamical density distribution ρ(r,t) can be obtained with the probability for a sonic particle to walk to location r during the time t P(r,t), that remains equation ( 5), with the following relationship [START_REF]Diffusion on self-similar structures[END_REF]:

∫ ∫ ∞ - = 0 ) , ( ) exp( ) exp( ) , ( t P t i dt i dr i r sr s ω ω ρ ( 1 1 )
with P(r,t), describing the sonic particle's probability for a fractional Brownian walk in a non-integer (fractal) D-dimensional space [START_REF] Gouyet | Physique et structures fractales[END_REF], [START_REF] Mandelbrot | Les objets fractals[END_REF]:

∞ → → N t r t t P D , 4 ² exp ) 4 ( 1 ) , ( 2 / δ πδ r ( 1 2 )
where δ is the diffusion coefficient of the D-dimensional structure.

Angular distribution function

This function can be evaluated using a Laplace transform [START_REF] Roman | [END_REF]. After integrating over the angles, we obtain, for the p d th diffraction order:

Fractal

Parceval theorem and diffusion volume

Parceval's theorem formulates that the energy in the frequency domain is the same as the energy in the spatial domain [START_REF] Young | Parceval's Theorem[END_REF]. Consequently, the mean square value on one side of the Fourier transform equation ( 8) is proportional to the mean square value on the other side. So do Perceval's theorem allows to express the phonons density distribution as a transform of the spatial distribution of the surface scatterers. This property allows us to express the angular distribution function as a discreet quadratic summation of elementary structure factors as following:

² 1 )² , , ( ∑ ∫ = hkl hkl V xyz F V dV z y x ρ , ( 1 6 )
Fractal Scattering Indicators for Urban Sound Diffusion.doc submitted to World Scientific : 10/07/2003 : 18:36 6/10

where the diffusion volume V xyz is a ratio between the square root of the discreet quadratic summation of the structure factors and the angular distribution function. This diffusion volume V xyz is experimentally obtained by a mathematical morphological measure using a Minkowski operator, which provides a ribbon surface constituting a neighborhood area, under the condition of continuity [START_REF] Pfeiffer | Fractal BET and FHH theories of adsorption: a comparative study[END_REF].

Considering the Minkowski analysis of a tridimensional structure, scrutated with a structuring element of variable radius Λ, the phonons density-density distribution can be expressed through the roughness autocorrelation of the diffusive structure with involving the diffusion volume V xyz , and the structure factor F hkl , which defines both the global and local behavior of the structure as:

α α ρ sin sin ) , , ( max max 0 2 0 + ∝ = ∑ ∑ Λ Λ d xyz xyz hkl V V F z y x ( 1 7 )
4 Application : a Frontage scattering characterization

The urban frontage model

The spatial configuration we measure here is a numerical 3-D model of a neoclassical frontages of an urban street of Nantes, France, the rue d'Orléans, belonging to a 19 th urban morphology type, with windows, doors, and freestone casting off. One of the main characteristics of this type of architecture is the relative exuberance of its frontage structure, following neo-classical composition. This frontage is considered as a tridimensional object situated in an ortho-normed space, rotating around the Z-axis (Fig. 5):

The Minkowski measurement technique

In order to characterize the scattering behavior of the volume of the frontage, we apply a fractal Minkowski operator, called Minkowski sausage, to evaluate the vertex multiscale densitometry distribution at each incidence angle. This operator consists into replacing each point of the vertexes of the urban geometry with a sphere with variable radius Λ, as seen figure 6:

Fractal Scattering Indicators for Urban Sound Diffusion.doc submitted to World Scientific : 10/07/2003 : 18:36 7/10 This transformation of the urban geometry corresponds to the dilation operation in the morpho-mathematical context [START_REF] Pfeiffer | Fractal BET and FHH theories of adsorption: a comparative study[END_REF]. The union of all spheres is called the 3-D Minkowski sausage. The variation of their diameter gives us successive approached perimeter/surface ratios at each vision angle, which regression evaluates the fractal dimension of the structure, in a specified validity domain.

Frontage fractal measurement

The spatial multiscale evolution of the perimeter-surface ratio P/S defines the profile's Shape spectrum of the frontage [START_REF] Woloszyn | Squaring the circle : diffusion volume and acoustic behavior of a fractal structure[END_REF]. This spectrum defines the multiscale relationship between the radius evolution of the spherical structuring element and the "mass" of the structure, for each the angular measure. As readable in the following figure, the specular domain is illustrated with a strong decrease of the P/S ratio, which corresponds to the limit Λ max for the radius of the structuring element . For this domain, the Euclidean dimension d and the fractal dimension D of the mean structure reach the same value. This break in the frontage indentations shape spectrum behavior occurs for Λ max = 100 cm, for every value of incidence angle α (figure 7): This angular evaluation of the vertexes distribution shows azimutal densitometries due to interreflexions of the corners and the freestone casting along three windows depth, corresponding to the lateral active diffraction zone. Global polar responses for growing localisation lengths shows globally a decreasing diffusivity, revealing a bilobe distribution structure of the biggest scatterers, a cardioid for middle-sized ones and very characteristic peaks for high frequency roughness.

Fractal Scattering Indicators for Urban Sound Diffusion.doc submitted to World Scientific : 10/07/2003 : 18:36 9/10

Conclusion

Through the determination of the structure factor, the Minkowski sausage technique provides a quantification of the scatter distribution function of the indented surface of a specified urban neo-classical frontage at each incidence angle. In order to perform an experimental validation of this model, experimental results will be compared to those indicators at each incidence angle, through an in situ and a 1/10 th scale model MLS multisensor measurement.

With discerning the angular vertex densitomentry of main types of architectures, we will be able to compute their specific angular spatial scattering function for every frequency, directly from the Minkowski analysis of the numerical 3-D model of their geometry. Through those morphological treatment of architectural shapes, this research work will confirm the definition of the diffusion process as a geometrical-dependant phenomenon, influenced by the built structure on urban acoustics.

Fig. 1 .

 1 Fig.1. Rayleigh criterion: Quantification of the dimensional limit between specularity and diffusion, as a function of frequency and incidence angle.

Fig. 2 .

 2 Fig. 2. Phase geometry

Fig. 3 .

 3 Fig. 3. Diffraction geometryConsequently, as the length of the diffraction vector s is equal to 1/Λ (inverse of the indentation depth), sr is equal to the distance between two Bragg planes (or indentation surfaces), and diffraction from any point r will have a phase of 2πsr. Moreover, we can define the phonon density resolution through the mean resolution distance, according to the period nΛ of the Fourier serie of the phonon density map. The following equation leads us to the calculus of the reflective resolution of the structure, involving the path difference ∆d as:

Fig. 4 .

 4 Fig. 4. Typical angular distribution function. The first shell represents the main density function at a distance r of the structure. ) ( ) (

Fig. 5 .

 5 Fig. 5. Orthographical rotative analyze of a frontage in the rue d'Orléans, Nantes.

Fig. 6 .

 6 Fig. 6. Tridimensional dilation of the urban scene vertexes (perspective views).

Fig. 7 .

 7 Fig. 7. Shape spectrums of the urban frontage with a spherical recovering element, at different incident angles.

4. 4

 4 Results of the analysis : Frontage's structure factors and vertex densitomentryThe Fourier transform of the surface roughness informs the frontage's complexity, leading both to the angular distribution function and the spatial scattering function of the indented surface calculations.Fractal Scattering Indicators forUrban Sound Diffusion.doc submitted to World Scientific : 10/07/2003 : 18:36 8/10 As an indicator of the indentations frequency, the Fourier transform discriminates clearly the structure of a surface, revealing the spatial occurences of the roughness peaks (figure 8.1). The angular distribution function is defined through the structure factor computation of the surface, and indicates the frontage scattering behaviour for a particular direction of the incident beam (figure 8.2). Moreover, the spatial scattering function offers a tridimensional interpretation of the angular distribution function, allowing the distribution of the surface's scatterers along every incidence angle of the acoustic source (figure 8.3).

Fig. 8 .

 8 Fig. 8. Fourier transform (1), angular distribution function (2) and spatial scattering function (3) of the frontage indented surface Those indicators allows the computation of the vertex densitomentry for every incidence angle of the surface, with an increment of 5 degrees for localisation lengths Λ from 0.05 to 10 m, which corresponding acoutical frequency domain is 25 Hz to 8 kHz. Those densitometries correspond to the characteristic directions of scattering, through the density distribution ρ(x, y, z) calculation for each incidence angle.

Fig. 9 .

 9 Fig. 9. Angular vertex densitomentry of the urban frontage applied to the urban scene. Measures for roughness values r of, respectively, 1 to 10 m, 0.2 to 0.5 m and 0.05 to 0.2 m .


Ph Y Lasne

Philippe Paillou

Gilles Ruffié

Carlos Serradilla

François Demontoux

Anthony Freeman

Tom Farr

K Mcdonald

B Chapman

J.-M Malézieux

G Paillou

C Ruffié

F Serradilla

Demontoux

EFFECT OF SALINITY ON THE DIELECTRIC PROPERTIES OF GEOLOGICAL MATERIALS : IMPLICATION FOR SOIL MOISTURE DETECTION BY MEANS OF REMOTE SENSING

Keywords: Earth, evaporites, dielectric mixing model, IEM, Mars, polarimetry, radar backscattering, salinity, SAR, soil moisture

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

I. INTRODUCTION

The measurement of soil moisture by means of radar systems has been widely investigated over the last two decades [START_REF] Lasne | A phase signature for detecting wet subsurface structures using polarimetric L-band SAR[END_REF][START_REF] Bindlish | Subpixel variability on remotely sensed soil moisture: An inter-comparison study of SAR and ESTAR[END_REF][START_REF] Shi | Estimation of bare surface soil moisture and surface roughness parameter using L-Band SAR image data[END_REF][START_REF] Ulaby | Microwave backscatter dependence on surface roughness, soil moisture, and soil texture, Part I -Bare soil[END_REF][START_REF] Ulaby | Microwave Remote Sensing: Active and Passive[END_REF][START_REF] Fung | Microwave Scattering and Emissions Models and Their Applications[END_REF]. As the electric properties of soils depend on their water content, it impacts the radar backscattering coefficient σ σ σ σ o [START_REF] Dubois | Measuring soil moisture with imaging radar[END_REF][START_REF] Su | Estimation of surface soil moisture by inversion of SAR data, surface scattering from random rough, bare soils, spatial and temporal soil moisture mapping from ERS-1/2, and JERS-1 SAR data and macroscale hydrologic modeling for regional climate models (RCM)[END_REF]. While the effect of water content on the permittivity has been widely studied and modeled, little has been done on the salinity effect. Recent work has underlined the influence of the presence of salts in solution on the dielectric properties of soils and especially on the imaginary part ε ε ε ε'' of the dielectric constant [START_REF] Aly | Modelling the backscattering coefficient of salt-affected soils: applications to Wadi el Natrun bottom, Egypt[END_REF][START_REF] Shao | Effect of dielectric properties of moist salinized soils on backscattering coefficients extracted from RADARSAT image[END_REF][START_REF] Sreenivas | Dielectric properties of salt-affected soils[END_REF]. If the real part ε ε ε ε' of the permittivity, related to the medium polarization, governs the velocity of propagation of a wave through the material, ε ε ε ε'' is related to the conductivity of the medium and represents the radar signal attenuation by energy absorption required to reach the polarization (ohmic losses). It thus appears essential to take into account the occurrence of saline deposits (evaporites) in radar remote sensing applications. We have started to study the influence of salts on the backscattering coefficient σ σ σ σ o through the dielectric properties of the material. The adopted methodology is based on measurements carried out in the laboratory by means of a vectorial network analyzer in order to firstly assess the validity of dielectric mixing models [START_REF] Dobson | Microwave dielectric behavior of wet soil -Part II: Dielectric mixing models[END_REF][START_REF] Stogryn | Equations for calculating the dielectric constant of saline water[END_REF][START_REF] Mironov | Generalized refractive mixing dielectric model for moist soils[END_REF][START_REF] Wang | An empirical model for the complex dielectric permittivity of soils as a function of water content[END_REF], based on the Debye formulas. These dielectric models will then provide input parameters required for the modeling of σ σ σ σ o by means of analytical scattering models (IEM, SPM) [START_REF] Ulaby | Microwave Remote Sensing: Active and Passive[END_REF][START_REF] Fung | Microwave Scattering and Emissions Models and Their Applications[END_REF], [START_REF] Fung | Backscattering from a randomly rough dielectric surface[END_REF][START_REF] Hsieh | A further study of the IEM surface scattering[END_REF][START_REF] Chen | A note on the multiple scattering in an IEM model[END_REF][START_REF] Wu | A reappraisal of the validity of the IEM model for backscattering from rough surfaces[END_REF]. Simulation results will finally be compared to field measurements (Pyla dune, Death Valley, Mojave Desert) and will be used for the interpretation of SAR data (AIRSAR, PALSAR). Our objective is to exploit the dielectric properties of saline deposits for the detection and mapping of moisture in arid regions on both Earth and Mars (nowadays the occurrence of evaporites on Mars is commonly accepted [START_REF] Tosca | Geochemical modeling of evaporites on Mars: Insight from Meridiani Planum[END_REF]).

II. EVAPORITES

Evaporites are sedimentary deposits resulting from a chemical precipitation of dissolved substances in natural solutions (continental or marine) with an increase in their concentrations by terrigenous contributions and evaporation [START_REF] Rouchy | Les Evaporites[END_REF]. The most important concentration factor lies in evaporation processes although congelation and hydrothermal processes can also lead to supersaturated conditions necessary to mineral precipitation. The formation and the paragenesis of saline deposits are thus closely related to the physicochemical properties of minerals in solution (in terms of solubility) and to the parameters of evaporitic environments (temperature, salinity, evaporation rate, hydrostatic differential, pH, microbial activity).

III. DIELECTRIC MIXING MODELS

The influence of saline deposits in radar remote sensing is related to the solubility behavior and the ionic properties of the minerals. In their ionic (dissolved) form, the weight of dissolved substances per kilogram of solution defines the conductivity of the solution. This conductivity is directly related to the presence of free electrons and ions [START_REF] Pérez | Electromagnétisme[END_REF]. Under the action of an electric field, the distribution of charges is distorted and the barycentres of positive and negative charges no longer coincide. This results in an induced dipole moment that can be interpreted as the polarization vector P. In this case, we will be interested in the microscopic interpretation of polarization: atoms, molecules, ions. The presence of such components generates three microscopic polarization mechanisms: electronic, ionic, and orientation polarizabilities, which can be related to the medium permittivity (Clausius-Mossotti relation for polar molecules). More precisely, ε ε ε ε'' being proportional to the conductivity (interaction of free charges), we have to evaluate the impact of the presence of salts on the dielectric properties of the medium.

Assuming a multiphase approach for the mixtures (soil particle, free water, bound water, air voids, salts), we initially considered the dielectric mixing models proposed by Dobson [START_REF] Dobson | Microwave dielectric behavior of wet soil -Part II: Dielectric mixing models[END_REF] and Wang [START_REF] Wang | An empirical model for the complex dielectric permittivity of soils as a function of water content[END_REF] to assess the influence of salinity on the dielectric properties of geological materials. Firstly, these models have been applied to the case of a sand/salt/water mixture corresponding to a test site we are working on: the Pyla dune [START_REF] Lasne | A phase signature for detecting wet subsurface structures using polarimetric L-band SAR[END_REF][START_REF] Grandjean | Subsurface structures detection by comining L-band polarimetric SAR and GPR data: Example of the Pyla dune (France)[END_REF][START_REF] Lasne | Effect of multiple scattering on the phase signature of wet subsurface structures: Applications to polarimetric L-and C-band SAR[END_REF]. As sea water contains mainly NaCl, we considered results obtained for NaCl solutions as a first approximation allowing the application of the Stogryn equations [START_REF] Ulaby | Microwave Remote Sensing: Active and Passive[END_REF][START_REF] Stogryn | Equations for calculating the dielectric constant of saline water[END_REF] for the electromagnetic characterization of sea water [START_REF] Hasted | Dielectric properties of aqueous ionic solutions. Parts I and II[END_REF].

Contrarily to the Dobson model, the semi-empirical model proposed by Wang at 1.4 and 5 GHz allows to distinguish two regions for the variations of the dielectric constant as a function of the mixture moisture. When m v < W t , W t being the transition moisture, water molecules are tightly bound to the soil particles. Making comparison to ice molecules, Wang has shown similarity in activation energy values. Consequently, we have considered the dielectric properties of ice as a first approximation for those of bound water. By opposition, for moisture values higher than the transition moisture (m v > W t ), water can be considered as free and its dielectric constant can be described by means of the classical equations of the Debye theory for a polar medium. Assuming a 4component dielectric mixing model, expressions of the complex permittivity are given by:

( ) ( ) r a v v P m P m ε ε ε - + - + = 1
for m v < W t , with:

( )

γ ε ε ε ε ⋅ ⋅ - + = t v i w i x W m and ( ) ( ) ( ) r a v w t v x t P m P W m W ε ε ε ε ε - + - + - + = 1 for m v > W t , with ( )γ ε ε ε ε i w i x - + =
where P denotes the porosity. ε a , ε w , ε r , and ε i are the dielectric constants of air, water, soil particles and ice respectively. ε x corresponds to the complex permittivity of bound water. W t and γ being soil texture dependent (volume fraction of sand, clay, loam...), they have been assessed on Pyla dune samples.

In order to take into account losses due to the ionic conductivity of samples (because of the presence of ions in the free water component), the dielectric properties of the NaCl solution have been determined using the Debye's classical theory modified by Lane and Saxton [START_REF] Lane | Dielectric dispersion in pure polar liquids at very high radio frequencies. III. The effect of electrolytes in solution[END_REF]. According to the Stogryn formulation, real and imaginary parts of the saline solution are given by [START_REF] Ulaby | Microwave Remote Sensing: Active and Passive[END_REF][START_REF] Stogryn | Equations for calculating the dielectric constant of saline water[END_REF]

: 2 ' ) 2 ( 1 f sw sw swo sw sw πτ ε ε ε ε - - + = ∞ ∞ o i sw sw swo sw sw f f f ε π σ πτ ε ε πτ ε 2 ) 2 ( 1 ) 2 ( 2 " + - - ⋅ = ∞
where τ sw and σ i correspond to the relaxation time and the ionic conductivity of the NaCl solution and are temperature as well as salinity dependent [START_REF] Stogryn | Equations for calculating the dielectric constant of saline water[END_REF].

The permittivity of the sand/sea water mixture was computed according to the frequency (L-and C-Bands), the moisture content (m v <0.6), and the salinity (S<140°/oo). The temperature was fixed at 20°C, the bulk density is assumed to be 1.74 g.cm -3 , and the specific density of the solid fraction 2.65 g.cm -3 (Figs. 1,2). The other constants correspond to those found in the literature [START_REF] Ulaby | Microwave Remote Sensing: Active and Passive[END_REF][START_REF] Stogryn | Equations for calculating the dielectric constant of saline water[END_REF].

A. Salinity Effect on the Dielectric Constant

Our first results show that if the real and imaginary parts increase with the moisture content, the impact of salinity isn't the same for ε ε ε ε' and ε ε ε ε''. As the real part is concerned, the results presented in Fig. 1 shows that soil salinity has a little influence on ε ε ε ε' except for soil with high moisture content (m v > 0.2) for which ε ε ε ε' decreases with increasing salinity. For small salinity values, the increasing moisture content appears to be the main factor in ε ε ε ε' variations. On the contrary, the imaginary part ε ε ε ε" is strongly affected by both salinity and moisture of soil samples. In particular, the higher the magnitude of humidity the stronger the effect of salinity on the imaginary part. Since ε ε ε ε" is proportional to the conductivity, such a behavior can be explained by the increase in soil moisture content that leads to a greater amount of salts dissolved in the soil system (greater free water component) and thus to the increase in conductivity. More precisely, for small water content, the bound water component dominates leading to a weak increase in dielectric constant since its dielectric properties are closed to the ice ones. For increasing water content values, the free water component becomes much more effective allowing a greater amount of dissolved salts and then a higher conductivity. Fig. 1 also clearly indicates that the rate of increase in ε ε ε ε" with the salinity is dependent on soil moisture content. Nevertheless, when salt concentrations are in excess (S > 100°/oo), ε ε ε ε" decreases. This can be related to a precipitation of dissolved salts leading to a decrease in free water conductivity. This behavior confirms the one reported in recent works of Mironov [START_REF] Mironov | Generalized refractive mixing dielectric model for moist soils[END_REF] on bentonite, Shao [START_REF] Shao | Effect of dielectric properties of moist salinized soils on backscattering coefficients extracted from RADARSAT image[END_REF] on NaCl solutions, and Aly [START_REF] Aly | Modelling the backscattering coefficient of salt-affected soils: applications to Wadi el Natrun bottom, Egypt[END_REF] on silty loam soil samples.

Assuming a transition moisture content, the semiempirical model proposed by Wang seems to provide a better description of the dielectric constant measurements. For such a reason, we preferred in the following the semiempirical approach of Wang to the Dobson one in order to characterize the dielectric properties of the sand/ saline water mixture

B. Frequency Effect on the Dielectric Constant

Since the conductivity depends on the frequency, we aim at assessing the frequency effect on the dielectric constant of our moistened and salinized mixture by means of the Wang semiempirical model.

If the results for the real part indicate that ε ε ε ε' slowly decreases with increment of frequency for high content moisture (m v > 20 %) whatever the salinity value may be, the most interesting results concern the imaginary part of the soil mixture related to the ionic conductivity of the NaCl electrolyte solution. Actually, it can be seen on Fig. 2 that ε ε ε ε" steeply decreases in the [1-4 GHz] frequency range in the presence of salinity (S > 0) while ε ε ε ε" increases when S = 0. Moreover, Shao [START_REF] Shao | Effect of dielectric properties of moist salinized soils on backscattering coefficients extracted from RADARSAT image[END_REF] reported the same ε ε ε ε" variations derived from experimental measurements performed on NaCl concentrated solutions. Likewise, investigations carried out by Komarov [START_REF] Komarov | Frequency dispersion in microwave for complex permittivity of bound water stored in soils and wet salts[END_REF] led to the same conclusions concerning kaolinite, montmorillonite and NaCl that may be attributed to the influence of the relaxation time of the saturated solution [START_REF] Dobson | Microwave dielectric behavior of wet soil -Part II: Dielectric mixing models[END_REF][START_REF] Lane | Dielectric dispersion in pure polar liquids at very high radio frequencies. III. The effect of electrolytes in solution[END_REF][START_REF] Falkenhagen | [END_REF][START_REF] Chandra | Frequency dependence of ionic conductivity of electrolyte solutions[END_REF]. According to the Debye-Falkenhagen theory, the variations of ε ε ε ε" with respect to the frequency could be attributed to the frequency dependence of the ionic conductivity which usually describes the motion of ions in an electrolyte solution [START_REF] Falkenhagen | [END_REF]. In particular, Chandra [START_REF] Chandra | Frequency dependence of ionic conductivity of electrolyte solutions[END_REF] presented a theory for the frequency dependence of the ionic conductivity of an electrolyte solution where the ionic conductivity decreases at high frequency. These authors considered the dynamic effect of the relaxation of an ion atmosphere (space of opposite sign of charge which surrounds the central ion) on the motion of an ion. Moving in an electrolyte solution, an ion is subject to a retarding force due to the ionic atmosphere lags. When an ion moves, through the liquid with a velocity produced by an external electric field, the ionic atmosphere cannot immediately follow the motion leading to a dissymmetry in the direction of the ion motion. This dissymmetry of the electric density causes a force (electric force of relaxation [START_REF] Falkenhagen | [END_REF]) on the moving ion which decreases its mobility. Assuming an oscillating electric field (microwave emission), the central ion oscillates and the ion atmosphere gets less time to reach the relaxation (relaxation time). The atmosphere is then less asymmetric. As a result, the effect of the electric force of relaxation is reduced leading to a higher ion mobility (reduction of electrolyte friction) and hence an enhancement of the conductivity at low frequency. At higher frequency, the dissymmetry of the ionic atmosphere cannot be built up since the central ion oscillates so fast that the net ionic motion is smaller than the one in the presence of a static or low frequency electric field. As a result, the retarding effect vanishes and the ionic atmosphere as well as the central ion can be regarded as motionless leading to a decrease in ion mobility and then in the ionic conductivity [START_REF] Falkenhagen | [END_REF][START_REF] Chandra | Frequency dependence of ionic conductivity of electrolyte solutions[END_REF]. Moreover, it was shown that at high frequency, the dominant loss mechanism on the dielectric constant is mainly due to the dielectric relaxation (polarization losses) of free water since the maximum of ε ε ε ε" occurs at the relaxation frequency [START_REF] Komarov | Frequency dispersion in microwave for complex permittivity of bound water stored in soils and wet salts[END_REF][START_REF] Sabburg | Dielectric behavior of moist swelling clay soils at microwave frequencies[END_REF] (17 GHz for pure water): it could explain the increase in ε ε ε ε" observed by Hallikainen [START_REF] Hallikainen | Microwave dielectric behavior of wat soil -Part I: empirical models and experimental observations[END_REF]. On the contrary, at lower frequency [1-4 GHz], the ionic conductivity is the main contributor in dielectric losses causing ε ε ε ε" of moistened salinized soils to vary inversely with frequency. Between these two regimes, ε ε ε ε" would be expected to pass through a minimum [START_REF] Sabburg | Dielectric behavior of moist swelling clay soils at microwave frequencies[END_REF] especially for small salinity and high moisture content values as reported by [START_REF] Shao | Effect of dielectric properties of moist salinized soils on backscattering coefficients extracted from RADARSAT image[END_REF] and [START_REF] Dobson | Microwave dielectric behavior of wet soil -Part II: Dielectric mixing models[END_REF].

IV. LABORATORY MEASUREMENTS

In order to determine the validity of the previous dielectric mixing model, we performed complex permittivity measurements for a sand/sea water mixture with the same frequency range, moisture content and salinity values.

Measurements were carried out by means of a vectorial network analyzer coupled to an open-ended coaxial probe (SMA type) providing the reflexion coefficient S11 (amplitude and phase) of the electromagnetic wave at the sample surface [32].

Since the electromagnetic field at the probe/sample interface can be represented by a capacitive equivalent circuit (capacitor), a calibration procedure performed on standard chemical solutions (for which the variations of the complex permittivity with the frequency are well known) allows to define the probe parameters. The knowledge of such parameters combined with measurements of the S11 reflection coefficient then makes it possible to retrieve real and imaginary parts of the dielectric constant of geological material samples using a capacitive inversion algorithm. Nevertheless, it should be noticed that the experimental results showing a transition moisture value (W t ~29% for S = 100‰ and ~33% for S = 40‰), they confirm the bimodal approach proposed by Wang [START_REF] Wang | An empirical model for the complex dielectric permittivity of soils as a function of water content[END_REF] which will then be used on the following.

V. NUMERICAL SIMULATIONS OF THE BACKSCATTERING COEFFICIENT

In order to assess the impact of salts on airborne or orbital SAR data, we computed the radar backscattering coefficients at L-Band (1.5 GHz) for the complex permittivity values previously measured. Assuming smooth surfaces (rms-height of 0.3 cm and correlation length of 2.7 cm), we used the analytical IEM and SPM scattering models. Considering the surface scattering term only, the single backscattering coefficient is expressed by: ( ) ( ) Results presented in Fig. 4 indicate that the sensitivity of the backscattering coefficient to the salinity depends on the moisture content. This sensitivity is more important for the vertical polarization (VV). Although salinity more slightly affects the horizontal polarization (HH), in particular for high moisture contents, the strong dependence of the backscattering coefficient on the salinity for low moisture values constitutes an important result for the detection of small amounts of water when salt is present. Assuming a typical instrument detection limit of about -30dB for an orbital radar, this result is particularly interesting for the Martian case where the expected moisture variations would not exceed a few percent [START_REF] Feldman | Global distribution of near surface hydrogen on Mars[END_REF][START_REF] Mitrofanov | Vertical distribution of shallow water in Mars subsurface from HEND/Odyssey data[END_REF][START_REF] Möhlmann | Water in the upper Martian surface at mid-and lowlatitude: presence, state, and consequences[END_REF].

! ) sin( 2 4 1 2 ² ) ²( cos ² 2

VI. FUTURE WORK

We initially considered the influence of salinity on the amplitude of the radar backscattering. As the copolar phase difference is a potential indicator for soil moisture detection [START_REF] Lasne | A phase signature for detecting wet subsurface structures using polarimetric L-band SAR[END_REF][START_REF] Lasne | Effect of multiple scattering on the phase signature of wet subsurface structures: Applications to polarimetric L-and C-band SAR[END_REF], we will also study the impact of salinity on radar phase variations.

Fig. 1 :

 1 Fig. 1: Effect of salinity on the complex permittivity of a sand/saline water mixture derived from the Wang's model at 1.5 GHz.

Fig. 2 :

 2 Fig. 2: Frequency variations of real (left) and imaginary (right) parts of the dielectric constant of the sand/saline water mixture derived from the Wang's model for several moisture content and fixed salinity values S = 100‰ (at the top) and S = 40‰ (at the bottom).

Fig. 3

 3 Fig.3displays the measurements results of real and imaginary parts of sand/saline water mixture as function of frequency and moisture for two salinity values (S = 40 and 100‰). These results

Fig. 3 :

 3 Fig. 3: Frequency variations of real (left) and imaginary (right) parts of the dielectric constant of the sand/saline water mixture derived from laboratory measurements for several moisture content and fixed salinity values S = 100‰ (at the top) and S = 40‰ (at the bottom) confirm the predicted salinity and frequency dependence of the dielectric constant. As the real part is concerned, measurements results clearly indicate that ε ε ε ε' decreases with increment in salinity as well as in frequency. Moreover, ε ε ε ε' values derived from the Wang model are in good agreement with those derived from measurements in the [1-3GHz] frequency range. Dealing with the imaginary part, laboratory results clearly indicate the influence of salinity on ε ε ε ε" leading to a strong increase of the imaginary part with increment of salinity. Laboratory measurements also confirm the theoretical frequency dependence of ε ε ε ε" displaying a steep variation rate in the [1-2GHz] frequency range although the theoretical values appear to underestimate the measured ones. It would thus be necessary to make some modifications to the dielectric mixing model according to experimental data sets.

  the SPM. pp indicates the polarization state of the emitted/scattered wave respectively (HH or VV), θ is the incident angle, k the wavenumber, W n the Fourier transform of the nth power of the surface correlation function and α pp are the Fresnel reflexion coefficients.

Fig. 4 :

 4 Fig. 4: IEM simulations for the backscattering coefficient at L-Band at 40° incidence angle.