Sea expresión

En informática, una expresión "let" asocia una definición de función con un alcance restringido .

La expresión "let" también puede definirse 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. En 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 una 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: let o "let rec". Let rec es una extensión de la expresión let simple que utiliza el combinador de punto fijo para implementar la recursión .

Historia

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 expresiones let de LCF.

Los lenguajes imperativos con estado como ALGOL y Pascal implementan esencialmente una expresión let para implementar un alcance restringido de funciones en estructuras de bloques. ^{[ cita requerida ]}

Una cláusula " where " estrechamente relacionada , junto con su variante recursiva " where rec ", apareció ya en The mechanical evaluation of expressions de Peter Landin . ^[4]

Descripción

Una expresión "let" define una función o un valor para su uso en otra expresión. Además de ser una construcción utilizada en muchos lenguajes de programación funcional, es una construcción del lenguaje natural que se utiliza a menudo en textos matemáticos. Es una construcción sintáctica alternativa para una cláusula where.

En ambos casos, toda la construcción es una expresión cuyo valor es 5. Al igual que en if-then-else, el tipo devuelto por la expresión no es necesariamente booleano.

Una expresión let viene en 4 formas principales,

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 está limitado a la estructura de la expresión let.

En matemáticas, la expresión let define una condición, que es una restricción de 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, la sintaxis y la semántica varían de un lenguaje a otro. En Scheme , let se utiliza para la forma simple y let rec para la forma recursiva. En ML , let marca solo el comienzo de un bloque de declaraciones, mientras que fun marca el comienzo de la definición de la función. En Haskell, let puede ser recursivo entre sí, y el compilador determina qué se necesita.

Definición

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 pueden estar compuestas para representar una función con un nombre. De esta forma se elimina la inconsistencia. El término lambda,

${\displaystyle (\lambda f.z)\ (\lambda x.y)}$

es equivalente a definir la función por en la expresión , que puede escribirse como la expresión let ; ${\displaystyle f}$ ${\displaystyle f\ x=y}$ ${\displaystyle z}$

${\displaystyle \operatorname {let} f\ x=y\operatorname {in} z}$

La expresión let se puede entender como una 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.

Definición de Let en matemáticas

En matemáticas, la expresión let se describe como la conjunción de expresiones. En lenguajes funcionales, la expresión let también se utiliza 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.

${\displaystyle (\exists xE\land F)\iff \operatorname {let} x:E\operatorname {in} F}$

donde E y F son de tipo booleano.

La expresión let permite que la sustitución se aplique 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 es en la aplicación a un ámbito restringido (llamado lambda dropping ). Estas reglas definen cómo se puede restringir el ámbito;

${\displaystyle {\begin{cases}x\not \in \operatorname {FV} (E)\land x\in \operatorname {FV} (F)\implies \operatorname {let} x:G\operatorname {in} E\ F=E\ (\operatorname {let} x:G\operatorname {in} F)\\x\in \operatorname {FV} (E)\land x\not \in \operatorname {FV} (F)\implies \operatorname {let} x:G\operatorname {in} E\ F=(\operatorname {let} x:G\operatorname {in} E)\ F\\x\not \in \operatorname {FV} (E)\land x\not \in \operatorname {FV} (F)\implies \operatorname {let} x:G\operatorname {in} E\ F=E\ F\end{cases}}}$

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 utiliza en un lenguaje funcional.

${\displaystyle x\not \in \operatorname {FV} (y)\implies (\operatorname {let} x:x=y\operatorname {in} z)=z[x:=y]=(\lambda x.z)\ y}$

Para simplificar, el marcador que especifica la variable existencial, , se omitirá de la expresión cuando resulte claro a partir del contexto. ${\displaystyle x:}$

${\displaystyle x\not \in \operatorname {FV} (y)\implies (\operatorname {let} x=y\operatorname {in} z)=z[x:=y]=(\lambda x.z)\ y}$

Derivación

Para obtener este resultado, supongamos primero que:

${\displaystyle x\not \in \operatorname {FV} (L)}$

entonces

