Reductions, intersection types, and explicit substitutions
Reductions, intersection types, and explicit substitutions
复制标题
归约、交集类型和显式替换
DOI：
10.1017/s0960129502003821
复制
发表时间：
2001
影响因子：
0.5
通讯作者：
P. Lescanne
中科院分区：
文献类型：
--
作者：
Daniel J. Dougherty;P. Lescanne
本文是从基础和应用的角度将显式替换视为主要 λ 演算的一般计划的一部分。我们研究显式替换的无组合微积分和通过添加显式垃圾收集获得的增强微积分，并探索交集类型和归约之间的关系。我们证明，通过最左归约标准化的项和通过头归约标准化的项都可以被表征为在某个系统中可输入的项。可打字性和强标准化之间的关系与经典情况略有不同：我们证明可打字术语是强标准化的，但给出了相反的反例。我们的最左和头部减少的概念是不确定的，我们的归一化定理适用于遵循这些策略的任何计算。通过这种方式，我们完善并强化了经典的归一化定理。证明需要在涉及显式替换的归约的情况下使用一些新技术。事实上，我们的证明并不依赖于经典 λ 演算的结果，在我们看来，经典 λ 演算从属于显式替换演算。
This paper is part of a general programme of treating explicit substitutions as the primary λ-calculi from the point of view of foundations as well as applications. We work in a composition-free calculus of explicit substitutions and an augmented calculus obtained by adding explicit garbage-collection, and explore the relationship between intersection-types and reduction. We show that the terms that normalise by leftmost reduction and the terms that normalise by head reduction can each be characterised as the terms typable in a certain system. The relationship between typability and strong normalisation is subtly different from the classical case: we show that typable terms are strongly normalising but give a counterexample to the converse. Our notions of leftmost and head reduction are non-deterministic, and our normalisation theorems apply to any computations obeying these strategies. In this way we refine and strengthen the classical normalisation theorems. The proofs require some new techniques in the presence of reductions involving explicit substitutions. Indeed, our proofs do not rely on results from classical λ-calculus, which in our view is subordinate to the calculus of explicit substitution.