On 10/14/07, Tim Newsham wrote:

I've been struggling with this for the last day and a half. I'm trying to get some exercise with the type system and with logic by playing with the curry-howard correspondence. I got stuck on the excluded-middle, and I think now I got it almost all the way there, but its still not quite right. Is this error I'm getting (inline at the end) easily fixed, and what exactly is going on?

I'll admit this is a cursory response, but (to my understanding) excluded middle doesn't hold in the Curry-Howard correspondence. It is an isomorphism between *constructive* logic and types; excluded middle is a nonconstructive axiom. Luke

You realize that Djinn can write all that code for you? :) Well, not with your encoding of Not, but with a similar one. -- Lennart On 10/14/07, Tim Newsham wrote:

I've been struggling with this for the last day and a half. I'm trying to get some exercise with the type system and with logic by playing with the curry-howard correspondence. I got stuck on the excluded-middle, and I think now I got it almost all the way there, but its still not quite right. Is this error I'm getting (inline at the end) easily fixed, and what exactly is going on?

---- code --- {-# OPTIONS_GHC -fglasgow-exts #-} module Classic where {- Classic logic. (See Intuit.hs first). In this system propositions all take a continuation. This allows us to define the law of the excluded middle. -} import Control.Monad

-- propositions are functions taking a continuation. data Prop r p = Prop ((p -> r) -> r) run :: Prop r p -> (p -> r) -> r run (Prop f) k = f k propCC :: ((p -> Prop r q) -> Prop r p) -> Prop r p propCC f = Prop (\k -> run (f (\a -> Prop (\k' -> k a))) k) instance Monad (Prop r) where return p = Prop (\c -> c p) p >>= mkq = Prop (\c -> run p (\r -> run (mkq r) c))

data TRUTH = TRUTH type FALSE r = Not r TRUTH data And r p q = And (Prop r p) (Prop r q) data Or r p q = OrL (Prop r p) | OrR (Prop r q) data Imp r p q = Imp (Prop r p -> Prop r q) data Equiv r p q = Equiv (Prop r p -> Prop r q) (Prop r q -> Prop r p) data Not r p = Not (forall q. (Prop r p -> Prop r q))

-- Truth truth :: Prop r TRUTH truth = return TRUTH

-- And-Injection -- P, Q |- P /\ Q andInj :: Prop r p -> Prop r q -> Prop r (And r p q) andInj p q = return (And p q)

-- And-Elimination, left and Right -- P /\ Q |- P andElimL :: Prop r (And r p q) -> Prop r p andElimL pq = pq >>= \(And p q) -> p -- P /\ Q |- Q andElimR :: Prop r (And r p q) -> Prop r q andElimR pq = pq >>= \(And p q) -> q

-- Or-Injection, left and right -- P |- P \/ Q orInjL :: Prop r p -> Prop r (Or r p q) orInjL p = return (OrL p) -- Q |- P \/ Q orInjR :: Prop r q -> Prop r (Or r p q) orInjR q = return (OrR q)

-- Or-Elimination. -- P \/ Q, P -> R, Q -> R |- R orElim :: Prop r (Or r p q) -> (Prop r p -> Prop r s) -> (Prop r q -> Prop r s) -> Prop r s orElim pORq p2r q2r = pORq >>= byCases where byCases (OrL p) = p2r p byCases (OrR q) = q2r q

-- Implication-Injection -- (P |- Q) |- P -> Q impInj :: (Prop r p -> Prop r q) -> Prop r (Imp r p q) impInj p2q = return (Imp p2q)

-- Implication-elimination (modus ponen) -- P, P -> Q |- Q impElim :: Prop r p -> Prop r (Imp r p q) -> Prop r q impElim p pIMPq = pIMPq >>= \(Imp p2q) -> p2q p

-- Equivalence-Injection -- P -> Q, Q -> P |- P = Q equivInj :: Prop r (Imp r p q) -> Prop r (Imp r q p) -> Prop r (Equiv r p q) equivInj pIMPq qIMPp = do (Imp p2q) <- pIMPq (Imp q2p) <- qIMPp return (Equiv p2q q2p)

-- Equivalence-Elimination, Left and Right -- P = Q |- P -> Q equivElimL :: Prop r (Equiv r p q) -> Prop r (Imp r p q) equivElimL pEQq = pEQq >>= \(Equiv p2q q2p) -> return (Imp p2q) equivElimR :: Prop r (Equiv r p q) -> Prop r (Imp r q p) equivElimR pEQq = pEQq >>= \(Equiv p2q q2p) -> return (Imp q2p)

-- Absurdity -- False |- P absurd :: Prop r (FALSE r) -> Prop r p absurd false = false >>= \(Not true2p) -> true2p truth

-- Not-Inj -- (P |- False) |- ~P notInj :: forall r p. (Prop r p -> Prop r (FALSE r)) -> Prop r (Not r p) notInj p2false = return (Not p2any) where p2any :: forall q. Prop r p -> Prop r q p2any assumep = absurd (p2false assumep)

-- Not-Elimination -- P, ~P |- Q notElim :: Prop r p -> Prop r (Not r p) -> Prop r q notElim p np = np >>= \(Not p2any) -> p2any p

-- Excluded-Middle -- P \/ ~P exclMiddle :: forall r p. Prop r (Or r p (Not r p)) exclMiddle = propCC func1 where func1 :: (Or r p (Not r p) -> Prop r q) -> Prop r (Or r p (Not r p)) -- k :: Or r p (Not r p) -> Prop r q func1 k = return (OrR (return (Not func2))) where func2 :: Prop r p -> Prop r q func2 k' = k (OrL k')

{- http://www.cse.ogi.edu/~magnus/mdo-callcc-slides.pdf -- A \/ ~A excmid :: Either a (a -> b) excmid = callcc (\k. Right (\a.k (Left a))) -}

{- Classic2.hs:114:27: Couldn't match expected type `q' (a rigid variable) against inferred type `q1' (a rigid variable) `q' is bound by the type signature for `func2' at Classic2.hs:113:44 `q1' is bound by the type signature for `func1' at Classic2.hs:110:45 Expected type: Prop r q Inferred type: Prop r q1 In the expression: k (OrL k') In the definition of `func2': func2 k' = k (OrL k') -}

-- False-Elimination -- (~P |- False) |- P

Tim Newsham http://www.thenewsh.com/~newsham/ _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe