Menu Close

LMF2012: Formas normales en Haskell

En la clase de hoy del curso de Lógica matemática y fundamentos (de 3º de Grado en Matemáticas) se ha comentado las soluciones de los ejercicios sobre la implementación en Haskell de las formas normales.

Las soluciones de los ejercicios se muestran a continuación. En los ejercicios se usa el módulo SintaxisSemantica desarrollado en la clase del día 13 de marzo.

module FormasNormales where
 
-- ---------------------------------------------------------------------
-- Librería suxiliares                                                --
-- ---------------------------------------------------------------------
 
import SintaxisSemantica 
import Data.List
 
-- ---------------------------------------------------------------------
-- Equivalencia lógica                                                --
-- ---------------------------------------------------------------------
 
-- ---------------------------------------------------------------------
-- Ejercicio 1: Definir la función
--    esEquivalente :: Prop -> Prop -> Bool
-- tal que (esEquivalente f g) se verifica si f y g son
-- equivalentes. Por ejemplo,
--    esEquivalente (p <--> q) ((p --> q) /\ (q --> p))  ==>  True
--    esEquivalente (p --> q)  ((no p) \/ q)             ==>  True
--    esEquivalente (p /\ q)   (no ((no p) \/ (no q)))   ==>  True
--    esEquivalente (p \/ q)   (no ((no p) /\ (no q)))   ==>  True
-- ---------------------------------------------------------------------
 
esEquivalente :: Prop -> Prop -> Bool
esEquivalente f g =
    esValida (Equi f g)
 
-- ---------------------------------------------------------------------
-- Transformación a forma normal negativa                             --
-- ---------------------------------------------------------------------
 
-- ---------------------------------------------------------------------
-- Ejercicio 2: Definir la función
--    eliminaEquivalencias :: Prop -> Prop
-- tal que (eliminaEquivalencias f) es una fórmula equivalente a f sin
-- signos de equivalencia. Por ejemplo,
--    eliminaEquivalencias (p <--> q)
--    ==> ((p --> q) /\ (q --> p))
--    eliminaEquivalencias ((p <--> q) /\ (q <--> r))
--    ==> (((p --> q) /\ (q --> p)) /\ ((q --> r) /\ (r --> q)))
-- ---------------------------------------------------------------------
 
eliminaEquivalencias :: Prop -> Prop
eliminaEquivalencias (Atom f)   = 
    (Atom f)
eliminaEquivalencias (Neg f)    = 
    Neg (eliminaEquivalencias f) 
eliminaEquivalencias (Conj f g) = 
    Conj (eliminaEquivalencias f) (eliminaEquivalencias g) 
eliminaEquivalencias (Disj f g) = 
    Disj (eliminaEquivalencias f) (eliminaEquivalencias g) 
eliminaEquivalencias (Impl f g) = 
    Impl (eliminaEquivalencias f) (eliminaEquivalencias g) 
eliminaEquivalencias (Equi f g) = 
    Conj (Impl (eliminaEquivalencias f) (eliminaEquivalencias g))
         (Impl (eliminaEquivalencias g) (eliminaEquivalencias f))
 
-- ---------------------------------------------------------------------
-- Ejercicio 3: Definir la función
--    eliminaImplicaciones :: Prop -> Prop
-- tal que (eliminaImplicaciones f) es una fórmula equivalente a f sin
-- signos de implicación. Por ejemplo,
--    eliminaImplicaciones (p --> q)
--    ==> (no p \/ q)
--    eliminaImplicaciones (eliminaEquivalencias (p <--> q))
--    ==> ((no p \/ q) /\ (no q \/ p))
-- Nota: Se supone que f no tiene signos de equivalencia.
-- ---------------------------------------------------------------------
 
eliminaImplicaciones :: Prop -> Prop
eliminaImplicaciones (Atom f)   = 
    (Atom f)
eliminaImplicaciones (Neg f)    = 
    Neg (eliminaImplicaciones f) 
eliminaImplicaciones (Conj f g) = 
    Conj (eliminaImplicaciones f) (eliminaImplicaciones g) 
eliminaImplicaciones (Disj f g) = 
    Disj (eliminaImplicaciones f) (eliminaImplicaciones g) 
eliminaImplicaciones (Impl f g) = 
    Disj (Neg (eliminaImplicaciones f)) (eliminaImplicaciones g) 
 
-- ---------------------------------------------------------------------
-- Ejercicio 4: Definir la función
--    interiorizaNegación :: Prop -> Prop
-- tal que (interiorizaNegación f) es una fórmula equivalente a f donde
-- las negaciones se aplican sólo a fórmulas atómicas. Por ejemplo,
--    interiorizaNegación (no (no p))         ==>  p
--    interiorizaNegación (no (p /\ q))       ==>  (no p \/ no q)
--    interiorizaNegación (no (p \/ q))       ==>  (no p /\ no q)
--    interiorizaNegación (no (no (p \/ q)))  ==>  (p \/ q)
--    interiorizaNegación (no ((no p) \/ q))  ==>  (p /\ no q)
-- Nota: Se supone que f no tiene equivalencias ni implicaciones. 
-- ---------------------------------------------------------------------
 
interiorizaNegación :: Prop -> Prop
interiorizaNegación (Atom f)   = 
    (Atom f)
interiorizaNegación (Neg f)    = 
    interiorizaNegaciónAux f
interiorizaNegación (Conj f g) = 
    Conj (interiorizaNegación f) (interiorizaNegación g) 
interiorizaNegación (Disj f g) = 
    Disj (interiorizaNegación f) (interiorizaNegación g) 
 
interiorizaNegaciónAux :: Prop -> Prop
interiorizaNegaciónAux (Atom f)   = 
    Neg (Atom f)
interiorizaNegaciónAux (Neg f)    = 
    interiorizaNegación f 
interiorizaNegaciónAux (Conj f g) = 
    Disj (interiorizaNegaciónAux f) (interiorizaNegaciónAux g) 
interiorizaNegaciónAux (Disj f g) = 
    Conj (interiorizaNegaciónAux f) (interiorizaNegaciónAux g) 
 
-- ---------------------------------------------------------------------
-- Ejercicio 5: Definir la función
--    formaNormalNegativa :: Prop -> Prop
-- tal que (formaNormalNegativa f) es una fórmula equivalente a f en
-- forma normal negativa. Por ejemplo,
--    formaNormalNegativa (p <--> q)
--    ==> ((no p \/ q) /\ (no q \/ p))
--    formaNormalNegativa ((p \/ (no q)) --> r)
--    ==> ((no p /\ q) \/ r)
--    formaNormalNegativa ((p /\ (q --> r)) --> s)
--    ==> ((no p \/ (q /\ no r)) \/ s)
-- ---------------------------------------------------------------------
 
formaNormalNegativa :: Prop -> Prop
formaNormalNegativa f =
    interiorizaNegación (eliminaImplicaciones (eliminaEquivalencias f))
 
-- ---------------------------------------------------------------------
-- Literales                                                          --
-- ---------------------------------------------------------------------
 
-- ---------------------------------------------------------------------
-- Ejercicio 6: Definir la función
--    literal :: Prop -> Bool
-- tal que (literal f) se verifica si la fórmula F es un literal. Por
-- ejemplo, 
--    literal p               ==>  True
--    literal (no p)          ==>  True
--    literal (no (p --> q))  ==>  False
-- ---------------------------------------------------------------------
 
literal :: Prop -> Bool
literal (Atom f)       = True
literal (Neg (Atom f)) = True
literal _              = False
 
-- ---------------------------------------------------------------------
-- Ejercicio 7: Definir el tipo de dato Literal como sinónimo de
-- fórmula. 
-- ---------------------------------------------------------------------
 
type Literal = Prop
 
-- ---------------------------------------------------------------------
-- Ejercicio 8: Definir la función
--    complementario :: Literal -> Literal
-- tal que (complementario l) es el complementario de l. Por ejemplo,
--    complementario p       ==>  no p
--    complementario (no p)  ==>  p
-- ---------------------------------------------------------------------
 
complementario :: Literal -> Literal
complementario (Atom f)       = Neg (Atom f)
complementario (Neg (Atom f)) = Atom f
 
-- ---------------------------------------------------------------------
-- Ejercicio 9: Definir la función
--    literalesFórmulaFNN :: Prop -> [Literal]
-- tal que (literalesFórmulaFNN f) es el conjunto de los literales de la
-- fórmula en forma normal negativa f.
--    literalesFórmulaFNN (p \/ ((no q) \/ r))  ==>  [p,no q,r]
--    literalesFórmulaFNN p                     ==>  [p]
--    literalesFórmulaFNN (no p)                ==>  [no p]
-- ---------------------------------------------------------------------
 
literalesFórmulaFNN :: Prop -> [Literal]
literalesFórmulaFNN (Disj f g) =
    (literalesFórmulaFNN f) `union` (literalesFórmulaFNN g)
literalesFórmulaFNN (Conj f g) =
    (literalesFórmulaFNN f) `union` (literalesFórmulaFNN g)
literalesFórmulaFNN f          = [f]
 
-- ---------------------------------------------------------------------
-- Transformación a forma normal conjuntiva                           --
-- ---------------------------------------------------------------------
 
-- ---------------------------------------------------------------------
-- Ejercicio 10: Definir la función
--    interiorizaDisyunción :: Prop -> Prop
-- tal que (interiorizaDisyunción f) es una fórmula equivalente a f
-- donde las disyunciones sólo se aplica a disyunciones o literales. Por
-- ejemplo,  
--    interiorizaDisyunción (p \/ (q /\ r))  ==>  ((p \/ q) /\ (p \/ r))
--    interiorizaDisyunción ((p /\ q) \/ r)  ==>  ((p \/ r) /\ (q \/ r))
-- Nota: Se supone que f está en forma normal negativa.
-- ---------------------------------------------------------------------
 
interiorizaDisyunción :: Prop -> Prop
interiorizaDisyunción (Disj (Conj f1 f2) g) =
   interiorizaDisyunción
   (Conj (Disj (interiorizaDisyunción f1) (interiorizaDisyunción g))
         (Disj (interiorizaDisyunción f2) (interiorizaDisyunción g)))
interiorizaDisyunción (Disj f (Conj g1 g2)) =
   interiorizaDisyunción
   (Conj (Disj (interiorizaDisyunción f) (interiorizaDisyunción g1))
         (Disj (interiorizaDisyunción f) (interiorizaDisyunción g2)))
interiorizaDisyunción (Conj f g) =
   Conj (interiorizaDisyunción f) (interiorizaDisyunción g)
interiorizaDisyunción (Disj f g)
   | tieneConj (Disj f g) = interiorizaDisyunción
                            (Disj (interiorizaDisyunción f)
                                  (interiorizaDisyunción g))
   | otherwise = Disj (interiorizaDisyunción f)
                      (interiorizaDisyunción g)
interiorizaDisyunción f = f
 
tieneConj:: Prop -> Bool
tieneConj (Conj f g) = True
tieneConj (Disj f g) = (tieneConj f) || (tieneConj g)
tieneConj _          = False
 
-- ---------------------------------------------------------------------
-- Ejercicio 11: Definir la función
--    formaNormalConjuntiva :: Prop -> Prop
-- tal que (formaNormalConjuntiva f) es una fórmula equivalente a f en
-- forma normal conjuntiva. Por ejemplo,
--    formaNormalConjuntiva (p /\ (q --> r))
--    ==> (p /\ (no q \/ r))
--    formaNormalConjuntiva (no (p /\ (q --> r)))
--    ==> ((no p \/ q) /\ (no p \/ no r))
--    formaNormalConjuntiva (no(p <--> r))
--    ==> (((p \/ r) /\ (p \/ no p)) /\ ((no r \/ r) /\ (no r \/ no p)))
-- ---------------------------------------------------------------------
 
formaNormalConjuntiva :: Prop -> Prop
formaNormalConjuntiva f =
    interiorizaDisyunción (formaNormalNegativa f)
 
-- ---------------------------------------------------------------------
-- Transformación a forma normal disyuntiva                           --
-- ---------------------------------------------------------------------
 
-- ---------------------------------------------------------------------
-- Ejercicio 12: Definir la función
--    interiorizaConjunción :: Prop -> Prop
-- tal que (interiorizaConjunción f) es una fórmula equivalente a f
-- donde las conjunciones sólo se aplica a conjunciones o literales. Por
-- ejemplo,  
--    interiorizaConjunción (p /\ (q \/ r))  ==>  ((p /\ q) \/ (p /\ r))
--    interiorizaConjunción ((p \/ q) /\ r)  ==>  ((p /\ r) \/ (q /\ r))
-- Nota: Se supone que f está en forma normal negativa.
-- ---------------------------------------------------------------------
 
interiorizaConjunción :: Prop -> Prop
interiorizaConjunción (Conj (Disj f1 f2) g) =
    interiorizaConjunción
    (Disj (Conj (interiorizaConjunción f1) (interiorizaConjunción g))
          (Conj (interiorizaConjunción f2) (interiorizaConjunción g)))
interiorizaConjunción (Conj f (Disj g1 g2)) =
    interiorizaConjunción
    (Disj (Conj (interiorizaConjunción f) (interiorizaConjunción g1))
          (Conj (interiorizaConjunción f) (interiorizaConjunción g2)))
interiorizaConjunción (Disj f g) =
    Disj (interiorizaConjunción f) (interiorizaConjunción g)
interiorizaConjunción f = f
 
-- ---------------------------------------------------------------------
-- Ejercicio 13: Definir la función
--    formaNormalDisyuntiva :: Prop -> Prop
-- tal que (formaNormalDisyuntiva f) es una fórmula equivalente a f en
-- forma normal disyuntiva. Por ejemplo,
--    formaNormalDisyuntiva (p /\ (q --> r))
--    ==> ((p /\ no q) \/ (p /\ r))
--    formaNormalDisyuntiva (no (p /\ (q --> r)))
--    ==> (no p \/ (q /\ no r))
-- ---------------------------------------------------------------------
 
formaNormalDisyuntiva :: Prop -> Prop
formaNormalDisyuntiva f =
    interiorizaConjunción (formaNormalNegativa f)
Sin categoría