formal language derivations

Logic/Language.hs

@@ -1,6 +1,9 @@
 module Logic.Language where
 
-type List a = [a]
+-- Convenience newtype so strings of symbols are less ugly
+newtype ConcatShowList symbol = ConcatShowList [symbol]
+instance Show a => Show (ConcatShowList a) where
+  show (ConcatShowList xs) = concat $ map show xs
 
 -- Formal language (/grammar/production system/whatever)
 class (Eq symbol, Show symbol) => Language symbol where
@@ -9,24 +12,28 @@ class (Eq symbol, Show symbol) => Language symbol where
   -- If Haskell had dependent types these could be generalized.
 
   -- axiomN : N wffs -> theorem
-  axiom0 :: [[symbol]]
-  axiom1 :: [[symbol] -> [symbol]]
-  axiom2 :: [[symbol] -> [symbol] -> [symbol]]
-  axiom3 :: [[symbol] -> [symbol] -> [symbol] -> [symbol]]
-
-  -- inferN : N theorems -> theorem
-  -- (axiom0 and infer0 would mean the same thing.)
-  infer1 :: [[symbol] -> List [symbol]]
-  infer2 :: [[symbol] -> [symbol] -> List [symbol]]
+  axiom0 :: [TypeAxiom0 symbol]
+  axiom1 :: [TypeAxiom1 symbol]
+  axiom2 :: [TypeAxiom2 symbol]
+  axiom3 :: [TypeAxiom3 symbol]
 
   axiom0 = []
   axiom1 = []
   axiom2 = []
   axiom3 = []
+
+  -- inferN : N theorems -> theorem
+  -- (axiom0 and infer0 would mean the same thing.)
+  infer1 :: [TypeInfer1 symbol]
+  infer2 :: [TypeInfer2 symbol]
+
   infer1 = []
   infer2 = []
 
--- Convenience newtype so strings are less ugly
-newtype Seq symbol = Seq [symbol]
-instance Show a => Show (Seq a) where
-  show (Seq xs) = concat $ map show xs
+type TypeAxiom0 s = [s]
+type TypeAxiom1 s = [s] -> [s]
+type TypeAxiom2 s = [s] -> [s] -> [s]
+type TypeAxiom3 s = [s] -> [s] -> [s] -> [s]
+
+type TypeInfer1 s = [s] -> [[s]]
+type TypeInfer2 s = [s] -> [s] -> [[s]]

Logic/Language/Derivation.hs

@@ -0,0 +1,93 @@
+module Logic.Language.Derivation where
+
+import Logic.Language (Language(..))
+
+data Derivation symbol
+  = Axiom0 Integer
+  | Axiom1 Integer [symbol]
+  | Axiom2 Integer [symbol] [symbol]
+  | Axiom3 Integer [symbol] [symbol] [symbol]
+  | Infer1 Integer Integer (Derivation symbol)
+  | Infer2 Integer Integer (Derivation symbol) (Derivation symbol)
+  deriving (Eq, Show)
+
+data DerivationError s
+  = SelectIndexError (DerivationSelectIndexError s)
+  | ResultIndexError (DerivationResultIndexError s)
+  | NotWellFormed [s]
+  deriving Show
+
+data DerivationSelectIndexError s = DerivationSelectIndexError
+  { dserrSelectPlace :: DerivationSelectIndexErrorPlace
+  , dserrSelectErrorIndex :: Integer
+  , dserrSize :: Int
+  , dserrWffs :: [[s]]
+  } deriving Show
+
+data DerivationSelectIndexErrorPlace
+  = AxiomSelect
+  | InferSelect
+  deriving Show
+
+data DerivationResultIndexError s = DerivationResultIndexError
+  { drerrPlace :: DerivationResultIndexErrorPlace
+  , drerrSelectIndex :: Integer
+  , drerrResultIndex :: Integer
+  , drerrResult :: [[s]]
+  , drerrTheorems :: [[s]]
+  } deriving Show
+
+data DerivationResultIndexErrorPlace
+  = InferResult
+  deriving Show
+
+resolveDerivation :: Language s => Derivation s -> Either (DerivationError s) [s]
+resolveDerivation derivation =
+  case derivation of
+    (Axiom0 index) -> trySelect AxiomSelect axiom0 index []
+    (Axiom1 index wff1)
+      | not $ isWellFormed wff1 -> Left $ NotWellFormed wff1
+      | otherwise -> do
+        rule <- trySelect AxiomSelect axiom1 index [wff1]
+        return $ rule wff1
+    (Axiom2 index wff1 wff2)
+      | not $ isWellFormed wff1 -> Left $ NotWellFormed wff1
+      | not $ isWellFormed wff2 -> Left $ NotWellFormed wff2
+      | otherwise -> do
+        rule <- trySelect AxiomSelect axiom2 index [wff1, wff2]
+        return $ rule wff1 wff2
+    (Axiom3 index wff1 wff2 wff3)
+      | not $ isWellFormed wff1 -> Left $ NotWellFormed wff1
+      | not $ isWellFormed wff2 -> Left $ NotWellFormed wff2
+      | not $ isWellFormed wff3 -> Left $ NotWellFormed wff3
+      | otherwise -> do
+        rule <- trySelect AxiomSelect axiom3 index [wff1, wff2, wff3]
+        return $ rule wff1 wff2 wff3
+    (Infer1 selectIndex resultIndex deriv1) -> do
+      theorem1 <- resolveDerivation deriv1
+      rule <- trySelect InferSelect infer1 selectIndex [theorem1]
+      let result = rule theorem1
+      tryResult InferResult selectIndex resultIndex result [theorem1]
+    (Infer2 selectIndex resultIndex deriv1 deriv2) -> do
+      theorem1 <- resolveDerivation deriv1
+      theorem2 <- resolveDerivation deriv2
+      rule <- trySelect InferSelect infer2 selectIndex [theorem1, theorem2]
+      let result = rule theorem1 theorem2
+      tryResult InferResult selectIndex resultIndex result [theorem1, theorem2]
+  where
+    trySelect place list index wffs = maybe
+      (Left $ SelectIndexError $ DerivationSelectIndexError place index (length list) wffs)
+      Right $
+      get index list
+
+    tryResult place selectIndex resultIndex list theorems = maybe
+      (Left $ ResultIndexError $ DerivationResultIndexError place selectIndex resultIndex list theorems)
+      Right $
+      get resultIndex list
+
+    get :: Integer -> [a] -> Maybe a
+    get 0 (x:xs) = Just x
+    get index [] = Nothing
+    get index (x:xs)
+      | index >= 1 = get (index - 1) xs
+      | otherwise = Nothing

Logic/Language/Impl/M.hs

@@ -1,6 +1,7 @@
 module Logic.Language.M where
 
-import Logic.Language (Language(..), Seq(..))
+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)
@@ -40,7 +41,7 @@ mRule2 _ = []
 mRule3 :: StringM -> [StringM]
 mRule3 string@(M:xs) = (M:) <$> aux xs
   where
-    aux (I:xs@(I:I:xs')) = (U:xs'):((I:) <$> aux xs)
+    aux (x@I:xs@(I:I:xs')) = (U:xs'):((x:) <$> aux xs)
     aux (x:xs) = (x:) <$> aux xs
     aux _  = []
 mRule3 _ = []
@@ -49,14 +50,36 @@ mRule3 _ = []
 mRule4 :: StringM -> [StringM]
 mRule4 string@(M:xs) = (M:) <$> aux xs
   where
-    aux (U:U:xs) = [xs]
+    aux (x@U:xs@(U:xs')) = xs':((x:) <$> aux xs)
     aux (x:xs) = (x:) <$> aux xs
     aux _ = []
 mRule4 _ = []
 
 {-
-ghci> map Seq infer0 :: [Seq AlphaM]
+ghci> map ConcatShowList infer0 :: [ConcatShowList AlphaM]
 [MI]
-ghci> map Seq $ concat $ map ($ [M, I, I, I, I, U, U, I]) infer1
+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]
+-}