Refactor (2)

packages/kripke/src/index.ts

@@ -0,0 +1,4 @@
+export * from "./syntax";
+export * from "./semantics";
+export * from "./parser";
+export * from "./sat";

packages/kripke/src/parser.ts

@@ -0,0 +1,192 @@
+import type {} from "@cannorin/utils/headless";
+import {
+  type Token,
+  alt,
+  apply,
+  buildLexer,
+  expectEOF,
+  expectSingleResult,
+  kmid,
+  lrec_sc,
+  rule,
+  seq,
+  tok,
+} from "typescript-parsec";
+import {
+  type Formula,
+  and,
+  bot,
+  box,
+  diamond,
+  eq,
+  not,
+  or,
+  propVars,
+  propvar,
+  to,
+  top,
+} from "./syntax";
+
+enum TokenKind {
+  PropVar = 0,
+  Top = 1,
+  Bot = 2,
+  Not = 3,
+  Box = 4,
+  Diamond = 5,
+  And = 6,
+  Or = 7,
+  To = 8,
+  Eq = 9,
+  LParen = 10,
+  RParen = 11,
+  Space = 12,
+}
+
+const escapeRegExp = (s: string) => s.replace(/[.*+?^${}()|[\]\\]/g, "\\$&");
+
+const generateAlt = (words: string[]) =>
+  new RegExp(`^(${words.map((s) => escapeRegExp(s)).join("|")})`, "g");
+
+export const topSymbols = ["⊤", "T", "1", "\\top", "top"];
+export const botSymbols = ["⊥", "F", "0", "\\bot", "bot"];
+export const notSymbols = ["¬", "~", "\\neg", "\\lnot", "not"];
+export const boxSymbols = ["□", "◻", "[]", "!", "L", "\\Box", "box"];
+export const diamondSymbols = [
+  "◇",
+  "◊",
+  "♢",
+  "⋄",
+  "<>",
+  "?",
+  "M",
+  "\\Diamond",
+  "dia",
+];
+export const andSymbols = ["∧", "^", "&", "\\wedge", "\\land", "and"];
+export const orSymbols = ["∨", "v", "|", "\\vee", "\\lor", "or"];
+export const toSymbols = ["→", "->", "⊃", ">", "\\rightarrow", "\\to", "to"];
+export const eqSymbols = [
+  "↔",
+  "<->",
+  "≡",
+  "=",
+  "\\leftrightarrow",
+  "\\equiv",
+  "eq",
+];
+export const lParenSymbols = ["(", "\\left"];
+export const rParenSymbols = [")", "\\right"];
+
+const lexer = buildLexer([
+  [true, generateAlt(propVars), TokenKind.PropVar],
+  [true, generateAlt(topSymbols), TokenKind.Top],
+  [true, generateAlt(botSymbols), TokenKind.Bot],
+  [true, generateAlt(notSymbols), TokenKind.Not],
+  [true, generateAlt(boxSymbols), TokenKind.Box],
+  [true, generateAlt(diamondSymbols), TokenKind.Diamond],
+  [true, generateAlt(andSymbols), TokenKind.And],
+  [true, generateAlt(orSymbols), TokenKind.Or],
+  [true, generateAlt(toSymbols), TokenKind.To],
+  [true, generateAlt(eqSymbols), TokenKind.Eq],
+  [true, generateAlt(lParenSymbols), TokenKind.LParen],
+  [true, generateAlt(rParenSymbols), TokenKind.RParen],
+  [false, /^\s+/g, TokenKind.Space],
+]);
+
+function atom(
+  value: Token<TokenKind.PropVar | TokenKind.Top | TokenKind.Bot>,
+): Formula {
+  switch (value.kind) {
+    case TokenKind.PropVar: {
+      if (propVars.includes(value.text)) {
+        return propvar(value.text);
+      }
+      throw new Error(`Unknown atom: ${value.text}`);
+    }
+    case TokenKind.Top:
+      return top;
+    case TokenKind.Bot:
+      return bot;
+    default:
+      throw new Error(`Unknown atom: ${value.text}`);
+  }
+}
+
+function unary([op, value]: [
+  Token<TokenKind.Not | TokenKind.Box | TokenKind.Diamond>,
+  Formula,
+]): Formula {
+  switch (op.kind) {
+    case TokenKind.Not:
+      return not(value);
+    case TokenKind.Box:
+      return box(value);
+    case TokenKind.Diamond:
+      return diamond(value);
+    default:
+      throw new Error(`Unknown unary operator: ${op.text}`);
+  }
+}
+
+function binary(
+  left: Formula,
+  [op, right]: [
+    Token<TokenKind.And | TokenKind.Or | TokenKind.To | TokenKind.Eq>,
+    Formula,
+  ],
+): Formula {
+  switch (op.kind) {
+    case TokenKind.And:
+      return and(left, right);
+    case TokenKind.Or:
+      return or(left, right);
+    case TokenKind.To:
+      return to(left, right);
+    case TokenKind.Eq:
+      return eq(left, right);
+    default:
+      throw new Error(`Unknown binary operator: ${op.text}`);
+  }
+}
+
+const TERM = rule<TokenKind, Formula>();
+const ANDOR = rule<TokenKind, Formula>();
+const EXP = rule<TokenKind, Formula>();
+
+TERM.setPattern(
+  alt(
+    apply(
+      alt(tok(TokenKind.PropVar), tok(TokenKind.Top), tok(TokenKind.Bot)),
+      atom,
+    ),
+    apply(
+      seq(
+        alt(tok(TokenKind.Not), tok(TokenKind.Box), tok(TokenKind.Diamond)),
+        TERM,
+      ),
+      unary,
+    ),
+    kmid(tok(TokenKind.LParen), EXP, tok(TokenKind.RParen)),
+  ),
+);
+
+ANDOR.setPattern(
+  lrec_sc(TERM, seq(alt(tok(TokenKind.And), tok(TokenKind.Or)), ANDOR), binary),
+);
+
+EXP.setPattern(
+  lrec_sc(ANDOR, seq(alt(tok(TokenKind.To), tok(TokenKind.Eq)), EXP), binary),
+);
+
+export function parse(expr: string): Formula {
+  return expectSingleResult(expectEOF(EXP.parse(lexer.parse(expr))));
+}
+
+export function tryParse(expr: string): Formula | undefined {
+  try {
+    return parse(expr);
+  } catch {
+    return undefined;
+  }
+}

packages/kripke/src/sat.ts

@@ -0,0 +1,282 @@
+import { BitSet, maximal } from "@cannorin/utils";
+import {
+  type Frame,
+  type Model,
+  type World,
+  left,
+  right,
+  worlds,
+} from "./semantics";
+import {
+  type Formula,
+  type NNFFormula,
+  not,
+  propVars,
+  simplify,
+  tagNNF,
+  toNNF,
+} from "./syntax";
+
+const allValuations = worlds.flatMap((w) =>
+  propVars.map((p) => `${w}${p}` as const),
+);
+
+const valuationSet = new BitSet(allValuations);
+
+export type Constraints = {
+  positive: number;
+  negative: number;
+};
+
+const empty: Constraints = {
+  positive: valuationSet.empty,
+  negative: valuationSet.empty,
+};
+
+export type Context = {
+  notFml: NNFFormula<number>;
+  next: Record<World, World[]>;
+  memo: Map<`${World}:${number}`, Constraints[]>;
+  constant: Map<`${World}:${number}`, boolean>;
+};
+
+export function buildContext(frame: Frame, fml: Formula): Context {
+  let index = 0;
+  const notFml = tagNNF(toNNF(simplify(not(fml))), () => {
+    index++;
+    return index;
+  });
+
+  const next: Record<World, World[]> = { a: [], b: [], c: [], d: [] };
+  for (const rel of frame.relations.values()) {
+    const u = left(rel);
+    const v = right(rel);
+    next[u].push(v);
+  }
+
+  const constant: Map<`${World}:${number}`, boolean> = new Map();
+  function addConstants(f: NNFFormula<number>) {
+    switch (f.type) {
+      case "top": {
+        for (const w of worlds) constant.set(`${w}:${f.tag}`, true);
+        return;
+      }
+      case "bot": {
+        for (const w of worlds) constant.set(`${w}:${f.tag}`, false);
+        return;
+      }
+      case "propvar":
+      case "not":
+        return;
+      case "box": {
+        addConstants(f.fml);
+        for (const w1 of worlds) {
+          const xs = next[w1].map((w2) => constant.get(`${w2}:${f.fml.tag}`));
+          if (xs.some((x) => x === undefined)) continue;
+          constant.set(
+            `${w1}:${f.tag}`,
+            xs.every((x) => x === true),
+          );
+        }
+        return;
+      }
+      case "diamond": {
+        addConstants(f.fml);
+        for (const w1 of worlds) {
+          const xs = next[w1].map((w2) => constant.get(`${w2}:${f.fml.tag}`));
+          if (xs.some((x) => x === undefined)) continue;
+          constant.set(
+            `${w1}:${f.tag}`,
+            xs.some((x) => x === true),
+          );
+        }
+        return;
+      }
+      case "or": {
+        addConstants(f.left);
+        addConstants(f.right);
+        for (const w of worlds) {
+          const l = constant.get(`${w}:${f.left.tag}`);
+          const r = constant.get(`${w}:${f.right.tag}`);
+          if (l === undefined || r === undefined) continue;
+          constant.set(`${w}:${f.tag}`, l || r);
+        }
+        return;
+      }
+      case "and": {
+        addConstants(f.left);
+        addConstants(f.right);
+        for (const w of worlds) {
+          const l = constant.get(`${w}:${f.left.tag}`);
+          const r = constant.get(`${w}:${f.right.tag}`);
+          if (l === undefined || r === undefined) continue;
+          constant.set(`${w}:${f.tag}`, l && r);
+        }
+        return;
+      }
+    }
+  }
+  addConstants(notFml);
+
+  return { notFml, next, memo: new Map(), constant };
+}
+
+const isWeaker = (c1: Constraints, c2: Constraints): boolean => {
+  return (
+    valuationSet.isSuperset(c1.positive, c2.positive) &&
+    valuationSet.isSuperset(c1.negative, c2.negative)
+  );
+};
+
+const union = (c1: Constraints, c2: Constraints): Constraints => {
+  return {
+    positive: valuationSet.union(c1.positive, c2.positive),
+    negative: valuationSet.union(c1.negative, c2.negative),
+  };
+};
+
+const consistent = (c: Constraints) => {
+  return valuationSet.isDisjoint(c.positive, c.negative);
+};
+
+function sat(
+  frame: Frame,
+  fml: NNFFormula<number>,
+  world: World,
+  ctx: Context = buildContext(frame, fml),
+): Constraints[] {
+  const key = `${world}:${fml.tag}` as const;
+  const c = ctx.constant.get(key);
+  if (c === true) return [empty];
+  if (c === false) return [];
+
+  let result = ctx.memo.get(key);
+  if (result) return result;
+
+  switch (fml.type) {
+    case "top":
+      result = [empty];
+      break;
+    case "bot":
+      result = [];
+      break;
+    case "propvar":
+      result = [
+        {
+          positive: valuationSet.create(`${world}${fml.name}`),
+          negative: valuationSet.empty,
+        },
+      ];
+      break;
+    case "not":
+      result = [
+        {
+          positive: valuationSet.empty,
+          negative: valuationSet.create(`${world}${fml.fml.name}`),
+        },
+      ];
+      break;
+    case "box": {
+      result = ctx.next[world]
+        .map((w) => sat(frame, fml.fml, w, ctx))
+        .reduce(
+          (prev, current) =>
+            maximal(
+              current.flatMap((c1) =>
+                prev.map((c2) => union(c1, c2)).filter(consistent),
+              ),
+              isWeaker,
+            ),
+          [empty],
+        );
+      break;
+    }
+    case "diamond": {
+      result = maximal(
+        ctx.next[world].flatMap((w) => sat(frame, fml.fml, w, ctx)),
+        isWeaker,
+      );
+      break;
+    }
+    case "and": {
+      result = [
+        sat(frame, fml.left, world, ctx),
+        sat(frame, fml.right, world, ctx),
+      ].reduce(
+        (prev, current) =>
+          maximal(
+            current.flatMap((c1) =>
+              prev.map((c2) => union(c1, c2)).filter(consistent),
+            ),
+            isWeaker,
+          ),
+        [empty],
+      );
+      break;
+    }
+    case "or": {
+      result = maximal(
+        [
+          sat(frame, fml.left, world, ctx),
+          sat(frame, fml.right, world, ctx),
+        ].flat(),
+        isWeaker,
+      );
+      break;
+    }
+  }
+
+  ctx.memo.set(key, result);
+  return result;
+}
+
+export function findCountermodelsAt(
+  frame: Frame,
+  fml: Formula,
+  world: World,
+  ctx = buildContext(frame, fml),
+): Model[] {
+  return sat(frame, ctx.notFml, world, ctx).map(({ positive }) => ({
+    ...frame,
+    valuations: valuationSet.decode(positive),
+  }));
+}
+
+export function findCountermodels(
+  frame: Frame,
+  fml: Formula,
+  ctx = buildContext(frame, fml),
+): Model[] {
+  return maximal(
+    worlds.flatMap((world) => sat(frame, ctx.notFml, world, ctx)),
+    isWeaker,
+  ).map(({ positive }) => ({
+    ...frame,
+    valuations: valuationSet.decode(positive),
+  }));
+}
+
+export function validInWorld(
+  frame: Frame,
+  fml: Formula,
+  world: World,
+  ctx = buildContext(frame, fml),
+) {
+  return sat(frame, ctx.notFml, world, ctx).length === 0;
+}
+
+export function validWorlds(
+  frame: Frame,
+  fml: Formula,
+  ctx = buildContext(frame, fml),
+) {
+  return worlds.filter((world) => validInWorld(frame, ctx.notFml, world, ctx));
+}
+
+export function validInFrame(
+  frame: Frame,
+  fml: Formula,
+  ctx = buildContext(frame, fml),
+) {
+  return worlds.every((world) => validInWorld(frame, ctx.notFml, world, ctx));
+}

