{"id":2028,"date":"2012-04-10T16:00:23","date_gmt":"2012-04-10T16:00:23","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=2028"},"modified":"2013-03-08T05:48:16","modified_gmt":"2013-03-08T05:48:16","slug":"lmf2012-formas-normales-en-haskell","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/lmf2012-formas-normales-en-haskell\/","title":{"rendered":"LMF2012: Formas normales en Haskell"},"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 ha comentado las soluciones de los ejercicios sobre la implementaci\u00f3n en Haskell de las formas normales.<\/p>\n<p>Las soluciones de los ejercicios se muestran a continuaci\u00f3n. En los ejercicios se usa el m\u00f3dulo SintaxisSemantica desarrollado en la <a href=\"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/lmf2012-sintaxis-y-semantica-de-la-logica-proposicional-en-haskell\">clase del d\u00eda 13 de marzo<\/a>.<br \/>\n<!--more--><\/p>\n<pre lang=\"haskell\">\r\nmodule FormasNormales where\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Librer\u00eda suxiliares                                                --\r\n-- ---------------------------------------------------------------------\r\n\r\nimport SintaxisSemantica \r\nimport Data.List\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Equivalencia l\u00f3gica                                                --\r\n-- ---------------------------------------------------------------------\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Ejercicio 1: Definir la funci\u00f3n\r\n--    esEquivalente :: Prop -> Prop -> Bool\r\n-- tal que (esEquivalente f g) se verifica si f y g son\r\n-- equivalentes. Por ejemplo,\r\n--    esEquivalente (p <--> q) ((p --> q) \/\\ (q --> p))  ==>  True\r\n--    esEquivalente (p --> q)  ((no p) \\\/ q)             ==>  True\r\n--    esEquivalente (p \/\\ q)   (no ((no p) \\\/ (no q)))   ==>  True\r\n--    esEquivalente (p \\\/ q)   (no ((no p) \/\\ (no q)))   ==>  True\r\n-- ---------------------------------------------------------------------\r\n\r\nesEquivalente :: Prop -> Prop -> Bool\r\nesEquivalente f g =\r\n    esValida (Equi f g)\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Transformaci\u00f3n a forma normal negativa                             --\r\n-- ---------------------------------------------------------------------\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Ejercicio 2: Definir la funci\u00f3n\r\n--    eliminaEquivalencias :: Prop -> Prop\r\n-- tal que (eliminaEquivalencias f) es una f\u00f3rmula equivalente a f sin\r\n-- signos de equivalencia. Por ejemplo,\r\n--    eliminaEquivalencias (p <--> q)\r\n--    ==> ((p --> q) \/\\ (q --> p))\r\n--    eliminaEquivalencias ((p <--> q) \/\\ (q <--> r))\r\n--    ==> (((p --> q) \/\\ (q --> p)) \/\\ ((q --> r) \/\\ (r --> q)))\r\n-- ---------------------------------------------------------------------\r\n\r\neliminaEquivalencias :: Prop -> Prop\r\neliminaEquivalencias (Atom f)   = \r\n    (Atom f)\r\neliminaEquivalencias (Neg f)    = \r\n    Neg (eliminaEquivalencias f) \r\neliminaEquivalencias (Conj f g) = \r\n    Conj (eliminaEquivalencias f) (eliminaEquivalencias g) \r\neliminaEquivalencias (Disj f g) = \r\n    Disj (eliminaEquivalencias f) (eliminaEquivalencias g) \r\neliminaEquivalencias (Impl f g) = \r\n    Impl (eliminaEquivalencias f) (eliminaEquivalencias g) \r\neliminaEquivalencias (Equi f g) = \r\n    Conj (Impl (eliminaEquivalencias f) (eliminaEquivalencias g))\r\n         (Impl (eliminaEquivalencias g) (eliminaEquivalencias f))\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Ejercicio 3: Definir la funci\u00f3n\r\n--    eliminaImplicaciones :: Prop -> Prop\r\n-- tal que (eliminaImplicaciones f) es una f\u00f3rmula equivalente a f sin\r\n-- signos de implicaci\u00f3n. Por ejemplo,\r\n--    eliminaImplicaciones (p --> q)\r\n--    ==> (no p \\\/ q)\r\n--    eliminaImplicaciones (eliminaEquivalencias (p <--> q))\r\n--    ==> ((no p \\\/ q) \/\\ (no q \\\/ p))\r\n-- Nota: Se supone que f no tiene signos de equivalencia.\r\n-- ---------------------------------------------------------------------\r\n\r\neliminaImplicaciones :: Prop -> Prop\r\neliminaImplicaciones (Atom f)   = \r\n    (Atom f)\r\neliminaImplicaciones (Neg f)    = \r\n    Neg (eliminaImplicaciones f) \r\neliminaImplicaciones (Conj f g) = \r\n    Conj (eliminaImplicaciones f) (eliminaImplicaciones g) \r\neliminaImplicaciones (Disj f g) = \r\n    Disj (eliminaImplicaciones f) (eliminaImplicaciones g) \r\neliminaImplicaciones (Impl f g) = \r\n    Disj (Neg (eliminaImplicaciones f)) (eliminaImplicaciones g) \r\n\r\n-- ---------------------------------------------------------------------\r\n-- Ejercicio 4: Definir la funci\u00f3n\r\n--    interiorizaNegaci\u00f3n :: Prop -> Prop\r\n-- tal que (interiorizaNegaci\u00f3n f) es una f\u00f3rmula equivalente a f donde\r\n-- las negaciones se aplican s\u00f3lo a f\u00f3rmulas at\u00f3micas. Por ejemplo,\r\n--    interiorizaNegaci\u00f3n (no (no p))         ==>  p\r\n--    interiorizaNegaci\u00f3n (no (p \/\\ q))       ==>  (no p \\\/ no q)\r\n--    interiorizaNegaci\u00f3n (no (p \\\/ q))       ==>  (no p \/\\ no q)\r\n--    interiorizaNegaci\u00f3n (no (no (p \\\/ q)))  ==>  (p \\\/ q)\r\n--    interiorizaNegaci\u00f3n (no ((no p) \\\/ q))  ==>  (p \/\\ no q)\r\n-- Nota: Se supone que f no tiene equivalencias ni implicaciones. \r\n-- ---------------------------------------------------------------------\r\n\r\ninteriorizaNegaci\u00f3n :: Prop -> Prop\r\ninteriorizaNegaci\u00f3n (Atom f)   = \r\n    (Atom f)\r\ninteriorizaNegaci\u00f3n (Neg f)    = \r\n    interiorizaNegaci\u00f3nAux f\r\ninteriorizaNegaci\u00f3n (Conj f g) = \r\n    Conj (interiorizaNegaci\u00f3n f) (interiorizaNegaci\u00f3n g) \r\ninteriorizaNegaci\u00f3n (Disj f g) = \r\n    Disj (interiorizaNegaci\u00f3n f) (interiorizaNegaci\u00f3n g) \r\n\r\ninteriorizaNegaci\u00f3nAux :: Prop -> Prop\r\ninteriorizaNegaci\u00f3nAux (Atom f)   = \r\n    Neg (Atom f)\r\ninteriorizaNegaci\u00f3nAux (Neg f)    = \r\n    interiorizaNegaci\u00f3n f \r\ninteriorizaNegaci\u00f3nAux (Conj f g) = \r\n    Disj (interiorizaNegaci\u00f3nAux f) (interiorizaNegaci\u00f3nAux g) \r\ninteriorizaNegaci\u00f3nAux (Disj f g) = \r\n    Conj (interiorizaNegaci\u00f3nAux f) (interiorizaNegaci\u00f3nAux g) \r\n\r\n-- ---------------------------------------------------------------------\r\n-- Ejercicio 5: Definir la funci\u00f3n\r\n--    formaNormalNegativa :: Prop -> Prop\r\n-- tal que (formaNormalNegativa f) es una f\u00f3rmula equivalente a f en\r\n-- forma normal negativa. Por ejemplo,\r\n--    formaNormalNegativa (p <--> q)\r\n--    ==> ((no p \\\/ q) \/\\ (no q \\\/ p))\r\n--    formaNormalNegativa ((p \\\/ (no q)) --> r)\r\n--    ==> ((no p \/\\ q) \\\/ r)\r\n--    formaNormalNegativa ((p \/\\ (q --> r)) --> s)\r\n--    ==> ((no p \\\/ (q \/\\ no r)) \\\/ s)\r\n-- ---------------------------------------------------------------------\r\n\r\nformaNormalNegativa :: Prop -> Prop\r\nformaNormalNegativa f =\r\n    interiorizaNegaci\u00f3n (eliminaImplicaciones (eliminaEquivalencias f))\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Literales                                                          --\r\n-- ---------------------------------------------------------------------\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Ejercicio 6: Definir la funci\u00f3n\r\n--    literal :: Prop -> Bool\r\n-- tal que (literal f) se verifica si la f\u00f3rmula F es un literal. Por\r\n-- ejemplo, \r\n--    literal p               ==>  True\r\n--    literal (no p)          ==>  True\r\n--    literal (no (p --> q))  ==>  False\r\n-- ---------------------------------------------------------------------\r\n\r\nliteral :: Prop -> Bool\r\nliteral (Atom f)       = True\r\nliteral (Neg (Atom f)) = True\r\nliteral _              = False\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Ejercicio 7: Definir el tipo de dato Literal como sin\u00f3nimo de\r\n-- f\u00f3rmula. \r\n-- ---------------------------------------------------------------------\r\n\r\ntype Literal = Prop\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Ejercicio 8: Definir la funci\u00f3n\r\n--    complementario :: Literal -> Literal\r\n-- tal que (complementario l) es el complementario de l. Por ejemplo,\r\n--    complementario p       ==>  no p\r\n--    complementario (no p)  ==>  p\r\n-- ---------------------------------------------------------------------\r\n\r\ncomplementario :: Literal -> Literal\r\ncomplementario (Atom f)       = Neg (Atom f)\r\ncomplementario (Neg (Atom f)) = Atom f\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Ejercicio 9: Definir la funci\u00f3n\r\n--    literalesF\u00f3rmulaFNN :: Prop -> [Literal]\r\n-- tal que (literalesF\u00f3rmulaFNN f) es el conjunto de los literales de la\r\n-- f\u00f3rmula en forma normal negativa f.\r\n--    literalesF\u00f3rmulaFNN (p \\\/ ((no q) \\\/ r))  ==>  [p,no q,r]\r\n--    literalesF\u00f3rmulaFNN p                     ==>  [p]\r\n--    literalesF\u00f3rmulaFNN (no p)                ==>  [no p]\r\n-- ---------------------------------------------------------------------\r\n\r\nliteralesF\u00f3rmulaFNN :: Prop -> [Literal]\r\nliteralesF\u00f3rmulaFNN (Disj f g) =\r\n    (literalesF\u00f3rmulaFNN f) `union` (literalesF\u00f3rmulaFNN g)\r\nliteralesF\u00f3rmulaFNN (Conj f g) =\r\n    (literalesF\u00f3rmulaFNN f) `union` (literalesF\u00f3rmulaFNN g)\r\nliteralesF\u00f3rmulaFNN f          = [f]\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Transformaci\u00f3n a forma normal conjuntiva                           --\r\n-- ---------------------------------------------------------------------\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Ejercicio 10: Definir la funci\u00f3n\r\n--    interiorizaDisyunci\u00f3n :: Prop -> Prop\r\n-- tal que (interiorizaDisyunci\u00f3n f) es una f\u00f3rmula equivalente a f\r\n-- donde las disyunciones s\u00f3lo se aplica a disyunciones o literales. Por\r\n-- ejemplo,  \r\n--    interiorizaDisyunci\u00f3n (p \\\/ (q \/\\ r))  ==>  ((p \\\/ q) \/\\ (p \\\/ r))\r\n--    interiorizaDisyunci\u00f3n ((p \/\\ q) \\\/ r)  ==>  ((p \\\/ r) \/\\ (q \\\/ r))\r\n-- Nota: Se supone que f est\u00e1 en forma normal negativa.\r\n-- ---------------------------------------------------------------------\r\n\r\ninteriorizaDisyunci\u00f3n :: Prop -> Prop\r\ninteriorizaDisyunci\u00f3n (Disj (Conj f1 f2) g) =\r\n   interiorizaDisyunci\u00f3n\r\n   (Conj (Disj (interiorizaDisyunci\u00f3n f1) (interiorizaDisyunci\u00f3n g))\r\n         (Disj (interiorizaDisyunci\u00f3n f2) (interiorizaDisyunci\u00f3n g)))\r\ninteriorizaDisyunci\u00f3n (Disj f (Conj g1 g2)) =\r\n   interiorizaDisyunci\u00f3n\r\n   (Conj (Disj (interiorizaDisyunci\u00f3n f) (interiorizaDisyunci\u00f3n g1))\r\n         (Disj (interiorizaDisyunci\u00f3n f) (interiorizaDisyunci\u00f3n g2)))\r\ninteriorizaDisyunci\u00f3n (Conj f g) =\r\n   Conj (interiorizaDisyunci\u00f3n f) (interiorizaDisyunci\u00f3n g)\r\ninteriorizaDisyunci\u00f3n (Disj f g)\r\n   | tieneConj (Disj f g) = interiorizaDisyunci\u00f3n\r\n                            (Disj (interiorizaDisyunci\u00f3n f)\r\n                                  (interiorizaDisyunci\u00f3n g))\r\n   | otherwise = Disj (interiorizaDisyunci\u00f3n f)\r\n                      (interiorizaDisyunci\u00f3n g)\r\ninteriorizaDisyunci\u00f3n f = f\r\n\r\ntieneConj:: Prop -> Bool\r\ntieneConj (Conj f g) = True\r\ntieneConj (Disj f g) = (tieneConj f) || (tieneConj g)\r\ntieneConj _          = False\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Ejercicio 11: Definir la funci\u00f3n\r\n--    formaNormalConjuntiva :: Prop -> Prop\r\n-- tal que (formaNormalConjuntiva f) es una f\u00f3rmula equivalente a f en\r\n-- forma normal conjuntiva. Por ejemplo,\r\n--    formaNormalConjuntiva (p \/\\ (q --> r))\r\n--    ==> (p \/\\ (no q \\\/ r))\r\n--    formaNormalConjuntiva (no (p \/\\ (q --> r)))\r\n--    ==> ((no p \\\/ q) \/\\ (no p \\\/ no r))\r\n--    formaNormalConjuntiva (no(p <--> r))\r\n--    ==> (((p \\\/ r) \/\\ (p \\\/ no p)) \/\\ ((no r \\\/ r) \/\\ (no r \\\/ no p)))\r\n-- ---------------------------------------------------------------------\r\n\r\nformaNormalConjuntiva :: Prop -> Prop\r\nformaNormalConjuntiva f =\r\n    interiorizaDisyunci\u00f3n (formaNormalNegativa f)\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Transformaci\u00f3n a forma normal disyuntiva                           --\r\n-- ---------------------------------------------------------------------\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Ejercicio 12: Definir la funci\u00f3n\r\n--    interiorizaConjunci\u00f3n :: Prop -> Prop\r\n-- tal que (interiorizaConjunci\u00f3n f) es una f\u00f3rmula equivalente a f\r\n-- donde las conjunciones s\u00f3lo se aplica a conjunciones o literales. Por\r\n-- ejemplo,  \r\n--    interiorizaConjunci\u00f3n (p \/\\ (q \\\/ r))  ==>  ((p \/\\ q) \\\/ (p \/\\ r))\r\n--    interiorizaConjunci\u00f3n ((p \\\/ q) \/\\ r)  ==>  ((p \/\\ r) \\\/ (q \/\\ r))\r\n-- Nota: Se supone que f est\u00e1 en forma normal negativa.\r\n-- ---------------------------------------------------------------------\r\n\r\ninteriorizaConjunci\u00f3n :: Prop -> Prop\r\ninteriorizaConjunci\u00f3n (Conj (Disj f1 f2) g) =\r\n    interiorizaConjunci\u00f3n\r\n    (Disj (Conj (interiorizaConjunci\u00f3n f1) (interiorizaConjunci\u00f3n g))\r\n          (Conj (interiorizaConjunci\u00f3n f2) (interiorizaConjunci\u00f3n g)))\r\ninteriorizaConjunci\u00f3n (Conj f (Disj g1 g2)) =\r\n    interiorizaConjunci\u00f3n\r\n    (Disj (Conj (interiorizaConjunci\u00f3n f) (interiorizaConjunci\u00f3n g1))\r\n          (Conj (interiorizaConjunci\u00f3n f) (interiorizaConjunci\u00f3n g2)))\r\ninteriorizaConjunci\u00f3n (Disj f g) =\r\n    Disj (interiorizaConjunci\u00f3n f) (interiorizaConjunci\u00f3n g)\r\ninteriorizaConjunci\u00f3n f = f\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Ejercicio 13: Definir la funci\u00f3n\r\n--    formaNormalDisyuntiva :: Prop -> Prop\r\n-- tal que (formaNormalDisyuntiva f) es una f\u00f3rmula equivalente a f en\r\n-- forma normal disyuntiva. Por ejemplo,\r\n--    formaNormalDisyuntiva (p \/\\ (q --> r))\r\n--    ==> ((p \/\\ no q) \\\/ (p \/\\ r))\r\n--    formaNormalDisyuntiva (no (p \/\\ (q --> r)))\r\n--    ==> (no p \\\/ (q \/\\ no r))\r\n-- ---------------------------------------------------------------------\r\n\r\nformaNormalDisyuntiva :: Prop -> Prop\r\nformaNormalDisyuntiva f =\r\n    interiorizaConjunci\u00f3n (formaNormalNegativa 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 ha comentado las soluciones de los ejercicios sobre la implementaci\u00f3n en Haskell de las formas normales. Las soluciones de los ejercicios se muestran a continuaci\u00f3n. En los ejercicios se usa el m\u00f3dulo SintaxisSemantica desarrollado en la&#8230;<\/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":[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\/2028"}],"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=2028"}],"version-history":[{"count":2,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/2028\/revisions"}],"predecessor-version":[{"id":2827,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/2028\/revisions\/2827"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=2028"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=2028"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=2028"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}