Elevación de Lambda

El levantamiento lambda es un metaproceso que reestructura un programa informático de manera que las funciones se definan independientemente unas de otras en un ámbito global . Un levantamiento individual transforma una función local (subrutina) en una función global. Es un proceso de dos pasos, que consiste en:

Eliminación de variables libres en la función mediante la adición de parámetros .
Trasladar funciones de un ámbito restringido a un ámbito más amplio o global.

El término "lambda lift" fue introducido por primera vez por Thomas Johnsson alrededor de 1982 y se consideró históricamente como un mecanismo para implementar lenguajes de programación basados en programación funcional . Se utiliza junto con otras técnicas en algunos compiladores modernos .

La elevación de expresiones lambda no es lo mismo que la conversión de cierre . Requiere ajustar todos los puntos de llamada (añadiendo argumentos (parámetros) adicionales) y no introduce un cierre para la expresión lambda elevada. En cambio, la conversión de cierre no requiere ajustar los puntos de llamada, pero sí introduce un cierre para la expresión lambda que asigna variables libres a valores.

La técnica puede utilizarse en funciones individuales, en la refactorización de código , para hacer que una función sea utilizable fuera del ámbito en el que fue escrita. Los levantamientos lambda también pueden repetirse para transformar el programa. Los levantamientos repetidos pueden utilizarse para convertir un programa escrito en cálculo lambda en un conjunto de funciones recursivas , sin lambdas. Esto demuestra la equivalencia de los programas escritos en cálculo lambda y los programas escritos como funciones. ^{[ 1 ]} Sin embargo, no demuestra la solidez del cálculo lambda para la deducción, ya que la reducción eta utilizada en el levantamiento lambda es el paso que introduce problemas de cardinalidad en el cálculo lambda, porque elimina el valor de la variable, sin comprobar primero que solo hay un valor que satisface las condiciones de la variable (véase la paradoja de Curry ).

La elevación de lambda es costosa en tiempo de procesamiento para el compilador. Una implementación eficiente de la elevación de lambda es $O(n^{2})$ en el tiempo de procesamiento para el compilador. ^{[ 2 ]}

En el cálculo lambda sin tipos , donde los tipos básicos son funciones, la elevación puede modificar el resultado de la reducción beta de una expresión lambda. Las funciones resultantes conservarán el mismo significado matemático, pero no se consideran la misma función en el cálculo lambda sin tipos. Véase también igualdad intensional frente a igualdad extensional .

La operación inversa a la elevación de lambda es la caída de lambda . ^{[ 3 ]}

La eliminación de funciones lambda puede acelerar la compilación de programas y aumentar la eficiencia del programa resultante al reducir el número de parámetros y el tamaño de los marcos de pila. Sin embargo, dificulta la reutilización de una función. Una función eliminada está vinculada a su contexto y solo puede utilizarse en un contexto diferente si primero se recupera.

Algoritmo

El siguiente algoritmo es una forma de elevar mediante lambda un programa arbitrario en un lenguaje que no admite cierres como objetos de primera clase :

Renombra las funciones de manera que cada una tenga un nombre único.
Reemplace cada variable libre con un argumento adicional para la función que la contiene y pase ese argumento en cada uso de la función.
Reemplaza cada definición de función local que no tenga variables libres con una función global idéntica.
Repita los pasos 2 y 3 hasta que se eliminen todas las variables libres y las funciones locales.

Si el lenguaje tiene cierres como objetos de primera clase que se pueden pasar como argumentos o que se pueden devolver desde otras funciones, el cierre deberá representarse mediante una estructura de datos que capture las vinculaciones de las variables libres.

Ejemplo

El siguiente programa en OCaml calcula la suma de los números enteros del 1 al 100:

sea rec suma n = si n = 1 entonces 1 sino sea f x = n + x en f ( suma ( n - 1 )) suma 100

( let recSe declara sumcomo una función que puede llamarse a sí misma). La función f, que suma el argumento de sum a la suma de los números menores que el argumento, es una función local. Dentro de la definición de f, n es una variable libre. Comience por convertir la variable libre en un parámetro:

sea rec suma n = si n = 1 entonces 1 sino sea f w x = w + x en f n ( suma ( n - 1 )) suma 100

A continuación, eleva f a una función global:

sea rec f w x = w + x y suma n = si n = 1 entonces 1 sino f n ( suma ( n - 1 )) en suma 100

El siguiente es el mismo ejemplo, esta vez escrito en JavaScript :

// Versión inicialfunción suma ( n ) { función f ( x ) { devolver n + x ; }if ( n == 1 ) return 1 ; else return f ( sum ( n - 1 )); }// Después de convertir la variable libre n en un parámetro formal wfunción suma ( n ) { función f ( w , x ) { return w + x ; }if ( n == 1 ) return 1 ; else return f ( n , sum ( n - 1 )); }// Después de elevar la función f al ámbito globalfunción f ( w , x ) { return w + x ; }función suma ( n ) { si ( n == 1 ) devolver 1 ; de lo contrario devolver f ( n , suma ( n - 1 )); }

Elevación de Lambda versus cierres

El levantamiento de lambda y el cierre son métodos para implementar programas con estructura de bloques . El levantamiento implementa la estructura de bloques eliminándola; todas las funciones se elevan al nivel global. La conversión de cierre proporciona un "cierre" que vincula el marco actual con otros marcos. La conversión de cierre requiere menos tiempo de compilación.

Las funciones recursivas y los programas estructurados en bloques, con o sin elevación, pueden implementarse mediante una implementación basada en pila , que es sencilla y eficiente. Sin embargo, una implementación basada en marco de pila debe ser estricta (eligible) . Esta implementación requiere que la vida útil de las funciones sea la última en entrar, la primera en salir (LIFO). Es decir, la función que más recientemente comenzó su cálculo debe ser la primera en terminar.

Algunos lenguajes funcionales (como Haskell ) se implementan mediante evaluación perezosa , que retrasa el cálculo hasta que se necesita el valor. Esta estrategia ofrece flexibilidad al programador. La evaluación perezosa requiere retrasar la llamada a una función hasta que se solicite el valor calculado por dicha función. Una implementación consiste en registrar una referencia a un "marco" de datos que describe el cálculo, en lugar del valor en sí. Posteriormente, cuando se requiere el valor, se utiliza el marco para calcularlo justo a tiempo. El valor calculado reemplaza entonces la referencia.

El "marco" es similar a un marco de pila , con la diferencia de que no se almacena en la pila. La evaluación perezosa requiere que todos los datos necesarios para el cálculo se guarden en el marco. Si la función se "eleva", el marco solo necesita registrar el puntero a la función y sus parámetros. Algunos lenguajes modernos utilizan la recolección de basura en lugar de la asignación basada en pila para gestionar el ciclo de vida de las variables. En un entorno gestionado con recolección de basura, un cierre registra referencias a los marcos desde los que se pueden obtener valores. En cambio, una función elevada tiene parámetros para cada valor necesario en el cálculo.

Expresiones de Let y cálculo lambda

La expresión `let` es útil para describir operaciones de elevación y eliminación, así como la relación entre ecuaciones recursivas y expresiones lambda. La mayoría de los lenguajes funcionales cuentan con expresiones `let`. Asimismo, los lenguajes de programación estructurados en bloques, como ALGOL y Pascal, son similares en el sentido de que también permiten la definición local de una función para su uso en un ámbito restringido .

La expresión `let` utilizada aquí es una versión totalmente recursiva mutua de `let rec` , tal como se implementa en muchos lenguajes funcionales.

Las expresiones `let` están relacionadas con el cálculo lambda . El cálculo lambda tiene una sintaxis y semántica sencillas, y es útil para describir la elevación de expresiones lambda. Es conveniente describir la elevación de expresiones lambda como una traducción de una expresión lambda a una expresión `let` , y la eliminación de expresiones lambda como el proceso inverso. Esto se debe a que las expresiones `let` permiten la recursión mutua, que, en cierto sentido, es más elevada que la que admite el cálculo lambda. El cálculo lambda no admite la recursión mutua y solo se puede definir una función en el ámbito global más externo.

Las reglas de conversión que describen la traducción sin elevación se dan en el artículo sobre expresiones Let .

Las siguientes reglas describen la equivalencia de las expresiones lambda y let,

Se proporcionarán metafunciones que describen la elevación y la eliminación de lambdas. Una metafunción es una función que recibe un programa como parámetro. El programa actúa como datos para el metaprograma. El programa y el metaprograma se encuentran en diferentes metaniveles.

Se utilizarán las siguientes convenciones para distinguir el programa del metaprograma,

Los corchetes [] se utilizarán para representar la aplicación de funciones en el metaprograma.
En el metaprograma, las variables se representarán con letras mayúsculas. En el programa, las variables se representarán con letras minúsculas.
$\equiv$ se utilizará para igualdades en el metaprograma.
$\_$ representa una variable ficticia o un valor desconocido.

Para simplificar, se aplicará la primera regla que indique coincidencias. Las reglas también presuponen que las expresiones lambda se han preprocesado de manera que cada abstracción lambda tenga un nombre único.

El operador de sustitución se utiliza ampliamente. La expresión $L[G:=S]$ Significa sustituir cada aparición de G en L por S y devolver la expresión. La definición utilizada se extiende para abarcar la sustitución de expresiones, a partir de la definición proporcionada en la página del cálculo lambda . La comparación de expresiones debe verificar la equivalencia alfa (cambio de nombre de las variables).

Elevación de Lambda en el cálculo lambda

Cada elevación lambda toma una abstracción lambda, que es una subexpresión de una expresión lambda, y la reemplaza por una llamada a función (aplicación) a una función que crea. Las variables libres en la subexpresión son los parámetros de la llamada a la función.

Las transformaciones mediante expresiones lambda pueden aplicarse a funciones individuales, en procesos de refactorización de código , para que una función pueda utilizarse fuera del ámbito en el que fue escrita. Estas transformaciones también pueden repetirse, hasta que la expresión no contenga abstracciones lambda, para así transformar el programa.

Elevación Lambda

Una elevación consiste en pasar una subexpresión dentro de una expresión a la parte superior de esa expresión. La expresión puede formar parte de un programa más grande. Esto permite controlar a dónde se eleva la subexpresión. La operación de elevación lambda utilizada para realizar una elevación dentro de un programa es:

\operatorname {lambda-lift-op} [S,L,P]=P[L:=\operatorname {lambda-lift} [S,L]]

La subexpresión puede ser una abstracción lambda o una abstracción lambda aplicada a un parámetro.

Son posibles dos tipos de ascensor.

Ascensor anónimo
Ascensor con nombre

