PropLogic-0.9: FastPropLogic.hs
{-# LANGUAGE TypeSynonymInstances, FlexibleInstances, MultiParamTypeClasses #-}
-- |
-- This module defines three altenative representations for certain propositional normal forms, namely
--
-- > data XPDNF a -- a representation for Prime Disjunctive Normal Forms or PDNF's on a given atom type a
-- > data XPCNF a -- a representation for Prime Disjunctive Normal Forms or PDNF's on a given atom type a
-- > data MixForm a -- a type made of pairwise minimal DNF's and CNF's on a given atom type a
--
-- For each of these types there is a converter from and a converter to propositional formulas
--
-- > fromXPDNF :: Ord a => XPDNF a -> PropForm a toXPDNF :: Ord a => PropForm a -> XPDNF a
-- > fromXPCNF :: Ord a => XPCNF a -> PropForm a toXPCNF :: Ord a => PropForm a -> XPCNF a
-- > fromMixForm :: Ord a => MixForm a -> PropForm a toMixForm :: Ord a => PropForm a -> MixForm a
--
-- Each of these three types is turned into a propositional algebra 'PropAlg', i.e. for every ordered type @a@ of /atoms/
-- we have three instances
--
-- > PropAlg a (XPDNF a)
-- > PropAlg a (XPCNF a)
-- > PropAlg a (MixForm a)
--
-- Different to the two default propositional algebras on propositional formulas and truth tables, these three algebras comprise fast
-- function implementations and thus provide practical versions for propositional algebras, where propositions of arbitrary size
-- are processed in reasonable time.
-- In more detail the involved complexities are given in the table below (see ......).
-- It also explains, which of the three algebras should be chosen in an actual application.
--
-- Actually, this module is essentially a re-implementation of already explained concepts from "PropLogicCore" and "DefaultPropLogic"
-- and for the user it shouldn't be necessary to further explain how the algorithms work.
-- The remainder of this document is an attempt to do just that.
-- However, if you at least want an idea of what is going on here, it may suffice to read the first section with the introductory
-- example below.
{-
This module defines three altenative representations for certain propositional normal forms, namely
'XPDNF' a representation for Prime Disjunctive Normal Forms 'DefaultPropLogic.PDNF',
'XPCNF' a representation for Prime Conjunctive Normal Forms 'DefaultPropLogic.PCNF', and
'MixForm' a type comprising pairwise minimal DNFs and CNFs.
For each of these types there is a converter from and a converter to propositional formulas 'PropLogicCore.PropForm'.
For example, for 'XPDNF' this is @fromXPDNF :: XPDNF a -> PropForm a@ and @toXPDNF :: PropForm a -> XPDNF a@.
Each of these three types is turned into a propositional algebra, i.e. it becomes an instance of 'PropLogicCore.PropAlg'.
Different to the two default propositional algebras on propositional formulas and truth tables (see 'DefaultPropLogic.PropForm' and 'DefaultPropLogic.TruthTable'), these three algebras comprise fast function implementations and thus provide practical versions for propositional algebras for propositions of any size, not just for formulas with very small atoms sets.
-}
module FastPropLogic (
-- * Introductory example
-- ** Generating a Prime Disjunctive Normal Form, the default and the fast way
-- | Recall, that we already defined /Disjunctive Normal Forms/ and /Prime Disjunctive Normal Forms/ in "DefaultPropLogic" as
-- special versions of propositional formulas, along with a canonizer @pdnf@ to obtain these normal forms
--
-- > type DNF a = PropForm a
-- > type PDNF a = DNF a
-- > pdnf :: PropForm a -> PDNF a
--
-- For a simple example formula @p@, given by
--
-- > > p = DJ [EJ [A "x", A "y"], N (A "z")] :: PropForm String
--
-- more conveniently displayed by
--
-- > > display p
-- > [[x <-> y] + -z]
--
-- the PDNF of @p@ is then generated by
--
-- > > pdnf p
-- > DJ [CJ [EJ [A "x",F],EJ [A "y",F]],CJ [EJ [A "x",T],EJ [A "y",T]],CJ [EJ [A "z",F]]]
-- > > display (pdnf p)
-- > [[[x <-> false] * [y <-> false]] + [[x <-> true] * [y <-> true]] + [* [z <-> false]]]
--
-- or more conveniently displayed in its evaluated form
--
-- > > display (eval (pdnf p))
-- > [[-x * -y] + [x * y] + -z]
--
-- .............!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!..............................
--
-- (Actually, each converter pair is also part of each of the given algebras. For example, in the XPDNF instance holds:
-- 'fromXPDNF' = 'toPropForm' and 'toXPDNF' = 'fromPropForm'.)
--
-- ** XPDNF as a propositional algebra
--
-- | ,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,
-- ** The canonization steps
--
-- * Syntax
IAtom,
ILit,
ILine,
IForm,
XLit,
XLine,
XForm,
XPDNF(..), XPCNF(..),
MixForm(..),
-- * Conversions
-- ** IdxPropForm -- indexed propositional formulas
IdxPropForm,
tr,
-- | @tr f form@ replaces each atom form occurrence @(A x)@ in the formula @form@ by the new atom @(A (f x))@. Everything else remains.
iTr,
-- | @iTr [i_1,...,i_n] iform@ replaces each index @j@ in @iform@ by @i_j@. For example,
--
-- > > let iform = iForm [[-1,3,-4,5],[-2,-3,4,6]] :: IForm
-- > > iform
-- > COSTACK [COSTACK [-1,3,-4,5],COSTACK [-2,-3,4,6]]
-- > > iTr [7,8,9,10,11,12,13] iform
-- > COSTACK [COSTACK [-7,9,-10,11],COSTACK [-8,-9,10,12]]
-- > > iTr [2,4] iform
-- > -- error, because the index list [2,4] must at least be of length 6 to cover the indices 1,..,6 of iform.
idx,
-- | @idx [i_1,...,i_n] i_k@ returns @k@, i.e. the index of the index in the given index list.
-- Note, that the first member of the list starts with index 1, not 0. For example,
--
-- > > idx [2,4,6,8] 6
-- > 3
nth,
-- | @nth [i_1,...,i_n] k@ returns @i_k@, i.e. the @k@'s element in the list @[i_1,...,i_n]@, counting from @1@. For example,
--
-- > > nth [2,4,6,8] 3
-- > 6
itr,
iUni,
unifyIdxPropForms,
unifyXForms,
fromIdxPropForm,
toIdxPropForm,
newAtomsXForm,
-- ** Purely syntactical conversions to propositional formulas
iLIT, iNLC, iNLD, iCNF, iDNF,
xLIT, xNLC, xNLD, xCNF, xDNF,
-- ** Conversions to and from propositional formulas
toXPDNF,
toXPCNF,
toM2DNF, toM2CNF,
fromXPDNF,
fromXPCNF,
fromMixForm,
-- * The IForm algebra
-- ** Basic operations
isIAtom,
isILit,
isILine,
isIForm,
iLine,
iForm,
iAtom,
iBool,
negLit,
lineIndices,
formIndices,
lineLength,
formLength,
volume,
isOrderedForm,
orderForm,
-- ** The propositional algebra operations
atomForm,
botForm,
topForm,
formJoinForm,
formListJoin,
lineMeetLine,
lineMeetForm,
formMeetForm,
formListMeet,
dualLine,
dualForm,
invertLine,
invertForm,
negLine,
negForm,
formCojoinLine,
formCojoinForm,
formAntijoinLine,
formAntijoinForm,
elimLine,
elimForm,
lineCovLine,
lineCovForm,
formCovForm,
-- ** Generation of pairwise minimal, minimal and prime forms
-- *** Generation of prime and pairwise minimal forms of two lines
pairPartition,
CaseSymbol(..),
caseSymbol,
pairPrim',
pairMin',
xprim',
xmin',
xprim,
xmin,
pairPrim,
pairMin,
-- *** Implementation of the M- and the P-Procedure
isMinimalPair,
allPairs,
isPairwiseMinimal,
cPrime,
cPrimes,
mrec,
m2form,
iformJoinM2form,
primForm,
iformJoinPrimForm,
-- * The XForm operations
xformAtoms,
xformRedAtoms,
xformIrrAtoms,
-- * The propositional algebras
-- ** XPDNF and XPCNF
-- ** MixForm
mixToPDNF,
mixToPCNF,
-- * Complexities and choice of a algebra
-- |
--
-- > DefaultPropLogic. FastPropLogic
-- > -------------------------------------- -----------------------------------
-- > PropForm TruthTable XPDNF XPCNF MixForm
-- > --------------------------------------------------------------------------------------------------------------------------
-- > at
-- > false
-- > true
-- > neg
-- > conj, disj, subj, equij
-- > valid
-- > satisfiable
-- > subvalent
-- > equivalent
-- > covalent, disvalent,
-- > properSubvalent, properDisvalent
-- > atoms
-- > redAtoms, irrAtoms
-- > nullatomic
-- > subatomic, equiatomic
-- > .........
-- > .........
) where ---------------------------------------------------------------------------------------------------------------
-- import
import qualified List as L
import qualified TextDisplay as D
import qualified Olist as O
import qualified Costack as C
import PropLogicCore
import DefaultPropLogic (NegNormForm, negNormForm)
-- the types
type IAtom = Int -- I-Atom
type IdxPropForm a = (O.Olist a, PropForm IAtom) -- indexed propositional formula
-- type IntLitNormForm = PropForm ILit -- integer literal normal form
type ILit = Int -- I-Literal or integer literal type
type ILine = C.Costack ILit -- I-Line or integer line type
type IForm = C.Costack ILine -- I-Form or integer form type
type XLit a = (O.Olist a, ILit) -- X-Literal or indexed literal type
type XLine a = (O.Olist a, ILine) -- X-Line or indexed line type
type XForm a = (O.Olist a, IForm) -- X-Form or indexed form type
data XPDNF a = XPDNF (XForm a) -- Indexed/Extended Prime Disjunctive Normal Forms
deriving (Show, Read, Eq)
data XPCNF a = XPCNF (XForm a) -- Indexed/Extended Prime Conjunctive Normal Forms
deriving (Show, Read, Eq)
data MixForm a -- Mixed Forms:
= M2DNF (XForm a) -- Pairwise Minimal Disjunctive Normal Forms
| M2CNF (XForm a) -- Pairwise Minimal Conjunctive Normal Forms
| PDNF (XForm a) -- Prime Disjunctive Normal Forms
| PCNF (XForm a) -- Prime Conjunctive Normal Forms
deriving (Show, Read, Eq)
-- display
instance D.Display IForm where
textFrame form = textframe
where indices = formIndices form
oneRow line iL = if C.isEmpty line
then if null iL
then []
else [""] : (oneRow line (Prelude.tail iL))
else case compare (iAtom (C.head line)) (Prelude.head iL) of
GT -> [""] : (oneRow line (Prelude.tail iL))
EQ -> if iBool (C.head line)
then ['+' : (show (C.head line))] : (oneRow (C.tail line) (Prelude.tail iL))
else [show (C.head line)] : (oneRow (C.tail line) (Prelude.tail iL))
frameTable = map (\ line -> oneRow line indices) (C.toList form)
textframe = D.gridMerge (D.normalTextFrameTable frameTable)
instance D.Display a => D.Display (XForm a) where
textFrame (aL, form) = textframe
where headRow = map D.textFrame aL
indices = [1..(length aL)] :: [IAtom]
oneRow line iL = if C.isEmpty line
then if null iL
then []
else [""] : (oneRow line (Prelude.tail iL))
else case compare (iAtom (C.head line)) (Prelude.head iL) of
GT -> [""] : (oneRow line (Prelude.tail iL))
EQ -> if iBool (C.head line)
then ['+' : (show (C.head line))] : (oneRow (C.tail line) (Prelude.tail iL))
else [show (C.head line)] : (oneRow (C.tail line) (Prelude.tail iL))
tableBody = map (\ line -> oneRow line indices) (C.toList form)
textframe = D.gridMerge (D.normalTextFrameTable (headRow:tableBody))
titledTextFrame :: D.Display a => (String,String,String) -> XForm a -> D.TextFrame
titledTextFrame (empty, full, title) (aL,iform) =
if null aL
then if C.isEmpty iform
then D.textFrameBox (D.correctTextFrame [title,empty])
else D.textFrameBox (D.correctTextFrame [title,full])
else let body = D.textFrame (aL,iform)
textframe = D.textFrameBox (D.plainMerge (D.normalTextFrameTable [[[title]],[body]]))
in textframe
instance D.Display a => D.Display (XPDNF a) where
textFrame (XPDNF xform) = titledTextFrame ("false", "true", "XPDNF") xform
instance D.Display a => D.Display (XPCNF a) where
textFrame (XPCNF xform) = titledTextFrame ("true", "false", "XPCNF") xform
instance D.Display a => D.Display (MixForm a) where
textFrame (M2DNF xform) = titledTextFrame ("false", "true", "M2DNF") xform
textFrame (M2CNF xform) = titledTextFrame ("true", "false", "M2CNF") xform
textFrame (PDNF xform) = titledTextFrame ("false", "true", "PDNF") xform
textFrame (PCNF xform) = titledTextFrame ("true", "false", "PCNF") xform
-- order
instance Ord ILine where
compare left right =
if C.isEmpty left
then if C.isEmpty right
then EQ
else LT
else if C.isEmpty right
then GT
else case compare (iAtom (C.head left)) (iAtom (C.head right)) of
LT -> LT
GT -> GT
EQ -> case compare (iBool (C.head left)) (iBool (C.head right)) of
LT -> LT
GT -> GT
EQ -> compare (C.tail left) (C.tail right)
instance Ord IForm where
compare form1 form2 = if C.isEmpty form1
then if C.isEmpty form2
then EQ
else LT
else if C.isEmpty form2
then GT
else case compare (C.head form1) (C.head form2) of
LT -> LT
GT -> GT
EQ -> compare (C.tail form1) (C.tail form2)
-- convertions via IntLitNormForm
toXPDNF :: Ord a => PropForm a -> XPDNF a
toXPDNF p = XPDNF (aL, primForm iform)
where (aL, iprop) = toIdxPropForm p
iform = fromNegNF (negNormForm iprop)
fromNegNF (A n) = atomForm n
fromNegNF (N (A n)) = atomForm (negLit n)
fromNegNF F = botForm
fromNegNF T = topForm
fromNegNF (CJ pL) = formListMeet (map fromNegNF pL)
fromNegNF (DJ pL) = formListJoin (map fromNegNF pL)
toXPCNF :: Ord a => PropForm a -> XPCNF a
toXPCNF p = XPCNF (aL, primForm iform)
where (aL, iprop) = toIdxPropForm p
iform = fromNegNF (negNormForm iprop)
fromNegNF (A n) = atomForm n
fromNegNF (N (A n)) = atomForm (negLit n)
fromNegNF F = topForm
fromNegNF T = botForm
fromNegNF (CJ pL) = formListJoin (map fromNegNF pL)
fromNegNF (DJ pL) = formListMeet (map fromNegNF pL)
fromXPDNF :: Ord a => XPDNF a -> PropForm a
fromXPDNF (XPDNF xform) = xDNF xform
fromXPCNF :: Ord a => XPCNF a -> PropForm a
fromXPCNF (XPCNF xform) = xCNF xform
toM2DNF :: Ord a => PropForm a -> MixForm a
toM2DNF p = M2DNF (aL, m2form iform)
where (aL, iprop) = toIdxPropForm p
iform = fromIntLitNormForm (negNormForm iprop)
fromIntLitNormForm (A n) = atomForm n
fromIntLitNormForm F = botForm
fromIntLitNormForm T = topForm
fromIntLitNormForm (CJ pL) = formListMeet (map fromIntLitNormForm pL)
fromIntLitNormForm (DJ pL) = formListJoin (map fromIntLitNormForm pL)
toM2CNF :: Ord a => PropForm a -> MixForm a
toM2CNF p = M2CNF (aL, m2form iform)
where (aL, iprop) = toIdxPropForm p
iform = fromIntLitNormForm (negNormForm iprop)
fromIntLitNormForm (A n) = atomForm n
fromIntLitNormForm F = topForm
fromIntLitNormForm T = botForm
fromIntLitNormForm (CJ pL) = formListJoin (map fromIntLitNormForm pL)
fromIntLitNormForm (DJ pL) = formListMeet (map fromIntLitNormForm pL)
fromMixForm :: Ord a => MixForm a -> PropForm a
fromMixForm (M2DNF xform) = xDNF xform
fromMixForm (M2CNF xform) = xCNF xform
fromMixForm (PDNF xform) = xDNF xform
fromMixForm (PCNF xform) = xCNF xform
-- translations, indices and unifications
tr :: (s -> t) -> PropForm s -> PropForm t
tr f (A x) = A (f x)
tr f F = F
tr f T = T
tr f (N prop) = N (tr f prop)
tr f (CJ propL) = CJ (map (tr f) propL)
tr f (DJ propL) = DJ (map (tr f) propL)
tr f (SJ propL) = SJ (map (tr f) propL)
tr f (EJ propL) = EJ (map (tr f) propL)
iTr :: O.Olist IAtom -> IForm -> IForm
iTr aL form = C.map (iTr' aL 1) form
where iTr' aL n line = if C.isEmpty line
then line
else case compare n (iAtom (C.head line)) of
EQ -> if (iBool (C.head line))
then C.cons (head aL) (iTr' (tail aL) (n + 1) (C.tail line))
else C.cons (negLit (head aL)) (iTr' (tail aL) (n + 1) (C.tail line))
LT -> iTr' (tail aL) (n + 1) line
idx :: Ord a => O.Olist a -> a -> IAtom
idx [] x = error "idx -- empty list"
idx (y:yL) x = case compare y x of
LT -> 1 + (idx yL x)
EQ -> 1
GT -> error "idx -- atom is not a list member"
nth :: Ord a => O.Olist a -> IAtom -> a
nth oli n = if n < 1
then error ("nth -- undefined IAtom " ++ (show n))
else iter (n, oli)
where iter (i, []) = error ("nth -- index " ++ (show n) ++ " exceeds the list length")
iter (i, (x:xL)) = if i == 1
then x
else iter (i - 1, xL)
itr :: Ord a => O.Olist a -> O.Olist a -> Maybe (O.Olist IAtom)
itr s1 s2 = iter True s1 s2 1 [] -- True means that s1 == s2
where iter b [] [] n nL = if b then Nothing else (Just (reverse nL))
iter b [] (y:yL) n nL = iter False [] yL (n + 1) nL
iter b (x:xL) (y:yL) n nL = case compare x y of
EQ -> iter b xL yL (n + 1) (n:nL)
GT -> iter False (x:xL) yL (n + 1) nL
LT -> error "itr -- first list is not included by second list"
iUni :: Ord a => [O.Olist a] -> (O.Olist a, [Maybe (O.Olist IAtom)])
iUni sL = (aL, map (\ s -> itr s aL) sL)
where aL = O.unionList sL
unifyIdxPropForms :: Ord a => [IdxPropForm a] -> (O.Olist a, [PropForm IAtom])
unifyIdxPropForms pL = (aL, ipropL)
where (aL, maybeL) = iUni (map fst pL)
update (iprop, Nothing) = iprop
update (iprop, Just iL) = tr (nth iL) iprop
ipropL = map update (zip (map snd pL) maybeL)
unifyXForms :: Ord a => [XForm a] -> (O.Olist a, [IForm])
unifyXForms xformL = (aL, iformL)
where (aL, maybeL) = iUni (map fst xformL)
update (iform, Nothing) = iform
update (iform, Just iL) = iTr iL iform
iformL = map update (zip (map snd xformL) maybeL)
newAtomsXForm :: Ord a => XForm a -> O.Olist a -> XForm a
newAtomsXForm (oldAts, iform) newAts = (newAts, updateIForm (updateList oldAts newAts) iform)
where updateList :: Ord a => O.Olist a -> O.Olist a -> [Maybe IAtom]
updateList oldAts newAts = updateList' oldAts 1 newAts
where updateList' [] n newAts = []
updateList' (x:xL) n [] = L.replicate (length (x:xL)) Nothing
updateList' (x:xL) n (y:yL) = case compare x y of
LT -> Nothing : (updateList' xL n (y:yL))
EQ -> (Just n) : (updateList' xL (n + 1) yL)
GT -> updateList' (x:xL) (n + 1) yL
updateIForm :: [Maybe IAtom] -> IForm -> IForm
updateIForm maL iform = C.map (updateILine maL) iform
updateILine :: [Maybe IAtom] -> ILine -> ILine
updateILine maL iline = updateILine' 1 maL iline
where updateILine' _ [] _ = C.empty
updateILine' n (x:xL) iline =
if C.isEmpty iline
then iline
else case compare n (iAtom (C.head iline)) of
LT -> updateILine' (n + 1) xL iline
EQ -> case x of
Nothing -> updateILine' (n + 1) xL (C.tail iline)
Just i -> if iBool (C.head iline)
then C.cons i (updateILine' (n + 1) xL (C.tail iline))
else C.cons (negLit i) (updateILine' (n + 1) xL (C.tail iline))
-- X-Prop conversions
fromIdxPropForm :: Ord a => IdxPropForm a -> PropForm a
fromIdxPropForm (s, iprop) = tr (nth s) iprop
toIdxPropForm :: Ord a => PropForm a -> IdxPropForm a
toIdxPropForm prop = (s, tr (idx s) prop)
where s = propFormAtoms prop
propFormAtoms :: Ord a => PropForm a -> O.Olist a
propFormAtoms p = case p of
(A a) -> [a]
F -> []
T -> []
(N p) -> propFormAtoms p
(CJ pL) -> O.unionList (map propFormAtoms pL)
(DJ pL) -> O.unionList (map propFormAtoms pL)
(SJ pL) -> O.unionList (map propFormAtoms pL)
(EJ pL) -> O.unionList (map propFormAtoms pL)
-- I-Form conversion
iLIT :: ILit -> PropForm IAtom
iLIT l | l < 0 = N (A (negLit l))
| l > 0 = A l
| otherwise = error "iLIT -- zero literal"
iNLC :: ILine -> PropForm IAtom
iNLC line = CJ (map iLIT (C.toList line))
iNLD :: ILine -> PropForm IAtom
iNLD line = DJ (map iLIT (C.toList line))
iCNF :: IForm -> PropForm IAtom
iCNF form = CJ (map iNLD (C.toList form))
iDNF :: IForm -> PropForm IAtom
iDNF form = DJ (map iNLC (C.toList form))
-- X-Form conversion
xLIT :: Ord a => XLit a -> PropForm a
xLIT (s, l) = fromIdxPropForm (s, iLIT l)
xNLC :: Ord a => XLine a -> PropForm a
xNLC (s, line) = fromIdxPropForm (s, iNLC line)
xNLD :: Ord a => XLine a -> PropForm a
xNLD (s, line) = fromIdxPropForm (s, iNLD line)
xCNF :: Ord a => XForm a -> PropForm a
xCNF (s, form) = fromIdxPropForm (s, iCNF form)
xDNF :: Ord a => XForm a -> PropForm a
xDNF (s, form) = fromIdxPropForm (s, iDNF form)
-- type correctness and type constructors
isIAtom :: Int -> Bool
isIAtom n = n > 0
isILit :: Int -> Bool
isILit n = n /= 0
isILine :: C.Costack Int -> Bool
isILine x = iter (C.toList x)
where iter [] = True
iter [n] = isILit(n)
iter (n1:n2:nL) = isILit(n1) && iAtom(n1) < iAtom(n2) && iter(n2:nL)
isIForm :: C.Costack (C.Costack Int) -> Bool
isIForm x = iter (C.toList x)
where iter [] = True
iter (c:cL) = (isILine c) && iter cL
iLine :: [Int] -> ILine
iLine iL = C.fromList (iter (zeroCheck iL))
where iter [] = []
iter [i] = [i]
iter (j:i:iL) = if (abs j) < (abs i)
then j:(iter (i:iL))
else error ("IForm.iLine -- in literal order " ++ (show j) ++
" is not before " ++ (show i))
zeroCheck [] = []
zeroCheck (i:iL) = if i == 0
then error "Iform.iLine -- there is a 0 in the list"
else i:(zeroCheck iL)
iForm :: [[Int]] -> IForm
iForm iLL = C.fromList (map iLine iLL)
-- literal operations
iAtom :: ILit -> IAtom
iAtom = abs
iBool :: ILit -> Bool
iBool l | l < 0 = False
| l > 0 = True
| l == 0 = error "IForm.iBool -- zero literal integer"
negLit :: ILit -> ILit
negLit = Prelude.negate
-- index lists
lineIndices :: ILine -> O.Olist IAtom
lineIndices line = map iAtom (C.toList line)
formIndices :: IForm -> O.Olist IAtom
formIndices form = O.unionList (C.toList (C.map lineIndices form))
-- syntactic sizes
lineLength :: ILine -> Int
lineLength = C.length
formLength :: IForm -> Int
formLength = C.length
volume :: IForm -> Int
volume form = C.foldr (+) 0 (C.map lineLength form)
-- ordered forms
isOrderedForm :: IForm -> Bool
isOrderedForm form = C.strictSorted form
orderForm :: IForm -> IForm
orderForm form = C.strictSort form
-- the propositional algebra operations
atomForm :: IAtom -> IForm
atomForm atom = C.singleton (C.singleton atom)
botForm :: IForm
botForm = C.empty
topForm :: IForm
topForm = C.singleton C.empty
formJoinForm :: IForm -> IForm -> IForm
formJoinForm form1 form2 = C.append form1 form2
formListJoin :: [IForm] -> IForm
formListJoin formL = C.concat formL
lineMeetLine :: ILine -> ILine -> IForm
lineMeetLine line1 line2 = jrec (line1, line2, C.empty)
where jrec (first, second, third) =
if C.isEmpty first
then C.singleton (C.append third second)
else if C.isEmpty second
then C.singleton (C.append third first)
else case compare (iAtom (C.head first)) (iAtom (C.head second)) of
LT -> jrec (C.tail first, second, C.cocons third (C.head first))
GT -> jrec (first, C.tail second, C.cocons third (C.head second))
EQ -> if (iBool (C.head first)) == (iBool (C.head second))
then jrec (C.tail first, C.tail second, C.cocons third (C.head first))
else C.empty
lineMeetForm :: ILine -> IForm -> IForm
lineMeetForm line form = formListJoin (map (lineMeetLine line) (C.toList form))
formMeetForm :: IForm -> IForm -> IForm
formMeetForm form1 form2 = formListJoin (map (\ line -> lineMeetForm line form2) (C.toList form1))
formListMeet :: [IForm] -> IForm
formListMeet [] = C.singleton C.empty
formListMeet [form] = form
formListMeet (form1:form2:formL) = formListMeet ((formMeetForm form1 form2) : formL)
dualLine :: ILine -> IForm
dualLine line = C.map C.singleton line
dualForm :: IForm -> IForm
dualForm form = formListMeet (map dualLine (C.toList form))
invertLine :: ILine -> ILine
invertLine = C.map negLit
invertForm :: IForm -> IForm
invertForm = C.map invertLine
negLine :: ILine -> IForm
negLine line = C.map (\ l -> (C.singleton (negLit l))) line
negForm :: IForm -> IForm
negForm form = formListMeet (map negLine (C.toList form))
formCojoinLine :: IForm -> ILine -> IForm
formCojoinLine form line = formJoinForm form (dualLine line)
formCojoinForm :: IForm -> IForm -> IForm
formCojoinForm form1 form2 = formListMeet (C.toList (C.map (formCojoinLine form1) form2))
formAntijoinLine :: IForm -> ILine -> IForm
formAntijoinLine form line = formJoinForm form (negLine line)
formAntijoinForm :: IForm -> IForm -> IForm
formAntijoinForm form1 form2 = formListMeet (C.toList (C.map (formAntijoinLine form1) form2))
elimLine :: ILine -> O.Olist IAtom -> ILine
elimLine line aL | C.isEmpty line = C.empty
| O.isEmpty aL = line
| otherwise = case compare (iAtom (C.head line)) (head aL) of
LT -> C.cons (C.head line) (elimLine (C.tail line) aL)
GT -> elimLine line (tail aL)
EQ -> elimLine (C.tail line) (tail aL)
elimForm :: IForm -> O.Olist IAtom -> IForm
elimForm form aL = C.map (\ line -> (elimLine line aL)) form
lineCovLine :: ILine -> ILine -> Bool
lineCovLine line1 line2 | C.isEmpty line2 = True
| C.isEmpty line1 = False
| otherwise = case compare (iAtom (C.head line1)) (iAtom (C.head line2)) of
LT -> lineCovLine (C.tail line1) line2
GT -> False
EQ -> if (iBool (C.head line1)) == (iBool (C.head line2))
then lineCovLine (C.tail line1) (C.tail line2)
else False
lineCovForm :: ILine -> IForm -> Bool
lineCovForm line form = if C.isEmpty form
then False
else if lineCovLine line (C.head form)
then True
else lineCovForm line (C.tail form)
formCovForm :: IForm -> IForm -> Bool
formCovForm form1 form2 = if C.isEmpty form1
then True
else if lineCovForm (C.head form1) form2
then formCovForm (C.tail form1) form2
else False
-- Generation of the prime and minimal form of two lines
pairPartition :: ILine -> ILine -> (ILine,ILine,ILine,ILine)
pairPartition line1 line2 = iter (C.empty, C.empty, C.empty, C.empty, line1, line2)
where iter :: (ILine,ILine,ILine,ILine,ILine,ILine) -> (ILine,ILine,ILine,ILine)
iter (piL, rhoL, sigmaL, tauL, line1, line2) =
if C.isEmpty line1
then (piL, rhoL, sigmaL, C.append tauL line2)
else if C.isEmpty line2
then (piL, rhoL, C.append sigmaL line1, tauL)
else case compare (iAtom (C.head line1)) (iAtom (C.head line2)) of
LT -> iter (piL, rhoL, C.cocons sigmaL (C.head line1), tauL, C.tail line1, line2)
GT -> iter (piL, rhoL, sigmaL, C.cocons tauL (C.head line2), line1, C.tail line2)
EQ -> if iBool (C.head line1) == iBool (C.head line2)
then iter (C.cocons piL (C.head line1), rhoL, sigmaL, tauL, C.tail line1, C.tail line2)
else iter (piL, C.cocons rhoL (C.head line1), sigmaL, tauL, C.tail line1, C.tail line2)
data CaseSymbol = NOOO | NOOP | NOPO | NOPP | NIOO | NIOP | NIPO | NIPP | NMNN
deriving (Show, Read, Eq, Ord)
caseSymbol :: ILine -> ILine -> CaseSymbol
caseSymbol left right
| p >= 0 && r == 0 && s == 0 && t == 0 = NOOO
| p >= 0 && r == 0 && s == 0 && t >= 1 = NOOP
| p >= 0 && r == 0 && s >= 1 && t == 0 = NOPO
| p >= 0 && r == 0 && s >= 1 && t >= 1 = NOPP
| p >= 0 && r == 1 && s == 0 && t == 0 = NIOO
| p >= 0 && r == 1 && s == 0 && t >= 1 = NIOP
| p >= 0 && r == 1 && s >= 1 && t == 0 = NIPO
| p >= 0 && r == 1 && s >= 1 && t >= 1 = NIPP
| p >= 0 && r >= 2 && s >= 0 && t >= 0 = NMNN
where (piL, rhoL, sigmaL, tauL) = pairPartition left right
(p,r,s,t) = (C.length piL, C.length rhoL, C.length sigmaL, C.length tauL)
-- First version
pairPrim' :: ILine -> ILine -> IForm
pairPrim' left right
| p >= 0 && r == 0 && s == 0 && t == 0 = C.singleton left
| p >= 0 && r == 0 && s == 0 && t >= 1 = C.singleton left
| p >= 0 && r == 0 && s >= 1 && t == 0 = C.singleton right
| p >= 0 && r == 0 && s >= 1 && t >= 1 = C.fromList [left,right]
| p >= 0 && r == 1 && s == 0 && t == 0 = C.singleton piL
| p >= 0 && r == 1 && s == 0 && t >= 1 = C.fromList [left, lineMerge piL tauL]
| p >= 0 && r == 1 && s >= 1 && t == 0 = C.fromList [lineMerge piL sigmaL, right]
| p >= 0 && r == 1 && s >= 1 && t >= 1 = C.fromList [left, right, lineMerge piL (lineMerge sigmaL tauL)]
| p >= 0 && r >= 2 && s >= 0 && t >= 0 = C.fromList [left, right]
where (piL, rhoL, sigmaL, tauL) = pairPartition left right
(p,r,s,t) = (C.length piL, C.length rhoL, C.length sigmaL, C.length tauL)
lineMerge line1 line2 | C.isEmpty line1 = line2
| C.isEmpty line2 = line1
| otherwise = case compare (iAtom (C.head line1)) (iAtom (C.head line2)) of
LT -> C.cons (C.head line1) (lineMerge (C.tail line1) line2)
GT -> C.cons (C.head line2) (lineMerge line1 (C.tail line2))
pairMin' :: ILine -> ILine -> IForm
pairMin' left right = C.take 2 (pairPrim' left right)
xprim' :: ILine -> ILine -> (CaseSymbol, IForm)
xprim' left right = (caseSymbol left right, pairPrim' left right)
xmin' :: ILine -> ILine -> (CaseSymbol, IForm)
xmin' left right = (caseSymbol left right, pairMin' left right)
-- Second, fast and final version
xprim :: ILine -> ILine -> (CaseSymbol, IForm)
xprim left right = xprec (C.empty, left, C.empty, right, C.empty, C.empty, C.empty, 0, 0, 0)
where xprec (left, left', right, right', c1, c2, c3, r, s, t)
| r > 1 =
(NMNN, C.fromList [C.append left left', C.append right right'])
| C.isEmpty left' && r == 0 && s == 0 && C.isEmpty right' && t == 0 =
(NOOO, C.singleton left)
| C.isEmpty left' && r == 0 && s == 0 =
(NOOP, C.singleton left)
| C.isEmpty left' && r == 0 && s > 0 && C.isEmpty right' && t == 0 =
(NOPO, C.singleton right)
| C.isEmpty left' && r == 0 && s > 0 =
(NOPP, C.fromList [left, C.append right right'])
| C.isEmpty left' && r == 1 && s == 0 && C.isEmpty right' && t == 0 =
(NIOO, C.singleton c1)
| C.isEmpty left' && r == 1 && s == 0 =
(NIOP, C.fromList [left, C.append c2 right'])
| C.isEmpty left' && r == 1 && s > 0 && C.isEmpty right' && t == 0 =
(NIPO, C.fromList [c1, C.append right right'])
| C.isEmpty left' && r == 1 && s > 0 =
(NIPP, C.fromList [left, C.append right right', C.append c3 right'])
| not (C.isEmpty left') && C.isEmpty right' && r == 0 && t == 0 =
(NOPO, C.singleton right)
| not (C.isEmpty left') && C.isEmpty right' && r == 0 && t > 0 =
(NOPP, C.fromList [C.append left left', right])
| not (C.isEmpty left') && C.isEmpty right' && r == 1 && t == 0 =
(NIPO, C.fromList [C.append c1 left', right])
| not (C.isEmpty left') && C.isEmpty right' && r == 1 && t > 0 =
(NIPP, C.fromList [C.append left left', right, C.append c3 left'])
| not (C.isEmpty left') && not (C.isEmpty right') =
let x = C.head left'
y = C.head right'
in case compare (iAtom x) (iAtom y) of
LT -> xprec (C.cocons left x, C.tail left', right, right',
C.cocons c1 x, c2, C.cocons c3 x, r, s + 1, t)
GT -> xprec (left, left', C.cocons right y, C.tail right',
c1, C.cocons c2 y, C.cocons c3 y, r, s, t + 1)
EQ -> if iBool x == iBool y
then xprec (C.cocons left x, C.tail left', C.cocons right y, C.tail right',
C.cocons c1 x, C.cocons c2 y, C.cocons c3 y, r, s, t)
else xprec (C.cocons left x, C.tail left', C.cocons right y, C.tail right',
c1, c2, c3, r + 1, s, t)
{-- old version of xprim
xprim :: ILine -> ILine -> (CaseSymbol, IForm)
xprim left right = xprec (C.empty, left, C.empty, right, C.empty, C.empty, C.empty, 0, 0, 0)
where xprec (left, left', right, right', cboth, cleft, cright, r, s, t) =
if r > 1
then (NMNN, C.fromList [C.append left left', C.append right right'])
else if C.isEmpty left'
then if r == 0
then if s == 0
then if (C.isEmpty right' && t == 0)
then (NOOO, C.singleton left)
else (NOOP, C.singleton left)
else if (C.isEmpty right' && t == 0)
then (NOPO, C.singleton right)
else (NOPP, C.fromList [left, C.append right right'])
else if s == 0
then if (C.isEmpty right' && t == 0)
then (NIOO, C.singleton cboth)
else (NIOP, C.fromList [left, C.append cleft right'])
else if (C.isEmpty right' && t == 0)
then (NIPO, C.fromList [cboth, C.append right right'])
else (NIPP, C.fromList [cboth, C.append right right', C.append cright right'])
else if C.isEmpty right'
then if r == 0
then if t == 0
then (NOPO, C.singleton right)
else (NOPP, C.fromList [C.append left left', right])
else if t == 0
then (NIPO, C.fromList [C.append cboth left', right])
else (NIPP, C.fromList [C.append left left', right, C.append cright left'])
else case compare (iAtom (C.head left')) (iAtom (C.head right')) of
LT -> xprec ( C.cocons left (C.head left'),
C.tail left',
right,
right',
C.cocons cboth (C.head left'),
cleft,
C.cocons cright (C.head left'),
r, s+1, t)
GT -> xprec ( left,
left',
C.cocons right (C.head right'),
C.tail right',
cboth,
C.cocons cleft (C.head right'),
C.cocons cright (C.head right'),
r, s, t+1)
EQ -> if iBool (C.head left') == iBool (C.head right')
then xprec ( C.cocons left (C.head left'),
C.tail left',
C.cocons right (C.head right'),
C.tail right',
C.cocons cboth (C.head left'),
C.cocons cleft (C.head left'),
C.cocons cright (C.head right'),
r, s, t)
else xprec ( C.cocons left (C.head left'),
C.tail left',
C.cocons right (C.head right'),
C.tail right',
cboth, cleft, cright,
r+1, s, t)
--}
xmin :: ILine -> ILine -> (CaseSymbol, IForm)
xmin left right = case xprim left right of
(NIPP, form) -> (NIPP, C.take 2 form)
(symb, form) -> (symb, form)
pairPrim :: ILine -> ILine -> IForm
pairPrim left right = snd (xprim left right)
pairMin :: ILine -> ILine -> IForm
pairMin left right = snd (xmin left right)
-- Pairwise minimality and complementary prime list
isMinimalPair :: ILine -> ILine -> Bool
isMinimalPair left right = [left, right] == C.toList (pairMin' left right)
allPairs :: [a] -> [(a,a)]
allPairs [] = []
allPairs [x] = []
allPairs (x:xL) = (iter x xL) ++ (allPairs xL)
where iter x [] = []
iter x (y:yL) = (x,y):(iter x yL)
isPairwiseMinimal :: IForm -> Bool
isPairwiseMinimal form = Prelude.all isMinPair (allPairs (C.toList form))
where isMinPair (x,y) = isMinimalPair x y
-- C-Primes
cPrime :: ILine -> ILine -> Maybe ILine
cPrime left right = case xprim left right of
(NIPP, form) -> Just (C.head (C.tail (C.tail form)))
(symb, form) -> Nothing
cPrimes :: IForm -> IForm
cPrimes form = C.fromList (concat (map cp (allPairs (C.toList form))))
where cp (left ,right) = case cPrime left right of
Just line -> [line]
Nothing -> []
-- The M-Procedure and functions with pairwise minimal IForm results
mrec :: (IForm,IForm,IForm) -> IForm
mrec (gammaL, muL, muL') =
if C.isEmpty gammaL
then C.append muL muL'
else if C.isEmpty muL'
then mrec (C.tail gammaL, C.empty, C.cons (C.head gammaL) muL)
else case xmin (C.head gammaL) (C.head muL') of
(NOOO, pp) -> mrec (C.tail gammaL, C.empty, C.append muL muL')
(NOOP, pp) -> mrec (C.append (C.tail gammaL) (C.tail muL'), C.empty, C.cons (C.head gammaL) muL)
(NOPO, pp) -> mrec (C.tail gammaL, C.empty, C.append muL muL')
(NOPP, pp) -> mrec (gammaL, C.cocons muL (C.head muL'), C.tail muL')
(NIOO, pp) -> mrec (C.append (C.tail gammaL) pp, C.empty, C.append muL (C.tail muL'))
(NIOP, pp) -> mrec (C.concat [C.tail gammaL, C.tail pp, C.tail muL'], C.empty, C.cons (C.head gammaL) muL)
(NIPO, pp) -> mrec (C.cocons (C.tail gammaL) (C.head pp), C.empty, C.append muL muL')
(NIPP, pp) -> mrec (gammaL, C.cocons muL (C.head muL'), C.tail muL')
(NMNN, pp) -> mrec (gammaL, C.cocons muL (C.head muL'), C.tail muL')
m2form :: IForm -> IForm
m2form form = mrec (form, C.empty, C.empty)
iformJoinM2form :: IForm -> IForm -> IForm
iformJoinM2form iform m2form = mrec (iform, C.empty, m2form)
-- The P-Procedure and functions with prime IForm results
primFormFromOrdM2form :: IForm -> IForm
primFormFromOrdM2form ordM2form =
let ordM2form' = orderForm (iformJoinM2form (cPrimes ordM2form) ordM2form)
in if ordM2form' == ordM2form
then ordM2form'
else primFormFromOrdM2form ordM2form'
primForm :: IForm -> IForm
primForm iform = primFormFromOrdM2form $ orderForm $ m2form iform
iformJoinPrimForm :: IForm -> IForm -> IForm
iformJoinPrimForm iform pform = primFormFromOrdM2form $ orderForm $ iformJoinM2form iform pform
{-- the following prec, primform, ordPrimForm are obsolete -----------------------------------------------------------
prec :: (IForm, IForm, IForm, IForm) -> IForm
prec (gammaL, muL, muL', piL)
| C.isEmpty gammaL && C.isEmpty piL =
C.append muL muL'
| C.isEmpty gammaL =
prec (piL, C.empty, C.append muL muL', C.empty)
| C.isEmpty muL' =
prec (C.append (C.tail gammaL) piL, C.empty, C.cons (C.head gammaL) muL, C.empty)
| otherwise =
case xprim (C.head gammaL) (C.head muL') of
(NOOO, pp) -> prec (C.tail gammaL, C.empty, C.append muL muL', C.empty)
(NOOP, pp) -> prec (C.concat [C.tail gammaL, C.tail muL', piL], C.empty, C.cons (C.head gammaL) muL, C.empty)
(NOPO, pp) -> prec (C.tail gammaL, C.empty, C.append muL muL', C.empty)
(NOPP, pp) -> prec (gammaL, C.cocons muL (C.head muL'), C.tail muL', piL)
(NIOO, pp) -> prec (C.append (C.tail gammaL) pp, C.empty, C.append muL (C.tail muL'), C.empty)
(NIOP, pp) -> prec (C.concat [C.tail gammaL, C.tail pp, C.tail muL', piL], C.empty, C.cons (C.head gammaL) muL, C.empty)
(NIPO, pp) -> prec (C.cocons (C.tail gammaL) (C.head pp), C.empty, C.append muL muL', C.empty)
(NIPP, pp) -> prec (gammaL, C.cocons muL (C.head muL'), C.tail muL', C.append (C.tail (C.tail pp)) piL)
(NMNN, pp) -> prec (gammaL, C.cocons muL (C.head muL'), C.tail muL', piL)
-- OLD VERSION --------
prec :: (IForm, IForm, IForm, IForm) -> IForm
prec (gammaL, muL, muL', piL) =
if C.isEmpty gammaL
then if C.isEmpty piL
then C.append muL muL'
else prec (piL, C.empty, C.append muL muL', C.empty)
else if C.isEmpty muL'
then prec (C.append (C.tail gammaL) piL, C.empty, C.cons (C.head gammaL) muL, C.empty)
else case xprim (C.head gammaL) (C.head muL') of
(NOOO, pp) ->
prec (C.tail gammaL, C.empty, C.append muL muL', C.empty)
(NOOP, pp) ->
prec (C.concat [C.tail gammaL, C.tail muL', piL], C.empty, C.cons (C.head gammaL) muL, C.empty)
(NOPO, pp) ->
prec (C.tail gammaL, C.empty, C.append muL muL', C.empty)
(NOPP, pp) ->
prec (gammaL, C.cocons muL (C.head muL'), C.tail muL', piL)
(NIOO, pp) ->
-- old version: --!!
-- prec (C.cocons (C.tail gammaL) (C.head pp), C.empty, C.append muL muL', C.empty)
prec (C.cocons (C.tail gammaL) (C.head pp), C.empty, C.append muL (C.tail muL'), C.empty)
(NIOP, pp) ->
prec (C.concat [C.tail gammaL, C.tail pp, C.tail muL', piL], C.empty, C.cons (C.head gammaL) muL, C.empty)
(NIPO, pp) ->
prec (C.cocons (C.tail gammaL) (C.head pp), C.empty, C.append muL muL', C.empty)
(NIPP, pp) ->
prec (gammaL, C.cocons muL (C.head muL'), C.tail muL', C.append (C.tail (C.tail pp)) piL)
(NMNN, pp) ->
prec (gammaL, C.cocons muL (C.head muL'), C.tail muL', piL)
primForm :: IForm -> IForm
primForm form = prec (form, C.empty, C.empty, C.empty)
ordPrimForm :: IForm -> IForm
ordPrimForm = orderForm . primForm
------------------------------------------------------------------------------------------------------------------}
-- XForm operations
xformAtoms :: Ord a => XForm a -> O.Olist a
xformAtoms (aL,iform) = aL
xformRedAtoms :: Ord a => XForm a -> O.Olist a
xformRedAtoms xform = O.difference (xformAtoms xform) (xformIrrAtoms xform)
xformIrrAtoms :: Ord a => XForm a -> O.Olist a
xformIrrAtoms (aL, iform) = iter aL 1 (formIndices iform)
where iter aL n [] = []
iter (a:aL) n (i:iL) = case compare n i of
EQ -> a : (iter aL (n + 1) iL)
LT -> iter aL (n + 1) (i:iL)
-- The XPDNF algebra
instance Ord a => PropAlg a (XPDNF a) where
at x = XPDNF ([x], atomForm 1)
false = XPDNF ([], botForm)
true = XPDNF ([], topForm)
neg (XPDNF (aL, iform)) = XPDNF (aL, primForm (negForm iform))
conj pL = XPDNF (aL, primForm (formListMeet iformL))
where (aL, iformL) = unifyXForms (map (\ (XPDNF xform) -> xform) pL)
disj pL = XPDNF (aL, primForm (formListJoin iformL))
where (aL, iformL) = unifyXForms (map (\ (XPDNF xform) -> xform) pL)
subj pL = XPDNF (aL, primForm (subj' iformL))
where (aL, iformL) = unifyXForms (map (\ (XPDNF xform) -> xform) pL)
subj' [] = topForm
subj' [iform] = topForm
subj' (iform1:iform2:iformL) = formMeetForm (formJoinForm (negForm iform1) iform2) (subj' (iform2:iformL))
equij pL = XPDNF (aL, primForm (iform))
where (aL, iformL) = unifyXForms (map (\ (XPDNF xform) -> xform) pL)
iform = formJoinForm (formListMeet iformL) (negForm (formListJoin iformL))
valid (XPDNF (aL, iform)) = iform == topForm
satisfiable (XPDNF (aL, iform)) = iform /= botForm
subvalent (XPDNF xform1) (XPDNF xform2) = formCovForm iform1 iform2
where (aL, [iform1, iform2]) = unifyXForms [xform1, xform2]
equivalent = (==)
covalent p1 p2 = satisfiable (conj [p1, p2])
properSubvalent p1 p2 = p1 /= p2 && subvalent p1 p2
properDisvalent p1 p2 = satisfiable p1 && satisfiable p2 && disvalent p1 p2
atoms (XPDNF xform) = xformAtoms xform
redAtoms (XPDNF xform) = xformRedAtoms xform
irrAtoms (XPDNF xform) = xformIrrAtoms xform
ext (XPDNF (xL, iform)) yL = XPDNF (yL', primForm iform')
where (yL', iform') = newAtomsXForm (xL, iform) (O.union xL (O.olist yL))
infRed (XPDNF (xL, iform)) yL = XPDNF (yL', iform''')
where iform' = primForm (dualForm iform)
(yL', iform'') = newAtomsXForm (xL, iform') (O.olist yL)
iform''' = primForm (dualForm iform'')
supRed (XPDNF xform) yL = XPDNF (yL', primForm iform')
where (yL', iform') = newAtomsXForm xform (O.olist yL)
infElim (XPDNF (xL, iform)) yL = infRed (XPDNF (xL, iform)) (O.difference xL (O.olist yL))
supElim (XPDNF (xL, iform)) yL = supRed (XPDNF (xL, iform)) (O.difference xL (O.olist yL))
toPropForm = fromXPDNF
fromPropForm = toXPDNF
instance Ord a => PropAlg a (XPCNF a) where
at x = XPCNF ([x], atomForm 1)
false = XPCNF ([], topForm)
true = XPCNF ([], botForm)
neg (XPCNF (aL, iform)) = XPCNF (aL, primForm (negForm iform))
conj pL = XPCNF (aL, primForm (formListJoin iformL))
where (aL, iformL) = unifyXForms (map (\ (XPCNF xform) -> xform) pL)
disj pL = XPCNF (aL, primForm (formListMeet iformL))
where (aL, iformL) = unifyXForms (map (\ (XPCNF xform) -> xform) pL)
subj pL = XPCNF (aL, primForm (subj' iformL))
where (aL, iformL) = unifyXForms (map (\ (XPCNF xform) -> xform) pL)
subj' [] = botForm
subj' [iform] = botForm
subj' (iform1:iform2:iformL) = formJoinForm (formMeetForm (negForm iform1) iform2) (subj' (iform2:iformL))
equij pL = XPCNF (aL, primForm (iform))
where (aL, iformL) = unifyXForms (map (\ (XPCNF xform) -> xform) pL)
iform = formMeetForm (formListJoin iformL) (negForm (formListMeet iformL))
valid (XPCNF (aL, iform)) = iform == botForm
satisfiable (XPCNF (aL, iform)) = iform /= topForm
subvalent (XPCNF xform1) (XPCNF xform2) = formCovForm iform2 iform1
where (aL, [iform1, iform2]) = unifyXForms [xform1, xform2]
equivalent = (==)
covalent p1 p2 = satisfiable (conj [p1, p2])
properSubvalent p1 p2 = p1 /= p2 && subvalent p1 p2
properDisvalent p1 p2 = satisfiable p1 && satisfiable p2 && disvalent p1 p2
atoms (XPCNF xform) = xformAtoms xform
redAtoms (XPCNF xform) = xformRedAtoms xform
irrAtoms (XPCNF xform) = xformIrrAtoms xform
ext (XPCNF (xL, iform)) yL = XPCNF (yL', primForm iform')
where (yL', iform') = newAtomsXForm (xL, iform) (O.union xL (O.olist yL))
infRed (XPCNF xform) yL = XPCNF (yL', primForm iform')
where (yL', iform') = newAtomsXForm xform (O.olist yL)
supRed (XPCNF (xL, iform)) yL = XPCNF (yL', iform''')
where iform' = primForm (dualForm iform)
(yL', iform'') = newAtomsXForm (xL, iform') (O.olist yL)
iform''' = primForm (dualForm iform'')
infElim (XPCNF (xL, iform)) yL = infRed (XPCNF (xL, iform)) (O.difference xL (O.olist yL))
supElim (XPCNF (xL, iform)) yL = supRed (XPCNF (xL, iform)) (O.difference xL (O.olist yL))
toPropForm = fromXPCNF
fromPropForm = toXPCNF
dualizeXPDNF :: Ord a => XPDNF a -> XPCNF a
dualizeXPDNF (XPDNF (aL, iform)) = XPCNF (aL, primForm (dualForm iform))
dualizeXPCNF :: Ord a => XPCNF a -> XPDNF a
dualizeXPCNF (XPCNF (aL, iform)) = XPDNF (aL, primForm (dualForm iform))
-- The MixForm algebra
instance Ord a => PropAlg a (MixForm a) where
at x = PDNF ([x], atomForm 1) -- alernatively = PCNF ([x], atomForm 1)
false = PDNF ([], botForm)
true = PCNF ([], botForm)
neg (M2DNF (aL, iform)) = M2CNF (aL, invertForm iform)
neg (M2CNF (aL, iform)) = M2DNF (aL, invertForm iform)
neg (PDNF (aL, iform)) = PCNF (aL, invertForm iform)
neg (PCNF (aL, iform)) = PDNF (aL, invertForm iform)
conj [] = true
conj [form] = form
conj formL = M2CNF (aL, m2form (formListJoin iformL))
where (aL,iformL) = unifyXForms cnfL
cnfL = map cnf formL
cnf (M2CNF (aL,iform)) = (aL, iform)
cnf (M2DNF (aL,iform)) = (aL, dualForm iform)
cnf (PCNF (aL,iform)) = (aL, iform)
cnf (PDNF (aL,iform)) = (aL, dualForm iform)
disj [] = false
disj [form] = form
disj formL = M2DNF (aL, m2form (formListJoin iformL))
where (aL,iformL) = unifyXForms dnfL
dnfL = map dnf formL
dnf (M2CNF (aL,iform)) = (aL, dualForm iform)
dnf (M2DNF (aL,iform)) = (aL, iform)
dnf (PCNF (aL,iform)) = (aL, dualForm iform)
dnf (PDNF (aL,iform)) = (aL, iform)
subj [] = true
subj [form] = PCNF (atoms form, botForm)
subj formL = fromPropForm (SJ (map toPropForm formL))
equij [] = true
equij [form] = PCNF (atoms form, botForm)
equij formL = fromPropForm (EJ (map toPropForm formL))
valid (M2DNF (aL,iform)) = primForm iform == topForm
valid (M2CNF (aL,iform)) = iform == botForm
valid (PDNF (aL,iform)) = iform == topForm
valid (PCNF (aL,iform)) = iform == botForm
satisfiable (M2DNF (aL,iform)) = iform /= botForm
satisfiable (M2CNF (aL,iform)) = primForm iform /= topForm
satisfiable (PDNF (aL,iform)) = iform /= botForm
satisfiable (PCNF (aL,iform)) = iform /= topForm
subvalent form1 form2 = valid (subj [form1, form2])
equivalent form1 form2 = valid (equij [form1, form2])
covalent form1 form2 = satisfiable (conj [form1, form2])
properSubvalent form1 form2 = subvalent form1 form2 && not (equivalent form1 form2)
properDisvalent form1 form2 = disvalent form1 form2 && satisfiable form1 && satisfiable form2
atoms (M2DNF (aL,iform)) = aL
atoms (M2CNF (aL,iform)) = aL
atoms (PDNF (aL,iform)) = aL
atoms (PCNF (aL,iform)) = aL
redAtoms (M2DNF (aL,iform)) = xformRedAtoms (aL, primForm iform)
redAtoms (M2CNF (aL,iform)) = xformRedAtoms (aL, primForm iform)
redAtoms (PDNF xform) = xformRedAtoms xform
redAtoms (PCNF xform) = xformRedAtoms xform
irrAtoms (M2DNF (aL,iform)) = xformIrrAtoms (aL, primForm iform)
irrAtoms (M2CNF (aL,iform)) = xformIrrAtoms (aL, primForm iform)
irrAtoms (PDNF xform) = xformIrrAtoms xform
irrAtoms (PCNF xform) = xformIrrAtoms xform
ext (M2DNF xform) aL = M2DNF (newAtomsXForm xform aL)
ext (M2CNF xform) aL = M2CNF (newAtomsXForm xform aL)
ext (PDNF xform) aL = PDNF (newAtomsXForm xform aL)
ext (PCNF xform) aL = PCNF (newAtomsXForm xform aL)
infRed form yL = M2CNF (yL', m2form iform')
where (PCNF (xL, iform)) = mixToPCNF form
(yL',iform') = newAtomsXForm (xL, iform) (O.olist yL)
supRed form yL = M2DNF (yL', m2form iform')
where (PDNF (xL, iform)) = mixToPDNF form
(yL',iform') = newAtomsXForm (xL, iform) (O.olist yL)
infElim form yL = infRed form (O.difference (atoms form) (O.olist yL))
supElim form yL = supRed form (O.difference (atoms form) (O.olist yL))
toPropForm = fromMixForm
fromPropForm = toM2DNF -- alternatively: toM2CNF
mixToPDNF :: Ord a => MixForm a -> MixForm a
mixToPDNF (M2DNF (aL, iform)) = PDNF (aL, primForm iform)
mixToPDNF (M2CNF (aL, iform)) = PDNF (aL, primForm (dualForm iform))
mixToPDNF (PDNF xform) = PDNF xform
mixToPDNF (PCNF (aL, iform)) = PDNF (aL, primForm (dualForm iform))
mixToPCNF :: Ord a => MixForm a -> MixForm a
mixToPCNF (M2DNF (aL, iform)) = PCNF (aL, primForm (dualForm iform))
mixToPCNF (M2CNF (aL, iform)) = PCNF (aL, primForm iform)
mixToPCNF (PDNF (aL, iform)) = PCNF (aL, primForm (dualForm iform))
mixToPCNF (PCNF xform) = PCNF xform