关于水头削减一元费用模型的不变性（长版）
On the Invariance of the Unitary Cost Model for Head Reduction (Long Version)
摘要：
λ演算是一种被广泛接受的高阶函数程序的计算模型，但目前还没有一个直接的、普遍接受的代价模型，因此，将lambda项约简为其范式的计算难度通常是通过对具体实现算法的推理来研究的。在本文中，我们表明，当头部减少的基本动力学，单位成本模型确实是不变的。这改进了已知的结果，这些结果只处理弱（按值调用或按名称调用）约简。不变性是通过显式替换的线性演算来证明的，这允许很好地将λ演算中的任何头部减少步骤分解为更基本的替换步骤，从而使头部减少的组合学更容易推理。该技术也是一个很有前途的工具来攻击我们所看到的主要开放问题，即理解哪些规范化策略推导复杂性是不变成本模型（如果有的话）。
英文摘要：
The lambda calculus is a widely accepted computational model of higher-order functional pro- grams, yet there is not any direct and universally accepted cost model for it. As a consequence, the computational difficulty of reducing lambda terms to their normal form is typically studied by reasoning on concrete implementation algorithms. In this paper, we show that when head reduction is the underlying dynamics, the unitary cost model is indeed invariant. This improves on known results, which only deal with weak (call-by-value or call-by-name) reduction. Invariance is proved by way of a linear calculus of explicit substitutions, which allows to nicely decompose any head reduction step in the lambda calculus into more elementary substitution steps, thus making the combinatorics of head-reduction easier to reason about. The technique is also a promising tool to attack what we see as the main open problem, namely understanding for which normalizing strategies derivation complexity is an invariant cost model, if any.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
