數學軟體——計算機上的數學

著名數學家吳文俊先生曾預言：「在不久的將來，電子計算機之於數學家，勢將如顯微鏡之於生物學家，望遠鏡之於天文學家那樣不可或缺。」如今這個預言已成為現實，計算機的應用已深入到自然科學的各個領域。對於以計算和推理為主要任務的數學，計算機的作用尤為明顯。

要使計算機能夠用來處理和解決數學問題，我們必須有指導計算機硬體設備執行運算的特殊數據和指令。這樣的數據和指令集就是數學軟體。數學軟體中的數據和指令是為處理數學對象，進行數學計算、推理、繪圖、文本製作等任務而編製的計算機程序，這裡數學對象有數值、符號、圖形等多種類型。由於數學任務種類繁多，數學軟體也形式各異。我們試從三個方面對數學軟體作簡單介紹。

數學對象的表示

為了簡明地表示數學概念及其邏輯結構，數學家引進了很多特殊的數學符號，如根號、求和號、積分號，並約定了相應的表達方式和結構，如上下標、分式等。這些符號和表達結構使數學表達式具有不同於普通文字線性排列的二維結構。因此，數學內容要在計算機上存儲和呈現，就必須按照特定格式或語言對其進行編碼。最廣泛使用的編碼格式當屬著名計算機科學家Donald E. Knuth發明的，它通過一系列基本的文本命令將複雜的數學公式線性化，並允許利用這些命令定義更複雜的高級命令，從而得到更易於用戶使用的編碼格式。譬如，美國計算機科學家Leslie Lamport在二十世紀八十年代初期就設計開發了後來廣泛使用的及其優化版本。利用及改進的排版系統可以對和命令進行編譯並生成高質量的dvi、pdf、ps等格式的可顯示文件，列印輸出。為了使數學表達式能通過互聯網傳播和處理，萬維網聯盟W3C的數學工作組於1998年制定並發布了MathML標記語言，作為通過互聯網交流數學符號和公式的標準規範。目前MathML已發展到第三代，與前二代相比，其表達能力更強、範圍更廣，並得到了Mozilla Firefox、Camino等瀏覽器的支持。以MathML編碼的數學公式能夠在網頁中以可讀的形式呈現，而Safari、Chrome、Opera、Internet Explorer等瀏覽器都曾經支持過MathML編碼的網頁，但出於安全和穩定性的考慮，目前已不再支持。又為了使數學內容與所有瀏覽器都兼容，MathJax聯盟開發了一款JavaScript程序，可以將MathML和編碼的數學表達式動態地轉化為HTML或者SVG格式，再通過CSS樣式表呈現出來。除了以上側重於數學表達式呈現結構的編碼格式之外，還有一類針對數學表達式語義的編碼語言，如OpenMath標記語言，它通過Content Dictionaries（CD）指明數學符號的語義，從而使數學表達式可以在不同數學軟體系統之間交互、共享和使用。例如，定積分表達式

用編碼為$int_0^1 e^x dx$，而使用MathML和OpenMath編碼則如下圖所示。

圖1 定積分表達式的MathML表示（左）和OpenMath表示（右）

另一方面，要利用計算機程序對數學對象進行計算和推理，還需要針對其特徵設計合適的數據結構。例如，32位計算機能夠處理的最大整數（無符號）是-1，更大的整數如何在計算機上表示是開發數學計算軟體所要解決的基本問題。事實上，假設B是一個大於1的整數，那麼任何一個正整數a在B進位下都可以唯一地表示為

式中表示a在B進位下的每一位。為了表示大整數，首先可以將B取得很大，比如可以令B-1為計算機所能表示的最大整數，然後用一個序列（如數組）來存這n+1個整數，這個序列的長度也可以很大，比如可以令n+1為計算機所能表示的最大整數，通過這種方式表示的正整數a就可以任意大。在現有的計算機代數系統中，考慮到效率和實用性，B通常不必設得很大就能夠滿足應用需求。依據這種數據結構還可以在計算機上表示諸如多項式等具有級數特徵的代數對象，通過設計相應的演算法便能實現代數運算。

數學計算與推理

數學計算可以分為兩種：數值計算和符號計算。前者是指帶有（截斷）誤差的浮點數之間的運算，如果運算步驟很多就會造成累計誤差很大，因此數值計算的演算法通常需要考慮穩定性，即輸入數據的微小擾動是否會引起輸出的大幅波動，還需要考慮演算法是否收斂以及收斂的速度如何等問題；後者是指具有數學含義的抽象符號之間的精確運算，例如分式化簡，函數的級數展開、求導、求積，符號方程求解，曲線曲面求交等，這些符號除了包括整數、數學常數、多項式等代數對象以外，還包括幾何對象、圖形、文本等。由於符號之間的邏輯關係可以很複雜，因此符號計算的演算法通常需要考慮如何設計優化的數據結構和模型來降低運算的空間與時間複雜度。數學計算軟體通常由用於解決問題的程序庫和功能模塊組成，種類繁多，但各有側重。例如，側重數值計算、分析和建模的Matlab（商業軟體）、Scilab（開源自由軟體）；側重符號計算、推導和化簡的Maple（商業軟體）、Mathematica（商業軟體）。另外還有側重於專門領域的軟體，如SAS（商業軟體）、R（開源自由軟體）等統計分析軟體；Gams（商業軟體）、Lingo（商業軟體）等運籌優化軟體；CGAL（開源自由軟體）等離散幾何計算軟體。

圖2數學計算軟體

數學推理是指從給定的一組被賦予數學含義的抽象符號關係式（即前提）出發，依據邏輯推理規則（如三段論）對這些符號關係式進行一系列替換和重排，得到另外一組具有數學含義的抽象符號關係式（即結論）的過程。由於整個過程只是對某些抽象符號進行形式上的操作和處理，因此數學推理在某種意義上也可以看作是一種特殊的符號計算。數學推理的演算法主要考慮如何設計具有嚴格語法規則的符號系統（即形式化語言，如一階謂詞邏輯語言）來承載數學語義，以及在此基礎上通過怎樣的推理規則和搜索策略實現從前提到結論的符號演變（這個演變過程即為證明，被證明過的結論即為定理）。數學推理軟體主要分為兩類：自動推理軟體和互動式證明助手。

（1）自動推理軟體是指推理過程能夠自動完成的軟體，有時也稱作自動定理證明器。這類軟體主要包括E、Otter、Vampire、SPASS等支持一階謂詞邏輯語言的通用證明器和適用於具體領域的專用證明器。在使用通用自動定理證明器進行數學推理時，需要將所涉及的全部數學公理（即不證自明的命題）都形式地表示成邏輯公式作為前提，才有可能保證自動推理的順利進行。然而實際上，這並不容易實現，因為人們在進行數學推理時會默認地應用一些常識性結論，而這些結論對證明至關重要。例如，Euclid《幾何原本》所列出的五條公設和五條公理其實並不完整，必須利用圖形的直觀作為推理的額外依據才能夠得到書中的某些結論。為了填補這個缺陷，DavidHilbert在《幾何基礎》一書中提出了一個更加嚴密而完整的平面幾何公理系統。又為了彌補通用自動定理證明器在數學推理上的不足，Theorema系統將數學知識庫與自動定理證明器結合起來，使之不僅擁有一個通用的高階謂詞邏輯證明器，還有一系列領域相關的專用證明器，讓數學推理變得更加友好、高效。除此之外，Mizar系統能夠自動驗證以Mizar語言編寫的數學文檔的邏輯推理正確性，並由此構建了一個包含千餘篇形式化文檔的數學知識庫。

在數學的眾多分支中，幾何學是自動推理髮展最為成功的領域之一，這主要歸功於以吳文俊先生為代表的一批中國學者的開創性工作。幾何定理自動證明器數量眾多，並以不同的方法實現了幾何學自動推理。例如，JGEX和超級畫板實現了面積法（將一組與面積大小有關的恆等式作為公理）、全形法（將一組與角度大小有關的恆等式作為公理）、資料庫演繹法（通過雙向推理自動獲得給定圖形所蘊含的所有定理）等幾何不變數方法，能夠自動生成簡潔漂亮的可讀證明；GEOTHER實現了吳方法（將幾何定理證明問題轉化為關於坐標變元的多項式方程組零點包含關係的判定問題）、Gr?bner基方法（將幾何定理證明問題轉化為關於坐標變元的多項式理想和根理想的成員判定問題）等代數方法；Cinderella實現了括弧代數法；GeoGebra實現了實例檢測法。

（2）互動式證明助手是指推理過程需要人機交互協作完成的軟體。這類軟體主要有Coq和Isabelle/HOL等，能夠在保證推理正確的前提下，幫助用戶構造形式化的證明，並可以從構造過程中自動生成可信的計算程序。正是由於所構造的證明具有高可信度，證明助手已被廣泛應用於航空航天、武器裝備、醫療設備、交通、核能、金融等安全攸關軟體系統的可靠性驗證。儘管人們利用證明助手構建了一些初等數學理論的形式化知識庫（包含公理、定義、定理、證明等），也構造出如四色定理等數學難題的形式化證明，然而在實際應用中，證明助手還沒有被數學家廣泛使用。主要原因有兩方面：一方面是構造形式化證明的成本太高，除了要學習具有精確語法的形式化語言來編碼數學知識，還要保證每步推理都必須嚴格有據，這就使得證明必須從相關的所有原始公理（或被證明過的定理）出發一步一步地有序進行，有時不恰當的策略會導致證明無路可走，甚至會出現循環證明的情況；另一方面是推理工具的自動化程度不高，形式化的證明與程序代碼沒有本質區別，晦澀而繁雜，在構造證明的過程中會頻繁使用已經證明過的定理，目前並沒有高效的定理搜索和策略推薦等自動化工具來輔助指導證明的構造。因此，互動式證明助手目前在數學上的應用還處於初級階段，但隨著形式化數學知識的不斷累積，以及能夠有效管理知識的自動化工具的出現，互動式證明助手終將成為數學家的好幫手。

人機交互界面

數學軟體一般都提供可通過滑鼠、鍵盤或觸控等方式進行操作的人機交互界面，主要包括以下三類。

（1）文本編輯：通過鍵盤輸入數學符號、圖形、圖表等編碼後的文本，經過編譯和運行後得到的結果直接返回到當前界面中，如WinEdt GUI、Maple Worksheet、Mathematica Notebook。

（2）按鈕點擊：通過滑鼠點擊按鈕得到相應數學符號的編碼文本（如、MathML），一般還會以所見即所得（WYSIWYG）的方式將數學符號呈現出來，如MathType、iMathEQ、MathMagic等數學公式編輯器以及LyX、Mathcha等數學文檔編輯器。

（3）手寫識別：通過滑鼠、觸控筆或手指在軟體界面上書寫數學表達式，經過專門的程序識別得到相應的數學編碼，如MathBrush、E-chalk、MathPad。

大部分數學計算軟體都具有圖形圖像繪製、函數動態模擬等可視化功能，並可以進行交互處理，使抽象的數學內容以直觀生動的方式呈現出來。還有一類如GeoGebra、Cinderella、JGEX、超級畫板等與幾何作圖有關的軟體，稱為動態幾何軟體。利用這些軟體所提供的作圖指令，用戶可以使用滑鼠或者觸控筆在軟體界面上精確地繪製出滿足給定約束關係（如平行、垂直）的幾何圖形，當拖動圖形中的某些對象時，整個圖形將被實時地重新繪製並依然保持給定的約束關係。動態幾何軟體的動態化和精確性能夠直觀地展示圖形所蘊含的幾何關係特徵，並且一般還具有函數、幾何、代數、微積分等計算功能，因此被廣泛應用於教育教學與科學研究。另外還有一類由演算法函數庫構成的工具包（如LIBM、PETSc /TAO），它們沒有人機交互界面，需要通過其提供的應用程序介面（API）供其他程序或軟體調用。

圖3動態幾何軟體

數學軟體遠不只本文所列出的這一小部分。隨著移動互聯和雲計算時代的到來，數學軟體正朝著模塊化、並行化和群智化的趨勢發展，並且互操作的需求正在顯現。在不久的將來，數學軟體會更加深刻地影響和改變科學研究的方式和工程應用的效率。

（本文經王東明教授審閱）

喜歡這篇文章嗎？立刻分享出去讓更多人知道吧！