# Probabilistic operational semantics for the lambda calculus

Ugo Dal Lago; Margherita Zorzi

RAIRO - Theoretical Informatics and Applications (2012)

- Volume: 46, Issue: 3, page 413-450
- ISSN: 0988-3754

## Access Full Article

top## Abstract

top## How to cite

topLago, Ugo Dal, and Zorzi, Margherita. "Probabilistic operational semantics for the lambda calculus." RAIRO - Theoretical Informatics and Applications 46.3 (2012): 413-450. <http://eudml.org/doc/277837>.

@article{Lago2012,

abstract = {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.},

author = {Lago, Ugo Dal, Zorzi, Margherita},

journal = {RAIRO - Theoretical Informatics and Applications},

keywords = {Lambda calculus; probabilistic computaion; operational semantics; lambda calculus},

language = {eng},

month = {8},

number = {3},

pages = {413-450},

publisher = {EDP Sciences},

title = {Probabilistic operational semantics for the lambda calculus},

url = {http://eudml.org/doc/277837},

volume = {46},

year = {2012},

}

TY - JOUR

AU - Lago, Ugo Dal

AU - Zorzi, Margherita

TI - Probabilistic operational semantics for the lambda calculus

JO - RAIRO - Theoretical Informatics and Applications

DA - 2012/8//

PB - EDP Sciences

VL - 46

IS - 3

SP - 413

EP - 450

AB - 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.

LA - eng

KW - Lambda calculus; probabilistic computaion; operational semantics; lambda calculus

UR - http://eudml.org/doc/277837

ER -

## References

top- 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). Zbl1235.68325
- P.-L. Curien and H. Herbelin, The duality of computation, in Proc. of International Conference on Functional Programming (2000) 233–243. Zbl1321.68146
- U. Dal Lago and M. Zorzi, Probabilistic operational semantics for the lambda calculus. Long Version. Available at , 2012. Zbl1279.68183URIhttp://arxiv.org/abs/1104.0195
- O. Danvy and A. Filinski, Representing control : A study of the CPS transformation. Math. Struct. Comput. Sci.2 (1992) 361–391. Zbl0798.68102
- O. Danvy and L.R. Nielsen, CPS transformation of beta-redexes. Inform. Process. Lett.94 (2005) 217–224. Zbl1182.68045
- B.A. Davey and H.A. Priestley, Introduction to Lattices and Order. Cambridge University Press (2002). Zbl1002.06001
- U. de’ Liguoro and A. Piperno, Nondeterministic extensions of untyped λ-calculus. Inform. Comput.122 (1995) 149–177.
- A. Di Pierro, C. Hankin and H. Wiklicky, Probabilistic λ-calculus and quantitative program analysis. J. Logic Comput.15 (2005) 159–179. Zbl1070.03008
- A. Edalat, Domains for computation in mathematics, physics and exact real arithmetic. Bull. Symbolic Logic3 (1997) 401–452. Zbl0946.03055
- 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.
- M. Gaboardi, Inductive and coinductive techniques in the operational analysis of functional programs : an introduction. Master’s thesis, Universita’ di Milano, Bicocca (2004).
- 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. Zbl0486.60034
- B. Jacobs and J. Rutten, A tutorial on (co)algebras and (co)induction. Bull. EATCS62 (1996) 222–259. Zbl0880.68070
- C. Jones, Probabilistic non-determinism. Ph.D. thesis, University of Edinburgh, Edinburgh, Scotland, UK (1989).
- 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. Zbl0716.06003
- X. Leroy and H. Grall, Coinductive big-step operational semantics. Inform. Comput.207 (2009) 284–304. Zbl1165.68044
- E. Moggi, Computational lambda-calculus and monads, in Proc. of IEEE Symposium on Logic in Computer Science. IEEE Computer Society Press (1989) 14–23. Zbl0716.03007
- E. Moggi, Notions of computation and monads. Inform. Comput.93 (1989) 55–92. Zbl0723.68073
- 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.
- S. Park, F. Pfenning and S. Thrun, A monadic probabilistic language. Manuscript. Available at (2003). URIhttp://www.cs.cmu.edu/˜fp/papers/prob03.pdf
- S. Park, F. Pfenning and S. Thrun, A probabilistic language based upon sampling functions, in Proc. of ACM Symposium on Principles of Programming Languages40 (2005) 171–182.
- G.D. Plotkin, Call-by-name, call-by-value and the λ-calculus. Theoret. Comput. Sci.1 (1975) 125–159.
- G.D. Plotkin, LCF considered as a programming language. Theoret. Comput. Sci.5 (1977) 223–255.
- 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. Zbl1323.68150
- J. Rutten, Elements of Stream Calculus (An Extensive Exercise In Coinduction). Electron. Notes Theor. Comput. Sci45 (2001) 358–423. Zbl1260.68246
- N. Saheb-Djaromi, Probabilistic LCF, in Proc. of International Symposium on Mathematical Foundations of Computer Science. Lect. Notes Comput. Sci.64 (1978) 442–451.
- D. Sangiorgi, Introduction to Bisimulation and Coinduction. Cambridge University Press (2012). Zbl1252.68008
- P. Selinger and B. Valiron, A lambda calculus for quantum computation with classical control. Math. Struct. Comput. Sci.16 (2006) 527–552. Zbl1122.68033
- 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).

## NotesEmbed ?

topTo embed these notes on your page include the following JavaScript code on your page where you want the notes to appear.