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).  Zbl1235.68325
  2. P.-L. Curien and H. Herbelin, The duality of computation, in Proc. of International Conference on Functional Programming (2000) 233–243.  Zbl1321.68146
  3. 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
  4. O. Danvy and A. Filinski, Representing control : A study of the CPS transformation. Math. Struct. Comput. Sci.2 (1992) 361–391.  Zbl0798.68102
  5. O. Danvy and L.R. Nielsen, CPS transformation of beta-redexes. Inform. Process. Lett.94 (2005) 217–224.  Zbl1182.68045
  6. B.A. Davey and H.A. Priestley, Introduction to Lattices and Order. Cambridge University Press (2002).  Zbl1002.06001
  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.  Zbl1070.03008
  9. A. Edalat, Domains for computation in mathematics, physics and exact real arithmetic. Bull. Symbolic Logic3 (1997) 401–452.  Zbl0946.03055
  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.  Zbl0486.60034
  13. B. Jacobs and J. Rutten, A tutorial on (co)algebras and (co)induction. Bull. EATCS62 (1996) 222–259.  Zbl0880.68070
  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.  Zbl0716.06003
  16. X. Leroy and H. Grall, Coinductive big-step operational semantics. Inform. Comput.207 (2009) 284–304.  Zbl1165.68044
  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.  Zbl0716.03007
  18. E. Moggi, Notions of computation and monads. Inform. Comput.93 (1989) 55–92.  Zbl0723.68073
  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.  Zbl1323.68150
  25. J. Rutten, Elements of Stream Calculus (An Extensive Exercise In Coinduction). Electron. Notes Theor. Comput. Sci45 (2001) 358–423.  Zbl1260.68246
  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).  Zbl1252.68008
  28. P. Selinger and B. Valiron, A lambda calculus for quantum computation with classical control. Math. Struct. Comput. Sci.16 (2006) 527–552.  Zbl1122.68033
  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.