Para el desarrollo de los aspectos prácticos de la asignatura, que extenderán naturalmente a los aspectos teórico-formales estudiados en la mismas, utilizaremos el lenguaje Elm, de origen declarativo pero con orientación a la interación Web, en concreto con las lobrerías LogicUS, que nos permitirán, a lo largo del curso, trasladar a un entorno más visual cada uno de los conceptos y algoritmos vistos en la asignatura.
En esta primera práctica veremos cómo trasladar los aspectos teórico formales de la sintáxis y semántica proposicionales en LogicUS abordando:
La sintáxis de fórmulas (y sus árboles de formación) y conjuntos proposicionales.
Definición de interpretaciones y evaluación de fórmulas y conjuntos respecto de las interpretaciones.
Satisfactibilidad y validez lógica, modelos y contramodelos, tablas de verdad y consecuencia lógica.
Si recordamos, la definición de las fórmulas proposicionalesn se ha dado como definición recursiva a partir de átomos (variables proposicionales) bajo la aplicación de las conectivas lógicas (negación, conjunción, disyunción, implicación y equivalencia). Siguiendo dicha definición constructiva se establece en LogicUS la estructura de las fórmulas de forma que:
Los símbolos proposicionales se definen como cadenas de caractéres (con la restricción de que deben usar minúsculas):
type alias PSymb = String
Las fórmulas proposicionales se definen según la estructura recursiva dada por:
type FormulaLP = Atom PSymb -- caso base | Neg FormulaLP --⎫ | Conj FormulaLP FormulaLP --⎪ | Disj FormulaLP FormulaLP --⎬ casos recursivos | Impl FormulaLP FormulaLP --⎪ | Equi FormulaLP FormulaLP --⎭ | Insat -- fórmula insatisfactible
De forma que se tiene como elemento fundamental el átomo y a partir de éste y con la aplicación de las conectivas a partir de subfórmulas (según la aridad de la conectiva) se permite la definición de cualquier fórmula proposicional. Además, se añade una representación explícita para la fórmula insatisfactible ().
Bien, una vez vista la clara analogía entre el formalismo y la implementación, pasemos directamente a definir las fórmulas. Para ello es necesario importar los módulos necesarios con los que vayamos a trabajar, en este caso bastará importar LogicUS.PL.SintaxSemantics.
Nota: En el repositorio de paquetes de Elm se encuentran los paquetes publicados. En ellos pueden consultarse cómodamete las funciones que se encuentran definidas en cada uno de sus módulos. En concreto para el paquete LogicUS.
Para importar el módulo (ya se da declarado en las dependdencias) es suficiente con ejecutar (en este caso en un chunk de litvis)
import LogicUS.PL.SintaxSemantics exposing (..)
Con exposing se pueden especificar qué funciones y tipos se quieren importar específicamente pero por el momento importaremos todas ellas con (..).
Una vez importados tenemos varias vías para definir las funciones:
Para ello basta con utilizar los constructores (Atom, Neg, Conj, Disj, Impl, Equi, Insat). Para ello, a una variable (el identificador debe comenzar por una letra minúscula) se le asocia la fórmula descrita de forma recursiva de forma que:
Para definir un átomo con la variable "p" basta escrbir:
f = Atom "p"
Para definir la negación de una fórmula, por ejemplo del átomo anterior basta escribir:
f2 = Neg f
o equivalentemente
f2 = Neg (Atom "p")
Para definir la conjunción, disyunción, implicación o equivalencia es necesario dar como argumento dos fórmulas. Por ejemplo, si consideramos la fórmula entonces debemos escribir:
f3 = Conj f f2
o equivalentemente
f3 = Conj (Atom "p") (Neg (Atom "p"))
Hagamos algunas puntualizaciones:
Aunque hemos dicho que realizar f2 = Neg f era equivalente a f2 = Neg (Atom "p") , en realidad no lo es. Elm es un lenguaje funcional y por tanto todos los objetos del lenguaje son funciones. De manera que cuando establecemos Neg f, f no es más que una referencia a la función f de forma que si cambia f entonces consecuentemente cambiará también f2, mientras que en el segundo caso al haberse definido a partir de elementos constantes (constructores y cadenas) entonces "f2" sólo cambiará si se modifica explícitamente.
Nótese que para todos los constructores el formato es similar Identificador Costructor + parámetros. De forma que los parámetros se dan según la aridad del mismo separados por espacios y encerrados entre paréntesis si no constan de un único elemento.
Según lo expuesto intetemos definir algunas funciones.
EJEMPLO: Formalizar los siguientes enunciados, definiendo las fórmulas correspondientes:
Si el sol brilla hoy, entonces no brillará mañana. (: el sol brilla hoy, :el sol brillará mañana)
Llueve o nieva siempre que la presión atmosférica está baja y sólo entonces. (: llueve, :nieva, :la presión está baja)
Si Pablo no se encontró con Chari ayer, entonces no tomaron café juntos ni pasearon por el parque. (: Pablo se encontró con Chari, : Pablo y chari tomaron café juntos, : Plablo y Chari pasearon por el parque)
Apartado 1:
f1 = Impl (Atom "p") (Neg (Atom "q"))
Apartado 2:
f2 = Equi (Disj (Atom "p") (Atom "q")) (Atom "r")
Apartado 3:
f3 = Impl (Neg (Atom "p")) (Conj (Neg (Atom "q")) (Neg (Atom "r")))
Desde luego, escribir las fórmulas a través de los constructores puede convertirse en una tarea ardua y propensa a errores, ya que es necesario construir previamente el árbol de formación y reproducirlo en el lenguaje. Por eso se proporciona una función de parseo que es capaz de leerlas de una cadena. Para que esa cadena pueda ser interpretada correctamente es necesario que cumpla las siguentes condiciones:
Símbolos proposicionales: según la expresión regular:
Esto es, una serie de caracteres en minúscula segidos (opcionalmente) por una lísta de subíndices especificados entre llaves.
Conectivas. Siguiendo la correspondencia y prioridad de asociación:
Las funciones que permiten realizar la lectura y extraerla son fplReadFromString y fplReadExtraction. La primera nos devolverá un error si no puede leer la fórmula.
EJEMPLO: Formalizar los siguientes enunciados, definiendo las fórmulas correspondientes:
Si el sol brilla hoy, entonces no brillará mañana. (: el sol brilla hoy, :el sol brillará mañana)
Llueve o nieva siempre que la presión atmosférica está baja y sólo entonces. (: llueve, :nieva, :la presión está baja)
Si Pablo no se encontró con Chari ayer, entonces no tomaron café juntos ni pasearon por el parque. (: Pablo se encontró con Chari, : Pablo y chari tomaron café juntos, : Plablo y Chari pasearon por el parque)
Apartado 1:
f1 = fplReadExtraction <| fplReadFromString "p -> ¬ q"
Apartado 2:
f2 = fplReadExtraction <| fplReadFromString "p \\/ q <-> r"
Nota: Veáse que el carácter "\" denota un símbolo de escape por lo que para poner la barra invertida es necesario escribir "\\".
Apartado 3:
f3 = fplReadExtraction <| fplReadFromString "¬p -> ¬q /\\ ¬r"
Si hubiésemos querido hacer uso de subíndices, en este último ejemeplo, podríamos haber escrito:
f4 = fplReadExtraction <| fplReadFromString "¬p_{1} -> ¬q_{1} /\\ ¬r_{1}"
Para mostrar las fórmulas podemos utilizar la función fplToString o la función fplToMathString (en formato latex), utilzando los triple hat chuncks.
En teoría se ha visto la representación de fórmulas mediante árboles de formación que contienen cada una de sus subfórmulas. La libería también permite también extraer los árboles de formación de las fórmulas, en concreto, a través de las funciones fplFormTree y fplFormTreeToDOT. La primera es la que computa el árbol mientras que la segunda da una representación del mismo en formato DOT que puede ser renderizado en un visualizador GraphViz.
VISUALIZACIÓN DE DOT EN LITVIS
Litvis posee dicho visualizador en un chunk tipo dot en el cuál podemos pegar la dot String generada. De forma que para visualizar cualquier gráfico DOT generado por la libería podemos hacer los isiguiente:
Crear una variable que la almacene definiendo su tipo como String (var : String).
En el chunk establecer los parámetros l (para mostrar el chunk) y m para ejecutar la salida como markdown lo nos mostrará el código en formato DOT. (Es indispensable establecer el tipo, si no se pone no se mostrará nada).
El código DOT mostrado podemos copiarlo en un chunk dot para visualizarlo.
Para dejar de mostrar el código DOT basta con quitar el parámetro m del chunk.
Por ejemplo si queremos extraer el árbol de formación de la última fórmula que hemos definido: ,
ft_f3 : String ft_f3 = fplFormTreeToDOT <| fplFormTree f3
Visto cómo podemos definir fórmulas, ¿cómo podemos ahora definir conjuntos de fórmulas?. En LogicUS los conjuntos de fórmulas están definidos como listas, de forma que para definir conjuntos es suficiente con definir las fórmulas y después el conjunto como una lista de ellas.
type alias LPSet = List FormulaLP
De forma que si, por ejemplo, queremos definir el conjunto:
Bastaría escribir:
f1 = fplReadExtraction <| fplReadFromString "p /\\ q \\/ p /\\ r" f2 = fplReadExtraction <| fplReadFromString " p /\\ r \\/ ¬ p /\\ q -> ¬q" f3 = fplReadExtraction <| fplReadFromString "(p <-> q) /\\ (q -> p) /\\ p " m = [f1, f2, f3]
Podemos mostrarlo en formato latex utilizando la función splToMathString:
Como se ha estudiado en la teoría, los valores de verdad corresponden a 1 (verdadero) y 0 (falso). Elm ya provee esos valores booleanos en el tipo Bool, por lo que no es necesario realizar ninguna definición alternativa para este concepto.
La definición de las funciones de verdad asociadas a las conectivas corresponden directamente a la aplicación de dichas funciones en la evaluación de las fórmulas. Antes de ver la evaluación resulta necesario ver la definición que se ha dado para las interpretaciones. Para ello, se ha elegido una representación "dispersa" que indica por medio de una lista los símbolos proposicionales de las variables que son tomadas como verdaderas. Las variables proposicionales asociadas a símbolos que no aparecen en la lista serán considerados como falsas.
type alias Interpretation = List PSymb
Con esta definición resulta sencillo llevar a cabo la evaluación de las fórmulas siguiendo exactamente los dos pasos anotados:
Evaluación de variables. Una variable será verdadera si pertenece a la lista de la interpretación, y será falsa en caso contrario.
Evaluación de conectivas. Aplicando las correspondientes funciones características:
fplValuation : FormulaLP -> Interpretation -> Bool fplValuation f i = case f of Atom symb -> List.member symb i Neg g -> not (valuation g i) Conj g h -> valuation g i && valuation h i Disj g h -> valuation g i || valuation h i Impl g h -> not (valuation g i) || valuation h i Equi g h -> valuation (Impl g h) i && valuation (Impl h g) i Insat -> False
NOTA: nótese que la fórmula insatisfactible es falsa respecto de cualquier valoración.
Luego, para realizar la evaluación de una fórmula respecto de una interpretación podemos utilizar la función fplValuation dando la fórmula y la interpretación. De forma que si queremos hallar la valoración de respecto de bastaría definir y y ejecutar la función fplValuation f i.
f = fplReadExtraction <| fplReadFromString "¬ (¬ (p \\/ q) \\/ (¬ r \\/ s))" i = ["p", "q"]
false
De igual modo, se puede hallar la valoración de un conjunto respecto de una valoración. Recuérdese que la valoración de un conjunto respecto a una valoración era verdadera si y sólo si todas las fórmulas del conjunto eran verdaderas respecto de dicha valoración. La función splValuation realiza justamente esta comparativa:
splValuation : PLSet -> Interpretation -> Bool splValuation fs i = List.all (\x -> fplValuation x i) fs
De forma que, análogamente a lo presentado para las fórmulas, bastaría definir el conjunto, la interpretación y ejecutar la función splValuation.
Como se ha estudiado en el correspondiente apartado teórico, una tabla de verdad recoge las valoraciones de una fórmula respecto a todas las posibles interpretaciones de sus símbolos proposicionales. Nótese que dada la implementación propuesta para las interpretaciones, las posibles interpretaciones de una fórmula corresponderían a todos los posibles subconjuntos del conjunto de los símbolos proposicionales de la fórmula (un conjunto de elementos tiene subconjuntos distintos, que justamente coincide con el número de entradas de la tabla de verdad).
En la libería LogicUS existen funciones para calcular los símbolos e interpretaciones, pero pasemos directamente a ver la tabla de verdad, que puede ser calculada mediante la función fplTruthTable de forma que dada una fórmula devuelve un conjunto (lista) de tuplas (Interpretation, Bool) correspondientes a las entradas de la tabla y las correspondientes valoraciones. Además para poderla visualizar cómodamente, se presenta también la función fplTruthTableMathString que recibe una fórmula y devuelve una cadena con la tabla en formato Latex.
De forma que, si queremos construir la tabla de la fórmula anterior bastaría ejecutar fplTruthTableMathString f.
De igual modo, para los conjuntos existen funciones de cálculo y representación de la tabla de verdad: splTruthTable y splTruthTableMathString , respectivamente.
A partir de la tabla de verdad (o directamente de la evaluación de las posibles interpretaciones) es posible extraer los modelos y contramodelos de una fórmula. Recuérdese que los modelos correspondían a las interpretaciones que hacían a la fórmula verdadera y los contramodelos los que la hacían falsa. En LogicUS las funciones fplModels y fplCounterModels realizan precisamente ese filtrado de forma que dada una fórmula devuelven una lista con las interpretaciones modelo y una lista con los contramodelos respectivamente.
De foma que si queremos obtener los modelos de la fórmula bastaría ejecutar fplModels f, dando como resultado:
O fplCountermodels f para los contramodelos:
De forma equivalente para los conjuntos se proporcionan las funciones splModels y splCounterModels
Una vez visto el cálculo de modelos, y dado que la satisfactibilidad y validez lógicas se dan de forma que si todas las interpretaciones hacen a la fórmula verdadera se tiene tautología, si alguna de ellas la hace verdadera se dice satisfactible, o si ninguna la hace se dice insatisfactible. De forma que dadas todas las interpretaciones bastaría comprobar si para todas ellas son modelos, si alguna lo es o si ninguna lo es.
Eso es justamente lo que hacen las funciones fplValidity, fplSatisfiablity y fplUnsatisfiability, de forma que dada una fórmula devuelven si es tautología (válida), satisfactible e insatisfactible, respectivamente. Por ejemplo, la fórmula es satisfactible y no tautología.
De igual forma se definen para los conjuntos las funciones fplSatisfiability y splUnsatisfiability para comprobar la consistencia de un conjunto. Y además se define la consecuencia lógica en la función logicalConsecuence y logicalConsecuence2 que recibiendo un conjunto y una fórmula determinan si , la primera de ellas comparando si todo modelo de lo es también de y la segunda comprobando si .
De forma que, si por ejemplo queremos comprobar si entonces:
f1 = fplReadExtraction <| fplReadFromString "p -> q" f2 = fplReadExtraction <| fplReadFromString "q -> p /\\ r" f3 = fplReadExtraction <| fplReadFromString "p -> (p -> q) -> r"