Davide Sangiorgi

Xian Xu

Trees from Functions as Processes

Trees are the best known tree structures on the λ-calculus. We give general conditions under which an encoding of the λ-calculus into the π-calculus is sound and complete with respect to such trees. We apply these conditions to various encodings of the call-by-name λ-calculus, showing how the two kinds of tree can be obtained by varying the behavioural equivalence adopted in the π-calculus and/or the encoding. The conditions are presented in the π-calculus but can be adapted to other concurrency formalisms.

Introduction

The π-calculus is a well-known model of computation with processes. Since its introduction, its comparison with the λ-calculus has received a lot of attention. Indeed, a deep comparison between a process calculus and the λ-calculus is interesting for several reasons: it is a significant test of expressiveness, and helps in getting deeper insight into its theory. From the λ-calculus perspective, it provides the means to study λ-terms in contexts other than purely sequential ones, and with the instruments available in the process calculus. A more practical motivations for describing functions as processes is to provide a semantic foundation for languages which combine concurrent and functional programming and to develop parallel implementations of functional languages.

Beginning with Milner's seminal work [START_REF] Milner | Functions as processes[END_REF], a number of encodings λ-calculus strategies have been encoded into the π-calculus, including call-by-name, strong call-by-name (and call-by-need variants), call-by-value, parallel call-by-value (see [START_REF] Sangiorgi | The π-calculus: a Theory of Mobile Processes[END_REF]Chapter 15]). In each case, several variant encodings have appeared, by varying the target language or details of the encoding itself. Usually, when an encoding is given, a few basic results about its correctness are established, such as operational correctness and validity of reduction (i.e., the property that the encoding of a λ-term and of a derivative of its are behaviourally undistinguishable). Only in a few cases the question of the equality on λ-terms induced by the encoding has been tackled, e.g., [3-5, 11, 12]. In this paper, we refer to this question as the full abstraction issue: for an encoding [[ ]] of the λ-calculus into π-calculus, an equality = λ on the λ-terms, and an equality = π on the π-terms, full abstraction is achieved when for all λ-terms M, N we have

M = λ N iff [[M ]] = π [[N ]]
. Full abstraction has two parts: soundness, which is the implication from right to left, and completeness, which is its converse.

The equality = λ usually is not the ordinary Morris-style contextual equivalence on the λ-terms: the π-calculus is richer -and hence more discriminating -than the λ-calculus; the latter is purely sequential, whereas the former can also express parallelism and non-determinism. (Exception to this are encodings into forms of π-calculus equipped with rigid constraints, e.g., typing constraints, which limit the set of legal π-calculus contexts.) Indeed, the interesting question is understanding what = λ is when = π is a well-know behavioural equivalence on π-terms. This question essentially amounts to using the encoding in order to build a λ-model, and then understanding the λ-model itself. While seldomly tackled, the outcomes of this study have been significant: for a few call-by-name encodings it has been shown that, taking (weak) bisimulation on the π-terms, then = λ corresponds to a well-known tree structure in the λ-calculus theory, namely the Lévy-Longo Trees (LTs) [START_REF] Sangiorgi | The π-calculus: a Theory of Mobile Processes[END_REF].

There is however another kind of tree structure in the λ-calculus, even more important: the Böhm Trees (BTs). BTs play a central role in the classical theory of the λ-calculus. The local structure of some of the most influential models of the λ-calculus, like Scott and Plotkin's P ω [START_REF] Scott | Data types as lattices[END_REF], Plotkin's T ω [START_REF] Plotkin | T ω as a universal domain[END_REF], is precisely the BT equality; and the local structure of Scott's D ∞ (historically the first mathematical, i.e., non-syntactical, model of the untyped λ-calculus) is the equality of the 'infinite η contraction' of BTs. The full abstraction results in the literature for encodings of λ-calculus into π-calculus, however, only concern LTs.

A major reason for the limited attention that the full abstraction issue for encodings of λ-calculus into π-calculus has received is that understanding what kind of the structure the encoding produces may be difficult, and the full abstraction proof itself is long and tedious. The contribution of this paper is twofold:

1. We present general conditions for soundness and completeness of an encoding of the λ-calculus with respect to both LTs and BTs. The conditions can be used both on coinductive equivalences such as bisimilarity, and on contextual equivalences such as may and must equivalences. 2. We show that by properly tuning the notion of observability and/or the details of the encoding it is possible to recover BTs in place of LTs.

Some conditions only concern the behavioural equivalence chosen for the π-calculus, and are independent of the encoding; a few conditions are purely syntactic (e.g., certain encoded contexts should be guarded); the only behavioural conditions are equality of β-convertible terms, equality among certain unsolvable terms, and existence of an inverse for certain contexts resulting from the encoding (i.e., the possibility of extracting their immediate subterms, up-to the behavioural equivalence chosen in the π-calculus). We use these properties to derive full abstraction results for BTs and LTs for various encodings and various behavioural equivalence of the π-calculus. For this we exploit a few basic properties of the encodings, making a large reuse of proofs.

In the paper we use the conditions with the π-calculus, but they could also be used in other concurrency formalisms. Structure of the paper. Section 2 collects background material. Section 3 introduces the notion of encoding of the λ-calculus, and concepts related to this. Section 4 presents the conditions for soundness and completeness. Section 5 applies the conditions on a few encodings of call-by-name and strong call-by-name from the literature, and for various behavioural equivalences on the π-calculus. Section 7 briefly discusses refinements of the π-calculus, notably with linear types. Some conclusions are reported in Section 8.

Background

The λ-calculus We use M, N to range over the set Λ of λ-terms, and x, y, z to range over variables. The standard syntax of λ-terms, and the rules for call-by-name and strong call-by-name (where reduction may continue underneath a λ-abstraction), are recalled in Appendix A. We assume the standard concepts of free and bound variables and substitutions, and identify α-convertible terms. We write Ω for the divergent term (λx. xx)(λx. xx). Intuitively, a term M has order of unsolvability n (0 n < ω) if it behaves like Ω after n initial abstractions; M has order of unsolvability ∞ if it can reduce to an unbounded number of nested abstractions; M is solvable otherwise, with a head normal form of the shape λ x. yM 1 . . . M n .

Definition 1 (Lévy-Longo trees and Böhm trees). The Lévy-Longo Tree of M ∈ Λ is the labelled tree, LT(M), defined coinductively as follows:

1. LT (M ) = ⊤ if M is an unsolvable of order ∞; 2. LT (M ) = λx 1 . . . x n . ⊥ if M is an unsolvable of order n; 3. LT (M ) = λ x. y LT (M 1 ) • • • • • • LT (M n )
if M has head normal form λ x. yM 1 . . . M n , n 0.

Two terms M, N have the same LT if LT (M ) = LT (N ). The definition of Böhm trees (BTs) is obtained from that of LTs using BT in place of LT in the definition above, and demanding that BT (M ) = ⊥ whenever M is unsolvable (in place of clauses (1) and ( 2)).

See [START_REF] Dezani-Ciancaglini | From Bohm's theorem to observational equivalences: an informal account[END_REF] for a thorough tutorial on observational equivalences for such trees.

The (asynchronous) π-calculus We first consider encodings into the asynchronous π-calculus because its theory is simpler and because it is the usual target language for encodings of the λ-calculus. In all encodings we consider, the encoding of a λ-term is parametric on a name, that is, is a function from names to π-calculus processes. We call such expressions abstractions. For the purposes of this paper unary abstractions, i.e., with only one parameter, suffice. The actual instantiation of the parameter of an abstraction F is done via the application construct F a . We use P, Q for process, F for abstractions. Processes and abstractions form the set of π-agents (or simply agents), ranged over by A. Small letters a, b, . . . , x, y, . . . range over the infinite set of names. We use a tilde to indicate tuples; and given a tuple t, we write t i for the i-th component of the tuple. Substitutions are ranged over by σ. The grammar of the calculus is thus:

A := P | F (agents)
P := 0 | a( b). P | a b | P 1 | P 2 | νa P | !a( b). P | F a (processes) F := (a) P (abstractions)
Since the calculus is polyadic, we assume a sorting system [START_REF] Milner | Communicating and Mobile Systems: the π-Calculus[END_REF] to avoid disagreements in the arities of the tuples of names carried by a given name. We will not present the sorting system because not essential. The reader should take for granted that all agents described obey a sorting. A context C of π is a π-agent in which some subterms have been replaced by the hole

