Reduction and Unification in Lambda Calculi with a General Notion of Subtype

Abstract:

Reduction, equality and unification are studied for a family of simply typed lambda 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 beta- and a subtype-dependent eta-reduction. These are related to a typed equality relation and shown to be confluent in a certain sense. We present a generic algorithm for pre-unification modulo beta-eta-conversion and an arbitrary subtype relation. Furthermore it is shown that unification with respect to any subtype relation is universal.

The paper is here.

FTP: ftp.uni-bremen.de:/pub/ZKW/INFORM/qian/hosu.ps.gz

For a preprint send a message to Zhenyu Qian.