Llamada por valor push

En la teoría de lenguajes de programación , el método call-by-push-value (CBPV) es un lenguaje intermedio que incorpora las estrategias de evaluación call-by-value (CBV) y call-by-name (CBN) . CBPV se estructura como un λ-cálculo polarizado con dos tipos principales: "valores" (+) y "computaciones" (-). ^{[ 1 ]} Las restricciones en las interacciones entre ambos tipos imponen un orden de evaluación controlado, similar a las mónadas o CPS . El cálculo puede incorporar efectos computacionales, como la no terminación, el estado mutable o el no determinismo. Existen traducciones naturales que preservan la semántica desde CBV y CBN a CBPV. Esto significa que al proporcionar una semántica a CBPV y demostrar sus propiedades, se establecen implícitamente también la semántica y las propiedades de CBV y CBN. Paul Blain Levy formuló y desarrolló CBPV en varios artículos y en su tesis doctoral. ^{[ 2 ] [ 3 ] [ 4 ]}

El paradigma CBPV se basa en el lema "un valor es, un cálculo hace". Una complicación en la presentación es distinguir las variables de tipo que abarcan tipos de valor de aquellas que abarcan tipos de cálculo. Este artículo sigue a Levy en el uso de subrayados para denotar cálculos, por lo que${\displaystyle B}$es un tipo de valor (arbitrario) pero${\displaystyle {\underline {B}}}$es un tipo de cálculo. ^{[ 4 ]} Algunos autores utilizan otras convenciones, como conjuntos distintos de letras. ^{[ 5 ]}

El conjunto exacto de construcciones varía según el autor y el uso deseado para el cálculo, pero las siguientes construcciones son típicas: ^{[ 2 ] [ 4 ]}

• Las lambdas λx.Mson cálculos de tipo${\displaystyle A\to {\underline {B}}}$, dónde${\displaystyle x:A}$y${\displaystyle M:{\underline {B}}}$. Una aplicación lambda F Vo V'Fes un cálculo de tipo${\displaystyle {\underline {B}}}$, dónde${\displaystyle V:A}$y${\displaystyle F:A\to {\underline {B}}}$La construcción de enlace let let { x_1 = V_1; ... }. Mvincula valores x_1a valores V_1de tipos coincidentes .${\displaystyle A_{1}}$, dentro de un cálculo M :${\displaystyle {\underline {B}}}$.
• Un thunk thunk Mes un valor de tipo${\displaystyle U{\underline {A}}}$construido a partir de un cálculo Mde tipo${\displaystyle {\underline {A}}}$Forzar una operación lógica es un cálculo force X :${\displaystyle {\underline {A}}}$para un thunk X :${\displaystyle U{\underline {A}}}$.
• También es posible envolver un valor Vde tipo${\displaystyle A}$como un cálculo return V :${\displaystyle FA}$Dicho cálculo puede utilizarse dentro de otro cálculo como M to x. N :${\displaystyle {\underline {B}}}$, dónde M :${\displaystyle FA}$, y N :${\displaystyle {\underline {B}}}$es un cálculo.
• Los valores también pueden incluir tipos de datos algebraicos construidos a partir de una etiqueta y cero o más subvalores, mientras que los cálculos incluyen una coincidencia de patrones deconstructiva match V as { (1,...) in M_1, ... }. Según la presentación, los tipos de datos algebraicos pueden limitarse a sumas y productos binarios, solo a valores booleanos o incluso omitirse por completo.

Un programa es un cálculo cerrado de tipo${\displaystyle FA}$, dónde${\displaystyle A}$es un tipo ADT terrestre. ^{[ 4 ]}

La traducción CBV produce valores CBPV para cada expresión. Una función CBV λx.M :${\displaystyle A\to _{v}B}$se traduce a :thunk λx.Mv ${\displaystyle U(A^{v}\a FB^{v})}$. Una aplicación CBV M N :${\displaystyle A}$se traduce en un cálculo de tipoMv to f in Nv to x in x'(force f)${\displaystyle FA}$, haciendo explícito el orden de evaluación. Una coincidencia de patrón match V as { (1,...) in M_1, ... }se traduce como . Los valores se envuelven con cuando es necesario, pero de lo contrario permanecen sin modificar. ^{[ 2 ]} En algunas traducciones, puede ser necesaria la secuenciación, como al traducir a . ^{[ 4 ]}Vv to z in match z as { (1,...) in M_1v, ... }returninl MM to x. return inl x

La traducción CBN produce cálculos CBPV para cada expresión. Una función CBN λx.M :${\displaystyle A\to B}$traduce sin alteraciones, :λx.MN ${\displaystyle (UA^{n})\to X^{n}}$. Una solicitud del Banco Central de Nigeria M N :${\displaystyle C}$se traduce en un cálculo de tipoMv (thunk Nv)${\displaystyle C^{n}}$. Una coincidencia de patrón match V as { (1,...) in M_1, ... }se traduce de forma similar a CBN como . Los valores ADT se envuelven con , pero y también son necesarios en la estructura interna. La traducción de Levy supone que , lo cual de hecho se cumple. ^{[ 2 ]}Vn to z in match z as { (1,...) in M_1n, ... }returnforcethunkM = force (thunk M)

También es posible extender CBPV para modelar la llamada por necesidad, introduciendo una M need x. Nconstrucción que permite el intercambio visible. Esta construcción tiene una semántica similar a M name x. N = (λy.N[x ↦ (force y)])(thunk M), excepto que con la needconstrucción, el thunk de Mse evalúa como máximo una vez. ^{[ 6 ]}

Algunos autores han señalado que CBPV puede simplificarse eliminando el constructor de tipo U (thunks) ^{[ 7 ]} o el constructor de tipo F (computaciones que devuelven valores). ^{[ 8 ]} Egger y Møgelberg justifican la omisión de U en función de una sintaxis simplificada y para evitar la complejidad de las conversiones inferibles de computaciones a valores. Esta elección convierte los tipos de computaciones en un subconjunto de los tipos de valores, y entonces es natural expandir los tipos de funciones a un espacio de funciones completo entre valores. Denominan a su cálculo "Cálculo de Efectos Enriquecidos". Este cálculo modificado es equivalente a un superconjunto de CBPV mediante una traducción bidireccional que preserva la semántica. ^{[ 7 ]} Ehrhard, en cambio, omite el constructor de tipo F, convirtiendo los valores en un subconjunto de computaciones. Ehrhard renombra las computaciones como "tipos generales" para reflejar mejor su semántica. Este cálculo modificado, el "cálculo lambda semipolarizado", tiene estrechas conexiones con la lógica lineal . ^{[ 8 ] [ 9 ]} Se puede traducir bidireccionalmente a un subconjunto de una variante totalmente polarizada de CBPV. ^{[ 10 ]}

Paul Blain Levy recibió el Premio Alonzo Church 2025 por su trabajo en CBPV. ^{[ 11 ]}

• Programación de funciones computables