[•] or, if the context is polyadic, with indexed holes [•] 1 , . . . , [•] n ; then C[A] or C[ A]
is the agent resulting from replacing the holes with the terms A or A. If the initial expression was an abstraction, we call the context an abstraction π-context ; otherwise it is a process π-context. (A hole itself may stand for an abstraction or a process.) A name in a statement is fresh if it does not occur in the objects of the statement.

The operational semantics of the π-calculus is recalled in Appendix B. Transitions are of the form P -→P ′ or (µ = τ and P = P ′ ). In bisimulations or similar coinductive relations for the asynchronous π-calculus, no name instantiation is required in the input clause or elsewhere (provided α-convertible processes are identified); i.e., the ground versions of the relations are congruences or precongruences [START_REF] Sangiorgi | The π-calculus: a Theory of Mobile Processes[END_REF].

Definition 2 (bisimilarity). Bisimilarity is the largest symmetric relation ≈ on π-processes such that whenever P ≈ Q and P

µ -→ P ′ then Q µ =⇒ Q ′ and P ≈ Q ′ .
A key preorder in our work will be expansion [START_REF] Arun-Kumar | An efficiency preorder for processes[END_REF][START_REF] Sangiorgi | The π-calculus: a Theory of Mobile Processes[END_REF]; this is a refinement of bisimulation that takes into account the number of internal actions in simulation. Intuitively, Q expands P if they are weak bisimilar and moreover Q has no fewer internal actions when simulating P .

Definition 3 (expansion relation).

A relation R on π-processes is an expansion relation if whenever P R Q:

-if P µ -→ P ′ then Q µ =⇒ Q ′ and P ′ R Q ′ ; -if Q µ -→ Q ′ then P µ -→ P ′ and P ′ R Q ′ ;
We write for the largest expansion relation, and simply call it expansion. We also need the 'divergence-sensitive' variant of expansion, written ⇑ , as an auxiliary relation when dealing with must equivalences. Using ⇑ to indicate divergence (i.e., P ⇑ if P can undergo an infinite sequence of τ transitions), then ⇑ is obtained by adding into Definition 3 the requirement that Q ⇑ implies P ⇑. We write and ⇑ for the inverse of and ⇑ , respectively. The predicate ⇓ indicates barb-observability (i.e., P ⇓ if P =⇒ µ -→ for some µ other than τ ). As instance of a contextual divergence-sensitive equivalence, we consider musttermination, because of the simplicity of its definition -other choices would have been possible. Definition 4 (may and must equivalences). The π-processes P and Q are may equivalent, written P ∼ may Q, if in all process contexts C we have

C[P ] ⇓ iff C[Q] ⇓. They are must-termination equivalent (briefly must equivalent), written P ∼ must Q, if in all process contexts C we have C[P ] ⇑ iff C[Q] ⇑.
The behavioural relations defined above make use of the standard observables of the π-calculus; the relations can be made coarser by using the observables of asynchronous calculi, where one takes into account that, since outputs are not blocking, only output transitions from tested processes are immediately detected by an observer. In our examples, the option of asynchronous observable will make a difference only in the case of may equivalence. In asynchronous may equivalence, ∼ asy may , the barb-observability predicate ⇓ is replaced by the asynchronous barbobservability predicate ⇓ asy , whereby P ⇓ asy holds if P = =⇒ µ -→ and µ is an output action. We have ⊆ ≈ ⊆ ∼ may ⊆ ∼ asy may , and ⇑ ⊆ ∼ must . The following results will be useful later. A process is inactive if it may never perform a visible action.

Lemma 1. For all process context C, we have:.

1. if P is inactive, then C[P ] ⇓ implies C[Q] ⇓, and C[P ] ⇓ asy implies C[Q] ⇓ asy ,
and C[a( x). P ] ⇓ asy implies

C[P ] ⇓ asy ; 2. if P ⇑ then C[Q] ⇑ implies C[P ] ⇑. Lemma 2. νa (a b | a( x). P ) ⇑ P { b / x}.

Encodings of the λ-calculus and full abstraction

In this paper an 'encoding of the λ-calculus into π-calculus' is supposed to be compositional (a mapping to π-calculus agents defined structurally on λ-terms), and uniform. The 'uniformity' condition refers to the treatment of the free variables: if the λ-term M and M ′ are the same modulo a renaming of free variables, then also their encodings should be same modulo a renaming of free names; since, in our encodings, λ-variables are included in the set of π-calculus names, a way of ensuring uniformity is to require that the encoding commutes with substitution, i.e., [

[M σ]] ≡ [[M ]]σ.
A compositional encoding can be extended to contexts. We will sometimes use:

-C x λ def = [[λx. [•]]],
an abstraction contexts of [[ ]] (the hole represents the body of an abstraction);

-C x,n var def = [[x[•] 1 • • • [•] n ]] (for n 0), a variable contexts of [[ ]]
(an application context in which the head is a variable and the holes represent the following sequence of terms).

In the remainder of the paper, 'encoding' refers to a 'compositional and uniform encoding of the λ-calculus into the π-calculus'.

Definition 5 (soundness, completeness, full abstraction, validity of β rule). An encoding [[ ]] and a relation R on π-agents are

-sound for LTs if [[M ]] R [[N ]] implies LT (M ) = LT (N ), for all M, N ∈ Λ; -complete for LTSs if LT (M ) = LT (N ) implies [[M ]] R [[N ]]
, for all M, N ∈ Λ; -fully abstract for LTs if they are both sound and complete for LTs.

The same definitions will also be applied to BTs -just replace 'LT' with 'BT'.

Moreover,

[[ ]] and R validate rule β if [[(λx. M )N ]] R [[M { N /x}]],
for all x, M, N .

Conditions for completeness and soundness

We first give the conditions for completeness of an encoding [[ ]] from the λcalculus into π with respect to a relation ≍ on π-agents; then those for soundness. In both cases, the conditions involve an auxiliary relation ≤ on on π-agents.

Completeness conditions. In the conditions for completeness the auxiliary precongruence ≤ is required so to validate an 'up-to ≤ and contexts' technique. Such technique is inspired by the the 'up-to expansion and contexts' technique for bisimulation [START_REF] Sangiorgi | The π-calculus: a Theory of Mobile Processes[END_REF], which allows us the following flexibility in the bisimulation game required on a candidate relation R: given a pair of derivatives P and Q, it is not necessary that the pair (P, Q) itself be in R, as in the ordinary definition of bisimulation; it is sufficient to find processes P , Q, and a context C such that P C[ P ], Q C[ Q], and P R Q; that is, we can manipulate the original derivatives in terms of so to isolate a common context C; this context is removed and only the resulting processes P , Q need to be in R. In the technique, the expansion relation is important: replacing it with bisimilarity breaks correctness. Also, some care is necessary when a hole of the contexts occurs underneath an input prefix, in which case a closure under name substitutions is required. Below, the technique is formulated in an abstract manner, using generic relations ≍ and ≤. In the encodings we shall examine, ≍ will be any of the congruence relations in Section 2, whereas ≤ will always be the expansion relation (or its divergence-sensitive variant, when ≍ is must equivalence).

Definition 6 (up-to-≤-and-contexts technique). Relation ≍ validates the up-to-≤-and-contexts technique if for any symmetric relation R on π-processes

we have R ⊆ ≍ whenever for any pair

(P, Q) ∈ R, if P µ -→ P ′ then Q µ =⇒ Q ′ and there are processes P , Q and a context C such that P ′ ≥ C[ P ], Q ′ ≥ C[ Q],
and, if n 0 is the length of the tuples P and Q, at least one of the following statements is true, for each i n:

1. P i ≍ Q i ; 2. P i R Q i and, if [•] i occurs under an input in C, also P i σ R Q i σ for all substitutions σ.
Below is the core of the completeness conditions. Some of these conditions ((1)-( 3)) only concern the chosen behavioural equivalence ≍ and its auxiliary relation ≤, and are independent of the encoding; the most important condition is the validity of the up-to-≤-and-contexts technique. Other conditions (such as (4)) are purely syntactic. The only behavioural conditions on the encoding are ( 5), (6) (plus (ii) in Theorem 1). They concern validity of β rule and equality of certain unsolvablesvery basic requirements for the operational correctness of an encoding.

