Definición de cálculo lambda

Formalismo matemático

El cálculo lambda es un sistema matemático formal basado en la abstracción lambda y la aplicación de funciones . Aquí se dan dos definiciones del lenguaje: una definición estándar y una definición que utiliza fórmulas matemáticas.

Definición estándar

Esta definición formal fue dada por Alonzo Church .

Definición

Las expresiones lambda se componen de

• variables , , ..., , ... ${\displaystyle v_{1}}$ ${\displaystyle v_{2}}$ ${\displaystyle v_{n}}$
• los símbolos de abstracción lambda ' ' y punto '. ${\displaystyle \lambda }$
• paréntesis ( )

El conjunto de expresiones lambda, , se puede definir inductivamente : ${\displaystyle \Lambda }$

1. Si es una variable, entonces ${\displaystyle x}$ ${\displaystyle x\in \Lambda }$
2. Si es una variable y , entonces ${\displaystyle x}$ ${\displaystyle M\in \Lambda }$ ${\displaystyle (\lambda x.M)\in \Lambda }$
3. Si , entonces ${\displaystyle M,N\in \Lambda }$ ${\displaystyle (M\ N)\in \Lambda }$

Las instancias de la regla 2 se conocen como abstracciones y las instancias de la regla 3 se conocen como aplicaciones. ^[1]

Notación

Para mantener despejada la notación de expresiones lambda, normalmente se aplican las siguientes convenciones.

• Los paréntesis más externos se eliminan: en lugar de ${\displaystyle M\ N}$ ${\displaystyle (M\ N)}$
• Se supone que las aplicaciones son asociativas por la izquierda: se puede escribir en lugar de ^[2] ${\displaystyle M\ N\ P}$ ${\displaystyle ((M\ N)\ P)}$
• El cuerpo de una abstracción se extiende lo más a la derecha posible : significa y no ${\displaystyle \lambda x.M\ N}$ ${\displaystyle \lambda x.(M\ N)}$ ${\displaystyle (\lambda x.M)\ N}$
• Una secuencia de abstracciones se contrae: se abrevia como ^{[3] [4]} ${\displaystyle \lambda x.\lambda y.\lambda z.N}$ ${\displaystyle \lambda xyz.N}$

Variables libres y variables ligadas

Se dice que el operador de abstracción, , vincula su variable dondequiera que aparezca en el cuerpo de la abstracción. Las variables que caen dentro del alcance de una abstracción se dice que están vinculadas . Todas las demás variables se denominan libres . Por ejemplo, en la siguiente expresión es una variable vinculada y es libre: . Observe también que una variable está vinculada por su abstracción "más cercana". En el siguiente ejemplo, la única aparición de en la expresión está vinculada por la segunda lambda: ${\displaystyle \lambda }$ ${\displaystyle y}$ ${\displaystyle x}$ ${\displaystyle \lambda y.x\ x\ y}$ ${\displaystyle x}$ ${\displaystyle \lambda x.y(\lambda x.z\ x)}$

El conjunto de variables libres de una expresión lambda, , se denota como y se define por recursión sobre la estructura de los términos, de la siguiente manera: ${\displaystyle M}$ ${\displaystyle \operatorname {FV} (M)}$

1. ${\displaystyle \operatorname {FV} (x)=\{x\}}$, donde es una variable ${\displaystyle x}$
2. ${\displaystyle \operatorname {FV} (\lambda x.M)=\operatorname {FV} (M)\backslash \{x\}}$
3. ${\displaystyle \operatorname {FV} (M\ N)=\operatorname {FV} (M)\cup \operatorname {FV} (N)}$^[5]

Se dice que una expresión que no contiene variables libres es cerrada . Las expresiones lambda cerradas también se conocen como combinadores y son equivalentes a los términos de la lógica combinatoria .

Reducción

El significado de las expresiones lambda se define por cómo se pueden reducir las expresiones. ^[6]

