理论计算机科学电子笔记269（2011）41-54www.elsevier.com/locate/entcs一般显式替换演算计算特性可视化的灵活框架5F. L. C. deloua，A. 诉 Bar bosa，M. Ayala-Rinc'on1，2，3DepartamentodeCipouchadaComputapouchaoUniversidadedeBras'ılia布拉西利亚、布拉齐尔F. Kamareddine4赫瑞瓦特大学苏格兰爱丁堡摘要SUBSEXPL是一个系统，最初开发用于可视化显式替换的三个重要演算中的约简，简化和规范化，并已被应用于理解和解释属性并比较了用de Bruijn符号实现λ-演算时，显式化替换运算的不同方式。 该系统是在OCaml中开发的，现在它可以可以在Emacs编辑器中以一种新的模式执行，这种模式允许非常容易的交互。特殊符号的使用使得它的应用程序对学生非常有用，因为屏幕上的符号一样接近尽可能地在纸上。除了处理λ演算和显式替换演算外，在de Bruijn符号中，现在可以使用λ演算和几个显式替换演算，也可以使用变量的名称表示。此外，与系统的原始版本相比，该版本仅限于三个显式替换的特定演算，新版本允许通过给出新演算的语法描述作为输入来包含新演算。 SUBSEXPL已被使用成功地教授了λ-演算的基本性质，并说明了计算的影响选择一种变量的表示（名称或索引），以及在基于λ演算的实际实现中进行显式替换关键词：项重写系统，显式替换演算，λ演算1电子邮件：flaviomoura@unb.br2电子邮件：alexvicentebarbosa@gmail.com3电子邮件：ayala@unb.br4电子邮件：fairouz@macs.hw.ac.uk5.由联邦行政区APesquisa基金会支持的工作-FAP-DF8- 004/20071571-0661 © 2011 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2011.03.00442F.L. C de Eschericha等人/理论计算机科学电子笔记269（2011）411引言系统SUBSEXPL [14]是在OCaml中开发的，作为一个系统来模拟和比较de Bruijn符号（变量作为索引）中显式替换的演算在这项工作中，我们提出了这个系统的扩展，它具有许多额外的功能，通过Emacs内部的专用使用简化了用户交互，允许将变量作为名称处理演算，并且比原始系统更灵活，因为现在可以通过输入语法描述来插入新的演算。在过去的二十年里，在显式替换领域已经做了大量的工作[27，1，7，23，31，3，21，12，18，16，2，15，26]。这些发展已经说明了显式替换演算对于实际概念的有用性，例如类型化函数式编程语言[30，35，20]和高阶证明助手[11，33，9，6]的实现SUBSEXPL专注于模拟不同结石的重写规则[5其中一些演算是使用deBruijn索引开发的，这些索引非常适合实现，因为人们不必处理α-等价，其他演算使用名称。命名表示法对人类很好，但α-等价类需要小心对待。最初，SUBSEXPL实现了三个使用de Bruijn索引的重要演算（在[2]中借助早期系统原型进行了(i) λσ-风格[1]引入了两个不同的实体集：一个用于术语，一个用于替换。(ii) λs-风格[23]利用了de Bruijn的Au- tomath [ 32 ]的哲学，该哲学指出，术语是由应用（应用于参数的函数），抽象（函数），替换或更新构建的。这种哲学的优点包括尽可能地接近熟悉的λ演算（cf. [22]）。(iii) 悬浮演算[31]，它引入了三个不同的实体集：一个用于术语，一个用于环境，一个用于环境列表本文中SUBSEXPL的新扩展，即所谓的SUBSEXPL 2.0，允许在de Bruijn或命名符号中只需几步就可以定义新的演算通过这种方式，用户可以玩他/她自己的演算，模拟归约和归一化，导出latex代码，并拥有原始实现中不可用的一方面，涉及显式替换演算的几个重大挑战已经得到解决，但另一方面，人们可以说它们还没有完全理解，因为演算的重要属性还不知道：悬置演算[31]是否保持强正规化（PSN）仍然是一个悬而未决的问题此外，开发de Bruijn符号的显式替换演算具有实际意义，它同时满足下面给出的特性[29]。事实上，就在最近，一种满足所需计算性质的显式替换演算被开发出来[26]。期望的F.L. C de Eschericha等人/理论计算机科学电子笔记269（2011）4143λc显式替换演算的性质，比如λc，包括：(a) 一步β约化的模拟：如果t→βtJ，则t →+tJ。(b) 开项上的一致性（CR）（也就是闭项上的一致性）：如果我们用所谓的元变量扩展微积分的语法，并且M是一个元变量可能同时发生的项，那么，如果M1<$λc<$M→<$λcM2，那么存在一个λ-项M3，使得M1→<$λcM3<$λc<$M2。(c) λc-型项的强正规化（SN）：如果λc-型项可以被类型化，那么t没有无限约简。(d) SN的保持性（PSN）：如果λ-演算中λ-项t的所有约化都是有限的，那么λc演算中t的所有约化也是有限的(e) F或所有条件t，tJ和变量x，t[x/tJ]→Δλct{x/tJ}。换句话说，隐式替换实现了显式替换。SUBSEXPL的特点之一是它有助于理解这些属性。本文的组织如下：完整的描述新版本的SUBSEXPL是在第2节。 在2.1小节中给出了一个如何用命名符号定义新微积分的例子。在2.2小节中给出了de Bruijn符号中的微积分以及著名的Mell i`es反例。在2.3小节中，我们举例说明了该系统在教育方面的应用。我们在第4节结束。2SUBSEXPL的描述SUBSEXPL 2.0 是 一 个 OCaml 实 现 ， 它 使 用句 法基 于 预 处 理 器 Camlp 5（www.example.com/camlp5/）提供的修订语法的扩展http://pauillac.inria.fr/。它允许以一种简单的方式定义新的演算及其重写规则，因为它实现了一个基于一阶签名的通用术语概念[5]，由下式给出类型表达式=[字符串和数组表达式T| String[String];此外，还描述了避免替换的（Meta）捕获的概念，由{x：= N}，以及显式一元替换。元替换根据修改后的语法实现如下：value rec replace（x，n）term=match term with[V_ when x = term -> n| V_-> term|：> when y = x-> term| <：generic< L（^y，^m，^t）>> when not（List.（Variable.free_variables n））->44F.L. C de Eschericha等人/理论计算机科学电子笔记269（2011）41设m =replace（x，n）min<：generic L（^y，^m，^t）>>| <：generic>->let fv= Variable.free_variables：genericA（^n，^m）>> inletname = ref（Variable.next_name y）inletz = do {while（List. valid.val fv）do {name.val：= Variable.next_name name.val};name.val }在letm =replace（y，z）min let m =replace（x，n） m在<：generic L（^z，^m，^t）>>| T nameargs ->T name（Array.map（replace（x，n））args）]显式替换的实现概念，其保留符号为[x：= N]，允许定义使用一元替换的显式替换的新演算在下一节中，我们提出，作为一个例子，显式的微积分用这样的一元替换。该演示文稿是用户友好的，因为它尽可能接近纸和铅笔表示，并且像λ和箭头这样的非asshole符号由与SUBSEXPL一起安装的x-symbol包提供。使用的接口是GNUEmacs系统（http://www.gnu.org/software/emacs/），它是一个可扩展的文本编辑器，支持文本编辑。开发了一个SUBSEXPL emacs模式，以允许一种更简单的方法来执行约简。这个emacs模式，如图1所示，允许对一个表达式、一个区域或整个缓冲器进行求值，以及启动/中断或终止SUBSEXPL交互模式。SUBSEXPL命令可以直接在SUBSEXPL交互模式下执行，也可以在subsexpl文件中键入（即，在评估之前，请使用extension.se文件在下一小节中，我们可以看到在SUBSEXPL系统中用名字和一元替换来定义一个微积分是多么容易2.1λex演算λex演算[26]是一种使用命名符号的显式替换演算。λex演算是通过扩展λx演算[27，34，7]得到的，其中一个重写规则指定相关替换的合成，一个方程指定独立替换的交换，如下所示：t：：= x|（t t）|（λx.t）|t [x/t]t[x/u][y/v] =Ct[y/v][x/u]，如果y/∈fv（u）x/∈fv（v）F.L. C de Eschericha等人/理论计算机科学电子笔记269（2011）4145Fig. 1. SUBSEXPL菜单（λx.t）u→Bt[x/u]x[x/u]→变量ut[x/u]→Gct，如果x/∈fv（t）（t u）[x/v]→Appt[x/v]u[x/v]（λy.t）[x/v]→Lamλy.t[x/v]t[x/u][y/v]→Compt[y/v][x/u[y/v]] 如果y∈fv（u）给出了SUBSEXPL系统中λex演算的具体化在图2中 在开始时加载的经典语法的选择图2顶部显示的lambda文件ex.se允许用户以命名符号定义微积分。规则的表示完全遵循“纸和笔”的为了从具有条件规则的系统执行正确的归约，系统将条件规则何时真正适用的决定作为 一个举例来说， 考虑 的（一步） 减少的的term（λx. （xy）（λyz. （z λu.u）w，如图2底部所示。命令#match-rules将迄今为止定义的所有规则与给定术语进行匹配。 系统列出了所有的规则，以及可以应用到条件的相应位置;在这种情况下，只有B规则可以应用到术语的根位置（用表示）。为了在词根处应用规则B，我们使用命令#→B（类型为#\toB\）和reduce（xyλy. λz.zλu.u）[x：=w]的显示与纸和铅笔的显示完全相同。此时，命令#match-rules返回规则App和Gc都可以被46F.L. C de Eschericha等人/理论计算机科学电子笔记269（2011）41图二. λex演算的一个简化应用于当前项的根。由于Gc是一个条件规则，用户必须首先检查条件是否满足。在这种情况下，它是不满足的，因为变量x在项（xyλ y）中有自由出现。λz.zλu.u），唯一的选择是应用规则App，我们得到项（x y）[x：=w]（（λy.λz.z λu.F.L. C de Eschericha等人/理论计算机科学电子笔记269（2011）4147u）[x：=w]）。此时，命令#match-rules在位置1返回一个App-redex，在位置1和2返回两个Gc -redex，在位置2返回一个Lam-redex。由于边条件，规则Gc不能应用于位置1，但我们可以应用于位置2，因为x不在项λy中。λz.zλu. 联合待定替换[x：=w]需要在子项x和y上传播，最后在应用Gc和Var之后，我们得到范式w yλy。λz.zλu.u. 在此之后，可以看到命令#match-rules返回一个空字符串，因为没有剩余的redex（可还原表达式），并且没有规则可以应用。命令可以在SUBSEXPL交互模式下直接输入，但是如果存储规则和归约很重要，那么所有这些信息都必须输入到扩展名为.se的文件中（参见。图2）。图三. λσ-演算2.2德布鲁因记号微积分所谓的de Bruijn符号[13]使用索引来表示绑定和自由变量。在这种表示法中，自由变量存储在一个表示术语上下文的列表中，其引用对应于其在该列表中的位置。例如，λ项λxy.xv（λz.yxzw）在上下文[v，w]中表示为λλ 2 3（λ2 3 1 5），在上下文[w，v]中表示为λλ 2 4（λ2 3 1 4）。作为de Bruijn符号中的微积分的一个例子，考虑由以下定义的λσ-微积分[1]：以下语法和规则：术语t：：= 1|（t t）|（λt）|t [s]替换s：：= id|↑ |a.S|ss48F.L. C de Eschericha等人/理论计算机科学电子笔记269（2011）41λσ（Beta版）（应用程序）（λab）（a b）[s]−→−→a[ b· id]（a）（b）（绝对值）（λa）[s]−→λ（ a[1·（ s<$↑）]）（克洛斯）（a[s]）[t]−→a[ s]（VarCons）1[a·s]−→一（Id）a[ id]−→一（阿森松岛）（st）−→s（t u）（地图）（a·s）t−→a[ t]·（s t）（国际标准升）身份证号码−→S（IdR）S型−→S（ShiftCons）天（a·s）−→S（VarShift）1·↑−→ID（SCons）1[s]·（↑s）−→S（埃塔）λ（ a1）−→B如果 a=σb[↑]λσ-演算的重写系统直接在文本文件中定义，扩展名（.se），如图3所示。 指令#select-output-syntaxsigma和#select-input-syntaxsigma涉及语法的定义。前一个指令定义了SUBSEXPL在buffer中输出术语的方式，后者定义了输入语法。这种简单而友好的交互使我们能够提供比以前版本的系统[ 14 ]更可读的Melli`es的coun ter-example演示2.2.1Melli`esc反例在[28]中，Mell证明了λ σ-演算不存在强正规化. 这个证明包括通过规则的适当组合，从良型的λ-项λ（（λ（λ1）（（λ1）1））（（λ1）1））建立一个无限导子。 在图4中，我们可以看到这个无限推导的初始步骤，它的符号与在纸上做的符号完全相同。这个推导对应于[28]中提出的重复引理的两个应用。重复引理指出，对于任何λ-项t，（λ 1）1·idt→+1[1[t]·t↑（1[t]·id）]·t. 在图4的第7行中，生成项包含（λ1）1·id<$（λ1）1·id作为子项，该子项是在两个规则beta的应用，之后是将两个待定替换组合成一个新替换的规则beta。通过重复引 理 ， 这 个 子 项 简 化 为 1[1[ （ λ1 ） 1·id]· （ （ λ1 ） 1·id ） <$↑ <$ （ 1[ （ λ1 ）1·id]·id）]·（λ1）1·id，它是第25行中项重复引理的应用是一个序列由规则map、app、idL、abs、beta、map、varCons和ascurl的应用程序按此顺序给出的9个重写步骤。 在图4中的简化之后，可以看到重复引理的两个连续应用：第一个从第8行开始，在位置12处应用规则映射，F.L. C de Eschericha等人/理论计算机科学电子笔记269（2011）4149（λ1）1·id在一个项列表上的替换。在位置123处应用的app规则在应用上传播替换（λ1）1·id。位置122处的规则idL移除替换组合的左侧中的替换id的出现。在位置1231处的规则abs生成在位置121处的新的β-redex，其在下一步骤中被缩减。 两个结尾替换1·（（λ1）1·id）↑和1[（λ1）1·id]·id通过规则的应用在位置121处组合。在位置1212处的映射的下一个应用将子项1[（λ1）1·id]·id传播到项的列表上，并且在位置12121处的规则varCons消除了替换id，并且最终在位置12122 处应用的规则ascons生成具有1[1[（λ1）1·id]·（（λ1）1·id）1[（λ1）1·id]·（λ1）1 · id的项作为子项，该子项对于t =（λ1）1 · id具有精确的期望形式1[1[t]·t（1[t]·id）]·t。这种表示的优点是在subsexpl emacs模式中表示的类似lat的符号通过这种方式，更容易遵循也可以作为乳胶文件导出的缩减。2.3用SUBSEXPLSUBSEXPL 系 统 已 用 于 研 究 生 和 本 科 生 的 （ 非 类 型 ） λ- 微 积 分 教 学 。 由 于SUBSEXPL使用的符号与课堂上介绍的符号完全相同，因此该工具对学生来说是一个非常有用的支持。最初的例子，使学生认识到如何基本的操作可以在一个语言与语法一样简单，如M：：= x|（男、女）|（λx.M）涉及与所谓的丘奇数的运算，丘奇数是λ -演算中将自然数编码的λ -项，如下所示：Cn<$λfx.f（f（f.（ fx） ， 其中抽象的主 体具有参数 f的n 次出现。在图5的顶部，可以 看到www.example.com文件，其中包含β-和η-约化的演示。church.se在同一文件的下一行中，标识符用于编码任意λ项：例如，λ项λx y. yx 表 示 Church 数 的 指 数 运 算 符 ， 通 过 输 入 Aexp\equiv\lambda x y 来 识 别Aexp。y x. 同样，第二个和第三个教堂数字在www.example.com文件中被C2和C3church.se。作为一个运行的例子，我们将计算表达式Aexp C2 C3，它将计算C2的幂C3的指数。运行subsexpl顶层并将所有标识符替换为相应的λ-term（#expand-macros）后的结果如图5底部所示。定义的规则（在本例中是β和η）可以应用的位置由命令#match-rules列出：最初，在位置1只有一个β-redex，没有η-redex。可以逐步执行约简，或者可以应用归一化策略，并且系统输出以范式结束的整个约简教授λ-演算的充分性也可以使SUBSEXPL的使用受益。使用标识符来表示复杂的长λ项，可以清楚地表示像递归这样的重要概念。事实上，在图6的顶部，可以看到一个简短的介绍，介绍了由定点运算符Y和更基本的结构（如谓词ISZERO，检查其参数是否为Church数零）构建的阶乘函数，乘法运算符MULT和前置运算符。50F.L. C de Eschericha等人/理论计算机科学电子笔记269（2011）41图四、Melli`es的反例F.L. C de Eschericha等人/理论计算机科学电子笔记269（2011）4151图五. 邱奇数函数PRED。图6的底部示出了项FACT C3的相当长的计算的尾部，其对应于3的阶乘：如预期的那样，缩减的最后一项是Church数6。这样的结构可以一步一步地完成，学生现在可以遵循更复杂的结构并运行自己的示例。3相关工作非平凡的重写约简通常难以手工模拟。这推动了几种重写工具的发展[10，8，25]，每一种都有特定的功能来处理（术语）重写系统。SUBSEXPL系统有一些52F.L. C de Eschericha等人/理论计算机科学电子笔记269（2011）41图第六章 关于λ-演算的表达能力与这些系统的相似之处在于重写系统的模拟;像CIME这样的系统专注于连续性和终止性的证明，而SUBSEXPL专注于显式替换演算的模拟和比较。特别是，SUBSEXPL打算填补缺乏教学λ-演算及其显式替换扩展的所提出的版本在这项任务中非常成功，因为所使用的符号与纸上使用的符号完全相同使用SUBSEXPL来教授λ-演算和显式替换演算，通过使用x-symbol包增强的emacs接口来简化，这使得输出非常接近于通常的写作;它还允许来回进行约简，或者将约简保存在文件中，还允许导出乳胶代码。在这个方向上有一些工具和很好的实验;例如，在 [19] 中，Huet 展示了 如何使用 函数式编程语 言来帮助 理 解λ-calculusuchasteBéohm定理的非平凡属性F.L. C de Eschericha等人/理论计算机科学电子笔记269（2011）41534结论和今后的工作我们给出了SUBSEXPL系统的扩展，它是一个OCaml实现，用于比较、模拟和研究λ演算和显式子项演算[24]。源代码可以在SUBSEXPL网页上免费获得：http://www.cic.unb.br/www.example.com/subsexpl/index.html。我们展示了SUBSEXPL如何用于教育和研究目的，使用变量作为名称或deBruijn指数。在这个扩展中，用户可以很容易地定义新的显式替换演算，模拟约简和规范化，导出乳胶代码等。在Emacs buffer中呈现的符号是一种类似于Latex的符号，用户可以使用alias来表示复杂的λ项。这一功能对于教授λ-演算理论、λ-演算变体的基本性质以及λ-演算变体中以几种显式替换形式实现的迭代和递归等复杂计算操作尤为重要。在现代系统，显式替换演算的几个实规范和实现使用了一种新的混合方法，称为局部无名[ 4 ]，其中绑定变量由de Bruijn索引表示，自由变量由名称表示。这种方法有利于α等价项类的酉表示，而不需要自由变量的上下文。在其未来版本中，SUBSEXPL将允许使用局部无名方法定义演算引用[1] M. 阿巴迪湖Cardelli，P. L. Curien和J. - J. 我也是。 明确的替代。JournalofFunctionalProgramming，1（4）：375 - 4 1 6 ， 1 9 9 1 .[2] M. Ayala-Rinc'on，F.L.C. deMoura和F. 卡玛瑞丁 η-归约显式代换演算的比较与实现。纯逻辑与应用逻辑年鉴，134：5[3] M. Ayala-Rinc'on和C. 我的天显式替换和所有这些。RevistaColecuanadeComputacion，1（1）：47 - 7 1 ， 2 0 0 0 .[4] B. E. 艾德米尔，A. 恰格乌埃罗湾C. 皮尔斯河，巴西-地 Polla ck和S. 我们爱你。工程形式元理论。在乔治C。Necula和Philip Wadler，编辑，POPL，第3ACM，2008年。[5] F. Baader和T.尼普科重写和所有这一切。剑桥大学出版社，1998年。[6] D.盆地在Nuprl中验证组合逻辑。计算机科学讲义，408：333[7] R.布卢和K。H.玫瑰使用显式替换和垃圾收集在命名lambda演算中保持强规范化。荷兰计算机科学，1995年11月[8] R. 本根角Sinz和J. Walter. Redux1.5：重写的新方面。 在Ganzinger[17]，第412-415页。[9] R. 用NUPRL开发系统实现数学。普伦蒂斯-霍尔，1986年。[10] E. Conn tejean和C. 是的。CiME：CompletionM oduloE. 在Ganzinger[17]，第416-419页。 系统说明可在www.example.com上获得http://cime.lri.fr/。[11] Coq开发团队Coq Proof Assistant参考手册8.2版。INRIA- Rocquencourt，2008年。[12] R. 大卫和B。纪尧姆 具有显式弱化和显式替换的隐式演算Mathematical Structures in Computer Science，11（1）：16954F.L. C de Eschericha等人/理论计算机科学电子笔记269（2011）41[13] N.G.德布鲁因Lambda演算符号与无名的假人，一个自动公式操作的工具，与应用到教会-罗瑟定理。Indag. Mat. ，34（5）：381[14] F.L. C deEscherichia，M. A yala-Rinc'on和F. 卡玛瑞丁SUBSEXPL：一个模拟和比较显式替换演算的框架。Journal of Applied and Non-classical Logics，16（1- 2）：119[15] F.L. C deMoura，M. A yala-Rin co′n和F. 卡玛瑞丁高阶统一：Huet方法和基于显式替换的方法之间的结构关系。Journal of Applied Logic，6（1）：72[16] F.L. CdeEscherichia，F.Kamareddine和M. 我也是。通过显式替换的二阶拟合。In F. Baader和A.Voronkov，编辑，第11届国际逻辑会议编程人工智能和推理（LPARSpringer-Verlag，2005.[17] H. 甘青格，编辑。重写技术和应用，第七届国际会议，RTA-96，新不伦瑞克，新泽西州，美国，1996年7月27-30日，会议记录，计算机科学讲义第1103卷。Springer，1996年。[18] T. 哈丁和J. - J. 我也是。 一个连续的替换演算。 Fran ce-Ja panArti ficialIntelligen ceand ComputerScience Symposium，1989年12月。[19] G. 休特 对Bohm定理的分析 TCS，121：145-167，1993。[20] S. P·琼斯，编辑。Haskell 98语言和库-修订报告。剑桥大学出版社，2003年。[21] F. Kamareddine和R. P. Nederpelt。逐步显式替换。International Journal of Foundations of ComputerScience，4（3）：197[22] F. Kamareddine和R. P. Nederpelt。 一个有用的λ-符号。TCS，155：85-109，1996.[23] F. Kamareddine和A. 好的带显式替换的λ-演算 在Proc. 参见PLILP'95 ， LNCS 的第982 卷，第45-62页。Springer，1995年。[24] F. Kamareddine 和A. 好的关于显式代换的λ σ-型和λs -型JournalofLogic and Computation，10（3）：349 -380，2000.[25] N.川口T. Sakabe和Y.稻垣简洁：一个可视化的环境，用于支持术语重写系统的分析、验证和转换。在Martin Wirsing和Maurice Nivat，编辑，AMAST，计算机科学讲义第1101卷，第571Springer，1996年。[26] D.凯斯纳一个安全完整的显式替换理论。计算机科学中的逻辑方法，5（3：1）：1[27] R.琳 丝 一 类 范 畴 组 合 子 的 一 个 新 运 算 公 式 。 第 八 届 自 动 演 绎 会 议 （ CADE ） ， LNCS 第 230 卷 ， 第89Springer-Verlag，1986.[28] P.- A. 好的。在TLCA'95的程序中，带有显式替换的类型λ-演算不能终止.LNCS，902，1995.[29] A. Mendelzon，A. R'ıos和B. 齐利安尼 交换：命名和索引显式替换演算之间的天然桥梁。第五届高阶重写国际研讨会- HOR 2010，第41-46页[30] R. Milner，M. Tofte和R. Harper. 标准ML的定义麻省理工学院出版社，马萨诸塞州剑桥，1991年。[31] G. Nadathur λ项的细粒度表示法及其在内涵运算中的应用。 J.的Func。和Logic Programming，1999（2）：1 - 6 2 ， 1 9 9 9 .[32] R. P. Nederpelt，J. H. Geuvers和R. C.德·弗里耶关于自动化的论文选集。 北荷兰，1994年。[33] T.尼普科湖C. Paulson和M.温泽尔Isabelle/HOL - A Proof Assistant for Higher-Order Logic，LNCS第2283卷。Springer，2002年。[34] K. H.玫瑰明确的循环取代。在Michal Rusinowitch和Jean-Luc Remy，编辑，CTRS，计算机科学讲义第656卷，第36Springer，1992年。[35] X. 勒罗伊等al.Objective Caml系统-版本3.11。技术报告，INRIA，2008年。
我的内容管理
展开
