A Commitment Relation for the Ambient Calculus
Luca Cardelli, Andrew D. Gordon · 2000
We present a commitment relation, a kind of labeled transition system, for the ambient calculus. This note is an extract from an unpublished annex to our original article [2] on the ambient calculus. 1 Review of the Ambient Calculus In this section we review the syntax of the ambient calculus, and the structural congruence and reduction relations. 1.1 Capabilities and Processes We assume an infinite set of names. We let m and n range over names. Moreover, we assume there is an infinite collections of variables ranged over by metavariables x, y, z. The sets of capabilities and processes are defined by the grammars: Mobility and Communication Primitives M ::= capability x variable n name in M can enter into M out M can exit out of M open M can open M null