Hay tres tipos de reducción:

• α-conversión : cambio de variables límite ( alfa );
• β-reducción : aplicación de funciones a sus argumentos ( beta );
• η-reducción : que captura una noción de extensionalidad ( eta ).

También hablamos de equivalencias resultantes: dos expresiones son β-equivalentes , si pueden ser β-convertidas en la misma expresión, y las α/η-equivalencias se definen de manera similar.

El término redex , abreviatura de expresión reducible , se refiere a subtérminos que pueden reducirse mediante una de las reglas de reducción. Por ejemplo, es un β-redex en que expresa la sustitución de por en ; si no es libre en , es un η-redex. La expresión a la que se reduce un redex se llama su reduct; utilizando el ejemplo anterior, los reducts de estas expresiones son respectivamente y . ${\displaystyle (\lambda x.M)\ N}$ ${\displaystyle N}$ ${\displaystyle x}$ ${\displaystyle M}$ ${\displaystyle x}$ ${\displaystyle M}$ ${\displaystyle \lambda x.M\ x}$ ${\displaystyle M[x:=N]}$ ${\displaystyle M}$

conversión α

La conversión alfa, a veces conocida como cambio de nombre alfa, ^[7] permite cambiar los nombres de las variables ligadas. Por ejemplo, la conversión alfa de podría dar como resultado . Los términos que difieren solo por la conversión alfa se denominan α-equivalentes . Con frecuencia, en los usos del cálculo lambda, los términos α-equivalentes se consideran equivalentes. ${\displaystyle \lambda x.x}$ ${\displaystyle \lambda y.y}$

Las reglas precisas para la conversión alfa no son completamente triviales. En primer lugar, cuando se realiza una conversión alfa de una abstracción, las únicas ocurrencias de variables que se renombran son aquellas que están vinculadas a la misma abstracción. Por ejemplo, una conversión alfa de podría dar como resultado , pero no podría dar como resultado . Este último tiene un significado diferente del original. ${\displaystyle \lambda x.\lambda x.x}$ ${\displaystyle \lambda y.\lambda x.x}$ ${\displaystyle \lambda y.\lambda x.y}$

En segundo lugar, la conversión alfa no es posible si da como resultado que una variable sea capturada por una abstracción diferente. Por ejemplo, si reemplazamos con in , obtenemos , que no es lo mismo en absoluto. ${\displaystyle x}$ ${\displaystyle y}$ ${\displaystyle \lambda x.\lambda y.x}$ ${\displaystyle \lambda y.\lambda y.y}$

En lenguajes de programación con alcance estático, se puede utilizar la conversión alfa para simplificar la resolución de nombres al garantizar que ningún nombre de variable enmascare un nombre en un alcance que lo contenga (ver cambio de nombre alfa para que la resolución de nombres sea trivial ).

Sustitución

La sustitución, escrita como , es el proceso de reemplazar todas las ocurrencias libres de la variable en la expresión con la expresión . La sustitución en términos del cálculo lambda se define por recursión en la estructura de términos, de la siguiente manera (nota: x e y son solo variables mientras que M y N son cualquier expresión λ). ${\displaystyle E[V:=R]}$ ${\displaystyle V}$ ${\displaystyle E}$ ${\displaystyle R}$

${\displaystyle {\begin{aligned}x[x:=N]&\equiv N\\y[x:=N]&\equiv y{\text{, if }}x\neq y\end{aligned}}}$

${\displaystyle {\begin{aligned}(M_{1}\ M_{2})[x:=N]&\equiv (M_{1}[x:=N])\ (M_{2}[x:=N])\\(\lambda x.M)[x:=N]&\equiv \lambda x.M\\(\lambda y.M)[x:=N]&\equiv \lambda y.(M[x:=N]){\text{, if }}x\neq y{\text{, provided }}y\notin FV(N)\end{aligned}}}$

Para sustituir en una abstracción lambda, a veces es necesario realizar una conversión α de la expresión. Por ejemplo, no es correcto que tenga como resultado , porque se suponía que el sustituido era libre pero terminó siendo ligado. La sustitución correcta en este caso es , hasta la equivalencia α. Observe que la sustitución se define de forma única hasta la equivalencia α. ${\displaystyle (\lambda x.y)[y:=x]}$ ${\displaystyle (\lambda x.x)}$ ${\displaystyle x}$ ${\displaystyle (\lambda z.x)}$

β-reducción

La β-reducción captura la idea de aplicación de funciones. La β-reducción se define en términos de sustitución: la β-reducción de es . ${\displaystyle ((\lambda V.E)\ E')}$ ${\displaystyle E[V:=E']}$

Por ejemplo, asumiendo alguna codificación de , tenemos la siguiente β-reducción: . ${\displaystyle 2,7,\times }$ ${\displaystyle ((\lambda n.\ n\times 2)\ 7)\rightarrow 7\times 2}$

η-reducción

La η-reducción expresa la idea de extensionalidad , que en este contexto es que dos funciones son iguales si y solo si dan el mismo resultado para todos los argumentos. La η-reducción convierte entre y siempre que no aparezca libre en . ${\displaystyle \lambda x.(fx)}$ ${\displaystyle f}$ ${\displaystyle x}$ ${\displaystyle f}$

Normalización

El propósito de la β-reducción es calcular un valor. Un valor en el cálculo lambda es una función. Por lo tanto, la β-reducción continúa hasta que la expresión parezca una abstracción de función.

Una expresión lambda que no se puede reducir más, ni mediante β-redex ni η-redex, está en forma normal. Tenga en cuenta que la conversión alfa puede convertir funciones. Todas las formas normales que se pueden convertir entre sí mediante la conversión α se definen como iguales. Consulte el artículo principal sobre la forma normal beta para obtener más detalles.

Definición de sintaxis en BNF

El cálculo lambda tiene una sintaxis sencilla. Un programa de cálculo lambda tiene la sintaxis de una expresión donde:

La lista de variables se define como,

 < lista-variables >  ::=  < variable > | < variable > , < lista-variables >

Una variable tal como la utilizan los científicos informáticos tiene la sintaxis:

 < variable >  ::=  < alfa >  < extensión >  < extensión >  ::=  < extensión >  ::=  < carácter-extensión >  < extensión >  < carácter-extensión >  ::=  < alfa > | < dígito > | _

En ocasiones, los matemáticos limitan una variable a un solo carácter alfabético. Cuando se utiliza esta convención, se omite la coma de la lista de variables.

Una abstracción lambda tiene una precedencia menor que una aplicación, por lo que;

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

Las aplicaciones se dejan asociativas;

${\displaystyle x\ y\ z=(x\ y)\ z}$

Una abstracción con múltiples parámetros es equivalente a múltiples abstracciones de un parámetro.

${\displaystyle \lambda x.y.z=\lambda x.\lambda y.z}$

dónde,

• x es una variable
• y es una lista de variables
• z es una expresión

Definición como fórmulas matemáticas

El problema de cómo se pueden renombrar las variables es complicado. Esta definición evita el problema sustituyendo todos los nombres por nombres canónicos, que se construyen en función de la posición de la definición del nombre en la expresión. El enfoque es análogo al que utiliza un compilador, pero se ha adaptado para que funcione dentro de las limitaciones de las matemáticas.

Semántica

La ejecución de una expresión lambda se realiza mediante las siguientes reducciones y transformaciones,

1. conversión α - ${\displaystyle \operatorname {alpha-conv} (a)\to \operatorname {canonym} [A,P]=\operatorname {canonym} [a[A],P]}$
2. β-reducción - ${\displaystyle \operatorname {beta-redex} [\lambda p.b\ v]=b[p:=v]}$
3. η-reducción - ${\displaystyle x\not \in \operatorname {FV} (f)\to \operatorname {eta-redex} [\lambda x.(f\ x)]=f}$

