Mizar语言及MKM：数学表达的形式化和语义基础的挑战

理论计算机科学电子笔记93（2004）60-69www.elsevier.com/locate/entcs使用和解析Mizar语言保罗凯恩斯1杰里米高2伦敦大学学院互动中心31摘要Mizar是一个建立良好的和成功的系统，用于产生正式的数学。我们通过研究Mizar语言来研究形式数学对数学家的可接受性具体来说，我们通过尝试为其构建语法来分析Mizar语言的各种特性，以便解析其库。我们的分析强调了语言中尚未解决的问题，这些问题可能会减少数学家的使用。保留字： Mizar，解析器，编译器编译器，上下文无关语法1语言MKM数学知识管理（MKM）关注的是使数学知识在广泛的环境中广泛地提供给众多用户。为了提供一个全面的、国际相关的数学知识库，必须能够在数学中使用的多种形式的语言之间进行翻译，包括单词、符号和约定。还有一个问题是如何将现有的数学转换成这样一种国际上健壮的形式。形式数学语言似乎在MKM社区中被普遍认可[2]，作为提供可由基于机器的MKM工具使用的语义基础数学形式的良好步骤语言上不同的数学形式可以通过自动生成1 电子邮件：p. ucl.ac.uk2 电子邮件：ucl.ac.uk1571-0661 © 2004 Elsevier B. V.根据CC BY-NC-ND许可证开放访问。doi：10.1016/j.entcs.2003.12.028P. Cairns，J. Gow / Electronic Notes in Theoretical Computer Science 93（2004）61从正式语言翻译过来。为了维持MKM存储库的增长，数学家需要能够直接为这些存储库做出贡献有了形式语言的基础，这意味着数学家必须能够产生，或者至少很容易地复制，他们自己的数学作为一种形式语言。我们的重点是研究数学家目前的工作方式和正式的数学语言之间的差距具体来说，我们研究了一种特殊的形式语言，Mizar语言[11]，并分析了数学家对其可用性的各个方面。这里的还有其他意义上的在下一节中，我们将详细介绍为什么选择Mizar-主要是因为它是一个具有许多好特性的大型库。在我们分析了Mizar语言的问题之后，我们讨论了形式数学语言的更普遍的含义。我们的主要结论是，由于语言的灵活性和更这是否是“更加数学化”的必然结果必须强调的是，虽然Mizar被用来强调正式语言的问题，但我们的意图不是专门批评Mizar，而是从中吸取一般的教训。事实上，我们认为Mizar是一个更容易被计算机接受的正式系统。这使得它特别值得关注和进一步改进。2为什么是米扎尔？Wiedijk最近整理了在15个主要形式系统上开发的形式证明的例子[13]。他对这些证据的分析允许在不同的系统之间对一些不同的因素进行比较。 很自然，这些系统各不相同，有各种各样的优点和缺点。从这一点来看，很明显，Mizar拥有迄今为止最大的图书馆，Mizar数学图书馆（MML），可以在网上以形式化数学杂志的形式获得[8]。此外，它有一个合理的数学重点是一阶，经典逻辑与简洁的语言很容易阅读的数学家不熟悉的Mizar的具体。由于这些原因，Mizar作为一种工具脱颖而出，数学家可能有兴趣使用它来编写数学，因此值得从可用性方面考虑62P. Cairns，J. Gow / Electronic Notes in Theoretical Computer Science 93（2004）perspective.在语言学上，Mizar语言也属于数学方言的类别，其各种语言在特定的功能上有所不同，但它们本质上都是形式的，一阶的，面向数学的，弱类型的语言。Mizar也是这一更广泛的语言类别的合理代表。Isar是Isabelle的前端，其灵感来自于Mizar，它为系统的用户提供了可读的形式证明与Mizar相比，Isar有许多优势，例如更好的文档和使用各种逻辑的能力[15]。然而，Isar系统在其他标准上的评分不太好，特别是那些与数学文本密切相关的标准。 例如，Mizar更像自然语言，并且通常具有更短的形式化。Mizar也有一些实用的功能，使其吸引人的研究。有几个版本的Mizar用于Windows和Unix平台，至少Windows版本的安装和与emacs文本编辑器集成非常简单。此外，还有Mizar网站[9]，它提供了大量的资源来理解Mizar语言，MML和开发Mizar文章的过程。从某种意义上说，这些考虑都是次要的，而不是Mizar系统本身的优势。然而，就系统的可用性和广泛使用而言，任何不提供这些服务的系统都自动处于不利地位。这并不是说Mizar没有可能的问题。最值得注意的是，所有关于学习Mizar的建议都提到了与经验丰富的Mizar用户密切合作的价值。这表明，除了最专注的个体工作者之外，所有人都难以避免或掌握开阳星的特质3分析方法为了客观地分析Mizar语言，根据Mizar网站上的语言描述建立了一个语法。使用的解析环境是JavaCC [7]，一个自顶向下的编译器。它对词法分析器和语法分析器使用类似Java的表示[1]，并将其转换为原生Java。JavaCC被选为各种可用编译器的代表。由于为Mizar开发解析器的困难，最初只解析摘要，尽管有些文章已经完整解析了3。3JavaCC也有局限性，这意味着，虽然原则上所有722个抽象都可以解析，但我们只能解析其中的491个（大约68%）。P. Cairns，J. Gow / Electronic Notes in Theoretical Computer Science 93（2004）63为一种语言建立一个解析器是任何计算机科学家的面包和黄油，通常不构成对语言的分析。然而，在这种情况下，Mizar语言有一些特性使得标准解析特别困难。有些功能允许语言在丰富的层次上发挥作用，其他功能只能通过系统的有机发展来解释。因此，解析充当了“系统取证”的工具，4解析Mizar语言关于Mizar，首先要注意的是，它不是一种简单的语言。Mizar的语法有超过150个产品和93个关键字。相比之下，Java语言只有83个产品和50个关键字。这并不是说Mizar一定更难学习或掌握，因为语言的困难然而，它确实表明Mizar肯定是一种有趣的语言，需要详细研究从所做的工作中，三个关键问题变得清晰起来，这大大增加了构建解析器的复杂性。首先，也是最令人惊讶的是，Mizar不是一种上下文无关的语言。其次，等式，特别是迭代等式需要特殊的语义。最后，括号法和数学中括号的使用一样复杂。我们依次讨论这些特征。4.1上下文敏感性自20世纪60从那时起，工具和技术已经标准化，以便开发新的编程语言作为一年级本科生的练习。上下文无关意味着语言可以使用产生式进行解析，而无需参考单个标记的含义，只要它们被词法分析器正确分类。然而，Mizar并不是上下文无关的。解析器需要三个结构，其中需要标记的语义含义，以便正确选择如何解析文章。这三个结构是：(i) 原子公式表达式(ii) 类型表达式(iii) 类型表达式在上述每种情况下，构造都是由标记后跟64P. Cairns，J. Gow / Electronic Notes in Theoretical Computer Science 93（2004）一个参数，然后是一个进一步的结构。出现问题是因为两个结构都用逗号分隔，第一个结构的参数也是逗号分隔。解析器不可能决定第二个构造是真正的构造还是仅仅是构造的参数。例如，在DECOMP 1中出现以下定义：定义设X，Y是非空的TopSpace;设f是X，Y的映射;attr f是s-连续的，表示.这里map是一个带有两个参数X和Y的模式符号。在不知道这一点的情况下，Y同样可以是一个像f一样的进一步定义或一个映射的参数（它确实是）。由于参数列表可以是任意长的，因此解决可能的歧义需要有限的前瞻，这大大减少了解析器性能。当然，计算机科学家对这个问题的解决方案是需要消歧括号。这没有抓住重点。数学家我们的方法的解决方案是确定可以跟随模式，结构和谓词构造的参数的数量，并在解析时计算标识符的数量。当总数达到时，很明显，任何随后的标识符都必须属于下一个构造。这并不完全可靠，因为重载谓词可以采用可变数量的标识符。然而，到目前为止，允许解析已经足够了。的下一步将是进行适当的基于上下文的修复。4.2平等当等式用于逻辑时，通常需要特殊处理[5]。这部分是因为它作为一个特殊的谓词的地位，能够重新标记语言的句法元素，部分是因为它的意义在三个世纪以来的巨大超载Recorde定义了等号。任何数学语言想要捕捉到等号的多样而丰富的用法，都不可避免地会遇到困难，这就是Mizar。在Mizar术语中，=符号是一个固定谓词，并且在特殊系统文章HIDDEN中确实被定义为这样。此外，它被反复地重新定义（重载），尽管通常引用回系统原始版本。然而，为了处理equals在句法上的特殊位置，有几种产生式专门区别对待=与其他同品种器械相比。虽然这使语言复杂化，但它也允许语言反映=的一些正常用法当需要做迭代等式时，=的使用变得复杂这种结构对应于生成看起来像这样的证明：P. Cairns，J. Gow / Electronic Notes in Theoretical Computer Science 93（2004）65（x +1）2=（x +1）。（x+1）=x. （x +1）+1。（x+1）=x2+x+x+1=x2+2x +1在这里，后面等式的左手边被省略，被理解为对于证明的所有行都是相同的。这种结构通常用于数学中，并在其他证明风格中得到反映，如计算证明[4]。Mizar通过特殊的符号实现迭代相等。在上面的计算中，除了第一行之外，所有行都使用=来代替=符号。这种用法对读者和Mizar文章的作者来说都是很自然的。从解析的角度来看，这有点棘手，因为第一行证明是等式，可以继续作为迭代等式，也可以简单地独立，然后证明以不同的结构继续。在给定的Mizar文法中，迭代等式需要无限的前瞻来寻找下一个可能。= symbol，因此知道要解析哪种证明结构。为了避免这种情况，唯一看起来简单有效的方法就是允许。=将校样线样式设置为跟随任何校样线。这允许解析器继续进行，但当然引入了具有可解析但无意义的证明的可能性。这当然需要在第二个解析阶段中修复。当然，这个问题并不是不可克服的，目前的迭代等式为数学家提供了一种方便而自然的证明方式。然而，在重新思考迭代等式语法的一部分之后，很明显，数学家确实使用了其他类型的迭代证明结构，Mizar可以有效地实现。例如，和的迭代等价物通常被使用。<用开阳星的术语来说，这可以通过一个特殊的方式来处理。前缀标记，指示迭代谓词。不清楚为什么Mizar没有这样的符号-它可能再次反映了数学中=谓词的特殊性质。一般谓词迭代器的实现最好由uniform处理所有谓词，包括平等。4.3交叉进在Mizar中的括号有点复杂。很自然地，Mizar有括号来逻辑地或表示地分离语法的部分。这些括号包括常见的嫌疑人：{}，（）和[]。此外，Mizar允许文章定义充当函子的方括号。例如，[]在核心Mizar语法中用于指示某些谓词的参数（私下66P. Cairns，J. Gow / Electronic Notes in Theoretical Computer Science 93（2004）定义的），而它们也用于表示有序对，三元组等。这种重载不会导致解析问题，而是词法分析问题。方括号是在词法分析器中定义的，这样它们就可以在私有谓词的语法然而，它们也需要被理解为可能的函子括号，它们具有完全不同的语法集合角色因此，括号的重载就像普通的数学一样。有些方括号只是简单的分隔符，帮助读者理解哪些内容属于一起。在其他时候，他们意味着更多的东西和含糊不清随之而来。例如，实分析中的f（a，b）可以等于作用于两个自变量的函数f，或者是函数f下从a到b的实开区间的图像。数学家们通常会做一些努力来澄清其含义，或者确保可以从上下文中推断出其含义。括号的问题突出了这样一个事实，即Mizar以复杂化机器语义为代价来反映正常的数学用法（随之而来的是混乱）解析这个重载在概念上并不复杂，但是它确实需要一些谨慎的实现。4.4一些小问题还有几个小问题是由于使用Mizar网站对Mizar语言的描述而产生的从本质上讲，这些规则几乎但不完全是语言的准确反映某些规则省略了可能的标记，例如基数类型可以有一个可选的模式TopGroup是类TopSpace类Group关联（非空TopGrStr）;“non”不包含在文档中对基数类型的描述中。或者再次，文章需要有一个DOS兼容的名称，在partic-至少有五个字符。 这条规则显然被文章打破了AMI 1。更微妙的是，能够在Mizar库中找到特定术语的定义和用法的findlist实用程序并不完全与库协调。有些被发现的定义实际上并不存在，但可以在图书馆的其他地方找到。显然，已经完成了一些重构，但不是在整个Mizar服务集所有这些问题一旦被认识到，就很容易得到解决有趣的是，Mizar语言的描述是重新制造的，而不是直接从Mizar系统中提取的。换句话说，“手册与系统不同这P. Cairns，J. Gow / Electronic Notes in Theoretical Computer Science 93（2004）67对于从飞机控制系统到录像机的用户来说，这是一个众所周知的问题来源[12]。此外，它对任何像我们这样希望在Mizar上工作并开发自己的工具的如果得知其他系统也有同样不准确的描述和手册，这一点也不奇怪。5讨论正如一开始所说的，这篇评论并不是要特别批评Mizar，而是要从Mizar那里了解一般形式语言的问题。Mizar有一些特殊的性质，但事实上，创造一种丰富而灵活的数学语言是完全合适的。MKM的整个领域证明，数学并不是许多非数学家所认为的那种纯粹、明确和不变的语言突出的三个主要解析问题，即上下文敏感语法，等式和括号，都允许Mizar反映真实的数学结构。例如，数学家通过简单地使基集相等而不参考实际拓扑来使两个拓扑空间相等。Mizar允许相同的用法。或者类似地，数学家经常懒得明确定义谓词或函数的参数数量。上下文使确切的意思清楚。在米扎尔也是如此。基本的假设似乎是，如果一种形式语言是可用的，并接受数学家，那么它必须符合尽可能接近公认的数学用法。Mizar显然采用了这种方法，因此在Wiedijk的研究中表现良好其缺点是，使语言可用，其作为数学的底层表示的有用性的影响。Bancerek已经指出，运算符的有用和有效的重载对Mizar库中的正式搜索和检索任务有影响[3]。鉴于学习Mizar的障碍之一是掌握广泛的库，因此不希望使搜索和检索变得困难。因此，搜索必须是上下文敏感的，并且依赖于搜索者的视角，而不是术语或符号的绝对含义这对人类可用和搜索系统可用都提出了挑战。此外，如果一种形式语言真的要反映当前的数学用法，那么它不仅在今天而且在将来都需要是灵活的。 Mizar允许重新定义术语，以便它们具有特定上下文所需的特定语法。这可能意味着用户正在使用新的术语或术语的语法开发新的数学，但是正在利用68P. Cairns，J. Gow / Electronic Notes in Theoretical Computer Science 93（2004）这是一种相对老式的资源。虽然这在短期内不是问题，实际上在数学中是正常的，但它可能会成为MML长期可用性的问题。例如，现代数学家很难理解由表示的集合的交集和并集。 和+ 符号，分别。这个符号没有什么错误或模棱两可的地方，它只是过时了。我们的关键点是，要想成功，一个系统需要广泛的接受。这可能涉及人们开发专门的工具，服务和适应他们的特殊需求。一个中央Mizar团队不可能提供一个庞大用户群可能需要的所有服务。相反，如果第三方能够基于Mizar核心开发自己的软件，那就更好了。Mizar显然有一个使其系统在各种平台上可用的政策。然而，我们在制定语法进行解析方面的问题，特别是缺乏对语言的准确描述，意味着使用和适应Mizar语言并不是它应该做的简单任务。6结论就目前而言，Mizar语言是一种灵活的、类似于代数学的语言，可用于指定形式证明。它的可伸缩性使它可用，但也破坏了它作为数学形式基础的有用性语言的几个方面不能很容易地重建，这对语言的潜在用户以及希望开发工具的人有明显的Mizar语言是为人和计算机设计的。我们强调的困难提出了一个问题，即一种语言是否有可能成功地实现这两个目标。我们认为，这是MKM社区的一个重要开放问题。也许可以改编Mizar或其他语言，以提供一种更明确定义和更容易理解的语言，适合两者。另一方面，如果MKM的语言分为两种可能会更好：一些语言将是数学家使用和发展数学的理想语言，另一些语言将是存储，标准化，搜索和检索任务的理想语言。翻译系统将确保数学家所产生的内容在更大的正式知识库中具有形式上的正确性。他们还将把知识库的部分翻译回工作数学家的语言环境。考虑到我们对可用性的关注和倾向，我们未来的工作是调整Mizar或基于Mizar的系统，使其成为一种编程人员认为有用和自然的语言。从这个意义上说，米扎尔指出，P. Cairns，J. Gow / Electronic Notes in Theoretical Computer Science 93（2004）69我们认为形式语言应该走的路。尽管我们已经讨论了这些问题，而且它已经有30年的历史了，但它仍然代表了形式语言的最新发展，可以想象，它可以被主流数学界所采用。确认感 谢 Harold Thimbleby 教 授 的 有 益 评 论 。 杰 里 米 · 高 是 由 教 授 资 助 的Thimbleby引用[1] A.阿霍河Sethi J. D. Ullman，韦斯利，1988年[2] A. 基蒂湾布赫伯格H. Davenport（eds），Proc.第二届数学知识管理国际会议LNCS 2594，Springer，2003年[3] G. 班塞雷克山口李晓云，信息检索在信息检索中的应用[2]，2003年[4] J. Grundy，“A browsable format for proof presentation，”Math. Universalis，2，1996http://www.ant.pl/MathUniversalis/2/grundy/mu.html[5] A. G.汉密尔顿，[6] E. T. Irons，Algol 60的语法指导编译器，重印于Comm. ACM，26（1）：14[7] Java编译器编译器，http://javacc.dev.java.net/[8] 形式化数学杂志，http://www.mizar.org/JFM/[9] Mizar项目主页，http://www.mizar.org/[10] R. P. Nederpelt，J.H. 格弗斯河C. 德Vrijer（编辑），逻辑研究和数学基础，第133卷，北荷兰，1994年。[11] P. Rudnicki，Mizar项目概述，1992年程序类型和证明研讨会论文集，1992年[12] H. Thimbleby P.B. Ladkin，A proper explanation when you need one，in People and ComputersX（HCI[13] F. Wiedijk，[14] M. Wenzel，Isar -可读的正式证明文件的一般解释方法。耶氏酵母中Bertot，G.Dowek，A.赫斯科维茨角波林湖Thery（eds），第12届高阶逻辑定理证明国际会议，LNCS 1690，Springer，1999年[15] M. Wenzel F. Wiedijk ， 数 学 证 明 语 言 Mizar 和 Isar 的 比 较 。 Journal of AutomatedReasoning，29（3-4）：389