减少与无约简归一化的建设方法

理论计算机科学电子笔记124（2005）79-100www.elsevier.com/locate/entcs从基于减少的到无约简归一化Olivier Danvy1金砖国家2丹麦奥胡斯大学计算机科学系，地址：Aabogade 34，DK-8200 Aarhus N摘要我们提出了一个系统的建设减少自由规范化功能。从基于归约的归一化函数开始，即，一步归约函数的传递闭包，我们连续地对其进行重新聚焦（即，森林砍伐的中间减少条款），简化（即，融合辅助功能），再功能化（即，Church编码）和直接式变换（即，CPS变换的逆）。我们考虑两个简单的例子，并详细处理它们：对于第一个，算术表达式，我们构造一个求值函数;对于第二个，自由幺半群中的项，我们构造一个基于累加器的递归函数。得到的两个函数是传统的无归约归一化函数。建设建立在以前的工作重新聚焦和评价和抽象机器之间的功能对应。它也是可逆的。关键词：评估规范化，重新聚焦，去功能化，继续传递风格（CPS）。1介绍通过评估进行规范化是一种规范化术语的“无归约”方法。而不是反复减少一项向其正常形式，如1 电子邮件地址：danvy@brics.dk主页：http://www.brics.dk/~danvy2计算机科学基础研究（www.brics.dk），由丹麦国家研究基金会资助。1571-0661 © 2005 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.01.00780O. Danvy/Electronic Notes in Theoretical Computer Science 124（2005）79在传统的基于归约的方法中，使用不构造任何中间项并且直接产生范式（如果存在任何范式的话）的可拓正规化函数[22]。通过评估的规范化已经在直觉类型理论[14，37，44]，证明理论[9，10]，范畴理论[5，16，41]，λ-可定义性[32]，部分求值[18，19，26]和形式语义学[1，29，30]。归约的术语和概念越复杂，归一化函数就越复杂。因此，通过求值进行归一化需要扩展定义一个非平凡的无归约归一化函数[6，7]。然而，我们的论点是，基于归约的归一化函数的计算内容，即，一个函数被定义为一步归约的传递闭包，可以为构造一个无归约的归一化函数铺平道路：我们的出发点：我们从术语语言的归约语义开始[28]，即，一个抽象的语法，一个以redex和相应的收缩函数的集合形式的归约概念减少战略。归约策略采用文法的形式的约简上下文，其关联的插入函数，以及将项映射到值或约简上下文和redex的分解函数（我们假设此分解是唯一的）。这样，我们定义了一个一步归约函数，它的固定点是值，否则它将一个非值项分解为一个归约上下文和一个redex，收缩这个redex，并将contractum插入上下文：非值分解上下文×redexter.M.一步。.还原..恒等式×收缩式JJ，context× contractumterm插头基于归约的归一化函数被定义为该归约函数的自反和传递闭包。重新聚焦：在达到范式的过程中，基于归约的规范化函数反复分解、收缩和插入。Ob-大多数情况下，分解函数应用于插塞函数的结果[25]，Nielsen和作者建议O. Danvy/Electronic Notes in Theoretical Computer Science 124（2005）7981通过将decomposition函数和plug函数的组合替换为将归约上下文和合同直接映射到下一个归约上下文和redex（如果有的话）的refocus函数，这种重新聚焦的归一化函数（即，使用重聚焦函数而不是分解函数和插入函数的归一化函数）可以被看作是抽象机器。函数对应：抽象机器通常是一个去函数化的连续传递程序[2，3，4，13，21]。在这种情况下，这样的抽象机器可以被重新功能化[24]并转化为直接风格[17]。根据我们的经验，从术语语言的归约语义开始，我们可以将相应的基于归约的规范化函数重新聚焦到抽象机器中，并将该抽象机器重新功能化为无归约的规范化函数。我们已经成功地尝试了这种构造的微积分，无论是弱头规范化和完全规范化。本文的目的是用算术表达式和自由幺半群的项的简单例子来说明它。概述：在第2节中，我们在标准ML中完整详细地实现了算术表达式的归约语义，并定义了相应的基于归约的归一化函数。 在第3节中，我们将第2节中基于约简的归一化函数重新聚焦到抽象机器中，并给出相应的无约简归一化函数。在第4节和第5节中，我们对自由幺半群中的项进行了同样的处理第2节和第4节可能看起来很吓人;但是，除了它们 在ML中表示，它们描述了Felleisen和他的同事在过去二十年中开发的直接归约语义[27，28，45]。因此，这两个部分具有平行结构。类似地，为了强调从基于归约的归一化函数构造无归约的归一化函数是系统的，我们还第3节和第5节为平行结构。必要条件：读者应该熟悉编程语言标准ML [39]，归约语义[25，28]，CPS变换[23，43]和去功能化[24，42]。特别是，我们建立在延续和评估上下文之间的关系上[20]。82O. Danvy/Electronic Notes in Theoretical Computer Science 124（2005）792算术表达式为了定义简化算术表达式（整数字面量和加法）的归约语义，我们指定了它们的抽象语法，它们的归约概念（计算两个整数的和），它们的归约上下文和相应的插入函数，以及如何将它们分解为归约上下文和最左最内的redex（如果有的话）。然后，我们定义了一个单步约简函数，它将非值项分解为约简上下文和redex，收缩redex，并将contractum插入上下文。我们最终可以定义一个基于归约的归一化函数，该函数重复应用一步归约函数，直到得到一个值，即，一个正常的形式，达到。2.1抽象语法算术表达式是一个文字或两个项的相加数据类型term = LIT ofint| ADD of term * term2.2归约概念redex是两个字面值的和，我们通过计算这个和来实现收缩数据类型redex =int*int 的SUM（* contract： redex -> term*）fun contract（SUM（n1，n2））= LIT（n1 + n2）最左最内的归约策略收敛并产生一个文字。2.3约简背景我们求一个项中最左最内的Redex。归约上下文的语法和对应的插入函数如下：数据类型context = C0| 术语* 上下文的C1| int* context的C2（* plug： context * term -> term*）fun plug（C0，t）= t| 塞（C1（t ' ， c ） ， t ）= plug（c，ADD（t，| 插头（C2（n，c），t）=plug（c， ADD（LIT n，t））O. Danvy/Electronic Notes in Theoretical Computer Science 124（2005）79832.4分解项是值（即，它不包含任何redex），或者它可以被分解为约简上下文和redex：数据类型value_or_decomposition =术语的VAL| 上下文的DEC * redex(No项被卡住了）。分解函数递归地搜索一个项中最左边最里面的redex。它通常在文献中没有具体说明[28]。我们在这里以我们在之前的约简语义研究中发现方便的形式定义它[25]，即使用两个辅助函数，decomposition（*decompose=| decode'（ADD（t1，t2），c）= decode（*=VAL（LIT n）|decompose'_aux（C1（t2，c），n）= decode| decompose'_aux（C2（n'，c），n）= DEC（c， SUM（（* decompose： term -> value_or_decompose*）函数分解t= decompose引理2.1项t或者是一个值，或者存在一个唯一的上下文c，使得decodet的值为DEC（c，r），其中r为redex。证据立 竿 见 影 的Q2.5一步还原我们现在可以定义一个一步归约函数，它（1）将一个非值项映射到一 个 归 约 上 下 文 和 一 个 redex 中 ， （ 2 ） 收 缩 redex ， （ 3 ） 将contractum插入到归约上下文中（* reduce： term -> term*）乐趣减少=（case decodetof（VAL=> t|（DEC（c，r））=>plug（c，contract r））84O. Danvy/Electronic Notes in Theoretical Computer Science 124（2005）792.6基于归约的归一化基于归约的归一化函数是迭代一步归约函数直到其产生值（即，固定点）：（* normalize： term -> term*）fun normalizet=（case reducet（LIT n）=> LIT n| t’=> normalize在下面的定义中，我们内联reduce是为了直接检查分解是否产生值或分解：（* iterate0： value_or_decomposition -> term*）fun iterate0（VALt）= t|迭代0（DEC（c，r））=iterate0（decode（plug（c， contractr）（* normalize0： term -> term*）fun normalize0t=iterate0（decodet）2.7基于归约的规范化，类型化normalize0的类型不提供信息。为了更清楚地表明归一化函数产生了标准形式，即，整数，我们可以将值的类型细化为整数，并调整decompose' aux的第一个子句数据类型value_or_decomposition =VAL ofint（* was：term *）| 上下文的DEC * redex...decompose'_= VAL n|......这是什么？（* reduce： term -> term*）乐趣减少=（case decodetof（VALn））=> LIT n|（DEC（c，r））=>plug（c，contract r））然后，基于归约的归一化函数可以返回整数而不是文字：（* iterate1： value_or_decomposition -> int*）fun iterate1（VAL n）= n|迭代1（DEC（c，r））=iterate1（decode（plug（c， contractr）（* normalize1： term -> int*）fun normalize1t=iterate1（decodet）O. Danvy/Electronic Notes in Theoretical Computer Science 124（2005）7985normalize1的类型比normalize0的类型信息量更大，因为它清楚地表明将normalize1应用于一个术语会产生一个值。2.8总结和结论我们已经在ML中实现了完整的细节，算术表达式的约简语义。使用这种归约语义，我们实现了一个基于归约的归一化函数。3从基于归约的规范化到无归约规范化在本节中，我们将第2.7节的基于归约的归一化函数转换为无归约的归一化函数，即，一个没有中间项的地方。我们首先重新聚焦基于归约的规范化函数[25]以消除中间项，并且我们获得了一个然后，我们将这个预抽象机器简化为抽象机器，即，状态转换系统。这个抽象机器是去功能化的形式[24]，我们重新功能化它。结果是延续传递风格，我们用直接风格重新表达它[17]。产生的direct-style函数是算术表达式的传统求值器;特别是，它是无约简的。3.1封堵分解在第2.7节的基于归约的归一化函数中，分解总是应用于第一次分解后的插补结果。让我们给plug添加一个vacuous初始调用，这样在所有情况下，分解都应用于plug的结果：（* normalize2： term -> int*）fun normalize2t=iterate1（decode（plug（C0，t）3.2重新聚焦正如Nielsen和作者[25]之前所研究的那样，分解和插入的组合可以被分解为一个重聚焦函数，以避免构造中间项。此外，这个重聚焦函数可以非常简单地用2.4节的分解函数来表示（这就是我们选择这样精确地指定它们的原因（* refocus： context * term -> value_or_decomposition*）fun refocus（c，t）= decompose86O. Danvy/Electronic Notes in Theoretical Computer Science 124（2005）79因此，重新确定重点的评价职能如下：（* iterate3： value_or_decomposition -> int*）fun iterate3（VAL v）= v|迭代3（DEC（c，r））=iterate3（refocus（c，contract r））（* normalize3： term -> int*）fun normalize3t=iterate3（refocus（C0，t））重新聚焦的归一化函数是无约简的，因为它不再基于（一步）约简函数。相反，refocus函数直接将约简上下文和契约映射到下一个约简上下文和redex（如果有的话）。3.3从重新聚焦的规范化函数到抽象机重新聚焦的规范化函数是我们所谓的“预抽象机”[ 25 ]，因为分解和分解形成过渡函数，迭代3是“蹦床”[ 31 ]，即，另一个转换函数，它不断激活另外两个函数，直到获得一个值。让我们融合迭代3和重新聚焦（即，decompose'和decompose' aux，我们为此将其重命名为refocus4和refocus4aux），以便将迭代3直接应用于decompose'和decompose' aux的结果。结果是（尾递归）状态转换函数，即，抽象机器[40]：（* iterate4： value_or_decomposition -> int*）fun iterate4（VAL v）= v|迭代4（DEC（c，r））=refocus4（合同r，c）（* refocus4： term * context ->int*）和refocus4（LITn， c）= refocus4_aux（c， n）| refocus4（ADD（t1，t2），c）=refocus4（t1， C1（t2，c））（* refocus4_aux： context *int->int*）和refocus4_aux（C0，n）=iterate4（VALn）| refocus4_aux（C1（t2，c），n）=refocus4（t2， C2（n，c））| refocus4_aux（C2（n'，c），n）=iterate4（DEC（c， SUM（（* normalize4： term -> int*）fun normalize4t= refocus4（t， C0）这种机器的形式是显著的，因为iterate 4实现了归约语义的归约规则，而refocus 4和refocus 4aux实现了它的同余规则--这一区别通常需要对现有的抽象机器进行非平凡的分析来建立[34]。O. Danvy/Electronic Notes in Theoretical Computer Science 124（2005）79873.4内联和简化由于iterate4和contract只是教学工具，让我们将它们内联来简化抽象机器。在refocus4 aux的最后一个子句中，内联合约产生以下子句：| refocus4_aux（C2（n'，c），n）=重新聚焦4（LIT（n由于refocus4是由其第一个参数的情况定义的，因此该子句可以简化如下：| refocus4_aux（C2（n'，c），n）= refocus4_aux（c，n由此产生的简化机器是一个3.5再功能化像许多其他抽象机器一样[2，3，4，13，21]，3.4节的抽象机器是去功能化的形式[24]：约简上下文与refocus4 aux一起是函数的一阶对应物。 抽象机器的高阶对应物如下：（* refocus5： term *（int->int）->int*）fun refocus5（LIT n，c）= c n| refocus5（ADD（t1，t2），c）=重新聚焦5（t1，fn n1 => refocus5（t2，fn n2 => c（n1 + n2）（* normalize5： term -> int*）fun normalize5t= refocus5（t， fn n => n）3.6Back to直接风格第3.5节的重新功能化定义是延续传递风格的，因为它有一个函数累加器，并且它的所有调用都是尾调用[23，17]。其直接风格的对应部分如下：（* refocus6： term -> int*）fun refocus6（LIT n）= n|refocus6（ADD（t1，t2））=（refocus6 t1）+（refocus6 t2）（* normalize6： term -> int*）fun normalize6t=重新聚焦6t由此产生的定义是算术表达式的常用求值函数，即，传统的无归约归一化函数。88O. Danvy/Electronic Notes in Theoretical Computer Science 124（2005）793.7总结和结论我们已经将第2节中基于归约的归一化函数重新聚焦到抽象机器中，并且我们展示了相应的无归约归一化函数。4自由幺半群为了定义给定载体集上自由幺半群中项的归约语义，我们指定了它们的抽象语法（一个独特的单位元素，载体集的其他元素和项的乘积），它们的归约概念（定向转换规则），它们的归约上下文和相应的插入函数，以及如何将它们分解为归约上下文和最右最内的redex（如果有）。然后，我们定义了一个单步约简函数，它将非值项分解为约简上下文和redex，收缩redex，并将contractum插入上下文。我们最终可以定义一个基于归约的归一化函数，该函数重复应用一步归约函数，直到得到一个值，即，一个正常的形式，达到。4.1抽象语法给定一个elem类型的载体集元素，自由幺半群中的一个项是单位元素，elem类型的元素，或两个项的乘积数据类型term = UNIT| ELEM of elem| PROD of term * term自由幺半群中的项遵守转换规则：单位元素对于乘积是中性的（在左边和右边），乘积是结合的。4.2归约概念我们通过将转换规则定向为归约规则来引入归约的概念：PROD（UNIT，t）−→tELEMe−→ PROD（ELEMe， UNIT）PROD（PROD（t11，t12），t2）−→ PROD（t11， PROD（t12，t2））我们将赎回表示为一种数据类型，并使用相应的归约规则实现它们的收缩：数据类型redex =LEFT_UNIT of term| RIGHTMOST of elemO. Danvy/Electronic Notes in Theoretical Computer Science 124（2005）7989| （term * term）* term（*contract：redex -> term *）的ASSOC资金合同（LEFT_UNITt）= t|合同（最右e）= PROD（元素，单位）| 合约（ASSOC（（t11，t12），t2））= PROD（t11， PROD（t12，t2））最右最内的归约策略收敛并产生一个规范形式的类似列表的项。4.3约简背景我们求一个项中最右最内的Redex。归约上下文的语法和对应的插入函数如下：数据类型context = C0| 术语* 上下文的C1（* plug： context * term -> term*）fun plug（C0，t）= t| 插头（C1（t1，c），t2）=插头（c，PROD（t1，t2））4.4分解项是值（即，它不包含任何redex），或者它可以被分解为约简上下文和redex：数据类型value_or_decomposition =术语的VAL| 上下文的DEC * redex(No项被卡住了）。分解函数递归地搜索一个项中最右最内的redex。如2.4节所述，我们用两个辅助函数来定义它，decompose（*decompose=| decode '（元素e，c）= DEC（c， RIGHTMOSTe）| decode '（PROD（t1，t2），c）= decode90O. Danvy/Electronic Notes in Theoretical Computer Science 124（2005）79（*= VALt|decompose'_aux（C1（UNIT，c），t2）= DEC（c， LEFT_UNITt2）|decompose'_aux（C1（ELEM e，c），t2）=| decompose'_aux（C1（PROD（t11，t12），c），t2）= DEC（c， ASSOC（（t11，t12），t2））（* decompose： term -> value_or_decompose*）函数分解t= decompose引理4.1项t或者是一个值，或者存在一个唯一的上下文c，使得decodet的值为DEC（c，r），其中r为redex。证据立 竿 见 影 的Q4.5一步还原我们现在可以定义一个一步归约函数，它（1）将一个非值项映射到一 个 归 约 上 下 文 和 一 个 redex 中 ， （ 2 ） 收 缩 redex ， （ 3 ） 将contractum插入到归约上下文中（* reduce： term -> term*）乐趣减少=（case decodetof（VAL=> t|（DEC（c，r））=>plug（c，contract r））4.6基于归约的归一化基于归约的归一化函数是迭代单步归约函数直到产生值的函数。在下面的定义中，和2.6节一样，我们内联约简并直接检查分解是否产生值或分解：（* iterate0： value_or_decomposition -> term*）fun iterate0（VALt）= t|迭代0（DEC（c，r））=iterate0（decode（plug（c， contractr）（* normalize0： term -> term*）fun normalize0t=iterate0（decodet）4.7基于归约的规范化，类型化与第2.7节一样，normalize 0的类型不提供信息。为了更清楚地表明规范化函数产生规范形式，让我们引入规范形式中的项的数据类型O. Danvy/Electronic Notes in Theoretical Computer Science 124（2005）7991数据类型term_nf = UNIT_nf|元素的PROD_nf* term_nf然后，我们可以细化值的类型，使其更加明显， 是正常的形式：数据类型value_or_decomposition = term的VAL*term_nf| 上下文的DEC * redex然后我们必须调整decompose（*decompose=| decode '（元素e，c）= DEC（c， RIGHTMOSTe）| decode '（PROD（t1，t2），c）= decode（*decompose’_aux-> value_or_decomposition*）和= VAL（t，t_nf）|decompose'_aux（C1（UNIT，c），t2，t2_nf）= DEC（c， LEFT_UNITt2）|decompose'_aux（C1（ELEM e，c），t2，t2_nf）=|decompose'_aux（C1（PROD（t11，t12），c），t2，t2_nf）= DEC（c， ASSOC（（t11，t12），t2））（* decompose： term -> value_or_decompose*）函数分解t= decompose然后，基于归约的归一化函数可以返回标准形式的项的表示：（* iterate1： value_or_decomposition -> term_nf*）fun iterate1（VAL（t， t_nf））= t_nf|迭代1（DEC（c，r））=iterate1（decode（plug（c， contractr）（* normalize1： term -> term_nf*）fun normalize1t=iterate1（decodet）normalize1的类型比normalize0的类型信息量更大，因为它清楚地表明，将normalize1应用于一个项会生成一个范式项。4.8总结和结论我们在ML中实现了自由幺半群中术语的约简语义，给定其载体集。使用这种约简语义，我们实现了一个基于约简的归一化函数。92O. Danvy/Electronic Notes in Theoretical Computer Science 124（2005）795从基于归约的规范化到无归约规范化在本节中，我们将4.7节中基于归约的归一化函数转换为无归约的归一化函数，即，一个没有中间项的地方。我们首先重新聚焦基于归约的归一化函数，得到一个预抽象机器。然后，我们将这个前抽象机器简化为抽象机器。这个抽象的机器是去功能化的形式，我们将其重新功能化，结果是延续传递风格，我们将其重新表达为直接风格。由此产生的直接风格的函数是一个传统的带累加器的函数;特别是，它是无约简的。5.1封堵分解在第4.7节的基于归约的归一化函数中，分解总是应用于第一次分解后的插入结果。让我们给plug添加一个vacuous初始调用，这样在所有情况下，分解都应用于plug的结果：（* normalize2： term -> term_nf*）fun normalize2t=iterate1（decode（plug（C0，t）5.2重新聚焦如3.2节所示，我们现在将decomposition的组合进行森林分解，并插入到一个refocus函数中：（* refocus： context * term -> value_or_decomposition*）fun refocus（c，t）= decompose因此，重新确定重点的评价职能如下：（* iterate3： value_or_decomposition -> term_nf*）fun iterate3（VAL（t， t_nf））= t_nf|迭代3（DEC（c，r））=iterate3（refocus（c，contract r））（* normalize3： term -> term_nf*）fun normalize3t=iterate3（refocus（C0，t））重新聚焦的归一化函数是无归约的，因为它不再基于归约函数，也不再构造中间项。O. Danvy/Electronic Notes in Theoretical Computer Science 124（2005）79935.3从重新聚焦的评价函数到抽象机器再次，重新聚焦的评估函数是一个“预抽象机”，在这个意义上，分解和分解形成一个过渡函数，迭代3是一个“蹦床”。 让我们融合迭代3和重新聚焦（即， decompose '和decompose' aux，我们在3.3节中将其重命名为refocus4和refocus4aux），因此iterate3直接应用于decompose'和decompose' aux的结果。结果是下面的抽象机器：（* iterate4： value_or_decomposition -> term_nf*）fun iterate4（VAL（t， t_nf））= t_nf|迭代4（DEC（c，r））=refocus4（合同r，c）（* refocus4： term * context -> term_nf*）和refocus4（UNIT，c）= refocus4_aux（c， UNIT，UNIT_nf）| refocus4（ELEM e，c）=iterate4（DEC（c， RIGHTMOSTe））| refocus4（PROD（t1，t2），c）=refocus4（t2， C1（t1，c））（* refocus4_aux： context * term * term_nf -> term_nf*）和refocus4_aux（C0，t，t_nf）=iterate4（VAL（t，t_nf））|refocus4_aux（C1（UNIT，c），t2，t2_nf）=iterate4（DEC（c， LEFT_UNITt2））| refocus4_aux（C1（ELEMe，c），t2，t2_nf）=refocus4_aux（c， PROD（ELEMe，t2）， PROD_nf（e，t2_nf））| refocus4_aux（C1（PROD（t11，t12），c），t2，t2_nf）=iterate4（DEC（c， ASSOC（（t11，t12），t2）（* normalize4： term -> term_nf*）fun normalize4t= refocus4（t， C0）5.4内联和简化和3.4节一样，我们内联iterate4并压缩以简化抽象机器。发生三种情况(i) 该条款| refocus4（ELEM e，c）=iterate4（DEC（c， RIGHTMOSTe））在内联iterate4和contract之后，如下所示| refocus4（ELEM e，c）=refocus4（PROD（ELEMe，UNIT），c）由于refocus4是由其第一个参数的case定义的，所以这个子句可以简化如下（跳过两步）：| refocus4（ELEM e，c）= refocus4_aux（c，PROD（ELEMe， UNIT），PROD_nf（e，UNIT_nf））(ii) 该条款|refocus4_aux（C1（UNIT，c），t2，t2_nf）=iterate4（DEC（c， LEFT_UNITt2））94O. Danvy/Electronic Notes in Theoretical Computer Science 124（2005）79在内联iterate4和contract之后，如下所示|refocus4_aux（C1（UNIT，c），t2，t2_nf）=refocus4（t2，c）然而，我们t2是标准形式，因此我们可以直接调用refocus4aux：|refocus4_aux（C1（UNIT，c），t2，t2_nf）= refocus4_aux（c，t2， t2_nf）(iii) 该条款| refocus4_aux（C1（PROD（t11，t12），c），t2，t2_nf）=iterate4（DEC（c， ASSOC（（t11，t12），t2）在内联iterate4和contract之后，如下所示| refocus4_aux（C1（PROD（t11，t12），c），t2，t2_nf）=重新聚焦4（PROD（t11， PROD（t12，t2）），c）由于refocus4是由其第一个参数的case定义的，所以这个子句可以简化如下（跳过两步）：| refocus4_aux（C1（PROD（t11，t12），c），t2，t2_nf）=重新聚焦4（t2， C1（t12， C1（t11，c）然而，我们t2是标准形式，因此我们可以直接调用refocus4aux：| refocus4_aux（C1（PROD（t11，t12），c），t2，t2_nf）=refocus4_aux（C1（t12， C1（t11，c）），t2，t2_nf）在由此产生的refocus4 aux的定义中，我们观察到第二个参数是死的，即，它从未被使用过。删除它（并将最后一个参数重命名为a）会产生以下定义：（* refocus4： term * context -> term_nf*）fun refocus4（UNIT，c）= refocus4_aux（c， UNIT_nf）| refocus4（ELEM e，c）= refocus4_aux（c， PROD_nf（e， UNIT_nf））| refocus4（PROD（t1，t2），c）=refocus4（t2， C1（t1，c））（* refocus4_aux： context * term_nf -> term_nf*）和refocus4_aux（C0，a）= a| refocus4_aux（C1（UNIT，c），a）= refocus4_aux（c， a）|refocus4_aux（C1（ELEMe，c），a）= refocus4_aux（c， PROD_nf（e，a））| refocus4_aux（C1（PROD（t11，t12），c），a）=refocus4_aux（C1（t12， C1（t11，c）），a）5.5再功能化上述refocus4和refocus4 aux的定义不是去功能化的形式，因为refocus4 aux的最后一个子句[24]。为了将它们置于去功能化的形式（eureka），我们需要再引入一个辅助函数：O. Danvy/Electronic Notes in Theoretical Computer Science 124（2005）7995（* refocus4： term * context -> term_nf*）fun refocus4（UNIT，c）= refocus4_aux（c， UNIT_nf）| refocus4（ELEM e，c）= refocus4_aux（c， PROD_nf（e， UNIT_nf））| refocus4（PROD（t1，t2），c）=refocus4（t2， C1（t1，c））（* refocus4_aux： context * term_nf -> term_nf*）和refocus4_aux（C0，a）= a|refocus4_aux（C1（t'，c），a）= refocus4_aux（* refocus4_aux= refocus4_aux（c， a）| refocus4_aux'（ELEMe，c，a）= refocus4_aux（c， PROD_nf（e，a））| refocus4_aux'（PROD（t11，t12），c，a）= refocus4_aux现在，约简上下文与refocus4 aux一起是函数的一阶对分。归一化函数的高阶对应部分如下：（* refocus5： term *（term_nf -> term_nf）-> term_nf*）fun refocus5（UNIT，c）= c UNIT_nf| refocus5（ELEM e，c）= c（PROD_nf（e， UNIT_nf））| refocus5（PROD（t1，t2），c）= refocus5（t2， fn（* refocus5_aux= c a| refocus5_aux'（ELEMe，c，a）= c（PROD_nf（e，a））| refocus5_aux'（PROD（t11，t12），c，a）= refocus5_aux（* normalize5： term -> term_nf*）fun normalize5t= refocus5（t， fn a => a）5.6Back to直接风格5.5节的重新功能化定义是延续传递风格的，因为它有一个函数累加器，并且它的所有调用都是尾调用。其直接风格的对应部分如下：（* refocus6： term -> term_nf*）fun refocus6UNIT= UNIT_nf|re