(a) [[M ]] ≍ [[Ω]] and [[N ]] ≍ [[Ω]]; (b) [[M ]] ≥ C x λ [[[M 1 ]]], [[N ]] ≥ C x λ [[[N 1 ]]] and ([[M 1 ]], [[N 1 ]]) ∈ R; (c) [[M ]] ≥ C x,n var [[[M 1 ]], . . . , [[M n ]]], [[N ]] ≥ C x,n var [[[N 1 ]], . . . , [[N n ]]] and ([[N i ]], [[N i ]]) ∈ R for all i.
Here, (a) is used when M and N are unsolvable of order 0, by appealing to clause (6) of Definition 7. In the remaining cases we obtain (b) or (c), depending on the shape of the LT for M and N , and appealing to clause (5) of Definition 7. The crux of the proof is exploiting the property that ≍ validates the up-to-≤and-contexts technique so to derive R ⊆ ≍. Intuitively, this is possible because the variable and abstraction contexts of [[ ]] are guarded, and therefore the first action from terms such as

C x λ [[[M 1 ]]] and C x,n var [[[M 1 ]], . . . , [[M n ]]
] only consumes the context, and because ≤ is an expansion relation (clause (2) of Definition 7). Note that condition (2) of Definition 6 requires closure under substitutions when a hole is underneath a prefix. In clause (c) above we can derive closure under substitutions from ([

[N i ]], [[N i ]]) ∈ R
because the LT equality is preserved by variable renaming and because we assume an encoding to act uniformly on the free names (Section 3).

In the results for BTs, the condition on abstraction contexts being guarded is not needed because the condition can be proved redundant in presence of the condition in the assertion (ii) of the theorem. Intuitively, the reason is that, if in a term the head reduction never unveils a variable, then the term is unsolvable and can be equated to Ω using condition (ii); if it does unveil a variable, then in the encoding the subterms following the variable are underneath at least one prefix (because the variable contexts of the encoding are guarded, by condition ( 4)) and then we are able to apply a reasoning similar to that in clause (c) above. Also, we do not need to explicitly prove [[λx. Ω]] ≍ [[Ω]], this can be derived from condition (ii) and clauses ( 5) and ( 6) of Definition 7.

Soundness conditions

In the conditions for soundness, one of the key requirements will be that certain contexts have an inverse. This intuitively means that it is possible to extract any of the processes in the holes of the context, up to the chosen behavioural equivalence. To have some more flexibility, we allow the appearance of the process of a hole after a rendez-vous with the external observer. This allows us to: initially restrict some names that are used to consume the context; then export such names before revealing the process of the hole. The reason why the restriction followed by the export of these names is useful is that the names might occur in the process of the hole; initially restricting them allows us to hide the names to the external environment; exporting them allows to remove the restrictions once the inversion work on the context is completed. The drawback of this initial rendez-vous is that we have to require a prefix-cancellation property on the behavioural equivalence; however, the requirement is straightforward to check in common behavioural equivalences.

We give the definition of inversion only for abstraction π-contexts whose holes are themselves abstractions. We only need this form of contexts when reasoning on λ-calculus encodings. Definition 8. Let C be an abstraction π-context with n holes, each occurring exactly once, each hole itself standing for an abstraction. We say that C has inverse with respect to a relation R on π-agents, if for every i = 1, . . . , n and for every A there exists a process π-context D i and fresh names a, z, b such that

D i [C[ A]] R (ν b )(a c | b(z). A i z ) , for b ∈ b ⊆ c.
It is useful to establish inverse properties for contexts for the finest possible behavioural relation, so to export the result to coarser relations. In our work, the finest such relation is the divergence-sensitive expansion ( ⇑ ).

Example 1.

We show examples of inversion using contexts that are similar to some abstraction and variable contexts in encodings of λ-calculus.

1. Consider a context C def = (p) p(x, q). ([•] q ). If F fills the context, then an inverse for ⇑ is the context

D def = νb (a b | b(r). νp ([•] p | p x, r ))
where all names are fresh (i.e., not free in F ). Indeed we have, using simple algebraic manipulations (such as the law of Lemma 2):

D[C[F ]] ⇑ νb (a b | b(r). νp (p(x, q). F q | p x, r )) ⇑ νb (a b | b(r). F r ) 2. Consider now a context C def = (p) (νr, y )(x r | r y, p | !y(q). [•] q ). If F fills the hole, then an inverse context is D def = ((νx, p, b )([•] p | x(r). r(y, z). (a x, b | b(u). y u )) (1)
where again all names are fresh with respect to F . We have: The cancellation property is straightforward for a behavioural relation ≍ because, in the initial processes, the output a c is the only possible initial action, after which the input at b must fire (the assumption 'a, b fresh' facilitates matters, though it is not essential).

D[C[F ]] = (νx, p, b )((C[F ]) p | x(r). r(y, z). (a x, b | b(u). y u )) ⇑ (νx, p, b )(νr, y )(x r | r y, p | !y(q). F q ) | x(r). r(y, z). (a x, b | b(u). y u ) ⇑ (νx, b)(νy (!y(q). F q | (a x, b | b(u). y u ))) ⇑ (νx, b)(a x, b | b(r). (νy (!y(q). F q | y r ))) ⇑ b)(a x
As for completeness, so for soundness we isolate the common conditions for LTs and BTs. Besides the conditions on inverse of contexts, the other main requirement is about the inequality among some structurally different λ-terms (condition 6). Definition 10. Let ≍ and ≤ be relations on π-agents where 1. ≍ is a congruence, ≤ a precongruence, 2. ≍ ⊇ ≥; 3. ≍ has the rendez-vous cancellation property.

An encoding [

[ ]] of the λ-calculus into π-calculus is respectful for ≍ under ≤ if 4. [[ ]] and ≥ validate rule β; 5. if M is an unsolvable of order 0, then [[M ]] ≍ [[Ω]]; 6. the terms [[Ω]], [[x M ]], [[x M ′ ]],

The condition on variable context having an inverse is the most delicate

In the encodings of the π-calculus we have examined, however, the condition is simple to achieve. For the proof of Theorem 2, we use a coinductive definition of LT and BT equality, as forms of bisimulation. Then we show that the relation

{(M, N ) | [[M ]] ≍ [[N ]
]} implies the corresponding tree equality. In the case of internal nodes of the trees, we exploit conditions such as ( 6) and ( 7) of Definition 10.

Full abstraction

We put together Theorems 1 and 2. In Theorems 1(i) and 3(i) for LTs the abstraction contexts are required to be guarded. This is reasonable in encodings of strategies, such as call-by-name, where evaluation does not continue underneath a λ-abstraction, but it is too demanding when evaluation can go past a λ-abstraction, such as strong call-by-name. We therefore present also the following alternative condition:

M, N unsolvable of order ∞ implies [[M ]] ≍ [[N ]].
( * ) Theorem 4. Theorems 1(i) and 3(i) continue to hold when the condition that the abstraction contexts be guarded is replaced by ( * ) above.

Examples with call-by-name

In this section we apply the theorems on soundness and completeness in the previous section to two well-known encodings of call-by-name λ-calculus: the one in Figure 1.a is Milner's original encoding [START_REF] Milner | Functions as processes[END_REF]. The one in Figure 1.b is a variant encoding in which a function communicates with its environment via a rendez-vous (request/answer) pattern. An advantage of this encoding is that it can be easily tuned to call-by-need, or even used in combination with call-by-value [START_REF] Sangiorgi | The π-calculus: a Theory of Mobile Processes[END_REF].

For each encoding we consider soundness and completeness with respect to four behavioural equivalences: bisimilarity (≈), may (∼ may ), must (∼ must ), and asynchronous may (∼ asy may ). The following lemma allows us to apply the up-to-≤and-contexts technique. Lemma 3. Relations ≈, ∼ may , and ∼ asy may validate the up-to--and-contexts technique; relation ∼ must validates the up-to-⇑ -and-contexts technique.

The result in Lemma 3 for bisimulation is from [START_REF] Sangiorgi | The π-calculus: a Theory of Mobile Processes[END_REF]. The proofs for the may equivalences follow the definitions of the equivalences, reasoning by induction on the number of steps required to bring out an observable. The proof for the must equivalence uses coinduction to reason on divergent paths. Both for the may and for the must equivalences, the role of expansion ( ) is similar to its role in the technique for bisimulation.

Theorem 5. The encoding of Figure 1.a is fully abstract for LTs when the behavioural equivalence for π-calculus is ≈, ∼ may , or ∼ must ; and fully abstract for BTs when the behavioural equivalence is ∼ asy may . The encoding of Figure 1.b is fully abstract for LTs under any of the equivalences ≈, ∼ may , ∼ must , or ∼ asy may .

As Lemma 3 brings up, in the proofs, the auxiliary relation for ≈, ∼ may , and ∼ asy may is ; for ∼ must it is ⇑ . With Lemma 3 at hand, the proofs for the soundness and completeness statements are simple. Moreover, there is a large reuse of proofs and results. For instance, in the completeness results for LTs, we only have to check that: the variable and abstraction contexts of the encoding are guarded; β rule is validated; all unsolvable of order 0 are equated. The first check is straightforward and is done only once. For the β rule, it suffices to establish its validity for ⇑ , which is the finest among the behavioural relations considered; this is done using distributivity laws for private replications [START_REF] Sangiorgi | The π-calculus: a Theory of Mobile Processes[END_REF], which are valid for strong bisimilarity and hence for ⇑ , and the law of Lemma 2. Similarly, for the unsolvable terms of order 0 it suffices to prove that they are all 'purely divergent' (i.e., divergent and unable to even perform some visible action), which follows from the validity of the β rule for ⇑ .

[[λx. M ]] def = (p) p(x, q). [[M ]] q [[x]] def = (p) x p [[M N ]] def = (p) (νr, x ) [[M ]] r | r x, p | !x(q). [[N ]] q (for x fresh)
Fig. 1.a: Milner's encoding Having checked the conditions for completeness, the only two additional conditions needed for soundness for LTs are conditions ( 6) and ( 7) of Definition 10, where we have to prove that certain terms are unrelated and that certain contexts have an inverse. The non-equivalence of the terms in condition ( 6) can be established for the coarsest equivalences, namely ∼ asy may and ∼ must , and then exported to the other equivalences. It suffices to look at visible traces of length 1 at most, except for terms of the form [[x M ]] and [[x M ′ ]], when tuples M and M ′ have different lengths, in which case one reasons by induction on the shortest of the two tuples.

[[λx. M ]] def = (p) νv (p v | v(x, q). [[M ]] q ) [[x]] def = (p) x p [[M N ]] def = (p) νr [[M ]] r | r(v). νx (v x, p | !x(q). [[N ]] q ) (for x fresh)
The most delicate point is the existence of an inverse for the abstraction and the variable contexts. This can be established for the finest equivalence ( ⇑ ), and then exported to coarser equivalences. The two constructions needed for this are similar to those examined in Example 1. For Milner's encoding, in the case of ∼ asy may , we actually obtain the BT equality. One may find this surprising at first: BTs are defined from weak head reduction, in which evaluation continues underneath a λ-abstraction; however Milner's encoding mimics the call-by-name strategy, where reduction stops when a λ-abstraction is uncovered. We obtain BTs with ∼ asy may by exploiting Lemma 1(1) as follows. The encoding of a term λx. M is (p) p(x, q). [[M ]] q . In an asynchronous semantics, an input is not directly observable; with ∼ asy may an input prefix can actually be erased provided, intuitively, that an output is never liberated. We sketch the proof of )

[[λx. M ]] def = (p) (νx, q)(p x, q | [[M ]] q ) [[x]] def = (p) (x(p ′ ). (p ′ ⊲ p)) [[M N ]] def = (p) (νq, r)([[M ]] q | q(x, p ′ ). (p ′ ⊲ p | !x r . [[N ]] r )) (for x fresh)
where r ⊲ q def = r(y, h). q y, h Fig. 2: Encoding of strong call-by-name

6 An example with strong call-by-name

In this section we consider a different λ-calculus strategy, strong call-by-name, where the evaluation of a term may continue underneath a λ-abstraction. The main reason is that we wish to see the impact of this difference on the equivalences induced by the encodings. Intuitively, evaluation underneath a λ-abstraction is fundamental in the definition of BTs and therefore we expect that obtaining the BT equality will be easier. However, the LT equality will still be predominant: in BTs a λ-abstraction is sometimes unobservable, whereas in an encoding into π-calculus a λ-abstraction always introduces a few prefixes, which are observable in the most common behavioural equivalences.

The encoding of strong call-by-name, from [START_REF] Hirschkoff | Duality and i/o-types in the π-calculus[END_REF], is in Figure 2. The encoding behaves similarly to that in Figure 1.b; reduction underneath a 'λ' is implemented by exploting special wire processes (such as q ⊲ p). They allow us to split the body M of an abstraction from its head λx; then the wires make the liaison between the head and the body. It actually uses the synchronous π-calculus, because some of the output prefixes have a continuation. Therefore the encoding also offers us the possibility of discussing the portability of our conditions to the synchronous π-calculus. For this, the only point in which some care is needed is that in the synchronous π-calculus, bisimilarity and expansion need some closure under name substitutions, in the input clause (on the placeholder name of the input), and the outermost level (i.e., before the bisimulation or expansion game is started) to become congruence or precongruence relations. Name substitutions may be applied following the early, late or open styles. The move from a style to another one does not affect the results in terms of BTs and LTs in the paper. We omit the definitions, see e.g., [START_REF] Sangiorgi | The π-calculus: a Theory of Mobile Processes[END_REF].

In short, for any of the standard behavioural congruences and expansion precongruences of the synchronous π-calculus, the conditions concerning ≍ and ≤ of the theorems in Section 4 remain valid. In Theorem 6 below, we continue to use the symbols ≈ and for bisimilarity and expansion, assuming that these are bisimulation congruences and expansion precongruences in any of the common π-calculus styles (early, late, open). (Again, in the case of must equivalence the expansion preorder should be divergence sensitive.) The proof of Theorem 6 is similar to that of Theorem 5. The main difference is that, since in strong call-by-name the abstraction contexts are not guarded, we have to adopt the modification in one of the conditions for LTs suggested in Theorem 4. Moreover, for the proof of validity of β rule for , we use the following law to reason about wire processes r ⊲ q (and similarly for ⇑ ):

νq (q ⊲ p | P ) P { p /q} provided p does not appear free in P , and q only appears free in P only once, in a subexpression of the form q v . 0. Theorem 6. The encoding of Figure 2 is fully abstract for LTs when the behavioural equivalence for the π-calculus is ≈, ∼ may , or ∼ asy may ; and fully abstract for BTs when the behavioural equivalence is ∼ must .

Thus we obtain the BT equality for the must equivalence. Indeed, under strong call-by-name, all unsolvable terms are divergent. In contrast with Milner's encoding of Figure 1.a, under asynchronous may equivalence we obtain LTs because in both encodings of strong call-by-name the first action of an abstraction is an output, rather than an input as in Milner's encoding, and outputs are observable in asynchronous equivalences.

Types and asynchrony

We show, using Milner's encoding (Figure 1.a), that we can sometimes switch from LTs to BTs by taking into account some simple type information together with asynchronous forms of behavioural equivalences. The type information needed is the linearity of the parameter name of the encoding (names p, q, r in Figure 1.a). Linearity ensures us that the external environment can never cause interferences along these names: if the input capability is used by the process encoding a λ-term, then the external environment cannot exercise the same (competing) capability. In an asynchronous behavioural equivalence input prefixes are not directly observable (as discussed earlier for asynchronous may).

Linear types and asynchrony can easily be incorporate in a bisimulation congruence by using a contextual form of bisimulation such as barbed congruence [START_REF] Sangiorgi | The π-calculus: a Theory of Mobile Processes[END_REF]. In this case, barbs (the observables of barbed congruence) are only produced by output prefixes (as in asynchronous may equivalence); and the contexts in which processes may be tested should respect the type information ascribed to processes (in particular the linearity mentioned earlier). We write ≈ lin,asy bc for the resulting asynchronous typed barbed congruence. Using Theorem 3(ii) we obtain: Theorem 7. The encoding of Figure 1.a is fully abstract for BTs when the behavioural equivalence for the π-calculus is ≈ lin,asy bc .

The auxiliary relation is still ; here asynchrony and linearity are not needed.

Conclusions and future work

