Ir al contenido principal

Simplificación de expresiones proposicionales

El siguiente tipo de dato algebraico representa las fórmulas proposicionales construidas con una variable (X), las constantes verdadera (V) y falsa (F), la negación (Neg) y la disyunción (Dis):

data Form = X
          | V
          | F
          | Neg Form
          | Dis Form Form
          deriving (Eq, Ord, Show)

Por ejemplo, la fórmula (¬X v V) se representa por (Dis (Neg X) V).

Definir las funciones

valor      :: Form -> Bool -> Bool
simplifica :: Form -> Form

tales que (valor p i) es el valor de la fórmula p cuando se le asigna a X el valor i. Por ejemplo,

valor (Neg X) True           ==  False
valor (Neg F) True           ==  True
valor (Dis X (Neg X)) True   ==  True
valor (Dis X (Neg X)) False  ==  True

y (simplifica p) es una forma obtenida aplicándole a p las siguientes reglas de simplificación:

Neg V       = F
Neg F       = V
Neg (Neg q) = q
Dis V q     = V
Dis F q     = q
Dis q V     = V
Dis q F     = F
Dis q q     = q

Por ejemplo,

simplifica (Dis X (Neg (Neg X)))                      ==  X
simplifica (Neg (Dis (Neg (Neg X)) F))                ==  Neg X
simplifica (Dis (Neg F) F)                            ==  V
simplifica (Dis (Neg V) (Neg (Dis (Neg X) F)))        ==  X
simplifica (Dis (Neg V) (Neg (Dis (Neg (Neg X)) F)))  ==  Neg X

Comprobar con QuickCheck que para cualquier fórmula p y cualquier booleano i se verifica que (valor (simplifica p) i) es igual a (valor p i).

Nota: Escribir las soluciones usando la siguiente plantilla que contiene un generador de fórmulas proposicionales

import Test.QuickCheck
import Control.Monad

data Form = X
          | V
          | F
          | Neg Form
          | Dis Form Form
          deriving (Eq, Ord, Show)

valor :: Form -> Bool -> Bool
valor = undefined

simplifica :: Form -> Form
simplifica = undefined

-- La propiedad es
prop_simplifica :: Form -> Bool -> Bool
prop_simplifica p i = undefined

-- La comprobación es

-- Generador de fórmulas
instance Arbitrary Form where
    arbitrary = sized form
        where form n | n <= 0    = atom
                     | otherwise = oneof [ atom
                                         , liftM Neg subform
                                         , liftM2 Dis subform subform ]
                     where atom    = oneof [elements [X,V,F]]
                           subform = form (n `div` 2)

Soluciones

import Test.QuickCheck
import Control.Monad

data Form = X
          | V
          | F
          | Neg Form
          | Dis Form Form
          deriving (Eq, Ord, Show)

valor :: Form -> Bool -> Bool
valor X i         = i
valor V _         = True
valor F _         = False
valor (Neg p) i   = not (valor p i)
valor (Dis p q) i = valor p i || valor q i

simplifica :: Form -> Form
simplifica X = X
simplifica V = V
simplifica F = F
simplifica (Neg p) = negacion (simplifica p)
    where negacion V       = F
          negacion F       = V
          negacion (Neg p) = p
          negacion p       = Neg p
simplifica (Dis p q) = disyuncion (simplifica p) (simplifica q)
    where disyuncion V q = V
          disyuncion F q = q
          disyuncion q V = V
          disyuncion q F = q
          disyuncion p q | p == q    = p
                         | otherwise = Dis p q

-- La propiedad es
prop_simplifica :: Form -> Bool -> Bool
prop_simplifica p i =
    valor (simplifica p) i == valor p i

-- La comprobación es
--    λ> quickCheck prop_simplifica
--    +++ OK, passed 100 tests.

-- Generador de fórmulas
instance Arbitrary Form where
    arbitrary = sized form
        where form n | n <= 0    = atom
                     | otherwise = oneof [ atom
                                         , liftM Neg subform
                                         , liftM2 Dis subform subform ]
                     where atom    = oneof [elements [X,V,F]]
                           subform = form (n `div` 2)