ideas-0.5.8: src/Domain/RelationAlgebra/Formula.hs
-----------------------------------------------------------------------------
-- Copyright 2009, 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.Formula where
import Common.Uniplate (Uniplate(..))
import Common.Rewriting
import Common.Utils
import Control.Monad
import Data.Char
import Data.List
import Data.Maybe
import qualified Data.Set as S
import System.Random (StdGen, mkStdGen, split)
import Test.QuickCheck
infixr 2 :.:
infixr 3 :+:
infixr 4 :||:
infixr 5 :&&:
-- | 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
| V -- universe
| I -- identity relation
deriving (Show, Eq, Ord)
-- The empty relation is a smart-constructor: it has no (longer an) actual constructor
-- in the RelAlg datatype
empty :: RelAlg
empty = Not V
-------------------------------------
isAtom :: RelAlg -> Bool
isAtom r =
case r of
Var _ -> True
Not I -> True
Not V -> True
Not (Var _) -> True
Inv (Var _) -> True
Not (Inv (Var _)) -> True
V -> True
I -> True
_ -> 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
-- | The type RelAlgAlgebra is the algebra for the data type RelAlg
-- | Used in the fold for RelAlg.
type RelAlgAlgebra a = (String -> a, a -> a -> a, a -> a -> a, a -> a -> a, a -> a -> a, a -> a, a -> a, a, a)
-- | foldRelAlg is the standard folfd for RelAlg.
foldRelAlg :: RelAlgAlgebra a -> RelAlg -> a
foldRelAlg (var, comp, add, conj, disj, not, inverse, universe, ident) = rec
where
rec term =
case term of
Var x -> var x
p :.: q -> rec p `comp` rec q
p :+: q -> rec p `add` rec q
p :&&: q -> rec p `conj` rec q
p :||: q -> rec p `disj` rec q
Not p -> not (rec p)
Inv p -> inverse (rec p)
V -> universe
I -> ident
type Relation a = S.Set (a, a)
evalRelAlg :: Ord a => (String -> Relation a) -> [a] -> RelAlg -> Relation a
evalRelAlg var as = foldRelAlg (var, comp, add, conj, disj, not, inverse, universe, ident)
where
pairs = cartesian as as
comp p q = let f (a1, a2) c = (a1, c) `S.member` p && (c, a2) `S.member` q
in S.fromAscList [ x | x <- pairs, any (f x) as ]
add p q = let f (a1, a2) c = (a1, c) `S.member` p || (c, a2) `S.member` q
in S.fromAscList [ x | x <- pairs, all (f x) as ]
conj = S.intersection
disj = S.union
not p = S.fromAscList [ x | x <- pairs, x `S.notMember` p ]
inverse = S.map (\(x, y) -> (y, x))
universe = S.fromAscList pairs
ident = S.fromAscList [ (x, x) | x <- as ]
-- | Try to find a counter-example showing that the two formulas are not equivalent.
probablyEqual :: RelAlg -> RelAlg -> Bool
probablyEqual = probablyEqualWith (mkStdGen 28)
probablyEqualWith :: StdGen -> RelAlg -> RelAlg -> Bool
probablyEqualWith rng p q = all (\i -> eval i p == eval i q) (makeRngs 50 rng)
where
-- size of (co-)domain
as = [0..1]
-- number of attemps (with different randomly generated relations)
makeRngs n g
| n == 0 = []
| otherwise = let (g1, g2) = split g in g1 : makeRngs (n-1) g2
eval g = evalRelAlg (generate 100 g (arbRelations as)) as
inspect :: [Int]
inspect = map f [1..100]
where f i = S.size $ generate 100 (mkStdGen i) (arbRelations [0..9]) "p"
arbRelations :: Eq a => [a] -> Gen (String -> Relation a)
arbRelations as = promote (\s -> coarbitrary s (arbRelation as))
-- Suitable for small domains (e.g., with just 2 elements)
arbRelation :: Eq a => [a] -> Gen (Relation a)
arbRelation as = do
let f _ = oneof $ map return [True, False]
xs <- filterM f (cartesian as as)
return (S.fromAscList xs)
-- Alternative relation generator, which works best for slightly
-- larger domains (for instance, with 4 elements or more)
arbRelationAlt:: Eq a => [a] -> Gen (Relation a)
arbRelationAlt as = do
n <- choose (0, 100)
let f x = do
m <- choose (1::Int, 100)
return [ x | n < m ]
xs <- mapM f $ cartesian as as
return $ S.fromAscList $ concat xs
-- Test on a limited domain whether two relation algebra terms are equivalent
(===) :: RelAlg -> RelAlg -> Property
p === q = forAll arbitrary $ \n -> probablyEqualWith (mkStdGen n) p q
-- | Function varsRelAlg returns the variables that appear in a RelAlg expression.
varsRelAlg :: RelAlg -> [String]
varsRelAlg = foldRelAlg (return, union, union, union, union, id, id, [], [])
instance Uniplate RelAlg where
uniplate term =
case term of
s :.: t -> ([s, t], \[a, b] -> a :.: b)
s :+: t -> ([s, t], \[a, b] -> a :+: b)
s :&&: t -> ([s, t], \[a, b] -> a :&&: b)
s :||: t -> ([s, t], \[a, b] -> a :||: b)
Not s -> ([s], \[a] -> Not a)
Inv s -> ([s], \[a] -> Inv a)
_ -> ([], \[] -> term)
instance MetaVar RelAlg where
isMetaVar (Var a) = isMetaVar a
isMetaVar _ = Nothing
metaVar = Var . metaVar
instance ShallowEq RelAlg where
shallowEq expr1 expr2 =
case (expr1, expr2) of
(Var a , Var b ) -> a==b
(_ :.: _ , _ :.: _ ) -> True
(_ :+: _ , _ :+: _ ) -> True
(_ :&&: _, _ :&&: _) -> True
(_ :||: _, _ :||: _) -> True
(Not _ , Not _ ) -> True
(Inv _ , Inv _ ) -> True
(V , V ) -> True
(I , I ) -> True
_ -> False