一种简化的悬置演算及其与其它显式代换演算的关系
A Simplified Suspension Calculus and its Relationship to Other Explicit Substitution Calculi
摘要：
本文讨论了λ演算中代换的显式处理。它的贡献之一是简化和合理化的暂停演算，体现了这样的待遇。这个演算的早期版本提供了一个繁琐的替换组合编码，这是一个对有效实现约简很重要的操作。这里简化了这种编码，从而产生了易于在应用程序中直接使用的处理。合理化包括消除在解开替换时实际上无关紧要的灵活性，这种灵活性具有丢失术语中上下文信息的无意副作用;修改后的演算现在具有自然支持逻辑分析的结构，例如与类型分配有关的结构，在lambda术语上。整体演算具有令人满意的理论性质，如强终止子演算的替代和汇合，即使在存在长期Meta变量，符合嫁接解释。本文的另一个贡献是确定了一系列广泛的属性，这些属性是显式替换演算所需的，并基于这些属性对各种拟议系统进行分类。悬浮演算是作为一种工具，在这项研究中。特别是，映射之间的描述，它和其他结石对理解后者的特点。
英文摘要：
This paper concerns the explicit treatment of substitutions in the lambda calculus. One of its contributions is the simplification and rationalization of the suspension calculus that embodies such a treatment. The earlier version of this calculus provides a cumbersome encoding of substitution composition, an operation that is important to the efficient realization of reduction. This encoding is simplified here, resulting in a treatment that is easy to use directly in applications. The rationalization consists of the elimination of a practically inconsequential flexibility in the unravelling of substitutions that has the inadvertent side effect of losing contextual information in terms; the modified calculus now has a structure that naturally supports logical analyses, such as ones related to the assignment of types, over lambda terms. The overall calculus is shown to have pleasing theoretical properties such as a strongly terminating sub-calculus for substitution and confluence even in the presence of term meta variables that are accorded a grafting interpretation. Another contribution of the paper is the identification of a broad set of properties that are desirable for explicit substitution calculi to support and a classification of a variety of proposed systems based on these. The suspension calculus is used as a tool in this study. In particular, mappings are described between it and the other calculi towards understanding the characteristics of the latter.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
