{"id":6394,"date":"2018-11-28T18:33:08","date_gmt":"2018-11-28T17:33:08","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=6394"},"modified":"2018-11-28T18:33:08","modified_gmt":"2018-11-28T17:33:08","slug":"i1m2018-programa-en-haskell-para-reconocer-tautologias","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/i1m2018-programa-en-haskell-para-reconocer-tautologias\/","title":{"rendered":"I1M2018: Programa en Haskell para reconocer tautolog\u00edas"},"content":{"rendered":"<p>En la primera parte de la clase de hoy de <a href=\"http:\/\/www.cs.us.es\/~jalonso\/cursos\/i1m-18\">Inform\u00e1tica de 1\u00ba del Grado en Matem\u00e1ticas<\/a>  se ha estudiado c\u00f3mo construir un programa para determinar si una f\u00f3rmula es una tautolog\u00eda.<\/p>\n<p>Para ello se consideran las siguientes fases:<\/p>\n<ol>\n<li>definir un tipo de dato algebraico para las f\u00f3rmulas proposicionales,<\/li>\n<li>definir un tipo de dato para las interpretaciones,<\/li>\n<li>definir una funci\u00f3n para calcular los valores de las f\u00f3rmulas en las interpretaciones<\/li>\n<li>definir una funci\u00f3n para generar todas las posibles interpretaciones de una f\u00f3rmula y<\/li>\n<li>definir una funci\u00f3n que para decidir si una f\u00f3rmula es tautolog\u00eda (es decir, su valor es verdadero en todas sus interpretaciones).<\/li>\n<\/ol>\n<p>Los apuntes correspondientes a la clase son<br \/>\n\n<!-- iframe plugin v.5.0 wordpress.org\/plugins\/iframe\/ -->\n<iframe loading=\"lazy\" src=\"https:\/\/www.cs.us.es\/~jalonso\/cursos\/i1m-18\/temas\/tema-9.html#sistema-de-decisi%C3%B3n-de-tautolog%C3%ADas\" width=\"100%\" frameborder=\"1\" height=\"500\" scrolling=\"yes\" class=\"iframe-class\"><\/iframe>\n<\/p>\n<p>El c\u00f3digo correspondiente es<br \/>\n<!--more--><\/p>\n<pre lang=\"haskell\">\n-- Las f\u00f3rmulas proposicionales se definen por:\n--    * Las constantes booleanas son f\u00f3rmulas proposicionales.\n--    * Las f\u00f3rmulas at\u00f3micas son f\u00f3rmulas proposicionales.\n--    * Si F es una f\u00f3mula proposicional, entonces -F tambi\u00e9n los es.\n--    * Si F y F son f\u00f3rmulas proposicionales, entonces (F \/\\ G) y \n--      (F -> G) tambi\u00e9n lo son.\ndata Prop = Const Bool\n          | Var Char\n          | Neg Prop\n          | Conj Prop Prop\n          | Impl Prop Prop\n          deriving Show\n\n-- Ejemplos de representaci\u00f3n de f\u00f3rmulas proposicionales: Las f\u00f3rmulas\n--    * p1 := A \/\\ -A\n--    * p2 := (A \/\\ B) -> A\n--    * p3 := A -> (A \/\\ B)\n--    * p4 := (A -> (A -> B)) -> B\n-- se representan por\np1, p2, p3, p4 :: Prop\np1 = Conj (Var 'A') (Neg (Var 'A'))\np2 = Impl (Conj (Var 'A') (Var 'B')) (Var 'A')\np3 = Impl (Var 'A') (Conj (Var 'A') (Var 'B'))\np4 = Impl (Conj (Var 'A') (Impl (Var 'A') (Var 'B'))) (Var 'B')\n\n-- Las interpretaciones son listas formadas por el nombre de una\n-- variable proposicional y un valor de verdad. \ntype Interpretacion = Asoc Char Bool\n\n-- (valor i p) es el valor de la proposici\u00f3n p en la interpretaci\u00f3n\n-- i. Por ejemplo, \n--    valor [('A',False),('B',True)] p3  =>  True\n--    valor [('A',True),('B',False)] p3  =>  False\nvalor :: Interpretacion -> Prop -> Bool\nvalor _ (Const b)  = b\nvalor i (Var x)    = busca x i\nvalor i (Neg p)    = not (valor i p)\nvalor i (Conj p q) = valor i p && valor i q\nvalor i (Impl p q) = valor i p <= valor i q\n\n-- (variables p) es la lista de los nombres de las variables de la\n-- f\u00f3rmula p. Por ejemplo,\n--    variables p3  ==  \"AAB\"\nvariables :: Prop -> [Char]\nvariables (Const _)  = []\nvariables (Var x)    = [x]\nvariables (Neg p)    = variables p\nvariables (Conj p q) = variables p ++ variables q\nvariables (Impl p q) = variables p ++ variables q\n\n-- (interpretacionesVar n) es la lista de las interpretaciones con n\n-- variables. Por ejemplo, \n--    *Main> interpretacionesVar 2\n--    [[False,False],\n--     [False,True],\n--     [True,False],\n--     [True,True]]\ninterpretacionesVar :: Int -> [[Bool]]\ninterpretacionesVar 0     = [[]]\ninterpretacionesVar (n+1) = map (False:) bss ++ map (True:) bss\n    where bss = interpretacionesVar n\n\n-- (interpretaciones p) es la lista de las interpretaciones de la\n-- f\u00f3rmula p. Por ejemplo, \n--    *Main> interpretaciones p3\n--    [[('A',False),('B',False)],\n--     [('A',False),('B',True)],\n--     [('A',True),('B',False)],\n--     [('A',True),('B',True)]]\ninterpretaciones :: Prop -> [Interpretacion]\ninterpretaciones p =  \n    map (zip vs) (interpretacionesVar (length vs))\n    where vs = nub (variables p)\n\n-- Una definici\u00f3n alternativa es\ninterpretaciones' :: Prop -> [Interpretacion]\ninterpretaciones' p =  \n    [zip vs i | i <- is]\n    where vs = nub (variables p)\n          is = (interpretacionesVar (length vs))\n\n-- (esTautologia p) se verifica si la f\u00f3rmula p es una tautolog\u00eda. Por\n-- ejemplo, \n--    esTautologia p1  =>  False\n--    esTautologia p2  =>  True\n--    esTautologia p3  =>  False\n--    esTautologia p4  =>  True\nesTautologia :: Prop -> Bool\nesTautologia p = and [valor i p | i <- interpretaciones p]\n<\/pre>\n<p>En la segunda parte se han comentado soluciones de problemas propuestos en <a href=\"https:\/\/www.glc.us.es\/~jalonso\/exercitium\/\">Exercitium<\/a>. Concretamente,<\/p>\n<ul>\n<li><a href=\"http:\/\/bit.ly\/2DPMUko\">N\u00fameros primos sumas de dos primos<\/a><\/li>\n<li><a href=\"http:\/\/bit.ly\/2DP9ytg\">Reconocimiento de particiones<\/a><\/li>\n<li><a href=\"http:\/\/bit.ly\/2Qo4QJz\">N\u00famero de parejas<\/a><\/li>\n<\/ul>\n","protected":false},"excerpt":{"rendered":"<p>En la primera parte de la clase de hoy de Inform\u00e1tica de 1\u00ba del Grado en Matem\u00e1ticas se ha estudiado c\u00f3mo construir un programa para determinar si una f\u00f3rmula es una tautolog\u00eda. Para ello se consideran las siguientes fases: definir un tipo de dato algebraico para las f\u00f3rmulas proposicionales, definir un tipo de dato para&#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":[320],"tags":[270,321],"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\/6394"}],"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=6394"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/6394\/revisions"}],"predecessor-version":[{"id":6395,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/6394\/revisions\/6395"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=6394"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=6394"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=6394"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}