[GHC] #13038: implementation of Modus ponens and Modus tollens

[GHC]

#13038: implementation of Modus ponens and Modus tollens
-------------------------------------+-------------------------------------
        Reporter:  vanto             |                Owner:
            Type:  feature request   |               Status:  infoneeded
        Priority:  normal            |            Milestone:
       Component:  libraries/base    |              Version:  8.0.1
      Resolution:                    |             Keywords:
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by vanto):

 The truth tables for mod_ponens and mod_tollens are the same as the truth
 table of logical implication. For mod_ponens the entrance is at a=1 and
 the exit is at b=1. For
 mod_tollens the entrance is at b=0 and the exit is at a=0. mod_ponens is
 not like a conjonction likewise mod_tollens is not like a negative
 disjonction. They are rules of inference.[[BR]]
 Read mod_ponens like this: From A and (A implies B), infer B.[[BR]]
 And for mod_tollens read this: From (not B) and (A implies B), infer (not
 A).[[BR]]
 If you want more details read the Hilbert system which is a deductive
 reasoning, please.[[BR]]
 I looked in the archive mailing list about logical implication. Sometimes
 people get confused about the logical implication. If we write
 "if...then..." into a piece of code it is not a logical implication. If we
 talk and say "if...then..." we can suppose and deduce a logical
 implication. Do you understand the difference?[[BR]]
 In Haskell we can consider two things. Give a name to the function or name
 the function using a symbol. The name may be "imply" or "implies" or
 "impl" or other. The symbol can be ->. or -. or -|> or -|>. or -| or -|.
 or ->|  or other.[[BR]]
 I am not running a second discussion on the logical implication. If the
 committee agree with the logical implication to be put in Haskell then it
 is ok and you can submit a patch instead of me. If the committee agree
 with mod_ponens and mod_tollens, idem. From my point of view, these three
 things have their place in the Haskell language.[[BR]]
 Happy new year!

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/13038#comment:4>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler