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)

---

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; 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%" ) ] ]
        [ 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 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.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

• exprToString should include parentheses () disambiguate expressions like P ⇒ Q ⇒ R
• Expr union type can probably be simplified to type Expr = Unary ... | Binary ...
• a String -> Expr parser
• Your ideas here 🔥