Re: [Haskell-cafe] Propositions in Haskell
Hi, Patrick Browne wrote: In am trying to understand why some equations are ok and others not. I suspect that in Haskell equations are definitions rather than assertions. Yes. Haskell function definitions look like equations, but in many ways, they aren't. Here is an example for an equation that is not valid as a Haskell function definition: g x = 42 f (g x) = x-- not valid The problem is that we cannot use g at the left-hand side. Here is an example that doesn't mean what you might be hoping for: f x = f x f x = 42 Seen as an equation system, this should constrain f to be a function that always returns 42. But in Haskell, it defines f to be a non-terminating function. The reason is that only the first line counts, because it covers all possible argument values. The second line is ignored. The behavior changes if we swap the two lines: g x = 42 g x = g x Again, only the first line counts, so g is the function that always returns 42. Here is a more complicated example: h 27 = 42 h x = h x h 13 = 100 What function is h? Tillmann ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Propositions in Haskell
I do understand the difference between theorem provers and Haskell programs.Logic can be used to reason 'about' Haskell programs and logic can be used 'within' Haskell programs.I am trying to clarify the difference between 'about' and 'within'Is approach 1 concerned with |= (model based 'within'), whereas approach 2 is concerned with |- (proof based 'about')?Thanks,PatOn 15/05/13, Alberto G. Corona agocor...@gmail.com wrote:Not exactly what you ask, but it is noteworthy that the mind has different logic processors. The fastest one work with IF THEN ELSE rules applied specifically to deals. This is why your example (and most examples of logic) involves a kind of deal expressed in the first person. This trigger a fast mental evaluation, while an equivalent but more general case is harder to process and need some paper work. (That special treatment of first person deals logic respond to the need to detect breaks of deals as fast as possible) http://en.wikipedia.org/wiki/Wason_selection_taskThat's why higher level languages have redundant logical structures and do not follow a general abstract and short mathematical notation. Therefore higher level, in programming languages, does not mean higher mathematical abstraction, but to be closer to the way the mind works. 2013/5/15 Patrick Browne patrick.bro...@dit.ie patrick.bro...@dit.ie -- Hi-- I am trying to show that a set of propositions and a conclusion the form a valid argument.-- I used two approaches; 1) using if-then-else, 2) using pattern matching. -- The version using if-then-else seems to be consistent with my knowledge of Haskell and logic (either of which could be wrong).-- Can the second approach be improved to better reflect the propositions and conclusion? Maybe type level reasoning could be used? -- -- Valid argument?-- 1. I work hard or I play piano-- 2. If I work hard then I will get a bonus-- 3. But I did not get a bonus-- Therefore I played piano-- Variables: p = Piano, w = worked hard, b = got a bonus -- (w \/ p) /\ (w = b) /\ ¬(b)-- --- -- p -- First approach using language control structure if-then-elsew, p, b::Bool-- Two equivalences for (w \/ p) as an implication. -- 1. (w \/ p) =equivalent-to= (not p) = w-- 2. (w \/ p) =equivalent-to= (not w) = p-- Picked 2p = if (not w) then True else False -- Contrapositive: (w = b) =equivalent-to= ~b = ~w w = if (not b) then False else Trueb = False -- gives p is true and w is false-- Second approach using pattern matching -- I think the rewriting goes from left to right but the logical inference goes in the opposite direction. w1, p1, b1::Boolp1 = (not w1) w1 = b1 -- Not consistent with statements, but I do not know how to write ~b1 = ~w1 in Haskellb1 = False-- Again gives p1 is true and w1 is false Tá an teachtaireacht seo scanta ó thaobh ábhar agus víreas ag Seirbhís Scanta Ríomhphost de chuid Seirbhísí Faisnéise, ITBÁC agus meastar í a bheith slán. http://www.dit.ie This message has been scanned for content and viruses by the DIT Information Services E-Mail Scanning Service, and is believed to be clean. http://www.dit.ie ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe -- Alberto. Tá an teachtaireacht seo scanta ó thaobh ábhar agus víreas ag Seirbhís Scanta Ríomhphost de chuid Seirbhísí Faisnéise, ITBÁC agus meastar í a bheith slán. http://www.dit.ie This message has been scanned for content and viruses by the DIT Information Services E-Mail Scanning Service, and is believed to be clean. http://www.dit.ie ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Propositions in Haskell
maybe this will help? Haskell code in and of itself isn't special. proofs can happen with the type system, but typically you'd want to define a target language and do assertions about it, similar to how a compiler inspects it's input programs. Haskell is not homoiconic nor is it like coq or prolog. But it is really really good at defining an ast and doing operations on it. On Thu, May 16, 2013 at 5:27 AM, Patrick Browne patrick.bro...@dit.iewrote: I do understand the difference between theorem provers and Haskell programs. Logic can be used to reason 'about' Haskell programs and logic can be used 'within' Haskell programs. I am trying to clarify the difference between 'about' and 'within' Is approach 1 concerned with |= (model based 'within'), whereas approach 2 is concerned with |- (proof based 'about')? Thanks, Pat On 15/05/13, *Alberto G. Corona * agocor...@gmail.com wrote: Not exactly what you ask, but it is noteworthy that the mind has different logic processors. The fastest one work with IF THEN ELSE rules applied specifically to deals. This is why your example (and most examples of logic) involves a kind of deal expressed in the first person. This trigger a fast mental evaluation, while an equivalent but more general case is harder to process and need some paper work. (That special treatment of first person deals logic respond to the need to detect breaks of deals as fast as possible) http://en.wikipedia.org/wiki/Wason_selection_task That's why higher level languages have redundant logical structures and do not follow a general abstract and short mathematical notation. Therefore higher level, in programming languages, does not mean higher mathematical abstraction, but to be closer to the way the mind works. 2013/5/15 Patrick Browne patrick.bro...@dit.ie patrick.bro...@dit.ie -- Hi -- I am trying to show that a set of propositions and a conclusion the form a valid argument. -- I used two approaches; 1) using if-then-else, 2) using pattern matching. -- The version using if-then-else seems to be consistent with my knowledge of Haskell and logic (either of which could be wrong). -- Can the second approach be improved to better reflect the propositions and conclusion? Maybe type level reasoning could be used? -- -- Valid argument? -- 1. I work hard or I play piano -- 2. If I work hard then I will get a bonus -- 3. But I did not get a bonus -- Therefore I played piano -- Variables: p = Piano, w = worked hard, b = got a bonus --(w \/ p) /\ (w = b) /\ ¬(b) -- --- --p -- First approach using language control structure if-then-else w, p, b::Bool -- Two equivalences for (w \/ p) as an implication. -- 1. (w \/ p) =equivalent-to= (not p) = w -- 2. (w \/ p) =equivalent-to= (not w) = p -- Picked 2 p = if (not w) then True else False -- Contrapositive: (w = b) =equivalent-to= ~b = ~w w = if (not b) then False else True b = False -- gives p is true and w is false -- Second approach using pattern matching -- I think the rewriting goes from left to right but the logical inference goes in the opposite direction. w1, p1, b1::Bool p1 = (not w1) w1 = b1 -- Not consistent with statements, but I do not know how to write ~b1 = ~w1 in Haskell b1 = False -- Again gives p1 is true and w1 is false Tá an teachtaireacht seo scanta ó thaobh ábhar agus víreas ag Seirbhís Scanta Ríomhphost de chuid Seirbhísí Faisnéise, ITBÁC agus meastar í a bheith slán. http://www.dit.ie This message has been scanned for content and viruses by the DIT Information Services E-Mail Scanning Service, and is believed to be clean. http://www.dit.ie ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe -- Alberto. Tá an teachtaireacht seo scanta ó thaobh ábhar agus víreas ag Seirbhís Scanta Ríomhphost de chuid Seirbhísí Faisnéise, ITBÁC agus meastar í a bheith slán. http://www.dit.ie This message has been scanned for content and viruses by the DIT Information Services E-Mail Scanning Service, and is believed to be clean. http://www.dit.ie ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Propositions in Haskell
-- Hi-- I am trying to show that a set of propositions and a conclusion the form a valid argument.-- I used two approaches; 1) using if-then-else, 2) using pattern matching.-- The version using if-then-else seems to be consistent with my knowledge of Haskell and logic (either of which could be wrong).-- Can the second approach be improved to better reflect the propositions and conclusion? Maybe type level reasoning could be used?-- -- Valid argument?-- 1. I work hard or I play piano-- 2. If I work hard then I will get a bonus-- 3. But I did not get a bonus-- Therefore I played piano-- Variables: p = Piano, w = worked hard, b = got a bonus-- (w \/ p) /\ (w = b) /\ ¬(b)-- --- -- p -- First approach using language control structure if-then-elsew, p, b::Bool-- Two equivalences for (w \/ p) as an implication.-- 1. (w \/ p) =equivalent-to= (not p) = w-- 2. (w \/ p) =equivalent-to= (not w) = p-- Picked 2p = if (not w) then True else False -- Contrapositive: (w = b) =equivalent-to= ~b = ~ww = if (not b) then False else Trueb = False -- gives p is true and w is false-- Second approach using pattern matching -- I think the rewriting goes from left to right but the logical inference goes in the opposite direction.w1, p1, b1::Boolp1 = (not w1) w1 = b1 -- Not consistent with statements, but I do not know how to write ~b1 = ~w1 in Haskellb1 = False-- Again gives p1 is true and w1 is false Tá an teachtaireacht seo scanta ó thaobh ábhar agus víreas ag Seirbhís Scanta Ríomhphost de chuid Seirbhísí Faisnéise, ITBÁC agus meastar í a bheith slán. http://www.dit.ie This message has been scanned for content and viruses by the DIT Information Services E-Mail Scanning Service, and is believed to be clean. http://www.dit.ie ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Propositions in Haskell
i don't understand what you're trying to do with that code, however you seem to be asking about theorem proving in general check out http://www.haskell.org/haskellwiki/Libraries_and_tools/Theorem_provers and http://en.wikipedia.org/wiki/Automated_theorem_proving hope it helps On Wed, May 15, 2013 at 11:34 AM, Patrick Browne patrick.bro...@dit.iewrote: -- Hi -- I am trying to show that a set of propositions and a conclusion the form a valid argument. -- I used two approaches; 1) using if-then-else, 2) using pattern matching. -- The version using if-then-else seems to be consistent with my knowledge of Haskell and logic (either of which could be wrong). -- Can the second approach be improved to better reflect the propositions and conclusion? Maybe type level reasoning could be used? -- -- Valid argument? -- 1. I work hard or I play piano -- 2. If I work hard then I will get a bonus -- 3. But I did not get a bonus -- Therefore I played piano -- Variables: p = Piano, w = worked hard, b = got a bonus --(w \/ p) /\ (w = b) /\ ¬(b) -- --- --p -- First approach using language control structure if-then-else w, p, b::Bool -- Two equivalences for (w \/ p) as an implication. -- 1. (w \/ p) =equivalent-to= (not p) = w -- 2. (w \/ p) =equivalent-to= (not w) = p -- Picked 2 p = if (not w) then True else False -- Contrapositive: (w = b) =equivalent-to= ~b = ~w w = if (not b) then False else True b = False -- gives p is true and w is false -- Second approach using pattern matching -- I think the rewriting goes from left to right but the logical inference goes in the opposite direction. w1, p1, b1::Bool p1 = (not w1) w1 = b1 -- Not consistent with statements, but I do not know how to write ~b1 = ~w1 in Haskell b1 = False -- Again gives p1 is true and w1 is false Tá an teachtaireacht seo scanta ó thaobh ábhar agus víreas ag Seirbhís Scanta Ríomhphost de chuid Seirbhísí Faisnéise, ITBÁC agus meastar í a bheith slán. http://www.dit.ie This message has been scanned for content and viruses by the DIT Information Services E-Mail Scanning Service, and is believed to be clean. http://www.dit.ie ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Propositions in Haskell
Not exactly what you ask, but it is noteworthy that the mind has different logic processors. The fastest one work with IF THEN ELSE rules applied specifically to deals. This is why your example (and most examples of logic) involves a kind of deal expressed in the first person. This trigger a fast mental evaluation, while an equivalent but more general case is harder to process and need some paper work. (That special treatment of first person deals logic respond to the need to detect breaks of deals as fast as possible) http://en.wikipedia.org/wiki/Wason_selection_task That's why higher level languages have redundant logical structures and do not follow a general abstract and short mathematical notation. Therefore higher level, in programming languages, does not mean higher mathematical abstraction, but to be closer to the way the mind works. 2013/5/15 Patrick Browne patrick.bro...@dit.ie -- Hi -- I am trying to show that a set of propositions and a conclusion the form a valid argument. -- I used two approaches; 1) using if-then-else, 2) using pattern matching. -- The version using if-then-else seems to be consistent with my knowledge of Haskell and logic (either of which could be wrong). -- Can the second approach be improved to better reflect the propositions and conclusion? Maybe type level reasoning could be used? -- -- Valid argument? -- 1. I work hard or I play piano -- 2. If I work hard then I will get a bonus -- 3. But I did not get a bonus -- Therefore I played piano -- Variables: p = Piano, w = worked hard, b = got a bonus --(w \/ p) /\ (w = b) /\ ¬(b) -- --- --p -- First approach using language control structure if-then-else w, p, b::Bool -- Two equivalences for (w \/ p) as an implication. -- 1. (w \/ p) =equivalent-to= (not p) = w -- 2. (w \/ p) =equivalent-to= (not w) = p -- Picked 2 p = if (not w) then True else False -- Contrapositive: (w = b) =equivalent-to= ~b = ~w w = if (not b) then False else True b = False -- gives p is true and w is false -- Second approach using pattern matching -- I think the rewriting goes from left to right but the logical inference goes in the opposite direction. w1, p1, b1::Bool p1 = (not w1) w1 = b1 -- Not consistent with statements, but I do not know how to write ~b1 = ~w1 in Haskell b1 = False -- Again gives p1 is true and w1 is false Tá an teachtaireacht seo scanta ó thaobh ábhar agus víreas ag Seirbhís Scanta Ríomhphost de chuid Seirbhísí Faisnéise, ITBÁC agus meastar í a bheith slán. http://www.dit.ie This message has been scanned for content and viruses by the DIT Information Services E-Mail Scanning Service, and is believed to be clean. http://www.dit.ie ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe -- Alberto. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Propositions in Haskell
The relation to theorem proving is the main motivation for my question. In am trying to understand why some equations are ok and others not. I suspect that in Haskell equations are definitions rather than assertions. If approach 2 is a non-starter in Haskell, then can approach 1, using if-then-else, achieve the same results for propositions? ThanksPatOn 15/05/13, Dan Mead d.w.m...@gmail.com wrote:i don't understand what you're trying to do with that code, however you seem to be asking about theorem proving in generalcheck outhttp://www.haskell.org/haskellwiki/Libraries_and_tools/Theorem_provers and http://en.wikipedia.org/wiki/Automated_theorem_provinghope it helps On Wed, May 15, 2013 at 11:34 AM, Patrick Browne patrick.bro...@dit.ie patrick.bro...@dit.ie wrote: -- Hi-- I am trying to show that a set of propositions and a conclusion the form a valid argument.-- I used two approaches; 1) using if-then-else, 2) using pattern matching. -- The version using if-then-else seems to be consistent with my knowledge of Haskell and logic (either of which could be wrong).-- Can the second approach be improved to better reflect the propositions and conclusion? Maybe type level reasoning could be used? -- -- Valid argument?-- 1. I work hard or I play piano-- 2. If I work hard then I will get a bonus-- 3. But I did not get a bonus-- Therefore I played piano-- Variables: p = Piano, w = worked hard, b = got a bonus -- (w \/ p) /\ (w = b) /\ ¬(b)-- --- -- p -- First approach using language control structure if-then-elsew, p, b::Bool-- Two equivalences for (w \/ p) as an implication. -- 1. (w \/ p) =equivalent-to= (not p) = w-- 2. (w \/ p) =equivalent-to= (not w) = p-- Picked 2p = if (not w) then True else False -- Contrapositive: (w = b) =equivalent-to= ~b = ~w w = if (not b) then False else Trueb = False -- gives p is true and w is false-- Second approach using pattern matching -- I think the rewriting goes from left to right but the logical inference goes in the opposite direction. w1, p1, b1::Boolp1 = (not w1) w1 = b1 -- Not consistent with statements, but I do not know how to write ~b1 = ~w1 in Haskellb1 = False-- Again gives p1 is true and w1 is false Tá an teachtaireacht seo scanta ó thaobh ábhar agus víreas ag Seirbhís Scanta Ríomhphost de chuid Seirbhísí Faisnéise, ITBÁC agus meastar í a bheith slán. http://www.dit.ie This message has been scanned for content and viruses by the DIT Information Services E-Mail Scanning Service, and is believed to be clean. http://www.dit.ie ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe Tá an teachtaireacht seo scanta ó thaobh ábhar agus víreas ag Seirbhís Scanta Ríomhphost de chuid Seirbhísí Faisnéise, ITBÁC agus meastar í a bheith slán. http://www.dit.ie This message has been scanned for content and viruses by the DIT Information Services E-Mail Scanning Service, and is believed to be clean. http://www.dit.ie ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Propositions in Haskell
You can stop suspecting: in Haskell, equations ARE definitions. On May 15, 2013, at 9:15 PM, Patrick Browne patrick.bro...@dit.ie wrote: The relation to theorem proving is the main motivation for my question. In am trying to understand why some equations are ok and others not. I suspect that in Haskell equations are definitions rather than assertions. If approach 2 is a non-starter in Haskell, then can approach 1, using if-then-else, achieve the same results for propositions? Thanks Pat On 15/05/13, Dan Mead d.w.m...@gmail.com wrote: i don't understand what you're trying to do with that code, however you seem to be asking about theorem proving in general check out http://www.haskell.org/haskellwiki/Libraries_and_tools/Theorem_provers and http://en.wikipedia.org/wiki/Automated_theorem_proving hope it helps On Wed, May 15, 2013 at 11:34 AM, Patrick Browne patrick.bro...@dit.ie patrick.bro...@dit.ie wrote: -- Hi -- I am trying to show that a set of propositions and a conclusion the form a valid argument. -- I used two approaches; 1) using if-then-else, 2) using pattern matching. -- The version using if-then-else seems to be consistent with my knowledge of Haskell and logic (either of which could be wrong). -- Can the second approach be improved to better reflect the propositions and conclusion? Maybe type level reasoning could be used? -- -- Valid argument? -- 1. I work hard or I play piano -- 2. If I work hard then I will get a bonus -- 3. But I did not get a bonus -- Therefore I played piano -- Variables: p = Piano, w = worked hard, b = got a bonus --(w \/ p) /\ (w = b) /\ ¬(b) -- --- --p -- First approach using language control structure if-then-else w, p, b::Bool -- Two equivalences for (w \/ p) as an implication. -- 1. (w \/ p) =equivalent-to= (not p) = w -- 2. (w \/ p) =equivalent-to= (not w) = p -- Picked 2 p = if (not w) then True else False -- Contrapositive: (w = b) =equivalent-to= ~b = ~w w = if (not b) then False else True b = False -- gives p is true and w is false -- Second approach using pattern matching -- I think the rewriting goes from left to right but the logical inference goes in the opposite direction. w1, p1, b1::Bool p1 = (not w1) w1 = b1 -- Not consistent with statements, but I do not know how to write ~b1 = ~w1 in Haskell b1 = False -- Again gives p1 is true and w1 is false Tá an teachtaireacht seo scanta ó thaobh ábhar agus víreas ag Seirbhís Scanta Ríomhphost de chuid Seirbhísí Faisnéise, ITBÁC agus meastar í a bheith slán. http://www.dit.ie This message has been scanned for content and viruses by the DIT Information Services E-Mail Scanning Service, and is believed to be clean. http://www.dit.ie ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe Tá an teachtaireacht seo scanta ó thaobh ábhar agus víreas ag Seirbhís Scanta Ríomhphost de chuid Seirbhísí Faisnéise, ITBÁC agus meastar í a bheith slán. http://www.dit.ie This message has been scanned for content and viruses by the DIT Information Services E-Mail Scanning Service, and is believed to be clean. http://www.dit.ie ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Propositions in Haskell
Patrick Browne patrick.bro...@dit.ie writes: -- Hi By the way, this is unrelated to your actual question, but if you haven't already, you might want to check out Bird-style Literate Haskell so you don't have to put -- in front of all of your non-Haskell text in a comment-heavy code-light file (or email message) :) http://www.haskell.org/haskellwiki/Literate_programming#Bird_Style -Keshav ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
