Finding Truth with Elm
Tags: elm, logic, learning, showdev
Published: 2018-07-21 00:20:05

---
title: Finding Truth with Elm
published: true
description: How to write a truth table generator for use with propositional logic
tags: elm, logic, learning, showdev
cover_image: https://thepracticaldev.s3.amazonaws.com/i/husrxa1yr2xk4iudyhnb.jpg
---

When working with [propositional logic](https://en.wikipedia.org/wiki/Propositional_calculus) one needs to create [truth tables](https://en.wikipedia.org/wiki/Truth_table) 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`&nbsp;—

**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`](http://package.elm-lang.org/packages/1hko/elm-truth-table/latest). 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&nbsp;—

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

```elm
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&nbsp;—

**P**|**Q**|**¬P**|**¬P ∨ Q**|**P ⇒ Q**
:-----:|:-----:|:-----:|:-----:|:-----:
&hellip;|&hellip;|&hellip;|&hellip;|&hellip;

> ***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`&nbsp;—

```elm
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&nbsp;—

```elm
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&nbsp;—

```elm
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`&nbsp;—

**P**|**Q**|**¬P**|**¬P ∨ Q**|**P ⇒ Q**
:-----:|:-----:|:-----:|:-----:|:-----:
T|T|&hellip;|&hellip;|&hellip;
T|F|&hellip;|&hellip;|&hellip;
F|T|&hellip;|&hellip;|&hellip;
F|F|&hellip;|&hellip;|&hellip;

> ***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&nbsp;—

**P**|**Q**|**R**|**(P ⇒ Q) ⇒ R**|**P ⇒ (Q ⇒ R)**|**(P ⇒ R) ∨ (Q ⇒ R)**
:-----:|:-----:|:-----:|:-----:|:-----:|:-----:
T|T|T|&hellip;|&hellip;|&hellip;
T|T|F|&hellip;|&hellip;|&hellip;
T|F|T|&hellip;|&hellip;|&hellip;
T|F|F|&hellip;|&hellip;|&hellip;
F|T|T|&hellip;|&hellip;|&hellip;
F|T|F|&hellip;|&hellip;|&hellip;
F|F|T|&hellip;|&hellip;|&hellip;
F|F|F|&hellip;|&hellip;|&hellip;

> ***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&nbsp;—

```elm
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&nbsp;—

```elm
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&nbsp;—

```elm
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&nbsp;—

```elm
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](https://en.wikipedia.org/wiki/Logical_equivalence). 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***
> ```elm
  truthTable
      [ And (Not (Var "P")) (Not (Var "Q"))
      , Not (Or (Var "P") (Var "Q"))
      ]
  ```
> * *[De Morgan's Law](https://en.wikipedia.org/wiki/De_Morgan%27s_laws): `¬(P ∨ Q)` is equivalent to `(¬P) ∧ (¬Q)`*
> * *ie, "<u>not</u> cloudy <u>or</u> raining" is equivalent to "<u>not</u> cloudy <u>and not</u> raining"*

---

### Truth Table Generator

Find truth for yourself with the full source code provided on [ellie-app](https://ellie-app.com/Qs4HCPzYfra1).

To write this post, I used this [online utility](https://jakebathman.github.io/Markdown-Table-Generator/) 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 🔥