iRho：基于模式匹配和证明助手的计算机科学电子笔记

理论计算机科学电子笔记135（2006）85-94www.elsevier.com/locate/entcsiRho：软件【系统说明】Luigi Liquori1INRIA，法国摘要本文描述了iRho的解释器的第一个实现，这是重写演算的命令式版本，基于模式匹配，模式抽象和侧效应。该实现包含一个解析器和一个Natural Semantics中的按值调用计算器;所有内容都是使用编程语言Scheme编写的。 这个实现的核心（评估器）使用证明助手Coq进行认证。与实现的最小本质相比，性能是诚实的。本文档通过示例介绍了如何使用iRho。最终目标是使iRho成为一种所谓的敏捷编程语言，就像一些有用的脚本语言一样，比如，e. G. Python和Ruby，证明搜索不仅可行而且简单。关键词：iRho，Scheme，Coq，SW描述。1重写微积分基于重写的语言的主要优点之一，如Elan[16]，Maude[14]，ASF+SDF[19，2]，OBJ[10]，Objugo[18]是模式匹配。模式匹配允许在备选方案之间进行区分：一旦识别出模式，则将模式与动作相关联。 因此，相应的模式被重写在新模式的适当实例基于重写的语言的另一个优点（与ML或Haskell相比）是处理结果集合意义上的非确定性的能力：模式匹配不需要是排他性的，即。e.多个分支可以1由CNRS ACI Modulogic资助。1571-0661 © 2006 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.09.02386L. Liquori/Electronic Notes in Theoretical Computer Science 135（2006）85同时被“解雇”。结果的空集合表示应用失败，单例表示确定性结果，而具有多个元素的集合表示集合元素之间的非确定性选择。这个特性使得演算也非常接近逻辑语言;这意味着可以生成两个模式的乘积，从而“并行”应用乐观/悲观语义可以通过将成功结果定义为至少具有与错误值不同的分量（相对于所有分量）的产品来强加给演算通过重新定义适当的回溯策略，应该可以有用的应用在于模式识别和字符串/树操作领域。模式匹配已广泛用于 函 数 和 逻 辑 编 程 中 ， 如 ML[15 ， 7] ， Haskell[11] ， Scheme[17] 或Prolog[9];通常，它被认为是表达关于函数参数的复杂需求的方便机制重写演算（Rho）[4，5]以统一的方式集成，匹配，重写和函数;它的抽象机制基于重写规则的形成：在形式P→A的项中，人们抽象了模式P。注意重写演算是λ演算的推广 如果模式P是变量。如果抽象P→A被应用于 术语B，则评价机制是基于自由的约束P中存在的变量对应于B中应用于A的适当子项。事实上，这种结合是通过将P与B匹配来实现的。 匹配的优点之一G.结合-交换模型今年，在[13]中提出了一个增强（功能性）Rho的命令式扩展;不久，我们引入了命令式功能，如引用（i. e. e. expr）和赋值运算符（X：=expr）。相关的类型系统被丰富的dereferencing-types （i. e. pointer-types，int ref）和product-types（e. G. int→intnat→nat）。这个扩展的数学内容是验证的帮助下，半自动证明助理Coq。一个玩具软-WarePrototype，模拟了动态语义的数学行为，并在Scheme中实现。本文简要介绍了该软件的第一个LGPL版本;已经实现了一个解析器，并添加了更多的语法糖，使解释更容易使用。核心内核符合[13]的语义规范;未来的版本还将提供一个机器辅助的L. Liquori/Electronic Notes in Theoretical Computer Science 135（2006）8587是正确的。 我们也可以设想主内核例程的证明提取，在Caml或Haskell 2中的软件的“端口”的情况下。 本文介绍了iRho语言的语法和一些可以在解释器中通过剪切和粘贴直接运行的例子。当 前 的分布可以在www.example.com 上 找 到 http://www-sop.inria.fr/mirho/Luigi.Liquori/iRho/ 。 它 包含：两个 软件发布了iRho-1.0.scm和iRho-1.1.scm，这是Linux architecture3的预编译二进制版本，一个包含许多示例的文件demo.rho，以及一份[13]论文的副本（期刊版）。最后，我们用一个表格显示了当前软件的未来版本和演变，如（多态）类型推断，强大的匹配和统一算法，异常处理程序，策略，调用外部语言，对象等。2使用iRhoSW口译员iRhoSW向您问候如下：|----------\||| i R h o >||----------/|| 一个强制重写的微积分解释器|| 由Proof AssistantCoq认证的内核||技术支持Bigloo Scheme||版权Inria 2005||版本1.1alpha||无效应理论加载||$ =开关理论||# =清洁空间||@= ExitiRho|像往常一样，首先要学习的是如何退出read-eval-print循环：只需计算对首先在[5]中介绍：我们将在给出语法和约简语义的草图之后，对这个理论进行更精确的描述。 Evalu-atee.一个空间，常量，函数和术语重写系统可以是名称并全局重用。语法iRho的无类型（抽象）语法如下：key：：=“（“|“）”中的|“、”|“啊！”|“啊！“的|“：=”|“-->”|“--？“的|“什么？”“的|“;”|“=|“[]|“]”|“的|“关键词2Coq中的提取机制目前可以针对Caml或Haskell代码。3ELF32位 LSB可执行文件，Intel 80386，版本 1（SYSV），用于 GNU/Linux2.2.5，动态链接（使用共享库），剥离。88L. Liquori/Electronic Notes in Theoretical Computer Science 135（2006）85var：：=const：：=patt：：= var|康斯特帕特|const patt|帕特，帕特| ^pattPatternsexpr：：= const|var |patt-> expr |expr expr|expr，expr|！|!expr|expr ： =expr |expr<- ？ expr ？ ->expr|var=expr| [（var=expr|）]表达式重要的一点是，模式中的线性在语法中没有强制执行;我们在重写演算的这种形式化和实现中采用的解决方案受到我们的操作语义的实现语言的选择的影响，即Scheme和采用的匹配al-tax m [12]。 因此，iRho中匹配算法的规范接受非线性模式，并比较数据（通过，通过原始equiv实现？ 在Scheme中）。 concilience是由于操作语义的按值调用策略法律术语的例子有：iRho输入>12;;iRho输出>12iRho输入>伪;; iRho输出>伪iRho在>x;;iRho OUT > xiRhoIN > X;;iRhoOUT>（效应：未结合的变量X）iRho IN >12;;iRho OUT > 12iRho输入>（12->1312）;;iRho输出> 13iRhoIN >（12->1214）;;iRhoOUT >（Effect：PatternMismatch）iRhoIN >（（a->b，a->d）a）;;iRhoOUT >（b，d）iRho IN >（（a->b，c->d）a）;;iRhoOUT> biRhoIN >（fX Y）->X;;iRhoOUT>（Fun（（fX）Y）-> X）iRhoIN >（（fX X）->X（f 34））;;iRhoOUT>（Effect： Pattern Mismatch）iRho IN >$;;iRhoOUT> Switching_to_empty_theoryiRho IN >（（a->b，c->d）a）;;iRhoOUT >（b，（Effect： Pattern Mismatch））最后一个例子可以帮助我们理解，无卡理论吸收了模式匹配失败，而空理论则没有。这也许是引入归约语义的一个好点。归约语义语义表现如下（参见[13]的详细介绍）：(patt-> expr exprnf）=>sigma（expr）其中sigma=patt exprnf（（expr 1，expr 2）exprnf）=>（（expr 1 exprnf），（expr 2 exprnf））第一条规则是，如果参数是标准形式（按值调用语义）并且与模式匹配，则启动应用程序，而第二条规则是，L. Liquori/Electronic Notes in Theoretical Computer Science 135（2006）8589将应用程序分发到结构的所有元素。 如果你只想处理Rho的功能片段，这简而言之，函数片段“只是e.多个分支可以同时触发）。并行触发多个匹配分支的可能性是重写演算w.r.t.的最大特点之一。其他语言具有（排他的和顺序的）模式匹配。添加命令式特性导致引入存储，即。e. 从位置到正规形式的表达式的全局局部映射（即，e. 值），并添加以下缩减规则：^ exprnf/s=>loc/（s，loc=exprnf）其中loc不在Dom（s）中！loc/s=> s（loc）/swherelocinDom（s） loc：=exprnf /s=> exprnf/（s，loc=exprnf）wherelocinDom（s）第二次出口=>（（X-> expr 2）expr 1）/s，其中X在 expr 2简而言之：第一条规则在存储中分配一个新的位置loc，并将其绑定到值exprnf;第二条规则读取位置loc的内容;第三条规则在位置loc中写入值exprnf。的last rule（sequence）只是一个伪函数应用程序的宏;按值调用策略确保了expr 1将在expr 2之前被求值（可能带有存储修改）。法律术语的例子有：iRhoIN > ^1，2;;iRhoOUT >（（Ref（1），2）iRhoIN >（1，2）;; iRhoOUT >（Ref（1，2））iRhoIN >（！^ (X->X）4）;;iRho OUT > 4iRhoIN>（（X，Y）->（X，Y）（^3，^4））;;iRhoOUT >（（Ref 3），（Ref 4））iRho IN>（（X，Y）->（Y：=！X;（！X！Y））（^3，^4））;; iRhoOUT >（3，3）iRho IN >（（X，Y）->（Y：=！X;（X，！X，Y，！Y））（^3，^4））;; iRho OUT>（（Ref3），（3，（（Ref 3），3））iRhoIN >（（fX Y）->（Z->（X：=！Z）X）（f^3^4））;;iRho OUT > 3iRhoIN >（X->（（^ Y->Y）X）^4）;;iRho OUT > 4iRhoIN >（（XREF->（（X->XREF：=X）5））^dummy）;iRho OUT > 5宏这个简单的宏允许修改一个全局命名空间;它也可以快速定义常量值，函数和带有内置定点的术语重写系统。iRho IN > ID =（X->X）;;iRhoOUT>（FunX-> X）iRho IN > IDID =（X->X X->X）;; iRhoOUT>（Fun X ->X）iRhoIN >ID;iRhoOUT>（Fun X-> X）iRho IN >（ID4）;;iRho OUT > 4iRhoIN > IDID;;iRhoOUT>（Fun X-> X）90L. Liquori/Electronic Notes in Theoretical Computer Science 135（2006）85iRhoint n>（n）;iRho OUT > 4iRhoIN > MATCHPAIR =（（f（X，Y））->X）;（MATCHPAIR（f（2，3）;;iRho OUT > 2iRho IN > MATCHCURRY =（fX Y）->X;（MATCHCURRY（f23））;;iRhoIN> SWAP=（（X，Y）->（（AUX->（AUX：=！X;X：=！Y;Y：=！AUX;（！X！Y，！AUX））（^0））;;iRho OUT>（Fun（X，Y）->（（Fun AUX->((Fun FRESH1005->.（（Bang X），（（Bang Y），（Bang AUX）(AssY（Bang AUX）（屁股X（Bang Y）（AssAUX（BangX）（Ref 0）交换两个变量iRhoint n>（n）;;iRhoOUT>（5，（4，4））iRho IN > FIXV = FUN->VAL->（FUN（FIXV FUN）VAL）;; iRho OUT >（FUN ->（Fun VAL->（（FUN (FIXVFUN））VAL）按值调用固定点iRhoint n>（intn）;;分割错误对不起，重新加载所有内容.iRhoIN > LETRECPLUS =（（PLUS->(PLUS（（succ（succ 0）），（succ（succ 0）（FIXV（PLUS-> VAL->(((0，N）->N，（（succ M），N）->（succ（PLUS（M，N）VAL）;;letrec PLUS =If-then-else控制结构可以很容易地定义如下：iRhointn =（true->false，false->true）;;iRhoOUT >（（Funtrue->false），（Funfalse->true）） iRho IN>（NEGtrue）;;iRho OUT >falseiRhoIN > AND =（（true，true）-> true，(true，false）-> false，（false，true）->false，（false，false）-> false）;iRhoOUT>（（Fun（true，true）->true），（（Fun（true，false）-> false），((Fun（false， true）-> false），(Fun（假，假）->假） iRhoIN > OR =（（真，真）->真，(true，false）-> true，（false，true）-> true，（false，false）->false）;;iRhoOUT>（（Fun（true，true）->true），（（Fun（true，false）-> true），((Fun（false， true）-> true），(Fun（false，false）->false）iRho IN >OMG=（X->（XX））;;iRho OUT>（Fun X->（X X））iRhoIN >（（OMG OMG）-？ (AND（true，true））？-> 4）;;Happy syntaxiRho OUT> 4定义术语重写系统L. Liquori/Electronic Notes in Theoretical Computer Science 135（2006）8591人们可能想知道一种更简单的方法来定义一个项重写系统和一个允许使用项重写系统的定点运算符;iRhoSW运算符提供了两种更简单有效的方法。第一种是使用宏92L. Liquori/Electronic Notes in Theoretical Computer Science 135（2006）85“=”这两种选择的主要区别在于效率（前者比后者快）。我们首先介绍Peano数的一些宏iRhoreturn 0;;return（0）;;TWO=（succONE）;;THREE=（succTWO）;;...然后我们简单地定义我们的PLUS项重写系统如下：iRhoIN> PLUS =（（0，N）-> N，（（succ N），M）->（succ（PLUS（N，M）;;iRhoOUT>（（Fun（0，N）->N），(Fun（（succ N），M）->（succ（PLUS（N，M） iRho IN>（PLUS（THREE，THREE））;iRhoOUT>（succ（succ（succ（succ（succ（succ0））或如下：iRhoIN > [PLUS =（（0，N）-> N，（（succN），M）->（succ（PLUS（N，M）];;iRhoOUT>术语重写系统定义iRhoIN >[PLUS=（（0，N）-> N，（（succ N），M）->（succ（PLUS（N，M）];（PLUS（THREE，THREE））;;iRhoOUT>（succ（succ（succ（succ（succ（succ0））请注意，在这两种编码中（使用“=”或“[...]”）一个术语重写系统可以iRhoIN> PLUS =（（0，N）-> N，（（succ N），M）->（succ（PLUS（N，M）; FIB=（0->（succ 0），(succ0）->（succ 0），(succ（succ X））->（PLUS（（FIB（succ X）），(FIB（X）;(FIBFOUR）;;First encodingiRhoIN > [PLUS =（（0，N）-> N，（（succ N），M）->（succ（PLUS（N，M）|FIB =（0->（succ 0），(succ0）->（succ 0），(succ（succ X））->（PLUS（（FIB（succ X）），(FIB（X）];(FIB四）;;第二编码iRho OUT>（succ（succ（succ（succ（succ0）iRhoIN > [PLUS=（（0，N）-> N，（（succ N），M）->（succ（PLUS（N，M）|MULT=（（0，M）->0，（（succ N），M）->（PLUS（M，（MULT（N，M）|POW =（（N，0）->（succ 0），（N，（succM））->（MULT（N，（POW（N，M）];;(POW（TWO，TEN））;;PoweriRhoIN > [ACK 为((0，N）->（succ N），（（succ M），0）->（ACK（M，（succ0），（（succ M），（succ N））->（ACK（M，（ACK（（succ M），N）];（ACK（THREE，FOUR））;;AckermanniRhoIN > LIST =（10，11，12，13，15，16，nil）;;iRho在> [FINDN =（（0，nil）->fail，（（succ N），nil）->fail，（（succ 0），（X，Y））-> X，L. Liquori/Electronic Notes in Theoretical Computer Science 135（2006）8593（（succ N），（X，Y））->（FINDN（N，Y）];（FINDN （THREE，LIST））;;在列表中查找元素iRho In> [KILLM =（（m，（n，nil））->（n，nil），（m，（m，X））-> X，（m，（n，X））->（n，（KILLM（m，X）];（KILLM（13，LIST））;;杀死列表一个更棘手的例子：否定范式此函数用于实现决策过程，几乎存在于所有模型检查器中。经处理的输入是具有生成语法的公式的无隐含语言：φ：：= p|和（φ，φ）|或（φ，φ）|not（φ）我们提出了三种编码，第一种使用“=”宏，第二种使用“[...]”最后一个只是第二个的宏扩展（省略了一些输出）。iRho IN > PHI =（and（（not（and（p，q），（not（and（p，q）;; iRho IN > NNF =（ p ->p，q ->q，(not（not X））->（NNF X），(not（或（X，Y）->（and（（not（NNF X）），（not（NNF Y），(not（和（X，Y））->（或((not（NNFX）），（not（NNF Y），(and（X，Y））->（和（（NNF X），（NNFY），(or（X，Y））->（或（（NNF X），（NNFY）;(NNFPHI）;;First encodingiRho2016 - 05 - 25 01：01：01p ->p，q ->q，(not（not X））->（NNF X），(not（或（X，Y）->（and（（not（NNF X）），（not（NNF Y），(not（和（X，Y））->（或((not（NNFX）），（not（NNF Y），(and（X，Y））->（和（（NNF X），（NNFY），(or（X，Y））->（或（（NNF X），（NNFY）];(NNFPHI）;;第二编码iRho OUT >（and（（or（（not p），（not q），（or（（not p），（not q）认证：DIMPRO模式在[13]中，我们尝试了一种有趣的design-IM plement-PROve，设计安全的软件，完全尊重其数学和功能规范。iRhoSW是这种方法的直接衍生物。直观地说，我们从一个干净优雅的数学设计开始，从这个设计开始，我们继续实现一个满足设计的原型（使用函数语言），最后我们通过寻找相关软件实现的最简单的这三个阶段是严格耦合的，而且经常是，一个阶段中的一个特定选择会94L. Liquori/Electronic Notes in Theoretical Computer Science 135（2006）85过程精化是通过迭代循环来完成的，直到达到所需的所有全局属性（该过程让人想起固定点计算或B-精化[1]）。这三个阶段都具有相同的状态，并且可以相互影响。我们的配方可能建议一个新的模式，或这可以成为今后工作的主题。一个小的软件解释器为我们的核心演算肯定是一个很好的测试“方法论”。更一般地说，这种方法可以应用于将软件质量提高到通用标准CC[6]的最高级别（从EAL 5到EAL 7）或能力成熟度模型CMM的第五级。我们在我们的日程安排我们的小说DIMPRO，在民间传说中的议程我们的iRhoSW非常年轻：下表列出了未来两个版本中计划的主要改进/版本2.03.0模式匹配失败C一阶类型推理C更多的控制结构和策略C简单对象和基于对象的继承C类型推理 拉达马米尔纳C统一与交流匹配理论C重写规则作为模式[3]C调用外部Scheme/Java/CCI/O（文件）C使用CoqC？？引用[1] J. R.阿布里尔B书：将程序转化为意义。[2] Asf+Sdf团队。 Asf+Sdf元环境主页，2005年。[3] G.巴特，H。奇尔斯泰阿角Kirchner和L.利口酒纯模式类型系统。在POPL。2003年。[4] H.奇尔斯泰阿角Kirchner和L. 利口酒 罗方块 在FOSSACS的Proc. ofFOSSACS，LNCS的第2030卷，第166-180页[5] H.西斯泰亚湖Liquori和B.变态 Rho演算与不动点：一阶系统。 在类型的过程。Springer-Verlag，2004.[6] 通用标准联盟。2005年，共同标准主页L. Liquori/Electronic Notes in Theoretical Computer Science 135（2006）8595[7] 水晶队 OCaml主页，2005年。[8] E.伽马河赫尔姆河约翰逊和J. Vlissides（四人帮）。可重用面向对象软件的设计模式元素。Addison-Wesley，1994年。[9] GNU Prolog团队。Prolog主页，2005年。[10] 杰·戈根2005年，家庭主页[11] Haskell团队 Haskell主页，2005年。[12] G. 嘿。 Resolutiond' e q u a t i o n s d a n s l a n gag e s d ' o r d r e 1，2，.，ω。 Ph. D. 《巴黎第七大学》，1976年。[13] 利科里湖Serpette，B. iRho，一个势在必行的重写微积分。 《人民民主党学报》，第167-178页。ACM Press，2004.[14] 莫德团队。首页> 2005年[15] R. Milner，M.托夫特河Harper和D.麦奎恩标准ML的定义（修订版）。MIT Press，1997.[16] Protheo团队2005年，Elan主页[17] 策划小组。 语言，2005年。[18] 阿汤哥队。2005年，《中国日报》[19] A. van Deursen，J.Heering和P.克林特语言原型，1996年。