La Enciclopedia Libre Universal en Español dispone de una lista de distribución pública, enciclo@listas.us.es
Cálculo lambda
Artículo de la Enciclopedia Libre Universal en Español.
El cálculo lambda es un formalismo para representar funciones, cuyo poder expresivo es equivalente a la máquina de Turing universal.
El cálculo lambda trabaja con objetos llamados lambda-términos, que son cadenas de símbolos de una de las formas siguientes:
- v
- λv.E1
- (E1 E2)
donde v es un nombre de variable tomado de un conjunto infinito predefinido de nombres de variables, y E1 y E2 son lambda-términos. Los términos de la forma λv.E1 son llamadas abstracciones. La variable ν se llama el parámetro formal de la abstracción, y E1 es el cuerpo de la abstracción.
El término λv.E1 representa la función que, si es aplicada a un argumento, liga el parámetro formal v al argumento y entonces computa el valor resultante de E1--- esto es, retorna E1, con cada ocurrencia de ν sustituido por el argumento.
Los términos de la forma (E1 E2) son llamados aplicaciones. Las aplicaciones modelan la invocación o ejecución de una función: La función representada por E1 es invocada, con E2 como su argumento, y se computa el resultado. Si E1 (a veces llamado el aplicando) es una abstracción, el término puede ser reducido: E2, el argumento, se puede sustituir en el cuerpo de E1 en lugar del parámetro formal de E1, y el resultado es un nuevo término lambda que es equivalente al antiguo. Si un término lambda no contiene ningún subtérmino de la forma (λv.E1 E2) entonces no puede ser reducido, y se dice que está en forma normal.
La expresión E[a/v] representa el resultado de tomar el término E y sustituir todas las ocurrencias libres de v por a:
(λv.E a) => E[a/v]
por convención tomamos (a b c d ... z) como abreviatura para (... (((a b) c) d)... z). (Regla de asociación por izquierda).
La motivación para esta definición de la reducción es que captura el comportamiento esencial de todas las funciones matemáticas. Por ejemplo, considérese la función que computa el cuadrado de un número. Se puede escribir el cuadrado de x es x*x (usando "*" para indicar la multiplicación.) x aquí es el parámetro formal de la función. Para evaluar el cuadrado para un argumento particular, digamos 3, lo insertamos en la definición en lugar del parámetro formal:
El cuadrado de 3 es 3*3
para evaluar la expresión que resulta 3*3, tendríamos que recurrir a nuestro conocimiento de la multiplicación y del número 3. Puesto que cualquier cómputo es simplemente una composición de la evaluación de funciones adecuadas con argumentos primitivos adecuados, este principio simple de sustitución es suficiente para capturar el mecanismo esencial del cómputo. Por otra parte, en el cálculo lambda, nociones tales como '3' y '*' puede ser representado sin ninguna necesidad de operadores primitivos externamente definidos o de constantes. Es posible identificar los términos que en el cálculo lambda, cuando están interpretados convenientemente, se comportan como el número 3 y el operador de la multiplicación.
El cálculo lambda es computacionalmente equivalente en poder a muchos otros modelos plausibles para el cómputo (máquinas de Turing incluídas); es decir, cualquier cálculo que se pueda lograr en cualesquiera de estos otros modelos se puede expresar en el cálculo lambda y viceversa. Según la tesis de Church-Turing, ambos modelos pueden expresar cualquier cómputo posible.
Quizás parezca sorprendente que el cálculo lambda pueda representar cualquier cómputo concebible usando solamente las nociones simples de abstracción funcional y aplicación basado en la substitución textual simple de términos por variables. Pero aún más notable es que incluso la abstracción no es requerible: la lógica combinatoria es un modelo del cómputo equivalente al cálculo lambda, pero sin la abstracción.
