1.2.1 Mobile Ambients

Ambient calculi were proposed by Cardelli and Gordon in Mobile Ambients (MA) (Cardelli and Gordon, Reference Cardelli and Gordon2000). The very first purpose of this kind of calculi is to capture the feature of concurrent computation with explicit location boundary. For example, $a[P]$ stands for an ambient named $a$ with process $P$ running inside. Indeed, MA describe mobile computation within a hierarchical framework (i.e., tree structure), which structures the processes with respect to locations and allows them to move under control. Such control is implemented by three capabilities in MA: entry (in-movement), exit (out-movement), and open (absorption). In addition, ambients can communicate, and the communication happens inside ambients (i.e., locally) in an anonymous manner. The capabilities and the local anonymous communication can be exemplified by the following reductions:

\begin{equation*} \begin{array}{lr} a[in\; b.P \,|\, Q] \,|\, b[R]\rightarrow b[a[P\,|\, Q] \,|\, R] \qquad \qquad & \mbox {in-movement} \\ b[a[out\; b.P \,|\, Q]\,|\, R]\rightarrow a[P\,|\, Q]\,|\, b[R] \qquad & \mbox {out-movement} \\ open\; a.P\,|\, a[Q]\rightarrow P\,|\, Q \qquad & \mbox {open} \\ a[(X)P \,|\, Q \,|\, \langle M \rangle \,|\, R] \rightarrow a[P\{M/X\} \,|\, Q \,|\, R] \qquad & \qquad \mbox {communication} \end{array} \end{equation*}

In the first reduction, ambient $a$ moves into ambient $b$ with the help of the capability $in\; b$ . The relative position of the two ambients changes from sibling to parent-child (i.e., $a$ becomes part of $b$ ). In the second reduction, ambient $a$ moves out of $b$ with the help of the capability $out\; b$ . The relative position of the two ambients changes from parent-child to sibling (i.e., $a$ is now on the same level as $b$ ). The third reduction permits dissolving the boundary of ambient $a$ , whose content becomes part of the surrounding environment (here involving $P$ ). The last reduction represents a communication inside ambient $a$ , where $\langle M \rangle$ delivers the resource $M$ , and $(X)P$ reads $M$ and continues as $P$ in which every occurrence of the variable $X$ is instantiated as $M$ .

The design of the movement in MA is quite simple and easy to understand. The control is monolateral; that is, only one side of the interacting ambients has full control. Though quite prototypical, the formulation of the ambient calculus is of great referential significance to upfront works, including the syntax, reduction-based semantics, and (barbed) bisimulation thereof.

1.2.2 Safe Ambients

Safe Ambients (SA) (Levi and Sangiorgi, Reference Levi and Sangiorgi2003; Merro and Hennessy, Reference Merro and Hennessy2006) are a variant of the original MA that strengthens the control of ambient movements to resolve the interference issue as one primary purpose. Every action of the entering, exiting, and opening of an ambient is no longer arbitrary and takes place on the agreement of both participants of the action. To be more specific, an action of an ambient now needs a coaction to enable interaction, that is, $\overline {in},\;\overline {out},\;\overline {open}$ , respectively, for paring with $in,\; out,\; open$ . For example, the following movements exhibit the situation of the three capabilities that have the same intuitive meaning as those in MA:

\begin{equation*} \begin{array}{lr} a[in\; b.P_1 \,|\, P_2 ] \,|\, b[\overline {in}\; b.Q_1|Q_2]\rightarrow b[a[P_1\,|\, P_2]\,|\, Q_1\,|\, Q_2] \qquad \qquad \qquad & \mbox {in-movement} \\ b[a[out\; b.P_1\,|\, P_2]|\overline {out}\; b.Q_1\,|\, Q_2]\rightarrow a[P_1\,|\, P_2]\,|\, b[Q_1\,|\, Q_2] \qquad \qquad \qquad & \mbox {out-movement} \\ open\; a.P\,|\, a[\overline {open}\; a.Q_1\,|\, Q_2]\rightarrow P\,|\, Q_1\,|\, Q_2 \qquad \qquad \qquad & \mbox {open} \end{array} \end{equation*}

SA are somewhat more robust in control without reducing the expressiveness of MA, and most of the properties of MA can be adapted to SA. However, the change in moving primitives leads to more difficulty in proving properties like congruence and coincidence between labeled transition system (LTS)-based bisimulation and reduction-based barbed congruence. To make SA more tractable in these properties, SA with passwords were proposed (Merro and Hennessy, Reference Merro and Hennessy2006), where a password is some information attached to the capabilities to enhance the control power further so that the desirable properties can be achieved. In these variants of MA, however, no HO communications are considered.

1.2.3 Boxed Ambients

Boxed Ambients (BA) (Bugliesi et al., Reference Bugliesi, Castagna and Crafa2001) are a variant of MA that removes the open capability (which is deemed overly powerful) and introduces more versatile communication methods. Such communications are still anonymous; that is, no explicit channels are declared. More specifically, the mobility in BA is inherited from MA (e.g., entering and exiting) with the same semantics, so it preserves the computational properties of MA. BA rely on different communication models, resulting from dropping the open capability. The communications in BA can be local as in MA (or its similar variants) or across ambient boundaries anonymously. In Bonelli et al. (Reference Bonelli, Compagnoni, Dezani-Ciancaglini and Garralda2007), BA are extended with a type system aiming at providing explicitly flexible communication policy, that is, directed input/output operations. In that way, BA enhance the flexibility of typed communications over MA and provide important observations for the relationship between synchronous and asynchronous input/output. Although in Bonelli et al. (Reference Bonelli, Compagnoni, Dezani-Ciancaglini and Garralda2007), the communication channels are not hidden as in the original BA, the aim of that work is different from this work, mainly in that we are more interested in the basic communication mechanism between ambients without typing assertion.

1.2.4 Fair Ambients

FA (Fu, Reference Fu2007) are built on several principles that rebase the semantics of ambients on top of a corresponding LTS, which further reshapes the previous ambient calculi concerning fairness to be glossed over shortly. A central design idea is that the elementary participants of interaction should be ambients themselves rather than part of them (e.g., a moving prefix or a process not residing in any ambient). Meanwhile, the interaction between ambients must be peer to peer, in other words, equally positioned or even displaced. For example, in the out-moving, the ambient that is called out should be explicitly informed who is doing this. This is what “fair” means. Our model in this work, as somewhat an extension of FA, also adheres to this principle of fairness. More specifically, the semantical rules for the capabilities are exemplified as follows. Following the original formulation in (Fu, Reference Fu2007), we use $\tau$ for an interaction:

\begin{equation*} \begin{array}{lr} b[in\; a.Q\,|\, N]\,|\, a[\overline {in}\; b.P\,|\, L] \xrightarrow {\tau } a[b[Q\,|\, N]\,|\, P\,|\, L] \qquad \qquad \qquad & \mbox {in-movement} \\ a[c[out\; b.Q\,|\, O]\,|\, L]\,|\, b[\overline {out}\; a.P\,|\, N] \xrightarrow {\tau } a[L]\,|\, c[Q\,|\, O]\,|\, b[P\,|\, N] \qquad \qquad \qquad & \mbox {out-movement} \\ b[open\; a.Q\,|\, N]\,|\, a[\overline {open}\; b.P\,|\, L] \xrightarrow {\tau } b[P\,|\, L\,|\, Q\,|\, N] \qquad \qquad \qquad & \mbox {open} \end{array} \end{equation*}

In the in-movement, ambient $b$ is capable of entering ambient $a$ , provided that the latter is willing to give permission to the former. In the out-movement, ambient $c$ specifies from whose call (here, ambient $b$ ) it may move out of ambient $a$ , provided that ambient $b$ indeed has this request. We notice here that ambient $b$ does not explicitly indicate who inside $a$ it is requesting to exit, and thus, the out-movement is anonymous (i.e., not real identity). We will, as part of this work, revisit this mechanism. In the open operation, both ambient $a$ and $b$ know each other and authorize the other’s actions in an explicit way. Unlike previous counterparts, in FA, the open capability enables ambient $b$ to exhaust the entire internal resources of $a$ for its own interest (we often say the capability of an ambient to mean its control over the mobility of the involved ambients). The open capability is a very strong/mighty operation, which somewhat behaves like a virus, robbing the codes of another application. Due to this downside, here in this work, we drop the open capability, like in BA. Based on the operational semantics, the standard bisimilarity is studied and proven to coincide with observational bisimilarity (or barbed bisimilarity).