dónde,

• canonym es un cambio de nombre de una expresión lambda para darle a la expresión nombres estándar, basados ​​en la posición del nombre en la expresión.
• Operador de sustitución, es la sustitución del nombre por la expresión lambda en expresión lambda . ${\displaystyle b[p:=v]}$ ${\displaystyle p}$ ${\displaystyle v}$ ${\displaystyle b}$
• El conjunto de variables libres es el conjunto de variables que no pertenecen a una abstracción lambda en . ${\displaystyle \operatorname {FV} (f)}$ ${\displaystyle f}$

La ejecución consiste en realizar reducciones β y reducciones η en subexpresiones en el canon de una expresión lambda hasta que el resultado sea una función lambda (abstracción) en la forma normal .

Se consideran equivalentes todas las conversiones α de una expresión λ.

Canonym - Nombres canónicos

Canonym es una función que toma una expresión lambda y renombra todos los nombres de manera canónica, según sus posiciones en la expresión. Esto se puede implementar de la siguiente manera:

${\displaystyle {\begin{aligned}\operatorname {canonym} [L,Q]&=\operatorname {canonym} [L,O,Q]\\\operatorname {canonym} [\lambda p.b,M,Q]&=\lambda \operatorname {name} (Q).\operatorname {canonym} [b,M[p:=Q],Q+N]\\\operatorname {canonym} [X\ Y,x,Q]&=\operatorname {canonym} [X,x,Q+F]\ \operatorname {canonym} [Y,x,E+S]\\\operatorname {canonym} [x,M,Q]&=\operatorname {name} (M[x])\end{aligned}}}$

Donde, N es la cadena "N", F es la cadena "F", S es la cadena "S", + es concatenación y "nombre" convierte una cadena en un nombre.

Operadores de mapas

Mapa de un valor a otro si el valor está en el mapa. O es el mapa vacío.

1. ${\displaystyle O[x]=x}$
2. ${\displaystyle M[x:=y][x]=y}$
3. ${\displaystyle x\neq z\to M[x:=y][z]=M[z]}$

Operador de sustitución

Si L es una expresión lambda, x es un nombre e y es una expresión lambda; significa sustituir x por y en L. Las reglas son: ${\displaystyle L[x:=y]}$

1. ${\displaystyle (\lambda p.b)[x:=y]=\lambda p.b[x:=y]}$
2. ${\displaystyle (X\,Y)[x:=y]=X[x:=y]\,Y[x:=y]}$
3. ${\displaystyle z=x\to (z)[x:=y]=y}$
4. ${\displaystyle z\neq x\to (z)[x:=y]=z}$

Tenga en cuenta que la regla 1 debe modificarse si se va a utilizar en expresiones lambda que no hayan cambiado de nombre de forma canónica. Consulte Cambios en el operador de sustitución.

Conjuntos de variables libres y acotadas

El conjunto de variables libres de una expresión lambda, M, se denota como FV(M). Este es el conjunto de nombres de variables que tienen instancias no vinculadas (usadas) en una abstracción lambda, dentro de la expresión lambda. Son los nombres de variables que pueden estar vinculados a variables de parámetros formales desde fuera de la expresión lambda.

El conjunto de variables enlazadas de una expresión lambda, M, se denota como BV(M). Este es el conjunto de nombres de variables que tienen instancias enlazadas (usadas) en una abstracción lambda, dentro de la expresión lambda.

Las reglas para los dos conjuntos se dan a continuación. ^[5]

Uso;

• El conjunto de variables libres, FV, se utiliza arriba en la definición de la η-reducción.
• El conjunto de variables ligadas, BV, se utiliza en la regla para β-redex de expresión lambda no canónica.

Estrategia de evaluación

Esta definición matemática está estructurada de modo que represente el resultado y no la forma en que se calcula. Sin embargo, el resultado puede ser diferente entre una evaluación perezosa y una evaluación entusiasta. Esta diferencia se describe en las fórmulas de evaluación.

