formal language derivations

Logic/Language/Impl/L.hs

@@ -0,0 +1,143 @@
+module Logic.Language.L where
+
+import Logic.Language (Language(..), Seq(..))
+import Logic.Statement (Statement(..))
+import Logic.Parse
+  ( Parser(..)
+  , ParseError
+  , Input(..)
+  , eof
+  , expected
+  , mkInput
+  , parseToken
+  )
+
+import Control.Applicative (Alternative((<|>)))
+import Data.Either (isRight)
+import Data.Maybe (fromJust, maybeToList)
+import Text.Read (readMaybe)
+
+-- The language L
+data AlphaL
+  = Arrow
+  | Tilde
+  | Open
+  | Close
+  | Variable Integer
+  deriving (Eq, Show)
+
+type StringL = [AlphaL]
+
+instance Language AlphaL where
+  isWellFormed string = isRight $ eof parseL $ mkInput string
+
+  axiom2 = [lAxiom1, lAxiom3]
+  axiom3 = [lAxiom2]
+  infer2 = [lRule1]
+
+-- (A → (B → A))
+lAxiom1 :: StringL -> StringL -> StringL
+lAxiom1 wff1 wff2 =
+  [Open] ++
+    wff1 ++
+  [Arrow] ++
+    [Open] ++ wff2 ++ [Arrow] ++ wff1 ++ [Close] ++
+  [Close]
+
+-- ((A → (B → C)) → ((A → B) → (A → C)))
+lAxiom2 :: StringL -> StringL -> StringL -> StringL
+lAxiom2 wff1 wff2 wff3 =
+  [Open] ++
+    [Open] ++
+      wff1 ++
+    [Arrow] ++
+      [Open] ++ wff2 ++ [Arrow] ++ wff3 ++ [Close] ++
+    [Close] ++
+  [Arrow] ++
+    [Open] ++
+      [Open] ++ wff1 ++ [Arrow] ++ wff2 ++ [Close] ++
+    [Arrow] ++
+      [Open] ++ wff1 ++ [Arrow] ++ wff3 ++ [Close] ++
+    [Close] ++
+  [Close]
+
+-- ((¬A → ¬B) → ((¬A → B) → A))
+lAxiom3 :: StringL -> StringL -> StringL
+lAxiom3 wff1 wff2 =
+  [Open] ++
+    [Open, Tilde] ++ wff1 ++ [Arrow, Tilde] ++ wff2 ++ [Close] ++
+  [Arrow] ++
+    [Open] ++
+      [Open, Tilde] ++ wff1 ++ [Arrow] ++ wff2 ++ [Close] ++
+    [Arrow] ++
+      wff1 ++
+    [Close] ++
+  [Close]
+
+{-
+ghci> import Logic.Statement.Eval (bucket)
+ghci> import Data.Either (fromRight)
+ghci> bucket $ fromRight undefined $ eof parseL $ mkInput $ lAxiom1 [Variable 0] [Variable 1]
+Tautology
+ghci> bucket $ fromRight undefined $ eof parseL $ mkInput $ lAxiom2 [Variable 0] [Variable 1] [Variable 2]
+Tautology
+ghci> bucket $ fromRight undefined $ eof parseL $ mkInput $ lAxiom3 [Variable 0] [Variable 1]
+Tautology
+-}
+
+-- Modus ponens: from (A → B) and A, conclude B.
+lRule1 :: StringL -> StringL -> [StringL]
+lRule1 theorem1 theorem2 = maybeToList $ do
+  s1 <- fromEither $ eof parseL $ mkInput theorem1
+  s2 <- fromEither $ eof parseL $ mkInput theorem2
+  case s1 of
+    Implies s1a s1b
+      | s2 == s1a -> Just $ fromJust $ serializeL s1b
+      | otherwise -> Nothing
+    _ -> Nothing
+  where
+    fromEither = either (const Nothing) Just
+
+{-
+ghci> f x = fromJust $ serializeL $ fromRight undefined $ eof stmt $ mkInput x
+ghci> lRule1 (f "(0->1)") (f "0")
+[[Variable 1]]
+ghci> lRule1 (f "((!0->2)->(!!!!!!!1->1))") (f "(!0->2)")
+[[Open,Tilde,Tilde,Tilde,Tilde,Tilde,Tilde,Tilde,Variable 1,Arrow,Variable 1,Close]]
+ghci> lRule1 (f "((!0->2)->(!!!!!!!1->1))") (f "(!0->3)")
+[]
+-}
+
+parseL :: Parser AlphaL Statement
+parseL = Parser variable <|> Parser tilde <|> arrow <|> fail
+  where
+    variable :: Input AlphaL -> Either ParseError (Statement, Input AlphaL)
+    variable input@(Input pos ((Variable n):xs)) =
+      Right (Atom $ show n, Input (pos + 1) xs)
+    variable input = Left $ expected "statement variable" input
+
+    tilde :: Input AlphaL -> Either ParseError (Statement, Input AlphaL)
+    tilde input@(Input pos (Tilde:xs)) =
+      (\(statement, rest) -> (Not statement, rest)) <$>
+      runParser parseL (Input (pos + 1) xs)
+    tilde input = Left $ expected "negation" input
+
+    arrow :: Parser AlphaL Statement
+    arrow = do
+      parseToken [Open]
+      s1 <- parseL
+      parseToken [Arrow]
+      s2 <- parseL
+      parseToken [Close]
+      return $ Implies s1 s2
+
+    fail :: Parser AlphaL Statement
+    fail = Parser $ \input -> Left $ expected "well-formed formula" input
+
+serializeL :: Statement -> Maybe [AlphaL]
+serializeL (Atom label) = (\x -> [x]) <$> Variable <$> readMaybe label
+serializeL (Not s) = (Tilde:) <$> serializeL s
+serializeL (Implies s1 s2) = do
+  l1 <- serializeL s1
+  l2 <- serializeL s2
+  return $ [Open] ++ l1 ++ [Arrow] ++ l2 ++ [Close]

Logic/Language/Impl/M.hs

@@ -0,0 +1,85 @@
+module Logic.Language.M where
+
+import Logic.Language (Language(..), ConcatShowList(..))
+import Logic.Language.Derivation (Derivation(..))
+
+-- The language M
+-- (from "Gödel, Escher, Bach: An Eternal Golden Braid" by Douglas Hofstadter)
+data AlphaM
+  = M
+  | I
+  | U
+  deriving (Eq, Show)
+
+type StringM = [AlphaM]
+
+instance Language AlphaM where
+  isWellFormed (M:_) = True
+  isWellFormed _ = False
+
+  axiom0 = [[M, I]]
+  infer1 =
+    [ mRule1
+    , mRule2
+    , mRule3
+    , mRule4
+    ]
+
+-- RULE I: If you possess a string whose last letter is I, you can add on a U at the end.
+mRule1 :: StringM -> [StringM]
+mRule1 [I] = [[I, U]]
+mRule1 (x:xs) = (x:) <$> mRule1 xs
+mRule1 _ = []
+
+-- RULE II: Suppose you have Mx. Then you may add Mxx to your collection.
+mRule2 :: StringM -> [StringM]
+mRule2 string@(M:xs) = [string ++ xs]
+mRule2 _ = []
+
+-- RULE III: If III occurs in one of the strings in your collection, you may
+-- make a new string with U in place of III.
+mRule3 :: StringM -> [StringM]
+mRule3 string@(M:xs) = (M:) <$> aux xs
+  where
+    aux (x@I:xs@(I:I:xs')) = (U:xs'):((x:) <$> aux xs)
+    aux (x:xs) = (x:) <$> aux xs
+    aux _  = []
+mRule3 _ = []
+
+-- RULE IV: If UU occurs inside one of your strings, you can drop it.
+mRule4 :: StringM -> [StringM]
+mRule4 string@(M:xs) = (M:) <$> aux xs
+  where
+    aux (x@U:xs@(U:xs')) = xs':((x:) <$> aux xs)
+    aux (x:xs) = (x:) <$> aux xs
+    aux _ = []
+mRule4 _ = []
+
+{-
+ghci> map ConcatShowList infer0 :: [ConcatShowList AlphaM]
+[MI]
+ghci> map ConcatShowList $ concat $ map ($ [M, I, I, I, I, U, U, I]) infer1
+[MIIIIUUIU,MIIIIUUIIIIIUUI,MUIUUI,MIUUUI,MIIIII]
+-}
+
+deriveMIIUII :: Derivation AlphaM
+deriveMIIUII =
+  Infer1 3 0 $
+  Infer1 2 2 $
+  Infer1 0 0 $
+  Infer1 3 0 $
+  Infer1 3 0 $
+  Infer1 2 2 $
+  Infer1 1 0 $
+  Infer1 2 5 $
+  Infer1 0 0 $
+  Infer1 1 0 $
+  Infer1 1 0 $
+  Infer1 1 0 $
+  Axiom0 0
+
+{-
+ghci> import Logic.Language.Derivation (resolveDerivation)
+ghci> resolveDerivation deriveMIIUII
+Right [M,I,I,U,I,I]
+-}