Posted:

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

Any more interesting tidbits of related Haskell code?

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