Thomas Given-Wilson
email: thomas.given-wilson@inria.fr

Expressiveness via Intensionality and Concurrency

Computation can be considered by taking into account two dimensions: extensional versus intensional, and sequential versus concurrent. Traditionally sequential extensional computation can be captured by the λ-calculus. However, recent work shows that there are more expressive intensional calculi such as S F-calculus. Traditionally process calculi capture computation by encoding the λ-calculus, such as in the π-calculus. Following this increased expressiveness via intensionality, other recent work has shown that concurrent pattern calculus is more expressive than π-calculus. This paper formalises the relative expressiveness of all four of these calculi by placing them on a square whose edges are irreversible encodings. This square is representative of a more general result: that expressiveness increases with both intensionality and concurrency.

Introduction

Computation can be characterised in two dimensions: extensional versus intensional; and sequential versus concurrent. Extensional sequential computation models are those whose functions cannot distinguish the internal structure of their arguments, here characterised by the λ-calculus [START_REF] Barendregt | The Lambda Calculus. Its Syntax and Semantics[END_REF]. However, Jay & Given-Wilson show that λ-calculus does not support all sequential computation [START_REF] Jay | A combinatory account of internal structure[END_REF]. In particular, there are intensional Turing-computable functions, characterised by pattern-matching, that can be represented within S F-calculus but not within λ-calculus [START_REF] Jay | A combinatory account of internal structure[END_REF]. Of course λ-calculus can encode Turing computation, but this is a weaker claim. Ever since Milner et al. showed that the π-calculus generalises λ-calculus [START_REF] Milner | Functions as processes[END_REF][START_REF] Milner | A calculus of mobile processes, part I/II[END_REF], concurrency theorists expect process calculi to subsume sequential computation as represented by λ-calculus [START_REF] Milner | Functions as processes[END_REF][START_REF] Milner | A calculus of mobile processes, part I/II[END_REF][START_REF] Milner | Communicating and Mobile Systems: the Pi-Calculus[END_REF]. Following from this, here extensional concurrent computation is characterised by process calculi that do not communicate terms with internal structure, and, at least, support λ-calculus. Intensional concurrent computation is represented by process calculi whose communication includes terms with internal structure, and reductions that depend upon the internal structure of terms. Here intensional concurrent computation is demonstrated by concurrent pattern calculus (CPC) that not only generalises intensional pattern-matching from sequential computation to pattern-unification in a process calculus, but also increases the symmetry of interaction [START_REF] Given-Wilson | Concurrent pattern calculus[END_REF][START_REF] Given-Wilson | A concurrent pattern calculus[END_REF].

These four calculi form the corners of a computation square where the left side is merely extensional and the right side also intensional; the top edge is sequential and the bottom edge concurrent. All the arrows preserve reduction. The horizontal (solid) arrows are homomorphisms in the sense that they also preserve application or parallel composition. The vertical (dashed) arrows are parallel encodings in that they map application to a parallel composition (with some machinery). Thus each arrow represents increased expressive power with CPC completing the square. This paper presents the formalisation of these expressiveness results for the four calculi above. This involves adapting some popular definitions of encodings [START_REF] Gorla | Comparing communication primitives via their relative expressive power[END_REF][START_REF] Gorla | A taxonomy of process calculi for distribution and mobility[END_REF][START_REF] Gorla | Towards a unified approach to encodability and separation results for process calculi[END_REF] and then building upon various prior results [START_REF] Curry | Combinatory Logic[END_REF][START_REF] Milner | Functions as processes[END_REF][START_REF] Milner | A calculus of mobile processes, part I/II[END_REF][START_REF] Given-Wilson | Concurrent pattern calculus[END_REF][START_REF] Jay | A combinatory account of internal structure[END_REF][START_REF] Given-Wilson | Concurrent Pattern Unification[END_REF]. These can be combined to yield the new expressiveness results here captured by the computation square.

The organisation of the paper is as follows. Section 2 reviews prior definitions of encodings and defines the ones used in this paper. Section 3 reviews λ-calculus and combinatory logic while introducing common definitions. Section 4 summarises intensionality in the sequential setting and formalises the arrow across the top of the square. Section 5 begins concurrency through π-calculus and its parallel encoding of λ v -calculus. Section 6 recalls concurrent pattern calculus and completes the results of the computation square. Section 7 draws conclusions, considers related work, and discusses future work.

Encodings

This section recalls valid encodings [START_REF] Gorla | Towards a unified approach to encodability and separation results for process calculi[END_REF] for formally relating process calculi and adapts the definition to define homomorphisms and parallel encodings. The validity of valid encodings in developing expressiveness studies emerges from the various works [START_REF] Gorla | Comparing communication primitives via their relative expressive power[END_REF][START_REF] Gorla | A taxonomy of process calculi for distribution and mobility[END_REF][START_REF] Gorla | Towards a unified approach to encodability and separation results for process calculi[END_REF], that have also recently inspired similar works [START_REF] Lanese | On the expressiveness of polyadic and synchronous communication in higher-order process calculi[END_REF][START_REF] Lanese | On the expressive power of primitives for compensation handling[END_REF][START_REF] Van Glabbeek | Musings on encodings and expressiveness[END_REF]. Here the adaptations are precise definitions of homomorphisms that give stronger positive results (the negative results are not required to be as strong). The parallel encodings are defined to account for the mixture of sequential and concurrent languages considered.

An encoding of a language L 1 into another language L 2 is a pair (

[[ • ]], ϕ [[ ]]
) where [[ • ]] translates every L 1 -term into an L 2 -term and ϕ [[ ]] maps every name (of the source language) into a tuple of k names (of the target language), for k > 0. The translation [[ • ]] turns every term of the source language into a term of the target; in doing this, the translation may fix some names to play a precise rôle or may translate a single name into a tuple of names. This can be obtained by exploiting ϕ

[[ ]] .
Now consider only encodings that satisfy the following properties. Let a k-ary context C( 1 ; . . . ; k ) be a term with k holes { 1 ; . . . ; k } that appear exactly once each. Moreover, denote with -→ i and =⇒ i the relations -→ (reduction relation) and =⇒ (the reflexive transitive closure of -→) in language L i ; denote with -→ ω i an infinite sequence of reductions in L i . Moreover, let ≡ i denote the structural equivalence relation for a language L i , and ∼ i denote a strong reference behavioural equivalence for language L i and ≃ i a weak reference behavioural equivalence. For simplicity the notation T -→ i ≡ i T ′ denotes that there exists T ′′ such that T -→ i T ′′ and T ′′ ≡ i T ′ , and may also be used with =⇒ i or ∼ i or ≃ i . Also, let P ⇓ i mean that there exists P ′ such that P =⇒ i P ′ and P ′ ≡ i P ′′ | √ , for some P ′′ where √ is a specific process to indicate success. Finally, to simplify reading, let S range over terms of the source language (viz., L 1 ) and T range over terms of the target language (viz., L 2 ).

Definition 1 (Valid Encoding (from [START_REF] Gorla | Towards a unified approach to encodability and separation results for process calculi[END_REF])). An encoding

([[ • ]], ϕ [[ ]] ) of L 1 into L 2 is valid if it satisfies
) = N, it holds that [[ op(S 1 , . . . , S k ) ]] = C N op ([[ S 1 ]]; . . . ; [[ S k ]]
). 2. Name invariance: for every S and name substitution σ, it holds that

[[ σS ]] = σ ′ [[ S ]] if σ is injective ∼ 2 σ ′ [[ S ]] otherwise where σ ′ is such that ϕ [[ ]] (σ(a)) = σ ′ (ϕ [[ ]] (a))
for every name a.

Operational correspondence:

for all S =⇒ 1 S ′ , it holds that

[[ S ]] =⇒ 2 ∼ 2 [[ S ′ ]]; -for all [[ S ]] =⇒ 2 T , there exists S ′ such that S =⇒ 1 S ′ and T =⇒ 2 ∼ 2 [[ S ′ ]]. 4. Divergence reflection: for every S such that [[ S ]] -→ ω 2 , it holds that S -→ ω 1 .

Success sensitiveness: for every S , it holds that S ⇓ 1 if and only if

[[ S ]] ⇓ 2 .
Observe that the definition of valid encoding is very general and, with the exception of success sensitiveness, can apply to sequential languages such as λ-calculus as well as process calculi. However, the relations presented in this work bring together a variety of prior results and account for them in a stronger and more uniform manner. To this end, the following definitions support the results. The first two define homomorphism in the sequential and concurrent settings.

Definition 2 (Homomorphism (Sequential)). A (sequential) homomorphism is a translation [[ • ]

] from one language to another that preserves reduction and application.

Definition 3 (Homomorphism (Concurrent)). A (concurrent) homomorphism is a valid encoding whose translation preserves parallel composition.

The next is for encoding sequential languages into concurrent languages and is strongly influenced by the definition of a valid encoding. Observe that [[ • ]] c indicates an encoding from source terms to target terms that is parametrised by a name c.

Definition 4 (Parallel Encoding). An encoding ([[

• ]] c , ϕ [[ ]] ) of L 1 into L 2 is a parallel encoding if it
satisfies the first four properties of a valid encoding (compositionality, name invariance, operational correspondence (with ∼ i replaced by ≃ i ), and divergence reflection) and the following additional property.

Parallelisation: The translation of the application MN is of the form

[[MN]] c def = (νn 1 )(νn 2 )(R | [[M]] n1 | [[N]] n2 )
where R depends only upon c and n 1 and n 2 .

The weakening of the operational correspondence from strong behavioural equivalence ∼ to weak behavioural equivalence ≃ is required to work with the existing results. This weakening can be alleviated by compromising on other properties, e.g. compositionality and parallelisation, and even strengthened to structural equivalence. However, since the results here are building on those already in the literature, the definition is adapted here with other approaches discussed later (in Section 6.2). Despite this weakening, the preservation of reduction and divergence is maintained.

Parallelisation is a restriction on the more general compositionality criteria. Here this ensures that in addition to compositionality, the translation must allow for independent reduction of the components of an application. As the shift from sequential to concurrent computation can exploit this to support parallel reductions, the definition of parallel encoding encourages more flexibility in reduction since components can be reduced independently.

The removal of the success sensitiveness property is for simplicity when using prior results. It is not difficult to include success sensitiveness, this involves adding the success primitive to the sequential languages and defining S ⇓, e.g. S ⇓ means that S -→ * √ . However, this requires adding a test process Q c to the definition of parallel encoding with success sensitiveness defined by: "for every S , it holds that S ⇓ 1 if and only if

[[ S ]] c | Q c ⇓ 2 .
However, since adding the success state √ to λ-calculus and combinatory logics would require redoing many existing results, it is easier to avoid the added complexity since no clarity or gain in significance is made by adding it.

Encodings from concurrent languages into sequential ones have not been defined specifically here since they prove impossible. The proof of these results relies merely on the requirement of reduction preservation or operational correspondence, and so shall be done on a case-by-case basis.

Sequential Extensional Computation

