data-structures - 在 Haskell 中递归修改部分数据结构

Question

大家好，我是 Haskell 的新手，我想创建一个 Haskell 程序，该程序可以将 DeMorgan 定律应用于逻辑表达式。问题是我无法将给定的表达式更改为新的表达式(在应用德摩根定律之后)

具体来说，这里是我的数据结构

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 "只是它采用数据结构“logicalExpression”而不是字符串，而不是 x 它采用我提到的模式并再次吐出整个逻辑表达式，但模式已更改。

P.S:我希望该函数采用任何 复杂逻辑表达式并使用德摩根定律将其简化

任何提示？

提前致谢。

Answer 1

卢克 (luqui) 提出了可能是考虑问题的最优雅的方式。但是，他的编码要求您为要创建的每个此类重写规则手动获取正确的大范围遍历。

来自 A Pattern for Almost Composable Functions 的 Bjorn Bringert 的作品可以使这更容易，特别是如果您需要编写多个此类规范化过程。它通常用 Applicatives 或 rank 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

然后我们可以应用它，就像上面 luqui 所做的那样，寻找否定的连词和析取词。而且，正如 Luke 指出的那样，一次完成所有否定分布可能更好，因此我们还将包括否定蕴涵的归一化和双重否定消除，从而产生否定范式的公式(假设我们已经消除的含义)

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 很有用，或以其他方式在您的重写规则中从事更复杂的事件。

您可能需要使用它，例如，如果您想尝试将 deMorgan 定律应用于它们适用的位置的任何子集，而不是追求正常形式。

请注意，无论您正在重写什么函数，使用什么 Applicative，甚至遍历过程中信息流的方向性， compos每种数据类型只需给出一次定义。