In this paper we have studied soundness and completeness conditions with respect to BTs and LTs for encodings of λ-calculus into the π-calculus. While the conditions have been presented on the π-calculus, they can be adapted to other concurrency formalisms. For instance, expansion, a key preorder in our conditions, can always be extracted from bisimilarity as its "efficiency" preorder. It might be difficult, in contrast, to adapt our conditions to sequential languages; a delicate condition, for instance, appears to be the one on inversion of variable contexts.

We have used the conditions to derive tree characterisations for various encodings and various behavioural equivalences, including bisimilarity, may and must equivalences, and asynchronous variants of them (see a summary in Appendix C). The proofs of the conditions can often be transported from a behavioural equivalence to another one, with little or no extra work (e.g., exploiting containments among equivalences and preorders). Overall, we found the conditions particularly useful when dealing with contextual equivalences, such as may and must equivalences. It is unclear to us how soundness and completeness could be proved for them by relying on, e.g., direct characterisations of the equivalences (such as trace equivalence or forms of acceptance trees) and standard proof techniques for them.

It would be interesting to examine additional conditions on the behavioural equivalences of the π-calculus capable to retrieve, as equivalence induced by an encoding, that of BTs under η contraction, or BTs under infinite η contractions [START_REF] Barendregt | The Lambda Calculus: Syntax, semantics[END_REF]. Works on linearity in the π-calculus, such as [START_REF] Yoshida | Linearity and bisimulation[END_REF] might be useful.

In the paper we have considered encodings of call-by-name or strong call-byname. These strategies fit the definition of BTs and LTs, in which reduction always picks the leftmost redex. We do not know, in contrast, what kind of tree structures could be obtained from encodings of the call-by-value strategy.

-=

  (an input, b are the bound names of the input prefix that has been fired), P ν d a b -→ P ′ (an output, where d ⊆ b are private names extruded in the output), and P τ -→ P ′ (an internal action). We use µ to range over the labels of transitions. We write =⇒ for the reflexive transitive closure of τ =⇒ if µ is not τ , and = =⇒ otherwise; finally P µ -→P ′ holds if P µ

Definition 7 .

 7 Let ≍ and ≤ be relations on π-agents such that:1. ≍ is a congruence and ≍ ⊇ ≥; 2. ≤ is an expansion relation and is a precongruence; 3. ≍ validates the up-to-≤-and-contexts technique.Now, an encoding[[ ]] of the λ-calculus into π-calculus is faithful for ≍ under ≤ if 4. the variable contexts of [[ ]] are guarded; 5. [[ ]] and ≥ validate rule β; 6. if M is an unsolvable of order 0 then [[M ]] ≍ [[Ω]].Theorem 1 (completeness). Let [[ ]] be an encoding of the λ-calculus into πcalculus, and ≍ a relation on π-agents. Suppose there is relation ≤ on π-agents such that [[ ]] is faithful for ≍ under ≤. We have: (i) if the abstraction contexts of [[ ]] are guarded, then [[ ]] and ≍ are complete for LTs; (ii) if [[M ]] ≍ [[Ω]] whenever M is unsolvable of order ∞, then [[ ]] and ≍ are complete for BTs. The proofs for LTs and BTs are similar. In the proof for LTs, for instance, we consider the relation R def = {([[M ]], [[N ]]) s.t. LT (M ) = LT (N )} and show that for each ([[M ]], [[N ]]) ∈ R one of the following conditions is true, for some abstraction context C x λ , variable context C x,n var , and terms M i , N i :

  , b | b(r). F r ) Definition 9. A relation R on π-agents has the rendez-vous cancellation property if whenever ν b (a c | b(r). P ) R ν b (a c | b(r). Q) where b ∈ b ⊆ c and a, b are fresh, then also P R Q.

  and [[y M ′′ ]] are pairwise unrelated by ≍, assuming that x = y and that tuples M and M ′ have different lengths; 7. the abstraction and variable contexts of [[ ]] have inverse with respect to ≥.

Theorem 2 (

 2 soundness). Let [[ ]] be an encoding of the λ-calculus into π-calculus, and ≍ a relation on π-agents. Suppose there is a relation ≤ on π-agents such that [[ ]] is is respectful for ≍ under ≤. We have: 1. if, for any M , the term [[λx. M ]] is unrelated by ≍ to [[Ω]] and to any term of the form [[x M ]], then [[ ]] and ≍ are sound for LTs; 2. if (a) [[M ]] ≍ [[Ω]] whenever M is unsolvable of order ∞, (b) M solvable implies that the term [[λx. M ]] is unrelated by ≍ to [[Ω]] and to any term of the form [[x M ]], then [[ ]] and ≍ are sound for BTs.

Theorem 3 .

 3 Let [[ ]] be an encoding of the λ-calculus into π-calculus, ≍ a congruence relation on π-agents. Suppose there is a precongruence ≤ on π-agents such that 1. ≤ is an expansion relation and ≍ ⊇ ≥; 2. ≍ validates the up-to-≤-and-contexts technique; 3. the variable contexts of [[ ]] are guarded; 4. the abstraction and variable contexts of [[ ]] have inverse with respect to ≥; 5. [[ ]] and ≥ validate rule β; 6. if M is an unsolvable of order 0 then [[M ]] ≍ [[Ω]]; 7. the terms [[Ω]], [[x M ]], [[x M ′ ]], and [[y M ′′ ]] are pairwise unrelated by ≍, assuming that x = y and that tuples M and M ′ have different lengths. We have: (i) if (a) the abstraction contexts of [[ ]] are guarded, and (b) for any M the term [[λx. M ]] is unrelated by ≍ to [[Ω]] and to any term of the form [[x M ]], then [[ ]] and ≍ are fully abstract for LTs; (ii) if (a) M solvable implies that the term [[λx. M ]] is unrelated by ≍ to [[Ω]] and to any term of the form [[x M ]], and (b) [[M ]] ≍ [[Ω]] whenever M is unsolvable of order ∞, then [[ ]] and ≍ are fully abstract for BTs.

