Posted: Mar 14, 2012 10:51 pm
mizvekov wrote:I see, I will take a look at that.
Any more interesting tidbits of related Haskell code?
Well, I've got quite a lot of code built on top of this. But I'll try to focus on just a couple.

Like I said a few posts back, the problem with the proof style here is that you can't make assumptions during a proof, and then later discharge them. To fix that, I wrote a tiny proof language:

Code: Select all
`module Bootstrap whereimport Propositionalimport Utilsimport Data.List-- Proof terms with assumptions. In comments, we write Γ ⊢ P to denote a proof with-- conclusion P and assumptions Γ. Proofs are not guaranteed to be valid, and are-- pushed through the kernel via verify.data Proof = Assume (Term String)           | UseTheorem (Theorem String)           | MP Proof Proof            deriving Show`

This is a common idea in Haskell and ML. You use a data-type to define the syntax of an embedded language. We now have two languages: the language of propositional terms, and a language of proofs. The equivalent idea in Java or C# (and C++?) would be to define an inheritance hierarchy rooted at a "Proof" interface, and with implementing classes for each data constructor. You'd then use the Visitor pattern to write things such as evaluation functionality. That's a lot of code. In ML and Haskell, things are much simpler. You use algebraic data-types and evaluators are just functions which pattern-match on that data-type. Incidentally, this was the raison d'etre for algebraic data-types: to define new languages. Indeed, ML is a language for defining languages: a MetaLanguage (no pun, that's what it stood for).

I use this pattern a lot because it's so lightweight.

Now we add some semantics. Here's some code to extract all the assumptions and the conclusion of a proof:

Code: Select all
`sequent :: Proof -> ([Term String], Term String)sequent (Assume a)   = ([a], a)sequent (UseTheorem t) = ([], theoremTerm t)sequent (MP pr pr')    = let (asms,c) = sequent pr' in  case sequent pr of    (asms', p :=>: q) | p == c    -> (nub \$ sort \$ asms ++ asms', q)                      | otherwise -> error "MP"    _ -> error "MP"concl :: Proof -> Term Stringconcl = snd . sequentassms :: Proof -> [Term String]assms = fst . sequent`

That's the easy bit. The hard step is to write a function which mirrors the Deduction Theorem. This function transforms a proof into a new proof in which you have made one less assumption. In other words, it is a function which discharges an assumption from a proof. I cribbed the idea for the implementation by basing it on the standard inductive proof of the theorem (inductive base case becomes recursive base case, while inductive step becomes the recursive call):

Code: Select all
`-- ⊢ P → Ptruth :: Theorem Stringtruth = let step1 = instL [p, p :=>: p] axiom1            step2 = instL [p, p :=>: p, p] axiom2            step3 = head \$ mp step2 step1            step4 = instL [p, p] axiom1 in        head \$ mp step3 step4discharge :: Term String -> Proof -> Proofdischarge asm pr = let inAsm = elem asm (assms pr) in d pr    where d pr@(Assume t) | t == asm  = UseTheorem (instL [t] truth)                          | otherwise =                              MP (UseTheorem (instL [concl pr,asm] axiom1)) pr          d pr@(UseTheorem t)               = MP (UseTheorem (instL [concl pr,asm] axiom1)) pr          d (MP imp p)               = let p'           = concl p                 in case concl imp of                  _ :=>: r' ->                      MP (MP (UseTheorem (instL [asm,p',r'] axiom2)) (d imp)) (d p)                  _         -> error "MP"`

With this function, we can now write the most important function: one which takes an object of our proof language and, if the proof is valid, spits out the proven theorem.

Code: Select all
`verify :: Proof -> Theorem Stringverify proof =   let v (UseTheorem t) = t      v (MP pr pr')    = case mp (v pr) (v pr') of        []     -> error "MP"        (t':_) -> t'  in case assms proof of    []  -> v proof    [a] -> v (discharge a proof)    as  -> error errorMsg      where errorMsg = "Undischarged assumptions:\n" ++                        unlines [ "  " ++ printTerm a | a <- as ]`

And now proofs are much easier to write. For example, the theorem "⊢ P → P", which took four lines when we used the kernel directly, can be produced simply with

Code: Select all
`verify (Assume p)`

Here's another simple example:

Code: Select all
`foo = let step1 = Assume p           step2 = Assume (p :=>: q)          step3 = MP step2 step1          step4 = discharge (p :=>: q) step3      in verify step4`

