Cálculo lambda

El cálculo lambda (también escrito como λ -cálculo ) es un sistema formal de lógica matemática para expresar cálculos basados ​​en la abstracción y aplicación de funciones mediante la vinculación y sustitución de variables . El cálculo lambda no tipificado, el tema de este artículo, es un modelo universal de computación que se puede utilizar para simular cualquier máquina de Turing (y viceversa). Fue introducido por el matemático Alonzo Church en la década de 1930 como parte de su investigación sobre los fundamentos de las matemáticas . En 1936, Church encontró una formulación que era lógicamente consistente y la documentó en 1940.

El cálculo lambda consiste en construir términos lambda y realizar operaciones de reducción sobre ellos. En la forma más simple del cálculo lambda, los términos se construyen utilizando únicamente las siguientes reglas: ^[a]

1. ${\textstyle x}$:Una variable es un carácter o cadena que representa un parámetro.
2. ${\textstyle (\lambda xM)}$:Una abstracción lambda es una definición de función, que toma como entrada la variable enlazada (entre λ y el punctum/punto ) y devuelve el cuerpo .${\estilo de visualización x}$${\textstyle M}$
3. ${\textstyle (M\ N)}$: Una aplicación que aplica una función a un argumento . Tanto y son términos lambda.${\textstyle M}$${\textstyle N}$${\textstyle M}$${\textstyle N}$

Las operaciones de reducción incluyen:

• ${\textstyle (\lambda xM[x])\rightarrow (\lambda yM[y])}$ : conversión α, cambio de nombre de las variables enlazadas en la expresión. Se utiliza para evitar colisiones de nombres .
• ${\textstyle ((\lambda xM)\ N)\rightarrow (M[x:=N])}$ : β-reducción, ^[b] reemplazando las variables enlazadas con la expresión del argumento en el cuerpo de la abstracción.

Si se utiliza la indexación de De Bruijn , ya no se requiere la conversión α, ya que no habrá colisiones de nombres. Si la aplicación repetida de los pasos de reducción finalmente termina, entonces, según el teorema de Church-Rosser, se producirá una forma β-normal .

Los nombres de variables no son necesarios si se utiliza una función lambda universal, como Iota y Jot , que puede crear cualquier comportamiento de función llamándola a sí misma en varias combinaciones.

El cálculo lambda es Turing completo , es decir, es un modelo universal de computación que puede utilizarse para simular cualquier máquina de Turing . ^[3] Su homónimo, la letra griega lambda (λ), se utiliza en expresiones lambda y términos lambda para denotar la vinculación de una variable en una función .

El cálculo lambda puede ser tipado o no tipado . En el cálculo lambda tipado, las funciones solo se pueden aplicar si son capaces de aceptar el "tipo" de datos de entrada dado. Los cálculos lambda tipados son más débiles que el cálculo lambda no tipado, que es el tema principal de este artículo, en el sentido de que los cálculos lambda tipados pueden expresar menos que el cálculo no tipado. Por otro lado, los cálculos lambda tipados permiten demostrar más cosas. Por ejemplo, en el cálculo lambda simplemente tipado , es un teorema que cada estrategia de evaluación termina para cada término lambda simplemente tipado, mientras que la evaluación de términos lambda no tipados no necesita terminar (ver más abajo). Una razón por la que hay muchos cálculos lambda tipados diferentes ha sido el deseo de hacer más (de lo que el cálculo no tipado puede hacer) sin renunciar a ser capaz de demostrar teoremas fuertes sobre el cálculo.

El cálculo lambda tiene aplicaciones en muchas áreas diferentes de las matemáticas , la filosofía , ^[4] la lingüística , ^{[5] [6]} y la informática . ^{[7] [8]} El cálculo lambda ha desempeñado un papel importante en el desarrollo de la teoría de los lenguajes de programación . Los lenguajes de programación funcional implementan el cálculo lambda. El cálculo lambda también es un tema de investigación actual en la teoría de categorías . ^[9]

El cálculo lambda fue introducido por el matemático Alonzo Church en la década de 1930 como parte de una investigación sobre los fundamentos de las matemáticas . ^{[10] [c]} El sistema original demostró ser lógicamente inconsistente en 1935 cuando Stephen Kleene y JB Rosser desarrollaron la paradoja de Kleene-Rosser . ^{[11] [12]}

Posteriormente, en 1936, Church aisló y publicó sólo la parte relevante para el cálculo, lo que ahora se llama cálculo lambda no tipificado. ^[13] En 1940, también introdujo un sistema computacionalmente más débil, pero lógicamente consistente, conocido como cálculo lambda simplemente tipificado . ^[14]

Hasta la década de 1960, cuando se aclaró su relación con los lenguajes de programación, el cálculo lambda era sólo un formalismo. Gracias a las aplicaciones de Richard Montague y otros lingüistas en la semántica del lenguaje natural, el cálculo lambda ha comenzado a disfrutar de un lugar respetable tanto en la lingüística ^[15] como en la informática. ^[16]

Existe cierta incertidumbre sobre el motivo por el cual Church utiliza la letra griega lambda (λ) como notación para la abstracción de funciones en el cálculo lambda, tal vez en parte debido a explicaciones contradictorias del propio Church. Según Cardone y Hindley (2006):

Por cierto, ¿por qué Church eligió la notación “λ”? En [una carta inédita de 1964 a Harald Dickson] afirmó claramente que provenía de la notación “ ” utilizada para la abstracción de clases por Whitehead y Russell , modificando primero “ ” a “ ” para distinguir la abstracción de funciones de la abstracción de clases, y luego cambiando “ ” a “λ” para facilitar la impresión.${\displaystyle {\hat {x}}}$${\displaystyle {\hat {x}}}$${\displaystyle \tierra x}$${\displaystyle \tierra}$

Este origen también fue reportado en [Rosser, 1984, p.338]. Por otra parte, en sus últimos años Church dijo a dos investigadores que la elección fue más bien accidental: se necesitaba un símbolo y λ simplemente fue elegido.

Dana Scott también ha abordado esta cuestión en varias conferencias públicas. ^[17] Scott cuenta que una vez le planteó una pregunta sobre el origen del símbolo lambda a John W. Addison Jr., ex alumno y yerno de Church, quien luego le escribió una postal a su suegro:

Estimado Profesor Church,

Russell tenía el operador iota y Hilbert el operador épsilon . ¿Por qué eligió lambda como operador?

Según Scott, toda la respuesta de Church consistió en devolver la postal con la siguiente anotación: " eeny, meeny, miny, moe ".

Las funciones computables son un concepto fundamental en la informática y las matemáticas. El cálculo lambda proporciona una semántica sencilla para el cálculo que resulta útil para estudiar formalmente las propiedades del cálculo. El cálculo lambda incorpora dos simplificaciones que simplifican su semántica.La primera simplificación es que el cálculo lambda trata las funciones de forma "anónima"; no les da nombres explícitos. Por ejemplo, la función

${\displaystyle \operatorname {suma\cuadrada} (x,y)=x^{2}+y^{2}}$

puede reescribirse en forma anónima como

${\displaystyle (x,y)\mapsto x^{2}+y^{2}}$

(que se lee como "una tupla de x e y se asigna a "). ^[d] De manera similar, la función${\textstyle x^{2}+y^{2}}$

${\displaystyle \nombre del operador {id} (x)=x}$

puede reescribirse en forma anónima como

${\displaystyle x\mapsto x}$

donde la entrada simplemente se asigna a sí misma. ^[d]

La segunda simplificación es que el cálculo lambda solo utiliza funciones de una sola entrada. Una función ordinaria que requiere dos entradas, por ejemplo la función , se puede transformar en una función equivalente que acepte una sola entrada y, como salida, devuelva otra función que, a su vez, acepte una sola entrada. Por ejemplo,${\textstyle \operatorname {cuadrado\_sum} }$

${\displaystyle (x,y)\mapsto x^{2}+y^{2}}$

se puede reelaborar en

${\displaystyle x\mapsto (y\mapsto x^{2}+y^{2})}$

Este método, conocido como currying , transforma una función que toma múltiples argumentos en una cadena de funciones, cada una con un solo argumento.

La aplicación de la función a los argumentos (5, 2), produce inmediatamente${\textstyle \operatorname {cuadrado\_sum} }$

${\textstyle ((x,y)\mapsto x^{2}+y^{2})(5,2)}$

${\textstyle =5^{2}+2^{2}}$

${\textstyle=29}$,

Mientras que la evaluación de la versión al curry requiere un paso más.

${\textstyle {\Bigl (}{\bigl (}x\mapsto (y\mapsto x^{2}+y^{2}){\bigr )}(5){\Bigr )}(2)}$

${\textstyle =(y\mapsto 5^{2}+y^{2})(2)}$// La definición de se ha utilizado en la expresión interna. Esto es como una β-reducción.${\estilo de visualización x}$${\estilo de visualización 5}$

${\textstyle =5^{2}+2^{2}}$// La definición de se ha utilizado con . Nuevamente, similar a la β-reducción.${\estilo de visualización y}$${\estilo de visualización 2}$

${\textstyle=29}$

para llegar al mismo resultado.

El cálculo lambda consiste en un lenguaje de términos lambda , que se definen mediante una sintaxis formal determinada, y un conjunto de reglas de transformación para manipular los términos lambda. Estas reglas de transformación pueden considerarse como una teoría ecuacional o como una definición operacional .

Como se describió anteriormente, al no tener nombres, todas las funciones en el cálculo lambda son funciones anónimas. Solo aceptan una variable de entrada, por lo que se utiliza la currificación para implementar funciones de varias variables.

La sintaxis del cálculo lambda define algunas expresiones como válidas y otras como no válidas, de la misma forma que algunas cadenas de caracteres son válidas en programas C y otras no. Una expresión válida del cálculo lambda se denomina " término lambda ".

Las siguientes tres reglas dan una definición inductiva que se puede aplicar para construir todos los términos lambda sintácticamente válidos: ^[e]

• La variable x es en sí misma un término lambda válido.
• si t es un término lambda y x es una variable, entonces ^[f] es un término lambda (llamado una abstracción );${\estilo de visualización (\lambda xt)}$
• Si t y s son términos lambda, entonces es un término lambda (llamado una aplicación ).${\estilo de visualización (t}$  ${\estilo de visualización s)}$

Ningún otro término lambda es válido. Es decir, un término lambda es válido si y solo si se puede obtener mediante la aplicación repetida de estas tres reglas. Por conveniencia, se pueden omitir algunos paréntesis al escribir un término lambda. Por ejemplo, los paréntesis más externos generalmente no se escriben. Consulte § Notación, a continuación, para obtener una descripción explícita de qué paréntesis son opcionales. También es común extender la sintaxis presentada aquí con operaciones adicionales, lo que permite dar sentido a términos como El enfoque de este artículo es el cálculo lambda puro sin extensiones, pero los términos lambda extendidos con operaciones aritméticas se utilizan con fines explicativos.${\displaystyle \lambda xx^{2}.}$

Una abstracción denota una función anónima ^[g] que toma una única entrada x y devuelve t . Por ejemplo, es una abstracción que representa la función definida mediante el uso del término para t . El nombre es superfluo cuando se utiliza la abstracción. La sintaxis vincula la variable x en el término t . La definición de una función con una abstracción simplemente "configura" la función pero no la invoca.${\displaystyle \lambda xt}$${\displaystyle \lambda x.(x^{2}+2)}$${\estilo de visualización f}$${\displaystyle f(x)=x^{2}+2,}$$estilo de visualización x^{2}+2}$${\estilo de visualización f}$${\estilo de visualización (\lambda xt)}$

Una aplicación representa la aplicación de una función t a una entrada s , es decir, representa el acto de llamar a la función t en la entrada s para producir .${\estilo de visualización t}$  ${\estilo de visualización s}$${\displaystyle t(s)}$

Un término lambda puede hacer referencia a una variable que no ha sido vinculada, como el término (que representa la definición de la función ). En este término, la variable y no ha sido definida y se considera una incógnita. La abstracción es un término sintácticamente válido y representa una función que suma su entrada a la aún desconocida y .${\displaystyle \lambda x.(x+y)}$${\displaystyle f(x)=x+y}$${\displaystyle \lambda x.(x+y)}$

Se pueden utilizar paréntesis y pueden ser necesarios para aclarar términos. Por ejemplo,

1. ${\displaystyle \lambda x.((\lambda xx)x)}$es de forma y por lo tanto es una abstracción, mientras que${\displaystyle \lambda xB}$
2. ${\displaystyle (\lambda x.(\lambda xx))}$ ${\estilo de visualización x}$es de forma y por tanto es una aplicación.${\estilo de visualización M}$  ${\estilo de visualización N}$

Los ejemplos 1 y 2 denotan términos diferentes, que difieren únicamente en la ubicación de los paréntesis. Tienen significados diferentes: el ejemplo 1 es una definición de función, mientras que el ejemplo 2 es una aplicación de función. La variable lambda x es un marcador de posición en ambos ejemplos.

Aquí, el ejemplo 1 define una función , donde es , una función anónima , con entrada ; mientras que el ejemplo 2, , es M aplicado a N, donde es el término lambda que se aplica a la entrada que es . Tanto el ejemplo 1 como el 2 se evaluarían como la función identidad .${\displaystyle \lambda xB}$${\estilo de visualización B}$${\estilo de visualización (\lambda xx)x}$${\estilo de visualización (\lambda xx)}$${\estilo de visualización x}$${\estilo de visualización M}$ ${\estilo de visualización N}$${\estilo de visualización M}$${\displaystyle (\lambda x.(\lambda xx))}$${\estilo de visualización N}$${\estilo de visualización x}$ ${\estilo de visualización \lambda xx}$

En el cálculo lambda, las funciones se consideran " valores de primera clase ", por lo que pueden usarse como entradas o devolverse como salidas de otras funciones.

Por ejemplo, el término lambda representa la función identidad , . Además, representa la función constante , la función que siempre devuelve , sin importar la entrada. Como ejemplo de una función que opera sobre funciones, la composición de funciones se puede definir como .${\estilo de visualización \lambda xx}$${\displaystyle x\mapsto x}$${\displaystyle \lambdaxy}$ ${\displaystyle x\mapsto y}$${\estilo de visualización y}$${\displaystyle \lambda f.\lambda g.\lambda x.(f(gx))}$

Existen varias nociones de "equivalencia" y "reducción" que permiten "reducir" los términos lambda a términos lambda "equivalentes".

Una forma básica de equivalencia, definible en términos lambda, es la equivalencia alfa . Capta la intuición de que la elección particular de una variable ligada, en una abstracción, no importa (normalmente). Por ejemplo, y son términos lambda alfa-equivalentes, y ambos representan la misma función (la función identidad). Los términos y no son alfa-equivalentes, porque no están ligados en una abstracción. En muchas presentaciones, es habitual identificar términos lambda alfa-equivalentes.${\estilo de visualización \lambda xx}$${\displaystyle \lambda yy}$${\estilo de visualización x}$${\estilo de visualización y}$

Las siguientes definiciones son necesarias para poder definir la β-reducción:

Las variables libres ^[h] de un término son aquellas variables que no están limitadas por una abstracción. El conjunto de variables libres de una expresión se define de forma inductiva:

• Las variables libres de son simplemente${\estilo de visualización x}$${\estilo de visualización x}$
• El conjunto de variables libres de es el conjunto de variables libres de , pero con eliminado${\displaystyle \lambda xt}$${\estilo de visualización t}$${\estilo de visualización x}$
• El conjunto de variables libres de es la unión del conjunto de variables libres de y el conjunto de variables libres de .${\estilo de visualización t}$ ${\estilo de visualización s}$${\estilo de visualización t}$${\estilo de visualización s}$

Por ejemplo, el término lambda que representa la identidad no tiene variables libres, pero la función tiene una única variable libre, .${\estilo de visualización \lambda xx}$${\displaystyle \lambdaxy}$ ${\estilo de visualización x}$${\estilo de visualización y}$

Supongamos que , y son términos lambda, y y son variables. La notación indica la sustitución de por en de una manera que evita la captura . Esto se define de la siguiente manera:${\estilo de visualización t}$${\estilo de visualización s}$${\estilo de visualización r}$${\estilo de visualización x}$${\estilo de visualización y}$${\displaystyle t[x:=r]}$${\estilo de visualización r}$${\estilo de visualización x}$${\estilo de visualización t}$

• ${\displaystyle x[x:=r]=r}$ ; con sustituido por , se convierte en${\estilo de visualización r}$${\estilo de visualización x}$${\estilo de visualización x}$${\estilo de visualización r}$
• ${\displaystyle y[x:=r]=y}$si  ; con sustituido por , (que no es ) permanece${\displaystyle x\neq y}$${\estilo de visualización r}$${\estilo de visualización x}$${\estilo de visualización y}$${\estilo de visualización x}$${\estilo de visualización y}$
• ${\estilo de visualización (t}$ ${\displaystyle s)[x:=r]=(t[x:=r])(s[x:=r])}$ ; la sustitución se distribuye a ambos lados de una aplicación
• ${\displaystyle (\lambda xt)[x:=r]=\lambda xt}$ ; una variable limitada por una abstracción no está sujeta a sustitución; sustituir dicha variable deja la abstracción sin cambios
• ${\displaystyle (\lambda yt)[x:=r]=\lambda y.(t[x:=r])}$si y no aparece entre las variables libres de ( se dice que es " fresco " para ); la sustitución de una variable que no está limitada por una abstracción se realiza en el cuerpo de la abstracción, siempre que la variable abstraída sea "fresca" para el término de sustitución .${\displaystyle x\neq y}$${\estilo de visualización y}$${\estilo de visualización r}$${\estilo de visualización y}$${\estilo de visualización r}$${\estilo de visualización y}$${\estilo de visualización r}$

Por ejemplo, , y .${\displaystyle (\lambda xx)[y:=y]=\lambda x.(x[y:=y])=\lambda xx}$${\displaystyle ((\lambda xy)x)[x:=y]=((\lambda xy)[x:=y])(x[x:=y])=(\lambda xy)y}$

La condición de frescura (que requiere que no esté en las variables libres de ) es crucial para garantizar que la sustitución no cambie el significado de las funciones.${\estilo de visualización y}$${\estilo de visualización r}$

Por ejemplo, una sustitución que ignore la condición de frescura podría generar errores: . Esta sustitución errónea convertiría la función constante en la identidad .${\displaystyle (\lambda xy)[y:=x]=\lambda x.(y[y:=x])=\lambda xx}$${\displaystyle \lambdaxy}$${\estilo de visualización \lambda xx}$

En general, el incumplimiento de la condición de frescura se puede solucionar renombrando primero con una variable nueva adecuada. Por ejemplo, volviendo a nuestra noción correcta de sustitución, en la abstracción se puede renombrar con una variable nueva para obtener , y el significado de la función se conserva por sustitución.${\displaystyle (\lambda xy)[y:=x]}$${\estilo de visualización z}$${\displaystyle (\lambda z.y)[y:=x]=\lambda z.(y[y:=x])=\lambda z.x}$

La regla de β-reducción ^[b] establece que una aplicación de la forma se reduce al término . La notación se utiliza para indicar que β-reduce a . Por ejemplo, para cada , . Esto demuestra que realmente es la identidad. De manera similar, , lo que demuestra que es una función constante.${\displaystyle (\lambda x.t)s}$${\displaystyle t[x:=s]}$${\displaystyle (\lambda x.t)s\to t[x:=s]}$${\displaystyle (\lambda x.t)s}$${\displaystyle t[x:=s]}$${\displaystyle s}$${\displaystyle (\lambda x.x)s\to x[x:=s]=s}$${\displaystyle \lambda x.x}$${\displaystyle (\lambda x.y)s\to y[x:=s]=y}$${\displaystyle \lambda x.y}$

El cálculo lambda puede considerarse una versión idealizada de un lenguaje de programación funcional, como Haskell o Standard ML . Según esta perspectiva,La β-reducción corresponde a un paso computacional. Este paso puede repetirse mediante β-reducciones adicionales hasta que no queden más aplicaciones para reducir. En el cálculo lambda no tipificado, como se presenta aquí, este proceso de reducción puede no terminar. Por ejemplo, considere el término . Aquí . Es decir, el término se reduce a sí mismo en una única β-reducción y, por lo tanto, el proceso de reducción nunca terminará.${\displaystyle \Omega =(\lambda x.xx)(\lambda x.xx)}$${\displaystyle (\lambda x.xx)(\lambda x.xx)\to (xx)[x:=\lambda x.xx]=(x[x:=\lambda x.xx])(x[x:=\lambda x.xx])=(\lambda x.xx)(\lambda x.xx)}$

Otro aspecto del cálculo lambda sin tipo es que no distingue entre distintos tipos de datos. Por ejemplo, puede ser conveniente escribir una función que solo opere con números. Sin embargo, en el cálculo lambda sin tipo no hay forma de evitar que una función se aplique a valores de verdad , cadenas u otros objetos que no sean números.

Las expresiones lambda se componen de:

• variables v ₁ , v ₂ , ...;
• los símbolos de abstracción λ (lambda) y . (punto);
• paréntesis ().

El conjunto de expresiones lambda, Λ , se puede definir inductivamente :

1. Si x es una variable, entonces x ∈ Λ.
2. Si x es una variable y M ∈ Λ, entonces (λ x . M ) ∈ Λ.
3. Si M , N ∈ Λ, entonces ( MN ) ∈ Λ.

Las instancias de la regla 2 se conocen como abstracciones y las instancias de la regla 3 se conocen como aplicaciones . ^[18] Véase § expresión reducible

Este conjunto de reglas puede escribirse en forma Backus-Naur como:

 < expresión >  :== < abstracción > | < aplicación > | < variable >  < abstracción >  :== λ < variable > . < expresión >  < aplicación >  :== ( < expresión >  < expresión > ) < variable >  :== v1 | v2 | ...

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

• Los paréntesis más externos se eliminan: M N en lugar de ( M N ).
• Se supone que las aplicaciones son asociativas por la izquierda: se puede escribir M N P en lugar de (( M N ) P ). ^[19]
• Cuando todas las variables son de una sola letra, se puede omitir el espacio en las aplicaciones: MNP en lugar de M N P . ^[20]
• El cuerpo de una abstracción se extiende lo más a la derecha posible : λ x . MN significa λ x .( MN ) y no (λ x . M ) N .
• Una secuencia de abstracciones se contrae: λ x .λ y .λ z . N se abrevia como λ xyz . N . ^{[21] [19]}

Se dice que el operador de abstracción, λ, vincula su variable donde sea que aparezca en el cuerpo de la abstracción. Se dice que las variables que caen dentro del alcance de una abstracción están vinculadas . En una expresión λ x . M , la parte λ x se suele llamar vinculante , como una pista de que la variable x se vincula anteponiendo λ x a M . Todas las demás variables se denominan libres . Por ejemplo, en la expresión λ y . xxy , y es una variable vinculada y x es una variable libre. Además, una variable está vinculada por su abstracción más cercana. En el siguiente ejemplo, la única aparición de x en la expresión está vinculada por el segundo lambda: λ x . y (λ x . zx ).

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

1. FV( x ) = { x }, donde x es una variable.
2. FV(λ x . M ) = FV( M ) \ { x }. ^[i]
3. FV( MN ) = FV( M ) ∪ FV( N ). ^[j]

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 .

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

Hay tres tipos de reducción:

• α-conversión : cambio de variables ligadas;
• β-reducción : aplicación de funciones a sus argumentos;
• η-reducción : que captura una noción de extensionalidad.

También hablamos de equivalencias resultantes: dos expresiones son α-equivalentes si pueden ser α-convertidas en la misma expresión. La β-equivalencia y la η-equivalencia 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, (λ x . M ) N es un β-redex al expresar la sustitución de N por x en M . La expresión a la que se reduce un redex se llama su reduct ; el reduct de (λ x . M ) N es M [ x  := N ]. ^[b]

Si x no es libre en M , λ x . M x es también un η-redex, con una reducción de M .

La conversión α ( alpha -conversión), a veces conocida como α-renombrado, ^[23] permite cambiar los nombres de las variables ligadas. Por ejemplo, la conversión α de λ x . x podría dar como resultado λ y . y . Los términos que difieren solo por la conversión α se denominan α-equivalentes . Con frecuencia, en los usos del cálculo lambda, los términos α-equivalentes se consideran equivalentes.

Las reglas precisas para la conversión α no son completamente triviales. Primero, cuando se convierte α una abstracción, las únicas ocurrencias de variables que se renombran son aquellas que están ligadas a la misma abstracción. Por ejemplo, una conversión α de λ x .λ x . x podría resultar en λ y .λ x . x , pero no podría resultar en λ y .λ x . y . Este último tiene un significado diferente del original. Esto es análogo a la noción de programación de sombreado de variables .

En segundo lugar, la conversión α no es posible si da como resultado que una variable sea capturada por una abstracción diferente. Por ejemplo, si reemplazamos x por y en λ x .λ y . x , obtenemos λ y .λ y . y , que no es en absoluto lo mismo.

En lenguajes de programación con alcance estático, la conversión α se puede utilizar 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 α para que la resolución de nombres sea trivial ).

En la notación del índice De Bruijn , dos términos α-equivalentes son sintácticamente idénticos.

La sustitución, escrita M [ x  := N ], es el proceso de reemplazar todas las ocurrencias libres de la variable x en la expresión M por la expresión 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 lambda):

x [ x  := N ] = N

y [ x  := N ] = y , si x ≠ y

( M ₁ M ₂ )[ x  := N ] = M ₁ [ x  := N ] M ₂ [ x  := N ]

(λ x . M )[ x  := N ] = λ x . M

(λ y . M )[ x  := N ] = λ y .( M [ x  := N ]), si x ≠ y e y ∉ FV( N ) Véase más arriba para FV

Para sustituir en una abstracción, a veces es necesario realizar una conversión α de la expresión. Por ejemplo, no es correcto que (λ x . y )[ y  := x ] dé como resultado λ x . x , porque se suponía que la x sustituida era libre pero terminó siendo ligada. La sustitución correcta en este caso es λ z . x , hasta la equivalencia α. La sustitución se define de forma única hasta la equivalencia α. Consulte las sustituciones que evitan la captura más arriba .

La β-reducción ( reducción beta ) captura la idea de aplicación de funciones. La β-reducción se define en términos de sustitución: la β-reducción de (λ x . M ) N es M [ x  := N ]. ^[b]

Por ejemplo, asumiendo alguna codificación de 2, 7, ×, tenemos la siguiente β-reducción: (λ n . n × 2) 7 → 7 × 2.

Se puede ver que la β-reducción es lo mismo que el concepto de reducibilidad local en la deducción natural , a través del isomorfismo de Curry-Howard .

La η-reducción ( reducción eta ) expresa la idea de extensionalidad , ^[24] 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 convierte entre λ x . f x y f siempre que x no aparezca libre en f .

Se puede ver que la η-reducción es lo mismo que el concepto de completitud local en la deducción natural , a través del isomorfismo de Curry-Howard .

Para el cálculo lambda no tipado, la β-reducción como regla de reescritura no es ni fuertemente normalizadora ni débilmente normalizadora .

Sin embargo, se puede demostrar que la β-reducción es confluente cuando se trabaja hasta la α-conversión (es decir, consideramos que dos formas normales son iguales si es posible α-convertir una en la otra).

Por lo tanto, tanto los términos fuertemente normalizados como los débiles tienen una forma normal única. En el caso de los términos fuertemente normalizados, cualquier estrategia de reducción garantiza la obtención de la forma normal, mientras que, en el caso de los términos débilmente normalizados, algunas estrategias de reducción pueden no lograr encontrarla.

El cálculo lambda básico se puede utilizar para modelar aritmética , operaciones booleanas, estructuras de datos y recursión, como se ilustra en las siguientes subsecciones i , ii , iii y § iv .

Hay varias formas posibles de definir los números naturales en el cálculo lambda, pero los más comunes son los numerales de Church , que se pueden definir de la siguiente manera:

0 := λ f .λ x . x

1 := λ f . λ x . f x

2 := λ f . λ x . f ( f x )

3 := λ f . λ x . f ( f ( f x ))

y así sucesivamente. O utilizando la sintaxis alternativa presentada anteriormente en Notación :

0 := λ fx . x

1 := λ fx . fx

2 := λ fx . f ( f x )

3 := λ fx . f ( f ( f x ))

Un numeral de Church es una función de orden superior : toma una función de un solo argumento f y devuelve otra función de un solo argumento. El numeral de Church n es una función que toma una función f como argumento y devuelve la n -ésima composición de f , es decir, la función f compuesta consigo misma n veces. Esto se denota f ^{( n )} y es de hecho la n -ésima potencia de f (considerada como un operador); f ⁽⁰⁾ se define como la función identidad. Tales composiciones repetidas (de una sola función f ) obedecen las leyes de los exponentes , por lo que estos numerales se pueden usar para aritmética. (En el cálculo lambda original de Church, se requería que el parámetro formal de una expresión lambda apareciera al menos una vez en el cuerpo de la función, lo que hacía imposible la definición anterior de 0 ).

Una forma de pensar en el numeral de la Iglesia n , que suele ser útil al analizar programas, es como una instrucción 'repetir n veces'. Por ejemplo, utilizando las funciones PAIR y NIL definidas a continuación, se puede definir una función que construya una lista (enlazada) de n elementos todos iguales a x repitiendo 'anteponer otro elemento x ' n veces, comenzando desde una lista vacía. El término lambda es

λ n .λ x . n (PAR x ) NULO

Variando lo que se repite y variando a qué argumento se aplica esa función que se repite, se pueden lograr muchos efectos diferentes.

Podemos definir una función sucesora, que toma un numeral de Church n y devuelve n + 1 agregando otra aplicación de f , donde '(mf)x' significa que la función 'f' se aplica 'm' veces en 'x':

SUCC := λ n .λ f .λ x . f ( n f x )

Dado que la composición m -ésima de f compuesta con la composición n -ésima de f da la composición m + n -ésima de f , la adición se puede definir de la siguiente manera:

MÁS := λ m .λ n .λ f .λ x . m f ( n f x )

PLUS se puede considerar como una función que toma dos números naturales como argumentos y devuelve un número natural; se puede verificar que

MÁS 2 3

y

5

son expresiones lambda β-equivalentes. Dado que sumar m a un número n se puede lograr sumando 1 m veces, una definición alternativa es:

MÁS := λ m .λ n . m SUCC norte  ^[25]

De manera similar, la multiplicación se puede definir como

MULT := λ m .λ n .λ f . m ( n f ) ^[21]

Alternativamente

MULT := λ m .λ n . metro (MÁS norte ) 0

ya que multiplicar m y n es lo mismo que repetir la función de sumar n m veces y luego aplicarla a cero. La exponenciación tiene una representación bastante simple en los números de la Iglesia, a saber:

POW := λ b .λ e . e b ^[1]

La función predecesora definida por PRED n = n − 1 para un entero positivo n y PRED 0 = 0 es considerablemente más difícil. La fórmula

PRED := λ n .λ f .λ x . norte (λ g .λ h . h ( g f )) (λ u . x ) (λ u . u )

se puede validar mostrando inductivamente que si T denota (λ g .λ h . h ( g f )) , entonces T ^{( n )} (λ u . x ) = (λ h . h ( f ^{( n −1)} ( x ))) para n > 0 . A continuación se dan otras dos definiciones de PRED , una utilizando condicionales y la otra utilizando pares. Con la función predecesora, la resta es sencilla. Definiendo

SUB := λ metro .λ norte . norte PRED m ,

SUB m n produce m − n cuando m > n y 0 en caso contrario.

Por convención, se utilizan las dos definiciones siguientes (conocidas como booleanos de Church) para los valores booleanos VERDADERO y FALSO :

VERDADERO := λ x .λ y . x

FALSO := λ x .λ y . y

Luego, con estos dos términos lambda, podemos definir algunos operadores lógicos (estas son solo formulaciones posibles; otras expresiones podrían ser igualmente correctas):

Y := λ p .λ q . p q p

O := λ p .λ q . p p q

NO := λ p . p FALSO VERDADERO

ENTONCES:= λ p .λ a .λ b . pag ​ ​

Ahora podemos calcular algunas funciones lógicas, por ejemplo:

Y VERDADERO FALSO

≡ (λ p .λ q . p q p ) VERDADERO FALSO → _β VERDADERO FALSO VERDADERO

≡ (λ x .λ y . x ) FALSO VERDADERO → _β FALSO

y vemos que Y VERDADERO FALSO es equivalente a FALSO .

Un predicado es una función que devuelve un valor booleano. El predicado más fundamental es ISZERO , que devuelve TRUE si su argumento es el numeral eclesiástico 0 , pero FALSE si su argumento es cualquier otro numeral eclesiástico:

ES CERO := λ norte . n (λ x .FALSO) VERDADERO

El siguiente predicado prueba si el primer argumento es menor o igual que el segundo:

LEQ := λ m .λ n .ISZERO (SUB m n ) ,

y como m = n , si LEQ m n y LEQ n m , es sencillo construir un predicado para la igualdad numérica.

La disponibilidad de predicados y la definición anterior de VERDADERO y FALSO hacen que sea conveniente escribir expresiones "si-entonces-de lo contrario" en el cálculo lambda. Por ejemplo, la función predecesora se puede definir como:

PRED := λ norte . n (λ g .λ k .ISZERO ( g 1) k (MÁS ( g k ) 1)) (λ v .0) 0

lo cual se puede verificar mostrando inductivamente que n (λ g .λ k .ISZERO ( g 1) k (PLUS ( g k ) 1)) (λ v .0) es la función suma n − 1 para n > 0.

Un par (2-tuplas) se puede definir en términos de VERDADERO y FALSO , utilizando la codificación Church para pares . Por ejemplo, PAIR encapsula el par ( x , y ), FIRST devuelve el primer elemento del par y SECOND devuelve el segundo.

PAR := λ x .λ y .λ f . f x y

PRIMERO := λ p . p VERDADERO

SEGUNDO := λ p . p FALSO

NULO := λ x .VERDADERO

NULO := λ p . p (λ x .λ y .FALSO)

Una lista enlazada se puede definir como NIL para la lista vacía o como el PAR de un elemento y una lista más pequeña. El predicado NULL prueba el valor NIL . (Alternativamente, con NIL := FALSE , la construcción l (λ h .λ t .λ z .deal_with_head_ h _and_tail_ t ) (deal_with_nil) obvia la necesidad de una prueba NULL explícita).

Como ejemplo del uso de pares, la función de desplazamiento e incremento que asigna ( m , n ) a ( n , n + 1) se puede definir como

Φ := λ x .PAR (SEGUNDO x ) (SUCC (SEGUNDO x ))

lo que nos permite dar quizás la versión más transparente de la función predecesora:

PRED := λ n .PRIMERO ( n Φ (PAR 0 0)).

Existe una gran cantidad de expresiones idiomáticas de programación para el cálculo lambda. Muchas de ellas se desarrollaron originalmente en el contexto del uso del cálculo lambda como base para la semántica de los lenguajes de programación , utilizando efectivamente el cálculo lambda como un lenguaje de programación de bajo nivel . Debido a que varios lenguajes de programación incluyen el cálculo lambda (o algo muy similar) como un fragmento, estas técnicas también se utilizan en la programación práctica, pero pueden percibirse como oscuras o extrañas.

En el cálculo lambda, una biblioteca tomaría la forma de una colección de funciones definidas previamente, que como términos lambda son simplemente constantes particulares. El cálculo lambda puro no tiene un concepto de constantes nombradas ya que todos los términos lambda atómicos son variables, pero uno puede emular tener constantes nombradas dejando de lado una variable como el nombre de la constante, usando abstracción para unir esa variable en el cuerpo principal y aplicar esa abstracción a la definición deseada. Por lo tanto, para usar f para significar N (algún término lambda explícito) en M (otro término lambda, el "programa principal"), uno puede decir

(λ f . M ) N

Los autores a menudo introducen azúcar sintáctico , como let , ^[k] para permitir escribir lo anterior en un orden más intuitivo.

sea ​​f = N en M

Al encadenar dichas definiciones, se puede escribir un "programa" de cálculo lambda como cero o más definiciones de funciones, seguidas de un término lambda que utiliza esas funciones que constituyen el cuerpo principal del programa.

Una restricción notable de este let es que el nombre f no debe estar definido en N , para que N quede fuera del alcance de la abstracción que vincula f ; esto significa que no se puede usar una definición de función recursiva como N con let . La construcción letrec ^[l] permitiría escribir definiciones de funciones recursivas.

La recursión es la definición de una función que se invoca a sí misma. Una definición que se contiene a sí misma dentro de sí misma, por valor, lleva a que todo el valor sea de tamaño infinito. Otras notaciones que admiten la recursión de forma nativa superan esto haciendo referencia a la definición de la función por nombre . El cálculo lambda no puede expresar esto: todas las funciones son anónimas en el cálculo lambda, por lo que no podemos hacer referencia por nombre a un valor que aún no se ha definido, dentro del término lambda que define ese mismo valor. Sin embargo, una expresión lambda puede recibirse a sí misma como su propio argumento, por ejemplo en  (λ x . x x ) E . Aquí E debería ser una abstracción, aplicando su parámetro a un valor para expresar la recursión.

Consideremos la función factorial F( n ) definida recursivamente por

F( n ) = 1, si n = 0; de lo contrario n × F( n − 1) .

En la expresión lambda que representa esta función, se supondrá que un parámetro (normalmente el primero) recibe la expresión lambda como su valor, de modo que llamarlo (aplicarlo a un argumento) equivaldrá a una recursión. Por lo tanto, para lograr la recursión, el argumento que se pretende que haga referencia a sí mismo (llamado aquí r ) siempre debe pasarse a sí mismo dentro del cuerpo de la función, en un punto de llamada:

G := λ r . λ n .(1, si n = 0; de lo contrario n × ( r r ( n −1)))

con  r r x = F x = G r x  para cumplir, entonces  r = G  y

F := GG = (λ x . x x ) G

La autoaplicación logra la replicación aquí, pasando la expresión lambda de la función a la siguiente invocación como un valor de argumento, haciéndola disponible para ser referenciada y llamada allí.

Esto lo resuelve, pero requiere reescribir cada llamada recursiva como una aplicación propia. Nos gustaría tener una solución genérica, sin necesidad de reescribir nada:

G := λ r . λ n .(1, si n = 0; de lo contrario n × ( r ( n −1)))

con  r x = F x = G r x  para cumplir, entonces  r = G r =: FIJO G  y

F := FIJO G  donde  FIJO g  := ( r donde r = g r ) = g (FIJO g )

de modo que  FIX G = G (FIX G) = (λ n .(1, si n = 0; de lo contrario n × ((FIX G) ( n −1))))

Dado un término lambda cuyo primer argumento representa una llamada recursiva (por ejemplo, G aquí), el combinador de punto fijo FIX devolverá una expresión lambda autorreplicante que representa la función recursiva (aquí, F ). La función no necesita pasarse explícitamente a sí misma en ningún momento, ya que la autorreplicación se organiza de antemano, cuando se crea, para que se realice cada vez que se la llama. Por lo tanto, la expresión lambda original (FIX G) se vuelve a crear dentro de sí misma, en el punto de llamada, logrando la autorreferencia .

De hecho, existen muchas definiciones posibles para este operador FIX , siendo la más simple de ellas:

Y  := λ g .(λ x . g ( x x )) (λ x . g ( x x ))

En el cálculo lambda, Y g   es un punto fijo de g , ya que se expande a:

Y g

(λ h .(λ x . h ( x x )) (λ x . h ( x x ))) g

(λ x . g ( x x )) (λ x . g ( x x ))

g ((λ x . g ( x x )) (λ x . g ( x x )))

g ( Y g )

Ahora, para realizar nuestra llamada recursiva a la función factorial, simplemente llamaríamos a ( Y G) n , donde n es el número del que estamos calculando el factorial. Dado n = 4, por ejemplo, esto da:

( YG ) 4

G ( Y G) 4

(λ r .λ n .(1, si n = 0; de lo contrario n × ( r ( n −1)))) ( Y G) 4

(λ n .(1, si n = 0; de lo contrario n × (( Y G) ( n −1)))) 4

1, si 4 = 0; de lo contrario 4 × (( Y G) (4−1))

4 × (G ( Y G) (4−1))

4 × ((λ n .(1, si n = 0; de lo contrario n × (( Y G) ( n −1)))) (4−1))

4 × (1, si 3 = 0; de lo contrario 3 × (( Y G) (3−1)))

4 × (3 × (G ( Y G) (3−1)))

4 × (3 × ((λ n .(1, si n = 0; de lo contrario n × (( Y G) ( n −1)))) (3−1)))

4 × (3 × (1, si 2 = 0; de lo contrario 2 × (( Y G) (2−1))))

4 × (3 × (2 × (G ( Y G) (2−1))))

4 × (3 × (2 × ((λ n .(1, si n = 0; de lo contrario n × (( Y G) ( n −1)))) (2−1))))

4 × (3 × (2 × (1, si 1 = 0; de lo contrario 1 × (( Y G) (1−1)))))

4 × (3 × (2 × (1 × (G ( Y G) (1−1)))))

4 × (3 × (2 × (1 × ((λ n .(1, si n = 0; de lo contrario n × (( Y G) ( n −1)))) (1−1)))))

4 × (3 × (2 × (1 × (1, si 0 = 0; de lo contrario 0 × (( Y G) (0−1))))))

4 × (3 × (2 × (1 × (1))))

24

Toda función definida recursivamente puede verse como un punto fijo de alguna función definida adecuadamente que cierra la llamada recursiva con un argumento adicional y, por lo tanto, utilizando Y , toda función definida recursivamente puede expresarse como una expresión lambda. En particular, ahora podemos definir claramente los predicados de resta, multiplicación y comparación de números naturales de forma recursiva.

Ciertos términos tienen nombres comúnmente aceptados: ^{[27] [28] [29]}

yo  := λ x . x

S  := λ x .λ y .λ z . x z ( y z )

K  := λ x . λ y . x

B  := λ x .λ y .λ z . x ( y z )

C  := λ x . λ y . λ z . x z y

W  := λ x . λ y . x y y

ω o Δ o U  := λ x . x x

Ω  := ω ω

I es la función identidad. SK y BCKW forman sistemas completos de cálculo combinatorio que pueden expresar cualquier término lambda (consulte la siguiente sección). Ω es UU , el término más pequeño que no tiene forma normal. YI es otro término de este tipo. Y es estándar y se definió anteriormente, y también se puede definir como Y = BU(CBU) , de modo que Y g=g( Y g) . VERDADERO y FALSO definidos anteriormente se abrevian comúnmente como T y F.

Si N es un término lambda sin abstracción, pero que posiblemente contenga constantes nombradas ( combinadores ), entonces existe un término lambda T ( x , N ) que es equivalente a λ x . N pero carece de abstracción (excepto como parte de las constantes nombradas, si estas se consideran no atómicas). Esto también puede verse como variables anonimizadas, ya que T ( x , N ) elimina todas las ocurrencias de x de N , mientras que todavía permite que los valores de los argumentos se sustituyan en las posiciones donde N contiene una x . La función de conversión T puede definirse por:

T ( x , x ):= yo

T ( x , N ) := K N si x no es libre en N .

T ( x , MN ) : = ST ( x , M ) T ( x , N )

En cualquier caso, un término de la forma T ( x , N ) P se puede reducir haciendo que el combinador inicial I , K o S tome el argumento P , tal como lo haría la β-reducción de (λ x . N ) P . I devuelve ese argumento. K descarta el argumento, tal como lo haría (λ x . N ) si x no tiene ninguna ocurrencia libre en N . S pasa el argumento a ambos subtérminos de la aplicación y luego aplica el resultado del primero al resultado del segundo.

Los combinadores B y C son similares a S , pero pasan el argumento a un solo subtérmino de una aplicación ( B al subtérmino "argumento" y C al subtérmino "función"), ahorrando así un K posterior si no hay ocurrencia de x en un subtérmino. En comparación con B y C , el combinador S en realidad combina dos funcionalidades: reorganizar argumentos y duplicar un argumento para que pueda usarse en dos lugares. El combinador W solo hace esto último, lo que produce el sistema B, C, K, W como una alternativa al cálculo del combinador SKI .

Un cálculo lambda tipado es un formalismo tipado que utiliza el símbolo lambda ( ) para denotar la abstracción de una función anónima. En este contexto, los tipos son normalmente objetos de naturaleza sintáctica que se asignan a términos lambda; la naturaleza exacta de un tipo depende del cálculo considerado (véase Tipos de cálculos lambda tipados ). Desde cierto punto de vista, los cálculos lambda tipados pueden verse como refinamientos del cálculo lambda no tipado, pero desde otro punto de vista, también pueden considerarse la teoría más fundamental y el cálculo lambda no tipado un caso especial con un solo tipo. ^[30]${\displaystyle \lambda }$

Los cálculos lambda tipados son lenguajes de programación fundamentales y son la base de los lenguajes de programación funcional tipados como ML y Haskell y, de forma más indirecta, de los lenguajes de programación imperativos tipados . Los cálculos lambda tipados desempeñan un papel importante en el diseño de sistemas de tipos para lenguajes de programación; aquí la tipabilidad suele capturar propiedades deseables del programa, por ejemplo, el programa no provocará una violación de acceso a memoria.

Los cálculos lambda tipados están estrechamente relacionados con la lógica matemática y la teoría de la prueba a través del isomorfismo de Curry-Howard y pueden considerarse como el lenguaje interno de las clases de categorías , por ejemplo, el cálculo lambda tipado simplemente es el lenguaje de las categorías cartesianas cerradas (CCC).

El que un término sea normalizador o no, y el trabajo que se necesita hacer para normalizarlo si lo es, depende en gran medida de la estrategia de reducción utilizada. Las estrategias de reducción de cálculo lambda más comunes incluyen: ^{[31] [32] [33]}

Orden normal

El redex más externo a la izquierda se reduce primero. Es decir, siempre que sea posible, los argumentos se sustituyen en el cuerpo de una abstracción antes de que se reduzcan. Si un término tiene una forma beta-normal, la reducción de orden normal siempre alcanzará esa forma normal.

Orden de aplicación

La redex más interna y más a la izquierda se reduce primero. Como consecuencia, los argumentos de una función siempre se reducen antes de que se los sustituya en la función. A diferencia de la reducción de orden normal, la reducción de orden aplicativo puede no encontrar la forma beta-normal de una expresión, incluso si dicha forma normal existe. Por ejemplo, el término se reduce a sí mismo por orden aplicativo, mientras que el orden normal lo reduce a su forma beta-normal .${\displaystyle (\;\lambda x.y\;\;(\lambda z.(zz)\;\lambda z.(zz))\;)}$${\displaystyle y}$

β-reducciones completas

Cualquier redex puede reducirse en cualquier momento. Esto significa, en esencia, que no existe ninguna estrategia de reducción en particular; en lo que respecta a la reducibilidad, "no hay nada que hacer".

Las estrategias de reducción débil no reducen bajo abstracciones lambda:

Llamada por valor

Similar al orden aplicativo, pero no se realizan reducciones dentro de las abstracciones. Esto es similar al orden de evaluación de lenguajes estrictos como C: los argumentos de una función se evalúan antes de llamar a la función, y los cuerpos de las funciones no se evalúan ni siquiera parcialmente hasta que se sustituyen los argumentos.

Llamar por nombre

Como el orden normal, pero no se realizan reducciones dentro de las abstracciones. Por ejemplo, λ x .(λ y . y ) x está en forma normal según esta estrategia, aunque contiene el redex (λ y . y ) x .

Las estrategias de compartición reducen los cálculos que son "iguales" en paralelo:

Reducción óptima

Como orden normal, pero los cálculos que tienen la misma etiqueta se reducen simultáneamente.

Llamar por necesidad

Como se llama por nombre (por lo tanto, es débil), pero las aplicaciones de función que duplicarían términos en su lugar nombrarían el argumento. El argumento se puede evaluar "cuando sea necesario", momento en el que la vinculación del nombre se actualiza con el valor reducido. Esto puede ahorrar tiempo en comparación con la evaluación de órdenes normal.

No existe ningún algoritmo que tome como entrada dos expresiones lambda cualesquiera y dé como salida VERDADERO o FALSO dependiendo de si una expresión se reduce a la otra. ^[13] Más precisamente, ninguna función computable puede decidir la cuestión. Este fue históricamente el primer problema para el que se pudo demostrar la indecidibilidad. Como es habitual en este tipo de pruebas, computable significa computable mediante cualquier modelo de cálculo que sea Turing completo . De hecho, la computabilidad se puede definir a través del cálculo lambda: una función F : N → N de números naturales es una función computable si y solo si existe una expresión lambda f tal que para cada par de x , y en N , F ( x )= y si y solo si f x  = _β y , donde x e y son los numerales de Church correspondientes a x e y , respectivamente y = _β que significa equivalencia con β-reducción. Véase la tesis de Church-Turing para otros enfoques para definir la computabilidad y su equivalencia.  

La prueba de incomputabilidad de Church reduce primero el problema a determinar si una expresión lambda dada tiene una forma normal . Luego supone que este predicado es computable y, por lo tanto, puede expresarse en cálculo lambda. Basándose en trabajos anteriores de Kleene y construyendo una numeración de Gödel para expresiones lambda, construye una expresión lambda e que sigue de cerca la prueba del primer teorema de incompletitud de Gödel . Si e se aplica a su propio número de Gödel, resulta una contradicción.

La noción de complejidad computacional para el cálculo lambda es un poco complicada, porque el costo de una β-reducción puede variar dependiendo de cómo se implemente. ^[34] Para ser precisos, uno debe encontrar de alguna manera la ubicación de todas las ocurrencias de la variable ligada V en la expresión E , lo que implica un costo de tiempo, o uno debe realizar un seguimiento de las ubicaciones de las variables libres de alguna manera, lo que implica un costo de espacio. Una búsqueda ingenua de las ubicaciones de V en E es O ( n ) en la longitud n de E . Las cadenas de directores fueron un enfoque temprano que intercambió este costo de tiempo por un uso de espacio cuadrático. ^[35] De manera más general, esto ha llevado al estudio de sistemas que utilizan la sustitución explícita .

En 2014, se demostró que el número de pasos de β-reducción tomados por la reducción de orden normal para reducir un término es un modelo de costo de tiempo razonable , es decir, la reducción se puede simular en una máquina de Turing en un tiempo polinomialmente proporcional al número de pasos. ^[36] Este era un problema abierto desde hace mucho tiempo, debido a la explosión de tamaño , la existencia de términos lambda que crecen exponencialmente en tamaño para cada β-reducción. El resultado soluciona esto trabajando con una representación compartida compacta. El resultado deja claro que la cantidad de espacio necesario para evaluar un término lambda no es proporcional al tamaño del término durante la reducción. Actualmente no se sabe cuál sería una buena medida de la complejidad espacial. ^[37]

Un modelo irrazonable no significa necesariamente ineficiente. La reducción óptima reduce todos los cálculos con la misma etiqueta en un paso, evitando el trabajo duplicado, pero el número de pasos de β-reducción paralelos para reducir un término dado a la forma normal es aproximadamente lineal en el tamaño del término. Esto es demasiado pequeño para ser una medida de costo razonable, ya que cualquier máquina de Turing puede codificarse en el cálculo lambda en un tamaño linealmente proporcional al tamaño de la máquina de Turing. El verdadero costo de reducir los términos lambda no se debe a la β-reducción per se, sino más bien al manejo de la duplicación de redexes durante la β-reducción. ^[38] No se sabe si las implementaciones de reducción óptima son razonables cuando se miden con respecto a un modelo de costo razonable, como el número de pasos más a la izquierda-más a la forma normal, pero se ha demostrado para fragmentos del cálculo lambda que el algoritmo de reducción óptima es eficiente y tiene como máximo una sobrecarga cuadrática en comparación con el más a la izquierda-más a la externa. ^[37] Además, la implementación del prototipo BOHM de reducción óptima superó tanto a Caml Light como a Haskell en términos lambda puros. ^[38]

Como se señala en el artículo de Peter Landin de 1965 "Una correspondencia entre ALGOL 60 y la notación Lambda de Church", ^{[39] los lenguajes} de programación procedimental secuencial pueden entenderse en términos del cálculo lambda, que proporciona los mecanismos básicos para la abstracción procedimental y la aplicación de procedimientos (subprogramas).

Por ejemplo, en Python la función "cuadrado" se puede expresar como una expresión lambda de la siguiente manera:

( lambda  x :  x ** 2 )

El ejemplo anterior es una expresión que se evalúa como una función de primera clase. El símbolo lambdacrea una función anónima, dada una lista de nombres de parámetros x(en este caso, solo un argumento) y una expresión que se evalúa como el cuerpo de la función. x**2Las funciones anónimas a veces se denominan expresiones lambda.

Por ejemplo, Pascal y muchos otros lenguajes imperativos han admitido durante mucho tiempo el paso de subprogramas como argumentos a otros subprogramas a través del mecanismo de punteros de función . Sin embargo, los punteros de función no son una condición suficiente para que las funciones sean tipos de datos de primera clase , porque una función es un tipo de datos de primera clase si y solo si se pueden crear nuevas instancias de la función en tiempo de ejecución. Y esta creación de funciones en tiempo de ejecución es compatible con Smalltalk , JavaScript y Wolfram Language , y más recientemente con Scala , Eiffel ("agentes"), C# ("delegados") y C++11 , entre otros.

La propiedad de Church-Rosser del cálculo lambda significa que la evaluación (β-reducción) se puede llevar a cabo en cualquier orden , incluso en paralelo. Esto significa que son relevantes varias estrategias de evaluación no deterministas . Sin embargo, el cálculo lambda no ofrece ningún constructo explícito para el paralelismo . Se pueden agregar constructos como Futuros al cálculo lambda. Se han desarrollado otros cálculos de procesos para describir la comunicación y la concurrencia.

El hecho de que los términos del cálculo lambda actúen como funciones sobre otros términos del cálculo lambda, e incluso sobre sí mismos, llevó a plantear preguntas sobre la semántica del cálculo lambda. ¿Podría asignarse un significado sensato a los términos del cálculo lambda? La semántica natural era encontrar un conjunto D isomorfo al espacio de funciones D → D , de funciones sobre sí mismo. Sin embargo, no puede existir un D no trivial, por restricciones de cardinalidad porque el conjunto de todas las funciones desde D hasta D tiene mayor cardinalidad que D , a menos que D sea un conjunto singleton .

En la década de 1970, Dana Scott demostró que si solo se consideraban funciones continuas , se podía encontrar un conjunto o dominio D con la propiedad requerida, proporcionando así un modelo para el cálculo lambda. ^[40]

Este trabajo también formó la base para la semántica denotacional de los lenguajes de programación.

Estas extensiones están en el cubo lambda :

• Cálculo lambda tipado – Cálculo lambda con variables (y funciones) tipadas
• Sistema F – Un cálculo lambda tipado con variables de tipo
• Cálculo de construcciones : un cálculo lambda tipado con tipos como valores de primera clase

Estos sistemas formales son extensiones del cálculo lambda que no están en el cubo lambda:

• Cálculo lambda binario : una versión del cálculo lambda con E/S binaria, una codificación binaria de términos y una máquina universal designada.
• Cálculo lambda-mu : una extensión del cálculo lambda para tratar la lógica clásica

Estos sistemas formales son variaciones del cálculo lambda:

• Cálculo kappa : un análogo de primer orden del cálculo lambda

Estos sistemas formales están relacionados con el cálculo lambda:

• Lógica combinatoria : una notación para lógica matemática sin variables
• Cálculo combinatorio SKI : un sistema computacional basado en los combinadores S , K e I , equivalente al cálculo lambda, pero reducible sin sustituciones de variables

• Abelson, Harold y Gerald Jay Sussman. Estructura e interpretación de programas informáticos . The MIT Press . ISBN  0-262-51087-1 .
• Barendregt, Hendrik Pieter Introducción al cálculo Lambda.
• Barendregt, Hendrik Pieter, El impacto del cálculo lambda en la lógica y la informática. The Bulletin of Symbolic Logic, volumen 3, número 2, junio de 1997.
• Barendregt, Hendrik Pieter, El cálculo lambda sin tipos , pp. 1091-1132 del Manual de lógica matemática , Holanda Septentrional (1977) ISBN 0-7204-2285-X 
• Cardone, Felice y Hindley, J. Roger, 2006. Historia del cálculo lambda y la lógica combinatoria Archivado el 6 de mayo de 2021 en Wayback Machine . En Gabbay y Woods (eds.), Handbook of the History of Logic , vol. 5. Elsevier.
• Church, Alonzo, Un problema insoluble de teoría de números elementales , American Journal of Mathematics , 58 (1936), págs. 345–363. Este artículo contiene la prueba de que la equivalencia de expresiones lambda en general no es decidible.
• Church, Alonzo (1941). Los cálculos de la conversión lambda. Princeton: Princeton University Press . Consultado el 14 de abril de 2020 .( ISBN 978-0-691-08394-0 ) 
• Frink Jr., Orrin (1944). "Reseña: Los cálculos de conversión lambda de Alonzo Church" (PDF) . Bull. Amer. Math. Soc . 50 (3): 169–172. doi : 10.1090/s0002-9904-1944-08090-7 .
• Kleene, Stephen, A theory of positive entirets in formal logic , American Journal of Mathematics , 57 (1935), pp. 153–173 y 219–244. Contiene las definiciones de cálculo lambda de varias funciones conocidas.
• Landin, Peter , A Correspondence Between ALGOL 60 and Church's Lambda-Notation , Communications of the ACM , vol. 8, no. 2 (1965), páginas 89-101. Disponible en el sitio de la ACM. Un artículo clásico que destaca la importancia del cálculo lambda como base para los lenguajes de programación.
• Larson, Jim, Introducción al cálculo lambda y Scheme. Una introducción sencilla para programadores.
• Michaelson, Greg (10 de abril de 2013). Introducción a la programación funcional mediante el cálculo lambda . Courier Corporation. ISBN 978-0-486-28029-5.^[41]
• Schalk, A. y Simmons, H. (2005) Introducción a los cálculos λ y a la aritmética con una buena selección de ejercicios . Notas para un curso de maestría en lógica matemática en la Universidad de Manchester.
• de Queiroz, Ruy JGB (2008). "Sobre reglas de reducción, significado como uso y semántica de teoría de la prueba". Studia Logica . 90 (2): 211–247. doi :10.1007/s11225-008-9150-5. S2CID  11321602.Un artículo que proporciona una base formal a la idea de que "el significado es uso" que, incluso si se basa en pruebas, es diferente de la semántica de teoría de pruebas como en la tradición de Dummett-Prawitz, ya que toma la reducción como las reglas que dan significado.
• Hankin, Chris, Introducción a los cálculos lambda para científicos informáticos, ISBN 0954300653 

Monografías/libros de texto para estudiantes de posgrado

• Sørensen, Morten Heine y Urzyczyn, Paweł (2006), Lectures on the Curry–Howard isomorphism , Elsevier, ISBN 0-444-52077-5 es una monografía reciente que cubre los temas principales del cálculo lambda desde la variedad libre de tipos hasta la mayoría de los cálculos lambda tipados , incluidos desarrollos más recientes como los sistemas de tipos puros y el cubo lambda . No cubre las extensiones de subtipificación . 
• Pierce, Benjamin (2002), Tipos y lenguajes de programación , MIT Press, ISBN 0-262-16209-1Cubre los cálculos lambda desde una perspectiva práctica del sistema de tipos; algunos temas como los tipos dependientes solo se mencionan, pero la subtipificación es un tema importante.

Documentos

• Una breve introducción al cálculo lambda ( PDF ) de Achim Jung
• Cronología del cálculo lambda ( PDF ) de Dana Scott
• Un tutorial de introducción al cálculo lambda ( PDF ) de Raúl Rojas
• Notas de clase sobre el cálculo lambda ( PDF ) de Peter Selinger
• Cálculo lambda gráfico de Marius Buliga
• Cálculo lambda como modelo de flujo de trabajo por Peter Kelly, Paul Coddington y Andrew Wendelborn; menciona la reducción de gráficos como un medio común para evaluar expresiones lambda y analiza la aplicabilidad del cálculo lambda para la computación distribuida (debido a la propiedad de Church-Rosser , que permite la reducción de gráficos paralelos para expresiones lambda).

Algunas partes de este artículo se basan en material de FOLDOC , utilizado con permiso .

Wikimedia Commons alberga una categoría multimedia sobre Cálculo lambda .

• Graham Hutton, Cálculo Lambda, un breve vídeo de Computerphile (12 minutos) sobre el Cálculo Lambda
• Helmut Brandl, Introducción paso a paso al cálculo lambda
• "Cálculo lambda", Enciclopedia de matemáticas , EMS Press , 2001 [1994]
• David C. Keenan, Disecar un ruiseñor: una notación gráfica para el cálculo lambda con reducción animada
• L. Allison, Algunos ejemplos ejecutables de cálculo λ
• Georg P. Loczewski, El cálculo lambda y A++
• Bret Victor, Huevos de caimán: un juego de rompecabezas basado en el cálculo lambda
• Cálculo Lambda Archivado el 14 de octubre de 2012 en Wayback Machine en el sitio web de Safalra Archivado el 2 de mayo de 2021 en Wayback Machine
• LCI Lambda Interpreter: un intérprete de cálculo puro simple pero potente
• Enlaces sobre cálculo lambda en Lambda-the-Ultimate
• Mike Thyer, Lambda Animator, una aplicación gráfica de Java que demuestra estrategias de reducción alternativas.
• Implementación del cálculo Lambda mediante plantillas C++
• Shane Steinert-Threlkeld, "Lambda Calculi", Enciclopedia de Filosofía de Internet
• Anton Salikhmetov, Cálculo macro lambda