85 lines
2 KiB
Haskell
85 lines
2 KiB
Haskell
module Logic.Language.Impl.MIU where
|
|
|
|
import Logic.Language (Language(..), ConcatShowList(..))
|
|
import Logic.Language.Derivation (Derivation(..))
|
|
|
|
-- The MIU system
|
|
-- (from "Gödel, Escher, Bach: An Eternal Golden Braid" by Douglas Hofstadter)
|
|
data AlphaMIU
|
|
= M
|
|
| I
|
|
| U
|
|
deriving Show
|
|
|
|
type StringMIU = [AlphaMIU]
|
|
|
|
instance Language AlphaMIU where
|
|
isWellFormed (M:_) = True
|
|
isWellFormed _ = False
|
|
|
|
axiom0 = [[M, I]]
|
|
infer1 =
|
|
[ miuRule1
|
|
, miuRule2
|
|
, miuRule3
|
|
, miuRule4
|
|
]
|
|
|
|
-- RULE I: If you possess a string whose last letter is I, you can add on a U at the end.
|
|
miuRule1 :: StringMIU -> [StringMIU]
|
|
miuRule1 [I] = [[I, U]]
|
|
miuRule1 (x:xs) = (x:) <$> miuRule1 xs
|
|
miuRule1 _ = []
|
|
|
|
-- RULE II: Suppose you have Mx. Then you may add Mxx to your collection.
|
|
miuRule2 :: StringMIU -> [StringMIU]
|
|
miuRule2 string@(M:xs) = [string ++ xs]
|
|
miuRule2 _ = []
|
|
|
|
-- 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.
|
|
miuRule3 :: StringMIU -> [StringMIU]
|
|
miuRule3 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 _ = []
|
|
miuRule3 _ = []
|
|
|
|
-- RULE IV: If UU occurs inside one of your strings, you can drop it.
|
|
miuRule4 :: StringMIU -> [StringMIU]
|
|
miuRule4 string@(M:xs) = (M:) <$> aux xs
|
|
where
|
|
aux (x@U:xs@(U:xs')) = xs':((x:) <$> aux xs)
|
|
aux (x:xs) = (x:) <$> aux xs
|
|
aux _ = []
|
|
miuRule4 _ = []
|
|
|
|
{-
|
|
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 AlphaMIU
|
|
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> ConcatShowList <$> resolveDerivation deriveMIIUII
|
|
Right MIIUII
|
|
-}
|