| Autor(es) | Alonzo Church (1903–1995); Stephen C. Kleene (1909–1994); J. Barkley Rosser (1907–1989) |
| Fecha / periodo | 1932–1941 · Siglo XX · Estados Unidos |
| Tipo | Formal |
| Deriva de | Teoría de tipos de Principia Mathematica · Formalismo y programa de Hilbert |
| Derivan de ella | Lógica de orden superior y teoría simple de tipos · Lógica categórica y de topos · Teoría de tipos de Martin-Löf y correspondencia Curry–Howard · Cálculo de construcciones y asistentes de prueba |
| Tres leyes | Identidad: ✓ (término \(\lambda x.x\); con tipos, \(A \to A\)) · No contradicción: no tematizado en el cálculo puro; el sistema lógico de Church de 1932–1933, con negación, resultó inconsistente (Kleene y Rosser, 1935) · Tercio excluso: no tematizado; con tipos simples, los tipos habitados son teoremas intuicionistas y \(A \lor \neg A\) no lo es |
Church quería un fundamento de la lógica más natural que la teoría de tipos de Russell, basado en la noción de función. Su instrumento fue un operador de abstracción: \(\lambda x.M\) designa la función que asigna a cada \(x\) el valor \(M\). Con abstracción, aplicación y una regla que dice cómo calcular la aplicación de una abstracción, se obtiene un cálculo muy simple que resultó capaz de expresar cualquier función computable. El sistema lógico que Church construyó encima era inconsistente, pero el núcleo sobrevivió. El gesto distintivo es identificar el cálculo con la manipulación de expresiones según reglas de conversión: evaluar es reescribir.
Sintaxis. Los términos son variables \(x, y, \dots\); aplicaciones \((MN)\); abstracciones \((\lambda x.M)\). Una variable está ligada si cae bajo un \(\lambda\) que la nombra.
Reglas de conversión (Church, The Calculi of Lambda-Conversion, 1941):
Church prefería el cálculo λI, que exige que \(x\) aparezca en \(M\) en toda abstracción \(\lambda x.M\); el cálculo λK, sin esa restricción, es el que se usa hoy.
Formas normales y confluencia. Un término está en forma normal si no contiene subtérminos de la forma \((\lambda x.M)N\). El teorema de Church–Rosser (1936) afirma que si \(M\) se reduce a \(N_1\) y a \(N_2\), ambos se reducen a un \(N_3\) común. De ahí se sigue que la forma normal es única y que el cálculo es consistente en el sentido de que no identifica todos los términos. El término \((\lambda x.xx)(\lambda x.xx)\) se reduce a sí mismo y no tiene forma normal.
Aritmética y recursión. Los numerales de Church son \(\bar n = \lambda f.\lambda x.f^n x\). El sucesor es \(\lambda n.\lambda f.\lambda x.f(nfx)\). El combinador de punto fijo \(Y = \lambda f.(\lambda x.f(xx))(\lambda x.f(xx))\) cumple \(YF = F(YF)\) y permite definir funciones por recursión. Kleene (1936) probó que las funciones λ-definibles son exactamente las recursivas generales, y Turing (1937) que coinciden con las computables por su máquina.
Indecidibilidad. Church (1936) mostró que no hay algoritmo λ-definible que decida si un término tiene forma normal. Identificando «efectivamente calculable» con «λ-definible» (tesis de Church), concluyó que el Entscheidungsproblem de Hilbert no tiene solución: la validez en lógica de primer orden no es decidible («A note on the Entscheidungsproblem», 1936).
La lógica de 1932–1933. Church añadió constantes para la negación, la implicación, la cuantificación y la descripción, con restricciones débiles para evitar la paradoja de Russell. Kleene y Rosser (1935) derivaron en él la paradoja de Richard: el sistema era inconsistente.
Tipos simples (1940). Church asigna a cada término un tipo: \(o\) (proposiciones), \(\iota\) (individuos) y \(\alpha \to \beta\). Solo se aplica \(M : \alpha \to \beta\) a \(N : \alpha\). Todo término tipado tiene forma normal (normalización fuerte), pero se pierde la recursión general. Los tipos habitados coinciden con el fragmento implicativo intuicionista.
Ejemplo. \((\lambda x.\lambda y.x)\,a\,b \to (\lambda y.a)\,b \to a\): el término \(\lambda x.\lambda y.x\) proyecta el primer argumento, como el combinador \(K\).
La notación viene de Principia Mathematica, que escribía \(\hat x\) para formar clases y funciones proposicionales. En una carta de 1964 Church explicó que desplazó el acento circunflejo delante de la variable y que un cambio tipográfico lo convirtió en λ. Más que la notación, heredó el problema: buscaba una alternativa a la jerarquía de tipos de Russell, que le parecía artificiosa. Del programa de Hilbert recibió la pregunta decisiva, el Entscheidungsproblem planteado por Hilbert y Ackermann en 1928, que el cálculo λ permitió responder negativamente en 1936.
Church mismo lo combinó en 1940 con la teoría simple de tipos, en la formulación de la lógica de orden superior que aún se usa. Lambek hizo corresponder el cálculo tipado con las categorías cartesianas cerradas, puente con la lógica categórica. La correspondencia Curry–Howard representa pruebas como términos λ tipados, y el cálculo de construcciones ocupa la cumbre del cubo de Barendregt de cálculos tipados, base de asistentes de prueba como Coq. Como afinidad, la lógica combinatoria de Schönfinkel y Curry es una formalización paralela de la abstracción y la aplicación, desarrollada al principio sin conocimiento mutuo.
El cálculo λ nació como fundamento de la lógica y fracasó como tal, pero se convirtió en una de las definiciones canónicas de la computabilidad y en el núcleo teórico de los lenguajes funcionales, desde LISP (1958) hasta ML y Haskell. Dana Scott dio en 1969 sus primeros modelos matemáticos. Para la pregunta «¿una lógica o muchas?», su historia es elocuente: un mismo cálculo, sin tipos, es inconsistente como lógica y fecundo como teoría de funciones; con tipos, da una lógica constructiva. Qué lógica se obtiene depende de las restricciones que se impongan a la formación de términos.