Adrien Durier

Daniel Hirschkoff

Davide Sangiorgi

Eager Functions as Processes

Keywords: pi-calculus, lambda-calculus, full abstraction, call-byvalue

published or not. The documents may come   L'archive ouverte pluridisciplinaire

Introduction

Milner's work on functions as processes [START_REF] Milner | Functions as processes[END_REF][START_REF] Milner | Functions as Processes[END_REF], that shows how the evaluation strategies of call-by-name -calculus and call-byvalue -calculus [START_REF] Abramsky | The Lazy -calculus[END_REF][START_REF] Plotkin | Call-by-Name, Call-by-Value and the lambda-Calculus[END_REF] can be faithfully mimicked in the -calculus, is generally considered a landmark in Concurrency Theory, and more generally in Programming Language Theory. The comparison with the -calculus is a significant expressiveness test for the -calculus. More than that, it promotes the -calculus to be a basis for general-purpose programming languages in which communication is the fundamental computing primitive. From the -calculus point of view, the comparison provides the means to study -terms in contexts other than purely sequential ones, and with the instruments available to reason about processes. Further, Milner's work, and the works that followed it, have contributed to understanding and developing the theory of the -calculus.

More precisely, Milner shows the operational correspondence between reductions in the -terms and in the encoding -terms. He then uses the correspondence to prove that the encodings are sound, i.e., if the processes encoding two -terms are behaviourally equivalent, then the source -terms are also behaviourally equivalent in the -calculus. Milner also shows that the converse, completeness, fails, intuitively because the encodings allow one to test the -terms in all contexts of the -calculus -more diverse than those of the -calculus.

The main problem that Milner work left open is the characterisation of the equivalence on -terms induced by the encoding, whereby two -terms are equal if their encodings are behaviourally equivalent -calculus terms. The question is largely independent of the precise form of behavioural equivalence adopted in thecalculus because the encodings are deterministic (or at least confluent). In the paper we consider contextual equivalence (that coincides with may testing and trace equivalence) and barbed congruence (that coincides with bisimilarity).

For the call-by-name -calculus, the answer was found shortly later [START_REF] Sangiorgi | An investigation into Functions as Processes[END_REF][START_REF] Sangiorgi | Lazy functions and mobile processes[END_REF]: the equality induced is the equality of Lévy-Longo Trees [START_REF] Longo | Set-theoretical models of lambda-calculus: theories, expansions, isomorphisms[END_REF], the lazy variant of Böhm Trees. It is actually also possible to obtain Böhm Trees, by modifying the call-by-name encoding so to allow also reductions underneath a -abstraction, and by including divergence among the observables [START_REF] Sangiorgi | Trees from Functions as Processes[END_REF]. These results show that, at least for call-by-name, the -calculus encoding, while not fully abstract for the contextual equivalence of the -calculus, is in remarkable agreement with the theory of the -calculus: several well-known models of the -calculus yield Lévy-Longo Trees or Böhm Trees as their induced equivalence [START_REF] Barendregt | The lambda calculus: its syntax and semantics[END_REF][START_REF] Lévy | An algebraic interpretation of the lambda beta-calculus and a labeled lambda-calculus[END_REF][START_REF] Longo | Set-theoretical models of lambda-calculus: theories, expansions, isomorphisms[END_REF].

For call-by-value, in contrast, the problem of identifying the equivalence induced by the encoding has remained open, for two main reasons. First, tree structures in call-by-value are less studied and less established than in call-by-name. Secondly, proving completeness of an encoding of into requires sophisticated proof techniques. For call-by-name, for instance, a central role is played by bisimulation up-to contexts. For call-by-value, however, existing proof techniques, including 'up-to contexts', appeared not to be powerful enough.

In this paper we study the above open problem for call-by-value. Our main result is that the equivalence induced on -terms by their call-by-value encoding into the -calculus is eager normal-form bisimilarity [START_REF] Søren | Eager Normal Form Bisimulation[END_REF][START_REF] Søren | Typed Normal Form Bisimulation[END_REF]. This is a tree structure for call-by-value, proposed by Lassen as the call-by-value counterpart of Lévy-Longo Trees. Precisely we obtain the variant that is insensitive to -expansion, called -eager normal-form bisimilarity.

To obtain the results we have however to make a few adjustments to Milner's encoding and/or specialise the target language of the encoding. These adjustments have to do with the presence of free outputs (outputs of known names) in the encoding. We show in the paper that this brings problems when analysing -terms with free variables: desirable call-by-value equalities fail. An example is given by the law:

( ) = (1)
where is . and is a value. Two possible solutions are:

1. rule out the free outputs; this essentially means transplanting the encoding onto the Internal -calculus [START_REF] Sangiorgi | Calculus, Internal Mobility, and Agent-Passing Calculi[END_REF], a version of the -calculus in which any name emitted in an output is fresh; 2. control the use of capabilities in the -calculus; for instance taking Asynchronous Local [START_REF] Merro | On asynchrony in name-passing calculi[END_REF] as the target of the translation. (Controlling capabilities allows one to impose a directionality on names, which, under certain technical conditions, may hide the identity of the emitted names.)

In the paper we consider both approaches, and show that in both cases, the equivalence induced coincides with -eager normalform bisimilarity.

In summary, there are two contributions in the paper:

1. Showing that Milner's encoding fails to equate terms that should be equal in call-by-value. 2. Rectifying the encoding, by considering different target calculi, and investigating Milner's problem in such a setting.

The rectification we make does not really change the essence of the encoding -in one case, the encoding actually remains the same. Moreover, the languages used are well-known dialects of thecalculus, studied in the literature for other reasons. In the encoding, they allow us to avoid certain accidental misuses of the names emitted in the communications. The calculi were not known at the time of Milner's paper [START_REF] Milner | Functions as Processes[END_REF].

A key role in the completeness proof is played by a technique of unique solution of equations, recently proposed [START_REF] Durier | Divergence and Unique Solution of Equations[END_REF]. The structure induced by Milner's call-by-value encoding was expected to look like Lassen's trees; however existing proof techniques did not seem powerful enough to prove it. The unique solution technique allows one to derive process bisimilarities from equations whose infinite unfolding does not introduce divergences, by proving that the processes are solutions of the same equations. The technique can be generalised to possibly-infinite systems of equations, and can be strengthened by allowing certain kinds of divergences in equations. In this respect, another goal of the paper is to carry out an extended case study on the applicability and expressiveness of the techniques. Then, a by-product of the study are a few further developments of the technique. In particular, one such result allows us to transplant uniqueness of solutions from a system of equations, for which divergences are easy to analyse, to another one. Another result is about the application of the technique to preorders.

Finally, we consider preorders -thus referring to the preorder on -terms induced by a behavioural preorder on their -calculus encodings. We introduce a preorder on Lassen's trees (preorders had not been considered by Lassen) and show that this is the preorder on -terms induced by the call-by-value encoding, when the behavioural relation on -calculus terms is the ordinary contextual preorder (again, with the caveat of points (1) and (2) above). With the move from equivalences to preorders, the overall structure of the proofs of our full abstraction results remains the same. However, the impact on the application of the unique-solution technique is substantial, because the phrasing of this technique in the cases of preorders and of equivalences is quite different.