FA also enable FO communication, in line with the fair principle imposed on ambients, so that the two sides of a communication are equally essential and clearly controlled concerning how and with whom an ambient is exchanging messages. As shown below, ambient $a$ sends a message $c$ , being a name itself, to ambient $b$ , formalized by the action prefix $\overline {b}c$ ; correspondingly, ambient $b$ receives and prepares its use with that message $c$ from ambient $a$ , formalized by the action prefix $a(x)$ :

\begin{equation*} a[\overline {b}c.P\,|\, M] \,|\, b[a(x).Q\,|\, N] \,{\xrightarrow {\tau }}\, a[P\,|\, M] \,|\, b[Q\{c/x\} \,|\, N] \end{equation*}

As an important result on computability, Fu shows that the FO pi-calculus is a sub-calculus of FA (Fu, Reference Fu2007). The communication in FA and related works on expressiveness guide the design of HO communication in this work.

In the abovementioned works, however, no explicit HO communications are considered. A likely reason is that FO communication (if any) seems more tractable, and HO communication appears unnecessary due to the moving capacity of ambients. This is more than debatable. First, HO communication is not known to be derivable in the ambient settings. Second, programming with HO primitives can usually offer more flexibility and convenience in practice, as they appear more “direct” in interaction/computation, in contrast to address-passing. Besides, for process models without explicit (physical) locations, it is well-known that hHO processes can be implemented with FO processes, but not the other way around (Sangiorgi, Reference Sangiorgi1993; Xu, Reference Xu2012). To the best of our knowledge, the relationship between HO and FO communications is barely known in the setting of ambients. To address this, a well-established theory of HO communication for ambients has to be developed in the first place.

1.2.5 SA with (restricted) local higher-order communication

In Cao (Reference Cao2011, Reference Cao2012, Reference Cao2013), Cao studies the SA extended with local HO communication, that is, within an ambient only. Such (local) communication is not allowed between ambients, for example, parent-child or between-sibling ones, and moreover, the communication is anonymous; that is, no explicit channel names are designated. In such a setting, labeled bisimulation and barbed bisimulation are proven to be coincident, and the capability of encoding plain HO processes is established. The encoding can somewhat be thought of as transplanting HO concurrency into ambients, and similar results are presented for FO processes, that is, from FO processes to ambients capable of (anonymous) FO communication. Although not very surprising, the results provide some useful techniques for related works. It would be interesting to study more flexible HO communication, for example, those across ambients, like in BA (Bugliesi et al., Reference Bugliesi, Castagna and Crafa2001; Bonelli et al., Reference Bonelli, Compagnoni, Dezani-Ciancaglini and Garralda2007) or FA (Fu, Reference Fu2007). In turn, the possibility of encoding FO communication would be worth exploring so that, among others, the encodability of FO processes in ambients without the same communication mechanism can be demonstrated.

1.2.6 More relevant works concerning higher-order extension of ambient calculi

In Coppo and Dezani-Ciancaglini (Reference Coppo and Dezani-Ciancaglini2002), Coppo and Dezani-Ciancaglini define a model for a variant of MA with synchronous HO value-passing and a new “selfopen” primitive. The main aim of that paper is to develop a denotational model (called the filter model) for the proposed model. This model is proven to be fully abstract with respect to the contextual equivalence with the observables being ambients (names) at the top level. The filter model is associated with a sophisticated type system to achieve full abstraction. In the variant ambient calculus of Coppo and Dezani-Ciancaglini (Reference Coppo and Dezani-Ciancaglini2002), processes can be passed as values only in a local manner, that is, inside an ambient. In particular, these design decisions make it possible to establish a fully abstract filter model. In the same line, the selfopen is used to ensure full abstraction. In contrast, due to different motivations and out of distinct design principles, our ambient model does not have local HO communication or open operation. What we are more interested in here is to come by an ambient model that facilitates peer-to-peer HO communication between ambients themselves with mutual awareness of the parts involved in the interaction.

