Общие преобразования на множестве данного типа данных

Question

Если у меня есть тип данных, представляющий подмножество логики высказываний, таких как

data Prop = Lit String
          | Neg Prop
          | And Prop Prop
          | Or Prop Prop

Есть ли тогда простые способы сделать общие преобразования на [[Prop]]? Например

• замещать [[And a b, c]] с [[a, b, c]]
• замещать [[Or a b, c]] с [[a], [b], [c]], или же
• удаление вхождений подсписков, содержащих как Neg a а также aнапример поворот [[Neg a, x, a], [b]] в [[b]]

Это похоже на то, что, например, делает uniplate, но "на два уровня выше".

Answer 1

Я предполагаю, что ваше второе правило неверно, и вы действительно хотели сказать либо:

• замещать [[Or a b],[c]] с [[a],[b],[c]]

или еще:

• замещать [[Or a b, c]] с [[a,c],[b,c]]

Другими словами, я предполагаю, что вы пытаетесь преобразовать Prop в альтернативное представление [[Prop]] где список первого уровня представляет собой "или", а список второго уровня - "и", причем все термины являются литералами или Neg-literals. Итак, вы пытаетесь представить, как можно применить набор общих структурных правил для таких преобразований, как:

[[And a (Or b c)]]
[[a, Or b c]]        -- apply "And" rule
[[a,b],[a,c]]        -- apply some kind of "Or" distribution rule

Если это так, то использование общих преобразований не очень полезно. С вашим текущим типом данных вы можете в любом случае применить эти преобразования только к выражениям верхнего уровня. Например, нет очевидного способа применить Or Править здесь:

[[And a (And b (Or c d))]]

без первого применения And правила пару раз. Если вы измените свой тип данных, добавив, скажем, L2 [[Prop]] конструктор, так что вы можете преобразовать вышеприведенное выражение в:

[[And a (And b (L2 [[c],[d]]))]]   -- apply "Or" rule

непонятно что это тебя покупает.

В конечном счете, я не думаю, что это правильный подход...

У вас есть совершенно адекватное представление вашей логики высказываний в Prop тип данных; и у вас есть желаемое окончательное представление. Вместо того, чтобы пытаться перевести ваш Prop представление в окончательное представление, используя частичные общие преобразования, преобразуйте Prop представление с использованием стандартных рекурсивных преобразований Prop-to-Prop в каноническое Prop Форма и сделать перевод в качестве последнего шага.

Здесь разумная каноническая форма:

Or e1 (Or e2 (... (Or e3 e4)))

где каждый ek имеет форму:

And t1 (And t2 (... (And t3 t4)))

и каждый tk это либо Lit _ или Neg (Lit _), Очевидно, что эту каноническую форму можно довольно легко перевести в желаемое окончательное представление в виде [[Prop]],

Я включил возможное решение ниже. Я не вижу такой большой возможности для упрощения вещей с помощью общих преобразований. Большая часть сопоставления с образцом, кажется, делает нетривиальную работу.

Возможное решение

После небольшой преамбулы:

import Data.List

data Prop = Lit String
          | Neg Prop
          | And Prop Prop
          | Or Prop Prop
          deriving (Eq)

тогда один способ перевести произвольный Prop в эту каноническую форму, чтобы сначала подтолкнуть все Negдо буквальных терминов:

pushNeg :: Prop -> Prop
pushNeg = push False
  where
    -- de Morgan's laws
    push neg (And x y) = (if neg then Or else And) (push neg x) (push neg y)
    push neg (Or x y)  = (if neg then And else Or) (push neg x) (push neg y)
    -- handle Neg and Lit
    push neg (Neg y) = push (not neg) y
    push neg (Lit l) = if neg then Neg (Lit l) else Lit l

затем нажмите все Andна них сверху. Это сложнее понять, но я думаю, что следующее правильно, хотя в некоторых случаях это делает немного ненужной работы:

pushAnd :: Prop -> Prop
pushAnd (Or x y) = Or (pushAnd x) (pushAnd y)
pushAnd (And x y)
  = let x' = pushAnd x
    in  case x' of
          Or u v -> Or (pushAnd (And u y)) (pushAnd (And v y))
          _ -> let y' = pushAnd y
               in case y' of
                    Or u v -> Or (pushAnd (And x' u)) (pushAnd (And x' v))
                    _ -> And x' y'
pushAnd x = x

а затем рекурсивно сделать все And а также Or пункты правоассоциативные:

rassoc :: Prop -> Prop
rassoc (Or (Or x y) z)   = rassoc (Or x (Or y z))
rassoc (Or x        z)   = Or (rassoc x) (rassoc z)
rassoc (And (And x y) z) = rassoc (And x (And y z))
rassoc (And x         z) = And x (rassoc z)
rassoc x = x

и, наконец, преобразуем каноническую форму в ее окончательное представление (отбрасывая несовместимые предложения и дублирующиеся термины, пока мы на нем):

translate :: Prop -> [[Prop]]
translate = nub . map nub . filter consistent . doOr
  where
    doOr x = case x of
      Or x y -> doAnd x : doOr y
      x      -> doAnd x : []
    doAnd x = case x of
      And x y -> x : doAnd y
      x       -> x : []
    consistent lits =
      let (falses, trues) = partition isNeg lits
          falses' = map (\(Neg (Lit l)) -> l) falses
          trues'  = map (\     (Lit l)  -> l) trues
      in null (intersect falses' trues')
    isNeg (Neg x) = True
    isNeg _       = False

Весь трубопровод это:

final :: Prop -> [[Prop]]
final = translate . rassoc . pushAnd . pushNeg

и вот некоторый тестовый код:

a = Lit "a"
b = Lit "b"
c = Lit "c"
d = Lit "d"
e = Lit "e"

-- Show instance, but only for `final` forms
instance Show Prop where
  show (Lit x) = x
  show (Neg (Lit x)) = '~':x

main :: IO ()
main = do print $ final (Neg a)
          print $ final (Or a b)
          print $ final (Or a a)
          print $ final (And a b)
          print $ final (And (Or (And (Or a b) c) d) e)
          print $ final (And (Or (Or a b) c) (Neg (And a (Or b d))))

какие выводы:

[[~a]]
[[a],[b]]
[[a]]
[[a,b]]
[[a,c,e],[b,c,e],[d,e]]
[[a,~b,~d],[b,~a],[c,~a],[c,~b,~d]]

Есть еще некоторая возможность для дальнейшего упрощения, как:

final (And a (Or a b))

дает окончательный вид [[a],[a,b]] вместо просто [[a]],