LMF2012: Sintaxis y semántica de la lógica proposicional en Haskell (1)
En la clase de hoy del curso de Lógica matemática y fundamentos (de 3º de Grado en Matemáticas) se han comentados las soluciones de los ejercicios de revisión de Haskell planteados en la clase anterior y se ha comenzado la solución de los ejercicios sobre la sintaxis y semántica de la lógica proposicional en Haskell.
Las soluciones de los ejercicios corregidos se muestran a continuación
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 |
module SintaxisSemantica where -- --------------------------------------------------------------------- -- Librerías auxiliares -- -- --------------------------------------------------------------------- import Data.List import Test.HUnit import Test.QuickCheck import Control.Monad import Verificacion -- --------------------------------------------------------------------- -- Gramática de fórmulas prosicionales -- -- --------------------------------------------------------------------- -- --------------------------------------------------------------------- -- Ejercicio 1: Definir los siguientes tipos de datos: -- * SimboloProposicional para representar los símbolos de proposiciones -- * FProp para representar las fórmulas proposicionales usando los -- constructores Atom, Neg, Conj, Disj, Impl y Equi para las fórmulas -- atómicas, negaciones, conjunciones, implicaciones y equivalencias, -- respectivamente. -- --------------------------------------------------------------------- type SimboloProposicional = String data FProp = Atom SimboloProposicional | Neg FProp | Conj FProp FProp | Disj FProp FProp | Impl FProp FProp | Equi FProp FProp deriving (Eq,Ord) instance Show FProp where show (Atom p) = p show (Neg p) = "no " ++ show p show (Conj p q) = "(" ++ show p ++ " /\\ " ++ show q ++ ")" show (Disj p q) = "(" ++ show p ++ " \\/ " ++ show q ++ ")" show (Impl p q) = "(" ++ show p ++ " --> " ++ show q ++ ")" show (Equi p q) = "(" ++ show p ++ " <--> " ++ show q ++ ")" -- --------------------------------------------------------------------- -- Ejercicio 2: Definir las siguientes fórmulas proposicionales -- atómicas: p, p1, p2, q, r, s, t y u. -- --------------------------------------------------------------------- p, p1, p2, q, r, s, t, u :: FProp p = Atom "p" p1 = Atom "p1" p2 = Atom "p2" q = Atom "q" r = Atom "r" s = Atom "s" t = Atom "t" u = Atom "u" -- --------------------------------------------------------------------- -- Ejercicio 3: Definir la función -- no :: FProp -> FProp -- tal que (no f) es la negación de f. -- --------------------------------------------------------------------- no :: FProp -> FProp no = Neg -- --------------------------------------------------------------------- -- Ejercicio 4: Definir los siguientes operadores -- (/\), (\/), (-->), (<-->) :: FProp -> FProp -> FProp -- tales que -- f /\ g es la conjunción de f y g -- f \/ g es la disyunción de f y g -- f --> g es la implicación de f a g -- f <--> g es la equivalencia entre f y g -- --------------------------------------------------------------------- infixr 5 \/ infixr 4 /\ infixr 3 --> infixr 2 <--> (/\), (\/), (-->), (<-->) :: FProp -> FProp -> FProp (/\) = Conj (\/) = Disj (-->) = Impl (<-->) = Equi -- --------------------------------------------------------------------- -- Símbolos proposicionales de una fórmula -- -- --------------------------------------------------------------------- -- --------------------------------------------------------------------- -- Ejercicio 5: Definir la función -- simbolosPropForm :: FProp -> [FProp] -- tal que (simbolosPropForm f) es el conjunto formado por todos los -- símbolos proposicionales que aparecen en f. Por ejemplo, -- simbolosPropForm (p /\ q --> p) == [p,q] -- --------------------------------------------------------------------- simbolosPropForm :: FProp -> [FProp] simbolosPropForm (Atom f) = [(Atom f)] simbolosPropForm (Neg f) = simbolosPropForm f simbolosPropForm (Conj f g) = simbolosPropForm f `union` simbolosPropForm g simbolosPropForm (Disj f g) = simbolosPropForm f `union` simbolosPropForm g simbolosPropForm (Impl f g) = simbolosPropForm f `union` simbolosPropForm g simbolosPropForm (Equi f g) = simbolosPropForm f `union` simbolosPropForm g -- --------------------------------------------------------------------- -- Interpretaciones -- -- --------------------------------------------------------------------- -- --------------------------------------------------------------------- -- Ejercicio 6: Definir el tipo de datos Interpretacion para -- representar las interpretaciones como listas de fórmulas atómicas. -- --------------------------------------------------------------------- type Interpretacion = [FProp] -- --------------------------------------------------------------------- -- Significado de una fórmula en una interpretación -- -- --------------------------------------------------------------------- -- --------------------------------------------------------------------- -- Ejercicio 7: Definir la función -- significado :: FProp -> Interpretacion -> Bool -- tal que (significado f i) es el significado de f en i. Por ejemplo, -- significado ((p \/ q) /\ ((no q) \/ r)) [r] == False -- significado ((p \/ q) /\ ((no q) \/ r)) [p,r] == True -- --------------------------------------------------------------------- significado :: FProp -> Interpretacion -> Bool significado (Atom f) i = (Atom f) `elem` i significado (Neg f) i = not (significado f i) significado (Conj f g) i = (significado f i) && (significado g i) significado (Disj f g) i = (significado f i) || (significado g i) significado (Impl f g) i = significado (Disj (Neg f) g) i significado (Equi f g) i = significado (Conj (Impl f g) (Impl g f)) i -- --------------------------------------------------------------------- -- Interpretaciones de una fórmula -- -- --------------------------------------------------------------------- -- --------------------------------------------------------------------- -- Ejercicio 8: Definir la función -- subconjuntos :: [a] -> [[a]] -- tal que (subconjuntos x) es la lista de los subconjuntos de x. Por -- ejmplo, -- subconjuntos "abc" == ["abc","ab","ac","a","bc","b","c",""] -- --------------------------------------------------------------------- subconjuntos :: [a] -> [[a]] subconjuntos [] = [[]] subconjuntos (x:xs) = [x:ys | ys <- xss] ++ xss where xss = subconjuntos xs -- --------------------------------------------------------------------- -- Ejercicio 9: Definir la función -- interpretacionesForm :: FProp -> [Interpretacion] -- tal que (interpretacionesForm f) es la lista de todas las -- interpretaciones de f. Por ejemplo, -- interpretacionesForm (p /\ q --> p) == [[p,q],[p],[q],[]] -- --------------------------------------------------------------------- interpretacionesForm :: FProp -> [Interpretacion] interpretacionesForm f = subconjuntos (simbolosPropForm f) |