Schmitt and Stefani present the M-calculus (Schmitt and Stefani, Reference Schmitt and Stefani2003), a distributed process calculus that extends the (distributed) Join calculus (Fournet and Gonthier, Reference Fournet and Gonthier1996; Fournet et al., Reference Fournet, Gonthier, Levy, Maranget and Remy1996; Fournet Reference Fournet1998) with call-by-value HO functions, programmable localities, and dynamic binding. To strengthen the control over migration, M-calculus implements the unification of communication and process migration, by means of fine-grained ambient-like routing control whose correctness is guaranteed by a type system. A passivation operator is also defined for programming different kinds of control in terms of localities. The main purpose of Schmitt and Stefani (Reference Schmitt and Stefani2003) is to improve on the weak points of the Join calculus, for example, inadequate control over communication and mobility, lack of dynamic binding, and limited local semantics. Unlike our work, the HO communication facilitated by M-calculus is local, and the control mechanism does not consider fairness of the participants as our model does. In addition, M-calculus has an associated type system for M-processes to function correctly, which might add to the complexity of potential applications.

The Kell calculus (Kell for short) is proposed as a family of HO process calculi with ambient-like hierarchical localities (Schmitt and Stefani, Reference Schmitt and Stefani2004). The main design principles of Kell include programmable distributed membranes, dynamic binding, and local actions based on which HO communication is defined. The syntax and semantics of Kell are defined, several instances of Kell calculus are discussed, and some examples are given to illustrate the expressive power of these calculi. A notion of contextual equivalence, as well as a co-inductive characterization of the contextual equivalence (called strong context bisimulation), is studied for Kell. Kell supports various HO communications, including those within a (local) location, those crossing tree-structured hierarchies (i.e., parent-child), and even a kind called passivation that destroys the boundary of a location. Differently, the HO communication mechanism in this work permits neither local nor parent-child ones. Moreover, the control mechanism of movement and communication follows the principle of fairness, on which we rest our design of the semantics and behavioral theory.

For the sake of clarity, in what follows, we highlight the main difference of this work concerning the works above, especially about design decisions:

(1) The HO communication mechanism is quite different. Particularly in the works above, HO communication does not happen between parallel ambients on an equal hierarchical level. That is, either parent-child or local HO communication is permitted in the models proposed by these works. By contrast, we choose to disallow both local and inter-hierarchy parent-child communication. This choice not only makes the model small but more importantly complies with the design idea that communication merely happens between equally leveled ambients via a peer-to-peer manner (e.g., concurrent sibling ambients). The obtained model turns out not to lose any computational power.

(2) The open operation (or its variant) may be admitted in some of the works above; for example, the calculus of Coppo and Dezani-Ciancaglini (Reference Coppo and Dezani-Ciancaglini2002) defines a “selfopen” operation. As explained previously, we cancel the open-like operation because it stands in the way of accommodating ambients as the first-class participants of interactions, including HO communication. What is more, open is a programming primitive that appears overly powerful concerning the inter-operation of processes (Bugliesi et al., Reference Bugliesi, Castagna and Crafa2001).

(3) From the overall viewpoint, the models in the above works are quite different. For example, Kell has sequential/passivation semantics; that is, a process can follow an ambient, and the whole content of that ambient can be sent to another process (not necessarily an ambient). M-calculus also has a kind of passivation that follows the line of the Join calculus. None of these constructs is formalized in our model since we only allow interactions between equally positioned ambients (like Fu (Reference Fu2007)). Moreover, in all these works, type systems are needed to formulate the calculus for various purposes. For example, in the M-calculus, a type system is employed to facilitate the unification of communication and process migration; in the variant ambient model of Coppo and Dezani-Ciancaglini (Reference Coppo and Dezani-Ciancaglini2002), a type system is required to achieve full abstraction. By contrast, type systems are not necessary for our work, and this might make some difference in potential applications of the results of this work.