Further related work. The standard behavioural equivalence in the -calculus is contextual equivalence. Encodings into the -calculus (be it for call-by-name or call-by-value) break contextual equivalence because -calculus contexts are richer than those in the (pure) -calculus. In the paper we try to understand how far beyond contextual equivalence the discriminating power of thecalculus brings us, for call-by-value. The opposite approach is to restrict the set of 'legal' -contexts so to remain faithful to contextual equivalence. This approach has been followed, for call-byname, and using type systems, in [START_REF] Berger | Sequentiality and the pi-Calculus[END_REF][START_REF] Toninho | On Polymorphic Sessions and Functions -A Tale of Two (Fully Abstract) Encodings[END_REF].

Open call-by-value has been studied in [START_REF] Accattoli | Open Call-by-Value[END_REF], where the focus is on operational properties of -terms; behavioural equivalences are not considered. An extensive presentation of call-by-value, including denotational models, is Ronchi della Rocca and Paolini's book [START_REF] Ronchi | The Parametric Lambda Calculus -A Metamodel for Computation[END_REF].

In [START_REF] Durier | Divergence and Unique Solution of Equations[END_REF], the unique-solution technique is used in the completeness proof for Milner's call-by-name encoding. That proof essentially revisits the proof of [START_REF] Sangiorgi | Lazy functions and mobile processes[END_REF], which is based on bisimulation upto context. We have explained above that the case for call-by-value is quite different.

Structure of the paper. We recall basic definitions about the callby-value -calculus and the -calculus in Section 1. The technique of unique solution of equations is introduced in Section 2, together with some new developments. Section 3 presents our analysis of Milner's encoding, beginning with the shortcomings related to the presence of free outputs. The first solution to these shortcomings is to move to the Internal -calculus: this is described in Section 4. For the proof of completeness, in Section 4.2, we rely on unique solution of equations; we also compare such technique with the 'up-to techniques'. The second solution is to move to the Asynchronous Local -calculus: this is discussed in Section 5. We show in Section 6 how our results can be adapted to preorders and to contextual equivalence. Finally in Section 7 we highlight conclusions and possible future work.

Background material

Throughout the paper, R ranges over relations. The composition of two relations R and R ′ is written R R ′ . We often use infix notation for relations; thus R means ( , ) ∈ R. A tilde represents a tuple. The -th element of a tuple is referred to as . Our notations are extended to tuples componentwise. Thus R means R for all components.

The call-by-value -calculus

We let and range over the set of -calculus variables. The set Λ of -terms is defined by the grammar :=

| . | 1 2 .
Free variables, closed terms, substitution, -conversion etc. are defined as usual [START_REF] Barendregt | The lambda calculus: its syntax and semantics[END_REF][START_REF] Hindley | Introduction to Combinators and Lambda-Calculus[END_REF]. Here and in the rest of the paper (including when reasoning about processes), we adopt the usual "Barendregt convention". This will allow us to assume freshness of bound variables and names whenever needed. The set of free variables in the term is fv( ). We group brackets on the left; therefore is ( ) . We abbreviate 1 . Therefore, given a term , either =⇒ ′ where ′ is a term in eager normal form, or there is an infinite reduction sequence starting from . In the first case, has eager normal form ′ , written ⇓ ′ , in the second diverges, written ⇑. We write ⇓ when ⇓ ′ for some ⇓ . ′ and ⇓ . ′ for some , ′ , ′ with ′ R ′ ; 4.

⇓ and ⇓ for some . Eager normal-form bisimilarity, , is the largest eager normal-form bisimulation.

Essentially, the structure of a -term that is unveiled by Definition 1.3 is that of a (possibly infinite) tree obtained by repeatedly applying v -reduction, and branching a tree whenever instantiation of a variable is needed to continue the reduction (clause (2)). We call such trees Eager Trees (ETs) and accordingly also call eager normal-form bisimilarity the Eager-Tree equality.

Example 1.4. Relation is strictly finer than contextual equivalence ≃ Λ ct : the inclusion ⊆ ≃ Λ ct follows from the congruence properties of [START_REF] Søren | Eager Normal Form Bisimulation[END_REF]; for the strictness, examples are the following equalities, that hold for ≃ Λ ct but not for :

Ω = ( . Ω)( ) = ( . )( ) .
Example 1.5 ( rule). The -rule is not valid for . For instance, we have Ω . Ω . The rule is not even valid on values, as we also have .

. It holds however for abstractions: . ( . ) . when ∉ fv( ).

The failure of the -rule .

is troublesome as, under any closed value substitution, the two terms are indeed eager normalform bisimilar (as well as contextually equivalent). Thus -eager normal-form bisimilarity [START_REF] Søren | Eager Normal Form Bisimulation[END_REF] takes -expansion into account so to recover such missing equalities. Definition 1.6 ( -eager normal-form bisimulation). A relation R between -terms is an -eager normal-form bisimulation if, whenever R , either one of the clauses of Definition 1.3, or one of the two following additional clauses, hold:

5.

⇓ and ⇓ . ′ for some , , and ′ such that ′ ⇓ e [ ], with R and R e [ ] for some value , evaluation context e , and fresh . 6. the converse of (5), i.e., ⇓ and ⇓ . ′ for some , , and ′ such that ′ ⇓ e [ ], with R and e [ ] R for some value , evaluation context e , and fresh . Then -eager normal-form bisimilarity, , is the largest -eager normal-form bisimulation.

We sometimes call relation the -Eager-Tree equality. )), and so on. Hence, we have .

The -calculus, I and AL

In all encodings we consider, the encoding of a -term is parametric on a name, i.e., it is a function from names to -calculus processes. We also need parametric processes (over one or several names) for writing recursive process definitions and equations. We call such parametric processes abstractions. The actual instantiation of the parameters of an abstraction is done via the application construct . We use , for processes, for abstractions. Processes and abstractions form the set of -agents (or simply agents), ranged over by . Small letters , , . . . , , , . . . range over the infinite set of names. The grammar of the -calculus is thus:

:= | (agents) := 0 | ( ). | . | (processes) | 1 | 2 | ! ( ). | := ( ) | (abstractions)
In prefixes ( ) and , we call the subject and the object. When the tilde is empty, the surrounding brackets in prefixes will be omitted. We often abbreviate as ( , ) . An input prefix ( ). , a restriction , and an abstraction ( ) are binders for names and , respectively, and give rise in the expected way to the definition of free names (fn) and bound names (bn) of a term or a prefix, and -conversion. An agent is name-closed if it does not contain free names. As in the -calculus, following the usual Barendregt convention we identify processes or actions which only differ on the choice of the bound names. The symbol = will mean "syntactic identity modulo -conversion". Sometimes, we use def = as abbreviation mechanism, to assign a name to an expression to which we want to refer later.

We use constants, ranged over by for writing recursive definitions. Each constant has a defining equation of the form △ = ( ) , where ( ) is name-closed; are the formal parameters of the constant (replaced by the actual parameters whenever the constant is used).

Since the calculus is polyadic, we assume a sorting system [START_REF] Milner | The polyadic -calculus: a tutorial[END_REF] to avoid disagreements in the arities of the tuples of names carried by a given name and in applications of abstractions. We will not present the sorting system because it is not essential. The reader should take for granted that all agents described obey a sorting. A context of is a -agent in which some subterms have been replaced by the hole [•] or, if the context is polyadic, with indexed holes [•] 1 , . . . , [•] ; then [ ] or [ ] is the agent resulting from replacing the holes with the terms or .

