Menu Close

I1M2018: Programa en Haskell para reconocer tautologías

José A. Alonso-

En la primera parte de la clase de hoy de Informática de 1º del Grado en Matemáticas se ha estudiado cómo construir un programa para determinar si una fórmula es una tautología.

Para ello se consideran las siguientes fases:

  1. definir un tipo de dato algebraico para las fórmulas proposicionales,
  2. definir un tipo de dato para las interpretaciones,
  3. definir una función para calcular los valores de las fórmulas en las interpretaciones
  4. definir una función para generar todas las posibles interpretaciones de una fórmula y
  5. definir una función que para decidir si una fórmula es tautología (es decir, su valor es verdadero en todas sus interpretaciones).

Los apuntes correspondientes a la clase son

El código correspondiente es

-- Las fórmulas proposicionales se definen por:
--    * Las constantes booleanas son fórmulas proposicionales.
--    * Las fórmulas atómicas son fórmulas proposicionales.
--    * Si F es una fómula proposicional, entonces -F también los es.
--    * Si F y F son fórmulas proposicionales, entonces (F /\ G) y 
--      (F -> G) también lo son.
data Prop = Const Bool
          | Var Char
          | Neg Prop
          | Conj Prop Prop
          | Impl Prop Prop
          deriving Show
 
-- Ejemplos de representación de fórmulas proposicionales: Las fórmulas
--    * p1 := A /\ -A
--    * p2 := (A /\ B) -> A
--    * p3 := A -> (A /\ B)
--    * p4 := (A -> (A -> B)) -> B
-- se representan por
p1, p2, p3, p4 :: Prop
p1 = Conj (Var 'A') (Neg (Var 'A'))
p2 = Impl (Conj (Var 'A') (Var 'B')) (Var 'A')
p3 = Impl (Var 'A') (Conj (Var 'A') (Var 'B'))
p4 = Impl (Conj (Var 'A') (Impl (Var 'A') (Var 'B'))) (Var 'B')
 
-- Las interpretaciones son listas formadas por el nombre de una
-- variable proposicional y un valor de verdad. 
type Interpretacion = Asoc Char Bool
 
-- (valor i p) es el valor de la proposición p en la interpretación
-- i. Por ejemplo, 
--    valor [('A',False),('B',True)] p3  =>  True
--    valor [('A',True),('B',False)] p3  =>  False
valor :: Interpretacion -> Prop -> 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 (Impl p q) = valor i p <= valor i q
 
-- (variables p) es la lista de los nombres de las variables de la
-- fórmula p. Por ejemplo,
--    variables p3  ==  "AAB"
variables :: Prop -> [Char]
variables (Const _)  = []
variables (Var x)    = [x]
variables (Neg p)    = variables p
variables (Conj p q) = variables p ++ variables q
variables (Impl p q) = variables p ++ variables q
 
-- (interpretacionesVar n) es la lista de las interpretaciones con n
-- variables. Por ejemplo, 
--    *Main> interpretacionesVar 2
--    [[False,False],
--     [False,True],
--     [True,False],
--     [True,True]]
interpretacionesVar :: Int -> [[Bool]]
interpretacionesVar 0     = [[]]
interpretacionesVar (n+1) = map (False:) bss ++ map (True:) bss
    where bss = interpretacionesVar n
 
-- (interpretaciones p) es la lista de las interpretaciones de la
-- fórmula p. Por ejemplo, 
--    *Main> interpretaciones p3
--    [[('A',False),('B',False)],
--     [('A',False),('B',True)],
--     [('A',True),('B',False)],
--     [('A',True),('B',True)]]
interpretaciones :: Prop -> [Interpretacion]
interpretaciones p =  
    map (zip vs) (interpretacionesVar (length vs))
    where vs = nub (variables p)
 
-- Una definición alternativa es
interpretaciones' :: Prop -> [Interpretacion]
interpretaciones' p =  
    [zip vs i | i <- is]
    where vs = nub (variables p)
          is = (interpretacionesVar (length vs))
 
-- (esTautologia p) se verifica si la fórmula p es una tautología. Por
-- ejemplo, 
--    esTautologia p1  =>  False
--    esTautologia p2  =>  True
--    esTautologia p3  =>  False
--    esTautologia p4  =>  True
esTautologia :: Prop -> Bool
esTautologia p = and [valor i p | i <- interpretaciones p]

En la segunda parte se han comentado soluciones de problemas propuestos en Exercitium. Concretamente,

I1M2018
,