Title: Strong normalizability for the combined system of the typed lmbda calculus and an arbitrary convergent term rewrite system
Abstract: We give a proof of strong normalizability of the typed λ-calculus 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.
Publication Year: 1989
Publication Date: 1989-01-01
Language: en
Type: article
Indexed In: ['crossref']
Access and Citation
Cited By Count: 47
AI Researcher Chatbot
Get quick answers to your questions about the article from our AI researcher chatbot