數學——符號推演的藝術

數學——符號推演的藝術

數學離不開各式各樣的符號. 數字如2, 0, 1, 8, 運算符如+, -, ×,÷,等號=, 不等號≠都是最常見的數學符號. 其他語義複雜一些的數學符號有π, √, sin, ∈, ∃, ⊥, ∂ 等等. 這些有趣的符號可以用來表示各種具體或者抽象的數學概念, 包括數學對象以及數學對象之間的相互關係, 而數學活動的主要內容正是研究、處理數學對象和數學對象之間的數量和邏輯關聯. 例如, 2+0÷1-8, eπi+1=0, x2+y2>r2, m||l 等, 它們都是典型的數學符號表達式. 數學從計數開始, 通過引進五花八門的符號系統, 建立內涵豐厚的分支體系, 逐漸發展成為描述、論證自然科學規律和現象的基礎語言.

數學分支和學科的形成遵循基本的發展規律: 首先選取一些原始的數學概念, 包括對象和度量以及它們之間的數量和邏輯關係. 這些原始概念大多是現實世界中各種事物的數學抽象, 它們沒有嚴密的數學定義. 譬如, 數論中的1、幾何學中的“點”和代數學中的“變元”都可以視為原始的數學概念, 對其我們很難給出嚴密的定義. 有了原始的數學概念, 我們再假定它們之間滿足某些不證自明的數量和邏輯關係, 也就是假定某些公理成立. 基於假定的公理, 我們可以利用形式演算和邏輯推理規則嚴格地證明、導出新的數量和邏輯關係, 即性質和定理. 有了原始和導出關係, 我們又可以引進導出概念, 再嚴格證明、導出更新的數量和邏輯關係, 如此類推. 在這個知識遞歸積累的過程中, 人們需要引進各種符號, 用來表示原始的和導出的數學概念. 數學研究的中心內容就是處理數學符號和符號關係式, 解決有關它們的演算、證明和推理問題.

數學研究離不開符號演算、離不開形式推理. 數學符號和符號之間的關係形式多樣、語義複雜, 有關它們的推理演算離不開工具: 過去和現在離不開稿紙、離不開黑板, 將來必然會離不開計算設備. 符號計算隨著計算機的出現應運而生並快速發展, 成為深度融合數學與計算機科學的交叉學科, 重點研究、探索數學也即符號數學演算和推理的算法化、機械化、自動化, 設計並實施適合在計算設備上運行的高效算法、軟件平臺和應用模塊. 符號數學推演既是基本的又是高級的智力勞動. 實現這種勞動的算法化和機械化是一項非常艱鉅的工作, 需要數代科學家和研究人員為之長期努力, 也需要社會各界的大力支持. 計算機科學與技術的發展已為數學的機械化提供了必要的理論基礎和應用設施, 但數學機械化的基本實現依然任重道遠, 創新求索的過程必然會艱難複雜. 如何有效推進符號數學推演的算法研究和軟件開發, 實現高級智力勞動的機械化、自動化, 讓數學作為自然科學的基礎語言和工具為科技文化教育的信息化建設與發展發揮更大作用, 這是時代賦予我們前所未有的挑戰和機遇, 我們必須積極應對.

現代符號計算的發展始於上世紀60年代初期, 當時美國的幾個科研小組幾乎同時開啟了符號計算軟件的研發. 麻省理工學院的J. R. Slagle設計實施了符號自動積分軟件SAINT, IBM 公司的J. E. Sammet研發了處理初等函數表達式的軟件系統FORMAC, 在斯坦福直線加速器中心訪問的M. J. G. Veltman研發了用於粒子物理計算的程序包SCHOONSCHIP, 貝爾實驗室的W. S. Brown研發了符號代數系統ALPAK和編程語言ALTRAN. 稍後, 斯坦福大學的A. C. Hearn 研發了主要用於物理計算的流行軟件系統REDUCE, 威斯康星大學的G. E. Collins將先前在IBM公司開發的多項式處理程序包PM升級為SAC-1 (後續版本: SAC-2, SAC/ALDES, SACLIB), 英國劍橋大學的J. Fitch等人研發了用於天體力學和相對論計算的劍橋代數系統CAMAL 等. 這些早期系統的實現大多基於程序設計語言LISP. 到了70 年代, 符號計算軟件的研發更是持續不斷: IBM公司成功研發了帶有嵌入知識的強類型代數計算系統SCRATCHPAD (後續版本: SCRATCHPAD II, AXIOM), 麻省理工學院研發了著名的符號與代數計算系統MACSYMA (MAXIMA), 而REDUCE系統的研發則從斯坦福大學轉移至猶他大學. 符號計算軟件研發的前20年基本上可以看作是之後開發成熟軟件系統的預研期. 這個時期的實踐表明, 符號計算軟件系統的有效實施不僅需要面對數據結構、表達式膨脹、垃圾清理和存儲管理等眾多計算機科學方面的問題, 而且還要求用於符號與代數計算的算法高效實用, 因而極大地推動了符號計算的算法研究, 包括算法的設計與優化、算法的理論複雜度分析和算法的實際計算效率分析. 許多有關多項式運算、代數化簡、符號積分的基礎性算法都是在那段時間發展成熟的. 與此同時, 新一代符號計算軟件系統的研發拉開了序幕, 支撐符號計算未來發展和應用的核心算法被深入研究並普遍受到重視, 基於符號推演的計算交換代數、計算微分代數、計算代數幾何和計算實幾何等新興學科開始形成. 它們為符號計算這門交叉學科朝著縱深的方向發展注入了強勁的動力.

