rationalskepticism.org

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 where

import Propositional
import Utils

import 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 String
concl = snd . sequent

assms :: 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 → P
truth :: Theorem String
truth = 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 step4

discharge :: Term String -> Proof -> Proof
discharge 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 String
verify 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 conversionals

module Conversions where

import Bootstrap hiding (matchMP)
import Propositional
import Utils
import 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 theorem
convMP :: 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 conditional
antC :: Conv String -> Conv String
antC (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 String
conclC (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 negation
notC :: Conv String -> Conv String
notC (Conv c) = Conv f
  where f (Not p) = c p >>= matchMP substNot
        f _       = []
       
-- Attempt the left conversion, and if it fails, attempt the right
orC :: Conv a -> Conv a -> Conv a
orC (Conv c) (Conv c') = Conv f
  where f t = c t `mplus` c' t
       
-- Try all conversions which succeed
tryC :: [Conv a] -> Conv a
tryC = foldr orC failC

-- Apply a conversion based on the term to be converted
ifC :: (Term a -> Bool) -> Conv a -> Conv a
ifC p c = Conv (\t -> if p t then applyC c t else [])

-- Apply one conversion after another
thenC :: Conv String -> Conv String -> Conv String
thenC 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 succeeds
allC :: Conv String
allC = Conv (\t -> return $ instL [t] reflEq)

-- The identity for orConv and zero for thenConv: always fails
failC :: Conv a
failC = Conv (const [])

-- Sequence conversions
everyC :: [Conv String] -> Conv String
everyC = foldl thenC allC
       
isImp :: Term a -> Bool
isImp (p :=>: q) = True
isImp _          = False

isNeg :: Term a -> Bool
isNeg (Not p) = True
isNeg _       = False

-- Apply a conversion to the first applicable term on a depth first search
depthConv1 :: Conv String -> Conv String
depthConv1 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.