Disclaimer: this first section is about alethic modal logic and truth trees. It's important to the question but significant parts of the code can probably be reviewed without it. You're welcome to skip ahead.
Alethic Modal Logic
For those who don't know, alethic modal logic is a superset of propositional logic enhanced with the necessity and possibility operators. Given a set of possible worlds, modal logic can express that a formula is true at all worlds as it is necessary that and that a formula is true at at least one world as it is possible that.
Truth Trees
A nice way to prove that a modal formula is always true is by using truth threes. If you don't feel like watching the video (as well as some follow-up videos) linked, here's a quick rundown of how it works:
In order to prove a formula always hold, given a set of axioms, you negate the formula and then apply a set of rules determined by the set of axioms and try to reduce the formula to a contradiction. If some branch does not result in a contradiction, the negated formula is true for some choice of primitive propositions and the original function is not necessarily true.
In modal logic (System K) there are the following rules:
¬¬f
-> addf
to the current branch in the current worldf&g
-> addf
andg
to the current branch in the current world¬(f&g)
-> make two branches, add¬f
to one,¬g
to the other◇f
(possibility) -> create a new world and addf
to that world- also add all
g
s so that□g
(necessity) at the current branch in the current world
- also add all
When you add axiom T, the possibility relationship become reflexive, hence:
◇f
-> addf
to the current branch in the current world
All other formulas can be reduced to one of the above, as it is done in the formulaType
function.
Code Explanation
I have implemented a (rather naive) version of modal truth trees in Haskell which I would like to have reviewed. Here's what you'll find in the code below along with some of my concerns and questions:
ModalFormula
This is the data type representing a modal formula. I've used TypeOperators to make it possible to write the formulas in a more or less natural way. I've also refrained from making it a type class because I felt like that would make it a lot easier to pattern match against them, but that may have been a mistake.
FormulaType
This represents the basic types of formulas that all formulas can be reduced to. In hindsight, I'm not terribly happy with this, since it seems like these types depend on the system of axioms you choose.
the function formulaType constructs these objects based on a ModalFormula.
World
This represents a possible world. It contains primitive functions that hold true at that world as well as formulas that are necessary and possible at that world and finally pairs of formulas, one of which is true. There are no other formulas, since those get deconstructed the moment they are added.
I'm not very pleased that I'm not using the type system to ensure that primitives
only contains primitive propositions and their negations. I feel like it night be possible using GADT's or type classes, but it might not be worth the effort.
addPrimitrive function and friends
These four functions add the formulas as one of the four types to the world and return the result. They use lenses, which I added in later, so the three last functions are trivially straightforward (might not be worth having as a function).
The addPrimitive
function has an additional use: it returns Nothing
if the resuting world would be inconsistent. It might be better to extract that functionality, but it felt natural to implement it like this.
FormulaAdder
FormulaAdders are functions that add a formula to a world accoring to a set of axioms. baseAdd
and addAll
implement the basic functionality and addK
and addT
enhance an adder with axiom K and T respectively.
k
and t
are FormulaAdders that correspond to system K and System T respectively, created by composing FormulaAddders that correspond to axioms and passing the result to baseAdder
prove and satisfiable
The prove
function is pretty straightforward if the implementation of satisfiable
is given. It constructs an world containing the negation of the formula that is to be proven and checks whether that world is satisfiable.
I'm not very pleased that I have to repeat explicitly add the negated formula at this point and deal with the returned world possibly being Nothing
here, maybe there's a nicer way to do this.
The satisfiable
function recursively calls itself and tries to evaluate all formulas in the world until it encounters an inconsistent world.
The implementation of this function might be a bit complex and possibly should have been split up more or written on more lines.
General concerns
- I might have gone overboard on trying to write code using point-free style
- is it too much?
- could some of it have been written better still using point-free style?
- I've used view patterns where it seemed fitting but might have gone overboard there as well
- is my use of view patterns readable?
- Did I miss some really cool features of Haskell that could have made this code more elegant?
- Unless it's really, really bad, I'm not very interested in performance
The Code
Without further ado, here's the code:
{-# Language TypeOperators, ViewPatterns, TemplateHaskell #-}
-- Contains data stuctures to represent alethic modal logic formulas
-- and functions to prove these formulas in system K and T.
module ModalLogic (
ModalFormula(..), prove, neg,
FormulaAdder,
World, emptyW, k, t
) where
import Data.Maybe
import Control.Lens
import Data.Set (Set, insert, empty, deleteFindMax, toList)
import Control.Monad ((>=>))
-- The infix TypeOperators to construct modal formulas.
infixl 6 :<=>
infixl 7 :=>
infixl 8 :|
infixl 9 :&
-- a modal formula
data ModalFormula = P Int | Q Int
| Not ModalFormula | Nec ModalFormula | Pos ModalFormula
| ModalFormula :& ModalFormula | ModalFormula :| ModalFormula
| ModalFormula :=> ModalFormula | ModalFormula :<=> ModalFormula
deriving (Show, Read, Eq, Ord)
-- the type of a formula with regards to how it acts in a truth three
data FormulaType = Primitive ModalFormula
| Branching (ModalFormula, ModalFormula)
| Possibility ModalFormula
| Necessity ModalFormula
| Multiple [ModalFormula]
-- a possible world
data World = World { _primitives :: Set ModalFormula,
_branching :: Set (ModalFormula, ModalFormula),
_possibilities :: Set ModalFormula,
_necessities :: Set ModalFormula }
deriving Show
makeLenses ''World
-- a possible world with no formulas in it
emptyW :: World
emptyW = World empty empty empty empty
-- the negation of a given formula
neg :: ModalFormula -> ModalFormula
neg (Not f) = f
neg f = Not f
-- adds a primitive expression (a primitive or its negation) to a world
-- returns Nothing if the resulting World is inconsistent
addPrimitive :: ModalFormula -> World -> Maybe World
addPrimitive f ((neg f `elem`) . view primitives -> True) = Nothing
addPrimitive f w = Just . (primitives %~ (insert f)) $ w
-- adds a branch to a world
addBranching :: (ModalFormula, ModalFormula) -> World -> World
addBranching f = branching %~ (insert f)
-- adds a possiblitily to a world
addPossibility :: ModalFormula -> World -> World
addPossibility f = possibilities %~ (insert f)
-- adds a necessity to a world
addNecessity :: ModalFormula -> World -> World
addNecessity f = necessities %~ (insert f)
-- a function that adds a formula to a world according to certain rules
-- corresponds to a system in logic
type FormulaAdder = ModalFormula -> World -> Maybe World
-- adds all formulas in a list to a world using a given FormulaAdder
addAll :: FormulaAdder -> [ModalFormula] -> World -> Maybe World
addAll a fs = flip (foldr $ (=<<) . a) fs . Just
-- adds basic rules to a FormulaAdder
-- use this to construct a FormulaAdder
baseAdd :: FormulaAdder -> FormulaAdder
baseAdd _ (formulaType -> Primitive f) = addPrimitive f
baseAdd _ (formulaType -> Branching t@(f, g)) = Just . addBranching t
baseAdd a (formulaType -> Multiple fs) = addAll (baseAdd a) fs
baseAdd a f = a f
---- Axioms ----
-- pass these or a composition of these to baseAdd
-- adds Possibility and Necessity to a FormulaAdder
addK :: FormulaAdder -> FormulaAdder
addK _ (formulaType -> Possibility f) = Just . addPossibility f
addK _ (formulaType -> Necessity f) = Just . addNecessity f
addK _ _ = Just . id
-- adds Reflexivity to a FormulaAdder
addT :: FormulaAdder -> FormulaAdder
addT a (formulaType -> Necessity f) = baseAdd a f
addT _ _ = Just . id
-- composes two FormulaAdders imto one that applies all rules
comp :: FormulaAdder -> FormulaAdder -> FormulaAdder
comp a1 a2 f = a1 f >=> a2 f
-- FormulaAdder corresponding to System K
k = baseAdd $ addK k
-- FormulaAdder corresponding to System T
t = baseAdd $ comp (addK t) (addT t)
-- converts a modal formula in a basic formula type
formulaType :: ModalFormula -> FormulaType
-- primitive
formulaType f@ (P _) = Primitive f
formulaType f@ (Q _) = Primitive f
formulaType f@(Not (P _)) = Primitive f
formulaType f@(Not (Q _)) = Primitive f
-- neccesity
formulaType (Nec f) = Necessity f
formulaType (Not (Nec f)) = Possibility $ neg f
-- possibility
formulaType (Pos f) = Possibility f
formulaType (Not (Pos f)) = Necessity $ neg f
-- conjunction
formulaType (f :| g) = Branching (f, g)
formulaType (Not (f :| g)) = formulaType $ neg f :& neg g
-- disjunction
formulaType (f :& g) = Multiple [f, g]
formulaType (Not (f :& g)) = formulaType $ neg f :| neg g
-- implication
formulaType (f :=> g) = formulaType $ Not f :| g
formulaType (Not (f :=> g)) = formulaType $ f :& Not g
-- equivalence
formulaType (f :<=> g) = formulaType $ (f :& g) :| (neg f :& neg g)
formulaType (Not (f :<=> g)) = formulaType $ (neg f :& g) :| (f :& neg g)
-- double negation
formulaType (Not (Not f)) = formulaType f
-- returns true if a modal formula is provable in a given system (FormulaAdder)
prove :: FormulaAdder -> ModalFormula -> Bool
prove a = not . fromMaybe False . fmap (satisfiable a) . flip a emptyW . Not
-- splits a Set in a single elements and the rest if possible
sMaxRest :: Ord a => Set a -> Maybe (a, Set a)
sMaxRest ((==empty) -> True) = Nothing
sMaxRest s = Just $ deleteFindMax s
-- returns true if a given world is satisfiable in a given system (FormulaAdder)
satisfiable :: FormulaAdder -> World -> Bool
-- apply branching rules first
satisfiable a
w@(sMaxRest . view branching -> Just ((f, g), bs))
= let newWorld = (branching .~ bs $ w) in
-- a world is satifiable if any of its branches is satisfiable
any (fromMaybe False) . map (fmap (satisfiable a) . flip a newWorld ) $ [f, g]
-- apply possibilities next
satisfiable a
w@(sMaxRest . view possibilities -> Just (f, fs))
-- all neccesities must be true in every possible world
= let createdWorld = addAll a (toList (insert f (_necessities w))) emptyW
newWorld = (possibilities .~ fs $ w) in
-- both the current world and the created world must be satisfiable
all (fromMaybe False) . map (fmap (satisfiable a)) $ [Just newWorld, createdWorld]
-- a world is satisfiable if there are no more rules left to apply
satisfiable _ _ = True