Both λ-calculus and traditional combinatory logic base reduction rules upon the application of a function to one or more arguments. Functions in both models are extensional in nature, that is a function does not have direct access to the internal structure of its arguments. Thus, functions that are extensionally equal are indistinguishable within either model even though they may have different normal forms.

The relationship between the λ-calculus and traditional combinatory logic is closer than sharing application-based reduction and extensionality. There is a homomorphism from call-by-value λ v -calculus into any combinatory logic that supports the combinators S and K [START_REF] Curry | Combinatory Logic[END_REF][START_REF] Barendregt | The Lambda Calculus. Its Syntax and Semantics[END_REF]. There is also a homomorphism from traditional combinatory logic to a λ-calculus with more generous operational semantics [START_REF] Curry | Combinatory Logic[END_REF][START_REF] Barendregt | The Lambda Calculus. Its Syntax and Semantics[END_REF].

λ-calculus

The term syntax of the λ-calculus is given by

t ::= x | t t | λx.t .
The free variables of a term are defined in the usual manner. A substitution σ is defined as a partial function from variables to terms. The domain of σ is denoted dom(σ); the free variables of σ, written fv(σ), is given by the union of the sets fv(σx) where x ∈ dom(σ). The variables of σ, written vars(σ), are dom(σ) ∪ fv(σ). A substitution σ avoids a variable x (or collection of variables µ) if x vars(σ) (respectively µ ∩ vars(σ) = {}). Substitution composition is denoted σ 2 •σ 1 and indicates that σ 2 •σ 1 (t) = σ 2 (σ 1 t). Note that all substitutions considered in this paper have finite domain. The application of a substitution σ to a term t is defined as usual, as is α-conversion = α .

There are several variations of the λ-calculus with different operational semantics. For construction of the computation square by exploiting the results of Milner et al. [START_REF] Milner | Functions as processes[END_REF], it is necessary to choose an operation semantics, such as call-by-value λ v -calculus or lazy λ l -calculus. The choice here is to use call-by-value λ v -calculus, although the results can be reproduced for lazy λ l -calculus as well. In addition a more generous operation semantics for λ-calculus will be presented for later discussion and relations.

To formalise the reduction of call-by-value λ v -calculus requires a notion of value v. These are defined in the usual way, by

v ::= x | λx.t
consisting of variables and λ-abstractions.

Computation in the λ v -calculus is through the

β v -reduction rule (λx.t)v -→ v {v/x}t .
When an abstraction λx.t is applied to a value v then substitute v for x in the body t. The reduction relation (also denoted -→ v ) is the smallest that satisfies the following rules

(λx.t)v -→ v {v/x}t s -→ v s ′ s t -→ v s ′ t t -→ v t ′ s t -→ v s t ′ .
The transitive closure of the reduction relation is denoted -→ * v though the star may be elided if it is obvious from the context.

The more generous operational semantics for the λ-calculus allows any term to be the argument when defining β-reduction. Thus the more generous β-reduction rule is

(λx.s)t -→ {t/x}s
where t is any term of the λ-calculus. The reduction relation -→ and the transitive closure thereof -→ * are obvious adaptations from those for the λ v -calculus. Observe that any reduction -→ v of λ v -calculus is also a reduction -→ of λ-calculus.

Traditional Combinatory Logic

A combinatory calculus is given by a finite collection O of operators (meta-variable O) that are used to define the O-combinators (meta-variables M, N, X, Y, Z) built from these by application M, N ::= O | MN .

Syntactic equality of combinators will be denoted by ≡. The O-combinatory calculus or O-calculus is given by the combinators plus their reduction rules.

Traditional combinatory logic can be represented by two combinators S and K [8] so the S K-calculus has reduction rules

S MNX -→ MX(NX) KXY -→ X .
The combinator S MNX duplicates X as the argument to both M and N. The combinator KXY eliminates Y and returns X. The reduction relation -→ is as for λ-calculus.

Although this is sufficient to provide a direct account of functions in the style of λ-calculus, an alternative is to consider the representation of arbitrary computable functions that act upon combinators.

A symbolic function is defined to be an n-ary partial function G of some combinatory logic, i.e. a function of the combinators that preserves their equality, as determined by the reduction rules. That is, if

X i = Y i for 1 ≤ i ≤ n then G(X 1 , X 2 , . . . , X n ) = G(Y 1 , Y 2 , . . . , Y n ) if both
sides are defined. A symbolic function is restricted to a set of combinators, e.g. the normal forms, if its domain is within the given set.

A combinator

G in a calculus represents G if GX 1 . . . X n = G(X 1 , . . . , X n )
whenever the right-hand side is defined. For example, the symbolic functions

S(X 1 , X 2 , X 3 ) = X 1 X 3 (X 2 X 3 ) and K(X 1 , X 2 ) = X 1

Relations

One of the goals of combinatory logic is to give an equational account of variable binding and substitution, particularly as it appears in λ-calculus. In order to represent λabstraction, it is necessary to have some variables to work with. Given O as before, define the O-terms by M, N ::

= x | O | MN
where x is as in λ-calculus. Free variables, substitutions, and symbolic computations are defined just as for O-calculus. Given a variable x and term M define a symbolic function G on terms by

G(X) = {X/x}M .
Note that if M has no free variables other than x then G is also a symbolic computation of the combinatory logic. If every such function G on O-combinators is representable then the O-combinatory logic is combinatorially complete in the sense of Curry [8, p. 5].

Given S and K then G above can be represented by a term λ * x.M given by

λ * x.x = I λ * x.y = Ky if y x λ * x.O = KO λ * x.MN = S (λ * x.M)(λ * x.N) .
The following lemma is a central result of combinatory logic [START_REF] Curry | Combinatory Logic[END_REF] and Theorem 2.3 of [START_REF] Jay | A combinatory account of internal structure[END_REF]. This is sufficient to show there is a homomorphism from λ v -calculus to any combinatory calculus that represents S and K.

Lemma 1. Any combinatory calculus that is able to represent S and K is combinatorially complete.

Theorem 1. There is a homomorphism from λ-calculus into S K-calculus.

There is a standard translation from S K-calculus into λ-calculus that preserves reduction and supports the following lemma [START_REF] Curry | Combinatory Logic[END_REF][START_REF] Barendregt | The Lambda Calculus. Its Syntax and Semantics[END_REF].

Lemma 2 (Theorem 2.3.3 of [11]). Translation from S K-calculus to λ-calculus preserves the reduction relation.

Theorem 2. There is a homomorphism from S K-calculus into λ-calculus.

Although the top left corner of the computation square is populated by λ v -calculus, the arrows out allow for either λ v -calculus or S K-calculus to be used. Indeed, the homomorphisms in both directions between λ-calculus and S K-calculus allow these two calculi to be considered equivalent.

Sequential Intensional Computation

Intuitively intensional functions are more expressive than merely extensional functions, however populating the top right corner of the computation square requires more formality than intuition. The cleanest account of this is by considering combinatory logic.

Even in S K-calculus there are Turing-computable functions defined upon the combinators that cannot be represented within S K-calculus. For example, consider the function that reduces any combinator of the form S KX to X. Such a function cannot be represented in S K-calculus, or λ-calculus, as all combinators of the form S KX represent the identity function. However, such a function is Turing-computable and definable upon the combinators. This is an example of a more general problem of factorising combinators that are both applications and stable under reduction.

Exploiting this factorisation is S F-calculus [START_REF] Jay | A combinatory account of internal structure[END_REF] that is able to support intensional functions on combinators including a structural equality of normal forms. Thus S Fcalculus sits at the top right hand corner of the computation square. The arrow across the top of the square is formalised by showing a homomorphism from S K-calculus into S F-calculus. The lack of a converse has been proven by showing that the intensionality of S F-calculus cannot be represented within S K-calculus, or λ-calculus [START_REF] Jay | A combinatory account of internal structure[END_REF].

Symbolic Functions

Symbolic functions need not be merely extensional, indeed it is possible to define symbolic functions that consider the structure of their arguments. Observe that each operator O has an arity given by the minimum number of arguments it requires to instantiate a rule. Thus, K has arity 2 while S has arity 3. A partially applied operator is a combinator of the form OX 1 . . . X k where k is less than the arity of O. An operator with a positive arity is an atom (meta-variable A). A partially applied operator that is an application is a compound. Hence, the partially applied operators of S K-calculus are the atoms S and K, and the compounds S M, S MN and K M for any M and N. Now define a factorisation function F on combinators by [START_REF] Jay | A combinatory account of internal structure[END_REF]). Factorisation of S K-combinators is a symbolic computation that is not representable within S K-calculus.

