可在www.sciencedirect.com在线获取理论计算机科学电子笔记285（2012）17-28www.elsevier.com/locate/entcs将Coq + SSRe与GAP弗拉基米尔·科曼丹茨基1 亚历山大·科诺瓦洛夫1 史蒂夫·林顿1圣安德鲁斯大学英国，圣安德鲁斯，KY16 9SX摘要我们报告的通信接口连接Coq证明助理的计算代数系统GAP使用符号计算软件可组合性协议（SCSCP）的可扩展的实现它允许Coq向本地或远程GAP实例发出OpenMath请求，并将服务器响应表示为Coq术语。保留字：Coq，GAP，符号计算软件可组合性协议，OpenMath1介绍定理证明器可以显著地扩展其功能，从与计算机代数系统（CAS）通信的能力。例子可能包括但不限于从CAS中可用的数学数据库中检索对象，或者计算结果不能单独使用定理证明器导出，但一旦知道，可以在证明器中验证或用作证明器的公理以进行进一步证明。这样的组合不仅可以加速证明器定理证明器和CAS之间现有接口的开发人员（我们在第2节中提到了其中的一些）。8）可以选择多种方式。例如，一个证明者可以写CAS输入文件，然后调用它;CAS将证明者的输入写入文件并退出;证明者将读取它并执行进一步的操作。这是可行的，但有相当严重的局限性。更好的设置可能允许证明器在其他CAS运行时与它们交互，并为每个可能的外部CAS提供单独的接口。1{vk|亚历克斯克|sal}@ cs.st-andrews.ac.uk2这项工作得到了欧盟FP 6项目026133“科学-欧洲符号计算基础结构”（www.example.com）的支持http://www.symbolic-computation.org/1571-0661 © 2012 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2012.06.00318诉Komendantsky等人/理论计算机科学电子笔记285（2012）17然而，实现这一点是一个主要的编程挑战，例如，如果另一个系统更改其I/O格式，接口将被破坏在欧盟框架VI项目“SCIENCE -欧洲符号计算基础结构”（www.example.com）中www.symbolic-computation.org开发了 它旨在为用户提供一种简单，健壮和可靠的方式来创建和消费在任何兼容系统中实现的服务，范围从通用服务（例如字符串或OpenMath对象的评估）到特殊服务（例如在数据库中查找;执行某些过程）。 这个接口实际上是一个轻量级的基于XML的远程过程调用协议，称为SCSCP（符号计算软件可组合性协议，[8]），其中数据和指令都表示为OpenMath对象，这是一个明显的选择，作为编组数学语义的常见方式。OpenMath [16]是一种成熟的可扩展语言，仅由12个语言元素（整数，双精度，变量，应用程序等）构建所有的语义都封装在内容字典（CD）中定义的符号中，并且与语言本身严格分离。OpenMath被设计成可以被计算机高效使用，并且可以用几种不同的编码来表示，其中最常用的是XML表示。SCSCP现在在几个计算机代数系统中实现，包括GAP [14]，KANT，Macaulay2，Maple，MuPAD，TRIP（详见[7，9]），并且具有API，可以轻松地将SCSCP接口添加到更多系统。这种方法的优点是，任何实现SCSCP的系统都可以立即连接到已经支持它的所有其他系统。这避免了对特殊情况的需要，并最大限度地减少了重复的请求。此外，SCSCP允许通过引用处理远程对象，这样客户端就可以处理其系统中根本不存在的对象类型。例如，要表示一个群的共轭类的数目，只需要整数的知识，而不需要群的知识SCSCP协议（当前版本为1.3）是基于套接字的。它使用由互联网电信号码管理局（IANA）分配的端口号26133和XML格式的消息。在本论文中，我们报告的原型实现的SC- SCP客户端在Coq允许发送OpenMath请求从Coq到本地或远程GAP SCSCP服务器，接收回的结果，并表示为Coq条款。这个实现提供了一个可扩展和可伸缩的框架：将来它可能支持更多种类的数学对象。此外，由于SC-SCP的灵活性，特定应用程序中的远程过程可以以某种方式设计，另一个方向可以是向Coq SCSCP服务器添加特征以允许处理来自其他应用的请求我们讨论了一个例子，涉及计算的差距的根的多项式中定义的SSRe在Sec。3 .第三章。节中第4和第5，我们给出了位于SSRe代数层次结构背后的Coq的两个特征：诉Komendantsky等人/理论计算机科学电子笔记285（2012）1719典型结构[20]。节中6，我们描述了我们的方法，根据该方法，用户负责为Coq调用编程+ SSRe引用GAP，因为它们指定了OpenMath如何请求GAP由Coq中的数据以及传入的OpenMath对象如何转换为Coq术语形成。特别地，OpenMath对象是使用由子类给出的子类信息构造的，而从给定OpenMath对象合成Coq项则重用规范结构机制。我们允许手动定义Coq术语，为在两个系统之间执行数据交换2从OpenMath到Coq的翻译从XML数据的翻译，尊重（Co-））归纳结构（pCic;参见[20]，第4章）到Coq可以很简单，尽管是例行程序[1]。相反，计算机代数系统（如GAP [5，10]）发送的数据的表示似乎存在一个中心问题。也就是说，pCic的对象是项;甚至证明也是由更小的项构造的项。问题是如何解释可以打包在OpenMath对象中的任意非pCic数据。这样的数据可能不对应于术语，因为计算机代数数据通常不是构造的，而是给定的，我们无法建立如何获得OpenMath对象中的值的构造性证明。这种表示的一种可能方法是将OpenMath数据转换为公理或值（后者是Sec.8个，S。Ould-Biha [17]）。因此，不需要证明如何获得值。具有这种功能的Coq扩展并没有增加证明的便利性如果可以从Coq证明模式内部调用GAP，它可以是一个方便的捷径，允许在不尊重构造性要求的情况下成功进行一些证明，也就是说，这样的证明将基于公理。我们可以正式地为Strong OpenMath（OpenMath的一个严格子集）因此，有可能通过形式分析将Strong OpenMath 然而，我们没有看到一种方法来限制或转换为强OpenMath的GAP生成的对象集。为了忠实地将给定的OpenMath对象转换为没有公理的纯pCic，需要用pCic来表示该对象。例如，如果GAP计算一组排列，则必须对pCic中的一组排列进行构造性定义，而不是可能是此类组的外部GAP表示的数字数组。我们倾向于认为，如果我们采用在SSRe [11]中已经存在的群论定义，这是可能至少部分满足的。然而，许多这种类型的构造对象依赖于证明（例如代数性质的证明），这使得完全自动化的翻译是不可能的。因此，某种形式的用户交互仍然存在。20诉Komendantsky等人/理论计算机科学电子笔记285（2012）17必需的.SSRe是基于有限域上的问题的构造性可解性，使用二值布尔逻辑（与无限值构造性逻辑相反）。因此，可以将Prop类的有限问题简化为等价的bool，具有由以下反射关系提供的归约概念感应反射（P： Prop）：bool -> Set：=| ReflectT：P->reflectP true| ReflectF：~P ->reflectP false。这具有深远的影响，因为这可以降低有限代数结构库中证明的复杂性[11]。3工作示例：多项式在SSRe 1.2中，环上多项式的定义如下：记录多项式（R： ringType）：类型：=Polynomial {polyseq：> seq R;_：last1 polyseq！=0}。一个多项式可以被看作是一个最后一个元素为非零的序列。强制polyseq的类型为R：ringType，polynomial R→seq R，它将环上的多项式转化为该环上的序列（同构于普通列表）例如，考虑有限集合上的算术模自然n{0，1，.，n− 1}，域Z / 3 Z上的多项式p（x）= x3− 1使用在模算术库zmodp.v中定义的域类型Fp_field（继承自ringType）构造。多项式p（x）可以被强制为一个序数序列，而序数序列又可以被强制为一个自然数序列缺点2（缺点0（缺点0（缺点1无）另一方面，要在GAP中构造这样的多项式并找到它的根，应该执行以下步骤：gap> x：=Indeterminate（GF（3），“x”）;; gap> f：=x^3-1;x^3-Z（3）^0int f（f）;[Z（3）^0，Z（3）^0，Z（3）^0]我们将在第二节中回到这个例子。图6和图7示出了由Coq发出的SCSCP过程调用和来自GAP服务器的对应响应4使用子类进行在类型论证明系统中，类型检验是一个判断一个类型判断是否可根据系统规则导出的问题。虽然这个问题在一般情况下是不可判定的，但对于大多数感兴趣的系统，特别是内射系统，它是可判定的[4]。在校对助手中，这项工作被委托给称为类型检查器的模块。另一个相关的问题是类型推断。它包括推断用户没有明确指定的类型，也就是说，合成或约束这些类型中省略的子项。我们特别感兴趣的是类型理论证明助手识别数学符号滥用的能力，诉Komendantsky等人/理论计算机科学电子笔记285（2012）1721在必须在不同的层次上观察同一数学对象的情况下是非常方便的（例如，在诸如SSReact之类数学理论的分层实现中）。这种能力是由称为精炼器的模块提供的。子类型关系≤是在pCic中推导出来的，以方便证明。它可以使用以下规则来表征：E[Γ]t：A E[Γ]cA，B：A≤BE[r]（cA，B t）：B这可以用pCic来定义[19]。一个继承类（class）要么是一个类型为x1：A1的项.（xn：An），s，n个参数，或抽象继承类SORT和FUN之一，分别是排序类和函数类。从terms到继承类的部分函数ClassOf定义如下：ClassOfs=SORTClassOf（A，B）=FUNClassOf（C t1. t n）=C如果C是一个有n个参数的类未定义，否则给定类C和D分别具有n和m个参数，项f可以被声明为具有域C和余域D的强制，表示为f：C>D，如果其类型具有以下形式：（x1：A1）... （x n：A n）（y：（C x1. x n）），（D u1. （m）C既不好玩，也不好玩。 设t：C t1. t n是类C中的类型良好的项。 我们可以将f对t的应用定义为f @ t = f t1. 不不。该 应用的类型被表示为f{t}，并且是D uJ1.uJm在哪里uJi = uJi [y：= t][x n：= t n]. [x1：= t1]对于1≤i≤m。类继承图Δ将类作为节点，将这些类之间的子作为边。一条强制路径由k个初等子的合成给出，对k ≥ 0，即f1<$··<$fk. 当在Δ中存在从C到D的强制路径时，类C被称为D在Δ中的子类。也有人说C继承自D。该图表示为一个子对象列表;类和路径是推断。具有继承的类型检查算法将环境E、上下文Γ、强制图Δ和项t作为输入，并输出显式项tJ和T，使得tJ：T通过将适当的子项应用于t（也称为隐式项）而获得。对此的类型判断可以写成E[Γ]Δ ttJ：T。为了将隐式项转换为显式项，在[19]中定义了一种算法来插入适当的子。仅当22诉Komendantsky等人/理论计算机科学电子笔记285（2012）17J这个问题不是以明确的形式提出的。该算法是部分的，如果案例匹配不成功，则会失败。类型化算法的以下属性是已知的：• 算法的正确性：如果E[Γ]Δt∈tJ：tJ，则t是良型项，T是它的推断类型;• 关于隐式类型判断的扩张的保守性：如果E[Γ]≤t：T，则对所有的凝聚图Δ，E[Γ]Δ≤t≤t：T。5规范结构提示在[2，18]中介绍了一种统一提示的一般方法 一般统一提示具有以下形式：？x1：= H1.？xn：= H nPQ其中PSQREQ是一个带有自由变量的类型等价模式？v这样，{？x1，.，？xn}？v、所有？xi是不同的，并且Hi不能依赖于任何模式变量？xj，其中1≤i≤j≤n。在Coq中，有一个专门的机制来处理特定类型的统一问题。π？一... ？n.其中π是由记录类型的声明创建的投影器之一，？1、......、？n（部分）未知参数，t是应用于参数的该投影的已知值这种机制是由规范结构提供的规范结构[20]是一个有目的地标记的记录实例（可能在最顶层包含函数抽象）。类型检查器在试图解决统一问题时使用这些标记的实例。这可以用下面的规则来表示：π=水头常数t？1：= t1.？n：=tn π？一... ？n.其中t1，.，t n是作为t的首常数的参数出现的项。Coq中的实际实现还有其他方面，例如统一策略（例如，定义常数的延迟展开）和函数记录的处理下面的例子引用了SSReact的标准相等类型，其定义遵循SSReact类混合设计模式，然后在标准类型nat上声明相等结构的统一提示：模块相等。定义公理mTe：=for allxy：T，reflect（x=y）（exy）. 结构mixin_of（T：Type）：Type：= Mixin {intT;_ ：axiom op}。表示法class_of：= mixin_of（仅解析）。结构类型：Type：=Pack{sort：> Type;_：class_of;_：Type}。诉Komendantsky等人/理论计算机科学电子笔记285（2012）1723...定义packTc：=@PackTcT。结束平等。定义eq_opT：= Equality.op（Equity. class T）。引理等式：等式.公理等式................Qed。规范结构nat_eqMixin：=相等。规范结构nat_eqType：=Equality中的Eval hnf.pack nat_eqMixin.由于声明了nat_eqType，符号@eq_op _ 0 1（省略了隐式类型参数）将被类型化为@eq_op nat_eqType 0 1后者是βιδ-可转换的，其中eqn是类型上的布尔等式，nat在SSRe中定义。6用户界面假设我们正在向GAP服务器提交一个请求来计算根在SEC中的多项式。3 .第三章。 获取OpenMath对象的过程 由于强制图，多项式相当简单。在这个对象中，我们拥有有限域的原始元素的幂，这些元素本质上是OpenMath整数。为了表示它们，用户提供以下映射：• 从相关的SSRe取幂场运算，如环取幂（由场结构继承）到由适当的内容字典和字典场组成的对（在取幂的情况下，分别是算术1和幂• 从SSRe的序数到OpenMath的整数（通过提供从序数到nat类型的强制转换）。还应该提供从多项式到OpenMath字典字段的类似映射。映射由Coq术语表示，OpenMath字典和字典字段的名称在Coq中定义。这些标识符由策略处理，并为XML字段名称获得相应的字符串值。在发送了一个请求的多项式从例子中。3到GAP服务器，如我们在第节中所述。7，策略应该接收包含以下对象的响应，对应于字段Z/3Z的三个乘法中性元素的列表： OMI>3/OMI>0/OMI>...... OMI>3/OMI>24诉Komendantsky等人/理论计算机科学电子笔记285（2012）170/OMI>为了将其表示为Coq术语，用户应该在Coq中的OpenMath内容字典中为相应条目定义一般来说，OpenMath对象在Coq中的表示在很大程度上取决于上下文。因此，不可能有一套固定的翻译规则。相反，我们应该为用户提供定义适当映射的方法例如，假设上下文需要将此对象表示为包含字段Z/3Z的元素的seq。为此，我 们 可 以 使 用 模 算 术 库 zmodp.v ， 其 中 这 样 的 序 列 将 被 类 型 化 为 seq（Fp_fieldpp），对于p：nat和pp：prime p。 OpenMath实体列表将映射到类型forall（T：Type），seq T。然后，用户必须满足证明义务素数p，对于给定的p。为了将乘法中性元素表示为Coq项，可以使用SSRe中定义的规范结构提示，与场地的类型有关。如何在一般情况下做到这一点的问题是一个有趣和具有挑战性的研究问题。7战术实施我们正在开发一个策略实现，用于Coq和GAP服务器之间的数据交换，后者应该使用GAP包SCSCP和OpenMath [6，14]启动。该策略被实现为一个Coq插件模块，可以通过Coq命令语言请求进行动态加载主客户端函数发起TCP/IP套接字连接，根据SCSCP规范执行握手，并评估客户端回调函数。后一个函数使用作为策略参数提供的数据，通过输出I/O通道编写并发送SCSCP请求，刷新输出通道并接收回包含服务器响应的SCSCP数据包。所有SCSCP数据包都包含一系列OpenMath XML对象，并包含在强制性的开始和结束标记中。因此，接收相当于从输入通道读取这些标记之间的所有OpenMath数据并解析数据。请求包和响应包具有类似的结构。例如，请求从Sec找到多项式的根3可能有形式诉Komendantsky等人/理论计算机科学电子笔记285（2012）1725 OMSTR>host：port：pid：string/OMSTR><公司简介 OMS cd=“setname2”name=“GFp”/> OMI>3/OMI>/OMA> OMI>3/OMI>0/OMI>3/OMI> OMI>3/OMI>0/OMI>2/OMI> OMI>3/OMI>0/OMI>1/OMI> OMI>3/OMI>1/OMI>0/OMI><公司简介这样的远程过程调用总是携带一个必须相同的调用ID在请求和响应中。调用ID由服务ID（主机、端口和进程ID）和客户端生成的随机字符串组成，服务ID是客户端在会话开始时的握手阶段从服务器获得的。然后为每个接收到的OpenMath对象检查此调用ID26诉Komendantsky等人/理论计算机科学电子笔记285（2012）178相关工作Harrison和T'ery用HOL定理和计算机代数系统Maple [12，13]之间的数据交换进行了扩展，特别是涉及Maple中实现的强大但模糊的提出了计算机代数程序的证明者可信度的概念。这个学位应该反映对解释计算机代数系统返回的计算值值得注意的是，已经在HOL的情况下，最合适的信任程度是最低的，即“完全不信任”。 这种选择首先是出于正确性的考虑，其次是定理证明器的项结构中隐含的约束由于计算值无论如何都必须重新组装为HOL项，因此发布一些正确性证明目标并将其委托给HOL用户是非常明智的。我们遵循类似的方法，使项对值和证明的依赖性稍微更明确。最近，S. Ould-Biha用C编写了一个有限的外部策略3coq_gap，使用库xml 2以安静模式执行GAP解释器，并通过Unix管道进行通信[17]。Coq脚本的一个示例如下：定义gap_fun： nat -> nat. intron.让x：= external“coq_gap”“Fun”n在精确的x中。定义了第三行是gap_fun n是自然数的存在性证明因此，gap_fun n等于x，它等于GAP解释器中调用Fun（n）;的字符串到自然值的转换值。事实上，由于一些内部限制，例如对nat → nat类型函数的限制，很难看到这种方法如何有效地推广到更一般类型的函数上。外部策略[20]在Coq接口中无处不在。它语法如下：外部“命令”“请求”arg_1. argn以下形式的XML树被发送到外部命令的标准输入：<请求req=“request”>第一个参数的XML树...最后一个参数的XML树<联系我们外部命令必须在其标准输出上发送以下格式的XML树：术语XML树<联系我们或者，如果回应是战术呼叫而不是术语，<调用uri=“ltac_qualified_ident”>第一个参数的XML...最后一个参数的XML树<联系我们[13]的作者可能会把这种策略称为桥梁。诉Komendantsky等人/理论计算机科学电子笔记285（2012）1727其中ltac_qualified_ident是Coq策略语言中定义的函数的名称，每个XML子树递归地是CALL或TERM节点。基于外部基础设施，由于H.Herbelin更新了一个较早的版本，由于M。Mayero和D.Delahaye [15]. 这个接口以类似于S的方式依赖于外部乌尔德比哈策略external在Coq中解释外部数据之前这是统一的，但不一定有效在中间数据不符合pCic DTD的情况下，可以通过其他方式自然地传递给Coq。在这方面，与Coq通信的日常示例，如本地CoqIDE [20]和ProofGeneral [3]，一个用于证明助手的Emacs前端，可以在那里表示通信数据的方式中提供灵感9结论我们讨论了一种设计模式，可用于将OpenMath数据解释为Coq的SSReplect库中的对象 我们正在Coq策略中实现这种设计模式。 目前，它对提供Coq-GAP接口的通信层的SCSCP协议提供了必要的支持。这一版本将在科学项目网站（http：//www.science）上提供。 symbolic-computation.org/），并将在那里发布进一步的更新。需要更多的工作来解释Coq从GAP收到的OpenMath数据，因为当前的实现只会逐字或至少接近逐字地呈现GAP响应。 我们希望在可观察的未来解决的其他相关问题包括使用GAP作为SSRe的搜索引擎，这将有助于找到有用的代数对象或检查属性，而无需实际定义Coq中的搜索算法。引用[1] Alberti，A.，L. 帕多瓦尼角我和萨塞多蒂·科恩Schena，HELM and the semantic Math-Web，in：TPHOLS 2001，LNCS2512（2001）。[2] Alberti，A.，W.里乔蒂角Sacerdoti Coen和E. Tassi，统一提示，在：Proc. TPHOLs 2009，LNCS5674，Munich，2009，pp. 84比98[3] 阿斯皮纳尔，D.， ProofGeneral，http://proofgeneral.inf.ed.ac.uk/。[4] Barthe，G.，类型检查单射纯类型系统，J. Functional Programming9（1999），pp. 675[5] Breuer，T.和S. Linton，GAP 4类型系统：组织代数算法，在：ISSAC38-45.[6] Costantini，M.，A. Konovalov和A.Solomon，http://www.cs.st-andrews.ac.uk/“OpenMath - OpenMathfunctionality in GAP，Version 10.1，”（2010），GAP package，www.example.com~alexk/openmath.htm.[7] Freundt，S.，P. Horn，A. Konovalov，S. Lesseni，S. Linton和D. Roozemond，OpenMath inScience：Evolving of Symbolic Computation Interaction，in Proceedings of OpenMath Workshop2009.[8] Freundt，S.，P. 霍恩，A.Konovalov，S.Linton和D.Roozemond，符号计算软件可组合性协议（SCSCP）规范，http://www.symbolic-computation.org/scscp，版本1.3，2009。28诉Komendantsky等人/理论计算机科学电子笔记285（2012）17[9] Freundt，S.，P. Horn，A. Konovalov，S. Linton和D. Roozemond，Symbolic computation softwarecomposability，in：AISC/MKM/Calculemus，Springer LNCS 5144，2008，pp. 285-295.[10] GAP Group，//www.gap-system.org网站。[11] Garillot ， F. ， G. Gonthier ， A. Mahboubi 和 L. Rideau ， Packaging mathematical structures ， in ：Theorem Proving in Higher Order Logics（2009），LNCS5674，2009.[12] Harrison，J. 和L. 今天， 我们来谈谈现实：霍 尔 的婚姻，在：A。 Voron kov，编辑，逻辑编程和自动推理：第四届国际会议论文集，LPAR' 9 3 ， 计 算 机 科 学 讲 义 6 9 8 （ 1 9 9 3 ） 。[13] Harrison，J. 和L. Ther y，Askeptic's app roach to combining HOL and Maple，Journal ofAutomated Reasoning 21（1998），pp. 279-294。[14] 科诺瓦洛夫，A.和S. Linton，http://www.cs.st-andrews.ac.uk/“SCSCP - Symbolic ComputationSoftware Composability Protocol，Version 1.2，”（2010），GAP package，www.example.com~alexk/scscp.htm.[15] 马耶罗湾和D. Delahaye，AMaple mode for Coq，http://coq.inria.fr/contribs/MapleMode.html.[16] OpenMath，http://www.openmath.org/。[17] Ould-Biha，S.，Coq有限群表示理论，第八届数学知识管理国际会议（2009），2009年。[18] Sacerdoti Coen角和E. Tassi，Working with mathematical structures in type theory，in：Proc. TYPES2007，LNCS4941，Cividale del Friuli，Udine，Italy，2007，pp.157-172.[19] S bi，A.，在具有继承性的类型理论中，键入算法为：P roc。 POPL'97，1997，pp. 292-301[20] Coq开发团队，Coq证明辅助参考手册，http://coq.inria.fr/refman/。
我的内容管理
展开
