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