数学机械化进展综述

第 卷第 期 年 月 数 学 进 展 、 , , 数学机械化进展综述 迎接 特约文章 高小山 中国科学院数学与系统科学研究院 , 北京 , , 中国 摘要 本文介绍数学机械化理论 构造性代数几何 、 构造性微分代数几何、 构造性实代数 几何、 方程求解 、 与几何自动推理的主要进展及其在若干领域的应用 我们还提出了一些待解 决的问 关键词 构造性数学 代数几何 方程求解 自动推理 主题分类 引言 世纪以来 , 人类经历了一场史无前例的技术革命 , 出现了以蒸汽机为代表的机器 , 代替 各种类型的体力劳动 如果说工业机器的出现导致的产业革命使人们逐渐实现了体力劳动的机 械化 , 促进了社会生产力的发展 , 那么本世纪电子计算机的产生 , 则为人类实现脑力劳动的机 械化创造了物质条件 与工业革命相适应出现了解析几何与微积分这些数学上的伟大创新 在 目前这一以计算机为标志的信息革命时代 , 数学应该有什么样的创新与之相适应呢 正是基于 这种考虑 , 吴文俊先生倡导数学机械化研究 数学是典型的脑力劳动 , 因此在脑力劳动机械化过程中有其特殊地位 不仅如此 数学是 自然科学与高科技的理论基础 , 数学方法的创新有可能带动科学发展与技术进步 因而 , 数学 机械化又有其迫切性与优先权 此外 , 数学具有表达精确 、 论证严谨等特点 , 数学机械化在各 类脑力劳动的机械化中又易于实现 事实也的确如此 初等几何定理证明被认为是典型的脑力 劳动 , 而吴文俊研究数学机械化正是从这里打开突破 口 的 回顾数学发展史 , 主要有两种思想 一是公理化思想 , 另一是机械化思想 前者源于希腊 , 后者则贯穿整个中国古代数学 这两种思想对数学发展都曾起过巨大作用 从汉初完成的 《九 章算术 》中对开平方 , 开立方的机械化过程的描述到宋元时代发展起来的求解高次代数方程组 的机械化方法 , 无一不与数学机械化思想有关 , 并对数学的发展起了巨大的作用 公理化思想 在现代数学 , 尤其是纯粹数学中占据着统治地位 然而 , 对数学史的考察可以发现数学多次重 大跃进无不与机械化思想有关 数学启蒙中的四则运算由于代数学的出现而实现了机械化 线 性方程组求解中的消去法是机械化思想的杰作 对近代数学起着决定作用的微积分也是得益于 经阿拉伯传入欧洲的东方数学的机械化思想 即使在现代纯粹数学研究中 , 机械化思想也一直 发挥着重大作用 倡导的数理逻辑为计算机的设计原理做了准备 数学巨匠 关于微分方程 、 微分几何及李群的著作中经常显现出机械化特色 关于代数拓扑学 同调群计算的工作可以看作是机械化思想的成功范例 数学机械化主要有两个步骤 一是算法化 数学的机械化有赖于计算机的使用 数学要实 收稿 日期 一 一 · 数 学 进 展 卷 现机械化就必须适当地变革 自己以适应计算机有限性 、 离散性 , 特别是算法性的特点 二是机 械化 , 即在计算机上有效地实现有关算法 在这一步有效性是至关重要的 , 只有有效的软件才 能真正用来解决实际问题 以机械化数学为基础的软件可以实现人力难以胜任的繁琐的计算与 推理功能 , 从而为数学研究提供新工具 , 为数学在高科技中的应用提供有力手段 数学机械化的目标是在数学的各个分支实现机械化 当然 , 从 以及其他的关于判定 问题的否定性结果 , 我们知道很多数学领域是不能机械化的 吴文俊设想 , 数学的机械化过程 应该是选择一些即有意义又可以有效算法化的问题类 , 加以解决 , 变传统的一题一证为一类一 证 年代 , 吴文俊由中国传统数学中的机械化思想出发 , 从几何定理证明入手开始数学机械 化研究 , 所建立的数学机械化方法 , 为国际 自动推理的研究开辟了新的前景 经过近 年的努 力 , 几何定理 自动证明的吴方法及在其影响下产生的一系列重要的新方法 , 己经发展成具有我 国特色且在国际上领先的数学机械化理论 , 形成了自动推理与方程求解的中国学派 数学机械 化理论以代数与微分方程求解的吴 一 零点分解定理为核心 我们将复数域 、 实数域 、 微分 域上以这一定理为核心展开的构造性理论分别称为构造性代数几何 、 构造性实代数几何 、 构造 性微分代数几何 应该指出 , 方程求解并不是机械化数学研究的唯一研究内容 , 但选择这一问题作为主要研 究对象也有一定的必然性 世纪 , 曾提出一般问题求解的下列构想 任意问题的解答 号 数学问题的解答 分 代数问题的解答 升 方程组求解 号 单个方程求解 道 “这一构想虽未成功 , 但它仍不失为一个伟大的设想 即使失败了 , 它对于科学 发展的影响比起千万个成功的小设想来 , 仍然要大的多 ” 这是因为虽然这一设想不能涵盖很多 问题 , 但却包括了大量有意义的问题 例如 , 几何定理机器证明的吴方法就是方程求解方法的 成功应用 又如 , 以吴 一 零点分解定理为基础的方程组求解方法已经在微分几何 , 理论物 理 , 力学等领域得到成功应用 , 还为机器人学 , 数控技术 , 几何辅助设计 , , 计算机视觉等 高科技领域提供了有力工具 本文将分 部分介绍数学机械化研究的主要进展 构造性代数几何 、 构造性微分代数几何 、 构造性实代数几何 、 几何自动推理 、 方程求解方法与应用 我们将侧重介绍与吴学派有关的结 果 , 对于其他相关工作则给出主要参考文献 构造性代数几何 代数几何是近代数学十分活跃的分支 当前流行的代数几何其研究方法大都是存在性的 构造性代数几何研究方程组在复数域上的求解方法 本节介绍以吴 一 零点分解定理为核心 的构造性代数几何理论 , 其他相关结果请见 吴 一 零点分解定理 这一定理是吴文俊关于数学机械化工作的核心 , 是方程求解 、 几何定理机器证明的吴方法 的基础 这一方法是吴文俊基于中国古代数学的求解代数方程组消去法的思想并借鉴 关于 微分代数的工作 ‘ 提出的 现介绍如下 设 为一特征为 的域 , , , ⋯ , 踢 是 上以 二 , , , ⋯ , 二 。 为变元的所有多项式组 成的环 设 是 的一个泛扩域 设 为多项式集合 , 我们用 表示 中多项式在 上的公共零点的集合 , 即代数簇 设 是另一多项式 , 表示是 的但不是 的零 点所组成的集合 , 称为拟代数簇 期 高小山 数学机械化进展综述 吴 一 零点分解定理就是要给出任意拟代数簇一个构造性描述 为此 , 我们需要下面概 念 一个多项式组称为升列 , 如果通过变量重新命名后可以写成如下形式 。 , ⋯ , 。 , 。 、。梦‘ 。, 的低次项 。、 , ⋯ , 。。 , 。 , , ‘, , 的低次项 , 。 , ⋯ , 二。 , 夕 , ⋯ , , 其中 十 , 且 关于 为 、 的初式 , , ⋯ , 尹 的结构已经确定 一 形菇 · 外 的低次项 从伍 力 的次数比 、关于 从伍 力 的次数要低 入 兴 称 设 二 , ⋯ , , , 为 、 的初式的乘积 , 我们可以认为 设 为一升列 , 定义 尸 存在 初式之积 使得 尸 任 我们有 对于不可约升列 , 是一个素理想 ‘ 对于任意升列 , 或为空集或是一个单纯代数簇 , 即 的所有 不可约分支均有相同的维数 旧侧 设 尸 为一多项式的非空集合 , 一升列 , 儿 , ⋯ , 人 称为 尸 的特征列 , 如果 介 任 乞 , , ⋯ , 且对任一多项式 任 , 对 的余式 , 我们有 定理 零点分解定理 一 弱形式 川 对一非空多项式集合 尸 与任一多项式 , 我 们可以在有限步内构造有限个升列 、 , 使得 一 、 人 , 其中 人 为 、 中多项式的初式之乘积 , 且 , 、 并 对定理 中诸 、 中的多项式依次做代数扩域上的因式分解 , 我们可得 定理 零点分解定理 一 强形式 , 对任意多项式的非空集合 和任一多项式 , 存在一算法在有限步内或者判定 尸 为空集 , 或者找出一组不可约升列 ‘ 乞二 , ⋯ , 川 满足 二 人 , 其中 人 为 、 中多项式的初式之乘积 , 且 , 、 并 哟 定理 代数簇的分解 对任意多项式的集合 和多项式 , 如果存在下面形式 的分解 一 日 ‘ 人 , 则有 一 , · 上述定理给出了代数簇的不可约分解与单纯维数分解 , 但其中有些分支是多余的 要想去 掉这些多余分支 , 我们需要计算 的生成基 对于不可约升列 , 」给出了基于 坐标的计算方法 也可以用 基方法计算 的生成基 , , 卷 定理 代数簇的唯一分解 对任意多项式集合 尸 和多项式 , 我们可以求得不 可约升列 ‘ 乞 , , ⋯ , 川 与素理想 ‘ 的生成基 尸 ‘ 使得 一 又 一 ‘ , 且以上分解中任何一个分支都不能去掉 上述定理导致了一系列后续研究 等人了该方法的复杂性问题 ‘ , ’ 另一 研究热点是各种不同的升列及其性质的研究 “ , ‘ , ‘ , , , ’, ‘ , 研究 了吴 一凡 零点分解定理在一类解析函数中的推广 沐 ‘ 李研究了吴 一 零点分解定理在 代数中的推广 问题 能否将上述零点分解定理推广到解析函数 、 某些非交换代数 、 差分代数 由于零 点分解定理有众多应用 , 这一推广应该可以用来解决相关方向的许多问题 投影定理 投影定理可以看作 结式概念的推广 设 尸 是 。 , ⋯ , 。。 , , ⋯ , 纵 」中的多 项式集合 , 是其中多项式 , 投影的概念定义如下 可二 , ⋯ , 。 任 】日 任 几 , 使得 , 任 · 如果 。 , 我们视 尸 是否为空集定义 叮二 ⋯二 。 尸 为 或 不难看 出 , 投影实际上给出了一个方程组对于变量 , 有解的条件 我们有 定理 拟代数集的投影是若干拟代数集的并 进一步 , 存在一个算法在有限步内 求得下面分解 , ⋯ , 。 一 、 从入 , 艺 其中 ‘ 是 中的升列 , 从 是 中的多项式 , 入 是 ‘ 的初式之乘积 这里 代 表变量 。 , ⋯ , 二。 作为投影定理的一个应用 , 我们可以给出复数域上的一阶谓词逻辑公式的判定算法 复数 域 上的一阶谓词逻辑公式 简称公式 可以严格定义如下 · 复数域 上的多项式等式 尸 , ⋯ , 动 是一个公式 · 如果 , 是两个公式 , 则 八 或与 , 绒或 , , 非 也是公式 · 如果 是一个公式 , 则 日 任 , 二‘ 任 也是公式 下面是一些公式的例子 , , ⋯ , 讹。日 “ 沙一‘ ⋯ 。 , 即代数学基本定理 ⋯ 。 八 ⋯八 井 , 即定理证明 · 设 是一个公式 , 通过一些简单的逻辑变换可以将 变为下面形式 。 , ⋯ 。 、 只 八 ⋯ 只 。‘ 八 ‘ 半 八 ⋯八 、、 、 并 , 其中 是量词 日或者 , 凡‘ , , , , ‘, 是多项式 变量 几‘ , ⋯ , 肠 称为被限制的变量 未被限制的变量称为 自由变量 所谓复数域 上的一阶谓词逻辑公式的判定是指下面两类问 题 期 高小山 数学机械化进展综述 判定问题 如果 中无 自由变量 , 判定公式 在复数域上是否正确 谓词消去 如果 中有自由变量 , 找到一个只含自由变量的公式 使得 与 在复数 域上等价 定理 复数域 上的一阶谓词逻辑公式的判定问题与谓词消去问题都可以由投影定 理给出 代数簇的若干表示及转换 代数簇最直接的表示形式是生成元或隐式表示 由 有限基定理 , 对任一代数簇 一定存在有限多项式集合 尸 , ⋯ , 纵 使得 代数簇的另一种常用的表示是其参数表示 一般地讲 。 , ⋯ , 。 , ⋯ , 。 · “ , 参数方程是指形式为 凡 。 , ⋯ , 。 , 。 。 , ⋯ , 。 , 的一组有理方程 几 中点 。 称为 名 的母元或 称为 的子元 , 如果对 【 中任一多项式 侧 , 由 。 二 可以推出 劝 点 个不可约代数簇 如果 二 的所有子元的集合记为 不难证明 是一 , 点 称为代数簇 的母元 不难证明代数簇是不可约 恤 的当且仅当它存在母元 吴文俊指出代数簇的母点可以由不可约升列显式给出 , ⋯ , ” , , , , ” , ⋯ , ”。 , , , , , ⋯ , 寿 “ , ⋯ , 。。 , , , ⋯ , 将变量 代换为一组自由变量后可以依次求得 , , ⋯ , 外 , 从而得到 的一组解 , 称为升列 的母点 设不可约升列的母点为 , 则 尸 二 定理 设 是一个形如 的不可约升列 我们可以求得整数 , ⋯ , , 与新变元 二 , ⋯ 四 , 使得在变元顺序 。 。 , ⋯ 、 下有 二 一 , 一 · 一 外 ‘ , 其中 是 的初式的乘积 夕 具有下面形式 , ⋯ , 二。 , 。 。 , ⋯。。 , 二 , 一 。 , ⋯ , 。 , 。 , ⋯ , 。 , ⋯ , 。。 , 二 夕 一 炜 。 , ⋯ , 。 , , 其中 , 几 , 队 乞 , , ⋯ , 川 均为变量 。 与 二 多项式 我们称 是素理想 的预解式 由此得到不可约代数簇的预解式表示 。 , ⋯ , 。 , 二 , 。 , ⋯ , 。 , 二 。 , ⋯ , 。。 , 二 ’ “ , 外 今 。 , ⋯ , 。。 , 二 叽 二 , ⋯ , 。。 , 设 是一个形如 的不可约升列 设 ⋯ 二、外 , 乞 二 , , ⋯ , 在变元顺序 切 夕 、 叨‘ ⋯ 切‘。 。 叨‘。 夕 下使用吴 一 零点定理可以在 与 数 学 进 展 卷 ‘ , 乞 , , ⋯ , 中消去 。 , ⋯ , 。。 , , , ⋯ , 外 , 得到多项式 二‘, 。、了 称为代数簇的 形式 我们现在已给出了代数簇的五种表示方法 下面介绍它们之间的互相转换 一 , 又称为隐式代数簇的参数化 这一问题一般分为两步 由定理 , 可以找到一个多项式 尸 定义的超曲面使其与给定的代数簇双有理等价 , 并给出相应的双有理变换 这样 , 一般代数簇的参数化问题就变成了超曲面的参数化问题 寻找超曲面的参数方程 这一问题还远未彻底解决 只对曲线 、 曲面给出了存在算法 参 见 , , , 」 问题 给出一般超曲面参数化的条件与有效算法 · 、 , 又称为参数方程的隐式化 这一问题在计算机图形学中有重要应用 对于参 数方程的隐式化我们可以提出下列问题 求参数方程定义的素理想的基 , 即以 , ⋯ , 氏 。 为母点的素理想的基 参数方程在 维空间形成的映象 一 一 , ⋯ , 几 , ⋯ , 几 尺 , ⋯ , 几 、 , , 。 下丁下苏一一 —下一下 卜 , “ ’ , 。 七 乃 了 材 。气 , ” ‘ , 。 的定义方程 对于一组可能的 的值 , 相应的 。 的值是否唯一 如果不唯一 , 能否找到一组新参数方 程与原方程等价且这样的值是唯一的 这些问题可以用零点定理解答 ‘” , 第三个问题与 定理有关 , 只对单个参 变量情形存在解答 问题 高维 定理 设 , ⋯ , 。 为变量 。 , ⋯ , 匈 司 的有理函数 , 求有理 函数 , ⋯ , 己 使得 , ⋯ , 。 , ⋯ , 己 , 其中 为有理数域 , 邢 、 , 一 , 。 可以用吴 一 零点分解定理来实现 一 见 奇异代数曲面的陈示性类 对一般代数簇 , 引进了陈省身示性类的概念 , 但须假定代数簇没有奇点 利 用不可约代数簇母点的概念 , 吴文俊对具有任意奇点的代数簇成功地建立了陈省身示性类的概 念 ‘“ , ‘ 当代数簇光滑时 , 昊给出的定义就是通常的陈省身示性类 而且他所定义的陈 示性类是代数等价类 , 是具体可计算的 应用这一定义 , 吴文俊 、 石赫证明了丘成桐 一 不等式的下述推广 【 , 定理 对任意给定的正数 , , 具有任意奇点的超 曲面 。 有 一 “艺‘无’ 、 , 、 瓜 “ 一 无从 全 乞 其中 、 由下式给定 片一 一‘ 无一戮默动 玲一 一‘ 丸一 ‘ 乞一 ‘ 默动 , ‘一 , , 一 ” 期 高小山 数学机械化进展综述 设 , 由具有奇点的超曲面 从 的对应于 的分拆 抓哟 的全体陈示类所张成的线 性空间为 “ 二 凡 、 域句 是 的所有分拆 定理 对具有奇点的 维超曲面 瓜 及任意给定的 , , 线性空间 的维数等于 由于当 时 无 的分拆个数多于 , 由上述定理对具有任意奇点的 维超曲面 瓜 , 当 时 , 。 的陈示性类满足一系列等式关系 例如 , 对 二 无三 , 从 的陈示性类满足下面 的等式 凡 瓜 艺 。 氏 一 , 葱 其中 。 , 二 一 , “ , 一 一 , 刘证明了吴定义的陈类是有理等价类 “ ‘〕, 并用这一定义给出了计算代数曲线亏格的新公 式 【 刘还证明了吴的定义与 年代出现的另外两种定义之间的关系 的定 义与吴的定义等价 , 但 的定义 阿 与吴的定义不同 构造性微分代数几何 微分代数几何基本上可以理解为将代数几何理论推广至代数微分方程 【 这一领域始于 关于微分代数的研究 ‘ 代数几何的很多理论 , 如吴 一 零点分解定理可以推广至微 分情形 但总体来说微分代数几何还有很大的发展空间 例如 , 代数曲线的亏格这一基本观念 就未能推广 问题 定义微分曲线 即维数为 的不可约微分簇 的亏格 特别 , 给出判定微分曲线 有理化的方法 微分域上的吴 一 零点分解定理 一个域 称作微分域 , 如果域 中除了具有通常域的运算与性质外 , 还有一个微分算子 , 例如有理函数域 在微分算子 ‘ 杀下就构成一微分域 系数在 中变量 二 , ⋯ , 二 及对 其导数的多项式称为微分多项式 设微分多项式 中的次序最高的变元为 , 尸 中 的最高 微分为 价 , 记为 孙 , 。 我们有 尸 一 , 。 十 一 招盆 二 十 。 , 其中 称为 尸 的初式 , 耀三二十 ⋯十 , 叫做 尸 的隔离子一个微分多项式组 的零点集合记为 一 我们有 定理 微分零点分解定理 一 弱形式 司 对一非空微分多项式集合 尸 与任一微分 多项式 我们可以在有限步内构造升列 、 , 使得 一 一 、 人 , , , ⋯ , 尸 , 其中 人 为 、 中微分多项式的初式与隔离子之乘积 , 且 , 、 并 定理 , , 一 可以推广到微分情形 关于这些定理的详细叙述请见 给出了基于弱升列的改进形式 叭认 给出了基于 消去法的改进 但是定理 尚不能推广 , 主要问题如下 数 学 进 展 卷 问题 凡 问题 给定两个不可约微分代数簇 , 的特征集 , , 判定 是否包 含 问题 理想成员问题 给出判定一个微分多项式属于由有限个微分多项式生成的理想的 判定方法 偏微系统的完全可积理论 上节的概念与结果均可推广到偏微情形 与常微情形不同 , 对于一个非平凡升列 一 二 , ⋯ , 二 , 我们需要引入可积多项式概念 , 将其变为被动的 通过引入 肠 形式级数 , 可以定义不可约 升列的母点 定理 若 一 是一个被动的不可约升列 , 是其母点 则有 是一个不可约微分代数簇 对微分多项式 只尸 当且仅当 尸 对于 一 的余式为零 对微分多项式 只 尸 二 必 当且仅当 尸 对于 一 的余式为零 同样 , 定理 一 , 一 可以推广到偏微分情形 求偏微分代数系统的可积性条件的算法可以分为两类 一类是源于 , , 关于偏微分方程的古典理论 吴 一形 零点定理就属于这类 一些新的发展可参考 , 另一类由 区。‘ 提出求所谓 自约化集 这一方法与著名的 基的算 法非常相似 , 一些新的发展可参考 , 问题 判断被动升列与 基是否相同 , 并对两种方法的效率进行比较 由 引入的 基的概念是符号计算与构造性代数几何中的基本工具 吴 于 中指出 , 基可以基于偏微可积理论中的 一 理论导出 微分方程的解析解 利用微分和差分 理论求微分和差分方程的解析解 , 是微分代数几何中一个非常有挑 战性的问题 因为解析解比数值解更能反映方程的结构和特性 , 所以受到物理学家和工程师的 高度重视 构造微分方程的初等函数解可以追溯到 世纪 的工作 在 年代给出了 复数域上单变量初等函数的积分为初等函数的精确算法 【 】 则将这一结果推广到二 阶齐次线性微分方程 区山 则提出了求一般线性微分方程 解的一般方法 ‘ 李和 给出了求解某类 偏微分方程的超指数函数解的方法 【 对于非线性微 分方程 , 即使是最简单的情形也还没有完整的结论 问题 给出求解常微分方程多项式解的算法 求解微分方程系统的重要手段是对其进行化简 较为一般的方法是通过偏微方程对称群的 计算可以将原方程降阶 , 或将偏微方程变为常微方程 , ‘ 对于单变量线性微分算子 , 李 在 , ’ 中提出了计算 代数中多项式的最小左公倍数与最大右公因子的模算法和无分 式算法 , 使得这一问题得到很好的解答 自从 一 在 年观察到浅水波中的孤立子现象以来 , 非线性发展方程行波解 孤立波解 , 孤立子解 的研究一直为数学家 、 物理学家所关注 寻求非线性发展方程的行波解 孤立波解 是一个重要的研究方向 李等人在 匡 , 中提出统一求解一类非线性发展方程 期 高小山 数学机械化进展综述 的行波解与孤立子的机械化方法 其想法是通过引进某种变换将微分方程求解问题化为代数方 程求解问题 , 然后再用吴方法求解代数方程 使用这一方法已经发现了上百种微分方程的孤立 波解与孤立子解 这一工作的综述参见 〕 张则提出了求力学中常见微分方程解析解的一般框架 对分解法 ’ , 并用这一方法 解出了力学与物理学中大量的微分方程 石赫将这一方法用于著名的杨 一 方程 , 得到了其 简化形式 〕 , 这一工作的综述参见 【 构造性实代数几何 实代数几何主要是研究多项式方程在实闭域上定义的零点结构 因为实闭域的结构比复数 域要复杂得多 , 实代数几何的进展一直很缓慢 近年来 , 由于人们认识到很多高科技问题 , 特别 是机器人与计算机视觉 , 可以归结为实代数几何问题 , 构造性实代数几何的研究逐渐兴起 【 实闭域的判定算法 在本世纪 年代 丁 证明了实闭域的可判定性 , 从而证明了初等几何与初等代数的可 判定性 这里 , ‘初等 , 是指一阶量词逻辑所能描述的公式 定义如下 变量 ⋯ , , 原子公式 多项式 多项式 多项式 多项式 , 公式 二 原子公式 卜公式 公式 公式 己变量 公式 变量 公式 , 给出了实数域上得一阶逻辑公式的量词消去法 在解决上述问题的已有算法中 , 提出的柱型代数分解算法 最为有效 , 并且 已在计算机上实现 算法一般形式可参阅 这一算法基于下面想法 一个句子的 真值仅依赖于多项式的符号 一 正 , 负 , 或零 , 所以若在一区域内公式中多项式的符号不变 , 则 公式的真值也不会变化 算法即将 分解为有限个柱型区域 , 使得相应公式中出现的 所有多项式在每一区域上不变号 这样 , 为了证明公式在整个空间上正确与否 , 只需在每一区 域上取一点代入公式检证即可 换句话说 , 为了说明一公式的正确性 , 我们只需在若干个点上 验证即可 以上方法虽然很完整 , 但其效率较低 现在已有的计算实现还不足以解决较困难的问题 下面将介绍两种效率较高的方法 全局优化符号计算法 针对一些常见的与不等式有关的问题 , 吴提出了求解下列优化问题的算法 网 问题 设 为欧氏空间 “ 中的区域 , 为 “ 上的实多项式 , 试决定 在下面条件 ‘ 二 , 乞 , , ⋯ , 兴 。下在区域 上的最小值 对于上述问题 , 吴证明了下面有限核定理 定理 设 , ⋯ , 。 , 则存在一算法确定 在 刃 上的有限个值 的集合 , 使得 中的最小值 二 在 刃 上的最小值 中的最大值 二 在 刃 上的最大值 这一算法的基本想法是首先用吴 一 零点分解定理将 功 化为 , 其中 为升列 , 且 中包含 的初式与隔离子 定义见第 节 再用 方法求极值 数 学 进 展 卷 吴将上述算法用于解决如下问题 给出多项式方程有正根的判断条件 , 非线性规划 ‘ , 机器人碰撞问题 〕及代数与几何不等式自动证明 , 多项式的完全判别系统 我们知道二次方程 “ 阮 十 的判别式为 护 一 给出了方程的根的性态 对于一 个 二 次多项式方程 , 高在 中定义了 尸 劝 的复完全判别式并给出了其计算 方法 如果考虑方程的实根 , 则需要实根 、 虚根的重数 这种情形比复数情形要困难得多 古典 结果己给出四次多项式的根的完全分类 借助 的 方法 自动给出四次 多项式的正定条件 杨等人在 」中提出了对任意次数的多项式建立完全判别系统的一个新 算法 , 并计算出了 至 次多项式的完全判别式 所谓单变量方程的完全判别式 , 就是对于该 方程次数 的任意拆分 , ⋯ , 、 , 给出这一方程具有 ⋯ , 琳‘ 个不同实根与 二 , ⋯ , 低 个不同虚根的显式条件 下面的 问题是计算机视觉中经典的定位问题 这一问题在计算机动画 、 机器人 、 制图 学中都有应用 一些相关结果请见 问题 问题 给定了空间中 个点 几 , 几 , ⋯ , 几 的相互位置及这些点对于点 尸 的 视角 只尸几 三 乞 三 , 求点 尸 的解的个数的分类 即给出 点有 , , ⋯个解的条件 不等式自动证明 构造性实代数几何的一个明显的应用是不等式自动证明 的 方法经 实 现后已经能够证明非平凡的不等式 近来 , 的实现在效率上又有所提高 等人 最近的工作表明 , 如果把消去理论限于二次方程 , 则可以得到高效的不等式证明器 , 在 中 , 周与高用吴零点分解定理来证明不等式 这一算法虽然不完全 , 但却能证明 相当困难的约 个不等式 在 阿 中 , 将吴零点分解定理与 的 方法相结合 首先用吴零点分解定理将问题简化 , 如果遇到高次方程的不等式问题再调用 的 程 序 基于完全判别式理论 , 杨提出了针对某类几何不等式的机器证明快速实用算法并编制成用 实现的通用程序 “ 厂 〔 这个程序对于 等人在其专著 《几何 不等式 》中所研究的那一类初等几何不等式的机器证明特别高效 用软件 在奔腾 上证明该书中 个基本的几何不等式总共费时仅 秒左右 用这个软件已证了 多个几何不等式 , 其中很多是若干年来人们提出但未解决的问题 多项式的正定判定问题是不等式证明的一个特殊问题 第 问题猜测一个正定 多项式总可以表示为若干有理函数的平方和 在 年证明了这一猜想 但是 , 这一问 题的构造性证明还未给出 问题 第 问题的构造性证明 给出算法将任意一个非负多元多项式表示为相 同变量的有理函数的平方和 几何自动推理 定理证明机械化思想由来已久 , 一些原始想法可以追溯到 世纪的 和 现在流行的自动推理方法可以分为三类 以 理论及 为代表的逻辑方法 以 , 等人为代表的人工智能方法厂鸡赤 理论与吴方法为代表的代数方法 几何定理证明的机械化可以追溯到本世纪初的 年代 , 证明了实闭域的 期 高小山 数学机械化进展综述 判定算法 , 从而给出了初等几何的判定算法 这一算法虽经 , 等人的改进 , 但仍然太繁杂 , 以至于不能证明有意义的几何定理 在计算机上尝试证明几何定理始自 年代 末 等人的经典工作 但此后几十年这方面进展不大 主要问题是所用的方法均不够 有效 吴文俊引入的基于代数计算的方法是第一个可以有效证明困难几何定理的方法 在吴的 工作的影响下 , 几何自动推理得到迅速发展 现在我们不仅可以有效地证明几何中的大部分定 理 , 而且可以自动发现定理 不仅可以证明初等几何中的定理 , 还可以证明微分几何 、 力学中 的定理 在证明方式方面 , 可以产生可读证明 对于一个定理可以产生多种证明与最短证明 在吴文俊获得 ‘ , 自动推理杰出成就奖 ” 的授奖辞中提到 “吴的工作将几何定理证明从 自动推理的一个不太成功的领域变为最成功的领域之一 在很少的领域中 , 我们可以讲机器证 明优于人的证明 几何定理证明就是这样的一个领域 ” 几何定理机器证明的吴方法 利用吴方法证明几何定理可以分为如下几个步骤 几何问题的代数化 建立坐标系 并对定理中的点选取适当的坐标 , 则定理的假设可以写成多项式方程组 、, ⋯ , 。 二 , ⋯ , , 二 , ⋯ , 。 , 结论写为 二 , , ⋯ , 动 整序 令 尸 , , ⋯ , 对 中所出现的变元 选取适当的次序 , 并对 尸 进行整序 , 求出 尸 的特征列 将结论多项式 , , ⋯ , 际 对 中的多项式按类的高低从大到小依次进行约化 , 求出 , , ⋯ , 。 对 的余式 如 果 , 则说明在诸 人 并 。的条件下 , 定理是正确的 吴方法的这一简单形式已经可以用于 证明大量非常困难的几何定理 ‘ , ‘ , ’〕, 还被用来发现了若干新定理 , 一般讲 , 设 是一个几何命题的假设所对应的多项式方程组 , 为几何命题的结 论 , 笋 , ⋯ , 拼 是几何命题的一组给定的非退化条件 由吴 一凡 零点分解定 理 又 去 , 泛 其中 是多项式 ‘ 的乘积 ‘ 是不可约升列 去 是 又 坛二 , , ⋯ , 约中多项式的初式 的乘积 如果 。 , 则原几何命题为可约的 我们有 结论 二 在复零点集 ‘ 所对应的图形上正确当且仅当 , 又 二 吴方法于 年代末出现后 , 引发了一场关于几何定理机器证明的高潮 吴对上述基本方 法作了很多改进以适应各种不同情况 一 王 、 胡 、 高等人研究用吴方法证明构造型定理与 轨迹求解问题 〔 ‘ , ‘ 林 、 刘将吴方法推广至有限几何 【 ‘ 、 。 、 、 高 等人研究用吴 一凡 分解算法证明定理 区 ‘ , ’, 关于非欧几何的代数化与定理证明方法 见 , 受吴方法的启发 , 年代中期 , , , 等人提出了基于 的方法 ’ , “‘ , ‘ 洪在 中基于吴方法提出了几何定理机器证明的单点例 证法 这一算法复杂度很高 , 未能用来证明大量几何定理 张 、 杨等人提出了多点例证法 , 提高 了例证法的效率 〕 , 张 、 杨等人提出了基于结式与 的证明方法 阵 ‘ , ‘ , 不用因式分解即可得到完整的定理证明算法 几何公式的自动推导 吴 一形 分解定理不仅可以证明定理 , 还可以自动发现定理 原理如下 设 为分解中 数 学 进 展 卷 得到的升列 , 而 , , ⋯ , 。。 , 为 中第一个多项式 则我们实际上求得独立变量 与变 量 , 之间的关系 这类问题是求方程的流形解 几何公式的推导与轨迹方程的计算就是这样两 类问题 】例如 , 设 与 是四面体 的外接圆的直径与体积 , 吴用他的方法发现 了下面公式 , , 一 一 一 , 其中 , , , 上述想法可以推广至更一般的形式 给定一个复数 实数 , 微分 域上的一阶谓词逻辑公 二 , ⋯ 、 沪 , 其中 , 是谓词 日或者 , 沪 是一个语句 利用第 , 节中的投影定理与量词消去法消去变 量 凡‘ , ⋯ , 肠 , 得到一个只含自由变量的公式 , 使得 与 在复数域 实数 , 微分 上等价 我们实际上发现了一个新定理 几何公式的自动发现在机器人学中有很多应用 , 一个著名的 例子见问题 微分几何与力学中的定理证明与发现 与初等几何的情形相似 , 微分多项式组的整序算法同样可以应用于微分几何中定理的机器 证明与一些几何关系或公式的自动发现与推导 详细论述请见 、 〕下面举例说明 一 问题 利用吴方法在微分域上的推广 , 可以研究 叩 经验定律与牛顿引 力定律之间的关系 定律为 行星绕太阳依椭圆轨道运行 , 并以太阳为该椭圆的一个焦点 从太阳到行星的向量在相同的时间内扫过相同的面积 牛顿引力定律为 行星的加速度与太阳到行星的距离的平方成反比 利用零点分解定理我们可以由 经验公式自动发现 定理 网 ‘ 中用吴方法发现了仿射微分几何中的若干新结果 实现了由吴提出的通过计 算维数来证明定理的想法 研究了将吴方法用于曲面的定理证明 匡 通过考虑微分形 式 , 将吴方法推广到向量情形 考虑了用其它消去法来证明微分几何定理 面积法与向 法 借助面积证明几何定理在几何解题方法中可以说是源远流长 用面积证明几何定理算法是 由张 、 高 、 周在近年给出的 这一方法可以生成几何定理的简短可读证明 用面积法证明定理的基本步骤是使用上述几何不变量 例如 , 面积 , 比例等 的基本命题 , 从几何命题的结论中消点 当结论中的所有点被消去后 , 命题的结论成为一个关于某些独立变 量的表达式 , 于是结论成立与否就不难判断了 下面是面积法使用的一个典型的消去规则 设 是直线 尸 , 的交点 , 则对于任意三角形 , 可以用下式将点 从面积 匀 中消去 面积方法被推广至立体几何 ‘ 丑 尸 一 尸刀 尸 几何 ‘ , 几何和 几 何 【 司 基于相似观点 , 中还提出了全角法 , 并与搜索方法结合用来生成一题多解与最 期 高小山 数学机械化进展综述 短证明 与面积法相似 , 可以发展基于向量的定理证明方法 三种算法由高 、 张 、 〕, ‘ , ‘ 给出 李与程在 中提出了基于 肠 代数与吴方法的向量算 法 这一算法不仅可以用来证明初等几何定理 , 还可以证明微分几何中的定理 王等提出 了基于重写规则与 代数的定理证明方法 田 〕并考虑了在计算机视觉中的应用 【 , 进一步发展了证明二次曲线的 代数方法 几何自动作图 与定理证明相比 , 几何作图问题的机械化在 自动推理界考虑较少 由于这一问题在 领域有重要应用 , 在这一领域一直受到关注 当然 , 几何作图问题可以直接转换为代数方程求 解问题 由于实际上遇到的问题经常包含上百个几何元 , 同时又要求得到方程的所有解 , 这使 得一般的数值计算与符号计算方法并不能很好地适用于这一问题 可行的办法是将一个大的问 题分解为若干小的问题 , 分别解决这些小的问题 , 然后再将它们装配起来 这样的方法称为几 何 自动作图的几何法 其中最主要的两步是问题的分解与装配 几何图形的分解主要有基于规则的方法 区 与基于图论的方法 田。‘ 基于规则的方法将 几何知识表示为推理规则 , 然后再用 自动推理方法求解几何问题 基于图论的方法则将作图问 题表示为关系图 , 然后再用图论算法将原问题分解为若干子问题 其中 月’ 一 利用图 的三连通分解给出了用尺规几何作图的有效算法 旧 ‘ 在 旧 中提出了将一般问 题分解为最小刚体的的图论算法 高等人提出的算法给出了用尺规 自动求解所有简单多边形问 题的有效算法 旧 但是 , 即使对于尺规作图 , 也不存在完整的几何算法 问题 给出一个基于图论算法或基于推理规则的判定尺规作图的算法 几何作图的装配主要是对于一些所谓基本形问题的计算 这些基本形被用作子问题装配的 基本模式 二维情形最简单的基本形具有 个点与 个距离约束 〕, 三维情形的基本形可以 是四面体 , 五面体与六面体 等人用符号计算与同伦法解决了若干基本形 , ’ 高 等人用四连杆与轨迹相交法解决了顶点数在 以内的所有基本形 方程求解的方法与应用 代数方程组求解主要有两种方法 数值计算法与符号计算法 符号计算法有 基 法 田 ’ 、 特征列法 网 与结式法等 一般来说 , 数值计算法具有速度快 、 应用范围广等优 点 , 但也有误差控制难 、 只能给出局部解等缺点 符号计算法则可以给出完全的精确解 包括 流型解 , 但常遇到因中间多项式过大而导致的计算困难 最近的研究热点是将数值计算与符号 计算相结合的混合运算 墓于吴 一 零点分解定理的求解算法 如第 节所述 , 吴方法就是将一个一般的代数方程组变为若干三角形式的方程组 , 而三角 形方程组的解结构已经基本清楚 这一方法具有以下特点 可以给出方程组解的完整结构 在 高维情形可以给出解流形 但这一方法也有其局限性 , 例如将这一方法用于实际问题 , 在计算过程中间中往往会遇到 大的多项式 李 国“ 指出 等人发现的多余因子问题在特征列计算中也会出现 为了解决 这一问题 , 吴在 中提出了基于子结式的特征列方法 这一方法主要有下面三个特点 消元采用 一 的方式 即先消下标最大的变量 这一点与 的算法一致 数 学 进 展 卷 · 用子结式序列两两消元 设 , 为两个含有相同主变量 的多项式 , , ⋯ , 凡 为 与 的子结式序列 如果 , 对 的结式为零 , 则 , 可以用它们的最大公因子代替 若 尹 且 , 子序列中存在含有 的非零子结式 凡 , 则 , 可以用 。 与 代替 否 则我们用 。 代替 , 中次数较高者 以上改进与杨等人提出的聚筛法 ‘ 相似 , 不同之处是聚筛法使用的是 结式 其它改进包括 使用不同类型的特征列 例如弱升列 ‘ , ‘ , 正规升列 陈 ‘ , ‘ ,“ , , , 其它 一 消去法 王对 消去法作了改进与实验 〕 等人也 提出了 一 消去法 区 , , 并用于特征列方法 一 高提出了用维数定理减少多余分支的想法 沁 ‘ 混合算法 吴提出的符号计算与数值计算的混合算法主要解决两个问题 混合计算中的误差估计问题 吴将一个近似数 。 表示为 。十 亡。 , 其中 亡。 一 , 将 亡。 当作变量 , 通过用特征基方法可以得到一个单变量多项式方程 。 十 对 十 ⋯ 。 十 及 , 其中 ‘ 为常数 , 双 为 艺 ⋯尤二 多项式 乞 , , ⋯ , 动 我们可以求解下列方程 。 犷 ⋯ 两者之间的误差 , 可以用 定理估计 这一方法还有其它优点 , 详见 多项式的近似因式分解 设 , , 任 , ‘, , ⋯叼 · 其中 为取值很小的变量 我们 说 可以 阶近似分解为 如果 一 对于 ⋯艺, 的阶数 七 十 在 中给出 了将多项式近似分解为两个多项式乘积的算法 一些新近发展见 吴方法的应用 吴文俊特别强调方程求解的应用 , 将他的方法用于解决力学 ‘ , 物理 ‘“ , 化学 等领域与机器人 网 , 几何造型 ‘ , 连杆设计 ,‘闭 等高科技的问题 吴的方法还被用 于多项式因式分解 【 , 发现微分系统新的极限环 〔 , 求解微分方程的行波解与孤立子解 哪‘ , ‘ , 理论物理 〔 ’ , , , 几何造型中的曲面形式转换问题 , , 一阶逻辑公式的证明 ‘ , 计算机视觉 【 , ‘ , 连杆设计问题 ‘ , 智能 , 组合恒等式 自动证明 ‘ 等 我们将介绍若干应用 曲面连接问题 在几何设计中有一大类问题可以一般地描述为 给出 ” 中的不约代数曲 线 认 , 几 , 、 , 乞任 , , 任 , 凡 任 , 其中 , , 都为有限指标集 , 以及两组不可约代数曲面 , 凡 , 、 , 任 么 任 , 分别包含曲线 几 与 , 确定一给定次数 。 的代数曲面 , 使得 通过所有的 公 , , 、 沿曲线 几 与 分别与曲面 , 、 光滑相切 沿 、 对 、 有相同的曲率 这类问题可以用吴方法解决 ‘ 对这一问题的综述可见 机器人与连杆机构的运动分析 运动分析有两类 已知连杆机构的构成 , 求该机构上某一 点的轨迹及该点的位置与连杆机构的关系 这类问题称为机械设计中的正解问题 反过来 , 求 期 高小山 数学机械化进展综述 解连杆机构的参数使得连杆机构上一点恰好位于空间的指定位置的问题 , 称为机械设计中的逆 解问题 这两类问题都可以看成方程求解问题 吴文俊在 中用特征集方法解决了一般 型机器人的逆解问题 , 在 中研究了四连杆的设计问题 下面是一个还未彻底解 决的正解的问题 问题 平台 如图所示 , 带网格的平台是空间中一个 活动平台 下面的平台是固定平台 六根连杆长度可变 求这六根连 杆的长度变化时平台的位置 这是一个非常困难的正解问题 , 现在还没有完全解决 已知这一 轨迹是一个次数为 的多项式所确定的空间图形 , ‘ 平台的研究具有很强的应用背景 最近研制的基于 平台的 数控机床被称为是 世纪的机床 关于这一问题的综述可见 旧 ‘ 赢赢赢 星体的中心构型的确定 设 个星体的质量为 , ⋯ , 在牛顿引力作用下 , 这些运动 的星体在某时刻的空间位置记为 , ⋯ , 。 这些星体的质量和位置 。 , ⋯ , 饥二 , ⋯ , 队 称 为这些星体 。、在位置 的一个构型 星体的构型称为中心构型 , 如果存在这些星体的一组初 速度使得它们在运动中与初始状态保持相似 关于中心构型 , 有下面猜想 猜想 对于任意质量 , 只有有限个中心构型 设 。 , 。 司 , 分别为 个给定质量的星体在空间 , 平面 , 直线上中心构型的个数 则有 , , 言 ,‘ , ‘”‘ · 吴文俊在 」中证明中心构型的决定可以化为代数方程的求解问题 , 并用这一方法证明了 时所有可能的中心构型即为由 与 给出的解答 , 在不可压缩非粘 性无穷大的流体中 , 若其受力非零且满足若干条件 , 则所有可能的中心构型为 线性型与 罗 等边型 杨 一 方程与 子群 杨 一 方程首先是由杨振宁先生在 年建立的 , 它 反映了物理量之间的交换关系 杨 一 方程是复数域上的一组代数方程 因此 , 从理论上 讲 , 应用吴消元法可求出方程的全部解 但是 , 一般 维情形下这组方程极为复杂 , 就是在二 维情形 , 这组方程由 个三次多项式方程组成 , 包括 个未知数 可应用吴消元法 , 采用人 机对话的方式 , 运用多种技巧 , 成功地求出了二维杨 一 方程的全部解 , 参阅 相应于杨 一 方程的解 , 可得到量子群 然而在获得杨振宁 一 方程的解之后 , 如何具体计算对应的量子群并非易事 文 给出六顶角的杨 一 方程的解与计算相应 量子群的机械化方法 微分系统稳定性判定与极限环的个数 我们知道 , 多项式微分系统 二 夕十 乃 , 夕 几 , , 一 氏 , , , 一 , , 万 二 , 军 ⋯ 二 , 夕 丽匆一 数 学 进 展 卷 极限环个数问题 , 即 第 问题 , 是微分方程定性理论研究中的重要问题 这一问题通 行的研究方法是构造微分系统的 函数 , 计算相应的判定量而获得结论 这一研究过程 涉及大量繁杂多项式的推导 、 简约 以吴消元法为理论基础 , 综合利用计算机代数中的各类技 巧 , 王等人用吴方法发现了具有六个极限环的三次系统 关于这类工作的综述参见 参考文献 〕 , 爪尸 记 乞夕几 , , 一 【 」 · 了百百召 二 · 二 几 , 云 几 乞几 云夕 几 , , 一 」 一 ’ , , , , 、 , , , 一 【 』 , , 。 、 , , 一 〕 , , , , , , , 、’ , , 一 【 」 一 犷 , , , , , 、 , , , 一 价 · · , 认飞〕 , , , , , 一 【 、 一 、 人 几 一 子 几亡 , 尺 , , 一 一 爪尸“ 亡 , 二乞 尹 ￡ 亡乞。二 , , 一 一 · 【 」 , , 叭 ,’」 ’ ’ , 、 , , , 一 【 一 · 一 ’ · , , , , , 一 , , , 一 · 【 一 , 一 、 ’ 玉 二亡 二乞 , , 一 , 。 夕, , 一 川 , 乃 几 乞 几 二 二艺。 , 一 , 夕吕 , , 一 【 」 一 , , , , , , 一 」 一 , , 【 」 , 、’ , 【 」 , 一 , , , 一 【 〕 一 , 、 , , 一 , 。坛。夕, , 一 【 一 , , 尸 夕‘夕月 , , , 一 【 〕 , 。 , 、亡 、 , , 一 【 〕 , 二 亡 坛。 , , 一 期 高小山 数学机械化进展综述 【 」 叭 一 , , 叮 , 一 , 罗 , , , 一 【 、 , , 一 【 」 一 , 肠 , , , 一 【 」 饭。。 。 。 , 夕 。二 二 , , 一 【 』 肠 罗 牡 几乞几 , , 一 」 牙 勺。 刀王 乞。。 , , 一 〕 一 夕。 葱。几 , , 于 」 一 韶 艺。 。。 乞 , , 一 二 记 。乞夕。 , , 一 【 」 , 饭 。 云 八 , , 一 一 罗 。。 , 亡 , , , , 至卜 」 叭了 , , , 合 , , , 【 , 一 ”又 记 夕几 , 【 」 二 、 。 , , 一 【 」 认飞 ‘ 泛 ‘。 , , 一 【 』 , , 叩 二二 , , 一 【 」 , , , , , 一 【 』 仔 , , , , , 一 , 一 即。 ‘ 尸。 ￡。 , , 一 【 」 , , , , , 一 即 , 诉 之几 ‘夕 , , 一 【 』 , 口 , , 、’ , , 一 〕 一 , ”, , , , , 一 , , 」 场 一 一 二 , , 一 〕 , 二 ‘ 坛 , , 一 【 」 , , 数 学 进 展 卷 〕 , ’ , 、 , , 、’ , , 一 【 』 , 尸尸 人 , , 一 【 』 尽 · · · 印 , , 一 【 」 , , 【 , 召。几之几夕, , 一 一 二 二 , 。 乞几 , , 一 【 」 · ‘ ” 犷瓦 爬艺‘ 夕 坛 , , 于 【 。。 几了口 认 扭 , 与 乏‘ 一 【 」 · 一 , 、 · , 。· ￡ · , 爪饭 “ 乞 , , 一 〕 ’ , , , , , , , 一 刁 ’ , , , , , , 一 【 」 一 · 夕 ” 李〕 乞。几 , 认了 , , 乞 , , 一 · 」 · , , 」 一 一 · 一 , , 一 【 」 乞。二 、二 饭二 , , 一 【 ’ , , , 一 【 」 认认 · 肠 一 一 · , 亡 二 饭 二 , , 」 韶 。。 , , 性 【 」 , 一 · 、 」, , · 一 , , , , , 一 【 【 」 〕 』 〕 【 」 【 肠 , , 一 ’ , 爪 云 ,刀夕。 才 , , 补 认飞 几 , 。 坛。 、 , , 一 依 , · 价 丑砚 , 爪 , , 一 、 几 , , 一 , , 兮 , , , , , , 一 , , 一 一 , , , , , 一 【 〕 · 夕 乞 亡 乞。几 , , 一 期 高小山 数学机械化进展综述 【 』 , , , 、乞 , 【 , 、 韶 一 一 一 夕 , , 【 」 , 二 乞 。 , , 〕认 夕。 二 , , 一 【、 』 , , , 白 , , , , , , 一 【认子 白 , 饰乞 呷 、 乞 , , 一 【 」 , 、 , , , , , , 一 , , 【 」 、 七 、 乞 乞 , , , 一 」 认七 ’ , , 一 , , , , 」叭厂 句 几 , , 一 一 一 。夕, , 一 【 』 ’ , 」 ’ 泛。 , 代 , 亡八 , , 一 【 』 ‘ 乞 二 , , , 一 【 认 认飞 一 一 几 从几 , , 认、 一 位 , , , 、丫 , , , 」、丫 认飞 一 位 一