Malgorzata Biernacka

Dariusz Biernacki

Sergueï Lenglet

Piotr Polesiuk

Damien Pous

Alan Schmitt

Małgorzata Biernacka

Fully Abstract Encodings of λ-Calculus in HOcore through Abstract Machines

come   L'archive ouverte pluridisciplinaire

I. INTRODUCTION

HOcore is a minimal process calculus with higher-order communication, meaning that messages are executable processes. It is a subcalculus of HOπ [START_REF] Sangiorgi | Bisimulation for higher-order process calculi[END_REF] with no construct to generate names or to restrict the scope of communication channels. Even with such a limited syntax, HOcore is Turing complete [START_REF] Lanese | On the expressiveness and decidability of higher-order process calculi[END_REF]. However, as a higher-order calculus, it is less expressive than the name passing π-calculus: polyadic message sending cannot be compositionally encoded in monadic message sending in HOπ [START_REF] Lanese | On the expressiveness of polyadic and synchronous communication in higher-order process calculi[END_REF], while it can be done in π [START_REF] Sangiorgi | The π-Calculus: A Theory of Mobile Processes[END_REF].

Although HOcore is Turing complete, we initially thought a fully abstract encoding of the λ-calculus into HOcore was impossible. Indeed, a λ-term potentially has an unbounded number of redexes. A straightforward encoding would use communication to emulate β-reduction, but since HOcore does not provide means to restrict the scope of communication, one would need as many distinct names as there are redexes to avoid interference. Moreover, as new redexes may be created by β-reduction, we also need a way to generate new names on which to communicate. To circumvent these problems and illustrate the expressiveness of HOcore, we consider encodings where the reduction strategy is fixed, thus for which at most one redex is enabled at any time. In this setting, β-reduction can be emulated using communication on a single, shared, name. A first contribution of this paper is a novel encoding of the call-by-name λ-calculus, or more precisely the Krivine Abstract Machine (KAM) [START_REF] Krivine | A call-by-name lambda-calculus machine[END_REF], into HOcore.

A faithful encoding not only reflects the operational semantics of a calculus, it should also reflect its equivalences. Ideally, an encoding is fully abstract: two source terms are behaviorally equivalent iff their translations are equivalent. On the HOcore side, we use barbed equivalence with hidden names [START_REF] Lanese | On the expressiveness and decidability of higher-order process calculi[END_REF], where a fixed number of names used for the translation cannot be observed. On the λ-calculus side, we consider three equivalences. First, we look at normal-form bisimilarity [START_REF] Lassen | Bisimulation in untyped lambda calculus: Böhm trees and bisimulation up to context[END_REF][START_REF] Lassen | Eager normal form bisimulation[END_REF], where normal forms are decomposed into subterms that must be bisimilar. Next, we turn to applicative bisimilarity [START_REF] Abramsky | Full abstraction in the lazy lambda calculus[END_REF], where normal forms must behave similarly when applied to identical arguments. And finally, we consider contextual equivalence, where terms must behave identically when put into arbitrary contexts. Our second contribution is an internalization of these equivalences into extended abstract machines: these machines expand the KAM, which performs the evaluation of a term, with additional transitions with flags interpreting the equivalences. By doing so, we can express these different equivalences on terms by a simpler bisimilarity on these flags-generating machines, which can be seen as labeled transition systems. Finally, and as third contribution, we translate these extended machines into HOcore and prove full abstraction for all three equivalences. Altogether, this work shows that a minimal process calculus with no name restriction can faithfully encode the call-by-name λ-calculus.

The chosen equivalences: One may wonder why we study normal-form and applicative bisimilarities, as faithfully encoding contextual equivalence is enough to get full abstraction. Our motivation is twofold. First, we start with normal-form bisimilarity because it is the simplest to translate. Indeed, there is no need to inject terms from the environment to establish the equivalence. We next show how we can inject terms for applicative bisimilarity, and we then extend this approach to contexts for contextual equivalence. Second, the study of quite different equivalences illustrate the robustness of the internalization technique.

Related work: Since Milner's seminal work [START_REF] Milner | Functions as processes[END_REF], other translations of the λ-calculus or one of its variants into π-calculus have been proposed, e.g., to study connections with logic [START_REF] Accattoli | Evaluating functions as processes[END_REF][START_REF] Beffara | Functions as proofs as processes[END_REF][START_REF] Toninho | Functions as session-typed processes[END_REF], termination [START_REF] Cimini | Functions as processes: Termination and the λµμ-calculus[END_REF][START_REF] Amadio | A decompilation of the pi-calculus and its application to termination[END_REF][START_REF] Yoshida | Strong normalisation in the pi -calculus[END_REF], sequentiality [START_REF] Berger | Sequentiality and the pi-calculus[END_REF], control [START_REF] Cimini | Functions as processes: Termination and the λµμ-calculus[END_REF][START_REF] Honda | Process types as a descriptive tool for interaction -control and the pi-calculus[END_REF][START_REF] Van Bakel | A fully-abstract semantics of lambdamu in the pi-calculus[END_REF], or Continuation-Passing Style (CPS) transforms [START_REF] Sangiorgi | From lambda to pi; or, rediscovering continuations[END_REF][START_REF] Sangiorgi | The π-Calculus: A Theory of Mobile Processes[END_REF][START_REF] Downen | Continuations, processes, and sharing[END_REF]. These works use the more expressive first-order π-calculus, except for [START_REF] Sangiorgi | From lambda to pi; or, rediscovering continuations[END_REF][START_REF] Sangiorgi | The π-Calculus: A Theory of Mobile Processes[END_REF], discussed below; full abstraction is proved w.r.t. contextual equivalence in [START_REF] Berger | Sequentiality and the pi-calculus[END_REF][START_REF] Yoshida | Strong normalisation in the pi -calculus[END_REF][START_REF] Honda | Process types as a descriptive tool for interaction -control and the pi-calculus[END_REF], normal-form bisimilarity in [START_REF] Van Bakel | A fully-abstract semantics of lambdamu in the pi-calculus[END_REF], and normalform and applicative bisimilarities in [START_REF] Sangiorgi | The π-Calculus: A Theory of Mobile Processes[END_REF]. The definitions of the encodings and the equivalences of [START_REF] Berger | Sequentiality and the pi-calculus[END_REF][START_REF] Yoshida | Strong normalisation in the pi -calculus[END_REF][START_REF] Honda | Process types as a descriptive tool for interaction -control and the pi-calculus[END_REF] are driven by types, and therefore cannot be compared to our untyped setting. In [START_REF] Van Bakel | A fully-abstract semantics of lambdamu in the pi-calculus[END_REF], van Bakel et al. establish a full abstraction result between the λµ-calculus with normal-form bisimilarity and the π-calculus. Their encoding relies on an unbounded number of restricted names to evaluate several translations of λ-terms in parallel, while we rely on flags and on barbed equivalence to know which translated λ-term is being evaluated. We explain the differences between the two approaches in Section IV-B.

Sangiorgi translates the λ-calculus into a higher-order calculus as an intermediary step in [START_REF] Sangiorgi | From lambda to pi; or, rediscovering continuations[END_REF][START_REF] Sangiorgi | The π-Calculus: A Theory of Mobile Processes[END_REF], but it is an abstractionpassing calculus, which is strictly more expressive than a process-passing calculus [START_REF] Lanese | On the expressiveness of polyadic and synchronous communication in higher-order process calculi[END_REF]. Like in our work, Sangiorgi fixes the evaluation strategy in the λ-calculus, except that he uses CPS translations rather than abstract machines. In the light of Danvy et al.'s functional correspondence [START_REF] Ager | A functional correspondence between evaluators and abstract machines[END_REF], the two approaches appear closely related, however it is difficult to compare our encoding with Sangiorgi's, since we use different target calculi, and we internalize the normalform and applicative bisimilarities in the abstract machines. Still, name restriction plays an important role in Sangiorgi's encodings, since a local channel is used for each application in a λ-term. Full abstraction w.r.t. normal-form bisimilarity (called "applicative open bisimilarity") is established in [START_REF] Sangiorgi | The π-Calculus: A Theory of Mobile Processes[END_REF]Chapter 18]. In [START_REF] Sangiorgi | The π-Calculus: A Theory of Mobile Processes[END_REF]Chapter 17], the encoding is proved to be sound but not complete w.r.t. applicative bisimilarity: there exist applicative bisimilar λ-terms whose translations are not bisimilar in π-calculus. It is then argued that completeness can be achieved for this encoding only by extending the λ-calculus with non-confluent constructs. We explain the discrepancy with our results in Remark 24.

Outline: Section II presents the syntax and semantics of HOcore. Section III shows how to encode the KAM; the machine and its encoding are then modified to get full abstraction with relation to normal-form bisimilarity (Section IV) and applicative bisimilarity (Section V). Section VI concludes this paper, and the appendix contains the main proofs.

II. THE CALCULUS HOCORE

Syntax and semantics: HOcore [START_REF] Lanese | On the expressiveness and decidability of higher-order process calculi[END_REF] is a simpler version of HOπ [START_REF] Sangiorgi | Bisimulation for higher-order process calculi[END_REF] where name restriction is removed. We let a, b, etc. range over channel names, and x, y, etc. range over process variables. The syntax of HOcore processes is: P, Q ∶∶= a(x).P a⟨P ⟩ P ∥ Q x 0. The process a(x).P is waiting for a message on a which, when received, is substituted for the variable x in P . If x does not occur in P , then we write a( ).P . The process a⟨P ⟩ is sending a message on a. Note that communication is higher order-processes are sent-and asynchronous-there is no continuation after a message output. The parallel composition of processes is written P ∥ Q, and the process 0 cannot perform any action. Input has a higher precedence than parallel composition, e.g., we write a(x).P ∥ Q for (a(x).P ) ∥ Q. We implicitly consider that parallel composition is associative, commutative, and has 0 as a neutral element. In an input a(x).P , the variable x is bound in P . We write fn(P ) for the channel names of P .

Informally, when an output a⟨P ⟩ is in parallel with an input a(x).Q, a communication on a takes place, producing [P x]Q, the capture avoiding substitution of x by P in Q. We define in Figure 1 the semantics of HOcore as a labeled transition system (LTS), omitting the rules symmetric to PAR and TAU. The labels (ranged over by l) are either τ for internal communication, a⟨P ⟩ for message output, or a(P ) for process input. We use label a for an input where the received process does not matter (e.g., a( ).P ).

Weak transitions allow for internal actions before and after a visible one. We write τ ⇒ for the reflexive and transitive closure τ → * , and

l ⇒ for τ ⇒ l → τ ⇒ when l ≠ τ . OUT a⟨P ⟩ a⟨P ⟩ → 0 INP a(x).Q a(P ) → [P x]Q PAR P l → P ′ P ∥ Q l → P ′ ∥ Q TAU P a⟨R⟩ → P ′ Q a(R) → Q ′ P ∥ Q τ → P ′ ∥ Q ′
a(Q) → R (resp. P a⟨Q⟩ → R) for some Q, R.
A process P has a weak observable action on γ, written P ⇓ γ , if P τ ⇒ P ′ ↓ γ for some P ′ . We write WkObs(P ) for the set of weak observable actions of P .

Our definition of barbed equivalence depends on a set H of hidden names, which allows some observable actions to be ignored. Instead of adding top-level name restrictions on these names, as in [START_REF] Lanese | On the expressiveness and decidability of higher-order process calculi[END_REF], we prefer to preserve the semantics of the calculus and simply hide some names in the equivalence. Hidden names are not a computational construct and are not required for the encoding of the KAM, but they are necessary to protect the encoding from an arbitrary environment when proving full abstraction. We emphasize that we do not need the full power of name restriction: the set of hidden names is finite and static-there is no way to create new hidden names.

Definition 2. A symmetric relation R is a barbed bisimulation w.r.t. H if P R Q implies • P ↓ γ and γ ∉ H implies Q ⇓ γ ;
• for all R such that fn(R) ∩ H = ∅, we have P ∥R R Q∥R;

• if P τ → P ′ , then there exists Q ′ such that Q τ ⇒ Q ′ and P ′ R Q ′ . Barbed equivalence w.r.t. H, noted ≈ H
HO , is the largest barbed bisimulation w.r.t. H.

A strong barbed equivalence can be defined by replacing ⇓ γ with ↓ γ in the first item, and τ ⇒ with τ → in the third. From [START_REF] Lanese | On the expressiveness and decidability of higher-order process calculi[END_REF], we know that strong barbed equivalence is decidable when H = ∅, but undecidable when H is of cardinal at least 4. We lower this bound to 2 in Theorem 4.

III. ENCODING THE KRIVINE ABSTRACT MACHINE

We show in this section that HOcore may faithfully encode a call-by-name λ-calculus through an operationally equivalent encoding of the KAM.

A. Definition of the KAM

The KAM [START_REF] Krivine | A call-by-name lambda-calculus machine[END_REF] is a machine for call-by-name evaluation of closed λ-calculus terms. We present a substitution-based variant of the KAM for simplicity, and to reuse the substitution of HOcore in the translation. A configuration C of the machine is composed of the term t being evaluated, and a stack π of λ-terms. Their syntax and the transitions are as follows.

C ∶∶= t ⋆ π (configurations) t, s ∶∶= x t t λx.t (terms) π ∶∶= t ∶∶ π [] (stacks) t s ⋆ π ↦ t ⋆ s ∶∶ π (PUSH) λx.t ⋆ s ∶∶ π ↦ [s x]t ⋆ π (GRAB) A λ-

B. Translation into HOcore

The translation of the KAM depends essentially on how we push and grab terms on the stack. We represent the stack by two messages, one on name hd c for its head, and one on name c (for continuation) for its tail (henceforth, a stack n is always encoded as a message on hd n for its head and one on n for its tail). The empty stack can be represented by an arbitrary, non-diverging, deterministic process, e.g., 0; here we use a third name to signal that the computation is finished with b⟨0⟩. As an example, the stack

1 ∶∶ 2 ∶∶ 3 ∶∶ 4 ∶∶ [] is represented by hd c ⟨1⟩ ∥ c⟨hd c ⟨2⟩ ∥ c⟨hd c ⟨3⟩ ∥ c⟨hd c ⟨4⟩ ∥ c⟨b⟨0⟩⟩⟩⟩⟩.
With this representation, pushing an element e on a stack p is done by creating the process hd c ⟨e⟩ ∥ c⟨p⟩, while grabbing the head of the stack corresponds to receiving on hd c . With this idea in mind, we define the translations for the stacks, terms, and configurations as follows, where we assume the variable p does not occur in the translated entities.

vt ⋆ πw ▵ = vtw ∥ c⟨vπw⟩ v[]w ▵ = b⟨0⟩ vt ∶∶ πw ▵ = hd c ⟨vtw⟩ ∥ c⟨vπw⟩ vt sw ▵ = c(p). vtw ∥ c⟨hd c ⟨vsw⟩ ∥ c⟨p⟩⟩ vλx.tw ▵ = c(p).(hd c (x). vtw ∥ p) vxw ▵ = x
In the translation of a configuration t ⋆ π, the stack is in a message on c, meaning that before pushing on π or grabbing the head of π, we have to get vπw by receiving on c. For instance, in the application case vt sw, we start by receiving the current stack p on c, and we then run vtw in parallel with the translation of the new stack hd c ⟨vsw⟩ ∥ c⟨p⟩. Similarly, in the λ-abstraction case vλx.tw, we get the current stack p on c, that we run in parallel with hd c (x). vtw. If p is not empty, then it is a process of the form hd c ⟨vsw⟩ ∥ c⟨vπw⟩, and a communication on hd c is possible, realizing the substitution of x by s in t; the execution then continues with v[s x]tw ∥ c⟨vπw⟩. Otherwise, p is b⟨0⟩, and the computation terminates.

Formally, the operational correspondence between the KAM and its translation is as follows.

Theorem 3. In the forward direction, if C ↦ * C ′ , then vCw τ ⇒ vC ′ w. In the backward direction, if vCw τ ⇒ P , then there exists a C ′ such that C ↦ * C ′ and either

• P = vC ′ w,
• or there exists P ′ such that P τ → P ′ = vC ′ w,

• or C ′ = λx.t ⋆ [] and P = hd c (x). vtw ∥ b⟨0⟩. Sketch. The proof is straightforward in the forward direction. In the backward direction, we show that the translation is deterministic (if

vCw τ ⇒ P τ → Q 1 and vCw τ ⇒ P τ → Q 2 , then Q 1 = Q 2 )
and we rely on the fact that the translation of a PUSH step uses one communication, while we use two communications for a GRAB step.

We can then improve over the result of [START_REF] Lanese | On the expressiveness and decidability of higher-order process calculi[END_REF] about undecidability of strong barbed equivalence by hiding hd c and c. Theorem 4. Strong barbed equivalence is undecidable in HOcore with 2 hidden names.

Proof. Assume we can decide strong barbed congruence with two hidden names, and let t be a closed λ-term. We can thus decide if vt ⋆ []w is strong barbed-congruent to c(x).( x ∥ c⟨x⟩ ) ∥ c⟨c(x).(x ∥ c⟨x⟩)⟩ when hd c and c are hidden. As the second term loops with no barbs, deciding congruence is equivalent to deciding whether the reduction of t converges, hence a contradiction.

IV. NORMAL-FORM BISIMILARITY

Our first full abstraction result is for normal-form bisimilarity [START_REF] Lassen | Bisimulation in untyped lambda calculus: Böhm trees and bisimulation up to context[END_REF]. We show how to internalize this equivalence in an extension of the KAM such that it may be captured by a simple barbed bisimilarity. We then translate this extended KAM into HOcore, and we finally prove full abstraction.

A. Normal-Form Bisimilarity

Normal-form bisimilarity compares terms by reducing them to weak head normal forms, if they converge, and then decomposes these normal forms into subterms that must be bisimilar. Unlike the KAM, normal-form bisimilarity is defined on open terms, thus we distinguish free variables, ranged over by α, from bound variables, ranged over by x. The grammars of terms (t, s) and values (v) become as follows.

t ∶∶= α x λx.t t t v ∶∶= α λx.t

Henceforth, we assume that λ-terms are well formed, i.e., all variables ranged over by x are bound: x is not a valid term but α is. We write fv(t) for the set of free variables of t. A variable α is said fresh if it does not occur in any entities under consideration.

When evaluating an open term, we can obtain either a λabstraction, or a free variable in a stack. We inductively extend a relation R on λ-terms to stacks by writing π R π

′ if π = π ′ = [], or if π 1 = t ∶∶ π ′ 1 , π 2 = s ∶∶ π ′ 2 , t R s, and π ′ 1 R π ′ 2 .
Definition 5. A symmetric relation R is a normal-form bisimulation if t R s implies:

• if t⋆[] ↦ * λx.t ′ ⋆[], then there exists s ′ such that s⋆[] ↦ * λx.s ′ ⋆ [] and [α x]t ′ R [α x]s ′ for a fresh α; • if t ⋆ [] ↦ * α ⋆ π, then there exists π ′ such that s ⋆ [] ↦ * α ⋆ π ′ and π R π ′ . Normal-form bisimilarity ≈ nf is the largest normal-form bisim- ulation.
Normal-form bisimilarity is not complete w.r.t. contextual equivalence in λ-calculus, but it characterizes Lévy-Longo tree equivalence [START_REF] Lassen | Bisimulation in untyped lambda calculus: Böhm trees and bisimulation up to context[END_REF].

B. Abstract Machine

We now describe how to extend the KAM so that it provides additional steps, identified by labeled transitions, that capture normal-form bisimilarity. These extended machines feature flagged transitions, terminating transitions, and a restricted form of non-determinism. Flagged transitions are usual transitions of the machine with some additional information to convey to the environment that a particular event is taking place. Machine bisimilarity, defined below, ensures that bisimilar machines have matching flags. Transitions without flags use a τ label. Terminating transitions are flagged transitions that indicate the computation has stopped. They are needed for bisimilarity: as machine bisimilarity ignores τ labels, we use terminating transitions to distinguish between terminated and divergent machine runs. Finally, we allow non-determinism in machines, i.e., a given configuration may take two different transitions, only if the transitions are flagged and have different flags. In other words, the non-deterministic choice is made explicit to the environment.

We define the NFB machine in Figure 2. When computation stops with a λ-abstraction and an empty stack, we have to restart the machine to evaluate the body of the abstraction with a freshly generated free variable (rule LAMBDA). To do so, we consider free variables as natural numbers, and we keep a counter n in the machine which is incremented each time a fresh variable is needed. For a configuration α ⋆ π, normal-form bisimilarity evaluates each of the t i in the stack (rule VAR). To internalize this step, we could launch several machines in parallel, as in [START_REF] Van Bakel | A fully-abstract semantics of lambdamu in the pi-calculus[END_REF], where the translated t i are run in parallel. This approach has two drawbacks: first, it is a further extension of abstract machines (a machine no longer steps to a single machine state but to a multiset of states). Second, when translating such extended machines into HOcore, we want to prevent them from interacting with each other, but we cannot rely on name restriction, as in [START_REF] Van Bakel | A fully-abstract semantics of lambdamu in the pi-calculus[END_REF], to encapsulate an unbounded number of translations. Alternatively, one could evaluate the elements of the stack sequentially, but this approach fails if one of the elements of the stack diverges, as the later elements will never be evaluated. We thus consider a third approach, built upon flagged non-determinism: the machine chooses arbitrarily an element of the stack to evaluate, and signals this choice using flags (rules ENTER, SKIP, and DONE). The burden of evaluating every element of the stack is thus relegated to the definition of machine bisimilarity: as

⟨t s, π, n⟩ ev τ Þ → ⟨t, s ∶∶ π, n⟩ ev (PUSH) ⟨λx.t, s ∶∶ π, n⟩ ev τ Þ → ⟨[s x]t, π, n⟩ ev (GRAB) ⟨λx.t, [], n⟩ ev ⊚ Þ → ⟨[n x]t, [], n + 1⟩ ev (LAMBDA) ⟨α, π, n⟩ ev α Þ → ⟨π, n⟩ ct (VAR) ⟨[], n⟩ ct Þ → (DONE) ⟨t ∶∶ π, n⟩ ct ▼ Þ → ⟨t, [], n⟩ ev (ENTER) ⟨t ∶∶ π, n⟩ ct ▶ Þ → ⟨π, n⟩ ct (SKIP)
Fig. 2: NFB Machine every flagged execution must be matched by an execution with the same flags, every possible choice is explored.

