Slightly Offtopic in Part
Hi folks The disjunction elimination rule: I've been trying to make sense of it and I think I have had some success; however, it's far from adequate. I wonder, is there a way of demonstrating it in Haskell? A code frag with a jargon-free explanation would be mucho appreciated. Cheers, Paul
I'm assuming you mean the rule described in http://en.wikibooks.org/wiki/Formal_Logic/Sentential_Logic/Inference_Rules
type Disj a b = Either a b
disj_elim :: Disj a b -> (a -> c) -> (b -> c) -> c disj_elim (Left a) a2c b2c = a2c a disj_elim (Right b) a2c b2c = b2c b
If you know "either a is true, or b is true"
and you know "from a, I can prove c",
and you know "from b, I can prove c",
then you can prove c.
-- ryan
On 2/8/08, PR Stanley
Hi folks The disjunction elimination rule: I've been trying to make sense of it and I think I have had some success; however, it's far from adequate. I wonder, is there a way of demonstrating it in Haskell? A code frag with a jargon-free explanation would be mucho appreciated. Cheers, Paul
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
On Fri, Feb 08, 2008 at 06:47:51PM -0800, Ryan Ingram wrote:
I'm assuming you mean the rule described in http://en.wikibooks.org/wiki/Formal_Logic/Sentential_Logic/Inference_Rules
type Disj a b = Either a b
disj_elim :: Disj a b -> (a -> c) -> (b -> c) -> c disj_elim (Left a) a2c b2c = a2c a disj_elim (Right b) a2c b2c = b2c b
If you know "either a is true, or b is true" and you know "from a, I can prove c", and you know "from b, I can prove c", then you can prove c.
aka: import Data.Either type Disj = Either disj_elim = either Stefan
For more details, look for a function called "orElim" in the write-up http://www.thenewsh.com/~newsham/formal/curryhoward/ Dan Ryan Ingram wrote:
I'm assuming you mean the rule described in http://en.wikibooks.org/wiki/Formal_Logic/Sentential_Logic/Inference_Rules
type Disj a b = Either a b
disj_elim :: Disj a b -> (a -> c) -> (b -> c) -> c disj_elim (Left a) a2c b2c = a2c a disj_elim (Right b) a2c b2c = b2c b
It should be emphasized that a type needs to be inhabited by (at least one) *total* function to prove a theorem. Otherwise, you could have the following partial function purporting to prove the phony theorem that "A or B implies A": phony :: Either a b -> a phony (Left a) = a Dan Dan Weston wrote:
For more details, look for a function called "orElim" in the write-up
http://www.thenewsh.com/~newsham/formal/curryhoward/
Dan
Ryan Ingram wrote:
I'm assuming you mean the rule described in http://en.wikibooks.org/wiki/Formal_Logic/Sentential_Logic/Inference_Rules
type Disj a b = Either a b
disj_elim :: Disj a b -> (a -> c) -> (b -> c) -> c disj_elim (Left a) a2c b2c = a2c a disj_elim (Right b) a2c b2c = b2c b
Out of context (am I missing some earlier part of this thread?) I'm not entirely sure what you mean. Are you're talking about the disjunction elim rule in intuitionistic natural deduction: Gamma |- A + B Gamma, A |- C Gamma, B |- C ---------------------------------------------- Gamma |- C If so, this is just 'case'. If you annotate the rule with proof terms (programs in the simply-typed lambda-calculus), you get the typing rule for case: Gamma |- e : A + B Gamma, x1 : A |- e1 : C Gamma, x2 : B |- e2 : C ------------------------------------------------------ Gamma |- case e of { Inl x1 -> e1 ; Inr x2 -> e2 } : C I.e., when pattern matching on the following type data Or a b = Inl a | Inr b (this type is isomorphic to Either in the Prelude) you have two cases to consider, one where you have an 'a' and the other where you have a 'b'. E.g., let's prove a simple theorem: comm :: Or a b -> Or b a comm x = case x of Inl x1 -> Inr x1 Inr x2 -> Inl x2 Does that help? -Dan On Feb09, PR Stanley wrote:
Hi folks The disjunction elimination rule: I've been trying to make sense of it and I think I have had some success; however, it's far from adequate. I wonder, is there a way of demonstrating it in Haskell? A code frag with a jargon-free explanation would be mucho appreciated. Cheers, Paul
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
participants (5)
-
Dan Licata -
Dan Weston -
PR Stanley -
Ryan Ingram -
Stefan O'Rear