¿Puede razonar una máquina?

En el siglo XVII Leibniz soñó con un calculus ratiocinator: un lenguaje tan preciso que las disputas se zanjarían calculando. «Calculemos», dirían dos filósofos, y se sentarían con lápiz y papel. Dos siglos después George Boole escribió las leyes del pensamiento como álgebra (The Laws of Thought, 1854), y en 1879 Gottlob Frege publicó la Begriffsschrift, el primer lenguaje formal completo para las matemáticas: variables, cuantificadores y reglas de inferencia.

Cuando llegaron los ordenadores, el sueño pareció al alcance. Si razonar es calcular, y un ordenador calcula, un ordenador puede razonar. En 1956, en el mismo taller de Dartmouth que bautizó la disciplina, Allen Newell, Herbert Simon y Cliff Shaw presentaron el Logic Theorist, que demostró 38 de los 52 primeros teoremas del capítulo 2 de los Principia Mathematica de Russell y Whitehead. Nacía la IA simbólica: la inteligencia como manipulación de símbolos según reglas lógicas.

§Verdad y demostración

La lógica de primer orden habla de objetos ($x$, $y$, $\text{tomas}$), funciones ($\text{madre}(x)$), relaciones ($\text{progenitor}(x,y)$), conectivas ($\neg ,\wedge ,\vee ,\to$) y los cuantificadores $\forall$ y $\exists$. Un conjunto de fórmulas $\mathrm{\Gamma }$ puede decir, por ejemplo, que todo progenitor de un antepasado es un antepasado:

Hay dos maneras de decir que una fórmula $\phi$ «se sigue» de $\mathrm{\Gamma }$. La semántica, $\mathrm{\Gamma }\models \phi$: $\phi$ es verdadera en todo mundo (toda interpretación de los símbolos) en el que lo es todo $\mathrm{\Gamma }$. Y la sintáctica, $\mathrm{\Gamma }⊢\phi$: hay una demostración, una sucesión finita de fórmulas en la que cada paso aplica una regla mecánica. La primera habla de significado; la segunda, de mover símbolos. El milagro es que coinciden.

Toda verdad que se sigue de los axiomas tiene demostración, y toda demostración establece una verdad. Esto es lo que hace verosímil el sueño de Leibniz: «verdadero en todos los mundos», una noción infinita, se reduce a «hay una demostración finita», algo que una máquina puede buscar. No hay que confundirlo con el otro teorema de Gödel, más famoso: la incompletitud (1931) dice que ningún conjunto de axiomas consistente y efectivo demuestra todas las verdades sobre los números naturales. La completitud trata de lo que se sigue de los axiomas; la incompletitud, de lo que los axiomas no llegan a fijar.

Pero buscar no es decidir. Las demostraciones se pueden enumerar una a una, así que si $\mathrm{\Gamma }⊢\phi$ la búsqueda acabará encontrando una. Si $\phi$ no se sigue, la búsqueda puede no terminar nunca. En 1936 Church y Turing demostraron que esto no tiene arreglo: no hay ningún algoritmo que decida si una fórmula de primer orden es válida. Es la cara lógica del problema de la parada. La lógica de primer orden es semidecidible: una máquina puede confirmar toda consecuencia, pero no siempre descartarla.

§Resolución: basta una regla

Los sistemas de demostración pensados para personas tienen muchas reglas. En 1965 John Alan Robinson encontró una que basta por sí sola y está hecha para máquinas. Primero, toda fórmula se pasa a forma clausal: una conjunción de cláusulas, cada una una disyunción de literales (átomos o átomos negados), con los cuantificadores existenciales sustituidos por funciones nuevas (funciones de Skolem) y los universales implícitos. Se conserva la satisfacibilidad, y eso basta, porque para demostrar $\phi$ a partir de $\mathrm{\Gamma }$ es suficiente ver que $\mathrm{\Gamma }\cup \{\neg \phi \}$ no tiene modelo.

