Content deleted Content added
→Translation: call-by-need |
→Award: m capitalization |
||
| (12 intermediate revisions by 9 users not shown) | |||
Line 1:
{{Short description|Intermediate language}}
In [[programming language theory]], '''call-by-push-value''' (CBPV) is an [[intermediate language]] that embeds the [[call-by-value]] (CBV) and [[call-by-name]] (
▲In [[programming language theory]], '''call-by-push-value''' (CBPV) is an [[intermediate language]] that embeds the [[call-by-value]] (CBV) and [[call-by-name]] (CBV) [[evaluation strategy|evaluation strategies]]. CBPV is structured as a polarized [[λ-calculus]] with two main types, "values" (+) and "computations" (-).<ref name="Kavvos2020">{{cite journal |last1=Kavvos |first1=G. A. |last2=Morehouse |first2=Edward |last3=Licata |first3=Daniel R. |last4=Danner |first4=Norman |title=Recurrence extraction for functional programs through call-by-push-value |journal=Proceedings of the ACM on Programming Languages |date=January 2020 |volume=4 |issue=POPL |pages=1–31 |doi=10.1145/3371083 |url=https://dl.acm.org/doi/pdf/10.1145/3371083 |language=en |issn=2475-1421}}</ref> Restrictions on interactions between the two types enforce a controlled order of evaluation, similar to [[Monad (functional programming)|monad]]s or [[continuation passing style|CPS]]. The calculus can embed computational effects, such as nontermination, mutable state, or nondeterminism. There are natural semantics-preserving translations from CBV and CBN into CBPV. This means that giving a CBPV semantics and proving its properties implicitly establishes CBV and CBN semantics and properties as well. Paul Blain Levy formulated and developed CBPV in several papers and his doctoral thesis.<ref name="Levy99">{{Cite conference |last=Blain Levy |first=Paul |date=April 1999 |title=Call-by-Push-Value: A Subsuming Paradigm |conference=Typed Lambda Calculi and Applications, 4th International Conference, TLCA'99, L'Aquila, Italy |series=Lecture Notes in Computer Science |volume=1581 |pages=228–242|url=https://www.cs.bham.ac.uk/~pbl/papers/tlca99.pdf}}</ref><ref name="Levy2003">{{cite book |last1=Levy |first1=Paul Blain |title=Call-by-push-value: a functional/imperative synthesis |date=2003 |publisher=Kluwer Academic Publishers |___location=Dordrecht ; Boston |isbn=978-1-4020-1730-8|url=https://www.cs.bham.ac.uk/~pbl/papers/thesisqmwphd.pdf}}</ref><ref name="Levy2022">{{cite journal |last1=Levy |first1=Paul Blain |title=Call-by-push-value |journal=ACM SIGLOG News |date=April 2022 |volume=9 |issue=2 |pages=7–29 |doi=10.1145/3537668.3537670}}</ref>
== Definition ==
Line 29 ⟶ 28:
It is also possible to extend CBPV to model call-by-need, by introducing a <code>M need x. N</code> construct that allows visible sharing. This construct has semantics similar to <code>M name x. N = (λy.N[x ↦ (force y)])(thunk M)</code>, except that with the <code>need</code> construct, the thunk of <code>M</code> is evaluated at most once.<ref>{{cite book |last1=McDermott |first1=Dylan |last2=Mycroft |first2=Alan |chapter=Extended Call-by-Push-Value: Reasoning About Effectful Programs and Evaluation Order |title=Programming Languages and Systems |date=2019 |pages=235–262 |doi=10.1007/978-3-030-17184-1_9 |isbn=978-3-030-17184-1 |publisher=Springer International Publishing |language=en}}</ref>
== Modifications ==
Some authors have noted that CBPV can be simplified, by removing either the U type constructor (thunks)<ref name="Egger2014">{{cite journal |last1=Egger |first1=J. |last2=Mogelberg |first2=R. E. |last3=Simpson |first3=A. |title=The enriched effect calculus: syntax and semantics |journal=Journal of Logic and Computation |date=1 June 2014 |volume=24 |issue=3 |pages=615–654 |doi=10.1093/logcom/exs025 |url=https://www.pure.ed.ac.uk/ws/portalfiles/portal/12289301/eec.pdf}}</ref> or the F type constructor (computations returning values).<ref name="Ehrhard2016">{{cite book |last1=Ehrhard |first1=Thomas |chapter=Call-By-Push-Value from a Linear Logic Point of View |title=Programming Languages and Systems |series=Lecture Notes in Computer Science |date=2016 |volume=9632 |pages=202–228 |doi=10.1007/978-3-662-49498-1_9|doi-access=free|isbn=978-3-662-49497-4 }}</ref> Egger and Mogelberg justify omitting U on the grounds of streamlined syntax and avoiding the clutter of inferable conversions from computations to values. This choice makes computation types a subset of value types, and it is then natural to expand function types to a full function space between values. They term their calculus the "Enriched Effects Calculus". This modified calculus is equivalent to a superset of CBPV via a bidirectional semantics-preserving translation.<ref name="Egger2014"/> Ehrhard in contrast omits the F type constructor, making values a subset of computations. Ehrhard renames computations to "general types" to better reflect their semantics. This modified calculus, the "half-polarized lambda calculus", has close connections to linear logic.<ref name="Ehrhard2016"/><ref>{{cite book |last1=Chouquet |first1=Jules |last2=Tasson |first2=Christine |title=Taylor expansion for Call-By-Push-Value |date=2020 |publisher=Schloss Dagstuhl – Leibniz-Zentrum für Informatik |series=Leibniz International Proceedings in Informatics |volume=152 |pages=16:1–16:16 |doi=10.4230/LIPIcs.CSL.2020.16 |doi-access=free |isbn=978-3-95977-132-0 |url=https://hal.science/hal-02318600/document}}</ref> It can be translated bidirectionally to a subset of a fully-polarized variant of CBPV.<ref>{{citation |last1=Ehrhard |first1=Thomas |title=A Call-By-Push-Value FPC and its interpretation in Linear Logic |date=July 2015 |url=https://hal.science/hal-01176033/document}}</ref>
== Award ==
Paul Blain Levy received the 2025 [[Alonzo Church Award]] for his work on CBPV.<ref>https://siglog.org/winner-of-the-2025-alonzo-church-award/</ref>
== See also ==
| |||