research-article

Open access

Environmental Bisimulations for Probabilistic Higher-order Languages

Authors:

Davide Sangiorgi,

Valeria VignudelliAuthors Info & Claims

ACM Transactions on Programming Languages and Systems (TOPLAS), Volume 41, Issue 4

Article No.: 22, Pages 1 - 64

https://doi.org/10.1145/3350618

Published: 12 October 2019 Publication History

All formats PDF

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.

References

[1]

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

[2]

Samson Abramsky. 1990. The lazy lambda calculus. In Research Topics in Functional Programming, David A. Turner (Ed.). Addison-Wesley, 65--116.

Digital Library

Google Scholar

[3]

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

[4]

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.

Digital Library

Google Scholar

[5]

Aleš Bizjak. 2016. On Semantics and Applications of Guarded Recursion. Ph.D. Dissertation. Aarhus University.

Google Scholar

[6]

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.

Crossref

Google Scholar

[7]

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

[8]

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.

Digital Library

Google Scholar

[9]

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

[10]

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

[11]

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.

Digital Library

Google Scholar

[12]

Ugo Dal Lago and Margherita Zorzi. 2012. Probabilistic operational semantics for the lambda calculus. RAIRO Theor. Info. Appl. 46, 3 (2012), 413--450.

Crossref

Google Scholar

[13]

Vincent Danos and Russell S. Harmer. 2002. Probabilistic game semantics. ACM Trans. Comput. Logic 3, 3 (2002), 359--382.

Digital Library

Google Scholar

[14]

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.

Crossref

Google Scholar

[15]

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.

Digital Library

Google Scholar

[16]

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.

Digital Library

Google Scholar

[17]

Andrew D. Gordon. 1995. Bisimilarity as a theory of functional programming. Electr. Notes Theor. Comput. Sci. 1 (1995), 232--252.

Crossref

Google Scholar

[18]

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.

Crossref

Google Scholar

[19]

Douglas J. Howe. 1996. Proving congruence of bisimulation in functional programming languages. Info. Comput. 124, 2 (1996), 103--112.

Digital Library

Google Scholar

[20]

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.

Digital Library

Google Scholar

[21]

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

[22]

Radha Jagadeesan, Corin Pitcher, and James Riely. 2009. Open bisimulation for aspects. T. Aspect-Orient. Softw. Dev. 5 (2009), 72--132.

Digital Library

Google Scholar

[23]

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.

Crossref

Google Scholar

[24]

V. Koutavas, P. B. Levy, and E. Sumii. 2011. From applicative to environmental bisimulation. Electr. Notes Theor.Comput. Sci. 276 (2011), 215--235.

Digital Library

Google Scholar

[25]

Vassileios Koutavas and Mitchell Wand. 2006. Bisimulations for untyped imperative objects. In Proceedings of the European Symposium on Programming (ESOP’06). 146--161.

Digital Library

Google Scholar

[26]

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.

Digital Library

Google Scholar

[27]

S. B. Lassen. 1998. Relational Reasoning about Functions and Nondeterminism. Ph.D. Dissertation. University of Aarhus.

Google Scholar

[28]

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

[29]

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.

Digital Library

Google Scholar

[30]

Robin Milner. 2006. Pure bigraphs: Structure and dynamics. Info. Comput. 204, 1 (2006), 60--122.

Digital Library

Google Scholar

[31]

John C. Mitchell. 1996. Foundations for Programming Languages. MIT Press.

Digital Library

Google Scholar

[32]

J. H. Morris Jr. 1968. Lambda-calculus Models of Programming Languages. Ph.D. Dissertation. Massachusetts Institute of Technology.

Google Scholar

[33]

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.

Digital Library

Google Scholar

[34]

D. Park. 1981. A new equivalence notion for communicating systems. In Bulletin EATCS, G. Maurer (Ed.), Vol. 14. 78--80.

Google Scholar

[35]

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.

Crossref

Google Scholar

[36]

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.

Digital Library

Google Scholar

[37]

Andrew Pitts. 2005. Typed operational reasoning. In Advanced Topics in Types and Programming Languages, Benjamin C. Pierce (Ed.). MIT Press, 245--289.

Google Scholar

[38]

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

[39]

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

[40]

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

