You realize that Djinn can write all that code for you? :)<br>Well, not with your encoding of Not, but with a similar one.<br><br> -- Lennart<br><br><div><span class="gmail_quote">On 10/14/07, <b class="gmail_sendername">
Tim Newsham</b> <<a href="mailto:newsham@lava.net">newsham@lava.net</a>> wrote:</span><blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;">
I've been struggling with this for the last day and a half. I'm<br>trying to get some exercise with the type system and with logic by<br>playing with the curry-howard correspondence. I got stuck on<br>the excluded-middle, and I think now I got it almost all the way
<br>there, but its still not quite right. Is this error I'm getting<br>(inline at the end) easily fixed, and what exactly is going on?<br><br>---- code ---<br>{-# OPTIONS_GHC -fglasgow-exts #-}<br>module Classic where
<br>{-<br>Classic logic. (See Intuit.hs first).<br>In this system propositions all take a continuation. This allows<br>us to define the law of the excluded middle.<br>-}<br>import Control.Monad<br><br><br>-- propositions are functions taking a continuation.
<br>data Prop r p = Prop ((p -> r) -> r)<br>run :: Prop r p -> (p -> r) -> r<br>run (Prop f) k = f k<br>propCC :: ((p -> Prop r q) -> Prop r p) -> Prop r p<br>propCC f = Prop (\k -> run (f (\a -> Prop (\k' -> k a))) k)
<br>instance Monad (Prop r) where<br> return p = Prop (\c -> c p)<br> p >>= mkq = Prop (\c -> run p (\r -> run (mkq r) c))<br><br><br>data TRUTH = TRUTH<br>type FALSE r = Not r TRUTH<br>data And r p q = And (Prop r p) (Prop r q)
<br>data Or r p q = OrL (Prop r p) | OrR (Prop r q)<br>data Imp r p q = Imp (Prop r p -> Prop r q)<br>data Equiv r p q = Equiv (Prop r p -> Prop r q) (Prop r q -> Prop r p)<br>data Not r p = Not (forall q. (Prop r p -> Prop r q))
<br><br><br>-- Truth<br>truth :: Prop r TRUTH<br>truth = return TRUTH<br><br>-- And-Injection<br>-- P, Q |- P /\ Q<br>andInj :: Prop r p -> Prop r q -> Prop r (And r p q)<br>andInj p q = return (And p q)<br><br>-- And-Elimination, left and Right
<br>-- P /\ Q |- P<br>andElimL :: Prop r (And r p q) -> Prop r p<br>andElimL pq = pq >>= \(And p q) -> p<br>-- P /\ Q |- Q<br>andElimR :: Prop r (And r p q) -> Prop r q<br>andElimR pq = pq >>= \(And p q) -> q
<br><br>-- Or-Injection, left and right<br>-- P |- P \/ Q<br>orInjL :: Prop r p -> Prop r (Or r p q)<br>orInjL p = return (OrL p)<br>-- Q |- P \/ Q<br>orInjR :: Prop r q -> Prop r (Or r p q)<br>orInjR q = return (OrR q)
<br><br>-- Or-Elimination.<br>-- P \/ Q, P -> R, Q -> R |- R<br>orElim :: Prop r (Or r p q) -> (Prop r p -> Prop r s) -> (Prop r q -> Prop r s) -> Prop r s<br>orElim pORq p2r q2r = pORq >>= byCases
<br> where byCases (OrL p) = p2r p<br> byCases (OrR q) = q2r q<br><br>-- Implication-Injection<br>-- (P |- Q) |- P -> Q<br>impInj :: (Prop r p -> Prop r q) -> Prop r (Imp r p q)<br>impInj p2q = return (Imp p2q)
<br><br>-- Implication-elimination (modus ponen)<br>-- P, P -> Q |- Q<br>impElim :: Prop r p -> Prop r (Imp r p q) -> Prop r q<br>impElim p pIMPq = pIMPq >>= \(Imp p2q) -> p2q p<br><br>-- Equivalence-Injection
<br>-- P -> Q, Q -> P |- P = Q<br>equivInj :: Prop r (Imp r p q) -> Prop r (Imp r q p) -> Prop r (Equiv r p q)<br>equivInj pIMPq qIMPp = do<br> (Imp p2q) <- pIMPq<br> (Imp q2p) <- qIMPp<br> return (Equiv p2q q2p)
<br><br>-- Equivalence-Elimination, Left and Right<br>-- P = Q |- P -> Q<br>equivElimL :: Prop r (Equiv r p q) -> Prop r (Imp r p q)<br>equivElimL pEQq = pEQq >>= \(Equiv p2q q2p) -> return (Imp p2q)<br>equivElimR :: Prop r (Equiv r p q) -> Prop r (Imp r q p)
<br>equivElimR pEQq = pEQq >>= \(Equiv p2q q2p) -> return (Imp q2p)<br><br>-- Absurdity<br>-- False |- P<br>absurd :: Prop r (FALSE r) -> Prop r p<br>absurd false = false >>= \(Not true2p) -> true2p truth
<br><br>-- Not-Inj<br>-- (P |- False) |- ~P<br>notInj :: forall r p. (Prop r p -> Prop r (FALSE r)) -> Prop r (Not r p)<br>notInj p2false = return (Not p2any)<br> where p2any :: forall q. Prop r p -> Prop r q<br>
p2any assumep = absurd (p2false assumep)<br><br>-- Not-Elimination<br>-- P, ~P |- Q<br>notElim :: Prop r p -> Prop r (Not r p) -> Prop r q<br>notElim p np = np >>= \(Not p2any) -> p2any p<br><br><br>
-- Excluded-Middle<br>-- P \/ ~P<br>exclMiddle :: forall r p. Prop r (Or r p (Not r p))<br>exclMiddle = propCC func1<br> where func1 :: (Or r p (Not r p) -> Prop r q) -> Prop r (Or r p (Not r p))<br> -- k :: Or r p (Not r p) -> Prop r q
<br> func1 k = return (OrR (return (Not func2)))<br> where func2 :: Prop r p -> Prop r q<br> func2 k' = k (OrL k')<br><br>{-<br><a href="http://www.cse.ogi.edu/~magnus/mdo-callcc-slides.pdf">
http://www.cse.ogi.edu/~magnus/mdo-callcc-slides.pdf</a><br>-- A \/ ~A<br>excmid :: Either a (a -> b)<br>excmid = callcc (\k. Right (\a.k (Left a)))<br>-}<br><br>{-<br>Classic2.hs:114:27:<br> Couldn't match expected type `q' (a rigid variable)
<br> against inferred type `q1' (a rigid variable)<br> `q' is bound by the type signature for `func2'<br> at Classic2.hs:113:44<br> `q1' is bound by the type signature for `func1'
<br> at Classic2.hs:110:45<br> Expected type: Prop r q<br> Inferred type: Prop r q1<br> In the expression: k (OrL k')<br> In the definition of `func2': func2 k' = k (OrL k')<br>
-}<br><br><br>-- False-Elimination<br>-- (~P |- False) |- P<br><br>Tim Newsham<br><a href="http://www.thenewsh.com/~newsham/">http://www.thenewsh.com/~newsham/</a><br>_______________________________________________<br>Haskell-Cafe mailing list
<br><a href="mailto:Haskell-Cafe@haskell.org">Haskell-Cafe@haskell.org</a><br><a href="http://www.haskell.org/mailman/listinfo/haskell-cafe">http://www.haskell.org/mailman/listinfo/haskell-cafe</a><br></blockquote></div><br>