@inproceedings{542054a24dd24d39974716a518147f34,
title = "Strong normalizability for the combined system of the typed lambda calculus and an arbitrary convergent term rewrite system",
abstract = "We give a proof of strong normalizability of the typed λ-calculas extended by an arbitrary convergent term rewriting system, which provides the affirmative answer to the open problem proposed in Breazu-Tannen [1]. Klop [6] showed that a combined system of the untyped λ-calculus and convergent term rewriting system is not Church-Rosser in general, though both are Church-Rosser. It is well-known that the typed λ-calculus is convergent (Church-Rosser and terminating). Breazu-Tannen [1] showed that a combined system of the typed λ-calculus and an arbitrary Church-Rosser term rewriting system is again Church-Rosser. Our strong normalization result in this paper shows that the combined system of the typed λ-calculus and an arbitrary convergent term rewriting system is again convergent. Our strong normalizability proof is easily extended to the case of the second order (polymorphically) typed lambda calculus and the case in which μ-reduction rule is added.",
author = "Mitsuhiro Okada",
note = "Funding Information: This work was partly supported by the Natural Science and Engineering Research Council of Canada, grant OGPO036663 and ICR0039976, Fonds pour la Formation de Rechercheur et l{\textquoteright}Aide & la Recherche, grant 89EQ4184, Social Science and Humanities Research Council of Canada, grant 410-88-0884, and the Committee on Aid to Research Activity of Concordia University. A part of this work was done when the author was visiting Universite de Paris XI, Orsay, France. The author wishes to thank those who attended his lectures at Laboratoire de Recherche Informatique at Orsay, esPeciallY Professors Common, Gaudel, Hsiang, Jouannaud, Rusinowitch, for their comments. In particular, the discussion with Prof. Jouannaud was very essential for this work. The authors would also like to express their thanks to Professors Dershowitz, Lascanne, &my, P. J. Scott and Toyama for discussion on related topics. Publisher Copyright: {\textcopyright} 1989 ACM.; 1989 ACM-SIGSAM International Symposium on Symbolic and Algebraic Computation, ISSAC 1989 ; Conference date: 17-07-1989 Through 19-07-1989",
year = "1989",
month = jul,
day = "17",
doi = "10.1145/74540.74582",
language = "English",
series = "Proceedings of the International Symposium on Symbolic and Algebraic Computation, ISSAC",
publisher = "Association for Computing Machinery",
pages = "357--363",
editor = "Gonnet, {G. H.}",
booktitle = "Proceedings of the ACM-SIGSAM 1989 International Symposium on Symbolic and Algebraic Computation, ISSAC 1989",
}