[41]

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.

Digital Library

Google Scholar

[42]

Davide Sangiorgi. 1994. The lazy lambda calculus in a concurrency scenario. Info. Comput. 111, 1 (May 1994), 120--153.

Google Scholar

[43]

D. Sangiorgi. 2012. Introduction to Bisimulation and Coinduction. Cambridge University Press, Cambridge.

Google Scholar

[44]

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.

Crossref

Google Scholar

[45]

Davide Sangiorgi, Naoki Kobayashi, and Eijiro Sumii. 2011. Environmental bisimulations for higher-order languages. ACM Trans. Program. Lang. Syst. 33, 1:5 (2011).

Digital Library

Google Scholar

[46]

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.

Digital Library

Google Scholar

[47]

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

[48]

Eijiro Sumii and Benjamin C. Pierce. 2007. A bisimulation for dynamic sealing. Theor. Comput. Sci. 375, 1--3 (2007), 169--192.

Digital Library

Google Scholar

[49]

Eijiro Sumii and Benjamin C. Pierce. 2007. A bisimulation for type abstraction and recursion. J. ACM 54, 5 (2007).

Digital Library

Google Scholar

Cited By

View all

Jagadeesan R(2023)(Towards a) Statistical Probabilistic Lazy Lambda CalculusSamson Abramsky on Logic and Structure in Computer Science and Beyond10.1007/978-3-031-24117-8_28(1073-1094)Online publication date: 2-Aug-2023
https://doi.org/10.1007/978-3-031-24117-8_28
Sabel DSchmidt-Schauß MMaio L(2022)Contextual Equivalence in a Probabilistic Call-by-Need Lambda-CalculusProceedings of the 24th International Symposium on Principles and Practice of Declarative Programming10.1145/3551357.3551374(1-15)Online publication date: 20-Sep-2022
https://dl.acm.org/doi/10.1145/3551357.3551374

Index Terms

Environmental Bisimulations for Probabilistic Higher-order Languages
1. Theory of computation
  1. Models of computation
    1. Probabilistic computation
  2. Semantics and reasoning
    1. Program reasoning
      1. Program verification
    2. Program semantics
      1. Operational semantics

Recommendations

Environmental bisimulations for probabilistic higher-order languages
POPL '16

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 ...
Environmental bisimulations for probabilistic higher-order languages
POPL '16: Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages

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 ...
Small bisimulations for reasoning about higher-order imperative programs
Proceedings of the 2006 POPL Conference

We 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

Reviewer: 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

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Transactions on Programming Languages and Systems

ACM Transactions on Programming Languages and Systems Volume 41, Issue 4

December 2019

186 pages

ISSN:0164-0925

EISSN:1558-4593

DOI:10.1145/3366632

Editor:
Andrew Myers
Cornell University, USA

Issue’s Table of Contents

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 12 October 2019

Accepted: 01 June 2019

Revised: 01 May 2019

Received: 01 July 2017

Published in TOPLAS Volume 41, Issue 4

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article
Research
Refereed

Funding Sources

Université de Lyon, within the program ”Investissements d'Avenir„
H2020-MSCA-RISE project ”Behapi„
ERC H2020 project ”CoVeCe„
LABEX MILYON
REPAS
PACE

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

2
Total Citations
View Citations
327
Total Downloads

Downloads (Last 12 months)154
Downloads (Last 6 weeks)11

Reflects downloads up to 20 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

Jagadeesan R(2023)(Towards a) Statistical Probabilistic Lazy Lambda CalculusSamson Abramsky on Logic and Structure in Computer Science and Beyond10.1007/978-3-031-24117-8_28(1073-1094)Online publication date: 2-Aug-2023
https://doi.org/10.1007/978-3-031-24117-8_28
Sabel DSchmidt-Schauß MMaio L(2022)Contextual Equivalence in a Probabilistic Call-by-Need Lambda-CalculusProceedings of the 24th International Symposium on Principles and Practice of Declarative Programming10.1145/3551357.3551374(1-15)Online publication date: 20-Sep-2022
https://dl.acm.org/doi/10.1145/3551357.3551374

View Options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

HTML Format

View this article in HTML Format.

HTML Format

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Abstract

References

Cited By

Index Terms

Recommendations