As before, we use C to range over configurations, which are now of two kinds. In evaluation mode, ⟨t, π, n⟩ ev is reducing t within stack π and with counter n. The transitions PUSH and GRAB are as in the KAM, except for the extra parameter. If we reach a λ-abstraction in the empty context (transition LAMBDA), then the machine flags ⊚ and then restarts to evaluate the body, replacing the bound variable by a fresh free variable, i.e., the current value n of the counter. If we reach a free variable α, i.e., a number, then we flag the value of α before entering the next mode (transition VAR).

In continuation mode ⟨π, n⟩ ct , the transition DONE simply finishes the execution if π = [], using the flag . Otherwise, π = t ∶∶ π ′ , and the machine either evaluates t with flag ▼ (and forgets about π ′ ), or skips t with a flag ▶ to eventually evaluate a term in π ′ . The machine may skip the evaluation of all the terms in π, but it would still provide some information, as it would generate m ▶ messages (followed by ), telling us that π has m elements. Note that the counter n is stored in continuation mode just to be passed to the evaluation mode when one of the t i is chosen with transition ENTER. Example 6. To illustrate how the machine works, we show the transitions starting from the term (λx.x) (λy.y 0 Ω), where Ω ▵ = (λx.x x) (λx.x x). The term is executed in the empty context, and with a counter initialized to a value greater than its free variables.

⟨(λx.x) (λy.y 0 Ω), [], 1⟩ ev τ Þ → ⟨λx.x, λy.y 0 Ω ∶∶ [], 1⟩ ev (PUSH) τ Þ → ⟨λy.y 0 Ω, [], 1⟩ ev (GRAB) ⊚ Þ → ⟨1 0 Ω, [], 2⟩ ev (LAMBDA) τ Þ → ⟨1 0, Ω ∶∶ [], 2⟩ ev τ Þ → ⟨1, 0 ∶∶ Ω ∶∶ [], 2⟩ ev (PUSH -PUSH) 1 Þ → ⟨0 ∶∶ Ω ∶∶ [], 2⟩ ct (VAR)
We then have three possibilities. First, we reduce the top of the stack, with the sequence

⟨0 ∶∶ Ω ∶∶ [], 2⟩ ct ▼ Þ → ⟨0, [], 2⟩ ev 0 Þ → ⟨[], 2⟩ ct Þ →. Second, we evaluate Ω with the sequence ⟨0 ∶∶ Ω ∶∶ [], 2⟩ ct ▶ Þ → ⟨Ω ∶∶ [], 2⟩ ct ▼ Þ → ⟨Ω, [],
2⟩ ev , and then the machine loops without generating any flag. Third, we skip both terms with

⟨0 ∶∶ Ω ∶∶ [], 2⟩ ct ▶ Þ → ⟨Ω ∶∶ [], 2⟩ ct ▶ Þ → ⟨[], 2⟩ ct Þ → .
Note that the three options generate different traces of flags.

Because the rules GRAB and PUSH are the same between the KAM and the NFB machine, there is a direct correspondence between the two.

Lemma 7. For all t, t ′ , π, π ′ , n, t⋆π ↦ t ′ ⋆π ′ iff ⟨t, π, n⟩ ev τ Þ → ⟨t ′ , π ′ , n⟩ ev .
We finally show that a notion of bisimilarity between configurations of an NFB machine captures normal-form bisimilarity.

To this end, we first define machine bisimilarity, where we denote the flags of the machine by f .

Definition 8. A symmetric relation R is a machine bisimula- tion if C 1 R C 2 implies: • if C 1 τ Þ → * f Þ → C ′ 1 , then there exists C ′ 2 such that C 2 τ Þ → * f Þ → C ′ 2 and C ′ 1 R C ′ 2 ; • if C 1 τ Þ → * f Þ →, then C 2 τ Þ → * f Þ →.
Machine bisimilarity ≈ m is the largest machine bisimulation.

Intuitively, machine bisimilarity ensures that every flag emitted by a machine is matched by an identical flag from the other machine, up to internal reductions. Note that a machine that diverges with τ labels can be related to any other diverging machine or any machine stuck without a flag. We make sure the latter case cannot occur in our machines by only having terminating transitions, which are flagged, as stuck transitions. We can now state that normal-form bisimilarity coincides with machine bisimilarity of NFB machines.

) t ≈ nf s, n > max (fv(t), fv(s))} ∪{(⟨π, n⟩ ct , ⟨π ′ , n⟩ ct ) π ≈ nf π ′ , n > max (fv(π), fv(π ′ ))}
is a machine bisimulation.

C. Translation into HOcore

In Figure 3, we present the translation of the NFB machine into HOcore, where we consider flags as channel names. Configurations now contain a counter n, which is represented by a message on k containing the value of n encoded as a process. We use v.w Int to translate a natural number n into a process suc( ). . . . suc( ) n times .z( ).init⟨0⟩; the role of the final output on init is explained later. Free variables α are also numbers, since we cannot generate new names in HOcore, and we use the same translation for them. We also use non-deterministic internal choice, encoded as follows:

P + Q ▵ = ch⟨P ⟩ ∥ ch⟨Q⟩ ∥ ch(x)
.ch( ).x: both messages are consumed, and only one process is executed. This encoding supposes that at most one choice is active at a given time, as we use only one name ch to encode all the choices. We also use n-ary choices for n > 2 in Section V-C, which can be encoded in the same way. A stack is represented as in the KAM, by messages on hd c and c, and the translation of an application vt sw is exactly the same as for the KAM. The encoding of the empty context [] is different, however, because contexts are used to distinguish between execution paths at two points in the machine: when evaluating a function λx.t in evaluation mode, and when deciding whether the execution is finished in continuation mode. The empty context is thus encoded as b(x).x, waiting to receive the process to execute in the empty case. For the non-empty case, this input on b is absent and there are instead messages on hd c and c. Thus the generic way to choose a branch is as follows: b⟨do this if empty⟩ ∥ hd c (x).c(y).b( ).do this if non-empty.

vt sw ▵ = c(p). vtw ∥ c⟨hd c ⟨vsw⟩ ∥ c⟨p⟩⟩ vλx.tw ▵ = c(p).(p ∥ b⟨Restart⟩ ∥ hd c (x).b( ). vtw) vxw ▵ = x vαw ▵ = vαw Int Restart ▵ = ⊚( ).k(x). ⎛ ⎝ hd c ⟨x⟩ ∥ k⟨suc( ).x⟩ ∥ c⟨v[]w⟩ ∥ b⟨0⟩ ⎞ ⎠ Rec ▵ = init( ).rec(x).(x ∥ rec⟨x⟩ ∥ Cont) Cont ▵ = c(p).(p ∥ b⟨ ( ).0⟩ ∥ hd c (x).b( ).Chce(x)) Chce(P t ) ▵ = ▼( ).c( ).(P t ∥ c⟨v[]w⟩) + ▶( ).init⟨0⟩ v[]w ▵ = b(x).x vt ∶∶ πw ▵ = hd c ⟨vtw⟩ ∥ c⟨vπw⟩ v0w Int ▵ = z( ).init⟨0⟩ vn + 1w Int ▵ = suc( ). vnw Int v⟨t, π, n⟩ ev w ▵ = vtw ∥ c⟨vπw⟩ ∥ k⟨vnw Int ⟩ ∥ Rec ∥ rec⟨Rec⟩ v⟨π, n⟩ ct w ▵ = c⟨vπw⟩ ∥ k⟨vnw Int ⟩ ∥ Cont ∥ Rec ∥ rec⟨Rec⟩
In the non-empty case, the input on b discards the message for the empty behavior that was not used.

For λ-abstractions, the behavior for the empty case is described in the process Restart. More precisely, vλx.tw receives the current stack vπw on c to run it in parallel with b⟨Restart⟩ ∥ hd c (x).b( ). vtw. If vπw is of the form hd c ⟨vt ′ w⟩ ∥ c⟨vπ ′ w⟩, then we have the same behavior as with the KAM, with an extra communication on b to garbage collect the Restart process. Otherwise, vπw = b(x).x and we obtain the following sequence of transitions.

b(x).x ∥ b⟨Restart⟩ ∥ hd c (x).b( ). vtw ∥ k⟨vnw Int ⟩ τ → ⊚( ).k(x).(hd c ⟨x⟩ ∥ k⟨suc( ).x⟩ ∥ c⟨v[]w⟩ ∥ b⟨0⟩) ∥ hd c (x).b( ). vtw ∥ k⟨vnw Int ⟩ ⊚ ⇒ hd c ⟨vnw Int ⟩ ∥ k⟨suc( ). vnw Int ⟩ ∥ c⟨v[]w⟩ ∥ b⟨0⟩ ∥ hd c (x).b( ). vtw τ → k⟨suc( ). vnw Int ⟩ ∥ c⟨v[]w⟩ ∥ b⟨0⟩ ∥ b( ). v[n x]tw τ → k⟨vn + 1w Int ⟩ ∥ c⟨v[]w⟩ ∥ v[n x]tw
In the end, we have effectively restarted the machine to evaluate [n x]t, as wished.

In continuation mode, the branching is done by the process Cont, which is executed after applying the transition VAR. More precisely, a free variable α is translated using v.w Int , which signals first the value of α (with the names suc and z), and then sends a message on init to enter the continuation mode. The way the NFB machine chooses which t i to evaluate in a stack t 1 ∶∶ . . . ∶∶ t m ∶∶ [] is a recursive mechanism, and recursion can be encoded in a higher-order calculus: Rec ∥ rec⟨Rec⟩ reduces to Cont ∥ Rec ∥ rec⟨Rec⟩ when it receives a message on init. The process Cont is doing a case analysis on vπw when it is executed in parallel with c⟨vπw⟩:

if π = [],
then vπw = b(x).x receives the message on b which flags and the machine stops. Otherwise, vπw = hd c ⟨vtw⟩ ∥ c⟨vπ ′ w⟩, and we have the following reductions:

Cont ∥ c⟨vπw⟩ τ → hd c ⟨vtw⟩ ∥ c⟨vπ ′ w⟩ ∥ b⟨ ( ).0⟩ ∥ hd c (x).b( ).Chce(x) τ → 2 c⟨vπ ′ w⟩ ∥ Chce(vtw)
At this point, Chce(vtw) either evaluates t with flag ▼, or flags ▶ and continues exploring π ′ . In the former case, the current stack π ′ is replaced by an empty stack, and in the latter, a message on init is issued to produce Cont ∥ c⟨vπ ′ w⟩ after some reduction steps.

D. Operational Correspondence and Full Abstraction

Establishing full abstraction requires first to state the correspondence between the NFB machine and its translation. In what follows, we let f range over the flags ⊚, ▼, ▶, , and α, where α is used as a shorthand for the succession of α suc flags followed by a z flag. We let f range over flags and τ . Definition 10. A process P is a machine process if there exists a configuration C of the machine such that vCw τ ⇒ P .

To establish the correspondence between the machine and its translation, we first define a predicate next( f , P ) such that, if Q ∈ next( f , P ), then there is a weak reduction with a step f from P to Q, Q is the translation of a machine, and there is no machine translation in between. Intuitively, it is the first translation reachable after a step f . Definition 11. We write

Q ∈ next( f , P ) if P τ ⇒ f → τ ⇒ Q, Q = vC ′
w for some C ′ , and for any P ′ such that P ′ ≠ P ,

P ′ ≠ Q, and P f ⇒ P ′ τ ⇒ Q or P τ ⇒ P ′ f ⇒ Q, we have P ′ ≠ vCw for any C.
A machine process is either a translation of a configuration, or an intermediary state between two translations; next( f , P ) gives the set of next processes which are translations. We now prove that, with a single exception, the translation is deterministic. The exception to determinism corresponds to the choice made in continuation mode, which is also not deterministic (but flagged) in the machine. We call choice process a process about to make that choice; such processes are of the form Chce(P t , P π , P n )

▵ = Chce(P t ) ∥ c⟨P π ⟩ ∥ k⟨P n ⟩ ∥ Rec ∥ rec⟨Rec⟩.
Lemma 12. Let P be a machine process which is not a choice process. If P f → P ′ and P f → P ′′ , then P ′ = P ′′ . Let P be a choice process. If P τ → P ′ , P τ → P ′′ , and WkObs(P ′ ) = WkObs(P ′′ ), then P ′ = P ′′ .

The choice process Chce(P t , P π , P n ) may only reduce to the translation of a configuration after a flag ▶ or ▼. Thus next(τ, Chce(P t , P π , P n )) is empty, and Lemma 12 implies that next( f , P ) is a singleton if it is not empty. In the following, we write next( f , P ) to assert that it is not empty and to directly denote the corresponding unique machine translation.

We can now state the correspondence between the NFB machine and its translation.

Lemma 13. The following assertions hold:

• C f Þ → C ′ iff vCw f ⇒ vC ′ w and next( f , vCw) = vC ′ w. • C Þ → iff vCw τ ⇒ → P and P ≈ HO 0.
With this result, we can relate the bisimilarities of each calculus. Henceforth, we write ≈ HO for ≈ H HO where H contains the names of the translation that are not flags. Given a flag f ≠ α, we write f for the process f ⟨0⟩. We also write α for the process complementing α, defined as n + 1

▵ = suc⟨0⟩ ∥ n and 0 ▵ = z⟨0⟩. Theorem 14. C ≈ m C ′ iff vCw ≈ HO vC ′ w.
Sketch. To prove that barbed equivalence implies machine equivalence, we show that

R ▵ = {(C, C ′ ) vCw ≈ HO vC ′ w} is a machine bisimulation. Let C 1 R C ′ 1 , so that C 1 τ Þ → * C 2 f Þ → C 3 ; then vC 1 w ∥ f τ ⇒ vC 2 w ∥ f τ ⇒ vC 3 w by
Lemma 13, which in turn implies that there exists P such that vC ′ 1 w ∥ f τ ⇒ P and vC 3 w ≈ HO P . In particular, we have WkObs(vC 3 w) = WkObs(P ), meaning that ¬(P ↓ f ).

Consequently, there exists P ′ such that vC ′ 1 w τ ⇒ P ′ and P ′ ↓ f . We can prove that P ≈ HO next(f, P ′ ), but by definition of next, there exists C ′ 3 so that next(f, P ′ ) = vC ′ 3 w. As a result, we have vC 3 w ≈ HO P ≈ HO vC ′ 3 w, i.e., C 3 R C ′ 3 , and

vC ′ 1 w f ⇒ vC ′ 3 w, which implies C ′ 1 τ Þ → * f Þ → C ′ 3 , as wished. The case C 1 τ Þ → * C 2 Þ → is similar.
For the reverse implication, we prove that

R ▵ = ⎧ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎨ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎩ (P C ∥ R, P C ′ ∥ R) C ≈ m C ′ , WkObs(P C ) = WkObs(P C ′ ) P C τ ⇒ vCw , P C ′ τ ⇒ vC ′ w or vCw τ ⇒ P C , vC ′ w τ ⇒ P C ′ , ⎫ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎬ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎭ ∪ {(P ∥ R, P ′ ∥ R) P ≈ HO 0 ≈ HO P ′ }
is a barbed bisimulation. The difficult part is to check that P C ∥ R τ → P ′ with a communication on a flag f is matched by P C ′ ∥ R. We have P C ↓ f , which implies that P C cannot reduce: a machine process is either reducing or has an observable action. We are therefore in the case vCw τ ⇒ P C , and R ↓ f . Suppose f ≠ ; then

P C f → P C2 τ ⇒ vC 2 w
for some P C2 and with vC 2 w = next(f, P C ). Because a machine process is deterministic (Lemma 12), then in fact

P ′ = P C2 ∥ R ′ for some R ′ . We have vCw f ⇒ vC 2 w, so C τ Þ → * f Þ → C 2 holds by Lemma 13. Because C ≈ m C ′ , there exists C ′ 2 such that C ′ τ Þ → * f Þ → C ′ 2 and C 2 ≈ m C ′ 2 . By Lemma 13, this implies vC ′ w f ⇒ vC ′ 2 w; in particular, there exists P C ′ 2 such that vC ′ w τ ⇒ f → P C ′ 2 τ ⇒ vC ′ 2 w. By Lemma 12, we have P C ′ τ ⇒ f → P C ′ 2 , therefore we have P C ′ ∥ R τ ⇒ P C ′ 2 ∥ R ′ , with P C2 ∥ R ′ R P C ′ 2 ∥ R ′ ,
as wished. In the case f = , we show that we obtain processes in the second set of R.

As a result, we can deduce full abstraction between HOcore and the λ-calculus with normal-form bisimilarity.

Corollary 15. We have t ≈ nf s iff there exists n > max (fv(t) ∪ fv(s)) such that v⟨t, [], n⟩ ev w ≈ HO v⟨s, [], n⟩ ev w.

Proof. By Theorems 9 and 14.

V. APPLICATIVE BISIMILARITY

Proving full abstraction w.r.t. normal-form bisimilarity requires minimal interactions-synchronizations on flagsbetween a machine process and the outside. Achieving full abstraction w.r.t. applicative bisimilarity is intuitively more difficult, since this bisimilarity tests λ-abstractions by applying them to an arbitrary argument. Internalizing such bisimilarity is simple using higher-order flags: one may think of the following transition to test the result of a computation:

λx.t ⋆ [] s Þ → [s x]t ⋆ []
Although HOcore has higher-order communications, we cannot use them to obtain a fully abstract encoding of such a machine for two reasons. First, allowing interactions where the environment provides a term may allow arbitrary processes to be received, including processes that are not in the image of the translation, thus potentially breaking invariants of the translation. Second, the translation of the KAM has to hide the names it uses for the translation to be fully abstract; it is thus impossible for the context to use such names and to provide translated λ-terms to be tested.

We thus propose in this section to internalize applicative bisimilarity using ordinary flags: when the abstract machine reaches a value, it switches to a different mode where it nondeterministically builds a test term step by step, using flags to indicate its choices so as to ensure that a bisimilar machine builds the same term. The translation of such a machine into HOcore is then similar to the translation of the NFB machine.

Using simple flags to generate terms step by step implies we need to deal with binders. In particular, and anticipating on the HOcore translation, we no longer can rely on the definition of binding and substitution from HOcore, as we cannot write a process that inputs a translation of t and outputs a translation of λx.t using an HOcore binding for x. We thus switch to a pure data description of bindings, using de Bruijn indices. As such terms still need to be executed, we first recall the definition of the KAM with de Bruijn indices and the definitions of contextual equivalence and applicative bisimilarity for λ-terms with de Bruijn indices. We then present the machine internalizing applicative bisimilarity, its translation into HOcore, and show they are fully abstract. We finally conclude this section by showing how contextual equivalence is internalized in an abstract machine, generating contexts instead of terms.

A. The KAM and Behavioral Equivalences

In the λ-calculus with de Bruijn indices, a variable is a natural number, which indicates which encompassing λ is its binder. For example, λx.x is written λ.0 and λxy.x y is written λ.λ. Applicative bisimilarity ≈ app is the largest applicative bisimulation.

We can prove full abstraction between HOcore and the λ-calculus by either internalizing contextual equivalence or applicative bisimilarity. We choose the latter, as it is closer to normal-form bisimilarity, and we show in Section V-D the machine for contextual equivalence.

B. Argument Generation for the Applicative Bisimilarity

After evaluating a term thanks to the KAM, we want to produce a closed argument to pass it to the resulting value, and then restart the evaluation process. If we represent a λterm as a syntax tree, then de Bruijn indices are at the leaves, and applications and λ-abstractions at the nodes. We start generating from the leftmost de Bruijn index, and we then go left to right, meaning that in an application, we create the term in function position before the argument. These choices are completely arbitrary, as doing the opposite-starting from the rightmost index and go right to left-is also possible. To be sure that we produce a valid, closed, λ-term, we have to check that each de Bruijn index n has at least n + 1 λ-abstractions enclosing it, and that each application node has two children.

To do so, we consider machine states with four components: the term t being constructed, a counter κ giving the minimal number of λ-abstractions required to close the term, a stack ρ used to build applications, whose syntax is ρ ∶∶= (t, κ) ∶∶ ρ ⊙ and which is explained in more detail later, and finally the closure η for which the argument is being built. This last element is never modified by the building process, and is just used to restart the machine in evaluation mode when the argument is finished. We distinguish two kinds of states: the index state ⟨n, κ, ρ, η⟩ ind , where only de Bruijn indices can be built, and the term state ⟨t, κ, ρ, η⟩ tm , where any term can be produced. The transitions for these states are given in Figure 4.

The transition ARG starts the building process when we reach a λ-abstraction in evaluation mode with the empty continuation []. We begin with the index 0, which requires at least 1 λ-abstraction above it, and with the empty stack ⊙. The value of the index can then be increased with the transition SUC, which accordingly also increases the value of κ. When we reach the needed value for the index, the transition VAR switches to the term mode; we use two modes to prevent a SUC transition on a term which is not an index.

In term mode, we can add λ-abstractions to the term, decreasing κ if κ > 0 with transition LAMBDA, or leaving κ at 0 with transition LAMBDA0; the abstractions we introduce when κ = 0 do not bind any variable. Once we are done building a term t in function position of an application, we use transition APPFUN to build the argument s. We start again in index mode, but we store on top of ρ the term t with its counter κ 2 . When we finish s with a counter κ 1 , we build the application with transition APP, which takes the maximum of κ 1 and κ 2 as the new minimal number of λ-abstractions needed above t s. Note that the APP transition is allowed only if ρ is not empty, meaning that at least one APPFUN has been done before. Finally, we can conclude the term building process with transition RESTART only if κ = 0, meaning that all the variables of the term are bound, and if ρ is empty, meaning that there is no application waiting to be finished. Any closed term t can be generated with the AB machine, and it is possible to define the sequence of flags Seq(t) that will be raised in the process. We write () for the empty sequence, and (f 1 , . . . , f n , (f ′ 1 , . . . , f ′ m ), f n+1 , . . . , f l ) for the sequence (f 1 , . . . , f n , f ′ 1 , . . . , f ′ m , f n+1 , . . . , f l ). Definition 19. Given a term t, we define Seq(t) as

Seq(t) ▵ = (SeqTm(t), ) SeqTm(t s) ▵ = (SeqTm(t), , SeqTm(s), @) SeqTm(λ.t) ▵ = (Seq(t), λ) SeqTm(n) ▵ = (SeqInd(n), ⊡) SeqInd(0) ▵ = () SeqInd(n + 1) ▵ = (SeqInd(n), ⊞) We write C Seq(t) Þ → C ′ for C f1 Þ → . . . fm Þ → C ′ where Seq(t) = (f 1 , . . . , f m ). Lemma 20. If t ′ is closed, then ⟨0, 1, ⊙, (t, e)⟩ ind Seq(t ′ ) Þ → ⟨t, (t ′ , ) ∶∶ e, []⟩ ev .
This lemma allows us to prove the correspondence between the AB machine and applicative bisimilarity.

⟨0, 1, ⊙, (t ′ , e ′ )⟩ ind Seq(t ′′ ) Þ → ⟨t ′ , (t ′′ , ) ∶∶ e ′ , []⟩ ev can only be ⟨0, 1, ⊙, η⟩ ind ⊡ Þ →⟨0, 1, ⊙, η⟩ tm 0 λ Þ →⟨λ.0, 0, ⊙, η⟩ tm λ 0 Þ →⟨0, 1, (λ.0, 0) ∶∶ ⊙, η⟩ ind 0 λ 0 ⊞ Þ → ⊡ Þ →⟨1, 2, (λ.0, 0) ∶∶ ⊙, η⟩ tm 1 λ 0 Þ →⟨0, 1, (1, 2) ∶∶ (λ.0, 0) ∶∶ ⊙, η⟩ ind 0 1 λ 0 ⊡ Þ → λ Þ →⟨λ.0, 0, (1, 2) ∶∶ (λ.0, 0) ∶∶ ⊙, η⟩ tm λ 0 1 λ 0 @ Þ →⟨1 λ.0, 2, (λ.0, 0) ∶∶ ⊙, η⟩ tm @ λ 0 1 λ 0 @ Þ →⟨(λ.0) (1 λ.0), 2, ⊙, η⟩ tm @ @ λ 0 1 λ 0 λ Þ →⟨λ.(λ.0) (1 λ.0), 1, ⊙, η⟩ tm λ @ @ λ 0 1 λ 0 λ Þ →⟨λ.λ.(λ.0) (1 λ.0), 0, ⊙, η⟩ tm λ λ @ @ λ 0 1 λ 0 Þ → Fig. 5: Example of argument generation matched by ⟨0, 1, ⊙, (s ′ , d ′ )⟩ ind Seq(t ′′ ) Þ → ⟨s ′ , (t ′′ , ) ∶∶ d ′ , []⟩ ev ,

C. Translation into HOcore

Figure 6 gives the translation of the AB machine in HOcore. We detail each component, starting with the evaluation mode, i.e., the KAM. We follow the same principles as in Section III: a non-empty stack π or environment e is represented by a pair of messages, respectively on hd c and c, and hd e and env. A closure is represented by two messages, one containing the term on η 1 and one containing the environment on η 2 . The process representing the empty environment should never be executed, because all the closures we manipulate are closed; as a result, we can choose any process to represent it, e.g., 0. The empty stack v[]w and the process P rec are used to generate an argument and are explained later.

The encoding of t s simulates the rule PUSH: we receive the current stack and environment e to create the new stack with (s, e) on top. Because we receive the current environment to put it on the stack, we have to recreate it on env, unchanged. In the encoding of λ.t, we capture the stack and environment, and if the stack is non-empty, we fetch its head η to create a new environment with η on top. Finally, a de Bruijn index n > 0 go through the current environment, until we reach the correct closure (case n = 0). In that case, we receive the head η and tail of the environment, discard the tail as it is no longer useful, and we restore the term and environment stored in η.

If λ.t is run in the environment e and the empty stack [], then we obtain v[]w ∥ hd c (z).(vtw ∥ env⟨hd e ⟨z⟩ ∥ env⟨vew⟩⟩), so v[]w has to start the argument generating process, and the result has then to be sent on hd c for the evaluation to restart. We write Stuck((t, e)) for the process in parallel with v[]w, which remains stuck during the whole generation process. We now explain how ⟨n, κ, ρ, η⟩ ind and ⟨t, κ, ρ, η⟩ tm are encoded, starting with κ and ρ.

The machine distinguishes cases based on whether κ is 0 or not, to know if we should apply the transition LAMBDA or LAMBDA0. In the encoding of these rules (see the definition of Lambda), we send on name zero the expected behavior if κ = 0, and on succ what to do otherwise. The translation of the counter receives both messages, executes the corresponding one (e.g., the one on zero for the encoding of 0), and discards the other. Apart from that, κ is translated as a natural number. Similarly, the translation of ρ combines the regular encodings of pairs and stacks, but also indicates whether ρ is empty or not, to know if we can apply the transitions APP and RESTART.

1) Evaluation mode

v⟨t, e, π⟩ ev w

▵ = vtw ∥ env⟨vew⟩ ∥ c⟨vπw⟩ ∥ P rec v(t, e)w ▵ = η 1 ⟨vtw⟩ ∥ η 2 ⟨vew⟩ v[]w ▵ = ⊚( ).(ind⟨v0w⟩ ∥ k⟨v1w c ⟩ ∥ r⟨v⊙w⟩ ∥ initInd⟨0⟩) v w ▵ = 0 vη ∶∶ πw ▵ = hd c ⟨vηw⟩ ∥ c⟨vπw⟩ vη ∶∶ ew ▵ = hd e ⟨vηw⟩ ∥ env⟨vew⟩ vt sw ▵ = App eval (vtw , vsw) App eval (P t , P s ) ▵ = c(x).env(y).(P t ∥ c⟨hd c ⟨v 1 ⟨P s ⟩ ∥ v 2 ⟨y⟩⟩ ∥ x⟩) vλ.tw ▵ = Lam eval (vtw) Lam eval (P t ) ▵ = c(x).(x ∥ hd c (y).env(z).(P t ∥ env⟨hd e ⟨y⟩ ∥ env⟨z⟩⟩)) vn + 1w ▵ = Ind eval (vnw) Ind eval (P n ) ▵ = env(q).x(x ∥ hd e ( ).P n ) v0w ▵ = env(x).(x ∥ hd e (y).env( ).(y ∥ η 1 (y 1 ).η 2 (y 2 ).(y 1 ∥ env⟨y 2 ⟩))) P rec ▵ = RecInd ∥ recint⟨RecInd⟩ ∥ RecTm ∥ rectm⟨RecTm⟩ ∥ RecMax ∥ recmax⟨RecMax⟩
2) Counter κ, stack ρ, and stuck process Stuck(η)

v0w c ▵ = zero(x).succ( ).x v⊙w ▵ = mt(x).cons( ).x vκ + 1w c ▵ = Suk(vκw c ) v(t, κ) ∶∶ ρw ▵ = ConsR(v(t, κ)w , vρw) Suk(P κ ) ▵ = suk⟨P κ ⟩ ∥ zero( ).succ(x).x ConsR(P hd , P ρ ) ▵ = hd r ⟨P hd ⟩ ∥ r⟨P ρ ⟩ ∥ mt( ).cons(x).x Stuck((t, e)) ▵ = hd c (z).(vtw ∥ env⟨hd e ⟨z⟩ ∥ env⟨vew⟩⟩) v(t, κ)w ▵ = w 1 ⟨vtw⟩ ∥ w 2 ⟨vκw c ⟩ 3) Creation of indices v⟨n, κ, ρ, η⟩ ind w ▵ = ind⟨vnw⟩ ∥ k⟨vκw c ⟩ ∥ r⟨vρw⟩ ∥ P rec ∥ initInd⟨0⟩ ∥ Stuck(η) RecInd ▵ = initInd( ).recind(x).(x ∥ recind⟨x⟩ ∥ Succ + Var) Succ ▵ = ⊞( ).ind(x).k(y).(ind⟨Ind eval (x)⟩ ∥ k⟨Suk(y)⟩ ∥ initInd⟨0⟩) Var ▵ = ⊡( ).ind(x).(tm⟨x⟩ ∥ initT m⟨0⟩) 4) Creation of terms v⟨t, κ, ρ, η⟩ tm w ▵ = tm⟨vtw⟩ ∥ k⟨vκw c ⟩ ∥ r⟨vρw⟩ ∥ P rec ∥ initT m⟨0⟩ ∥ Stuck(η) Lambda(P κ ) ▵ = λ( ).tm(x). ⎛ ⎝ tm⟨Lam eval (x)⟩ ∥ P κ ∥ zero⟨k⟨P κ ⟩ ∥ initT m⟨0⟩⟩ ∥ succ⟨suk(y).(k⟨y⟩ ∥ initT m⟨0⟩)⟩ ⎞ ⎠ AppFun(P κ , P ρ ) = ( ).tm(x).(r⟨ConsR(hd r ⟨w 1 ⟨x⟩ ∥ w 2 ⟨P κ ⟩⟩, P ρ )⟩ ∥ ind⟨v0w⟩ ∥ k⟨v1w c ⟩ ∥ initInd⟨0⟩) Done ▵ = ( ).tm(x).(hd c ⟨η 1 ⟨x⟩ ∥ η 2 ⟨v w⟩⟩ ∥ c⟨v[]w⟩) App(P κ , P hd , P ρ ) ▵ = @( ).tm(x 2 ). P hd ∥ w 2 (y).w 1 (x 1 ). max1⟨y⟩ ∥ max2⟨P κ ⟩ ∥ init1⟨y⟩ ∥ init2⟨P κ ⟩ ∥ resu(z).(tm⟨App eval (x 1 , x 2 )⟩ ∥ P ρ ∥ k⟨z⟩ ∥ initT m⟨0⟩) RecMax ▵ = init1(x 1 ).init2(x 2 ).recmax(y).(y ∥ recmax⟨y⟩ ∥ Max(x 1 , x 2 )) Max(P 1 , P 2 ) ▵ = P 1 ∥ zero⟨max2(x).resu⟨x⟩⟩ ∥ succ ⟨suk(x 1 ). ⎛ ⎝ P 2 ∥ zero⟨max1(x).resu⟨x⟩⟩ ∥ succ⟨suk(x 2 ).(init1⟨x 1 ⟩ ∥ init2⟨x 2 ⟩)⟩ ⎞ ⎠ ⟩ RecTm ▵ = initT m( ).rectm(x). ⎛ ⎜ ⎜ ⎜ ⎜ ⎜ ⎜ ⎜ ⎜ ⎜ ⎜ ⎝ x ∥ rectm⟨x⟩ ∥ r(y).y ∥ cons ⟨ k(z).hd r (y 1 ).r(y 2 ). (Lambda(z) ∥ y) + AppFun(z, y) + App(z, y 1 , y 2 ) ⟩ ∥ mt ⟨k(z). ⎛ ⎜ ⎜ ⎜ ⎜ ⎜ ⎝ z ∥ zero ⟨ (Lambda(z) ∥ v⊙w) + AppFun(z, v⊙w) + Done ⟩ ∥ succ ⟨suk( ). (Lambda(z) ∥ v⊙w) + AppFun(z, v⊙w) ⟩ ⎞ ⎟ ⎟ ⎟ ⎟ ⎟ ⎠ ⟩ ⎞ ⎟ ⎟ ⎟ ⎟ ⎟ ⎟ ⎟ ⎟ ⎟ ⎟ ⎠
Fig. 6: Translation of the AB machine After flagging ⊚, the process v[]w starts the argument generation process in index mode: the index being built is sent on ind (here, initialized with v0w), the counter on k, and the stack on r. The message on initInd triggers the recursive process RecInd, which non-deterministically chooses between Succ and Var. Executing Succ flags ⊞, increases the values of the index (thanks to Ind eval ) and the counter (with Suk), and relaunches the RecInd process with a message on initInt. Executing Var flags ⊡, moves the index from ind to tm, and initiates the term mode by sending a message on initT m, which triggers the process RecTm.

The goal of RecTm is to non-deterministically choose between the four transitions available in term mode, namely

λ Þ →, Þ →, @ Þ
→, and Þ →. However, some of these transitions have requirements: @ Þ → needs ρ ≠ ⊙ and Þ → needs ρ = ⊙ and κ = 0. The process RecTm is therefore doing a case analysis to check these conditions. First, it captures vρw on r: if ρ ≠ ⊙, it executes the message on cons, which makes a choice between λ, , and @, which are represented by respectively Lambda, AppFun, and App. If ρ = ⊙, then we do a case analysis on κ. If κ = 0, then we can do either λ, , or (represented by Done), otherwise, only λ or are possible.

The process Lambda adds a λ-abstraction to the term in tm, updating κ (represented by P κ ) accordingly: if κ = 0, then it is restored unchanged on k, otherwise, it is decreased by 1 by releasing the message in suk. The process AppFun pushes on the stack P ρ the current term t 1 on tm and its counter κ 1 (represented by P κ ), which is the term in function position of an application. It then relaunches the index mode to build the argument t 2 with its counter κ 2 . The process App can then build the application itself, by computing the maximum between κ 1 and κ 2 with the processes RecMax and Max.

We compute the maximum between κ 1 and κ 2 by removing the layers of successors common to κ 1 and κ 2 , until we reach 0 for one of them. If we reach 0 for κ 1 first, then κ 2 is the max, otherwise it is κ 1 . We store the initial values of κ 1 and κ 2 in respectively max1 and max2, and the decomposition occurs in Max, where init1 is initialized with κ 1 and init2 with κ 2 . If P 1 = vκ 1 w c = v0w c , then we send κ 2 (stored in max2) on resu. Otherwise, P 1 = suk⟨P ′ 1 ⟩, and we do a case analysis on the process P 2 = vκ 2 w c . If P 2 = v0w c , then we send κ 1 on resu, otherwise P 2 = suk⟨P ′ 2 ⟩, and we restart RecMax by sending P ′ 1 and P ′ 2 on init1 and init2, respectively. Once the max is known on resu, then App builds the application t 1 t 2 and relaunches RecTm.

Finally, the process Done ends the argument generation phase, and restarts the computation by restoring the empty continuation and by passing the term in tm to Stuck(η). The process P rec contains all the processes necessary to encode the different recursive mechanisms.

Full abstraction: We use the notions of Section IV-D to prove the correspondence between the AB machine and its translation. The definition of next carries over to the translation of the AB machine, and Lemmas 12 and 13 still hold (but without terminating transitions). Recall that ≈ HO stands for ≈ H HO , where H contains the names of the translation

⟨n, κ, ρ⟩ ind ⊞ Þ → ⟨n + 1, κ + 1, ρ⟩ ind (SUC) ⟨n, κ, ρ⟩ ind ⊡ Þ → ⟨n, κ, ρ⟩ tm (VAR) ⟨t, κ + 1, ρ⟩ tm λ Þ → ⟨λ.t, κ, ρ⟩ tm (LAMBDA) ⟨t, 0, ρ⟩ tm λ Þ → ⟨λ.t, 0, ρ⟩ tm (LAMBDA0) ⟨t, κ, ρ⟩ tm Þ → ⟨0, 1, (t, κ) ∶∶ ρ⟩ ind (APPPUSH) ⟨t, κ 1 , (s, κ 2 ) ∶∶ ρ⟩ tm ← @ Þ → ⟨t s, max(κ 1 , κ 2 ), ρ⟩ tm ( ← APP) ⟨t, κ 1 , (s, κ 2 ) ∶∶ ρ⟩ tm → @ Þ → ⟨s t, max(κ 1 , κ 2 ), ρ⟩ tm ( → APP) ⟨t, 0, ⊙⟩ tm ⍟ Þ → ⟨t, , []⟩ ev (START) ⟨λ.t, e, []⟩ ev Þ → (DONE)
Fig. 7: Contextual equivalence machine that are not flags. The proof of the following theorem is then the same as for Theorem 14.

Theorem 22. C ≈ m C ′ iff vCw ≈ HO vC ′ w.
We then deduce a full abstraction result between λ-calculus with applicative bisimilarity and HOcore. Remark 24. As explained in the introduction, the encoding of [START_REF] Sangiorgi | The π-Calculus: A Theory of Mobile Processes[END_REF] is not complete w.r.t. applicative bisimilarity, while ours is. The difference is that our translation is tailored to protect itself from bad behaviors of the environment, by limiting its interactions with the outside to synchronizations on flags. A translated λ-abstraction in [START_REF] Sangiorgi | The π-Calculus: A Theory of Mobile Processes[END_REF] is waiting for a channel name which gives access to the argument, but the environment may use this name to give access to a process which is not an encoded λ-term, thus breaking the encoding.

D. Internalizing Contextual Equivalence

Corollary 23 is enough to deduce full abstraction w.r.t. contextual equivalence, since t ≈ ctx s ⇐⇒ (t, ) ≈ app (s, ). However, it is possible to prove this result directly, by internalizing contextual equivalence in an abstract machine.

Figure 7 gives the transitions of this machine, except for the τ Þ → transitions, which are the same as in Section V-A. In contrast with the AB machine, the contextual equivalence machine produces a context first, and then reduces the resulting term; consequently, the starting point is a state ⟨t, 0, ⊙⟩ tm , where t is the closed term we want to plug in the context. When the context is finished, the transition ⍟ Þ → switches to the evaluation mode. Also, the evaluation part of the machine is not executed several times, since ≈ ctx is not coinductive. We flag when the evaluation terminates, to distinguish a terminating term from a diverging one.

Creating a context C is almost the same as generating an argument in the AB machine, except that we want to plug a closed term t inside. We build C[t] by starting the generation process from t; t can be anywhere in C[t], not necessarily at the leftmost position, so we cannot do the generation process going left to right in an application, as with the AB machine (Section V-B). Instead, after producing a term t and with a term s on the stack, we can do either the transition APPLEFT to build t s, or APPRIGHT to build s t.

Example 25. We show how to generate the context λ.(0 0) (◻ 0) around t.

⟨t, 0, ⊙⟩ tm Þ → ⊡ Þ → ⟨0, 1, (t, 0) ∶∶ ⊙⟩ tm → @ Þ → ⟨t 0, 1, ⊙⟩ tm Þ → ⊡ Þ → ⟨0, 1, (t 0, 1) ∶∶ ⊙⟩ tm Þ → ⊡ Þ → ⟨0, 1, (0, 1) ∶∶ (t 0, 1) ∶∶ ⊙⟩ tm → @ Þ → ⟨0 0, 1, (t 0, 1) ∶∶ ⊙⟩ tm ← @ Þ → ⟨(0 0) (t 0), 1, ⊙⟩ tm λ Þ → ⟨λ.(0 0) (t 0), 0, ⊙⟩ tm
The translation of the contextual equivalence machine into HOcore and the full abstraction proofs are then the same as with the AB machine.

Theorem 26. If t and s are closed terms, then t ≈ ctx s iff v⟨t, 0, ⊙⟩ tm w ≈ HO v⟨s, 0, ⊙⟩ tm w.

VI. CONCLUSION AND FUTURE WORK

We propose encodings of the call-by-name λ-calculus into HOcore, fully abstract w.r.t. different equivalences of the λcalculus, namely normal-form and applicative bisimilarities, and contextual equivalence. This shows that a minimal higherorder calculus with a fixed number of hidden names, which is much less expressive than the name-passing π-calculus, still has enough expressive power to faithfully encode the call-byname λ-calculus. Note that our encodings can immediately be ported to HOπ by adding a few top-level restrictions. Our fullabstraction results then hold with the usual barbed equivalence of HOπ, no longer requiring hidden names. This, however, gives no intuition on the expressiveness of HOcore.

We use abstract machines not only to fix the reduction strategy, but also as an intermediary step between the equivalences of the λ-calculus and HOcore. We turn the equivalences of the λ-calculus, and their potentially complex testing conditions, into a bisimilarity over a labeled transition system (a flags-generating machine), which is closer to the HOcore equivalence. We believe this internalization technique can be applied to other languages for which an abstract machine has been defined, like, e.g., the call-by-value calculus and its CK machine [START_REF] Felleisen | Semantics Engineering with PLT Redex[END_REF] (see Appendix C), or a calculus with control operators [START_REF] Biernacka | An operational foundation for delimited continuations in the CPS hierarchy[END_REF]. Even though the bisimilarities for these calculi can be quite intricate (see, e.g., [START_REF] Biernacki | Bisimulations for delimitedcontrol operators[END_REF]), it should be always possible to generate a context as in Section V-D to internalize contextual equivalence. We also think we can internalize more complex equivalences, like environmental bisimilarities, using Madiot's framework [START_REF] Madiot | Higher-order languages: dualities and bisimulation enhancements[END_REF], which expresses these bisimilarities as a labeled transition system.

Finally, the encodings of the extended abstract machines into HOcore rely on the same principles, e.g., to represent stacks, non-deterministic choice, case analyses on terms, etc. We believe it is possible to automatically derive the encoding from an abstract machine, so that the generated translation is deterministic (up to flags for choice processes, as in Lemma 12) and with an operational correspondence result similar to Lemma 13. As these two ingredients are almost sufficient to get full abstraction between machines and HOcore, it would give us Theorem 14 or Theorem 22 for free.

R are easy to match, and the observable actions are the same because of the condition WkObs(P C ) = WkObs(P C ′ ). What is left to check are the reductions.

If P C τ → P ′ C , then we show that there exists

P ′ C ′ ∥ R such that P C ′ ∥ R τ ⇒ P ′ C ′ ∥ R and P ′ C ∥ R R P ′ C ′ ∥ R. If P C τ ⇒
= P C2 ∥ R ′ . We have vCw f ⇒ vC 2 w, so C τ Þ → * f Þ → C 2 holds by Lemma 13. Because C ≈ m C ′ , there exists C ′ 2 such that C ′ τ Þ → * f Þ → C ′ 2 and C 2 ≈ m C ′ 2 . By Lemma 13, this implies vC ′ w f ⇒ vC ′ 2 w; in particular, there exists P C ′ 2 such that vC ′ w τ ⇒ f → P C ′ 2 τ ⇒ vC ′ 2 w. By Lemma 12, we also have P C ′ τ ⇒ f → P C ′ 2 , therefore we have P C ′ ∥ R τ ⇒ P C ′ 2 ∥ R ′ , with P C2 ∥ R ′ R P C ′ 2 ∥ R ′ , as wished.
If f = , then P C → P for some P ′′ such that P ′′ ≈ HO 0, and by Lemma 12, we have Þ → ⟨t ′ , κ, ρ, η⟩ tm where κ = max (fv(t ′ )) + 1 if t ′ is not closed, and κ = 0 otherwise. The case t = n is concluded with the previous observation. If Þ → ⟨t ′′ , κ, ρ, η⟩ tm , and then ⟨t ′′ , κ, ρ, η⟩ tm λ Þ → ⟨t ′ , κ ′ , ρ, η⟩ tm where κ ′ is as wished depending on κ.

P ′ = P ′′ ∥ R ′ . We have vCw τ ⇒ → P ′′ , so C τ Þ → * Þ → holds by Lemma 13. Because C ≈ m C ′ , we have C ′ τ Þ → * Þ →.
t ′ = t ′ 1 t ′ 2 , then ⟨0, 1, ρ, η⟩ ind SeqTm(t ′ 1 ) Þ → ⟨t ′ 1 , κ 1 , ρ, η⟩ tm (by induction) Þ → ⟨0, 1, (t ′ 1 , κ 1 ) ∶∶ ρ, η⟩ ind SeqTm(t ′ 2 ) Þ → ⟨t ′ 2 , κ 2 , (t ′ 1 , κ 1 ) ∶∶ ρ, η⟩ tm (by induction) @ Þ → ⟨t ′ 1 t ′ 2 , max (κ 1 , κ 2 ),
This implies that for a closed term t ′ , we have We present a variant of the CK machine [START_REF] Felleisen | Semantics Engineering with PLT Redex[END_REF] with evaluation contexts below.

t s ⋆ E τ Þ → t ⋆ E s (FUN) v ⋆ E τ Þ → E ⋆ ct v (SWITCH) E t ⋆ ct v τ Þ → t ⋆ v E (ARG) (λx.t) E ⋆ ct v τ Þ → [v x]t ⋆ E (BETA)
When we get a value in an evaluation context, we switch into the continuation mode (rule SWITCH) to evaluate the argument of that value (rule ARG), or do the β-reduction if the argument itself is a value (rule BETA). Normal-form bisimilarity for call-by-value is defined as follows.

Definition 30. A symmetric relation R is a normal-form bisimulation if t R s implies:

• if t ⋆ ◻ τ Þ → * ◻ ⋆ ct α, then s ⋆ ◻ τ Þ → * ◻ ⋆ ct α; • if t ⋆ ◻ τ Þ → * ◻ ⋆ ct λx.t ′ , then there exists s ′ such that s ⋆ ◻ τ Þ → * ◻ ⋆ ct λx.s ′ and [α x]t ′ R [α x]s ′ for a fresh α; • if t ⋆ ◻ τ Þ → * α E ⋆ ct v, then there exist E ′ and v ′ such that s ⋆ ◻ τ Þ → * α E ′ ⋆ ct v ′ , v R v ′ , and E[α ′ ] R E ′ [α ′ ]
for a fresh α ′ . Normal-form bisimilarity ≈ nf , is the largest normal-form bisimulation.

We extend the CK machine into a NFB machine in Figure 8. We have a counter n to generate fresh variables, as in call-byname. The four last rules tell us what to do to compare normal forms. If we get a variable α, then we signal its value and we are done (transition DONE). If we have a λ-abstraction, we restart the machine (transition LAMBDA). If we have a context of the form α E, it means that we have a normal form E[α v]: we have to choose if we either test v (transition VAL) or E (transition CONTEXT). To test v, we forget about E, and enter the context mode with ⟨◻, v, n⟩ ct after flagging α and ▼. Depending on v, we will then apply the transition DONE or LAMBDA. To test E, we generate a fresh variable to plug into E, meaning that we continue with ⟨E, n, n + 1⟩ ct (after flagging α and ▶).

We can translate this machine in HOcore using the same techniques and prove full abstraction as in call-by-name. Internalizing applicative bisimilarity in call-by-value is straightforward: its definition differs from call-by-value only in the fact that the testing argument must be a λ-abstraction. Consequently, we just use the argument-generating rules from Figure 4 on top of the CK machine, and change the rule RESTART so that it can trigger only if the constructed term is a λ-abstraction.

Fig. 1 :Definition 1 .

 11 Fig. 1: HOcore LTS

Theorem

Fig. 3 :

 3 Fig. 3: Translation of the NFB machine into HOcore

Example 18 .

 18 Figure 5 presents how we generate the term λ.λ.(λ.0) (1 λ.0); we start with the underlined 0.

Corollary 23 .

 23 If (t, e) and (s, d) are closed closures, then (t, e) ≈ app (s, d) iff v⟨t, e, []⟩ ev w ≈ HO v⟨s, d, []⟩ ev w.

⟨0, 1 ,

 1 ⊙, η⟩ ind SeqTm(t ′ ) Þ → ⟨t ′ , 0, ⊙, η⟩ tm , and the last transition Þ → gives what we want. Theorem 21. (t, e) ≈ app (s, d) iff ⟨t, e, []⟩ ev ≈ m ⟨s, d, []⟩ ev . Proof. To prove that machine bisimilarity implies applicative bisimilarityt, e), (s, d)) ⟨t, e, []⟩ ev≈ m ⟨s, d, []⟩ ev } is an applicative bisimulation. If ⟨t, e, []⟩ ev τ Þ → * ⟨λ.t ′ , e ′ , []⟩ ev , then because we have also ⟨λ.t ′ , e ′ , []⟩ ev ⊚ Þ → ⟨0, 1, ⊙, (t ′ , e ′ )⟩ ind , there exist s ′ and d ′ such that ⟨s, d, []⟩ ev τ Þ → * ⟨λ.s ′ , d ′ , []⟩ ev ⊚ Þ → ⟨0, 1, ⊙, (s ′ , d ′ )⟩ ind and ⟨0, 1, ⊙, (t ′ , e ′ )⟩ ind ≈ m ⟨0, 1, ⊙, (s ′ , d ′ )⟩ ind . For all closed t ′′ , we have then ⟨0, 1, ⊙, (t ′ , e ′ )⟩ ind Seq(t) Þ → ⟨t ′ , (t ′′ , ) ∶∶ e ′ , []⟩ ev byLemma 20, which can only be matched by⟨0, 1, ⊙, (s ′ , d ′ )⟩ ind Seq(t) Þ → ⟨s ′ , (t ′′ , ) ∶∶ d ′ , []⟩ ev meaning that ⟨t ′ , (t ′′ , ) ∶∶ e ′ , []⟩ ev ≈ m ⟨s ′ , (t ′′ , ) ∶∶ d ′ , []⟩ ev .We can then easily conclude.For the reverse implication, we show thatR ▵ = {(⟨t, e, []⟩ ev , ⟨s, d, []⟩ ev ) (t, e) ≈ app (s, d)} ∪ {(⟨n, κ, ρ, (t, e)⟩ ind ), ⟨n, κ, ρ, (s, d)⟩ ind ) (λ.t, e) ≈ app (λ.s, d)} ∪ {(⟨t ′ , κ, ρ, (t, e)⟩ tm ), ⟨t ′ , κ, ρ, (s, d)⟩ tm ) (λ.t, e) ≈ app (λ.s, d)} is a machine bisimulation. If ⟨t, e, []⟩ ev τ Þ → * ⊚ Þ → ⟨0, 1, ⊙, (t ′ , e ′ )⟩ ind , then we have ⟨t, e, []⟩ ev τ Þ → * ⟨λ.t ′ , e ′ , []⟩ ev , so there exists (s ′ , d ′ ) such that ⟨s, d, []⟩ ev τ Þ → * ⟨λ.s ′ , d ′ , []⟩ ev so that (λ.t ′ , e ′ ) ≈ app (λ.s ′ , d ′ ). But then also ⟨λ.t ′ , e ′ , []⟩ ev ⊚ Þ → ⟨0, 1, ⊙, (s ′ , e ′ )⟩ind and we obtain configurations in R. If ⟨t ′ , κ, ρ, (t, e)⟩ arg f Þ → C with f ≠ and arg ∈ {ind, tm}, then ⟨t ′ , κ, ρ, (t, e)⟩ arg f Þ → C ′ where C ′ is the same as C except for the stored closures, which are not changed and therefore still applicative bisimilar; we have therefore C R C ′ . If ⟨t ′ , κ, ρ, (t, e)⟩ tm Þ → ⟨t, (t ′ , ) ∶∶ e, []⟩ ev , then ⟨t ′ , κ, ρ, (s, d)⟩ tm Þ → ⟨s, (t ′ , ) ∶∶ d, []⟩ ev , and the resulting terms are in R because (λ.

▵=

  E[v t]. Normal forms are either values or terms of the form E[α v].

  abstraction λx.t binds x in t; a term is closed if it does not contain any free variables. We use [] to denote the empty stack. In PUSH, the argument s of an application is stored on the stack while the term t in function position is evaluated. If we get a λ-abstraction λx.t, then an argument s is fetched from the stack (transition GRAB), and the evaluation continues with [s x]t. If a configuration of the form λx.t⋆[] is reached, then the evaluation is finished, and the result is λx.t. Because we evaluate closed terms only, it is not possible to obtain a configuration of the form x ⋆ π.

  [START_REF] Cimini | Functions as processes: Termination and the λµμ-calculus[END_REF]. We have t ≈ nf s iff there exists n > max (fv(t) ∪ fv(s)) such that ⟨t, [], n⟩ ev ≈ m ⟨s, [], n⟩ ev .

Sketch. Machine bisimilarity implies ≈ nf because {(t, s) ⟨t, [], n⟩ ev ≈ m ⟨s, [], n⟩ ev , n > max (fv(t) ∪ fv(s))} is a normal-form bisimulation, and the other direction is by showing that {(⟨t, [], n⟩ ev , ⟨s, [], n⟩ ev

  1 0. The syntax of terms (t, s), closures (η), environments (e, d), and values (v) is as follows. t ∶∶= n t s λ.t η ∶∶= (t, e) e ∶∶= η ∶∶ e v ∶∶= (λ.t, e) A closure η is a pair (t, e) where e is an environment mapping the free variables of t to closures; environments are used in lieu of substitutions. A term t is closed if fv(t) = ∅, and a closure (t, e) is closed if the number of elements of e is bigger than the highest free variable of t. The semantics is given by the original, environment-based KAM, where a configuration C is now composed of the closed closure (t, e) being evaluated, and a stack π of closures. The transitions rules are as follows. C ∶∶= ⟨t, e, π⟩ ev (configurations) Contextual equivalence compares closed terms by testing them within all contexts. A context C is a term with a hole ◻ at a variable position; plugging a term t in C is written C[t]. A context is closed if fv(C) = ∅. Contextual equivalence is then defined as follows. ′ , d ′ , []⟩ ev for some s ′ and d ′ . ′ , d ′ , []⟩ ev , and for all closed t ′′ , we have (t, (t ′′ , ) ∶∶ e) R (s, (t ′′ , ) ∶∶ d).

		⟨λ.t, e, []⟩ ev	⊚ Þ → ⟨0, 1, ⊙, (t, e)⟩ ind	(ARG)
		⟨n, κ, ρ, η⟩ ind	⊞ Þ → ⟨n + 1, κ + 1, ρ, η⟩ ind	(SUC)
		⟨n, κ, ρ, η⟩ ind	⊡ Þ → ⟨n, κ, ρ, η⟩ tm	(VAR)
	⟨t, κ + 1, ρ, η⟩ tm	λ Þ → ⟨λ.t, κ, ρ, η⟩ tm	(LAMBDA)
		⟨t, 0, ρ, η⟩ tm	λ Þ → ⟨λ.t, 0, ρ, η⟩ tm	(LAMBDA0)
		⟨t, κ, ρ, η⟩ tm Þ → ⟨0, 1, (t, κ) ∶∶ ρ, η⟩ ind (APPFUN)
	⟨s, κ 1 , (t, κ 2 ) ∶∶ ρ, η⟩ tm	@ Þ → ⟨t s, max(κ 1 , κ 2 ), ρ, η⟩ tm (APP)
	⟨t, 0, ⊙, (s, e)⟩ tm Þ → ⟨s, (t, ) ∶∶ e, []⟩ ev	(RESTART)
	Fig. 4: AB machine: argument generation
	⟨s, d, []⟩ ev	τ Þ →	*	⟨λ.s
					Definition 16. Two closed terms t and s are contextually
					equivalent, written t ≈ ctx s, if for all closed contexts C, ⟨C[t], , []⟩ ev * τ Þ → ⟨λ.t ′ , e ′ , []⟩ ev for some t ′ and e ′ iff ⟨C[s], , []⟩ ev * τ Þ → ⟨λ.s Contextual equivalence is characterized by applicative
					bisimilarity [1], which reduces closed terms to values that are
					then applied to an arbitrary argument.

π ∶∶= η ∶∶ π [] (stacks) ⟨t s, e, π⟩ ev τ Þ → ⟨t, e, (s, e) ∶∶ π⟩ ev (PUSH) ⟨0, (t, e) ∶∶ d, π⟩ ev τ Þ → ⟨t, e, π⟩ ev (ZERO) ⟨n + 1, (t, e) ∶∶ d, π⟩ ev τ Þ → ⟨n, d, π⟩ ev (ENV) ⟨λ.t, e, η ∶∶ π⟩ ev τ Þ → ⟨t, η ∶∶ e, π⟩ ev (GRAB) In PUSH, the argument s of an application is stored on the stack with its environment e while the term t in function position is evaluated. If we get a λ-abstraction λ.t (transition GRAB), then an argument η is moved from the stack to the top of the environment to remember that η corresponds to the de Bruijn index 0, and the evaluation continues with t. Looking up the closure corresponding to a de Bruijn index in the environment is done with the rules ENV and ZERO. Because we evaluate closed closures only, it is not possible to obtain a configuration of the form ⟨n + 1, , π⟩ ev . If a configuration of the form ⟨λ.t, e, []⟩ ev is reached, then the evaluation is finished, and the result is (λ.t, e). Behavioral equivalences: Definition 17. A symmetric relation R on closed closures is an applicative bisimulation if (t, e) R (s, d) and ⟨t, e, []⟩ ev τ Þ → * ⟨λ.t ′ , e ′ , []⟩ ev implies that there exist s ′ and d ′ such that

  Theorem 21. (t, e) ≈ app (s, d) iff ⟨t, e, []⟩ ev ≈ m ⟨s, d, []⟩ ev .

	Sketch. To prove that machine bisimilarity implies applicative
	bisimilarity, we show that

{((t, e), (s, d)) ⟨t, e, []⟩ ev ≈ m ⟨s, d, []⟩ ev } is an applicative bisimulation. Roughly, (t, e) evaluating to (λ.t ′ , e ′ ) means that (s, d) evaluates to (λ.s ′ , d ′ ) thanks to ⊚. Then for all closed t ′′ , the sequence

  so we can conclude. For the reverse implication, we show that R []⟩ ev , ⟨s, d, []⟩ ev ) (t, e) ≈ app (s, d)} ∪ {(⟨n, κ, ρ, (t, e)⟩ ind ), ⟨n, κ, ρ, (s, d)⟩ ind )

	(λ.t, e) ≈ app (λ.s, d)}
	∪ {(⟨t ′ , κ, ρ, (t, e)⟩ tm ), ⟨t ′ , κ, ρ, (s, d)⟩ tm )
	(λ.t, e) ≈ app (λ.s, d)}
	is a machine bisimulation, which is easy to check.

▵ = {(⟨t, e,

  vCw and P C ′ τ ⇒ vC ′ w, then taking P ′ C ′ = vC ′ w works. If vCw τ ⇒ P C and vC ′ w τ ⇒ P C ′ , then we distinguish two cases. If P C is not a choice process, then WkObs(P C ) = WkObs(P ′ C ), and we can simply choose P ′ C ′ = P C ′ . Otherwise, the transition P C τ → P ′ C is making a choice, and we have WkObs(P C ) = {▶, ▼}, and either WkObs(P ′ C ) = {▶} or WkObs(P ′ C ) = {▼}. But WkObs(P C ) = WkObs(P C ′ ), which is possible only if P C ′ also reduces to a choice process. Then it is possible to choose the corresponding branch, and define P ′ C ′ accordingly. Suppose P C ∥ R τ → P ′ with a communication on a flag f -a communication on another name is not possible; then P C ↓ f , which is possible only in the case vCw τ ⇒ P C , and R ↓ f . Suppose f ≠ . Then we also have P C f → P C2 τ ⇒ vC 2 w for some P C2 and with vC 2 w = next(f, P C ), so by Lemma 12, there exist R ′ such that P ′

  By Lemma 13, this implies vC ′ w Theorem 14. C ≈ m C ′ iff vCw ≈ HO vC ′ w.

	Proof. By Lemmas 28 and 29.
	B. Proofs for Applicative Bisimilarity
	Lemma 20. If t ′ is closed, then ⟨0, 1, ⊙, (t, e)⟩ ind	Seq(t ′ Þ → )
	⟨t, (t

τ ⇒ → P ′′′ for some P ′′′ such that P ′′′ ≈ HO 0. By Lemma 12, we also have

P C ′ τ ⇒ f → P ′′′ , therefore we have P C ′ ∥ R τ ⇒ P ′′′ ∥ R ′ ,

so we obtain processes in the second set of R. ′ , ) ∶∶ e, []⟩ ev . Proof. Let η = (t, e). First, for all n, we have ⟨0, 1, ρ, η⟩ ind ⊞ Þ → n ⊡ Þ → ⟨n, n + 1, ρ, η⟩ tm . Then we show by induction on t ′ that ⟨0, 1, ρ, η⟩ ind SeqTm(t ′ )

  ρ, η⟩ tm And by case analysis on (κ 1 , κ 2 ), one can check that max (κ 1 , κ 2 ) is the desired value. If t ′ = λ.t ′′ , then by induction, we have ⟨0, 1, ρ, η⟩ ind SeqTm(t ′′ )

  t, e) ≈ app (λ.s, d) implies (t, (t ′ , ) ∶∶ e) ≈ app (s, (t ′ , ) ∶∶ d) for all closed t ′ . NFB machine for call by valueC. Call-by-ValueWe informally present the machines for the call-by-value λ-calculus, without the proofs, to see how our techniques can be adapted in that case. The syntax of values and call-by-value contexts are as follows.

	⟨t s, E, n⟩ ev	τ Þ → ⟨t, E s, n⟩ ev	(FUN)
	⟨v, E, n⟩ ev	τ Þ → ⟨E, v, n⟩ ct	(SWITCH)
	⟨E t, v, n⟩ ct	τ Þ → ⟨t, v E, n⟩ ev	(ARG)
	⟨(λx.t) E, v, n⟩ ct	τ Þ → ⟨[v x]t, E, n⟩ ev	(BETA)
	⟨◻, α, n⟩ ct	α Þ →	(DONE)
	⟨◻, λx.t, n⟩ ct	⊚ Þ → ⟨[n x]t, ◻, n + 1⟩ ev	(LAMBDA)
	⟨α E, v, n⟩ ct	α▼ Þ → ⟨◻, v, n⟩ ct	(VAL)
	⟨α E, v, n⟩ ct	α▶ Þ → ⟨E, n, n + 1⟩ ct	(CONTEXT)
	Fig. 8:

v ∶∶= α λx.t E ∶∶= ◻ E t v E

Contexts are represented inside-out: plugging is defined as

◻[t] ▵ = t, (E t 2 )[t 1 ] ▵ = E[t 1 t 2 ]

, and (v E)

[t]

⟨α, π, n⟩ ev by Lemma 7, and then Lemma 7) and π R π ′ , as required.

For the reverse implication, we show that

n⟩ ev with ⟨t, [], n⟩ ev R ⟨s, [], n⟩ ev , as wished.

Lemma 12. Let P be a machine process which is not a choice process. If P f → P ′ and P f → P ′′ , then P ′ = P ′′ . Let P be a choice process. If P τ → P ′ , P τ → P ′′ , and WkObs(P ′ ) = WkObs(P ′′ ), then P ′ = P ′′ .

Proof. A machine process which is not a choice process has at most one possible communication. For choice processes, the flags tell us which branch has been selected.

Lemma 13. The following assertions hold:

• C Þ → iff vCw τ ⇒ → P and P ≈ HO 0.

Proof. By case analyses on

and vCw.

The following lemma allows us to reason up to τ -transitions on the HOcore side.

Lemma 27. Let P , P ′ be machine processes. If P τ ⇒ P ′ and WkObs(P ) = WkObs(P ′ ), then P ≈ HO P ′ .

Proof. One can show that {(P ∥ R, P ′ ∥ R) P τ ⇒ P ′ , WkObs(P ) = WkObs(P ′ )} ∪ {(R, R)} is a barbed bisimulation, using Lemma 12.

Lemma 28. The relation Lemma 13, which in turn implies that there exists P such that vC ′ 1 w ∥ f τ ⇒ P and vC 3 w ≈ HO P . In particular, we have WkObs(vC 3 w) = WkObs(P ), meaning that ¬(P ↓ f ). Consequently, there exists P ′ such that vC ′ 1 w τ ⇒ P ′ and P ′ ↓ f . Then we have

τ ⇒ vC 2 w ∥ τ ⇒ P with P ≈ HO 0 by Lemma 13, which in turn implies that there exists P ′ such that vC ′ 1 w ∥ τ ⇒ P ′ and P ≈ HO P ′ ≈ HO 0, so by Lemma 13, we have C ′