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