摘要

本文介紹一個(gè)以 MoonBit 實(shí)現(xiàn)的符號(hào)計(jì)算內(nèi)核 Symbit，目標(biāo)是通過(guò)AI輔助，在保留 sympy 風(fēng)格符號(hào)表達(dá)與精確計(jì)算能力的同時(shí)，將大部分算法移植到 MoonBit，利用 native 與 WebAssembly 后端提升執(zhí)行效率并降低用戶訪問(wèn)門檻，理想情況下用戶只需要用瀏覽器即可訪問(wèn)此計(jì)算系統(tǒng)。

我們重點(diǎn)討論表達(dá)式表示的差異化設(shè)計(jì)，并通過(guò) differential testing 與基準(zhǔn)測(cè)試評(píng)估其正確性與性能。在若干典型 workload 上，該實(shí)現(xiàn)相對(duì)原始 Python/sympy 路徑取得數(shù)倍的 native 性能提升，在瀏覽器上使用 WASM 亦可得到 2x 的平均性能提升，更提高了可訪問(wèn)性。

引言

計(jì)算機(jī)代數(shù)系統(tǒng)(computer algebra system, CAS)是計(jì)算機(jī)科學(xué)和數(shù)學(xué)領(lǐng)域的重要工具，可以對(duì)表達(dá)式進(jìn)行構(gòu)造、變換、化簡(jiǎn)與求解。與數(shù)值計(jì)算不同，符號(hào)計(jì)算更強(qiáng)調(diào)精確性、可解釋性與結(jié)構(gòu)保持，操作的對(duì)象通常是表達(dá)式樹(shù)。例如，有理數(shù)應(yīng)以精確分?jǐn)?shù)而非浮點(diǎn)近似表示，多項(xiàng)式應(yīng)保留其代數(shù)結(jié)構(gòu)而非退化為采樣結(jié)果，矩陣運(yùn)算與方程求解也往往需要在精確域上完成。

在現(xiàn)有開(kāi)源生態(tài)中，sympy 以 Python 為宿主語(yǔ)言，為符號(hào)表達(dá)、代數(shù)變換、微積分、矩陣、方程求解和多項(xiàng)式計(jì)算等任務(wù)提供了統(tǒng)一而靈活的抽象接口。其優(yōu)勢(shì)在于能夠與 Python 的科學(xué)計(jì)算生態(tài)自然結(jié)合。

然而，這種設(shè)計(jì)也繼承了動(dòng)態(tài)語(yǔ)言運(yùn)行時(shí)的若干工程特征：大量細(xì)粒度對(duì)象分配、深層遞歸遍歷、頻繁的動(dòng)態(tài)分派，以及在表達(dá)式重寫(xiě)過(guò)程中反復(fù)進(jìn)行的結(jié)構(gòu)構(gòu)造與析構(gòu)。在以表達(dá)式規(guī)范化、多項(xiàng)式操作、精確線性代數(shù)為代表的一類高頻符號(hào)負(fù)載中，這些開(kāi)銷會(huì)逐步累積，并成為性能瓶頸之一。換言之，符號(hào)計(jì)算系統(tǒng)的效率問(wèn)題并不總是來(lái)自「數(shù)學(xué)算法本身不夠好」，也常常來(lái)自其承載算法的數(shù)據(jù)表示與運(yùn)行時(shí)執(zhí)行模型。此外，因?yàn)?Python 是動(dòng)態(tài)類型語(yǔ)言，sympy 的實(shí)現(xiàn)也很難通過(guò)靜態(tài)分析來(lái)保證運(yùn)行時(shí)無(wú)類型錯(cuò)誤。

除了執(zhí)行效率，符號(hào)計(jì)算系統(tǒng)的可部署性同樣值得關(guān)注。盡管桌面或服務(wù)器環(huán)境中的 Python 生態(tài)已經(jīng)相當(dāng)成熟，但當(dāng)目標(biāo)場(chǎng)景轉(zhuǎn)向?yàn)g覽器時(shí)，傳統(tǒng)方案往往面臨更高的接入成本：用戶也許會(huì)期望「打開(kāi)網(wǎng)頁(yè)即可使用」，而不是預(yù)先安裝解釋器、環(huán)境或依賴;另一方面，前端交互式教學(xué)、在線計(jì)算工具和嵌入式數(shù)學(xué)組件等應(yīng)用，也要求核心引擎能夠以更輕量的方式部署到 Web 環(huán)境中。對(duì)于此類場(chǎng)景而言，一個(gè)既能在 native 環(huán)境高效運(yùn)行、又能以 WebAssembly 形式直接進(jìn)入瀏覽器的符號(hào)計(jì)算內(nèi)核，具有明確的工程意義。

基于上述動(dòng)機(jī)，我們提出 Symbit，一個(gè)用 MoonBit 實(shí)現(xiàn)的符號(hào)計(jì)算內(nèi)核。其算法設(shè)計(jì)主要參照 sympy，但在實(shí)現(xiàn)層面上，我們重新審視了表達(dá)式對(duì)象設(shè)計(jì)、規(guī)范化、精確有理數(shù)、多項(xiàng)式操作與矩陣消元等核心結(jié)構(gòu)，并通過(guò)差分測(cè)試驗(yàn)證其正確性。最后我們將在 native 與 WebAssembly 兩類環(huán)境中評(píng)估其性能表現(xiàn)。

設(shè)計(jì)邊界

本節(jié)討論我們的設(shè)計(jì)的目標(biāo)與非目標(biāo)。

語(yǔ)義兼容性的目標(biāo)

