{"id":1932,"date":"2012-03-07T19:45:19","date_gmt":"2012-03-07T19:45:19","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=1932"},"modified":"2012-03-08T09:45:50","modified_gmt":"2012-03-08T09:45:50","slug":"i1m2011-extension-de-un-programa-en-haskell-para-decidir-tautologias","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/i1m2011-extension-de-un-programa-en-haskell-para-decidir-tautologias\/","title":{"rendered":"I1M2011: Extensi\u00f3n de un programa en Haskell para decidir 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-11\">Inform\u00e1tica de 1\u00ba del Grado en Matem\u00e1ticas<\/a> se han explicado las soluciones de los ejercicios de la  <a href=\"https:\/\/www.glc.us.es\/~jalonso\/ejerciciosI1M2011G1\/images\/0\/0a\/Rel_20.hs\">20\u00aa relaci\u00f3n<\/a>, en la que se propone extiender el demostrador proposicional estudiado en el <a href=\"http:\/\/www.cs.us.es\/~jalonso\/cursos\/i1m-11\/temas\/tema-9.pdf\">tema 9<\/a> para incluir disyunciones y equivalencias. <\/p>\n<p>Los ejercicios, y sus soluciones, se muestran a continuaci\u00f3n.<br \/>\n<!--more--><\/p>\n<pre lang=\"haskell\">\r\n-- ---------------------------------------------------------------------\r\n-- Importaci\u00f3n de librer\u00edas auxiliares                                  \r\n-- ---------------------------------------------------------------------\r\n\r\nimport Data.List\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Ejercicio 1. Extender el procedimiento de decisi\u00f3n de tautolog\u00edas\r\n-- para incluir las disyunciones (Disj) y las equivalencias (Equi). Por\r\n-- ejemplo, \r\n--    ghci> esTautologia (Equi (Var 'A') (Disj (Var 'A') (Var 'A')))\r\n--    True\r\n--    ghci> esTautologia (Equi (Var 'A') (Disj (Var 'A') (Var 'B')))\r\n--    False\r\n-- Se incluye el c\u00f3digo del procedimiento visto en clase para que se\r\n-- extienda de manera adecuada.\r\n-- ---------------------------------------------------------------------\r\n\r\ndata FProp = Const Bool\r\n           | Var Char\r\n           | Neg FProp\r\n           | Conj FProp FProp\r\n           | Disj FProp FProp   -- A\u00f1adido\r\n           | Impl FProp FProp\r\n           | Equi FProp FProp   -- A\u00f1adido\r\n           deriving Show\r\n\r\ntype Interpretacion = [(Char, Bool)]\r\n\r\nvalor :: Interpretacion -> FProp -> Bool\r\nvalor _ (Const b)  = b\r\nvalor i (Var x)    = busca x i\r\nvalor i (Neg p)    = not (valor i p)\r\nvalor i (Conj p q) = valor i p && valor i q\r\nvalor i (Disj p q) = valor i p || valor i q    -- A\u00f1adido \r\nvalor i (Impl p q) = valor i p <= valor i q\r\nvalor i (Equi p q) = valor i p == valor i q    -- A\u00f1adido \r\n\r\nbusca :: Eq c => c -> [(c,v)] -> v\r\nbusca c t = head [v | (c',v) <- t, c == c']\r\n\r\nvariables :: FProp -> [Char]\r\nvariables (Const _)  = []\r\nvariables (Var x)    = [x]\r\nvariables (Neg p)    = variables p\r\nvariables (Conj p q) = variables p ++ variables q\r\nvariables (Disj p q) = variables p ++ variables q   -- A\u00f1adido\r\nvariables (Impl p q) = variables p ++ variables q\r\nvariables (Equi p q) = variables p ++ variables q   -- A\u00f1adido\r\n\r\ninterpretacionesVar :: Int -> [[Bool]]\r\ninterpretacionesVar 0     = [[]]\r\ninterpretacionesVar (n+1) = \r\n    map (False:) bss ++ map (True:) bss\r\n    where bss = interpretacionesVar n\r\n\r\ninterpretaciones :: FProp -> [Interpretacion]\r\ninterpretaciones p =  \r\n    map (zip vs) (interpretacionesVar (length vs))\r\n    where vs = nub (variables p)\r\n\r\nesTautologia :: FProp -> Bool\r\nesTautologia p = \r\n    and [valor i p | i <- interpretaciones p]\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Ejercicio 2. Definir la funci\u00f3n\r\n--    interpretacionesVar' :: Int -> [[Bool]]\r\n-- que sea equivalente a interpretacionesVar pero que en su definici\u00f3n\r\n-- use listas de comprensi\u00f3n en lugar de map. Por ejemplo,\r\n--    ghci> interpretacionesVar' 2\r\n--    [[False,False],[False,True],[True,False],[True,True]]\r\n-- ---------------------------------------------------------------------\r\n\r\ninterpretacionesVar' :: Int -> [[Bool]]\r\ninterpretacionesVar' 0     = [[]]\r\ninterpretacionesVar' (n+1) = \r\n    [False:bs | bs <- bss] ++ [True:bs | bs <- bss]\r\n    where bss = interpretacionesVar' n\r\n\r\n-- ---------------------------------------------------------------------\r\n-- Ejercicio 3. Definir la funci\u00f3n\r\n--    interpretaciones' :: FProp -> [Interpretacion]\r\n-- que sea equivalente a interpretaciones pero que en su definici\u00f3n\r\n-- use listas de comprensi\u00f3n en lugar de map. Por ejemplo,\r\n--    ghci> interpretaciones' (Impl (Var 'A') (Conj (Var 'A') (Var 'B')))\r\n--    [[('A',False),('B',False)],\r\n--     [('A',False),('B',True)],\r\n--     [('A',True),('B',False)],\r\n--     [('A',True),('B',True)]]\r\n-- ---------------------------------------------------------------------\r\n\r\ninterpretaciones' :: FProp -> [Interpretacion]\r\ninterpretaciones' p =  \r\n    [zip vs i | i <- is] \r\n    where vs = nub (variables p)\r\n          is = interpretacionesVar (length vs)\r\n<\/pre>\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 han explicado las soluciones de los ejercicios de la 20\u00aa relaci\u00f3n, en la que se propone extiender el demostrador proposicional estudiado en el tema 9 para incluir disyunciones y equivalencias. Los ejercicios, y sus soluciones, se muestran&#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":[295],"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\/1932"}],"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=1932"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/1932\/revisions"}],"predecessor-version":[{"id":1933,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/1932\/revisions\/1933"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=1932"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=1932"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=1932"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}