predicate logic

lib/Logic/Parse.hs

@@ -88,3 +88,6 @@ parseIf description check = Parser $ \input@(Input pos xs) ->
     (char:chars)
       | check char -> Right $ (char,) $ Input (pos + 1) chars
       | otherwise -> Left $ expected description input
+
+parseFail :: Show s => String -> Parser s a
+parseFail thing = Parser $ \input -> Left $ expected thing input

lib/Logic/Predicate/Bounded.hs

@@ -0,0 +1,227 @@
+module Logic.Predicate.Bounded where
+
+import Control.Applicative (many, some, empty, (<|>))
+import Data.Char (isAlphaNum, isNumber)
+import Data.Either (fromRight)
+import Data.List (intercalate)
+
+import Logic.Parse
+
+-- I'm calling this Formula not Predicate.  If I did
+-- call it Predicate there would be a nice correspondence
+-- with the statement logic implementation because the
+-- main type there is called Statement.  But predicates
+-- are relations not statements.
+data Formula
+  = Not     Formula
+  | Or      Formula Formula
+  | And     Formula Formula
+  | Implies Formula Formula
+  | Iff     Formula Formula
+  | Forall String Formula
+  | Exists String Formula
+  | Predicate String PredicateArgs
+  deriving (Eq, Show)
+
+data PredicateArgs
+  = PredicateArgs0
+  | PredicateArgs1 Term
+  | PredicateArgs2 Term Term
+  | PredicateArgs3 Term Term Term
+  deriving (Eq, Show)
+
+data Term
+  = Variable String
+  | Function String FunctionArgs
+  deriving (Eq, Show)
+
+data FunctionArgs
+  = FunctionArgs0
+  | FunctionArgs1 Term
+  | FunctionArgs2 Term Term
+  deriving (Eq, Show)
+
+-- "@forall x. @forall y. %leq.2 add.2 $x $y mul.2 $x $y"
+formulaExample1 :: Formula
+formulaExample1 = Forall "x" $ Forall "y" $ Predicate "leq" $ PredicateArgs2 addXY mulXY
+  where
+    addXY = Function "add" $ FunctionArgs2 (Variable "x") (Variable "y")
+    mulXY = Function "mul" $ FunctionArgs2 (Variable "x") (Variable "y")
+
+-- "@forall x. !%equal.2 succ.1 $x zero.0"
+formulaExample2 :: Formula
+formulaExample2 = Forall "x" $ Not $ Predicate "equal" $ PredicateArgs2 succX zero
+  where
+    succX = Function "succ" $ FunctionArgs1 (Variable "x")
+    zero = Function "zero" FunctionArgs0
+
+-- "!@exists n. (%prime.1 $n && %leq.2 $n zero.0)"
+formulaExample3 :: Formula
+formulaExample3 = Not $ Exists "n" $ And nPrime nLeqZero
+  where
+    nPrime = Predicate "prime" $ PredicateArgs1 (Variable "n")
+    nLeqZero = Predicate "leq" $ PredicateArgs2 (Variable "n") zero
+    zero = Function "zero" FunctionArgs0
+
+serializeFormula :: Formula -> String
+serializeFormula = whitespace . aux
+  where
+    aux (Not p) = ["!" <> serializeFormula p]
+    aux (Or      p1 p2) = binary "||"   p1 p2
+    aux (And     p1 p2) = binary "&&"   p1 p2
+    aux (Implies p1 p2) = binary "->"  p1 p2
+    aux (Iff     p1 p2) = binary "<->" p1 p2
+    aux (Forall name p) = ["@forall", name <> "."] <> aux p
+    aux (Exists name p) = ["@exists", name <> "."] <> aux p
+    aux (Predicate name args) = aux' name args
+
+    aux' name PredicateArgs0 =
+      [ "%" <> name <> ".0"
+      ]
+    aux' name (PredicateArgs1 p1) =
+      [ "%" <> name <> ".1"
+      , serializeTerm p1
+      ]
+    aux' name (PredicateArgs2 p1 p2) =
+      [ "%" <> name <> ".2"
+      , serializeTerm p1
+      , serializeTerm p2
+      ]
+    aux' name (PredicateArgs3 p1 p2 p3) =
+      [ "%" <> name <> ".3"
+      , serializeTerm p1
+      , serializeTerm p2
+      , serializeTerm p3
+      ]
+
+    binary sep p1 p2 = ["("] <> aux p1 <> [sep] <> aux p2 <> [")"]
+
+    whitespace [] = ""
+    whitespace [x] = x
+    whitespace ("(":xs) = "(" <> whitespace xs
+    whitespace (x:")":xs) = x <> ")" <> whitespace xs
+    whitespace (x:xs) = x <> " " <> whitespace xs
+
+serializeTerm :: Term -> String
+serializeTerm = aux
+  where
+    aux (Variable name) = "$" <> name
+    aux (Function name args) = aux' name args
+
+    aux' name FunctionArgs0 = name <> ".0"
+    aux' name (FunctionArgs1 term1) = intercalate " "
+      [ name <> ".1"
+      , serializeTerm term1
+      ]
+    aux' name (FunctionArgs2 term1 term2) = intercalate " "
+      [ name <> ".2"
+      , serializeTerm term1
+      , serializeTerm term2
+      ]
+
+isNameChar :: Char -> Bool
+isNameChar char = isAlphaNum char || char == '_'
+
+parseTerm :: Parser Char Term
+parseTerm = Parser $ \input -> (flip runParser) input $
+    case inputSeq input of
+      ('$':_) -> parseVariable
+      (char:_)
+        | isNameChar char -> parseFunction
+        | otherwise -> parseFail "term"
+      _ -> parseFail "term"
+  where
+    parseVariable = do
+      _ <- parseToken "$"
+      name <- some $ parseIf "variable name" isNameChar
+      return $ Variable name
+
+    parseFunction = do
+      name <- some $ parseIf "function name" isNameChar
+      _ <- parseToken "."
+      arity <- some $ parseIf "function arity" isNumber
+      case arity of
+        "0" -> do
+          return $ Function name FunctionArgs0
+
+        "1" -> do
+          arg1 <- some (parseToken " ") *> parseTerm
+          return $ Function name $ FunctionArgs1 arg1
+
+        "2" -> do
+          arg1 <- some (parseToken " ") *> parseTerm
+          arg2 <- some (parseToken " ") *> parseTerm
+          return $ Function name $ FunctionArgs2 arg1 arg2
+
+        _ -> parseFail "function arity less than 3"
+
+parseFormula :: Parser Char Formula
+parseFormula = Parser $ \input -> (flip runParser) input $
+  case inputSeq input of
+    ('%':_) -> parsePredicate
+    ('@':'f':_) -> parseQuantifier "@forall" Forall
+    ('@':'e':_) -> parseQuantifier "@exists" Exists
+    ('!':_) -> parseNot
+    ('(':_) -> parseBinary
+    _ -> parseFail "predicate"
+  where
+    parsePredicate = do
+      _ <- parseToken "%"
+      name <- some $ parseIf "relation name" isNameChar
+      _ <- parseToken "."
+      arity <- some $ parseIf "relation arity" isNumber
+      case arity of
+        "0" -> do
+          return $ Predicate name PredicateArgs0
+
+        "1" -> do
+          arg1 <- some (parseToken " ") *> parseTerm
+          return $ Predicate name $ PredicateArgs1 arg1
+
+        "2" -> do
+          arg1 <- some (parseToken " ") *> parseTerm
+          arg2 <- some (parseToken " ") *> parseTerm
+          return $ Predicate name $ PredicateArgs2 arg1 arg2
+
+        "3" -> do
+          arg1 <- some (parseToken " ") *> parseTerm
+          arg2 <- some (parseToken " ") *> parseTerm
+          arg3 <- some (parseToken " ") *> parseTerm
+          return $ Predicate name $ PredicateArgs3 arg1 arg2 arg3
+
+        _ -> parseFail "relation arity less than 4"
+
+    parseQuantifier token ctor = do
+      _ <- parseToken token
+      _ <- some $ parseToken " "
+      name <- some $ parseIf "variable name" isNameChar
+      _ <- parseToken "."
+      _ <- many $ parseToken " "
+      p <- parseFormula
+      return $ ctor name p
+
+    parseNot = do
+      p <- parseToken "!" *> parseFormula
+      return $ Not p
+
+    parseBinary = do
+      _ <- parseToken "("
+      _ <- many $ parseToken " "
+      p1 <- parseFormula
+      _ <- many $ parseToken " "
+      sep <- some $ parseIf "connective" (/= ' ')
+      case
+        case sep of
+          "&&" -> Just And
+          "||" -> Just Or
+          "->" -> Just Implies
+          "<->" -> Just Iff
+          _ -> Nothing
+        of
+          Nothing -> parseFail "connective"
+          Just ctor -> do
+            _ <- many $ parseToken " "
+            p2 <- parseFormula
+            _ <- many $ parseToken " "
+            _ <- parseToken ")"
+            return $ ctor p1 p2

lib/Logic/Predicate/Illegal.hs

@@ -0,0 +1,20 @@
+module Logic.Predicate.Illegal where
+
+-- some illegal states are representable
+-- e.g. a function with arity 2 having 3 arguments
+
+data Formula
+  = Not Formula
+  | Or Formula Formula
+  | And Formula Formula
+  | Implies Formula Formula
+  | Iff Formula Formula
+  | Forall String Formula
+  | Exists String Formula
+  | Predicate String [Term]
+  deriving Show
+
+data Term
+  = Variable String
+  | Function String [Term]
+  deriving Show

logic.cabal

@@ -22,6 +22,8 @@ library
         Logic.Language.Impl.L
         Logic.Language.Impl.MIU
         Logic.Parse
+        Logic.Predicate.Illegal
+        Logic.Predicate.Bounded
         Logic.Statement
         Logic.Statement.Eval
         Logic.Statement.Laws

readme.md

@@ -1,5 +1,7 @@
 # statement logic !!!
 
+(and predicate logic too)
+
 see [lib/Logic/readme.md](lib/Logic) for more details about what's here
 
 ## requirements