Symbit 的首要目標(biāo)是在可觀測(cè)語(yǔ)義上盡可能保持 sympy 風(fēng)格的符號(hào)行為。這里的「可觀測(cè)語(yǔ)義」至少包括四層：

API 的基本行為：一個(gè)用戶在構(gòu)造表達(dá)式、調(diào)用化簡(jiǎn)、求解、多項(xiàng)式操作或矩陣運(yùn)算時(shí)，得到的對(duì)象種類與主要結(jié)果形態(tài)應(yīng)與 sympy 保持一致;

對(duì)象語(yǔ)義：例如 Add、Mul、Pow 等核心表達(dá)式節(jié)點(diǎn)在構(gòu)造時(shí)如何進(jìn)行扁平化、系數(shù)合并、參數(shù)保序與未求值保留;

精確數(shù)值與集合語(yǔ)義：整數(shù)、有理數(shù)、有限集合、區(qū)間、條件集合等對(duì)象必須按照精確代數(shù)語(yǔ)義傳播，而不能為了簡(jiǎn)化實(shí)現(xiàn)輕易退化為浮點(diǎn)近似或字符串占位丟失信息;

觀測(cè)語(yǔ)義：打印、展示與前端集成行為，這一層較為靈活，輸出字符串可與 sympy 不同，但是語(yǔ)義等價(jià)。

工程目標(biāo)

在語(yǔ)義兼容之外，Symbit 將通過(guò)新的實(shí)現(xiàn)基座改善執(zhí)行效率，尤其是 native 場(chǎng)景下的表達(dá)式重寫(xiě)、多項(xiàng)式計(jì)算、精確矩陣運(yùn)算與部分求解。當(dāng)然性能目標(biāo)并不是抽象的「整體更快」盡管使用 MoonBit 重寫(xiě)確實(shí)可以免費(fèi)獲得這一點(diǎn)，但更多的也包含一些算法決策級(jí)別的優(yōu)化。

MoonBit 是多后端編程語(yǔ)言，這帶來(lái)了一些額外好處：我們可以近乎免費(fèi)地獲得 WebAssembly 部署能力，理論上用戶可以直接在瀏覽器中使用 Symbit，而不需要安裝 Python 環(huán)境或依賴。這對(duì)于在線教學(xué)、交互式計(jì)算工具和嵌入式數(shù)學(xué)組件等應(yīng)用場(chǎng)景具有明顯的吸引力。令人驚喜的是，我們最終也完成了這個(gè)目標(biāo)。

非目標(biāo)

Sympy 有部分包還依賴于 Python 的一些特性，例如 multidispatch 利用 class 機(jī)制做多重分派，這在 MoonBit 中并無(wú)直接對(duì)應(yīng)，也有依賴于其他復(fù)雜 Python 庫(kù)的包，例如 plotting 依賴于 matplotlib，因此本文并不宣稱已經(jīng)完整遷移 sympy 全部頂層包，而是把目標(biāo)限定在核心 symbolic engine 相關(guān)的包，例如 core、polys、matrices、solvers 等，它們占據(jù)了 sympy 90% 的代碼。

評(píng)估邊界

我們采用如下方法評(píng)定 Symbit 的完成度：

新增功能必須同時(shí)具備局部行為測(cè)試與 parity/oracle (差分) 測(cè)試，且后者必須覆蓋到核心語(yǔ)義邊界;

通過(guò)靜態(tài)類型系統(tǒng)把所有類型錯(cuò)誤暴露在編譯階段，而不是運(yùn)行時(shí);

在 native 場(chǎng)景下，Symbit 的算法應(yīng)該比對(duì)應(yīng)的 sympy 算法有數(shù)倍的性能提升。

系統(tǒng)架構(gòu)

一個(gè)符號(hào)計(jì)算系統(tǒng)的難點(diǎn)在于如何將這些算法如何被組織到統(tǒng)一的對(duì)象模型之下，否則就很難稱為一個(gè)「系統(tǒng)」，而更像是一些獨(dú)立的工具庫(kù)。如果表達(dá)式表示、精確數(shù)值、多項(xiàng)式、矩陣和求解器各自維護(hù)一套局部規(guī)則，那么系統(tǒng)規(guī)模一旦變大，就會(huì)出現(xiàn)語(yǔ)義不一致、重復(fù)實(shí)現(xiàn)、難以測(cè)試等問(wèn)題。因而本章節(jié)將討論 Symbit 的整體架構(gòu)，以及它與 sympy 在組織方式上的相似與不同。

Sympy 的對(duì)象模型

Sympy 的核心是圍繞 Basic / Expr 的基于類繼承的表達(dá)式樹(shù)。無(wú)論是 Add、Mul、Pow 這表表達(dá)式基礎(chǔ)結(jié)構(gòu)，還是矩陣、集合、關(guān)系、函數(shù)應(yīng)用與特殊對(duì)象，都需要接入這一套動(dòng)態(tài)對(duì)象模型，通過(guò)繼承來(lái)組織表達(dá)式，其關(guān)系大致是 Add <: Expr <: Basic，在解析 + 的時(shí)候會(huì)構(gòu)造一個(gè) Add 對(duì)象，Add 的參數(shù)又是其他 Expr 對(duì)象，依此類推。一旦某個(gè)對(duì)象被納入 Basic 體系，它就自動(dòng)獲得了打印、比較、替換、遍歷、匹配、重寫(xiě)等一系列通用能力。

classBasic(Printable):
  __slots__ = ('_mhash','_args','_assumptions')

  is_number =False
  is_Atom =False
  is_Symbol =False
  is_Add =False
  is_Mul =False
  is_Pow =False
  ...

@sympify_method_args
classExpr(Basic, EvalfMixin):
  __slots__ = ()
  ...

這讓系統(tǒng)在可擴(kuò)展性和可讀性上都非常成功，特別適合逐步長(zhǎng)出一個(gè)覆蓋面極廣的 CAS 生態(tài)。但它也存在許多不足：很多原本可以在更低層被隔離的成本，最終都會(huì)回落到通用對(duì)象系統(tǒng)中，例如對(duì)象構(gòu)造開(kāi)銷、動(dòng)態(tài)分派、運(yùn)行時(shí)比較與容器重建。并且因?yàn)?Python 的動(dòng)態(tài)類型系統(tǒng)，若寫(xiě)出類型 / 類不匹配的問(wèn)題時(shí)很難在編譯階段發(fā)現(xiàn)。

Symbit 的代數(shù)數(shù)據(jù)類型

Symbit 在總體上仍然保留了 sympy 的主題劃分，例如 symcore、sympolys、symmatrices、symsolvers、symsimplify 等包大體對(duì)應(yīng)上游的數(shù)學(xué)模塊。其中最底層的是 symcore 與 symnum。前者負(fù)責(zé)表達(dá)式節(jié)點(diǎn)、規(guī)范化、比較、替換、遍歷以及若干基礎(chǔ)對(duì)象語(yǔ)義，后者則提供精確整數(shù)、有理數(shù)以及部分?jǐn)?shù)值兼容層 (因此我們也重寫(xiě)了 Python 的任意精度浮點(diǎn)數(shù)庫(kù) mpmath)。

盡管我們可以用 tagless final 和 trait 來(lái)模仿 class 風(fēng)格的代碼組織，但這里我們選擇了一種更直接的風(fēng)格：用一個(gè)單一的代數(shù)數(shù)據(jù)類型來(lái)表示所有表達(dá)式節(jié)點(diǎn)，因此 Parser 的代碼會(huì)相對(duì)耦合一些，借助模式匹配和窮盡檢查等功能(擴(kuò)展變體可讓類型檢查器發(fā)現(xiàn)遺漏之處)，代碼也能保持相當(dāng)清晰。

pub(all)enumExpr{
 Number(@symnum.BigRational)
 Float(Float)
 NumberSymbol(NumberSymbolKind)
 Boolean(Bool)
 Apply(Expr, Array[Expr])
 Add(Array[Expr])
 Mul(Array[Expr])
 Pow(Expr, Expr)
 Mod(Expr, Expr)
 Tuple(Array[Expr])
 Dict(Array[(Expr, Expr)])
 ...
}

這本質(zhì)上算是一個(gè)表達(dá)式問(wèn)題，但考慮到未來(lái) MoonBit 可能會(huì)加入 Extensible Variants 的支持，且數(shù)學(xué)領(lǐng)域很多東西也是多年不變的，我們認(rèn)為此種做法或不會(huì)受到太多維護(hù)成本的影響，并且相比 sympy 在許多方面是更優(yōu)的。另一方面，sympy 很多表達(dá)式處理都是借助節(jié)點(diǎn)的「內(nèi)在屬性」，因而有時(shí)候需要傳遞一些額外的參數(shù)來(lái)維持這些屬性，例如evaluate=False來(lái)控制是否在構(gòu)造時(shí)進(jìn)行規(guī)范化。

classAdd(Expr, AssocOp):
  ...

classAssocOp(Basic):
  @cacheit
 def__new__(cls, *args, evaluate=None, _sympify=True):
    ...

Symbit 則使用「智能構(gòu)造子」形式來(lái)應(yīng)對(duì)不同場(chǎng)景的規(guī)范化需求，可以在一定程度上解耦合（實(shí)際上，在編寫(xiě) Symbit 引擎的過(guò)程中我們還發(fā)現(xiàn)了 sympy 真實(shí)存在的因?yàn)閰?shù)傳遞和弱類型導(dǎo)致的 bug）：

pubfnexpr_new_raw(op:ExprOp,args:Array[@symcore.Expr])-> @symcore.Expr{
 matchop{
   ExprOp::Add => @symcore.raw_add(args)
    ExprOp::Mul => @symcore.raw_mul(args)
    ExprOp::Pow => @symcore.raw_pow(args[0], args[1])
    ExprOp::Function(name) => @symcore.raw_function(name, args)
    ...
  }
}

pubfnexpr_new_eval(op:ExprOp,args:Array[@symcore.Expr])-> @symcore.Expr{
 matchop{
   ExprOp::Add => @symcore.add(args)
    ExprOp::Mul => @symcore.mul(args)
    ExprOp::Pow => @symcore.pow(args[0], args[1])
    ExprOp::Function(name) => @symcore.function(name, args)
    ...
  }
}

在此之上則是各種代數(shù)基礎(chǔ)設(shè)施包，例如之前提到的 sympolys 和 symmatrices (分別用于多項(xiàng)式處理和矩陣計(jì)算)。還有一個(gè) sympy 包，顧名思義，是一個(gè) parity 層，專門用來(lái)調(diào)用 sympy 進(jìn)行 oracle 測(cè)試。下一節(jié)我們將討論它的設(shè)計(jì)，以及它在整個(gè)系統(tǒng)中的作用。

測(cè)試系統(tǒng)