F (A, M, N) -→ M if A is an atom F (XY, M, N) -→ NXY if XY is a compound. Lemma 3 (Theorem 3.2 of

SF-calculus

When considering intensionality in a combinatory logic it is tempting to specify a factorisation combinator F as a representative for F . However, F is defined using partially applied operators, which cannot be known until all reduction rules are given, including those for F. This circularity of definition is broken by beginning with a syntactic characterisation of the combinators that are to be factorable.

The S F-calculus [START_REF] Jay | A combinatory account of internal structure[END_REF] has factorable forms given by

S | S M | S MN | F | F M | F MN and reduction rules S MNX -→ MX(NX) FOMN -→ M if O is S or F F(XY)MN -→ NXY if XY is a factorable form.
The expressive power of S F-calculus subsumes that of S K-calculus since K is here defined to be FF and I is defined to be S KK as before.

Lemma 4 (Theorem 5.2.3 of [START_REF] Given-Wilson | Concurrent Pattern Unification[END_REF]). There is a homomorphism from S K-calculus into S F-calculus.

Theorem 3 (Corollary 5.2.4 of [11]). There is a homomorphism from λ v -calculus to S F-calculus.

Theorem 4. There is no homomorphism from S F-calculus to λ v -calculus.

Proof. Observe that FyS (FF(S (FF)(FF))) with y replaced by a combinator of the form S KX reduces to X. By Lemma 3 it is impossible to represent this reduction in S K-calculus and thus reduction cannot be preserved. This completes the top edge of the computation square by showing that S F-calculus subsumes λ v -calculus and that the subsumption is irreversible. Indeed, these results hold for λ-calculus [11, Theorem 5.2.6] and S K-calculus (by Lemma 3) as well.

Concurrent Extensional Computation

The bottom left corner of the computation square considers extensional concurrent computation, here defined to be extensional process calculi that subsume λ-calculus. The π-calculus [START_REF] Milner | A calculus of mobile processes, part I/II[END_REF] holds a pivotal rôle amongst process calculi due to popularity, being the first to represent topological changes, and subsuming λ v -calculus [START_REF] Milner | Functions as processes[END_REF]. Note that although there are many π-calculi, the one here is that used by Milner so as to more easily exploit previous results [START_REF] Milner | Functions as processes[END_REF] (and here augmented with a success process √ ). The processes for the π-calculus are given as follows and exploit a class of names (denoted m, n, x, y, z, . . . similar to variables in the λ-calculus):

P ::= 0 | P| P | !P | (νa)P | a(b).P | a b .P | √ .
The names of the π-calculus are used for channels of communication and for information being communicated. The free names of a process fn(P) are as usual. Substitutions in the π-calculus are partial functions that map names to names, with domain, range, free names, names, and avoidance, all straightforward adaptations from substitutions of the λ-calculus. The application of a substitution to a process is defined in the usual manner. Issues where substitutions must avoid restricted or input names are handled by α-conversion = α that is the congruence relation defined in the usual manner. The general structural equivalence relation ≡ is defined by:

P | 0 ≡ P P | Q ≡ Q | P P | (Q | R) ≡ (P | Q) | R !P ≡ P | !P (νn)0 ≡ 0 (νn)(νm)P ≡ (νm)(νn)P P | (νn)Q ≡ (νn)(P | Q) if n fn(P)
The π-calculus has one reduction rule given by a(b).P | a c .Q -→ {c/b}P | Q .

The reduction rule is then closed under parallel composition, restriction and structural equivalence to yield the reduction relation -→ as follows:

P -→ P ′ P | Q -→ P ′ | Q P -→ P ′ (νn)P -→ (νn)P ′ P ≡ Q Q -→ Q ′ Q ′ ≡ P ′ P -→ P ′ .
The reflexive, transitive closure of -→ is denoted =⇒. Now that the π-calculus and process calculus concepts are recalled, it remains to demonstrate that Milner's encoding [START_REF] Milner | Functions as processes[END_REF] can meet the criteria for a parallel encoding.

As the β v -reduction rule depends upon the argument being a value the translation into π-calculus must be able to recognise values. Thus, Milner defines the following

[[y := λx.t]] def = !y(w).w(x).w(c).[[t]] c [[y := x]] def = !y(w).x w .
Also the following translation of λ v -terms

[[v]] c def = (νy)c y .[[y := v]] y not free in v [[s t]] c def = (νq)(νr)(ap(c, q, r) | [[s]] q | [[t]] r )
ap(p, q, r) def = q(y).(νv)y v .r(z).v z .v p .

Lemma 5. The translation [[ • ]

] c preserves and reflects reduction. That is:

1. If s -→ v t then [[ s ]] c =⇒≃ [[ t ]] c ; 2. if [[ s ]] c -→ Q then there exists Q ′ and s ′ such that Q =⇒ Q ′ and Q ′ ≃ [[ s ′ ]] c and either s -→ v s ′ or s = s ′ . Theorem 5. The translation [[•]] c is a parallel encoding from λ v -calculus to π-calculus.
There is some difficulty in attempting to define the analogue of a parallel encoding or homomorphism from a language with a parallel composition operator into a language without. However, this difficulty can be avoided by observing that any valid encoding, parallel encoding, or homomorphism must preserve reduction. Reduction preservation can then be exploited to show when an encoding is impossible. Here this is by exploiting Theorem 14.4.12 of Barendregt [START_REF] Barendregt | The Lambda Calculus. Its Syntax and Semantics[END_REF], showing that λ-calculus is unable to render concurrency or support concurrent computations. Theorem 6. There is no reduction preserving encoding of π-calculus into λ-calculus.

Concurrent Intensional Computation

Intensionality in sequential computation yields greater expressive power so it is natural to consider intensional concurrent computation. Intensionality in CPC is supported by a generalisation of pattern-matching to symmetric pattern-unification that provides the basis for defining interaction.

Concurrent Pattern Calculus

The patterns (meta-variables p, p ′ , p 1 , q, q ′ , q 1 , . . .) are built using a class of names familiar from π-calculus and have the following forms

p ::= λx | x | x | p • p
Binding names λx denote an input sought by the pattern. Variable names x may be output or tested for equality. Protected names x can only be tested for equality. A compound combines two patterns p and q, its components, into a pattern p • q and is left associative. The atoms are patterns that are not compounds and the atoms x and x are defined to know x. The binding names of a pattern must be pairwise distinct.

A communicable pattern contains no binding or protected names. Given a pattern p, the binding names bn(p), variable names vn(p), and protected names pn(p), are as expected, with the free names fn(p) being the union of variable and protected names.

A substitution σ (also denoted σ 1 , ρ, ρ 1 , θ, θ 1 , . . .) is a partial function from names to communicable patterns. Otherwise substitutions and their properties are familiar from earlier sections and are applied to patterns in the obvious manner. (Observe that protection can be extended to a communicable pattern by p • q = p • q in the application of a substitution to a protected name.)

The symmetric matching or unification {p q} of two patterns p and q attempts to unify p and q by generating substitutions upon their binding names. When defined, the result is some pair of substitutions whose domains are the binding names of p and of q, respectively. The rules to generate the substitutions are:

{x x} = {x x } = { x x} = { x x } def = ({}, {}) {λx q} def = ({q/x}, {}) if q is communicable {p λx} def = ({}, {p/x}) if p is communicable {p 1 • p 2 q 1 • q 2 } def = (σ 1 ∪ σ 2 , ρ 1 ∪ ρ 2 ) if {p i q i } = (σ i , ρ i ) for i ∈ {1, 2}
Two atoms unify if they know the same name. A binding name unifies with any communicable pattern to produce a binding for its underlying name. Two compounds unify if their corresponding components do; the resulting substitutions are given by taking unions of those produced by unifying the components. Otherwise the patterns cannot be unified and the matching is undefined.

The processes of CPC are the same as for π-calculus except for the input and output replaced by the case p → P with pattern p and body P. A case with the null process as the body p → 0 may also be written p when no ambiguity may occur.

The free names of processes, denoted fn(P), are defined as usual for all the traditional primitives and fn(p → P) = fn(p) ∪ (fn(P)\bn(p)) for the case. As expected the binding names of the pattern bind their free occurrences in the body. The application σP of a substitution σ to a process P is defined in the usual manner to avoid name capture. For cases this ensures that substitution avoids the binding names in the pattern: σ(p → P) = (σp) → (σP) if σ avoids bn(p). Renaming of a case is handled through α-conversion, = α , that is the congruence relation generated by the following axiom p → P = α ({λy/λx}p) → ({y/x}P) when x ∈ bn(p), y fn(P) ∪ bn(p). Renaming of a restriction is as usual. The renaming of a binding name (e.g. by {λy/λx}) is also as expected with the usual restrictions. The general structural equivalence relation ≡ is defined just as in π-calculus.

CPC has one interaction axiom given by

(p → P) | (q → Q) -→ (σP) | (ρQ) if {p q} = (σ, ρ) .
It states that if the unification of two patterns p and q is defined and generates (σ, ρ), then apply the substitutions σ and ρ to the bodies P and Q, respectively. If the matching of p and q is undefined then no interaction occurs. The interaction rule is then closed under parallel composition, restriction and structural equivalence in the usual manner. The reflexive and transitive closure of -→ is denoted =⇒. Finally, the reference behavioural equivalence relation ∼ for CPC is already well detailed [START_REF] Given-Wilson | Concurrent Pattern Unification[END_REF][START_REF] Given-Wilson | Pattern matching and bisimulation[END_REF][START_REF] Given-Wilson | A concurrent pattern calculus[END_REF].

Completing the Square

Support for both intensionality and concurrency places CPC at the bottom right corner of the computation square. This section shows how S F-calculus and π-calculus can both be subsumed by CPC, and thus completes the computation square. Down the right side of the square there is a parallel encoding from S F-calculus into CPC that also maps the combinators S and F to reserved names S and F, respectively. The impossibility of finding a parallel encoding of CPC into S F-calculus is proved in the same manner as the relation between λ v -calculus and π-calculus. Interestingly, in contrast with the parallel encoding of λ-calculus into π-calculus, the parallel encoding of S F-calculus into CPC does not fix a reduction strategy for S F-calculus. This is achieved by exploiting the intensionality of CPC to directly encode the reduction rules for S F-calculus into an S F-reducing process, or S F-machine. In turn, this process can then operate on translated combinators and so support reduction and rewriting.

The square is completed by showing a homomorphism from π-calculus into CPC, and by showing that there cannot be any homomorphism (or indeed a more general valid encoding) from CPC into π-calculus.

SF-calculus. The S F-calculus combinators can be easily encoded into patterns by defining the construction (| • |

), exploiting reserved names S and F, as follows

(|S | ) def = S (|F| ) def = F (|MN| ) def = (|M| ) • (|N| ) .
Observe that the first two rules map the operators to the same names. The third rules maps application to a compound of the components M and N. By representing S F-calculus combinators in the pattern of a CPC case, the reduction can then be driven by defining cases that recognise a reducible structure and perform the appropriate operations. The reduction rules can be captured by matching on the structure of the left hand side of the rule and reducing to the structure on the right. So (considering each possible instance for the F reduction rules) they can be encoded by cases as follows.

S • λm • λn • λx → m • x • (n • x) F • S • λm • λn → m F • F • λm • λn → m . . . F • (F • λp • λq) • λm • λn → n • (F • p) • q .
These processes capture the reduction rules, matching the pattern for the left hand side and transforming it to the structure on the right hand side. Of course these process do not capture the possibility of reduction of a sub-combinator, so further rules are required. Rather than detail them all, consider the example of a reduction MNOP -→ MN ′ OP that can be captured by

λm • (λu • λv • λw • λx) • λo • λp → u • v • w • x → λz → m • z • o • p
This process unifies with a combinator MXOP where X is reducible (observable from the structure), here binding the components of X to four names u, v, w and x. These four names are then shared as a pattern, which can then be unified with another process that can perform the reduction. The result will then (eventually) unify with λz and be substituted back into m • z • o • p to complete the reduction.

To exploit these processes in constructing a parallel encoding requires the addition of a name, used like a channel, to control application. Thus, prefix each pattern that matches the structure of an S F-combinator with a binding name λc and add this to the result, e.g. λc • (F • S • λm • λn) → c • m. Now the processes that handle each possible reduction rule can be placed under a replication and in parallel composition with each other. This yields the S F-reducing process R as shown in Figure 1 where the last four rules capture reduction of sub-combinators.

The translation [[•]] c from S F-combinators into CPC processes is here parametrised by a name c and combines application with a process ap(c, m, n). This is similar to Milner's encoding from λ v -calculus into π-calculus and allows the parallel encoding to exploit compositional encoding of sub-terms as processes and thus parallel reduction, while preventing confusion of application.

The translation [[•]] c of S F-combinators into CPC, exploiting the S F-reducing process R and reserved names S and F, is defined as follows:

[[S ]] c def = c • S | R [[F]] c def = c • F | R [[MN]] c def = (νm)(νn)(ap(c, m, n) | [[M]] m | [[N]] n ) ap(c, m, n) def = m • λx → n • λy → c • (x • y) | R .
The following lemmas are at the core of the operational correspondence and divergence reflection components of the proof of valid encoding, similar to Milnder's Theorem 7.7 [START_REF] Milner | Functions as processes[END_REF]. Further, it provides a general sense of how to capture the reduction of combinatory logics or similar rewrite systems. (Note that the results exploit that The lack of an encoding of CPC (or even π-calculus) into S F-calculus can be proved in the same manner as Theorem 6 for showing no encoding of π-calculus into λ-calculus. Theorem 8. There is no reduction preserving encoding from CPC into S F-calculus.

1. If M -→ N then [[ M ]] c =⇒≃ [[ N ]] c ; 2. if [[ M ]] c -→ Q then there exists Q ′ and N such that Q =⇒ Q ′ and Q ′ ≃ [[ N ]]
It may appear that the factorisation operator F adds some expressiveness that could be used to capture the parallel-or function g. Perhaps use F to switch on the result of the first function so that (assuming true is some operator T then) g x y is represented by F xT(K(Ky)) that reduces to T when x = T and to K(Ky)MN =⇒ y when x = MN that somehow is factorable but not terminating. However, this kind of attempt is equivalent to exploiting factorisation to detect termination and turns out to be paradoxical as demonstrated in the proof of Theorem 5.1 of [START_REF] Jay | A combinatory account of internal structure[END_REF].

This completes the arrow down the right side of the computation square. The rest of this section discusses some properties of translations and the diagonal from the top left to the bottom right corner of the square.

Observe that the parallel encoding from S F-calculus into CPC does not require the choice of a reduction strategy, unlike Milner's encodings from λ-calculus into πcalculus. The structure of patterns and peculiarities of pattern-unification allow the reduction relation to be directly rendered by CPC. In some sense this is similar to encoding the S F-combinators onto the tape of a Turing machine, the pattern (| • | ), and providing another process to be the state that reads the tape and performs operations upon it, the S F-reducing process R. This approach can also be adapted in a straightforward manner to support a parallel encoding of S K-calculus into CPC, that like the encoding of S F-calculus does not fix a reduction strategy.

Theorem 9. There is a translation [[•]] c that is a parallel encoding from S K-calculus into CPC.

The translation from S F-calculus to CPC presented here is designed to map application to parallel composition (with some restriction and process R) so as to meet the parallelisation and compositionality criteria for a parallel encoding. π-calculus. Across the bottom of the computation square there is a homomorphism from π-calculus into CPC. The converse separation result can be proved multiple ways [START_REF] Given-Wilson | Concurrent pattern calculus[END_REF][START_REF] Given-Wilson | Concurrent Pattern Unification[END_REF][START_REF] Given-Wilson | A concurrent pattern calculus[END_REF].

The translation [[ • ]] from π-calculus into CPC is homomorphic on all process forms except for the input and output which are translated as follows:

[[a(b).P]] def = a • λb • in → [[P]] [[a b .P]] def = a • b • λx → [[P]]
x not free in P.

Here in is any name, a symbolic name is used for clarity but no result relies upon this choice. The fresh name x is used to prevent the introduction of new reductions due to CPC's symmetric matching.

Lemma 9 (Corollary 7.2.3 of [START_REF] Given-Wilson | Concurrent Pattern Unification[END_REF]). The translation

[[ • ]] from π-calculus into CPC is a valid encoding.
Theorem 10. There is a homomorphism from π-calculus into CPC.

Thus the translation provided above is a homomorphism from π-calculus into CPC. Now consider the converse separation result.

Lemma 10 (Theorem 7.2.5 of [START_REF] Given-Wilson | Concurrent Pattern Unification[END_REF]). There is no valid encoding of CPC into πcalculus.

Theorem 11. There is no homomorphism from CPC into π-calculus.

Conclusions and Future Work

This work illustrates that there are increases in expressive power by shifting along two dimensions: from extensional to intensional, and from sequential to concurrent. This is best illustrated by the computation square that relates λ v -calculus, S F-calculus, πcalculus, and CPC as follows

λ v -calculus S F-calculus π-calculus concurrent pattern calculus ✲ ✲ ❄ ❄
where the left side is extensional, the right side intensional, the top side sequential, and the bottom side concurrent. The horizontal arrows are homomorphisms that map application/parallel composition to itself, and preserve and reflect reduction. The vertical arrows are parallel encodings that map application to parallel composition (with some extra machinery), and preserve and reflect reduction. Further, there are no reverse arrows as each arrow signifies an increase in expressive power. Such a square identifies relations that are more general than simply the choice of calculi here. The top left corner could be populated by λ v -calculus or λ l -calculus with minimal changes to the proofs. Alternatively, choosing λ-calculus or S K-calculus may also hold, although a parallel encoding into π-calculus requires some work. The top right corner could be populated by any of the structure complete combinatory logics without much effort [START_REF] Jay | A combinatory account of internal structure[END_REF][START_REF] Given-Wilson | Concurrent Pattern Unification[END_REF]. It may also be possible to place a pattern calculus [START_REF] Jay | First-class patterns[END_REF][START_REF] Jay | Pattern Calculus: Computing with Functions and Data Structures[END_REF], at the top right. The bottom left corner is also open to many other calculi: monadic/polyadic synchronous/asynchronous π-calculus could replace π-calculus with no significant changes to the results [START_REF] Given-Wilson | Concurrent Pattern Unification[END_REF][START_REF] Given-Wilson | A concurrent pattern calculus[END_REF]. Similarly there are, and will be, other process calculi that can take the place of CPC at the bottom right. For Spi calculus [START_REF] Abadi | A calculus for cryptographic protocols: The spi calculus[END_REF] an encoding of S F-calculus is delicate due to correctly handling reduction and not introducing infinite reductions or blocking on Spi calculus primitives and reductions. For Psi calculus [START_REF] Bengtson | Psi-calculi: a framework for mobile processes with nominal data and logic[END_REF] the encoding can be achieved very similarly to CPC, although arguably the implicit computation component of Psi calculus could simply allow for S F-calculus with the rest being moot. Although multiple process calculi may populate the bottom right hand corner, the elegance of CPC's intensionality is illustrated by the construction (| • | ) for combinatory logics.

Related Work

The choice of relations here is influenced by existing approaches. Homomorphisms in the sequential setting are standard [START_REF] Curry | Combinatory Logic[END_REF][START_REF] Barendregt | The Lambda Calculus. Its Syntax and Semantics[END_REF][START_REF] Felleisen | On the expressive power of programming languages[END_REF]. Valid encodings are popular [15-17, 21, 22, 30] albeit not the only approach as other ways to relate process calculi are also used that vary on the choice to map parallel composition to parallel composition (i.e. the homomorphism requirement here) [START_REF] Palamidessi | Comparing the expressive power of the synchronous and the asynchronous pi-calculus[END_REF][START_REF] Busi | On expressiveness of linda coordination primitives[END_REF][START_REF] De Nicola | On the expressive power of klaim-based calculi[END_REF][START_REF] Nielsen | Multiparty symmetric sum types[END_REF][START_REF] Van Glabbeek | Musings on encodings and expressiveness[END_REF]. Since the choice here is to build on prior results, valid encodings are the obvious basis for relating π-calculus and CPC, but no doubt this could be formalised under different criteria. Finally, the definition of parallel encodings here is to exploit the existing encodings in the literature and to be similar to valid encodings/homomorphisms. However, other approaches are possible as in [START_REF] Milner | Functions as processes[END_REF][START_REF] Parrow | The fusion calculus: Expressiveness and symmetry in mobile processes[END_REF] and doubtless many more as encoding λ-calculus into process calculi is common [START_REF] Berry | The chemical abstract machine[END_REF][START_REF] Milner | A calculus of mobile processes, part I/II[END_REF][START_REF] Cardelli | Mobile ambients[END_REF][START_REF] Milner | Communicating and Mobile Systems: the Pi-Calculus[END_REF].

The separation results here build upon results already in the literature. For showing the inability to encoding concurrent languages into sequential, the work of Abramsky [START_REF] Abramsky | The lazy lambda calculus[END_REF] and Plotkin [START_REF] Plotkin | Full abstraction, totality and pcf[END_REF] can also be considered. The impossibility of encoding CPC into π-calculus can be proved by using matching degree or symmetry [11, proofs for Theorem 7.2.5].

Future Work

Future work may proceed along several directions. The techniques used to encode S Fcalculus into CPC can be generalised for any combinatory logic, indeed it is likely a general result can be proved for all similar rewrite systems. This approach could also be used to clarify the relation between Turing machines and process calculi directly, rather than through λ-calculus. Another path of exploration is to generalise the account of intensionality in concurrency with full results in a general manner, this would include formalising the intensionality (or lack of) of Spi calculus, Psi calculus, and other popular process calculi. yielding the required result.

Proof (Lemma 8). The first part can be proved by exploiting Lemmas 6 and 7. The second is by considering the reduction [[ M ]] c -→ Q which must arise from the encoding of an application. It is then straightforward to show that either: the reductions Q =⇒ Q ′ correspond only to rebuilding the structure as in Lemma 6; or the reductions correspond to a reduction M -→ N and

Q ′ ≃ [[ N ]] c .
Proof (Theorem 7). Compositionality, parallelisation, and name invariance hold by construction. Operational correspondence follows from Lemma 7. Divergence reflection can be proved by observing that the only reductions introduced in the translation that do not correspond to reductions in the source language are from translated applications, and these are bounded by the size of the source term.

Proof (Theorem 8). The same technique as for Theorem 6 can be used.

Proof (Theorem 9). Straightforward by adapting the techniques used for the translation [[•]

] c from S F-calculus to CPC that is a parallel encoding.

Proof (Theorem 10). By the definition of translation [[ • ]] and Lemma 9.

Proof ( Theorem 11). By Lemma 10.

⋆

  This work has been partially supported by the project ANR-12-IS02-001 PACE.

  are represented by S and K, respectively, in S K-calculus. Consider the symbolic function I(X) = X. In S KI-calculus where I has the rule IY -→ Y then I is represented by I. In both S KI-calculus and S K-calculus, I is represented by any combinator of the form S KX since S KXY = KY(XY) = Y. For convenience define the identity combinator I in S K-calculus to be S KK.

Fig. 1 .

 1 Fig. 1. The S F-reducing process R.

Lemma 6 .Lemma 8 .

 68 R | R ∼ R to remove redundant copies of R [11, Theorem 8.7.2].) Given an S F-combinator M the translation [[M]] c has a reduction sequence to a process of the form c • (|M| ) | R. Lemma 7 (Theorem 7.1.2 of [11]). Given an S F-combinator M the translation [[M]] c preserves reduction. The translation [[ • ]] c preserves and reflects reduction. That is:

Theorem 7 .

 7 c and either M -→ N or M = N. The translation [[•]] c is a parallel encoding from S F-calculus to CPC.

  However, the construction (| • | ) can be used to provide a cleaner translation if these are not required. Consider an alternative translation [[•]] c parametrised by a name c as usual and defined by [[M]] c def = c • (|M| ) | R. Such a translation still supports name invariance, operational correspondence (up to structural equivalence ≡ instead of weak behavioural equivalence ≃), and divergence reflection.

  the following five properties: 1. Compositionality: for every k-ary operator op of L 1 and for every subset of names N, there exists a k-ary context C N op ( 1 ; . . . ; k ) of L 2 such that, for all S 1 , . . . , S k with fn(S 1 , . . . , S k

Appendix

This appendix provides greater detail for proofs omitted in the body of the paper.

Lemma 11. For all terms M and N and variables x there is a reduction (λ * x.M) N -→ * {N/x}M.

Proof. The proof straightforward is by induction on the structure of the combinator M.

Proof (Lemma 1). Given G(X) = {X/x}M as above define G to be λ * x.M and apply Lemma 11.

Proof (Theorem 1).

Straightforward by definition of the translation and Lemma 1.

Proof (Theorem 2).

Straightforward by definition of the translation and Lemma 2.

Proof (Lemma 5). The first part can be proved by exploiting Milner's Theorem 7.7 [START_REF] Milner | Functions as processes[END_REF]. The second is by considering the reduction [[ s ]] c -→ Q which must arise from the encoding of an application. It is then straightforward to show that either: the reductions Q =⇒ Q ′ correspond only to translated applications and thus

Proof (Theorem 5). Compositionality, parallelisation, and name invariance hold by construction. Operational correspondence follows from Lemma 5. Divergence reflection can be proved by observing that the only reductions introduced in the translation that do not correspond to reductions in the source language are from translated applications, and these are bounded by the size of the source term.

Proof (Theorem 6). Define the parallel-or function and show that it can be represented in π-calculus. The parallel-or function is a function g(x, y) that satisfies the following three rules g(⊥, ⊥) -→ * ⊥ and g(T, ⊥) -→ * T and g(⊥, T) -→ * T where ⊥ represents non-termination and T represents true. Such a function is trivial to encode in π-calculus by g(n 1 , n 2 ) = G = n 1 (x).m x .0 | n 2 (x).m x .0. Consider G in parallel with two processes P 1 and P 2 that output their result on n 1 and n 2 , respectively. If either P 1 or P 2 outputs T then G will also output T along m. Clearly π-calculus can represent the parallel-or function, and since Barendregt's Theorem 14.4.12 shows that λ-calculus cannot, there cannot be any reduction preserving encoding of π-calculus into λ-calculus.

Proof (Lemma 6).

The proof is by induction on the structure of M.

By two applications of induction, [[M

. Now there are reductions as follows:


Kais Ammari
email: kais.ammari@fsm.rnu.tn

Denis Mercier
email: denis.mercier@univ-valenciennes.fr

Kaïs Ammari

Boundary feedback stabilization of a chain of serially connected strings

Keywords: 2010 Mathematics Subject Classification. 35L05, 35M10, 35R02, 47A10, 93D15, 93D20 Network, wave equation, resolvent method, transfert function, boundary feedback stabilization

We consider N strings connected to one another and forming a particular network which is a chain of strings. We study a stabilization problem and precisley we prove that the energy of the solutions of the dissipative system decay exponentially to zero when the time tends to infinity, independently of the densities of the strings. Our technique is based on a frequency domain method and a special analysis for the resolvent. Moreover, by same appraoch, we study the transfert function associated to the chain of strings and the stability of the Schrödinger system.

Introduction

We consider the evolution problem (P ) described by the following system of N equations:

(P )                    (∂ 2 t u j -ρ j ∂ 2
x u j )(t, x) = 0, x ∈ (j, j + 1), t ∈ (0, ∞), j = 0, ..., N -1, ρ 0 ∂ x u 0 (t, 0) = ∂ t u 0 (t, 0), u N -1 (t, N ) = 0, t ∈ (0, ∞), u j-1 (t, j) = u j (t, j), t ∈ (0, ∞), j = 1, ..., N -1, -ρ j-1 ∂ x u j-1 (t, j) + ρ j ∂ x u j (t, j) = 0, t ∈ (0, ∞), j = 1, ..., N -1, u j (0, x) = u 0 j (x), ∂ t u j (0, x) = u 1 j (x), x ∈ (j, j + 1), j = 0, ..., N -1, where ρ j > 0, ∀ j = 0, ..., N -1.

We can rewrite the system (P) as a first order hyperbolic system, by putting

V j =   ∂ t u j ρ j ∂ x u j   , and V 0 j =   u 1 j ρ j ∂ x u 0 j   , 0 ≤ j ≤ N -1, (P ′ )              (∂ t V j -B j ∂ x V j )(t,
x) = 0, x ∈ (j, j + 1), t ∈ (0, ∞), j = 0, ..., N -1,

C 0 V 0 (t, 0) = 0, C N -1 V N -1 (t, N ) = 0, t ∈ (0, ∞),
V j-1 (t, j) = V j (t, j), t ∈ (0, ∞), j = 1, ..., N -1,

V j (0, x) = V 0 j (x), x ∈ (j, j + 1), j = 0, ..., N -1, where

B j =   0 1 ρ j 0   , C 0 =   1 -1 0 0   , C N -1 =   1 0 0 0   , 0 ≤ j ≤ N -1. (1.1)
Models of the transient behavior of some or all of the state variables describing the motion of flexible structures have been of great interest in recent years, for details about physical motivation for the models, see [START_REF] Dáger | Wave propagation, observation and control in 1-d flexible multi-structures[END_REF], [START_REF] Lagnese | Modeling, Analysis of dynamic elastic multi-link structures[END_REF] and the references therein.

Mathematical analysis of transmission partial differential equations is detailed in [START_REF] Lagnese | Modeling, Analysis of dynamic elastic multi-link structures[END_REF].

Let us first introduce some notation and definitions which will be used throughout the rest of the paper, in particular some which are linked to the notion of C ν -networks, ν ∈ N (as introduced in [START_REF] Below | Classical solvability of linear parabolic equations on networks[END_REF]).

Let Γ be a connected topological graph embedded in R, with N edges (N ∈ N * ). Let K = {k j : 0 ≤ j ≤ N -1} be the set of the edges of Γ. Each edge k j is a Jordan curve in R and is assumed to be parametrized by its arc length x j such that the parametrization π j : [j, j + 1] → k j : x j → π j (x j ) is ν-times differentiable, i.e. π j ∈ C ν ([j, j + 1], R) for all 0 ≤ j ≤ N -1. The density of the edge k j is ρ j > 0. The C ν -network R associated with Γ is then defined as the union

R = N -1 j=0 k j .
We study a feedback stabilization problem for a wave and a Schr dinger equations in networks, see [START_REF] Ammari | Asymptotic behaviour of the solutions and optimal location of the actuator for the pointwise stabilization of a string[END_REF]- [START_REF] Ammari | Stabilization of generic trees of strings[END_REF], [START_REF] Lagnese | Modeling, Analysis of dynamic elastic multi-link structures[END_REF] and Figure 1.

ρ 0 string 1 ρ 1 string 2 ρ 2 string 3 ... ... ρ N -2 string N-1 ρ N -1 string N • • • • • • • • Figure 1: Serially connected strings
More precisely, we study a linear system modelling the vibrations of a chain of strings.

For each edge k j , the scalar function u j (t, x) for x ∈ R and t > 0 contains the information on the vertical displacement of the string, 0 ≤ j ≤ N -1.

Our aim is to study the behaviour of the resolvent of the spatial operator which is defined in Section 3 and to obtain stability result for (P ).

We define the natural energy E(t) of a solution u = (u 0 , ..., u N -1 ) of (P ) and the natural energy of a solution V of (P ′ ), respectively, by

E(t) = 1 2 N -1 j=0 j+1 j |∂ t u j (t, x)| 2 + ρ j |∂ x u j (t, x)| 2 dx , (1.2)
e(t) = 1 2 N -1 j=0 V j 2 L 2 ρ j (j,+,j+1)×L 2 (j,j+1) , 0 ≤ j ≤ N -1, (1.3)
where L 2 ρ j (j, j + 1) = L 2 ρ j ((j, j + 1), dx) = L 2 ((j, +j + 1), ρ j dx).

We note that E(t) ≍ e(t), ∀ t ≥ 0.

We can easily check that every sufficiently smooth solution of (P ) satisfies the following dissipation law

E ′ (t) = -∂ t u 0 (t, 0) 2 ≤ 0, e ′ (t) = -C 0 V 0 (t, 0) 2 ≤ 0, (1.4)
and therefore, the energy is a nonincreasing function of the time variable t.

The result concerns the well-posedness of the solutions of (P ) and the exponential decay of the energy E(t) of the solutions of (P ).

The main result of this paper then concerns the precise asymptotic behaviour of the solutions of (P ). Our technique is based on a frequency domain method and a special analysis for the resolvent.

This paper is organized as follows: In Section 2, we give the proper functional setting for system (P ) and prove that the system is well-posed. In Section 3, we then show that the energie of system (P ) tends to zero. We study, in Section 3, the stabilization result for (P ) by the frequency domain technique and give the explicit decay rate of the energy of the solutions of (P ). Finally, in the last sections, we study the transfert function associated to a string network and the exponential stability of the Schrödinger system.

2 Well-posedness of the system

In order to study system (P ) we need a proper functional setting. We define the following spaces

H = N -1 j=0 (L 2 ρ j (j, j + 1) × L 2 (j, j + 1))
and

V = u = (u 0 , ..., u N -1 ) ∈ N -1 j=0 H 1 (j, j+1), u N -1 (N ) = 0, u j-1 (j) = u j (j), j = 1, . . . , N -1 ,
equipped with the inner products

< V, Ṽ > H = N -1 j=0 j+1 j ρ j u j (x) ũj (x) + v j (x) ṽj (x)dx , V =   u v   , Ṽ =   ũ ṽ   , (2.5)
< u, ũ > V = N -1 j=0 j+1 j ρ j ∂ x u j (x)∂ x ũj (x)dx . (2.6)
It is well-known that system (P ) may be rewritten as the first order evolution equation

   U ′ = AU, U (0) = (u 0 , u 1 ) = U 0 , (2.7)
where U is the vector U = (u, ∂ t u) t and the operator A :

D(A) → H = V × N -1 j=0 L 2 (j, j + 1) is defined by A(u, v) t := (v, (ρ j ∂ 2 x u j ) 0≤j≤N -1 ) t , with D(A) :=    (u, v) ∈ N -1 j=0 H 2 (j, j + 1) × V : satisfies (2.8) to (2.9) hereafter    , ρ 0 ∂ x u 0 (0) = v 0 (0) (2.8) -ρ j ∂ x u j (j) + ρ j-1 ∂ x u j-1 (j) = 0, j = 1, ..., N -1. (2.9)
It is clear that H is a Hilbert space, equipped with the usual inner product

  u v   ,   ũ ṽ   H = N -1 j=0 j+1 j v j (x)ṽ j (x) + ρ j ∂ x u j (x)∂ x ũj (x) dx.
By the same way we define the operator A as following:

A : D(A) ⊂ H → H, AV = B ∂ x V, ∀ V ∈ D(A),
where

D(A) = V = (V j ) 0≤j≤N -1 ∈ H, V j ∈ (H 1 (j, j + 1)) 2 , V j-1 (j) = V j (j), 1 ≤ j ≤ N -1, C 0 V 0 (0) = 0, C N -1 V N -1 (N ) = 0 and B = (B j ) 0≤j≤N -1 .
Now we can prove the well-posedness of system (P ) and that the solution of (P ) satisfies the dissipation law (1.4).

Proposition 2.1. (i) For an initial datum U 0 ∈ H, there exists a unique solution

U ∈ C([0, +∞), H) to problem (2.7). Moreover, if U 0 ∈ D(A), then U ∈ C([0, +∞), D(A)) ∩ C 1 ([0, +∞), H).
(ii) The solution u of (P ) with initial datum in D(A) satisfies (1.4). Therefore the energy is decreasing.

Proof. (i) By Lumer-Phillips' theorem (see [START_REF] Pazy | Semigroups of linear operators and applications to partial differential equations[END_REF][START_REF] Tucsnak | Observation and control for operator semigroups[END_REF]), it suffices to show that A is dissipative and maximal.

We first prove that A is dissipative. Take U = (u, v) t ∈ D(A). Then

AU, U H = N -1 j=0 j+1 j ρ j ∂ 2 x u j (x)v j (x) + ρ j ∂ x v j (x)∂ x u j (x) dx .
By integration by partsand by using the transmission and boundary conditions, we have

ℜ ( AU, U H ) = -|v 0 (0)| 2 ≤ 0. (2.10)
This shows the dissipativeness of A.

Let us now prove that A is maximal, i.e. that λI -A is surjective for some λ > 0.

Let (f , g) t ∈ H. We look for

U = (u, v) t ∈ D(A) solution of (λI -A)   u v   =   f g   , (2.11)
or equivalently    λu jv j = f j ∀j ∈ {0, ..., N -1}, λv jρ j ∂ 2 x u j = g j ∀j ∈ {0, ..., N -1}.

(2.12)

Suppose that we have found u with the appropriate regularity. Then for all j ∈ {0, ..., N -1}, we have

v j := λu j -f j ∈ V. (2.13)
It remains to find u. By (2.12) and (2.13), u j must satisfy, for all j = 0, ..., N -1,

λ 2 u j -ρ j ∂ 2 x u j = g j + λf j .
Multiplying these identities by a test function φ, integrating in space and using integration by parts, we obtain

N -1 j=0 j+1 j λ 2 u j φ j + ρ j ∂ x u j ∂ x φ j dx - N -1 j=0 ρ j ∂ x u j φ j j+1 j = N -1 j=0 j+1 j (g j + λf j ) φ j dx.
Since (u, v) ∈ D(A) and (u, v) satisfies (2.13), we then have

N -1 j=0 j+1 j λ 2 u j φ j + ρ j ∂ x u j ∂ x φ j dx+ (λu 0 (0) -f 0 (0)) φ 0 (0) = N -1 j=0 j+1 j (g j + λf j ) φ j dx. (2.14)
This problem has a unique solution u ∈ V by Lax-Milgram's lemma, because the left-

hand side of (2.14) is coercive on V . If we consider φ ∈ N -1 j=0 D(j, j + 1) ⊂ V , then u satisfies λ 2 u j -ρ j ∂ 2 x u j = g j + λf j in D ′ (j, j + 1), j = 0, • • • , N -1.
This directly implies that u ∈

N -1 j=0 H 2 (j, j + 1) and then u ∈ V ∩ N -1 j=0 H 2 (j, j + 1).
Coming back to (2.14) and by integrating by parts, we find

- N -1 j=0 ρ j ∂ x u j (j)φ j (j) -ρ j ∂ x u j (j + 1)φ j (j + 1) + (λu 0 (0) -f 0 (0)) φ 0 (0) = 0.
Consequently, by taking particular test functions φ, we obtain

ρ 0 ∂ x u 0 (0) = v 0 (0) and ρ j ∂ x u j (j) -ρ j-1 ∂ x u j-1 (j) = 0, j = 1, • • • , N -1.
In summary we have found (u, v) t ∈ D(A) satisfying (2.11), which finishes the proof of (i).

(ii) To prove (ii), it suffices to derivate the energy (1.2) for regular solutions and to use system (P ). The calculations are analogous to those of the proof of the dissipativeness of A in (i), and then, are left to the reader.

Remark 2.2. By the same we can prove that the operator A is a m-dissipatif operator of H and generates a C 0 -semigroup of contractions of H.

Exponential stability

We prove a decay result of the energy of system (P ), independently of N and of the densities, for all initial data in the energy space. Our technique is based on a frequency domain method and a special analysis for the resolvent.

Theorem 3.1. There exists a constant C, ω > 0 such that, for all (u 0 , u 1 ) ∈ H, the solution of system (P ) satisfies the following estimate

E(t) ≤ C e -ω t (u 0 , u 1 ) 2 H , ∀ t > 0. (3.15)
Proof. By classical result (see Huang [START_REF] Huang | Characteristic conditions for exponential stability of linear dynamical systems in Hilbert space[END_REF] and Prüss [START_REF] Prüss | On the spectrum of C 0 -semigroups[END_REF]) it suffices to show that A satisfies the following two conditions:) of a C 0 semigroup of contractions on a Hilbert space:

ρ(A) ⊃ iβ β ∈ R ≡ iR, (3.16)
and lim sup

|β|→∞ (iβ -A) -1 L(H) < ∞, (3.17)
where ρ(A) denotes the resolvent set of the operator A.

Then the proof of Theorem 3.1 is based on the following two lemmas.

Lemma 3.2. The spectrum of A contains no point on the imaginary axis.

Proof. Since A has compact resolvent, its spectrum σ(A) only consists of eigenvalues of A. We will show that the equation

AZ = iβ Z (3.18) with Z =   y v   ∈ D(A)
and β = 0 has only the trivial solution.

By taking the inner product of (3.18) with Z ∈ H and using

ℜ < AZ, Z > H = -|v 0 (0)| 2 , (3.19)
we obtain that v 0 (0) = 0. Next, we eliminate v in (3.18) to get a second order ordinary differential system:

       ρ j d 2 y j
dx 2 + β 2 y j = 0, (j, j + 1), j = 0, ..., N -1, y 0 (0) = dy 0 dx (0) = 0, y N -1 (N ) = 0, y j-1 (j) = y j (j), j = 1, ..., N -1.

(3.20)

The above system has only trivial solution.

Lemma 3.3. The resolvent operator of A satisfies condition (3.17).

Proof. In order to prove (3.17) or by equivalence the following lim sup

|β|→∞ (iβ -A) -1 L(H) < ∞, (3.21)
we will compute and estimate the resolvent of the operator A associated to the problem

(P ′ ). More precisely, let λ = iβ, β ∈ R, G = (G 0 , ..., G N -1 ) ∈ H, we look for W = (W 0 , ..., W N -1 ) ∈ D(A) solution of (iβ -B∂ x )W = G, (3.22)
where B = (B 0 , ..., B N -1 ) and

B j =   0 1 ρ j 0   , j = 0, ...N -1.
We want to prove that there exists a constant C independent of β such that

W H ≤ C G H (3.23)
First step : Computation of the resolvent From (3.22) we have

∂ x W j = iβB -1 j W i -B -1 j G j , j = 0, ..., N -1 therefore W 0 (x) = e iβ(x-1)B -1 0 F 0 - x 1 e iβ(x-s)B -1 0 B -1 0 G 0 (s) ds, ∀x ∈ [0, 1], (3.24)
and

W j (x) = e iβ(x-j)B -1 j F j - x j e iβ(x-s)B -1 j B -1 j G j (s) ds, ∀x ∈ [j, j + 1], j = 1, 2, ..., N -1, (3.25)
where F 0 = W 0 (1) and F j = W j (j), j = 0, ..., N -1. For simplification we set Gj (x) =

x j e iβ(x-s)B -1 j B -1 j G j (s) ds, j = 0, ..., N -1.

(3.26)

Using the transmission conditions at nodes j = 1, ..., N -1 we have

F 1 = F 0 , and F j = W j-1 (j), j = 2, ..., N -1, (3.27)
which implies that

F j =   k=1 k=j-1 e iβB -1 k   F 0 -   j-1 p=2   k=p k=j-1 e iβB -1 k   Gp-1 (p) + Gj-1 (j)   , j = 2, ..., N -1.
(3.28)

For all j = 1, ..., N -1 we set

M j (β) =   k=1 k=j-1 e iβB -1 k   and Γ j (β) = j-1 p=2   k=p k=j-1 e iβB -1 k   Gp-1 (p) + Gj-1 (j), (3.29)
hence (1, 0).e iβB -1 N-1 F N -1 = (1, 0). GN-1 (N ).

F j = M j (β)F 0 -Γ j (β). ( 3
Inserting (3.30) in the previous equation we get [START_REF] Ammari | Spectral analysis and stabilization of a chain of serially connected Euler-Bernoulli beams and strings[END_REF]0).e iβB -1

N-1 M N -1 (β)F 0 = (1, 0). GN-1 (N ) + e iβB -1 N-1 Γ N -1 (β) . (3.32)
If we denote by H N -1 the 2 × 2 matrix whose the first line is the vector line is

(1, -1).e -iβB -1 0 and the second line is (1, 0).e iβB -1

N-1 M N -1 (β) i.e H N -1 =   (1, -1).e -iβB -1 0 (1, 0).e iβB -1 N-1   (3.33)
and Y N -1 the 2 × 1 vectors columns by

Y N -1 =   (1, -1). G0 (0) (1, 0). GN-1 (N ) + e iβB -1 N-1 Γ N -1 (β)   (3.34)
then equation (3.31) and (3.32) are equivalent to the following system:

H N -1 F 0 = Y N -1 . (3.35)
Second step: estimate of F 0

We first start by given an estimation of G = ( G0 , ..., GN-1 ) where Gj are defined in (3.26).

For all j = 0, ..., N -1, the matrix is B j is invertible:

B -1 j =   0 1 ρ j 1 0  
and we easily find after some computation that

e iβxB -1 j =       cos( βx √ ρ j ) i sin( βx √ ρ j ) √ ρ j i √ ρ j sin( βx √ ρ j ) cos( βx √ ρ j )       . (3.36)
Since β ∈ R, from the previous identity, we directly get the following estimates

| Gj (j)| G H , | Gj (j + 1)| G H , j = 0, ..., N -1 (3.37) G H G H . (3.38)
From the definition of Γ j in (3.29) we also get

|Γ j (β)| G H , j = 1, ..., N -1. (3.39)
It follows that

Y N -1 G H . (3.40)
Note that from (3.36) the entries of H N -1 are bounded and so it is for the entries of the matrix (comH N -1 ) T . Assume for the moment that there exists a constant γ N -1 > 0 such that

∀β ∈ R, | det(H N -1 )| ≥ γ N -1 , (3.41)
then it follows with (3.40) that

F 0 = 1 det H N -1 (comH N -1 ) T Y N -1 G H . (3.42)
It remains to prove (3.41).

The idea of the proof is that (3.41) is well known for N = 1 and that this property spreads by iteration.

First, similarly to (3.33) we define for all N ∈ N * the matrix

HN-1 =   (1, -1).e -iβB -1 0 (0, 1).e iβB -1 N-1   (3.43)
and we set

D N -1 = det(H N -1 ), DN-1 = det( HN-1 ), ∀N ∈ N * .
Particularly, for N = 1 we have

H 0 =         cos( β √ ρ 0 ) + i √ ρ 0 sin( β √ ρ 0 ) -cos( β √ ρ 0 ) -i sin( β √ ρ 0 ) √ ρ 0 cos( β √ ρ 0 ) -i sin( β √ ρ 0 ) √ ρ 0         , and
H0 =       cos( β √ ρ 0 ) + i √ ρ 0 sin( β √ ρ 0 ) -cos( β √ ρ 0 ) -i sin( β √ ρ 0 ) √ ρ 0 i √ ρ 0 sin( β √ ρ 0 ) cos( β √ ρ 0 )       . Thus D 0 = cos( 2β √ ρ 0 ) + i sin( 2β √ ρ 0 ) √ ρ 0 , D0 = cos( 2β √ ρ 0 ) + i √ ρ 0 sin( 2β √ ρ 0 ),
and

|D 0 | 2 = cos 2 ( 2β √ ρ 0 ) + sin 2 ( 2β √ ρ 0 ) ρ 0 ≥ min(1, 1 ρ 0 ) > 0, | D0 | 2 = cos 2 ( 2β √ ρ 0 ) + ρ 0 sin 2 ( 2β √ ρ 0 ) ≥ min(1, ρ 0 ) > 0.
It is useful for the sequel to remark that

ℜ(D 0 D0 ) = 1.
Using (3.36) we have the following identity

       D N -1 = cos( β √ ρ N -1 )D N -2 + i √ ρ N -1 sin( β √ ρ N -1 ) DN-2 , DN-1 = i √ ρ N -1 sin( β √ ρ N -1 )D N -2 + cos( β √ ρ N -1
) DN-2 .

A simple computation shows that

ℜ(D N -1 DN-1 ) = ℜ(D N -2 DN-2 ) consequently, ∀N ∈ N * , ℜ(D N -1 DN-1 ) = 1. Now, since |D N -1 | 2 = (cos( β √ ρ N -1
), sin(

β √ ρ N -1
))

    |D N -2 | 2 1 √ ρ N -1 ℑ(D N -2 DN-2 ) 1 √ ρ N -1 ℑ(D N -2 DN-2 ) | 1 √ ρ N -1 DN-2 | 2         cos( β √ ρ N -1 ) sin( β √ ρ N -1 )     , it follows that |D N -1 | 2 ≥ µ min,N -2 , (3.44)
where µ min,N -2 is the smallest eigenvalue of the matrix in the previous identity. The determinant of this matrix is:

1 ρ N -1 ℜ(D N -2 DN-2 ) 2 = 1 ρ N -1 .
Since D N -2 and DN-2 are clearly bounded the trace of this matrix is bounded, i.e

∃C ′ N -1 > 0, |D N -2 | 2 + | 1 √ ρ N -1 DN-2 | 2 ≤ C ′ N -1 .
It follows that

µ min,N -2 ≥ 1 ρ N -1 C ′ N -1 . Setting C N -1 = 1 ρ N -1 C ′ N -1
, then (3.44) implies (3.41). Consequently we have prove the estimate (3.42) for F 0 . Which implies (3.21) and thereafter (3.17), and end the proof of Theorem 3.1.

Comments and related questions

The same strategy can be applied to stabilize the following models and to verify and compute the transfer function.

Transfer function

We can use the same strategy to verify that the operator L 2 (j, j + 1) → H is defined by

H(λ) = λ C * (λ 2 I + A) -1 C ∈ L(U ), λ ∈ C + ,
A(u) := (-ρ j ∂ 2 x u j ) 0≤j≤N -1 , with D(A) :=    u ∈ N -1 j=0
H 2 (j, j + 1) : satisfies (4.46) to (4.47) hereafter

   , ρ 0 ∂ x u 0 (0) = 0 (4.46) -ρ j ∂ x u j (j) + ρ j-1 ∂ x u j-1 (j) = 0, j = 1, ..., N -1. (4.47) C ∈ L(C, V ′ = D(A 1 2 ) ′ ), Ck = √ ρ 0 A -1 N k = k           1 √ ρ 0 δ 0 . . . 0           , ∀ k ∈ C, C * u = 1 √ ρ 0 u 0 (0) 0 ... 0 , ∀ u ∈ V,
where A -1 is the extension of A to (D(A)) ′ (the duality is in the sense of H) and N is the Neumann map,

       ρ j ∂ 2 x (N k) j = 0, (j, j + 1), 0 ≤ j ≤ N -1, ∂ x (N k) 0 (0) = k, (N k) N -1 (N ) = 0, ρ j-1 ∂ x (N k) j-1 (j) = ρ j ∂ x (N k) j (j), 1 ≤ j ≤ N -1.
Lemma 4.1. The transfer function H satisfies the following estimate:

sup ℜλ=γ λ C * (λ 2 I + A) -1 C L(U ) < ∞, (4.48)
for γ > 0.

Proof. In the same way as the proof of Lemma 3.3, we give an equivalent formulation of the function H. For that purpose, we consider

W = (W j ) 0≤j≤N -1 ∈ H, W j ∈ (H 1 (j, j + 1)) 2 solution of (λ -B∂ x )W = 0, W j-1 (j) = W j (j), 1 ≤ j ≤ N -1, C0 W 0 (0) =   z 0   , C N -1 W N -1 (N ) = 0
H(λ) : z ∈ C → (1, 0).W 0 (0) ∈ C.
Consequently to prove (4.48) it suffices to check that for a fixed γ > 0, there exists a

constant c γ > 0 such that ∀λ ∈ C, ℜ(λ) = γ, |(1, 0).W 0 (0)| ≤ c γ |z|. (4.50)
Using (3.24), (3.25), (3.28), we have

W 0 (x) = e λ(x-1)B -1 0 F 0 , W j (x) = e λ(x-j)B -1 j F j , j = 1, ..., N -1,
where

F 0 = W 0 (1), F 1 = F 0 , and F j =   k=1 k=j-1 e λB -1 k   F 0 , j = 2, ..., N -1.
Therefore, from the boundary conditions at x = 0 and x = N, we find that F 0 is the solution of

H N -1 F 0 =   z 0   , where H N -1 is the 2 × 2 matrix     (0, 1).e -λB -1 0 (1, 0). k=1 k=N -1 e λB -1 k     ,
with the convention that

k=1 k=N -1 e λB -1 k is the identity matrix if N = 1.

Estimate of F 0

Since for all j e λxB -1

j =   cosh( λx c j ) sinh( λx c j ) c j c j sinh( λx c j ) cosh( λx c j )   , it is clear that there exists a constant c ′ γ > 0 sucht that ∀λ ∈ C, ℜ(λ) = γ, H N -1 ≤ c ′ γ . (4.51)
We need a similar estimate for H -1 N -1 ; this will be done by giving a lower uniform bound of |D N -1 | on the line ℜ(λ) = γ, where we have set D N -1 = det(H N -1 ). Thus we introduce the matrix

HN-1 =   (0, 1).e -λB -1 0 (0, 1). k=1 k=N -1 e λB -1 k   , N ≥ 1,
and set DN-1 = det( HN-1 ). Now, we prove by iteration that

ℜ(D N -1 DN-1 ) ≥ k N -1 > 0.
For N = 1 we have

H 0 =   -sinh( λ c 0 ) cosh( λ c 0 ) 1 0   , H0 =   -sinh( λ c 0 ) cosh( λ c 0 ) 0 1   , thus ℜ(D 0 D0 ) = 1 2 sinh( 2γ c 0 ) > 0.
Assume that there exists a constant k N -2 > 0 such that

ℜ(D N -2 DN-2 ) ≥ k N -2 > 0. (4.52)
We have the following easily checked identities

D N -1 = cosh( λ c N -1 )D N -2 + 1 c N -1 sinh( λ c N -1 ) DN-2 DN-1 = c N -1 sinh( λ c N -1 )D N -2 + cosh( λ c N -1
) DN-2 .

A computation leads to

ℜ(D N -1 DN-1 ) = ℜ(cosh( λ c N-1 )sinh( λ c N-1 ))(c N -1 |D N -2 | 2 + 1 c N -1 | DN-2 | 2 ) + (| cosh( λ c N-1 )| 2 + | sinh( λ c N-1 )| 2 )ℜ(D N -2 DN-2 ) = 1 2 sinh( 2γ c N-1 )(c N -1 |D N -2 | 2 + 1 c N -1 | DN-2 | 2 ) + cosh( 2γ c N-1 )ℜ(D N -2 DN-2 ) ≥ cosh( 2γ c N-1 )k N -2 = k N -1 > 0.
We have proved (4.52). It follows

|D N -1 DN-1 | ≥ k N -1 > 0.
But | DN-1 | is obviously upper bounded on the line ℜ(λ) = γ, consequently there exists

a constant k ′ N -1 > 0 such that ∀λ, ℜ(λ) = γ, |D N -1 | ≥ k ′ N -1 > 0.
Finally, with (4.51) we deduce that H -1 N -1 is bounded on the line ℜ(λ) = γ and it follows that there exits c γ > 0 such that ∀z ∈ C, ∀λ :

ℜ(λ) = γ, |F 0 | ≤ c γ z.
Conclusion: (4.50) is a direct consequence of the previous estimate. The proof is complete As application is that the open loop system associated to (P ) is satisfies a regularity property.

Corollary 4.2. Let T > 0. Then, for all v ∈ L 2 (0, T ) the following problem

                   (∂ 2 t ψ j -ρ j ∂ 2 x ψ j )(t, x) = 0, x ∈ (j, j + 1), t ∈ (0, ∞), j = 0, ..., N -1, ρ 0 ∂ x ψ 0 (t, 0) = v(t), ψ N -1 (t, N ) = 0, t ∈ (0, ∞),
ψ j-1 (t, j) = ψ j (t, j), t ∈ (0, ∞), j = 1, ..., N -1, -ρ j-1 ∂ x ψ j-1 (t, j) + ρ j ∂ x ψ j (t, j) = 0, t ∈ (0, ∞), j = 1, ..., N -1, ψ j (0, x) = 0, ∂ t ψ j (0, x) = 0, x ∈ (j, j + 1), j = 0, ..., N -1. admits a unique solution (ψ, ∂ t ψ) ∈ C(0, T ; H) which satisfies the following regularity property (says also open loop admissibility): there exists a constant C > 0 such that

T 0 |∂ t ψ 0 (t, 0)| 2 dt ≤ C v 2 L 2 (0,T ) , ∀ v ∈ L 2 (0, T ).
Moreover, according to [5, Theorem 2.2], we have that:

Corollary 4.3. The system (P ) is exponentially stable in the energy space if and only if there exists T, C > such that

T 0 |∂ t ϕ 0 (t, 0)| 2 dt ≥ C (ϕ 0 , ϕ 1 ) 2 H , ∀ (ϕ 0 , ϕ 1 ) ∈ D(A),
where

D(A) :=    (u, v) ∈ N -1 j=0
H 2 (j, j + 1) × V : satisfies -ρ j ∂ x u j (j) + ρ j-1 ∂ x u j-1 (j) = 0, j = 1, ..., N -1. (4.54)

and ϕ = (ϕ 0 , ..., ϕ N -1 ) satisfies the following problem

                   (∂ 2 t ϕ j -ρ j ∂ 2 x ϕ j )(t, x) = 0, x ∈ (j, j + 1), t ∈ (0, ∞), j = 0, ..., N -1, ρ 0 ∂ x ϕ 0 (t, 0) = 0, ϕ N -1 (t, N ) = 0, t ∈ (0, ∞), ϕ j-1 (t, j) = ϕ j (t, j), t ∈ (0, ∞), j = 1, ..., N -1, -ρ j-1 ∂ x ϕ j-1 (t, j) + ρ j ∂ x ϕ j (t, j) = 0, t ∈ (0, ∞), j = 1, ..., N -1, ϕ j (0, x) = ϕ 0 j (x), ∂ t ϕ j (0, x) = ϕ 1 j (x),
x ∈ (j, j + 1), j = 0, ..., N -1.

Schrödinger system

We consider the evolution problem (S) described by the following system of N equations:

(S)

                   (∂ t u j + iρ j ∂ 2 x u j )(t, x) = 0, x ∈ (j, j + 1), t ∈ (0, ∞), j = 0, ..., N -1, ρ 0 ∂ x u 0 (t, 0) = iu 0 (t, 0), u N -1 (t, N ) = 0, t ∈ (0, ∞), u j-1 (t, j) = u j (t, j), t ∈ (0, ∞), j = 1, ..., N -1, -ρ j-1 ∂ x u j-1 (t, j) + ρ j ∂ x u j (t, j) = 0, t ∈ (0, ∞), j = 1, ..., N -1, u j (0, x) = u 0 j (x), j = 0, ..., N -1,
where ρ j > 0, ∀ j = 0, ..., N -1.

We define the natural energy E(t) of a solution u = (u 0 , ..., u N -1 ) of (S) by

E(t) = 1 2 N -1 j=0 j+1 j |u j (t, x)| 2 dx, (5.1)
We can easily check that every sufficiently smooth solution of (S) satisfies the following dissipation law

E ′ (t) = -u 0 (t, 0) 2 ≤ 0, (5.2)
and therefore, the energy is a nonincreasing function of the time variable t.

In order to study system (S) we introduce the following Hilbert space

H = u = (u 0 , ..., u N -1 ) ∈ N -1 j=0 L 2 (j, j + 1)) , ∀u ∈ D(A), ℜ ( Au, u H ) = -|u 0 (0)| 2 ≤ 0.
(5.7)

Now, let f ∈ H. We look for u ∈ D(A) solution of -Au = f.

(5.8)

or equivalently

iρ j ∂ 2 x u j = f j , ∀j ∈ {0, ..., N -1}, (5.9)
and u satisfies the boundary and transmission conditions (5.4)-(5.6).

The general solution of (5.9) is

u j (x) = 1 iρ j x j u j f j (s)ds du + p i (x), j = 0, ..., N -1, x ∈ [j, j + 1],
where each p j is a polynomial of degree 1. It remains to find p j , j = 0, ..., N -1 such that the equations (5.4)-(5.6) are satisfied. It is equivalent to solve a linear system with 2N equations and 2N unknowns. This system admits an unique solution if and only if the corresponding homogeneous system admits only the trivial solution.

So we suppose that p j , j = 0, ..., N -1 are polynomials of degree 1 and satisfy (5.4)-(5.6).

Then by integrations by parts and using (5.4)-(5.6) we get

N -1 j=0 ρ j j+1 j |p ′ j (x)| 2 dx = - N -1 j=0 ρ j j+1 j p ′′ j (x)p j (x)dx = 0.
Consequently, the polynomials p j are constant and finally vanish from the continuity conditions and the right Dirichlet condition. Hence we have proved that (5.8) admits an unique solution. Consequently A is maximal.

(ii) To prove (ii), we use the same argument as in the proof of Theorem 2.1.

Exponential stability of the Schrödinger system

The stability result of system (S) is given by Theorem 5.2. There exist constants C > 0 and ω > 0 such that, for all u 0 ∈ H, the solution of system (S) satisfies the following estimate ρ j (∂ x u j )(j + 1)

E(t) ≤ C e -ω t u 0 2 H , ∀ t > 0. ( 5
  =        cos( √ β √ ρ j ) sin( √ β √ ρ j ) √ β √ ρ j - √ β √ ρ j sin( √ β √ ρ j ) cos( √ β √ ρ j )        F j +   G j (j + 1) (∂ x G j )(j + 1)   .
For simplification we introduce the matrix M j and the vector W j as Thus we find that

M j =        cos( √ β √ ρ j ) sin( √ β √ ρ j ) √ β √ ρ j - √ β √ ρ j sin( √ β √ ρ j ) cos( √ β √ ρ j )     
c 1 0 = ω N,1 α N,1 + iγ N,1
.

This last identity completely determine the solution u of (5.13).

Second step : Estimate of F 0 for β large.

From one hand, since the order of each matrix M j is

  O(1) O( 1 √ β ) O( √ β) O(1)   (5.22)
then it is easy to see that all the matrices involved in (5.21) have the same order.

On the other hand, from (5.16) we have clearly

  .30) Note that the solution W is completely determined if F 0 is known. Indeed, it suffices to insert the identity (3.30) in(3.25). Thus, we give the equation satisfied by F 0 . The boundary conditions at nodes x = 0 and x = N are respectively C 0 W 0 (0C 0 , C N -1 are the matrices given in (1.1). Since the second lines of C 0 and C N -1 vanish the previous equations may be written as (1, -1).W 0 (0) = 0, and (1, 0).W N -1 (N ) = 0, where "." represents the matrix-product of a vector line by a vector column. These equations are equivalent to (1, -1).e -iβB -1 0 F 0 = (1, -1), G0 (0)(3.31) and

Finally, using

  estimates (3.42), (3.37), (3.38) in (3.27) and (3.28) and the fact that the matrices involved in (3.28) are uniformly bounded we get F j G H , ∀j = 1, ...N -1. Using (3.42) and the previous estimates in (3.24) and (3.25), we get (3.23).

  satisfies the property (4.48) of the following lemma, where here A is the self-adjoint operator corresponding to the conservative problem associated to problem (P), namely we replace in (P) the boundary feedback condition byρ 0 ∂ x u 0 (t, 0) = 0, (4.45) i.e., A : D(A) ⊂ H = N -1 j=0

( 4 . 1

 41 49)where z ∈ C, B is defined as in the proof of Lemma 3.3, C N -1 is the matrix given in (Therefore, for λ ∈ C, ℜ(λ) = γ > 0, the transfer function is

  (4.53) to (4.54) hereafter

c 1 j

 1 , c 2 j , ∈ C. Note that c 1 j = u j (j) and ρ j (∂ x u j )(j) = c 2 j . = 0, ..., N -1, then using the transmission conditions (5

F- 2 Mwe now compute c 1 0 2 M

 212 j+1 = M j F j + W j , j = 0, ..., Nj )W k + W N -1 . (5.19)From the first boundary condition (5.4) we have F 0 = c by using the second boundary condition(5.4). For that we set0 j=N -1 M j =   α N,1 γ N,1 α N,2 γ N,2 j )W k + W N -1 =

  x G j )(j + 1)| g j g , j = 0, ...., N -1.(5.24)Therefore using the order (5.22) and estimate (5.23)-(5.24) for W k in (5.21) we get ω remark that for all j = 0, ..., N -1, det M j = 1, which implies from (5.20) thatα N,1 γ N,2α N,2 γ N,1 = 1. Thus |α N,1 + iγ N,1 ||α N,2 + iγ N,2 | ≥ Re[(α N,1 + iγ N,1 )(α N,2 + iγ N,2 )] = 1,implies with (5.22) and (5.20) that 1 |α N,1 + iγ N,1 | ≤ |α N,2 + iγ N,2 | ≤ O( β).

equipped with the inner product < u, ũ > H = N -1 j=0 j+1 j u j (x) ũj (x)dx.

The system (S) is a first order evolution equation which as the form    u ′ = Au, u(0) = u 0 , (5.3) where u 0 = (u 0 0 , u 0 1 , ..., u 0 N -1 ) ∈ H and the operator A : D(A) → H is defined by

H 2 (j, j + 1) : satisfies (5.4) to (5.6) hereafter

u j-1 (j) = u j (j), j = 1, ..., N -1, (

-ρ j-1 ∂ x u j-1 (j) + ρ j ∂ x u j (j) = 0, j = 1, ..., N -1.

(5.6)

Now we can prove the well-posedness of system (S) and that the solution of (S) satisfies the dissipation law (5.2).

Proposition 5.1. (i) For an initial datum u 0 ∈ H, there exists a unique solution

(ii) The solution u of (S) with initial datum in D(A) satisfies (5.2). Therefore the energy is decreasing.

Proof. (i) By Lumer-Phillips' theorem, it suffices to show that A is dissipative and maximal.

A is clearly dissipative. Indeed, by integration by parts and by using the transmission and boundary conditions, we have Proof. As in the proof of Theorem (3.1) the result is based on the following two lemmas.

Lemma 5.3. The spectrum of A contains no point on the imaginary axis.

Proof. Since A has compact resolvent, its spectrum σ(A) only consists of eigenvalues of A. We will show that the equation

with u = (u 0 , ..., u N -1 ) ∈ D(A) and β = 0, β ∈ R has only the trivial solution.

By taking the inner product of (5.11) with u ∈ H and using (5.7) we get that u 0 (0) = 0.

From the left boundary condition we deduce also that ∂ x u 0 (0) = 0. Therefore we get that

Therefore by iteration we easily find u j = 0, j = 1, ..., N -1.

The system (5.11) has only trivial solution.

Lemma 5.4. The resolvent operator of A satisfies

Proof. In order to prove (5.12) we look for u = (u 0 , ..., u N -1 ) ∈ D(A) solution of (iβ -A)u = g, (5.13) where β ∈ R and g = (g 0 , ..., g N -1 ) ∈ H.

We will consider two cases since for each case the method is different.

First case : β > 0.

First step : Computation of the resolvent

The solution of( 5.13) satisfies

An easy calculation shows that

The previous estimate and (5.25) lead to

Last step : Estimate of u.

First, from (5.16) we have G j g j g , j = 0, ..., N -1.

Then, using (5.18), (5.22) and ( 5.26) we get by iteration the components of F j , j = 0, ..., N -1 satisfy :

Consequently, using the two previous estimates in (5.15) we directly obtain that the solution of (5. (5.28)

Finally the result follows from (5.27)-(5.28).