{"id":2538,"date":"2013-02-27T17:33:55","date_gmt":"2013-02-27T17:33:55","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=2538"},"modified":"2013-05-02T11:39:47","modified_gmt":"2013-05-02T11:39:47","slug":"lmf2013-sintaxis-y-semantica-de-la-logica-proposicional-en-haskell","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/lmf2013-sintaxis-y-semantica-de-la-logica-proposicional-en-haskell\/","title":{"rendered":"LMF2013: Sintaxis y sem\u00e1ntica de la l\u00f3gica proposicional en Haskell"},"content":{"rendered":"<p>En la clase de hoy del curso de <a href=\"http:\/\/www.cs.us.es\/~jalonso\/cursos\/lmf-12\">L\u00f3gica matem\u00e1tica y fundamentos<\/a> (de 3\u00ba de Grado en Matem\u00e1ticas) se han comentado las soluciones de los 11 primeros ejercicios de la sintaxis y sem\u00e1ntica de la l\u00f3gica proposicional en Haskell.<\/p>\n<p>Las soluciones de los ejercicios corregidos se muestran a continuaci\u00f3n<br \/>\n<!--more--><\/p>\n<pre lang=\"haskell\">\r\nmodule SintaxisSemantica where\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Librer\u00edas auxiliares                                               --\r\n-- ---------------------------------------------------------------------\r\n\r\nimport Data.List \r\n\r\n-- ---------------------------------------------------------------------\r\n-- Gram\u00e1tica de f\u00f3rmulas prosicionales                                --\r\n-- ---------------------------------------------------------------------\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Ejercicio 1: Definir los siguientes tipos de datos:\r\n-- * SimboloProposicional para representar los s\u00edmbolos de proposiciones\r\n-- * Prop para representar las f\u00f3rmulas proposicionales usando los\r\n--   constructores Atom, Neg, Conj, Disj, Impl y Equi para las f\u00f3rmulas\r\n--   at\u00f3micas, negaciones, conjunciones, implicaciones y equivalencias,\r\n--   respectivamente.  \r\n-- ---------------------------------------------------------------------\r\n\r\ntype SimboloProposicional = String\r\n\r\ndata Prop = Atom SimboloProposicional\r\n          | Neg Prop \r\n          | Conj Prop Prop \r\n          | Disj Prop Prop \r\n          | Impl Prop Prop \r\n          | Equi Prop Prop \r\n          deriving (Eq,Ord)\r\n\r\ninstance Show Prop where\r\n    show (Atom p)   = p\r\n    show (Neg p)    = \"no \" ++ show p\r\n    show (Conj p q) = \"(\" ++ show p ++ \" \/\\\\ \" ++ show q ++ \")\"\r\n    show (Disj p q) = \"(\" ++ show p ++ \" \\\\\/ \" ++ show q ++ \")\"\r\n    show (Impl p q) = \"(\" ++ show p ++ \" --> \" ++ show q ++ \")\"\r\n    show (Equi p q) = \"(\" ++ show p ++ \" <--> \" ++ show q ++ \")\"\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Ejercicio 2: Definir las siguientes f\u00f3rmulas proposicionales\r\n-- at\u00f3micas: p, p1, p2, q, r, s, t y u.\r\n-- ---------------------------------------------------------------------\r\n\r\np, p1, p2, q, r, s, t, u :: Prop\r\np  = Atom \"p\"\r\np1 = Atom \"p1\"\r\np2 = Atom \"p2\"\r\nq  = Atom \"q\"\r\nr  = Atom \"r\"\r\ns  = Atom \"s\"\r\nt  = Atom \"t\"\r\nu  = Atom \"u\"\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Ejercicio 3: Definir la funci\u00f3n\r\n--    no :: Prop -> Prop\r\n-- tal que (no f) es la negaci\u00f3n de f.\r\n-- ---------------------------------------------------------------------\r\n\r\nno :: Prop -> Prop\r\nno = Neg\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Ejercicio 4: Definir los siguientes operadores\r\n--    (\/\\), (\\\/), (-->), (<-->) :: Prop -> Prop -> Prop\r\n-- tales que\r\n--    f \/\\ g      es la conjunci\u00f3n de f y g\r\n--    f \\\/ g      es la disyunci\u00f3n de f y g\r\n--    f --> g     es la implicaci\u00f3n de f a g\r\n--    f <--> g    es la equivalencia entre f y g\r\n-- ---------------------------------------------------------------------\r\n\r\ninfixr 5 \\\/\r\ninfixr 4 \/\\\r\ninfixr 3 -->\r\ninfixr 2 <-->\r\n(\/\\), (\\\/), (-->), (<-->) :: Prop -> Prop -> Prop\r\n(\/\\)   = Conj\r\n(\\\/)   = Disj\r\n(-->)  = Impl\r\n(<-->) = Equi\r\n\r\n-- ---------------------------------------------------------------------\r\n-- S\u00edmbolos proposicionales de una f\u00f3rmula                            --\r\n-- ---------------------------------------------------------------------\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Ejercicio 5: Definir la funci\u00f3n\r\n--    simbolosPropForm :: Prop -> [Prop]\r\n-- tal que (simbolosPropForm f) es el conjunto formado por todos los\r\n-- s\u00edmbolos proposicionales que aparecen en f. Por ejemplo,\r\n--    simbolosPropForm (p \/\\ q --> p)  == [p,q]\r\n-- ---------------------------------------------------------------------\r\n\r\nsimbolosPropForm :: Prop -> [Prop]\r\nsimbolosPropForm (Atom f)   = [(Atom f)]\r\nsimbolosPropForm (Neg f)    = simbolosPropForm f\r\nsimbolosPropForm (Conj f g) = simbolosPropForm f `union` simbolosPropForm g\r\nsimbolosPropForm (Disj f g) = simbolosPropForm f `union` simbolosPropForm g\r\nsimbolosPropForm (Impl f g) = simbolosPropForm f `union` simbolosPropForm g\r\nsimbolosPropForm (Equi f g) = simbolosPropForm f `union` simbolosPropForm g\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Interpretaciones                                                   --\r\n-- ---------------------------------------------------------------------\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Ejercicio 6: Definir el tipo de datos Interpretacion para\r\n-- representar las interpretaciones como listas de f\u00f3rmulas at\u00f3micas.\r\n-- ---------------------------------------------------------------------\r\n\r\ntype Interpretacion = [Prop]\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Significado de una f\u00f3rmula en una interpretaci\u00f3n                   --\r\n-- ---------------------------------------------------------------------\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Ejercicio 7: Definir la funci\u00f3n\r\n--    significado :: Prop -> Interpretacion -> Bool\r\n-- tal que (significado f i) es el significado de f en i. Por ejemplo,\r\n--    significado ((p \\\/ q) \/\\ ((no q) \\\/ r)) [r]    ==  False\r\n--    significado ((p \\\/ q) \/\\ ((no q) \\\/ r)) [p,r]  ==  True\r\n-- ---------------------------------------------------------------------\r\n\r\nsignificado :: Prop -> Interpretacion -> Bool\r\nsignificado (Atom f)   i = (Atom f) `elem` i\r\nsignificado (Neg f)    i = not (significado f i)\r\nsignificado (Conj f g) i = (significado f i) && (significado g i)\r\nsignificado (Disj f g) i = (significado f i) || (significado g i)\r\nsignificado (Impl f g) i = significado (Disj (Neg f) g) i\r\nsignificado (Equi f g) i = significado (Conj (Impl f g) (Impl g f)) i\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Interpretaciones de una f\u00f3rmula                                    --\r\n-- ---------------------------------------------------------------------\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Ejercicio 8: Definir la funci\u00f3n\r\n--    subconjuntos :: [a] -> [[a]]\r\n-- tal que (subconjuntos x) es la lista de los subconjuntos de x. Por\r\n-- ejmplo, \r\n--    subconjuntos \"abc\"  ==  [\"abc\",\"ab\",\"ac\",\"a\",\"bc\",\"b\",\"c\",\"\"]\r\n-- ---------------------------------------------------------------------\r\n\r\nsubconjuntos :: [a] -> [[a]]\r\nsubconjuntos []     = [[]]\r\nsubconjuntos (x:xs) = [x:ys | ys <- xss] ++ xss\r\n                      where xss = subconjuntos xs\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Ejercicio 9: Definir la funci\u00f3n\r\n--    interpretacionesForm :: Prop -> [Interpretacion]\r\n-- tal que (interpretacionesForm f) es la lista de todas las\r\n-- interpretaciones de f. Por ejemplo, \r\n--    interpretacionesForm (p \/\\ q --> p)  ==  [[p,q],[p],[q],[]]\r\n-- ---------------------------------------------------------------------\r\n\r\ninterpretacionesForm :: Prop -> [Interpretacion]\r\ninterpretacionesForm f = subconjuntos (simbolosPropForm f)\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Modelos de f\u00f3rmulas                                                --\r\n-- ---------------------------------------------------------------------\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Ejercicio 10: Definir la funci\u00f3n\r\n--    esModeloFormula :: Interpretacion -> Prop -> Bool\r\n-- tal que (esModeloFormula i f) se verifica si i es un modelo de f. Por\r\n-- ejemplo, \r\n--    esModeloFormula [r]   ((p \\\/ q) \/\\ ((no q) \\\/ r))    ==  False\r\n--    esModeloFormula [p,r] ((p \\\/ q) \/\\ ((no q) \\\/ r))    ==  True\r\n-- ---------------------------------------------------------------------\r\n\r\nesModeloFormula :: Interpretacion -> Prop -> Bool\r\nesModeloFormula i f = significado f i\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Ejercicio 11: Definir la funci\u00f3n\r\n--    modelosFormula :: Prop -> [Interpretacion]\r\n-- tal que (modelosFormula f) es la lista de todas las interpretaciones\r\n-- de f que son modelo de F. Por ejemplo,\r\n--    modelosFormula ((p \\\/ q) \/\\ ((no q) \\\/ r)) \r\n--    == [[p,q,r],[p,r],[p],[q,r]]\r\n-- ---------------------------------------------------------------------\r\n\r\nmodelosFormula :: Prop -> [Interpretacion]\r\nmodelosFormula f =\r\n    [i | i <- interpretacionesForm f,\r\n         esModeloFormula i f]\r\n\r\n-- ---------------------------------------------------------------------\r\n-- F\u00f3rmulas v\u00e1lidas, satisfacibles e insatisfacibles                  --\r\n-- ---------------------------------------------------------------------\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Ejercicio 12: Definir la funci\u00f3n\r\n--    esValida :: Prop -> Bool\r\n-- tal que (esValida f) se verifica si f es v\u00e1lida. Por ejemplo,\r\n--    esValida (p --> p)                 ==  True\r\n--    esValida (p --> q)                 ==  False\r\n--    esValida ((p --> q) \\\/ (q --> p))  ==  True\r\n-- ---------------------------------------------------------------------\r\n\r\nesValida :: Prop -> Bool\r\nesValida f = \r\n    modelosFormula f == interpretacionesForm f\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Ejercicio 13: Definir la funci\u00f3n\r\n--    esInsatisfacible :: Prop -> Bool\r\n-- tal que (esInsatisfacible f) se verifica si f es insatisfacible. Por\r\n-- ejemplo, \r\n--    esInsatisfacible (p \/\\ (no p))             ==  True\r\n--    esInsatisfacible ((p --> q) \/\\ (q --> r))  ==  False\r\n-- ---------------------------------------------------------------------\r\n\r\nesInsatisfacible :: Prop -> Bool\r\nesInsatisfacible f =\r\n    modelosFormula f == []\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Ejercicio 14: Definir la funci\u00f3n\r\n--    esSatisfacible :: Prop -> Bool\r\n-- tal que (esSatisfacible f) se verifica si f es satisfacible. Por\r\n-- ejemplo, \r\n--    esSatisfacible (p \/\\ (no p))             ==  False\r\n--    esSatisfacible ((p --> q) \/\\ (q --> r))  ==  True\r\n-- ---------------------------------------------------------------------\r\n\r\nesSatisfacible :: Prop -> Bool\r\nesSatisfacible f =\r\n    modelosFormula f \/= []\r\n\r\n-- ---------------------------------------------------------------------\r\n-- S\u00edmbolos proposicionales de un conjunto de f\u00f3rmulas                --\r\n-- ---------------------------------------------------------------------\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Ejercicio 15: Definir la funci\u00f3n\r\n--    unionGeneral :: Eq a => [[a]] -> [a]\r\n-- tal que (unionGeneral x) es la uni\u00f3n de los conjuntos de la lista de\r\n-- conjuntos x. Por ejemplo,\r\n--    unionGeneral []                 ==  []\r\n--    unionGeneral [[1]]              ==  [1]\r\n--    unionGeneral [[1],[1,2],[2,3]]  ==  [1,2,3]\r\n-- ---------------------------------------------------------------------\r\n\r\nunionGeneral :: Eq a => [[a]] -> [a]\r\nunionGeneral []     = []\r\nunionGeneral (x:xs) = x `union` unionGeneral xs \r\n\r\n-- ---------------------------------------------------------------------\r\n-- Ejercicio 16: Definir la funci\u00f3n\r\n--    simbolosPropConj :: [Prop] -> [Prop]\r\n-- tal que (simbolosPropConj s) es el conjunto de los s\u00edmbolos\r\n-- proposiciones de s. Por ejemplo,\r\n--    simbolosPropConj [p \/\\ q --> r, p --> s]  ==  [p,q,r,s]\r\n-- ---------------------------------------------------------------------\r\n\r\nsimbolosPropConj :: [Prop] -> [Prop]\r\nsimbolosPropConj s\r\n    = unionGeneral [simbolosPropForm f | f <- s]\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Interpretaciones de un conjunto de f\u00f3rmulas                        --\r\n-- ---------------------------------------------------------------------\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Ejercicio 17: Definir la funci\u00f3n\r\n--    interpretacionesConjunto :: [Prop] -> [Interpretacion]\r\n-- tal que (interpretacionesConjunto s) es la lista de las\r\n-- interpretaciones de s. Por ejemplo,\r\n--    interpretacionesConjunto [p --> q, q --> r]\r\n--    == [[p,q,r],[p,q],[p,r],[p],[q,r],[q],[r],[]]\r\n-- ---------------------------------------------------------------------\r\n\r\ninterpretacionesConjunto :: [Prop] -> [Interpretacion]\r\ninterpretacionesConjunto s =\r\n    subconjuntos (simbolosPropConj s)\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Modelos de conjuntos de f\u00f3rmulas                                   --\r\n-- ---------------------------------------------------------------------\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Ejercicio 18: Definir la funci\u00f3n\r\n--    esModeloConjunto :: Interpretacion -> [Prop] -> Bool\r\n-- tal que (esModeloConjunto i s) se verifica si i es modelo de s. Por\r\n-- ejemplo, \r\n--    esModeloConjunto [p,r] [(p \\\/ q) \/\\ ((no q) \\\/ r), q --> r]\r\n--    == True\r\n--    esModeloConjunto [p,r] [(p \\\/ q) \/\\ ((no q) \\\/ r), r --> q]\r\n--    == False\r\n-- ---------------------------------------------------------------------\r\n\r\nesModeloConjunto :: Interpretacion -> [Prop] -> Bool\r\nesModeloConjunto i s =\r\n    and [esModeloFormula i f | f <- s]\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Ejercicio 19: Definir la funci\u00f3n\r\n--    modelosConjunto :: [Prop] -> [Interpretacion]\r\n-- tal que (modelosConjunto s) es la lista de modelos del conjunto\r\n-- s. Por ejemplo,\r\n--    modelosConjunto [(p \\\/ q) \/\\ ((no q) \\\/ r), q --> r]\r\n--    == [[p,q,r],[p,r],[p],[q,r]]\r\n--    modelosConjunto [(p \\\/ q) \/\\ ((no q) \\\/ r), r --> q]\r\n--    == [[p,q,r],[p],[q,r]]\r\n-- ---------------------------------------------------------------------\r\n\r\nmodelosConjunto :: [Prop] -> [Interpretacion]\r\nmodelosConjunto s =\r\n    [i | i <- interpretacionesConjunto s,\r\n         esModeloConjunto i s]\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Conjuntos consistentes e inconsistentes de f\u00f3rmulas                --\r\n-- ---------------------------------------------------------------------\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Ejercicio 20: Definir la funci\u00f3n\r\n--    esConsistente :: [Prop] -> Bool\r\n-- tal que (esConsistente s) se verifica si s es consistente. Por\r\n-- ejemplo, \r\n--    esConsistente [(p \\\/ q) \/\\ ((no q) \\\/ r), p --> r]        \r\n--    == True\r\n--    esConsistente [(p \\\/ q) \/\\ ((no q) \\\/ r), p --> r, no r]  \r\n--    == False\r\n-- ---------------------------------------------------------------------\r\n\r\nesConsistente :: [Prop] -> Bool\r\nesConsistente s =\r\n    modelosConjunto s \/= []\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Ejercicio 21: Definir la funci\u00f3n\r\n--    esInconsistente :: [Prop] -> Bool\r\n-- tal que (esInconsistente s) se verifica si s es inconsistente. Por\r\n-- ejemplo, \r\n--    esInconsistente [(p \\\/ q) \/\\ ((no q) \\\/ r), p --> r]        \r\n--    == False\r\n--    esInconsistente [(p \\\/ q) \/\\ ((no q) \\\/ r), p --> r, no r]  \r\n--    == True\r\n-- ---------------------------------------------------------------------\r\n\r\nesInconsistente :: [Prop] -> Bool\r\nesInconsistente s =\r\n    modelosConjunto s == []\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Consecuencia l\u00f3gica                                                --\r\n-- ---------------------------------------------------------------------\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Ejercicio 22: Definir la funci\u00f3n\r\n--    esConsecuencia :: [Prop] -> Prop -> Bool\r\n-- tal que (esConsecuencia s f) se verifica si f es consecuencia de\r\n-- s. Por ejemplo,\r\n--    esConsecuencia [p --> q, q --> r] (p --> r)  ==  True\r\n--    esConsecuencia [p] (p \/\\ q)                  ==  False\r\n-- ---------------------------------------------------------------------\r\n\r\nesConsecuencia :: [Prop] -> Prop -> Bool\r\nesConsecuencia s f =\r\n    null [i | i <- interpretacionesConjunto (f:s),\r\n              esModeloConjunto i s,\r\n              not (esModeloFormula i f)]\r\n<\/pre>\n","protected":false},"excerpt":{"rendered":"<p>En la clase de hoy del curso de L\u00f3gica matem\u00e1tica y fundamentos (de 3\u00ba de Grado en Matem\u00e1ticas) se han comentado las soluciones de los 11 primeros ejercicios de la sintaxis y sem\u00e1ntica de la l\u00f3gica proposicional en Haskell. Las soluciones de los ejercicios corregidos se muestran a continuaci\u00f3n<\/p>\n","protected":false},"author":2,"featured_media":0,"comment_status":"closed","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"jetpack_post_was_ever_published":false,"_kad_post_transparent":"","_kad_post_title":"","_kad_post_layout":"","_kad_post_sidebar_id":"","_kad_post_content_style":"","_kad_post_vertical_padding":"","_kad_post_feature":"","_kad_post_feature_position":"","_kad_post_header":false,"_kad_post_footer":false,"_jetpack_newsletter_access":"","_jetpack_dont_email_post_to_subs":false,"_jetpack_newsletter_tier_id":0,"_jetpack_memberships_contains_paywalled_content":false,"footnotes":"","_jetpack_memberships_contains_paid_content":false},"categories":[1],"tags":[202],"jetpack_featured_media_url":"","jetpack_sharing_enabled":true,"jetpack_likes_enabled":false,"_links":{"self":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/2538"}],"collection":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/users\/2"}],"replies":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/comments?post=2538"}],"version-history":[{"count":4,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/2538\/revisions"}],"predecessor-version":[{"id":3290,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/2538\/revisions\/3290"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=2538"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=2538"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=2538"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}