I1M2011: Extensión de un programa en Haskell para decidir tautologías
En la primera parte de la clase de hoy de Informática de 1º del Grado en Matemáticas se han explicado las soluciones de los ejercicios de la 20ª relación, 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 a continuación.
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 |
-- --------------------------------------------------------------------- -- Importación de librerías auxiliares -- --------------------------------------------------------------------- import Data.List -- --------------------------------------------------------------------- -- Ejercicio 1. Extender el procedimiento de decisión de tautologías -- para incluir las disyunciones (Disj) y las equivalencias (Equi). Por -- ejemplo, -- ghci> esTautologia (Equi (Var 'A') (Disj (Var 'A') (Var 'A'))) -- True -- ghci> esTautologia (Equi (Var 'A') (Disj (Var 'A') (Var 'B'))) -- False -- Se incluye el código del procedimiento visto en clase para que se -- extienda de manera adecuada. -- --------------------------------------------------------------------- data FProp = Const Bool | Var Char | Neg FProp | Conj FProp FProp | Disj FProp FProp -- Añadido | Impl FProp FProp | Equi FProp FProp -- Añadido deriving Show type Interpretacion = [(Char, Bool)] valor :: Interpretacion -> FProp -> Bool valor _ (Const b) = b valor i (Var x) = busca x i valor i (Neg p) = not (valor i p) valor i (Conj p q) = valor i p && valor i q valor i (Disj p q) = valor i p || valor i q -- Añadido valor i (Impl p q) = valor i p <= valor i q valor i (Equi p q) = valor i p == valor i q -- Añadido busca :: Eq c => c -> [(c,v)] -> v busca c t = head [v | (c',v) <- t, c == c'] variables :: FProp -> [Char] variables (Const _) = [] variables (Var x) = [x] variables (Neg p) = variables p variables (Conj p q) = variables p ++ variables q variables (Disj p q) = variables p ++ variables q -- Añadido variables (Impl p q) = variables p ++ variables q variables (Equi p q) = variables p ++ variables q -- Añadido interpretacionesVar :: Int -> [[Bool]] interpretacionesVar 0 = [[]] interpretacionesVar (n+1) = map (False:) bss ++ map (True:) bss where bss = interpretacionesVar n interpretaciones :: FProp -> [Interpretacion] interpretaciones p = map (zip vs) (interpretacionesVar (length vs)) where vs = nub (variables p) esTautologia :: FProp -> Bool esTautologia p = and [valor i p | i <- interpretaciones p] -- --------------------------------------------------------------------- -- Ejercicio 2. Definir la función -- interpretacionesVar' :: Int -> [[Bool]] -- que sea equivalente a interpretacionesVar pero que en su definición -- use listas de comprensión en lugar de map. Por ejemplo, -- ghci> interpretacionesVar' 2 -- [[False,False],[False,True],[True,False],[True,True]] -- --------------------------------------------------------------------- interpretacionesVar' :: Int -> [[Bool]] interpretacionesVar' 0 = [[]] interpretacionesVar' (n+1) = [False:bs | bs <- bss] ++ [True:bs | bs <- bss] where bss = interpretacionesVar' n -- --------------------------------------------------------------------- -- Ejercicio 3. Definir la función -- interpretaciones' :: FProp -> [Interpretacion] -- que sea equivalente a interpretaciones pero que en su definición -- use listas de comprensión en lugar de map. Por ejemplo, -- ghci> interpretaciones' (Impl (Var 'A') (Conj (Var 'A') (Var 'B'))) -- [[('A',False),('B',False)], -- [('A',False),('B',True)], -- [('A',True),('B',False)], -- [('A',True),('B',True)]] -- --------------------------------------------------------------------- interpretaciones' :: FProp -> [Interpretacion] interpretaciones' p = [zip vs i | i <- is] where vs = nub (variables p) is = interpretacionesVar (length vs) |