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

Abstract

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

How to cite

top

Lago, 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
  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).  
  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 , 2012.  URIhttp://arxiv.org/abs/1104.0195
  4. O. Danvy and A. Filinski, Representing control : A study of the CPS transformation. Math. Struct. Comput. Sci.2 (1992) 361–391.  
  5. O. Danvy and L.R. Nielsen, CPS transformation of beta-redexes. Inform. Process. Lett.94 (2005) 217–224.  
  6. B.A. Davey and H.A. Priestley, Introduction to Lattices and Order. Cambridge University Press (2002).  
  7. U. de’ Liguoro and A. Piperno, Nondeterministic extensions of untyped λ-calculus. Inform. Comput.122 (1995) 149–177.  
  8. A. Di Pierro, C. Hankin and H. Wiklicky, Probabilistic λ-calculus and quantitative program analysis. J. Logic Comput.15 (2005) 159–179.  
  9. A. Edalat, Domains for computation in mathematics, physics and exact real arithmetic. Bull. Symbolic Logic3 (1997) 401–452.  
  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.  
  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.  
  13. B. Jacobs and J. Rutten, A tutorial on (co)algebras and (co)induction. Bull. EATCS62 (1996) 222–259.  
  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.  
  16. X. Leroy and H. Grall, Coinductive big-step operational semantics. Inform. Comput.207 (2009) 284–304.  
  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.  
  18. E. Moggi, Notions of computation and monads. Inform. Comput.93 (1989) 55–92.  
  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 (2003).  URIhttp://www.cs.cmu.edu/˜fp/papers/prob03.pdf
  21. 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.  
  22. G.D. Plotkin, Call-by-name, call-by-value and the λ-calculus. Theoret. Comput. Sci.1 (1975) 125–159.  
  23. G.D. Plotkin, LCF considered as a programming language. Theoret. Comput. Sci.5 (1977) 223–255.  
  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. Sci45 (2001) 358–423.  
  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.  
  27. D. Sangiorgi, Introduction to Bisimulation and Coinduction. Cambridge University Press (2012).  
  28. P. Selinger and B. Valiron, A lambda calculus for quantum computation with classical control. Math. Struct. Comput. Sci.16 (2006) 527–552.  
  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).  

NotesEmbed ?

top

You must be logged in to post comments.

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

Only the controls for the widget will be shown in your chosen language. Notes will be shown in their authored language.

Tells the widget how many notes to show per page. You can cycle through additional notes using the next and previous controls.

    
                

                
Note: Best practice suggests putting the JavaScript code just before the closing </body> tag.