# Short theorem prover

### From HaskellWiki

BrettGiles (Talk | contribs) m (Short theorum prover moved to Short theorem prover) |
BrettGiles (Talk | contribs) (Spelling and format) |
||

Line 1: | Line 1: | ||

− | + | Theoreum prover in 625 characters of Haskell | |

− | + | ||

− | + | ||

− | + | ||

− | + | ||

− | + | ||

− | + | ||

− | + | ||

− | + | ||

− | + | ||

− | + | ||

− | + | ||

− | + | ||

− | + | ||

− | + | ||

− | + | ||

− | + | ||

− | + | ||

− | + | ||

− | + | ||

+ | <haskell> | ||

+ | import Monad;import Maybe;import List | ||

+ | infixr 9 ? | ||

+ | (?)=(:>);z=Just;y=True | ||

+ | data P=A Integer|P:>P deriving(Read,Show,Eq) | ||

+ | [a,b,c,d,e,f]=map A[1,3..11] | ||

+ | g=h(?).(A.) | ||

+ | h f z(A x)=z x | ||

+ | h f z(x:>y)=h f z x`f`h f z y | ||

+ | i p(A i)j=p&&i==j | ||

+ | i p(a:>b)j=i y a j||i y b j | ||

+ | j(A l)s(A k)|i False s l=Nothing|l==k=z s|y=z$A k | ||

+ | j f@(A i)s(a:>b)=liftM2(?)(j f s a)(j f s b) | ||

+ | j f s@(A i)p=j s f p | ||

+ | j(a:>b)(c:>d)p=let u=j a c in join$liftM3 j(u b)(u d)(u p) | ||

+ | l x=g(toInteger.fromJust.flip elemIndex (h union (:[]) x))x | ||

+ | m=(a?a:)$map l$catMaybes$liftM2(uncurry.j.g(*2))m[((((a?b?c) | ||

+ | ?(a?b)?a?c)?(d?e?d)?f),f),((a?b),(c?a)?c?b)] | ||

+ | main=getLine>>=print.(`elem`m).read | ||

+ | </haskell> | ||

You are not expected to understand that, so here is the explanation: | You are not expected to understand that, so here is the explanation: | ||

− | First, we need a type of prepositions. Each A constructor represents a prepositional variable (a, b, c, etc), and :> represents implication. Thus, for example, (A 0 :> A 0) is the axiom of tautology in classical logic. | + | First, we need a type of prepositions. Each A constructor represents a prepositional variable (a, b, c, etc), and <hask>:></hask> represents implication. Thus, for example, <hask>(A 0 :> A 0)</hask> is the axiom of tautology in classical logic. |

− | > type U = Integer | + | <haskell> |

− | + | type U = Integer | |

− | + | data P = A U | P:>P deriving(Read,Show,Eq) | |

− | + | infixr 9 :> | |

− | To prove | + | </haskell> |

− | + | To prove theorems, we need axioms and deduction rules. This theorem prover is based on the [[Curry-Howard-Lambek correspondence]] applied to the programming language Jot (http://ling.ucsd.edu/~barker/Iota/#Goedel). Thus, we have a single basic combinator and two deduction rules, corresponding to partial application of the base case and two combinators of Jot. | |

− | + | ||

− | + | ||

+ | <haskell> | ||

+ | axiom = A 0:>A 0 | ||

+ | rules = let[a,b,c,d,e,f]=map A[1,3..11]in[ (((a:>b:>c):>(a:>b):>a:>c):>(d:>e:>d):>f):>f, (a:>b):>(c:>a):>c:>b] | ||

+ | </haskell> | ||

We will also define foogomorphisms on the data structure: | We will also define foogomorphisms on the data structure: | ||

− | > pmap :: (U -> U) -> P -> P | + | <haskell> |

− | + | pmap :: (U -> U) -> P -> P | |

− | + | pmap f = pfold (:>) (A .f) | |

− | + | ||

− | + | ||

− | + | ||

− | + | ||

− | + | ||

− | > cnt p(A i) j = p && i == j | + | pfold :: (a -> a -> a) -> (U -> a) -> P -> a |

− | + | pfold f z (A x) = z x | |

+ | pfold f z (x:>y) = pfold f z x`f`pfold f z y | ||

+ | </haskell> | ||

+ | In order to avoid infinite types (which are not intrinsically dangerous in a programming language but wreak havoc in logic because terms such as <hask>fix a. (a -> b)</hask> correspond to statements such as "this statement is false"), we check whether the replaced variable is mentioned in the replacing term: | ||

+ | <haskell> | ||

+ | cnt p(A i) j = p && i == j | ||

+ | cnt p(a:>b) j = cnt True a j || cnt True b j | ||

+ | </haskell> | ||

The deduction steps are performed by a standard unification routine: | The deduction steps are performed by a standard unification routine: | ||

− | > unify :: P -> P -> P -> Maybe P | + | <haskell> |

− | + | unify :: P -> P -> P -> Maybe P | |

− | + | unify (A i) s (A j) | cnt False s i = Nothing | |

− | + | | i == j = Just $ s | |

− | + | | otherwise = Just $ A j | |

− | + | unify f@(A i) s (a:>b) = liftM2 (:>) (unify f s a) (unify f s b) | |

− | + | unify f s@(A i) pl = unify s f pl | |

+ | unify (a:>b) (c:>d) pl = let u = unify a c in join $ liftM3 unify (u b) (u d) (u pl) | ||

+ | </haskell> | ||

We need to renumber terms to prevent name conflicts. | We need to renumber terms to prevent name conflicts. | ||

− | > fan (A x) = A (x*2) | + | <haskell> |

− | + | fan (A x) = A (x*2) | |

+ | fan (x:>y)= fan x:> fan y | ||

+ | </haskell> | ||

Make a deduction given a rule, by setting the LHS of the rule equal to the state and taking the RHS of the rule. | Make a deduction given a rule, by setting the LHS of the rule equal to the state and taking the RHS of the rule. | ||

− | > deduce t r = let (a:>b)=r in unify (fan t) a b | + | <haskell> |

+ | deduce t r = let (a:>b)=r in unify (fan t) a b | ||

+ | </haskell> | ||

Canonicalize the numbers in the rule, thus allowing matching. | Canonicalize the numbers in the rule, thus allowing matching. | ||

− | > canon :: P -> P | + | <haskell> |

− | + | canon :: P -> P | |

− | + | canon x = pmap (toInteger . fromJust . flip elemIndex ( allvars x )) x | |

− | + | allvars :: P -> [U] | |

+ | allvars = pfold union (:[]) | ||

+ | </haskell> | ||

Given this, we can lazily construct the list of all true statements: | Given this, we can lazily construct the list of all true statements: | ||

− | > facts = nub $ (axiom:) $ map canon $ catMaybes $ liftM2 deduce facts rules | + | <haskell> |

+ | facts = nub $ (axiom:) $ map canon $ catMaybes $ liftM2 deduce facts rules | ||

main=getLine>>=print.(`elem`facts).read | main=getLine>>=print.(`elem`facts).read | ||

+ | </haskell> | ||

[[Category:Code]] | [[Category:Code]] |

## Revision as of 17:11, 22 December 2006

Theoreum prover in 625 characters of Haskell

import Monad;import Maybe;import List infixr 9 ? (?)=(:>);z=Just;y=True data P=A Integer|P:>P deriving(Read,Show,Eq) [a,b,c,d,e,f]=map A[1,3..11] g=h(?).(A.) h f z(A x)=z x h f z(x:>y)=h f z x`f`h f z y i p(A i)j=p&&i==j i p(a:>b)j=i y a j||i y b j j(A l)s(A k)|i False s l=Nothing|l==k=z s|y=z$A k j f@(A i)s(a:>b)=liftM2(?)(j f s a)(j f s b) j f s@(A i)p=j s f p j(a:>b)(c:>d)p=let u=j a c in join$liftM3 j(u b)(u d)(u p) l x=g(toInteger.fromJust.flip elemIndex (h union (:[]) x))x m=(a?a:)$map l$catMaybes$liftM2(uncurry.j.g(*2))m[((((a?b?c) ?(a?b)?a?c)?(d?e?d)?f),f),((a?b),(c?a)?c?b)] main=getLine>>=print.(`elem`m).read

You are not expected to understand that, so here is the explanation:

First, we need a type of prepositions. Each A constructor represents a prepositional variable (a, b, c, etc), andtype U = Integer data P = A U | P:>P deriving(Read,Show,Eq) infixr 9 :>

To prove theorems, we need axioms and deduction rules. This theorem prover is based on the Curry-Howard-Lambek correspondence applied to the programming language Jot (http://ling.ucsd.edu/~barker/Iota/#Goedel). Thus, we have a single basic combinator and two deduction rules, corresponding to partial application of the base case and two combinators of Jot.

axiom = A 0:>A 0 rules = let[a,b,c,d,e,f]=map A[1,3..11]in[ (((a:>b:>c):>(a:>b):>a:>c):>(d:>e:>d):>f):>f, (a:>b):>(c:>a):>c:>b]

We will also define foogomorphisms on the data structure:

pmap :: (U -> U) -> P -> P pmap f = pfold (:>) (A .f) pfold :: (a -> a -> a) -> (U -> a) -> P -> a pfold f z (A x) = z x pfold f z (x:>y) = pfold f z x`f`pfold f z y

cnt p(A i) j = p && i == j cnt p(a:>b) j = cnt True a j || cnt True b j

The deduction steps are performed by a standard unification routine:

unify :: P -> P -> P -> Maybe P unify (A i) s (A j) | cnt False s i = Nothing | i == j = Just $ s | otherwise = Just $ A j unify f@(A i) s (a:>b) = liftM2 (:>) (unify f s a) (unify f s b) unify f s@(A i) pl = unify s f pl unify (a:>b) (c:>d) pl = let u = unify a c in join $ liftM3 unify (u b) (u d) (u pl)

We need to renumber terms to prevent name conflicts.

fan (A x) = A (x*2) fan (x:>y)= fan x:> fan y

Make a deduction given a rule, by setting the LHS of the rule equal to the state and taking the RHS of the rule.

deduce t r = let (a:>b)=r in unify (fan t) a b

Canonicalize the numbers in the rule, thus allowing matching.

canon :: P -> P canon x = pmap (toInteger . fromJust . flip elemIndex ( allvars x )) x allvars :: P -> [U] allvars = pfold union (:[])

Given this, we can lazily construct the list of all true statements:

facts = nub $ (axiom:) $ map canon $ catMaybes $ liftM2 deduce facts rules main=getLine>>=print.(`elem`facts).read