logic.hs

import Prelude hiding (print, negate)
import Data.List (nub)

data PVar = X Int deriving (Eq,Ord)
x = Var . X
data Connective = And | Or | Imp | Bi
data Boolean = T | F deriving Eq
data PL = Boole Boolean | Var PVar | Not PL | Conn Connective PL PL

type Substitution = (PVar -> PL)

type Assignment = (PVar -> Boolean)

instance Show Connective where
    show And = "^"
    show Or = "v"
    show Imp = "->"
    show Bi = "<->"

instance Show Boolean where
    show T = "1"
    show F = "0"

instance Show PVar where
    show (X i) = "X" ++ show i

instance Show PL where
    show p = foldLogic
           show
           show
           (\p -> "¬(" ++ p ++ ")")
           (\c p q -> "(" ++ p ++ ") " ++ (show c) ++ " (" ++ q ++ ")")
           p

instance Eq PL where
    p == q = tautology (Conn Bi p q)

negate :: Boolean -> Boolean
negate T = F
negate F = T

apply :: Connective -> Boolean -> Boolean -> Boolean

apply And F _ = F
apply And _ x = x

apply Or T _ = T
apply Or _ x = x

apply Imp F _ = T
apply Imp T x = x

apply Bi T T = T
apply Bi F F = T
apply Bi _ _ = F

foldLogic :: (Boolean -> a) -> (PVar -> a) -> (a -> a) -> (Connective -> a -> a -> a) -> PL -> a
foldLogic f g h i (Boole b) = f b
foldLogic f g h i (Var pv) = g pv
foldLogic f g h i (Not pl) = h $ foldLogic f g h i pl
foldLogic f g h i (Conn c p q) = i c (foldLogic f g h i p) (foldLogic f g h i q)

logicIdentity = foldLogic Boole Var Not Conn

evaluate :: Assignment -> PL -> Boolean
evaluate beta = foldLogic id beta negate apply

makeAssignment :: [(Int, Boolean)] -> Assignment
makeAssignment xs = 
    \(X i) -> case lookup i xs of
               (Just b) -> b
               Nothing -> error ("Assignment not suitable for " ++ show (x i))

substitute :: Substitution -> PL -> PL
substitute sub = foldLogic Boole sub Not Conn

makeSubstitution :: [(Int, PL)] -> Substitution
makeSubstitution xs = 
    \(X i) -> case lookup i xs of
               (Just p) -> p
               Nothing -> (x i)

subFormulas :: PL -> [PL]
subFormulas = foldLogic 
              ((:[]) . Boole)
              ((:[]) . Var)
              (\p -> Not (head p) : p)
              (\c p q -> Conn c (head p) (head q) : (p ++ q))

size :: PL -> Int
size = foldLogic
       (const 1)
       (const 1)
       (1+)
       (const (+))

bigDisjunction :: [PL] -> PL
bigDisjunction (x:xs) = foldl (Conn Or) x xs 

bigConjunction :: [PL] -> PL
bigConjunction (x:xs) = foldl (Conn And) x xs

vars :: PL -> [PVar]
vars = foldLogic
       (const [])
       (:[])
       id
       (const merge)
    where
      merge [] ys = ys
      merge xs [] = xs
      merge (x:xs) (y:ys) | x < y = x : (merge xs (y:ys))
                          | x > y = y : (merge (x:xs) ys)
                          | x == y = x : (merge xs ys)

cartesian :: [[a]] -> [[a]]
cartesian = foldr cp [[]]
            where cp newl oldl = concatMap (\x -> map (:x) newl) oldl

makeAssignments :: PL -> [Assignment]
makeAssignments p = map (makeAssignment . (zip vis)) cs
    where
      vs = vars p
      vis = map (\(X i) -> i) vs
      cs = cartesian (replicate (length vs) [T,F])

truthTable :: PL -> [Boolean]
truthTable p = map ((flip evaluate) p) (makeAssignments p)

tautology :: PL -> Bool
tautology = (==T) . foldr (apply And) T . truthTable

unsatisfiable :: PL -> Bool
unsatisfiable = (==F) . foldr (apply Or) F . truthTable