This HTML5 document contains 20 embedded RDF statements represented using HTML+Microdata notation.

The embedded RDF content will be recognized by any processor of HTML5 Microdata.

Namespace Prefixes

PrefixIRI
dcthttp://purl.org/dc/terms/
dbohttp://dbpedia.org/ontology/
foafhttp://xmlns.com/foaf/0.1/
dbthttp://dbpedia.org/resource/Template:
rdfshttp://www.w3.org/2000/01/rdf-schema#
freebasehttp://rdf.freebase.com/ns/
rdfhttp://www.w3.org/1999/02/22-rdf-syntax-ns#
owlhttp://www.w3.org/2002/07/owl#
n8http://en.wikipedia.org/wiki/
dbchttp://dbpedia.org/resource/Category:
dbphttp://dbpedia.org/property/
provhttp://www.w3.org/ns/prov#
xsdhhttp://www.w3.org/2001/XMLSchema#
dbrhttp://dbpedia.org/resource/

Statements

Subject Item
dbr:Call-by-push-value
rdfs:label
Call-by-push-value
rdfs:comment
In programming language theory, the call-by-push-value (CBPV) paradigm, inspired by monads, 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 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 lambda-calculus term according to either the call-by-name (CBN) or call-by-value (CBV) reduction 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-
owl:sameAs
freebase:m.012hptls
dbp:wikiPageUsesTemplate
dbt:Technical dbt:Comp-sci-theory-stub
dct:subject
dbc:Lambda_calculus dbc:Programming_language_semantics
prov:wasDerivedFrom
n8:Call-by-push-value?oldid=1047394145&ns=0
dbo:wikiPageID
863579
dbo:wikiPageLength
1903
dbo:wikiPageRevisionID
1047394145
dbo:wikiPageWikiLink
dbr:Reduction_strategy dbr:Evaluation_strategy dbr:Monad_(functional_programming) dbr:Programming_language_theory dbc:Programming_language_semantics dbr:Lambda_calculus dbc:Lambda_calculus
dbo:abstract
In programming language theory, the call-by-push-value (CBPV) paradigm, inspired by monads, 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 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 lambda-calculus term according to either the call-by-name (CBN) or call-by-value (CBV) reduction 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.
foaf:isPrimaryTopicOf
n8:Call-by-push-value