没有合适的资源?快使用搜索试试~ 我知道了~
《理论计算机科学电子札记》59卷第4期(2001年)URL:http://www.elsevier.nl/locate/entcs/volume 59. html17页s实践中的句法理论Olivier Danvy和Lasse R. 尼尔森金砖国家1丹麦奥胡斯大学计算机科学系,540号楼,丹麦电子邮件:{danvy,lrn}@ brics.dk摘要语法理论的求值函数被规范地定义为传递闭包,它是(1)将程序分解为求值上下文和redex,(2)收缩这个redex,(3)将结果插入上下文。因此,直接实现这个评估功能产生一个解释器的最坏情况下的开销,对于每一步,这是线性的输入程序的大小。我们在语法理论上提出了足够的条件来规避这种开销,并说明了该方法与按值调用λ-演算的解释器和到连续传递风格(CPS)的转换。特别是,我们机械地改变这个CPS变换的时间复杂度从潜在的二次线性。扩展版本可作为技术报告BRICS RS-01-31 [4]获得1介绍语法理论提供了一个统一、简洁和优雅的框架来指定一种编程语言并对其进行推理[5]。我们考虑的问题,实现的句法理论的形式的解释器的评价功能然而,我们的重点不是自动化这个过程,在Xiao和Ariola2相反,我们展示了如何规避直接实现评估函数所带来的开销首先,我们要确定开销。然后,我们列出了足够的条件来改写句法理论,以便实现其评估功能不会产生这种开销。证明这些条件是充分的是建设性的,因为它表明如何机械地改写句法1计算机科学基础研究(www.brics.dk),由丹麦国家研究基金会资助。2www.cs.uoregon.edu/~ariola/SL/2001年由ElsevierScie nceB出版。 V. 操作访问和C CB Y-NC-ND许可证。DANVY和 NIELSEN2的|理论来规避开销。我们考虑两个例子:用于按值调用λ -演算的句法理论和由于Sabry和Felleisen [8]而将λ -项转换为延续传递风格。2重新聚焦于句法理论句法理论是一个小步骤语义学,其中求值被定义为单个归约的传递闭包,每个归约都是通过(1)将程序分解为上下文和redex,(2)收缩redex,以及(3)将收缩的结果插入上下文中来执行的大多数句法理论满足一个唯一的分解性质。对应于其求值函数的句法理论的解释器自然由分解-收缩-插入循环组成。通常,分解的唯一可行实现是在抽象语法树中进行深度优先搜索。因此,分解步骤引入了与程序大小成比例的显著开销。类似地,插入也可能花费与程序大小成线性关系的时间,尽管它总是最多花费与下面的分解一样长的时间,如果有分解的话,如下所示例如,下面是按值调用λ演算的语法理论:e ∈ Λe::= x|λx.e|eev∈值v::= x|λx.ex∈VarsE∈ EvContE::= [ ] |Ee| vE r ∈Redexr::= v v用表达式填补求值上下文的漏洞的定义与往常一样:([ ])[e] =e(E eJ)[e] =E[e]eJ(v E)[e] =vE[e]唯一的归约规则如下:E[(λx.e)v]→E[e[v/x]]分解导致线性开销,因此评估可能需要二次时间。让我们用教会数字来说明这种复杂性:[n|是数字n 的丘奇数,即,λs.λz. s(s(. (sz).. . ))).“我的天,n例2.1我们考虑项n(λx.x)v,其中v是任意值。这一项在两个步骤中简化为(λx.x)((λ x. x)((λx.x)(. ((λx.x)v).. . ))。 从“我的天,nDANVY和 NIELSEN3××然后,每次分解到上下文和redex,总是(λx.x)v,花费的时间与剩余应用程序的数量成比例。因此,总的计算时间是O(n2)。✷例2.2更一般地说,让我们考虑术语(λx.x)((λx.x)((λx.x)(. ((λx.x)e).. . )))“我的天,n其中e在m步中减少到v。时间复杂度为O(n + n),但时间复杂度为O(n+n)。实 际 上,因子n被附加到m个约简步骤中的每一个步骤,因此在这种情况下将e约简为v的时间复杂度至少为O(m n),之后我们回到前面的例子。✷我们提出了一种替代实现连续的plug-and-decom- pose操作,避免了开销。在这个替代实现中,plug和decode的组合被我们称为refocus的单个函数所取代。这种替换只有在句法理论满足了某些性质时才是可能的,这些性质本质上相当于下一个redex在decomposition的深度优先遍历中发生的时间比任何其他可能出现在求值上下文中的表达式都要晚。我们表明,如果句法理论是在“标准”的方式通过值和求值上下文的上下文无关我们还展示了如何构造一个重聚焦函数,以避免开销。2.1上下文无关句法理论(术语)首先,我们可以假设语言语法的一些属性。我们正在使用抽象语法,即,程序是抽象语法树,其中每个节点由语言语法中的产生式创建。因为抽象语法不需要对应于具体语法,所以我们可以不失一般性地假设(1)所有的产生式都具有以下形式:e::= c(e1,.,e n)对于某个终端符号C和非终端E1,.,e n,以及(2)只有一个使用c的产生式。我们把终结符c称为构造函数,把非终结符e称为项标识符。从语法的每个非终结符生成的术语集合与该非终结符相关联,并且非终结符用于指代该集合中的任何元素。当我们在形式e::= c(e1,.,e n),与e相关的集合称为E XP,由e1到e n覆盖的集合分别称为E XP1到E XPn。我们假设没有平凡的句法范畴,即,其中EXPi只包含零个或一个元素。有一些标准的方法可以将任何文法转换成一个等价的文法,而没有琐碎的句法范畴[6,4.4节DANVY和 NIELSEN4◦我们还要求句法理论由值、求值上下文和赎回的上下文无关语法来定义(Xiao,Sabry和Ariola也对术语和评估上下文做出了这种假设[11]。2.2上下文无关句法理论(价值观)如果e::= c(e1,.,e n)是语言语法中的产生式,则值的产生式具有以下形式:v::= c(x1,.,x n)其中xi是项标识符ei,或者是像v一样表示值的非终结符。我们称这种非终结符为值标识符。值标识符vi的值项集合称为VALi,并且必然是EXPi的子集。2.3语境无关句法理论(Context-free syntax theories)类似地,求值上下文由以下形式的语法给出:E::= [ ] | c (x1,...,xi−1,E i,x i+1.,x n) | ...其中xj我们称这种非终结符为上下文标识符。终端[ ]被称为上下文的洞二元运算符构造两个上下文的组合。它根据第一个参数的结构归纳地定义如下。[]E2=E2c(e1,. ,E,. ,e n)∈ E2= c(e1,. ,E E2,. (e)因此,组成满足(E1<$E2)[e] =E1[E2[e]]。具有组合的上下文形成幺半群,其中空上下文[ ]是单位,并且所有其他求值上下文可以通过组合基本上下文来构造,即,其中直接子上下文是漏洞的上下文,例如, c(x1,. ,xi−1,[],x i+1,. ,xn)。因为组合是关联的,所以我们可以定义评估上下文,对左边或右边的构图作出反应。例如,在第2节开始时,我们给出了EvCont的传统定义,其中评估上下文由左侧的组合创建。我们还可以指定EvCont,以便通过右侧的组合创建评估上下文E∈ EvContE::= [ ] |E [[ ] e] |E [v []用表达式填充求值上下文的漏洞然后迭代地定义如下:([ ])[e] =e(E[[]eJ])[e]=E[e eJ](E[v[ ]])[e] =E[v e]DANVY和 NIELSEN5| || ·|在评估上下文表示从项到项的函数的意义上,它是单射的,即,如果E[e] =E[eJ],则e=eJ。这种内射性可以通过E上的结构归纳法来证明。我们将求值上下文的深度E定义为创建它所使用的生成的数量,我们将其写为E,并将深度函数在求值上下文的结构上归纳定义如下。|=零|= 0|c (e1,...,E,.,e n)|= 1 + |E|人们可以很容易地证明,|E1和E2|为|E1|+的|E2|和|E| = 0 E = [ ].我们还定义了一个基于合成运算的评价上下文的偏序:如果存在一个EJ使得E2=E1<$Ej,则E1≤E2。这关系是自反的、反对称的和传递的(简单证明省略)。如果两个求值上下文都小于第三个,那么这两个上下文本身是相关的。这是由求值上下文的语法结构得出的,因此我们可以唯一地定义任何上下文集合关于排序的最大下界。我们写E1E2求E1和E2如果E1严格小于E2,即,当E1≤E2且E1=/E2时,采用传统的记法E1 j,即,如果e1是序列没有分解与除非它们满足这两种情况之一。✷的关系是自反的、对称的和传递的(省略证明),即,这是一个排序关系。它也是一个整体,即,对于同一项的任意两个分解,E1[e1] =E2[e2],或者是(E1,e1)±(E2,e2),或者是(E2,e2)±(E1,e1). 这可以从任意两个分解得出,E1[e1] =E2[e2],至少三种情况之一:(i) E1E2=E1,在这种情况下,E1 i,则refocusaux(ei, . . ,[],ei+1, . . ,en),v)=refocus(ei+1, Ef oc1(e1, . . ,v,[], . . . ,en))。NB:(E_c1(e1, . . . ,v,[], . . . ,en),ei+1)<$(Eci(e1, . . . ,[],ei+1, . . ,en),v).她需要一个子归纳法来说明对us (ei+1, E_(?)c( e1 , . . ,v,[ ],.,e n))最终计算值,或者调用具有小于(E_i(e1, . . . ,[],ei+1, . . ,en),v).这是一种结构归纳法。我们知道,对于一个-元素,(e,E),重新聚焦,或者发生上述情况,或者重新聚焦调用自身,其中参数为s直到small er(wrt. i)than(Eci(e1, . . . ,[],ei+1,...,e n),v),并且在结构上小于e,保证最终的 终端,民族 这三种情况如下。• refocus调用refocusaux时使用的参数与它自己收到的参数相同(顺序相反)。这些参数小于(Eci(e1, . . ,[],ei+1, . . ,en),v)通过归纳总结。• 重新聚焦以作为评估上下文的结果和Redex。• refocus用结构上更小的参数来调用自己,并且这是一个错误的decompositionthan(Eci(e1, . . ,[],ei+1, . . ,en),v).证明了如果(E1,e1)<$(EJ,EJ)和E1/EJ(即,<由于定义中的第二种情况,则任何其他分解(E2,e2)满足E1
下载后可阅读完整内容,剩余1页未读,立即下载
![zip](https://img-home.csdnimg.cn/images/20210720083736.png)
![pdf](https://img-home.csdnimg.cn/images/20210720083512.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://profile-avatar.csdnimg.cn/default.jpg!1)
cpongm
- 粉丝: 4
- 资源: 2万+
上传资源 快速赚钱
我的内容管理 收起
我的资源 快来上传第一个资源
我的收益
登录查看自己的收益我的积分 登录查看自己的积分
我的C币 登录后查看C币余额
我的收藏
我的下载
下载帮助
![](https://csdnimg.cn/release/wenkucmsfe/public/img/voice.245cc511.png)
会员权益专享
最新资源
- VMP技术解析:Handle块优化与壳模板初始化
- C++ Primer 第四版更新:现代编程风格与标准库
- 计算机系统基础实验:缓冲区溢出攻击(Lab3)
- 中国结算网上业务平台:证券登记操作详解与常见问题
- FPGA驱动的五子棋博弈系统:加速与创新娱乐体验
- 多旋翼飞行器定点位置控制器设计实验
- 基于流量预测与潮汐效应的动态载频优化策略
- SQL练习:查询分析与高级操作
- 海底数据中心散热优化:从MATLAB到动态模拟
- 移动应用作业:MyDiaryBook - Google Material Design 日记APP
- Linux提权技术详解:从内核漏洞到Sudo配置错误
- 93分钟快速入门 LaTeX:从入门到实践
- 5G测试新挑战与罗德与施瓦茨解决方案
- EAS系统性能优化与故障诊断指南
- Java并发编程:JUC核心概念解析与应用
- 数据结构实验报告:基于不同存储结构的线性表和树实现
资源上传下载、课程学习等过程中有任何疑问或建议,欢迎提出宝贵意见哦~我们会及时处理!
点击此处反馈
![](https://img-home.csdnimg.cn/images/20220527035711.png)
![](https://img-home.csdnimg.cn/images/20220527035711.png)
![](https://img-home.csdnimg.cn/images/20220527035111.png)
安全验证
文档复制为VIP权益,开通VIP直接复制
![](https://csdnimg.cn/release/wenkucmsfe/public/img/green-success.6a4acb44.png)