一个安全全合成的显式替换理论
A Theory of Explicit Substitutions with Safe and Full Composition
摘要：
已经提出了许多不同的系统与显式替代实现了一个大类的高阶语言。本文的第一部分调查的动机和挑战，指导这种演算的功能框架的发展。然后，非常简单的技术在命名变量风格的符号是用来建立一个理论的显式替代的Alzada演算享有一整套有用的属性，如完整的组成，模拟一步β-减少，保存β-强规范化，强规范化的类型条款和汇合元术语。相关结石的规范化也进行了讨论。
英文摘要：
Many different systems with explicit substitutions have been proposed to implement a large class of higher-order languages. Motivations and challenges that guided the development of such calculi in functional frameworks are surveyed in the first part of this paper. Then, very simple technology in named variable-style notation is used to establish a theory of explicit substitutions for the lambda-calculus which enjoys a whole set of useful properties such as full composition, simulation of one-step beta-reduction, preservation of beta-strong normalisation, strong normalisation of typed terms and confluence on metaterms. Normalisation of related calculi is also discussed.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
