Reduction and Unification in Lambda Calculi with Subtypes
Reduction and Unification in Lambda Calculi with Subtypes
复制标题
具有子类型的 Lambda 演算的约简和统一
DOI：
--
复制
发表时间：
1992
期刊：
影响因子：
--
通讯作者：
Zhenyu Qian
中科院分区：
文献类型：
--
作者：
T. Nipkow;Zhenyu Qian
研究了一族带子类型的单型λ-演算的约化、相等和统一问题。子类型关系只需要将基类型与基类型相关联，并满足某些序理论条件。常量必须有一个最小的类型，即“没有重载”。我们定义了通常的β和子类型依赖的η-约化。它们与一个类型化的等式关系有关，并且在某种意义上是合流的。
Reduction, equality and unification are studied for a family of simply typed λ-calculi with subtypes. The subtype relation is required to relate base types only to base types and to satisfy some order-theoretic conditions. Constants are required to have a least type, i.e. “no overloading”. We define the usual β and a subtype-dependent η-reduction. These are related to a typed equality relation and shown to be confluent in a certain sense.