L'algorithme de Quine pour savoir si une formule est satifiable.

quine.hs

{-# LANGUAGE InstanceSigs #-}
{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}
{-# LANGUAGE StrictData #-}

module Quine where
import Data.Maybe ( fromJust )

-- Propositional calculus
data Formula = Top | Bottom | P !Integer | Disjunction !Formula !Formula | Conjunction !Formula !Formula | Negation !Formula

instance Show Formula where
    show :: Formula -> String
    show Top = "T"
    show Bottom = "⊥"
    show (P n) = "p" ++ show n
    show (Disjunction f1 f2) = "(" ++ show f1 ++ ") v (" ++ show f2 ++ ")"
    show (Conjunction f1 f2) = "(" ++ show f1 ++ ") ∧ (" ++ show f2 ++ ")"
    show (Negation f) = "¬(" ++ show f ++ ")"

instance Eq Formula where
    (==) :: Formula -> Formula -> Bool
    Top == Top = True
    Bottom == Bottom = True
    (Disjunction f1 f2) == (Disjunction f3 f4) = f1 == f3 && f2 == f4
    (Conjunction f1 f2) == (Conjunction f3 f4) = f1 == f3 && f2 == f4
    (Negation f1) == (Negation f2) = f1 == f2
    (P i) == (P j) = i == j
    _ == _ = False

substitution :: Formula -> Formula -> Formula -> Formula
substitution f f1 f2 = if f == f1 then f2 else case f of
    Conjunction fa fb -> Conjunction (substitution fa f1 f2) (substitution fb f1 f2)
    Disjunction fa fb -> Disjunction (substitution fa f1 f2) (substitution fb f1 f2)
    Negation fa -> Negation (substitution fa f1 f2)
    P i -> P i
    Top -> Top
    Bottom -> Bottom

-- A satisfiable formula and an antilogy
f :: Formula
f = Conjunction Top (Negation (Conjunction (P 2) Top))
f2 :: Formula
f2 = Conjunction (P 1) (Negation $ P 1)

-- The valuation function
valuation :: [Bool] -> Formula -> Bool
valuation l Top =  True
valuation l Bottom = False
valuation l (Conjunction f1 f2) = valuation l f1 && valuation l f2
valuation l (Disjunction f1 f2) = valuation l f1 || valuation l f2
valuation l (Negation f) = not (valuation l f)
valuation l (P i) = l !! fromInteger i


-- Simplification rules
simplify :: Formula -> Formula
simplify Top = Top
simplify Bottom = Bottom

simplify (Negation Bottom) = Top
simplify (Negation Top) = Bottom

simplify (Disjunction Top f) = Top
simplify (Disjunction f Top) = Top
simplify (Disjunction Bottom f) = f
simplify (Disjunction f Bottom) = f

simplify (Conjunction Top f) = f
simplify (Conjunction f Top) = f
simplify (Conjunction Bottom f) = Bottom
simplify (Conjunction f Bottom) = Bottom

simplify (Conjunction f1 f2) = Conjunction (simplify f1) (simplify f2)
simplify (Disjunction f1 f2) = Disjunction (simplify f1) (simplify f2)
simplify (Negation f) = Negation (simplify f)

simplify (P i) = P i

-- Simplifies the expression using the rules
applySimplifications :: Formula -> Formula
applySimplifications f = if f/=q then applySimplifications q else q
    where
        q = simplify f

-- Finds a variable in the tree
findVariable :: Formula -> Maybe Formula
findVariable (Conjunction f1 f2) = case findVariable f1 of
    Just v -> Just v
    Nothing -> findVariable f2
findVariable (Disjunction f1 f2) = case findVariable f1 of
    Just v -> Just v
    Nothing -> findVariable f2
findVariable (Negation f) = findVariable f
findVariable (P i) = Just $ P i
findVariable _ = Nothing

newTree :: Formula -> Formula
newTree f = Disjunction (substitution f p Top) (substitution f p Bottom)
    where
        p = fromJust $ findVariable f

quineAlgorithm :: Formula -> Formula
quineAlgorithm f = if q == Top || q == Bottom then q else quineAlgorithm $ newTree q
    where
        q = applySimplifications f