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.
Mots-clés : lambda calculus, probabilistic computaion, operational semantics
@article{ITA_2012__46_3_413_0, author = {Dal Lago, Ugo 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://archive.numdam.org/articles/10.1051/ita/2012012/} }
TY - JOUR AU - Dal Lago, Ugo 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://archive.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 Dal Lago, Ugo %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://archive.numdam.org/articles/10.1051/ita/2012012/ %R 10.1051/ita/2012012 %G en %F ITA_2012__46_3_413_0
Dal Lago, Ugo; 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://archive.numdam.org/articles/10.1051/ita/2012012/
[1] Proofs of randomized algorithms in Coq, in Proc. of Mathematics of Program Construction. Lect. Notes Comput. Sci. 4014 49-68 (2006). | MR | Zbl
and ,[2] The duality of computation, in Proc. of International Conference on Functional Programming (2000) 233-243.
and ,[3] Probabilistic operational semantics for the lambda calculus. Long Version. Available at http://arxiv.org/abs/1104.0195, 2012.
and ,[4] Representing control : A study of the CPS transformation. Math. Struct. Comput. Sci. 2 (1992) 361-391. | MR | Zbl
and ,[5] CPS transformation of beta-redexes. Inform. Process. Lett. 94 (2005) 217-224. | MR | Zbl
and ,[6] Introduction to Lattices and Order. Cambridge University Press (2002). | MR | Zbl
and ,[7] U. de' Liguoro and A. Piperno, Nondeterministic extensions of untyped λ-calculus. Inform. Comput. 122 (1995) 149-177. | MR | Zbl
[8] Probabilistic λ-calculus and quantitative program analysis. J. Logic Comput. 15 (2005) 159-179. | MR | Zbl
, and ,[9] Domains for computation in mathematics, physics and exact real arithmetic. Bull. Symbolic Logic 3 (1997) 401-452. | MR | Zbl
,[10] Integration in real PCF, in Proc. of IEEE Symposium on Logic in Computer Science. Society Press (1996) 382-393. | MR | Zbl
and ,[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 | Zbl
,[13] A tutorial on (co)algebras and (co)induction. Bull. EATCS 62 (1996) 222-259. | Zbl
and ,[14] Probabilistic non-determinism. Ph.D. thesis, University of Edinburgh, Edinburgh, Scotland, UK (1989).
,[15] A probabilistic powerdomain of evaluations, in Proc. of IEEE Symposium on Logic in Computer Science. IEEE Press (1989) 186-195. | Zbl
and ,[16] Coinductive big-step operational semantics. Inform. Comput. 207 (2009) 284-304. | MR | Zbl
and ,[17] Computational lambda-calculus and monads, in Proc. of IEEE Symposium on Logic in Computer Science. IEEE Computer Society Press (1989) 14-23. | Zbl
,[18] Notions of computation and monads. Inform. Comput. 93 (1989) 55-92. | MR | Zbl
,[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] A monadic probabilistic language. Manuscript. Available at http://www.cs.cmu.edu/˜fp/papers/prob03.pdf (2003).
, and ,[21] A probabilistic language based upon sampling functions, in Proc. of ACM Symposium on Principles of Programming Languages 40 (2005) 171-182.
, and ,[22] Call-by-name, call-by-value and the λ-calculus. Theoret. Comput. Sci. 1 (1975) 125-159. | MR | Zbl
,[23] LCF considered as a programming language. Theoret. Comput. Sci. 5 (1977) 223-255. | MR | Zbl
,[24] Stochastic lambda calculus and monads of probability distributions, in Proc. of ACM Symposium on Principles of Programming Languages. ACM Press (2002) 154-165.
and ,[25] Elements of Stream Calculus (An Extensive Exercise In Coinduction). Electron. Notes Theor. Comput. Sci 45 (2001) 358-423. | Zbl
,[26] Probabilistic LCF, in Proc. of International Symposium on Mathematical Foundations of Computer Science. Lect. Notes Comput. Sci. 64 (1978) 442-451. | MR | Zbl
,[27] Introduction to Bisimulation and Coinduction. Cambridge University Press (2012). | MR | Zbl
,[28] A lambda calculus for quantum computation with classical control. Math. Struct. Comput. Sci. 16 (2006) 527-552. | MR | Zbl
and ,[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
,Cité par Sources :