| Abstract: | Pure Mobile Ambients (i.e., Mobile Ambients without communication) provides three mobility primitives: in and out for ambient movement, and open to dissolve ambient boundaries. In this paper we consider the expressiveness of the primitives in and out for ambient movement; more precisely, we concentrate on the interplay between ambient movement and the ability to create new names (exploiting the restriction operator). To this aim, we consider a version of Pure Mobile Ambients (with explicit recursive definitions instead of replication) and we concentrate on the three fragments of the calculus that can be obtained removing either one or both between movement and the ability to create new names. The unique mobility primitive that we retain in all of the considered calculi is open. Te three fragments are denoted as follows: MA−mv without ambient movement, MA−v without restriction, and MA−mv−v without both movement and restriction. We prove that both the fragments MA−mv and MA−v are Turing-complete, while this is not the case for MA−mv−v. Indeed, we prove that in this latter calculus the existence of an infinite computation turns to be a decidable property. |
