3

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

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

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

我想创建一个接受“LogicalExpression”并在应用德摩根定律后返回“LogicalExpression”的函数。

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

这个想法很简单，但是在haskell中实现起来非常困难，这就像试图创建一个搜索x并将其转换为y的函数（我们称之为Z），所以如果Z被赋予“vx”，它会将其转换为“vy " 仅在数据结构“logicalExpression”中采用字符串而不是 x 而不是 x 它采用我提到的模式并再次吐出整个logicalExpression，但模式已更改。

PS：我希望该函数采用任何复杂的逻辑表达式并使用德摩根定律对其进行简化

有什么提示吗？

提前致谢。

4

4 回答 4

7

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

Bjorn Bringert 来自A Pattern for Nearly Composable Functions 的组合可以使这更容易，特别是如果您需要编写多个这样的规范化通道。它通常用 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或以其他方式在重写规则中参与更复杂的活动，这将很有用。

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

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

于 2011-06-01T02:52:39.330 回答
6

如果我理解正确，您想应用德摩根定律将否定尽可能推入树中。您必须多次显式递归树：

-- 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 QImpli

于 2011-05-31T22:11:50.270 回答
4

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

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 演算评估器是一个Apply消除器。SKI 转换器是一种Lambda消除器。

于 2011-06-01T00:25:21.973 回答
2

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

于 2011-05-31T21:20:06.730 回答