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

[GHC]

#13038: implementation of Modus ponens and Modus tollens
-------------------------------------+-------------------------------------
        Reporter:  vanto             |                Owner:  (none)
            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):

 Replying to [[span(style=color: #FF0000, AntC )]]:\\
 Here is an example.\\
 P and Q are propositions (statements).\\
 v(P) and v(Q) are logic values.\\
 We say: if P is True : v(P) = 1; if P is False: v(P) = 0; idem for Q and
 v(Q).\\
 First:\\
 let the expression :{{{length (xs ++ (y:ys)) = 1 + length xs + length
 ys}}} We will prove that this expression is True.\\
 we know that: {{{length (xs ++ ys) = length xs ++ length ys}}} is True.
 So,\\

 {{{
 length (xs ++ (y:ys))
       = length xs + length (y:ys)
       = length xs + (1 + length ys)
       = 1 + length xs + length ys
 }}}
 Demonstration of Modus Tollens:\\

 {{{
 let xs = [1,2,3]
 let y:ys = [4,5,6]
 }}}
 Attention to the following: you have to replace v(P) by the
 variable{{{a}}} and v(Q) by the variable {{{b}}}, for instance, in GHCi
 for a good functioning.\\

 {{{let v(P) = length (xs ++ (y:ys))}}} is 1\\

 {{{let v(Q) = 1 + length xs + length ys}}} is 1\\
 let the implication: v(length (xs ++ (y:ys)) -> 1 + length xs + length ys)
 is 1.
 Remember the implication:\\

 {{{
 P       Q       P->Q
 False   False   True
 False   True    True
 True    False   False
 True    True    True
 }}}
 explanation of Modus Tollens:\\
 Theorem :v(P->Q), (not)v(Q){{{|-}}}(not)v(P)\\
 This theorem become new inference rule:\\

 {{{
 v(P->Q)   (not)v(Q)
 _________________{modTol}
     (not)v(P)
 }}}
 Now consider the values of v(P) and v(Q) as real values (equal to 1 since
 they are True)\\
 (not)v(Q) = negate q = -6 is 0\\
 the implication v(P->Q) is 1\\
 so, (not)v(P) = negate p = -6 is 0\\
 we have just inferred in the opposite direction of the Modus Ponens (from
 the conclusion and towards the premise).\\
 I point out that my idea is to insert the Modus Tollens inside the type
 inference algorithm or it will make sense rather than control a
 finalized expression. We could put it in touch with Typed Hole, for
 example, to specify the answer of the compiler.
 Modus Tollens is not specific to programming, it can be found in
 electronic circuits.(We can build AND,OR,NAND Gates ...)\\
 Hope that help. I stop here. Thank you.

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