TMCOq: 证明助理的理论计算机科学电子笔记

理论计算机科学电子笔记103（2004）27-48www.elsevier.com/locate/entcsTE Xmacs作为形式化开发Philippe Audebaud1LemmeProjectINRIASophia Antipolis，法国劳伦斯·里多2LemmeProjectINRIASophia Antipolis，法国摘要我们提出了一个用于出版和传播由证明助理认证的正式理论的创作工具。 我们使用了TeXmacs，这是一种关键词：认证，创作工具，证明助手，形式化开发，结构化D ocum nt，LATEX。1介绍我们提出了一个名为TM CO q的工具包，对于使用定理证明器助手验证某些形式化开发的用户很有帮助，例如CO q[9]和希望为科学出版物或在线浏览做好准备。因此，我们假设用户的主要要求是，首先，能够以数学文章的常用语言呈现他们的1我是菲利普。奥德巴@所以我是菲利普。in ri a.fr2电子邮件：Laurence. inria.fr1571-0661 © 2004 Elsevier B. V.根据CC BY-NC-ND许可证开放访问。doi：10.1016/j.entcs.2004.09.01228P. Audebaud，L. Rideau / Electronic Notes in Theoretical Computer Science 103（2004）保留相关发展项目仍由本公司核证的性质。为了实现第一个目标，我们提供了一个有效的工具，它提供了LATEX质量排版，用于展示正式的开发及其文档。tation在一起。为了保持每一步开发的正确性，我们实现第二个目标的方法是始终致力于整个开发，但要对这个开发提供不同的观点出于文档的目的，用户更希望能够看到整个开发，而article是完整文档开发的选定视图，仅显示整个开发代码的片段。第一个解决方案包括编写一份LATEX文件。这是一个典型的分歧如何使用他的结果，插入在地方选择件的正式发展。这种方法有明显的缺点。 剪切和粘贴过程可能会在正式开发没有错误时引入错误。开发中的任何修改都需要在文章中进行同步，否则会使后者在使用定理证明器执行的证明步骤方面不准确甚至错误。插入的源代码片段是逐字介绍的，这意味着语法可能与通常的数学语言和自然语言相去甚远。因此，符号和非正式解释与正式文本非常不同。定理证明器的语法甚至可能会改变，从而引入另一个误解的来源。为了找到一个更好的解决方案，让我们仔细看看是什么构成了这样一个正式的发展。它由一个或多个称为脚本的文件组成，从编程的角度来看，其结构遵循通常的结构声明、陈述、命令等都是证明者特有的，都是方言句子的一部分。它们构成了脚本的活跃部分这意味着它们是脚本中定理证明者需要知道的唯一部分。在代码中放置的任何文档或解释只能放在注释字段中，这些字段是不相关的（即，（1）从观察者请注意，到目前为止，已经为编程语言开发了许多文档工具。 J AVADOC和D OXYGEN（以及其他公司）为此做出了有趣的贡献。 但是，它们太代码化了-centrictobeusefulinorconttext.由于正式的开发由定义、定理和证明组成，而不是程序片段，因此用户不会使用LATEX来编写、记录和发布他们的工作然而，尽管如此，一个起点是简单地将TEX命令作为脚本的一部分放在注释中。在TeoremProverAssist中，PVS[6]提供了一个用于显示公式和证明的LATEX生成它是基于一个简单的P. Audebaud，L. Rideau / Electronic Notes in Theoretical Computer Science 103（2004）29使用替代机制。 META PRL[8]提供（低级）格式化基于其OCAML实现语言，以及POSTSCRI pT和HTML输出格式，但没有LATEX代码ggenrationa sfarasweknownow. 为了更好，Isato ool [1]提供了一个蝙蝠LATEXDOCNtgenera或r。 在Coqcontext中，该函数基本上由COqDOC[5]来实现，其将LATEX和HTML作为脚本的输出格式。该工具进行了简单的词法分析，生成标识符的超链接和各种语句的索引表。白话句子只是逐字插入生成的文档。这样的工具仍然无法以用户友好的语法呈现正式的开发片段，尽可能独立于CO q端的变化。此外，文档和代码仍然属于不同的世界。不可能进行前向引用，以确保整个生成的文档的统一标记。虽然这一进程已自动化，因此不太容易出现人为错误，结果仍然绑定到用于认证的CO q1.1目标正式开发的传播（在科学文章中或通过Web上的代码分发）是开发生命周期的重要组成部分该工具必须帮助用户编写代码文档（例如，在程序中编写注释），它还必须通过允许代码导入和易于添加自然语言解释来帮助用户生成科学文章。我们希望提供各种输出格式，例如，允许通过Web界面（即，该工具必须管理代码中的导航链接）并操作在科学目标发布中使用的所有标准输出格式：LATEX，HTML，POSTSCRI pT，etc.该工具必须提供高质量的可视化，使用读者熟悉的符号（例如，使用标准数学符号）以及用户友好的界面。它还必须允许使用自然语法来呈现正式的开发，并且必须尽可能避免使用一个理论家用他自己的语言来解释。是这样的，这件事应该-播放视频：nat，a2=|一|而不是（a：nat）（等于（sqrt（a（2）（absolu a））。用户必须能够定义自己的符号，而这不-在文档的各个部分中必须保持一致（即，在解释中保持与导入的代码片段中相同的符号）。30P. Audebaud，L. Rideau / Electronic Notes in Theoretical Computer Science 103（2004）最后，为了避免在从源代码到演示文稿的翻译中出现常见的错误（错别字总是令人不快，但在经过认证的开发环境中尤其令人讨厌），该工具必须允许自动导入源代码（例如定理陈述，定义等）。以保持其正确性。这种自动翻译还应该能够保留演示文稿和脚本之间的链接、连接和来回的对应关系，并由证明者控制。只要用户不修改它，自动翻译就可以保持可视化代码的正确性。在这里，人们只能在最终文档中导入经过认证的代码的片段。但是，一旦需要修改导入的代码，为了确保正确性，我们的工具必须管理整个开发（即使只显示片段），以便允许提取开发以进行工具外部的认证，或者允许在工具内部进行交互式认证，直接与证明器通信。实际上，不像程序代码的片段可以独立于代码的其余部分来考虑，正式开发的片段只能在整个开发的上下文中进行验证。图1显示了文档流程，首先导入脚本，然后是文档步骤，最后提取为各种格式，特别是CO q脚本提取，允许另一个认证周期。图1.一、从CO q脚本生成文档的目标很重要。首先，出于兼容性的原因，我们必须提供脚本的独立版本，其中文档片段被插入到适当的注释区域中。第二，更重要的是，这个目标是一个证据，可以从丰富的文档中提取的部分，涉及用户的正式开发，这个新的脚本必须接受的证明者之后。P. Audebaud，L. Rideau / Electronic Notes in Theoretical Computer Science 103（2004）311.2一些示例我们的工具并不紧密耦合到给定的定理证明器。在未来，它甚至应该是一个独立的工具。 然而，我们从一个案例研究开始我们的正式发展，主要是使用Coq定理证明。因此，所呈现的示例使用Coq语法。让我们举一个简单的例子。注意，在Coq具体语法中，（X：A）B代表全称量化X：A.B，~A代表逻辑否定A，而（EXT x：C| P）表示存在连接词x：C.P（x）。因此，不是将not_all_ex_not的类型显示为（U：类型; P：（U->Prop））~（（n：U）（P n））->（EXTn：U| ~（Pn））（1）人们宁愿看到（二）最终，人们甚至希望有可能用自然语言漂亮地打印这个语句。 例如，代替原始的CO q引理：这在很大程度上取决于符号增强机制，人们更愿意看到引理1.1（Set nrootIR）<$n∈N. 0 （sum AB）| inr : B -> (sum A B).值得注意的是，具体语法通常是根据以下方面来选择的：36P. Audebaud，L. Rideau / Electronic Notes in Theoretical Computer Science 103（2004）(i) 它能够被人类读者轻松阅读(ii) 以及其被自动读取从而被计算机理解的能力。想一想，如果我们把人类和计算机也换一下，这两点都成立！需要记住的重要一点是，对于这两点，应该可以从具体表示中推断出，归纳定义在结构上是由有限序列的命名项（在这个例子中是inl，inr）作为具有各自类型信息的构造函数组成的。此外，语法[A，B：Set]意味着集合A和B是定义中的参数，结果是一个集合，如片段“：Set”所示。因此，一个归纳定义有它的名称、参数、结果类型和有限的构造函数列表。因此，我们必须抓住这些场，作为结构的一部分，以便能够以各种风格展示归纳定义。TE XMACS中的一个简单表示是：一个简单的变化，更接近数学符号可以是：用户可以在所有这些代表中自由地决定全局或局部。更重要的是，它们之间的切换也可以在TE XMACS界面中进行。从相应的来源可以在LATEX中获得相同的结果：\归纳{sum}{A，B：{\sort{Set}{{\sort{Set}{\begin{constructors}\constructor[inl]：${\arrowc{A}{{\appc{sumAB}$\constructor [inr]：${\arrowc{B}{{\appc{sumAB}$\end{构造函数}}在适当的宏定义的帮助下。需要产生的结构CO q越多，用户获得适当符号的自由度就越大。作为一个例子，人们可能想在推理规则的帮助下提出这样的归纳定义。在CO q用户手册（第4.5.1节）中，P. Audebaud，L. Rideau / Electronic Notes in Theoretical Computer Science 103（2004）37（* 集合A的元素列表 *）归纳列表[A：集合]：集合：=无：（列表A）|缺点：A->（列表A）->（列表A）。（* 此类列表的长度 *）归纳长度[A：Set]：（list A）-> nat -> Prop：=Lnil：（LengthA（nil A）O）| Lcons：（a：A）（l：（list A））（n：nat）（长度Al n）->（长度A（cons Aal）（Sn））。根据上下文，（Lcons）a：A，l：list（A），n：N（LengthA l n）a：A，l：list（A），n：N（LengthA（a.l）（n+1））或（Lcons）长度A（l）=n长度A（a.l）=n+1当上下文足够清楚时，可以在不对基础文档进行任何更改的情况下进行。这些陈述没有引起技术上的困难。相反，它们需要在C O q结构表示输出中进行更多的分解。在LATEX中，用于电感定义的构造类型可以沿着该示例的思路来准备：\构造函数[Lcons]\inferrule[a：A，l：（listA），n：nat]{（LengthAl n）}{（LengthA（consA al）（Sn）}第4.6节讨论了必须在CO q方面处理此类输出问题的其他地方。3利用TM CO q系统由几个部分组成：-C O q，它为我们提供免费的脚本解析。实际上，我们的版本是修改为允许生成TE XMACS格式。一组用于渲染的TE XMACS样式和宏。用户可以自由地定制这个包，就像LLNCS类在标准LATEXa riticlecla ss.一组用于计算LATEX和COqscr iptsexpor tation滤波器的S che m e c r e s f r e c r e s f r ec r e s f r e fr f r e c r f−−38P. Audebaud，L. Rideau / Electronic Notes in Theoretical Computer Science 103（2004）最后两个组件可从TE XMACS用户界面获得在T E X内存中重复使用LATEX内存是可行的，因为它可以提高效率。TEXMACS尚未提供将TEXMACS宏转换为LATEX macs宏的功能。出于文档目的，我们修改后的CO q分布提供了一个新的coqtop程序的包装 器，名为tmdoc。 一 般 的使用包括运行命令：tmdocMyScript.v，这将导致T E X MACS文件MyScript.tm。直接从tmdoc获得的其他输出格式是LATEX、SCHE ME。 然而，如图（1）所示，也可以通过编辑MyScript.tm。让我们通过下面两节中的两个完整的例子来进一步说明。3.1CO q标准库让我们看看CO q标准库中的theories/Init/Wf.v（*i $Id：Wf.tm，v 1.1 2003/05/27 11：30：57 paudebau Exp $i*）（** 本模块证明了- 良基递归（也称为值过程）- 良基归纳法从给定集合上的良基排序 *）需要逻辑。需要逻辑分析。（** Prop上的良基归纳原理 *）变量A：集合。变量R：A-> A-> Prop。（** 可访问性谓词被定义为非信息性 *）感应接入：A-> Prop：= Acc_intro：（x：A）（（y：A）（R y x）->（Accy））->（Acc x）。引理Acc_inv：（x：A）（Acc x）->（y：A）（R yx）->（Acc y）。NewDestruct 1; Trivial.定义了P. Audebaud，L. Rideau / Electronic Notes in Theoretical Computer Science 103（2004）39（** 信息消除：[letAcc_rec F =letrec wf x = F x wf in wf]*）C O q注释的格式为（*...*）。 文档片段由特殊注释结构（**...*）标识。这个骗局结构如下COqDOC几乎是文本约定，这有助于写作结构化的文本片段，而不需要知道太多的TE X或HTML语法而且更重要的是以独立的语法方式。因此，为了与CO qDOC风格的现有文档片段保持兼容性，我们为tmdoc添加了另一种输出格式，以使TE XMACS能够理解这些标记。这句话被翻译成（** texmacs：本模块证明了<关于我们<项>良基递归（也称为值过程有理有据归纳法从给定集合上的良基排序 *）可以看到，我们已经通过语法（**filter：.）扩展了注释作为文档的类。 * ） 其 中filter 的 范 围 包 括 coqdoc ，scheme，texmacs，latex，为了兼容性起见，默认为coqdoc。至于本地命令的翻译，我们的工具远远超出了CO qDOC功能，但代价是需要coqtop同时执行这两项功能解析和TE XMACS感知的结构化输出，如前所述。40P. Audebaud，L. Rideau / Electronic Notes in Theoretical Computer Science 103（2004）请注意，Require命令和proof不会出现，尽管它们已被翻译并仍然存在于生成的文档中我们提供了一个标签，允许一个修改所提出的材料，这是在方便完整的脚本渲染或显示此文件。不用说，TE XMACS提供了更多的选择，无论是通过现有的环境，宏，还是GUILE脚本。在这些简短的解释之后，完整的CO q标准库由我们的文档工具自动生成，作为一系列可以在编辑器中浏览的TEX宏蓝色项Acc（在引理5中）表示到定义声明Inductive 4的超链接。。我们的控制-bution包含一套完整的TE XMACS文件，可从编辑器中在线访问，并以与CO q网站上的Web文档相同的方式浏览。3.2RSA形式化RSA是一种基于素数分解的非对称公钥加密算法。它的正确性已在各种证明中得到形式化的证明，包括J. C. Almeida，andmorerececentlybyL. 是的。完整的形式化由[ 10 ]中提供的六个C O q脚本组成。在Binomials.v中，人们发现了关于二项式的著名Pascal声明：定理exp_Pascal：（a，b，n：nat）（幂（加上a b）n）=（sum_nmO n[k： nat]（多个（二项式n k）(mult（power a（minus n k））（powerb k）。虽然片段不包含任何提示，但tmdoc生成的结构足够丰富，允许用户定义宏，以便提供以下输出。然而，注意到求和并没有像人们所期望的那样使用索引k。这将是我们开发的下一阶段的一个轻微增强。简而言之，这要求宏定义可以检查其参数的结构，在我们的例子中，抓住k循环索引将其放在符号下。P. Audebaud，L. Rideau / Electronic Notes in Theoretical Computer Science 103（2004）41有关我们对这一发展所做贡献的完整介绍，所需材料可从TM CO q网站获得[4]。除了与标准库相同的文档接口外，我们的贡献还提供了一种从文件集自动生成文章的机制。这是基于一个S方案脚本，这是很容易配置。4增强功能我们最初的目标之一是保持文档的脚本部分在任何时候都可以被证明者证明的不变式。为此，我们开发了以下描述的几个功能，并基于以下备注。在引言中，我们指出CO q脚本是一个源程序，标记为注释的非活动区域是插入文档的好地方。从一个正式的发展写一篇文章给了我们另一个视角所有内容都是可打印的文本，除非宏或环境对元素有不同的处理。在克努特然而，对于普通用户来说，符号所以关键的想法是用户在工作在关于节目源编辑的双重世界中。 我们的工具将将任何程序源文件转换为双文档源文件，因为TE XMACS基本上与TE X的工作方式相同。我们从文档的TEXMACS视图中获得的另一个属性是它是强结构化的。这种结构使我们能够引入各种利益-这些功能包括与面向对象的工具的通信、Coq脚本接收、LATEXex移植以及交互式认证。之所以可行，是因为我们可以使用一种解释来处理所有这些特征模型关键思想在于根据文档的结构遍历文档。对于每个Coq相关的标签，我们根据我们的具体需要转换相应的子树。4.1一种可移植的外部XML格式关于TE XMACS文档的结构形式，必须注意的是，TE XMACS尚未使用MATH ML标准在磁盘上进行文件格式（这是其开发团队正在进行的工作）。然而，XML格式最近被引入到导入/导出过滤器中，独立，由我们为特定目的，解释后。在MOWGLI欧洲项目[11]的背景下，需要允许注释和重新组织证明片段，以使演示文稿更具可读性。由于证明来自CO q，42P. Audebaud，L. Rideau / Electronic Notes in Theoretical Computer Science 103（2004）这个特性需要一个编辑器，我们对TE XMACS的扩展是一个很好的候选者。XML是MoWGLI项目中文档的专用格式，同时大量使用样式表（stylesheets，简称CSS）作为转换语言。 因此，我们建议设立一个特定的进口/出口过滤器，对于XML。虽然我们可以决定一组特定的过滤器wrt到TM- CO q，但最好还是选择一种通用的转换方法，因为这样的文档应该允许在编辑器之外进行编辑，例如通过编辑样式表。因此，我们定义了最通用的DTD（见图4），它不限于由tmdoc生成的文档，而是将任何TE XMACS文档描述为由几个段落组成，并丰富了使用特殊的宏和环境，就像我们习惯于使用LATEX DOCUMENTS。自从我们结束了我们的实验，TE XMACS也丰富了这样的格式，虽然基于不同的观点，因此没有泛型DTD。从M O WGLI和T M C O q两方面来看，由于采用了通用的结构化方法，我们的方法足够健壮，只需要重写模板生成的输出（到样式表中）。因此，我们将为TE XMAC用户提供相同的功能。<！--texmacs.dtd --v 1.0--><！ENTITY % TeXmacs PUBLIC“-//TeXmacs//DTD TeXmacs文档//EN”“http://www-sop.inria. fr/lemme/Philippe. Audebaud/tmcoq/texmacs. dtd”><！-- 文档结构--><！ELEMENT文档（款次）+><！ELEMENT段落（宏|sym|spc）*><！ELEMENT宏（文件|款次）*><！ATTLIST宏name CDATA #必填><！ELEMENT spc空><！--处理特殊情况，如文本中的rightarrow>符号--><！ELEMENT sym EMPTY><！ATTLIST symarg CDATA #REQUIRED><！-- 符号--><！ENTITY % HTMLlat1 PUBLIC“-//W3C//ENTITIESLatin1for XHTML//EN”http://www.w3.org/TR/xhtml1/DTD/xhtml-lat1.entwww.example.com%HTMLlat1;见图4。 TeXmacs文档P. Audebaud，L. Rideau / Electronic Notes in Theoretical Computer Science 103（2004）434.2CO q脚本（再）输出在引言中，我们已经解释了在CO q正式开发和用TE XMACS编辑的文档之间来回切换的必要性。因此，需要重新导出为CO q脚本。 作为一项因此，我们还需要将文档（或非正式部分）保存到导出的脚本中，以便在之后恢复这部分，返回到文档步骤。假设我们正在处理一个从开发中生成的TEXMACS 在本文档中提供的所有材料中，我们的工具可确保任何本地命令都可以在特定宏（或环境）的帮助下完美识别，正如已经注意到的那样。因此，这是一个简单的任务（由于TE X的苹果电脑的白话命令之间的其余CO q-无关的材料内的文档.一旦被收集并转换成实际的CO q具体的syn- tax，这些文本片段就组成了CO q脚本其他一切都被视为文件。在某种程度上，这可能可以作为注释插入到脚本中，但是注释会被CO q词法分析器丢弃。为了收集源脚本中提供的文档，我们必须更改lexer行为，以便不是所有注释都被忽略。然而，在每个地方这样做，可能会导致解析器具有不合理的复杂性。我们决定采用文档和代码交替的模型，但是在本地命令中不查找文档片段可能出现在给定脚本的TEXMACS我们通过放置，确保它们不会在输出步骤中丢失在他们所处的地方，他们可以找到他们。但是，我们不能保证他们的确切位置得到保留。4.3LATEXEXPORTIONTEXM ACSalr eadysup p ortsLATEXexportation. 然而，我们所处理的问题是特殊的。因此，我们将输出分为两个步骤，第一个步骤得益于我们能够在整个文档中识别出CO q特有的片段第一步被设计成一个GUILE脚本过滤器，用户可以随意重写选择导出的材料可以在文档（源代码）内部进行本地调优，方法是在本地为特定变量赋值，遵循与将片段标记为数学、粗体或斜体相同的思想。之后，一切都交给普通人44P. Audebaud，L. Rideau / Electronic Notes in Theoretical Computer Science 103（2004）LATEXex portationfilter.从用户的角度来看，该解决方案具有良好的可操作性和足够的4.4CO q-TE XMACS让我们来看看CO q分布提供的coq-tex工具 这是一个独立的程序，其中包含在LATEX文件中嵌入的COq短语。这将为Co q v e rnacula r命令生成LATEX，由特定LATEXevironmt 标 签 （ coq_exampless 、 coq_examples* 、 coq_eval ） 标识。结果存储在临时脚本中并发送到C O q toplevel（coqtop）进行评估。根据周围的标记、命令本身或结果将重新插入到LATEX文件中。总之，使用coq-tex标记的病毒标签基于两个标准为用户提供了不同的可能性：i）要显示的本地命令，ii）其评价结果显示？只要对问题的答复是肯定的，就在适当的地方逐字印出适当的案文假设我们从一个TE XMACS文件开始，我们可以模拟相同的行为。然而，我们可以做得更多！显示的材料是没有不再局限于原始逐字格式，也不是简单的组合 两个标准。此外，由于源文档是结构化的，因此不需要准备中间CO q脚本;只要需要，可以在发送的命令之后直接插入相应的答案因此，我们的coq-texmacs基于上述导出工具实现了此功能。4.5版本模式事实上，我们非常接近提供另一个功能，我们去-通过与拼写检查器进行比较来解释。在TE XMACS内部，拼写检查器的启动方式与EMACS内部相同。也就是说，编辑器一个接一个地选择每个单词并将其发送到拼写检查器。的拼写检查器在后台启动。就拼写而言，必须在bu中隔离的（原子）项是一个单词，意思是由空格或标点符号分隔的字符序列，这取决于底层语言。现在假设拼写检查器是CO q，单词将被替换为本地命令。 但我们知道如何分离这个类的项目，因此使TE X的MAC电脑足够聪明，以正确的顺序发送每个本地命令，以一些CO q进程在后台运行。这种模式提供了一种方法来证明（底层）正式开发，站在编辑的一边。显然，预期的行为不能与拼写检查器相同。只要遇到错误，这可能会抑制P. Audebaud，L. Rideau / Electronic Notes in Theoretical Computer Science 103（2004）45认证机制将继续。事实上，语句和它们的证明之间的一些依赖信息将被证明是足够的，允许部分运行证明过程，留下我们开发中被拒绝的（子树）片段，标记为需要进一步纠正。4.6交互性由于用户在交互式编辑器中工作，因此非常希望获得许可证，这要求编辑器与CO q进程保持通信。 为了实现这个目标，我们进行了实验，TE XMACS与CO q的交互模式。在第2.1.1节中，我们已经证明，编辑器TE XMACS使用外部程序创建会话模式。要使这种与CO q的交流成为可能，需要做的很少，正如下面与CO q的对话所示。图5给出了一个示例会话。从这个例子中，我们可以得出一些有用的结论。到目前为止，我们的解释主要涉及公式。实际上，导出完整的脚本并不会带来更多困难。但是当与CO q交互时，似乎证明者真的决定了各种上下文中的呈现！的信息在验证会话期间显示的错误消息或对本地命令的回答由证明器控制最有趣的问题是关于校对。按照上面的会话，人们会期望编辑器允许用户编辑校对脚本，而不是在编辑器中积累步骤。 这是可能在TE XMACS中，由于SCHEME扩展语言并通过特定的树命令提供，以及文档被由运行的程序（以及用户或编辑器界面）修改。5结论和展望我们最初的动机是为用户提供更强大的解决方案，以记录他们的CO q正式开发。现有的工具已经提供了更有用的手段，但缺乏以科学文件的常用语言呈现这种数学或逻辑发展的能力，而且它们都不允许重大修改或甚至最终调整，同时保留基本的正式文件已由证明人证明的基本属性。在第一种情况下，我们得出结论，这是唯一可能的代价是在专用解析器后面工作由于CO q所处理的语言的复杂性，并且出于分享我们的工作和成果的目的，CO q各种输出格式，我们决定实现我们的文档generatortmdoc作为CO q源分发的一部分。现阶段46P. Audebaud，L. Rideau / Electronic Notes in Theoretical Computer Science 103（2004）图五.与TM CO q