Expressing First-Order pi-Calculus in Higher-Order Calculus of Communicating Systems

In the study of process calculi, encoding between different calculiis an effective way to compare the expressive power of calculi and canshed light on the essence of where the difference lies. Thomsen andSangiorgi have worked on the higher-order calculi (higher-order Calculusof Communicating Systems (CCS) and higher-order \pi-calculus, respectively) and the encodingfrom and to first-order \pi-calculus. However a fully abstractencoding of first-order \pi-calculus with higher-order CCS isnot available up-today. This is what we intend to settle in thispaper. We follow the encoding strategy, first proposed by Thomsen, oftranslating first-order \pi-calculus into Plain CHOCS. We show that theencoding strategy is fully abstract with respect to earlybisimilarity (first-order \pi-calculus) and wired bisimilarity(Plain CHOCS) (which is a bisimulation defined on wired processes only sendingand receiving wires), that is the core of the encoding strategy.Moreover from the fact that the wired bisimilarity is contained by thewell-established context bisimilarity, we secure the soundness ofthe encoding, with respect to early bisimilarity and contextbisimilarity. We use index technique to get around all the technicaldetails to reach these main results of this paper. Finally, we makesome discussion on our work and suggest some future work.