Computing Reviews
Today's Issue Hot Topics Search Browse Recommended My Account Log In
Review Help
Search
Environmental bisimulations for probabilistic higher-order languages
Sangiorgi D., Vignudelli V. ACM Transactions on Programming Languages and Systems41 (4):1-64,2019.Type:Article
Date Reviewed: Feb 2 2021

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.

Reviewer:  Markus Wolf Review #: CR147176 (2106-0157)
Bookmark and Share
 
General (D.3.0 )
 
 
Program Analysis (F.3.2 ... )
 
 
Semantics Of Programming Languages (F.3.2 )
 
 
General (F.0 )
 
Would you recommend this review?
yes
no
Other reviews under "General": Date
Programming languages: paradigm and practice
Appleby D., McGraw-Hill, Inc., New York, NY, 1991. Type: Book (9780075579045)
Jan 1 1992
Programming languages
Dershem H. (ed), Jipping M., Wadsworth Publ. Co., Belmont, CA, 1990. Type: Book (9780534129002)
Jan 1 1992
Comparative programming languages
Friedman L., Prentice-Hall, Inc., Upper Saddle River, NJ, 1991. Type: Book (9780131554825)
Jan 1 1992
more...

E-Mail This Printer-Friendly
Send Your Comments
Contact Us
Reproduction in whole or in part without permission is prohibited.   Copyright 1999-2024 ThinkLoud®
Terms of Use
| Privacy Policy