162 lines
4.6 KiB
Haskell
162 lines
4.6 KiB
Haskell
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
|
|
| s2 == s1a -> 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]
|
|
|
|
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
|