diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -0,0 +1,30 @@ +Copyright (c)2011, Benedict Eastaugh + +All rights reserved. + +Redistribution and use in source and binary forms, with or without +modification, are permitted provided that the following conditions are met: + + * Redistributions of source code must retain the above copyright + notice, this list of conditions and the following disclaimer. + + * Redistributions in binary form must reproduce the above + copyright notice, this list of conditions and the following + disclaimer in the documentation and/or other materials provided + with the distribution. + + * Neither the name of Benedict Eastaugh nor the names of other + contributors may be used to endorse or promote products derived + from this software without specific prior written permission. + +THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS +"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT +LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR +A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT +OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, +SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT +LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, +DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY +THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT +(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE +OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. diff --git a/README.md b/README.md new file mode 100644 --- /dev/null +++ b/README.md @@ -0,0 +1,72 @@ +Hatt +==== + +[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. + + +Installation +------------ + +Hatt is available from [Hackage]. To install it with `cabal-install`, update +your list of known packages and then install Hatt. + + $ cabal update + $ cabal install hatt + +To build it from source, `cd` into the directory containing the Hatt source +files, including `hatt.cabal`, and run `cabal install`. + + +Valid Hatt expressions +---------------------- + +The following are all valid expression forms which can be parsed by Hatt, where +ϕ and ψ are metalinguistic variables standing in for any valid expression. The +parser isn't as smart about parentheses as it could be, so you have to follow +these rules quite literally. This shouldn't be a great hardship, but it does +mean that, for example, while `(A -> B)` is a valid expression, `A -> B` isn't. + +* Variables: `P`, `Q`, `R` etc.---basically anything in the character class + `[A-Z]` +* Negation: `~ϕ` +* Conjunction: `(ϕ & ψ)` +* Disjunction: `(ϕ | ψ)` +* Conditional: `(ϕ -> ψ)` +* Biconditional: `(ϕ <-> ψ)` + + +Using the `hatt` command-line program +------------------------------------- + +The `--evaluate` flag lets you pass an expression to be evaluated directly. +Here's an example session doing just that. + + $ hatt --evaluate="(P -> (Q | ~R))" + P Q R | (P → (Q ∨ ¬R)) + ---------------------- + T T T | F + T T F | F + T F T | F + T F F | F + F T T | F + F T F | F + F F T | T + F F F | F + +Note that while you need to use ASCII symbols to interact with `hatt`, it +pretty-prints expressions using the more common logical symbols. The Hatt +library exposes the `showAscii` function which will print expressions in the +format in which they're entered. + + +Using Hatt in other programs +---------------------------- + +Hatt exposes the `Data.Logic.Propositional` module, which provides a simple API +for parsing, evaluating, and printing truth tables. + + +[Hatt]: http://extralogical.net/projects/hatt +[Hackage]: http://hackage.haskell.org/ diff --git a/Setup.hs b/Setup.hs new file mode 100644 --- /dev/null +++ b/Setup.hs @@ -0,0 +1,2 @@ +import Distribution.Simple +main = defaultMain diff --git a/hatt.cabal b/hatt.cabal new file mode 100644 --- /dev/null +++ b/hatt.cabal @@ -0,0 +1,44 @@ +Name: hatt +Version: 0.1 +Stability: experimental + +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. +License: BSD3 +License-file: LICENSE +Author: Benedict Eastaugh +Maintainer: benedict@eastaugh.net +Copyright: (c) 2011 Benedict Eastaugh +Homepage: https://github.com/beastaugh/hatt +Category: Logic +Cabal-version: >= 1.6 + +Build-type: Simple +Extra-source-files: README.md + +Source-repository head + Type: git + Location: git://github.com/beastaugh/hatt.git + +Library + Hs-Source-Dirs: src + GHC-options: -Wall + Build-depends: base >= 4.2 && < 4.3, + containers >= 0.3 && < 0.4, + parsec >= 2.1 && < 2.2 + Exposed-modules: Data.Logic.Propositional, + Data.Logic.Propositional.Core, + Data.Logic.Propositional.Parser, + Data.Logic.Propositional.Tables + +Executable hatt + Hs-Source-Dirs: src + Main-Is: hatt.hs + GHC-options: -Wall + Build-depends: base >= 4.2 && < 4.3, + cmdargs >= 0.6 && < 0.7, + containers >= 0.3 && < 0.4, + parsec >= 2.1 && < 2.2 diff --git a/src/Data/Logic/Propositional.hs b/src/Data/Logic/Propositional.hs new file mode 100644 --- /dev/null +++ b/src/Data/Logic/Propositional.hs @@ -0,0 +1,28 @@ +-- | The "Data.Logic.Propositional" module provides a set of functions for +-- parsing, manipulating and generating truth tables for expressions in +-- classical propositional logic. +-- +-- The core of the API is the 'Expr' data type, which has constructors for all +-- the usual expression forms: variables, standing for atomic propositions; +-- negation, the only unary connective; and the binary connectives of +-- conjunction, disjunction, material implication and logical equivalence. +module Data.Logic.Propositional + ( Expr (..) + , Mapping + + , equivalent + , interpret + , assignments + , isContingent + , isContradiction + , isTautology + , parseExpr + , show + , showAscii + , truthTable + , variables + ) where + +import Data.Logic.Propositional.Core +import Data.Logic.Propositional.Parser +import Data.Logic.Propositional.Tables diff --git a/src/Data/Logic/Propositional/Core.hs b/src/Data/Logic/Propositional/Core.hs new file mode 100644 --- /dev/null +++ b/src/Data/Logic/Propositional/Core.hs @@ -0,0 +1,104 @@ +{-# OPTIONS_HADDOCK hide #-} + +module Data.Logic.Propositional.Core where + +import Prelude hiding (lookup) + +import Control.Monad (replicateM) +import Data.Map (Map, fromList, lookup) +import Data.Maybe (fromMaybe) + +data Expr = Variable String + | Negation Expr + | Conjunction Expr Expr + | Disjunction Expr Expr + | Conditional Expr Expr + | Biconditional Expr Expr + deriving Eq + +instance Show Expr where + show (Variable name) = 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 + +-- | 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) +-- depends on the truth values of its component parts. For example, the Haskell +-- expression below would evaluate to @False@. +-- +-- > interpret +-- > (Conjunction (Variable "A") (Variable "B")) +-- > (fromList [("A", True), ("B", False)]) +interpret :: Expr -> Mapping -> Bool +interpret (Variable v) vs = fromMaybe False (lookup v vs) +interpret (Negation expr) vs = not $ interpret expr vs +interpret (Conjunction exp1 exp2) vs = interpret exp1 vs && interpret exp2 vs +interpret (Disjunction exp1 exp2) vs = interpret exp1 vs || interpret exp2 vs +interpret (Conditional exp1 exp2) vs = not $ interpret exp1 vs || interpret exp2 vs +interpret (Biconditional exp1 exp2) vs = interpret exp1 vs == interpret exp2 vs + +-- | Generates the possible assignments of variables in an expression. +assignments :: Expr -> [Mapping] +assignments expr = let vs = variables expr + ps = replicateM (length vs) [True, False] + in map (fromList . zip vs) ps + +-- | Lists the names of variables present in an expression. +variables :: Expr -> [String] +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 vars_ expr [] + +-- | Determines whether two expressions are extensionally equivalent (that is, +-- have the same values under all interpretations). +equivalent :: Expr -> Expr -> Bool +equivalent exp1 exp2 = values exp1 == values exp2 + +-- | Determines whether an expression is tautological. +isTautology :: Expr -> Bool +isTautology = and . values + +-- | Determines whether an expression is contradictory. +isContradiction :: Expr -> Bool +isContradiction = not . or . values + +-- | Determines whether an expression is contingent (that is, true in at least +-- one interpretation and false in at least one interpretation). +isContingent :: Expr -> Bool +isContingent expr = not (isTautology expr || isContradiction expr) + +-- | Lists the values of an expression under all interpretations (that is, all +-- assignments of values to variables). +values :: Expr -> [Bool] +values expr = map (interpret expr) (assignments expr) + +-- | Represents expressions using only ASCII characters (the 'show' function +-- pretty-prints expressions using logical symbols only present in extended +-- character sets). +showAscii :: Expr -> String +showAscii (Variable name) = name +showAscii (Negation expr) = '~' : showAscii expr +showAscii (Conjunction exp1 exp2) = showBCA "&" exp1 exp2 +showAscii (Disjunction exp1 exp2) = showBCA "|" exp1 exp2 +showAscii (Conditional exp1 exp2) = showBCA "->" exp1 exp2 +showAscii (Biconditional exp1 exp2) = showBCA "<->" exp1 exp2 + +showBinaryConnective :: (Expr -> String) -> String -> Expr -> Expr -> String +showBinaryConnective show_ symbol exp1 exp2 = + '(' : show_ exp1 ++ " " ++ symbol ++ " " ++ show_ exp2 ++ ")" + +showBC :: String -> Expr -> Expr -> String +showBC = showBinaryConnective show + +showBCA :: String -> Expr -> Expr -> String +showBCA = showBinaryConnective showAscii diff --git a/src/Data/Logic/Propositional/Parser.hs b/src/Data/Logic/Propositional/Parser.hs new file mode 100644 --- /dev/null +++ b/src/Data/Logic/Propositional/Parser.hs @@ -0,0 +1,74 @@ +{-# OPTIONS_GHC -fno-warn-unused-do-bind #-} +{-# OPTIONS_HADDOCK hide #-} + +module Data.Logic.Propositional.Parser + ( parseExpr + ) where + +import Data.Logic.Propositional.Core (Expr (..)) + +import Text.ParserCombinators.Parsec + (char, choice, eof, oneOf, parse, spaces, string) + +import Text.ParserCombinators.Parsec.Error (ParseError) +import Text.ParserCombinators.Parsec.Pos (SourceName) +import Text.ParserCombinators.Parsec.Prim (GenParser) + +-- | The 'parseExpr' function accepts the name of a source, and a string to be +-- parsed, and attempts to parse the string as a logical expression of the +-- following forms, where @φ@ and @ψ@ are metalinguistic variables +-- standing for any valid expression. +-- +-- * Variables: @\"P\"@, @\"Q\"@, @\"R\"@ etc.; basically anything in the +-- character class @[A-Z]@ +-- +-- * Negation: @\"~φ\"@ +-- +-- * Conjunction: @\"(φ & ψ)\"@ +-- +-- * Disjunction: @\"(φ | ψ)\"@ +-- +-- * Conditional: @\"(φ -> ψ)\"@ +-- +-- * Biconditional: @\"(φ \<-> ψ)\"@ +parseExpr :: SourceName -> String -> Either ParseError Expr +parseExpr = parse statement + +statement :: GenParser Char st Expr +statement = do spaces + x <- expr + spaces + eof + return x + +expr :: GenParser Char st Expr +expr = choice [binaryP, negation, variable] + +variable :: GenParser Char st Expr +variable = do c <- oneOf ['A'..'Z'] + return $ Variable [c] + +negation :: GenParser Char st Expr +negation = do char '~' + x <- expr + return $ Negation x + +binaryP :: GenParser Char st Expr +binaryP = do char '(' + x <- binary + char ')' + return x + +binary :: GenParser Char st Expr +binary = do x1 <- expr + spaces + s <- choice [string "&", string "|", string "->", string "<->"] + spaces + x2 <- expr + return $ connective s x1 x2 + where + connective "&" = Conjunction + connective "|" = Disjunction + connective "->" = Conditional + connective "<->" = Biconditional + connective _ = error "Impossible case" diff --git a/src/Data/Logic/Propositional/Tables.hs b/src/Data/Logic/Propositional/Tables.hs new file mode 100644 --- /dev/null +++ b/src/Data/Logic/Propositional/Tables.hs @@ -0,0 +1,30 @@ +{-# OPTIONS_HADDOCK hide #-} + +module Data.Logic.Propositional.Tables + ( truthTable + ) where + +import Data.Logic.Propositional.Core + +import Data.Map (fold) + +-- | The 'truthTable' function produces a truth table for the given expression. +truthTable :: Expr -> String +truthTable expr = unlines [header, separator, body] + where + header = unwords vs ++ " | " ++ show expr + body = unlines $ map (showAssignment expr) as + separator = concat $ replicate sepLength "-" + sepLength = length vs * 2 + length (show expr) + 2 + as = assignments expr + vs = variables expr + +showAssignment :: Expr -> Mapping -> String +showAssignment expr a = showVarValues ++ " | " ++ showExprValue + where + showVarValues = unwords $ fold ((:) . showBool) [] a + showExprValue = showBool $ interpret expr a + +showBool :: Bool -> String +showBool True = "T" +showBool False = "F" diff --git a/src/hatt.hs b/src/hatt.hs new file mode 100644 --- /dev/null +++ b/src/hatt.hs @@ -0,0 +1,31 @@ +{-# LANGUAGE DeriveDataTypeable #-} + +module Main + ( main + ) where + +import Data.Logic.Propositional + +import System.Console.CmdArgs + +data HattOpts = HattOpts + { evaluate :: String + } deriving (Show, Data, Typeable) + +hattOpts :: HattOpts +hattOpts = HattOpts + { evaluate = def &= opt "" &= typ "EXPRESSION" + &= help "Print the truth table for the given expression" + } &= summary "Hatt 0.1, (c) Benedict Eastaugh 2011" + &= program "hatt" + +main :: IO () +main = do opts <- cmdArgs hattOpts + case evaluate opts of + "" -> putStrLn "Try using the --evaluate[=EXPRESSION] flag" + expr -> putStr (eval expr) + +eval :: String -> String +eval str = case parseExpr "" str of + Left err -> "parse error at " ++ show err ++ "\n" + Right expr -> truthTable expr