Derivar $\square$ es haber llegado a una contradicción, como en una demostración por reducción al absurdo. Detrás del teorema está el de Herbrand (1930): un conjunto de cláusulas es insatisfacible si y solo si ya lo es, como lógica proposicional, algún conjunto finito de sus instancias básicas (con constantes en lugar de variables). La resolución busca esas instancias de forma perezosa, sustituyendo solo lo necesario. La clave para hacerlo es la operación del subíndice de la regla, que merece sección propia.

§Unificación

Para resolver $\text{progenitor}(\text{tomas},X)$ contra $\neg \text{progenitor}(Y,\text{bea})$ hace falta una sustitución que haga iguales los dos átomos: $\theta =\{X\mapsto \text{bea},Y\mapsto \text{tomas}\}$. Una sustitución así es un unificador. Puede haber infinitos (para unificar $f(X)$ y $f(Y)$ se pueden poner las dos a $a$, a $b$, a $g(a)$…), pero no todos son igual de buenos: $\{X\mapsto Y\}$ no se compromete a nada más de lo necesario.

Demostración (el algoritmo de Martelli y Montanari)

Se parte del conjunto de ecuaciones $\{s=t\}$ y se aplica cualquiera de estas reglas mientras alguna encaje:

1. Descomponer: se sustituye $f(s_1,\dots ,s_n)=f(t_1,\dots ,t_n)$ por $s_1=t_1,\dots ,s_n=t_n$.
2. Choque: si $f(\dots )=g(\dots )$ con símbolos o aridades distintos, se falla.
3. Borrar: se quita $X=X$.
4. Intercambiar: se sustituye $t=X$, con $t$ que no es variable, por $X=t$.
5. Prueba de ocurrencia: si $X=t$ con $X$ dentro de $t\ne X$, se falla.
6. Eliminar: si $X=t$ con $X$ que no aparece en $t$ pero sí en otras ecuaciones, se sustituye $X$ por $t$ en todas ellas.

Cada regla conserva el conjunto de unificadores del sistema, y las dos de fallo solo se aplican a sistemas sin unificador: ninguna sustitución hace igual $f$ a $g$, ni $X$ igual a un término estrictamente mayor que el propio $X$. El proceso termina, porque cada paso reduce, en orden lexicográfico, el número de variables aún sin resolver, el tamaño total de los términos y el número de ecuaciones de la forma $t=X$. Cuando no encaja ninguna regla, el sistema tiene la forma $\{X_1=t_1,\dots ,X_k=t_k\}$, con variables distintas que no aparecen en ningún otro sitio. Entonces $\theta =\{X_i\mapsto t_i\}$ es un unificador y, como el sistema original tiene los mismos unificadores que el final, cualquier otro unificador $\sigma$ cumple $X_i\sigma =t_i\sigma$, es decir, $\sigma =\theta \sigma$. Así que $\sigma$ se factoriza a través de $\theta$.

§Prolog: la lógica como programa

La resolución sobre cláusulas cualesquiera explota combinatoriamente. Pero si cada cláusula tiene como mucho un literal positivo (una cláusula de Horn), se puede leer como una regla, «$A$ es cierto si lo son $B_1,\dots ,B_n$»:

En 1972 Alain Colmerauer y Philippe Roussel, en Marsella, construyeron sobre esa idea un lenguaje para procesar lenguaje natural: Prolog (programmation en logique). Robert Kowalski, en Edimburgo, puso la teoría: un conjunto de cláusulas de Horn se puede leer de dos maneras, como afirmaciones verdaderas o como procedimientos que se ejecutan. Lo resumió como «algoritmo = lógica + control». Tú escribes qué es cierto; la máquina decide cómo buscar.

progenitor(tomas, bea).        % hechos: cláusulas sin cuerpo
progenitor(bea, ana).
progenitor(bea, pablo).

