Cálculo lambda

Compartir Imprimir Citar
Sistema matemático-lógico basado en funciones

Lambda calculus (también escrito como λ-calculus) es un sistema formal en lógica matemática para expresar el cálculo basado en la abstracción y aplicación de funciones. utilizando unión y sustitución de variables. Es un modelo universal de computación que se puede utilizar para simular cualquier máquina de Turing. 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.

El cálculo lambda consiste en construir § términos lambda y realizar § operaciones de reducción sobre ellos. En la forma más simple de cálculo lambda, los términos se construyen usando solo las siguientes reglas:

Las operaciones de reducción incluyen:

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, producirá una forma β-normal.

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

Explicación y aplicaciones

El cálculo Lambda es Turing completo, es decir, es un modelo universal de computación que se puede utilizar para simular cualquier máquina de Turing. 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 sin tipo o escrito. En el cálculo lambda tipado, las funciones se pueden aplicar solo si son capaces de aceptar el 'tipo' de la entrada dada. de datos. Los cálculos lambda tipificados son más débiles que los cálculos lambda no tipificados, que es el tema principal de este artículo, en el sentido de que los cálculos lambda tipificados pueden expresar menos que los cálculos no tipificados, pero, por otro lado, los cálculos lambda tipificados permiten probar más cosas; en el cálculo lambda de tipo simple es, por ejemplo, un teorema de que toda estrategia de evaluación termina para cada término lambda de tipo simple, mientras que la evaluación de términos lambda no tipificados no necesita terminar. Una de las razones por las que hay muchos cálculos lambda tipificados diferentes ha sido el deseo de hacer más (de lo que puede hacer el cálculo no tipificado) sin renunciar a poder probar teoremas sólidos sobre el cálculo.

El cálculo lambda tiene aplicaciones en muchas áreas diferentes de las matemáticas, la filosofía, la lingüística y la informática. El cálculo lambda ha jugado 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.

Historia

El matemático Alonzo Church introdujo el cálculo lambda en la década de 1930 como parte de una investigación sobre los fundamentos de las matemáticas. Se demostró que el sistema original era lógicamente inconsistente en 1935 cuando Stephen Kleene y J. B. Rosser desarrollaron la paradoja de Kleene-Rosser.

Posteriormente, en 1936, Church aisló y publicó solo la parte relevante para el cálculo, lo que ahora se denomina cálculo lambda sin tipo. En 1940, también introdujo un sistema computacionalmente más débil, pero lógicamente consistente, conocido como cálculo lambda de tipo simple.

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 Richard Montague y otros lingüistas' aplicaciones en la semántica del lenguaje natural, el cálculo lambda ha comenzado a disfrutar de un lugar respetable tanto en la lingüística como en la informática.

Origen del símbolo lambda

Existe cierta incertidumbre sobre el motivo por el que Church utiliza la letra griega lambda (λ) como notación para la función-abstracción en el cálculo lambda, quizás en parte debido a las explicaciones contradictorias del propio Church. Según Cardone y Hindley (2006):

Por cierto, ¿por qué la Iglesia eligió la notación “λ”? En [una carta inédita de 1964 a Harald Dickson] dijo claramente que vino de la notación "x^ ^ {displaystyle {hat {x}}” utilizado para la abstracción de clase por Whitehead y Russell, modificando primero “x^ ^ {displaystyle {hat {x}}” a “∧ ∧ x{displaystyle land x}” para distinguir la abstracción de la función de la abstracción de clase, y luego cambiar “∧ ∧ {displaystyle land }” a “λ” para facilidad de impresión.

This origin was also reported in [Rosser, 1984, p.338]. Por otro lado, en sus últimos años La Iglesia dijo a dos preguntadores que la elección era más accidental: un símbolo era necesario y λ acababa de ser elegido.

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

Querido profesor Iglesia,

Russell tenía el operador de yota, Hilbert tenía el operador de epsilon. ¿Por qué elegiste lambda para tu operador?

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

Descripción informal

Motivación

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

square¿Qué? ¿Qué? sum⁡ ⁡ ()x,Sí.)=x2+Sí.2{displaystyle operatorname {square_sum} (x,y)=x^{2}+y^{2}

puede reescribirse en forma anónima como

()x,Sí.)↦ ↦ x2+Sí.2{displaystyle (x,y)mapsto x^{2}+y^{2}

(que se lee como "un tuple de x y Sí. es mapeado a x2+Sí.2{textstyle x^{2}+y^{2}"). Asimismo, la función

id⁡ ⁡ ()x)=x{displaystyle operatorname {id} (x)=x}

puede reescribirse en forma anónima como

x↦ ↦ x{displaystyle xmapsto x}

donde la entrada simplemente se asigna a sí misma.

La segunda simplificación es que el cálculo de la lambda solo utiliza funciones de una sola entrada. Una función ordinaria que requiere dos entradas, por ejemplo la square¿Qué? ¿Qué? sum{textstyle operatorname {square_sum} función, se puede volver a trabajar en una función equivalente que acepta una sola entrada, y como rendimiento de salida otro función, que a su vez acepta una sola entrada. Por ejemplo,

()x,Sí.)↦ ↦ x2+Sí.2{displaystyle (x,y)mapsto x^{2}+y^{2}

puede transformarse en

x↦ ↦ ()Sí.↦ ↦ x2+Sí.2){displaystyle xmapsto (ymapsto x^{2}+y^{2}}

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

Aplicación de la función square¿Qué? ¿Qué? sum{textstyle operatorname {square_sum} función a los argumentos (5, 2), rendimientos a la vez

()()x,Sí.)↦ ↦ x2+Sí.2)()5,2){textstyle (x,y)mapsto x^{2}+y^{2}(5,2)}
=52+22{textstyle =5^{2}+2^{2}
=29{textstyle =29},

mientras que la evaluación de la versión con curry requiere un paso más

()()x↦ ↦ ()Sí.↦ ↦ x2+Sí.2))()5))()2){fnMicrosoft Sans Serif} {fnMicrosoft Sans Serif} {fnMicrosoft Sans Serif}} {bigr]}(5){Bigr)}(2)}}
=()Sí.↦ ↦ 52+Sí.2)()2){textstyle =(ymapsto 5^{2}+y^{2}(2)} // la definición de x{displaystyle x} se ha utilizado con 5{displaystyle 5} en la expresión interna. Esto es como β-reducción.
=52+22{textstyle =5^{2}+2^{2} // la definición de Sí.{displaystyle y} se ha utilizado con 2{displaystyle 2}. Otra vez, similar a β-reducción.
=29{textstyle =29}

para llegar al mismo resultado.

El cálculo lambda

El cálculo lambda consiste en un lenguaje de términos lambda, que están definidos por una cierta sintaxis formal, y un conjunto de reglas de transformación para manipular los términos lambda. Estas reglas de transformación pueden verse como una teoría ecuacional o como una definición operativa.

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 currying se utiliza para implementar funciones de varias variables.

Términos lambda

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

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

Nada más es un término lambda. Por lo tanto, un término lambda es válido si y solo si puede obtenerse mediante la aplicación repetida de estas tres reglas. Sin embargo, algunos paréntesis se pueden omitir de acuerdo con ciertas reglas. Por ejemplo, los paréntesis más externos generalmente no se escriben. Ver Notación, a continuación.

An abstracción λ λ x.t{displaystyle lambda x.t} denota una función anónima que toma una sola entrada x y retornos t. Por ejemplo, λ λ x.x2+2{displaystyle lambda x.x^{2}+2} es una abstracción para la función f()x)=x2+2{displaystyle f(x)=x^{2}+2} utilizando el término x2+2{displaystyle x^{2}+2} para t. El nombre f()x){displaystyle f(x)} es superfluo al usar la abstracción. ()λ λ x.t){displaystyle (lambda x.t)} une la variable x en el término t. La definición de una función con una abstracción simplemente "ajusta" la función pero no la invoca.

An aplicación t{displaystyle t} s{displaystyle s} representa la aplicación de una función t a una entrada s, es decir, representa el acto de la función de llamada t sobre la entrada s para producir t()s){displaystyle t(s)}.

No hay concepto en el cálculo de lambda de declaración variable. En una definición como λ λ x.x+Sí.{displaystyle lambda x.x+y} (i.e. f()x)=x+Sí.{displaystyle f(x)=x+y}), en Lambda cálculo Sí. es una variable que aún no está definida. La abstracción λ λ x.x+Sí.{displaystyle lambda x.x+y} es sintácticamente válida, y representa una función que añade su entrada al aún desconocido Sí..

Pueden usarse paréntesis y pueden ser necesarios para eliminar la ambigüedad de los términos. Por ejemplo,

  1. λ λ x.()()λ λ x.x)x){displaystyle lambda x.(lambda x.x)x)} que es de forma λ λ x.B{displaystyle lambda x. B. - una abstracción, y
  2. ()()λ λ x.x)x){displaystyle (lambda x.x)x)} que es de forma MN{displaystyle MN. - Una aplicación. Los ejemplos 1 y 2 denotan diferentes términos; sin embargo, el ejemplo 1 es una definición de función, mientras que el ejemplo 2 es una aplicación.

Aquí, ejemplo 1 define una función λ λ x.B{displaystyle lambda x. B., donde B{displaystyle B} es ()()λ λ x.x)x){displaystyle (lambda x.x)x)}, el resultado de la aplicación ()λ λ x.x){displaystyle (lambda x.x)} a x, mientras que el ejemplo 2 es MN{displaystyle MN.; M{displaystyle M} es el término lambda ()λ λ x.x){displaystyle (lambda x.x)} para ser aplicado a la entrada N. Ambos ejemplos 1 y 2 evaluarían a la función de identidad λ λ x.x{displaystyle lambda x.x}.

Funciones que operan sobre funciones

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

Por ejemplo, λ λ x.x{displaystyle lambda x.x} representa la función de identidad, x↦ ↦ x{displaystyle xmapsto x}, y ()λ λ x.x)Sí.{displaystyle (lambda x.x)y} representa la función de identidad aplicada Sí.{displaystyle y}. Además, ()λ λ x.Sí.){displaystyle (lambda x.y)} representa el función constante x↦ ↦ Sí.{displaystyle xmapsto y}, la función que siempre regresa Sí.{displaystyle y}No importa la entrada. En el cálculo de lambda, la aplicación de la función se considera como asociativa izquierda, de modo que stx{displaystyle stx} medios ()st)x{displaystyle (st)x}.

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

Equivalencia alfa

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

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

Variables libres

Las variables libres de un término son aquellas variables no ligadas por una abstracción. El conjunto de variables libres de una expresión se define inductivamente:

Por ejemplo, el término lambda que representa la identidad λ λ x.x{displaystyle lambda x.x} no tiene variables libres, pero la función λ λ x.Sí.{displaystyle lambda x.y} x{displaystyle x} tiene una sola variable libre, Sí.{displaystyle y}.

Sustituciones para evitar capturas

Un cambio sistemático en las variables para evitar la captura de una variable libre puede introducir errores en un lenguaje de programación funcional donde las funciones son ciudadanos de primera clase.

Suppose t{displaystyle t}, s{displaystyle s} y r{displaystyle r} son términos de lambda y x{displaystyle x} y Sí.{displaystyle y} son variables. La notación t[x:=r]{displaystyle t[x:=r]} indica la sustitución de r{displaystyle r} para x{displaystyle x} dentro t{displaystyle t} en una capturar-evitar Así. Esto se define de modo que:

Por ejemplo, ()λ λ x.x)[Sí.:=Sí.]=λ λ x.()x[Sí.:=Sí.])=λ λ x.x{displaystyle (lambda x.x)[y:=y]=lambda x.(x[y:=y])=lambda x.x}, y ()()λ λ x.Sí.)x)[x:=Sí.]=()()λ λ x.Sí.)[x:=Sí.])()x[x:=Sí.])=()λ λ x.Sí.)Sí.{displaystyle (lambda x.y)x)[x:=y]=(lambda x.y)[x:=y])(x[x:=y])=(lambda x.y)y}.

El estado de frescura (requiriendo que Sí.{displaystyle y} no está en las variables libres r{displaystyle r}) es crucial para asegurar que la sustitución no cambie el significado de las funciones. Por ejemplo, una sustitución que ignora la condición de frescura puede llevar a errores: ()λ λ x.Sí.)[Sí.:=x]=λ λ x.()Sí.[Sí.:=x])=λ λ x.x{displaystyle (lambda x.y)[y:=x]=lambda x.(y[y:=x])=lambda x.x}. Esta sustitución gira la función constante λ λ x.Sí.{displaystyle lambda x.y} en la identidad λ λ x.x{displaystyle lambda x.x} por sustitución.

En general, el incumplimiento de la condición de frescura puede ser remediado por alfa-renaming con una variable fresca adecuada. Por ejemplo, cambiar de nuevo a nuestra noción correcta de sustitución, en ()λ λ x.Sí.)[Sí.:=x]{displaystyle (lambda x.y)[y:=x]} la abstracción se puede renombrar con una variable fresca z{displaystyle z}, para obtener ()λ λ z.Sí.)[Sí.:=x]=λ λ z.()Sí.[Sí.:=x])=λ λ z.x{displaystyle (lambda z.y)[y:=x]=lambda z.(y[y:=x])=lambda z.x}, y el significado de la función se conserva por sustitución.

Β-reducción

La regla de reducción β establece que una aplicación de la forma ()λ λ x.t)s{displaystyle (lambda x.t)s} reduce al término t[x:=s]{displaystyle t[x:=s]}. La notación ()λ λ x.t)s→ → t[x:=s]{displaystyle (lambda x.t)sto t[x:=s]} se utiliza para indicar que ()λ λ x.t)s{displaystyle (lambda x.t)s} β-reduce a t[x:=s]{displaystyle t[x:=s]}. Por ejemplo, para cada s{displaystyle s}, ()λ λ x.x)s→ → x[x:=s]=s{displaystyle (lambda x.x)sto x[x:=s]=s}. Esto demuestra que λ λ x.x{displaystyle lambda x.x} realmente es la identidad. Análogamente, ()λ λ x.Sí.)s→ → Sí.[x:=s]=Sí.{displaystyle (lambda x.y)sto y[x:=s]=y}, que demuestra que λ λ x.Sí.{displaystyle lambda x.y} es una función constante.

El cálculo de lambda puede verse como una versión idealizada de un lenguaje de programación funcional, como Haskell o Standard ML. En esta opinión, β-reducción corresponde a un paso computacional. Este paso puede repetirse con reducciones adicionales de β hasta que no quedan más aplicaciones para reducir. En el cálculo de lambda sin tipo, como se presenta aquí, este proceso de reducción puede no terminar. Por ejemplo, considere el término Ω Ω =()λ λ x.xx)()λ λ x.xx){displaystyle Omega =(lambda x.xx)(lambda x.xx)}. Aquí. ()λ λ x.xx)()λ λ x.xx)→ → ()xx)[x:=λ λ x.xx]=()x[x:=λ λ x.xx])()x[x:=λ λ x.xx])=()λ λ x.xx)()λ λ x.xx){displaystyle (lambda x.xx)(lambda x.xx)to (xx)[x:=lambda x.xx]=(x[x:=lambda x.xxx])(x[x:=lambda x.xx])=(lambda x.xx)(lambda x.xxxx}. Es decir, el término se reduce a sí mismo en una sola β-reducción, y por lo tanto el proceso de reducción nunca terminará.

Otro aspecto del cálculo lambda sin tipo es que no distingue entre diferentes tipos de datos. Por ejemplo, puede ser deseable 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.

Definición formal

Definición

Las expresiones lambda se componen de:

El conjunto de expresiones lambda, Λ, se puede definir de forma inductiva:

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

Las instancias de la regla 2 se conocen como abstracciones y las instancias de la regla 3 se conocen como aplicaciones.

Notación

Para mantener ordenada la notación de las expresiones lambda, se suelen aplicar las siguientes convenciones:

Variables libres y enlazadas

Se dice que el operador de abstracción, λ, vincula su variable dondequiera 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 ligadas. En una expresión λx.M, la parte λx a menudo se llama aglutinante, como una pista de que el la variable x se vincula agregando λx a M. Todas las demás variables se denominan libres. Por ejemplo, en la expresión λy.x x y, y es una variable ligada y x es una variable libre. También una variable está ligada por su abstracción más cercana. En el siguiente ejemplo, la aparición única de x en la expresión está limitada por la segunda expresión 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 recursividad en el 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}.
  3. FV(M N) = FV(M∪ FV(N).

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

Reducción

El significado de las expresiones lambda se define por cómo se pueden reducir las expresiones.

Hay tres tipos de reducción:

También hablamos de las equivalencias resultantes: dos expresiones son α-equivalentes, si pueden convertirse en α 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 reducción; la reducción de (λx.M) N es M[x: = N].

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

Conversión Α

La conversión α, a veces conocida como cambio de nombre α, permite cambiar los nombres de las variables vinculadas. Por ejemplo, la conversión α de λx.x podría producir λy.y. Los términos que difieren solo en la conversión α se denominan equivalente α. 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. En primer lugar, cuando se convierte una abstracción en α, las únicas ocurrencias de variables que se renombran son aquellas que están vinculadas a la misma abstracción. Por ejemplo, una conversión α de λx.λx.x podría resultar en λy.λ x.x, pero podría no resultar en λy.λx.y. Este último tiene un significado diferente al original. Esto es análogo a la noción de programación de sombreado variable.

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 con 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 usar para simplificar la resolución de nombres al garantizar que ningún nombre de variable enmascare un nombre en un alcance contenedor (consulte Cambio de nombre α para hacer que la resolución de nombres sea trivial).

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

Sustitución

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 con expresión N. La sustitución en los términos del cálculo lambda se define mediante la recursión en la estructura de los 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
Sí.[x:= N= Sí., si x ل Sí.
()M1 M2[x:= N= M1[x:= N] M2[x:= N]
(λ)x.M[x:= N] = λx.M
(λ)Sí..M[x:= N] = λSí..(M[x:= N]), si x ل Sí. y Sí. ∉ FV(N) Ver arriba para el FV

Para sustituir en una abstracción, a veces es necesario convertir la expresión en α. Por ejemplo, no es correcto que (λx.y)[y:= x] resulte en λx.x, porque se suponía que el x sustituido era libre pero terminó siendo atado. La sustitución correcta en este caso es λz.x, hasta la equivalencia α. La sustitución se define de forma única hasta la equivalencia α.

Β-reducción

La reducción β captura la idea de la 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].

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

Puede verse 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.

Η-reducción

η-reducción (reducción eta) 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 λx.f x y f siempre que x lo hace no aparece libre en f.

Puede verse 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.

Formas normales y confluencia

Para el cálculo lambda sin tipo, la reducción β como regla de reescritura no es ni fuerte 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 de normalización fuerte como los términos de normalización débil tienen una forma normal única. Para términos fuertemente normalizados, se garantiza que cualquier estrategia de reducción producirá la forma normal, mientras que para términos débilmente normalizados, algunas estrategias de reducción pueden fallar en encontrarla.

Codificación de tipos de datos

El cálculo lambda básico puede usarse para modelar booleanos, aritmética, estructuras de datos y recursividad, como se ilustra en las siguientes subsecciones.

Aritmética en cálculo lambda

Hay varias formas posibles de definir los números naturales en el cálculo lambda, pero, con diferencia, las más comunes son los números de Iglesia, 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 usando la sintaxis alternativa presentada arriba en Notación:

0:= λfx.x
1:= λfx.f x
2:= λfx.f ()f x)
3:= λfx.f ()f ()f x)

