1votos

Forma normal Conjuntiva en Haskell

por josejuan hace 6 meses

En lugar de NFC he puesto NFD, realmente son completamente equivalentes (cambiar AND por OR) pero NFD es la más usual de ver (y para mi de leer). Con generación de test automáticos.

Transformar formulas lógicas compuestas por (or, and y not) a su forma normal conjuntiva

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
98
99
100
101
102
103
104
105
106
107
108
109
{-# LANGUAGE OverloadedStrings, LambdaCase #-} 
import Data.String 
import Control.Monad.Reader 
import Data.List (nub, sort) 
import Test.QuickCheck 
 
-- Una expresión cualquiera puede expresarse con 
data Expr = Var String | Not Expr | Expr :|: Expr | Expr :&: Expr deriving Eq 
 
-- Entonces, convertir a forma normal disyuntiva (que es la más usual) 
nfd e = if e == e' then e else nfd e' 
  where e' = rec e 
        rec x@(Var _) = x 
        rec x@(Not (Var _)) = x 
        rec (Not (Not x)) = x 
        rec (Not (a :|: b)) = rec $ Not a :&: Not b 
        rec (Not (a :&: b)) = rec $ Not a :|: Not b 
        rec ((a :|: b) :&: c) = rec $ (a :&: c) :|: (b :&: c) 
        rec (a :&: (b :|: c)) = rec $ (a :&: b) :|: (a :&: c) 
        rec (a :&: b) = rec a :&: rec b 
        rec (a :|: b) = rec a :|: rec b 
 
-- Y ya está. 
 
 
 
 
 
 
-- Podemos evaluar cualquier expresión como la anterior si nos dan los 
-- valores de cada variable 
eval :: Expr -> Reader [(String, Bool)] Bool 
eval (Var x) = asks (lookup x) >>= maybe (fail $ "Var `" ++ x ++ "` not defined!") return 
eval (Not x) = not <$> eval x 
eval (a :&: b) = (&&) <$> eval a <*> eval b 
eval (a :|: b) = (||) <$> eval a <*> eval b 
 
-- Podemos mostrar de forma adecuada expresiones 
instance Show Expr where 
  show (Var x) = x 
  show (Not (Var x)) = "¬" ++ x 
  show (Not x) = "¬(" ++ show x ++ ")" 
  show (a :|: b) = show' a ++ " ∨ " ++ show' b where show' c@(_ :&: _) = "(" ++ show c ++ ")"; show' c = show c 
  show (a :&: b) = show' a ++ " ∧ " ++ show' b where show' c@(_ :|: _) = "(" ++ show c ++ ")"; show' c = show c 
 
-- Por comodidad, pueden definirse variables directamente desde cadenas 
instance IsString Expr where 
  fromString = Var 
 
-- Podemos obtener la evaluación de una fórmula cualquiera para todo el 
-- dominio (es decir, obtener toda la imagen) 
fullImage e = (runReader (eval e) . zipWith (,) vs) <$> bits (length vs) 
  where vs = nub $ sort $ vars e 
        vars (Var x) = [x] 
        vars (Not x) = vars x 
        vars (a :&: b) = vars a ++ vars b 
        vars (a :|: b) = vars a ++ vars b 
        bits 0 = [[]] 
        bits n = ((False:) <$> xs) ++ ((True:) <$> xs) where xs = bits (n - 1) 
 
 
-- Así, podemos verificar que la imagen de una expresión cualquiera sigue 
-- siendo la misma al reducirla a NFD 
testNFD e = fullImage e == fullImage (nfd e) 
 
 
{- Ahora podemos jugar un poco 
 
> let e1 = ("a" :&: Not ("b" :|: Not ("c" :&: Not "d")) :|: Not "e") :&: (Not "f" :&: ("g" :|: Not "h")) 
> e1 
((a ∧ ¬(b ∨ ¬(c ∧ ¬d))) ∨ ¬e) ∧ ¬f ∧ (g ∨ ¬h) 
> nfd e1 
(a ∧ ¬b ∧ c ∧ ¬d ∧ ¬f ∧ g) ∨ (a ∧ ¬b ∧ c ∧ ¬d ∧ ¬f ∧ ¬h) ∨ (¬e ∧ ¬f ∧ g) ∨ (¬e ∧ ¬f ∧ ¬h) 
> testNFD e1 
True 
> length $ fullImage e1 
256 
 
-} 
 
-- Claro que lo suyo es no tener que generar a mano instancias, podemos 
-- generarlas aleatoriamente, por lo que nuestros test serán automáticos 
-- y mucho más profundos 
instance Arbitrary Expr where 
  arbitrary = sized gen 
              where gen n = choose (1, max 1 (min 4 n)) >>= \case 
                              1 -> (Var . (:"") . (['a'..]!!)) <$> choose (1, 5) -- no más de 5 vars 
                              2 -> (:&:) <$> gen (n-1) <*> gen (n-1) 
                              3 -> (:|:) <$> gen (n-1) <*> gen (n-1) 
                              4 -> Not <$> gen (n-1) 
 
 
-- Por ejemplo, ahora generamos aleatoriamente montañas de fórmulas de 
-- longitudes muy dispares 
{- 
 
> mapM (\_ -> (length . show) <$> (generate arbitrary :: IO Expr)) [1..] 
[4573,20593,6,2682,1,43029,12657,2109,5,41722,22654,11,1,9,2,15251,34403,5,18662,1,9944,1,11405,13462,17508,22818,8945,6226,1,1,1,1,13979,12689,1,1,6,2,28917,1,1,1,23842,10133,1,15947,2348,5,1,2,14519,1,11006,300,1,5,27084,1,18956,18070,2,13507,2351,1,10234,1,1,9798,1,1,5382,19,11,9208,4730,1,1,4249,1,60366,12397,33657,6,3240,44,1,8298,9356,4586,12324,1,8800,14834,18016,12,28159,2024,19304,42432,1,4237,6,1,34792,1,12462,1,1,17,7929,5,27619,2,1,1,17608,17308,28861,26,20960,27,16,9,5,8,49715,57,2,1,1,12615,1,1,1,14838,2,25827,33049,21764,5,7747,6,1,19227,42815,2332,18057,20470,15379,12872,3383,9044,16,6,19,6182,.. 
 
-} 
 
-- Y probar nuestra propiedad automáticamente en instancias gigantes (ej. 
-- ver en la lista anterior instancias de decenas de miles de nodos 
{- 
 
> quickCheckWith (stdArgs {maxSize = 10, maxSuccess = 1000}) testNFD 
+++ OK, passed 1000 tests. 
 
-} 
1 comentario

Comenta la solución

Tienes que identificarte para poder publicar tu comentario.