Clément Aubert
email: caubert@augusta.edu

Daniele Varacca
email: daniele.varacca@u-pec.fr

Processes, Systems & Tests: Defining Contextual Equivalences

In this position paper, we would like to offer and defend a template to study equivalences between programs-in the particular framework of process algebras for concurrent computation. We believe that our layered model of development will clarify the distinction that is too often left implicit between the tasks and duties of the programmer and of the tester. It will also enlighten pre-existing issues that have been running across process algebras such as the calculus of communicating systems, the π-calculus-also in its distributed version-or mobile ambients. Our distinction starts by subdividing the notion of process in three conceptually separated entities, that we call Processes, Systems and Tests. While the role of what can be observed and the subtleties in the definitions of congruences have been intensively studied, the fact that not every process can be tested, and that the tester should have access to a different set of tools than the programmer is curiously left out, or at least not often formally discussed. We argue that this blind spot comes from the under-specification of contexts-environments in which comparisons occur-that play multiple distinct roles but supposedly always "stay the same".

Introduction

In the study of programming languages, contextual equivalences play a central role: to study the behavior of a program, or a process, one needs to observe its interactions with different environments, e.g. what outcomes it produces. If the program is represented by a term in a given syntax, environments are often represented as contexts surrounding the terms. But contexts play multiple roles that serve different actors with different purposes. The programmer uses them to construct larger programs, the user employs them to provide input and obtain an output, and the tester or attacker uses them to debug and compare the program or to try to disrupt its intended behavior.

We believe that representing those different purposes with the same "monolithic" syntactical notion of context forced numerous authors to repeatedly "adjust" their definition of context without always acknowledging it. We also argue that collapsing multiple notions of contexts into one prevented further progress. In this article, we propose a way of clarifying how to define contextual equivalences, and show that having co-existing notions of equivalences legitimates and explains recurring choices, and supports a rigorous guideline to separate the development of a program from its usage and testing.

Maybe in the mind of most of the experts in the formal study of programming language is our proposal too obvious to discuss. However, if this is the case, we believe that this "folklore" remains unwritten, and that since we were not at that "seminar at Columbia in 1976" 1 , we are to remain in darkness.

We believe the interactive and friendly community of ICE to be the ideal place to reach curious and open-minded actors in the field, and to either be proven wrong or-hopefully-impact some researchers. Non-technical articles can at times have a tremendous impact [START_REF] Edsger | Letters to the editor: go to statement considered harmful[END_REF], and even if we do not claim to have Dijkstra's influence or talent, we believe that our precise, documented proposition can shed a new light on past results, and frame current reflections and future developments. We also believe that ignoring or downplaying the distinctions we stress have repeatedly caused confusions.

The Flow of Testing

We begin by illustrating with a simple Java example the three syntactic notions-process, system and test-we will be using. Imagine giving a user the code while(i < 10){x *= x; i++;}. A user cannot execute or use this "snippet" unless it is wrapped into a method, with adequate header, and possibly variable declaration(s) and return statement. Once the programmer performed this operation, the user can use the obtained program, and the tester can interact with it further, e.g. by calling it from a main method.

All in all, a programmer would build on the snippet, then the tester would build an environment to interact with the resulting program, and we could obtain the code below. Other situations could arise-e.g., if the snippet was already wrapped-, but we believe this is a fair rendering of "the life of a snippet". public class Main{ public static int foo(int x){ int i = 0; while(i < 10){ x *= x; i++; } return x; } public static void main(){ System.out.print(foo(2)); } }

In this example, the snippet is what we will call a process, the snippet once wrapped is what we will call a system and the "Interaction" part without the system in it, but with additional "observations"-i.e. measures on the execution, terminal output-, is what we will call a test. Our terminology comes from the study of concurrent process algebras, where most of our intuitions and references are located, but let us first make a brief detour to examine how our lens applies to λ -calculus.

A Foreword on λ -Calculus

Theoretical languages often take λ -calculus as a model or a comparison basis. It is often said that the λ -calculus is to sequential programs what the π-calculus is to concurrent programs [START_REF] Sangiorgi | Pi-Calculus[END_REF][START_REF] Varela | Programming Distributed Computing Systems: A Foundational Approach[END_REF]. Indeed, pure λcalculus (i.e. without types or additional features like probabilistic sum [START_REF] Faggian | Lambda Calculus and Probabilistic Computation[END_REF] or quantum capacities [START_REF] Selinger | Quantum Lambda Calculus[END_REF][START_REF] Van Tondervan | A Lambda Calculus for Quantum Computation[END_REF]) is a reasonable [START_REF] Accattoli | Beta reduction is invariant[END_REF], Turing-complete and elegant language, that requires only a couple of operators, one reduction rule and one equivalence relation to produce a rich and meaningful theory, sometimes seen as an idealized target language for functional programming languages.

Since most terms 2 do not reduce as they are, to study their behavior, one needs first to make them interact with an environment, represented by a context. Contexts are generally defined as "term[s] with some holes" [13, p. 29, 2.1.18], that we prefer to call slots and denote [ ]. Under this apparent simplicity, they should not be manipulated carelessly, as having multiple slots or not being careful when defining what it means to "fill a slot" can lead to e.g. lose confluence [18, pp. 40-41, Example 2.2.1], and as those issues persist even in the presence of a typing system [START_REF] Hashimoto | A typed context calculus[END_REF]. Furthermore, definitions and theorems that use contexts frequently impose some restrictions on the contexts considered, to exclude e.g. (λ x.y)[ ] that simply "throw away" the term put in the slot in one step of reduction. Following the above observations, we conclude that contexts often come in two flavors, depending on the nature of the term considered:

For closed terms (i.e. without free variables), a context is essentially a series of arguments to feed the term. This observation allows to define e.g. For open terms (i.e. with free variables), a context is a Böhm transformation [13, p. 246, 10.3.3], which is equivalent [13, p. 246, 10.3.4] to a series of abstractions followed by a series of applications, and sometimes called "head context" [7, p. 25].

