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:
Sintaxis | Nombre | Descripción |
---|---|---|
X | Variable | Carácter o cadena que representa un parámetro o valor matemático / lógico. |
(λ x . M ) | Abstracción | Definición de función ( M es un término lambda). La variable x se une a la expresión. |
( M N ) | Solicitud | Aplicar una función a un argumento. M y N son términos lambda. |
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:
Operación | Nombre | Descripción |
---|---|---|
(λ x . M [ x ]) → (λ y . M [ y ]) | α-conversión | Cambiar el nombre de las variables vinculadas en la expresión. Se usa para evitar colisiones de nombres . |
((λ x . M ) E ) → ( M [ x : = E ]) | β-reducción | Reemplazo de las variables vinculadas con la expresión del argumento en el cuerpo de la abstracción. |
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 . [1] 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 , [2] lingüística , [3] [4] e informática . [5] 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 . [6]
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 . [7] [a] Se demostró que el sistema original era lógicamente inconsistente en 1935 cuando Stephen Kleene y JB Rosser desarrollaron la paradoja de Kleene-Rosser . [8] [9]
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. [10] En 1940, también introdujo un sistema computacionalmente más débil, pero lógicamente consistente, conocido como el cálculo lambda simplemente tipado . [11]
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 [12] como en informática. [13]
Origen del símbolo lambda
Existe cierta controversia 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 “"Utilizado para la abstracción de clases por Whitehead y Russell , modificando primero""A" ∧”Para distinguir la abstracción de funciones de la abstracción de clases, y luego cambiar“ ∧ ”a“ λ ”para facilitar la impresión.
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 controversia en varias conferencias públicas. [14] Scott cuenta 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
se puede reescribir de forma anónima como
(que se lee como "una tupla de x y y se asignan a"). Del mismo modo, la función
se puede reescribir de forma anónima como
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, lafunció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,
se puede reelaborar en
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.
Aplicación de la función del función a los argumentos (5, 2), produce a la vez
- ,
mientras que la evaluación de la versión al curry requiere un paso más
- // la definición de ha sido usado con en la expresión interior. Esto es como una reducción β.
- // la definición de ha sido usado con . Nuevamente, similar a la reducción β.
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í mismo un término lambda válido
- 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 );
- Si y son términos lambda, entonces es un término lambda (llamado aplicación ).
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 abstraccion es una definición de una función anónima que es capaz de tomar una sola entrada y sustituyéndolo en la expresión . Por tanto, define una función anónima que toma y vuelve . Por ejemplo, es una abstracción de la función usando el término por . 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 plazo .
Una aplicación representa la aplicación de una función a una entrada , es decir, representa el acto de llamar a la función en la entrada para producir .
No hay ningún concepto en el cálculo lambda de declaración de variable. En una definición como (es decir ), el cálculo lambda trata como una variable que aún no está definida. La abstraccion es sintácticamente válido y representa una función que agrega su entrada a la aún desconocida .
Se pueden usar corchetes y pueden ser necesarios para eliminar la ambigüedad de los términos. Por ejemplo, y denotan términos diferentes (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 lo tanto, ambos ejemplos evalúan la función de identidad .
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 de identidad ,, y representa la función de identidad aplicada a . Más,representa la función constante , la función que siempre devuelve , no importa la entrada. En el cálculo lambda, la aplicación de funciones se considera asociativa a la izquierda , de modo que medio .
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 alfa-equivalentes y ambos representan la misma función (la función de identidad). Los términos y no son equivalentes alfa, porque no están vinculados a una abstracción. En muchas presentaciones, es habitual identificar términos lambda equivalentes a alfa.
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
- El conjunto de variables libres de es el conjunto de variables libres de , pero con remoto
- El conjunto de variables libres de es la unión del conjunto de variables libres de y el conjunto de variables libres de .
Por ejemplo, el término lambda que representa la identidad no tiene variables libres, pero la función tiene una única variable libre, .
Sustituciones que evitan la captura
Suponer , y son términos lambda y y son variables. La notación indica sustitución de por en en una captura evitando manera. Esto se define de modo que:
- ;
- Si ;
- ;
- ;
- Si y no está en las variables libres de . La variable se dice que es "fresco" para .
Por ejemplo, , y .
La condición de frescura (que requiere que no está en las variables libres de ) es crucial para garantizar que la sustitución no cambie el significado de las funciones. Por ejemplo, se realiza una sustitución que ignora la condición de frescura:. Esta sustitución convierte la función constante en la identidad por sustitución.
En general, el incumplimiento de la condición de frescura puede remediarse mediante un cambio de nombre alfa con una variable fresca adecuada. Por ejemplo, volviendo a nuestra noción correcta de sustitución, en la abstracción se puede renombrar con una nueva variable , para obtener , y el significado de la función se conserva mediante sustitución.
β-reducción
La regla de reducción β establece que una aplicación de la forma se reduce al término . La notación se utiliza para indicar que β-se reduce a . Por ejemplo, para cada, . Esto demuestra querealmente es la identidad. Similar,, lo que demuestra que es una función constante.
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á.
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 1 , v 2 , ...;
- los símbolos de abstracción λ (lambda) y. (punto);
- paréntesis ().
El conjunto de expresiones lambda, Λ, se puede definir inductivamente :
- Si x es una variable, entonces x ∈ Λ.
- Si x es una variable y M ∈ Λ, entonces (λ x . M ) ∈ Λ.
- 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 . [15] [16]
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 ). [17]
- 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 . [18] [17]
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:
- FV ( x ) = { x }, donde x es una variable.
- FV (λ x . M ) = FV ( M ) \ { x }.
- FV ( MN ) = FV ( M ) ∪ FV ( N ). [19]
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. [20]
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 subtermas 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
α-conversión, a veces conocida como α-cambio de nombre, [21] 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 1 M 2 ) [ x : = N ] = ( M 1 [ x : = N ]) ( M 2 [ 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 considerar 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 no 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 ))
y así. 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 la Iglesia es una función de orden superior ; se necesita una función de un solo argumento f , y devuelve otra función de un solo argumento. El numeral de la Iglesia n es una función que toma una función f como argumento y devuelve el n -ésima composición de f , es decir, la función F compuesto consigo mismo n veces. Esto se denota f ( n ) y es de hecho el n -ésimo poder de f (considerado como operador); f (0) se define como la función de identidad. Tales composiciones repetidas (de una sola función f ) obedecer las leyes de los exponentes , razón por la cual estos numerales se pueden usar para aritmética. (En el cálculo lambda original de Church, se requería que el parámetro formal de una expresión lambda ocurriera al menos una vez en el cuerpo de la función, lo que hizo que la definición anterior de 0 imposible.)
Una forma de pensar en el numeral de la Iglesia n , que a menudo es útil al analizar programas, es como una instrucción 'repetir n veces'. Por ejemplo, usando el PAREJA y Sin funciones 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 la función que se repite, se pueden lograr muchos efectos diferentes.
Podemos definir una función de sucesor, que toma un número de Iglesia ny regresa 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 )
Porque el m -ésima composición de f compuesto con el 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:
- 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 β. Desde que agrego m a un número n se puede lograr agregando 1 m veces, una definición alternativa es:
- MÁS: = λ m .λ n . m SUCC n [22]
De manera similar, la multiplicación se puede definir como
- MULT: = λ m .λ n .λ f . m ( n f ) [18]
Alternativamente
- MULT: = λ m .λ n . m (MÁS n ) 0
desde multiplicar m y n es lo mismo que repetir la suma n función m veces y luego aplicándolo 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 [19]
La función predecesora definida por PRED n = n - 1 para un número 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 )
puede validarse mostrando inductivamente que si T denota (λ g .λ h . h ( g f )) , luego T ( n ) (λ u . X ) = (λ h . H ( f ( n −1) ( x ))) para n > 0 . Otras dos definiciones de Los PRED se dan a continuación, uno usando condicionales y el otro usando pares . Con la función predecesora, la resta es sencilla. Definiendo
- SUB: = λ m .λ n . n PRED m ,
SUB m n rendimientos m - n cuando m > n y 0 de lo 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 FALSE 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 vuelve VERDADERO si su argumento es el numeral de la Iglesia 0 , y FALSO si su argumento es cualquier otro numeral 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 desde 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 FALSE hace que sea conveniente escribir expresiones "si-entonces-si no" en 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
que se puede verificar mostrando inductivamente que n (λ g .λ k .ISZERO ( g 1) k (PLUS ( g k ) 1)) (λ v .0) es la suma n - 1 función 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 Pruebas NULL para el valor NULO . (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 mapea ( 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 suelen introducir azúcar sintáctico , como vamos , para permitir escribir lo anterior en el orden más intuitivo
- sea f = Men 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 deja es que el nombre f no está definido en M , ya que M está fuera del alcance del enlace de abstracción f ; esto significa que una definición de función recursiva no se puede utilizar como M con dejar . El mas avanzado La construcción sintáctica de azúcar letrec que permite escribir definiciones de funciones recursivas en ese estilo ingenuo en su lugar 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 recursividad aún se puede lograr organizando 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 factorialF ( n ) definido de forma recursiva 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 autorreferencia (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 )
- así que eso FIX G = G (FIX G) = (λ n . (1, si n = 0; de lo contrario n × ((FIX G) ( n −1))))
Dado un término lambda con el primer argumento que representa una llamada recursiva (p. Ej. G aquí), el combinador de punto fijoFIX 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í mismo, en el punto de llamada, logrando una autorreferencia .
De hecho, hay muchas definiciones posibles para este Operador FIX , siendo el 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; de lo contrario 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; si no 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, se usa 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
Algunos términos tienen nombres comúnmente aceptados: [ cita requerida ]
- 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 posiblemente contiene constantes nombradas ( combinadores ), entonces existe un término lambda T ( x , N ) que es equivalente a λ x . N pero carece de abstracción (excepto como parte de las constantes nombradas, si estas se consideran no atómicas). Esto también puede verse como variables anonimizadas, como T ( x , N ) elimina todas las apariciones de x de N , mientras que aún permite que los valores de los argumentos se sustituyan en las posiciones donde N contiene un 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 puede reducir haciendo que el combinador inicial I , K o S tome el argumento P , al igual que la reducción β de (λ x . N) P haría. Me devuelve ese argumento. K descarta el argumento, al igual que (λ x . N) haría si x 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 de "argumento" y C al subtermo de "función"), ahorrando así un K subsiguiente si no hay ocurrencia de x en un subterráneo. En comparación con B y C , elcombinador S en realidad combina dos funcionalidades: reorganizar argumentos y duplicar un argumento para que pueda usarse en dos lugares. Elcombinador W solo hace lo último, produciendo el sistema B, C, K, W como una alternativa al cálculo del combinador SKI .
Cálculo lambda tipificado
Un cálculo lambda escrito es un formalismo escrito que usa 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. [23]
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).
Funciones computables y 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 fx = β y , donde x y y son los números de la Iglesia correspondientes ax e y , respectivamente y = β que significa equivalencia con β-reducción. Ésta es una de las muchas formas de definir la computabilidad; ver la tesis de Church-Turing para una discusión de otros enfoques y su equivalencia.
Indecidibilidad de equivalencia
No hay ningún algoritmo que tome como entrada dos expresiones lambda y salidas VERDADERO o FALSO dependiendo de si las dos expresiones son equivalentes o no. [10] Más precisamente, ninguna función computable puede decidir la equivalencia. 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 .
La prueba de Church primero reduce el problema a determinar si una expresión lambda dada tiene una forma normal . Una forma normal es una expresión equivalente que no se puede reducir más bajo las reglas impuestas por la forma. 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, resulta una contradicción.
Cálculo lambda y lenguajes de programación
Como se señala en el artículo de 1965 de Peter Landin "A Correspondence between ALGOL 60 and Church's Lambda-notation", [24] 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) aplicación.
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 lambda
crea una función anónima, dada una lista de nombres de parámetros; (x)
en este caso, solo un argumento y una expresión que se evalúa como el cuerpo de la función (* x 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.
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. La distinción entre estrategias de reducción se relaciona con la distinción en lenguajes de programación funcionales entre evaluación ansiosa y evaluación perezosa .
- 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".
- 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.
- La mayoría de los lenguajes de programación (incluidos Lisp, ML y lenguajes imperativos como C y Java ) se describen como "estrictos", lo que significa que las funciones aplicadas a argumentos que no se normalizan no se normalizan. Esto se hace esencialmente usando el orden aplicativo, llamado por reducción de valor ( ver más abajo ), pero generalmente llamado "evaluación ansiosa".
- Orden normal
- El redex más a la izquierda y más externo 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.
- Llamar por valor
- Solo se reducen los redex más externos: un redex se reduce solo cuando su lado derecho se ha reducido a un valor (variable o abstracción).
- 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 .
- Llame por necesidad
- Como orden normal, pero las aplicaciones funcionales que duplicarían términos en su lugar nombran el argumento, que luego se reduce solo "cuando es necesario". Denominado en contextos prácticos "evaluación perezosa". En las implementaciones, este "nombre" toma la forma de un puntero, con el redex representado por un thunk .
El orden de aplicación no es una estrategia de normalización. El contraejemplo habitual es el siguiente: define Ω = ωω donde ω = λ x . xx . Esta expresión completa contiene solo un redex, a saber, la expresión completa; su reducción es de nuevo Ω . Dado que esta es la única reducción disponible, Ω no tiene una forma normal (bajo ninguna estrategia de evaluación). Usando orden aplicativo, la expresión KIΩ = (λ x .λ y . X ) (λ x . X ) Ω se reduce reduciendo primero Ω a la forma normal (ya que es el redex más a la derecha), pero desde Ω no tiene forma normal, el orden aplicativo no encuentra una forma normal para KIΩ .
Por el contrario, el orden normal se llama así porque siempre encuentra una reducción normalizadora, si existe. En el ejemplo anterior, KIΩ se reduce en orden normal a I , una forma normal. Un inconveniente es que los redexs en los argumentos se pueden copiar, lo que da como resultado un cálculo duplicado (por ejemplo, (λ x . xx ) ((λ x . x ) y ) se reduce a ((λ x . x ) y ) ((λ x . x ) y ) usando esta estrategia; ahora hay dos redexs, por lo que la evaluación completa necesita dos pasos más, pero si el argumento se hubiera reducido primero, ahora no habría ninguno).
La compensación positiva de usar el orden aplicativo es que no causa cálculos innecesarios, si se usan todos los argumentos, porque nunca sustituye los argumentos que contienen redexes y, por lo tanto, nunca necesita copiarlos (lo que duplicaría el trabajo). En el ejemplo anterior, en orden de aplicación (λ x . xx ) ((λ x . x ) y ) se reduce primero a (λ x . xx ) y y luego al orden normal yy , dando dos pasos en lugar de tres.
La mayoría de los lenguajes de programación puramente funcionales (en particular Miranda y sus descendientes, incluido Haskell), y los lenguajes de prueba de los probadores de teoremas , utilizan la evaluación perezosa , que es esencialmente lo mismo que llamar por necesidad. Esto es como la reducción de pedidos normal, pero la llamada por necesidad logra evitar la duplicación de trabajo inherente a la reducción de pedidos normal mediante el uso compartido . En el ejemplo anterior, (λ x . xx ) ((λ x . x ) y ) se reduce a ((λ x . x ) y ) ((λ x . x ) y ) , que tiene dos redexes, pero en la llamada por necesidad se representan utilizando el mismo objeto en lugar de copiarse, por lo que cuando uno se reduce el otro también.
Una nota sobre la complejidad
Si bien la idea de la reducción β parece bastante simple, no es un paso atómico, ya que debe tener un costo no trivial al estimar la complejidad computacional . [25] 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 estas ubicaciones 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 . Esto ha llevado al estudio de sistemas que utilizan la sustitución explícita . Las cadenas de director de Sinot [26] ofrecen una forma de rastrear las ubicaciones de las variables libres en expresiones.
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.
Reducción óptima
En el artículo de 1988 de Lévy " Compartir en la evaluación de expresiones lambda ", define una noción de intercambio óptimo, de modo que no se duplica ningún trabajo . Por ejemplo, realizar una reducción β en orden normal en (λ x . xx ) (II) lo reduce a II (II) . El argumento II está duplicado por la aplicación al primer término lambda. Si la reducción se realizó primero en un orden de aplicación, ahorramos trabajo porque el trabajo no se duplica: (λ x . xx ) (II) se reduce a (λ x . xx ) I . Por otro lado, el uso del orden aplicativo puede resultar en reducciones redundantes o incluso posiblemente nunca reducirse a la forma normal. Por ejemplo, realizar una reducción β en orden normal en (λ f .f I) (λy. (λ x . xx ) (y I)) produce (λy. (λ x . xx ) (y I)) Yo , (λ x . xx ) (II) que sabemos que podemos hacer sin duplicar el trabajo. Haciendo lo mismo, pero en orden aplicativo, se obtiene (λ f .f I) (λy.y I (y I)) , (λy.y I (y I)) Yo , II (II) , y ahora se duplica el trabajo.
Lévy muestra la existencia de términos lambda donde no existe una secuencia de reducciones que los reduzca sin duplicar el trabajo. El siguiente término lambda es un ejemplo.
((λg. (g (g (λx.x)))) (λh. ((λf. (f (f (λz.z)))) (λw. (h (w (λy.y)))) )))
Está compuesto por tres términos similares, x = ((λg. ...) (λh.y)) y y = ((λf. ...) (λw.z)) , y finalmente z = λw. (h (w (λy.y))) . Aquí solo se pueden hacer dos posibles reducciones β, en x y en y. Reducir el término x externo primero da como resultado que el término y interno se duplique, y cada copia tendrá que reducirse, pero reducir primero el término y interno duplicará su argumento z, lo que hará que el trabajo se duplique cuando los valores de h y w se dan a conocer. Por cierto, el término anterior se reduce a la función de identidad (λy.y) , y se construye haciendo envoltorios que hacen que la función de identidad esté disponible para los aglutinantes g = λh ... , f = λw ... , h = λx.x (al principio), y w = λz.z (al principio), todos los cuales se aplican al término más interno λy.y .
La noción precisa de trabajo duplicado se basa en advertir que después de la primera reducción de Ya está hecho, el valor de la otra II se puede determinar porque tienen la misma estructura (y de hecho tienen exactamente los mismos valores) y son el resultado de un ancestro común. A cada una de estas estructuras similares se le puede asignar una etiqueta que se puede rastrear a través de las reducciones. Si se asigna un nombre al redex que produce todos los resultados II términos, y luego todas las apariciones duplicadas de II se puede rastrear y reducir de una vez. Sin embargo, no es obvio que un redex produzca el II plazo. Identificar las estructuras que son similares en diferentes partes de un término lambda puede involucrar un algoritmo complejo y posiblemente puede tener una complejidad igual al historial de la reducción en sí.
Si bien Lévy define la noción de intercambio óptimo, no proporciona un algoritmo para hacerlo. En el artículo Lambdascope de Vincent van Oostrom, Kees-Jan van de Looij y Marijn Zwitserlood : otra implementación óptima del cálculo lambda , proporcionan tal algoritmo al transformar términos lambda en redes de interacción , que luego se reducen. En términos generales, la reducción resultante es óptima porque cada término que tendría las mismas etiquetas que el artículo de Lévy también sería el mismo gráfico en la red de interacción. En el documento, mencionan que la implementación de su prototipo de Lambdascope funciona tan bien como la versión optimizada de la máquina de referencia óptima de orden superior BOHM. [B]
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 de 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
- Sistemas de computación aplicativos - Tratamiento de objetos al estilo del cálculo lambda
- Categoría cerrada cartesiana : un ajuste para el cálculo lambda en la teoría de categorías
- Máquina abstracta categórica : un modelo de cálculo aplicable al cálculo lambda
- Isomorfismo de Curry-Howard : la correspondencia formal entre programas y pruebas
- Índice de Bruijn : notación que elimina la ambigüedad de las conversiones alfa
- Notación de Bruijn - notación usando funciones de modificación de sufijo
- Cálculo lambda deductivo : la consideración de los problemas asociados con considerar el cálculo lambda como un sistema deductivo .
- Teoría de dominio : estudio de ciertos posets que dan semántica denotacional para el cálculo lambda
- Estrategia de evaluación - Reglas para la evaluación de expresiones en lenguajes de programación.
- Sustitución explícita : la teoría de la sustitución, como se usa en la reducción β
- Programación funcional
- Fórmula de Harrop : una especie de fórmula lógica constructiva tal que las pruebas son términos lambda
- Redes de interacción
- Paradoja de Kleene-Rosser : una demostración de que alguna forma de cálculo lambda es inconsistente
- Knights of the Lambda Calculus : una organización semificticia de piratas informáticos LISP y Scheme
- Krivine machine : una máquina abstracta para interpretar la llamada por nombre en el cálculo lambda
- Definición de cálculo lambda: definición formal del cálculo lambda.
- Let expression : una expresión estrechamente relacionada con una abstracción.
- Minimalismo (informática)
- Reescritura - Transformación de fórmulas en sistemas formales
- Máquina SECD : una máquina virtual diseñada para el cálculo lambda
- Teorema de Scott-Curry : un teorema sobre conjuntos de términos lambda
- Para burlarse de un ruiseñor : una introducción a la lógica combinatoria
- Máquina universal de Turing : una máquina informática formal que es equivalente al cálculo lambda
- Unlambda : un lenguaje de programación funcional esotérico basado en lógica combinatoria
Notas
- ↑ Para obtener una historia completa, consulte "Historia del cálculo Lambda y la lógica combinatoria" de Cardone y Hindley (2006).
- ^ Se pueden encontrar más detalles en el artículo breve Acerca de la reducción eficiente de términos lambda .
Referencias
- ^ Turing, Alan M. (diciembre de 1937). "Computabilidad y λ-definibilidad". El diario de la lógica simbólica . 2 (4): 153-163. doi : 10.2307 / 2268280 . JSTOR 2268280 .
- ^ Coquand, Thierry . Zalta, Edward N. (ed.). "Teoría de tipos" . La Enciclopedia de Filosofía de Stanford (edición de verano de 2013) . Consultado el 17 de noviembre de 2020 .
- ^ Moortgat, Michael (1988). Investigaciones categóricas: aspectos lógicos y lingüísticos del cálculo de Lambek . Publicaciones Foris. ISBN 9789067653879.
- ^ Bunt, Harry; Muskens, Reinhard, eds. (2008). Computación del significado . Saltador. ISBN 978-1-4020-5957-5.
- ^ Mitchell, John C. (2003). Conceptos en lenguajes de programación . Prensa de la Universidad de Cambridge. pag. 57. ISBN 978-0-521-78098-8..
- ^ Pierce, Benjamin C. Teoría de categorías básicas para informáticos . pag. 53.
- ^ Iglesia, Alonzo (1932). "Un conjunto de postulados para la fundación de la lógica". Annals of Mathematics . Serie 2. 33 (2): 346–366. doi : 10.2307 / 1968337 . JSTOR 1968337 .
- ^ Kleene, Stephen C .; Rosser, JB (julio de 1935). "La inconsistencia de ciertas lógicas formales". Los anales de las matemáticas . 36 (3): 630. doi : 10.2307 / 1968646 . JSTOR 1968646 .
- ^ Iglesia, Alonzo (diciembre de 1942). "Revisión de Haskell B. Curry, la inconsistencia de ciertas lógicas formales ". El diario de la lógica simbólica . 7 (4): 170-171. doi : 10.2307 / 2268117 . JSTOR 2268117 .
- ^ a b Iglesia, Alonzo (1936). "Un problema irresoluble de la teoría de números elementales". Revista Estadounidense de Matemáticas . 58 (2): 345–363. doi : 10.2307 / 2371045 . JSTOR 2371045 .
- ^ Iglesia, Alonzo (1940). "Una formulación de la sencilla teoría de tipos". Revista de lógica simbólica . 5 (2): 56–68. doi : 10.2307 / 2266170 . JSTOR 2266170 .
- ^ Partee, BBH; ter Meulen, A .; Wall, RE (1990). Métodos matemáticos en lingüística . Saltador. ISBN 9789027722454. Consultado el 29 de diciembre de 2016 .
- ^ Alma, Jesse. Zalta, Edward N. (ed.). "El cálculo Lambda" . La Enciclopedia de Filosofía de Stanford (edición de verano de 2013) . Consultado el 17 de noviembre de 2020 .
- ^ Dana Scott, " Looking backward; Looking Forward ", charla invitada en el taller en honor al 85 cumpleaños de Dana Scott y los 50 años de teoría del dominio, 7-8 de julio, FLoC 2018 (charla el 7 de julio de 2018). El pasaje relevante comienza en 32:50 . (Véase también este extracto de una charla de mayo de 2016 en la Universidad de Birmingham, Reino Unido).
- ^ Barendregt, Hendrik Pieter (1984). El cálculo lambda: su sintaxis y semántica . Estudios de Lógica y Fundamentos de las Matemáticas. 103 (Ed. Revisada). Holanda Septentrional. ISBN 0-444-87508-5.
- ^ Correcciones .
- ^ a b "Ejemplo de reglas de asociatividad" . Lambda-bound.com . Consultado el 18 de junio de 2012 .
- ^ a b Selinger, Peter (2008), Lecture Notes on the Lambda Calculus (PDF) , 0804 , Departamento de Matemáticas y Estadística, Universidad de Ottawa, p. 9, arXiv : 0804.3434 , Bibcode : 2008arXiv0804.3434S
- ^ a b Barendregt, Henk ; Barendsen, Erik (marzo de 2000), Introducción al cálculo Lambda (PDF)
- ^ de Queiroz, Ruy JGB (1988). "Una explicación teórica de la prueba de la programación y el papel de las reglas de reducción". Dialectica . 42 (4): 265-282. doi : 10.1111 / j.1746-8361.1988.tb00919.x .
- ^ Turbak, Franklyn; Gifford, David (2008), Conceptos de diseño en lenguajes de programación , MIT press, p. 251, ISBN 978-0-262-20175-9
- ^ Felleisen, Matthias; Flatt, Matthew (2006), Lenguajes de programación y cálculos Lambda (PDF) , p. 26, archivado desde el original (PDF) el 2009-02-05; Una nota (consultada en 2017) en la ubicación original sugiere que los autores consideran que el trabajo al que se hace referencia originalmente ha sido reemplazado por un libro.
- ^ Tipos y lenguajes de programación, p. 273, Benjamín C. Pierce
- ^ Landin, PJ (1965). "Una correspondencia entre ALGOL 60 y notación Lambda de Church". Comunicaciones de la ACM . 8 (2): 89–101. doi : 10.1145 / 363744.363749 . S2CID 6505810 .
- ^ Statman, Richard (1979). "El cálculo λ escrito no es recursivo elemental" . Informática Teórica . 9 (1): 73–81. doi : 10.1016 / 0304-3975 (79) 90007-0 . hdl : 2027,42 / 23535 .
- ^ Sinot, F.-R. (2005). "Director cadenas revisadas: un enfoque genérico para la representación eficiente de variables libres en reescritura de orden superior" . Revista de Lógica y Computación . 15 (2): 201–218. doi : 10.1093 / logcom / exi010 .[ enlace muerto permanente ]
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 ) [1]
- Frink Jr., Orrin, Revisión: Los cálculos de conversión de Lambda [2]
- 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, Conferencias sobre el isomorfismo Curry-Howard , Elsevier, 2006, ISBN 0-444-52077-5 es una monografía reciente que cubre los temas principales del cálculo lambda desde la variedad sin tipo hasta la mayoría de los cálculos lambda tipificados , 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 cálculo de Lambda 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 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
- ^ Iglesia, Alonzo (1941). Los cálculos de conversión lambda . Princeton: Prensa de la Universidad de Princeton . Consultado el 14 de abril de 2020 .
- ^ Frink Jr., Orrin (1944). "Revisión: los cálculos de conversión de lambda por la iglesia de Alonzo" (PDF) . Toro. Amer. Matemáticas. Soc . 50 (3): 169-172. doi : 10.1090 / s0002-9904-1944-08090-7 .