${\displaystyle {\begin{aligned}L\ (\operatorname {let} x:x=y\operatorname {in} z)&\iff (\operatorname {let} x:x=y\operatorname {in} L\ z)\\&\iff x=y\land L\ z\end{aligned}}}$

Utilizando la regla de sustitución,

${\displaystyle {\begin{aligned}&\iff x=y\land (L\ z)[x:=y]\\&\iff x=y\land (L[x:=y]\ z[x:=y])\\&\iff x=y\land L\ z[x:=y]\\&\implies L\ z[x:=y]\end{aligned}}}$

Entonces, para todos los L ,

${\displaystyle L\operatorname {let} x:x=y\operatorname {in} z\implies L\ z[x:=y]}$

Sea donde K es una nueva variable. entonces, ${\displaystyle L\ X=(X=K)}$

${\displaystyle (\operatorname {let} x:x=y\operatorname {in} z)=K\implies z[x:=y]=K}$

Entonces,

${\displaystyle \operatorname {let} x:x=y\operatorname {in} z=z[x:=y]}$

Pero a partir de la interpretación matemática de una reducción beta,

${\displaystyle (\lambda x.z)\ y=z[x:=y]}$

Aquí, si y es una función de una variable x, no es la misma x que en z. Se puede aplicar un cambio de nombre alfabético. Por lo tanto, debemos tener:

${\displaystyle x\not \in \operatorname {FV} (y)}$

entonces,

${\displaystyle x\not \in \operatorname {FV} (y)\implies \operatorname {let} x:x=y\operatorname {in} z=(\lambda x.z)\ y}$

Este resultado se representa en un lenguaje funcional de forma abreviada, donde el significado es inequívoco;

${\displaystyle x\not \in \operatorname {FV} (y)\implies (\operatorname {let} x=y\operatorname {in} z)=z[x:=y]=(\lambda x.z)\ y}$

Aquí la variable x se reconoce implícitamente como parte de la ecuación que define x y como variable en el cuantificador existencial.

No se puede levantar nada de Boolean

Surge una contradicción si E se define por . En este caso, ${\displaystyle E=\neg }$

${\displaystyle x\not \in \operatorname {FV} (E)\land x\in \operatorname {FV} (F)\implies \operatorname {let} x:G\operatorname {in} E\ F=E\ (\operatorname {let} x:G\operatorname {in} F)}$

se convierte,

${\displaystyle \operatorname {let} x:G\operatorname {in} \neg F=\neg \ (\operatorname {let} x:G\operatorname {in} F)}$

y usando,

${\displaystyle (\exists xE\land F)\iff \operatorname {let} x:E\operatorname {in} F}$

${\displaystyle (\exists xG\land \neg F)=\neg \ (\exists xG\land F)}$

${\displaystyle =(\exists x\neg G\lor \neg F)}$

Esto es falso si G es falso. Para evitar esta contradicción, no se permite que F sea de tipo booleano. Para el tipo booleano F, la declaración correcta de la regla de eliminación utiliza implicación en lugar de igualdad.

${\displaystyle x\not \in \operatorname {FV} (E)\land x\in \operatorname {FV} (F)\implies (\operatorname {let} x:G\operatorname {in} E\ F\to E\ (\operatorname {let} x:G\operatorname {in} F))}$

Puede parecer extraño que se aplique una regla diferente para los booleanos que para otros tipos. La razón de esto es que la regla,

${\displaystyle (\exists xE\land F)\iff \operatorname {let} x:E\operatorname {in} F}$

Sólo se aplica cuando F es booleana. La combinación de las dos reglas crea una contradicción, por lo que cuando una regla se cumple, la otra no.

Unir expresiones let

Las expresiones Let se pueden definir con múltiples variables,

${\displaystyle (\exists v\cdots \exists w\exists xE\land F)\iff \operatorname {let} v,\ldots ,w,x:E\operatorname {in} F}$

Entonces se puede derivar,

${\displaystyle x\not \in FV(E)\implies (\exists v\cdots \exists w\exists xE\land F)\iff (\exists v\cdots \exists w(E\land \exists xF))}$

entonces,

${\displaystyle x\not \in FV(E)\implies (\operatorname {let} v,\ldots ,w,x:E\land F\operatorname {in} L\equiv \operatorname {let} v,\ldots ,w:E\operatorname {in} \operatorname {let} x:F\operatorname {in} L)}$

Leyes que relacionan el cálculo lambda con las expresiones let

La reducción de Eta proporciona una regla para describir las abstracciones lambda. Esta regla, junto con las dos leyes derivadas anteriormente, define la relación entre el cálculo lambda y las expresiones let.

Sea la definición definida a partir del cálculo lambda

Para evitar los posibles problemas asociados con la definición matemática, Dana Scott definió originalmente la expresión let a partir del cálculo lambda. Esta puede considerarse como la definición de abajo hacia arriba o constructiva de la expresión let , en contraste con la definición matemática de arriba hacia abajo o axiomática.

La expresión let , simple y no recursiva , se definió como un azúcar sintáctico para la abstracción lambda aplicada a un término. En esa definición,

${\displaystyle (\operatorname {let} _{s}x=y\operatorname {in} z)\equiv (\lambda x.z)\ y}$

La definición de expresión let simple se amplió luego para permitir la recursión utilizando el combinador de punto fijo .

Combinador de punto fijo

El combinador de punto fijo puede representarse mediante la expresión,

${\displaystyle \lambda f.\operatorname {let} x=f\ x\operatorname {in} x}$

Esta representación se puede convertir en un término lambda. Una abstracción lambda no admite referencias al nombre de la variable en la expresión aplicada, por lo que x debe pasarse como parámetro a x .

${\displaystyle \lambda f.\operatorname {let} x\ x=f\ (x\ x)\operatorname {in} x\ x}$

Utilizando la regla de reducción de eta,

${\displaystyle f\ x=y\equiv f=\lambda x.y}$

da,

${\displaystyle \lambda f.\operatorname {let} x=\lambda x.f\ (x\ x)\operatorname {in} x\ x}$

Una expresión let puede expresarse como una abstracción lambda usando,

${\displaystyle n\not \in FV(E)\to (\operatorname {let} n=E\operatorname {in} L\equiv (\lambda n.L)\ E)}$

da,

${\displaystyle \lambda f.(\lambda x.x\ x)\ (\lambda x.f\ (x\ x))}$

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 proporciona la forma más simétrica del combinador Y de Curry.

${\displaystyle \lambda f.(\lambda x.f\ (x\ x))\ (\lambda x.f\ (x\ x))}$

Expresión let recursiva

La expresión let recursiva denominada "let rec" se define utilizando el combinador Y para expresiones let recursivas.

${\displaystyle (\operatorname {let\ rec} x=y\operatorname {in} z)\equiv (\lambda x.z)\ (Y\ (\lambda x.y))}$

Expresión let recursiva mutua

Este enfoque se generaliza luego para admitir la recursión mutua. Se puede componer una expresión let mutuamente recursiva reorganizando la expresión para eliminar cualquier condición y . Esto se logra reemplazando múltiples definiciones de función con una única definición de función, que establece una lista de variables igual a una lista de expresiones. Luego se utiliza una versión del combinador Y, llamado el combinador de punto fijo polivariádico Y* ^[5] para calcular el punto fijo de todas las funciones al mismo tiempo. El resultado es una implementación mutuamente recursiva de la expresión let .

Valores múltiples

Una expresión let se puede utilizar para representar un valor que es miembro de un conjunto,

${\displaystyle \operatorname {let} x\in X\operatorname {in} x}$

En la aplicación de una función, de una expresión let a otra,

${\displaystyle {\begin{aligned}&(\operatorname {let} x\in X\operatorname {in} x)\ (\operatorname {let} y\in Y\operatorname {in} y)\\&=\operatorname {let} x\in X\land y\in Y\operatorname {in} x\ y\\&=\operatorname {let} (x,y)\in X\times Y\operatorname {in} x\ y\end{aligned}}}$

Pero se aplica una regla diferente para aplicar la expresión let a sí misma.

${\displaystyle {\begin{aligned}&(\operatorname {let} x\in X\operatorname {in} x)\ (\operatorname {let} x\in X\operatorname {in} x)\\&=\operatorname {let} x\in X\operatorname {in} x\ x\end{aligned}}}$

No parece existir una regla sencilla para combinar valores. Lo que se necesita es una forma general de expresión que represente una variable cuyo valor sea miembro de un conjunto de valores. La expresión debe basarse en la variable y el conjunto.

La aplicación de una función a esta forma debe dar como resultado otra expresión en la misma forma. De esta manera, cualquier expresión sobre funciones de múltiples valores puede tratarse como si tuviera un solo valor.

No basta con que la forma represente únicamente 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, llamado "conjunto de valores". Véase la limitación de los conjuntos de valores algebraicos .

Reglas para la conversión entre el cálculo lambda y las expresiones let

Se dará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 es información 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,

• Se utilizarán corchetes [] para representar la aplicación de la función en el metaprograma.
• Se utilizarán letras mayúsculas para las variables del metaprograma. Las letras minúsculas representan las variables del programa.
• ${\displaystyle \equiv }$se utilizará para iguales en el metaprograma.

Para simplificar, se aplicará la primera regla que establece que se aplicarán las coincidencias. Las reglas también suponen que las expresiones lambda se han procesado previamente de modo que cada abstracción lambda tenga un nombre único.

También se utiliza el operador de sustitución. La expresión significa sustituir cada ocurrencia de G en L por S y devolver la expresión. La definición utilizada se extiende para cubrir la sustitución de expresiones, a partir de la definición proporcionada en la página de cálculo Lambda . La comparación de expresiones debe comparar expresiones para determinar la equivalencia alfa (cambio de nombre de las variables). ${\displaystyle L[G:=S]}$

Conversión de expresiones lambda a let

Las siguientes reglas describen cómo convertir una expresión lambda a una expresión let , sin alterar la estructura.

1. ${\displaystyle \operatorname {de-lambda} [V]\equiv V}$
2. ${\displaystyle \operatorname {de-lambda} [M\ N]\equiv \operatorname {de-lambda} [M]\ \operatorname {de-lambda} [N]}$
3. ${\displaystyle \operatorname {de-lambda} [F=\lambda P.E]\equiv \operatorname {de-lambda} [F\ P=E]}$
4. ${\displaystyle \operatorname {de-lambda} [E=F]\equiv \operatorname {de-lambda} [E]=\operatorname {de-lambda} [F]}$
5. ${\displaystyle \operatorname {de-lambda} [(\lambda F.E)L]\equiv \operatorname {let-combine} [\operatorname {let} F:\operatorname {de-lambda} [F=L]\operatorname {in} E]}$
6. ${\displaystyle V\not \in \operatorname {FV} [\lambda F.E]\to \operatorname {de-lambda} [\lambda F.E]\equiv \operatorname {let-combine} [\operatorname {let} V:\operatorname {de-lambda} [V\ F=E]\operatorname {in} V]}$
7. ${\displaystyle V\neq W\to \operatorname {let-combine} [\operatorname {let} V:E\operatorname {in} \operatorname {let} W:F\operatorname {in} G]\equiv \operatorname {let} V,W:E\land F\operatorname {in} G}$
8. ${\displaystyle \operatorname {let-combine} [\operatorname {let} V:E\operatorname {in} F]\equiv \operatorname {let} V:E\operatorname {in} F}$

La regla 6 crea una variable única V, como nombre para la función.

Ejemplo

Por ejemplo, el combinador Y ,

${\displaystyle \lambda f.(\lambda x.f\ (x\ x))\ (\lambda x.f\ (x\ x))}$

se convierte en,

${\displaystyle \operatorname {let} p:p\ f=\operatorname {let} x:x\ q=f\ (q\ q)\operatorname {in} f\ (x\ x)\operatorname {in} p}$

Conversión de expresiones let a lambda

