递归地修改Haskell中数据结构的一部分

| 大家好，我是Haskell的新手，我想创建一个Haskell程序，该程序可以在逻辑表达式上应用DeMorgan的定律。问题是我无法将给定的表达式更改为新的表达式（在应用了德摩根定律之后）具体来说就是我的数据结构

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

我想创建一个在应用DeMorgan定律后接受\“ LogicalExpression \”并返回\\“ LogicalExpression \”的函数。例如，每当我找到以下模式：Neg（conj（Var \'a \'）（Var \'b \'））时，我都需要将其转换为Conj（Neg（Var \'a \'）Neg （Var \'b \'））。这个想法很简单，但是很难在haskell中实现，就像试图创建一个搜索x并将其转换为y的函数（让我们将其称为Z）一样，因此如果给定Z \“ vx \”仅将其转换为\“ vy \”而不是将其转换为数据结构\“ logicalExpression \”的字符串，并且将x转换为我提到的模式，并再次使用该模式吐出整个logicalExpression改变了。 P.S：我希望函数采用任何复杂的逻辑表达式，并使用DeMorgan定律简化它有什么提示吗？提前致谢。

已邀请:

4 个回复

为陡土

卢克（luqui）提出了思考问题的最优雅方法。但是，他的编码要求您为要创建的每个此类重写规则手动获得正确的遍历范围。比约恩·布林格特（Bjorn Bringert）的“几乎可组合功能的模式”中的组合可以使此操作变得更容易，尤其是如果您需要编写多个这样的规范化遍历时。它通常是用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一样，我们可以应用它，寻找否定的连接词和析取词。而且，正如Luke指出的那样，最好一次完成所有否定分布，所以我们还将包括否定蕴涵的归一化和双重否定消除，从而得出否定正态形式的公式（假设我们ve已经消除了暗示）

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推入到项中，然后对其进行归一化，因此您只应在叶的末尾加上负数变量，因为ѭ5cases在另一个构造函数之前的所有其他情况都将被归一化。更高级的版本将使用

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

这对您的特定情况没有帮助，但是稍后在您需要返回多个重写结果，执行“ 9”或在重写规则中进行更复杂的活动时很有用。您可能需要使用此方法，例如，如果您想尝试将deMorgan法则应用于其适用位置的任何子集中，而不是遵循常规形式。请注意，无论您正在重写什么功能，正在使用的“应用程序”，甚至遍历过程中信息流的方向性，每种数据类型都仅需给出一次“ 10”定义。

马口

如果我理解正确，那么您想应用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构造函数，生活会变得容易得多。公式上每个函数的用例数会减少。）

才改隘瘁

其他人给予了很好的指导。但是我将其表述为否定消除器，这意味着您拥有：

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项，最多只能应用一次。我喜欢将这样的转换视为消除器：即，通过向下推来试图“摆脱”某个构造函数的事物。将要消除的构造函数与每个内部构造函数（包括自身）进行匹配，然后将其余的转发。例如，lambda演算评估器是ѭ18消除器。 SKI转换器是一个19消除器。

械怒等

重要的是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）中应用转换。

要回复问题请先登录或注册

递归地修改Haskell中数据结构的一部分

4 个回复

发起人

data_structures

haskell

referential_transparency

问题状态

递归地修改Haskell中数据结构的一部分

与内容相关的链接

4 个回复

发起人

data_structures

haskell

referential_transparency

问题状态