Document Open Access Logo

Resource Transition Systems and Full Abstraction for Linear Higher-Order Effectful Programs

Authors Ugo Dal Lago , Francesco Gavazzo

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2021.23.pdf
  • Filesize: 0.86 MB
  • 19 pages

Document Identifiers

Author Details

Ugo Dal Lago
  • University of Bologna, Italy
  • INRIA Sophia Antipolis, France
Francesco Gavazzo
  • University of Bologna, Italy
  • INRIA Sophia Antipolis, France

Funding

The authors are supported by the ERC Consolidator Grant DLV-818616 DIAPASoN.

Cite AsGet BibTex

Ugo Dal Lago and Francesco Gavazzo. Resource Transition Systems and Full Abstraction for Linear Higher-Order Effectful Programs. In 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 195, pp. 23:1-23:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
https://doi.org/10.4230/LIPIcs.FSCD.2021.23

Abstract

We investigate program equivalence for linear higher-order (sequential) languages endowed with primitives for computational effects. More specifically, we study operationally-based notions of program equivalence for a linear λ-calculus with explicit copying and algebraic effects à la Plotkin and Power. Such a calculus makes explicit the interaction between copying and linearity, which are intensional aspects of computation, with effects, which are, instead, extensional. We review some of the notions of equivalences for linear calculi proposed in the literature and show their limitations when applied to effectful calculi where copying is a first-class citizen. We then introduce resource transition systems, namely transition systems whose states are built over tuples of programs representing the available resources, as an operational semantics accounting for both intensional and extensional interactive behaviours of programs. Our main result is a sound and complete characterization of contextual equivalence as trace equivalence defined on top of resource transition systems.

Subject Classification

ACM Subject Classification
  • Theory of computation → Operational semantics
Keywords
  • algebraic effects
  • linearity
  • program equivalence
  • full abstraction

Metrics

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

Related Versions

References

  1. Samson Abramsky. The lazy lambda calculus. In D. Turner, editor, Research Topics in Functional Programming, pages 65-117. Addison Wesley, 1990. Google Scholar
  2. Amal Ahmed, Matthew Fluet, and Greg Morrisett. L^3: A linear language with locations. Fundam. Informaticae, 77(4):397-449, 2007. Google Scholar
  3. Andrew W. Appel and Daddiv A. McAllester. An indexed model of recursive types for foundational proof-carrying code. ACM Trans. Program. Lang. Syst., 23(5):657-683, 2001. Google Scholar
  4. Robert Atkey. Syntax and semantics of quantitative type theory. In Proc. of LICS 2018, pages 56-65, 2018. Google Scholar
  5. Hendrik P. Barendregt. The lambda calculus: its syntax and semantics. Studies in logic and the foundations of mathematics. North-Holland, 1984. Google Scholar
  6. Hendrik P. Barendregt, Wil Dekkers, and Richard Statman. Lambda Calculus with Types. Perspectives in logic. Cambridge University Press, 2013. Google Scholar
  7. Michael Barr. Relational algebras. Lect. Notes Math., 137:39-55, 1970. Google Scholar
  8. Nick Benton and Philip Wadler. Linear logic, monads and the lambda calculus. In Proc. of LICS 1996, pages 420-431, 1996. Google Scholar
  9. Jean-Philippe Bernardy, Mathieu Boespflug, Ryan R. Newton, Simon Peyton Jones, and Arnaud Spiwack. Linear haskell: practical linearity in a higher-order polymorphic language. PACMPL, 2(POPL):5:1-5:29, 2018. Google Scholar
  10. Gavin M. Bierman. Program equivalence in a linear functional language. J. Funct. Program., 10(2):167-190, 2000. Google Scholar
  11. Gavin M. Bierman, Andrew M. Pitts, and Claudio V. Russo. Operational properties of lily, a polymorphic linear lambda calculus with recursion. Electr. Notes Theor. Comput. Sci., 41(3):70-88, 2000. Google Scholar
  12. Dariusz Biernacki, Maciej Piróg, Piotr Polesiuk, and Filip Sieczkowski. Handle with care: relational interpretation of algebraic effects and handlers. PACMPL, 2(POPL):8:1-8:30, 2018. Google Scholar
  13. Ales Bizjak and Lars Birkedal. Step-indexed logical relations for probability. In Proc. of FOSSACS 2015, pages 279-294, 2015. Google Scholar
  14. Aloïs Brunel, Marco Gaboardi, Damiano Mazza, and Steve Zdancewic. A core quantitative coeffect calculus. In Proc. of ESOP 2014, pages 351-370, 2014. Google Scholar
  15. Roy L. Crole. Completeness of bisimilarity for contextual equivalence in linear theories. Logic Journal of the IGPL, 9(1):27-51, 2001. Google Scholar
  16. Raphaëlle Crubillé and Ugo Dal Lago. On probabilistic applicative bisimulation and call-by-value lambda-calculi. In Proc. of ESOP 2014, pages 209-228, 2014. Google Scholar
  17. Raphaëlle Crubillé and Ugo Dal Lago. Metric reasoning about lambda-terms: The affine case. In Proc. of LICS 2015, pages 633-644, 2015. Google Scholar
  18. Raphaëlle Crubillé and Ugo Dal Lago. Metric reasoning about lambda-terms: The general case. In Proc. of ESOP 2017, pages 341-367, 2017. Google Scholar
  19. Ugo Dal Lago and Francesco Gavazzo. Effectful normal form bisimulation. In Proc. of ESOP 2019, pages 263-292, 2019. Google Scholar
  20. Ugo Dal Lago and Francesco Gavazzo. Resource transition systems and full abstraction for linear higher-order effectful programs (extended version), 2021. URL: http://www.cs.unibo.it/~dallago/resbranch.pdf.
  21. Ugo Dal Lago, Francesco Gavazzo, and Paul Blain Levy. Effectful applicative bisimilarity: Monads, relators, and howe’s method. In Proc. of LICS 2017, pages 1-12, 2017. Google Scholar
  22. Ugo Dal Lago, Francesco Gavazzo, and Ryo Tanaka. Effectful applicative similarity for call-by-name lambda calculi. Theor. Comput. Sci., 813:234-247, 2020. Google Scholar
  23. Ugo Dal Lago and Martin Hofmann. Bounded linear logic, revisited. In Proc. of TLCA 2009, pages 80-94, 2009. Google Scholar
  24. Ugo Dal Lago, Davide Sangiorgi, and Michele Alberti. On coinductive equivalences for higher-order probabilistic functional programs. In Proc. of POPL 2014, pages 297-308, 2014. Google Scholar
  25. Ugo Dal Lago and Margherita Zorzi. Probabilistic operational semantics for the lambda calculus. RAIRO - Theor. Inf. and Applic., 46(3):413-450, 2012. Google Scholar
  26. Yuxin Deng and Yuan Feng. Bisimulations for probabilistic linear lambda calculi. In Proc. of TASE 2017, pages 1-8, 2017. Google Scholar
  27. Yuxin Deng and Yu Zhang. Program equivalence in linear contexts. Theor. Comput. Sci., 585:71-90, 2015. Google Scholar
  28. Jeff Egger, Rasmus Ejlers Møgelberg, and Alex Simpson. Linear-use CPS translations in the enriched effect calculus. Logical Methods in Computer Science, 8(4), 2012. Google Scholar
  29. Marco Gaboardi, Shin-ya Katsumata, Dominic A. Orchard, Flavien Breuvart, and Tarmo Uustalu. Combining effects and coeffects via grading. In Proc. of ICFP 2016, pages 476-489, 2016. Google Scholar
  30. Francesco Gavazzo. Quantitative behavioural reasoning for higher-order effectful programs: Applicative distances. In Proc. of LICS 2018, pages 452-461, 2018. Google Scholar
  31. Francesco Gavazzo. Coinductive Equivalences and Metrics for Higher-order Languages with Algebraic Effects. PhD thesis, University of Bologna, Italy, 2019. URL: http://amsdottorato.unibo.it/9075/.
  32. Dan R. Ghica and Alex I. Smith. Bounded linear types in a resource semiring. In Proc. of ESOP 2014, pages 331-350, 2014. Google Scholar
  33. J-Y. Girard, A. Scedrov, and P.J. Scott. Bounded linear logic: A modular approach to polynomial-time computability. Theor. Comput. Sci., 97:1-66, 1992. Google Scholar
  34. Jean-Yves Girard. Linear logic. Theor. Comput. Sci., 50:1-102, 1987. Google Scholar
  35. Martin Hyland, Gordon D. Plotkin, and John Power. Combining effects: Sum and tensor. Theor. Comput. Sci., 357(1-3):70-99, 2006. Google Scholar
  36. Patricia Johann, Alex Simpson, and Janis Voigtländer. A generic operational metatheory for algebraic effects. In Proc. of LICS 2010, pages 209-218. IEEE Computer Society, 2010. Google Scholar
  37. Neelakantan R. Krishnaswami, Pierre Pradic, and Nick Benton. Integrating linear and dependent types. In Proc. of POPL 2015, pages 17-30, 2015. Google Scholar
  38. Alexander Kurz and Jiri Velebil. Relation lifting, a survey. J. Log. Algebr. Meth. Program., 85(4):475-499, 2016. Google Scholar
  39. Ugo Dal Lago and Francesco Gavazzo. On bisimilarity in lambda calculi with continuous probabilistic choice. In Proc. of MFPS 2019, pages 121-141, 2019. Google Scholar
  40. Søren B. Lassen. Bisimulation in untyped lambda calculus: Böhm trees and bisimulation up to context. Electr. Notes Theor. Comput. Sci., 20:346-374, 1999. Google Scholar
  41. Søren B. Lassen. Eager normal form bisimulation. In Proceedings of LICS 2005, pages 345-354, 2005. Google Scholar
  42. Paul B. Levy, John Power, and Hayo Thielecke. Modelling environments in call-by-value programming languages. Inf. Comput., 185(2):182-210, 2003. Google Scholar
  43. Saunders MacLane. Categories for the Working Mathematician. Springer-Verlag, 1971. Google Scholar
  44. Jean-Marie Madiot, Damien Pous, and Davide Sangiorgi. Bisimulations up-to: Beyond first-order transition systems. In Proc. of CONCUR 2014, pages 93-108, 2014. Google Scholar
  45. Ian A. Mason and Carolyn L. Talcott. Equivalence in functional languages with effects. J. Funct. Program., 1(3):287-327, 1991. Google Scholar
  46. Cristina Matache and Sam Staton. A sound and complete logic for algebraic effects. In Proc. of FOSSACS 2019, pages 382-399, 2019. Google Scholar
  47. Nicholas D. Matsakis and Felix S. Klock II. The rust language. In Proceedings of the 2014 ACM SIGAda annual conference on High integrity language technology, HILT 2014, Portland, Oregon, USA, October 18-21, 2014, pages 103-104, 2014. Google Scholar
  48. Rasmus Ejlers Møgelberg and Sam Staton. Linear usage of state. Logical Methods in Computer Science, 10(1), 2014. Google Scholar
  49. Eugenio Moggi. Computational lambda-calculus and monads. In Proc. of LICS 1989, pages 14-23. IEEE Computer Society, 1989. Google Scholar
  50. Eugenio Moggi. Notions of computation and monads. Inf. Comput., 93(1):55-92, 1991. Google Scholar
  51. J. Morris. Lambda Calculus Models of Programming Languages. PhD thesis, MIT, 1969. Google Scholar
  52. Dominic Orchard, Vilem-Benjamin Liepelt, and Harley Eades III. Quantitative program reasoning with graded modal types. Proc. ACM Program. Lang., 3(ICFP):110:1-110:30, 2019. Google Scholar
  53. Tomas Petricek, Dominic A. Orchard, and Alan Mycroft. Coeffects: a calculus of context-dependent computation. In Proc. of ICFP 2014, pages 123-135, 2014. Google Scholar
  54. Andrew M. Pitts. Parametric polymorphism and operational equivalence. Mathematical Structures in Computer Science, 10(3):321-359, 2000. Google Scholar
  55. Marinus J. Plasmeijer. CLEAN: a programming environment based on term graph rewriting. Electr. Notes Theor. Comput. Sci., 2:215-221, 1995. Google Scholar
  56. Gordon Plotkin. Lambda-definability and logical relations. Technical Report SAI-RM-4, School of A.I., University of Edinburgh, 1973. Google Scholar
  57. Gordon D. Plotkin and John Power. Adequacy for algebraic effects. In Proc. of FOSSACS 2001, pages 1-24, 2001. Google Scholar
  58. Gordon D. Plotkin and John Power. Semantics for algebraic operations. Electr. Notes Theor. Comput. Sci., 45:332-345, 2001. Google Scholar
  59. Gordon D. Plotkin and John Power. Notions of computation determine monads. In Proc. of FOSSACS 2002, pages 342-356, 2002. Google Scholar
  60. Gordon D. Plotkin and John Power. Algebraic operations and generic effects. Applied Categorical Structures, 11(1):69-94, 2003. Google Scholar
  61. John C. Reynolds. Types, abstraction and parametric polymorphism. In IFIP Congress, pages 513-523, 1983. Google Scholar
  62. Davide Sangiorgi, Naoki Kobayashi, and Eijiro Sumii. Environmental bisimulations for higher-order languages. ACM Trans. Program. Lang. Syst., 33(1):5:1-5:69, 2011. Google Scholar
  63. Davide Sangiorgi and Valeria Vignudelli. Environmental bisimulations for probabilistic higher-order languages. In Proceedings of POPL 2016, pages 595-607, 2016. Google Scholar
  64. Peter Selinger and Benoît Valiron. A lambda calculus for quantum computation with classical control. Mathematical Structures in Computer Science, 16(3):527-552, 2006. Google Scholar
  65. Peter Selinger and Benoît Valiron. A linear-non-linear model for a computational call-by-value lambda calculus (extended abstract). In Proc. of FOSSACS 2008, pages 81-96, 2008. Google Scholar
  66. Kurt Sieber. Reasoning about sequential functions via logical relations. In M. P. Fourman, P. T. Johnstone, and A. M. Pitts, editors, Applications of Categories in Computer Science, volume 177 of London Mathematical Society Lecture Note Series, pages 258-269. Cambridge University Press, 1992. Google Scholar
  67. Alex Simpson and Niels Voorneveld. Behavioural equivalence via modalities for algebraic effects. In Proc. of ESOP 2018, pages 300-326, 2018. Google Scholar
  68. David N. Turner and Philip Wadler. Operational interpretations of linear logic. Theor. Comput. Sci., 227(1-2):231-248, 1999. Google Scholar
  69. Philip Wadler. Linear types can change the world! In Programming concepts and methods, 1990, page 561, 1990. Google Scholar
  70. Philip Wadler. Monads for functional programming. In Advanced Functional Programming, First International Spring School on Advanced Functional Programming Techniques, Båstad, Sweden, May 24-30, 1995, Tutorial Text, pages 24-52, 1995. Google Scholar
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