Short theorem prover
(625 *character* theroum prover, and dissection (FIXME: looking like haddocks))
(found one more tweak, down to 590 ch)
Revision as of 02:08, 22 December 2006
Theorum prover in 590 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 > j f@(A l)s(A k)|h(||)(==l)s&&f/=s=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), 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 theorums, we need axioms and deduction rules. This theorum prover is based on the Curry-Howard-Lambek 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.
> 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 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:
> 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