3.1 Tipos de lógica combinatoria y características

Puesto que la abstracción es la única manera de fabricar funciones en el cálculo lambda, algo debe substituirlo en el cálculo combinatorio. En vez de la abstracción, el cálculo combinatorio proporciona un conjunto limitado de funciones primitivas y de las cuales las otras funciones pueden ser construidas.
[escribe]Términos combinatorios
Un término combinatorio tiene una de las formas siguientes:
  • V
  • P
  • (E1 E2)
donde V es una variable, P es una de las funciones primitivas, E1 y E2 son términos combinatorios. Las funciones primitivas mismas son combinadores, o funciones que no contienen ninguna variable libre.

La igualdad extensional
La igualdad extensional captura la noción matemática de la igualdad de funciones: que dos funciones son 'iguales' si producen siempre los mismos resultados para las mismos argumentos. En contraste, los términos mismos capturan la noción de igualdad intensional de funciones: que dos funciones son 'iguales' solamente si tienen implementaciones idénticas. Hay muchas maneras de implementar una función identidad; (S K K) y I están entre estas maneras. (S K S) es otro. Utilizaremos la palabra equivalente para indicar la igualdad extensional, reservando igual para los términos combinatorios idénticos.
Un combinador más interesante es el combinador de punto fijo o combinator Y, que se puede utilizar para implementar la recursión.


Completitud de la base S-K
Es, quizás, un hecho asombroso que S y K se puedan componer para producir los combinadores que son extensionalmente iguales a cualquier término lambda, y por lo tanto, por la tesis de Church, a cualquier función computable. La prueba es presentar una transformación, T[ ], que convierte un término arbitrario lambda en un combinador equivalente. T[ ] puede ser definido como sigue: T[V] => V T[(E1 E2)] => (T[E1] T[E2]) T[λx.E] => (K E) (si x no está libre en E) T[λx.x] => I T[λx.λy.E] => T[λx.T[λy.E]] (si x está libre en E) T[λx.(E1 E2)] => (S T[λx.E1] T[λx.E2])


Sumario del cálculo lambda

El cálculo lambda se refiere a 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 ν substituido 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 substituir 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 substituyendo todas las ocurrencias libres de v por el a. Escribimos así

(λv.E a) ⇒ E[a/v]
por convención, tomamos (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 substitució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 incluidas); 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.



Comments