Reduction and Unification in Lambda Calculi with Subtypes

Tobias Nipkow, Zhenyu Qian

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.

A generic algorithm for pre-unification modulo beta-eta-conversion and an arbitrary subtype relation is presented. Furthermore it is shown that unification w.r.t. any subtype relation is universal.

SpringerLink

BibTeX:

@inproceedings{Nipkow-Qian-CADE-92,
author="Tobias Nipkow and Zhenyu Qian",
title="Reduction and Unification in Lambda Calculi with Subtypes",
booktitle="Proc.\ 11th Int.\ Conf.\ Automated Deduction",year=1992,
editor="Deepak Kapur",
publisher=Springer,series=LNCS,volume=607,pages="66--78"}

A revised version appeared in Journal of Automated Reasoning.