Being closed corresponds to being "wrapped"-ready to use-, and feeding arguments to a term corresponds to interacting with it from a main method: the Böhm transformation actually encapsulates two operations at once. In this case, the interaction can observe different aspects: whether the term terminates, whether it grows in size, etc., but it is generally agreed upon that no additional operator or reduction rule should be used. Actually, the syntax is restricted when testing, as only application is allowed: the tested term should not be wrapped in additional layers of abstraction if it is already closed.

Adding features to the λ -calculus certainly does not restore the supposed purity or unicity of the concept of context, but actually distances it even further from being simply "a term with a slot". For instance, contexts are narrowed down to term context [84, p. 1126] and surface context [29, pp. 4, 10] for respectively quantum and probabilistic λ -calculus, to "tame" the power of contexts. In resource sensitive extensions of the λ -calculus, the quest for full abstraction even led to a drastic separation of λ -terms between terms and tests [START_REF] Bucciarelli | Full Abstraction for Resource Calculus with Tests[END_REF], a separation naturally extended to contexts [START_REF] Breuvart | Dissecting denotational semantics[END_REF]p. 73,Figure 2.4].

This variety happened after the 2000's formal studies of contexts was undertaken [START_REF] Bognar | Contexts in Lambda Calculus[END_REF][START_REF] Bognar | A Calculus of Lambda Calculus Contexts[END_REF][START_REF] Hashimoto | A typed context calculus[END_REF], which led to the observation that treating contexts "merely as a notation [. . .] hinders any formal reasoning[, while treating them] as first-class objects [allows] to gain control over variable capturing and, more generally, 'communication' between a context and expressions to be put into its holes" [19, p. 29]. It is ironic that λ -calculists took inspiration from a concurrent language to split their syntax in two right at its core [22, p. 97], or to study formally the communication between a context and the term in its slot, while concurrent languages sometimes tried to keep the "purity" and indistinguishability of their contexts. It can be noted that this re-definition of contexts had impacts on other fields, e.g. on modal type theory [START_REF] Nanevski | Contextual Modal Type Theory[END_REF].

In the case of concurrent calculi like the calculus of communicating systems (CCS) or the π-calculus, interactions with environments are also represented using a notion of context. But the status of contexts in concurrent calculi is even more unsettling when one notes that, while "wrapping" contexts are of interest mainly for open terms in lambda calculus, all terms need a pertinent notion of context in concurrent systems to be tested and observed. Indeed, as the notion of "feeding arguments to a concurrent process" concurs with the idea of wrapping it into a larger process, it seems that the distinction we just made between two kinds of contexts in λ -calculus cannot be ported to concurrent calculi. Our contribution starts by questioning whenever, indeed, process calculi have treated contexts as a uniform notion independently from the nature of the term or what it was used for.

Contextual Relations

Comparing terms is at the core of the study of programming languages, and process algebra is no exception. Generally, and similarly to what is done in λ -calculus, a comparison is deemed of interest only if it is valid in every possible context 3 an idea formally captured by the notion of (pre-)congruence. An equivalence relation R is usually said to be a congruence if it is closed by context, i.e. if for all P, Q (open or closed) terms, (P, Q) ∈ R implies that for all context C[ ], (C[P],C[Q]) ∈ R. (Sometimes, the additional requirement that terms in the relation needs to be similar up to uniform substitution is added [START_REF] Honda | On Reduction-Based Process Semantics[END_REF], and sometimes [68, p. 516, Definition 2], only the closure by substitution-seen as a particular kind of context-is required.)

A notable example of congurence is barbed congruence [50, Definition 2.1.4, 61, Definition 8], which closes by context a reduction-closed relation used to observe "barbs"-the channel(s) on which a process can emit or receive. It is often taken to be the "reference behavioural equivalence" [50, p. 4], as it observes the interface of processes, i.e. on which channels they can interact over the time and in parallel.

But behind this apparent uniformity in the definition of congruences, the definition of contextual relations itself have often been tweaked by altering the definition of context, with no clear explanation nor justification, as we illustrate below.

In the calculus of communicating systems, notions as central as contextual bisimulation [8, In the semantic theory for processes, at least in the foundational theory we would like to discuss below, one difficulty is that the class of formal theories restricted to "reduction contexts" [40, p. 448] still fall short on providing a satisfactory "formulation of semantic theories for processes which does not rely on the notion of observables or convergence". Hence, the authors have to furthermore restrict the class of terms to insensitive terms [40, p. 450] terms are terms that will not interact with the context in which they are placed, and that need to be equated by sound theories.

Across calculi, a notion of "closing context"-that emerged from λ -calculus [8, p. 85], and matches the "wrapping" of a snippet-can be found in e.g. typed versions of the π-calculus [79, p. 479], in mobile ambient [85, p. 134], in the applied π-calculus [1, p. 7], and in the fusion calculus [51, p. 6]. Also known as "completing context" [74, p. 466], those contexts are parametric in a term, the idea being that such a context will "close" the term under study, making it amenable to tests and comparisons.

Let us try to extract some general principles from this short survey. It seems that contexts are 1. in appearance given access to the same operators than terms, 2. sometimes deemed to be "un-reasonable", without always a clear justification, 3. shrunken by need, to bypass some of the difficulties they raise, or to preserve some notions, 4. sometimes picked by the term itself-typically because the same "wrapping" cannot be applied to all processes. Additionally, in all those cases, contexts are given access to a subset of operators, or restricted to contexts with particular behavior, but never extended. If we consider that contexts are the main tool to test the equivalence of processes, then why should the testers-or the attackeralways have access to fewer tools than the programmer? What reason is there not to extend the set of tools, of contexts, or simply take it to be orthogonal? The method we sketch below allows and actually encourages such nuances, would justify and acknowledge the restrictions we just discussed instead of adding them passing-by, and actually corresponds to common usage.

Processes, Systems and Tests

As in the λ -calculus, most concurrent calculi make a distinction between open and closed terms. For instance, the distributed π-calculus [START_REF] Hennessy | A distributed Pi-calculus[END_REF] implements a distinction between closed terms (called processes [36, p. 14]) and open terms, based on binding operators (input and recursion).

Most of the time, and since the origin of the calculus of communicating systems, the theory starts by considering only programs-"closed behaviour expression[s], i.e. ones with no free variable" [54, p. 73]when comparing terms, as-exactly like in λ -calculus-they correspond to self-sufficient, well-rounded programs: it is generally agreed upon that open terms should not be released "into the wild", as they are not able to remain in control of their internal variables, and can be subject to undesirable or uncontrolled interferences. Additionally, closed terms are also the only ones to have a reduction semantics, which means that they can evolve without interacting with the environment-this would corresponds, in Java, to being wrapped, i.e. inserted into a proper header and ready to be used or tested.

However, in concurrent calculi, the central notions of binders and of variables have been changing, and still seem today sometimes "up in the air". For instance, in the original CCS, restriction was not a binder [54, p. 68], and by "refusing to admit channels as entities distinct from agents" [57, p. 16] and defining two different notions of scopes [57, p. 18], everything was set-up to produce a long and recurring confusion as to what a "closed" term meant in CCS. In the original definition of π-calculus [START_REF] Milner | A Calculus of Mobile Processes[END_REF][START_REF] Milner | A Calculus of Mobile Processes[END_REF], there is no notion of closed terms, as every (input) binding on a channel introduces a new and free occurrence of a variable. However, the language they build upon-ECCS [START_REF] Engberg | A calculus of communicating systems with label passing -ten years after[END_REF]-made this distinction clear, by separating channel constants and variables.

Once again in an attempt to mimic the "economy" [58, p. 86] of λ -calculus, but also taking inspiration from the claimed "monotheism" of the actor model [START_REF]Actor Induction and Meta-Evaluation[END_REF], different notions such as values, variables, or channels have been united under the common terminology of "names". This is at times identified as a strength, to obtain a "richer calculus in which values of many kinds may be communicated, and in which value computations may be freely mixed with communications." [59, p. 20] However, it seems that a distinction between those notions always needs to be carefully re-introduced when discussing technically the language [8, p. 258, Remark 493], extensions to it [1, p. 4] or possible implementations [16, p. 13, 31]. Finally, let us note that extensions of π-calculus can sometimes have different binders, as e.g. output binders are binding in the private π-calculus [67, p. 113].

In the λ -calculus, being closed is what makes a term "ready to be executed in an external environment". But in concurrent calculi, being a closed term-no matter how it is defined-is often not enough, as it is routine to exclude e.g. terms with un-guarded operators like sum [79, p. 416] or recursion [57, p. 166]. However, these operators are sometimes not excluded from the start, even if they can never be parts of tested terms. The usual strategy [START_REF] Amadio | Operational methods in semantics[END_REF]Remark 414,[START_REF] Milner | Communication and Concurrency[END_REF]is often to keep them "as long as possible", and to exclude them only when their power cannot be tamed any more to fit the framework or prove the desired result, such as the preservation of weak bisimulation by all contexts.

In our opinion, the right distinction is not about binders of free variables, but about the role played by the syntactic objects in the theory. As "being closed" is 1. not always well-defined, or at least changing, 2. sometimes not the only condition, we would like to use the slightly more generic adjectives complete and incomplete-wrapped or not, in our Java terminology. Process algebras generally study terms by 1. completing them if needed, 2. inserting them in an environment, 3. executing them, 4. observing them thanks to predicates on the execution ("terminates", "emitted the barb a", etc.), hence constructing equivalences, preorders or metrics [START_REF] Horita | A Metric Semantics for the π-Calculus Extended with External Events[END_REF] on them. Often, the environment is essentially made of another process composed in parallel with the one studied, and tweaked to improve the likeliness of observing a particular behavior: hence, we would like to think of them as tests that the observed systems has to pass, justifying the terminology we will be using.

Processes are "partial" programs, still under development; sometimes called "open terms", they correspond to incomplete terms. They would be called code fragments, or snippets, in standard programming.

Systems are "configured processes", ready to be executed in any external environment: sometimes called "closed terms", they correspond to complete terms. They would be functions shipped with a library in standard programming, and ready to be executed.

Tests are defined using contexts and observations, and aims at executing and testing systems. They would be main methods calling a library or an API in standard programming, along with a set of observables.

Our terminology is close to the one used e.g. in ADPI [START_REF] Hennessy | A distributed Pi-calculus[END_REF]Chapter 5] or mobile ambients [52, Table 1], which distinguish processes and systems. In the literature of process algebra, the term "process" is commonly used to denote these three layers, possibly generating confusion. We believe this usage comes from a strong desire to keep the three layers uniform, using the same name, operators and rules, but this principle is actually constantly dented (as discussed in Sect. 4), for reasons we expose below.

Designing Layered Concurrent Languages

Concurrent languages could benefit from this organization from their conception: Define processes The first step is to select a set of operators called construction operators, used by the programmer to write processes. Those operators should be expressive, easy to combine, with constraints as light as possible, and selected with the situation that is being modeled in mind-and not depending on whenever they fare well with not-yet-defined relations, as it is often done to privilege the guarded sum over the internal choice. To ease their usage, a "meta-syntax" can be used, something that is generally represented by the structural equivalence. (Another interesting approach is proposed in "the π-calculus, at a distance" [4, p. 45], that bypasses the need for a structural equivalence without losing the flexibility it usually provides.)

