#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