Expressing FirstOrder piCalculus in HigherOrder Calculus of Communicating Systems

Abstract
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 higherorder calculi (higherorder Calculusof Communicating Systems (CCS) and higherorder \picalculus, respectively) and the encodingfrom and to firstorder \picalculus. However a fully abstractencoding of firstorder \picalculus with higherorder CCS isnot available uptoday. This is what we intend to settle in thispaper. We follow the encoding strategy, first proposed by Thomsen, oftranslating firstorder \picalculus into Plain CHOCS. We show that theencoding strategy is fully abstract with respect to earlybisimilarity (firstorder \picalculus) 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 thewellestablished 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.

