简化的挂起演算及其与其他显式替换演算的关系

本文关注 lambda 演算中替换的显式处理。其贡献之一是对体现这种处理的挂起演算进行了简化与合理化。早期版本的该演算对替换组合提供了一种繁琐的编码，这种操作对于归约的高效实现很重要。本文简化了这种编码，产生了一种易于在应用中直接使用的处理方式。合理化在于消除了在替换解耦中一种实际影响微小的灵活性，该灵活性具有丢失项中上下文信息的无意副作用；修改后的演算现在具有一种自然支持逻辑分析的结构，例如与 lambda 项的类型赋值相关的分析。结果表明，整个演算具有令人满意的理论性质，例如用于替换的强终止子演算，以及即使在存在被赋予嫁接解释的项元变量的情况下也具有合流性。本文的另一项贡献是确定了一组广泛的属性，这些属性是显式替换演算应予以支持的，并基于这些属性对各种已提出的系统进行了分类。挂起演算被用作本研究的工具。具体而言，描述了它与其他演算之间的映射，以理解后者的特性。