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 ⇒ Qis 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) ⇒ Ris not equivalent toP ⇒ (Q ⇒ R)P ⇒ (Q ⇒ R)is logically equivalent to(P ⇒ R) ∨ (Q ⇒ R)
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.
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
Table Header
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;
PandQ- 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%" ) ] ]
[ Html.thead [] [ tableHeader columns ]
, -- ...
]
tableHeader : List String -> Html msg
tableHeader labels =
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 possibleTrue/Falsepermutations for 2 variables,PandQ
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 possibleTrue/Falsepermutations for 3 variables,PandQandR
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.thead [] [ tableHeader columns ]
, 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"
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
To-do
I will continue to make improvements on this as time permits
-
exprToStringshould include parentheses()disambiguate expressions likeP ⇒ Q ⇒ R -
Exprunion type can probably be simplified totype Expr = Unary ... | Binary ... - a
String -> Exprparser - Your ideas here 🔥
Top comments (0)