Logic/Language.hs

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

Logic/Language/Derivation.hs

@@ -1,93 +0,0 @@
-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/M.hs

@@ -1,7 +1,6 @@
 module Logic.Language.M where
 
-import Logic.Language (Language(..), ConcatShowList(..))
+import Logic.Language (Language(..), Seq(..))
-import Logic.Language.Derivation (Derivation(..))
 
 -- The language M
 -- (from "Gödel, Escher, Bach: An Eternal Golden Braid" by Douglas Hofstadter)
@@ -41,7 +40,7 @@ mRule2 _ = []
 mRule3 :: StringM -> [StringM]
 mRule3 string@(M:xs) = (M:) <$> aux xs
   where
-    aux (x@I:xs@(I:I:xs')) = (U:xs'):((x:) <$> aux xs)
+    aux (I:xs@(I:I:xs')) = (U:xs'):((I:) <$> aux xs)
     aux (x:xs) = (x:) <$> aux xs
     aux _  = []
 mRule3 _ = []
@@ -50,36 +49,14 @@ mRule3 _ = []
 mRule4 :: StringM -> [StringM]
 mRule4 string@(M:xs) = (M:) <$> aux xs
   where
-    aux (x@U:xs@(U:xs')) = xs':((x:) <$> aux xs)
+    aux (U:U:xs) = [xs]
     aux (x:xs) = (x:) <$> aux xs
     aux _ = []
 mRule4 _ = []
 
 {-
-ghci> map ConcatShowList infer0 :: [ConcatShowList AlphaM]
+ghci> map Seq infer0 :: [Seq AlphaM]
 [MI]
-ghci> map ConcatShowList $ concat $ map ($ [M, I, I, I, I, U, U, I]) infer1
+ghci> map Seq $ 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]
--}