关于头归约的单元成本模型的不变性（长版本）
计算机科学中的逻辑
2012-02-09 v1 编程语言
摘要
λ 演算是被广泛接受的高阶函数式程序计算模型，然而目前尚无任何直接且普遍公认的成本模型。因此，将 λ 项归约至其范式所需的计算难度通常通过对具体实现算法的推理来进行研究。在本文中，我们证明了当头归约作为底层动力学时，单元成本模型确实是不变的。这一结果改进了已知结论，后者仅涉及弱归约（按值调用或按名调用）。不变性的证明借助于一种显式替换的线性演算，该演算能够将 λ 演算中的任何头归约步骤优雅地分解为更基本的替换步骤，从而使头归约的组合结构更易于推理。该技术也是解决我们所认为的主要开放问题（即理解对于哪些规范化策略，推导复杂度是一个不变的成本模型，如果存在的话）的一个有前景的工具。
引用
@article{arxiv.1202.1641,
title = {On the Invariance of the Unitary Cost Model for Head Reduction (Long Version)},
author = {Beniamino Accattoli and Ugo Dal Lago},
journal= {arXiv preprint arXiv:1202.1641},
year = {2012}
}
备注
22 pages