TypeScript: propositional formulas as a discriminated union

Represent formulas as trees, evaluate them for any assignment, and test for tautologies.

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

Explanation

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.

Explore the dry run

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

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.

TypeScript: propositional formulas as a discriminated union

Explanation

Follow the example

Cost and common mistakes

Try it yourself

Further reading