上世紀80年代初期, B. Buchberger的GrÖbner基方法和吳文俊的特徵列方法在符號計算領域受到高度關注, 進而廣為人知. 學者們從不同的層面對這兩種方法展開了深入研究. 緊隨其後, 由G. E. Collins提出的基於柱形代數分解的量詞消去方法也得到了很大改進. 這三種方法可以用來有效處理多項式系統、多項式理想、半代數系統及其定義的各種代數與幾何對象, 系統研究其性質與表示以及它們之間的相互關係, 因此有著非常廣泛的理論和實際應用. 圍繞這三種方法, 符號計算領域的研究呈現出勃勃生機, 很多基本而棘手的數學問題如代數方程求解和幾何定理求證都可以通過這些方法來機械地、自動地或者交互式地獲得解答. 由此衍生的各種基礎和應用研究也豐富了符號計算的內涵, 推動了符號計算這門學科的全面發展, 加速了符號計算軟件的研發進程.

從80年代中期開始, 以MAPLE和MATHEMATICA為代表的新一代科學計算通用軟件在全球發佈, 並實行商業化運營; 數十種其他通用或專用軟件系統如DERIVE, MuPAD, MAGMA, MACAULAY 2, SINGULAR, CoCoA, Risa/Asir, SageMath 等也相繼推出. 這些系統具有強大的符號計算、數值計算和圖形計算功能. 近30年來, 符號計算軟件的研發團隊始終關注算法研究的最新進展, 他們緊跟信息科學與技術的發展, 將科學研究的成果及時快捷地植入軟件產品, 行之有效地推動了產學研的良性互動與深度融合.

我國學者為符號計算的發展做出了傑出貢獻. 以著名數學家吳文俊先生為代表的中國學派長期致力於數學算法化、機械化的研究和發展, 成就斐然, 在國際學術界有很高的地位和廣泛的影響. 吳先生提出的證明幾何定理和計算多項式組與微分多項式組的特徵列與零點分解的方法是自動推理和符號計算領域的核心方法, 也是數學機械化方法的典範. 吳方法和吳先生的數學機械化思想激發了國內外學者的大量後續工作, 其中由國內學者引領發展的理論和方法涉及多項式系統、微分多項式系統和差分多項式系統的算法化消元與三角化分解, 數學定理的機器證明與發現, 半代數系統的實解隔離與實解分類, GrÖbner 基的計算與基於GrÖbner 基的特徵分解, 曲線曲面的隱式化與拼接, 代數、幾何與組合計算, 符號與數值混合計算, 多項式、微分多項式與差分多項式的基本運算等. 我國學者在與之有關的國際學術活動中也表現出色: 數十人次先後擔任國際學術期刊《符號計算雜誌》(JSC) 的編委、《計算機科學中的數學》(MCS) 的創刊主編和編委, 符號與代數計算國際研討會(ISSAC)、 自動推理國際會議(CADE)、 人工智能與符號計算國際會議(AISC)、 數學軟件國際會議(ICMS)等系列學術會議的大會或者程序委員會主席, ACM 符號與代數計算專業委員會(SIGSAM) 主任以及ISSAC 指導委員會主任等職; 多次在這些學術會議上作特邀報告, 並且是ASCM, ADG, MACIS等多個國際學術會議系列的創辦人. 我國符號計算領域的學者在國際學術界的可見度和影響力還在繼續上升.

沒有符號, 就沒有數學! 沒有符號計算, 就沒有數學機械化!


分享到:


相關文章: