（应用数学专业论文）mizar语言系统与四元数的代数结构.pdf

青岛科技大学研究牛学位论文 m i z a r 语言系统与四元数的代数结构 摘要 计算机证明数学问题是当今世界积极研究的一个热门领域。迄今为止，世界 已有多种可用来进行数学命题证明和逻辑推理的机器语言系统，但其中只有少数 几种语言可被普遍接受并受到数学家与计算机专家的认可，如h o l 、m i z a r 、p v s 、 c o q 等，它们各自的初衷不同，却有一个共同的特征：人类使用机器语言书写、 计算、逻辑推理和证明文本性质的数学问题，并由计算机自动验证其正确性。我 们这里讨论的m l z 盯系统是由波兰p l o c k 科学协会的a n d r z e jt r y b u l e c 教授领导下 开发的。经过近3 0 年的发展，m i z a r 系统已经形成了著名的数学知识处理的形式 化系统。在此系统下，完成了大量的数学问题的计算机证明。这些数学知识涵盖 了几乎数学的每一个分支，解决了人们用手无法计算和证明的一些复杂问题。同 时，它在自动控制、声音和图像识别等研究领域有着广泛的应用，为今后讨论数 学及其相关学科奠定了一个良好的基础。 本文首先介绍了m t z a r 系统的计算机操作原理和使用方法，给出了在m l z a r 语言系统下四元数、四元数的运算、共轭、内积、模等代数结构理论的证明，所 做结论都通过了m i z a r 系统的验证，发表在波兰的( f o r m a l i z e dm a t h e m a t i c s ) ) 杂 志上，并被收录到m m l ( m i z a rm a t h e m a t i c a ll i b r a r y ) 数据库中。 在此研究领域，作者在导师的指导下，在( f o r m a l i z e dm a t h e m a t i c s ) ) 杂志上 已发表了5 篇论文，详见网站h t t p ：w w w m i z a r , o r g f m 。 关键词：计算机数学问题m i z a r 系统四元数代数结构 竺! ! 竺堡童墨堕量四垄墼盟! ! 墼堕塑 m a i z a rp r o j e c ta n da l g e b r as t r u c t u r e o ft h eq u a t e r n i o nn u m b e r s a b s t r a c t u s ec o m p u t e rt op r o v em a t h e m a t i c a lp r o b l e mi sah o tf i e l dw h i c hm a n yc o u n t r i e s a r et a k i n ga c t i v ep a r ti nu m f ln o w , t h e r ea r em a n yk i n d so f m a c h i n el a n g u a g es y s t e m w h i c ha r eu s et op r o v em a t h e m a t i c a lt h e o r e m s ，a n ds e v e r a lo f t h e ma r er e c o g n i z e db y t h em a t h e m a t i c i a na n dc o m p u t e re x p e r t s ，s u c ha sh o i ，m t z a r , p v s ，c o qe t ct h e s p e c i f i cg o a l so ft h e s ep r o j e c t sv a r yh o w e v e r ，t h e yh a v eo d ec o m m o nf e a t u r e ：t h e h u m a nw r i t e sm a t h e m a t i c a lt e x t sa n dt h em a c h i n ev e r i f i e st h e i rc o r r e c t n e s s t h e p r o j e c tm l z a rs t a r t e d3 0y e a r sa g ou n d e rt h el e a d e r s h i po fa n d r z e jt r y b u l e c a tt h e p l o c ks c i e n t i f i cs o c i e t y , p o l a n ds i n c et h e n , h o w e v e r ，m i z a rt h ep r o c e s sh a se v o l v e d t oa p r o o f c h e c k e rw i t ht h el a r g e s tk n o w nr e p o s i t o r yo f f o r m a l l yv e r i f i e dm a t h e m a t i c a l k n o w l e d g ec o v e r i n gan u m b e ro ft o p i c s i ta l s oa p p l e si n m a n yf i e l d ss u c h a s a u t o c o n t r o l ，v o i c e ，i m a g ei d e n t i f i c a t i o ne t c ，a n ds e tag o o df o u n d a t i o nt om a t h e m a t i c s a n dt h er e l a t e dm a j o r i nt h i sp a p e r , w ed e s c r i b et h eh i s t o r yo fm i z a rs y s t e ma n dt h em e t h o dt oi i s ct h e m i z a rs y s t e mt h e nw eg i v et h ed e f i n i t i o no fq u a t e r n i o nn u m b e r s ，m o d u l e ，a l g e b r a s t r u c t r ee r e ，a n dt h e nw ep r o v ei t sp r o p e r t i e st h e yh a v eb e e nc h e c k e db ym i z a r s y s t e m ，p u b l i s h e di nt h ej o u r n a lo f f o r m a l i z e dm a t h e m a t i c s ) ) s y s t e m ，a n da c c e p t e d j n t o t h em m l i nt h i sf i e l d ih a v ep u b l i s h e d5a r t i c l e s i nt h ej o u r n a lo f f o r m a l i z e d m a t h e m a t i c s ) i nt h ei n s t r u c t i o no f m yt u t o r , p l e a s el o o ka tt h ep a g eo f 7 0 青岛科技大学研究牛学位论文 k e yw o r d s ：c o m p u t e rm a t h e m a t i c a lp r o b l e m sm i z a rp r o j e c tq u a t e r n i o nn u m b e r s a l g e b r as t r u c t u r e i i l m i z a r 语言系统与四元数的代数结构 独创性声明 本人声明所呈交的论文是我个人在导师指导f 进行的研究工作及取得的研 究成果。尽我所知，除了文中特别加以标注和致谢中所罗列的内容以外，论文中 不包含其他人已经发表或撰写过的研究成果，也不包含本人己用于其他学位申请 的论文或成果。与我一同工作的同志对本研究所做的任何贡献均已在论文中做了 明确的说明并表示了谢意。 申请学位论文与资料若有不实之处，本人承担一切相关责任。 本人签名：蓖永1 羁 日期： 汐7 年6 月9 日 关于论文使用授权的说明 本学位论文作者完全了解青岛科技大学有关保留、使用学位论文的规定，有 权保留并向国家有关部门或机构送交论文的复印件和磁盘，允许论文被查阅和借 阅。本人授权学校可以将学位论文的全部或部分内容编入有关数据库进行检索， 可以采用影印、缩印或扫描等复制手段保存、汇编学位论文。本人离校后发表或 使用学位论文或与该论文直接相关的学术论文或成果时，署名单位仍然为青岛科 技大学。( 保密的学位论文在解密后适用本授权书1 本学位论文属丁： 保密口，在年解密后适用于本声明。 不保密d 。 f 请在以上方框内打“、”1 日期加8 7 年f 月阜e 1 日期：7 年6 月7 日 贝泉 引前 访面汐个 名名签签 人师 本导 青岛科技大学研究牛学位论文 数学命题的机械化证明的历史 1绪论 数学命题的机械化证明( a t p ) ，又叫自动推理，是人工智能领域中的一个重要 分支，是数学与计算机科学的一门交叉学科。自动推理是指使用计算机在某一语 言系统下推理演绎数学命题的过程，是通过一套符号体系加以形式化，变成一系 列在计算机上自动实现的符号计算过程。其实质是把具有智能特点的推理演绎 过程机械化。自动推理是涉及人类智能问题的主要研究课题之一，从传统的数学 命题的手工证明到机器证明，是现代数学思想方法的一次重大突破。 近代的机器证明思想由莱布尼兹首先提出，起源于他的数学命题证明机械化 设想。到1 9 世纪末，希尔伯特等创立并发展了数理逻辑及数学的公理化方法， 为数学命题证明机械化提供了一个强有力的工具，使这一设想有了明确的数学形 式，上个世纪初，数理逻辑学家与计算机专家对数学命题证明的机械化进行了大 量的理论探索使得数学研究这样的脑力劳动机械化。自上世纪2 0 、3 0 年代，数 理逻辑学家们就己开始关注利用机器装置进行数学命题证明的问题。在此之前， 尽管几代数学家都为数学命题证明机械化作出过不懈的努力，然而，由于数学家 们只能使用简单的推理工具，实际上都未能取得良好的效果。直到电子计算机的 问世，为机器证明数学命题提供了物质条件，使这一设想的实现有了现实可能性， 因此数学命题证明机械化的研究蓬勃发展起来。 5 0 年代，数学命题机器证明开始兴起，成为一个数学领域。波兰著名的数学 家、逻辑学家塔斯基( a t a r s k i ) 为此做出了贡献。他在1 9 4 8 年的一本经典著作初 等代数和几何的判定法中，证明了一切初等几何及初等代数范围内的定理证明 是可以用计算机判断的，并且给出了具体的机械化证明的方法，这为人们开始这 方面的可行性研究树立了信心。5 0 年代中期，美同开始了利用计算机证明数学定 理的尝试。 机器证明史上第一项奠基性的突破，是由美国的卡尔基大学兰德公司协 作组作出的。1 9 5 6 年，此协作组的纽厄尔( a n e w e l l ) 、西蒙( hs i m o n ) 和肖乌等人 通过研究证明数学命题的心理过程，建立了机器证明的启发式搜索法，编制了一 个“逻辑理论机”程序( l 1 1 ) ，成功证明了罗素和怀特所著的数学原理第二章 5 2 条定理中的3 8 条，这一年可作为历史上计算机证明和人工智能研究的丌端。 1 9 6 3 年，他们又在计算机上证明了全部5 2 条定理。5 0 年代末，著名美籍华人、 m i z a r 语言系统与四元数的代数结构 数理逻辑学家、美国洛克菲勒大学的王浩教授发明了王浩算法，把机器证明规则 化。1 9 5 9 年他只用了9 分钟的时间，用计算机编写的程序证明了数学原理中 的一阶逻辑部分的全部3 5 0 多条定理，王浩所取得的成就在当时震动了数学与数 理逻辑学界，他的先驱性成就被人们誉为“一击落七蝇( s e v e nf l i e sw i t ho f l e b l o w ) ”【2 】。这一现实的成功极大地激发了人们寻求用计算机高效证明定理的努 力。正是王浩吹响了向数学机械化进军的号角。 7 0 年代，机器证明获得新的重大进展。1 9 7 6 年，美国伊利诺斯大学的阿佩 尔( ka p p e l ) 、哈肯( w h a k e n ) 和科奇( jk o c h ) 完成了构造可约构形的不可避免集的 工作，在电子计算机上解决了1 0 0 多年来手工证明未能解决的著名难题“四 色猜想”问题。 国内外研究动态 随着研究的进一步深入，今天人们已经能根据机械化方法编制程序，在计算 机上给出证明。在短短几年内，人们便在初等几何中的一些主要定理的证明上实 现了机械化，不仅如此，人们还用计算机语言证明了微分几何中的一些主要定理。 近来又对三角函数，双曲函数等一类超越函数公式实现了机械化的证明。机器证 明在分析拓扑学、集合论以及递归函数等方面都获得了成功的应用。因此，可以 预料，随着计算机愈来愈小型化而内存又愈来愈大，以及机器证明理论研究的不 断深入，将会开辟机器证明的新时代。 当前，国外有许多围家都在积极地进行数学命题的机器证明，其中比较著名 的定理证明验证系统有h o l 、m z a r 、p v s 、c o q 等1 5 个著名的数学命题证明系 统。其中，h o l 、m i z a r 、p v s 、c o q 、o m e g a 、l s a b e l l e f l s a r 、i m p s 和n u p r l8 个系统均需要有庞大的数学领域知识库支持【2 】。 在国内，以吴文俊院士为首的数学家在从事几何定理证明机械化的研究。吴 文俊教授用他自己建立的机器证明方法和编写的程序，在计算机上成功地证明了 非欧几何、圆几何、线几何以及微分几何的六百多条重要定理。上世纪9 0 年代 以后，在吴文俊教授的带领下，他的同事及学生吴文达、高小山、石赫、刘卓军 等在方程求解与数学机械化应用方面己得出一系列理论及实际应用的结果。如多 元多项式因子分解和极限环问题等。 青岛科技大学研究牛学位论文 1 3m iz a r 语言系统的发展过程及现状 1 3 1m i2 a r 系统概述 m i z a r 系统是一个利用计算机进行形式化处理项臼的总称，由波兰华沙大学的 a n d r z e jt r y b u l e c 教授组织! 的m i z a r 协会领导【4 】。m i z a r 系统的起始目的是设计建 立一个软件环境来帮助数学家处理、撰写和验证数学论文。因此发展的软件环境 是用来书写传统的数学论文，所以古典数学和集合理论就成为软件环境未来发展 的基础【5 】。m i z a r 系统主要是由如下三部分组成：一是m i z a r 语言，它可以帮助数 学家使用计算机撰写数学论文；二是m i z a r 软件，它可以收集整理数学论文和检验 数学论文的正确性与否；三是m i z a r 数据库，它被认为是世界上最大的可以被计算 机检验和处理的数学知识数据库【6 】。m m a r 系统通过使用m i z a r 语言来描述数学定 理，成为m l z a r 文章，并用m i z a r 本身提供的软件在p c 机上进行验证，通过验证的 完整无误的m i z a r 文章将会被发表在波兰的( f o r m a l i z e dm a t h e m a t i c s ) ) 杂志上，并 被收录l q m m l 数据库中。当我们在撰写m m a r 文章的时候，我们可以参考m m l 数 据库中被收录的文章7 。 1 3 2m iz a r 语言系统的发展历史 8 m i z a r 起源于1 9 7 3 年当时a n d r z c jt r y b u l e e 教授正在完成他的关于拓扑学的 博士论文，在那时他就有了一个强烈的愿望，使用计算机来帮助他编辑处理数学 论文。1 9 7 3 年l o 月，在他访问莫斯科科学技术学院期间，a n d r z e jt r y b u l e c 教授讨 论了他的想法。而m m a r 第一次被完整的提出来是在1 9 7 3 年1 1 月1 4 日华沙大学组织 的一次会议上，a n d r z e j 教授提出了可以开发一门可以记录数学文章的语言，它至 少有以下功能： 1 、文章可以存储到计算机里，并可以翻译成自然语言。 2 、文章应是形式化的、简洁易懂的。 3 、可以形成自动信息处理机制。 4 、能很容易地检测错误、确认参考书目、删除重复的定理等。 5 、能够实现计算机辅助教育的功能。 6 、可以实现自动排版。 在系统发展的初级阶段，强调这些是非常重要的。第一个可以运行的m t z a r 系统是a n d r z e jt r y b u l e c ，k r z y s z t o f l e b k o w s k i 和r o m a nm a t u s z e w s k i 教授于1 9 7 4 年秋天设计的用于谓词演算验证的o d r a - 1 2 0 4 系统。虽然非常的脆弱，但全部 的语法分析是非常成功的。 1 9 7 5 年，m i z a r 语言的研究得到波兰科学协会的资金支持，a n d r z e jt r y b u l e e 3 m i z a r 语言系统与四元数的代数结构 教授受k a l u z h n m 的思想的启发，于1 9 7 5 年1 1 月向该协会做出一份报告，同时 提交了m i z a r 语言的初级版本：m i z a r - p c ( p c 代表命题演算) ，此版本可以使用 雅斯科夫斯基( j a s k o w s k i ) 自然演绎推理的方法证明命题演算。值得一提的是在 报告中预见性地提出了数学知识数据库的问题，即1 9 8 9 年才设计成功的m m l 。 1 9 7 5 1 9 7 6 年间，m i z a r p c 被用来在华沙大学教谓词逻辑及数学命题的计算机辅 助证明这门课程。 经过3 0 多年的发展，到现在为止，m t z a r 系统己发展到78 版本，m v i l 为 42 7 版本。内含上千篇文章，2 万多数学定义，将近4 0 万条定理【8 】。 而现在的m i z a r 系统已经从单独的逻辑推理与数学证明发展到多方面的应用， 它的开发与应用主要包括四个方面的内容： 一、m i z a r 语言本身的开发。在应用过程会出现大量新的定义与符号，为了不 断提升m i z a r 语言的处理能力，就必须对系统进行升级，定义新的数据结构和新的 数据类型，建立新的数据模型，为进一步形式化做好准备，同时用m t z a r 语言所撰 写的并被验证无误的文章，即m i z a r 文章也被收录到m m l 系统中，成为数学知识 管理系统的基础。此项功能已得到北美数学知识管理组织( n a m k m ：m a t h e m a t i c a l k n o w l e d g em a n a g e m e n t ) 的重视1 0 】。 二、m m l 系统的修正。几乎每天都会收录新的m i z a r 文章，所以m m l 系统需 要经常性的修正，修正的内容有增强系统性能、归纳定义定理、重新组织数据库 中文章的顺序等。 三、形式化定理的翻译，m i z a r 语言产生的初始目的是使用计算机辅助数学家 撰写论文的，所以其形式化定理被人所认识是必需的一个功能。因此收录的m t z a r 文章能够被人所认识和接受就必须有相应的翻译机制和原理，还需要有效的计算 算法、领域知识，所以对其进行分析并完善，成为另外一个重要的研究内容。并 且，随着i n t e r n e t 的发展，网上数学的表示也越来越盛行，各种表示方式也层出不 穷，为了能够与比较流行的其它软件之间能够进行研究内容上的转换，重要的是 i 句o p e n m a t h ( o m d o c ) 转换，也必须有相应的策略和算法，这也是一个重要的研 究内容1 0 1 。 四、自动定理证明。自1 9 5 6 年n e w e l l ，s h a w 和s i m o n 完成了一个自动证明数 学定理的计算机程序l t 后，自动定理证明就成为一个独立的分支从人工智能领域 中分离出来。之后世界上就出现了不同的定理证明系统。到目前为止m m a r 系统在 此领域已经占有了一席之地，并且数学领域的绝大多数知识都可以使用m i z a r 语言 来验证，如集合论、代数、分析、拓扑、范畴论以及一些数学领域之外的如数学 难题、计算机模拟等 11 。并且其数据库m v l l 中已经收录了许多著名的数学定 理。m m a r 的发展需要庞大的数学领域知识库支持。因此数学领域知识的获取必将 青岛科技大学研究牛学位论文 有效地推动数学命题的自动证明，推动数学机械化的发展。 1 4 本文内容及安排 我们利用m i z a r 语言给出了四元数，四元数的运算，四元数的模、共轭、内 积和代数结构的定义，并讨论了相关性质。本论文共分5 章： 第一章：绪论 第二章：m i z a r 系统简介 第三章：m i z a r 数据库与系统 第四章：四元数、四元数的运算、模、共轭、内积及相关性质在m m a r 语言系统 中的实现 第五章：四元数的代数结构及其性质在m m a r 语言系统中的实现 2 1m iz a r 论文结构 2m iz a r 系统简介 m m a r 文章包括两部分：环境部( e n v i r o n ) 和文章的主体部分( m a i ns e c t i o n ) 。环 境部以e n v t r o n 开始，以分号结束。文章的主体部分以b e g i n 开始，以分号结束。 当然我们可以把文章的主体分成好几部分，每一部分以一个b e g i n 开始，表示如 下： e n v i r o n 环境部 b e g i n 主体部分l b e g i n 主体部分2 b e g i n 主体部分n 在e n v i r o n 部分，我们需要对写作文章过程【 i 需要引用的定义、定理、符号 等进行设置。具体可以表示如下： m i z a r 语言系统与网元数的代数结构 c n v l l 0 1 l v o c a b u l a r y a l ，a 2 ，a 。； n o t a t i o n s a l , a 2 ，a 。； c o n s t r u c t o r s a l ，a 2 ，a ； r e g i s t r a t i o n sa l ，a 2 ，a 。， t h e o r e m s a l ，a 2 ，a 。； s c h e m e s a l , a 2 ，a 。； r e q u i r e m e n t sa i ，a 2 ，a 。； 这里的4 ，a ，a 。都是m t z a r 文章的名字。其中v o c a b u l a r y 文件里面包含了 m i z a r 表达式中所使用的词汇，同时也表明了算符词汇的运算优先级，如数学运 算符。当然，作者可以使用已经定义的数百个词汇，也可以自己定义新的词汇。 s i g n a t u r e 部分( 包括n o t a t i o n s ，c o n s t r u c t o r s ，r e g i s t r a t i o n s ，r e q u i r e m e n t s 四部分) 通知m t z a r 处理器这篇文章可以使用此处列出的文章里的符号，来生成m t z a r 表 达式。 余下的三个引用；r e g i s t r a t i o n s ，t h e o r e m s ，s c h e m e s 就是告诉m i z a r 处理器町以 使用这些列表文章中的定义、定理和模式等。 “文章主体”包括我们所作的数学术语和定义以及与这些定义相关的性质。 当我们的文章有不同的内容想要表达时，每一部分都以“b e g i n 开头。其一般包含 以下几项； 一、预声明模块。声明标识符( 变量) 的类型。定理证明过程中使用到一个变 量而没有指出它的类型，此变量的类型即为预先声明的类型。 二、定义模块。用来定义或重新定义m m a r 语法构造：数学术语的构造( 即 f u n c t i o n s ) ，公式构造( 即p r e d i c a t e s ) 和类型构造( 即m o d e s ) 。当然，一篇文章不一 定同时要包含这几种定义形式。 三、定理证明。它证明一个数学命题，以后可以被其它定理或文章引用。 四、辅助信息。它包含了一些本地可以使用的对象，如引理等，这些内容不 会被收录到数据库文件中，当然其它文章也小可以引用。 青岛科技大学研究牛学位论文 2 2m jz a r 语言的基本语法结构 2 2 1m iz a r 语言的数据类型 在m i z a r 语言中，每一个变量都有数据类型。所以m i z a r 处理系统在处理m i z a r 文章时必须知道所使用的变量是m m l ( m i z a r 数据库) 中的哪一种数据类型。m i z a r 中的数据类型有r e a l ( 实数) 、s e t ( 集合) 、t o p s p a c e ( 拓扑空间、m a t r i x ( 矩阵) 等等，新类型的定义可以通过s t r u g t u r e 、m o d e 、a t t r 和c l u s t e r 等定义而得到。在使 用已有的数据类型时，一种方法可以通过预声明的方式声明它的类型，例如： t s e t v etf o rt o p s p a c e ； 上面语句的意思是声明t 为拓扑空间。在表达一个使用变量的语句时，如果变量 没有预先声明过，则此时应该明确给出它的类型，例如： f o rab e i n gc o m p l e xn u m b e r ，mb e i n gm a t r i xo f c o m p l e xh o l d s l e n ( a + m ) = l e nm & w i d t h ( a + m p - w i d t hm ： 变量a 在语句中说明是复数，m 复数矩阵。 如果想使片j 在其它文章中定义的数据类型，如n 文章中的0 类型，则需要在论 文环境部加入引_ e f j 如下： v o c a b u l a r ya ；s i g n a t u r e ； 2 2 2m i z a r 语言的公式 在m i z a r 语- 言中，否定、与、或、蕴含和当且仅当用n o t 、o r 、i m p l i e s 、i f f 表示。它们的优先级别依次降低，其中i m p l i e s 、i f 珀q 优先级相同。对于由n o t 和& 构成的式子可以不带括号，系统自动为它们加上，如： 巾l & 睨& 0 3 系统将自动翻译为：( m l & 0 2 ) & 3 ；相反的，i m p l i e s 和l f 坝0 不可以省括号，如： o li f f 0 2i f f 0 3 是不正确的写法。 对于公式，有三种类型的公式： 一、一般性的简单公式，如： f o r x , yb e i n g r e a lh o l d sx = y ； 二、具有条件的公式，如： f o r x , y b e i n g r e a ls t x 0 0 & y 0 0 h o l d s x + y o ； 三、具有存在谓词的公式，如： f o rx , yb e i n gn a ts tx s e t ，p a n y , a n y ： e x f s t d o m f = f ( ) & f o r xs t xe f oh o l d s p l x , f x 】p r o v i d e d a 1f o r x , y l ，y 2s tx f ( ) & p x , y 1 & p 【x ，y 2 】h o l d s y l = y 2a n d a 2 ：f o r xs t x f ( ) e x ys t p x ，y 】证叫略； 前提a 1 ，a 2 通过关键词p r o v i d e d 引出，并通过a n d 将两个命题分开。 2 4 定义 2 4 ，1 词汇表文件的书写方法 讲到定义，首先要讲到词汇表文件( v o c 文件) 的建立的问题。所谓词汇表 是指自己的文章里的新定义的数学术语，而在m i z a r 数据库中是不存在的。例如 定义个新函数，为了使用它，就必须把它放到v o c 文件中。例如下面就是数据 库里的一篇文章的词汇文件p r e _ t o p c v o c ： m i z a r 语言系统与四元数的代数结构 所定义的词汇 表里每一行定义一个新词汇，其中第一个大写字母是词汇的类型，后面紧跟 的是定义的词汇，不可以带空格，特别的对于0 ，可以在前面的基础上再加入空 格和数字，数字代表它的运算优先级别，为l 到2 5 5 ，缺省为6 4 。对于第一个字 母说明如下表 符号代表的含义 mm o d e o f u n c t o r r p r e d i c a t e k 左括号 l 右括号 gs t r u c t i l l g us e l e c t o r va t t n b u t e 表2 - 2 词汇表表丈中首字母的意义 经过这样的定义之后，下一步把这个v o c 文件存在一个d i c t 文件夹里，d i c t 文件夹和m i z a r 文章在同一个文件夹里。另外，还需要在环境部加入这个新定义 的v o c 文件的文件名，就可以在我们的推理过程中使用这些新定义的词汇了。当 然，在定义之前还必须保证在m i z a r 数据库中没有定义过，方法就是在m 二m 系 统中执行c h e c k v o c 【v o c a b u l a r y 命令，根掘命令的执行结果，就可以知道所定 义的数学术语在是否已经存在m m l 数据库里。 青岛科技大学研究牛学位论文 2 4 2 结构的定义 结构的定义有两种类型：一个是不带参数的结构，一个是带有参数的结构。 对于前者，其定义格式如下： s t r u c t h # o i 一 0 1 ，一 0 耐) ； 这里，为结构的名字，0 1 ，o 。是函子名，0 i ，0 。是类型。结构的名字 以及函子的名需要包含在v o c 文件，前面分别加上g 和u 。例如 1 3 】： d e f i n i t i o n s t r u c tl n c p r o j s t r ( # p o i n t s ，l i n e s 一，n o ne m p t y s e t ， i n c - ，r e l a t i o no f t h ep o i n t s ，t h el i n e s # ) ； e n d ； 和 d e f i n i t i o n s t r u e t ( i n c p r o j s t r ) i n c s t r u c t ( # p o i n t s ，l i n e s ，p l a n e s n o ne m p t ys e t ， i n c 一 r e l a t i o no f t h ep o i n t s ，t h el i n e s 。 i n c 2 一 r e l a t i o no f t h ep o i n t s t h ep l a n e s i n c 3 一r e l a t i o no f t h el i n e s ，t h ep l a n e s # ) ； e n d ； 这是两个结构的定义，其中第二个定义由第一个定义派生出来的。 对于后者，即带参数得结构，其定义格式如下： d e f i n i t i o nl e t x lb e0 i ，) 【i lb e0 。； s t r u c t o v e r x i ，x k ( # o l 一 0 1 ( x j ，) ，o - o n ( x l ，) # ) ； e n d ； 这里的x r l 。，x , k x i ， 。例如1 1 4 1 ： d e f i n i t i o nl e tfb e1 s o r t e d ； s t r u c t ( l o o p s t r ) v e c t s p s t ro v e rf ( # c a r r i e r s e t ， a d d b i n o po f t h ec a r r i e r , z e r o e l e m e n to f t h ec a r r i e r , l m u l t f u n c t i o no f ：t h ec a r r i e ro ff , t h ec a r r i e r ： ， t h ec a r r i e r # 1 ： e n d ； 2 4 3m o d e 的定义 最经常使用的m o d e 的定义格式如下： d e f i n i t i o nl e t x 1b e0 j ，) ( r ib eo n ； m o d e r o f x i ，x k - - ) 。( x l ，h ，x n ) m e a n s ：l ：8 ( x l ，) 【n ，n ) ； e x i s t e n c e ； e n d ； m i z a r 语言系统与四元数的代数结构 r 是m o d e 的名字，它需要放到v o c 文件中，前面加大写字母m 。对于m o d e 需要证明e x i s t e n c e ，即存在性。它对应于下面这个定理： f o r x lb e i n g0 1 ，b e i n ge n ，y b e i n go ( x l ，) h o l d s y i s fo f x 1 ，x l ki f f 8 ( x j 。，【| l ，y ) ， 2 4 4 属性( a t t r ) 的定义 d e f i n i t i o nl e tx jb e0 1 ，b e0 n ； a t t r 0 【x i ，) ( r i ) i s am e a n s 8 ( x l ，) 【n ，n ) ； e n d ； 是属性名，它应该放到v o c 文件中，格式：v a ，0 l ，0 。是属性的参数。例如 1 6 1 ： d e f i n i t i o n l e tc b e n u m b e r ； a t t rci sc o m p l e xm e a n sci nc o m p l e x ； e n d ； 2 4 5c i u s t e r 的定义 给予某个数据类型以性质就可以得到一个新的数据类型，如给予类型r e a l 以p o s i t i v e 属性，就可以得到一个新的数据类型- p o s 赴i v er e a l ( 即正实数类型) ， 它就是c l u s t e r 。新的c l u s t e r 一定义，其它文章就可以应用