diff --git a/Logic/Language.hs b/Logic/Language.hs new file mode 100644 index 0000000..6be2b16 --- /dev/null +++ b/Logic/Language.hs @@ -0,0 +1,15 @@ +module Logic.Language where + +-- Formal language (/grammar/production system/whatever) +class (Eq symbol, Show symbol) => Language symbol where + -- If Haskell had dependent types this could be generalized. + -- For now the languages I want to make use at most up to infer3. + infer0 :: [[symbol]] + infer1 :: [[symbol] -> [[symbol]]] + infer2 :: [[symbol] -> [symbol] -> [[symbol]]] + infer3 :: [[symbol] -> [symbol] -> [symbol] -> [[symbol]]] + +-- 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 diff --git a/Logic/Language/M.hs b/Logic/Language/M.hs new file mode 100644 index 0000000..5d4aa24 --- /dev/null +++ b/Logic/Language/M.hs @@ -0,0 +1,61 @@ +module Logic.Language.M where + +import Logic.Language (Language(..), Seq(..)) + +-- 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 + infer0 = [[M, I]] + infer1 = + [ mRule1 + , mRule2 + , mRule3 + , mRule4 + ] + infer2 = [] + infer3 = [] + +-- 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 (I:xs@(I:I:xs')) = (U:xs'):((I:) <$> 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 (U:U:xs) = [xs] + aux (x:xs) = (x:) <$> aux xs + aux _ = [] +mRule4 _ = [] + +{- +ghci> map Seq infer0 :: [Seq AlphaM] +[MI] +ghci> map Seq $ concat $ map ($ [M, I, I, I, I, U, U, I]) infer1 +[MIIIIUUIU,MIIIIUUIIIIIUUI,MUIUUI,MIUUUI,MIIIII] +-}