From e46bcf6ddc56dcc07d5a93c00f5dd136827771e8 Mon Sep 17 00:00:00 2001
From: hi <hi>
Date: Tue, 12 Aug 2025 05:21:15 +0000
Subject: [PATCH] nice readme, rename M to MIU system

---
 Logic/Language.hs                    |  1 +
 Logic/Language/Impl/{M.hs => MIU.hs} | 20 ++++++-------
 readme.md                            | 43 +++++++++++++++++++++++++---
 3 files changed, 50 insertions(+), 14 deletions(-)
 rename Logic/Language/Impl/{M.hs => MIU.hs} (83%)

diff --git a/Logic/Language.hs b/Logic/Language.hs
index a12a46f..78c6a40 100644
--- a/Logic/Language.hs
+++ b/Logic/Language.hs
@@ -6,6 +6,7 @@ instance Show a => Show (ConcatShowList a) where
   show (ConcatShowList xs) = concat $ map show xs
 
 -- Formal language (/grammar/production system/whatever)
+-- https://en.wikipedia.org/wiki/Post_canonical_system
 class (Eq symbol, Show symbol) => Language symbol where
   isWellFormed :: [symbol] -> Bool
 
diff --git a/Logic/Language/Impl/M.hs b/Logic/Language/Impl/MIU.hs
similarity index 83%
rename from Logic/Language/Impl/M.hs
rename to Logic/Language/Impl/MIU.hs
index be883a7..9b52411 100644
--- a/Logic/Language/Impl/M.hs
+++ b/Logic/Language/Impl/MIU.hs
@@ -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 $
diff --git a/readme.md b/readme.md
index d841c09..ff28f2a 100644
--- a/readme.md
+++ b/readme.md
@@ -1,18 +1,53 @@
-Statement logic !!!
+# statement logic !!!
 
-# Compile it
+things you can do with this:
+
+### general things
+
+- parse string -> statement
+- parse L (the formal language) string -> statement
+- serialize a statement to plaintext, LaTeX, L (the formal language)
+
+### semantic things (statements have meaning I guess)
+
+- evaluate statements
+- from a statement generate a LaTeX truth table
+- match/replace patterns in statements (e.g. logical laws)
+- verify logical-law equivalence of statements (TODO)
+- find logical-law equivalence of statements with breadth-first search
+
+### syntactic things (statements are strings of symbols)
+
+- implement formal languages (symbols, axioms schemas, and inference rules):
+  <https://en.wikipedia.org/wiki/Post_canonical_system>
+- verify derivations in formal languages
+
+### formal languages implemented
+
+- the MIU system (from "Gödel, Escher, Bach")
+- L
+
+## Requirements
+
+a haskell compiler e.g. GHC
+
+## Compile it
 
 ```sh
 make
 ```
 
-# Usage
+or look in `Makefile`
+
+## Usage
+
+only this has been implemented in the main function:
 
 ```sh
 echo '((p->q)<->(!q->!p))' | ./logic
 ```
 
-## Output
+### Output
 
 ```
 Iff (Implies (Atom "p") (Atom "q")) (Implies (Not (Atom "q")) (Not (Atom "p")))