符號(hào)系統(tǒng)面對(duì)的是結(jié)構(gòu)對(duì)象，這些對(duì)象往往存在多種語(yǔ)義等價(jià)但結(jié)構(gòu)不同的表示形式，并且很多錯(cuò)誤并不會(huì)立刻表現(xiàn)為程序崩潰，而是表現(xiàn)為規(guī)范形不穩(wěn)定、定義域被忽略、過(guò)早求值或錯(cuò)誤地返回了一個(gè)看似合理的表達(dá)式。因此，Symbit 的測(cè)試系統(tǒng)從一開(kāi)始就并不只是依賴于簡(jiǎn)單的單元測(cè)試，而采用一個(gè)分層驗(yàn)證體系：用快照測(cè)試記錄可觀察表示，用行為測(cè)試約束局部語(yǔ)義，用 parity / oracle 測(cè)試對(duì)照 sympy，并在必要時(shí)直接嵌入 CPython 運(yùn)行時(shí)來(lái)復(fù)用其參考語(yǔ)義。

更形式化地說(shuō)，我們希望驗(yàn)證的并不是單個(gè)函數(shù)的一個(gè)輸出值，而是一個(gè) MoonBit 實(shí)現(xiàn) f_mb與一個(gè) sympy 參考實(shí)現(xiàn) f_sp在輸入域 D 上的觀測(cè)等價(jià)性(當(dāng)然，D 的表示也因語(yǔ)言不同而存在差異)

其中關(guān)系 并不總是簡(jiǎn)單的字符串相等。在某些場(chǎng)景下，可以是完全結(jié)構(gòu)相等;在另一些場(chǎng)景下，它可能是經(jīng)規(guī)范化后的表達(dá)式相等、殘差為零(下方公式) 、集合意義下等價(jià)，或在浮點(diǎn)物理量場(chǎng)景中滿足一定誤差界，測(cè)試設(shè)計(jì)者應(yīng)該根據(jù)對(duì)象語(yǔ)義選擇合適的比較關(guān)系。

MoonBit 的快照式測(cè)試

在最基礎(chǔ)的一層，Symbit 大量使用 MoonBit 自帶的 inspect(..., content=...) 風(fēng)格測(cè)試來(lái)記錄穩(wěn)定輸出。這種測(cè)試主要用來(lái)固定一段當(dāng)前實(shí)現(xiàn)的可觀察表示，尤其適合打印器、parser、debug representation 以及某些公開(kāi) API 的回歸驗(yàn)證。與傳統(tǒng)手寫(xiě) assert_eq 相比，這種寫(xiě)法在符號(hào)系統(tǒng)里尤其自然，更大的便利是當(dāng)輸出改變時(shí)可以直接給出 diff，檢查正確后可用 moon test -u 來(lái)更新快照，而不需要手動(dòng)修改斷言文本。如果沒(méi)有成體系的快照更新機(jī)制，這類工作往往會(huì)退化成機(jī)械地逐條修改斷言文本，既低效，也容易遺漏。

test"prelude constructors round trip through printers"{
letexpr = add([
 integer(1),
  mul([Symbol("x"), pow(Symbol("y"),integer(2))]),
 ])
 debug_inspect(expr, content="(+ (* sym:x (^ sym:y 2)) 1)")
 inspect(expr, content="x*y**2 + 1")
}

這里的兩個(gè) inspect 實(shí)際上對(duì)應(yīng)兩類不同的斷言。前者是內(nèi)部結(jié)構(gòu)快照(通過(guò) Debug trait 實(shí)現(xiàn))，用來(lái)保證表達(dá)式構(gòu)造與規(guī)范化沒(méi)有悄悄改變底層表示;后者是用戶可見(jiàn)輸出快照，用來(lái)保證打印行為與 API 接口的穩(wěn)定性。這兩類快照都很重要，因?yàn)閷?duì)于符號(hào)系統(tǒng)而言， 「內(nèi)部結(jié)構(gòu)變化但外部字符串不變」與「外部字符串變化但內(nèi)部結(jié)構(gòu)不變」都可能導(dǎo)致一些意外的回歸問(wèn)題。

Oracle / Parity Testing 的原理

僅靠快照測(cè)試仍然不夠。符號(hào)系統(tǒng)中更難的問(wèn)題在于， 「看起來(lái)不同」的結(jié)果可能是等價(jià)的，而「看起來(lái)合理」的結(jié)果也可能在語(yǔ)義上是錯(cuò)的。因此，Symbit 在包級(jí)遷移中采用了第二層測(cè)試機(jī)制：在 src/sympy/* 下維護(hù)一棵鏡像式的 parity/oracle 樹(shù)(諭示機(jī))，專門把 MoonBit 的實(shí)現(xiàn)結(jié)果與 sympy 參考結(jié)果進(jìn)行對(duì)照。這一層基本上綁定了 sympy 全部的外部接口。而實(shí)現(xiàn)層應(yīng)永遠(yuǎn)不依賴 sympy，只有測(cè)試層可以調(diào)用 sympy 作為參考語(yǔ)義。也就是說(shuō)，MoonBit 代碼能夠算出自己的答案，而 oracle 層會(huì)將這個(gè)答案轉(zhuǎn)換成 sympy 對(duì)象，并調(diào)用 sympy 對(duì)應(yīng)的 API 來(lái)驗(yàn)證它的正確性。或者直接將同樣的輸入 轉(zhuǎn)換為 sympy 對(duì)象并調(diào)用 sympy 函數(shù)，得到結(jié)果后與 symbit 進(jìn)行比較。

在代碼層面上， symbit/src/sym* 負(fù)責(zé)實(shí)現(xiàn)，而 symbit/src/sympy/* 則按包鏡像上游模塊，包含 *_oracle.mbt、*_port_test.mbt、port_support_test.mbt 等文件。例如 core、polys、solvers、physics 等子樹(shù)都各自維護(hù)了對(duì)應(yīng)的 oracle 層。

在比較關(guān)系 R 的設(shè)計(jì)上，正如我們之前所言，Symbit 并不假設(shè)所有對(duì)象都適合用同一種比較方式。實(shí)踐中我們主要使用了三類 parity 技巧。

第一類是直接的結(jié)構(gòu)或文本 oracle。如果一個(gè)對(duì)象的輸出形式本身就是穩(wěn)定語(yǔ)義的一部分，例如 srepr、latex 或某些調(diào)試表示，那么最直接的做法就是把 MoonBit 對(duì)象轉(zhuǎn)換成 sympy 對(duì)象，再調(diào)用 sympy 的對(duì)應(yīng) printer 取得參考輸出，并和 MoonBit 的序列化結(jié)果進(jìn)行字符串比較。例如 core_oracle 中：

pub fn core_expr_sstr(expr :@symcore.Expr) ->Stringraise {
letobj =@sympy.expr_to_sympy(expr)
 py_str_obj(
  objenum_to_obj(
   sympy_call_must("sympy.sstr", [@sympy.OracleArg::PyObj(obj)]),
  ),
 )
}

第二類是經(jīng)規(guī)范化后的表達(dá)式等價(jià)。對(duì)于許多代數(shù)結(jié)果而言，直接比較字符串會(huì)過(guò)于脆弱。例如 x - y 與 -y + x 在文本上不同，但在表達(dá)式意義下等價(jià)。這時(shí)更合適的比較關(guān)系是：

這種比較方式特別適合 simplify、factor、expand、solve 等場(chǎng)景。在求解器中，進(jìn)一步常見(jiàn)的做法是比較殘差而不是比較解的打印形式。如果一個(gè)候選解 滿足

并且其定義域條件與 sympy 一致，那么即便解集的內(nèi)部排列或局部打印形式不同，它仍然應(yīng)被視為正確結(jié)果。因此在 solver oracle 測(cè)試中，我們可以運(yùn)行最后的結(jié)果放置在無(wú)序容器中進(jìn)行比較，而不是試圖要求所有結(jié)果逐字符一致。

第三類是數(shù)值近似語(yǔ)義的 oracle。這類場(chǎng)景主要出現(xiàn)在物理、控制、繪圖或某些數(shù)值 API 中。在這些路徑里，sympy 本身也未必總返回純精確對(duì)象，而 MoonBit 側(cè)有時(shí)會(huì)經(jīng)過(guò)不同的數(shù)值后端或離散化過(guò)程。此時(shí)更合適的關(guān)系通常是

這類比較在系統(tǒng)中并不是主流，但它們提醒我們：oracle 測(cè)試的關(guān)鍵不在于「永遠(yuǎn)追求字符串一致」，而在于為每種對(duì)象語(yǔ)義選擇恰當(dāng)?shù)谋容^關(guān)系。

sympy 對(duì)象構(gòu)造

在 parity/oracle 測(cè)試?yán)?，我們盡量直接通過(guò) FFI 構(gòu)造 sympy 對(duì)象，而不是先把 MoonBit 表達(dá)式打印成字符串再交給 Python 解析。如果 oracle 建立在字符串 round-trip 之上，那么 parser、printer 與對(duì)象橋接這三類問(wèn)題就會(huì)纏在一起。此時(shí)一旦出現(xiàn)不一致，很難判斷究竟是 MoonBit 側(cè)對(duì)象語(yǔ)義錯(cuò)了，還是打印錯(cuò)了，還是 Python 側(cè)解析路徑改變了，非常不利于 debug。

因此，在 pybridge.mbt 中， Symbit 把 Expr 直接映射到 sympy 對(duì)象：

pub fn expr_to_sympy(expr :@symcore.Expr) ->@py.PyObject raise {
letdummy_cache : Map[Int,@py.PyObject] = {}
letwild_cache : Map[String,@py.PyObject] = {}
 expr_to_sympy_cached(
 @symcore.normalize_legacy_expr(expr),
  dummy_cache,
  wild_cache,
 )
}

更進(jìn)一步，Add、Mul、Pow這些對(duì)象在橋接時(shí)會(huì)顯式傳入evaluate=false，以保留結(jié)構(gòu)語(yǔ)義而不是讓 sympy 在橋接階段重新化簡(jiǎn)：

@symcore.Expr::Add(args) =>
 sympy_nary_obj("sympy.Add", args,"0", dummy_cache, wild_cache, kwargs={
 "evaluate":OracleArg::Bool(false),
 })
@symcore.Expr::Mul(args) =>
 sympy_nary_obj("sympy.Mul", args,"1", dummy_cache, wild_cache, kwargs={
 "evaluate":OracleArg::Bool(false),
 })
@symcore.Expr::Pow(base, exp) =>
 sympy_call_obj(
 "sympy.Pow",
  [OracleArg::PyObj(base_obj),OracleArg::PyObj(exp_obj)],
  kwargs={"evaluate":OracleArg::Bool(false) },
 )

因?yàn)?oracle testing 想比較的是「兩個(gè)系統(tǒng)對(duì)同一對(duì)象的理解是否一致」，而不是「MoonBit 打印出的字符串能否再次被 sympy 接受并重寫(xiě)成某種形態(tài)」。通過(guò)對(duì)象級(jí)橋接，oracle 層可以最大程度剝離 parser/printer 噪聲，把測(cè)試焦點(diǎn)放回真正的符號(hào)語(yǔ)義上。

利用 CFFI 接入 CPython 運(yùn)行時(shí)的經(jīng)驗(yàn)

要讓上述 parity/oracle 機(jī)制可用，還需要一個(gè)現(xiàn)實(shí)前提： MoonBit 必須能夠穩(wěn)定地嵌入 CPython 運(yùn)行時(shí)，并以足夠低的摩擦調(diào)用 sympy。在 Symbit 中，這部分實(shí)現(xiàn)集中在 symbit/src/sympy 這層 Python bridge。從代碼組織上看，它又可以拆成三小層：

types.mbt：定義跨邊界參數(shù)類型 OracleArg

py_pack.mbt：負(fù)責(zé)參數(shù)打包與 Python 對(duì)象構(gòu)造

py_call.mbt / pybridge.mbt：負(fù)責(zé)運(yùn)行時(shí)初始化、調(diào)用和對(duì)象級(jí)橋接

例如 types.mbt 中，所有跨邊界參數(shù)都先被封裝成一個(gè)統(tǒng)一的代數(shù)數(shù)據(jù)類型：

pub(all)enumOracleArg{
 Null
 Str(String)
 Int(Int)
 Bool(Bool)
 StrList(Array[String])
 IntList(Array[Int])
 List(Array[OracleArg])
 Dict(Map[String, OracleArg])
 PyObj(@py.PyObject)
}

有了這些方便的函數(shù)我們就不必再到處手寫(xiě)不同的 FFI 調(diào)用，而是通過(guò)一層統(tǒng)一的參數(shù)打包協(xié)議。絕大多數(shù) oracle helper 都可以在 OracleArg 這一層復(fù)用相同的參數(shù)傳遞邏輯，而不用每個(gè)包都自己拼接 Python 參數(shù)。

隨后在 py_pack.mbt 中，這些參數(shù)被打包成真實(shí)的 Python 對(duì)象：

pubfnpy_pack(arg:OracleArg)-> @py.PyObject{
matcharg{
 OracleArg::Str(s) => @py.PyString::from(s).obj()
  OracleArg::Int(n) => @py.PyInteger::from(n.to_int64()).obj()
  OracleArg::Bool(b) => @py.PyBool::from(b).obj()
  OracleArg::PyObj(obj) => {
   @cpython.py_incref(obj.obj_ref())
   obj
  }
  ...
 }
}

一個(gè)常見(jiàn)的坑時(shí)引用計(jì)數(shù)問(wèn)題，但跨邊界傳入現(xiàn)有的 PyObj 時(shí)，必須顯式 incref，否則一些的生命周期錯(cuò)誤會(huì)非常難查(它們甚至看起來(lái)是隨機(jī)發(fā)生的)。

oracle 層盡量不依賴「把字符串塞進(jìn) Python 的 eval 函數(shù)」，這對(duì)代碼可讀性、錯(cuò)誤定位和測(cè)試穩(wěn)定性都非常不利。我們僅在 core_oracle.mbt 等受限場(chǎng)景下調(diào)用 Python eval，但這類邏輯主要用于便捷地獲取參考值;而真正從 MoonBit 對(duì)象進(jìn)入 sympy 對(duì)象的主路徑，仍然是前面提到的 expr_to_sympy。這種分工可以概括為：

而不應(yīng)該是

后者雖然實(shí)現(xiàn)更快(且我們?cè)缙诖_實(shí)希望通過(guò)這個(gè)簡(jiǎn)化實(shí)現(xiàn)，但帶來(lái)的收益不如帶來(lái)的麻煩多)，但它把 parser、printer、引用環(huán)境和語(yǔ)義比較混成了一條鏈，對(duì)于遷移工程來(lái)說(shuō)噪聲過(guò)大。

最后，CFFI 接入還有一個(gè)經(jīng)驗(yàn)是：橋接層必須被視為「測(cè)試基礎(chǔ)設(shè)施」，而不是「核心實(shí)現(xiàn)的一部分」。實(shí)現(xiàn)層不能夠依賴 sympy_call(...) 這類接口來(lái)獲得最終結(jié)果，否則整個(gè)遷移項(xiàng)目就會(huì)失去意義。

評(píng)估

到目前為止，本文討論了系統(tǒng)目標(biāo)、對(duì)象架構(gòu)、一個(gè)代表性多項(xiàng)式算法以及測(cè)試與 oracle 機(jī)制。最后一個(gè)問(wèn)題自然是：這些設(shè)計(jì)在實(shí)際運(yùn)行中帶來(lái)了什么結(jié)果。對(duì)于一個(gè) CAS 實(shí)現(xiàn)而言，評(píng)估不能只給出若干「更快」的例子，因?yàn)榉?hào)系統(tǒng)的性能高度依賴負(fù)載的結(jié)構(gòu)：有些路徑主要受精確算術(shù)支配，有些受表達(dá)式重寫(xiě)支配，有些則受數(shù)據(jù)結(jié)構(gòu)構(gòu)造、項(xiàng)排序與規(guī)范化頻率支配。因此我們應(yīng)該給不同的包，挑選大部分具有代表性的 API 進(jìn)行測(cè)試，實(shí)踐中我們借助 symbench 把負(fù)載按包與 API 家族組織起來(lái)，分別給出 native 與 WebAssembly 路徑上的結(jié)果。

實(shí)際上這里還有個(gè)相當(dāng)有趣的問(wèn)題就是構(gòu)造「有趣」的數(shù)學(xué)表達(dá)式以用于測(cè)試，這并非一個(gè)顯然的問(wèn)題，我們使用了很多 property based testing 中的生成器設(shè)計(jì)方法來(lái)完成此事，對(duì)此感興趣的讀者可以見(jiàn)我們之前發(fā)表的關(guān)于 QuickCheck 的文章。

評(píng)估方法

Symbit 的 benchmark 系統(tǒng)建立在 symbench 之上。每個(gè) benchmark case 都包含三部分：MoonBit 側(cè)輸入構(gòu)造器、sympy 側(cè) oracle 定義，以及統(tǒng)一的運(yùn)行入口。在進(jìn)入計(jì)時(shí)之前，所有 case 都必須先通過(guò)語(yǔ)義校驗(yàn)，也就是先確認(rèn)

再把同一 workload 交給基準(zhǔn)腳本計(jì)時(shí)。無(wú)論何時(shí)我們都應(yīng)該先驗(yàn)證語(yǔ)義正確性，再比較性能，畢竟更快地得到錯(cuò)誤結(jié)果并沒(méi)有什么意義。

考慮到 Python 具有啟動(dòng)成本，benchmark 為盡可能聚焦算法內(nèi)核本身的運(yùn)行代價(jià)，應(yīng)該啟動(dòng)之后多次重復(fù)執(zhí)行同一樣例來(lái)攤薄啟動(dòng)成本。至于 Symbit 則使用 native-binary + release 路徑，在這一定義下，本文采用如下速度比：

若該值大于 ，則表示 Symbit 更快。本文收集了幾種常見(jiàn)這些報(bào)表按負(fù)載家族分別整理，例如 sympolys-all、symsolvers-all、symseries-all 等，基本上也能對(duì)應(yīng)到 symbit / sympy 的包結(jié)構(gòu)。

基準(zhǔn)測(cè)試結(jié)果

Native 路徑上的結(jié)果相當(dāng)不錯(cuò)，在當(dāng)前已經(jīng)整理成穩(wěn)定分包報(bào)表的 workload 上，Symbit 在多數(shù)包內(nèi)都取得了穩(wěn)定領(lǐng)先，且這種領(lǐng)先并不局限于某一種類型的算法。在多項(xiàng)式、求解器、整數(shù)論、級(jí)數(shù)、集合運(yùn)算、積分以及部分組合函數(shù) workload，都表現(xiàn)出了明顯的優(yōu)勢(shì)。

下表匯總了若干當(dāng)前已經(jīng)穩(wěn)定維護(hù)的分包報(bào)表。其中「范圍」表示該包內(nèi)最慢與最快樣例的加速比區(qū)間，而「代表 case」則列出若干最能體現(xiàn)該類 workload 特征的樣例。

下圖給出了 symseries 分包報(bào)表中的加速比分布，可以直觀看到不同多項(xiàng)式工作負(fù)載之間的差異。其中橫軸是具體 benchmark 樣例，縱軸是相對(duì)于 sympy 的加速比。

可見(jiàn)不同的負(fù)載均得到了提升，而不是某一個(gè)特例。更多結(jié)果表明，在 sympolys 中，gcd、resultant、discriminant、sturm sequence、Groebner basis 與有理插值都明顯快于 sympy;在 symsolvers 中，線性方程組、非線性方程組、solveset 與線性規(guī)劃也都表現(xiàn)出穩(wěn)定優(yōu)勢(shì)。這說(shuō)明速度提升并不是來(lái)自某一個(gè)特殊路徑，而是來(lái)自對(duì)象表示、規(guī)范化、精確域算術(shù)與底層算法組織方式的共同變化。在結(jié)構(gòu)更復(fù)雜、對(duì)象層成本更突出的 case 上，提升還會(huì)繼續(xù)擴(kuò)大。當(dāng)然，在一些已經(jīng)相對(duì)緊湊的組合或微積分核上，結(jié)果也可能只領(lǐng)先 1.x 到 3.x。我們也對(duì) WebAssembly 平臺(tái)進(jìn)行了測(cè)試(對(duì)不 sympy 本地解釋)，也有 1.x ~ 3.x 的整體提升，不過(guò)幅度并未有 native 這么大，它更大的優(yōu)勢(shì)是瀏覽器部署，并且輸出小巧。

結(jié)果解讀與局限

這些評(píng)估結(jié)果支持了本文的基本判斷：把 sympy 風(fēng)格的符號(hào)對(duì)象系統(tǒng)遷移到 MoonBit，并改變對(duì)象表示、規(guī)范化鏈路與底層精確算術(shù)的執(zhí)行特性，確實(shí)帶來(lái)了可觀的性能提升。在一批經(jīng)過(guò) oracle 校驗(yàn)的代表性負(fù)載上，這種變化最終表現(xiàn)為穩(wěn)定的 native 優(yōu)勢(shì)，以及仍具競(jìng)爭(zhēng)力的 WebAssembly 路徑。

但與此同時(shí)，本文并不將這些數(shù)字解釋為「所有符號(hào)負(fù)載都會(huì)自動(dòng)得到同等提升」。首先，當(dāng)前報(bào)表雖然已經(jīng)覆蓋了多項(xiàng)式、求解器、整數(shù)論、積分、集合、級(jí)數(shù)、函數(shù)與部分微積分，但它們?nèi)匀皇墙?jīng)過(guò)篩選和構(gòu)造的 kernel family，而不是完整地覆蓋整個(gè) sympy API 空間。其次，benchmark 結(jié)果本身也是系統(tǒng)演化過(guò)程的一部分。某些樣例在項(xiàng)目早期曾經(jīng)顯著落后，后來(lái)通過(guò)對(duì)齊 sympy 代碼路徑、調(diào)整對(duì)象表示或改進(jìn) exact kernel 而被拉回;這意味著評(píng)估系統(tǒng)同時(shí)也是性能診斷系統(tǒng)，而不僅是展示系統(tǒng)。若要把它推廣為一個(gè)更完整的學(xué)術(shù)評(píng)估，還需要在未來(lái)補(bǔ)充更多內(nèi)容：例如更系統(tǒng)的 workload 分類、更大規(guī)模的隨機(jī)與性質(zhì)測(cè)試集、更細(xì)粒度的 profiler 分析，以及跨版本的 longitudinal benchmark。

綜合來(lái)看，Symbit 的評(píng)估結(jié)果并不是「證明一切都已經(jīng)完成」，而是表明這條技術(shù)路線是成立的：一個(gè)保持 sympy 風(fēng)格語(yǔ)義與精確計(jì)算能力的符號(hào)系統(tǒng)，確實(shí)可以在編譯型語(yǔ)言中獲得顯著的內(nèi)核運(yùn)行收益，并同時(shí)保留進(jìn)入瀏覽器環(huán)境的現(xiàn)實(shí)可行性。

瀏覽器 Demo

本項(xiàng)目還利用 MoonBit 的多后端能力打造了一個(gè) Symbit Web-Demo，名為 symweb：https://caimeo.space/symweb

我們將計(jì)算內(nèi)核編譯到 WASM 加速，而前端 GUI 部分則使用 Rabbita 編譯到 JavaScript。兩者之間通過(guò)一層很薄的 JSON bridge 通訊。另外借助 KaTeX 來(lái)渲染 LaTeX 輸出，整個(gè)系統(tǒng)在瀏覽器端形成了一個(gè)小型的 CAS 交互界面。 sympy 的經(jīng)典用法往往需要安裝 Python 環(huán)境、配置依賴、編寫(xiě)腳本或 notebook，而我們通過(guò) Symweb 把這些交互直接搬到了瀏覽器里，輕量用戶可以直接在頁(yè)面里編輯表達(dá)式、切換 parser 選項(xiàng)、觀察結(jié)構(gòu)化結(jié)果，并即時(shí)得到反饋。我們?cè)?Demo 里面實(shí)現(xiàn)了大部分常用的 symbolic API，例如 simplify、expand、factor、solve、series 等，并且在一些頁(yè)面里還展示了表達(dá)式的結(jié)構(gòu)化表示、LaTeX 輸出以及求值結(jié)果等多層信息。并且頁(yè)面相當(dāng)小，整個(gè)前端代碼和內(nèi)核編譯之后不到 3 MB，相比之下若我們想要把 sympy 運(yùn)行在瀏覽器上，需要打包 Pyodide 運(yùn)行時(shí)、自己?jiǎn)为?dú)寫(xiě)膠水代碼和 std 支持，然后加載 sympy 和 mpmath 本體，肯定不會(huì)這么簡(jiǎn)潔 (運(yùn)行性能更不用說(shuō)了)。

Symbit Playground - caimeo.space/symweb

當(dāng)然，symweb 仍然只是一個(gè) demo，而不是完整的 notebook 或 CAS IDE。它目前更適合展示一個(gè)函數(shù)如何解析輸入、如何形成結(jié)構(gòu)化結(jié)果、以及在當(dāng)前 kernel 中給出什么輸出，而不是承擔(dān)長(zhǎng)會(huì)話、多文檔、任意插件或大規(guī)?？梢暬雀氐娜蝿?wù)。對(duì)于這種復(fù)雜任務(wù)，我們建議直接本地安裝 Symbit 體驗(yàn)。

未來(lái)工作

雖然我們已經(jīng)取得了許多進(jìn)展，但未來(lái)仍有很多工作需要完成。除了繼續(xù)部分關(guān)鍵包的語(yǔ)義，減少與 Sympy 在語(yǔ)義上的差距。并逐步推進(jìn)一些更復(fù)雜的算法實(shí)現(xiàn)和 Bug 修復(fù)：即使是 Sympy 本身也有數(shù)千個(gè) issues 待修復(fù)和 PR 等待合并，我們希望 Symbit 能一定程度上跟隨這些變化和改進(jìn)，甚至走在前面。

結(jié)論

本文致此完結(jié)，我們討論了 Sympy 風(fēng)格的符號(hào)表達(dá)、精確計(jì)算與常見(jiàn) CAS 算法，并不必然依賴 Python 這一宿主環(huán)境。通過(guò) MoonBit 這樣的編譯型多后端語(yǔ)言，可以把同樣的語(yǔ)義重建為一個(gè)能夠同時(shí)面向 native 與 WebAssembly 的符號(hào)計(jì)算內(nèi)核;在這一過(guò)程中，表達(dá)式表示、規(guī)范化、精確數(shù)值、多項(xiàng)式與矩陣算法、測(cè)試基礎(chǔ)設(shè)施與部署方式都會(huì)被重新組織。當(dāng)前結(jié)果表明，這條路線不僅在工程上可行，而且在若干典型 workload 上已經(jīng)能夠提供穩(wěn)定的性能收益，并形成一個(gè)真實(shí)可交互的瀏覽器前端。這并不意味著 Symbit 已經(jīng)完成，但至少說(shuō)明：構(gòu)建一個(gè)編譯型、可部署、且保持精確語(yǔ)義的現(xiàn)代 CAS 內(nèi)核，是一條成立且值得繼續(xù)推進(jìn)的方向。

若讀者覺(jué)得這個(gè)項(xiàng)目有趣，歡迎訪問(wèn) https://github.com/CAIMEOX/symbit.git 以了解更多細(xì)節(jié)。