Структура данных для логических выражений в Haskell

Мы собираемся следовать прекрасному предложению Даниэля Вагнера и использовать «наивное представление (ваше первое) плюс функцию, которая выбирает одну из известных нормальных форм». Мы собираемся использовать алгебраическую нормальную форму по двум причинам. Основная причина в том, что алгебраическая нормальная форма не требует перечисления всех возможных значений типа переменной, хранящихся в Property. Алгебраическая нормальная форма также довольно проста.

Алгебраическая нормальная форма

Мы будем представлять алгебраическую нормальную форму с помощью newtype ANF a = ANF [[a]], который не экспортирует свой конструктор. Каждый внутренний список является конъюнкцией (и) всех своих предикатов; если внутренний список пуст, он всегда истинен. Внешний список является операцией исключающего ИЛИ всех его предикатов; если оно пустое, оно ложно.

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

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

Мы приложим усилия, чтобы любое построенное нами ANF было каноническим. Мы построим ANFs так, чтобы внутренний список всегда был отсортирован и уникален. Внешний список также всегда будет отсортирован. Если во внешнем списке есть два (или четное количество) одинаковых элементов, мы удалим их оба. Если во внешнем списке нечетное количество одинаковых элементов, мы удалим все, кроме одного.

Использование функций из Data.List.Ordered в пакет data-ordlist, мы можем очистить список списков, представляющих 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 в пакете lattices мы можем определить класс BooleanAlgebras

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])

Используя законы Де Моргана, 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 — это отрицание, которое может быть выполнено с помощью xoring со значением true.

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, имеет представление в ANF a. Пусть k будет количеством жителей a. Существует 2^(2^k) возможных логических функций для k логических переменных. Каждый внутренний список ANF представляет собой набор as; существует 2^k возможных наборов as и, таким образом, 2^k возможных внутренних списков. Внешний список ANF представляет собой набор внутренних списков; каждый внутренний список может встречаться во внешнем списке не более одного раза. Есть 2^(2^k) возможных ANF as. Поскольку каждая булева функция имеет представление в 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 различных переменных.

Я бы рекомендовал использовать решатель SAT/SMT для проверки эквивалентности. В общем, такого рода проверки могут быть очень дорогими (NP-полными), и любой вид перевода в нормальные формы может привести к экспоненциальному взрыву в представлении. Решатели SAT/SMT имеют специальные алгоритмы для решения таких проблем, и лучше всего использовать такой решатель. Было бы тривиально перевести два экземпляра Property и спросить, одинаковы ли они при всех назначениях переменных. Можно использовать библиотеку SBV (https://hackage.haskell.org/package/sbv). делать перевод с высокоуровневого Haskell. В ответе на следующий вопрос есть некоторые подробности о том, как это сделать: generate-a-predicate-from-a-parsed">Решение SAT с библиотекой haskell SBV: как сгенерировать предикат из проанализированной строки?

Если вы хотите отразить ассоциативность логических связок и (&&) и или, используйте ассоциативную структуру данных, например список:

data Property a = And [Property a] | ...

Если вам также нужна коммутативность (A && B == B && A), используйте Data.Set.

Я помню эту удобную диаграмму для того, какие типы использовать, если вам нужны определенные свойства:

+-----------+-----------+----------+----------
|Associative|Commutative|Idempotent|   type
+-----------+-----------+----------+----------
|(a+b)+c=   |  a+b=b+a  |  a+a=a   |
|    a+(b+c)|           |          |
+-----------+-----------+----------+----------
|    no     |    no     |    no    |binary trees
|    no     |   yes     |    no    | “mobiles”
|   yes     |    no     |    no    |lists (arrays)
|   yes     |   yes     |    no    |multisets (bags)
|   yes     |   yes     |   yes    |sets
+-----------+-----------+----------+----------

Страница 51 лекции Гая Стила.