Davide Sangiorgi
Abstract
Environmental bisimulations for probabilistic higher-order languages are studied. In contrast with applicative bisimulations, environmental bisimulations are known to be more robust and do not require sophisticated techniques such as Howe’s in the proofs of congruence.
As representative calculi, call-by-name and call-by-value λ-calculus, and a (call-by-value) λ-calculus extended with references (i.e., a store) are considered. In each case, full abstraction results are derived for probabilistic environmental similarity and bisimilarity with respect to contextual preorder and contextual equivalence, respectively. Some possible enhancements of the (bi)simulations, as “up-to techniques,” are also presented.
Probabilities force a number of modifications to the definition of environmental bisimulations in non-probabilistic languages. Some of these modifications are specific to probabilities, others may be seen as general refinements of environmental bisimulations, applicable also to non-probabilistic languages. Several examples are presented, to illustrate the modifications and the differences.
- Martín Abadi and Andrew D. Gordon. 1998. A bisimulation method for cryptographic protocols. In Proceedings of the European Symposium on Programming (ESOP’98) (LNCS), Chris Hankin (Ed.), Vol. 1381. Springer, 12--26.Google Scholar
- Samson Abramsky. 1990. The lazy lambda calculus. In Research Topics in Functional Programming, David A. Turner (Ed.). Addison-Wesley, 65--116.Google ScholarDigital Library
- Andrés Aristizábal, Dariusz Biernacki, Sergueï Lenglet, and Piotr Polesiuk. 2016. Environmental bisimulations for delimited-control operators with dynamic prompt generation. In Proceedings of the International Conference on Formal Structures for Computation and Deduction (FSCD’16). 9:1--9:17.Google Scholar
- Dariusz Biernacki and Sergueï Lenglet. 2013. Environmental bisimulations for delimited-control operators. In Proceedings of the Asian Symposium on Programming Languages and Systems (APLAS’13) (LNCS), Vol. 8301. Springer, 333--348.Google ScholarDigital Library
- Aleš Bizjak. 2016. On Semantics and Applications of Guarded Recursion. Ph.D. Dissertation. Aarhus University.Google Scholar
- Ales Bizjak and Lars Birkedal. 2015. Step-indexed logical relations for probability. In Proceedings of the International Conference on Foundations of Software Science and Computation Structures (FoSSaCS’15). 279--294.Google ScholarCross Ref
- M. Boreale and D. Sangiorgi. 1998. Bisimulation in name-passing calculi without matching. In Proceedings of the ACM/IEEE Symposium on Logic in Computer Science (LICS’98). IEEE Computer Society Press.Google Scholar
- Raphaëlle Crubillé and Ugo Dal Lago. 2014. On probabilistic applicative bisimulation and call-by-value λ-calculi. In Proceedings of the European Symposium on Programming (ESOP’14) (LNCS), Vol. 8410. Springer, 209--228.Google ScholarDigital Library
- Raphaëlle Crubillé and Ugo Dal Lago. 2015. Metric reasoning about λ-terms: The affine case. In Proceedings of the ACM/IEEE Symposium on Logic in Computer Science (LICS’15). IEEE, 633--644.Google Scholar
- Raphaëlle Crubillé, Ugo Dal Lago, Davide Sangiorgi, and Valeria Vignudelli. 2015. On applicative similarity, sequentiality, and full abstraction. In Correct System Design, Roland Meyer, André Platzer, and Heike Wehrheim (Eds.). Springer, 65--82.Google Scholar
- Ugo Dal Lago, Davide Sangiorgi, and Michele Alberti. 2014. On coinductive equivalences for higher-order probabilistic functional programs. In Proceedings of the ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’14). ACM, 297--308.Google ScholarDigital Library
- Ugo Dal Lago and Margherita Zorzi. 2012. Probabilistic operational semantics for the lambda calculus. RAIRO Theor. Info. Appl. 46, 3 (2012), 413--450.Google ScholarCross Ref
- Vincent Danos and Russell S. Harmer. 2002. Probabilistic game semantics. ACM Trans. Comput. Logic 3, 3 (2002), 359--382.Google ScholarDigital Library
- Josee Desharnais, Radha Jagadeesan, Vineet Gupta, and Prakash Panangaden. 2002. The metric analogue of weak bisimulation for probabilistic processes. In Proceedings of the ACM/IEEE Symposium on Logic in Computer Science (LICS’02). IEEE Computer Society, 413--422.Google ScholarCross Ref
- Josée Desharnais, François Laviolette, and Mathieu Tracol. 2008. Approximate analysis of probabilistic processes: Logic, simulation and games. In Proceedings of the International Conference on Quantitative Evaluation of Systems (QEST’08). IEEE Computer Society, 264--273.Google ScholarDigital Library
- Thomas Ehrhard, Christine Tasson, and Michele Pagani. 2014. Probabilistic coherence spaces are fully abstract for probabilistic PCF. In Proceedings of the ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’14). 309--320.Google ScholarDigital Library
- Andrew D. Gordon. 1995. Bisimilarity as a theory of functional programming. Electr. Notes Theor. Comput. Sci. 1 (1995), 232--252.Google ScholarCross Ref
- Jean Goubault-Larrecq. 2015. Full abstraction for non-deterministic and probabilistic extensions of PCF I: The angelic cases. J. Logic. Algebra. Methods Program. 84, 1 (2015), 155--184.Google ScholarCross Ref
- Douglas J. Howe. 1996. Proving congruence of bisimulation in functional programming languages. Info. Comput. 124, 2 (1996), 103--112.Google ScholarDigital Library
- Chung-Kil Hur, Derek Dreyer, Georg Neis, and Viktor Vafeiadis. 2012. The marriage of bisimulations and Kripke logical relations. In Proceedings of the ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’12). 59--72.Google ScholarDigital Library
- Guilhem Jaber and Nicolas Tabareau. 2015. Kripke open bisimulation—A marriage of game semantics and operational techniques. In Proceedings of the Asian Symposium on Programming Languages and Systems (APLAS’15). 271--291.Google Scholar
- Radha Jagadeesan, Corin Pitcher, and James Riely. 2009. Open bisimulation for aspects. T. Aspect-Orient. Softw. Dev. 5 (2009), 72--132.Google ScholarDigital Library
- Alan Jeffrey and Julian Rathke. 1999. Towards a theory of bisimulation for local names. In Proceedings of the ACM/IEEE Symposium on Logic in Computer Science (LICS’99). 56--66.Google ScholarCross Ref
- V. Koutavas, P. B. Levy, and E. Sumii. 2011. From applicative to environmental bisimulation. Electr. Notes Theor.Comput. Sci. 276 (2011), 215--235.Google ScholarDigital Library
- Vassileios Koutavas and Mitchell Wand. 2006. Bisimulations for untyped imperative objects. In Proceedings of the European Symposium on Programming (ESOP’06). 146--161.Google ScholarDigital Library
- Vassileios Koutavas and Mitchell Wand. 2006. Small bisimulations for reasoning about higher-order imperative programs. In Proceedings of the ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’06). 141--152.Google ScholarDigital Library
- S. B. Lassen. 1998. Relational Reasoning about Functions and Nondeterminism. Ph.D. Dissertation. University of Aarhus.Google Scholar
- Søren B. Lassen and Paul Blain Levy. 2007. Typed normal form bisimulation. In Proceedings of the Conference on Computer Science Logic (CSL’07) (LNCS), Vol. 4646. Springer, 283--297.Google Scholar
- John Maraist, Martin Odersky, David N. Turner, and Philip Wadler. 1999. Call-by-name, call-by-value, call-by-need and the linear lambda calculus. Theor. Comput. Sci. 228, 1--2 (1999), 175--210.Google ScholarDigital Library
- Robin Milner. 2006. Pure bigraphs: Structure and dynamics. Info. Comput. 204, 1 (2006), 60--122.Google ScholarDigital Library
- John C. Mitchell. 1996. Foundations for Programming Languages. MIT Press.Google ScholarDigital Library
- J. H. Morris Jr. 1968. Lambda-calculus Models of Programming Languages. Ph.D. Dissertation. Massachusetts Institute of Technology.Google Scholar
- Georg Neis, Chung-Kil Hur, Jan-Oliver Kaiser, Craig McLaughlin, Derek Dreyer, and Viktor Vafeiadis. 2015. Pilsner: A compositionally verified compiler for a higher-order imperative language. In Proceedings of the International Conference on Functional Programming (ICFP’15). ACM, New York, NY, USA, 166--178.Google ScholarDigital Library
- D. Park. 1981. A new equivalence notion for communicating systems. In Bulletin EATCS, G. Maurer (Ed.), Vol. 14. 78--80.Google Scholar
- Adrien Piérard and Eijiro Sumii. 2011. Sound bisimulations for higher-order distributed process calculus. In Proceedings of the International Conference on Foundations of Software Science and Computation Structures (FoSSaCS’11). 123--137.Google ScholarCross Ref
- Adrien Piérard and Eijiro Sumii. 2012. A higher-order distributed calculus with name creation. In Proceedings of the ACM/IEEE Symposium on Logic in Computer Science (LICS’12). 531--540.Google ScholarDigital Library
- Andrew Pitts. 2005. Typed operational reasoning. In Advanced Topics in Types and Programming Languages, Benjamin C. Pierce (Ed.). MIT Press, 245--289.Google Scholar
- Andrew Pitts. 2012. Howe’s method for higher-order languages. In Advanced Topics in Bisimulation and Coinduction, D. Sangiorgi and J. Rutten (Eds.). Cambridge Tracts in Theoretical Computer Science, Vol. 52. Cambridge University Press, Cambridge, 197--232.Google Scholar
- Damien Pous and Davide Sangiorgi. 2012. Enhancements of the bisimulation proof method. In Advanced Topics in Bisimulation and Coinduction, Davide Sangiorgi and Jan Rutten (Eds.). Cambridge University Press.Google Scholar
- Jan Rutten and Bart Jacobs. 2012. (Co)algebras and (Co)induction. In Advanced Topics in Bisimulation and Coinduction, Davide Sangiorgi and Jan Rutten (Eds.). Cambridge University Press.Google Scholar
- David Sands. 1997. From SOS rules to proof principles: An operational metatheory for functional languages. In Proceedings of the ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’97). 428--441.Google ScholarDigital Library
- Davide Sangiorgi. 1994. The lazy lambda calculus in a concurrency scenario. Info. Comput. 111, 1 (May 1994), 120--153.Google Scholar
- D. Sangiorgi. 2012. Introduction to Bisimulation and Coinduction. Cambridge University Press, Cambridge.Google Scholar
- Davide Sangiorgi, Naoki Kobayashi, and Eijiro Sumii. 2007. Logical bisimulations and functional languages. In Proceedings of the International Conference on Fundamentals of Software Engineering (FSEN’07) (LNCS). Springer, 364--379.Google ScholarCross Ref
- Davide Sangiorgi, Naoki Kobayashi, and Eijiro Sumii. 2011. Environmental bisimulations for higher-order languages. ACM Trans. Program. Lang. Syst. 33, 1:5 (2011).Google ScholarDigital Library
- Nobuyuki Sato and Eijiro Sumii. 2009. The higher-order, call-by-value applied pi-calculus. In Proceedings of the Asian Symposium on Programming Languages and Systems (APLAS’09). 311--326.Google ScholarDigital Library
- Kristian Støvring and Soren B. Lassen. 2007. A complete, co-inductive syntactic theory of sequential control and state. In Proceedings of the ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’07). 161--172.Google Scholar
- Eijiro Sumii and Benjamin C. Pierce. 2007. A bisimulation for dynamic sealing. Theor. Comput. Sci. 375, 1--3 (2007), 169--192.Google ScholarDigital Library
- Eijiro Sumii and Benjamin C. Pierce. 2007. A bisimulation for type abstraction and recursion. J. ACM 54, 5 (2007).Google ScholarDigital Library
Index Terms
- Environmental Bisimulations for Probabilistic Higher-order Languages
Recommendations
Environmental bisimulations for probabilistic higher-order languages
POPL '16Environmental bisimulations for probabilistic higher-order languages are studied. In contrast with applicative bisimulations, environmental bisimulations are known to be more robust and do not require sophisticated techniques such as Howe’s in the ...
Environmental bisimulations for probabilistic higher-order languages
POPL '16: Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming LanguagesEnvironmental bisimulations for probabilistic higher-order languages are studied. In contrast with applicative bisimulations, environmental bisimulations are known to be more robust and do not require sophisticated techniques such as Howe’s in the ...
Small bisimulations for reasoning about higher-order imperative programs
Proceedings of the 2006 POPL ConferenceWe introduce a new notion of bisimulation for showing contextual equivalence of expressions in an untyped lambda-calculus with an explicit store, and in which all expressed values, including higher-order values, are storable. Our notion of bisimulation ...
Reviews
Markus Wolf
Bisimulation is a technique for proving the behavioral equivalence of labeled transition systems. It is used in the study of calculi, for example, especially in the context of concurrency. The basic idea is to find a relation between program terms such that one can prove for any two terms in relation that a reduction on one of the terms means there is always a reduction on the other term; so, the reduction results are again in relation, and vice versa for the other term. The study of such relations and proof techniques has quite a long history, and this paper adds to this history by studying environmental bisimulations and their use in proving behavioral equivalences for higher-order languages with a probabilistic choice operator. An environmental bisimulation not only puts terms in relations, but rather pairs of terms and environments. This basic idea was proposed in a previous paper in order to ease the treatment of extensions to pure calculus where the usual bisimulation techniques become technically difficult. In order to model the choice aspects of the languages, the environments consist of a recording of the possible choices. This is called a formal sum in the paper, and is a syntactic representation of the probability distribution of possible terms. After a motivating introduction and some technical preliminaries, the paper discusses three languages: call-by-name -calculus, call-by-value -calculus, and an extension of the latter with locations and references. For call-by-name -calculus the notion of an environmental bisimulation is first introduced, illustrated by several examples and investigated. The notion of environmental bisimulation needs to be extended for call-by-value -calculus. A motivating example for this is the fact that a choice between a value and a divergent term under a is equivalent to a choice between two expressions in call-by-name. However, this is no longer the case in a call-by-value scheme. The solution chosen is to allow for the environment to be updated during the bisimulation game. The addition of locations and references leads to the final extension of bisimulation in which the pairs are extended to triples, that is, adding a store to the environment. The resulting final theoretical apparatus is quite heavy, but still manageable. A discussion of related and future work concludes the paper. The read is quite enjoyable, despite its heavy technical flavor, thanks to motivating examples and a clear exposition. Proofs to the small lemmas and theorems are mostly omitted or only sketched, and several concepts related to bisimulation are referenced but not completely explained. For a reader completely new to bisimulations, it is not a good starting point.
Access critical reviews of Computing literature here
Become a reviewer for Computing Reviews.
Comments