| Autor(es) | Moses Schönfinkel (1887 o 1889–1942); Haskell B. Curry (1900–1982) |
| Fecha / periodo | 1924–1930 · Siglo XX · Alemania y Estados Unidos |
| Tipo | Formal |
| Deriva de | Teoría de tipos de Principia Mathematica |
| Derivan de ella | Teoría de tipos de Martin-Löf y correspondencia Curry–Howard |
| Tres leyes | Identidad: ✓ (combinador \(I = SKK\), de tipo \(A \to A\)) · No contradicción: no tematizado en el cálculo puro; la versión «ilativa» sin restricciones es inconsistente (paradoja de Curry) · Tercio excluso: no tematizado; con tipos, solo lógica implicativa intuicionista (la ley de Peirce no tiene habitante) |
Las variables ligadas son la parte más delicada de la lógica: exigen reglas de sustitución con condiciones sobre variables libres y cambios de nombre. La lógica combinatoria las elimina. Todo se expresa con unas pocas constantes, los combinadores, y una sola operación, la aplicación de una función a un argumento. Schönfinkel buscaba los «ladrillos» mínimos de la lógica matemática; Curry, un análisis de la sustitución en sus pasos más simples. El gesto distintivo es que la abstracción, la cuantificación y la sustitución se reducen a combinaciones de \(S\) y \(K\), de modo que la lógica queda sin variables y con reglas puramente combinatorias.
Schönfinkel, «Über die Bausteine der mathematischen Logik» (Mathematische Annalen 92, 1924).
El cálculo puro (Curry, «Grundlagen der kombinatorischen Logik», 1930). Los términos se forman a partir de variables y de las constantes \(S\) y \(K\) por aplicación, asociando a la izquierda. Axiomas de reducción débil:
Completitud combinatoria. Para cada término \(M\) y variable \(x\) hay un término \([x]M\), sin \(x\), tal que \(([x]M)N\) se reduce a \(M\) con \(N\) en lugar de \(x\). Se construye por «abstracción de corchetes»:
Ejemplo: \(SKKa \triangleright Ka(Ka) \triangleright a\), luego \(SKK\) actúa como la identidad.
Propiedades. La reducción débil es confluente (teorema de Church–Rosser): si un término se reduce a dos, ambos se reducen a un tercero común, de modo que la forma normal, si existe, es única. Hay términos sin forma normal, como \(SII(SII)\). La lógica combinatoria pura es Turing-completa: define todas las funciones recursivas.
Lógica ilativa. Curry quiso añadir constantes lógicas (\(\Xi\) para la inclusión, \(P\) para la implicación, \(H\) para «ser proposición»). Sin restricciones, el sistema es inconsistente: Kleene y Rosser (1935) derivaron una contradicción en sistemas de este tipo, y Curry (1942) halló la paradoja que lleva su nombre, que no usa la negación. Con el combinador de punto fijo \(Y\) se construye \(X\) tal que \(X = (X \to A)\); de ahí, por contracción y modus ponens, se deriva cualquier \(A\).
Funcionalidad (Curry, 1934). Asignando tipos a los combinadores, los tipos principales son
exactamente los dos axiomas del fragmento implicativo de Hilbert. La regla de tipado de la aplicación coincide con el modus ponens. Los tipos habitados por términos cerrados son los teoremas de la lógica implicativa intuicionista.
Curry llegó a la lógica combinatoria leyendo Principia Mathematica: observó que su regla de sustitución, esencial para las pruebas, no estaba formulada con precisión, y quiso descomponerla en operaciones elementales. Solo después descubrió el artículo de Schönfinkel, que Behmann había preparado a partir de la conferencia de Gotinga de 1920. El paso de 1934, que asocia tipos de combinadores y axiomas de implicación, es la primera forma de la correspondencia entre pruebas y programas, que Howard extendió en 1969 y que la teoría de tipos de Martin-Löf convirtió en fundamento.
Dos afinidades deben leerse como atribuciones. Cardone y Hindley señalan que los axiomas de implicación del Begriffsschrift de Frege coinciden con los tipos principales de \(K\), \(S\) y \(C\), aunque ellos mismos juzgan forzado verlo como anticipación. El cálculo λ de Church es una formalización paralela de la abstracción y la aplicación; ambos proyectos avanzaron sin que sus autores conocieran al principio el trabajo del otro, y luego se mostró que son interdefinibles.
Durante décadas fue un saber marginal, cultivado por Curry y su escuela en Pensilvania. Su recepción llegó por la informática: Turner la usó en los años setenta para implementar lenguajes funcionales por reducción de grafos, y el lenguaje Haskell lleva el nombre de Curry. Para la pregunta «¿una lógica o muchas?» aporta dos lecciones. Una es que lo que parece esencial a la lógica, las variables, puede suprimirse sin perder poder expresivo. Otra, que al añadir constantes lógicas a un cálculo sin tipos aparecen paradojas que no dependen de la negación, lo que obliga a elegir entre tipos, restricciones de la contracción u otras lógicas.