Cálculo lambda - Lambda calculus

El cálculo lambda (también escrito como cálculo λ ) es un sistema formal en lógica matemática para expresar el cálculo basado en la abstracción y aplicación de funciones mediante la vinculación y sustitución de variables . Es un modelo de cálculo universal 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 en ellos. En la forma más simple de cálculo lambda, los términos se construyen usando solo las siguientes reglas:

produciendo expresiones como: (λ x .λ y . (λ z . (λ x . zx ) (λ y . zy )) ( xy )). Los paréntesis se pueden quitar si la expresión no es ambigua. Para algunas aplicaciones, se pueden incluir términos para operaciones y constantes lógicas y matemáticas.

Las operaciones de reducción incluyen:

Si se usa la indexación de De Bruijn , entonces la conversión α ya no es necesaria 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 variable 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 sobre sí misma en varias combinaciones.

Explicación y aplicaciones

El cálculo lambda es Turing completo , es decir, es un modelo universal de cálculo 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 no estar tipificado o tipificado . En el cálculo lambda tipado, las funciones se pueden aplicar solo si son capaces de aceptar el "tipo" de datos de la entrada dada. Los cálculos lambda tipificados son más débiles que el cálculo lambda no tipificado, que es el tema principal de este artículo, en el sentido de que los cálculos lambda tipificados pueden expresar menos que el cálculo lambda no tipificado, pero por otro lado los cálculos lambda tipificados permiten probar más cosas. ; en el cálculo lambda simplemente tipado es, por ejemplo, un teorema que toda 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. Una razón por la que hay muchos cálculos lambda con tipos diferentes ha sido el deseo de hacer más (de lo que puede hacer el cálculo sin tipo) sin renunciar a poder demostrar teoremas sólidos sobre el cálculo.

El cálculo lambda tiene aplicaciones en muchas áreas diferentes en matemáticas , filosofía , lingüística e 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 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 . Se demostró que el sistema original era lógicamente inconsistente en 1935 cuando Stephen Kleene y JB 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 no tipificado. En 1940, también introdujo un sistema computacionalmente más débil, pero lógicamente consistente, conocido como cálculo lambda simplemente tipado .

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 disfrutar de un lugar respetable tanto en lingüística como en informática.

Origen del símbolo lambda

Existe cierta incertidumbre sobre la razón por la que Church usa la letra griega lambda (λ) como la 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é 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 clase por Whitehead y Russell , modificando primero " " a "∧ " para distinguir la abstracción de función de la abstracción de clase, y luego cambiar “∧” a “λ” para facilitar la impresión. ${\ Displaystyle {\ hat {x}}}$${\ Displaystyle {\ hat {x}}}$${\ Displaystyle x}$

Este origen también se informó en [Rosser, 1984, p.338]. Por otro lado, en sus últimos años, Church les dijo a dos investigadores que la elección era más accidental: se necesitaba un símbolo y, por casualidad, se eligió λ.

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

Estimado profesor Church,

Russell tenía el operador iota , Hilbert tenía el operador épsilon . ¿Por qué eligió lambda para su 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 el cálculo, lo que permite estudiar formalmente las propiedades del cálculo. El cálculo lambda incorpora dos simplificaciones que simplifican esta semántica. La primera simplificación es que el cálculo lambda trata las funciones de forma "anónima", sin darles nombres explícitos. Por ejemplo, la función

${\ Displaystyle \ operatorname {cuadrado \ _sum} (x, y) = x ^ {2} + y ^ {2}}$

se puede reescribir de forma anónima como

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

(que se lee como "una tupla de x y y se asignan a "). Del mismo modo, la función ${\ textstyle x ^ {2} + y ^ {2}}$

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

se puede reescribir de forma anónima como

${\ Displaystyle x \ mapsto x}$

donde la entrada simplemente se asigna a sí misma.

La segunda simplificación es que el cálculo lambda solo usa funciones de una sola entrada. Una función ordinaria que requiere dos entradas, por ejemplo la función, se puede reelaborar en una función equivalente que acepta una sola entrada y, como salida, devuelve otra función, que a su vez acepta 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 currización , 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 de la función a los argumentos (5, 2), produce a la vez ${\ 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)}$// se ha utilizado la definición de en la expresión interna. Esto es como una reducción β.${\ Displaystyle x}$${\ Displaystyle 5}$

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

${\ textstyle = 29}$

para llegar al mismo resultado.

El cálculo lambda

El cálculo lambda consiste en un lenguaje de términos lambda , que se definen mediante una determinada sintaxis formal, y un conjunto de reglas de transformación, que permiten la manipulación de los términos lambda. Estas reglas de transformación pueden verse como una teoría de ecuaciones o como una definición operativa .

Como se describió anteriormente, todas las funciones en el cálculo lambda son funciones anónimas, sin nombre. Solo aceptan una variable de entrada, y el curry se utiliza para implementar funciones con varias variables.

Términos lambda

La sintaxis del cálculo lambda define algunas expresiones como expresiones válidas de cálculo lambda y otras como inválidas, al igual 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 dan una definición inductiva que se puede aplicar para construir todos los términos lambda sintácticamente válidos:

• una variable, es en sí misma un término lambda válido${\ Displaystyle x}$
• si es un término lambda y es una variable, entonces (a veces escrito en ASCII como ) es un término lambda (llamado abstracción );${\ Displaystyle t}$${\ Displaystyle x}$${\ Displaystyle (\ lambda xt)}$${\ Displaystyle ({\ text {L}} xt)}$
• si y son términos lambda, entonces es un término lambda (llamado aplicación ).${\ Displaystyle t}$${\ Displaystyle s}$${\ Displaystyle (ts)}$

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

Una abstracción es una definición de una función anónima que es capaz de tomar una sola entrada y sustituirla en la expresión . Por tanto, define una función anónima que toma y devuelve . Por ejemplo, es una abstracción para la función que usa el término para . La definición de una función con una abstracción simplemente "configura" la función pero no la invoca. La abstracción une la variable en el término . ${\ Displaystyle \ lambda xt}$${\ Displaystyle x}$${\ Displaystyle t}$${\ Displaystyle x}$${\ Displaystyle t}$${\ Displaystyle \ lambda xx ^ {2} +2}$${\ Displaystyle f (x) = x ^ {2} +2}$${\ Displaystyle x ^ {2} +2}$${\ Displaystyle t}$${\ Displaystyle x}$${\ Displaystyle t}$

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

No hay ningún concepto en el cálculo lambda de declaración de variable. En una definición como (ie ), el cálculo lambda trata como una variable que aún no está definida. La abstracción es sintácticamente válida y representa una función que agrega su entrada a lo aún desconocido . ${\ Displaystyle \ lambda x.x + y}$${\ Displaystyle f (x) = x + y}$${\ Displaystyle y}$${\ Displaystyle \ lambda x.x + y}$${\ Displaystyle y}$

Se pueden usar corchetes y pueden ser necesarios para eliminar la ambigüedad de los términos. Por ejemplo, y denotan diferentes términos (aunque casualmente se reducen al mismo valor). Aquí, el primer ejemplo define una función cuyo término lambda es el resultado de aplicar x a la función secundaria, mientras que el segundo ejemplo es la aplicación de la función más externa a la entrada x, que devuelve la función secundaria. Por tanto, ambos ejemplos evalúan la función identidad . ${\ Displaystyle \ lambda x. ((\ lambda xx) x)}$${\ Displaystyle (\ lambda x. (\ lambda xx)) x}$ ${\ Displaystyle \ lambda xx}$

Funciones que operan en 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, representa la función identidad , y representa la función identidad aplicada a . Además, representa la función constante , la función que siempre regresa , sin importar la entrada. En el cálculo lambda, la aplicación de funciones se considera asociativa por la izquierda , es decir . ${\ Displaystyle \ lambda xx}$${\ Displaystyle x \ mapsto x}$${\ Displaystyle (\ lambda xx) y}$${\ Displaystyle y}$${\ Displaystyle (\ lambda xy)}$ ${\ Displaystyle x \ mapsto y}$${\ Displaystyle y}$${\ displaystyle stx}$${\ Displaystyle (st) x}$

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

Equivalencia alfa

Una forma básica de equivalencia, definible en términos lambda, es la 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, y son términos lambda equivalentes a alfa, y ambos representan la misma función (la función de identidad). Los términos y no son equivalentes alfa, porque no están ligados a una abstracción. En muchas presentaciones, es habitual identificar términos lambda equivalentes a alfa. ${\ Displaystyle \ lambda xx}$${\ Displaystyle \ lambda yy}$${\ Displaystyle x}$${\ Displaystyle y}$

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

Variables libres

Las variables libres 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 inductivamente:

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

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

Sustituciones que evitan la captura

Supongamos , y son términos lambda y e son variables. La notación indica sustitución de para en una captura evitando manera. Esto se define de manera que: ${\ Displaystyle t}$${\ Displaystyle s}$${\ Displaystyle r}$${\ Displaystyle x}$${\ Displaystyle y}$${\ Displaystyle t [x: = r]}$${\ Displaystyle r}$${\ Displaystyle x}$${\ Displaystyle t}$

• ${\ Displaystyle x [x: = r] = r}$;
• ${\ Displaystyle y [x: = r] = y}$si ;${\ Displaystyle x \ neq y}$
• ${\ Displaystyle (ts) [x: = r] = (t [x: = r]) (s [x: = r])}$;
• ${\ Displaystyle (\ lambda xt) [x: = r] = \ lambda xt}$;
• ${\ Displaystyle (\ lambda yt) [x: = r] = \ lambda y. (t [x: = r])}$si y no está en las variables libres de . Se dice que la variable es "fresca" para .${\ Displaystyle x \ neq y}$${\ Displaystyle y}$${\ Displaystyle r}$${\ Displaystyle y}$${\ Displaystyle 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 asegurar que la sustitución no cambie el significado de las funciones. Por ejemplo, una sustitución se hace que ignora la condición de frescura: . Esta sustitución convierte la función constante en la identidad por sustitución. ${\ Displaystyle y}$${\ Displaystyle r}$${\ Displaystyle (\ lambda xy) [y: = x] = \ lambda x. (y [y: = x]) = \ lambda xx}$${\ Displaystyle \ lambda xy}$${\ Displaystyle \ lambda xx}$

En general, el incumplimiento de la condición de frescura puede remediarse mediante un cambio de nombre alfa con una variable de frescura adecuada. Por ejemplo, volviendo a nuestra noción correcta de sustitución, en la abstracción se puede cambiar el nombre con una nueva variable , para obtener , y el significado de la función se conserva por sustitución. ${\ Displaystyle (\ lambda xy) [y: = x]}$${\ Displaystyle z}$${\ Displaystyle (\ lambda zy) [y: = x] = \ lambda z. (y [y: = x]) = \ lambda zx}$

β-reducción

La regla de reducción β establece que una aplicación de la forma se reduce al término . La notación se usa para indicar que β-se 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 xt) s}$${\ Displaystyle t [x: = s]}$${\ Displaystyle (\ lambda xt) s \ to t [x: = s]}$${\ Displaystyle (\ lambda xt) s}$${\ Displaystyle t [x: = s]}$${\ Displaystyle s}$${\ Displaystyle (\ lambda xx) s \ a x [x: = s] = s}$${\ Displaystyle \ lambda xx}$${\ Displaystyle (\ lambda xy) s \ to y [x: = s] = y}$${\ Displaystyle \ lambda xy}$

El cálculo lambda puede verse como una versión idealizada de un lenguaje de programación funcional, como Haskell o Standard ML . Bajo este punto de vista, la reducción β corresponde a un paso computacional. Este paso puede repetirse mediante reducciones β adicionales hasta que no queden más aplicaciones que reducir. En el cálculo lambda sin tipo, 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 sola 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 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.

Definicion formal

Definición

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 .

Notación

Para mantener ordenada la notación de las 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: M N P se puede escribir en lugar de (( M N ) P ).
• 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 .
• Se contrae una secuencia de abstracciones: λ x .λ y .λ z . N se abrevia como λ xyz . N .

Variables libres y ligadas

Se dice que el operador de abstracción, λ, vincula su variable dondequiera que ocurra 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 es a menudo llamado ligante , como un indicio de que la variable x se está obligado añadiendo λ x a M . Todas las demás variables se denominan libres . Por ejemplo, en la expresión λ y . xxy , y es una variable ligada y x es una variable libre. Además, una variable está limitada por su abstracción más cercana. En el siguiente ejemplo, la única aparición de x en la expresión está vinculada por la segunda 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 la estructura de los términos, como sigue:

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

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 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:

• α-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 las 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 subtermos que pueden reducirse mediante una de las reglas de reducción. Por ejemplo, (λ x . M ) N es un β-redex en la expresión de la sustitución de N para x en M . La expresión a la que se reduce un redex se llama su reducto ; la reducción de (λ x . M ) N es M [ x  : = N ].

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

α-conversión

La conversión α, a veces conocida como cambio de nombre α, permite cambiar los nombres de las variables vinculadas. Por ejemplo, α-conversión de λ x . x podría producir λ y . y . Los términos que difieren solo en 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 del todo triviales. Primero, cuando se convierte en α una abstracción, las únicas ocurrencias de variables que se renombran son aquellas que están vinculadas a la misma abstracción. Por ejemplo, una conversión α 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 del 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 con y en λ x .λ y . x , obtenemos λ y .λ y . y , que no es en absoluto lo mismo.

En los lenguajes de programación con alcance estático, la conversión α se puede utilizar para simplificar la resolución de nombres asegurándose de que ningún nombre de variable enmascare un nombre en un alcance contenedor (consulte el cambio de nombre α para hacer que la resolución de nombres sea trivial ).

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

Sustitución

Cambio en el escrito M [ V  : = N ], es el proceso de sustitución de todos los libres ocurrencias de la variable V en la expresión M con la expresión N . La sustitución en términos del cálculo lambda se define por recursividad en la estructura de términos, como sigue (nota: xey 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 . METRO

(λ y . M ) [ x  : = N ] = λ y . ( M [ x  : = N ]), si x ≠ y e y ∉ FV ( N )

Para sustituirlo en una abstracción, a veces es necesario α-convertir la expresión. Por ejemplo, no es correcto que (λ x . Y ) [ y  : = x ] resulte en λ x . x , porque se suponía que la x sustituida era libre, pero acabó ligada. La sustitución correcta en este caso es λ z . x , hasta α-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. β-reducción se define en términos de sustitución: la β-reducción de (λ V . M ) N es M [ V  : = N ].

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

Se puede considerar 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 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 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 .

Formas normales y confluencia

Para el cálculo lambda no tipificado, la reducción β como regla de reescritura no normaliza fuertemente ni normaliza débilmente .

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 términos débilmente normalizados 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 se puede utilizar para modelar valores booleanos, aritméticos , 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 las más comunes son los números de la 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 ))

etcétera. O usando la sintaxis alternativa presentada anteriormente en Notación :

0: = λ fx . X

1: = λ fx . f x

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 f de un solo argumento 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 de identidad. Tales composiciones repetidas (de una sola función f ) obedecen a las leyes de los exponentes , razón por la cual estos números pueden usarse para 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 sobre el número n de la Iglesia , que a menudo es ú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 (vinculada) de n elementos todos iguales ax repitiendo 'anteponer otro elemento x ' n veces, comenzando desde una lista vacía. El término lambda es

λ n .λ x . n (PAR x ) NINGUNO

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

Podemos definir una función sucesora, que toma un número 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 )

Debido a que la m -ésima composición de f compuesta con la n -ésima composición de f da la m + n -ésima composición 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 a β. 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 n 

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

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

Alternativamente

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

desde multiplicando m y n es la misma que la repetición de los add n función de m veces y luego aplicarlo a cero. La exponenciación tiene una interpretació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 )) , 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 que usa condicionales y la otra que usa pares . Con la función predecesora, la resta es sencilla. Definiendo

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

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

Lógica y predicados

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

VERDADERO: = λ x .λ y . X

FALSO: = λ x .λ y . y

(Tenga en cuenta que FALSO es equivalente al número cero de la Iglesia definido anteriormente)

Luego, 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

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

NO: = λ p . p FALSO VERDADERO

SI ENTONCES: = λ p .λ a .λ b . p a b

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

Y VERDAD 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 VERDADERO si su argumento es el número 0 de la Iglesia y FALSO si su argumento es cualquier otro número de la Iglesia:

ISZERO: = λ n . n (λ x .FALSE) VERDADERO

El siguiente predicado prueba 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 TRUE y FALSE hacen que sea conveniente escribir expresiones "if-then-else" en el cálculo lambda. Por ejemplo, la función predecesora se puede definir como:

PRED: = λ n . n (λ g .λ k .ISZERO ( g 1) k (PLUS ( 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.

Pares

Un par (2-tupla) 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 SEGUNDO devuelve el segundo.

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

PRIMERO: = λ p . p VERDADERO

SEGUNDO: = λ p . p FALSO

NULO: = λ x .TRUE

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

Una lista enlazada se puede definir como NIL para la lista vacía o como 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)).

Técnicas de programación adicionales

Existe una cantidad 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 se usan en la programación práctica, pero luego pueden percibirse como oscuras o extrañas.

Constantes nombradas

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 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 se puede emular tener constantes nombradas dejando a un lado una variable como el nombre de la constante, usando la abstracción para vincular esa variable en el cuerpo principal y aplique esa abstracción a la definición deseada. Por lo tanto, para usar f para significar M (algún término lambda explícito) en N (otro término lambda, el "programa principal"), se puede decir

(λ f . N ) M

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

sea f = M en N

Al encadenar tales definiciones, se puede escribir un "programa" de cálculo lambda como cero o más definiciones de función, seguido de un término lambda utilizando esas funciones que constituyen el cuerpo principal del programa.

Una restricción notable de este let es que el nombre f no está definido en M , ya que M está fuera del alcance de la abstracción vinculante f ; esto significa que una definición de función recursiva no se puede usar como M con let . La construcción sintáctica de azúcar más avanzada de letrec que permite escribir definiciones de funciones recursivas en ese estilo ingenuo, emplea además combinadores de punto fijo.

Recurrencia y puntos fijos

La recursividad es la definición de una función que utiliza la propia función. El cálculo lambda no puede expresar esto tan directamente como algunas 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, la recursión todavía se puede conseguir mediante la disposición de una expresión lambda para recibir 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; de lo contrario 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 expresión lambda en sí como su valor, de modo que llamarlo, aplicarlo a un argumento, equivaldrá a una recursividad. Por lo tanto, para lograr la recursividad, el argumento pretendido 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  para mantener, entonces  {{{1}}}  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 volver a escribir cada llamada recursiva como autoaplicación. Nos gustaría tener una solución genérica, sin necesidad de reescrituras:

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

con  r x = F x = G r x  para mantener, entonces  r = G r =: FIX G  y

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

de modo que  FIX G = G (FIX G) = (λ n . (1, if n = 0; else 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 ). 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 llame. Así, 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:

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

(λ altura (λ x . altura ( x x )) (λ x . altura ( 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 ( 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

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; más 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; si no 3 × (( Y G) (3−1)))

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

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

4 × (3 × (1, si 2 = 0; si no 2 × (( Y G) (2−1))))

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

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

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; 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

Cada función definida de forma recursiva puede verse como un punto fijo de alguna función adecuadamente definida que se cierra sobre la llamada recursiva con un argumento adicional y, por lo tanto, utilizando Y , cada función definida de forma recursiva 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 de forma recursiva.

Cláusulas estándar

Ciertos términos tienen nombres comúnmente aceptados:

Yo  : = λ x . X

K  : = λ x .λ y . X

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

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

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

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

U  : = λ x . x x

ω  : = λ x . x x

Ω  : = ω ω

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

Varios de estos tienen aplicaciones directas en la eliminación de la abstracción que convierte los términos lambda en términos de cálculo combinador .

Eliminación de abstracción

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 se puede ver como variables anonimizadas, ya que T ( x , N ) elimina todas las apariciones de x de N , al 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 ): = yo

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 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. Me devuelve ese argumento. K lanza el argumento de distancia, al igual que (λ x . N ) haría si x no tiene ninguna ocurrencia libre en N . S pasa el argumento a ambos subterráneos 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 subtermo de una aplicación ( B al subtermo "argumento" y C al subtermo "función"), ahorrando así un K subsiguiente si no hay ocurrencia de x en un subterráneo. 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 lo último, produciendo el sistema B, C, K, W como una alternativa al cálculo del combinador SKI .

Cálculo lambda mecanografiado

Un cálculo lambda con tipo es un formalismo con tipo que utiliza el símbolo lambda ( ) para denotar la abstracción de funciones anónimas. 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 (consulte Tipos de cálculos lambda tipificados ). Desde cierto punto de vista, los cálculos lambda tipificados pueden verse como refinamientos del cálculo lambda no tipificado, pero desde otro punto de vista, también pueden considerarse la teoría más fundamental y el cálculo lambda no tipificado es un caso especial con un solo tipo. ${\ Displaystyle \ lambda}$

Los cálculos lambda tipificados son lenguajes de programación fundamentales y son la base de los lenguajes de programación funcionales 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; en este caso, la tipificación suele capturar propiedades deseables del programa, por ejemplo, el programa no provocará una infracció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 clases de categorías , por ejemplo, el cálculo lambda simplemente tipificado es el lenguaje de categorías cerradas cartesianas (CCC).

Estrategias de reducción

Si un término se normaliza o no, y cuánto trabajo hay que hacer para normalizarlo, depende en gran medida de la estrategia de reducción utilizada. Las estrategias comunes de reducción del cálculo lambda incluyen:

Orden normal

La redex más a la izquierda y más externa siempre 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.

Orden de aplicación

El redex más a la izquierda y más interno siempre se reduce primero. Intuitivamente, esto significa que los argumentos de una función siempre se reducen antes que la función en sí. El orden aplicativo siempre intenta aplicar funciones a formas normales, incluso cuando esto no es posible.

Reducciones β completas

Cualquier redex puede reducirse 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 canceladas".

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

Llamar por valor

Un redex se reduce solo cuando su lado derecho se ha reducido a un valor (variable o abstracción). Solo se reducen los redexes más externos.

Llamar por nombre

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

Las estrategias con compartir 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.

Llame por necesidad

Como llamada por nombre (por lo tanto débil), pero las aplicaciones de función que duplicarían términos en su lugar nombran el argumento, que luego se reduce solo "cuando es necesario".

Computabilidad

No existe un algoritmo que tome como entrada dos expresiones lambda y dé como resultado VERDADERO o FALSO dependiendo de si una expresión se reduce a la otra. 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 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 sólo si f x  = _β  y , donde x y y son los números Iglesia correspondiente a x y y , respectivamente y = _β 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 demostración del primer teorema de incompletitud de Gödel . 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 complicada, porque el costo de una reducción β puede variar dependiendo de 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 se debe realizar un seguimiento de las ubicaciones de las variables libres de alguna manera, lo que implica un costo de espacio. Una búsqueda naïve para las ubicaciones de V en E es O ( n ) de la longitud n de E . Las cadenas de director fueron un enfoque temprano que intercambió este costo de tiempo por un uso de espacio cuadrático. 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 plazo es un modelo de costo de tiempo razonable , es decir, la reducción se puede simular en una máquina de Turing en tiempo polinomialmente proporcional al número de pasos . 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 soluciona esto trabajando con una representación compartida compacta. El resultado deja en 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 no se sabe cuál sería una buena medida de la complejidad espacial.

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 estar codificada en el cálculo lambda en 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 hacia 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 extremo izquierdo-exterior. Además, la implementación del prototipo BOHM de reducción óptima superó tanto a Caml Light como a Haskell en términos puramente lambda.

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 procedimental secuenciales pueden entenderse en términos del cálculo lambda, que proporciona los mecanismos básicos para la abstracción y el procedimiento procedimentales (subprograma) solicitud.

Funciones anónimas

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

(lambda (x) (* x x))

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)- solo un argumento en este caso, y una expresión que se evalúa como el cuerpo de la función (* x x),. Las funciones anónimas a veces se denominan expresiones lambda.

Por ejemplo, Pascal y muchos otros lenguajes imperativos han soportado 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 está soportada en Smalltalk , JavaScript y Wolfram Language , y más recientemente en 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 β) se puede realizar 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 constructos como Futuros al cálculo lambda. Se han desarrollado otros cálculos de procesos para describir la comunicación y la concurrencia.

Semántica

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

En la década de 1970, Dana Scott demostró que si solo se consideraran funciones continuas, se podrí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 ampliaciones

Estas extensiones están en el cubo lambda :

• Cálculo lambda tipado : cálculo lambda con variables tipadas (y funciones)
• Sistema F : un cálculo lambda tipificado con variables de tipo
• Cálculo de construcciones : un cálculo lambda tipificado 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 del combinador de SKI : un sistema computacional basado en los combinadores S , K e I , equivalente al cálculo lambda, pero reducible sin sustituciones de variables.

Ver también

Notas

Referencias

Otras lecturas

• Abelson, Harold y Gerald Jay Sussman. Estructura e interpretación de programas informáticos . La prensa del MIT . ISBN  0-262-51087-1 .
• Hendrik Pieter Barendregt Introducción al cálculo Lambda .
• Henk Barendregt , El impacto del cálculo lambda en lógica e informática . The Bulletin of Symbolic Logic, Volumen 3, Número 2, junio de 1997.
• Barendregt, Hendrik Pieter , The Type Free Lambda Calculus pp1091-1132 del Handbook of Mathematical Logic , Holanda Septentrional (1977) ISBN  0-7204-2285-X
• Cardone y Hindley, 2006. Historia del cálculo lambda y lógica combinatoria . En Gabbay y Woods (eds.), Handbook of the History of Logic , vol. 5. Elsevier.
• Church, Alonzo, Un problema irresoluble de la 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.
• Iglesia de Alonzo, Los cálculos de conversión de Lambda ( ISBN  978-0-691-08394-0 )
• Frink Jr., Orrin, Revisión: Los cálculos de conversión Lambda
• 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 de cálculo lambda de varias funciones familiares.
• 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 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 y esquema Lambda . Una suave introducción para programadores.
• Schalk, A. y Simmons, H. (2005) Una introducción a los cálculos λ y la aritmética con una selección decente de ejercicios . Notas 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 prueba". Studia Logica . 90 (2): 211–247. doi : 10.1007 / s11225-008-9150-5 . S2CID  11321602 . Un artículo que da un sustento formal a la idea de "significado-es-uso" que, incluso si se basa en pruebas, es diferente de la semántica de la teoría de la prueba como en la tradición Dummett-Prawitz, ya que toma la reducción como las reglas que dan significado.
• Hankin, Chris, Introducción a los cálculos Lambda para informáticos, ISBN  0954300653

Monografías / libros de texto para estudiantes de posgrado:

• Morten Heine Sørensen, Paweł Urzyczyn, Lectures on the Curry-Howard isomorphism , Elsevier, 2006, ISBN  0-444-52077-5 es una monografía reciente que cubre los principales temas del cálculo lambda desde la variedad libre de tipos hasta la mayoría de lambda tipificada. cálculos , incluidos desarrollos más recientes como los sistemas de tipos puros y el cubo lambda . No cubre las extensiones de subtipo .
• 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 el subtipo es un tema importante.

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

enlaces externos

• Graham Hutton, Lambda Calculus , un video corto (12 minutos) Computerphile sobre el Lambda Calculus
• Helmut Brandl, Introducción paso a paso al cálculo Lambda
• "Lambda-calculus" , Enciclopedia de Matemáticas , EMS Press , 2001 [1994]
• Achim Jung, una breve introducción al cálculo Lambda - ( PDF )
• Dana Scott, Una línea de tiempo del cálculo lambda - ( PDF )
• David C.Keenan, Diseccionar un ruiseñor: una notación gráfica para el cálculo lambda con reducción animada
• Raúl Rojas, Tutorial de introducción al cálculo Lambda - ( PDF )
• Peter Selinger, Notas de la conferencia sobre el cálculo Lambda - ( PDF )
• L. Allison, Algunos ejemplos ejecutables de cálculo λ
• Georg P. Loczewski, El cálculo Lambda y A ++
• Bret Victor, Alligator Eggs: un juego de rompecabezas basado en el cálculo Lambda
• Cálculo Lambda en el sitio web de Safalra
• LCI Lambda Interpreter un intérprete de cálculo puro simple pero potente
• Enlaces de Lambda Calculus en Lambda-the-Ultimate
• Mike Thyer, Lambda Animator , un subprograma Java gráfico que demuestra estrategias de reducción alternativas.
• Implementación del cálculo de Lambda mediante plantillas C ++
• Marius Buliga, cálculo lambda gráfico
• 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 lapropiedad Church-Rosser , que permite lareducción de gráficos paralelos para expresiones lambda).
• Shane Steinert-Threlkeld, "Lambda Calculi" , Enciclopedia de Filosofía de Internet
• Anton Salikhmetov, cálculo macro lambda