From 2e36390a5d752dfa03a5360dd1813f912ceed8cb Mon Sep 17 00:00:00 2001 From: cannorin Date: Mon, 17 Feb 2025 23:21:53 +0900 Subject: [PATCH] Add packages/kripke --- package.json | 1 + packages/kripke/biome.json | 3 + packages/kripke/global.d.ts | 36 ++++++++ packages/kripke/index.ts | 3 + packages/kripke/package.json | 22 +++++ packages/kripke/parser.ts | 148 +++++++++++++++++++++++++++++++ packages/kripke/semantics.ts | 162 ++++++++++++++++++++++++++++++++++ packages/kripke/syntax.ts | 53 +++++++++++ packages/kripke/tsconfig.json | 12 +++ packages/kripke/utils.ts | 41 +++++++++ yarn.lock | 24 +++++ 11 files changed, 505 insertions(+) create mode 100644 packages/kripke/biome.json create mode 100644 packages/kripke/global.d.ts create mode 100644 packages/kripke/index.ts create mode 100644 packages/kripke/package.json create mode 100644 packages/kripke/parser.ts create mode 100644 packages/kripke/semantics.ts create mode 100644 packages/kripke/syntax.ts create mode 100644 packages/kripke/tsconfig.json create mode 100644 packages/kripke/utils.ts diff --git a/package.json b/package.json index 3d5c730..4316ddc 100644 --- a/package.json +++ b/package.json @@ -11,6 +11,7 @@ }, "devDependencies": { "@biomejs/biome": "1.9.4", + "@tsconfig/strictest": "2.0.5", "turbo": "2.3.3" }, "engines": { diff --git a/packages/kripke/biome.json b/packages/kripke/biome.json new file mode 100644 index 0000000..52a1d9f --- /dev/null +++ b/packages/kripke/biome.json @@ -0,0 +1,3 @@ +{ + "extends": ["../../biome.json"] +} diff --git a/packages/kripke/global.d.ts b/packages/kripke/global.d.ts new file mode 100644 index 0000000..5912f19 --- /dev/null +++ b/packages/kripke/global.d.ts @@ -0,0 +1,36 @@ +interface String { + startsWith(searchString: S): this is `${S}${string}`; + endsWith(searchString: S): this is `${string}${S}`; + includes( + searchString: S, + position?: number, + ): this is `${string}${S}${string}`; +} + +type LiteralUnionLike = 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 { + includes( + searchElement: T extends LiteralUnionLike ? unknown : never, + fromIndex?: number, + ): searchElement is T extends LiteralUnionLike ? T : never; +} + +interface ReadonlyArray { + includes( + searchElement: T extends LiteralUnionLike ? unknown : never, + fromIndex?: number, + ): searchElement is T extends LiteralUnionLike ? T : never; +} diff --git a/packages/kripke/index.ts b/packages/kripke/index.ts new file mode 100644 index 0000000..b2ccf9a --- /dev/null +++ b/packages/kripke/index.ts @@ -0,0 +1,3 @@ +export * from "./syntax"; +export * from "./semantics"; +export * from "./parser"; diff --git a/packages/kripke/package.json b/packages/kripke/package.json new file mode 100644 index 0000000..31de2a4 --- /dev/null +++ b/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" + } +} diff --git a/packages/kripke/parser.ts b/packages/kripke/parser.ts new file mode 100644 index 0000000..44dcfa4 --- /dev/null +++ b/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, +): 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, + 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, + 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(); +const ANDOR = rule(); +const EXP = rule(); + +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)))); +} diff --git a/packages/kripke/semantics.ts b/packages/kripke/semantics.ts new file mode 100644 index 0000000..01abe67 --- /dev/null +++ b/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; +} + +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( + frame: T, + permutation: Map, +) { + const relations = new Set(); + 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(); + + 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 }; diff --git a/packages/kripke/syntax.ts b/packages/kripke/syntax.ts new file mode 100644 index 0000000..df01341 --- /dev/null +++ b/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 { + 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; diff --git a/packages/kripke/tsconfig.json b/packages/kripke/tsconfig.json new file mode 100644 index 0000000..9c1eff7 --- /dev/null +++ b/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 + } +} diff --git a/packages/kripke/utils.ts b/packages/kripke/utils.ts new file mode 100644 index 0000000..e4848b6 --- /dev/null +++ b/packages/kripke/utils.ts @@ -0,0 +1,41 @@ +const bitIsSet = (num: number, pos: number) => (num & (1 << pos)) !== 0; + +export function encode(all: readonly T[], set: Set): 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(all: readonly T[], flags: number): Set { + const total = 2 ** all.length; + if (flags < 0 || flags >= total) throw Error("invalid flags"); + const decoded = new Set(); + for (let j = 0; j < all.length; j++) { + if (bitIsSet(flags, j)) decoded.add(all[j] as T); + } + return decoded; +} + +export function* power(xs: readonly T[]) { + const total = 2 ** xs.length; + for (let i = 0; i < total; i++) { + yield decode(xs, i); + } +} + +export function permutations(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; +} diff --git a/yarn.lock b/yarn.lock index b16a56f..fde70a5 100644 --- a/yarn.lock +++ b/yarn.lock @@ -113,6 +113,15 @@ __metadata: languageName: node linkType: hard +"@cannorin/kripke@workspace:packages/kripke": + version: 0.0.0-use.local + resolution: "@cannorin/kripke@workspace:packages/kripke" + dependencies: + typescript: "npm:5.7.2" + typescript-parsec: "npm:0.3.4" + languageName: unknown + linkType: soft + "@emnapi/runtime@npm:^1.2.0": version: 1.3.1 resolution: "@emnapi/runtime@npm:1.3.1" @@ -890,6 +899,13 @@ __metadata: languageName: node linkType: hard +"@tsconfig/strictest@npm:2.0.5": + version: 2.0.5 + resolution: "@tsconfig/strictest@npm:2.0.5" + checksum: 10c0/cfc86da2d57f7b4b0827701b132c37a4974284e5c40649656c0e474866dfd8a69f57c6718230d8a8139967e2a95438586b8224c13ab0ff9d3a43eda771c50cc4 + languageName: node + linkType: hard + "@types/cookie@npm:^0.6.0": version: 0.6.0 resolution: "@types/cookie@npm:0.6.0" @@ -2401,6 +2417,7 @@ __metadata: resolution: "monorepo@workspace:." dependencies: "@biomejs/biome": "npm:1.9.4" + "@tsconfig/strictest": "npm:2.0.5" turbo: "npm:2.3.3" languageName: unknown linkType: soft @@ -3508,6 +3525,13 @@ __metadata: languageName: node linkType: hard +"typescript-parsec@npm:0.3.4": + version: 0.3.4 + resolution: "typescript-parsec@npm:0.3.4" + checksum: 10c0/fc467ad846c804af9e347a6801b2afeb85ace88e3add53b8e4ccff8290c9984d1bf35c350d72074e8c10792433ee5acc51570e2483b83520d99a50452039ff44 + languageName: node + linkType: hard + "typescript@npm:5.7.2": version: 5.7.2 resolution: "typescript@npm:5.7.2"