文献类型：期刊文献

英文题名：On higher-order communication in ambient calculi

作者：Xu, Xian[1];Huang, Yan[1];Yao, Zhihuan[1]

机构：[1]East China Univ Sci & Technol, Shanghai, Peoples R China

年份：2025

卷号：35

外文期刊名：MATHEMATICAL STRUCTURES IN COMPUTER SCIENCE

收录：;EI(收录号：20251518229753);WOS:【SCI-EXPANDED(收录号:WOS:001467322700001)】；

基金：This work has been supported by project ANR 12IS02001 PACE and NSF of China (62072299, 61872142) and Shanghai "Science and Technology Innovation Action Plan" (24BC3200500, 24BC3200300).

语种：英文

外文关键词：Ambient calculus; communication; higher-order; processes; encoding

摘要：We revisit the communication primitive in ambient calculi. Previously, such communication was confined to first-order (FO) mode (e.g., merely names or capabilities of ambients can be sent), local mode (e.g., the communication only occurs inside an ambient), or particular cross-hierarchy mode (e.g., parent-child communication). In this work, we explore further higher-order (HO) communication in ambient calculi. Specifically, such a communication mechanism allows sending a whole piece of a program across the borders of ambients and is the only form of communication that can happen exactly between ambients. Since ambients are basically of HO nature (i.e., those being moved may be ambients themselves), in a sense, it appears more natural to have HO communication than FO communication. We stipulate that communications merely occur between equally positioned ambients in a peer-to-peer fashion (e.g., between sibling ambients). Following this line, we drop the local or other forms of communication that violate this criterion. As the workbench, we work on a variant of Fair Ambients extended with HO communication, FAHO. This variant also strengthens the original version in that entirely real-identity interaction is guaranteed. We study the semantics, bisimulation, and expressiveness of FAHO. Particularly, we provide the operational semantics using a labeled transition system. Over the semantics, we define the bisimulation in line with the standard notion of bisimulation for ambients and prove that the bisimulation equivalence (i.e., bisimilarity) is a congruence. In addition, we demonstrate that bisimilarity coincides with observational congruence (i.e., barbed congruence). Moreover, we show that FAHO can encode a minimal Turing-complete HO calculus and thus is computationally complete.