Haskell中逻辑表达式的数据结构

Question

我尝试创建一个用于处理逻辑表达式的数据结构.乍一看,逻辑表达式看起来像Trees,所以从树上组成它似乎是合理的:

data Property a = And (Property a) (Property a) |
                 Or  (Property a) (Property a) |
                 Not (Property a) | Property a   deriving (Show,Eq)

但这不是一个好主意,因为我的树的左右分支之间确实没有区别,因为 A && B == B && A

好吧,也许List更好？

data Property a = Empty | And a (Property a) | Or a (Property a) | Not a (Property a)  deriving Show

但在这种情况下,我无法形成一个"逻辑树",只能形成一个"逻辑列表".所以我需要一个类似Tree但没有左右"分支" 的数据结构.

Answer 1

我们将遵循Daniel Wagner的出色建议并使用"天真的表现形式(你的第一个),以及一个选择其中一个着名的正常形式的功能".我们将使用代数正规形式有两个原因.主要原因是代数范式不需要枚举a中保存的变量类型的所有可能值Property.代数正规形式也相当简单.

代数范式

我们将代表一个newtype ANF a = ANF [[a]]不导出其构造函数的代数正规形式.每个内部列表都是其所有谓词的连接(和); 如果内部列表为空,则始终为真.外部列表是其所有谓词的独占或排序; 如果是空的则是假的.

module Logic (
    ANF (getANF),
    anf,
    ...
)

newtype ANF a = ANF {getANF :: [[a]]}
  deriving (Eq, Ord, Show)

我们将努力使任何ANF我们构建的都是规范的.我们将构建ANFs,以便内部列表始终排序和唯一.外部列表也将始终排序.如果外部列表中有两个(或偶数个)相同的项目,我们将删除它们.如果外部列表中存在奇数个相同的项目,我们将删除除其中一个之外的所有项目.

使用data-ordlist包Data.List.Ordered中的函数,我们可以清理表示连词xor-ing 的列表列表,其中列表已排序并且已删除重复项.ANF

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

逻辑表达式形成一个布尔代数,它是一个带有额外分配律和补充(否定)的有界点.利用格子包中的现有BoundedLattice类,我们可以定义s 的类BooleanAlgebra

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 as形成一个BooleanAlgebra只要a有一个Ord实例,以便我们可以保持ANF规范的形式.

的meet一个布尔代数的是合乎逻辑的and.逻辑and分布xor.我们将利用内部列表已经排序以快速将它们合并在一起的事实.

instance (Ord a) => MeetSemiLattice (ANF a) where
    ANF xs `meet` ANF ys = ANF (nubPairs [Ordered.union x y | x <- xs, y <- ys])

使用德摩根定律中,join或逻辑or可以写在条款meet或逻辑and.

instance (Ord a) => JoinSemiLattice (ANF a) where
    xs `join` ys = complement (complement xs `meet` complement ys)

该top格子的始终是真实的.

instance (Ord a) => BoundedMeetSemiLattice (ANF a) where
    top = ANF [[]]

该bottom格子的永远是假的.

instance (Ord a) => BoundedJoinSemiLattice (ANF a) where
    bottom = ANF []

逻辑and和逻辑or满足晶格吸收定律,a join (a meet b) == a meet (a join b) == a.

instance (Ord a) => Lattice (ANF a)
instance (Ord a) => BoundedLattice (ANF a)

最后,complement操作是否定,可以xor通过真实来完成.

instance (Ord a) => BooleanAlgebra (ANF a) where
    complement (ANF ([]:xs)) = ANF xs
    complement (ANF xs)      = ANF ([]:xs)

随着Pointed我们可以使用BooleanAlgebra定义类的持有逻辑表达式的事情,Logical.

import Data.Pointed

class Logical f where
    toLogic :: (Pointed g, BooleanAlgebra (g a)) => f a -> g a

代数范式包含逻辑表达式.

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

代数正规形式也是Pointed,因此可以转换为使用toLogic.

instance Pointed ANF where
    point x = ANF [[x]]

toANF :: (Logical f, Ord a) => f a -> ANF a
toANF = toLogic

我们可以Logical通过比较来判断它是否在逻辑上是等价的,看它在转换为规范代数范式时是否在结构上是等价的.

equivalent :: (Logical f, Logical g, Ord a) => f a -> g a -> Bool
equivalent a b = toANF a == toANF b

将属性转换为ANF

逻辑表达式应该形成一个布尔代数,它是一个带有额外分配律和补充(否定)的有界格.为了使Property布尔代数更加平行,我们需要为格子的边界top和bottom边界添加两个元素.top总是True,bottom永远False.我将把这些称为Trivial总是True和Impossible属性的属性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是属性的抽象语法树.它的派生Eq和Ord实例只是结构上的平等.

A Property是Logical,我们可以把它转换成任何一个Pointed BooleanAlgebra.

instance Logical Property where
    toLogic (And a b)    = (toLogic a) `meet` (toLogic b)
    toLogic (Or  a b)    = (toLogic a) `join` (toLogic b)
    toLogic (Not a)      = complement (toLogic a)
    toLogic (Property a) = point a
    toLogic Trivial      = top
    toLogic Impossible   = bottom

使用equivalent上一节和我们的Logical实例,我们可以检查两个属性是否与某些示例等效.

runExample :: (Ord a, Show a) => Property a -> Property a -> IO ()
runExample p q = 
    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)

这会产生以下输出.

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

要使用这些示例,我们还需要BooleanAlgebra和Pointed实例Property.BooleanAlgebra法律的等价关系是等价的解释而不是结构的平等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

证明

每个布尔函数,因此每个有限Property,都有一个唯一的表示ANF.所述BooleanAlgebra和Pointed实例用于ANF证明一切Logical a,并且因此每一个有限Property a通过索引和布尔函数a,具有在表示ANF a.让我们k的居民数量a.有2^(2^k)可能的布尔函数k布尔变量.a的每个内部列表ANF是一组as; 有2^k可能的as组,因此2^k可能是内部列表.a的外部列表ANF是一组内部列表; 每个内部列表最多可以在外部列表中出现一次.有2^(2^k)可能ANF a秒.由于每个布尔函数都有一个表示,ANF并且只ANF存在与布尔函数一样多的可能居民,因此每个布尔函数都有一个唯一的表示ANF.

放弃

该Ord例如ANF是一个结构性的秩序,除了平等的,无关与晶格结构引起的部分订单.

代数范式可以指数大于其输入.n变量列表的分离具有大小.5*n*2^n.例如,length . getANF . foldr join bottom . map point $ ['a'..'g']is 127和foldr join bottom . map point $ ['a'..'g']包含不同变量的总448出现次数7.