packages/kripke/src/semantics.ts

@@ -0,0 +1,156 @@
+import { BitSet, permutate } from "@cannorin/utils";
+import type { Formula, PropVar } from "./syntax";
+
+export const worlds = ["a", "b", "c", "d"] as const;
+
+export type World = (typeof worlds)[number];
+
+export type Relation = `${World}${World}`;
+export const left = (rel: Relation) => rel[0] as World;
+export const right = (rel: Relation) => rel[1] as World;
+export const reverse = (rel: Relation) =>
+  `${right(rel)}${left(rel)}` as Relation;
+
+export const relation: Relation[] = worlds.flatMap((w) =>
+  worlds.map((x) => `${w}${x}` as const),
+);
+
+const relationSet = new BitSet(relation);
+
+export interface Frame {
+  relations: Set<Relation>;
+}
+
+export interface Model extends Frame {
+  valuations: Set<`${World}${PropVar}`>;
+}
+
+export function satisfy(m: Model, w: World, fml: Formula): boolean {
+  switch (fml.type) {
+    case "top":
+      return true;
+    case "bot":
+      return false;
+    case "propvar":
+      return m.valuations.has(`${w}${fml.name}`);
+    case "not":
+      return !satisfy(m, w, fml.fml);
+    case "box": {
+      for (const rel of m.relations.values()) {
+        if (left(rel) !== w) continue;
+        if (!satisfy(m, right(rel), fml.fml)) return false;
+      }
+      return true;
+    }
+    case "diamond": {
+      for (const rel of m.relations.values()) {
+        if (left(rel) !== w) continue;
+        if (satisfy(m, right(rel), fml.fml)) return true;
+      }
+      return false;
+    }
+    case "to": {
+      if (!satisfy(m, w, fml.left)) return true;
+      return satisfy(m, w, fml.right);
+    }
+    case "or": {
+      if (satisfy(m, w, fml.left)) return true;
+      return satisfy(m, w, fml.right);
+    }
+    case "and": {
+      if (!satisfy(m, w, fml.left)) return false;
+      return satisfy(m, w, fml.right);
+    }
+    case "eq": {
+      return satisfy(m, w, fml.left) === satisfy(m, w, fml.right);
+    }
+  }
+}
+
+export const validInModel = (m: Model, fml: Formula) =>
+  worlds.every((w) => satisfy(m, w, fml));
+
+export function getFrame(id: number): Frame {
+  return { relations: relationSet.decode(id) };
+}
+
+export function getId(frame: Frame) {
+  return relationSet.encode(frame.relations);
+}
+
+const worldPermutations = permutate(worlds).map(
+  (perm) => new Map(worlds.map((k, i) => [k, perm[i] as World])),
+);
+
+function applyPermutation<T extends Frame>(
+  frame: T,
+  permutation: Map<World, World>,
+) {
+  const relations = new Set<Relation>();
+  for (const rel of frame.relations) {
+    const l = left(rel);
+    const r = right(rel);
+    relations.add(
+      `${permutation.get(l) ?? l}${permutation.get(r) ?? r}` as Relation,
+    );
+  }
+  return { ...frame, relations } as T;
+}
+
+export function generateAllFrames() {
+  const canonicals: number[] = [];
+  const nontrivials: number[] = [];
+  const map = new Map<number, number>();
+
+  const total = 2 ** relation.length;
+  for (let id = 0; id < total; id++) {
+    if (map.has(id)) continue;
+
+    const relations = relationSet.decode(id);
+
+    const frame = { relations };
+    const equivalentIds: number[] = [];
+
+    let canonicalId = id;
+    for (const perm of worldPermutations) {
+      const permuted = applyPermutation(frame, perm);
+      const permutedId = relationSet.encode(permuted.relations);
+      equivalentIds.push(permutedId);
+      if (canonicalId === null || permutedId < canonicalId) {
+        canonicalId = permutedId;
+      }
+    }
+
+    canonicals.push(canonicalId);
+    for (const equivalentId of equivalentIds) {
+      map.set(equivalentId, canonicalId);
+    }
+
+    // Exclude the sizes with less than 10 frames (= can be bruteforced)
+    if (relations.size >= 3 && relations.size <= 13) {
+      nontrivials.push(canonicalId);
+    }
+  }
+
+  const isomorphic: Uint16Array = new Uint16Array(total);
+  for (let id = 0; id < total; id++) {
+    const value = map.get(id);
+    if (value === undefined) throw Error(`impossible (${id})`);
+    isomorphic[id] = value;
+  }
+
+  return { canonicals, isomorphic, nontrivials };
+}
+
+const allFrames = generateAllFrames();
+
+/** canonical frames among all the isomorphic ones */
+const canonicals = allFrames.canonicals;
+
+/** mapping to get the canonical frame */
+const isomorphic = allFrames.isomorphic;
+
+/** frames that are suitable for the puzzle */
+const nontrivials = allFrames.nontrivials;
+
+export { canonicals, isomorphic, nontrivials };