(4) None of these works has investigated, through explicit encoding, the computational completeness of the corresponding calculus. As a primary goal of this work, we accomplish the Turing completeness of our calculus, to our knowledge, for the first time for an ambient calculus with HO communication. The accompanying results and techniques may be of independent importance for further work.

1.3.1 Ambients with higher-order communication

As commented above, the start idea of this work is to enable HO (i.e., higher-order) communication for ambients. Interactions in ambient calculi are of HO nature; that is, ambients can move around between ambients. As such, it makes sense to allow ambients to be passed around, as an alternative (and probably more natural) method of interaction. Moreover, arguably, this ambient-passing communication is better over explicitly designated channel names, exactly like those in the HO pi-calculus. First, the formalism of the HO pi-calculus (or similar calculi) can be reused to some extent. Second, from the practical viewpoint, this kind of explicit HO communication appears more controllable because the locations are well-defined before the interaction happens. Also, this conforms to the rationale that interactions occur between ambients alone in a fair fashion, as discussed above. In a sense, HO communication offers a measure of quick-passage moving; that is, it can transmit a piece of (ambient) code deep into an ambient’s enclosure, rather than stepwise moving. This can make a big difference in the eyes of a programmer. More importantly, to be certain, such HO communications in effect cannot be derived using only the mobility of ambients (i.e., the basic moving capability of ambients); for example, HO communications can send a piece of code to a position beneath a prefix, whereas by no means can the basic movement manage to do this.

As an example, we have the following HO communication in our ambient calculus, which appears to be beyond the basic moving capability of ambients:

\begin{equation*} a[\overline {b}A.M \,|\, N] \,\,|\,\, b[a(X).R \,|\, O] \quad \,{\xrightarrow {\tau }}\, \quad a[M\,|\, N] \,\,|\,\, b[R\{A/X\} \,|\, O] \end{equation*}

In this example, prefix $\overline {b}A.M$ means “send $A$ to ambient $b$ and continue as $M$ ,” and prefix $a(X).R$ means “receive a term from ambient $a$ to instantiate the variable $X$ in $R$ .” So one can see that the HO communication relies on the names of both ambients taking part in the interaction. We will formally define this in Section 2.

1.3.2 The capability of exiting

Concerning the exiting capability, we use a more precise and, as such, more secure out-moving capability. That is, the requester has to clearly say which ambient is being called for moving out of the surrounding ambient, that is, real-name (or real-identity) moving. This real-name stipulation makes the exporting of programs more exact and thus more trustworthy and meanwhile helps reduce the possibility of interference. We see an example as follows:

(1) \begin{equation} a[\overline {out}\; cd.M\,|\, N] \;\,|\,\; c[d[out\; ca.O \,|\, A] \,|\, B] \quad \,{\xrightarrow {\tau }}\, \quad a[M\,|\, N] \;\,|\,\; c[B] \,|\, d[O \,|\, A] \end{equation}

In this example, $\overline {out}\; cd$ means “invite ambient $d$ to come out of ambient $c$ ,” and $out\; ca$ means “called by ambient $a$ to exit (the surrounding) ambient $c$ .” Here we require that the name of the ambient that is invited to exit the ambient containing it should be explicitly designated by the ambient that makes the exit call. Specifically, in equation (1), ambient $a$ knows the name of ambient $d$ (i.e., $d$ ) that it is calling to get out of $c$ . Previously, in FA, this is not mandatory (see Section 1.2); that is, $a$ does not need to be aware of the name of the ambient that is to move out, and thus, any ambient in $c$ can exit, hence the term “anonymous exit.” More to this point, if $d$ changes its name to, say $f$ , anonymous exit still works. However, in our model, since anonymity is disallowed and precise name is enforced, that is not possible. This is what we mean exactly by real name.

We note that $out\; ca$ can be simplified to be $out\; a$ , since $c$ is obviously the ambient from which ambient $d$ is moving out, and actually can be detected during run-time. From a pragmatic standpoint, this simple form of out-moving is more flexible and easier to implement and maintain than hard-coding the name of the surrounding ambient. So we can reformulate the above example as follows:

