cabal
only doing this because Data.Set is not in the stdlib
This commit is contained in:
hi
parent
30941456a2
commit
dff5b9f365
19 changed files with 101 additions and 16 deletions
97
lib/Logic/Language/Derivation.hs
Normal file
97
lib/Logic/Language/Derivation.hs
Normal file
|
|
@ -0,0 +1,97 @@
|
|||
module Logic.Language.Derivation where
|
||||
|
||||
import Logic.Language (Language(..))
|
||||
|
||||
data Derivation symbol
|
||||
= Hypothesis [symbol]
|
||||
| Axiom0 Integer
|
||||
| Axiom1 Integer [symbol]
|
||||
| Axiom2 Integer [symbol] [symbol]
|
||||
| Axiom3 Integer [symbol] [symbol] [symbol]
|
||||
| Infer1 Integer Integer (Derivation symbol)
|
||||
| Infer2 Integer Integer (Derivation symbol) (Derivation symbol)
|
||||
deriving Show
|
||||
|
||||
data DerivationError s
|
||||
= SelectIndexError (DerivationSelectIndexError s)
|
||||
| ResultIndexError (DerivationResultIndexError s)
|
||||
| NotWellFormed [s]
|
||||
deriving Show
|
||||
|
||||
data DerivationSelectIndexError s = DerivationSelectIndexError
|
||||
{ dserrSelectPlace :: DerivationSelectIndexErrorPlace
|
||||
, dserrSelectErrorIndex :: Integer
|
||||
, dserrSize :: Int
|
||||
, dserrWffs :: [[s]]
|
||||
} deriving Show
|
||||
|
||||
data DerivationSelectIndexErrorPlace
|
||||
= AxiomSelect
|
||||
| InferSelect
|
||||
deriving Show
|
||||
|
||||
data DerivationResultIndexError s = DerivationResultIndexError
|
||||
{ drerrPlace :: DerivationResultIndexErrorPlace
|
||||
, drerrSelectIndex :: Integer
|
||||
, drerrResultIndex :: Integer
|
||||
, drerrResult :: [[s]]
|
||||
, drerrTheorems :: [[s]]
|
||||
} deriving Show
|
||||
|
||||
data DerivationResultIndexErrorPlace
|
||||
= InferResult
|
||||
deriving Show
|
||||
|
||||
resolveDerivation :: Language s => Derivation s -> Either (DerivationError s) [s]
|
||||
resolveDerivation derivation =
|
||||
case derivation of
|
||||
(Hypothesis wff)
|
||||
| not $ isWellFormed wff -> Left $ NotWellFormed wff
|
||||
| otherwise -> Right wff
|
||||
(Axiom0 index) -> trySelect AxiomSelect axiom0 index []
|
||||
(Axiom1 index wff1)
|
||||
| not $ isWellFormed wff1 -> Left $ NotWellFormed wff1
|
||||
| otherwise -> do
|
||||
rule <- trySelect AxiomSelect axiom1 index [wff1]
|
||||
return $ rule wff1
|
||||
(Axiom2 index wff1 wff2)
|
||||
| not $ isWellFormed wff1 -> Left $ NotWellFormed wff1
|
||||
| not $ isWellFormed wff2 -> Left $ NotWellFormed wff2
|
||||
| otherwise -> do
|
||||
rule <- trySelect AxiomSelect axiom2 index [wff1, wff2]
|
||||
return $ rule wff1 wff2
|
||||
(Axiom3 index wff1 wff2 wff3)
|
||||
| not $ isWellFormed wff1 -> Left $ NotWellFormed wff1
|
||||
| not $ isWellFormed wff2 -> Left $ NotWellFormed wff2
|
||||
| not $ isWellFormed wff3 -> Left $ NotWellFormed wff3
|
||||
| otherwise -> do
|
||||
rule <- trySelect AxiomSelect axiom3 index [wff1, wff2, wff3]
|
||||
return $ rule wff1 wff2 wff3
|
||||
(Infer1 selectIndex resultIndex deriv1) -> do
|
||||
theorem1 <- resolveDerivation deriv1
|
||||
rule <- trySelect InferSelect infer1 selectIndex [theorem1]
|
||||
let result = rule theorem1
|
||||
tryResult InferResult selectIndex resultIndex result [theorem1]
|
||||
(Infer2 selectIndex resultIndex deriv1 deriv2) -> do
|
||||
theorem1 <- resolveDerivation deriv1
|
||||
theorem2 <- resolveDerivation deriv2
|
||||
rule <- trySelect InferSelect infer2 selectIndex [theorem1, theorem2]
|
||||
let result = rule theorem1 theorem2
|
||||
tryResult InferResult selectIndex resultIndex result [theorem1, theorem2]
|
||||
where
|
||||
trySelect place list index wffs = maybe
|
||||
(Left $ SelectIndexError $ DerivationSelectIndexError place index (length list) wffs)
|
||||
Right $
|
||||
get index list
|
||||
|
||||
tryResult place selectIndex resultIndex list theorems = maybe
|
||||
(Left $ ResultIndexError $ DerivationResultIndexError place selectIndex resultIndex list theorems)
|
||||
Right $
|
||||
get resultIndex list
|
||||
|
||||
get :: Integer -> [a] -> Maybe a
|
||||
get 0 (x:xs) = Just x
|
||||
get index [] = Nothing
|
||||
get index (x:xs)
|
||||
| index >= 1 = get (index - 1) xs
|
||||
| otherwise = Nothing
|
||||
163
lib/Logic/Language/Impl/L.hs
Normal file
163
lib/Logic/Language/Impl/L.hs
Normal file
|
|
@ -0,0 +1,163 @@
|
|||
module Logic.Language.Impl.L where
|
||||
|
||||
import Logic.Language (Language(..))
|
||||
import Logic.Language.Derivation (Derivation(..))
|
||||
import Logic.Statement (Statement(..))
|
||||
import Logic.Parse
|
||||
( Parser(..)
|
||||
, ParseError
|
||||
, Input(..)
|
||||
, eof
|
||||
, expected
|
||||
, mkInput
|
||||
, parseToken
|
||||
)
|
||||
|
||||
import Control.Applicative (Alternative((<|>)))
|
||||
import Data.Either (isRight)
|
||||
import Data.Maybe (fromJust, maybeToList)
|
||||
import Text.Read (readMaybe)
|
||||
|
||||
-- The language L
|
||||
data AlphaL
|
||||
= Arrow
|
||||
| Tilde
|
||||
| Open
|
||||
| Close
|
||||
| Variable Integer
|
||||
deriving (Eq, Show)
|
||||
|
||||
type StringL = [AlphaL]
|
||||
|
||||
instance Language AlphaL where
|
||||
isWellFormed string = isRight $ eof parseL $ mkInput string
|
||||
|
||||
axiom2 = [lAxiom1, lAxiom3]
|
||||
axiom3 = [lAxiom2]
|
||||
infer2 = [lRule1]
|
||||
|
||||
-- (A → (B → A))
|
||||
lAxiom1 :: StringL -> StringL -> StringL
|
||||
lAxiom1 wff1 wff2 =
|
||||
[Open] ++
|
||||
wff1 ++
|
||||
[Arrow] ++
|
||||
[Open] ++ wff2 ++ [Arrow] ++ wff1 ++ [Close] ++
|
||||
[Close]
|
||||
|
||||
-- ((A → (B → C)) → ((A → B) → (A → C)))
|
||||
lAxiom2 :: StringL -> StringL -> StringL -> StringL
|
||||
lAxiom2 wff1 wff2 wff3 =
|
||||
[Open] ++
|
||||
[Open] ++
|
||||
wff1 ++
|
||||
[Arrow] ++
|
||||
[Open] ++ wff2 ++ [Arrow] ++ wff3 ++ [Close] ++
|
||||
[Close] ++
|
||||
[Arrow] ++
|
||||
[Open] ++
|
||||
[Open] ++ wff1 ++ [Arrow] ++ wff2 ++ [Close] ++
|
||||
[Arrow] ++
|
||||
[Open] ++ wff1 ++ [Arrow] ++ wff3 ++ [Close] ++
|
||||
[Close] ++
|
||||
[Close]
|
||||
|
||||
-- ((¬A → ¬B) → ((¬A → B) → A))
|
||||
lAxiom3 :: StringL -> StringL -> StringL
|
||||
lAxiom3 wff1 wff2 =
|
||||
[Open] ++
|
||||
[Open, Tilde] ++ wff1 ++ [Arrow, Tilde] ++ wff2 ++ [Close] ++
|
||||
[Arrow] ++
|
||||
[Open] ++
|
||||
[Open, Tilde] ++ wff1 ++ [Arrow] ++ wff2 ++ [Close] ++
|
||||
[Arrow] ++
|
||||
wff1 ++
|
||||
[Close] ++
|
||||
[Close]
|
||||
|
||||
{-
|
||||
ghci> import Logic.Statement.Eval (bucket)
|
||||
ghci> import Data.Either (fromRight)
|
||||
ghci> bucket $ fromRight undefined $ eof parseL $ mkInput $ lAxiom1 [Variable 0] [Variable 1]
|
||||
Tautology
|
||||
ghci> bucket $ fromRight undefined $ eof parseL $ mkInput $ lAxiom2 [Variable 0] [Variable 1] [Variable 2]
|
||||
Tautology
|
||||
ghci> bucket $ fromRight undefined $ eof parseL $ mkInput $ lAxiom3 [Variable 0] [Variable 1]
|
||||
Tautology
|
||||
-}
|
||||
|
||||
-- Modus ponens: from (A → B) and A, conclude B.
|
||||
lRule1 :: StringL -> StringL -> [StringL]
|
||||
lRule1 theorem1 theorem2 = maybeToList $ do
|
||||
s1 <- fromEither $ eof parseL $ mkInput theorem1
|
||||
s2 <- fromEither $ eof parseL $ mkInput theorem2
|
||||
case s1 of
|
||||
Implies s1a s1b
|
||||
| s1a == s2 -> Just $ fromJust $ serializeL s1b
|
||||
| otherwise -> Nothing
|
||||
_ -> Nothing
|
||||
where
|
||||
fromEither = either (const Nothing) Just
|
||||
|
||||
{-
|
||||
ghci> f x = fromJust $ serializeL $ fromRight undefined $ eof stmt $ mkInput x
|
||||
ghci> lRule1 (f "(0->1)") (f "0")
|
||||
[[Variable 1]]
|
||||
ghci> lRule1 (f "((!0->2)->(!!!!!!!1->1))") (f "(!0->2)")
|
||||
[[Open,Tilde,Tilde,Tilde,Tilde,Tilde,Tilde,Tilde,Variable 1,Arrow,Variable 1,Close]]
|
||||
ghci> lRule1 (f "((!0->2)->(!!!!!!!1->1))") (f "(!0->3)")
|
||||
[]
|
||||
-}
|
||||
|
||||
parseL :: Parser AlphaL Statement
|
||||
parseL = Parser variable <|> Parser tilde <|> arrow <|> fail
|
||||
where
|
||||
variable :: Input AlphaL -> Either ParseError (Statement, Input AlphaL)
|
||||
variable input@(Input pos ((Variable n):xs)) =
|
||||
Right (Atom $ show n, Input (pos + 1) xs)
|
||||
variable input = Left $ expected "statement variable" input
|
||||
|
||||
tilde :: Input AlphaL -> Either ParseError (Statement, Input AlphaL)
|
||||
tilde input@(Input pos (Tilde:xs)) =
|
||||
(\(statement, rest) -> (Not statement, rest)) <$>
|
||||
runParser parseL (Input (pos + 1) xs)
|
||||
tilde input = Left $ expected "negation" input
|
||||
|
||||
arrow :: Parser AlphaL Statement
|
||||
arrow = do
|
||||
_ <- parseToken [Open]
|
||||
s1 <- parseL
|
||||
_ <- parseToken [Arrow]
|
||||
s2 <- parseL
|
||||
_ <- parseToken [Close]
|
||||
return $ Implies s1 s2
|
||||
|
||||
fail :: Parser AlphaL Statement
|
||||
fail = Parser $ \input -> Left $ expected "well-formed formula" input
|
||||
|
||||
serializeL :: Statement -> Maybe [AlphaL]
|
||||
serializeL (Atom label) = (\x -> [x]) <$> Variable <$> readMaybe label
|
||||
serializeL (Not s) = (Tilde:) <$> serializeL s
|
||||
serializeL (Implies s1 s2) = do
|
||||
l1 <- serializeL s1
|
||||
l2 <- serializeL s2
|
||||
return $ [Open] ++ l1 ++ [Arrow] ++ l2 ++ [Close]
|
||||
serializeL _ = Nothing
|
||||
|
||||
deriveLExample1 :: Derivation AlphaL
|
||||
deriveLExample1 = step5
|
||||
where
|
||||
step1 = Hypothesis [Open, Variable 1, Arrow, Variable 2, Close]
|
||||
step2 = Axiom2 0 [Open, Variable 1, Arrow, Variable 2, Close] [Variable 0]
|
||||
step3 = Infer2 0 0 step2 step1
|
||||
step4 = Axiom3 0 [Variable 0] [Variable 1] [Variable 2]
|
||||
step5 = Infer2 0 0 step4 step3
|
||||
|
||||
deriveLExample2 :: Derivation AlphaL
|
||||
deriveLExample2 = step5
|
||||
where
|
||||
step1 = Axiom2 0 [Variable 0] [Open, Variable 0, Arrow, Variable 0, Close]
|
||||
step2 = Axiom3 0 [Variable 0] [Open, Variable 0, Arrow, Variable 0, Close] [Variable 0]
|
||||
step3 = Infer2 0 0 step2 step1
|
||||
step4 = Axiom2 0 [Variable 0] [Variable 0]
|
||||
step5 = Infer2 0 0 step3 step4
|
||||
86
lib/Logic/Language/Impl/MIU.hs
Normal file
86
lib/Logic/Language/Impl/MIU.hs
Normal file
|
|
@ -0,0 +1,86 @@
|
|||
module Logic.Language.Impl.MIU where
|
||||
|
||||
import Logic.Language (Language(..))
|
||||
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> import Logic.Language (ConcatShowList(..))
|
||||
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
|
||||
-}
|
||||
Loading…
Add table
Add a link
Reference in a new issue