Add packages/kripke

packages/kripke/biome.json

@@ -0,0 +1,3 @@
+{
+  "extends": ["../../biome.json"]
+}

packages/kripke/global.d.ts

@@ -0,0 +1,36 @@
+interface String {
+  startsWith<S extends string>(searchString: S): this is `${S}${string}`;
+  endsWith<S extends string>(searchString: S): this is `${string}${S}`;
+  includes<S extends string>(
+    searchString: S,
+    position?: number,
+  ): this is `${string}${S}${string}`;
+}
+
+type LiteralUnionLike<T> = T extends string
+  ? T extends ""
+    ? T
+    : T extends `${T}${T}`
+      ? never
+      : T
+  : T extends number
+    ? `${T}0` extends `${number}`
+      ? T
+      : never
+    : T extends null | undefined
+      ? T
+      : never;
+
+interface Array<T> {
+  includes(
+    searchElement: T extends LiteralUnionLike<T> ? unknown : never,
+    fromIndex?: number,
+  ): searchElement is T extends LiteralUnionLike<T> ? T : never;
+}
+
+interface ReadonlyArray<T> {
+  includes(
+    searchElement: T extends LiteralUnionLike<T> ? unknown : never,
+    fromIndex?: number,
+  ): searchElement is T extends LiteralUnionLike<T> ? T : never;
+}

packages/kripke/index.ts

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

packages/kripke/package.json

@@ -0,0 +1,22 @@
+{
+  "name": "@cannorin/kripke",
+  "version": "0.0.1",
+  "private": true,
+  "exports": {
+    ".": "./index.ts",
+    "./syntax": "./syntax.ts",
+    "./semantics": "./semantics.ts",
+    "./parser": "./parser.ts"
+  },
+  "scripts": {
+    "build": "tsc",
+    "lint": "biome check",
+    "fix": "biome check --fix"
+  },
+  "devDependencies": {
+    "typescript": "5.7.2"
+  },
+  "dependencies": {
+    "typescript-parsec": "0.3.4"
+  }
+}

packages/kripke/parser.ts

@@ -0,0 +1,148 @@
+import {
+  type Token,
+  alt,
+  apply,
+  buildLexer,
+  expectEOF,
+  expectSingleResult,
+  kmid,
+  lrec_sc,
+  rule,
+  seq,
+  tok,
+} from "typescript-parsec";
+import {
+  type Formula,
+  and,
+  bot,
+  box,
+  diamond,
+  iff,
+  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,
+  Iff = 9,
+  LParen = 10,
+  RParen = 11,
+  Space = 12,
+}
+
+const lexer = buildLexer([
+  [true, /^[pqrs]/g, TokenKind.PropVar],
+  [true, /^(T|⊤|1|\\top)/g, TokenKind.Top],
+  [true, /^(F|⊥|0|\\bot)/g, TokenKind.Bot],
+  [true, /^(~|¬|\\neg|\\lnot)/g, TokenKind.Not],
+  [true, /^(\[\]|□|L|\\Box)/g, TokenKind.Box],
+  [true, /^(<>|⋄|M|\\Diamond)/g, TokenKind.Diamond],
+  [true, /^(&|\^|∧|\\wedge|\\land)/g, TokenKind.And],
+  [true, /^(\||v|∨|\\vee|\\lor)/g, TokenKind.Or],
+  [true, /^(->|→|\\rightarrow|\\to|\\implies)/g, TokenKind.To],
+  [true, /^(<->|↔|\\leftrightarrow|\\iff)/g, TokenKind.Iff],
+  [true, /^(\(|\\left\()/g, TokenKind.LParen],
+  [true, /^(\)|\\right\))/g, 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.Iff>,
+    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.Iff:
+      return iff(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.Iff)), EXP), binary),
+);
+
+export function parse(expr: string): Formula {
+  return expectSingleResult(expectEOF(EXP.parse(lexer.parse(expr))));
+}

packages/kripke/semantics.ts

@@ -0,0 +1,162 @@
+import { type Formula, type PropVar, propVars, vars } from "./syntax";
+import { decode, encode, permutations, power } from "./utils";
+
+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 relation: Relation[] = worlds.flatMap((w) =>
+  worlds.map((x) => `${w}${x}` as const),
+);
+
+export interface Frame {
+  relations: Set<Relation>;
+}
+
+export interface Model extends Frame {
+  valuations: Set<`${World}${PropVar}`>;
+}
+
+export function valuation(fml?: Formula): `${World}${PropVar}`[] {
+  const vs = fml ? Array.from(vars(fml)) : propVars;
+  return worlds.flatMap((w) => vs.map((p) => `${w}${p}` as const));
+}
+
+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 "iff": {
+      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 validInFrame(f: Frame, fml: Formula) {
+  for (const valuations of power(valuation(fml))) {
+    if (!validInModel({ ...f, valuations }, fml)) return false;
+  }
+  return true;
+}
+
+export function validWorlds(f: Frame, fml: Formula) {
+  const result: World[] = [];
+  for (const w of worlds) {
+    let valid = true;
+    for (const valuations of power(valuation(fml))) {
+      if (!satisfy({ ...f, valuations }, w, fml)) {
+        valid = false;
+        break;
+      }
+    }
+    if (valid) result.push(w);
+  }
+  return result;
+}
+
+export function getFrame(id: number): Frame {
+  return { relations: decode(relation, id) };
+}
+
+export function getId(frame: Frame) {
+  return encode(relation, frame.relations);
+}
+
+const worldPermutations = permutations(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 map = new Map<number, number>();
+
+  const total = 2 ** relation.length;
+  for (let id = 0; id < total; id++) {
+    if (map.has(id)) continue;
+
+    const relations = decode(relation, id);
+    const frame = { relations };
+    const equivalentIds: number[] = [];
+
+    let canonicalId = id;
+    for (const perm of worldPermutations) {
+      const permuted = applyPermutation(frame, perm);
+      const permutedId = encode(relation, permuted.relations);
+      equivalentIds.push(permutedId);
+      if (canonicalId === null || permutedId < canonicalId) {
+        canonicalId = permutedId;
+      }
+    }
+
+    canonicals.push(canonicalId);
+    for (const equivalentId of equivalentIds) {
+      map.set(equivalentId, canonicalId);
+    }
+  }
+
+  const mapping: Uint16Array = new Uint16Array(total);
+  for (let id = 0; id < total; id++) {
+    const value = map.get(id);
+    if (value === undefined) throw Error(`impossible (${id})`);
+    mapping[id] = value;
+  }
+
+  return { canonicals, mapping };
+}
+
+const { canonicals, mapping } = generateAllFrames();
+export { canonicals, mapping };

packages/kripke/syntax.ts

@@ -0,0 +1,53 @@
+export type PropVar = "p" | "q" | "r" | "s";
+
+export const propVars: PropVar[] = ["p", "q", "r", "s"];
+
+export type Formula =
+  | { type: "top" | "bot" }
+  | { type: "propvar"; name: PropVar }
+  | { type: "not" | "box" | "diamond"; fml: Formula }
+  | {
+      type: "to" | "or" | "and" | "iff";
+      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 "iff":
+      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 iff = (left: Formula, right: Formula) =>
+  ({ type: "iff", left, right }) as const satisfies Formula;

packages/kripke/tsconfig.json

@@ -0,0 +1,12 @@
+{
+  "extends": "@tsconfig/strictest/tsconfig.json",
+  "compilerOptions": {
+    "target": "esnext",
+    "lib": ["esnext"],
+    "module": "esnext",
+    "moduleResolution": "Bundler",
+    "resolveJsonModule": true,
+    "noEmit": true,
+    "allowSyntheticDefaultImports": true
+  }
+}

packages/kripke/utils.ts

@@ -0,0 +1,41 @@
+const bitIsSet = (num: number, pos: number) => (num & (1 << pos)) !== 0;
+
+export function encode<T>(all: readonly T[], set: Set<T>): number {
+  let flags = 0;
+  for (let i = 0; i < all.length; i++) {
+    if (set.has(all[i] as T)) {
+      flags |= 1 << i;
+    }
+  }
+  return flags;
+}
+
+export function decode<T>(all: readonly T[], flags: number): Set<T> {
+  const total = 2 ** all.length;
+  if (flags < 0 || flags >= total) throw Error("invalid flags");
+  const decoded = new Set<T>();
+  for (let j = 0; j < all.length; j++) {
+    if (bitIsSet(flags, j)) decoded.add(all[j] as T);
+  }
+  return decoded;
+}
+
+export function* power<T>(xs: readonly T[]) {
+  const total = 2 ** xs.length;
+  for (let i = 0; i < total; i++) {
+    yield decode(xs, i);
+  }
+}
+
+export function permutations<T>(arr: readonly T[]): T[][] {
+  if (arr.length === 0) return [[]];
+  const result: T[][] = [];
+  for (let i = 0; i < arr.length; i++) {
+    const current = arr[i];
+    const remaining = [...arr.slice(0, i), ...arr.slice(i + 1)];
+    for (const perm of permutations(remaining)) {
+      result.push([current as T, ...perm]);
+    }
+  }
+  return result;
+}