From c1af7bda259979388446a10afbbccf6398fd2adf Mon Sep 17 00:00:00 2001 From: cannorin Date: Sat, 15 Feb 2025 01:50:40 +0900 Subject: [PATCH] Initial commit --- .editorconfig | 9 +++ .gitignore | 175 +++++++++++++++++++++++++++++++++++++++ .vscode/settings.json | 16 ++++ LICENSE | 21 +++++ README.md | 90 +++++++++++++++++++++ biome.json | 49 +++++++++++ bun.lockb | Bin 0 -> 7016 bytes global.d.ts | 36 +++++++++ index.ts | 107 ++++++++++++++++++++++++ package.json | 19 +++++ parser.ts | 184 ++++++++++++++++++++++++++++++++++++++++++ semantics.ts | 168 ++++++++++++++++++++++++++++++++++++++ syntax.ts | 53 ++++++++++++ tsconfig.json | 24 ++++++ utils.ts | 51 ++++++++++++ 15 files changed, 1002 insertions(+) create mode 100644 .editorconfig create mode 100644 .gitignore create mode 100644 .vscode/settings.json create mode 100644 LICENSE create mode 100644 README.md create mode 100644 biome.json create mode 100755 bun.lockb create mode 100644 global.d.ts create mode 100644 index.ts create mode 100644 package.json create mode 100644 parser.ts create mode 100644 semantics.ts create mode 100644 syntax.ts create mode 100644 tsconfig.json create mode 100644 utils.ts diff --git a/.editorconfig b/.editorconfig new file mode 100644 index 0000000..c6c8b36 --- /dev/null +++ b/.editorconfig @@ -0,0 +1,9 @@ +root = true + +[*] +indent_style = space +indent_size = 2 +end_of_line = lf +charset = utf-8 +trim_trailing_whitespace = true +insert_final_newline = true diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..9b1ee42 --- /dev/null +++ b/.gitignore @@ -0,0 +1,175 @@ +# Based on https://raw.githubusercontent.com/github/gitignore/main/Node.gitignore + +# Logs + +logs +_.log +npm-debug.log_ +yarn-debug.log* +yarn-error.log* +lerna-debug.log* +.pnpm-debug.log* + +# Caches + +.cache + +# Diagnostic reports (https://nodejs.org/api/report.html) + +report.[0-9]_.[0-9]_.[0-9]_.[0-9]_.json + +# Runtime data + +pids +_.pid +_.seed +*.pid.lock + +# Directory for instrumented libs generated by jscoverage/JSCover + +lib-cov + +# Coverage directory used by tools like istanbul + +coverage +*.lcov + +# nyc test coverage + +.nyc_output + +# Grunt intermediate storage (https://gruntjs.com/creating-plugins#storing-task-files) + +.grunt + +# Bower dependency directory (https://bower.io/) + +bower_components + +# node-waf configuration + +.lock-wscript + +# Compiled binary addons (https://nodejs.org/api/addons.html) + +build/Release + +# Dependency directories + +node_modules/ +jspm_packages/ + +# Snowpack dependency directory (https://snowpack.dev/) + +web_modules/ + +# TypeScript cache + +*.tsbuildinfo + +# Optional npm cache directory + +.npm + +# Optional eslint cache + +.eslintcache + +# Optional stylelint cache + +.stylelintcache + +# Microbundle cache + +.rpt2_cache/ +.rts2_cache_cjs/ +.rts2_cache_es/ +.rts2_cache_umd/ + +# Optional REPL history + +.node_repl_history + +# Output of 'npm pack' + +*.tgz + +# Yarn Integrity file + +.yarn-integrity + +# dotenv environment variable files + +.env +.env.development.local +.env.test.local +.env.production.local +.env.local + +# parcel-bundler cache (https://parceljs.org/) + +.parcel-cache + +# Next.js build output + +.next +out + +# Nuxt.js build / generate output + +.nuxt +dist + +# Gatsby files + +# Comment in the public line in if your project uses Gatsby and not Next.js + +# https://nextjs.org/blog/next-9-1#public-directory-support + +# public + +# vuepress build output + +.vuepress/dist + +# vuepress v2.x temp and cache directory + +.temp + +# Docusaurus cache and generated files + +.docusaurus + +# Serverless directories + +.serverless/ + +# FuseBox cache + +.fusebox/ + +# DynamoDB Local files + +.dynamodb/ + +# TernJS port file + +.tern-port + +# Stores VSCode versions used for testing VSCode extensions + +.vscode-test + +# yarn v2 + +.yarn/cache +.yarn/unplugged +.yarn/build-state.yml +.yarn/install-state.gz +.pnp.* + +# IntelliJ based IDEs +.idea + +# Finder (MacOS) folder config +.DS_Store diff --git a/.vscode/settings.json b/.vscode/settings.json new file mode 100644 index 0000000..915c8bc --- /dev/null +++ b/.vscode/settings.json @@ -0,0 +1,16 @@ +{ + "editor.formatOnSave": true, + "typescript.tsdk": "node_modules/typescript/lib", + "[typescript]": { + "editor.defaultFormatter": "biomejs.biome" + }, + "[javascript]": { + "editor.defaultFormatter": "biomejs.biome" + }, + "[json]": { + "editor.defaultFormatter": "biomejs.biome" + }, + "[jsonc]": { + "editor.defaultFormatter": "biomejs.biome" + } +} diff --git a/LICENSE b/LICENSE new file mode 100644 index 0000000..026ea12 --- /dev/null +++ b/LICENSE @@ -0,0 +1,21 @@ +MIT License + +Copyright (c) 2024 cannorin + +Permission is hereby granted, free of charge, to any person obtaining a copy +of this software and associated documentation files (the "Software"), to deal +in the Software without restriction, including without limitation the rights +to use, copy, modify, merge, publish, distribute, sublicense, and/or sell +copies of the Software, and to permit persons to whom the Software is +furnished to do so, subject to the following conditions: + +The above copyright notice and this permission notice shall be included in all +copies or substantial portions of the Software. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR +IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, +FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE +AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER +LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, +OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE +SOFTWARE. diff --git a/README.md b/README.md new file mode 100644 index 0000000..fcbcd10 --- /dev/null +++ b/README.md @@ -0,0 +1,90 @@ +# KRIPKE + +## Setup + +To install dependencies: + +```bash +bun install +``` + +To run: + +```bash +bun run index.ts +``` + +This project was created using `bun init` in bun v1.1.33. [Bun](https://bun.sh) is a fast all-in-one JavaScript runtime. + +## Rules + +* A Kripke frame with 4 worlds are generated, +* You have a total of 10 moves. In each move you can do one of the following: + - Enter a modal formula. + - The game tells you in how many worlds the formula is valid (for every valuation). + - Guess the Kripke frame. + - If your frame is equal or isomorphic to the secret frame, you win. +* You lose when you run out of moves. + +A typical gameplay looks like this: +``` +Run !help for available commands. +A new Kripke frame is created! It has 4 worlds and 4 relations. +[10] Lp -> p +valid in 1 worlds, invalid in the rest. +[9] ~L0 +valid in 3 worlds, invalid in the rest. +[8] ML0 +valid in 1 worlds, invalid in the rest. +[7] (Lp -> p) & ML0 +invalid. +[6] M(Lp -> p) & ML0 +invalid. +[5] M(Lp -> p) +valid in 2 worlds, invalid in the rest. +[4] !guess aRa, bRc, bRd, dRa +incorrect. +[3] !guess aRa, bRc, dRa, dRb +incorrect. +[2] !guess aRa, bRc, dRa, dRc +incorrect. +[1] !guess aRa, bRc, dRa, aRd +correct! congratuations!! +id: 389 +a ==> a +a ==> c +b ==> d +c ==> a +``` + +## Syntax + +See `syntax.ts` for details. + +### Formulae + +You may use the following symbols: +* propositional variables, `p`, `q`, `r`, `s` (four are enough) +* verum: `T`, `⊤`, `1`, `\top` +* falsum: `F`, `⊥`, `0`, `\bot` +* negation: `~`, `¬`, `\neg`, `\lnot` +* box modality: `[]`, `□`, `L`, `\Box` +* diamond modality: `<>`, `⋄`, `M`, `\Diamond` +* conjunction: `&`, `^`, `∧`, `\wedge`, `\land` +* disjunction: `|`, `v`, `∨`, `\vee`, `\lor` +* implication: `->`, `→`, `\rightarrow`, `\to`, `\implies` +* equivalence: `<->`, `↔`, `\leftrightarrow`, `\iff` +* parentheses: `(`, `)` + +All operators are right associative. + +### Frames + +You may use the following symbols: +* worlds: `a`, `b`, `c`, `d` +* accessibility relation: `R`, `<`, `≺`, `\prec` +* comma: `,` (to separate relations) + +## License + +MIT diff --git a/biome.json b/biome.json new file mode 100644 index 0000000..c5ca063 --- /dev/null +++ b/biome.json @@ -0,0 +1,49 @@ +{ + "$schema": "https://biomejs.dev/schemas/1.9.1/schema.json", + "vcs": { + "enabled": true, + "clientKind": "git", + "useIgnoreFile": true + }, + "files": { + "ignoreUnknown": false, + "ignore": [".env", ".env.*", ".yarn/**/*", "*.*css"] + }, + "formatter": { + "enabled": true, + "indentStyle": "space" + }, + "organizeImports": { + "enabled": true + }, + "linter": { + "enabled": true, + "rules": { + "recommended": true + } + }, + "javascript": { + "formatter": { + "quoteStyle": "double" + } + }, + "overrides": [ + { + "include": ["*.svelte", "*.md"], + "linter": { + "rules": { + "correctness": { + "noUnusedLabels": "off" + }, + "suspicious": { + "noConfusingLabels": "off" + }, + "style": { + "useConst": "off", + "useImportType": "off" + } + } + } + } + ] +} diff --git a/bun.lockb b/bun.lockb new file mode 100755 index 0000000000000000000000000000000000000000..2a11a3e95bffd6de88aa5de563dd46feb3ed86f7 GIT binary patch literal 7016 zcmeHMd0bOh7Ji8lkh$x6sSIj~nVV77Jwj!e7f&&s_z(5w7MG&+m;6fc2s8v7| zQJ~_6W35$Dgx1k2xZ{Gjpr})2vF=h)=(#WNkuazQnLj$e>G}CM@7;U9@1A?!x#zwd zZHF*b3OO@EBxMSv^KBwjQX{zNVwoT&QY04ABV}?4UrC?OGNNJ_wy3Y*R^Zr{?lmi) zyVhRYy~Q~$cg@|98&8-XyaUvWSqYVvFbKp%t1!d=&}!n@pB#Wc_r@?a6YiijM7gF5*og;5fwmD5lWW5h2G-0laG$@Y#TO0X*ac4DIpG#{XRa zj03y@V9h#WI5CE_|I_Xm<_LI{0pS+qv&&z$0uAxX>Q%sGzly>qQ#b067nr zu4t4CkS~#qec(dR#&97)8a?YL_CJRm&3&4YVgF45J_@Gg)u*OCG;aJ?z36(*w7Es2 zI7Mr#hS(KUP7$ul`nPmqMaiYoc|v8(Su8jIZpf^gZ^Y)CoW&QLJr4F-dG-2(f1JXY zkNA4LWE>!~X;%(e)k~khUgMkQ^4rKm$^7^&mP@K^1jX)2y|1MvPT4qdx7hLaa4(OP zm6Nz*=DA&-aWLTWmEIGMOvNr%(E_(`1u_am1bRpMaYQRAJY-Zoy{E;Am~(lPi>arL zf-3G`-EYClVh_GNVug1&vngf}HMnS)bpR{GwZH3*sKP$EC4V1zyKM2|QYxQXfZK~1 zB3?4yaC_C>5zUU8rJKI3GrauEB8&2Ko4H$#xEpSBNa$BTW_8mxCqr-51MhuV5~p=qzjX(!Wj48rYRkI(a%jPufPP89#7(8N>39?@rxdim};pAm2L<%w0x7aUvW z-m7@Ft-MELS$5o}WS98an(HstI)q=Teo{fT6k7T0ydNH)RuN>$w_d0qc-26N_BAQA zAEw`71gsCu%=szFs8rs=*gWXifc%EuGvAXyw&T3L&deM{t6RE2D=>`Ki z+Y-HQ?~e8THthcGb8glIFY*K0tEA8ter;Y+Q(5FBm`e3I++&xg#@1%QVyEXfTo#=? zqB+I8j_r6c-%vg>>6H4FI$&VIHHzawYv$gPC3!S6(*x7uQQX2mLvjzd@@5-QmbYY? z{1TluVvom6KhGtDgC1{}J)(4P*xr!nbnSfjzM?xX=X0@TX3U&$W^bQh)k4b<-^`Lb zT)ULx&#EH{UNsP+vz-*$lhv{8e%>DW*|qN6!8Q4&QkLhdCKJhW@?1{QaqCBO>mv$eb?NV7qU`_^&cz zdi{j+YWEv_!?gdQS>Pk&^X3QhY@!M3Yy)# zzvcPoGqWbWaJ1`L<7FM-YLKxh|N2_*pe8+DGA|->+Jxb!2dC%nskBwwCoh{&QG{_X zC;D__zFqxU_8Z9+uju^^(@rccD_neO>zz3ptTp} zOHyd%-CoY&RqkK(wBqNbGpy%0u5@dzVLmlC8{PeZU76*{OuvoWOcqX}9vAfM8(gLF z3jThmQ0T#%mUPt^o8DL)kf3L;{&_-kVx&e11cxQeV?k+F4L4tMq_xy9?=&>C%AyY! zMfXjsco@^ycZPM-oz#rNpit)UGjqE6XzF;2(|5nk4K827)#F8ZofMj+y3%a_(LjrF zr;k6{V|{<-pw)-#71OHoWXjn&bz!0E>e+QMjq5{RReZ-4oOB$gd0U_uy_caVyHS!d zA}@1qfF3W32~ud!lKc5O&<3?E9oP5it#xnra)RF^dna1I*mtSCQgp~nc4c7Dj?kL# zqI}%m9-7&r33X$0DsALfo@}g1@l2?5TnxM&6_iIKL^6pG^a{ApZvjyM_d@1tQh$s? zI`JAlhW;4U^va^i=Uk^5{mH&o>eKH|2n(Y~#Z5Dw;2Zzk#{#*{D)gT-Ls)gZiwth^Xf#eAhu zp~SEufPrmjRWWc5ndL)OE{dK4Ab z!)CByEo4QEtVmHQUpg~540{$v*3QV<6_qj?#v>uCX=F7EFkA*3y@vN=N{P3O_0w{+ z-6RU3WWG?&m>91V%B6hqG^Jc5jT&oXuL}g{Hi4j22ymLxCbN9`H>qZ*kcry*+{$%- zWc5XnQlSvafibkgMl&_iuW=>>BkT$F5@*h7O8h6yEW(QOMCB6p7Q~(X`@#;3k&9wu zgmj5)u23vgE{GK>1kj@7;kQgEo$~Onjc5gwRN<>bH-a9^mn(#Vc}iuh!j;LC3!_8| zrF;QH8Y_ubFl6#5X1lRWdiypy9+wPdR03KlKF0?r+ZqFWIDn3aFyd(K7l=i4u}G?l zr^j<0+qA}sqz>$Mt#kQu=xEohrQpjY?<8s8PSCXPXtjkdQ7Oc24APqe@9fC(b<4x2 z!g1h@cQxyr(>Y@BTYFlvvGb(*o*^vNZ|Xdu_C4auC;0SQI!~wf7T)2=)&T3M4|Va> zcCpBTohEAy*)|LPD5};tY_rG?Q?+IVfTRCb!E-IXdEo)?{D6ZHKue$n zh#M)Sqz|y^jRIrPU^<)4u!lnq*`t!q6$wOtXp;UgV9|f1YZE^r`(rEO6o8IX(D4HX jH$a=WwYmBOc-#kg#svc11D(Tgg7X^Y)}ASUzQ4Z%=`U?G literal 0 HcmV?d00001 diff --git a/global.d.ts b/global.d.ts new file mode 100644 index 0000000..5912f19 --- /dev/null +++ b/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/index.ts b/index.ts new file mode 100644 index 0000000..247f322 --- /dev/null +++ b/index.ts @@ -0,0 +1,107 @@ +import { parse, parseFrame } from "./parser"; +import { + type Frame, + canonicals, + getFrame, + getId, + left, + mapping, + right, + validWorlds, + worlds, +} from "./semantics"; +import { sample } from "./utils"; + +import { stdin, stdout } from "node:process"; +import * as readline from "node:readline"; + +let frame: Frame = { relations: new Set() }; +let count = 0; + +const reset = () => { + frame = getFrame(sample(canonicals, 1)[0]); + count = 10; + console.log( + `A new Kripke frame is created! It has 4 worlds and ${frame.relations.size} relations.`, + ); +}; + +const show = () => { + console.log(`id: ${getId(frame)}`); + for (const rel of frame.relations) { + console.log(`${left(rel)} ==> ${right(rel)}`); + } +}; + +const query = (expr: string) => { + const fml = parse(expr); + return validWorlds(frame, fml).length; +}; + +const guess = (expr: string) => { + const relations = parseFrame(expr); + const id = mapping[getId({ relations })]; + return id === getId(frame); +}; + +const gameover = () => { + console.log("game over!"); + show(); + reset(); +}; + +const help = () => { + console.log(" ... check if the formula is valid in the frame"); + console.log("!guess ... guess the frame"); + console.log("!reset ... abandon this frame and start over"); + console.log("!show ... see the frame (CHEAT)"); + console.log("!help ... show this"); + console.log("!exit ... bye bye"); +}; + +const rl = readline.createInterface({ input: stdin, output: stdout }); +console.log("Run !help for available commands."); +reset(); +rl.setPrompt(`[${count}] `); +rl.on("line", (line) => { + const input = line.trim(); + if (input.startsWith("!reset")) reset(); + else if (input.startsWith("!show")) show(); + else if (input.startsWith("!exit")) rl.close(); + else if (input.startsWith("!help")) help(); + else if (input.startsWith("!guess")) { + const expr = input.replace("!guess", "").trim(); + try { + if (guess(expr)) { + console.log("correct! congratuations!!"); + show(); + reset(); + } else { + console.log("incorrect."); + count = count - 1; + } + } catch (e) { + console.log("invalid frame expression."); + console.log("example: aRa, aRb, bRb"); + } + } else { + try { + const num = query(input); + if (num === 0) { + console.log("invalid."); + } else if (num < worlds.length) { + console.log(`valid in ${num} worlds, invalid in the rest.`); + } else { + console.log("valid!"); + } + count = count - 1; + } catch (e) { + console.log("invalid formula"); + console.log("example: Mp -> LMp"); + } + } + if (count === 0) gameover(); + rl.setPrompt(`[${count}] `); + rl.prompt(); +}).on("close", () => process.exit(0)); +rl.prompt(); diff --git a/package.json b/package.json new file mode 100644 index 0000000..f8b9ba3 --- /dev/null +++ b/package.json @@ -0,0 +1,19 @@ +{ + "name": "kripke", + "module": "index.ts", + "devDependencies": { + "@types/bun": "latest" + }, + "peerDependencies": { + "typescript": "^5.0.0" + }, + "scripts": { + "lint": "biome check", + "fix": "biome check --fix" + }, + "type": "module", + "dependencies": { + "@biomejs/biome": "^1.9.4", + "typescript-parsec": "^0.3.4" + } +} diff --git a/parser.ts b/parser.ts new file mode 100644 index 0000000..c05a9da --- /dev/null +++ b/parser.ts @@ -0,0 +1,184 @@ +import { + type Token, + alt, + apply, + buildLexer, + expectEOF, + expectSingleResult, + kmid, + lrec_sc, + rule, + seq, + tok, +} from "typescript-parsec"; +import { type Relation, worlds } from "./semantics"; +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)))); +} + +const frameLexer = buildLexer([ + [true, /^[abcd]/g, "world" as const], + [true, /^(R|<|≺|\\prec)/g, "relation" as const], + [true, /^,/g, "separator" as const], + [false, /^\s+/g, "spaces" as const], +]); + +const RELATION = rule< + "world" | "relation" | "separator" | "spaces", + Set +>(); +RELATION.setPattern( + apply(seq(tok("world"), tok("relation"), tok("world")), ([x, _r, y]) => { + const w1 = x.text; + const w2 = y.text; + if (!worlds.includes(w1) || !worlds.includes(w2)) throw new Error(); + return new Set([`${w1}${w2}`]); + }), +); +const RELATIONS = rule< + "world" | "relation" | "separator" | "spaces", + Set +>(); +RELATIONS.setPattern( + lrec_sc( + RELATION, + seq(tok("separator"), RELATIONS), + (l, [_s, r]) => new Set([...l, ...r]), + ), +); + +export function parseFrame(expr: string): Set { + return expectSingleResult(expectEOF(RELATIONS.parse(frameLexer.parse(expr)))); +} diff --git a/semantics.ts b/semantics.ts new file mode 100644 index 0000000..cb96c4a --- /dev/null +++ b/semantics.ts @@ -0,0 +1,168 @@ +import { type Formula, type PropVar, and, 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]])), +); + +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 stats = { + equivalentPerRelations: new Uint16Array(relation.length), + }; + stats.equivalentPerRelations.fill(0); + + 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); + } + stats.equivalentPerRelations[relations.size]++; + } + + 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, stats }; +} + +const { canonicals, mapping } = generateAllFrames(); +export { canonicals, mapping }; diff --git a/syntax.ts b/syntax.ts new file mode 100644 index 0000000..df01341 --- /dev/null +++ b/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/tsconfig.json b/tsconfig.json new file mode 100644 index 0000000..2bb153e --- /dev/null +++ b/tsconfig.json @@ -0,0 +1,24 @@ +{ + "compilerOptions": { + // Enable latest features + "lib": ["ESNext", "DOM"], + "target": "ESNext", + "module": "ESNext", + "moduleDetection": "force", + "jsx": "react-jsx", + "allowJs": true, + // Bundler mode + "moduleResolution": "bundler", + "allowImportingTsExtensions": true, + "verbatimModuleSyntax": true, + "noEmit": true, + // Best practices + "strict": true, + "skipLibCheck": true, + "noFallthroughCasesInSwitch": true, + // Some stricter flags (disabled by default) + "noUnusedLocals": false, + "noUnusedParameters": false, + "noPropertyAccessFromIndexSignature": false + } +} diff --git a/utils.ts b/utils.ts new file mode 100644 index 0000000..ae09ddb --- /dev/null +++ b/utils.ts @@ -0,0 +1,51 @@ +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])) { + 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]); + } + 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, ...perm]); + } + } + return result; +} + +export function sample(arr: readonly T[], n: number = arr.length): T[] { + if (n > arr.length) return sample(arr, arr.length); + const copy = [...arr]; + for (let i = 0; i < n; i++) { + const j = i + Math.floor(Math.random() * (copy.length - i)); + [copy[i], copy[j]] = [copy[j] as T, copy[i] as T]; + } + return copy.slice(0, n); +}