On coinductive equivalences for higher-order probabilistic functional programs

DOI10.1145/2535838.2535872MaRDI QIDQ5408426zbMATH OpenOpenAlexFDO

Authors Ugo Dal Lago, Davide Sangiorgi, Michele Alberti

Publication date 10 April 2014

Published in Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1311.1722

zbMATH Keywords

bisimulationcoinductionHowe's technique.probabilistic lambda-calculus

Mathematics Subject Classification ID

Logic in computer science (03B70) Functional programming and lambda calculus (68N18) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87)

Abstract: We study bisimulation and context equivalence in a probabilistic $lambda$-calculus. The contributions of this paper are threefold. Firstly we show a technique for proving congruence of probabilistic applicative bisimilarity. While the technique follows Howe's method, some of the technicalities are quite different, relying on non-trivial "disentangling" properties for sets of real numbers. Secondly we show that, while bisimilarity is in general strictly finer than context equivalence, coincidence between the two relations is attained on pure $lambda$-terms. The resulting equality is that induced by Levy-Longo trees, generally accepted as the finest extensional equivalence on pure $lambda$-terms under a lazy regime. Finally, we derive a coinductive characterisation of context equivalence on the whole probabilistic language, via an extension in which terms akin to distributions may appear in redex position. Another motivation for the extension is that its operational semantics allows us to experiment with a different congruence technique, namely that of logical bisimilarity.

Recommendations

• On probabilistic applicative bisimulation and call-by-value \(\lambda \)-calculi
• scientific article; zbMATH DE number 1231459
• On applicative similarity, sequentiality, and full abstraction
• scientific article; zbMATH DE number 860036
• Proving congruence of bisimulation in functional programming languages

Cited in

(20)

• Effectful applicative similarity for call-by-name lambda calculi
• On bisimilarity in lambda calculi with continuous probabilistic choice
• Program equivalence in linear contexts
• Program equivalence in an untyped, call-by-value functional language with uncurried functions
• On equivalences, metrics, and polynomial time
• Metric reasoning about -terms: the general case
• Contextual equivalence for probabilistic programs with continuous random variables and scoring
• On applicative similarity, sequentiality, and full abstraction
• Applicative bisimulation and quantum -calculi
• scientific article; zbMATH DE number 1231459 (Why is no real title available?)
• Program equivalence is coinductive
• scientific article; zbMATH DE number 860036 (Why is no real title available?)
• The geometry of Bayesian programming
• The discriminating power of the let-in operator in the lazy call-by-name probabilistic \(\lambda\)-calculus
• On the termination problem for probabilistic higher-order recursive programs
• Probabilistic Böhm trees and probabilistic separation
• On probabilistic applicative bisimulation and call-by-value \(\lambda \)-calculi
• Program equivalence in a typed probabilistic call-by-need functional language
• Solvability in a probabilistic setting (invited talk)
• A contextual formalization of structural coinduction

This page was built for publication: On coinductive equivalences for higher-order probabilistic functional programs

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5408426)