在Haskell中递归修改数据结构的各个部分

Question

大家好,我是Haskell的新手,我想创建一个可以应用DeMorgan关于逻辑表达式的法则的Haskell程序.问题是我无法将给定表达式更改为新表达式(在应用DeMorgan定律后)

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

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

我想创建一个函数,它接受"LogicalExpression"并在应用DeMorgan定律后返回"LogicalExpression".

例如,每当我在logicalExpression中找到这种模式:Neg(Conj(Var'a')(Var'b'))时,我需要将其转换为Conj(Neg(Var'a')Neg(Var'b') ).

这个想法很简单,但是在haskell中很难实现,就像试图创建一个函数(让我们称之为Z)来搜索x并将其转换为y,所以如果Z给出"vx"它将它转换为"vy" "只代替在数据结构中使用的字符串"logicalExpression"而不是x它采用我提到的模式并再次吐出整个logicalExpression,但模式已更改.

PS:我希望函数采用任何复杂的逻辑表达式,并使用DeMorgan定律简化它

任何提示？

提前致谢.

Answer 1

Luke(luqui)提出了可能是最优雅的方式来思考这个问题.但是,他的编码要求您为要创建的每个此类重写规则手动获取正确的遍历大量遍历.

Bjorn Bringert的A Pattern for Almost Composable函数的组合可以使这更容易,特别是如果你需要编写多个这样的规范化传递.它通常用Applicatives或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在上面所做的那样,寻找否定的连词和析取.而且,正如卢克指出的那样,在一次通过中做你所有的否定分布可能更好,我们还将包括否定蕴涵和双否定消除的归一化,产生否定正规形式的公式(假设我们已经消除暗示)

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法律应用于它们适用的位置的任何子集,而不是追求正常形式.

请注意,无论您正在重写哪种函数,在遍历期间使用的是应用程序,甚至是信息流的方向性,compos每种数据类型只需要给出一次定义.

Answer 2

如果我理解正确,你想要应用De Morgan的定律尽可能地将否定推入树中.你必须多次明确地递归树:

-- 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构造函数.案件在各功能配方奶粉的数量变少.)