Alex Simpson
Skip Abstract Section
Abstract
The article investigates behavioural equivalence between programs in a call-by-value functional language extended with a signature of (algebraic) effect-triggering operations. Two programs are considered as being behaviourally equivalent if they enjoy the same behavioural properties. To formulate this, we define a logic whose formulas specify behavioural properties. A crucial ingredient is a collection of modalities expressing effect-specific aspects of behaviour. We give a general theory of such modalities. If two conditions, openness and decomposability, are satisfied by the modalities, then the logically specified behavioural equivalence coincides with a modality-defined notion of applicative bisimilarity, which can be proven to be a congruence by a generalisation of Howe’s method. We show that the openness and decomposability conditions hold for several examples of algebraic effects: nondeterminism, probabilistic choice, global store, and input/output.
- Martin Abadi and Gordon Plotkin. 2009. A model of cooperative threads. In Proceedings of the 36th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’09). ACM, New York, 29--40. DOI:https://doi.org/10.1145/1480881.1480887Google Scholar
Digital Library
- Samson Abramsky. 1990. The lazy lambda calculus. In Research Topics in Functional Programming, David A. Turner (Ed.). Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 65--116.Google ScholarDigital Library
- Samson Abramsky. 1991. Domain theory in logical form. Annals of Pure and Applied Logic 51, 1--2 (1991), 1--77.Google ScholarCross Ref
- Danel Ahman, Catalin Hritcu, Kenji Maillard, Guido Martínez, Gordon Plotkin, Jonathan Protzenko, Aseem Rastogi, and Nikhil Swamy. 2017. Dijkstra monads for free. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL’17). ACM, New York, 515--529. DOI:https://doi.org/10.1145/3009837.3009878Google ScholarDigital Library
- Nick Benton, Martin Hofmann, and Vivek Nigam. 2014. Abstract effects and proof-relevant logical relations. In Proceedings of the 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’14), (San Diego, CA, January 20--21, 2014). ACM, New York, 619--632. DOI:https://doi.org/10.1145/2535838.2535869Google ScholarDigital Library
- Sergey Goncharov and Lutz Schröder. 2013. A relatively complete generic Hoare logic for order-enriched effects. In Proceedings of the 28th Annual Symposium on Logic in Computer Science (LICS 2013). IEEE Computer Society, Washington, DC, 273--282.Google ScholarDigital Library
- Andrew D. Gordon and Gareth D. Rees. 1996. Bisimilarity for a first-order calculus of objects with subtyping. In Proceedings of the 23rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’96). ACM, New York, 386--395. DOI:https://doi.org/10.1145/237721.237807Google ScholarDigital Library
- Ichiro Hasuo. 2015. Generic weakest precondition semantics from monads enriched with order. Theoretical Computer Science 604 (2015), 2--29.Google ScholarDigital Library
- Matthew Hennessy and Robin Milner. 1985. Algebraic laws for nondeterminism and concurrency. Journal of the ACM (JACM) 32, 1 (1985), 137--161.Google ScholarDigital Library
- Martin Hofmann. 2015. Logical relations and nondeterminism. In Software, Services, and Systems. Lecture Notes in Computer Science, Rocco De Nicola and Rolf Hennicker (Eds.). Vol. 8950. Springer International Publishing, Cham, 62--74. DOI:https://doi.org/10.1007/978-3-319-15545-6_7Google ScholarCross Ref
- Douglas J. Howe. 1989. Equality in lazy computation systems. In Proceedings of the 4th Annual Symposium on Logic in Computer Science. IEEE Press, Piscataway, NJ, 198--203.Google ScholarCross Ref
- Douglas J. Howe. 1996. Proving congruence of bisimulation in functional programming languages. Information and Computation 124, 2 (1996), 103--112.Google ScholarDigital Library
- Bart Jacobs. 2016. Introduction to Coalgebra: Towards Mathematics of States and Observation. Cambridge University Press, Cambridge, UK.Google Scholar
- Patricia Johann, Alex Simpson, and Janis Voigtländer. 2010. A generic operational metatheory for algebraic effects. In Proceedings of the 2010 25th Annual IEEE Symposium on Logic in Computer Science (LICS’10). IEEE Computer Society, Washington, DC, 209--218. DOI:https://doi.org/10.1109/LICS.2010.29Google ScholarDigital Library
- Shin-ya Katsumata. 2011. Relating computational effects by TT-lifting. In Automata, Languages and Programming, Luca Aceto, Monika Henzinger, and Jiří Sgall (Eds.). Springer Berlin, Berlin, 174--185.Google Scholar
- Vasileios Koutavas, Paul Blain Levy, and Eijiro Sumii. 2011. From applicative to environmental bisimulation. Electronic Notes in Theoretical Computer Science 276 (2011), 215--235. DOI:https://doi.org/10.1016/j.entcs.2011.09.023 (Twenty-seventh Conference on the Mathematical Foundations of Programming Semantics (MFPS XXVII)).Google ScholarDigital Library
- Ugo Dal Lago, Francesco Gavazzo, and Paul Blain Levy. 2017. Effectful applicative bisimilarity: Monads, relators, and Howe’s method. In Ptoceedings of the 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, (LICS 2017), (Reykjavik, Iceland, June 20--23, 2017). IEEE Computer Society, Washington, DC, 1--12. DOI:https://doi.org/10.1109/LICS.2017.8005117Google ScholarCross Ref
- Søren Bøgh Lassen. 1998. Relational reasoning about contexts. In Higher Order Operational Techniques in Semantics, Andrew D. Gordon and Andrew M. Pitts (Eds.). Cambridge University Press, New York, 91--136. http://dl.acm.org/citation.cfm?id=309656.309665Google Scholar
- Søren Bøgh Lassen. 1998. Relational Reasoning about Functions and Nondeterminism. Ph.D Dissertation. BRICS.Google Scholar
- Paul Blain Levy. 2006. Call-by-push-value: Decomposing call-by-value and call-by-name. Higher-Order and Symbolic Computation 19, 4 (2006), 377--414.Google ScholarDigital Library
- Paul Blain Levy. 2011. Similarity quotients as final coalgebras. Lecture Notes in Computer Science, vol. 6604. Springer, Berlin, 27--41.Google Scholar
- Paul Blain Levy, John Power, and Hayo Thielecke. 2003. Modelling environments in call-by-value programming languages. Information and Computation 185, 2 (2003), 182--210.Google ScholarDigital Library
- Aliaume Lopez and Alex Simpson. 2018. Basic operational preorders for algebraic effects in general, and for combined probability and nondeterminism in particular. In Proceedings of the 27th EACSL Annual Conference on Computer Science Logic (CSL 2018) (Leibniz International Proceedings in Informatics (LIPIcs)), Dan Ghica and Achim Jung (Eds.), Vol. 119. Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, 29:1--29:17. DOI:https://doi.org/10.4230/LIPIcs.CSL.2018.29Google ScholarCross Ref
- Kenji Maillard, Danel Ahman, Robert Atkey, Guido Martínez, Catalin Hritcu, Exequiel Rivas, and Éric Tanter. 2019. Dijkstra monads for all. In Proceedings of the 24th ACM SIGPLAN International Conference on Functional Programming (ICFP). ACM, New York. https://arxiv.org/abs/1903.01237.Google ScholarDigital Library
- Gregory Malecha, Greg Morrisett, and Ryan Wisnesky. 2011. Trace-based verification of imperative programs with I/O. J. Symb. Comput. 46, 2 (Feb. 2011), 95--118. DOI:https://doi.org/10.1016/j.jsc.2010.08.004Google ScholarDigital Library
- Robin Milner. 1982. A Calculus of Communicating Systems. Springer-Verlag New York, Inc., Secaucus, NJ.Google Scholar
- Eugenio Moggi. 1991. Notions of computation and monads. Information and Computation 93, 1 (1991), 55--92.Google ScholarDigital Library
- Till Mossakowski, Lutz Schröder, and Sergey Goncharov. 2010. A generic complete dynamic logic for reasoning about purity and effects. Formal Aspects of Computing 22, 3--4 (2010), 363--384.Google ScholarDigital Library
- Aleksandar Nanevski, J. Gregory Morrisett, and Lars Birkedal. 2008. Hoare type theory, polymorphism and separation. J. Funct. Program. 18 (2008), 865--911.Google ScholarDigital Library
- C.-H. Luke Ong. 1993. Non-determinism in a functional setting. In Symposium on Logic in Computer Science, Montreal, Ont., Canada. 8 (1993), 275--286.Google Scholar
- David Park. 1981. Concurrency and automata on infinite sequences. Lecture Notes in Computer Science, vol. 154. Springer, Berlin, 561--572.Google Scholar
- Willem Penninckx, Bart Jacobs, and Frank Piessens. 2015. Sound, modular and compositional verification of the input/output behavior of programs. In Programming Languages and Systems, Jan Vitek (Ed.). Springer Berlin, Berlin, 158--182.Google Scholar
- Andrew Pitts. 1991. Evaluation logic. In Proceedings of 4th Higher Order Workshop. Springer London, London, 162--189.Google ScholarCross Ref
- Andrew M. Pitts. 2000. Parametric polymorphism and operational equivalence. Mathematical Structures in Computer Science 10, 3 (June 2000), 321--359. DOI:https://doi.org/10.1017/S0960129500003066Google ScholarDigital Library
- A. M. Pitts. 2005. Typed operational reasoning. In Advanced Topics in Types and Programming Languages, B. C. Pierce (Ed.). The MIT Press, London, UK, Chapter 7, 245--289.Google Scholar
- Gordon Plotkin. 1977. LCF considered as a programming language. Theoretical Computer Science 5, 3 (1977), 223--255.Google ScholarCross Ref
- Gordon Plotkin. 2009. Adequacy for infinitary algebraic effects. In Proceedings of the 3rd International Conference on Algebra and Coalgebra in Computer Science (CALCO’09). Springer-Verlag, Berlin, 1--2. http://dl.acm.org/citation.cfm?id=1812941.1812943Google ScholarDigital Library
- Gordon Plotkin and John Power. 2001. Adequacy for algebraic effects. In Foundations of Software Science and Computation Structures. Springer Berlin, Berlin, 1--24.Google Scholar
- Gordon Plotkin and John Power. 2002. Notions of computation determine monads. In Proceedings of the 5th International Conference on Foundations of Software Science and Computation Structures. Springer-Verlag, London, UK, 342--356.Google ScholarDigital Library
- Gordon Plotkin and Matija Pretnar. 2008. A logic for algebraic effects. In Proceedings of Logic in Computer Science. IEEE Computer Society, Washington, DC, 118--129.Google ScholarDigital Library
- Gordon D. Plotkin and Matija Pretnar. 2013. Handling algebraic effects. Logical Methods in Computer Science 9, 4 (2013), 1--36. DOI:https://doi.org/10.2168/LMCS-9(4:23)2013Google ScholarCross Ref
- Amir Pnueli. 1977. The temporal logic of programs. In Proceedings of the 18th Annual Symposium on the Foundations of Computer Science. IEEE Computer Society, Washington, DC, 46--57.Google ScholarDigital Library
- Davide Sangiorgi. 2011. Introduction to Bisimulation and Coinduction. Cambridge University Press, Cambridge, UK.Google Scholar
- Davide Sangiorgi, Naoki Kobayashi, and Eijiro Sumii. 2011. Environmental bisimulations for higher-order languages. ACM Trans. Program. Lang. Syst. 33, 1, Article 5 (Jan. 2011), 69 pages. DOI:https://doi.org/10.1145/1889997.1890002Google ScholarDigital Library
- Davide Sangiorgi and Jan Rutten (Eds.). 2011. Advanced Topics in Bisimulation and Coinduction. Cambridge University Press, Cambridge, UK. DOI:https://doi.org/10.1017/CBO9780511792588Google ScholarCross Ref
- Alex Simpson and Niels Voorneveld. 2018. Behavioural equivalence via modalities for algebraic effects. In Programming Languages and Systems. Springer International Publishing, Cham, 300--326.Google Scholar
- Nikhil Swamy, Catalin Hritcu, Chantal Keller, Aseem Rastogi, Antoine Delignat-Lavaud, Simon Forest, Karthikeyan Bhargavan, Cédric Fournet, Pierre-Yves Strub, Markulf Kohlweiss, Jean-Karim Zinzindohoué, and Santiago Zanella-Béguelin. 2016. Dependent types and multi-monadic effects in F*. In Proceedings of the 43rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL). ACM, New York, 256--270. https://www.fstar-lang.org/papers/mumon/.Google ScholarDigital Library
- Nikhil Swamy, Joel Weinberger, Cole Schlesinger, Juan Chen, and Benjamin Livshits. 2013. Verifying higher-order programs with the dijkstra monad. SIGPLAN Notes 48, 6 (June 2013), 387--398. DOI:https://doi.org/10.1145/2499370.2491978Google ScholarDigital Library
- Albert Marchienus Thijs. 1996. Simulation and fixpoint semantics. Ph.D Dissertation. Rijksuniversiteit Groningen.Google Scholar
- Rob van Glabbeek and Gordon Plotkin. 2010. On CSP and the Algebraic Theory of Effects. Springer London, London, 333--369. DOI:https://doi.org/10.1007/978-1-84882-912-1_15Google ScholarCross Ref
- Niels Voorneveld. 2019. Quantitative logics for equivalence of effectful programs. In Proceedings of the 35th Conference on Mathematical Foundations of Progamming Semantics, (MFPS XXXV).Google ScholarDigital Library
Index Terms
- Behavioural Equivalence via Modalities for Algebraic Effects
Recommendations
Quantitative Logics for Equivalence of Effectful Programs
AbstractIn order to reason about effects, we can define quantitative formulas to describe behavioural aspects of effectful programs. These formulas can for example express probabilities that (or sets of correct starting states for which) a program ...
Quantitative Behavioural Reasoning for Higher-order Effectful Programs: Applicative Distances
LICS '18: Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer ScienceThis paper studies quantitative refinements of Abramsky's applicative similarity and bisimilarity in the context of a generalisation of Fuzz, a call-by-value λ-calculus with a linear type system that can express program sensitivity, enriched with ...
Streams of Approximations, Equivalence of Recursive Effectful Programs
Mathematics of Program ConstructionAbstractBehavioural equivalence for functional languages with algebraic effects and general recursion is often difficult to formalize. When modelling the behaviour of higher-order programs, one often needs to employ multiple coinductive structures ...
Comments