LogicParser.hs

-- Some code for parsing natural language, transforming grammar trees into statements in
-- propositional logic, and infering things from those propositions.
--
-- This code is pretty unstructured, but I might salvage some of some day.
-- I'm leaving this here on the off chance that someone stumbles upon this and finds it
-- useful, enjoy!

module Main where

import Data.List.Split

-- English Grammar data types --

data D = The | A

type Adj = String
type Adv = String
type N = String
type V = String

data NP = NP (Maybe D) (Maybe Adj) N
data VP = VP V NP (Maybe Adv)

data S = S NP VP

-- Propositional data types --

data Proposition a b = Is a b
    deriving (Eq,Show)

data PropLogic a = Prop a | Tautology | Contradiction | And (PropLogic a) (PropLogic a)
                | Or (PropLogic a) (PropLogic a) | Implies (PropLogic a) (PropLogic a)
                | Not (PropLogic a)
    deriving (Eq,Show)

{--
data PropQuantifiedLogic a = Prop a | Tautology | Contradiction | And (PropQuantifiedLogic a) (PropQuantifiedLogic a)
                | Or (PropQuantifiedLogic a) (PropQuantifiedLogic a) | Implies (PropQuantifiedLogic a) (PropQuantifiedLogic a)
                | Not (PropQuantifiedLogic a) | Forall (PropQuantifiedLogic a) | Exists (PropQuantifiedLogic a)
    deriving (Eq,Show)
--}

type IntProp = PropLogic Int

type STDProp = PropLogic (Proposition String String)

-- Logic values --

-- Values for a trivalent logic system
data Trivalent = TTrue | TFalse | TNil
    deriving(Show,Enum)

-- Basic inference functions --

modusPonens :: [STDProp] -> STDProp
modusPonens [Implies p q, r] | p == r = p

doubleNegation :: [STDProp] -> STDProp
doubleNegation [Not (Not x)] = x

modusTollens :: [STDProp] -> STDProp
modusTollens [Implies p q, Not r] | r == q = Not p

commute :: STDProp -> STDProp
commute (And a b) = And b a
commute (Or a b) = Or b a

distribute :: STDProp -> STDProp
distribute (And a (Or b c)) = Or (And a b) c
distribute (Or a (And b c)) = And (Or a b) (Or a c)

deMorgan :: STDProp -> STDProp
deMorgan (Not (And a b)) = Or (Not a) (Not b)
deMorgan (Not (Or a b)) = And (Not a) (Not b)

addition :: [STDProp] -> STDProp
addition [p,q] = And p q

subtraction1 :: [STDProp] -> STDProp
subtraction1 [p,q] = p

subtraction2 :: [STDProp] -> STDProp
subtraction2 [p,q] = q

reduceImplyOr :: STDProp -> STDProp
reduceImplyOr (Implies p q) = Or (Not p) q

hypotheticalSyllogism [Implies p q, Implies r s] | q == r = Implies p s

-- Functions for reducing tautologies and contradictions, possibly can be renamed --

cont1 [p, Not p'] | p == p' = Contradiction

cont2 (And p Contradiction) = Contradiction

cont3 (Or p Contradiction) = Contradiction

taut1 (And p q) = p -- Should I change tautology to match contradiction? (i.e. no argument)

-- taut2

-- taut3

-- Testing the inference functions --

-- English -> Propositional parsing --

-- Will need recursion for full english -> prop parsing function, but this
-- is a general idea of how it should work.
englishToProp :: S -> STDProp
englishToProp (S (NP _ _ n) (VP "is" (NP _ _ adj) _)) = Prop (Is n adj) -- This is the general "is" case
-- englishToProp (S (NP _ _ n) (VP v (NP _ _ adj) _)) = Tautology (Is n [adj,v]) -- This is the case where a non-is verb is transformed into the correct proposition.
-- ^ For this case, I need to first implement multiple adjectives somehow.

-- Inference engines --

-- Basic inference strategy for classical inference
-- Basically go through the list of STDProps to see if the
-- requested fact has already been infered.
classicalInfer :: [STDProp] -> STDProp -> Maybe Bool
classicalInfer _ Tautology = Just True
classicalInfer _ Contradiction = Just False
classicalInfer (x:_) y | x == y = Just True
classicalInfer (_:xs) y = classicalInfer xs y
classicalInfer [] _ = Nothing

infiniteInfer = InferResult classicalInfer
              : InferUpdate subtractAll
              : infiniteInfer

infiniteInfer2 = InferResult classicalInfer : infiniteInfer2

-- Define a type for two different kinds of functions used for inference strategies.
--
-- An InferResult takes a list of propositions (given), a proposition (query), and returns Just True or Just False
-- if the strategy can decide whether or not the given query is true. If it cannot determine whether or not
-- then it returns Nothing.
--
-- An InferUpdate is used for taking a list of propositions and infering new results from them, or removing unnescesary
-- ones.

-- Functions used for filtering lists for types of propositions, used in some of the
-- inference strategies.

isAnd (And a b) = True
isAnd x = False

isImplies (Implies a b) = True
isImplies x = False

isOr (Or a b) = True
isOr _ = False

isNand (Not (And a b)) = True
isNand _ = False

isNor (Not (Or a b)) = True
isNor _ = False

isNotImplies (Not (Implies a b)) = True
isNotImplies _ = False


-- Precondition: Should be a list of [PropLogic a] where all of the elements of the list match
-- the pattern (And p q):xs.
-- Postcondition: Returns a list of just (Prop x)'s
--
-- Used to build the subtractAll function.
--
_subtractAll :: [PropLogic a] -> [PropLogic a]
_subtractAll (And p q : xs) = subtractAll xs ++ [p,q]
_subtractAll x = x

subtractAll :: [PropLogic a] -> [PropLogic a]
subtractAll x = _subtractAll (filter (isAnd) x) ++ x

l = [(And (Prop 1) (Prop 2)),(Prop 3)]
l2 = subtractAll l

data InferFunction = InferResult ([STDProp] -> STDProp -> Maybe Bool)
                   | InferUpdate ([STDProp] -> [STDProp])

-- Try various inference strategies until one does not return Nothing.
try :: [InferFunction] -> [STDProp] -> STDProp -> Maybe Bool
try ((InferResult f):fs) x y = if f x y == Nothing
                then try fs x y
                else f x y
try ((InferUpdate f):fs) x y = try fs (f x) y

-- Try two strategies.
-- tr = try infiniteInfer [(And (Prop (Is "Michael" "Cool")) (Prop (Is "Nate" "Cool"))), (Prop (Is "Nate" "cool"))] (Prop (Is "Nate" "cool"))
-- tr2 = try infiniteInfer2 [(Prop (Is "Nate" "Cool"))] (Prop (Is "Nate" "cool"))

mBool :: Maybe a -> Bool
mBool (Just x) = True
mBool Nothing = False

-- classicalQuantifiedInfer ::

-- modalInfer ::

-- temporalInfer ::

-- intuitionisticInfer ::

-- inuitionQuantifiedInfer ::

-- String -> English parsing --

tokenize :: String -> [String]
tokenize x = splitOn " " x

splitSentences :: String -> [String]
splitSentences x = splitOn "." x

parseString x = map ((filterOut "") . tokenize) (splitSentences x)

-- Random neat little utility function. I should keep this for use later.
filterOut x y = filter (/= x) y

parse :: [String] -> [S]
parse [x,"is",y] = [(S (NP Nothing Nothing x) (VP "is" (NP Nothing Nothing y) Nothing))]

-- Once again, this is just a base case, with proper recursion, this should work for all cases.

-- type English = [S] -- English is a list of sentences
-- parseEnglish :: String -> English

-- "Deep structure" gramatical transformation functions might be nescesary to parse some of the more complicated
-- aspects of the English language. Read Chomsky plz.

-- test4 = S (NP Nothing Nothing "Nate") (VP "test" (Just "quickly"))

-- Note: In order to make the gramatical analysis correct, strings have to be split up into sentences. This is trivial, but average everyday humans may not
-- be able to consistantly write in the proper format.
--
-- To rememdy this, a machine learning system could be setup where "casual input" from everyday English speakers is mapped to the proper (likley) input.
--
-- Aditional propositions might also be infered from the user's writing style or punctuation.

-- Test values --

x = modusTollens [Implies (Prop (Is "Nate" "Happy")) (Prop (Is "Nate" "Dance")),
                  Not (Prop (Is "Nate" "Dance"))]

y = englishToProp test3 -- Is "Nate" "Cool"

s = splitSentences "This is two sentences. These two sentences need to be split"
s2 = tokenize "These are words"
s3 = parseString "This is two sentences. These two sentences need to be split"

test = VP "is" (NP Nothing Nothing "cool") Nothing
test2 = NP Nothing Nothing "Nate"
test3 = S test2 test -- Nate is cool.

f = parse . tokenize
z = englishToProp $ (head (f "Nate is cool"))

inf = classicalInfer [(Prop (Is "Nate" "cool"))] (Prop (Is "Nate" "cool"))

list :: [PropLogic Int]
list = [(And (Prop 1) (Prop 2)),(Or (Prop 5) (Prop 7)),(Implies (Prop 15) (Prop 2)),(Or (Prop 3) (Prop 1))]
list2 = filter isOr list
list4 = filter isAnd list
list3 = filter isImplies list

main :: IO ()
main = do
    putStrLn "test"