Reduction and unification in lambda calculi with subtypes

Tobias Nipkow; Zhenyu Qian

doi:10.1007/3-540-55602-8_156

Reduction and unification in lambda calculi with subtypes

Tobias Nipkow, Zhenyu Qian

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

4 Scopus citations

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, 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. A generic algorithm for pre-unification modulo βη-conversion and an arbitrary subtype relation is presented. Furthermore it is shown that unification w.r.t. any subtype relation is universal.

Original language	English
Title of host publication	Automated Deduction — CADE-11 - 11 th International Conference on Automated Deduction, Proceedings
Editors	Deepak Kapur
Publisher	Springer Verlag
Pages	66-78
Number of pages	13
ISBN (Print)	9783540556022
DOIs	https://doi.org/10.1007/3-540-55602-8_156
State	Published - 1992
Externally published	Yes
Event	11th International Conference on Automated Deduction, CADE, 1992 - Saratoga Springs, United States Duration: 15 Jun 1992 → 18 Jun 1992

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	607 LNAI
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	11th International Conference on Automated Deduction, CADE, 1992
Country/Territory	United States
City	Saratoga Springs
Period	15/06/92 → 18/06/92

Access to Document

10.1007/3-540-55602-8_156

Cite this

Nipkow, T., & Qian, Z. (1992). Reduction and unification in lambda calculi with subtypes. In D. Kapur (Ed.), Automated Deduction — CADE-11 - 11 th International Conference on Automated Deduction, Proceedings (pp. 66-78). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 607 LNAI). Springer Verlag. https://doi.org/10.1007/3-540-55602-8_156

Nipkow, Tobias ; Qian, Zhenyu. / Reduction and unification in lambda calculi with subtypes. Automated Deduction — CADE-11 - 11 th International Conference on Automated Deduction, Proceedings. editor / Deepak Kapur. Springer Verlag, 1992. pp. 66-78 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{d07f55fcf7224892a4a7c7b27de1c7a7,

title = "Reduction and unification in lambda calculi with subtypes",

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, 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. A generic algorithm for pre-unification modulo βη-conversion and an arbitrary subtype relation is presented. Furthermore it is shown that unification w.r.t. any subtype relation is universal.",

author = "Tobias Nipkow and Zhenyu Qian",

note = "Publisher Copyright: {\textcopyright} Springer-Verlag Berlin Heidelberg 1994.; 11th International Conference on Automated Deduction, CADE, 1992 ; Conference date: 15-06-1992 Through 18-06-1992",

year = "1992",

doi = "10.1007/3-540-55602-8_156",

language = "English",

isbn = "9783540556022",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Verlag",

pages = "66--78",

editor = "Deepak Kapur",

booktitle = "Automated Deduction — CADE-11 - 11 th International Conference on Automated Deduction, Proceedings",

}

Nipkow, T & Qian, Z 1992, Reduction and unification in lambda calculi with subtypes. in D Kapur (ed.), Automated Deduction — CADE-11 - 11 th International Conference on Automated Deduction, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 607 LNAI, Springer Verlag, pp. 66-78, 11th International Conference on Automated Deduction, CADE, 1992, Saratoga Springs, United States, 15/06/92. https://doi.org/10.1007/3-540-55602-8_156

Reduction and unification in lambda calculi with subtypes. / Nipkow, Tobias; Qian, Zhenyu.
Automated Deduction — CADE-11 - 11 th International Conference on Automated Deduction, Proceedings. ed. / Deepak Kapur. Springer Verlag, 1992. p. 66-78 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 607 LNAI).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - Reduction and unification in lambda calculi with subtypes

AU - Nipkow, Tobias

AU - Qian, Zhenyu

N1 - Publisher Copyright: © Springer-Verlag Berlin Heidelberg 1994.

PY - 1992

Y1 - 1992

N2 - 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. A generic algorithm for pre-unification modulo βη-conversion and an arbitrary subtype relation is presented. Furthermore it is shown that unification w.r.t. any subtype relation is universal.

AB - 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. A generic algorithm for pre-unification modulo βη-conversion and an arbitrary subtype relation is presented. Furthermore it is shown that unification w.r.t. any subtype relation is universal.

UR - http://www.scopus.com/inward/record.url?scp=85026901463&partnerID=8YFLogxK

U2 - 10.1007/3-540-55602-8_156

DO - 10.1007/3-540-55602-8_156

M3 - Conference contribution

AN - SCOPUS:85026901463

SN - 9783540556022

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 66

EP - 78

BT - Automated Deduction — CADE-11 - 11 th International Conference on Automated Deduction, Proceedings

A2 - Kapur, Deepak

PB - Springer Verlag

T2 - 11th International Conference on Automated Deduction, CADE, 1992

Y2 - 15 June 1992 through 18 June 1992

ER -

Nipkow T, Qian Z. Reduction and unification in lambda calculi with subtypes. In Kapur D, editor, Automated Deduction — CADE-11 - 11 th International Conference on Automated Deduction, Proceedings. Springer Verlag. 1992. p. 66-78. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/3-540-55602-8_156

Reduction and unification in lambda calculi with subtypes

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Cite this