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
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
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)
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
--
G
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
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
__
