[Haskell-cafe] haskell-curry, classical logic, excluded middle

[Lennart Augustsson]

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 <newsham at lava.net> 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 at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-cafe/attachments/20071014/66280f86/attachment-0001.htm