Environmental bisimulation

Environmental bisimulation is a notion of program equivalence that is based on bisimulation, and is particularly well-suited for higher-order languages.

Environmental bisimulation is similar to applicative bisimulation, in that it is about applying programs to arguments and testing the results. However, environmental bisimulation carries significantly more complex conditions, by allowing the following additional tests Koutavas et al. 2011:

Accumulation of values: In applicative bisimulation, the context may only call related functions it has received from related programs. In environmental bisimulation, the context accumulates the functions it has received, and can call them at will. This is needed when we have state, as functions are not pure anymore.
Resourceful arguments: In applicative bisimulation, the context supplies a single closed value to which related functions get applied. In environmental bisimulation, the context supplies a single open value, closed by corresponding functions from the inventory. Therefore related functions get applied to different arguments.

Both of these types of tests are necessary; otherwise environmental bisimulation is unsound for languages with any of the following: state, exceptions, names, and polymorphism Koutavas et al. 2011.

The notion of environmental simulation originated in bisimulations for higher-order languages with information hiding Sumii and Pierce 2004, Sumii and Pierce 2005. However, it only acquired a name in a LICS 2007 paper Sangiorgi et al. 2007. Many early references to uses of environmental bisimulation can be found in Koutavas et al. 2011.

References

The name of environmental bisimulations was introduced in a LICS 2007 paper. There was then a journal version published in ACM TOPLAS in 2011.

Sangiorgi, Davide, Naoki Kobayashi, and Eijiro Sumii. 2007. ‘Environmental Bisimulations for Higher-Order Languages’. In 22nd Annual IEEE Symposium on Logic in Computer Science (LICS 2007), 293–302. IEEE. https://doi.org/10.1109/LICS.2007.17.

@inproceedings{sangiorgi_environmental_2007,
	title = {Environmental Bisimulations for Higher-Order Languages},
	doi = {10.1109/LICS.2007.17},
	pages = {293--302},
	booktitle = {22nd Annual {IEEE} Symposium on Logic in Computer Science ({LICS} 2007)},
	publisher = {{IEEE}},
	author = {Sangiorgi, Davide and Kobayashi, Naoki and Sumii, Eijiro},
	date = {2007},
}

Sangiorgi, Davide, Naoki Kobayashi, and Eijiro Sumii. 2011. ‘Environmental Bisimulations for Higher-Order Languages’. ACM Transactions on Programming Languages and Systems 33 (1): 1–69. https://doi.org/10.1145/1889997.1890002.

@article{sangiorgi_2011,
	title = {Environmental bisimulations for higher-order languages},
	volume = {33},
	doi = {10.1145/1889997.1890002},
	pages = {1--69},
	number = {1},
	journaltitle = {{ACM} Transactions on Programming Languages and Systems},
	author = {Sangiorgi, Davide and Kobayashi, Naoki and Sumii, Eijiro},
	date = {2011},
}

Koutavas, Vasileios, Paul Blain Levy, and Eijiro Sumii. ‘From Applicative to Environmental Bisimulation’. Electronic Notes in Theoretical Computer Science 276 (September 2011): 215–235. https://doi.org/10.1016/j.entcs.2011.09.023.

@article{koutavas_2011,
	title = {From {Applicative} to {Environmental} {Bisimulation}},
	volume = {276},
	doi = {10.1016/j.entcs.2011.09.023},
	journal = {Electronic Notes in Theoretical Computer Science},
	author = {Koutavas, Vasileios and Levy, Paul Blain and Sumii, Eijiro},
	month = sep,
	year = {2011},
	pages = {215--235},
}

Sumii, Eijiro and Benjamin C. Pierce. ‘A bisimulation for dynamic sealing’. POPL '04: Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages: 161-172. https://doi.org/10.1145/964001.964015

@inproceedings{DBLP:conf/popl/SumiiP04,
  author       = {Eijiro Sumii and
                  Benjamin C. Pierce},
  editor       = {Neil D. Jones and
                  Xavier Leroy},
  title        = {A bisimulation for dynamic sealing},
  booktitle    = {Proceedings of the 31st {ACM} {SIGPLAN-SIGACT} Symposium on Principles
                  of Programming Languages, {POPL} 2004, Venice, Italy, January 14-16,
                  2004},
  pages        = {161--172},
  publisher    = {{ACM}},
  year         = {2004},
  url          = {https://doi.org/10.1145/964001.964015},
  doi          = {10.1145/964001.964015},
  timestamp    = {Fri, 25 Jun 2021 14:48:54 +0200},
  biburl       = {https://dblp.org/rec/conf/popl/SumiiP04.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

Sumii, Eijiro and Benjamin C. Pierce. ’A bisimulation for type abstraction and recursion’. POPL '05: Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages: 63-74. https://doi.org/10.1145/1040305.1040311

@inproceedings{DBLP:conf/popl/SumiiP05,
  author       = {Eijiro Sumii and
                  Benjamin C. Pierce},
  editor       = {Jens Palsberg and
                  Mart{\'{\i}}n Abadi},
  title        = {A bisimulation for type abstraction and recursion},
  booktitle    = {Proceedings of the 32nd {ACM} {SIGPLAN-SIGACT} Symposium on Principles
                  of Programming Languages, {POPL} 2005, Long Beach, California, USA,
                  January 12-14, 2005},
  pages        = {63--74},
  publisher    = {{ACM}},
  year         = {2005},
  url          = {https://doi.org/10.1145/1040305.1040311},
  doi          = {10.1145/1040305.1040311},
  timestamp    = {Sat, 31 Jul 2021 17:22:14 +0200},
  biburl       = {https://dblp.org/rec/conf/popl/SumiiP05.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}