Probabilistic operational semantics for a nondeterministic extension of pure λ-calculus is studied. In this semantics, a term evaluates to a (finite or infinite) distribution of values. Small-step and big-step semantics, inductively and coinductively defined, are given. Moreover, small-step and big-step semantics are shown to produce identical outcomes, both in call-by-value and in call-by-name. Plotkin's CPS translation is extended to accommodate the choice operator and shown correct with respect to the operational semantics. Finally, the expressive power of the obtained system is studied: the calculus is shown to be sound and complete with respect to computable probability distributions.
@article{ITA_2012__46_3_413_0,
author = {Lago, Ugo Dal and Zorzi, Margherita},
title = {Probabilistic operational semantics for the lambda calculus},
journal = {RAIRO - Theoretical Informatics and Applications - Informatique Th\'eorique et Applications},
volume = {46},
year = {2012},
pages = {413-450},
doi = {10.1051/ita/2012012},
mrnumber = {2981677},
zbl = {1279.68183},
language = {en},
url = {http://dml.mathdoc.fr/item/ITA_2012__46_3_413_0}
}
Lago, Ugo Dal; Zorzi, Margherita. Probabilistic operational semantics for the lambda calculus. RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications, Tome 46 (2012) pp. 413-450. doi : 10.1051/ita/2012012. http://gdmltest.u-ga.fr/item/ITA_2012__46_3_413_0/
[1] and , Proofs of randomized algorithms in Coq, in Proc. of Mathematics of Program Construction. Lect. Notes Comput. Sci. 4014 49-68 (2006). | MR 2305855 | Zbl 1235.68325
[2] and , The duality of computation, in Proc. of International Conference on Functional Programming (2000) 233-243.
[3] and , Probabilistic operational semantics for the lambda calculus. Long Version. Available at http://arxiv.org/abs/1104.0195, 2012. | MR 2981677
[4] and , Representing control : A study of the CPS transformation. Math. Struct. Comput. Sci. 2 (1992) 361-391. | MR 1202719 | Zbl 0798.68102
[5] and , CPS transformation of beta-redexes. Inform. Process. Lett. 94 (2005) 217-224. | MR 2135568 | Zbl 1182.68045
[6] and , Introduction to Lattices and Order. Cambridge University Press (2002). | MR 1902334 | Zbl 1002.06001
[7] U. de' Liguoro and A. Piperno, Nondeterministic extensions of untyped λ-calculus. Inform. Comput. 122 (1995) 149-177. | MR 1358023 | Zbl 1096.03502
[8] , and , Probabilistic λ-calculus and quantitative program analysis. J. Logic Comput. 15 (2005) 159-179. | MR 2194620 | Zbl 1070.03008
[9] , Domains for computation in mathematics, physics and exact real arithmetic. Bull. Symbolic Logic 3 (1997) 401-452. | MR 1619397 | Zbl 0946.03055
[10] and , Integration in real PCF, in Proc. of IEEE Symposium on Logic in Computer Science. Society Press (1996) 382-393. | MR 1461850 | Zbl 1005.03035
[11] , Inductive and coinductive techniques in the operational analysis of functional programs : an introduction. Master's thesis, Universita' di Milano, Bicocca (2004).
[12] , A categorical approach to probability theory, in Categorical Aspects of Topology and Analysis, edited by B. Banaschewski. Springer, Berlin, Heidelberg (1982) 68-85. | MR 659884 | Zbl 0486.60034
[13] and , A tutorial on (co)algebras and (co)induction. Bull. EATCS 62 (1996) 222-259. | Zbl 0880.68070
[14] , Probabilistic non-determinism. Ph.D. thesis, University of Edinburgh, Edinburgh, Scotland, UK (1989).
[15] and , A probabilistic powerdomain of evaluations, in Proc. of IEEE Symposium on Logic in Computer Science. IEEE Press (1989) 186-195. | Zbl 0716.06003
[16] and , Coinductive big-step operational semantics. Inform. Comput. 207 (2009) 284-304. | MR 2498711 | Zbl 1165.68044
[17] , Computational lambda-calculus and monads, in Proc. of IEEE Symposium on Logic in Computer Science. IEEE Computer Society Press (1989) 14-23. | Zbl 0716.03007
[18] , Notions of computation and monads. Inform. Comput. 93 (1989) 55-92. | MR 1115262 | Zbl 0723.68073
[19] , A calculus for probabilistic languages, in Proc. of ACM SIGPLAN International Workshop on Types in Languages Design and Implementation. ACM Press (2003) 38-49.
[20] , and , A monadic probabilistic language. Manuscript. Available at http://www.cs.cmu.edu/˜fp/papers/prob03.pdf (2003).
[21] , and , A probabilistic language based upon sampling functions, in Proc. of ACM Symposium on Principles of Programming Languages 40 (2005) 171-182.
[22] , Call-by-name, call-by-value and the λ-calculus. Theoret. Comput. Sci. 1 (1975) 125-159. | MR 429501 | Zbl 0325.68006
[23] , LCF considered as a programming language. Theoret. Comput. Sci. 5 (1977) 223-255. | MR 484798 | Zbl 0369.68006
[24] and , Stochastic lambda calculus and monads of probability distributions, in Proc. of ACM Symposium on Principles of Programming Languages. ACM Press (2002) 154-165.
[25] , Elements of Stream Calculus (An Extensive Exercise In Coinduction). Electron. Notes Theor. Comput. Sci 45 (2001) 358-423. | Zbl 1260.68246
[26] , Probabilistic LCF, in Proc. of International Symposium on Mathematical Foundations of Computer Science. Lect. Notes Comput. Sci. 64 (1978) 442-451. | MR 519861 | Zbl 0396.68037
[27] , Introduction to Bisimulation and Coinduction. Cambridge University Press (2012). | MR 2868379 | Zbl 1252.68008
[28] and , A lambda calculus for quantum computation with classical control. Math. Struct. Comput. Sci. 16 (2006) 527-552. | MR 2243284 | Zbl 1122.68033
[29] , Some unusual λ-calculus numeral systems, in To H.B. Curry : Essays on Combinatory Logic, Lambda Calculus and Formalism, edited by J.P. Seldin and J.R. Hindley. Academic Press (1980). | MR 592792