Define deployment criteria How a process can become a system ready to be executed and tested should then be defined as a series of conditions on the binding of variables, the presence or absence of some construction operators at top-level, and even the addition of deployment operators, marking the process as ready to be deployed in an external environment 4 . Having a set of deployment operators that restricts, expands or intersects with the set of construction operators is perfectly acceptable, and it should enable the transformation of processes into systems and their composition.

Define tests

The last step requires to define 1. a set of testing operators, 2. a notion of environment constructed from those operators, along with instructions on how to place a system in it, 3. a system of reduction rules regimenting how a system can execute in an environment, 4. a set of observables, i.e. a function from systems in environments to a subset of a set of atomic proposition (like "emits barb a", "terminates", "contains recursion operator", etc.).

Observe that each step uses its own set of operators and generates its own notion of context-to construct, to deploy, or to test. Tests would be key in defining notions of congruence, that would likely be reduction-closed, observational contextually-closed relations. Determining if tests should wrap processes into systems or if that should be done ahead of the test itself resonates with a long-standing debate in process algebra, and is discussed in Sect. 9.2. Note that compared to how concurrent languages are generally designed, our approach is refined along two axis: 1. every step previously exposed allows the introduction of novel operators, 2. multiple notions of systems or tests can and should co-exist in the same process algebra.

Addressing Existing Issues

In the process algebras literature, processes and systems often have the same structure as tests and all use the same operators and contexts, to preserve and nurture a supposedly required simplicity-at least on the surface of it. But actually, we believe that the distinction we offer is constantly used "under the hood", without always a clear discussion, but that it captures and clarifies some of the choices, debates, improvements and explanations that have been proposed. One could even imagine having a series of "contexts and observations lemmas" illustrating how certain observations can be simulated by some operators, or reciprocally.

Co-defining observations and contexts

Justifying the "silent" transition's treatment It is routine to define relations (often called "weak") that ignore silent (a.k.a. τ-) transitions, seen as "internal". This sort of transitions was dubbed "unobservable internal activity" [36, p. 6] and sometimes opposed to "externally observable actions" [77, p. 230].

While we agree that "[t]his abstraction from internal differences is essential for any tractable theory of processes" [57, p. 3], we would also like to stress that both can and should be accommodated, and that "internal" transition should be treated as invisible to the user, but should still be accessible to the programmer when they are running their own tests.

The question "to what extent should one identify processes differing only in their internal or silent actions?" [15, p. 6] is sometimes asked, and discussed as if it was a property of the process algebra and not something that can be internally tuned when needed. We argue that the answer to that question is "it depends who is asking!": from a user perspective, internal actions should not be observed, but it makes sense to let a programmer observe them when testing to help in deciding which process to prefer based on information not available to users.

Letting multiple comparisions co-exist

The discussion on τ-transitions resonates with a long debate on which notion of behavioral relation is the most "reasonable", and-still recently-a textbook can conclude a brief overview of this issue by "hop[ing] that [they] have provided enough information to

[their] readers so that they can draw their own conclusions on this long-standing debate" [77, p. 160]. Sometimes, a similar question is phrased in terms of choosing the right level of abstraction to obtain meaningful language comparisons [48, Section 3]. We firmly believe that the best answer to both questions is to acknowledge that different relations and comparisons tools match different needs, and that there is no "one size fits all" answer for the needs of all the variety of testers. Of course, comparing multiple relations is an interesting and needed task [START_REF] Fournet | A hierarchy of equivalences for asynchronous calculi[END_REF][START_REF] Van Glabbeek | The Linear Time -Branching Time Spectrum II[END_REF], but one should also state that multiple comparison tools can and should co-exist, and such vision will be encapsulated by the division we are proposing.

Embracing a feared distinction The distinction between our notions of processes and systems is rampant in the literature, but too often feared, as if it was a parenthesis that needed to be closed to restore some supposedly required purity and uniformity of the syntax. A good example is probably given by mobile ambients [START_REF] Merro | Behavioral theory for mobile ambients[END_REF]. The authors start with a two-level syntax that distinguishes between processes and systems [52, p. 966 The authors even extend further the syntax for processes with a special • operator [52, p. 971, Definition 3.1], and note that the equivalences studied will not consider this additional constructor: we can see at work the distinction we sketched, where operators are added and removed based on different needs, and where the language needs not to be monolithic. The authors furthermore introduce two different reduction barbed congruences [52, p. 969, Definition 2.4]-one for systems, and one for processes, with different notions of contexts-but later on prove that they coincide on systems [52, p 989, Theorem 6.10]. It seems to us that the distinction between processes and systems was essentially introduced for technical reasons, but that re-unifying the syntax-or at least prove that systems do not do more than processes-was a clear goal right from the start. We believe it would have been fruitful to embrace this distinction in a framework similar to the one we sketched: while retaining the interesting results already proven, maintaining this two-level syntax would allow to make a clearer distinction between the user's and the programmer's roles and interests, and assert that, sometimes, systems can and should do more than processes-for instance, interacting with users!-, and can be compared using different tools.

Keeping on extending contexts

We are not the first to argue that constructors can and should be added to calculi to access better discriminatory power, but without necessarily changing the "original" language. The mismatch operator, for instance, has a similar feeling: "reasonable" testing equivalences [20, p. 280] require it, and multiple languages [2, p. 24] use it to provide finer-grained equivalences. For technical reasons [79, p. 13], this operator is generally not part of the "core" of π-calculus, but resurfaces by need to obtain better equivalences: we defend a liberal use of this fruitful technics, by making a clear separation between the construction operators-added for their expressivity-and the testing operatorsthat improve the testing capacities.

Treating extensions as different completions It would benefit their study and usage to consider different extensions of processes algebras as different completion strategies for the same construction operators. For instance, reversible [START_REF] Lanese | Static versus dynamic reversibility in CCS[END_REF] or timed [START_REF] Yi | CCS + Time = An Interleaving Model for Real Time Systems[END_REF] extensions of CCS could be seen as two completion strategiesdifferent conditions for a process to become a system-for the same class of processes, inspired from the usual CCS syntax [8, Chapter 28.1]. Those completion strategies would be suited for different needs, as one could e.g. complete a CSS process as a RCCS [START_REF] Danos | Reversible Communicating Systems[END_REF] system to test for relations such as hereditary history-preserving bisimulation [START_REF] Aubert | How Reversibility Can Solve Traditional Questions: The Example of Hereditary History-Preserving Bisimulation[END_REF], and then complete it with time markers as a safety-critical system. This would correspond to having multiple compilation, or deployment, strategies, based on the need, similar to "debug" and "real-time", versions of the same piece of software.We think also of Debian's DebugPackage, enabling generation of stack traces for any package, or of the CONFIG_PREEMPT_RT patch that converts a kernel into a real-time micro-kernel: both uses the same source code as their "casual" versions.

Obtaining fine-grained typing systems The development of typing systems for concurrent programming languages is a notoriously difficult topic. Some results in π-calculus have been solidified [79, Part III], but diverse difficulties remain. Among them, the co-existence of multiple systems for e.g. session types [START_REF] Bas Van Den | Session Type Systems based on Linear Logic: Classical versus Intuitionistic[END_REF], the difficulty to tie them precisely to other type systems as Linear Logic [START_REF] Caires | Linear logic propositions as session types[END_REF], and the doubts about the adaptation of the "proof-as-program" paradigm in a concurrent setting [START_REF] Beffara | Proofs as executions[END_REF], make this problem active and diverse. The ultimate goal seems to find a typing system that would accommodate different uses and scenarios that are not necessarily comparable.

Using our proposal, one could imagine easing this process by developing two different typing systems, one aimed at programmers-to track bugs and produce meaningful error messages-and one aimed at users-to track security leaks or perform user-input validation. Once again, having a system developed along the layers we recommend would allow to have e.g. a type system for processes only, and to erase the information when completing the process, so that the typing discipline would be enforced only when the program is being developed, but not executed. This is similar to arrays of parameterized types in Java [66, pp. 253-258], that checks the typing discipline at compilation time, but not at run-time.

While this series of examples and references illustrates how our proposal could clarify pre-existing distinctions, we would like to stress that 1. nothing prevents from collapsing our distinction when it is not needed, 2. additional progresses could be made using it, as we sketch in the next section.

Exploiting Context Awareness

We would like to sketch below some possible exploitations of our frame that we believe could benefit the study and expressivity of some popular concurrent languages.

For CCS, we sketch below two possible improvements, the second being related to security. Testing for auto-concurrency Auto-concurrency (a.k.a. auto-parallelism) is when a system has two different transitions-leading to different states-labeled with the same action [64, p. 391 on the right, where the label of the event executed is on the edge and configurations are represented with •. Non-interleaving models of concurrency [START_REF] Vladimiro Sassone | Models for Concurrency: Towards a Classification[END_REF] distinguishes between them, as "true concurrency models" would. / 0

• • • a b a b / 0 • • • • a b a b
Some forms of "back-and-forth-bisimulations" cannot discriminate between them if a = b [START_REF] Phillips | Reversibility and Models for Concurrency[END_REF]. While not being able to distinguish between those two terms may make sense from an external-user's-point of view, we argue that a programmer should have access to an internal mechanism that could answer the question "Can this process perform two barbs with the same label at the same time?". Such an observation-possibly coupled with a testing operator-would allow to distinguish between e.g. !a.P |!a.P and !a.P, that are generally taken to be bisimilar, and would re-integrate auto-concurrent systems-that are, after all, unjustifiably excluded-in the realm of comparable systems.

Representing man-in-the-middle One could add to the testing operators an operator ∇a.P, which would forbid P to act silently on channel a. This novel operator would add the possibility for the environment to "spy" on a determined channel, as if the environment was controlling (part of) the router of the tested system. One could then reduce "normally" in a context ∇a[ ] if the channel is still secure:

∇a(b.Q | b.P) → τ ∇a(Q | P) (If a = b)
But in the case where a = b, the environment could intercept the communication and then decide to forward, prevent, or alter it. Adding this operator to the set of testing operators would for instance open up the possibility of interpreting νa(P) as an operation securing the channel a in P, enabling the study of relations ∼ that could include e.g. While the first rule enforces that, once secured, channel names are α-equivalent (the process can decide to migrate to a different channel without being spied on), the second illustrates that, once a channel is tapped, a process cannot obtain any confidentiality on it anymore.

In π-calculus, all tests are instantiating contexts (in the sense that the term tested needs to be either already closed, or to be closed by the context), and all instantiating contexts use only construction operators, and hence are "construction contexts". This situation corresponds to Situation A in Figure 1.

We believe the picture could be much more general, with tests having access to more constructors, and not needing to be instantiating-in the sense that completion can be different from closedness-, so that we would obtain Situation B in Figure 1. While we believe this remark applies to most of the process algebras we have discussed so far, it is particularly salient in π-calculus, where the match and mismatch operators have been used "to internalize a lot of meta theory" [32, p. 57], standing "inside" the "Construction operators" circle while most authors seem to agree that they would prefer not to add it to the internals of the language 5 . It should also be noted that the mismatch operator-in its "intuitionistic" version-furthermore "tried to escape the realm of instantiating contexts" by being tightly connected [START_REF] Horne | Quasi-Open Bisimilarity with Mismatch is Intuitionistic[END_REF] to quasi-open bissimilarities [78, p. 300, Definition 6], which is a subtle variation on how substitutions can be applied by context to the terms being tested. Having a notion of "being complete" not requiring closedness could be useful when representing distributed programming, where "one often wants to send a piece of code to a remote site and execute it there. [. . . ] [T]his feature will greatly enhance the expressive power of distributed programming[ by ] send [ing] an open term and to make the necessary binding at the remote site." [35, p. 250] We believe that maintaining the possibility of testing "partially closed"-but still complete-terms would enable a more theoretical understanding of distributed programming and remote compilation.

Distributed π-calculus, could explore the possible differences between two parallelisms: between threads in the same process-in the Unix sense-and between units of computation. Such a distinction could be rephrased thanks to two parallel operators, one on processes and the other on systems. Such a distinction would allow to observationally distinguish e.g. the execution of a program with two threads on a dual-core computer and the execution of two single thread programs on two single-core computers.

For cryptographic protocols, we could imagine representing encryption of data as a special context E [ ] that would transform a process P into an encrypted system E [P], and make it un-executable unless "plugged" in an environment D[ ] that could decrypt it. This could allow the applied π-calculus [START_REF] Abadi | The Applied Pi Calculus: Mobile Values, New Names, and Secure Communication[END_REF] to become more expressive and to be treated as a decoration of the pure π-calculus more effectively. This could also, as the authors wish, make "the formalization of attackers as contexts [. . . ] continue to play a role in the analysis of security protocols" [1, p. 35].

Recent progresses in the field of verification of cryptographic protocols [START_REF] Baelde | Contributions à la Vérification des Protocoles Cryptographiques[END_REF] hinted in this direction as well. By taking "[t]he notion of test [to] be relative to an environment" [12, p. 12], a formal development involving "frames" [12, Definition 2.3] can emerge and give flesh to some ideas expressed in our proposal.

It should be noted that this work also "enrich[. . . ] processes with a success construct" [12, p. 12], that cannot be used to construct processes, to construct "experiments".

Concluding Remarks

We conclude by discussing related approaches, by casting a new light on a technical issue related to barbed congruences, by offering the context lemmas a new interpretation, and by coming back to our motivations.

An Approved and Promising Perspective

We would like to stress that our proposal resonates with previous comments, and should not be treated as an isolated historical perspective that will have no impact on the future.

In the study of process algebras, in addition to the numerous hints toward our formalism that we already discussed, there are at least two instances when the power of the "testing suite" was explicitly discussed [START_REF] Sangiorgi | Introduction to Bisimulation and Coinduction[END_REF]Remark 5.2.21]. In a 1981 article, it is assumed that "by varying the ambiant ('weather') conditions, an experimenter" [55, p. 32] can observe and discriminate better than a simple user could. Originally, this idea seemed to encapsulate two orthogonal dimensions: the first was that the tester could run the tested system any number of times, something that would now be represented by the addition of the replication operator ! to the set of testing operators. The second was that the tester could enumerate all possible non-deterministic transitions of the tested system. This second dimension gave birth to "a language for testing concurrent processes" [49, p. 1] that is more powerful than the language used to write the programs being tested. In this particular example, the tester has access to a termination operator and probabilistic features that are not available to the programmer: as a result, the authors "may distinguish non-bisimilar processes through testing" [49, p. 19].

Looking forward, the vibrant field of secure compilation made a clear-cut distinction between "target language contexts" representing adversarial code and programmers' "source context" to explore property preservation of programs [START_REF] Abate | Journey Beyond Full Abstraction: Exploring Robust Property Preservation for Secure Compilation[END_REF]. This perspective was already partially at play in the spi calculus for cryptographic protocols [2, p. 1], where the attacker is represented as the "environment of a protocol". We believe that both approaches-coming from the secure compilation, from the concurrency community, but also from other fields-concur to the same observation that the environment-formally captured by a particular notion of context-deserves an explicit and technical study to model different interactions with systems, and need to be detached from "construction" contexts.

When Should Contexts Come into Play?

The interesting question of when to use contexts when testing terms [79, pp. 116-117, Section 2.4.4] raises a technical question that is put under a different perspective by our analysis. Essentially, the question is whether the congruences under study should being defined as congruences (e.g. reduction-closed barbed congruence [79, p. 116]), or being defined in two steps, i.e. as the contextual closure of a pre-existing relation (e.g. strong barbed congruence [79, p. 61, Definition 2.1.17], which is the contextual closure of strong barbed bisimilarity [79, p. 57, Definition 2.1.7])?

Indeed, bisimulations can be presented as an "interaction game" [START_REF] Stirling | Modal and Temporal Logics for Processes[END_REF] generally played as 1. Pick an environment for both terms (i.e., complete them, then embed them in the same testing environment), 2. Have them "play" (i.e. have them try to match each other's step). But a more dynamic version of the game let picking an environment be part of the game, so that each process can not only pick the next step, but also in which environment it needs to be performed. This version of the game, called "dynamic observational congruence" [START_REF] Montanari | Dynamic congruence vs. progressing bisimulation for CCS[END_REF], provides a better software modularity and reusability, as it allows to study the similarity of terms that can be re-configured "on the fly". Embedding the contexts in the definitions of the relations is a strategy that was also used to obtain behavioral characterization of theories [START_REF] Honda | On Reduction-Based Process Semantics[END_REF]p. 455,Proposition 3.24], and that corresponds to open bisimilarities [START_REF] Sangiorgi | A Theory of Bisimulation for the pi-Calculus[END_REF]p. 77,Proposition 3.12] Those two approaches have been extensively compared and studied-still are [1, p. 24]-but to our knowledge they rarely co-exist, as if one had to take a side at the early stage of the language design, instead of letting the tester decide later on which approach is best suited for what they wish to observe. We argue that both approaches are equally valid, provided we acknowledge they play different roles.

This question of when are the terms completed? can be rephrased as what is it that you are trying to observe?, or even who is completing them?: is the completion provided by the programmer, once and for all, or is the tester allowed to explore different completions and to change them as the tests unfold? Looking back at our Java example from Sect. 2, this corresponds to letting the tester repeatedly tweak the parameter or return type of the wrapping from int to long, allowing them to have finer comparisons between snippets. In this frame, moving from the static definition of congruence to dynamic one would 1. Playing on the variation "should I complete the terms before or during their comparison?" is not simply a technical question, but reflects a choice between two different situations equally interesting.

2. This choice can appeal to different notions of systems, completions and tests: for instance, while completing a process before testing it (Situation A) may indeed be needed when the environment represents an external deployment platform, it makes less sense if we think of the environment as part of the development workflow, in charge of providing feedback to the programmer or as a powerful attacker than can manipulate the conditions in which the process is executed (Situation B).

If completion is seen as compilation, this opens up the possibility of studying how the bindings performed by the user, on their particular set-up, during a remote compilation, can alter a program. One can then compare different relations-some comparing source code's releases, some comparing binaries' releases-to get a better, fuller, picture of the program.

Penetrating Context Lemmas' Meanings

What is generally refereed to as the context lemma6 is actually a series of results stating that considering all the operators when constructing the context for a congruence may not be needed. For instance, it is equivalent to define the barbed congruence [79, p. 95, Definition 2.4.5] as the closure of barbed bisimilarity under all context, or only under contexts of the form [ ]σ | P for all substitution σ and term P. In its first version [72, p. 432, Lemma 5.2.2], this lemma had additional requirements e.g. on sorting contexts, but the core idea is always the same: "there is no need to consider all contexts to determine if a relation is a congruence, you can consider only contexts of a particular form".

The "flip side" of the context lemma is what we would like to call the "anti-context pragmatism": whenever a particular type of operator or context prevents a relation from being a congruence, it is tempting to simply exclude it. For instance, contexts like [ ]+0 are routinely removed-as we discussed in Sect. 4to define the barbed congruence of π-calculus, or contexts were restricted to what is called harnesses in the mobile ambients calculus [START_REF] Gordon | Equational Properties Of Mobile Ambients[END_REF] Taken together, those two remarks produce a strange impression: while it is mathematically elegant and interesting to prove that weaker conditions are enough to satisfy an interesting property, it seems to us that this result is sometimes "forced" into the process algebra by having ahead of time excluded all the operators that would not fit, hence producing a result that is not only weaker, but also somehow artificial, or even tautological. Furthermore the criteria of "not adding any discriminating power" should not be a positive criterion when deciding if a context belongs to the algebra: on the opposite, one would want contexts to increase the discriminating power-as for the mismatch operator-and not to "conform" to what substitution and parallel composition have already decided.

Context lemmas seem to embrace an uncanny perspective: instead of being used to prove properties about tests more easily, they should be considered from the perspective of the ease of use of testing systems. Stated differently, we believe that the set of testing operators should come first, and then then, if the language designer wishes to add operators to ease the testers' life, they can do so providing they obtain a context lemma proving that those operators do not alter the original testing capacities. Once again, varying the testing suite is perfectly acceptable, but once fixed, the context lemma is simply present to show that adding some testing operators is innocent, that it will simply make testing certain properties easier.

Embracing the Diversity

Before daring to submit a non-technical paper, we tried to conceive a technical construction that could convey our ideas. In particular we tried to build a syntactic (even categorical) meta-theory of processes, systems and tests. We wanted to define congruences in this meta-theory, and to answer the following question: what could be the minimal requirements on contexts and operators to prove a generic form of context lemma for concurrent languages?

However, as the technical work unfolded, we realized that the definitions of contexts, observations, and operators, were so deeply interwoven that it was nearly impossible to extract any general or useful principle. Context lemmas use specific features of languages, in a narrow sense, as for instance no context lemma can exist in the "Situation B" of Figure 2 [79, p. 117], and we were not able to find a unifying framework. This also suggests that context lemmas are often fit for particular process algebras by chance, and dependent intrinsically of the language considered, for no deep reasons.

This was also liberating, as all the nuances of languages we had been fighting against started to form a regular pattern: every single language we considered exhibited (at least parts of) the structure we sketched in the present proposal. Furthermore, our framework was a good lens to read and answer some of the un-spoken questions suggested in the margin or the footnotes-but rarely upfront-of the multiple research papers, lecture notes and books we consulted. So, even without mathematical proofs, we consider this contribution a good way of stirring the community, and to question the traditional wisdom.

It seems indeed to us that there is nothing but benefits in altering the notion of context, as it is actually routine to do so, even recently [START_REF] Hirschkoff | On the Representation of References in the Pi-Calculus[END_REF], and that stating the variations used will only improve the expressiveness of the testing capacities and the clarity of the exposition.

It is a common trope to observe the immense variety of process calculi, and to sometimes wish there could be a common formalism to capture them all-to this end, the π-calculus is often considered the best candidate. Acknowledging this diversity is already being one step ahead of the λ -calculus-that keeps forgetting that there is more than one λ -calculus, depending on the evaluation strategy and on features such as sharing [START_REF] Accattoli | A Fresh Look at the lambda-Calculus (Invited Talk)[END_REF]-and this proposal encourages to push the decomposition into smaller languages even further, as well as it encourages to see whole theories as simple "completion" of standard languages. As we defended, breaking the monolithic status of context7 will actually make the theory and presentation follow more closely the technical developments, and liberate from the goal of having to find the process algebra with its unique observation technique that would capture all possible needs.

Postscript

The tone and scope of this essay may seem "timeless", but discussions during the 14th Interaction and Concurrency Experience (particularly with Alceste Scalas and Emilio Tuosto) and with colleagues (among which David Baelde and Ross Horne) finished anchoring it to very concrete and timely questions. We would like to briefly sketch a handful of future themes, hoping to faithfully record the fascinating discussions that led to them.

1. Semantical approaches to security revealed multiple small gaps that are hard to explain or solve with usual notions of contexts and equivalences. For instance, the study of equivalence properties led to distinguish between semantics where all the communications have to be made via the environment (i.e., the attacker) and semantics where communications inside the process and communications between the process and its environment are treated differently. The (surprising) result [START_REF] Babel | On the semantics of communications when verifying equivalence properties[END_REF] is that while both treatments coincide for reachability properties, they are incomparable for indistinguishability properties. The resulting classical, private and eavesdropping semantics each yield their own may-testing and observational equivalences, that could possibly be elegantly captured by our frame. The interested reader should refer to a recent discussion [START_REF] Baelde | Contributions à la Vérification des Protocoles Cryptographiques[END_REF]Section 4.1.6] for more insight on this issue.

2. Our discussion could also be used to bridge possible gaps between process algebras and game semantics, or at least introduce a gradation between them. Indeed, while "usual" algebraic contexts are extremely passive and with limited (static) knowledge of the term placed inside of them, strategies generally have all laterality to evolve, and to store information about the play unfolding.

We would like to argue, following a classical paper [START_REF] Laird | A Game Semantics of the Asynchronous π-Calculus[END_REF]Section 5], that maybe processes (or, in our case, contexts) could represent strategies, and that there could be a gradation in the "dynamicity" of contexts: from very statical ones to more dynamical and reactive ones. This could be used e.g. to study the open barbed bisimilarity between processes with free variables, by allowing contexts to use and retain information about permitted submissions.

3. Reversible CCS (RCCS) [START_REF] Danos | Reversible Communicating Systems[END_REF] and CCS with keys (CCSK) [START_REF] Phillips | Reversing Algebraic Process Calculi[END_REF] are two extensions to CCS aiming at formalizing reversible concurrent computation. They have been compared and studied, but, as it turns out, they actually are the two faces of the same coin [START_REF] Lanese | Static versus dynamic reversibility in CCS[END_REF]. However, when defining contexts, and despite the similarities in the definitions, two recent studies [START_REF] Aubert | Explicit Identifiers and Contexts in Reversible Concurrent Calculus[END_REF][START_REF] Lanese | Forward-Reverse Observational Equivalences in CCSK[END_REF] came to exactly opposite conclusions: while the RCCS-inspired system seems to provide definitive evidence that no relation can be a congruence if the context can change the history of the process [10, Theorem 2], the

  Originally, the barb was a predicate[61, p. 690], whose definition was purely syntactic. Probably inspired by the notion of observer for testing equivalences[25, p. 91], an alternative definition was made in terms of parallel composition with a tester process [50, p. 10, Definition 2.1.3]. This illustrates perfectly how the set of observables and the notion of context are inter-dependent, and that tests should always come with a definition of observable and a notion of context: we believe our proposal could help in clarifying the interplay between observations and contexts.

  ∇a(νa(P|Q) ∼ ∇a(νb(P[a/b]|Q[a/b])) (For b not in the free names of P nor Q) νa(∇a(P|Q)) ∼ ∇a(P|Q) (Uselessness of securing a hacked channel)

Figure 1 :

 1 Figure 1: Opening up the testing capacities of π-calculus

Figure 2 :

 2 Figure 2: Distinguishing between completing strategies

  solvable terms [13, p. 171, 8.3.1 and p. 416, 16.2.1].

  before proving such results. As strong bisimulation[68, p. 514, Definition 1] is not preserved by input prefix [68, p. 515, Proposition 4] but is by all the other operators, it is sometimes tempting to simply remove input prefix from the set of constructors allowed at top-level in contexts, which is what non-input contexts [79, p. 62, Definition 2.1.22] do, and then to establish a context lemma for this limited notion of context.

To re-use in our setting Paul Taylor's witty comment[START_REF] Taylor | Comment to "Substitution is pullback[END_REF].

Actually, if application, abstraction and variables all count as one, the ratio between normal term and term with redexes is unknown[17]. We imply here "since most interesting terms", in the sense of terms that represent programs.

As a reviewer noted, "Proving a behavioural equivalence is a congruence has a reading that is somewhat left out of the discussion in the paper. Namely, the behavioural equivalence provides a mathematical notion of behaviour and showing such

Exactly like a Java method header can use keywords-extends, implements, etc.-that cannot be used in a method body.

To be more precise: while "most occurences of matching can be encoded by parallel composition [. . . ,] mismatching cannot be encoded in the original π-calculus"[69, p. 526], which makes it somehow suspicious.

At least, in process algebra, as the same name is used for a different type of meaning in e.g. λ -calculus[53, p. 6].

This may be a good place to mention that this monolithicity probably comes in part from the original will of making e.g. CCS a programming and specification language-an original perspective that was reminded to us by Ilaria Castellani, who we wish to thank. The specification was supposed to be the program itself, that would be easy to check for correctness: the goal was to make it "possible to describe existing systems, to specify and program new systems, and to argue mathematically about them, all without leaving the notational framework of the calculus"[56, p. 1]. This original research project slightly shifted-from specifying programs to specifying behaviors-but that original perspective remained.

Processes, Systems & Tests

Acknowledgements

The author wish to thank the organizer of ICE 2021 for organizing this welcoming, open workshop, as well as the reviewers who kindly shared their comments, suggestions and insights with us. This paper benefited a lot from them, as well as from the discussions mentioned in Sect. 10.

CCSK approach came to the conclusion that a particular barbed bisimilarity was a congruence [START_REF] Lanese | Forward-Reverse Observational Equivalences in CCSK[END_REF]Corollary 5.12]. Does the difference rest only on the definition of context, or is there a more subtle distinction at work? It is our hope that the approach sketched here could help to solve this mystery.

Last but not least, an "easy" exercise to illustrate the relevance of our perspective would be to study a Morris-style equivalence of the programming language Java, using the convenient, "simplified", Featherweight Java [START_REF] Igarashi | Featherweight Java: A Minimal Core Calculus for Java and GJ[END_REF]. It is our hope that this lead, on which we will be working in the near future, will fruitfully illustrate the benefits of the distinction we detailed in this paper.