Un número de iglesia 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 número de iglesia n es una función que asume 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 de hecho es el n-ésima potencia de f (considerado como un operador); f(0) se define como la función de identidad. Tales composiciones repetidas (de una sola función f) obedecen las leyes de los exponentes, razón por la cual estos números se pueden usar para la aritmética. (En el cálculo lambda original de Church, se requería que el parámetro formal de una expresión lambda ocurriera 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 número de iglesia n, que suele ser útil al analizar programas, es como una instrucción 'repetir n veces'. Por ejemplo, usando las funciones PAIR y NIL definidas a continuación, se puede definir una función que construye una lista (enlazada) de n elementos todos iguales a x repitiendo 'anteponer otro elemento x' n veces, a partir de una lista vacía. El término lambda es

λn.λx.n (PAIR xNIL

Al variar lo que se repite y el argumento al que se aplica la función que se repite, se pueden lograr muchos efectos diferentes.

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

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

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

PLUS:= λ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 comprobar que

PLUS 2 3

y

5

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

PLUS:= λm.λn.m SUCC n

Del mismo modo, la multiplicación se puede definir como

MULT:= λm.λn.λf.m ()n f)

Alternativamente

MULT:= λm.λn.m (PLUS n)

ya que multiplicar m y n es lo mismo que repitiendo la función add n m veces y luego aplicándola a cero. La exponenciación tiene una traducción bastante simple en los números de la Iglesia, a saber

POW:= λb.λe.e b

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 formula

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

se puede validar mostrando inductivamente que si T denota (λg.λh.h (g f)), luego T(n)(λu.x) = (λh.h(f(n−1)(x))) para <span class="monospaced" n > 0. A continuación se dan otras dos definiciones de PRED, una con condicionales y la otra con pares. Con la función predecesora, la resta es sencilla. Definición

SUB:= λm.λn.n PRED m,

SUB m n produce m − n cuando m > n y 0 de lo contrario.

Lógica y predicados

Por convención, las dos definiciones siguientes (conocidas como booleanos de la Iglesia) se utilizan para los valores booleanos TRUE y FALSE:

TRUE:= λx.λSí..x
FALSE:= λx.λSí..Sí.

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

Y...p.λq.p q p
OR:= λp.λq.p p q
NO:= λp.p FALSE TRUE
IFTHENELSE:= λp.λa.λb.p a b

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

Y la verdad
(λ)p.λq.p q p) TRUE FALSE →β TRUE FALSE TRUE
(λ)x.λSí..x) FALSE TRUE →β FALSE

y vemos que AND TRUE FALSE es equivalente a FALSE.

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 número de iglesia 0 , y FALSE si su argumento es cualquier otro número de Iglesia:

ISZERO:= λn.n (λ)xTRUE

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

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

y dado que 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 "si- entonces-más" Expresiones en cálculo lambda. Por ejemplo, la función predecesora se puede definir como:

PRED:= λn.n (λ)g.λk.ISZEROg 1) k (PLUS)g k1))v0) 0

que se puede verificar mostrando inductivamente que n (λg.λk.ISZERO (g 1) k (MÁS (g k) 1)) (λv.0) es la función de añadir n − 1 para n > 0.

Parejas

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

PAIR:= λx.λSí..λf.f x Sí.
PRIMERO:= λp.p TRUE
SEGUNDO:= λp.p FALSE
NIL:= λx. TRUE
NULL:= λp.p (λ)x.λSí..FALSE)

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

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

⋅:= λx. PAIR (SECOND x(SUCC) x)

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

PRED:= λn. PRIMERAn Ё (PAIR 0 0)).

Técnicas de programación adicionales

Existe un cuerpo considerable de modismos de programación para el cálculo lambda. Muchos de estos se desarrollaron originalmente en el contexto del uso del cálculo lambda como base para la semántica del lenguaje 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 tienen uso en la programación práctica, pero luego pueden percibirse como oscuras o extrañas.

Constantes con nombre

En el cálculo lambda, una biblioteca tomaría la forma de una colección de funciones previamente definidas, que como términos lambda son meramente 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 al reservar una variable como el nombre de la constante, usando la abstracción para vincular esa variable en el cuerpo principal., y aplicar esa abstracción a la definición prevista. Por lo tanto, usar f para significar N (algún término lambda explícito) en M (otro término lambda, el "programa principal"), se puede decir

(λ)f.M) N

Los autores suelen introducir azúcar sintáctico, como let, para permitir escribir lo anterior en un orden más intuitivo.

Deja f =N dentro M

Al encadenar tales 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 se define en N, para que N esté fuera del alcance del enlace de abstracción f; esto significa que una definición de función recursiva no se puede usar como N con let. La construcción letrec permitiría escribir definiciones de funciones recursivas.

Recursión y puntos fijos

La recursividad es la definición de una función usando la función misma. El cálculo lambda no puede expresar esto tan directamente como otras notaciones: todas las funciones son anónimas en el cálculo lambda, por lo que no podemos referirnos a un valor que aún no se ha definido, dentro del término lambda que define ese mismo valor. Sin embargo, aún se puede lograr la recursión al hacer arreglos para que una expresión lambda se reciba a sí misma como su valor de argumento, por ejemplo en  (λx.x x) E.

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

F(n) = 1, si n = 0; si no n × F(n −1).

En la expresión lambda que va a representar esta función, se supondrá que un parámetro (normalmente el primero) recibe la propia expresión lambda como su valor, de modo que al llamarla, aplicarla a un argumento – equivaldrá a la recursividad. Por lo tanto, para lograr la recursividad, el argumento previsto como autorreferencial (llamado r aquí) 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; si no n ×r r ()n−1))
con r r x F x G r x Espera, así que r G y
F:= G = (λ)x.x xG

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, lo que hace que esté disponible para ser referenciada y llamada allí.

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

G:= λrλn.(1, si n = 0; si no n ×r ()n−1))
con r x F x G r x Espera, así que r G r =: FIX G y
F:= FIX G Donde FIX g:=r Donde r = g r) g (FIX g)
así FIX G = G (FIX G) = (λ)n.(1, si n = 0; si no n × (FIX G)n−1)))

Dado un término lambda con el primer argumento que 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). No es necesario que la función se pase 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 recrea dentro de sí misma, en el punto de llamada, logrando la autorreferencia.

De hecho, hay 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:

()Y G) 4
GY G) 4
(λ)r.λn.(1, si n = 0; si no n ×r ()n−1))) ()Y G) 4
(λ)n.(1, si n = 0; si no n ×Y G)n−1))) 4
1, si 4 = 0; si no 4 × ((Y G) (4−1))
4 × (G)Y G) (4−1))
4 × ((λ)n.(1, si n = 0; si no n ×Y G)n−1))) – (41))
4 × (1, si 3 = 0; si no 3 × ((Y G) (3 a 1)))
4 × (3 × (G)Y G) (3 a 1)))
4 × (3 ×)n.(1, si n = 0; si no n ×Y G)n1)) (31)))
4 × (3 × (1, si 2 = 0; si no 2 × ((Y G) (2 a 1))))
4 × (3 × (2 × (G)Y G) (2 a 1))))
4 × (3 × (2 ×)n.(1, si n = 0; si no n ×Y G)n1)) (21)))
4 × (3 × (2 × 1, si 1 = 0; si no 1 × ((Y G) (1−1)))))
4 × (3 × (2 × (1 × (G)Y G) (1−1)))))
4 × (3 × (2 × (1 ×)n.(1, si n = 0; si no n ×Y G)n−1)))) (1−1))))
4 × (3 × (2 × (1 × 1, si 0 = 0; si no 0 × ((Y G) (0 a 1)))))))
4 × (3 × (2 × (1 × 1))))
24

Cada función definida de forma recursiva puede verse como un punto fijo de alguna función adecuadamente definida que cierra la llamada recursiva con un argumento adicional y, por lo tanto, usa Y, cada función definida recursivamente se puede expresar como una expresión lambda. En particular, ahora podemos definir claramente el predicado de resta, multiplicación y comparación de números naturales recursivamente.

Condiciones estándar

Ciertos términos tienen nombres comúnmente aceptados:

I:=x.x
S:=x.λSí..λz.x z ()Sí. z)
K:=x.λSí..x
B:=x.λSí..λz.x ()Sí. z)
C:=x.λSí..λz.x z Sí.
W:=x.λSí..x Sí. Sí.
⋅ o Δ o U:=x.x x
Ω:= ω

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

Eliminación de abstracción

Si N es un término lambda sin abstracción, pero posiblemente contiene constantes con nombre (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 se consideran no atómicas). Esto también se puede ver como variables anonimizadoras, ya que T(x,N) elimina todas las apariciones de x de N, al mismo tiempo que permite que los valores de los argumentos se sustituyan en las posiciones donde N contiene una x. La función de conversión T se puede definir mediante:

T()x, x) I
T()x, N) K N si x no es libre en N.
T()x, M N) S T()x, M) T()x, N)

En cualquier caso, un término de la forma T(x,N) P puede reducir si el combinador inicial I, K o S toma el argumento P , al igual que la reducción β de (λx.N) P sería suficiente. I devuelve ese argumento. K descarta el argumento, al igual que (λx.N) funcionaría si x no tuviera 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 solo un subtérmino de una aplicación ( B al subtérmino "argumento" y C al subtérmino "función"), guardando así un subsiguiente K si no aparece 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 hace solo lo último, produciendo el sistema B, C, K, W como una alternativa al cálculo del combinador SKI.

Cálculo lambda escrito

A lambda cálculo es un formalismo tipo que utiliza el lambda-símbolo (λ λ {displaystyle lambda }) para denotar la abstracción de funciones anónimas. En este contexto, los tipos son generalmente objetos de naturaleza sintáctica que se asignan a términos de lambda; la naturaleza exacta de un tipo depende del cálculo considerado (ver Tipos de calculi de lambda tipo). Desde cierto punto de vista, calculi de lambda tipod se puede ver como refinamientos del cálculo de la lambda sin tipo, pero desde otro punto de vista, también pueden considerarse la teoría más fundamental y lambda cálculo un caso especial con un solo tipo.

Los cálculos lambda tipificados son lenguajes de programación fundamentales y son la base de los lenguajes de programación funcional tipificados como ML y Haskell y, más indirectamente, los lenguajes de programación imperativos tipificados. Los cálculos lambda tipificados juegan un papel importante en el diseño de sistemas de tipos para lenguajes de programación; aquí tipificación por lo general captura las propiedades deseables del programa, por ejemplo, el programa no causará una violación de acceso a la memoria.

Los cálculos lambda tipificados 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, p. el cálculo lambda simplemente tipeado es el lenguaje de las categorías cerradas cartesianas (CCC).

Estrategias de reducción

Si un término se está normalizando o no, y cuánto trabajo se necesita hacer para normalizarlo, si es así, depende en gran medida de la estrategia de reducción utilizada. Las estrategias comunes de reducción del cálculo lambda incluyen:

Orden normal
El más izquierdo, el más exterior de Redex siempre se reduce primero. Es decir, siempre que sea posible, los argumentos se sustituyen al cuerpo de una abstracción antes de que se reduzcan los argumentos.
Orden Aplicable
El más izquierdista, más interior, siempre se reduce primero. Intuitivamente esto significa que los argumentos de una función siempre se reducen antes de la función misma. El orden aplicado siempre intenta aplicar funciones a formas normales, incluso cuando esto no es posible.
Reducciones completas de β
Cualquier redex se puede reducir en cualquier momento. Esto significa esencialmente la falta de una estrategia de reducción en particular, con respecto a la reducibilidad, "todas las apuestas están fuera".

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

Llamada por valor
Un redex se reduce sólo cuando su lado derecho se ha reducido a un valor (variable o abstracción). Sólo los redexes exteriores se reducen.
Llamada por nombre
Como orden normal, pero no se realizan reducciones dentro de abstracciones. Por ejemplo, λx.(λ)Sí..Sí.)x está en forma normal según esta estrategia, aunque contiene el redex (λ)Sí..Sí.)x.

Las estrategias para compartir reducen los cálculos que son "iguales" en paralelo:

Reducción óptima
Como orden normal, pero las computaciones que tienen la misma etiqueta se reducen simultáneamente.
Llamada por necesidad
Como llamada por nombre (hence débil), pero aplicaciones de función que duplicarían términos en lugar de nombrar el argumento, que se reduce sólo "cuando se necesita".

Computabilidad

No hay ningún algoritmo que tome como entrada dos expresiones lambda y genere TRUE o FALSE dependiendo de si una expresión reduce para el otro. Más precisamente, ninguna función computable puede decidir la cuestión. Este fue históricamente el primer problema para el que se pudo probar la indecidibilidad. Como es habitual para tal demostración, computable significa computable por cualquier modelo de computación que sea Turing completo. De hecho, la computabilidad se puede definir mediante el 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 y y son los números de iglesia correspondientes a x y y, respectivamente y =β que significa equivalencia con β-reducción. Consulte la tesis de Church-Turing para conocer otros enfoques para definir la computabilidad y su equivalencia.

La prueba de incomputabilidad de Church primero reduce 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. 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 de Gödel' s primer teorema de incompletitud. Si e se aplica a su propio número de Gödel, se produce una contradicción.

Complejidad

La noción de complejidad computacional para el cálculo lambda es un poco engañosa, porque el costo de una reducción β puede variar según cómo se implemente. Para ser precisos, de alguna manera se debe encontrar 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 director fueron un enfoque temprano que cambió este costo de tiempo por un uso de espacio cuadrático. De manera más general, 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 β 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 un Turing máquina en el tiempo polinomialmente proporcional al número de pasos. 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 al trabajar con una representación compartida compacta. El resultado deja en 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 del espacio.

Un modelo poco razonable no significa necesariamente que sea ineficiente. La reducción óptima reduce todos los cálculos con la misma etiqueta en un solo paso, evitando el trabajo duplicado, pero el número de pasos paralelos de reducción β para reducir un término dado a su 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 al manejo de la duplicación de redexes durante la reducción β. 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 y más externos 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 y el más externo. 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.

Cálculo lambda y lenguajes de programación

Como se señaló en el artículo de 1965 de Peter Landin 'A Correspondence between ALGOL 60 and Church's Lambda-notation', los lenguajes de programación de procedimientos secuenciales se pueden entender en términos del cálculo lambda, que proporciona los mecanismos básicos para la abstracción de procedimientos y la aplicación de procedimientos (subprogramas).

Funciones anónimas

Por ejemplo, en Python, el "cuadrado" La función 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 lambda crea una función anónima, dada una lista de nombres de parámetros, x, solo un argumento en este caso, y una expresión que se evalúa como el cuerpo del función, x**2. Las funciones anónimas a veces se denominan expresiones lambda.

Por ejemplo, Pascal y muchos otros lenguajes imperativos han admitido durante mucho tiempo pasar 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.

Paralelismo y concurrencia

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

Semántica

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ó dudas 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 era encontrar un conjunto D isomorfo al espacio funcional D → D, de funciones sobre sí mismo. Sin embargo, no puede existir ninguna no trivial como D, por restricciones de cardinalidad porque el conjunto de todas las funciones de D a 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.

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

Variaciones y extensiones

Estas extensiones están en el cubo lambda:

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

Estos sistemas formales son variaciones del cálculo lambda:

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