有限Eilenberg机的反应引擎模拟算法及其形式正确性证明与实例应用分析

理论计算机科学电子笔记229（5）（2011）119-134www.elsevier.com/locate/entcs用反应机模拟有限Eilenberg机Beno Razet1技术和计算机科学学院，塔塔基础研究所，Homi Bhabha路，孟买400 005，印度摘要艾伦伯格机于1974年在形式语言理论领域被引入。它们是有限自动机，其字母表由抽象集合上的数学关系解释。它们概括了许多有限状态机。我们认为，在目前的工作中，我们提供了一个可执行的完整的模拟器有限艾伦伯格机器的子类。此程序使用Coq证明助手指定。 该算法的正确性也得到了形式上的证明，并使用鸡使用其提取机制，Coq证明助手允许将规范转换为可执行的OCaml程序。算法和具体化的灵感来自G'erardHuet的反应引擎有限艾伦伯格机模型包括确定性和非确定性自动机（DFA和NFA），但也实时传感器。作为一个例子，我们提出了一个下推自动机（PDA）识别歧义λ-项被证明是一个有限的Eilenberg机。然后，模拟下推自动机的反应引擎为这种特定的上下文无关语言提供了一个完整的识别器。保留字：自动机，艾伦伯格机，Coq1引言Samuel Eilenberg在他的书《Automata，Languages and Machines》[ 4 ]的第10章中介绍了 在这种形式主义中，一台机器被定义为一个自动机，在一个集合上标记有二元关系。X.集合X抽象了语言理论中常见的数据结构，如磁带，计数器，堆栈等，用于单词自动机，下推自动机，转换器等。此外，二元关系给出了一个内在的非决定论概念。通常的计算模型的许多翻译[4]，如自动机，传感器，实时传感器，双向自动机，下推自动机和图灵机可以表示为艾伦伯格机。1电子邮件：benoit. gmail.com1571-0661 © 2011 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2011.02.019120B. Razet/Electronic Notes in Theoretical Computer Science 229（5）（2011）119这个模型的通用性是有趣的指定问题，使用许多不同类型的机器。不幸的是，这种形式主义的表达能力和它在集合论中的表现，使它从有效的角度来看是不现实的。由于这些原因，我们在最近的一篇论文[8]中引入了称为有限艾伦伯格机 我们已经提供了一个模拟算法，在精神的re主动引擎的G'erardHuet[5]。它是用OCaml[7]编写的，我们已经给出了它的正确性的非正式证明正确性的证明使用了一个基于三个相互递归谓词的多集排序[3]的归纳原则。由于终止参数的微妙性，我们发现有必要在证明中将模拟形式化。使用Coq证明助手[2]及其扩展[10]，我们提供了有限Eilenberg机的一个规范，以及其终止性和正确性的机械化证明本文的其余部分组织如下。第2节给出了有限Eilenberg机的具体说明。第3节介绍了第4节中提供的反应式发动机定义所需的终止证明技术。第5节给出了反应式引擎的正确性证明。第六节讨论了Coq的提取机理，并给出了相应的程序。第7节提供了一个下推自动机的例子，它将λ-演算的单词识别为有限的艾伦伯格机，并讨论了反应引擎的效率，它提供了关于下推自动机的所有解决方案2有限Eilenberg机我们记得unit是包含唯一值tt的单例数据类型。在我们的规范中，流是按需枚举的有限定义对象（懒惰列表）。感应流（数据：设置）：设置：=|EOS：流数据|流：数据→（单位→流数据）→流数据。定义延迟（数据：设置）：设置：=单元→流数据。流值是用于编码空枚举的空流EOS（d，以及作为枚举的其余部分的延迟计算的值del。由于这种指定将被转换为ML，并且因为ML在λ-演算的限制下计算弱约简，因此延迟数据类型的值（如del）的计算被延迟，因为它是一个函数值。这种众所周知的技术允许按需计算。请注意，这种技术不适用于在函数体内求值的编程语言（λ-演算术语中的强简化）。注：流值必然是有限的，因为它是一个归纳定义。CoInductive构造提供了允许Coq中潜在无穷值的更一般的B. Razet/Electronic Notes in Theoretical Computer Science 229（5）（2011）119121→→→|∀→→|∀数学关系是指定可能的非确定性计算的对象。我们将我们的研究限制在一个域数据上的二元关系，该域数据被定义为从数据到数据流的Coq函数：定义关系（数据：设置）：设置：=数据→流数据。打破关系对称性的选择是由集合X的值对的子集与从X到X的子集的函数之间的同构所证明的。一个流值可以编码一个有限集合，因此类型关系的关系是局部有限关系，即：对于所有数据d，与d相关的元素集合是有限的。让我们为流引入一个类似于谓词In的成员关系谓词在库列表中：Inductiv eIn_stre am（data：Set）：datastreamdataProp：=InStr1：（d：data）（del：delay data），In_strea m_d（Streamdataddel）InStr2：（d：data）（d'：data）（del：delay data），InStr2：（d：dat）（dIn_strea m_d（Streamdatad其中In_delay（data：Set）：data→Proydata→Prop：=| InDel：numb（d：data）（del：延迟数据），In_stream _d（del tt）→In_delay _d del.它是流和延迟类型上的归纳相互递归谓词我们定义我们的Eilenberg机器的子类，首先使用指定为关系类型的关系，然后作为包含五个参数的模块。让我们把这样的模块称为机器：模块式机器。参数数据：设置。参数状态：设置。参数转换：状态列表（（关系数据）* 州）。参数首字母缩写：列表状态。参数terminal：statebool.结束机器。库List和Bool提供数据结构类型list和bool。参数数据对应于在Eilenberg的原始工作中称为X的抽象集其他参数状态、跃迁、初始和终止编码传统上写为（Q，δ，I，T）的自动子结构。机器是一种自动机，它用关系而不是传统的字母表来标记。在其余部分中，我们将使用以下符号：d d现在我们假设给定一个Machine类型的机器M，声明一个函子，作为论据。模块发动机（百万美元）：机器）。进口M.下面的单元格类型是机器的定义细胞：设置：=（data*州）。122B. Razet/Electronic Notes in Theoretical Computer Science 229（5）（2011）119|⇒|⇒|⇒|⇒→ →→|∀|∀→定义解决方案（d d'：data）：Prop：=序列：序列，路径顺序D=FST（hd_seqseq）D' =FST（tl_seqseq）下面的边属性指定了机器M中的正确归约步骤：定义边缘DSreld' s ' ： P r o p ： =In（rel，s'）（transition n s）I n _ s t re a m datat a d'（re l d）.直观地说，它是两个单元格（d，s）和（d '，s'）之间的关系，它们rel;（rel， 一个有限的归约步骤序列以列表的方式编码感应序列：设置：=|Seq1：数据→状态→序列|Seq2：数据→状态→（关系数据）→序列→顺序约简序列不允许为空，它至少包含一个单元格。这个序列的定义并没有指定约简是正确的边，这是使用下面定义的路径谓词来指定的。为此，函数hd_seq和tl_seq分别给出序列seq的头部单元和尾部单元：定义hd_seq（以下顺序）：sequence）：cell：=匹配seqwithSeq1 d s（d，s）Seq2 ds__（d，s）端不动点tl_seq（以下顺序）：sequence）{structseq}：cell：=匹配seqwithSeq1% d % s（% d，% s）Seq2 _seq ' tl_seq随后端一个正确的序列然后被定义为以下归纳谓词：感应路径：sequenceProp：= Path1： ds，path（Seq1 ds）Path2：ds reld' s' seq，路径seq（d '，s'）=hd_seq seqedge ds rel d's'path（Seq2dsrelseq）。以下两个函数init和term确保单元c的状态相对于机器M的初始和终端参数是初始和终端。定义init（c：cell）：Prop：= In（snd c）initial。定义term（c：cell）：Prop：=终端（瑞典）c）= true。最后，我们将数据d具体如下：init（hd_seqseq）term（tl_seq seq）。数据d我们记得有限艾伦贝格机模型[8]包含关于艾伦贝格机的两(i) 上述关系操作的具体说明是从数据到有限数据流的函数。（第一个条件）B. Razet/Electronic Notes in Theoretical Computer Science 229（5）（2011）119123∃(ii) “计算”必然是有限的。（第二个条件）对于第二个条件，我们引入了一个关于细胞的关系，我们假设它是一个有根据的关系：定义Rcell（c' c：cell）：Prop：=rel：关系数据，边缘（fst c）（snd c）rel（fst c'）（snd c '）。假设WfRcell：∀c：单元，ACC雷塞尔角在第3节中，我们将清楚为什么这个假设对应于无限路径的不存在。在这一点上，我们已经拥有了所有我们需要阐明的定理，我们的目的是证明：定理 goal：目标：关系数据（relation data），（dd'：dat a），S o l u t i o n d ' ← → I n _ s t re a m dat a d '（f d）.它说，存在一个函数关系f，它正确地模拟了机器M关于解的指定。 在剩余部分中，我们将提供这样一个f，它是G′erardHuet的反应引擎的推广，并提供该函数的定理。即使我们的函数f本质上是一个反应过程，我们也会证明f对于任何数据d都是终止的，这允许我们使用Coq的不动点构造来定义它 我们将说f是M的特征关系，因此称之为特征关系。3反应引擎的终止论证的构造在本节中，我们给出了终止证明技术，用于证明模拟任何有限艾伦伯格机的过程的终止性。这些技术依赖于使用良好的基础关系。Coq为此提供了一个名为Wf的库。让我们回顾一下图书馆的基本概念。首先，A型元素上的二元关系是谓词R：A→A→Prop。一个良基关系是一个关系，对于这个关系，由R左相关的元素的链必然是有限的。这由以下可访问性谓词Acc形式化：感应ACC（右）：一个→一→道具）（x：A）：Prop：=| Acc_intro:(∀y:A,Ryx→AccRy)→AccRx.直觉上，如果Acc R x成立，那么不可能有无限序列xi（i∈N）使得R xi+1xi对任何索引i成立。一个关系R是良基的，如果每个元素都是可达的：定义有根据的（右）：一→一→道具）：=∀a：A，ACCR a.我们还考虑了良基归纳原理well_founded_ind：定理well-founded_ind：n（R：A→A→Prop），well-founded R→CUP：一个→道具，（X：A，（Y：A，Ryx→Py）→Px）→Xa：A，Pa.进一步的解释在YvesBertot和PierreCas t′s[1]的书中提供。现在我们将定义一个包含集合D和良基关系R的模类型，并称这个模类型为WFMOT：124B. Razet/Electronic Notes in Theoretical Computer Science 229（5）（2011）119∀→→模块类型 WFMONOW。参数多：准备。参数R：DDProp. 假设WFD：d：D，Acc R d。结束WFMOTORIO。列表上传统的良基关系是它们的长度排序让我们在列表上定义一个新的良基关系，称为BiListExtension：模块BiListExtension（N个：WFMMONOW）。进口 N.感应回复：列表D→列表D→道具：=|Reext 1：Reext（d：D）（l：list D），Reextl（d：：l）|Rext2：0（d1 d2：D）（1：列表D），R d1 d2-Rext（dl：：l）（d2：：l）|Rext3：d2（d1 d2 d3：D）（1：列表D），R d1 d3→ R d2 d3- Rext（dl：：（d2：：l））（d3：：l）。关系Rext是多集序扩展的一个简单情况[3]，原因如下：(i) 一个元素的替换只在列表的头部元素上执行，而不是在任何位置。(ii) 它用最多两个严格小于关系R的元素替换一个元素。多集序允许一个元素被严格更少的其他元素的有限多集我们证明Rext是有根据的：定理WfRext：（l：listD），Acc雷克特 湖证明是通过列表l上的结构归纳法，利用D是有根据的这一事实.端B i L i s t E x t e n s i o n .让我们介绍机器M的转换列表的缩写：定义选择：设置：=列表（（关系数据）* 状态）。我们定义了反应引擎使用的以下两个数据库：感应回溯：设置：=|提前：数据→状态→回溯|选择：数据→状态→选择→（关系数据）→（延迟数据）→状态→回溯。定义恢复：设置：=列表回溯。有限Eilenberg机可能是不确定的，因此需要一个回溯机制，他们的模拟。由于机器的不确定性，backtrack类型的值允许保存多个选择反应式引擎将在恢复类型的恢复中堆叠这样的回溯值。 值Advance ds表示位于单元格（d，s）上。值Backtrack dschreldels'意味着在单元（ d，s）上， 查看（transition s）的transition（rel，s'），del是（rel d）的延迟，并且ch个transitions包括在transition s中。这由以下WellFormedBack谓词指定，它是构造的任何回溯值的不变量B. Razet/Electronic Notes in Theoretical Computer Science 229（5）（2011）119125→→∀→→|∀|∀→|⇒|⇒|⇒|⇒感应WellFormedBack：backtrackProp：= WFB1： ds，WellFormedBack（Advance ds）WFB2：d s ch rel delIn（rel，（ d1，In_strea mdatad1（deltt）In_strea mdatad1（reld））incl ch（transition s）WellFormedBack（选择DSchreldel s ' ） 。格式良好的选项是格式良好的回溯值的列表定义WellFormedRes（res：恢复）：Prop：=∀b：回溯，在Bres→WellFormedBack湾在Coq中，我们需要证明递归函数的终止性。现在让我们构建我们的终止论证。首先，我们引入一个测度chi，它是由一个单元和两个自然数组成的三元组感应迟：设置：=|气：细胞→nat→nat→气。这两个自然数分别是选择列表的长度和流的长度。第一个已经在List库中可用，函数length和第二个函数length_del在这里定义如下：不动点长度字符串（str：流data）{structstr}：nat：=匹配串与EOS OStream _ del S（length_str（deltt））端定义length_del（del：delay data）：nat：= length_str（del tt）.chi度量与回溯值关联如下：定义赤背（背面：回溯）：chi：=匹配回来高级d s池（d，个）（二）+（长度（过渡s））O选择d s ch雷尔-德尔斯（d，个）（长度ch）（S（length_del del））端我们将考虑证明终止的最终测量值是chi测量的列表。这些值使用模块List的map函数与任何恢复相关联：查询chi_res（res：res umpti on）：列表chi：=mapchi_ backres 。现在，我们将在chi列表上引入一个有良好基础的关系，并使用它来终止反应引擎。Pred关系只是自然数上的前置关系，它是有根据的：定义Pred（n'n：nat）：道具：=n=是的。引理WfPred：n：nat，Acc Pred n.设RChi是Chi上的一个关系，它是一个特定的字典序。感应RChi：迟→迟→道具：=|RC1：C'n1'n2'Cn1n2，Rcell c|RC2：Cn1'n2'n1n2，Pred n1'n1→RChi（Chi c n1|RC 3：RCn1 n2126B. Razet/Electronic Notes in Theoretical Computer Science 229（5）（2011）119⇒|⇒|⇒|⇒|⇒|⇒|⇒|⇒|⇒|⇒|⇒Pred n2'n2→RChi（Chi c n1 n2'）（Chicn1n2）.RChi的关系也是有根据的。引理WfRChi：Chiv：chi，AccRChi诉现在我们在MyUtil模块中将RChi扩展为BiListExtension：Module ModuleWfChiRes. 定义D：= chi。 定义R：= RChi。定义WFD：= WfRChi。End ModuleWfChiRes.模块MyUtil：=BiListExtension（ModuleWfChiRes）.进口M y U t i l 。因此，我们得到相应的实例良好的基础Rext关系的列表chi。4反应式引擎我们现在将介绍所谓的反应引擎，它模拟有限的艾伦伯格机M，这是一个先验的非确定性机器;一个数据d可能有许多关于解谓词的解d反应式引擎的核心部分被定义为三个相互递归的函数，反应，选择和继续扩展[10]。程序固定点反应（d：data）（s：state）（res：recovery）（h1：WellFormedRes res）（h）：接入Rext（（Chi（d，s）（S（length（transition s）））O）：：（chi_resres）））{structh}：（stream数据）：=如果端子s然后流数据d（fun x：单位选择DS（过渡个）resH1（__）其他选择DS（过渡（s）resH1- -withchoose（d：data）（s：state）（ch：choice）（res：re sum ption）（h1：Well Form edResre s）（h2：inclch（transitions））（h）Rext（（Chi（d，s）（长度ch）O）：：（chi_res res）））{structh}：（stream数据）：=匹配 同[]continue res h1 _（rel，匹配 （相关）D.与EOS choose d s rest res h1 _ _ Streamd反应dD s休息reldel结束结束continue（res：resume）（h1：WellFormedRes res）（h）Rext（chi_resres））{structh}：（stream数据）：=比赛保留地使用[]EOS数据返回：：res匹配回来前进dsreact dsres匹配 （deltt）与EOS choose dsrest res反应dD的休息reldel 's '）：：res '）__B. Razet/Electronic Notes in Theoretical Computer Science 229（5）（2011）119127|⇒|⇒|⇒|⇒⇒|... 我...|⇒|⇒结束结束端首先在这个定义中省略参数h1、h2和h。函数react检查状态是否是终端，然后提供流的一个元素，延迟调用函数choose的其余探索。这个函数choose在转换上执行非确定性搜索，按照列表数据结构的自然顺序选择它们函数continue管理回溯机制和关系的有限流的枚举;它总是选择回溯恢复中的最后一个推送值。注意，这三个相互递归的函数不使用任何副作用，并且以纯函数风格编写，完全尾递归，使用恢复作为延续机制。这三个函数确保如果参数作为谓词h1中的前置条件是格式良好的，则计算出的参数作为后置条件是格式良好的。谓词h2确保了函数choose中转换列表的部分格式良好性。使用谓词h中chi列表上的可访问性谓词来确保终止;属性WfRext用于确保所有递归调用都使用结构较少的h参数执行。使用Coq [10]的扩展，我们得到了一个可读的程序定义。这是由于两个特点，首先，它允许给出函数定义，而不提供作为证明义务而延迟的所有逻辑证明。函数体中的每个下划线字符根据函数声明创建一个证明义务。其次，在相关模式匹配方面，SVM带来了以下增强：匹配 v返回没和v1 t1......vn tn端匹配v作为X返回v = x→T与被替换为|v1游戏（乐趣EQ（1）vn（funeqtn）端（refl_equal v）与研究报告[9]中提出的无反作用发动机相比，人们应该欣赏反作用发动机定义中的反作用发动机带来的改进。PRO-10生成的证明义务与研究报告中反应式引擎定义中明确提供的谓词相同;它们是由于程序不变量对应于h1 h2和终止参数对应于h而产生的属性。设d是一个数据，机器可以用它的任何初始状态初始化。我们把这种非决定论编码为一种只包含高级参数的恢复这是由下面的init_res函数执行的定点（d：数 据）（l：列表状 态 ）（acc：数据）{structl}：恢复：=匹配l与[]访问（s：：rest）init_resD休息（（提前D个）* 行政协调会）端参数acc是结果恢复的累加器功能128B. Razet/Electronic Notes in Theoretical Computer Science 229（5）（2011）119⇒∃ ∃ ∃init_res用一个空的累加器初始化，参数l等于initial（机器的初始状态列表）。由init_res计算的恢复很容易被证明是良构的：Lemmalemma_init：nodl，We llFor medRes（init_resdl[]）.最后，我们定义期望类型关系数据的函数characteristic_relation，它应该具有以下功能：给定数据d，流characteristic_relation d包含所有数据d定义特征关系：关系数据：=fun（d：data）continue（init_resD初始[]）（lemma_initD姓名首字母）（WfRext（chi_res（init_resDinitial []））。函数characteristic_relation是定理目标的函数f我们正在寻找的。备注4.1（发动机与机器）我们区分术语“发动机”和“机器”。机器可以是非确定性的，而引擎是能够模拟非确定性的确定性过程。有限艾伦伯格机描述了由确定性过程（反应式引擎）枚举的非确定性计算5反应式引擎的正确性：可靠性和完整性我们要证明函数特征关系的可靠性和完备性。为此，我们需要证明三个相互递归的函数react、choose和continue的可靠性和完备性。以下谓词指定这些函数的不变量：定义PartSol（d）：data）（s）：state）（d'：data）：P rop：=序列：序列，路径顺序（d，s）=hd_seqseqD' =FST（tl_seqseq）term（tl_seqseq）。当且仅当单元格（d，s）以具有数据d'的终端单元格开始路径时，属性PartSold s d我们在回溯和恢复值上扩展这个谓词感应零件背面：回溯→数据→道具：=|SB1：“d sPartSold s d'→零件解决方案返回（预付款）d s）d|SB2：我的天s1 d '，PartSolds d '→PartSolBack（Choosedschadels1）d'.ParrtSol Res（res：resumption）（d∃b：回溯，Inb respartSolBackBd '。下面的谓词丰富了PartSol的选择transi- tions的规范。定义PartSol_选择（d）data）（ch：选择）（d'：data）：Prop：=rel，s1，d1，In（rel，s1）ch（In_strea mdatad1（reld））PartSolD1S1d '。我们将其扩展到回溯和恢复值：B. Razet/Electronic Notes in Theoretical Computer Science 229（5）（2011）119129→|∀→→|∀→→→→∀PartSolD1S1d' ）→In_strea mdatadIn_strea mdatadPartSolDs dPartSolResresd感应零件背面2：backtrackdataProp：=SB3：d sPartSold s dPartSol_选择D杰达零件SolBack2（选择D S CHreldel s1）d|SB5：D S CHreldels1 d1（In_delaydatad1delPartSolBack2（Choose d s ch rel del s1）d定义PartSolRes2（res：（续）（d'：data）：Prop：=∃b：回溯，Inb resPartSolBack 2Bd '。三个函数react、choose和continue的可靠性引理如下：Lemmasoundness_lemma：（v：listchi），（（dsresh1hdv =（Chi（d，s）（S（长度（过渡s）0：：奇雷斯res）→（dschresh1h 2hdv =（Chi（d，s）（长度ch）0：：奇雷斯res）→PartSolds d' PartSolResres d '）（Partire s h 1 h d '，v=奇雷斯雷斯In_ste a mdatad'（cntinueresh1h）PartSolResresd'））.证明是一个案例分析的同时良基归纳的v.使用这个可靠性引理，我们证明了反应引擎的可靠性定理：对于所有数据d和d定理可靠性：（d d'：data），In_stre amdatad'（c h a r ac t e r i s t i c _ r e l a t i n d）→解决方案d '。以同样的方式，我们给出了完整性引理，它比可靠性引理的逆更强，因为它使用了PartSolRes 2和ParSol_choice而不是PartSolRes和PartSol。Lemmacompleteness_lemma：（v：listchi），（（dsresh1hdv =（Chi（d，s）（S（长度（过渡s）0：：chi_resres）→PartSolDs dPartSolRes2resd '→In_strea mdatad'（reac t d s re s h 1 h））（dschresh1h 2hdv =（Chi（d，s）（长度ch）0：：奇雷斯res）→PartSol_选择D杰达PartSolRes2resd '→In_strea mdatad'（choos e d s c h r e s h 1 h 2 h））（res h1）hPartSolRes2雷斯德In_ste a mdatad'（ c n t i nu e re s h 1 h ）.证明再次是一个案例分析，同时良好的理由归纳措施v。使用完备性引理，我们证明了反应引擎的完备性对于所有数据d和d定理完整性：（d d解决方案d' → I n _ s t re a m dat a d '（c h a r a c t e r i s t i c _ r e l at i n d）。→130B. Razet/Electronic Notes in Theoretical Computer Science 229（5）（2011）119→→→|→|→|→|→反应式引擎的正确性结合了可靠性和完整性：反应式引擎精确地枚举了所有解决方案：定理correctness：numb（d d'：data），解决方案d' ← → I n _ s t r e a m dat a d '（c h a r ac t e r i s t i c _ r e la t i o n d）。端发动机6节目提取上面的形式化开发使用了归纳构造演算作为规范语言，这是一种高阶逻辑，适用于抽象数学开发，也适用于关于计算对象的构造性推理这里，当排序Set用于计算对象时，逻辑属性需要排序Prop这允许程序提取技术，其可以被调用以提取验证逻辑规范的实际计算机程序。因此，使用OCaml作为目标提取语言，Coq证明助手机械地提供以下程序：类型'alist=|无|缺点的'a*’a类型 的数据流=|EOS|流的的数据*（单位→’类型的数据延迟=单位→类型'数据关系= '数据→模块类型Machine =sig类型数据类型状态Val转换：状态（数据关系*状态）列表Val初始：状态列表Valterminal：state bool端模E 引擎e=功能（M：机器e）→结构类型选择=（M ：机器e）这是一个真正的LATI ON*M。统计e）上市测试类型回溯=M. 那是个*M。斯塔特选择M。 那是个*M。 State*choice*M. 这是一个真正的LATI ON*M。datadummy*M. 国家typeresumption=backtracklist让rec反应DSres =I fM. 特米纳公司n个Stream（d，（funxchooseds（M. （transitions）res））el s echooseds（M. 把它转过来和选择D schres =匹配 同Nil continue res Cons（p，rest）let（rel，EOS choose d s rest res Stream（react d' s'（缺点（（选择（d，s，rest，rel，del，||B. Razet/Electronic Notes in Theoretical Computer Science 229（5）（2011）119131|→|→|→|→|→|→和继续=function无EOSCons（back，res匹配回来提前（d，s）react dsres'C h o o s e （ d ， s ， r e s t ，r e l ， d e l ， s ' ） m a t c hd e l（ ） withEOS choose d s rest resreact d' s'（缺点（（选择（d，s，rest，rel，del让recinit_resDlaccc =匹配l与|无→访问|缺点（s，休息）→init_resD休息（缺点）（（提前（d，（s））、（acc））设characteristic_relation d =continuee（init_resdM. initialNil）端尽管它的高级字符，这个程序是计算效率。请注意，所有递归调用都是终端调用，因此通过跳转实现。从OCaml程序员那里提取的程序是可以预期的，因为它没有混杂着计算方面不需要的逻辑判断：在react、choose和continue的定义中出现的predh、h1和h2被擦除。读者将检查这个程序确实非常接近原始的有限Eilenberg机[8]，但也非常接近由G'erardHuet[5]或其扩展[6]引入的原始反应式引擎。7示例：下推自动机识别λ-演算的我们在本节中讨论上面获得的反应引擎的效率。为此，让我们在有限艾伦伯格机模型中嵌入一个识别λ演算项的下推自动机。然后，我们将讨论效率的反应引擎执行搜索的解决方案后，这个下推自动机。考虑以下λ-项的歧义语法T：=X（变量）|λx·T（抽象）||T@T（T）（申请）这种语言的终端符号是x、λ、·、@、（、）和@。 符号T是非终结符. 根据这个语法，λ-项“λx.x@ λ x.x”可以被识别为“λx. x”。（x@λx.x）”，但也称为“（λx.x）@（λx.x）”。 因此，一个完整的解析算法应该返回两个解。该文法是上下文无关的，并且可由下推自动机（PDA）识别 让我们回想一下，PDA同时操作磁带和堆栈。要识别的字写在磁带上，堆栈用作弱化存储器（只允许push和pop操作）。图1中给出的PDA识别上述语法的λ-项用于绘制132B. Razet/Electronic Notes in Theoretical Computer Science 229（5）（2011）119开始Fig. 1. 下推自动机（PDA）识别歧义λ-项为了方便起见，初始状态q1是重复的，它的两次出现应被认为是相等的。可能遇到的堆栈符号如下：t、λ、@和（。 用指数+（分别为−）写的标签被解释为 堆栈上的push（相应的pop）操作。不带指数的标签被解释为磁带截断。假设该PDA的运行是用等于λ项的磁带和空栈初始化的。PDA的验收条件是磁带是空的，并且堆栈仅包含符号t。从q1到q的边标记为Acceptenc，表示这是一个接受条件。在Coq规范中，磁带和堆栈被指定为两个列表值。让tape和stack是两个对应的数据集，每个标记这个PDA的操作都很容易编码为关系（tape* stack），因此它满足有限Eilenberg机的第一个条件。还有一个测度依赖于状态的三重数和带与栈的长度，它沿任意边递减;它表明，在深度上的计算必然是有限的，这正是必须服从有限艾伦伯格机的第二个条件。Coq我们得到一个反应式引擎，模拟下推自动机插入M引擎函子。现在我们有了一个完整的λ演算单词识别器。给定一个λ-项，反应引擎会枚举下推自动机的所有可能的 解（枚举 ）。此枚 举按需计 算为流值。例 如，使用 λ 项“λx.x@（λx.λx.x@x）@x@x@λx.x@x”产生一个Q5X年q4t+@@+（年q3（+年q1λQ2XQ7·+Q8λ年q1t−t+接受问6λ−Q9t+QF@−Q10t−Q11t+（−Q12）十三题B. Razet/Electronic Notes in Theoretical Computer Science 229（5）（2011）119133运行时间（秒）0.8 0.80.6 0.60.4 0.40.2 0.20050000100000单词长度（符号数量）1500002000000050000100000单词长度（符号数量）150000200000(a)（b）第（1）款图二、反应引擎的运行时间为：2（a）第一个解决随机生成的二义性2（b）随机生成的无歧义λ-项的唯一解长度522，也就是说，有522种不同的方式来识别项;λ项“x@x @ x @ x@x @ x @ x @ x @ x @ x@x@x@x”产生长度为208012的流与更一般的广度优先搜索相比，反应引擎的深度优先搜索策略具有良好的复杂度特性，而广度优先搜索对于模拟有限Eilenberg机器来说是不需要的。两个基准表明，我们的方法是相关的。图2（a）中的第一个基准测试显示了获得随机生成的λ项的第一个解决方案的反应式引擎运行时间。图2（b）中的第二个基准测试显示了获得随机生成的明确λ项的唯一解的反应式引擎运行时间这两个基准测试都表明，反应引擎的平均运行时间与单词的长度呈线性8结论我们给出了有限Eilenberg机模型的一个完整的规范我们设计并形式化地规定了多集序的一个限制[3]。它允许我们将模拟有限艾伦伯格机的反应引擎由于这些形式化，我们已经能够正式证明反应式引擎关于有限艾伦伯格机的正确性（可靠性和完整性）这里提出的反应式引擎从Coq的扩展中获益[10]。它的定义与OCaml中介绍有限Eilenberg机模型的文章[8]中提出的定义非常接近。由于确定性和非确定性有限自动机（DFA和NFA）和实时传感器是特定的有限Eilenberg机器，因此我们的反应式引擎可以用于解决这些机器上的单词问题此外，我们已经表明，我们的方法解决了更高的复杂性问题，因为我们已经嵌