Call-by-push-value: Difference between revisions

Revision as of 07:46, 24 December 2014

Revision as of 14:02, 24 December 2014

Line 4:

}}

In [[programming language theory]], the '''call-by-push-value''' ('''CBPV''') paradigm,<ref>{{cite journal|title=Call-by-Push-Value: A Subsuming Paradigm|author=Paul Blain Levy}}</ref> inspired by [[monadMonad (functional programming)|monads]]s, allows writing semantics for lambda-calculus without writing two variants to deal with the difference between '''call-by-name''' and '''call-by-value'''. To do so, CBPV introduced a CBPV term language that distinguishes computations and values, according to the slogan is ''a value is, a computation does''; this term language has a single evaluation order. However, to evaluate a [[lambda-calculus]] term according to either the call-by-name ('''CBN''') or call-by-value ('''CBV''') [[evaluation strategy]], one can translate the term to CBPV using a call-by-name or call-by-value translation strategy, which give rise to different terms. Evaluating the result of the call-by-value translation corresponds to evaluating the original term with the call-by-value strategy; evaluating the result of the call-by-name translation corresponds instead to evaluating the original term with the call-by-name strategy.

This is especially useful when dealing with the semantics of different side effects, such as nontermination, mutable state or nondeterminism. Instead of giving two variants of the semantics, one for the call-by-name evaluation order and one for the call-by-value one, one can simply give a semantics for the CBPV term language; one gets two semantics for lambda-calculus by composing this CBPV semantics with the same CBV and CBN translations from lambda-calculus.

Line 13:

{{stub}}

[[Category:Lambda calculus]]

{{Uncategorized stub|date=December 2014}}

[[Category:Programming language semantics]]