From bf846e32ce2a68c7a6917c5054f5cc73fde143ed Mon Sep 17 00:00:00 2001 From: hi Date: Fri, 29 Aug 2025 12:53:28 +0000 Subject: [PATCH] predicate logic --- lib/Logic/Parse.hs | 3 + lib/Logic/Predicate/Bounded.hs | 226 +++++++++++++++++++++++++++++++++ lib/Logic/Predicate/Illegal.hs | 20 +++ logic.cabal | 2 + readme.md | 2 + 5 files changed, 253 insertions(+) create mode 100644 lib/Logic/Predicate/Bounded.hs create mode 100644 lib/Logic/Predicate/Illegal.hs diff --git a/lib/Logic/Parse.hs b/lib/Logic/Parse.hs index ada6a68..e344ab1 100644 --- a/lib/Logic/Parse.hs +++ b/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 diff --git a/lib/Logic/Predicate/Bounded.hs b/lib/Logic/Predicate/Bounded.hs new file mode 100644 index 0000000..7984a7a --- /dev/null +++ b/lib/Logic/Predicate/Bounded.hs @@ -0,0 +1,226 @@ +module Logic.Predicate.Bounded where + +import Control.Applicative (many, some, empty) +import Data.Char (isAlphaNum, isNumber) +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 diff --git a/lib/Logic/Predicate/Illegal.hs b/lib/Logic/Predicate/Illegal.hs new file mode 100644 index 0000000..3478550 --- /dev/null +++ b/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 diff --git a/logic.cabal b/logic.cabal index 7904d07..24f7e4e 100644 --- a/logic.cabal +++ b/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 diff --git a/readme.md b/readme.md index 0a29d97..62c3efe 100644 --- a/readme.md +++ b/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