We will follow Daniel Wagner's excellent suggestion and use the "naive representation (your first), as well as a function that selects one of the famous normal forms." We will use the algebraic normal form for two reasons. The main reason is that the algebraic normal form does not require an enumeration of all possible values of the variable type stored in Property . The algebraic normal form is also quite simple.
Algebraic normal form
We will represent an algebraic normal form with newtype ANF a = ANF [[a]] , which does not export its constructor. Each internal list is a conjunction (i-ing) of all its predicates; if the internal list is empty, it is always true. An external list is exclusive or contains all its predicates; if it is empty, it is incorrect.
module Logic ( ANF (getANF), anf, ... ) newtype ANF a = ANF {getANF :: [[a]]} deriving (Eq, Ord, Show)
We will endeavor to ensure that any ANF constructor is canonical. We will build ANF so that the internal list is always sorted and unique. The external list will also be sorted. If there are two (or an even number) of identical elements in the external list, we will delete both of them. If the external list contains an odd number of identical elements, we will delete all but one of them.
Using the functions from Data.List.Ordered in data-ordlist , we can clear the list of lists representing xor-ing conjunctions in ANF with the removal of lists and duplicates.
import qualified Data.List.Ordered as Ordered anf :: Ord a => [[a]] -> ANF a anf = ANF . nubPairs . map Ordered.nubSort nubPairs :: Ord a => [a] -> [a] nubPairs = removePairs . Ordered.sort where removePairs (x:y:zs) | x == y = removePairs zs | otherwise = x:removePairs (y:zs) removePairs xs = xs
Logical expressions form a Boolean algebra , which is a bounded lattice with an additional distribution law and complement (negation). Using the existing BoundedLattice class in lattices , we can define the BooleanAlgebra s class
import Algebra.Lattice class (BoundedLattice a) => BooleanAlgebra a where complement :: a -> a -- Additional Laws: -- a `join` complement a == top -- a `meet` complement a == bottom -- a `join` (b `meet` c) == (a `join` b) `meet` (a `join` c) -- a `meet` (b `join` c) == (a `meet` b) `join` (a `meet` c)
ANF a form a BooleanAlgebra when a has an Ord instance so that we can save ANF in canonical form.
The letter meet logical algebra is logical and . Logical and distributed by xor . We will take advantage of the fact that internal lists are already sorted to quickly merge them together.
instance (Ord a) => MeetSemiLattice (ANF a) where ANF xs `meet` ANF ys = ANF (nubPairs [Ordered.union xy | x <- xs, y <- ys])
Using the laws of De Morgan , join or logical or can be written in terms of meet or logical and .
instance (Ord a) => JoinSemiLattice (ANF a) where xs `join` ys = complement (complement xs `meet` complement ys)
The top grid is always true.
instance (Ord a) => BoundedMeetSemiLattice (ANF a) where top = ANF [[]]
The bottom lattice is always incorrect.
instance (Ord a) => BoundedJoinSemiLattice (ANF a) where bottom = ANF []
Logical and and logical or satisfy the law of absorption of the lattice, a join (a meet b) == a meet (a join b) == a .
instance (Ord a) => Lattice (ANF a) instance (Ord a) => BoundedLattice (ANF a)
Finally, the complement operation is a negation that can be done with xor with true.
instance (Ord a) => BooleanAlgebra (ANF a) where complement (ANF ([]:xs)) = ANF xs complement (ANF xs) = ANF ([]:xs)
Along with Pointed we can use BooleanAlgebra to define a class of things that contain logical expressions, Logical .
import Data.Pointed class Logical f where toLogic :: (Pointed g, BooleanAlgebra (ga)) => fa -> ga
The algebraic normal form has a logical expression.
xor :: BooleanAlgebra a => a -> a -> a p `xor` q = (p `join` q) `meet` complement (p `meet` q) instance Logical ANF where toLogic = foldr xor bottom . map (foldr meet top . map point) . getANF
The algebraic normal form is also Pointed and therefore can be converted to using toLogic .
instance Pointed ANF where point x = ANF [[x]] toANF :: (Logical f, Ord a) => fa -> ANF a toANF = toLogic
We can check if something Logical logically equivalent by comparing it if it is structurally equivalent when converting to canonical algebraic normal form.
equivalent :: (Logical f, Logical g, Ord a) => fa -> ga -> Bool equivalent ab = toANF a == toANF b
Convert Property to ANF
Logical expressions should form a Boolean algebra, which is a bounded lattice with an additional distribution law and complement (negation). To make Property more closely parallel to Boolean algebra, we need to add two more elements for the top and bottom boundaries of the lattice. top always True , and bottom always False . I will call these Trivial for properties, always True and Impossible for properties that are always False .
data Property a = And (Property a) (Property a) | Or (Property a) (Property a) | Not (Property a) | Property a | Trivial | Impossible deriving (Eq, Ord, Read, Show)
Property is an abstract syntax tree for a property. Its derived instances of Eq and Ord are only structural equality.
A Property - Logical , and we can transform it into any Pointed BooleanAlgebra .
instance Logical Property where toLogic (And ab) = (toLogic a) `meet` (toLogic b) toLogic (Or ab) = (toLogic a) `join` (toLogic b) toLogic (Not a) = complement (toLogic a) toLogic (Property a) = point a toLogic Trivial = top toLogic Impossible = bottom
Using the equivalent from the previous section and our Logical instance, we can check if the two properties are equivalent for some examples.
runExample :: (Ord a, Show a) => Property a -> Property a -> IO () runExample pq = if p `equivalent` q then putStrLn (show p ++ " == " ++ show q) else putStrLn (show p ++ " /= " ++ show q) main = do runExample (point 'a' `meet` point 'b') (point 'b' `meet` point 'a') runExample (point 'a' `meet` point 'b') (point 'b' `meet` point 'a' `meet` point 'a') runExample (point 'a' `meet` point 'b') (point 'b' `meet` point 'a' `join` point 'a') runExample (point 'a' `join` complement (point 'a')) (top) runExample (point 'a' `meet` complement (point 'a')) (bottom)
The following conclusion is issued here.
And (Property 'a') (Property 'b') == And (Property 'b') (Property 'a') And (Property 'a') (Property 'b') == And (And (Property 'b') (Property 'a')) (Pr operty 'a') And (Property 'a') (Property 'b') /= Or (And (Property 'b') (Property 'a')) (Pro perty 'a') Or (Property 'a') (Not (Property 'a')) == Trivial And (Property 'a') (Not (Property 'a')) == Impossible
To use these examples as written, we also need instances of BooleanAlgebra and Pointed for Property . The equivalence relation for the laws of BooleanAlgebra is an equivalent interpretation, not a structural equality of Property .
instance MeetSemiLattice (Property a) where meet = And instance BoundedMeetSemiLattice (Property a) where top = Trivial instance JoinSemiLattice (Property a) where join = Or instance BoundedJoinSemiLattice (Property a) where bottom = Impossible instance Lattice (Property a) instance BoundedLattice (Property a) instance BooleanAlgebra (Property a) where complement = Not instance Pointed Property where point = Property
Proof
Each Boolean function, and therefore every finite Property , has a unique representation in ANF . The BooleanAlgebra and Pointed instances for ANF have demonstrated that all Logical a and, therefore, each finite Property a and Boolean function indexed on a have a representation in ANF a . Let k be the number of inhabitants a . There are 2^(2^k) possible Boolean functions from k Boolean variables. Each ANF internal list is a collection of a s; there are 2^k possible sets a and, therefore, 2^k possible internal lists. An ANF external list is a collection of internal lists; each internal list may occur more than once in the external list. 2^(2^k) possible ANF a s are possible. Since each Boolean function has a representation in ANF and there are as many possible inhabitants of ANF as there are Boolean functions, each Boolean function has a unique representation in ANF .
Renouncement
The Ord instance for ANF is a structural order and, apart from equality, has nothing to do with the partial orders caused by the lattice structure.
An algebraic normal form can be exponentially larger than its input. The disjunction of the variable list n is of size .5*n*2^n . For example, length . getANF . foldr join bottom . map point $ ['a'..'g'] length . getANF . foldr join bottom . map point $ ['a'..'g'] length . getANF . foldr join bottom . map point $ ['a'..'g'] is 127 , and foldr join bottom . map point $ ['a'..'g'] foldr join bottom . map point $ ['a'..'g'] contains a total of 448 occurrences of 7 different variables.