antepasado(X, Y) :- progenitor(X, Y).        % reglas: ":-" se lee "si"
antepasado(X, Y) :- progenitor(X, Z),        % "," se lee "y"
                    antepasado(Z, Y).

Una consulta como ?- antepasado(tomas, Quien). es un objetivo que refutar: la máquina supone que nadie desciende de Tomás y busca la contradicción. Resolver siempre el objetivo de más a la izquierda contra las cláusulas del programa, en orden, es la resolución SLD, y la sustitución que va acumulando es la respuesta: Quien = bea, Quien = ana, Quien = pablo.

§Qué significa un programa lógico

Un programa tiene un significado independiente de cómo se ejecute. Llamemos ${ℬ}_P$ al conjunto de todos los átomos básicos (sin variables) que se pueden escribir con los símbolos del programa, y $\mathrm{ground}(P)$ al conjunto de instancias básicas de sus cláusulas. Considera el operador que toma un conjunto $I\subseteq {ℬ}_P$ y devuelve todo lo que se deduce de él en un paso:

Demostración

Un conjunto de átomos básicos $I$ es modelo de $P$ exactamente cuando $T_P(I)\subseteq I$: toda regla cuyo cuerpo se cumple en $I$ tiene su cabeza en $I$. La intersección de modelos es un modelo (si el cuerpo está en todos, la cabeza también), así que hay un modelo mínimo, $M_P$, la intersección de todos.

$T_P$ es monótono ($I\subseteq J$ implica $T_P(I)\subseteq T_P(J)$) y, como cada cuerpo es finito, continuo: un átomo deducido de la unión de una cadena creciente ya se deduce en alguna etapa finita. Por el teorema del punto fijo de Kleene, $\bigcup _k{T}_P^k(\varnothing )$ es el menor punto fijo. Está contenido en todo modelo, por inducción en $k$, y es a su vez un modelo, así que coincide con $M_P$. Por último, $P\models A$ para un $A$ básico significa que $A$ es verdadero en todo modelo de $P$, y basta mirar los modelos formados por átomos básicos (todo modelo induce uno con los mismos átomos básicos verdaderos). Si $A$ es verdadero en todos ellos, está en $M_P$; y todo átomo de $M_P$ es verdadero en todos, porque todos contienen a $M_P$.

Para el programa de la familia: $T_P(\varnothing )$ contiene los tres hechos; un paso más añade $\text{antepasado}(\text{tomas},\text{bea})$, $\text{antepasado}(\text{bea},\text{ana})$ y $\text{antepasado}(\text{bea},\text{pablo})$; otro más, $\text{antepasado}(\text{tomas},\text{ana})$ y $\text{antepasado}(\text{tomas},\text{pablo})$; y a partir de ahí no aparece nada nuevo. Ese es el significado del programa, y el procedimiento está a la altura:

La condición importa. Prolog recorre el árbol en profundidad, cláusula a cláusula, porque es rápido y gasta poca memoria. Pero si una rama es infinita, Prolog se mete en ella y no vuelve, aunque haya respuestas más a la derecha. Escribe la regla recursiva como antepasado(X, Y) :- antepasado(Z, Y), progenitor(X, Z). y ponla la primera: el significado lógico es exactamente el mismo, pero el programa ya no responde nada. Compara las dos versiones en la figura.

Prolog añade además piezas ajenas a la lógica pura: aritmética (X is Y + 1), el corte !, que poda alternativas del árbol, y la negación por fallo (Clark, 1978): \+ P tiene éxito si $P$ no se puede demostrar. Es la hipótesis del mundo cerrado, «lo que no puedo deducir es falso». Es muy práctica en bases de datos, y no es monótona: añadir un hecho puede volver falsa una conclusión.

§Tu propio Prolog

