Probabilistic operational semantics for the lambda calculus

Dal Lago, Ugo; Zorzi, Margherita

RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications, Tome 46 (2012) no. 3, pp. 413-450

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.

Classification : 68Q55, 03B70
Keywords: lambda calculus, probabilistic computaion, operational semantics

[1] P. Audebaud and C. Paulin-Mohring, Proofs of randomized algorithms in Coq, in Proc. of Mathematics of Program Construction. Lect. Notes Comput. Sci. 4014 49-68 (2006). | Zbl | MR

[2] P.-L. Curien and H. Herbelin, The duality of computation, in Proc. of International Conference on Functional Programming (2000) 233-243.

[3] U. Dal Lago and M. Zorzi, Probabilistic operational semantics for the lambda calculus. Long Version. Available at http://arxiv.org/abs/1104.0195, 2012.

[4] O. Danvy and A. Filinski, Representing control : A study of the CPS transformation. Math. Struct. Comput. Sci. 2 (1992) 361-391. | Zbl | MR

[5] O. Danvy and L.R. Nielsen, CPS transformation of beta-redexes. Inform. Process. Lett. 94 (2005) 217-224. | Zbl | MR

[6] B.A. Davey and H.A. Priestley, Introduction to Lattices and Order. Cambridge University Press (2002). | Zbl | MR

[7] U. de' Liguoro and A. Piperno, Nondeterministic extensions of untyped λ-calculus. Inform. Comput. 122 (1995) 149-177. | Zbl | MR

[8] A. Di Pierro, C. Hankin and H. Wiklicky, Probabilistic λ-calculus and quantitative program analysis. J. Logic Comput. 15 (2005) 159-179. | Zbl | MR

[9] A. Edalat, Domains for computation in mathematics, physics and exact real arithmetic. Bull. Symbolic Logic 3 (1997) 401-452. | Zbl | MR

[10] A. Edalat and M.H. Escard, Integration in real PCF, in Proc. of IEEE Symposium on Logic in Computer Science. Society Press (1996) 382-393. | Zbl | MR

[11] M. Gaboardi, Inductive and coinductive techniques in the operational analysis of functional programs : an introduction. Master's thesis, Universita' di Milano, Bicocca (2004).

[12] M. Giry, A categorical approach to probability theory, in Categorical Aspects of Topology and Analysis, edited by B. Banaschewski. Springer, Berlin, Heidelberg (1982) 68-85. | Zbl | MR

[13] B. Jacobs and J. Rutten, A tutorial on (co)algebras and (co)induction. Bull. EATCS 62 (1996) 222-259. | Zbl

[14] C. Jones, Probabilistic non-determinism. Ph.D. thesis, University of Edinburgh, Edinburgh, Scotland, UK (1989).

[15] C. Jones and G. Plotkin, A probabilistic powerdomain of evaluations, in Proc. of IEEE Symposium on Logic in Computer Science. IEEE Press (1989) 186-195. | Zbl

[16] X. Leroy and H. Grall, Coinductive big-step operational semantics. Inform. Comput. 207 (2009) 284-304. | Zbl | MR

[17] E. Moggi, Computational lambda-calculus and monads, in Proc. of IEEE Symposium on Logic in Computer Science. IEEE Computer Society Press (1989) 14-23. | Zbl

[18] E. Moggi, Notions of computation and monads. Inform. Comput. 93 (1989) 55-92. | Zbl | MR

[19] S. Park, 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] S. Park, F. Pfenning and S. Thrun, A monadic probabilistic language. Manuscript. Available at http://www.cs.cmu.edu/˜fp/papers/prob03.pdf (2003).

[21] S. Park, F. Pfenning and S. Thrun, A probabilistic language based upon sampling functions, in Proc. of ACM Symposium on Principles of Programming Languages 40 (2005) 171-182.

[22] G.D. Plotkin, Call-by-name, call-by-value and the λ-calculus. Theoret. Comput. Sci. 1 (1975) 125-159. | Zbl | MR

[23] G.D. Plotkin, LCF considered as a programming language. Theoret. Comput. Sci. 5 (1977) 223-255. | Zbl | MR

[24] N. Ramsey and A. Pfeffer, Stochastic lambda calculus and monads of probability distributions, in Proc. of ACM Symposium on Principles of Programming Languages. ACM Press (2002) 154-165.

[25] J. Rutten, Elements of Stream Calculus (An Extensive Exercise In Coinduction). Electron. Notes Theor. Comput. Sci 45 (2001) 358-423. | Zbl

[26] N. Saheb-Djaromi, Probabilistic LCF, in Proc. of International Symposium on Mathematical Foundations of Computer Science. Lect. Notes Comput. Sci. 64 (1978) 442-451. | Zbl | MR

[27] D. Sangiorgi, Introduction to Bisimulation and Coinduction. Cambridge University Press (2012). | Zbl | MR

[28] P. Selinger and B. Valiron, A lambda calculus for quantum computation with classical control. Math. Struct. Comput. Sci. 16 (2006) 527-552. | Zbl | MR

[29] C. Wadsworth, 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