Reduction and Unification in Lambda Calculi with a General Notion of
Subtype
Zhenyu Qian, Tobias Nipkow
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.
BibTeX:
<![CDATA[
@article{Qian-Nipkow-JAR,author="Zhenyu Qian and Tobias Nipkow",
title=
"Reduction and Unification in Lambda Calculi with a General Notion of Subtype",
journal=JAR,volume=12,pages={389--406},year=1994}
]]></plaintext></p></div></div>