|
文章来源 科学网王东明的博客 2018-1-28 23:26
在不久的将来，电子计算机之于数学家，势将如显微镜之于生 物学家，望远镜之于天文学家那样不可或缺。 ——吴文俊 要使计算机能够处理和解决数学问题，需要有指导计算机硬件设备执行运算的特殊数据和指令。这样的数据和指令集就是数学软件，也就是处理数学对象（包括数学计算、推理、绘图、文本制作等）的计算机程序。这里数学对象有数值、符号、图形等多种类型。由于数学任务种类繁多，数学软件也形式各异。 数学对象的表示 为了简明地表示数学概念及其逻辑结构，数学家引进了很多特殊的数学符号，如积分号、求和号、根号，并约定了相应的表达方式和结构，如上下标、分式等。这些符号和表达结构使数学表达式具有不同于普通文字线性排列的二维结构。数学内容要在计算机上存储和呈现，就必须按照特定格式或语言对其进行编码。最广泛使用的编码格式当属著名计算机科学家Donald E. Knuth发明的 为了使数学表达式能通过互联网传播和处理，万维网联盟W3C的数学工作组于1998年制定并发布了MathML标记语言，作为通过互联网交流数学符号和公式的标准规范。目前MathML已发展到第三代，与前二代相比，其表达能力更强、范围更广，并得到了Mozilla Firefox、Camino等浏览器的支持。以MathML编码的数学公式能够在网页中以可读的形式呈现，而Safari、Chrome、Opera、InternetExplorer等浏览器都曾经支持过MathML编码的网页，但出于安全和稳定性的考虑，目前已不再支持。又为了使数学内容与所有浏览器都兼容，MathJax联盟开发了一款JavaScript程序，可以将MathML和 另一方面，要利用计算机程序对数学对象进行计算和推理，还需要针对其特征设计合适的数据结构。例如，32位计算机能够处理的最大整数（无符号）是232-1，更大的整数如何在计算机上表示是开发数学计算软件所要解决的基本问题。事实上，假设B是一个大于1的整数，那么任何一个正整数a在B进制下都可以唯一地表示为 式中 在现有的计算机代数系统中，考虑到效率和实用性，B通常并不需要设得很大就能够满足应用需求。同时，这种数据结构还可以在计算机上表示诸具有级数特征的代数对象，通过设计相应的算法便能实现代数运算。 数学计算与推理 计算机中的数学计算分为两种：数值计算和符号计算。 前者是指带有（截断）误差的浮点数之间的运算，如果运算步骤很多就会造成累计误差很大，因此数值计算的算法通常需要考虑稳定性，即输入数据的微小扰动是否会引起输出的大幅波动，还需要考虑算法是否收敛以及收敛的速度如何等问题。 后者是指具有数学含义的抽象符号之间的精确运算，例如分式化简，函数的级数展开、求导、求积，符号方程求解，曲线曲面求交等，这些符号除了包括整数、数学常数、多项式等代数对象以外，还包括几何对象、图形、文本等。由于符号之间的逻辑关系可以很复杂，因此符号计算的算法通常需要考虑如何设计优化的数据结构和模型来降低运算的空间与时间复杂度。 数学计算软件通常由用于解决问题的程序库和功能模块组成，种类繁多，各有侧重。例如，侧重数值计算、分析和建模的Matlab（商业软件）、Scilab（开源自由软件）；侧重符号计算、推导和化简的Maple（商业软件）、Mathematica（商业软件）。另外还有侧重于专门领域的软件，如SAS（商业软件）、R（开源自由软件）等统计分析软件；Gams（商业软件）、Lingo（商业软件）等运筹优化软件；CGAL（开源自由软件）等离散几何计算软件。 数学推理是指从给定的一组被赋予数学含义的抽象符号关系式（即前提）出发，依据逻辑推理规则（如三段论）对这些符号关系式进行一系列替换和重排，得到另外一组具有数学含义的抽象符号关系式（即结论）的过程。由于整个过程只是对某些抽象符号进行形式上的操作和处理，因此数学推理在某种意义上也可以看作是一种特殊的符号计算。 数学推理的算法主要考虑如何设计具有严格语法规则的符号系统（即形式化语言，如一阶谓词逻辑语言）来承载数学语义，以及在此基础上通过怎样的推理规则和搜索策略实现从前提到结论的符号演变（这个演变过程即为证明，被证明过的结论即为定理）。数学推理软件主要分为两类：自动推理软件和交互式证明助手。 1）.自动推理软件是指推理过程能够自动完成的软件，有时也称作自动定理证明器。这类软件主要包括E、Otter、Vampire、SPASS等支持一阶谓词逻辑语言的通用证明器和适用于具体领域的专用证明器。在使用通用自动定理证明器进行数学推理时，需要将所涉及的全部数学公理（即不证自明的命题）都形式地表示成逻辑公式作为前提，才有可能保证自动推理的顺利进行。 然而，实际上这并不容易实现，因为人们在进行数学推理时会默认地应用一些常识性结论，而这些结论对证明至关重要。例如，Euclid《几何原本》所列出的五条公设和五条公理其实并不完整，必须利用图形的直观作为推理的额外依据才能够得到书中的某些结论。为了填补这个缺陷，David Hilbert在《几何基础》一书中提出了一个更加严密而完整的平面几何公理系统。又为了弥补通用自动定理证明器在数学推理上的不足，Theorema系统将数学知识库与自动定理证明器结合起来，使之不仅拥有一个通用的高阶谓词逻辑证明器，还有一系列领域相关的专用证明器，让数学推理变得更加友好、高效。除此之外，Mizar系统能够自动验证以Mizar语言编写的数学文档的逻辑推理正确性，并由此构建了一个包含千余篇形式化文档的数学知识库。 在数学的众多分支中，几何学是自动推理发展最为成功的领域之一，这主要归功于以吴文俊先生为代表的一批中国学者的开创性工作。几何定理自动证明器数量众多，并以不同的方法实现了几何学自动推理。例如，JGEX和超级画板实现了面积法（将一组与面积大小有关的恒等式作为公理）、全角法（将一组与角度大小有关的恒等式作为公理）、数据库演绎法（通过双向推理自动获得给定图形所蕴含的所有定理）等几何不变量方法，能够自动生成简洁漂亮的可读证明；GEOTHER实现了吴方法（将几何定理证明问题转化为关于坐标变元的多项式方程组零点包含关系的判定问题）、Gröbner基方法（将几何定理证明问题转化为关于坐标变元的多项式理想和根理想的成员判定问题）等代数方法；Cinderella实现了括号代数法；GeoGebra实现了实例检测法。 2）.交互式证明助手是指推理过程需要人机交互协作完成的软件。这类软件主要有Coq和Isabelle/HOL等，能够在保证推理正确的前提下，帮助用户构造形式化的证明，并可以从构造过程中自动生成可信的计算程序。正是由于所构造的证明具有高可信度，证明助手已被广泛应用于航空航天、武器装备、医疗设备、交通、核能、金融等安全攸关软件系统的可靠性验证。 尽管人们利用证明助手构建了一些初等数学理论的形式化知识库（包含公理、定义、定理、证明等），也构造出如四色定理等数学难题的形式化证明，然而在实际应用中，证明助手还没有被数学家广泛使用。其原因主要有两方面：一是构造形式化证明的成本太高，除了要学习具有精确语法的形式化语言来编码数学知识，还要保证每步推理都必须严格有据，这就使得证明必须从相关的所有原始公理（或被证明过的定理）出发一步一步地有序进行，不然不恰当的策略会导致证明无路可走，甚至会出现循环证明的情况；另一方面是推理工具的自动化程度不高，形式化的证明与程序代码没有本质区别，晦涩而繁杂，在构造证明的过程中会频繁使用已经证明过的定理，目前并没有高效的定理搜索和策略推荐等自动化工具来辅助指导证明的构造。 因此，交互式证明助手目前在数学上的应用还处于初级阶段。随着形式化数学知识的不断累积，以及能够有效管理知识的自动化工具的出现，交互式证明助手终将成为数学家的好帮手。 人机交互界面 数学软件一般都提供可通过鼠标、键盘或触控等方式进行操作的人机交互界面，这种人机交互主要包括以下三类。 1）.文本编辑：通过键盘输入数学符号、图形、图表等编码后的文本，经过编译和运行后得到的结果直接返回到当前界面中。如WinEdt GUI、Maple Worksheet、Mathematica Notebook。 2）.按钮点击：通过鼠标点击按钮得到相应数学符号的编码文本（如 3）.手写识别：通过鼠标、触控笔或手指在软件界面上书写数学表达式，经过专门的程序识别得到相应的数学编码。如MathBrush、E-chalk、MathPad。 大部分数学计算软件都具有图形图像绘制、函数动态模拟等可视化功能，并可以进行交互处理，使抽象的数学内容以直观生动的方式呈现出来。还有一类如GeoGebra、Cinderella、JGEX、超级画板等与几何作图有关的软件，称为动态几何软件。利用这些软件所提供的作图指令，用户可以使用鼠标或者触控笔在软件界面上精确地绘制出满足给定约束关系（如平行、垂直）的几何图形，当拖动图形中的某些对象时，整个图形将被实时地重新绘制并依然保持给定的约束关系。动态几何软件的动态化和精确性能够直观地展示图形所蕴含的几何关系特征，并且一般还具有函数、几何、代数、微积分等计算功能，因此被广泛应用于教育教学与科学研究。另外还有一类由算法函数库构成的工具包（如LIBM、PETSc/TAO），它们没有人机交互界面，需要通过其提供的应用程序接口（API）供其他程序或软件调用。 数学软件远不只本文所列出的这一小部分。随着移动互联和云计算时代的到来，数学软件正朝着模块化、并行化和群智化的趋势发展，并且互操作的需求正在显现。在不久的将来，数学软件会更加深刻地影响和改变科学研究的方式和工程应用的效率。 |
|
|
