Cálculo lambda

En lógica matemática , el cálculo lambda (también escrito como cálculo λ ) es un sistema formal para expresar la computación basado en la abstracción de funciones y su aplicación mediante la vinculación y sustitución de variables . El cálculo lambda sin tipos, tema de este artículo, es una máquina universal , es decir, un modelo de computación que puede utilizarse 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 lógicamente consistente y la documentó en 1940.

El cálculo lambda consiste en un lenguaje de términos lambda , que se definen mediante una sintaxis formal, y un conjunto de reglas de transformación para manipular esos términos. En BNF , la sintaxis es${\displaystyle e::=x\mid \lambda x.e\mid e\,e,}$donde las variables x , y , z abarcan un conjunto infinito de nombres. Los términos M , N , t , s , e , f abarcan todos los términos lambda. Esto corresponde a la siguiente definición inductiva :

• Una variable x es un término lambda válido.
• Una abstracción es un término lambda.${\displaystyle (\lambda x.t)}$donde t es un término lambda, denominado cuerpo de la abstracción , y x es la variable de parámetro de la abstracción ,
• Una aplicación es un término lambda.${\displaystyle (t\,s)}$donde t y s son términos lambda.

Un término lambda es sintácticamente válido si se puede obtener mediante la aplicación repetida de estas tres reglas. Para mayor comodidad, a menudo se pueden omitir los paréntesis al escribir un término lambda; consulte la definición de cálculo lambda, sección  Notación, para obtener más detalles.

Dentro de los términos lambda, cualquier ocurrencia de una variable que no sea un parámetro de algún λ que la encierre se dice que es libre . Cualquier ocurrencia libre de${\displaystyle x}$en un término${\displaystyle M}$está limitado en${\displaystyle \lambda x.M}$. Cualquier ocurrencia libre de cualquier otra variable dentro${\displaystyle M}$permanece libre en${\displaystyle \lambda x.M}$.

Por ejemplo, en el término${\displaystyle x\,y}$, ambos${\displaystyle x}$y${\displaystyle y}$ocurren gratis. En${\displaystyle (\lambda x.x\,y)}$,${\displaystyle y}$es gratis, pero${\displaystyle x}$en el cuerpo (es decir, después del punto) no es libre y se dice que está ligado (al parámetro). Mientras que${\displaystyle y}$es gratis en${\displaystyle (\lambda x.x\,y)}$, está encuadernado en${\displaystyle (\lambda y.\lambda x.x\,y)}$Hay dos ocurrencias de${\displaystyle x}$en${\displaystyle (\lambda y.(\lambda x.x\,y)\,x)}$– uno está atado y el otro es libre.

FV(M) es el conjunto de variables libres de M , es decir, aquellas variables que aparecen libres en M al menos una vez. Se puede definir inductivamente de la siguiente manera:

• ${\displaystyle \operatorname {FV} (x)=\{x\}}$
• ${\displaystyle \operatorname {FV} (M_{1}M_{2})=\operatorname {FV} (M_{1})\cup \operatorname {FV} (M_{2})}$
• ${\displaystyle \operatorname {FV} (\lambda x.M)=\operatorname {FV} (M)\backslash \{x\}}$

La notación${\displaystyle M[x:=N]}$denota una sustitución que evita la captura : sustituir N por cada ocurrencia libre de x en M , evitando la captura de variables. ^{[ a ]} ​​Esta operación se define inductivamente de la siguiente manera:

• ${\displaystyle x[x:=N]=N}$;${\displaystyle y[x:=N]=y}$si${\displaystyle y\neq x}$.
• ${\displaystyle (M_{1}M_{2})[x:=N]=(M_{1}[x:=N])(M_{2}[x:=N])}$.
• ${\displaystyle (\lambda y.M)[x:=N]}$tiene tres casos:
  • Si${\displaystyle y=x}$, se convierte en${\displaystyle \lambda x.M}$(${\displaystyle x}$está vinculado; sin cambios).
  • Si${\displaystyle y\notin FV(N)}$, se convierte en${\displaystyle \lambda y.(M[x:=N])}$.
  • Si${\displaystyle y\in FV(N)}$, primer α-cambio de nombre${\displaystyle \lambda y.M}$a${\displaystyle \lambda y'.M[y:=y']}$con${\displaystyle y'}$fresco para evitar colisiones de nombres , luego continúe como se indicó anteriormente. Se convierte en${\displaystyle \lambda y'.M[y:=y'][x:=N]}$con${\displaystyle y'\notin \operatorname {FV} (M)\cup \operatorname {FV} (N)}$.

Existen varias nociones de "equivalencia" y "reducción" que permiten reducir términos lambda a términos lambda equivalentes. ^{[ 3 ]}

• La conversión α captura la intuición de que la elección particular de una variable ligada, en una abstracción, no suele importar. Si${\displaystyle y\notin FV(M)}$, entonces los términos${\displaystyle \lambda x.M}$y${\displaystyle \lambda y.M[x:=y]}$se consideran alfa-equivalentes , escritos${\displaystyle \lambda x.M\equiv _{\alpha }\lambda y.M[x:=y]}$. La relación de equivalencia es la relación de congruencia más pequeña sobre términos lambda generada por esta regla. Por ejemplo,${\displaystyle \lambda x.x}$y${\displaystyle \lambda y.y}$son términos lambda alfa-equivalentes.
• La regla de β-reducción establece que una β-redex, una aplicación de la forma${\displaystyle (\lambda x.t)s}$, se reduce al término${\displaystyle t[x:=s]}$. ^{[ b ]} Por ejemplo, para cada${\displaystyle s}$,${\displaystyle (\lambda x.x)s\to x[x:=s]=s}$Esto demuestra que${\displaystyle \lambda x.x}$realmente es la identidad. De manera similar,${\displaystyle (\lambda x.y)s\to y[x:=s]=y}$, lo cual demuestra que${\displaystyle \lambda x.y}$es una función constante.
• La conversión η expresa extensionalidad y convierte entre${\displaystyle \lambda x.fx}$y${\displaystyle f}$cuando sea${\displaystyle x}$no parece libre en${\displaystyle f}$. A menudo se omite en muchos tratamientos del cálculo lambda.

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 que expresa la sustitución de N por x en M . La expresión a la que se reduce un redex se llama su reducto ; el reducto de (λ x . M ) N es M [ x  := N ].

El cálculo lambda es Turing completo , es decir, es un modelo universal de computación que puede usarse para simular cualquier máquina de Turing . ^{[ 4 ]} Su homónimo, la letra griega lambda (λ), se usa 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 no tipado o tipado . En el cálculo lambda tipado, las funciones solo se pueden aplicar si son capaces de aceptar el "tipo" de datos de entrada. Los cálculos lambda tipados son estrictamente 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 pueden expresar menos que el cálculo no tipado. Por otro lado, se pueden demostrar más cosas con cálculos lambda tipados. Por ejemplo, en el cálculo lambda simplemente tipado , es un teorema que toda estrategia de evaluación termina para cada término lambda simplemente tipado, ^{[ 5 ]} mientras que la evaluación de términos lambda no tipados no tiene por qué terminar (véase más adelante ). Una razón por la que existen muchos cálculos lambda tipados diferentes ha sido el deseo de hacer más (de lo que puede hacer el cálculo no tipado) sin renunciar a la capacidad 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 , ^{[ 6 ]} la lingüística , ^{[ 7 ] [ 8 ]} y la informática . ^{[ 9 ] [ 10 ]} 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 . ^{[ 11 ]}

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 . ^{[ 12 ] [ c ]} Se demostró que el sistema original era lógicamente inconsistente en 1935 cuando Stephen Kleene y JB Rosser desarrollaron la paradoja de Kleene-Rosser . ^{[ 13 ] [ 14 ]}

Posteriormente, en 1936, Church aisló y publicó únicamente la parte relevante para la computación, lo que ahora se conoce como el cálculo lambda sin tipado. ^{[ 15 ]} En 1940, también introdujo un sistema computacionalmente más débil, pero lógicamente consistente, conocido como el cálculo lambda simplemente tipado . ^{[ 16 ]}

Hasta la década de 1960, cuando se aclaró su relación con los lenguajes de programación, el cálculo lambda era solo 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 gozar de un lugar respetable tanto en la lingüística ^{[ 17 ]} como en la informática. ^{[ 18 ]}

Las funciones computables son un concepto fundamental en informática y matemáticas. El cálculo lambda proporciona una semántica sencilla para la computación, útil para el estudio formal de sus propiedades. El cálculo lambda incorpora dos simplificaciones que hacen que su semántica sea simple. La primera simplificación es que el cálculo lambda trata las funciones "anónimamente"; no les da nombres explícitos. Por ejemplo, la función

${\displaystyle \operatorname {square\_sum} (x,y)=x^{2}+y^{2}}$

puede reescribirse de 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${\textstyle x^{2}+y^{2}}$"). ^{[ d ]} De manera similar, la función

${\displaystyle \operatorname {id} (x)=x}$

puede reescribirse de forma anónima como

${\displaystyle x\mapsto x}$

donde la entrada simplemente se mapea 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,${\textstyle \operatorname {square\_sum} }$La función se puede reelaborar 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,

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

puede ser reelaborado en

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

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

Aplicación funcional de la${\textstyle \operatorname {square\_sum} }$función para los argumentos (5, 2), produce inmediatamente

${\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 currificada 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${\displaystyle x}$se ha utilizado con${\displaystyle 5}$en la expresión interna. Esto es como una β-reducción.

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

${\textstyle =29}$

para llegar al mismo resultado.

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${\displaystyle \lambda x.x}$representa la función identidad ,${\displaystyle x\mapsto x}$. Más,${\displaystyle \lambda x.y}$representa la función constante${\displaystyle x\mapsto y}$, la función que siempre devuelve${\displaystyle y}$, independientemente de la entrada. Como ejemplo de una función que opera sobre funciones, la composición de funciones se puede definir como${\displaystyle \lambda f.\lambda g.\lambda x.(f(gx))}$.

Se puede demostrar que la β-reducción es confluente hasta la α-conversión (es decir, cuando dos formas normales se consideran iguales si es posible α-convertir una en la otra). Según el teorema de Church-Rosser , cualquier secuencia particular de pasos de reducción que comience desde un término lambda dado que finalmente termine producirá la misma β-forma normal . Sin embargo, el cálculo lambda sin tipo bajo la β-reducción como regla de reescritura no es ni fuertemente normalizador ni débilmente normalizador ; hay términos sin forma normal como Ω .

Considerando los términos individualmente, tanto los términos fuertemente normalizadores como los débilmente normalizadores poseen una forma normal única. Para los términos fuertemente normalizadores, cualquier estrategia de reducción garantiza la obtención de la forma normal, mientras que para los términos débilmente normalizadores, algunas estrategias de reducción pueden no lograr encontrarla.

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

Existe un considerable conjunto de modismos de programación para el cálculo lambda. Muchos de ellos se desarrollaron originalmente en el contexto del uso del cálculo lambda como base para la semántica de los lenguajes de programación , utilizándolo efectivamente como un lenguaje de programación de bajo nivel . Dado 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 ajenas.

Un cálculo lambda tipado es un formalismo tipado que utiliza el símbolo lambda (${\displaystyle \lambda }$) para denotar la abstracción de función anónima. En este contexto, los tipos suelen ser 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. ^{[ 29 ]}

Los cálculos lambda tipados son fundamentales para los lenguajes de programación y constituyen la base de lenguajes de programación funcional tipados como ML y Haskell, y, de forma más indirecta, de 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; en este caso, la tipabilidad suele reflejar propiedades deseables del programa, como por ejemplo, que el programa no provoque una violación de acceso a la memoria.

Los cálculos lambda tipados están estrechamente relacionados con la lógica matemática y la teoría de la demostración 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 una categoría cartesiana cerrada (CCC). ^{[ 30 ]}

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

Orden normal

El redex externo más 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 su reducción. Si un término tiene una forma beta-normal, la reducción en orden normal siempre alcanzará dicha forma.

Orden de aplicación

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

Reducciones β completas

Cualquier redex puede reducirse en cualquier momento. Esto significa, esencialmente, la ausencia de una estrategia de reducción específica: en lo que respecta a la reducibilidad, "todo vale".

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

Llamar por valor

Similar al orden aplicativo, pero sin 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 llamarla, y el cuerpo de la función no se evalúa ni siquiera parcialmente hasta que se sustituyen los argumentos.

Llamar por nombre

Como en 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 en el orden habitual, pero los cálculos que tienen la misma etiqueta se reducen simultáneamente.

Llamar según sea necesario

Como se denomina por nombre (y por lo tanto débil), las aplicaciones de función que duplicarían términos en su lugar nombran el argumento. El argumento puede evaluarse "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 en orden normal.

No existe ningún algoritmo que tome como entrada dos expresiones lambda cualesquiera y produzca VERDADERO o FALSO dependiendo de si una expresión se reduce a la otra. ^{[ 15 ]} Más precisamente, ninguna función computable puede decidir la cuestión. Históricamente, este fue el primer problema para el que se pudo demostrar la indecidibilidad. Como es habitual en este tipo de demostraciones, computable significa computable por cualquier modelo de computación que sea Turing completo . De hecho, la computabilidad puede definirse 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 = _β significa equivalencia con β-reducción. Véase la tesis de Church-Turing para otros enfoques para definir la computabilidad y su equivalencia.  

La demostración de Church sobre la incomputabilidad reduce primero el problema a determinar si una expresión lambda dada tiene una forma normal . Luego, asume que este predicado es computable y, por lo tanto, puede expresarse en cálculo lambda. Partiendo de 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 demostración del primer teorema de incompletitud de Gödel . Si se aplica e a su propio número de Gödel, se produce 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 hacer un seguimiento de las ubicaciones de las variables libres de alguna manera, lo que implica un costo de espacio. Una búsqueda ingenua para las ubicaciones de V en E es O ( n ) en la longitud n de E . Las cadenas directoras fueron un enfoque temprano que intercambió este costo de tiempo por un uso de espacio cuadrático. ^{[ 35 ]} Más generalmente esto ha llevado al estudio de sistemas que usan sustitución explícita .

En 2014, se demostró que el número de pasos de β-reducción necesarios para reducir un término mediante una reducción de orden normal constituye un modelo de coste temporal razonable ; es decir, la reducción puede simularse en una máquina de Turing en un tiempo polinomialmente proporcional al número de pasos. ^{[ 36 ]} Este era un problema abierto de larga data, 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 sortea este problema trabajando con una representación compartida compacta. El resultado deja claro que la cantidad de espacio necesaria para evaluar un término lambda no es proporcional al tamaño del término durante la reducción. Actualmente se desconoce 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 términos lambda no se debe a la β-reducción en sí, 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 leftmost-outmost 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 leftmost-outmost. ^{[ 37 ]} Además, la implementación prototipo de reducción óptima de BOHM superó a Caml Light y Haskell en términos de lambda pura. ^{[ 38 ]}

Como lo señaló Peter Landin en su artículo de 1965 " Una correspondencia entre ALGOL 60 y la notación Lambda de Church ", ^{[ 39 ]} los lenguajes de programación procedimentales secuenciales 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).

( lambda x : x ** 2 )

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, generó interrogantes sobre la semántica del cálculo lambda. ¿Se podría asignar un significado sensato a los términos del cálculo lambda? La semántica natural consistía en 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 de este tipo , debido a restricciones de cardinalidad , ya que el conjunto de todas las funciones de D a D tiene mayor cardinalidad que D , a menos que D sea un conjunto unitario .

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 sentó las bases de la semántica denotacional de los lenguajes de programación.

Estas extensiones se encuentran 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 entrada/salida (E/S) binaria, una codificación binaria de los términos y una máquina universal designada.
• Cálculo lambda-mu : una extensión del cálculo lambda para el tratamiento de 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 la 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.

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

• 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 . Boletín de lógica simbólica, volumen 3, número 2, junio de 1997.
• Barendregt, Hendrik Pieter, El cálculo lambda sin tipos, págs. 1091-1132 del Manual de lógica matemática , North-Holland (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.), Manual de historia de la lógica , vol. 5. Elsevier.
• Church, Alonzo, Un problema irresoluble de la teoría elemental de números , American Journal of Mathematics , 58 (1936), pp.  345–363. Este artículo contiene la demostración de que la equivalencia de expresiones lambda no es, en general, decidible.
• Church, Alonzo (1941). Los cálculos de la conversión lambda . Princeton: Princeton University Press . Recuperado el 14 de abril de 2020 .( ISBN 978-0-691-08394-0)
• Frink Jr., Orrin (1944). "Reseña: The Calculi of Lambda-Conversion de Alonzo Church" (PDF) . Boletín de la Sociedad Matemática Americana . 50 (3): 169– 172. doi : 10.1090/s0002-9904-1944-08090-7 .
• Kleene, Stephen, Una teoría de los enteros positivos en lógica formal , American Journal of Mathematics , 57 (1935), pp.  153–173 y 219–244. Contiene las definiciones del cálculo lambda de varias funciones conocidas.
• Landin, Peter , «Una correspondencia entre ALGOL 60 y la notación lambda de Church» , Communications of the ACM , vol. 8, n.º 2 (1965), páginas 89-101. Disponible en el sitio web 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.^{[ 1 ]}
• Schalk, A. y Simmons, H. (2005) Introducción al cálculo lambda y a la aritmética con una buena selección de ejercicios . Apuntes para un curso de la maestría en lógica matemática en la Universidad de Manchester.
• de Queiroz, Ruy JGB (2008). "Sobre las reglas de reducción, el significado como uso y la semántica de la teoría de la demostración". 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", la cual, aunque se basa en demostraciones, es diferente de la semántica de la teoría de la demostración como en la tradición de Dummett-Prawitz, ya que toma la reducción como las reglas que dan significado.
• Hankin, Chris, Introducción al cálculo 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), Lecciones sobre el isomorfismo de Curry-Howard , Elsevier, ISBN 0-444-52077-5Es una monografía reciente que abarca los principales temas del cálculo lambda, desde la variante sin tipos hasta la mayoría de los cálculos lambda tipados , incluyendo desarrollos más recientes como los sistemas de tipos puros y el cubo lambda . No incluye extensiones de subtipos .
• Pierce, Benjamin (2002), Tipos y lenguajes de programación , MIT Press, ISBN 0-262-16209-1El libro abarca el cálculo lambda desde la perspectiva de un sistema de tipos práctico; algunos temas, como los tipos dependientes, solo se mencionan, pero el subtipado es un tema importante.

Documentos

• Una breve introducción al cálculo lambda ( PDF ) por Achim Jung
• Cronología del cálculo lambda - ( PDF ) por Dana Scott
• Introducción al cálculo lambda ( PDF ) por Raúl Rojas
• Apuntes de clase sobre el cálculo lambda ( PDF ) por Peter Selinger
• Cálculo lambda gráfico de Marius Buliga
• El libro "Cálculo Lambda como Modelo de Flujo de Trabajo" de Peter Kelly, Paul Coddington y Andrew Wendelborn menciona la reducción de grafos como un método 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 paralela de grafos para expresiones lambda).

• Graham Hutton, Cálculo Lambda , un breve vídeo (12 minutos) de Computerphile 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, Diseccionar 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
• LCI Lambda Interpreter: un intérprete de cálculo puro sencillo pero potente.
• Enlaces sobre cálculo lambda en Lambda-the-Ultimate
• Mike Thyer, Lambda Animator , un miniaplicativo gráfico de Java que demuestra estrategias de reducción alternativas.
• Implementación del cálculo lambda mediante plantillas de C++
• Shane Steinert-Threlkeld, "Lambda Calculi" , Enciclopedia de Filosofía de Internet
• Anton Salikhmetov, Cálculo macro lambda