A Simply Typed Context Calculus with First-class Environments
A Simply Typed Context Calculus with First-class Environments
复制标题
具有一流环境的简单类型上下文演算
DOI：
10.1007/3-540-44716-4_23
复制
发表时间：
2001
影响因子：
--
通讯作者：
Yukiyoshi Kameyama
中科院分区：
文献类型：
--
作者：
M. Sato;Takafumi Sakurai;Yukiyoshi Kameyama
我们介绍了一个简单键入的λ-calculusλϰɛ“，它既有上下文和环境作为一流的值。在λϰɛ中”，上下文中的孔由适当类型的普通变量表示，孔填充代表了功能应用程序，以及新的孔。填充术语的抽象机制，用于填充上下文的孔。 λβ-Calculus具有降低主体，是汇合且稳固的正常化。
定义替代的传统方法对我们的计算不起作用。替代。
We introduce a simply typed λ-calculus λϰƐ" which has both contexts and environments as first-class values. In λϰƐ", holes in contexts are represented by ordinary variables of appropriate types and hole filling is represented by the functional application together with a new abstraction mechanism which takes care of packing and unpacking of the term which is used to fill in the holes of the context. λϰƐ" is a conservative extension of the simply typed λβ-calculus, enjoys subject reduction property, is confluent and strongly normalizing.
The traditional method of defining substitution does not work for our calculus. So, we also introduce a new method of defining substitution. Although we introduce the new definition of substitution out of necessity, the new definition turns out to be conceptually simpler than the traditional definition of substitution.