diff --git a/LICENSE b/LICENSE --- a/LICENSE +++ b/LICENSE @@ -1,4 +1,4 @@ -Copyright (c) 2011, Benedict Eastaugh +Copyright (c) 2012, Benedict Eastaugh All rights reserved. diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -116,13 +116,27 @@ tables which it prints: green for true, red for false. You can enable colouring during interactive mode by using the `colour` command. +You can print out the normal forms of expressions too, by prefixing an +expression with `nnf`, `dnf` or `cnf`. + $ hatt --pretty + > nnf ~(P -> (Q & R)) + (P ∧ (¬Q ∨ ¬R)) + +The three supported normal forms are [negation normal form], [conjunctive normal +form] and [disjunctive normal form]. + + Using Hatt in other programs ---------------------------- Hatt exposes the `Data.Logic.Propositional` module, which provides a simple API -for parsing, evaluating, and printing truth tables. +for parsing, evaluating, and printing truth tables, and for converting logical +expressions into normal forms. [Hatt]: http://extralogical.net/projects/hatt [Hackage]: http://hackage.haskell.org/ +[negation normal form]: http://en.wikipedia.org/wiki/Negation_normal_form +[conjunctive normal form]: http://en.wikipedia.org/wiki/Conjunctive_normal_form +[disjunctive normal form]: http://en.wikipedia.org/wiki/Disjunctive_normal_form diff --git a/hatt.cabal b/hatt.cabal --- a/hatt.cabal +++ b/hatt.cabal @@ -1,11 +1,13 @@ Name: hatt -Version: 1.4.0.2 +Version: 1.5.0.0 Synopsis: A truth table generator for classical propositional logic. Description: Hatt is a command-line program which prints truth tables for expressions in classical propositional logic, and a library allowing its parser, evaluator and truth table - generator to be used in other programs. + generator to be used in other programs. It includes support + for converting logical expressions into several normal + forms. License: BSD3 License-file: LICENSE Author: Benedict Eastaugh @@ -13,7 +15,7 @@ Copyright: (c) 2012 Benedict Eastaugh Homepage: http://extralogical.net/projects/hatt Category: Logic -Cabal-version: >= 1.6 +Cabal-version: >= 1.8 Build-type: Simple Extra-source-files: README.md @@ -28,19 +30,27 @@ Build-depends: base >= 4 && < 5, containers >= 0.3 && < 0.5, parsec >= 2.1 && < 3.2, + QuickCheck >= 2.4, ansi-wl-pprint >= 0.6 && < 0.7 - Exposed-modules: Data.Logic.Propositional + Exposed-modules: Data.Logic.Propositional, + Data.Logic.Propositional.Tables, + Data.Logic.Propositional.NormalForms Other-modules: Data.Logic.Propositional.Core, - Data.Logic.Propositional.Parser, - Data.Logic.Propositional.Tables + Data.Logic.Propositional.Parser Executable hatt - Hs-Source-Dirs: src - Main-Is: hatt.hs + Main-Is: src/hatt.hs GHC-options: -Wall Build-depends: base >= 4 && < 5, + hatt, cmdargs >= 0.7, - containers >= 0.3 && < 0.5, - parsec >= 2.1 && < 3.2, - ansi-wl-pprint >= 0.6 && < 0.7, haskeline >= 0.6 && < 0.7 + +Test-Suite test-hatt + Type: exitcode-stdio-1.0 + Main-is: test/main.hs + GHC-options: -Wall + Build-depends: base >= 4 && < 5, + hatt, + test-framework >= 0.4.1, + test-framework-quickcheck2 diff --git a/src/Data/Logic/Propositional.hs b/src/Data/Logic/Propositional.hs --- a/src/Data/Logic/Propositional.hs +++ b/src/Data/Logic/Propositional.hs @@ -8,22 +8,27 @@ -- conjunction, disjunction, material implication and logical equivalence. module Data.Logic.Propositional ( Expr (..) + , Var (..) , Mapping , equivalent , interpret , assignments + , values + , variables , isContingent , isContradiction , isTautology + , parseExpr + , show , showAscii + , truthTable , truthTableP - , variables ) where import Data.Logic.Propositional.Core import Data.Logic.Propositional.Parser -import Data.Logic.Propositional.Tables +import Data.Logic.Propositional.Tables (truthTable, truthTableP) diff --git a/src/Data/Logic/Propositional/Core.hs b/src/Data/Logic/Propositional/Core.hs --- a/src/Data/Logic/Propositional/Core.hs +++ b/src/Data/Logic/Propositional/Core.hs @@ -4,12 +4,21 @@ import Prelude hiding (lookup) -import Control.Monad (replicateM) -import Data.List (nub) +import Control.Monad (liftM, liftM2, replicateM) +import Data.Char (chr) +import Data.Functor ((<$>)) +import Data.List (group, sort) import Data.Map (Map, fromList, lookup) import Data.Maybe (fromMaybe) +import Test.QuickCheck (Arbitrary, Gen, arbitrary, elements, oneof, sized) -data Expr = Variable String +newtype Var = Var Char + deriving (Eq, Ord) + +instance Show Var where + show (Var v) = [v] + +data Expr = Variable Var | Negation Expr | Conjunction Expr Expr | Disjunction Expr Expr @@ -18,15 +27,43 @@ deriving Eq instance Show Expr where - show (Variable name) = name + show (Variable name) = show name show (Negation expr) = '¬' : show expr show (Conjunction exp1 exp2) = showBC "∧" exp1 exp2 show (Disjunction exp1 exp2) = showBC "∨" exp1 exp2 show (Conditional exp1 exp2) = showBC "→" exp1 exp2 show (Biconditional exp1 exp2) = showBC "↔" exp1 exp2 -type Mapping = Map String Bool +instance Arbitrary Var where + arbitrary = liftM Var . elements . map chr $ [65..90] ++ [97..122] +instance Arbitrary Expr where + arbitrary = randomExpr + +randomExpr :: Gen Expr +randomExpr = sized randomExpr' + +randomExpr' :: Int -> Gen Expr +randomExpr' n | n > 0 = oneof [ randomVar + , randomNeg boundedExpr + , randomBin boundedExpr + ] + | otherwise = randomVar + where + boundedExpr = randomExpr' (n `div` 2) + +randomBin :: Gen Expr -> Gen Expr +randomBin rExp = oneof . map (\c -> liftM2 c rExp rExp) + $ [Conjunction, Disjunction, Conditional, Biconditional] + +randomNeg :: Gen Expr -> Gen Expr +randomNeg rExp = Negation <$> rExp + +randomVar :: Gen Expr +randomVar = Variable <$> arbitrary + +type Mapping = Map Var Bool + -- | In order to interpret an expression, a mapping from variables to truth -- values needs to be provided. Truth values are compositional; that's to say, -- the value of a composite expression (any expression which is not atomic) @@ -51,14 +88,14 @@ in map (fromList . zip vs) ps -- | Lists the names of variables present in an expression. -variables :: Expr -> [String] +variables :: Expr -> [Var] variables expr = let vars_ (Variable v) vs = v : vs vars_ (Negation e) vs = vars_ e vs vars_ (Conjunction e1 e2) vs = vars_ e1 vs ++ vars_ e2 vs vars_ (Disjunction e1 e2) vs = vars_ e1 vs ++ vars_ e2 vs vars_ (Conditional e1 e2) vs = vars_ e1 vs ++ vars_ e2 vs vars_ (Biconditional e1 e2) vs = vars_ e1 vs ++ vars_ e2 vs - in nub $ vars_ expr [] + in map head . group . sort $ vars_ expr [] -- | Determines whether two expressions are extensionally equivalent (that is, -- have the same values under all interpretations). @@ -87,7 +124,7 @@ -- pretty-prints expressions using logical symbols only present in extended -- character sets). showAscii :: Expr -> String -showAscii (Variable name) = name +showAscii (Variable name) = show name showAscii (Negation expr) = '~' : showAscii expr showAscii (Conjunction exp1 exp2) = showBCA "&" exp1 exp2 showAscii (Disjunction exp1 exp2) = showBCA "|" exp1 exp2 diff --git a/src/Data/Logic/Propositional/NormalForms.hs b/src/Data/Logic/Propositional/NormalForms.hs new file mode 100644 --- /dev/null +++ b/src/Data/Logic/Propositional/NormalForms.hs @@ -0,0 +1,94 @@ +{-# OPTIONS_HADDOCK hide #-} + +module Data.Logic.Propositional.NormalForms + ( toNNF + , toCNF + , toDNF + ) where + +import Data.Logic.Propositional.Core + +-- | The 'toNNF' function converts expressions to negation normal form. This +-- function is total: it's defined for all expressions, not just those which +-- only use negation, conjunction and disjunction, although all expressions in +-- negation normal form do in fact only use those connectives. +-- +-- The conversion is carried out by replacing any condtitionals or +-- biconditionals with equivalent expressions using only negation, conjunction +-- and disjunction. Then de Morgan's laws are applied to convert negated +-- conjunctions and disjunctions into the conjunction or disjunction of the +-- negation of their conjuncts: @¬(φ ∧ ψ)@ is converted to @(¬φ ∨ ¬ψ)@ +-- while @¬(φ ∨ ψ)@ becomes @(¬φ ∧ ¬ψ)@. +toNNF :: Expr -> Expr +toNNF expr@(Variable _) = expr +toNNF expr@(Negation (Variable _)) = expr +toNNF (Negation (Negation expr)) = expr + +toNNF (Conjunction exp1 exp2) = toNNF exp1 `conj` toNNF exp2 +toNNF (Negation (Conjunction exp1 exp2)) = toNNF $ neg exp1 `disj` neg exp2 + +toNNF (Disjunction exp1 exp2) = toNNF exp1 `disj` toNNF exp2 +toNNF (Negation (Disjunction exp1 exp2)) = toNNF $ neg exp1 `conj` neg exp2 + +toNNF (Conditional exp1 exp2) = toNNF $ neg exp1 `disj` exp2 +toNNF (Negation (Conditional exp1 exp2)) = toNNF $ exp1 `conj` neg exp2 + +toNNF (Biconditional exp1 exp2) = let a = exp1 `conj` exp2 + b = neg exp1 `conj` neg exp2 + in toNNF $ a `disj` b +toNNF (Negation (Biconditional exp1 exp2)) = let a = exp1 `disj` exp2 + b = neg exp1 `disj` neg exp2 + in toNNF $ a `conj` b + +-- | The 'toCNF' function converts expressions to conjunctive normal form: a +-- conjunction of clauses, where a clause is a disjunction of literals +-- (variables and negated variables). +-- +-- The conversion is carried out by first converting the expression into +-- negation normal form, and then applying the distributive law. +-- +-- Because it first applies 'toNNF', it is a total function and can handle +-- expressions which include conditionals and biconditionals. +toCNF :: Expr -> Expr +toCNF = toCNF' . toNNF + where + toCNF' :: Expr -> Expr + toCNF' (Conjunction exp1 exp2) = toCNF' exp1 `conj` toCNF' exp2 + toCNF' (Disjunction exp1 exp2) = toCNF' exp1 `dist` toCNF' exp2 + toCNF' expr = expr + + dist :: Expr -> Expr -> Expr + dist (Conjunction e11 e12) e2 = (e11 `dist` e2) `conj` (e12 `dist` e2) + dist e1 (Conjunction e21 e22) = (e1 `dist` e21) `conj` (e1 `dist` e22) + dist e1 e2 = e1 `disj` e2 + +-- | The 'toDNF' function converts expressions to disjunctive normal form: a +-- disjunction of clauses, where a clause is a conjunction of literals +-- (variables and negated variables). +-- +-- The conversion is carried out by first converting the expression into +-- negation normal form, and then applying the distributive law. +-- +-- Because it first applies 'toNNF', it is a total function and can handle +-- expressions which include conditionals and biconditionals. +toDNF :: Expr -> Expr +toDNF = toDNF' . toNNF + where + toDNF' :: Expr -> Expr + toDNF' (Conjunction exp1 exp2) = toDNF' exp1 `dist` toDNF' exp2 + toDNF' (Disjunction exp1 exp2) = toDNF' exp1 `disj` toDNF' exp2 + toDNF' expr = expr + + dist :: Expr -> Expr -> Expr + dist (Disjunction e11 e12) e2 = (e11 `dist` e2) `disj` (e12 `dist` e2) + dist e1 (Disjunction e21 e22) = (e1 `dist` e21) `disj` (e1 `dist` e22) + dist e1 e2 = e1 `conj` e2 + +neg :: Expr -> Expr +neg = Negation + +disj :: Expr -> Expr -> Expr +disj = Disjunction + +conj :: Expr -> Expr -> Expr +conj = Conjunction diff --git a/src/Data/Logic/Propositional/Parser.hs b/src/Data/Logic/Propositional/Parser.hs --- a/src/Data/Logic/Propositional/Parser.hs +++ b/src/Data/Logic/Propositional/Parser.hs @@ -5,7 +5,7 @@ ( parseExpr ) where -import Data.Logic.Propositional.Core (Expr (..)) +import Data.Logic.Propositional.Core (Expr (..), Var (..)) import Text.ParserCombinators.Parsec ((<|>), char, choice, eof, letter, parse, spaces, string, try) @@ -50,7 +50,7 @@ variable :: GenParser Char st Expr variable = do c <- letter - return $ Variable [c] + return $ Variable (Var c) negation :: GenParser Char st Expr negation = do char '~' diff --git a/src/Data/Logic/Propositional/Tables.hs b/src/Data/Logic/Propositional/Tables.hs --- a/src/Data/Logic/Propositional/Tables.hs +++ b/src/Data/Logic/Propositional/Tables.hs @@ -25,7 +25,7 @@ truthTableP :: Printer -> Expr -> String truthTableP (expPrinter, boolPrinter) expr = unlines [header, separator, body] where - header = unwords vs ++ " | " ++ expPrinter expr + header = (unwords . map show) vs ++ " | " ++ expPrinter expr body = init . unlines $ map (showAssignment boolPrinter expr) as separator = concat $ replicate sepLength "-" sepLength = length vs * 2 + length (expPrinter expr) + 2 diff --git a/src/hatt.hs b/src/hatt.hs --- a/src/hatt.hs +++ b/src/hatt.hs @@ -4,17 +4,26 @@ import Data.Logic.Propositional import Data.Logic.Propositional.Tables +import Data.Logic.Propositional.NormalForms import Control.Monad (when, unless) -import Data.Char (isSpace, toLower) +import Data.Char (toLower) import System.Console.CmdArgs -import System.Console.Haskeline (InputT, runInputT, defaultSettings, getInputLine, outputStr, outputStrLn) +import System.Console.Haskeline + ( InputT + , runInputT + , defaultSettings + , getInputLine + , outputStr + , outputStrLn + ) data Command = Exit | Help | Pretty | Coloured | Eval Expr + | Convert NormalForm Expr | Error String data ProgramMode = ProgramMode @@ -24,6 +33,8 @@ , coloured :: Bool } deriving (Show, Data, Typeable) +data NormalForm = NNF | CNF | DNF + programMode :: ProgramMode programMode = ProgramMode { evaluate = "" &= typ "EXPRESSION" @@ -58,17 +69,19 @@ case minput of Nothing -> return () Just cmd -> case parseCommand cmd of - Exit -> return () - Help -> outputStr (replHelpText printer) - >> repl mode - Pretty -> outputStrLn ppMessage - >> repl (mode {pretty = not isPretty}) - Coloured -> outputStrLn cpMessage - >> repl (mode {coloured = not isColoured}) - (Eval expr) -> outputStr (truthTableP printer expr) - >> repl mode - (Error err) -> outputStrLn ("Error: " ++ err) - >> repl mode + Exit -> return () + Help -> outputStr (replHelpText printer) + >> repl mode + Pretty -> outputStrLn ppMessage + >> repl (mode {pretty = not isPretty}) + Coloured -> outputStrLn cpMessage + >> repl (mode {coloured = not isColoured}) + (Eval expr) -> outputStr (truthTableP printer expr) + >> repl mode + (Convert nf expr) -> outputStrLn (toNFStr nf (fst printer) expr) + >> repl mode + (Error err) -> outputStrLn ("Error: " ++ err) + >> repl mode where printer = selectPrinter mode isPretty = pretty mode @@ -82,20 +95,29 @@ Right expr -> truthTableP p expr parseCommand :: String -> Command -parseCommand input = case cmd . words . dropWhile isSpace $ input of +parseCommand input = case cmd . words $ input of "" -> Error "you must enter an expression or a command." "exit" -> Exit "help" -> Help "pretty" -> Pretty "colour" -> Coloured - _ -> eval_ input + "nnf" -> eval_ (Convert NNF) (getExpr input) + "cnf" -> eval_ (Convert CNF) (getExpr input) + "dnf" -> eval_ (Convert DNF) (getExpr input) + _ -> eval_ Eval input where - cmd [] = "" - cmd ws = map toLower . head $ ws - eval_ str = case parseExpr "" str of - Left err -> Error $ "parse error at " ++ show err - Right expr -> Eval expr + cmd [] = "" + cmd ws = map toLower . head $ ws + eval_ dt str = case parseExpr "hatt" str of + Left err -> Error $ "parse error at " ++ show err + Right expr -> dt expr + getExpr = unwords . tail . words +toNFStr :: NormalForm -> (Expr -> String) -> Expr -> String +toNFStr NNF p = p . toNNF +toNFStr CNF p = p . toCNF +toNFStr DNF p = p . toDNF + replIntroText :: String replIntroText = unwords [ "Entering interactive mode." @@ -128,14 +150,25 @@ , "For example, if you enter \"(A -> B)\" at the prompt, Hatt will print the" , "truth table for that expression. Here's an example console session." , "" - , " > A | B" - , indentBy 4 $ truthTableP printer (Disjunction (Variable "A") (Variable "B")) - ++ "> P -> (Q & R)\n" - ++ truthTableP printer (Conditional - (Variable "P") - (Conjunction (Variable "Q") (Variable "R"))) + , " > " ++ showAscii exp1 + , indentBy 4 $ truthTableP printer exp1 + ++ "> " ++ showAscii exp2 ++ "\n" + ++ truthTableP printer exp2 + , "You can also convert expressions to different normal forms: negation" + , "normal form, conjunctive normal form and disjunctive normal form. To do" + , "this just prepend the expression you want to convert with \"nnf\", \"cnf\"" + , "or \"dnf\". For example," + , "" + , " > nnf " ++ showAscii exp3 + , " " ++ (fst printer . toNNF) exp3 + , "" , "If none of this makes any sense, try reading the README file." ] + where + exp1 = Disjunction (Variable $ Var 'A') (Variable $ Var 'B') + exp2 = Conditional (Variable $ Var 'P') exp4 + exp3 = Negation exp2 + exp4 = Conjunction (Variable $ Var 'Q') (Variable $ Var 'R') selectPrinter :: ProgramMode -> Printer selectPrinter m = let expPrinter = if pretty m then show else showAscii diff --git a/test/main.hs b/test/main.hs new file mode 100644 --- /dev/null +++ b/test/main.hs @@ -0,0 +1,32 @@ +module Main (main) where + +import Data.Logic.Propositional +import Data.Logic.Propositional.NormalForms + +import Test.Framework as TF (defaultMain, testGroup, Test) +import Test.Framework.Providers.QuickCheck2 (testProperty) + +main :: IO () +main = defaultMain tests + +tests :: [TF.Test] +tests = + [ testGroup "QuickCheck Data.Logic.Propositional.NormalForms" + [ testProperty "SelfEquiv" propSelfEquiv + , testProperty "NNFEquiv" propNNFEquiv + , testProperty "CNFEquiv" propCNFEquiv + , testProperty "DNFEquiv" propDNFEquiv + ] + ] + +propSelfEquiv :: Expr -> Bool +propSelfEquiv expr = expr `equivalent` expr + +propNNFEquiv :: Expr -> Bool +propNNFEquiv expr = expr `equivalent` toNNF expr + +propCNFEquiv :: Expr -> Bool +propCNFEquiv expr = expr `equivalent` toCNF expr + +propDNFEquiv :: Expr -> Bool +propDNFEquiv expr = expr `equivalent` toDNF expr