En informática, una expresión "dejar" asocia una definición de función con un ámbito restringido .
La expresión "dejar" también se puede definir en matemáticas, donde asocia una condición booleana con un alcance restringido.
La expresión "let" puede considerarse como una abstracción lambda aplicada a un valor. Dentro de las matemáticas, una expresión let también puede considerarse como una conjunción de expresiones, dentro de un cuantificador existencial que restringe el alcance de la variable.
La expresión let está presente en muchos lenguajes funcionales para permitir la definición local de expresión, para su uso en la definición de otra expresión. La expresión let está presente en algunos lenguajes funcionales en dos formas; dejar o "dejar rec". Let rec es una extensión de la expresión let simple que usa el combinador de punto fijo para implementar la recursividad .
El lenguaje LCF de Dana Scott [1] fue una etapa en la evolución del cálculo lambda hacia los lenguajes funcionales modernos. Este lenguaje introdujo la expresión let, que ha aparecido en la mayoría de los lenguajes funcionales desde entonces.
Los lenguajes Scheme , [2] ML y más recientemente Haskell [3] han heredado las expresiones let de LCF.
Los lenguajes imperativos con estado como ALGOL y Pascal esencialmente implementan una expresión let, para implementar un alcance restringido de funciones, en estructuras de bloques. [ cita requerida ]
Una estrecha relación "donde la cláusula", junto con su variante recursivo "donde rec ", ya aparecía en Pedro Landin 's La evaluación mecánica de expresiones . [4]
Una expresión "dejar" define una función o valor para usar en otra expresión. Además de ser una construcción utilizada en muchos lenguajes de programación funcional, es una construcción de lenguaje natural que se utiliza a menudo en textos matemáticos. Es una construcción sintáctica alternativa para una cláusula where.
Dejemos expresión | Dónde cláusula |
---|
Dejar
y
en
|
dónde
y
|
En ambos casos, la construcción completa es una expresión cuyo valor es 5. Al igual que if-then-else, el tipo devuelto por la expresión no es necesariamente booleano.
Una expresión let viene en 4 formas principales,
Formulario | Y | Recursivo | Definición / restricción | Descripción |
---|
Sencillo | No | No | Definición | Definición de función simple no recursiva. |
Recursivo | No | sí | Definición | Definición de función recursiva (implementada usando el combinador Y ). |
Mutuo | sí | sí | Definición | Definición de función recursiva mutua. |
Matemático | sí | sí | Restricción | Definición matemática que respalda una condición let booleana general. |
En los lenguajes funcionales, la expresión let define funciones que pueden llamarse en la expresión. El alcance del nombre de la función se limita a la estructura de la expresión let.
En matemáticas, la expresión let define una condición, que es una restricción sobre la expresión. La sintaxis también puede admitir la declaración de variables cuantificadas existencialmente locales a la expresión let.
La terminología, sintaxis y semántica varían de un idioma a otro. En Scheme , let se usa para la forma simple y let rec para la forma recursiva. En ML, let marca solo el comienzo de un bloque de declaraciones con diversión marcando el comienzo de la definición de la función. En Haskell, let puede ser recursivo mutuamente, con el compilador averiguando lo que se necesita.
Una abstracción lambda representa una función sin nombre. Esta es una fuente de inconsistencia en la definición de una abstracción lambda. Sin embargo, las abstracciones lambda se pueden componer para representar una función con un nombre. De esta forma se elimina la inconsistencia. El término lambda,
es equivalente a definir la función por en la expresion , que puede escribirse como la expresión let ;
La expresión let es comprensible como expresión de lenguaje natural. La expresión let representa la sustitución de una variable por un valor. La regla de sustitución describe las implicaciones de la igualdad como sustitución.
Dejemos que la definición en matemáticas
En matemáticas, la expresión let se describe como la conjunción de expresiones. En los lenguajes funcionales, la expresión let también se usa para limitar el alcance. En matemáticas, el alcance se describe mediante cuantificadores. La expresión let es una conjunción dentro de un cuantificador existencial.
donde E y F son de tipo booleano.
La expresión let permite aplicar la sustitución a otra expresión. Esta sustitución se puede aplicar dentro de un ámbito restringido, a una subexpresión. El uso natural de la expresión let se aplica a un ámbito restringido (llamado lambda drop ). Estas reglas definen cómo se puede restringir el alcance;
donde F no es de tipo booleano . De esta definición se puede derivar la siguiente definición estándar de una expresión let, tal como se usa en un lenguaje funcional.
Para simplificar el marcador que especifica la variable existencial, , se omitirá de la expresión cuando esté claro en el contexto.
Derivación
Para derivar este resultado, primero asuma,
luego
Usando la regla de sustitución,
así que para todos L ,
Dejar donde K es una nueva variable. luego,
Entonces,
Pero a partir de la interpretación matemática de una reducción beta,
Aquí, si y es una función de una variable x, no es lo mismo x que en z. Se puede aplicar un cambio de nombre alfa. Entonces debemos tener
entonces,
Este resultado se representa en un lenguaje funcional en forma abreviada, donde el significado es inequívoco;
Aquí, la variable x se reconoce implícitamente como parte de la ecuación que define x y como variable en el cuantificador existencial.
Sin levantar de booleano
Surge una contradicción si E se define por . En este caso,
se convierte en
y usando,
Esto es falso si G es falso. Para evitar esta contradicción, F no puede ser de tipo booleano. Para Boolean F, el enunciado correcto de la regla de eliminación usa implicación en lugar de igualdad,
Puede parecer extraño que se aplique una regla diferente para booleanos que para otros tipos. La razón de esto es que la regla,
solo se aplica cuando F es booleano. La combinación de las dos reglas crea una contradicción, por lo que cuando una regla se cumple, la otra no.
Uniendo expresiones let
Dejemos que las expresiones se puedan definir con múltiples variables,
entonces se puede derivar,
entonces,
Leyes que relacionan el cálculo lambda y las expresiones let
La reducción Eta proporciona una regla para describir abstracciones lambda. Esta regla, junto con las dos leyes derivadas anteriormente, definen la relación entre el cálculo lambda y las expresiones let.
Nombre | Ley |
---|
Equivalencia de reducción de eta | |
Equivalencia let-lambda | (dónde es un nombre de variable.) |
Deje la combinación | |
Deje la definición definida a partir del cálculo lambda
Para evitar los problemas potenciales asociados con la definición matemática , Dana Scott originalmente definió la expresión let a partir del cálculo lambda. Esto puede considerarse como la definición de abajo hacia arriba, o constructiva, de la expresión let , en contraste con la definición de arriba hacia abajo o matemática axiomática.
La expresión let simple y no recursiva se definió como azúcar sintáctica para la abstracción lambda aplicada a un término. En esa definición,
La definición de la expresión let simple se amplió para permitir la recursividad utilizando el combinador de punto fijo .
Combinador de punto fijo
El combinador de coma fija se puede representar por la expresión,
Esta representación se puede convertir en un término lambda. Una abstracción lambda no admite la referencia al nombre de la variable en la expresión aplicada, por lo que x debe pasarse como parámetro ax .
Usando la regla de reducción de eta,
da,
Una expresión let puede expresarse como una abstracción lambda usando,
da,
Esta es posiblemente la implementación más simple de un combinador de punto fijo en el cálculo lambda. Sin embargo, una reducción beta da la forma más simétrica del combinador Y de Curry.
Expresión let recursiva
La expresión let recursiva llamada "let rec" se define usando el combinador Y para expresiones let recursivas.
Expresión let recursiva mutuamente
Luego, este enfoque se generaliza para respaldar la recursividad mutua. Una expresión let recursiva se puede componer reorganizando la expresión para eliminar cualquier condición y. Esto se logra reemplazando múltiples definiciones de función con una sola definición de función, que establece una lista de variables igual a una lista de expresiones. A continuación, se utiliza una versión del combinador Y, denominado combinador de punto fijo polivariado Y * [5] para calcular el punto fijo de todas las funciones al mismo tiempo. El resultado es una implementación recursiva mutua de la expresión let .
Se puede usar una expresión let para representar un valor que es miembro de un conjunto,
Bajo la aplicación de la función, de una expresión let a otra,
Pero se aplica una regla diferente para aplicar la expresión let a sí misma.
No parece haber una regla simple para combinar valores. Lo que se requiere es una forma general de expresión que represente una variable cuyo valor es miembro de un conjunto de valores. La expresión debe basarse en la variable y el conjunto.
La aplicación de función aplicada a este formulario debe dar otra expresión en el mismo formulario. De esta forma, cualquier expresión sobre funciones de valores múltiples puede tratarse como si tuviera un valor.
No es suficiente que el formulario represente solo el conjunto de valores. Cada valor debe tener una condición que determine cuándo la expresión toma el valor. La construcción resultante es un conjunto de pares de condiciones y valores, denominado "conjunto de valores". Consulte el estrechamiento de conjuntos de valores algebraicos .
Se proporcionarán metafunciones que describen la conversión entre expresiones lambda y let . Una metafunción es una función que toma un programa como parámetro. El programa son datos para el metaprograma. El programa y el metaprograma se encuentran en diferentes metaniveles.
Las siguientes convenciones se utilizarán para distinguir el programa del metaprograma,
- Los corchetes [] se utilizarán para representar la aplicación de la función en el metaprograma.
- Se utilizarán letras mayúsculas para las variables en el metaprograma. Las letras minúsculas representan variables en el programa.
- se utilizará para iguales en el metaprograma.
Para simplificar la primera regla dada que se aplicarán las coincidencias. Las reglas también asumen que las expresiones lambda se han procesado previamente para que cada abstracción lambda tenga un nombre único.
También se utiliza el operador de sustitución. La expresionsignifica sustituir cada aparición de G en L por S y devolver la expresión. La definición utilizada se amplía para cubrir la sustitución de expresiones, a partir de la definición dada en la página de cálculo Lambda . La coincidencia de expresiones debe comparar expresiones para la equivalencia alfa (cambio de nombre de las variables).
Conversión de lambda a expresiones let
Las siguientes reglas describen cómo convertir de una expresión lambda a una expresión let , sin alterar la estructura.
La regla 6 crea una variable única V, como nombre para la función.
Ejemplo
Por ejemplo, el combinador Y ,
se convierte en,
Regla | Expresión lambda |
---|
6 | |
---|
| | |
|
4 | |
---|
| | | | | |
---|
|
5 | |
---|
| | | | |
|
3 | |
---|
| | | | |
|
8 | |
---|
| | | | |
|
8 | |
---|
| | | |
|
4 | |
---|
| | | | |
|
2 | |
---|
| | | | |
|
1 | |
---|
| |
|
| |
Conversión de expresiones let a lambda
Estas reglas invierten la conversión descrita anteriormente. Convierten de una expresión let a una expresión lambda, sin alterar la estructura. No todas las expresiones let se pueden convertir utilizando estas reglas. Las reglas asumen que las expresiones ya están organizadas como si hubieran sido generadas por de-lambda .
No existe un equivalente estructural exacto en el cálculo lambda para las expresiones let que tienen variables libres que se utilizan de forma recursiva. En este caso, se requiere alguna adición de parámetros. Las reglas 8 y 10 agregan estos parámetros.
Las reglas 8 y 10 son suficientes para dos ecuaciones recursivas entre sí en la expresión let . Sin embargo, no funcionarán para tres o más ecuaciones recursivas entre sí. El caso general necesita un nivel adicional de bucle que hace que la meta función sea un poco más difícil. Las reglas que siguen reemplazan las reglas 8 y 10 en la implementación del caso general. Las reglas 8 y 10 se han dejado para que se pueda estudiar primero el caso más simple.
- forma lambda : convierte la expresión en una conjunción de expresiones, cada una de las cuales tiene la forma variable = expresión .
- ...... donde V es una variable.
- lift-vars : obtiene el conjunto de variables que necesitan X como parámetro, porque la expresión tiene X como variable libre.
- sub-vars : para cada variable del conjunto, sustitúyala por la variable aplicada a X en la expresión. Esto hace que X sea una variable pasada como parámetro, en lugar de ser una variable libre en el lado derecho de la ecuación.
- de-let - Eleve cada condición en E para que X no sea una variable libre en el lado derecho de la ecuación.
Ejemplos de
Por ejemplo, la expresión let obtenida del combinador Y ,
se convierte en,
Regla | Expresión lambda |
---|
6 | |
---|
| | |
|
1 | |
---|
| | |
|
2 | |
---|
| | |
|
3 | |
---|
| | |
|
7 | |
---|
| | | |
|
4 | |
---|
| | | | |
|
4 | |
---|
| | | | |
|
5 | |
---|
| |
|
1 | |
---|
| | | | |
|
2 | |
---|
| | | | |
|
3 | |
---|
| | | | |
|
4 | |
---|
| | | | | | | |
|
5 | |
---|
| | |
|
| |
Para un segundo ejemplo, tome la versión mejorada del combinador Y ,
se convierte en,
Regla | Expresión lambda |
---|
8 | |
7 | |
1, 2 | |
7, 4, 5 | |
1, 2 | |
| |
Para un tercer ejemplo, la traducción de,
es,
Regla | Expresión lambda |
---|
9 | |
1 | |
2 | |
| |
7 | |
1 | |
2 | |
| |