# Finding Truth with Elm

When working with propositional logic one needs to create truth tables such as the one below —

P Q ¬P ¬P ∨ Q P ⇒ Q
T T F T T
T F F F F
F T T T T
F F T T T

Table 1

• `P ⇒ Q` is logically equivalent to `¬P ∨ Q`

It’s important to do the exercise, but it’s also easy to make mistakes. If we had a program generate the truth table for us, we could be more certain of the results. And it enables laziness so of course we want to do this.

### Goal

The program should be intuitive and simply take a list of propositional expressions. Analysis of the expressions will determine which `True`/`False` permutations to construct. For example, the following set of expressions contains 3 unique variables `P`, `Q` and `R` —

P Q R (P ⇒ Q) ⇒ R P ⇒ (Q ⇒ R) (P ⇒ R) ∨ (Q ⇒ R)
T T T T T T
T T F F F F
T F T T T T
T F F T T T
F T T T T T
F T F F T T
F F T T T T
F F F F T T

Table 2

• `⇒` is not commutative
• `(P ⇒ Q) ⇒ R` is not equivalent to `P ⇒ (Q ⇒ R)`
• `P ⇒ (Q ⇒ R)` is logically equivalent to `(P ⇒ R) ∨ (Q ⇒ R)`

### Possible API

I wasn’t looking for anything fancy. Propositions should be easy to specify allowing the user to specify any amount of variables in a set of expressions —

``````type Expr =
-- ...

truthTable : List Expr -> Html msg
truthTable exprs =
-- ...

-- table 1
truthTable
[ Not (Var "P")                  -- ¬P
, Or (Not (Var "P")) (Var "Q")   -- ¬P ∨ Q
, Implies (Var "P")  (Var "Q")   -- P ⇒ Q
]

-- table 2
truthTable
-- (P => Q) => R
[ Implies (Implies (Var "P")  (Var "Q")) (Var "R")

-- P => (Q => R)
, Implies (Var "P") (Implies (Var "Q")  (Var "R"))

-- (P ⇒ R) ∨ (Q ⇒ R)
, Or (Implies (Var "P") (Var "R")) (Implies (Var "Q") (Var "R"))
]
``````

Later we can make a `String -> Expr` function later that parses `"Q => P" : String` to `Implies (Var "Q") (Var "P") : Expr`. But for now, this is all we need to get started.

### Implementation

A single union type `Expr` is sufficient for our program’s needs. I’ll show the complete type here but know that I completely implemented one variant before moving onto the next

``````type Expr
= Or Expr Expr
| And Expr Expr
| Xor Expr Expr
| Implies Expr Expr
| Equiv Expr Expr
| Not Expr
| Var String
``````

Every table starts with a `<thead>`. Our program needs to analyze and create column headers based on the input expressions. In Table 1 we saw —

P Q ¬P ¬P ∨ Q P ⇒ Q

Table 1

• One column header for each variable appearing in the set of expressions; `P` and `Q`
• One column for each expression – `¬P`, `¬P ∨ Q`, `P ⇒ Q`

To compute the columns for each variable, we create `vars` —

``````vars : Expr -> Set String
vars expr =
case expr of
Or a b ->
Set.union (vars a) (vars b)

Xor a b ->
Set.union (vars a) (vars b)

And a b ->
Set.union (vars a) (vars b)

Implies a b ->
Set.union (vars a) (vars b)

Equiv a b ->
Set.union (vars a) (vars b)

Not a ->
vars a

Var a ->
Set.singleton a

And (Var "P") (Var "Q") |> vars
-- [ "P", "Q" ] : Set String
``````

We can convert each expression to a string to be used in the remaining column headers —

``````exprToString : Expr -> String
exprToString expr =
case expr of
And a b ->
exprToString a ++ " ∧  " ++ exprToString b

Or a b ->
exprToString a ++ " ∨ " ++ exprToString b

Xor a b ->
exprToString a ++ " ⊕ " ++ exprToString b

Implies a b ->
exprToString a ++ " ⇒ " ++ exprToString b

Equiv a b ->
exprToString a ++ " ⇔ " ++ exprToString b

Not a ->
"¬" ++ exprToString a

Var a ->
a

Implies (Var "P") (Var "Q") |> exprToString
-- "P ⇒ Q" : String
``````

We can start filling in some of the implementation for `truthTable` now —

``````truthTable : List Expr -> Html msg
truthTable exprs =
let
ids =
exprs
|> List.map vars
|> List.foldl Set.union Set.empty
|> Set.toList

columns =
ids ++ List.map exprToString exprs

-- ...
in
Html.table [ Attributes.style [ ( "width", "100%" ) ] ]
, -- ...
]

tableHeader : List String -> Html msg
labels
|> List.map (tableCell [ ( "font-weight", "bold" ) ])
|> Html.tr []

