Personal tools

Short theorem prover

From HaskellWiki

(Difference between revisions)
Jump to: navigation, search
m (cat:code)
Current revision (08:23, 13 December 2009) (edit) (undo)
m
 
(3 intermediate revisions not shown.)
Line 1: Line 1:
-
Theorum prover in 625 characters of Haskell
+
Theorem 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
+
 +
<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=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 [[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.
+
</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.
-
> 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 f = pfold (:>) (A .f)
+
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
+
pfold :: (a -> a -> a) -> (U -> a) -> P -> a
-
> cnt p(a:>b) j = cnt True a j || cnt True b j
+
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
-
> | otherwise = Just $ A j
+
| i == j = Just $ s
-
> unify f@(A i) s (a:>b) = liftM2 (:>) (unify f s a) (unify f s b)
+
| otherwise = Just $ A j
-
> unify f s@(A i) pl = unify s f pl
+
unify f@(A i) s (a:>b) = liftM2 (:>) (unify f s a) (unify f s b)
-
> unify (a:>b) (c:>d) pl = let u = unify a c in join $ liftM3 unify (u b) (u d) (u pl)
+
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 (x:>y)= fan x:> fan y
+
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 = pfold union (:[])
+
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=readLn>>=print.(`elem`facts)
 +
</haskell>
[[Category:Code]]
[[Category:Code]]

Current revision

Theorem 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=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 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
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)
Retrieved from "http://www.haskell.org/haskellwiki/Short_theorem_prover"

Category: Code