Diferencia entre revisiones de «Lógica combinatoria»

== Introducción ==

La teoría, a causa de su simplicidad, captura las características esenciales de la naturaleza del cómputo. La lógica combinatoria ('''LC''') es el fundamento del cálculo lambda, al eliminar el último tipo de variable de éste: la variable lambda. En '''LC''' las expresiones lambda (usadas para permitir la abstracción funcional) son substituidas por un sistema limitado de combinadores, las funciones primitivas que no contienen ninguna [[variable libre]] ('''ni ligada'''). Es fácil transformar expresiones lambda en expresiones combinatorias, y puesto que la reducción de un combinador es más simple que la reducción lambda, '''LC''' se ha utilizado como la base para la puesta en práctica de algunos lenguajes de programación funcionales ''no-estrictos'' en software y hardware.

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

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]]'''.

por convención, tomamos (b c d... z) como abreviatura para (... (((a b) c) d)... z). ('''[[Magma (álgebra)#No_asociatividadNo asociatividad|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:

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'''.

== Cálculos Combinatorios ==

Puesto que la abstracción es la única manera de fabricar funciones en el cálculo lambda, algo debe sustituirlo 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.

=== Términos combinatorios ===

* ''V''

* ''P''

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]].

=== Ejemplos de combinadores ===

para todos los términos ''x''. otro combinator simple es '''K''', que produce funciones constantes: ('''K''' ''x'') es la función que, para cualquier argumento, devuelve ''x'', así que decimos

'''S''' aplica ''x'' a ''y'' después de substituir primero a z en cada uno de ellos.

para cualquier término ''x''. Nótese que aunque (('''S''' '''K''' '''K''') ''x'') = ('''I''' ''x'') para cualquier ''x'', ('''S''' '''K''' '''K''') en sí mismo no es igual a '''I'''. Decimos que los términos son extensionalmente iguales.

==== 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.

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

==== Conversión de un término lambda a un término combinatorio equivalente ====

si aplicamos este combinator a cualesquiera dos términos ''x'' y ''y'', reduce como sigue:

La representación combinatoria, ('''S''' ('''K''' ('''S''' '''I''')) ('''S''' ('''K''' '''K''') '''I''')) es mucho más larga que la representación como término lambdaλ''x''.λ''y''.(''y'' ''x''). Esto es típico. En general, la construcción de ''T''[ ] puede ampliar un término lambda de la longitud n a un término combinatorio de la longitud

==== Explicación de la transformación ''T''[ ] ====

La transformación ''T''[ ] es motivada por un deseo de eliminar la abstracción. Dos casos especiales, reglas 3 y 4, son triviales: λ''x''.''x'' es claramente equivalente a I, y λ''x''.''E'' es claramente equivalente a (K E) si x no aparece libre en E.

Las primeras dos reglas son también simples: Las variables se convierten en sí mismas, y las aplicaciones permitidas en términos combinatorios, son convertidas los combinadores simplemente convirtiendo el aplicando y el argumento a combinadores.

Son las reglas 5 y 6 las que tienen interés. La regla 5 dice simplemente esto: para convertir una abstracción compleja a un combinador, debemos primero convertir su cuerpo a un combinator, y después eliminamos la abstracción. La regla 6 elimina realmente la abstracción.

λ''x''.''(E1E2)'' es una función que toma un argumento, digamos ''a'', y lo substituye en el término lambda ''(E1 E2)'' en lugar de ''x'', dando ''(E1 E2)''[''a''/''x'']. Pero substituir a en (E1 E2) en lugar de x es precisamente igual que sustituirlo en E1 y E2, así que

evidentemente cumple el objetivo. ''E1'' y ''E2'' contienen cada uno estrictamente menos aplicaciones que ''(E1 E2)'', así que la repetición debe terminar en un término lambda sin aplicación ninguna-ni una variable, ni un término de la forma λ''x''.''E''.

=== Simplificaciones de la transformación ===

==== η-reducción ====

[[''λx''.(''E'' x)]] es la función que toma un argumento, x, y aplica la función E a él; esto es extensionalmente igual a la función ''E'' misma. Es por lo tanto suficiente convertir E a la forma combinatoria.

semejantemente, la versión original de la transformación ''T''[ ] transformó la función identidad ''λf''.''λx''.(''f'' ''x'') en ('''S''' ('''S''' ('''K''' '''S''') ('''S''' ('''K''' '''K''') '''I''')) ('''K''' '''I''')). Con la regla de η-reducción, ''λf''.''λx''.(''f'' ''x'') se transformó en '''I'''.

==== los combinadores B, C de Curry ====

Los combinadores '''S''', '''K''' se encuentran ya en [[Moses Schoenfinkel |Schönfinkel]] (aunque el símbolo '''C''' se usaba por el actual '''K''') [[Haskell Curry|Curry]] introdujo el uso de '''B''', '''C''', '''W''' (y '''K'''), ya antes de su ''tesis doctoral de 1930''. En ''Lógica combinatoria T. I'', Se ha vuelto a '''S''', '''K''' pero se muestra, (vía [[algoritmos de Markov]]) que el uso de '''B''' y '''C''' pueden simplificar muchas reducciones. Esto parece haberse utilizado mucho después por [[David Turner]], cuyo nombre ha quedado ligado a su uso computacional. Se introducen dos nuevos combinadores:

# ''T''[''V''] => ''V''

# ''T''[(''E1'' ''E2'')] => (''T''[''E1''] ''T''[''E2''])

# ''T''[''λx''.''E''] => ('''K''' ''E'') (if ''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'']) (si ''x'' está libre tanto en ''E1'' como en ''E2'')

# ''T''[''λx''.(''E1'' ''E2'')] => ('''C''' ''T''[''λx''.''E1''] ''E2'') (si ''x'' está libre en ''E1'' pero no en ''E2'')

# ''T''[''λx''.(''E1'' ''E2'')] => ('''B''' ''E1'' ''T''[''λx''.''E2'']) (si ''x'' está libre en ''E2'' pero no en ''E1'')

La conversión ''L''[ ] de términos combinatorios a términos lambda es

Nótese, sin embargo, que esta transformación no es la transformación inversa de ninguna de las versiones de '''T'''[ ] que se han visto.

Es indecidible cuándo un término combinatorio general tiene forma normal; cuando dos términos combinatorios son equivalentes, etc. Esto es

equivalente a la indecidibilidad de los correspondientes problemas para términos lambda. No obstante, una prueba directa es como sigue:

Ahora, supongamos que '''N''' fuera un combinador para detectar formas normales,

Las versiones combinatorias tienen '''T''' = '''K''' y '''F''' = ('''K''' '''I''') = 0 = K'.)

y consideremos el término ('''S''' '''I''' '''I''' ''Z''). Tiene ('''S''' '''I''' '''I''' ''Z'') una forma normal? La tiene si y sólo si:

O bien ('''S''' '''I''' '''I''' ''Z'') tiene una forma normal, o no la tiene. Si ''tuviera'' forma normal, entonces se reduce como sigue:

pero '''A''' ''no'' tiene una forma normal, por tanto tenemos una contradicción. Pero si ('''S''' '''I''' '''I''' ''Z'') ''no'' tiene una forma normal, se reduce como sigue:

lo que significa que la forma normal de ('''S''' '''I''' '''I''' ''Z'') es simplemente '''I''', otra contradicción. Por tanto, el hipotético combinador de forma normal '''N''' no puede existir.

== Referencias ==