Wyrm：基于开源正确性引擎的触控代数求解器

背景

在数学教育领域，代数方程的求解通常依赖纸笔演算或符号计算软件（如 Mathematica、SymPy），但这些工具要么缺乏交互性，要么无法提供精细的逐步操作反馈。另一方面，触控设备上的数学学习应用往往只做简单的计算器功能，或者通过有限状态机预设操作路径，难以覆盖代数变形的全部合法步骤。
Wyrm 项目正是为了解决这一矛盾而生：它提供了一个条件完备、逐步骤可验证的符号代数引擎，专门用于构建“可操控的数学界面”——用户可以直接拖动等式中的项跨越等号、点击幂次展开、提取公因子等，系统保证每一步操作都是合法的，并且非法的操作根本不可能发生。

核心内容

Wyrm 是一个精确的、条件完备的符号代数引擎，核心设计理念是：合法操作必须可行，非法操作必须不可行。它不采用传统的“验证等式是否成立”的思路，而是完全通过重写规则（rewrite rules）来变换方程，因此每个可达状态在构造上就是合法的。
这种合法性是有条件的：某些操作仅在特定条件下有效（例如除以 b 要求 b ≠ 0），或者可能引入增根（如两边同时乘方）。引擎不禁止这些操作，而是将条件升级为显式的、可视化的假设（Assumptions），随方程一同移动。

Wyrm 引擎使用纯 TypeScript 编写，零依赖、零 DOM，可运行于 Node.js、浏览器、Web Worker、原生 WebView 等任何环境。它也是移动端应用 Wyrm Math（iOS/Android）背后的引擎，该应用允许用户通过手势操作代数方程。引擎以 MIT 协议开源，而应用是项目的可持续方式。

引擎的公共 API 位于 src/index.ts，分为十个文档化类别，其结构类似目录。ARCHITECTURE.md 深入解释了不变式和合同。关键技术特性包括：

• 精确性：所有算术运算基于 bigint 有理数。表达式在未定义点（例如除以零、无理根）被视为无定义，绝不近似。引擎的全局正确性合同为“两者都有定义时真值相同”。
• 稳定 ID：每个节点拥有稳定 ID，操作不会改变未触及子树的 ID。这为命中检测和动画提供了基础：渲染器可以在重写前后匹配节点并进行刚性移动。
• 条件完备性：对于普通规则和“限制发射”规则，属性测试会拒绝替换那些不满足结果判断假设的实例，并断言真值保持。对于“扩展发射”规则，检查退化为单向（解不会丢失），并通过 checkSolution 覆盖增益义务。
• 析取（分支）：产生分支的规则会返回多个结果，这些结果解集的并集与原方程的解集相同（例如 x² = 9 ⇒ x = 3 或 x = -3）。推导树中所有分支都作为活跃、可导航的状态保留。

安装与测试：pnpm install 后使用 pnpm test（基于 vitest + fast-check 属性测试），pnpm typecheck 类型检查，pnpm build 输出 dist/（ESM + d.ts）。引擎必须保持无 DOM：tsconfig.json 不包含 DOM lib，test/boundary.test.ts 扫描源码中是否存在浏览器全局变量。

引擎采用 MIT 许可证。

关键要点

• 引擎核心不变式：合法操作可行，非法操作不可行。不验证方程，只通过重写规则变换，每个可达状态在构造上合法。
• 条件完备性：除以零、平方等可能引入非合法条件的操作不被禁止，而是生成显式的假设，随方程一起传播。
• 纯 TypeScript、零依赖、零 DOM：跨环境兼容（Node、浏览器、Worker、WebView）。
• 精确算术：使用 bigint 有理数，对未定义点（除以零、无理根）保持无定义，绝不近似。
• 稳定节点 ID：每个节点有稳定 id，操作保留未触及子树的 id，便于渲染器进行动画和命中检测。
• 析取分支：分支规则产生多个结果（如 x² = 9 产生 x=3 或 x=-3），所有分支在推导树中保持活跃。
• 公共 API 清晰：十类文档化接口，包括方程解析、推导、枚举移动、按 ID 应用规则、布局节点等。
• 测试与质量：属性测试（vitest + fast-check）是核心；确保引擎无 DOM 依赖；输出 ESM + TypeScript 声明文件。
• 开源与商业模式：引擎 MIT，但配套应用（Wyrm Math）是项目可持续的方式。

意义与影响

Wyrm 在符号代数引擎的设计上开辟了新路径：不是作为“计算器”或“证明器”，而是作为交互式数学操作的基础设施。它让教育类应用可以构建真正的“拖拽式”代数练习系统，用户每步操作都被引擎严格保证合法，同时条件假设透明可见，有助于学生理解代数变形的约束条件（如分母非零）。
其无 DOM、纯 TypeScript、零依赖的特性使其极易嵌入各种前端框架或原生应用。稳定 ID 设计为触控交互中的动画和手势识别提供了可靠基础。
从技术角度看，Wyrm 的属性测试方法和条件完备性模型可作为其他符号系统（如公式编辑器、定理证明器）的设计参考。开源 MIT 协议鼓励社区贡献，而付费应用模式为长期维护提供保障。
长远来看，Wyrm 可能推动更广泛的“可操控数学界面”发展——从代数到微积分、线性代数，让交互式数学教育从“看演示”进化为“动手操作”。