We omit the operators of sum and matching (not needed in the encodings). We refer to [START_REF] Milner | The polyadic -calculus: a tutorial[END_REF] for detailed discussions on the operators of the language. We assign parallel composition the lowest precedence among the operators.

Operational semantics. The operational semantics of the -calculus is standard [START_REF] Sangiorgi | The Pi-Calculus -a theory of mobile processes[END_REF] (including the labelled transition system). The reference behavioural equivalence for -calculi will be the usual barbed congruence. We recall its definition, on a generic subset L of -calculus processes. A L-context is a process of L with a single hole [•] in it (the hole has a sort too, as it could be in place of an abstraction). We write ⇓ if can make an output action whose subject is , possibly after some internal moves. (We make only output observable because this is standard in asynchronous calculi; adding also observability of inputs does not affect barbed congruence on the synchronous calculi we will consider.)

Definition 1.8 (Barbed congruence). Barbed bisimilarity is the largest symmetric relation ≃ • on -calculus processes such that ≃ • implies: 1. If =⇒ ′ then there is ′ such that =⇒ ′ and ′ ≃ • ′ . 2. ⇓ iff ⇓ .
Let L be a set of -calculus agents, and , ∈ L. We say that and are barbed congruent in L, written ≃ L , if for each

(well-sorted) L-context , it holds that [ ] ≃ • [ ].
Remark 1.9. Barbed congruence has been uniformly defined on processes and abstractions (via a quantification on all process contexts). Usually, however, definitions will only be given for processes; it is then intended that they are extended to abstractions by requiring closure under ground parameters, i.e., by supplying fresh names as arguments.

As for all contextually-defined behavioural relations, so barbed congruence is hard to work with. In all calculi we consider, it can be characterised in terms of ground bisimilarity, under the (mild) condition that the processes are image-finite up to ≈. (We recall that the class of processes image-finite up to ≈ is the largest subset IF of -calculus processes which is derivation closed and such that ∈ IF implies that, for all actions , the set { ′ | = = ⇒ ′ } quotiented by ≈ is finite. The definition is extended to abstractions as by Remark 1.9.) All the agents in the paper, including those obtained by encodings of the -calculus, are image-finite up to ≈. The distinctive feature of ground bisimilarity is that it does not involve instantiation of the bound names of inputs (other than by means of fresh names), and similarly for abstractions. In the remainder, we omit the adjective 'ground'. Processes and are bisimilar, written ≈ , if R for some bisimulation R.

We will use two subcalculi: the Internal -calculus (I ), and the Asynchronous Local -calculus (AL ), obtained by placing certain constraints on prefixes.

I .

In I , all outputs are bound. This is syntactically enforced by replacing the output construct with the bound-output construct ( ). , which, with respect to the grammar of the ordinarycalculus, is an abbreviation for . . In all tuples (input, output, abstractions, applications) the components are pairwise distinct so to make sure that distinctions among names are preserved by reduction.

AL . AL is defined by enforcing that in an input ( ). , all names in appear only in output position in . Moreover, AL being asynchronous, output prefixes have no continuation; in the grammar of the -calculus this corresponds to having only outputs of the form . 0 (which we will simply write ). In AL , to maintain the characterisation of barbed congruence as (ground) bisimilarity, the transition system has to be modified [START_REF] Merro | On asynchrony in name-passing calculi[END_REF], allowing the dynamic introduction of additional processes (the 'links', sometimes also called forwarders).

Theorem 1.11.

1. In I , on agents that are image-finite up to ≈, barbed congruence and bisimilarity coincide. 2. In AL , on agents that are image-finite up to ≈ and where no free name is used in input, barbed congruence and bisimilarity coincide.

All encodings of the -calculus (into I and AL ) in the paper satisfy the conditions of Theorem 1.11. Thus we will be able to use bisimilarity as a proof technique for barbed congruence. (In part (2) of the theorem, the condition on inputs can be removed by adopting an asynchronous variant of bisimilarity; however, the synchronous version is easier to use in our proofs based on unique solution of equations).

Unique solutions in I and AL

We adapt the proof technique of unique solution of equations, from [START_REF] Durier | Divergence and Unique Solution of Equations[END_REF] to the calculi I and AL , in order to derive bisimilarity results. The technique is discussed in [START_REF] Durier | Divergence and Unique Solution of Equations[END_REF] on the asynchronous -calculus (for possibly-infinite systems of equations). The structure of the proofs for I and AL is similar; in particular the completeness part is essentially the same because bisimilarity is the same. The differences in the syntax of I , and in the transition system of AL , show up only in certain technical details of the soundness proofs.

We need variables to write equations. We use capital letters , , for these variables and call them equation variables. The body of an equation is a name-closed abstraction possibly containing equation variables (that is, applications can also be of the form ). We use to range over such expressions; and E to range over systems of equations, defined as follows. In the definitions below, the indexing set can be infinite. Definition 2.1. Assume that, for each of a countable indexing set , we have a variable , and an expression , possibly containing some variables. Then { = } ∈ (sometimes written = ) is a system of equations. (There is one equation for each variable ; we sometimes use to refer to that equation.)

A system of equations is guarded if each occurrence of a variable in the body of an equation is underneath a prefix.

[ ] is the abstraction resulting from by replacing each variable with the abstraction (as usual assuming and have the same sort). Definition 2.2. Suppose { = } ∈ is a system of equations. We say that:

• is a solution of the system of equations for ≈ if for each it holds that ≈ [ ].

• The system has a unique solution for ≈ if whenever and are both solutions for ≈, we have ≈ .

Definition 2.3 (Syntactic solutions). The syntactic solutions of the system of equations = are the recursively defined constants K , △ = [ K ], for each ∈ , where is the indexing set of the system.

The syntactic solutions of a system of equations are indeed solutions of it.

A process diverges if it can perform an infinite sequence of internal moves, possibly after some visible ones (i.e., actions different from ); formally, there are processes , ≥ 0, and some ,

such that = 0 0 --→ 1 1 --→ 2 2
--→ . . . and for all > , = .

We call a divergence of the sequence of transitions --→ +1 . In the case of an abstraction, has a divergence if the process has a divergence, where are fresh names. A tuple of agents is divergence-free if none of the components has a divergence.

The following result is the technique we rely on to establish completeness of the encoding. As announced above, it holds in both I and AL . Theorem 2.4. In I and AL , a guarded system of equations with divergence-free syntactic solutions has unique solution for ≈.

Techniques for ensuring termination, hence divergence freedom, for the -calculus have been studied in, e.g., [START_REF] Demangeon | Termination in Impure Concurrent Languages[END_REF][START_REF] Sangiorgi | Termination of processes[END_REF][START_REF] Yoshida | Strong normalisation in the pi -calculus[END_REF].

Further Developments

We present some further developments to the theory of unique solution of equations, that are needed for the results in this paper. The first result allows us to derive the unique-solution property for a system of equations from the analogous property of an extended system. Definition 2.5. A system of equations E ′ extends system E if there exists a fixed set of indices such that any solution of E can be obtained from a solution of E ′ by removing the components corresponding to indices in . Theorem 2.6. Consider two systems of equations E ′ and E where E ′ extends E. If E ′ has a unique solution, then the property also holds for E.

We shall use Theorem 2.6 in Section 4.2, in a situation where we transform a certain system into another one, whose uniqueness of solutions is easier to establish. Remark 2.7. We cannot derive Theorem 2.6 by comparing the syntactic solutions of the two systems E ′ and E. For instance, the equations = . and = . . . . . have (strongly) bisimilar syntactic solutions, yet only the latter equation has the unique-solution property. (Further, Theorem 2.6 allows us to compare systems of different size.)

The second development is a generalisation of Theorem 2.4 to preorders; we postpone its presentation to Section 6.

Milner's encodings 3.1 Background

Milner noticed [START_REF] Milner | Functions as processes[END_REF][START_REF] Milner | Functions as Processes[END_REF] that his call-by-value encoding can be easily tuned so to mimic forms of evaluation in which, in an application , the function is run first, or the argument is run first, or function and argument are run in parallel (the proofs are actually carried out for this last option). We chose here the first one, because it is more in line with ordinary call-by-value. A discussion on the 'parallel' call-by-value is deferred to Section 7.

The core of any encoding of the -calculus into a process calculus is the translation of function application. This becomes a particular form of parallel combination of two processes, the function and its argument; v -reduction is then modeled as process interaction.

The encoding of a -term is parametric over a name; this may be thought of as the location of that term, or as its continuation. A term that becomes a value signals so at its continuation name and, in doing so, it grants access to the body of the value. Such body is replicated, so that the value may be copied several times. When the value is a function, its body can receive two names: (the access to) its value-argument, and the following continuation. In the translation of application, first the function is run, then the argument; finally the function is informed of its argument and continuation.

In the original paper [START_REF] Milner | Functions as processes[END_REF], Milner presented two candidates for the encoding of call-by-value -calculus [START_REF] Plotkin | Call-by-Name, Call-by-Value and the lambda-Calculus[END_REF]. They follow the same idea of translation, but with a technical difference in the rule for variables. One encoding, V, is so defined:

V [[ . ]] def = ( ) ( ). ! ( , ). V [[ ]] V [[ ]] def = ( ) ( )(V [[ ]] | ( ). (V [[ ]] | ( ). , )) V [[ ]] def = ( )
In the other encoding, V ′ , application and -abstraction are treated as in V; the rule for variables is:

V ′ [[ ]] def = ( ) ( ). ! ( , ). , .
The encoding V is more efficient than V ′ , as it uses fewer communications.

Some problems with the encoding

The immediate free output in the encoding of variables in V breaks the validity of v -reduction; i.e., there exist a term and a value

