（计算数学专业论文）面向几何对象语言的设计与实施.pdf

摘要 本学位论文主要介绍一种用于符号几何计算、几何推理以及视化几何 对象的面向几何对缘语言的设计与实施这种语言允许用确定的数据或刁i 确 定的符号来构造平面或其它几伺空间中的对象对构造的几何对象，可以容 易地作出如重命名变元、改变参数值等修改，还可以有效地对它们进行基本 运算和计算陈述它们之间的相互关系并用一种合理的结构来表示这些关系 通过构造的对象以及相互之间的关系，通常的几何问题可以用一种特定的规 则来描述、进而用高等的方法验证或者证明根据这种语言实现的系统允许 用户进行严格精确的几何计算和推理、证明和发现几何定理、自动生成静 态或动态几何图形以及交互式的文档， 在这种语言中，我们采用一种情形区分技术来形式化描述符号几何对象 和几何关系该技术允许遍历所有可能情形来构造和操作几何对象、进行几 何计算和推理基于该技术，本文引入两个重要的概念嗄合几何对象和复合 几何关系情形区分技术把处理符号几何对象的不确定肚和退化情形转化为 处理包含在复合对象和复合关系中边条件的问题进而推广到几伺约束处理 问题本文对该问题在约束化简、检查相容性、关系推导等方面进行了讨论 并给出些特殊的处理方法 本文围绕着这种面向几何对象语言的设计和实现展开首先本文的主 体给出有关几何计算和推理方法的综述，简单介绍几何定理机器证明发展的 情况和些常用的方法及相关软件包然后，本文详细介绍用情形区分技术 描述几何对象和关系的方法，描述这种语言所期望具有的基本功能和整体设 计思想、所包含的主要组成部分及各部分的基本功能，并给出一个基于上述 设计思想的具体实施过程，包括语言的选择、实现的模块和主要的数据结构 等进而，本文从理论上讨论几何约束处理问题给出一些特殊的方法和策 略、并一种动态求解包含不等式的几何约束问题的方法以及自动生成动态图 形的过程最后，总结全文，列举一些尚未解决的问题、如知识处理、半代数 集求解和保持几何性等 a b s t r a c t t h i st h e s i sp r e s e n t st h ed e s i g na i 】( 1i l n p l e n l e n t a t i ( ) no fag e o u i e t r i e o bi e c t o r i e n t e dl a n g u a g ef o rs y m b o l i cg e o m e t r i cc o m p u t a t i o n ，r e a s o n i n g ，a n dv i s u a l i z a t i o nt h i sl a n g u a g ea l l o w su s e r st oc o n s t r u c tg e o m e t r i co b ) e e t si np l a n e g e o m e t r yo ro t h e rg e o m e t r ys p a c e sw i t hc e r t a i no ru n c e r t a i nd a t a i nt m s l a n g n a g e ，u s e r sc a ne a s i l ym o d i f yt i l ec o n s t m i c t e do b j e c t ss u c ha sh yr e u a i n i n g v a r i a b l e ss l i dc h a n g i n gv a l u e so fp a r a m e t e r s ，e f f e c t i v e l yp e r f o r n lo p e r a t i o n s a i l dc a l c u l a t i o n s ( i nt h e m ，a n dd e c l a r er e l a t i o n sa n l o n gt h c n lm l ( 1r ) i n t n l a t e s i i c hr e l a t i o n sw i t hap r o p e rs t r u e t , u r ew i t ht h ec o n s t r u c t e do b j e e t ss l i d t h e i rr e l a t i o n s g e o m e t r i cp r o b l e m sc a nb ef o i n m l a t e dw i t hs p e c i f i e ds y n t a x ， a n ( 1t h e nt h e yc , a r l1 ) 、v e r i f i e ( 1o rp r o v e r lw i t ha d v a r i c e dt e c h n i q u e s as y s t e m i m p l e m e n t e do i lt h eb a s i so ft h i sl a n g u a g cw i l la l l o wt h eu s e rt , op e t f o r mg e e l i l e t l i ee o m p u t a t ；i o na l l dr e a s o n i n gr i g o r o u s l yt op r o v ea 1 1 ( jd i s c o v e rg e o n i e t r i e t l l e o r e i l l s a l l dg e n e r a l ( ? s t a t i c o rd y n a u f i eg e o n l e t i i cd i a g r a m sa n di n t e r a c t i v e d o e l l i u e n t sa u t o l n a t i e a l l y i nt h i sl a n g u a g e w ea d o p tac a s ed i s t i n c t i o nt e e h i i i q n ef ( j r f o r m a l i z i n g s y m b o l i cg e o i n e t r i eo b j e c t sa n dr e l a t i o n s t h i st e c l m i q u ca l l o w sl l s e r st oc o i l s t r u c ta n dn i a n i p l d a t eg e o r r i e t r i co t ) j e c t sa n dp e r f o r u ig e o m e t r i cc o m p u t a t i o n s a n dr o e s o n i n gb ye n u m e r a t i n ga l lp o s s i b l ed i s t i n c tc a s e s b a s c do nt h et e c h n i q u e ，t w oi m p o r t a n tc o n c e l ) t s c o m p o s e dg e o m e t t i co b j e c t sa n dc o m p o s e d g e o m e t r i cr e l a t i o n s ，a , r ei n t r o d u c e d t h ec a s ed i s t i n c t i o nl e e h n i q u er e d u c e s t h ep r o b l e mo fh a n d l i n gu n e e i t a i n t ya n dd e g e n e r a c yt ot h a to fm a n i p u l a t i n g c o m p l i e a t e ds i d ec o n d i t i o n si n v o l v e di l lc o m p o s e dg e o i n e t r i co b j e c t sa n dr e l a t i o n s ，a n dt h e nt ot h ep r o b l e mo fc o n s t r a i n th a n d l i n gi nt h i st h e s i s ，w ei n t r o d u c es o l l l ( s p e c i a lt e c h n i q u e sa n ds t r a t e g i e st b rg e o m e t r i cc o n s t r a i n th a n d l i n g ： r e p r e s e n t a t i o n ，s i m p l i f i c a t i o n ，c o n s i s t e n c yc h e c k i n g ，a n dr e l a t i o nd e r i v a t i o n t h i st h e s i sm a i n l yd i s c u s s e st h ed e s i g na n di m p l e m e n t a t i o no ft h ep l o p o s e dl a n g u a g e i t , f i r s tg i v e sas u r v e yo ng e o m e t r i cc o n l p n t a t i o na n dr e a s o n i n g ，i np a r t i c u l a rt h ed e v e l o p m e n to fg e o m e t r i ct h e o r e n li ) i e y i n g ：a n dr e v i e w s s o m eo ft i l ei m p o r t a n tm e t h o d sa n ds o f t w a r ep a c k s g e s t h e nt h et h e s i sd e - 中国科学技术大学博士学位论文 t a i l st h ef o r m a l i s mo fc a s ed i s t i n c t i o nb yd e f i n i n gc 0 1 1 1 p ( ) s o dg e o m e t r i co b j c , - l s a n f lr e l a t i m i s p r e s e n t st h ee x p e c t e dc a p a b i l i t i e sa n do v e r a l ld e s i g no ft h i sl a n g u a g ea n di t sn l a i nc o m p o n e n t sa n ( if l m c t i o n a l i t i e so fe a c hc o m p o n e n t s o m e i m p m n e n t a t i o ni s s u e sa r ca ! t d r c s s e db a s e d0 1 1t h ed e s i g ni n c l u d i n gs e l e c t i o no f p r o g r a m m i n gl a n g u a g e m o d e l so fi m p l e m e n t a t i o n ) a n ds o m em a i nd a t as t r u t t l l r ea f t e r 。t h a t s e i n ep r o b l e m sa b e l i tc o n s t r a i n t sh a m t l i n ga r ed i s c u s s e d 、a l l ( ：l as p e c i a l i z e da p p r o a c hi si n t r o d u c e dt os o l v eg e o m e t r i cc o n s t r a i n t si n v o l v i n g a l g e b r a i ci n e q u a l i t i e sd y n a m i c t f l l ya n dt h ep r o c e s si sp r e s e n t e dt og e n e r a t e d y n a n f i cg e o m e r i ed i a g r a m sa u t o m a t i c a l l y t h et h e s i si sc o n c l u d e dw i t ha s i l l n l l l a l l _ ya n dab t 。i o fd i s c u s s i o no ns o m ep r o b l e m se n e o l m t e r ( 蝴b u tn o tc o i i i p l e t e l ys c t d e ds l l c ha sm a n a g i n gg c o m e t r i ek n o w l e d g e ，s o l v i n gs e m i a l g e b r a i c s y s t e m s f t l l dk e e p i n gt h el a n g u a g em o r eg e o m e t l i e 中国科学技术大学学位论文相关声明 本人声明所呈交的学位论文，是本人在导师指导下进行研究工作 所取得的成果。除已特别加以标注和致谢的地方外，论文中不包含任 何他人已经发表或撰写过的研究成果。与我一同工作的同志对本研究 所做的贡献均已在论文中作了明确的说明。 本人授权中国科学技术大学拥有学位论文的部分使用权，即：学 校有权按有关规定向国家有关部门或机构送交论文的复印件和电子 版，允许论文被查阅和借阅，可以将学位论文编入有关数据库进行检 索，可以采用影印、缩印或扫描等复制手段保存、汇编学位论文。 保密的学位论文在解密后也遵守此规定。 作者签名：互狲 夕钐 年月r 日 1 1 选题动机 第一章引言 几何学是数学中最为经典和基础的学科之一，其中包含的知识和处理问 题的方法为建立现实世界以及其中物体的抽象模型并理解现实世界提供了 重要的依据，这使得几何学得到了广泛的研究和发展，到现在仍然是数学研 究领域中一个重要的分支几何学从起源到发展成为一门具有不同分支的学 科的过程中，有着不同的方式、方法和途径，其中相对重要的一个就是公理 化思想在经典名著几何原本中，e u c l i d 提出了为几何建立一个公理体 系，并以此作为演绎推理的依据的思想后来，h i l b c r t 在e u c l i d 工作的的基础 上建立了一个完整的公理系统f 2 6 1 ，使得通常的欧几里锝几蚵有了一个严实 的基础该公理系统以一些不必要给以定义的基本概念为主要讨论目标这 些基本概念被分为两类一一基本对象( 点、线面) 和对象间的基本关系，它 们满足若干公理，并作为逻辑推理的出发点h i l b e r t 完成的公理系统促进了 几何学的发展，为通常的几何推理提供了重要的依据，更为重要的是它为现 代的数学推理建立了一个公理化的模型 然而，在几何定理机器证明的基本原理( 初等几何部分) f 7 9 1 一书中， 吴文俊先生首先指出h i l b e r t 的公理化体系远远不够严格，而且建立一个与 h i l b e r t 的公理化方法类似的，能严格而准确描述几何问题的公理化体系是 非常困难，甚至是不可能的；即使建立了一个严密的公理系统作为一切几何 构造、描述和推理的依据，欧氏几何中的问题和推理方法仍然不可能达到逻 辑上的绝对严密出现这样问题的症结在于：在通常的几何关系、公理和定 理的叙述中都隐含地假设了所考虑的几何构型都处于某种正常的、一般的 的位置，而非带有特殊性的退化情形例如，说到两条直线平行时，就隐含着 它们不会重合为一条直线；当说两条直线相交时也隐含地假设了这两条直线 不会重合又如考虑一个三角形，通常都隐含地假设了这个三角型不会退化 为一条直线，否则后如求垂心，外接圆等等与之相关的几何操作将无法进行， 从而与这个三角型相关的几何定理和推论等将出现错误或变得没有意义因 第一章引言中国科学技术大学博士学位论文 此，吴指出通常几何中的几乎所有定理只能说是一般性成立，或者说仅在某 些非退化备件下成立 退化情形和非退化条件并没有引起经典几何学家太多的注意，这也许是 因为在经典的几何传统中退化情形通常作为一种特殊或者平凡的情形而被 忽略随着计算机的出现和发展，越来越多的几何工作者希望通过计算杌来 进行几何研究然而，当我们考虑如何在计算机上来表示和操作几何对象， 进行几何计算和推理时，我们不得不去面对那些特殊的情形由于计算机无 法预知并处理那些隐含的假设，本来在传统意义下恒正确的几何命题可能在 某些情形下出现错误这时，为了确保关于几何对象的计算和操作的正确、 严格，所有的退化情形都应很好地被处理随着人们对几何计算和推理方法 的深入研究，退化情形以及非退化条件的重要性在几何推理研究领域得到了 广泛的认知，很多几何工作者在设计和实施几何定理证明方法时加入了处理 f 收集、分析，翻译等) 非退化条件的功能模块，出现了很多可以处理退化情 形的推理方法( 见f 9 ，3 8 ，4 0 ，6 l ，7 9 1 等文献) - 基于不断发展的计算机技术和推理方法，很多学者开发了不同的几何软 件或工具包，如c a b r i 、c i n d e r e l l a 、g e x 、g e o t h e r 、超级画板等通过 这类软件，用户不仅可以进行如几何作图、几何量计算等基本的几何操作， 而且还能进行如几何定理自动证明，几何约束求解、生成动态几何图形等 复杂操作尽管这些已有的方法、工具和软件为几何研究和教育提供了有力 的支持和帮助，但是对计算机辅助几何的基础的研究还很少在现有的软件 和工具中，对几何对象以及相互关系的表示和描述各自拥有自己的一套方法， 而没有统一的形式，这种情况必然导致新的几何软件设计和实施不得不重复 前人的工作，造成不必要的浪费此外，由于通常考虑的几何对象都是不确定 的或者说是符号的，比如说考虑一个圆，这个圆就是一个一般的圆，它的圆心 和半径可能不是具体的数值而是不确定的符号，如何合理地表示这样的不确 定符号对象、描述相互关系、进行精确的计算和严格的形式推理等都是我 们关心的问题 为了能更好地使用计算机有效，严格、准确地辅助几何研究和教学，我 们迫切需要开发一_ 种综合性的形式化语言来描述，表示、视化和操作符号 几何对象和几何关系。进而能在不确定性和退化情形存在的情况下有效且正 确地对这些对象以及相互关系进行精确的计算和形式化的推理这样的一种 2 中国科学技术大学博士学位论文1 2 研发现状 语言应该还能够表示和处理几何事实、公理、定理、历史背景等诸如此类 的几何知识，并利用它们产生交互式文档、图形、网页等基于这种形式化 语言的软件系统除了可以用于辅助几何研究和教育外，还应该能够应用到现 代几何相关的众多领域如计算机辅助几何设计、几何建模、计算机视觉以 及计算机图形学等 基于以上动机，我们设计了文中所述的用于几何计算、推理以及视化的 面向几何对象语言( g e o m e t r i c o b j e c t o r i c n t c dl a n g u a g e ) ，文中用该语言 的英文单词首字母g m l 来指代这种面向几何对象语言通过对这种语言设计 与实施的叙述，本文将给出一种形式化描述几何对象和关系的一般方式并介 绍了处理不确定性以及退化情形的相关技术 1 2 研发现状 g l 是面向几何对象的，可以进行几何计算和推理以及视化几何对象和 相互之间的关系这种语言的中心元素是符号几何对象，准确，严格、有效 地构造和操作这样的对象、对它们进行基本几何运算、探索不同对象间的 关系、生成对象和几何关系的图形是这种语言研究的一些重点问题 处理符号几何对象的主要困难在于由符号引入的不确定性以及可能的 退化情形，如何设计并开发有效的方法来处理它们是设计这种语言时必须解 决的一个主要问题本文中，我们采用了一种情形区分的技术来处理不确定 性和退化情形这种技术允许遍历构造和操作过程中所有可能出现的不同情 形来形式化描述符号几何对象、几何关系、几和计算和推理等通过这种描 述，符号几何对象通常伴随着类型以及与该类型对应的边条件给出，表示该 对象在边条件成立的情况下始终具有指定的类型，这样每一个几何对象都严 格地界定了类型而不会退化到别的类型从一组给定的符号几何对象我们可 以用与定义分段函数类似的方法来定义这些对象的一个复合几何对象，它的 每一个分支具有特定的类型以及相应的边条件复合几何对象通常是几何运 算等操作的返回结果类似地，由几何对象问相互关系我们可以定义复合几 何对象间的复合几何关系 情形区分技术把处理不确定的符号对象的问题转化为处理各种各样包 含在复合几何对象和符合几何关系中的边条件的问题，它与几何对象间相互 3 第一章引言中国科学技术大学博士学位论文 关系以及相关假设组成了g m l 中的几何约束：对它们的求解是几何研究领域 中非常重要的一个分支很多几何学者对这类问题作了广泛的研究，设计和 开发了一些有效的方法，如基于图形的方法、代数方法、数值计算方法以及 逻辑方法等( 请参阅f 3 0 ，2 9 1 ) ，然而这些已有的方法主要是为求解那些代数表 示只包含等式的约束问题而设计的g l 中的边条件、几何关系和假设的代 数表示通常既包含等式也包含不等式尽管有些方法，如柱形代数分解，可 以处理这样的不等式约束，然而直接把这些方法应用到几何问题中的效率比 较低( 根据我们所作的一些简单实验) 此外，边条件的引入导致g l 中的几 何问题通常包含很多的几何约束，这无疑给本就复杂的几何计算带来更大困 难，然而在实际中，很多几何约束代数表示相对都很简单，而且有时不同表示 的约束可能具有相同的意思，甚至有些约束可能是其它几何约束的直接推论 为此对于一个几何问题，我们通常采用如下渐进的方法：先对几何问题中的 几何约束集合进行预处理，然后用三角列等方法处理等式约束，最后用c a d 等方法来处理不等式 此外，对上述包含等式和不等式的几何约束还有一种动态求解的方式： 生成满足约束条件的动态图形这种方法的个主要问题是如何高效地求得 给定的约束集的实数解，为此我们提出了半代数系统的解的根式表示的概念 和具体的求解方法它的主要思想是将约束集合的实数解用显式的根式表示 出来，这在通常来说是不可能的( a b e l g a l s i s 理论) ，然而通常的( 特别是平面 几何中的) 几何约束通常只包含次数较低的等式，这使得我们能够求得根式 表示的实数解 基于以上处理几何对象以及约束的理论方法，g c o l 的设计与实施变得相 对简单首先，我们为它选择一个基本的语言模型由于几何对象本身具有严 格的类型，这与面向对象语言中的类的概念一致，而几何又具有很强的等级 属性，这使得我们很自然地选择一般的面向对象语言作为g o a l 的基本模型 通过这种模型可以很容易地表示( 复合) 几何对象以及几何关系，从而为g l 的设计和实施带来了很大方便 有了基本模型，我们的设计和实施过程遵循软件设计中的基本过程：需 求分析、系统设计、程序设计首先我们详细地研究并规划了这种面向几何 对象语言所应该具有的功能，并根据这些功能将g o o l 进行模块化，建立总体 设计框架：然后对每一模块继续细化后给出具体功能描述、包含的主要元素 4 中国科学技术大学博士学位论文 12 研发现状 或模块以及相互关系，确定主要的数据结构和数据流程；综合每一模块，完成 设计，付诸实施 设计和实施这样一种语言是一个长期的过程，需要投入很多的时间和人 力来完善设计和完全实施所应有的功能我们已建立了g c o l 整体框架，明确 地规划了所包含的主要部分及各部分的具体功能设计了描述和表示一般几 何对象的结构和方法，并设计和实施一些特殊的化简几何约束，检查约束相 容性等处理约束的策略和方法此外，我仍还实照了一种具有一般性( 不依赖 g w l ) 的动态约束求解方法，该方法可以将给定的约束集合分解为有限多个 解的根式表示，进而用这些显式表示生成动态图形，获得了很好的结果 为了测试我们设计的思想和提出的策略。我们为g c o l 实施了一个测试版 本，在这个版本中，我们实现了有关符号计算的整数、有理数，多项式、代 数表达式、逻辑表达式等的表示和基本运算和操作方法，建立了表示几何对 象以及它们之间承继关系的各种类，给出了描述几何约束的类似三元组的数 据结构，并提供了一个基本的图形用户界面和简单的命令解释器以及其它一 些常用的工具类包 尽管花费了很多努力，该测试版本的功能仍然很基础，现将它目前具有 的基本功能罗列如下 通过确定或不确定的数据构造欧式平面几何中的凡何对象，如点、直 线、圆、三角形，线段等，构造之前先验证给定数据( 及其它数据) 是 否会使对象退化； 可以修改构造的几何对象的参数值，添加有关对象或其子对象和派生 对象的假设，陈述对象间的关系，并检测所作修改和陈述的相容性i 对构造的几何对象进行基本运算，如求对象间交点、验证对象是否相 切、平行、垂直等；以及简单计算，如求周长、距离、面积等； 通过构造的几何对象以及陈述的关系和假设，通常的几何命题可被形 式化地描述，进而用几何计算和推理的方法证明； 几何约束可以化简并正规化，并通过给定的对象以及相互关系推导对 象问的其它关系： 动态几何约束求解，给定一组满足某些约束的对象，( 自动) 生成满足这 些约束的动态几何图形 5 第一章引言 中国科学技术大学博士学位论文 1 3 论文结构 本论文所述工作的基本思想来自于导师王东明教授，笔者对这些思想进 行细化以完成设计，并根据所作设计对g m l 进行了实施文中给出的表示几 何对象的结构以及为处理不确定性和退化情形而引入的情形区分技术是我 们工作的新意所在，它们为设计和实施可靠的、功能强大的以符号对象为中 心的、能严格准确地进行符号几何计算和推理的几何软件提供了有效的方 法此外，文中给出的动态求解包含不等式约束问题的方法为含有低次数等 式的半代数集求解以及自动生成几何图形等工作提供了重要的理论依据 本文的内容以对这种语言的设计和实施为主体，穿插一些有关几何计算 和推理方法的介绍以及几何约束处理的内容值得说明的是，本文对设计和 实施的叙述并没有完全遵循一般软件设计的描述方法，而是使用了更容易理 解的叙述方法，而且本文的重点在于试图给出计算机辅助几何基础的研究方 法，所以文中并没有讲述太多的计算算法和理论，论文的具体组织结构安排 如下 本文的第二章是对几何计算和推理方法的一个综述可以看作后续章节 所需内容的基础知识首先我们回顾几何机械化的历史、列举一些常用的几 何计算和推理方法，然后概述坐标法和非坐标法中的一些常用的方法如吴方 法、g r 6 b n e r 基方法、面积法、c l i f f o r d 代数法等，进而介绍一些常用的几何 计算和推理的工具和软件包及一些动态几何软件，最后列举几何计算和推理 进一步研究中的一些问题 第三章是g c o l 的设计部分首先介绍g c o l 的一些语言特征一一面向对 象、解释性、专用性，然后详细地给出g 1 应该具有的功能和特点以及所包 含的主要组成部分：核心、构造器、修改器，运算器、描述器、推理器和 视化器，进而分节介绍这些组成部分的功能，给出一些函子的描述，讨论设计 各组成部分时可能出现的的问题、以及在实现和几何计算中的困难， 第四章为g c o l 的实施部分，主要阐述在实现这种语言实现过程中面l 临的 一些基本问题和相应的解决方法我们把g l 的实现分为三个主要的块：符 号块( 处理与符号相关的整数、有理数、一般符号、以及符号对应的多项式 表示和运算等) 、对象块( 实现g c o l 中不同几何对象的表示以及相互的继承关 6 中国科学技术大学博士学位论文1 3 论文结构 系) 、以及约束块( 讨论几何约束的表示、相互之间的转化等等) 基于以上 的三大模块，我们介绍实现中的若干细节问题，如多项式的表示、约束的数 据结构、逻辑表达式、代数表达式，用户界面等等 第五章阐述了g l 中约束处理这一章首先给出约束化简的目标和简单 过程，然后介绍一种融合三角列方法和柱形代数分解方法的过程来检查约束 相容性，进而讲述g 1 中经常用到的对象搜索和约束集合建立的具体过程， 最后，通过给出具体的几何实例来展示这种g c o l 的基本应用 第六章是一个可以独立出来的章节，主要讨论包含不等式的几何约束的 动态求解问题首先我们给出半代数系统解的根式表示的定义，然后介绍将 给定半代数系统分解为有限多个显式解的方法，进而给出自动生成满足给定 约束的动态几何图形的过程，最后通过两个代表性的实例来展示该方法的有 效性和具体过程 最后，我们对本文做一个简单的总结介绍工作中的困难所在，列举具有 代表性的尚未解决的问题，如半代数集处理、几何知识管理以及保持几何性 等，这些问题是进一步研究工作的重点 本文第三章、第四章和第五章的内容基于作者与王东明教授合作的论 文f 4 8 ，4 9 ，5 0 】，而第六章的部分内容是作者与h o o nh o n g 教授、王东明教授 以及李丽赞女士合作的结果f 2 8 1 7 第二章几何计算和推理 几何定理的机械化证明是自动推理和符号计算领域最活跃的分支之一， 以吴方法为代表的符号几何计算和推理方法是在计算机上证明和发现几何 定理，解决各种几何问题的有效工具在这一章中我们首先通过介绍几何 定理机械化证明的历史来简要地回顾一下几何计算和推理的历史和发展然 后概述现有的一些常用方法，如吴方法、g r s b n c r 基方法、结式消元等基于 坐标的方法和面积法、括号代数法、c l i f f o r d 代数法等非基于坐标的方法 本章可以看作是本文后面所需要的基础知识的简要介绍，因此内容并未涵盖 关于几何计算和推理的所有内容，感兴趣的读者可以参阅f 8 ，6 3 ，6 7 ，7 9 ，8 3 】 以及那里的众多文献本章的写作主要参照了文献【8 ，6 3 1 2 1 历史背景 几何定理机械化证明的思想可以追溯到十七世纪的r d e s c a r t c s 和g w l c i b n i z 时代前者创立了解析几何，在空间形式和数量关系之间建立了重 要的联系，从而实现了几何问题的代数化，为定理证明的代数方法打下了坚 实的基础；后者通过研究逻辑，促进了布尔代数数理逻辑等以及计算机科 学的研究，为定理证明的逻辑方法作出了重要贡献然而，吴文俊先生指出 f 7 9 1 ，对几何机械化最早作出理论贡献的人之一是h i l b c r t ，在他的经典名著 几何基础f 26 1 中，h i l b c r t 提出了一条可以对一类纯粹的交点定理进行判 定的定理，该定理指明了实现机械化目标的道路，该书也是几何机械化的代 表吴根据h i l b c r t 方法的机械化特征，将该定理重新陈述如下： h i l b e r t 机械化定理平面上构造型纯交点定理的h i l b c r t 类是可以机城 化的， 另一方面t a r s k i 在1 9 5 0 年建立了一个用来对初等几何和初等代数范围的命 题进行机械化判定的一般性方法，得到了如下著名的结论： t a r s k i 机械化定理通常意义下的初等几何是可以机械化的 9 第二章计算和推理 中国科学技术大学博士学位论文 但是该方法由于复杂度太高以至于到现在也没有在计算机上实现 几何定理机器证明获得突破性进展要归功于吴的工作1 7 5 】，他在古代数 学机械化和代数化思想的启发下提出了自己的机械化方法一一吴方法吴 方法为几何定理机器证明找到了一条切实可行的方法，从而推动了几何计算 和推理的发展吴的工作引起了自动推理届学者的极大兴趣，很多国外学着 通过 8 0 】等文章了解到吴的工作后纷纷开始学习，研究并改进了吴的方法， 出现了很多基于该方法的改进算法和基于这些算法的几何定理证明器，如 f 2 3 ，3 6 ，7 l ，7 2 ) 后来，人们发现吴方法中所用的代数方法可以通过r i t t 的方 法f 5 8 1 来建立，所以这个方法在代数上被称为吴一r i t t 特征列方法 吴方法的成功使得几何定理机器证明这个曾被深入研究但当时停滞不 前的分支再度活跃，大量的学术论著相继出现很多研究人员尝试着把已有 的处理代数问题的方法应用到几何推理中，并开始探索新的方法来进行几 何计算和推理g r s b n c r 基就是其中一例，1 9 8 5 - - 1 9 8 6 年问出现了一些使用 g r 6 b n e r 基来进行几何自动推理的论文f 1 5 ，3 3 ，4 0 ，4 1 】其它的被应用到几何 自动推理中的消元方法还有结式方法【9 0 ，9 l 】、数值例证法【9 5 】、计算最大公 因子方法 3 1 、d i x i o n 结式方法 3 4 等 值得注意的是吴方法以及g r s b n e r 基方法只能处理只包含等式的定理 对于不等式型定理的证明，数学家们也开始探索新的方法来处理这样的问题 一个重要的工作就是c o l l i n s 改进了t a r s k i 的判定方法，提出了柱形代数分 解( c a d ) 的方法，该方法到现在仍然是t a r s k i 类型问题求解的一般性方法 后来，c o l l i n s 和h o n g 进一步改进了c a d 方法【1 6 1 ，提出了部分c a d 的方法， 提高了计算的效率，使得该方法在很多领域中有了更广泛的应用同时，很多 学者设计出了一些高效的特殊方法，如基于特征列和c a d 的混合方法【5 1 】、 基于量词消去的方法【1 9 】等杨路等专家学者提出了一个完备判别式理论 f 9 1 】来对多项式进行实根分离，并开发了一个不等式证明器，用它来证明超过 一千个有意义的几何不等式，而且发现了很多新的不等式 8 4 ，8 7 ，8 9 1 前面所述的方法面向的都是吴意义上的初等几何，没有涉及到微分运 算事实上，特征列方法经过推广后还可以应用到微分多项式上，进而用来证 明微分几何中的定理 7 6 1 吴推广了他的方法并将它应用到空间曲线理论中 s l l ，证明了很多空间曲线理论中非平凡的定理此外，人们还探索新的方法 来证明微分几何中的问题如计算零点集合维数的方法 3 l 、s e i d c n b c r g 消去 1 0 中国科学技术大学博士学位论文2 2 坐标法 理论f 6 2 1 向量计算( v e c t o rc a l c u l a t i o n ) 1 4 s 关于吴方法在微分几何定理证 明中的工作还有6 ，7 ，8 2 1 上面的所有方法( 习惯性地称为坐标法) 都有一个共性：经过坐标化后 把几何属性转化为代数方程组然后用代数的方法来求解但是很多工作者 一直相信可以找到一种基于向量的方法对几何定理进行证明，因为这样的方 法可以产生出漂亮的、甚至是可读的证明这方面的工作开始与上世纪8 0 中期，到9 0 年代出就已经有了几个成功的基于向量的方法：面积法【6 】 括号 代数法f 55 j 和c l i f f o r d 代数法1 2 2 ，4 3 4 5 ，4 6 ，6 4 】等这些方法( 通常称为非坐 标法) 生成的证明通常比上述坐标法生成的简短在非坐标法中只有面积方 法用的是纯粹的几何不变量如面积、比例等，它的主要优点证明中的每一步 都有明确的几何意义，可以被用户理解即证明是可读的 几何计算和推理方法有着非常广泛的应用，如机器人运动分析、联动装 置设计、计算机视觉、智能计算机辅助设计，智能计算机辅助教学，几何 建模、计算机辅助几何设计等等基于上面提到的方法，人们设计并实现了 一些用于进行符号计算几何研究( 如计算、推理等) 和教育的几何软件系统 如g e o m e t r ye x p e r tf 2 4 1 ，g e o t h e r1 6 8 l 等 2 2 坐标法 坐标法的一个根本思想是几何问题的代数化：引进坐标，把几何命题的 叙述用代数方程的形式重新表达，进而把证明问题转化为判定假设的代数方 程是否能推出结论的代数方程这类方法把通常几何证明中质的困难转化 为量的复杂，而且使整个推理更加严密这- - d , 节我们将简要介绍一些常见 的、应用比较广泛的基于坐标的方法 对于通常的几何定理，选取适当的坐标后，如果其中的假设条件可以表 示为一组代数方程： 噩 1 1 ( 2 - 1 ) o 0 0 i | = = 、 n n h o z z ， ， ， $ z z 肌也 以 ，ill-_j(1_l-i【 茎三兰生差塑垄垄里型兰垫查查兰堡主兰竺丝壅 而定理的结论由代数方程 c ( z l ，靠) = 0 给出其中h l ，峨和e 都是以z t ，的多项式，那么几何定理的证 明可以归结为如下研究代数方程之间的问题 问题构造并提供一种确定的算法，使得依此算法进行有限步之后即可 判定：在若干附加条件下是否有h l = 0 ，一，也= 0 蕴舍c = 0 ；如果能判定， 则原定理一般性地成立 2 2 1 吴方法 吴改进了r i t t 的特征列的概念和方法，设计了计算任意多项式组的特征 列算法，发展出一套关于特征列的理论，从而给出了上述问题的一个完满解 答我们首先简要介绍一下特征列的有关概念和结果 设| c 为特征为0 的域，为瓦上以z = ( x l ，o 。) 为变元的多项式 环我们将变元刃排成固定的次序茹1 - 4 ( z 。对任意非常数多项式p ，我 们称p 对x 。的次数大于0 的最大下标p 为p 的类，记为c t s ( p ) ；称为多项 式p 的导元，记为l v ( p ) ；称p 对z p 的次数为导次数，记为l d e g ( p ) ；p 对唧 最高次项的系数l c ( p ) 为p 的初式，记为i a i ( p ) 定义2 1 _ j c 【霉1 中非常数多项式组成的有限非空有序集合 面= i n ，t 2 ，乃】 称为三角列，如果 c l s ( t 1 _ ) c l s ( t 2 ) c l s ( 露) 可将任意一个三角列t 写成 t = 五0 - ， 疋( z l ， ，x p t ) ， ，1 ，t ，z m ) t , ( x l ，z p l ，z m ，) 1 2 正( t 正，1 ) ， ( 让，l ，f 2 ) z ( u ，l ，抛，y ，) 中国科学技术大学博士学位论文22 坐标法 其中0 p l 芦 n ，t = 茁( z m ，z 舢 ，且p i = c l s ( 正) ，y = ，i = 1 ，r 任意p 为一个多项式如果多项式尸的次数比任意z 的导 次数小，则称p 对面是约化的 定义2 2 三角列t = i t , ，t 2 ，t r 】c 陋1 称为升列，如果对所有的 2 i r ，正对m ，耳一1 】都是约化的 我们把多项式r = p r e m ( p r e m ( p , t ) ，t t ) = 1 ，卵r p 一 ：。q 正简记为p r e m ( p , t ) ，并称其为p 对t 的伪余式对任意一组多 项式p ，p r e m ( p ，t ) 表示 p r e m ( p , t ) ip p 定义2 3 升列c 称为非空多项式组p c 的特征列，如果 c c ( p ) ，p r c m ( p ，c ) = o 令p ，q 为两组多项式，记z c r o ( p ) 为p 中所有多项式的公共零点集合，而 z e r o ( 吖q ) = z e r o ( 1 p ) u o qz e r o ( q ) 下面的结果刻画了给定多项式组与其 特征列之间的关系 命题2 1 设c = c 1 ，口】为多项式组pc 【z 】的特征列，且命 厶= i n i ( a ) ，峨= p u 厶，i = 1 ，r = i n i ( c ) = j ， 则 z e r o ( c i ) cz e r o ( p ) cz e r o ( c ) z e r o ( p ) = z e r o ( c i ) uu z o r 0 0 。) = l 在庀及足的任意扩域中成立 从上面命题中的后一个零点关系，我们继续求巩u c 的特征列，经过有 限步之后可以得到如下的零点分解， e z e r o ( ) = uz e r o ( c t u ( 2 - 2 ) l = i 其中每个c ；都是升列，而皿= i n k q ) 在吴方法中，把从给定多项式组驴 获取特征列c 的过程称为吴一r i t t 整序原理而把这一零点分解的算法称为 吴一r i t t 零点分解算法 1 3 第二章计算和推理 中国科学技术大学博士学位论文 定义2 4 设尼o = 瓦( u ) 为添加未定元札得到的扩域升列t ； 陬，矸】称为不可约升列，如果它满足如下条件： 乃作为。【l 】上的多项式为不可约的， 对t = 2 ，一，r ，设耽l 为多项式正一l ，m ，哺“玑一1 ) 在瓦l - 2 某扩 域上的零点并记丘。= 一2 ( 仉一1 ) 为尼t 一2 通过添加哺一l 所