nice readme, rename M to MIU system

This commit is contained in:
hi 2025-08-12 05:21:15 +00:00
parent b28263fdc3
commit e46bcf6ddc
3 changed files with 50 additions and 14 deletions

View file

@ -3,17 +3,17 @@ module Logic.Language.Impl.M where
import Logic.Language (Language(..), ConcatShowList(..))
import Logic.Language.Derivation (Derivation(..))
-- The language M
-- The MIU system
-- (from "Gödel, Escher, Bach: An Eternal Golden Braid" by Douglas Hofstadter)
data AlphaM
data AlphaMIU
= M
| I
| U
deriving (Eq, Show)
type StringM = [AlphaM]
type StringMIU = [AlphaMIU]
instance Language AlphaM where
instance Language AlphaMIU where
isWellFormed (M:_) = True
isWellFormed _ = False
@ -26,19 +26,19 @@ instance Language AlphaM where
]
-- 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 :: StringMIU -> [StringMIU]
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 :: StringMIU -> [StringMIU]
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 :: StringMIU -> [StringMIU]
mRule3 string@(M:xs) = (M:) <$> aux xs
where
aux (x@I:xs@(I:I:xs')) = (U:xs'):((x:) <$> aux xs)
@ -47,7 +47,7 @@ mRule3 string@(M:xs) = (M:) <$> aux xs
mRule3 _ = []
-- RULE IV: If UU occurs inside one of your strings, you can drop it.
mRule4 :: StringM -> [StringM]
mRule4 :: StringMIU -> [StringMIU]
mRule4 string@(M:xs) = (M:) <$> aux xs
where
aux (x@U:xs@(U:xs')) = xs':((x:) <$> aux xs)
@ -56,13 +56,13 @@ mRule4 string@(M:xs) = (M:) <$> aux xs
mRule4 _ = []
{-
ghci> map ConcatShowList infer0 :: [ConcatShowList AlphaM]
ghci> map ConcatShowList infer0 :: [ConcatShowList AlphaMIU]
[MI]
ghci> map ConcatShowList $ concat $ map ($ [M, I, I, I, I, U, U, I]) infer1
[MIIIIUUIU,MIIIIUUIIIIIUUI,MUIUUI,MIUUUI,MIIIII]
-}
deriveMIIUII :: Derivation AlphaM
deriveMIIUII :: Derivation AlphaMIU
deriveMIIUII =
Infer1 3 0 $
Infer1 2 2 $