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

我尝试创建一个用于处理逻辑表达式的数据结构。乍一看，逻辑表达式看起来像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的数据结构，但没有左右“分支”。

最佳答案

我们将遵循丹尼尔·瓦格纳(Daniel Wagner)的出色建议，并使用“幼稚的表示形式(您的第一个表示形式)，以及选择一种著名的正常形式的函数”。我们将使用algebraic normal form有两个原因。主要原因是代数范式不需要枚举Property中保存的变量类型的所有可能值。代数范式也相当简单。

代数范式

我们将使用不导出其构造函数的newtype ANF a = ANF [[a]]表示代数范式。每个内部列表都是其所有谓词的连接(与)。如果内部列表为空，则始终为true。外部列表是所有谓词的异或。如果为空，则为假。

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

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

我们将努力使我们构造的任何ANF都规范。我们将构建ANF，以便内部列表始终被排序和唯一。外部列表也将始终进行排序。如果外部列表中有两个(或偶数个)相同的项目，我们将同时删除它们。如果外部列表中奇数个相同项目，我们将除去其中所有项目。

使用 Data.List.Ordered 包中data-ordlist中的函数，我们可以清理一个列表，该列表表示将连接词异化为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

逻辑表达式形成boolean algebra，它是一个有附加分配律和补码(负数)的有界晶格。利用 BoundedLattice 包中现有的lattices类，我们可以定义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 a具有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])

使用De Morgan's laws，可以按照join或逻辑or编写meet或逻辑and。

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

晶格的top始终为true。

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

晶格的bottom始终为false。

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 ing完成。

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实例只是结构上的相等。
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和Boolean函数都具有ANF a的表示形式。令k为a的居民人数。 2^(2^k)布尔变量有k可能的布尔函数。 ANF的每个内部列表都是a的集合；存在2^k可能的a组，因此也可能存在2^k的内部列表。 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']是127，而foldr join bottom . map point $ ['a'..'g']包含448出现的7不同变量的总数。

关于haskell - Haskell中逻辑表达式的数据结构，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/28286694/