(2) \begin{equation} a[\overline {out}\; cd.M\,|\, N] \;\,|\,\; c[d[out\; a.O \,|\, A] \,|\, B] \quad \,{\xrightarrow {\tau }}\, \quad a[M\,|\, N] \;\,|\,\; c[B] \,|\, d[O \,|\, A] \end{equation}

The new out-moving capability eliminates the possibility of moving anonymously. That is, every movement of an ambient should be explicitly and precisely set up in communicating sessions. We stress that this strengthens the entirely real-name and mutually fair interaction between ambients and removes one loose design end of FA, that is, allowing anonymous out-moving (in fact, this may also be attributed to some technical convenience in the discussion of FA). The concept of anonymity here is somewhat different from that in the paradigm of security, where the notion of anonymity captures the requirement for privacy; for example, a ciphertext should not leak any information about the key or sender/recipient. Here there is no ciphertext but actions (or instructions) instead. So the anonymity in the formalism of ambients is more or less an attribute of unnecessary flavor, at least pertaining to the moving capacity.

If one insists on somehow moving an anonymous ambient around, for example, ambient $c$ in $a[(c)c[M]\,|\, N]$ , then the HO communication can be used to achieve this in a different yet still effective manner. Intuitively, HO communication enables one to transmit some (anonymous) sub-ambient from one ambient to another. For example, we have the following:

\begin{equation*} \begin{array}{l} a[\overline {b}A.M' \,|\, N] \,\,|\,\, b[a(X).X \,|\, O] \quad \,{\xrightarrow {\tau }}\, \quad a[M'\,|\, N] \,\,|\,\, b[A\,|\, O] \\ A\stackrel {\mathrm {def}}{=} (c)c[M] \end{array} \end{equation*}

Besides, as to another point, the example above can be tuned to implement scope extrusion. That is,

\begin{equation*} \begin{array}{l} a[(c)\overline {b}A'.M' \,|\, N] \,\,|\,\, b[a(X).X \,|\, O] \quad \,{\xrightarrow {\tau }}\, \quad (c)(a[M'\,|\, N] \,\,|\,\, b[A'\,|\, O]) \\ A'\stackrel {\mathrm {def}}{=} c[M] \text { and } c {\notin } \textrm {fn}O(N,O)\, (\text { i.e.,} \ c \text { does not appear free in } N \text { and } O) \end{array} \end{equation*}

This reminds one of the standard bound output in the HO pi-calculus.

1.3.3 Other points

We do not allow parent-child communication for the same reason as in FA. In a nutshell, we stick to the principle that interaction only happens between standalone independent ambients, whereas allowing parent-child communication is as undesirable as allowing communication between an ambient and a non-ambient.

Moreover, in establishing the computational completeness of our ambient calculus, it seems that allowing father-child communication would defeat the purpose of encoding a Turing-complete model: FO pi-calculus in the case of FA and HO pi-calculus in the case of this work. The reason is that the following process would be very arduous to interpret correctly:

\begin{equation*} \overline {a}A.a(X).0 \end{equation*}

Roughly, the encoding of this process would have an internal action between the ambient encoding prefix $\overline {a}$ and the inside ambient encoding prefix $a(X)$ , leading to a case that breaks full abstraction. However, this reminds us of asynchronous communication. To this point, parent-child communication is likely essential to encode processes enabling asynchrony.

We drop the open capability for a similar reason as BA. In addition, from the viewpoint of software reuse, directly merging the source code of two ambients is not efficient and easy to raise errors. It would break modularity and render the system hard to test and maintain. A more feasible approach is to use the (third-party) codes as some kind of service (or library). This way, the imported codes are ensured to run correctly, as long as it has been thoroughly tested and properly configured, and, moreover, to delimit the error rate to the greatest extent.

Organization

The remainder of this paper is organized as follows. Section 2 defines the ambient calculus of this work, including its syntax, semantics, and related conventions. Section 3 presents the behavioral theory of our ambient calculus, including the bisimulation equality (i.e., bisimilarity), and its equivalence and congruence properties. Section 4 investigates the observational theory. We define the barbed congruence and show its coincidence with bisimilarity. Section 5 demonstrates the expressiveness of the ambient calculus. We exploit an encoding of the minimal HO calculus. Section 5.3.2 concludes the paper with some future work.