Document Open Access Logo

Non-Deterministic Functions as Non-Deterministic Processes

Authors Joseph W. N. Paulus, Daniele Nantes-Sobrinho , Jorge A. Pérez

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2021.21.pdf
  • Filesize: 0.9 MB
  • 22 pages

Document Identifiers

Author Details

Joseph W. N. Paulus
  • University of Groningen, The Netherlands
Daniele Nantes-Sobrinho
  • University of Brasília, Brazil
Jorge A. Pérez
  • University of Groningen, The Netherlands
  • CWI, Amsterdam, The Netherlands

Funding

Paulus and Pérez have been partially supported by the Dutch Research Council (NWO) under project No. 016.Vidi.189.046 (Unifying Correctness for Communicating Software).

Acknowledgements

We are grateful to the anonymous reviewers for their careful reading and constructive remarks.

Cite AsGet BibTex

Joseph W. N. Paulus, Daniele Nantes-Sobrinho, and Jorge A. Pérez. Non-Deterministic Functions as Non-Deterministic Processes. In 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 195, pp. 21:1-21:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
https://doi.org/10.4230/LIPIcs.FSCD.2021.21

Abstract

We study encodings of the λ-calculus into the π-calculus in the unexplored case of calculi with non-determinism and failures. On the sequential side, we consider λ^↯_⊕, a new non-deterministic calculus in which intersection types control resources (terms); on the concurrent side, we consider 𝗌π, a π-calculus in which non-determinism and failure rest upon a Curry-Howard correspondence between linear logic and session types. We present a typed encoding of λ^↯_⊕ into 𝗌π and establish its correctness. Our encoding precisely explains the interplay of non-deterministic and fail-prone evaluation in λ^↯_⊕ via typed processes in 𝗌π. In particular, it shows how failures in sequential evaluation (absence/excess of resources) can be neatly codified as interaction protocols.

Subject Classification

ACM Subject Classification
  • Theory of computation → Type structures
  • Theory of computation → Process calculi
Keywords
  • Resource calculi
  • π-calculus
  • intersection types
  • session types
  • linear logic

Metrics

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

Related Versions

