
handle: 11585/586780 , 11585/730806
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.
[INFO.INFO-LO] Computer Science [cs]/Logic in Computer Science [cs.LO], Imperative Languages, Contextual equivalence; Environmental bisimulation; Imperative languages; Probabilistic lambda calculus, Environmental Bisimulation, [INFO] Computer Science [cs], Probabilistic Lambda Calculus, [INFO.INFO-PL] Computer Science [cs]/Programming Languages [cs.PL], Theory of computation → Program verification, Operational semantics, Contextual Equivalence, Environmental bisimulation, Probabilistic computation, [INFO.INFO-FL] Computer Science [cs]/Formal Languages and Automata Theory [cs.FL]
[INFO.INFO-LO] Computer Science [cs]/Logic in Computer Science [cs.LO], Imperative Languages, Contextual equivalence; Environmental bisimulation; Imperative languages; Probabilistic lambda calculus, Environmental Bisimulation, [INFO] Computer Science [cs], Probabilistic Lambda Calculus, [INFO.INFO-PL] Computer Science [cs]/Programming Languages [cs.PL], Theory of computation → Program verification, Operational semantics, Contextual Equivalence, Environmental bisimulation, Probabilistic computation, [INFO.INFO-FL] Computer Science [cs]/Formal Languages and Automata Theory [cs.FL]
| selected citations These citations are derived from selected sources. This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | 16 | |
| popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network. | Top 10% | |
| influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | Top 10% | |
| impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network. | Top 10% |
