{"id":1960,"date":"2012-03-06T14:10:41","date_gmt":"2012-03-06T14:10:41","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=1960"},"modified":"2012-03-19T14:11:53","modified_gmt":"2012-03-19T14:11:53","slug":"lmf2012-sintaxis-y-semantica-de-la-logica-proposicional-en-haskell-1","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/lmf2012-sintaxis-y-semantica-de-la-logica-proposicional-en-haskell-1\/","title":{"rendered":"LMF2012: Sintaxis y sem\u00e1ntica de la l\u00f3gica proposicional en Haskell (1)"},"content":{"rendered":"<p>En la clase de hoy del curso de <a href=\"http:\/\/www.cs.us.es\/~jalonso\/cursos\/lmf-11\">L\u00f3gica matem\u00e1tica y fundamentos<\/a> (de 3\u00ba de Grado en Matem\u00e1ticas) se han comentados las soluciones de los ejercicios de revisi\u00f3n de Haskell planteados en la <a href=\"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/lmf2012-revision-de-la-programacion-con-haskell\/\">clase anterior<\/a> y se ha comenzado la soluci\u00f3n de los ejercicios sobre 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\nimport Test.HUnit\r\nimport Test.QuickCheck\r\nimport Control.Monad\r\nimport Verificacion\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-- * FProp 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 FProp = Atom SimboloProposicional\r\n          | Neg FProp \r\n          | Conj FProp FProp \r\n          | Disj FProp FProp \r\n          | Impl FProp FProp \r\n          | Equi FProp FProp \r\n          deriving (Eq,Ord)\r\n\r\ninstance Show FProp 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 :: FProp\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 :: FProp -> FProp\r\n-- tal que (no f) es la negaci\u00f3n de f.\r\n-- ---------------------------------------------------------------------\r\n\r\nno :: FProp -> FProp\r\nno = Neg\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Ejercicio 4: Definir los siguientes operadores\r\n--    (\/\\), (\\\/), (-->), (<-->) :: FProp -> FProp -> FProp\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(\/\\), (\\\/), (-->), (<-->) :: FProp -> FProp -> FProp\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 :: FProp -> [FProp]\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 :: FProp -> [FProp]\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 = [FProp]\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 :: FProp -> 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 :: FProp -> 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 :: FProp -> [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 :: FProp -> [Interpretacion]\r\ninterpretacionesForm f = subconjuntos (simbolosPropForm 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 comentados las soluciones de los ejercicios de revisi\u00f3n de Haskell planteados en la clase anterior y se ha comenzado la soluci\u00f3n de los ejercicios sobre la sintaxis y sem\u00e1ntica de la l\u00f3gica proposicional en Haskell&#8230;.<\/p>\n","protected":false},"author":2,"featured_media":0,"comment_status":"open","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":[192],"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\/1960"}],"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=1960"}],"version-history":[{"count":2,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/1960\/revisions"}],"predecessor-version":[{"id":1962,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/1960\/revisions\/1962"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=1960"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=1960"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=1960"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}