Fig. 1 .Fig. 1 :

 11 Fig. 1.b: a variant encoding Fig. 1: The two encodings of call-by-name

  [[M ]] ∼ asy may [[Ω]] whenever M is unsolvable of order ∞, as required in condition (ii) of Theorem 3. Consider a context C with C[[[M ]]] ⇓, and suppose the observable is reached after n internal reductions. Term M , as ∞-unsolvable, can be β-reduced to M ′ def = (λx) n . N , for some N . By validity of β-rule for , also C[[[M ′ ]]] ⇓ in at most n steps; hence the subterm [[N ]] of [[M ′ ]] does not contribute to the observable, since the abstraction contexts of the encodings are guarded and M ′ has n initial abstractions. We thus derive C[[[(λx) n . Ω]]] ⇓ and then, by repeatedly applying the third statement of Lemma 1(1) (as Ω is inactive), also C[[[Ω]]] ⇓. (The converse implication is given by the first statement in Lemma 1(1).

Appendix

A λ-calculus: syntax and call-by-name rules

The set Λ of λ-terms is:

We will encode call-by-name λ-calculus, in its weak or strong form. In both cases, we have rules β and µ, only in the strong case we have also ξ:

B Operational semantics of the π-calculus

Below is the standard operational semantics for the asynchronous polyadic πcalculus (we assume that α-convertible terms are identified). We write fn(P ) for the free names of a process P , and bn(µ) for the bound names of action µ.

C Summary of the results for the encoding examined

The tables below summarise the results with respect to BTs and LTs for the encodings and the behavioural equivalences examined in the paper. In a table, a checkmark means that corresponding the result holds; otherwise the result is false.

We recall that ≈ is weak bisimilarity; ∼ may is may equivalence; ∼ asy may is asynchronous may equivalence; ∼ must is must equivalence; and ≈ lin,asy bc is asynchronous barbed congruence with the linearity type constraints on the location names of the encoded λ-terms (i.e., the abstracted name in the encoding of a λ-term).

≈ ∼may ∼ asy may ∼must ≈


Higher-order languages: bisimulation and coinductive equivalences (extended abstract)

Davide Sangiorgi 1
Università di Bologna and INRIA 1 Summary

Higher-order languages have been widely studied in functional programming, following the λ-calculus. In a higher-order calculus, variables may be instantiated with terms of the language. When multiple occurrences of the variable exist, this mechanism results in the possibility of copying the terms of the language. Equivalence proof of computer programs is an important but challenging problem. Equivalence between two programs means that the programs should behave "in the same manner" under any context [START_REF] Morris | Lambda-Calculus Models of Programming Languages[END_REF]. Finding effective methods for equivalence proofs is particularly challenging in higher-order languages: pure functional languages like the λ-calculus, and richer languages including nonfunctional features such as non-determinism, information hiding mechanisms (e.g., generative names, store, data abstraction), concurrency, and so on.

Bisimulation [Par81a,Par81b,Mil89,San09,San12] has emerged as a very powerful operational method for proving equivalence of programs in various kinds of languages, due to the associated co-inductive proof method. Further, a number of enhancements of the bisimulation method have been studied, usually called up-to techniques. To be useful, the behavioral relation resulting from bisimulationbisimilarity-should be a congruence. Bisimulation has been transplanted onto higher-order languages by Abramsky [Abr90]. This version of bisimulation, called applicative bisimulations, and variants of it, have received considerable attention [START_REF] Gordon | Functional Programming and Input/Output[END_REF][START_REF] Gordon | Bisimilarity for a first-order calculus of objects with subtyping[END_REF][START_REF] Pitts | Operationally-based theories of program equivalence[END_REF][START_REF] Sands | Improvement theory and its applications[END_REF][START_REF] Lassen | Relational Reasoning about Functions and Nondeterminism[END_REF]. In short, two functions P and Q are applicatively bisimilar when their applications P (M ) and Q(M ) are applicatively bisimilar for any argument M .

Applicative bisimulations have some serious limitations. For instance, they are unsound under the presence of generative names [START_REF] Jeffrey | Towards a theory of bisimulation for local names[END_REF] or data abstraction [START_REF] Sumii | A bisimulation for type abstraction and recursion[END_REF] because they apply bisimilar functions to an identical argument. Secondly, congruence proofs of applicative bisimulations are notoriously hard. Such proofs usually rely on Howe's method [START_REF] Douglas | Proving congruence of bisimulation in functional programming languages[END_REF]. The method appears however rather subtle and fragile, for instance under the presence of generative names [START_REF] Jeffrey | Towards a theory of bisimulation for local names[END_REF], non-determinism [START_REF] Douglas | Proving congruence of bisimulation in functional programming languages[END_REF], or concurrency (e.g., [START_REF] Ferreira | A theory of weak bisimulation for core CML[END_REF][START_REF] Chr | Extending Howe's method to early bisimulations for typed mobile embedded resources with local names[END_REF]). Also, the method is very syntactical and lacks good intuition about when and why it works. Related to the problems with congruence are also the difficulties of applicative bisimulations with "up-to context" techniques (the usefulness of these techniques in higher-order languages and its problems with applicative bisimulations have been extensively studied by Lassen [START_REF] Lassen | Relational Reasoning about Functions and Nondeterminism[END_REF]; see also [START_REF] Sands | Improvement theory and its applications[END_REF][START_REF] Koutavas | Small bisimulations for reasoning about higher-order imperative programs[END_REF]).

Congruence proofs for bisimulations usually exploit the bisimulation method itself to establish that the closure of the bisimilarity under contexts is again a bisimulation. To see why, intuitively, this proof does not work for applicative bisimulation, consider a pair of bisimilar functions P 1 , Q 1 and another pair of bisimilar terms P 2 , Q 2 . In an application context they yield the terms P 1 P 2 and Q 1 Q 2 which, if bisimilarity is a congruence, should be bisimilar. However the argument for the functions P 1 and Q 1 are bisimilar, but not necessarily identical: hence we are unable to apply the bisimulation hypothesis on the functions.

Proposals for improving applicative bisimilarity include environmental bisimulations [SKS11,KLS11,PS12] and logical bisimulations [START_REF] Sangiorgi | Logical bisimulations and functional languages[END_REF]. A key idea of environmental bisimulations is to make a clear distinction between the tested terms and the environment. An element of an environmental bisimulation has, in addition to the tested terms, a further component, the environment, which expresses the observer's current knowledge. (In languages richer than pure λcalculi, there may be other components, for instance to keep track of generated names.) The bisimulation requirements for higher-order inputs and outputs naturally follow. For instance, in higher-order outputs, the values emitted by the tested terms are published to the environment, and are added to it, as part of the updated current knowledge. In contrast, when the tested terms perform a higher-order input (e.g., in λ-calculi the tested terms are functions that require an argument), the arguments supplied are terms that the observer can build using the current knowledge; that is, terms obtained by composing the values currently in the environment using the operators of the calculus.

A possible drawback of environmental bisimulations over, say, applicative bisimulations, is that the set of arguments to related functions that have to be considered in the bisimulation clause is larger (since it also includes nonidentical arguments). As a remedy to this is offered by up-to techniques (in particular techniques involving up-to contexts), which are easier to establish for environmental bisimulations than for applicative bisimulations, and which allow us to considerably enhance the bisimulation proof method.

The difference between environmental bisimulations and logical bisimulations is that the latter does not make use of an explicit environment: the environment is implicitly taken to be the set of pairs forming the bisimulation. This simplifies the definition, but has the drawback of making the functional of bisimulation non-monotone. In λ-calculi one usually is able to show that the functional has nevertheless a greatest fixed-point which coincides with contextual equivalence. But in richer languages this does not appear to be possible.

For bisimulation and coinductive techniques, a non-trivial extension of higherorder languages concern probabilities. Probabilistic models are more and more pervasive. Not only they are a formidable tool when dealing with uncertainty and incomplete information, but they sometimes are a necessity rather than an alternative, like in computational cryptography (where, e.g., secure public key encryption schemes need to be probabilistic [START_REF] Goldwasser | Probabilistic encryption[END_REF]). A nice way to deal compu-tationally with probabilistic models is to allow probabilistic choice as a primitive when designing algorithms, this way switching from usual, deterministic computation to a new paradigm, called probabilistic computation. Examples of application areas in which probabilistic computation has proved to be useful include natural language processing [MS99], robotics [START_REF] Thrun | Robotic mapping: A survey[END_REF], computer vision [START_REF] Comaniciu | Kernel-based object tracking[END_REF], and machine learning [Pea88].

This new form of computation, of course, needs to be available to programmers to be accessible. And indeed, various programming languages have been introduced in the last years, spanning from abstract ones [JP89,RP02,PPT08] to more concrete ones [START_REF] Pfeffer | IBAL: A probabilistic rational programming language[END_REF][START_REF] Noah | The principles and practice of probabilistic programming[END_REF], being inspired by various programming paradigms like imperative, functional or even object oriented. A quite common scheme consists in endowing any deterministic language with one or more primitives for probabilistic choice, like binary probabilistic choice or primitives for distributions.

One class of languages which cope well with probabilistic computation are functional languages. Indeed, viewing algorithms as functions allows a smooth integration of distributions into the playground, itself nicely reflected at the level of types through monads [GAB + 13,RP02]. As a matter of fact, many existing probabilistic programming languages [START_REF] Pfeffer | IBAL: A probabilistic rational programming language[END_REF][START_REF] Noah | The principles and practice of probabilistic programming[END_REF] are designed around the λcalculus or one of its incarnations, like Scheme. All these allows to write higherorder functions (programs can take functions as inputs and produce them as outputs).

Bisimulation and context equivalence in a probabilistic λ-calculus have been considered in [START_REF] Alberti | On coinductive equivalences for higher-order probabilistic functional programs[END_REF], where a technique is proposed for proving congruence of probabilistic applicative bisimilarity. While the technique follows Howe's method, some of the technicalities are quite different, relying on non-trivial "disentangling" properties for sets of real numbers, these properties themselves proved by tools from linear algebra. The bisimulation is proved to be sound for contextual equivalence. Completeness, however, fails: applicative bisimilarity is strictly finer. A subtle aspect is also the late vs. early formulation of bisimilarity; with a choice operator the two versions are semantically different; the congruence proof of bisimilarity crucially relies on the late style.

Context equivalence and bisimilarity, however, coincidence on pure λ-terms. The resulting equality is that induced by Levy-Longo trees (LLT), generally accepted as the finest extensional equivalence on pure λ-terms under a lazy regime. The proof follows Böhm-out techniques along the lines of [START_REF] Sangiorgi | The lazy lambda calculus in a concurrency scenario[END_REF][START_REF] Sangiorgi | The pi-Calculus -a theory of mobile processes[END_REF]. The result is in sharp contrast with what happens under a nondeterministic interpretation of choice (or in the absence of choice), where context equivalence is coarser than LLT equality.

A coinductive characterisation of context equivalence on the whole probabilistic language is possible via an extension in which weighted formal sumsterms akin to distributions -may appear in redex position. Thinking of distributions as sets of terms, the construction reminds us of the reduction of nondeterministic to deterministic automata. The technical details are however quite different, because we are in a higher-order language and therefore -once more -we are faced with the congruence problem for bisimulation, and because formal sums may contain an infinite number of terms. The proof of congruence of bisimulation in this extended language uses the technique of logical bisimulation, therefore allowing bisimilar functions to be tested with bisimilar (rather than identical) arguments (more precisely, the arguments should be in the context closure of the bisimulation). In the probabilistic setting, however, the ordinary logical bisimulation game has to be modified substantially. For instance, formal sums represent possible evolutions of running terms, hence they should appear in redex position only (allowing them anywhere would complicate considerably). The obligation of redex position for certain terms is in contrast with the basic schema of logical bisimulation, in which related terms can be used as arguments to bisimilar functions and can therefore end up in arbitrary positions. This problem is solved by moving to coupled logical bisimulations, where a bisimulation is formed by a pair of relations, one on ordinary terms, the other on terms extended with formal sums. The bisimulation game is played on both relations, but only the first relation is used to assemble input arguments for functions.

In higher-order languages coinductive equivalences and techniques appear to be more fundamental than in first-order languages. Evidence of this are the above-mentioned results of correspondence between forms of bisimilarity and contextual equivalence in various λ-calculi. Contextual equivalence is a 'may' of form of testing that, in first-order languages (e.g., CCS) is quite different from bisimilarity or even simulation equivalence. Indeed, in general, higher-order languages have a stronger discriminating power than first-order languages [START_REF] Bernardo | On the discriminating power of passivation and higher-order interaction[END_REF]. For instance, if we use higher-order languages to test first-order languages, using (may-like) contextual equivalence, then the equivalences induced is often finer than the equivalences induced by first-order languages (usually trace equivalence); moreover, the natural definition of the former equivalences is coinductive, whereas that for the latter equivalences is inductive. In distributed higher-order languages, a construct that may strongly enhance the discriminating power is passivation [SS03,GH05a,LSS09a,LSS09b,LSS11,LPSS11,PS12,KH13]. Passivation offers the capability of capturing the content of a certain location into a variable, possibly copying it, and then restarting the execution in different contexts. The same discriminating power can also be obtained in call-by-value λ-calculi (that is, without concurrency or nondeterminism) extended with a location-like construct akin to a store of imperative λ-calculi, and operators for reading the content of this location, overriding it, and, if the location contains a process, for consuming such process (i.e., performing observations on the process actions). When the tested first-order processes are probabilistic, the difference in discriminating power between first-order and higher-order languages increases further: in higher-order languages equipped with passivation, or in a call-by-value λcalculus, bisimilarity may be recovered [START_REF] Bernardo | On the discriminating power of passivation and higher-order interaction[END_REF].


Charles Ricordel

Marie Labalette-Tiercin

Alexandra Lespagnol

Mallorie Kerjouan

Catherine Dugast

Jean Mosser

Benoit Desrues

Hervé Léna
email: herve.lena@chu-rennes.fr

EFGR-mutant lung adenocarcinoma and Li-Fraumeni syndrome: report of two cases and review of the literature

Keywords: Li-Fraumeni syndrome, Non-small cell lung cancer, Epidermal Growth Factor Receptor, Tyrosine Kinase Inhibitor, Molecular biology, Genetic predisposition to cancer

come

A c c e p t e d M a n u s c r i p t

Abstract :

We report two cases of non-smoker patients diagnosed with EGFR-mutated lung adenocarcinoma and bearing germinal TP53 gene mutation, also known as Li-Fraumeni syndrome (LFS). We describe for the first time an EGFR-TKI resistance mutation in this population. Finally, we provide an analysis of discerning epidemiological data obtained from the IARC database and from all the published cases of EGFR-mutated lung cancer in TP53 germline mutation carriers.

A c c e p t e d M a n u s c r i p t

Li-Fraumeni syndrome (LFS) was initially described in the late 60's, based on the report of four families with high tumor occurrence [START_REF] Li | Soft-tissue sarcomas, breast cancer, and other neoplasms. A familial syndrome?[END_REF]. This condition has been characterized by an autosomal dominant predisposition to various malignancies. The principal localizations are sarcomas, gliomas and breast carcinomas. Direct involvement of germline TP53 gene mutations has emerged approximately two decades after the primary description [START_REF] Malkin | Germ line p53 mutations in a familial syndrome of breast cancer, sarcomas, and other neoplasms[END_REF]. In most cases, mutation of the TP53 tumor suppressor gene result in a loss-of-function of p53 protein, leading to alterations in DNA repair, apoptosis cell-cycle control and consequently genome instability [START_REF] Toledo | Regulating the p53 pathway: in vitro hypotheses, in vivo veritas[END_REF]. A worldwide database is now collecting both somatic and germline TP53 mutation on International Agency for Research on Cancer (p53.iarc.fr). Despite growing knowledge about LFS, prevalence of lung cancer is still unknown in this population but an increased risk has been described in observational studies [START_REF] Malkin | Li-fraumeni syndrome[END_REF]. Moreover, the literature is still scarce regarding the molecular abnormalities of lung neoplasms in this particular setting. An early report suggests an association between tumoral TP53 mutation and EGFR-driven lung cancer [START_REF] Cortot | Mutation of TP53 and alteration of p14(arf) expression in EGFR-and KRAS-mutated lung adenocarcinomas[END_REF].

We report two cases of patients with LFS and EGFR-mutated lung adenocarcinoma, and provide the first description of resistance mutation to EGFR-TKI in this population. We highlight a potentially underreported association and emphasize the need for molecular alterations compiling in the particular setting of LFS. Reviewing all the published cases to date, we finally bring perspectives for clinical management. Eastern cooperative oncology group (ECOG) performance status was quantified to 0 at diagnosis. The patient was known to carry a LFS, because emergence of unusual childhood tumors in descendants led to germline TP53 gene sequencing a few years ago (TP53 germline mutation H179Y). First line chemotherapy with platinum and pemetrexed was administered, followed by EGFR-TKI (erlotinib). Three months later, paclitaxel was prescribed because of a cervical and mediastinal progression, which stabilized the disease for eight months. Observational studies show that lung cancer belong to the spectrum of predisposed tumors in LFS [START_REF] Malkin | Li-fraumeni syndrome[END_REF]. According to Chompret criteria revised in 2009, a proband diagnosed with lung cancer before the age of 46 years and with at least one first-degree or second-degree relative with a core LFS tumor should be selected for a TP53 germline mutation testing. Our two patients do not meet these criteria and LFS was evocated because early-onset cancers in family history. Approximately 29%-35% of families with these criteria were shown to have TP53 germline mutations [START_REF] Bougeard | Molecular basis of the Li-Fraumeni syndrome: an update from the French LFS families[END_REF] [START_REF] Gonzalez | Beyond Li Fraumeni Syndrome: clinical characteristics of families with p53 germline mutations[END_REF]. Importantly, recognition of LFS impacts the familial and personal cancer risk assessment, regarding potential radio-induced neoplasms. Thoracic oncologists should be aware of the possibility of this inherited predisposition syndrome especially when familial history of early-onset cancers is known. Our cases highlight the need for exhaustive medical family history interrogation when lung cancer is diagnosed, notably for young and non-smoker patients.

The literature is scarce regarding epidemiologic characteristics of lung cancer in LFS. The International Agency for Research on Cancer mutation database collecting the germline TP53 mutation reports various pathological subtypes in this restricted population [START_REF] Petitjean | Impact of mutant p53 functional properties on TP53 mutation patterns and tumor phenotype: lessons from recent developments in the IARC TP53 database[END_REF].

Adenocarcinomas, including lepidic growth carcinomas (previously known as bronchoalveolar), represent the largest part of the confirmed pathological type when TP53 germline mutation is known (figure 2, panel A). In addition, majority of these tumors arise before the fifth decade and for a large part in women (figure 2, panel B). To date, this database do not contain molecular characteristic of these tumors. In our two patients, EGFR mutational status was unknown at diagnosis, but found during follow-up. Interestingly, co-A c c e p t e d M a n u s c r i p t occurrence of tumoral somatic TP53 mutations and EGFR mutations has been found in 34% of lung adenocarcinomas in a recent international project [9]. Two retrospective studies tried specifically to assess this association, based on mixed genomic and immunohistochemical approaches [START_REF] Cortot | Mutation of TP53 and alteration of p14(arf) expression in EGFR-and KRAS-mutated lung adenocarcinomas[END_REF] [START_REF] Mounawar | Patterns of EGFR, HER2, TP53, and KRAS mutations of p14arf expression in non-small cell lung cancers in relation to smoking history[END_REF]. Tumoral p53/arf pathway inactivation was observed in respectively 100% and 58.1% of EGFR-mutated lung cancers, supporting this hypothesis. Interestingly, a similar distribution of germinal and tumoral mutations is observed in the TP35 gene coding sequence, occurring preferentially in the DNA binding domain (exon 5 to 8). Nevertheless, it appears that all tumoral TP53 mutations are not equivalent regarding their intrinsic prognostic value. Indeed, a recent publication has described that non-disruptive TP53 mutations are associated with a worse outcome in EGFR-mutated NSCLC [START_REF] Molina-Vila | Nondisruptive p53 mutations are associated with shorter survival in advanced non-small-cell lung cancer patients[END_REF]. Moreover, a recent analysis of age of cancer onset from the IARC database suggests unequal repercussion of the different TP53 germline missense mutations [START_REF] Xu | Heterogeneity of Li-Fraumeni syndrome links to unequal gain-of-function effects of p53 mutations[END_REF]. Taken together, these clinical data suggest an important heterogeneity concerning the tumorigenic potential of the different subtype of TP53 mutations.

No exhaustive data concerning molecular biologic characteristics of lung cancers in the context of LFS has been published so far. Nevertheless, a growing number of publications reported EGFR mutant lung cancer in carriers of LFS suggesting a potential link between these two conditions [START_REF] Bemis | EGFR-mutant lung adenocarcinoma in a patient with Li-Fraumeni syndrome[END_REF][14] [15][16]. Table 1 recapitulates important characteristics of the previous cases reported as well as our two patients. Consistent with IARC database, the majorities of tumors arise before the fifth decade and occur predominantly in woman.

Interestingly, a majority of LFS patients harboring EGFR and/or ERBB2 mutated lung adenocarcinomas encompass good tumoral and clinical response to targeted therapy (except for the patient with T790M resistance mutation). The benefit appears to be quite similar than in non-LFS population with a progression-free survival of approximately one year. Some dedicated studies are needed to confirm this observation. As expected from clinical trials, A c c e p t e d M a n u s c r i p t rechallenge with EGFR-TKI after progression show no benefit in our second case, even in the absence of identified resistance mutation. Third generation TKI recently show promising antitumor activity, but current investigation are limited to the tumors with identified resistance mutation. Furthermore, we report for the first time acquisition of EGFR-TKI resistance mutation in the context of LFS. Familial cases of germline T790M may exist in 50% of these cases [START_REF] Oxnard | Screening for germline EGFR T790M mutations through lung cancer genotyping[END_REF].It was ruled out in our first patient because allele frequency was not consistent with this hypothesis (around 7%) and the mutation was not found in her daughter genome (data not shown). However, we cannot exclude that EGFR T790M mutation was not present at the time of diagnosis because reduced sample materials from hepatic needle-biopsy do not allow us to perform molecular biology. Still, these cases suggest a common natural history of resistance to TKI than in general population. In LFS patients, as the first genetic hit is inherited, we argue that a second-hit, according Knudson hypothesis, can arise sooner in the time course of tumorigenesis. Interestingly, some authors incriminate radiation therapy or chemotherapy as a second hit. Notably, five of six LFS cases with EGFR-mutated lung adenocarcinoma were previously treated with chemotherapy or radiotherapy in a context of mammary malignancies.

Even if a causative role remains to be demonstrated, benefice-risk assessment of radiotherapy should be carefully evaluated and discussed with patients in this particular setting.

In conclusion, thoracic oncologists should evoke LFS in the context of illegitimate lung cancer (young and non-smoker patients). EGFR mutation is frequently reported in the Li-Fraumeni setting, but epidemiological studies are needed to assess this potential association.

Response to targeted therapy seems to be similar as in the general population. Arguably, we show for the first time that same resistance mechanism could arise in the LFS context..

  A c c e p t e d M a n u s c r i p t Cases A fifty-five year old non-smoker man was diagnosed with a lower left leg deep venous thrombosis in December 2010. CT-scan evaluation revealed upper right lobe lung mass, abnormal mediastinal lymph nodes and two liver lesions. A liver biopsy confirmed the presence of a metastatic localization of a stage IV (T2a N3 M1b) lung adenocarcinoma.

  Symptomatic pleural effusion occurred and the patient clinically benefit from a re-challenge of platinum doublet chemotherapy. Approximately two years after diagnosis, CT-scan guided biopsy was performed on a new pulmonary nodule to assess tumoral molecular abnormality status and rule out transition to small cell lung cancer. The presence of an adenocarcinoma with both an EGFR exon 19 deletion (del2235-2249, delE745-A750) and an exon 20 T790M (c.2369C>T) mutation was confirmed respectively by automated electrophoresis system (LabChip GX) and pyrosequencing (figure1, panel A and B). A tumoral TP53 gene mutation was also found, similarly to the germline mutation previously described (data not shown). No mutation on HER2, PI3KCA, BRAF or KRAS genes or rearrangement of ALK gene was found. A fourth line of chemotherapy was proposed with an objective response observed after 4 cycles of carboplatin pemetrexed bevacizumab. The patient died a few months later from rapidly progressive pulmonary lymphangitic carcinomatosis (figure1, panel C).

  A c c e p t e d M a n u s c r i p t A fifty-seven year old woman presented with a two month history of inflammatory lumbar pain in November 2008. MRI evaluation revealed a body lesion of L1 suspect of malignant origin. Needle bone biopsy confirmed the presence of a secondary metastasis of an upper left lobe lung adenocarcinoma. It was a stage IV (T2aN2M1b) disease and ECOG performance status was quantified to 0 at diagnosis. She never smoked and presented right breast carcinoma in 2002, treated by surgery and radiation. EGFR status was unknown at diagnosis because bone sample conditioning does not allow us to perform molecular analysis. After two cycles of cisplatin vinorelbin, the disease progressed, therefore erlotinib was prescribed. This therapy resulted in a significant and prolonged response. In october 2009, she was tested for germline TP53 mutation because her daughter was diagnosed with corticosurrenaloma. LFS was confirmed (TP53 mutation R273H). Thoracic progression occurred in November 2011 and the patient was enrolled in a phase 1 study evaluating an irreversible EGFR-TKI inhibitor (afatinib). Pleural metastasis was diagnosed in March 2012 and the targeted therapy was stopped. A surgical pleurodesis showed pleural localization of an adenocarcinoma with EGFR exon 21 mutation L858R (c.2573T>G) without T790M mutation, as assess pyrosequencing (figure 1, panel D). No mutation on HER2, PI3KCA, BRAF or KRAS genes or rearrangement of ALK gene was found. Consequently, a re-challenge with erlotinib resulted in a 5 month stable disease. The patient died from respiratory failure because of multiple pulmonary metastasis, more than four years after initial diagnosis (figure 1, panel E).

  A c c e p t e d M a n u s c r i p tDiscussionWe report two LFS patients diagnosed with EGFR-mutated lung adenocarcinoma.

  , MK, HL and BD were responsible for the literature search. CR, MLT, MK and HL were responsible for figures. CR was responsible for data collection. CD, AL and JM were responsible for molecular biology data collection and analysis. All authors were responsible for data interpretation, and writing and final approval of the article. CR takes responsibility for the paper as a whole.

  Figure 1:

Figure 2 :

 2 Figure 2:

Table 1 :

 1 Clinical and biological characteristics of LFS patients diagnosed with EGFR-mutated lung adenocarcinoma. Obtained from case reports published in the literature. (CR: complete response, PR: partial response, PD: progressive disease)

  A c c e p t e d M a n u s c r

Acknowledgments:

We would like to thanks Dr. H. Symington for valuable comments and suggestions to improve the quality of the paper.

A c c e p t e d M a n u s c r i p t