En lógica matemática, un literal http://bit.ly/1RQ5yJU es una fórmula atómica o su negación. Se puede definir por el tipo de dato
data Literal = Atom String | Neg Literal deriving (Eq, Show) |
Por ejemplo, el literal los literales p y ¬q se representan por las expresiones (Atom “p”) y (Neg (Atom “q”)), respectivamente.
Una lista de literales (que se interpreta como su disyunción) es un tautología si contiene a una fórmula atómica y su negación.
Definir la función
tautologia :: [Literal] -> Bool |
tal que (tautologia xs) se verifica si la lista de literales xs es una tautología. Por ejemplo,
λ> tautologia [Atom "p", Neg (Atom "q"), Neg (Atom "p")] True λ> tautologia [Atom "p", Neg (Atom "q"), Neg (Atom "r")] False λ> tautologia [Atom "p", Neg (Atom "q"), Neg (Atom "q")] False |
Soluciones
import Data.List (intersect) data Literal = Atom String | Neg Literal deriving (Eq, Show) -- 1ª solución -- =========== tautologia1 :: [Literal] -> Bool tautologia1 xs = or [elem x xs && elem (Neg x) xs | x <- xs] -- 2ª solución -- =========== tautologia2 :: [Literal] -> Bool tautologia2 xs = not (null (intersect ns (map neg ps))) where (ps,ns) = span esPositivo xs neg x = Neg x esPositivo :: Literal -> Bool esPositivo (Atom _) = True esPositivo _ = False -- Comparación de eficiencia -- ========================= -- λ> tautologia1 (replicate 4000 (Atom "p")) -- False -- (6.70 secs, 1031428 bytes) -- λ> tautologia2 (replicate 4000 (Atom "p")) -- False -- (0.01 secs, 1061604 bytes) |
La solución anterior falla en casos con doble negación
Neg (Neg f)
. Una solución mejor:Las doble negaciones no son literales.