% -*- coding: iso-8859-1-unix; -*- % cap03.tex % % Programación Lógica y Funcional % Álvaro Tasistro - Jorge Vidart % III E.B.A.I. (1988) % % maquetación LaTeX por César Ballardini % % Copyright (C) 1988 Álvaro Tasistro - Jorge Vidart. % % Permission is granted to copy, distribute and/or modify this document % under the terms of the GNU Free Documentation License, Version 1.2 or % any later version published by the Free Software Foundation; with no % Invariant Sections, no Front-Cover Texts, and no Back-Cover Texts. A % copy of the license is included in the section entitled ``GNU Free % Documentation License'' % % $Id: cap03.tex,v 1.1 2003/08/13 04:01:21 cballard Exp $ % \chapter{Interpretación lógica} \label{cha:interpretacionlogica} % -------------------------------------------------------- \begin{abstract} \label{sec:intlogresumen} Una\pagina{29} de las características de la programación en lógica es que admite múltiples interpretaciones. Una de ellas proviene de la lógica. En ella un programa constituye una definición axiomática de una teoría, y a una invocación a la ejecución del mismo se la considera como una fórmula a demostrar en dicha teoría. Luego de una introducción general al tema, en la primera sección se introduce la definición sintáctica de los programas en lógica. Asimismo se presentan los mecanismos de estructuración de datos, los que se obtienen a partir de los símbolos funcionales que puede introducir el usuario. El significado de los programas en lógica se presenta en la segunda sección, utilizando los conceptos de lógica que se definen. A continuación se plantean los mecanismos de derivación lógica a partir de reglas de inferencia, y el concepto de unificación que es el que permite realizar dicha operación en presencia de variables. El capítulo concluye con la presentación de un modelo general para el paso inferencial y con un ejemplo de aplicación. \end{abstract} En\pagina{30} la introducción se ha visto cómo es posible definir y manipular relaciones mediante programas en lógica. Para dichos programas fue presentada una semántica intuitiva, a finde comprender las \textit{ejecuciones} de los mismos. En lo que sigue se utilizarán nociones de la lógica para el mismo objetivo. Se tratará de no realizar un planteo excesivamente formal de tal manera que se puedan rescatar las ideas intuitivas subyacentes. El lector interesado puede recurrir al excelente libro de Lloyd~\cite{Llo84}. La idea de base de la programación en lógica radica en utilizar conceptos de la lógica para referirse a todos y cada uno de los procesos de construcción de programas y de ejecución de los mismos. Un programa, como el formado por el conjunto de las reglas de la introducción, corresponderá a la definición de una teoría axiomática, y una ejecución, es decir la evaluación de una interrogación de alguna de las relaciones definidas, significará una demostración o prueba a partir de los axiomas. En esta perspectiva, un intérprete de programas en lógica es, en definitiva, un demostrador automático de teoremas. Desde el punto de vista lógico una cláusula como: \begin{verbatim} PADRE( juan, raquel ). \end{verbatim} \noindent representa la afirmación del hecho que \texttt{juan} es el \texttt{PADRE} de \texttt{raquel}. Sin embargo es importante destacar que las palabras \texttt{juan} y \texttt{raquel} son simplemente sucesiones de caracteres. La interpretación de que ambas palabras representan a ciertas personas dadas, está solamente en la intención del programador y dicha información no la tiene el sistema de evaluación lógica. Esta situación tendrá relevancia cuando se presenten los mecanismos de demostración lógica y se introduzca el concepto de satisfactibilidad. Una cláusula como: \begin{verbatim} TIO(ricardo,diego) <- PADRE(jorge,diego), HERMANO(jorge,ricardo) \end{verbatim} \noindent representará\pagina{31} la afirmación condicional que si es cierto que \texttt{jorge} es el \texttt{PADRE} de \texttt{diego}, y que \texttt{jorge} es el \texttt{HERMANO} de \texttt{ricardo}, entonces se puede concluir que \texttt{ricardo} es \texttt{TIO} de \texttt{diego}. Y si la cláusula fuera con variables: \begin{verbatim} TIO(X,Y) <- PADRE(Z,Y), HERMANO(X,Z) \end{verbatim} \noindent representará la afirmación que para todo valor posible de \texttt{X} y \texttt{Y}, si existe un valor de \texttt{Z} tal que \texttt{Z} es el \texttt{PADRE} de \texttt{Y}, y además ese mismo \texttt{Z} es \texttt{HERMANO} de \texttt{X}, entonces \texttt{X} es \texttt{TIO} de \texttt{Y}. Finalmente debe considerarse el caso de la invocación a la ejecución de un programa. Así la fórmula: \begin{verbatim} <- HERMANO(jorge, ricardo) \end{verbatim} \noindent expresa que se desea determinar si el predicado que aparece en la misma, es válido a partir de la información que ofrece el programa visto anteriormente. En otras palabras se pretende demostrar que la fórmula en cuestión es una consecuencia lógica de las fórmulas que conforman el programa. % -------------------------------------------------------- \section{Sintaxis de programas en lógica} \label{sec:sintaxisprogramaslogica} El lenguaje que se utiliza en la programación en lógica proviene de la lógica de predicados de primer orden. Se dispone de: \begin{itemize} \item un conjunto de elementos simples llamados átomos. \item un vocabulario $V$ de variables. \item un vocabulario $F$ de símbolos funcionales. \item un vocabulario $P$ de símbolos predicativos. \end{itemize} \noindent Cada\pagina{32} símbolo funcional y predicativo tiene asociado un número entero que corresponde a su aridad. Como convención se adoptará que los átomos estarán formados por caracteres en minúsculas y números, por ejemplo: \begin{verbatim} a, b, raquel, 1, 3200, paris, caracas \end{verbatim} Las variables se denotarán utilizando letras mayúsculas: \begin{verbatim} X, Y, Z, ... \end{verbatim} Para los símbolos funcionales se usarán también letras minúsculas, lo que no ofrece ambigüedad con los átomos, debido a su diferenciada ubicación sintáctica. Los símbolos predicativos serán denotados usando letras mayúsculas. \begin{definicion}[Sintaxis de programas en lógica] \begin{itemize} \item Un \textbf{término} es: \begin{itemize} \item un átomo \item una variable \item un símbolo funcional seguido de una sucesión de términos, tantos como la aridad del símbolo funcional. \end{itemize} \item Un \textbf{predicado} es un símbolo predicativo seguido de una sucesión de términos, tantos como la aridad del símbolo predicativo. \item Una \textbf{regla} o \textbf{cláusula}, es alguna de las siguientes alternativas: $$ \begin{array}{ccll} A & \leftarrow & . & \mathrm{(I)}\\ A & \leftarrow & B_1, \ldots , B_m . & \mathrm{(II)}\\ & \leftarrow & B_1, \ldots , B_m . & \mathrm{(III)} \end{array} $$ siendo $A, B_1, \ldots, B_m$ predicados. \item Un \textbf{programa lógico} es un conjunto de reglas. \end{itemize} \end{definicion} Mediante\pagina{33} el concepto de términos, y utilizando los símbolos funcionales es posible estructurar la información a ser manipulada por los programas en lógica. Por ejemplo, si se tiene: \begin{verbatim} empleado( jaime, 32, 1827 ) \end{verbatim} \noindent con \texttt{empleado} símbolo funcional, y \texttt{jaime}, \texttt{32} y \texttt{1827}, átomos, el significado de dicho término podría ser que \texttt{jaime} es un empleado que tiene \texttt{32} años, y que su número interno es \texttt{1827}. La interpretación de cada uno de los átomos presentes surge entonces de su posición en el término, lo que equivale a asignar significado a los dominios del símbolo funcional. Si se desea un mayor poder de expresión, esto puede lograrse agregando nuevos símbolos funcionales (unarios) como en el ejemplo: \begin{verbatim} empleado( nombre(jaime), edad(32), numero(1827) ). \end{verbatim} Un símbolo funcional distinguido, y que será denotado con un punto («.») permite definir expresiones simbólicas (árboles binarios). Estas estructuras, llamadas S-expresiones, fueron introducidas para los lenguajes funcionales como LISP. Su sintaxis es muy simple: \begin{verbatim} S-expresión ::= átomo S-expresión ::= "[" S-expresión "." S-expresión "]" \end{verbatim} Mediante el símbolo funcional «\texttt{.}», y admitiendo para él una notación infija, se obtienen las S-expresiones como términos del lenguaje. Así por ejemplo se pueden escribir los términos: \begin{verbatim} [a.[b.c]], [[[x.t].y].[r.[o.p]]] \end{verbatim} \noindent los que \textit{visualizados} como árboles binarios tendrían la siguiente representación: \begin{verbatim} * * / \ / \ / \ / \ a * * * / \ / \ / \ / \ / \ / \ b c * v r * / \ / \ / \ / \ x t o p \end{verbatim} Para\pagina{34} la definición recursiva de los árboles es necesario considerar un elemento particular que representa el árbol \textit{vacío} y que se denotará con «\texttt{[\,]}» (también se le representa como \texttt{NIL}). Con dicho elemento es posible considerar un caso particular de árboles binarios, que corresponderá al concepto de listas. Una lista, o sucesión de elementos, por ejemplo $(a\ b\ c\ d)$, tendrá como representación al siguiente árbol binario: \texttt{[a.[b.[c.[d.[]]]]]}. En base a las estructuras de árboles recién vistas, se puede diseñar un programa lógico cuyo cometido sea el de concatenar dos listas. Este es un problema clásico para resolver en programación funcional, donde el objetivo es escribir una función que recibiendo como argumentos dos listas, como por ejemplo $(a\ b)$ y $(c\ d)$, evalúe como resultado la concatenación de las mismas. En el ejemplo sería: $(a\ b\ c\ d)$. En programación en lógica el programa es el siguiente: \begin{verbatim} CONCAT( [], X, X ) <- . CONCAT( [X.L], Y, [X.Z] ) <- CONCAT( L, Y, Z ). \end{verbatim} De acuerdo a lo que se planteó en la sintaxis, este programa es un conjunto de dos reglas, que tal como se vió en la introducción definen una relación: \pagina{35} \begin{verbatim} CONCAT en (listas) x (listas) x (listas). \end{verbatim} En realidad el problema propuesto corresponde a una función de: \begin{verbatim} (listas) x (listas) -> (listas). \end{verbatim} \noindent si se interpreta que el tercer argumento corresponde a la concatenación del primero con el segundo, pero en la programación en lógica sólo se pueden representar relaciones. Cabe destacar aquí que las variables que aparecen en el programa tienen como alcance cada una de las reglas. Es decir que la \texttt{X} en la primera regla es diferente a la de la segunda. Varias pueden ser las formas de \textit{leer} el programa \texttt{CONCAT}. La primera regla indica que la concatenación de la lista vacía con cualquier listas \texttt{X}, da como resultado la misma lista \texttt{X}. Esta regla expresa además que éste es un hecho sin condicionantes, ya que no aparecen predicados a la derecha del símbolo «\texttt{<-}». La segunda regla puede leerse de derecha a izquierda. Si adoptamos la notación de «\texttt{*}» para el operador de concatenación de listas, la regla representa: $$ \mathbf{si}\ Z = L * Y\ \mathbf{entonces}\ \forall X\ [X.Z] = [X.L] * Y $$ \noindent lo que equivale al paso inductivo de una definición recursiva de la relación \texttt{CONCAT}. Un primer elemento a destacar de los programas en lógica, es su carácter declarativo. Al analizar el programa \texttt{CONCAT}, se constata que el mismo se parece mucho más a una definición formal que a una descripción algorítmica. Uno de los problemas más complejos de la programación tradicional es el de estableceer mecanismos formales que permitan especificar el problema a resolver, y que además sirvan para determinar si un cierto algoritmo dado verifica las condiciones del problema. Dicho de otra manera, la dificultad consiste en vincular la especificación de un problema donde se define \textit{qué} significa, con un algoritmo para resolverlo donde se expresa \textit{cómo} hacerlo. La brecha entre\pagina{36} el \textit{qué} y el \textit{cómo} se reduce enormemente en la programación lógica, como puede constatarse en los ejemplos presentados, aún cuando existen dificultades al introducir los componentes de control, tal como se verá en el capítulo siguiente. Una segunda característica muy importante de la programación lógica, se basa en sus aspectos relacionales, que la diferencian de los otros paradigmas que asocian funciones a los programas. Tanto en la programación imperativa tradicional como en la programación funcional, queda perfectamente establecido la dependencia entre datos de entrada y resultados de la ejecución. El flujo de información es un elemento de diseño, y un cambio del mismo implica una modificación importante del programa. Supóngase por ejemplo que se dispone de un programa en PASCAL (o en ADA, o en cualquier lenguaje clásico), que computa la función \textit{concatenación} en el sentido que recibe dos listas (\texttt{X} y \texttt{Y}) como datos de entrada, y devuelve como resultado la lista (\texttt{Z}) obtenida de concatenar la primera con la segunda ($Z=X*Y$). Si en un momento dado resulta necesario cambiar ligeramente las condiciones del problema, por ejemplo dadas dos listas (\texttt{X} y \texttt{Z}), se desea calcular una tercera lista (\texttt{Y}) tal que esta última concatenada a la derecha con el primer argumento dé como resultado el segundo argumento ($Z=X*Y$), entonces se debe proceder a realizar cambios sustanciales en el programa original. El aspecto relacional de la programación en lógica le da un carácter de reversibilidad a sus argumentos, y el mismo programa permite, en general, todas las combinaciones posibles de dependencias de entrada/salida. Si se considera el programa \texttt{CONCAT} ya visto, las siguientes son utilizaciones posibles del mismo: \begin{verbatim} <- CONCAT ( (a b), (c d), Z ). \end{verbatim} \noindent la ejecución da como resultado \begin{verbatim} Z = (a b c d). \end{verbatim} \begin{verbatim} <- CONCAT ( (a b), Y, (a b c d) ). \end{verbatim} \noindent la ejecución da como resultado \begin{verbatim} Y = (c d). \end{verbatim} \pagina{37} \begin{verbatim} <- CONCAT ( X, Y, (a b) ). \end{verbatim} \noindent la ejecución da como resultados \begin{verbatim} X = () , Y = (a b). X = (a) , Y = (b). X = (a b) , Y = (). \end{verbatim} \noindent donde «\texttt{()}» representa a la lista vacía (o árbol vacío «\texttt{[\,]}»). La sintaxis de la programación en lógica presentada proviene de la correspondiente a la lógica de primer orden. En el lenguaje de dicha lógica se utilizan los vocabularios ya mencionados, así como conectores lógicos y los cuantificadores (universal y existencial). Con miras a unificar el tratamiento de las fórmulas bien formadas de la lógica de primer orden se han definido diversas formas normales. Entre ellas resulta de particular interés la llamada forma clausal de Skolem, cuyo formato general es el siguiente: \begin{equation*} \forall X_1 \ldots X_j\ (A_1 \vee \ldots \vee A_n \vee \neg B_1 \vee \ldots \vee \neg B_m) \qquad (IV) \end{equation*} \noindent donde los $A_i$ y los $B_j$ son predicados en el sentido de la definición vista. En dicho formato no aparecen los cuantificadores existenciales, y que los predicados están relacionados únicamente por el conector~$\vee$. La distinción en utilizar los símbolos $A$ y $B$, tiene el propósito de destacar que los segundos están prefijados por el símbolo de negación. Se puede demostrar que para toda fórmula bien formada del cálculo de predicados, existe una fórmula en forma clausal de Skolem tal que ambas tienen las mismas propiedades de satisfactibilidad semántica. Por propiedades bien conocidas de los conectores lógicos es fácil ver que la fórmula (IV) es equivalente a la siguiente: $$ \forall X_1 \ldots X_j\ (A_1 \vee \ldots \vee A_n \leftarrow B_1 \wedge \ldots \wedge B_m ) \qquad (V) $$ \begin{definicion}[Cláusulas de Horn]\pagina{38} Una fórmula bien formada del cálculo de predicados de primer orden está en forma clausal de Horn si: \begin{itemize} \item está en forma clausal de Skolem \item tiene a lo sumo un predicado \textit{positivo} (no prefijado con~$\neg$) \end{itemize} \end{definicion} Resulta evidente que las cláusulas de Horn conforman un subconjunto estricto del lenguaje del cálculo de predicados de primer orden. De acuerdo a la definición son tres las posibilidades para las cláusulas de Horn: $$ \begin{array}{ll} \forall X_1 \ldots X_j\ ( A \leftarrow B_1 \wedge \ldots \wedge B_m ) & \mathrm{(VI)}\\ \forall X_1 \ldots X_j\ ( A ) & \mathrm{(VII)}\\ \forall X_1 \ldots X_j\ ( \neg B_1 \vee \ldots \vee \neg B_m ) & \mathrm{(VIII)} \end{array} $$ \noindent que es equivalente a: $$ \not\exists X_1 \ldots X_j\ ( B_1 \wedge \ldots \wedge B_m ) \qquad\qquad (IX) $$ Dado que en la forma clausal los únicos cuantificadores que aparecen son los universales, pueden entonces ser suprimidos, interpretando toda cláusula como clausurada universalmente. Al proceder de esta manera se puede reconocer que los tres tipos posibles de cláusulas para la programación en lógica (I, II, y III) corresponden a variaciones sintácticas de las formas VI, VII y IX. De esta forma es posible dar una interpretación a cada tipo de cláusulas. Las de tipo (I) corresponden a la afirmación del predicado $A$ por parte del programador. Las del tipo (II) representan los hechos condicionales: $\mathrm{si}\ B_1\ \mathrm{y}\ B_2\ \mathrm{y}\ \ldots\ \mathrm{y}\ B_m$ son predicados ciertos, entonces $A$ también es cierto. Finalmente las cláusulas de tipo (III) corresponden a las invocaciones de ejecución del programa, o si se prefiere a las interrogaciones de las relaciones definidas: ¿existen valores de las variables $X_1, \ldots, X_j$ tales que con dichos valores los predicados $B_1\ \mathrm{y}\ B_2\ \mathrm{y}\ \ldots\ \mathrm{y}\ B_m$ son ciertos? % -------------------------------------------------------- \section{Semántica de programas en lógica} \label{sec:semanticaprogramaslogica} Tal\pagina{39} como surge de la definición sintáctica de los programas en lógica, los mismos se estructuran a partir de conceptos elementales que llamamos \emph{átomos}. Dichos átomos tienen una estructura lexicográfica bien definida: sucesión de caracteres válidos en un vocabulario dado. Pero lo que es importante, es que carecen de todo valor semántico, y es por ello que a los lenguajes con esta concepción se les llama lenguajes de manipulación simbólica. Esta carencia de valor semántico también es aplicable a los símbolos funcionales y predicativos. Sin embargo todo usuario al escribir un programa tiene una intencionalidad semántica bien definida. Así en el ejemplo de la introducción, pocos pueden dudar que lo que se pretende con dicho programa es establecer relaciones familiares entre personas. Por otra parte, cuando se plantea una pregunta, la misma tiene también un valor semántico preciso para el usuario. Esta (aparente) falta de conexión entre los objetos sintácticos y el significado asociado a los mismos, no impide que los sistemas que procesan programas en lógica los evalúen de acuerdo a las expectativas semánticas del programa en cuestión. Desde el punto de vista de la interpretación lógica, la explicación proviene del hecho que cada invocación para la ejecución de un programa es considerada como una fórmula a ser demostrada como consecuencia lógica de la teoría formada por las reglas del programa. Esto significa que para cualquier interpretación que hace \emph{verdaderos} los elementos del programa, hará también \emph{verdadera} a la fórmula de la pregunta. \begin{definicion}[Interpretación] Sea $R$ un programa en lógica, con sus vocabularios: \begin{itemize} \item $V$ de átomos. \item $F$ de símbolos funcionales. \item $P$ de símbolos predicativos. \end{itemize} \noindent Sea\pagina{40} $D$ un conjunto (dominio) dado. Una interpretación $I(D)$ sobre el programa $R$ asigna: \begin{enumerate}[i.] \item a cada elemento de $V$, un elemento de $D$. \item a cada elemento $f$ de $F$, una función de $$ D^n \longrightarrow D $$ \noindent siendo $n$ la aridad del símbolo $f$. \item a cada elemento $p$ de $P$ una función de $$ D^n \longrightarrow (\mbox{verdadero},\mbox{falso}) $$ \noindent siendo $n$ la aridad del símbolo $p$. \end{enumerate} \end{definicion} \begin{definicion}[Satisfacción lógica] Una interpretación $I(D)$ satisface a una fórmula $f$, ssi su aplicación sobre la fórmula da como resultado «verdadero». Una interpretación $I(D)$ satisface a un conjunto de fórmulas $R$, ssi satisface a toda fórmula de $R$. \end{definicion} \begin{definicion}[Consecuencia lógica o deducción] Una fórmula $f$ es consecuencia lógica, o se deduce, de un conjunto de fórmulas $R$, ssi para todo dominio $D$, toda interpretación $I(D)$ que satisface $R$, satisface también a $f$. \end{definicion} \begin{notacion} Si $f$ es consecuencia lógica de $R$, se escribirá $R \models f$. \end{notacion} El concepto de consecuencia lógica es el que permite determinar la forma en que los programas en lógica son evaluados. La aparente falta de conexión que aparecía entre los elementos sintácticos y sus significados, se resuelve al considerar una invocación de ejecución de un programa como una fórmula que debe probarse como consecuencia lógica de éste. Es decir que dicha fórmula debe ser satisfecha para \emph{toda}\pagina{41} interpretación que satisfaga al programa, lo que en definitiva libera a la prueba de todo valor semántico que pudiera haberle asignado el usuario en el momento de la concepción del programa. De acuerdo a lo que se acaba de presentar, una ejecución corresponde a una prueba de consecuencia lógica, y ésta según la definición implicaría una desmostración que involucraría a toda intrepretación posible del programa a evaluar. Existen sin embargo otros mecanismos, basados en la derivación sintáctica, que permiten realizar el proceso de la prueba en forma más simple. % -------------------------------------------------------- \section{Inferencia lógica} \label{sec:inferencialogica} La inferencia lógica es un mecanismo de derivación sintáctica que a partir de un conjunto dado de fórmulas permite derivar nuevas fórmulas, utilizando operaciones que se denominan reglas de inferencia. El conjunto inicial de fórmulas son sentencias válidas en un cierto lenguaje y se les llama axiomas. Los axiomas junto a las reglas de inferencia constituyen lo que Frege denomina un sistema formal. Mediante la inferencia lógica, es posible demostrar fórmulas sin necesidad de considerar interpretación alguna. Una prueba será una derivación en el sistema formal, y la utilidad de la misma surgirá de ciertas propiedades de las reglas de inferencia, llamadas de completitud, que serán presentadas más adelante. A los efectos de esta presentación, las fórmulas a considerar serán las que satisfagan los requerimientos sintácticos que fueron introducidos en~\ref{sec:sintaxisprogramaslogica}. En una primera instancia no se considerarán los predicados con variables, para estudiar en detalle los mecanismos de demostración. La influencia de la presencia de variables será considerada en la sección~\ref{sec:unificacion}. Una\pagina{42} de las reglas de inferencia más conocida, y que forma parte de numerosos sistemas formales es la denominada \emph{modus ponens}. Ella se basa en el conector de implicación lógica «$\rightarrow$». \begin{definicion}[Modus ponens] De las fórmulas $A$ y $A\rightarrow B$, se puede inferir $B$, lo que usualmente se escribe de la siguiente forma: $$ \begin{array}{lll} A \\ A & \rightarrow & B \\ \hline B \end{array} $$ \end{definicion} En lo que sigue se presentan una serie de definiciones que serán utilizadas posteriormente. En un sistema formal, un paso de inferencia corresponde a la aplicación de una regla para inferir una nueva fórmula. \begin{definicion}[Demostración] Una demostración será una sucesión $F_1, F_2, \ldots, F_n$ de fórmulas del lenguaje, tal que todo $F_i$ es un axioma, o se obtiene de las fórmulas anteriores en la sucesión por la aplicación de alguna regla de inferencia. \end{definicion} \begin{definicion}[Teorema] Una fórmula $F$ es un teorema si existe una demostración en la que $F$ es el último término de la sucesión. \end{definicion} \begin{notacion} Si $F$ es un teorema se notará $\vdash F$ \end{notacion} \begin{definicion}[Deducción lógica]\pagina{43} Sea $F$ una fórmula y $R$ un conjunto de fórmulas de una cierta teoría, se dice que $F$ es deducible lógicamente a partir de $R$, y se escribe $R \vdash F$, si existe una sucesión de fórmulas $F_1, F_2, \ldots, F_n$ tal que $F = F_n$ y cada $F_i$ es \begin{itemize} \item un axioma de la teoría \item o una fórmula de $R$ \item o deducible de un fórmula precedente en la sucesión. \end{itemize} \noindent Las fórmulas de $R$ se llaman hipótesis. \end{definicion} \begin{notacion} Si $A$ es deducible lógicamente de $R$ se notará: $R \vdash A$ \end{notacion} Una propiedad importante, que será utilizada más adelante, es la siguiente: \begin{definicion}[Consistencia] Un sistema formal, en el que existe el símbolo de la negación «$\neg$» se dice que es consistente si no existe una fórmula $F$ en el sistema tal que pueda deducirse $F$ y $\neg F$. Un sistema se llama inconsistente en caso contrario. \end{definicion} Resumiendo los conceptos presentados, se han introducido dos alternativas vinculadas con la idea de prueba de fórmulas. En primer lugar se tiene el concepto de \emph{satisfacción lógica}, que tiene connotaciones semánticas, y que en definitiva es la que interesa cuando se intenta dar un significado a la ejecución de un programa en lógica. Sin embargo no parece evidente encontrar mecanismos automatizables para la prueba, que consideren todas las interpretaciones posibles, tal como\pagina{44} se necesita a partir de la definición de satisfacción lógica. En segundo lugar se presentó el mecanismo de inferencia lógica, que basado en elementos sintácticos, permte definir derivaciones entre fórmulas, e introducir el concepto de \emph{teoremas}, a partir de un conjunto de axiomas, y de las reglas de inferencia utilizadas. Esta alternativa parece ser más útil desde un punto de vista informático, si se encuentran procedimientos que implementen las reglas del sistema. La vinculación entre ambas alternativas surge de la propiedad de \emph{completitud} de las reglas de inferencia. \begin{definicion}[Completitud] Sea un programa en lógica $P$, y una cláusula $p$ que corresponde a una invocación del programa $P$. Sea $Q$ una regla de inferencia. Se dice que $Q$ es completa si se cumple que: $p$ es deducible lógicamente de $P$, utilizando $Q$ ssi $p$ es consecuencia lógica de $P$ O sea $P \vdash p \Leftrightarrow P \models p$ \end{definicion} \begin{nota} En la literatura se encuentra que frecuentemente se le llama robustez (\eningles{\emph{soundness}}) a la parte «sólo si» de la propiedad definida, y completitud a la parte «si» de la misma. \end{nota} Según la definición anterior, si se dispone de reglas de inferencia que cumplan con la propiedad de completitud, alcanza con demostrar la deducibilidad de una fórmula para demostrar que la misma es consecuencia lógica del programa. Dentro del área de automatización de pruebas mediante el concepto de deducibilidad, un aporte importante es debido a Robinson, quien introdujo la llamada \emph{regla de resolución}. \begin{definicion}[Regla de Resolución]\pagina{45} Sean $A_1, \ldots, A_n$ y $B_1, \ldots, B_m$ símbolos predicativos, la regla dice: $$ \begin{array}{l} \neg(A_1, \ldots, A_k, \ldots, A_n) \\ A_k \leftarrow B_1, \ldots, B_m \\ \hline \neg(A_1, \ldots, A_{k-1}, B_1, \ldots, B_m, A_{k+1}, \ldots, A_n) \end{array} $$ \end{definicion} De la definición puede observarse que la regla de resolución resulta particularmente adaptada para los programas en lógica. Una invocación o pregunta, corresponde a fórmulas del primer tipo, y las reglas o cláusulas del programa corresponden al segundo tipo. La aplicación de las reglas introduce una nueva cláusula producto de la anulación o cancelación del predicado $A_k$. Como casos particulares de a regla de resolución se pueden considerar los siguientes: a) $$ \begin{array}{rll} \neg A & & \\ A & \leftarrow & B \\ \hline \neg B \end{array} $$ \noindent llamada \emph{modus tollens}. b) $$ \begin{array}{rr} \neg A \\ A & \qquad\mbox{o «} A \leftarrow .\mbox{» según la sintaxis.}\\ \cline{1-1} [] \end{array} $$ \noindent que significa que se ha concluído con una contradicción. El aporte realmente importante de la regla de resolución surge del siguiente teorema. \begin{teorema}[Completitud de la resolución]\pagina{46} La regla de resolución es completa. \end{teorema} En virtud de lo anterior es posible concebir un sistema de demostración automática que evalúe los programas en lógica, mediante la aplicación reiterada de la regla de resolución, tratando de demostrar la deducibilidad lógica de la invocación. Una manera de realizar la prueba es la llamada prueba por contradicción o por reducción al absurdo, que se basa en el siguiente teorema. \begin{teorema} Sea $F$ una fórmula y $R$ un conjunto de fórmulas. $F$ es deducible lógicamente a partir de $R$, ssi el conjunto formado por $R$ con $\neg F$ es inconsistente. O sea, $$ R \vdash F \Leftrightarrow R \cup \{ \neg F \} \mbox{ es inconsistente} $$ \end{teorema} Las definiciones y teoremas presentados son la base para comprender el significado de los programas en lógica, y de la ejecución de los mismos. Las demostraciones se han omitido para abreviar la exposición. El lector interesado puede encontrar una presentación formal y completa de estos temas en el libro de E.~Mendelson~\cite{Men64}, y un buen resumen de los mismos en el primer capítulo de la tesis de R.~Caferra~\cite{Caf82}. Es posible ahora presentar un modelo sobre la evaluación de un programa en lógica. De la definición sintáctica se sabe que los tres tipos de reglas posibles en programación en lógica son: $$ \begin{array}{lcll} A & \leftarrow & . & \mathrm{(I)}\\ A & \leftarrow & B_1, \ldots, B_m & \mathrm{(II)}\\ & \leftarrow & B_1, \ldots, B_m & \mathrm{(III)} \end{array} $$\pagina{47} Las reglas tipo (I) y (II) corresponden a las fórmulas que conforman el programa: en el sistema lógico representan los axiomas. Las fórmulas de tipo (III) son las invocaciones de ejecución, y si se recuerda su interpretación como cláusulas de Horn, representan a la negación de la conjunción de los $B_i$, tal como aparece en la fórmula (IX) vista anteriormente. El modelo se presenta fácilmente mediante un ejemplo. \begin{ejemplo} Sea el programa $P$: $$ \begin{array}{lcll} A & \leftarrow & . & (1)\\ B & \leftarrow & . & (2)\\ D & \leftarrow & . & (3)\\ C & \leftarrow & D, A. & (4)\\ F & \leftarrow & C, B. & (5) \end{array} $$ \noindent y la invocación dada por la fórmula $p$: $$ \begin{array}{lcll} & \leftarrow & F. & (6) \end{array} $$ \noindent La intención es probar que $$P \models F$$ \noindent lo que se realiza demostrando mediante la regla de resolución que: $$P \vdash F$$ \noindent Realizando la demostración por el absurdo, el procedimiento será probar que: el conjunto $P \cup \{\neg F\}$ es inconsistente. \noindent Pero la fórmula $p$ es $\neg F$, por lo que se debe demostrar es que: el conjunto $P \cup \{ p \}$ es inconsistente Para demostrar que el conjunto 1-6 es inconsistente se va aplicando resolución para inferir nuevas cláusulas. Por ejemplo: \begin{quotation}\pagina{48} \begin{tabbing} De (2) y (10) \= se infiere \= $\leftarrow D, A, B$ \= (11) \kill De (5) y (6) \> se infiere \> $\leftarrow C, B$ \>(7)\\ De (4) y (7) \> se infiere \> $\leftarrow D, A, B$ \> (8)\\ De (3) y (8) \> se infiere \> $\leftarrow A, B$ \>(9)\\ De (1) y (9) \> se infiere \> $\leftarrow B$ \> (10)\\ De (2) y (10) \> se infiere \> $\leftarrow [\,]$ \>(11) \end{tabbing} \end{quotation} \noindent El paso (11) indica que se ha inferido el conjunto vacío. Esto surge de considerar las reglas (2) y (10). La primera afirma $B$ y la segunda afirma $\neg B$, por lo tanto el sistema es inconsistente. \end{ejemplo} De la evaluación del ejemplo surgen las siguientes consideraciones: \begin{enumerate} \item Una invocación corresponde a una cláusula de tipo (III) con un solo símbolo predicativo. \item Las nuevas cláusulas que se van infiriendo corresponden a clásulas de tipo (III), donde cada uno de los símbolos predicativos que aparecen en ellas corresponderán a pasos de inferencia que deberán ser realizados. \item Cuando la resolución se aplica entre una cláusula de tipo (II) y una $b$ de tipo (III), la cláusula obtenida tiene los símbolos de $b$, menos el símbolo consecuente de $a$, que ha sido sustituído por el conjunto de sus antecedentes. Aquí la cláusula obtenida tiene más, o la misma cantidad de símbolos que $b$. \item La estrategia de la demostración consiste en buscar inferir la cláusula vacía ($[\,]$). \end{enumerate} % -------------------------------------------------------- \section{Unificación} \label{sec:unificacion} En la sección anterior se ha hecho hincapié en el proceso de la demostración, y para ello no se han considerado las variables que pueden aparecer en los predicados, tal como lo expresa la sintaxis de los programas en lógica. Se\pagina{49} asume que las variables de una cláusula están cuantificadas universalmente, y tienen como \emph{alcance} a la propia cláusula. En estos casos el procedimiento de demostración es similar a lo ya visto, salvo que es necesario contemplar la presencia de variables. La resolución se realizará sólo cuando es posible encontrar una instanciación de las variables que hacen iguales los predicados a anular. Por ejemplo, sea el programa siguiente: \begin{verbatim} PADRE ( jorge, diego ) <- . (1) HERMANO ( ricardo, jorge ) <- . (2) TIO(X, Y) <- PADRE(Z, Y), HERMANO(X, Z). (3) \end{verbatim} La tercera cláusula, como se ha dicho, está cuantificada universalmente para las variables \texttt{X}, \texttt{Y} y \texttt{Z}. Si se considera la invocación: \begin{verbatim} <- TIO ( W, diego ). (4) \end{verbatim} \noindent La demostración se realiza de la forma siguiente: \begin{enumerate}[i)] \item\label{enu:pasouno} La cláusula (3) está cuantificada universalmente. Por lo tanto es también válida para el caso que la variable \texttt{Y} tenga como valor \texttt{diego}, situación que puede representarse por \begin{verbatim} TIO(X, diego) <- PADRE(Z, diego), HERMANO(X, Z) (5) \end{verbatim} \item Como las variables tienen por alcance la cláusula donde aparecen, entonces (4) no cambia si se reemplaza \texttt{W} por \texttt{X}. Hecho esto es posible \emph{resolver} (4) y (5), pues se ha encontrado una instanciación de (3) que lo posibilita. De esta forma se obtiene: \begin{verbatim} <- PADRE(Z, diego), HERMANO(X, Z) (6) \end{verbatim} \item Se\pagina{50} busca ahora resolver (1) con (6) a través del predicado \texttt{PADRE}. Nuevamente es necesario encontrar una instanciación, esta vez en (6), obteniéndose: \begin{verbatim} PADRE(jorge, diego), HERMANO(X, jorge) (7) \end{verbatim} \item Ahora es posible la resolución buscada, realizándola entre (1) y (7), lo que permite inferir: \begin{verbatim} HERMANO(X, jorge) (8) \end{verbatim} \item\label{enu:pasocinco} Finalmente, e instanciando \texttt{X} en (8) con \texttt{ricardo} se puede resolver la nueva cláusula con (2), obteniéndose: \begin{verbatim} [ ] \end{verbatim} \end{enumerate} Los pasos~\ref{enu:pasouno}) a~\ref{enu:pasocinco}) constituyen la demostración de la fórmula (4). Resulta claro que al escribir dicha fórmula el usuario no estaba directamente interesado en una prueba, sino que más bien quería conocer quién es \texttt{TIO} de \texttt{diego}. La variable \texttt{W} original fue cambiada por \texttt{X} en el paso~\ref{enu:pasouno}), y esa variable fue instanciada en el paso~\ref{enu:pasocinco}) para completar la prueba. El valor que le fue asignado, es decir, \texttt{ricardo}, es la respuesta que da el sistema, y que corresponde al interés inicial del usuario. El problema que se plantea para la regla de resolución es entonces cómo \emph{resolver} dos predicados que tengan el mismo símbolo predicativo, pero que sus argumentos no coinciden. El mecanismo que va a permitir resolver dicho problema es el llamado de \emph{unificación}. \begin{definicion}[Sustitución]\pagina{51} Una sustitución es un conjunto de asignaciones del tipo: $$X := t$$ \noindent donde $X$ es una variable y $t$ es un término, en el sentido de la definición sintáctica de los programas en lógica. En una sustitución no pueden existir más de una asignación a la misma variable. \end{definicion} \paragraph{Ejemplos} \mbox{} $$ \begin{array}{l} \{ X := \mbox{juan}, Y := \mbox{noe} \}\\ \{ W := Z, R := \mbox{empleado}(T, 1200) \}\\ \{ Q := [\,], X := [ Y, Z ] \} \end{array} $$ \begin{definicion}[Aplicación de sustitución] Dada una sustitución $\theta$, y un predicado $P$, la aplicación de $\theta$ a $P$ produce un nuevo predicado, que se denota $P\theta$, y que corresponde al predicado inicial $P$, donde toda variable asignada en $\theta$ es cambiada por el término correspondiente, y las otras variables permanecen incambiadas. \end{definicion} \begin{definicion}[Unificador] Dadas dos expresiones del lenguaje definido, por ejemplo dos predicados $$E_1, E_2$$ \noindent se llama unificador a una sustitución $\theta$ tal que se cumple que: $$E_1\theta = E_2\theta$$ \noindent Es decir que la aplicación de la sustitución a ambas expresiones, da la misma expresión. \end{definicion} \paragraph{Ejemplos}\pagina{52} \begin{enumerate} \item Dadas las expresiones \begin{center} \texttt{PADRE ( Z , diego)} y \texttt{PADRE ( jorge , diego)} \end{center} \noindent la sustitución $\theta$\texttt{ = \{ Z := jorge \}} es un unificador de las mismas. \item Dadas las expresiones \begin{center} \texttt{TIO ( X , diego)} y \texttt{TIO ( W , diego)} \end{center} \noindent la sustitución $\theta$\texttt{ = \{ X := W \}} es un unificador de las mismas. La sustitución $\theta$\texttt{ = \{ W := X \}} también es un unificador. La sustitución $\theta$\texttt{ = \{ X := guillermo, W := guillermo \}} también es un unificador. \item Dadas las expresiones $$ Q( q(X,Y), X, h(4)) \quad \mathrm{y} \quad Q( q(3,Z), W, h(Z)) $$ \noindent la sustitución $\theta = \{X:= 3, Z:= 4, W:= 3, Y:= 4\}$ es un unificador de las mismas. \item Sean las expresiones \begin{center} \texttt{R ( [X . Y] )} y \texttt{ R( [[a.[b.[]]].[c.[d.[]]]] )} \end{center} Debe recordarse que el término \texttt{[[a.[b.[]]].[c.[d.[]]]]} corresponde a la lista $((a\ b)\ c\ d)$. La sustitución $\theta$\texttt{ = \{ X:= [a.[b.[]]], Y := [c.[d.[]]]\}} es un unificador de las mismas. En notación de listas: $\theta = \{ X:= (a\ b), Y:= (c\ d)\}$. Si se utiliza la notación de listas, lo que frecuentemente resulta muy cómodo, la expresión \texttt{[X.Y]} representa una lista, donde, según otros lenguajes, \texttt{X} corresponde al «\texttt{CAR}», «\emph{head}» o «\emph{cabeza}» de la lista; \texttt{Y} corresponde al «\texttt{CDR}», «\emph{tail}», o «\emph{resto}» de la misma; «\texttt{.}» corresponde al constructor «\texttt{CONS}». \item Dadas las expresiones \begin{center} \texttt{R ( [X . Y] )} y \texttt{ R( [] )} \end{center} No existe un unificador para ambas. \end{enumerate} De\pagina{53} la definición de unificador y de los ejemplos presentados surge que existen expresiones para las cuales no existe un unificador, mientras que en otros casos es posible encontrar más de un unificador. Para el procedimiento de demostración, y en caso de existir más de un unificador entre dos predicados que permita aplicar la regla de resolución, va a interesar aquel que sea \emph{más general}, en el sentido que necesite asignaciones menos específicas de términos a variables. En el ejemplo 2. visto anteriormente, los dos primeros unificadores, que en definitiva son el mismo ---a menos de un renombramiento--- son más generales que el tercero. \begin{definicion}[Unificador más general] Dadas dos sustituciones $\theta_1$ y $\theta_2$ y que ambas son unificadores de las expresiones $E_1$ y $E_2$, se dice que $\theta_1$ es más general que $\theta_2$ si existe una sustitución $\theta_3$ tal que: $$ E_1 \theta_1 \theta_3 = E_2 \theta_2 $$ La relación «más general que» es un preorden. Al mínimo del preorden «más general que» se le llama \emph{unificador más general}. \end{definicion} Existen múltiples propuestas de algoritmos para calcular el unificador más general, y ello se debe a que dicho algoritmo tiene una importancia capital en el proceso de la demostración. % -------------------------------------------------------- \section{Evaluación de programas en lógica} \label{sec:evaluacionprogramaslogica} En las secciones precedentes se ha visto la síntesis de los programas en lógica, así como las bases lógicas que permiten dar un significado a la ejecución de los mismos. En lo que sigue se presentarán las acciones a cumplir para ejecutar un paso de inferencia usando resolución. Se\pagina{54} dispone de un programa $P$ formado por las cláusulas de tipo I) y II) ya vistas, y una cláusula de tipo III) $$ \leftarrow Q_1, \ldots, Q_m $$ \noindent que corresponde a la invocación de ejecución. Al conjunto $Q = \{ Q_1, \ldots, Q_m \}$ se le denomina conjunto de objetivos. LA evaluación del programa implica la aplicación de la regla de recolución. Para cada paso de inferencia se procede siguiendo los pasos siguientes: \begin{enumerate} \item Se elige un predicado del conjunto $Q$ tal que su símbolo predicativo sea igual al símbolo del predicado consecuente de una regla del programa. Si esto no es posible fracasa el paso inferencial. \item Se calcula el unificador «más general» entre el predicado escogido y el consecuente de la regla determinada en el paso anterior. Si no existe tal unificador, entonces fracasa el paso de inferencia. \item Se reemplaza en el conjunto $Q$ el predicado escogido, por el conjunto de predicados que aparecen como antecedentes de la regla determinada; si la regla es de tipo I), entonces se elimina el predicado de $Q$. En este paso se modifica el conjunto $Q$, eventualmente convirtiéndolo en el conjunto vacío. \item Se aplica el unificador más general a todos lo predicados de $Q$. \end{enumerate} \paragraph{Ejemplo} Sea el programa en lógica para la concatenación de listas que ya fue presentado: \begin{verbatim} CONCAT( [], X, X ) <- . (1) CONCAT( [X.L], Y, [X.Z] ) <- CONCAT( L, Y, Z ). (2) \end{verbatim} \noindent y la invocación: \pagina{55}% \begin{verbatim} <- CONCAT ( [a.[]], [b.[]], W ). \end{verbatim} El conjunto de objetivos a ser demostrado es: $$ Q = \{ \mathtt{CONCAT ( [a.[]], [b.[]], W )} \} $$ \begin{enumerate}[i] \item La regla (1) no puede resolverse con el único predicado de $Q$. Dicha regla necesita que su primer argumento sea la lista vacía, mientras que el predicado tiene en ese argumento una lista no vacía. \item Se resuelve la regla (2) con el objetivo, mediante la sustitución $$ \theta_1 = \{ \mathtt{X:=a, L:=[], Y:=[b.[]], W:=[a.Z]} \} $$ \item Se sustituye el predicado de $Q$ por el antecedente de la regla, y se le aplica la sustitución anterior quedando $$ Q = \{ \mathtt{CONCAT ( [], [b.[]], Z )} \} $$ \item El nuevo y único predicado de $Q$ no puede resolverse con la regla (2) debido al primer argumento de \texttt{CONCAT}. El de la regla es \texttt{[X.L]}, y ello indica, por la existencia del símbolo funcional «\texttt{.}», que se necesita una lista con al menos un elemento, mientras que el argumento del predicado de $Q$ es precisamente la lista vacía. \item Se resuelve la regla (1) con el objetivo, mediante la sustitución $$ \theta_2 = \{ \mathtt{X:=[b.[]], Z:=[b.[]]} \} $$ \item Como la regla aplicada es del tipo I), se elimina el predicado del conjunto $Q$, quedando $$ Q = \{ \ \} $$ \noindent por lo que se termina la demostración, concluyéndose que la invocación es consecuencia lógica del programa. Es\pagina{56} que lo que el usuario necesita es el valor de \texttt{W}. \item En el paso ii) la primera sustitución produjo que \begin{verbatim} W := [a.Z] \end{verbatim} \item En el paso v) la segunda sustitución profujo que \begin{verbatim} Z := [b.[]] \end{verbatim} \item De vii) y viii) se concluye que el valor de \texttt{W} que permitió la demostración es: \begin{verbatim} W := [a.[b.[]]] \end{verbatim} \noindent es decir la lista $(a\ b)$ \end{enumerate} \paragraph{Problemas} \begin{enumerate} \item Definir el predicado \texttt{MEMBER(X,L)}que determina si el elemento \texttt{X} pertenece a la lista \texttt{L}. \item Definir los siguientes predicados para listas: \begin{enumerate} \item \texttt{SUFIX(L1,L2)} donde \texttt{L1} es sufijo de \texttt{L2}. \item \texttt{PREFIX(L1,L2)} donde \texttt{L1} es prefijo de \texttt{L2}. \item \texttt{SUBLIST(L1,L2)} donde \texttt{L1} es una sublista de \texttt{L2}. \end{enumerate} \item Escribir un programa en lógica que ordene listas, usando la idea de \emph{quicksort}. \item Definir el predicado \texttt{ISOTREE(T1,T2)} que será verdadero si \texttt{T1} y \texttt{T2} son árboles binarios isomorfos (es decir, iguales a menos de los valores asociados a los nodos). \end{enumerate} % EOF cap03.tex %%% Local Variables: %%% mode: latex %%% TeX-master: "plyf" %%% End: