Difference between revisions of "Short theorem prover"
(625 *character* theroum prover, and dissection (FIXME: looking like haddocks)) 
m 

(5 intermediate revisions by 3 users not shown)  
Line 1:  Line 1:  
−  +  Theorem prover in 625 characters of Haskell 

−  
−  > import Monad;import Maybe;import List 

−  > infixr 9 ? 

−  > (?)=(:>);z=Just;y=True 

−  > data P=A IntegerP:>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 ji y b j 

−  > j(A l)s(A k)i False s l=Nothingl==k=z sy=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> 

+  import Monad;import Maybe;import List 

+  infixr 9 ? 

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

+  data P=A IntegerP:>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 ji y b j 

+  j(A l)s(A k)i False s l=Nothingl==k=z sy=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=readLn>>=print.(`elem`m) 

+  </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> 

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

+  type U = Integer 

−  > infixr 9 :> 

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

−  
+  infixr 9 :> 

−  To prove theorums, we need axioms and deduction rules. This theorum prover is based on the [[CurryHowardLambek correspondance]] 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> 

−  
+  To prove theorems, we need axioms and deduction rules. This theorem prover is based on the [[CurryHowardLambek 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] 

+  <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) 

−  > 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 

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

−  +  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 (A i) s (A j)  cnt False s i = Nothing 

+  unify :: P > P > P > Maybe P 

−  >  i == j = Just $ s 

+  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 x = pmap (toInteger . fromJust . flip elemIndex ( allvars x )) x 

+  canon :: P > P 

−  > allvars :: P > [U] 

+  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= 
+  main=readLn>>=print.(`elem`facts) 
+  </haskell> 

+  [[Category:Code]] 
Latest revision as of 08:23, 13 December 2009
Theorem prover in 625 characters of Haskell
import Monad;import Maybe;import List
infixr 9 ?
(?)=(:>);z=Just;y=True
data P=A IntegerP:>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 ji y b j
j(A l)s(A k)i False s l=Nothingl==k=z sy=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=readLn>>=print.(`elem`m)
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.
type 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 CurryHowardLambek 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
In order to avoid infinite types (which are not intrinsically dangerous in a programming language but wreak havoc in logic because terms such as fix a. (a > b)
correspond to statements such as "this statement is false"), we check whether the replaced variable is mentioned in the replacing term:
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=readLn>>=print.(`elem`facts)