Parameterizing higher-order processes on names and processes

Xu, Xian

RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications, Tome 53 (2019) no. 3-4, pp. 153-206.

Suite au passage du modèle économique de la revue en S20, le texte intégral des articles des années 2019 et 2020 est accessible uniquement sur le site de l'éditeur et est réservé aux abonnés.

Parameterization extends higher-order processes with the capability of abstraction and application (like those in lambda-calculus). As is well-known, this extension is strict, meaning that higher-order processes equipped with parameterization are strictly more expressive than those without parameterization. This paper studies strictly higher-order processes (i.e., no name-passing) with two kinds of parameterization: one on names and the other on processes themselves. We present two main results. One is that in presence of parameterization, higher-order processes can interpret first-order (name-passing) processes in a quite elegant fashion, in contrast to the fact that higher-order processes without parameterization cannot encode first-order processes at all. We present two such encodings and analyze their properties in depth, particularly full abstraction. In the other result, we provide a simpler characterization of the standard context bisimilarity for higher-order processes with parameterization, in terms of the normal bisimilarity that stems from the well-known normal characterization for higher-order calculus. As a spinoff, we show that the bisimulation up-to context technique is sound in the higher-order setting with parameterization.

[1] M. Bundgaard, T. Hildebrandt and J.C. Godskesen, A cps encoding of name-passing in higher-order mobile embedded resources. Theor. Comput. Sci. 356 (2006) 422–439. | DOI | MR | Zbl

[2] A. Durier, D. Hirschkoff and D. Sangiorgi, Towards “up to context” reasoning about higher-order processes. Theor. Comput. Sci. DOI: (2019). | DOI | MR | Zbl

[3] U.H. Engberg and M. Nielsen, A calculus of communicating systems with label passing. Tech. Rep. DAIMI PB-208, Computer Science Department, University of Aarhus (1986).

[4] U.H. Engberg and M. Nielsen, A calculus of communicating systems with label passing - ten years after. In Proof, Language, and Interaction: Essays in Honour of Robin Milner. MIT Press Cambridge (2000) 599–622. | MR

[5] Y. Fu, On quasi open bisimulation. Theor. Comput. Sci. 338 (2005) 96–126. | DOI | MR | Zbl

[6] Y. Fu, Fair ambients. Acta Inform. 43 (2007) 535–594. | DOI | MR | Zbl

[7] Y. Fu, Theory of interaction. Theor. Comput. Sci. 611 (2015) 1–49. | DOI | MR

[8] Y. Fu and H. Lu, On the expressiveness of interaction. Theor. Comput. Sci. 411 (2010) 1387–1451. | DOI | MR | Zbl

[9] D. Gorla, Towards a unified approach to encodability and separation results for process calculi. In Proceedings of the 19th International Conference on Concurrency Theory (CONCUR 2008), vol. 5201 of Lecture Notes in Computer Science. Springer Verlag (2008) 492–507. | DOI | MR | Zbl

[10] D. Gorla, On the relative expressive power of calculi for mobility. Electr. Notes Theor. Comput. Sci. 249 (2009) 269–286. | DOI | Zbl

[11] D. Gorla and U. Nestmann, Full abstraction for expressiveness: History, myths and facts. Math. Struct. Comput. Sci. 26 (2016) 639–654. | DOI | MR | Zbl

[12] D. Kouzapas, J.A. Pérez and N. Yoshida, On the relative expressiveness of higher-order session processes. In Proceedings of the 25th European Symposium on Programming (ESOP 2016). In Vol. 9632 of Lecture Notes in Computer Science. Springer (2016) 446–475. | DOI | MR | Zbl

[13] I. Lanese, J. Pérez, D. Sangiorgi and A. Schmitt, On the expressiveness and decidability of higher-order process calculi. In Proceedings of the 23rd Annual IEEE Symposium on Logic in Computer Science (LICS 2008). IEEE Computer Society (2008) 145–155. | DOI | Zbl

[14] I. Lanese, J.A. Pérez, D. Sangiorgi and A. Schmitt, On the expressiveness of polyadic and synchronous communication in higher-order process calculi. In Proceedings of the 36th International Colloquium on Automata, Languages and Programming (ICALP 2010). In Vol. 6199 of Lecture Notes in Computer Science. Springer Verlag (2010) 442–453. | DOI | MR | Zbl

[15] I. Lanese, J.A. Pérez, D. Sangiorgi and A. Schmitt, On the expressiveness and decidability of higher-order process calculi. Inf. Comput. 209 (2011) 198–226. | DOI | MR | Zbl

