0 
-- | data type definition of WFF: well formed formula
data Wff = Var String 
        | Not Wff
        | And Wff Wff 
        | Or Wff Wff
        | Imply Wff Wff

-- | Negation norm form  nnf function
--   precondition: φ is implication free
--   postcondition: NNF (φ) computes a NNF for φ
nnf :: Wff -> Wff
nnf (Var p) = Var p
nnf (Not (Not p)) = (nnf p)
nnf (And p q) = And (nnf p) (nnf q)
nnf (Or p q) = Or (nnf p) (nnf q)
nnf (Not (And p q)) = Or (nnf(Not p)) (nnf(Not q))
nnf (Not (Or p q)) = And (nnf(Not p)) (nnf(Not q))

テストケース: ¬( p ∨ Q )

(*** Exception:: Non-exhaustive patterns in function nnf

ただし、nnf (Not p) = Not (nnf p)関数に追加すると、表示されます

Pattern match(es) are overlapped
In an equation for ‘nnf’:
    nnf (Not (Not p)) = ...
    nnf (Not (And p q)) = ...
    nnf (Not (Or p q)) = ...

私は何が間違っているのだろうか？

4

1 に答える 1

2

間違った場所に行を挿入しているだけです。nnf (Not p) = ...否定のキャッチオールです。その後、 のようなより具体的な否定を処理する他の句を追加するとNot (And p q)、それらはおそらくもうトリガーできません。

キャッチオール句は最後にする必要があります。

nnf (Var p) = Var p
nnf (Not (Not p)) = (nnf p)
nnf (And p q) = And (nnf p) (nnf q)
nnf (Or p q) = Or (nnf p) (nnf q)
nnf (Not (And p q)) = Or (nnf $ Not p) (nnf $ Not q)
nnf (Not (Or p q)) = And (nnf $ Not p) (nnf $ Not q)
nnf (Not p) = Not $ nnf p
于 2016-02-14T23:51:39.423 に答える