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 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 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 > 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 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