A typed context calculus
A typed context calculus
复制标题
类型化上下文演算
DOI：
10.1016/s0304-3975(00)00174-2
复制
发表时间：
2001
期刊：
影响因子：
--
通讯作者：
A. Ohori
中科院分区：
文献类型：
--
作者：
M. Hashimoto;A. Ohori
本文开发了一种上下文类型演算，即带“洞”的lambda项。除了普通的lambda项外，微积分还包含标记的孔、孔抽象和用于操作第一级上下文的上下文应用程序。上下文的主要操作是填充空穴，它捕获自由变量。这个操作与lambda演算的替换相冲突，两者的直接混合会导致不一致的系统。我们通过定义一个类型系统来解决这个问题，该类型系统精确地指定上下文的变量捕获特性，并跟踪绑定变量的重命名。这些机制使我们能够定义一个还原系统，适当地整合β还原和孔填充。所得到的演算是Church-Rosser的，类型系统具有主题约简性质。我们相信，上下文演算将作为开发具有高级功能的编程语言的基础，这些功能要求对开放术语进行操作。
This paper develops a typed calculus for contexts i.e., lambda terms with “holes”. In addition to ordinary lambda terms, the calculus contains labeled holes, hole abstraction and context application for manipulating first-class contexts. The primary operation for contexts is hole-filling, which captures free variables. This operation conflicts with substitution of the lambda calculus, and a straightforward mixture of the two results in an inconsistent system. We solve this problem by defining a type system that precisely specifies the variable-capturing nature of contexts and that keeps track of bound variable renaming. These mechanisms enable us to define a reduction system that properly integrates β-reduction and hole-filling. The resulting calculus is Church–Rosser and the type system has the subject reduction property. We believe that the context calculus will serve as a basis for developing a programming language with advanced features that call for manipulation of open terms.