dicroce/wyrm_math

Source: https://github.com/dicroce/wyrm_math

wyrm-math

An exact, conditionally-sound symbolic algebra engine for building manipulative math interfaces — the kind where users solve equations by dragging terms across the equals sign, tapping a power to expand it, or pulling a shared factor out of two terms.

The core invariant: legal moves are possible, illegal moves are impossible. Equations are never validated — they are only ever transformed by rewrite rules, so every reachable state is sound by construction. And soundness is conditional: moves that are only valid under a condition (dividing by b requires b ≠ 0) or that can introduce extraneous solutions (multiplying both sides, squaring) are not forbidden — their conditions become first-class, visible Assumptions that travel with the equation.

Pure TypeScript, zero dependencies, zero DOM — runs in Node, browsers, workers, native webviews, anywhere.

wyrm-math is the engine behind Wyrm Math, a gesture-based algebra app for iOS and Android — try the in-browser demo or get the app. The engine is MIT; the app is how the project sustains itself.

import {
  parseEquation, Derivation,
  enumerateMoves, ruleById, layoutNode, exprToString,
} from "wyrm-math";

const d = new Derivation(parseEquation("2x + 3 = 11"));

// What can the user legally do right now?
const moves = enumerateMoves(d.current);

// Drag the 3 across the equals sign (the UI picks a Move; the engine
// guarantees it is legal — enumeration is precondition-checked):
const move = moves.find((m) => m.ruleId === "move-term-across")!;
d.apply(ruleById(move.ruleId), move.location, move.params);

console.log(exprToString(d.current.equation)); // 2x = 11 + -3

// Render it however you like: layoutNode gives positioned, id-keyed boxes
// and glyphs from static metric tables (no font measurement needed).
const layout = layoutNode(d.current.equation);

What’s inside

The public API is src/index.ts, organized into ten documented groups — it reads as a table of contents:

ARCHITECTURE.md explains the invariants and contracts in depth.

Design commitments

• Exactness. All arithmetic is bigint rationals. Points where an expression is undefined (division by zero, irrational roots) are treated as undefined, never approximated. The engine-wide soundness contract is truth-where-both-defined.
• Stable ids. Every node has an id; operations preserve the ids of untouched subtrees. This is the currency of hit testing and animation: a renderer can match nodes across a rewrite and move them rigidly.
• Conditional soundness. For ordinary and Restriction-emitting rules, property tests rejection-sample substitutions to those satisfying the result judgment’s assumptions and assert truth preservation. For Extension-emitting rules the check weakens to one direction (solutions are never lost), with checkSolution covering the gain obligation.
• Disjunction. Branching rules return several outcomes whose solution sets union to the original’s (x² = 9 ⇒ x = 3 or x = −3); the derivation tree holds all arms as live, navigable states.

Development

pnpm install
pnpm test        # vitest + fast-check (property tests are the soul of this project)
pnpm typecheck
pnpm build       # emits dist/ (ESM + d.ts)

The engine must stay DOM-free: tsconfig.json has no DOM lib and test/boundary.test.ts scans the sources for browser globals.

License

MIT