On the Expressiveness of Pure Mobile Ambients

AbstractWe consider the Pure Ambient Calculus, which is Cardelli and Gordon's Ambient Calculus (or more precisely its safe version by Levi and Sangiorgi) restricted to its mobility primitives, and we focus on its expressive power. Since it has no form of communication or substitution, we show how these notions can be simulated by mobility and modifications in the hierarchical structure of ambients. As an example, we give an encoding of the synchronous π-calculus into pure ambients and we state an operational correspondence result. In order to simplify the proof and give an intuitive understanding of the encoding, we design an intermediate language: the π-Calculus with Explicit Substitutions and Channels, which is a syntactic extension of the π-calculus with a specific operational semantics