(In)E效率和合理成本模型的λ-演算时间费用模型研究

可在www.sciencedirect.com在线获取理论计算机科学电子笔记338（2018）23-43www.elsevier.com/locate/entcs(In)E效率和合理成本模型Beniamino Accattoli1InriaLIX，E'colePolytechnique摘要本文是关于λ-演算的时间费用模型的一个探索性文章。为了允许在λ演算中直接定义标准复杂性类，如P或EXP，成本模型必须是合理的，也就是说，与图灵机的多项式相关。对于λ-演算，存在一个评估策略，其步数是一个合理的成本模型，一直是一个长期的开放问题。自1995年以来，对特殊情况的回答是肯定的，但仅提供了一般情况的解决方案2014年这个问题很特殊，因为它的某些方面有些违反直觉。本文致力于解释这个基本主题的微妙之处。经常被误解的一个关键点是，效率和合理是两个不相关的属性，这一点在这里进行了详细的讨论评价战略。本文的第二个重点是标准策略和合理策略之间的关系。关键词：Lambda演算，成本模型，共享，计算复杂性，函数式编程。这项工作是一个更广泛的研究领域的一部分，COCA HOLA项目[1]。1引言这篇不寻常的论文旨在解释λ-演算的合理时间费用模型问题。合理在这里是一个技术词汇，基本上意味着多项式等价于图灵机的时间成本模型。这是一个基本的问题，对大多数计算机科学家来说很容易解释，它的解决方案在技术上要求很高。然而，在很长一段时间里，它吸引的关注令人惊讶地少。我们认为，原因在于它的某些方面是微妙的，如果不是违反直觉的话。在过去的几年里，λ演算的成本模型的研究取得了相当大的进展，从2014年开始，Accattoli和Dal Lago证明了最左最外（LO）评估策略是合理的[13]-当其步骤数提供合理的成本模型时，策略是合理的一方面，这一结果加强了关于薄弱战略的结果（其中评价1电子邮件：beniamino. inria.frhttps://doi.org/10.1016/j.entcs.2018.10.0031571-0661/© 2018作者。出版社：Elsevier B.V.这是一篇基于CC BY-NC-ND许可证的开放获取文章（http://creativecommons.org/licenses/by-nc-nd/4.0/）。24B. Accattoli/理论计算机科学电子笔记338（2018）23Blelloch和Greiner在1995年 [20]，Sands，Gustavsson和Moran在2002年[40]，以及Dal Lago和Martini在2009年[34]和[26]中结合结果的那些。另一方面，它抵消了Asperti和Mairson这一进展需要对问题有一个新的理解，这反过来又引发了一个更系统的、仍在进行的探索，澄清了各种观点。本文试图将它们总结起来，并将其呈现给一个不那么专业的观众。合理有效的策略。这篇论文背后的动机之一 事实上，这个问题通常被误解，甚至被λ演算的专家误解为关于λ项的有效评估。在λ演算中，求值是不确定的，不同的求值策略确实可能在步骤数方面非常不同。情况是微妙的：λ演算是连续的，也就是说，当它存在时，结果是唯一的，因此非决定论不是关于不同的结果，而是关于获得结果的不同方法。此外，即使结果存在，一些评估策略也可能会出现分歧，因此计算结果的方式至关重要。首先，问题在于评估策略的选择，人们会假设一个合理的策略必须是一个有效的策略。然而，直觉具有误导性：合理性和有效性是战略的不相关属性。粗略地说，效率是一种比较属性，只有当有许多策略并且一个策略旨在比较它们时，效率才有意义。相反，合理性是策略本身的一个属性，独立于任何其他策略，它可以归结为这样一个事实，即策略可以以微不足道的开销实现。合理策略的效率。然而，说合理和有效是策略的正交属性有点误导，因为它低估了研究合理成本模型的价值。事实上，对效率的研究可以显著简化合理的策略。对于一个合理的策略，可以将其步骤数作为合理的成本模型，因为粗略地说，每个步骤都可以被认为成本为1，即是一个原子操作。然后，通过简单地比较两个合理的策略在同一项上采取了多少步骤，就可以比较它们的效率当策略不被认为是合理的，相反，不清楚如何比较它们的效率，因为它们的步骤不能假设成本为1。 一个策略的效率是给定的， 它的步骤数量确实是基于隐藏的假设，是合理的。很少有评价策略被证明是合理的，至少有一个不合理的策略的例子。L'evy的最优策略的一个简单的迭代可以有一个对于不合理的策略，自然的方法是比较它们的实现在同一术语上采取了多少步骤。然而，这种进行方式具有各种缺点。首先，它在很大程度上取决于固定策略的执行，因此它几乎不是策略本身的属性其次，成本更难分析，B. Accattoli/理论计算机科学电子笔记338（2018）2325因为它取决于固定实现的许多细节。 最后， 这种方法与λ演算的机器独立性有些冲突可以有其他方式来比较不合理的策略，但远远不是合理策略所提供的简单。对于L′evy的最优策略，例如，一些作品[14，17，30，31]已经能够揭示其效率的某些方面，并且有一些例子可以提供相当大的尽管如此，在其引入近40年后，仍然不清楚在一般情况下它是否有效合理的优化。研究合理的成本模式与提高效率密切相关，还有一个更深层次的原因。证明一个策略是合理的总是需要某种形式的共享，因为实现β-约简的简单方法会增加指数开销。然而，不同的战略需要不同形式的共享和不同的优化。仔细观察表明，这些技术是独立于策略效率的一般优化原则特别是，其中一些方法最初是针对LO评估的低效情况而开发的，但它们适用于更有效的策略，如按值调用或按需调用。其中之一，称为按需替换抽象-由Accattoli和Dal Lago在[13]中引入，然后由Accattoli和Guerrieri在[12]中进行了更深入的研究-对于强策略的合理实现是必不可少的，但是据我们所知，没有基于λ演算的工具实现它。因此，没有这样的工具，例如Coq或Isabelle，依赖于合理的实现：对成本模型的研究可能因此影响实现理论，提供给定策略的更有效的实现。标准和合理的策略。本文的另一个目的是解释λ演算的标准化定理和合理成本模型之间令人惊讶的联系。Accattoli和Dal Lago在[13]中指出了这种联系，实际上这种联系源于他们结果的开始。粗略地说，根据目前对问题的理解，合理的策略必须是标准的。这一事实可以从两个方面解读一方面，它提供了一个坚实的理论证明，把LO策略（标准策略）作为一种规范的合理策略。另一方面，它揭示了标准化定理意想不到的复杂性理论内容。这样的定理是Curry和Feis在1958年引入的重写工具，用于研究λ-演算[23]，但它的范围已经扩展并推广到许多其他重写系统。相关工作。关于这个主题的调查似乎是不平衡的，因为大多数被引用的关于成本模型的论文都来自作者和他的合著者。是然而，事实上，这个话题一直被λ-演算社区所忽视。Frandsen和Sturtivant[28]在 1991年的一篇论文中讨论了合理成本模型，但其内容现在已经过时。Lawall和Mairson对于一阶重写，Dal Lago和Martini，以及独立的Avanzini和Moser，通过图重写证明了一些相当普遍的结果[34，16]，这本身就是一种共享形式。其他参考资料在本文件其余部分酌情提供26B. Accattoli/理论计算机科学电子笔记338（2018）232引入合理的成本模型图灵机是复杂性的标准模型，因为它们的成本模型是不言而喻的：时间：转换次数;空间：执行期间使用的磁带的最大单元数。为了研究不同模型X的复杂性，首先必须确定X的成本模型。成本模型的基本要求是合理的：应该在时间上的多项式有界开销和空间上的常数因子开销内对图灵机（或另一个合理模型）进行双向模拟，如Slot和van Emde Boas所述[42]。例如，随机存取机（RAM）是合理的。这个概念的重要性依赖于这样一个事实，即对于合理的系统，定义在X上的多项式时间问题的类与定义在图灵机（TM，从现在开始）上的多项式时间问题的类一致：类P然后变得鲁棒，即与模型无关。对于其他（超）多项式类（如EXP或PSPACE）也是如此。更一般地说，（不）有效可计算于是成为一个类似于（不）有效可计算的概念，并且，毫不奇怪，它有自己的论题，或者被称为强的、扩展的、有效的、现代的或复杂性理论的丘奇（-图灵）论题，或者也被称为不变性论题：所有模型都是合理的。这是自然想知道是否该论文可以加强甚至更多，要求，例如，所有的模型是相关的线性开销的时间。事实证明，这样的要求太强了，因为模型之间的模拟通常需要非线性开销，例如TM模拟具有二次开销的RAM，需要模拟顺序磁带上的随机访问。不同地说，子多项式类不是鲁棒的，这是类P如此相关的原因之一。这里我们感兴趣的模型是λ演算。自计算机科学诞生以来，图灵机被认为比λ演算更有效，因为λ演算的成本模型并不明显。更准确地说，有自然成本模型：时间：β-归约的次数，λ-演算的计算步骤，以及空间：由这些步骤产生的最大λ-项的大小然而，这种天真的观点有两个问题：(i) 策略：λ演算只是半确定性的：如果有结果的话，结果是唯一的，但是可以有许多方法来获得它，并且即使结果存在，一些策略也可能不会终止。哪种战略应被视为提供合理的成本模式？有没有一种策略可以提供一个规范的成本模型，不管这意味着什么？(ii) β的原子性：β-约化看起来不像原子操作，因为它B. Accattoli/理论计算机科学电子笔记338（2018）2327可能以指数速率增加λ项的大小-这是一种称为大小爆炸的现象。严重的问题涉及规模爆炸，这表明自然成本模型是不合理的。然而，通过一个有共享的精化λ演算的迂回，可以证明β步数是λ演算（没有共享）的合理成本模型。准确地说，我们应该确定λ演算的一个特定方言和一个求值策略，然后证明，在某种程度上，固定策略的β步骤可以被认为是原子的。文献中最强的结果是最左最外（LO）求值是（强）λ演算的合理策略[13]。一旦理解了如何规避规模爆炸，战略问题就变得更加相关，这在某种程度上是本文的主题。我们在这里讨论了两个方面，似乎是合理的策略的关键特征，即终止和子项属性，并在这个意义上，LO策略是规范的。成本模型的研究实际上由两个子问题组成，这两个子问题将在接下来的两节中详细讨论，即发现：(i) 合理模型（通常是TM）在λ演算中的合理编码(ii) λ演算在合理模型（通常是RAM）中的合理编码让我们指出，我们将只考虑单一成本模型，成本模型根据某种策略对β步进行计数，并简单地对每一步计数1。 这是成本模型最自然的思维方式为λ-演算，并提供了简单的工具来工作，复杂性分析。Dal Lago和Martini在[ 25 ]中考虑了非酉合理成本模型（即，步骤的成本是redex的大小与reduce的大小之间的差异），或者Lawall和Mairson [35]建议（基于L'evy的标签的大小）。虽然空间在我们理解这个问题中起着关键作用，但我们没有解决λ演算的合理空间成本模型正如我们将要解释的那样，共享是处理合理成本模型的关键工具。然而，它不是空间的正确工具：每个β步骤（即每个时间单位）都需要一个共享注释，这意味着在这样的评估模式中，空间在时间量上总是线性的，这是最糟糕的可能空间行为，复杂性。正如Schöopp[41]首先指出的，交互作用的几何学提供了一种替代的交互评估机制，该机制在空间方面更加节俭，并且可以提供合理的空间成本模型-然而，该问题是开放的。3从图灵机到λ-演算大多数关于λ-演算的课程都展示了如何将部分递归函数表示成λ-演算-例如参见Barendregt [19]或Krivine[33]的经典书籍。TM的表示可以追溯到图灵1936年论文的附录然而，在当代文学中，这种表现很难找到，但它本身并不困难。这也不难证明，TM可以合理地28B. Accattoli/理论计算机科学电子笔记338（2018）23›Ms →在λ演算中模拟原因很简单：TM是一阶系统，而λ-演算是高阶系统，因此期望高阶系统可以合理地模拟一阶系统乍一看，这个方向似乎并不特别令人兴奋。然而，这是问题的第一个违反直觉的方面。正是因为高阶世界比一阶世界大得多，在λ演算的一个非常简单的片段中，我们喜欢称之为确定性λ演算Λ det。让我们介绍一下。确定性λ演算。Λdet的术语语言是λ-演算，定义为：特尔姆斯t，s，u，r：：= v|tvV值v，vJ，vJJ ：：= λx.t|X请注意，应用程序的右子项必须是一个值，这与普通λ-演算中发生的情况相反在Λdet中的求值也严格地比在普通λ-演算中的求值 评价环境薄弱，即： 它们不进入抽象内部（元级替换记为t{x}）：顶级上下文关闭时的WEAK评估上下文规则E：：=·|Ev（λx.t）s<$→βt{x s} E<$t<$$> →detE<$s <$ift<$→βs确定性λ-演算本质上是连续传递式（CPS）演算（其中参数只能是值）和弱演算的交集作为CPS，按名称调用和按值调用是一致的，因为所有参数都是值。然而，CPS结石通常依赖于强评估，而在这里我们采用弱评估。CPS和弱限制的组合提供了以下决定性性质（通过对项的结构的简单归纳证明），这证明了微积分的名称引理3.1（决定论）设t∈ Λ det. 至多有一个s∈ Λ det使得t →βs，在这种情况下，t是一个应用。在Accattoli和Dal Lago的[ 10 ]中这种编码并没有受到太多的关注，它被限制在与[10]相关的技术报告中，但实际上它有一个非常有趣的结果。这就是为什么我们重新设计它，使其在注释中更广泛地面向受众[24]。该说明的主要结果如下。定理3.2（线性模拟，[24]）设f是一个字母表，f：f→ f由图灵机M在时间g计算的函数。还有一种编码·在到Λdet中，对于每个s∈ππ，ndet （1）当n = 0时，n = 0（|S|）+的|S|）的。现在让弱战略。从本质上讲，λ - 演 算 的 所有弱策略都 崩溃了，B. Accattoli/理论计算机科学电子笔记338（2018）2329β当限制到确定性λ演算时：项至多有一个弱redex，因此所有弱策略一致。那么所有的弱策略都提供了TM的合理模拟，并且只要（无限制λ演算的）弱策略可以在合理的模型上合理地模拟，那么它就是合理的，与它的效率。现在让我们回到λ演算的半决定论。 差异 策略之间的效率可能是这样的，在给定的条件下，一个策略正态化，而另一个策略发散。尽管它令人绝望的不精确性，但如果发散策略可以在多项式开销内实现，那么它是合理的。这确实是可能的：（弱）按值调用是一个合理的策略，但当（弱）按名称调用终止时，它可能会出现分歧。通常，以下项（λx.y）（（λz.zz）（λz.zz））在按名称调用中在一个步骤中归一化，但在按值调用中发散（注意，它不属于Λ det）。因此，合理的弱势策略-gies不需要终止，这是一个非常违反直觉的事实。强有力的战略。对于强策略，这个问题比较微妙。定理3.2的编码为每个强策略提供了TM的线性模拟，在任何强策略之前减少弱赎回或弱头赎回前者的一个例子是强按值调用，它通常通过在抽象下迭代弱按值调用来获得后者之一是最左最外求值。然而，对于强策略，关于终止的行为并不像弱策略那样无关紧要。关键是编码依赖于定点运算符。在各种可能的求值中，不动点算子总是有一些发散求值。在定理3.2中，发散是避免的，因为所使用的定点只有在使用特定的强求值时才发散，但只要求值是弱的，一切都正常。存在永久的强策略，即尽可能发散的策略，例如最大策略，它总是选择发散路径。这些策略会在每个TM的编码上发散，至少在[24]的编码方面，因此它们不允许模拟它们。目前尚不清楚什么是强策略的确切终止要求，也不清楚是否有一个更好的TM编码，在强的情况下也是终止无关的。然而，就目前所知，合理的强策略似乎不可能是永久的。我们将在第二节中回到这一点7、讨论标准化定理时4从λ-演算到图灵机将λ演算编码到TM中是证明λ演算是合理的困难部分，因为它需要将高阶世界编码到一阶世界。给定λ演算中的导数t0→ns，我们希望在TM上以时间多项式模拟它，其中有以下两个关键参数：(i) 输入的大小：大小|的t0|初始项，即t 0中的构造函数的数量。(ii) 求值长度：β步数n。30B. Accattoli/理论计算机科学电子笔记338（2018）23det关键是存在项的大小爆炸族，即项的大小在n中是线性的，在n个β-步骤中求值，并且其结果在n中具有大小指数。乍一看，所需的模拟似乎是不可能的，因为简单地写下结果需要n的时间指数（并且|的t0|，其本身在n中是线性的）。出路是切换到λ-演算的一些改进与共享，其中评估产生普通范式的紧凑，共享表示，避免大小爆炸。我们现在要剖析这些奇妙的微妙之处。首先，不幸的是，规模爆炸影响了λ演算的每一个策略。这可以通过证明确定性λ演算已经支持了尺寸爆炸来优雅地证明。由于所有的弱策略都在Λdet上崩溃，它们都受到规模爆炸的影响。让我们展示它。第一个微妙之处：决定性的，或与策略无关的规模爆炸。 考虑下面的尺寸爆炸族（该族是通过将tn应用于恒等式I=u0而获得的），取自[2]：t1：= λx.λy. （yxx）t n+1：= λx. （t n（λy.（yxx）u0：= Iun+1：= λy. （余若英）命题4.1（确定性大小爆炸，[2]）设n> 0。 那么t n I →n联合国 此外，委员会认为，|t n I|时间复杂度O（n）|u n| = Ω（2 n），t n I是闭的，u n是正规的。这个例子还表明，Λdet不应该被认为是一阶设置，因为，尽管它看起来很简单，但它已经受到了尺寸爆炸的影响，这是高阶结石的典型疾病确定性λ演算到强求值的扩展不再是确定性的。然而，给定的确定性大小爆炸族，即使在强评估方面，本质上也是从技术上讲，t n I有n个平行的强β-赎回，所以它看起来不是确定的，但这些赎回是独立的：赎回不能复制或擦除彼此（钻石性质适用于t n I），也没有任何赎回的创建，因此所有对范式的评估（包括L′evy最优形式）都需要n个步骤，就像weak的情况一样。因此，也强和平行的战略，从而简单地所有的战略，supranier的大小爆炸.第二个微妙之处：关于空间的隐藏假设。规模爆炸似乎意味着β步骤的数量不可能是一个合理的时间成本模型：步骤的数量甚至没有考虑到写下结果的时间，这是显着更大。虽然这是理解规模爆炸的自然方式，但这也是错误的结论。事实上，β步数是一个合理的成本模型，这意味着自然阅读中隐藏着一个错误的假设。让我们暂且不谈如何避免规模爆炸，让我们把重点放在这样一个错误的假设上。本质上，我们假设λ演算中的空间是由计算期间的最大项大小给出的，并且由于在序列模型中时间大于或等于空间（因为需要一个单位时间来使用一个单位空间），B. Accattoli/理论计算机科学电子笔记338（2018）2331→→→→→→→→→›→›››nn›爆炸 通常，定义t0：=x0和tn+1：=tn[xn<$xn+1xn+1]。那么tn有爆炸家族的规模至少是指数级的。错误的假设是，空间是评估期间项的最大大小。目前还不清楚在λ演算中是什么解释了空间，但是对时间成本模型的研究清楚地表明，空间不是项的大小第三个微妙之处：规避规模爆炸需要基于策略的子项共享。λ-演算的所有方言都源于规模爆炸，它们通常可以通过转换到分解β-约简的形式主义来治愈在微步中，并使用某种形式的子项共享来模拟。微步形式体系可以是具有显式替换的λ演算、抽象机器或某种图重写机制。虽然细节当然很重要，但这些方法基本上都是等效的。我们在这里给出一个草图的显式替代方法。其基本思想是，在β-赎回（λx.t）s→βt{x s}的定义中使用的元级替换t{x s}被延迟，并引入了对它的注释，记为t[x s]，称为显式替换。因此，语言由下式给出（注意，这里我们是在一般λ-演算中，因此应用程序有项作为右子项）：具有共享t，s，u，r：：= x的条件|λx.t |ts |t [x s]显式替换是解释共享的构造，并且在更可读但不太紧凑的形式letx=sint下可能更熟悉。这个想法是，人们可以展开它们，获得非共享的底层项。展开操作定义如下：展开x：=x（λx.t）：=λx.t（t s）：=t s（t[x›s]）：=t{x›s}很容易看出，展开可以放大引入指数的项，大小在n中是线性的，一个简单的归纳表明，指数的;指数的= x... X有大小` 2n X微步评估的定义取决于所研究的策略-这里我们试图给出一个策略不可知的草图。一般来说，有一个评估上下文E的概念（其精确定义取决于策略），它包含显式替换和单个微步替换规则：多步取代E→subE如果E包含[x t]用t的新副本替换求值位置中的x的单次出现（而不是如β归约中的x的每次出现）。从本质上讲，共享是一次展开一个变量，并且只有在需要继续评估时才展开。现在让我们回到规模爆炸问题。大小爆炸是元级替换的固有问题，并且归结为每个β约简可能重复先前步骤数量中的大小指数的参数的事实。Cir-32B. Accattoli/理论计算机科学电子笔记338（2018）23（λ y. （yxx））[x <$λ y. （yxx）]。 . . [x]λ y。（yxx）][x›I]（1）通过微步系统X来防止它通常需要以下几点：(i) 合理的单步和子项性质：X中的单个微步在适当的意义上可以被认为是原子的，也就是说，它们的成本不会爆炸。在我们所知道的所有微步系统中，这是基本子项性质的必然结果：每个微步重复只涉及初始项的子项。根据我们的草图，由rule →sub复制的项t都是初始项的子项。注意，确定性大小爆炸意味着λ演算的任何策略都不具有子项性质（因为至少有一个步骤复制了一个子项，该子项的大小与初始项的大小呈指数关系第一千一百零八章未来宗门。第7章更深入地讨论了子项属性(ii) 合理的模拟：模拟X中的β只需要多项式数量的步骤-在我们的草图中，这转化为这样一个事实，即只需要多项式数量的→子步骤来模拟λ演算的固定策略。与子项性质一起，我们得到微步求值在β步数的大小多项式的共享结果上结束，这是λ演算中结果的紧凑表示。这一点可能很棘手：有时（在强大而开放的方言中，将很快讨论）单个步骤是合理的，但模拟似乎需要指数数量的步骤-然后需要细化→子规则(iii) 合理的表示：紧凑的表示（即共享项）可以在合理的（即多项式）时间内进行管理（通常比较相等性），而不必展开共享（这将重新引入指数爆破）。这个事实是独立的策略，它只需要被证明一次（作为显式替换或let表达式共享）-它已经在Accattoli和Dal Lago的[ 10 ]中完成这个模式被所有已知的证明策略是合理的。然而，证明其关键属性，即子项属性和合理的模拟，可能需要非常不同的技术。让我们总结一下文献中的结果：(i) 封闭方言：对于具有封闭项的弱λ-演算-建模函数编程语言-标准实现技术，如基于环境的抽象机器，在RAM上提供合理的模拟从道德上讲，命题4.1的策略独立大小爆炸族tn I评估为`n−1x展开为指数级更大的结果，但其大小明显与n成线性关系。关键是在λy中。（yxx）x的两次出现是抽象的，但是评估是弱的，因此它在到达它们之前停止-避免了重复并且避免了大小爆炸弱策略的第一个结果是Blelloch和Greiner在1995年提出的B. Accattoli/理论计算机科学电子笔记338（2018）2333[20]并涉及弱按值调用评估。Sands、Gustavsson和Moran在2002年[40]独立地证明了类似的结果，他们也解决了按名称呼叫和按需要呼叫的问题，并在2009年[27]和[26]中结合了Dal Lago和Martini的结果，他们也解决了按名称呼叫的问题[34]。头部（按名称调用）评估（既不弱也不封闭）在[10]中使用基本相同的技术被证明是合理的，但在Accattoli和Kesner的线性替代演算（LSC）[ 7 ]中被重新铸造Accattoli、Barenbaum、Mazza和Sacerdoti Coen在[5，8]中通过LSC进一步剖析和改进了关于弱策略的已知结果。封闭演算的朴素实现（如Krivine抽象机）的开销在β步数上是二次的，在大小上是线性的。第一个学期。通过简单的优化和对数据结构的仔细选择，可以将开销降低到β步数的线性和初始项大小的对数-参见Accattoli和Barras(ii) 强方言：对于强策略-在证明辅助引擎中工作-需要更多的努力和照顾，因为-正如我们之前暗示的那样-普通的抽象机器（如Cregut 关键是微步评估不再停留在抽象上，因此重复的数量爆炸式增长。第二个层次的分享细化→子，称为有用的分享，并在Sect中概述。5、获得合理的微步模拟是必要的第一个这样的语义是由Accattoli和Dal Lago在2014年引入的（并于2016年发表在期刊上[13]），用于LO策略，依靠LSC。然后Accattoli在[3]中利用一个复杂的抽象机给出了一个新的证明。强情况下的开销比弱情况下的开销具有更高的复杂度。它在初始项的大小上是线性的，而不是抽象的，因为即使简单地识别一个项是正常的，也需要遍历整个项，因此不能在对数时间内完成（在封闭的情况下，它是一个常数时间操作-只需检查第一个构造器是否是抽象）。在文献中提供的情况下，对β步数的依赖性是二次的。Accattoli和Sacerdoti Coen [8]已经详细研究了如何从β步骤中获得线性依赖性，并且该技术似乎可以顺利扩展到强评估-仅为了简单起见，文献中的案例中(iii) 开放方言：通过尝试更好地理解强求值的结果，结果发现在封闭和强演算之间存在一个中间设置，即具有开放项的弱求值[29，9，11，12]。关键点在于，可以将强求值描述为开放情况抽象下的迭代有趣的是，对于成本模型的研究，开放方言严格来说比封闭方言更难实现，严格来说比强方言更简单，从这个意义上说，34B. Accattoli/理论计算机科学电子笔记338（2018）23RLW→它们需要在封闭情况下的超连续优化，并且它们不需要在强情况下所需的优化。我们将在节中暗示这些优化五、开放式机箱的关键特征是一种尺寸爆炸的形式，这在封闭式设置中是不可能的。最简单的方法来证明它是关于从右到左的弱求值的，这里注意到→rlw。定义：t0：=y tn+1：=（λx.xx）tn s0：=y sn+1：=sn sn注意，由于第一项t0=y，族{tn}n∈N是开的。然后又道：命题4.2（开尺寸爆炸，[9]）设n ∈ N。 然后t n→ns n，此外|t n|时间复杂度O（n）|S n| = Ω（2 n），并且s n是正规的，不是抽象的。开放案例与按值调用评估相关，其中Plotkin对于封闭案例的操作语义是不够的。在[29]中，Gr′egoire和Leroy首先给出了opencall-by-alue的实现，但没有进行必要的优化以使其合理。Accattoli和Sacerdoti Coen在[9]中提供了第一个这样的实现，通过从按名称调用的情况中调整有用的共享，并在β步骤的数量和初始项的大小Accattoli和Guer-rieri在[9]中进一步简化了机器，并且还证明了开情形比强情形严格简单。最后，在[11]中，Accattoli和Guerrieri表明不同的开放按值调用演算共享相同的成本模型。公开点名和公开按需点名在文献中从未被讨论过。第四个微妙之处：新的强范式。避免规模爆炸需要共享子项和规范形式的紧凑表示强情形的困难换句话说，在不改变范式概念的情况下增加共享（即转向微步求值）仍然会计算完整范式，而不是它的紧凑表示。不可避免的解决方案由Accattoli和Dal Lago的有用共享提供形式t是正常的，可以有效地计算和操纵。通过柯里-霍华德同构，用逻辑术语可以更好地理解这个结果的微妙之处。从逻辑上讲，这意味着规范化不需要计算无割证明，而只需要计算展开为无割证明的证明线性逻辑提供了一个更精确的理解，因为它提供了一个逻辑解释，说明展开一个证明意味着什么共享和替换过程确实由线性逻辑的指数片段来处理。微妙之处可以重新表述如下：证明与指数削减其指数发展是削减自由（和潜在的指数更大）可以接受为正常（和计算B. Accattoli/理论计算机科学电子笔记338（2018）2335›并进行了有效的比较）。从本质上讲，Accattoli和Dal Lago的结果已经提出并收到了关于成本模型的结果。然而，它是基于一种关于什么是范式的新观点，而这种观点的变化大多没有被注意到。第五个微妙之处：不合理的实现无助于合理的实现。规模爆炸会影响每一个策略，因此它不依赖于策略的效率。因此，提供一个合理的实现也是不平凡的不明智的战略。最大策略给出了一个退化但有趣的案例研究。 它是一个永久的策略，也就是说，只要有可能，它就会发散，而且当它终止时，它需要最大数量的步骤才能达到标准形式。因此，它是一个非常不明智的策略，根据第三节的结尾，它似乎不是一个合理的策略，因为它不允许模拟TM。尽管如此，它仍然允许合理的实现，如注释[4]所示。这种实现方式需要与LO策略（已知合理实现方式的唯一其他强策略）完全相同的技术（即有用共享），尽管该策略效率较低，甚至没有提供合理的成本模型。5有用分享一瞥在这里，我们试图解释如何以及为什么有用的共享技术，用于[13，3]中的LO策略，用于[9]中的开放式按值调用和[4]中的最大策略，诱导合理的实现。实现总是将β步分解为微步。特别地，它们分解了替换过程：通过使用共享/显式替换来延迟替换，并且变量出现一次替换一个，仅当它们进入求值位置时。为了合理起见，应该避免对β-赎回没有贡献的微替换步骤，即应该避免无用的变量替换，只执行有用的变量替换。有用和无用的替代品。根据第4节中给出的草图，设Ex是求值上下文E中的变量出现x，它具有x的显式替换[x t]，并考虑用t替换x。什么时候对β-Redexes有用？两个案例：(i) redex的副本：如果t包含β-redex，则复制t，并将其放在E t中的求值位置（忘记在替换它之前最好减少t，这是一个不必要的优化(ii) 创建一个redex：可能t是正常的，但是它的替换在E t中创建了一个新的redex。确切地说，当t = λy.s且E是可应用的，即E = F·u，所以替换产生了redexEt= F（λy.s）u。双重地，替换是无用的，(i) 中性：t是正常的，它不是一个抽象-我们说t是中性的。在36B. Accattoli/理论计算机科学电子笔记338（2018）23这种情况下，复制t是没有用的，因为不能复制也不能创建兑换;(ii) 非应用上下文中的正常抽象：替换项是一个抽象，因此原则上它可以创建一个redex，但上下文不提供参数，因此替换不会创建任何redex有用的分享是避免无用的替换。请注意，这是一个微步概念：用t替换x的元级替换可能对x的某些出现有用，而对其他出现无用。有用的共享和封闭的方言。封闭设置（弱评估加上封闭项）不需要有用的共享，因为其中的替换总是有用的，这要归功于严格的限制。有用的共享和开放的方言。在开放设置（弱但有开放术语）中，合理的实现必须避免替换中性术语（即第一类无用术语），但可以在任何时候替换抽象。注意，在开尺寸爆炸族（命题4.2）中，爆炸是由中性项的重复给出的。有用的分享和强大的方言。强评估的合理实现还必须避免第二类无用的替换，在[12]中有时称为按需替换抽象的优化。实际上，请注意，在第10页（1）中的抽象中，避免对x进行替换的关键限制是x的那些出现不被应用。为了获得强策略的合理实现，这样的优化是必要的，但是我们所知道的强策略的实现（通常在证明助手中）没有实现它。因此，合理成本模型的理论研究在高阶工具的实现上有具体的失败。[12]参见Accattoli和Sacerdoti Coen实际上，有用的分享更棘手。在这个有用的分享的介绍中，我们忽略了一个关键的技术成分。在微步设置中，替换被延迟，不容易理解变量是被正常项还是被中性项替换，这是实现有用共享的两种情况所需的原因在于，用于替换x的项t可能会被分解成小块，分散在环境中的许多延迟替换中，并且t中的redex只有当这些块放在一起时才能看到。这就是为什么实现有用共享的抽象机器经常在环境条目上使用标签来跟踪，当以后将片段放在一起时，条目是否会有一个redex，将是一个抽象，或者将是中性的。这是在[9，3，4]中遵循的方法。6效率和合理成本模型最优序贯评价。众所周知，λ演算的最优一步求值策略这里还有另一个微妙的问题：先验的，非递归的并不意味着B. Accattoli/理论计算机科学电子笔记338（2018）2337这是不合理的，因为可能存在用于评估的递归次优算法，该算法在最优策略的步骤中是多项式的并且不模拟策略本身-然而，这样的算法的存在是不可能的。更一般地说，注意成本模型是一个度量，而不是一个计算问题-知道问题不是递归的并不意味着与之相关的度量是不合理的。让我们也指出，[19]中关于最优策略不是递归的证明并没有提供如何证明它是不合理的提示，这是一个开放的问题。最佳的绩效评估。 另一方面，L′evy的最优p a r a l e l evalation [ 36 ]是可判定的，即使它需要的步骤数小于或等于最优一步策略。1998年，Liechti和Mairson [15]指出L'evy的最优估计是不合理的，这也是唯一已知的合理策略的可验证结果。关键在于，L'evy的概念在其定义的巧妙性中隐藏了其实现的复杂性它共享了太多，将太多步骤的复杂性压缩为一个步骤，使最佳步骤的数量成为一个不可靠的度量。让我们再次强调，最优策略不合理的事实并不意味着它是不合理的，也不意味着它的实施是不合理的。简单地说，最佳步骤的数量是一个不可靠的度量，但如果相对于合理的成本模型（例如到范式的LO步骤的数量）进行测量，则然而，这个问题是开放的。正如在引言中指出的，困难在于，由于并行优化策略是不合理的，人们不能依赖于计算步骤的λ演算，但它必须仔细研究系统实现它，这是比普通的λ演算涉及更多相对于普通的求值技术，有一些变体的线性逻辑引入了具有有限复杂性（初等的，多项式的）的λ -演算的片段。 这些片段有助于更好地理解L'evy的最优性，因为它们的最优实现要简单得多（不需要所谓的oracl e）。在[14]中，Asperti，Coppola，andMartini证明了L'evy的最优策略在基本片段中也是不合理的巴约、科波拉和达拉戈[17]以及Guerrini和Soleri在[31]中表明，另一方面，通过L'evy的最优方法在预期的碎片复杂性中评估这些碎片，证明不合理并不意味着共享子项和共享计算。让我们在一个高的水平上比较阿卡蒂和迈尔森的结果与阿卡托利和达拉戈的结果。 LO战略是一种最大非共享的标准化策略，其中尽可能地复制赎回，并且不需要的赎回永远不会减少，关于最佳推导，这是双重的。LO策略的合理实施采用有用共享，但重要的是不要混淆两个不同的共享水平：有用共享共享子项，但不计算，而L'evy的最佳正是因为有用共享不共享计算，所以它具有子项性质，这是证明这是合理的。在[13]中，子项性质被证明与线性替换演算的标准化定理38B. Accattoli/理论计算机科学电子笔记338（2018）23和概念的指数框在线性逻辑，也见即将举行的节。第七章合理分摊计算费用。子项的共享和计算的共享并不是不相容的，如果我们不走到Levy的最优评价的程度的话。在弱域中，按值调用和按需要调用策略与按名称调用（这是LO求值的弱类比）相比，确实可以被视为共享计算的策略。例如，在命题4.2的开放大小爆炸家族中，按值调用和按需求调用比按名称调用采取的步骤要少。按值调用和按需要调用都有子项属性，允许共享子项。此外，它们的微步实现是非常有效的，具有在β步的数量上是线性的因此，我们确实知道既合理又有效的策略。正如在第4节中已经讨论过的，开放式按值调用也有一些有效的实现。类似的技术也可以处理开放的按需调用，但这个案例研究尚未发表。如何证明强的按值调用和按需调用也是合理的是一个活跃的研究课题。处理强按值调用的工具基本上是在[9，12]中开发的，我们希望它们也能适应强按需调用，其操作语义正在以