Probabilistic operational semantics for the lambda calculus
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.

DOI : 10.1051/ita/2012012
Classification : 68Q55, 03B70
Mots clés : lambda calculus, probabilistic computaion, operational semantics
@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},
     pages = {413--450},
     publisher = {EDP-Sciences},
     volume = {46},
     number = {3},
     year = {2012},
     doi = {10.1051/ita/2012012},
     mrnumber = {2981677},
     zbl = {1279.68183},
     language = {en},
     url = {http://www.numdam.org/articles/10.1051/ita/2012012/}
}
TY  - JOUR
AU  - Lago, Ugo Dal
AU  - Zorzi, Margherita
TI  - Probabilistic operational semantics for the lambda calculus
JO  - RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications
PY  - 2012
SP  - 413
EP  - 450
VL  - 46
IS  - 3
PB  - EDP-Sciences
UR  - http://www.numdam.org/articles/10.1051/ita/2012012/
DO  - 10.1051/ita/2012012
LA  - en
ID  - ITA_2012__46_3_413_0
ER  - 
%0 Journal Article
%A Lago, Ugo Dal
%A Zorzi, Margherita
%T Probabilistic operational semantics for the lambda calculus
%J RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications
%D 2012
%P 413-450
%V 46
%N 3
%I EDP-Sciences
%U http://www.numdam.org/articles/10.1051/ita/2012012/
%R 10.1051/ita/2012012
%G en
%F 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) no. 3, pp. 413-450. doi : 10.1051/ita/2012012. http://www.numdam.org/articles/10.1051/ita/2012012/

[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). | MR | Zbl

[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. | MR | Zbl

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

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

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

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

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

[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. | MR | Zbl

[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. | MR | Zbl

[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. | MR | Zbl

[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. | MR | Zbl

[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. | MR | Zbl

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

[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. | MR | Zbl

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

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

[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

Cité par Sources :