Una elevación anónima tiene una expresión de elevación que es solo una abstracción lambda. Se considera que define una función anónima . Se debe crear un nombre para la función.

Una expresión de elevación con nombre tiene una abstracción lambda aplicada a una expresión. Esta elevación se considera una definición con nombre de una función.

Ascensor anónimo

Un levantamiento anónimo toma una abstracción lambda (llamada S ). Para S ;

Crea un nombre para la función que reemplazará a S (llamada V ). Asegúrate de que el nombre identificado por V no haya sido utilizado.
Agregue parámetros a V , para todas las variables libres en S , para crear una expresión G (consulte make-call ).

La elevación lambda consiste en la sustitución de la abstracción lambda S por una aplicación de función, junto con la adición de una definición para la función.

\operatorname {lambda-lift} [S,L]\equiv \operatorname {let} V:\operatorname {de-lambda} [G=S]\operatorname {in} L[S:=G]

La nueva expresión lambda tiene S sustituido por G: L [ S := G ] significa la sustitución de S por G en L. A las definiciones de función se les ha añadido la definición de función G = S.

En la regla anterior, G es la aplicación de la función que se sustituye por la expresión S. Se define por:

G=\operatorname {make-call} [V,\operatorname {FV} [S]]

donde V es el nombre de la función. Debe ser una variable nueva, es decir, un nombre que no se haya utilizado previamente en la expresión lambda.

V\not \in \operatorname {vars} [\operatorname {let} F\operatorname {in} L]

dónde $\operatorname {vars} [E]$ es una metafunción que devuelve el conjunto de variables utilizadas en E.

Construyendo la llamada

La llamada a la función G se construye agregando parámetros para cada variable en el conjunto de variables libres (representado por V ), a la función H ,

$X\in V\to \operatorname {make-call} [H,V]\equiv \operatorname {make-call} [H,V\cap \neg \{X\}]\ X$
$\operatorname {make-call} [H,\{\}]\equiv H$

Ascensor con nombre

El ascensor con nombre es similar al ascensor anónimo, excepto que se proporciona el nombre de la función V.

\operatorname {lambda-lift} [(\lambda V.E)\ S,L]\equiv \operatorname {let} V:\operatorname {de-lambda} [G=S]\operatorname {in} L[(\lambda V.E)\ S:=E[V:=G]]

En cuanto al levantamiento anónimo, la expresión G se construye a partir de V aplicando las variables libres de S. Se define por:

G=\operatorname {make-call} [V,\operatorname {FV} [S]]

Transformación Lambda-lift

Una transformación de elevación lambda toma una expresión lambda y eleva todas las abstracciones lambda a la parte superior de la expresión. Luego, las abstracciones se traducen en funciones recursivas , lo que elimina las abstracciones lambda. El resultado es un programa funcional de la forma,

$\operatorname {let} M\operatorname {in} N$

donde M es una serie de definiciones de funciones y N es la expresión que representa el valor devuelto.

Por ejemplo,

\operatorname {lambda-lift-tran} [\lambda f.(\lambda x.f\ (x\ x))\ (\lambda x.f\ (x\ x))]\equiv \operatorname {let} p\ f\ x=f\ (x\ x)\land q\ p\ f=(p\ f)\ (p\ f)\operatorname {in} q\ p

La función meta de-let se puede utilizar para convertir el resultado de nuevo en cálculo lambda.

\operatorname {de-let} [\operatorname {lambda-lift-tran} [\lambda f.(\lambda x.f\ (x\ x))\ (\lambda x.f\ (x\ x))]]\equiv (\lambda p.(\lambda q.q\ p)\ \lambda p.\lambda f.(p\ f)\ (p\ f))\ \lambda f.\lambda x.f\ (x\ x)

El procesamiento de la transformación de la expresión lambda es una serie de elevaciones. Cada elevación tiene,

Una subexpresión elegida para ella por la función lift-choice . La subexpresión debe elegirse de manera que pueda convertirse en una ecuación sin lambdas.
El levantamiento se realiza mediante una llamada a la metafunción lambda-lift , descrita en la siguiente sección,

{\begin{cases}\operatorname {lambda-lift-tran} [L]=\operatorname {drop-params-tran} [\operatorname {merge-let} [\operatorname {lambda-apply} [L]]]\\\operatorname {lambda-apply} [L]=\operatorname {lambda-process} [\operatorname {lift-choice} [L],L]\\\operatorname {lambda-process} [\operatorname {none} ,L]=L\\\operatorname {lambda-process} [S,L]=\operatorname {lambda-apply} [\operatorname {lambda-lift} [S,L]]\end{cases}}

Una vez aplicados los ajustes, los alquileres se combinan en un único alquiler.

{\begin{cases}\operatorname {merge-let} [\operatorname {let} V:E\operatorname {in} \operatorname {let} W:F\operatorname {in} G]=\operatorname {merge-let} [\operatorname {let} V,W:E\land F\operatorname {in} G]\\\operatorname {merge-let} [E]=E\end{cases}}

Luego, se aplica la eliminación de parámetros para suprimir aquellos que no son necesarios en la expresión "let". La expresión "let" permite que las definiciones de función se referencien directamente entre sí, mientras que las abstracciones lambda son estrictamente jerárquicas y una función no puede referirse directamente a sí misma.

Elegir la expresión para levantar

Existen dos maneras distintas de seleccionar una expresión para su elevación. La primera trata todas las abstracciones lambda como funciones anónimas. La segunda trata las abstracciones lambda aplicadas a un parámetro como funciones anónimas. Las abstracciones lambda aplicadas a un parámetro tienen una doble interpretación: pueden ser expresiones `let` que definen una función o funciones anónimas. Ambas interpretaciones son válidas.

Estos dos predicados son necesarios para ambas definiciones.

lambda-free - Una expresión que no contiene abstracciones lambda.

{\begin{cases}\operatorname {lambda-free} [\lambda F.X]=\operatorname {false} \\\operatorname {lambda-free} [V]=\operatorname {true} \\\operatorname {lambda-free} [M\ N]=\operatorname {lambda-free} [M]\land \operatorname {lambda-free} [N]\end{cases}}

lambda-anon - Una función anónima. Una expresión como $\lambda x_{1}.\ ...\ \lambda x_{n}.X$ donde X es libre de lambda.

{\begin{cases}\operatorname {lambda-anon} [\lambda F.X]=\operatorname {lambda-free} [X]\lor \operatorname {lambda-anon} [X]\\\operatorname {lambda-anon} [V]=\operatorname {false} \\\operatorname {lambda-anon} [M\ N]=\operatorname {false} \end{cases}}

Elegir funciones anónimas solo para levantar

Se busca la abstracción anónima más profunda, de modo que al aplicar la elevación, la función elevada se convierta en una ecuación simple. Esta definición no reconoce las abstracciones lambda con un parámetro como funciones. Todas las abstracciones lambda se consideran funciones anónimas.

lift-choice - El primer anónimo encontrado al recorrer la expresión o ninguno si no hay función.

$\operatorname {lambda-anon} [X]\to \operatorname {lift-choice} [X]=X$
$\operatorname {lift-choice} [\lambda F.X]=\operatorname {lift-choice} [X]$
$\operatorname {lift-choice} [M]\neq \operatorname {none} \to \operatorname {lift-choice} [M\ N]=\operatorname {lift-choice} [M]$
$\operatorname {lift-choice} [M\ N]=\operatorname {lift-choice} [N]$
$\operatorname {lift-choice} [V]=\operatorname {none}$

Por ejemplo,

Elegir funciones con nombre y anónimas para levantar

Busca la definición de función anónima o con nombre más profunda, de modo que al aplicar la elevación, la función elevada se convierta en una ecuación simple. Esta definición reconoce una abstracción lambda con un parámetro real como la definición de una función. Solo las abstracciones lambda sin aplicación se tratan como funciones anónimas.

nombre lambda

Una función con nombre. Una expresión como

(\lambda F.M)\ N

donde M es libre de lambda y N es libre de lambda o una función anónima.

{\begin{array}{l}\operatorname {lambda-named} [(\lambda F.M)\ N]=\operatorname {lambda-free} [M]\land \operatorname {lambda-anon} [N]\\\operatorname {lambda-named} [\lambda F.X]=\operatorname {false} \\\operatorname {lambda-named} [V]=\operatorname {false} \end{array}}

opción de ascensor

La primera función anónima o con nombre que se encuentre al recorrer la expresión, o ninguna si no hay ninguna función.

$\operatorname {lambda-named} [X]\lor \operatorname {lambda-anon} [X]\to \operatorname {lift-choice} [X]=X$
$\operatorname {lift-choice} [\lambda F.X]=\operatorname {lift-choice} [X]$
$\operatorname {lift-choice} [M]\neq \operatorname {none} \to \operatorname {lift-choice} [M\ N]=\operatorname {lift-choice} [M]$
$\operatorname {lift-choice} [M\ N]=\operatorname {lift-choice} [N]$
$\operatorname {lift-choice} [V]=\operatorname {none}$

Por ejemplo,

Ejemplos

Por ejemplo, el combinador Y ,

\lambda f.(\lambda x.f\ (x\ x))\ (\lambda x.f\ (x\ x))

se levanta como,

\operatorname {let} x\ f\ y=f\ (y\ y)\land q\ x\ f=f\ ((x\ f)\ (x\ f))\operatorname {in} q\ x

y después de la caída del parámetro ,

\operatorname {let} x\ f\ y=f\ (y\ y)\land q\ f=f\ ((x\ f)\ (x\ f))\operatorname {in} q

Como una expresión lambda (véase Conversión de let a expresiones lambda ),

(\lambda x.(\lambda q.q)\ \lambda f.f\ (x\ f)\ (x\ f))\ \lambda f.\lambda y.f\ (y\ y)

Si solo se levantan funciones anónimas, el combinador Y es,

\operatorname {let} p\ f\ x=f\ (x\ x)\land q\ p\ f=(p\ f)\ (p\ f)\operatorname {in} q\ p

y después de la caída del parámetro ,

\operatorname {let} p\ f\ x=f\ (x\ x)\land q\ f=(p\ f)\ (p\ f)\operatorname {in} q

Como expresión lambda,

(\lambda p.(\lambda q.q)\ \lambda f.(p\ f)\ (p\ f))\ \lambda f.\lambda x.f\ (x\ x)

La primera subexpresión que se debe elegir para el levantamiento es $\lambda x.f\ (x\ x)$ Esto transforma la expresión lambda en $\lambda f.(p\ f)\ (p\ f)$ y crea la ecuación $p\ f\ x=f(x\ x)$ .

La segunda subexpresión que se debe elegir para el levantamiento es $\lambda f.(p\ f)\ (p\ f)$ Esto transforma la expresión lambda en $q\ p$ y crea la ecuación $q\ p\ f=(p\ f)\ (p\ f)$ .

Y el resultado es,

\operatorname {let} p\ f\ x=f\ (x\ x)\land q\ p\ f=(p\ f)\ (p\ f)\operatorname {in} q\ p\

Sorprendentemente, este resultado es más sencillo que el obtenido al elevar funciones con nombre.

Ejecución

Aplicar función a $K$ ,

{\begin{cases}\lambda f.(\lambda x.f\ (x\ x))\ (\lambda x.f\ (x\ x))\ K&\ \operatorname {let} \ p\ f\ x=f\ (x\ x)\land q\ p\ f=(p\ f)\ (p\ f)\ \operatorname {in} \ q\ p\ K\\(\lambda x.K\ (x\ x))\ (\lambda x.K\ (x\ x))&\ \operatorname {let} \ p\ f\ x=f\ (x\ x)\land q\ p\ f=(p\ f)\ (p\ f)\ \operatorname {in} \ p\ K\ (p\ K)\\K\ ((\lambda x.K\ (x\ x))\ (\lambda x.K\ (x\ x)))&\ \operatorname {let} \ p\ f\ x=f\ (x\ x)\land q\ p\ f=p\ f\ (p\ f)\ \operatorname {in} \ K\ (p\ K\ (p\ K))\\\end{cases}}

Entonces,

(\lambda x.K\ (x\ x))\ (\lambda x.K\ (x\ x))=K\ ((\lambda x.K\ (x\ x))\ (\lambda x.K\ (x\ x))))\

o

p\ K\ (p\ K)=K\ (p\ K\ (p\ K))

El combinador Y llama repetidamente a su parámetro (función) sobre sí mismo. El valor está definido si la función tiene un punto fijo . Pero la función nunca terminará.

Caída de Lambda en el cálculo lambda

La técnica de lambda droping ^{[ 4 ]} consiste en reducir el alcance de las funciones y utilizar el contexto de dicho alcance reducido para disminuir el número de parámetros. Reducir el número de parámetros facilita la comprensión de las funciones.

En la sección de elevación de Lambda , se describió una metafunción para elevar y luego convertir la expresión lambda resultante en una ecuación recursiva. La metafunción Lambda Drop realiza el proceso inverso: primero convierte las ecuaciones recursivas en abstracciones lambda y luego elimina la expresión lambda resultante en el ámbito más pequeño que abarca todas las referencias a la abstracción lambda.

La eliminación de Lambda se realiza en dos pasos,

Hundimiento
Caída de parámetros

Caída de Lambda

Se aplica una función Lambda a una expresión que forma parte de un programa. Esta función se controla mediante un conjunto de expresiones de las que se excluirá la función.

\operatorname {lambda-drop-op} [L,P,X]=P[L:=\operatorname {drop-params-tran} [\operatorname {sink-test} [L,X]]]

dónde,

L es la abstracción lambda que se va a eliminar.

P es el programa

X es un conjunto de expresiones que deben excluirse del descarte.

Transformación de caída Lambda

La transformación de eliminación de lambda hunde todas las abstracciones en una expresión. El hundimiento está excluido de las expresiones en un conjunto de expresiones,

\operatorname {lambda-drop-tran} [L,X]=\operatorname {drop-params-tran} [\operatorname {sink-tran} [\operatorname {de-let} [L,X]]]

dónde,

L es la expresión que se va a transformar.

X es un conjunto de subexpresiones que se excluirán del descarte.

sink-tra hunde cada abstracción, comenzando desde la más interna,

{\begin{cases}\operatorname {sink-tran} [(\lambda N.B)\ Y,X]=\operatorname {sink-test} [(\lambda N.\operatorname {sink-tran} [B])\ \operatorname {sink-tran} [Y],X]\\\operatorname {sink-tran} [\lambda N.B,X]=\lambda N.\operatorname {sink-tran} [B,X]\\\operatorname {sink-tran} [M\ N,X]=\operatorname {sink-tran} [M,X]\ \operatorname {sink-tran} [M,X]\\\operatorname {sink-tran} [V,X]=V\end{cases}}

Hundimiento de abstracción

El proceso de "hundimiento" consiste en mover una abstracción lambda hacia adentro lo más posible, de manera que siga estando fuera de todas las referencias a la variable.

Solicitud - 4 casos.

{\begin{cases}E\not \in \operatorname {FV} [G]\land E\not \in \operatorname {FV} [H]\to \operatorname {sink} [(\lambda E.G\ H)\ Y,X]=G\ H\\E\not \in \operatorname {FV} [G]\land E\in \operatorname {FV} [H]\to \operatorname {sink} [(\lambda E.G\ H)\ Y,X]=\operatorname {sink-test} [G\ \operatorname {sink-test} [(\lambda E.H)\ Y,X]]\\E\in \operatorname {FV} [G]\land E\not \in \operatorname {FV} [H]\to \operatorname {sink} [(\lambda E.G\ H)\ Y,X]=(\operatorname {sink-test} [(\lambda E.G)\ Y,X])\ H\\E\in \operatorname {FV} [G]\land E\in \operatorname {FV} [H]\to \operatorname {sink} [(\lambda E.G\ H)\ Y,X]=(\lambda E.G\ H)\ Y\end{cases}}

Abstracción . Utilice el cambio de nombre para garantizar que todos los nombres de las variables sean distintos.

V\neq W\to \operatorname {sink} [(\lambda V.\lambda W.E)\ Y,X]=\lambda W.\operatorname {sink-test} [(\lambda V.E)\ Y,X]

Variable - 2 casos.

E\neq V\to \operatorname {sink} [(\lambda E.V)\ Y,X]=V

E=V\to \operatorname {sink} [(\lambda E.V)\ Y,X]=Y

La prueba de sumidero excluye las expresiones de ser descartadas,

L\in X\to \operatorname {sink-test} [L,X]=L

L\not \in X\to \operatorname {sink-test} [L,X]=\operatorname {sink} [L,X]

Ejemplo

Caída de parámetros

La eliminación de parámetros consiste en optimizar una función para su posición dentro de la misma. El levantamiento de lambda añade parámetros necesarios para que una función pueda salir de su contexto. En la eliminación de parámetros, este proceso se invierte y se pueden eliminar parámetros adicionales que contienen variables libres.

Eliminar un parámetro de una función consiste en suprimir un parámetro innecesario, siempre y cuando el parámetro original que se pasa sea la misma expresión. Las variables libres de la expresión también deben estar libres en el lugar donde se define la función. En este caso, el parámetro eliminado se reemplaza por la expresión en el cuerpo de la definición de la función, lo que hace que el parámetro sea innecesario.

Por ejemplo, consideremos:

\lambda m,p,q.(\lambda g.\lambda n.(n\ (g\ m\ p\ n)\ (g\ q\ p\ n)))\ \lambda x.\lambda o.\lambda y.o\ x\ y

En este ejemplo, el parámetro real para el parámetro formal o siempre es p . Como p es una variable libre en toda la expresión, el parámetro puede omitirse. El parámetro real para el parámetro formal y siempre es n . Sin embargo , n está ligado a una abstracción lambda. Por lo tanto, este parámetro no puede omitirse.

El resultado de eliminar el parámetro es,

\operatorname {drop-params-tran} [\lambda m,p,q.(\lambda g.\lambda n.n\ (g\ m\ p\ n)\ (g\ q\ p\ n))\ \lambda x.\lambda o.\lambda y.o\ x\ y

\equiv \lambda m,p,q.(\lambda g.\lambda n.n\ (g\ m\ n)\ (g\ q\ n))\ \lambda x.\lambda y.p\ x\ y

Por ejemplo principal,

\operatorname {drop-params-tran} [\lambda f.(\lambda p.(p\ f)\ (p\ f))\ (\lambda f.\lambda x.f\ (x\ x))]

\equiv \lambda f.(\lambda p.p\ p)\ (\lambda x.f\ (x\ x))

La definición de drop-params-tran es,

\operatorname {drop-params-tran} [L]\equiv (\operatorname {drop-params} [L,D,FV[L],[]])

dónde,

\operatorname {build-param-list} [L,D,V,\_]

Listas de parámetros de compilación

Para cada abstracción que define una función, se debe generar la información necesaria para tomar decisiones sobre la eliminación de nombres. Esta información describe cada parámetro: su nombre, la expresión que representa su valor y una indicación de que todas las expresiones tienen el mismo valor.

Por ejemplo, en,

\lambda m,p,q.(\lambda g.\lambda n.(n\ (g\ m\ p\ n)\ (g\ q\ p\ n)))\ \lambda x.\lambda o.\lambda y.o\ x\ y

Los parámetros de la función g son:

Cada abstracción se renombra con un nombre único, y la lista de parámetros se asocia con el nombre de la abstracción. Por ejemplo, g tiene una lista de parámetros.

D[g]=[[x,\operatorname {false} ,\_],[o,\_,p],[y,\_,n]]

build-param-lists construye todas las listas para una expresión, recorriendo la expresión. Tiene cuatro parámetros;

La expresión lambda que se está analizando.
La tabla de parámetros enumera los nombres.
Tabla de valores para los parámetros.
La lista de parámetros devueltos, que es utilizada internamente por el

Abstracción - Una expresión lambda de la forma $(\lambda N.S)\ L$ Se analiza para extraer los nombres de los parámetros de la función.

{\begin{cases}\operatorname {build-param-lists} [(\lambda N.S)\ L,D,V,R]\equiv \operatorname {build-param-lists} [S,D,V,R]\land \operatorname {build-list} [L,D,V,D[N]]\\\operatorname {build-param-lists} [\lambda N.S,D,V,R]\equiv \operatorname {build-param-lists} [S,D,V,R]\end{cases}}

Localiza el nombre y comienza a construir la lista de parámetros para ese nombre, completando los nombres formales de los parámetros. Recibe también cualquier lista de parámetros real del cuerpo de la expresión y devuélvela como la lista de parámetros real de esta expresión.

{\begin{cases}\operatorname {build-list} [\lambda P.B,D,V,[X,\_,\_]::L]\equiv \operatorname {build-list} [B,D,V,L]\\\operatorname {build-list} [B,D,V,[]]\equiv \operatorname {build-param-lists} [B,D,V,\_]\end{cases}}

Variable - Una llamada a una función.

\operatorname {build-param-lists} [N,D,V,D[N]]

Para un nombre de función o parámetro, comience a completar la lista de parámetros real mostrando la lista de parámetros para ese nombre.

Aplicación : Se procesa una aplicación (llamada a función) para extraer los detalles reales de los parámetros.

\operatorname {build-param-lists} [E\ P,D,V,R]\equiv \operatorname {build-param-lists} [E,D,V,T]\land \operatorname {build-param-lists} [P,D,V,K]

\land T=[F,S,A]::R\land (S\implies (\operatorname {equate} [A,P]\land V[F]=A))\land D[F]=K

Recupera las listas de parámetros de la expresión y del parámetro. Recupera un registro de parámetro de la lista de parámetros de la expresión y comprueba que el valor del parámetro actual coincida con este parámetro. Registra el valor del nombre del parámetro para su posterior verificación.

{\begin{cases}\operatorname {equate} [A,N]\equiv A=N\lor (\operatorname {def} [V[N]]\land A=V[N])&{\text{if }}N{\text{ is a variable.}}\\\operatorname {equate} [A,E]\equiv A=E&{\text{otherwise.}}\end{cases}}

La lógica anterior es bastante sutil en su funcionamiento. El indicador de valor idéntico nunca se establece en verdadero. Solo se establece en falso si no se pueden encontrar coincidencias entre todos los valores. El valor se obtiene utilizando S para construir un conjunto de valores booleanos permitidos para S. Si verdadero es un miembro, entonces todos los valores para este parámetro son iguales y el parámetro puede descartarse.

\operatorname {ask} [S]\equiv S\in \{X:X=S\}

De manera similar, def utiliza la teoría de conjuntos para consultar si a una variable se le ha asignado un valor;

\operatorname {def} [F]\equiv |\{X:X=F\}|

Let - Expresión Let.

\operatorname {build-param-list} [\operatorname {let} V:E\operatorname {in} L,D,V,\_]\equiv \operatorname {build-param-list} [E,D,V,\_]\land \operatorname {build-param-list} [L,D,V,\_]

Y - Para usar en "let".

\operatorname {build-param-lists} [E\land F,D,V,\_]\equiv \operatorname {build-param-lists} [E,D,V,\_]\land \operatorname {build-param-lists} [F,D,V,\_]

Ejemplos

Por ejemplo, al crear las listas de parámetros para,

\lambda m,p,q.(\lambda g.\lambda n.(n\ (g\ m\ p\ n)\ (g\ q\ p\ n)))\ \lambda x.\lambda o.\lambda y.o\ x\ y

da,

D[g]=[[x,\operatorname {false} ,\_],[o,\operatorname {true} ,p],[y,\operatorname {true} ,n]]

y el parámetro o se elimina para dar,

\lambda m,p,q.(\lambda g.\lambda n.(n\ (g\ m\ n)\ (g\ q\ n)))\ \lambda x.\lambda y.p\ x\ y

Otro ejemplo es,

\lambda f.((\lambda p.f\ (p\ p\ f))\ (\lambda q.\lambda x.x\ (q\ q\ x))

Aquí x es igual a f. La asignación de la lista de parámetros es:

D[p]=[[q,\_,p],[x,\_,f]]

y el parámetro x se elimina para dar,

\lambda f.((\lambda q.f\ (q\ q))\ (\lambda q.f\ (q\ q))

Parámetros de caída

Utilice la información obtenida mediante las listas de parámetros de compilación para eliminar los parámetros reales que ya no son necesarios. drop-params tiene los parámetros,

La expresión lambda en la que se eliminarán los parámetros.
Asignación de nombres de variables a listas de parámetros (listas de parámetros de compilación integradas).
El conjunto de variables libres en la expresión lambda.
La lista de parámetros devueltos. Un parámetro utilizado internamente en el algoritmo.

Abstracción

\operatorname {drop-params} [(\lambda N.S)\ L,D,V,R]\equiv (\lambda N.\operatorname {drop-params} [S,D,F,R])\ \operatorname {drop-formal} [D[N],L,F]

dónde,

F=FV[(\lambda N.S)\ L]

\operatorname {drop-params} [\lambda N.S,D,V,R]\equiv (\lambda N.\operatorname {drop-params} [S,D,F,R])

dónde,

F=FV[\lambda N.S]

Variable

\operatorname {drop-params} [N,D,V,D[N]]\equiv N

Para un nombre de función o parámetro, comience a completar la lista de parámetros real mostrando la lista de parámetros para ese nombre.

Aplicación : una aplicación (llamada a función) se procesa para extraer

(\operatorname {def} [F]\land \operatorname {ask} [S]\land FV[A]\subset V)\to \operatorname {drop-params} [E\ P,D,V,R]\equiv \operatorname {drop-params} [E,D,V,[F,S,A]::R]

\neg (\operatorname {def} [F]\land \operatorname {ask} [S]\land FV[A]\subset V)\to \operatorname {drop-params} [E\ P,D,V,R]\equiv \operatorname {drop-params} [E,D,V,[F,S,A]::R]\ \operatorname {drop-params} [P,D,V,\_]

Let - Expresión Let.

\operatorname {drop-params} [\operatorname {let} V:E\operatorname {in} L]\equiv \operatorname {let} V:\operatorname {drop-params} [E,D,FV[E],[]]\operatorname {in} \operatorname {drop-params} [L,D,FV[L],[]]

Y - Para usar en "let".

\operatorname {drop-params} [E\land F,D,V,\_]\equiv \operatorname {drop-params} [E,D,V,\_]\land \operatorname {drop-params} [F,D,V,\_]

Eliminar parámetros formales

drop-formal elimina parámetros formales, basándose en el contenido de las listas desplegables. Sus parámetros son:

La lista de elementos descartados,
La definición de la función (abstracción lambda).
Las variables libres de la definición de la función.

drop-formal se define como,

$(\operatorname {ask} [S]\land FV[A]\subset V)\to \operatorname {drop-formal} [[F,S,A]::Z,\lambda F.Y,V]\equiv \operatorname {drop-formal} [[F,S,A]::Z,Y[F:=A],L]$
$\neg (\operatorname {ask} [S]\land FV[A]\subset V)\to \operatorname {drop-formal} [[F,S,A]::Z,\lambda F.Y,V]\equiv \lambda F.\operatorname {drop-formal} [[F,S,A]::Z,Y,V]$
$\operatorname {drop-formal} [Z,Y,V]\equiv Y$

Lo cual se puede explicar como,

Si todos los parámetros reales tienen el mismo valor y todas las variables libres de ese valor están disponibles para la definición de la función, entonces elimine el parámetro y reemplace el parámetro anterior con su valor.
De lo contrario, no elimine el parámetro.
De lo contrario, devuelve el cuerpo de la función.

Ejemplo

Comenzando con la definición de la función del combinador Y,

\operatorname {let} p\ f\ x=f\ (x\ x)\land q\ p\ f=(p\ f)\ (p\ f)\operatorname {in} q\ p\

Lo que devuelve el combinador Y ,

\lambda f.(\lambda x.f\ (x\ x))\ (\lambda x.f\ (x\ x))

Véase también

Referencias

↑ Johnsson, Thomas (1985). "Lambda Lifting: Transforming Programs to Recursive Equations". En Jouannaud, JP (ed.). Functional Programming Languages and Computer Architecture. FPCA 1985. Lecture Notes in Computer Science. Vol. 201. Springer. CiteSeerX 10.1.1.48.4346 . doi : 10.1007/3-540-15975-4_37 . ISBN 3-540-15975-4.
↑ Morazán, Marco T.; Schultz, Ulrik P. (2008). "Optimal Lambda Lifting in Quadratic Time". Implementation and Application of Functional Languages – Revised Selected Papers . pp. 37–56 . doi : 10.1007/978-3-540-85373-2_3 . ISBN 978-3-540-85372-5.
↑ Danvy, O.; Schultz, UP (1997). "Lambda-dropping" . ACM SIGPLAN Notices . 32 (12): 90– 106. doi : 10.1145/258994.259007 .
↑ Danvy, Olivier; Schultz, Ulrik P. (octubre de 2000). "Lambda-Dropping: Transforming Recursive Equations into Programs with Block Structure" (PDF) . Theoretical Computer Science . 248 ( 1–2 ): 243–287 . CiteSeerX 10.1.1.16.3943 . doi : 10.1016/S0304-3975(00)00054-2 . BRICS-RS-99-27.

Enlaces externos

Explicación en Stack Overflow, con un ejemplo en JavaScript.
Slonneger, Ken; Kurtz, Barry. "5. Algunas discusiones sobre expresiones let" (PDF) . Fundamentos de lenguajes de programación . Universidad de Iowa.

[1] Johnsson, Thomas (1985). "Lambda Lifting: Transforming Programs to Recursive Equations". En Jouannaud, JP (ed.). Functional Programming Languages and Computer Architecture. FPCA 1985. Lecture Notes in Computer Science. Vol. 201. Springer. CiteSeerX 10.1.1.48.4346 . doi : 10.1007/3-540-15975-4_37 . ISBN 3-540-15975-4.

[Quadratic-2] Morazán, Marco T.; Schultz, Ulrik P. (2008). "Optimal Lambda Lifting in Quadratic Time". Implementation and Application of Functional Languages – Revised Selected Papers . pp. 37–56 . doi : 10.1007/978-3-540-85373-2_3 . ISBN 978-3-540-85372-5.

[3] Danvy, O.; Schultz, UP (1997). "Lambda-dropping" . ACM SIGPLAN Notices . 32 (12): 90– 106. doi : 10.1145/258994.259007 .

[4] Danvy, Olivier; Schultz, Ulrik P. (octubre de 2000). "Lambda-Dropping: Transforming Recursive Equations into Programs with Block Structure" (PDF) . Theoretical Computer Science . 248 ( 1–2 ): 243–287 . CiteSeerX 10.1.1.16.3943 . doi : 10.1016/S0304-3975(00)00054-2 . BRICS-RS-99-27.

[ 1 ]

[ 2 ]

[ 3 ]

[ 4 ]

Algoritmo

Ejemplo

Elevación de Lambda versus cierres

Expresiones de Let y cálculo lambda

Elevación de Lambda en el cálculo lambda

Elevación Lambda

Ascensor anónimo

Construyendo la llamada

Ascensor con nombre

Transformación Lambda-lift

Elegir la expresión para levantar

Elegir funciones anónimas solo para levantar

Elegir funciones con nombre y anónimas para levantar

Ejemplos

Ejecución

Caída de Lambda en el cálculo lambda

Caída de Lambda

Transformación de caída Lambda

Hundimiento de abstracción

Ejemplo

Caída de parámetros

Listas de parámetros de compilación

Ejemplos

Parámetros de caída

Eliminar parámetros formales

Ejemplo

Véase también

Referencias

Enlaces externos

Articulos relacionados