En el cálculo lambda , una rama de la lógica matemática que se ocupa del estudio formal de funciones, una estrategia de reducción es cómo una expresión compleja se reduce a una expresión simple mediante sucesivos pasos de reducción. Es similar, pero sutilmente diferente, a la noción de estrategia de evaluación en informática .
Descripción general
Aproximadamente, una estrategia de reducción es una función que asigna un término de cálculo lambda con expresiones reducibles a una expresión reducible particular, la que se reducirá a continuación. Los lógicos matemáticos han estudiado las propiedades de este sistema durante décadas, y la similitud superficial entre la descripción de las estrategias de evaluación y las estrategias de reducción originalmente engañó a los investigadores de lenguajes de programación para especular que los dos eran idénticos, una creencia que todavía es visible en los libros de texto populares desde principios de este siglo. Década de 1980; [1] estos son, sin embargo, conceptos diferentes. [ cita requerida ]
Plotkin [2] demostró en 1973, sin embargo, que un modelo adecuado de una estrategia de evaluación requiere la formulación de un nuevo axioma para las llamadas a funciones, es decir, un cálculo completamente nuevo. Él valida esta idea con dos cálculos diferentes: uno para llamada por nombre y otro para llamada por valor , cada uno para lenguajes de programación puramente funcionales . También muestra que tal cálculo satisface dos criterios naturales. Primero, un cálculo define una función de evaluación que mapea términos cerrados (representaciones de programas) a respuestas (representaciones de resultados). Este teorema se basa en un teorema convencional de Church-Rosser para el cálculo modificado. La función de evaluación se define mediante el teorema de estandarización tradicional de Curry-Feys. En segundo lugar, el cálculo es un sistema de razonamiento ecuacional sólido con respecto a la noción de equivalencia observacional de Morris . [3]
Veinte años después, Crank y Felleisen mostraron cómo escalar el trabajo de Plotkin a lenguajes con declaraciones de asignación imperativas. [4] Definen cálculos para un lenguaje con variables, funciones, aplicación de funciones y declaración de asignación que capturan las nociones convencionales de paso de parámetros y estrategias de evaluación de una amplia gama de lenguajes de programación. Muestran que cada cálculo satisface los criterios de Plotkin, incluidos los teoremas tradicionales de Church-Rosser y Curry-Feys, respectivamente. Además, introducen un cálculo que reifica la noción de ML de celda de referencia.
Ariola y Felleisen [5] e independientemente Maraist, Odersky y Wadler [6] completaron esta línea de trabajo con el diseño de un cálculo lambda que relaciona precisamente la noción de llamada por necesidad, también conocida como programación funcional perezosa, con un sistema de cálculo ecuacional. A diferencia de los cálculos de llamada por valor y llamada por nombre de Plotkin, este cálculo de llamada por necesidad requiere cuatro axiomas para caracterizar las llamadas a funciones. Chang y Felleisen [7] finalmente pudieron mostrar cómo crear un cálculo por necesidad con un axioma único, pero complejo.
Ver también
- Call-by-push-value , un paradigma semántico que permite tratar tanto la llamada por nombre como la llamada por valor.
- La máquina abstracta de geometría dinámica de interacción es un marco eficiente basado en gráficos para cualquier estrategia de evaluación (consulte la implementación interactiva en línea ).
Referencias
- ^ Estructura e interpretación de programas de computadora por Abelson y Sussman, MIT Press 1983
- ^ Llamada por nombre, llamada por valor y cálculo lambda
- ^ "Lenguajes de programación y cálculo lambda por James Morris, MIT 1968"
- ^ Paso de parámetros y cálculo de Lambda por Crank y Felleisen, Principios de lenguajes de programación 1991
- ^ El cálculo lambda de llamada por necesidad de Ariola y Felleisen, Journal of Functional Programming 1997
- ^ El cálculo lambda de llamada por necesidad de Maraist Odersky y Wadler, Journal of Functional Programming 1999
- ^ El cálculo lambda de llamada por necesidad, revisado por Chang y Felleisen, Simposio europeo sobre programación, 2012