So we now have a new proof language which allows us to prove theorems in propositional logic which are still verified by our secure logical kernel. Our kernel was so simple as to be almost useless for proof, but we can build more convenient tools over the top without having to break the encapsulation of that secure kernel.

For a real challenge, you might try one of the exercises from Mendelson, where you have to prove "⊢ (¬P → Q) -> (¬P → ¬Q) → P".

I should probably stop there, but I think I should say something about the next stage. One of the things I wanted to do was to implement a language for equational reasoning. That way, if you can prove that one proposition is logically equivalent to another (say that ¬¬P ↔ P), then you can substitute occurrences of the left hand side with the right hand side.

The language we implement for this is called a "conversions" language. It is not based on an algebraic data-type, but is instead based on combinators. Combinators are just higher-order functions composed in a "point-free" style, so that you don't see the underlying inputs and outputs. There are interesting theoretical distinctions between these two styles of language. One language is defined by a syntax and is then given an explicit semantics. The other is defined directly by its semantics.

Code: Select all
`-- Basic conversions and conversionalsmodule Conversions whereimport Bootstrap hiding (matchMP)import Propositionalimport Utilsimport Control.Monad.Error-- Conversions wrap functions which take terms and derive equations. Each -- equation has an lhs which is the original term.newtype Conv a = Conv (Term a -> [Theorem a])applyC :: Conv a -> Term a -> [Theorem a]applyC (Conv c) term = c term-- Use a conversion to rewrite a theoremconvMP :: Conv String -> Theorem String -> [Theorem String]convMP c thm = do eq  <- applyC c (theoremTerm thm)                  imp <- matchMP eqMP eq                  mp imp thm-- Apply a conversion to the antecedent of a conditionalantC :: Conv String -> Conv StringantC (Conv c) = Conv f  where f (p :=>: q) = c p >>= matchMP substLeft'          where substLeft' = instM (Var . avoid (vars q)) [("p",q)] substLeft        f _          = []  -- Apply a conversion to the consequent of a conditional        conclC :: Conv String -> Conv StringconclC (Conv c) = Conv f  where f (p :=>: q) = c q >>= matchMP substRight'          where substRight' = instM (Var . avoid (vars p)) [("p",p)] substRight        f _          = []-- Apply a conversion to the body of a negationnotC :: Conv String -> Conv StringnotC (Conv c) = Conv f   where f (Not p) = c p >>= matchMP substNot        f _       = []        -- Attempt the left conversion, and if it fails, attempt the rightorC :: Conv a -> Conv a -> Conv aorC (Conv c) (Conv c') = Conv f  where f t = c t `mplus` c' t        -- Try all conversions which succeedtryC :: [Conv a] -> Conv atryC = foldr orC failC-- Apply a conversion based on the term to be convertedifC :: (Term a -> Bool) -> Conv a -> Conv aifC p c = Conv (\t -> if p t then applyC c t else [])-- Apply one conversion after anotherthenC :: Conv String -> Conv String -> Conv StringthenC c c' = Conv f  where f t = do thm   <- applyC c t                 r     <- rhs (theoremTerm thm)                 thm'  <- applyC c' r                 thm'' <- matchMP trans thm                 matchMP thm'' thm'        rhs (Not ((p :=>: q) :=>: Not (r :=>: s))) | p == s && q == r = return q        rhs _  = []        -- The zero for orConv and identity for thenConv: always succeedsallC :: Conv StringallC = Conv (\t -> return \$ instL [t] reflEq)-- The identity for orConv and zero for thenConv: always failsfailC :: Conv afailC = Conv (const [])-- Sequence conversionseveryC :: [Conv String] -> Conv StringeveryC = foldl thenC allC        isImp :: Term a -> Bool isImp (p :=>: q) = TrueisImp _          = FalseisNeg :: Term a -> BoolisNeg (Not p) = TrueisNeg _       = False-- Apply a conversion to the first applicable term on a depth first searchdepthConv1 :: Conv String -> Conv StringdepthConv1 c = tryC [ c                    , ifC isNeg (notC c')                    , ifC isImp (antC c' `orC` conclC c') ]  where c' = depthConv1 c`
This is a pretty rich combinator language already, with some nice algebraic structure, but the goal here is to be able to write lots of new more sophisticated conversions by composing the primitive conversions. It's kind of overkill for propositional logic, but when you're working in higher-order theories, you want to use this sort of language to build powerful rewrite based automation and domain specific rewriting automation.