TypeScript: propositional formulas as a discriminated union

Before you start

TypeScript union types, switch, and recursion.

Represent formulas as trees, evaluate them for any assignment, and test for tautologies.
Predict the sample output and explain the state changes.
Complete the practice task and check the boundary cases.

The concept

A propositional formula is a tree: variables are the leaves and the connectives not, and, or, and implies are the inner nodes. A discriminated union gives each kind of node its own shape and a kind field. A switch on kind narrows the type in each branch, so the compiler knows which fields exist.

The default branch assigns the unreachable value to a variable of type never. If someone adds a new connective but forgets to handle it, the program stops compiling. That exhaustiveness check is a strong guard for a growing language of formulas. A tautology is a formula that is true under every assignment, and the program tests this by enumerating all of them.

Code example

TypeScript

type Expr =
  | { kind: "var"; name: string }
  | { kind: "not"; arg: Expr }
  | { kind: "and"; left: Expr; right: Expr }
  | { kind: "or"; left: Expr; right: Expr }
  | { kind: "implies"; left: Expr; right: Expr };

const v = (name: string): Expr => ({ kind: "var", name });
const implies = (left: Expr, right: Expr): Expr => ({ kind: "implies", left, right });
const and = (left: Expr, right: Expr): Expr => ({ kind: "and", left, right });

function evaluate(e: Expr, env: Record<string, boolean>): boolean {
  switch (e.kind) {
    case "var":
      return env[e.name];
    case "not":
      return !evaluate(e.arg, env);
    case "and":
      return evaluate(e.left, env) && evaluate(e.right, env);
    case "or":
      return evaluate(e.left, env) || evaluate(e.right, env);
    case "implies":
      return !evaluate(e.left, env) || evaluate(e.right, env);
    default: {
      const unreachable: never = e;
      return unreachable;
    }
  }
}

const P = v("P");
const Q = v("Q");
const rule = implies(P, Q);
for (const p of [false, true]) {
  for (const q of [false, true]) {
    console.log("P=" + p + " Q=" + q + ": " + evaluate(rule, { P: p, Q: q }));
  }
}

const modusPonens = implies(and(P, rule), Q);
let tautology = true;
for (const p of [false, true]) {
  for (const q of [false, true]) {
    tautology = tautology && evaluate(modusPonens, { P: p, Q: q });
  }
}
console.log("modus ponens is a tautology: " + tautology);

Output

P=false Q=false: true
P=false Q=true: true
P=true Q=false: false
P=true Q=true: true
modus ponens is a tautology: true

Example details

Follow the code

Open the walkthrough to inspect the example one step at a time.

Show guided walkthrough

Guided walkthroughReady

1type Expr =

2 | { kind: "var"; name: string }

3 | { kind: "not"; arg: Expr }

4 | { kind: "and"; left: Expr; right: Expr }

5 | { kind: "or"; left: Expr; right: Expr }

6 | { kind: "implies"; left: Expr; right: Expr };

8const v = (name: string): Expr => ({ kind: "var", name });

9const implies = (left: Expr, right: Expr): Expr => ({ kind: "implies", left, right });

10const and = (left: Expr, right: Expr): Expr => ({ kind: "and", left, right });

12function evaluate(e: Expr, env: Record<string, boolean>): boolean {

13 switch (e.kind) {

14 case "var":

15 return env[e.name];

16 case "not":

17 return !evaluate(e.arg, env);

18 case "and":

19 return evaluate(e.left, env) && evaluate(e.right, env);

20 case "or":

21 return evaluate(e.left, env) || evaluate(e.right, env);

22 case "implies":

23 return !evaluate(e.left, env) || evaluate(e.right, env);

24 default: {

25 const unreachable: never = e;

26 return unreachable;

27 }

28 }

29}

31const P = v("P");

32const Q = v("Q");

33const rule = implies(P, Q);

34for (const p of [false, true]) {

35 for (const q of [false, true]) {

36 console.log("P=" + p + " Q=" + q + ": " + evaluate(rule, { P: p, Q: q }));

37 }

38}

40const modusPonens = implies(and(P, rule), Q);

41let tautology = true;

42for (const p of [false, true]) {

43 for (const q of [false, true]) {

44 tautology = tautology && evaluate(modusPonens, { P: p, Q: q });

45 }

46}

47console.log("modus ponens is a tautology: " + tautology);

Follow the example

Start to inspect the source, values, and output. These prepared steps explain the published sample; grouped loop steps describe multiple iterations.

View the complete dry-run table

Prepared trace of the published program. Some rows group repeated iterations.
What happens	State after step	Output so far
Each kind of formula node has its own fields.	`—`	—
P implies Q is the same as not-P or Q.	`—`	—
If a new kind is added and not handled above, e is not never and this line fails to compile.	`—`	—
The truth table of P → Q: it is false only when P is true and Q is false.	`—`	P=false Q=false: true P=false Q=true: true P=true Q=false: false P=true Q=true: true
(P ∧ (P → Q)) → Q is true for all four assignments.	`—`	P=false Q=false: true P=false Q=true: true P=true Q=false: false P=true Q=true: true modus ponens is a tautology: true

Behind the scenes

How TypeScript processes this code

TypeScript checks types and emits JavaScript. Type annotations are removed before execution.

Cost and common mistakes

O(size of the formula) per evaluation; O(2ⁿ) assignments for n variables.

Without the never check, a missing case silently returns undefined at run time.
env[e.name] is undefined for an unassigned variable. A real evaluator should report that error.
Enumerating all assignments is exponential in the number of variables, so it works only for small formulas.

Try it yourself

Is P ∨ ¬P a tautology?

Reveal answer and reasoning

Yes. For P = true the first part is true and for P = false the negation is true, so it holds under both assignments.