TypeScript: propositional formulas as a discriminated union
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.
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);