具有安全与完全组合的显式替换理论

许多不同的显式替换系统已被提出用于实现一大类高阶语言。本文第一部分综述了在函数式框架中指导此类演算发展的动机与挑战。随后，采用命名变量风格符号的非常简单的技术，为λ演算建立了一个显式替换理论，该理论拥有一系列有用性质，如完全组合、单步β归约的模拟、β强规范化的保持、类型化项的强规范化以及元项上的合流性。还讨论了相关演算的规范化问题。