Contextual Equivalence in a Probabilistic Call-by-Need Lambda-Calculus
Article No.: 4, Pages 1 - 15
Abstract
To support the understanding of declarative probabilistic programming languages, we introduce a lambda-calculus with a fair binary probabilistic choice that chooses between its arguments with equal probability. The reduction strategy of the calculus is a call-by-need strategy that performs lazy evaluation and implements sharing by recursive let-expressions. Expected convergence of expressions is the limit of the sum of all successful reduction outputs weighted by their probability. We use contextual equivalence as program semantics: two expressions are contextually equivalent if and only if the expected convergence of the expressions plugged into any program context is always the same. We develop and illustrate techniques to prove equivalences including a context lemma, two derived criteria to show equivalences and a syntactic diagram-based method. This finally enables us to show correctness of a large set of program transformations with respect to the contextual equivalence.
References
[1]
AProVE. 2022. Homepage of AProVE. http://aprove.informatik.rwth-aachen.de.
[2]
Zena M. Ariola and Matthias Felleisen. 1997. The call-By-need lambda calculus. JFP 7, 3 (1997), 265–301.
[3]
Zena M. Ariola, Matthias Felleisen, John Maraist, Martin Odersky, and Philip Wadler. 1995. A call-by-need lambda calculus. In POPL 1995. ACM, 233–246. https://doi.org/10.1145/199448.199507
[4]
Martin Avanzini, Gilles Barthe, and Ugo Dal Lago. 2021. On continuation-passing transformations and expected cost analysis. Proc. ACM Program. Lang. 5, ICFP (2021), 1–30. https://doi.org/10.1145/3473592
[5]
Ales Bizjak and Lars Birkedal. 2015. Step-Indexed Logical Relations for Probability. In FoSSaCS 2015(LNCS), Vol. 9034. Springer, 279–294. https://doi.org/10.1007/978-3-662-46678-0_18
[6]
CeTA. 2022. Homepage of CeTA. http://cl-informatik.uibk.ac.at/software/ceta.
[7]
Raphaelle Crubillé and Ugo Dal Lago. 2014. On Probabilistic Applicative Bisimulation and Call-by-Value λ-Calculi. In ESOP 2014(LNCS), Vol. 8410. Springer, 209–228. https://doi.org/10.1007/978-3-642-54833-8_12
[8]
Ugo Dal Lago. 2020. On Probabilistic Λ-Calculi. Cambridge University Press, 121–144. https://doi.org/10.1017/9781108770750.005
[9]
U. Dal Lago and F. Gavazzo. 2019. Effectful Normal Form Bisimulation. In ESOP 2019(LNCS), Vol. 11423. Springer, 263–292. https://doi.org/10.1007/978-3-030-17184-1_10
[10]
Ugo Dal Lago, Giulio Guerrieri, and Willem Heijltjes. 2020. Decomposing Probabilistic Lambda-Calculi. In FoSSaCS 2020(LNCS), Vol. 12077. Springer, 136–156. https://doi.org/10.1007/978-3-030-45231-5_8
[11]
Ugo Dal Lago, Davide Sangiorgi, and Michele Alberti. 2014. On coinductive equivalences for higher-order probabilistic functional programs. In POPL 2014. ACM, 297–308. https://doi.org/10.1145/2535838.2535872
[12]
Ugo Dal Lago and Margherita Zorzi. 2012. Probabilistic operational semantics for the lambda calculus. RAIRO-Theor. Inf. Appl. 46, 3 (2012), 413–450. https://doi.org/10.1051/ita/2012012
[13]
Claudia Faggian and Simona Ronchi Della Rocca. 2019. Lambda Calculus and Probabilistic Computation. In LICS 2019. IEEE, 1–13. https://doi.org/10.1109/LICS.2019.8785699
[14]
Jürgen Giesl, Marc Brockschmidt, Fabian Emmes, Florian Frohn, Carsten Fuhs, Carsten Otto, Martin Plücker, Peter Schneider-Kamp, Thomas Ströder, Stephanie Swiderski, and René Thiemann. 2014. Proving Termination of Programs Automatically with AProVE. In IJCAR 2014(LNCS), Vol. 8562. Springer, 184–191. https://doi.org/10.1007/978-3-319-08587-6_13
[15]
Claire Jones and Gordon D. Plotkin. 1989. A Probabilistic Powerdomain of Evaluations. In LICS 1989. IEEE Computer Society, 186–195. https://doi.org/10.1109/LICS.1989.39173
[16]
Martin Korp, Christian Sternagel, Harald Zankl, and Aart Middeldorp. 2009. Tyrolean Termination Tool 2. In RTA 2009(LNCS), Vol. 5595. Springer, 295–304. https://doi.org/10.1007/978-3-642-02348-4_21
[17]
Arne Kutzner and Manfred Schmidt-Schauß. 1998. A Non-Deterministic Call-by-Need Lambda Calculus. In ICFP 1998. ACM, 324–335. https://doi.org/10.1145/289423.289462
[18]
Ian A. Mason, Scott. F. Smith, and Carolyn. L. Talcott. 1996. From Operational Semantics to Domain Theory. Inf. Comput. 128, 1 (1996), 26–47. https://doi.org/10.1006/inco.1996.0061
[19]
Andrw Moran, David Sands, and Magnus Carlsson. 1999. Erratic Fudgets: A Semantic Theory for an Embedded Coordination Language. In COORDINATION 1999(LNCS), Vol. 1594. Springer, 85–102. https://doi.org/10.1007/3-540-48919-3_8
[20]
Andrw Moran, David Sands, and Magnus Carlsson. 2003. Erratic Fudgets: a semantic theory for an embedded coordination language. Sci. Comput. Program. 46, 1-2 (2003), 99–135. https://doi.org/10.1016/S0167-6423(02)00088-6
[21]
James H. Morris. 1968. Lambda-Calculus Models of Programming Languages. Ph.D. Dissertation. MIT.
[22]
Prakash Panangaden. 1995. The Expressive Power of Indeterminate Primitives in Asynchronous Computation. In FSTTCS 1995(LNCS), Vol. 1026. Springer, 124–150. https://doi.org/10.1007/3-540-60692-0
[23]
Conrad Rau, David Sabel, and Manfred Schmidt-Schauß. 2012. Correctness of Program Transformations as a Termination Problem. In IJCAR 2012(LNCS), Vol. 7364. Springer, 462–476. https://doi.org/10.1007/978-3-642-31365-3_36
[24]
David Sabel. 2019. Automating the Diagram Method to Prove Correctness of Program Transformations. In WPTE 2018(Electronic Proceedings in Theoretical Computer Science), Vol. 289. Open Publishing Association, 17–33. https://doi.org/10.4204/EPTCS.289.2
[25]
David Sabel and Manfred Schmidt-Schauß. 2008. A Call-by-Need Lambda-Calculus with Locally Bottom-Avoiding Choice: Context Lemma and Correctness of Transformations. Math. Structures Comput. Sci. 18, 03 (2008), 501–553. https://doi.org/10.1017/S0960129508006774
[26]
David Sabel, Manfred Schmidt-Schauß, and Luca Maio. 2022. A Probabilistic Call-by-Need Lambda-Calculus – Extended Version. CoRR (2022). https://doi.org/10.48550/ARXIV.2205.14916
[27]
Nasser Saheb-Djahromi. 1978. Probabilistic LCF. In MFCS 1978(LNCS), Vol. 64. Springer, 442–451. https://doi.org/10.1007/3-540-08921-7_92
[28]
Davide Sangiorgi and Valeria Vignudelli. 2019. Environmental Bisimulations for Probabilistic Higher-order Languages. ACM Trans. Program. Lang. Syst. 41, 4 (2019), 22:1–22:64. https://doi.org/10.1145/3350618
[29]
Manfred Schmidt-Schauß and David Sabel. 2010. Closures of may-, should- and must-convergences for contextual equivalence. Inform. Process. Lett. 110, 6 (2010), 232 – 235. https://doi.org/10.1016/j.ipl.2010.01.001
[30]
Manfred Schmidt-Schauß and David Sabel. 2010. On generic context lemmas for higher-order calculi with sharing. Theoret. Comput. Sci. 411, 11-13 (2010), 1521 – 1541. https://doi.org/10.1016/j.tcs.2009.12.001
[31]
Manfred Schmidt-Schauß and David Sabel. 2016. Unification of Program Expressions with Recursive Bindings. In PPDP 2016. ACM, 160–173. https://doi.org/10.1145/2967973.2968603
[32]
Manfred Schmidt-Schauß, David Sabel, and Elena Machkasova. 2011. Counterexamples to applicative simulation and extensionality in non-deterministic call-by-need lambda-calculi with letrec. Inf. Process. Lett. 111, 14 (2011), 711–716. https://doi.org/10.1016/j.ipl.2011.04.011
[33]
Manfred Schmidt-Schauß, Marko Schütz, and David Sabel. 2008. Safety of Nöcker’s Strictness Analysis. JFP 18, 04 (2008), 503–551. https://doi.org/10.1017/S0956796807006624
[34]
René Thiemann and Christian Sternagel. 2009. Certification of Termination Proofs Using CeTA. In TPHOLs 2009(LNCS), Vol. 5674. Springer, 452–468. https://doi.org/10.1007/978-3-642-03359-9_31
[35]
TTT2. 2022. Homepage of TTT2. http://cl-informatik.uibk.ac.at/software/ttt2/.
Index Terms
- Contextual Equivalence in a Probabilistic Call-by-Need Lambda-Calculus
Recommendations
Similarity implies equivalence in a class of non-deterministic call-by-need lambda calculi
It has become a standard approach to reason about contextual equivalence using some notion of (bi)simulation. The main technical task of this approach is to show that (bi)simulation is a (pre)congruence, and hence is sound for reasoning about contextual ...
Congruence of Bisimulation in a Non-Deterministic Call-By-Need Lambda Calculus
We present a call-by-need λ-calculus λND with an erratic non-deterministic operator pick and a non-recursive let. A definition of a bisimulation is given, which has to be based on a further calculus named λ≈, since the naïve bisimulation definition is ...
The call-by-need lambda calculus, revisited
ESOP'12: Proceedings of the 21st European conference on Programming Languages and SystemsThe existing call-by-need λ describe lazy evaluation via equational logics. A programmer can use these logics to safely ascertain whether one term is behaviorally equivalent to another or to determine the value of a lazy program. However, neither of the ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
September 2022
187 pages
ISBN:9781450397032
DOI:10.1145/3551357
Copyright © 2022 ACM.
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 20 September 2022
Check for updates
Author Tags
Qualifiers
- Research-article
- Research
- Refereed limited
Conference
PPDP 2022
PPDP 2022: 24th International Symposium on Principles and Practice of Declarative Programming
September 20 - 22, 2022
Tbilisi, Georgia
Acceptance Rates
Overall Acceptance Rate 230 of 486 submissions, 47%
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 46Total Downloads
- Downloads (Last 12 months)9
- Downloads (Last 6 weeks)0
Reflects downloads up to 20 Nov 2024
Other Metrics
Citations
View Options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign inFull Access
View options
View or Download as a PDF file.
PDFeReader
View online with eReader.
eReaderHTML Format
View this article in HTML Format.
HTML Format