Рекурсивно модифицирующие части структуры данных в Haskell

Question

Привет, ребята. Я новичок в Haskell, я хотел бы создать программу на Haskell, которая могла бы применять законы Деморгана к логическим выражениям. Проблема в том, что я не могу изменить данное выражение на новое (после применения законов Деморгана)

Чтобы быть конкретным, вот моя структура данных

data LogicalExpression = Var Char
        | Neg LogicalExpression
        | Conj LogicalExpression LogicalExpression
        | Disj LogicalExpression LogicalExpression
        | Impli LogicalExpression LogicalExpression
        deriving(Show)

Я хотел бы создать функцию, которая принимает "LogicalExpression" и возвращает "LogicalExpression" после применения законов Деморгана.

Например, когда я нахожу этот шаблон: Neg ( Conj (Var 'a') (Var 'b')) в логическом выражении, мне нужно преобразовать его в Conj ( Neg (Var 'a') Neg (Var 'b')).

Идея проста, но ее трудно реализовать в haskell, это все равно, что пытаться создать функцию (назовем ее Z), которая ищет x и преобразует его в y, поэтому, если Z задан как "vx", он преобразует его в "vy". "только вместо строк он принимает в структуре данных" логическое выражение ", а вместо х он берет шаблон, который я упомянул, и снова выплевывает все логическое выражение, но с измененным шаблоном.

PS: я хочу, чтобы функция принимала любое сложное логическое выражение и упрощала его, используя законы Деморгана.

Есть намеки?

Заранее спасибо.

Answer 1

Люк (Luqui) представил, пожалуй, самый элегантный способ думать о проблеме. Тем не менее, его кодировка требует, чтобы вы вручную получали правильные большие объемы обхода для каждого такого правила перезаписи, которое вы хотите создать.

Композиции Бьорна Брингерта из "Образца для почти составных функций" могут упростить эту задачу, особенно если у вас есть несколько таких проходов нормализации, которые вам нужно написать. Обычно он написан с использованием Applicative или типов ранга 2, но для простоты здесь я отложу это:

Учитывая ваш тип данных

data LogicalExpression
    = Var Char
    | Neg LogicalExpression
    | Conj LogicalExpression LogicalExpression
    | Disj LogicalExpression LogicalExpression
    | Impl LogicalExpression LogicalExpression
deriving (Show)

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

class Compos a where
    compos' :: (a -> a) -> a -> a

instance Compos LogicalExpression where
    compos' f (Neg e)    = Neg (f e)
    compos' f (Conj a b) = Conj (f a) (f b)
    compos' f (Disj a b) = Disj (f a) (f b)
    compos' f (Impl a b) = Impl (f a) (f b)
    compos' _ t = t

Например, мы могли бы устранить все последствия:

elimImpl :: LogicalExpression -> LogicalExpression
elimImpl (Impl a b) = Disj (Not (elimImpl a)) (elimImpl b)
elimImpl t = compos' elimImpl t -- search deeper

Затем мы можем применить его, как это делает Луки выше, для поиска отрицательных союзов и дизъюнкций. А поскольку, как указывает Люк, вероятно, лучше выполнить все распределение отрицаний за один проход, мы также включим нормализацию отрицательного подтекста и исключение двойного отрицания, получая формулу в нормальной форме отрицания (при условии, что мы уже устранены последствия)

nnf :: LogicalExpression -> LogicalExpression
nnf (Neg (Conj a b)) = Disj (nnf (Neg a)) (nnf (Neg b))
nnf (Neg (Disj a b)) = Conj (nnf (Neg a)) (nnf (Neg b))
nnf (Neg (Neg a))    = nnf a
nnf t                = compos' nnf t -- search and replace

Ключ - последняя строка, в которой говорится, что если ни один из вышеперечисленных случаев не совпадает, поищите подвыражения, где вы можете применить это правило. Кроме того, так как мы выдвигаем Neg в терминах, а затем нормализовать их, вы должны в конечном итоге только с отрицательными переменными на листьях, так как все другие случаи, когда Neg предшествует другой конструктор будет нормализован прочь.

Более продвинутая версия будет использовать

import Control.Applicative
import Control.Monad.Identity

class Compos a where
    compos :: Applicative f => (a -> f a) -> a -> f a

compos' :: Compos a => (a -> a) -> a -> a
compos' f = runIdentity . compos (Identity . f) 

а также

instance Compos LogicalExpression where
    compos f (Neg e)    = Neg <$> f e
    compos f (Conj a b) = Conj <$> f a <*> f b
    compos f (Disj a b) = Disj <$> f a <*> f b
    compos f (Impl a b) = Impl <$> f a <*> f b
    compos _ t = pure t

Это не поможет в вашем конкретном случае здесь, но полезно позже, если вам нужно вернуть несколько переписанных результатов, выполните IOили иным образом участвуйте в более сложных действиях в вашем правиле перезаписи.

Возможно, вам придется использовать это, если, например, вы хотите попытаться применить законы деМоргана в любом подмножестве мест, где они применяются, а не следовать обычной форме.

Обратите внимание, что независимо от того, какую функцию вы переписываете, которую вы используете, или даже направленности потока информации во время обхода, compos определение должно быть дано только один раз для каждого типа данных.

Answer 2

Если я правильно понимаю, вы хотите применить законы Де Моргана, чтобы оттолкнуть отрицание в дерево как можно дальше. Вам придется многократно выполнять рекурсию по дереву:

-- no need to call self on the top-level structure,
-- since deMorgan is never applicable to its own result
deMorgan (Neg (a `Conj` b))  =  (deMorgan $ Neg a) `Disj` (deMorgan $ Neg b)
deMorgan (Neg (a `Disj` b))  =  (deMorgan $ Neg a) `Conj` (deMorgan $ Neg b)
deMorgan (Neg a)             =  Neg $ deMorgan a
deMorgan (a `Conj` b)        =  (deMorgan a) `Conj` (deMorgan b)
-- ... etc.

Все это было бы намного проще в системе переписывания терминов, но это не то, чем является Haskell.

(Кстати, жизнь становится намного проще, если вы переводите P -> Q в not P or Q в парсере формул и удалите Impli конструктор. Количество падежей в каждой функции по формулам становится меньше.)

Answer 3

Другие дали хорошее руководство. Но я бы сформулировал это как устранитель отрицания, так что это означает, что у вас есть:

deMorgan (Neg (Var x)) = Neg (Var x)
deMorgan (Neg (Neg a)) = deMorgan a
deMorgan (Neg (Conj a b)) = Disj (deMorgan (Neg a)) (deMorgan (Neg b))
-- ... etc. match Neg against every constructor
deMorgan (Conj a b) = Conj (deMorgan a) (deMorgan b)
-- ... etc. just apply deMorgan to subterms not starting with Neg

По индукции мы можем видеть, что в результате Neg будет применяться только к Var сроки и самое большее один раз.

Мне нравится думать о таких преобразованиях как об устранителях: то есть о вещах, которые пытаются "избавиться" от определенного конструктора на верхнем уровне, отталкивая его вниз. Сопоставьте конструктор, который вы удаляете, с каждым внутренним конструктором (включая самого себя), а затем просто переместите все остальное. Например, оценщик лямбда-исчисления является Apply Выпрямитель. SKI конвертер является Lambda Выпрямитель.

Answer 4

Важным моментом является рекурсивное применение deMorgan. Это сильно отличается от (например):

 deMorgan' z@(Var x) = z
 deMorgan' (Neg (Conj x y)) = (Disj (Neg x) (Neg y))
 deMorgan' (Neg (Disj x y)) = (Conj (Neg x) (Neg y))
 deMorgan' z@(Neg x) = z
 deMorgan' (Conj x y) = Conj x y
 deMorgan' (Disj x y) = Disj x y

который не работает:

 let var <- (Conj (Disj (Var 'A') (Var 'B')) (Neg (Disj (Var 'D') (Var 'E'))))
 *Main> deMorgan' var
 Conj (Disj (Var 'A') (Var 'B')) (Neg (Disj (Var 'D') (Var 'E')))

Проблема здесь в том, что вы не применяете преобразования в подвыражении (x и ys).