Strong normalizability for the combined system of the typed lambda calculus and an arbitrary convergent term rewrite system

Research output: Chapter in Book/Report/Conference proceedingConference contribution

32 Citations (Scopus)

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.

Original languageEnglish
Title of host publicationProceedings of the ACM-SIGSAM 1989 International Symposium on Symbolic and Algebraic Computation, ISSAC 1989
PublisherAssociation for Computing Machinery
Pages357-363
Number of pages7
VolumePart F130182
ISBN (Electronic)0897913256
DOIs
Publication statusPublished - 1989 Jul 17
Externally publishedYes
Event1989 ACM-SIGSAM International Symposium on Symbolic and Algebraic Computation, ISSAC 1989 - Portland, United States
Duration: 1989 Jul 171989 Jul 19

Other

Other1989 ACM-SIGSAM International Symposium on Symbolic and Algebraic Computation, ISSAC 1989
CountryUnited States
CityPortland
Period89/7/1789/7/19

Fingerprint

Term Rewriting Systems
Typed lambda Calculus
Calculus
Arbitrary
Term
Strong Normalization
Open Problems

ASJC Scopus subject areas

  • Mathematics(all)

Cite this

Okada, M. (1989). Strong normalizability for the combined system of the typed lambda calculus and an arbitrary convergent term rewrite system. In Proceedings of the ACM-SIGSAM 1989 International Symposium on Symbolic and Algebraic Computation, ISSAC 1989 (Vol. Part F130182, pp. 357-363). Association for Computing Machinery. https://doi.org/10.1145/74540.74582

Strong normalizability for the combined system of the typed lambda calculus and an arbitrary convergent term rewrite system. / Okada, Mitsuhiro.

Proceedings of the ACM-SIGSAM 1989 International Symposium on Symbolic and Algebraic Computation, ISSAC 1989. Vol. Part F130182 Association for Computing Machinery, 1989. p. 357-363.

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Okada, M 1989, Strong normalizability for the combined system of the typed lambda calculus and an arbitrary convergent term rewrite system. in Proceedings of the ACM-SIGSAM 1989 International Symposium on Symbolic and Algebraic Computation, ISSAC 1989. vol. Part F130182, Association for Computing Machinery, pp. 357-363, 1989 ACM-SIGSAM International Symposium on Symbolic and Algebraic Computation, ISSAC 1989, Portland, United States, 89/7/17. https://doi.org/10.1145/74540.74582
Okada M. Strong normalizability for the combined system of the typed lambda calculus and an arbitrary convergent term rewrite system. In Proceedings of the ACM-SIGSAM 1989 International Symposium on Symbolic and Algebraic Computation, ISSAC 1989. Vol. Part F130182. Association for Computing Machinery. 1989. p. 357-363 https://doi.org/10.1145/74540.74582
Okada, Mitsuhiro. / Strong normalizability for the combined system of the typed lambda calculus and an arbitrary convergent term rewrite system. Proceedings of the ACM-SIGSAM 1989 International Symposium on Symbolic and Algebraic Computation, ISSAC 1989. Vol. Part F130182 Association for Computing Machinery, 1989. pp. 357-363
@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",
year = "1989",
month = "7",
day = "17",
doi = "10.1145/74540.74582",
language = "English",
volume = "Part F130182",
pages = "357--363",
booktitle = "Proceedings of the ACM-SIGSAM 1989 International Symposium on Symbolic and Algebraic Computation, ISSAC 1989",
publisher = "Association for Computing Machinery",

}

TY - GEN

T1 - Strong normalizability for the combined system of the typed lambda calculus and an arbitrary convergent term rewrite system

AU - Okada, Mitsuhiro

PY - 1989/7/17

Y1 - 1989/7/17

N2 - 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.

AB - 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.

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

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

U2 - 10.1145/74540.74582

DO - 10.1145/74540.74582

M3 - Conference contribution

VL - Part F130182

SP - 357

EP - 363

BT - Proceedings of the ACM-SIGSAM 1989 International Symposium on Symbolic and Algebraic Computation, ISSAC 1989

PB - Association for Computing Machinery

ER -