迭代和标记迭代：从程序员的角度分析传统迭代表示和提出基于Java风格的替代语法

−可在www.sciencedirect.com在线获取理论计算机科学电子笔记325（2016）127-146www.elsevier.com/locate/entcs迭代和标记迭代Bram Geron1和Paul Blain Levy2计算机科学学院，伯明翰大学，Edgbaston，伯明翰，B15 2TT，英国摘要我们从程序员的角度分析了传统的基于和的迭代表示，并表明他们所建议的语法根本不是Java风格迭代的良好表示for，while，break，continue。我们提出了一种替代语法，我们称之为语言进行了分析：我们给指称和操作语义，充分证明这两种语言，和翻译功能的总和为基础的迭代标记关键词：迭代，循环，词法绑定，操作语义，指称语义，高阶语言，lambda演算，de Bruijn指数1介绍1.1概述迭代是编程语言的一个重要特性。在命令式语言中，它在for和while循环中最为人所知。这种循环的意义是重复编码，直到满足某个条件，或者如果永远不满足该条件，则循环发散。这样的循环通常由break和continue来补充。它也被研究在lambda演算设置[13，19，21]。在分类设置中，迭代对应于完整的Elgot monads [9]。它们起源于迭代、迭代和Elgot理论，以及它们的代数和单子[7，1，2，3，23]，它们研究基于和的迭代的变体。 这个场与Kleene monads有关[10，17，18]。1电子邮件：bxg314@cs.bham.ac.uk2电子邮件：P.B. cs.bham.ac.ukhttp://dx.doi.org/10.1016/j.entcs.2016.09.0351571-0661/© 2016由Elsevier B. V.这是一篇基于CC BY-NC-ND许可证的开放获取文章（http://creativecommons.org/licenses/by-nc-nd/4.0/）。●●●128B. Geron，P.B.Levy/Electronic Notes in Theoretical Computer Science 325（2016）127–−V，x. M∶B==′′∑0≤i ≤810 - 20°C迭代可以使用递归实现，但它更简单：递归的语义需要一个最小定点，其中迭代具有简单的基于集合的语义。同样从程序员1.2迭代的和基表示我们研究迭代的两种表示。 首先，经典的基于和的构造它把一个计算T，A M A B变成一个计算T，A M<$B。分类上，这种迭代表示对应于完全Elgot monads [9]。 为了更好地理解这种对应关系，我们引入了一个项构造函数iter。（详情见第2节）ΓvV∶AΓ，x∶AcM∶A+B现在可以使用iter对带有for和while的命令式程序进行编码。例如，左边的程序对应于右边的项势在必行类λ演算x V;publicintfindDuplicate（）{iterV，x.如果p（x）}x=f（x）;然后返回inlf（x）returng（x）;return intg（x）其工作原理如下。iter构造引入了一个新的标识符x，它从V开始。身体被评估。如果body的计算结果为inrW，则循环结束，其结果为W。如果body的计算结果是inlV，那么我们将x设置为V，并继续计算body，直到它的计算结果是inrW。1.3“De Bruijn指数”与基于和的表示的使用命令式语言的程序员经常使用嵌套循环，以及它们相关的break和continue语句，这些语句可能被标记。这样的语句对于编程来说并不是必不可少的，使用break或continue的代码可以重写，这样它就不会使用任何一条语句，但这通常会以可读性为代价。break和continue通常有一种有标签的和一种无标签的形式。在图1的左侧，我们展示了一个用类Java语言编写的程序，其中包含嵌套的带标签的循环和带标签的continue语句。颜色可以是-目前没有。 程序计算公式a[i][0]5a[i][j]evena[i][j]，B. Geron，P.B.Levy/Electronic Notes in Theoretical Computer Science 325（2016）127129return inlproda[i][j]，j+1=//product将为0。（[ ][ ] ==）=（<$（[ ][]））如果i≥9，则return inlsum，i+1如果j≥9，则++return inlprod，j+1∑0≤i ≤8∏∧0≤j≤8}●联系我们+intsum0;publicint findDuplicate（inti=0;i≤8;i++）{如果 a i0 5continueouter;intprod1;publicint findDuplicate（intj=0;j≤8;j++）{即使是一个ij继续内;if（a[i][j] ==0）继续向外;int[i][j];iter=0，0，l1。 设i = 1，i= 1，返回inr sum如果a[i][0]=5，则否则iter =1，0，l2. 设 n_prod，j_p =l2inreturn inr inlsum普劳德，我1否则，如果连a[i][j]，else ifa[i][j] ==0then returninr inlsum，i1其他}sum=sum+prod;intsum=sum;图1.两个程序计算相同的公式。 左边的程序写的是在Java中，右边的程序使用细粒度的 按值调用和基于求和的迭代。相关片段有相同的颜色。两个程序都计算a[i][0]5a[i][j]even a[i][j]。尽管具体的公式对于该示例并不重要。回想一下Java，语句它将隐式地中止内部循环在右边，我们有一个类似的程序来计算相同的公式，但使用基于求和的迭代。我们用颜色来表示直观上相关的片段，因为控制流到这些片段之后的同一个地方：在continueinner和两次return inl，j1之后，控制返回到内部循环的开始。我们在这些碎片周围画了一个实心的紫色盒子。左边prod的赋值也在内部循环的开始之前，我们将其涂成紫色。130B. Geron，P.B.Levy/Electronic Notes in Theoretical Computer Science 325（2016）127⟨⋯⟩return inl返回⟨⋯⟩（）（）●（）●外接对于return inlsum，i+1⟨⋯⟩∶在两次出现之后，控件将跳转到外部循环. 类似地，在两次出现return inr inl之后和之后，控制返回到外部iter的开头。 我们有在那些碎片周围画了一个粗虚线红框。 对sum的赋值左边的也在外部循环的开始之前，我们把它涂成红色。请注意，在左边的（Java）程序中，红框中的两个语句都写得一样：这两个程序都可以工作，但右边程序的语法对程序员来说有两个尴尬之处：(i) 在一种情况下，继续到外部循环（红色），在其他情况下返回inr inl。相同的这使得将代码移入和移出内部循环容易出错。(ii) return inl用于恢复内部和外部迭代。 为了找出控制在哪里恢复，程序的读者必须仔细查找最里面的封闭迭代。相比之下，在Java程序中，continue outer之后控制在哪里恢复是不会有错误的。当有三个或更多具有相同结构的嵌套循环时，这种尴尬会加剧：在右手边，return inl将继续最内层的封闭迭代return inr inl将继续第二个最内层的封闭迭代return inr inr inl将继续第三个最内部的封闭迭代，它将始终是外部迭代。我们称之为事实上，De Bruijn [6]声称他的符号在很多方面都很好，但并没有声称它“对于人类读者来说很容易书写和阅读”。关于De Bruijn指数的简要介绍，我们参考[14];同样的问题也在[4，22]中从不同的角度进行了研究1.4标签迭代（Labelled我们用第二个迭代构造解决了De Bruijn索引的尴尬，我们称之为标记迭代，我们也将拼写为iter。它绑定一个名称x A，具有双重目的：它具有类型A的值。它用作重新启动循环的标签，必须提供一个类型为A●●●●B. Geron，P.B.Levy/Electronic Notes in Theoretical Computer Science 325（2016）127131//product将为0。raisel2proda[i][j]，j+1==（[ ][ ] ==）（<$（[ ][]））如果i≥9，则如果j≥9，则提高n+1，i+1，l1提高生产率，j+1l2++∑0≤i ≤8}∏∧0≤j≤8+intsum0;publicint findDuplicate（inti=0;i≤8;i++）{如果 a i0 5continueouter;intprod1;publicint findDuplicate（intj=0;j≤8;j++）{即使是一个ij继续内;if（a[i][j] ==0）继续向外;int[i][j];iter =0，0，l1。 设i =sum，i=l1，返回sum如果a[i][0]=5，则否则iter =1，0，l2.设n =prod，jn =l2，求l1和prod，i 1否则，即使是[i][j]thenelse ifa[i][j]==0thenraisel1sum，i1其他}sum=sum+prod;intsum=sum;图2.两个程序计算相同的公式。左边的程序是用Java编写的;右边的程序使用带 标 签 迭 代 的 细粒度按值调用。相关片段有同样的颜色。两个程序都计算a[i][0]5a[i][j]even a[i][j]。在图2中，我们将相同的Java程序与使用标记迭代的实现并排放置。与基于求和的迭代一样，带标签的迭代也具有基于集合的语义，但类型系统更复杂。我们将在第3节中更详细地解释标记迭代。我们选择拼写raise是因为它与raising an exception有相似之处;参见第4节的讨论。1.5贡献我们定义了两种语言：我们给出了两种语言的类型系统，指称语义，大步操作语义和充分性定理。我们用第一种语言解释了De Bruijn指数的尴尬，并给出了一个现实的例子。132B. Geron，P.B.Levy/Electronic Notes in Theoretical Computer Science 325（2016）127（1）={0}<$A×B）=<$A×<$B）<$）∈<$）→<$））=）=我们证明了第一个结构可以用第二个结构来宏观表达。对于这两种类型的迭代，我们只研究continue循环：我们省略break因为我们相信这是一个简单的延伸。我们在第2节中定义了基于和的迭代的语言，在第3节中定义了标记迭代的语言。2和基迭代我们根据细粒度按值调用或FGCBV [20]定义了我们的构造，这是按值调用lambda演算的变体，在值和计算之间具有语法分离，并且其中求值顺序是显式的。我们在这里解释FGCBV和基于求和的迭代。FGCBV的语法和类型系统如图3所示。我们给出了一个简单的基于集合的发散语义1（nat）=N<$r）=λ（x∶A）∈Γ（A）<$A+B）=<$A）+<$B）<$A→B）=<$A）→（<$B）+{}）VVA<$<$rcM∶A）∈<$<$r）→（<$A）+{}）普通的FGCBV和基于和的迭代的FGCBV的语义是相同的，当然，除了后者有一个额外的构造。我们在图5中给出了这两种语言的大步操作语义。充分性声明很简单：提案2.1（适足性）(i) 对于没有迭代的普通FGCBV的每个闭项M，存在唯一的V，使得M返回V，并且M为V。(ii) 对于具有基于和的迭代的FGCBV的每个闭项M，● 存在唯一的V，使得M返回V，并且M包括V ，或者● M不归约为终结点，且<$M）=inr。3纯函数类型的标号迭代3.1介绍B. Geron，P.B.Levy/Electronic Notes in Theoretical Computer Science 325（2016）127133为了修复1.3节中指出的De Bruijn索引的笨拙，我们现在给出一种具有有效的“标记迭代”结构的语言。的判决134B. Geron，P.B.Levy/Electronic Notes in Theoretical Computer Science 325（2016）127VWM;succx. N}==的情况V。M; inr y. N}{\displaystyle\mathbb{N}{\displaystyle\mathbb（∶）∈⊢∶⊢∶⊢∶⊢∶v⊢ ∶ ∶ ⊢∶vc⊢ ∶ ⊢∶⊢ ∶ ∶ ⊢∶Cc∶ ⊢∶⊢ ∶ → ⊢∶V，x. M∶B⊢ ∶ ⊢ ∶ ∶ ⊢∶rc是x，y的情形V。 M∶C∶+∶编程c⊢∶值V、Wx0 成功VinlV inr VV，Wλx. M计算M，N∶∶=n返回V，设V为x。M=x。 NA、B、C型∶∶=1自然型→A+B→A×B→A→BxAΓΓvx∶AΓv∶1Γv0∶natVVnatΓ⊢vsuccV∶natVV AV∶A+B中的ΓvΓV AV∶A返回VBV∶A+B中的ΓvΓV AΓ，x A M B令Vbex. M∶BVV AVBΓvV，W∶A×BrM Ar，x A N BrcM到x。N∶BΓ，x AcM BΓvλx. M∶A→BV ABV A BV W∶BΓvV natΓcM CΓ，xnatc{0}的情况V。 M;succx. N}∶CΓV A B Γ，x A M CΓ，y B N C在{inlx. M;inr y. N}∶CΓvV∶A×BΓ， x∶A，y∶B<$cM∶C基于和的迭代ΓvV∶AΓ， x∶AcM∶A+B图3.上图：纯细粒度按值调用的语法。基于求和的迭代只添加一个术语构造，而不添加值或类型;该术语的类型派生如下所示在这种语言中，Δ; ΓcM A用于计算值的ΓvV∶A我们在图6中给出了类型规则。像往常一样，ΓΔ只存在于计算中;它是类型化标签的上下文。外延B. Geron，P.B.Levy/Electronic Notes in Theoretical Computer Science 325（2016）127135（0）=0ρ（）=（）ρ<$inlV）=inl<$V）ρρ<$returnV）=inl<$V）ρρ如果<$M）=inrρ（1）=（2））（三））λx. M）=λ（a∈A））。（μM）ρ（ρ，xλa）⎩（：{0}的第五种情况。 M;succx. 如果<$V）ρ=0，则N}）ρ（ ∶）∈第五集（第一集） M;inr y. 如果<$V）ρ=inla，则N}）ρ=π<$M）（ρ，xπa）一个基于和的迭代算法的改进ks.t. v0=（V）ρ（x∶B）∈Γ（y∶C）∈Δ（<$B））→（<$A）。细粒度按值调用x ρ x（1）ρ= 0<$succV）ρ=1+<$V）ρ<$inrV）ρ=inr<$V）ρ<$V，W<$）ρ=<$V）ρ，<$W）ρ设V为x。 M ρM ρ，xV ρM到X。如果<$M）ρ=inlv，则N）ρ=整数<$N）（ρ，x<$v）<$V W）ρ=<$V）ρ<$W）ρn（ρ，x<$n）如果V=1+n⎧⎪¢N)¢)ρ（N）（ρ，y<$b）如果（五）=inrb第五种情况{x，y}。M}）ρ=<$M）（ρ，x<$a，y<$b）如果<$V）ρ=<$a，b<$第五，x。 M）ρ= π（ρ，x∈vi）=inl inlvi+1M）（ρ，x∈vk）=inl inrw如果没有这样的v0，请提交。k存在图4.细粒度按值调用中的值和术语的指称语义，以及基于求和的迭代构造的语义。的判决是△;r△cA）=（△（B））→（∑<$C）+<$A）+{}）r用于形成值。x B）∈ΓxAΓvx∶AΔ用于形成计算，就像引发异常一样。然而，传统上，异常名称来自一个全局集合。我们的（A）=（A）136B. Geron，P.B.Levy/Electronic Notes in Theoretical Computer Science 325（2016）127此外，当标签被引发时，它必须由B. Geron，P.B.Levy/Electronic Notes in Theoretical Computer Science 325（2016）127137[/ ][/][/ ][/]（[/ ]）⇓0[ /][][][// ][ / /][ /]甲磺酸（）{}[ /]N-异丙基乙胺：（ ∶ ）∈iterV，x. M返回Z0（∶ ×） （∶ ∶）/（∶×）（∶∶）x∶（∶×）（∶∶）x∶（∶ ×） （∶ ∶）∶T∶∶=返回V细粒度按值调用returnV返回VM V x T设V为x。MTM返回VN V xTM到x。NTM W x Tλx。M）WTM T第0个案例，共{0. M0; succ x.Msucc}成功MVx，Wy T{x，y}的情形V，W。 M} TM Vx T{ 0}的case（succ V）。 M0; succ x. Msucc}成功M Vx T情况 输入V的 在10年内，Minl; inr x.MinrT基于和的迭代M Vx Tcase（inr V）of {inl x. Minl; inr x.最小值T∶∶=返回V<$k≥0<$（V1，<$，Vk）<$i∈{1.. k}∶M[Vi−1/x]n = 1ViM[Vk/x]n = 1Z图5.简单的细粒度按值调用和基于求和的迭代的大步操作语义。在我们的操作语义中，封闭术语减少到相同类型的“终端”术语，或者它们在所有.我们使用元变量T表示终端。对于FGCBV及其基于求和的迭代扩展，终端项总是返回V的形式。引入一个单独的终端概念现在看起来可能有点奇怪，但在图8中，我们扩展了FGCBV的规则，并添加了另一种形式的终端。 所以上面的T可能会代表的不是返回V对应的类型。 键入规则如下：VA x AΔΔ;r=c升高xV∶B因此，我们有这些判断。xnatbool ;ynat，zboolcraise3，true stringxnatbool;ynat，zboolcraisey，z 0xnat bool ;ynat，z boolcreturny nat但我们不能提高识别率：xnatbool ;ynat，zboolcraisey3我们也可以不使用标签的价值：138B. Geron，P.B.Levy/Electronic Notes in Theoretical Computer Science 325（2016）127（ ∶×） （∶ ∶）/∶ ×xnatbool ;ynat，zboolcreturnxnat bool实际上，return的类型规则（参见下一页的图6）表明x不是B. Geron，P.B.Levy/Electronic Notes in Theoretical Computer Science 325（2016）127139Γvx∶A⊢∶⊢∶⋅ ∶ ⊢∶⊢ ∶ ∶ ⊢∶⊢ ∶ ∶ ⊢∶⊢∶⊢ ∶ → ⊢∶⊢∶⊢ ∶⊢∶⊢ ∶ ⊢ ∶ ∶ ⊢∶⊢∶×∶ ∶⊢∶vc∶+∶编程c⊢ ∶ ∶ ∶ ⊢∶：（ ∶ ）∈∶ ∶⊢∶×值和类型与第133图3中的细粒度按值调用相同。计算M，N∶∶= N×V，x。M升xV（x∶A）∈ΓVV AΔ; ΓcreturnV A;r，x AcM BΓvλx. M∶A→BΓvV AΔ; Γ，x AcMB令V为x。M BΔ; ΓcM AΔ; Γ，x AcN BΔ; rcM到x。N BV ABV A BΔ;r=V W∶BΓ⊢v⟨⟩∶1VVAV∶A+B中的ΓvVBV∶A+B中的ΓvΓvVnatΔ; ΓcM CΔ; Γ，x AcN CΔ;r={0. M;succx. N}∶CΓV A B Δ; Γ，x A M CΔ; Γ，y B N CΔ;r={inlx. M;inr y. N}∶CΓV A B Δ;Γ，x A，yB M CΔ;r∈c，v∈x，y∈ v。 M∶CΓvV AΔ，x A;Γ，x AcM BΔ;r∈CiterV，x. M∶BVA x AΔΔ;r=c升高xV∶B图6.标号迭代的迭代次数。在要返回的参数的上下文中可用：ynat，zboolvVnat bool（x∶nat×bool）;（y∶nat，z∶bool）n阶返回V∶nat×bool我们使用的语法上独立的名称与肯尼迪[16]使用的函数名称类似。140B. Geron，P.B.Levy/Electronic Notes in Theoretical Computer Science 325（2016）127––Δ;r∈CiterV，x. M∶B（ ∶）∈（∶）∈（ ）−Δ;Γc返回V∶AΓvλx. M∶A→B标号迭代我们现在希望使用标号来推广iterV，x。M从最后一节开始。记住，当M减少到返回inlV，则循环应该以值V重试，返回inr W，则循环的结果是W。我们的新符号也是iter V，x。 M. 然而，这里x既是标识符又是标签：ΓvV∶AΔ，x∶A;Γ，x∶A<$cM∶B同样地，当写iterV，x时。当M减少到提高V，则循环应该以值V重试，raiseyW，y x 然后循环应该中止并且循环y应该以值W重试返回W，则循环的结果是W。我们希望重复一遍，相同的名称x可以同时出现在Δ和Γ中。 我们不对x AΔ和x BΓ作任何一般的句法限制，使它们具有相同的类型。 然而，为了能够形成iterV，x。M，我们必须使x在相同类型的Δ和Γ中。在这一点上，我们还希望注意到，我们在绑定图[8]上定义了我们的语言的语义，也就是说，在抽象语法模α-等价上。标号迭代和λ既然计算的上下文与值的上下文不同，传统的细粒度按值调用判断必须进行调整才能在这种设置下工作。图6中返回的类型规则很简单：当我们从计算向上移动到值判断时，我们只需忘记Δ。V∶A但是，对于λ，我们有一个选择：Δ应该是什么？ 我们采取似乎是唯一合理的选择：将Δ重置为空的上下文，即Δ。n;r，x∶A<$cM∶BJava同意这种选择：在当前方法之外编写带标签的continue或break是语法错误[11]。从程序员B. Geron，P.B.Levy/Electronic Notes in Theoretical Computer Science 325（2016）127141（：（nat）=N(iii)-是的<$A×B）=<$A×<$B）⋅ ⊢∶⋅ ⊢∶∶′ ′→（∶）∈（）∶′ → ⋅′ → ⋅Δ′; Γ′ Δ;ΓΔ′Δ⊆（∶）∈（）（（）∶）σ∶Δ′; Γ′ →Δ; Γ<$→）=<$）→（<$）+{}）′→（∑（∶）∈）+<$）+{}）（∈Ⅲ））（x∶B）∈Γ（y∶C）∈Δ（A）=（A）<$B））→<$A）A B AB3.2指称语义回想一下，术语和值判断的语义如下。<$Δ;<$cA）=（<$<$B））→（∑<$C）+<$A）+{<$}）x B）∈Γ类型的表示如下。<$1）={}<$A+B）=<$A）+<$B）我们在图7中给出了术语和值的语义。我们使用以下符号表示三进制和xBΔBA的元素：(i) 对于A，返回a（与术语表示法比较：返回V），(ii) raisexb（forb ∈B））（与术语符号比较： 升高xV），3.1我们说：“比什么都强，比什么都弱。换句话说，我们说Δ;Γ比Δ′; Γ′弱。一个上下文中的术语也是一个较弱上下文中的术语，具有相同的推导。上下文中的值也是较弱上下文中的值，具有相同的派生。定义3.2[封闭性](i) 当vV A时，我们说V是闭的。(ii) 当Δ;cMA，那么我们说M是封闭的。定义3.3替代（两区上下文之间）σΔ; rΔ; r由两部分组成，● 对于每个标签x AΔ′，Δ中的A型标签σlabx，以及● 对于每个标识符x AΓ′，有一个值σidx ΓvσidxA。备注3.4从一个两区代换，我们可以很容易地得到一个单区代换Γ。 由于符号的滥用，我们也将这个在单区上下文中获得的替换记为σ。 同样，从一个区域替代σrr，我们平凡地得到一个两区代换;r; r，我们也把它记为σ。142B. Geron，P.B.Levy/Electronic Notes in Theoretical Computer Science 325（2016）127<$）=ρ（V）=raise（V）xρxρ（Ⅲ）<$<$）=<$<$$>）<$） ρρ<${}）=<$）（））=（1）=（2）Γσ∶ Γ′→ Γ类似地，ΓvV σ∶A。σ∶Δ′; Γ′→ Δ;Γ∈（）●x∈Δ raisexVx（）下一页<$succV）ρ=1+<$V）ρ⊢ ∶ ⊢∶（ρ>）如果M=returnv{0}的第五种情况。 M;succx. 如果<$V）ρ=0，则N }）ρ =零第五集（第一集） M;inry. 如果<$V）ρ=inla，则N}）ρ=π<$M）（ρ，xπa）返回wif n=0.. ks.t. v0=（V）ρ第五，x。 M）ρ=λraiseywifλv0. ks.t. v0=（V）ρ（x）ρ=ρ（x）（0）ρ=0<$returnV）ρ=return<$V）ρ令V为x。 M）ρ=<$M）（ρ，x<$<$V））<$inlV）ρ=inl<$V）ρρρρ，x vρ<$inrV）=inr<$V）M到X。如果<$M）ρ=raiseyw，则N）ρ=raiseywV WρVρWρ如果<$M）=1000，V，W V，Wλ x. M）ρ= λ（a ∈ A））。（ρ，xa）ρ<$）=<$）<$）n（ρ，x<$n）如果V=1+n⎧⎪¢N)¢)ρ（N）（ρ，y<$b）如果（五）=inrbx，y的情况V。Mρ Mρ，x a，y b如果Vρa，b⎪∧i∶M）（ρ，x∈vi）=raisexvi+1（ρ，xvk）=returnw⎪∧i∶M）（ρ，x∈vi）=raisexvi+1⎪⎪⎩ıMρ，x vkraiseyw如果没有其他情况匹配图7. 带有标记迭代的语言的项和值的指称语义。 另见 第3.2节。我们可以用如下的替换项 给定一个术语Δ′; Γ′cM A，我们通过下式获得项Δ;ΓcMσ A：对于任何，用raiseσlab（x）V σ代替所有出现的（其中是free），其中Vσ类似地通过归纳法给出和● 对于任何xΓ，用σ id x替换标识符的所有值出现。对于单区域上下文，我们有通常的替换概念，将s值（overrr）分配给r′的每个子项。并给出了V∶A，得到两区上下文及其替换形成一个类别，一区上下文及其替换形成另一个类别。B. Geron，P.B.Levy/Electronic Notes in Theoretical Computer Science 325（2016）127143也就是说，替换可以结合地组合，并且组合具有同一性。引理3.5（替换引理）144B. Geron，P.B.Levy/Electronic Notes in Theoretical Computer Science 325（2016）127iterV，x. M返回Z0iterV，x. M升高Z0y<$Vσ）=<$V）。ρ（x<$σ（x）′ρx∈Γ==∈(ii)设两区代换σ∶Δ′; Γ′→Δ; Γ。M∶Aρx∈ΓX(ii) 如果M raisexV，则<$M）= raisex<$V）。T∶∶=返回V升高xVM升高VM到X。N升高xV<$k ≥ 0 <$（V1，<$，Vk）<$i ∈ {1.. k} ∶ M [V i−1/x] n =增加xV iM [V k/x] n=返回Z<$k≥0<$（V1，<$，Vk）<$i∈ {1.. k} ∶M [V i−1/x]n +xV iM[V k/x]n +yZ（xy）图8. 标记迭代的大步操作语义。 该图扩展了图5。 也就是说，我们添加了 规则，我们添加了一种新的终端形式：raisex V。(i) 给出了单区代换σ∶Γ′→ Γ。若Γ′≠V∶A，则若Δ′;Γ′∈cM∶A，则<$Mσ）ρ=f（<$M）（x<$<$σ（x）’），3.3操作语义我们定义了封闭项c之间的一个大步和（闭）终端Δ;Δt=T∶A，使得对于每个M要么(i) M T 返回V，或(ii) M T raisexV，xdom Δ，or(iii) M不会减少。推导规则如图8所示，归约关系定义为它们的最小不动点。定理3.6（充分性）（i）如果M返回V，则<$M）=返回<$V）。(iii)如果M不减少，则<$M）=。其中f映射提升xv到提升σ实验室;实验室IDB. Geron，P.B.Levy/Electronic Notes in Theoretical Computer Science 325（2016）127145ΓM∶AΓV∶Atranslate（M） translate（V）⋅ ⊢ () ∶ ⊢ (）：则<$M）=<$translate（M））。ρ ρ则<$V）=<$translate（V））。ρ ρ{（）下（Ⅲ）M'Ttranslate（M）T′<$T）=<$T）3.4从基于求和的迭代转换让c或v是语言中的项或值，具有基于求和的迭代。 我们从 基 于 求 和 的 迭 代 中 定 义 一 个 翻 译 ， 使得;ΓctranslateMA 或Γv平 移 VA， 分 别 在 具 有 标记 迭 代 的 语 言 中。translation宏扩展sum-basediter如下。其他结构保持不变。translate（iterV，x. M）=iterV，x。（translate（M）toresult.“}）案例结果 inly. 提高xy;提高x returnx其中translateM通过将x添加到Δ而被隐式地削弱。定理3.7（翻译保持语义）(i) LetΓcM∶A是语言中的一个项，它以和-b为定义元，ρ∈Γ）.(ii) Letr∈vV∶A是一个以sum-b为定义元的语言的值，且ρ∈r.推论3.8如果在具有基于和的迭代的语言中，那么在具有标记迭代的语言中存在这样的，并且。如果M不约化为终端，则translate（M）不约化为终端。4讨论和相关工作在标号迭代的介绍中，我们选择只考虑纯函数。今后的一项重要任务是扩展目前的系统，以便允许产生迭代的功能。我们已经注意到De Bruijn索引在迭代之外的设置中很笨拙。例如，在Haskell等函数式语言中，习惯使用monad transformer [12]来嵌入具有多个副作用的命令式程序，但它们会出现类似的De Bruijn索引尴尬：第i个monad transformer通过编写“lift i e transform“来解决这个问题和提出的解决方案已经在文献[15，24，5]中进行了研究，但使用标签解决问题似乎尚未探索。命令式语言使用标识符来处理可变单元，并且使用标签来处理对象可能也会有利于类似函数程序的可读性。许多编程语言不仅有unlabeled和labeledcontinue，在此之后，我们模拟了iter和raise的组合，而且还有unlabeled和labeledbreak。引入一个绑定到一个类似iter的标签，但是当标签用参数a引发时，该构造的结果是a，因此该标签的引发类似于break。这样一个结构，终端146B. Geron，P.B.Levy/Electronic Notes in Theoretical Computer Science 325（2016）127与本文中使用的raise类似，类似于异常处理的过程内形式。如果我们在这个新的结构中包装一个iter5结论在这篇文章中，我们总结了基于和的迭代表示的本质，并从编程的角度对其进行了评估。虽然从语义的角度来看，它可能工作得很好，但对于程序员来说，它不足以进行编程。我们提出了一种替代的迭代表示，适合程序员，但仍然有相对干净的语义。引用[1] Peter Aczel，Jiuhí Adámek，Stefan Milius，and Jiuhí Velebil. 无限树和完全迭代理论：共代数观点。理论计算机科学，300（1[2] Jií Adámek，Stefan Milius，and Jií Velebil. Elgot代数计算机科学中的逻辑方法，2（5），2006年11月。[3] Jií Adámek，Stefan Milius，and Jií Velebil.埃尔戈理论：迭代方程性质的新观点。Mathematical Structuresin Computer Science，21（Special Issue 02）：417[4] Stefan Berghoun和Christian Urban。德布鲁因指数和名称的头对头比较Electronic Notes in Theoretical Computer Science，174（5）：53[5] 埃 德 温 · 布 雷 迪 用 代 数 学 和 依 赖 类 型 进 行 编 程 和 推 理 。 在 Proceedings of the 18th ACM SIGPLANInternational Conference on Functional Programming，ICFPACM。[6] N. G. 德布鲁因 λ演算符号与无名假人，一工具为自动公式操作，并应用于Church-Rosser定理。Indagationes Mathematicae（Proceedings），75（5）：381[7] 卡尔文·C.埃尔戈特一元计算与迭代代数理论。In H. E.罗斯和J. C. Shepherdson，编者，《逻辑与数学基础研究》，逻辑讨论会爱思唯尔，1975年。[8] M. Fiore ，G. Plotkin 和D.图里抽象语法和变量绑定。1999 年第14届计算机科学逻辑研讨会。Proceedings，pages 193-202，1999.[9] Sergey Goncharov ， Christoph Rauch ， and Lutz Schröder.共 归 纳 恢 复 上 的 无 保 护 递 归 。 在Proceedings of the 31st Conference on the Mathematical Foundations of Programming Semantics（MFPS XXXI ） ， 第 319卷 ， Electronic Notes in Theoretical Computer Science ， 第 183-198 页 。Elsevier，2015年12月。[10] 谢尔盖·贡恰洛夫卢茨·施罗德和蒂尔·莫萨科夫斯基Kleene Monads：Handling Iteration in a Framework ofGeneric Eectors. 在 Alexander Kurz ， Marina Lenisa ， and Andrzej Tarlecki ， editors ， Algebra andCoalgebra in Computer Science， number 5728 in Lecture Notes in Computer Science ， pages 18SpringerBerlin Heidelberg，2009年9月DOI：10.1007/978-3-642-03741-2_3。[11] 詹姆斯·高斯林比尔·乔伊盖伊·L斯蒂尔吉拉德·布拉查和亚历克斯·巴克利Java语言规范。Addison-Wesley，Upper Saddle River，NJ，java se 8 edition，2014.[12] 马克·P·琼斯重载和高阶多态的函数式编程。 在Johan Jeuring和Erik Meijer编辑的Advanced FunctionalProgramming，第925卷，第97- 99136. Springer，1995年。