tableCell : List ( String, String ) -> String -> Html msg
tableCell style text =
Html.td [ Attributes.style style ] [ Html.text text ]
``````

#### Table Rows

Moving along, we get to `<tbody>`. In Table 1 we see that `True`/`False` values need to be generated for each possible scenario of `P` and `Q` —

P Q ¬P ¬P ∨ Q P ⇒ Q
T T
T F
F T
F F

Table 1
all possible `True`/`False` permutations for 2 variables, `P` and `Q`

When the set of expressions expanded to include a third variable, `R`, in Table 2, another column was added, and more `True`/`False` values permutations too —

P Q R (P ⇒ Q) ⇒ R P ⇒ (Q ⇒ R) (P ⇒ R) ∨ (Q ⇒ R)
T T T
T T F
T F T
T F F
F T T
F T F
F F T
F F F

Table 2
all possible `True`/`False` permutations for 3 variables, `P` and `Q` and `R`

We implement `permute` to generate the values needed fill in each row —

``````permute : Int -> List a -> List (List a)
permute n list =
let
loop acc n xs =
if n == 0 then
[ acc ]
else
list
|> List.concatMap (\x -> loop (acc ++ [ x ]) (n - 1) xs)
in
loop [] n list

permute 2 [ "A", "B" ]
-- [ [ "A", "A" ]
-- , [ "A", "B" ]
-- , [ "B", "A" ]
-- , [ "B", "B" ]
-- ] : List (List String)
``````

Given a list of variables and a list of values, we make it possible to evaluate an expression —

``````makeEnv : List String -> List Bool -> Env
makeEnv ids values =
values
|> List.map2 (,) ids
|> Dict.fromList

eval : Env -> Expr -> Result String Bool
eval env expr =
case expr of
And a b ->
Result.map2 (&&) (eval env a) (eval env b)

Or a b ->
Result.map2 (||) (eval env a) (eval env b)

Xor a b ->
Result.map2 xor (eval env a) (eval env b)

Implies a b ->
Result.map2 implies (eval env a) (eval env b)

Equiv a b ->
Result.map2 equiv (eval env a) (eval env b)

Not a ->
Result.map not (eval env a)

Var a ->
Dict.get a env
|> Result.fromMaybe ("unbound identifier: " ++ toString a)

And (Var "P") (Var "Q")
|> eval (makeEnv [ "P", "Q" ], [ True, False ])
-- Ok False : Result String Bool
``````

To finish `truthTable`, we first generate the `True`/`False` value permutations and then evaluate them for each expression —

``````truthTable : List Expr -> Html msg
truthTable exprs =
let
ids =
-- ...

columns =
-- ...

count =
List.length ids

rows =
permute count [ True, False ]
|> List.map (tableRows (makeEnv ids) exprs)
in
Html.table [ Attributes.style [ ( "width", "100%" ) ] ]
, Html.tbody [] rows
]
``````

Finally we write `tableRows` to glue all the pieces together —

``````tableRows : (List Bool -> Env) -> List Expr -> List Bool -> Html msg
tableRows makeEnv exprs values =
let
env =
makeEnv values

results =
exprs
|> List.map (eval env)
|> List.foldr (Result.map2 (::)) (Ok [])
|> Result.map ((++) values)
|> Result.withDefault []

viewCell truth =
if truth then
tableCell [ ( "color", "#19A974" ) ] "T"
else
tableCell [ ( "color", "#E7040F" ) ] "F"
in
results
|> List.map viewCell
|> Html.tr []
``````

### Practical Application

“If user is logged in, and token is not invalid, and user belongs to editors, and post is editable, and post is not locked then …” – Writing programs that are easy to read is difficult. Sometimes complex logical propositions can be replaced with a simplified equivalent expression. Truth tables help us identify these equivalences

P Q (¬P) ∧ (¬Q) ¬(P ∨ Q)
T T F F
T F F F
F T F F
F F T T

Table 3

``````truthTable
[ And (Not (Var "P")) (Not (Var "Q"))
, Not (Or (Var "P") (Var "Q"))
]
``````
• De Morgan’s Law: `¬(P ∨ Q)` is equivalent to `(¬P) ∧ (¬Q)`
• ie, “not cloudy or raining” is equivalent to “not cloudy and not raining”

### Live Truth Table Generator

Find truth for yourself with the full source code provided on ellie-app.

To write this post, I used this online utility to convert HTML tables to GHF Markdown.

Cross-posted on dev.to.

### Now available as a package

This program now exists in the Elm package repository, `1hko/elm-truth-table`. The code you see in this post is mostly the same with a few things renamed. Check out the github issues to see if you can help.

9 Likes

This is really cool! I was thinking about building a system for natural deduction. This will come in handy!

1 Like

I’m happy you found it useful. Thanks for reading.

This topic was automatically closed 10 days after the last reply. New replies are no longer allowed.