Las definiciones que se dan aquí suponen que se utilizará la primera definición que coincida con la expresión lambda. Esta convención se utiliza para que la definición sea más legible. De lo contrario, se requerirían algunas condiciones if para que la definición sea precisa.

Ejecutar o evaluar una expresión lambda L es,

${\displaystyle \operatorname {eval} [\operatorname {canonym} [L,Q]]}$

donde Q es un prefijo de nombre posiblemente una cadena vacía y eval se define por,

${\displaystyle {\begin{aligned}\operatorname {eval} [x\ y]&=\operatorname {eval} [\operatorname {apply} [\operatorname {eval} [x]\ \operatorname {strategy} [y]]]\\\operatorname {apply} [(\lambda x.y)\ z]&=\operatorname {canonym} [\operatorname {beta-redex} [(\lambda x.y)\ z],x]\\\operatorname {apply} [x]&=x{\text{ if x does match the above.}}\\\operatorname {eval} [\lambda x.(f\ x)]&=\operatorname {eval} [\operatorname {eta-redex} [\lambda x.(f\ x)]]\\\operatorname {eval} [L]&=L\\\operatorname {lazy} [X]&=X\\\operatorname {eager} [X]&=\operatorname {eval} [X]\end{aligned}}}$

Entonces la estrategia de evaluación puede elegirse como,

${\displaystyle {\begin{aligned}\operatorname {strategy} &=\operatorname {lazy} \\\operatorname {strategy} &=\operatorname {eager} \end{aligned}}}$

El resultado puede ser diferente según la estrategia utilizada. La evaluación ansiosa aplicará todas las reducciones posibles, dejando el resultado en forma normal, mientras que la evaluación perezosa omitirá algunas reducciones en los parámetros, dejando el resultado en "forma normal de cabeza débil".

Forma normal

Se han aplicado todas las reducciones que se pueden aplicar. Este es el resultado obtenido al aplicar la evaluación entusiasta.

${\displaystyle {\begin{aligned}\operatorname {normal} [(\lambda x.y)\ z]&=\operatorname {false} \\\operatorname {normal} [\lambda x.(f\ x)]&=\operatorname {false} \\\operatorname {normal} [x\ y]&=\operatorname {normal} [x]\land \operatorname {normal} [y]\end{aligned}}}$

En todos los otros casos,

${\displaystyle \operatorname {normal} [x]=\operatorname {true} }$

Forma normal de cabeza débil

(La definición a continuación es errónea, está en contradicción con la definición que dice que la forma normal de la cabeza débil es la forma normal de la cabeza o el término es una abstracción. ^[8] La noción fue introducida por Simon Peyton Jones. ^[9] )

Se han aplicado reducciones a la función (cabeza), pero no todas las reducciones al parámetro. Este es el resultado obtenido al aplicar la evaluación diferida.

${\displaystyle {\begin{aligned}\operatorname {whnf} [(\lambda x.y)\ z]&=\operatorname {false} \\\operatorname {whnf} [\lambda x.(f\ x)]&=\operatorname {false} \\\operatorname {whnf} [x\ y]&=\operatorname {whnf} [x]\end{aligned}}}$

En todos los otros casos,

${\displaystyle \operatorname {whnf} [x]=\operatorname {true} }$

Derivación del estándar a partir de la definición matemática

La definición estándar del cálculo lambda utiliza algunas definiciones que pueden considerarse teoremas, que pueden demostrarse basándose en la definición como fórmulas matemáticas.

La definición de nombres canónicos aborda el problema de la identidad de las variables construyendo un nombre único para cada variable basado en la posición de la abstracción lambda para el nombre de la variable en la expresión.

Esta definición introduce las reglas utilizadas en la definición estándar y las explica en términos de la definición de cambio de nombre canónico.

Variables libres y variables ligadas

El operador de abstracción lambda, λ, toma una variable de parámetro formal y una expresión de cuerpo. Cuando se evalúa, la variable de parámetro formal se identifica con el valor del parámetro real.

Las variables de una expresión lambda pueden ser "ligadas" o "libres". Las variables ligadas son nombres de variables que ya están asociados a variables de parámetros formales en la expresión.

Se dice que la variable de parámetro formal enlaza el nombre de la variable dondequiera que aparezca libre en el cuerpo. Se dice que las variables (nombres) que ya se han emparejado con la variable de parámetro formal están enlazadas . Todas las demás variables en la expresión se denominan libres .

Por ejemplo, en la siguiente expresión y es una variable ligada y x es libre: . Observe también que una variable está ligada por su abstracción lambda "más cercana". En el siguiente ejemplo, la única aparición de x en la expresión está ligada por la segunda lambda: ${\displaystyle \lambda y.x\ x\ y}$ ${\displaystyle \lambda x.y\ (\lambda x.z\ x)}$

Cambios en el operador de sustitución

En la definición del Operador de Sustitución la regla,

• ${\displaystyle (\lambda p.b)[x:=y]=\lambda p.b[x:=y]}$

debe ser reemplazado por,

1. ${\displaystyle (\lambda x.b)[x:=y]=\lambda x.b}$
2. ${\displaystyle z\neq x\ \to (\lambda z.b)[x:=y]=\lambda z.b[x:=y]}$

Esto sirve para evitar que se sustituyan las variables enlazadas con el mismo nombre. Esto no habría ocurrido en una expresión lambda con un nombre canónico.

Por ejemplo, las reglas anteriores se habrían traducido erróneamente:

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

Las nuevas reglas bloquean esta sustitución de modo que permanece como,

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

Transformación

El significado de las expresiones lambda se define por cómo se pueden transformar o reducir las expresiones. ^[6]

Hay tres tipos de transformación:

• α-conversión : cambio de variables límite ( alfa );
• β-reducción : aplicar funciones a sus argumentos ( beta ), llamar funciones;
• η-reducción : que captura una noción de extensionalidad ( eta ).

También hablamos de equivalencias resultantes: dos expresiones son β-equivalentes , si pueden ser β-convertidas en la misma expresión, y las α/η-equivalencias se definen de manera similar.

El término redex , abreviatura de expresión reducible , se refiere a subtérminos que pueden reducirse mediante una de las reglas de reducción.

conversión α

La conversión alfa, a veces conocida como cambio de nombre alfa, ^[7] permite cambiar los nombres de las variables ligadas. Por ejemplo, la conversión alfa de podría dar como resultado . Los términos que difieren solo por la conversión alfa se denominan α-equivalentes . ${\displaystyle \lambda x.x}$ ${\displaystyle \lambda y.y}$

En una conversión α, los nombres pueden sustituirse por nombres nuevos si el nuevo nombre no está libre en el cuerpo, ya que esto conduciría a la captura de variables libres.

${\displaystyle (y\not \in FV(b)\land a(\lambda x.b)=\lambda y.b[x:=y])\to \operatorname {alpha-con} (a)}$

Tenga en cuenta que la sustitución no se repetirá en el cuerpo de las expresiones lambda con parámetros formales debido al cambio en el operador de sustitución descrito anteriormente. ${\displaystyle x}$

Ver ejemplo;

β-reducción (evitación de captura)

La β-reducción captura la idea de aplicación de función (también llamada llamada de función) e implementa la sustitución de la expresión del parámetro real por la variable del parámetro formal. La β-reducción se define en términos de sustitución.

Si no hay nombres de variables libres en el parámetro real y enlazados en el cuerpo, se puede realizar una reducción β en la abstracción lambda sin cambio de nombre canónico.

${\displaystyle (\forall z:z\not \in FV(y)\lor z\not \in BV(b))\to \operatorname {beta-redex} [\lambda x.b\ y]=b[x:=y]}$

El cambio de nombre alfa se puede utilizar para cambiar el nombre de nombres que están libres en pero ligados en , para cumplir con la condición previa para esta transformación. ${\displaystyle b}$ ${\displaystyle y}$ ${\displaystyle b}$

Ver ejemplo;

${\displaystyle {\begin{array}{r}((\lambda x.z\ x)(\lambda y.z\ y))[z:=(x\ y)]\\((\lambda a.z\ a)(\lambda b.z\ b))[z:=(x\ y)]\end{array}}}$

En este ejemplo,

1. En el β-redex,
   1. Las variables libres son, ${\displaystyle \operatorname {FV} (x\ y)=\{x,y\}}$
   2. Las variables ligadas son, ${\displaystyle \operatorname {BV} ((\lambda x.z\ x)(\lambda y.z\ y))=\{x,y\}}$
2. El β-redex ingenuo cambió el significado de la expresión porque x e y del parámetro real quedaron capturados cuando las expresiones se sustituyeron en las abstracciones internas.
3. El cambio de nombre alfa eliminó el problema al cambiar los nombres de x e y en la abstracción interna para que sean distintos de los nombres de x e y en el parámetro real.
   1. Las variables libres son, ${\displaystyle \operatorname {FV} (x\ y)=\{x,y\}}$
   2. Las variables ligadas son, ${\displaystyle \operatorname {BV} ((\lambda a.z\ a)(\lambda b.z\ b))=\{a,b\}}$
4. El β-redex procedió entonces con el significado previsto.

η-reducción

La η-reducción expresa la idea de extensionalidad , que en este contexto es que dos funciones son iguales si y sólo si dan el mismo resultado para todos los argumentos.

La reducción η se puede utilizar sin cambios en expresiones lambda que no hayan sido renombradas canónicamente.

${\displaystyle x\not \in \mathrm {FV} (f)\to {\text{η-redex}}[\lambda x.(fx)]=f}$

El problema de utilizar un η-redex cuando f tiene variables libres se muestra en este ejemplo,

Este uso indebido de la η-reducción cambia el significado al dejar x sin sustituir. ${\displaystyle \lambda y.y\,x}$

Referencias

1. Barendregt, Hendrik Pieter (1984), El cálculo lambda: su sintaxis y semántica, Estudios de lógica y fundamentos de las matemáticas, vol. 103 (edición revisada), Holanda Septentrional, Ámsterdam, ISBN. 978-0-444-87508-2, archivado desde el original el 23 de agosto de 2004— Correcciones
2. "Ejemplo de reglas de asociatividad". Lambda-bound.com . Consultado el 18 de junio de 2012 .
3. Selinger, Peter (2008), Notas de clase sobre el cálculo lambda (PDF) , vol. 0804, Departamento de Matemáticas y Estadística, Universidad de Ottawa, pág. 9, arXiv : 0804.3434 , Bibcode :2008arXiv0804.3434S
4. "Ejemplo de regla de asociatividad". Lambda-bound.com . Consultado el 18 de junio de 2012 .
5. Barendregt, Henk; Barendsen, Erik (marzo de 2000), Introducción al cálculo Lambda (PDF)
6. de Queiroz, Ruy JGB "Una explicación teórica de la programación y el papel de las reglas de reducción". Dialectica 42 (4), páginas 265-282, 1988.
7. Turbak, Franklyn; Gifford, David (2008), Conceptos de diseño en lenguajes de programación , MIT press, pág. 251, ISBN 978-0-262-20175-9
8. "Notas sobre la evaluación de términos de cálculo λ y máquinas abstractas". scholar.google.ca . Consultado el 14 de mayo de 2024 .
9. Peyton Jones, Simon L. (1987). La implementación de lenguajes de programación funcional . Englewood Cliffs, NJ: Prentice/Hill International. ISBN 978-0-13-453333-9.