[16] S. Lenglet, A. Schmitt and J.B. Stefani, Normal bisimulations in calculi with passivation. In: Proceedings of the 12th International Conference on Foundations of Software Science and Computational Structures (FOSSACS 2009). Vol. 5504 of Lecture Notes in Computer Science. Springer Verlag (2009) 257–271. | MR | Zbl

[17] S. Lenglet, A. Schmitt and J.B. Stefani, Characterizing contextual equivalence in calculi with passivation. Inf. Comput. 209 (2011) 1390–1433. | DOI | MR | Zbl

[18] J.M. Madiot, D. Pous and D. Sangiorgi, Bisimulations up-to: Beyond first-order transition systems. In: Proceedings of the 25th Conference on Concurrency Theory (CONCUR 2014). In Vol. 8704 of Lecture Notes in Computer Science. Springer Verlag (2014) 93–108. | DOI | MR | Zbl

[19] M. Merro and M. Hennessy, Bisimulation congruences in safe ambients. In: Proceedings of the 29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 02). Portland, Oregon (2002) 71–80. | DOI | Zbl

[20] R. Milner, Communication and Concurrency. Prentice Hall (1989). | Zbl

[21] R. Milner, J. Parrow and D. Walker, A calculus of mobile processes (parts i and ii). Inf. Comput. 100 (1992) 1–77. | DOI | MR

[22] J. Parrow, General conditions for full abstraction. Math. Struct. Comput. Sci. 26 (2016) 655–657. | DOI | MR | Zbl

[23] D. Pous and D. Sangiorgi, Enhancements of the bisimulation proof method, chap. Enhancements of the coinductive proof method. Cambridge University Press (2011). | MR | Zbl

[24] D. Sangiorgi, Expressing mobility in process algebras: First-order and higher-order paradigms. Ph.D. thesis, University of Edinburgh (1992).

[25] D. Sangiorgi, Bisimulation for higher-order process calculi. Inf. Comput. 131 (1996) 141–178. | DOI | MR | Zbl

[26] D. Sangiorgi, On the bisimulation proof method. Math. Struct. Comput. Sci. 8 (1998) 447–479. | DOI | MR | Zbl

[27] D. Sangiorgi, Introduction to Bisimulation and Coinduction. Cambridge University Press (2011). | DOI | MR | Zbl

[28] D. Sangiorgi, Concurrency theory: timed automata, testing, program synthesis. Distrib. Comput. 25 (2012) 3–4. | DOI

[29] D. Sangiorgi, N. Kobayashi and E. Sumii, Environmental bisimulations for higher-order languages. ACM Trans. Prog. Lang. Syst. 33 (2011) 5. | DOI

[30] D. Sangiorgi and J. Rutten, Advanced Topics in Bisimulation and Coinduction. Cambridge University Press (2012). | Zbl

[31] D. Sangiorgi and D. Walker, The Pi-calculus: a Theory of Mobile Processes. Cambridge University Press (2001). | MR | Zbl

[32] B. Thomsen, Calculi for higher order communicating systems. Ph.D. thesis, Department of Computing, Imperial College (1990).

[33] B. Thomsen, Plain CHOCS, a second generation calculus for higher-order processes. Acta Inf. 30 (1993) 1–59. | DOI | MR | Zbl

[34] X. Xu, Higher-order processes with parameterization over names and processes. In: Proceedings of Combined 23rd International Workshop on Expressiveness in Concurrency and 13th Workshop on Structural Operational Semantics (EXPRESS/2016), EPTCS 222 (2016) 15–29. | MR | Zbl

[35] X. Xu, Distinguishing and relating higher-order and first-order processes by expressiveness. Acta In. 49 (2012) 445–484. | MR | Zbl

[36] X. Xu, On context bisimulation for parameterized higher-order processes. In: Proceedings of the 6th Interaction and Concurrency Experience (ICE 2013), EPTCS 131 (2013) 37–51. | MR | Zbl

[37] X. Xu, Q. Yin and H. Long, On the computation power of name parameterization in higher-order processes. In: Proceedings of 8th Interaction and Concurrency Experience (ICE 2015). EPTCS 189 (2015) 114–127. | MR | Zbl

[38] Q. Yin, X. Xu and H. Long, On parameterization of higher-order processes. Int. J. Comput. Math. 7(94) (2017) 1451–1478. | DOI | MR | Zbl