Estas reglas invierten la conversión descrita anteriormente. Convierten una expresión let en una expresión lambda sin alterar la estructura. No todas las expresiones let pueden convertirse utilizando estas reglas. Las reglas suponen que las expresiones ya están organizadas como si hubieran sido generadas por de-lambda .

1. ${\displaystyle \operatorname {get-lambda} [F,G\ V=E]=\operatorname {get-lambda} [F,G=\lambda V.E]}$
2. ${\displaystyle \operatorname {get-lambda} [F,F=E]=\operatorname {de-let} [E]}$
3. ${\displaystyle \operatorname {de-let} [\lambda V.E]\equiv \lambda V.\operatorname {de-let} [E]}$
4. ${\displaystyle \operatorname {de-let} [M\ N]\equiv \operatorname {de-let} [M]\ \operatorname {de-let} [N]}$
5. ${\displaystyle \operatorname {de-let} [V]\equiv V}$
6. ${\displaystyle V\not \in FV[\operatorname {get-lambda} [V,E]]\to \operatorname {de-let} [\operatorname {let} V:E\ \operatorname {in} V]\equiv \operatorname {get-lambda} [V,E]}$
7. ${\displaystyle V\not \in FV[\operatorname {get-lambda} [V,E]]\to \operatorname {de-let} [\operatorname {let} V:E\ \operatorname {in} L]\equiv (\lambda V.\operatorname {de-let} [L])\ \operatorname {get-lambda} [V,E]}$
8. ${\displaystyle W\not \in \operatorname {FV} [\operatorname {get-lambda} [V,E]]\to \operatorname {de-let} [\operatorname {let} V,W:E\land F\ \operatorname {in} G]\equiv \operatorname {de-let} [\operatorname {let} V:E\ \operatorname {in} \operatorname {let} W:F\ \operatorname {in} G]}$
9. ${\displaystyle V\in \operatorname {FV} [\operatorname {get-lambda} [V,E]]\to \operatorname {de-let} [\operatorname {let} V:E\ \operatorname {in} L]\equiv \operatorname {de-let} [\operatorname {let} V:V\ V=\operatorname {get-lambda} [V,E][V:=V\ V]\ \operatorname {in} L[V:=V\ V]]}$
10. ${\displaystyle W\in \operatorname {FV} [\operatorname {get-lambda} [V,E]]\to \operatorname {de-let} [\operatorname {let} V,W:E\land F\ \operatorname {in} L]\equiv \operatorname {de-let} [\operatorname {let} V:V\ W=\operatorname {get-lambda} [V,E][V:=V\ W]\ \operatorname {in} \operatorname {let} W:F[V:=V\ W]\ \operatorname {in} L[V:=V\ W]]}$

No existe un equivalente estructural exacto en el cálculo lambda para las expresiones let que tienen variables libres que se usan de forma recursiva. En este caso, se requiere la adición de algunos 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 repetición que hace que la función meta 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.

1. forma lambda - Convierte la expresión en una conjunción de expresiones, cada una de la forma variable = expresión .
   1. ${\displaystyle \operatorname {lambda-form} [G\ V=E]=\operatorname {lambda-form} [G=\lambda V.E]}$
   2. ${\displaystyle \operatorname {lambda-form} [E\land F]=\operatorname {lambda-form} [E]\land \operatorname {lambda-form} [F]}$
   3. ${\displaystyle \operatorname {lambda-form} [V=E]=V=E}$......donde V es una variable.
2. lift-vars : obtiene el conjunto de variables que necesitan X como parámetro, porque la expresión tiene X como variable libre.
   1. ${\displaystyle X\in \operatorname {FV} [E]\to \operatorname {lift-vars} [X,V=E]=\{V\}}$
   2. ${\displaystyle X\not \in \operatorname {FV} [E]\to \operatorname {lift-vars} [X,V=E]=\{\}}$
   3. ${\displaystyle \operatorname {lift-vars} [X,E\land F]=\operatorname {lift-vars} [X,E]\cup \operatorname {lift-vars} [X.F]}$
3. sub-variables : para cada variable del conjunto, sustitúyala por la variable aplicada a X en la expresión. Esto hace que X sea una variable que se pasa como parámetro, en lugar de ser una variable libre en el lado derecho de la ecuación.
   1. ${\displaystyle \operatorname {sub-vars} [E,\{V\}\cup S,X]=\operatorname {sub-vars} [E[V:=V\ X],S,X]}$
   2. ${\displaystyle \operatorname {sub-vars} [E,\{\},X]=E}$
4. de-let - Levanta cada condición en E para que X no sea una variable libre en el lado derecho de la ecuación.
   1. ${\displaystyle {\begin{aligned}L&=\operatorname {lambda-form} [E]\land S=\operatorname {lift-vars} [X,L]\to \operatorname {de-let} [\operatorname {let} V\ldots W,X:E\land F\ \operatorname {in} G]\\&\equiv \operatorname {de-let} [\operatorname {let} V\ldots W:\operatorname {sub-vars} [L,S,X]\ \operatorname {in} \operatorname {let} \operatorname {sub-vars} [\operatorname {lambda-form} [F],S,X]\ \operatorname {in} \operatorname {sub-vars} [G,S,X]]\end{aligned}}}$

Ejemplos

Por ejemplo, la expresión let obtenida del combinador Y ,

${\displaystyle \operatorname {let} p:p\ f=\operatorname {let} x:x\ q=f\ (q\ q)\ \operatorname {in} f\ (x\ x)\ \operatorname {in} p}$

se convierte en,

${\displaystyle \lambda f.(\lambda x.f\ (x\ x))\ (\lambda q.f\ (q\ q))}$

Para un segundo ejemplo, tomemos la versión elevada del combinador Y ,

${\displaystyle \operatorname {let} p,q:p\ f\ x=f\ (x\ x)\land q\ p\ f=(p\ f)\ (p\ f)\ \operatorname {in} q\ p}$

se convierte en,

${\displaystyle (\lambda p.(\lambda q.q\ p)\ \lambda p.\lambda f.(p\ f)\ (p\ f))\ \lambda f.\lambda x.f\ (x\ x)}$

Para un tercer ejemplo la traducción de,

${\displaystyle \operatorname {let} x:x\ f=f\ (x\ f)\ \operatorname {in} x}$

es,

${\displaystyle (\lambda x.x\ x)\ (\lambda x.\lambda f.f\ (x\ x\ f))}$

Para un cuarto ejemplo la traducción de,

${\displaystyle \operatorname {let} x:x=f\ x\ \operatorname {in} x}$

es,

${\displaystyle (\lambda x.x\ x)\ (\lambda x.f\ (x\ x))}$

que es el famoso combinador y .

Personas clave

• Dana Scott

Véase también

• Alcance (informática)
• Elevación de lambda
• Combinador de punto fijo
• Cálculo lambda
• La paradoja de Curry
• Cálculo lambda deductivo
• Programación lógica de restricciones
• Estrechamiento de conjuntos de valores algebraicos

Referencias

1. "PCF es un lenguaje de programación para funciones computables, basado en LCF, la lógica de funciones computables de Scott" (Plotkin 1977). Programación de funciones computables es utilizado por (Mitchell 1996). También se lo conoce como Programación con funciones computables o Lenguaje de programación para funciones computables .
2. "Esquema - Variables y expresiones Let".
3. Simon, Marlow (2010). "Informe sobre el lenguaje Haskell 2010: expresiones Let".
4. Landin, Peter J. (1964). "La evaluación mecánica de expresiones". The Computer Journal . 6 (4). British Computer Society : 308–320. doi : 10.1093/comjnl/6.4.308 .
5. "Combinadores de punto fijo polivariádicos más simples para recursión mutua".

Obras citadas

• Mitchell, John C. (1996). Fundamentos de lenguajes de programación. MIT Press. ISBN 978-0-262-13321-0.
• Plotkin, GD (diciembre de 1977). "LCF considerado como lenguaje de programación". Theoretical Computer Science . 5 (3): 223–255. doi : 10.1016/0304-3975(77)90044-5 .