ideas-0.6: src/Domain/RelationAlgebra/Equivalence.hs
-----------------------------------------------------------------------------
-- Copyright 2010, Open Universiteit Nederland. This file is distributed
-- under the terms of the GNU General Public License. For more information,
-- see the file "LICENSE.txt", which is included in the distribution.
-----------------------------------------------------------------------------
-- |
-- Maintainer : bastiaan.heeren@ou.nl
-- Stability : provisional
-- Portability : portable (depends on ghc)
--
-----------------------------------------------------------------------------
module Domain.RelationAlgebra.Equivalence (isEquivalent) where
import Data.List
import Data.Maybe
import Domain.RelationAlgebra.Formula
import Common.Apply
import Common.Context
import Domain.RelationAlgebra.Strategies
{-
infixr 1 :.:
infixr 2 :+:
infixr 3 :||:
infixr 4 :&&:
-}
{-
-- | The data type RelAlg is the abstract syntax for the domain
-- | of logic expressions.
data RelAlg = Var String
| RelAlg :.: RelAlg -- composition
| RelAlg :+: RelAlg -- relative addition
| RelAlg :&&: RelAlg -- and (conjunction)
| RelAlg :||: RelAlg -- or (disjunction)
| Not RelAlg -- not
| Inv RelAlg -- inverse
| U -- universe
| E -- empty
deriving (Show, Eq, Ord)
-------------------------------------
isAtom :: RelAlg -> Bool
isAtom r =
case r of
Var x -> True
Not (Var x) -> True
Inv (Var x) -> True
Not (Inv (Var x)) -> True
U -> True
E -> True
otherwise -> False
isMolecule :: RelAlg -> Bool
isMolecule (r :.: s) = isMolecule r && isMolecule s
isMolecule (r :+: s) = isMolecule r && isMolecule s
isMolecule r = isAtom r
isDisj :: RelAlg -> Bool
isDisj (r :||: s) = isDisj r && isDisj s
isDisj r = isMolecule r
isCNF :: RelAlg -> Bool
isCNF (r :&&: s) = isCNF r && isCNF s
isCNF r = isDisj r
-}
-- | maak er een cnf van
isEquivalent :: RelAlg -> RelAlg -> Bool
isEquivalent x1 x2 =
let res1 = fromContext (applyD toCNF (inContext x1)) -- cnf van x1
res2 = fromContext (applyD toCNF (inContext x2)) -- cnf van x2
mols = union (getSetOfMolecules res1) (getSetOfMolecules res2)
(rs, r1, r2) = remCompls mols res1 res2
vals = createValuations rs
in all (\ v -> evalFormula r1 v == evalFormula r2 v) vals
{-
-- | zet 'm in cnf
solve (Inv (Inv (Not (Var "p")) :+: Not (Var "q"))) = Not (Var "p") :+: Not (Inv (Var "q"))
solve (Not (Not (Var "p") :+: Not (Inv (Var "q")))) = undefined
solve (Not (Inv (Inv (Not (Var "p")) :+: Not (Var "q")))) = undefined
solve (Not (Var "p" :.: Inv (Var "q"))) = Inv (Inv (Not (Var "p")) :+: Not (Var "q"))
solve x = x
-}
{-
ra1 = Var "a" :||: (Var "p" :.: Inv (Var "q"))
ra2 = Var "a" :||: (Inv (Inv (Not (Var "p")) :+: Not (Var "q")))
fa1 = Inv (Var "r" :+: Var "s")
fa2 = Inv (Var "s") :+: Inv (Var "r")
-}
{-
mols = union (getSetOfMolecules ra1) (getSetOfMolecules ra2)
triple@(t1, t2, t3) = remCompls mols ra1 ra2
vs = createValuations t1
bb = and (map (\v -> evalFormula ra1 v == evalFormula ra2 v) vs)
-}
remCompls :: [RelAlg] -> RelAlg -> RelAlg -> ([RelAlg], RelAlg, RelAlg)
remCompls rs r1 r2 =
let complements = searchForComplements rs
-- sub = [ (r1, Not r2) | (r1, r2) <- complements ]
in ( removeCompls rs complements
, substCompls r1 complements
, substCompls r2 complements
)
-- |
substCompls :: RelAlg -> [(RelAlg, RelAlg)] -> RelAlg
substCompls = foldl subst
subst :: RelAlg -> (RelAlg, RelAlg) -> RelAlg
subst r (r1, r2) =
case r of
p :&&: q -> subst p (r1, r2) :&&: subst q (r1, r2)
p :||: q -> subst p (r1, r2) :||: subst q (r1, r2)
_ -> if r == r1
then Not r2
else r
removeCompls :: [RelAlg] -> [(RelAlg, RelAlg)] -> [RelAlg]
removeCompls xs ys = [ x | x <- xs, notElem x (map snd ys)]
-- | Search for complements
searchForComplements ::[RelAlg] -> [(RelAlg, RelAlg)]
searchForComplements [] = []
searchForComplements (x:xs) = [(x,z) | z <- xs, isComplement x z] ++ searchForComplements xs
isComplement :: RelAlg -> RelAlg -> Bool
isComplement = (==) . fromContext . applyD toCNF . inContext . Not
-- FIXME: what should we do with the identity relation?
evalFormula :: RelAlg -> [(RelAlg, Bool)] -> Bool
evalFormula f val =
case lookup f val of
Just b -> b
Nothing ->
case f of
f1 :&&: f2 -> evalFormula f1 val && evalFormula f2 val
f1 :||: f2 -> evalFormula f1 val || evalFormula f2 val
Not f -> not (evalFormula f val)
V -> True
E -> False
x -> let value = lookup x val
in if value == Nothing
then error $ "evalFormula: molecule not in valuation " ++ show (f, val)
else fromJust value
-- | Get the set of molecules of an expression in CNF as list.
getSetOfMolecules :: RelAlg -> [RelAlg]
getSetOfMolecules = nub . getMolecules
where
getMolecules :: RelAlg -> [RelAlg]
getMolecules expr =
case expr of
p :&&: q -> getMolecules p ++ getMolecules q
p :||: q -> getMolecules p ++ getMolecules q
Not p -> getMolecules p
V -> []
E -> []
I -> []
p -> [p]
{-------------------------------------------------------------------
Given a varList, for example [x,y], function createValuations
creates all valuations:
[[(x,0),(y,0)],[(x,0),(y,1)],[(x,1),(y,0)],[(x,1),(y,1)]],
where (x,0) means: variable x equals 0.
--------------------------------------------------------------------}
type Molecule = RelAlg
-- type Valuation = (RelAlg, Bool)
createValuations :: [a] -> [[(a, Bool)]]
createValuations = foldr op [[]]
where op a vs = [ (a, b):v | v <- vs, b <- [True, False] ]
prop :: RelAlg -> RelAlg -> Bool
prop p q = isEquivalent p q == probablyEqual p q