Hostname: page-component-586b7cd67f-2brh9 Total loading time: 0 Render date: 2024-11-23T07:54:16.174Z Has data issue: false hasContentIssue false
  • English
  • Français

Probabilistic operational semantics for the lambda calculus

Published online by Cambridge University Press:  22 June 2012

Ugo Dal Lago  and
Margherita Zorzi
Ugo Dal Lago
Affiliation:
Universitàdi Bologna & EPI FOCUS, Dipartimento di Scienze dell’Informazione Mura Anteo Zamboni, 7, 40127 Bologna, Italy. [email protected]
Margherita Zorzi
Affiliation:
Laboratoire d’Informatique L.I.P.N., Université Paris-Nord, supported by ANR Complice Project, France; [email protected]
Get access

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.

Keywords

Lambda calculusprobabilistic computaionoperational semantics
Type
Research Article
Information
RAIRO - Theoretical Informatics and Applications , Volume 46 , Issue 3 , July 2012 , pp. 413 - 450
Copyright
© EDP Sciences 2012

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

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).
P.-L. Curien and H. Herbelin, The duality of computation, in Proc. of International Conference on Functional Programming (2000) 233–243.
U. Dal Lago and M. Zorzi, Probabilistic operational semantics for the lambda calculus. Long Version. Available at http://arxiv.org/abs/1104.0195, 2012.
Danvy, O. and Filinski, A., Representing control : A study of the CPS transformation. Math. Struct. Comput. Sci. 2 (1992) 361–391. Google Scholar
Danvy, O. and Nielsen, L.R., CPS transformation of beta-redexes. Inform. Process. Lett. 94 (2005) 217–224. Google Scholar
B.A. Davey and H.A. Priestley, Introduction to Lattices and Order. Cambridge University Press (2002).
de’ Liguoro, U. and Piperno, A., Nondeterministic extensions of untyped λ-calculus. Inform. Comput. 122 (1995) 149–177. Google Scholar
Di Pierro, A., Hankin, C. and Wiklicky, H., Probabilistic λ-calculus and quantitative program analysis. J. Logic Comput. 15 (2005) 159–179. Google Scholar
Edalat, A., Domains for computation in mathematics, physics and exact real arithmetic. Bull. Symbolic Logic 3 (1997) 401–452. Google Scholar
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.
Jacobs, B. and Rutten, J., A tutorial on (co)algebras and (co)induction. Bull. EATCS 62 (1996) 222–259. Google Scholar
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.
Leroy, X. and Grall, H., Coinductive big-step operational semantics. Inform. Comput. 207 (2009) 284–304. Google Scholar
E. Moggi, Computational lambda-calculus and monads, in Proc. of IEEE Symposium on Logic in Computer Science. IEEE Computer Society Press (1989) 14–23.
Moggi, E., Notions of computation and monads. Inform. Comput. 93 (1989) 55–92. Google Scholar
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 http://www.cs.cmu.edu/˜fp/papers/prob03.pdf (2003).
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.
Plotkin, G.D., Call-by-name, call-by-value and the λ-calculus. Theoret. Comput. Sci. 1 (1975) 125–159. Google Scholar
Plotkin, G.D., LCF considered as a programming language. Theoret. Comput. Sci. 5 (1977) 223–255. Google Scholar
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.
Rutten, J., Elements of Stream Calculus (An Extensive Exercise In Coinduction). Electron. Notes Theor. Comput. Sci 45 (2001) 358–423. Google Scholar
Saheb-Djaromi, N., Probabilistic LCF, in Proc. of International Symposium on Mathematical Foundations of Computer Science. Lect. Notes Comput. Sci. 64 (1978) 442–451. Google Scholar
D. Sangiorgi, Introduction to Bisimulation and Coinduction. Cambridge University Press (2012).
Selinger, P. and Valiron, B., A lambda calculus for quantum computation with classical control. Math. Struct. Comput. Sci. 16 (2006) 527–552. Google Scholar
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).