[Haskell-cafe] Propositions in Haskell

[MigMit]

You can stop suspecting: in Haskell, equations ARE definitions.

On May 15, 2013, at 9:15 PM, Patrick Browne <patrick.browne at 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.mead at 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.browne at dit.ie <patrick.browne at 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 at haskell.org <Haskell-Cafe at 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 at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe