Monadic plumbing

As a quick reminder, here is the definition of the list monad.

instance Monad [] where
  return a     = [a]
  [] >>= _     = []
  (a:as) >>= k = k a ++ as >>= k

It'll be useful to have this definition on hand as we manipulate lists and the functions that act on them!

Recall the type we associate with a rule (remember that a rule is a way of extending a tableau at one of its terminal nodes, according to the main connective of the formula that occurs at that node and the formula's sign):

type Rule = Path -> SignedForm -> [Branch]

where

type SigneForm = (Form, Bool)
type Path = [SignedForm]
type Branch = [SignedForm]

Thus given some path (which the rule might use to determine, e.g., which names are fresh), a rule takes a signed formula at some node onto the set of new branches that should extend out from that node once the rule has applied.

What we would like is a way of promoting a Rule to a function which can be applied to an entire Path. That is, we require a function

applyRule :: Rule -> Path -> [Path]

which applies a rule to each path in some tableau—by targeting all the nodes on that path—in order to give back a new tableau. Then, using applyRule, we can write a function

allRules :: Path -> [Path]
allRules p = do p0 <- applyRule (const andRule) p
                p1 <- applyRule (const orRule) p0
                p2 <- applyRule (const notRule) p1
                p3 <- applyRule gammaRule p2
                p4 <- applyRule deltaRule p3
                return p4

which starts with some path p, and then successively applies each rule to that path. That is, first andRule is applied to p via applyRule—note that const :: a -> b -> a simply allows andRule to ignore the first (Path type) argument—and then p1 is drawn from the result; next, orRule is applied to p1, and p2 is drawn from the result; etc., until we've applied each rule exactly once.

Given such a function, we can implement a way of looping all the rules over a tableau and then checking each path for a contradiction.

For the latter, we need the function

contradiction :: [Path] -> Bool
contradiction [] = False
contradiction ((f, b) : fs) = (f, not b) `elem` fs || contradiction fs

That is, for each signed formula on some path, we check whether the same formula, but with opposite sign, occurs somewhere else on the path; if not, we check to see if the rest of the path (excluding that signed formula) is somehow contradictory.

Now let's write a function that implements one loop! This function, loop, should have type

loop :: Tableau -> Tableau

where

type Tableau = [Maybe Path]

In other words, a Tableau is a list of things which might be paths. If some path has been determined to be contradictory, it should get replaced by a Nothing, indicating that we never have to worry about it again. If not, we should apply allRules to it and map Just over the resulting paths, indicating that they are still live. Thus we may define loop as

loop tableau = do
  maybefs <- tableau
  case maybefs of
    Nothing -> pure Nothing
    Just fs -> do
      newFs <- allRules fs
      if contradictory newFs
      then pure Nothing
      else pure (Just newFs)

We are almost there! Now, given a list of signed formulae, we would like to be able to check if they are contradictory, given some depth n of application of our rules. Thus we write a function

depth :: Int -> [SignedForm] -> Bool
depth n sfs = all (== Nothing) (iterate loop [map Just sfs] !! n)

which turns the list of signed formulae sfs into a starting Tableau (by doing [map Just sfs]) and then loops the rules over it n times, using iterate. If the tableau is contradictory after n loops—that is, if all the branches are Nothing—we assume we have a contradiction; otherwise, we we assume the signed formulae are not contradictory. Note that we might sometimes be wrong.¹

In terms of our function depth, we my define a function that checks (at some depth) whether or not some set of formulae entails another formula. We do this by applying depth to a starting tableau in which the possibly-entailed formula is paired with False and the other formulae are paired with True. Thus if the formula is truly entailed, a contradiction will ensue.

entails :: Int -> [Form] -> Form -> Bool
entails n antecedents consequent = depth n sfs
  where sfs = (consequent, False) : map (, True) antecedents

Yay!