Document Open Access Logo

Output Without Delay: A π-Calculus Compatible with Categorical Semantics

Authors Ken Sakayori , Takeshi Tsukada

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2021.32.pdf
  • Filesize: 0.91 MB
  • 22 pages

Document Identifiers

Author Details

Ken Sakayori
  • The University of Tokyo, Japan
Takeshi Tsukada
  • Chiba University, Japan

Funding

This work was supported by JSPS KAKENHI Grant Numbers JP20J13473 and JP19K20211.

Acknowledgements

We would like to thank anonymous referees for useful comments.

Cite AsGet BibTex

Ken Sakayori and Takeshi Tsukada. Output Without Delay: A π-Calculus Compatible with Categorical Semantics. In 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 195, pp. 32:1-32:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
https://doi.org/10.4230/LIPIcs.FSCD.2021.32

Abstract

The quest for logical or categorical foundations of the π-calculus (not limited to session-typed variants) remains an important challenge. A categorical type theory correspondence for a variant of the i/o-typed π-calculus was recently revealed by Sakayori and Tsukada, but, at the same time, they exposed that this categorical semantics contradicts with most of the behavioural equivalences. This paper diagnoses the nature of this problem and attempts to fill the gap between categorical and operational semantics. We first identify the source of the problem to be the mismatch between the operational and categorical interpretation of a process called the forwarder. From the operational viewpoint, a forwarder may add an arbitrary delay when forwarding a message, whereas, from the categorical viewpoint, a forwarder must not add any delay when forwarding a message. Led by this observation, we introduce a calculus that can express forwarders that do not introduce delay. More specifically, the calculus we introduce is a variant of the π-calculus with a new operational semantics in which output actions are forced to happen as soon as they get unguarded. We show that this calculus (i) is compatible with the categorical semantics and (ii) can encode the standard π-calculus.

Subject Classification

ACM Subject Classification
  • Theory of computation → Concurrency
  • Theory of computation → Process calculi
  • Theory of computation → Denotational semantics
Keywords
  • π-calculus
  • categorical semantics
  • linear approximation

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Samson Abramsky. Proofs as processes. Theor. Comput. Sci., 135(1):5-9, 1994. URL: https://doi.org/10.1016/0304-3975(94)00103-0.
  2. Samson Abramsky, Simon J. Gay, and Rajagopal Nagarajan. Interaction categories and the foundations of typed concurrent programming. In Proceedings of the NATO Advanced Study Institute on Deductive Program Design, Marktoberdorf, Germany, pages 35-113, 1996. Google Scholar
  3. Gianluigi Bellin and Philip J. Scott. On the π-calculus and linear logic. Theor. Comput. Sci., 135(1):11-65, 1994. URL: https://doi.org/10.1016/0304-3975(94)00104-9.
  4. Michele Boreale. On the expressiveness of internal mobility in name-passing calculi. Theor. Comput. Sci., 195(2):205-226, 1998. URL: https://doi.org/10.1016/S0304-3975(97)00220-X.
  5. Gérard Boudol. The lambda-calculus with multiplicities (abstract). In Eike Best, editor, CONCUR '93, 4th International Conference on Concurrency Theory, Hildesheim, Germany, August 23-26, 1993, Proceedings, volume 715 of Lecture Notes in Computer Science, pages 1-6. Springer, 1993. URL: https://doi.org/10.1007/3-540-57208-2_1.
  6. Luís Caires, Frank Pfenning, and Bernardo Toninho. Linear logic propositions as session types. Mathematical Structures in Computer Science, 26(3):367-423, 2016. URL: https://doi.org/10.1017/S0960129514000218.
  7. Simon Castellan and Nobuko Yoshida. Two sides of the same coin: session types and game semantics: a synchronous side and an asynchronous side. PACMPL, 3(POPL):27:1-27:29, 2019. URL: https://doi.org/10.1145/3290340.
  8. Gian Luca Cattani, Ian Stark, and Glynn Winskel. Presheaf models for the pi-calculus. In Category Theory and Computer Science, 7th International Conference, CTCS '97, Santa Margherita Ligure, Italy, September 4-6, 1997, Proceedings, pages 106-126, 1997. URL: https://doi.org/10.1007/BFb0026984.
  9. Gian Luca Cattani and Glynn Winskel. Presheaf models for concurrency. In Computer Science Logic, 10th International Workshop, CSL '96, Annual Conference of the EACSL, Utrecht, The Netherlands, September 21-27, 1996, Selected Papers, pages 58-75, 1996. URL: https://doi.org/10.1007/3-540-63172-0_32.
  10. Thomas Ehrhard and Laurent Regnier. Uniformity and the taylor expansion of ordinary lambda-terms. Theor. Comput. Sci., 403(2-3):347-372, 2008. URL: https://doi.org/10.1016/j.tcs.2008.06.001.
  11. Marcelo P. Fiore, Eugenio Moggi, and Davide Sangiorgi. A fully abstract model for the π-calculus. Inf. Comput., 179(1):76-117, 2002. URL: https://doi.org/10.1006/inco.2002.2968.
  12. André Joyal, Mogens Nielsen, and Glynn Winskel. Bisimulation from open maps. Inf. Comput., 127(2):164-185, 1996. URL: https://doi.org/10.1006/inco.1996.0057.
  13. Ugo Dal Lago, Marc de Visme, Damiano Mazza, and Akira Yoshimizu. Intersection types and runtime errors in the pi-calculus. PACMPL, 3(POPL):7:1-7:29, 2019. URL: https://doi.org/10.1145/3290320.
  14. Damiano Mazza, Luc Pellissier, and Pierre Vial. Polyadic approximations, fibrations and intersection types. PACMPL, 2(POPL):6:1-6:28, 2018. URL: https://doi.org/10.1145/3158094.
  15. Paul-André Melliès. Categorical combinatorics of scheduling and synchronization in game semantics. PACMPL, 3(POPL):23:1-23:30, 2019. URL: https://doi.org/10.1145/3290336.
  16. Massimo Merro. Locality in the π-calculus and applications to distributed objects. PhD thesis, École Nationale Supérieure des Mines de Paris, 2000. Google Scholar
  17. Benjamin C. Pierce and Davide Sangiorgi. Typing and subtyping for mobile processes. Mathematical Structures in Computer Science, 6(5):409-453, 1996. URL: https://doi.org/10.1017/S096012950007002X.
  18. John Power and Edmund Robinson. Premonoidal categories and notions of computation. Mathematical Structures in Computer Science, 7(5):453-468, 1997. URL: https://doi.org/10.1017/S0960129597002375.
  19. Ken Sakayori and Takeshi Tsukada. A categorical model of an i/o-typed π-calculus. In Programming Languages and Systems - 28th European Symposium on Programming, ESOP 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings, pages 640-667, 2019. URL: https://doi.org/10.1007/978-3-030-17184-1_23.
  20. Ian Stark. A fully abstract domain model for the π-calculus. In Proceedings, 11th Annual IEEE Symposium on Logic in Computer Science, New Brunswick, New Jersey, USA, July 27-30, 1996, pages 36-42, 1996. URL: https://doi.org/10.1109/LICS.1996.561301.
  21. Takeshi Tsukada, Kazuyuki Asada, and C.-H. Luke Ong. Generalised species of rigid resource terms. In 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017, Reykjavik, Iceland, June 20-23, 2017, pages 1-12, 2017. URL: https://doi.org/10.1109/LICS.2017.8005093.
  22. Takeshi Tsukada and C.-H. Luke Ong. Plays as resource terms via non-idempotent intersection types. In Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '16, New York, NY, USA, July 5-8, 2016, pages 237-246, 2016. URL: https://doi.org/10.1145/2933575.2934553.
  23. Glynn Winskel and Mogens Nielsen. Presheaves as transition systems. In Partial Order Methods in Verification, Proceedings of a DIMACS Workshop, Princeton, New Jersey, USA, July 24-26, 1996, pages 129-140, 1996. URL: https://doi.org/10.1090/dimacs/029/08.
  24. Nobuko Yoshida. Minimality and separation results on asynchronous mobile processes - representability theorems by concurrent combinators. Theor. Comput. Sci., 274(1-2):231-276, 2002. URL: https://doi.org/10.1016/S0304-3975(00)00310-8.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact