Sistema certificado de decisión proposicional basado en polinomios

Sistema certificado de decisi´on proposicional basado en polinomios Jos´e A. Alonso-Jim´enez, Gonzalo A. Aranda-Corral y Joaqu´ın Borrego-D´ıaz Dpto. Ciencias de la Computaci´on e Inteligencia Artificial ETS Ingenier´ıa Inform´atica - Universidad de Sevilla. Avda. Reina Mercedes s.n. 41012-Sevilla , Spain {jalonso, jborrego, garanda}@us.es Abstract. En [2] introducimos una regla de inferencia para la l´ogica proposicional (basado en el uso de la derivaci´on de polinomios) denominada regla de independencia, dise˜nada para el c´alculo de retracciones conservativas, y que sirve para dise˜nar un procedimiento de decisi´on proposicional. En el presente trabajo presentamos una implementaci´on en Haskell del procedimiento y su certificaci´on mediante QuickCheck. 1 Introducci´on Este trabajo puede considerarse como un trabajo de tr´ansito: es la implementaci´on en Haskell[7] y certificaci´on con QuickCheck[4] del procedimiento de decisi´on introducido en [2] y su objetivo es la verificaci´on formal de la implementaci´on en el sistema Isabelle. S´olo presentamos los elementos m´as destacados, el c´odigo completo puede consultarse en CLAI2009.hs. La regla de independencia, en la que se basa el procedimiento de decisi´on, se basa a su vez en una interpretaci´on l´ogica de la derivaci´on polinomial en caracter´ıstica 2. La idea de un operador de derivaci´on sobre f´ormulas proposicionales consiste en la traducci´on de las derivaciones usuales para aplicarlas sobre f´ormulas v´ıa la traducci´on cl´asica entre f´ormulas y polinomios sobre cuerpos finitos [5] (v´ease tambi´en [3]). Para m´as detalles sobre la definici´on formal y sus propiedades se puede consultar [2]. En [1] se aplica la derivaci´on y la regla para extender los m´etodos cl´asicos de exploraci´on de atributos en contextos formales. La derivada booleana es una herramienta muy utilizada en el c´alculo de funciones booleanas (cf. [8]). En nuestro, caso, el operador sobre f´ormulas se obtiene como una traducci´on de los operadores usuales de derivaci´on sobre anillos, es decir, operadores sobre un anillo R d :R→Rverificando que: 1. d(a+b) = d(a) + d(b) 2. d(a·b) = d(a)·b+a·d(b) 102 J. A. Alonso-Jim´enez, G. A. Aranda-Corral, J. Borrego-D´ıaz Una derivaci´on booleana es una aplicaci´on ∂:PForm →PForm tal que existe una derivaci´on dsobre F2[x] tal que el siguiente diagrama es conmutativo PForm ∂ →PForm π↓#↑Θ F2[x]d →F2[x] (donde πyΘson las transformaciones usuales entre polinomios y f´ormulas proposicionales. Es decir ∂=Θ◦d◦π Si d=∂ ∂xp, se denota ∂por ∂ ∂p . La f´ormula ∂ ∂p (F) expresa la dependencia del valor de Fcon respecto al valor de p, es decir, ∂ ∂p F≡ ¬(F{p/¬p} ↔ F). La regla de independecia (o regla ∂) sobre dos f´ormulas polinomiales (polinomios de grado a lo sumo 1 con respecto a cualquier variable) a1, a2∈F2[x] se define como: a1, a2 1 + Φ£(1 + a1·a2)(1 + a1·∂ ∂x a2+a2·∂ ∂x a1+∂ ∂x a1·∂ ∂x a2)¤ donde Φ(X α∈I xα) = X α∈I xsg(α)ysg(α1,...,αn) = (min(1, δ1),...,min(1, δn)) Al resultado lo denotamos por ∂x(a1, a2). Es decir, si ai=bi+xp·ci,con degxp(bi) = degxp(ci) = 0 (i= 1,2), ∂x(b1+xp·c1, b2+xp·c2) = Φ[1 + (1 + b1·b2)[1 + (b1+c1)(b2+c2)]] La regla de independencia sobre f´ormulas es: ∂p(F1, F2) := Θ(∂xp(π(F1), π(F2))). El c´alculo inducido por la regla de independencia es adecuado y refutacionalmente completo [2]. La prueba de la completitud muestra, de hecho, un procedimiento de decisi´on basado en la regla que consiste en la retracci´on conservativa del conjunto de f´ormulas a analizar, eliminando una a una las variables proposicionales: Si Γes un conjunto de f´ormulas inconsistente, entonces Γ⊢∂⊥. La prueba consiste en calcular los conjuntos ∂k[Γ] (k≤n) definidios por recursion como sigue: ∂0[Γ] := Γand, if k≥1, ∂k[Γ] := {∂pk(F1, F2) : F1, F2∈∂k−1[Γ]} N´otese que si F∈∂k[Γ], entonces var(F)⊆ {pk+1,...pn}. Por tanto, ∂n[Γ]⊆ {⊤,⊥}. Se verifica que Γis inconsistente si y s´olo si ⊥ ∈ ∂n(Γ). Sistema certificado de decisi´on proposicional basado en polinomios 103 2 Formalizaci´on de la L´ogica proposicional Esta secci´on se describen la implementaci´on en Haskell de los conceptos de la l´ogica proposicional necesarios para la certificaci´on de nuestro procedimiento de decisi´on. 2.1 Gram´atica de la l´ogica proposicional Los s´ımbolos proposicionales se representar´an mediante cadenas y las f´ormulas proposicionales se definen por recursi´on: –⊤y⊥son f´ormulas. –Si Aes una f´ormula, tambi´en lo es ¬A. –Si AyBson f´ormulas, entonces (A∧B), (A∨B), (A→B) y (A↔B) tambi´en lo son. mediante los constructores T, F, Neg, Conj, Disj, Impl y Equiv, respectivamente. Para facilitar su escritura definimos las f´ormulas at´omicas p,q,rysas´ı como las funciones para las conectivas no,/\,\/,--> y<-->. As´ımismo, se define el procedimiento show para facilitar la lectura de f´ormulas y el procedimiento arbitrary para generar f´ormulas aleatoriamente. 2.2 Sem´antica de la l´ogica proposicional Las interpretaciones las representamos como listas de f´ormulas, entendiendo que las f´ormulas verdaderas son las que pertenecen a la lista. type Interpretacion = [FProp] Por recursi´on, se define la funci´on (significado f i) que es el significado de la f´ormula fen la interprestaci´on iy a partir de ella las funciones para reconocer si una interpretaci´on es modelo de una f´ormula o de un conjunto de f´ormulas. esModeloFormula :: Interpretacion -> FProp -> Bool esModeloFormula i f = significado f i esModeloConjunto :: Interpretacion -> [FProp] -> Bool esModeloConjunto i s = and [esModeloFormula i f | f <- s] Por recursi´on se define la funci´on (simbolosPropForm f) que es el conjunto formado por todos los s´ımbolos proposicionales que aparecen en la f´ormula f. A partir de ella, se definen las funciones para generar las interpretaciones y los modelos de una f´ormula 104 J. A. Alonso-Jim´enez, G. A. Aranda-Corral, J. Borrego-D´ıaz interpretacionesForm :: FProp -> [Interpretacion] interpretacionesForm f = subconjuntos (simbolosPropForm f) modelosFormula :: FProp -> [Interpretacion] modelosFormula f = [i | i <- interpretacionesForm f, esModeloFormula i f] An´alogamente se generan los modelos de conjuntos de f´ormulas modelosConjunto :: [FProp] -> [Interpretacion] modelosConjunto s = [i | i <- interpretacionesConjunto s, esModeloConjunto i s] interpretacionesConjunto :: [FProp] -> [Interpretacion] interpretacionesConjunto s = subconjuntos (simbolosPropConj s) donde (simbolosPropConj s) es el conjunto de los s´ımbolos proposiciones del conjunto de f´ormulas s. Finalmente se definen las funciones para reconocer si un conjunto de f´ormulas es inconsistente, si una f´ormula es consecuencia de un conjunto de f´ormulas, si una f´ormula es v´alida y si dos f´ormulas son equivalentes: esInconsistente :: [FProp] -> Bool esInconsistente s = modelosConjunto s == [] esConsecuencia :: [FProp] -> FProp -> Bool esConsecuencia s f = esInconsistente (Neg f:s) esValida :: FProp -> Bool esValida f = esConsecuencia [] f equivalentes :: FProp -> FProp -> Bool equivalentes f g = esValida (f <--> g) 3 Formalizaci´on del ´algebra de polinomios sobre Z/2Z 3.1 Representaci´on de polinomios Las variables se representan por cadenas. Los monomios son productos de variables y los representamos por listas ordenadas de variables. Los polinomios son suma de monomios y los representamos por listas ordenadas de monomios. Sistema certificado de decisi´on proposicional basado en polinomios 105 type Variable = String data Monomio = M [Variable] deriving (Eq, Ord) data Polinomio = P [Monomio] deriving (Eq, Ord) Los reconocedores de monomios y polinomios se definen por esMonomio :: Monomio -> Bool esMonomio (M vs) = vs == sort (nub vs) esPolinomio :: Polinomio -> Bool esPolinomio (P ms) = ms == sort (nub ms) El monomio correspondiente a la lista vac´ıa es el monomio uno, el polinomio correspondiente a la lista vac´ıa es el polinomio cero y el correspondiente a la lista cuyo ´unico elemento es el monomio uno es el polinomio uno, mUno :: Monomio mUno = M [] cero, uno :: Polinomio cero = P [] uno = P [mUno] 3.2 Operaciones con polinomios Las definiciones de suma de polinomios y producto de polinomios son suma :: Polinomio -> Polinomio -> Polinomio suma (P []) (P q) = (P q) suma (P p) (P q) = P (sumaAux p q) where sumaAux [] y = y sumaAux (c:r) y | elem c y = sumaAux r (delete c y) | otherwise = insert c (sumaAux r y) producto :: Polinomio -> Polinomio -> Polinomio producto (P []) _ = P [] producto (P (m:ms)) q = suma (productoMP m q) (producto (P ms) q) productoMP :: Monomio -> Polinomio -> Polinomio productoMP m1 (P []) = P [] productoMP m1 (P (m:ms)) = suma (P [productoMM m1 m]) (productoMP m1 (P ms)) productoMM :: Monomio -> Monomio -> Monomio productoMM (M x) (M y) = M (sort (x ‘union‘ y)) 106 J. A. Alonso-Jim´enez, G. A. Aranda-Corral, J. Borrego-D´ıaz 3.3 Generaci´on de polinomios Para generar aleatoriamente polinomios se definen generadores de caracteres de letras min´usculas, de variables con longitud 1 ´o 2, de monomios con el n´umero de variables entre 0 y 3 y de polinomios con el n´umero de monomios entre 0 y 3. caracteres :: Gen Char caracteres = chr ‘fmap‘ choose (97,122) variables :: Gen String variables = do k <- choose (1,2) vectorOf k caracteres monomios :: Gen Monomio monomios = do k <- choose (0,3) vs <- vectorOf k variables return (M (sort (nub vs))) polinomios :: Gen Polinomio polinomios = do k <- choose (0,3) ms <- vectorOf k monomios return (P (sort (nub ms))) Por ejemplo, *Main> sample polinomios 0 pp*sa gn*nf*zg Declaramos los polinomios instancias de Arbitrary, para usar QuickCheck, y de Num para facilitar la escritura. instance Arbitrary Polinomio where arbitrary = polinomios instance Num Polinomio where (+) = suma (*) = producto (-) = suma abs = undefined signum = undefined fromInteger = undefined Sistema certificado de decisi´on proposicional basado en polinomios 107 3.4 Certificaci´on con QuickCheck A continuaci´on vamos a usar la herramienta QuickCheck para la certificaci´on de la implementaci´on realizada de los polinomios, y posteriormente de los resultados que se obtengan tambi´en con f´ormulas proposicionales. QuickCheck es una herramienta que nos permite definir propiedades de los programas, que suponemos que son ciertas, y testearlas con un gran n´umero de ejemplos. Fue desarrollado por Claessen and Hughes para Haskell. Los puntos fuertes de esta herramienta son la facilidad para la escritura de propiedades y la rapidez de comprobaci´on, siendo para ello muy importante la definici´on correcta de los generadores de ejemplos. Adem´as, el uso de QuickCheck para la certificaci´on de nuestro programa es un paso previo a su verificaci´on formal con Isabelle. Recientemente se ha creado una herramienta de traducci´on autom´atica desde c´odigo Haskell a Isabelle, denominada Haskabelle1, pero que se encuentra en fase de desarrollo, y que pensamos usar para convertir nuestro c´odigo en una teor´ıa y poder demostrar formalmente sus propiedades. En el caso concreto de los polinomios certificaremos todas las operaciones implementadas exigiendo que est´en bien definidas y que cumplan las propiedades, que en sintaxis de QuickCheck se escribe de la siguiente forma: prop_polinomios :: Polinomio -> Polinomio -> Polinomio -> Bool prop_polinomios p q r = esPolinomio (p+q) && p+q == q+p && p+(q+r) == (p+q)+r && p + cero == p && p+p == cero && esPolinomio (p*q) && p*q == q*p && p*(q*r) == (p*q)*r && p * uno == p && p*p == p && p*(q+r) == (p*q)+(p*r) 4 Polinomios y f´ormulas proposicionales Los polinomios pueden transformarse en f´ormulas y las f´ormulas en polinomios de manera que las transformaciones sean reversibles. tr :: FProp -> Polinomio tr T = uno tr F = cero tr (Atom p) = P [M [p]] 1http://isabelle.in.tum.de/haskabelle 108 J. A. Alonso-Jim´enez, G. A. Aranda-Corral, J. Borrego-D´ıaz tr (Neg p) = uno + (tr p) tr (Conj a b) = (tr a) * (tr b) tr (Disj a b) = (tr a) + (tr b) + ((tr a) * (tr b)) tr (Impl a b) = uno + ((tr a) + ((tr a) * (tr b))) tr (Equi a b) = uno + ((tr a) + (tr b)) theta :: Polinomio -> FProp theta (P ms) = thetaAux ms where thetaAux [] = F thetaAux [m] = theta2 m thetaAux (m:ms) = no ((theta2 m) <--> (theta (P ms))) Las propiedades de reversibilidad pueden comprobarse con QuickCheck prop_theta_tr :: FProp -> Bool prop_theta_tr p = equivalentes (theta (tr p)) p prop_tr_theta :: Polinomio -> Bool prop_tr_theta p = tr (theta p) == p 5 Procedimiento de decisi´on proposicional basado en polinomios 5.1 Derivaci´on y regla delta La derivada de un polinomio prespecto de una variable xes la lista de monomios pque contienen x, elimin´andola. La derivaci´on se extiende a las f´ormulas mediante las funciones de transformaci´on deriv :: Polinomio -> Variable -> Polinomio deriv (P ms) x = P [M (delete x m) | (M m) <- ms, elem x m] derivP :: FProp -> Variable -> FProp derivP f v = theta (deriv (tr f) v) La regla delta para polinomios y f´ormula es deltap :: Polinomio -> Polinomio -> Variable -> Polinomio deltap a1 a2 v = uno + ((uno+a1*a2)*(uno+a1*c2+a2*c1+c1*c2)) where c1 = deriv a1 v c2 = deriv a2 v delta :: FProp -> FProp -> Variable -> FProp delta f1 f2 v = theta (deltap (tr f1) (tr f2) v) Sistema certificado de decisi´on proposicional basado en polinomios 109 Con QuickCheck se comprueba que la regla delta es adecuada prop_adecuacion_delta :: FProp -> FProp -> Bool prop_adecuacion_delta f1 f2 = and [esConsecuencia [f1, f2] (delta f1 f2 x) | x <- variablesProp (f1 /\ f2) variablesProp f = [v | (Atom v) <- simbolosPropForm f] 5.2 Procedimiento de decisi´on La funci´on (derivadas fs x) es la lista de las proposiciones distintas de ⊤ obtenidas aplicando la regla delta a dos f´ormulas de fs respecto de la variable x. derivadas :: [FProp] -> Variable -> [FProp] derivadas fs x = delete T (nub [delta f1 f2 x | (f1,f2) <- pares fs]) pares :: [a] -> [(a,a)] pares [] = [] pares [x] = [(x,x)] pares (x:xs) = [(x,y) | y <- (x:xs)] ++ (pares xs) A partir de la anterior, se determina cuando un conjunto de f´ormulas es refutable por la regla delta deltaRefutable :: [FProp] -> Bool deltaRefutable [] = False deltaRefutable fs = (elem F fs) || (deltaRefutable (derivadas fs (eligeVariable fs))) where eligeVariable fs = head (concat [variablesProp f | f <- fs]) Con QuickCheck se comprueba que el procedimiento de delta–refutaci´on es adecuado y completo prop_adecuacion_completitud_delta :: [FProp] -> Bool prop_adecuacion_completitud_delta fs = esInconsistente fs == deltaRefutable fs A partir del procedimiento de refutaci´on se pueden definir los de demostrabilidad y validez