References

  1. Martin Berger, Kohei Honda, and Nobuko Yoshida. Genericity and the pi-calculus. In Andrew D. Gordon, editor, Foundations of Software Science and Computational Structures, 6th International Conference, FOSSACS 2003 Held as Part of the Joint European Conference on Theory and Practice of Software, ETAPS 2003, Warsaw, Poland, April 7-11, 2003, Proceedings, volume 2620 of Lecture Notes in Computer Science, pages 103-119. Springer, 2003. URL: https://doi.org/10.1007/3-540-36576-1_7.
  2. Viviana Bono and Mariangiola Dezani-Ciancaglini. A tale of intersection types. In Holger Hermanns, Lijun Zhang, Naoki Kobayashi, and Dale Miller, editors, LICS '20: 35th Annual ACM/IEEE Symposium on Logic in Computer Science, Saarbrücken, Germany, July 8-11, 2020, pages 7-20. ACM, 2020. URL: https://doi.org/10.1145/3373718.3394733.
  3. Gérard Boudol. The lambda-calculus with multiplicities (abstract). In Eike Best, editor, CONCUR '93, 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.
  4. Gérard Boudol and Cosimo Laneve. lambda-calculus, multiplicities, and the pi-calculus. In Proof, Language, and Interaction, Essays in Honour of Robin Milner, pages 659-690, 2000. Google Scholar
  5. Antonio Bucciarelli, Delia Kesner, and Daniel Ventura. Non-idempotent intersection types for the lambda-calculus. Logic Journal of the IGPL, 25(4):431-464, 2017. Google Scholar
  6. Luís Caires and Jorge A. Pérez. Linearity, control effects, and behavioral types. In Hongseok Yang, editor, Programming Languages and Systems - 26th European Symposium on Programming, ESOP 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings, volume 10201 of Lecture Notes in Computer Science, pages 229-259. Springer, 2017. URL: https://doi.org/10.1007/978-3-662-54434-1_9.
  7. Luís Caires and Frank Pfenning. Session types as intuitionistic linear propositions. In CONCUR 2010 - Concurrency Theory, 21th International Conference, CONCUR 2010, Paris, France, August 31-September 3, 2010. Proceedings, pages 222-236, 2010. URL: https://doi.org/10.1007/978-3-642-15375-4_16.
  8. Mariangiola Dezani-Ciancaglini, Ugo de'Liguoro, and Adolfo Piperno. Filter models for a parallel and non deterministic lambda-calculus. In Andrzej M. Borzyszkowski and Stefan Sokolowski, editors, Mathematical Foundations of Computer Science 1993, 18th International Symposium, MFCS'93, Gdansk, Poland, August 30-September 3, 1993, Proceedings, volume 711 of Lecture Notes in Computer Science, pages 403-412. Springer, 1993. URL: https://doi.org/10.1007/3-540-57182-5_32.
  9. Thomas Ehrhard and Laurent Regnier. The differential lambda-calculus. Theor. Comput. Sci., 309(1-3):1-41, 2003. URL: https://doi.org/10.1016/S0304-3975(03)00392-X.
  10. Silvia Ghilezan, Jelena Ivetic, Pierre Lescanne, and Silvia Likavec. Intersection types for the resource control lambda calculi. In Theoretical Aspects of Computing - ICTAC 2011 - 8th International Colloquium, Johannesburg, South Africa, August 31-September 2, 2011. Proceedings, pages 116-134, 2011. URL: https://doi.org/10.1007/978-3-642-23283-1_10.
  11. Daniele Gorla. Towards a unified approach to encodability and separation results for process calculi. Inf. Comput., 208(9):1031-1053, 2010. URL: https://doi.org/10.1016/j.ic.2010.05.002.
  12. Daniele Gorla and Uwe Nestmann. Full abstraction for expressiveness: history, myths and facts. Math. Struct. Comput. Sci., 26(4):639-654, 2016. URL: https://doi.org/10.1017/S0960129514000279.
  13. Tom Gundersen, Willem Heijltjes, and Michel Parigot. Atomic lambda calculus: A typed lambda-calculus with explicit sharing. In 28th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2013, New Orleans, LA, USA, June 25-28, 2013, pages 311-320, 2013. URL: https://doi.org/10.1109/LICS.2013.37.
  14. Kohei Honda. Types for dyadic interaction. In Eike Best, editor, CONCUR '93, Hildesheim, Germany, August 23-26, 1993, Proceedings, volume 715 of Lecture Notes in Computer Science, pages 509-523. Springer, 1993. URL: https://doi.org/10.1007/3-540-57208-2_35.
  15. Kohei Honda, Vasco Thudichum Vasconcelos, and Makoto Kubo. Language primitives and type discipline for structured communication-based programming. In Chris Hankin, editor, Programming Languages and Systems - ESOP'98, 7th European Symposium on Programming, Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS'98, Lisbon, Portugal, March 28-April 4, 1998, Proceedings, volume 1381 of Lecture Notes in Computer Science, pages 122-138. Springer, 1998. URL: https://doi.org/10.1007/BFb0053567.
  16. Kohei Honda, Nobuko Yoshida, and Martin Berger. Process types as a descriptive tool for interaction - control and the pi-calculus. In Gilles Dowek, editor, Rewriting and Typed Lambda Calculi - Joint International Conference, RTA-TLCA 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014. Proceedings, volume 8560 of Lecture Notes in Computer Science, pages 1-20. Springer, 2014. URL: https://doi.org/10.1007/978-3-319-08918-8_1.
  17. Dimitrios Kouzapas, Jorge A. Pérez, and Nobuko Yoshida. On the relative expressiveness of higher-order session processes. Inf. Comput., 268, 2019. URL: https://doi.org/10.1016/j.ic.2019.06.002.
  18. Robin Milner. Functions as processes. Mathematical Structures in Computer Science, 2(2):119-141, 1992. URL: https://doi.org/10.1017/S0960129500001407.
  19. Robin Milner, Joachim Parrow, and David Walker. A calculus of mobile processes, I. Inf. Comput., 100(1):1-40, 1992. URL: https://doi.org/10.1016/0890-5401(92)90008-4.
  20. Dominic A. Orchard and Nobuko Yoshida. Effects as sessions, sessions as effects. In Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, January 20-22, 2016, pages 568-581. ACM, 2016. URL: https://doi.org/10.1145/2837614.2837634.
  21. Michele Pagani and Simona Ronchi Della Rocca. Solvability in resource lambda-calculus. In C.-H. Luke Ong, editor, Foundations of Software Science and Computational Structures, 13th International Conference, FOSSACS 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010, Paphos, Cyprus, March 20-28, 2010. Proceedings, volume 6014 of Lecture Notes in Computer Science, pages 358-373. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-12032-9_25.
  22. Joseph Paulus, Daniele Nantes-Sobrinho, and Jorge A. Pérez. Non-Deterministic Functions as Non-Deterministic Processes (Extended Version). CoRR, abs/2104.14759, 2021. URL: http://arxiv.org/abs/2104.14759.
  23. Davide Sangiorgi. From lambda to pi; or, rediscovering continuations. Math. Struct. Comput. Sci., 9(4):367-401, 1999. URL: http://journals.cambridge.org/action/displayAbstract?aid=44843.
  24. Davide Sangiorgi and David Walker. The Pi-Calculus - a theory of mobile processes. Cambridge University Press, 2001. Google Scholar
  25. Bernardo Toninho, Luís Caires, and Frank Pfenning. Functions as session-typed processes. In Lars Birkedal, editor, Foundations of Software Science and Computational Structures - 15th International Conference, FOSSACS 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012, Tallinn, Estonia, March 24-April 1, 2012. Proceedings, volume 7213 of Lecture Notes in Computer Science, pages 346-360. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-28729-9_23.
  26. Bernardo Toninho and Nobuko Yoshida. On polymorphic sessions and functions - A tale of two (fully abstract) encodings. In Amal Ahmed, editor, 27th European Symposium on Programming, ESOP 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings, volume 10801 of Lecture Notes in Computer Science, pages 827-855. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-89884-1_29.
  27. Philip Wadler. Propositions as sessions. In Peter Thiemann and Robby Bruce Findler, editors, ACM SIGPLAN International Conference on Functional Programming, ICFP'12, Copenhagen, Denmark, September 9-15, 2012, pages 273-286. ACM, 2012. URL: https://doi.org/10.1145/2364527.2364568.
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