La lógica combinatoria es una notación para eliminar la necesidad de variables cuantificadas en la lógica matemática . Fue presentado por Moses Schönfinkel [1] y Haskell Curry , [2] y más recientemente se ha utilizado en informática como modelo teórico de computación y también como base para el diseño de lenguajes de programación funcionales . Se basa en combinadores que fueron introducidos por Schönfinkel en 1920 con la idea de proporcionar una forma análoga de construir funciones y eliminar cualquier mención de variables, particularmente en la lógica de predicados.. Un combinador es una función de orden superior que usa solo la aplicación de función y combinadores definidos anteriormente para definir un resultado a partir de sus argumentos.
La lógica combinatoria se pensó originalmente como una "prelógica" que aclararía el papel de las variables cuantificadas en la lógica, esencialmente eliminándolas. Otra forma de eliminar variables cuantificadas es la lógica de funtores predicados de Quine . Mientras que el poder expresivo de la lógica combinatoria típicamente excede al de la lógica de primer orden , el poder expresivo de la lógica de funtores de predicados es idéntico al de la lógica de primer orden ( Quine 1960, 1966, 1976 ).
El inventor original de la lógica combinatoria, Moses Schönfinkel , no publicó nada sobre lógica combinatoria después de su artículo original de 1924. Haskell Curry redescubrió los combinadores mientras trabajaba como instructor en la Universidad de Princeton a fines de 1927. [3] A fines de la década de 1930, Alonzo Church y sus estudiantes en Princeton inventaron un formalismo rival para la abstracción funcional, el cálculo lambda , que resultó ser más popular que el combinatorio. lógica. El resultado de estas contingencias históricas fue que hasta que la informática teórica comenzó a interesarse por la lógica combinatoria en las décadas de 1960 y 1970, casi todo el trabajo sobre el tema fue de Haskell Curry .y sus alumnos, o por Robert Feys en Bélgica . Curry y Feys (1958), y Curry et al. (1972) examinan la historia temprana de la lógica combinatoria. Para un tratamiento más moderno de la lógica combinatoria y el cálculo lambda juntos, vea el libro de Barendregt , [4] que revisa los modelos que Dana Scott ideó para la lógica combinatoria en las décadas de 1960 y 1970.
En ciencias de la computación , la lógica combinatoria se utiliza como un modelo simplificado de cálculo , utilizado en la teoría de la computabilidad y la teoría de la prueba . A pesar de su simplicidad, la lógica combinatoria captura muchas características esenciales de la computación.
La lógica combinatoria se puede ver como una variante del cálculo lambda , en el que las expresiones lambda (que representan la abstracción funcional) se reemplazan por un conjunto limitado de combinadores , funciones primitivas sin variables libres . Es fácil transformar expresiones lambda en expresiones de combinador, y la reducción de combinador es mucho más simple que la reducción de lambda. Por lo tanto, la lógica combinatoria se ha utilizado para modelar algunos lenguajes de programación y hardware funcionales no estrictos . La forma más pura de esta vista es el lenguaje de programación Unlambda, cuyas únicas primitivas son los combinadores S y K aumentados con entrada/salida de caracteres. Aunque no es un lenguaje de programación práctico, Unlambda tiene cierto interés teórico.
A la lógica combinatoria se le puede dar una variedad de interpretaciones. Muchos de los primeros artículos de Curry mostraron cómo traducir conjuntos de axiomas para la lógica convencional en ecuaciones de lógica combinatoria (Hindley y Meredith 1990). Dana Scott en las décadas de 1960 y 1970 mostró cómo unir la teoría de modelos y la lógica combinatoria.