La figura de abajo es un intérprete de Prolog completo que se ejecuta en tu navegador: unificación, vuelta atrás, corte, aritmética con enteros de cualquier tamaño, listas, gramáticas de cláusulas definidas y los predicados predefinidos habituales. Elige un ejemplo, modifícalo o escribe tu propio programa, y hazle preguntas. Activa la traza para ver los cuatro puertos clásicos de cada llamada: Call (llamada), Exit (salida), Redo (reintento) y Fail (fallo).

§Sistemas expertos, y sus límites

En los años setenta y ochenta la IA simbólica llegó a la industria. Los sistemas expertos guardaban el conocimiento de un especialista en cientos o miles de reglas: MYCIN (Stanford, 1976) recomendaba tratamientos para infecciones de la sangre, y en una evaluación a ciegas de 1979 sus prescripciones recibieron tan buena nota como las de especialistas en enfermedades infecciosas; XCON configuraba ordenadores de DEC y le ahorraba a la empresa millones al año. En 1982 Japón lanzó el proyecto de Sistemas de Computación de Quinta Generación, diez años de dinero público para construir máquinas que ejecutaran programas lógicos en paralelo. La programación lógica era su núcleo.

No cumplió lo prometido. Los obstáculos no estaban en la lógica sino en el mundo:

• El cuello de botella de la adquisición del conocimiento. Los expertos saben más de lo que pueden poner en reglas, y cada regla tiene excepciones a las excepciones.
• La fragilidad. Fuera de los casos previstos por las reglas, un sistema experto no se degrada con elegancia: simplemente falla.
• La incertidumbre. La lógica habla de verdadero y falso, y el mundo está hecho de «probablemente». MYCIN tuvo que inventarse unos «factores de certeza» ad hoc.
• La explosión combinatoria. La semidecidibilidad y el tamaño del espacio de búsqueda no son tecnicismos: encarecen el razonamiento justo donde importa.

El mercado de las máquinas Lisp se hundió en 1987, y con él llegó el segundo invierno de la IA. Pero la lógica no desapareció. Sigue viva en Datalog y en las consultas recursivas de SQL, en la inferencia de tipos, en los solucionadores SAT y SMT que verifican chips y programas, en asistentes de demostración como Lean, que los matemáticos ya usan para comprobar demostraciones, y en sistemas que combinan modelos de lenguaje con herramientas simbólicas. La diferencia con aquella época es el orden: hoy las reglas no se escriben a mano, se aprenden.

Aprender de ejemplos significa aceptar que las conclusiones nunca son seguras, solo más o menos probables. Razonar con grados de creencia en lugar de con valores de verdad exige otra matemática. Eso es la probabilidad.

§Referencias

1. G. Boole (1854). An Investigation of the Laws of Thought. Walton and Maberly.
2. G. Frege (1879). Begriffsschrift, eine der arithmetischen nachgebildete Formelsprache des reinen Denkens. Halle.
3. K. Gödel (1930). «Die Vollständigkeit der Axiome des logischen Funktionenkalküls». Monatshefte für Mathematik und Physik, 37.
4. A. Newell y H. A. Simon (1956). «The Logic Theory Machine». IRE Transactions on Information Theory, 2(3).
5. J. A. Robinson (1965). «A Machine-Oriented Logic Based on the Resolution Principle». Journal of the ACM, 12(1).
6. R. Kowalski (1974). «Predicate Logic as Programming Language». Proceedings of IFIP Congress 74.
7. M. H. van Emden y R. Kowalski (1976). «The Semantics of Predicate Logic as a Programming Language». Journal of the ACM, 23(4).
8. K. L. Clark (1978). «Negation as Failure». En Logic and Data Bases, Plenum Press.
9. A. Martelli y U. Montanari (1982). «An Efficient Unification Algorithm». ACM Transactions on Programming Languages and Systems, 4(2).
10. J. W. Lloyd (1987). Foundations of Logic Programming, 2.ª ed. Springer.
11. A. Colmerauer y P. Roussel (1993). «The Birth of Prolog». ACM SIGPLAN Notices, 28(3).