Рекурсивно модифицирующие части структуры данных в 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" только вместо строк, которые он принимает в структуре данных "logicExpression", а вместо x он берет шаблон, который я упомянул, и снова выплевывает все логическое выражение, но с измененным шаблоном.

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

Любые подсказки?

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

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