kripke: support word syntax

2025-02-22 10:53:58 +09:00
parent 64a4523e9f
commit d8e03512ad
4 changed files with 75 additions and 39 deletions
--- a/apps/web/src/routes/kripke/components/rules.svelte
+++ b/apps/web/src/routes/kripke/components/rules.svelte
@@ -1,5 +1,18 @@
 <script lang="ts">
 import Katex from "$lib/components/katex.svelte";
+import {
+  andSymbols,
+  botSymbols,
+  boxSymbols,
+  diamondSymbols,
+  eqSymbols,
+  lParenSymbols,
+  notSymbols,
+  orSymbols,
+  rParenSymbols,
+  toSymbols,
+  topSymbols,
+} from "@cannorin/kripke";
 import LuHeart from "lucide-svelte/icons/heart";

 let { relationSize }: { relationSize: number } = $props();
@@ -41,18 +54,24 @@ const validCount =
  </li>
 </ul>

+{#snippet symbols(words: string[])}
+  {#each words as word, i}
+    {i > 0 ? ", " : ""}<code>{word}</code>
+  {/each}
+{/snippet}
+
 <h2>Syntax</h2>
 <p>You may use the following symbols:</p>
 <ul>
-  <li>propositional variables: <code>p</code>, <code>q</code>, <code>r</code>, <code>s</code></li>
-  <li>verum: <code>⊤</code>, <code>T</code>, <code>1</code>, <code>\top</code></li>
-  <li>falsum: <code>⊥</code>, <code>F</code>, <code>0</code>, <code>\bot</code></li>
-  <li>negation: <code>¬</code>, <code>~</code>, <code>\neg</code>, <code>\lnot</code></li>
-  <li>box modality: <code>□</code>, <code>[]</code>, <code>!</code>, <code>L</code>, <code>\Box</code></li>
-  <li>diamond modality: <code>⋄</code>, <code>&lt;&gt;</code>, <code>?</code>, <code>M</code>, <code>\Diamond</code></li>
-  <li>conjunction: <code>∧</code>, <code>^</code>, <code>&amp;</code>,  <code>\wedge</code>, <code>\land</code></li>
-  <li>disjunction: <code>∨</code>, <code>v</code>, <code>|</code>, <code>\vee</code>, <code>\lor</code></li>
-  <li>implication: <code>→</code>, <code>-&gt;</code>, <code>&gt;</code>, <code>\rightarrow</code>, <code>\to</code></li>
-  <li>equivalence: <code>↔</code>,  <code>&lt;-&gt;</code>, <code>=</code>, <code>\leftrightarrow</code>, <code>\equiv</code></li>
-  <li>parentheses: <code>(</code>, <code>)</code></li>
+  <li>propositional variables: {@render symbols(["p", "q", "r", "s"])}</li>
+  <li>verum: {@render symbols(topSymbols)}</li>
+  <li>falsum: {@render symbols(botSymbols)}</li>
+  <li>negation: {@render symbols(notSymbols)}</li>
+  <li>box: {@render symbols(boxSymbols)}</li>
+  <li>diamond: {@render symbols(diamondSymbols)}</li>
+  <li>conjunction: {@render symbols(andSymbols)}</li>
+  <li>disjunction: {@render symbols(orSymbols)}</li>
+  <li>implication: {@render symbols(toSymbols)}</li>
+  <li>equivalence: {@render symbols(eqSymbols)}</li>
+  <li>parentheses: {@render symbols([...lParenSymbols, ...rParenSymbols])}</li>
 </ul>
--- a/packages/kripke/parser.ts
+++ b/packages/kripke/parser.ts
@@ -17,7 +17,7 @@ import {
  bot,
  box,
  diamond,
-  iff,
+  eq,
  not,
  or,
  propVars,
@@ -36,25 +36,42 @@ enum TokenKind {
  And = 6,
  Or = 7,
  To = 8,
-  Iff = 9,
+  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, /^[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)/g, TokenKind.To],
-  [true, /^(=|<->|↔|\\leftrightarrow|\\equiv)/g, TokenKind.Iff],
-  [true, /^(\(|\\left\()/g, TokenKind.LParen],
-  [true, /^(\)|\\right\))/g, TokenKind.RParen],
+  [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],
 ]);

@@ -96,7 +113,7 @@ function unary([op, value]: [
 function binary(
  left: Formula,
  [op, right]: [
-    Token<TokenKind.And | TokenKind.Or | TokenKind.To | TokenKind.Iff>,
+    Token<TokenKind.And | TokenKind.Or | TokenKind.To | TokenKind.Eq>,
    Formula,
  ],
 ): Formula {
@@ -107,8 +124,8 @@ function binary(
      return or(left, right);
    case TokenKind.To:
      return to(left, right);
-    case TokenKind.Iff:
-      return iff(left, right);
+    case TokenKind.Eq:
+      return eq(left, right);
    default:
      throw new Error(`Unknown binary operator: ${op.text}`);
  }
@@ -140,7 +157,7 @@ ANDOR.setPattern(
 );

 EXP.setPattern(
-  lrec_sc(ANDOR, seq(alt(tok(TokenKind.To), tok(TokenKind.Iff)), EXP), binary),
+  lrec_sc(ANDOR, seq(alt(tok(TokenKind.To), tok(TokenKind.Eq)), EXP), binary),
 );

 export function parse(expr: string): Formula {
--- a/packages/kripke/semantics.ts
+++ b/packages/kripke/semantics.ts
@@ -64,7 +64,7 @@ export function satisfy(m: Model, w: World, fml: Formula): boolean {
      if (!satisfy(m, w, fml.left)) return false;
      return satisfy(m, w, fml.right);
    }
-    case "iff": {
+    case "eq": {
      return satisfy(m, w, fml.left) === satisfy(m, w, fml.right);
    }
  }
--- a/packages/kripke/syntax.ts
+++ b/packages/kripke/syntax.ts
@@ -7,7 +7,7 @@ export type Formula =
  | { type: "propvar"; name: PropVar }
  | { type: "not" | "box" | "diamond"; fml: Formula }
  | {
-      type: "to" | "or" | "and" | "iff";
+      type: "to" | "or" | "and" | "eq";
      left: Formula;
      right: Formula;
    };
@@ -24,7 +24,7 @@ export function vars(fml: Formula): Set<PropVar> {
    case "to":
    case "or":
    case "and":
-    case "iff":
+    case "eq":
      return new Set([...vars(fml.left), ...vars(fml.right)]);
    case "propvar":
      return new Set([fml.name]);
@@ -49,8 +49,8 @@ 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;
+export const eq = (left: Formula, right: Formula) =>
+  ({ type: "eq", left, right }) as const satisfies Formula;

 export type Symbols = Record<Exclude<Formula["type"], "propvar">, string>;

@@ -63,7 +63,7 @@ export const asciiSymbols: Symbols = {
  and: "^",
  or: "v",
  to: "->",
-  iff: "<->",
+  eq: "<->",
 };

 export const unicodeSymbols: Symbols = {
@@ -75,7 +75,7 @@ export const unicodeSymbols: Symbols = {
  and: "∧",
  or: "∨",
  to: "→",
-  iff: "↔",
+  eq: "↔",
 };

 export const latexSymbols: Symbols = {
@@ -87,7 +87,7 @@ export const latexSymbols: Symbols = {
  and: "\\land",
  or: "\\lor",
  to: "\\to",
-  iff: "\\leftrightarrow",
+  eq: "\\leftrightarrow",
 };

 export function prettyPrint(
@@ -138,13 +138,13 @@ export function prettyPrint(
        `${prettyPrint(fml.left, { symbols, paren: true })} ${symbols.to} ${prettyPrint(fml.right, newConfig)}`,
      );
    }
-    case "iff": {
+    case "eq": {
      const newConfig: typeof config = {
        symbols,
-        paren: (f) => f.type !== "iff",
+        paren: (f) => f.type !== "eq",
      };
      return withParen(
-        `${prettyPrint(fml.left, newConfig)} ${symbols.iff} ${prettyPrint(fml.right, newConfig)}`,
+        `${prettyPrint(fml.left, newConfig)} ${symbols.eq} ${prettyPrint(fml.right, newConfig)}`,
      );
    }
  }