packages/kripke/src/syntax.ts

@@ -0,0 +1,374 @@
+export type PropVar = "p" | "q" | "r" | "s";
+
+export const propVars = ["p", "q", "r", "s"] as const satisfies PropVar[];
+
+export type Formula =
+  | { type: "top" | "bot" }
+  | { type: "propvar"; name: PropVar }
+  | { type: "not" | "box" | "diamond"; fml: Formula }
+  | {
+      type: "to" | "or" | "and" | "eq";
+      left: Formula;
+      right: Formula;
+    };
+
+export function vars(fml: Formula): Set<PropVar> {
+  switch (fml.type) {
+    case "top":
+    case "bot":
+      return new Set();
+    case "box":
+    case "diamond":
+    case "not":
+      return vars(fml.fml);
+    case "to":
+    case "or":
+    case "and":
+    case "eq":
+      return new Set([...vars(fml.left), ...vars(fml.right)]);
+    case "propvar":
+      return new Set([fml.name]);
+  }
+}
+
+export const propvar = (name: PropVar) => ({ type: "propvar", name }) as const;
+
+export const top = { type: "top" } as const satisfies Formula;
+export const bot = { type: "bot" } as const satisfies Formula;
+
+export const box = (fml: Formula) =>
+  ({ type: "box", fml }) as const satisfies Formula;
+export const diamond = (fml: Formula) =>
+  ({ type: "diamond", fml }) as const satisfies Formula;
+export const not = (fml: Formula) =>
+  ({ type: "not", fml }) as const satisfies Formula;
+
+export const to = (left: Formula, right: Formula) =>
+  ({ type: "to", left, right }) as const satisfies Formula;
+export const and = (left: Formula, right: Formula) =>
+  ({ type: "and", left, right }) as const satisfies Formula;
+export const or = (left: Formula, right: Formula) =>
+  ({ type: "or", left, right }) as const satisfies Formula;
+export const eq = (left: Formula, right: Formula) =>
+  ({ type: "eq", left, right }) as const satisfies Formula;
+
+export type Symbols = Record<Exclude<Formula["type"], "propvar">, string>;
+
+export const asciiSymbols: Symbols = {
+  top: "T",
+  bot: "F",
+  box: "[]",
+  diamond: "<>",
+  not: "~",
+  and: "^",
+  or: "v",
+  to: "->",
+  eq: "<->",
+};
+
+export const unicodeSymbols: Symbols = {
+  top: "⊤",
+  bot: "⊥",
+  box: "□",
+  diamond: "◇",
+  not: "¬",
+  and: "∧",
+  or: "∨",
+  to: "→",
+  eq: "↔",
+};
+
+export const latexSymbols: Symbols = {
+  top: "\\top ",
+  bot: "\\bot ",
+  box: "\\Box ",
+  diamond: "\\Diamond ",
+  not: "\\neg ",
+  and: "\\land",
+  or: "\\lor",
+  to: "\\to",
+  eq: "\\leftrightarrow",
+};
+
+export function prettyPrint(
+  fml: Formula,
+  config?: { paren?: boolean | ((fml: Formula) => boolean); symbols?: Symbols },
+): string {
+  const { paren = false, symbols = unicodeSymbols } = config ?? {};
+  const withParen = (s: string) =>
+    (typeof paren === "boolean" ? paren : paren(fml)) ? `(${s})` : s;
+
+  switch (fml.type) {
+    case "top":
+      return symbols.top;
+    case "bot":
+      return symbols.bot;
+    case "propvar":
+      return fml.name;
+    case "not":
+      return `${symbols.not}${prettyPrint(fml.fml, { paren: true, symbols })}`;
+    case "box":
+      return `${symbols.box}${prettyPrint(fml.fml, { paren: true, symbols })}`;
+    case "diamond":
+      return `${symbols.diamond}${prettyPrint(fml.fml, { paren: true, symbols })}`;
+    case "and": {
+      const newConfig: typeof config = {
+        symbols,
+        paren: (f) => f.type !== "and",
+      };
+      return withParen(
+        `${prettyPrint(fml.left, newConfig)} ${symbols.and} ${prettyPrint(fml.right, newConfig)}`,
+      );
+    }
+    case "or": {
+      const newConfig: typeof config = {
+        symbols,
+        paren: (f) => f.type !== "or",
+      };
+      return withParen(
+        `${prettyPrint(fml.left, newConfig)} ${symbols.or} ${prettyPrint(fml.right, newConfig)}`,
+      );
+    }
+    case "to": {
+      const newConfig: typeof config = {
+        symbols,
+        paren: (f) => f.type !== "to",
+      };
+      return withParen(
+        `${prettyPrint(fml.left, { symbols, paren: true })} ${symbols.to} ${prettyPrint(fml.right, newConfig)}`,
+      );
+    }
+    case "eq": {
+      const newConfig: typeof config = {
+        symbols,
+        paren: (f) => f.type !== "eq",
+      };
+      return withParen(
+        `${prettyPrint(fml.left, newConfig)} ${symbols.eq} ${prettyPrint(fml.right, newConfig)}`,
+      );
+    }
+  }
+}
+
+export function simplify(fml: Formula): Formula {
+  switch (fml.type) {
+    case "top":
+    case "bot":
+    case "propvar":
+      return fml;
+    case "not":
+    case "box":
+    case "diamond": {
+      const inner = simplify(fml.fml);
+      if (fml.type === "not" && inner.type === "not") return inner.fml;
+      if (fml.type === "not" && inner.type === "top") return bot;
+      if (fml.type === "not" && inner.type === "bot") return top;
+      if (fml.type === "box" && inner.type === "top") return top;
+      if (fml.type === "diamond" && inner.type === "bot") return bot;
+
+      return {
+        type: fml.type,
+        fml: inner,
+      };
+    }
+    case "or":
+    case "and":
+    case "to":
+    case "eq": {
+      const innerLeft = simplify(fml.left);
+      const innerRight = simplify(fml.right);
+
+      if (fml.type === "and" && innerLeft.type === "top") return innerRight;
+      if (fml.type === "and" && innerRight.type === "top") return innerLeft;
+      if (
+        fml.type === "and" &&
+        (innerLeft.type === "bot" || innerRight.type === "bot")
+      )
+        return bot;
+      if (fml.type === "or" && innerLeft.type === "bot") return innerRight;
+      if (fml.type === "or" && innerRight.type === "bot") return innerLeft;
+      if (
+        fml.type === "or" &&
+        (innerLeft.type === "top" || innerRight.type === "top")
+      )
+        return top;
+      if (fml.type === "to" && innerLeft.type === "top") return innerRight;
+      if (fml.type === "to" && innerLeft.type === "bot") return top;
+      if (fml.type === "to" && innerRight.type === "top") return top;
+      if (fml.type === "to" && innerRight.type === "bot")
+        return simplify(not(innerLeft));
+      if (fml.type === "eq" && innerLeft.type === "top") return innerRight;
+      if (fml.type === "eq" && innerRight.type === "top") return innerLeft;
+      if (fml.type === "eq" && innerRight.type === "bot")
+        return simplify(not(innerLeft));
+      if (fml.type === "eq" && innerLeft.type === "bot")
+        return simplify(not(innerRight));
+
+      return {
+        type: fml.type,
+        left: innerLeft,
+        right: innerRight,
+      };
+    }
+  }
+}
+
+export type NNFFormula<T = undefined> =
+  | { type: "top" | "bot"; tag: T }
+  | { type: "propvar"; name: PropVar; tag: T }
+  | { type: "not"; fml: { type: "propvar"; name: PropVar; tag: T }; tag: T }
+  | { type: "box" | "diamond"; fml: NNFFormula<T>; tag: T }
+  | {
+      type: "and" | "or";
+      left: NNFFormula<T>;
+      right: NNFFormula<T>;
+      tag: T;
+    };
+
+export function toNNF(fml: Formula): NNFFormula {
+  switch (fml.type) {
+    case "top":
+      return { ...fml, tag: undefined };
+    case "bot":
+      return { ...fml, tag: undefined };
+    case "propvar":
+      return { ...fml, tag: undefined };
+    case "box": {
+      return {
+        type: "box",
+        fml: toNNF(fml.fml),
+        tag: undefined,
+      };
+    }
+    case "diamond": {
+      return {
+        type: "diamond",
+        fml: toNNF(fml.fml),
+        tag: undefined,
+      };
+    }
+    case "to": {
+      return toNNF(or(not(fml.left), fml.right));
+    }
+    case "eq": {
+      return toNNF(
+        and(or(not(fml.left), fml.right), or(not(fml.right), fml.left)),
+      );
+    }
+    case "or": {
+      return {
+        type: "or",
+        left: toNNF(fml.left),
+        right: toNNF(fml.right),
+        tag: undefined,
+      };
+    }
+    case "and": {
+      return {
+        type: "and",
+        left: toNNF(fml.left),
+        right: toNNF(fml.right),
+        tag: undefined,
+      };
+    }
+    case "not": {
+      switch (fml.fml.type) {
+        case "top":
+          return { ...bot, tag: undefined };
+        case "bot":
+          return { ...top, tag: undefined };
+        case "propvar":
+          return {
+            type: "not",
+            fml: { ...fml.fml, tag: undefined },
+            tag: undefined,
+          };
+        case "not":
+          return toNNF(fml.fml.fml);
+        case "box":
+          return {
+            type: "diamond",
+            fml: toNNF(not(fml.fml.fml)),
+            tag: undefined,
+          };
+        case "diamond":
+          return { type: "box", fml: toNNF(not(fml.fml.fml)), tag: undefined };
+        case "or":
+          return {
+            type: "and",
+            left: toNNF(not(fml.fml.left)),
+            right: toNNF(not(fml.fml.right)),
+            tag: undefined,
+          };
+        case "and":
+          return {
+            type: "or",
+            left: toNNF(not(fml.fml.left)),
+            right: toNNF(not(fml.fml.right)),
+            tag: undefined,
+          };
+        case "to":
+          return {
+            type: "and",
+            left: toNNF(fml.fml.left),
+            right: toNNF(not(fml.fml.right)),
+            tag: undefined,
+          };
+        case "eq":
+          return {
+            type: "or",
+            left: {
+              type: "and",
+              left: toNNF(fml.fml.left),
+              right: toNNF(not(fml.fml.right)),
+              tag: undefined,
+            },
+            right: {
+              type: "and",
+              left: toNNF(not(fml.fml.left)),
+              right: toNNF(fml.fml.right),
+              tag: undefined,
+            },
+            tag: undefined,
+          };
+      }
+    }
+  }
+}
+
+export function tagNNF<T, U>(
+  fml: NNFFormula<T>,
+  tagger: (fml: Omit<NNFFormula<T>, "tag">, tag: T) => U,
+): NNFFormula<U> {
+  switch (fml.type) {
+    case "top":
+    case "bot":
+    case "propvar":
+      return { ...fml, tag: tagger(fml, fml.tag) };
+    case "not":
+      return {
+        type: "not",
+        fml: {
+          type: "propvar",
+          name: fml.fml.name,
+          tag: tagger(fml.fml, fml.fml.tag),
+        },
+        tag: tagger(fml, fml.tag),
+      };
+    case "box":
+    case "diamond":
+      return {
+        type: fml.type,
+        fml: tagNNF(fml.fml, tagger),
+        tag: tagger(fml, fml.tag),
+      };
+    case "and":
+    case "or":
+      return {
+        type: fml.type,
+        left: tagNNF(fml.left, tagger),
+        right: tagNNF(fml.right, tagger),
+        tag: tagger(fml, fml.tag),
+      };
+  }
+}