日々の流転

λ. 連言標準形への変形

ふと、論理式の連言標準形(Conjunctive normal form, CNF)への変形を素朴に書いてみたのだけど……イマイチ。

type Var = Int

data Formula
    = Var Var
    | Not (Formula)
    | And [Formula]
    | Or [Formula]
    | Imply Formula Formula
    | Equiv Formula Formula

data Lit = Pos Var | Neg Var
type Clause = [Lit]
type CNF = [Clause]

toCNF :: Formula -> CNF
toCNF = f
  where
    f :: Formula -> CNF
    f (Var v)     = [[Pos v]]
    f (Not a)     = g a
    f (And xs)    = concatMap f xs
    f (Or xs)     = cnfOr (map f xs)
    f (Imply a b) = f (Or [Not a, b])
    f (Equiv a b) = f (And [Imply a b, Imply b a])

    g :: Formula -> CNF
    g (Var v)     = [[Neg v]]
    g (Not a)     = f a
    g (And xs)    = cnfOr (map g xs)
    g (Or xs)     = concatMap g xs
    g (Imply a b) = g (Or [Not a, b])
    g (Equiv a b) = g (And [Imply a b, Imply b a])

    cnfOr :: [CNF] -> CNF
    cnfOr = foldr (\xs ys -> [x++y | x <- xs, y <- ys]) [[]]

Imply や Equiv の処理で再帰呼び出しの部分は、定義を展開して特殊化したコードを出力してほしかったのだけど、inline 組み込み関数を使ってもそれは無理だった。しょうがないと言えばしょうがないけど、うまい方法はないものか。