such that V [[( . ) ]] ≈ V [[ { / }]] [23]
. The encoding V ′ fixes this by communicating, instead of a free name, a fresh pointer to that name. Technically, the initial free output of is replaced by a bound output coupled with a link to (the process ! ( , ).

, , receiving at and re-emitting at ). Thus v -reduction is validated [START_REF] Sangiorgi | Expressing mobility in process algebras : first-order and higher-order paradigms[END_REF]. (The final version of Milner's paper [START_REF] Milner | Functions as Processes[END_REF], was written after the results in [START_REF] Sangiorgi | Expressing mobility in process algebras : first-order and higher-order paradigms[END_REF] were known and presents only the encoding V ′ .)

Nevertheless, V ′ only delays the free output, as the added link contains itself a free output. As a consequence, we can show that other desirable equalities of call-by-value are broken. An example is law (1) from the Introduction, as stated by Proposition 3.1 below. This law is desirable (and indeed valid for contextual equivalence, We recall that ≃ is barbed congruence in the -calculus. Proposition 3.1. For any value , we have:

I [[ . ]] def = ( ) ( ). ! ( , ). I [[ ]] I[[ ]] def = ( ) ( ). ⊲ I[[ ]] def = ( ) I [[ ]] | ( ). I [[ ]] | ( ). ( ′ , ′ ). ( ′ ⊲ | ′ ⊲ )
V ′ [[ ( )]] V ′ [[ ]] and V [[ ( )]] V [[ ]] .
(The law is violated also under coarser equivalences, such as contextual equivalence.) Technically, the reason why the law fails in can be illustrated when = , for encoding V. We have:

V [[ ]] ≃ ( ). ( , | ! ( ). ) V [[ ( )]] ≃ ( ). ( , )( , | ! ( ). | ( ). ( ′ ). ! ′ ( ′ ). ′ )
In presence of the normal form , the identity becomes observable. Indeed, in the second term, a fresh name, , is sent instead of continuation , and a link between and is installed. This corresponds to a law which is valid in AL , but not in . This problem can be avoided by iterating the transformation that takes us from V to V ′ (i.e., the replacement of a free output with a bound output so to avoid all emissions of free names). Thus the target language becomes Internal ; the resulting encoding is analysed in Section 4.

Another solution is to control the use of name capabilities in processes. In this case the target language becomes AL , and we need not modify the initial encoding V. This situation is analysed in Section 5.

Moreover, in both solutions, the use of link processes validates the following law -a form of -expansion -(the law fails for Milner's encoding into the -calculus):

. =

In the call-by-value -calculus this is a useful law (that holds because substitutions replace variables with values).

4 Encoding in the Internal -calculus 4.1 Encoding and soundness Figure 1 presents the encoding into I , derived from Milner's encoding by removing the free outputs as explained in Section 3. Process ⊲ represents a link (sometimes called forwarder; for readability we have adopted the infix notation ⊲ for the constant ⊲). It transforms all outputs at into outputs at (therefore , are names of the same sort). Thus the body of ⊲ is replicated, unless and are continuation names (names such as , , over which the encoding of a term is abstracted). The definition of the constant ⊲ therefore is:

⊲ △ =              ( , ) ( ). ( ). ⊲ if , are continuation names ( , ) ! ( , ). ( , ). ( ⊲ | ⊲ ) otherwise
(The distinction between continuation names and the other sorts of names is not necessary, but simplifies the proofs.)

The encoding validates v -reduction. The structure of the proof of soundness of the encoding is similar to that for the analogous property for Milner's call-by-name encoding with respect to Levy-Longo Trees [START_REF] Sangiorgi | Lazy functions and mobile processes[END_REF]. The details are however different, as in call-by-value both the encoding and the trees (the Eager Trees extended to handle -expansion) are more complex.

We first need to establish an operational correspondence for the encoding. For this we make use of an optimised encoding, obtained from the one in Figure 1 by performing a few (deterministic) reductions, at the price of a more complex definition. Precisely, in the encoding of application, we remove some of the initial communications, including those with which a term signals that it has become a value. Correctness of the optimisations is established by algebraic reasoning.

Using the operational correspondence, we then show that the observables for bisimilarity in the encoding -terms imply the observables for -eager normal-form bisimilarity in the encodedterms. The delicate cases are those in which a branch in the tree of the terms is produced -case (2) of Definition 1.3 -and where anexpansion occurs -thus a variable is equivalent to an abstraction, cases ( 5) and ( 6) of Definition 1.6.

For the branching, we exploit a decomposition property onterms, roughly allowing us to derive from the bisimilarity of two parallel compositions the componentwise bisimilarity of the single components. For the -expansion, if

I [[ ]] ≈ I [[ . ]],
where

⇓ e [ ],
we use a coinductive argument to derive and e [ ] , for fresh; from this we then obtain . .

Lemma 4.2 (Soundness). For any , ∈ Λ, if I [[ ]] ≈ I[[ ]]

then .

Completeness and Full Abstraction

To ease the reader into the proof, we first show the completeness for , rather than .

The system of equations. Suppose R is an eager normal-form bisimulation. We define a (possibly infinite) system of equations E R , solutions of which will be obtained from the encodings of the pairs in R. We then use Theorem 2.4 and Theorem 2.6 to show that E R has a unique solution.

We assume an ordering on names and variables, so to be able to view (finite) sets of these as tuples. Moreover, if is an abstraction, say ( ) , then ( ) is an abbreviation for its uncurrying ( , ) .

There is one equation , = , for each pair ( , ) ∈ R.

The body

, is essentially the encoding of the eager normal form of and , with the variables of the equations representing the coinductive hypothesis. To formalise this, we extend the Proof. Consider an eager normal-form bisimulation R, and the corresponding systems of equations E R and E ′ R . Lemmas 4.5 and 4.4 allow us to apply Theorem 2.6 and deduce that E R has a unique solution. By Lemma 4.3,

I c [[R 1 ]] and I c [[R 2 ]] are solutions of E R . Thus, from R , we deduce ( ) I [[ ]] ≈ ( ) I [[ ]]
, where = fv( , ). Hence also

I[[ ]] ≈ I [[ ]].

Completeness for

. The proof for is extended to , maintaining its structure. We highlight the main differences.

We enrich E R with the equations corresponding to the two additional clauses of (Definition 1.6). When ⇓ and ⇓ . ′ , where ′

, we proceed as in case 4 of the definition of E R , given that . (( . e [ ])( )); the equation is:

, = ( ) I [[ . ( . , e [ ] ) ( , ) ]] .
We proceed likewise for the symmetric case.

In the optimised equations that we use to derive unique solutions, we add the following equation (relating values), as well as its symmetric counterpart:

V , . ′ = ( 0 , ) ! 0 ( , ). ( ′ , ′ ). ( V , ′ , ′ | ′ ( ). , e [ ] ′′ , ) .
Finally, to prove that

I c [[R 1 ]] and I c [[R 2 ]
] are solutions of E R , we show that, whenever ⇓ and ⇓ . ′ , with ′ ⇓ e [ ]:

I [[ ]] ≈ , [I c [[R 1 ]]] = I [[ . (( . )( ))]]
and

I [[ ]] ≈ , [I c [[R 2 ]]] = I [[ . (( . e [ ])( ))]] .
To establish the former, we use algebraic reasoning to infer

I [[ ]] ≈ I [[ . ]].
For the latter, we use law (2) (given in the proof of Lemma 4.3). Remark 4.9 (Unique solutions versus up-to techniques). For Milner's encoding of call-by-name -calculus, the completeness part of the full abstraction result with respect to Lévy-Longo Trees [START_REF] Sangiorgi | Lazy functions and mobile processes[END_REF] relies on up-to techniques for bisimilarity. Precisely, given a relation R on -terms that represents a tree bisimulation, one shows that the -calculus encoding of R is a -calculus bisimulation up-to context and expansion. Expansion is a preorder that intuitively guarantees that a term is 'more efficient' than another one. In the up-to technique, expansion is used to manipulate the derivatives of two transitions so to bring up a common context. Such up-to technique is not powerful enough for the call-by-value encoding and the Eager Trees because some of the required transformations would violate expansion (i.e., they would require to replace a term by a 'less efficient' one). An example of this is law (2) (in the proof of Lemma 4.3), that would have to be applied from right to left so to implement the branching in clause (2) of Definition 1.3 (as a context with two holes).

The use of the technique of unique solution of equations allows us to overcome the problem: law (2) and similar laws that introduce 'inefficiencies' can be used (and they are indeed used, in various places), as long as they do not produce new divergences.

Encoding into AL

Full abstraction with respect to -Eager-Tree equality also holds for Milner's simplest encoding, namely V (Section 3), provided that the target language of the encoding is taken to be AL . The adoption of AL implicitly allows us to control capabilities, avoiding violations of laws such as (1) in the Introduction. In AL , bound output prefixes such as ( ). ( ) are abbreviations for ( | ( )).

Theorem 5.1. iff V [[ ]] ≃ AL V [[ ]],
for any , ∈ Λ.

The main difference with respect to the proofs of Lemmas 4.6 and 4.7 is when proving absence of divergences for the (optimised) system of equations. Indeed, in AL the characterisation of barbed congruence (≃ AL ) as bisimilarity makes use of a different labelled transition system where visible transitions may create new processes (the 'static links'), that could thus produce new reductions. Thus one has to show that the added processes do not introduce new divergences.

Contextual equivalence and preorders

We have presented full abstraction for -Eager-Tree equality taking a 'branching' behavioural equivalence, namely barbed congruence, on the -processes. We show here the same result for contextual equivalence, the most common 'linear' behavioural equivalence. We also extend the results to preorders.

We only discuss the encoding I into I . Similar results however hold for the encoding V into AL .

Contextual relations and traces

Contextual equivalence is defined in the -calculus analogously to its definition in the -calculus (Definition 1.2); thus, with respect to barbed congruence, the bisimulation game on reduction is dropped. Since we wish to handle preorders, we also introduce the contextual preorder. To manage contextual preorder and equivalence in proofs, we exploit characterisations of them as trace inclusion and equivalence. For = 1 , . . . , , where each is a visible action, we set ct coincides with ≈ tr .

= ⇒ if 1 ==⇒ 1 2 ==⇒ 2 . . . -1 = == ⇒ , for

A proof technique for preorders

We modify the technique of unique solution of equations to reason about preorders, precisely the trace inclusion preorder.

In the case of equivalence, the technique of unique solutions exploits symmetry arguments, but symmetry does not hold for preorders. We overcome the problem by referring to the syntactic solution of the system in an asymmetric manner. This yields the two lemmas below, intuitively stating that the syntactic solution of a system is its smallest pre-fixed point, as well as, under the divergence-freeness hypothesis, its greatest post-fixed point. We say that is a pre-fixed point for tr of a system of equations

{ = } if [ ] tr ; similarly, is a post-fixed point for tr if tr [ ].
Lemma 6.4 (Pre-fixed points, tr ). Let E be a system of equations, and K E its syntactic solution. If is a pre-fixed point for tr of E, then K E tr Lemma 6.5 (Post-fixed points, tr ). Let E be a guarded system of equations, and K E its syntactic solution. Suppose K E has no divergences. If is a post-fixed point for tr of E, then tr K E .

Lemma 6.4 is immediate; the proof of Lemma 6.5 is similar to the proof of Theorem 2.4 (for bisimilarity). We thus derive the following proof technique. Theorem 6.6. Suppose that E is a guarded system of equations with a divergence-free syntactic solution. If is a pre-fixed point for tr of E, and a post-fixed point, then tr .

We can also extend Theorem 2.6 to preorders. We say that a system of equations E ′ extends E with respect to a given preorder if there exists a fixed set of indices such that:

1. any pre-fixed point of E for the preorder can be obtained from a pre-fixed point of E ′ (for the same preorder) by removing the components corresponding to indices in ; 2. the same as (1) with post-fixed points in place of pre-fixed points.

Theorem 6.7. Consider two systems of equations E ′ and E where E ′ extends E with respect to tr . Furthermore, suppose E ′ is guarded and has a divergence-free syntactic solution. If is a pre-fixed point for tr of E, and a post-fixed point, then tr .

Full abstraction results

The preorder on -terms induced by the contextual preorder iseager normal-form similarity, ≤ . It is obtained by imposing that ≤ for all , whenever is divergent. Thus, with respect to the bisimilarity relation , we only have to change clause (1) of Definition 1.3, by requiring only to be divergent. (The bisimilarity is then the intersection of ≤ and its converse ≥ .) Theorem 6.8 (Full abstraction on preorders). For any , ∈ Λ, we have ≤

iff I [[ ]] I ct I[[ ]]
. The structure of the proofs is similar to that for bisimilarity, using however Theorem 6.6. We discuss the main aspects of the completeness part.

Given an -eager normal-form simulation R, we define a system of equations E R as in Section 4.2. The only notable difference in the definition of the equations is in the case where R , diverges and has an eager normal form. In this case, we use the following equation instead:

, = ( ) I [[Ω]] .
(3) As in Section 4.2, we define a system of guarded equations E ′ R whose syntactic solutions do not diverge. Equation ( 3) is replaced with , = ( , ) 0. Exploiting Theorem 6.7, we can use unique solution for preorders (Theorem 6.6) with E R instead of

E ′ R . Defining I c [[R 1 ]] and I c [[R 2 ]] as previously, we need to prove that I c [[R 1 ]] tr R [I c [[R 1 ]]] and R [I c [[R 2 ]]] tr I c [[R 2 ]].
The former result is established along the lines of the analogous result in Section 4.2: indeed,

I c [[R 1 ]
] is a solution of E R for ≈, and ≈ tr is coarser than ≈.

For the latter, the only difference is due to equation (3), when R , and diverges but not . In that case, we have to prove that I 7 Conclusions and future work

In the paper we have studied the main question raised in Milner's landmark paper on functions as -calculus processes, which is about the equivalence induced on -terms by their process encoding. We have focused on call-by-value, where the problem was still open; as behavioural equivalence on -calculus we have taken contextual equivalence and barbed congruence (the most common 'linear' and 'branching' equivalences).

First we have shown that some expected equalities for open terms fail under Milner's encoding. We have considered two ways for overcoming this issue: rectifying the encodings (precisely, avoiding free outputs); restricting the target language to AL , so to control the capabilities of exported names. We have proved that, in both cases, the equivalence induced is Eager-Tree equality, modulo (i.e., Lassen's -eager normal-form bisimulation). We have then introduced a preorder on these trees, and derived similar full abstraction results for them with respect to the contextual preorder on -terms. The paper is also a test case for the technique of unique solution of equations (and inequations), which is essential in all our completeness proofs.

Lassen had introduced Eager Trees as the call-by-value analogous of Lévy-Longo and Böhm Trees. The results in the paper confirm the claim, on process encodings of -terms: it was known that for (weak and strong) call-by-name, the equalities induced are those of Lévy-Longo Trees and Böhm Trees [START_REF] Sangiorgi | Trees from Functions as Processes[END_REF].

For controlling capabilities, we have used AL . Another possibility would have been to use a type system. In this case however, the technique of unique solution of equations needs to be extended to typed calculi. We leave this for future work.

We also leave for future work a thorough comparison between the technique of unique solution of equations and techniques based on enhancements of the bisimulation proof method (the "up-to" proof techniques), including if and how our completeness results can be derived using the latter techniques. (We recall that the "upto" proof techniques are used in the completeness proofs with respect to Lévy-Longo Trees and Böhm Trees for the call-by-name encodings. We have discussed the problems with call-by-value in Remark 4.9.) In any case, even if other solutions existed, for this specific problem the unique solution technique appears to provide an elegant and natural framework to carry out the proofs.

For our encodings we have used the polyadic -calculus; Milner's original paper [START_REF] Milner | Functions as processes[END_REF] used the monadic calculus (the polyadic -calculus makes the encoding easier to read; it had not been introduced at the time of [START_REF] Milner | Functions as processes[END_REF]). We believe that polyadicity does not affect the results in the paper (the possibility of autoconcurrency breaks full abstraction of the encoding of the polyadic -calculus into the monadic one, but autoconcurrency does not appear in the encoding of -terms).

In the call-by-value strategy we have followed, the function is reduced before the argument in an application. Our results can be adapted to the case in which the argument runs first, changing the definition of evaluation contexts. The parallel call-by-value, in which function and argument can run in parallel (considered in [START_REF] Milner | Functions as Processes[END_REF]), appears more delicate, as we cannot rely on the usual notion of evaluation context.

Interpretations of -calculi into -calculi appear related to game semantics [START_REF] Berger | Sequentiality and the pi-Calculus[END_REF][START_REF] Honda | Game-Theoretic Analysis of Call-by-Value Computation[END_REF][START_REF] Hyland | Pi-Calculus, Dialogue Games and PCF[END_REF]. In particular, for untyped call-by-name they both allow us to derive Böhm Trees and Lévy-Longo Trees [START_REF] Ker | Adapting innocent game models for the Böhm treelambda-theory[END_REF][START_REF] Ong | Games characterizing Levy-Longo trees[END_REF]. To our knowledge, game semantics exist based on typed call-byvalue, e.g., [START_REF] Abramsky | Call-by-Value Games[END_REF][START_REF] Honda | Game-Theoretic Analysis of Call-by-Value Computation[END_REF], but not in the untyped case. In this respect, it would be interesting to see whether the relationship betweencalculus and Eager Trees studied in this paper could help to establish similar relationships in game semantics.

Remark 1 . 7 .

 17 Definition 1.6 coinductively allows -expansions to occur underneath other -expansions, hence trees with infinite -expansions may be equated with finite trees. For instance, . . ( . ) . ( . ( . )) . . . A concrete example is given by taking a fixpoint , and setting def = ( . ( )). We then have =⇒ . ( ), and then ( ) =⇒ ( . (

Definition 1 .

 1 10 (Bisimilarity). A symmetric relation R on -processes is a bisimulation, if whenever R and -→ ′ , then ˆ = = ⇒ ′ for some ′ with ′ R ′ .

Figure 1 .

 1 Figure 1. The encoding into I

Lemma 4 . 1 (

 41 Validity of v -reduction). For any , in Λ, -→ implies I [[ ]] ≈ I [[ ]].

Lemma 4 . 7 (

 47 Completeness for ). For any , in Λ, implies I [[ ]] ≈ I [[ ]]. Combining Lemmas 4.2 and 4.7, and Theorem 1.11 we derive Full Abstraction for with respect to barbed congruence. Theorem 4.8 (Full Abstraction for ). For any , in Λ, we have iff I [[ ]] ≃ I I[[ ]]

Definition 6 . 1 .

 61 Two I agents , are in the contextual preorder, written I ct , if [ ] ⇓ implies [ ] ⇓ , for all contexts . They are contextually equivalent, written ≃ I ct ,

  [[Ω]] tr I[[ ]], which follows easily because the only trace of I [[Ω]] is the empty one, hence I[[Ω]] tr for any . Corollary 6.9 (Full abstraction for ≃ I ct ). For any , in Λ, iff I[[ ]] ≃ I ct I[[ ]].

  ) ] -→ e [ { / }] .We write =⇒ for the reflexive transitive closure of -→. A term in eager normal form is a term that has no eager reduction.

	Proposition 1.1. and -→ ′ , for any value substitution . 1. If -→ ′ , then e [ ] -→ e [ ′ ]
	2. Terms in eager normal form are either values or of the shape
		• • • .		. as 1 • • • . , or
	. if the length of is not important. Symbol Ω stands for the
	always-divergent term ( . )( . ).
	A context is a term with a hole [•], possibly occurring more than
	once. If is a context, [ ] is a shorthand for where the hole
	[•] is substituted by . An evaluation context is a special kind of
	context, with exactly one hole [•], and in which the inserted term
	can immediately run. In the pure -calculus values are abstractions
	and variables.
	Evaluation contexts	e := [•] | e |	e
	Values	:=	|	.
	In call-by-value, substitutions replace variables with values; we
	call them value substitutions.
	Eager reduction (or v -reduction), -→ ⊆ Λ × Λ, is determined
	by the rule:

e [( . e [ ].

  some processes 1 , . . . , .

	Definition 6.2. Two I processes , are in the trace inclusion,
	written	tr , if = ⇒ implies = ⇒, for each trace . They are
	trace equivalent, written ≈ tr , if both	tr	and	tr hold.
	As usual, these relations are extended to abstractions by requir-
	ing instantiation of the parameters with fresh names.
	Theorem 6.3. In I , relation I

ct coincides with tr , and relation ≃ I

Acknowledgments

This work has been supported by the European Research Council (ERC) under the Horizon 2020 programme (CoVeCe, grant agreement No 678157); the ANR under the programmes "Investissements d'Avenir" (ANR-11-IDEX-0007), LABEX MILYON (ANR-10-LABX-0070), and Elica (ANR-14-CE25-0005); and the Université Franco-Italienne under the programme Vinci.

encoding of the -calculus to equation variables by setting

where = fv( , ) .

We now describe the equation , = , , for ( , ) ∈ R. The equation is parametrised on the free variables of and (to ensure that the body , is a name-closed abstraction) and an additional continuation name (as all encodings of terms). Below = fv( , ).

1. If ⇓ and ⇓ , then the equation is the encoding of :

If ⇑ and ⇑, then the equation uses a purely-divergent term; we choose the encoding of Ω:

3. If ⇓ . ′ and ⇓ . ′ , then the equation encodes an abstraction whose body refers to the normal forms of ′ , ′ , via the variable ′ , ′ :

, we separate the evaluation contexts and the values, as in Definition 1.3. In the body of the equation, this is achieved by: ( ) rewriting e [ ] into ( . e [ ])( ), for some fresh , and similarly for ′ e and ′ (such a transformation is valid for ); and ( ) referring to the variable for the evaluation contexts, e [ ], ′

e [ ] , and to the variable for the values, , ′ . This yields the equation (for fresh):

As an example, suppose ( , . ) ∈ R, where = . and = ( . ) ′ . The free variables of are and ′ . We obtain the following equations:

Solutions of E R . Having set the system of equations for R, we now define solutions for it from the encoding of the pairs in R.

We can view the relation R as an ordered sequence of pairs (e.g., assuming some lexicographical ordering). Then R indicates the tuple obtained by projecting the pairs in R onto the -th component ( = 1, 2). Moreover ( , ) is the -th pair in R, and is fv( , ).

We write

] for the closed abstractions resulting from the encoding of R 1 , i.e., the tuple whose -th component is

and similarly for

Proof. We show that each component of

] is solution of the corresponding equation, i.e., for the -th component we show

We reason by cases over the shape of the eager normal form of , . The most interesting case is when

in which case we use the following equality (for fresh), which is proved using algebraic reasoning:

We also exploit the validity of v for ≈ (Lemma 4.1).

Unique solution for E R . We use Theorem 2.6 to prove uniqueness of solutions for E R . The only delicate requirement is the one on divergence for the syntactic solution. We introduce for this an auxiliary system of equations, E ′ R , that extends E R , and whose syntactic solutions have no -transition and hence trivially satisfy the requirement. Like the original system E R , so the new one E ′ R is defined by inspection of the pairs in R; in E ′ R , however, a pair of R may sometimes yield more than one equation. Thus, let ( , ) ∈ R with = fv( , ).

1. When ⇑ and ⇑, the equation is , = ( , ) 0 .

When

⇓ and ⇓ ′ , we introduce a new equation variable V

, ′ and a new equation; this will allow us, in the following step (3), to perform some optimisations. The equation is

, ′ , ′ , and we have, accordingly, the two following additional equations corresponding to the cases where values are functions or variables: Proof. The new system E ′ R is obtained from E R by modifying the equations and adding new ones. Ones shows that the solutions to the common equations are the same, using algebraic reasoning. Proof. Divergence-freedom for the syntactic solutions of E ′ R holds because in the equations each name (bound or free) can appear either only in inputs or only in outputs. As a consequence, since the labelled transition system is ground (names are only replaced by fresh ones), no -transition can ever be performed, after any number of visible actions. Further, E ′ R is guarded. Hence we can apply Theorem 2.4.


Angèle Laurent

Claudio Satriano

Pascal Bernard

Pascal Bernard Accurate

Accurate depth determination of VLF events of the ongoing seismo-volcanic crisis in Mayotte

Accurate depth determination of VLF events

of the ongoing seismo-volcanic crisis in Mayotte.

Angèle Laurent, Claudio Satriano, Pascal Bernard

Methodology :

Back-projection location : Cross-correlation for each pair of stations (BB & OBH) of the filtered (10-20s) VLF signal and 1-bit normalised. Mapping of station-pair cross-correlations in 3D space using a constant velocity. Stacking of the cross-correlation maps to find the maximum likelihood source location. Event depth (Z) depends on chosen velocity: Z>20 km @ 2.5 km/s; Z<5 km @ 4.5 km/s. Correction of the OBH pressure data into acceleration as on-land broadband stations, as proposed by An et al., [2017]. Cross-correlation between OBH and broadband on-land stations, all corrected in acceleration, shows a pattern linked to the source effect.

Perfect correlation all along the duration of the event b e t we e n a l l s t a t i o n s : t h e s o u r c e m e c h a n i s m i s axisymmetric.

In agreement with this observation, VLF source mechanism is limited between two end-members models : pure explosive source or 100% CLVD, a type of mechanism that can explain transient volcano signals [Chouet, Kumagai].

For the moment, we perform synthetics with one of the 2 end-members : pure isotropic source [see Section 3].

Direct modelling :

Aim : Explore depth and focal mechanism with parametrised synthetics.

Set up:

Axitra [Cotton and Coutant, 1997] allows us to configure the source with an impulsive 100% explosive and isotropic mechanism without displacement (dirac function). Velocities are inspired from the local velocity model made with VELEST by A. Lavayssière [AGU, 2020].

Synthetics are made for several depths : 5, 10, 20, 30, 40 and 50 km.

The Green function is thus convolved with a parametrised source time function built like an sinusoïdal exponential decaying function, with a period of 15.57s, a duration of 1700s, inspired from the 2018-11-11 biggest VLF of the crisis. 36 velocity models were tested by fixing Vp to 5.5, 6, 6.5, 7, 7.5, 8 km/s and Vp/Vs to as, 1.4, 1.5, 1.6, 1.7, 1.8, 1.9.

Synthetic dataset attributes :

All synthetics undergo the same processing than the real data with crosscorrelation to correct from the wave propagation delay, which is retrieved and drawn in function of the epicentral distance and amplitude ratio. Alternatively, for events of this size, the hypothesis of fluid resonance within the whole magmatic layer can be considered.

:

Confirmation of the VLFs location in depth with direct modelling with local and teleseismic stations. Refine amplitude ratio analysis.

parameter space to better understand particle motion.

☞ Better understand of the source phenomenon through numerical modelling of the VLF waveform as a dumped oscillator embedded in a medium (rock and fluids).

Integral amplitude ratio :

Integral of the absolute signal between all station of the network and the reference station (MONO/002).

Cross-correlation delay versus epicentral distance :

Delay retrieve by the cross-correlation of the waveform at each station with the reference station (MONO/002).

Synthetic particle motion :

In addition to the time delay and amplitude ratio attributes, we compute particle motion. Polarization attributes of the particle motion (aspect ratio, tilt of the elliptic shape) depend on the source depth and on the velocity model. Preliminary results show the effect of mixed waves (P & SV) on the polarization. Synthetic particle motion show good agreement for the closest station (PMZI), but the difference between observed and modelled data increases with distance.

Particle motion is a promising alternative method but a thorough exploration of all depth and velocity model is necessary.

Synthetic results :

For more information, check my previous poster for AGU Fall Meeting 2020 fmax = 0.065 Hz, Tmax = 15.57 s

  Institut de Physique du globe de Paris, Université Paris Diderot-PRES Paris Université -Paris, France (alaurent@ipgp.fr) Frequency signal [VLF] of long duration (> 2500s), monochromatic period of ~15s and vertical elliptic polarization. Source mechanism hypothesis : Talandier et al. [2016] (for similar signals at Le Rocard submarine volcano, French Polynesia) : a resonance in an open superficial and pressurized pipe induced by fluid migration. Lemoine et al., [2019] : an action of oscillating fluids into a magmatic reservoir. Cesca et al. [2020] : excitation and resonance of fluid-filled crack in depth by a piston-like action caused by pressure variation into the magma chamber. They propose that VLFs are resulting of interaction between two fluids-filled cracks at a depth of 37 +/-11 km.

  Cai, C., Zheng, Y., Meng, L., & Liu, P. (2017). Theoretical applications of ocean bottom pressure induced by seismic seafloor motion. Geophysical Research Letters, 44, 10,272-Berthod, C., et al. (2021) The 2018-ongoing Mayotte submarine eruption: magma migration imaged by petrological monitoring. Earth and Planetary Science Letters. Cesca, S., Letort, J., Razafindrakoto, H. N. T., Heimann, S., Rivalta , E., Isken, M. P.,Nikkhoo, M., Passarelli, L., Petersen, M., Cotton, F., & Dahm, T. (2020). Drainage of a deep magma reservoir near Mayotte inferred from and deformation. Nature Geosciences. Chouet B. (1985) Excitation of a buried magmatic pipe : a seismic source model for volcanic tremor. JGR, VOL 90(B2):1881-1893. Dofal, A., (2021). Structure de la lithosphère de l'océan Indien occidental révélée par la méthode des fonctions récepteur. Feuillet, N., et al. Birth of a large volcanic edifice offshore Mayotte through lithosphere-scale rifting. Kumagai H., Miyakawa K., Inoue H. N., Obara K . , S u e t s u g u D . ( 2 0 0 3 ) , M a g m a t i c D i k e Resonances Inferred from Very-Long-Period Seismic Signals. SCIENCE, 299, Lavayssière, A., Crawford, W., Saurel, J-M., Satriano, C., Komorowski, J-C., & REVOSIMA consortium. New 1D velocity model and absolute locations image Mayotte seismo-volcanic region. AGU Fall Meting 2020. Lemoine, A., Bertil, D., Roullé, A., & Briole, P. (2020). The volcano-tectonic crisis of 2018 east of Mayotte, Comoros islands. Poiata, N., C. Satriano, J.-P. Vilotte, P. Bernard, & K. Obara. (2016). Multiband array detection and location of seismic sources recorded by dense seismic networks, Geophys J Int, 205(3), 1548-1573. Talandier, J., Hyvernaud, O., & Maury, R. C. (May 2016).Unusual seismic activity in 2011 and 2013 at the submarine volcano rocard, society hot spot (french polynesia). Geophysical Research Letters, 43(9) : 4247-4254.

  convolved fct .010..Z Station 010 synthetics for an isotropic source, at 20 km depth velocity model of : Vp = 6 km/s and Vs = 4 km/probably located above the main seismic swarm, in layer. The depth location of 20 km (blue star) fits with the hypothesis of a shallow magmatic layer found by petrochemical analysis performed by C. Berthod et al. [2021]. In addition, other seismic analyses point towards possible magma underplating: A. Dofal [2021] founds clues from receiver functions for a 9 km thick magmatic layer around 20 km of depth; long-period seismicity located around 25 km of depth [Retailleau et al., AGU 2020] further suggests the presence of fluids in this transition zone. Our source can be linked to the resonance of magmatic fluid filled cracks, as proposed by Cesca et al. [2020].

  -correlation delay in function of the epicentral distance. Grey part indicates the data selection : positive cross-correlation coefficient and positive delay. 2. Amplitude integrals ratio in function of the epicentral distance. What is the best velocity model and depth ? Time delay and amplitude ratio point toward a mean Vp, Vs of 7 km/s and 5 km/s respectively (Vp/Vs = 1.4) and a shallow depth (Z < 20 km). Where are they located ? They are ~15 km east of Petite Terre and (probably) at ~20 km of depth. What do VLFs tell us on the magmatic system in Mayotte? VLFs source depth and mechanism allow to constraint the properties of magmatic fluids in Mayotte and retrieve information about the structure and mechanics of the magmatic system.

☞

  Compare VLF with other type of seismicity recorded during the Mayotte crisis as LP (1-5 Hz) [Retailleau et al., AGU 2020] and VT [Mercury et al. AGU 2020]. Synthetic particle motion : Particle motion compute for all synthetics station, set by increasing (right to left) epicentral distance. Two examples shown for a two different velocity models set up and different depths (shallow and deep).

  . In addition, 1250 LP (long period) events and 700 very long period events have been recorded. The seismicity is organised into two main swarms: the first is located approximately 50 km east of the Petite Terre seismic crisis, the second is only approximately 20 km from the coast [Lemoine et al, 2019]. During the MAYOBS1 marine campaign (1-19 May 2019 aboard of the "Marion Dufresne"), a new submarine v o l c a n o w a s d i s c o v e r e d , a b o u t 5 0 k m E a s t o f M a y o t t e i s l a n d [ h t t p s : / / d o i . o r g / 10.18142/291]. Also, GNSS stations recorded a global movement of the island of a dozen of centimeters eastand-downward. These movements are interpreted as the deflation of a source at 30 km deep East of Mayotte, with a total volume of drained magma estimated at of around 2 km3 on November 2019