62 lines
1.5 KiB
Haskell
62 lines
1.5 KiB
Haskell
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
|
|
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 Seq infer0 :: [Seq AlphaM]
|
|
[MI]
|
|
ghci> map Seq $ concat $ map ($ [M, I, I, I, I, U, U, I]) infer1
|
|
[MIIIIUUIU,MIIIIUUIIIIIUUI,MUIUUI,MIUUUI,MIIIII]
|
|
-}
|