Reduction and unification in lambda calculi with a general notion of subtype |
| |
Authors: | Zhenyu Qian Tobias Nipkow |
| |
Affiliation: | (1) FB3 Informatik, Universität Bremen, Bibliothekstr., 28359 Bremen, Germany;(2) Institut für Informatik, Technische Universität München, Arcisstr. 21, 80290 Munich, Germany |
| |
Abstract: | 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, that is, 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. We present a generic algorithm for preunification modulo ![beta](/content/r2442w0717406g0v/xxlarge946.gif) -conversion and an arbitrary subtype relation. Furthermore it is shown that unification with respect to any subtype relation is universal. |
| |
Keywords: | simply typed -calculi" target="_blank">gif" alt="lambda" align="BASELINE" BORDER="0">-calculi subtypes reduction higher-order unification |
本文献已被 SpringerLink 等数据库收录! |
|