rewriting-0.2: examples/logic/Logic.hs
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
-----------------------------------------------------------------------------
-- Copyright 2008, 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 Logic (Logic(..), isDNF, foldLogic, size, height, metaVars, matchLogic, (|->)) where
import Data.List
import Data.Maybe
import qualified Data.Set as S
import qualified Data.Map as M
import Test.QuickCheck
import Control.Monad
import Data.Char
import Generics.Regular.Rewriting
infixr 1 :<->:
infixr 2 :->:
infixr 3 :||:
infixr 4 :&&:
-- | The data type Logic is the abstract syntax for the domain
-- | of logic expressions.
data Logic = Var String
| Logic :->: Logic -- implication
| Logic :<->: Logic -- equivalence
| Logic :&&: Logic -- and (conjunction)
| Logic :||: Logic -- or (disjunction)
| Not Logic -- not
| T -- true
| F -- false
deriving (Show, Eq, Ord)
-- | The type LogicAlg is the algebra for the data type Logic
-- | Used in the fold for Logic.
type LogicAlg a = (String -> a, a -> a -> a, a -> a -> a, a -> a -> a, a -> a -> a, a -> a, a, a)
-- | foldLogic is the standard fold for Logic.
foldLogic :: LogicAlg a -> Logic -> a
foldLogic (var, impl, equiv, and, or, not, true, false) = rec
where
rec logic =
case logic of
Var x -> var x
p :->: q -> rec p `impl` rec q
p :<->: q -> rec p `equiv` rec q
p :&&: q -> rec p `and` rec q
p :||: q -> rec p `or` rec q
Not p -> not (rec p)
T -> true
F -> false
-- | evalLogic takes a function that gives a logic value to a variable,
-- | and a Logic expression, and evaluates the boolean expression.
evalLogic :: (String -> Bool) -> Logic -> Bool
evalLogic env = foldLogic (env, impl, (==), (&&), (||), not, True, False)
where
impl p q = not p || q
-- | eqLogic determines whether or not two Logic expression are logically
-- | equal, by evaluating the logic expressions on all valuations.
eqLogic p q = all (\f -> evalLogic f p == evalLogic f q) fs
where
xs = varsLogic p `union` varsLogic q
fs = map (flip elem) (subsets xs)
subsets :: [a] -> [[a]]
subsets = foldr op [[]]
where op a list = list ++ map (a:) list
-- | Functions noNot, noOr, and noAnd determine whether or not a Logic
-- | expression contains a not, or, and and constructor, respectively.
noNot, noOr, noAnd :: Logic -> Bool
noNot = foldLogic (const True, (&&), (&&), (&&), (&&), const False, True, True)
noOr = foldLogic (const True, (&&), (&&), (&&), \_ _ -> False, id, True, True)
noAnd = foldLogic (const True, (&&), (&&), \_ _ -> False, (&&), id, True, True)
-- | A Logic expression is atomic if it is a variable or a constant True or False.
isAtomic :: Logic -> Bool
isAtomic logic =
case logic of
Var _ -> True
Not (Var _) -> True
_ -> False
-- | Functions isDNF, and isCNF determine whether or not a Logix expression
-- | is in disjunctive normal form, or conjunctive normal form, respectively.
isDNF, isCNF :: Logic -> Bool
isDNF = all isAtomic . concatMap conjunctions . disjunctions
isCNF = all isAtomic . concatMap disjunctions . conjunctions
-- | Function disjunctions returns all Logic expressions separated by an or
-- | operator at the top level.
disjunctions :: Logic -> [Logic]
disjunctions F = []
disjunctions (p :||: q) = disjunctions p ++ disjunctions q
disjunctions logic = [logic]
-- | Function conjunctions returns all Logic expressions separated by an and
-- | operator at the top level.
conjunctions :: Logic -> [Logic]
conjunctions T = []
conjunctions (p :&&: q) = conjunctions p ++ conjunctions q
conjunctions logic = [logic]
size :: Logic -> Int
size = foldLogic (const 1, bin, bin, bin, bin, succ, 1, 1)
where bin x y = x+y+1
height :: Logic -> Int
height = foldLogic (const 1, bin, bin, bin, bin, succ, 1, 1)
where bin x y = 1 + (x `max` y)
-- | Count the number of implicationsations :: Logic -> Int
countImplications :: Logic -> Int
countImplications = foldLogic (const 0, \x y -> x+y+1, (+), (+), (+), id, 0, 0)
-- | Count the number of equivalences
countEquivalences :: Logic -> Int
countEquivalences = foldLogic (const 0, (+), \x y -> x+y+1, (+), (+), id, 0, 0)
-- | Count the number of binary operators
countBinaryOperators :: Logic -> Int
countBinaryOperators = foldLogic (const 0, binop, binop, binop, binop, id, 0, 0)
where binop x y = x + y + 1
-- | Count the number of double negations
countDoubleNegations :: Logic -> Int
countDoubleNegations = fst . foldLogic (const zero, bin, bin, bin, bin, notf, zero, zero)
where
zero = (0, False)
bin (n, _) (m, _) = (n+m, False)
notf (n, b) = if b then (n+1, False) else (n, True)
-- | Function varsLogic returns the variables that appear in a Logic expression.
varsLogic :: Logic -> [String]
varsLogic = foldLogic (return, union, union, union, union, id, [], [])
test = associativityAnd $ (Var "a" :||: Var "b") :||: (Var "c" :||: Var "d" :||: Var "e")
associativityAnd, associativityOr :: Logic -> [Logic]
associativityAnd = associativity conjunctions (:&&:) [T]
associativityOr = associativity disjunctions (:||:) [F]
-- Helper function (polymorphic, domain independent)
associativity :: (a -> [a]) -> (a -> a -> a) -> [a] -> a -> [a]
associativity f op nil = rec . f
where
rec ps
| n == 0 = nil
| n == 1 = ps
| otherwise = concatMap f [1 .. n-1]
where
n = length ps
f i = let (xs, ys) = splitAt i ps
in [ x `op` y | x <- rec xs, y <- rec ys ]
eqAssociative :: Logic -> Logic -> Bool
eqAssociative p q =
case (p, q) of
(Var x, Var y) -> x==y
(p1 :->: p2, q1 :->: q2) -> eqAssociative p1 q1 && eqAssociative p2 q2
(p1 :<->: p2, q1 :<->: q2) -> eqAssociative p1 q1 && eqAssociative p2 q2
(_ :&&: _, _ :&&: _) -> and $ zipWith eqAssociative (conjunctions p) (conjunctions q)
(_ :||: _, _ :||: _) -> and $ zipWith eqAssociative (disjunctions p) (disjunctions q)
(Not p1, Not q1 ) -> eqAssociative p1 q1
(T, T ) -> True
(F, F ) -> True
_ -> False
-- sized, no nested equivalences
-- arbLogic :: Bool -> Int -> Gen Logic
arbLogic b n
| n <= 1 = frequency
[ (1, oneof $ map return [F, T])
, (3, oneof $ map (return . Var) ["p", "q", "r"])
]
| otherwise = frequency
[ (4, arbLogic b 0)
, (2, bin (:->:))
, (i, liftM2 (:<->:) recF recF)
, (3, bin (:&&:))
, (3, bin (:||:))
, (3, liftM Not rec)
]
where
i = if b then 1 else 0
rec = arbLogic b (n `div` 2)
recF = arbLogic False (n `div` 2)
bin f = liftM2 f rec rec
-----------------------------------------------------------
--- Unification
type Substitution = M.Map Char Logic
isMetaVar :: Logic -> Maybe Char
isMetaVar (Var ['_', c]) = Just c
isMetaVar _ = Nothing
metaVars :: [Logic]
metaVars = [ Var ['_', c] | c <- ['a' .. 'z'] ]
(|->) :: Substitution -> Logic -> Logic
(|->) sub = foldLogic (var, (:->:), (:<->:), (:&&:), (:||:), Not, T, F)
where
var s = case isMetaVar (Var s) of
Just i -> fromMaybe (Var s) (M.lookup i sub)
_ -> Var s
matchLogic :: Logic -> Logic -> Maybe Substitution
matchLogic p q =
case isMetaVar p of
Just i -> return (M.singleton i q)
Nothing ->
case (p, q) of
(Var x, Var y) | x==y -> return M.empty
(p1 :->: p2, q1 :->: q2) -> matchPairs (p1, p2) (q1, q2)
(p1 :<->: p2, q1 :<->: q2) -> matchPairs (p1, p2) (q1, q2)
(p1 :&&: p2, q1 :&&: q2 ) -> matchPairs (p1, p2) (q1, q2)
(p1 :||: p2, q1 :||: q2 ) -> matchPairs (p1, p2) (q1, q2)
(Not p1, Not q1 ) -> matchLogic p1 q1
(T, T ) -> return M.empty
(F, F ) -> return M.empty
_ -> Nothing
where
matchPairs :: (Logic, Logic) -> (Logic, Logic) -> Maybe Substitution
matchPairs (x1, x2) (y1, y2) = do
s1 <- matchLogic x1 y1
s2 <- matchLogic (s1 |-> x2) y2
return (M.union s1 s2)
-----------------------------------------------------------
--- QuickCheck generator
instance Arbitrary Logic where
arbitrary = sized (arbLogic True)
coarbitrary logic =
case logic of
Var x -> variant 0 . coarbitrary (map ord x)
p :->: q -> variant 1 . coarbitrary p . coarbitrary q
p :<->: q -> variant 2 . coarbitrary p . coarbitrary q
p :&&: q -> variant 3 . coarbitrary p . coarbitrary q
p :||: q -> variant 4 . coarbitrary p . coarbitrary q
Not p -> variant 5 . coarbitrary p
T -> variant 6
F -> variant 7
#ifdef FixView
type instance PF Logic =
(((K String) :+: I :*: I) :+: (I :*: I :+: I :*: I))
:+:
((I :*: I :+: I) :+: (U :+: U))
instance Regular Logic where
from (Var x) = L (L (L (K x)))
from (p :<->: q) = L (L (R ((I (from p)) :*: (I (from q)))))
from (p :->: q) = L (R (L ((I (from p)) :*: (I (from q)))))
from (p :&&: q) = L (R (R ((I (from p)) :*: (I (from q)))))
from (p :||: q) = R (L (L ((I (from p)) :*: (I (from q)))))
from (Not p) = R (L (R (I (from p))))
from T = R (R (L U))
from F = R (R (R U))
to (L (L (L (K x)))) = Var x
to (L (L (R ((I p) :*: (I q))))) = to p :<->: to q
to (L (R (L ((I p) :*: (I q))))) = to p :->: to q
to (L (R (R ((I p) :*: (I q))))) = to p :&&: to q
to (R (L (L ((I p) :*: (I q))))) = to p :||: to q
to (R (L (R (I p)))) = Not (to p)
to (R (R (L U))) = T
to (R (R (R U))) = F
#else
type instance PF Logic =
(((K String) :+: I :*: I) :+: (I :*: I :+: I :*: I))
:+:
((I :*: I :+: I) :+: (U :+: U))
instance Regular Logic where
from (Var x) = L (L (L (K x)))
from (p :<->: q) = L (L (R ((I p) :*: (I q))))
from (p :->: q) = L (R (L ((I p) :*: (I q))))
from (p :&&: q) = L (R (R ((I p) :*: (I q))))
from (p :||: q) = R (L (L ((I p) :*: (I q))))
from (Not p) = R (L (R (I p)))
from T = R (R (L U))
from F = R (R (R U))
to (L (L (L (K x)))) = Var x
to (L (L (R ((I p) :*: (I q))))) = p :<->: q
to (L (R (L ((I p) :*: (I q))))) = p :->: q
to (L (R (R ((I p) :*: (I q))))) = p :&&: q
to (R (L (L ((I p) :*: (I q))))) = p :||: q
to (R (L (R (I p)))) = Not p
to (R (R (L U))) = T
to (R (R (R U))) = F
#endif
instance Rewrite Logic