[GHC] #13038: implementation of Modus ponens and Modus tollens
#13038: implementation of Modus ponens and Modus tollens -------------------------------------+------------------------------------- Reporter: vanto | Owner: Type: feature | Status: new request | Priority: normal | Milestone: Component: | Version: 8.0.1 libraries/base | Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- Can we have in Prelude - Booleans, Modus ponens and Modus tollens implemented? Or in another module? reminder:[[BR]] P is a proposition and v(p) is the logic value of P.[[BR]] P is true, v(P) = 1[[BR]] P is false, v(P) = 0[[BR]] P -> Q is always true in propositional logic. Modus ponens:[[BR]] v(P) = 1[[BR]] v(P -> Q) = 1[[BR]] v(Q) = 1[[BR]] v(P) and v(P -> q) are premiss, v(q) is the conclusion.[[BR]] or in a more general form[[BR]] P : X is A[[BR]] P -> Q : A -> B[[BR]] Q : X is B[[BR]] Modus tollens:[[BR]] v(Q) = 0[[BR]] v(P -> Q) = 1[[BR]] v(P) = 0[[BR]] v(Q) and v(P -> Q) are premiss, v(P) is the conclusion.[[BR]] or in a more general form[[BR]] not Q : X is not B[[BR]] P -> Q : A -> B[[BR]] not P : X is not A[[BR]][[BR]] As well as using the numbers 0 and 1 for the respective values false and true, we'll use the letters F for False and T for True.[[BR]] We are always:[[BR]] v(F) = 0[[BR]] v(T) = 1[[BR]] v(P -> Q) = 1[[BR]] -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13038 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * status: new => infoneeded Comment: I have no idea what you are proposing in terms of Haskell code. What are the functions' names, type signatures, and implementations? Moreover, Trac is not the place to be making proposals for API additions in core libraries like `base`. Please propose these functions at the [https://mail.haskell.org/mailman/listinfo/libraries Haskell libraries mailing list] first to see if there is a consensus that these functions really should be added in the first place. If there is community support, we can revisit this idea. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13038#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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): Here is the code[[BR]] a is v(p) and b is v(q) and the implies function is separate and can be used independently of the other functions.[[BR]] {{{ implies::Bool->Bool->Bool implies a b = (||) (not a) b mod_ponens :: Bool -> Bool -> Bool mod_ponens a b = if a==True && implies a b == True then True else False mod_tollens :: Bool -> Bool -> Bool mod_tollens a b = if b==False && implies a b == True then True else False }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13038#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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 RyanGlScott): Thanks. You'll notice that if you examine the truth tables for `mod_ponens` and `mod_tollens`, you'll notice that: {{{#!hs mod_ponens = (&&) }}} and {{{#!hs mod_tollens x y = not (x || y) }}} I don't think either of these things break the Fairbairn threshold. The `implies` function [https://mail.haskell.org/pipermail/libraries/2016-January/026559.html Haskell has been proposed before on the libraries mailing list]. The consensus seemed to be that folks were generally supportive of the idea of introducing an `implies` function to `Data.Bool` (though the idea did have some detractors). You might wish to start a new libraries mailing list thread to see if that's still the case. If there's clear support, then feel free to submit a patch that adds `implies` to `base` via Phabricator. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13038#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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
#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): I have rewrite the two functions.[[BR]] Here are simpler and concise functions.[[BR]] We understand better the rules of inference.[[BR]] {{{ mod_ponens :: Bool -> Bool -> Bool mod_ponens a b = a && implies a b mod_tollens :: Bool -> Bool -> Bool mod_tollens a b = not b && implies a b }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13038#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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 Iceland_jack): Regarding adding `implies` (`(==>)`), [https://ghc.haskell.org/trac/ghc/ticket/10592#comment:12 here is the hierarchy] I'm most intrigued by {{{#!hs class Boolean (Logic a) => Eq a where type Logic a :: Type (==) :: a -> a -> Logic a class Eq a => POrd a where inf :: a -> a -> a class POrd a => MinBound a where minBound :: a class POrd a => Lattice a where sup :: a -> a -> a class (Lattice a, MinBound a) => Bounded a where maxBound :: a class Bounded a => Complemented a where not :: a -> a class Bounded a => Heyting a where infixr 3 ==> (==>) :: a -> a -> a class (Complemented a, Heyting a) => Boolean a }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13038#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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): The H.M algorithm is based on the reasoning of the Modus Ponens.\\ 1) f is a function that maps arguments of type A to results of type B.\\ {{{ f :: A -> B is identical to v(P -> Q) = 1 }}} 2) e is an expression of type A\\ {{{ e :: A is identical to v(P) = 1 }}} 3) Then the application f e has type B\\ {{{ f e :: B is identical to v(Q) = 1 }}} The inference algorithm tells us which type has a value, but it does not tell us what type does not have the value. I also think it is important for the compiler to know what types the value does not have. To know this, we must infer the inverse of the algorithm and must use the Modus Tollens.\\ {{{ 1) f e :: not B is identical to v(Q) = 0 }}} {{{ 2) f :: A -> B is identical to v(P -> Q) = 1 }}} {{{ 3) e :: not A is identical to v(P) = 0 }}} The utility of Modus tollens is complementary for many checks. I also propose that an inference algorithm based on Modus Tollens be coded in GHC. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13038#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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 AntC): Replying to [comment:7 vanto]:
The H.M algorithm is based on the reasoning of the Modus Ponens.\\
Yes: type inference is monotonic. That is, adding more definitions cannot make previously correct code become incorrect. (For example importing a compiled module and adding definitions in this module cannot invalidate the type inference in the imported module.) (That's not quite true in GHC with some of the 'advanced' extensions; and that's why type inference can become incoherent.)
The inference algorithm tells us which type has a value, but it does not tell us what type does not have the value.
(Not sure I understand but ...) that's impossible in general: there might be a later definition, perhaps in another module, that will provide a suitable type.
The utility of Modus tollens is complementary for many checks.
Please give some examples of the checks you're talking about. This is all very abstract so far.
I also propose that an inference algorithm based on Modus Tollens be coded in GHC.
Coded where? You mean in a Library/as an operator? Or I think you are talking about type inference in general? Then you would need a very strong reason to overturn Hindley-Milner. I suggest you ask some questions on the cafe; especially to discuss examples. And far-reaching proposals should be submitted through the github process, rather than Trac. There is already one proposal to use [https://github.com/AntC2/ghc- proposals/blob/instance-apartness-guards/proposals/0000-instance- apartness-guards.rst 'negative information' in type inference] -- kinda. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13038#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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 AntC): Replying to [comment:7 vanto]: Let me see if I can work an example.
1) f is a function that maps arguments of type A to results of type B.\\
{{{ f :: A -> B is identical to v(P -> Q) = 1 }}}
2) e is an expression of type A\\
{{{ e :: A is identical to v(P) = 1 }}}
3) Then the application f e has type B\\
{{{ f e :: B is identical to v(Q) = 1 }}}
..., we must infer the inverse of the algorithm and must use the Modus Tollens.\\
OK let's take the function as `length` from the Prelude. {{{ length :: Foldable t => t a -> Int }}} And take the use: `if (length xs) then ...`. That is, the context tells us to expect result `Bool`, which is not `Int`. Does this help infer the type for `xs`?
{{{ 1) f e :: not B is identical to v(Q) = 0 }}}
{{{ 2) f :: A -> B is identical to v(P -> Q) = 1 }}}
{{{ 3) e :: not A is identical to v(P) = 0 }}}
Firstly if this worked, we'd get `xs :: `**not** `(Foldable t => t a)`. I'm not seeing how knowing this would help improve the type for `xs`. But more importantly this doesn't work. If `length`'s result is required to be `Bool` but declared as `Int`, we have a contradiction. We have both `v(P -> Q) = 1` from the declaration and `v(P -> Q) = 0` from the context. So GHC should not infer anything about the type for `xs`; it should report an error -- which is what it does.
The utility of Modus tollens is complementary for many checks.
No, I think it has no utility.
I also propose that an inference algorithm based on Modus Tollens be coded in GHC.
I propose we close this ticket: invalid. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13038#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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
#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 AntC): Replying to [comment:10 vanto]:
Replying to [[span(style=color: #FF0000, AntC )]]:\\ Here is an example.\\
Not needed: I understand how modus tollens works/how to use it. (And you can reasonably expect that anyone who replies to you would know.)
I point out that my idea is to insert the Modus Tollens inside the type inference algorithm ...
Then what is needed is an example of how type inference would work.
Modus Tollens is not specific to programming, it can be found in electronic circuits.(We can build AND,OR,NAND Gates ...)\\
In Boolean logic, we have a closed world: not(True) ==> False; not(False) ==> True. In type inference we don't have a closed world. Knowing that type `a0` is `not(a0 ~ Int)` or `not(Num a0)` doesn't help draw any conclusions about `a0`. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13038#comment:11 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC