3

こんにちは、私は Haskell の初心者です。DeMorgan の法則を論理式に適用できる Haskell プログラムを作成したいと考えています。問題は、与えられた式を新しい式に変更できないことです (DeMorgan の法則を適用した後)

具体的には、私のデータ構造です

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

「LogicalExpression」を受け取り、DeMorgan の法則を適用した後に「LogicalExpression」を返す関数を作成したいと思います。

たとえば、このパターンを見つけるたびに: Neg ( Conj (Var 'a') (Var 'b') ) in a logicalExpression, Conj ( Neg (Var 'a') Neg (Var 'b') に変換する必要があります）。

アイデアは単純ですが、haskell で実装するのは非常に難しいです。x を検索して y に変換する関数 (Z と呼びましょう) を作成しようとするようなもので、Z に "vx" を指定すると、それは "vy" に変換されます。文字列の代わりにデータ構造「logicalExpression」を取り、x の代わりに私が言及したパターンを取り、logicalExpression 全体を再び吐き出しますが、パターンは変更されています。

PS:関数が任意の複雑な論理式を取り、DeMorgan の法則を使用して単純化するようにしたい

ヒントはありますか？

前もって感謝します。

4

4 に答える 4

7

Luke (luqui) は、おそらく最も洗練された問題の考え方を提示しました。ただし、彼のエンコーディングでは、作成する書き換えルールごとに、トラバーサルの大部分を手動で取得する必要があります。

A Pattern for Most Composable Functionsの 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 が指摘しているように、すべての否定分布を 1 回のパスで実行する方がおそらく良いため、否定された含意の正規化と二重否定の除去も含めて、否定の正規形の式を生成します (既に排除された含意)

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定義はデータ型ごとに 1 回だけ指定する必要があることに注意してください。

于 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 Qを削除すると、作業がずっと楽になりますImpli。数式の各関数のケース数は少なくなります。)

于 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、多くても 1 回であることがわかります。

私は、このような変換をエリミネーターと考えるのが好きです。つまり、特定のコンストラクターを最上位レベルで押し下げて「取り除こうとする」ものです。削除するコンストラクターをすべての内部コンストラクター (それ自体を含む) と照合し、残りを転送します。たとえば、ラムダ計算エバリュエーターは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 に答える