programming language theory Programming language theory (PLT) is a branch of computer science that deals with the design, implementation, analysis, characterization, and classification of formal languages known as programming languages. Programming language theory is clos ...

, the call-by-push-value (CBPV) paradigm, inspired by monads, allows writing semantics for

lambda-calculus Lambda calculus (also written as ''λ''-calculus) is a formal system in mathematical logic for expressing computation based on function abstraction and application using variable binding and substitution. It is a universal model of computation tha ...

without writing two variants to deal with the difference between

call-by-name In a programming language, an evaluation strategy is a set of rules for evaluating expressions. The term is often used to refer to the more specific notion of a ''parameter-passing strategy'' that defines the kind of value that is passed to the f ...

and

call-by-value In a programming language, an evaluation strategy is a set of rules for evaluating expressions. The term is often used to refer to the more specific notion of a ''parameter-passing strategy'' that defines the kind of value that is passed to the f ...

. To do so, CBPV introduces a term language that distinguishes computations and values, according to the slogan ''a value is, a computation does''; this term language has a single evaluation order. However, to evaluate a

term according to either the call-by-name (CBN) or call-by-value (CBV)

reduction strategy In rewriting, a reduction strategy or rewriting strategy is a relation specifying a rewrite for each object or term, compatible with a given reduction relation. Some authors use the term to refer to an evaluation strategy. Definitions Formally, ...

, 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.

References

{{comp-sci-theory-stub Lambda calculus Programming language semantics