infix 7 :=> data Wff = Var String | T | F | Not Wff | Wff :=> Wff isImp :: Wff -> Bool isImp (_ :=> _) = True isImp _ = False limp, rimp :: Wff -> Wff limp (x :=> _) = x rimp (_ :=> x) = x vars :: Wff -> [String] vars (x :=> y) = vars x `union` vars y vars (Not x) = vars x vars (Var s) = [s] vars _ = [] infix 6 :|- data Prf = K Wff Wff | S Wff Wff Wff | CP Wff Wff | Top Wff | Bot Wff | Hyp Wff | MP Prf Prf infixr 8 `union` infix 8 `without` data Seq = [Wff] :|- Wff seq :: Prf -> Seq seq (K x y) = [] :|- x :=> (y :=> x) seq (S x y z) = [] :|- (x :=> (y :=> z)) :=> ((x :=> y) :=> (x :=> z)) seq (CP x y) = [] :|- (Not x :=> Not y) :=> (y :=> x) seq (Top x) = [] :|- x :=> T seq (Bot x) = [] :|- F :=> x seq (Hyp x) = [x] :|- x seq (MP p q) = ws `union` hs :|- y, if w == x where ws :|- w = seq p hs :|- x :=> y = seq q con :: Prf -> Wff con p = x where _ :|- x = seq p hyps :: Prf -> [Wff] hyps p = hs where hs :|- _ = seq p gp :: Prf -> Bool gp (MP p q) = gp p && gp q && isImp cq && cp == limp cq where cp = con p cq = con q gp _ = True just :: Prf -> Seq -> Bool p `just` (hs :|- x) = gp p && con p == x && hyps p `subset` hs reflex :: Wff -> Prf reflex x = MP (K x x) (MP (K x (x :=> x)) (S x (x :=> x) x)) ded :: Wff -> Prf -> Prf ded h (MP p q) = MP (ded h p) (MP (ded h q) (S h (con p) (rimp (con q)))) ded h (Hyp x) = reflex h, if h == x ded h p = MP p (K (con p) h) data BL = TT | FF imp :: BL -> BL -> BL FF `imp` _ = TT TT `imp` x = x neg :: BL -> BL neg TT = FF neg FF = TT type Env a = [(String, a)] dom :: Env a -> [String] dom = nub . map fst lookup :: Env a -> String -> a lookup e s = head [x | (s',x) <- e, s' == s] eval :: Env BL -> Wff -> BL eval v (x :=> y) = eval v x `imp` eval v y eval v (Not x) = neg (eval v x) eval v T = TT eval v F = FF eval v (Var s) = lookup v s sub :: Env Wff -> Wff -> Wff sub e (x :=> y) = sub e x :=> sub e y sub e (Not x) = Not (sub e x) sub e T = T sub e F = F sub e (Var s) = lookup e s , if s `elem` dom e = Var s , otherwise syntax :: Env BL -> Env Wff syntax e = [(s, syn x) | (s,x) <- e] syn :: BL -> Wff syn TT = T syn FF = F type Tactic = Goal -> Opt ([Goal],Validation) data Opt a = Ok a | Fail type Validation = [Prf] -> Prf type ParamValidation = [Wff] -> Validation type Goal = Seq idtac, failtac :: Tactic idtac g = Ok ([g], (\[x] -> x)) failtac g = Fail (t1 `alttac` t2) g = t1 g ? t2 g ( ?) :: Opt a -> Opt a -> Opt a Ok x ? _ = Ok x Fail ? y = y alttacs :: [Tactic] -> Tactic alttacs = foldr alttac failtac usetac :: Tactic -> Goal -> Prf usetac t g = f [] where Ok ([],f) = t g sizeSeq :: Seq -> Int sizeSeq (hs :|- x) = sum (map g hs) + g x where g (y :=> z) = 2 + g y + g z g (Not y) = 1 + g y g _ = 1 tacCI, tacCNN, tacCNI, tacHNN, tacHI, tacHNI :: Tactic tacCI = mktac "|- X => Y" "X |- Y" ci "X" tacCNN = mktac "|- ~~X" "|- X" cnn "" tacCNI = mktac "|- ~(X => Y)" "|- X; |- ~Y" cni "" tacHNN = mktac "~~X |- Z" "X |- Z" hnn "X" tacHI = mktac "X => Y |- Z" "~X |- Z; Y |- Z" hi "X,Y" tacHNI = mktac "~(X => Y) |- Z" "X, ~Y |- Z" hni "X,Y" tacCTRAD, tacHYP, tacCT, tacCNF, tacHF, tacHNT :: Tactic tacCTRAD = mktac "X, ~X |- Y" "" ctrad "X,Y" tacHYP = mktac "X |- X" "" hyp "X" tacCT = mktac "|- T" "" ct "" tacCNF = mktac "|- ~F" "" cnf "" tacHF = mktac "F |- X" "" hf "X" tacHNT = mktac "~T |- X" "" hnt "X" tacprove = reptac (alttacs [ -- `theorem' tactics: tacCTRAD, tacHYP, tacCT, tacCNF, tacHF, tacHNT, -- `inference' tactics: tacCI, tacCNN, tacCNI, tacHI, tacHNN, tacHNI]) prove :: Seq -> Prf prove = usetac tacprove {- isOK checks if its argument is an exception -} isOk :: Opt a -> Bool isOk Fail = False isOk (Ok _) = True isFail :: Opt a -> Bool isFail = not . isOk unOk (Ok x) = x {- reptac is the repetition tactical. For efficiency, it is defined as a cyclic structure -} reptac :: Tactic -> Tactic reptac t = r where r = (t `thentac` r) `alttac` idtac {- thentac is the sequential composition tactical. -} thentac :: Tactic -> Tactic -> Tactic (t1 `thentac` t2) g = Ok (gs,f) , if isOk ng1 && ng2Ok = Fail , otherwise where ng1 = t1 g (gs1, f1) = unOk ng1 ng2 = map t2 gs1 ng2Ok = all isOk ng2 gs2 = map (fst . unOk) ng2 fs = map (snd . unOk) ng2 gs = concat gs2 ls = map length gs2 f = f1 . mappart ls fs {- part takes a list of ints and a list of arbitrary type and partitions the latter into sublists of sizes specified in the former. -} part :: [Int] -> [a] -> [[a]] part [] [] = [] part (n:ns) xs = take n xs : part ns (drop n xs) mappart :: [Int] -> [[a] -> b] -> [a] -> [b] mappart ns fs xs = zipWith ( $) fs (part ns xs) wrap x = [x] unwrap [x] = x {- mktac parses and normalizes its arguments and passes them to mktac' -} mktac :: String -> String -> ParamValidation -> String -> Tactic mktac g gs f xs = mktac' (nubSeq (parSeq g)) (map nubSeq (parSeqs gs)) f (parWffs xs) {- mktac' takes the description of an inference rule and generates the corresponding tactic -} mktac' :: Goal -> [Goal] -> ParamValidation -> [Wff] -> Tactic mktac' g gs f xs g' = Ok (gs', f xs'), if isOk e = Fail , otherwise where e = matchSeq g g' (e',hs) = unOk e gs' = map (addhyps ys . subS e') gs xs' = map (sub e') xs zs :|- _ = g' ys = zs `withoutlist` hs {- matchWff finds a substitution environment to match its first argument to its second -} matchWff :: Wff -> Wff -> Opt (Env Wff) matchWff (Var s) y = Ok [(s,y)] matchWff (w :=> x) (y :=> z) = matchWff w y `joinEnv` matchWff x z matchWff (Not x) (Not y) = matchWff x y matchWff _ _ = Fail {- matchSeq s1 s2 tries to find a substitution environment for matching s1 's conclusion to s2 's conclusion and s1 's hypotheses to a subset of s2' s hypotheses. If successful, it returns the environment and the list of the hypotheses in s2 leftover. -} matchSeq :: Seq -> Seq -> Opt (Env Wff, [Wff]) matchSeq (ws :|- x) (hs :|- y) = Ok (head ms), if not (null ms) = Fail , otherwise where e' = matchWff x y ms = [(unOk e,xs) | (e'',xs) <- matchmatch ws hs, e = e' `joinEnv` Ok e'', isOk e] {- matches takes a wff and a list of wffs and returns all possible ways of matching the wff to an element of the list and, in each case, the leftover wffs not matched. -} matches :: Wff -> [Wff] -> [(Env Wff, Wff)] matches w hs = [(unOk e,h) | h <- hs, e = matchWff w h, isOk e] {- matchmatch takes two lists of wffs and returns all possible ways of matching the first list to a subset of the second and in each case the leftover wffs not matched. -} matchmatch :: [Wff] -> [Wff] -> [(Env Wff, [Wff])] matchmatch [] hs = [([],[])] matchmatch (w:ws) hs = [(unOk e'', h:hs') | (e,h) <- matches w hs, (e',hs') <- matchmatch ws (hs `without` h), e'' = Ok e `joinEnv` Ok e', isOk e''] {- joinEnv joins two compatible substitution environments -} joinEnv Fail _ = Fail joinEnv _ Fail = Fail joinEnv (Ok v) (Ok e) = Fail , if not (null xs) = Ok (v `union` e), otherwise where xs = [s |(s,x) <- v, s `elem` dom e && lookup e s /= x] cni, cnn, hnn, hni, hi, ct, cnf, hf, hnt, ctrad, hyp :: ParamValidation ci [x] [p] = ded x p cni [] [p,q] = MP q ((anticontrapos . ded xiy) (MP p (Hyp xiy))) where (_ :|- x) = seq p (_ :|- Not y) = seq q xiy = x :=> y cnn [] [p] = MP p (impnotnot (con p)) hnn [x] [p] = MP (unded (notnotimp x)) (ded x p) hni [x,y] [p] = (nottrade (con p) . ded x . nottrade y) p hi [x,y] [p,q] = nottrade z (cni [] [nottrade x p, anticptrade y q]), if z == z' where (z, z') = (con p, con q) hyp [x] [] = Hyp x ctrad [x,y] [] = nottrade y (Hyp x) ct [] [] = MP (Top T) (Top (T :=> T)) cnf [] [] = MP (cnn [] [ct [] []]) (anticontrapos (Bot (Not T))) hf [x] [] = unded (Bot x) hnt [x] [] = nottrade x (ct [] []) unded :: Prf -> Prf unded p = MP (Hyp (limp (con p))) p contrapos :: Prf -> Prf contrapos p = MP p (CP x y) where (_ :|- Not x :=> Not y) = seq p dedantec :: Prf -> Prf dedantec p = ded x (MP (Hyp x) p) where x = limp (con p) notnotimp :: Wff -> Prf notnotimp x = (dedantec . contrapos . contrapos) (MP (Hyp nt2x) (K nt2x nt4x)) where nt2x = Not (Not x) nt4x = Not (Not nt2x) impnotnot :: Wff -> Prf impnotnot x = contrapos (notnotimp (Not x)) nottrade :: Wff -> Prf -> Prf nottrade x p = (unded . contrapos . ded (Not x) . cnn [] . wrap) p anticptrade :: Wff -> Prf -> Prf anticptrade x p = (unded . anticontrapos . ded x) p cptrade :: Wff -> Prf -> Prf cptrade x p = (hnn [rimp (con p)] . wrap . nottrade (Not x)) p anticontrapos :: Prf -> Prf anticontrapos p = (contrapos . ded nt2x . cnn [] . wrap . hnn [x] . wrap . unded) p where x = limp (con p) nt2x = Not (Not x) {- showWff pretty prints a wff -} showWff x = sliceparens (showWff' x []) showWff' (Var s) zs = s ++ zs showWff' (Not x) zs = '~' : showWff' x zs showWff' (x :=> y) zs = '(' : showWff' x (" => " ++ showWff' y (')':zs)) showWff' T zs = 'T':zs showWff' F zs = 'F':zs sliceparens "" = "" sliceparens (x:xs) | x == '(' = init xs | otherwise = (x:xs) showWffs = foldr f [] . map showWff where f xs [] = xs ++ " " f xs ys = xs ++ ", " ++ ys showSeq (hs :|- w) = showWffs hs ++ "|- " ++ showWff w {- numnodes counts the number of nodes in a proof -} numnodes :: Prf -> Int numnodes (MP p q) = numnodes p + numnodes q + 1 numnodes _ = 1 {- showPrf pretty prints a proof -} showPrf p = fst (showPrf' p 0 []) showPrf' p @ (MP q1 q2) n zs = (sh1, s), if x == y where (sh1,s1) = showPrf' q1 n sh2 (sh2,s2) = showPrf' q2 (n+n1) (shPline p s (n+n1+n2) ++ show (n+n1-1) ++ ", " ++ show (n+n1+n2-1) ++ "\n" ++ zs) (n1,n2) = (numnodes q1, numnodes q2) ws :|- x = s1 hs :|- y :=> z = s2 s = ws `union` hs :|- z showPrf' p n zs = (shPline p s n ++ "\n" ++ zs, s) where s = seq p shPline p s n = shlinnum n ++ showSeq s ++ " " ++ showrsn p shlinnum :: Int -> String shlinnum = ljustify 4 . show showrsn (K x y) = "K " ++ showWff x ++ ", " ++ showWff y showrsn (S x y z) = "S " ++ showWff x ++ ", " ++ showWff y ++ ", " ++ showWff z showrsn (CP x y) = "CP " ++ showWff x ++ ", " ++ showWff y showrsn (MP _ _) = "MP " showrsn (Hyp x) = "Hyp " ++ showWff x showrsn (Top x) = "Top " ++ showWff x showrsn (Bot x) = "Top " ++ showWff x {- A parsing library. The following is lifted directly from the parser library of Mark Jones's Mini-Prolog language written in Gofer (demos/prolog/parser in the distribution) which, in turn, was taken from Richard Bird's notes on parsers done in Orwell. (I have lifted Jones' explanations as well since they make the following comprehensible.) -} infixr 6 ->> infixr 4 ||| infixl 5 `do` -- Type definition: type Parser a = [Char] -> [(a,[Char])] {- A parser is a function which maps an input stream of characters into a list of pairs each containing a parsed value and the remainder of the unused input stream. This approach allows us to use the list of successes technique to detect errors (i.e. empty list ==> syntax error). it also permits the use of ambiguous grammars in which there may be more than one valid parse of an input string. Primitive parsers: fail is a parser which always fails. okay v is a parser which always succeeds without consuming any characters from the input string, with parsed value v. tok w is a parser which succeeds if the input stream begins with the string (token) w, returning the matching string and the following input. If the input does not begin with w then the parser fails. sat p is a parser which succeeds with value c if c is the first input character and c satisfies the predicate p. -} fail :: Parser a fail is = [] okay :: a -> Parser a okay v is = [(v,is)] tok :: [Char] -> Parser [Char] tok w is = [(w, drop n is) | w == take n is] where n = length w sat :: (Char -> Bool) -> Parser Char sat p [] = [] sat p (c:is) = [ (c,is) | p c ] {- Parser combinators: p1 ||| p2 is a parser which returns all possible parses of the input string, first using the parser p1, then using parser p2. p1 ->> p2 is a parser which returns pairs of values (v1,v2) where v1 is the result of parsing the input string using p1 and v2 is the result of parsing the remaining input using p2. p `do` f is a parser which behaves like the parser p, but returns the value f v wherever p would have returned the value v. many p returns a list of values, each parsed using the parser p. many1 p parses a non-empty list of values, each parsed using p. listOf p s parses a list of input values using the parser p, with separators parsed using the parser s. -} (|||) :: Parser a -> Parser a -> Parser a (p1 ||| p2) is = p1 is ++ p2 is ( ->>) :: Parser a -> Parser b -> Parser (a,b) (p1 ->> p2) is = [((v1,v2),is2) | (v1,is1) <- p1 is, (v2,is2) <- p2 is1] do :: Parser a -> (a -> b) -> Parser b (p `do` f) is = [(f v, is1) | (v,is1) <- p is] many :: Parser a -> Parser [a] many p = q where q = (p ->> q `do` makeList) ||| (okay []) many1 :: Parser a -> Parser [a] many1 p = p ->> many p `do` makeList listOf :: Parser a -> Parser b -> Parser [a] listOf p s = p ->> many (s ->> p) `do` nonempty ||| okay [] where nonempty (x,xs) = x:(map snd xs) makeList :: (a,[a]) -> [a] makeList (x,xs) = x:xs {- Parsing wffs and sequents. Here is the EBNF style grammar for wffs: pW = pW' "=>" pW' | pW' pW' = literal | "~" pW' | "(" pW' ")" | "(" pW' "=>" pW' ")" There is a special case in pW since "X => Y" should be a valid string to parse, i.e., the outermost implication needn't be enclosed in parentheses. As a result, backtracking must be done to resolve the two cases of pW, but, clearly, the grammar isn't ambiguous. -} parWff = fst . head . pW . filtSpaces filtSpaces = filter ( /= ' ') pW = pW' ->> tok "=>" ->> pW' `do` getImp ||| pW' pW' = many1 (sat isAlpha) `do` getident ||| tok "~" ->> pW' `do` getNot ||| tok "(" ->> pW' ->> tok "=>" ->> pW' ->> tok ")" `do` getparenImp ||| tok "(" ->> pW' ->> tok ")" `do` getparen getNot (_,y) = Not y getident "T" = T getident "F" = F getident xs = Var xs getparenImp (_,(x,(_,(y,_)))) = x :=> y getImp (x, (_, y)) = x :=> y getparen (_,(x,_)) = x pWs = listOf pW (tok ",") parWffs = fst . head . pWs . filtSpaces parSeq = fst . head . parSeq' . filtSpaces parSeq' = pWs ->> tok "|-" ->> pW `do` getSeq getSeq (xs, (_, x)) = xs :|- x parSeqs = fst . head . parSeqs'. filtSpaces parSeqs' = listOf parSeq' (tok ";") `do` id xs `union` ys = nub (xs ++ ys) xs `subset` ys = all (`elem` ys) xs xs `without` x = filter ( /= x) xs xs `withoutlist` ys = filter (`notElem` ys) xs nubSeq (hs :|- x) = nub hs :|- x addhyps hs (ws :|- x) = (ws `union` hs) :|- x pprove :: String -> String pprove = showPrf . prove . parSeq {- subS performs a substitution on sequent -} subS e (hs :|- x) = map (sub e) hs :|- sub e x {- instance ... adds wffs to the equality type-class -} instance Eq Wff where (w :=> x) == (y :=> z) = w == y && x == z (Not x) == (Not y) = x == y (Var s) == (Var t) = s == t T == T = True F == F = True _ == _ = False