15 May 17:34 2013

## Propositions in Haskell

Patrick Browne <patrick.browne <at> dit.ie>

2013-05-15 15:34:28 GMT

2013-05-15 15:34:28 GMT

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

-- 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 http://www.haskell.org/mailman/listinfo/haskell-cafe